Skip to content

Commit

Permalink
Remove Array8, Array16 and Array32 types
Browse files Browse the repository at this point in the history
  • Loading branch information
Kmeakin committed Feb 13, 2023
1 parent 3960a94 commit 45d6d7b
Show file tree
Hide file tree
Showing 50 changed files with 358 additions and 465 deletions.
20 changes: 7 additions & 13 deletions fathom/src/core.rs
Original file line number Diff line number Diff line change
Expand Up @@ -333,13 +333,7 @@ def_prims! {
OptionType => "Option",
/// Type of dynamically sized arrays.
ArrayType => "Array",
/// Type of arrays, with 8-bit indices.
Array8Type => "Array8",
/// Type of arrays, with 16-bit indices.
Array16Type => "Array16",
/// Type of arrays, with 32-bit indices.
Array32Type => "Array32",
/// Type of arrays, with 64-bit indices.
/// Type of fixed size arrays, with 64-bit indices.
Array64Type => "Array64",
/// Type of stream positions.
PosType => "Pos",
Expand Down Expand Up @@ -384,12 +378,6 @@ def_prims! {
FormatF64Be => "f64be",
/// 64-bit, IEEE-754 floating point formats (little-endian).
FormatF64Le => "f64le",
/// Repeat formats up to an unsigned 8-bit length.
FormatRepeatLen8 => "repeat_len8",
/// Repeat formats up to an unsigned 16-bit length.
FormatRepeatLen16 => "repeat_len16",
/// Repeat formats up to an unsigned 32-bit length.
FormatRepeatLen32 => "repeat_len32",
/// Repeat formats up to an unsigned 64-bit length.
FormatRepeatLen64 => "repeat_len64",
/// Repeat a format until the length of the given parse scope is reached.
Expand Down Expand Up @@ -444,6 +432,9 @@ def_prims! {
U8And => "u8_and",
U8Or => "u8_or",
U8Xor => "u8_xor",
U8ExtendU16 => "u8_extend_u16",
U8ExtendU32 => "u8_extend_u32",
U8ExtendU64 => "u8_extend_u64",

U16Eq => "u16_eq",
U16Neq => "u16_neq",
Expand All @@ -461,6 +452,8 @@ def_prims! {
U16And => "u16_and",
U16Or => "u16_or",
U16Xor => "u16_xor",
U16ExtendU32 => "u16_extend_u32",
U16ExtendU64 => "u16_extend_u64",

U32Eq => "u32_eq",
U32Neq => "u32_neq",
Expand All @@ -478,6 +471,7 @@ def_prims! {
U32And => "u32_and",
U32Or => "u32_or",
U32Xor => "u32_xor",
U32ExtendU64 => "u32_extend_u64",

U64Eq => "u64_eq",
U64Neq => "u64_neq",
Expand Down
3 changes: 0 additions & 3 deletions fathom/src/core/binary.rs
Original file line number Diff line number Diff line change
Expand Up @@ -425,9 +425,6 @@ impl<'arena, 'data> Context<'arena, 'data> {
(Prim::FormatF32Le, []) => read_const(reader, span, read_f32le, Const::F32),
(Prim::FormatF64Be, []) => read_const(reader, span, read_f64be, Const::F64),
(Prim::FormatF64Le, []) => read_const(reader, span, read_f64le, Const::F64),
(Prim::FormatRepeatLen8, [FunApp(_, len), FunApp(_, format)]) => self.read_repeat_len(reader, span, len, format),
(Prim::FormatRepeatLen16, [FunApp(_, len), FunApp(_, format)]) => self.read_repeat_len(reader, span, len, format),
(Prim::FormatRepeatLen32, [FunApp(_, len), FunApp(_, format)]) => self.read_repeat_len(reader, span, len, format),
(Prim::FormatRepeatLen64, [FunApp(_, len), FunApp(_, format)]) => self.read_repeat_len(reader, span, len, format),
(Prim::FormatRepeatUntilEnd, [FunApp(_,format)]) => self.read_repeat_until_end(reader, format),
(Prim::FormatLimit8, [FunApp(_, limit), FunApp(_, format)]) => self.read_limit(reader, limit, format),
Expand Down
36 changes: 12 additions & 24 deletions fathom/src/core/prim.rs
Original file line number Diff line number Diff line change
Expand Up @@ -46,9 +46,6 @@ impl<'arena> Env<'arena> {
const S16_TYPE: Term<'_> = Term::Prim(Span::Empty, S16Type);
const S32_TYPE: Term<'_> = Term::Prim(Span::Empty, S32Type);
const S64_TYPE: Term<'_> = Term::Prim(Span::Empty, S64Type);
const ARRAY8_TYPE: Term<'_> = Term::Prim(Span::Empty, Array8Type);
const ARRAY16_TYPE: Term<'_> = Term::Prim(Span::Empty, Array16Type);
const ARRAY32_TYPE: Term<'_> = Term::Prim(Span::Empty, Array32Type);
const ARRAY64_TYPE: Term<'_> = Term::Prim(Span::Empty, Array64Type);
const POS_TYPE: Term<'_> = Term::Prim(Span::Empty, PosType);

Expand All @@ -68,9 +65,6 @@ impl<'arena> Env<'arena> {
env.define_prim(F64Type, &UNIVERSE);
env.define_prim_fun(OptionType, [&UNIVERSE], &UNIVERSE);
env.define_prim_fun(ArrayType, [&UNIVERSE], &UNIVERSE);
env.define_prim_fun(Array8Type, [&U8_TYPE, &UNIVERSE], &UNIVERSE);
env.define_prim_fun(Array16Type, [&U16_TYPE, &UNIVERSE], &UNIVERSE);
env.define_prim_fun(Array32Type, [&U32_TYPE, &UNIVERSE], &UNIVERSE);
env.define_prim_fun(Array64Type, [&U64_TYPE, &UNIVERSE], &UNIVERSE);
env.define_prim(PosType, &UNIVERSE);
env.define_prim_fun(RefType, [&FORMAT_TYPE], &UNIVERSE);
Expand All @@ -94,9 +88,6 @@ impl<'arena> Env<'arena> {
env.define_prim(FormatF32Le, &FORMAT_TYPE);
env.define_prim(FormatF64Be, &FORMAT_TYPE);
env.define_prim(FormatF64Le, &FORMAT_TYPE);
env.define_prim_fun(FormatRepeatLen8, [&U8_TYPE, &FORMAT_TYPE], &FORMAT_TYPE);
env.define_prim_fun(FormatRepeatLen16, [&U16_TYPE, &FORMAT_TYPE], &FORMAT_TYPE);
env.define_prim_fun(FormatRepeatLen32, [&U32_TYPE, &FORMAT_TYPE], &FORMAT_TYPE);
env.define_prim_fun(FormatRepeatLen64, [&U64_TYPE, &FORMAT_TYPE], &FORMAT_TYPE);
env.define_prim_fun(FormatRepeatUntilEnd, [&FORMAT_TYPE], &FORMAT_TYPE);
env.define_prim_fun(FormatLimit8, [&U8_TYPE, &FORMAT_TYPE], &FORMAT_TYPE);
Expand Down Expand Up @@ -197,6 +188,9 @@ impl<'arena> Env<'arena> {
env.define_prim_fun(U8And, [&U8_TYPE, &U8_TYPE], &U8_TYPE);
env.define_prim_fun(U8Or, [&U8_TYPE, &U8_TYPE], &U8_TYPE);
env.define_prim_fun(U8Xor, [&U8_TYPE, &U8_TYPE], &U8_TYPE);
env.define_prim_fun(U8ExtendU16, [&U8_TYPE], &U16_TYPE);
env.define_prim_fun(U8ExtendU32, [&U8_TYPE], &U32_TYPE);
env.define_prim_fun(U8ExtendU64, [&U8_TYPE], &U64_TYPE);

env.define_prim_fun(U16Eq, [&U16_TYPE, &U16_TYPE], &BOOL_TYPE);
env.define_prim_fun(U16Neq, [&U16_TYPE, &U16_TYPE], &BOOL_TYPE);
Expand All @@ -214,6 +208,8 @@ impl<'arena> Env<'arena> {
env.define_prim_fun(U16And, [&U16_TYPE, &U16_TYPE], &U16_TYPE);
env.define_prim_fun(U16Or, [&U16_TYPE, &U16_TYPE], &U16_TYPE);
env.define_prim_fun(U16Xor, [&U16_TYPE, &U16_TYPE], &U16_TYPE);
env.define_prim_fun(U16ExtendU32, [&U16_TYPE], &U32_TYPE);
env.define_prim_fun(U16ExtendU64, [&U16_TYPE], &U64_TYPE);

env.define_prim_fun(U32Eq, [&U32_TYPE, &U32_TYPE], &BOOL_TYPE);
env.define_prim_fun(U32Neq, [&U32_TYPE, &U32_TYPE], &BOOL_TYPE);
Expand All @@ -231,6 +227,7 @@ impl<'arena> Env<'arena> {
env.define_prim_fun(U32And, [&U32_TYPE, &U32_TYPE], &U32_TYPE);
env.define_prim_fun(U32Or, [&U32_TYPE, &U32_TYPE], &U32_TYPE);
env.define_prim_fun(U32Xor, [&U32_TYPE, &U32_TYPE], &U32_TYPE);
env.define_prim_fun(U32ExtendU64, [&U32_TYPE], &U64_TYPE);

env.define_prim_fun(U64Eq, [&U64_TYPE, &U64_TYPE], &BOOL_TYPE);
env.define_prim_fun(U64Neq, [&U64_TYPE, &U64_TYPE], &BOOL_TYPE);
Expand Down Expand Up @@ -437,13 +434,7 @@ impl<'arena> Env<'arena> {
)),
))
};
let array8_find_type = find_type(&U8_TYPE, &ARRAY8_TYPE);
let array16_find_type = find_type(&U16_TYPE, &ARRAY16_TYPE);
let array32_find_type = find_type(&U32_TYPE, &ARRAY32_TYPE);
let array64_find_type = find_type(&U64_TYPE, &ARRAY64_TYPE);
env.define_prim(Array8Find, array8_find_type);
env.define_prim(Array16Find, array16_find_type);
env.define_prim(Array32Find, array32_find_type);
env.define_prim(Array64Find, array64_find_type);

// fun (@len : UN) (@A : Type) (index : UN) -> ArrayN len A -> A
Expand Down Expand Up @@ -486,13 +477,7 @@ impl<'arena> Env<'arena> {
)),
))
};
let array8_index_type = array_index_type(&U8_TYPE, &ARRAY8_TYPE);
let array16_index_type = array_index_type(&U16_TYPE, &ARRAY16_TYPE);
let array32_index_type = array_index_type(&U32_TYPE, &ARRAY32_TYPE);
let array64_index_type = array_index_type(&U64_TYPE, &ARRAY64_TYPE);
env.define_prim(Array8Index, array8_index_type);
env.define_prim(Array16Index, array16_index_type);
env.define_prim(Array32Index, array32_index_type);
env.define_prim(Array64Index, array64_index_type);

env.define_prim_fun(PosAddU8, [&POS_TYPE, &U8_TYPE], &POS_TYPE);
Expand Down Expand Up @@ -611,9 +596,6 @@ pub fn repr(prim: Prim) -> Step {
Prim::FormatF32Le => step!(_, [] => Spanned::empty(Arc::new(Value::prim(Prim::F32Type, [])))),
Prim::FormatF64Be => step!(_, [] => Spanned::empty(Arc::new(Value::prim(Prim::F64Type, [])))),
Prim::FormatF64Le => step!(_, [] => Spanned::empty(Arc::new(Value::prim(Prim::F64Type, [])))),
Prim::FormatRepeatLen8 => step!(env, [len, elem] => Spanned::empty(Arc::new(Value::prim(Prim::Array8Type, [len.clone(), env.format_repr(elem)])))),
Prim::FormatRepeatLen16 => step!(env, [len, elem] => Spanned::empty(Arc::new(Value::prim(Prim::Array16Type, [len.clone(), env.format_repr(elem)])))),
Prim::FormatRepeatLen32 => step!(env, [len, elem] => Spanned::empty(Arc::new(Value::prim(Prim::Array32Type, [len.clone(), env.format_repr(elem)])))),
Prim::FormatRepeatLen64 => step!(env, [len, elem] => Spanned::empty(Arc::new(Value::prim(Prim::Array64Type, [len.clone(), env.format_repr(elem)])))),
Prim::FormatLimit8 => step!(env, [_, elem] => env.format_repr(elem)),
Prim::FormatLimit16 => step!(env, [_, elem] => env.format_repr(elem)),
Expand Down Expand Up @@ -666,6 +648,9 @@ pub fn step(prim: Prim) -> Step {
Prim::U8And => const_step!([x, xst: U8, y, yst: U8] => Const::U8(u8::bitand(*x, *y), UIntStyle::merge(*xst, *yst))),
Prim::U8Or => const_step!([x, xst: U8, y, yst: U8] => Const::U8(u8::bitor(*x, *y), UIntStyle::merge(*xst, *yst))),
Prim::U8Xor => const_step!([x, xst: U8, y, yst: U8] => Const::U8(u8::bitxor(*x, *y), UIntStyle::merge(*xst, *yst))),
Prim::U8ExtendU16 => const_step!([x, xst: U8] => Const::U16(u16::from(*x), *xst)),
Prim::U8ExtendU32 => const_step!([x, xst: U8] => Const::U32(u32::from(*x), *xst)),
Prim::U8ExtendU64 => const_step!([x, xst: U8] => Const::U64(u64::from(*x), *xst)),

Prim::U16Eq => const_step!([x: U16, y: U16] => Const::Bool(x == y)),
Prim::U16Neq => const_step!([x: U16, y: U16] => Const::Bool(x != y)),
Expand All @@ -683,6 +668,8 @@ pub fn step(prim: Prim) -> Step {
Prim::U16And => const_step!([x, xst: U16, y, yst: U16] => Const::U16(u16::bitand(*x, *y), UIntStyle::merge(*xst, *yst))),
Prim::U16Or => const_step!([x, xst: U16, y, yst: U16] => Const::U16(u16::bitor(*x, *y), UIntStyle::merge(*xst, *yst))),
Prim::U16Xor => const_step!([x, xst: U16, y, yst: U16] => Const::U16(u16::bitxor(*x, *y), UIntStyle::merge(*xst, *yst))),
Prim::U16ExtendU32 => const_step!([x, xst: U16] => Const::U32(u32::from(*x), *xst)),
Prim::U16ExtendU64 => const_step!([x, xst: U16] => Const::U64(u64::from(*x), *xst)),

Prim::U32Eq => const_step!([x: U32, y: U32] => Const::Bool(x == y)),
Prim::U32Neq => const_step!([x: U32, y: U32] => Const::Bool(x != y)),
Expand All @@ -700,6 +687,7 @@ pub fn step(prim: Prim) -> Step {
Prim::U32And => const_step!([x, xst: U32, y, yst: U32] => Const::U32(u32::bitand(*x, *y), UIntStyle::merge(*xst, *yst))),
Prim::U32Or => const_step!([x, xst: U32, y, yst: U32] => Const::U32(u32::bitor(*x, *y), UIntStyle::merge(*xst, *yst))),
Prim::U32Xor => const_step!([x, xst: U32, y, yst: U32] => Const::U32(u32::bitxor(*x, *y), UIntStyle::merge(*xst, *yst))),
Prim::U32ExtendU64 => const_step!([x, xst: U32] => Const::U64(u64::from(*x), *xst)),

Prim::U64Eq => const_step!([x: U64, y: U64] => Const::Bool(x == y)),
Prim::U64Neq => const_step!([x: U64, y: U64] => Const::Bool(x != y)),
Expand Down
94 changes: 55 additions & 39 deletions fathom/src/surface/elaboration.rs
Original file line number Diff line number Diff line change
Expand Up @@ -597,28 +597,62 @@ impl<'arena> Context<'arena> {
)
}

// Otherwise, unify the types
(_, _) => match self.unification_context().unify(&from, &to) {
Ok(()) => expr,
Err(error) => {
let range = match span {
Span::Range(range) => range,
Span::Empty => {
let range = self.file_range(surface_range);
self.push_message(Message::MissingSpan { range });
range
}
};
(_, _) => {
// Implictly extend unsigned integer types
let extend_prim = match Option::zip(from.match_prim_spine(), to.match_prim_spine())
{
Some(((Prim::U8Type, []), (Prim::U16Type, []))) => Prim::U8ExtendU16,
Some(((Prim::U8Type, []), (Prim::U32Type, []))) => Prim::U8ExtendU32,
Some(((Prim::U8Type, []), (Prim::U64Type, []))) => Prim::U8ExtendU64,

self.push_message(Message::FailedToUnify {
range,
found: self.pretty_value(&from),
expected: self.pretty_value(&to),
error,
});
core::Term::Prim(span, Prim::ReportedError)
}
},
Some(((Prim::U16Type, []), (Prim::U32Type, []))) => Prim::U16ExtendU32,
Some(((Prim::U16Type, []), (Prim::U64Type, []))) => Prim::U16ExtendU64,

Some(((Prim::U32Type, []), (Prim::U64Type, []))) => Prim::U32ExtendU64,

// Otherwise, unify the types
_ => return self.convert(surface_range, expr, &from, &to),
};

core::Term::FunApp(
span,
Plicity::Explicit,
self.scope.to_scope(core::Term::Prim(span, extend_prim)),
self.scope.to_scope(expr),
)
}
}
}

fn convert(
&mut self,
surface_range: ByteRange, /* TODO: could be removed if we never encounter empty spans in
* the core term */
expr: core::Term<'arena>,
from: &ArcValue<'arena>,
to: &ArcValue<'arena>,
) -> core::Term<'arena> {
let span = expr.span();
match self.unification_context().unify(from, to) {
Ok(()) => expr,
Err(error) => {
let range = match span {
Span::Range(range) => range,
Span::Empty => {
let range = self.file_range(surface_range);
self.push_message(Message::MissingSpan { range });
range
}
};

self.push_message(Message::FailedToUnify {
range,
found: self.pretty_value(from),
expected: self.pretty_value(to),
error,
});
core::Term::Prim(span, Prim::ReportedError)
}
}
}

Expand Down Expand Up @@ -734,9 +768,6 @@ impl<'arena> Context<'arena> {
Some((Prim::U16Type, [])) => self.parse_ascii(*range, *lit, Const::U16),
Some((Prim::U32Type, [])) => self.parse_ascii(*range, *lit, Const::U32),
Some((Prim::U64Type, [])) => self.parse_ascii(*range, *lit, Const::U64),
// Some((Prim::Array8Type, [len, _])) => todo!(),
// Some((Prim::Array16Type, [len, _])) => todo!(),
// Some((Prim::Array32Type, [len, _])) => todo!(),
// Some((Prim::Array64Type, [len, _])) => todo!(),
Some((Prim::ReportedError, _)) => None,
_ => {
Expand Down Expand Up @@ -1141,15 +1172,6 @@ impl<'arena> Context<'arena> {

let (len_value, elem_type) = match expected_type.match_prim_spine() {
Some((Prim::ArrayType, [App(_, elem_type)])) => (None, elem_type),
Some((Prim::Array8Type, [App(_, len), App(_, elem_type)])) => {
(Some(len), elem_type)
}
Some((Prim::Array16Type, [App(_, len), App(_, elem_type)])) => {
(Some(len), elem_type)
}
Some((Prim::Array32Type, [App(_, len), App(_, elem_type)])) => {
(Some(len), elem_type)
}
Some((Prim::Array64Type, [App(_, len), App(_, elem_type)])) => {
(Some(len), elem_type)
}
Expand All @@ -1167,9 +1189,6 @@ impl<'arena> Context<'arena> {

let len = match len_value.map(|val| val.as_ref()) {
None => Some(elem_exprs.len() as u64),
Some(Value::ConstLit(Const::U8(len, _))) => Some(*len as u64),
Some(Value::ConstLit(Const::U16(len, _))) => Some(*len as u64),
Some(Value::ConstLit(Const::U32(len, _))) => Some(*len as u64),
Some(Value::ConstLit(Const::U64(len, _))) => Some(*len),
Some(Value::Stuck(Head::Prim(Prim::ReportedError), _)) => {
return core::Term::Prim(file_range.into(), Prim::ReportedError);
Expand Down Expand Up @@ -1207,9 +1226,6 @@ impl<'arena> Context<'arena> {
Some((Prim::U16Type, [])) => self.parse_ascii(*range, *lit, Const::U16),
Some((Prim::U32Type, [])) => self.parse_ascii(*range, *lit, Const::U32),
Some((Prim::U64Type, [])) => self.parse_ascii(*range, *lit, Const::U64),
// Some((Prim::Array8Type, [len, _])) => todo!(),
// Some((Prim::Array16Type, [len, _])) => todo!(),
// Some((Prim::Array32Type, [len, _])) => todo!(),
// Some((Prim::Array64Type, [len, _])) => todo!(),
Some((Prim::ReportedError, _)) => None,
_ => {
Expand Down
2 changes: 1 addition & 1 deletion formats/edid.fathom
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ def chromacity_coordinates = {
};

def established_timing = {
mode_bitmap <- repeat_len8 3 u8, // TODO: bit patterns
mode_bitmap <- repeat_len64 3 u8, // TODO: bit patterns
};

def standard_timing_information : Format = {
Expand Down
2 changes: 1 addition & 1 deletion formats/edid.snap
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ def chromacity_coordinates : Format = {
white_x_msb <- u8,
white_y_msb <- u8,
};
def established_timing : Format = { mode_bitmap <- repeat_len8 3 u8 };
def established_timing : Format = { mode_bitmap <- repeat_len64 3 u8 };
def standard_timing_information : Format = ();
def main : Format = {
header <- header,
Expand Down
6 changes: 3 additions & 3 deletions formats/gif.fathom
Original file line number Diff line number Diff line change
Expand Up @@ -29,8 +29,8 @@ def logical_screen_descriptor = {
///
/// - [GIF89a Specification: Section 17](https://www.w3.org/Graphics/GIF/spec-gif89a.txt)
def header = {
magic <- repeat_len8 3 u8, // TODO: where magic == ascii "GIF"`,
version <- repeat_len8 3 u8,
magic <- repeat_len64 3 u8, // TODO: where magic == ascii "GIF"`,
version <- repeat_len64 3 u8,
};

/// # Global Color Table Entry
Expand All @@ -50,7 +50,7 @@ def color_table_entry = {
///
/// - [GIF89a Specification: Section 19](https://www.w3.org/Graphics/GIF/spec-gif89a.txt)
def global_color_table (len : U16) = {
entries <- repeat_len16 len color_table_entry,
entries <- repeat_len64 len color_table_entry,
};

def main = {
Expand Down
6 changes: 3 additions & 3 deletions formats/gif.snap
Original file line number Diff line number Diff line change
Expand Up @@ -7,12 +7,12 @@ def logical_screen_descriptor : Format = {
pixel_aspect_ratio <- u8,
};
def header : Format = {
magic <- repeat_len8 3 u8,
version <- repeat_len8 3 u8,
magic <- repeat_len64 3 u8,
version <- repeat_len64 3 u8,
};
def color_table_entry : Format = { red <- u8, green <- u8, blue <- u8 };
def global_color_table : U16 -> Format = fun len => {
entries <- repeat_len16 len color_table_entry,
entries <- repeat_len64 (u16_extend_u64 len) color_table_entry,
};
def main : Format = { header <- header, screen <- logical_screen_descriptor };
'''
Expand Down
2 changes: 1 addition & 1 deletion formats/ideas/ico.fathom
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ def image = {

def main = {
// NOTE: Could be useful to have invertible patterns here?
magic <- repeat_len8 4 u8 match {
magic <- repeat_len64 4 u8 match {
[0, 0, 1, 0] => icon, // TODO
[0, 0, 2, 0] => cursor, // TODO
},
Expand Down
2 changes: 1 addition & 1 deletion formats/image.fathom
Original file line number Diff line number Diff line change
Expand Up @@ -15,5 +15,5 @@ def main = {
/// The height of the image, in pixels.
height <- u32be,
/// The pixel data.
pixels <- repeat_len32 (width * height) pixel,
pixels <- repeat_len64 (width * height) pixel,
};
Loading

0 comments on commit 45d6d7b

Please sign in to comment.