diff options
| -rw-r--r-- | dhall/src/typecheck.rs | 2 | ||||
| -rw-r--r-- | dhall_core/src/core.rs | 24 | ||||
| -rw-r--r-- | dhall_core/src/printer.rs | 2 | ||||
| -rw-r--r-- | dhall_generator/src/dhall_expr.rs | 13 |
4 files changed, 23 insertions, 18 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 31702db..da52ba8 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -28,7 +28,7 @@ fn rule(a: Const, b: Const) -> Result<Const, ()> { } } -fn match_vars(vl: &V, vr: &V, ctx: &[(Label, Label)]) -> bool { +fn match_vars(vl: &V<Label>, vr: &V<Label>, ctx: &[(Label, Label)]) -> bool { let mut vl = vl.clone(); let mut vr = vr.clone(); let mut ctx = ctx.to_vec(); diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs index 456a68c..5ac3db6 100644 --- a/dhall_core/src/core.rs +++ b/dhall_core/src/core.rs @@ -100,7 +100,7 @@ pub enum Const { /// appear as a numeric suffix. /// #[derive(Debug, Clone, PartialEq, Eq)] -pub struct V(pub Label, pub usize); +pub struct V<Label>(pub Label, pub usize); // Definition order must match precedence order for // pretty-printing to work correctly @@ -173,19 +173,19 @@ pub type DhallExpr = ResolvedExpr; #[derive(Debug, PartialEq, Eq)] pub struct SubExpr<Note, Embed>(pub Rc<Expr<Note, Embed>>); -pub type Expr<Note, Embed> = ExprF<SubExpr<Note, Embed>, Note, Embed>; +pub type Expr<Note, Embed> = ExprF<SubExpr<Note, Embed>, Label, Note, Embed>; /// Syntax tree for expressions // Having the recursion out of the enum definition enables writing // much more generic code and improves pattern-matching behind // smart pointers. #[derive(Debug, Clone, PartialEq, Eq)] -pub enum ExprF<SubExpr, Note, Embed> { +pub enum ExprF<SubExpr, Label, Note, Embed> { /// `Const c ~ c` Const(Const), /// `Var (V x 0) ~ x`<br> /// `Var (V x n) ~ x@n` - Var(V), + Var(V<Label>), /// `Lam x A b ~ λ(x : A) -> b` Lam(Label, SubExpr, SubExpr), /// `Pi "_" A B ~ A -> B` @@ -337,22 +337,24 @@ fn add_ui(u: usize, i: isize) -> usize { } /// Map over the immediate children of the passed Expr -pub fn map_subexpr<SE1, SE2, S, T, A, B, F1, F2, F3, F4, F5>( - e: &ExprF<SE1, S, A>, +pub fn map_subexpr<SE1, SE2, L1, L2, S, T, A, B, F1, F2, F3, F4, F5>( + e: &ExprF<SE1, L1, S, A>, map: F1, map_note: F2, map_embed: F3, map_label: F4, map_under_binder: F5, -) -> ExprF<SE2, T, B> +) -> ExprF<SE2, L2, T, B> where + L1: Ord, + L2: Ord, SE1: Clone, SE2: Clone, F1: Fn(&SE1) -> SE2, F2: FnOnce(&S) -> T, F3: FnOnce(&A) -> B, - F4: Fn(&Label) -> Label, - F5: FnOnce(&Label, &SE1) -> SE2, + F4: Fn(&L1) -> L2, + F5: FnOnce(&L1, &SE1) -> SE2, { use crate::ExprF::*; let map = ↦ @@ -505,7 +507,7 @@ where /// pub fn shift<S, A>( delta: isize, - var: &V, + var: &V<Label>, in_expr: &SubExpr<S, A>, ) -> SubExpr<S, A> { use crate::ExprF::*; @@ -534,7 +536,7 @@ pub fn shift<S, A>( /// ``` /// pub fn subst<S, A>( - var: &V, + var: &V<Label>, value: &SubExpr<S, A>, in_expr: &SubExpr<S, A>, ) -> SubExpr<S, A> { diff --git a/dhall_core/src/printer.rs b/dhall_core/src/printer.rs index fb3b8e8..746b863 100644 --- a/dhall_core/src/printer.rs +++ b/dhall_core/src/printer.rs @@ -462,7 +462,7 @@ impl Display for Scheme { } } -impl Display for V { +impl<Label: Display> Display for V<Label> { fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { let V(x, n) = self; x.fmt(f)?; diff --git a/dhall_generator/src/dhall_expr.rs b/dhall_generator/src/dhall_expr.rs index 96201e8..b057850 100644 --- a/dhall_generator/src/dhall_expr.rs +++ b/dhall_generator/src/dhall_expr.rs @@ -17,17 +17,20 @@ pub fn dhall_expr(input: proc_macro::TokenStream) -> proc_macro::TokenStream { // Returns an expression of type ExprF<T, _, _>, where T is the // type of the subexpressions after interpolation. -pub fn quote_expr<TS>(expr: ExprF<TS, X, X>) -> TokenStream +pub fn quote_expr<TS>(expr: ExprF<TS, Label, X, X>) -> TokenStream where TS: quote::ToTokens + std::fmt::Debug, { let quote_map = |m: BTreeMap<Label, TS>| -> TokenStream { - let (keys, values): (Vec<TokenStream>, Vec<TS>) = - m.into_iter().map(|(k, v)| (quote_label(&k), v)).unzip(); + let entries = + m.into_iter().map(|(k, v)| { + let k = quote_label(&k); + quote!(m.insert(#k, #v);) + }); quote! { { use std::collections::BTreeMap; let mut m = BTreeMap::new(); - #( m.insert(#keys, #values); )* + #( #entries )* m } } }; @@ -151,7 +154,7 @@ fn quote_binop(b: BinOp) -> TokenStream { fn quote_label(l: &Label) -> TokenStream { let l = String::from(l); - quote! { #l.into() } + quote! { dhall_core::Label::from(#l) } } fn bx(x: TokenStream) -> TokenStream { |