summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/builtins.rs51
-rw-r--r--dhall/src/ctxt.rs12
-rw-r--r--dhall/src/lib.rs76
-rw-r--r--dhall/src/operations/normalization.rs6
-rw-r--r--dhall/src/operations/typecheck.rs72
-rw-r--r--dhall/src/semantics/nze/env.rs42
-rw-r--r--dhall/src/semantics/nze/nir.rs197
-rw-r--r--dhall/src/semantics/nze/normalize.rs39
-rw-r--r--dhall/src/semantics/resolve/cache.rs24
-rw-r--r--dhall/src/semantics/resolve/env.rs13
-rw-r--r--dhall/src/semantics/resolve/hir.rs42
-rw-r--r--dhall/src/semantics/resolve/resolve.rs32
-rw-r--r--dhall/src/semantics/tck/env.rs16
-rw-r--r--dhall/src/semantics/tck/tir.rs60
-rw-r--r--dhall/src/semantics/tck/typecheck.rs60
-rw-r--r--dhall/tests/spec.rs158
16 files changed, 475 insertions, 425 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 {
diff --git a/dhall/src/ctxt.rs b/dhall/src/ctxt.rs
index 37fab35..a171ebe 100644
--- a/dhall/src/ctxt.rs
+++ b/dhall/src/ctxt.rs
@@ -23,7 +23,7 @@ pub struct StoredImport<'cx> {
#[derive(Default)]
pub struct CtxtS<'cx> {
imports: FrozenVec<Box<StoredImport<'cx>>>,
- import_results: FrozenVec<Box<Typed>>,
+ import_results: FrozenVec<Box<Typed<'cx>>>,
}
/// Context for the dhall compiler. Stores various global maps.
@@ -58,7 +58,7 @@ impl<'cx> Ctxt<'cx> {
ImportId(id)
}
/// Store the result of fetching an import.
- pub fn push_import_result(self, res: Typed) -> ImportResultId {
+ pub fn push_import_result(self, res: Typed<'cx>) -> ImportResultId {
let id = self.0.import_results.len();
self.0.import_results.push(Box::new(res));
ImportResultId(id)
@@ -77,12 +77,12 @@ impl<'cx> StoredImport<'cx> {
}
/// Get the result of fetching this import. Returns `None` if the result has not yet been
/// fetched.
- pub fn get_result(&self) -> Option<&'cx Typed> {
+ pub fn get_result(&self) -> Option<&'cx Typed<'cx>> {
let res = self.get_resultid()?;
Some(&self.cx[res])
}
/// Store the result of fetching this import.
- pub fn set_result(&self, res: Typed) -> ImportResultId {
+ pub fn set_result(&self, res: Typed<'cx>) -> ImportResultId {
let res = self.cx.push_import_result(res);
self.set_resultid(res);
res
@@ -103,8 +103,8 @@ impl<'cx> std::ops::Index<ImportId> for CtxtS<'cx> {
}
}
impl<'cx> std::ops::Index<ImportResultId> for CtxtS<'cx> {
- type Output = Typed;
- fn index(&self, id: ImportResultId) -> &Typed {
+ type Output = Typed<'cx>;
+ fn index(&self, id: ImportResultId) -> &Typed<'cx> {
&self.import_results[id.0]
}
}
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index 661c33c..ec2b813 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -5,7 +5,8 @@
clippy::needless_lifetimes,
clippy::new_ret_no_self,
clippy::new_without_default,
- clippy::useless_format
+ clippy::useless_format,
+ unreachable_code
)]
pub mod builtins;
@@ -36,20 +37,20 @@ pub struct Parsed(Expr, ImportLocation);
///
/// Invariant: there must be no `Import` nodes or `ImportAlt` operations left.
#[derive(Debug, Clone)]
-pub struct Resolved(Hir);
+pub struct Resolved<'cx>(Hir<'cx>);
/// A typed expression
#[derive(Debug, Clone)]
-pub struct Typed {
- pub hir: Hir,
- pub ty: Type,
+pub struct Typed<'cx> {
+ pub hir: Hir<'cx>,
+ pub ty: Type<'cx>,
}
/// A normalized expression.
///
/// This is actually a lie, because the expression will only get normalized on demand.
#[derive(Debug, Clone)]
-pub struct Normalized(Nir);
+pub struct Normalized<'cx>(Nir<'cx>);
/// Controls conversion from `Nir` to `Expr`
#[derive(Copy, Clone, Default)]
@@ -76,11 +77,10 @@ impl Parsed {
parse::parse_binary(data)
}
- pub fn resolve(self) -> Result<Resolved, Error> {
- // TODO: thread cx
- Ctxt::with_new(|cx| resolve::resolve(cx, self))
+ pub fn resolve<'cx>(self, cx: Ctxt<'cx>) -> Result<Resolved<'cx>, Error> {
+ resolve::resolve(cx, self)
}
- pub fn skip_resolve(self) -> Result<Resolved, Error> {
+ pub fn skip_resolve<'cx>(self) -> Result<Resolved<'cx>, Error> {
resolve::skip_resolve(self)
}
@@ -90,16 +90,16 @@ impl Parsed {
}
}
-impl Resolved {
- pub fn typecheck(&self) -> Result<Typed, TypeError> {
- // TODO: thread cx
- Ctxt::with_new(|cx| Ok(Typed::from_tir(typecheck(cx, &self.0)?)))
+impl<'cx> Resolved<'cx> {
+ pub fn typecheck(&self, cx: Ctxt<'cx>) -> Result<Typed<'cx>, TypeError> {
+ Ok(Typed::from_tir(typecheck(cx, &self.0)?))
}
- pub fn typecheck_with(self, ty: &Hir) -> Result<Typed, TypeError> {
- // TODO: thread cx
- Ctxt::with_new(|cx| {
- Ok(Typed::from_tir(typecheck_with(cx, &self.0, ty)?))
- })
+ pub fn typecheck_with(
+ self,
+ cx: Ctxt<'cx>,
+ ty: &Hir<'cx>,
+ ) -> Result<Typed<'cx>, TypeError> {
+ 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 {
@@ -107,16 +107,16 @@ impl Resolved {
}
}
-impl Typed {
- fn from_tir(tir: Tir<'_>) -> Self {
+impl<'cx> Typed<'cx> {
+ fn from_tir(tir: Tir<'cx, '_>) -> Self {
Typed {
hir: tir.as_hir().clone(),
ty: tir.ty().clone(),
}
}
/// Reduce an expression to its normal form, performing beta reduction
- pub fn normalize(&self) -> Normalized {
- Normalized(self.hir.eval_closed_expr())
+ pub fn normalize(&self, cx: Ctxt<'cx>) -> Normalized<'cx> {
+ Normalized(self.hir.eval_closed_expr(cx))
}
/// Converts a value back to the corresponding AST expression.
@@ -124,24 +124,24 @@ impl Typed {
self.hir.to_expr(ToExprOptions { alpha: false })
}
- pub fn ty(&self) -> &Type {
+ pub fn ty(&self) -> &Type<'cx> {
&self.ty
}
- pub fn get_type(&self) -> Result<Normalized, TypeError> {
+ pub fn get_type(&self) -> Result<Normalized<'cx>, TypeError> {
Ok(Normalized(self.ty.clone().into_nir()))
}
}
-impl Normalized {
+impl<'cx> Normalized<'cx> {
/// Converts a value back to the corresponding AST expression.
pub fn to_expr(&self) -> Expr {
self.0.to_expr(ToExprOptions::default())
}
/// Converts a value back to the corresponding Hir expression.
- pub fn to_hir(&self) -> Hir {
+ pub fn to_hir(&self) -> Hir<'cx> {
self.0.to_hir_noenv()
}
- pub fn as_nir(&self) -> &Nir {
+ pub fn as_nir(&self) -> &Nir<'cx> {
&self.0
}
/// Converts a value back to the corresponding AST expression, alpha-normalizing in the process.
@@ -178,37 +178,31 @@ impl From<Parsed> for Expr {
other.to_expr()
}
}
-impl From<Normalized> for Expr {
- fn from(other: Normalized) -> Self {
+impl<'cx> From<Normalized<'cx>> for Expr {
+ fn from(other: Normalized<'cx>) -> Self {
other.to_expr()
}
}
-impl Display for Resolved {
+impl<'cx> Display for Resolved<'cx> {
fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> {
self.to_expr().fmt(f)
}
}
-impl Eq for Typed {}
-impl PartialEq for Typed {
- fn eq(&self, other: &Self) -> bool {
- self.normalize() == other.normalize()
- }
-}
-impl Display for Typed {
+impl<'cx> Display for Typed<'cx> {
fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> {
self.to_expr().fmt(f)
}
}
-impl Eq for Normalized {}
-impl PartialEq for Normalized {
+impl<'cx> Eq for Normalized<'cx> {}
+impl<'cx> PartialEq for Normalized<'cx> {
fn eq(&self, other: &Self) -> bool {
self.0 == other.0
}
}
-impl Display for Normalized {
+impl<'cx> Display for Normalized<'cx> {
fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> {
self.to_expr().fmt(f)
}
diff --git a/dhall/src/operations/normalization.rs b/dhall/src/operations/normalization.rs
index 28375b2..6c68e7c 100644
--- a/dhall/src/operations/normalization.rs
+++ b/dhall/src/operations/normalization.rs
@@ -8,7 +8,7 @@ use crate::semantics::{
};
use crate::syntax::{ExprKind, Label, NumKind};
-fn normalize_binop(o: BinOp, x: Nir, y: Nir) -> Ret {
+fn normalize_binop<'cx>(o: BinOp, x: Nir<'cx>, y: Nir<'cx>) -> Ret<'cx> {
use BinOp::*;
use NirKind::{EmptyListLit, NEListLit, Num, RecordLit, RecordType};
use NumKind::{Bool, Natural};
@@ -119,7 +119,7 @@ fn normalize_binop(o: BinOp, x: Nir, y: Nir) -> Ret {
}
}
-fn normalize_field(v: &Nir, field: &Label) -> Ret {
+fn normalize_field<'cx>(v: &Nir<'cx>, field: &Label) -> Ret<'cx> {
use self::BinOp::{RecursiveRecordMerge, RightBiasedRecordMerge};
use NirKind::{Op, RecordLit, UnionConstructor, UnionType};
use OpKind::{BinOp, Field, Projection};
@@ -187,7 +187,7 @@ fn normalize_field(v: &Nir, field: &Label) -> Ret {
}
}
-pub fn normalize_operation(opkind: OpKind<Nir>) -> Ret {
+pub fn normalize_operation<'cx>(opkind: OpKind<Nir<'cx>>) -> Ret<'cx> {
use self::BinOp::RightBiasedRecordMerge;
use NirKind::{
EmptyListLit, EmptyOptionalLit, NEListLit, NEOptionalLit, Num, Op,
diff --git a/dhall/src/operations/typecheck.rs b/dhall/src/operations/typecheck.rs
index 5718114..9b19c84 100644
--- a/dhall/src/operations/typecheck.rs
+++ b/dhall/src/operations/typecheck.rs
@@ -14,8 +14,8 @@ use crate::syntax::{Const, ExprKind, Span};
fn check_rectymerge(
span: &Span,
env: &TyEnv<'_>,
- x: Nir,
- y: Nir,
+ x: Nir<'_>,
+ y: Nir<'_>,
) -> Result<(), TypeError> {
let kts_x = match x.kind() {
NirKind::RecordType(kts) => kts,
@@ -44,13 +44,14 @@ fn check_rectymerge(
Ok(())
}
-fn typecheck_binop(
- env: &TyEnv<'_>,
+fn typecheck_binop<'cx>(
+ env: &TyEnv<'cx>,
span: Span,
op: BinOp,
- l: Tir<'_>,
- r: Tir<'_>,
-) -> Result<Type, TypeError> {
+ l: Tir<'cx, '_>,
+ r: Tir<'cx, '_>,
+) -> Result<Type<'cx>, TypeError> {
+ let cx = env.cx();
let span_err = |msg: &str| mk_span_err(span.clone(), msg);
use BinOp::*;
use NirKind::{ListType, RecordType};
@@ -124,17 +125,20 @@ fn typecheck_binop(
Type::from_const(Const::Type)
}
op => {
- let t = Type::from_builtin(match op {
- BoolAnd | BoolOr | BoolEQ | BoolNE => Builtin::Bool,
- NaturalPlus | NaturalTimes => Builtin::Natural,
- TextAppend => Builtin::Text,
- ListAppend
- | RightBiasedRecordMerge
- | RecursiveRecordMerge
- | RecursiveRecordTypeMerge
- | Equivalence => unreachable!(),
- ImportAlt => unreachable!("ImportAlt leftover in tck"),
- });
+ let t = Type::from_builtin(
+ cx,
+ match op {
+ BoolAnd | BoolOr | BoolEQ | BoolNE => Builtin::Bool,
+ NaturalPlus | NaturalTimes => Builtin::Natural,
+ TextAppend => Builtin::Text,
+ ListAppend
+ | RightBiasedRecordMerge
+ | RecursiveRecordMerge
+ | RecursiveRecordTypeMerge
+ | Equivalence => unreachable!(),
+ ImportAlt => unreachable!("ImportAlt leftover in tck"),
+ },
+ );
if *l.ty() != t {
return span_err("BinOpTypeMismatch");
@@ -149,13 +153,13 @@ fn typecheck_binop(
})
}
-fn typecheck_merge(
- env: &TyEnv<'_>,
+fn typecheck_merge<'cx>(
+ env: &TyEnv<'cx>,
span: Span,
- record: &Tir<'_>,
- scrut: &Tir<'_>,
- type_annot: Option<&Tir<'_>>,
-) -> Result<Type, TypeError> {
+ record: &Tir<'cx, '_>,
+ scrut: &Tir<'cx, '_>,
+ type_annot: Option<&Tir<'cx, '_>>,
+) -> Result<Type<'cx>, TypeError> {
let span_err = |msg: &str| mk_span_err(span.clone(), msg);
use NirKind::{OptionalType, PiClosure, RecordType, UnionType};
@@ -287,11 +291,12 @@ fn typecheck_merge(
})
}
-pub fn typecheck_operation(
- env: &TyEnv<'_>,
+pub fn typecheck_operation<'cx>(
+ env: &TyEnv<'cx>,
span: Span,
- opkind: OpKind<Tir<'_>>,
-) -> Result<Type, TypeError> {
+ opkind: OpKind<Tir<'cx, '_>>,
+) -> Result<Type<'cx>, TypeError> {
+ let cx = env.cx();
let span_err = |msg: &str| mk_span_err(span.clone(), msg);
use NirKind::{ListType, PiClosure, RecordType, UnionType};
use OpKind::*;
@@ -347,7 +352,7 @@ pub fn typecheck_operation(
}
BinOp(o, l, r) => typecheck_binop(env, span, o, l, r)?,
BoolIf(x, y, z) => {
- if *x.ty().kind() != NirKind::from_builtin(Builtin::Bool) {
+ if *x.ty().kind() != NirKind::from_builtin(cx, Builtin::Bool) {
return span_err("InvalidPredicate");
}
if y.ty().ty().as_const().is_none() {
@@ -399,7 +404,7 @@ pub fn typecheck_operation(
return span_err(err_msg);
}
match kts.get("mapKey") {
- Some(t) if *t == Nir::from_builtin(Builtin::Text) => {}
+ Some(t) if *t == Nir::from_builtin(cx, Builtin::Text) => {}
_ => return span_err(err_msg),
}
match kts.get("mapValue") {
@@ -418,9 +423,12 @@ pub fn typecheck_operation(
}
let mut kts = HashMap::new();
- kts.insert("mapKey".into(), Nir::from_builtin(Builtin::Text));
+ kts.insert(
+ "mapKey".into(),
+ Nir::from_builtin(cx, Builtin::Text),
+ );
kts.insert("mapValue".into(), entry_type);
- let output_type: Type = Nir::from_builtin(Builtin::List)
+ let output_type: Type = Nir::from_builtin(cx, Builtin::List)
.app(Nir::from_kind(RecordType(kts)))
.to_type(Const::Type);
if let Some(annot) = annot {
diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs
index ec99dbe..30fa8af 100644
--- a/dhall/src/semantics/nze/env.rs
+++ b/dhall/src/semantics/nze/env.rs
@@ -1,4 +1,5 @@
use crate::semantics::{AlphaVar, Nir, NirKind};
+use crate::Ctxt;
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum NzVar {
@@ -9,19 +10,20 @@ pub enum NzVar {
}
#[derive(Debug, Clone)]
-enum EnvItem<Type> {
+enum EnvItem<'cx, T> {
// Variable is bound with given type
- Kept(Type),
+ Kept(T),
// Variable has been replaced by corresponding value
- Replaced(Nir, Type),
+ Replaced(Nir<'cx>, T),
}
#[derive(Debug, Clone)]
-pub struct ValEnv<Type> {
- items: Vec<EnvItem<Type>>,
+pub struct ValEnv<'cx, T> {
+ cx: Ctxt<'cx>,
+ items: Vec<EnvItem<'cx, T>>,
}
-pub type NzEnv = ValEnv<()>;
+pub type NzEnv<'cx> = ValEnv<'cx, ()>;
impl NzVar {
pub fn new(idx: usize) -> Self {
@@ -46,11 +48,17 @@ impl NzVar {
}
}
-impl<Type: Clone> ValEnv<Type> {
- pub fn new() -> Self {
- ValEnv { items: Vec::new() }
+impl<'cx, T: Clone> ValEnv<'cx, T> {
+ pub fn new(cx: Ctxt<'cx>) -> Self {
+ ValEnv {
+ cx,
+ items: Vec::new(),
+ }
+ }
+ pub fn cx(&self) -> Ctxt<'cx> {
+ self.cx
}
- pub fn discard_types(&self) -> ValEnv<()> {
+ pub fn discard_types(&self) -> ValEnv<'cx, ()> {
let items = self
.items
.iter()
@@ -59,27 +67,27 @@ impl<Type: Clone> ValEnv<Type> {
EnvItem::Replaced(val, _) => EnvItem::Replaced(val.clone(), ()),
})
.collect();
- ValEnv { items }
+ ValEnv { cx: self.cx, items }
}
- pub fn insert_type(&self, ty: Type) -> Self {
+ pub fn insert_type(&self, ty: T) -> Self {
let mut env = self.clone();
env.items.push(EnvItem::Kept(ty));
env
}
- pub fn insert_value(&self, e: Nir, ty: Type) -> Self {
+ pub fn insert_value(&self, e: Nir<'cx>, ty: T) -> Self {
let mut env = self.clone();
env.items.push(EnvItem::Replaced(e, ty));
env
}
- pub fn lookup_val(&self, var: AlphaVar) -> NirKind {
+ pub fn lookup_val(&self, var: AlphaVar) -> NirKind<'cx> {
let idx = self.items.len() - 1 - var.idx();
match &self.items[idx] {
EnvItem::Kept(_) => NirKind::Var(NzVar::new(idx)),
EnvItem::Replaced(x, _) => x.kind().clone(),
}
}
- pub fn lookup_ty(&self, var: AlphaVar) -> Type {
+ pub fn lookup_ty(&self, var: AlphaVar) -> T {
let idx = self.items.len() - 1 - var.idx();
match &self.items[idx] {
EnvItem::Kept(ty) | EnvItem::Replaced(_, ty) => ty.clone(),
@@ -87,8 +95,8 @@ impl<Type: Clone> ValEnv<Type> {
}
}
-impl<'a> From<&'a NzEnv> for NzEnv {
- fn from(x: &'a NzEnv) -> Self {
+impl<'cx, 'a> From<&'a NzEnv<'cx>> for NzEnv<'cx> {
+ fn from(x: &'a NzEnv<'cx>) -> Self {
x.clone()
}
}
diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs
index 7bda836..538b8ea 100644
--- a/dhall/src/semantics/nze/nir.rs
+++ b/dhall/src/semantics/nze/nir.rs
@@ -11,7 +11,7 @@ use crate::semantics::{
use crate::syntax::{
Const, Expr, ExprKind, InterpolatedTextContents, Label, NumKind, Span,
};
-use crate::ToExprOptions;
+use crate::{Ctxt, ToExprOptions};
/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation
/// automatically. Uses a Rc<OnceCell> to share computation.
@@ -20,31 +20,31 @@ use crate::ToExprOptions;
/// normalize as needed.
/// Stands for "Normalized Intermediate Representation"
#[derive(Clone)]
-pub struct Nir(Rc<lazy::Lazy<Thunk, NirKind>>);
+pub struct Nir<'cx>(Rc<lazy::Lazy<Thunk<'cx>, NirKind<'cx>>>);
/// An unevaluated subexpression
#[derive(Debug, Clone)]
-pub enum Thunk {
+pub enum Thunk<'cx> {
/// A completely unnormalized expression.
- Thunk { env: NzEnv, body: Hir },
+ Thunk { env: NzEnv<'cx>, body: Hir<'cx> },
/// A partially normalized expression that may need to go through `normalize_one_layer`.
- PartialExpr { env: NzEnv, expr: ExprKind<Nir> },
+ PartialExpr { expr: ExprKind<Nir<'cx>> },
}
/// An unevaluated subexpression that takes an argument.
#[derive(Debug, Clone)]
-pub enum Closure {
+pub enum Closure<'cx> {
/// Normal closure
- Closure { env: NzEnv, body: Hir },
+ Closure { env: NzEnv<'cx>, body: Hir<'cx> },
/// Closure that ignores the argument passed
- ConstantClosure { body: Nir },
+ ConstantClosure { body: Nir<'cx> },
}
/// A text literal with interpolations.
// Invariant: this must not contain interpolations that are themselves TextLits, and contiguous
// text values must be merged.
#[derive(Debug, Clone, PartialEq, Eq)]
-pub struct TextLit(Vec<InterpolatedTextContents<Nir>>);
+pub struct TextLit<'cx>(Vec<InterpolatedTextContents<Nir<'cx>>>);
/// This represents a value in Weak Head Normal Form (WHNF). This means that the value is
/// normalized up to the first constructor, but subexpressions may not be fully normalized.
@@ -54,67 +54,65 @@ pub struct TextLit(Vec<InterpolatedTextContents<Nir>>);
/// In particular, this means that once we get a `NirKind`, it can be considered immutable, and
/// we only need to recursively normalize its sub-`Nir`s to get to the NF.
#[derive(Debug, Clone, PartialEq, Eq)]
-pub enum NirKind {
+pub enum NirKind<'cx> {
/// Closures
LamClosure {
binder: Binder,
- annot: Nir,
- closure: Closure,
+ annot: Nir<'cx>,
+ closure: Closure<'cx>,
},
PiClosure {
binder: Binder,
- annot: Nir,
- closure: Closure,
+ annot: Nir<'cx>,
+ closure: Closure<'cx>,
},
- AppliedBuiltin(BuiltinClosure),
+ AppliedBuiltin(BuiltinClosure<'cx>),
Var(NzVar),
Const(Const),
Num(NumKind),
// Must be a number type, Bool or Text
BuiltinType(Builtin),
- TextLit(TextLit),
- EmptyOptionalLit(Nir),
- NEOptionalLit(Nir),
- OptionalType(Nir),
+ TextLit(TextLit<'cx>),
+ EmptyOptionalLit(Nir<'cx>),
+ NEOptionalLit(Nir<'cx>),
+ OptionalType(Nir<'cx>),
// EmptyListLit(t) means `[] : List t`, not `[] : t`
- EmptyListLit(Nir),
- NEListLit(Vec<Nir>),
- ListType(Nir),
- RecordLit(HashMap<Label, Nir>),
- RecordType(HashMap<Label, Nir>),
- UnionConstructor(Label, HashMap<Label, Option<Nir>>),
- UnionLit(Label, Nir, HashMap<Label, Option<Nir>>),
- UnionType(HashMap<Label, Option<Nir>>),
- Equivalence(Nir, Nir),
- Assert(Nir),
+ EmptyListLit(Nir<'cx>),
+ NEListLit(Vec<Nir<'cx>>),
+ ListType(Nir<'cx>),
+ RecordLit(HashMap<Label, Nir<'cx>>),
+ RecordType(HashMap<Label, Nir<'cx>>),
+ UnionConstructor(Label, HashMap<Label, Option<Nir<'cx>>>),
+ UnionLit(Label, Nir<'cx>, HashMap<Label, Option<Nir<'cx>>>),
+ UnionType(HashMap<Label, Option<Nir<'cx>>>),
+ Equivalence(Nir<'cx>, Nir<'cx>),
+ Assert(Nir<'cx>),
/// Invariant: evaluation must not be able to progress with `normalize_operation`.
/// This is used when an operation couldn't proceed further, for example because of variables.
- Op(OpKind<Nir>),
+ Op(OpKind<Nir<'cx>>),
}
-impl Nir {
+impl<'cx> Nir<'cx> {
/// Construct a Nir from a completely unnormalized expression.
- pub fn new_thunk(env: NzEnv, hir: Hir) -> Nir {
+ pub fn new_thunk(env: NzEnv<'cx>, hir: Hir<'cx>) -> Self {
Nir(Rc::new(lazy::Lazy::new(Thunk::new(env, hir))))
}
/// Construct a Nir from a partially normalized expression that's not in WHNF.
- pub fn from_partial_expr(e: ExprKind<Nir>) -> Nir {
- // TODO: env
- let env = NzEnv::new();
- Nir(Rc::new(lazy::Lazy::new(Thunk::from_partial_expr(env, e))))
+ pub fn from_partial_expr(e: ExprKind<Self>) -> Self {
+ Nir(Rc::new(lazy::Lazy::new(Thunk::from_partial_expr(e))))
}
/// Make a Nir from a NirKind
- pub fn from_kind(v: NirKind) -> Nir {
+ pub fn from_kind(v: NirKind<'cx>) -> Self {
Nir(Rc::new(lazy::Lazy::new_completed(v)))
}
pub fn from_const(c: Const) -> Self {
Self::from_kind(NirKind::Const(c))
}
- pub fn from_builtin(b: Builtin) -> Self {
- Self::from_builtin_env(b, &NzEnv::new())
+ pub fn from_builtin(cx: Ctxt<'cx>, b: Builtin) -> Self {
+ Self::from_builtin_env(b, &NzEnv::new(cx))
}
- pub fn from_builtin_env(b: Builtin, env: &NzEnv) -> Self {
+ pub fn from_builtin_env(b: Builtin, env: &NzEnv<'cx>) -> Self {
Nir::from_kind(NirKind::from_builtin_env(b, env.clone()))
}
pub fn from_text(txt: impl ToString) -> Self {
@@ -129,51 +127,54 @@ impl Nir {
}
/// This is what you want if you want to pattern-match on the value.
- pub fn kind(&self) -> &NirKind {
+ pub fn kind(&self) -> &NirKind<'cx> {
&*self.0
}
/// The contents of a `Nir` are immutable and shared. If however we happen to be the sole
/// owners, we can mutate it directly. Otherwise, this clones the internal value first.
- pub fn kind_mut(&mut self) -> &mut NirKind {
+ pub fn kind_mut(&mut self) -> &mut NirKind<'cx> {
Rc::make_mut(&mut self.0).get_mut()
}
/// If we are the sole owner of this Nir, we can avoid a clone.
- pub fn into_kind(self) -> NirKind {
+ pub fn into_kind(self) -> NirKind<'cx> {
match Rc::try_unwrap(self.0) {
Ok(lazy) => lazy.into_inner(),
Err(rc) => (**rc).clone(),
}
}
- pub fn to_type(&self, u: impl Into<Universe>) -> Type {
+ pub fn to_type(&self, u: impl Into<Universe>) -> Type<'cx> {
Type::new(self.clone(), u.into())
}
/// Converts a value back to the corresponding AST expression.
pub fn to_expr(&self, opts: ToExprOptions) -> Expr {
self.to_hir_noenv().to_expr(opts)
}
- pub fn to_expr_tyenv(&self, tyenv: &TyEnv) -> Expr {
+ pub fn to_expr_tyenv(&self, tyenv: &TyEnv<'cx>) -> Expr {
self.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv)
}
- pub fn app(&self, v: Nir) -> Nir {
+ pub fn app(&self, v: Self) -> Self {
Nir::from_kind(self.app_to_kind(v))
}
- pub fn app_to_kind(&self, v: Nir) -> NirKind {
+ pub fn app_to_kind(&self, v: Self) -> NirKind<'cx> {
apply_any(self, v)
}
- pub fn to_hir(&self, venv: VarEnv) -> Hir {
- let map_uniontype = |kts: &HashMap<Label, Option<Nir>>| {
- ExprKind::UnionType(
- kts.iter()
- .map(|(k, v)| {
- (k.clone(), v.as_ref().map(|v| v.to_hir(venv)))
- })
- .collect(),
- )
- };
+ pub fn to_hir(&self, venv: VarEnv) -> Hir<'cx> {
+ let map_uniontype =
+ |kts: &HashMap<Label, Option<Nir<'cx>>>| -> ExprKind<Hir<'cx>> {
+ ExprKind::UnionType(
+ kts.iter()
+ .map(|(k, v)| {
+ (k.clone(), v.as_ref().map(|v| v.to_hir(venv)))
+ })
+ .collect(),
+ )
+ };
+ let builtin =
+ |b| Hir::new(HirKind::Expr(ExprKind::Builtin(b)), Span::Artificial);
let hir = match self.kind() {
NirKind::Var(v) => HirKind::Var(venv.lookup(*v)),
@@ -204,21 +205,21 @@ impl Nir {
NirKind::BuiltinType(b) => ExprKind::Builtin(*b),
NirKind::Num(l) => ExprKind::Num(l.clone()),
NirKind::OptionalType(t) => ExprKind::Op(OpKind::App(
- Nir::from_builtin(Builtin::Optional).to_hir(venv),
+ builtin(Builtin::Optional),
t.to_hir(venv),
)),
NirKind::EmptyOptionalLit(n) => ExprKind::Op(OpKind::App(
- Nir::from_builtin(Builtin::OptionalNone).to_hir(venv),
+ builtin(Builtin::OptionalNone),
n.to_hir(venv),
)),
NirKind::NEOptionalLit(n) => ExprKind::SomeLit(n.to_hir(venv)),
NirKind::ListType(t) => ExprKind::Op(OpKind::App(
- Nir::from_builtin(Builtin::List).to_hir(venv),
+ builtin(Builtin::List),
t.to_hir(venv),
)),
NirKind::EmptyListLit(n) => ExprKind::EmptyListLit(Hir::new(
HirKind::Expr(ExprKind::Op(OpKind::App(
- Nir::from_builtin(Builtin::List).to_hir(venv),
+ builtin(Builtin::List),
n.to_hir(venv),
))),
Span::Artificial,
@@ -276,52 +277,52 @@ impl Nir {
Hir::new(hir, Span::Artificial)
}
- pub fn to_hir_noenv(&self) -> Hir {
+ pub fn to_hir_noenv(&self) -> Hir<'cx> {
self.to_hir(VarEnv::new())
}
}
-impl NirKind {
- pub fn into_nir(self) -> Nir {
+impl<'cx> NirKind<'cx> {
+ pub fn into_nir(self) -> Nir<'cx> {
Nir::from_kind(self)
}
- pub fn from_builtin(b: Builtin) -> NirKind {
- NirKind::from_builtin_env(b, NzEnv::new())
+ pub fn from_builtin(cx: Ctxt<'cx>, b: Builtin) -> Self {
+ NirKind::from_builtin_env(b, NzEnv::new(cx))
}
- pub fn from_builtin_env(b: Builtin, env: NzEnv) -> NirKind {
+ pub fn from_builtin_env(b: Builtin, env: NzEnv<'cx>) -> Self {
BuiltinClosure::new(b, env)
}
}
-impl Thunk {
- fn new(env: NzEnv, body: Hir) -> Self {
+impl<'cx> Thunk<'cx> {
+ fn new(env: NzEnv<'cx>, body: Hir<'cx>) -> Self {
Thunk::Thunk { env, body }
}
- fn from_partial_expr(env: NzEnv, expr: ExprKind<Nir>) -> Self {
- Thunk::PartialExpr { env, expr }
+ fn from_partial_expr(expr: ExprKind<Nir<'cx>>) -> Self {
+ Thunk::PartialExpr { expr }
}
- fn eval(self) -> NirKind {
+ fn eval(self) -> NirKind<'cx> {
match self {
- Thunk::Thunk { env, body } => normalize_hir(&env, &body),
- Thunk::PartialExpr { env, expr } => normalize_one_layer(expr, &env),
+ Thunk::Thunk { env, body, .. } => normalize_hir(&env, &body),
+ Thunk::PartialExpr { expr } => normalize_one_layer(expr),
}
}
}
-impl Closure {
- pub fn new(env: &NzEnv, body: Hir) -> Self {
+impl<'cx> Closure<'cx> {
+ pub fn new(env: &NzEnv<'cx>, body: Hir<'cx>) -> Self {
Closure::Closure {
env: env.clone(),
body,
}
}
/// New closure that ignores its argument
- pub fn new_constant(body: Nir) -> Self {
+ pub fn new_constant(body: Nir<'cx>) -> Self {
Closure::ConstantClosure { body }
}
- pub fn apply(&self, val: Nir) -> Nir {
+ pub fn apply(&self, val: Nir<'cx>) -> Nir<'cx> {
match self {
Closure::Closure { env, body, .. } => {
body.eval(env.insert_value(val, ()))
@@ -329,7 +330,7 @@ impl Closure {
Closure::ConstantClosure { body, .. } => body.clone(),
}
}
- fn apply_var(&self, var: NzVar) -> Nir {
+ fn apply_var(&self, var: NzVar) -> Nir<'cx> {
match self {
Closure::Closure { .. } => {
self.apply(Nir::from_kind(NirKind::Var(var)))
@@ -339,13 +340,13 @@ impl Closure {
}
/// Convert this closure to a Hir expression
- pub fn to_hir(&self, venv: VarEnv) -> Hir {
+ pub fn to_hir(&self, venv: VarEnv) -> Hir<'cx> {
self.apply_var(NzVar::new(venv.size()))
.to_hir(venv.insert())
}
/// If the closure variable is free in the closure, return Err. Otherwise, return the value
/// with that free variable remove.
- pub fn remove_binder(&self) -> Result<Nir, ()> {
+ pub fn remove_binder(&self) -> Result<Nir<'cx>, ()> {
match self {
Closure::Closure { .. } => {
let v = NzVar::fresh();
@@ -358,20 +359,20 @@ impl Closure {
}
}
-impl TextLit {
+impl<'cx> TextLit<'cx> {
pub fn new(
- elts: impl Iterator<Item = InterpolatedTextContents<Nir>>,
+ elts: impl Iterator<Item = InterpolatedTextContents<Nir<'cx>>>,
) -> Self {
TextLit(squash_textlit(elts))
}
- pub fn interpolate(v: Nir) -> TextLit {
+ pub fn interpolate(v: Nir<'cx>) -> Self {
TextLit(vec![InterpolatedTextContents::Expr(v)])
}
- pub fn from_text(s: String) -> TextLit {
+ pub fn from_text(s: String) -> Self {
TextLit(vec![InterpolatedTextContents::Text(s)])
}
- pub fn concat(&self, other: &TextLit) -> TextLit {
+ pub fn concat(&self, other: &Self) -> Self {
TextLit::new(self.iter().chain(other.iter()).cloned())
}
pub fn is_empty(&self) -> bool {
@@ -379,7 +380,7 @@ impl TextLit {
}
/// If the literal consists of only one interpolation and not text, return the interpolated
/// value.
- pub fn as_single_expr(&self) -> Option<&Nir> {
+ pub fn as_single_expr(&self) -> Option<&Nir<'cx>> {
use InterpolatedTextContents::Expr;
if let [Expr(v)] = self.0.as_slice() {
Some(v)
@@ -398,43 +399,45 @@ impl TextLit {
None
}
}
- pub fn iter(&self) -> impl Iterator<Item = &InterpolatedTextContents<Nir>> {
+ pub fn iter(
+ &self,
+ ) -> impl Iterator<Item = &InterpolatedTextContents<Nir<'cx>>> {
self.0.iter()
}
}
-impl lazy::Eval<NirKind> for Thunk {
- fn eval(self) -> NirKind {
+impl<'cx> lazy::Eval<NirKind<'cx>> for Thunk<'cx> {
+ fn eval(self) -> NirKind<'cx> {
self.eval()
}
}
/// Compare two values for equality modulo alpha/beta-equivalence.
-impl std::cmp::PartialEq for Nir {
+impl<'cx> std::cmp::PartialEq for Nir<'cx> {
fn eq(&self, other: &Self) -> bool {
Rc::ptr_eq(&self.0, &other.0) || self.kind() == other.kind()
}
}
-impl std::cmp::Eq for Nir {}
+impl<'cx> std::cmp::Eq for Nir<'cx> {}
-impl std::cmp::PartialEq for Thunk {
+impl<'cx> std::cmp::PartialEq for Thunk<'cx> {
fn eq(&self, _other: &Self) -> bool {
unreachable!(
"Trying to compare thunks but we should only compare WHNFs"
)
}
}
-impl std::cmp::Eq for Thunk {}
+impl<'cx> std::cmp::Eq for Thunk<'cx> {}
-impl std::cmp::PartialEq for Closure {
+impl<'cx> std::cmp::PartialEq for Closure<'cx> {
fn eq(&self, other: &Self) -> bool {
let v = NzVar::fresh();
self.apply_var(v) == other.apply_var(v)
}
}
-impl std::cmp::Eq for Closure {}
+impl<'cx> std::cmp::Eq for Closure<'cx> {}
-impl std::fmt::Debug for Nir {
+impl<'cx> std::fmt::Debug for Nir<'cx> {
fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
if let NirKind::Const(c) = self.kind() {
return write!(fmt, "{:?}", c);
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 62efc5f..cce421d 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -5,7 +5,7 @@ use crate::semantics::NzEnv;
use crate::semantics::{Binder, Closure, Hir, HirKind, Nir, NirKind, TextLit};
use crate::syntax::{ExprKind, InterpolatedTextContents};
-pub fn apply_any(f: &Nir, a: Nir) -> NirKind {
+pub fn apply_any<'cx>(f: &Nir<'cx>, a: Nir<'cx>) -> NirKind<'cx> {
match f.kind() {
NirKind::LamClosure { closure, .. } => closure.apply(a).kind().clone(),
NirKind::AppliedBuiltin(closure) => closure.apply(a),
@@ -16,16 +16,16 @@ pub fn apply_any(f: &Nir, a: Nir) -> NirKind {
}
}
-pub fn squash_textlit(
- elts: impl Iterator<Item = InterpolatedTextContents<Nir>>,
-) -> Vec<InterpolatedTextContents<Nir>> {
+pub fn squash_textlit<'cx>(
+ elts: impl Iterator<Item = InterpolatedTextContents<Nir<'cx>>>,
+) -> Vec<InterpolatedTextContents<Nir<'cx>>> {
use std::mem::replace;
use InterpolatedTextContents::{Expr, Text};
- fn inner(
- elts: impl Iterator<Item = InterpolatedTextContents<Nir>>,
+ fn inner<'cx>(
+ elts: impl Iterator<Item = InterpolatedTextContents<Nir<'cx>>>,
crnt_str: &mut String,
- ret: &mut Vec<InterpolatedTextContents<Nir>>,
+ ret: &mut Vec<InterpolatedTextContents<Nir<'cx>>>,
) {
for contents in elts {
match contents {
@@ -81,22 +81,22 @@ where
kvs
}
-pub type Ret = NirKind;
+pub type Ret<'cx> = NirKind<'cx>;
-pub fn ret_nir(x: Nir) -> Ret {
+pub fn ret_nir<'cx>(x: Nir<'cx>) -> Ret<'cx> {
x.into_kind()
}
-pub fn ret_kind(x: NirKind) -> Ret {
+pub fn ret_kind<'cx>(x: NirKind<'cx>) -> Ret<'cx> {
x
}
-pub fn ret_ref(x: &Nir) -> Ret {
+pub fn ret_ref<'cx>(x: &Nir<'cx>) -> Ret<'cx> {
x.kind().clone()
}
-pub fn ret_op(x: OpKind<Nir>) -> Ret {
+pub fn ret_op<'cx>(x: OpKind<Nir<'cx>>) -> Ret<'cx> {
NirKind::Op(x)
}
-pub fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
+pub fn normalize_one_layer<'cx>(expr: ExprKind<Nir<'cx>>) -> NirKind<'cx> {
use NirKind::{
Assert, Const, NEListLit, NEOptionalLit, Num, RecordLit, RecordType,
UnionType,
@@ -106,15 +106,13 @@ pub fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
ExprKind::Var(..)
| ExprKind::Lam(..)
| ExprKind::Pi(..)
- | ExprKind::Let(..) => {
+ | ExprKind::Let(..)
+ | ExprKind::Builtin(..) => {
unreachable!("This case should have been handled in normalize_hir")
}
ExprKind::Const(c) => ret_kind(Const(c)),
ExprKind::Num(l) => ret_kind(Num(l)),
- ExprKind::Builtin(b) => {
- ret_kind(NirKind::from_builtin_env(b, env.clone()))
- }
ExprKind::TextLit(elts) => {
let tlit = TextLit::new(elts.into_iter());
// Simplify bare interpolation
@@ -154,7 +152,7 @@ pub fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
}
/// Normalize Hir into WHNF
-pub fn normalize_hir(env: &NzEnv, hir: &Hir) -> NirKind {
+pub fn normalize_hir<'cx>(env: &NzEnv<'cx>, hir: &Hir<'cx>) -> NirKind<'cx> {
match hir.kind() {
HirKind::Var(var) => env.lookup_val(*var),
HirKind::Import(hir, _) => normalize_hir(env, hir),
@@ -178,9 +176,12 @@ pub fn normalize_hir(env: &NzEnv, hir: &Hir) -> NirKind {
let val = val.eval(env);
body.eval(env.insert_value(val, ())).kind().clone()
}
+ HirKind::Expr(ExprKind::Builtin(b)) => {
+ NirKind::from_builtin_env(*b, env.clone())
+ }
HirKind::Expr(e) => {
let e = e.map_ref(|hir| hir.eval(env));
- normalize_one_layer(e, env)
+ normalize_one_layer(e)
}
}
}
diff --git a/dhall/src/semantics/resolve/cache.rs b/dhall/src/semantics/resolve/cache.rs
index b00a2d5..59463dd 100644
--- a/dhall/src/semantics/resolve/cache.rs
+++ b/dhall/src/semantics/resolve/cache.rs
@@ -5,7 +5,7 @@ use std::path::{Path, PathBuf};
use crate::error::{CacheError, Error};
use crate::parse::parse_binary;
use crate::syntax::{binary, Hash};
-use crate::Typed;
+use crate::{Ctxt, Typed};
use std::ffi::OsStr;
use std::fs::File;
@@ -52,9 +52,13 @@ impl Cache {
self.cache_dir.join(filename_for_hash(hash))
}
- pub fn get(&self, hash: &Hash) -> Result<Typed, Error> {
+ pub fn get<'cx>(
+ &self,
+ cx: Ctxt<'cx>,
+ hash: &Hash,
+ ) -> Result<Typed<'cx>, Error> {
let path = self.entry_path(hash);
- let res = read_cache_file(&path, hash);
+ let res = read_cache_file(cx, &path, hash);
if res.is_err() && path.exists() {
// Delete cache file since it's invalid. We ignore the error.
let _ = std::fs::remove_file(&path);
@@ -62,14 +66,22 @@ impl Cache {
res
}
- pub fn insert(&self, hash: &Hash, expr: &Typed) -> Result<(), Error> {
+ pub fn insert<'cx>(
+ &self,
+ hash: &Hash,
+ expr: &Typed<'cx>,
+ ) -> Result<(), Error> {
let path = self.entry_path(hash);
write_cache_file(&path, expr)
}
}
/// Read a file from the cache, also checking that its hash is valid.
-fn read_cache_file(path: &Path, hash: &Hash) -> Result<Typed, Error> {
+fn read_cache_file<'cx>(
+ cx: Ctxt<'cx>,
+ path: &Path,
+ hash: &Hash,
+) -> Result<Typed<'cx>, Error> {
let data = crate::utils::read_binary_file(path)?;
match hash {
@@ -81,7 +93,7 @@ fn read_cache_file(path: &Path, hash: &Hash) -> Result<Typed, Error> {
}
}
- Ok(parse_binary(&data)?.skip_resolve()?.typecheck()?)
+ Ok(parse_binary(&data)?.skip_resolve()?.typecheck(cx)?)
}
/// Write a file to the cache.
diff --git a/dhall/src/semantics/resolve/env.rs b/dhall/src/semantics/resolve/env.rs
index 82f21e8..2b998f8 100644
--- a/dhall/src/semantics/resolve/env.rs
+++ b/dhall/src/semantics/resolve/env.rs
@@ -86,9 +86,12 @@ impl<'cx> ImportEnv<'cx> {
Some(*self.mem_cache.get(location)?)
}
- pub fn get_from_disk_cache(&self, hash: &Option<Hash>) -> Option<Typed> {
+ pub fn get_from_disk_cache(
+ &self,
+ hash: &Option<Hash>,
+ ) -> Option<Typed<'cx>> {
let hash = hash.as_ref()?;
- let expr = self.disk_cache.as_ref()?.get(hash).ok()?;
+ let expr = self.disk_cache.as_ref()?.get(self.cx(), hash).ok()?;
Some(expr)
}
@@ -100,7 +103,7 @@ impl<'cx> ImportEnv<'cx> {
self.mem_cache.insert(location, result);
}
- pub fn write_to_disk_cache(&self, hash: &Option<Hash>, expr: &Typed) {
+ pub fn write_to_disk_cache(&self, hash: &Option<Hash>, expr: &Typed<'cx>) {
if let Some(disk_cache) = self.disk_cache.as_ref() {
if let Some(hash) = hash {
let _ = disk_cache.insert(hash, &expr);
@@ -111,8 +114,8 @@ impl<'cx> ImportEnv<'cx> {
pub fn with_cycle_detection(
&mut self,
location: ImportLocation,
- do_resolve: impl FnOnce(&mut Self) -> Result<Typed, Error>,
- ) -> Result<Typed, Error> {
+ do_resolve: impl FnOnce(&mut Self) -> Result<Typed<'cx>, Error>,
+ ) -> Result<Typed<'cx>, Error> {
if self.stack.contains(&location) {
return Err(
ImportError::ImportCycle(self.stack.clone(), location).into()
diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs
index c2d1883..c67ab75 100644
--- a/dhall/src/semantics/resolve/hir.rs
+++ b/dhall/src/semantics/resolve/hir.rs
@@ -10,19 +10,19 @@ pub struct AlphaVar {
}
#[derive(Debug, Clone, PartialEq, Eq)]
-pub enum HirKind {
+pub enum HirKind<'cx> {
/// A resolved variable (i.e. a DeBruijn index)
Var(AlphaVar),
/// Result of resolving an import.
- Import(Hir, Type),
+ Import(Hir<'cx>, Type<'cx>),
// Forbidden ExprKind variants: Var, Import, Completion
- Expr(ExprKind<Hir>),
+ Expr(ExprKind<Hir<'cx>>),
}
// An expression with resolved variables and imports.
#[derive(Debug, Clone)]
-pub struct Hir {
- kind: Box<HirKind>,
+pub struct Hir<'cx> {
+ kind: Box<HirKind<'cx>>,
span: Span,
}
@@ -35,15 +35,15 @@ impl AlphaVar {
}
}
-impl Hir {
- pub fn new(kind: HirKind, span: Span) -> Self {
+impl<'cx> Hir<'cx> {
+ pub fn new(kind: HirKind<'cx>, span: Span) -> Self {
Hir {
kind: Box::new(kind),
span,
}
}
- pub fn kind(&self) -> &HirKind {
+ pub fn kind(&self) -> &HirKind<'cx> {
&*self.kind
}
pub fn span(&self) -> Span {
@@ -63,7 +63,7 @@ impl Hir {
let opts = ToExprOptions { alpha: true };
self.to_expr(opts)
}
- pub fn to_expr_tyenv(&self, env: &TyEnv) -> Expr {
+ pub fn to_expr_tyenv(&self, env: &TyEnv<'cx>) -> Expr {
let opts = ToExprOptions { alpha: false };
let mut env = env.as_nameenv().clone();
hir_to_expr(self, opts, &mut env)
@@ -72,29 +72,33 @@ impl Hir {
/// Typecheck the Hir.
pub fn typecheck<'hir>(
&'hir self,
- env: &TyEnv,
- ) -> Result<Tir<'hir>, TypeError> {
+ env: &TyEnv<'cx>,
+ ) -> Result<Tir<'cx, 'hir>, TypeError> {
type_with(env, self, None)
}
pub fn typecheck_noenv<'hir>(
&'hir self,
- cx: Ctxt<'_>,
- ) -> Result<Tir<'hir>, TypeError> {
+ cx: Ctxt<'cx>,
+ ) -> Result<Tir<'cx, 'hir>, TypeError> {
self.typecheck(&TyEnv::new(cx))
}
/// Eval the Hir. 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> {
Nir::new_thunk(env.into(), self.clone())
}
/// Eval a closed Hir (i.e. without free variables). It will actually get evaluated only as
/// needed on demand.
- pub fn eval_closed_expr(&self) -> Nir {
- self.eval(NzEnv::new())
+ pub fn eval_closed_expr(&self, cx: Ctxt<'cx>) -> Nir<'cx> {
+ self.eval(NzEnv::new(cx))
}
}
-fn hir_to_expr(hir: &Hir, opts: ToExprOptions, env: &mut NameEnv) -> Expr {
+fn hir_to_expr<'cx>(
+ hir: &Hir<'cx>,
+ opts: ToExprOptions,
+ env: &mut NameEnv,
+) -> Expr {
let kind = match hir.kind() {
HirKind::Var(v) if opts.alpha => ExprKind::Var(V("_".into(), v.idx())),
HirKind::Var(v) => ExprKind::Var(env.label_var(*v)),
@@ -127,9 +131,9 @@ fn hir_to_expr(hir: &Hir, opts: ToExprOptions, env: &mut NameEnv) -> Expr {
Expr::new(kind, hir.span())
}
-impl std::cmp::PartialEq for Hir {
+impl<'cx> std::cmp::PartialEq for Hir<'cx> {
fn eq(&self, other: &Self) -> bool {
self.kind == other.kind
}
}
-impl std::cmp::Eq for Hir {}
+impl<'cx> std::cmp::Eq for Hir<'cx> {}
diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs
index cf72f80..488c516 100644
--- a/dhall/src/semantics/resolve/resolve.rs
+++ b/dhall/src/semantics/resolve/resolve.rs
@@ -231,12 +231,13 @@ impl ImportLocation {
&self,
env: &mut ImportEnv<'cx>,
span: Span,
- ) -> Result<Typed, Error> {
+ ) -> Result<Typed<'cx>, Error> {
let (hir, ty) = match self.mode {
ImportMode::Code => {
let parsed = self.kind.fetch_dhall()?;
- let typed = resolve_with_env(env, parsed)?.typecheck()?;
- let hir = typed.normalize().to_hir();
+ let typed =
+ resolve_with_env(env, parsed)?.typecheck(env.cx())?;
+ let hir = typed.normalize(env.cx()).to_hir();
(hir, typed.ty)
}
ImportMode::RawText => {
@@ -245,7 +246,7 @@ impl ImportLocation {
HirKind::Expr(ExprKind::TextLit(text.into())),
span,
);
- (hir, Type::from_builtin(Builtin::Text))
+ (hir, Type::from_builtin(env.cx(), Builtin::Text))
}
ImportMode::Location => {
let expr = self.kind.to_location();
@@ -286,7 +287,11 @@ fn make_aslocation_uniontype() -> Expr {
mkexpr(ExprKind::UnionType(union))
}
-fn check_hash(import: &Import, typed: &Typed, span: Span) -> Result<(), Error> {
+fn check_hash<'cx>(
+ import: &Import,
+ typed: &Typed<'cx>,
+ span: Span,
+) -> Result<(), Error> {
if let (ImportMode::Code, Some(Hash::SHA256(hash))) =
(import.mode, &import.hash)
{
@@ -338,11 +343,11 @@ fn desugar(expr: &Expr) -> Cow<'_, Expr> {
/// Traverse the expression, handling import alternatives and passing
/// found imports to the provided function. Also resolving names.
-fn traverse_resolve_expr(
+fn traverse_resolve_expr<'cx>(
name_env: &mut NameEnv,
expr: &Expr,
- f: &mut impl FnMut(Import, Span) -> Result<Typed, Error>,
-) -> Result<Hir, Error> {
+ f: &mut impl FnMut(Import, Span) -> Result<Typed<'cx>, Error>,
+) -> Result<Hir<'cx>, Error> {
let expr = desugar(expr);
Ok(match expr.kind() {
ExprKind::Var(var) => match name_env.unlabel_var(&var) {
@@ -447,7 +452,7 @@ fn fetch_import<'cx>(
fn resolve_with_env<'cx>(
env: &mut ImportEnv<'cx>,
parsed: Parsed,
-) -> Result<Resolved, Error> {
+) -> Result<Resolved<'cx>, Error> {
let Parsed(expr, base_location) = parsed;
let resolved = traverse_resolve_expr(
&mut NameEnv::new(),
@@ -463,17 +468,20 @@ fn resolve_with_env<'cx>(
Ok(Resolved(resolved))
}
-pub fn resolve(cx: Ctxt<'_>, parsed: Parsed) -> Result<Resolved, Error> {
+pub fn resolve<'cx>(
+ cx: Ctxt<'cx>,
+ parsed: Parsed,
+) -> Result<Resolved<'cx>, Error> {
resolve_with_env(&mut ImportEnv::new(cx), parsed)
}
-pub fn skip_resolve_expr(expr: &Expr) -> Result<Hir, Error> {
+pub fn skip_resolve_expr<'cx>(expr: &Expr) -> Result<Hir<'cx>, Error> {
traverse_resolve_expr(&mut NameEnv::new(), expr, &mut |import, _span| {
Err(ImportError::UnexpectedImport(import).into())
})
}
-pub fn skip_resolve(parsed: Parsed) -> Result<Resolved, Error> {
+pub fn skip_resolve<'cx>(parsed: Parsed) -> Result<Resolved<'cx>, Error> {
let Parsed(expr, _) = parsed;
let resolved = skip_resolve_expr(&expr)?;
Ok(Resolved(resolved))
diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index fc0ce9f..fdcc62d 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -13,7 +13,7 @@ pub struct VarEnv {
pub struct TyEnv<'cx> {
cx: Ctxt<'cx>,
names: NameEnv,
- items: ValEnv<Type>,
+ items: ValEnv<'cx, Type<'cx>>,
}
impl VarEnv {
@@ -45,7 +45,7 @@ impl<'cx> TyEnv<'cx> {
TyEnv {
cx,
names: NameEnv::new(),
- items: ValEnv::new(),
+ items: ValEnv::new(cx),
}
}
pub fn cx(&self) -> Ctxt<'cx> {
@@ -54,34 +54,34 @@ impl<'cx> TyEnv<'cx> {
pub fn as_varenv(&self) -> VarEnv {
self.names.as_varenv()
}
- pub fn to_nzenv(&self) -> NzEnv {
+ pub fn to_nzenv(&self) -> NzEnv<'cx> {
self.items.discard_types()
}
pub fn as_nameenv(&self) -> &NameEnv {
&self.names
}
- pub fn insert_type(&self, x: &Label, ty: Type) -> Self {
+ pub fn insert_type(&self, x: &Label, ty: Type<'cx>) -> 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 {
+ pub fn insert_value(&self, x: &Label, e: Nir<'cx>, ty: Type<'cx>) -> Self {
TyEnv {
cx: self.cx,
names: self.names.insert(x),
items: self.items.insert_value(e, ty),
}
}
- pub fn lookup(&self, var: AlphaVar) -> Type {
+ pub fn lookup(&self, var: AlphaVar) -> Type<'cx> {
self.items.lookup_ty(var)
}
}
-impl<'a, 'cx> From<&'a TyEnv<'cx>> for NzEnv {
- fn from(x: &'a TyEnv) -> Self {
+impl<'a, 'cx> From<&'a TyEnv<'cx>> for NzEnv<'cx> {
+ fn from(x: &'a TyEnv<'cx>) -> Self {
x.to_nzenv()
}
}
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),
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 7e8c0e1..8218368 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -29,11 +29,12 @@ 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<'_>,
- ekind: ExprKind<Tir<'_>>,
+fn type_one_layer<'cx>(
+ env: &TyEnv<'cx>,
+ ekind: ExprKind<Tir<'cx, '_>>,
span: Span,
-) -> Result<Type, TypeError> {
+) -> Result<Type<'cx>, TypeError> {
+ let cx = env.cx();
let span_err = |msg: &str| mk_span_err(span.clone(), msg);
Ok(match ekind {
@@ -51,18 +52,21 @@ fn type_one_layer(
ExprKind::Const(Const::Type) => Type::from_const(Const::Kind),
ExprKind::Const(Const::Kind) => Type::from_const(Const::Sort),
- ExprKind::Num(num) => Type::from_builtin(match num {
- NumKind::Bool(_) => Builtin::Bool,
- NumKind::Natural(_) => Builtin::Natural,
- NumKind::Integer(_) => Builtin::Integer,
- NumKind::Double(_) => Builtin::Double,
- }),
+ ExprKind::Num(num) => Type::from_builtin(
+ cx,
+ match num {
+ NumKind::Bool(_) => Builtin::Bool,
+ NumKind::Natural(_) => Builtin::Natural,
+ NumKind::Integer(_) => Builtin::Integer,
+ NumKind::Double(_) => Builtin::Double,
+ },
+ ),
ExprKind::Builtin(b) => {
let t_hir = type_of_builtin(b);
typecheck(env.cx(), &t_hir)?.eval_to_type(env)?
}
ExprKind::TextLit(interpolated) => {
- let text_type = Type::from_builtin(Builtin::Text);
+ let text_type = Type::from_builtin(cx, Builtin::Text);
for contents in interpolated.iter() {
use InterpolatedTextContents::Expr;
if let Expr(x) = contents {
@@ -79,7 +83,7 @@ fn type_one_layer(
}
let t = x.ty().to_nir();
- Nir::from_builtin(Builtin::Optional)
+ Nir::from_builtin(cx, Builtin::Optional)
.app(t)
.to_type(Const::Type)
}
@@ -104,7 +108,9 @@ fn type_one_layer(
}
let t = x.ty().to_nir();
- Nir::from_builtin(Builtin::List).app(t).to_type(Const::Type)
+ Nir::from_builtin(cx, Builtin::List)
+ .app(t)
+ .to_type(Const::Type)
}
ExprKind::RecordLit(kvs) => {
// An empty record type has type Type
@@ -171,11 +177,11 @@ fn type_one_layer(
/// to compare with.
// 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<'_>,
- hir: &'hir Hir,
- annot: Option<Type>,
-) -> Result<Tir<'hir>, TypeError> {
+pub fn type_with<'cx, 'hir>(
+ env: &TyEnv<'cx>,
+ hir: &'hir Hir<'cx>,
+ annot: Option<Type<'cx>>,
+) -> Result<Tir<'cx, 'hir>, TypeError> {
let tir = match hir.kind() {
HirKind::Var(var) => Tir::from_hir(hir, env.lookup(*var)),
HirKind::Import(_, ty) => Tir::from_hir(hir, ty.clone()),
@@ -268,19 +274,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>(
- cx: Ctxt<'_>,
- hir: &'hir Hir,
-) -> Result<Tir<'hir>, TypeError> {
+pub fn typecheck<'cx, 'hir>(
+ cx: Ctxt<'cx>,
+ hir: &'hir Hir<'cx>,
+) -> Result<Tir<'cx, '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> {
+pub fn typecheck_with<'cx, 'hir>(
+ cx: Ctxt<'cx>,
+ hir: &'hir Hir<'cx>,
+ ty: &Hir<'cx>,
+) -> Result<Tir<'cx, 'hir>, TypeError> {
let ty = typecheck(cx, ty)?.eval_to_type(&TyEnv::new(cx))?;
type_with(&TyEnv::new(cx), hir, Some(ty))
}
diff --git a/dhall/tests/spec.rs b/dhall/tests/spec.rs
index 646083a..ab1dc2f 100644
--- a/dhall/tests/spec.rs
+++ b/dhall/tests/spec.rs
@@ -15,7 +15,7 @@ use walkdir::WalkDir;
use dhall::error::Error as DhallError;
use dhall::error::ErrorKind;
use dhall::syntax::{binary, Expr};
-use dhall::{Normalized, Parsed, Resolved, Typed};
+use dhall::{Ctxt, Normalized, Parsed, Resolved, Typed};
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
enum FileType {
@@ -108,16 +108,16 @@ impl TestFile {
})
}
/// Parse and resolve the target file
- pub fn resolve(&self) -> Result<Resolved> {
- Ok(self.parse()?.resolve()?)
+ pub fn resolve<'cx>(&self, cx: Ctxt<'cx>) -> Result<Resolved<'cx>> {
+ Ok(self.parse()?.resolve(cx)?)
}
/// Parse, resolve and tck the target file
- pub fn typecheck(&self) -> Result<Typed> {
- Ok(self.resolve()?.typecheck()?)
+ pub fn typecheck<'cx>(&self, cx: Ctxt<'cx>) -> Result<Typed<'cx>> {
+ Ok(self.resolve(cx)?.typecheck(cx)?)
}
/// Parse, resolve, tck and normalize the target file
- pub fn normalize(&self) -> Result<Normalized> {
- Ok(self.typecheck()?.normalize())
+ pub fn normalize<'cx>(&self, cx: Ctxt<'cx>) -> Result<Normalized<'cx>> {
+ Ok(self.typecheck(cx)?.normalize(cx))
}
/// If UPDATE_TEST_FILES is `true`, we overwrite the output files with our own output.
@@ -586,79 +586,81 @@ fn run_test(test: &SpecTest) -> Result<()> {
output: expected,
..
} = test;
- match test.kind {
- ParserSuccess => {
- let expr = expr.parse()?;
- // This exercices both parsing and binary decoding
- expected.compare_debug(expr)?;
- }
- ParserFailure => {
- use std::io;
- let err = unwrap_err(expr.parse())?;
- match err.downcast_ref::<DhallError>() {
- Some(err) => match err.kind() {
- ErrorKind::Parse(_) => {}
- ErrorKind::IO(e)
- if e.kind() == io::ErrorKind::InvalidData => {}
- e => Err(TestError(format!(
- "Expected parse error, got: {:?}",
- e
- )))?,
- },
- None => {}
+ Ctxt::with_new(|cx| {
+ match test.kind {
+ ParserSuccess => {
+ let expr = expr.parse()?;
+ // This exercices both parsing and binary decoding
+ expected.compare_debug(expr)?;
+ }
+ ParserFailure => {
+ use std::io;
+ let err = unwrap_err(expr.parse())?;
+ match err.downcast_ref::<DhallError>() {
+ Some(err) => match err.kind() {
+ ErrorKind::Parse(_) => {}
+ ErrorKind::IO(e)
+ if e.kind() == io::ErrorKind::InvalidData => {}
+ e => Err(TestError(format!(
+ "Expected parse error, got: {:?}",
+ e
+ )))?,
+ },
+ None => {}
+ }
+ expected.compare_ui(err)?;
+ }
+ BinaryEncoding => {
+ let expr = expr.parse()?;
+ expected.compare_binary(expr)?;
+ }
+ BinaryDecodingSuccess => {
+ let expr = expr.parse()?;
+ expected.compare_debug(expr)?;
+ }
+ BinaryDecodingFailure => {
+ let err = unwrap_err(expr.parse())?;
+ expected.compare_ui(err)?;
+ }
+ Printer => {
+ let parsed = expr.parse()?;
+ // Round-trip pretty-printer
+ let reparsed = Parsed::parse_str(&parsed.to_string())?;
+ assert_eq!(reparsed, parsed);
+ expected.compare_ui(parsed)?;
+ }
+ ImportSuccess => {
+ let expr = expr.normalize(cx)?;
+ expected.compare(expr)?;
+ }
+ ImportFailure => {
+ let err = unwrap_err(expr.resolve(cx))?;
+ expected.compare_ui(err)?;
+ }
+ SemanticHash => {
+ let expr = expr.normalize(cx)?.to_expr_alpha();
+ let hash = hex::encode(expr.sha256_hash()?);
+ expected.compare_ui(format!("sha256:{}", hash))?;
+ }
+ TypeInferenceSuccess => {
+ let ty = expr.typecheck(cx)?.get_type()?;
+ expected.compare(ty)?;
+ }
+ TypeInferenceFailure => {
+ let err = unwrap_err(expr.typecheck(cx))?;
+ expected.compare_ui(err)?;
+ }
+ Normalization => {
+ let expr = expr.normalize(cx)?;
+ expected.compare(expr)?;
+ }
+ AlphaNormalization => {
+ let expr = expr.normalize(cx)?.to_expr_alpha();
+ expected.compare(expr)?;
}
- expected.compare_ui(err)?;
- }
- BinaryEncoding => {
- let expr = expr.parse()?;
- expected.compare_binary(expr)?;
- }
- BinaryDecodingSuccess => {
- let expr = expr.parse()?;
- expected.compare_debug(expr)?;
- }
- BinaryDecodingFailure => {
- let err = unwrap_err(expr.parse())?;
- expected.compare_ui(err)?;
- }
- Printer => {
- let parsed = expr.parse()?;
- // Round-trip pretty-printer
- let reparsed = Parsed::parse_str(&parsed.to_string())?;
- assert_eq!(reparsed, parsed);
- expected.compare_ui(parsed)?;
- }
- ImportSuccess => {
- let expr = expr.normalize()?;
- expected.compare(expr)?;
- }
- ImportFailure => {
- let err = unwrap_err(expr.resolve())?;
- expected.compare_ui(err)?;
- }
- SemanticHash => {
- let expr = expr.normalize()?.to_expr_alpha();
- let hash = hex::encode(expr.sha256_hash()?);
- expected.compare_ui(format!("sha256:{}", hash))?;
- }
- TypeInferenceSuccess => {
- let ty = expr.typecheck()?.get_type()?;
- expected.compare(ty)?;
- }
- TypeInferenceFailure => {
- let err = unwrap_err(expr.typecheck())?;
- expected.compare_ui(err)?;
- }
- Normalization => {
- let expr = expr.normalize()?;
- expected.compare(expr)?;
- }
- AlphaNormalization => {
- let expr = expr.normalize()?.to_expr_alpha();
- expected.compare(expr)?;
}
- }
- Ok(())
+ Ok(())
+ })
}
fn main() {
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 17:57:18 +0000