feat(library/init/lean/elaborator): add expected type

library/init/lean/elaborator/basic.lean

@@ -73,7 +73,7 @@ abbrev Elab := ReaderT ElabContext (EState ElabException ElabState)
 
 instance str2ElabException : HasCoe String ElabException := ⟨ElabException.other⟩
 
-abbrev TermElab    := SyntaxNode Expr → Elab (Syntax Expr)
+abbrev TermElab    := SyntaxNode Expr → Option Expr → Elab (Syntax Expr)
 abbrev CommandElab := SyntaxNode → Elab Unit
 
 abbrev TermElabTable : Type := SMap SyntaxNodeKind TermElab Name.quickLt

library/init/lean/elaborator/preterm.lean

@@ -53,6 +53,17 @@ Expr.mdata (MData.empty.setName `annotation ann) e
 
 private def dummy : Expr := Expr.const `Prop []
 
+def mkAsIs (e : Expr) : PreTerm :=
+e.mkAnnotation `as_is
+
+def mkPreTypeAscription (p : PreTerm) (expectedType : Expr) : PreTerm :=
+Expr.app (Expr.app (Expr.const `typedExpr []) expectedType) p
+
+def mkPreTypeAscriptionIfSome (p : PreTerm) (expectedType : Option Expr) : PreTerm :=
+match expectedType with
+| none => p
+| some expectedType => mkPreTypeAscription p expectedType
+
 namespace Elab
 
 partial def toLevel : Syntax Expr → Elab Level
@@ -134,12 +145,12 @@ 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
+def oldElaborate (stx : Syntax Expr) (expectedType : Option Expr := none) : Elab Expr :=
+do
   p ← toPreTerm stx;
   scope ← getScope;
   s ← get;
-  match oldElaborateAux s.env scope.options s.mctx scope.lctx p with
+  match oldElaborateAux s.env scope.options s.mctx scope.lctx (mkPreTypeAscriptionIfSome p expectedType) with
   | Except.error (some pos, fmt) => do
     ctx ← read;
     logMessage { fileName := ctx.fileName, pos := pos, text := fmt.pretty scope.options };

library/init/lean/elaborator/term.lean

@@ -10,16 +10,19 @@ import init.lean.elaborator.basic
 namespace Lean
 namespace Elab
 
-def elabTerm (stx : Syntax Expr) : Elab (Syntax Expr) :=
+def elabTerm (stx : Syntax Expr) (expectedType : Option Expr) : Elab (Syntax Expr) :=
 stx.ifNode
   (fun n => do
     s ← get;
     let tables := termElabAttribute.ext.getState s.env;
     let k      := n.getKind;
     match tables.find k with
-    | some elab => elab n
+    | some elab => elab n expectedType
     | none      => logErrorAndThrow stx ("term elaborator failed, no support for syntax '" ++ toString k ++ "'"))
-  (fun _ => throw "term elaborator failed, unexpected syntax")
+  (fun _=>
+    match stx with
+    | Syntax.other e => pure stx
+    | _              => throw "term elaborator failed, unexpected syntax")
 
 end Elab
 end Lean