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/builtins.rs | 51 ++++++++++++++++++++++++---------------------------
 1 file changed, 24 insertions(+), 27 deletions(-)

(limited to 'dhall/src/builtins.rs')

diff --git a/dhall/src/builtins.rs b/dhall/src/builtins.rs
index f92f1c3..39cc4ef 100644
--- a/dhall/src/builtins.rs
+++ b/dhall/src/builtins.rs
@@ -11,7 +11,6 @@ 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)]
@@ -90,25 +89,23 @@ impl Builtin {
 /// A partially applied builtin.
 /// Invariant: the evaluation of the given args must not be able to progress further
 #[derive(Debug, Clone)]
-pub struct BuiltinClosure {
-    env: NzEnv,
+pub struct BuiltinClosure<'cx> {
+    env: NzEnv<'cx>,
     b: Builtin,
     /// Arguments applied to the closure so far.
-    args: Vec<Nir>,
+    args: Vec<Nir<'cx>>,
 }
 
-impl BuiltinClosure {
-    pub fn new(b: Builtin, env: NzEnv) -> NirKind {
-        // TODO: thread cx
-        Ctxt::with_new(|cx| apply_builtin(cx, b, Vec::new(), env))
+impl<'cx> BuiltinClosure<'cx> {
+    pub fn new(b: Builtin, env: NzEnv<'cx>) -> NirKind<'cx> {
+        apply_builtin(b, Vec::new(), env)
     }
-    pub fn apply(&self, a: Nir) -> NirKind {
+    pub fn apply(&self, a: Nir<'cx>) -> NirKind<'cx> {
         use std::iter::once;
         let args = self.args.iter().cloned().chain(once(a)).collect();
-        // TODO: thread cx
-        Ctxt::with_new(|cx| apply_builtin(cx, self.b, args, self.env.clone()))
+        apply_builtin(self.b, args, self.env.clone())
     }
-    pub fn to_hirkind(&self, venv: VarEnv) -> HirKind {
+    pub fn to_hirkind(&self, venv: VarEnv) -> HirKind<'cx> {
         HirKind::Expr(self.args.iter().fold(
             ExprKind::Builtin(self.b),
             |acc, v| {
@@ -181,7 +178,7 @@ macro_rules! make_type {
     };
 }
 
-pub fn type_of_builtin(b: Builtin) -> Hir {
+pub fn type_of_builtin<'cx>(b: Builtin) -> Hir<'cx> {
     use Builtin::*;
     let expr = match b {
         Bool | Natural | Integer | Double | Text => make_type!(Type),
@@ -310,19 +307,19 @@ macro_rules! make_closure {
 }
 
 #[allow(clippy::cognitive_complexity)]
-fn apply_builtin(
-    cx: Ctxt<'_>,
+fn apply_builtin<'cx>(
     b: Builtin,
-    args: Vec<Nir>,
-    env: NzEnv,
-) -> NirKind {
+    args: Vec<Nir<'cx>>,
+    env: NzEnv<'cx>,
+) -> NirKind<'cx> {
+    let cx = env.cx();
     use NirKind::*;
     use NumKind::{Bool, Double, Integer, Natural};
 
     // Small helper enum
-    enum Ret {
-        NirKind(NirKind),
-        Nir(Nir),
+    enum Ret<'cx> {
+        NirKind(NirKind<'cx>),
+        Nir(Nir<'cx>),
         DoneAsIs,
     }
     let make_closure = |e| {
@@ -494,7 +491,7 @@ fn apply_builtin(
                     let mut kts = HashMap::new();
                     kts.insert(
                         "index".into(),
-                        Nir::from_builtin(Builtin::Natural),
+                        Nir::from_builtin(cx, Builtin::Natural),
                     );
                     kts.insert("value".into(), t.clone());
                     let t = Nir::from_kind(RecordType(kts));
@@ -524,7 +521,7 @@ fn apply_builtin(
             }
         }
         (Builtin::ListBuild, [t, f]) => {
-            let list_t = Nir::from_builtin(Builtin::List).app(t.clone());
+            let list_t = Nir::from_builtin(cx, Builtin::List).app(t.clone());
             Ret::Nir(
                 f.app(list_t)
                     .app(
@@ -551,7 +548,7 @@ fn apply_builtin(
             _ => Ret::DoneAsIs,
         },
         (Builtin::NaturalBuild, [f]) => Ret::Nir(
-            f.app(Nir::from_builtin(Builtin::Natural))
+            f.app(Nir::from_builtin(cx, Builtin::Natural))
                 .app(make_closure(make_closure!(
                     λ(x : Natural) ->
                     1 + var(x)
@@ -562,7 +559,7 @@ fn apply_builtin(
         (Builtin::NaturalFold, [n, t, succ, zero]) => match &*n.kind() {
             Num(Natural(0)) => Ret::Nir(zero.clone()),
             Num(Natural(n)) => {
-                let fold = Nir::from_builtin(Builtin::NaturalFold)
+                let fold = Nir::from_builtin(cx, Builtin::NaturalFold)
                     .app(Num(Natural(n - 1)).into_nir())
                     .app(t.clone())
                     .app(succ.clone())
@@ -580,12 +577,12 @@ fn apply_builtin(
     }
 }
 
-impl std::cmp::PartialEq for BuiltinClosure {
+impl<'cx> std::cmp::PartialEq for BuiltinClosure<'cx> {
     fn eq(&self, other: &Self) -> bool {
         self.b == other.b && self.args == other.args
     }
 }
-impl std::cmp::Eq for BuiltinClosure {}
+impl<'cx> std::cmp::Eq for BuiltinClosure<'cx> {}
 
 impl std::fmt::Display for Builtin {
     fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
-- 
cgit v1.2.3