summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/src/error/mod.rs1
-rw-r--r--dhall/src/lib.rs3
-rw-r--r--dhall/src/semantics/nze/normalize.rs1
-rw-r--r--dhall/src/semantics/resolve/env.rs8
-rw-r--r--dhall/src/semantics/resolve/hir.rs7
-rw-r--r--dhall/src/semantics/resolve/resolve.rs20
-rw-r--r--dhall/src/semantics/tck/typecheck.rs1
7 files changed, 26 insertions, 15 deletions
diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index b8f2fca..8829d47 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -1,7 +1,6 @@
use std::io::Error as IOError;
use crate::semantics::resolve::ImportStack;
-use crate::semantics::Hir;
use crate::syntax::{Import, ParseError};
mod builder;
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index c2f5020..9922144 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -123,6 +123,9 @@ impl Typed {
self.hir.to_expr(ToExprOptions { alpha: false })
}
+ pub(crate) fn ty(&self) -> &Type {
+ &self.ty
+ }
pub(crate) fn get_type(&self) -> Result<Normalized, TypeError> {
Ok(Normalized(self.ty.clone().into_nir()))
}
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 4c2aa33..604db8f 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -442,6 +442,7 @@ pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> NirKind {
match hir.kind() {
HirKind::Var(var) => env.lookup_val(var),
+ HirKind::Import(hir, _) => normalize_hir_whnf(env, hir),
HirKind::Expr(ExprKind::Lam(binder, annot, body)) => {
let annot = annot.eval(env);
NirKind::LamClosure {
diff --git a/dhall/src/semantics/resolve/env.rs b/dhall/src/semantics/resolve/env.rs
index ff743d3..43676cc 100644
--- a/dhall/src/semantics/resolve/env.rs
+++ b/dhall/src/semantics/resolve/env.rs
@@ -1,7 +1,7 @@
use std::collections::HashMap;
use crate::error::{Error, ImportError};
-use crate::semantics::{AlphaVar, Hir, Import, VarEnv};
+use crate::semantics::{AlphaVar, Import, TypedHir, VarEnv};
use crate::syntax::{Label, V};
/// Environment for resolving names.
@@ -10,7 +10,7 @@ pub(crate) struct NameEnv {
names: Vec<Label>,
}
-pub(crate) type ImportCache = HashMap<Import, Hir>;
+pub(crate) type ImportCache = HashMap<Import, TypedHir>;
pub(crate) type ImportStack = Vec<Import>;
/// Environment for resolving imports
@@ -75,8 +75,8 @@ impl ImportEnv {
pub fn handle_import(
&mut self,
import: Import,
- mut do_resolve: impl FnMut(&mut Self, &Import) -> Result<Hir, Error>,
- ) -> Result<Hir, Error> {
+ mut do_resolve: impl FnMut(&mut Self, &Import) -> Result<TypedHir, Error>,
+ ) -> Result<TypedHir, Error> {
if self.stack.contains(&import) {
return Err(
ImportError::ImportCycle(self.stack.clone(), import).into()
diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs
index 73fc371..2f3464a 100644
--- a/dhall/src/semantics/resolve/hir.rs
+++ b/dhall/src/semantics/resolve/hir.rs
@@ -1,5 +1,5 @@
use crate::error::TypeError;
-use crate::semantics::{type_with, NameEnv, Nir, NzEnv, Tir, TyEnv};
+use crate::semantics::{type_with, NameEnv, Nir, NzEnv, Tir, TyEnv, Type};
use crate::syntax::{Expr, ExprKind, Span, V};
use crate::{NormalizedExpr, ToExprOptions};
@@ -13,6 +13,8 @@ pub struct AlphaVar {
pub(crate) enum HirKind {
/// A resolved variable (i.e. a DeBruijn index)
Var(AlphaVar),
+ /// Result of resolving an import.
+ Import(Hir, Type),
// Forbidden ExprKind variants: Var, Import, Completion
Expr(ExprKind<Hir>),
}
@@ -96,6 +98,9 @@ fn hir_to_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)),
+ HirKind::Import(hir, _) => {
+ return hir_to_expr(hir, opts, &mut NameEnv::new())
+ }
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 23d4c3d..82800ec 100644
--- a/dhall/src/semantics/resolve/resolve.rs
+++ b/dhall/src/semantics/resolve/resolve.rs
@@ -3,7 +3,7 @@ use std::path::{Path, PathBuf};
use crate::error::ErrorBuilder;
use crate::error::{Error, ImportError};
-use crate::semantics::{mkerr, Hir, HirKind, ImportEnv, NameEnv};
+use crate::semantics::{mkerr, Hir, HirKind, ImportEnv, NameEnv, Type};
use crate::syntax;
use crate::syntax::{BinOp, Expr, ExprKind, FilePath, ImportLocation, URL};
use crate::{Parsed, ParsedExpr, Resolved};
@@ -11,6 +11,9 @@ use crate::{Parsed, ParsedExpr, Resolved};
// TODO: evaluate import headers
pub(crate) type Import = syntax::Import<()>;
+/// Owned Hir with a type. Different from Tir because the Hir is owned.
+pub(crate) type TypedHir = (Hir, Type);
+
/// A root from which to resolve relative imports.
#[derive(Debug, Clone, PartialEq, Eq)]
pub(crate) enum ImportRoot {
@@ -21,7 +24,7 @@ fn resolve_one_import(
env: &mut ImportEnv,
import: &Import,
root: &ImportRoot,
-) -> Result<Hir, Error> {
+) -> Result<TypedHir, Error> {
use self::ImportRoot::*;
use syntax::FilePrefix::*;
use syntax::ImportLocation::*;
@@ -43,12 +46,10 @@ fn resolve_one_import(
}
}
-fn load_import(env: &mut ImportEnv, f: &Path) -> Result<Hir, Error> {
+fn load_import(env: &mut ImportEnv, f: &Path) -> Result<TypedHir, Error> {
let parsed = Parsed::parse_file(f)?;
- Ok(resolve_with_env(env, parsed)?
- .typecheck()?
- .normalize()
- .to_hir())
+ let typed = resolve_with_env(env, parsed)?.typecheck()?;
+ Ok((typed.normalize().to_hir(), typed.ty().clone()))
}
/// Desugar the first level of the expression.
@@ -85,7 +86,7 @@ fn desugar(expr: &Expr) -> Cow<'_, Expr> {
fn traverse_resolve_expr(
name_env: &mut NameEnv,
expr: &Expr,
- f: &mut impl FnMut(Import) -> Result<Hir, Error>,
+ f: &mut impl FnMut(Import) -> Result<TypedHir, Error>,
) -> Result<Hir, Error> {
let expr = desugar(expr);
Ok(match expr.kind() {
@@ -124,7 +125,8 @@ fn traverse_resolve_expr(
ExprKind::Import(import) => {
// TODO: evaluate import headers
let import = import.traverse_ref(|_| Ok::<_, Error>(()))?;
- f(import)?.kind().clone()
+ let imported = f(import)?;
+ HirKind::Import(imported.0, imported.1)
}
kind => HirKind::Expr(kind),
};
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 0787b32..972326b 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -710,6 +710,7 @@ pub(crate) fn type_with<'hir>(
) -> Result<Tir<'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::Expr(ExprKind::Var(_)) => {
unreachable!("Hir should contain no unresolved variables")
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 03:45:53 +0000