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