From 84796fd247eb1a13fcd092a7cd7ec2d587b261bd Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 8 Mar 2020 17:11:34 +0000
Subject: Add SimpleValue type to facilitate deserialization

---
 dhall/src/semantics/nze/nir.rs | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

(limited to 'dhall/src/semantics/nze')

diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs
index 32ef590..9e3644c 100644
--- a/dhall/src/semantics/nze/nir.rs
+++ b/dhall/src/semantics/nze/nir.rs
@@ -11,6 +11,7 @@ use crate::syntax::{
     Span,
 };
 use crate::{NormalizedExpr, ToExprOptions};
+use crate::{SValKind, SimpleValue};
 
 /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation
 /// automatically. Uses a Rc<RefCell> to share computation.
@@ -142,6 +143,39 @@ impl Nir {
     pub(crate) fn to_expr_tyenv(&self, tyenv: &TyEnv) -> NormalizedExpr {
         self.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv)
     }
+    pub(crate) fn to_simple_value(&self) -> Option<SimpleValue> {
+        Some(SimpleValue::new(match self.kind() {
+            NirKind::Lit(lit) => SValKind::Lit(lit.clone()),
+            NirKind::TextLit(x) => SValKind::Text(
+                x.as_text()
+                    .expect("Normal form should ensure the text is a string"),
+            ),
+            NirKind::EmptyOptionalLit(_) => SValKind::Optional(None),
+            NirKind::NEOptionalLit(x) => {
+                SValKind::Optional(Some(x.to_simple_value()?))
+            }
+            NirKind::EmptyListLit(_) => SValKind::List(vec![]),
+            NirKind::NEListLit(xs) => SValKind::List(
+                xs.iter()
+                    .map(|v| v.to_simple_value())
+                    .collect::<Option<_>>()?,
+            ),
+            NirKind::RecordLit(kvs) => SValKind::Record(
+                kvs.iter()
+                    .map(|(k, v)| Some((k.into(), v.to_simple_value()?)))
+                    .collect::<Option<_>>()?,
+            ),
+            NirKind::UnionLit(field, x, _) => {
+                SValKind::Union(field.into(), Some(x.to_simple_value()?))
+            }
+            NirKind::UnionConstructor(field, ty)
+                if ty.get(field).map(|f| f.is_some()) == Some(false) =>
+            {
+                SValKind::Union(field.into(), None)
+            }
+            _ => return None,
+        }))
+    }
 
     pub(crate) fn normalize(&self) {
         self.0.normalize()
-- 
cgit v1.2.3


From 94850b720b0171444694452027f1baf947b3c18f Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 8 Mar 2020 21:47:26 +0000
Subject: Add SimpleType to mirror SimpleValue

---
 dhall/src/semantics/nze/nir.rs | 48 +++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 47 insertions(+), 1 deletion(-)

(limited to 'dhall/src/semantics/nze')

diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs
index 9e3644c..4615b39 100644
--- a/dhall/src/semantics/nze/nir.rs
+++ b/dhall/src/semantics/nze/nir.rs
@@ -11,7 +11,7 @@ use crate::syntax::{
     Span,
 };
 use crate::{NormalizedExpr, ToExprOptions};
-use crate::{SValKind, SimpleValue};
+use crate::{STyKind, SValKind, SimpleType, SimpleValue};
 
 /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation
 /// automatically. Uses a Rc<RefCell> to share computation.
@@ -176,6 +176,52 @@ impl Nir {
             _ => return None,
         }))
     }
+    pub(crate) fn to_simple_type(&self) -> Option<SimpleType> {
+        Some(SimpleType::new(match self.kind() {
+            NirKind::AppliedBuiltin(BuiltinClosure { b, args, .. })
+                if args.is_empty() =>
+            {
+                match b {
+                    Builtin::Bool => STyKind::Bool,
+                    Builtin::Natural => STyKind::Natural,
+                    Builtin::Integer => STyKind::Integer,
+                    Builtin::Double => STyKind::Double,
+                    Builtin::Text => STyKind::Text,
+                    _ => return None,
+                }
+            }
+            NirKind::AppliedBuiltin(BuiltinClosure {
+                b: Builtin::Optional,
+                args,
+                ..
+            }) if args.len() == 1 => {
+                STyKind::Optional(args[0].to_simple_type()?)
+            }
+            NirKind::AppliedBuiltin(BuiltinClosure {
+                b: Builtin::List,
+                args,
+                ..
+            }) if args.len() == 1 => STyKind::List(args[0].to_simple_type()?),
+            NirKind::RecordType(kts) => STyKind::Record(
+                kts.iter()
+                    .map(|(k, v)| Some((k.into(), v.to_simple_type()?)))
+                    .collect::<Option<_>>()?,
+            ),
+            NirKind::UnionType(kts) => STyKind::Union(
+                kts.iter()
+                    .map(|(k, v)| {
+                        Some((
+                            k.into(),
+                            v.as_ref()
+                                .map(|v| Ok(v.to_simple_type()?))
+                                .transpose()?,
+                        ))
+                    })
+                    .collect::<Option<_>>()?,
+            ),
+            _ => return None,
+        }))
+    }
 
     pub(crate) fn normalize(&self) {
         self.0.normalize()
-- 
cgit v1.2.3


From 2f5c45fd2f712f7befe6f7c92b62dc76d5f77538 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 13 Mar 2020 16:50:49 +0000
Subject: Rename LitKind to NumKind

---
 dhall/src/semantics/nze/nir.rs       | 10 +++---
 dhall/src/semantics/nze/normalize.rs | 70 ++++++++++++++++++------------------
 2 files changed, 40 insertions(+), 40 deletions(-)

(limited to 'dhall/src/semantics/nze')

diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs
index 4615b39..6f482a8 100644
--- a/dhall/src/semantics/nze/nir.rs
+++ b/dhall/src/semantics/nze/nir.rs
@@ -7,7 +7,7 @@ use crate::semantics::{
     BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, Type, Universe, VarEnv,
 };
 use crate::syntax::{
-    BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Label, LitKind,
+    BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Label, NumKind,
     Span,
 };
 use crate::{NormalizedExpr, ToExprOptions};
@@ -75,7 +75,7 @@ pub(crate) enum NirKind {
 
     Var(NzVar),
     Const(Const),
-    Lit(LitKind),
+    Num(NumKind),
     EmptyOptionalLit(Nir),
     NEOptionalLit(Nir),
     // EmptyListLit(t) means `[] : List t`, not `[] : t`
@@ -145,7 +145,7 @@ impl Nir {
     }
     pub(crate) fn to_simple_value(&self) -> Option<SimpleValue> {
         Some(SimpleValue::new(match self.kind() {
-            NirKind::Lit(lit) => SValKind::Lit(lit.clone()),
+            NirKind::Num(lit) => SValKind::Num(lit.clone()),
             NirKind::TextLit(x) => SValKind::Text(
                 x.as_text()
                     .expect("Normal form should ensure the text is a string"),
@@ -268,7 +268,7 @@ impl Nir {
                     closure.to_hir(venv),
                 ),
                 NirKind::Const(c) => ExprKind::Const(*c),
-                NirKind::Lit(l) => ExprKind::Lit(l.clone()),
+                NirKind::Num(l) => ExprKind::Num(l.clone()),
                 NirKind::EmptyOptionalLit(n) => ExprKind::App(
                     Nir::from_builtin(Builtin::OptionalNone).to_hir(venv),
                     n.to_hir(venv),
@@ -366,7 +366,7 @@ impl NirKind {
 
     pub(crate) fn normalize(&self) {
         match self {
-            NirKind::Var(..) | NirKind::Const(_) | NirKind::Lit(_) => {}
+            NirKind::Var(..) | NirKind::Const(_) | NirKind::Num(_) => {}
 
             NirKind::EmptyOptionalLit(tth) | NirKind::EmptyListLit(tth) => {
                 tth.normalize();
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 79d55e8..c5e66a1 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -6,7 +6,7 @@ use crate::semantics::{
     Binder, BuiltinClosure, Closure, Hir, HirKind, Nir, NirKind, TextLit,
 };
 use crate::syntax::{
-    BinOp, Builtin, ExprKind, InterpolatedTextContents, LitKind,
+    BinOp, Builtin, ExprKind, InterpolatedTextContents, NumKind,
 };
 
 pub(crate) fn apply_any(f: Nir, a: Nir) -> NirKind {
@@ -99,40 +99,40 @@ fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option<Ret<'a>> {
         NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
         RightBiasedRecordMerge, TextAppend,
     };
-    use LitKind::{Bool, Natural};
-    use NirKind::{EmptyListLit, Lit, NEListLit, RecordLit, RecordType};
+    use NirKind::{EmptyListLit, NEListLit, Num, RecordLit, RecordType};
+    use NumKind::{Bool, Natural};
 
     Some(match (o, x.kind(), y.kind()) {
-        (BoolAnd, Lit(Bool(true)), _) => Ret::NirRef(y),
-        (BoolAnd, _, Lit(Bool(true))) => Ret::NirRef(x),
-        (BoolAnd, Lit(Bool(false)), _) => Ret::NirKind(Lit(Bool(false))),
-        (BoolAnd, _, Lit(Bool(false))) => Ret::NirKind(Lit(Bool(false))),
+        (BoolAnd, Num(Bool(true)), _) => Ret::NirRef(y),
+        (BoolAnd, _, Num(Bool(true))) => Ret::NirRef(x),
+        (BoolAnd, Num(Bool(false)), _) => Ret::NirKind(Num(Bool(false))),
+        (BoolAnd, _, Num(Bool(false))) => Ret::NirKind(Num(Bool(false))),
         (BoolAnd, _, _) if x == y => Ret::NirRef(x),
-        (BoolOr, Lit(Bool(true)), _) => Ret::NirKind(Lit(Bool(true))),
-        (BoolOr, _, Lit(Bool(true))) => Ret::NirKind(Lit(Bool(true))),
-        (BoolOr, Lit(Bool(false)), _) => Ret::NirRef(y),
-        (BoolOr, _, Lit(Bool(false))) => Ret::NirRef(x),
+        (BoolOr, Num(Bool(true)), _) => Ret::NirKind(Num(Bool(true))),
+        (BoolOr, _, Num(Bool(true))) => Ret::NirKind(Num(Bool(true))),
+        (BoolOr, Num(Bool(false)), _) => Ret::NirRef(y),
+        (BoolOr, _, Num(Bool(false))) => Ret::NirRef(x),
         (BoolOr, _, _) if x == y => Ret::NirRef(x),
-        (BoolEQ, Lit(Bool(true)), _) => Ret::NirRef(y),
-        (BoolEQ, _, Lit(Bool(true))) => Ret::NirRef(x),
-        (BoolEQ, Lit(Bool(x)), Lit(Bool(y))) => Ret::NirKind(Lit(Bool(x == y))),
-        (BoolEQ, _, _) if x == y => Ret::NirKind(Lit(Bool(true))),
-        (BoolNE, Lit(Bool(false)), _) => Ret::NirRef(y),
-        (BoolNE, _, Lit(Bool(false))) => Ret::NirRef(x),
-        (BoolNE, Lit(Bool(x)), Lit(Bool(y))) => Ret::NirKind(Lit(Bool(x != y))),
-        (BoolNE, _, _) if x == y => Ret::NirKind(Lit(Bool(false))),
+        (BoolEQ, Num(Bool(true)), _) => Ret::NirRef(y),
+        (BoolEQ, _, Num(Bool(true))) => Ret::NirRef(x),
+        (BoolEQ, Num(Bool(x)), Num(Bool(y))) => Ret::NirKind(Num(Bool(x == y))),
+        (BoolEQ, _, _) if x == y => Ret::NirKind(Num(Bool(true))),
+        (BoolNE, Num(Bool(false)), _) => Ret::NirRef(y),
+        (BoolNE, _, Num(Bool(false))) => Ret::NirRef(x),
+        (BoolNE, Num(Bool(x)), Num(Bool(y))) => Ret::NirKind(Num(Bool(x != y))),
+        (BoolNE, _, _) if x == y => Ret::NirKind(Num(Bool(false))),
 
-        (NaturalPlus, Lit(Natural(0)), _) => Ret::NirRef(y),
-        (NaturalPlus, _, Lit(Natural(0))) => Ret::NirRef(x),
-        (NaturalPlus, Lit(Natural(x)), Lit(Natural(y))) => {
-            Ret::NirKind(Lit(Natural(x + y)))
+        (NaturalPlus, Num(Natural(0)), _) => Ret::NirRef(y),
+        (NaturalPlus, _, Num(Natural(0))) => Ret::NirRef(x),
+        (NaturalPlus, Num(Natural(x)), Num(Natural(y))) => {
+            Ret::NirKind(Num(Natural(x + y)))
         }
-        (NaturalTimes, Lit(Natural(0)), _) => Ret::NirKind(Lit(Natural(0))),
-        (NaturalTimes, _, Lit(Natural(0))) => Ret::NirKind(Lit(Natural(0))),
-        (NaturalTimes, Lit(Natural(1)), _) => Ret::NirRef(y),
-        (NaturalTimes, _, Lit(Natural(1))) => Ret::NirRef(x),
-        (NaturalTimes, Lit(Natural(x)), Lit(Natural(y))) => {
-            Ret::NirKind(Lit(Natural(x * y)))
+        (NaturalTimes, Num(Natural(0)), _) => Ret::NirKind(Num(Natural(0))),
+        (NaturalTimes, _, Num(Natural(0))) => Ret::NirKind(Num(Natural(0))),
+        (NaturalTimes, Num(Natural(1)), _) => Ret::NirRef(y),
+        (NaturalTimes, _, Num(Natural(1))) => Ret::NirRef(x),
+        (NaturalTimes, Num(Natural(x)), Num(Natural(y))) => {
+            Ret::NirKind(Num(Natural(x * y)))
         }
 
         (ListAppend, EmptyListLit(_), _) => Ret::NirRef(y),
@@ -212,12 +212,12 @@ fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option<Ret<'a>> {
 
 #[allow(clippy::cognitive_complexity)]
 pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
-    use LitKind::Bool;
     use NirKind::{
-        EmptyListLit, EmptyOptionalLit, Lit, NEListLit, NEOptionalLit,
+        EmptyListLit, EmptyOptionalLit, NEListLit, NEOptionalLit, Num,
         PartialExpr, RecordLit, RecordType, UnionConstructor, UnionLit,
         UnionType,
     };
+    use NumKind::Bool;
 
     let ret = match expr {
         ExprKind::Import(..) | ExprKind::Completion(..) => {
@@ -235,7 +235,7 @@ pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
         ExprKind::Builtin(b) => Ret::Nir(Nir::from_builtin_env(b, env)),
         ExprKind::Assert(_) => Ret::Expr(expr),
         ExprKind::App(v, a) => Ret::Nir(v.app(a)),
-        ExprKind::Lit(l) => Ret::NirKind(Lit(l)),
+        ExprKind::Num(l) => Ret::NirKind(Num(l)),
         ExprKind::SomeLit(e) => Ret::NirKind(NEOptionalLit(e)),
         ExprKind::EmptyListLit(t) => {
             let arg = match t.kind() {
@@ -271,12 +271,12 @@ pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
         }
         ExprKind::BoolIf(ref b, ref e1, ref e2) => {
             match b.kind() {
-                Lit(Bool(true)) => Ret::NirRef(e1),
-                Lit(Bool(false)) => Ret::NirRef(e2),
+                Num(Bool(true)) => Ret::NirRef(e1),
+                Num(Bool(false)) => Ret::NirRef(e2),
                 _ => {
                     match (e1.kind(), e2.kind()) {
                         // Simplify `if b then True else False`
-                        (Lit(Bool(true)), Lit(Bool(false))) => Ret::NirRef(b),
+                        (Num(Bool(true)), Num(Bool(false))) => Ret::NirRef(b),
                         _ if e1 == e2 => Ret::NirRef(e1),
                         _ => Ret::Expr(expr),
                     }
-- 
cgit v1.2.3


From 35db1b4b54dba8b0cafe661329e0099dfabd8073 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 13 Mar 2020 17:04:47 +0000
Subject: Remove top-level Expr aliases

---
 dhall/src/semantics/nze/nir.rs | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'dhall/src/semantics/nze')

diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs
index 6f482a8..7365463 100644
--- a/dhall/src/semantics/nze/nir.rs
+++ b/dhall/src/semantics/nze/nir.rs
@@ -7,10 +7,10 @@ use crate::semantics::{
     BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, Type, Universe, VarEnv,
 };
 use crate::syntax::{
-    BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Label, NumKind,
-    Span,
+    BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label,
+    NumKind, Span,
 };
-use crate::{NormalizedExpr, ToExprOptions};
+use crate::ToExprOptions;
 use crate::{STyKind, SValKind, SimpleType, SimpleValue};
 
 /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation
@@ -137,10 +137,10 @@ impl Nir {
         Type::new(self.clone(), u.into())
     }
     /// Converts a value back to the corresponding AST expression.
-    pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
+    pub(crate) fn to_expr(&self, opts: ToExprOptions) -> Expr {
         self.to_hir_noenv().to_expr(opts)
     }
-    pub(crate) fn to_expr_tyenv(&self, tyenv: &TyEnv) -> NormalizedExpr {
+    pub(crate) fn to_expr_tyenv(&self, tyenv: &TyEnv) -> Expr {
         self.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv)
     }
     pub(crate) fn to_simple_value(&self) -> Option<SimpleValue> {
-- 
cgit v1.2.3


From 6a2a407f27b8068769f208383119ac855f629e96 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 13 Mar 2020 20:35:42 +0000
Subject: Move conversion to SimpleVal/Ty to simple module

---
 dhall/src/semantics/nze/nir.rs | 81 ------------------------------------------
 1 file changed, 81 deletions(-)

(limited to 'dhall/src/semantics/nze')

diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs
index 7365463..1148e31 100644
--- a/dhall/src/semantics/nze/nir.rs
+++ b/dhall/src/semantics/nze/nir.rs
@@ -11,7 +11,6 @@ use crate::syntax::{
     NumKind, Span,
 };
 use crate::ToExprOptions;
-use crate::{STyKind, SValKind, SimpleType, SimpleValue};
 
 /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation
 /// automatically. Uses a Rc<RefCell> to share computation.
@@ -143,86 +142,6 @@ impl Nir {
     pub(crate) fn to_expr_tyenv(&self, tyenv: &TyEnv) -> Expr {
         self.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv)
     }
-    pub(crate) fn to_simple_value(&self) -> Option<SimpleValue> {
-        Some(SimpleValue::new(match self.kind() {
-            NirKind::Num(lit) => SValKind::Num(lit.clone()),
-            NirKind::TextLit(x) => SValKind::Text(
-                x.as_text()
-                    .expect("Normal form should ensure the text is a string"),
-            ),
-            NirKind::EmptyOptionalLit(_) => SValKind::Optional(None),
-            NirKind::NEOptionalLit(x) => {
-                SValKind::Optional(Some(x.to_simple_value()?))
-            }
-            NirKind::EmptyListLit(_) => SValKind::List(vec![]),
-            NirKind::NEListLit(xs) => SValKind::List(
-                xs.iter()
-                    .map(|v| v.to_simple_value())
-                    .collect::<Option<_>>()?,
-            ),
-            NirKind::RecordLit(kvs) => SValKind::Record(
-                kvs.iter()
-                    .map(|(k, v)| Some((k.into(), v.to_simple_value()?)))
-                    .collect::<Option<_>>()?,
-            ),
-            NirKind::UnionLit(field, x, _) => {
-                SValKind::Union(field.into(), Some(x.to_simple_value()?))
-            }
-            NirKind::UnionConstructor(field, ty)
-                if ty.get(field).map(|f| f.is_some()) == Some(false) =>
-            {
-                SValKind::Union(field.into(), None)
-            }
-            _ => return None,
-        }))
-    }
-    pub(crate) fn to_simple_type(&self) -> Option<SimpleType> {
-        Some(SimpleType::new(match self.kind() {
-            NirKind::AppliedBuiltin(BuiltinClosure { b, args, .. })
-                if args.is_empty() =>
-            {
-                match b {
-                    Builtin::Bool => STyKind::Bool,
-                    Builtin::Natural => STyKind::Natural,
-                    Builtin::Integer => STyKind::Integer,
-                    Builtin::Double => STyKind::Double,
-                    Builtin::Text => STyKind::Text,
-                    _ => return None,
-                }
-            }
-            NirKind::AppliedBuiltin(BuiltinClosure {
-                b: Builtin::Optional,
-                args,
-                ..
-            }) if args.len() == 1 => {
-                STyKind::Optional(args[0].to_simple_type()?)
-            }
-            NirKind::AppliedBuiltin(BuiltinClosure {
-                b: Builtin::List,
-                args,
-                ..
-            }) if args.len() == 1 => STyKind::List(args[0].to_simple_type()?),
-            NirKind::RecordType(kts) => STyKind::Record(
-                kts.iter()
-                    .map(|(k, v)| Some((k.into(), v.to_simple_type()?)))
-                    .collect::<Option<_>>()?,
-            ),
-            NirKind::UnionType(kts) => STyKind::Union(
-                kts.iter()
-                    .map(|(k, v)| {
-                        Some((
-                            k.into(),
-                            v.as_ref()
-                                .map(|v| Ok(v.to_simple_type()?))
-                                .transpose()?,
-                        ))
-                    })
-                    .collect::<Option<_>>()?,
-            ),
-            _ => return None,
-        }))
-    }
-
     pub(crate) fn normalize(&self) {
         self.0.normalize()
     }
-- 
cgit v1.2.3


From ef3734a3e9381b2e91552089774126f58f560bc3 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 13 Mar 2020 21:21:32 +0000
Subject: Improve handling of builtin types in Nir

---
 dhall/src/semantics/nze/nir.rs       | 35 +++++++++++++++++++++++++++--------
 dhall/src/semantics/nze/normalize.rs | 22 +++++-----------------
 2 files changed, 32 insertions(+), 25 deletions(-)

(limited to 'dhall/src/semantics/nze')

diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs
index 1148e31..e6482fc 100644
--- a/dhall/src/semantics/nze/nir.rs
+++ b/dhall/src/semantics/nze/nir.rs
@@ -70,13 +70,17 @@ pub(crate) enum NirKind {
         annot: Nir,
         closure: Closure,
     },
-    AppliedBuiltin(BuiltinClosure<Nir>),
+    AppliedBuiltin(BuiltinClosure),
 
     Var(NzVar),
     Const(Const),
+    // Must be a number type, Bool or Text
+    BuiltinType(Builtin),
     Num(NumKind),
+    OptionalType(Nir),
     EmptyOptionalLit(Nir),
     NEOptionalLit(Nir),
+    ListType(Nir),
     // EmptyListLit(t) means `[] : List t`, not `[] : t`
     EmptyListLit(Nir),
     NEListLit(Vec<Nir>),
@@ -187,12 +191,21 @@ impl Nir {
                     closure.to_hir(venv),
                 ),
                 NirKind::Const(c) => ExprKind::Const(*c),
+                NirKind::BuiltinType(b) => ExprKind::Builtin(*b),
                 NirKind::Num(l) => ExprKind::Num(l.clone()),
+                NirKind::OptionalType(t) => ExprKind::App(
+                    Nir::from_builtin(Builtin::Optional).to_hir(venv),
+                    t.to_hir(venv),
+                ),
                 NirKind::EmptyOptionalLit(n) => ExprKind::App(
                     Nir::from_builtin(Builtin::OptionalNone).to_hir(venv),
                     n.to_hir(venv),
                 ),
                 NirKind::NEOptionalLit(n) => ExprKind::SomeLit(n.to_hir(venv)),
+                NirKind::ListType(t) => ExprKind::App(
+                    Nir::from_builtin(Builtin::List).to_hir(venv),
+                    t.to_hir(venv),
+                ),
                 NirKind::EmptyListLit(n) => ExprKind::EmptyListLit(Hir::new(
                     HirKind::Expr(ExprKind::App(
                         Nir::from_builtin(Builtin::List).to_hir(venv),
@@ -285,14 +298,20 @@ impl NirKind {
 
     pub(crate) fn normalize(&self) {
         match self {
-            NirKind::Var(..) | NirKind::Const(_) | NirKind::Num(_) => {}
-
-            NirKind::EmptyOptionalLit(tth) | NirKind::EmptyListLit(tth) => {
-                tth.normalize();
+            NirKind::Var(..)
+            | NirKind::Const(_)
+            | NirKind::Num(_)
+            | NirKind::BuiltinType(..) => {}
+
+            NirKind::EmptyOptionalLit(v)
+            | NirKind::EmptyListLit(v)
+            | NirKind::OptionalType(v)
+            | NirKind::ListType(v) => {
+                v.normalize();
             }
 
-            NirKind::NEOptionalLit(th) => {
-                th.normalize();
+            NirKind::NEOptionalLit(v) => {
+                v.normalize();
             }
             NirKind::LamClosure { annot, closure, .. }
             | NirKind::PiClosure { annot, closure, .. } => {
@@ -341,7 +360,7 @@ impl NirKind {
         NirKind::from_builtin_env(b, NzEnv::new())
     }
     pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> NirKind {
-        NirKind::AppliedBuiltin(BuiltinClosure::new(b, env))
+        BuiltinClosure::new(b, env)
     }
 }
 
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index c5e66a1..46d8fb5 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -2,12 +2,8 @@ use itertools::Itertools;
 use std::collections::HashMap;
 
 use crate::semantics::NzEnv;
-use crate::semantics::{
-    Binder, BuiltinClosure, Closure, Hir, HirKind, Nir, NirKind, TextLit,
-};
-use crate::syntax::{
-    BinOp, Builtin, ExprKind, InterpolatedTextContents, NumKind,
-};
+use crate::semantics::{Binder, Closure, Hir, HirKind, Nir, NirKind, TextLit};
+use crate::syntax::{BinOp, ExprKind, InterpolatedTextContents, NumKind};
 
 pub(crate) fn apply_any(f: Nir, a: Nir) -> NirKind {
     match f.kind() {
@@ -239,11 +235,7 @@ pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
         ExprKind::SomeLit(e) => Ret::NirKind(NEOptionalLit(e)),
         ExprKind::EmptyListLit(t) => {
             let arg = match t.kind() {
-                NirKind::AppliedBuiltin(BuiltinClosure {
-                    b: Builtin::List,
-                    args,
-                    ..
-                }) if args.len() == 1 => args[0].clone(),
+                NirKind::ListType(t) => t.clone(),
                 _ => panic!("internal type error"),
             };
             Ret::NirKind(NirKind::EmptyListLit(arg))
@@ -442,12 +434,8 @@ pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
         ExprKind::ToMap(ref v, ref annot) => match v.kind() {
             RecordLit(kvs) if kvs.is_empty() => {
                 match annot.as_ref().map(|v| v.kind()) {
-                    Some(NirKind::AppliedBuiltin(BuiltinClosure {
-                        b: Builtin::List,
-                        args,
-                        ..
-                    })) if args.len() == 1 => {
-                        Ret::NirKind(EmptyListLit(args[0].clone()))
+                    Some(NirKind::ListType(t)) => {
+                        Ret::NirKind(EmptyListLit(t.clone()))
                     }
                     _ => Ret::Expr(expr),
                 }
-- 
cgit v1.2.3


From f4a1a6b8d4de5f83649b2ddd90d65f6e6d76e5e1 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 13 Mar 2020 21:29:08 +0000
Subject: Nir::normalize isn't useful

It pretends to normalize but actually can't normalize under lambdas. The
correct way to normalize a Nir is to convert it to Hir.
---
 dhall/src/semantics/nze/nir.rs | 76 ------------------------------------------
 1 file changed, 76 deletions(-)

(limited to 'dhall/src/semantics/nze')

diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs
index e6482fc..5fccbf1 100644
--- a/dhall/src/semantics/nze/nir.rs
+++ b/dhall/src/semantics/nze/nir.rs
@@ -146,9 +146,6 @@ impl Nir {
     pub(crate) fn to_expr_tyenv(&self, tyenv: &TyEnv) -> Expr {
         self.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv)
     }
-    pub(crate) fn normalize(&self) {
-        self.0.normalize()
-    }
 
     pub(crate) fn app(&self, v: Nir) -> Nir {
         Nir::from_kind(apply_any(self.clone(), v))
@@ -286,9 +283,6 @@ impl NirInternal {
     fn kind(&self) -> &NirKind {
         &self.kind
     }
-    fn normalize(&self) {
-        self.kind().normalize();
-    }
 }
 
 impl NirKind {
@@ -296,66 +290,6 @@ impl NirKind {
         Nir::from_kind(self)
     }
 
-    pub(crate) fn normalize(&self) {
-        match self {
-            NirKind::Var(..)
-            | NirKind::Const(_)
-            | NirKind::Num(_)
-            | NirKind::BuiltinType(..) => {}
-
-            NirKind::EmptyOptionalLit(v)
-            | NirKind::EmptyListLit(v)
-            | NirKind::OptionalType(v)
-            | NirKind::ListType(v) => {
-                v.normalize();
-            }
-
-            NirKind::NEOptionalLit(v) => {
-                v.normalize();
-            }
-            NirKind::LamClosure { annot, closure, .. }
-            | NirKind::PiClosure { annot, closure, .. } => {
-                annot.normalize();
-                closure.normalize();
-            }
-            NirKind::AppliedBuiltin(closure) => closure.normalize(),
-            NirKind::NEListLit(elts) => {
-                for x in elts.iter() {
-                    x.normalize();
-                }
-            }
-            NirKind::RecordLit(kvs) => {
-                for x in kvs.values() {
-                    x.normalize();
-                }
-            }
-            NirKind::RecordType(kvs) => {
-                for x in kvs.values() {
-                    x.normalize();
-                }
-            }
-            NirKind::UnionType(kts) | NirKind::UnionConstructor(_, kts) => {
-                for x in kts.values().flatten() {
-                    x.normalize();
-                }
-            }
-            NirKind::UnionLit(_, v, kts) => {
-                v.normalize();
-                for x in kts.values().flatten() {
-                    x.normalize();
-                }
-            }
-            NirKind::TextLit(tlit) => tlit.normalize(),
-            NirKind::Equivalence(x, y) => {
-                x.normalize();
-                y.normalize();
-            }
-            NirKind::PartialExpr(e) => {
-                e.map_ref(Nir::normalize);
-            }
-        }
-    }
-
     pub(crate) fn from_builtin(b: Builtin) -> NirKind {
         NirKind::from_builtin_env(b, NzEnv::new())
     }
@@ -408,9 +342,6 @@ impl Closure {
         }
     }
 
-    // TODO: somehow normalize the body. Might require to pass an env.
-    pub fn normalize(&self) {}
-
     /// Convert this closure to a Hir expression
     pub fn to_hir(&self, venv: VarEnv) -> Hir {
         self.apply_var(NzVar::new(venv.size()))
@@ -474,13 +405,6 @@ impl TextLit {
     pub fn iter(&self) -> impl Iterator<Item = &InterpolatedTextContents<Nir>> {
         self.0.iter()
     }
-    /// Normalize the contained values. This does not break the invariant because we have already
-    /// ensured that no contained values normalize to a TextLit.
-    pub fn normalize(&self) {
-        for x in self.0.iter() {
-            x.map_ref(Nir::normalize);
-        }
-    }
 }
 
 impl lazy::Eval<NirKind> for Thunk {
-- 
cgit v1.2.3


From 7848c8e8d3147ebe428290558aa6c0efcbf59ee5 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 18 Mar 2020 18:58:51 +0000
Subject: Brutally make all of dhall pub

---
 dhall/src/semantics/nze/env.rs       |  6 +++---
 dhall/src/semantics/nze/mod.rs       |  8 +++----
 dhall/src/semantics/nze/nir.rs       | 42 ++++++++++++++++++------------------
 dhall/src/semantics/nze/normalize.rs | 10 ++++-----
 dhall/src/semantics/nze/var.rs       |  4 ++--
 5 files changed, 35 insertions(+), 35 deletions(-)

(limited to 'dhall/src/semantics/nze')

diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs
index ef2bee6..ec99dbe 100644
--- a/dhall/src/semantics/nze/env.rs
+++ b/dhall/src/semantics/nze/env.rs
@@ -1,7 +1,7 @@
 use crate::semantics::{AlphaVar, Nir, NirKind};
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
-pub(crate) enum NzVar {
+pub enum NzVar {
     /// Reverse-debruijn index: counts number of binders from the bottom of the stack.
     Bound(usize),
     /// Fake fresh variable generated for expression equality checking.
@@ -17,11 +17,11 @@ enum EnvItem<Type> {
 }
 
 #[derive(Debug, Clone)]
-pub(crate) struct ValEnv<Type> {
+pub struct ValEnv<Type> {
     items: Vec<EnvItem<Type>>,
 }
 
-pub(crate) type NzEnv = ValEnv<()>;
+pub type NzEnv = ValEnv<()>;
 
 impl NzVar {
     pub fn new(idx: usize) -> Self {
diff --git a/dhall/src/semantics/nze/mod.rs b/dhall/src/semantics/nze/mod.rs
index 2648339..23022e0 100644
--- a/dhall/src/semantics/nze/mod.rs
+++ b/dhall/src/semantics/nze/mod.rs
@@ -3,7 +3,7 @@ pub mod lazy;
 pub mod nir;
 pub mod normalize;
 pub mod var;
-pub(crate) use env::*;
-pub(crate) use nir::*;
-pub(crate) use normalize::*;
-pub(crate) use var::*;
+pub use env::*;
+pub use nir::*;
+pub use normalize::*;
+pub use var::*;
diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs
index 5fccbf1..e0d227e 100644
--- a/dhall/src/semantics/nze/nir.rs
+++ b/dhall/src/semantics/nze/nir.rs
@@ -19,7 +19,7 @@ use crate::ToExprOptions;
 /// normalize as needed.
 /// Stands for "Normalized intermediate representation"
 #[derive(Clone)]
-pub(crate) struct Nir(Rc<NirInternal>);
+pub struct Nir(Rc<NirInternal>);
 
 #[derive(Debug)]
 struct NirInternal {
@@ -28,7 +28,7 @@ struct NirInternal {
 
 /// An unevaluated subexpression
 #[derive(Debug, Clone)]
-pub(crate) enum Thunk {
+pub enum Thunk {
     /// A completely unnormalized expression.
     Thunk { env: NzEnv, body: Hir },
     /// A partially normalized expression that may need to go through `normalize_one_layer`.
@@ -37,7 +37,7 @@ pub(crate) enum Thunk {
 
 /// An unevaluated subexpression that takes an argument.
 #[derive(Debug, Clone)]
-pub(crate) enum Closure {
+pub enum Closure {
     /// Normal closure
     Closure { env: NzEnv, body: Hir },
     /// Closure that ignores the argument passed
@@ -48,7 +48,7 @@ pub(crate) enum Closure {
 // Invariant: this must not contain interpolations that are themselves TextLits, and contiguous
 // text values must be merged.
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub(crate) struct TextLit(Vec<InterpolatedTextContents<Nir>>);
+pub struct TextLit(Vec<InterpolatedTextContents<Nir>>);
 
 /// This represents a value in Weak Head Normal Form (WHNF). This means that the value is
 /// normalized up to the first constructor, but subexpressions may not be fully normalized.
@@ -58,7 +58,7 @@ pub(crate) struct TextLit(Vec<InterpolatedTextContents<Nir>>);
 /// In particular, this means that once we get a `NirKind`, it can be considered immutable, and
 /// we only need to recursively normalize its sub-`Nir`s to get to the NF.
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub(crate) enum NirKind {
+pub enum NirKind {
     /// Closures
     LamClosure {
         binder: Binder,
@@ -97,34 +97,34 @@ pub(crate) enum NirKind {
 
 impl Nir {
     /// Construct a Nir from a completely unnormalized expression.
-    pub(crate) fn new_thunk(env: NzEnv, hir: Hir) -> Nir {
+    pub fn new_thunk(env: NzEnv, hir: Hir) -> Nir {
         NirInternal::from_thunk(Thunk::new(env, hir)).into_nir()
     }
     /// Construct a Nir from a partially normalized expression that's not in WHNF.
-    pub(crate) fn from_partial_expr(e: ExprKind<Nir>) -> Nir {
+    pub fn from_partial_expr(e: ExprKind<Nir>) -> Nir {
         // TODO: env
         let env = NzEnv::new();
         NirInternal::from_thunk(Thunk::from_partial_expr(env, e)).into_nir()
     }
     /// Make a Nir from a NirKind
-    pub(crate) fn from_kind(v: NirKind) -> Nir {
+    pub fn from_kind(v: NirKind) -> Nir {
         NirInternal::from_whnf(v).into_nir()
     }
-    pub(crate) fn from_const(c: Const) -> Self {
+    pub fn from_const(c: Const) -> Self {
         let v = NirKind::Const(c);
         NirInternal::from_whnf(v).into_nir()
     }
-    pub(crate) fn from_builtin(b: Builtin) -> Self {
+    pub fn from_builtin(b: Builtin) -> Self {
         Self::from_builtin_env(b, &NzEnv::new())
     }
-    pub(crate) fn from_builtin_env(b: Builtin, env: &NzEnv) -> Self {
+    pub fn from_builtin_env(b: Builtin, env: &NzEnv) -> Self {
         Nir::from_kind(NirKind::from_builtin_env(b, env.clone()))
     }
-    pub(crate) fn from_text(txt: impl ToString) -> Self {
+    pub fn from_text(txt: impl ToString) -> Self {
         Nir::from_kind(NirKind::TextLit(TextLit::from_text(txt.to_string())))
     }
 
-    pub(crate) fn as_const(&self) -> Option<Const> {
+    pub fn as_const(&self) -> Option<Const> {
         match &*self.kind() {
             NirKind::Const(c) => Some(*c),
             _ => None,
@@ -132,22 +132,22 @@ impl Nir {
     }
 
     /// This is what you want if you want to pattern-match on the value.
-    pub(crate) fn kind(&self) -> &NirKind {
+    pub fn kind(&self) -> &NirKind {
         self.0.kind()
     }
 
-    pub(crate) fn to_type(&self, u: impl Into<Universe>) -> Type {
+    pub fn to_type(&self, u: impl Into<Universe>) -> Type {
         Type::new(self.clone(), u.into())
     }
     /// Converts a value back to the corresponding AST expression.
-    pub(crate) fn to_expr(&self, opts: ToExprOptions) -> Expr {
+    pub fn to_expr(&self, opts: ToExprOptions) -> Expr {
         self.to_hir_noenv().to_expr(opts)
     }
-    pub(crate) fn to_expr_tyenv(&self, tyenv: &TyEnv) -> Expr {
+    pub fn to_expr_tyenv(&self, tyenv: &TyEnv) -> Expr {
         self.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv)
     }
 
-    pub(crate) fn app(&self, v: Nir) -> Nir {
+    pub fn app(&self, v: Nir) -> Nir {
         Nir::from_kind(apply_any(self.clone(), v))
     }
 
@@ -286,14 +286,14 @@ impl NirInternal {
 }
 
 impl NirKind {
-    pub(crate) fn into_nir(self) -> Nir {
+    pub fn into_nir(self) -> Nir {
         Nir::from_kind(self)
     }
 
-    pub(crate) fn from_builtin(b: Builtin) -> NirKind {
+    pub fn from_builtin(b: Builtin) -> NirKind {
         NirKind::from_builtin_env(b, NzEnv::new())
     }
-    pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> NirKind {
+    pub fn from_builtin_env(b: Builtin, env: NzEnv) -> NirKind {
         BuiltinClosure::new(b, env)
     }
 }
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 46d8fb5..570e106 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -5,7 +5,7 @@ use crate::semantics::NzEnv;
 use crate::semantics::{Binder, Closure, Hir, HirKind, Nir, NirKind, TextLit};
 use crate::syntax::{BinOp, ExprKind, InterpolatedTextContents, NumKind};
 
-pub(crate) fn apply_any(f: Nir, a: Nir) -> NirKind {
+pub fn apply_any(f: Nir, a: Nir) -> NirKind {
     match f.kind() {
         NirKind::LamClosure { closure, .. } => closure.apply(a).kind().clone(),
         NirKind::AppliedBuiltin(closure) => closure.apply(a),
@@ -16,7 +16,7 @@ pub(crate) fn apply_any(f: Nir, a: Nir) -> NirKind {
     }
 }
 
-pub(crate) fn squash_textlit(
+pub fn squash_textlit(
     elts: impl Iterator<Item = InterpolatedTextContents<Nir>>,
 ) -> Vec<InterpolatedTextContents<Nir>> {
     use std::mem::replace;
@@ -54,7 +54,7 @@ pub(crate) fn squash_textlit(
     ret
 }
 
-pub(crate) fn merge_maps<K, V, F>(
+pub fn merge_maps<K, V, F>(
     map1: &HashMap<K, V>,
     map2: &HashMap<K, V>,
     mut f: F,
@@ -207,7 +207,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option<Ret<'a>> {
 }
 
 #[allow(clippy::cognitive_complexity)]
-pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
+pub fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
     use NirKind::{
         EmptyListLit, EmptyOptionalLit, NEListLit, NEOptionalLit, Num,
         PartialExpr, RecordLit, RecordType, UnionConstructor, UnionLit,
@@ -464,7 +464,7 @@ pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
 }
 
 /// Normalize Hir into WHNF
-pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> NirKind {
+pub fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> NirKind {
     match hir.kind() {
         HirKind::Var(var) => env.lookup_val(*var),
         HirKind::Import(hir, _) => normalize_hir_whnf(env, hir),
diff --git a/dhall/src/semantics/nze/var.rs b/dhall/src/semantics/nze/var.rs
index 413c759..302dbb7 100644
--- a/dhall/src/semantics/nze/var.rs
+++ b/dhall/src/semantics/nze/var.rs
@@ -8,10 +8,10 @@ pub struct Binder {
 }
 
 impl Binder {
-    pub(crate) fn new(name: Label) -> Self {
+    pub fn new(name: Label) -> Self {
         Binder { name }
     }
-    pub(crate) fn to_label(&self) -> Label {
+    pub fn to_label(&self) -> Label {
         self.clone().into()
     }
 }
-- 
cgit v1.2.3