From 41f4476ca8f87dd7b92dcd60d4e4915a1acabbda Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 12 Dec 2019 15:15:20 -0800 Subject: [PATCH] feat: add synthetic sorry --- src/Init/Core.lean | 2 +- src/Init/Lean/Elab/Term.lean | 16 +++++++++- src/Init/Lean/Util/Sorry.lean | 58 +++++++++++++++++++++++++++++++++++ tests/lean/run/frontend1.lean | 12 +++++--- 4 files changed, 82 insertions(+), 6 deletions(-) create mode 100644 src/Init/Lean/Util/Sorry.lean diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 1da33cb272..2cf6a06317 100644 --- a/src/Init/Core.lean +++ b/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 -/ diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean index a3e1d41e66..9c21ca1905 100644 --- a/src/Init/Lean/Elab/Term.lean +++ b/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 diff --git a/src/Init/Lean/Util/Sorry.lean b/src/Init/Lean/Util/Sorry.lean new file mode 100644 index 0000000000..cc28a63bfc --- /dev/null +++ b/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 diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean index b3e8a00abc..176ca5893a 100644 --- a/tests/lean/run/frontend1.lean +++ b/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