From 6da000f63cfcc22691771fbd9ee2da6d1d2a7f8d Mon Sep 17 00:00:00 2001 From: Wesley Moore Date: Thu, 25 Aug 2022 10:23:33 +1000 Subject: [PATCH 1/7] Add or_succeed primitive --- fathom/src/core.rs | 2 ++ fathom/src/core/binary.rs | 15 +++++++++++++++ fathom/src/core/semantics.rs | 1 + fathom/src/surface/elaboration.rs | 19 +++++++++++++++++++ tests/succeed/primitives.fathom | 1 + tests/succeed/primitives.snap | 1 + 6 files changed, 39 insertions(+) diff --git a/fathom/src/core.rs b/fathom/src/core.rs index 774d7e90e..bb9664959 100644 --- a/fathom/src/core.rs +++ b/fathom/src/core.rs @@ -390,6 +390,8 @@ def_prims! { FormatDeref => "deref", /// A format that always succeeds with some data. FormatSucceed => "succeed", + /// A format that always succeeds with a default value if a supplied condition is false. + FormatOrSucceed => "or_succeed", /// A format that always fails to parse. FormatFail => "fail", /// Unwrap an option, or fail to parse. diff --git a/fathom/src/core/binary.rs b/fathom/src/core/binary.rs index 7e2881d38..2e8216ee1 100644 --- a/fathom/src/core/binary.rs +++ b/fathom/src/core/binary.rs @@ -424,6 +424,7 @@ impl<'arena, 'env, 'data> Context<'arena, 'env, 'data> { (Prim::FormatDeref, [FunApp(format), FunApp(r#ref)]) => self.read_deref(format, r#ref), (Prim::FormatStreamPos, []) => read_stream_pos(reader, span), (Prim::FormatSucceed, [_, FunApp(elem)]) => Ok(elem.clone()), + (Prim::FormatOrSucceed, [FunApp(cond), FunApp(format), FunApp(default)]) => self.read_or_succeed(reader, cond, format, default), (Prim::FormatFail, []) => Err(ReadError::ReadFailFormat(span)), (Prim::FormatUnwrap, [_, FunApp(option)]) => match option.match_prim_spine() { Some((Prim::OptionSome, [FunApp(elem)])) => Ok(elem.clone()), @@ -540,6 +541,20 @@ impl<'arena, 'env, 'data> Context<'arena, 'env, 'data> { self.lookup_or_read_ref(pos, format) } + fn read_or_succeed( + &mut self, + reader: &mut BufferReader<'data>, + cond: &ArcValue<'arena>, + format: &ArcValue<'arena>, + default: &ArcValue<'arena>, + ) -> Result, ReadError<'arena>> { + match cond.as_ref() { + Value::ConstLit(Const::Bool(true)) => self.read_format(reader, format), + Value::ConstLit(Const::Bool(false)) => Ok(default.clone()), + _ => Err(ReadError::InvalidValue(Span::Empty)), + } + } + fn lookup_ref<'context>( &'context self, pos: usize, diff --git a/fathom/src/core/semantics.rs b/fathom/src/core/semantics.rs index ddd828d8c..970a30bc4 100644 --- a/fathom/src/core/semantics.rs +++ b/fathom/src/core/semantics.rs @@ -860,6 +860,7 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> { (Prim::FormatDeref, [Elim::FunApp(elem), _]) => return self.format_repr(elem), (Prim::FormatStreamPos, []) => Value::prim(Prim::PosType, []), (Prim::FormatSucceed, [Elim::FunApp(elem), _]) => return elem.clone(), + (Prim::FormatOrSucceed, [_, Elim::FunApp(elem), _]) => return self.format_repr(elem), (Prim::FormatFail, []) => Value::prim(Prim::VoidType, []), (Prim::FormatUnwrap, [Elim::FunApp(elem), _]) => return elem.clone(), (Prim::ReportedError, []) => Value::prim(Prim::ReportedError, []), diff --git a/fathom/src/surface/elaboration.rs b/fathom/src/surface/elaboration.rs index 498ac1194..1810b16a3 100644 --- a/fathom/src/surface/elaboration.rs +++ b/fathom/src/surface/elaboration.rs @@ -216,6 +216,25 @@ impl<'arena> RigidEnv<'arena> { &Term::FunType(Span::Empty, None, &VAR0, &FORMAT_TYPE), ), ); + env.define_prim( + FormatOrSucceed, + scope.to_scope(Term::FunType( + Span::Empty, + env.name("cond"), + &BOOL_TYPE, + scope.to_scope(Term::FunType( + Span::Empty, + env.name("A"), + &FORMAT_TYPE, + &Term::FunType( + Span::Empty, + None, + &Term::FunApp(Span::Empty, &Term::Prim(Span::Empty, FormatRepr), &VAR0), + &FORMAT_TYPE, + ), + )), + )), + ); env.define_prim(FormatFail, &FORMAT_TYPE); env.define_prim( FormatUnwrap, diff --git a/tests/succeed/primitives.fathom b/tests/succeed/primitives.fathom index 4621458fa..add374949 100644 --- a/tests/succeed/primitives.fathom +++ b/tests/succeed/primitives.fathom @@ -64,6 +64,7 @@ let _ = link : Pos -> Format -> Format; let _ = deref : fun (f : Format) -> Ref f -> Format; let _ = stream_pos : Format; let _ = succeed : fun (Elem : Type) -> Elem -> Format; +let _ = or_succeed : Bool -> fun (A : Format) -> Repr A -> Format; let _ = fail : Format; let _ = unwrap : fun (A : Type) -> Option A -> Format; let _ = Repr : Format -> Type; diff --git a/tests/succeed/primitives.snap b/tests/succeed/primitives.snap index d5c8841cf..62df3424e 100644 --- a/tests/succeed/primitives.snap +++ b/tests/succeed/primitives.snap @@ -61,6 +61,7 @@ let _ : _ = link; let _ : _ = deref; let _ : _ = stream_pos; let _ : _ = succeed; +let _ : _ = or_succeed; let _ : _ = fail; let _ : _ = unwrap; let _ : _ = Repr; From c39210571c266d1099e8c61e0c23c977b5fc940f Mon Sep 17 00:00:00 2001 From: Wesley Moore Date: Thu, 25 Aug 2022 15:21:14 +1000 Subject: [PATCH 2/7] Add read_repeat_until_full primitive --- fathom/src/core.rs | 5 ++++ fathom/src/core/binary.rs | 45 +++++++++++++++++++++++++++++++ fathom/src/core/semantics.rs | 8 +++++- fathom/src/surface/elaboration.rs | 30 +++++++++++++++++++++ tests/succeed/primitives.fathom | 2 ++ 5 files changed, 89 insertions(+), 1 deletion(-) diff --git a/fathom/src/core.rs b/fathom/src/core.rs index bb9664959..a3b863db1 100644 --- a/fathom/src/core.rs +++ b/fathom/src/core.rs @@ -373,6 +373,10 @@ def_prims! { FormatArray64 => "array64", /// Repeat a format until the length of the given parse scope is reached. FormatRepeatUntilEnd => "repeat_until_end", + /// Repeat a format until the array is filled. + /// + /// The value read by the format is replicated according to a supplied function. + FormatRepeatUntilFull => "repeat_until_full", /// Limit the format to an unsigned 8-bit byte length. FormatLimit8 => "limit8", /// Limit the format to an unsigned 16-bit byte length. @@ -442,6 +446,7 @@ def_prims! { U16And => "u16_and", U16Or => "u16_or", U16Xor => "u16_xor", + U16FromU8 => "u16_from_u8", U32Eq => "u32_eq", U32Neq => "u32_neq", diff --git a/fathom/src/core/binary.rs b/fathom/src/core/binary.rs index 2e8216ee1..179d6bc00 100644 --- a/fathom/src/core/binary.rs +++ b/fathom/src/core/binary.rs @@ -416,6 +416,7 @@ impl<'arena, 'env, 'data> Context<'arena, 'env, 'data> { (Prim::FormatArray32, [FunApp(len), FunApp(format)]) => self.read_array(reader, span, len, format), (Prim::FormatArray64, [FunApp(len), FunApp(format)]) => self.read_array(reader, span, len, format), (Prim::FormatRepeatUntilEnd, [FunApp(format)]) => self.read_repeat_until_end(reader, format), + (Prim::FormatRepeatUntilFull, [FunApp(len), FunApp(format), FunApp(replicate)]) => self.read_repeat_until_full(reader, len, replicate, format), (Prim::FormatLimit8, [FunApp(limit), FunApp(format)]) => self.read_limit(reader, limit, format), (Prim::FormatLimit16, [FunApp(limit), FunApp(format)]) => self.read_limit(reader, limit, format), (Prim::FormatLimit32, [FunApp(limit), FunApp(format)]) => self.read_limit(reader, limit, format), @@ -485,6 +486,50 @@ impl<'arena, 'env, 'data> Context<'arena, 'env, 'data> { } } + fn read_repeat_until_full( + &mut self, + reader: &mut BufferReader<'data>, + len: &ArcValue<'arena>, + replicate: &ArcValue<'arena>, + elem_format: &ArcValue<'arena>, + ) -> Result, ReadError<'arena>> { + let len = match self.elim_env().force(len).as_ref() { + Value::ConstLit(Const::U8(len, _)) => Some(usize::from(*len)), + Value::ConstLit(Const::U16(len, _)) => Some(usize::from(*len)), + Value::ConstLit(Const::U32(len, _)) => usize::try_from(*len).ok(), + Value::ConstLit(Const::U64(len, _)) => usize::try_from(*len).ok(), + _ => return Err(ReadError::InvalidValue(len.span())), + } + .ok_or_else(|| ReadError::InvalidValue(len.span()))?; + + // TODO: Do we need to force replicate as well? + // let replicate = self.elim_env().force(replicate); + + let mut elems = Vec::with_capacity(len); + while elems.len() < len { + match self.read_format(reader, elem_format) { + Ok(elem) => { + // Call the function to determine how many items this represents + let closure_res = self.elim_env().fun_app(replicate.clone(), elem.clone()); + let repeat = match closure_res.as_ref() { + Value::ConstLit(Const::U16(n, _)) => *n, + _ => return Err(ReadError::InvalidValue(replicate.span())), + }; + + // Push it that many times onto the array + // TODO: Error/limit if this exceeds len? + elems.extend(std::iter::repeat(elem).take(usize::from(repeat))); + } + Err(err) => return Err(err), + }; + } + + Ok(Spanned::new( + elem_format.span(), + Arc::new(Value::ArrayLit(elems)), + )) + } + fn read_limit( &mut self, reader: &BufferReader<'data>, diff --git a/fathom/src/core/semantics.rs b/fathom/src/core/semantics.rs index 970a30bc4..dbc49308a 100644 --- a/fathom/src/core/semantics.rs +++ b/fathom/src/core/semantics.rs @@ -475,6 +475,7 @@ fn prim_step(prim: Prim) -> PrimStep { 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::U16FromU8 => const_step!([x, xst: U8] => Const::U16(u16::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)), @@ -854,13 +855,18 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> { (Prim::FormatRepeatUntilEnd, [Elim::FunApp(elem)]) => { Value::prim(Prim::ArrayType, [self.format_repr(elem)]) } + (Prim::FormatRepeatUntilFull, [Elim::FunApp(len), Elim::FunApp(elem), _]) => { + Value::prim(Prim::Array16Type, [len.clone(), self.format_repr(elem)]) + } (Prim::FormatLink, [_, Elim::FunApp(elem)]) => { Value::prim(Prim::RefType, [elem.clone()]) } (Prim::FormatDeref, [Elim::FunApp(elem), _]) => return self.format_repr(elem), (Prim::FormatStreamPos, []) => Value::prim(Prim::PosType, []), (Prim::FormatSucceed, [Elim::FunApp(elem), _]) => return elem.clone(), - (Prim::FormatOrSucceed, [_, Elim::FunApp(elem), _]) => return self.format_repr(elem), + (Prim::FormatOrSucceed, [_, Elim::FunApp(elem), _]) => { + return self.format_repr(elem) + } (Prim::FormatFail, []) => Value::prim(Prim::VoidType, []), (Prim::FormatUnwrap, [Elim::FunApp(elem), _]) => return elem.clone(), (Prim::ReportedError, []) => Value::prim(Prim::ReportedError, []), diff --git a/fathom/src/surface/elaboration.rs b/fathom/src/surface/elaboration.rs index 1810b16a3..db2d5820e 100644 --- a/fathom/src/surface/elaboration.rs +++ b/fathom/src/surface/elaboration.rs @@ -187,6 +187,35 @@ impl<'arena> RigidEnv<'arena> { env.define_prim_fun(FormatArray32, [&U32_TYPE, &FORMAT_TYPE], &FORMAT_TYPE); env.define_prim_fun(FormatArray64, [&U64_TYPE, &FORMAT_TYPE], &FORMAT_TYPE); env.define_prim_fun(FormatRepeatUntilEnd, [&FORMAT_TYPE], &FORMAT_TYPE); + // repeat_until_full16 : U16 -> fun (A : Format) -> (Repr A -> U16) -> Format + env.define_prim( + FormatRepeatUntilFull, + scope.to_scope(core::Term::FunType( + Span::Empty, + None, + &U16_TYPE, + scope.to_scope(core::Term::FunType( + Span::Empty, + env.name("A"), + &FORMAT_TYPE, + scope.to_scope(core::Term::FunType( + Span::Empty, + None, + scope.to_scope(Term::FunType( + Span::Empty, + None, + scope.to_scope(Term::FunApp( + Span::Empty, + &Term::Prim(Span::Empty, FormatRepr), + &VAR0, + )), + &U16_TYPE, + )), + &FORMAT_TYPE, + )), + )), + )), + ); env.define_prim_fun(FormatLimit8, [&U8_TYPE, &FORMAT_TYPE], &FORMAT_TYPE); env.define_prim_fun(FormatLimit16, [&U16_TYPE, &FORMAT_TYPE], &FORMAT_TYPE); env.define_prim_fun(FormatLimit32, [&U32_TYPE, &FORMAT_TYPE], &FORMAT_TYPE); @@ -294,6 +323,7 @@ impl<'arena> RigidEnv<'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(U16FromU8, [&U8_TYPE], &U16_TYPE); env.define_prim_fun(U32Eq, [&U32_TYPE, &U32_TYPE], &BOOL_TYPE); env.define_prim_fun(U32Neq, [&U32_TYPE, &U32_TYPE], &BOOL_TYPE); diff --git a/tests/succeed/primitives.fathom b/tests/succeed/primitives.fathom index add374949..f05f1943f 100644 --- a/tests/succeed/primitives.fathom +++ b/tests/succeed/primitives.fathom @@ -56,6 +56,7 @@ let _ = array16 : U16 -> Format -> Format; let _ = array32 : U32 -> Format -> Format; let _ = array64 : U64 -> Format -> Format; let _ = repeat_until_end : Format -> Format; +let _ = repeat_until_full : U16 -> fun (A : Format) -> (Repr A -> U16) -> Format; let _ = array8 : U8 -> Format -> Format; let _ = array16 : U16 -> Format -> Format; let _ = array32 : U32 -> Format -> Format; @@ -109,6 +110,7 @@ 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_from_u8 : U8 -> U16; let _ = u32_eq : U32 -> U32 -> Bool; let _ = u32_neq : U32 -> U32 -> Bool; From 0f3c9b7133562de3a05765b240824ff3bdd47194 Mon Sep 17 00:00:00 2001 From: Wesley Moore Date: Wed, 31 Aug 2022 16:08:16 +1000 Subject: [PATCH 3/7] Add array16_map primitive --- fathom/src/core.rs | 2 ++ fathom/src/core/binary.rs | 25 +++++++++++++++++++++++ fathom/src/core/semantics.rs | 3 +++ fathom/src/surface/elaboration.rs | 33 +++++++++++++++++++++++++++++++ tests/succeed/primitives.fathom | 1 + 5 files changed, 64 insertions(+) diff --git a/fathom/src/core.rs b/fathom/src/core.rs index a3b863db1..ca517add7 100644 --- a/fathom/src/core.rs +++ b/fathom/src/core.rs @@ -367,6 +367,8 @@ def_prims! { FormatArray8 => "array8", /// Array formats, with unsigned 16-bit indices. FormatArray16 => "array16", + /// Map a function over an Array16 + FormatArray16Map => "array16_map", /// Array formats, with unsigned 32-bit indices. FormatArray32 => "array32", /// Array formats, with unsigned 64-bit indices. diff --git a/fathom/src/core/binary.rs b/fathom/src/core/binary.rs index 179d6bc00..db05246bb 100644 --- a/fathom/src/core/binary.rs +++ b/fathom/src/core/binary.rs @@ -415,6 +415,7 @@ impl<'arena, 'env, 'data> Context<'arena, 'env, 'data> { (Prim::FormatArray16, [FunApp(len), FunApp(format)]) => self.read_array(reader, span, len, format), (Prim::FormatArray32, [FunApp(len), FunApp(format)]) => self.read_array(reader, span, len, format), (Prim::FormatArray64, [FunApp(len), FunApp(format)]) => self.read_array(reader, span, len, format), + (Prim::FormatArray16Map, [_, _, FunApp(map_fn), FunApp(array)]) => self.array_map(reader, span, map_fn, array), (Prim::FormatRepeatUntilEnd, [FunApp(format)]) => self.read_repeat_until_end(reader, format), (Prim::FormatRepeatUntilFull, [FunApp(len), FunApp(format), FunApp(replicate)]) => self.read_repeat_until_full(reader, len, replicate, format), (Prim::FormatLimit8, [FunApp(limit), FunApp(format)]) => self.read_limit(reader, limit, format), @@ -458,6 +459,30 @@ impl<'arena, 'env, 'data> Context<'arena, 'env, 'data> { Ok(Spanned::new(span, Arc::new(Value::ArrayLit(elem_exprs)))) } + fn array_map( + &mut self, + reader: &mut BufferReader<'data>, + span: Span, + map_fn: &ArcValue<'arena>, + array: &ArcValue<'arena>, + ) -> Result, ReadError<'arena>> { + let array = self.elim_env().force(array); + let array = match array.as_ref() { + Value::ArrayLit(ary) => ary, + _ => return Err(ReadError::InvalidValue(array.span())), + }; + + let elem_exprs = array + .iter() + .map(|elem| { + let elem_format = self.elim_env().fun_app(map_fn.clone(), elem.clone()); + self.read_format(reader, &elem_format) + }) + .collect::>()?; + + Ok(Spanned::new(span, Arc::new(Value::ArrayLit(elem_exprs)))) + } + fn read_repeat_until_end( &mut self, reader: &mut BufferReader<'data>, diff --git a/fathom/src/core/semantics.rs b/fathom/src/core/semantics.rs index dbc49308a..9a5cb3241 100644 --- a/fathom/src/core/semantics.rs +++ b/fathom/src/core/semantics.rs @@ -842,6 +842,9 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> { (Prim::FormatArray16, [Elim::FunApp(len), Elim::FunApp(elem)]) => { Value::prim(Prim::Array16Type, [len.clone(), self.format_repr(elem)]) } + (Prim::FormatArray16Map, [Elim::FunApp(len), _, Elim::FunApp(map_fn), _]) => { + Value::prim(Prim::Array16Type, [len.clone(), self.format_repr(map_fn)]) + } (Prim::FormatArray32, [Elim::FunApp(len), Elim::FunApp(elem)]) => { Value::prim(Prim::Array32Type, [len.clone(), self.format_repr(elem)]) } diff --git a/fathom/src/surface/elaboration.rs b/fathom/src/surface/elaboration.rs index db2d5820e..afff65b0e 100644 --- a/fathom/src/surface/elaboration.rs +++ b/fathom/src/surface/elaboration.rs @@ -186,6 +186,39 @@ impl<'arena> RigidEnv<'arena> { env.define_prim_fun(FormatArray16, [&U16_TYPE, &FORMAT_TYPE], &FORMAT_TYPE); env.define_prim_fun(FormatArray32, [&U32_TYPE, &FORMAT_TYPE], &FORMAT_TYPE); env.define_prim_fun(FormatArray64, [&U64_TYPE, &FORMAT_TYPE], &FORMAT_TYPE); + // (A@0 -> Format) + let map_fn = Term::FunType(Span::Empty, None, &VAR0, &FORMAT_TYPE); + // Array16 len@2 A@1 + let array_ty = Term::FunApp( + Span::Empty, + scope.to_scope(Term::FunApp(Span::Empty, &ARRAY16_TYPE, &VAR2)), + &VAR1, + ); + // array16_map : fun (len : U16) -> fun (A : Type) -> (A -> Format) -> Array16 len A -> Format; + env.define_prim( + FormatArray16Map, + scope.to_scope(Term::FunType( + Span::Empty, + env.name("len"), + &U16_TYPE, + scope.to_scope(Term::FunType( + Span::Empty, + env.name("A"), + &UNIVERSE, + scope.to_scope(Term::FunType( + Span::Empty, + None, + scope.to_scope(map_fn), + scope.to_scope(Term::FunType( + Span::Empty, + None, + scope.to_scope(array_ty), + &FORMAT_TYPE, + )), + )), + )), + )), + ); env.define_prim_fun(FormatRepeatUntilEnd, [&FORMAT_TYPE], &FORMAT_TYPE); // repeat_until_full16 : U16 -> fun (A : Format) -> (Repr A -> U16) -> Format env.define_prim( diff --git a/tests/succeed/primitives.fathom b/tests/succeed/primitives.fathom index f05f1943f..8f390076b 100644 --- a/tests/succeed/primitives.fathom +++ b/tests/succeed/primitives.fathom @@ -61,6 +61,7 @@ let _ = array8 : U8 -> Format -> Format; let _ = array16 : U16 -> Format -> Format; let _ = array32 : U32 -> Format -> Format; let _ = array64 : U64 -> Format -> Format; +let _ = array16_map : fun (len : U16) -> fun (A : Type) -> (A -> Format) -> Array16 len A -> Format; let _ = link : Pos -> Format -> Format; let _ = deref : fun (f : Format) -> Ref f -> Format; let _ = stream_pos : Format; From cc28bd2b441b18cc73cab27d8daabaedb9eb308c Mon Sep 17 00:00:00 2001 From: Wesley Moore Date: Wed, 31 Aug 2022 16:44:28 +1000 Subject: [PATCH 4/7] Add array{8,32,64}_map --- fathom/src/core.rs | 10 +++++++-- fathom/src/core/binary.rs | 3 +++ fathom/src/core/semantics.rs | 15 ++++++++++--- fathom/src/surface/elaboration.rs | 37 +++++++++++++++++++------------ tests/succeed/primitives.fathom | 3 +++ 5 files changed, 49 insertions(+), 19 deletions(-) diff --git a/fathom/src/core.rs b/fathom/src/core.rs index ca517add7..44e719fb7 100644 --- a/fathom/src/core.rs +++ b/fathom/src/core.rs @@ -367,12 +367,18 @@ def_prims! { FormatArray8 => "array8", /// Array formats, with unsigned 16-bit indices. FormatArray16 => "array16", - /// Map a function over an Array16 - FormatArray16Map => "array16_map", /// Array formats, with unsigned 32-bit indices. FormatArray32 => "array32", /// Array formats, with unsigned 64-bit indices. FormatArray64 => "array64", + /// Map a function over an Array8 + FormatArray8Map => "array8_map", + /// Map a function over an Array16 + FormatArray16Map => "array16_map", + /// Map a function over an Array32 + FormatArray32Map => "array32_map", + /// Map a function over an Array64 + FormatArray64Map => "array64_map", /// Repeat a format until the length of the given parse scope is reached. FormatRepeatUntilEnd => "repeat_until_end", /// Repeat a format until the array is filled. diff --git a/fathom/src/core/binary.rs b/fathom/src/core/binary.rs index db05246bb..6a1461c47 100644 --- a/fathom/src/core/binary.rs +++ b/fathom/src/core/binary.rs @@ -415,7 +415,10 @@ impl<'arena, 'env, 'data> Context<'arena, 'env, 'data> { (Prim::FormatArray16, [FunApp(len), FunApp(format)]) => self.read_array(reader, span, len, format), (Prim::FormatArray32, [FunApp(len), FunApp(format)]) => self.read_array(reader, span, len, format), (Prim::FormatArray64, [FunApp(len), FunApp(format)]) => self.read_array(reader, span, len, format), + (Prim::FormatArray8Map, [_, _, FunApp(map_fn), FunApp(array)]) => self.array_map(reader, span, map_fn, array), (Prim::FormatArray16Map, [_, _, FunApp(map_fn), FunApp(array)]) => self.array_map(reader, span, map_fn, array), + (Prim::FormatArray32Map, [_, _, FunApp(map_fn), FunApp(array)]) => self.array_map(reader, span, map_fn, array), + (Prim::FormatArray64Map, [_, _, FunApp(map_fn), FunApp(array)]) => self.array_map(reader, span, map_fn, array), (Prim::FormatRepeatUntilEnd, [FunApp(format)]) => self.read_repeat_until_end(reader, format), (Prim::FormatRepeatUntilFull, [FunApp(len), FunApp(format), FunApp(replicate)]) => self.read_repeat_until_full(reader, len, replicate, format), (Prim::FormatLimit8, [FunApp(limit), FunApp(format)]) => self.read_limit(reader, limit, format), diff --git a/fathom/src/core/semantics.rs b/fathom/src/core/semantics.rs index 9a5cb3241..968fb37f7 100644 --- a/fathom/src/core/semantics.rs +++ b/fathom/src/core/semantics.rs @@ -842,15 +842,24 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> { (Prim::FormatArray16, [Elim::FunApp(len), Elim::FunApp(elem)]) => { Value::prim(Prim::Array16Type, [len.clone(), self.format_repr(elem)]) } - (Prim::FormatArray16Map, [Elim::FunApp(len), _, Elim::FunApp(map_fn), _]) => { - Value::prim(Prim::Array16Type, [len.clone(), self.format_repr(map_fn)]) - } (Prim::FormatArray32, [Elim::FunApp(len), Elim::FunApp(elem)]) => { Value::prim(Prim::Array32Type, [len.clone(), self.format_repr(elem)]) } (Prim::FormatArray64, [Elim::FunApp(len), Elim::FunApp(elem)]) => { Value::prim(Prim::Array64Type, [len.clone(), self.format_repr(elem)]) } + (Prim::FormatArray8Map, [Elim::FunApp(len), _, Elim::FunApp(map_fn), _]) => { + Value::prim(Prim::Array8Type, [len.clone(), self.format_repr(map_fn)]) + } + (Prim::FormatArray16Map, [Elim::FunApp(len), _, Elim::FunApp(map_fn), _]) => { + Value::prim(Prim::Array16Type, [len.clone(), self.format_repr(map_fn)]) + } + (Prim::FormatArray32Map, [Elim::FunApp(len), _, Elim::FunApp(map_fn), _]) => { + Value::prim(Prim::Array32Type, [len.clone(), self.format_repr(map_fn)]) + } + (Prim::FormatArray64Map, [Elim::FunApp(len), _, Elim::FunApp(map_fn), _]) => { + Value::prim(Prim::Array64Type, [len.clone(), self.format_repr(map_fn)]) + } (Prim::FormatLimit8, [_, Elim::FunApp(elem)]) => return self.format_repr(elem), (Prim::FormatLimit16, [_, Elim::FunApp(elem)]) => return self.format_repr(elem), (Prim::FormatLimit32, [_, Elim::FunApp(elem)]) => return self.format_repr(elem), diff --git a/fathom/src/surface/elaboration.rs b/fathom/src/surface/elaboration.rs index afff65b0e..1854bddda 100644 --- a/fathom/src/surface/elaboration.rs +++ b/fathom/src/surface/elaboration.rs @@ -186,21 +186,20 @@ impl<'arena> RigidEnv<'arena> { env.define_prim_fun(FormatArray16, [&U16_TYPE, &FORMAT_TYPE], &FORMAT_TYPE); env.define_prim_fun(FormatArray32, [&U32_TYPE, &FORMAT_TYPE], &FORMAT_TYPE); env.define_prim_fun(FormatArray64, [&U64_TYPE, &FORMAT_TYPE], &FORMAT_TYPE); - // (A@0 -> Format) - let map_fn = Term::FunType(Span::Empty, None, &VAR0, &FORMAT_TYPE); - // Array16 len@2 A@1 - let array_ty = Term::FunApp( - Span::Empty, - scope.to_scope(Term::FunApp(Span::Empty, &ARRAY16_TYPE, &VAR2)), - &VAR1, - ); - // array16_map : fun (len : U16) -> fun (A : Type) -> (A -> Format) -> Array16 len A -> Format; - env.define_prim( - FormatArray16Map, + let format_array_map = |index_type, array_type| { + // (A@0 -> Format) + let map_fn = Term::FunType(Span::Empty, None, &VAR0, &FORMAT_TYPE); + // Array16 len@2 A@1 + let array_ty = Term::FunApp( + Span::Empty, + scope.to_scope(Term::FunApp(Span::Empty, array_type, &VAR2)), + &VAR1, + ); + // array16_map : fun (len : U16) -> fun (A : Type) -> (A -> Format) -> Array16 len A -> Format; scope.to_scope(Term::FunType( Span::Empty, env.name("len"), - &U16_TYPE, + index_type, scope.to_scope(Term::FunType( Span::Empty, env.name("A"), @@ -217,9 +216,19 @@ impl<'arena> RigidEnv<'arena> { )), )), )), - )), - ); + )) + }; + + let format_array8_map = format_array_map(&U8_TYPE, &ARRAY8_TYPE); + let format_array16_map = format_array_map(&U16_TYPE, &ARRAY16_TYPE); + let format_array32_map = format_array_map(&U32_TYPE, &ARRAY32_TYPE); + let format_array64_map = format_array_map(&U64_TYPE, &ARRAY64_TYPE); + env.define_prim(FormatArray8Map, format_array8_map); + env.define_prim(FormatArray16Map, format_array16_map); + env.define_prim(FormatArray32Map, format_array32_map); + env.define_prim(FormatArray64Map, format_array64_map); env.define_prim_fun(FormatRepeatUntilEnd, [&FORMAT_TYPE], &FORMAT_TYPE); + // repeat_until_full16 : U16 -> fun (A : Format) -> (Repr A -> U16) -> Format env.define_prim( FormatRepeatUntilFull, diff --git a/tests/succeed/primitives.fathom b/tests/succeed/primitives.fathom index 8f390076b..ff759c456 100644 --- a/tests/succeed/primitives.fathom +++ b/tests/succeed/primitives.fathom @@ -61,7 +61,10 @@ let _ = array8 : U8 -> Format -> Format; let _ = array16 : U16 -> Format -> Format; let _ = array32 : U32 -> Format -> Format; let _ = array64 : U64 -> Format -> Format; +let _ = array8_map : fun (len : U8) -> fun (A : Type) -> (A -> Format) -> Array8 len A -> Format; let _ = array16_map : fun (len : U16) -> fun (A : Type) -> (A -> Format) -> Array16 len A -> Format; +let _ = array32_map : fun (len : U32) -> fun (A : Type) -> (A -> Format) -> Array32 len A -> Format; +let _ = array64_map : fun (len : U64) -> fun (A : Type) -> (A -> Format) -> Array64 len A -> Format; let _ = link : Pos -> Format -> Format; let _ = deref : fun (f : Format) -> Ref f -> Format; let _ = stream_pos : Format; From 927cb7fbbb66eef2dccf818c15d89acf5a122273 Mon Sep 17 00:00:00 2001 From: Wesley Moore Date: Thu, 1 Sep 2022 10:23:51 +1000 Subject: [PATCH 5/7] Update OpenType description to read simple glyph coordinates --- formats/data/opentype/woff/valid-005.snap | 109 +++++++++++++++++++++- formats/opentype.fathom | 67 +++++++++---- formats/opentype.snap | 39 +++++++- tests/succeed/primitives.snap | 6 ++ 4 files changed, 197 insertions(+), 24 deletions(-) diff --git a/formats/data/opentype/woff/valid-005.snap b/formats/data/opentype/woff/valid-005.snap index 20726588d..162dd2d11 100644 --- a/formats/data/opentype/woff/valid-005.snap +++ b/formats/data/opentype/woff/valid-005.snap @@ -756,8 +756,115 @@ stdout = ''' end_pts_of_contours = [ 7, 17, 23, 27, 30 ], instruction_length = 0, instructions = [], - last_end_point_index = 30, number_of_coords = 31, + flags = [ + { flag = 33, repeat = 0 }, + { flag = 1, repeat = 0 }, + { flag = 33, repeat = 0 }, + { flag = 1, repeat = 0 }, + { flag = 33, repeat = 0 }, + { flag = 39, repeat = 0 }, + { flag = 33, repeat = 0 }, + { flag = 7, repeat = 0 }, + { flag = 1, repeat = 0 }, + { flag = 33, repeat = 0 }, + { flag = 17, repeat = 0 }, + { flag = 33, repeat = 0 }, + { flag = 17, repeat = 0 }, + { flag = 33, repeat = 0 }, + { flag = 17, repeat = 0 }, + { flag = 33, repeat = 0 }, + { flag = 17, repeat = 0 }, + { flag = 33, repeat = 0 }, + { flag = 1, repeat = 0 }, + { flag = 33, repeat = 0 }, + { flag = 17, repeat = 0 }, + { flag = 33, repeat = 0 }, + { flag = 17, repeat = 0 }, + { flag = 33, repeat = 0 }, + { flag = 1, repeat = 0 }, + { flag = 33, repeat = 0 }, + { flag = 17, repeat = 0 }, + { flag = 33, repeat = 0 }, + { flag = 1, repeat = 0 }, + { flag = 51, repeat = 0 }, + { flag = 3, repeat = 0 }, + ], + read_coord = fun is_short => fun is_same => fun f => { + coord <- match (is_short f) { + false => match (is_same f) { + false => s16be, + true => succeed S16 0, + }, + true => u8, + }, + }, + x_coordinates = [ + { coord = 1182 }, + { coord = 436 }, + { coord = 606 }, + { coord = 436 }, + { coord = -503 }, + { coord = 66 }, + { coord = -416 }, + { coord = 63 }, + { coord = -1407 }, + { coord = 1073 }, + { coord = 0 }, + { coord = -588 }, + { coord = 0 }, + { coord = 502 }, + { coord = 0 }, + { coord = -502 }, + { coord = 0 }, + { coord = -485 }, + { coord = 3248 }, + { coord = 485 }, + { coord = 0 }, + { coord = 576 }, + { coord = 0 }, + { coord = -1061 }, + { coord = -680 }, + { coord = 485 }, + { coord = 0 }, + { coord = -485 }, + { coord = -1012 }, + { coord = 246 }, + { coord = 123 }, + ], + y_coordinates = [ + { coord = 0 }, + { coord = 1434 }, + { coord = 0 }, + { coord = -1434 }, + { coord = 0 }, + { coord = 244 }, + { coord = 0 }, + { coord = 244 }, + { coord = 1434 }, + { coord = 0 }, + { coord = -336 }, + { coord = 0 }, + { coord = -267 }, + { coord = 0 }, + { coord = -331 }, + { coord = 0 }, + { coord = -500 }, + { coord = 0 }, + { coord = 1434 }, + { coord = 0 }, + { coord = -1065 }, + { coord = 0 }, + { coord = -369 }, + { coord = 0 }, + { coord = 1434 }, + { coord = 0 }, + { coord = -1434 }, + { coord = 0 }, + { coord = 565 }, + { coord = 0 }, + { coord = 467 }, + ], }, }, ], diff --git a/formats/opentype.fathom b/formats/opentype.fathom index 14d20bdb6..a15ee016a 100644 --- a/formats/opentype.fathom +++ b/formats/opentype.fathom @@ -2793,25 +2793,54 @@ def glyph_header = { /// /// - [Microsoft's OpenType Spec: Glyph Headers](https://docs.microsoft.com/en-us/typography/opentype/spec/glyf#simple-glyph-description) /// - [Apple's TrueType Reference Manual: The `'loca'` table](https://developer.apple.com/fonts/TrueType-Reference-Manual/RM06/Chap6glyf.html) -def simple_glyph = fun (number_of_contours : U16) => { - /// Array of point indices for the last point of each contour, in increasing numeric order. - end_pts_of_contours <- array16 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 <- array16 instruction_length u8, - let last_end_point_index = array16_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, - /// xCoordinates[variable] Contour point x-coordinates. Coordinate for the first point is relative to (0,0); - /// others are relative to previous point. - // or int16 <- uint8, - /// yCoordinates[variable] Contour point y-coordinates. Coordinate for the first point is relative to (0,0); - /// others are relative to previous point. - // or int16 <- uint8, -}; +def simple_glyph = fun (number_of_contours : U16) => ( + let flag = { + flag <- u8, + repeat <- or_succeed ((u8_and flag 8) != (0 : U8)) u8 0, + }; + + let flag_repeat = fun (f : Repr flag) => u16_from_u8 f.repeat + (1 : U16); + let flag_is_set = fun (bit : U8) => fun (f : Repr flag) => u8_and f.flag bit != (0 : U8); + let x_is_short = flag_is_set 2; + let x_is_same = flag_is_set 0x10; + let y_is_short = flag_is_set 4; + let y_is_same = flag_is_set 0x20; + + { + /// Array of point indices for the last point of each contour, in increasing numeric order. + end_pts_of_contours <- array16 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 <- array16 instruction_length u8, + + let number_of_coords = match (u16_gt number_of_contours (0 : U16)) { + true => array16_index _ _ (number_of_contours - (1 : U16)) end_pts_of_contours + (1 : U16), + false => 0 + }, + + /// Array of flag elements. + flags <- repeat_until_full number_of_coords flag flag_repeat, + + let read_coord = fun (is_short : Repr flag -> Bool) => fun (is_same : Repr flag -> Bool) => fun (f : Repr flag) => { + coord <- match (is_short f) { + true => u8, + false => match (is_same f) { + true => succeed S16 0, + false => s16be, + } + } + }, + + /// Contour point x-coordinates. Coordinate for the first point is relative to (0,0); + /// others are relative to previous point. + x_coordinates <- array16_map number_of_coords _ (read_coord x_is_short x_is_same) flags, + /// Contour point y-coordinates. Coordinate for the first point is relative to (0,0); + /// others are relative to previous point. + y_coordinates <- array16_map number_of_coords _ (read_coord y_is_short y_is_same) flags, + } +); def args_are_signed = fun (flags : U16) => u16_and flags 0x0002 != (0 : U16); diff --git a/formats/opentype.snap b/formats/opentype.snap index 6d85be59d..178c4abeb 100644 --- a/formats/opentype.snap +++ b/formats/opentype.snap @@ -380,13 +380,44 @@ def composite_glyph : Format = { argument1 <- arg_format flags, argument2 <- arg_format flags, }; -def simple_glyph : U16 -> Format = fun number_of_contours => { +def simple_glyph : U16 -> Format = fun number_of_contours => let flag : +_ number_of_contours = { + flag <- u8, + repeat <- or_succeed (u8_and flag 8 != (0 : U8)) u8 0, +}; +let flag_repeat : _ number_of_contours = fun f => u16_from_u8 f.repeat + (1 : +U16); +let flag_is_set : _ number_of_contours = +fun bit => fun f => u8_and f.flag bit != (0 : U8); +let x_is_short : _ number_of_contours = flag_is_set 2; +let x_is_same : _ number_of_contours = flag_is_set 0x10; +let y_is_short : _ number_of_contours = flag_is_set 4; +let y_is_same : _ number_of_contours = flag_is_set 0x20; +{ end_pts_of_contours <- array16 number_of_contours u16be, instruction_length <- u16be, instructions <- array16 instruction_length u8, - let last_end_point_index : U16 = array16_index (_ number_of_contours end_pts_of_contours instruction_length instructions) (_ number_of_contours end_pts_of_contours instruction_length instructions) (number_of_contours - (1 : - U16)) end_pts_of_contours, - let number_of_coords : U16 = last_end_point_index + (1 : U16), + let number_of_coords : U16 = match (u16_gt number_of_contours 0) { + false => 0, + true => array16_index (_ number_of_contours end_pts_of_contours instruction_length instructions) (_ number_of_contours end_pts_of_contours instruction_length instructions) (number_of_contours - (1 : + U16)) end_pts_of_contours + (1 : U16), + }, + flags <- repeat_until_full number_of_coords flag flag_repeat, + let read_coord : ({ flag : U8, repeat : U8 } -> Bool) -> ({ + flag : U8, + repeat : U8, + } -> Bool) -> { flag : U8, repeat : U8 } -> + Format = fun is_short => fun is_same => fun f => { + coord <- match (is_short f) { + false => match (is_same f) { + false => s16be, + true => succeed S16 0, + }, + true => u8, + }, + }, + x_coordinates <- array16_map number_of_coords (_ number_of_contours end_pts_of_contours instruction_length instructions number_of_coords flags read_coord) (read_coord x_is_short x_is_same) flags, + y_coordinates <- array16_map number_of_coords (_ number_of_contours end_pts_of_contours instruction_length instructions number_of_coords flags read_coord x_coordinates) (read_coord y_is_short y_is_same) flags, }; def glyph : Format = { header <- glyph_header, diff --git a/tests/succeed/primitives.snap b/tests/succeed/primitives.snap index 62df3424e..d9c67436a 100644 --- a/tests/succeed/primitives.snap +++ b/tests/succeed/primitives.snap @@ -53,10 +53,15 @@ let _ : _ = array16; let _ : _ = array32; let _ : _ = array64; let _ : _ = repeat_until_end; +let _ : _ = repeat_until_full; let _ : _ = array8; let _ : _ = array16; let _ : _ = array32; let _ : _ = array64; +let _ : _ = array8_map; +let _ : _ = array16_map; +let _ : _ = array32_map; +let _ : _ = array64_map; let _ : _ = link; let _ : _ = deref; let _ : _ = stream_pos; @@ -103,6 +108,7 @@ let _ : _ = u16_shr; let _ : _ = u16_and; let _ : _ = u16_or; let _ : _ = u16_xor; +let _ : _ = u16_from_u8; let _ : _ = u32_eq; let _ : _ = u32_neq; let _ : _ = u32_gt; From c34df110eb8ab7179c8f9a74372679f7c36af543 Mon Sep 17 00:00:00 2001 From: Wesley Moore Date: Thu, 1 Sep 2022 10:40:34 +1000 Subject: [PATCH 6/7] Add versions of repeat_until_full for other index sizes --- fathom/src/core.rs | 16 ++++++++++++-- fathom/src/core/binary.rs | 35 +++++++++++++++++-------------- fathom/src/core/semantics.rs | 11 +++++++++- fathom/src/surface/elaboration.rs | 23 +++++++++++++------- formats/opentype.fathom | 2 +- formats/opentype.snap | 2 +- tests/succeed/primitives.fathom | 5 ++++- tests/succeed/primitives.snap | 5 ++++- 8 files changed, 69 insertions(+), 30 deletions(-) diff --git a/fathom/src/core.rs b/fathom/src/core.rs index 44e719fb7..b8e3cbc32 100644 --- a/fathom/src/core.rs +++ b/fathom/src/core.rs @@ -381,10 +381,22 @@ def_prims! { FormatArray64Map => "array64_map", /// Repeat a format until the length of the given parse scope is reached. FormatRepeatUntilEnd => "repeat_until_end", - /// Repeat a format until the array is filled. + /// Repeat a format until the array with 8-bit indices is filled. /// /// The value read by the format is replicated according to a supplied function. - FormatRepeatUntilFull => "repeat_until_full", + FormatRepeatUntilFull8 => "repeat_until_full8", + /// Repeat a format until the array with 16-bit indices is filled. + /// + /// The value read by the format is replicated according to a supplied function. + FormatRepeatUntilFull16 => "repeat_until_full16", + /// Repeat a format until the array with 32-bit indices is filled. + /// + /// The value read by the format is replicated according to a supplied function. + FormatRepeatUntilFull32 => "repeat_until_full32", + /// Repeat a format until the array with 64-bit indices is filled. + /// + /// The value read by the format is replicated according to a supplied function. + FormatRepeatUntilFull64 => "repeat_until_full64", /// Limit the format to an unsigned 8-bit byte length. FormatLimit8 => "limit8", /// Limit the format to an unsigned 16-bit byte length. diff --git a/fathom/src/core/binary.rs b/fathom/src/core/binary.rs index 6a1461c47..ebd0172c2 100644 --- a/fathom/src/core/binary.rs +++ b/fathom/src/core/binary.rs @@ -411,19 +411,22 @@ impl<'arena, 'env, 'data> Context<'arena, 'env, '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::FormatArray8, [FunApp(len), FunApp(format)]) => self.read_array(reader, span, len, format), - (Prim::FormatArray16, [FunApp(len), FunApp(format)]) => self.read_array(reader, span, len, format), - (Prim::FormatArray32, [FunApp(len), FunApp(format)]) => self.read_array(reader, span, len, format), + (Prim::FormatArray8, [FunApp(len), FunApp(format)]) | + (Prim::FormatArray16, [FunApp(len), FunApp(format)]) | + (Prim::FormatArray32, [FunApp(len), FunApp(format)]) | (Prim::FormatArray64, [FunApp(len), FunApp(format)]) => self.read_array(reader, span, len, format), - (Prim::FormatArray8Map, [_, _, FunApp(map_fn), FunApp(array)]) => self.array_map(reader, span, map_fn, array), - (Prim::FormatArray16Map, [_, _, FunApp(map_fn), FunApp(array)]) => self.array_map(reader, span, map_fn, array), - (Prim::FormatArray32Map, [_, _, FunApp(map_fn), FunApp(array)]) => self.array_map(reader, span, map_fn, array), + (Prim::FormatArray8Map, [_, _, FunApp(map_fn), FunApp(array)]) | + (Prim::FormatArray16Map, [_, _, FunApp(map_fn), FunApp(array)]) | + (Prim::FormatArray32Map, [_, _, FunApp(map_fn), FunApp(array)]) | (Prim::FormatArray64Map, [_, _, FunApp(map_fn), FunApp(array)]) => self.array_map(reader, span, map_fn, array), (Prim::FormatRepeatUntilEnd, [FunApp(format)]) => self.read_repeat_until_end(reader, format), - (Prim::FormatRepeatUntilFull, [FunApp(len), FunApp(format), FunApp(replicate)]) => self.read_repeat_until_full(reader, len, replicate, format), - (Prim::FormatLimit8, [FunApp(limit), FunApp(format)]) => self.read_limit(reader, limit, format), - (Prim::FormatLimit16, [FunApp(limit), FunApp(format)]) => self.read_limit(reader, limit, format), - (Prim::FormatLimit32, [FunApp(limit), FunApp(format)]) => self.read_limit(reader, limit, format), + (Prim::FormatRepeatUntilFull8, [FunApp(len), FunApp(format), FunApp(replicate)]) | + (Prim::FormatRepeatUntilFull16, [FunApp(len), FunApp(format), FunApp(replicate)]) | + (Prim::FormatRepeatUntilFull32, [FunApp(len), FunApp(format), FunApp(replicate)]) | + (Prim::FormatRepeatUntilFull64, [FunApp(len), FunApp(format), FunApp(replicate)]) => self.read_repeat_until_full(reader, len, replicate, format), + (Prim::FormatLimit8, [FunApp(limit), FunApp(format)]) | + (Prim::FormatLimit16, [FunApp(limit), FunApp(format)]) | + (Prim::FormatLimit32, [FunApp(limit), FunApp(format)]) | (Prim::FormatLimit64, [FunApp(limit), FunApp(format)]) => self.read_limit(reader, limit, format), (Prim::FormatLink, [FunApp(pos), FunApp(format)]) => self.read_link(span, pos, format), (Prim::FormatDeref, [FunApp(format), FunApp(r#ref)]) => self.read_deref(format, r#ref), @@ -529,9 +532,7 @@ impl<'arena, 'env, 'data> Context<'arena, 'env, 'data> { _ => return Err(ReadError::InvalidValue(len.span())), } .ok_or_else(|| ReadError::InvalidValue(len.span()))?; - - // TODO: Do we need to force replicate as well? - // let replicate = self.elim_env().force(replicate); + let replicate = self.elim_env().force(replicate); let mut elems = Vec::with_capacity(len); while elems.len() < len { @@ -544,9 +545,11 @@ impl<'arena, 'env, 'data> Context<'arena, 'env, 'data> { _ => return Err(ReadError::InvalidValue(replicate.span())), }; - // Push it that many times onto the array - // TODO: Error/limit if this exceeds len? - elems.extend(std::iter::repeat(elem).take(usize::from(repeat))); + // Push it that many times onto the array, limiting to the length of the + // output array. + elems.extend( + std::iter::repeat(elem).take(usize::from(repeat).min(len - elems.len())), + ); } Err(err) => return Err(err), }; diff --git a/fathom/src/core/semantics.rs b/fathom/src/core/semantics.rs index 968fb37f7..de5967cf6 100644 --- a/fathom/src/core/semantics.rs +++ b/fathom/src/core/semantics.rs @@ -867,9 +867,18 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> { (Prim::FormatRepeatUntilEnd, [Elim::FunApp(elem)]) => { Value::prim(Prim::ArrayType, [self.format_repr(elem)]) } - (Prim::FormatRepeatUntilFull, [Elim::FunApp(len), Elim::FunApp(elem), _]) => { + (Prim::FormatRepeatUntilFull8, [Elim::FunApp(len), Elim::FunApp(elem), _]) => { + Value::prim(Prim::Array8Type, [len.clone(), self.format_repr(elem)]) + } + (Prim::FormatRepeatUntilFull16, [Elim::FunApp(len), Elim::FunApp(elem), _]) => { Value::prim(Prim::Array16Type, [len.clone(), self.format_repr(elem)]) } + (Prim::FormatRepeatUntilFull32, [Elim::FunApp(len), Elim::FunApp(elem), _]) => { + Value::prim(Prim::Array32Type, [len.clone(), self.format_repr(elem)]) + } + (Prim::FormatRepeatUntilFull64, [Elim::FunApp(len), Elim::FunApp(elem), _]) => { + Value::prim(Prim::Array64Type, [len.clone(), self.format_repr(elem)]) + } (Prim::FormatLink, [_, Elim::FunApp(elem)]) => { Value::prim(Prim::RefType, [elem.clone()]) } diff --git a/fathom/src/surface/elaboration.rs b/fathom/src/surface/elaboration.rs index 1854bddda..7b9f37903 100644 --- a/fathom/src/surface/elaboration.rs +++ b/fathom/src/surface/elaboration.rs @@ -230,12 +230,11 @@ impl<'arena> RigidEnv<'arena> { env.define_prim_fun(FormatRepeatUntilEnd, [&FORMAT_TYPE], &FORMAT_TYPE); // repeat_until_full16 : U16 -> fun (A : Format) -> (Repr A -> U16) -> Format - env.define_prim( - FormatRepeatUntilFull, + let repeat_until_full = |index_type| { scope.to_scope(core::Term::FunType( Span::Empty, - None, - &U16_TYPE, + env.name("len"), + index_type, scope.to_scope(core::Term::FunType( Span::Empty, env.name("A"), @@ -251,13 +250,23 @@ impl<'arena> RigidEnv<'arena> { &Term::Prim(Span::Empty, FormatRepr), &VAR0, )), - &U16_TYPE, + index_type, )), &FORMAT_TYPE, )), )), - )), - ); + )) + }; + + let repeat_until_full8 = repeat_until_full(&U8_TYPE); + let repeat_until_full16 = repeat_until_full(&U16_TYPE); + let repeat_until_full32 = repeat_until_full(&U32_TYPE); + let repeat_until_full64 = repeat_until_full(&U64_TYPE); + env.define_prim(FormatRepeatUntilFull8, repeat_until_full8); + env.define_prim(FormatRepeatUntilFull16, repeat_until_full16); + env.define_prim(FormatRepeatUntilFull32, repeat_until_full32); + env.define_prim(FormatRepeatUntilFull64, repeat_until_full64); + env.define_prim_fun(FormatLimit8, [&U8_TYPE, &FORMAT_TYPE], &FORMAT_TYPE); env.define_prim_fun(FormatLimit16, [&U16_TYPE, &FORMAT_TYPE], &FORMAT_TYPE); env.define_prim_fun(FormatLimit32, [&U32_TYPE, &FORMAT_TYPE], &FORMAT_TYPE); diff --git a/formats/opentype.fathom b/formats/opentype.fathom index a15ee016a..2490e627c 100644 --- a/formats/opentype.fathom +++ b/formats/opentype.fathom @@ -2821,7 +2821,7 @@ def simple_glyph = fun (number_of_contours : U16) => ( }, /// Array of flag elements. - flags <- repeat_until_full number_of_coords flag flag_repeat, + flags <- repeat_until_full16 number_of_coords flag flag_repeat, let read_coord = fun (is_short : Repr flag -> Bool) => fun (is_same : Repr flag -> Bool) => fun (f : Repr flag) => { coord <- match (is_short f) { diff --git a/formats/opentype.snap b/formats/opentype.snap index 178c4abeb..877f9ebc2 100644 --- a/formats/opentype.snap +++ b/formats/opentype.snap @@ -402,7 +402,7 @@ let y_is_same : _ number_of_contours = flag_is_set 0x20; true => array16_index (_ number_of_contours end_pts_of_contours instruction_length instructions) (_ number_of_contours end_pts_of_contours instruction_length instructions) (number_of_contours - (1 : U16)) end_pts_of_contours + (1 : U16), }, - flags <- repeat_until_full number_of_coords flag flag_repeat, + flags <- repeat_until_full16 number_of_coords flag flag_repeat, let read_coord : ({ flag : U8, repeat : U8 } -> Bool) -> ({ flag : U8, repeat : U8, diff --git a/tests/succeed/primitives.fathom b/tests/succeed/primitives.fathom index ff759c456..2041662bf 100644 --- a/tests/succeed/primitives.fathom +++ b/tests/succeed/primitives.fathom @@ -56,7 +56,10 @@ let _ = array16 : U16 -> Format -> Format; let _ = array32 : U32 -> Format -> Format; let _ = array64 : U64 -> Format -> Format; let _ = repeat_until_end : Format -> Format; -let _ = repeat_until_full : U16 -> fun (A : Format) -> (Repr A -> U16) -> Format; +let _ = repeat_until_full8 : U8 -> fun (A : Format) -> (Repr A -> U8) -> Format; +let _ = repeat_until_full16 : U16 -> fun (A : Format) -> (Repr A -> U16) -> Format; +let _ = repeat_until_full32 : U32 -> fun (A : Format) -> (Repr A -> U32) -> Format; +let _ = repeat_until_full64 : U64 -> fun (A : Format) -> (Repr A -> U64) -> Format; let _ = array8 : U8 -> Format -> Format; let _ = array16 : U16 -> Format -> Format; let _ = array32 : U32 -> Format -> Format; diff --git a/tests/succeed/primitives.snap b/tests/succeed/primitives.snap index d9c67436a..e817424f5 100644 --- a/tests/succeed/primitives.snap +++ b/tests/succeed/primitives.snap @@ -53,7 +53,10 @@ let _ : _ = array16; let _ : _ = array32; let _ : _ = array64; let _ : _ = repeat_until_end; -let _ : _ = repeat_until_full; +let _ : _ = repeat_until_full8; +let _ : _ = repeat_until_full16; +let _ : _ = repeat_until_full32; +let _ : _ = repeat_until_full64; let _ : _ = array8; let _ : _ = array16; let _ : _ = array32; From cd4cc01da318a342670b4ffcdc37fd6a63cecf6c Mon Sep 17 00:00:00 2001 From: Wesley Moore Date: Thu, 1 Sep 2022 12:04:23 +1000 Subject: [PATCH 7/7] Add new primitives to reference --- doc/reference.md | 65 ++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 57 insertions(+), 8 deletions(-) diff --git a/doc/reference.md b/doc/reference.md index 6bfbafaf1..8d58c6b39 100644 --- a/doc/reference.md +++ b/doc/reference.md @@ -27,6 +27,7 @@ elaboration, and core language is forthcoming. - [Overlap formats](#overlap-formats) - [Number formats](#number-formats) - [Array formats](#array-formats) + - [Map formats](#map-formats) - [Repeat formats](#repeat-formats) - [Limit formats](#limit-formats) - [Stream position formats](#stream-position-formats) @@ -505,6 +506,30 @@ of the host [array types](#array-types). | `array32 len format` | `Array32 len (Repr format)` | | `array64 len format` | `Array64 len (Repr format)` | +### Map formats + +There are four array map formats, corresponding to the four [array types](#arrays). +These allow mapping a supplied function over the elements of an array in order +to parse another array: + +- `array8_map : fun (len : U8) -> fun (A : Type) -> (A -> Format) -> Array8 len A -> Format` +- `array16_map : fun (len : U16) -> fun (A : Type) -> (A -> Format) -> Array16 len A -> Format` +- `array32_map : fun (len : U32) -> fun (A : Type) -> (A -> Format) -> Array32 len A -> Format` +- `array64_map : fun (len : U64) -> fun (A : Type) -> (A -> Format) -> Array64 len A -> Format` + +#### Representation of map formats + +The [representation](#format-representations) of the array map formats preserve the +lengths, and use the representation of the map function as the element types +of the host [array types](#array-types). + +| format | `Repr` format | +|----------------------------------|-----------------------------| +| `array8_map len A map_fn array` | `Array8 len (Repr map_fn)` | +| `array16_map len A map_fn array` | `Array16 len (Repr map_fn)` | +| `array32_map len A map_fn array` | `Array32 len (Repr map_fn)` | +| `array64_map len A map_fn array` | `Array64 len (Repr map_fn)` | + ### Repeat formats The `repeat_until_end` format repeats parsing the given format until the end of @@ -512,15 +537,31 @@ the current binary stream is reached: - `repeat_until_end : Format -> Format` +There are four repeat until full formats that parse and replicate a format until +a given length is reached: + +- `repeat_until_full8 : U8 -> fun (A : Format) -> (Repr A -> U8) -> Format` +- `repeat_until_full16 : U16 -> fun (A : Format) -> (Repr A -> U16) -> Format` +- `repeat_until_full32 : U32 -> fun (A : Format) -> (Repr A -> U32) -> Format` +- `repeat_until_full64 : U64 -> fun (A : Format) -> (Repr A -> U64) -> Format` + +The supplied function can be used to replicate a single parsed format multiple +times into the final array. + #### Representation of repeat formats -Because the repeat format does not have a predefined length, it is +Because the repeat until end format does not have a predefined length, it is [represented](#format-representations) as a dynamically sized -[array type](#array-types): +[array type](#array-types). The repeat until full format preserves the length +in its [representation](#format-representations): -| format | `Repr` format | -| ------------------------- | --------------------- | -| `repeat_until_end format` | `Array (Repr format)` | +| format | `Repr` format | +|-------------------------------------|-----------------------------| +| `repeat_until_end format` | `Array (Repr format)` | +| `repeat_until_full8 len replicate` | `Array8 len (Repr format)` | +| `repeat_until_full16 len replicate` | `Array16 len (Repr format)` | +| `repeat_until_full32 len replicate` | `Array32 len (Repr format)` | +| `repeat_until_full64 len replicate` | `Array64 len (Repr format)` | ### Limit formats @@ -595,11 +636,18 @@ embedded in the resulting parsed output. - `succeed : fun (A : Type) -> A -> Format` +The `or_succeed` accepts a boolean condition value. If the condition value is +`true` then the format is used, otherwise the default value is used, consuming +no input: + +- `or_succeed : Bool -> fun (A : Format) -> Repr A -> Format` + #### Representation of succeed formats -| format | `Repr` format | -| ------------- | ------------- | -| `succeed A a` | `A` | +| format | `Repr` format | +|----------------------------------|---------------| +| `succeed A a` | `A` | +| `or_succeed cond format default` | `Repr format` | ### Fail format @@ -845,6 +893,7 @@ A number of operations are defined for the numeric types: - `u16_and : U16 -> U16 -> U16` - `u16_or : U16 -> U16 -> U16` - `u16_xor : U16 -> U16 -> U16` +- `u16_from_u8 : U8 -> U16` - `u32_eq : U32 -> U32 -> Bool` - `u32_neq : U32 -> U32 -> Bool`