diff options
author | Nadrieril | 2019-08-15 13:06:56 +0200 |
---|---|---|
committer | Nadrieril | 2019-08-15 13:06:56 +0200 |
commit | aabca76a62256aa7cad66c2016ed504e49651d5a (patch) | |
tree | 6147764069602e60855ab6bbd3e47718763ceaa3 /dhall | |
parent | ba19f41873fec98bb24ba709f4b76c3f58ca5aaa (diff) |
Remove special closures from Value
Instead construct their values directly
Diffstat (limited to 'dhall')
-rw-r--r-- | dhall/src/core/value.rs | 95 | ||||
-rw-r--r-- | dhall/src/core/var.rs | 6 | ||||
-rw-r--r-- | dhall/src/phase/normalize.rs | 97 |
3 files changed, 62 insertions, 136 deletions
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 845596b..036a20c 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -30,13 +30,6 @@ pub enum Value { Pi(AlphaLabel, TypedThunk, TypedThunk), // Invariant: the evaluation must not be able to progress further. AppliedBuiltin(Builtin, Vec<Thunk>), - /// `λ(x: a) -> Some x` - OptionalSomeClosure(TypedThunk), - /// `λ(x : a) -> λ(xs : List a) -> [ x ] # xs` - /// `λ(xs : List a) -> [ x ] # xs` - ListConsClosure(TypedThunk, Option<Thunk>), - /// `λ(x : Natural) -> x + 1` - NaturalSuccClosure, Var(AlphaVar), Const(Const), @@ -74,47 +67,6 @@ 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::Lam( - 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), @@ -131,27 +83,6 @@ impl Value { } e } - Value::OptionalSomeClosure(n) => { - let a = n.normalize_to_expr_maybe_alpha(alpha); - 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); - 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); - make_expr!(λ(xs : List a) -> [ v ] # var(xs)) - } - Value::NaturalSuccClosure => { - make_expr!(λ(x : Natural) -> 1 + var(x)) - } Value::Pi(x, t, e) => rc(ExprF::Pi( x.to_label_maybe_alpha(alpha), t.normalize_to_expr_maybe_alpha(alpha), @@ -257,8 +188,7 @@ impl Value { pub fn normalize_mut(&mut self) { match self { - Value::NaturalSuccClosure - | Value::Var(_) + Value::Var(_) | Value::Const(_) | Value::BoolLit(_) | Value::NaturalLit(_) @@ -266,7 +196,6 @@ impl Value { | Value::DoubleLit(_) => {} Value::EmptyOptionalLit(tth) - | Value::OptionalSomeClosure(tth) | Value::EmptyListLit(tth) => { tth.normalize_mut(); } @@ -287,12 +216,6 @@ impl Value { x.normalize_mut(); } } - Value::ListConsClosure(t, v) => { - t.normalize_mut(); - for x in v.iter_mut() { - x.normalize_mut(); - } - } Value::NEListLit(elts) => { for x in elts.iter_mut() { x.normalize_mut(); @@ -375,14 +298,6 @@ impl Shift for Value { .map(|v| Ok(v.shift(delta, var)?)) .collect::<Result<_, _>>()?, ), - Value::NaturalSuccClosure => Value::NaturalSuccClosure, - Value::OptionalSomeClosure(tth) => { - Value::OptionalSomeClosure(tth.shift(delta, var)?) - } - Value::ListConsClosure(t, v) => Value::ListConsClosure( - t.shift(delta, var)?, - v.as_ref().map(|v| Ok(v.shift(delta, var)?)).transpose()?, - ), Value::Pi(x, t, e) => Value::Pi( x.clone(), t.shift(delta, var)?, @@ -516,14 +431,6 @@ impl Subst<Typed> for Value { t.subst_shift(var, val), e.subst_shift(&var.under_binder(x), &val.under_binder(x)), ), - Value::NaturalSuccClosure => Value::NaturalSuccClosure, - Value::OptionalSomeClosure(tth) => { - Value::OptionalSomeClosure(tth.subst_shift(var, val)) - } - Value::ListConsClosure(t, v) => Value::ListConsClosure( - t.subst_shift(var, val), - v.as_ref().map(|v| v.subst_shift(var, val)), - ), Value::Pi(x, t, e) => Value::Pi( x.clone(), t.subst_shift(var, val), diff --git a/dhall/src/core/var.rs b/dhall/src/core/var.rs index 35bff80..0faa091 100644 --- a/dhall/src/core/var.rs +++ b/dhall/src/core/var.rs @@ -67,6 +67,12 @@ impl AlphaVar { alpha: None, } } + pub fn from_var_and_alpha(normal: V<Label>, alpha: usize) -> Self { + AlphaVar { + normal, + alpha: Some(V((), alpha)), + } + } } impl AlphaLabel { diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index adbcb02..f11269e 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -1,19 +1,61 @@ use std::collections::HashMap; use dhall_syntax::{ - BinOp, Builtin, ExprF, InterpolatedText, InterpolatedTextContents, + BinOp, Builtin, ExprF, InterpolatedText, InterpolatedTextContents, Label, NaiveDouble, }; use crate::core::context::NormalizationContext; use crate::core::thunk::{Thunk, TypedThunk}; use crate::core::value::Value; -use crate::core::var::Subst; +use crate::core::var::{Shift, Subst}; use crate::phase::{Normalized, NormalizedSubExpr, ResolvedSubExpr, Typed}; pub type InputSubExpr = ResolvedSubExpr; pub type OutputSubExpr = NormalizedSubExpr; +// Ad-hoc macro to help construct closures +macro_rules! make_closure { + (#$var:ident) => { $var.clone() }; + (var($var:ident, $n:expr)) => {{ + let var = crate::core::var::AlphaVar::from_var_and_alpha( + Label::from(stringify!($var)).into(), + $n + ); + Value::Var(var).into_thunk() + }}; + (λ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => { + Value::Lam( + Label::from(stringify!($var)).into(), + TypedThunk::from_thunk_untyped(make_closure!($($ty)*)), + make_closure!($($rest)*), + ).into_thunk() + }; + (Natural) => { Value::from_builtin(Builtin::Natural).into_thunk() }; + (List $($rest:tt)*) => { + Value::from_builtin(Builtin::List) + .app_thunk(make_closure!($($rest)*)) + .into_thunk() + }; + (Some $($rest:tt)*) => { + Value::NEOptionalLit(make_closure!($($rest)*)).into_thunk() + }; + (1 + $($rest:tt)*) => { + Value::PartialExpr(ExprF::BinOp( + dhall_syntax::BinOp::NaturalPlus, + make_closure!($($rest)*), + Thunk::from_value(Value::NaturalLit(1)), + )).into_thunk() + }; + ([ $($head:tt)* ] # $($tail:tt)*) => { + Value::PartialExpr(ExprF::BinOp( + dhall_syntax::BinOp::ListAppend, + Value::NEListLit(vec![make_closure!($($head)*)]).into_thunk(), + make_closure!($($tail)*), + )).into_thunk() + }; +} + #[allow(clippy::cognitive_complexity)] pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value { use dhall_syntax::Builtin::*; @@ -179,10 +221,15 @@ pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value { _ => Ok(( r, f.app_val(Value::from_builtin(List).app_thunk(t.clone())) - .app_val(ListConsClosure( - TypedThunk::from_thunk(t.clone()), - None, - )) + .app_thunk({ + // Move `t` under new `x` variable + let t1 = t.under_binder(Label::from("x")); + make_closure!( + λ(x : #t) -> + λ(xs : List #t1) -> + [ var(x, 1) ] # var(xs, 0) + ) + }) .app_val(EmptyListLit(TypedThunk::from_thunk(t.clone()))), )), }, @@ -214,9 +261,7 @@ pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value { _ => Ok(( r, f.app_val(Value::from_builtin(Optional).app_thunk(t.clone())) - .app_val(OptionalSomeClosure(TypedThunk::from_thunk( - t.clone(), - ))) + .app_thunk(make_closure!(λ(x: #t) -> Some var(x, 0))) .app_val(EmptyOptionalLit(TypedThunk::from_thunk( t.clone(), ))), @@ -240,7 +285,7 @@ pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value { _ => Ok(( r, f.app_val(Value::from_builtin(Natural)) - .app_val(NaturalSuccClosure) + .app_thunk(make_closure!(λ(x : Natural) -> 1 + var(x, 0))) .app_val(NaturalLit(0)), )), }, @@ -284,38 +329,6 @@ pub fn apply_any(f: Thunk, a: Thunk) -> Value { let args = args.iter().cloned().chain(once(a.clone())).collect(); apply_builtin(*b, args) } - Value::OptionalSomeClosure(_) => Value::NEOptionalLit(a), - Value::ListConsClosure(t, None) => { - Value::ListConsClosure(t.clone(), Some(a)) - } - Value::ListConsClosure(_, Some(x)) => { - let a_borrow = a.as_value(); - match &*a_borrow { - Value::EmptyListLit(_) => Value::NEListLit(vec![x.clone()]), - Value::NEListLit(xs) => { - use std::iter::once; - let xs = - once(x.clone()).chain(xs.iter().cloned()).collect(); - Value::NEListLit(xs) - } - _ => { - drop(f_borrow); - drop(a_borrow); - fallback(f, a) - } - } - } - Value::NaturalSuccClosure => { - let a_borrow = a.as_value(); - match &*a_borrow { - Value::NaturalLit(n) => Value::NaturalLit(n + 1), - _ => { - drop(f_borrow); - drop(a_borrow); - fallback(f, a) - } - } - } Value::UnionConstructor(l, kts) => { Value::UnionLit(l.clone(), a, kts.clone()) } |