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/builtins.rs | 19 ++++++---- dhall/src/lib.rs | 15 +++++++- 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 +- serde_dhall/src/options/de.rs | 2 +- serde_dhall/tests/serde.rs | 19 ++++++++++ 8 files changed, 94 insertions(+), 40 deletions(-) diff --git a/dhall/src/builtins.rs b/dhall/src/builtins.rs index 39cc4ef..123e03d 100644 --- a/dhall/src/builtins.rs +++ b/dhall/src/builtins.rs @@ -2,15 +2,13 @@ use std::collections::{BTreeMap, HashMap}; use std::convert::TryInto; use crate::operations::{BinOp, OpKind}; -use crate::semantics::{ - nze, skip_resolve_expr, typecheck, Hir, HirKind, Nir, NirKind, NzEnv, - VarEnv, -}; +use crate::semantics::{nze, Hir, HirKind, Nir, NirKind, NzEnv, VarEnv}; use crate::syntax::Const::Type; use crate::syntax::{ Const, Expr, ExprKind, InterpolatedText, InterpolatedTextContents, Label, NaiveDouble, NumKind, Span, UnspannedExpr, V, }; +use crate::{Ctxt, Parsed}; /// Built-ins #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)] @@ -178,7 +176,7 @@ macro_rules! make_type { }; } -pub fn type_of_builtin<'cx>(b: Builtin) -> Hir<'cx> { +pub fn type_of_builtin<'cx>(cx: Ctxt<'cx>, b: Builtin) -> Hir<'cx> { use Builtin::*; let expr = match b { Bool | Natural | Integer | Double | Text => make_type!(Type), @@ -253,7 +251,10 @@ pub fn type_of_builtin<'cx>(b: Builtin) -> Hir<'cx> { forall (A: Type) -> Optional A ), }; - skip_resolve_expr(&expr).unwrap() + Parsed::from_expr_without_imports(expr) + .resolve(cx) + .unwrap() + .0 } // Ad-hoc macro to help construct closures @@ -323,8 +324,12 @@ fn apply_builtin<'cx>( DoneAsIs, } let make_closure = |e| { - typecheck(cx, &skip_resolve_expr(&e).unwrap()) + Parsed::from_expr_without_imports(e) + .resolve(cx) + .unwrap() + .typecheck(cx) .unwrap() + .as_hir() .eval(env.clone()) }; diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index 7f77334..c27b633 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -58,6 +58,11 @@ pub struct ToExprOptions { } impl Parsed { + /// Construct from an `Expr`. This `Expr` will have imports disabled. + pub fn from_expr_without_imports(e: Expr) -> Self { + Parsed(e, ImportLocation::dhall_code_without_imports()) + } + pub fn parse_file(f: &Path) -> Result { parse::parse_file(f) } @@ -78,8 +83,11 @@ impl Parsed { pub fn resolve<'cx>(self, cx: Ctxt<'cx>) -> Result, Error> { resolve::resolve(cx, self) } - pub fn skip_resolve<'cx>(self) -> Result, Error> { - resolve::skip_resolve(self) + pub fn skip_resolve<'cx>( + self, + cx: Ctxt<'cx>, + ) -> Result, Error> { + resolve::skip_resolve(cx, self) } /// Converts a value back to the corresponding AST expression. @@ -122,6 +130,9 @@ impl<'cx> Typed<'cx> { self.hir.to_expr(cx, ToExprOptions { alpha: false }) } + pub fn as_hir(&self) -> &Hir<'cx> { + &self.hir + } pub fn ty(&self) -> &Type<'cx> { &self.ty } 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); diff --git a/serde_dhall/src/options/de.rs b/serde_dhall/src/options/de.rs index fc8c6dc..30846a2 100644 --- a/serde_dhall/src/options/de.rs +++ b/serde_dhall/src/options/de.rs @@ -243,7 +243,7 @@ impl<'a, A> Deserializer<'a, A> { let resolved = if self.allow_imports { parsed.resolve(cx)? } else { - parsed.skip_resolve()? + parsed.skip_resolve(cx)? }; let typed = match &T::get_annot(self.annot) { None => resolved.typecheck(cx)?, diff --git a/serde_dhall/tests/serde.rs b/serde_dhall/tests/serde.rs index 1181f72..fe0bffb 100644 --- a/serde_dhall/tests/serde.rs +++ b/serde_dhall/tests/serde.rs @@ -226,6 +226,25 @@ mod serde { Ok(true) ); } + + #[test] + fn test_import() { + assert_de( + "../dhall-lang/tests/parser/success/unit/BoolLitTrueA.dhall", + true, + ); + assert_eq!( + serde_dhall::from_str( + "../dhall-lang/tests/parser/success/unit/BoolLitTrueA.dhall" + ) + .imports(false) + .static_type_annotation() + .parse::() + .map_err(|e| e.to_string()), + Err("UnexpectedImport(Import { mode: Code, location: Local(Parent, FilePath { file_path: [\"dhall-lang\", \"tests\", \"parser\", \"success\", \"unit\", \"BoolLitTrueA.dhall\"] }), hash: None })".to_string()) + ); + } + // TODO: test various builder configurations // In particular test cloning and reusing builder } -- cgit v1.2.3