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 ++++----- dhall/src/ctxt.rs | 12 +- dhall/src/lib.rs | 76 ++++++------- dhall/src/operations/normalization.rs | 6 +- dhall/src/operations/typecheck.rs | 72 ++++++------ dhall/src/semantics/nze/env.rs | 42 ++++--- dhall/src/semantics/nze/nir.rs | 197 +++++++++++++++++---------------- dhall/src/semantics/nze/normalize.rs | 39 +++---- dhall/src/semantics/resolve/cache.rs | 24 +++- dhall/src/semantics/resolve/env.rs | 13 ++- dhall/src/semantics/resolve/hir.rs | 42 +++---- dhall/src/semantics/resolve/resolve.rs | 32 ++++-- dhall/src/semantics/tck/env.rs | 16 +-- dhall/src/semantics/tck/tir.rs | 60 +++++----- dhall/src/semantics/tck/typecheck.rs | 60 +++++----- dhall/tests/spec.rs | 158 +++++++++++++------------- 16 files changed, 475 insertions(+), 425 deletions(-) (limited to 'dhall') 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, + args: Vec>, } -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, - env: NzEnv, -) -> NirKind { + args: Vec>, + 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>>, - import_results: FrozenVec>, + import_results: FrozenVec>>, } /// 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 for CtxtS<'cx> { } } impl<'cx> std::ops::Index 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 { - // TODO: thread cx - Ctxt::with_new(|cx| resolve::resolve(cx, self)) + pub fn resolve<'cx>(self, cx: Ctxt<'cx>) -> Result, Error> { + resolve::resolve(cx, self) } - pub fn skip_resolve(self) -> Result { + pub fn skip_resolve<'cx>(self) -> Result, Error> { resolve::skip_resolve(self) } @@ -90,16 +90,16 @@ impl Parsed { } } -impl Resolved { - pub fn typecheck(&self) -> Result { - // 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, TypeError> { + Ok(Typed::from_tir(typecheck(cx, &self.0)?)) } - pub fn typecheck_with(self, ty: &Hir) -> Result { - // 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, 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 { + pub fn get_type(&self) -> Result, 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 for Expr { other.to_expr() } } -impl From for Expr { - fn from(other: Normalized) -> Self { +impl<'cx> From> 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) -> Ret { +pub fn normalize_operation<'cx>(opkind: OpKind>) -> 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 { + l: Tir<'cx, '_>, + r: Tir<'cx, '_>, +) -> Result, 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 { + record: &Tir<'cx, '_>, + scrut: &Tir<'cx, '_>, + type_annot: Option<&Tir<'cx, '_>>, +) -> Result, 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>, -) -> Result { + opkind: OpKind>, +) -> Result, 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 { +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 { - items: Vec>, +pub struct ValEnv<'cx, T> { + cx: Ctxt<'cx>, + items: Vec>, } -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 ValEnv { - 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 ValEnv { 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 ValEnv { } } -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 to share computation. @@ -20,31 +20,31 @@ use crate::ToExprOptions; /// normalize as needed. /// Stands for "Normalized Intermediate Representation" #[derive(Clone)] -pub struct Nir(Rc>); +pub struct Nir<'cx>(Rc, 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 }, + PartialExpr { expr: ExprKind> }, } /// 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>); +pub struct TextLit<'cx>(Vec>>); /// 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>); /// 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), - ListType(Nir), - RecordLit(HashMap), - RecordType(HashMap), - UnionConstructor(Label, HashMap>), - UnionLit(Label, Nir, HashMap>), - UnionType(HashMap>), - Equivalence(Nir, Nir), - Assert(Nir), + EmptyListLit(Nir<'cx>), + NEListLit(Vec>), + ListType(Nir<'cx>), + RecordLit(HashMap>), + RecordType(HashMap>), + UnionConstructor(Label, HashMap>>), + UnionLit(Label, Nir<'cx>, HashMap>>), + UnionType(HashMap>>), + 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), + Op(OpKind>), } -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 { - // 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 { + 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) -> Type { + pub fn to_type(&self, u: impl Into) -> 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>| { - 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>>| -> ExprKind> { + 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) -> Self { - Thunk::PartialExpr { env, expr } + fn from_partial_expr(expr: ExprKind>) -> 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 { + pub fn remove_binder(&self) -> Result, ()> { 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>, + elts: impl Iterator>>, ) -> 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> { + pub fn iter( + &self, + ) -> impl Iterator>> { self.0.iter() } } -impl lazy::Eval for Thunk { - fn eval(self) -> NirKind { +impl<'cx> lazy::Eval> 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>, -) -> Vec> { +pub fn squash_textlit<'cx>( + elts: impl Iterator>>, +) -> Vec>> { use std::mem::replace; use InterpolatedTextContents::{Expr, Text}; - fn inner( - elts: impl Iterator>, + fn inner<'cx>( + elts: impl Iterator>>, crnt_str: &mut String, - ret: &mut Vec>, + ret: &mut Vec>>, ) { 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) -> Ret { +pub fn ret_op<'cx>(x: OpKind>) -> Ret<'cx> { NirKind::Op(x) } -pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { +pub fn normalize_one_layer<'cx>(expr: ExprKind>) -> NirKind<'cx> { use NirKind::{ Assert, Const, NEListLit, NEOptionalLit, Num, RecordLit, RecordType, UnionType, @@ -106,15 +106,13 @@ pub fn normalize_one_layer(expr: ExprKind, 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, 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 { + pub fn get<'cx>( + &self, + cx: Ctxt<'cx>, + hash: &Hash, + ) -> Result, 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 { +fn read_cache_file<'cx>( + cx: Ctxt<'cx>, + path: &Path, + hash: &Hash, +) -> Result, Error> { let data = crate::utils::read_binary_file(path)?; match hash { @@ -81,7 +93,7 @@ fn read_cache_file(path: &Path, hash: &Hash) -> Result { } } - 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) -> Option { + pub fn get_from_disk_cache( + &self, + hash: &Option, + ) -> Option> { 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, expr: &Typed) { + pub fn write_to_disk_cache(&self, hash: &Option, 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, - ) -> Result { + do_resolve: impl FnOnce(&mut Self) -> Result, Error>, + ) -> Result, 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), + Expr(ExprKind>), } // An expression with resolved variables and imports. #[derive(Debug, Clone)] -pub struct Hir { - kind: Box, +pub struct Hir<'cx> { + kind: Box>, 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, TypeError> { + env: &TyEnv<'cx>, + ) -> Result, TypeError> { type_with(env, self, None) } pub fn typecheck_noenv<'hir>( &'hir self, - cx: Ctxt<'_>, - ) -> Result, TypeError> { + cx: Ctxt<'cx>, + ) -> Result, 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) -> Nir { + pub fn eval(&self, env: impl Into>) -> 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 { + ) -> Result, 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, -) -> Result { + f: &mut impl FnMut(Import, Span) -> Result, Error>, +) -> Result, 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 { +) -> Result, 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 { +pub fn resolve<'cx>( + cx: Ctxt<'cx>, + parsed: Parsed, +) -> Result, Error> { resolve_with_env(&mut ImportEnv::new(cx), parsed) } -pub fn skip_resolve_expr(expr: &Expr) -> Result { +pub fn skip_resolve_expr<'cx>(expr: &Expr) -> Result, Error> { traverse_resolve_expr(&mut NameEnv::new(), expr, &mut |import, _span| { Err(ImportError::UnexpectedImport(import).into()) }) } -pub fn skip_resolve(parsed: Parsed) -> Result { +pub fn skip_resolve<'cx>(parsed: Parsed) -> Result, 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, + 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 { 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 { 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) -> Nir { + pub fn eval(&self, env: impl Into>) -> 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 { + pub fn eval_to_type( + &self, + env: &TyEnv<'cx>, + ) -> Result, 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(span: Span, msg: S) -> Result { /// When all sub-expressions have been typed, check the remaining toplevel /// layer. -fn type_one_layer( - env: &TyEnv<'_>, - ekind: ExprKind>, +fn type_one_layer<'cx>( + env: &TyEnv<'cx>, + ekind: ExprKind>, span: Span, -) -> Result { +) -> Result, 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, -) -> Result, TypeError> { +pub fn type_with<'cx, 'hir>( + env: &TyEnv<'cx>, + hir: &'hir Hir<'cx>, + annot: Option>, +) -> Result, 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, TypeError> { +pub fn typecheck<'cx, 'hir>( + cx: Ctxt<'cx>, + hir: &'hir Hir<'cx>, +) -> Result, 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, TypeError> { +pub fn typecheck_with<'cx, 'hir>( + cx: Ctxt<'cx>, + hir: &'hir Hir<'cx>, + ty: &Hir<'cx>, +) -> Result, 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 { - Ok(self.parse()?.resolve()?) + pub fn resolve<'cx>(&self, cx: Ctxt<'cx>) -> Result> { + Ok(self.parse()?.resolve(cx)?) } /// Parse, resolve and tck the target file - pub fn typecheck(&self) -> Result { - Ok(self.resolve()?.typecheck()?) + pub fn typecheck<'cx>(&self, cx: Ctxt<'cx>) -> Result> { + Ok(self.resolve(cx)?.typecheck(cx)?) } /// Parse, resolve, tck and normalize the target file - pub fn normalize(&self) -> Result { - Ok(self.typecheck()?.normalize()) + pub fn normalize<'cx>(&self, cx: Ctxt<'cx>) -> Result> { + 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::() { - 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::() { + 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() { -- cgit v1.2.3