diff options
Diffstat (limited to 'dhall')
| -rw-r--r-- | dhall/src/typecheck.rs | 146 |
1 files changed, 50 insertions, 96 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 2916526..00b8b47 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -9,8 +9,8 @@ use dhall_core::core; use dhall_core::core::Builtin::*; use dhall_core::core::Const::*; use dhall_core::core::Expr::*; -use dhall_core::core::{app, pi}; use dhall_core::core::{bx, shift, subst, Expr, Label, V, X}; +use dhall_generator::dhall_expr; use self::TypeMessage::*; @@ -373,34 +373,24 @@ where Ok(ty) } NaturalLit(_) => Ok(Builtin(Natural)), - Builtin(NaturalFold) => Ok(pi( - "_", - Natural, - pi( - "natural", - Const(Type), - pi( - "succ", - pi("_", "natural", "natural"), - pi("zero", "natural", "natural"), - ), - ), + Builtin(NaturalFold) => Ok(dhall_expr!( + Natural -> + forall (natural: Type) -> + forall (succ: natural -> natural) -> + forall (zero: natural) -> + natural )), - Builtin(NaturalBuild) => Ok(pi( - "_", - pi( - "natural", - Const(Type), - pi( - "succ", - pi("_", "natural", "natural"), - pi("zero", "natural", "natural"), - ), - ), - Natural, + Builtin(NaturalBuild) => Ok(dhall_expr!( + (forall (natural: Type) -> + forall (succ: natural -> natural) -> + forall (zero: natural) -> + natural) -> + Natural )), Builtin(NaturalIsZero) | Builtin(NaturalEven) | Builtin(NaturalOdd) => { - Ok(pi("_", Natural, Bool)) + Ok(dhall_expr!( + Natural -> Bool + )) } BinOp(NaturalPlus, ref l, ref r) => { op2_type(ctx, e, Natural, CantAdd, l, r) @@ -443,62 +433,35 @@ where } Ok(App(bx(Builtin(List)), t)) } - Builtin(ListBuild) => Ok(pi( - "a", - Const(Type), - pi( - "_", - pi( - "list", - Const(Type), - pi( - "cons", - pi("_", "a", pi("_", "list", "list")), - pi("nil", "list", "list"), - ), - ), - app(List, "a"), - ), + Builtin(ListBuild) => Ok(dhall_expr!( + forall (a: Type) -> + (forall (list: Type) -> + forall (cons: a -> list -> list) -> + forall (nil: list) -> + list) -> + List a )), - Builtin(ListFold) => Ok(pi( - "a", - Const(Type), - pi( - "_", - app(List, "a"), - pi( - "list", - Const(Type), - pi( - "cons", - pi("_", "a", pi("_", "list", "list")), - pi("nil", "list", "list"), - ), - ), - ), + Builtin(ListFold) => Ok(dhall_expr!( + forall (a: Type) -> + List a -> + forall (list: Type) -> + forall (cons: a -> list -> list) -> + forall (nil: list) -> + list )), Builtin(ListLength) => { - Ok(pi("a", Const(Type), pi("_", app(List, "a"), Natural))) + Ok(dhall_expr!(forall (a: Type) -> List a -> Natural)) } - Builtin(ListHead) | Builtin(ListLast) => Ok(pi( - "a", - Const(Type), - pi("_", app(List, "a"), app(Optional, "a")), - )), - Builtin(ListIndexed) => { - let mut m: BTreeMap<Label, Expr<_, _>> = BTreeMap::new(); - m.insert("index".into(), Builtin(Natural)); - m.insert("value".into(), Var(V("a".into(), 0))); - Ok(pi( - "a", - Const(Type), - pi("_", app(List, Var(V("a".into(), 0))), app(List, Record(m))), - )) + Builtin(ListHead) | Builtin(ListLast) => { + Ok(dhall_expr!(forall (a: Type) -> List a -> Optional a)) } - Builtin(ListReverse) => Ok(pi( - "a", - Const(Type), - pi("_", app(List, "a"), app(List, "a")), + Builtin(ListIndexed) => Ok(dhall_expr!( + forall (a: Type) -> + List a -> + List { index: Natural, value: a } + )), + Builtin(ListReverse) => Ok(dhall_expr!( + forall (a: Type) -> List a -> List a )), OptionalLit(ref t, ref xs) => { let mut iter = xs.iter(); @@ -535,26 +498,17 @@ where } Ok(App(bx(Builtin(Optional)), t)) } - Builtin(OptionalFold) => Ok(pi( - "a", - Const(Type), - pi( - "_", - app(Optional, "a"), - pi( - "optional", - Const(Type), - pi( - "just", - pi("_", "a", "optional"), - pi("nothing", "optional", "optional"), - ), - ), - ), + Builtin(OptionalFold) => Ok(dhall_expr!( + forall (a: Type) -> + Optional a -> + forall (optional: Type) -> + forall (just: a -> optional) -> + forall (nothing: optional) -> + optional + )), + Builtin(List) | Builtin(Optional) => Ok(dhall_expr!( + Type -> Type )), - Builtin(List) | Builtin(Optional) => { - Ok(pi("_", Const(Type), Const(Type))) - } Builtin(Bool) | Builtin(Natural) | Builtin(Integer) | Builtin(Double) | Builtin(Text) => Ok(Const(Type)), Record(ref kts) => { |