diff options
Diffstat (limited to '')
| -rw-r--r-- | dhall/src/api/mod.rs | 4 | ||||
| -rw-r--r-- | dhall/src/core/thunk.rs | 4 | ||||
| -rw-r--r-- | dhall/src/core/value.rs | 50 | ||||
| -rw-r--r-- | dhall/src/phase/mod.rs | 3 | ||||
| -rw-r--r-- | dhall/src/phase/typecheck.rs | 107 |
5 files changed, 126 insertions, 42 deletions
diff --git a/dhall/src/api/mod.rs b/dhall/src/api/mod.rs index 233d7cf..188b6c0 100644 --- a/dhall/src/api/mod.rs +++ b/dhall/src/api/mod.rs @@ -66,10 +66,6 @@ mod typ { )) } #[doc(hidden)] - pub fn from_normalized_expr(e: NormalizedSubExpr) -> Self { - Type(Typed::from_normalized_expr_untyped(e)) - } - #[doc(hidden)] pub fn make_record_type( kts: impl Iterator<Item = (String, Type)>, ) -> Self { diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index 5bc25f2..f41579c 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -111,10 +111,6 @@ impl Thunk { ThunkInternal::Value(WHNF, v).into_thunk() } - pub fn from_normalized_expr(e: OutputSubExpr) -> Thunk { - Thunk::new(NormalizationContext::new(), e.absurd()) - } - pub fn from_partial_expr(e: ExprF<Thunk, X>) -> Thunk { ThunkInternal::PartialExpr(e).into_thunk() } diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 26568b5..0b68bf6 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -1,6 +1,5 @@ use std::collections::HashMap; -use dhall_proc_macros as dhall; use dhall_syntax::{ rc, Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, NaiveDouble, Natural, X, @@ -75,6 +74,47 @@ impl Value { /// Convert the value to a fully normalized syntactic expression. Also alpha-normalize /// if alpha is `true` pub fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr { + // Ad-hoc macro to help construct the unapplied closures + macro_rules! make_expr { + (Natural) => { rc(ExprF::Builtin(Builtin::Natural)) }; + (var($var:ident)) => { + rc(ExprF::Var(dhall_syntax::V(stringify!($var).into(), 0))) + }; + ($var:ident) => { $var }; + (List $($rest:tt)*) => { + rc(ExprF::App( + rc(ExprF::Builtin(Builtin::List)), + make_expr!($($rest)*) + )) + }; + (Some $($rest:tt)*) => { + rc(ExprF::SomeLit( + make_expr!($($rest)*) + )) + }; + (1 + $($rest:tt)*) => { + rc(ExprF::BinOp( + dhall_syntax::BinOp::NaturalPlus, + rc(ExprF::NaturalLit(1)), + make_expr!($($rest)*) + )) + }; + ([ $($head:tt)* ] # $($tail:tt)*) => { + rc(ExprF::BinOp( + dhall_syntax::BinOp::ListAppend, + rc(ExprF::NEListLit(vec![make_expr!($($head)*)])), + make_expr!($($tail)*) + )) + }; + (λ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => { + rc(ExprF::Pi( + stringify!($var).into(), + make_expr!($($ty)*), + make_expr!($($rest)*) + )) + }; + } + match self { Value::Lam(x, t, e) => rc(ExprF::Lam( x.to_label_maybe_alpha(alpha), @@ -93,24 +133,24 @@ impl Value { } Value::OptionalSomeClosure(n) => { let a = n.normalize_to_expr_maybe_alpha(alpha); - dhall::subexpr!(λ(x: a) -> Some x) + make_expr!(λ(x: a) -> Some var(x)) } Value::ListConsClosure(a, None) => { // Avoid accidental capture of the new `x` variable let a1 = a.under_binder(Label::from("x")); let a1 = a1.normalize_to_expr_maybe_alpha(alpha); let a = a.normalize_to_expr_maybe_alpha(alpha); - dhall::subexpr!(λ(x : a) -> λ(xs : List a1) -> [ x ] # xs) + make_expr!(λ(x : a) -> λ(xs : List a1) -> [ var(x) ] # var(xs)) } Value::ListConsClosure(n, Some(v)) => { // Avoid accidental capture of the new `xs` variable let v = v.under_binder(Label::from("xs")); let v = v.normalize_to_expr_maybe_alpha(alpha); let a = n.normalize_to_expr_maybe_alpha(alpha); - dhall::subexpr!(λ(xs : List a) -> [ v ] # xs) + make_expr!(λ(xs : List a) -> [ v ] # var(xs)) } Value::NaturalSuccClosure => { - dhall::subexpr!(λ(x : Natural) -> x + 1) + make_expr!(λ(x : Natural) -> 1 + var(x)) } Value::Pi(x, t, e) => rc(ExprF::Pi( x.to_label_maybe_alpha(alpha), diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs index 681b7fe..ccedff2 100644 --- a/dhall/src/phase/mod.rs +++ b/dhall/src/phase/mod.rs @@ -127,9 +127,6 @@ impl Typed { pub fn from_value_untyped(v: Value) -> Self { Typed::from_thunk_untyped(Thunk::from_value(v)) } - pub fn from_normalized_expr_untyped(e: NormalizedSubExpr) -> Self { - Typed::from_thunk_untyped(Thunk::from_normalized_expr(e)) - } // TODO: Avoid cloning if possible pub fn to_value(&self) -> Value { diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 297a096..8f5ca8b 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -1,6 +1,5 @@ use std::collections::HashMap; -use dhall_proc_macros as dhall; use dhall_syntax::{ rc, Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, Span, SubExpr, X, @@ -173,41 +172,97 @@ pub fn type_of_const(c: Const) -> Result<Type, TypeError> { } } +// Ad-hoc macro to help construct the types of builtins +macro_rules! make_type { + (Type) => { ExprF::Const(Const::Type) }; + (Bool) => { ExprF::Builtin(Builtin::Bool) }; + (Natural) => { ExprF::Builtin(Builtin::Natural) }; + (Integer) => { ExprF::Builtin(Builtin::Integer) }; + (Double) => { ExprF::Builtin(Builtin::Double) }; + (Text) => { ExprF::Builtin(Builtin::Text) }; + ($var:ident) => { + ExprF::Var(dhall_syntax::V(stringify!($var).into(), 0)) + }; + (Optional $ty:ident) => { + ExprF::App( + rc(ExprF::Builtin(Builtin::Optional)), + rc(make_type!($ty)) + ) + }; + (List $($rest:tt)*) => { + ExprF::App( + rc(ExprF::Builtin(Builtin::List)), + rc(make_type!($($rest)*)) + ) + }; + ({ $($label:ident : $ty:ident),* }) => {{ + let mut kts = dhall_syntax::map::DupTreeMap::new(); + $( + kts.insert( + Label::from(stringify!($label)), + rc(make_type!($ty)), + ); + )* + ExprF::RecordType(kts) + }}; + ($ty:ident -> $($rest:tt)*) => { + ExprF::Pi( + "_".into(), + rc(make_type!($ty)), + rc(make_type!($($rest)*)) + ) + }; + (($($arg:tt)*) -> $($rest:tt)*) => { + ExprF::Pi( + "_".into(), + rc(make_type!($($arg)*)), + rc(make_type!($($rest)*)) + ) + }; + (forall ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => { + ExprF::Pi( + stringify!($var).into(), + rc(make_type!($($ty)*)), + rc(make_type!($($rest)*)) + ) + }; +} + fn type_of_builtin(b: Builtin) -> Expr<X, X> { use dhall_syntax::Builtin::*; match b { - Bool | Natural | Integer | Double | Text => dhall::expr!(Type), - List | Optional => dhall::expr!( + Bool | Natural | Integer | Double | Text => make_type!(Type), + List | Optional => make_type!( Type -> Type ), - NaturalFold => dhall::expr!( + NaturalFold => make_type!( Natural -> forall (natural: Type) -> forall (succ: natural -> natural) -> forall (zero: natural) -> natural ), - NaturalBuild => dhall::expr!( + NaturalBuild => make_type!( (forall (natural: Type) -> forall (succ: natural -> natural) -> forall (zero: natural) -> natural) -> Natural ), - NaturalIsZero | NaturalEven | NaturalOdd => dhall::expr!( + NaturalIsZero | NaturalEven | NaturalOdd => make_type!( Natural -> Bool ), - NaturalToInteger => dhall::expr!(Natural -> Integer), - NaturalShow => dhall::expr!(Natural -> Text), - NaturalSubtract => dhall::expr!(Natural -> Natural -> Natural), + NaturalToInteger => make_type!(Natural -> Integer), + NaturalShow => make_type!(Natural -> Text), + NaturalSubtract => make_type!(Natural -> Natural -> Natural), - IntegerToDouble => dhall::expr!(Integer -> Double), - IntegerShow => dhall::expr!(Integer -> Text), - DoubleShow => dhall::expr!(Double -> Text), - TextShow => dhall::expr!(Text -> Text), + IntegerToDouble => make_type!(Integer -> Double), + IntegerShow => make_type!(Integer -> Text), + DoubleShow => make_type!(Double -> Text), + TextShow => make_type!(Text -> Text), - ListBuild => dhall::expr!( + ListBuild => make_type!( forall (a: Type) -> (forall (list: Type) -> forall (cons: a -> list -> list) -> @@ -215,28 +270,28 @@ fn type_of_builtin(b: Builtin) -> Expr<X, X> { list) -> List a ), - ListFold => dhall::expr!( + ListFold => make_type!( forall (a: Type) -> - List a -> + (List a) -> forall (list: Type) -> forall (cons: a -> list -> list) -> forall (nil: list) -> list ), - ListLength => dhall::expr!(forall (a: Type) -> List a -> Natural), + ListLength => make_type!(forall (a: Type) -> (List a) -> Natural), ListHead | ListLast => { - dhall::expr!(forall (a: Type) -> List a -> Optional a) + make_type!(forall (a: Type) -> (List a) -> Optional a) } - ListIndexed => dhall::expr!( + ListIndexed => make_type!( forall (a: Type) -> - List a -> + (List a) -> List { index: Natural, value: a } ), - ListReverse => dhall::expr!( - forall (a: Type) -> List a -> List a + ListReverse => make_type!( + forall (a: Type) -> (List a) -> List a ), - OptionalBuild => dhall::expr!( + OptionalBuild => make_type!( forall (a: Type) -> (forall (optional: Type) -> forall (just: a -> optional) -> @@ -244,15 +299,15 @@ fn type_of_builtin(b: Builtin) -> Expr<X, X> { optional) -> Optional a ), - OptionalFold => dhall::expr!( + OptionalFold => make_type!( forall (a: Type) -> - Optional a -> + (Optional a) -> forall (optional: Type) -> forall (just: a -> optional) -> forall (nothing: optional) -> optional ), - OptionalNone => dhall::expr!( + OptionalNone => make_type!( forall (a: Type) -> Optional a ), } |