refactor(library/init/lean/{syntax,macro}): remove syntax.ident, simply syntax.atom, remove expander prototype

library/init/lean/macro.lean

@@ -1,90 +0,0 @@
-/-
-Copyright (c) 2018 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Sebastian Ullrich
--/
-prelude
-import init.data.rbmap init.lean.parser.syntax init.control.combinators
-
-namespace lean
-namespace expander
-open parser
-
-local attribute [instance] name.has_lt_quick
-
-@[irreducible, derive monad monad_except monad_reader monad_state]
-def parse_m (r σ) := except_t string $ reader_t r $ state σ
-
-namespace parse_m
-section
-local attribute [reducible] parse_m
-
--- not clear how to auto-derive these
-instance (r σ σ') : monad_state_adapter σ σ' (parse_m r σ) (parse_m r σ')  := infer_instance
-instance (r r' σ) : monad_reader_adapter r r' (parse_m r σ) (parse_m r' σ) := infer_instance
-
-def run {r σ α} (cfg : r) (st : σ) (x : parse_m r σ α) :=
-(x.run.run cfg).run st
-end
-
-def run' {r σ α} (cfg : r) (st : σ): parse_m r σ α → except string α :=
-λ x, prod.fst $ parse_m.run cfg st x
-end parse_m
-
-structure resolve_cfg :=
-(global_scope : rbmap name syntax (<))
-
-abbreviation transformer :=
---- TODO: What else does an expander need? How to model recursive expansion?
-syntax_node syntax → option syntax
-
-def exp_fuel := 1000
-
-structure parse_state :=
-(transformers : rbmap name transformer (<))
-(resolve_cfg : resolve_cfg)
-
--- identifiers in macro expansions are annotated with incremental tags
-structure expand_state :=
-(next_tag : ℕ)
-
-@[reducible] def exp_m := parse_m parse_state expand_state
-
-def mk_tag : exp_m ℕ :=
-do st ← get,
-   put {st with next_tag := st.next_tag + 1},
-   pure st.next_tag
-
-def flip_tag (tag : ℕ) : syntax → syntax
-| (syntax.node node) := syntax.node {node with args := (node.args.map
-    -- flip_tag
-    (λ s, flip_tag s))}
-| (syntax.ident ident@{msc := none, ..}) := syntax.ident {ident with msc := some tag}
-| (syntax.ident ident@{msc := some tag', ..}) :=
-    syntax.ident {ident with msc := if tag = tag' then none else some tag'}
-| stx := stx
-
-def expand : ℕ → syntax → exp_m syntax
-| 0 _ := throw "macro expansion limit exceeded"
-| (fuel + 1) (syntax.node node) :=
-do cfg ← read,
-   some t ← pure $ do { k ← node.kind, cfg.transformers.find k.name }
-     | (λ 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},
-   (match t node' with
-    -- expand recursively
-    | some stx' := expand fuel $ flip_tag tag stx'
-    | none := (λ args, syntax.node {node with args := args}) <$> node.args.mmap (expand fuel))
-| _ stx := pure stx
-
-def scope := rbmap (name × option macro_scope_id) var_offset (<)
-
-def scope.insert (sc : scope) (id : syntax_ident) : scope :=
-(sc.map (λ _ idx, idx + 1)).insert (id.name, id.msc) 0
-
-def expand' (stx : syntax) : parse_m parse_state unit syntax :=
-adapt_state (λ _, ({expand_state . next_tag := 0}, ())) (λ _, id) (expand 1000 stx)
-
-end expander
-end lean

library/init/lean/parser/basic.lean

@@ -122,7 +122,7 @@ parser.run cfg ⟨trie, message_log.empty, s.mk_iterator⟩ s $ do
   let stop := tk_start.to_end in
   pure $ syntax.node ⟨none, [
     stx,
-    syntax.node ⟨eoi, [syntax.atom ⟨some ⟨⟨tk_start, stop⟩, stop.offset, ⟨stop, stop⟩⟩, atomic_val.string ""⟩]⟩
+    syntax.node ⟨eoi, [syntax.atom ⟨some ⟨⟨tk_start, stop⟩, stop.offset, ⟨stop, stop⟩⟩, ""⟩]⟩
   ]⟩
 
 structure parse.view_ty :=

library/init/lean/parser/command.lean

@@ -56,7 +56,7 @@ node! «precedence» [":", prec: number]/-TODO <|> expr-/
 
 def quoted_symbol.parser : command_parser :=
 do (s, info) ← with_source_info $ take_until (= '`'),
-   pure $ syntax.atom ⟨info, atomic_val.string s⟩
+   pure $ syntax.atom ⟨info, s⟩
 
 instance quoted_symbol.tokens : parser.has_tokens quoted_symbol.parser := ⟨[]⟩
 instance quoted_symbol.view : parser.has_view quoted_symbol.parser syntax := default _
@@ -163,7 +163,7 @@ do v ← view mixfix stx,
        rules := [{
          symbol := v.symbol,
          transition := optional_view.some $ transition.view.arg $ {
-           id := `b,
+           id := review id {part := ident_part.view.default "b", suffix := optional_view.none},
            action := prec_to_action <$> prec}}]}
      | _ := sorry,
    pure $ review «notation» ⟨"notation", spec, ":=", v.term⟩

library/init/lean/parser/pratt.lean

@@ -21,7 +21,7 @@ def curr_lbp : m nat :=
 do st ← get,
    except.ok tk ← (monad_lift $ observing $ lookahead token) <* put st | pure 0 <* put st,
    match tk with
-   | syntax.atom ⟨_, atomic_val.string sym⟩ := do
+   | syntax.atom ⟨_, sym⟩ := do
      st ← get,
      some ⟨_, tk_cfg⟩ ← pure (st.tokens.match_prefix sym.mk_iterator) | error "curr_lbp: unreachable",
      pure tk_cfg.lbp

library/init/lean/parser/syntax.lean

@@ -23,24 +23,8 @@ structure source_info :=
 (pos      : parsec.position)
 (trailing : substring)
 
-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 :=
-(info : option source_info) (name : name) (msc : option macro_scope_id) (res : option resolved)
-
-inductive atomic_val
-| string (s : string)
-| name   (n : name)
-
 structure syntax_atom :=
-(info : option source_info) (val : atomic_val)
+(info : option source_info) (val : string)
 
 /-- A simple wrapper that should remind you to use the static declaration instead
     of hard-coding the node name. -/
@@ -52,7 +36,6 @@ structure syntax_node (syntax : Type) :=
 (kind : option syntax_node_kind) (args : list syntax)
 
 inductive syntax
-| ident (val : syntax_ident)
 /- any non-ident atom -/
 | atom (val : syntax_atom)
 | node (val : syntax_node syntax)
@@ -62,10 +45,7 @@ instance : inhabited syntax :=
 ⟨syntax.missing⟩
 
 instance coe_string_syntax : has_coe string syntax :=
-⟨λ s, syntax.atom ⟨none, atomic_val.string s⟩⟩
-
-instance coe_name_syntax : has_coe name syntax :=
-⟨λ n, syntax.ident ⟨none, n, none, none⟩⟩
+⟨λ s, syntax.atom ⟨none, s⟩⟩
 
 def substring.to_string (s : substring) : string :=
 (s.start.extract s.stop).get_or_else ""
@@ -75,27 +55,7 @@ open lean.format
 
 protected mutual def to_format, to_format_lst
 with to_format : syntax → format
-| (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
-  n
-| (atom ⟨_, atomic_val.string s⟩) := to_fmt $ repr s
-| (atom ⟨_, atomic_val.name   n⟩) := to_fmt "`" ++ to_fmt n
+| (atom ⟨_, s⟩) := to_fmt $ repr s
 | (node {kind := none, args := args, ..}) :=
   sbracket $ join_sep (to_format_lst args) line
 | (node {kind := some kind, args := args, ..}) :=
@@ -111,9 +71,7 @@ def reprint_with_info : option source_info → string → string
 
 mutual def reprint, reprint_lst
 with reprint : syntax → string
-| (ident id) := reprint_with_info id.info id.name.to_string
-| (atom ⟨info, atomic_val.string s⟩) := reprint_with_info info s
-| (atom ⟨info, atomic_val.name   n⟩) := reprint_with_info info n.to_string
+| (atom ⟨info, s⟩) := reprint_with_info info s
 | (node n) := reprint_lst n.args
 | missing := ""
 with reprint_lst : list syntax → string

library/init/lean/parser/token.lean

@@ -86,7 +86,7 @@ do token_start ← parser_state.token_start <$> get,
 def raw {α : Type} (p : m α) (leading_ws := ff) (trailing_ws := ff) : parser :=
 try $ do
   (ss, info) ← with_source_info (as_substring p) leading_ws trailing_ws,
-  pure $ syntax.atom ⟨info, atomic_val.string ss.to_string⟩
+  pure $ syntax.atom ⟨info, ss.to_string⟩
 
 instance raw.tokens {α} (p : m α) : parser.has_tokens (raw p : parser) := ⟨[]⟩
 instance raw.view {α} (p : m α) : parser.has_view (raw p : parser) syntax := default _
@@ -98,7 +98,7 @@ end
 --TODO(Sebastian): other bases
 private def number' : basic_parser_m (source_info → syntax) :=
 do num ← take_while1 char.is_digit,
-   pure $ λ i, syntax.node ⟨base10_lit, [syntax.atom ⟨i, atomic_val.string num⟩]⟩
+   pure $ λ i, syntax.node ⟨base10_lit, [syntax.atom ⟨i, num⟩]⟩
 
 set_option class.instance_max_depth 200
 
@@ -129,9 +129,9 @@ do tk ← match_token,
    -- constant-length token
    | some ⟨tk, _, none⟩   :=
      do str tk,
-        pure $ λ i, syntax.atom ⟨some i, atomic_val.string tk⟩
+        pure $ λ i, syntax.atom ⟨some i, tk⟩
    -- variable-length token
-   | some ⟨tk, _, some r⟩ := error "not implemented" --str tk *> monad_parsec.lift r
+   | some ⟨tk, _, some r⟩ := error "symbol': not implemented" --str tk *> monad_parsec.lift r
    | none                 := error
 
 def token : basic_parser_m syntax :=
@@ -149,7 +149,7 @@ variable [monad_basic_read m]
 def symbol (sym : string) (lbp := 0) : parser :=
 lift $ try $ do
   it ← left_over,
-  stx@(syntax.atom ⟨_, atomic_val.string sym'⟩) ← token | error "" (dlist.singleton (repr sym)) it,
+  stx@(syntax.atom ⟨_, sym'⟩) ← token | error "" (dlist.singleton (repr sym)) it,
   when (sym ≠ sym') $
     error "" (dlist.singleton (repr sym)) it,
   pure stx
@@ -188,10 +188,10 @@ lift $ try $ do
   it ← left_over,
   stx ← token,
   let sym' := match stx with
-  | syntax.atom ⟨_, atomic_val.string sym'⟩ := some sym'
+  | syntax.atom ⟨_, sym'⟩ := some sym'
   | syntax.node ⟨ident, _⟩ :=
     (match syntax_node_kind.has_view.view id stx with
-     | some {part := ident_part.view.default (syntax.atom ⟨_, atomic_val.string sym'⟩),
+     | some {part := ident_part.view.default (syntax.atom ⟨_, sym'⟩),
              suffix := optional_view.none} := some sym'
      | _ := none)
   | _ := none,