summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/typecheck.rs38
-rw-r--r--dhall/tests/common/mod.rs2
-rw-r--r--dhall/tests/normalization.rs1
-rw-r--r--dhall/tests/parser.rs1
-rw-r--r--dhall/tests/typecheck.rs1
5 files changed, 24 insertions, 19 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 3815f9f..5be43cf 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -370,7 +370,9 @@ pub fn type_with(
}
Let(f, mt, r, b) => {
let r = if let Some(t) = mt {
- rc(Annot(SubExpr::clone(r), SubExpr::clone(t)))
+ let r = SubExpr::clone(r);
+ let t = SubExpr::clone(t);
+ dhall::subexpr!(r: t)
} else {
SubExpr::clone(r)
};
@@ -409,8 +411,8 @@ pub fn type_with(
Lam(_, _, _) => unreachable!(),
Pi(_, _, _) => unreachable!(),
Let(_, _, _, _) => unreachable!(),
- Const(Type) => Ok(RetExpr(Const(Kind))),
- Const(Kind) => Ok(RetExpr(Const(Sort))),
+ Const(Type) => Ok(RetExpr(dhall::expr!(Kind))),
+ Const(Kind) => Ok(RetExpr(dhall::expr!(Sort))),
Const(Sort) => Ok(RetType(TYPE_OF_SORT)),
Var(V(x, n)) => match ctx.lookup(&x, n) {
Some(e) => Ok(RetExpr(e.unroll())),
@@ -531,7 +533,7 @@ pub fn type_with(
InvalidFieldType(k.clone(), t.clone()),
)?;
}
- Ok(RetExpr(Const(Type)))
+ Ok(RetExpr(dhall::expr!(Type)))
}
RecordLit(kvs) => {
let kts = kvs
@@ -554,25 +556,25 @@ pub fn type_with(
_ => Err(mkerr(NotARecord(x.clone(), r.clone()))),
},
Builtin(b) => Ok(RetExpr(type_of_builtin(b))),
- BoolLit(_) => Ok(RetExpr(Builtin(Bool))),
- NaturalLit(_) => Ok(RetExpr(Builtin(Natural))),
- IntegerLit(_) => Ok(RetExpr(Builtin(Integer))),
- DoubleLit(_) => Ok(RetExpr(Builtin(Double))),
+ BoolLit(_) => Ok(RetExpr(dhall::expr!(Bool))),
+ NaturalLit(_) => Ok(RetExpr(dhall::expr!(Natural))),
+ IntegerLit(_) => Ok(RetExpr(dhall::expr!(Integer))),
+ DoubleLit(_) => Ok(RetExpr(dhall::expr!(Double))),
// TODO: check type of interpolations
- TextLit(_) => Ok(RetExpr(Builtin(Text))),
+ TextLit(_) => Ok(RetExpr(dhall::expr!(Text))),
BinOp(o, l, r) => {
let t = mktype(
ctx,
- rc(Builtin(match o {
- BoolAnd => Bool,
- BoolOr => Bool,
- BoolEQ => Bool,
- BoolNE => Bool,
- NaturalPlus => Natural,
- NaturalTimes => Natural,
- TextAppend => Text,
+ match o {
+ BoolAnd => dhall::subexpr!(Bool),
+ BoolOr => dhall::subexpr!(Bool),
+ BoolEQ => dhall::subexpr!(Bool),
+ BoolNE => dhall::subexpr!(Bool),
+ NaturalPlus => dhall::subexpr!(Natural),
+ NaturalTimes => dhall::subexpr!(Natural),
+ TextAppend => dhall::subexpr!(Text),
_ => panic!("Unimplemented typecheck case: {:?}", e),
- })),
+ },
)?;
ensure_equal(&l.get_type(), &t, mkerr, || {
diff --git a/dhall/tests/common/mod.rs b/dhall/tests/common/mod.rs
index 3c2fc3c..fc5aa5b 100644
--- a/dhall/tests/common/mod.rs
+++ b/dhall/tests/common/mod.rs
@@ -122,7 +122,7 @@ pub fn run_test(base_path: &str, feature: Feature) {
let expr = rc(read_dhall_file(&expr_file_path).unwrap());
let expected =
rc(read_dhall_file(&expected_file_path).unwrap());
- typecheck::type_of(rc(ExprF::Annot(expr, expected)))
+ typecheck::type_of(dhall::subexpr!(expr: expected))
.unwrap();
})
.unwrap()
diff --git a/dhall/tests/normalization.rs b/dhall/tests/normalization.rs
index 5ecc02f..a36a6ac 100644
--- a/dhall/tests/normalization.rs
+++ b/dhall/tests/normalization.rs
@@ -1,3 +1,4 @@
+#![feature(proc_macro_hygiene)]
#![feature(custom_inner_attributes)]
#![rustfmt::skip]
mod common;
diff --git a/dhall/tests/parser.rs b/dhall/tests/parser.rs
index 0b5e2d6..3969dc9 100644
--- a/dhall/tests/parser.rs
+++ b/dhall/tests/parser.rs
@@ -1,3 +1,4 @@
+#![feature(proc_macro_hygiene)]
#![feature(custom_inner_attributes)]
#![rustfmt::skip]
mod common;
diff --git a/dhall/tests/typecheck.rs b/dhall/tests/typecheck.rs
index 6e05a87..8d72313 100644
--- a/dhall/tests/typecheck.rs
+++ b/dhall/tests/typecheck.rs
@@ -1,3 +1,4 @@
+#![feature(proc_macro_hygiene)]
#![feature(custom_inner_attributes)]
#![rustfmt::skip]
mod common;