summaryrefslogtreecommitdiff
path: root/dhall/src/builtins.rs
diff options
context:
space:
mode:
authorNadrieril2020-12-06 23:55:21 +0000
committerNadrieril2020-12-07 19:34:38 +0000
commitc785b7c0c6cd8b3b1cc15eb79caf982a757020ba (patch)
tree6d38e68385814073b8b22ee8a8956435546892dc /dhall/src/builtins.rs
parent6287b7a7f9e421877ee13fefa586395fec844c99 (diff)
Thread cx through normalization
Diffstat (limited to 'dhall/src/builtins.rs')
-rw-r--r--dhall/src/builtins.rs51
1 files changed, 24 insertions, 27 deletions
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 {