feat: add synthetic sorry

src/Init/Core.lean

@@ -328,7 +328,7 @@ inductive Nat
 /- Auxiliary axiom used to implement `sorry`.
    TODO: add this theorem on-demand. That is,
    we should only add it if after the first error. -/
-unsafe axiom sorryAx (α : Sort u) (synthetic := true) : α
+axiom sorryAx (α : Sort u) (synthetic := true) : α
 
 /- Declare builtin and reserved notation -/
 

src/Init/Lean/Elab/Term.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Init.Lean.Util.Sorry
 import Init.Lean.Meta
 import Init.Lean.Elab.Log
 import Init.Lean.Elab.Alias
@@ -178,6 +179,7 @@ def mkFreshExprMVar (ref : Syntax) (type? : Option Expr := none) (synthetic : Bo
 match type? with
 | some type => liftMetaM ref $ Meta.mkFreshExprMVar type userName? synthetic
 | none      => liftMetaM ref $ do u ← Meta.mkFreshLevelMVar; Meta.mkFreshExprMVar (mkSort u) userName? synthetic
+def getLevel (ref : Syntax) (type : Expr) : TermElabM Level := liftMetaM ref $ Meta.getLevel type
 
 def mkForall (ref : Syntax) (xs : Array Expr) (e : Expr) : TermElabM Expr := liftMetaM ref $ Meta.mkForall xs e
 def trySynthInstance (ref : Syntax) (type : Expr) : TermElabM (LOption Expr) := liftMetaM ref $ Meta.trySynthInstance type
@@ -206,6 +208,15 @@ finally x $ do
 ctx ← read;
 tracingAtPos (ref.getPos.getD ctx.cmdPos) x
 
+def exceptionToSorry (ref : Syntax) (ex : Exception) (expectedType? : Option Expr) : TermElabM Expr := do
+expectedType : Expr ← match expectedType? with
+  | none              => mkFreshExprMVar ref
+  | some expectedType => pure expectedType;
+u ← getLevel ref expectedType;
+let syntheticSorry := mkApp2 (mkConst `sorryAx [u]) expectedType (mkConst `Bool.true);
+unless ex.data.hasSyntheticSorry $ logMessage ex;
+pure syntheticSorry
+
 def elabTerm (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr :=
 withNode stx $ fun node => do
   trace! `Elab.step (toString stx);
@@ -213,7 +224,10 @@ withNode stx $ fun node => do
   let tables := termElabAttribute.ext.getState s.env;
   let k := node.getKind;
   match tables.find k with
-  | some elab => tracingAt stx (elab node expectedType?)
+  | some elab =>
+    catch
+      (tracingAt stx (elab node expectedType?))
+      (fun ex => exceptionToSorry stx ex expectedType?)
   | none      => throwError stx ("elaboration function for '" ++ toString k ++ "' has not been implemented")
 
 def ensureType (ref : Syntax) (e : Expr) : TermElabM Expr := do

src/Init/Lean/Util/Sorry.lean

@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Lean.Util.Message
+
+namespace Lean
+
+def Expr.isSorry : Expr → Bool
+| Expr.app (Expr.app (Expr.const `sorryAx _ _) _ _) _ _ => true
+| _ => false
+
+def Expr.isSyntheticSorry : Expr → Bool
+| Expr.app (Expr.app (Expr.const `sorryAx _ _) _ _) (Expr.const `Bool.true _ _) _ => true
+| _ => false
+
+def Expr.hasSorry : Expr → Bool
+| Expr.const c _ _     => c == `sorryAx
+| Expr.app f a _       => f.hasSorry || a.hasSorry
+| Expr.letE _ t v b _  => t.hasSorry || v.hasSorry || b.hasSorry
+| Expr.forallE _ d b _ => d.hasSorry || b.hasSorry
+| Expr.lam _ d b _     => d.hasSorry || b.hasSorry
+| Expr.mdata _ e _     => e.hasSorry
+| Expr.proj _ _ e _    => e.hasSorry
+| _                    => false
+
+def Expr.hasSyntheticSorry : Expr → Bool
+| e@(Expr.app f a _)   => e.isSyntheticSorry  || f.hasSyntheticSorry || a.hasSyntheticSorry
+| Expr.letE _ t v b _  => t.hasSyntheticSorry || v.hasSyntheticSorry || b.hasSyntheticSorry
+| Expr.forallE _ d b _ => d.hasSyntheticSorry || b.hasSyntheticSorry
+| Expr.lam _ d b _     => d.hasSyntheticSorry || b.hasSyntheticSorry
+| Expr.mdata _ e _     => e.hasSyntheticSorry
+| Expr.proj _ _ e _    => e.hasSyntheticSorry
+| _                    => false
+
+partial def MessageData.hasSorry : MessageData → Bool
+| MessageData.ofExpr e          => e.hasSorry
+| MessageData.context _ _ _ msg => msg.hasSorry
+| MessageData.nest _ msg        => msg.hasSorry
+| MessageData.group msg         => msg.hasSorry
+| MessageData.compose msg₁ msg₂ => msg₁.hasSorry || msg₂.hasSorry
+| MessageData.tagged _ msg      => msg.hasSorry
+| MessageData.node msgs         => msgs.any MessageData.hasSorry
+| _                             => false
+
+partial def MessageData.hasSyntheticSorry : MessageData → Bool
+| MessageData.ofExpr e          => e.hasSyntheticSorry
+| MessageData.context _ _ _ msg => msg.hasSyntheticSorry
+| MessageData.nest _ msg        => msg.hasSyntheticSorry
+| MessageData.group msg         => msg.hasSyntheticSorry
+| MessageData.compose msg₁ msg₂ => msg₁.hasSyntheticSorry || msg₂.hasSyntheticSorry
+| MessageData.tagged _ msg      => msg.hasSyntheticSorry
+| MessageData.node msgs         => msgs.any MessageData.hasSyntheticSorry
+| _                             => false
+
+end Lean

tests/lean/run/frontend1.lean

@@ -3,21 +3,24 @@ open Lean
 open Lean.Elab
 
 
-def run (input : String) : MetaIO Unit :=
+def run (input : String) (failIff : Bool := true) : MetaIO Unit :=
 do env  ← MetaIO.getEnv;
    opts ← MetaIO.getOptions;
    let (env, messages) := process input env opts;
    messages.toList.forM $ fun msg => IO.println msg;
-   when messages.hasErrors $ throw (IO.userError "errors have been found");
+   when (failIff && messages.hasErrors) $ throw (IO.userError "errors have been found");
+   when (!failIff && !messages.hasErrors) $ throw (IO.userError "there are no errors");
    pure ()
 
+def fail (input : String) : MetaIO Unit :=
+run input false
+
 def M := IO Unit
 
 def zero := 0
 def one := 1
 def two := 2
--- set_option trace.Elab.app true
--- set_option trace.Meta true
+def hello : String := "hello"
 
 def act1 : IO String :=
 pure "hello"
@@ -29,6 +32,7 @@ pure "hello"
 #eval run "#check one + two > one ∧ True"
 #eval run "#check act1 >>= IO.println"
 #eval run "#check one + two == one"
+#eval fail "#check one + one + hello == hello ++ one"
 
 #eval run
 "universe u universe v