diff options
author | Nadrieril | 2020-02-10 19:14:07 +0000 |
---|---|---|
committer | Nadrieril | 2020-02-10 19:14:07 +0000 |
commit | c3ed75dc4b354becac0821e4288105dc2a300c4c (patch) | |
tree | b85acbcfe0bdd0591cfc197de6bd68d9482801a6 | |
parent | 35cc98dc767247f4881866de40c7d8dd82eba8a5 (diff) |
Remove need for Embed
This was an archaic leftover from copying the Haskell datatypes anyway
-rw-r--r-- | dhall/src/semantics/hir.rs | 1 | ||||
-rw-r--r-- | dhall/src/semantics/nze/env.rs | 6 | ||||
-rw-r--r-- | dhall/src/semantics/resolve.rs | 25 | ||||
-rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 10 |
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) => { |