Thread cx through typecheck

8 files changed, 65 insertions, 28 deletions

diff --git a/dhall/src/builtins.rs b/dhall/src/builtins.rs
index cc426dd..f92f1c3 100644
--- a/dhall/src/builtins.rs
+++ b/dhall/src/builtins.rs
@@ -11,6 +11,7 @@ use crate::syntax::{
     Const, Expr, ExprKind, InterpolatedText, InterpolatedTextContents, Label,
     NaiveDouble, NumKind, Span, UnspannedExpr, V,
 };
+use crate::Ctxt;
 
 /// Built-ins
 #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
@@ -98,12 +99,14 @@ pub struct BuiltinClosure {
 
 impl BuiltinClosure {
     pub fn new(b: Builtin, env: NzEnv) -> NirKind {
-        apply_builtin(b, Vec::new(), env)
+        // TODO: thread cx
+        Ctxt::with_new(|cx| apply_builtin(cx, 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();
-        apply_builtin(self.b, args, self.env.clone())
+        // TODO: thread cx
+        Ctxt::with_new(|cx| apply_builtin(cx, self.b, args, self.env.clone()))
     }
     pub fn to_hirkind(&self, venv: VarEnv) -> HirKind {
         HirKind::Expr(self.args.iter().fold(
@@ -307,7 +310,12 @@ macro_rules! make_closure {
 }
 
 #[allow(clippy::cognitive_complexity)]
-fn apply_builtin(b: Builtin, args: Vec<Nir>, env: NzEnv) -> NirKind {
+fn apply_builtin(
+    cx: Ctxt<'_>,
+    b: Builtin,
+    args: Vec<Nir>,
+    env: NzEnv,
+) -> NirKind {
     use NirKind::*;
     use NumKind::{Bool, Double, Integer, Natural};
 
@@ -318,7 +326,7 @@ fn apply_builtin(b: Builtin, args: Vec<Nir>, env: NzEnv) -> NirKind {
         DoneAsIs,
     }
     let make_closure = |e| {
-        typecheck(&skip_resolve_expr(&e).unwrap())
+        typecheck(cx, &skip_resolve_expr(&e).unwrap())
             .unwrap()
             .eval(env.clone())
     };
diff --git a/dhall/src/ctxt.rs b/dhall/src/ctxt.rs
index 2394d8e..37fab35 100644
--- a/dhall/src/ctxt.rs
+++ b/dhall/src/ctxt.rs
@@ -108,3 +108,11 @@ impl<'cx> std::ops::Index<ImportResultId> for CtxtS<'cx> {
         &self.import_results[id.0]
     }
 }
+
+/// Empty impl, because `FrozenVec` does not implement `Debug` and I can't be bothered to do it
+/// myself.
+impl<'cx> std::fmt::Debug for Ctxt<'cx> {
+    fn fmt(&self, _: &mut std::fmt::Formatter) -> std::fmt::Result {
+        Ok(())
+    }
+}
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index d079e92..661c33c 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -77,7 +77,8 @@ impl Parsed {
     }
 
     pub fn resolve(self) -> Result<Resolved, Error> {
-        resolve::resolve(self)
+        // TODO: thread cx
+        Ctxt::with_new(|cx| resolve::resolve(cx, self))
     }
     pub fn skip_resolve(self) -> Result<Resolved, Error> {
         resolve::skip_resolve(self)
@@ -91,10 +92,14 @@ impl Parsed {
 
 impl Resolved {
     pub fn typecheck(&self) -> Result<Typed, TypeError> {
-        Ok(Typed::from_tir(typecheck(&self.0)?))
+        // TODO: thread cx
+        Ctxt::with_new(|cx| Ok(Typed::from_tir(typecheck(cx, &self.0)?)))
     }
     pub fn typecheck_with(self, ty: &Hir) -> Result<Typed, TypeError> {
-        Ok(Typed::from_tir(typecheck_with(&self.0, ty)?))
+        // TODO: thread cx
+        Ctxt::with_new(|cx| {
+            Ok(Typed::from_tir(typecheck_with(cx, &self.0, ty)?))
+        })
     }
     /// Converts a value back to the corresponding AST expression.
     pub fn to_expr(&self) -> Expr {
diff --git a/dhall/src/operations/typecheck.rs b/dhall/src/operations/typecheck.rs
index bc0e864..5718114 100644
--- a/dhall/src/operations/typecheck.rs
+++ b/dhall/src/operations/typecheck.rs
@@ -13,7 +13,7 @@ use crate::syntax::{Const, ExprKind, Span};
 
 fn check_rectymerge(
     span: &Span,
-    env: &TyEnv,
+    env: &TyEnv<'_>,
     x: Nir,
     y: Nir,
 ) -> Result<(), TypeError> {
@@ -45,7 +45,7 @@ fn check_rectymerge(
 }
 
 fn typecheck_binop(
-    env: &TyEnv,
+    env: &TyEnv<'_>,
     span: Span,
     op: BinOp,
     l: Tir<'_>,
@@ -150,7 +150,7 @@ fn typecheck_binop(
 }
 
 fn typecheck_merge(
-    env: &TyEnv,
+    env: &TyEnv<'_>,
     span: Span,
     record: &Tir<'_>,
     scrut: &Tir<'_>,
@@ -288,7 +288,7 @@ fn typecheck_merge(
 }
 
 pub fn typecheck_operation(
-    env: &TyEnv,
+    env: &TyEnv<'_>,
     span: Span,
     opkind: OpKind<Tir<'_>>,
 ) -> Result<Type, TypeError> {
diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs
index 8869915..c2d1883 100644
--- a/dhall/src/semantics/resolve/hir.rs
+++ b/dhall/src/semantics/resolve/hir.rs
@@ -1,7 +1,7 @@
 use crate::error::TypeError;
 use crate::semantics::{type_with, NameEnv, Nir, NzEnv, Tir, TyEnv, Type};
 use crate::syntax::{Expr, ExprKind, Span, V};
-use crate::ToExprOptions;
+use crate::{Ctxt, ToExprOptions};
 
 /// Stores an alpha-normalized variable.
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
@@ -76,8 +76,11 @@ impl Hir {
     ) -> Result<Tir<'hir>, TypeError> {
         type_with(env, self, None)
     }
-    pub fn typecheck_noenv<'hir>(&'hir self) -> Result<Tir<'hir>, TypeError> {
-        self.typecheck(&TyEnv::new())
+    pub fn typecheck_noenv<'hir>(
+        &'hir self,
+        cx: Ctxt<'_>,
+    ) -> Result<Tir<'hir>, TypeError> {
+        self.typecheck(&TyEnv::new(cx))
     }
 
     /// Eval the Hir. It will actually get evaluated only as needed on demand.
diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs
index 955e2fa..cf72f80 100644
--- a/dhall/src/semantics/resolve/resolve.rs
+++ b/dhall/src/semantics/resolve/resolve.rs
@@ -250,7 +250,7 @@ impl ImportLocation {
             ImportMode::Location => {
                 let expr = self.kind.to_location();
                 let hir = skip_resolve_expr(&expr)?;
-                let ty = hir.typecheck_noenv()?.ty().clone();
+                let ty = hir.typecheck_noenv(env.cx())?.ty().clone();
                 (hir, ty)
             }
         };
@@ -463,8 +463,8 @@ fn resolve_with_env<'cx>(
     Ok(Resolved(resolved))
 }
 
-pub fn resolve(parsed: Parsed) -> Result<Resolved, Error> {
-    Ctxt::with_new(|cx| resolve_with_env(&mut ImportEnv::new(cx), parsed))
+pub fn resolve(cx: Ctxt<'_>, parsed: Parsed) -> Result<Resolved, Error> {
+    resolve_with_env(&mut ImportEnv::new(cx), parsed)
 }
 
 pub fn skip_resolve_expr(expr: &Expr) -> Result<Hir, Error> {
diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index 1fa66f0..fc0ce9f 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -1,5 +1,6 @@
 use crate::semantics::{AlphaVar, NameEnv, Nir, NzEnv, NzVar, Type, ValEnv};
 use crate::syntax::Label;
+use crate::Ctxt;
 
 /// Environment for indexing variables.
 #[derive(Debug, Clone, Copy, Default)]
@@ -9,7 +10,8 @@ pub struct VarEnv {
 
 /// Environment for typing expressions.
 #[derive(Debug, Clone)]
-pub struct TyEnv {
+pub struct TyEnv<'cx> {
+    cx: Ctxt<'cx>,
     names: NameEnv,
     items: ValEnv<Type>,
 }
@@ -38,13 +40,17 @@ impl VarEnv {
     }
 }
 
-impl TyEnv {
-    pub fn new() -> Self {
+impl<'cx> TyEnv<'cx> {
+    pub fn new(cx: Ctxt<'cx>) -> Self {
         TyEnv {
+            cx,
             names: NameEnv::new(),
             items: ValEnv::new(),
         }
     }
+    pub fn cx(&self) -> Ctxt<'cx> {
+        self.cx
+    }
     pub fn as_varenv(&self) -> VarEnv {
         self.names.as_varenv()
     }
@@ -57,12 +63,14 @@ impl TyEnv {
 
     pub fn insert_type(&self, x: &Label, ty: Type) -> Self {
         TyEnv {
+            cx: self.cx,
             names: self.names.insert(x),
             items: self.items.insert_type(ty),
         }
     }
     pub fn insert_value(&self, x: &Label, e: Nir, ty: Type) -> Self {
         TyEnv {
+            cx: self.cx,
             names: self.names.insert(x),
             items: self.items.insert_value(e, ty),
         }
@@ -72,7 +80,7 @@ impl TyEnv {
     }
 }
 
-impl<'a> From<&'a TyEnv> for NzEnv {
+impl<'a, 'cx> From<&'a TyEnv<'cx>> for NzEnv {
     fn from(x: &'a TyEnv) -> Self {
         x.to_nzenv()
     }
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 498bd76..7e8c0e1 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -5,6 +5,7 @@ use crate::error::{ErrorBuilder, TypeError, TypeMessage};
 use crate::operations::typecheck_operation;
 use crate::semantics::{Hir, HirKind, Nir, NirKind, Tir, TyEnv, Type};
 use crate::syntax::{Const, ExprKind, InterpolatedTextContents, NumKind, Span};
+use crate::Ctxt;
 
 fn function_check(a: Const, b: Const) -> Const {
     if b == Const::Type {
@@ -29,7 +30,7 @@ pub fn mk_span_err<T, S: ToString>(span: Span, msg: S) -> Result<T, TypeError> {
 /// When all sub-expressions have been typed, check the remaining toplevel
 /// layer.
 fn type_one_layer(
-    env: &TyEnv,
+    env: &TyEnv<'_>,
     ekind: ExprKind<Tir<'_>>,
     span: Span,
 ) -> Result<Type, TypeError> {
@@ -58,7 +59,7 @@ fn type_one_layer(
         }),
         ExprKind::Builtin(b) => {
             let t_hir = type_of_builtin(b);
-            typecheck(&t_hir)?.eval_to_type(env)?
+            typecheck(env.cx(), &t_hir)?.eval_to_type(env)?
         }
         ExprKind::TextLit(interpolated) => {
             let text_type = Type::from_builtin(Builtin::Text);
@@ -171,7 +172,7 @@ fn type_one_layer(
 // We pass the annotation to avoid duplicating the annot checking logic. I hope one day we can use
 // it to handle the annotations in merge/toMap/etc. uniformly.
 pub fn type_with<'hir>(
-    env: &TyEnv,
+    env: &TyEnv<'_>,
     hir: &'hir Hir,
     annot: Option<Type>,
 ) -> Result<Tir<'hir>, TypeError> {
@@ -267,15 +268,19 @@ pub fn type_with<'hir>(
 
 /// Typecheck an expression and return the expression annotated with its type if type-checking
 /// succeeded, or an error if type-checking failed.
-pub fn typecheck<'hir>(hir: &'hir Hir) -> Result<Tir<'hir>, TypeError> {
-    type_with(&TyEnv::new(), hir, None)
+pub fn typecheck<'hir>(
+    cx: Ctxt<'_>,
+    hir: &'hir Hir,
+) -> Result<Tir<'hir>, TypeError> {
+    type_with(&TyEnv::new(cx), hir, None)
 }
 
 /// Like `typecheck`, but additionally checks that the expression's type matches the provided type.
 pub fn typecheck_with<'hir>(
+    cx: Ctxt<'_>,
     hir: &'hir Hir,
     ty: &Hir,
 ) -> Result<Tir<'hir>, TypeError> {
-    let ty = typecheck(ty)?.eval_to_type(&TyEnv::new())?;
-    type_with(&TyEnv::new(), hir, Some(ty))
+    let ty = typecheck(cx, ty)?.eval_to_type(&TyEnv::new(cx))?;
+    type_with(&TyEnv::new(cx), hir, Some(ty))
 }