diff options
Diffstat (limited to 'dhall_syntax/src')
-rw-r--r-- | dhall_syntax/src/core/expr.rs | 6 | ||||
-rw-r--r-- | dhall_syntax/src/core/visitor.rs | 1 | ||||
-rw-r--r-- | dhall_syntax/src/parser.rs | 12 | ||||
-rw-r--r-- | dhall_syntax/src/printer.rs | 4 |
4 files changed, 22 insertions, 1 deletions
diff --git a/dhall_syntax/src/core/expr.rs b/dhall_syntax/src/core/expr.rs index b293357..6522cb1 100644 --- a/dhall_syntax/src/core/expr.rs +++ b/dhall_syntax/src/core/expr.rs @@ -44,7 +44,7 @@ impl From<NaiveDouble> for f64 { } /// Constants for a pure type system -#[derive(Debug, Copy, Clone, PartialEq, Eq)] +#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord)] pub enum Const { Type, Kind, @@ -99,6 +99,8 @@ pub enum BinOp { BoolEQ, /// `x != y` BoolNE, + /// x === y + Equivalence, } /// Built-ins @@ -175,6 +177,8 @@ pub enum ExprF<SubExpr, Embed> { Let(Label, Option<SubExpr>, SubExpr, SubExpr), /// `x : t` Annot(SubExpr, SubExpr), + /// `assert : t` + Assert(SubExpr), /// Built-in values Builtin(Builtin), // Binary operations diff --git a/dhall_syntax/src/core/visitor.rs b/dhall_syntax/src/core/visitor.rs index 68ad956..18f76d9 100644 --- a/dhall_syntax/src/core/visitor.rs +++ b/dhall_syntax/src/core/visitor.rs @@ -148,6 +148,7 @@ where ), Field(e, l) => Field(v.visit_subexpr(e)?, l.clone()), Projection(e, ls) => Projection(v.visit_subexpr(e)?, ls.clone()), + Assert(e) => Assert(v.visit_subexpr(e)?), Embed(a) => return v.visit_embed_squash(a), }) } diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs index 72dfcdd..9ae6dc8 100644 --- a/dhall_syntax/src/parser.rs +++ b/dhall_syntax/src/parser.rs @@ -311,6 +311,7 @@ fn can_be_shortcutted(rule: Rule) -> bool { | times_expression | equal_expression | not_equal_expression + | equivalent_expression | application_expression | first_application_expression | selector_expression @@ -744,6 +745,7 @@ make_parser! { token_rule!(forall<()>); token_rule!(arrow<()>); token_rule!(merge<()>); + token_rule!(assert<()>); token_rule!(if_<()>); token_rule!(in_<()>); @@ -777,6 +779,9 @@ make_parser! { [merge(()), expression(x), expression(y), expression(z)] => { spanned(span, Merge(x, y, Some(z))) }, + [assert(()), expression(x)] => { + spanned(span, Assert(x)) + }, [expression(e)] => e, )); @@ -875,6 +880,13 @@ make_parser! { rest.fold(first, |acc, e| unspanned(BinOp(o, acc, e))) }, )); + rule!(equivalent_expression<ParsedSubExpr> as expression; children!( + [expression(e)] => e, + [expression(first), expression(rest)..] => { + let o = crate::BinOp::Equivalence; + rest.fold(first, |acc, e| unspanned(BinOp(o, acc, e))) + }, + )); rule!(annotated_expression<ParsedSubExpr> as expression; span; children!( [expression(e)] => e, diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs index 1d6c113..70b224e 100644 --- a/dhall_syntax/src/printer.rs +++ b/dhall_syntax/src/printer.rs @@ -44,6 +44,9 @@ impl<SE: Display + Clone, E: Display> Display for ExprF<SE, E> { Annot(a, b) => { write!(f, "{} : {}", a, b)?; } + Assert(a) => { + write!(f, "assert : {}", a)?; + } ExprF::BinOp(op, a, b) => { write!(f, "{} {} {}", a, op, b)?; } @@ -286,6 +289,7 @@ impl Display for BinOp { ImportAlt => "?", RightBiasedRecordMerge => "⫽", ListAppend => "#", + Equivalence => "≡", }) } } |