From aabca76a62256aa7cad66c2016ed504e49651d5a Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 15 Aug 2019 13:06:56 +0200
Subject: Remove special closures from Value

Instead construct their values directly
---
 dhall/src/core/value.rs      | 95 +------------------------------------------
 dhall/src/core/var.rs        |  6 +++
 dhall/src/phase/normalize.rs | 97 +++++++++++++++++++++++++-------------------
 3 files changed, 62 insertions(+), 136 deletions(-)

(limited to 'dhall')

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())
         }
-- 
cgit v1.2.3