diff options
| -rw-r--r-- | dhall/src/typecheck.rs | 38 | ||||
| -rw-r--r-- | dhall/tests/common/mod.rs | 2 | ||||
| -rw-r--r-- | dhall/tests/normalization.rs | 1 | ||||
| -rw-r--r-- | dhall/tests/parser.rs | 1 | ||||
| -rw-r--r-- | dhall/tests/typecheck.rs | 1 | ||||
| -rw-r--r-- | dhall_core/src/parser.rs | 2 | ||||
| -rw-r--r-- | dhall_generator/src/quote.rs | 3 |
7 files changed, 29 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; diff --git a/dhall_core/src/parser.rs b/dhall_core/src/parser.rs index 67bcf77..41a2ce7 100644 --- a/dhall_core/src/parser.rs +++ b/dhall_core/src/parser.rs @@ -764,6 +764,7 @@ make_parser! { "False" => BoolLit(false), "Type" => Const(crate::Const::Type), "Kind" => Const(crate::Const::Kind), + "Sort" => Const(crate::Const::Sort), _ => Var(V(l, idx)), } } @@ -777,6 +778,7 @@ make_parser! { "False" => BoolLit(false), "Type" => Const(crate::Const::Type), "Kind" => Const(crate::Const::Kind), + "Sort" => Const(crate::Const::Sort), _ => Var(V(l, 0)), } } diff --git a/dhall_generator/src/quote.rs b/dhall_generator/src/quote.rs index d0c5733..8fce89d 100644 --- a/dhall_generator/src/quote.rs +++ b/dhall_generator/src/quote.rs @@ -63,6 +63,9 @@ where let a = quote_vec(a); quote! { dhall_core::ExprF::App(#f, #a) } } + Annot(x, t) => { + quote! { dhall_core::ExprF::Annot(#x, #t) } + } Const(c) => { let c = quote_const(c); quote! { dhall_core::ExprF::Const(#c) } |