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/semantics/nze/env.rs | 42 +++++--- dhall/src/semantics/nze/nir.rs | 197 ++++++++++++++++++----------------- dhall/src/semantics/nze/normalize.rs | 39 +++---- 3 files changed, 145 insertions(+), 133 deletions(-) (limited to 'dhall/src/semantics/nze') 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) } } } -- cgit v1.3.1 From 8c5b3ff15f2125e9d731fc199e194e1993c36b37 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 7 Dec 2020 14:15:43 +0000 Subject: Thread cx everywhere else imports are read --- dhall/src/ctxt.rs | 6 +++++ dhall/src/lib.rs | 42 ++++++++-------------------------- dhall/src/semantics/nze/nir.rs | 4 ++-- dhall/src/semantics/resolve/cache.rs | 11 ++++++--- dhall/src/semantics/resolve/env.rs | 18 +++++++++++---- dhall/src/semantics/resolve/hir.rs | 20 ++++++++-------- dhall/src/semantics/resolve/resolve.rs | 36 +++++++++++++++-------------- dhall/tests/spec.rs | 27 ++++++++++------------ serde_dhall/src/options/de.rs | 1 + serde_dhall/src/value.rs | 17 ++++++++++---- 10 files changed, 93 insertions(+), 89 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/ctxt.rs b/dhall/src/ctxt.rs index 8bdf99d..3809bc9 100644 --- a/dhall/src/ctxt.rs +++ b/dhall/src/ctxt.rs @@ -83,6 +83,12 @@ impl<'cx> StoredImport<'cx> { let res = self.get_resultid()?; Some(&self.cx[res]) } + /// Get the result of fetching this import. Panicx if the result has not yet been + /// fetched. + pub fn unwrap_result(&self) -> &'cx Typed<'cx> { + self.get_result() + .expect("imports should all have been resolved at this stage") + } /// Store the result of fetching this import. pub fn set_result(&self, res: Typed<'cx>) -> ImportResultId<'cx> { let res = self.cx.push_import_result(res); diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index ec2b813..7f77334 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -5,8 +5,7 @@ clippy::needless_lifetimes, clippy::new_ret_no_self, clippy::new_without_default, - clippy::useless_format, - unreachable_code + clippy::useless_format )] pub mod builtins; @@ -17,7 +16,6 @@ pub mod semantics; pub mod syntax; pub mod utils; -use std::fmt::Display; use std::path::Path; use url::Url; @@ -102,8 +100,8 @@ impl<'cx> Resolved<'cx> { Ok(Typed::from_tir(typecheck_with(cx, &self.0, ty)?)) } /// Converts a value back to the corresponding AST expression. - pub fn to_expr(&self) -> Expr { - self.0.to_expr_noopts() + pub fn to_expr(&self, cx: Ctxt<'cx>) -> Expr { + self.0.to_expr_noopts(cx) } } @@ -120,8 +118,8 @@ impl<'cx> Typed<'cx> { } /// Converts a value back to the corresponding AST expression. - fn to_expr(&self) -> Expr { - self.hir.to_expr(ToExprOptions { alpha: false }) + fn to_expr(&self, cx: Ctxt<'cx>) -> Expr { + self.hir.to_expr(cx, ToExprOptions { alpha: false }) } pub fn ty(&self) -> &Type<'cx> { @@ -134,8 +132,8 @@ impl<'cx> Typed<'cx> { 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()) + pub fn to_expr(&self, cx: Ctxt<'cx>) -> Expr { + self.0.to_expr(cx, ToExprOptions::default()) } /// Converts a value back to the corresponding Hir expression. pub fn to_hir(&self) -> Hir<'cx> { @@ -145,8 +143,8 @@ impl<'cx> Normalized<'cx> { &self.0 } /// Converts a value back to the corresponding AST expression, alpha-normalizing in the process. - pub fn to_expr_alpha(&self) -> Expr { - self.0.to_expr(ToExprOptions { alpha: true }) + pub fn to_expr_alpha(&self, cx: Ctxt<'cx>) -> Expr { + self.0.to_expr(cx, ToExprOptions { alpha: true }) } } @@ -178,23 +176,6 @@ impl From for Expr { other.to_expr() } } -impl<'cx> From> for Expr { - fn from(other: Normalized<'cx>) -> Self { - other.to_expr() - } -} - -impl<'cx> Display for Resolved<'cx> { - fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> { - self.to_expr().fmt(f) - } -} - -impl<'cx> Display for Typed<'cx> { - fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> { - self.to_expr().fmt(f) - } -} impl<'cx> Eq for Normalized<'cx> {} impl<'cx> PartialEq for Normalized<'cx> { @@ -202,8 +183,3 @@ impl<'cx> PartialEq for Normalized<'cx> { self.0 == other.0 } } -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/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs index 538b8ea..8cf06c5 100644 --- a/dhall/src/semantics/nze/nir.rs +++ b/dhall/src/semantics/nze/nir.rs @@ -148,8 +148,8 @@ impl<'cx> Nir<'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(&self, cx: Ctxt<'cx>, opts: ToExprOptions) -> Expr { + self.to_hir_noenv().to_expr(cx, opts) } pub fn to_expr_tyenv(&self, tyenv: &TyEnv<'cx>) -> Expr { self.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv) diff --git a/dhall/src/semantics/resolve/cache.rs b/dhall/src/semantics/resolve/cache.rs index 59463dd..9a5e835 100644 --- a/dhall/src/semantics/resolve/cache.rs +++ b/dhall/src/semantics/resolve/cache.rs @@ -68,11 +68,12 @@ impl Cache { pub fn insert<'cx>( &self, + cx: Ctxt<'cx>, hash: &Hash, expr: &Typed<'cx>, ) -> Result<(), Error> { let path = self.entry_path(hash); - write_cache_file(&path, expr) + write_cache_file(cx, &path, expr) } } @@ -97,8 +98,12 @@ fn read_cache_file<'cx>( } /// Write a file to the cache. -fn write_cache_file(path: &Path, expr: &Typed) -> Result<(), Error> { - let data = binary::encode(&expr.to_expr())?; +fn write_cache_file<'cx>( + cx: Ctxt<'cx>, + path: &Path, + expr: &Typed<'cx>, +) -> Result<(), Error> { + let data = binary::encode(&expr.to_expr(cx))?; File::create(path)?.write_all(data.as_slice())?; Ok(()) } diff --git a/dhall/src/semantics/resolve/env.rs b/dhall/src/semantics/resolve/env.rs index ba6205f..0d1952b 100644 --- a/dhall/src/semantics/resolve/env.rs +++ b/dhall/src/semantics/resolve/env.rs @@ -1,9 +1,9 @@ use std::collections::HashMap; use crate::error::{Error, ImportError}; -use crate::semantics::{AlphaVar, Cache, ImportLocation, VarEnv}; +use crate::semantics::{check_hash, AlphaVar, Cache, ImportLocation, VarEnv}; use crate::syntax::{Hash, Label, V}; -use crate::{Ctxt, ImportResultId, Typed}; +use crate::{Ctxt, ImportId, ImportResultId, Typed}; /// Environment for resolving names. #[derive(Debug, Clone, Default)] @@ -95,6 +95,11 @@ impl<'cx> ImportEnv<'cx> { Some(expr) } + /// Invariant: the import must have been fetched. + pub fn check_hash(&self, import: ImportId<'cx>) -> Result<(), Error> { + check_hash(self.cx(), import) + } + pub fn write_to_mem_cache( &mut self, location: ImportLocation, @@ -103,10 +108,13 @@ impl<'cx> ImportEnv<'cx> { self.mem_cache.insert(location, result); } - pub fn write_to_disk_cache(&self, hash: &Option, expr: &Typed<'cx>) { + /// Invariant: the import must have been fetched. + pub fn write_to_disk_cache(&self, import: ImportId<'cx>) { + let import = &self.cx()[import]; if let Some(disk_cache) = self.disk_cache.as_ref() { - if let Some(hash) = hash { - let _ = disk_cache.insert(hash, &expr); + if let Some(hash) = &import.import.hash { + let expr = import.unwrap_result(); + let _ = disk_cache.insert(self.cx(), hash, expr); } } } diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs index c67ab75..5575888 100644 --- a/dhall/src/semantics/resolve/hir.rs +++ b/dhall/src/semantics/resolve/hir.rs @@ -51,22 +51,23 @@ impl<'cx> Hir<'cx> { } /// Converts a closed Hir expr back to the corresponding AST expression. - pub fn to_expr(&self, opts: ToExprOptions) -> Expr { - hir_to_expr(self, opts, &mut NameEnv::new()) + pub fn to_expr(&self, cx: Ctxt<'cx>, opts: ToExprOptions) -> Expr { + hir_to_expr(cx, self, opts, &mut NameEnv::new()) } /// Converts a closed Hir expr back to the corresponding AST expression. - pub fn to_expr_noopts(&self) -> Expr { + pub fn to_expr_noopts(&self, cx: Ctxt<'cx>) -> Expr { let opts = ToExprOptions { alpha: false }; - self.to_expr(opts) + self.to_expr(cx, opts) } - pub fn to_expr_alpha(&self) -> Expr { + pub fn to_expr_alpha(&self, cx: Ctxt<'cx>) -> Expr { let opts = ToExprOptions { alpha: true }; - self.to_expr(opts) + self.to_expr(cx, opts) } pub fn to_expr_tyenv(&self, env: &TyEnv<'cx>) -> Expr { let opts = ToExprOptions { alpha: false }; + let cx = env.cx(); let mut env = env.as_nameenv().clone(); - hir_to_expr(self, opts, &mut env) + hir_to_expr(cx, self, opts, &mut env) } /// Typecheck the Hir. @@ -95,6 +96,7 @@ impl<'cx> Hir<'cx> { } fn hir_to_expr<'cx>( + cx: Ctxt<'cx>, hir: &Hir<'cx>, opts: ToExprOptions, env: &mut NameEnv, @@ -103,14 +105,14 @@ fn hir_to_expr<'cx>( HirKind::Var(v) if opts.alpha => ExprKind::Var(V("_".into(), v.idx())), HirKind::Var(v) => ExprKind::Var(env.label_var(*v)), HirKind::Import(hir, _) => { - return hir_to_expr(hir, opts, &mut NameEnv::new()) + return hir_to_expr(cx, hir, opts, &mut NameEnv::new()); } HirKind::Expr(e) => { let e = e.map_ref_maybe_binder(|l, hir| { if let Some(l) = l { env.insert_mut(l); } - let e = hir_to_expr(hir, opts, env); + let e = hir_to_expr(cx, hir, opts, env); if l.is_some() { env.remove_mut(); } diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs index 9021155..db162ef 100644 --- a/dhall/src/semantics/resolve/resolve.rs +++ b/dhall/src/semantics/resolve/resolve.rs @@ -287,19 +287,21 @@ fn make_aslocation_uniontype() -> Expr { mkexpr(ExprKind::UnionType(union)) } -fn check_hash<'cx>( - import: &Import, - typed: &Typed<'cx>, - span: Span, +/// Invariant: the import must have been fetched. +pub fn check_hash<'cx>( + cx: Ctxt<'cx>, + import: ImportId<'cx>, ) -> Result<(), Error> { + let import = &cx[import]; if let (ImportMode::Code, Some(Hash::SHA256(hash))) = - (import.mode, &import.hash) + (import.import.mode, &import.import.hash) { - let actual_hash = typed.hir.to_expr_alpha().sha256_hash()?; + let expr = import.unwrap_result().hir.to_expr_alpha(cx); + let actual_hash = expr.sha256_hash()?; if hash[..] != actual_hash[..] { mkerr( ErrorBuilder::new("hash mismatch") - .span_err(span, "hash mismatch") + .span_err(import.span.clone(), "hash mismatch") .note(format!("Expected sha256:{}", hex::encode(hash))) .note(format!( "Found sha256:{}", @@ -411,15 +413,14 @@ fn fetch_import<'cx>( cx[import_id].set_resultid(res_id); // The same location may be used with different or no hashes. Thus we need to check // the hashes every time. - let typed = &cx[res_id]; - check_hash(import, typed, span)?; - env.write_to_disk_cache(&import.hash, typed); + env.check_hash(import_id)?; + env.write_to_disk_cache(import_id); return Ok(()); } if let Some(typed) = env.get_from_disk_cache(&import.hash) { - // No need to check the hash, it was checked before reading the file. We also don't - // write to the in-memory cache, because the location might be completely unrelated - // to the cached file (e.g. `missing sha256:...` is valid). + // No need to check the hash, it was checked before reading the file. + // We also don't write to the in-memory cache, because the location might be completely + // unrelated to the cached file (e.g. `missing sha256:...` is valid). // This actually means that importing many times a same hashed import will take // longer than importing many times a same non-hashed import. cx[import_id].set_result(typed); @@ -441,9 +442,10 @@ fn fetch_import<'cx>( }; // Add the resolved import to the caches - check_hash(import, &typed, span)?; - env.write_to_disk_cache(&import.hash, &typed); - let res_id = cx[import_id].set_result(typed); + let res_id = cx[import_id].set_result(typed.clone()); + env.check_hash(import_id)?; + env.write_to_disk_cache(import_id); + // Cache the mapping from this location to the result. env.write_to_mem_cache(location, res_id); Ok(()) @@ -462,7 +464,7 @@ fn resolve_with_env<'cx>( env.cx().push_import(base_location.clone(), import, span); fetch_import(env, import_id)?; // TODO: store import id in Hir - Ok(env.cx()[import_id].get_result().unwrap().clone()) + Ok(env.cx()[import_id].unwrap_result().clone()) }, )?; Ok(Resolved(resolved)) diff --git a/dhall/tests/spec.rs b/dhall/tests/spec.rs index ab1dc2f..a0fe583 100644 --- a/dhall/tests/spec.rs +++ b/dhall/tests/spec.rs @@ -160,8 +160,7 @@ impl TestFile { } /// Check that the provided expression matches the file contents. - pub fn compare(&self, expr: impl Into) -> Result<()> { - let expr = expr.into(); + pub fn compare(&self, expr: Expr) -> Result<()> { if !self.path().is_file() { return self.write_expr(expr); } @@ -177,8 +176,7 @@ impl TestFile { Ok(()) } /// Check that the provided expression matches the file contents. - pub fn compare_debug(&self, expr: impl Into) -> Result<()> { - let expr = expr.into(); + pub fn compare_debug(&self, expr: Expr) -> Result<()> { if !self.path().is_file() { return self.write_expr(expr); } @@ -194,8 +192,7 @@ impl TestFile { Ok(()) } /// Check that the provided expression matches the file contents. - pub fn compare_binary(&self, expr: impl Into) -> Result<()> { - let expr = expr.into(); + pub fn compare_binary(&self, expr: Expr) -> Result<()> { match self { TestFile::Binary(_) => {} _ => Err(TestError(format!("This is not a binary file")))?, @@ -591,7 +588,7 @@ fn run_test(test: &SpecTest) -> Result<()> { ParserSuccess => { let expr = expr.parse()?; // This exercices both parsing and binary decoding - expected.compare_debug(expr)?; + expected.compare_debug(expr.to_expr())?; } ParserFailure => { use std::io; @@ -612,11 +609,11 @@ fn run_test(test: &SpecTest) -> Result<()> { } BinaryEncoding => { let expr = expr.parse()?; - expected.compare_binary(expr)?; + expected.compare_binary(expr.to_expr())?; } BinaryDecodingSuccess => { let expr = expr.parse()?; - expected.compare_debug(expr)?; + expected.compare_debug(expr.to_expr())?; } BinaryDecodingFailure => { let err = unwrap_err(expr.parse())?; @@ -627,24 +624,24 @@ fn run_test(test: &SpecTest) -> Result<()> { // Round-trip pretty-printer let reparsed = Parsed::parse_str(&parsed.to_string())?; assert_eq!(reparsed, parsed); - expected.compare_ui(parsed)?; + expected.compare_ui(parsed.to_expr())?; } ImportSuccess => { let expr = expr.normalize(cx)?; - expected.compare(expr)?; + expected.compare(expr.to_expr(cx))?; } ImportFailure => { let err = unwrap_err(expr.resolve(cx))?; expected.compare_ui(err)?; } SemanticHash => { - let expr = expr.normalize(cx)?.to_expr_alpha(); + let expr = expr.normalize(cx)?.to_expr_alpha(cx); let hash = hex::encode(expr.sha256_hash()?); expected.compare_ui(format!("sha256:{}", hash))?; } TypeInferenceSuccess => { let ty = expr.typecheck(cx)?.get_type()?; - expected.compare(ty)?; + expected.compare(ty.to_expr(cx))?; } TypeInferenceFailure => { let err = unwrap_err(expr.typecheck(cx))?; @@ -652,10 +649,10 @@ fn run_test(test: &SpecTest) -> Result<()> { } Normalization => { let expr = expr.normalize(cx)?; - expected.compare(expr)?; + expected.compare(expr.to_expr(cx))?; } AlphaNormalization => { - let expr = expr.normalize(cx)?.to_expr_alpha(); + let expr = expr.normalize(cx)?.to_expr_alpha(cx); expected.compare(expr)?; } } diff --git a/serde_dhall/src/options/de.rs b/serde_dhall/src/options/de.rs index d57759a..fc8c6dc 100644 --- a/serde_dhall/src/options/de.rs +++ b/serde_dhall/src/options/de.rs @@ -250,6 +250,7 @@ impl<'a, A> Deserializer<'a, A> { Some(ty) => resolved.typecheck_with(cx, &ty.to_hir())?, }; Ok(Value::from_nir_and_ty( + cx, typed.normalize(cx).as_nir(), typed.ty().as_nir(), )) diff --git a/serde_dhall/src/value.rs b/serde_dhall/src/value.rs index e5f5acd..b259c4b 100644 --- a/serde_dhall/src/value.rs +++ b/serde_dhall/src/value.rs @@ -5,6 +5,7 @@ use dhall::operations::OpKind; use dhall::semantics::{Hir, HirKind, Nir, NirKind}; pub use dhall::syntax::NumKind; use dhall::syntax::{Expr, ExprKind, Span}; +use dhall::Ctxt; use crate::{Error, ErrorKind, FromDhall, Result, ToDhall}; @@ -206,7 +207,11 @@ pub enum SimpleType { } impl Value { - pub(crate) fn from_nir_and_ty(x: &Nir, ty: &Nir) -> Result { + pub(crate) fn from_nir_and_ty<'cx>( + cx: Ctxt<'cx>, + x: &Nir<'cx>, + ty: &Nir<'cx>, + ) -> Result { Ok(if let Some(val) = SimpleValue::from_nir(x) { // The type must be simple if the value is simple. let ty = SimpleType::from_nir(ty).unwrap(); @@ -218,7 +223,7 @@ impl Value { kind: ValueKind::Ty(ty), } } else { - let expr = x.to_hir_noenv().to_expr(Default::default()); + let expr = x.to_hir_noenv().to_expr(cx, Default::default()); return Err(Error(ErrorKind::Deserialize(format!( "this is neither a simple type nor a simple value: {}", expr @@ -342,7 +347,7 @@ impl SimpleValue { let type_error = || { Error(ErrorKind::Serialize(format!( "expected a value of type {}, found {:?}", - ty.unwrap().to_hir().to_expr(Default::default()), + ty.unwrap().to_expr(), self ))) }; @@ -439,7 +444,9 @@ impl SimpleValue { /// Converts back to the corresponding AST expression. pub(crate) fn to_expr(&self, ty: Option<&SimpleType>) -> Result { - Ok(self.to_hir(ty)?.to_expr(Default::default())) + Ctxt::with_new(|cx| { + Ok(self.to_hir(ty)?.to_expr(cx, Default::default())) + }) } } @@ -514,7 +521,7 @@ impl SimpleType { /// Converts back to the corresponding AST expression. pub(crate) fn to_expr(&self) -> Expr { - self.to_hir().to_expr(Default::default()) + Ctxt::with_new(|cx| self.to_hir().to_expr(cx, Default::default())) } } -- cgit v1.3.1 From c1fe26d45c831eec015ad5c015236fce1928613a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 7 Dec 2020 14:32:06 +0000 Subject: Pass import results via the global context --- dhall/src/semantics/nze/normalize.rs | 5 ++++- dhall/src/semantics/resolve/hir.rs | 13 +++++++------ dhall/src/semantics/resolve/resolve.rs | 9 ++++----- dhall/src/semantics/tck/typecheck.rs | 5 ++++- 4 files changed, 19 insertions(+), 13 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index cce421d..d545750 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -155,7 +155,10 @@ pub fn normalize_one_layer<'cx>(expr: ExprKind>) -> NirKind<'cx> { 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), + HirKind::Import(import) => { + let typed = env.cx()[import].unwrap_result(); + normalize_hir(env, &typed.hir) + } HirKind::Expr(ExprKind::Lam(binder, annot, body)) => { let annot = annot.eval(env); NirKind::LamClosure { diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs index 5575888..cfde47e 100644 --- a/dhall/src/semantics/resolve/hir.rs +++ b/dhall/src/semantics/resolve/hir.rs @@ -1,7 +1,7 @@ use crate::error::TypeError; -use crate::semantics::{type_with, NameEnv, Nir, NzEnv, Tir, TyEnv, Type}; +use crate::semantics::{type_with, NameEnv, Nir, NzEnv, Tir, TyEnv}; use crate::syntax::{Expr, ExprKind, Span, V}; -use crate::{Ctxt, ToExprOptions}; +use crate::{Ctxt, ImportId, ToExprOptions}; /// Stores an alpha-normalized variable. #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] @@ -13,8 +13,8 @@ pub struct AlphaVar { pub enum HirKind<'cx> { /// A resolved variable (i.e. a DeBruijn index) Var(AlphaVar), - /// Result of resolving an import. - Import(Hir<'cx>, Type<'cx>), + /// An import. It must have been resolved by the time we get to typechecking/normalization. + Import(ImportId<'cx>), // Forbidden ExprKind variants: Var, Import, Completion Expr(ExprKind>), } @@ -104,8 +104,9 @@ fn hir_to_expr<'cx>( 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)), - HirKind::Import(hir, _) => { - return hir_to_expr(cx, hir, opts, &mut NameEnv::new()); + HirKind::Import(import) => { + let typed = cx[import].unwrap_result(); + return hir_to_expr(cx, &typed.hir, opts, &mut NameEnv::new()); } HirKind::Expr(e) => { let e = e.map_ref_maybe_binder(|l, hir| { diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs index db162ef..011ed45 100644 --- a/dhall/src/semantics/resolve/resolve.rs +++ b/dhall/src/semantics/resolve/resolve.rs @@ -348,7 +348,7 @@ fn desugar(expr: &Expr) -> Cow<'_, Expr> { fn traverse_resolve_expr<'cx>( name_env: &mut NameEnv, expr: &Expr, - f: &mut impl FnMut(Import, Span) -> Result, Error>, + f: &mut impl FnMut(Import, Span) -> Result, Error>, ) -> Result, Error> { let expr = desugar(expr); Ok(match expr.kind() { @@ -387,8 +387,8 @@ fn traverse_resolve_expr<'cx>( ExprKind::Import(import) => { // TODO: evaluate import headers let import = import.traverse_ref(|_| Ok::<_, Error>(()))?; - let imported = f(import, expr.span())?; - HirKind::Import(imported.hir, imported.ty) + let import_id = f(import, expr.span())?; + HirKind::Import(import_id) } kind => HirKind::Expr(kind), }; @@ -463,8 +463,7 @@ fn resolve_with_env<'cx>( let import_id = env.cx().push_import(base_location.clone(), import, span); fetch_import(env, import_id)?; - // TODO: store import id in Hir - Ok(env.cx()[import_id].unwrap_result().clone()) + Ok(import_id) }, )?; Ok(Resolved(resolved)) diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 8218368..f47563e 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -184,7 +184,10 @@ pub fn type_with<'cx, 'hir>( ) -> 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()), + HirKind::Import(import) => { + let typed = env.cx()[import].unwrap_result(); + Tir::from_hir(hir, typed.ty.clone()) + } HirKind::Expr(ExprKind::Var(_)) => { unreachable!("Hir should contain no unresolved variables") } -- cgit v1.3.1 From 7a392b07166c089979e69d4c8a68da3298964c28 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 7 Dec 2020 17:48:20 +0000 Subject: Defer name errors to typechecking We aren't supposed to inspect anything before alternatives are chosen --- dhall/src/semantics/nze/normalize.rs | 1 + dhall/src/semantics/resolve/hir.rs | 3 +++ dhall/src/semantics/resolve/resolve.rs | 9 ++++----- dhall/src/semantics/tck/typecheck.rs | 5 +++++ 4 files changed, 13 insertions(+), 5 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index d545750..0a09a80 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -154,6 +154,7 @@ pub fn normalize_one_layer<'cx>(expr: ExprKind>) -> NirKind<'cx> { /// Normalize Hir into WHNF pub fn normalize_hir<'cx>(env: &NzEnv<'cx>, hir: &Hir<'cx>) -> NirKind<'cx> { match hir.kind() { + HirKind::MissingVar(..) => unreachable!("ruled out by typechecking"), HirKind::Var(var) => env.lookup_val(*var), HirKind::Import(import) => { let typed = env.cx()[import].unwrap_result(); diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs index 3e282b4..05a8550 100644 --- a/dhall/src/semantics/resolve/hir.rs +++ b/dhall/src/semantics/resolve/hir.rs @@ -13,6 +13,8 @@ pub struct AlphaVar { pub enum HirKind<'cx> { /// A resolved variable (i.e. a DeBruijn index) Var(AlphaVar), + /// A variable that couldn't be resolved. Detected during resolution, but causes an error during typeck. + MissingVar(V), /// An import. It must have been resolved by the time we get to typechecking/normalization. Import(ImportId<'cx>), // Forbidden ExprKind variants: Var, Import, Completion @@ -104,6 +106,7 @@ fn hir_to_expr<'cx>( 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)), + HirKind::MissingVar(v) => ExprKind::Var(v.clone()), HirKind::Import(import) => { let typed = cx[import].unwrap_result(); return hir_to_expr(cx, &typed.hir, opts, &mut NameEnv::new()); diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs index 7450825..c4cd518 100644 --- a/dhall/src/semantics/resolve/resolve.rs +++ b/dhall/src/semantics/resolve/resolve.rs @@ -377,11 +377,7 @@ fn traverse_resolve_expr<'cx>( Ok(match expr.kind() { ExprKind::Var(var) => match name_env.unlabel_var(&var) { Some(v) => Hir::new(HirKind::Var(v), expr.span()), - None => mkerr( - ErrorBuilder::new(format!("unbound variable `{}`", var)) - .span_err(expr.span(), "not found in this scope") - .format(), - )?, + None => Hir::new(HirKind::MissingVar(var.clone()), expr.span()), }, ExprKind::Op(OpKind::BinOp(BinOp::ImportAlt, l, r)) => { match traverse_resolve_expr(name_env, l, f) { @@ -492,6 +488,8 @@ fn resolve_with_env<'cx>( Ok(Resolved(resolved)) } +/// Resolves all imports and names. Returns errors if importing failed. Name errors are deferred to +/// typechecking. pub fn resolve<'cx>( cx: Ctxt<'cx>, parsed: Parsed, @@ -499,6 +497,7 @@ pub fn resolve<'cx>( resolve_with_env(&mut ImportEnv::new(cx), parsed) } +/// Resolves names and errors if we find any imports. pub fn skip_resolve<'cx>( cx: Ctxt<'cx>, parsed: Parsed, diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 5a44c9c..e14bcc6 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -184,6 +184,11 @@ pub fn type_with<'cx, 'hir>( ) -> Result, TypeError> { let tir = match hir.kind() { HirKind::Var(var) => Tir::from_hir(hir, env.lookup(*var)), + HirKind::MissingVar(var) => mkerr( + ErrorBuilder::new(format!("unbound variable `{}`", var)) + .span_err(hir.span(), "not found in this scope") + .format(), + )?, HirKind::Import(import) => { let typed = env.cx()[import].unwrap_result(); Tir::from_hir(hir, typed.ty.clone()) -- cgit v1.3.1 From 4473f3549f331c51a7df0e307d356a06c00d7288 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 7 Dec 2020 19:02:07 +0000 Subject: Resolve imports and alternatives outside of the ast traversal --- dhall/src/ctxt.rs | 203 ++++++++++++++++++++++----------- dhall/src/lib.rs | 2 +- dhall/src/semantics/nze/normalize.rs | 8 ++ dhall/src/semantics/resolve/hir.rs | 14 ++- dhall/src/semantics/resolve/resolve.rs | 189 ++++++++++++++++++++---------- dhall/src/semantics/tck/typecheck.rs | 8 ++ 6 files changed, 294 insertions(+), 130 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/ctxt.rs b/dhall/src/ctxt.rs index 3809bc9..aad1a1b 100644 --- a/dhall/src/ctxt.rs +++ b/dhall/src/ctxt.rs @@ -3,29 +3,19 @@ use once_cell::sync::OnceCell; use std::marker::PhantomData; use std::ops::{Deref, Index}; -use crate::semantics::{Import, ImportLocation}; +use crate::semantics::{Import, ImportLocation, ImportNode}; use crate::syntax::Span; use crate::Typed; -#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)] -pub struct ImportId<'cx>(usize, PhantomData<&'cx ()>); -#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)] -pub struct ImportResultId<'cx>(usize, PhantomData<&'cx ()>); - -/// What's stored for each `ImportId`. Allows getting and setting a result for this import. -pub struct StoredImport<'cx> { - cx: Ctxt<'cx>, - pub base_location: ImportLocation, - pub import: Import, - pub span: Span, - result: OnceCell>, -} +///////////////////////////////////////////////////////////////////////////////////////////////////// +// Ctxt /// Implementation detail. Made public for the `Index` instances. #[derive(Default)] pub struct CtxtS<'cx> { imports: FrozenVec>>, - import_results: FrozenVec>>, + import_alternatives: FrozenVec>>, + import_results: FrozenVec>>, } /// Context for the dhall compiler. Stores various global maps. @@ -40,33 +30,46 @@ impl Ctxt<'_> { f(cx) } } -impl<'cx> Ctxt<'cx> { - /// Store an import and the location relative to which it must be resolved. - pub fn push_import( - self, - base_location: ImportLocation, - import: Import, - span: Span, - ) -> ImportId<'cx> { - let stored = StoredImport { - cx: self, - base_location, - import, - span, - result: OnceCell::new(), - }; - let id = self.0.imports.len(); - self.0.imports.push(Box::new(stored)); - ImportId(id, PhantomData) +impl<'cx> Deref for Ctxt<'cx> { + type Target = &'cx CtxtS<'cx>; + fn deref(&self) -> &&'cx CtxtS<'cx> { + &self.0 } - /// Store the result of fetching an import. - pub fn push_import_result(self, res: Typed<'cx>) -> ImportResultId<'cx> { - let id = self.0.import_results.len(); - self.0.import_results.push(Box::new(res)); - ImportResultId(id, PhantomData) +} +impl<'a, 'cx, T> Index<&'a T> for CtxtS<'cx> +where + Self: Index, + T: Copy, +{ + type Output = >::Output; + fn index(&self, id: &'a T) -> &Self::Output { + &self[*id] + } +} + +/// Empty impl, because `FrozenVec` does not implement `Debug` and I can't be bothered to do it +/// myself. +impl<'cx> std::fmt::Debug for Ctxt<'cx> { + fn fmt(&self, _: &mut std::fmt::Formatter) -> std::fmt::Result { + Ok(()) } } +///////////////////////////////////////////////////////////////////////////////////////////////////// +// Imports + +#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)] +pub struct ImportId<'cx>(usize, PhantomData<&'cx ()>); + +/// What's stored for each `ImportId`. Allows getting and setting a result for this import. +pub struct StoredImport<'cx> { + cx: Ctxt<'cx>, + pub base_location: ImportLocation, + pub import: Import, + pub span: Span, + result: OnceCell>, +} + impl<'cx> StoredImport<'cx> { /// Get the id of the result of fetching this import. Returns `None` if the result has not yet /// been fetched. @@ -79,58 +82,130 @@ 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<'cx>> { + pub fn get_result(&self) -> Option<&'cx StoredImportResult<'cx>> { let res = self.get_resultid()?; Some(&self.cx[res]) } /// Get the result of fetching this import. Panicx if the result has not yet been /// fetched. - pub fn unwrap_result(&self) -> &'cx Typed<'cx> { + pub fn unwrap_result(&self) -> &'cx StoredImportResult<'cx> { self.get_result() .expect("imports should all have been resolved at this stage") } /// Store the result of fetching this import. - pub fn set_result(&self, res: Typed<'cx>) -> ImportResultId<'cx> { + pub fn set_result( + &self, + res: StoredImportResult<'cx>, + ) -> ImportResultId<'cx> { let res = self.cx.push_import_result(res); self.set_resultid(res); res } } - -impl<'cx> Deref for Ctxt<'cx> { - type Target = &'cx CtxtS<'cx>; - fn deref(&self) -> &&'cx CtxtS<'cx> { - &self.0 +impl<'cx> Ctxt<'cx> { + /// Store an import and the location relative to which it must be resolved. + pub fn push_import( + self, + base_location: ImportLocation, + import: Import, + span: Span, + ) -> ImportId<'cx> { + let stored = StoredImport { + cx: self, + base_location, + import, + span, + result: OnceCell::new(), + }; + let id = self.0.imports.len(); + self.0.imports.push(Box::new(stored)); + ImportId(id, PhantomData) } } - impl<'cx> Index> for CtxtS<'cx> { type Output = StoredImport<'cx>; fn index(&self, id: ImportId<'cx>) -> &StoredImport<'cx> { &self.imports[id.0] } } -impl<'cx> Index> for CtxtS<'cx> { - type Output = Typed<'cx>; - fn index(&self, id: ImportResultId<'cx>) -> &Typed<'cx> { - &self.import_results[id.0] + +///////////////////////////////////////////////////////////////////////////////////////////////////// +// Import alternatives + +#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)] +pub struct ImportAlternativeId<'cx>(usize, PhantomData<&'cx ()>); + +/// What's stored for each `ImportAlternativeId`. +pub struct StoredImportAlternative<'cx> { + pub left_imports: Box<[ImportNode<'cx>]>, + pub right_imports: Box<[ImportNode<'cx>]>, + /// `true` for left, `false` for right. + selected: OnceCell, +} + +impl<'cx> StoredImportAlternative<'cx> { + /// Get which alternative got selected. `true` for left, `false` for right. + pub fn get_selected(&self) -> Option { + self.selected.get().copied() + } + /// Get which alternative got selected. `true` for left, `false` for right. + pub fn unwrap_selected(&self) -> bool { + self.get_selected() + .expect("imports should all have been resolved at this stage") + } + /// Set which alternative got selected. `true` for left, `false` for right. + pub fn set_selected(&self, selected: bool) { + let _ = self.selected.set(selected); } } -impl<'a, 'cx, T> Index<&'a T> for CtxtS<'cx> -where - Self: Index, - T: Copy, -{ - type Output = >::Output; - fn index(&self, id: &'a T) -> &Self::Output { - &self[*id] +impl<'cx> Ctxt<'cx> { + pub fn push_import_alternative( + self, + left_imports: Box<[ImportNode<'cx>]>, + right_imports: Box<[ImportNode<'cx>]>, + ) -> ImportAlternativeId<'cx> { + let stored = StoredImportAlternative { + left_imports, + right_imports, + selected: OnceCell::new(), + }; + let id = self.0.import_alternatives.len(); + self.0.import_alternatives.push(Box::new(stored)); + ImportAlternativeId(id, PhantomData) + } +} +impl<'cx> Index> for CtxtS<'cx> { + type Output = StoredImportAlternative<'cx>; + fn index( + &self, + id: ImportAlternativeId<'cx>, + ) -> &StoredImportAlternative<'cx> { + &self.import_alternatives[id.0] } } -/// Empty impl, because `FrozenVec` does not implement `Debug` and I can't be bothered to do it -/// myself. -impl<'cx> std::fmt::Debug for Ctxt<'cx> { - fn fmt(&self, _: &mut std::fmt::Formatter) -> std::fmt::Result { - Ok(()) +///////////////////////////////////////////////////////////////////////////////////////////////////// +// Import results + +#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)] +pub struct ImportResultId<'cx>(usize, PhantomData<&'cx ()>); + +type StoredImportResult<'cx> = Typed<'cx>; + +impl<'cx> Ctxt<'cx> { + /// Store the result of fetching an import. + pub fn push_import_result( + self, + res: StoredImportResult<'cx>, + ) -> ImportResultId<'cx> { + let id = self.0.import_results.len(); + self.0.import_results.push(Box::new(res)); + ImportResultId(id, PhantomData) + } +} +impl<'cx> Index> for CtxtS<'cx> { + type Output = StoredImportResult<'cx>; + fn index(&self, id: ImportResultId<'cx>) -> &StoredImportResult<'cx> { + &self.import_results[id.0] } } diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index c27b633..03d3931 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -26,7 +26,7 @@ use crate::semantics::resolve::ImportLocation; use crate::semantics::{typecheck, typecheck_with, Hir, Nir, Tir, Type}; use crate::syntax::Expr; -pub use ctxt::{Ctxt, ImportId, ImportResultId}; +pub use ctxt::*; #[derive(Debug, Clone)] pub struct Parsed(Expr, ImportLocation); diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index 0a09a80..59710d1 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -160,6 +160,14 @@ pub fn normalize_hir<'cx>(env: &NzEnv<'cx>, hir: &Hir<'cx>) -> NirKind<'cx> { let typed = env.cx()[import].unwrap_result(); normalize_hir(env, &typed.hir) } + HirKind::ImportAlternative(alt, left, right) => { + let hir = if env.cx()[alt].unwrap_selected() { + left + } else { + right + }; + normalize_hir(env, hir) + } HirKind::Expr(ExprKind::Lam(binder, annot, body)) => { let annot = annot.eval(env); NirKind::LamClosure { diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs index 05a8550..8baad10 100644 --- a/dhall/src/semantics/resolve/hir.rs +++ b/dhall/src/semantics/resolve/hir.rs @@ -1,7 +1,7 @@ use crate::error::TypeError; use crate::semantics::{type_with, typecheck, NameEnv, Nir, NzEnv, Tir, TyEnv}; use crate::syntax::{Expr, ExprKind, Span, V}; -use crate::{Ctxt, ImportId, ToExprOptions}; +use crate::{Ctxt, ImportAlternativeId, ImportId, ToExprOptions}; /// Stores an alpha-normalized variable. #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] @@ -15,8 +15,10 @@ pub enum HirKind<'cx> { Var(AlphaVar), /// A variable that couldn't be resolved. Detected during resolution, but causes an error during typeck. MissingVar(V), - /// An import. It must have been resolved by the time we get to typechecking/normalization. + /// An import. It must have been resolved after resolution. Import(ImportId<'cx>), + /// An import alternative. It must have been decided after resolution. + ImportAlternative(ImportAlternativeId<'cx>, Hir<'cx>, Hir<'cx>), // Forbidden ExprKind variants: Var, Import, Completion Expr(ExprKind>), } @@ -111,6 +113,14 @@ fn hir_to_expr<'cx>( let typed = cx[import].unwrap_result(); return hir_to_expr(cx, &typed.hir, opts, &mut NameEnv::new()); } + HirKind::ImportAlternative(alt, left, right) => { + let hir = if cx[alt].unwrap_selected() { + left + } else { + right + }; + return hir_to_expr(cx, hir, opts, env); + } HirKind::Expr(e) => { let e = e.map_ref_maybe_binder(|l, hir| { if let Some(l) = l { diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs index c4cd518..116e1a5 100644 --- a/dhall/src/semantics/resolve/resolve.rs +++ b/dhall/src/semantics/resolve/resolve.rs @@ -15,7 +15,10 @@ use crate::syntax::{ Expr, ExprKind, FilePath, FilePrefix, Hash, ImportMode, ImportTarget, Span, UnspannedExpr, URL, }; -use crate::{Ctxt, ImportId, ImportResultId, Parsed, Resolved, Typed}; +use crate::{ + Ctxt, ImportAlternativeId, ImportId, ImportResultId, Parsed, Resolved, + Typed, +}; // TODO: evaluate import headers pub type Import = syntax::Import<()>; @@ -252,7 +255,7 @@ impl ImportLocation { let typed = match self.mode { ImportMode::Code => { let parsed = self.kind.fetch_dhall()?; - let typed = resolve_with_env(env, parsed)?.typecheck(cx)?; + let typed = parsed.resolve_with_env(env)?.typecheck(cx)?; Typed { // TODO: manage to keep the Nir around. Will need fixing variables. hir: typed.normalize(cx).to_hir(), @@ -366,56 +369,6 @@ 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<'cx>( - name_env: &mut NameEnv, - expr: &Expr, - 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) { - Some(v) => Hir::new(HirKind::Var(v), expr.span()), - None => Hir::new(HirKind::MissingVar(var.clone()), expr.span()), - }, - ExprKind::Op(OpKind::BinOp(BinOp::ImportAlt, l, r)) => { - match traverse_resolve_expr(name_env, l, f) { - Ok(l) => l, - Err(_) => { - match traverse_resolve_expr(name_env, r, f) { - Ok(r) => r, - // TODO: keep track of the other error too - Err(e) => return Err(e), - } - } - } - } - kind => { - let kind = kind.traverse_ref_maybe_binder(|l, e| { - if let Some(l) = l { - name_env.insert_mut(l); - } - let hir = traverse_resolve_expr(name_env, e, f)?; - if l.is_some() { - name_env.remove_mut(); - } - Ok::<_, Error>(hir) - })?; - let kind = match kind { - ExprKind::Import(import) => { - // TODO: evaluate import headers - let import = import.traverse_ref(|_| Ok::<_, Error>(()))?; - let import_id = f(import, expr.span())?; - HirKind::Import(import_id) - } - kind => HirKind::Expr(kind), - }; - Hir::new(kind, expr.span()) - } - }) -} - /// Fetch the import and store the result in the global context. fn fetch_import<'cx>( env: &mut ImportEnv<'cx>, @@ -469,22 +422,123 @@ fn fetch_import<'cx>( Ok(res_id) } +/// Part of a tree of imports. +#[derive(Debug, Clone, Copy)] +pub enum ImportNode<'cx> { + Import(ImportId<'cx>), + Alternative(ImportAlternativeId<'cx>), +} + +/// Traverse the expression and replace each import and import alternative by an id into the global +/// context. The ids are also accumulated into `nodes` so that we can resolve them afterwards. +fn traverse_accumulate<'cx>( + env: &mut ImportEnv<'cx>, + name_env: &mut NameEnv, + nodes: &mut Vec>, + base_location: &ImportLocation, + expr: &Expr, +) -> Hir<'cx> { + let cx = env.cx(); + let expr = desugar(expr); + let kind = match expr.kind() { + ExprKind::Var(var) => match name_env.unlabel_var(&var) { + Some(v) => HirKind::Var(v), + None => HirKind::MissingVar(var.clone()), + }, + ExprKind::Op(OpKind::BinOp(BinOp::ImportAlt, l, r)) => { + let mut imports_l = Vec::new(); + let l = traverse_accumulate( + env, + name_env, + &mut imports_l, + base_location, + l, + ); + let mut imports_r = Vec::new(); + let r = traverse_accumulate( + env, + name_env, + &mut imports_r, + base_location, + r, + ); + let alt = + cx.push_import_alternative(imports_l.into(), imports_r.into()); + nodes.push(ImportNode::Alternative(alt)); + HirKind::ImportAlternative(alt, l, r) + } + kind => { + let kind = kind.map_ref_maybe_binder(|l, e| { + if let Some(l) = l { + name_env.insert_mut(l); + } + let hir = + traverse_accumulate(env, name_env, nodes, base_location, e); + if l.is_some() { + name_env.remove_mut(); + } + hir + }); + match kind { + ExprKind::Import(import) => { + // TODO: evaluate import headers + let import = import.map_ref(|_| ()); + let import_id = cx.push_import( + base_location.clone(), + import, + expr.span(), + ); + nodes.push(ImportNode::Import(import_id)); + HirKind::Import(import_id) + } + kind => HirKind::Expr(kind), + } + } + }; + Hir::new(kind, expr.span()) +} + +/// Take a list of nodes and recursively resolve them. +fn resolve_nodes<'cx>( + env: &mut ImportEnv<'cx>, + nodes: &[ImportNode<'cx>], +) -> Result<(), Error> { + for &node in nodes { + match node { + ImportNode::Import(import) => { + let res_id = fetch_import(env, import)?; + env.cx()[import].set_resultid(res_id); + } + ImportNode::Alternative(alt) => { + let alt = &env.cx()[alt]; + if resolve_nodes(env, &alt.left_imports).is_ok() { + alt.set_selected(true); + } else { + resolve_nodes(env, &alt.right_imports)?; + alt.set_selected(false); + } + } + } + } + Ok(()) +} + fn resolve_with_env<'cx>( env: &mut ImportEnv<'cx>, parsed: Parsed, ) -> Result, Error> { let Parsed(expr, base_location) = parsed; - let resolved = traverse_resolve_expr( + let mut nodes = Vec::new(); + // First we collect all imports. + let resolved = traverse_accumulate( + env, &mut NameEnv::new(), + &mut nodes, + &base_location, &expr, - &mut |import, span| { - let import_id = - env.cx().push_import(base_location.clone(), import, span); - let res_id = fetch_import(env, import_id)?; - env.cx()[import_id].set_resultid(res_id); - Ok(import_id) - }, - )?; + ); + // Then we resolve them and choose sides for the alternatives. + resolve_nodes(env, &nodes)?; Ok(Resolved(resolved)) } @@ -494,10 +548,10 @@ pub fn resolve<'cx>( cx: Ctxt<'cx>, parsed: Parsed, ) -> Result, Error> { - resolve_with_env(&mut ImportEnv::new(cx), parsed) + parsed.resolve_with_env(&mut ImportEnv::new(cx)) } -/// Resolves names and errors if we find any imports. +/// Resolves names, and errors if we find any imports. pub fn skip_resolve<'cx>( cx: Ctxt<'cx>, parsed: Parsed, @@ -506,6 +560,15 @@ pub fn skip_resolve<'cx>( Ok(resolve(cx, parsed)?) } +impl Parsed { + fn resolve_with_env<'cx>( + self, + env: &mut ImportEnv<'cx>, + ) -> Result, Error> { + resolve_with_env(env, self) + } +} + pub trait Canonicalize { fn canonicalize(&self) -> Self; } diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index e14bcc6..23c2bd2 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -193,6 +193,14 @@ pub fn type_with<'cx, 'hir>( let typed = env.cx()[import].unwrap_result(); Tir::from_hir(hir, typed.ty.clone()) } + HirKind::ImportAlternative(alt, left, right) => { + let hir = if env.cx()[alt].unwrap_selected() { + left + } else { + right + }; + return type_with(env, hir, annot); + } HirKind::Expr(ExprKind::Var(_)) => { unreachable!("Hir should contain no unresolved variables") } -- cgit v1.3.1