From 015b76ce47af5b1b31661a934aee13843215c6b0 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 27 Dec 2019 16:48:33 +0000
Subject: Construct T/Build closures in Expr space

---
 dhall/src/semantics/core/var.rs        |   6 --
 dhall/src/semantics/phase/normalize.rs | 113 +++++++++++++++++----------------
 dhall/src/semantics/phase/typecheck.rs |   3 +-
 3 files changed, 58 insertions(+), 64 deletions(-)

(limited to 'dhall/src')

diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs
index 1548713..017a689 100644
--- a/dhall/src/semantics/core/var.rs
+++ b/dhall/src/semantics/core/var.rs
@@ -62,12 +62,6 @@ impl AlphaVar {
             self.normal.clone()
         }
     }
-    pub(crate) fn from_var_and_alpha(normal: V<Label>, alpha: usize) -> Self {
-        AlphaVar {
-            normal,
-            alpha: V((), alpha),
-        }
-    }
 }
 
 impl AlphaLabel {
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index bf0c626..0c581fe 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -3,7 +3,8 @@ use std::convert::TryInto;
 
 use crate::semantics::core::value::Value;
 use crate::semantics::core::value::ValueKind;
-use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
+use crate::semantics::core::var::Subst;
+use crate::semantics::phase::typecheck::{rc, typecheck};
 use crate::semantics::phase::Normalized;
 use crate::syntax;
 use crate::syntax::Const::Type;
@@ -14,60 +15,51 @@ use crate::syntax::{
 
 // Ad-hoc macro to help construct closures
 macro_rules! make_closure {
-    (#$var:ident) => { $var.clone() };
-    (var($var:ident, $n:expr, $($ty:tt)*)) => {{
-        let var = AlphaVar::from_var_and_alpha(
+    (var($var:ident)) => {{
+        rc(ExprKind::Var(syntax::V(
             Label::from(stringify!($var)).into(),
-            $n
-        );
-        ValueKind::Var(var)
-            .into_value_with_type(make_closure!($($ty)*))
+            0
+        )))
     }};
-    // Warning: assumes that $ty, as a dhall value, has type `Type`
     (λ($var:tt : $($ty:tt)*) -> $($body:tt)*) => {{
-        let var: AlphaLabel = Label::from(stringify!($var)).into();
+        let var = Label::from(stringify!($var));
         let ty = make_closure!($($ty)*);
         let body = make_closure!($($body)*);
-        let body_ty = body.get_type_not_sort();
-        let lam_ty = ValueKind::Pi(var.clone(), ty.clone(), body_ty)
-            .into_value_with_type(Value::from_const(Type));
-        ValueKind::Lam(var, ty, body).into_value_with_type(lam_ty)
+        rc(ExprKind::Lam(var, ty, body))
     }};
-    (Natural) => {
-        Value::from_builtin(Builtin::Natural)
+    (Type) => {
+        rc(ExprKind::Const(Type))
     };
-    (List $($rest:tt)*) => {
-        Value::from_builtin(Builtin::List)
-            .app(make_closure!($($rest)*))
+    (Natural) => {
+        rc(ExprKind::Builtin(Builtin::Natural))
     };
-    (Some($($rest:tt)*)) => {{
-        let v = make_closure!($($rest)*);
-        let v_type = v.get_type_not_sort();
-        let opt_v_type = Value::from_builtin(Builtin::Optional).app(v_type);
-        ValueKind::NEOptionalLit(v).into_value_with_type(opt_v_type)
+    (List $($ty:tt)*) => {{
+        let ty = make_closure!($($ty)*);
+        rc(ExprKind::App(
+            rc(ExprKind::Builtin(Builtin::List)),
+            ty
+        ))
     }};
-    (1 + $($rest:tt)*) => {
-        ValueKind::PartialExpr(ExprKind::BinOp(
+    (Some($($v:tt)*)) => {
+        rc(ExprKind::SomeLit(
+            make_closure!($($v)*)
+        ))
+    };
+    (1 + $($v:tt)*) => {
+        rc(ExprKind::BinOp(
             syntax::BinOp::NaturalPlus,
-            make_closure!($($rest)*),
-            Value::from_kind_and_type(
-                ValueKind::NaturalLit(1),
-                make_closure!(Natural)
-            ),
-        )).into_value_with_type(
-            make_closure!(Natural)
-        )
+            make_closure!($($v)*),
+            rc(ExprKind::NaturalLit(1))
+        ))
     };
     ([ $($head:tt)* ] # $($tail:tt)*) => {{
         let head = make_closure!($($head)*);
         let tail = make_closure!($($tail)*);
-        let list_type = tail.get_type_not_sort();
-        ValueKind::PartialExpr(ExprKind::BinOp(
+        rc(ExprKind::BinOp(
             syntax::BinOp::ListAppend,
-            ValueKind::NEListLit(vec![head])
-                .into_value_with_type(list_type.clone()),
+            rc(ExprKind::NEListLit(vec![head])),
             tail,
-        )).into_value_with_type(list_type)
+        ))
     }};
 }
 
@@ -274,16 +266,16 @@ pub(crate) fn apply_builtin(
             let list_t = Value::from_builtin(List).app(t.clone());
             Ret::Value(
                 f.app(list_t.clone())
-                    .app({
-                        // Move `t` under new variables
-                        let t1 = t.under_binder(Label::from("a"));
-                        let t2 = t1.under_binder(Label::from("as"));
-                        make_closure!(
-                            λ(a : #t) ->
-                            λ(as : List #t1) ->
-                            [ var(a, 1, #t2) ] # var(as, 0, List #t2)
-                        )
-                    })
+                    .app(
+                        typecheck(make_closure!(
+                            λ(T : Type) ->
+                            λ(a : var(T)) ->
+                            λ(as : List var(T)) ->
+                            [ var(a) ] # var(as)
+                        ))
+                        .unwrap()
+                        .app(t.clone()),
+                    )
                     .app(EmptyListLit(t.clone()).into_value_with_type(list_t)),
             )
         }
@@ -302,10 +294,15 @@ pub(crate) fn apply_builtin(
             let optional_t = Value::from_builtin(Optional).app(t.clone());
             Ret::Value(
                 f.app(optional_t.clone())
-                    .app({
-                        let t1 = t.under_binder(Label::from("a"));
-                        make_closure!(λ(a: #t) -> Some(var(a, 0, #t1)))
-                    })
+                    .app(
+                        typecheck(make_closure!(
+                            λ(T : Type) ->
+                            λ(a : var(T)) ->
+                            Some(var(a))
+                        ))
+                        .unwrap()
+                        .app(t.clone()),
+                    )
                     .app(
                         EmptyOptionalLit(t.clone())
                             .into_value_with_type(optional_t),
@@ -324,9 +321,13 @@ pub(crate) fn apply_builtin(
         },
         (NaturalBuild, [f]) => Ret::Value(
             f.app(Value::from_builtin(Natural))
-                .app(make_closure!(
-                    λ(x : Natural) -> 1 + var(x, 0, Natural)
-                ))
+                .app(
+                    typecheck(make_closure!(
+                        λ(x : Natural) ->
+                        1 + var(x)
+                    ))
+                    .unwrap(),
+                )
                 .app(
                     NaturalLit(0)
                         .into_value_with_type(Value::from_builtin(Natural)),
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index c8d934d..2e1cc02 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -291,10 +291,9 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
 }
 
 pub(crate) fn builtin_to_value(b: Builtin) -> Value {
-    let ctx = TyCtx::new();
     Value::from_kind_and_type(
         ValueKind::from_builtin(b),
-        type_with(&ctx, type_of_builtin(b)).unwrap(),
+        typecheck(type_of_builtin(b)).unwrap(),
     )
 }
 
-- 
cgit v1.2.3