diff options
| author | Nadrieril | 2019-12-24 22:08:22 +0000 |
|---|---|---|
| committer | Nadrieril | 2019-12-24 22:08:22 +0000 |
| commit | 12e7626c9fd8c1c1699bc0043b6524704dc6be82 (patch) | |
| tree | 1b42c889c6143131cbe8b3c488afc11450efbdad /dhall/src/semantics | |
| parent | f5a588defc0ad22ce2f0d3b32ef8f0e22e43e672 (diff) | |
Ensure normalization respects var names on the nose
Diffstat (limited to '')
| -rw-r--r-- | dhall/src/semantics/phase/normalize.rs | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 459eaf1..bf0c626 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -24,7 +24,7 @@ macro_rules! make_closure { .into_value_with_type(make_closure!($($ty)*)) }}; // Warning: assumes that $ty, as a dhall value, has type `Type` - (λ($var:ident : $($ty:tt)*) -> $($body:tt)*) => {{ + (λ($var:tt : $($ty:tt)*) -> $($body:tt)*) => {{ let var: AlphaLabel = Label::from(stringify!($var)).into(); let ty = make_closure!($($ty)*); let body = make_closure!($($body)*); @@ -276,12 +276,12 @@ pub(crate) fn apply_builtin( f.app(list_t.clone()) .app({ // Move `t` under new variables - let t1 = t.under_binder(Label::from("x")); - let t2 = t1.under_binder(Label::from("xs")); + let t1 = t.under_binder(Label::from("a")); + let t2 = t1.under_binder(Label::from("as")); make_closure!( - λ(x : #t) -> - λ(xs : List #t1) -> - [ var(x, 1, #t2) ] # var(xs, 0, List #t2) + λ(a : #t) -> + λ(as : List #t1) -> + [ var(a, 1, #t2) ] # var(as, 0, List #t2) ) }) .app(EmptyListLit(t.clone()).into_value_with_type(list_t)), @@ -303,8 +303,8 @@ pub(crate) fn apply_builtin( Ret::Value( f.app(optional_t.clone()) .app({ - let t1 = t.under_binder(Label::from("x")); - make_closure!(λ(x: #t) -> Some(var(x, 0, #t1))) + let t1 = t.under_binder(Label::from("a")); + make_closure!(λ(a: #t) -> Some(var(a, 0, #t1))) }) .app( EmptyOptionalLit(t.clone()) |