From 5bbc80fdade8ac186978eaa80fa992eac718c9f4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 Mar 2019 15:18:34 -0700 Subject: [PATCH] chore(*): fixed token.lean --- library/init/Lean/Parser/token.lean | 22 ++++++------- src/frontends/lean/elaborator.cpp | 48 ++++++++++++++--------------- 2 files changed, 35 insertions(+), 35 deletions(-) diff --git a/library/init/Lean/Parser/token.lean b/library/init/Lean/Parser/token.lean index 0afe73e597..776be9a9c3 100644 --- a/library/init/Lean/Parser/token.lean +++ b/library/init/Lean/Parser/token.lean @@ -100,8 +100,8 @@ Syntax.atom ⟨some {leading := ⟨start, start⟩, pos := start.offset, trailin if trailingWs then withTrailing stx else pure stx instance raw.tokens {α} (p : m α) (t) : Parser.HasTokens (raw p t : Parser) := default _ -instance raw.View {α} (p : m α) (t) : Parser.HasView (Option SyntaxAtom) (raw p t : Parser) := -{ View := λ stx, match stx with +instance raw.view {α} (p : m α) (t) : Parser.HasView (Option SyntaxAtom) (raw p t : Parser) := +{ view := λ stx, match stx with | Syntax.atom atom := some atom | _ := none, review := λ a, (Syntax.atom <$> a).getOrElse Syntax.missing } @@ -121,7 +121,7 @@ set_option class.instance_max_depth 200 @[derive HasTokens HasView] def detailIdentPart.Parser : BasicParserM Syntax := nodeChoice! detailIdentPart { - escaped: Node! detailIdentPartEscaped [ + escaped: node! detailIdentPartEscaped [ escBegin: rawStr idBeginEscape.toString, escaped: raw $ takeUntil1 isIdEndEscape, escEnd: rawStr idEndEscape.toString, @@ -133,10 +133,10 @@ nodeChoice! detailIdentPart { def detailIdentSuffix.Parser : RecT unit Syntax BasicParserM Syntax := -- consume '.' only when followed by a character starting an detailIdentPart try (lookahead (ch '.' *> (ch idBeginEscape <|> satisfy isIdFirst))) -*> Node! detailIdentSuffix [«.»: rawStr ".", ident: recurse ()] +*> node! detailIdentSuffix [«.»: rawStr ".", ident: recurse ()] def detailIdent' : RecT unit Syntax BasicParserM Syntax := -Node! detailIdent [part: monadLift detailIdentPart.Parser, suffix: optional detailIdentSuffix.Parser] +node! detailIdent [part: monadLift detailIdentPart.Parser, suffix: optional detailIdentSuffix.Parser] /-- A Parser that gives a more detailed View of `SyntaxIdent.rawVal`. Not used by default for performance reasons. -/ @@ -181,7 +181,7 @@ nodeLongestChoice! number { } def stringLit' : basicParser := -Node! stringLit [val: raw parseStringLiteral] +node! stringLit [val: raw parseStringLiteral] private def mkConsumeToken (tk : TokenConfig) (it : String.Iterator) : basicParser := let it' := it.nextn tk.prefix.length in @@ -250,7 +250,7 @@ symbolCore sym lbp (Dlist.singleton sym) instance symbol.tokens (sym lbp) : Parser.HasTokens (symbol sym lbp : Parser) := ⟨[⟨sym.trim, lbp, none⟩]⟩ instance symbol.View (sym lbp) : Parser.HasView (Option SyntaxAtom) (symbol sym lbp : Parser) := -{ View := λ stx, match stx with +{ view := λ stx, match stx with | Syntax.atom atom := some atom | _ := none, review := λ a, (Syntax.atom <$> a).getOrElse Syntax.missing } @@ -266,7 +266,7 @@ lift $ try $ do { } "number" instance number.Parser.tokens : Parser.HasTokens (number.Parser : Parser) := default _ -instance number.Parser.View : Parser.HasView number.View (number.Parser : Parser) := +instance number.Parser.view : Parser.HasView number.View (number.Parser : Parser) := {..number.HasView} private def toNatCore (base : Nat) : String.Iterator → Nat → Nat → Nat @@ -292,7 +292,7 @@ def number.View.toNat : number.View → Nat | (number.View.base16 (some atom)) := toNatBase atom.val 16 | _ := 1138 -- should never happen, but let's still choose a grep-able number -def number.View.ofNat (n : Nat) : number.View := +def number.view.ofNat (n : Nat) : number.View := number.View.base10 (some {val := toString n}) def stringLit.Parser : Parser := @@ -322,7 +322,7 @@ lift $ try $ do { instance ident.Parser.tokens : Parser.HasTokens (ident.Parser : Parser) := default _ instance ident.Parser.View : Parser.HasView SyntaxIdent (ident.Parser : Parser) := -{ View := λ stx, match stx with +{ view := λ stx, match stx with | Syntax.ident id := id | _ := {rawVal := Substring.ofString "NOTAnIdent", val := `NOTAnIdent}, review := Syntax.ident } @@ -371,7 +371,7 @@ lift $ do n ← match tk with | Syntax.atom ⟨_, s⟩ := pure $ mkSimpleName s | Syntax.ident _ := pure `ident - | Syntax.rawNode n := pure n.kind.Name + | Syntax.rawNode n := pure n.kind.name | _ := error "", Option.toMonad $ map.find n diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 7fb6d255c4..5cc08a0aa1 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -3221,7 +3221,7 @@ expr elaborator::visit_node_macro(expr const & e, optional const & expecte unsigned i = 0; struc << "@[pattern] def " << esc_macro.to_string(); struc << " := {SyntaxNodeKind . name := `" << full_macro.to_string() << "}\n" - << "structure " << macro.to_string() << ".view :=\n"; + << "structure " << macro.to_string() << ".View :=\n"; buffer new_args; // unhygiene when nested in namespaces auto opts = update(options(), {"pp", "full_names"}, true); @@ -3243,7 +3243,7 @@ expr elaborator::visit_node_macro(expr const & e, optional const & expecte << "'"); auto m2 = mk_metavar(m, r); auto defval_inst = m_ctx.mk_class_instance( - mk_app(mk_app(mk_const(name{"Lean", "Parser", "hasView_default"}), exp, r, m), *inst, m2)); + mk_app(mk_app(mk_const(name{"Lean", "Parser", "HasView_default"}), exp, r, m), *inst, m2)); if (defval_inst) struc << "(«" << fname << "» : " << instantiate_mvars(m) << " := " << pp(instantiate_mvars(m2)) << ")\n"; else @@ -3264,7 +3264,7 @@ expr elaborator::visit_node_macro(expr const & e, optional const & expecte if (is_mdata(r)) { new_args.push_back(add_field(r)); } else {// try block - binds << "let stxs := match stxs with stx::stxs := (match stx.as_node with some n := n.args ++ stxs | _ := stxs) | _ := stxs in\n"; + binds << "let stxs := match stxs with stx::stxs := (match stx.asNode with some n := n.args ++ stxs | _ := stxs) | _ := stxs in\n"; reviews << "Syntax.list ["; buffer new_try_args; for (expr args = app_arg(app_arg(r)); is_app(args); args = app_arg(args)) { @@ -3273,17 +3273,17 @@ expr elaborator::visit_node_macro(expr const & e, optional const & expecte } reviews << "]"; new_args.push_back(mk_app(mk_const({"Lean", "Parser", "MonadParsec", "try"}), - mk_app(mk_const({"Lean", "Parser", "combinators", "seq"}), + mk_app(mk_const({"Lean", "Parser", "Combinators", "seq"}), mk_lean_list(new_try_args)))); } } - struc << "def " << macro.to_string() << ".hasView' : HasView " << macro.to_string() << ".view " << esc_macro.to_string() << " :=\n" - << "{ view := fun stx, let stxs : List Syntax := match stx.as_node with" + struc << "def " << macro.to_string() << ".HasView' : HasView " << macro.to_string() << ".View " << esc_macro.to_string() << " :=\n" + << "{ view := fun stx, let stxs : List Syntax := match stx.asNode with" << "| some n := n.args | _ := [] in\n" << binds.str() - << macro.to_string() << ".view.mk " << mk_args.str() << ",\n" + << macro.to_string() << ".View.mk " << mk_args.str() << ",\n" << "review := fun ⟨" << view_pat.str() << "⟩, Syntax.mkNode " << esc_macro.to_string() << " [" << reviews.str() << "] }"; - struc << "instance " << macro.to_string() << ".hasView := " << macro.to_string() << ".hasView'"; + struc << "instance " << macro.to_string() << ".HasView := " << macro.to_string() << ".HasView'"; trace_elab_detail(tout() << "expansion of node! macro:\n" << struc.str();); std::istringstream in(struc.str()); parser p(m_env, get_global_ios(), in, get_pos_info_provider()->get_file_name()); @@ -3294,7 +3294,7 @@ expr elaborator::visit_node_macro(expr const & e, optional const & expecte p.parse_command_like(); m_env = p.env(); m_ctx.set_env(m_env); - return visit(mk_app(mk_const({"Lean", "Parser", "combinators", "Node"}), mk_const(get_namespace(p.env()) + macro), mk_lean_list(new_args)), + return visit(mk_app(mk_const({"Lean", "Parser", "Combinators", "node"}), mk_const(get_namespace(p.env()) + macro), mk_lean_list(new_args)), expected_type); } @@ -3310,7 +3310,7 @@ expr elaborator::visit_node_choice_macro(expr const & e, bool longest_match, opt unsigned i = 0; struc << "@[pattern] def " << esc_macro.to_string(); struc << " := {SyntaxNodeKind . name := `" << full_macro.to_string() << "}\n" - << "inductive " << macro.to_string() << ".view\n"; + << "inductive " << macro.to_string() << ".View\n"; buffer new_args; // unhygiene when nested in namespaces auto opts = update(options(), {"pp", "full_names"}, true); @@ -3331,38 +3331,38 @@ expr elaborator::visit_node_choice_macro(expr const & e, bool longest_match, opt mk_app(mk_app(mk_const(name{"Lean", "Parser", "HasView_default"}), exp, r, m), *inst, m2)); if (defval_inst) struc << "| " << fname << " : opt_param (" << instantiate_mvars(m) << ") (" - << pp(instantiate_mvars(m2)) << ") -> " << macro.to_string() << ".view\n"; + << pp(instantiate_mvars(m2)) << ") -> " << macro.to_string() << ".View\n"; else - struc << "| " << fname << " : " << instantiate_mvars(m) << " -> " << macro.to_string() << ".view\n"; + struc << "| " << fname << " : " << instantiate_mvars(m) << " -> " << macro.to_string() << ".View\n"; view_cases << "| "; if (is_app(app_arg(e))) view_cases << i; else view_cases << "_"; - view_cases << " := " << macro.to_string() << ".view." << fname << " $ Parser.HasView.view (" << pp(r) + view_cases << " := " << macro.to_string() << ".View." << fname << " $ Parser.HasView.view (" << pp(r) << " : " << pp(exp) << ") stx\n"; - review_cases << "| " << macro.to_string() << ".view." << fname << " a := " - << "Syntax.mkNode (SyntaxNodeKind.mk (Name.mkNumeral Name.Anonymous " << i << ")) " + review_cases << "| " << macro.to_string() << ".View." << fname << " a := " + << "Syntax.mkNode (SyntaxNodeKind.mk (Name.mkNumeral Name.anonymous " << i << ")) " << "[review (" << pp(r) << " : " << pp(exp) << ") a]\n"; i++; new_args.push_back(mk_as_is(r)); } - struc << "def " << macro.to_string() << ".hasView' : HasView " << macro.to_string() << ".view " + struc << "def " << macro.to_string() << ".HasView' : HasView " << macro.to_string() << ".View " << esc_macro.to_string() << " :=\n" - << "{ view := fun stx, let (stx, i) := match stx.as_node : _ -> Prod Syntax Nat with\n" + << "{ view := fun stx, let (stx, i) := match stx.asNode : _ -> Prod Syntax Nat with\n" << "| some {kind := " << esc_macro.to_string() << ", args := [stx], ..} := (match stx.asNode : _ -> Prod Syntax Nat with\n" - << " | some {kind := SyntaxNodeKind.mk (Name.mkNumeral Name.Anonymous i), args := [stx], ..} := (stx, i)\n" - << " | _ := (Syntax.Missing, 0))\n" - << "| _ := (Syntax.Missing, 0) in\n" + << " | some {kind := SyntaxNodeKind.mk (Name.mkNumeral Name.anonymous i), args := [stx], ..} := (stx, i)\n" + << " | _ := (Syntax.missing, 0))\n" + << "| _ := (Syntax.missing, 0) in\n" << "match i with\n" << view_cases.str() << ",\n" << "review := fun v, Syntax.mkNode " << esc_macro.to_string() << " [match v with\n" << review_cases.str() << "] }"; - struc << "instance " << macro.to_string() << ".hasView := " << macro.to_string() << ".hasView'"; - trace_elab_detail(tout() << "expansion of node_choice! macro:\n" << struc.str();); + struc << "instance " << macro.to_string() << ".HasView := " << macro.to_string() << ".HasView'"; + trace_elab_detail(tout() << "expansion of nodeChoice! macro:\n" << struc.str();); std::istringstream in(struc.str()); parser p(m_env, get_global_ios(), in, "foo"); p.set_imports_parsed(); @@ -3372,10 +3372,10 @@ expr elaborator::visit_node_choice_macro(expr const & e, bool longest_match, opt p.parse_command_like(); m_env = p.env(); m_ctx.set_env(m_env); - return visit(mk_app(mk_const({"Lean", "Parser", "combinators", "node"}), + return visit(mk_app(mk_const({"Lean", "Parser", "Combinators", "node"}), mk_const(full_macro), mk_app(mk_const({"List", "cons"}), - mk_app(mk_const({"Lean", "Parser", "combinators", longest_match ? "longestChoice" : "choice"}), + mk_app(mk_const({"Lean", "Parser", "Combinators", longest_match ? "longestChoice" : "choice"}), mk_lean_list(new_args)), mk_const({"List", "nil"}))), expected_type); }