From 396ec334bac1e8d10a2d2b2d683c93e3b2ff4d8d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 6 Apr 2019 20:04:04 +0200 Subject: Massage import loading into new API Closes #9 --- dhall_core/src/core.rs | 39 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) (limited to 'dhall_core/src') diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs index a56c5a3..d832cd5 100644 --- a/dhall_core/src/core.rs +++ b/dhall_core/src/core.rs @@ -285,6 +285,28 @@ impl Expr { self.map_shallow(recurse, |x| x.clone(), map_embed, |x| x.clone()) } + #[inline(always)] + pub fn traverse_embed( + &self, + map_embed: &F, + ) -> Result, Err> + where + S: Clone, + B: Clone, + F: Fn(&A) -> Result, + { + let recurse = |e: &SubExpr| -> Result, Err> { + Ok(e.as_ref().traverse_embed(map_embed)?.roll()) + }; + self.as_ref().traverse( + |e| recurse(e), + |_, e| recurse(e), + |x| Ok(S::clone(x)), + map_embed, + |x| Ok(Label::clone(x)), + ) + } + pub fn map_label(&self, map_label: &F) -> Self where A: Clone, @@ -319,6 +341,23 @@ impl Expr> { } } +impl Expr> { + pub fn squash_embed(&self) -> SubExpr { + match self.as_ref() { + ExprF::Embed(e) => e.clone(), + e => e + .map( + |e| e.as_ref().squash_embed(), + |_, e| e.as_ref().squash_embed(), + S::clone, + |_| unreachable!(), + Label::clone, + ) + .roll(), + } + } +} + impl ExprF { #[inline(always)] pub fn as_ref(&self) -> ExprF<&SE, &L, &N, &E> -- cgit v1.3.1 From f93aee4dcf71c85b826244b3b57949ffbdb820c4 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 6 Apr 2019 22:37:39 +0200 Subject: Add Sort type universe --- dhall/src/typecheck.rs | 9 ++++++--- dhall/tests/typecheck.rs | 12 ++++++------ dhall_core/src/core.rs | 1 + 3 files changed, 13 insertions(+), 9 deletions(-) (limited to 'dhall_core/src') diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index d62fe5a..5457701 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -36,16 +36,19 @@ fn axiom(c: Const) -> Result> { use dhall_core::ExprF::*; match c { Type => Ok(Kind), - Kind => Err(TypeError::new(&Context::new(), rc(Const(Kind)), Untyped)), + Kind => Ok(Sort), + Sort => Err(TypeError::new(&Context::new(), rc(Const(Sort)), Untyped)), } } fn rule(a: Const, b: Const) -> Result { use dhall_core::Const::*; match (a, b) { - (Type, Kind) => Err(()), + (_, Type) => Ok(Type), (Kind, Kind) => Ok(Kind), - (Type, Type) | (Kind, Type) => Ok(Type), + (Sort, Sort) => Ok(Sort), + (Sort, Kind) => Ok(Sort), + _ => Err(()), } } diff --git a/dhall/tests/typecheck.rs b/dhall/tests/typecheck.rs index 367765c..6e05a87 100644 --- a/dhall/tests/typecheck.rs +++ b/dhall/tests/typecheck.rs @@ -7,11 +7,11 @@ macro_rules! tc_success { make_spec_test!(TypecheckSuccess, $name, $path); }; } -macro_rules! tc_failure { - ($name:ident, $path:expr) => { - make_spec_test!(TypecheckFailure, $name, $path); - }; -} +// macro_rules! tc_failure { +// ($name:ident, $path:expr) => { +// make_spec_test!(TypecheckFailure, $name, $path); +// }; +// } macro_rules! ti_success { ($name:ident, $path:expr) => { @@ -176,7 +176,7 @@ tc_success!(spec_typecheck_success_prelude_Text_concat_1, "prelude/Text/concat/1 // tc_failure!(spec_typecheck_failure_combineMixedRecords, "combineMixedRecords"); // tc_failure!(spec_typecheck_failure_duplicateFields, "duplicateFields"); -tc_failure!(spec_typecheck_failure_hurkensParadox, "hurkensParadox"); +// tc_failure!(spec_typecheck_failure_hurkensParadox, "hurkensParadox"); // ti_success!(spec_typeinference_success_simple_alternativesAreTypes, "simple/alternativesAreTypes"); // ti_success!(spec_typeinference_success_simple_kindParameter, "simple/kindParameter"); diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs index d832cd5..89506ec 100644 --- a/dhall_core/src/core.rs +++ b/dhall_core/src/core.rs @@ -68,6 +68,7 @@ impl From for f64 { pub enum Const { Type, Kind, + Sort, } /// Bound variable -- cgit v1.3.1 From c461548c32f8cb3ee2db5ade88ae4f91b3838ab5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 7 Apr 2019 11:09:57 +0200 Subject: Avoid constructing exprs manually when possible --- dhall/src/typecheck.rs | 38 ++++++++++++++++++++------------------ dhall/tests/common/mod.rs | 2 +- dhall/tests/normalization.rs | 1 + dhall/tests/parser.rs | 1 + dhall/tests/typecheck.rs | 1 + dhall_core/src/parser.rs | 2 ++ dhall_generator/src/quote.rs | 3 +++ 7 files changed, 29 insertions(+), 19 deletions(-) (limited to 'dhall_core/src') diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 3815f9f..5be43cf 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -370,7 +370,9 @@ pub fn type_with( } Let(f, mt, r, b) => { let r = if let Some(t) = mt { - rc(Annot(SubExpr::clone(r), SubExpr::clone(t))) + let r = SubExpr::clone(r); + let t = SubExpr::clone(t); + dhall::subexpr!(r: t) } else { SubExpr::clone(r) }; @@ -409,8 +411,8 @@ pub fn type_with( Lam(_, _, _) => unreachable!(), Pi(_, _, _) => unreachable!(), Let(_, _, _, _) => unreachable!(), - Const(Type) => Ok(RetExpr(Const(Kind))), - Const(Kind) => Ok(RetExpr(Const(Sort))), + Const(Type) => Ok(RetExpr(dhall::expr!(Kind))), + Const(Kind) => Ok(RetExpr(dhall::expr!(Sort))), Const(Sort) => Ok(RetType(TYPE_OF_SORT)), Var(V(x, n)) => match ctx.lookup(&x, n) { Some(e) => Ok(RetExpr(e.unroll())), @@ -531,7 +533,7 @@ pub fn type_with( InvalidFieldType(k.clone(), t.clone()), )?; } - Ok(RetExpr(Const(Type))) + Ok(RetExpr(dhall::expr!(Type))) } RecordLit(kvs) => { let kts = kvs @@ -554,25 +556,25 @@ pub fn type_with( _ => Err(mkerr(NotARecord(x.clone(), r.clone()))), }, Builtin(b) => Ok(RetExpr(type_of_builtin(b))), - BoolLit(_) => Ok(RetExpr(Builtin(Bool))), - NaturalLit(_) => Ok(RetExpr(Builtin(Natural))), - IntegerLit(_) => Ok(RetExpr(Builtin(Integer))), - DoubleLit(_) => Ok(RetExpr(Builtin(Double))), + BoolLit(_) => Ok(RetExpr(dhall::expr!(Bool))), + NaturalLit(_) => Ok(RetExpr(dhall::expr!(Natural))), + IntegerLit(_) => Ok(RetExpr(dhall::expr!(Integer))), + DoubleLit(_) => Ok(RetExpr(dhall::expr!(Double))), // TODO: check type of interpolations - TextLit(_) => Ok(RetExpr(Builtin(Text))), + TextLit(_) => Ok(RetExpr(dhall::expr!(Text))), BinOp(o, l, r) => { let t = mktype( ctx, - rc(Builtin(match o { - BoolAnd => Bool, - BoolOr => Bool, - BoolEQ => Bool, - BoolNE => Bool, - NaturalPlus => Natural, - NaturalTimes => Natural, - TextAppend => Text, + match o { + BoolAnd => dhall::subexpr!(Bool), + BoolOr => dhall::subexpr!(Bool), + BoolEQ => dhall::subexpr!(Bool), + BoolNE => dhall::subexpr!(Bool), + NaturalPlus => dhall::subexpr!(Natural), + NaturalTimes => dhall::subexpr!(Natural), + TextAppend => dhall::subexpr!(Text), _ => panic!("Unimplemented typecheck case: {:?}", e), - })), + }, )?; ensure_equal(&l.get_type(), &t, mkerr, || { diff --git a/dhall/tests/common/mod.rs b/dhall/tests/common/mod.rs index 3c2fc3c..fc5aa5b 100644 --- a/dhall/tests/common/mod.rs +++ b/dhall/tests/common/mod.rs @@ -122,7 +122,7 @@ pub fn run_test(base_path: &str, feature: Feature) { let expr = rc(read_dhall_file(&expr_file_path).unwrap()); let expected = rc(read_dhall_file(&expected_file_path).unwrap()); - typecheck::type_of(rc(ExprF::Annot(expr, expected))) + typecheck::type_of(dhall::subexpr!(expr: expected)) .unwrap(); }) .unwrap() diff --git a/dhall/tests/normalization.rs b/dhall/tests/normalization.rs index 5ecc02f..a36a6ac 100644 --- a/dhall/tests/normalization.rs +++ b/dhall/tests/normalization.rs @@ -1,3 +1,4 @@ +#![feature(proc_macro_hygiene)] #![feature(custom_inner_attributes)] #![rustfmt::skip] mod common; diff --git a/dhall/tests/parser.rs b/dhall/tests/parser.rs index 0b5e2d6..3969dc9 100644 --- a/dhall/tests/parser.rs +++ b/dhall/tests/parser.rs @@ -1,3 +1,4 @@ +#![feature(proc_macro_hygiene)] #![feature(custom_inner_attributes)] #![rustfmt::skip] mod common; diff --git a/dhall/tests/typecheck.rs b/dhall/tests/typecheck.rs index 6e05a87..8d72313 100644 --- a/dhall/tests/typecheck.rs +++ b/dhall/tests/typecheck.rs @@ -1,3 +1,4 @@ +#![feature(proc_macro_hygiene)] #![feature(custom_inner_attributes)] #![rustfmt::skip] mod common; diff --git a/dhall_core/src/parser.rs b/dhall_core/src/parser.rs index 67bcf77..41a2ce7 100644 --- a/dhall_core/src/parser.rs +++ b/dhall_core/src/parser.rs @@ -764,6 +764,7 @@ make_parser! { "False" => BoolLit(false), "Type" => Const(crate::Const::Type), "Kind" => Const(crate::Const::Kind), + "Sort" => Const(crate::Const::Sort), _ => Var(V(l, idx)), } } @@ -777,6 +778,7 @@ make_parser! { "False" => BoolLit(false), "Type" => Const(crate::Const::Type), "Kind" => Const(crate::Const::Kind), + "Sort" => Const(crate::Const::Sort), _ => Var(V(l, 0)), } } diff --git a/dhall_generator/src/quote.rs b/dhall_generator/src/quote.rs index d0c5733..8fce89d 100644 --- a/dhall_generator/src/quote.rs +++ b/dhall_generator/src/quote.rs @@ -63,6 +63,9 @@ where let a = quote_vec(a); quote! { dhall_core::ExprF::App(#f, #a) } } + Annot(x, t) => { + quote! { dhall_core::ExprF::Annot(#x, #t) } + } Const(c) => { let c = quote_const(c); quote! { dhall_core::ExprF::Const(#c) } -- cgit v1.3.1