diff options
| -rw-r--r-- | dhall/src/api/mod.rs | 4 | ||||
| -rw-r--r-- | dhall/src/core/thunk.rs | 4 | ||||
| -rw-r--r-- | dhall/src/core/value.rs | 50 | ||||
| -rw-r--r-- | dhall/src/phase/mod.rs | 3 | ||||
| -rw-r--r-- | dhall/src/phase/typecheck.rs | 107 | ||||
| -rw-r--r-- | dhall/tests/traits.rs | 30 | ||||
| -rw-r--r-- | dhall_proc_macros/src/lib.rs | 11 | ||||
| -rw-r--r-- | dhall_proc_macros/src/quote.rs | 223 |
8 files changed, 137 insertions, 295 deletions
diff --git a/dhall/src/api/mod.rs b/dhall/src/api/mod.rs index 233d7cf..188b6c0 100644 --- a/dhall/src/api/mod.rs +++ b/dhall/src/api/mod.rs @@ -66,10 +66,6 @@ mod typ { )) } #[doc(hidden)] - pub fn from_normalized_expr(e: NormalizedSubExpr) -> Self { - Type(Typed::from_normalized_expr_untyped(e)) - } - #[doc(hidden)] pub fn make_record_type( kts: impl Iterator<Item = (String, Type)>, ) -> Self { diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index 5bc25f2..f41579c 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -111,10 +111,6 @@ impl Thunk { ThunkInternal::Value(WHNF, v).into_thunk() } - pub fn from_normalized_expr(e: OutputSubExpr) -> Thunk { - Thunk::new(NormalizationContext::new(), e.absurd()) - } - pub fn from_partial_expr(e: ExprF<Thunk, X>) -> Thunk { ThunkInternal::PartialExpr(e).into_thunk() } diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 26568b5..0b68bf6 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -1,6 +1,5 @@ use std::collections::HashMap; -use dhall_proc_macros as dhall; use dhall_syntax::{ rc, Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, NaiveDouble, Natural, X, @@ -75,6 +74,47 @@ impl Value { /// Convert the value to a fully normalized syntactic expression. Also alpha-normalize /// if alpha is `true` pub fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr { + // Ad-hoc macro to help construct the unapplied closures + macro_rules! make_expr { + (Natural) => { rc(ExprF::Builtin(Builtin::Natural)) }; + (var($var:ident)) => { + rc(ExprF::Var(dhall_syntax::V(stringify!($var).into(), 0))) + }; + ($var:ident) => { $var }; + (List $($rest:tt)*) => { + rc(ExprF::App( + rc(ExprF::Builtin(Builtin::List)), + make_expr!($($rest)*) + )) + }; + (Some $($rest:tt)*) => { + rc(ExprF::SomeLit( + make_expr!($($rest)*) + )) + }; + (1 + $($rest:tt)*) => { + rc(ExprF::BinOp( + dhall_syntax::BinOp::NaturalPlus, + rc(ExprF::NaturalLit(1)), + make_expr!($($rest)*) + )) + }; + ([ $($head:tt)* ] # $($tail:tt)*) => { + rc(ExprF::BinOp( + dhall_syntax::BinOp::ListAppend, + rc(ExprF::NEListLit(vec![make_expr!($($head)*)])), + make_expr!($($tail)*) + )) + }; + (λ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => { + rc(ExprF::Pi( + stringify!($var).into(), + make_expr!($($ty)*), + make_expr!($($rest)*) + )) + }; + } + match self { Value::Lam(x, t, e) => rc(ExprF::Lam( x.to_label_maybe_alpha(alpha), @@ -93,24 +133,24 @@ impl Value { } Value::OptionalSomeClosure(n) => { let a = n.normalize_to_expr_maybe_alpha(alpha); - dhall::subexpr!(λ(x: a) -> Some x) + make_expr!(λ(x: a) -> Some var(x)) } Value::ListConsClosure(a, None) => { // Avoid accidental capture of the new `x` variable let a1 = a.under_binder(Label::from("x")); let a1 = a1.normalize_to_expr_maybe_alpha(alpha); let a = a.normalize_to_expr_maybe_alpha(alpha); - dhall::subexpr!(λ(x : a) -> λ(xs : List a1) -> [ x ] # xs) + make_expr!(λ(x : a) -> λ(xs : List a1) -> [ var(x) ] # var(xs)) } Value::ListConsClosure(n, Some(v)) => { // Avoid accidental capture of the new `xs` variable let v = v.under_binder(Label::from("xs")); let v = v.normalize_to_expr_maybe_alpha(alpha); let a = n.normalize_to_expr_maybe_alpha(alpha); - dhall::subexpr!(λ(xs : List a) -> [ v ] # xs) + make_expr!(λ(xs : List a) -> [ v ] # var(xs)) } Value::NaturalSuccClosure => { - dhall::subexpr!(λ(x : Natural) -> x + 1) + make_expr!(λ(x : Natural) -> 1 + var(x)) } Value::Pi(x, t, e) => rc(ExprF::Pi( x.to_label_maybe_alpha(alpha), diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs index 681b7fe..ccedff2 100644 --- a/dhall/src/phase/mod.rs +++ b/dhall/src/phase/mod.rs @@ -127,9 +127,6 @@ impl Typed { pub fn from_value_untyped(v: Value) -> Self { Typed::from_thunk_untyped(Thunk::from_value(v)) } - pub fn from_normalized_expr_untyped(e: NormalizedSubExpr) -> Self { - Typed::from_thunk_untyped(Thunk::from_normalized_expr(e)) - } // TODO: Avoid cloning if possible pub fn to_value(&self) -> Value { diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 297a096..8f5ca8b 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -1,6 +1,5 @@ use std::collections::HashMap; -use dhall_proc_macros as dhall; use dhall_syntax::{ rc, Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, Span, SubExpr, X, @@ -173,41 +172,97 @@ pub fn type_of_const(c: Const) -> Result<Type, TypeError> { } } +// Ad-hoc macro to help construct the types of builtins +macro_rules! make_type { + (Type) => { ExprF::Const(Const::Type) }; + (Bool) => { ExprF::Builtin(Builtin::Bool) }; + (Natural) => { ExprF::Builtin(Builtin::Natural) }; + (Integer) => { ExprF::Builtin(Builtin::Integer) }; + (Double) => { ExprF::Builtin(Builtin::Double) }; + (Text) => { ExprF::Builtin(Builtin::Text) }; + ($var:ident) => { + ExprF::Var(dhall_syntax::V(stringify!($var).into(), 0)) + }; + (Optional $ty:ident) => { + ExprF::App( + rc(ExprF::Builtin(Builtin::Optional)), + rc(make_type!($ty)) + ) + }; + (List $($rest:tt)*) => { + ExprF::App( + rc(ExprF::Builtin(Builtin::List)), + rc(make_type!($($rest)*)) + ) + }; + ({ $($label:ident : $ty:ident),* }) => {{ + let mut kts = dhall_syntax::map::DupTreeMap::new(); + $( + kts.insert( + Label::from(stringify!($label)), + rc(make_type!($ty)), + ); + )* + ExprF::RecordType(kts) + }}; + ($ty:ident -> $($rest:tt)*) => { + ExprF::Pi( + "_".into(), + rc(make_type!($ty)), + rc(make_type!($($rest)*)) + ) + }; + (($($arg:tt)*) -> $($rest:tt)*) => { + ExprF::Pi( + "_".into(), + rc(make_type!($($arg)*)), + rc(make_type!($($rest)*)) + ) + }; + (forall ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => { + ExprF::Pi( + stringify!($var).into(), + rc(make_type!($($ty)*)), + rc(make_type!($($rest)*)) + ) + }; +} + fn type_of_builtin(b: Builtin) -> Expr<X, X> { use dhall_syntax::Builtin::*; match b { - Bool | Natural | Integer | Double | Text => dhall::expr!(Type), - List | Optional => dhall::expr!( + Bool | Natural | Integer | Double | Text => make_type!(Type), + List | Optional => make_type!( Type -> Type ), - NaturalFold => dhall::expr!( + NaturalFold => make_type!( Natural -> forall (natural: Type) -> forall (succ: natural -> natural) -> forall (zero: natural) -> natural ), - NaturalBuild => dhall::expr!( + NaturalBuild => make_type!( (forall (natural: Type) -> forall (succ: natural -> natural) -> forall (zero: natural) -> natural) -> Natural ), - NaturalIsZero | NaturalEven | NaturalOdd => dhall::expr!( + NaturalIsZero | NaturalEven | NaturalOdd => make_type!( Natural -> Bool ), - NaturalToInteger => dhall::expr!(Natural -> Integer), - NaturalShow => dhall::expr!(Natural -> Text), - NaturalSubtract => dhall::expr!(Natural -> Natural -> Natural), + NaturalToInteger => make_type!(Natural -> Integer), + NaturalShow => make_type!(Natural -> Text), + NaturalSubtract => make_type!(Natural -> Natural -> Natural), - IntegerToDouble => dhall::expr!(Integer -> Double), - IntegerShow => dhall::expr!(Integer -> Text), - DoubleShow => dhall::expr!(Double -> Text), - TextShow => dhall::expr!(Text -> Text), + IntegerToDouble => make_type!(Integer -> Double), + IntegerShow => make_type!(Integer -> Text), + DoubleShow => make_type!(Double -> Text), + TextShow => make_type!(Text -> Text), - ListBuild => dhall::expr!( + ListBuild => make_type!( forall (a: Type) -> (forall (list: Type) -> forall (cons: a -> list -> list) -> @@ -215,28 +270,28 @@ fn type_of_builtin(b: Builtin) -> Expr<X, X> { list) -> List a ), - ListFold => dhall::expr!( + ListFold => make_type!( forall (a: Type) -> - List a -> + (List a) -> forall (list: Type) -> forall (cons: a -> list -> list) -> forall (nil: list) -> list ), - ListLength => dhall::expr!(forall (a: Type) -> List a -> Natural), + ListLength => make_type!(forall (a: Type) -> (List a) -> Natural), ListHead | ListLast => { - dhall::expr!(forall (a: Type) -> List a -> Optional a) + make_type!(forall (a: Type) -> (List a) -> Optional a) } - ListIndexed => dhall::expr!( + ListIndexed => make_type!( forall (a: Type) -> - List a -> + (List a) -> List { index: Natural, value: a } ), - ListReverse => dhall::expr!( - forall (a: Type) -> List a -> List a + ListReverse => make_type!( + forall (a: Type) -> (List a) -> List a ), - OptionalBuild => dhall::expr!( + OptionalBuild => make_type!( forall (a: Type) -> (forall (optional: Type) -> forall (just: a -> optional) -> @@ -244,15 +299,15 @@ fn type_of_builtin(b: Builtin) -> Expr<X, X> { optional) -> Optional a ), - OptionalFold => dhall::expr!( + OptionalFold => make_type!( forall (a: Type) -> - Optional a -> + (Optional a) -> forall (optional: Type) -> forall (just: a -> optional) -> forall (nothing: optional) -> optional ), - OptionalNone => dhall::expr!( + OptionalNone => make_type!( forall (a: Type) -> Optional a ), } diff --git a/dhall/tests/traits.rs b/dhall/tests/traits.rs index 75eaf75..0f75553 100644 --- a/dhall/tests/traits.rs +++ b/dhall/tests/traits.rs @@ -1,23 +1,18 @@ #![feature(proc_macro_hygiene)] -use dhall::de::{StaticType, Type}; -use dhall_proc_macros::subexpr; -use dhall_syntax::{SubExpr, X}; +use dhall::de::{from_str, StaticType, Type}; #[test] fn test_static_type() { - fn mktype(x: SubExpr<X, X>) -> Type { - Type::from_normalized_expr(x) + fn parse(s: &str) -> Type { + from_str(s, None).unwrap() } - assert_eq!(bool::static_type(), mktype(subexpr!(Bool))); - assert_eq!(String::static_type(), mktype(subexpr!(Text))); - assert_eq!( - <Option<bool>>::static_type(), - mktype(subexpr!(Optional Bool)) - ); + assert_eq!(bool::static_type(), parse("Bool")); + assert_eq!(String::static_type(), parse("Text")); + assert_eq!(<Option<bool>>::static_type(), parse("Optional Bool")); assert_eq!( <(bool, Vec<String>)>::static_type(), - mktype(subexpr!({ _1: Bool, _2: List Text })) + parse("{ _1: Bool, _2: List Text }") ); #[derive(dhall::de::StaticType)] @@ -28,7 +23,7 @@ fn test_static_type() { } assert_eq!( <A as dhall::de::StaticType>::static_type(), - mktype(subexpr!({ field1: Bool, field2: Optional Bool })) + parse("{ field1: Bool, field2: Optional Bool }") ); #[derive(StaticType)] @@ -52,7 +47,7 @@ fn test_static_type() { struct D(); assert_eq!( <C<D>>::static_type(), - mktype(subexpr!({ _1: {}, _2: Optional Text })) + parse("{ _1: {}, _2: Optional Text }") ); #[derive(StaticType)] @@ -61,10 +56,7 @@ fn test_static_type() { A(T), B(String), }; - assert_eq!( - <E<bool>>::static_type(), - mktype(subexpr!(< A: Bool | B: Text >)) - ); + assert_eq!(<E<bool>>::static_type(), parse("< A: Bool | B: Text >")); #[derive(StaticType)] #[allow(dead_code)] @@ -72,5 +64,5 @@ fn test_static_type() { A, B(bool), }; - assert_eq!(F::static_type(), mktype(subexpr!(< A | B: Bool >))); + assert_eq!(F::static_type(), parse("< A | B: Bool >")); } diff --git a/dhall_proc_macros/src/lib.rs b/dhall_proc_macros/src/lib.rs index e4aa8b5..5304429 100644 --- a/dhall_proc_macros/src/lib.rs +++ b/dhall_proc_macros/src/lib.rs @@ -6,20 +6,9 @@ extern crate proc_macro; mod derive; -mod quote; use proc_macro::TokenStream; -#[proc_macro] -pub fn expr(input: TokenStream) -> TokenStream { - quote::expr(input) -} - -#[proc_macro] -pub fn subexpr(input: TokenStream) -> TokenStream { - quote::subexpr(input) -} - #[proc_macro_derive(StaticType)] pub fn derive_static_type(input: TokenStream) -> TokenStream { derive::derive_static_type(input) diff --git a/dhall_proc_macros/src/quote.rs b/dhall_proc_macros/src/quote.rs deleted file mode 100644 index 3dbfba9..0000000 --- a/dhall_proc_macros/src/quote.rs +++ /dev/null @@ -1,223 +0,0 @@ -extern crate proc_macro; -use dhall_syntax::context::Context; -use dhall_syntax::*; -use proc_macro2::TokenStream; -use quote::quote; - -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(); - let no_import = - |_: &Import| -> X { panic!("Don't use import in dhall::expr!()") }; - let expr = expr.map_embed(no_import); - let output = quote_expr(expr.as_ref(), &Context::new()); - output.into() -} - -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(); - let no_import = - |_: &Import| -> X { panic!("Don't use import in dhall::subexpr!()") }; - let expr = expr.map_embed(no_import); - let output = quote_subexpr(&expr, &Context::new()); - output.into() -} - -// Returns an expression of type ExprF<T, _>, where T is the -// type of the subexpressions after interpolation. -pub fn quote_exprf<TS>(expr: ExprF<TS, X>) -> TokenStream -where - TS: quote::ToTokens + std::fmt::Debug, -{ - use dhall_syntax::ExprF::*; - match expr { - Var(_) => unreachable!(), - Pi(x, t, b) => { - let x = quote_label(&x); - quote! { dhall_syntax::ExprF::Pi(#x, #t, #b) } - } - Lam(x, t, b) => { - let x = quote_label(&x); - quote! { dhall_syntax::ExprF::Lam(#x, #t, #b) } - } - App(f, a) => { - quote! { dhall_syntax::ExprF::App(#f, #a) } - } - Annot(x, t) => { - quote! { dhall_syntax::ExprF::Annot(#x, #t) } - } - Const(c) => { - let c = quote_const(c); - quote! { dhall_syntax::ExprF::Const(#c) } - } - Builtin(b) => { - let b = quote_builtin(b); - quote! { dhall_syntax::ExprF::Builtin(#b) } - } - BinOp(o, a, b) => { - let o = quote_binop(o); - quote! { dhall_syntax::ExprF::BinOp(#o, #a, #b) } - } - NaturalLit(n) => { - quote! { dhall_syntax::ExprF::NaturalLit(#n) } - } - BoolLit(b) => { - quote! { dhall_syntax::ExprF::BoolLit(#b) } - } - SomeLit(x) => { - quote! { dhall_syntax::ExprF::SomeLit(#x) } - } - EmptyListLit(t) => { - quote! { dhall_syntax::ExprF::EmptyListLit(#t) } - } - NEListLit(es) => { - let es = quote_vec(es); - quote! { dhall_syntax::ExprF::NEListLit(#es) } - } - RecordType(m) => { - let m = quote_map(m); - quote! { dhall_syntax::ExprF::RecordType(#m) } - } - RecordLit(m) => { - let m = quote_map(m); - quote! { dhall_syntax::ExprF::RecordLit(#m) } - } - UnionType(m) => { - let m = quote_opt_map(m); - quote! { dhall_syntax::ExprF::UnionType(#m) } - } - e => unimplemented!("{:?}", e), - } -} - -// Returns an expression of type SubExpr<_, _>. Expects interpolated variables -// to be of type SubExpr<_, _>. -fn quote_subexpr<N>( - expr: &SubExpr<N, 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!(), - ) { - 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::V(#s.into(), #n) }; - rc(quote! { dhall_syntax::ExprF::Var(#var) }) - } - // Free variable; interpolates as a rust variable - None => { - let s: String = s.into(); - // TODO: insert appropriate shifts ? - let v: TokenStream = s.parse().unwrap(); - quote! { { - let x: dhall_syntax::SubExpr<_, _> = #v.clone(); - x - } } - } - } - } - e => rc(quote_exprf(e)), - } -} - -// Returns an expression of type Expr<_, _>. Expects interpolated variables -// to be of type SubExpr<_, _>. -fn quote_expr<N>(expr: &Expr<N, 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!(), - ) { - 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::V(#s.into(), #n) }; - quote! { dhall_syntax::ExprF::Var(#var) } - } - // Free variable; interpolates as a rust variable - None => { - let s: String = s.into(); - // TODO: insert appropriate shifts ? - let v: TokenStream = s.parse().unwrap(); - quote! { { - let x: dhall_syntax::SubExpr<_, _> = #v.clone(); - x.unroll() - } } - } - } - } - e => quote_exprf(e), - } -} - -fn quote_builtin(b: Builtin) -> TokenStream { - format!("::dhall_syntax::Builtin::{:?}", b).parse().unwrap() -} - -fn quote_const(c: Const) -> TokenStream { - format!("::dhall_syntax::Const::{:?}", c).parse().unwrap() -} - -fn quote_binop(b: BinOp) -> TokenStream { - format!("::dhall_syntax::BinOp::{:?}", b).parse().unwrap() -} - -fn quote_label(l: &Label) -> TokenStream { - let l = String::from(l); - quote! { dhall_syntax::Label::from(#l) } -} - -fn rc(x: TokenStream) -> TokenStream { - quote! { ::dhall_syntax::rc(#x) } -} - -fn quote_opt<TS>(x: Option<TS>) -> TokenStream -where - TS: quote::ToTokens + std::fmt::Debug, -{ - match x { - Some(x) => quote!(Some(#x)), - None => quote!(None), - } -} - -fn quote_vec<TS>(e: Vec<TS>) -> TokenStream -where - TS: quote::ToTokens + std::fmt::Debug, -{ - quote! { vec![ #(#e),* ] } -} - -fn quote_map<TS>(m: impl IntoIterator<Item = (Label, TS)>) -> TokenStream -where - TS: quote::ToTokens + std::fmt::Debug, -{ - let entries = m.into_iter().map(|(k, v)| { - let k = quote_label(&k); - quote!(m.insert(#k, #v);) - }); - quote! { { - let mut m = ::dhall_syntax::map::DupTreeMap::new(); - #( #entries )* - m - } } -} - -fn quote_opt_map<TS>( - m: impl IntoIterator<Item = (Label, Option<TS>)>, -) -> TokenStream -where - TS: quote::ToTokens + std::fmt::Debug, -{ - quote_map(m.into_iter().map(|(k, v)| (k, quote_opt(v)))) -} |