summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2020-12-07 14:32:06 +0000
committerNadrieril2020-12-07 19:34:39 +0000
commitc1fe26d45c831eec015ad5c015236fce1928613a (patch)
treebdba83d6854005d4de29fc38427967989367da6f
parent8c5b3ff15f2125e9d731fc199e194e1993c36b37 (diff)
Pass import results via the global context
-rw-r--r--dhall/src/semantics/nze/normalize.rs5
-rw-r--r--dhall/src/semantics/resolve/hir.rs13
-rw-r--r--dhall/src/semantics/resolve/resolve.rs9
-rw-r--r--dhall/src/semantics/tck/typecheck.rs5
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")
}