summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Cargo.lock11
-rw-r--r--dhall_generator/Cargo.toml15
-rw-r--r--dhall_generator/src/lib.rs87
-rw-r--r--dhall_normalize/Cargo.toml1
-rw-r--r--dhall_normalize/src/lib.rs1
-rw-r--r--dhall_normalize/src/normalize.rs10
6 files changed, 120 insertions, 5 deletions
diff --git a/Cargo.lock b/Cargo.lock
index 57ad661..f15b230 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -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),