From 38df819817c6697381ed3feeec43327628529f81 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 1 Jan 2019 23:58:41 +0100 Subject: [PATCH] fix(library/init/lean/expander): all identifiers in terms should be `ident_univs` --- library/init/lean/elaborator.lean | 1 - library/init/lean/expander.lean | 24 +++++++++++++----------- library/init/lean/parser/term.lean | 3 --- 3 files changed, 13 insertions(+), 15 deletions(-) diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean index cd23ff4f50..49651ab7e5 100644 --- a/library/init/lean/elaborator.lean +++ b/library/init/lean/elaborator.lean @@ -185,7 +185,6 @@ expr.mdata (kvmap.set_name {} `annotation `anonymous_constructor) e def dummy : expr := expr.const `Prop [] def to_pexpr : syntax → elaborator_m expr -| (syntax.ident id) := pure $ expr.const (mangle_ident id) [] | stx@(syntax.raw_node {kind := k, args := args}) := (match k with | @ident_univs := (match view ident_univs stx with | {id := id, univs := some univs} := expr.const (mangle_ident id) <$> univs.levels.mmap to_level diff --git a/library/init/lean/expander.lean b/library/init/lean/expander.lean index d3ab49953d..1bdf3dd38f 100644 --- a/library/init/lean/expander.lean +++ b/library/init/lean/expander.lean @@ -53,8 +53,10 @@ instance coe_name_ident : has_coe name syntax_ident := /-- Create an identifier preresolved against a global binding. Because we cannot use syntax quotations yet, which the expander would have preresolved against the global context at macro declaration time, we have to do the preresolution manually instead. -/ -def glob_id (n : name) : syntax_ident := -{val := n, raw_val := substring.of_string n.to_string, preresolved := [n]} +def glob_id (n : name) : syntax := +review ident_univs { + id :={val := n, raw_val := substring.of_string n.to_string, preresolved := [n]}, +} instance coe_ident_ident_univs : has_coe syntax_ident ident_univs.view := ⟨λ id, {id := id}⟩ @@ -240,9 +242,9 @@ def expand_bracketed_binder : bracketed_binder.view → transform_m (list simple let type := get_opt_type bc.type, type ← match bc.default with | none := pure type - | some (binder_default.view.val bdv) := pure $ mk_capp (glob_id `opt_param) [type, bdv.term] + | some (binder_default.view.val bdv) := pure $ mk_app (glob_id `opt_param) [type, bdv.term] | some bdv@(binder_default.view.tac bdt) := match bc.type with - | none := pure $ mk_capp (glob_id `auto_param) [bdt.term] + | none := pure $ mk_app (glob_id `auto_param) [bdt.term] | some _ := error (review binder_default bdv) "unexpected auto param after type annotation", pure $ bc.ids.map (λ bid, mk_simple_binder (binder_ident_to_ident bid) bi type) @@ -307,12 +309,12 @@ def paren.transform : transformer := λ stx, do let v := view paren stx, match v.content with - | none := pure $ syntax.ident (glob_id `unit.star) + | none := pure $ glob_id `unit.star | some {term := t, special := none} := pure t | some {term := t, special := paren_special.view.tuple tup} := - pure $ some $ (tup.tail.map sep_by.elem.view.item).foldr (λ t tup, mk_capp (glob_id `prod.mk) [t, tup]) t + pure $ some $ (tup.tail.map sep_by.elem.view.item).foldr (λ t tup, mk_app (glob_id `prod.mk) [t, tup]) t | some {term := t, special := paren_special.view.typed pst} := - pure $ mk_capp (glob_id `typed_expr) [pst.type, t] + pure $ mk_app (glob_id `typed_expr) [pst.type, t] def assume.transform : transformer := λ stx, do @@ -328,10 +330,10 @@ def if.transform : transformer := λ stx, do let v := view «if» stx, pure $ match v.id with - | some id := mk_capp (glob_id `dite) [v.prop, + | some id := mk_app (glob_id `dite) [v.prop, review lambda {binders := binders.view.simple $ simple_binder.view.explicit {id := id.id, type := v.prop}, body := v.then_branch}, - review lambda {binders := binders.view.simple $ simple_binder.view.explicit {id := id.id, type := mk_capp (glob_id `not) [v.prop]}, body := v.else_branch}] - | none := mk_capp (glob_id `ite) [v.prop, v.then_branch, v.else_branch] + review lambda {binders := binders.view.simple $ simple_binder.view.explicit {id := id.id, type := mk_app (glob_id `not) [v.prop]}, body := v.else_branch}] + | none := mk_app (glob_id `ite) [v.prop, v.then_branch, v.else_branch] def let.transform : transformer := λ stx, do @@ -379,7 +381,7 @@ def level.leading.transform : transformer := def subtype.transform : transformer := λ stx, do let v := view term.subtype stx, - pure $ mk_capp (glob_id `subtype) [review lambda { + pure $ mk_app (glob_id `subtype) [review lambda { binders := mk_simple_binder v.id binder_info.default $ get_opt_type v.type, body := v.prop }] diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean index 8dfa76f7c2..a4100eec6e 100644 --- a/library/init/lean/parser/term.lean +++ b/library/init/lean/parser/term.lean @@ -375,9 +375,6 @@ node! app [fn: get_leading, arg: term.parser max_prec] def mk_app (fn : syntax) (args : list syntax) : syntax := args.foldl (λ fn arg, syntax.mk_node app [fn, arg]) fn -def mk_capp (fn : syntax_ident) (args : list syntax) : syntax := -mk_app (syntax.ident fn) args - @[derive parser.has_tokens parser.has_view] def arrow.parser : trailing_term_parser := node! arrow [dom: get_leading, op: unicode_symbol "→" "->" 25, range: term.parser 24]