summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/builtins.rs16
-rw-r--r--dhall/src/ctxt.rs8
-rw-r--r--dhall/src/lib.rs11
-rw-r--r--dhall/src/operations/typecheck.rs8
-rw-r--r--dhall/src/semantics/resolve/hir.rs9
-rw-r--r--dhall/src/semantics/resolve/resolve.rs6
-rw-r--r--dhall/src/semantics/tck/env.rs16
-rw-r--r--dhall/src/semantics/tck/typecheck.rs19
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))
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 17:26:11 +0000