diff options
Diffstat (limited to 'dhall/src/core')
| -rw-r--r-- | dhall/src/core/thunk.rs | 4 | ||||
| -rw-r--r-- | dhall/src/core/value.rs | 50 |
2 files changed, 45 insertions, 9 deletions
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), |