Introduce proper Type struct

5 files changed, 121 insertions, 57 deletions

diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index ad54c9f..144cac5 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -120,7 +120,7 @@ impl Typed {
     }
 
     pub(crate) fn get_type(&self) -> Result<Normalized, TypeError> {
-        Ok(Normalized(self.0.ty().clone()))
+        Ok(Normalized(self.0.ty().clone().into_value()))
     }
 }
 
diff --git a/dhall/src/semantics/hir.rs b/dhall/src/semantics/hir.rs
index c8258ff..d0a8a96 100644
--- a/dhall/src/semantics/hir.rs
+++ b/dhall/src/semantics/hir.rs
@@ -1,6 +1,6 @@
 #![allow(dead_code)]
 use crate::error::TypeError;
-use crate::semantics::{type_with, NameEnv, NzEnv, TyEnv, TyExpr, Value};
+use crate::semantics::{type_with, NameEnv, NzEnv, TyEnv, TyExpr, Type, Value};
 use crate::syntax::{Expr, ExprKind, Span, V};
 use crate::{NormalizedExpr, ToExprOptions};
 
@@ -79,6 +79,10 @@ impl Hir {
     pub fn eval(&self, env: impl Into<NzEnv>) -> Value {
         Value::new_thunk(env.into(), self.clone())
     }
+    /// Evaluate to a Type.
+    pub fn eval_to_type(&self, env: impl Into<NzEnv>) -> Type {
+        self.eval(env).into()
+    }
     /// Eval a closed Hir (i.e. without free variables). It will actually get evaluated only as
     /// needed on demand.
     pub fn eval_closed_expr(&self) -> Value {
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 3a5b5b5..f31fd6c 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -4,7 +4,7 @@ use std::rc::Rc;
 use crate::semantics::nze::lazy;
 use crate::semantics::{
     apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit, Binder,
-    BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, VarEnv,
+    BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, Type, VarEnv,
 };
 use crate::syntax::{
     BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Label, LitKind,
@@ -139,6 +139,9 @@ impl Value {
         self.0.kind()
     }
 
+    pub(crate) fn to_type(&self) -> Type {
+        self.clone().into()
+    }
     /// Converts a value back to the corresponding AST expression.
     pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
         if opts.normalize {
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index dfb4397..4999899 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,17 +1,53 @@
 use crate::error::TypeError;
-use crate::semantics::{Hir, HirKind, NzEnv, TyEnv, Value};
-use crate::syntax::{Const, Span};
+use crate::semantics::{Hir, HirKind, NzEnv, TyEnv, Value, ValueKind, VarEnv};
+use crate::syntax::{Builtin, Const, Span};
 use crate::{NormalizedExpr, ToExprOptions};
 
-pub(crate) type Type = Value;
+/// An expression representing a type
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub(crate) struct Type {
+    val: Value,
+}
 
-// A hir expression plus its inferred type.
+/// A hir expression plus its inferred type.
 #[derive(Debug, Clone)]
 pub(crate) struct TyExpr {
     hir: Hir,
     ty: Type,
 }
 
+impl Type {
+    pub fn from_const(c: Const) -> Self {
+        Value::from_const(c).into()
+    }
+    pub fn from_builtin(b: Builtin) -> Self {
+        Value::from_builtin(b).into()
+    }
+
+    pub fn to_value(&self) -> Value {
+        self.val.clone()
+    }
+    pub fn as_value(&self) -> &Value {
+        &self.val
+    }
+    pub fn into_value(self) -> Value {
+        self.val
+    }
+    pub fn as_const(&self) -> Option<Const> {
+        self.val.as_const()
+    }
+    pub fn kind(&self) -> &ValueKind {
+        self.val.kind()
+    }
+
+    pub fn to_hir(&self, venv: VarEnv) -> Hir {
+        self.val.to_hir(venv)
+    }
+    pub fn to_expr_tyenv(&self, tyenv: &TyEnv) -> NormalizedExpr {
+        self.val.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv)
+    }
+}
+
 impl TyExpr {
     pub fn new(kind: HirKind, ty: Type, span: Span) -> Self {
         TyExpr {
@@ -52,6 +88,10 @@ impl TyExpr {
     pub fn eval(&self, env: impl Into<NzEnv>) -> Value {
         self.as_hir().eval(env.into())
     }
+    /// Evaluate to a Type.
+    pub fn eval_to_type(&self, env: impl Into<NzEnv>) -> Type {
+        self.eval(env).into()
+    }
     /// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as
     /// needed on demand.
     pub fn eval_closed_expr(&self) -> Value {
@@ -64,3 +104,9 @@ impl TyExpr {
         val
     }
 }
+
+impl From<Value> for Type {
+    fn from(x: Value) -> Type {
+        Type { val: x }
+    }
+}
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 36f7173..dd996ae 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -38,7 +38,8 @@ fn check_rectymerge(
     };
     for (k, tx) in kts_x {
         if let Some(ty) = kts_y.get(k) {
-            check_rectymerge(span, env, tx.clone(), ty.clone())?;
+            // TODO: store Type in RecordType ?
+            check_rectymerge(span, env, tx.clone().into(), ty.clone().into())?;
         }
     }
     Ok(())
@@ -105,7 +106,7 @@ fn type_one_layer(
                     .format(),
                 );
             }
-            let body_env = env.insert_type(&binder, annot.eval(env));
+            let body_env = env.insert_type(&binder, annot.eval_to_type(env));
             if body.get_kind(&body_env)?.is_none() {
                 return span_err("Invalid output type");
             }
@@ -117,7 +118,7 @@ fn type_one_layer(
                 )),
                 span.clone(),
             )
-            .eval(env)
+            .eval_to_type(env)
         }
         ExprKind::Pi(_, annot, body) => {
             let ks = match annot.ty().as_const() {
@@ -148,29 +149,29 @@ fn type_one_layer(
                 _ => return span_err("Invalid output type"),
             };
 
-            Value::from_const(function_check(ks, kt))
+            Type::from_const(function_check(ks, kt))
         }
         ExprKind::Let(_, _, _, body) => body.ty().clone(),
 
-        ExprKind::Const(Const::Type) => Value::from_const(Const::Kind),
-        ExprKind::Const(Const::Kind) => Value::from_const(Const::Sort),
+        ExprKind::Const(Const::Type) => Type::from_const(Const::Kind),
+        ExprKind::Const(Const::Kind) => Type::from_const(Const::Sort),
         ExprKind::Builtin(b) => {
             let t_hir = type_of_builtin(*b);
             let t_tyexpr = typecheck(&t_hir)?;
-            t_tyexpr.eval(env)
+            t_tyexpr.eval_to_type(env)
         }
-        ExprKind::Lit(LitKind::Bool(_)) => Value::from_builtin(Builtin::Bool),
+        ExprKind::Lit(LitKind::Bool(_)) => Type::from_builtin(Builtin::Bool),
         ExprKind::Lit(LitKind::Natural(_)) => {
-            Value::from_builtin(Builtin::Natural)
+            Type::from_builtin(Builtin::Natural)
         }
         ExprKind::Lit(LitKind::Integer(_)) => {
-            Value::from_builtin(Builtin::Integer)
+            Type::from_builtin(Builtin::Integer)
         }
         ExprKind::Lit(LitKind::Double(_)) => {
-            Value::from_builtin(Builtin::Double)
+            Type::from_builtin(Builtin::Double)
         }
         ExprKind::TextLit(interpolated) => {
-            let text_type = Value::from_builtin(Builtin::Text);
+            let text_type = Type::from_builtin(Builtin::Text);
             for contents in interpolated.iter() {
                 use InterpolatedTextContents::Expr;
                 if let Expr(x) = contents {
@@ -182,7 +183,7 @@ fn type_one_layer(
             text_type
         }
         ExprKind::EmptyListLit(t) => {
-            let t = t.eval(env);
+            let t = t.eval_to_type(env);
             match t.kind() {
                 ValueKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::List,
@@ -205,16 +206,16 @@ fn type_one_layer(
                 return span_err("InvalidListType");
             }
 
-            let t = x.ty().clone();
-            Value::from_builtin(Builtin::List).app(t)
+            let t = x.ty().to_value();
+            Value::from_builtin(Builtin::List).app(t).to_type()
         }
         ExprKind::SomeLit(x) => {
             if x.get_kind(env)? != Some(Const::Type) {
                 return span_err("InvalidOptionalType");
             }
 
-            let t = x.ty().clone();
-            Value::from_builtin(Builtin::Optional).app(t)
+            let t = x.ty().to_value();
+            Value::from_builtin(Builtin::Optional).app(t).to_type()
         }
         ExprKind::RecordLit(kvs) => {
             use std::collections::hash_map::Entry;
@@ -225,7 +226,7 @@ fn type_one_layer(
                     Entry::Occupied(_) => {
                         return span_err("RecordTypeDuplicateField")
                     }
-                    Entry::Vacant(e) => e.insert(v.ty().clone()),
+                    Entry::Vacant(e) => e.insert(v.ty().to_value()),
                 };
 
                 // Check that the fields have a valid kind
@@ -235,7 +236,7 @@ fn type_one_layer(
                 }
             }
 
-            Value::from_kind(ValueKind::RecordType(kts))
+            Value::from_kind(ValueKind::RecordType(kts)).to_type()
         }
         ExprKind::RecordType(kts) => {
             use std::collections::hash_map::Entry;
@@ -259,7 +260,7 @@ fn type_one_layer(
                 }
             }
 
-            Value::from_const(k)
+            Type::from_const(k)
         }
         ExprKind::UnionType(kts) => {
             use std::collections::hash_map::Entry;
@@ -286,17 +287,17 @@ fn type_one_layer(
             // an union type with only unary variants also has type Type
             let k = k.unwrap_or(Const::Type);
 
-            Value::from_const(k)
+            Type::from_const(k)
         }
         ExprKind::Field(scrut, x) => {
             match scrut.ty().kind() {
                 ValueKind::RecordType(kts) => match kts.get(&x) {
-                    Some(tth) => tth.clone(),
+                    Some(val) => val.clone().to_type(),
                     None => return span_err("MissingRecordField"),
                 },
                 // TODO: branch here only when scrut.ty() is a Const
                 _ => {
-                    let scrut_nf = scrut.eval(env);
+                    let scrut_nf = scrut.eval_to_type(env);
                     match scrut_nf.kind() {
                         ValueKind::UnionType(kts) => match kts.get(x) {
                             // Constructor has type T -> < x: T, ... >
@@ -304,8 +305,11 @@ fn type_one_layer(
                                 Value::from_kind(ValueKind::PiClosure {
                                     binder: Binder::new(x.clone()),
                                     annot: ty.clone(),
-                                    closure: Closure::new_constant(scrut_nf),
+                                    closure: Closure::new_constant(
+                                        scrut_nf.into_value(),
+                                    ),
                                 })
+                                .to_type()
                             }
                             Some(None) => scrut_nf,
                             None => return span_err("MissingUnionField"),
@@ -316,7 +320,7 @@ fn type_one_layer(
             }
         }
         ExprKind::Assert(t) => {
-            let t = t.eval(env);
+            let t = t.eval_to_type(env);
             match t.kind() {
                 ValueKind::Equivalence(x, y) if x == y => {}
                 ValueKind::Equivalence(..) => {
@@ -328,8 +332,9 @@ fn type_one_layer(
         }
         ExprKind::App(f, arg) => {
             match f.ty().kind() {
+                // TODO: store Type in closure
                 ValueKind::PiClosure { annot, closure, .. } => {
-                    if arg.ty() != annot {
+                    if arg.ty().as_value() != annot {
                         return mkerr(
                             ErrorBuilder::new(format!(
                                 "wrong type of function argument"
@@ -358,7 +363,7 @@ fn type_one_layer(
                     }
 
                     let arg_nf = arg.eval(env);
-                    closure.apply(arg_nf)
+                    closure.apply(arg_nf).to_type()
                 }
                 _ => return mkerr(
                     ErrorBuilder::new(format!(
@@ -407,7 +412,7 @@ fn type_one_layer(
                 Ok(r_t.clone())
             })?;
 
-            Value::from_kind(ValueKind::RecordType(kts))
+            Value::from_kind(ValueKind::RecordType(kts)).to_type()
         }
         ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
             check_rectymerge(&span, env, x.ty().clone(), y.ty().clone())?;
@@ -420,15 +425,20 @@ fn type_one_layer(
                 )),
                 span.clone(),
             )
-            .eval(env)
+            .eval_to_type(env)
         }
         ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
-            check_rectymerge(&span, env, x.eval(env), y.eval(env))?;
+            check_rectymerge(
+                &span,
+                env,
+                x.eval_to_type(env),
+                y.eval_to_type(env),
+            )?;
 
             // A RecordType's type is always a const
             let xk = x.ty().as_const().unwrap();
             let yk = y.ty().as_const().unwrap();
-            Value::from_const(max(xk, yk))
+            Type::from_const(max(xk, yk))
         }
         ExprKind::BinOp(BinOp::ListAppend, l, r) => {
             match l.ty().kind() {
@@ -453,10 +463,10 @@ fn type_one_layer(
                 return span_err("EquivalenceArgumentsMustBeTerms");
             }
 
-            Value::from_const(Const::Type)
+            Type::from_const(Const::Type)
         }
         ExprKind::BinOp(o, l, r) => {
-            let t = Value::from_builtin(match o {
+            let t = Type::from_builtin(match o {
                 BinOp::BoolAnd
                 | BinOp::BoolOr
                 | BinOp::BoolEQ
@@ -507,7 +517,7 @@ fn type_one_layer(
 
             let mut inferred_type = None;
             for (x, handler_type) in handlers {
-                let handler_return_type = match variants.get(x) {
+                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, .. } => {
@@ -542,7 +552,7 @@ fn type_one_layer(
                             }
 
                             match closure.remove_binder() {
-                                Ok(v) => v,
+                                Ok(v) => v.to_type(),
                                 Err(()) => {
                                     return span_err(
                                         "MergeReturnTypeIsDependent",
@@ -586,7 +596,7 @@ fn type_one_layer(
                         }
                     },
                     // Union alternative without type
-                    Some(None) => handler_type.clone(),
+                    Some(None) => handler_type.clone().to_type(),
                     None => return span_err("MergeHandlerMissingVariant"),
                 };
                 match &inferred_type {
@@ -604,7 +614,7 @@ fn type_one_layer(
                 }
             }
 
-            let type_annot = type_annot.as_ref().map(|t| t.eval(env));
+            let type_annot = type_annot.as_ref().map(|t| t.eval_to_type(env));
             match (inferred_type, type_annot) {
                 (Some(t1), Some(t2)) => {
                     if t1 != t2 {
@@ -638,7 +648,7 @@ fn type_one_layer(
                          annotation",
                     );
                 };
-                let annot_val = annot.eval(env);
+                let annot_val = annot.eval_to_type(env);
 
                 let err_msg = "The type of `toMap x` must be of the form \
                                `List { mapKey : Text, mapValue : T }`";
@@ -679,10 +689,11 @@ fn type_one_layer(
                 let mut kts = HashMap::new();
                 kts.insert("mapKey".into(), Value::from_builtin(Builtin::Text));
                 kts.insert("mapValue".into(), entry_type);
-                let output_type = Value::from_builtin(Builtin::List)
-                    .app(Value::from_kind(ValueKind::RecordType(kts)));
+                let output_type: Type = Value::from_builtin(Builtin::List)
+                    .app(Value::from_kind(ValueKind::RecordType(kts)))
+                    .to_type();
                 if let Some(annot) = annot {
-                    let annot_val = annot.eval(env);
+                    let annot_val = annot.eval_to_type(env);
                     if output_type != annot_val {
                         return span_err("Annotation mismatch");
                     }
@@ -713,7 +724,7 @@ fn type_one_layer(
                 };
             }
 
-            Value::from_kind(ValueKind::RecordType(new_kts))
+            Value::from_kind(ValueKind::RecordType(new_kts)).to_type()
         }
         ExprKind::ProjectionByExpr(record, selection) => {
             let record_type = record.ty();
@@ -722,7 +733,7 @@ fn type_one_layer(
                 _ => return span_err("ProjectionMustBeRecord"),
             };
 
-            let selection_val = selection.eval(env);
+            let selection_val = selection.eval_to_type(env);
             let sel_kts = match selection_val.kind() {
                 ValueKind::RecordType(kts) => kts,
                 _ => return span_err("ProjectionByExprTakesRecordType"),
@@ -781,9 +792,9 @@ pub(crate) fn type_with(
         HirKind::Expr(ExprKind::Annot(x, t)) => {
             let t = match t.kind() {
                 HirKind::Expr(ExprKind::Const(Const::Sort)) => {
-                    Value::from_const(Const::Sort)
+                    Type::from_const(Const::Sort)
                 }
-                _ => type_with(env, t, None)?.eval(env),
+                _ => type_with(env, t, None)?.eval_to_type(env),
             };
             type_with(env, x, Some(t))
         }
@@ -791,21 +802,21 @@ pub(crate) fn type_with(
             let ekind = match ekind {
                 ExprKind::Lam(binder, annot, body) => {
                     let annot = type_with(env, annot, None)?;
-                    let annot_nf = annot.eval(env);
+                    let annot_nf = annot.eval_to_type(env);
                     let body_env = env.insert_type(binder, annot_nf);
                     let body = type_with(&body_env, body, None)?;
                     ExprKind::Lam(binder.clone(), annot, body)
                 }
                 ExprKind::Pi(binder, annot, body) => {
                     let annot = type_with(env, annot, None)?;
-                    let annot_nf = annot.eval(env);
-                    let body_env = env.insert_type(binder, annot_nf);
+                    let annot_val = annot.eval_to_type(env);
+                    let body_env = env.insert_type(binder, annot_val);
                     let body = type_with(&body_env, body, None)?;
                     ExprKind::Pi(binder.clone(), annot, body)
                 }
                 ExprKind::Let(binder, annot, val, body) => {
                     let val_annot = if let Some(t) = annot {
-                        Some(type_with(env, t, None)?.eval(env))
+                        Some(type_with(env, t, None)?.eval_to_type(env))
                     } else {
                         None
                     };
@@ -831,6 +842,6 @@ pub(crate) fn typecheck(hir: &Hir) -> Result<TyExpr, TypeError> {
 
 /// Like `typecheck`, but additionally checks that the expression's type matches the provided type.
 pub(crate) fn typecheck_with(hir: &Hir, ty: Hir) -> Result<TyExpr, TypeError> {
-    let ty = typecheck(&ty)?.eval(&TyEnv::new());
+    let ty = typecheck(&ty)?.eval_to_type(&TyEnv::new());
     type_with(&TyEnv::new(), hir, Some(ty))
 }