refactor(library/init/lean/parser): make views shallow via tysyntax

library/init/lean/parser/basic.lean

@@ -79,9 +79,16 @@ protected class has_view (r : ρ) (α : out_param Type) :=
 instance has_view.default (r : ρ) : inhabited (parser.has_view r syntax) :=
 ⟨{ view := some, review := id }⟩
 
-class syntax_node_kind.has_view (k : syntax_node_kind) (α : out_param Type) :=
-(view : syntax → option α)
-(review : α → syntax)
+abbreviation tysyntax (α : Type) := syntax
+
+class tysyntax.is_view (α : Type) :=
+(view : tysyntax α → option α)
+(review : α → tysyntax α)
+
+export tysyntax.is_view (view review)
+
+def view_with (α : Type) [tysyntax.is_view α] (stx : syntax) : option α :=
+view (stx : tysyntax α)
 
 def message_of_parsec_message {μ : Type} (cfg : parser_config) (msg : parsec.message μ) : message :=
 -- FIXME: translate position

library/init/lean/parser/combinators.lean

@@ -32,12 +32,12 @@ do (args, _) ← rs.mfoldl (λ (p : list syntax × nat) r, do
    pure $ syntax.node ⟨k, args.reverse⟩
 
 @[reducible] def seq : list parser → parser := node' none
-@[reducible] def node (k : syntax_node_kind) : list parser → parser := node' k
+@[reducible] def node (k : syntax_node_kind) (α : Type) : list parser → parser := node' k
 
 instance node'.tokens (k) (rs : list parser) [parser.has_tokens rs] : parser.has_tokens (node' k rs) :=
 ⟨tokens rs⟩
 
-instance node.view (k) (rs : list parser) [i : syntax_node_kind.has_view k α] : parser.has_view (node k rs) α :=
+instance node.view (k) (α : Type) (rs : list parser) [i : tysyntax.is_view α] : parser.has_view (node k α rs) α :=
 { view := i.view, review := i.review }
 
 private def many1_aux (p : parser) : list syntax → nat → parser
@@ -54,12 +54,14 @@ do rem ← remaining, many1_aux r [] (rem+1)
 instance many1.tokens (r : parser) [parser.has_tokens r] : parser.has_tokens (many1 r) :=
 ⟨tokens r⟩
 
-instance many1.view (r : parser) [parser.has_view r α] : parser.has_view (many1 r) (list α) :=
+instance list.is_view : tysyntax.is_view (list (tysyntax α)) :=
 { view := λ stx, match stx with
-    | syntax.missing := list.ret <$> view r syntax.missing
-    | syntax.node ⟨none, stxs⟩ := stxs.mmap (view r)
+    | syntax.node ⟨none, stxs⟩ := pure stxs
     | _ := failure,
-  review := λ as, syntax.node ⟨none, as.map (review r)⟩ }
+  review := λ as, syntax.node ⟨none, as⟩ }
+
+instance many1.view (r : parser) [parser.has_view r α] : parser.has_view (many1 r) (list (tysyntax α)) :=
+{..list.is_view}
 
 def many (r : parser) : parser :=
 many1 r <|> pure (syntax.node ⟨none, []⟩)
@@ -67,7 +69,7 @@ many1 r <|> pure (syntax.node ⟨none, []⟩)
 instance many.tokens (r : parser) [parser.has_tokens r] : parser.has_tokens (many r) :=
 ⟨tokens r⟩
 
-instance many.view (r : parser) [has_view r α] : parser.has_view (many r) (list α) :=
+instance many.view (r : parser) [has_view r α] : parser.has_view (many r) (list (tysyntax α)) :=
 {..many1.view r}
 
 private def sep_by_aux (p : m syntax) (sep : parser) (allow_trailing_sep : bool) : bool → list syntax → nat → parser
@@ -134,29 +136,18 @@ do r ← optional $
 instance optional.tokens (r : parser) [parser.has_tokens r] : parser.has_tokens (optional r) :=
 ⟨tokens r⟩
 
-inductive optional_view (α : Type)
-| some (a : α) : optional_view
-| none {} : optional_view
-| missing {} : optional_view
-
-namespace optional_view
-instance : functor optional_view :=
-{ map := λ _ _ f v, match v with
-  | some a  := some (f a)
-  | none    := none
-  | missing := missing }
-end optional_view
-
-instance optional.view (r : parser) [parser.has_view r α] : parser.has_view (optional r) (optional_view α) :=
+instance optional.is_view : tysyntax.is_view (option (tysyntax α)) :=
 { view := λ stx, match stx with
-    | syntax.missing := pure optional_view.missing
-    | syntax.node ⟨none, []⟩ := pure optional_view.none
-    | syntax.node ⟨none, [stx]⟩ := optional_view.some <$> view r stx
+    | syntax.missing := failure
+    | syntax.node ⟨none, []⟩ := pure none
+    | syntax.node ⟨none, [stx]⟩ := pure (some stx)
     | _ := failure,
   review := λ a, match a with
-    | optional_view.some a  := syntax.node ⟨none, [review r a]⟩
-    | optional_view.none    := syntax.node ⟨none, []⟩
-    | optional_view.missing := syntax.missing }
+    | some a := syntax.node ⟨none, [a]⟩
+    | none   := syntax.node ⟨none, []⟩ }
+
+instance optional.view (r : parser) [parser.has_view r α] : parser.has_view (optional r) (option (tysyntax α)) :=
+{..optional.is_view}
 
 /-- Parse a list `[p1, ..., pn]` of parsers as `p1 <|> ... <|> pn`.
     Note that there is NO explicit encoding of which parser was chosen;

library/init/lean/parser/command.lean

@@ -69,26 +69,29 @@ end parser
 
 namespace parser
 namespace «command»
-open syntax_node_kind.has_view combinators notation_spec
+open combinators notation_spec
 
 -- example macro
-def mixfix.expand (stx : syntax) : option syntax :=
-do v ← view mixfix stx,
+def mixfix.expand (stx : tysyntax mixfix.view) : option (tysyntax notation.view) :=
+do v ← view stx,
    -- TODO: reserved token case
-   notation_symbol.view.quoted {prec:=prec, ..} ← pure v.symbol,
+   notation_symbol.view.quoted quoted ← view v.symbol,
+   quoted ← view quoted,
+   prec ← view quoted.prec,
    -- `notation` allows more syntax after `:` than mixfix commands, so we have to do a small conversion
    let prec_to_action : precedence.view → action.view :=
-     λ prec, {action := action_kind.view.prec prec.prec, ..prec},
-   let spec := view.rules $ match v.kind with
-     | mixfix.kind.view.prefix _ := {
-       id := optional_view.none,
-       rules := [{
+     λ prec, {action := review $ action_kind.view.prec prec.prec, ..prec},
+   k ← view v.kind,
+   let spec := view.rules $ match k with
+     | mixfix.kind.view.prefix _ := review {
+       id := review none,
+       rules := review [review {
          symbol := v.symbol,
-         transition := optional_view.some $ transition.view.arg $ {
-           id := review ident {part := ident_part.view.default "b", suffix := optional_view.none},
-           action := prec_to_action <$> prec}}]}
+         transition := review $ some $ review $ transition.view.arg $ review {
+           id := review {part := review $ ident_part.view.default "b", suffix := review none},
+           action := review $ do prec ← prec, prec ← view prec, pure $ review $ prec_to_action prec}}]}
      | _ := sorry,
-   pure $ review «notation» ⟨"notation", spec, ":=", v.term⟩
+   pure $ review ⟨"notation", review spec, ":=", v.term⟩
 
 end «command»
 end parser

library/init/lean/parser/term.lean

@@ -166,7 +166,7 @@ any_of [
 
 @[derive parser.has_tokens parser.has_view]
 def sort_app.parser : trailing_term_parser :=
-do { l ← get_leading, guard (syntax_node_kind.has_view.view sort l).is_some } *>
+do { l ← get_leading, guard (view_with sort.view l).is_some } *>
 node! sort_app [fn: get_leading, arg: monad_lift (level.parser max_prec)]
 
 @[derive parser.has_tokens parser.has_view]

library/init/lean/parser/token.lean

@@ -182,7 +182,8 @@ lift $ try $ do {
 } <?> "identifier"
 
 instance ident.parser.tokens : parser.has_tokens (ident.parser : parser) := default _
-instance ident.parser.view : parser.has_view (ident.parser : parser) syntax := default _
+instance ident.parser.view : parser.has_view (ident.parser : parser) ident.view :=
+{..ident.view.is_view}
 
 /-- Check if the following token is the symbol _or_ identifier `sym`. Useful for
     parsing local tokens that have not been added to the token table (but may have
@@ -197,11 +198,12 @@ lift $ try $ do
   stx ← token,
   let sym' := match stx with
   | syntax.atom ⟨_, sym'⟩ := some sym'
-  | syntax.node ⟨ident, _⟩ :=
-    (match syntax_node_kind.has_view.view ident stx with
-     | some {part := ident_part.view.default (syntax.atom ⟨_, sym'⟩),
-             suffix := optional_view.none} := some sym'
-     | _ := none)
+  | syntax.node ⟨ident, _⟩ := do {
+     id ← view_with ident.view stx,
+     ident_part.view.default (syntax.atom ⟨_, sym'⟩) ← view id.part | none,
+     none ← view id.suffix | none,
+     some sym'
+   }
   | _ := none,
   when (sym' ≠ some sym) $
     error "" (dlist.singleton (repr sym)) it,

src/frontends/lean/elaborator.cpp

@@ -3216,7 +3216,7 @@ expr elaborator::visit_node_macro(expr const & e, optional<expr> const & expecte
     if (!expected_type)
         throw elaborator_exception(e, "node!: expected type must be known");
     expr exp = expected_type.value();
-    sstream struc, stx_pat, binds, mk_args, view_pat, reviews;
+    sstream struc, stx_pat, mk_args, view_pat, reviews;
     unsigned i = 0;
     struc << "@[pattern] def " << esc_macro.to_string();
     struc << " := {syntax_node_kind . name := `" << full_macro.to_string() << "}\n"
@@ -3238,19 +3238,18 @@ expr elaborator::visit_node_macro(expr const & e, optional<expr> const & expecte
             if (!inst)
                 throw elaborator_exception(e, sstream() << "Could not infer instance of parser.has_view for '" << r
                                                         << "'");
-            struc << "(«" << fname << "» : " << instantiate_mvars(m) << ")\n";
+            struc << "(«" << fname << "» : tysyntax (" << instantiate_mvars(m) << "))\n";
 
             if (i != 0)
                 stx_pat << ", ";
             stx_pat << "stx" << i;
-            binds << "a" << i << " <- view (" << pp(r) << " : " << pp(exp) << ") stx" << i << ",\n";
-            mk_args << "a" << i << " ";
+            mk_args << "stx" << i << " ";
             if (i != 0)
                 view_pat << ", ";
             view_pat << "a" << i;
             if (i != 0)
                 reviews << ", ";
-            reviews << "review (" << pp(r) << " : " << pp(exp) << ") a" << i;
+            reviews << "a" << i;
             i++;
             return mk_as_is(r);
         };
@@ -3271,10 +3270,9 @@ expr elaborator::visit_node_macro(expr const & e, optional<expr> const & expecte
                                              mk_lean_list(new_try_args))));
         }
     }
-    struc << "instance " << macro.to_string() << ".has_view : " << macro.to_string() << ".has_view " << macro.to_string() << ".view :=\n"
+    struc << "instance " << macro.to_string() << ".view.is_view : tysyntax.is_view " << macro.to_string() << ".view :=\n"
             << "{ view := fun stx, do {\n"
             << "syntax.node (syntax_node.mk " << esc_macro.to_string() << " [" << stx_pat.str() << "]) <- pure stx | failure,\n"
-            << binds.str()
             << "pure (" << macro.to_string() << ".view.mk " << mk_args.str() << ") },\n"
             << "review := fun ⟨" << view_pat.str() << "⟩, syntax.node (syntax_node.mk " << esc_macro.to_string() << " [" << reviews.str() << "]) }";
     trace_elab_detail(tout() << "expansion of node! macro:\n" << struc.str(););
@@ -3286,7 +3284,10 @@ expr elaborator::visit_node_macro(expr const & e, optional<expr> 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(full_macro),
+                        mk_const(full_macro + "view"),
+                        mk_lean_list(new_args)),
                  expected_type);
 }
 
@@ -3318,18 +3319,16 @@ expr elaborator::visit_node_choice_macro(expr const & e, optional<expr> const &
         if (!inst)
             throw elaborator_exception(e, sstream() << "Could not infer instance of parser.has_view for '" << r
                                                     << "'");
-        struc << "| " << fname << " : " << instantiate_mvars(m) << " -> " << macro.to_string() << ".view\n";
+        struc << "| " << fname << " : tysyntax (" << instantiate_mvars(m) << ") -> " << macro.to_string() << ".view\n";
 
-        view_cases << "| " << i << " := " << macro.to_string() << ".view." << fname << " <$> view  (" << pp(r)
-                << " : " << pp(exp) << ") stx\n";
+        view_cases << "| " << i << " := " << macro.to_string() << ".view." << fname << " stx\n";
         review_cases << "| " << macro.to_string() << ".view." << fname << " a := "
                 << "syntax.node (syntax_node.mk (some (syntax_node_kind.mk (name.mk_numeral name.anonymous " << i << "))) "
-                << "[review (" << pp(r) << " : " << pp(exp) << ") a])\n";
+                << "[a])\n";
         i++;
         new_args.push_back(mk_as_is(r));
     }
-    struc << "instance " << macro.to_string() << ".has_view : " << macro.to_string() << ".has_view "
-          << macro.to_string() << ".view :=\n"
+    struc << "instance " << macro.to_string() << ".view.is_view : tysyntax.is_view " << macro.to_string() << ".view :=\n"
           << "{ view := fun stx, do {\n"
           << "syntax.node (syntax_node.mk " << esc_macro.to_string()
           << " [syntax.node (syntax_node.mk (some (syntax_node_kind.mk (name.mk_numeral name.anonymous i))) [stx])]) <- pure stx | failure,\n"
@@ -3350,6 +3349,7 @@ expr elaborator::visit_node_choice_macro(expr const & e, optional<expr> const &
     m_ctx.set_env(m_env);
     return visit(mk_app(mk_const({"lean", "parser", "combinators", "node"}),
                         mk_const(full_macro),
+                        mk_const(full_macro + "view"),
                         mk_app(mk_const({"list", "cons"}),
                                mk_app(mk_const({"lean", "parser", "combinators", "choice"}),
                                       mk_lean_list(new_args)),