From 8aa621efb2e1eb6ec973fa1061102eaa72c39019 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 14 Sep 2018 13:45:59 -0700 Subject: [PATCH] refactor(library/init/lean/{syntax,macro}): remove syntax.ident, simply syntax.atom, remove expander prototype --- library/init/lean/macro.lean | 90 --------------------------- library/init/lean/parser/basic.lean | 2 +- library/init/lean/parser/command.lean | 4 +- library/init/lean/parser/pratt.lean | 2 +- library/init/lean/parser/syntax.lean | 50 ++------------- library/init/lean/parser/token.lean | 14 ++--- 6 files changed, 15 insertions(+), 147 deletions(-) delete mode 100644 library/init/lean/macro.lean diff --git a/library/init/lean/macro.lean b/library/init/lean/macro.lean deleted file mode 100644 index 2ebaf230cc..0000000000 --- a/library/init/lean/macro.lean +++ /dev/null @@ -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 diff --git a/library/init/lean/parser/basic.lean b/library/init/lean/parser/basic.lean index 4fb594f913..c8543d31a8 100644 --- a/library/init/lean/parser/basic.lean +++ b/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 := diff --git a/library/init/lean/parser/command.lean b/library/init/lean/parser/command.lean index 4a755db155..17ea8a83d6 100644 --- a/library/init/lean/parser/command.lean +++ b/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⟩ diff --git a/library/init/lean/parser/pratt.lean b/library/init/lean/parser/pratt.lean index a5ee0d17ab..282e404f5b 100644 --- a/library/init/lean/parser/pratt.lean +++ b/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 diff --git a/library/init/lean/parser/syntax.lean b/library/init/lean/parser/syntax.lean index 09a949312a..c8bc81da5e 100644 --- a/library/init/lean/parser/syntax.lean +++ b/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 diff --git a/library/init/lean/parser/token.lean b/library/init/lean/parser/token.lean index b467f8e1a5..e1dce5c207 100644 --- a/library/init/lean/parser/token.lean +++ b/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,