From 1b1c34b90bb4bf3859b05b1da6db2dcb374996bb Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 4 May 2019 14:58:18 +0200 Subject: Move `Note`s into the spine of the AST --- dhall/src/normalize.rs | 12 +-- dhall/src/typecheck.rs | 2 +- dhall_proc_macros/src/quote.rs | 4 +- dhall_syntax/src/core.rs | 69 +++++------- dhall_syntax/src/parser.rs | 2 +- dhall_syntax/src/printer.rs | 10 +- dhall_syntax/src/visitor.rs | 234 +++++++++-------------------------------- 7 files changed, 86 insertions(+), 247 deletions(-) diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index 4636859..4d87225 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -163,7 +163,7 @@ pub(crate) enum Value { UnionLit(Label, Thunk, BTreeMap>), TextLit(Vec>), /// Invariant: This must not contain a value captured by one of the variants above. - PartialExpr(ExprF), + PartialExpr(ExprF), } impl Value { @@ -497,7 +497,6 @@ impl Value { |v| v.shift(delta, var), |x, v| v.shift(delta, &var.shift(1, &x.into())), X::clone, - X::clone, Label::clone, )) } @@ -607,7 +606,6 @@ impl Value { ) }, X::clone, - X::clone, Label::clone, )) } @@ -1125,11 +1123,10 @@ fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> Value { } // Thunk subexpressions - let expr: ExprF = + let expr: ExprF = expr.as_ref().map_ref_with_special_handling_of_binders( |e| Thunk::new(ctx.clone(), e.clone()), |x, e| Thunk::new(ctx.skip(x), e.clone()), - X::clone, |_| unreachable!(), Label::clone, ); @@ -1137,7 +1134,7 @@ fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> Value { normalize_one_layer(expr) } -fn normalize_one_layer(expr: ExprF) -> Value { +fn normalize_one_layer(expr: ExprF) -> Value { use Value::{ BoolLit, EmptyListLit, EmptyOptionalLit, Lam, NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType, TextLit, UnionConstructor, @@ -1149,7 +1146,7 @@ fn normalize_one_layer(expr: ExprF) -> Value { RetValue(Value), RetThunk(Thunk), RetThunkRef(&'a Thunk), - RetExpr(ExprF), + RetExpr(ExprF), } use Ret::{RetExpr, RetThunk, RetThunkRef, RetValue}; @@ -1157,7 +1154,6 @@ fn normalize_one_layer(expr: ExprF) -> Value { ExprF::Embed(_) => unreachable!(), ExprF::Var(_) => unreachable!(), ExprF::Annot(x, _) => RetThunk(x), - ExprF::Note(_, e) => RetThunk(e), ExprF::Lam(x, t, e) => RetValue(Lam(x, t, e)), ExprF::Pi(x, t, e) => { RetValue(Pi(x, TypeThunk::from_thunk(t), TypeThunk::from_thunk(e))) diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 74de59b..ce4ca96 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -719,7 +719,7 @@ fn type_with( /// layer. fn type_last_layer( ctx: &TypecheckContext, - e: ExprF, + e: ExprF, ) -> Result { use dhall_syntax::BinOp::*; use dhall_syntax::Builtin::*; diff --git a/dhall_proc_macros/src/quote.rs b/dhall_proc_macros/src/quote.rs index c2323fa..e11bbaa 100644 --- a/dhall_proc_macros/src/quote.rs +++ b/dhall_proc_macros/src/quote.rs @@ -27,7 +27,7 @@ pub fn subexpr(input: proc_macro::TokenStream) -> proc_macro::TokenStream { // Returns an expression of type ExprF, where T is the // type of the subexpressions after interpolation. -pub fn quote_exprf(expr: ExprF) -> TokenStream +pub fn quote_exprf(expr: ExprF) -> TokenStream where TS: quote::ToTokens + std::fmt::Debug, { @@ -103,7 +103,6 @@ fn quote_subexpr( |e| quote_subexpr(e, ctx), |l, e| quote_subexpr(e, &ctx.insert(l.clone(), ())), |_| unreachable!(), - |_| unreachable!(), Label::clone, ) { Var(V(ref s, n)) => { @@ -138,7 +137,6 @@ fn quote_expr(expr: &Expr, ctx: &Context) -> TokenStream { |e| quote_subexpr(e, ctx), |l, e| quote_subexpr(e, &ctx.insert(l.clone(), ())), |_| unreachable!(), - |_| unreachable!(), Label::clone, ) { Var(V(ref s, n)) => { diff --git a/dhall_syntax/src/core.rs b/dhall_syntax/src/core.rs index 3db07dd..a81f96c 100644 --- a/dhall_syntax/src/core.rs +++ b/dhall_syntax/src/core.rs @@ -141,17 +141,25 @@ pub type ParsedExpr = SubExpr; pub type ResolvedExpr = SubExpr; pub type DhallExpr = ResolvedExpr; -#[derive(Debug, PartialEq, Eq)] -pub struct SubExpr(pub Rc>); +#[derive(Debug)] +pub struct SubExpr(Rc>, Option); -pub type Expr = ExprF, Label, Note, Embed>; +impl std::cmp::PartialEq for SubExpr { + fn eq(&self, other: &Self) -> bool { + self.0 == other.0 + } +} + +impl std::cmp::Eq for SubExpr {} + +pub type Expr = ExprF, Label, Embed>; /// Syntax tree for expressions // Having the recursion out of the enum definition enables writing // much more generic code and improves pattern-matching behind // smart pointers. #[derive(Debug, Clone, PartialEq, Eq)] -pub enum ExprF { +pub enum ExprF { Const(Const), /// `x` /// `x@n` @@ -208,28 +216,25 @@ pub enum ExprF { Field(SubExpr, Label), /// `e.{ x, y, z }` Projection(SubExpr, Vec