From 6bb8e618f66df4a955d800d49b3b6863aabd5b41 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 29 Apr 2019 23:28:16 +0200
Subject: Remove NF/WHNF distinction at runtime

---
 dhall/src/expr.rs      |   2 +-
 dhall/src/normalize.rs | 165 +++++++++++++++++++++----------------------------
 dhall/src/typecheck.rs |  12 ++--
 3 files changed, 79 insertions(+), 100 deletions(-)

(limited to 'dhall')

diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index e7beafa..b2f2bec 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -47,7 +47,7 @@ derive_other_traits!(Typed);
 
 #[derive(Debug, Clone)]
 pub(crate) struct PartiallyNormalized<'a>(
-    pub(crate) crate::normalize::Value<crate::normalize::WHNF>,
+    pub(crate) crate::normalize::Value,
     pub(crate) Option<Type<'static>>,
     pub(crate) PhantomData<&'a ()>,
 );
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index d58ea7a..3b21b86 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -70,12 +70,12 @@ impl<'a> PartiallyNormalized<'a> {
             self.2,
         )
     }
-    pub(crate) fn into_whnf(self) -> Value<WHNF> {
+    pub(crate) fn into_whnf(self) -> Value {
         self.0
     }
 }
 
-fn apply_builtin(b: Builtin, args: Vec<Value<WHNF>>) -> Value<WHNF> {
+fn apply_builtin(b: Builtin, args: Vec<Value>) -> Value {
     use dhall_core::Builtin::*;
     use Value::*;
 
@@ -264,7 +264,7 @@ fn apply_builtin(b: Builtin, args: Vec<Value<WHNF>>) -> Value<WHNF> {
 
 #[derive(Debug, Clone)]
 enum EnvItem {
-    Expr(Value<WHNF>),
+    Expr(Value),
     Skip(V<Label>),
 }
 
@@ -302,7 +302,7 @@ impl NormalizationContext {
     fn new() -> Self {
         NormalizationContext(Rc::new(Context::new()))
     }
-    fn insert(&self, x: &Label, e: Value<WHNF>) -> Self {
+    fn insert(&self, x: &Label, e: Value) -> Self {
         NormalizationContext(Rc::new(
             self.0.insert(x.clone(), EnvItem::Expr(e)),
         ))
@@ -314,7 +314,7 @@ impl NormalizationContext {
                 .insert(x.clone(), EnvItem::Skip(V(x.clone(), 0))),
         ))
     }
-    fn lookup(&self, var: &V<Label>) -> Value<WHNF> {
+    fn lookup(&self, var: &V<Label>) -> Value {
         let V(x, n) = var;
         match self.0.lookup(x, *n) {
             Some(EnvItem::Expr(e)) => e.clone(),
@@ -355,53 +355,41 @@ impl NormalizationContext {
     }
 }
 
+/// A semantic value.
 #[derive(Debug, Clone)]
-pub(crate) struct WHNF;
-#[derive(Debug, Clone)]
-pub(crate) enum NF {}
-
-/// A semantic value. `Form` should be either `WHNF` or `NF`.
-/// `NF` stands for Normal Form and indicates that all subexpressions are normalized.
-/// `WHNF` stands for Weak Head Normal-Form and indicates that subexpressions may not be normalized.
-///
-/// Weak Head Normal-Form means that the expression is normalized as
-/// little as possible, but just enough to know the first constructor of the normal form. This is
-/// identical to normal form for simple types like integers, but for e.g. a record literal
-/// this means knowing just the field names.
-#[derive(Debug, Clone)]
-pub(crate) enum Value<Form> {
+pub(crate) enum Value {
     /// Closures
-    Lam(Label, Thunk<Form>, Thunk<Form>),
-    AppliedBuiltin(Builtin, Vec<Value<Form>>),
+    Lam(Label, Thunk, Thunk),
+    AppliedBuiltin(Builtin, Vec<Value>),
     /// `λ(x: a) -> Some x`
-    OptionalSomeClosure(TypeThunk<Form>),
+    OptionalSomeClosure(TypeThunk),
     /// `λ(x : a) -> λ(xs : List a) -> [ x ] # xs`
     /// `λ(xs : List a) -> [ x ] # xs`
-    ListConsClosure(TypeThunk<Form>, Option<Thunk<Form>>),
+    ListConsClosure(TypeThunk, Option<Thunk>),
     /// `λ(x : Natural) -> x + 1`
     NaturalSuccClosure,
-    Pi(Label, TypeThunk<Form>, TypeThunk<Form>),
+    Pi(Label, TypeThunk, TypeThunk),
 
     Var(V<Label>),
     Const(Const),
     BoolLit(bool),
     NaturalLit(Natural),
     IntegerLit(Integer),
-    EmptyOptionalLit(TypeThunk<Form>),
-    NEOptionalLit(Thunk<Form>),
-    EmptyListLit(TypeThunk<Form>),
-    NEListLit(Vec<Thunk<Form>>),
-    RecordLit(BTreeMap<Label, Thunk<Form>>),
-    RecordType(BTreeMap<Label, TypeThunk<Form>>),
-    UnionType(BTreeMap<Label, Option<TypeThunk<Form>>>),
-    UnionConstructor(Label, BTreeMap<Label, Option<TypeThunk<Form>>>),
-    UnionLit(Label, Thunk<Form>, BTreeMap<Label, Option<TypeThunk<Form>>>),
-    TextLit(Vec<InterpolatedTextContents<Thunk<Form>>>),
+    EmptyOptionalLit(TypeThunk),
+    NEOptionalLit(Thunk),
+    EmptyListLit(TypeThunk),
+    NEListLit(Vec<Thunk>),
+    RecordLit(BTreeMap<Label, Thunk>),
+    RecordType(BTreeMap<Label, TypeThunk>),
+    UnionType(BTreeMap<Label, Option<TypeThunk>>),
+    UnionConstructor(Label, BTreeMap<Label, Option<TypeThunk>>),
+    UnionLit(Label, Thunk, BTreeMap<Label, Option<TypeThunk>>),
+    TextLit(Vec<InterpolatedTextContents<Thunk>>),
     /// This must not contain a value captured by one of the variants above.
     Expr(OutputSubExpr),
 }
 
-impl Value<NF> {
+impl Value {
     /// Convert the value back to a (normalized) syntactic expression
     pub(crate) fn normalize_to_expr(self) -> OutputSubExpr {
         match self {
@@ -493,7 +481,7 @@ impl Value<NF> {
             )),
             Value::TextLit(elts) => {
                 fn normalize_textlit(
-                    elts: Vec<InterpolatedTextContents<Thunk<NF>>>,
+                    elts: Vec<InterpolatedTextContents<Thunk>>,
                 ) -> InterpolatedText<OutputSubExpr> {
                     elts.into_iter()
                         .flat_map(|contents| {
@@ -523,14 +511,8 @@ impl Value<NF> {
             Value::Expr(e) => e,
         }
     }
-}
-
-impl Value<WHNF> {
-    pub(crate) fn normalize_to_expr(self) -> OutputSubExpr {
-        self.normalize().normalize_to_expr()
-    }
 
-    pub(crate) fn normalize(&self) -> Value<NF> {
+    pub(crate) fn normalize(&self) -> Value {
         match self {
             Value::Lam(x, t, e) => {
                 Value::Lam(x.clone(), t.normalize(), e.normalize())
@@ -613,7 +595,7 @@ impl Value<WHNF> {
     }
 
     /// Apply to a value
-    pub(crate) fn app(self, val: Value<WHNF>) -> Value<WHNF> {
+    pub(crate) fn app(self, val: Value) -> Value {
         match (self, val) {
             (Value::Lam(x, _, e), val) => {
                 let val =
@@ -651,7 +633,7 @@ impl Value<WHNF> {
         }
     }
 
-    pub(crate) fn from_builtin(b: Builtin) -> Value<WHNF> {
+    pub(crate) fn from_builtin(b: Builtin) -> Value {
         Value::AppliedBuiltin(b, vec![])
     }
 
@@ -846,41 +828,44 @@ impl Value<WHNF> {
 /// Contains either a (partially) normalized value or a
 /// non-normalized value alongside a normalization context.
 #[derive(Debug, Clone)]
-pub(crate) enum Thunk<Form> {
-    Value(Box<Value<Form>>),
-    Unnormalized(Form, NormalizationContext, InputSubExpr),
+pub(crate) enum Thunk {
+    // Normal form, i.e. completely normalized
+    NF(Box<Value>),
+    // Weak Head Normal Form, i.e. subexpressions may not be normalized
+    WHNF(Box<Value>),
+    Unnormalized(NormalizationContext, InputSubExpr),
 }
 
-impl Thunk<WHNF> {
-    fn new(ctx: NormalizationContext, e: InputSubExpr) -> Thunk<WHNF> {
-        Thunk::Unnormalized(WHNF, ctx, e)
+impl Thunk {
+    fn new(ctx: NormalizationContext, e: InputSubExpr) -> Thunk {
+        Thunk::Unnormalized(ctx, e)
     }
 
-    fn from_whnf(v: Value<WHNF>) -> Thunk<WHNF> {
-        Thunk::Value(Box::new(v))
+    fn from_whnf(v: Value) -> Thunk {
+        Thunk::WHNF(Box::new(v))
     }
 
-    pub(crate) fn normalize_whnf(&self) -> Value<WHNF> {
+    pub(crate) fn normalize_whnf(&self) -> Value {
         match self {
-            Thunk::Value(v) => (**v).clone(),
-            Thunk::Unnormalized(_, ctx, e) => {
+            Thunk::WHNF(v) => (**v).clone(),
+            Thunk::NF(v) => (**v).clone(),
+            Thunk::Unnormalized(ctx, e) => {
                 normalize_whnf(ctx.clone(), e.clone())
             }
         }
     }
 
-    fn normalize(&self) -> Thunk<NF> {
-        Thunk::Value(Box::new(self.normalize_whnf().normalize()))
+    fn normalize(&self) -> Thunk {
+        Thunk::NF(Box::new(self.normalize_whnf().normalize()))
     }
 
     fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         match self {
-            Thunk::Value(v) => Thunk::Value(Box::new(v.shift(delta, var))),
-            Thunk::Unnormalized(marker, ctx, e) => Thunk::Unnormalized(
-                marker.clone(),
-                ctx.shift(delta, var),
-                e.clone(),
-            ),
+            Thunk::WHNF(v) => Thunk::WHNF(Box::new(v.shift(delta, var))),
+            Thunk::NF(v) => Thunk::NF(Box::new(v.shift(delta, var))),
+            Thunk::Unnormalized(ctx, e) => {
+                Thunk::Unnormalized(ctx.shift(delta, var), e.clone())
+            }
         }
     }
 
@@ -890,50 +875,49 @@ impl Thunk<WHNF> {
         val: &PartiallyNormalized<'static>,
     ) -> Self {
         match self {
-            Thunk::Value(v) => Thunk::Value(Box::new(v.subst_shift(var, val))),
-            Thunk::Unnormalized(marker, ctx, e) => Thunk::Unnormalized(
-                marker.clone(),
-                ctx.subst_shift(var, val),
-                e.clone(),
-            ),
+            Thunk::WHNF(v) => Thunk::WHNF(Box::new(v.subst_shift(var, val))),
+            Thunk::NF(v) => Thunk::NF(Box::new(v.subst_shift(var, val))),
+            Thunk::Unnormalized(ctx, e) => {
+                Thunk::Unnormalized(ctx.subst_shift(var, val), e.clone())
+            }
         }
     }
-}
 
-impl Thunk<NF> {
-    pub(crate) fn to_nf(&self) -> Value<NF> {
+    pub(crate) fn to_nf(&self) -> Value {
         match self {
-            Thunk::Value(v) => (**v).clone(),
-            Thunk::Unnormalized(m, _, _) => match *m {},
+            Thunk::NF(v) => (**v).clone(),
+            Thunk::WHNF(_) | Thunk::Unnormalized(_, _) => {
+                self.normalize_whnf().normalize()
+            }
         }
     }
 }
 
 /// A thunk in type position.
 #[derive(Debug, Clone)]
-pub(crate) enum TypeThunk<Form> {
-    Thunk(Thunk<Form>),
+pub(crate) enum TypeThunk {
+    Thunk(Thunk),
     Type(Type<'static>),
 }
 
-impl TypeThunk<WHNF> {
-    fn new(ctx: NormalizationContext, e: InputSubExpr) -> TypeThunk<WHNF> {
+impl TypeThunk {
+    fn new(ctx: NormalizationContext, e: InputSubExpr) -> TypeThunk {
         TypeThunk::from_thunk(Thunk::new(ctx, e))
     }
 
-    fn from_whnf(v: Value<WHNF>) -> TypeThunk<WHNF> {
+    fn from_whnf(v: Value) -> TypeThunk {
         TypeThunk::from_thunk(Thunk::from_whnf(v))
     }
 
-    fn from_thunk(th: Thunk<WHNF>) -> TypeThunk<WHNF> {
+    fn from_thunk(th: Thunk) -> TypeThunk {
         TypeThunk::Thunk(th)
     }
 
-    pub(crate) fn from_type(t: Type<'static>) -> TypeThunk<WHNF> {
+    pub(crate) fn from_type(t: Type<'static>) -> TypeThunk {
         TypeThunk::Type(t)
     }
 
-    fn normalize(&self) -> TypeThunk<NF> {
+    fn normalize(&self) -> TypeThunk {
         match self {
             TypeThunk::Thunk(th) => TypeThunk::Thunk(th.normalize()),
             TypeThunk::Type(t) => TypeThunk::Type(t.clone()),
@@ -957,10 +941,8 @@ impl TypeThunk<WHNF> {
             TypeThunk::Type(t) => TypeThunk::Type(t.subst_shift(var, val)),
         }
     }
-}
 
-impl TypeThunk<NF> {
-    pub(crate) fn to_nf(&self) -> Value<NF> {
+    pub(crate) fn to_nf(&self) -> Value {
         match self {
             TypeThunk::Thunk(th) => th.to_nf(),
             // TODO: let's hope for the best with the unwrap
@@ -975,10 +957,7 @@ impl TypeThunk<NF> {
 }
 
 /// Reduces the imput expression to Value. See doc on `Value` for details.
-fn normalize_whnf(
-    ctx: NormalizationContext,
-    expr: InputSubExpr,
-) -> Value<WHNF> {
+fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> Value {
     match expr.as_ref() {
         ExprF::Var(v) => ctx.lookup(&v),
         ExprF::Annot(x, _) => normalize_whnf(ctx, x.clone()),
@@ -1074,7 +1053,7 @@ fn normalize_whnf(
         }
         expr => {
             // Recursively normalize subexpressions
-            let expr: ExprF<Value<WHNF>, Label, X, X> = expr
+            let expr: ExprF<Value, Label, X, X> = expr
                 .map_ref_with_special_handling_of_binders(
                     |e| normalize_whnf(ctx.clone(), e.clone()),
                     |x, e| normalize_whnf(ctx.skip(x), e.clone()),
@@ -1089,7 +1068,7 @@ fn normalize_whnf(
 }
 
 /// When all sub-expressions have been (partially) normalized, eval the remaining toplevel layer.
-fn normalize_last_layer(expr: ExprF<Value<WHNF>, Label, X, X>) -> Value<WHNF> {
+fn normalize_last_layer(expr: ExprF<Value, Label, X, X>) -> Value {
     use dhall_core::BinOp::*;
     use Value::*;
 
@@ -1173,7 +1152,7 @@ fn normalize_last_layer(expr: ExprF<Value<WHNF>, Label, X, X>) -> Value<WHNF> {
             Expr(rc(ExprF::Merge(
                 RecordLit(handlers).normalize_to_expr(),
                 e.normalize_to_expr(),
-                t.map(<Value<WHNF>>::normalize_to_expr),
+                t.map(<Value>::normalize_to_expr),
             )))
         }
         // Couldn't do anything useful, so just normalize subexpressions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 4f0dcd9..38da955 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -6,7 +6,7 @@ use std::fmt;
 use std::marker::PhantomData;
 
 use crate::expr::*;
-use crate::normalize::{TypeThunk, Value, WHNF};
+use crate::normalize::{TypeThunk, Value};
 use crate::traits::DynamicType;
 use dhall_core;
 use dhall_core::context::Context;
@@ -99,7 +99,7 @@ impl<'a> Type<'a> {
     pub(crate) fn into_normalized(self) -> Result<Normalized<'a>, TypeError> {
         self.0.into_normalized()
     }
-    fn normalize_whnf(self) -> Result<Value<WHNF>, TypeError> {
+    fn normalize_whnf(self) -> Result<Value, TypeError> {
         self.0.normalize_whnf()
     }
     pub(crate) fn partially_normalize(
@@ -110,7 +110,7 @@ impl<'a> Type<'a> {
     fn internal(&self) -> &TypeInternal<'a> {
         &self.0
     }
-    fn internal_whnf(&self) -> Option<&Value<WHNF>> {
+    fn internal_whnf(&self) -> Option<&Value> {
         self.0.whnf()
     }
     pub(crate) fn shift0(&self, delta: isize, label: &Label) -> Self {
@@ -143,7 +143,7 @@ impl Type<'static> {
     }
 }
 
-impl TypeThunk<WHNF> {
+impl TypeThunk {
     fn normalize_to_type(
         self,
         ctx: &TypecheckContext,
@@ -178,7 +178,7 @@ impl<'a> TypeInternal<'a> {
     pub(crate) fn into_normalized(self) -> Result<Normalized<'a>, TypeError> {
         Ok(self.partially_normalize()?.normalize())
     }
-    fn normalize_whnf(self) -> Result<Value<WHNF>, TypeError> {
+    fn normalize_whnf(self) -> Result<Value, TypeError> {
         Ok(self.partially_normalize()?.into_whnf())
     }
     fn partially_normalize(self) -> Result<PartiallyNormalized<'a>, TypeError> {
@@ -193,7 +193,7 @@ impl<'a> TypeInternal<'a> {
             }
         })
     }
-    fn whnf(&self) -> Option<&Value<WHNF>> {
+    fn whnf(&self) -> Option<&Value> {
         match self {
             TypeInternal::PNzed(e) => Some(&e.0),
             _ => None,
-- 
cgit v1.2.3