From 13a67cb9a73873fe0b5b421e6d58606b87435b87 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 13 Aug 2019 19:42:41 -0700
Subject: [PATCH] feat(library/init/lean/elaborator/preterm): add glue code for
 new and old elaborators

---
 library/init/lean/elaborator/basic.lean   |  5 +++--
 library/init/lean/elaborator/command.lean |  2 +-
 library/init/lean/elaborator/preterm.lean | 25 ++++++++++++++++++-----
 3 files changed, 24 insertions(+), 8 deletions(-)

diff --git a/library/init/lean/elaborator/basic.lean b/library/init/lean/elaborator/basic.lean
index c8ff35117b..0e621516f5 100644
--- a/library/init/lean/elaborator/basic.lean
+++ b/library/init/lean/elaborator/basic.lean
@@ -221,6 +221,8 @@ mkElabAttribute `commandTerm "command" builtinCommandElabTable
 constant commandElabAttribute : CommandElabAttribute := default _
 
 namespace Elab
+def logMessage (msg : Message) : Elab Unit :=
+modify $ fun s => { messages := s.messages.add msg, .. s }
 
 def getPosition (pos : Option String.Pos := none) : Elab Position :=
 do ctx ← read;
@@ -234,8 +236,7 @@ do ctx ← read;
    pure { filename := ctx.fileName, pos := pos, text := msg }
 
 def logErrorAt (pos : String.Pos) (errorMsg : String) : Elab Unit :=
-do msg ← mkMessage errorMsg pos;
-   modify (fun s => { messages := s.messages.add msg, .. s })
+mkMessage errorMsg pos >>= logMessage
 
 def logErrorUsingCmdPos (errorMsg : String) : Elab Unit :=
 do s ← get;
diff --git a/library/init/lean/elaborator/command.lean b/library/init/lean/elaborator/command.lean
index 1f77747ccf..036a010853 100644
--- a/library/init/lean/elaborator/command.lean
+++ b/library/init/lean/elaborator/command.lean
@@ -199,7 +199,7 @@ fun n => do
 @[builtinCommandElab «preterm»] def elabPreTerm : CommandElab :=
 fun n => do
   let s := n.getArg 1;
-  pre ← toPreTerm s;
+  pre ← toPreTerm (s.lift Expr);
   runIO (IO.println pre.dbgToString);
   pure ()
 
diff --git a/library/init/lean/elaborator/preterm.lean b/library/init/lean/elaborator/preterm.lean
index dd1c877dda..7b2665ac98 100644
--- a/library/init/lean/elaborator/preterm.lean
+++ b/library/init/lean/elaborator/preterm.lean
@@ -11,9 +11,9 @@ namespace Lean
 abbrev PreTerm := Expr
 
 @[extern "lean_old_elaborate"]
-constant oldElaborate : Environment → Options → MetavarContext → LocalContext → PreTerm → Except (Option Position × Format) (Environment × MetavarContext × Expr) := default _
+constant oldElaborateAux : Environment → Options → MetavarContext → LocalContext → PreTerm → Except (Option Position × Format) (Environment × MetavarContext × Expr) := default _
 
-abbrev PreTermElab := SyntaxNode → Elab PreTerm
+abbrev PreTermElab := SyntaxNode Expr → Elab PreTerm
 
 abbrev PreTermElabTable : Type := HashMap SyntaxNodeKind PreTermElab
 
@@ -55,7 +55,7 @@ private def dummy : Expr := Expr.const `Prop []
 
 namespace Elab
 
-partial def toLevel : Syntax → Elab Level
+partial def toLevel : Syntax Expr → Elab Level
 | stx => do
   match stx.getKind with
   | `Lean.Parser.Level.paren  => toLevel $ stx.getArg 1
@@ -82,7 +82,7 @@ partial def toLevel : Syntax → Elab Level
      pure $ level.addOffset k
   | other => throw "unexpected universe level syntax"
 
-private def setPos (stx : Syntax) (p : PreTerm) : Elab PreTerm :=
+private def setPos (stx : Syntax Expr) (p : PreTerm) : Elab PreTerm :=
 if stx.isOfKind `Lean.Parser.Term.app then pure p
 else do
   cfg ← read;
@@ -92,7 +92,7 @@ else do
     let pos := cfg.fileMap.toPosition pos;
     pure $ Expr.mdata ((MData.empty.setNat `column pos.column).setNat `row pos.line) p
 
-def toPreTerm (stx : Syntax) : Elab PreTerm :=
+def toPreTerm (stx : Syntax Expr) : Elab PreTerm :=
 stx.ifNode
   (fun n => do
     s ← get;
@@ -134,5 +134,20 @@ fun _ => pure $ Expr.mvar Name.anonymous
 @[builtinPreTermElab «sorry»] def convertSorry : PreTermElab :=
 fun _ => pure $ Expr.app (Expr.const `sorryAx []) (Expr.mvar Name.anonymous)
 
+def oldElaborate : Syntax Expr → Elab Expr :=
+fun stx => do
+  p ← toPreTerm stx;
+  scope ← getScope;
+  s ← get;
+  match oldElaborateAux s.env scope.options s.mctx scope.lctx p with
+  | Except.error (some pos, fmt) => do
+    ctx ← read;
+    logMessage { filename := ctx.fileName, pos := pos, text := fmt.pretty scope.options };
+    throw ElabException.silent
+  | Except.error (none, fmt)     => logErrorAndThrow stx (fmt.pretty scope.options)
+  | Except.ok (env, mctx, e)     => do
+    modify $ fun s => { env := env, mctx := mctx, .. s };
+    pure e
+
 end Elab
 end Lean