diff options
Diffstat (limited to '')
| -rw-r--r-- | Cargo.lock | 11 | ||||
| -rw-r--r-- | dhall_generator/Cargo.toml | 15 | ||||
| -rw-r--r-- | dhall_generator/src/lib.rs | 87 | ||||
| -rw-r--r-- | dhall_normalize/Cargo.toml | 1 | ||||
| -rw-r--r-- | dhall_normalize/src/lib.rs | 1 | ||||
| -rw-r--r-- | dhall_normalize/src/normalize.rs | 10 |
6 files changed, 120 insertions, 5 deletions
@@ -157,11 +157,22 @@ dependencies = [ ] [[package]] +name = "dhall_generator" +version = "0.1.0" +dependencies = [ + "dhall_core 0.1.0", + "itertools 0.8.0 (registry+https://github.com/rust-lang/crates.io-index)", + "proc-macro2 0.4.27 (registry+https://github.com/rust-lang/crates.io-index)", + "quote 0.6.11 (registry+https://github.com/rust-lang/crates.io-index)", +] + +[[package]] name = "dhall_normalize" version = "0.1.0" dependencies = [ "bytecount 0.5.1 (registry+https://github.com/rust-lang/crates.io-index)", "dhall_core 0.1.0", + "dhall_generator 0.1.0", "itertools 0.8.0 (registry+https://github.com/rust-lang/crates.io-index)", "lalrpop-util 0.16.3 (registry+https://github.com/rust-lang/crates.io-index)", "nom 3.2.1 (registry+https://github.com/rust-lang/crates.io-index)", diff --git a/dhall_generator/Cargo.toml b/dhall_generator/Cargo.toml new file mode 100644 index 0000000..ada6707 --- /dev/null +++ b/dhall_generator/Cargo.toml @@ -0,0 +1,15 @@ +[package] +name = "dhall_generator" +version = "0.1.0" +authors = ["Nadrieril <nadrieril@users.noreply.github.com>"] +edition = "2018" + +[lib] +proc-macro = true +doctest = false + +[dependencies] +itertools = "0.8.0" +quote = "0.6.11" +proc-macro2 = "0.4.27" +dhall_core = { path = "../dhall_core" } diff --git a/dhall_generator/src/lib.rs b/dhall_generator/src/lib.rs new file mode 100644 index 0000000..85f9ce2 --- /dev/null +++ b/dhall_generator/src/lib.rs @@ -0,0 +1,87 @@ +extern crate proc_macro; +use proc_macro2::TokenStream; +use proc_macro2::Literal; +use quote::quote; +use dhall_core::*; + +#[proc_macro] +pub fn dhall(input: proc_macro::TokenStream) -> proc_macro::TokenStream { + let input_str = input.to_string(); + let expr = parser::parse_expr_pest(&input_str).unwrap(); + let output = dhall_to_tokenstream(&expr); + output.into() +} + +// Returns an expression of type Expr<_, _>. Expects input variables +// to be of type Box<Expr<_, _>> (future-proof for structural sharing). +fn dhall_to_tokenstream(expr: &Expr<X, X>) -> TokenStream { + use dhall_core::Expr::*; + match expr { + Var(V(s, _)) => { + let v: TokenStream = s.parse().unwrap(); + quote!{ (*#v).clone() } + }, + Lam(x, ref t, ref b) => { + let x = Literal::string(x); + let t = dhall_to_tokenstream_bx(t); + let b = dhall_to_tokenstream_bx(b); + quote!{ Lam(#x, #t, #b) } + } + App(ref f, ref a) => { + let f = dhall_to_tokenstream_bx(f); + let a = dhall_to_tokenstream_bx(a); + quote!{ App(#f, #a) } + } + Builtin(ref b) => { + let b = builtin_to_tokenstream(b); + quote!{ Builtin(#b) } + }, + OptionalLit(ref t, ref es) => { + let t = option_tks(t.as_ref().map(deref).map(dhall_to_tokenstream_bx)); + let es = vec_tks(es.into_iter().map(dhall_to_tokenstream)); + quote!{ OptionalLit(#t, #es) } + } + e => unimplemented!("{:?}", e), + } +} + +// Returns an expression of type Box<Expr<_, _>> +fn dhall_to_tokenstream_bx(expr: &Expr<X, X>) -> TokenStream { + use dhall_core::Expr::*; + match expr { + Var(V(s, _)) => { + let v: TokenStream = s.parse().unwrap(); + quote!{ #v.clone() } + }, + e => bx(dhall_to_tokenstream(e)), + } +} + +fn builtin_to_tokenstream(b: &Builtin) -> TokenStream { + use dhall_core::Builtin::*; + match b { + Optional => quote!{ Optional }, + b => unimplemented!("{:?}", b), + } +} + +fn deref<T>(x: &Box<T>) -> &T { + &*x +} + +fn bx(x: TokenStream) -> TokenStream { + quote!{ bx(#x) } +} + +fn option_tks(x: Option<TokenStream>) -> TokenStream { + match x { + Some(x) => quote!{ Some(#x) }, + None => quote!{ None }, + } +} + +fn vec_tks<T>(x: T) -> TokenStream +where T: Iterator<Item=TokenStream> +{ + quote!{ vec![ #(#x),* ] } +} diff --git a/dhall_normalize/Cargo.toml b/dhall_normalize/Cargo.toml index 3affee8..ad1cc0d 100644 --- a/dhall_normalize/Cargo.toml +++ b/dhall_normalize/Cargo.toml @@ -15,3 +15,4 @@ nom = "3.0.0" term-painter = "0.2.3" pest = { git = "https://github.com/pest-parser/pest" } dhall_core = { path = "../dhall_core" } +dhall_generator = { path = "../dhall_generator" } diff --git a/dhall_normalize/src/lib.rs b/dhall_normalize/src/lib.rs index a2f7041..df49146 100644 --- a/dhall_normalize/src/lib.rs +++ b/dhall_normalize/src/lib.rs @@ -1,5 +1,6 @@ #![feature(box_patterns)] #![feature(trace_macros)] +#![feature(proc_macro_hygiene)] mod normalize; pub use crate::normalize::*; diff --git a/dhall_normalize/src/normalize.rs b/dhall_normalize/src/normalize.rs index 1fa5524..3b87419 100644 --- a/dhall_normalize/src/normalize.rs +++ b/dhall_normalize/src/normalize.rs @@ -1,6 +1,7 @@ #![allow(non_snake_case)] use std::fmt; use dhall_core::core::*; +use dhall_generator::dhall; /// Reduce an expression to its normal form, performing beta reduction /// @@ -158,11 +159,10 @@ where normalize(&b) } (App(box Builtin(OptionalBuild), a0), g) => { - let e2: Expr<_, _> = app(app(app(g, - App(bx(Builtin(Optional)), a0.clone())), - Lam("x", a0.clone(), - bx(OptionalLit(Some(a0.clone()), vec![Var(V("x", 0))])))), - OptionalLit(Some(a0), vec![])); + let x = bx(Var(V("x", 0))); + let g = bx(g); + let e2: Expr<_, _> = + dhall!((g (Optional a0)) (λ(x: a0) -> [x] : Optional a0) ([] : Optional a0)); normalize(&e2) } (f2, a2) => app(f2, a2), |