Rename Value to Nir

3 files changed, 58 insertions, 62 deletions

diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index f290c02..17b3cfe 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -1,4 +1,4 @@
-use crate::semantics::{AlphaVar, NameEnv, NzEnv, NzVar, Type, ValEnv, Value};
+use crate::semantics::{AlphaVar, NameEnv, Nir, NzEnv, NzVar, Type, ValEnv};
 use crate::syntax::Label;
 
 /// Environment for indexing variables.
@@ -61,7 +61,7 @@ impl TyEnv {
             items: self.items.insert_type(ty),
         }
     }
-    pub fn insert_value(&self, x: &Label, e: Value, ty: Type) -> Self {
+    pub fn insert_value(&self, x: &Label, e: Nir, ty: Type) -> Self {
         TyEnv {
             names: self.names.insert(x),
             items: self.items.insert_value(e, ty),
diff --git a/dhall/src/semantics/tck/tir.rs b/dhall/src/semantics/tck/tir.rs
index 800d1b7..908bf8f 100644
--- a/dhall/src/semantics/tck/tir.rs
+++ b/dhall/src/semantics/tck/tir.rs
@@ -1,5 +1,5 @@
 use crate::error::{ErrorBuilder, TypeError};
-use crate::semantics::{mkerr, Hir, NzEnv, TyEnv, Value, ValueKind, VarEnv};
+use crate::semantics::{mkerr, Hir, Nir, NirKind, NzEnv, TyEnv, VarEnv};
 use crate::syntax::{Builtin, Const, Span};
 use crate::{NormalizedExpr, ToExprOptions};
 
@@ -10,7 +10,7 @@ pub(crate) struct Universe(u8);
 /// An expression representing a type
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub(crate) struct Type {
-    val: Value,
+    val: Nir,
     univ: Universe,
 }
 
@@ -44,7 +44,7 @@ impl Universe {
 }
 
 impl Type {
-    pub fn new(val: Value, univ: Universe) -> Self {
+    pub fn new(val: Nir, univ: Universe) -> Self {
         Type { val, univ }
     }
     /// Creates a new Type and infers its universe by re-typechecking its value.
@@ -52,7 +52,7 @@ impl Type {
     /// PiClosure.
     pub fn new_infer_universe(
         env: &TyEnv,
-        val: Value,
+        val: Nir,
     ) -> Result<Self, TypeError> {
         let c = val.to_hir(env.as_varenv()).typecheck(env)?.ty().as_const();
         let u = match c {
@@ -65,7 +65,7 @@ impl Type {
         Ok(Type::new(val, u))
     }
     pub fn from_const(c: Const) -> Self {
-        Self::new(Value::from_const(c), c.to_universe().next())
+        Self::new(Nir::from_const(c), c.to_universe().next())
     }
     pub fn from_builtin(b: Builtin) -> Self {
         use Builtin::*;
@@ -74,7 +74,7 @@ impl Type {
             _ => unreachable!("this builtin is not a type: {}", b),
         }
 
-        Self::new(Value::from_builtin(b), Universe::from_const(Const::Type))
+        Self::new(Nir::from_builtin(b), Universe::from_const(Const::Type))
     }
 
     /// Get the type of this type
@@ -82,19 +82,19 @@ impl Type {
         self.univ
     }
 
-    pub fn to_value(&self) -> Value {
+    pub fn to_nir(&self) -> Nir {
         self.val.clone()
     }
-    pub fn as_value(&self) -> &Value {
+    pub fn as_nir(&self) -> &Nir {
         &self.val
     }
-    pub fn into_value(self) -> Value {
+    pub fn into_nir(self) -> Nir {
         self.val
     }
     pub fn as_const(&self) -> Option<Const> {
         self.val.as_const()
     }
-    pub fn kind(&self) -> &ValueKind {
+    pub fn kind(&self) -> &NirKind {
         self.val.kind()
     }
 
@@ -136,7 +136,7 @@ impl Tir {
     }
 
     /// Eval the Tir. It will actually get evaluated only as needed on demand.
-    pub fn eval(&self, env: impl Into<NzEnv>) -> Value {
+    pub fn eval(&self, env: impl Into<NzEnv>) -> Nir {
         self.as_hir().eval(env.into())
     }
     pub fn ensure_is_type(&self, env: &TyEnv) -> Result<(), TypeError> {
@@ -175,11 +175,11 @@ impl Tir {
     }
     /// Eval a closed Tir (i.e. without free variables). It will actually get evaluated only as
     /// needed on demand.
-    pub fn eval_closed_expr(&self) -> Value {
+    pub fn eval_closed_expr(&self) -> Nir {
         self.eval(NzEnv::new())
     }
     /// Eval a closed Tir fully and recursively;
-    pub fn rec_eval_closed_expr(&self) -> Value {
+    pub fn rec_eval_closed_expr(&self) -> Nir {
         let val = self.eval_closed_expr();
         val.normalize();
         val
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 7bf15af..42a9165 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, Tir, TyEnv,
-    Type, Value, ValueKind,
+    type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, Nir,
+    NirKind, Tir, TyEnv, Type,
 };
 use crate::syntax::{
     BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, LitKind, Span,
@@ -15,11 +15,11 @@ use crate::syntax::{
 fn check_rectymerge(
     span: &Span,
     env: &TyEnv,
-    x: Value,
-    y: Value,
+    x: Nir,
+    y: Nir,
 ) -> Result<(), TypeError> {
     let kts_x = match x.kind() {
-        ValueKind::RecordType(kts) => kts,
+        NirKind::RecordType(kts) => kts,
         _ => {
             return mk_span_err(
                 span.clone(),
@@ -28,7 +28,7 @@ fn check_rectymerge(
         }
     };
     let kts_y = match y.kind() {
-        ValueKind::RecordType(kts) => kts,
+        NirKind::RecordType(kts) => kts,
         _ => {
             return mk_span_err(
                 span.clone(),
@@ -118,7 +118,7 @@ fn type_one_layer(
         ExprKind::EmptyListLit(t) => {
             let t = t.eval_to_type(env)?;
             match t.kind() {
-                ValueKind::AppliedBuiltin(BuiltinClosure {
+                NirKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::List,
                     args,
                     ..
@@ -139,18 +139,16 @@ fn type_one_layer(
                 return span_err("InvalidListType");
             }
 
-            let t = x.ty().to_value();
-            Value::from_builtin(Builtin::List)
-                .app(t)
-                .to_type(Const::Type)
+            let t = x.ty().to_nir();
+            Nir::from_builtin(Builtin::List).app(t).to_type(Const::Type)
         }
         ExprKind::SomeLit(x) => {
             if x.ty().ty().as_const() != Some(Const::Type) {
                 return span_err("InvalidOptionalType");
             }
 
-            let t = x.ty().to_value();
-            Value::from_builtin(Builtin::Optional)
+            let t = x.ty().to_nir();
+            Nir::from_builtin(Builtin::Optional)
                 .app(t)
                 .to_type(Const::Type)
         }
@@ -165,7 +163,7 @@ fn type_one_layer(
                     Entry::Occupied(_) => {
                         return span_err("RecordTypeDuplicateField")
                     }
-                    Entry::Vacant(e) => e.insert(v.ty().to_value()),
+                    Entry::Vacant(e) => e.insert(v.ty().to_nir()),
                 };
 
                 // Check that the fields have a valid kind
@@ -175,7 +173,7 @@ fn type_one_layer(
                 }
             }
 
-            Value::from_kind(ValueKind::RecordType(kts)).to_type(k)
+            Nir::from_kind(NirKind::RecordType(kts)).to_type(k)
         }
         ExprKind::RecordType(kts) => {
             use std::collections::hash_map::Entry;
@@ -230,21 +228,21 @@ fn type_one_layer(
         }
         ExprKind::Field(scrut, x) => {
             match scrut.ty().kind() {
-                ValueKind::RecordType(kts) => match kts.get(&x) {
+                NirKind::RecordType(kts) => match kts.get(&x) {
                     Some(val) => Type::new_infer_universe(env, val.clone())?,
                     None => return span_err("MissingRecordField"),
                 },
-                ValueKind::Const(_) => {
+                NirKind::Const(_) => {
                     let scrut = scrut.eval_to_type(env)?;
                     match scrut.kind() {
-                        ValueKind::UnionType(kts) => match kts.get(x) {
+                        NirKind::UnionType(kts) => match kts.get(x) {
                             // Constructor has type T -> < x: T, ... >
                             Some(Some(ty)) => {
-                                Value::from_kind(ValueKind::PiClosure {
+                                Nir::from_kind(NirKind::PiClosure {
                                     binder: Binder::new(x.clone()),
                                     annot: ty.clone(),
                                     closure: Closure::new_constant(
-                                        scrut.to_value(),
+                                        scrut.to_nir(),
                                     ),
                                 })
                                 .to_type(scrut.ty())
@@ -261,10 +259,8 @@ fn type_one_layer(
         ExprKind::Assert(t) => {
             let t = t.eval_to_type(env)?;
             match t.kind() {
-                ValueKind::Equivalence(x, y) if x == y => {}
-                ValueKind::Equivalence(..) => {
-                    return span_err("AssertMismatch")
-                }
+                NirKind::Equivalence(x, y) if x == y => {}
+                NirKind::Equivalence(..) => return span_err("AssertMismatch"),
                 _ => return span_err("AssertMustTakeEquivalence"),
             }
             t
@@ -272,8 +268,8 @@ fn type_one_layer(
         ExprKind::App(f, arg) => {
             match f.ty().kind() {
                 // TODO: store Type in closure
-                ValueKind::PiClosure { annot, closure, .. } => {
-                    if arg.ty().as_value() != annot {
+                NirKind::PiClosure { annot, closure, .. } => {
+                    if arg.ty().as_nir() != annot {
                         return mkerr(
                             ErrorBuilder::new(format!(
                                 "wrong type of function argument"
@@ -318,7 +314,7 @@ fn type_one_layer(
             }
         }
         ExprKind::BoolIf(x, y, z) => {
-            if *x.ty().kind() != ValueKind::from_builtin(Builtin::Bool) {
+            if *x.ty().kind() != NirKind::from_builtin(Builtin::Bool) {
                 return span_err("InvalidPredicate");
             }
             if y.ty().ty().as_const() != Some(Const::Type) {
@@ -336,12 +332,12 @@ fn type_one_layer(
 
             // Extract the LHS record type
             let kts_x = match x_type.kind() {
-                ValueKind::RecordType(kts) => kts,
+                NirKind::RecordType(kts) => kts,
                 _ => return span_err("MustCombineRecord"),
             };
             // Extract the RHS record type
             let kts_y = match y_type.kind() {
-                ValueKind::RecordType(kts) => kts,
+                NirKind::RecordType(kts) => kts,
                 _ => return span_err("MustCombineRecord"),
             };
 
@@ -352,10 +348,10 @@ fn type_one_layer(
             })?;
 
             let u = max(x.ty().ty(), y.ty().ty());
-            Value::from_kind(ValueKind::RecordType(kts)).to_type(u)
+            Nir::from_kind(NirKind::RecordType(kts)).to_type(u)
         }
         ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
-            check_rectymerge(&span, env, x.ty().to_value(), y.ty().to_value())?;
+            check_rectymerge(&span, env, x.ty().to_nir(), y.ty().to_nir())?;
 
             let hir = Hir::new(
                 HirKind::Expr(ExprKind::BinOp(
@@ -379,7 +375,7 @@ fn type_one_layer(
         }
         ExprKind::BinOp(BinOp::ListAppend, l, r) => {
             match l.ty().kind() {
-                ValueKind::AppliedBuiltin(BuiltinClosure {
+                NirKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::List,
                     ..
                 }) => {}
@@ -431,14 +427,14 @@ fn type_one_layer(
         ExprKind::Merge(record, union, type_annot) => {
             let record_type = record.ty();
             let handlers = match record_type.kind() {
-                ValueKind::RecordType(kts) => kts,
+                NirKind::RecordType(kts) => kts,
                 _ => return span_err("Merge1ArgMustBeRecord"),
             };
 
             let union_type = union.ty();
             let variants = match union_type.kind() {
-                ValueKind::UnionType(kts) => Cow::Borrowed(kts),
-                ValueKind::AppliedBuiltin(BuiltinClosure {
+                NirKind::UnionType(kts) => Cow::Borrowed(kts),
+                NirKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::Optional,
                     args,
                     ..
@@ -457,7 +453,7 @@ fn type_one_layer(
                 let handler_return_type: Type = match variants.get(x) {
                     // Union alternative with type
                     Some(Some(variant_type)) => match handler_type.kind() {
-                        ValueKind::PiClosure { closure, annot, .. } => {
+                        NirKind::PiClosure { closure, annot, .. } => {
                             if variant_type != annot {
                                 return mkerr(
                                     ErrorBuilder::new(format!(
@@ -578,7 +574,7 @@ fn type_one_layer(
             }
             let record_t = record.ty();
             let kts = match record_t.kind() {
-                ValueKind::RecordType(kts) => kts,
+                NirKind::RecordType(kts) => kts,
                 _ => {
                     return span_err("The argument to `toMap` must be a record")
                 }
@@ -598,7 +594,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() {
-                    ValueKind::AppliedBuiltin(BuiltinClosure {
+                    NirKind::AppliedBuiltin(BuiltinClosure {
                         b: Builtin::List,
                         args,
                         ..
@@ -606,14 +602,14 @@ fn type_one_layer(
                     _ => return span_err(err_msg),
                 };
                 let kts = match arg.kind() {
-                    ValueKind::RecordType(kts) => kts,
+                    NirKind::RecordType(kts) => kts,
                     _ => return span_err(err_msg),
                 };
                 if kts.len() != 2 {
                     return span_err(err_msg);
                 }
                 match kts.get(&"mapKey".into()) {
-                    Some(t) if *t == Value::from_builtin(Builtin::Text) => {}
+                    Some(t) if *t == Nir::from_builtin(Builtin::Text) => {}
                     _ => return span_err(err_msg),
                 }
                 match kts.get(&"mapValue".into()) {
@@ -632,10 +628,10 @@ fn type_one_layer(
                 }
 
                 let mut kts = HashMap::new();
-                kts.insert("mapKey".into(), Value::from_builtin(Builtin::Text));
+                kts.insert("mapKey".into(), Nir::from_builtin(Builtin::Text));
                 kts.insert("mapValue".into(), entry_type);
-                let output_type: Type = Value::from_builtin(Builtin::List)
-                    .app(Value::from_kind(ValueKind::RecordType(kts)))
+                let output_type: Type = Nir::from_builtin(Builtin::List)
+                    .app(Nir::from_kind(NirKind::RecordType(kts)))
                     .to_type(Const::Type);
                 if let Some(annot) = annot {
                     let annot_val = annot.eval_to_type(env)?;
@@ -649,7 +645,7 @@ fn type_one_layer(
         ExprKind::Projection(record, labels) => {
             let record_type = record.ty();
             let kts = match record_type.kind() {
-                ValueKind::RecordType(kts) => kts,
+                NirKind::RecordType(kts) => kts,
                 _ => return span_err("ProjectionMustBeRecord"),
             };
 
@@ -671,19 +667,19 @@ fn type_one_layer(
 
             Type::new_infer_universe(
                 env,
-                Value::from_kind(ValueKind::RecordType(new_kts)),
+                Nir::from_kind(NirKind::RecordType(new_kts)),
             )?
         }
         ExprKind::ProjectionByExpr(record, selection) => {
             let record_type = record.ty();
             let rec_kts = match record_type.kind() {
-                ValueKind::RecordType(kts) => kts,
+                NirKind::RecordType(kts) => kts,
                 _ => return span_err("ProjectionMustBeRecord"),
             };
 
             let selection_val = selection.eval_to_type(env)?;
             let sel_kts = match selection_val.kind() {
-                ValueKind::RecordType(kts) => kts,
+                NirKind::RecordType(kts) => kts,
                 _ => return span_err("ProjectionByExprTakesRecordType"),
             };