Add support for dependent types

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 => "≡",
         })
     }
 }