From 76ea8169bc9ceffe78cdfb52ea8a1f2a166bfbfa Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sun, 23 Sep 2018 21:56:09 -0700
Subject: [PATCH] feat(library/init/lean/expander): `prefix` ~> `notation`
 macro: construct RHS, move to new module

---
 library/init/lean/expander.lean       | 48 +++++++++++++++++++++++++++
 library/init/lean/parser/command.lean | 29 ----------------
 library/init/lean/parser/term.lean    |  2 +-
 3 files changed, 49 insertions(+), 30 deletions(-)
 create mode 100644 library/init/lean/expander.lean

diff --git a/library/init/lean/expander.lean b/library/init/lean/expander.lean
new file mode 100644
index 0000000000..11a0a68758
--- /dev/null
+++ b/library/init/lean/expander.lean
@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2018 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Sebastian Ullrich
+
+Macro expander for the Lean language
+-/
+prelude
+import init.lean.parser.module
+
+namespace lean
+namespace expander
+open parser
+open parser.term
+open parser.command
+open parser.command.notation_spec
+
+def mixfix.transform (stx : tysyntax mixfix.view) : option (tysyntax notation.view) :=
+do v ← view stx,
+   -- TODO: reserved token case
+   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 := review $ action_kind.view.prec prec.prec, ..prec},
+   k ← view v.kind,
+   let (spec, term) := match k : _ → (notation_spec.view × syntax) with
+     | mixfix.kind.view.prefix _ :=
+       let b : tysyntax parser.ident.view := review {part := review $ ident_part.view.default "b", suffix := review none} in
+       (notation_spec.view.rules $ review {
+          id := review none,
+          rules := review [review {
+            symbol := v.symbol,
+            transition := review $ some $ review $ transition.view.arg $ review {
+              id := b,
+              action := review $ do prec ← prec, prec ← view prec, pure $ review $ prec_to_action prec}}]},
+        review {lambda.view . op := review lambda_op.view.«λ», binders := review [review $
+            binder.view.unbracketed $ review {
+              ids := review [review $ binder_id.view.id $ review {id := b, univ := review none}],
+              type := review none, default := review none}
+          ],
+          body := review_as app.view {fn := v.term, arg := b}})
+     | _ := sorry,
+   pure $ review {spec := review spec, term := term}
+
+end expander
+end lean
diff --git a/library/init/lean/parser/command.lean b/library/init/lean/parser/command.lean
index e984456bf7..785bab413f 100644
--- a/library/init/lean/parser/command.lean
+++ b/library/init/lean/parser/command.lean
@@ -66,33 +66,4 @@ any_of [open.parser, section.parser, universe.parser, notation.parser, reserve_n
   mixfix.parser, reserve_mixfix.parser, check.parser, declaration.parser] <?> "command"
 
 end parser
-
-namespace parser
-namespace «command»
-open combinators notation_spec
-
--- example macro
-def mixfix.expand (stx : tysyntax mixfix.view) : option (tysyntax notation.view) :=
-do v ← view stx,
-   -- TODO: reserved token case
-   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 := 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 := 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", review spec, ":=", v.term⟩
-
-end «command»
-end parser
 end lean
diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean
index 9bc3c022ff..47f1db8e19 100644
--- a/library/init/lean/parser/term.lean
+++ b/library/init/lean/parser/term.lean
@@ -121,7 +121,7 @@ end binder
 @[derive parser.has_tokens parser.has_view]
 def lambda.parser : term_parser :=
 node! lambda [
-  op: any_of [symbol "λ", symbol "fun"],
+  op: node_choice! lambda_op {"λ", "fun"},
   binders: binder.parser+,
   ",",
   body: recurse 0