diff options
Diffstat (limited to '')
-rw-r--r-- | dhall/src/binary.rs | 22 | ||||
-rw-r--r-- | dhall/src/expr.rs | 32 | ||||
-rw-r--r-- | dhall/src/normalize.rs | 48 | ||||
-rw-r--r-- | dhall/src/serde.rs | 2 | ||||
-rw-r--r-- | dhall/src/traits/static_type.rs | 14 | ||||
-rw-r--r-- | dhall/src/typecheck.rs | 65 | ||||
-rw-r--r-- | dhall/tests/traits.rs | 4 | ||||
-rw-r--r-- | dhall_proc_macros/src/quote.rs | 62 | ||||
-rw-r--r-- | dhall_syntax/src/core.rs | 207 | ||||
-rw-r--r-- | dhall_syntax/src/parser.rs | 24 | ||||
-rw-r--r-- | dhall_syntax/src/printer.rs | 44 | ||||
-rw-r--r-- | dhall_syntax/src/visitor.rs | 130 |
12 files changed, 303 insertions, 351 deletions
diff --git a/dhall/src/binary.rs b/dhall/src/binary.rs index 0d9f28a..9c31d4c 100644 --- a/dhall/src/binary.rs +++ b/dhall/src/binary.rs @@ -2,7 +2,7 @@ use dhall_syntax::*; use itertools::*; use serde_cbor::value::value as cbor; -type ParsedExpr = SubExpr<Label, X, Import>; +type ParsedExpr = SubExpr<X, Import>; #[derive(Debug)] pub enum DecodeError { @@ -18,32 +18,28 @@ pub fn decode(data: &[u8]) -> Result<ParsedExpr, DecodeError> { } fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> { - use cbor::Value::{Array, Bool, Null, Object, String, F64, I64, U64}; + use cbor::Value::*; use dhall_syntax::{BinOp, Builtin, Const}; - use ExprF::{ - Annot, App, BoolIf, BoolLit, DoubleLit, Embed, EmptyListLit, Field, - IntegerLit, Lam, Let, Merge, NEListLit, NaturalLit, OldOptionalLit, Pi, - RecordLit, RecordType, SomeLit, TextLit, UnionLit, UnionType, - }; + use ExprF::*; Ok(rc(match data { String(s) => match Builtin::parse(s) { Some(b) => ExprF::Builtin(b), None => match s.as_str() { "True" => BoolLit(true), "False" => BoolLit(false), - "Type" => ExprF::Const(Const::Type), - "Kind" => ExprF::Const(Const::Kind), - "Sort" => ExprF::Const(Const::Sort), + "Type" => Const(Const::Type), + "Kind" => Const(Const::Kind), + "Sort" => Const(Const::Sort), _ => Err(DecodeError::WrongFormatError("builtin".to_owned()))?, }, }, - U64(n) => ExprF::Var(Var(Label::from("_"), *n as usize)), + U64(n) => Var(V(Label::from("_"), *n as usize)), F64(x) => DoubleLit((*x).into()), Bool(b) => BoolLit(*b), Array(vec) => match vec.as_slice() { [String(l), U64(n)] => { let l = Label::from(l.as_str()); - ExprF::Var(Var(l, *n as usize)) + Var(V(l, *n as usize)) } [U64(0), f, args..] => { let mut f = cbor_value_to_dhall(&f)?; @@ -96,7 +92,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> { Err(DecodeError::WrongFormatError("binop".to_owned()))? } }; - ExprF::BinOp(op, x, y) + BinOp(op, x, y) } [U64(4), t] => { let t = cbor_value_to_dhall(&t)?; diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs index efc3928..5bde68f 100644 --- a/dhall/src/expr.rs +++ b/dhall/src/expr.rs @@ -23,17 +23,15 @@ macro_rules! derive_other_traits { }; } -type OutputSubExpr = SubExpr<Label, X, X>; - #[derive(Debug, Clone)] pub(crate) struct Parsed( - pub(crate) SubExpr<Label, Span, Import>, + pub(crate) SubExpr<Span, Import>, pub(crate) ImportRoot, ); derive_other_traits!(Parsed); #[derive(Debug, Clone)] -pub(crate) struct Resolved(pub(crate) SubExpr<Label, Span, Normalized>); +pub(crate) struct Resolved(pub(crate) SubExpr<Span, Normalized>); derive_other_traits!(Resolved); pub(crate) use self::typed::TypedInternal; @@ -59,12 +57,12 @@ impl std::fmt::Display for Normalized { } mod typed { - use super::{OutputSubExpr, Type, Typed}; + use super::{Type, Typed}; use crate::normalize::{Thunk, Value}; use crate::typecheck::{ TypeError, TypeInternal, TypeMessage, TypecheckContext, }; - use dhall_syntax::{Const, Label, Var}; + use dhall_syntax::{Const, Label, SubExpr, V, X}; use std::borrow::Cow; #[derive(Debug, Clone)] @@ -92,7 +90,7 @@ mod typed { } } - pub(crate) fn to_expr(&self) -> OutputSubExpr { + pub(crate) fn to_expr(&self) -> SubExpr<X, X> { self.to_value().normalize_to_expr() } @@ -131,7 +129,7 @@ mod typed { } } - pub(crate) fn shift(&self, delta: isize, var: &Var<Label>) -> Self { + pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self { match self { TypedInternal::Value(th, t) => TypedInternal::Value( th.shift(delta, var), @@ -141,11 +139,7 @@ mod typed { } } - pub(crate) fn subst_shift( - &self, - var: &Var<Label>, - val: &Typed, - ) -> Self { + pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self { match self { TypedInternal::Value(th, t) => TypedInternal::Value( th.subst_shift(var, val), @@ -164,7 +158,7 @@ mod typed { /// /// For a more general notion of "type", see [Type]. #[derive(Debug, Clone)] -pub struct SimpleType(pub(crate) OutputSubExpr); +pub struct SimpleType(pub(crate) SubExpr<X, X>); derive_other_traits!(SimpleType); pub(crate) use crate::typecheck::TypeInternal; @@ -184,16 +178,16 @@ impl std::fmt::Display for Type { // Exposed for the macros #[doc(hidden)] -impl From<SimpleType> for OutputSubExpr { - fn from(x: SimpleType) -> OutputSubExpr { +impl From<SimpleType> for SubExpr<X, X> { + fn from(x: SimpleType) -> SubExpr<X, X> { x.0 } } // Exposed for the macros #[doc(hidden)] -impl From<OutputSubExpr> for SimpleType { - fn from(x: OutputSubExpr) -> SimpleType { +impl From<SubExpr<X, X>> for SimpleType { + fn from(x: SubExpr<X, X>) -> SimpleType { SimpleType(x) } } @@ -210,7 +204,7 @@ impl Normalized { pub(crate) fn from_thunk_and_type(th: Thunk, t: Type) -> Self { Normalized(TypedInternal::from_thunk_and_type(th, t)) } - pub(crate) fn to_expr(&self) -> OutputSubExpr { + pub(crate) fn to_expr(&self) -> SubExpr<X, X> { self.0.to_expr() } pub(crate) fn to_value(&self) -> Value { diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index 3de12ee..8ae746d 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -6,13 +6,13 @@ use dhall_proc_macros as dhall; use dhall_syntax::context::Context; use dhall_syntax::{ rc, BinOp, Builtin, Const, ExprF, Integer, InterpolatedText, - InterpolatedTextContents, Label, Natural, Span, SubExpr, Var, X, + InterpolatedTextContents, Label, Natural, Span, SubExpr, V, X, }; use crate::expr::{Normalized, Type, Typed, TypedInternal}; -type InputSubExpr = SubExpr<Label, Span, Normalized>; -type OutputSubExpr = SubExpr<Label, X, X>; +type InputSubExpr = SubExpr<Span, Normalized>; +type OutputSubExpr = SubExpr<X, X>; impl Typed { /// Reduce an expression to its normal form, performing beta reduction @@ -38,11 +38,11 @@ impl Typed { Normalized(internal) } - pub(crate) fn shift(&self, delta: isize, var: &Var<Label>) -> Self { + pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self { Typed(self.0.shift(delta, var)) } - pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self { + pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self { Typed(self.0.subst_shift(var, val)) } @@ -58,11 +58,11 @@ impl Typed { #[derive(Debug, Clone)] enum EnvItem { Thunk(Thunk), - Skip(Var<Label>), + Skip(V<Label>), } impl EnvItem { - fn shift(&self, delta: isize, var: &Var<Label>) -> Self { + fn shift(&self, delta: isize, var: &V<Label>) -> Self { use EnvItem::*; match self { Thunk(e) => Thunk(e.shift(delta, var)), @@ -70,7 +70,7 @@ impl EnvItem { } } - pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self { + pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self { match self { EnvItem::Thunk(e) => EnvItem::Thunk(e.subst_shift(var, val)), EnvItem::Skip(v) if v == var => EnvItem::Thunk(val.to_thunk()), @@ -93,8 +93,8 @@ impl NormalizationContext { .insert(x.clone(), EnvItem::Skip(x.into())), )) } - fn lookup(&self, var: &Var<Label>) -> Value { - let Var(x, n) = var; + fn lookup(&self, var: &V<Label>) -> Value { + let V(x, n) = var; match self.0.lookup(x, *n) { Some(EnvItem::Thunk(t)) => t.to_value(), Some(EnvItem::Skip(newvar)) => Value::Var(newvar.clone()), @@ -118,11 +118,11 @@ impl NormalizationContext { NormalizationContext(Rc::new(ctx)) } - fn shift(&self, delta: isize, var: &Var<Label>) -> Self { + fn shift(&self, delta: isize, var: &V<Label>) -> Self { NormalizationContext(Rc::new(self.0.map(|_, e| e.shift(delta, var)))) } - fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self { + fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self { NormalizationContext(Rc::new( self.0.map(|_, e| e.subst_shift(var, val)), )) @@ -144,7 +144,7 @@ pub(crate) enum Value { NaturalSuccClosure, Pi(Label, TypeThunk, TypeThunk), - Var(Var<Label>), + Var(V<Label>), Const(Const), BoolLit(bool), NaturalLit(Natural), @@ -403,7 +403,7 @@ impl Value { Value::AppliedBuiltin(b, vec![]) } - fn shift(&self, delta: isize, var: &Var<Label>) -> Self { + fn shift(&self, delta: isize, var: &V<Label>) -> Self { match self { Value::Lam(x, t, e) => Value::Lam( x.clone(), @@ -500,7 +500,7 @@ impl Value { } } - pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self { + pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self { match self { Value::Lam(x, t, e) => Value::Lam( x.clone(), @@ -616,7 +616,7 @@ mod thunk { OutputSubExpr, Value, }; use crate::expr::Typed; - use dhall_syntax::{Label, Var}; + use dhall_syntax::{Label, V}; use std::cell::{Ref, RefCell}; use std::rc::Rc; @@ -693,7 +693,7 @@ mod thunk { } } - fn shift(&self, delta: isize, var: &Var<Label>) -> Self { + fn shift(&self, delta: isize, var: &V<Label>) -> Self { match self { ThunkInternal::Unnormalized(ctx, e) => { ThunkInternal::Unnormalized( @@ -707,7 +707,7 @@ mod thunk { } } - fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self { + fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self { match self { ThunkInternal::Unnormalized(ctx, e) => { ThunkInternal::Unnormalized( @@ -805,15 +805,11 @@ mod thunk { apply_any(self.clone(), th) } - pub(crate) fn shift(&self, delta: isize, var: &Var<Label>) -> Self { + pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self { self.0.borrow().shift(delta, var).into_thunk() } - pub(crate) fn subst_shift( - &self, - var: &Var<Label>, - val: &Typed, - ) -> Self { + pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self { self.0.borrow().subst_shift(var, val).into_thunk() } } @@ -859,14 +855,14 @@ impl TypeThunk { self.normalize_nf().normalize_to_expr() } - fn shift(&self, delta: isize, var: &Var<Label>) -> Self { + fn shift(&self, delta: isize, var: &V<Label>) -> Self { match self { TypeThunk::Thunk(th) => TypeThunk::Thunk(th.shift(delta, var)), TypeThunk::Type(t) => TypeThunk::Type(t.shift(delta, var)), } } - pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self { + pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self { match self { TypeThunk::Thunk(th) => TypeThunk::Thunk(th.subst_shift(var, val)), TypeThunk::Type(t) => TypeThunk::Type(t.subst_shift(var, val)), diff --git a/dhall/src/serde.rs b/dhall/src/serde.rs index bc76c49..96bc765 100644 --- a/dhall/src/serde.rs +++ b/dhall/src/serde.rs @@ -11,7 +11,7 @@ impl<'a, T: serde::Deserialize<'a>> Deserialize<'a> for T { } } -struct Deserializer<'a>(Cow<'a, SubExpr<Label, X, X>>); +struct Deserializer<'a>(Cow<'a, SubExpr<X, X>>); impl serde::de::Error for Error { fn custom<T>(msg: T) -> Self diff --git a/dhall/src/traits/static_type.rs b/dhall/src/traits/static_type.rs index c3f323b..f90b8df 100644 --- a/dhall/src/traits/static_type.rs +++ b/dhall/src/traits/static_type.rs @@ -32,7 +32,7 @@ pub trait SimpleStaticType { fn get_simple_static_type() -> SimpleType; } -fn mktype(x: SubExpr<Label, X, X>) -> SimpleType { +fn mktype(x: SubExpr<X, X>) -> SimpleType { x.into() } @@ -106,22 +106,22 @@ impl SimpleStaticType for String { impl<A: SimpleStaticType, B: SimpleStaticType> SimpleStaticType for (A, B) { fn get_simple_static_type() -> SimpleType { - let ta: SubExpr<_, _, _> = A::get_simple_static_type().into(); - let tb: SubExpr<_, _, _> = B::get_simple_static_type().into(); + let ta: SubExpr<_, _> = A::get_simple_static_type().into(); + let tb: SubExpr<_, _> = B::get_simple_static_type().into(); mktype(dhall::subexpr!({ _1: ta, _2: tb })) } } impl<T: SimpleStaticType> SimpleStaticType for Option<T> { fn get_simple_static_type() -> SimpleType { - let t: SubExpr<_, _, _> = T::get_simple_static_type().into(); + let t: SubExpr<_, _> = T::get_simple_static_type().into(); mktype(dhall::subexpr!(Optional t)) } } impl<T: SimpleStaticType> SimpleStaticType for Vec<T> { fn get_simple_static_type() -> SimpleType { - let t: SubExpr<_, _, _> = T::get_simple_static_type().into(); + let t: SubExpr<_, _> = T::get_simple_static_type().into(); mktype(dhall::subexpr!(List t)) } } @@ -142,8 +142,8 @@ impl<T: SimpleStaticType, E: SimpleStaticType> SimpleStaticType for std::result::Result<T, E> { fn get_simple_static_type() -> SimpleType { - let tt: SubExpr<_, _, _> = T::get_simple_static_type().into(); - let te: SubExpr<_, _, _> = E::get_simple_static_type().into(); + let tt: SubExpr<_, _> = T::get_simple_static_type().into(); + let te: SubExpr<_, _> = E::get_simple_static_type().into(); mktype(dhall::subexpr!(< Ok: tt | Err: te>)) } } diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 63041bb..8b7f011 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -14,16 +14,13 @@ use dhall_syntax::*; use self::TypeMessage::*; -type InputSubExpr = SubExpr<Label, Span, Normalized>; -type OutputSubExpr = SubExpr<Label, X, X>; - impl Resolved { pub fn typecheck(self) -> Result<Typed, TypeError> { type_of(self.0) } pub fn typecheck_with(self, ty: &Type) -> Result<Typed, TypeError> { - let expr = self.0; - let ty = ty.to_expr().embed_absurd().note_absurd(); + let expr: SubExpr<_, _> = self.0; + let ty: SubExpr<_, _> = ty.to_expr().embed_absurd().note_absurd(); type_of(expr.rewrap(ExprF::Annot(expr.clone(), ty))) } /// Pretends this expression has been typechecked. Use with care. @@ -46,7 +43,7 @@ impl Typed { } impl Normalized { - fn shift(&self, delta: isize, var: &Var<Label>) -> Self { + fn shift(&self, delta: isize, var: &V<Label>) -> Self { Normalized(self.0.shift(delta, var)) } pub(crate) fn to_type(self) -> Type { @@ -58,7 +55,7 @@ impl Type { pub(crate) fn to_normalized(&self) -> Normalized { self.0.to_normalized() } - pub(crate) fn to_expr(&self) -> OutputSubExpr { + pub(crate) fn to_expr(&self) -> SubExpr<X, X> { self.0.to_expr() } pub(crate) fn to_value(&self) -> Value { @@ -76,10 +73,10 @@ impl Type { fn internal_whnf(&self) -> Option<Value> { self.0.whnf() } - pub(crate) fn shift(&self, delta: isize, var: &Var<Label>) -> Self { + pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self { Type(self.0.shift(delta, var)) } - pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self { + pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self { Type(self.0.subst_shift(var, val)) } @@ -127,7 +124,7 @@ impl TypeInternal { fn to_normalized(&self) -> Normalized { self.to_typed().normalize() } - fn to_expr(&self) -> OutputSubExpr { + fn to_expr(&self) -> SubExpr<X, X> { self.to_normalized().to_expr() } fn to_value(&self) -> Value { @@ -151,14 +148,14 @@ impl TypeInternal { _ => None, } } - fn shift(&self, delta: isize, var: &Var<Label>) -> Self { + fn shift(&self, delta: isize, var: &V<Label>) -> Self { use TypeInternal::*; match self { Typed(e) => Typed(Box::new(e.shift(delta, var))), Const(c) => Const(*c), } } - fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self { + fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self { use TypeInternal::*; match self { Typed(e) => Typed(Box::new(e.subst_shift(var, val))), @@ -176,12 +173,12 @@ impl PartialEq for TypeInternal { #[derive(Debug, Clone)] pub(crate) enum EnvItem { - Type(Var<Label>, Type), + Type(V<Label>, Type), Value(Normalized), } impl EnvItem { - fn shift(&self, delta: isize, var: &Var<Label>) -> Self { + fn shift(&self, delta: isize, var: &V<Label>) -> Self { use EnvItem::*; match self { Type(v, e) => Type(v.shift(delta, var), e.shift(delta, var)), @@ -208,8 +205,8 @@ impl TypecheckContext { pub(crate) fn insert_value(&self, x: &Label, t: Normalized) -> Self { TypecheckContext(self.0.insert(x.clone(), EnvItem::Value(t))) } - pub(crate) fn lookup(&self, var: &Var<Label>) -> Option<Cow<'_, Type>> { - let Var(x, n) = var; + pub(crate) fn lookup(&self, var: &V<Label>) -> Option<Cow<'_, Type>> { + let V(x, n) = var; match self.0.lookup(x, *n) { Some(EnvItem::Type(_, t)) => Some(Cow::Borrowed(&t)), Some(EnvItem::Value(t)) => Some(t.get_type()?), @@ -241,12 +238,8 @@ fn function_check(a: Const, b: Const) -> Result<Const, ()> { } } -fn match_vars( - vl: &Var<Label>, - vr: &Var<Label>, - ctx: &[(&Label, &Label)], -) -> bool { - let (Var(xL, mut nL), Var(xR, mut nR)) = (vl, vr); +fn match_vars(vl: &V<Label>, vr: &V<Label>, ctx: &[(&Label, &Label)]) -> bool { + let (V(xL, mut nL), V(xR, mut nR)) = (vl, vr); for &(xL2, xR2) in ctx { match (nL, nR) { (0, 0) if xL == xL2 && xR == xR2 => return true, @@ -272,8 +265,8 @@ where use dhall_syntax::ExprF::*; fn go<'a, S, T>( ctx: &mut Vec<(&'a Label, &'a Label)>, - el: &'a SubExpr<Label, S, X>, - er: &'a SubExpr<Label, T, X>, + el: &'a SubExpr<S, X>, + er: &'a SubExpr<T, X>, ) -> bool where S: ::std::fmt::Debug, @@ -357,9 +350,9 @@ fn type_of_const(c: Const) -> Result<Type, TypeError> { } } -fn type_of_builtin(b: Builtin) -> InputSubExpr { +fn type_of_builtin<E>(b: Builtin) -> Expr<X, E> { use dhall_syntax::Builtin::*; - rc(match b { + match b { Bool | Natural | Integer | Double | Text => dhall::expr!(Type), List | Optional => dhall::expr!( Type -> Type @@ -439,8 +432,7 @@ fn type_of_builtin(b: Builtin) -> InputSubExpr { OptionalNone => dhall::expr!( forall (A: Type) -> Optional A ), - }) - .note_absurd() + } } macro_rules! ensure_equal { @@ -627,7 +619,10 @@ impl TypeIntermediate { /// Takes an expression that is meant to contain a Type /// and turn it into a type, typechecking it along the way. -fn mktype(ctx: &TypecheckContext, e: InputSubExpr) -> Result<Type, TypeError> { +fn mktype( + ctx: &TypecheckContext, + e: SubExpr<Span, Normalized>, +) -> Result<Type, TypeError> { Ok(type_with(ctx, e)?.to_type()) } @@ -650,7 +645,7 @@ enum Ret { /// succeeded, or an error if type-checking failed fn type_with( ctx: &TypecheckContext, - e: InputSubExpr, + e: SubExpr<Span, Normalized>, ) -> Result<Typed, TypeError> { use dhall_syntax::ExprF::{ Annot, App, Embed, Lam, Let, OldOptionalLit, Pi, SomeLit, @@ -761,7 +756,7 @@ fn type_last_layer( mkerr(TypeMismatch(f.clone(), tx.clone().to_normalized(), a)) }); - Ok(RetType(tb.subst_shift(&x.into(), &a))) + Ok(RetType(tb.subst_shift(&V(x.clone(), 0), &a))) } Annot(x, t) => { let t = t.to_type(); @@ -942,7 +937,9 @@ fn type_last_layer( } } Const(c) => Ok(RetTyped(const_to_typed(c))), - Builtin(b) => Ok(RetType(mktype(ctx, type_of_builtin(b))?)), + Builtin(b) => { + Ok(RetType(mktype(ctx, rc(type_of_builtin(b)).note_absurd())?)) + } BoolLit(_) => Ok(RetType(builtin_to_type(Bool)?)), NaturalLit(_) => Ok(RetType(builtin_to_type(Natural)?)), IntegerLit(_) => Ok(RetType(builtin_to_type(Integer)?)), @@ -1001,7 +998,7 @@ fn type_last_layer( /// `typeOf` is the same as `type_with` with an empty context, meaning that the /// expression must be closed (i.e. no free variables), otherwise type-checking /// will fail. -fn type_of(e: InputSubExpr) -> Result<Typed, TypeError> { +fn type_of(e: SubExpr<Span, Normalized>) -> Result<Typed, TypeError> { let ctx = TypecheckContext::new(); let e = type_with(&ctx, e)?; // Ensure `e` has a type (i.e. `e` is not `Sort`) @@ -1012,7 +1009,7 @@ fn type_of(e: InputSubExpr) -> Result<Typed, TypeError> { /// The specific type error #[derive(Debug)] pub(crate) enum TypeMessage { - UnboundVariable(Var<Label>), + UnboundVariable(V<Label>), InvalidInputType(Normalized), InvalidOutputType(Normalized), NotAFunction(Typed), diff --git a/dhall/tests/traits.rs b/dhall/tests/traits.rs index cf68d7d..6604c06 100644 --- a/dhall/tests/traits.rs +++ b/dhall/tests/traits.rs @@ -1,11 +1,11 @@ #![feature(proc_macro_hygiene)] use dhall::de::SimpleStaticType; use dhall_proc_macros; -use dhall_syntax::{Label, SubExpr, X}; +use dhall_syntax::{SubExpr, X}; #[test] fn test_static_type() { - fn mktype(x: SubExpr<Label, X, X>) -> dhall::expr::SimpleType { + fn mktype(x: SubExpr<X, X>) -> dhall::expr::SimpleType { x.into() } diff --git a/dhall_proc_macros/src/quote.rs b/dhall_proc_macros/src/quote.rs index d0deaad..eaf4946 100644 --- a/dhall_proc_macros/src/quote.rs +++ b/dhall_proc_macros/src/quote.rs @@ -7,7 +7,7 @@ use std::collections::BTreeMap; pub fn expr(input: proc_macro::TokenStream) -> proc_macro::TokenStream { let input_str = input.to_string(); - let expr: SubExpr<_, _, Import> = parse_expr(&input_str).unwrap().unnote(); + let expr: SubExpr<_, Import> = parse_expr(&input_str).unwrap().unnote(); let no_import = |_: &Import| -> X { panic!("Don't use import in dhall::expr!()") }; let expr = expr.map_embed(no_import); @@ -17,7 +17,7 @@ pub fn expr(input: proc_macro::TokenStream) -> proc_macro::TokenStream { pub fn subexpr(input: proc_macro::TokenStream) -> proc_macro::TokenStream { let input_str = input.to_string(); - let expr: SubExpr<_, _, Import> = parse_expr(&input_str).unwrap().unnote(); + let expr: SubExpr<_, Import> = parse_expr(&input_str).unwrap().unnote(); let no_import = |_: &Import| -> X { panic!("Don't use import in dhall::subexpr!()") }; let expr = expr.map_embed(no_import); @@ -31,59 +31,60 @@ pub fn quote_exprf<TS>(expr: ExprF<TS, Label, X>) -> TokenStream where TS: quote::ToTokens + std::fmt::Debug, { + use dhall_syntax::ExprF::*; match expr { - ExprF::Var(_) => unreachable!(), - ExprF::Pi(x, t, b) => { + Var(_) => unreachable!(), + Pi(x, t, b) => { let x = quote_label(&x); quote! { dhall_syntax::ExprF::Pi(#x, #t, #b) } } - ExprF::Lam(x, t, b) => { + Lam(x, t, b) => { let x = quote_label(&x); quote! { dhall_syntax::ExprF::Lam(#x, #t, #b) } } - ExprF::App(f, a) => { + App(f, a) => { quote! { dhall_syntax::ExprF::App(#f, #a) } } - ExprF::Annot(x, t) => { + Annot(x, t) => { quote! { dhall_syntax::ExprF::Annot(#x, #t) } } - ExprF::Const(c) => { + Const(c) => { let c = quote_const(c); quote! { dhall_syntax::ExprF::Const(#c) } } - ExprF::Builtin(b) => { + Builtin(b) => { let b = quote_builtin(b); quote! { dhall_syntax::ExprF::Builtin(#b) } } - ExprF::BinOp(o, a, b) => { + BinOp(o, a, b) => { let o = quote_binop(o); quote! { dhall_syntax::ExprF::BinOp(#o, #a, #b) } } - ExprF::NaturalLit(n) => { + NaturalLit(n) => { quote! { dhall_syntax::ExprF::NaturalLit(#n) } } - ExprF::BoolLit(b) => { + BoolLit(b) => { quote! { dhall_syntax::ExprF::BoolLit(#b) } } - ExprF::SomeLit(x) => { + SomeLit(x) => { quote! { dhall_syntax::ExprF::SomeLit(#x) } } - ExprF::EmptyListLit(t) => { + EmptyListLit(t) => { quote! { dhall_syntax::ExprF::EmptyListLit(#t) } } - ExprF::NEListLit(es) => { + NEListLit(es) => { let es = quote_vec(es); quote! { dhall_syntax::ExprF::NEListLit(#es) } } - ExprF::RecordType(m) => { + RecordType(m) => { let m = quote_map(m); quote! { dhall_syntax::ExprF::RecordType(#m) } } - ExprF::RecordLit(m) => { + RecordLit(m) => { let m = quote_map(m); quote! { dhall_syntax::ExprF::RecordLit(#m) } } - ExprF::UnionType(m) => { + UnionType(m) => { let m = quote_opt_map(m); quote! { dhall_syntax::ExprF::UnionType(#m) } } @@ -94,21 +95,22 @@ where // Returns an expression of type SubExpr<_, _>. Expects interpolated variables // to be of type SubExpr<_, _>. fn quote_subexpr( - expr: &SubExpr<Label, X, X>, + expr: &SubExpr<X, X>, ctx: &Context<Label, ()>, ) -> TokenStream { + use dhall_syntax::ExprF::*; match expr.as_ref().map_ref_with_special_handling_of_binders( |e| quote_subexpr(e, ctx), |l, e| quote_subexpr(e, &ctx.insert(l.clone(), ())), |_| unreachable!(), Label::clone, ) { - ExprF::Var(Var(ref s, n)) => { + Var(V(ref s, n)) => { match ctx.lookup(s, n) { // Non-free variable; interpolates as itself Some(()) => { let s: String = s.into(); - let var = quote! { dhall_syntax::Var(#s.into(), #n) }; + let var = quote! { dhall_syntax::V(#s.into(), #n) }; rc(quote! { dhall_syntax::ExprF::Var(#var) }) } // Free variable; interpolates as a rust variable @@ -117,7 +119,7 @@ fn quote_subexpr( // TODO: insert appropriate shifts ? let v: TokenStream = s.parse().unwrap(); quote! { { - let x: dhall_syntax::SubExpr<_, _, _> = #v.clone(); + let x: dhall_syntax::SubExpr<_, _> = #v.clone(); x } } } @@ -127,24 +129,22 @@ fn quote_subexpr( } } -// Returns an expression of type Expr<_, _, _>. Expects interpolated variables -// to be of type SubExpr<_, _, _>. -fn quote_expr( - expr: &Expr<Label, X, X>, - ctx: &Context<Label, ()>, -) -> TokenStream { +// Returns an expression of type Expr<_, _>. Expects interpolated variables +// to be of type SubExpr<_, _>. +fn quote_expr(expr: &Expr<X, X>, ctx: &Context<Label, ()>) -> TokenStream { + use dhall_syntax::ExprF::*; match expr.map_ref_with_special_handling_of_binders( |e| quote_subexpr(e, ctx), |l, e| quote_subexpr(e, &ctx.insert(l.clone(), ())), |_| unreachable!(), Label::clone, ) { - ExprF::Var(Var(ref s, n)) => { + Var(V(ref s, n)) => { match ctx.lookup(s, n) { // Non-free variable; interpolates as itself Some(()) => { let s: String = s.into(); - let var = quote! { dhall_syntax::Var(#s.into(), #n) }; + let var = quote! { dhall_syntax::V(#s.into(), #n) }; quote! { dhall_syntax::ExprF::Var(#var) } } // Free variable; interpolates as a rust variable @@ -153,7 +153,7 @@ fn quote_expr( // TODO: insert appropriate shifts ? let v: TokenStream = s.parse().unwrap(); quote! { { - let x: dhall_syntax::SubExpr<_, _, _> = #v.clone(); + let x: dhall_syntax::SubExpr<_, _> = #v.clone(); x.unroll() } } } diff --git a/dhall_syntax/src/core.rs b/dhall_syntax/src/core.rs index c8a2425..a186d19 100644 --- a/dhall_syntax/src/core.rs +++ b/dhall_syntax/src/core.rs @@ -60,7 +60,19 @@ pub enum Const { /// The `Int` field is a DeBruijn index. /// See dhall-lang/standard/semantics.md for details #[derive(Debug, Clone, PartialEq, Eq)] -pub struct Var<Label>(pub Label, pub usize); +pub struct V<Label>(pub Label, pub usize); + +// This is only for the specific `Label` type, not generic +impl From<Label> for V<Label> { + fn from(x: Label) -> V<Label> { + V(x, 0) + } +} +impl<'a> From<&'a Label> for V<Label> { + fn from(x: &'a Label) -> V<Label> { + V(x.clone(), 0) + } +} // Definition order must match precedence order for // pretty-printing to work correctly @@ -125,52 +137,44 @@ pub enum Builtin { TextShow, } -pub type ParsedExpr = SubExpr<Label, X, Import>; -pub type ResolvedExpr = SubExpr<Label, X, X>; +pub type ParsedExpr = SubExpr<X, Import>; +pub type ResolvedExpr = SubExpr<X, X>; pub type DhallExpr = ResolvedExpr; // Each node carries an annotation. In practice it's either X (no annotation) or a Span. #[derive(Debug)] -pub struct SubExpr<VarLabel, Note, Embed>( - Rc<(Expr<VarLabel, Note, Embed>, Option<Note>)>, -); +pub struct SubExpr<Note, Embed>(Rc<(Expr<Note, Embed>, Option<Note>)>); -impl<VarLabel: PartialEq, Note, Embed: PartialEq> std::cmp::PartialEq - for SubExpr<VarLabel, Note, Embed> -{ +impl<Note, Embed: PartialEq> std::cmp::PartialEq for SubExpr<Note, Embed> { fn eq(&self, other: &Self) -> bool { self.0.as_ref().0 == other.0.as_ref().0 } } -impl<VarLabel: Eq, Note, Embed: Eq> std::cmp::Eq - for SubExpr<VarLabel, Note, Embed> -{ -} +impl<Note, Embed: Eq> std::cmp::Eq for SubExpr<Note, Embed> {} -pub type Expr<VarLabel, Note, Embed> = - ExprF<SubExpr<VarLabel, Note, Embed>, VarLabel, Embed>; +pub type Expr<Note, Embed> = ExprF<SubExpr<Note, Embed>, 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<SubExpr, VarLabel, Embed> { +pub enum ExprF<SubExpr, Label, Embed> { Const(Const), /// `x` /// `x@n` - Var(Var<VarLabel>), + Var(V<Label>), /// `λ(x : A) -> b` - Lam(VarLabel, SubExpr, SubExpr), + Lam(Label, SubExpr, SubExpr), /// `A -> B` /// `∀(x : A) -> B` - Pi(VarLabel, SubExpr, SubExpr), + Pi(Label, SubExpr, SubExpr), /// `f a` App(SubExpr, SubExpr), /// `let x = r in e` /// `let x : t = r in e` - Let(VarLabel, Option<SubExpr>, SubExpr, SubExpr), + Let(Label, Option<SubExpr>, SubExpr, SubExpr), /// `x : t` Annot(SubExpr, SubExpr), /// Built-in values @@ -231,7 +235,11 @@ impl<SE, L, E> ExprF<SE, L, E> { visit_under_binder: impl FnOnce(&'a L, &'a SE) -> Result<SE2, Err>, visit_embed: impl FnOnce(&'a E) -> Result<E2, Err>, visit_label: impl FnMut(&'a L) -> Result<L2, Err>, - ) -> Result<ExprF<SE2, L2, E2>, Err> { + ) -> Result<ExprF<SE2, L2, E2>, Err> + where + L: Ord, + L2: Ord, + { self.visit(visitor::TraverseRefWithBindersVisitor { visit_subexpr, visit_under_binder, @@ -245,7 +253,11 @@ impl<SE, L, E> ExprF<SE, L, E> { visit_subexpr: impl FnMut(&'a SE) -> Result<SE2, Err>, visit_embed: impl FnOnce(&'a E) -> Result<E2, Err>, visit_label: impl FnMut(&'a L) -> Result<L2, Err>, - ) -> Result<ExprF<SE2, L2, E2>, Err> { + ) -> Result<ExprF<SE2, L2, E2>, Err> + where + L: Ord, + L2: Ord, + { self.visit(visitor::TraverseRefVisitor { visit_subexpr, visit_embed, @@ -259,7 +271,11 @@ impl<SE, L, E> ExprF<SE, L, E> { mut map_under_binder: impl FnMut(&'a L, &'a SE) -> SE2, map_embed: impl FnOnce(&'a E) -> E2, mut map_label: impl FnMut(&'a L) -> L2, - ) -> ExprF<SE2, L2, E2> { + ) -> ExprF<SE2, L2, E2> + where + L: Ord, + L2: Ord, + { trivial_result(self.traverse_ref_with_special_handling_of_binders( |x| Ok(map_subexpr(x)), |l, x| Ok(map_under_binder(l, x)), @@ -273,7 +289,11 @@ impl<SE, L, E> ExprF<SE, L, E> { mut map_subexpr: impl FnMut(&'a SE) -> SE2, map_embed: impl FnOnce(&'a E) -> E2, mut map_label: impl FnMut(&'a L) -> L2, - ) -> ExprF<SE2, L2, E2> { + ) -> ExprF<SE2, L2, E2> + where + L: Ord, + L2: Ord, + { trivial_result(self.traverse_ref( |x| Ok(map_subexpr(x)), |x| Ok(map_embed(x)), @@ -286,7 +306,7 @@ impl<SE, L, E> ExprF<SE, L, E> { visit_subexpr: impl FnMut(&'a SE) -> Result<SE2, Err>, ) -> Result<ExprF<SE2, L, E>, Err> where - L: Clone, + L: Ord + Clone, E: Clone, { self.traverse_ref( @@ -301,31 +321,26 @@ impl<SE, L, E> ExprF<SE, L, E> { map_subexpr: impl Fn(&'a SE) -> SE2, ) -> ExprF<SE2, L, E> where - L: Clone, + L: Ord + Clone, E: Clone, { self.map_ref(map_subexpr, E::clone, L::clone) } } -impl<L, N, E> Expr<L, N, E> { +impl<N, E> Expr<N, E> { fn traverse_embed<E2, Err>( &self, visit_embed: impl FnMut(&E) -> Result<E2, Err>, - ) -> Result<Expr<L, N, E2>, Err> + ) -> Result<Expr<N, E2>, Err> where - L: Clone, N: Clone, { self.visit(&mut visitor::TraverseEmbedVisitor(visit_embed)) } - fn map_embed<E2>( - &self, - mut map_embed: impl FnMut(&E) -> E2, - ) -> Expr<L, N, E2> + fn map_embed<E2>(&self, mut map_embed: impl FnMut(&E) -> E2) -> Expr<N, E2> where - L: Clone, N: Clone, { trivial_result(self.traverse_embed(|x| Ok(map_embed(x)))) @@ -333,52 +348,52 @@ impl<L, N, E> Expr<L, N, E> { pub fn squash_embed<E2>( &self, - f: impl FnMut(&E) -> SubExpr<L, N, E2>, - ) -> SubExpr<L, N, E2> + f: impl FnMut(&E) -> SubExpr<N, E2>, + ) -> SubExpr<N, E2> where - L: Clone, N: Clone, { trivial_result(self.visit(&mut visitor::SquashEmbedVisitor(f))) } } -impl<L: Clone, E: Clone> Expr<L, X, E> { - pub fn note_absurd<N>(&self) -> Expr<L, N, E> { +impl<E: Clone> Expr<X, E> { + pub fn note_absurd<N>(&self) -> Expr<N, E> { self.visit(&mut visitor::NoteAbsurdVisitor) } } -impl<L: Clone, N: Clone> Expr<L, N, X> { - pub fn embed_absurd<E>(&self) -> Expr<L, N, E> { +impl<N: Clone> Expr<N, X> { + pub fn embed_absurd<E>(&self) -> Expr<N, E> { self.visit(&mut visitor::EmbedAbsurdVisitor) } } -impl<V, N, E> SubExpr<V, N, E> { - pub fn as_ref(&self) -> &Expr<V, N, E> { +impl<N, E> SubExpr<N, E> { + pub fn as_ref(&self) -> &Expr<N, E> { &self.0.as_ref().0 } - pub fn new(x: Expr<V, N, E>, n: N) -> Self { + pub fn new(x: Expr<N, E>, n: N) -> Self { SubExpr(Rc::new((x, Some(n)))) } - pub fn from_expr_no_note(x: Expr<V, N, E>) -> Self { + pub fn from_expr_no_note(x: Expr<N, E>) -> Self { SubExpr(Rc::new((x, None))) } - pub fn unnote(&self) -> SubExpr<V, X, E> + pub fn unnote(&self) -> SubExpr<X, E> where - V: Clone, E: Clone, { SubExpr::from_expr_no_note( self.as_ref().visit(&mut visitor::UnNoteVisitor), ) } +} - pub fn rewrap<E2>(&self, x: Expr<V, N, E2>) -> SubExpr<V, N, E2> +impl<N: Clone, E> SubExpr<N, E> { + pub fn rewrap<E2>(&self, x: Expr<N, E2>) -> SubExpr<N, E2> where N: Clone, { @@ -388,9 +403,8 @@ impl<V, N, E> SubExpr<V, N, E> { pub fn traverse_embed<E2, Err>( &self, visit_embed: impl FnMut(&E) -> Result<E2, Err>, - ) -> Result<SubExpr<V, N, E2>, Err> + ) -> Result<SubExpr<N, E2>, Err> where - V: Clone, N: Clone, { Ok(self.rewrap(self.as_ref().traverse_embed(visit_embed)?)) @@ -399,9 +413,8 @@ impl<V, N, E> SubExpr<V, N, E> { pub fn map_embed<E2>( &self, map_embed: impl FnMut(&E) -> E2, - ) -> SubExpr<V, N, E2> + ) -> SubExpr<N, E2> where - V: Clone, N: Clone, { self.rewrap(self.as_ref().map_embed(map_embed)) @@ -410,12 +423,8 @@ impl<V, N, E> SubExpr<V, N, E> { pub fn map_subexprs_with_special_handling_of_binders<'a>( &'a self, map_expr: impl FnMut(&'a Self) -> Self, - map_under_binder: impl FnMut(&'a V, &'a Self) -> Self, - ) -> Self - where - V: Clone, - N: Clone, - { + map_under_binder: impl FnMut(&'a Label, &'a Self) -> Self, + ) -> Self { match self.as_ref() { ExprF::Embed(_) => SubExpr::clone(self), // This calls ExprF::map_ref @@ -423,7 +432,7 @@ impl<V, N, E> SubExpr<V, N, E> { map_expr, map_under_binder, |_| unreachable!(), - V::clone, + Label::clone, )), } } @@ -432,34 +441,26 @@ impl<V, N, E> SubExpr<V, N, E> { /// capture by shifting variable indices /// See https://github.com/dhall-lang/dhall-lang/blob/master/standard/semantics.md#shift /// for details - pub fn shift(&self, delta: isize, var: &Var<V>) -> Self - where - V: Clone + PartialEq, - N: Clone, - { + pub fn shift(&self, delta: isize, var: &V<Label>) -> Self { match self.as_ref() { ExprF::Var(v) => self.rewrap(ExprF::Var(v.shift(delta, var))), _ => self.map_subexprs_with_special_handling_of_binders( |e| e.shift(delta, var), - |x: &V, e| e.shift(delta, &var.shift(1, &Var::new(x.clone()))), + |x: &Label, e| e.shift(delta, &var.shift(1, &x.into())), ), } } - pub fn subst_shift(&self, var: &Var<V>, val: &Self) -> Self - where - V: Clone + PartialEq, - N: Clone, - { + pub fn subst_shift(&self, var: &V<Label>, val: &Self) -> Self { match self.as_ref() { ExprF::Var(v) if v == var => val.clone(), ExprF::Var(v) => self.rewrap(ExprF::Var(v.shift(-1, var))), _ => self.map_subexprs_with_special_handling_of_binders( |e| e.subst_shift(var, val), - |x: &V, e| { + |x: &Label, e| { e.subst_shift( - &var.shift(1, &Var::new(x.clone())), - &val.shift(1, &Var::new(x.clone())), + &var.shift(1, &x.into()), + &val.shift(1, &x.into()), ) }, ), @@ -467,26 +468,26 @@ impl<V, N, E> SubExpr<V, N, E> { } } -impl<L: Clone, N: Clone> SubExpr<L, N, X> { - pub fn embed_absurd<T>(&self) -> SubExpr<L, N, T> { +impl<N: Clone> SubExpr<N, X> { + pub fn embed_absurd<T>(&self) -> SubExpr<N, T> { self.rewrap(self.as_ref().embed_absurd()) } } -impl<L: Clone, E: Clone> SubExpr<L, X, E> { - pub fn note_absurd<N>(&self) -> SubExpr<L, N, E> { +impl<E: Clone> SubExpr<X, E> { + pub fn note_absurd<N>(&self) -> SubExpr<N, E> { SubExpr::from_expr_no_note(self.as_ref().note_absurd()) } } -impl<L, N, E> Clone for SubExpr<L, N, E> { +impl<N, E> Clone for SubExpr<N, E> { fn clone(&self) -> Self { SubExpr(Rc::clone(&self.0)) } } // Should probably rename this -pub fn rc<L, E>(x: Expr<L, X, E>) -> SubExpr<L, X, E> { +pub fn rc<E>(x: Expr<X, E>) -> SubExpr<X, E> { SubExpr::from_expr_no_note(x) } @@ -500,35 +501,18 @@ fn add_ui(u: usize, i: isize) -> usize { } } -impl<L> Var<L> { - fn new(x: L) -> Self { - Var(x, 0) - } -} -impl<L: PartialEq + Clone> Var<L> { - pub fn shift(&self, delta: isize, var: &Var<L>) -> Self { - let Var(x, n) = var; - let Var(y, m) = self; +impl<Label: PartialEq + Clone> V<Label> { + pub fn shift(&self, delta: isize, var: &V<Label>) -> Self { + let V(x, n) = var; + let V(y, m) = self; if x == y && n <= m { - Var(y.clone(), add_ui(*m, delta)) + V(y.clone(), add_ui(*m, delta)) } else { - Var(y.clone(), *m) + V(y.clone(), *m) } } } -// This is only for the specific `Label` type, not generic -impl From<Label> for Var<Label> { - fn from(x: Label) -> Var<Label> { - Var(x, 0) - } -} -impl<'a> From<&'a Label> for Var<Label> { - fn from(x: &'a Label) -> Var<Label> { - Var(x.clone(), 0) - } -} - /// `shift` is used by both normalization and type-checking to avoid variable /// capture by shifting variable indices /// See https://github.com/dhall-lang/dhall-lang/blob/master/standard/semantics.md#shift @@ -536,9 +520,9 @@ impl<'a> From<&'a Label> for Var<Label> { /// pub fn shift<N, E>( delta: isize, - var: &Var<Label>, - in_expr: &SubExpr<Label, N, E>, -) -> SubExpr<Label, N, E> + var: &V<Label>, + in_expr: &SubExpr<N, E>, +) -> SubExpr<N, E> where N: Clone, { @@ -547,8 +531,8 @@ where pub fn shift0_multiple<N, E>( deltas: &HashMap<Label, isize>, - in_expr: &SubExpr<Label, N, E>, -) -> SubExpr<Label, N, E> + in_expr: &SubExpr<N, E>, +) -> SubExpr<N, E> where N: Clone, { @@ -558,15 +542,16 @@ where fn shift0_multiple_inner<N, E>( ctx: &Context<Label, ()>, deltas: &HashMap<Label, isize>, - in_expr: &SubExpr<Label, N, E>, -) -> SubExpr<Label, N, E> + in_expr: &SubExpr<N, E>, +) -> SubExpr<N, E> where N: Clone, { + use crate::ExprF::*; match in_expr.as_ref() { - ExprF::Var(Var(y, m)) if ctx.lookup(y, *m).is_none() => { + Var(V(y, m)) if ctx.lookup(y, *m).is_none() => { let delta = deltas.get(y).unwrap_or(&0); - in_expr.rewrap(ExprF::Var(Var(y.clone(), add_ui(*m, *delta)))) + in_expr.rewrap(Var(V(y.clone(), add_ui(*m, *delta)))) } _ => in_expr.map_subexprs_with_special_handling_of_binders( |e| shift0_multiple_inner(ctx, deltas, e), diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs index bdef553..83ccc1e 100644 --- a/dhall_syntax/src/parser.rs +++ b/dhall_syntax/src/parser.rs @@ -8,13 +8,7 @@ use std::rc::Rc; use dhall_generated_parser::{DhallParser, Rule}; -use crate::ExprF::{ - Annot, App, BinOp, BoolIf, BoolLit, Builtin, Const, DoubleLit, Embed, - EmptyListLit, Field, IntegerLit, Lam, Let, Merge, NEListLit, NaturalLit, - OldOptionalLit, Pi, Projection, RecordLit, RecordType, SomeLit, TextLit, - UnionLit, UnionType, -}; - +use crate::ExprF::*; use crate::*; // This file consumes the parse tree generated by pest and turns it into @@ -22,10 +16,10 @@ use crate::*; // their own crate because they are quite general and useful. For now they // are here and hopefully you can figure out how they work. -type ParsedExpr = Expr<Label, Span, Import>; -type ParsedSubExpr = SubExpr<Label, Span, Import>; -type ParsedText = InterpolatedText<ParsedSubExpr>; -type ParsedTextContents = InterpolatedTextContents<ParsedSubExpr>; +type ParsedExpr = Expr<Span, Import>; +type ParsedSubExpr = SubExpr<Span, Import>; +type ParsedText = InterpolatedText<SubExpr<Span, Import>>; +type ParsedTextContents = InterpolatedTextContents<SubExpr<Span, Import>>; pub type ParseError = pest::error::Error<Rule>; @@ -510,17 +504,17 @@ make_parser! { rule!(identifier<ParsedSubExpr> as expression; span; children!( [variable(v)] => { - spanned(span, ExprF::Var(v)) + spanned(span, Var(v)) }, [builtin(e)] => e, )); - rule!(variable<Var<Label>>; children!( + rule!(variable<V<Label>>; children!( [label(l), natural_literal(idx)] => { - Var(l, idx) + V(l, idx) }, [label(l)] => { - Var(l, 0) + V(l, 0) }, )); diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs index 9cc1b46..e3b180b 100644 --- a/dhall_syntax/src/printer.rs +++ b/dhall_syntax/src/printer.rs @@ -3,9 +3,7 @@ use itertools::Itertools; use std::fmt::{self, Display}; /// Generic instance that delegates to subexpressions -impl<SE: Display + Clone, L: Display + Clone, E: Display> Display - for ExprF<SE, L, E> -{ +impl<SE: Display + Clone, E: Display> Display for ExprF<SE, Label, E> { fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { use crate::ExprF::*; match self { @@ -15,10 +13,9 @@ impl<SE: Display + Clone, L: Display + Clone, E: Display> Display BoolIf(a, b, c) => { write!(f, "if {} then {} else {}", a, b, c)?; } - // TODO: arrow type - // Pi(a, b, c) if &String::from(a) == "_" => { - // write!(f, "{} → {}", b, c)?; - // } + Pi(a, b, c) if &String::from(a) == "_" => { + write!(f, "{} → {}", b, c)?; + } Pi(a, b, c) => { write!(f, "∀({} : {}) → {}", a, b, c)?; } @@ -127,25 +124,21 @@ enum PrintPhase { // Wraps an Expr with a phase, so that phase selsction can be done // separate from the actual printing #[derive(Clone)] -struct PhasedExpr<'a, L, S, A>(&'a SubExpr<L, S, A>, PrintPhase); +struct PhasedExpr<'a, S, A>(&'a SubExpr<S, A>, PrintPhase); -impl<'a, L: Display + Clone, S: Clone, A: Display + Clone> Display - for PhasedExpr<'a, L, S, A> -{ +impl<'a, S: Clone, A: Display + Clone> Display for PhasedExpr<'a, S, A> { fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { self.0.as_ref().fmt_phase(f, self.1) } } -impl<'a, L: Display + Clone, S: Clone, A: Display + Clone> - PhasedExpr<'a, L, S, A> -{ - fn phase(self, phase: PrintPhase) -> PhasedExpr<'a, L, S, A> { +impl<'a, S: Clone, A: Display + Clone> PhasedExpr<'a, S, A> { + fn phase(self, phase: PrintPhase) -> PhasedExpr<'a, S, A> { PhasedExpr(self.0, phase) } } -impl<L: Display + Clone, S: Clone, A: Display + Clone> Expr<L, S, A> { +impl<S: Clone, A: Display + Clone> Expr<S, A> { fn fmt_phase( &self, f: &mut fmt::Formatter, @@ -179,12 +172,11 @@ impl<L: Display + Clone, S: Clone, A: Display + Clone> Expr<L, S, A> { // Annotate subexpressions with the appropriate phase, defaulting to Base let phased_self = match self.map_ref_simple(|e| PhasedExpr(e, Base)) { Pi(a, b, c) => { - // TODO: arrow type - // if &String::from(&a) == "_" { - // Pi(a, b.phase(Operator), c) - // } else { - Pi(a, b, c) - // } + if &String::from(&a) == "_" { + Pi(a, b.phase(Operator), c) + } else { + Pi(a, b, c) + } } Merge(a, b, c) => Merge( a.phase(Import), @@ -220,9 +212,7 @@ impl<L: Display + Clone, S: Clone, A: Display + Clone> Expr<L, S, A> { } } -impl<L: Display + Clone, S: Clone, A: Display + Clone> Display - for SubExpr<L, S, A> -{ +impl<S: Clone, A: Display + Clone> Display for SubExpr<S, A> { fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { self.as_ref().fmt_phase(f, PrintPhase::Base) } @@ -484,9 +474,9 @@ impl Display for Scheme { } } -impl<Label: Display> Display for Var<Label> { +impl<Label: Display> Display for V<Label> { fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { - let Var(x, n) = self; + let V(x, n) = self; x.fmt(f)?; if *n != 0 { write!(f, "@{}", n)?; diff --git a/dhall_syntax/src/visitor.rs b/dhall_syntax/src/visitor.rs index a8e5a8c..7fdf217 100644 --- a/dhall_syntax/src/visitor.rs +++ b/dhall_syntax/src/visitor.rs @@ -48,6 +48,8 @@ pub trait ExprFVeryGenericVisitor<'a, Ret, SE1, L1, E1>: Sized { impl<'a, T, Ret, SE1, L1, E1> GenericVisitor<&'a ExprF<SE1, L1, E1>, Result<Ret, T::Error>> for T where + L1: Ord, + T::L2: Ord, T: ExprFVeryGenericVisitor<'a, Ret, SE1, L1, E1>, { fn visit(self, input: &'a ExprF<SE1, L1, E1>) -> Result<Ret, T::Error> { @@ -67,27 +69,31 @@ where }) } fn btmap<'a, V, Ret, SE, L, E>( - x: &'a BTreeMap<Label, SE>, + x: &'a BTreeMap<L, SE>, mut v: V, - ) -> Result<BTreeMap<Label, V::SE2>, V::Error> + ) -> Result<BTreeMap<V::L2, V::SE2>, V::Error> where + L: Ord, + V::L2: Ord, V: ExprFVeryGenericVisitor<'a, Ret, SE, L, E>, { x.iter() - .map(|(k, x)| Ok((k.clone(), v.visit_subexpr(x)?))) + .map(|(k, x)| Ok((v.visit_label(k)?, v.visit_subexpr(x)?))) .collect() } fn btoptmap<'a, V, Ret, SE, L, E>( - x: &'a BTreeMap<Label, Option<SE>>, + x: &'a BTreeMap<L, Option<SE>>, mut v: V, - ) -> Result<BTreeMap<Label, Option<V::SE2>>, V::Error> + ) -> Result<BTreeMap<V::L2, Option<V::SE2>>, V::Error> where + L: Ord, + V::L2: Ord, V: ExprFVeryGenericVisitor<'a, Ret, SE, L, E>, { x.iter() .map(|(k, x)| { Ok(( - k.clone(), + v.visit_label(k)?, match x { Some(x) => Some(v.visit_subexpr(x)?), None => None, @@ -98,14 +104,9 @@ where } let mut v = self; - use crate::ExprF::{ - Annot, App, BinOp, BoolIf, BoolLit, Builtin, Const, DoubleLit, - Embed, EmptyListLit, Field, IntegerLit, Lam, Let, Merge, NEListLit, - NaturalLit, OldOptionalLit, Pi, Projection, RecordLit, RecordType, - SomeLit, TextLit, UnionLit, UnionType, - }; + use crate::ExprF::*; T::visit_resulting_exprf(match input { - ExprF::Var(Var(l, n)) => ExprF::Var(Var(v.visit_label(l)?, *n)), + Var(V(l, n)) => Var(V(v.visit_label(l)?, *n)), Lam(l, t, e) => { let t = v.visit_subexpr(t)?; let (l, e) = v.visit_binder(l, e)?; @@ -149,16 +150,20 @@ where RecordType(kts) => RecordType(btmap(kts, v)?), RecordLit(kvs) => RecordLit(btmap(kvs, v)?), UnionType(kts) => UnionType(btoptmap(kts, v)?), - UnionLit(l, x, kts) => { - UnionLit(l.clone(), v.visit_subexpr(x)?, btoptmap(kts, v)?) - } + UnionLit(k, x, kts) => UnionLit( + v.visit_label(k)?, + v.visit_subexpr(x)?, + btoptmap(kts, v)?, + ), Merge(x, y, t) => Merge( v.visit_subexpr(x)?, v.visit_subexpr(y)?, opt(t, |e| v.visit_subexpr(e))?, ), - Field(e, l) => Field(v.visit_subexpr(e)?, l.clone()), - Projection(e, ls) => Projection(v.visit_subexpr(e)?, ls.clone()), + Field(e, l) => Field(v.visit_subexpr(e)?, v.visit_label(l)?), + Projection(e, ls) => { + Projection(v.visit_subexpr(e)?, vec(ls, |l| v.visit_label(l))?) + } Embed(a) => return v.visit_embed_squash(a), }) } @@ -309,6 +314,8 @@ where impl<'a, T, SE1, SE2, L1, L2, E1, E2> GenericVisitor<&'a ExprF<SE1, L1, E1>, ExprF<SE2, L2, E2>> for T where + L1: Ord, + L2: Ord, T: ExprFInFallibleVisitor<'a, SE1, SE2, L1, L2, E1, E2>, { fn visit(self, input: &'a ExprF<SE1, L1, E1>) -> ExprF<SE2, L2, E2> { @@ -330,6 +337,8 @@ where SE: 'a, L: 'a, E: 'a, + L: Ord, + L2: Ord, F1: FnMut(&'a SE) -> Result<SE2, Err>, F2: FnOnce(&'a L, &'a SE) -> Result<SE2, Err>, F4: FnOnce(&'a E) -> Result<E2, Err>, @@ -368,6 +377,8 @@ where SE: 'a, L: 'a, E: 'a, + L: Ord, + L2: Ord, F1: FnMut(&'a SE) -> Result<SE2, Err>, F3: FnOnce(&'a E) -> Result<E2, Err>, F4: FnMut(&'a L) -> Result<L2, Err>, @@ -387,11 +398,10 @@ where pub struct TraverseEmbedVisitor<F1>(pub F1); -impl<'a, 'b, L, N, E, E2, Err, F1> - ExprFFallibleVisitor<'a, SubExpr<L, N, E>, SubExpr<L, N, E2>, L, L, E, E2> +impl<'a, 'b, N, E, E2, Err, F1> + ExprFFallibleVisitor<'a, SubExpr<N, E>, SubExpr<N, E2>, Label, Label, E, E2> for &'b mut TraverseEmbedVisitor<F1> where - L: Clone + 'a, N: Clone + 'a, F1: FnMut(&E) -> Result<E2, Err>, { @@ -399,48 +409,50 @@ where fn visit_subexpr( &mut self, - subexpr: &'a SubExpr<L, N, E>, - ) -> Result<SubExpr<L, N, E2>, Self::Error> { + subexpr: &'a SubExpr<N, E>, + ) -> Result<SubExpr<N, E2>, Self::Error> { Ok(subexpr.rewrap(subexpr.as_ref().visit(&mut **self)?)) } fn visit_embed(self, embed: &'a E) -> Result<E2, Self::Error> { (self.0)(embed) } - fn visit_label(&mut self, label: &'a L) -> Result<L, Self::Error> { - Ok(L::clone(label)) + fn visit_label(&mut self, label: &'a Label) -> Result<Label, Self::Error> { + Ok(Label::clone(label)) } } pub struct SquashEmbedVisitor<F1>(pub F1); -impl<'a, 'b, L, N, E1, E2, F1> - ExprFVeryGenericVisitor<'a, SubExpr<L, N, E2>, SubExpr<L, N, E1>, L, E1> +impl<'a, 'b, N, E1, E2, F1> + ExprFVeryGenericVisitor<'a, SubExpr<N, E2>, SubExpr<N, E1>, Label, E1> for &'b mut SquashEmbedVisitor<F1> where - L: Clone + 'a, N: Clone + 'a, - F1: FnMut(&E1) -> SubExpr<L, N, E2>, + F1: FnMut(&E1) -> SubExpr<N, E2>, { type Error = X; - type SE2 = SubExpr<L, N, E2>; - type L2 = L; + type SE2 = SubExpr<N, E2>; + type L2 = Label; type E2 = E2; fn visit_subexpr( &mut self, - subexpr: &'a SubExpr<L, N, E1>, + subexpr: &'a SubExpr<N, E1>, ) -> Result<Self::SE2, Self::Error> { Ok(subexpr.as_ref().visit(&mut **self)?) } - fn visit_label(&mut self, label: &'a L) -> Result<Self::L2, Self::Error> { - Ok(L::clone(label)) + fn visit_label( + &mut self, + label: &'a Label, + ) -> Result<Self::L2, Self::Error> { + Ok(Label::clone(label)) } fn visit_binder( mut self, - label: &'a L, - subexpr: &'a SubExpr<L, N, E1>, + label: &'a Label, + subexpr: &'a SubExpr<N, E1>, ) -> Result<(Self::L2, Self::SE2), Self::Error> { Ok((self.visit_label(label)?, self.visit_subexpr(subexpr)?)) } @@ -448,7 +460,7 @@ where fn visit_embed_squash( self, embed: &'a E1, - ) -> Result<SubExpr<L, N, E2>, Self::Error> { + ) -> Result<SubExpr<N, E2>, Self::Error> { Ok((self.0)(embed)) } @@ -456,7 +468,7 @@ where // Useful to change the result type, and/or avoid some loss of info fn visit_resulting_exprf( result: ExprF<Self::SE2, Self::L2, Self::E2>, - ) -> Result<SubExpr<L, N, E2>, Self::Error> { + ) -> Result<SubExpr<N, E2>, Self::Error> { // TODO: don't lose note Ok(SubExpr::from_expr_no_note(result)) } @@ -464,69 +476,57 @@ where pub struct UnNoteVisitor; -impl<'a, 'b, L, N, E> - ExprFInFallibleVisitor<'a, SubExpr<L, N, E>, SubExpr<L, X, E>, L, L, E, E> +impl<'a, 'b, N, E> + ExprFInFallibleVisitor<'a, SubExpr<N, E>, SubExpr<X, E>, Label, Label, E, E> for &'b mut UnNoteVisitor where - L: Clone + 'a, E: Clone + 'a, { - fn visit_subexpr( - &mut self, - subexpr: &'a SubExpr<L, N, E>, - ) -> SubExpr<L, X, E> { + fn visit_subexpr(&mut self, subexpr: &'a SubExpr<N, E>) -> SubExpr<X, E> { SubExpr::from_expr_no_note(subexpr.as_ref().visit(&mut **self)) } fn visit_embed(self, embed: &'a E) -> E { E::clone(embed) } - fn visit_label(&mut self, label: &'a L) -> L { - L::clone(label) + fn visit_label(&mut self, label: &'a Label) -> Label { + Label::clone(label) } } pub struct NoteAbsurdVisitor; -impl<'a, 'b, L, N, E> - ExprFInFallibleVisitor<'a, SubExpr<L, X, E>, SubExpr<L, N, E>, L, L, E, E> +impl<'a, 'b, N, E> + ExprFInFallibleVisitor<'a, SubExpr<X, E>, SubExpr<N, E>, Label, Label, E, E> for &'b mut NoteAbsurdVisitor where - L: Clone + 'a, E: Clone + 'a, { - fn visit_subexpr( - &mut self, - subexpr: &'a SubExpr<L, X, E>, - ) -> SubExpr<L, N, E> { + fn visit_subexpr(&mut self, subexpr: &'a SubExpr<X, E>) -> SubExpr<N, E> { SubExpr::from_expr_no_note(subexpr.as_ref().visit(&mut **self)) } fn visit_embed(self, embed: &'a E) -> E { E::clone(embed) } - fn visit_label(&mut self, label: &'a L) -> L { - L::clone(label) + fn visit_label(&mut self, label: &'a Label) -> Label { + Label::clone(label) } } pub struct EmbedAbsurdVisitor; -impl<'a, 'b, L, N, E> - ExprFInFallibleVisitor<'a, SubExpr<L, N, X>, SubExpr<L, N, E>, L, L, X, E> +impl<'a, 'b, N, E> + ExprFInFallibleVisitor<'a, SubExpr<N, X>, SubExpr<N, E>, Label, Label, X, E> for &'b mut EmbedAbsurdVisitor where - L: Clone + 'a, N: Clone + 'a, { - fn visit_subexpr( - &mut self, - subexpr: &'a SubExpr<L, N, X>, - ) -> SubExpr<L, N, E> { + fn visit_subexpr(&mut self, subexpr: &'a SubExpr<N, X>) -> SubExpr<N, E> { subexpr.rewrap(subexpr.as_ref().visit(&mut **self)) } fn visit_embed(self, embed: &'a X) -> E { match *embed {} } - fn visit_label(&mut self, label: &'a L) -> L { - L::clone(label) + fn visit_label(&mut self, label: &'a Label) -> Label { + Label::clone(label) } } |