From e6b988a10a1d670327e78a59dd158af54fc50c52 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 13 Jun 2020 16:20:23 +0200
Subject: [PATCH] feat: add natural language demo

---
 tests/playground/forthelean/ForTheLean.lean   |  1 +
 .../forthelean/ForTheLean/Demo.lean           | 82 +++++++++++++++++++
 .../forthelean/ForTheLean/Prelim.lean         | 79 ++++++++++++++++++
 3 files changed, 162 insertions(+)
 create mode 100644 tests/playground/forthelean/ForTheLean.lean
 create mode 100644 tests/playground/forthelean/ForTheLean/Demo.lean
 create mode 100644 tests/playground/forthelean/ForTheLean/Prelim.lean

diff --git a/tests/playground/forthelean/ForTheLean.lean b/tests/playground/forthelean/ForTheLean.lean
new file mode 100644
index 0000000000..9af054101d
--- /dev/null
+++ b/tests/playground/forthelean/ForTheLean.lean
@@ -0,0 +1 @@
+import ForTheLean.Demo
diff --git a/tests/playground/forthelean/ForTheLean/Demo.lean b/tests/playground/forthelean/ForTheLean/Demo.lean
new file mode 100644
index 0000000000..82504a4538
--- /dev/null
+++ b/tests/playground/forthelean/ForTheLean/Demo.lean
@@ -0,0 +1,82 @@
+-- -*- origami-fold-style: triple-braces -*-
+import ForTheLean.Prelim
+new_frontend
+open Lean
+open Lean.Elab.Command
+open Prelim
+
+-- {{{ [synonym]
+syntax variant := "-"? wlexem
+syntax [synonym] "[synonym " wlexem ("/" (wlexem <|> variant))+ "]" : command
+@[commandElab synonym]
+def elabSynonym : CommandElab :=
+fun stx => match_syntax stx with
+| `([synonym $w:ident/ -$w':ident]) => modifyEnv $ fun env => addSynonym env w.getId (w.getId.appendAfter w'.getId.toString)
+| `([synonym $w:ident/$w':ident]) => modifyEnv $ fun env => addSynonym env w.getId w'.getId
+| _ => throwUnsupportedSyntax
+-- }}}
+
+[synonym number/numbers]
+
+-- {{{
+syntax indef := "A" <|> "a" <|> "An" <|> "an"
+syntax art := "The" <|> "the" <|> indef
+
+syntax notionPattern := art wlexem+
+
+-- all class nouns are added dynamically
+declare_syntax_cat classNoun
+
+syntax "Signature." notionPattern "is" indef (classNoun <|> "notion") "." : command
+macro_rules
+| `(Signature. The $words:wlexem* is a notion.) =>
+  let words := words.map Syntax.getId;
+  let parsers := words.map mkSyntaxAtom;
+  let desc := mkIdent $ mkNameSimple $ "_".intercalate $ words.toList.map toString;
+  `(axiom $desc:ident : Type
+    syntax_synonyms [$desc] $parsers:syntax* : classNoun
+    @[macro $desc] def expandSig : Macro := fun _ => `($desc))
+| `(Signature. The $words:wlexem* is a $n.) =>
+  let words := words.map Syntax.getId;
+  let parsers := words.map mkSyntaxAtom;
+  let desc := mkIdent $ mkNameSimple $ "_".intercalate $ words.toList.map toString;
+  `(axiom $desc:ident : $n
+    syntax_synonyms [$desc] $parsers:syntax* : classNoun
+    @[macro $desc] def expandSig : Macro := fun _ => `($desc))
+-- }}}
+
+Signature. A real number is a notion.
+
+-- {{{
+-- TODO: should be single character
+syntax newVar := ident
+syntax standFor := "stand" "for"
+syntax standForDenote := standFor <|> "denote"
+syntax "Let" (sepBy newVar ",") standForDenote (indef)? classNoun "." : command
+macro_rules
+| `(Let $vs* denote $indef* $noun.) =>
+  `(variables ($(vs.getSepElems.map (fun v => v.getArg 0)):ident* : $noun))
+-- }}}
+
+Let x,y stand for real numbers.
+
+-- {{{
+syntax var := ident  -- TODO: should be single character
+syntax uniPredPattern := var "is" wlexem+ var
+syntax predPattern := uniPredPattern
+syntax "Signature." predPattern "is" (indef)? "atom" "." : command
+macro_rules
+| `(Signature. $x:var is $words:wlexem* $y:var is an atom.) =>
+  let words := words.toList.map Syntax.getId;
+  let desc := mkNameSimple $ "_".intercalate $ words.map toString;
+  `(axiom $(mkIdent desc):ident : type_of $(x.getArg 0) → type_of $(y.getArg 0) → Prop)
+-- }}}
+
+Signature. x is greater than y is an atom.
+Signature. A packing of congruent balls in Euclidean three space is a notion.
+Signature. The face centered cubic packing is a packing of congruent balls in Euclidean three space.
+Let P denote a packing of congruent balls in Euclidean three space.
+-- incomplete from here on
+Signature. The density of P is a real number.
+
+Theorem The_Kepler_conjecture. No packing of congruent balls in Euclidean three space has density greater than the density of the face centered cubic packing.
diff --git a/tests/playground/forthelean/ForTheLean/Prelim.lean b/tests/playground/forthelean/ForTheLean/Prelim.lean
new file mode 100644
index 0000000000..e58b243338
--- /dev/null
+++ b/tests/playground/forthelean/ForTheLean/Prelim.lean
@@ -0,0 +1,79 @@
+import Lean
+namespace Lean.Elab.Command
+open Lean
+-- to get around missing structure notation support
+def modifyEnv (f : Environment → Environment) : CommandElabM Unit :=
+modify $ fun s => { s with env := f s.env }
+end Lean.Elab.Command
+
+namespace Prelim
+open Lean
+open Lean.Parser
+
+-- for declaring simple parsers I can still use within other `syntax`
+@[commandParser] def syntaxAbbrev := parser! "syntax " >> ident >> " := " >> many1 syntaxParser
+@[macro syntaxAbbrev] def elabSyntaxAbbrev : Macro :=
+fun stx => match_syntax stx with
+| `(syntax $id := $p*) => `(declare_syntax_cat $id  syntax:0 $p* : $id)
+| _ => Macro.throwUnsupported
+
+def mkSyntaxAtom (n : Name) : Syntax :=
+Syntax.node `Lean.Parser.Syntax.atom #[Lean.mkStxStrLit n.toString, mkNullNode]
+
+-- store known synonyms of a word
+
+-- HACK: can't define new environment extension at runtime, so I'm reusing this matching one...
+def addSynonym (env : Environment) (a : Name) (e : Name) : Environment :=
+addAlias env (`_subst ++ a) (e)
+
+def getSynonyms (env : Environment) (a : Name) : List Name :=
+match (aliasExtension.getState env).find? (`_subst ++ a) with
+| none    => []
+| some es => es
+
+def checkPrev (p : Syntax → Bool) (errorMsg : String) : Parser :=
+{ fn := fun c s =>
+  let prev := s.stxStack.back;
+  if p prev then s else s.mkError errorMsg }
+
+-- a word lexem is any identifier/keyword except for variables and "is"
+def wlexem : Parser :=
+try (rawIdent >> checkPrev (fun stx => stx.getId.toString.length > 1 && not ([`is].contains stx.getId)) "")
+end Prelim
+
+new_frontend
+open Lean
+open Lean.Elab
+open Lean.Elab.Command
+open Prelim
+
+syntax [type_of] "type_of" term:max : term
+@[termElab «type_of»]
+def elabTypeOf : Term.TermElab :=
+fun stx _ => match_syntax stx with
+| `(type_of $e) =>
+  Term.elabTerm e none >>= Term.inferType e
+| _ => Term.throwUnsupportedSyntax
+
+syntax [syntax_synonyms] "syntax_synonyms" "[" ident "]" «syntax»+ ":" ident : command
+@[commandElab «syntax_synonyms»] def elabSyntaxSynonyms : CommandElab :=
+fun stx => match_syntax stx with
+| `(syntax_synonyms [$kind] $stxs* : $cat) =>
+  -- TODO: do notation
+  getEnv >>= fun env =>
+  -- map word w with synonyms w1... to syntax ("w" <|> "w1" <|> ...)
+  let stxs := stxs.map (fun stx =>
+    if stx.isOfKind `Lean.Parser.Syntax.atom then
+      let word := (Lean.Syntax.isStrLit? (stx.getArg 0)).getD "";
+      let substs := getSynonyms env (mkNameSimple word);
+      -- TODO: `(syntax|` antiquotation
+      -- TODO: `foldl1` would be nice
+      substs.foldl (fun stx word => Syntax.node `Lean.Parser.Syntax.orelse #[stx, mkAtom "<|>", mkSyntaxAtom word])
+        stx
+    else stx);
+  `(syntax [$kind] $stxs:syntax* : $cat) >>= elabCommand
+| _ => throwUnsupportedSyntax
+
+-- HACK: get `wlexem` into `syntax` world
+declare_syntax_cat wlexem
+@[wlexemParser] def wlexem := Prelim.wlexem