summaryrefslogtreecommitdiff
path: root/dhall_syntax/src
diff options
context:
space:
mode:
Diffstat (limited to 'dhall_syntax/src')
-rw-r--r--dhall_syntax/src/core/expr.rs6
-rw-r--r--dhall_syntax/src/core/visitor.rs1
-rw-r--r--dhall_syntax/src/parser.rs12
-rw-r--r--dhall_syntax/src/printer.rs4
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 => "≡",
})
}
}