diff --git a/Auto/Embedding/LamTermInterp.lean b/Auto/Embedding/LamTermInterp.lean index 69de7de..ccc69dd 100644 --- a/Auto/Embedding/LamTermInterp.lean +++ b/Auto/Embedding/LamTermInterp.lean @@ -268,10 +268,10 @@ abbrev InterpM := StateRefT State MetaState.MetaStateM def getLCtxTy! (idx : Nat) : InterpM LamSort := do let lctxTyRev ← getLctxTyRev if idx ≥ lctxTyRev.size then - throwError "getLCtxTy! :: Index out of bound" + throwError "{decl_name%} :: Index out of bound" match lctxTyRev[idx]? with | .some s => return s - | .none => throwError "getLCtxTy! :: Unexpected error" + | .none => throwError "{decl_name%} :: Unexpected error" /-- Turning a sort into `fvar` in a hash-consing manner @@ -303,7 +303,7 @@ def collectSortFor (ltv : LamTyVal) : LamTerm → InterpM LamSort | .atom n => do let _ ← sort2FVarId (ltv.lamVarTy n) return ltv.lamVarTy n -| .etom _ => throwError "collectSortFor :: etoms should not occur here" +| .etom _ => throwError "{decl_name%} :: etoms should not occur here" | .base b => do let s := b.lamCheck ltv let _ ← sort2FVarId s @@ -325,8 +325,8 @@ def collectSortFor (ltv : LamTyVal) : LamTerm → InterpM LamSort if argTy' == argTy && argTy' == s then return resTy else - throwError "collectSortFor :: Application type mismatch" - | _ => throwError "collectSortFor :: Malformed application" + throwError "{decl_name%} :: Application type mismatch" + | _ => throwError "{decl_name%} :: Malformed application" where withLCtxTy {α : Type} (s : LamSort) (k : InterpM α) : InterpM α := do let lctxTyRev ← getLctxTyRev setLctxTyRev (lctxTyRev.push s) diff --git a/Auto/IR/SMT.lean b/Auto/IR/SMT.lean index 1384e37..32c70eb 100644 --- a/Auto/IR/SMT.lean +++ b/Auto/IR/SMT.lean @@ -472,7 +472,7 @@ section if let .some name := h2lMap.get? cstr then return name let .some nameSuggestion := nameSuggestion - | throwError "IR.SMT.h2Symb :: Fresh high-level constraint {cstr} without name suggestion" + | throwError "{decl_name%} :: Fresh high-level constraint {cstr} without name suggestion" let name ← processSuggestedName nameSuggestion setL2hMap (l2hMap.insert name cstr) setH2lMap (h2lMap.insert cstr name) diff --git a/Auto/LemDB.lean b/Auto/LemDB.lean index 9ab8ad6..f7f2a36 100644 --- a/Auto/LemDB.lean +++ b/Auto/LemDB.lean @@ -42,7 +42,7 @@ partial def LemDB.toHashSet : LemDB → AttrM (Std.HashSet Name) let mut ret := Std.HashSet.empty for hdb in hdbs do let some hdb := state.get? hdb - | throwError "LemDB.toHashSet :: Unknown lemma database {hdb}" + | throwError "{decl_name%} :: Unknown lemma database {hdb}" let hset ← hdb.toHashSet ret := ret.insertMany hset return ret diff --git a/Auto/Lib/DeCompile.lean b/Auto/Lib/DeCompile.lean index 4d79c70..f9f2f3a 100644 --- a/Auto/Lib/DeCompile.lean +++ b/Auto/Lib/DeCompile.lean @@ -86,7 +86,7 @@ private partial def exprDeCompileAux (final : Bool) (e : Expr) : ExprDeCompM Str | .natVal l => return toString l | .strVal s => return toString s | Expr.sort l => return s!"Sort ({l})" - | Expr.mvar .. => throwError "exprDeCompile :: Metavariable is not supported" + | Expr.mvar .. => throwError "{decl_name%} :: Metavariable is not supported" | Expr.fvar f => let some decl := (← getLCtx).find? f | throwError "Unknown free variable {e}" @@ -103,9 +103,9 @@ where String.intercalate ", " (us.map toString) ++ "}" etaExpandConst (cst : Expr) (appliedArgs : Nat) := do if !cst.isConst then - throwError s!"exprDeCompile :: etaExpandConst received non-const {cst}" + throwError s!"{decl_name%} :: etaExpandConst received non-const {cst}" let some val := (← getEnv).find? cst.constName! - | throwError s!"exprDeCompile :: Unknown identifier {cst.constName!}" + | throwError s!"{decl_name%} :: Unknown identifier {cst.constName!}" let ty := val.type let lparams := val.levelParams let bs := Expr.forallBinders ty @@ -145,7 +145,7 @@ def exprCollectNames (e : Expr) : StateT (Std.HashSet String) MetaM Unit := do | Expr.mvar .. => return | Expr.fvar f => let some decl := (← getLCtx).find? f - | throwError "Unknown free variable {e}" + | throwError "{decl_name%} :: Unknown free variable {e}" let name := decl.userName.toString modify (fun s => s.insert name) | Expr.bvar .. => return diff --git a/Auto/Lib/ExprExtra.lean b/Auto/Lib/ExprExtra.lean index a83f10b..336d554 100644 --- a/Auto/Lib/ExprExtra.lean +++ b/Auto/Lib/ExprExtra.lean @@ -203,7 +203,7 @@ def Expr.depArgs (e : Expr) : Array Nat := ⟨Expr.depArgsIdx e 0⟩ -/ def Expr.constDepArgs (c : Name) : CoreM (Array Nat) := do let .some decl := (← getEnv).find? c - | throwError "Expr.constDepArgs :: Unknown constant {c}" + | throwError "{decl_name%} :: Unknown constant {c}" return Expr.depArgs decl.type def Expr.numLeadingDepArgs : Expr → Nat @@ -234,14 +234,14 @@ def Expr.formatWithUsername (e : Expr) : MetaM Format := do let names ← fvarIds.mapM (fun fid => do match ← fid.findDecl? with | .some decl => return decl.userName - | .none => throwError "Expr.formatWithUsername :: Unknown free variable {(Expr.fvar fid).dbgToString}") + | .none => throwError "{decl_name%}e :: Unknown free variable {(Expr.fvar fid).dbgToString}") let e := e.replaceFVars (fvarIds.map Expr.fvar) (names.map (Expr.const · [])) let e ← instantiateMVars e let mvarIds := (Expr.collectMVars {} e).result let names ← mvarIds.mapM (fun mid => do match ← mid.findDecl? with | .some decl => return decl.userName - | .none => throwError "xpr.formatWithUsername :: Unknown metavariable {(Expr.mvar mid).dbgToString}") + | .none => throwError "{decl_name%} :: Unknown metavariable {(Expr.mvar mid).dbgToString}") let e := (e.abstract (mvarIds.map Expr.mvar)).instantiateRev (names.map (Expr.const · [])) return f!"{e}" @@ -257,14 +257,14 @@ unsafe def elabGetExprAndApply : CommandElab := fun stx => match stx with | `(command | #getExprAndApply[ $t:term | $i:ident ]) => withRef stx <| do let some iexpr ← Term.resolveId? i - | throwError "elabGetExprAndApply :: Unknown identifier {i}" + | throwError "{decl_name%} :: Unknown identifier {i}" let e ← Term.elabTerm t none Term.synthesizeSyntheticMVarsNoPostponing (ignoreStuckTC := true) let e ← Term.levelMVarToParam (← instantiateMVars e) let fname := iexpr.constName! match (← getEnv).evalConst (Expr → TermElabM Unit) (← getOptions) fname with | Except.ok f => f e - | Except.error err => throwError "elabGetExprAndApply :: Failed to evaluate {fname} to a term of type (Expr → TermElabM Unit), error : {err}" + | Except.error err => throwError "{decl_name%} :: Failed to evaluate {fname} to a term of type (Expr → TermElabM Unit), error : {err}" | _ => throwUnsupportedSyntax /-- @@ -274,7 +274,7 @@ unsafe def elabGetExprAndApply : CommandElab := fun stx => unsafe def exprFromExpr (eToExpr : Expr) : TermElabM Expr := do let ty ← Meta.inferType eToExpr if ! (← Meta.isDefEq ty (.const ``Expr [])) then - throwError "exprFromExpr :: Type `{ty}` of input is not definitionally equal to `Expr`" + throwError "{decl_name%} :: Type `{ty}` of input is not definitionally equal to `Expr`" let declName := `_exprFromExpr let addAndCompile (value : Expr) : TermElabM Unit := do let value ← Term.levelMVarToParam (← instantiateMVars value) @@ -359,7 +359,7 @@ section EvalAtTermElabM let α ← reduce (skipTypes := false) α synthInstance (mkApp (Lean.mkConst evalClassName [u]) α) catch _ => - throwError "expression{indentExpr e}\nhas type{indentExpr α}\nbut instance{indentExpr inst}\nfailed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `{evalClassName}` class" + throwError "{decl_name%} :: expression{indentExpr e}\nhas type{indentExpr α}\nbut instance{indentExpr inst}\nfailed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `{evalClassName}` class" private def mkRunMetaEval (e : Expr) : MetaM Expr := withLocalDeclD `env (mkConst ``Lean.Environment) fun env => diff --git a/Auto/Lib/MetaExtra.lean b/Auto/Lib/MetaExtra.lean index 25e0f56..b16d25d 100644 --- a/Auto/Lib/MetaExtra.lean +++ b/Auto/Lib/MetaExtra.lean @@ -40,7 +40,7 @@ def Meta.inspectMVarAssignments : MetaM Unit := do def Meta.trySynthInhabited (e : Expr) : MetaM (Option Expr) := do let eSort ← Expr.normalizeType (← instantiateMVars (← Meta.inferType e)) let .sort lvl := eSort - | throwError "trySynthInhabited :: {e} is not a type" + | throwError "{decl_name%} :: {e} is not a type" try if let .some inh ← Meta.synthInstance? e then return .some inh @@ -58,10 +58,10 @@ syntax (name := fromMetaTactic) "fromMetaTactic" "[" ident "]" : tactic unsafe def evalFromMetaTactic : Tactic.Tactic | `(fromMetaTactic | fromMetaTactic [ $i ]) => do let some iexpr ← Term.resolveId? i - | throwError "evalFromMetaTactic :: Unknown identifier {i}" + | throwError "{decl_name%} :: Unknown identifier {i}" let mtname := iexpr.constName! let Except.ok mt := (← getEnv).evalConst (MVarId → MetaM (List MVarId)) (← getOptions) mtname - | throwError "evalFromMetaTactic :: Failed to evaluate {mtname} to a term of type (Expr → TermElabM Unit)" + | throwError "{decl_name%} :: Failed to evaluate {mtname} to a term of type (Expr → TermElabM Unit)" Tactic.liftMetaTactic mt | _ => Elab.throwUnsupportedSyntax diff --git a/Auto/Lib/MetaState.lean b/Auto/Lib/MetaState.lean index 458d95d..abfe707 100644 --- a/Auto/Lib/MetaState.lean +++ b/Auto/Lib/MetaState.lean @@ -75,7 +75,7 @@ private def runWithFVars (lctx : LocalContext) (fvarids : Array FVarId) (k : Met newlctx := newlctx.mkLocalDecl fvarId userName type bi kind | .ldecl _ fvarId userName type value nonDep kind => newlctx := newlctx.mkLetDecl fvarId userName type value nonDep kind - | .none => throwError "runWithFVars :: Unknown free variable {Expr.fvar fid}" + | .none => throwError "{decl_name%} :: Unknown free variable {Expr.fvar fid}" withReader (fun ctx => {ctx with lctx := newlctx}) k private def runWithIntroducedFVarsImp (m : MetaStateM (Array FVarId × α)) (k : α → MetaM β) : MetaM β := do diff --git a/Auto/Lib/MonadUtils.lean b/Auto/Lib/MonadUtils.lean index ba33e99..57bbda7 100644 --- a/Auto/Lib/MonadUtils.lean +++ b/Auto/Lib/MonadUtils.lean @@ -53,13 +53,13 @@ syntax (name := genMonadState) "#genMonadState" term : command -/ def structureProjs (structTy : Expr) : CoreM (Name × Expr × Array (Name × Expr)) := do let .const structName lvls := structTy.getAppFn - | throwError s!"structureProjs :: Head symbol of {structTy} is not a constant" + | throwError s!"{decl_name%} :: Head symbol of {structTy} is not a constant" let some structInfo := getStructureInfo? (← getEnv) structName - | throwError s!"structureProjs :: {structName} is not a structure" + | throwError s!"{decl_name%} :: {structName} is not a structure" let .some (.inductInfo structi) := (← getEnv).find? structName - | throwError s!"structureProjs :: Unknown identifier {structName}" + | throwError s!"{decl_name%} :: Unknown identifier {structName}" let [structDotMk] := structi.ctors - | throwError s!"structureProjs :: {structName} is not a structure" + | throwError s!"{decl_name%} :: {structName} is not a structure" let structMkExpr := mkAppN (Expr.const structDotMk lvls) structTy.getAppArgs let tyArgs := structTy.getAppArgs let nameMap : Std.HashMap Name StructureFieldInfo := Std.HashMap.ofList @@ -75,7 +75,7 @@ private def elabStx (stx : Term) : TermElabM Expr := do Term.synthesizeSyntheticMVarsNoPostponing (ignoreStuckTC := true) let e ← instantiateMVars expr if e.hasMVar then - throwError "elabStx :: {e} contains metavariables" + throwError "{decl_name%} :: {e} contains metavariables" return e private def addDefnitionValFromExpr (e : Expr) (name : Name) : MetaM Unit := do @@ -91,9 +91,9 @@ private def addDefnitionValFromExpr (e : Expr) (name : Name) : MetaM Unit := do private def elabGenMonadContextAux (m : Term) (stx : Syntax) : CommandElabM Unit := runTermElabM <| fun xs => do let mexpr ← elabStx m let .const mname _ := mexpr.getAppFn - | throwError "elabGenMonadContext :: Unknown monad" + | throwError "{decl_name%} :: Unknown monad" let .str pre _ := mname - | throwError "elabGenMonadContext :: {mname} is not a valid constant name" + | throwError "{decl_name%} :: {mname} is not a valid constant name" let pureInst ← elabStx (← `(inferInstanceAs (Pure $m))) let mctxInst ← elabStx (← `(inferInstanceAs (MonadReader _ $m))) let mctxInstTy ← Meta.inferType mctxInst @@ -122,9 +122,9 @@ where private def elabGenMonadStateAux (m : Term) (stx : Syntax) : CommandElabM Unit := runTermElabM <| fun xs => do let mexpr ← elabStx m let .const mname _ := mexpr.getAppFn - | throwError "elabGenMonadState :: Unknown monad" + | throwError "{decl_name%} :: Unknown monad" let .str pre _ := mname - | throwError "elabGenMonadState :: {mname} is not a valid constant name" + | throwError "{decl_name%} :: {mname} is not a valid constant name" let pureInst ← elabStx (← `(inferInstanceAs (Pure $m))) let mstateInst ← elabStx (← `(inferInstanceAs (MonadState _ $m))) let mstateInstTy ← Meta.inferType mstateInst diff --git a/Auto/Parser/TPTP.lean b/Auto/Parser/TPTP.lean index 15351c7..fd66be9 100644 --- a/Auto/Parser/TPTP.lean +++ b/Auto/Parser/TPTP.lean @@ -854,8 +854,8 @@ def getProof (lamVarTy lamEVarTy : Array LamSort) (cmds : Array Command) : MetaM match term2LamTerm pi val with | .term (.base .prop) t => ret := ret.push t - | .error e => throwError ("getProof :: " ++ e) - | lc => throwError "getProof :: Unexpected LamConstr {lc}, expected term" + | .error e => throwError (decl_name% ++ " :: " ++ e) + | lc => throwError "{decl_name%} :: Unexpected LamConstr {lc}, expected term" else match val with | ⟨.ident name, [ty]⟩ => @@ -863,13 +863,13 @@ def getProof (lamVarTy lamEVarTy : Array LamSort) (cmds : Array Command) : MetaM if name.take 3 == "sk_" then match term2LamTerm pi ty with | .sort s => pi := pi.addSkolem name s - | lc => throwError "getProof :: Unexpected LamConstr {lc}, expected sort" + | lc => throwError "{decl_name%} :: Unexpected LamConstr {lc}, expected sort" else continue | _ => continue | _ => continue - | "include" => throwError "getProof :: `include` should not occur in proof output of TPTP solvers" - | _ => throwError "getProof :: Unknown command {cmd}" + | "include" => throwError "{decl_name%} :: `include` should not occur in proof output of TPTP solvers" + | _ => throwError "{decl_name%} :: Unknown command {cmd}" return ret /-- Returns the unsat core of an array of TSTP steps -/ diff --git a/Auto/Solver/Native.lean b/Auto/Solver/Native.lean index ebfa75d..61181ae 100644 --- a/Auto/Solver/Native.lean +++ b/Auto/Solver/Native.lean @@ -42,7 +42,7 @@ opaque queryNative : Array Lemma → Array Lemma → MetaM Expr def emulateNative (lemmas : Array Lemma) (_ : Array Lemma) : MetaM Expr := do let _ ← lemmas.mapM (fun lem => do if lem.params.size != 0 then - throwError "Solver.emulateNative :: Universe levels parameters are not supported") + throwError "{decl_name%} :: Universe levels parameters are not supported") let descrs := lemmas.zipWithIndex.map (fun (lem, i) => (Name.mkSimple s!"lem{i}", lem.type, .default)) let sty := Expr.mkForallFromBinderDescrs descrs (.const ``False []) let sorryExpr := Lean.mkApp2 (.const ``sorryAx [.zero]) sty (.const ``Bool.false []) diff --git a/Auto/Solver/SMT.lean b/Auto/Solver/SMT.lean index 06687c5..67fca0d 100644 --- a/Auto/Solver/SMT.lean +++ b/Auto/Solver/SMT.lean @@ -97,7 +97,7 @@ private def emitCommands (p : SolverProc) (c : Array IR.SMT.Command) : IO Unit : def createSolver (name : SolverName) : MetaM SolverProc := do let tlim := auto.smt.timeout.get (← getOptions) match name with - | .none => throwError "createSolver :: Unexpected error" + | .none => throwError "{decl_name%} :: Unexpected error" | .z3 => createAux "z3" #["-in", "-smt2", s!"-T:{tlim}"] | .cvc4 => throwError "cvc4 is not supported" | .cvc5 => createAux "cvc5" #[s!"--tlimit={tlim * 1000}", "--produce-models"] @@ -111,31 +111,31 @@ axiom autoSMTSorry.{u} (α : Sort u) : α def getSexp (s : String) : MetaM (Sexp × String) := match parseSexp s ⟨0⟩ {} with | .complete se p => return (se, Substring.toString ⟨s, p, s.endPos⟩) - | .incomplete _ _ => throwError s!"getSexp :: Incomplete input {s}" - | .malformed => throwError s!"getSexp :: Malformed (prefix of) input {s}" + | .incomplete _ _ => throwError s!"{decl_name%} :: Incomplete input {s}" + | .malformed => throwError s!"{decl_name%} :: Malformed (prefix of) input {s}" /-- Recover id of valid facts from unsat core. Refer to `lamFOL2SMT` -/ def validFactOfUnsatCore (unsatCore : Sexp) : MetaM (Array Nat) := do let .app unsatCore := unsatCore - | throwError "validFactOfUnsatCore :: Malformed unsat core `{unsatCore}`" + | throwError "{decl_name%} :: Malformed unsat core `{unsatCore}`" let mut ret := #[] for sexp in unsatCore do let .atom (.symb name) := sexp | continue if name.take 11 == "valid_fact_" then let .some n := (name.drop 11).toNat? - | throwError "validFactOfUnsatCore :: The id {name.drop 11} of {name} is invalid" + | throwError "{decl_name%} :: The id {name.drop 11} of {name} is invalid" ret := ret.push n return ret /-- Only put declarations in the query -/ def querySolver (query : Array IR.SMT.Command) : MetaM (Option (Sexp × String)) := do if !(auto.smt.get (← getOptions)) then - throwError "querySolver :: Unexpected error" + throwError "{decl_name%} :: Unexpected error" if (auto.smt.solver.name.get (← getOptions) == .none) then - logInfo "querySolver :: Skipped" + logInfo s!"{decl_name%} :: Skipped" return .none let name := auto.smt.solver.name.get (← getOptions) let solver ← createSolver name @@ -175,7 +175,7 @@ def querySolver (query : Array IR.SMT.Command) : MetaM (Option (Sexp × String)) def saveQuery (query : Array IR.SMT.Command) : MetaM Unit := do if !(auto.smt.save.get (← getOptions)) then - throwError "querySolver :: Unexpected error" + throwError "{decl_name%} :: Unexpected error" let path := auto.smt.savepath.get (← getOptions) IO.FS.withFile path IO.FS.Mode.write fun fd => for cmd in query do diff --git a/Auto/Solver/TPTP.lean b/Auto/Solver/TPTP.lean index f5c4f70..121b236 100644 --- a/Auto/Solver/TPTP.lean +++ b/Auto/Solver/TPTP.lean @@ -114,7 +114,7 @@ def queryZEPort (zept : ZEPortType) (query : String) : MetaM String := do catch e => let estr := toString (← (Exception.toMessageData e).format) if estr.extract ⟨0⟩ ⟨44⟩ != "already exists (error code: 17, file exists)" then - throwError "queryZEPort :: Unexpected error" + throwError "{decl_name%} :: Unexpected error" idx := idx + (← IO.rand 0 100) IO.FS.withFile s!"./.zeport_ignore/problem{idx}.p" .writeNew (fun stream => stream.putStr query) let solver ← createSolver path idx @@ -149,7 +149,7 @@ def queryE (query : String) : MetaM String := do def querySolver (query : String) : MetaM (Array Parser.TPTP.Command) := do if !(auto.tptp.get (← getOptions)) then - throwError "querySolver :: Unexpected error" + throwError "{decl_name%} :: Unexpected error" let stdout ← (do match auto.tptp.solver.name.get (← getOptions) with | .zipperposition => queryZipperposition query diff --git a/Auto/Tactic.lean b/Auto/Tactic.lean index 20060ff..ddee40c 100644 --- a/Auto/Tactic.lean +++ b/Auto/Tactic.lean @@ -87,11 +87,11 @@ def parseUnfolds : TSyntax ``unfolds → TacticM (Array Prep.ConstUnfoldInfo) | `(unfolds| u[ $[$hs],* ]) => do let exprs ← hs.mapM (fun i => do let some expr ← Term.resolveId? i - | throwError "parseUnfolds :: Unknown identifier {i}. {defeqUnfoldErrHint}" + | throwError "{decl_name%} :: Unknown identifier {i}. {defeqUnfoldErrHint}" return expr) exprs.mapM (fun expr => do let some name := expr.constName? - | throwError "parseUnfolds :: Unknown declaration {expr}. {defeqUnfoldErrHint}" + | throwError "{decl_name%} :: Unknown declaration {expr}. {defeqUnfoldErrHint}" Prep.getConstUnfoldInfo name) | _ => throwUnsupportedSyntax @@ -99,11 +99,11 @@ def parseDefeqs : TSyntax ``defeqs → TacticM (Array Name) | `(defeqs| d[ $[$hs],* ]) => do let exprs ← hs.mapM (fun i => do let some expr ← Term.resolveId? i - | throwError "parseDefeqs :: Unknown identifier {i}. {defeqUnfoldErrHint}" + | throwError "{decl_name%} :: Unknown identifier {i}. {defeqUnfoldErrHint}" return expr) exprs.mapM (fun expr => do let some name := expr.constName? - | throwError "parseDefeqs :: Unknown declaration {expr}. {defeqUnfoldErrHint}" + | throwError "{decl_name%} :: Unknown declaration {expr}. {defeqUnfoldErrHint}" return name) | _ => throwUnsupportedSyntax @@ -121,12 +121,12 @@ def parseUOrDs (stxs : Array (TSyntax ``uord)) : TacticM (Array Prep.ConstUnfold match ← parseUOrD stx with | .inl u => if hasUnfolds then - throwError "Auto :: Duplicated unfold hint" + throwError "{decl_name%} :: Duplicated unfold hint" hasUnfolds := true unfolds := u | .inr d => if hasDefeqs then - throwError "Auto :: Duplicated defeq hint" + throwError "{decl_name%} :: Duplicated defeq hint" hasDefeqs := true defeqs := defeqs.append d return (unfolds, defeqs) @@ -262,7 +262,7 @@ def queryTPTP (exportFacts : Array REntry) : LamReif.ReifM (Array Embedding.Lam. let exportLamTerms ← exportFacts.mapM (fun re => do match re with | .valid [] t => return t - | _ => throwError "runAuto :: Unexpected error") + | _ => throwError "{decl_name%} :: Unexpected error") let query ← lam2TH0 lamVarTy lamEVarTy exportLamTerms trace[auto.tptp.printQuery] "\n{query}" let tptpProof ← Solver.TPTP.querySolver query @@ -276,7 +276,7 @@ def queryTPTP (exportFacts : Array REntry) : LamReif.ReifM (Array Embedding.Lam. let mut ret := #[] for n in unsatCore do let .some re := exportFacts[n]? - | throwError "queryTPTP :: Index {n} out of range" + | throwError "{decl_name%} :: Index {n} out of range" ret := ret.push re return ret @@ -287,7 +287,7 @@ def querySMT (exportFacts : Array REntry) (exportInds : Array MutualIndInfo) : L let exportLamTerms ← exportFacts.mapM (fun re => do match re with | .valid [] t => return t - | _ => throwError "runAuto :: Unexpected error") + | _ => throwError "{decl_name%} :: Unexpected error") let sni : SMT.SMTNamingInfo := {tyVal := (← LamReif.getTyVal), varVal := (← LamReif.getVarVal), lamEVarTy := (← LamReif.getLamEVarTy)} let ((commands, validFacts), state) ← (lamFOL2SMT sni lamVarTy lamEVarTy exportLamTerms exportInds).run @@ -307,20 +307,20 @@ def querySMT (exportFacts : Array REntry) (exportInds : Array MutualIndInfo) : L -- **Print STerms corresponding to `validFacts` in unsatCore** for id in unsatCoreIds do let .some sterm := validFacts[id]? - | throwError "runAuto :: Index {id} of `validFacts` out of range" + | throwError "{decl_name%} :: Index {id} of `validFacts` out of range" trace[auto.smt.unsatCore.smtTerms] "|valid_fact_{id}| : {sterm}" -- **Print Lean expressions correesponding to `validFacts` in unsatCore** SMT.withExprValuation sni state.h2lMap (fun tyValMap varValMap etomValMap => do for id in unsatCoreIds do let .some t := exportLamTerms[id]? - | throwError "runAuto :: Index {id} of `exportLamTerms` out of range" + | throwError "{decl_name%} :: Index {id} of `exportLamTerms` out of range" let e ← Lam2D.interpLamTermAsUnlifted tyValMap varValMap etomValMap 0 t trace[auto.smt.unsatCore.leanExprs] "|valid_fact_{id}| : {← Core.betaReduce e}" ) -- **Print derivation of unsatCore** for id in unsatCoreIds do let .some t := exportLamTerms[id]? - | throwError "runAuto :: Index {id} of `exportLamTerm` out of range" + | throwError "{decl_name%} :: Index {id} of `exportLamTerm` out of range" let vderiv ← LamReif.collectDerivFor (.valid [] t) trace[auto.smt.unsatCore.deriv] "|valid_fact_{id}| : {vderiv}" if auto.smt.rconsProof.get (← getOptions) then @@ -392,18 +392,18 @@ def callNative_direct (Lam2DAAF.callNativeWithAtomAsFVar nonemptiesWithDTr validsWithDTr prover).run' { tyVal := tyVal, varVal := varVal, lamEVarTy := lamEVarTy } if usedEtoms.size != 0 then - throwError "callNative_direct :: etoms should not occur here" + throwError "{decl_name%} :: etoms should not occur here" let ss ← usedInhs.mapM (fun re => do match ← lookupREntryProof! re with | .inhabitation e _ _ => return e | .chkStep (.n (.nonemptyOfAtom n)) => match varVal[n]? with | .some (e, _) => return e - | .none => throwError "callNative_direct :: Unexpected error" - | _ => throwError "callNative_direct :: Cannot find external proof of {re}") + | .none => throwError "{decl_name%} :: Unexpected error" + | _ => throwError "{decl_name%} :: Cannot find external proof of {re}") let ts ← usedHyps.mapM (fun re => do let .assertion e _ _ ← lookupREntryProof! re - | throwError "callNative_direct :: Cannot find external proof of {re}" + | throwError "{decl_name%} :: Cannot find external proof of {re}" return e) return mkAppN proof (ss ++ ts) @@ -484,7 +484,7 @@ def evalAuto : Tactic -- now the goal is just `G` let (goalBinders, newGoal) ← (← getMainGoal).intros let [nngoal] ← newGoal.apply (.const ``Classical.byContradiction []) - | throwError "evalAuto :: Unexpected result after applying Classical.byContradiction" + | throwError "{decl_name%} :: Unexpected result after applying Classical.byContradiction" let (ngoal, absurd) ← MVarId.intro1 nngoal replaceMainGoal [absurd] withMainContext do @@ -505,7 +505,7 @@ def evalIntromono : Tactic | `(intromono | intromono $hints $[$uords]*) => withMainContext do let (goalBinders, newGoal) ← (← getMainGoal).intros let [nngoal] ← newGoal.apply (.const ``Classical.byContradiction []) - | throwError "evalAuto :: Unexpected result after applying Classical.byContradiction" + | throwError "{decl_name%} :: Unexpected result after applying Classical.byContradiction" let (ngoal, absurd) ← MVarId.intro1 nngoal replaceMainGoal [absurd] withMainContext do @@ -552,12 +552,12 @@ def runNativeProverWithAuto if let .some expr ← queryNative declName? exportFacts exportInhs prover then return expr else - throwError "runNativeProverWithAuto :: Failed to find proof") + throwError "{decl_name%} :: Failed to find proof") let (proof, _) ← Monomorphization.monomorphize lemmas inhFacts (@id (Reif.ReifM Expr) do let s ← get let u ← computeMaxLevel s.facts (afterReify s.facts s.inhTys).run' {u := u}) - trace[auto.tactic] "runNativeProverWithAuto :: Found proof of {← Meta.inferType proof}" + trace[auto.tactic] "{decl_name%} :: Found proof of {← Meta.inferType proof}" return proof @[tactic mononative] @@ -568,7 +568,7 @@ def evalMonoNative : Tactic -- now the goal is just `G` let (goalBinders, newGoal) ← (← getMainGoal).intros let [nngoal] ← newGoal.apply (.const ``Classical.byContradiction []) - | throwError "evalAuto :: Unexpected result after applying Classical.byContradiction" + | throwError "{decl_name%} :: Unexpected result after applying Classical.byContradiction" let (ngoal, absurd) ← MVarId.intro1 nngoal replaceMainGoal [absurd] withMainContext do diff --git a/Auto/Translation/Assumptions.lean b/Auto/Translation/Assumptions.lean index 17ff339..c332a03 100644 --- a/Auto/Translation/Assumptions.lean +++ b/Auto/Translation/Assumptions.lean @@ -73,7 +73,7 @@ def Lemma.betaReduceType (lem : Lemma) : CoreM Lemma := do /-- Create a `Lemma` out of a constant, given the name of the constant -/ def Lemma.ofConst (name : Name) (deriv : DTr) : CoreM Lemma := do let .some decl := (← getEnv).find? name - | throwError "Lemma.ofConst :: Unknown constant {name}" + | throwError "{decl_name%} :: Unknown constant {name}" let type := decl.type let params := decl.levelParams return ⟨⟨.const name (params.map Level.param), type, deriv⟩, ⟨params⟩⟩ @@ -125,7 +125,7 @@ def Lemma.reorderForallInstDep (lem : Lemma) : MetaM Lemma := do def Lemma.rewriteUMonoRigid? (lem : Lemma) (rw : UMonoFact) : MetaM (Option Lemma) := do let ⟨rwproof, rwtype, rwDeriv⟩ := rw let .some (α, lhs, rhs) ← Meta.matchEq? rwtype - | throwError "Lemma.rewriteUMonoRigid :: {rwtype} is not an equality" + | throwError "{decl_name%} :: {rwtype} is not an equality" let ⟨⟨proof, e, lemDeriv⟩, params⟩ := lem let eAbst ← Meta.kabstract e lhs unless eAbst.hasLooseBVars do @@ -133,7 +133,7 @@ def Lemma.rewriteUMonoRigid? (lem : Lemma) (rw : UMonoFact) : MetaM (Option Lemm let eNew := eAbst.instantiate1 rhs let motive := mkLambda `_a BinderInfo.default α eAbst unless (← Meta.isTypeCorrect motive) do - throwError "Lemma.rewriteUMonoRigid :: Motive {motive} is not type correct" + throwError "{decl_name%} :: Motive {motive} is not type correct" let eqPrf ← Meta.mkEqNDRec motive proof rwproof return .some ⟨⟨eqPrf, eNew, .node "rw" #[lemDeriv, rwDeriv]⟩, params⟩ @@ -149,16 +149,16 @@ def Lemma.rewriteUPolyRigid (lem : Lemma) (rw : Lemma) : MetaM Lemma := do let s ← saveState -- Test whether `rhs` contains `lhs let .some (_, lhs, rhs) ← Meta.matchEq? rw.type - | throwError "Lemma.rewriteUMonoRigid :: {rw.type} is not an equality" + | throwError "{decl_name%} :: {rw.type} is not an equality" let lhs' := lhs.instantiateLevelParamsArray rw.params (← rw.params.mapM (fun _ => Meta.mkFreshLevelMVar)) let rhs' := rhs.instantiateLevelParamsArray rw.params (← rw.params.mapM (fun _ => Meta.mkFreshLevelMVar)) if (← Meta.kabstract rhs' lhs').hasLooseBVars then - throwError "Lemma.rewriteUPolyRigid :: Right-hand side {rhs} of equality contains left-hand side {lhs}" + throwError "{decl_name%} :: Right-hand side {rhs} of equality contains left-hand side {lhs}" restoreState s while true do let umvars ← rw.params.mapM (fun _ => Meta.mkFreshLevelMVar) let .some urw := (rw.instantiateLevelParamsArray umvars).toUMonoFact? - | throwError "Lemma.rewriteUPolyRigid :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" let .some lem' ← Lemma.rewriteUMonoRigid? lem urw | break let restmvars := (← umvars.mapM Level.collectLevelMVars).concatMap id @@ -219,7 +219,7 @@ def LemmaInst.ofLemmaLeadingDepOnly (lem : Lemma) : MetaM LemmaInst := do let nld := Expr.numLeadingDepArgs type Meta.forallBoundedTelescope type nld fun xs _ => do if xs.size != nld then - throwError "LemmaInst.ofLemmaLeadingDepOnly :: Unexpected error" + throwError "{decl_name%} :: Unexpected error" let proof ← Meta.mkLambdaFVars xs (mkAppN proof xs) let lem' : Lemma := ⟨⟨proof, type, deriv⟩, params⟩ return ⟨lem', xs.size, xs.size⟩ @@ -235,19 +235,19 @@ instance : ToMessageData LemmaInst where def LemmaInst.subsumeQuick (li₁ li₂ : LemmaInst) : MetaM Bool := Meta.withNewMCtxDepth <| do if li₁.nargs != li₂.nargs then - throwError "LemmaInst.subsumeQuick :: {li₁} and {li₂} are not instance of the same lemma" + throwError "{decl_name%} :: {li₁} and {li₂} are not instance of the same lemma" let lem₁ := li₁.toLemma let lem₂ := li₂.toLemma let (_, _, body₂) ← Meta.lambdaMetaTelescope lem₂.proof li₂.nbinders let args₂ := Expr.getAppBoundedArgs li₂.nargs body₂ if args₂.size != li₂.nargs then - throwError "LemmaInst.subsumeQuick :: {li₂} is expected to have {li₂.nargs} args, but actually has {args₂.size}" + throwError "{decl_name%} :: {li₂} is expected to have {li₂.nargs} args, but actually has {args₂.size}" Meta.withNewMCtxDepth do let paramInst₁ ← lem₁.params.mapM (fun _ => Meta.mkFreshLevelMVar) let (_, _, body₁) ← Meta.lambdaMetaTelescope lem₁.proof li₁.nbinders let args₁ := Expr.getAppBoundedArgs li₁.nargs body₁ if args₁.size != li₁.nargs then - throwError "LemmaInst.subsumeQuick :: {li₁} is expected to have {li₁.nargs} args, but actually has {args₁.size}" + throwError "{decl_name%} :: {li₁} is expected to have {li₁.nargs} args, but actually has {args₁.size}" let args₁ := args₁.map (fun e => e.instantiateLevelParamsArray lem₁.params paramInst₁) for (arg₁, arg₂) in args₁.zip args₂ do if !(← Meta.isDefEq arg₁ arg₂) then @@ -288,10 +288,10 @@ def MLemmaInst.ofLemmaInst (li : LemmaInst) : MetaM (Array Level × Array Expr let type := type.instantiateLevelParamsArray params lvls let (mvars, _, proof) ← Meta.lambdaMetaTelescope proof li.nbinders let .some origProof := Expr.getAppFnN li.nargs proof - | throwError "MLemmaInst.ofLemmaInst :: Insufficient number of arguments" + | throwError "{decl_name%} :: Insufficient number of arguments" let args := Expr.getAppBoundedArgs li.nargs proof if args.size != li.nargs then - throwError "MLemmaInst.ofLemmaInst :: Unexpected error" + throwError "{decl_name%} :: Unexpected error" let type ← Meta.instantiateForall type mvars return (lvls, mvars, ⟨origProof, args, type, deriv⟩) @@ -340,7 +340,7 @@ partial def collectUniverseLevels : Expr → MetaM (Std.HashSet Level) return mergeHashSet (mergeHashSet tys vs) bodys | .lit _ => return Std.HashSet.empty.insert (.succ .zero) | .mdata _ e' => collectUniverseLevels e' -| .proj .. => throwError "Please unfold projections before collecting universe levels" +| .proj .. => throwError "{decl_name%} :: Please unfold projections before collecting universe levels" def computeMaxLevel (facts : Array UMonoFact) : MetaM Level := do let levels ← facts.foldlM (fun hs ⟨_, ty, _⟩ => do diff --git a/Auto/Translation/Inductive.lean b/Auto/Translation/Inductive.lean index 52b6083..fff8a96 100644 --- a/Auto/Translation/Inductive.lean +++ b/Auto/Translation/Inductive.lean @@ -18,7 +18,7 @@ namespace Auto -/ def isFamily (tyctorname : Name) : CoreM Bool := do let .some (.inductInfo val) := (← getEnv).find? tyctorname - | throwError "isFamily :: {tyctorname} is not a type constructor" + | throwError "{decl_name%} :: {tyctorname} is not a type constructor" return (Expr.forallBinders val.type).size != val.numParams /-- @@ -26,7 +26,7 @@ def isFamily (tyctorname : Name) : CoreM Bool := do -/ def isIndProp (tyctorname : Name) : CoreM Bool := do let .some (.inductInfo val) := (← getEnv).find? tyctorname - | throwError "isIndProp :: {tyctorname} is not a type constructor" + | throwError "{decl_name%} :: {tyctorname} is not a type constructor" (Meta.withTransparency (n := MetaM) .all <| Meta.forallTelescopeReducing val.type fun _ body => Meta.isDefEq body (.sort .zero)).run' {} @@ -36,7 +36,7 @@ def isIndProp (tyctorname : Name) : CoreM Bool := do -/ def isSimpleCtor (ctorname : Name) : CoreM Bool := do let .some (.ctorInfo val) := (← getEnv).find? ctorname - | throwError "isSimpleCtor :: {ctorname} is not a type constructor" + | throwError "{decl_name%} :: {ctorname} is not a type constructor" Meta.MetaM.run' <| Meta.forallBoundedTelescope val.type val.numParams fun _ body => pure ((Expr.depArgs body).size == 0) @@ -46,7 +46,7 @@ def isSimpleCtor (ctorname : Name) : CoreM Bool := do -/ def isSimpleInductive (tyctorname : Name) : CoreM Bool := do let .some (.inductInfo val) := (← getEnv).find? tyctorname - | throwError "isSimple :: {tyctorname} is not a type constructor" + | throwError "{decl_name%} :: {tyctorname} is not a type constructor" return (← val.ctors.allM isSimpleCtor) && !(← isFamily tyctorname) structure SimpleIndVal where @@ -90,7 +90,7 @@ abbrev IndCollectM := StateRefT CollectInduct.State MetaM private def collectSimpleInduct (tyctor : Name) (lvls : List Level) (args : Array Expr) : MetaM SimpleIndVal := do let .some (.inductInfo val) := (← getEnv).find? tyctor - | throwError "collectSimpleInduct :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" let ctors ← (Array.mk val.ctors).mapM (fun ctorname => do let instctor := mkAppN (Expr.const ctorname lvls) args let type ← Meta.inferType instctor @@ -100,7 +100,7 @@ private def collectSimpleInduct let projs ← (getStructureInfo? env tyctor).mapM (fun si => do si.fieldNames.mapM (fun fieldName => do let .some projFn := getProjFnForField? env tyctor fieldName - | throwError "collectSimpleInduct :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" return mkAppN (Expr.const projFn lvls) args)) return ⟨tyctor, mkAppN (Expr.const tyctor lvls) args, ctors, projs⟩ @@ -128,7 +128,7 @@ mutual if !(← getRecorded).contains tyctor then setRecorded ((← getRecorded).insert tyctor #[]) let .some arr := (← getRecorded).get? tyctor - | throwError "collectAppInstSimpleInduct :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" for e' in arr do if ← Meta.isDefEq e e' then return @@ -151,9 +151,9 @@ mutual return collectExprSimpleInduct ty collectExprSimpleInduct body - | .letE .. => throwError "collectExprSimpleInduct :: Let-expressions should have been reduced" - | .mdata .. => throwError "collectExprSimpleInduct :: mdata should have been consumed" - | .proj .. => throwError "collectExprSimpleInduct :: Projections should have been turned into ordinary expressions" + | .letE .. => throwError "{decl_name%} :: Let-expressions should have been reduced" + | .mdata .. => throwError "{decl_name%} :: mdata should have been consumed" + | .proj .. => throwError "{decl_name%} :: Projections should have been turned into ordinary expressions" | e => collectAppInstSimpleInduct e end diff --git a/Auto/Translation/Inhabitation.lean b/Auto/Translation/Inhabitation.lean index 14cf56e..ff21a13 100644 --- a/Auto/Translation/Inhabitation.lean +++ b/Auto/Translation/Inhabitation.lean @@ -96,7 +96,7 @@ private def inhFactMatchAtomTysAux (inhTy : Lemma) (atomTys : Array Expr) : Meta let s ← saveState let (_, _, mi) ← MLemmaInst.ofLemmaInst li let .some e := getExprNonImpPosition mip mi.type - | throwError "inhFactMatchAtomTys :: Unexpected error, cannot get position {mip} from {mi.type}" + | throwError "{decl_name%} :: Unexpected error, cannot get position {mip} from {mi.type}" for a in atomTys do let s' ← saveState if (← Meta.isDefEq e a) then @@ -134,6 +134,6 @@ where for a in atomTys do if (← Meta.withNewMCtxDepth (Meta.isDefEq inhTy a)) then return inhTy - throwError "inhFactMatchAtomTys :: Unable to canonicalize {inhTy}" + throwError "{decl_name%} :: Unable to canonicalize {inhTy}" end Auto.Inhabitation diff --git a/Auto/Translation/Lam2DAtomAsFVar.lean b/Auto/Translation/Lam2DAtomAsFVar.lean index ce5f137..e9c0bfa 100644 --- a/Auto/Translation/Lam2DAtomAsFVar.lean +++ b/Auto/Translation/Lam2DAtomAsFVar.lean @@ -71,7 +71,7 @@ def withTypeAtomsAsFVar (atoms : Array Nat) : ExternM Unit := if (← getTypeAtomFVars).contains atom then continue let .some (e, lvl) := (← getTyVal)[atom]? - | throwError "withTypeAtomAsFVar :: Unknown type atom {atom}" + | throwError "{decl_name%} :: Unknown type atom {atom}" let name := (`_exTy).appendIndexAfter (← getTypeAtomFVars).size let newFVarId ← withLocalDecl name .default (.sort lvl) .default setAtomsToAbstract ((← getAtomsToAbstract).push (newFVarId, e)) @@ -82,7 +82,7 @@ def withTermAtomsAsFVar (atoms : Array Nat) : ExternM Unit := if (← getTermAtomFVars).contains atom then continue let .some (e, s) := (← getVarVal)[atom]? - | throwError "withTermAtomAsFVar :: Unknown term atom {atom}" + | throwError "{decl_name%} :: Unknown term atom {atom}" let sinterp ← Lam2D.interpLamSortAsUnlifted (← getTypeAtomFVars) s let name := (`e!).appendIndexAfter (← getTermAtomFVars).size let newFVarId ← withLocalDecl name .default sinterp .default @@ -94,7 +94,7 @@ def withEtomsAsFVar (etoms : Array Nat) : ExternM Unit := if (← getEtomFVars).contains etom then return let .some s := (← getLamEVarTy)[etom]? - | throwError "withEtomAsFVar :: Unknown etom {etom}" + | throwError "{decl_name%} :: Unknown etom {etom}" let sinterp ← Lam2D.interpLamSortAsUnlifted (← getTypeAtomFVars) s let name := (`e?).appendIndexAfter (← getEtomFVars).size let newFVarId ← withLocalDecl name .default sinterp .default @@ -147,7 +147,7 @@ def callNativeWithAtomAsFVar let ss ← nonemptiesWithDTr.mapM (fun (re, _) => do match re with | .nonempty s => return s - | _ => throwError "callNativeWithAtomAsFVar :: {re} is not a `nonempty` entry") + | _ => throwError "{decl_name%} :: {re} is not a `nonempty` entry") let inhs ← withTranslatedLamSorts ss for inh in inhs do trace[auto.lam2D.printInhs] "{inh}" @@ -158,13 +158,13 @@ def callNativeWithAtomAsFVar let ts ← valids.mapM (fun re => do match re with | .valid [] t => return t - | _ => throwError "callNativeWithAtomAsFVar :: {re} is not a `valid` entry") + | _ => throwError "{decl_name%} :: {re} is not a `valid` entry") let hyps ← withTranslatedLamTerms ts for hyp in hyps do if !(← runMetaM <| Meta.isTypeCorrect hyp) then - throwError "callNative :: Malformed hypothesis {hyp}" + throwError "{decl_name%} :: Malformed hypothesis {hyp}" if !(← runMetaM <| Meta.isProp hyp) then - throwError "callNative :: Hypothesis {hyp} is not a proposition" + throwError "{decl_name%} :: Hypothesis {hyp} is not a proposition" trace[auto.lam2D.printHyps] "{hyp}" let hyps ← runMetaM <| hyps.mapM (fun e => Core.betaReduce e) let hypFvars ← withHyps hyps @@ -207,7 +207,7 @@ def callNativeWithAtomAsFVar let proofLamTermPre := proofLamTermPre.abstractsRevImp ((Array.mk usedEtoms).map LamTerm.etom) let usedEtomTys ← usedEtoms.mapM (fun etom => do let .some ty := lamEVarTy[etom]? - | throwError "callNative :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" return ty) let proof := mkAppN expr ⟨usedVals⟩ let proofLamTerm := usedEtomTys.foldr (fun s cur => LamTerm.mkForallEF s cur) proofLamTermPre diff --git a/Auto/Translation/Lam2TH0.lean b/Auto/Translation/Lam2TH0.lean index b1996fa..48eb783 100644 --- a/Auto/Translation/Lam2TH0.lean +++ b/Auto/Translation/Lam2TH0.lean @@ -26,11 +26,11 @@ def lam2TH0 (lamVarTy : Array LamSort) (lamEVarTy : Array LamSort) (facts : Arra bvHs.toList.map (fun bvc => s!"thf(typedecl_bv{transBitVecConst bvc}, type, t_bv{transBitVecConst bvc}: {transBitVecConstSort bvc}).") ++ (← termHs.toList.mapM (fun i => do let .some s := lamVarTy.get? i - | throwError "lam2TH0 :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" return s!"thf(typedecl_t_a{i}, type, t_a{i}: {transLamSort s}).")) ++ (← etomHs.toList.mapM (fun i => do let .some s := lamEVarTy.get? i - | throwError "lam2TH0 :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" return s!"thf(typedecl_t_e{i}, type, t_e{i}: {transLamSort s}).")) -- Empty type is not inhabited if (lamVarTy ++ lamEVarTy).any (fun s => s == .base .empty) then diff --git a/Auto/Translation/LamFOL2SMT.lean b/Auto/Translation/LamFOL2SMT.lean index 29f5090..912c5b3 100644 --- a/Auto/Translation/LamFOL2SMT.lean +++ b/Auto/Translation/LamFOL2SMT.lean @@ -55,15 +55,15 @@ def LamAtomic.toLeanExpr match atomic with | .sort n => do let .some e := tyValMap.get? n - | throwError "SMT.printValuation :: Unknown sort atom {n}" + | throwError "{decl_name%} :: Unknown sort atom {n}" return e | .term n => do let .some e := varValMap.get? n - | throwError "SMT.printValuation :: Unknown term atom {n}" + | throwError "{decl_name%} :: Unknown term atom {n}" return e | .etom n => do let .some e := etomValMap.get? n - | throwError "SMT.printValuation :: Unknown etom {n}" + | throwError "{decl_name%} :: Unknown etom {n}" return e | .bvOfNat n => do let e := Expr.app (.const ``BitVec.ofNat []) (.lit (.natVal n)) @@ -95,7 +95,7 @@ where go : LamSort → MetaM String | .atom n => do let .some (e, _) := sni.tyVal[n]? - | throwError "lamSortAtom2String :: Unexpected sort atom {repr (LamSort.atom n)}" + | throwError "{decl_name%} :: Unexpected sort atom {repr (LamSort.atom n)}" exprToSuggestion e | .base b => return b.toString -- Suggest name based on return type @@ -109,11 +109,11 @@ where go : LamAtomic → MetaM String | .sort n => do let .some (e, _) := sni.tyVal[n]? - | throwError "lamSortAtom2String :: Unexpected sort atom {repr (LamSort.atom n)}" + | throwError "{decl_name%} :: Unexpected sort atom {repr (LamSort.atom n)}" exprToSuggestion e | .term n => do let .some (e, _) := sni.varVal[n]? - | throwError "lamTermAtom2String :: Unexpected term atom {repr (LamTerm.atom n)}" + | throwError "{decl_name%} :: Unexpected term atom {repr (LamTerm.atom n)}" exprToSuggestion e | .etom n => return s!"sk{n}" | .bvOfNat n => exprToSuggestion (Expr.app (.const ``BitVec.ofNat []) (.lit (.natVal n))) @@ -145,7 +145,7 @@ private def lamSortAtom2String (sni : SMTNamingInfo) (n : Nat) : TransM LamAtomi private def lamSort2SSortAux (sni : SMTNamingInfo) : LamSort → TransM LamAtomic SSort | .atom n => do return .app (.symb (← lamSortAtom2String sni n)) #[] | .base b => return lamBaseSort2SSort b -| .func _ _ => throwError "lamSort2STermAux :: Unexpected error. Higher order input?" +| .func _ _ => throwError "{decl_name%} :: Unexpected error. Higher order input?" /-- Only translates first-order types -/ private def lamSort2SSort (sni : SMTNamingInfo) : LamSort → TransM LamAtomic (List SSort × SSort) @@ -193,7 +193,7 @@ private def bitVec2STerm (n i : Nat) : STerm := private def lamBaseTerm2STerm_Arity3 (arg1 arg2 arg3 : STerm) : LamBaseTerm → TransM LamAtomic STerm | .scst .srepall => return .qStrApp "str.replace_all" #[arg1, arg2, arg3] -| t => throwError "lamTerm2STerm :: The arity of {repr t} is not 3" +| t => throwError "{decl_name%} :: The arity of {repr t} is not 3" private def lamBaseTerm2STerm_Arity2 (arg1 arg2 : STerm) : LamBaseTerm → TransM LamAtomic STerm | .pcst .and => return .qStrApp "and" #[arg1, arg2] @@ -248,7 +248,7 @@ private def lamBaseTerm2STerm_Arity2 (arg1 arg2 : STerm) : LamBaseTerm → Trans | .bvcst (.bvshOp _ smt? op) => match smt? with | false => - throwError "lamTerm2STerm :: Non-smt shift operations should not occur here" + throwError "{decl_name%} :: Non-smt shift operations should not occur here" | true => match op with | .shl => return .qStrApp "bvshl" #[arg1, arg2] @@ -256,7 +256,7 @@ private def lamBaseTerm2STerm_Arity2 (arg1 arg2 : STerm) : LamBaseTerm → Trans | .ashr => return .qStrApp "bvashr" #[arg1, arg2] | .bvcst (.bvappend _ _) => return .qStrApp "concat" #[arg1, arg2] | .ocst (.smtAttr1T name _ _) => return .attrApp name arg1 arg2 -| t => throwError "lamTerm2STerm :: The arity of {repr t} is not 2" +| t => throwError "{decl_name%} :: The arity of {repr t} is not 2" private def lamBaseTerm2STerm_Arity1 (sni : SMTNamingInfo) (arg : STerm) : LamBaseTerm → TransM LamAtomic STerm | .pcst .not => return .qStrApp "not" #[arg] @@ -316,7 +316,7 @@ private def lamBaseTerm2STerm_Arity1 (sni : SMTNamingInfo) (arg : STerm) : LamBa return .qIdApp (.ident (.indexed "sign_extend" #[.inr (v - w)])) #[arg] else return .qIdApp (.ident (.indexed "extract" #[.inr (v - 1), .inr 0])) #[arg] -| t => throwError "lamTerm2STerm :: The arity of {repr t} is not 1" +| t => throwError "{decl_name%} :: The arity of {repr t} is not 1" where solverName : MetaM Solver.SMT.SolverName := do return Solver.SMT.auto.smt.solver.name.get (← getOptions) @@ -332,11 +332,11 @@ private def lamBaseTerm2STerm_Arity0 : LamBaseTerm → TransM LamAtomic STerm | .ncst (.natVal n) => return .sConst (.num n) | .scst (.strVal s) => return .sConst (.str s) | .bvcst (.bvVal n i) => return bitVec2STerm n i -| t => throwError "lamTerm2STerm :: The arity of {repr t} is not 0" +| t => throwError "{decl_name%} :: The arity of {repr t} is not 0" def lamTermAtom2String (sni : SMTNamingInfo) (lamVarTy : Array LamSort) (n : Nat) : TransM LamAtomic (LamSort × String) := do let .some s := lamVarTy[n]? - | throwError "lamTermAtom2String :: Unexpected term atom {repr (LamTerm.atom n)}" + | throwError "{decl_name%} :: Unexpected term atom {repr (LamTerm.atom n)}" -- Empty type is not inhabited if s == .base .empty then addCommand (.assert (.qStrApp "false" #[])) @@ -349,7 +349,7 @@ def lamTermAtom2String (sni : SMTNamingInfo) (lamVarTy : Array LamSort) (n : Nat def lamTermEtom2String (sni : SMTNamingInfo) (lamEVarTy : Array LamSort) (n : Nat) : TransM LamAtomic (LamSort × String) := do let .some s := lamEVarTy[n]? - | throwError "lamTerm2STerm :: Unexpected etom {repr (LamTerm.etom n)}" + | throwError "{decl_name%} :: Unexpected etom {repr (LamTerm.etom n)}" -- Empty type is not inhabited if s == .base .empty then addCommand (.assert (.qStrApp "false" #[])) @@ -365,12 +365,12 @@ private def lamTerm2STermAux (sni : SMTNamingInfo) (lamVarTy lamEVarTy : Array L | .atom n => do let (s, name) ← lamTermAtom2String sni lamVarTy n if args.size != s.getArgTys.length then - throwError "lamTerm2STerm :: Argument number mismatch. Higher order input?" + throwError "{decl_name%} :: Argument number mismatch. Higher order input?" return .qIdApp (QualIdent.ofString name) args | .etom n => do let (s, name) ← lamTermEtom2String sni lamEVarTy n if args.size != s.getArgTys.length then - throwError "lamTerm2STerm :: Argument number mismatch. Higher order input?" + throwError "{decl_name%} :: Argument number mismatch. Higher order input?" return .qIdApp (QualIdent.ofString name) args | .base b => match args with @@ -378,8 +378,8 @@ private def lamTerm2STermAux (sni : SMTNamingInfo) (lamVarTy lamEVarTy : Array L | #[u₁] => lamBaseTerm2STerm_Arity1 sni u₁ b | #[u₁, u₂] => lamBaseTerm2STerm_Arity2 u₁ u₂ b | #[u₁, u₂, u₃] => lamBaseTerm2STerm_Arity3 u₁ u₂ u₃ b - | _ => throwError "lamTerm2STerm :: Argument number mismatch. Higher order input?" -| t => throwError "lamTerm2STerm :: Unexpected head term {repr t}" + | _ => throwError "{decl_name%} :: Argument number mismatch. Higher order input?" +| t => throwError "{decl_name%} :: Unexpected head term {repr t}" def lamQuantified2STerm (sni : SMTNamingInfo) (forall? : Bool) (s : LamSort) (body : TransM LamAtomic STerm) : TransM LamAtomic STerm := do -- Empty type is not inhabited @@ -400,13 +400,13 @@ private partial def lamTerm2STerm (sni : SMTNamingInfo) (lamVarTy lamEVarTy : Ar | .base b => lamBaseTerm2STerm_Arity0 b | .bvar n => return .bvar n | .app _ (.app _ (.base (.eqI _)) _) _ => - throwError ("lamTerm2STerm :: " ++ LamExportUtils.exportError.ImpPolyLog) + throwError (decl_name% ++ " :: " ++ LamExportUtils.exportError.ImpPolyLog) | .app _ (.base (.forallEI _)) (.lam _ _) => - throwError ("lamTerm2STerm :: " ++ LamExportUtils.exportError.ImpPolyLog) + throwError (decl_name% ++ " :: " ++ LamExportUtils.exportError.ImpPolyLog) | .app _ (.base (.existEI _)) (.lam _ _) => - throwError ("lamTerm2STerm :: " ++ LamExportUtils.exportError.ImpPolyLog) + throwError (decl_name% ++ " :: " ++ LamExportUtils.exportError.ImpPolyLog) | .app _ (.app _ (.app _ (.base (.iteI _)) _) _) _ => - throwError ("lamTerm2STerm :: " ++ LamExportUtils.exportError.ImpPolyLog) + throwError (decl_name% ++ " :: " ++ LamExportUtils.exportError.ImpPolyLog) | .app _ (.app _ (.base (.eq _)) arg₁) arg₂ => do let arg₁' ← lamTerm2STerm sni lamVarTy lamEVarTy arg₁ let arg₂' ← lamTerm2STerm sni lamVarTy lamEVarTy arg₂ @@ -442,16 +442,16 @@ private def lamMutualIndInfo2STerm (sni : SMTNamingInfo) (mind : MutualIndInfo) -- be declared during the following `lamSort2SSort` for ⟨type, _, _⟩ in mind do let .atom sn := type - | throwError "lamMutualIndInfo2STerm :: Inductive type {type} is not a sort atom" + | throwError "{decl_name%} :: Inductive type {type} is not a sort atom" -- Do not use `lamSortAtom2String` because we don't want to `declare-sort` let _ ← h2Symb (.sort sn) (← sni.suggestNameForAtomic (.sort sn)) for ⟨type, ctors, projs⟩ in mind do let .atom sn := type - | throwError "lamMutualIndInfo2STerm :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" let mut projInfos : Array (LamSort × String) := #[] if let .some projs := projs then if ctors.length != 1 then - throwError "lamMutualIndInfo2STerm :: Unexpected error" + throwError "{decl_name%} :: Unexpected error" for (s, t) in projs do let mut projname := "" match t with @@ -477,7 +477,7 @@ private def lamMutualIndInfo2STerm (sni : SMTNamingInfo) (mind : MutualIndInfo) let mut selDecls := #[] if projs.isSome then if argTys.length != projInfos.size then - throwError "lamMutualIndInfo2STerm :: Unexpected error" + throwError "{decl_name%} :: Unexpected error" selDecls := ((Array.mk argTys).zip projInfos).map (fun (argTy, _, name) => (name, argTy)) else selDecls := (Array.mk argTys).zipWithIndex.map (fun (argTy, idx) => @@ -534,7 +534,7 @@ def withExprValuation match atomic with | .etom n => .some (n, name) | _ => .none) let declInfos ← etomsWithName.mapM (fun (n, name) => do let .some s := sni.lamEVarTy[n]? - | throwError "SMT.printValuation :: Unknown etom {n}" + | throwError "{decl_name%} :: Unknown etom {n}" let type ← Lam2D.interpLamSortAsUnlifted tyValMap s return (Name.mkSimple name, .default, fun _ => pure type)) Meta.withLocalDecls declInfos (fun etomFVars => do diff --git a/Auto/Translation/LamReif.lean b/Auto/Translation/LamReif.lean index 49ddc87..6a1f1f4 100644 --- a/Auto/Translation/LamReif.lean +++ b/Auto/Translation/LamReif.lean @@ -141,7 +141,7 @@ def printProofs : ReifM Unit := do for re in (← getRTable) do if let .some cs := chkMap.get? re then let .some n := (← getRst).findPos? re - | throwError "printProofs :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" let etoms := match (← getChkStepCache).get? cs with | .some (_, arr) => @@ -152,13 +152,13 @@ def printProofs : ReifM Unit := do match re with | .valid [] t => let .some (expr, _, n) := (← getAssertions).get? t - | throwError "printProofs :: Unable to find assertion associated with {t}" + | throwError "{decl_name%} :: Unable to find assertion associated with {t}" trace[auto.lamReif.printProofs] "{n} : External fact ⦗⦗{← Meta.inferType expr}⦘⦘ proves ⦗⦗{re}⦘⦘" | .nonempty s => let .some (expr, _, n) := (← getInhabitations).get? s - | throwError "printProofs :: Unable to find inhabitation fact associated with {s}" + | throwError "{decl_name%} :: Unable to find inhabitation fact associated with {s}" trace[auto.lamReif.printProofs] "{n} : Inhabitation fact ⦗⦗{← Meta.inferType expr}⦘⦘ proves ⦗⦗{re}⦘⦘" - | _ => throwError "printProofs :: Unexpected entry {re}" + | _ => throwError "{decl_name%} :: Unexpected entry {re}" def sort2LamILTyIdx (s : LamSort) : ReifM Nat := do let isomTyMap ← getIsomTyMap @@ -175,32 +175,32 @@ def lookupTyVal! (n : Nat) : ReifM (Expr × Level) := do if let .some r := (← getTyVal)[n]? then return r else - throwError "lookupTyVal! :: Unknown type atom {n}" + throwError "{decl_name%} :: Unknown type atom {n}" /-- Lookup valuation of term atom -/ def lookupVarVal! (n : Nat) : ReifM (Expr × LamSort) := do if let .some r := (← getVarVal)[n]? then return r else - throwError "lookupVarVal! :: Unknown term atom {n}" + throwError "{decl_name%} :: Unknown term atom {n}" def lookupLamILTy! (idx : Nat) : ReifM LamSort := do if let .some s := (← getLamILTy)[idx]? then return s else - throwError "lookupLamILTy! :: Unknown index {idx}" + throwError "{decl_name%} :: Unknown index {idx}" def lookupAssertion! (t : LamTerm) : ReifM (Expr × DTr × LamTerm × Nat) := do if let .some r := (← getAssertions).get? t then return r else - throwError "lookupAssertion! :: Unknown assertion {t}" + throwError "{decl_name%} :: Unknown assertion {t}" def lookupRTable! (pos : Nat) : ReifM REntry := do if let .some r := (← getRTable).get? pos then return r else - throwError "lookupRTable! :: Unknown REntry {pos}" + throwError "{decl_name%} :: Unknown REntry {pos}" def lookupREntryPos! (re : REntry) : ReifM Nat := do match (← getRst).findPos? re with @@ -210,12 +210,12 @@ def lookupREntryPos! (re : REntry) : ReifM Nat := do | .valid [] t => match (← getAssertions).get? t with | .some (_, _, _, n) => return n - | .none => throwError "lookupREntryPos! :: Unknown REntry {re}" + | .none => throwError "{decl_name%} :: Unknown REntry {re}" | .nonempty s => match (← getInhabitations).get? s with | .some (_, _, n) => return n - | .none => throwError "lookupREntryPos! :: Unknown REntry {re}" - | _ => throwError "lookupREntryPos! :: Unknown REntry {re}" + | .none => throwError "{decl_name%} :: Unknown REntry {re}" + | _ => throwError "{decl_name%} :: Unknown REntry {re}" inductive REntryProof where | chkStep : ChkStep → REntryProof @@ -240,31 +240,31 @@ def lookupREntryProof? (re : REntry) : ReifM (Option REntryProof) := do def lookupREntryProof! (re : REntry) : ReifM REntryProof := do match ← lookupREntryProof? re with | .some proof => return proof - | .none => throwError "lookupREntryProof! :: Unknown REntry {re}" + | .none => throwError "{decl_name%} :: Unknown REntry {re}" def lookupLamEVarTy! (idx : Nat) : ReifM LamSort := do if let .some s := (← getLamEVarTy)[idx]? then return s else - throwError "lookupLamEVarTy! :: Unknown etom {idx}" + throwError "{decl_name%} :: Unknown etom {idx}" def lookupChkStepEtom! (cs : ChkStep) : ReifM (Array Nat) := do if let .some (_, arr) := (← getChkStepCache).get? cs then return arr else - throwError "lookupChkStepEtom! :: ChkStep {cs} did not produce new etom" + throwError "{decl_name%} :: ChkStep {cs} did not produce new etom" def lookupChkStepResult! (cs : ChkStep) : ReifM EvalResult := do if let .some (er, _) := (← getChkStepCache).get? cs then return er else - throwError "lookupChkStepEtom! :: ChkStep {cs} did not produce new etom" + throwError "{decl_name%} :: ChkStep {cs} did not produce new etom" def lookupEtomChkStep! (eidx : Nat) : ReifM ChkStep := do if let .some c := (← getEtomChkStep).get? eidx then return c else - throwError "lookupEtomChkStep! :: Unknown etom {eidx}" + throwError "{decl_name%} :: Unknown etom {eidx}" /-- This should only be used at the meta level, i.e. in code that will @@ -289,7 +289,7 @@ def resolveLamBaseTermImport : LamBaseTerm → ReifM LamBaseTerm /-- Models `resolveImport` on the `meta` level -/ def resolveImport : LamTerm → ReifM LamTerm | .atom n => return .atom n -| .etom _ => throwError "resolveImport :: etom should not occur here" +| .etom _ => throwError "{decl_name%} :: etom should not occur here" | .base b => return .base (← resolveLamBaseTermImport b) | .bvar n => return .bvar n | .lam s t => return .lam s (← resolveImport t) @@ -311,7 +311,7 @@ def resolveImport : LamTerm → ReifM LamTerm -/ def mkImportVersion : LamTerm → ReifM LamTerm | .atom n => return (.atom n) -| .etom _ => throwError "mkImportVersion :: etom should not occur here" +| .etom _ => throwError "{decl_name%} :: etom should not occur here" | .base b => match b with | .eq s => return .base (.eqI (← sort2LamILTyIdx s)) @@ -343,9 +343,9 @@ def newChkStep (c : ChkStep) (res? : Option EvalResult) : ReifM (Bool × EvalRes let res := c.eval ltv.lamVarTy ltv.lamILTy ⟨← getRTableTree, ← getMaxEVarSucc, ← getLamEVarTyTree⟩ if let .some res' := res? then if res' != res then - throwError "newChkStep :: Result {res} of ChkStep {c} does not match with expected {res'}" + throwError "{decl_name%} :: Result {res} of ChkStep {c} does not match with expected {res'}" match res with - | .fail => throwError "newChkStep :: Evaluation of ChkStep {c} produces `fail`" + | .fail => throwError "{decl_name%} :: Evaluation of ChkStep {c} produces `fail`" | .addEntry re => -- If `re` is already provable, do nothing if let .some _ ← lookupREntryProof? re then @@ -478,7 +478,7 @@ section ILLifting let (upFunc, downFunc, ty, upTy) ← updownFunc s let sortOrig ← Expr.normalizeType (← Meta.inferType ty) let .sort uOrig := sortOrig - | throwError "mkImportAux :: Unexpected sort {sortOrig} when processing sort {s}" + | throwError "{decl_name%} :: Unexpected sort {sortOrig} when processing sort {s}" return (upFunc, downFunc, ty, upTy, uOrig) set_option pp.universes true @@ -503,20 +503,20 @@ section Checker def nonemptyOfAtom (n : Nat) : ReifM (Option REntry) := do let .some (_, s) := (← getVarVal).get? n - | throwError "nonemptyOfAtom :: Index {n} out of bound" + | throwError "{decl_name%} :: Index {n} out of bound" if !(← inhSubsumptionCheck s) then return .none let (_, .addEntry re) ← newChkStep (.n (.nonemptyOfAtom n)) (.some (.addEntry (.nonempty s))) - | throwError "nonemptyOfAtom :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return .some re def nonemptyOfEtom (n : Nat) : ReifM (Option REntry) := do let .some s := (← getLamEVarTy).get? n - | throwError "nonemptyOfEtom :: Index {n} out of bound" + | throwError "{decl_name%} :: Index {n} out of bound" if !(← inhSubsumptionCheck s) then return .none let (_, .addEntry re) ← newChkStep (.n (.nonemptyOfEtom n)) (.some (.addEntry (.nonempty s))) - | throwError "nonemptyOfEtom :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return .some re def validOfIntros (v : REntry) (idx : Nat) : ReifM REntry := do @@ -524,12 +524,12 @@ section Checker return v let p ← lookupREntryPos! v let (_, .addEntry re) ← newChkStep (.l (.validOfIntros p idx)) .none - | throwError "validOfIntros :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return re def validOfIntroMost (v : REntry) : ReifM REntry := do let .valid _ t := v - | throwError "validOfIntroMost :: Unexpected entry {v}" + | throwError "{decl_name%} :: Unexpected entry {v}" let mut idx := 0 let mut t := t while true do @@ -543,12 +543,12 @@ section Checker def validOfReverts (v : REntry) (idx : Nat) : ReifM REntry := do let p ← lookupREntryPos! v let (_, .addEntry re) ← newChkStep (.l (.validOfReverts p idx)) .none - | throwError "validOfReverts :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return re def validOfRevertAll (v : REntry) : ReifM REntry := do let .valid lctx _ := v - | throwError "validOfRevertAll :: Unexpected entry {v}" + | throwError "{decl_name%} :: Unexpected entry {v}" if lctx.length == 0 then return v validOfReverts v lctx.length @@ -556,26 +556,26 @@ section Checker def validOfAppend (v : REntry) (ex : Array LamSort) : ReifM REntry := do let p ← lookupREntryPos! v let (_, .addEntry re) ← newChkStep (.l (.validOfAppend p ex.toList)) .none - | throwError "validOfAppend :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return re def validOfPrepend (v : REntry) (ex : Array LamSort) : ReifM REntry := do let p ← lookupREntryPos! v let (_, .addEntry re) ← newChkStep (.l (.validOfPrepend p ex.toList)) .none - | throwError "validOfPrepend :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return re def validOfHeadBeta (v : REntry) : ReifM REntry := do let p ← lookupREntryPos! v let (_, .addEntry re) ← newChkStep (.c (.validOfHeadBeta p)) .none - | throwError "validOfHeadBeta :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return re def validOfHnf (v : REntry) : ReifM REntry := do let mut v := v while true do let .valid _ t := v - | throwError "validOfHnf :: Unexpected entry {v}" + | throwError "{decl_name%} :: Unexpected entry {v}" if !t.isHeadBetaTarget then break v ← validOfHeadBeta v @@ -584,50 +584,50 @@ section Checker def validOfBetaBounded (v : REntry) (bound : Nat) : ReifM REntry := do let p ← lookupREntryPos! v let (_, .addEntry re) ← newChkStep (.c (.validOfBetaBounded p bound)) .none - | throwError "validOfBetaBounded :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return re def validOfBetaReduce (v : REntry) : ReifM REntry := do let .valid _ t := v - | throwError "validOfBetaReduce :: Unexpected entry {v}" + | throwError "{decl_name%} :: Unexpected entry {v}" validOfBetaBounded v t.betaReduceHackyIdx def validOfExtensionalize (v : REntry) : ReifM REntry := do let p ← lookupREntryPos! v let (_, .addEntry re) ← newChkStep (.c (.validOfExtensionalize p)) .none - | throwError "validOfExtensionalize :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return re def validOfEqSymm (v : REntry) : ReifM REntry := do let p ← lookupREntryPos! v let (_, .addEntry re) ← newChkStep (.c (.validOfEqSymm p)) .none - | throwError "validOfEqSymm :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return re def validOfMp (vp : REntry) (vrw : REntry) : ReifM REntry := do let pp ← lookupREntryPos! vp let prw ← lookupREntryPos! vrw let (_, .addEntry re) ← newChkStep (.c (.validOfMp pp prw)) .none - | throwError "validOfMp :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return re def validOfMpAll (vp : REntry) (vrw : REntry) : ReifM REntry := do let pp ← lookupREntryPos! vp let prw ← lookupREntryPos! vrw let (_, .addEntry re) ← newChkStep (.c (.validOfMpAll pp prw)) .none - | throwError "validOfMpAll :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return re def validOfEtaExpand1At (v : REntry) (occ : List Bool) : ReifM REntry := do let pv ← lookupREntryPos! v let (_, .addEntry re) ← newChkStep (.ca (.validOfEtaExpand1At pv occ)) .none - | throwError "validOfEtaExpand1At :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return re def validOfEtaReduce1At (v : REntry) (occ : List Bool) : ReifM REntry := do let pv ← lookupREntryPos! v let (_, .addEntry re) ← newChkStep (.ca (.validOfEtaReduce1At pv occ)) .none - | throwError "validOfEtaReduce1At :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return re def validOfEtaExpandNAt (v : REntry) (n : Nat) (occ : List Bool) : ReifM REntry := do @@ -637,7 +637,7 @@ section Checker if n == 1 then return ← validOfEtaExpand1At v occ let (_, .addEntry re) ← newChkStep (.ca (.validOfEtaExpandNAt pv n occ)) .none - | throwError "validOfEtaExpandNAt :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return re def validOfEtaReduceNAt (v : REntry) (n : Nat) (occ : List Bool) : ReifM REntry := do @@ -647,55 +647,55 @@ section Checker if n == 1 then return ← validOfEtaReduce1At v occ let (_, .addEntry re) ← newChkStep (.ca (.validOfEtaReduceNAt pv n occ)) .none - | throwError "validOfEtaReduceNAt :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return re def validOfEtaExpandAt (v : REntry) (occ : List Bool) : ReifM REntry := do let .valid _ t := v - | throwError "validOfEtaExpandAt :: Unexpected entry {v}" + | throwError "{decl_name%} :: Unexpected entry {v}" let .some (rty, _) := LamTerm.getPosWith occ (.base .prop) t - | throwError "validOfEtaExpandAt :: {occ} is not a valid position of {t}" + | throwError "{decl_name%} :: {occ} is not a valid position of {t}" let n := rty.getArgTys.length validOfEtaExpandNAt v n occ def validOfEtaReduceAt (v : REntry) (occ : List Bool) : ReifM REntry := do let .valid _ t := v - | throwError "validOfEtaReduceAt :: Unexpected entry {v}" + | throwError "{decl_name%} :: Unexpected entry {v}" let .some tocc := LamTerm.getPos occ t - | throwError "validOfEtaReduceAt :: {occ} is not a valid position of {t}" + | throwError "{decl_name%} :: {occ} is not a valid position of {t}" let n := tocc.getLamTys.length validOfEtaReduceNAt v n occ def validOfExtensionalizeEqAt (v : REntry) (occ : List Bool) : ReifM REntry := do let pv ← lookupREntryPos! v let (_, .addEntry re) ← newChkStep (.ca (.validOfExtensionalizeEqAt pv occ)) .none - | throwError "validOfExtensionalizeEqAt :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return re def validOfExtensionalizeEqFNAt (v : REntry) (n : Nat) (occ : List Bool) : ReifM REntry := do let pv ← lookupREntryPos! v let (_, .addEntry re) ← newChkStep (.ca (.validOfExtensionalizeEqFNAt pv n occ)) .none - | throwError "validOfExtensionalizeEqFNAt :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return re def validOfIntensionalizeEqAt (v : REntry) (occ : List Bool) : ReifM REntry := do let pv ← lookupREntryPos! v let (_, .addEntry re) ← newChkStep (.ca (.validOfIntensionalizeEqAt pv occ)) .none - | throwError "validOfIntensionalizeEqAt :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return re def validOfBVarLower (v : REntry) (n : REntry) : ReifM REntry := do let pv ← lookupREntryPos! v let pn ← lookupREntryPos! n let (_, .addEntry re) ← newChkStep (.i (.validOfBVarLower pv pn)) .none - | throwError "validOfBVarLower :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return re def validOfBVarLowers (v : REntry) (ns : Array REntry) : ReifM REntry := do let pv ← lookupREntryPos! v let pns ← ns.mapM lookupREntryPos! let (_, .addEntry re) ← newChkStep (.i (.validOfBVarLowers pv pns.toList)) .none - | throwError "validOfBVarLowers :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return re /-- @@ -710,27 +710,27 @@ section Checker let p₁₂ ← lookupREntryPos! v₁₂ let p₁ ← lookupREntryPos! v₁ let (_, .addEntry re) ← newChkStep (.i (.validOfImp p₁₂ p₁)) .none - | throwError "validOfImp :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return re def validOfImps (impV : REntry) (hypVs : Array REntry) : ReifM REntry := do let imp ← lookupREntryPos! impV let ps ← hypVs.mapM lookupREntryPos! let (_, .addEntry re) ← newChkStep (.i (.validOfImps imp ps.toList)) .none - | throwError "validOfImps :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return re /-- Repeated instantiation -/ def validOfInstantiate (v : REntry) (args : Array LamTerm) : ReifM REntry := do let p ← lookupREntryPos! v let (_, .addEntry re) ← newChkStep (.i (.validOfInstantiate p args.toList)) .none - | throwError "validOfInstantiate :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return re def validOfInstantiateRev (v : REntry) (args : Array LamTerm) : ReifM REntry := do let p ← lookupREntryPos! v let (_, .addEntry re) ← newChkStep (.i (.validOfInstantiateRev p args.toList)) .none - | throwError "validOfInstantiateRev :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return re /-- @@ -746,22 +746,22 @@ section Checker def validOfAndLeft (v : REntry) (occ : List Bool) : ReifM REntry := do let p ← lookupREntryPos! v let (_, .addEntry re) ← newChkStep (.i (.validOfAndLeft p occ)) .none - | throwError "validOfAndLeft :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return re def validOfAndRight (v : REntry) (occ : List Bool) : ReifM REntry := do let p ← lookupREntryPos! v let (_, .addEntry re) ← newChkStep (.i (.validOfAndRight p occ)) .none - | throwError "validOfAndRight :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return re /-- Exhaustively decompose `∧` at position `occ` -/ partial def decomposeAnd (v : REntry) (occ : List Bool) : ReifM (Array REntry) := do let .valid _ t := v - | throwError "decomposeAnd :: Unexpected entry" - if !(t.isSign true occ) then throwError "decomposeAnd :: {occ} is not a positive position of {t}" + | throwError "{decl_name%} :: Unexpected entry" + if !(t.isSign true occ) then throwError "{decl_name%} :: {occ} is not a positive position of {t}" let .some sub := t.getPos occ - | throwError "decomposeAnd :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" if sub.getAppFn == .base .and && sub.getAppArgs.length == 2 then let left ← validOfAndLeft v occ let right ← validOfAndRight v occ @@ -771,19 +771,19 @@ section Checker def boolFacts : ReifM REntry := do let (_, .addEntry re) ← newChkStep (.f .boolFacts) .none - | throwError "boolFacts :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return re def iteSpec (s : LamSort) : ReifM REntry := do let (_, .addEntry re) ← newChkStep (.f (.iteSpec s)) .none - | throwError "iteSpec :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return re def skolemize (exV : REntry) : ReifM REntry := do let eidx ← getMaxEVarSucc let ex ← lookupREntryPos! exV let (new?, .newEtomWithValid _ lctx t) ← newChkStep (.e (.skolemize ex)) .none - | throwError "skolemize :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" if new? then let _ ← nonemptyOfEtom eidx return .valid lctx t @@ -793,11 +793,11 @@ section Checker let mut exV := exV while true do let .valid _ t := exV - | throwError "skolemizeMostIntoForall :: Unexpected entry {exV}" + | throwError "{decl_name%} :: Unexpected entry {exV}" if t.isMkForallE then exV ← validOfIntroMost exV let .valid _ t := exV - | throwError "skolemizeMostIntoForall :: Unexpected entry {exV}" + | throwError "{decl_name%} :: Unexpected entry {exV}" if t.isMkExistE then exV ← skolemize exV exV ← validOfHnf exV @@ -808,7 +808,7 @@ section Checker def define (t : LamTerm) : ReifM REntry := do let eidx ← getMaxEVarSucc let (new?, .newEtomWithValid _ [] t) ← newChkStep (.e (.define t)) .none - | throwError "define :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" if new? then let _ ← nonemptyOfEtom eidx return .valid [] t @@ -816,7 +816,7 @@ section Checker def validOfPrepConv (pc : PrepConvStep) (v : REntry) (occ : List Bool) : ReifM REntry := do let p ← lookupREntryPos! v let (_, .addEntry re) ← newChkStep (.p pc p occ) .none - | throwError "validOfPrepConv :: Unexpected evaluation result" + | throwError "{decl_name%} :: Unexpected evaluation result" return re end Checker @@ -829,17 +829,17 @@ section CheckerUtils -/ def reorderLCtx (v : REntry) (rmap : Array Nat) : ReifM REntry := do let .valid lctx _ := v - | throwError "reorderLCtx :: Unexpected entry {v}" + | throwError "{decl_name%} :: Unexpected entry {v}" let lsize := lctx.length if rmap.size != lsize then - throwError "reorderLCtx :: Length of lctx does not equal size of reorder map" + throwError "{decl_name%} :: Length of lctx does not equal size of reorder map" let mut ex : Array LamSort := rmap.map (fun _ => .atom 0) let mut argBVarIdx : Array Nat := #[] for (s, i) in (Array.mk lctx).zipWithIndex do let .some i' := rmap[i]? - | throwError "reorderLCtx :: Does not know where does `.bvar i` map to" + | throwError "{decl_name%} :: Does not know where does `.bvar i` map to" if i' >= lsize then - throwError "reorderLCtx :: Index {i'} out of bound {lsize}" + throwError "{decl_name%} :: Index {i'} out of bound {lsize}" ex := ex.set! i' s argBVarIdx := argBVarIdx.push (lsize - i - 1 + i') let v ← validOfAppend v ex @@ -848,7 +848,7 @@ section CheckerUtils /-- Refer to docstring of `LamTerm.isGeneral` -/ def toDefinition? (v : REntry) : ReifM (Option REntry) := do let .valid lctx t := v - | throwError "toDefinition :: Unexpected entry {v}" + | throwError "{decl_name%} :: Unexpected entry {v}" let mut introed := t.betaReduceHacky let mut lctx' := lctx while true do @@ -863,7 +863,7 @@ section CheckerUtils let mr := rhs.getLamBody.isGeneral (lctx'.length + rhs.getLamTys.length) if ml.isNone && mr.isNone then return .none let .some m := ml <|> mr - | throwError "toDefinition? :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" let v ← validOfBetaReduce v let v ← validOfIntroMost v let v ← (do if (head == .iff) then validOfPrepConv .validOfPropext v [] else pure v) @@ -897,7 +897,7 @@ section CheckerUtils | passive := passive.push back; continue trace[auto.lamReif.prep.def] "Entry {back} is def-like and is turned into {v'}" let .valid [] rw@(.app _ (.app _ (.base (.eq _)) lhs) rhs) := v' - | throwError "recognizeDefsAndUnfold :: Unexpected definition entry {v'}" + | throwError "{decl_name%} :: Unexpected definition entry {v'}" -- If the left-hand-side occurs inside the right-hand-side, -- then this definition is recursive and we will not unfold it if rhs.abstractsImp #[lhs] != rhs then @@ -906,7 +906,7 @@ section CheckerUtils active ← active.mapM (validOfMpAll · v') minds ← minds.mapM (fun mind => do let .some mind := mind.mpAll? rw - | throwError "recognizeDefsAndUnfold :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" return mind) return (passive, minds) @@ -972,7 +972,7 @@ def newTypeExpr (e : Expr) : ReifM LamSort := do let origSort ← Meta.inferType e let origSort := (← instantiateMVars origSort).headBeta let .sort lvl := origSort - | throwError "newTypeExpr :: Unexpected sort {origSort}" + | throwError "{decl_name%} :: Unexpected sort {origSort}" setTyVal (tyVal.push (e, lvl)) setTyVarMap (tyVarMap.insert e idx) return .atom idx @@ -1129,15 +1129,15 @@ def processSimpleLit (l : Literal) : LamTerm := def processSimpleConst (name : Name) (lvls : List Level) : ReifM (Option LamTerm) := do if let .some t := reifMapConstNilLvl.get? name then if lvls.length != 0 then - throwError "processSimpleConst :: ConstNilLvl constants should have nil level list" + throwError "{decl_name%} :: ConstNilLvl constants should have nil level list" return t if name == ``Embedding.ImpF then let [u, v] := lvls - | throwError "processSimpleConst :: Invalid levels {lvls} for Auto.Embedding.ImpF" + | throwError "{decl_name%} :: Invalid levels {lvls} for Auto.Embedding.ImpF" if (← Meta.isLevelDefEq u .zero) ∧ (← Meta.isLevelDefEq v .zero) then return .some (.base .imp) else - throwError "processSimpleConst :: Non-propositional implication is not supported" + throwError "{decl_name%} :: Non-propositional implication is not supported" return .none def processSimpleApp (fn arg : Expr) : ReifM (Option LamTerm) := do @@ -1146,22 +1146,22 @@ def processSimpleApp (fn arg : Expr) : ReifM (Option LamTerm) := do let .const name lvls := fn | return .none match args.toList with - | [] => throwError "processSimpleApp :: Unexpected error" + | [] => throwError "{decl_name%} :: Unexpected error" | [arg] => if let .some tcon := reifMapBVConst1.get? name then if lvls.length != 0 then - throwError "processSimpleApp :: BVConst1 should have nil level list" + throwError "{decl_name%} :: BVConst1 should have nil level list" if let .some n ← @id (MetaM _) (Meta.evalNat arg) then return .some (tcon n) return .none if let .some attrName := reifMapAttributesProp.get? name then if lvls.length != 1 then - throwError "processSimpleApp :: Attribute should have one level" + throwError "{decl_name%} :: Attribute should have one level" return .some (.base (.ocst (.smtAttr1T attrName (← reifType arg) (.base .prop)))) if let .some tcon := reifMapIL.get? name then if name == ``Embedding.forallF then let [lvl₁, lvl₂] := lvls - | throwError "processSimpleApp :: Auto.Embedding.forallF should have two levels" + | throwError "{decl_name%} :: Auto.Embedding.forallF should have two levels" if !(← Meta.isLevelDefEq lvl₂ .zero) then return .none return .some (.base (tcon (← reifType arg))) @@ -1169,7 +1169,7 @@ def processSimpleApp (fn arg : Expr) : ReifM (Option LamTerm) := do | [arg₁, arg₂] => if let .some tcon := reifMapBVConst2.get? name then if lvls.length != 0 then - throwError "processSimpleApp :: BVConst2 should have nil level list" + throwError "{decl_name%} :: BVConst2 should have nil level list" match ← @id (MetaM _) (Meta.evalNat arg₁), ← @id (MetaM _) (Meta.evalNat arg₂) with | .some n, .some m => return .some (tcon n m) @@ -1178,7 +1178,7 @@ def processSimpleApp (fn arg : Expr) : ReifM (Option LamTerm) := do | [arg₁, arg₂, arg₃] => if let .some tcon := reifMapBVConst3.get? name then if lvls.length != 0 then - throwError "processSimpleApp :: BVConst2 should have nil level list" + throwError "{decl_name%} :: BVConst2 should have nil level list" match ← @id (MetaM _) (Meta.evalNat arg₁), ← @id (MetaM _) (Meta.evalNat arg₂), ← @id (MetaM _) (Meta.evalNat arg₃) with @@ -1322,13 +1322,13 @@ def processLam0Arg2 (e fn arg₁ arg₂ : Expr) : MetaM (Option LamTerm) := do | return .none if arg₁.isConst then let .const arg₁Name _ := arg₁ - | throwError "processLam0Arg2 :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" if let .some (e', t) := reifMapLam0Arg2NoLit.get? (fnName, arg₁Name) then if (← Meta.isDefEqD e e') then return .some t if arg₁.isApp then let .app arg₁fn arg₁arg := arg₁ - | throwError "processLam0Arg2 :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" if let .const arg₁FnName _ := arg₁fn then if let .some candidates := reifMapLam0Arg2Natlit.get? (fnName, arg₁FnName) then if let .some n ← Meta.evalNat arg₁arg then @@ -1344,20 +1344,20 @@ def processLam0Arg3 (e fn arg₁ arg₂ arg₃ : Expr) : MetaM (Option LamTerm) | .const ``Nat _ => if (← Meta.isDefEqD e arg₂) then let .lit (.natVal nv) := arg₂ - | throwError "processLam0Arg3 :: OfNat.ofNat instance is not based on a nat literal" + | throwError "{decl_name%} :: OfNat.ofNat instance is not based on a nat literal" return .some (.base (.natVal nv)) return .none | .const ``Int _ => if (← Meta.isDefEqD e (.app (.const ``Int.ofNat []) arg₂)) then let .lit (.natVal nv) := arg₂ - | throwError "processLam0Arg3 :: OfNat.ofNat instance is not based on a nat literal" + | throwError "{decl_name%} :: OfNat.ofNat instance is not based on a nat literal" return .some (.mkIOfNat (.base (.natVal nv))) return .none | .app (.const ``BitVec []) nExpr => if let .some n ← Meta.evalNat nExpr then if (← Meta.isDefEqD e (mkApp2 (.const ``BitVec.ofNat []) (.lit (.natVal n)) arg₂)) then let .lit (.natVal nv) := arg₂ - | throwError "processLam0Arg3 :: OfNat.ofNat instance is not based on a nat literal" + | throwError "{decl_name%} :: OfNat.ofNat instance is not based on a nat literal" return .some (.base (.bvVal n nv)) return .none | _ => return .none @@ -1368,19 +1368,19 @@ def processLam0Arg4 (e fn arg₁ arg₂ arg₃ arg₄ : Expr) : MetaM (Option La | return .none if arg₁.isConst && arg₂.isConst then let .const arg₁name _ := arg₁ - | throwError "processLam0Arg4 :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" let .const arg₂name _ := arg₂ - | throwError "processLam0Arg4 :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" if let .some (e', t) := reifMapLam0Arg4NoLit.get? (fnName, arg₁name, arg₂name) then if (← Meta.isDefEqD e e') then return .some t return .none if arg₁.isApp && arg₂.isConst then let .app arg₁fn arg₁arg := arg₁ - | throwError "processLam0Arg4 :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" if arg₁fn.isConst then let .const arg₁fnName _ := arg₁fn - | throwError "processLam0Arg4 :: Unexpected error {arg₁fn}" + | throwError "{decl_name%} :: Unexpected error {arg₁fn}" if let .some candidates := reifMapLam0Arg4NatLit.get? (fnName, arg₁fnName) then for (e'con, tcon) in candidates do if let .some n ← Meta.evalNat arg₁arg then @@ -1388,12 +1388,12 @@ def processLam0Arg4 (e fn arg₁ arg₂ arg₃ arg₄ : Expr) : MetaM (Option La return tcon n if arg₁.isApp && arg₂.isApp then let .app arg₁fn arg₁arg := arg₁ - | throwError "processLam0Arg4 :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" let .app arg₂fn arg₂arg := arg₂ - | throwError "processLam0Arg4 :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" if arg₁fn.isConst && arg₂fn.isConst then let .const arg₁fnName _ := arg₁fn - | throwError "processLam0Arg4 :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" if let .some candidates := reifMapLam0Arg4NatLitNatLitEq.get? (fnName, arg₁fnName) then for (e'con, tcon) in candidates do if let .some n ← Meta.evalNat arg₁arg then @@ -1481,7 +1481,7 @@ def reifTermCheckType (e : Expr) : ReifM (LamSort × LamTerm) := do let t ← reifTerm .empty e let ltv ← getLamTyValAtMeta let .some s := t.lamCheck? ltv Embedding.Lam.dfLCtxTy - | throwError "reifTermCheckType :: LamTerm {t} is not type correct" + | throwError "{decl_name%} :: LamTerm {t} is not type correct" return (s, t) /-- Return the positions of the reified and `resolveImport`-ed facts within the `validTable` -/ @@ -1489,7 +1489,7 @@ def reifFacts (facts : Array UMonoFact) : ReifM (Array LamTerm) := facts.mapM (fun ⟨proof, ty, deriv⟩ => do let (s, lamty) ← reifTermCheckType ty if s != .base .prop then - throwError "reifFacts :: Fact {lamty} is not of type `prop`" + throwError "{decl_name%} :: Fact {lamty} is not of type `prop`" trace[auto.lamReif.printResult] "Successfully reified proof of {← Meta.zetaReduce ty} to λterm `{lamty}`" newAssertion proof deriv lamty return lamty) @@ -1578,7 +1578,7 @@ section BuildChecker for re in (← getRTable) do if let .some cs := rst.chkMap.get? re then let .some n := rst.findPos? re - | throwError "buildChkStepsExpr :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" chkSteps := chkSteps.push (cs, n) -- `ChkMap` are run using `foldl`, so we use `BinTree.ofListFoldl` let e := Lean.toExpr (BinTree.ofListFoldl chkSteps.toList) @@ -1650,7 +1650,7 @@ section BuildChecker let itEntry := Lean.mkApp3 (.const ``importTablePSigmaMk [u]) chkValExpr ieExpr e importTable := importTable.insert n itEntry if t.maxLooseBVarSucc != 0 || t.maxEVarSucc != 0 then - throwError "buildImportTableExpr :: Invalid imported fact {t}" + throwError "{decl_name%} :: Invalid imported fact {t}" let veEntry := REntry.valid [] t importedFactsTree := importedFactsTree.insert n veEntry for (s, (inh, _, n)) in (← getInhabitations).toList do @@ -1683,7 +1683,7 @@ section BuildChecker let (itExpr, _) ← buildImportTableExpr cpvFVarExpr let csExpr ← buildChkStepsExpr let .valid lctx t := re - | throwError "buildFullCheckerExprFor :: {re} is not a `valid` entry" + | throwError "{decl_name%} :: {re} is not a `valid` entry" let vExpr := Lean.toExpr (← lookupREntryPos! re) let eqExpr ← Meta.mkAppM ``Eq.refl #[← Meta.mkAppM ``Option.some #[Lean.toExpr (lctx, t)]] let getEntry := Lean.mkApp7 (.const ``Checker.getValidExport_directReduce [u]) @@ -1709,7 +1709,7 @@ section BuildChecker let (itExpr, ifExpr) ← buildImportTableExpr cpvFVarExpr let csExpr ← buildChkStepsExpr let .valid lctx t := re - | throwError "buildFullCheckerExprFor :: {re} is not a `valid` entry" + | throwError "{decl_name%} :: {re} is not a `valid` entry" let vExpr := Lean.toExpr (← lookupREntryPos! re) let hImportExpr ← Meta.mkAppM ``Eq.refl #[ifExpr] let hLvtExpr ← Meta.mkAppM ``Eq.refl #[lvtExpr] @@ -1766,7 +1766,7 @@ section BuildChecker let csExpr ← buildChkStepsExpr let csNativeName ← mkNativeAuxDecl `lam_ssrefl_cs (Lean.mkConst ``ChkSteps) csExpr let .valid lctx t := re - | throwError "buildFullCheckerExprFor :: {re} is not a `valid` entry" + | throwError "{decl_name%} :: {re} is not a `valid` entry" let vExpr := Lean.toExpr (← lookupREntryPos! re) let hImportExpr ← Meta.mkAppM ``Eq.refl #[Lean.mkConst ifNativeName] let hLvtExpr ← Meta.mkAppM ``Eq.refl #[Lean.mkConst lvtNativeName] @@ -1891,7 +1891,7 @@ open Embedding.Lam LamReif trace[auto.buildChecker] "Collecting for etom {e} by ChkStep {cs}" let _ ← processChkStep ref cs let .some n := (← getEtomH2lMap).get? e - | throwError "transEtom :: Cannot find translation of etom {e}" + | throwError "{decl_name%} :: Cannot find translation of etom {e}" return n partial def transLamTerm (ref : State) : LamTerm → TransM LamTerm @@ -1974,11 +1974,11 @@ open Embedding.Lam LamReif match cs with | .nonemptyOfAtom n => do let .atom n' ← transLamTerm ref (.atom n) - | throwError "transChkStep :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" return .nonemptyOfAtom n' | .nonemptyOfEtom n => do let .etom n' ← transLamTerm ref (.etom n) - | throwError "transChkStep :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" return .nonemptyOfEtom n' | .p cs pos occ => return ChkStep.p cs (← transPos ref pos) occ | .w cs => ChkStep.w <$> @@ -1995,7 +1995,7 @@ open Embedding.Lam LamReif let cs' ← transChkStep ref cs setCsH2lMap ((← getCsH2lMap).insert cs cs') let (true, er) ← newChkStep cs' .none - | throwError "processChkStep :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" trace[auto.buildChecker] "Checkstep {cs} translated to {cs'}, producing {er}" match er with | .newEtomWithValid .. => do @@ -2017,22 +2017,22 @@ open Embedding.Lam LamReif trace[auto.buildChecker] "Collecting for {hre} by ChkStep {cs}" let er ← processChkStep ref cs match er with - | .fail => throwError "collectProofFor :: Unexpected evaluation result" + | .fail => throwError "{decl_name%} :: Unexpected evaluation result" | .addEntry reNew => do let expectedEntry ← transREntry ref hre - if expectedEntry != reNew then throwError "collectProofFor :: Entry mismatch" + if expectedEntry != reNew then throwError "{decl_name%} :: Entry mismatch" | .newEtomWithValid _ lctx t => do let expectedEntry ← transREntry ref hre - if expectedEntry != .valid lctx t then throwError "collectProofFor :: Entry mismatch" + if expectedEntry != .valid lctx t then throwError "{decl_name%} :: Entry mismatch" | .inhabitation e deriv _ => let .nonempty hs := hre - | throwError "collectProofFor :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" let s ← transLamSort ref hs newInhabitation e deriv s trace[auto.buildChecker] "Inhabitation fact {hs} translated to {s}" | .assertion e deriv _ => let .valid [] ht := hre - | throwError "collectProofFor :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" let t ← transLamTerm ref ht newAssertion e deriv t trace[auto.buildChecker] "Import fact {ht} translated to {t}" diff --git a/Auto/Translation/LamUtils.lean b/Auto/Translation/LamUtils.lean index e71b816..ad8ccd7 100644 --- a/Auto/Translation/LamUtils.lean +++ b/Auto/Translation/LamUtils.lean @@ -68,10 +68,10 @@ namespace LamExportUtils def collectLamBaseTermAtoms (b : LamBaseTerm) : CoreM (Std.HashSet Nat) := do let s? : Option LamSort ← (do match b with - | .eqI _ => throwError ("collectAtoms :: " ++ exportError.ImpPolyLog) - | .forallEI _ => throwError ("collectAtoms :: " ++ exportError.ImpPolyLog) - | .existEI _ => throwError ("collectAtoms :: " ++ exportError.ImpPolyLog) - | .iteI _ => throwError ("collectAtoms :: " ++ exportError.ImpPolyLog) + | .eqI _ => throwError (decl_name% ++ " :: " ++ exportError.ImpPolyLog) + | .forallEI _ => throwError (decl_name% ++ " :: " ++ exportError.ImpPolyLog) + | .existEI _ => throwError (decl_name% ++ " :: " ++ exportError.ImpPolyLog) + | .iteI _ => throwError (decl_name% ++ " :: " ++ exportError.ImpPolyLog) | .eq s => return .some s | .forallE s => return .some s | .existE s => return .some s @@ -95,11 +95,11 @@ namespace LamExportUtils LamTerm → CoreM (Std.HashSet Nat × Std.HashSet Nat × Std.HashSet Nat) | .atom n => do let .some s := lamVarTy[n]? - | throwError "collectAtoms :: Unknown term atom {n}" + | throwError "{decl_name%} :: Unknown term atom {n}" return (collectLamSortAtoms s, Std.HashSet.empty.insert n, Std.HashSet.empty) | .etom n => do let .some s := lamEVarTy[n]? - | throwError "collectAtoms :: Unknown etom {n}" + | throwError "{decl_name%} :: Unknown etom {n}" return (collectLamSortAtoms s, Std.HashSet.empty, Std.HashSet.empty.insert n) | .base b => do return (← collectLamBaseTermAtoms b, Std.HashSet.empty, Std.HashSet.empty) @@ -194,7 +194,7 @@ namespace Lam2D | .or => return .const ``Or [] | .imp => do let .some (.defnInfo impVal) := (← getEnv).find? ``ImpF - | throwError "interpLamBaseTermAsUnlifted :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" return impVal.value.instantiateLevelParams impVal.levelParams [.zero, .zero] | .iff => return .const ``Iff [] @@ -306,7 +306,7 @@ namespace Lam2D def interpLamSortAsUnlifted (tyVal : Std.HashMap Nat Expr) : LamSort → CoreM Expr | .atom n => do let .some e := tyVal.get? n - | throwError "interpLamSortAsUnlifted :: Cannot find fvarId assigned to type atom {n}" + | throwError "{decl_name%} :: Cannot find fvarId assigned to type atom {n}" return e | .base b => return Lam2D.interpLamBaseSortAsUnlifted b | .func s₁ s₂ => do @@ -314,18 +314,18 @@ namespace Lam2D def interpOtherConstAsUnlifted (tyVal : Std.HashMap Nat Expr) (oc : OtherConst) : MetaM Expr := do let .some (.defnInfo constIdVal) := (← getEnv).find? ``constId - | throwError "interpOtherConstAsUnlifted :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" let constIdExpr := fun params => constIdVal.value.instantiateLevelParams constIdVal.levelParams params match oc with | .smtAttr1T _ sattr sterm => do let tyattr ← interpLamSortAsUnlifted tyVal sattr let sortattr ← Expr.normalizeType (← Meta.inferType tyattr) let Expr.sort lvlattr := sortattr - | throwError "interpOtherConstAsUnlifted :: Unexpected sort {sortattr}" + | throwError "{decl_name%} :: Unexpected sort {sortattr}" let tyterm ← interpLamSortAsUnlifted tyVal sterm let sortterm ← Expr.normalizeType (← Meta.inferType tyterm) let Expr.sort lvlterm := sortterm - | throwError "interpOtherConstAsUnlifted :: Unexpected sort {sortterm}" + | throwError "{decl_name%} :: Unexpected sort {sortterm}" return Lean.mkApp2 (constIdExpr [lvlattr, lvlterm]) tyattr tyterm def interpLamBaseTermAsUnlifted (tyVal : Std.HashMap Nat Expr) : LamBaseTerm → MetaM Expr @@ -336,19 +336,19 @@ namespace Lam2D | .scst sc => Lam2D.interpStringConstAsUnlifted sc | .bvcst bvc => Lam2D.interpBitVecConstAsUnlifted bvc | .ocst oc => interpOtherConstAsUnlifted tyVal oc - | .eqI _ => throwError ("interpLamTermAsUnlifted :: " ++ LamExportUtils.exportError.ImpPolyLog) - | .forallEI _ => throwError ("interpLamTermAsUnlifted :: " ++ LamExportUtils.exportError.ImpPolyLog) - | .existEI _ => throwError ("interpLamTermAsUnlifted :: " ++ LamExportUtils.exportError.ImpPolyLog) - | .iteI _ => throwError ("interpLamTermAsUnlifted :: " ++ LamExportUtils.exportError.ImpPolyLog) + | .eqI _ => throwError (decl_name% ++ " :: " ++ LamExportUtils.exportError.ImpPolyLog) + | .forallEI _ => throwError (decl_name% ++ " :: " ++ LamExportUtils.exportError.ImpPolyLog) + | .existEI _ => throwError (decl_name% ++ " :: " ++ LamExportUtils.exportError.ImpPolyLog) + | .iteI _ => throwError (decl_name% ++ " :: " ++ LamExportUtils.exportError.ImpPolyLog) | .eq s => do return ← Meta.mkAppOptM ``Eq #[← interpLamSortAsUnlifted tyVal s] | .forallE s => do let ty ← interpLamSortAsUnlifted tyVal s let sort ← Expr.normalizeType (← Meta.inferType ty) let Expr.sort lvl := sort - | throwError "interpLamBaseTermAsUnlifted :: Unexpected sort {sort}" + | throwError "{decl_name%} :: Unexpected sort {sort}" let .some (.defnInfo forallVal) := (← getEnv).find? ``forallF - | throwError "interpLamBaseTermAsUnlifted :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" let forallFExpr := forallVal.value.instantiateLevelParams forallVal.levelParams [lvl, .zero] return mkAppN forallFExpr #[← interpLamSortAsUnlifted tyVal s] | .existE s => do @@ -369,11 +369,11 @@ namespace Lam2D (lctx : Nat) : LamTerm → MetaM Expr | .atom n => do let .some e := varVal.get? n - | throwError "interpLamTermAsUnlifted :: Cannot find fvarId assigned to term atom {n}" + | throwError "{decl_name%} :: Cannot find fvarId assigned to term atom {n}" return e | .etom n => do let .some efvar := etomVal.get? n - | throwError "interpLamSortAsUnlifted :: Cannot find fvarId assigned to etom {n}" + | throwError "{decl_name%} :: Cannot find fvarId assigned to etom {n}" return efvar | .base b => interpLamBaseTermAsUnlifted tyVal b | .bvar n => return .bvar n diff --git a/Auto/Translation/Monomorphization.lean b/Auto/Translation/Monomorphization.lean index 12b3f27..bc41cdd 100644 --- a/Auto/Translation/Monomorphization.lean +++ b/Auto/Translation/Monomorphization.lean @@ -184,7 +184,7 @@ def ConstInst.equiv (ci₁ ci₂ : ConstInst) : MetaM Bool := do let ⟨head₁, argsInst₁, idx₁⟩ := ci₁ let ⟨head₂, argsInst₂, idx₂⟩ := ci₂ if head₁.fingerPrint != head₂.fingerPrint then - throwError "ConstInst.equiv :: {ci₁.head} and {ci₂.head} have different fingerprints" + throwError "{decl_name%} :: {ci₁.head} and {ci₂.head} have different fingerprints" if !(← head₁.equiv head₂) then return false if argsInst₁.size != argsInst₂.size || idx₁ != idx₂ then @@ -207,7 +207,7 @@ def ConstInst.matchExpr (e : Expr) (ci : ConstInst) : MetaM Bool := do return false let argsIdx := ci.argsIdx if argsIdx.size != ci.argsInst.size then - throwError "ConstInst.matchExpr :: Unexpected error" + throwError "{decl_name%} :: Unexpected error" let args := e.getAppArgs for (idx, ciarg) in argsIdx.zip ci.argsInst do let .some arg := args[idx]? @@ -252,7 +252,7 @@ def ConstInst.ofExpr? (params : Array Name) (bvars : Array Expr) (e : Expr) : Me for (arg, idx) in args.zipWithIndex do headType ← Core.betaReduce headType let .forallE _ ty body bi := headType - | throwError "ConstInst.ofExpr? :: {headType} is not a `∀`" + | throwError "{decl_name%} :: {headType} is not a `∀`" if let some _ := ty.find? (fun e => bvarSet.contains e) then return .none if ← shouldInstantiate fn ty body bi then @@ -308,7 +308,7 @@ def ConstInst.toExpr (ci : ConstInst) : MetaM Expr := do for (arg, idx) in ci.argsInst.zip ci.argsIdx do args := args.setD idx (.some arg) let .some ret := ConstInst.toExprAux args.toList [] ci.head.toExpr type - | throwError "ConstInst.toExpr :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" return ret /-- @@ -350,9 +350,9 @@ private partial def collectConstInsts (params : Array Name) (bvars : Array Expr) return insts else return insts ++ (← collectConstInsts params bvars ty) -| .letE .. => throwError "collectConstInsts :: Let-expressions should have been reduced" -| .mdata .. => throwError "collectConstInsts :: mdata should have been consumed" -| .proj .. => throwError "collectConstInsts :: Projections should have been turned into ordinary expressions" +| .letE .. => throwError "{decl_name%} :: Let-expressions should have been reduced" +| .mdata .. => throwError "{decl_name%} :: mdata should have been consumed" +| .proj .. => throwError "{decl_name%} :: Projections should have been turned into ordinary expressions" | _ => return #[] where processOther (params : Array Name) (e : Expr) : MetaM (Array ConstInst) := do match ← ConstInst.ofExpr? params bvars e with @@ -380,7 +380,7 @@ def ConstInsts.canonicalize? (cis : ConstInsts) (ci : ConstInst) : MetaM (Option This function is used by `LemmaInst.matchConstInst` only -/ private partial def MLemmaInst.matchConstInst (ci : ConstInst) (mi : MLemmaInst) : Expr → MetaM (Std.HashSet LemmaInst) -| .bvar _ => throwError "MLemmaInst.matchConstInst :: Loose bound variable" +| .bvar _ => throwError "{decl_name%} :: Loose bound variable" | e@(.app ..) => do let args := e.getAppArgs let mut ret := Std.HashSet.empty @@ -395,7 +395,7 @@ private partial def MLemmaInst.matchConstInst (ci : ConstInst) (mi : MLemmaInst) let mut ret ← MLemmaInst.matchConstInst ci mi body for x in xs do let .fvar id := x - | throwError "MLemmaInst.matchConstInst :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" let type ← id.getType ret := mergeHashSet ret (← MLemmaInst.matchConstInst ci mi type) return ret @@ -403,9 +403,9 @@ private partial def MLemmaInst.matchConstInst (ci : ConstInst) (mi : MLemmaInst) let tyInst ← MLemmaInst.matchConstInst ci mi ty let bodyInst ← MLemmaInst.matchConstInst ci mi (body.instantiate1 x) return mergeHashSet tyInst bodyInst -| .letE .. => throwError "MLemmaInst.matchConstInst :: Let-expressions should have been reduced" -| .mdata .. => throwError "MLemmaInst.matchConstInst :: mdata should have been consumed" -| .proj .. => throwError "MLemmaInst.matchConstInst :: Projections should have been turned into ordinary expressions" +| .letE .. => throwError "{decl_name%} :: Let-expressions should have been reduced" +| .mdata .. => throwError "{decl_name%} :: mdata should have been consumed" +| .proj .. => throwError "{decl_name%} :: Projections should have been turned into ordinary expressions" | _ => return Std.HashSet.empty /-- Given a LemmaInst `li` and a ConstInst `ci`, try to match all subexpressions of `li` against `ci` -/ @@ -426,7 +426,7 @@ where match e with | .forallE name ty body bi => Meta.withLocalDecl name bi ty fun x => do let Expr.fvar xid := x - | throwError "Monomorphization.leadingForallQuasiMonomorphic :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" let bodyi := body.instantiate1 x if ← Meta.isProp ty then if !(← Meta.isProp bodyi) then @@ -472,7 +472,7 @@ def LemmaInst.monomorphic? (li : LemmaInst) : MetaM (Option LemmaInst) := do | return .none match mvar with | .mvar id => id.assign inst - | _ => throwError "LemmaInst.monomorphic? :: Unexpected error" + | _ => throwError "{decl_name%} :: Unexpected error" LemmaInst.ofMLemmaInst mi /- @@ -571,9 +571,9 @@ def dequeueActiveCi? : MonoM (Option (Expr × Nat)) := do def lookupActiveCi! (fgp : Expr) (idx : Nat) : MonoM ConstInst := do let .some cis := (← getCiMap).get? fgp - | throwError "lookupActiveCi :: Unknown CiHead {fgp}" + | throwError "{decl_name%} :: Unknown CiHead {fgp}" let .some ci := cis[idx]? - | throwError "lookupActiveCi :: Index {idx} out of bound" + | throwError "{decl_name%} :: Index {idx} out of bound" return ci def saturationThresholdReached? (cnt : Nat) : CoreM Bool := do @@ -718,7 +718,7 @@ namespace FVarRep let ci ← MetaState.runMetaM (do match ← CiMap.canonicalize? ciMap ci with | (true, _, ci') => return ci' - | _ => throwError "constInst2FVarId :: Cannot find canonicalized instance of {ci}") + | _ => throwError "{decl_name%} :: Cannot find canonicalized instance of {ci}") let ciIdMap ← FVarRep.getCiIdMap match ciIdMap.get? ci with | .some fid => return fid @@ -778,7 +778,7 @@ namespace FVarRep -- Type of λ binder cannot depend on previous bound variables let (ty, hasBfvars) ← processType ty if hasBfvars then - return .inr m!"replacePolyWithFVar :: Type {ty} of λ binder contains bound variables" + return .inr m!"{decl_name%} :: Type {ty} of λ binder contains bound variables" let fvarId ← MetaState.withLocalDecl name binfo ty .default setBfvars ((← getBfvars).push fvarId) let b' ← replacePolyWithFVar (body.instantiate1 (.fvar fvarId)) @@ -789,14 +789,14 @@ namespace FVarRep | e@(.forallE name ty body binfo) => do let tysort ← MetaState.runMetaM (do Expr.normalizeType (← Meta.inferType ty)) let .sort tylvl := tysort - | throwError "replacePolyWithFVar :: Unexpected error, {tysort} is not a sort" + | throwError "{decl_name%} :: Unexpected error, {tysort} is not a sort" let (ty, tyHasBfvars) ← processType ty let fvarId ← MetaState.withLocalDecl name binfo ty .default setBfvars ((← getBfvars).push fvarId) let body' := body.instantiate1 (.fvar fvarId) let bodysort ← MetaState.runMetaM <| do Expr.normalizeType (← Meta.inferType body') let .sort bodylvl := bodysort - | throwError "replacePolyWithFVar :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" let bodyrep ← replacePolyWithFVar body' let .inl bodyrep := bodyrep | return bodyrep @@ -805,9 +805,9 @@ namespace FVarRep -- of this `∀` does not occur in the body if ← MetaState.isLevelDefEqRigid tylvl .zero then if !(← MetaState.isLevelDefEqRigid bodylvl .zero) then - return .inr m!"replacePolyWithFVar :: In {e}, type of ∀ bound variable is of sort `Prop`, but body isn't of sort `Prop`" + return .inr m!"{decl_name%} :: In {e}, type of ∀ bound variable is of sort `Prop`, but body isn't of sort `Prop`" if body.hasLooseBVar 0 then - return .inr m!"replacePolyWithFVar :: In {e}, type of dependent ∀ bound variable is of sort `Prop`" + return .inr m!"{decl_name%} :: In {e}, type of dependent ∀ bound variable is of sort `Prop`" let impFun := Expr.const ``ImpF [.zero, .zero] addForallImpFInst impFun let tyrep ← replacePolyWithFVar ty @@ -819,7 +819,7 @@ namespace FVarRep -- bound variables else if tyHasBfvars then - return .inr m!"replacePolyWithFVar :: In {e}, type of ∀ bound variable is not of sort `Prop`, and depends on bound variables" + return .inr m!"{decl_name%} :: In {e}, type of ∀ bound variable is not of sort `Prop`, and depends on bound variables" let forallFun := Expr.app (.const ``forallF [tylvl, bodylvl]) ty addForallImpFInst forallFun let forallFunId ← replacePolyWithFVar forallFun diff --git a/Auto/Translation/Preprocessing.lean b/Auto/Translation/Preprocessing.lean index b2430e9..dc2d127 100644 --- a/Auto/Translation/Preprocessing.lean +++ b/Auto/Translation/Preprocessing.lean @@ -28,7 +28,7 @@ def elabLemma (stx : Term) (deriv : DTr) : TacticM Lemma := def addRecAsLemma (recVal : RecursorVal) : MetaM (Array Lemma) := do let some (.inductInfo indVal) := (← getEnv).find? recVal.getInduct - | throwError "Expected inductive datatype: {recVal.getInduct}" + | throwError "{decl_name%} :: Expected inductive datatype: {recVal.getInduct}" let expr := mkConst recVal.name (recVal.levelParams.map Level.param) let res ← forallBoundedTelescope (← inferType expr) recVal.getMajorIdx fun xs _ => do let expr := mkAppN expr xs @@ -39,7 +39,7 @@ def addRecAsLemma (recVal : RecursorVal) : MetaM (Array Lemma) := do let ctor := mkAppN ctor ys let expr := mkApp expr ctor let some redExpr ← reduceRecMatcher? expr - | throwError "Could not reduce recursor application: {expr}" + | throwError "{decl_name%} :: Could not reduce recursor application: {expr}" let redExpr ← Core.betaReduce redExpr let eq ← mkEq expr redExpr let proof ← mkEqRefl expr @@ -50,7 +50,7 @@ def addRecAsLemma (recVal : RecursorVal) : MetaM (Array Lemma) := do for lem in res do let ty' ← Meta.inferType lem.proof if !(← Meta.isDefEq ty' lem.type) then - throwError "addRecAsLemma :: Application type mismatch" + throwError "{decl_name%} :: Application type mismatch" return Array.mk res def elabDefEq (name : Name) : TacticM (Array Lemma) := do @@ -69,10 +69,10 @@ def elabDefEq (name : Name) : TacticM (Array Lemma) := do -- If we have inductively defined propositions, we might -- need to add constructors as lemmas | some (.ctorInfo _) => return #[] - | some (.opaqueInfo _) => throwError "Opaque constants cannot be provided as lemmas" - | some (.quotInfo _) => throwError "Quotient constants cannot be provided as lemmas" - | some (.inductInfo _) => throwError "Inductive types cannot be provided as lemmas" - | none => throwError "Unknown constant {name}" + | some (.opaqueInfo _) => throwError "{decl_name%} :: Opaque constants cannot be provided as lemmas" + | some (.quotInfo _) => throwError "{decl_name%} :: Quotient constants cannot be provided as lemmas" + | some (.inductInfo _) => throwError "{decl_name%} :: Inductive types cannot be provided as lemmas" + | none => throwError "{decl_name%} :: Unknown constant {name}" def isNonemptyInhabited (ty : Expr) : MetaM Bool := do let .some name ← Meta.isClass? ty @@ -86,9 +86,9 @@ structure ConstUnfoldInfo where def getConstUnfoldInfo (name : Name) : MetaM ConstUnfoldInfo := do let .some ci := (← getEnv).find? name - | throwError "getConstUnfoldInfo :: Unknown declaration {name}" + | throwError "{decl_name%} :: Unknown declaration {name}" let .some val := ci.value? - | throwError "getConstUnfoldInfo :: {name} is not a definition, thus cannot be unfolded" + | throwError "{decl_name%} :: {name} is not a definition, thus cannot be unfolded" let val ← prepReduceExpr val let params := ci.levelParams return ⟨name, val, ⟨params⟩⟩ @@ -110,13 +110,13 @@ partial def topoSortUnfolds (unfolds : Array ConstUnfoldInfo) : MetaM (Array Con let mut ret := #[] for name in nameArr do let .some ui := nameMap.get? name - | throwError "topoSortUnfolds :: Unexpected error" + | throwError "{decl_name%} :: Unexpected error" ret := ret.push ui return ret.reverse where go (depMap : Std.HashMap Name (Std.HashSet Name)) (stack : Std.HashSet Name) (n : Name) : StateRefT (Std.HashSet Name × Array Name) MetaM Unit := do if stack.contains n then - throwError "topoSortUnfolds :: Cyclic dependency" + throwError "{decl_name%} :: Cyclic dependency" let (done, ret) ← get if done.contains n then return diff --git a/Auto/Translation/Reduction.lean b/Auto/Translation/Reduction.lean index 7bc758d..a5e53b5 100644 --- a/Auto/Translation/Reduction.lean +++ b/Auto/Translation/Reduction.lean @@ -29,14 +29,14 @@ def unfoldProj (e : Expr) : MetaM Expr := match e with | .proj name idx struct => do let some (.inductInfo indi) := (← getEnv).find? name - | throwError s!"unfoldProj :: {name} is not a inductive type" + | throwError s!"{decl_name%} :: {name} is not a inductive type" let some structInfo := getStructureInfo? (← getEnv) name - | throwError s!"unfoldProj :: {name} is not a structure" + | throwError s!"{decl_name%} :: {name} is not a structure" let nameMap : Std.HashMap Name StructureFieldInfo := Std.HashMap.ofList (structInfo.fieldInfo.map (fun sfi => (sfi.fieldName, sfi))).toList let sorted := structInfo.fieldNames.map (fun name => nameMap.get? name) let .some (.some sfi) := sorted[idx]? - | throwError s!"unfoldProj :: Projection index out of bound" + | throwError s!"{decl_name%} :: Projection index out of bound" let nones : List (Option Expr) := (List.range indi.numParams).map (fun _ => .none) Meta.mkAppOptM sfi.projFn ((Array.mk nones).push struct) | _ => return e diff --git a/Auto/Translation/ReifM.lean b/Auto/Translation/ReifM.lean index e5256ce..c4a414c 100644 --- a/Auto/Translation/ReifM.lean +++ b/Auto/Translation/ReifM.lean @@ -42,11 +42,11 @@ abbrev ReifM := StateT State MetaM @[inline] def resolveTy (e : Expr) : ReifM Expr := do match (← getTyCanMap).get? (Expr.eraseMData e) with | .some id => return id - | .none => throwError "resolveTy :: Unable to resolve {e}" + | .none => throwError "{decl_name%} :: Unable to resolve {e}" def mkAuxName (suffix : Name) : ReifM Name := do match (← getDeclName?) with - | none => throwError "ReifM.mkAuxName :: auxiliary declaration cannot be created when declaration name is not available" + | none => throwError "{decl_name%} :: auxiliary declaration cannot be created when declaration name is not available" | some declName => Lean.mkAuxName (declName ++ suffix) 1 end Auto.Reif diff --git a/Doc/LamPULift.lean b/Doc/LamPULift.lean index d3790d5..2c0524c 100644 --- a/Doc/LamPULift.lean +++ b/Doc/LamPULift.lean @@ -30,7 +30,7 @@ initialize Note that `types/terms depending on types` are not fully supported For example, if we have const/fvar `f : ∀ (α : Type), α → Prop` and `h : Nat → Nat`, then calling `termLift` on `f (Nat → Nat) h` - would fail. This is because + would fail. This is because (1) `h` will be lifted to `hLift : GLift Nat → GLift Nat`, so The lifted version of `f (Nat → Nat)` must have type `(GLift Nat → GLift Nat) → GLift Prop` @@ -78,11 +78,11 @@ mutual -- In the return type, the first `Expr` is `e↑`, and the second `Expr` is -- the type of `e↑` partial def cstULiftPos (u : Level) (e : Expr) : (ty : Expr) → MetaM (Expr × Expr) - | .bvar idx => throwError "Auto.cstULift :: Loose bound variable" - | .lam .. => throwError "Auto.cstULift :: Please β-reduce type before calling cstULift" - | .letE .. => throwError "Auto.cstULift :: Please ζ-reduce type before calling cstULift" - | .lit .. => throwError "Auto.cstULift :: Malformed type" - | .proj .. => throwError "Auto.cstULift :: Please unfold projections in type before calling cstULift" + | .bvar idx => throwError "{decl_name%} :: Loose bound variable" + | .lam .. => throwError "{decl_name%} :: Please β-reduce type before calling cstULift" + | .letE .. => throwError "{decl_name%} :: Please ζ-reduce type before calling cstULift" + | .lit .. => throwError "{decl_name%} :: Malformed type" + | .proj .. => throwError "{decl_name%} :: Please unfold projections in type before calling cstULift" | .forallE name biTy body binfo => do -- We want to reate a free variable (intended) of type `bity↑`. -- However, we still don't what's `bity↑`, so we first @@ -120,7 +120,7 @@ mutual -- The same holds for `cstULiftNeg` let sort ← instantiateMVars (← Meta.inferType ty) if !sort.isSort then - throwError "Auto.ULift :: Expected sort" + throwError "{decl_name%} :: Expected sort" let lvl := sort.sortLevel! let eUpTy := mkApp (.const ``GLift [lvl, u]) ty let eUp := mkAppN (.const ``GLift.up [lvl, u]) #[ty, e] @@ -128,11 +128,11 @@ mutual /-- In the return type, the first `Expr` is `eUp↓`, and the second `Expr` is the type of `e↑` -/ partial def cstULiftNeg (u : Level) (eUp : Expr) : (ty : Expr) → MetaM (Expr × Expr) - | .bvar idx => throwError "Auto.cstULift :: Loose bound variable" - | .lam .. => throwError "Auto.cstULift :: Please β-reduce type before calling cstULift" - | .letE .. => throwError "Auto.cstULift :: Please ζ-reduce type before calling cstULift" - | .lit .. => throwError "Auto.cstULift :: Malformed type" - | .proj .. => throwError "Auto.cstULift :: Please unfold projections in type before calling cstULift" + | .bvar idx => throwError "{decl_name%} :: Loose bound variable" + | .lam .. => throwError "{decl_name%} :: Please β-reduce type before calling cstULift" + | .letE .. => throwError "{decl_name%} :: Please ζ-reduce type before calling cstULift" + | .lit .. => throwError "{decl_name%} :: Malformed type" + | .proj .. => throwError "{decl_name%} :: Please unfold projections in type before calling cstULift" | .mdata data ty' => cstULiftNeg u eUp ty' | .forallE name biTy body binfo => do -- `upFunc` is such that `upFunc binder` is equivalent to `binder↑` @@ -163,7 +163,7 @@ mutual | ty => do let sort ← instantiateMVars (← Meta.inferType ty) if !sort.isSort then - throwError "Auto.ULift :: Expected sort" + throwError "{decl_name%} :: Expected sort" let lvl := sort.sortLevel! let eUpTy := mkApp (.const ``GLift [lvl, u]) ty let eUpDown := mkAppN (.const ``GLift.down [lvl, u]) #[ty, eUp] @@ -191,10 +191,9 @@ section TestcstULift let (eup, eupTy) ← cstULiftPos (.param `tmp) e ety let eup ← postProcessULift eup logInfo eup - + set_option pp.universes true set_option pp.funBinderTypes true - set_option pp.structureProjections false private def f₁ := fun (x : Nat) => x #getExprAndApply [f₁ | ulift] @@ -270,7 +269,7 @@ noncomputable def A_Constant.Lift.{u} := fun /- Now, we want to implement a function `termULift` which lifts an expressions - `e` to `GLift.up e`, such that all the constants occurring in `e↑` are [lifted + `e` to `GLift.up e`, such that all the constants occurring in `e↑` are [lifted counterparts of constants in `e`]. To do this, the function requires that all the constants in `e` has already had their lifted counterparts calculated. Before we implement this function, let's first look at what we'll obtain @@ -325,4 +324,4 @@ noncomputable def example₁.Lift.{u} := fun (*) Introduce a let binder `let fvarp↑ : ty↑ := body↑` into the local context -/ -end Auto.LamPULift \ No newline at end of file +end Auto.LamPULift