From c785b7c0c6cd8b3b1cc15eb79caf982a757020ba Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 6 Dec 2020 23:55:21 +0000
Subject: Thread cx through normalization

---
 dhall/src/semantics/tck/tir.rs | 60 ++++++++++++++++++++++--------------------
 1 file changed, 32 insertions(+), 28 deletions(-)

(limited to 'dhall/src/semantics/tck/tir.rs')

diff --git a/dhall/src/semantics/tck/tir.rs b/dhall/src/semantics/tck/tir.rs
index f34802c..7b04f57 100644
--- a/dhall/src/semantics/tck/tir.rs
+++ b/dhall/src/semantics/tck/tir.rs
@@ -2,6 +2,7 @@ use crate::builtins::Builtin;
 use crate::error::{ErrorBuilder, TypeError};
 use crate::semantics::{mkerr, Hir, Nir, NirKind, NzEnv, TyEnv, VarEnv};
 use crate::syntax::{Const, Expr, Span};
+use crate::Ctxt;
 
 /// The type of a type. 0 is `Type`, 1 is `Kind`, etc...
 #[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Default)]
@@ -9,17 +10,17 @@ pub struct Universe(u8);
 
 /// An expression representing a type
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub struct Type {
-    val: Nir,
+pub struct Type<'cx> {
+    val: Nir<'cx>,
     univ: Universe,
 }
 
 /// A hir expression plus its inferred type.
 /// Stands for "Typed intermediate representation"
 #[derive(Debug, Clone)]
-pub struct Tir<'hir> {
-    hir: &'hir Hir,
-    ty: Type,
+pub struct Tir<'cx, 'hir> {
+    hir: &'hir Hir<'cx>,
+    ty: Type<'cx>,
 }
 
 impl Universe {
@@ -43,16 +44,16 @@ impl Universe {
     }
 }
 
-impl Type {
-    pub fn new(val: Nir, univ: Universe) -> Self {
+impl<'cx> Type<'cx> {
+    pub fn new(val: Nir<'cx>, univ: Universe) -> Self {
         Type { val, univ }
     }
     /// Creates a new Type and infers its universe by re-typechecking its value.
     /// TODO: ideally avoid this function altogether. Would need to store types in RecordType and
     /// PiClosure.
     pub fn new_infer_universe(
-        env: &TyEnv,
-        val: Nir,
+        env: &TyEnv<'cx>,
+        val: Nir<'cx>,
     ) -> Result<Self, TypeError> {
         let c = val.to_hir(env.as_varenv()).typecheck(env)?.ty().as_const();
         let u = match c {
@@ -67,14 +68,14 @@ impl Type {
     pub fn from_const(c: Const) -> Self {
         Self::new(Nir::from_const(c), c.to_universe().next())
     }
-    pub fn from_builtin(b: Builtin) -> Self {
+    pub fn from_builtin(cx: Ctxt<'cx>, b: Builtin) -> Self {
         use Builtin::*;
         match b {
             Bool | Natural | Integer | Double | Text => {}
             _ => unreachable!("this builtin is not a type: {}", b),
         }
 
-        Self::new(Nir::from_builtin(b), Universe::from_const(Const::Type))
+        Self::new(Nir::from_builtin(cx, b), Universe::from_const(Const::Type))
     }
 
     /// Get the type of this type
@@ -82,60 +83,60 @@ impl Type {
         self.univ
     }
 
-    pub fn to_nir(&self) -> Nir {
+    pub fn to_nir(&self) -> Nir<'cx> {
         self.val.clone()
     }
-    pub fn as_nir(&self) -> &Nir {
+    pub fn as_nir(&self) -> &Nir<'cx> {
         &self.val
     }
-    pub fn into_nir(self) -> Nir {
+    pub fn into_nir(self) -> Nir<'cx> {
         self.val
     }
     pub fn as_const(&self) -> Option<Const> {
         self.val.as_const()
     }
-    pub fn kind(&self) -> &NirKind {
+    pub fn kind(&self) -> &NirKind<'cx> {
         self.val.kind()
     }
 
-    pub fn to_hir(&self, venv: VarEnv) -> Hir {
+    pub fn to_hir(&self, venv: VarEnv) -> Hir<'cx> {
         self.val.to_hir(venv)
     }
-    pub fn to_expr_tyenv(&self, tyenv: &TyEnv) -> Expr {
+    pub fn to_expr_tyenv(&self, tyenv: &TyEnv<'cx>) -> Expr {
         self.val.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv)
     }
 }
 
-impl<'hir> Tir<'hir> {
-    pub fn from_hir(hir: &'hir Hir, ty: Type) -> Self {
+impl<'cx, 'hir> Tir<'cx, 'hir> {
+    pub fn from_hir(hir: &'hir Hir<'cx>, ty: Type<'cx>) -> Self {
         Tir { hir, ty }
     }
 
     pub fn span(&self) -> Span {
         self.as_hir().span()
     }
-    pub fn ty(&self) -> &Type {
+    pub fn ty(&self) -> &Type<'cx> {
         &self.ty
     }
-    pub fn into_ty(self) -> Type {
+    pub fn into_ty(self) -> Type<'cx> {
         self.ty
     }
 
-    pub fn to_hir(&self) -> Hir {
+    pub fn to_hir(&self) -> Hir<'cx> {
         self.as_hir().clone()
     }
-    pub fn as_hir(&self) -> &Hir {
-        &self.hir
+    pub fn as_hir(&self) -> &'hir Hir<'cx> {
+        self.hir
     }
-    pub fn to_expr_tyenv(&self, env: &TyEnv) -> Expr {
+    pub fn to_expr_tyenv(&self, env: &TyEnv<'cx>) -> Expr {
         self.as_hir().to_expr_tyenv(env)
     }
 
     /// Eval the Tir. It will actually get evaluated only as needed on demand.
-    pub fn eval(&self, env: impl Into<NzEnv>) -> Nir {
+    pub fn eval(&self, env: impl Into<NzEnv<'cx>>) -> Nir<'cx> {
         self.as_hir().eval(env.into())
     }
-    pub fn ensure_is_type(&self, env: &TyEnv) -> Result<(), TypeError> {
+    pub fn ensure_is_type(&self, env: &TyEnv<'cx>) -> Result<(), TypeError> {
         if self.ty().as_const().is_none() {
             return mkerr(
                 ErrorBuilder::new(format!(
@@ -159,7 +160,10 @@ impl<'hir> Tir<'hir> {
         Ok(())
     }
     /// Evaluate to a Type.
-    pub fn eval_to_type(&self, env: &TyEnv) -> Result<Type, TypeError> {
+    pub fn eval_to_type(
+        &self,
+        env: &TyEnv<'cx>,
+    ) -> Result<Type<'cx>, TypeError> {
         self.ensure_is_type(env)?;
         Ok(Type::new(
             self.eval(env),
-- 
cgit v1.2.3