Conditional formats

doc/reference.md

@@ -21,6 +21,7 @@ elaboration, and core language is forthcoming.
   - [Format types](#format-types)
   - [Format representations](#format-representations)
   - [Record formats](#record-formats)
+  - [Conditional formats](#conditional-formats)
   - [Overlap formats](#overlap-formats)
   - [Number formats](#number-formats)
   - [Array formats](#array-formats)
@@ -272,6 +273,29 @@ Some examples are as follows:
 | `{ x <- f32le, y <- f32le }`               | `{ x : F32, y : F32 }`                 |
 | `{ len <- u16be, data <- array16 len s8 }` | `{ len : U16, data : Array16 len S8 }` |
 
+### Conditional formats
+
+Conditional formats are formats with an associated condition predicate. The format
+will only succeed if the condition is `true`. This can be used to verify magic numbers
+or version expectations. E.g.
+
+```fathom
+{ magic <- { magic <- u64le | u64_eq magic 0x00ffffffffffff00 } }
+```
+
+```fathom
+{ major_version <- { version <- u16be | u16_lte version 2 } }
+```
+
+#### Representation of conditional formats
+
+The [representation](#format-representations) of a conditional format is the same
+as the representation of the format guarded by the predicate. I.e.
+
+| format                    | `Repr` format        |
+| ------------------------- | -------------------- |
+| `{ x <- format \| cond }` | `Repr format`        |
+
 ### Overlap formats
 
 Overlap formats are very similar to [record formats](#record-formats), only each

fathom/src/core.rs

@@ -138,6 +138,8 @@ pub enum Term<'arena> {
 
     /// Record formats, consisting of a list of dependent formats.
     FormatRecord(&'arena [StringId], &'arena [Term<'arena>]),
+    /// Conditional format, consisting of a format and predicate.
+    FormatCond(StringId, &'arena Term<'arena>, &'arena Term<'arena>),
     /// Overlap formats, consisting of a list of dependent formats, overlapping
     /// in memory.
     FormatOverlap(&'arena [StringId], &'arena [Term<'arena>]),

fathom/src/core/binary.rs

@@ -77,6 +77,22 @@ impl<'arena, 'env> Context<'arena, 'env> {
 
                 Ok(Arc::new(Value::RecordLit(labels, exprs)))
             }
+            Value::FormatCond(_label, format, cond) => {
+                let value = self.read_format(reader, &format)?;
+                let cond_res = self.elim_context().apply_closure(cond, value.clone());
+
+                match *cond_res {
+                    Value::ConstLit(Const::Bool(true)) => Ok(value),
+                    Value::ConstLit(Const::Bool(false)) => {
+                        // TODO: better user experience for this case
+                        Err(io::Error::new(io::ErrorKind::Other, "cond failed"))
+                    }
+                    _ => {
+                        // This shouldn't happen since we check that the cond type is Bool earlier
+                        Err(io::Error::new(io::ErrorKind::Other, "expected bool"))
+                    }
+                }
+            }
             Value::FormatOverlap(labels, formats) => {
                 let initial_pos = reader.stream_position()?;
                 let mut max_pos = initial_pos;

fathom/src/core/semantics.rs

@@ -41,6 +41,8 @@ pub enum Value<'arena> {
 
     /// Record formats, consisting of a list of dependent formats.
     FormatRecord(&'arena [StringId], Telescope<'arena>),
+    /// Conditional format, consisting of a format and predicate.
+    FormatCond(StringId, ArcValue<'arena>, Closure<'arena>),
     /// Overlap formats, consisting of a list of dependent formats, overlapping
     /// in memory.
     FormatOverlap(&'arena [StringId], Telescope<'arena>),
@@ -337,6 +339,11 @@ impl<'arena, 'env> EvalContext<'arena, 'env> {
                 let formats = Telescope::new(self.rigid_exprs.clone(), formats);
                 Arc::new(Value::FormatRecord(labels, formats))
             }
+            Term::FormatCond(name, format, cond) => {
+                let format = self.eval(format);
+                let cond_expr = Closure::new(self.rigid_exprs.clone(), cond);
+                Arc::new(Value::FormatCond(*name, format, cond_expr))
+            }
             Term::FormatOverlap(labels, formats) => {
                 let formats = Telescope::new(self.rigid_exprs.clone(), formats);
                 Arc::new(Value::FormatOverlap(labels, formats))
@@ -748,6 +755,7 @@ impl<'arena, 'env> ElimContext<'arena, 'env> {
             Value::FormatRecord(labels, formats) | Value::FormatOverlap(labels, formats) => {
                 Arc::new(Value::RecordType(labels, formats.clone().apply_repr()))
             }
+            Value::FormatCond(_label, format, _cond) => Arc::clone(format),
             Value::Stuck(Head::Prim(prim), spine) => match (prim, &spine[..]) {
                 (Prim::FormatU8, []) => Arc::new(Value::prim(Prim::U8Type, [])),
                 (Prim::FormatU16Be, []) => Arc::new(Value::prim(Prim::U16Type, [])),
@@ -927,6 +935,15 @@ impl<'in_arena, 'out_arena, 'env> QuoteContext<'in_arena, 'out_arena, 'env> {
 
                 Term::FormatRecord(labels, formats)
             }
+            Value::FormatCond(label, format, cond) => {
+                let format = self.quote(format);
+                let cond = self.quote_closure(cond);
+                Term::FormatCond(
+                    *label,
+                    self.scope.to_scope(format),
+                    self.scope.to_scope(cond),
+                )
+            }
             Value::FormatOverlap(labels, formats) => {
                 let labels = self.scope.to_scope_from_iter(labels.iter().copied()); // FIXME: avoid copy if this is the same arena?
                 let formats = self.quote_telescope(formats);
@@ -1078,6 +1095,15 @@ impl<'arena, 'env> ConversionContext<'arena, 'env> {
                 labels0 == labels1 && self.is_equal_telescopes(formats0, formats1)
             }
 
+            (
+                Value::FormatCond(label0, format0, cond0),
+                Value::FormatCond(label1, format1, cond1),
+            ) => {
+                label0 == label1
+                    && self.is_equal(format0, format1)
+                    && self.is_equal_closures(cond0, cond1)
+            }
+
             (Value::ConstLit(const0), Value::ConstLit(const1)) => const0 == const1,
 
             (_, _) => false,
@@ -1196,3 +1222,36 @@ impl<'arena, 'env> ConversionContext<'arena, 'env> {
         })
     }
 }
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::core::Const;
+
+    #[test]
+    fn value_has_unify_and_is_equal_impls() {
+        let value = Arc::new(Value::ConstLit(Const::Bool(false)));
+
+        // This test exists in order to cause a test failure when `Value` is changed. If this test
+        // has failed and you have added a new variant to Value it is a prompt to ensure that
+        // variant is handled in:
+        //
+        // - surface::elaboration::Context::unify
+        // - core::semantics::is_equal
+        //
+        // NOTE: Only update the match below when you've updated the above functions.
+        match value.as_ref() {
+            Value::Stuck(_, _) => {}
+            Value::Universe => {}
+            Value::FunType(_, _, _) => {}
+            Value::FunLit(_, _) => {}
+            Value::RecordType(_, _) => {}
+            Value::RecordLit(_, _) => {}
+            Value::ArrayLit(_) => {}
+            Value::FormatRecord(_, _) => {}
+            Value::FormatCond(_, _, _) => {}
+            Value::FormatOverlap(_, _) => {}
+            Value::ConstLit(_) => {}
+        }
+    }
+}

fathom/src/surface.rs

@@ -133,6 +133,13 @@ pub enum Term<'arena, Range> {
     FormatRecord(Range, &'arena [((Range, StringId), Term<'arena, Range>)]),
     /// Overlap format.
     FormatOverlap(Range, &'arena [((Range, StringId), Term<'arena, Range>)]),
+    /// Conditional format.
+    FormatCond(
+        Range,
+        (Range, StringId),
+        &'arena Term<'arena, Range>,
+        &'arena Term<'arena, Range>,
+    ),
     /// Reported error sentinel.
     ReportedError(Range),
 }
@@ -161,6 +168,7 @@ impl<'arena, Range: Clone> Term<'arena, Range> {
             | Term::NumberLiteral(range, _)
             | Term::BooleanLiteral(range, _)
             | Term::FormatRecord(range, _)
+            | Term::FormatCond(range, _, _, _)
             | Term::FormatOverlap(range, _)
             | Term::ReportedError(range) => range.clone(),
         }

fathom/src/surface/distillation.rs

@@ -402,6 +402,18 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
             core::Term::FormatRecord(labels, formats) => {
                 Term::FormatRecord((), self.synth_format_fields(labels, formats))
             }
+            core::Term::FormatCond(label, format, cond) => {
+                let format = self.check(format);
+                self.push_rigid(Some(*label));
+                let cond = self.check(cond);
+                self.pop_rigid();
+                Term::FormatCond(
+                    (),
+                    ((), *label),
+                    self.scope.to_scope(format),
+                    self.scope.to_scope(cond),
+                )
+            }
             core::Term::FormatOverlap(labels, formats) => {
                 Term::FormatOverlap((), self.synth_format_fields(labels, formats))
             }

fathom/src/surface/elaboration.rs

@@ -1717,6 +1717,25 @@ impl<'interner, 'arena, 'error> Context<'interner, 'arena, 'error> {
 
                 (core::Term::FormatRecord(labels, formats), format_type)
             }
+            Term::FormatCond(_range, (_, label), format, cond) => {
+                let format_type = Arc::new(Value::prim(Prim::FormatType, []));
+                let format = self.check(format, &format_type);
+                let format_value = self.eval_context().eval(&format);
+                let r#type = self.elim_context().format_repr(&format_value);
+                self.rigid_env.push_param(Some(*label), r#type);
+                let bool_type = Arc::new(Value::prim(Prim::BoolType, []));
+                let cond_expr = self.check(cond, &bool_type);
+                self.rigid_env.pop();
+
+                (
+                    core::Term::FormatCond(
+                        *label,
+                        self.scope.to_scope(format),
+                        self.scope.to_scope(cond_expr),
+                    ),
+                    format_type,
+                )
+            }
             Term::FormatOverlap(range, format_fields) => {
                 let format_type = Arc::new(Value::prim(Prim::FormatType, []));
                 let (labels, formats) = self.check_format_fields(*range, format_fields);

fathom/src/surface/elaboration/unification.rs

@@ -271,6 +271,17 @@ impl<'arena, 'env> Context<'arena, 'env> {
                 self.unify_telescopes(formats0, formats1)
             }
 
+            (
+                Value::FormatCond(label0, format0, cond0),
+                Value::FormatCond(label1, format1, cond1),
+            ) => {
+                if label0 != label1 {
+                    return Err(Error::Mismatch);
+                }
+                self.unify(format0, format1)?;
+                self.unify_closures(cond0, cond1)
+            }
+
             (Value::ConstLit(const0), Value::ConstLit(const1)) if const0 == const1 => Ok(()),
 
             // Flexible-rigid cases
@@ -584,6 +595,15 @@ impl<'arena, 'env> Context<'arena, 'env> {
 
                 Ok(Term::FormatRecord(labels, formats))
             }
+            Value::FormatCond(label, format, cond) => {
+                let format = self.rename(flexible_var, format)?;
+                let cond = self.rename_closure(flexible_var, cond)?;
+                Ok(Term::FormatCond(
+                    *label,
+                    self.scope.to_scope(format),
+                    self.scope.to_scope(cond),
+                ))
+            }
             Value::FormatOverlap(labels, formats) => {
                 let labels = self.scope.to_scope(labels); // FIXME: avoid copy if this is the same arena?
                 let formats = self.rename_telescope(flexible_var, formats)?;

fathom/src/surface/grammar.lalrpop

@@ -37,6 +37,7 @@ extern {
         "." => Token::FullStop,
         "->" => Token::HyphenGreater,
         "<-" => Token::LessHyphen,
+        "|" => Token::Pipe,
         ";" => Token::Semicolon,
         "_" => Token::Underscore,
 
@@ -152,6 +153,9 @@ AtomicTerm: Term<'arena, ByteRange> = {
     <start: @L> "{" <fields: NonEmptySeq<(<RangedName> "<-" <Term>), ",">> "}" <end: @R> => {
         Term::FormatRecord(ByteRange::new(start, end), fields)
     },
+    <start: @L> "{" <name:RangedName> "<-" <format:Term> "|" <cond:Term> "}" <end: @R> => {
+        Term::FormatCond(ByteRange::new(start, end), name, scope.to_scope(format), scope.to_scope(cond))
+    },
     <start: @L> "overlap" "{" <fields: NonEmptySeq<(<RangedName> "<-" <Term>), ",">> "}" <end: @R> => {
         Term::FormatOverlap(ByteRange::new(start, end), fields)
     },

fathom/src/surface/lexer.rs

@@ -43,6 +43,8 @@ pub enum Token<'source> {
     HyphenGreater,
     #[token("<-")]
     LessHyphen,
+    #[token("|")]
+    Pipe,
     #[token(";")]
     Semicolon,
     #[token("_")]
@@ -125,6 +127,7 @@ impl<'source> Token<'source> {
             Token::HyphenGreater => "->",
             Token::LessHyphen => "<-",
             Token::Semicolon => ";",
+            Token::Pipe => "|",
             Token::Underscore => "_",
             Token::OpenBrace => "{",
             Token::CloseBrace => "}",

fathom/src/surface/pretty.rs

@@ -247,6 +247,21 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
                 self.text(","),
                 self.text("}"),
             ),
+            Term::FormatCond(_, (_, label), format, cond) => self.concat([
+                self.text("{"),
+                self.space(),
+                self.string_id(*label),
+                self.space(),
+                self.text("<-"),
+                self.space(),
+                self.term_prec(Prec::Top, format),
+                self.space(),
+                self.text("|"),
+                self.space(),
+                self.term_prec(Prec::Top, cond),
+                self.space(),
+                self.text("}"),
+            ]),
             Term::FormatOverlap(_, format_fields) => self.sequence(
                 self.concat([self.text("overlap"), self.space(), self.text("{")]),
                 format_fields.iter().map(|((_, label), format)| {