diff options
| -rw-r--r-- | dhall/src/semantics/nze/normalize.rs | 5 | ||||
| -rw-r--r-- | dhall/src/semantics/resolve/hir.rs | 13 | ||||
| -rw-r--r-- | dhall/src/semantics/resolve/resolve.rs | 9 | ||||
| -rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 5 |
4 files changed, 19 insertions, 13 deletions
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<Nir<'cx>>) -> 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<Hir<'cx>>), } @@ -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<Typed<'cx>, Error>, + f: &mut impl FnMut(Import, Span) -> Result<ImportId<'cx>, Error>, ) -> Result<Hir<'cx>, 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<Tir<'cx, 'hir>, TypeError> { let tir = match hir.kind() { HirKind::Var(var) => Tir::from_hir(hir, env.lookup(*var)), - HirKind::Import(_, ty) => Tir::from_hir(hir, ty.clone()), + 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") } |