From bd7ee8b01b4e13abf46a7deca150bfe9e933aff1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 14 Sep 2019 08:41:49 -0700
Subject: [PATCH] feat(library/init/lean/elaborator/term): add `elabList`, and
 fix `elabTermAux`

---
 library/init/lean/elaborator/command.lean |  5 ++++-
 library/init/lean/elaborator/term.lean    | 16 +++++++++++++---
 library/init/lean/parser/term.lean        |  3 +++
 library/init/lean/syntax.lean             |  5 +++++
 tests/playground/frontend1.lean           |  7 ++++---
 5 files changed, 29 insertions(+), 7 deletions(-)

diff --git a/library/init/lean/elaborator/command.lean b/library/init/lean/elaborator/command.lean
index 4ac81aba39..68bb44d3ff 100644
--- a/library/init/lean/elaborator/command.lean
+++ b/library/init/lean/elaborator/command.lean
@@ -204,6 +204,7 @@ fun n => do
 @[builtinCommandElab «preterm»] def elabPreTerm : CommandElab :=
 fun n => do
   let s := n.getArg 1;
+  runIO (IO.println s);
   pre ← toPreTerm (s.lift Expr);
   runIO (IO.println pre.dbgToString);
   pure ()
@@ -214,7 +215,9 @@ fun n => do
   r ← elabTerm (s.lift Expr);
   match r with
   | Syntax.other e => runIO (IO.println e.dbgToString)
-  | _              => throw "failed to elaborate syntax"
+  | other          => do
+    runIO (IO.println other);
+    throw "failed to elaborate syntax"
 
 /- We just ignore Lean3 notation declaration commands. -/
 @[builtinCommandElab «mixfix»] def elabMixfix : CommandElab := fun _ => pure ()
diff --git a/library/init/lean/elaborator/term.lean b/library/init/lean/elaborator/term.lean
index fbb1ffa223..d0feafeeb4 100644
--- a/library/init/lean/elaborator/term.lean
+++ b/library/init/lean/elaborator/term.lean
@@ -18,7 +18,11 @@ partial def elabTermAux : Syntax Expr → Option Expr → Bool → Elab (Syntax
     let tables := termElabAttribute.ext.getState s.env;
     let k      := n.getKind;
     match tables.find k with
-    | some elab => elab n expectedType
+    | some elab => do
+      newStx ← elab n expectedType;
+      match newStx with
+      | Syntax.other _ => pure newStx
+      | _              => elabTermAux newStx expectedType expanding
     | none      => do
       -- recursively expand syntax
       let k := n.getKind;
@@ -38,10 +42,16 @@ partial def elabTermAux : Syntax Expr → Option Expr → Bool → Elab (Syntax
 def elabTerm (stx : Syntax Expr) (expectedType : Option Expr := none) : Elab (Syntax Expr) :=
 elabTermAux stx expectedType false
 
+open Lean.Parser
+
 @[builtinTermElab «list»] def elabList : TermElab :=
 fun stx _ => do
-  runIO (IO.println stx.val);
-  pure stx.val
+  let openBkt  := stx.getArg 0;
+  let args     := stx.getArg 1;
+  let closeBkt := stx.getArg 2;
+  let consId   := openBkt.mkIdent `List.cons;
+  let nilId    := closeBkt.mkIdent `List.nil;
+  pure $ args.foldSepArgs (fun arg r => mkAppStx consId [arg, r]) nilId
 
 end Elab
 end Lean
diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean
index e4dd82afeb..feb9928b8f 100644
--- a/library/init/lean/parser/term.lean
+++ b/library/init/lean/parser/term.lean
@@ -176,5 +176,8 @@ def checkIsSort := checkLeading (fun leading => leading.isOfKind `Lean.Parser.Te
 
 end Term
 
+def mkAppStx {α} (fn : Syntax α) (args : List (Syntax α)) : Syntax α :=
+args.foldl (fun fn arg => Syntax.node `Lean.Parser.Term.app [fn, arg].toArray) fn
+
 end Parser
 end Lean
diff --git a/library/init/lean/syntax.lean b/library/init/lean/syntax.lean
index d8ab0be98f..95afdcf2d3 100644
--- a/library/init/lean/syntax.lean
+++ b/library/init/lean/syntax.lean
@@ -457,5 +457,10 @@ match stx.isNatLit with
 | some val => val
 | none     => 0
 
+/-- Create an identifier using `SourceInfo` from `src` -/
+def mkIdent {α} (src : Syntax α) (val : Name) : Syntax α :=
+let info := src.getHeadInfo;
+Syntax.ident info (toString val).toSubstring val []
+
 end Syntax
 end Lean
diff --git a/tests/playground/frontend1.lean b/tests/playground/frontend1.lean
index d16156fbe6..be8961cb9a 100644
--- a/tests/playground/frontend1.lean
+++ b/tests/playground/frontend1.lean
@@ -2,9 +2,10 @@ import init.lean.elaborator
 open Lean
 
 def main (xs : List String) : IO Unit :=
-do path ← IO.getEnv "LEAN_PATH";
-   IO.println path;
+do initSearchPath "../../library:.";
+   -- path ← IO.getEnv "LEAN_PATH";
+   -- IO.println path;
    contents ← IO.readTextFile xs.head;
-   (env, messages) ← testFrontend contents xs.head;
+   (env, messages) ← Elab.testFrontend contents xs.head;
    messages.toList.mfor $ fun msg => IO.println msg;
    pure ()