summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
authorNadrieril2020-02-10 19:14:07 +0000
committerNadrieril2020-02-10 19:14:07 +0000
commitc3ed75dc4b354becac0821e4288105dc2a300c4c (patch)
treeb85acbcfe0bdd0591cfc197de6bd68d9482801a6 /dhall
parent35cc98dc767247f4881866de40c7d8dd82eba8a5 (diff)
Remove need for Embed
This was an archaic leftover from copying the Haskell datatypes anyway
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/semantics/hir.rs1
-rw-r--r--dhall/src/semantics/nze/env.rs6
-rw-r--r--dhall/src/semantics/resolve.rs25
-rw-r--r--dhall/src/semantics/tck/typecheck.rs10
4 files changed, 22 insertions, 20 deletions
diff --git a/dhall/src/semantics/hir.rs b/dhall/src/semantics/hir.rs
index 9ad7374..b45851f 100644
--- a/dhall/src/semantics/hir.rs
+++ b/dhall/src/semantics/hir.rs
@@ -11,6 +11,7 @@ pub struct AlphaVar {
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub(crate) enum HirKind {
+ /// A resolved variable (i.e. a DeBruijn index)
Var(AlphaVar),
// Forbidden ExprKind variants: Var, Import, Embed
Expr(ExprKind<Hir, Normalized>),
diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs
index 5b036f0..241af40 100644
--- a/dhall/src/semantics/nze/env.rs
+++ b/dhall/src/semantics/nze/env.rs
@@ -86,3 +86,9 @@ impl<Type: Clone> ValEnv<Type> {
}
}
}
+
+impl<'a> From<&'a NzEnv> for NzEnv {
+ fn from(x: &'a NzEnv) -> Self {
+ x.clone()
+ }
+}
diff --git a/dhall/src/semantics/resolve.rs b/dhall/src/semantics/resolve.rs
index 8c9bb05..80e5132 100644
--- a/dhall/src/semantics/resolve.rs
+++ b/dhall/src/semantics/resolve.rs
@@ -16,7 +16,7 @@ pub(crate) enum ImportRoot {
LocalDir(PathBuf),
}
-type ImportCache = HashMap<Import, Normalized>;
+type ImportCache = HashMap<Import, Hir>;
pub(crate) type ImportStack = Vec<Import>;
@@ -36,8 +36,8 @@ impl ResolveEnv {
pub fn handle_import(
&mut self,
import: Import,
- mut do_resolve: impl FnMut(&mut Self, &Import) -> Result<Normalized, Error>,
- ) -> Result<Normalized, Error> {
+ mut do_resolve: impl FnMut(&mut Self, &Import) -> Result<Hir, Error>,
+ ) -> Result<Hir, Error> {
if self.stack.contains(&import) {
return Err(
ImportError::ImportCycle(self.stack.clone(), import).into()
@@ -68,7 +68,7 @@ fn resolve_one_import(
env: &mut ResolveEnv,
import: &Import,
root: &ImportRoot,
-) -> Result<Normalized, Error> {
+) -> Result<Hir, Error> {
use self::ImportRoot::*;
use syntax::FilePrefix::*;
use syntax::ImportLocation::*;
@@ -90,9 +90,12 @@ fn resolve_one_import(
}
}
-fn load_import(env: &mut ResolveEnv, f: &Path) -> Result<Normalized, Error> {
+fn load_import(env: &mut ResolveEnv, f: &Path) -> Result<Hir, Error> {
let parsed = Parsed::parse_file(f)?;
- Ok(resolve_with_env(env, parsed)?.typecheck()?.normalize())
+ Ok(resolve_with_env(env, parsed)?
+ .typecheck()?
+ .normalize()
+ .to_hir())
}
/// Traverse the expression, handling import alternatives and passing
@@ -100,7 +103,7 @@ fn load_import(env: &mut ResolveEnv, f: &Path) -> Result<Normalized, Error> {
fn traverse_resolve_expr(
name_env: &mut NameEnv,
expr: &Expr<Normalized>,
- f: &mut impl FnMut(Import) -> Result<Normalized, Error>,
+ f: &mut impl FnMut(Import) -> Result<Hir, Error>,
) -> Result<Hir, Error> {
let kind = match expr.kind() {
ExprKind::Var(var) => match name_env.unlabel_var(&var) {
@@ -134,10 +137,10 @@ fn traverse_resolve_expr(
}
Ok::<_, Error>(hir)
})?;
- HirKind::Expr(match kind {
- ExprKind::Import(import) => ExprKind::Embed(f(import)?),
- kind => kind,
- })
+ match kind {
+ ExprKind::Import(import) => f(import)?.kind().clone(),
+ kind => HirKind::Expr(kind),
+ }
}
};
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 7f02832..4e45637 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -761,21 +761,13 @@ fn type_one_layer(
/// `type_with` typechecks an expressio in the provided environment.
pub(crate) fn type_with(env: &TyEnv, hir: &Hir) -> Result<TyExpr, TypeError> {
let (tyekind, ty) = match hir.kind() {
- HirKind::Var(var) => (TyExprKind::Var(*var), Some(env.lookup(&var))),
+ HirKind::Var(var) => (TyExprKind::Var(*var), Some(env.lookup(var))),
HirKind::Expr(ExprKind::Var(_)) => {
unreachable!("Hir should contain no unresolved variables")
}
HirKind::Expr(ExprKind::Const(Const::Sort)) => {
(TyExprKind::Expr(ExprKind::Const(Const::Sort)), None)
}
- HirKind::Expr(ExprKind::Embed(p)) => {
- let val = p.clone().into_value();
- (
- val.to_tyexpr_noenv().kind().clone(),
- Some(val.get_type(&TyEnv::new())?),
- )
- // return Ok(p.clone().into_value().to_tyexpr_noenv())
- }
HirKind::Expr(ekind) => {
let ekind = match ekind {
ExprKind::Lam(binder, annot, body) => {