From 922199ab322efa7b62bf4698cf5ed9e2d7a378c0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 7 Dec 2020 15:24:36 +0000 Subject: Unify `skip_resolve_expr` with normal resolution --- dhall/src/semantics/resolve/cache.rs | 2 +- dhall/src/semantics/resolve/hir.rs | 4 +- dhall/src/semantics/resolve/resolve.rs | 69 ++++++++++++++++++++++------------ dhall/src/semantics/tck/typecheck.rs | 4 +- 4 files changed, 49 insertions(+), 30 deletions(-) (limited to 'dhall/src/semantics') diff --git a/dhall/src/semantics/resolve/cache.rs b/dhall/src/semantics/resolve/cache.rs index 9a5e835..1fc8dd3 100644 --- a/dhall/src/semantics/resolve/cache.rs +++ b/dhall/src/semantics/resolve/cache.rs @@ -94,7 +94,7 @@ fn read_cache_file<'cx>( } } - Ok(parse_binary(&data)?.skip_resolve()?.typecheck(cx)?) + Ok(parse_binary(&data)?.resolve(cx)?.typecheck(cx)?) } /// Write a file to the cache. diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs index cfde47e..3e282b4 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, typecheck, NameEnv, Nir, NzEnv, Tir, TyEnv}; use crate::syntax::{Expr, ExprKind, Span, V}; use crate::{Ctxt, ImportId, ToExprOptions}; @@ -81,7 +81,7 @@ impl<'cx> Hir<'cx> { &'hir self, cx: Ctxt<'cx>, ) -> Result, TypeError> { - self.typecheck(&TyEnv::new(cx)) + typecheck(cx, self) } /// Eval the Hir. It will actually get evaluated only as needed on demand. diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs index 011ed45..e040cf4 100644 --- a/dhall/src/semantics/resolve/resolve.rs +++ b/dhall/src/semantics/resolve/resolve.rs @@ -29,8 +29,10 @@ enum ImportLocationKind { Remote(Url), /// Environment variable Env(String), - /// Data without a location + /// Data without a location; chaining will start from current directory. Missing, + /// Token to signal that thi sfile should contain no imports. + NoImport, } /// The location of some data. @@ -101,6 +103,7 @@ impl ImportLocationKind { url = url.join(&path.file_path.join("/"))?; ImportLocationKind::Remote(url) } + ImportLocationKind::NoImport => unreachable!(), }) } @@ -120,6 +123,7 @@ impl ImportLocationKind { ImportLocationKind::Missing => { return Err(ImportError::Missing.into()) } + ImportLocationKind::NoImport => unreachable!(), }) } @@ -134,6 +138,7 @@ impl ImportLocationKind { ImportLocationKind::Missing => { return Err(ImportError::Missing.into()) } + ImportLocationKind::NoImport => unreachable!(), }) } @@ -149,6 +154,7 @@ impl ImportLocationKind { ("Environment", Some(name.clone())) } ImportLocationKind::Missing => ("Missing", None), + ImportLocationKind::NoImport => unreachable!(), }; let asloc_ty = make_aslocation_uniontype(); @@ -171,6 +177,12 @@ impl ImportLocation { mode: ImportMode::Code, } } + pub fn dhall_code_without_imports() -> Self { + ImportLocation { + kind: ImportLocationKind::NoImport, + mode: ImportMode::Code, + } + } pub fn local_dhall_code(path: PathBuf) -> Self { ImportLocation { kind: ImportLocationKind::Local(path), @@ -191,6 +203,10 @@ impl ImportLocation { fn chain(&self, import: &Import) -> Result { // Makes no sense to chain an import if the current file is not a dhall file. assert!(matches!(self.mode, ImportMode::Code)); + if matches!(self.kind, ImportLocationKind::NoImport) { + Err(ImportError::UnexpectedImport(import.clone()))?; + } + let kind = match &import.location { ImportTarget::Local(prefix, path) => { self.kind.chain_local(*prefix, path)? @@ -232,30 +248,37 @@ impl ImportLocation { env: &mut ImportEnv<'cx>, span: Span, ) -> Result, Error> { - let (hir, ty) = match self.mode { + let cx = env.cx(); + let typed = match self.mode { ImportMode::Code => { let parsed = self.kind.fetch_dhall()?; - let typed = - resolve_with_env(env, parsed)?.typecheck(env.cx())?; - let hir = typed.normalize(env.cx()).to_hir(); - (hir, typed.ty) + let typed = resolve_with_env(env, parsed)?.typecheck(cx)?; + Typed { + // TODO: manage to keep the Nir around. Will need fixing variables. + hir: typed.normalize(cx).to_hir(), + ty: typed.ty, + } } ImportMode::RawText => { let text = self.kind.fetch_text()?; - let hir = Hir::new( - HirKind::Expr(ExprKind::TextLit(text.into())), - span, - ); - (hir, Type::from_builtin(env.cx(), Builtin::Text)) + Typed { + hir: Hir::new( + HirKind::Expr(ExprKind::TextLit(text.into())), + span, + ), + ty: Type::from_builtin(cx, Builtin::Text), + } } ImportMode::Location => { let expr = self.kind.to_location(); - let hir = skip_resolve_expr(&expr)?; - let ty = hir.typecheck_noenv(env.cx())?.ty().clone(); - (hir, ty) + Parsed::from_expr_without_imports(expr) + .resolve(cx) + .unwrap() + .typecheck(cx) + .unwrap() } }; - Ok(Typed { hir, ty }) + Ok(typed) } } @@ -476,16 +499,12 @@ pub fn resolve<'cx>( resolve_with_env(&mut ImportEnv::new(cx), parsed) } -pub fn skip_resolve_expr<'cx>(expr: &Expr) -> Result, Error> { - traverse_resolve_expr(&mut NameEnv::new(), expr, &mut |import, _span| { - Err(ImportError::UnexpectedImport(import).into()) - }) -} - -pub fn skip_resolve<'cx>(parsed: Parsed) -> Result, Error> { - let Parsed(expr, _) = parsed; - let resolved = skip_resolve_expr(&expr)?; - Ok(Resolved(resolved)) +pub fn skip_resolve<'cx>( + cx: Ctxt<'cx>, + parsed: Parsed, +) -> Result, Error> { + let parsed = Parsed::from_expr_without_imports(parsed.0); + Ok(resolve(cx, parsed)?) } pub trait Canonicalize { diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index f47563e..5a44c9c 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -62,8 +62,8 @@ fn type_one_layer<'cx>( }, ), ExprKind::Builtin(b) => { - let t_hir = type_of_builtin(b); - typecheck(env.cx(), &t_hir)?.eval_to_type(env)? + let t_hir = type_of_builtin(cx, b); + typecheck(cx, &t_hir)?.eval_to_type(env)? } ExprKind::TextLit(interpolated) => { let text_type = Type::from_builtin(cx, Builtin::Text); -- cgit v1.2.3