summaryrefslogtreecommitdiff
path: root/dhall_generator
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall_generator/src/dhall_expr.rs168
-rw-r--r--dhall_generator/src/lib.rs166
2 files changed, 171 insertions, 163 deletions
diff --git a/dhall_generator/src/dhall_expr.rs b/dhall_generator/src/dhall_expr.rs
new file mode 100644
index 0000000..07873bd
--- /dev/null
+++ b/dhall_generator/src/dhall_expr.rs
@@ -0,0 +1,168 @@
+extern crate proc_macro;
+use dhall_core::context::Context;
+use dhall_core::*;
+use proc_macro2::TokenStream;
+use quote::quote;
+use std::collections::BTreeMap;
+use std::rc::Rc;
+
+pub fn dhall_expr(input: proc_macro::TokenStream) -> proc_macro::TokenStream {
+ let input_str = input.to_string();
+ let expr: SubExpr<X, Import> = parse_expr(&input_str).unwrap();
+ let no_import =
+ |_: &Import| -> X { panic!("Don't use import in dhall!()") };
+ let expr = rc(expr.map_embed(&no_import));
+ let output = dhall_to_tokenstream_bx(&expr, &Context::new());
+ output.into()
+}
+
+// Returns an expression of type Expr<_, _>. Expects interpolated variables
+// to be of type Rc<Expr<_, _>>.
+fn dhall_to_tokenstream(
+ expr: &DhallExpr,
+ ctx: &Context<Label, ()>,
+) -> TokenStream {
+ use dhall_core::Expr::*;
+ match expr.as_ref() {
+ Var(_) => {
+ let v = dhall_to_tokenstream_bx(expr, 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 = label_to_tokenstream(x);
+ quote! { Lam(#x, #t, #b) }
+ }
+ App(f, a) => {
+ let f = dhall_to_tokenstream_bx(f, ctx);
+ let a = vec_to_tokenstream(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) }
+ }
+ BinOp(o, a, b) => {
+ let o = binop_to_tokenstream(*o);
+ let a = dhall_to_tokenstream_bx(a, ctx);
+ let b = dhall_to_tokenstream_bx(b, ctx);
+ quote! { BinOp(#o, #a, #b) }
+ }
+ NaturalLit(n) => {
+ quote! { NaturalLit(#n) }
+ }
+ EmptyOptionalLit(x) => {
+ let x = dhall_to_tokenstream_bx(x, ctx);
+ quote! { EmptyOptionalLit(#x) }
+ }
+ NEOptionalLit(x) => {
+ let x = dhall_to_tokenstream_bx(x, ctx);
+ quote! { NEOptionalLit(#x) }
+ }
+ EmptyListLit(t) => {
+ let t = dhall_to_tokenstream_bx(t, ctx);
+ quote! { EmptyListLit(#t) }
+ }
+ NEListLit(es) => {
+ let es = vec_to_tokenstream(es, ctx);
+ quote! { NEListLit(#es) }
+ }
+ RecordType(m) => {
+ let m = map_to_tokenstream(m, ctx);
+ quote! { RecordType(#m) }
+ }
+ RecordLit(m) => {
+ let m = map_to_tokenstream(m, ctx);
+ quote! { RecordLit(#m) }
+ }
+ e => unimplemented!("{:?}", e),
+ }
+}
+
+// Returns an expression of type Rc<Expr<_, _>>
+fn dhall_to_tokenstream_bx(
+ expr: &DhallExpr,
+ ctx: &Context<Label, ()>,
+) -> TokenStream {
+ use dhall_core::Expr::*;
+ match expr.as_ref() {
+ Var(V(s, n)) => {
+ match ctx.lookup(&s, *n) {
+ // Non-free variable; interpolates as itself
+ Some(()) => {
+ let s: String = s.into();
+ quote! { bx(Var(V(#s.into(), #n))) }
+ }
+ // 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: Rc<Expr<_, _>> = #v.clone();
+ x
+ } }
+ }
+ }
+ }
+ _ => bx(dhall_to_tokenstream(expr, ctx)),
+ }
+}
+
+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()
+}
+
+fn label_to_tokenstream(l: &Label) -> TokenStream {
+ let l = String::from(l);
+ quote! { #l.into() }
+}
+
+fn map_to_tokenstream(
+ m: &BTreeMap<Label, Rc<Expr<X, X>>>,
+ ctx: &Context<Label, ()>,
+) -> TokenStream {
+ let (keys, values): (Vec<TokenStream>, Vec<TokenStream>) = m
+ .iter()
+ .map(|(k, v)| {
+ (label_to_tokenstream(k), dhall_to_tokenstream_bx(&*v, ctx))
+ })
+ .unzip();
+ quote! { {
+ use std::collections::BTreeMap;
+ let mut m = BTreeMap::new();
+ #( m.insert(#keys, #values); )*
+ m
+ } }
+}
+
+fn vec_to_tokenstream(
+ e: &Vec<DhallExpr>,
+ ctx: &Context<Label, ()>,
+) -> TokenStream {
+ let e = e.iter().map(|x| dhall_to_tokenstream_bx(x, ctx));
+ quote! { vec![ #(#e),* ] }
+}
+
+fn bx(x: TokenStream) -> TokenStream {
+ quote! { bx(#x) }
+}
diff --git a/dhall_generator/src/lib.rs b/dhall_generator/src/lib.rs
index ee9af5e..7d3304b 100644
--- a/dhall_generator/src/lib.rs
+++ b/dhall_generator/src/lib.rs
@@ -1,169 +1,9 @@
extern crate proc_macro;
-use dhall_core::context::Context;
-use dhall_core::*;
-use proc_macro2::TokenStream;
-use quote::quote;
-use std::collections::BTreeMap;
-use std::rc::Rc;
+
+mod dhall_expr;
#[proc_macro]
pub fn dhall_expr(input: proc_macro::TokenStream) -> proc_macro::TokenStream {
- let input_str = input.to_string();
- let expr: Rc<Expr<X, Import>> = parse_expr(&input_str).unwrap();
- let no_import =
- |_: &Import| -> X { panic!("Don't use import in dhall!()") };
- let expr = rc(expr.map_embed(&no_import));
- let output = dhall_to_tokenstream_bx(&expr, &Context::new());
- output.into()
-}
-
-// Returns an expression of type Expr<_, _>. Expects interpolated variables
-// to be of type Rc<Expr<_, _>>.
-fn dhall_to_tokenstream(
- expr: &DhallExpr,
- ctx: &Context<Label, ()>,
-) -> TokenStream {
- use dhall_core::Expr::*;
- match expr.as_ref() {
- Var(_) => {
- let v = dhall_to_tokenstream_bx(expr, 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 = label_to_tokenstream(x);
- quote! { Lam(#x, #t, #b) }
- }
- App(f, a) => {
- let f = dhall_to_tokenstream_bx(f, ctx);
- let a = vec_to_tokenstream(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) }
- }
- BinOp(o, a, b) => {
- let o = binop_to_tokenstream(*o);
- let a = dhall_to_tokenstream_bx(a, ctx);
- let b = dhall_to_tokenstream_bx(b, ctx);
- quote! { BinOp(#o, #a, #b) }
- }
- NaturalLit(n) => {
- quote! { NaturalLit(#n) }
- }
- EmptyOptionalLit(x) => {
- let x = dhall_to_tokenstream_bx(x, ctx);
- quote! { EmptyOptionalLit(#x) }
- }
- NEOptionalLit(x) => {
- let x = dhall_to_tokenstream_bx(x, ctx);
- quote! { NEOptionalLit(#x) }
- }
- EmptyListLit(t) => {
- let t = dhall_to_tokenstream_bx(t, ctx);
- quote! { EmptyListLit(#t) }
- }
- NEListLit(es) => {
- let es = vec_to_tokenstream(es, ctx);
- quote! { NEListLit(#es) }
- }
- RecordType(m) => {
- let m = map_to_tokenstream(m, ctx);
- quote! { RecordType(#m) }
- }
- RecordLit(m) => {
- let m = map_to_tokenstream(m, ctx);
- quote! { RecordLit(#m) }
- }
- e => unimplemented!("{:?}", e),
- }
-}
-
-// Returns an expression of type Rc<Expr<_, _>>
-fn dhall_to_tokenstream_bx(
- expr: &DhallExpr,
- ctx: &Context<Label, ()>,
-) -> TokenStream {
- use dhall_core::Expr::*;
- match expr.as_ref() {
- Var(V(s, n)) => {
- match ctx.lookup(&s, *n) {
- // Non-free variable; interpolates as itself
- Some(()) => {
- let s: String = s.into();
- quote! { bx(Var(V(#s.into(), #n))) }
- }
- // 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: Rc<Expr<_, _>> = #v.clone();
- x
- } }
- }
- }
- }
- _ => bx(dhall_to_tokenstream(expr, ctx)),
- }
-}
-
-fn builtin_to_tokenstream(b: Builtin) -> TokenStream {
- format!("{:?}", b).parse().unwrap()
-}
-
-fn const_to_tokenstream(c: Const) -> TokenStream {
- format!("{:?}", c).parse().unwrap()
+ dhall_expr::dhall_expr(input)
}
-fn binop_to_tokenstream(b: BinOp) -> TokenStream {
- format!("{:?}", b).parse().unwrap()
-}
-
-fn label_to_tokenstream(l: &Label) -> TokenStream {
- let l = String::from(l);
- quote! { #l.into() }
-}
-
-fn map_to_tokenstream(
- m: &BTreeMap<Label, Rc<Expr<X, X>>>,
- ctx: &Context<Label, ()>,
-) -> TokenStream {
- let (keys, values): (Vec<TokenStream>, Vec<TokenStream>) = m
- .iter()
- .map(|(k, v)| {
- (label_to_tokenstream(k), dhall_to_tokenstream_bx(&*v, ctx))
- })
- .unzip();
- quote! { {
- use std::collections::BTreeMap;
- let mut m = BTreeMap::new();
- #( m.insert(#keys, #values); )*
- m
- } }
-}
-
-fn vec_to_tokenstream(
- e: &Vec<DhallExpr>,
- ctx: &Context<Label, ()>,
-) -> TokenStream {
- let e = e.iter().map(|x| dhall_to_tokenstream_bx(x, ctx));
- quote! { vec![ #(#e),* ] }
-}
-
-fn bx(x: TokenStream) -> TokenStream {
- quote! { bx(#x) }
-}
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-04 15:58:20 +0000