Add or_succeed primitive

Author: wezm

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.

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<ArcValue<'arena>, 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,

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, []),

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,

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;

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;