diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean index 0db2160a57..0a246245d9 100644 --- a/src/Lean/Elab/PreDefinition/Main.lean +++ b/src/Lean/Elab/PreDefinition/Main.lean @@ -64,8 +64,14 @@ preDefs.forM ensureNoUnassignedMVarsAtPreDef; addAndCompileUnsafe preDefs else if preDefs.any fun preDef => preDef.modifiers.isPartial then addAndCompilePartial preDefs - else unlessM (structuralRecursion preDefs) do - WFRecursion preDefs - + else + mapError + (orelseMergeErrors + (structuralRecursion preDefs) + (WFRecursion preDefs)) + (fun msg => + let preDefMsgs := preDefs.toList.map fun preDef => MessageData.ofExpr $ mkConst preDef.declName; + "fail to show that" ++ indentD (MessageData.joinSep preDefMsgs Format.line) + ++ Format.line ++ "terminate, errors:" ++ Format.line ++ msg) end Elab end Lean diff --git a/src/Lean/Elab/PreDefinition/Structural.lean b/src/Lean/Elab/PreDefinition/Structural.lean index 41f189be88..0a572e457d 100644 --- a/src/Lean/Elab/PreDefinition/Structural.lean +++ b/src/Lean/Elab/PreDefinition/Structural.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ import Lean.Util.ForEachExpr +import Lean.Meta.ForEachExpr import Lean.Meta.RecursorInfo import Lean.Meta.Match.Match import Lean.Elab.PreDefinition.Basic @@ -12,14 +13,6 @@ namespace Lean namespace Elab open Meta -def registerStructualId : IO InternalExceptionId := -registerInternalExceptionId `structuralRec -@[init registerStructualId] -constant structuralExceptionId : InternalExceptionId := arbitrary _ - -def throwStructuralFailed {α m} [MonadExceptOf Exception m] : m α := -throw $ Exception.internal structuralExceptionId - private def getFixedPrefix (declName : Name) (xs : Array Expr) (value : Expr) : Nat := let visitor {ω} : StateRefT Nat (ST ω) Unit := value.forEach' fun e => @@ -70,6 +63,9 @@ indParams.findSomeM? fun p => do (pure (some (p, y))) (pure none) +private def throwStructuralFailed {α} : MetaM α := +throwError "structural recursion cannot be used" + private partial def findRecArgAux {α} (numFixed : Nat) (xs : Array Expr) (k : RecArgInfo → MetaM α) : Nat → MetaM α | i => if h : i < xs.size then do @@ -85,14 +81,15 @@ private partial def findRecArgAux {α} (numFixed : Nat) (xs : Array Expr) (k : R let indArgs := xType.getAppArgs; let indParams := indArgs.extract 0 indInfo.nparams; let indIndices := indArgs.extract indInfo.nparams indArgs.size; - if !indIndices.all Expr.isFVar then do - trace! `Elab.definition.structural - ("argument #" ++ toString (i+1) ++ " was not used because its type is an inductive family and indices are not variables" ++ indentExpr xType); - findRecArgAux (i+1) - else if !indIndices.allDiff then do - trace! `Elab.definition.structural - ("argument #" ++ toString (i+1) ++ " was not used because its type is an inductive family and indices are not pairwise distinct" ++ indentExpr xType); - findRecArgAux (i+1) + if !indIndices.all Expr.isFVar then + orelseMergeErrors + (throwError $ "argument #" ++ toString (i+1) ++ " was not used because its type is an inductive family and indices are not variables" ++ indentExpr xType) + (findRecArgAux (i+1)) + else if !indIndices.allDiff then + orelseMergeErrors + (throwError $ "argument #" ++ toString (i+1) + ++ " was not used because its type is an inductive family and indices are not pairwise distinct" ++ indentExpr xType) + (findRecArgAux (i+1)) else do let indexMinPos := getIndexMinPos xs indIndices; let numFixed := if indexMinPos < numFixed then indexMinPos else numFixed; @@ -100,24 +97,26 @@ private partial def findRecArgAux {α} (numFixed : Nat) (xs : Array Expr) (k : R let ys := xs.extract numFixed xs.size; badDep? ← hasBadIndexDep? ys indIndices; match badDep? with - | some (index, y) => do - trace! `Elab.definition.structural - ("argument #" ++ toString (i+1) ++ " was not used because its type is an inductive family" ++ indentExpr xType ++ - Format.line ++ "and index" ++ indentExpr index ++ - Format.line ++ "depends on the non index" ++ indentExpr y); - findRecArgAux (i+1) + | some (index, y) => + orelseMergeErrors + (throwError $ + "argument #" ++ toString (i+1) ++ " was not used because its type is an inductive family" ++ indentExpr xType ++ + Format.line ++ "and index" ++ indentExpr index ++ + Format.line ++ "depends on the non index" ++ indentExpr y) + (findRecArgAux (i+1)) | none => do badDep? ← hasBadParamDep? ys indParams; match badDep? with - | some (indParam, y) => do - trace! `Elab.definition.structural - ("argument #" ++ toString (i+1) ++ " was not used because its type is an inductive datatype" ++ indentExpr xType ++ - Format.line ++ "and parameter" ++ indentExpr indParam ++ - Format.line ++ "depends on" ++ indentExpr y); - findRecArgAux (i+1) + | some (indParam, y) => + orelseMergeErrors + (throwError $ + "argument #" ++ toString (i+1) ++ " was not used because its type is an inductive datatype" ++ indentExpr xType ++ + Format.line ++ "and parameter" ++ indentExpr indParam ++ + Format.line ++ "depends on" ++ indentExpr y) + (findRecArgAux (i+1)) | none => do let indicesPos := indIndices.map fun index => match ys.indexOf index with | some i => i.val | none => unreachable!; - catchInternalId structuralExceptionId + orelseMergeErrors (k { fixedParams := fixedParams, ys := ys, pos := i - fixedParams.size, indicesPos := indicesPos, indName := indInfo.name, @@ -125,7 +124,7 @@ private partial def findRecArgAux {α} (numFixed : Nat) (xs : Array Expr) (k : R indParams := indParams, indIndices := indIndices, reflexive := indInfo.isReflexive }) - (fun _ => findRecArgAux (i+1)) + (findRecArgAux (i+1)) else throwStructuralFailed @@ -135,6 +134,14 @@ findRecArgAux numFixed xs k numFixed private def containsRecFn (recFnName : Name) (e : Expr) : Bool := (e.find? fun e => e.isConstOf recFnName).isSome +private def ensureNoRecFn (recFnName : Name) (e : Expr) : MetaM Expr := do +if containsRecFn recFnName e then do + Meta.forEachExpr e fun e => when (e.isAppOf recFnName) $ + throwError $ "unexpected occurrence of recursive application" ++ indentExpr e; + pure e +else + pure e + private partial def replaceRecApps (recFnName : Name) (argInfo : RecArgInfo) : Expr → Expr → MetaM Expr | below, e@(Expr.lam _ _ _ _) => lambdaTelescope e fun xs b => do b ← replaceRecApps below b; mkLambdaFVars xs b | below, Expr.letE n type val body _ => do @@ -160,31 +167,19 @@ private partial def replaceRecApps (recFnName : Name) (argInfo : RecArgInfo) : E | some matcherApp => if !containsRecFn recFnName e then processApp e else do - matcherApp ← catch (matcherApp.addArg below) - (fun ex => do - trace! `Elab.definition.structural - ("failed to add `below` argument to 'matcher' application" ++ indentD ex.toMessageData); - throwStructuralFailed); + matcherApp ← mapError (matcherApp.addArg below) (fun msg => "failed to add `below` argument to 'matcher' application" ++ indentD msg); altsNew ← (Array.zip matcherApp.alts matcherApp.altNumParams).mapM fun ⟨alt, numParams⟩ => lambdaTelescope alt fun xs altBody => do { trace! `Elab.definition.structural ("altNumParams: " ++ toString numParams ++ ", xs: " ++ xs); - unless (xs.size >= numParams) do { - trace! `Elab.definition.structural - ("unexpected matcher application alternative " ++ indentExpr alt ++ Format.line ++ "at application" ++ indentExpr e); - throwStructuralFailed - }; + unless (xs.size >= numParams) $ + throwError $ "unexpected matcher application alternative " ++ indentExpr alt ++ Format.line ++ "at application" ++ indentExpr e; let belowForAlt := xs.get! (numParams - 1); altBodyNew ← replaceRecApps belowForAlt altBody; mkLambdaFVars xs altBodyNew }; pure { matcherApp with alts := altsNew }.toExpr | none => processApp e -| _, e => - if containsRecFn recFnName e then do - trace! `Elab.definition.structural ("unexpected occurrence of recursive function at" ++ indentExpr e); - throwStructuralFailed - else - pure e +| _, e => ensureNoRecFn recFnName e private def mkBRecOn (recFnName : Name) (argInfo : RecArgInfo) (value : Expr) : MetaM Expr := do type ← inferType value; @@ -229,23 +224,17 @@ lambdaTelescope preDef.value fun xs value => do valueNew ← mkBRecOn preDef.declName argInfo value; valueNew ← mkLambdaFVars xs valueNew; trace! `Elab.definition.structural ("result: " ++ valueNew); - if containsRecFn preDef.declName valueNew then do - -- This can happen when the recursive function occurs in expressions that are not visited by replaceRecApps (e.g., types) - trace! `Elab.definition.structural ("unexpected occurrence of recursive function at" ++ indentExpr valueNew); - throwStructuralFailed - else - pure { preDef with value := valueNew } + -- Recursive applications may still occur in expressions that were not visited by replaceRecApps (e.g., in types) + valueNew ← ensureNoRecFn preDef.declName valueNew; + pure { preDef with value := valueNew } -def structuralRecursion (preDefs : Array PreDefinition) : TermElabM Bool := +def structuralRecursion (preDefs : Array PreDefinition) : TermElabM Unit := if preDefs.size != 1 then - pure false -else - catchInternalId structuralExceptionId - (do preDefNonRec ← liftMetaM $ elimRecursion (preDefs.get! 0); - addNonRec preDefNonRec; - addAndCompileUnsafeRec preDefs; - pure true) - (fun _ => pure false) + throwError "structural recursion does not handle mutually recursive functions" +else do + preDefNonRec ← liftMetaM $ elimRecursion (preDefs.get! 0); + addNonRec preDefNonRec; + addAndCompileUnsafeRec preDefs @[init] private def regTraceClasses : IO Unit := do registerTraceClass `Elab.definition.structural; diff --git a/src/Lean/Elab/PreDefinition/WF.lean b/src/Lean/Elab/PreDefinition/WF.lean index 8d15ee678c..42d9fe9907 100644 --- a/src/Lean/Elab/PreDefinition/WF.lean +++ b/src/Lean/Elab/PreDefinition/WF.lean @@ -10,7 +10,7 @@ namespace Elab open Meta def WFRecursion (preDefs : Array PreDefinition) : TermElabM Unit := -throwError "WIP" +throwError "well founded recursion has not been implemented yet" end Elab end Lean diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index f81b11adf3..ff2c307492 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -1002,6 +1002,40 @@ catch x (fun _ => do setEnv env; setMCtx mctx; y) instance Meta.hasOrelse {α} : HasOrelse (MetaM α) := ⟨Meta.orelse⟩ +@[inline] private def orelseMergeErrorsImp {α} (x y : MetaM α) + (mergeRef : Syntax → Syntax → Syntax := fun r₁ r₂ => r₁) + (mergeMsg : MessageData → MessageData → MessageData := fun m₁ m₂ => m₁ ++ Format.line ++ m₂) + : MetaM α := do +env ← getEnv; +mctx ← getMCtx; +catch x fun ex => do + setEnv env; setMCtx mctx; + match ex with + | Exception.error ref₁ m₁ => + catch y fun ex => match ex with + | Exception.error ref₂ m₂ => throw $ Exception.error (mergeRef ref₁ ref₂) (mergeMsg m₁ m₂) + | _ => throw ex + | _ => throw ex + +/-- + Similar to `orelse`, but merge errors. Note that internal errors are not caught. + The default `mergeRef` uses the `ref` (position information) for the first message. + The default `mergeMsg` combines error messages using `Format.line ++ Format.line` as a separator. -/ +@[inline] def orelseMergeErrors {α m} [MonadControlT MetaM m] [Monad m] (x y : m α) + (mergeRef : Syntax → Syntax → Syntax := fun r₁ r₂ => r₁) + (mergeMsg : MessageData → MessageData → MessageData := fun m₁ m₂ => m₁ ++ Format.line ++ Format.line ++ m₂) + : m α := do +controlAt MetaM fun runInBase => orelseMergeErrorsImp (runInBase x) (runInBase y) mergeRef mergeMsg + +/-- Execute `x`, and apply `f` to the produced error message -/ +def mapErrorImp {α} (x : MetaM α) (f : MessageData → MessageData) : MetaM α := +catch x fun ex => match ex with + | Exception.error ref msg => throw $ Exception.error ref $ f msg + | _ => throw ex + +@[inline] def mapError {α m} [MonadControlT MetaM m] [Monad m] (x : m α) (f : MessageData → MessageData) : m α := +controlAt MetaM fun runInBase => mapErrorImp (runInBase x) f + /-- `commitWhenSome? x` executes `x` and keep modifications when it returns `some a`. -/ @[specialize] def commitWhenSome? {α} (x? : MetaM (Option α)) : MetaM (Option α) := do env ← getEnv;