From 45d6d7bf4e88bb7aef94fe2d8a47f5fe726e4fe5 Mon Sep 17 00:00:00 2001 From: Karl Meakin Date: Mon, 13 Feb 2023 05:59:39 +0000 Subject: [PATCH] Remove `Array8`, `Array16` and `Array32` types --- fathom/src/core.rs | 20 +- fathom/src/core/binary.rs | 3 - fathom/src/core/prim.rs | 36 +-- fathom/src/surface/elaboration.rs | 94 ++++---- formats/edid.fathom | 2 +- formats/edid.snap | 2 +- formats/gif.fathom | 6 +- formats/gif.snap | 6 +- formats/ideas/ico.fathom | 2 +- formats/image.fathom | 2 +- formats/image.snap | 2 +- formats/object-id.fathom | 4 +- formats/object-id.snap | 4 +- formats/opentype.fathom | 210 ++++++++--------- formats/opentype.snap | 216 +++++++++--------- formats/stl-binary.fathom | 6 +- formats/stl-binary.snap | 6 +- formats/unwrap-none.fathom | 4 +- formats/unwrap-none.snap | 4 +- tests/cmd/fathom-elab.md | 4 +- .../mismatched-array-length/array16.fathom | 3 - .../mismatched-array-length/array16.snap | 12 - .../mismatched-array-length/array32.fathom | 3 - .../mismatched-array-length/array32.snap | 12 - .../mismatched-array-length/array8.fathom | 3 - .../mismatched-array-length/array8.snap | 12 - .../numeric-literal/mismatched-length.fathom | 2 +- .../numeric-literal/mismatched-length.snap | 2 +- .../succeed/ann/array-literal-array16.fathom | 1 - tests/succeed/ann/array-literal-array16.snap | 4 - .../succeed/ann/array-literal-array32.fathom | 1 - tests/succeed/ann/array-literal-array32.snap | 4 - tests/succeed/ann/array-literal-array8.fathom | 1 - tests/succeed/ann/array-literal-array8.snap | 4 - tests/succeed/binops/synth.fathom | 2 +- tests/succeed/binops/synth.snap | 2 +- tests/succeed/format-deref/simple.fathom | 2 +- tests/succeed/format-deref/simple.snap | 2 +- tests/succeed/format-overlap/dependent.fathom | 4 +- tests/succeed/format-overlap/dependent.snap | 7 +- .../format-record/computed-fields.fathom | 8 +- .../format-record/computed-fields.snap | 8 +- .../format-record/field-refinements.fathom | 4 +- .../format-record/field-refinements.snap | 9 +- tests/succeed/format-repr/primitives.fathom | 6 - tests/succeed/format-repr/primitives.snap | 12 - tests/succeed/primitive-ops.fathom | 7 - tests/succeed/primitive-ops.snap | 6 - tests/succeed/primitives.fathom | 21 +- tests/succeed/primitives.snap | 26 +-- 50 files changed, 358 insertions(+), 465 deletions(-) delete mode 100644 tests/fail/elaboration/mismatched-array-length/array16.fathom delete mode 100644 tests/fail/elaboration/mismatched-array-length/array16.snap delete mode 100644 tests/fail/elaboration/mismatched-array-length/array32.fathom delete mode 100644 tests/fail/elaboration/mismatched-array-length/array32.snap delete mode 100644 tests/fail/elaboration/mismatched-array-length/array8.fathom delete mode 100644 tests/fail/elaboration/mismatched-array-length/array8.snap delete mode 100644 tests/succeed/ann/array-literal-array16.fathom delete mode 100644 tests/succeed/ann/array-literal-array16.snap delete mode 100644 tests/succeed/ann/array-literal-array32.fathom delete mode 100644 tests/succeed/ann/array-literal-array32.snap delete mode 100644 tests/succeed/ann/array-literal-array8.fathom delete mode 100644 tests/succeed/ann/array-literal-array8.snap diff --git a/fathom/src/core.rs b/fathom/src/core.rs index 64b3ddefc..d25451da3 100644 --- a/fathom/src/core.rs +++ b/fathom/src/core.rs @@ -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", @@ -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. @@ -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", @@ -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", @@ -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", diff --git a/fathom/src/core/binary.rs b/fathom/src/core/binary.rs index 661f014e6..4d9444e1d 100644 --- a/fathom/src/core/binary.rs +++ b/fathom/src/core/binary.rs @@ -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), diff --git a/fathom/src/core/prim.rs b/fathom/src/core/prim.rs index e4e99808f..23442069a 100644 --- a/fathom/src/core/prim.rs +++ b/fathom/src/core/prim.rs @@ -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); @@ -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); @@ -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); @@ -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); @@ -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); @@ -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); @@ -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 @@ -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); @@ -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)), @@ -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)), @@ -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)), @@ -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)), diff --git a/fathom/src/surface/elaboration.rs b/fathom/src/surface/elaboration.rs index cf4a19466..48108acf0 100644 --- a/fathom/src/surface/elaboration.rs +++ b/fathom/src/surface/elaboration.rs @@ -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) + } } } @@ -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, _ => { @@ -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) } @@ -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); @@ -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, _ => { diff --git a/formats/edid.fathom b/formats/edid.fathom index ea171de5f..27e02bfe5 100644 --- a/formats/edid.fathom +++ b/formats/edid.fathom @@ -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 = { diff --git a/formats/edid.snap b/formats/edid.snap index 16017796b..e6122b1c2 100644 --- a/formats/edid.snap +++ b/formats/edid.snap @@ -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, diff --git a/formats/gif.fathom b/formats/gif.fathom index 719ba18c2..7494f749b 100644 --- a/formats/gif.fathom +++ b/formats/gif.fathom @@ -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 @@ -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 = { diff --git a/formats/gif.snap b/formats/gif.snap index 422a9e181..c4a34f759 100644 --- a/formats/gif.snap +++ b/formats/gif.snap @@ -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 }; ''' diff --git a/formats/ideas/ico.fathom b/formats/ideas/ico.fathom index 0c76aa8ea..3bf2b38b3 100644 --- a/formats/ideas/ico.fathom +++ b/formats/ideas/ico.fathom @@ -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 }, diff --git a/formats/image.fathom b/formats/image.fathom index 1f8f5606a..1a297b38f 100644 --- a/formats/image.fathom +++ b/formats/image.fathom @@ -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, }; diff --git a/formats/image.snap b/formats/image.snap index a7dea0e8a..a75ba59be 100644 --- a/formats/image.snap +++ b/formats/image.snap @@ -3,7 +3,7 @@ def pixel : Format = { red <- s32be, green <- s32be, blue <- s32be }; def main : Format = { width <- u32be, height <- u32be, - pixels <- repeat_len32 (width * height) pixel, + pixels <- repeat_len64 (u32_extend_u64 width * u32_extend_u64 height) pixel, }; ''' stderr = '' diff --git a/formats/object-id.fathom b/formats/object-id.fathom index 513b3dee2..6fd8d4054 100644 --- a/formats/object-id.fathom +++ b/formats/object-id.fathom @@ -5,7 +5,7 @@ //! - [Mongo Reference](https://docs.mongodb.com/manual/reference/bson-types/#objectid) // TODO: make this a primitive -def u24be = repeat_len8 3 u8; +def u24be = repeat_len64 3 u8; def main = { /// 4-byte timestamp value representing the creation time of the ObjectId, @@ -13,7 +13,7 @@ def main = { timestamp <- u32be, /// Random value generated once per process. This random value is unique to /// the machine and process. - random <- repeat_len8 5 u8, + random <- repeat_len64 5 u8, /// Incrementing counter, initialized to a random value. counter <- u24be, }; diff --git a/formats/object-id.snap b/formats/object-id.snap index bedf14a46..f8e715d2c 100644 --- a/formats/object-id.snap +++ b/formats/object-id.snap @@ -1,8 +1,8 @@ stdout = ''' -def u24be : Format = repeat_len8 3 u8; +def u24be : Format = repeat_len64 3 u8; def main : Format = { timestamp <- u32be, - random <- repeat_len8 5 u8, + random <- repeat_len64 5 u8, counter <- u24be, }; ''' diff --git a/formats/opentype.fathom b/formats/opentype.fathom index 7eda8a62f..698a4e5ca 100644 --- a/formats/opentype.fathom +++ b/formats/opentype.fathom @@ -75,7 +75,7 @@ def table_directory (file_start : Pos) = { /// An array of table records // FIXME: sorted in ascending order by tag - table_records <- repeat_len16 num_tables table_record, + table_records <- repeat_len64 num_tables table_record, /// Font table links /// @@ -230,7 +230,7 @@ def ttc_header (start : Pos) = ( /// Number of fonts in TTC num_fonts <- u32be, /// Array of offsets to the TableDirectory for each font from the beginning of the file - table_directories <- repeat_len32 num_fonts (offset32 start (table_directory start)), + table_directories <- repeat_len64 num_fonts (offset32 start (table_directory start)), }; /// TTC Header Version 2.0 @@ -238,7 +238,7 @@ def ttc_header (start : Pos) = ( /// Number of fonts in TTC num_fonts <- u32be, /// Array of offsets to the TableDirectory for each font from the beginning of the file - table_directories <- repeat_len32 num_fonts (offset32 start (table_directory start)), + table_directories <- repeat_len64 num_fonts (offset32 start (table_directory start)), /// Tag indicating that a DSIG table exists, 0x44534947 ('DSIG') (null if no signature) dsig_tag <- u32be, /// The length (in bytes) of the DSIG table (null if no signature) @@ -292,13 +292,13 @@ def table_record = { /// Find a table record using the given `table_id`. def find_table = fun (@num_tables : U16) => - fun (table_records : Array16 num_tables (Repr table_record)) => + fun (table_records : Array64 num_tables (Repr table_record)) => fun (table_id : Repr tag) => // TODO: accelerate using binary search // TODO: make use of `table_record.search_range` // TODO: make use of `table_record.entry_selector` // TODO: make use of `table_record.range_shift` - array16_find + array64_find (fun (table_record : Repr table_record) => table_record.table_id == table_id) table_records; @@ -368,7 +368,7 @@ def f2dot14 : Format = s16be; /// ## References /// /// - [Microsoft's OpenType Spec: uint24](https://docs.microsoft.com/en-us/typography/opentype/spec/otff#dt_uint24) -def u24be : Format = repeat_len8 3 u8; +def u24be : Format = repeat_len64 3 u8; /// Date represented in number of seconds since 12:00 midnight, January 1, 1904. /// @@ -389,7 +389,7 @@ def long_date_time : Format = s64be; def tag : Format = // TODO: constrain array elements to the range 0x20 to 0x7E. // TODO: pattern matching on arrays - // repeat_len8 4 u8; + // repeat_len64 4 u8; u32be; /// # Unknown table format @@ -515,7 +515,7 @@ def class_def_format_1 = { /// Size of the class_value_array glyph_count <- u16be, /// Array of Class Values — one per glyph ID - class_value_array <- repeat_len16 glyph_count u16be, + class_value_array <- repeat_len64 glyph_count u16be, }; /// # Class Definition Table Format 2 @@ -538,7 +538,7 @@ def class_def_format_2 = ( /// Number of ClassRangeRecords class_range_count <- u16be, /// Array of ClassRangeRecords — ordered by startGlyphID - class_range_records <- repeat_len16 class_range_count class_range_record, + class_range_records <- repeat_len64 class_range_count class_range_record, } ); @@ -567,7 +567,7 @@ def coverage_format_1 = { /// Number of glyphs in the glyph array glyph_count <- u16be, /// Array of glyph IDs — in numerical order - glyph_array <- repeat_len16 glyph_count u16be, + glyph_array <- repeat_len64 glyph_count u16be, }; /// # Coverage Format 2 @@ -590,7 +590,7 @@ def coverage_format_2 = ( /// Number of RangeRecords range_count <- u16be, /// Array of glyph ranges — ordered by startGlyphID - range_records <- repeat_len16 range_count range_record, + range_records <- repeat_len64 range_count range_record, } ); @@ -687,7 +687,7 @@ def device_table = ( /// Array of compressed data delta_values <- let delta_bits = delta_bits delta_format (num_sizes start_size end_size); - repeat_len16 (u16_div_ceil delta_bits 16) u16be, + repeat_len64 (u16_div_ceil delta_bits 16) u16be, } ); @@ -704,7 +704,7 @@ def variation_index_table = { def device_or_variation_index_table = overlap { // Initial pass to figure out the table format init <- { - _skipped <- repeat_len8 4 u8, + _skipped <- repeat_len64 4 u8, table_format <- u16be, }, // Device and VariationIndex Tables @@ -732,7 +732,7 @@ def lang_sys = { /// Number of feature index values for this language system — excludes the required feature feature_index_count <- u16be, /// Array of indices into the FeatureList, in arbitrary order - feature_indices <- repeat_len16 feature_index_count u16be, + feature_indices <- repeat_len64 feature_index_count u16be, }; /// # Language System Record @@ -762,7 +762,7 @@ def script_table = { /// Number of LangSysRecords for this script — excluding the default LangSys lang_sys_count <- u16be, /// Array of LangSysRecords, listed alphabetically by LangSys tag - lang_sys_records <- repeat_len16 lang_sys_count (lang_sys_record table_start), + lang_sys_records <- repeat_len64 lang_sys_count (lang_sys_record table_start), }; /// # Script list table @@ -785,7 +785,7 @@ def script_list = ( /// Number of ScriptRecords script_count <- u16be, /// Array of ScriptRecords, listed alphabetically by script tag - script_records <- repeat_len16 script_count (script_record table_start), + script_records <- repeat_len64 script_count (script_record table_start), } ); @@ -803,7 +803,7 @@ def feature_table = { /// Number of LookupList indices for this feature lookup_index_count <- u16be, /// Array of indices into the LookupList — zero-based (first lookup is LookupListIndex = 0) - lookup_list_indices <- repeat_len16 lookup_index_count u16be, + lookup_list_indices <- repeat_len64 lookup_index_count u16be, }; /// # Feature List Table @@ -826,7 +826,7 @@ def feature_list = ( feature_count <- u16be, /// Array of FeatureRecords — zero-based (first feature has FeatureIndex = 0), listed /// alphabetically by feature tag - feature_records <- repeat_len16 feature_count (feature_record table_start), + feature_records <- repeat_len64 feature_count (feature_record table_start), } ); @@ -843,9 +843,9 @@ def sequence_context_format1 = ( /// Number of SequenceLookupRecords seq_lookup_count <- u16be, /// Array of input glyph IDs—starting with the second glyph - input_sequence <- repeat_len16 (u16_sub glyph_count 1) u16be, + input_sequence <- repeat_len64 (u16_sub glyph_count 1) u16be, /// Array of Sequence lookup records - seq_lookup_records <- repeat_len16 seq_lookup_count sequence_lookup_record, + seq_lookup_records <- repeat_len64 seq_lookup_count sequence_lookup_record, }; /// SequenceRuleSet table—all contexts beginning with the same glyph @@ -855,7 +855,7 @@ def sequence_context_format1 = ( /// Number of SequenceRule tables seq_rule_count <- u16be, /// Array of offsets to SequenceRule tables, from beginning of the SequenceRuleSet table - seq_rules <- repeat_len16 seq_rule_count (offset16 table_start sequence_rule), + seq_rules <- repeat_len64 seq_rule_count (offset16 table_start sequence_rule), }; { @@ -867,7 +867,7 @@ def sequence_context_format1 = ( seq_rule_set_count <- u16be, /// Array of offsets to SequenceRuleSet tables, from beginning of /// SequenceContextFormat1 table (offsets may be NULL) - seq_rule_sets <- repeat_len16 seq_rule_set_count (offset16 table_start sequence_rule_set), + seq_rule_sets <- repeat_len64 seq_rule_set_count (offset16 table_start sequence_rule_set), } ); @@ -885,9 +885,9 @@ def sequence_context_format2 = ( seq_lookup_count <- u16be, /// Sequence of classes to be matched to the input glyph sequence, beginning with the /// second glyph position - input_sequence <- repeat_len16 (u16_sub glyph_count 1) u16be, + input_sequence <- repeat_len64 (u16_sub glyph_count 1) u16be, /// Array of SequenceLookupRecords - seqLookupRecords <- repeat_len16 seq_lookup_count sequence_lookup_record, + seqLookupRecords <- repeat_len64 seq_lookup_count sequence_lookup_record, }; /// ClassSequenceRuleSet table @@ -898,7 +898,7 @@ def sequence_context_format2 = ( class_seq_rule_count <- u16be, /// Array of offsets to ClassSequenceRule tables, from beginning of ClassSequenceRuleSet /// table - class_seq_rules <- repeat_len16 class_seq_rule_count (offset16 table_start class_sequence_rule), + class_seq_rules <- repeat_len64 class_seq_rule_count (offset16 table_start class_sequence_rule), }; { @@ -912,7 +912,7 @@ def sequence_context_format2 = ( class_seq_rule_set_count <- u16be, /// Array of offsets to ClassSequenceRuleSet tables, from beginning of /// SequenceContextFormat2 table (may be NULL) - class_seq_rule_sets <- repeat_len16 class_seq_rule_set_count (offset16 table_start class_sequence_rule_set), + class_seq_rule_sets <- repeat_len64 class_seq_rule_set_count (offset16 table_start class_sequence_rule_set), } ); @@ -929,9 +929,9 @@ def sequence_context_format3 = { /// Number of SequenceLookupRecords seq_lookup_count <- u16be, /// Array of offsets to Coverage tables, from beginning of SequenceContextFormat3 subtable - coverage_tables <- repeat_len16 glyph_count (offset16 table_start coverage_table), + coverage_tables <- repeat_len64 glyph_count (offset16 table_start coverage_table), /// Array of SequenceLookupRecords - seq_lookup_records <- repeat_len16 seq_lookup_count sequence_lookup_record, + seq_lookup_records <- repeat_len64 seq_lookup_count sequence_lookup_record, }; def sequence_context = { @@ -956,19 +956,19 @@ def chained_sequence_context_format_1 = ( /// Number of glyphs in the backtrack sequence backtrack_glyph_count <- u16be, /// Array of backtrack glyph IDs - backtrack_sequence <- repeat_len16 backtrack_glyph_count u16be, + backtrack_sequence <- repeat_len64 backtrack_glyph_count u16be, /// Number of glyphs in the input sequence input_glyph_count <- u16be, /// Array of input glyph IDs—start with second glyph - input_sequence <- repeat_len16 (u16_sub input_glyph_count 1) u16be, + input_sequence <- repeat_len64 (u16_sub input_glyph_count 1) u16be, /// Number of glyphs in the lookahead sequence lookahead_glyph_count <- u16be, /// Array of lookahead glyph IDs - lookahead_sequence <- repeat_len16 lookahead_glyph_count u16be, + lookahead_sequence <- repeat_len64 lookahead_glyph_count u16be, /// Number of SequenceLookupRecords seq_lookup_count <- u16be, /// Array of SequenceLookupRecords - seq_lookup_records <- repeat_len16 seq_lookup_count sequence_lookup_record, + seq_lookup_records <- repeat_len64 seq_lookup_count sequence_lookup_record, }; let chained_sequence_rule_set = { @@ -978,7 +978,7 @@ def chained_sequence_context_format_1 = ( chained_seq_rule_count <- u16be, /// Array of offsets to ChainedSequenceRule tables, from beginning of /// ChainedSequenceRuleSet table - chained_seq_rules <- repeat_len16 chained_seq_rule_count (offset16 table_start chained_sequence_rule), + chained_seq_rules <- repeat_len64 chained_seq_rule_count (offset16 table_start chained_sequence_rule), }; { @@ -990,7 +990,7 @@ def chained_sequence_context_format_1 = ( chained_seq_rule_set_count <- u16be, /// Array of offsets to ChainedSeqRuleSet tables, from beginning of /// ChainedSequenceContextFormat1 table (may be NULL) - chained_seq_rule_sets <- repeat_len16 chained_seq_rule_set_count (offset16 table_start chained_sequence_rule_set), + chained_seq_rule_sets <- repeat_len64 chained_seq_rule_set_count (offset16 table_start chained_sequence_rule_set), } ); @@ -1005,19 +1005,19 @@ def chained_sequence_context_format_2 = ( /// Number of glyphs in the backtrack sequence backtrack_glyph_count <- u16be, /// Array of backtrack-sequence classes - backtrack_sequence <- repeat_len16 backtrack_glyph_count u16be, + backtrack_sequence <- repeat_len64 backtrack_glyph_count u16be, /// Total number of glyphs in the input sequence input_glyph_count <- u16be, /// Array of input sequence classes, beginning with the second glyph position - input_sequence <- repeat_len16 (u16_sub input_glyph_count 1) u16be, + input_sequence <- repeat_len64 (u16_sub input_glyph_count 1) u16be, /// Number of glyphs in the lookahead sequence lookahead_glyph_count <- u16be, /// Array of lookahead-sequence classes - lookahead_sequence <- repeat_len16 lookahead_glyph_count u16be, + lookahead_sequence <- repeat_len64 lookahead_glyph_count u16be, /// Number of SequenceLookupRecords seq_lookup_count <- u16be, /// Array of SequenceLookupRecords - seq_lookup_records <- repeat_len16 seq_lookup_count sequence_lookup_record, + seq_lookup_records <- repeat_len64 seq_lookup_count sequence_lookup_record, }; /// ChainedClassSequenceRuleSet table @@ -1028,7 +1028,7 @@ def chained_sequence_context_format_2 = ( chained_class_seq_rule_count <- u16be, /// Array of offsets to ChainedClassSequenceRule tables, from beginning of /// ChainedClassSequenceRuleSet - chained_class_seq_rules <- repeat_len16 chained_class_seq_rule_count (offset16 table_start chained_class_sequence_rule), + chained_class_seq_rules <- repeat_len64 chained_class_seq_rule_count (offset16 table_start chained_class_sequence_rule), }; { @@ -1049,7 +1049,7 @@ def chained_sequence_context_format_2 = ( chained_class_seq_rule_set_count <- u16be, /// Array of offsets to ChainedClassSequenceRuleSet tables, from beginning of /// ChainedSequenceContextFormat2 table (may be NULL) - chained_class_seq_rule_sets <- repeat_len16 chained_class_seq_rule_set_count (offset16 table_start chained_class_sequence_rule_set), + chained_class_seq_rule_sets <- repeat_len64 chained_class_seq_rule_set_count (offset16 table_start chained_class_sequence_rule_set), } ); @@ -1064,19 +1064,19 @@ def chained_sequence_context_format_3 = { /// Number of glyphs in the backtrack sequence backtrack_glyph_count <- u16be, /// Array of offsets to coverage tables for the backtrack sequence - backtrack_coverages <- repeat_len16 backtrack_glyph_count (offset16 table_start coverage_table), + backtrack_coverages <- repeat_len64 backtrack_glyph_count (offset16 table_start coverage_table), /// Number of glyphs in the input sequence input_glyph_count <- u16be, /// Array of offsets to coverage tables for the input sequence - input_coverage_tables <- repeat_len16 input_glyph_count (offset16 table_start coverage_table), + input_coverage_tables <- repeat_len64 input_glyph_count (offset16 table_start coverage_table), /// Number of glyphs in the lookahead sequence lookahead_glyph_count <- u16be, /// Array of offsets to coverage tables for the lookahead sequence - lookahead_coverages <- repeat_len16 lookahead_glyph_count (offset16 table_start coverage_table), + lookahead_coverages <- repeat_len64 lookahead_glyph_count (offset16 table_start coverage_table), /// Number of SequenceLookupRecords seq_lookup_count <- u16be, /// Array of SequenceLookupRecords - seq_lookup_records <- repeat_len16 seq_lookup_count sequence_lookup_record, + seq_lookup_records <- repeat_len64 seq_lookup_count sequence_lookup_record, }; def chained_sequence_context = { @@ -1117,7 +1117,7 @@ def single_substitution = { /// Number of glyph IDs in the substitute_glyph_ids array glyph_count <- u16be, /// Array of substitute glyph IDs — ordered by Coverage index - substitute_glyph_ids <- repeat_len16 glyph_count u16be, + substitute_glyph_ids <- repeat_len64 glyph_count u16be, }, _ => unknown_table }, @@ -1134,7 +1134,7 @@ def multiple_substitution = ( /// 0. glyph_count <- u16be, /// String of glyph IDs to substitute - substitute_glyph_ids <- repeat_len16 glyph_count u16be, + substitute_glyph_ids <- repeat_len64 glyph_count u16be, }; { @@ -1150,7 +1150,7 @@ def multiple_substitution = ( sequence_count <- u16be, /// Array of offsets to Sequence tables. Offsets are from beginning of substitution /// subtable, ordered by Coverage index - sequences <- repeat_len16 sequence_count (offset16 table_start sequence_table), + sequences <- repeat_len64 sequence_count (offset16 table_start sequence_table), }, _ => unknown_table, }, @@ -1168,7 +1168,7 @@ def alternate_substitution = ( /// Number of glyph IDs in the alternate_glyph_ids array glyph_count <- u16be, /// Array of alternate glyph IDs, in arbitrary order - alternate_glyph_ids <- repeat_len16 glyph_count u16be, + alternate_glyph_ids <- repeat_len64 glyph_count u16be, }; { @@ -1184,7 +1184,7 @@ def alternate_substitution = ( alternate_set_count <- u16be, /// Array of offsets to AlternateSet tables. Offsets are from beginning of /// substitution subtable, ordered by Coverage index - alternate_sets <- repeat_len16 alternate_set_count (offset16 table_start alternate_set), + alternate_sets <- repeat_len64 alternate_set_count (offset16 table_start alternate_set), }, _ => unknown_table, }, @@ -1205,7 +1205,7 @@ def ligature_substitution = ( component_count <- u16be, /// Array of component glyph IDs — start with the second component, ordered in writing /// direction - component_glyph_ids <- repeat_len16 (u16_sub component_count 1) u16be, + component_glyph_ids <- repeat_len64 (u16_sub component_count 1) u16be, }; /// LigatureSet table: All ligatures beginning with the same glyph @@ -1223,7 +1223,7 @@ def ligature_substitution = ( /// the components (componentGlyphIDs). The array starts with the second component glyph in /// the ligature (glyph sequence index = 1, componentGlyphIDs array index = 0) because the /// first component glyph is specified in the Coverage table. - ligatures <- repeat_len16 ligature_count (offset16 table_start ligature_table), + ligatures <- repeat_len64 ligature_count (offset16 table_start ligature_table), }; { @@ -1239,7 +1239,7 @@ def ligature_substitution = ( ligature_set_count <- u16be, /// Array of offsets to LigatureSet tables. Offsets are from beginning of /// substitution subtable, ordered by Coverage index - ligature_sets <- repeat_len16 ligature_set_count (offset16 table_start ligature_set), + ligature_sets <- repeat_len64 ligature_set_count (offset16 table_start ligature_set), }, _ => unknown_table, }, @@ -1275,15 +1275,15 @@ def reverse_chaining_contextual_single_substitution = ( /// Number of glyphs in the backtrack sequence. backtrack_glyph_count <- u16be, /// Array of offsets to coverage tables in backtrack sequence, in glyph sequence order. - backtrack_coverage_tables <- repeat_len16 backtrack_glyph_count (offset16 table_start coverage_table), + backtrack_coverage_tables <- repeat_len64 backtrack_glyph_count (offset16 table_start coverage_table), /// Number of glyphs in lookahead sequence. lookahead_glyph_count <- u16be, /// Array of offsets to coverage tables in lookahead sequence, in glyph sequence order. - lookahead_coverage_tables <- repeat_len16 lookahead_glyph_count (offset16 table_start coverage_table), + lookahead_coverage_tables <- repeat_len64 lookahead_glyph_count (offset16 table_start coverage_table), /// Number of glyph IDs in the substituteGlyphIDs array. glyph_count <- u16be, /// Array of substitute glyph IDs — ordered by Coverage index. - substitute_glyph_ids <- repeat_len16 glyph_count u16be, + substitute_glyph_ids <- repeat_len64 glyph_count u16be, }; { @@ -1505,7 +1505,7 @@ def mark_array_table = ( /// Number of MarkRecords mark_count <- u16be, /// Array of MarkRecords, ordered by corresponding glyphs in the associated mark Coverage table. - mark_records <- repeat_len16 mark_count (mark_record table_start), + mark_records <- repeat_len64 mark_count (mark_record table_start), } ); @@ -1536,7 +1536,7 @@ def single_adjustment = ( /// Number of ValueRecords — must equal glyphCount in the Coverage table. value_count <- u16be, /// Array of ValueRecords — positioning values applied to glyphs. - value_records <- repeat_len16 value_count (value_record table_start value_format), + value_records <- repeat_len64 value_count (value_record table_start value_format), }; { @@ -1578,7 +1578,7 @@ def pair_adjustment = ( /// Number of PairValueRecords pair_value_count <- u16be, /// Array of PairValueRecords, ordered by glyph ID of the second glyph. - pair_value_records <- repeat_len16 pair_value_count (pair_value_record table_start value_format1 value_format2), + pair_value_records <- repeat_len64 pair_value_count (pair_value_record table_start value_format1 value_format2), }; /// Pair Adjustment Positioning Format 1: Adjustments for Glyph Pairs (PairPosFormat1) @@ -1595,7 +1595,7 @@ def pair_adjustment = ( pair_set_count <- u16be, /// Array of offsets to PairSet tables. Offsets are from beginning of PairPos subtable, /// ordered by Coverage Index. - pair_sets <- repeat_len16 pair_set_count (offset16 table_start (pair_set value_format1 value_format2)), + pair_sets <- repeat_len64 pair_set_count (offset16 table_start (pair_set value_format1 value_format2)), }; /// Class2Record @@ -1609,7 +1609,7 @@ def pair_adjustment = ( /// Class1Record let class1_record = fun (table_start : Pos) (class2_count : U16) (value_format1 : U16) (value_format2 : U16) => { /// Array of Class2 records, ordered by classes in classDef2. - class2_records <- repeat_len16 class2_count (class2_record table_start value_format1 value_format2), + class2_records <- repeat_len64 class2_count (class2_record table_start value_format1 value_format2), }; /// Pair Adjustment Positioning Format 2: Class Pair Adjustment (PairPosFormat2) @@ -1631,7 +1631,7 @@ def pair_adjustment = ( /// Number of classes in classDef2 table — includes Class 0. class2_count <- u16be, /// Array of Class1 records, ordered by classes in classDef1. - class1_records <- repeat_len16 class1_count (class1_record pair_pos_start class2_count value_format1 value_format2), + class1_records <- repeat_len64 class1_count (class1_record pair_pos_start class2_count value_format1 value_format2), }; { @@ -1672,7 +1672,7 @@ def cursive_attachment = ( /// Number of EntryExit records entry_exit_count <- u16be, /// Array of EntryExit records, in Coverage index order. - entry_exit_record <- repeat_len16 entry_exit_count (entry_exit_record table_start), + entry_exit_record <- repeat_len64 entry_exit_count (entry_exit_record table_start), }; { @@ -1700,7 +1700,7 @@ def mark_to_base_attachment = ( let base_record = fun (table_start : Pos) (mark_class_count : U16) => { /// Array of offsets (one per mark class) to Anchor tables. Offsets are from beginning of /// BaseArray table, ordered by class (offsets may be NULL). - base_anchors <- repeat_len16 mark_class_count (offset16 table_start anchor_table), + base_anchors <- repeat_len64 mark_class_count (offset16 table_start anchor_table), }; /// BaseArray Table @@ -1708,7 +1708,7 @@ def mark_to_base_attachment = ( /// Number of BaseRecords base_count <- u16be, /// Array of BaseRecords, in order of baseCoverage Index. - base_records <- repeat_len16 base_count (base_record table_start mark_class_count), + base_records <- repeat_len64 base_count (base_record table_start mark_class_count), }; /// MarkBasePosFormat1 Subtable @@ -1749,7 +1749,7 @@ def mark_to_ligature_attachment = ( let component_record = fun (table_start : Pos) (mark_class_count : U16) => { /// Array of offsets (one per class) to Anchor tables. Offsets are from beginning of /// LigatureAttach table, ordered by class (offsets may be NULL). - ligature_anchors <- repeat_len16 mark_class_count (offset16 table_start anchor_table), + ligature_anchors <- repeat_len64 mark_class_count (offset16 table_start anchor_table), }; /// LigatureAttach Table @@ -1757,7 +1757,7 @@ def mark_to_ligature_attachment = ( /// Number of ComponentRecords in this ligature component_count <- u16be, /// Array of Component records, ordered in writing direction. - component_records <- repeat_len16 component_count (component_record table_start mark_class_count), + component_records <- repeat_len64 component_count (component_record table_start mark_class_count), }; /// LigatureArray Table @@ -1766,7 +1766,7 @@ def mark_to_ligature_attachment = ( ligature_count <- u16be, /// Array of offsets to LigatureAttach tables. Offsets are from beginning of LigatureArray /// table, ordered by ligatureCoverage index. - ligature_attaches <- repeat_len16 ligature_count (offset16 table_start (ligature_attach table_start mark_class_count)), + ligature_attaches <- repeat_len64 ligature_count (offset16 table_start (ligature_attach table_start mark_class_count)), }; /// MarkLigPosFormat1 Subtable @@ -1910,7 +1910,7 @@ def lookup_table (tag : U32) = ( /// Number of subtables for this lookup sub_table_count <- u16be, /// Array of offsets to lookup subtables, from beginning of Lookup table - subtables <- repeat_len16 sub_table_count (offset16 table_start (lookup_subtable tag lookup_type)), + subtables <- repeat_len64 sub_table_count (offset16 table_start (lookup_subtable tag lookup_type)), /// Index (base 0) into GDEF mark glyph sets structure. This field is only present if the /// USE_MARK_FILTERING_SET lookup flag is set. mark_filtering_set <- match (u16_and lookup_flag USE_MARK_FILTERING_SET != (0 : U16)) { @@ -1931,7 +1931,7 @@ def lookup_list (tag : U32) = { /// Number of lookups in this table lookup_count <- u16be, /// Array of offsets to Lookup tables, from beginning of LookupList - lookups <- repeat_len16 lookup_count (offset16 table_start (lookup_table tag)), + lookups <- repeat_len64 lookup_count (offset16 table_start (lookup_table tag)), }; // ----------------------------------------------------------------------------- @@ -2031,7 +2031,7 @@ def default_uvs_table = { /// Number of Unicode character ranges. num_unicode_value_ranges <- u32be, /// Array of UnicodeRange records. - ranges <- repeat_len32 num_unicode_value_ranges unicode_range, + ranges <- repeat_len64 num_unicode_value_ranges unicode_range, }; /// # UVSMapping Record @@ -2062,7 +2062,7 @@ def non_default_uvs_table = { /// Number of UVS Mappings that follow num_uvs_mappings <- u32be, /// Array of UVSMapping records. - uvs_mappings <- repeat_len32 num_uvs_mappings uvs_mapping, + uvs_mappings <- repeat_len64 num_uvs_mappings uvs_mapping, }; /// # VariationSelector Record for cmap sub-table format 14 @@ -2104,7 +2104,7 @@ def cmap_subtable_format0 (platform : platform_id) = { /// A 1 to 1 mapping that converts character codes to glyph indexes (limited /// to 256 glyphs). Only the first 256 glyphs will be accessible for larger /// glyph sets. - glyph_id_array <- repeat_len16 256 small_glyph_id, + glyph_id_array <- repeat_len64 256 small_glyph_id, }; /// # Format 2: High-byte mapping through table @@ -2123,7 +2123,7 @@ def cmap_subtable_format2 (platform : platform_id) = { /// The language ID of the subtable language <- cmap_language_id platform, /// Array that maps high bytes to subHeaders: value is subHeader index × 8. - sub_header_keys <- repeat_len16 256 u16be, + sub_header_keys <- repeat_len64 256 u16be, // TODO: These probably need length limiting formats // https://github.com/yeslogic/fathom/pull/310 // /// Variable-length array of SubHeader records. @@ -2159,15 +2159,15 @@ def cmap_subtable_format4 (platform : platform_id) = { /// segCount times 2, minus searchRange ((segCount * 2) - searchRange) range_shift <- u16be, /// End characterCode for each segment, last=0xFFFF. - end_code <- repeat_len16 seg_count u16be, + end_code <- repeat_len64 seg_count u16be, /// Set to 0. _reserved_pad <- reserved s16be 0, /// Start character code for each segment. - start_code <- repeat_len16 seg_count u16be, + start_code <- repeat_len64 seg_count u16be, /// Delta for all character codes in segment. - id_delta <- repeat_len16 seg_count s16be, + id_delta <- repeat_len64 seg_count s16be, /// Offsets into glyphIdArray or 0 - id_range_offsets <- repeat_len16 seg_count u16be, + id_range_offsets <- repeat_len64 seg_count u16be, // TODO: Needs length limiting formats // /// Glyph index array (arbitrary length) // glyph_id_array[ ] <- u16be, @@ -2192,7 +2192,7 @@ def cmap_subtable_format6 (platform : platform_id) = { /// Number of character codes in subrange. entry_count <- u16be, /// Array of glyph index values for character codes in the range. - glyph_id_array <- repeat_len16 entry_count u16be, + glyph_id_array <- repeat_len64 entry_count u16be, }; /// # Format 8: mixed 16-bit and 32-bit coverage @@ -2215,11 +2215,11 @@ def cmap_subtable_format8 (platform : platform_id) = { language <- cmap_language_id32 platform, /// Tightly packed array of bits (8K bytes total) indicating whether the particular 16-bit /// (index) value is the start of a 32-bit character code - is32 <- repeat_len16 8192 u8, + is32 <- repeat_len64 8192 u8, /// Number of groupings which follow num_groups <- u32be, /// Array of SequentialMapGroup records. - groups <- repeat_len32 num_groups sequential_map_group, + groups <- repeat_len64 num_groups sequential_map_group, }; /// # Format 10: Trimmed table mapping @@ -2244,7 +2244,7 @@ def cmap_subtable_format10 (platform : platform_id) = { /// Number of character codes covered num_chars <- u32be, /// Array of glyph indices for the character codes covered - glyph_id_array <- repeat_len32 num_chars u16be, + glyph_id_array <- repeat_len64 num_chars u16be, }; /// # Format 12: Segmented coverage @@ -2266,7 +2266,7 @@ def cmap_subtable_format12 (platform : platform_id) = { /// Number of groupings which follow num_groups <- u32be, /// Array of SequentialMapGroup records. - groups <- repeat_len32 num_groups sequential_map_group, + groups <- repeat_len64 num_groups sequential_map_group, }; /// # Format 13: Many-to-one range mappings @@ -2290,7 +2290,7 @@ def cmap_subtable_format13 (platform : platform_id) = { /// Number of groupings which follow num_groups <- u32be, /// Array of ConstantMapGroup records. - groups <- repeat_len32 num_groups constant_map_group, + groups <- repeat_len64 num_groups constant_map_group, }; /// # Format 14: Unicode Variation Sequences @@ -2311,7 +2311,7 @@ def cmap_subtable_format14 (platform : platform_id) (table_start : Pos) = { /// Number of variation Selector Records num_var_selector_records <- u32be, /// Array of VariationSelector records. - var_selector <- repeat_len32 num_var_selector_records (variation_selector table_start), + var_selector <- repeat_len64 num_var_selector_records (variation_selector table_start), }; /// # Character Mapping subtable @@ -2363,7 +2363,7 @@ def cmap_table = { /// The number of encoding tables that follow num_tables <- u16be, /// An array of encoding records in the character mapping table - encoding_records <- repeat_len16 num_tables (encoding_record table_start), + encoding_records <- repeat_len64 num_tables (encoding_record table_start), }; @@ -2555,10 +2555,10 @@ def long_horizontal_metric = { /// - [Apple's TrueType Reference Manual: The `'hmtx'` table](https://developer.apple.com/fonts/TrueType-Reference-Manual/RM06/Chap6hmtx.html) def htmx_table (number_of_long_horizontal_metrics : U16) (num_glyphs : U16) = { /// Long horizontal metrics, indexed by the glyph ID. - h_metrics <- repeat_len16 number_of_long_horizontal_metrics long_horizontal_metric, + h_metrics <- repeat_len64 number_of_long_horizontal_metrics long_horizontal_metric, /// Left side bearings for glyph IDs greater than or equal to the /// `number_of_long_horizontal_metrics`. - left_side_bearings <- repeat_len16 (u16_sub num_glyphs number_of_long_horizontal_metrics) s16be, + left_side_bearings <- repeat_len64 (u16_sub num_glyphs number_of_long_horizontal_metrics) s16be, }; @@ -2702,7 +2702,7 @@ def name_record (storage_start : Pos) = { /// String length length <- u16be, /// Offset to the string data, relative to the start of the storage area - offset <- offset16 storage_start (repeat_len16 length u8), + offset <- offset16 storage_start (repeat_len64 length u8), }; /// # Language tag record @@ -2715,14 +2715,14 @@ def lang_tag_record (storage_start : Pos) = { /// Language tag string length length <- u16be, /// Offset to the language tag string data - offset <- offset16 storage_start (repeat_len16 length u8), + offset <- offset16 storage_start (repeat_len64 length u8), }; def name_version_1 (storage_start : Pos) = { /// The number of language tags to expect lang_tag_count <- u16be, /// The array of language tag records - lang_tag_records <- repeat_len16 lang_tag_count (lang_tag_record storage_start), + lang_tag_records <- repeat_len64 lang_tag_count (lang_tag_record storage_start), }; /// # Naming table @@ -2742,7 +2742,7 @@ def name_table = { /// The offset to the string storage area, relative to the start of the naming table. storage_offset <- u16be, /// The array of name records - name_records <- repeat_len16 name_count (name_record (pos_add_u16 table_start storage_offset)), + name_records <- repeat_len64 name_count (name_record (pos_add_u16 table_start storage_offset)), /// Version specific data data <- match version { @@ -2761,9 +2761,9 @@ def name_table = { def loca_table (num_glyphs : U16) (index_to_loc_format : S16) = { offsets <- match index_to_loc_format { // short offsets - 0 => repeat_len16 (u16_add num_glyphs 1) u16be, // TODO Offset16 + 0 => repeat_len64 (u16_add num_glyphs 1) u16be, // TODO Offset16 // long offsets - 1 => repeat_len16 (u16_add num_glyphs 1) u32be, // TODO Offset32 + 1 => repeat_len64 (u16_add num_glyphs 1) u32be, // TODO Offset32 _ => unknown_table } }; @@ -2796,13 +2796,13 @@ def glyph_header = { /// - [Apple's TrueType Reference Manual: The `'loca'` table](https://developer.apple.com/fonts/TrueType-Reference-Manual/RM06/Chap6glyf.html) def simple_glyph (number_of_contours : U16) = { /// Array of point indices for the last point of each contour, in increasing numeric order. - end_pts_of_contours <- repeat_len16 number_of_contours u16be, + end_pts_of_contours <- repeat_len64 number_of_contours u16be, /// Total number of bytes for instructions. If instructionLength is zero, no instructions are /// present for this glyph, and this field is followed directly by the flags field. instruction_length <- u16be, /// Array of instruction byte code for the glyph. - instructions <- repeat_len16 instruction_length u8, - let last_end_point_index = array16_index (number_of_contours - (1 : U16)) end_pts_of_contours, + instructions <- repeat_len64 instruction_length u8, + let last_end_point_index = array64_index (number_of_contours - (1 : U16)) end_pts_of_contours, let number_of_coords = last_end_point_index + (1 : U16), /// Array of flag elements. // flags[variable] <- uint8, @@ -2864,7 +2864,7 @@ def glyph = { /// - [Microsoft's OpenType Spec: Glyph Data](https://docs.microsoft.com/en-us/typography/opentype/spec/glyf) /// - [Apple's TrueType Reference Manual: The `'glyf'` table](https://developer.apple.com/fonts/TrueType-Reference-Manual/RM06/Chap6glyf.html) def glyf_table (num_glyphs : U16) = { - glyphs <- repeat_len16 num_glyphs glyph, + glyphs <- repeat_len64 num_glyphs glyph, }; // ----------------------------------------------------------------------------- @@ -2945,7 +2945,7 @@ def os2_table (table_length : U32) = { y_strikeout_size <- s16be, y_strikeout_position <- s16be, s_family_class <- s16be, - panose <- repeat_len8 10 u8, + panose <- repeat_len64 10 u8, ul_unicode_range1 <- u32be, ul_unicode_range2 <- u32be, ul_unicode_range3 <- u32be, @@ -3021,7 +3021,7 @@ def post_table = { /// Number of glyphs (this should be the same as numGlyphs in 'maxp' table). num_glyphs <- u16be, /// Array of indices into the string data. - glyph_name_index <- repeat_len16 num_glyphs u16be, + glyph_name_index <- repeat_len64 num_glyphs u16be, /// Storage for the string data. string_data <- stream_pos, }, @@ -3030,7 +3030,7 @@ def post_table = { /// Number of glyphs num_glyphs <- u16be, /// Difference between graphic index and standard order of glyph - offset <- repeat_len16 num_glyphs s8, + offset <- repeat_len64 num_glyphs s8, }, /// Version 3, no glyph names stored in font /// @@ -3075,7 +3075,7 @@ def attach_list = ( /// Number of attachment points on this glyph point_count <- u16be, /// Array of contour point indices -in increasing numerical order - point_indices <- repeat_len16 point_count u16be, + point_indices <- repeat_len64 point_count u16be, }; { @@ -3087,7 +3087,7 @@ def attach_list = ( glyph_count <- u16be, /// Array of offsets to AttachPoint tables-from beginning of AttachList table-in Coverage Index /// order - attach_point_offsets <- repeat_len16 glyph_count (offset16 table_start attach_point_table), + attach_point_offsets <- repeat_len64 glyph_count (offset16 table_start attach_point_table), } ); @@ -3156,7 +3156,7 @@ def lig_glyph = { caret_count <- u16be, /// Array of offsets to CaretValue tables, from beginning of LigGlyph table — in increasing /// coordinate order - caret_values <- repeat_len16 caret_count (offset16 table_start caret_value), + caret_values <- repeat_len64 caret_count (offset16 table_start caret_value), }; /// # Ligature Caret List Table @@ -3173,7 +3173,7 @@ def lig_caret_list = { lig_glyph_count <- u16be, /// Array of offsets to LigGlyph tables, from beginning of LigCaretList table — in Coverage /// Index order - lig_glyph_offsets <- repeat_len16 lig_glyph_count (offset16 table_start lig_glyph), + lig_glyph_offsets <- repeat_len64 lig_glyph_count (offset16 table_start lig_glyph), }; /// # Mark Glyph Sets table @@ -3190,7 +3190,7 @@ def mark_glyph_sets = { mark_glyph_set_count <- u16be, /// Array of offsets to mark glyph set coverage tables, from the start of the MarkGlyphSets /// table. - coverage <- repeat_len16 mark_glyph_set_count (offset32 table_start coverage_table), + coverage <- repeat_len64 mark_glyph_set_count (offset32 table_start coverage_table), }; /// # GDEF — Glyph Definition Table diff --git a/formats/opentype.snap b/formats/opentype.snap index 9596e81c9..0e4afee59 100644 --- a/formats/opentype.snap +++ b/formats/opentype.snap @@ -6,7 +6,8 @@ def table_record : Format = { offset <- u32be, length <- u32be, }; -def find_table : fun (@num_tables : U16) -> Array16 num_tables { +def find_table : fun (@num_tables : U16) -> +Array64 (u16_extend_u64 num_tables) { table_id : U32, checksum : U32, offset : U32, @@ -16,7 +17,8 @@ def find_table : fun (@num_tables : U16) -> Array16 num_tables { checksum : U32, offset : U32, length : U32, -} = fun @num_tables table_records table_id => array16_find @num_tables @{ +} = +fun @num_tables table_records table_id => array64_find @(u16_extend_u64 num_tables) @{ table_id : U32, checksum : U32, offset : U32, @@ -42,12 +44,12 @@ def small_glyph_id : Format = u8; def cmap_subtable_format0 : Repr platform_id -> Format = fun platform => { length <- u16be, language <- cmap_language_id platform, - glyph_id_array <- repeat_len16 256 small_glyph_id, + glyph_id_array <- repeat_len64 256 small_glyph_id, }; def cmap_subtable_format2 : Repr platform_id -> Format = fun platform => { length <- u16be, language <- cmap_language_id platform, - sub_header_keys <- repeat_len16 256 u16be, + sub_header_keys <- repeat_len64 256 u16be, }; def reserved : fun (format : Format) -> Repr format -> Format = fun format default => format; @@ -59,18 +61,18 @@ def cmap_subtable_format4 : Repr platform_id -> Format = fun platform => { search_range <- u16be, entry_selector <- u16be, range_shift <- u16be, - end_code <- repeat_len16 seg_count u16be, + end_code <- repeat_len64 (u16_extend_u64 seg_count) u16be, _reserved_pad <- reserved s16be 0, - start_code <- repeat_len16 seg_count u16be, - id_delta <- repeat_len16 seg_count s16be, - id_range_offsets <- repeat_len16 seg_count u16be, + start_code <- repeat_len64 (u16_extend_u64 seg_count) u16be, + id_delta <- repeat_len64 (u16_extend_u64 seg_count) s16be, + id_range_offsets <- repeat_len64 (u16_extend_u64 seg_count) u16be, }; def cmap_subtable_format6 : Repr platform_id -> Format = fun platform => { length <- u16be, language <- cmap_language_id platform, first_code <- u16be, entry_count <- u16be, - glyph_id_array <- repeat_len16 entry_count u16be, + glyph_id_array <- repeat_len64 (u16_extend_u64 entry_count) u16be, }; def language_id32 : Format = u32be; def cmap_language_id32 : Repr platform_id -> Format = @@ -84,9 +86,9 @@ def cmap_subtable_format8 : Repr platform_id -> Format = fun platform => { _reserved <- reserved u16be 0, length <- u32be, language <- cmap_language_id32 platform, - is32 <- repeat_len16 8192 u8, + is32 <- repeat_len64 8192 u8, num_groups <- u32be, - groups <- repeat_len32 num_groups sequential_map_group, + groups <- repeat_len64 (u32_extend_u64 num_groups) sequential_map_group, }; def cmap_subtable_format10 : Repr platform_id -> Format = fun platform => { _reserved <- reserved u16be 0, @@ -94,14 +96,14 @@ def cmap_subtable_format10 : Repr platform_id -> Format = fun platform => { language <- cmap_language_id32 platform, start_char_code <- u32be, num_chars <- u32be, - glyph_id_array <- repeat_len32 num_chars u16be, + glyph_id_array <- repeat_len64 (u32_extend_u64 num_chars) u16be, }; def cmap_subtable_format12 : Repr platform_id -> Format = fun platform => { _reserved <- reserved u16be 0, length <- u32be, language <- cmap_language_id32 platform, num_groups <- u32be, - groups <- repeat_len32 num_groups sequential_map_group, + groups <- repeat_len64 (u32_extend_u64 num_groups) sequential_map_group, }; def constant_map_group : Format = sequential_map_group; def cmap_subtable_format13 : Repr platform_id -> Format = fun platform => { @@ -109,21 +111,21 @@ def cmap_subtable_format13 : Repr platform_id -> Format = fun platform => { length <- u32be, language <- cmap_language_id32 platform, num_groups <- u32be, - groups <- repeat_len32 num_groups constant_map_group, + groups <- repeat_len64 (u32_extend_u64 num_groups) constant_map_group, }; -def u24be : Format = repeat_len8 3 u8; +def u24be : Format = repeat_len64 3 u8; def unicode_range : Format = { start_unicode_value <- u24be, additional_count <- u8, }; def default_uvs_table : Format = { num_unicode_value_ranges <- u32be, - ranges <- repeat_len32 num_unicode_value_ranges unicode_range, + ranges <- repeat_len64 (u32_extend_u64 num_unicode_value_ranges) unicode_range, }; def uvs_mapping : Format = { unicode_value <- u24be, glyph_id <- u16be }; def non_default_uvs_table : Format = { num_uvs_mappings <- u32be, - uvs_mappings <- repeat_len32 num_uvs_mappings uvs_mapping, + uvs_mappings <- repeat_len64 (u32_extend_u64 num_uvs_mappings) uvs_mapping, }; def variation_selector : Pos -> Format = fun table_start => { var_selector <- u24be, @@ -134,7 +136,7 @@ def cmap_subtable_format14 : Repr platform_id -> Pos -> Format = fun platform table_start => { length <- u32be, num_var_selector_records <- u32be, - var_selector <- repeat_len32 num_var_selector_records (variation_selector table_start), + var_selector <- repeat_len64 (u32_extend_u64 num_var_selector_records) (variation_selector table_start), }; def unknown_table : Format = (); def cmap_subtable : Repr platform_id -> Format = fun platform => { @@ -162,7 +164,7 @@ def cmap_table : Format = { table_start <- stream_pos, version <- u16be, num_tables <- u16be, - encoding_records <- repeat_len16 num_tables (encoding_record table_start), + encoding_records <- repeat_len64 (u16_extend_u64 num_tables) (encoding_record table_start), }; def fixed : Format = u32be; def long_date_time : Format = s64be; @@ -239,8 +241,8 @@ def long_horizontal_metric : Format = { }; def htmx_table : U16 -> U16 -> Format = fun number_of_long_horizontal_metrics num_glyphs => { - h_metrics <- repeat_len16 number_of_long_horizontal_metrics long_horizontal_metric, - left_side_bearings <- repeat_len16 (num_glyphs - number_of_long_horizontal_metrics) s16be, + h_metrics <- repeat_len64 (u16_extend_u64 number_of_long_horizontal_metrics) long_horizontal_metric, + left_side_bearings <- repeat_len64 (u16_extend_u64 (num_glyphs - number_of_long_horizontal_metrics)) s16be, }; def offset16 : Pos -> Format -> Format = fun base format => { offset <- u16be, @@ -252,22 +254,22 @@ def name_record : Pos -> Format = fun storage_start => { language <- language_id, name_id <- u16be, length <- u16be, - offset <- offset16 storage_start (repeat_len16 length u8), + offset <- offset16 storage_start (repeat_len64 (u16_extend_u64 length) u8), }; def lang_tag_record : Pos -> Format = fun storage_start => { length <- u16be, - offset <- offset16 storage_start (repeat_len16 length u8), + offset <- offset16 storage_start (repeat_len64 (u16_extend_u64 length) u8), }; def name_version_1 : Pos -> Format = fun storage_start => { lang_tag_count <- u16be, - lang_tag_records <- repeat_len16 lang_tag_count (lang_tag_record storage_start), + lang_tag_records <- repeat_len64 (u16_extend_u64 lang_tag_count) (lang_tag_record storage_start), }; def name_table : Format = { table_start <- stream_pos, version <- u16be, name_count <- u16be, storage_offset <- u16be, - name_records <- repeat_len16 name_count (name_record (table_start + storage_offset)), + name_records <- repeat_len64 (u16_extend_u64 name_count) (name_record (table_start + storage_offset)), data <- match version { 0 => (), 1 => name_version_1 (table_start + storage_offset), @@ -316,7 +318,7 @@ def os2_table : U32 -> Format = fun table_length => { y_strikeout_size <- s16be, y_strikeout_position <- s16be, s_family_class <- s16be, - panose <- repeat_len8 10 u8, + panose <- repeat_len64 10 u8, ul_unicode_range1 <- u32be, ul_unicode_range2 <- u32be, ul_unicode_range3 <- u32be, @@ -349,12 +351,12 @@ def post_table : Format = { 0x10000 => (), 0x20000 => { num_glyphs <- u16be, - glyph_name_index <- repeat_len16 num_glyphs u16be, + glyph_name_index <- repeat_len64 (u16_extend_u64 num_glyphs) u16be, string_data <- stream_pos, }, 0x25000 => { num_glyphs <- u16be, - offset <- repeat_len16 num_glyphs s8, + offset <- repeat_len64 (u16_extend_u64 num_glyphs) s8, }, 0x30000 => (), _ => (), @@ -379,11 +381,10 @@ def composite_glyph : Format = { argument2 <- arg_format flags, }; def simple_glyph : U16 -> Format = fun number_of_contours => { - end_pts_of_contours <- repeat_len16 number_of_contours u16be, + end_pts_of_contours <- repeat_len64 (u16_extend_u64 number_of_contours) u16be, instruction_length <- u16be, - instructions <- repeat_len16 instruction_length u8, - let last_end_point_index : U16 = array16_index @number_of_contours @U16 (number_of_contours - (1 : - U16)) end_pts_of_contours, + instructions <- repeat_len64 (u16_extend_u64 instruction_length) u8, + let last_end_point_index : U16 = array64_index @(u16_extend_u64 number_of_contours) @U16 (u16_extend_u64 number_of_contours - u16_extend_u64 1) end_pts_of_contours, let number_of_coords : U16 = last_end_point_index + (1 : U16), }; def glyph : Format = { @@ -393,19 +394,19 @@ def glyph : Format = { else simple_glyph (s16_unsigned_abs header.number_of_contours), }; def glyf_table : U16 -> Format = fun num_glyphs => { - glyphs <- repeat_len16 num_glyphs glyph, + glyphs <- repeat_len64 (u16_extend_u64 num_glyphs) glyph, }; def loca_table : U16 -> S16 -> Format = fun num_glyphs index_to_loc_format => { offsets <- match index_to_loc_format { - 0 => repeat_len16 (num_glyphs + (1 : U16)) u16be, - 1 => repeat_len16 (num_glyphs + (1 : U16)) u32be, + 0 => repeat_len64 (u16_extend_u64 (num_glyphs + (1 : U16))) u16be, + 1 => repeat_len64 (u16_extend_u64 (num_glyphs + (1 : U16))) u32be, _ => unknown_table, }, }; def base_table : Format = unknown_table; def coverage_format_1 : Format = { glyph_count <- u16be, - glyph_array <- repeat_len16 glyph_count u16be, + glyph_array <- repeat_len64 (u16_extend_u64 glyph_count) u16be, }; def coverage_format_2 : Format = let range_record : Format = { start_glyph_id <- u16be, @@ -414,7 +415,7 @@ def coverage_format_2 : Format = let range_record : Format = { }; { range_count <- u16be, - range_records <- repeat_len16 range_count range_record, + range_records <- repeat_len64 (u16_extend_u64 range_count) range_record, }; def coverage_table : Format = { coverage_format <- u16be, @@ -428,12 +429,12 @@ def mark_glyph_sets : Format = { table_start <- stream_pos, format <- u16be, mark_glyph_set_count <- u16be, - coverage <- repeat_len16 mark_glyph_set_count (offset32 table_start coverage_table), + coverage <- repeat_len64 (u16_extend_u64 mark_glyph_set_count) (offset32 table_start coverage_table), }; def class_def_format_1 : Format = { start_glyph_id <- u16be, glyph_count <- u16be, - class_value_array <- repeat_len16 glyph_count u16be, + class_value_array <- repeat_len64 (u16_extend_u64 glyph_count) u16be, }; def class_def_format_2 : Format = let class_range_record : Format = { start_glyph_id <- u16be, @@ -442,7 +443,7 @@ def class_def_format_2 : Format = let class_range_record : Format = { }; { class_range_count <- u16be, - class_range_records <- repeat_len16 class_range_count class_range_record, + class_range_records <- repeat_len64 (u16_extend_u64 class_range_count) class_range_record, }; def class_def : Format = { class_format <- u16be, @@ -454,13 +455,13 @@ def class_def : Format = { }; def attach_list : Format = let attach_point_table : Format = { point_count <- u16be, - point_indices <- repeat_len16 point_count u16be, + point_indices <- repeat_len64 (u16_extend_u64 point_count) u16be, }; { table_start <- stream_pos, coverage <- offset16 table_start coverage_table, glyph_count <- u16be, - attach_point_offsets <- repeat_len16 glyph_count (offset16 table_start attach_point_table), + attach_point_offsets <- repeat_len64 (u16_extend_u64 glyph_count) (offset16 table_start attach_point_table), }; def device_table : Format = let u16_div_ceil : U16 -> U16 -> U16 = fun numerator denominator => let quotient : U16 = numerator / denominator; @@ -479,14 +480,14 @@ let num_sizes : U16 -> U16 -> U16 = fun start end => end - start + (1 : U16); delta_format <- u16be, delta_values <- let delta_bits : U16 = delta_bits delta_format (num_sizes start_size end_size); - repeat_len16 (u16_div_ceil delta_bits 16) u16be, + repeat_len64 (u16_extend_u64 (u16_div_ceil delta_bits 16)) u16be, }; def variation_index_table : Format = { delta_set_outer_index <- u16be, delta_set_inner_index <- u16be, }; def device_or_variation_index_table : Format = overlap { - init <- { _skipped <- repeat_len8 4 u8, table_format <- u16be }, + init <- { _skipped <- repeat_len64 4 u8, table_format <- u16be }, table <- match init.table_format { 0x1 => device_table, 0x2 => device_table, @@ -516,13 +517,13 @@ let caret_value_format_3 : Pos -> Format = fun table_start => { def lig_glyph : Format = { table_start <- stream_pos, caret_count <- u16be, - caret_values <- repeat_len16 caret_count (offset16 table_start caret_value), + caret_values <- repeat_len64 (u16_extend_u64 caret_count) (offset16 table_start caret_value), }; def lig_caret_list : Format = { table_start <- stream_pos, coverage <- offset16 table_start coverage_table, lig_glyph_count <- u16be, - lig_glyph_offsets <- repeat_len16 lig_glyph_count (offset16 table_start lig_glyph), + lig_glyph_offsets <- repeat_len64 (u16_extend_u64 lig_glyph_count) (offset16 table_start lig_glyph), }; def gdef_table : Format = let gdef_header_version_1_2 : Pos -> Format = fun gdef_start => { @@ -551,7 +552,7 @@ def lang_sys : Format = { lookup_order_offset <- u16be, required_feature_index <- u16be, feature_index_count <- u16be, - feature_indices <- repeat_len16 feature_index_count u16be, + feature_indices <- repeat_len64 (u16_extend_u64 feature_index_count) u16be, }; def lang_sys_record : Pos -> Format = fun script_start => { lang_sys_tag <- tag, @@ -561,7 +562,7 @@ def script_table : Format = { table_start <- stream_pos, default_lang_sys <- offset16 table_start lang_sys, lang_sys_count <- u16be, - lang_sys_records <- repeat_len16 lang_sys_count (lang_sys_record table_start), + lang_sys_records <- repeat_len64 (u16_extend_u64 lang_sys_count) (lang_sys_record table_start), }; def script_list : Format = let script_record : Pos -> Format = fun script_list_start => { @@ -571,13 +572,13 @@ fun script_list_start => { { table_start <- stream_pos, script_count <- u16be, - script_records <- repeat_len16 script_count (script_record table_start), + script_records <- repeat_len64 (u16_extend_u64 script_count) (script_record table_start), }; def feature_table : Format = { table_start <- stream_pos, feature_params <- u16be, lookup_index_count <- u16be, - lookup_list_indices <- repeat_len16 lookup_index_count u16be, + lookup_list_indices <- repeat_len64 (u16_extend_u64 lookup_index_count) u16be, }; def feature_list : Format = let feature_record : Pos -> Format = fun feature_list_start => { @@ -587,7 +588,7 @@ fun feature_list_start => { { table_start <- stream_pos, feature_count <- u16be, - feature_records <- repeat_len16 feature_count (feature_record table_start), + feature_records <- repeat_len64 (u16_extend_u64 feature_count) (feature_record table_start), }; def single_substitution : Format = { table_start <- stream_pos, @@ -600,14 +601,14 @@ def single_substitution : Format = { 2 => { coverage <- offset16 table_start coverage_table, glyph_count <- u16be, - substitute_glyph_ids <- repeat_len16 glyph_count u16be, + substitute_glyph_ids <- repeat_len64 (u16_extend_u64 glyph_count) u16be, }, _ => unknown_table, }, }; def multiple_substitution : Format = let sequence_table : Format = { glyph_count <- u16be, - substitute_glyph_ids <- repeat_len16 glyph_count u16be, + substitute_glyph_ids <- repeat_len64 (u16_extend_u64 glyph_count) u16be, }; { table_start <- stream_pos, @@ -616,14 +617,14 @@ def multiple_substitution : Format = let sequence_table : Format = { subst <- match subst_format { 1 => { sequence_count <- u16be, - sequences <- repeat_len16 sequence_count (offset16 table_start sequence_table), + sequences <- repeat_len64 (u16_extend_u64 sequence_count) (offset16 table_start sequence_table), }, _ => unknown_table, }, }; def alternate_substitution : Format = let alternate_set : Format = { glyph_count <- u16be, - alternate_glyph_ids <- repeat_len16 glyph_count u16be, + alternate_glyph_ids <- repeat_len64 (u16_extend_u64 glyph_count) u16be, }; { table_start <- stream_pos, @@ -632,7 +633,7 @@ def alternate_substitution : Format = let alternate_set : Format = { subst <- match subst_format { 1 => { alternate_set_count <- u16be, - alternate_sets <- repeat_len16 alternate_set_count (offset16 table_start alternate_set), + alternate_sets <- repeat_len64 (u16_extend_u64 alternate_set_count) (offset16 table_start alternate_set), }, _ => unknown_table, }, @@ -640,12 +641,13 @@ def alternate_substitution : Format = let alternate_set : Format = { def ligature_substitution : Format = let ligature_table : Format = { ligature_glyph <- u16be, component_count <- u16be, - component_glyph_ids <- repeat_len16 (component_count - (1 : U16)) u16be, + component_glyph_ids <- repeat_len64 (u16_extend_u64 (component_count - (1 : + U16))) u16be, }; let ligature_set : Format = { table_start <- stream_pos, ligature_count <- u16be, - ligatures <- repeat_len16 ligature_count (offset16 table_start ligature_table), + ligatures <- repeat_len64 (u16_extend_u64 ligature_count) (offset16 table_start ligature_table), }; { table_start <- stream_pos, @@ -654,7 +656,7 @@ let ligature_set : Format = { subst <- match subst_format { 1 => { ligature_set_count <- u16be, - ligature_sets <- repeat_len16 ligature_set_count (offset16 table_start ligature_set), + ligature_sets <- repeat_len64 (u16_extend_u64 ligature_set_count) (offset16 table_start ligature_set), }, _ => unknown_table, }, @@ -666,44 +668,46 @@ def sequence_lookup_record : Format = { def sequence_context_format1 : Format = let sequence_rule : Format = { glyph_count <- u16be, seq_lookup_count <- u16be, - input_sequence <- repeat_len16 (glyph_count - (1 : U16)) u16be, - seq_lookup_records <- repeat_len16 seq_lookup_count sequence_lookup_record, + input_sequence <- repeat_len64 (u16_extend_u64 (glyph_count - (1 : + U16))) u16be, + seq_lookup_records <- repeat_len64 (u16_extend_u64 seq_lookup_count) sequence_lookup_record, }; let sequence_rule_set : Format = { table_start <- stream_pos, seq_rule_count <- u16be, - seq_rules <- repeat_len16 seq_rule_count (offset16 table_start sequence_rule), + seq_rules <- repeat_len64 (u16_extend_u64 seq_rule_count) (offset16 table_start sequence_rule), }; { table_start <- stream_pos, coverage <- offset16 table_start coverage_table, seq_rule_set_count <- u16be, - seq_rule_sets <- repeat_len16 seq_rule_set_count (offset16 table_start sequence_rule_set), + seq_rule_sets <- repeat_len64 (u16_extend_u64 seq_rule_set_count) (offset16 table_start sequence_rule_set), }; def sequence_context_format2 : Format = let class_sequence_rule : Format = { glyph_count <- u16be, seq_lookup_count <- u16be, - input_sequence <- repeat_len16 (glyph_count - (1 : U16)) u16be, - seqLookupRecords <- repeat_len16 seq_lookup_count sequence_lookup_record, + input_sequence <- repeat_len64 (u16_extend_u64 (glyph_count - (1 : + U16))) u16be, + seqLookupRecords <- repeat_len64 (u16_extend_u64 seq_lookup_count) sequence_lookup_record, }; let class_sequence_rule_set : Format = { table_start <- stream_pos, class_seq_rule_count <- u16be, - class_seq_rules <- repeat_len16 class_seq_rule_count (offset16 table_start class_sequence_rule), + class_seq_rules <- repeat_len64 (u16_extend_u64 class_seq_rule_count) (offset16 table_start class_sequence_rule), }; { table_start <- stream_pos, coverage <- offset16 table_start coverage_table, class_def <- offset16 table_start class_def, class_seq_rule_set_count <- u16be, - class_seq_rule_sets <- repeat_len16 class_seq_rule_set_count (offset16 table_start class_sequence_rule_set), + class_seq_rule_sets <- repeat_len64 (u16_extend_u64 class_seq_rule_set_count) (offset16 table_start class_sequence_rule_set), }; def sequence_context_format3 : Format = { table_start <- stream_pos, glyph_count <- u16be, seq_lookup_count <- u16be, - coverage_tables <- repeat_len16 glyph_count (offset16 table_start coverage_table), - seq_lookup_records <- repeat_len16 seq_lookup_count sequence_lookup_record, + coverage_tables <- repeat_len64 (u16_extend_u64 glyph_count) (offset16 table_start coverage_table), + seq_lookup_records <- repeat_len64 (u16_extend_u64 seq_lookup_count) sequence_lookup_record, }; def sequence_context : Format = { format <- u16be, @@ -730,11 +734,11 @@ let reverse_chain_single_subst_format1 : Format = { table_start <- stream_pos, coverage <- offset16 table_start coverage_table, backtrack_glyph_count <- u16be, - backtrack_coverage_tables <- repeat_len16 backtrack_glyph_count (offset16 table_start coverage_table), + backtrack_coverage_tables <- repeat_len64 (u16_extend_u64 backtrack_glyph_count) (offset16 table_start coverage_table), lookahead_glyph_count <- u16be, - lookahead_coverage_tables <- repeat_len16 lookahead_glyph_count (offset16 table_start coverage_table), + lookahead_coverage_tables <- repeat_len64 (u16_extend_u64 lookahead_glyph_count) (offset16 table_start coverage_table), glyph_count <- u16be, - substitute_glyph_ids <- repeat_len16 glyph_count u16be, + substitute_glyph_ids <- repeat_len64 (u16_extend_u64 glyph_count) u16be, }; { subst_format <- u16be, @@ -796,7 +800,7 @@ let single_pos_format2 : Pos -> Format = fun table_start => { coverage_offset <- offset16 table_start coverage_table, value_format <- u16be, value_count <- u16be, - value_records <- repeat_len16 value_count (value_record table_start value_format), + value_records <- repeat_len64 (u16_extend_u64 value_count) (value_record table_start value_format), }; { table_start <- stream_pos, @@ -820,14 +824,14 @@ Format = fun table_start value_format1 value_format2 => { let pair_set : U16 -> U16 -> Format = fun value_format1 value_format2 => { table_start <- stream_pos, pair_value_count <- u16be, - pair_value_records <- repeat_len16 pair_value_count (pair_value_record table_start value_format1 value_format2), + pair_value_records <- repeat_len64 (u16_extend_u64 pair_value_count) (pair_value_record table_start value_format1 value_format2), }; let pair_pos_format1 : Pos -> Format = fun table_start => { coverage <- offset16 table_start coverage_table, value_format1 <- u16be, value_format2 <- u16be, pair_set_count <- u16be, - pair_sets <- repeat_len16 pair_set_count (offset16 table_start (pair_set value_format1 value_format2)), + pair_sets <- repeat_len64 (u16_extend_u64 pair_set_count) (offset16 table_start (pair_set value_format1 value_format2)), }; let class2_record : Pos -> U16 -> U16 -> Format = fun table_start value_format1 value_format2 => { @@ -836,7 +840,7 @@ fun table_start value_format1 value_format2 => { }; let class1_record : Pos -> U16 -> U16 -> U16 -> Format = fun table_start class2_count value_format1 value_format2 => { - class2_records <- repeat_len16 class2_count (class2_record table_start value_format1 value_format2), + class2_records <- repeat_len64 (u16_extend_u64 class2_count) (class2_record table_start value_format1 value_format2), }; let pair_pos_format2 : Pos -> Format = fun pair_pos_start => { coverage <- offset16 pair_pos_start coverage_table, @@ -846,7 +850,7 @@ let pair_pos_format2 : Pos -> Format = fun pair_pos_start => { class_def2 <- offset16 pair_pos_start class_def, class1_count <- u16be, class2_count <- u16be, - class1_records <- repeat_len16 class1_count (class1_record pair_pos_start class2_count value_format1 value_format2), + class1_records <- repeat_len64 (u16_extend_u64 class1_count) (class1_record pair_pos_start class2_count value_format1 value_format2), }; { table_start <- stream_pos, @@ -884,7 +888,7 @@ fun table_start => { let cursive_pos_format1 : Pos -> Format = fun table_start => { coverage <- offset16 table_start coverage_table, entry_exit_count <- u16be, - entry_exit_record <- repeat_len16 entry_exit_count (entry_exit_record table_start), + entry_exit_record <- repeat_len64 (u16_extend_u64 entry_exit_count) (entry_exit_record table_start), }; { table_start <- stream_pos, @@ -902,16 +906,16 @@ fun table_start => { { table_start <- stream_pos, mark_count <- u16be, - mark_records <- repeat_len16 mark_count (mark_record table_start), + mark_records <- repeat_len64 (u16_extend_u64 mark_count) (mark_record table_start), }; def mark_to_base_attachment : Format = let base_record : Pos -> U16 -> Format = fun table_start mark_class_count => { - base_anchors <- repeat_len16 mark_class_count (offset16 table_start anchor_table), + base_anchors <- repeat_len64 (u16_extend_u64 mark_class_count) (offset16 table_start anchor_table), }; let base_array_table : Pos -> U16 -> Format = fun table_start mark_class_count => { base_count <- u16be, - base_records <- repeat_len16 base_count (base_record table_start mark_class_count), + base_records <- repeat_len64 (u16_extend_u64 base_count) (base_record table_start mark_class_count), }; let mark_base_pos_format1 : Pos -> Format = fun table_start => { mark_coverage <- offset16 table_start coverage_table, @@ -930,17 +934,17 @@ let mark_base_pos_format1 : Pos -> Format = fun table_start => { }; def mark_to_ligature_attachment : Format = let component_record : Pos -> U16 -> Format = fun table_start mark_class_count => { - ligature_anchors <- repeat_len16 mark_class_count (offset16 table_start anchor_table), + ligature_anchors <- repeat_len64 (u16_extend_u64 mark_class_count) (offset16 table_start anchor_table), }; let ligature_attach : Pos -> U16 -> Format = fun table_start mark_class_count => { component_count <- u16be, - component_records <- repeat_len16 component_count (component_record table_start mark_class_count), + component_records <- repeat_len64 (u16_extend_u64 component_count) (component_record table_start mark_class_count), }; let ligature_array : Pos -> U16 -> Format = fun table_start mark_class_count => { ligature_count <- u16be, - ligature_attaches <- repeat_len16 ligature_count (offset16 table_start (ligature_attach table_start mark_class_count)), + ligature_attaches <- repeat_len64 (u16_extend_u64 ligature_count) (offset16 table_start (ligature_attach table_start mark_class_count)), }; let mark_lig_pos_format1 : Pos -> Format = fun table_start => { mark_coverage <- offset16 table_start coverage_table, @@ -1015,7 +1019,7 @@ let lookup_subtable : U32 -> U16 -> Format = fun tag lookup_type => match tag { lookup_type <- u16be, lookup_flag <- u16be, sub_table_count <- u16be, - subtables <- repeat_len16 sub_table_count (offset16 table_start (lookup_subtable tag lookup_type)), + subtables <- repeat_len64 (u16_extend_u64 sub_table_count) (offset16 table_start (lookup_subtable tag lookup_type)), mark_filtering_set <- if u16_and lookup_flag USE_MARK_FILTERING_SET != (0 : U16) then u16be @@ -1024,7 +1028,7 @@ let lookup_subtable : U32 -> U16 -> Format = fun tag lookup_type => match tag { def lookup_list : U32 -> Format = fun tag => { table_start <- stream_pos, lookup_count <- u16be, - lookups <- repeat_len16 lookup_count (offset16 table_start (lookup_table tag)), + lookups <- repeat_len64 (u16_extend_u64 lookup_count) (offset16 table_start (lookup_table tag)), }; def layout_table : U32 -> Format = fun tag => { table_start <- stream_pos, @@ -1045,7 +1049,7 @@ def table_directory : Pos -> Format = fun file_start => { search_range <- u16be, entry_selector <- u16be, range_shift <- u16be, - table_records <- repeat_len16 num_tables table_record, + table_records <- repeat_len64 (u16_extend_u64 num_tables) table_record, table_links <- let required_table : U32 -> Format -> Format = fun table_id table_format => { table_record <- unwrap @{ @@ -1246,11 +1250,11 @@ def table_directory : Pos -> Format = fun file_start => { def ttc_header : Pos -> Format = fun start => let ttc_header1 : Pos -> Format = fun start => { num_fonts <- u32be, - table_directories <- repeat_len32 num_fonts (offset32 start (table_directory start)), + table_directories <- repeat_len64 (u32_extend_u64 num_fonts) (offset32 start (table_directory start)), }; let ttc_header2 : Pos -> Format = fun start => { num_fonts <- u32be, - table_directories <- repeat_len32 num_fonts (offset32 start (table_directory start)), + table_directories <- repeat_len64 (u32_extend_u64 num_fonts) (offset32 start (table_directory start)), dsig_tag <- u32be, dsig_length <- u32be, dsig_offset <- u32be, @@ -1281,40 +1285,42 @@ def f2dot14 : Format = s16be; def chained_sequence_context_format_1 : Format = let chained_sequence_rule : Format = { backtrack_glyph_count <- u16be, - backtrack_sequence <- repeat_len16 backtrack_glyph_count u16be, + backtrack_sequence <- repeat_len64 (u16_extend_u64 backtrack_glyph_count) u16be, input_glyph_count <- u16be, - input_sequence <- repeat_len16 (input_glyph_count - (1 : U16)) u16be, + input_sequence <- repeat_len64 (u16_extend_u64 (input_glyph_count - (1 : + U16))) u16be, lookahead_glyph_count <- u16be, - lookahead_sequence <- repeat_len16 lookahead_glyph_count u16be, + lookahead_sequence <- repeat_len64 (u16_extend_u64 lookahead_glyph_count) u16be, seq_lookup_count <- u16be, - seq_lookup_records <- repeat_len16 seq_lookup_count sequence_lookup_record, + seq_lookup_records <- repeat_len64 (u16_extend_u64 seq_lookup_count) sequence_lookup_record, }; let chained_sequence_rule_set : Format = { table_start <- stream_pos, chained_seq_rule_count <- u16be, - chained_seq_rules <- repeat_len16 chained_seq_rule_count (offset16 table_start chained_sequence_rule), + chained_seq_rules <- repeat_len64 (u16_extend_u64 chained_seq_rule_count) (offset16 table_start chained_sequence_rule), }; { table_start <- stream_pos, coverage <- offset16 table_start coverage_table, chained_seq_rule_set_count <- u16be, - chained_seq_rule_sets <- repeat_len16 chained_seq_rule_set_count (offset16 table_start chained_sequence_rule_set), + chained_seq_rule_sets <- repeat_len64 (u16_extend_u64 chained_seq_rule_set_count) (offset16 table_start chained_sequence_rule_set), }; def chained_sequence_context_format_2 : Format = let chained_class_sequence_rule : Format = { backtrack_glyph_count <- u16be, - backtrack_sequence <- repeat_len16 backtrack_glyph_count u16be, + backtrack_sequence <- repeat_len64 (u16_extend_u64 backtrack_glyph_count) u16be, input_glyph_count <- u16be, - input_sequence <- repeat_len16 (input_glyph_count - (1 : U16)) u16be, + input_sequence <- repeat_len64 (u16_extend_u64 (input_glyph_count - (1 : + U16))) u16be, lookahead_glyph_count <- u16be, - lookahead_sequence <- repeat_len16 lookahead_glyph_count u16be, + lookahead_sequence <- repeat_len64 (u16_extend_u64 lookahead_glyph_count) u16be, seq_lookup_count <- u16be, - seq_lookup_records <- repeat_len16 seq_lookup_count sequence_lookup_record, + seq_lookup_records <- repeat_len64 (u16_extend_u64 seq_lookup_count) sequence_lookup_record, }; let chained_class_sequence_rule_set : Format = { table_start <- stream_pos, chained_class_seq_rule_count <- u16be, - chained_class_seq_rules <- repeat_len16 chained_class_seq_rule_count (offset16 table_start chained_class_sequence_rule), + chained_class_seq_rules <- repeat_len64 (u16_extend_u64 chained_class_seq_rule_count) (offset16 table_start chained_class_sequence_rule), }; { table_start <- stream_pos, @@ -1323,18 +1329,18 @@ let chained_class_sequence_rule_set : Format = { input_class_def <- offset16 table_start class_def, lookahead_class_def <- offset16 table_start class_def, chained_class_seq_rule_set_count <- u16be, - chained_class_seq_rule_sets <- repeat_len16 chained_class_seq_rule_set_count (offset16 table_start chained_class_sequence_rule_set), + chained_class_seq_rule_sets <- repeat_len64 (u16_extend_u64 chained_class_seq_rule_set_count) (offset16 table_start chained_class_sequence_rule_set), }; def chained_sequence_context_format_3 : Format = { table_start <- stream_pos, backtrack_glyph_count <- u16be, - backtrack_coverages <- repeat_len16 backtrack_glyph_count (offset16 table_start coverage_table), + backtrack_coverages <- repeat_len64 (u16_extend_u64 backtrack_glyph_count) (offset16 table_start coverage_table), input_glyph_count <- u16be, - input_coverage_tables <- repeat_len16 input_glyph_count (offset16 table_start coverage_table), + input_coverage_tables <- repeat_len64 (u16_extend_u64 input_glyph_count) (offset16 table_start coverage_table), lookahead_glyph_count <- u16be, - lookahead_coverages <- repeat_len16 lookahead_glyph_count (offset16 table_start coverage_table), + lookahead_coverages <- repeat_len64 (u16_extend_u64 lookahead_glyph_count) (offset16 table_start coverage_table), seq_lookup_count <- u16be, - seq_lookup_records <- repeat_len16 seq_lookup_count sequence_lookup_record, + seq_lookup_records <- repeat_len64 (u16_extend_u64 seq_lookup_count) sequence_lookup_record, }; ''' stderr = '' diff --git a/formats/stl-binary.fathom b/formats/stl-binary.fathom index b56b3556a..72dba09ac 100644 --- a/formats/stl-binary.fathom +++ b/formats/stl-binary.fathom @@ -21,12 +21,12 @@ def vec3d = { def triangle = { normal <- vec3d, - vertices <- repeat_len8 3 vec3d, + vertices <- repeat_len64 3 vec3d, attribute_byte_count <- u16le, }; def main = { - header <- repeat_len8 80 u8, + header <- repeat_len64 80 u8, triangle_count <- u32le, - triangles <- repeat_len32 triangle_count triangle, + triangles <- repeat_len64 triangle_count triangle, }; diff --git a/formats/stl-binary.snap b/formats/stl-binary.snap index 642283791..0e16cfc08 100644 --- a/formats/stl-binary.snap +++ b/formats/stl-binary.snap @@ -2,13 +2,13 @@ stdout = ''' def vec3d : Format = { x <- f32le, y <- f32le, z <- f32le }; def triangle : Format = { normal <- vec3d, - vertices <- repeat_len8 3 vec3d, + vertices <- repeat_len64 3 vec3d, attribute_byte_count <- u16le, }; def main : Format = { - header <- repeat_len8 80 u8, + header <- repeat_len64 80 u8, triangle_count <- u32le, - triangles <- repeat_len32 triangle_count triangle, + triangles <- repeat_len64 (u32_extend_u64 triangle_count) triangle, }; ''' stderr = '' diff --git a/formats/unwrap-none.fathom b/formats/unwrap-none.fathom index 267c402f2..acf160325 100644 --- a/formats/unwrap-none.fathom +++ b/formats/unwrap-none.fathom @@ -1,4 +1,4 @@ def main = { - let ary : Array16 3 U16 = [1, 2, 3], - x <- unwrap (array16_find (fun (el : U16) => el == (4 : U16)) ary), + let ary : Array64 3 U16 = [1, 2, 3], + x <- unwrap (array64_find (fun (el : U16) => el == (4 : U16)) ary), }; diff --git a/formats/unwrap-none.snap b/formats/unwrap-none.snap index f12ac67f3..d4fc29cdb 100644 --- a/formats/unwrap-none.snap +++ b/formats/unwrap-none.snap @@ -1,7 +1,7 @@ stdout = ''' def main : Format = { - let ary : Array16 3 U16 = [1, 2, 3], - x <- unwrap @U16 (array16_find @3 @U16 (fun el => el == (4 : U16)) ary), + let ary : Array64 3 U16 = [1, 2, 3], + x <- unwrap @U16 (array64_find @3 @U16 (fun el => el == (4 : U16)) ary), }; ''' stderr = '' diff --git a/tests/cmd/fathom-elab.md b/tests/cmd/fathom-elab.md index be4258003..657634c59 100644 --- a/tests/cmd/fathom-elab.md +++ b/tests/cmd/fathom-elab.md @@ -44,10 +44,10 @@ Modules can be elaborated with `--module` ```console $ fathom elab --module formats/object-id.fathom -def u24be : Format = repeat_len8 3 u8; +def u24be : Format = repeat_len64 3 u8; def main : Format = { timestamp <- u32be, - random <- repeat_len8 5 u8, + random <- repeat_len64 5 u8, counter <- u24be, }; diff --git a/tests/fail/elaboration/mismatched-array-length/array16.fathom b/tests/fail/elaboration/mismatched-array-length/array16.fathom deleted file mode 100644 index 94021c2cd..000000000 --- a/tests/fail/elaboration/mismatched-array-length/array16.fathom +++ /dev/null @@ -1,3 +0,0 @@ -//~ exit-code = 1 - -[34] : Array16 0 U32 diff --git a/tests/fail/elaboration/mismatched-array-length/array16.snap b/tests/fail/elaboration/mismatched-array-length/array16.snap deleted file mode 100644 index 4729df4b7..000000000 --- a/tests/fail/elaboration/mismatched-array-length/array16.snap +++ /dev/null @@ -1,12 +0,0 @@ -stdout = '' -stderr = ''' -error: mismatched array length - ┌─ tests/fail/elaboration/mismatched-array-length/array16.fathom:3:1 - │ -3 │ [34] : Array16 0 U32 - │ ^^^^ array with invalid length - │ - = expected length 0 - = found length 1 - -''' diff --git a/tests/fail/elaboration/mismatched-array-length/array32.fathom b/tests/fail/elaboration/mismatched-array-length/array32.fathom deleted file mode 100644 index c633bc698..000000000 --- a/tests/fail/elaboration/mismatched-array-length/array32.fathom +++ /dev/null @@ -1,3 +0,0 @@ -//~ exit-code = 1 - -[1] : Array32 3 U32 diff --git a/tests/fail/elaboration/mismatched-array-length/array32.snap b/tests/fail/elaboration/mismatched-array-length/array32.snap deleted file mode 100644 index 12f88497b..000000000 --- a/tests/fail/elaboration/mismatched-array-length/array32.snap +++ /dev/null @@ -1,12 +0,0 @@ -stdout = '' -stderr = ''' -error: mismatched array length - ┌─ tests/fail/elaboration/mismatched-array-length/array32.fathom:3:1 - │ -3 │ [1] : Array32 3 U32 - │ ^^^ array with invalid length - │ - = expected length 3 - = found length 1 - -''' diff --git a/tests/fail/elaboration/mismatched-array-length/array8.fathom b/tests/fail/elaboration/mismatched-array-length/array8.fathom deleted file mode 100644 index 3b1c10e54..000000000 --- a/tests/fail/elaboration/mismatched-array-length/array8.fathom +++ /dev/null @@ -1,3 +0,0 @@ -//~ exit-code = 1 - -[] : Array8 2 U32 diff --git a/tests/fail/elaboration/mismatched-array-length/array8.snap b/tests/fail/elaboration/mismatched-array-length/array8.snap deleted file mode 100644 index 68f57543a..000000000 --- a/tests/fail/elaboration/mismatched-array-length/array8.snap +++ /dev/null @@ -1,12 +0,0 @@ -stdout = '' -stderr = ''' -error: mismatched array length - ┌─ tests/fail/elaboration/mismatched-array-length/array8.fathom:3:1 - │ -3 │ [] : Array8 2 U32 - │ ^^ array with invalid length - │ - = expected length 2 - = found length 0 - -''' diff --git a/tests/fail/elaboration/numeric-literal/mismatched-length.fathom b/tests/fail/elaboration/numeric-literal/mismatched-length.fathom index 847ecc4f6..7b98a4f5e 100644 --- a/tests/fail/elaboration/numeric-literal/mismatched-length.fathom +++ b/tests/fail/elaboration/numeric-literal/mismatched-length.fathom @@ -1,3 +1,3 @@ //~ exit-code = 1 -[3, 4] : Array8 12 U32 +[3, 4] : Array64 12 U32 diff --git a/tests/fail/elaboration/numeric-literal/mismatched-length.snap b/tests/fail/elaboration/numeric-literal/mismatched-length.snap index cdadc4b5b..0dbd772f7 100644 --- a/tests/fail/elaboration/numeric-literal/mismatched-length.snap +++ b/tests/fail/elaboration/numeric-literal/mismatched-length.snap @@ -3,7 +3,7 @@ stderr = ''' error: mismatched array length ┌─ tests/fail/elaboration/numeric-literal/mismatched-length.fathom:3:1 │ -3 │ [3, 4] : Array8 12 U32 +3 │ [3, 4] : Array64 12 U32 │ ^^^^^^ array with invalid length │ = expected length 12 diff --git a/tests/succeed/ann/array-literal-array16.fathom b/tests/succeed/ann/array-literal-array16.fathom deleted file mode 100644 index 99c08e6ec..000000000 --- a/tests/succeed/ann/array-literal-array16.fathom +++ /dev/null @@ -1 +0,0 @@ -[] : Array16 0 U32 diff --git a/tests/succeed/ann/array-literal-array16.snap b/tests/succeed/ann/array-literal-array16.snap deleted file mode 100644 index dcf7a189a..000000000 --- a/tests/succeed/ann/array-literal-array16.snap +++ /dev/null @@ -1,4 +0,0 @@ -stdout = ''' -[] : Array16 0 U32 -''' -stderr = '' diff --git a/tests/succeed/ann/array-literal-array32.fathom b/tests/succeed/ann/array-literal-array32.fathom deleted file mode 100644 index c62158a5d..000000000 --- a/tests/succeed/ann/array-literal-array32.fathom +++ /dev/null @@ -1 +0,0 @@ -[1, 2, 3] : Array32 3 U32 diff --git a/tests/succeed/ann/array-literal-array32.snap b/tests/succeed/ann/array-literal-array32.snap deleted file mode 100644 index 9ce81b9ae..000000000 --- a/tests/succeed/ann/array-literal-array32.snap +++ /dev/null @@ -1,4 +0,0 @@ -stdout = ''' -[1, 2, 3] : Array32 3 U32 -''' -stderr = '' diff --git a/tests/succeed/ann/array-literal-array8.fathom b/tests/succeed/ann/array-literal-array8.fathom deleted file mode 100644 index 921846036..000000000 --- a/tests/succeed/ann/array-literal-array8.fathom +++ /dev/null @@ -1 +0,0 @@ -[3, 4] : Array8 2 U32 diff --git a/tests/succeed/ann/array-literal-array8.snap b/tests/succeed/ann/array-literal-array8.snap deleted file mode 100644 index ea9af0c60..000000000 --- a/tests/succeed/ann/array-literal-array8.snap +++ /dev/null @@ -1,4 +0,0 @@ -stdout = ''' -[3, 4] : Array8 2 U32 -''' -stderr = '' diff --git a/tests/succeed/binops/synth.fathom b/tests/succeed/binops/synth.fathom index b89ae12f7..927852dcb 100644 --- a/tests/succeed/binops/synth.fathom +++ b/tests/succeed/binops/synth.fathom @@ -32,7 +32,7 @@ let device_table = ( /// Array of compressed data delta_values <- let delta_bits = delta_bits delta_format (num_sizes start_size end_size); - repeat_len16 (u16_div_ceil delta_bits 16) u16be, + repeat_len64 (u16_div_ceil delta_bits 16) u16be, } ); diff --git a/tests/succeed/binops/synth.snap b/tests/succeed/binops/synth.snap index ff3bf27b2..623ab140c 100644 --- a/tests/succeed/binops/synth.snap +++ b/tests/succeed/binops/synth.snap @@ -16,7 +16,7 @@ let num_sizes : U16 -> U16 -> U16 = fun start end => end - start + (1 : U16); delta_format <- u16be, delta_values <- let delta_bits : U16 = delta_bits delta_format (num_sizes start_size end_size); - repeat_len16 (u16_div_ceil delta_bits 16) u16be, + repeat_len64 (u16_extend_u64 (u16_div_ceil delta_bits 16)) u16be, }; () : () ''' diff --git a/tests/succeed/format-deref/simple.fathom b/tests/succeed/format-deref/simple.fathom index 7c1ce685d..47b6b216c 100644 --- a/tests/succeed/format-deref/simple.fathom +++ b/tests/succeed/format-deref/simple.fathom @@ -3,5 +3,5 @@ link <- link start u16be, len <- deref link, _reserved <- u16be, - data <- repeat_len16 len u16be, + data <- repeat_len64 len u16be, } diff --git a/tests/succeed/format-deref/simple.snap b/tests/succeed/format-deref/simple.snap index e34454805..dfd2deac7 100644 --- a/tests/succeed/format-deref/simple.snap +++ b/tests/succeed/format-deref/simple.snap @@ -4,7 +4,7 @@ stdout = ''' link <- link start u16be, len <- deref @u16be link, _reserved <- u16be, - data <- repeat_len16 len u16be, + data <- repeat_len64 (u16_extend_u64 len) u16be, } : Format ''' stderr = '' diff --git a/tests/succeed/format-overlap/dependent.fathom b/tests/succeed/format-overlap/dependent.fathom index 7c7764763..8f993f7c7 100644 --- a/tests/succeed/format-overlap/dependent.fathom +++ b/tests/succeed/format-overlap/dependent.fathom @@ -7,7 +7,7 @@ let record0 = { let record1 = fun (length : U8) => { _length <- u8, // Skip length - data <- repeat_len8 length u8, + data <- repeat_len64 length u8, }; let silly = overlap { @@ -18,7 +18,7 @@ let silly = overlap { let _ : Repr silly -> { record0 : { length : U8 }, - record1 : { _length : U8, data : Array8 record0.length U8 }, + record1 : { _length : U8, data : Array64 record0.length U8 }, } = fun silly => silly; diff --git a/tests/succeed/format-overlap/dependent.snap b/tests/succeed/format-overlap/dependent.snap index 0f017d55c..fbb0c600a 100644 --- a/tests/succeed/format-overlap/dependent.snap +++ b/tests/succeed/format-overlap/dependent.snap @@ -2,7 +2,7 @@ stdout = ''' let record0 : Format = { length <- u8 }; let record1 : U8 -> Format = fun length => { _length <- u8, - data <- repeat_len8 length u8, + data <- repeat_len64 (u8_extend_u64 length) u8, }; let silly : Format = overlap { record0 <- record0, @@ -10,7 +10,10 @@ let silly : Format = overlap { }; let _ : Repr silly -> { record0 : { length : U8 }, - record1 : { _length : U8, data : Array8 record0.length U8 }, + record1 : { + _length : U8, + data : Array64 (u8_extend_u64 record0.length) U8, + }, } = fun silly => silly; () : () ''' diff --git a/tests/succeed/format-record/computed-fields.fathom b/tests/succeed/format-record/computed-fields.fathom index e07dbbef6..837834b52 100644 --- a/tests/succeed/format-record/computed-fields.fathom +++ b/tests/succeed/format-record/computed-fields.fathom @@ -5,15 +5,15 @@ let format = { /// Number of contiguous ranges of character codes let seg_count = u16_div seg_count_x2 2, - start_code <- repeat_len16 seg_count u16be, - id_delta <- repeat_len16 seg_count s16be, + start_code <- repeat_len64 seg_count u16be, + id_delta <- repeat_len64 seg_count s16be, }; let _ : Repr format -> { seg_count_x2 : U16, seg_count : U16, - start_code : Array16 seg_count U16, - id_delta : Array16 seg_count S16, + start_code : Array64 seg_count U16, + id_delta : Array64 seg_count S16, } = fun x => x; let format = { diff --git a/tests/succeed/format-record/computed-fields.snap b/tests/succeed/format-record/computed-fields.snap index fdf12baa8..86fbd11f5 100644 --- a/tests/succeed/format-record/computed-fields.snap +++ b/tests/succeed/format-record/computed-fields.snap @@ -2,14 +2,14 @@ stdout = ''' let format : Format = { seg_count_x2 <- u16be, let seg_count : U16 = seg_count_x2 / (2 : U16), - start_code <- repeat_len16 seg_count u16be, - id_delta <- repeat_len16 seg_count s16be, + start_code <- repeat_len64 (u16_extend_u64 seg_count) u16be, + id_delta <- repeat_len64 (u16_extend_u64 seg_count) s16be, }; let _ : Repr format -> { seg_count_x2 : U16, seg_count : U16, - start_code : Array16 seg_count U16, - id_delta : Array16 seg_count S16, + start_code : Array64 (u16_extend_u64 seg_count) U16, + id_delta : Array64 (u16_extend_u64 seg_count) S16, } = fun x => x; let format : Format = { let x : U32 = 256 }; let _ : Repr format -> { x : U32 } = fun x => x; diff --git a/tests/succeed/format-record/field-refinements.fathom b/tests/succeed/format-record/field-refinements.fathom index 94a6c5e76..8d9346ed3 100644 --- a/tests/succeed/format-record/field-refinements.fathom +++ b/tests/succeed/format-record/field-refinements.fathom @@ -1,10 +1,10 @@ let format = { magic <- u64le where u64_eq magic 0x00ffffffffffff00, len <- u8 where u8_lte len 16, - data <- repeat_len8 len u8, + data <- repeat_len64 len u8, }; -let _ : Repr format -> { magic : U64, len : U8, data : Array8 len U8 } = +let _ : Repr format -> { magic : U64, len : U8, data : Array64 len U8 } = fun x => x; {} diff --git a/tests/succeed/format-record/field-refinements.snap b/tests/succeed/format-record/field-refinements.snap index e53127fb2..65595e5e9 100644 --- a/tests/succeed/format-record/field-refinements.snap +++ b/tests/succeed/format-record/field-refinements.snap @@ -2,10 +2,13 @@ stdout = ''' let format : Format = { magic <- u64le where magic == (0xffffffffffff00 : U64), len <- u8 where len <= (16 : U8), - data <- repeat_len8 len u8, + data <- repeat_len64 (u8_extend_u64 len) u8, }; -let _ : Repr format -> { magic : U64, len : U8, data : Array8 len U8 } = -fun x => x; +let _ : Repr format -> { + magic : U64, + len : U8, + data : Array64 (u8_extend_u64 len) U8, +} = fun x => x; () : () ''' stderr = '' diff --git a/tests/succeed/format-repr/primitives.fathom b/tests/succeed/format-repr/primitives.fathom index 4d7029fa8..b0dda42f4 100644 --- a/tests/succeed/format-repr/primitives.fathom +++ b/tests/succeed/format-repr/primitives.fathom @@ -17,16 +17,10 @@ let test_f32le_repr : Repr f32le -> F32 = fun x => x; let test_f64be_repr : Repr f64be -> F64 = fun x => x; let test_f64le_repr : Repr f64le -> F64 = fun x => x; -let test_repeat_len8 : fun n f -> Repr (repeat_len8 n f) -> Array8 n (Repr f) = fun _ => fun _ => fun x => x; -let test_repeat_len16 : fun n f -> Repr (repeat_len16 n f) -> Array16 n (Repr f) = fun _ => fun _ => fun x => x; -let test_repeat_len32 : fun n f -> Repr (repeat_len32 n f) -> Array32 n (Repr f) = fun _ => fun _ => fun x => x; let test_repeat_len64 : fun n f -> Repr (repeat_len64 n f) -> Array64 n (Repr f) = fun _ => fun _ => fun x => x; let test_repeat_until_end : fun f -> Repr (repeat_until_end f) -> Array (Repr f) = fun _ => fun x => x; -let test_limit8 : fun n f -> Repr (limit8 n f) -> Repr f = fun _ => fun _ => fun x => x; -let test_limit16 : fun n f -> Repr (limit16 n f) -> Repr f = fun _ => fun _ => fun x => x; -let test_limit32 : fun n f -> Repr (limit32 n f) -> Repr f = fun _ => fun _ => fun x => x; let test_limit64 : fun n f -> Repr (limit64 n f) -> Repr f = fun _ => fun _ => fun x => x; let test_link : fun pos f -> Repr (link pos f) -> Ref f = fun _ => fun _ => fun x => x; diff --git a/tests/succeed/format-repr/primitives.snap b/tests/succeed/format-repr/primitives.snap index 27f7d8e68..d4c7b1322 100644 --- a/tests/succeed/format-repr/primitives.snap +++ b/tests/succeed/format-repr/primitives.snap @@ -17,22 +17,10 @@ let test_f32be_repr : Repr f32be -> F32 = fun x => x; let test_f32le_repr : Repr f32le -> F32 = fun x => x; let test_f64be_repr : Repr f64be -> F64 = fun x => x; let test_f64le_repr : Repr f64le -> F64 = fun x => x; -let test_repeat_len8 : fun (n : U8) (f : Format) -> Repr (repeat_len8 n f) -> -Array8 n (Repr f) = fun _ _ x => x; -let test_repeat_len16 : fun (n : U16) (f : Format) -> Repr (repeat_len16 n f) -> -Array16 n (Repr f) = fun _ _ x => x; -let test_repeat_len32 : fun (n : U32) (f : Format) -> Repr (repeat_len32 n f) -> -Array32 n (Repr f) = fun _ _ x => x; let test_repeat_len64 : fun (n : U64) (f : Format) -> Repr (repeat_len64 n f) -> Array64 n (Repr f) = fun _ _ x => x; let test_repeat_until_end : fun (f : Format) -> Repr (repeat_until_end f) -> Array (Repr f) = fun _ x => x; -let test_limit8 : fun (n : U8) (f : Format) -> Repr (limit8 n f) -> Repr f = -fun _ _ x => x; -let test_limit16 : fun (n : U16) (f : Format) -> Repr (limit16 n f) -> Repr f = -fun _ _ x => x; -let test_limit32 : fun (n : U32) (f : Format) -> Repr (limit32 n f) -> Repr f = -fun _ _ x => x; let test_limit64 : fun (n : U64) (f : Format) -> Repr (limit64 n f) -> Repr f = fun _ _ x => x; let test_link : fun (pos : Pos) (f : Format) -> Repr (link pos f) -> Ref f = diff --git a/tests/succeed/primitive-ops.fathom b/tests/succeed/primitive-ops.fathom index ad7591992..9bf47df7f 100644 --- a/tests/succeed/primitive-ops.fathom +++ b/tests/succeed/primitive-ops.fathom @@ -1,11 +1,4 @@ -let test : Array8 (u8_add 1 2) {} -> Array8 3 {} = fun x => x; -let test : Array16 (u16_add 1 2) {} -> Array16 3 {} = fun x => x; -let test : Array32 (u32_add 1 2) {} -> Array32 3 {} = fun x => x; let test : Array64 (u64_add 1 2) {} -> Array64 3 {} = fun x => x; - -let test : Array8 (u8_sub 3 1) {} -> Array8 2 {} = fun x => x; -let test : Array16 (u16_sub 3 1) {} -> Array16 2 {} = fun x => x; -let test : Array32 (u32_sub 3 1) {} -> Array32 2 {} = fun x => x; let test : Array64 (u64_sub 3 1) {} -> Array64 2 {} = fun x => x; Type diff --git a/tests/succeed/primitive-ops.snap b/tests/succeed/primitive-ops.snap index d1994c908..4cdcef2d0 100644 --- a/tests/succeed/primitive-ops.snap +++ b/tests/succeed/primitive-ops.snap @@ -1,11 +1,5 @@ stdout = ''' -let test : Array8 ((1 : U8) + (2 : U8)) () -> Array8 3 () = fun x => x; -let test : Array16 ((1 : U16) + (2 : U16)) () -> Array16 3 () = fun x => x; -let test : Array32 ((1 : U32) + (2 : U32)) () -> Array32 3 () = fun x => x; let test : Array64 ((1 : U64) + (2 : U64)) () -> Array64 3 () = fun x => x; -let test : Array8 ((3 : U8) - (1 : U8)) () -> Array8 2 () = fun x => x; -let test : Array16 ((3 : U16) - (1 : U16)) () -> Array16 2 () = fun x => x; -let test : Array32 ((3 : U32) - (1 : U32)) () -> Array32 2 () = fun x => x; let test : Array64 ((3 : U64) - (1 : U64)) () -> Array64 2 () = fun x => x; Type : Type ''' diff --git a/tests/succeed/primitives.fathom b/tests/succeed/primitives.fathom index f81d0d9f6..63b3db604 100644 --- a/tests/succeed/primitives.fathom +++ b/tests/succeed/primitives.fathom @@ -14,9 +14,6 @@ let _ = F32 : Type; let _ = F64 : Type; let _ = Option : Type -> Type; let _ = Array : Type -> Type; -let _ = Array8 : U8 -> Type -> Type; -let _ = Array16 : U16 -> Type -> Type; -let _ = Array32 : U32 -> Type -> Type; let _ = Array64 : U64 -> Type -> Type; let _ = Pos : Type; let _ = Ref : Format -> Type; @@ -51,14 +48,8 @@ let _ = f32be : Format; let _ = f32le : Format; let _ = f64be : Format; let _ = f64le : Format; -let _ = repeat_len8 : U8 -> Format -> Format; -let _ = repeat_len16 : U16 -> Format -> Format; -let _ = repeat_len32 : U32 -> Format -> Format; let _ = repeat_len64 : U64 -> Format -> Format; let _ = repeat_until_end : Format -> Format; -let _ = repeat_len8 : U8 -> Format -> Format; -let _ = repeat_len16 : U16 -> Format -> Format; -let _ = repeat_len32 : U32 -> Format -> Format; let _ = repeat_len64 : U64 -> Format -> Format; let _ = link : Pos -> Format -> Format; let _ = deref : fun (@f : Format) -> Ref f -> Format; @@ -93,6 +84,9 @@ let _ = u8_shr : U8 -> U8 -> U8; let _ = u8_and : U8 -> U8 -> U8; let _ = u8_or : U8 -> U8 -> U8; let _ = u8_xor : U8 -> U8 -> U8; +let _ = u8_extend_u16 : U8 -> U16; +let _ = u8_extend_u32 : U8 -> U32; +let _ = u8_extend_u64 : U8 -> U64; let _ = u16_eq : U16 -> U16 -> Bool; let _ = u16_neq : U16 -> U16 -> Bool; @@ -110,6 +104,8 @@ let _ = u16_shr : U16 -> U8 -> U16; let _ = u16_and : U16 -> U16 -> U16; let _ = u16_or : U16 -> U16 -> U16; let _ = u16_xor : U16 -> U16 -> U16; +let _ = u16_extend_u32 : U16 -> U32; +let _ = u16_extend_u64 : U16 -> U64; let _ = u32_eq : U32 -> U32 -> Bool; let _ = u32_neq : U32 -> U32 -> Bool; @@ -127,6 +123,7 @@ let _ = u32_shr : U32 -> U8 -> U32; let _ = u32_and : U32 -> U32 -> U32; let _ = u32_or : U32 -> U32 -> U32; let _ = u32_xor : U32 -> U32 -> U32; +let _ = u32_extend_u64 : U32 -> U64; let _ = u64_eq : U64 -> U64 -> Bool; let _ = u64_neq : U64 -> U64 -> Bool; @@ -205,14 +202,8 @@ let _ = some : fun (@A : Type) -> A -> Option A; let _ = none : fun (@A : Type) -> Option A; let _ = option_fold : fun (@A : Type) (@B : Type) -> B -> (A -> B) -> Option A -> B; -let _ = array8_find : fun (@len : U8) (@A : Type) -> (A -> Bool) -> Array8 len A -> Option A; -let _ = array16_find : fun (@len : U16) (@A : Type) -> (A -> Bool) -> Array16 len A -> Option A; -let _ = array32_find : fun (@len : U32) (@A : Type) -> (A -> Bool) -> Array32 len A -> Option A; let _ = array64_find : fun (@len : U64) (@A : Type) -> (A -> Bool) -> Array64 len A -> Option A; -let _ = array8_index : fun (@len : U8) (@A : Type) -> U8 -> Array8 len A -> A; -let _ = array16_index : fun (@len : U16) (@A : Type) -> U16 -> Array16 len A -> A; -let _ = array32_index : fun (@len : U32) (@A : Type) -> U32 -> Array32 len A -> A; let _ = array64_index : fun (@len : U64) (@A : Type) -> U64 -> Array64 len A -> A; let _ = pos_add_u8 : Pos -> U8 -> Pos; diff --git a/tests/succeed/primitives.snap b/tests/succeed/primitives.snap index d3d8a8525..5ac2441d6 100644 --- a/tests/succeed/primitives.snap +++ b/tests/succeed/primitives.snap @@ -13,9 +13,6 @@ let _ : Type = F32; let _ : Type = F64; let _ : Type -> Type = Option; let _ : Type -> Type = Array; -let _ : U8 -> Type -> Type = Array8; -let _ : U16 -> Type -> Type = Array16; -let _ : U32 -> Type -> Type = Array32; let _ : U64 -> Type -> Type = Array64; let _ : Type = Pos; let _ : Format -> Type = Ref; @@ -48,14 +45,8 @@ let _ : Format = f32be; let _ : Format = f32le; let _ : Format = f64be; let _ : Format = f64le; -let _ : U8 -> Format -> Format = repeat_len8; -let _ : U16 -> Format -> Format = repeat_len16; -let _ : U32 -> Format -> Format = repeat_len32; let _ : U64 -> Format -> Format = repeat_len64; let _ : Format -> Format = repeat_until_end; -let _ : U8 -> Format -> Format = repeat_len8; -let _ : U16 -> Format -> Format = repeat_len16; -let _ : U32 -> Format -> Format = repeat_len32; let _ : U64 -> Format -> Format = repeat_len64; let _ : Pos -> Format -> Format = link; let _ : fun (@f : Format) -> Ref f -> Format = deref; @@ -87,6 +78,9 @@ let _ : U8 -> U8 -> U8 = u8_shr; let _ : U8 -> U8 -> U8 = u8_and; let _ : U8 -> U8 -> U8 = u8_or; let _ : U8 -> U8 -> U8 = u8_xor; +let _ : U8 -> U16 = u8_extend_u16; +let _ : U8 -> U32 = u8_extend_u32; +let _ : U8 -> U64 = u8_extend_u64; let _ : U16 -> U16 -> Bool = u16_eq; let _ : U16 -> U16 -> Bool = u16_neq; let _ : U16 -> U16 -> Bool = u16_gt; @@ -103,6 +97,8 @@ let _ : U16 -> U8 -> U16 = u16_shr; let _ : U16 -> U16 -> U16 = u16_and; let _ : U16 -> U16 -> U16 = u16_or; let _ : U16 -> U16 -> U16 = u16_xor; +let _ : U16 -> U32 = u16_extend_u32; +let _ : U16 -> U64 = u16_extend_u64; let _ : U32 -> U32 -> Bool = u32_eq; let _ : U32 -> U32 -> Bool = u32_neq; let _ : U32 -> U32 -> Bool = u32_gt; @@ -119,6 +115,7 @@ let _ : U32 -> U8 -> U32 = u32_shr; let _ : U32 -> U32 -> U32 = u32_and; let _ : U32 -> U32 -> U32 = u32_or; let _ : U32 -> U32 -> U32 = u32_xor; +let _ : U32 -> U64 = u32_extend_u64; let _ : U64 -> U64 -> Bool = u64_eq; let _ : U64 -> U64 -> Bool = u64_neq; let _ : U64 -> U64 -> Bool = u64_gt; @@ -191,19 +188,8 @@ let _ : fun (@A : Type) -> A -> Option A = some; let _ : fun (@A : Type) -> Option A = none; let _ : fun (@A : Type) (@B : Type) -> B -> (A -> B) -> Option A -> B = option_fold; -let _ : fun (@len : U8) (@A : Type) -> (A -> Bool) -> Array8 len A -> Option A = -array8_find; -let _ : fun (@len : U16) (@A : Type) -> (A -> Bool) -> Array16 len A -> -Option A = array16_find; -let _ : fun (@len : U32) (@A : Type) -> (A -> Bool) -> Array32 len A -> -Option A = array32_find; let _ : fun (@len : U64) (@A : Type) -> (A -> Bool) -> Array64 len A -> Option A = array64_find; -let _ : fun (@len : U8) (@A : Type) -> U8 -> Array8 len A -> A = array8_index; -let _ : fun (@len : U16) (@A : Type) -> U16 -> Array16 len A -> A = -array16_index; -let _ : fun (@len : U32) (@A : Type) -> U32 -> Array32 len A -> A = -array32_index; let _ : fun (@len : U64) (@A : Type) -> U64 -> Array64 len A -> A = array64_index; let _ : Pos -> U8 -> Pos = pos_add_u8;