diff --git a/library/init/data/rbmap/basic.lean b/library/init/data/rbmap/basic.lean index 5b44754ac8..7b716454ef 100644 --- a/library/init/data/rbmap/basic.lean +++ b/library/init/data/rbmap/basic.lean @@ -90,6 +90,10 @@ def contains (m : rbmap α β lt) (k : α) : bool := def from_list (l : list (α × β)) (lt : α → α → Prop) [decidable_rel lt] : rbmap α β lt := l.foldl (λ m p, insert m p.1 p.2) (mk_rbmap α β lt) +-- TODO: replace with more efficient, structure-preserving implementation (needs wf proof) +def map (f : α → β → δ) (m : rbmap α β lt) : rbmap α δ lt := +m.fold (λ a b m, rbmap.insert m a (f a b)) (mk_rbmap α δ lt) + end rbmap def rbmap_of {α : Type u} {β : Type v} (l : list (α × β)) (lt : α → α → Prop) [decidable_rel lt] : rbmap α β lt := diff --git a/library/init/lean/name.lean b/library/init/lean/name.lean index 4f7ca34e16..de9f79d4ae 100644 --- a/library/init/lean/name.lean +++ b/library/init/lean/name.lean @@ -72,6 +72,20 @@ instance has_decidable_eq : decidable_eq name | (mk_numeral _ _) anonymous := is_false $ λ h, name.no_confusion h | (mk_numeral _ _) (mk_string _ _) := is_false $ λ h, name.no_confusion h +def replace_prefix : name → name → name → name +| anonymous anonymous new_p := new_p +| anonymous _ _ := anonymous +| n@(mk_string p s) query_p new_p := + if n = query_p then + new_p + else + mk_string (p.replace_prefix query_p new_p) s +| n@(mk_numeral p s) query_p new_p := + if n = query_p then + new_p + else + mk_numeral (p.replace_prefix query_p new_p) s + @[simp] def quick_lt : name → name → bool | anonymous anonymous := ff | anonymous _ := tt diff --git a/library/init/lean/parser/macro.lean b/library/init/lean/parser/macro.lean index 8780b5bd44..c8015912b3 100644 --- a/library/init/lean/parser/macro.lean +++ b/library/init/lean/parser/macro.lean @@ -33,27 +33,9 @@ def run' {r σ α} (cfg : r) (st : σ): parse_m r σ α → except string α := λ x, prod.fst $ parse_m.run cfg st x end parse_m -structure resolved := --- local or (overloaded) global -(decl : syntax_id ⊕ list name) -/- prefix of the reference that corresponds to the decl. All trailing name components - are field accesses. -/ -(«prefix» : name) - -instance resolved.has_to_format : has_to_format resolved := ⟨λ r, to_fmt (r.decl, r.prefix)⟩ - structure resolve_cfg := (global_scope : rbmap name syntax (<)) -@[reducible] def resolve_map := rbmap syntax_id resolved (<) - -structure resolve_state := -(resolve_map : resolve_map) - -def scope := rbmap (name × option macro_scope_id) syntax_id (<) - -@[reducible] def resolve_m := parse_m resolve_cfg resolve_state - def exp_fuel := 1000 structure macro := @@ -61,7 +43,6 @@ structure macro := -- (read : reader) -- TODO: What else does an expander need? How to model recursive expansion? (expand : option (syntax_node syntax → syntax) := none) -(resolve : option (scope → syntax_node syntax → resolve_m (list scope)) := none) -- (elaborate : list syntax → expr → tactic expr) structure parse_state := @@ -95,7 +76,7 @@ def expand : ℕ → syntax → exp_m syntax | 0 _ := throw "macro expansion limit exceeded" | (fuel + 1) (syntax.node node) := do cfg ← read, - some {expand := some exp, ..} ← pure $ cfg.macros.find node.m + some {expand := some exp, ..} ← pure $ cfg.macros.find node.macro | (λ args, syntax.node {node with args := args}) <$> node.args.mmap (expand fuel), tag ← mk_tag, let node := {node with args := node.args.map $ flip_tag tag}, @@ -103,28 +84,43 @@ do cfg ← read, expand fuel $ flip_tag tag $ exp node | _ stx := pure stx -@[reducible] def resolve_m' := parse_m parse_state resolve_state +def scope := rbmap (name × option macro_scope_id) var_offset (<) -def resolve : scope → syntax → resolve_m' unit -| sc (syntax.node node) := -do cfg ← read, - some {resolve := some res, ..} ← pure $ cfg.macros.find node.m - | node.args.mfor $ resolve sc, - arg_scopes ← adapt_reader parse_state.resolve_cfg $ res sc node, - (arg_scopes.zip node.args).mfor -- (uncurry resolve) - (λ ⟨sc, stx⟩, resolve sc stx) -| _ _ := pure () +def scope.insert (sc : scope) (id : syntax_ident) : scope := +(sc.map (λ _ idx, idx + 1)).insert (id.name, id.msc) 0 + +def resolve_name (msc : option macro_scope_id) (sc : scope) : name → option resolved +| n@(name.mk_string n' s) := +do { + decl ← sc.find (n, msc), + pure ⟨sum.inl decl, n⟩ +} <|> resolve_name n' +| _ := none + +def resolve : scope → syntax → parse_m parse_state unit syntax +-- TODO(Sebastian): move `match` back into primary pattern, use fuel if necessary +| sc (syntax.node n) := (match n with + | ({macro := `bind, args := [syntax.lst vars, body], ..}) := + do sc ← vars.mfoldl (λ sc var, + do syntax.ident var ← pure var | throw "ill-shaped 'bind' macro", + pure $ scope.insert sc var) sc, + body ← resolve sc body, + pure $ syntax.node {n with args := [syntax.lst vars, body]} + | _ := + do args ← n.args.mmap (resolve sc), + pure $ syntax.node {n with args := args}) +| sc (syntax.ident id) := +do some res ← pure $ resolve_name id.msc sc id.name + | throw ("unknown identifier " ++ id.name.to_string), + pure $ syntax.ident {id with res := some res} +| _ stx := pure stx def expand' (stx : syntax) : parse_m parse_state unit syntax := adapt_state (λ _, ({expand_state . next_tag := 0}, ())) (λ _, id) (expand 1000 stx) -def resolve' (stx : syntax) : parse_m parse_state unit (syntax × resolve_state) := -let sc : scope := mk_rbmap _ _ _, - st : resolve_state := ⟨mk_rbmap _ _ _⟩ in - adapt_state (λ _, (st, ())) (λ _, id) $ - do resolve sc stx, - rsm ← get, - pure (stx, rsm) +def resolve' (stx : syntax) : parse_m parse_state unit syntax := +let sc : scope := mk_rbmap _ _ _ in +resolve sc stx end parser end lean diff --git a/library/init/lean/parser/syntax.lean b/library/init/lean/parser/syntax.lean index 3b7c86ecab..70f704e487 100644 --- a/library/init/lean/parser/syntax.lean +++ b/library/init/lean/parser/syntax.lean @@ -9,21 +9,31 @@ import init.lean.name init.lean.parser.parser_t namespace lean namespace parser -@[reducible] def syntax_id := ℕ +/-- De Bruijn index relative to surrounding 'bind' macros -/ +@[reducible] def var_offset := ℕ @[reducible] def macro_scope_id := ℕ structure span := (left : position) (right : position) +structure resolved := +-- local or (overloaded) global +(decl : var_offset ⊕ list name) +/- prefix of the reference that corresponds to the decl. All trailing name components + are field accesses. -/ +(«prefix» : name) + +instance resolved.has_to_format : has_to_format resolved := ⟨λ r, to_fmt (r.decl, r.prefix)⟩ + structure syntax_ident := -(id : syntax_id) (span : option span) (name : name) (msc : option macro_scope_id) +(span : option span) (name : name) (msc : option macro_scope_id) (res : option resolved) structure syntax_atom := -(id : syntax_id) (span : option span) (val : name) +(span : option span) (val : name) structure syntax_node (syntax : Type) := -(id : syntax_id) (span : option span) (m : name) (args : list syntax) +(span : option span) (macro : name) (args : list syntax) inductive syntax | ident (val : syntax_ident) @@ -43,17 +53,32 @@ protected def span : syntax → option span protected mutual def to_format, to_format_lst with to_format : syntax → format -| (ident {id := id, name := n, msc := none, ..}) := - paren (to_fmt id ++ ": ident " ++ to_fmt n) -| (ident {id := id, name := n, msc := some sc, ..}) := - paren (to_fmt id ++ ": ident " ++ to_fmt n ++ " from " ++ to_fmt sc) -| (atom a) := paren (to_fmt a.id ++ ": atom " ++ to_fmt a.val) -| (lst ls) := paren $ join $ to_format_lst ls -| (node {id := id, m := n, args := args, ..}) := - paren (to_fmt id ++ ": node " ++ to_fmt n ++ join (to_format_lst args)) +| (ident id) := + let n := + to_fmt id.name ++ + (match id.msc with + | some msc := "!" ++ to_fmt msc + | none := "") ++ + (match id.res with + | some res := + ":" ++ + (match res.decl with + | sum.inl idx := to_fmt idx + | sum.inr [n] := to_fmt n + | sum.inr ns := to_fmt ns) + ++ if res.prefix = id.name then + to_fmt "" + else + to_fmt ".(" ++ to_fmt (id.name.replace_prefix res.prefix name.anonymous) ++ ")" + | none := "") in + paren ("ident " ++ n) +| (atom a) := paren ("atom " ++ to_fmt a.val) +| (lst ls) := sbracket $ join_sep (to_format_lst ls) line +| (node {macro := n, args := args, ..}) := + paren ("node " ++ to_fmt n ++ prefix_join line (to_format_lst args)) with to_format_lst : list syntax → list format | [] := [] -| (s::ss) := (line ++ to_format s) :: to_format_lst ss +| (s::ss) := to_format s :: to_format_lst ss end syntax instance : has_to_format syntax := ⟨syntax.to_format⟩ diff --git a/tests/lean/macro1.lean b/tests/lean/macro1.lean index 8b38ddeb21..a5b76bd08d 100644 --- a/tests/lean/macro1.lean +++ b/tests/lean/macro1.lean @@ -7,90 +7,58 @@ def sp : option span := none def lambda_macro := {macro . name := "lambda", - resolve := some $ λ sc node, - do [syntax.ident ident, body] ← pure node.args - | throw "unreachable", - pure [sc, sc.insert (ident.name, ident.msc) ident.id]} - -def resolve_name (msc : option macro_scope_id) (sc : scope) : name → option resolved -| (name.mk_string n s) := -do { - decl ← sc.find (n.mk_string s, msc), - pure ⟨sum.inl decl, n.mk_string s⟩ -} <|> resolve_name n -| _ := none - -def ref_macro := {macro . - name := "ref", - resolve := some $ λ sc node, - do [syntax.ident ident] ← pure node.args - | throw "unreachable", - some resolved ← pure $ resolve_name ident.msc sc ident.name - | throw sformat!"unknown identifier {ident.name}", - modify (λ st, ⟨st.resolve_map.insert ident.id resolved⟩), - pure []} + expand := some $ λ node, + match node.args with + | [ident@(syntax.ident _), body] := + syntax.node {macro := `lambda_core, span := sp, args := [ + syntax.node {macro := `bind, span := sp, args := [ + syntax.lst [ident], + body + ]} + ]} + | _ := syntax.node node} def intro_x_macro := {macro . name := "intro_x", expand := some $ λ node, - -- TODO: how to manage IDs? - syntax.node ⟨5, sp, "lambda", syntax.ident ⟨6, sp, "x", none⟩ :: node.args⟩} + syntax.node ⟨sp, "lambda", syntax.ident ⟨sp, "x", none, none⟩ :: node.args⟩} def macros : name → option macro -| "lambda" := some lambda_macro -| "ref" := some ref_macro -| "intro_x" := some intro_x_macro +| `lambda := some lambda_macro +| `intro_x := some intro_x_macro | _ := none def cfg : parse_state := -{macros := rbmap.from_list ([lambda_macro, ref_macro, intro_x_macro].map (λ m, (m.name, m))) _, +{macros := rbmap.from_list ([lambda_macro, intro_x_macro].map (λ m, (m.name, m))) _, resolve_cfg := {global_scope := mk_rbmap _ _ _}} -namespace rbmap - universes u v w - variables {α : Type u} {β : Type v} {δ : Type w} {lt : α → α → Prop} - open lean.format prod - variables [has_to_format α] [has_to_format β] - - private meta def format_key_data (a : α) (b : β) (first : bool) : format := - (if first then to_fmt "" else to_fmt "," ++ to_fmt line) ++ to_fmt a ++ " " ++ to_fmt "←" ++ " " ++ to_fmt b - - private meta def to_format (m : rbmap α β lt) : format := - group $ to_fmt "⟨" ++ nest 1 (fst (rbmap.fold (λ a b p, (fst p ++ format_key_data a b (snd p), ff)) m (to_fmt "", tt))) ++ - to_fmt "⟩" - - meta instance : has_to_format (rbmap α β lt) := - ⟨to_format⟩ -end rbmap - meta def test (stx : syntax) : command := match (expand' stx >>= resolve').run' cfg () with | except.error e := tactic.fail e -| except.ok (stx, ⟨rsm⟩) := tactic.trace stx >> tactic.trace (stx, rsm) +| except.ok stx := tactic.trace stx -run_cmd test $ syntax.node ⟨0, sp, "lambda", [ - syntax.ident ⟨1, sp, "x", none⟩, - syntax.node ⟨2, sp, "ref", [ - syntax.ident ⟨3, sp, "x", none⟩ - ]⟩ +run_cmd test $ syntax.node ⟨sp, "lambda", [ + syntax.ident ⟨sp, "x", none, none⟩, + syntax.ident ⟨sp, "x", none, none⟩ +]⟩ + +run_cmd test $ syntax.node ⟨sp, "lambda", [ + syntax.ident ⟨sp, "x", none, none⟩, + syntax.ident ⟨sp, "y", none, none⟩ ]⟩ -- test macro shadowing -run_cmd test $ syntax.node ⟨0, sp, "lambda", [ - syntax.ident ⟨1, sp, "x", none⟩, - syntax.node ⟨4, sp, "intro_x", [ - syntax.node ⟨2, sp, "ref", [ - syntax.ident ⟨3, sp, "x", none⟩ - ]⟩ +run_cmd test $ syntax.node ⟨sp, "lambda", [ + syntax.ident ⟨sp, "x", none, none⟩, + syntax.node ⟨sp, "intro_x", [ + syntax.ident ⟨sp, "x", none, none⟩ ]⟩ ]⟩ -- test field notation -run_cmd test $ syntax.node ⟨0, sp, "lambda", [ - syntax.ident ⟨1, sp, `x.y, none⟩, - syntax.node ⟨2, sp, "ref", [ - syntax.ident ⟨3, sp, `x.y.z, none⟩ - ]⟩ +run_cmd test $ syntax.node ⟨sp, "lambda", [ + syntax.ident ⟨sp, `x.y, none, none⟩, + syntax.ident ⟨sp, `x.y.z, none, none⟩ ]⟩ end lean diff --git a/tests/lean/macro1.lean.expected.out b/tests/lean/macro1.lean.expected.out index e48c71b5b6..816fd4d9b0 100644 --- a/tests/lean/macro1.lean.expected.out +++ b/tests/lean/macro1.lean.expected.out @@ -1,6 +1,6 @@ -(0: node lambda (1: ident x) (2: node ref (3: ident x))) -((0: node lambda (1: ident x) (2: node ref (3: ident x))), ⟨3 ← ((inl 1), x)⟩) -(0: node lambda (1: ident x) (5: node lambda (6: ident x from 0) (2: node ref (3: ident x)))) -((0: node lambda (1: ident x) (5: node lambda (6: ident x from 0) (2: node ref (3: ident x)))), ⟨3 ← ((inl 1), x)⟩) -(0: node lambda (1: ident x.y) (2: node ref (3: ident x.y.z))) -((0: node lambda (1: ident x.y) (2: node ref (3: ident x.y.z))), ⟨3 ← ((inl 1), x.y)⟩) +(node lambda_core (node bind [(ident x)] (ident x:0))) +macro1.lean:45:0: error: unknown identifier y +state: +⊢ true +(node lambda_core (node bind [(ident x)] (node lambda_core (node bind [(ident x!1)] (ident x:1))))) +(node lambda_core (node bind [(ident x.y)] (ident x.y.z:0.(z))))