feat(library/init/lean/parser): remove syntax_id, use De Bruijn indices instead

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 :=

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

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

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⟩

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

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))))