Improve handling of builtin types in Nir

5 files changed, 66 insertions, 86 deletions

diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
index eb50612..7fbb933 100644
--- a/dhall/src/semantics/builtins.rs
+++ b/dhall/src/semantics/builtins.rs
@@ -14,22 +14,17 @@ use std::convert::TryInto;
 /// A partially applied builtin.
 /// Invariant: the evaluation of the given args must not be able to progress further
 #[derive(Debug, Clone)]
-pub(crate) struct BuiltinClosure<Nir> {
-    pub env: NzEnv,
-    pub b: Builtin,
+pub(crate) struct BuiltinClosure {
+    env: NzEnv,
+    b: Builtin,
     /// Arguments applied to the closure so far.
-    pub args: Vec<Nir>,
+    args: Vec<Nir>,
 }
 
-impl BuiltinClosure<Nir> {
-    pub fn new(b: Builtin, env: NzEnv) -> Self {
-        BuiltinClosure {
-            env,
-            b,
-            args: Vec::new(),
-        }
+impl BuiltinClosure {
+    pub fn new(b: Builtin, env: NzEnv) -> NirKind {
+        apply_builtin(b, Vec::new(), env)
     }
-
     pub fn apply(&self, a: Nir) -> NirKind {
         use std::iter::once;
         let args = self.args.iter().cloned().chain(once(a)).collect();
@@ -272,6 +267,14 @@ fn apply_builtin(b: Builtin, args: Vec<Nir>, env: NzEnv) -> NirKind {
     };
 
     let ret = match (b, args.as_slice()) {
+        (Builtin::Bool, [])
+        | (Builtin::Natural, [])
+        | (Builtin::Integer, [])
+        | (Builtin::Double, [])
+        | (Builtin::Text, []) => Ret::NirKind(BuiltinType(b)),
+        (Builtin::Optional, [t]) => Ret::NirKind(OptionalType(t.clone())),
+        (Builtin::List, [t]) => Ret::NirKind(ListType(t.clone())),
+
         (Builtin::OptionalNone, [t]) => {
             Ret::NirKind(EmptyOptionalLit(t.clone()))
         }
@@ -489,9 +492,9 @@ fn apply_builtin(b: Builtin, args: Vec<Nir>, env: NzEnv) -> NirKind {
     }
 }
 
-impl<Nir: std::cmp::PartialEq> std::cmp::PartialEq for BuiltinClosure<Nir> {
+impl std::cmp::PartialEq for BuiltinClosure {
     fn eq(&self, other: &Self) -> bool {
         self.b == other.b && self.args == other.args
     }
 }
-impl<Nir: std::cmp::Eq> std::cmp::Eq for BuiltinClosure<Nir> {}
+impl std::cmp::Eq for BuiltinClosure {}
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),
                 }
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 6951d62..880ab22 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -5,8 +5,8 @@ use std::collections::HashMap;
 use crate::error::{ErrorBuilder, TypeError, TypeMessage};
 use crate::semantics::merge_maps;
 use crate::semantics::{
-    type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, Nir,
-    NirKind, Tir, TyEnv, Type,
+    type_of_builtin, Binder, Closure, Hir, HirKind, Nir, NirKind, Tir, TyEnv,
+    Type,
 };
 use crate::syntax::{
     BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, NumKind, Span,
@@ -121,11 +121,7 @@ fn type_one_layer(
         ExprKind::EmptyListLit(t) => {
             let t = t.eval_to_type(env)?;
             match t.kind() {
-                NirKind::AppliedBuiltin(BuiltinClosure {
-                    b: Builtin::List,
-                    args,
-                    ..
-                }) if args.len() == 1 => {}
+                NirKind::ListType(..) => {}
                 _ => return span_err("InvalidListType"),
             };
             t
@@ -376,10 +372,7 @@ fn type_one_layer(
         }
         ExprKind::BinOp(BinOp::ListAppend, l, r) => {
             match l.ty().kind() {
-                NirKind::AppliedBuiltin(BuiltinClosure {
-                    b: Builtin::List,
-                    ..
-                }) => {}
+                NirKind::ListType(..) => {}
                 _ => return span_err("BinOpTypeMismatch"),
             }
 
@@ -435,12 +428,7 @@ fn type_one_layer(
             let union_type = union.ty();
             let variants = match union_type.kind() {
                 NirKind::UnionType(kts) => Cow::Borrowed(kts),
-                NirKind::AppliedBuiltin(BuiltinClosure {
-                    b: Builtin::Optional,
-                    args,
-                    ..
-                }) if args.len() == 1 => {
-                    let ty = &args[0];
+                NirKind::OptionalType(ty) => {
                     let mut kts = HashMap::new();
                     kts.insert("None".into(), None);
                     kts.insert("Some".into(), Some(ty.clone()));
@@ -595,11 +583,7 @@ fn type_one_layer(
                 let err_msg = "The type of `toMap x` must be of the form \
                                `List { mapKey : Text, mapValue : T }`";
                 let arg = match annot_val.kind() {
-                    NirKind::AppliedBuiltin(BuiltinClosure {
-                        b: Builtin::List,
-                        args,
-                        ..
-                    }) if args.len() == 1 => &args[0],
+                    NirKind::ListType(t) => t,
                     _ => return span_err(err_msg),
                 };
                 let kts = match arg.kind() {
diff --git a/dhall/src/simple.rs b/dhall/src/simple.rs
index 2e5d3c4..45fa656 100644
--- a/dhall/src/simple.rs
+++ b/dhall/src/simple.rs
@@ -1,6 +1,6 @@
 use std::collections::BTreeMap;
 
-use crate::semantics::{BuiltinClosure, Hir, HirKind, Nir, NirKind};
+use crate::semantics::{Hir, HirKind, Nir, NirKind};
 use crate::syntax::{Builtin, ExprKind, NumKind, Span};
 use crate::Value;
 
@@ -90,30 +90,16 @@ impl SimpleType {
     }
     pub(crate) fn from_nir(nir: &Nir) -> Option<Self> {
         Some(SimpleType::new(match nir.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(Self::from_nir(&args[0])?)
-            }
-            NirKind::AppliedBuiltin(BuiltinClosure {
-                b: Builtin::List,
-                args,
-                ..
-            }) if args.len() == 1 => STyKind::List(Self::from_nir(&args[0])?),
+            NirKind::BuiltinType(b) => match b {
+                Builtin::Bool => STyKind::Bool,
+                Builtin::Natural => STyKind::Natural,
+                Builtin::Integer => STyKind::Integer,
+                Builtin::Double => STyKind::Double,
+                Builtin::Text => STyKind::Text,
+                _ => unreachable!(),
+            },
+            NirKind::OptionalType(t) => STyKind::Optional(Self::from_nir(t)?),
+            NirKind::ListType(t) => STyKind::List(Self::from_nir(t)?),
             NirKind::RecordType(kts) => STyKind::Record(
                 kts.iter()
                     .map(|(k, v)| Some((k.into(), Self::from_nir(v)?)))