From 3c5c6b31d3e35219f907499f094643e1bfba5db2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 9 Mar 2019 23:42:34 +0100 Subject: Considerably simplify typecheck using dhall_expr!() Closes #17 --- dhall/src/typecheck.rs | 146 ++++++++++++++++----------------------------- dhall_generator/src/lib.rs | 84 +++++++++++++++++--------- 2 files changed, 107 insertions(+), 123 deletions(-) diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 2916526..00b8b47 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -9,8 +9,8 @@ use dhall_core::core; use dhall_core::core::Builtin::*; use dhall_core::core::Const::*; use dhall_core::core::Expr::*; -use dhall_core::core::{app, pi}; use dhall_core::core::{bx, shift, subst, Expr, Label, V, X}; +use dhall_generator::dhall_expr; use self::TypeMessage::*; @@ -373,34 +373,24 @@ where Ok(ty) } NaturalLit(_) => Ok(Builtin(Natural)), - Builtin(NaturalFold) => Ok(pi( - "_", - Natural, - pi( - "natural", - Const(Type), - pi( - "succ", - pi("_", "natural", "natural"), - pi("zero", "natural", "natural"), - ), - ), + Builtin(NaturalFold) => Ok(dhall_expr!( + Natural -> + forall (natural: Type) -> + forall (succ: natural -> natural) -> + forall (zero: natural) -> + natural )), - Builtin(NaturalBuild) => Ok(pi( - "_", - pi( - "natural", - Const(Type), - pi( - "succ", - pi("_", "natural", "natural"), - pi("zero", "natural", "natural"), - ), - ), - Natural, + Builtin(NaturalBuild) => Ok(dhall_expr!( + (forall (natural: Type) -> + forall (succ: natural -> natural) -> + forall (zero: natural) -> + natural) -> + Natural )), Builtin(NaturalIsZero) | Builtin(NaturalEven) | Builtin(NaturalOdd) => { - Ok(pi("_", Natural, Bool)) + Ok(dhall_expr!( + Natural -> Bool + )) } BinOp(NaturalPlus, ref l, ref r) => { op2_type(ctx, e, Natural, CantAdd, l, r) @@ -443,62 +433,35 @@ where } Ok(App(bx(Builtin(List)), t)) } - Builtin(ListBuild) => Ok(pi( - "a", - Const(Type), - pi( - "_", - pi( - "list", - Const(Type), - pi( - "cons", - pi("_", "a", pi("_", "list", "list")), - pi("nil", "list", "list"), - ), - ), - app(List, "a"), - ), + Builtin(ListBuild) => Ok(dhall_expr!( + forall (a: Type) -> + (forall (list: Type) -> + forall (cons: a -> list -> list) -> + forall (nil: list) -> + list) -> + List a )), - Builtin(ListFold) => Ok(pi( - "a", - Const(Type), - pi( - "_", - app(List, "a"), - pi( - "list", - Const(Type), - pi( - "cons", - pi("_", "a", pi("_", "list", "list")), - pi("nil", "list", "list"), - ), - ), - ), + Builtin(ListFold) => Ok(dhall_expr!( + forall (a: Type) -> + List a -> + forall (list: Type) -> + forall (cons: a -> list -> list) -> + forall (nil: list) -> + list )), Builtin(ListLength) => { - Ok(pi("a", Const(Type), pi("_", app(List, "a"), Natural))) + Ok(dhall_expr!(forall (a: Type) -> List a -> Natural)) } - Builtin(ListHead) | Builtin(ListLast) => Ok(pi( - "a", - Const(Type), - pi("_", app(List, "a"), app(Optional, "a")), - )), - Builtin(ListIndexed) => { - let mut m: BTreeMap> = BTreeMap::new(); - m.insert("index".into(), Builtin(Natural)); - m.insert("value".into(), Var(V("a".into(), 0))); - Ok(pi( - "a", - Const(Type), - pi("_", app(List, Var(V("a".into(), 0))), app(List, Record(m))), - )) + Builtin(ListHead) | Builtin(ListLast) => { + Ok(dhall_expr!(forall (a: Type) -> List a -> Optional a)) } - Builtin(ListReverse) => Ok(pi( - "a", - Const(Type), - pi("_", app(List, "a"), app(List, "a")), + Builtin(ListIndexed) => Ok(dhall_expr!( + forall (a: Type) -> + List a -> + List { index: Natural, value: a } + )), + Builtin(ListReverse) => Ok(dhall_expr!( + forall (a: Type) -> List a -> List a )), OptionalLit(ref t, ref xs) => { let mut iter = xs.iter(); @@ -535,26 +498,17 @@ where } Ok(App(bx(Builtin(Optional)), t)) } - Builtin(OptionalFold) => Ok(pi( - "a", - Const(Type), - pi( - "_", - app(Optional, "a"), - pi( - "optional", - Const(Type), - pi( - "just", - pi("_", "a", "optional"), - pi("nothing", "optional", "optional"), - ), - ), - ), + Builtin(OptionalFold) => Ok(dhall_expr!( + forall (a: Type) -> + Optional a -> + forall (optional: Type) -> + forall (just: a -> optional) -> + forall (nothing: optional) -> + optional + )), + Builtin(List) | Builtin(Optional) => Ok(dhall_expr!( + Type -> Type )), - Builtin(List) | Builtin(Optional) => { - Ok(pi("_", Const(Type), Const(Type))) - } Builtin(Bool) | Builtin(Natural) | Builtin(Integer) | Builtin(Double) | Builtin(Text) => Ok(Const(Type)), Record(ref kts) => { diff --git a/dhall_generator/src/lib.rs b/dhall_generator/src/lib.rs index 4be3fa0..512df94 100644 --- a/dhall_generator/src/lib.rs +++ b/dhall_generator/src/lib.rs @@ -1,9 +1,9 @@ extern crate proc_macro; use dhall_core::context::Context; use dhall_core::*; -use proc_macro2::Literal; use proc_macro2::TokenStream; use quote::quote; +use std::collections::BTreeMap; #[proc_macro] pub fn dhall_expr(input: proc_macro::TokenStream) -> proc_macro::TokenStream { @@ -28,17 +28,27 @@ fn dhall_to_tokenstream( let v = dhall_to_tokenstream_bx(e, ctx); quote! { *#v } } + Pi(x, t, b) => { + let t = dhall_to_tokenstream_bx(t, ctx); + let b = dhall_to_tokenstream_bx(b, &ctx.insert(x.clone(), ())); + let x = label_to_tokenstream(x); + quote! { Pi(#x, #t, #b) } + } Lam(x, t, b) => { let t = dhall_to_tokenstream_bx(t, ctx); let b = dhall_to_tokenstream_bx(b, &ctx.insert(x.clone(), ())); - let x = Literal::string(&String::from(x.clone())); - quote! { Lam(#x.into(), #t, #b) } + let x = label_to_tokenstream(x); + quote! { Lam(#x, #t, #b) } } App(f, a) => { let f = dhall_to_tokenstream_bx(f, ctx); let a = dhall_to_tokenstream_bx(a, ctx); quote! { App(#f, #a) } } + Const(c) => { + let c = const_to_tokenstream(*c); + quote! { Const(#c) } + } Builtin(b) => { let b = builtin_to_tokenstream(*b); quote! { Builtin(#b) } @@ -50,23 +60,19 @@ fn dhall_to_tokenstream( quote! { BinOp(#o, #a, #b) } } OptionalLit(t, es) => { - let t = option_tks( - t.as_ref() - .map(deref) - .map(|x| dhall_to_tokenstream_bx(x, ctx)), - ); - let es = vec_tks(es.iter().map(|x| dhall_to_tokenstream(x, ctx))); + let t = option_to_tokenstream(t, ctx); + let es = vec_to_tokenstream(es, ctx); quote! { OptionalLit(#t, #es) } } ListLit(t, es) => { - let t = option_tks( - t.as_ref() - .map(deref) - .map(|x| dhall_to_tokenstream_bx(x, ctx)), - ); - let es = vec_tks(es.iter().map(|x| dhall_to_tokenstream(x, ctx))); + let t = option_to_tokenstream(t, ctx); + let es = vec_to_tokenstream(es, ctx); quote! { ListLit(#t, #es) } } + Record(m) => { + let m = map_to_tokenstream(m, ctx); + quote! { Record(#m) } + } e => unimplemented!("{:?}", e), } } @@ -105,29 +111,53 @@ fn builtin_to_tokenstream(b: Builtin) -> TokenStream { format!("{:?}", b).parse().unwrap() } +fn const_to_tokenstream(c: Const) -> TokenStream { + format!("{:?}", c).parse().unwrap() +} + fn binop_to_tokenstream(b: BinOp) -> TokenStream { format!("{:?}", b).parse().unwrap() } -#[allow(clippy::borrowed_box)] -fn deref(x: &Box) -> &T { - &*x +fn label_to_tokenstream(l: &Label) -> TokenStream { + let l = String::from(l.clone()); + quote! { #l.into() } } -fn bx(x: TokenStream) -> TokenStream { - quote! { bx(#x) } +fn map_to_tokenstream( + m: &BTreeMap>, + ctx: &Context, +) -> TokenStream { + let (keys, values): (Vec, Vec) = m + .iter() + .map(|(k, v)| (label_to_tokenstream(k), dhall_to_tokenstream(v, ctx))) + .unzip(); + quote! { { + let mut m = BTreeMap::new(); + #( m.insert(#keys, #values); )* + m + } } } -fn option_tks(x: Option) -> TokenStream { - match x { +fn option_to_tokenstream( + e: &Option>>, + ctx: &Context, +) -> TokenStream { + let e = e.as_ref().map(|x| dhall_to_tokenstream_bx(x, ctx)); + match e { Some(x) => quote! { Some(#x) }, None => quote! { None }, } } -fn vec_tks(x: T) -> TokenStream -where - T: Iterator, -{ - quote! { vec![ #(#x),* ] } +fn vec_to_tokenstream( + e: &Vec>, + ctx: &Context, +) -> TokenStream { + let e = e.iter().map(|x| dhall_to_tokenstream(x, ctx)); + quote! { vec![ #(#e),* ] } +} + +fn bx(x: TokenStream) -> TokenStream { + quote! { bx(#x) } } -- cgit v1.2.3