feat(library/init/lean/expander): very basic expander

library/init/lean/expander.lean

@@ -15,7 +15,17 @@ open parser.term
 open parser.command
 open parser.command.notation_spec
 
-def mixfix.transform (stx : tysyntax mixfix.view) : option (tysyntax notation.view) :=
+@[derive monad]
+def transform_m := option_t $ except message
+abbreviation transformer := syntax → transform_m syntax
+
+section
+local attribute [reducible] transform_m
+instance coe_option_transform_m {α : Type} : has_coe (option α) (transform_m α) :=
+⟨λ o, match o with some a := pure a | none := failure⟩
+end
+
+def mixfix.transform (stx : tysyntax mixfix.view) : transform_m (tysyntax notation.view) :=
 do v ← view stx,
    -- TODO: reserved token case
    notation_symbol.view.quoted quoted ← view v.symbol,
@@ -42,5 +52,18 @@ do v ← view stx,
      | _ := sorry,
    pure $ review {spec := review spec, term := term}
 
+local attribute [instance] name.has_lt_quick
+
+-- TODO(Sebastian): replace with attribute
+def transformers : rbmap name transformer (<) := rbmap.from_list [
+  (mixfix.name, mixfix.transform)
+] _
+
+def expand (stx : syntax) : except message syntax :=
+--TODO(Sebastian): recursion, hygiene, error messages
+do syntax.node {kind := some k, ..} ← pure stx | pure stx,
+   some t ← pure $ transformers.find k.name | pure stx,
+   flip option.get_or_else stx <$> t stx
+
 end expander
 end lean

tests/lean/parser1.lean

@@ -1,7 +1,7 @@
-import init.lean.parser.module init.io
+import init.lean.parser.module init.lean.expander init.io
 open lean
 open lean.parser
-open lean.parser.syntax_node_kind.has_view
+open lean.expander
 
 def show_result (p : syntax × message_log) (s : string) : except_t string io unit :=
 let (stx, msgs) := p in
@@ -57,16 +57,6 @@ universes u v
 -- parsed as `Type (max) (u) (v)`, will fail on elaboration ("max: must have at least two arguments", "function expected at 'Type'", "unknown identifier 'u'/'v'")
 #eval show_parse "#check Type max u v"
 
--- expansion example
-#eval (do {
-  (stx, ⟨[]⟩) ← monad_except.lift_except $ parse_module "prefix `+`:10 := _",
-  some {root := stx, ..} ← pure $ parser.parse.view stx,
-  some {commands := [stx], ..} ← pure $ view module stx,
-  some stx ← pure $ command.mixfix.expand stx | throw "expand fail",
-  io.println stx,
-  io.println stx.reprint
-} : except_t string io unit)
-
 -- slowly progressing...
 #eval do
   s ← io.fs.read_file "../../library/init/core.lean",
@@ -77,5 +67,7 @@ universes u v
     | coroutine_result_core.done p := show_result p s *> pure (sum.inr ())
     | coroutine_result_core.yielded cmd k := do {
       --io.println "command:" *> io.println cmd,
-      pure (sum.inl k)
+      match expand cmd with
+      | except.ok cmd' := pure (sum.inl k)
+      | except.error e := throw e.text
     }

tests/lean/parser1.lean.expected.out

@@ -117,30 +117,6 @@ result:
       (term.ident `u []))
      (term.ident `v [])))])
  (eoi "")]
-(command.notation
- "notation"
- (command.notation_spec
-  (1
-   (command.notation_spec.rules
-    []
-    [(command.notation_spec.rule
-      (command.notation_spec.notation_symbol
-       (0
-        (command.notation_spec.notation_quoted_symbol
-         "`"
-         "+"
-         "`"
-         [(command.notation_spec.precedence ":" (base10_lit "10"))])))
-      [(command.notation_spec.transition
-        (2
-         (command.notation_spec.argument
-          `b
-          [(command.notation_spec.action
-            ":"
-            (command.notation_spec.action_kind (0 (base10_lit "10"))))])))])])))
- ":="
- (term.hole "_"))
-notation`+`:10 b:10 :=_
 error at line 223, column 6:
 unexpected '='
 error at line 225, column 44:
@@ -841,7 +817,7 @@ partial syntax tree:
          (command.simple_decl_val
           ":="
           (term.lambda
-           "λ"
+           (term.lambda_op (0 "λ"))
            [(term.binder
              (1
               (term.binder_content
@@ -1164,7 +1140,7 @@ partial syntax tree:
           (term.anonymous_constructor
            "⟨"
            [(term.lambda
-             "λ"
+             (term.lambda_op (0 "λ"))
              [(term.binder
                (1 (term.binder_content [(term.binder_id (1 (term.hole "_")))] [] [])))]
              ","
@@ -1274,7 +1250,7 @@ partial syntax tree:
           (term.anonymous_constructor
            "⟨"
            [(term.lambda
-             "λ"
+             (term.lambda_op (0 "λ"))
              [(term.binder
                (1 (term.binder_content [(term.binder_id (1 (term.hole "_")))] [] [])))]
              ","
@@ -1348,7 +1324,7 @@ partial syntax tree:
           (term.anonymous_constructor
            "⟨"
            [(term.lambda
-             "λ"
+             (term.lambda_op (0 "λ"))
              [(term.binder
                (1 (term.binder_content [(term.binder_id (1 (term.hole "_")))] [] [])))]
              ","
@@ -1438,7 +1414,7 @@ partial syntax tree:
           (term.anonymous_constructor
            "⟨"
            [(term.lambda
-             "λ"
+             (term.lambda_op (0 "λ"))
              [(term.binder
                (1 (term.binder_content [(term.binder_id (1 (term.hole "_")))] [] [])))]
              ","
@@ -1548,7 +1524,7 @@ partial syntax tree:
           (term.anonymous_constructor
            "⟨"
            [(term.lambda
-             "λ"
+             (term.lambda_op (0 "λ"))
              [(term.binder
                (1 (term.binder_content [(term.binder_id (1 (term.hole "_")))] [] [])))]
              ","
@@ -1622,7 +1598,7 @@ partial syntax tree:
           (term.anonymous_constructor
            "⟨"
            [(term.lambda
-             "λ"
+             (term.lambda_op (0 "λ"))
              [(term.binder
                (1 (term.binder_content [(term.binder_id (1 (term.hole "_")))] [] [])))]
              ","
@@ -1843,7 +1819,7 @@ partial syntax tree:
               (term.paren
                "("
                [(term.lambda
-                 "λ"
+                 (term.lambda_op (0 "λ"))
                  [(term.binder
                    (1
                     (term.binder_content
@@ -1962,7 +1938,7 @@ partial syntax tree:
                (term.paren
                 "("
                 [(term.lambda
-                  "λ"
+                  (term.lambda_op (0 "λ"))
                   [(term.binder
                     (1
                      (term.binder_content