From 4b58c4cc025434f685262cc154135a5ef658652e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 Aug 2021 17:18:55 -0700 Subject: [PATCH] refactor: instances that "hide" coercions MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Example: ``` instance [CoeHTCT α β] [Add β] : HAdd α β β where hAdd a b := Add.add a b ``` --- src/Init/Coe.lean | 50 ------ src/Lean/Data/Json/Basic.lean | 12 +- src/Lean/Elab/Print.lean | 2 +- src/Lean/Elab/StructInst.lean | 2 +- src/Lean/Meta/IndPredBelow.lean | 268 ++++++++++++++++---------------- 5 files changed, 142 insertions(+), 192 deletions(-) diff --git a/src/Init/Coe.lean b/src/Init/Coe.lean index 773e46b14e..f4382de448 100644 --- a/src/Init/Coe.lean +++ b/src/Init/Coe.lean @@ -145,53 +145,3 @@ instance [CoeFun α (fun _ => β)] : CoeTail α β where instance [CoeSort α β] : CoeTail α β where coe a := coeSort a - -/- Coe and heterogeneous operators, we use `CoeHTCT` instead of `CoeT` to avoid expensive coercions such as `CoeDep` -/ - -instance [CoeHTCT α β] [Add β] : HAdd α β β where - hAdd a b := Add.add a b - -instance [CoeHTCT α β] [Add β] : HAdd β α β where - hAdd a b := Add.add a b - -instance [CoeHTCT α β] [Sub β] : HSub α β β where - hSub a b := Sub.sub a b - -instance [CoeHTCT α β] [Sub β] : HSub β α β where - hSub a b := Sub.sub a b - -instance [CoeHTCT α β] [Mul β] : HMul α β β where - hMul a b := Mul.mul a b - -instance [CoeHTCT α β] [Mul β] : HMul β α β where - hMul a b := Mul.mul a b - -instance [CoeHTCT α β] [Div β] : HDiv α β β where - hDiv a b := Div.div a b - -instance [CoeHTCT α β] [Div β] : HDiv β α β where - hDiv a b := Div.div a b - -instance [CoeHTCT α β] [Mod β] : HMod α β β where - hMod a b := Mod.mod a b - -instance [CoeHTCT α β] [Mod β] : HMod β α β where - hMod a b := Mod.mod a b - -instance [CoeHTCT α β] [Append β] : HAppend α β β where - hAppend a b := Append.append a b - -instance [CoeHTCT α β] [Append β] : HAppend β α β where - hAppend a b := Append.append a b - -instance [CoeHTCT α β] [OrElse β] : HOrElse α β β where - hOrElse a b := OrElse.orElse a b - -instance [CoeHTCT α β] [OrElse β] : HOrElse β α β where - hOrElse a b := OrElse.orElse a b - -instance [CoeHTCT α β] [AndThen β] : HAndThen α β β where - hAndThen a b := AndThen.andThen a b - -instance [CoeHTCT α β] [AndThen β] : HAndThen β α β where - hAndThen a b := AndThen.andThen a b diff --git a/src/Lean/Data/Json/Basic.lean b/src/Lean/Data/Json/Basic.lean index 7bae4d83ec..72041a9be6 100644 --- a/src/Lean/Data/Json/Basic.lean +++ b/src/Lean/Data/Json/Basic.lean @@ -78,10 +78,10 @@ instance : LT JsonNumber := instance (a b : JsonNumber) : Decidable (a < b) := inferInstanceAs (Decidable (lt a b = true)) - + instance : Ord JsonNumber where - compare x y := - if x < y then Ordering.lt + compare x y := + if x < y then Ordering.lt else if x > y then Ordering.gt else Ordering.eq @@ -99,7 +99,7 @@ protected def toString : JsonNumber → String let exp := if exp < 0 then exp else 0 let e' := (10 : Int) ^ (e - exp.natAbs) let left := (m / e').repr - let right := e' + m % e' + let right := e' + coe m % e' |>.repr.toSubstring.drop 1 |>.dropRightWhile (fun c => c = '0') |>.toString @@ -188,14 +188,14 @@ def getNum? : Json → Except String JsonNumber | _ => throw "number expected" def getObjVal? : Json → String → Except String Json - | obj kvs, k => + | obj kvs, k => match kvs.find compare k with | some v => v | none => throw s!"property not found: {k}" | _ , _ => throw "object expected" def getArrVal? : Json → Nat → Except String Json - | arr a, i => + | arr a, i => match a.get? i with | some v => v | none => throw s!"index out of bounds: {i}" diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean index bead86786e..070af7e067 100644 --- a/src/Lean/Elab/Print.lean +++ b/src/Lean/Elab/Print.lean @@ -17,7 +17,7 @@ private def levelParamsToMessageData (levelParams : List Name) : MessageData := | u::us => do let mut m := m!".\{{u}" for u in us do - m := m ++ ", " ++ u + m := m ++ ", " ++ toMessageData u return m ++ "}" private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (safety : DefinitionSafety) : CommandElabM MessageData := do diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean index 1be8b4141c..844d79f634 100644 --- a/src/Lean/Elab/StructInst.lean +++ b/src/Lean/Elab/StructInst.lean @@ -280,7 +280,7 @@ partial def Struct.allDefault (s : Struct) : Bool := | FieldVal.nested s => allDefault s def formatField (formatStruct : Struct → Format) (field : Field Struct) : Format := - Format.joinSep field.lhs " . " ++ " := " ++ + Format.joinSep field.lhs " . " ++ format " := " ++ match field.val with | FieldVal.term v => v.prettyPrint | FieldVal.nested s => formatStruct s diff --git a/src/Lean/Meta/IndPredBelow.lean b/src/Lean/Meta/IndPredBelow.lean index 0427646ef5..dfe4dcd0f6 100644 --- a/src/Lean/Meta/IndPredBelow.lean +++ b/src/Lean/Meta/IndPredBelow.lean @@ -16,11 +16,11 @@ open Match register_builtin_option maxBackwardChainingDepth : Nat := { defValue := 10 descr := "The maximum search depth used in the backwards chaining part of the proof of `brecOn` for inductive predicates." - } + } /-- The context used in the creation of the `below` scheme for inductive predicates. --/ +-/ structure Context where motives : Array (Name × Expr) typeInfos : Array InductiveVal @@ -40,7 +40,7 @@ structure Variables where motives : Array Expr innerType : Expr deriving Inhabited - + /-- Collection of variables used to keep track of the local context used in the `brecOn` proof. -/ @@ -58,46 +58,46 @@ def mkContext (declName : Name) : MetaM Context := do let motives ←motiveTypes.mapIdxM fun j motive => do (←motiveName motiveTypes j.val, motive) let headers := typeInfos.mapM $ mkHeader motives indVal.numParams - return { + return { motives := motives typeInfos := typeInfos numParams := indVal.numParams headers := ←headers belowNames := ←indVal.all.toArray.map (· ++ `below) } -where - motiveName (motiveTypes : Array Expr) (i : Nat) : MetaM Name := - if motiveTypes.size > 1 +where + motiveName (motiveTypes : Array Expr) (i : Nat) : MetaM Name := + if motiveTypes.size > 1 then mkFreshUserName s!"motive_{i.succ}" else mkFreshUserName "motive" - mkHeader - (motives : Array (Name × Expr)) - (numParams : Nat) + mkHeader + (motives : Array (Name × Expr)) + (numParams : Nat) (indVal : InductiveVal) : MetaM Expr := do let header ← forallTelescope indVal.type fun xs t => do withNewBinderInfos (xs.map fun x => (x.fvarId!, BinderInfo.implicit)) $ mkForallFVars xs $ ←mkArrow (mkAppN (mkIndValConst indVal) xs) t addMotives motives numParams header - addMotives (motives : Array (Name × Expr)) (numParams : Nat) : Expr → MetaM Expr := - motives.foldrM (fun (motiveName, motive) t => - forallTelescope t fun xs s => do + addMotives (motives : Array (Name × Expr)) (numParams : Nat) : Expr → MetaM Expr := + motives.foldrM (fun (motiveName, motive) t => + forallTelescope t fun xs s => do let motiveType ← instantiateForall motive xs[:numParams] withLocalDecl motiveName BinderInfo.implicit motiveType fun motive => do mkForallFVars (xs.insertAt numParams motive) s) - - motiveType (indVal : InductiveVal) : MetaM Expr := + + motiveType (indVal : InductiveVal) : MetaM Expr := forallTelescope indVal.type fun xs t => do mkForallFVars xs $ ←mkArrow (mkAppN (mkIndValConst indVal) xs) (mkSort levelZero) mkIndValConst (indVal : InductiveVal) : Expr := mkConst indVal.name $ indVal.levelParams.map mkLevelParam - -partial def mkCtorType - (ctx : Context) - (belowIdx : Nat) - (originalCtor : ConstructorVal) : MetaM Expr := - forallTelescope originalCtor.type fun xs t => addHeaderVars + +partial def mkCtorType + (ctx : Context) + (belowIdx : Nat) + (originalCtor : ConstructorVal) : MetaM Expr := + forallTelescope originalCtor.type fun xs t => addHeaderVars { innerType := t indVal := #[] motives := #[] @@ -110,13 +110,13 @@ where (ctx.belowNames[idx], fun _ => pure header) withLocalDeclsD headersWithNames fun xs => - addMotives { vars with indVal := xs } + addMotives { vars with indVal := xs } addMotives (vars : Variables) := do - let motiveBuilders ← ctx.motives.mapM fun (motiveName, motiveType) => - (motiveName, BinderInfo.implicit, fun _ => + let motiveBuilders ← ctx.motives.mapM fun (motiveName, motiveType) => + (motiveName, BinderInfo.implicit, fun _ => instantiateForall motiveType vars.params) - withLocalDecls motiveBuilders fun xs => + withLocalDecls motiveBuilders fun xs => modifyBinders { vars with target := vars.target ++ xs, motives := xs } 0 modifyBinders (vars : Variables) (i : Nat) := do @@ -131,24 +131,24 @@ where else modifyBinders { vars with target := vars.target.push binder } i.succ else rebuild vars - rebuild (vars : Variables) := + rebuild (vars : Variables) := vars.innerType.withApp fun f args => do - let hApp := - mkAppN + let hApp := + mkAppN (mkConst originalCtor.name $ ctx.typeInfos[0].levelParams.map mkLevelParam) (vars.params ++ vars.args) let innerType := mkAppN vars.indVal[belowIdx] $ vars.params ++ vars.motives ++ args[ctx.numParams:] ++ #[hApp] - let x ← mkForallFVars vars.target innerType + let x ← mkForallFVars vars.target innerType replaceTempVars vars x replaceTempVars (vars : Variables) (ctor : Expr) := - let levelParams := + let levelParams := ctx.typeInfos[0].levelParams.map mkLevelParam ctor.replaceFVars vars.indVal $ ctx.belowNames.map fun indVal => mkConst indVal levelParams - + checkCount (domain : Expr) : MetaM Bool := do let run (x : StateRefT Nat MetaM Expr) : MetaM (Expr × Nat) := StateRefT'.run x 0 let (_, cnt) ←run $ transform domain fun e => do @@ -158,15 +158,15 @@ where set $ cnt + 1 TransformStep.visit e - if cnt > 1 then + if cnt > 1 then throwError "only arrows are allowed as premises. Multiple recursive occurrences detected:{indentExpr domain}" - + return cnt == 1 - - mkBelowBinder - (vars : Variables) - (binder : Expr) - (domain : Expr) + + mkBelowBinder + (vars : Variables) + (binder : Expr) + (domain : Expr) {α : Type} (k : Nat → Expr → MetaM α) : MetaM α := do forallTelescope domain fun xs t => do let fail _ := do @@ -174,33 +174,33 @@ where t.withApp fun f args => do if let some name := f.constName? then - if let some idx := ctx.typeInfos.findIdx? + if let some idx := ctx.typeInfos.findIdx? fun indVal => indVal.name == name then let indVal := ctx.typeInfos[idx] let hApp := mkAppN binder xs - let t := + let t := mkAppN vars.indVal[idx] $ vars.params ++ vars.motives ++ args[ctx.numParams:] ++ #[hApp] let newDomain ← mkForallFVars xs t - + withLocalDecl (←copyVarName binder.fvarId!) binder.binderInfo newDomain (k idx) else fail () else fail () - mkMotiveBinder - (vars : Variables) - (indValIdx : Nat) - (binder : Expr) - (domain : Expr) + mkMotiveBinder + (vars : Variables) + (indValIdx : Nat) + (binder : Expr) + (domain : Expr) {α : Type} (k : Expr → MetaM α) : MetaM α := do forallTelescope domain fun xs t => do t.withApp fun f args => do let hApp := mkAppN binder xs let t := mkAppN vars.motives[indValIdx] $ args[ctx.numParams:] ++ #[hApp] let newDomain ← mkForallFVars xs t - - withLocalDecl (←copyVarName binder.fvarId!) binder.binderInfo newDomain k - + + withLocalDecl (←copyVarName binder.fvarId!) binder.binderInfo newDomain k + copyVarName (oldName : FVarId) : MetaM Name := do let binderDecl ← getLocalDecl oldName mkFreshUserName binderDecl.userName @@ -209,13 +209,13 @@ def mkConstructor (ctx : Context) (i : Nat) (ctor : Name) : MetaM Constructor := let ctorInfo ← getConstInfoCtor ctor let name := ctor.updatePrefix ctx.belowNames[i] let type ← mkCtorType ctx i ctorInfo - return { + return { name := name type := type } -def mkInductiveType - (ctx : Context) - (i : Fin ctx.typeInfos.size) +def mkInductiveType + (ctx : Context) + (i : Fin ctx.typeInfos.size) (indVal : InductiveVal) : MetaM InductiveType := do return { name := ctx.belowNames[i] @@ -224,8 +224,8 @@ def mkInductiveType def mkBelowDecl (ctx : Context) : MetaM Declaration := do let lparams := ctx.typeInfos[0].levelParams - Declaration.inductDecl - lparams + Declaration.inductDecl + lparams (ctx.numParams + ctx.motives.size) (←ctx.typeInfos.mapIdxM $ mkInductiveType ctx).toList ctx.typeInfos[0].isUnsafe @@ -234,24 +234,24 @@ partial def backwardsChaining (m : MVarId) (depth : Nat) : MetaM Bool := do if depth = 0 then false else withMVarContext m do - let lctx ← getLCtx + let lctx ← getLCtx let mTy ← getMVarType m - lctx.anyM fun localDecl => - if localDecl.isAuxDecl then - false - else + lctx.anyM fun localDecl => + if localDecl.isAuxDecl then + false + else commitWhen do let (mvars, _, t) ← forallMetaTelescope localDecl.type - if ←isDefEq mTy t then + if ←isDefEq mTy t then assignExprMVar m (mkAppN localDecl.toExpr mvars) - mvars.allM fun v => + mvars.allM fun v => isExprMVarAssigned v.mvarId! <||> backwardsChaining v.mvarId! (depth - 1) else false - + partial def proveBrecOn (ctx : Context) (indVal : InductiveVal) (type : Expr) : MetaM Expr := do let main ← mkFreshExprSyntheticOpaqueMVar type let (m, vars) ← intros main.mvarId! - let [m] ← applyIH m vars | + let [m] ← applyIH m vars | throwError "applying the induction hypothesis should only return one goal" let ms ← induction m vars let ms ← applyCtors ms @@ -268,11 +268,11 @@ where return (m, ⟨params, motives, indices, witness, indHyps⟩) applyIH (m : MVarId) (vars : BrecOnVariables) : MetaM (List MVarId) := do - match ←vars.indHyps.findSomeM? + match ←vars.indHyps.findSomeM? (fun ih => do try some $ (←apply m $ mkFVar ih) catch ex => none) with | some goals => goals | none => throwError "cannot apply induction hypothesis: {MessageData.ofGoal m}" - + induction (m : MVarId) (vars : BrecOnVariables) : MetaM (List MVarId) := do let params := vars.params.map mkFVar let motives := vars.motives.map mkFVar @@ -282,17 +282,17 @@ where forallTelescope motive fun xs _ => do mkLambdaFVars xs $ mkAppN (mkConst ctx.belowNames[idx] levelParams) $ (params ++ motives ++ xs) let recursorInfo ← getConstInfo $ mkRecName indVal.name - let recLevels := - if recursorInfo.numLevelParams > levelParams.length - then levelZero::levelParams - else levelParams + let recLevels := + if recursorInfo.numLevelParams > levelParams.length + then levelZero::levelParams + else levelParams let recursor ← mkAppN (mkConst recursorInfo.name $ recLevels) $ params ++ motives - apply m recursor - + apply m recursor + applyCtors (ms : List MVarId) : MetaM $ List MVarId := do let mss ← ms.toArray.mapIdxM fun idx m => do - let m ← introNPRec m - (←getMVarType m).withApp fun below args => + let m ← introNPRec m + (←getMVarType m).withApp fun below args => withMVarContext m do args.back.withApp fun ctor ctorArgs => do let ctorName := ctor.constName!.updatePrefix below.constName! @@ -300,24 +300,24 @@ where let ctorInfo ← getConstInfoCtor ctorName let (mvars, _, t) ← forallMetaTelescope ctorInfo.type let ctor := mkAppN ctor mvars - apply m ctor + apply m ctor return mss.foldr List.append [] introNPRec (m : MVarId) : MetaM MVarId := do if (←getMVarType m).isForall then introNPRec (←intro1P m).2 else m - + closeGoal (vars : BrecOnVariables) (maxDepth : Nat) (m : MVarId) : MetaM Unit := do unless ←isExprMVarAssigned m do let m ← introNPRec m unless ←backwardsChaining m maxDepth do withMVarContext m do throwError "couldn't solve by backwards chaining ({``maxBackwardChainingDepth} = {maxDepth}): {MessageData.ofGoal m}" - + def mkBrecOnDecl (ctx : Context) (idx : Nat) : MetaM Declaration := do let type ← mkType let indVal := ctx.typeInfos[idx] let name := indVal.name ++ brecOnSuffix - Declaration.thmDecl { + Declaration.thmDecl { name := name levelParams := indVal.levelParams type := type @@ -331,22 +331,22 @@ where let motiveBinders ← ctx.motives.mapIdxM $ mkIH params motives withLocalDeclsD motiveBinders fun ys => do mkForallFVars (xs ++ ys) (mkAppN motives[idx] indices) - mkIH + mkIH (params : Array Expr) (motives : Array Expr) - (idx : Fin ctx.motives.size) + (idx : Fin ctx.motives.size) (motive : Name × Expr) : MetaM $ Name × (Array Expr → MetaM Expr) := do let name := if ctx.motives.size > 1 then mkFreshUserName s!"ih_{idx.val.succ}" else mkFreshUserName "ih" let ih ← instantiateForall motive.2 params - let mkDomain _ := + let mkDomain _ := forallTelescope ih fun ys t => do let levels := ctx.typeInfos[idx].levelParams.map mkLevelParam let args := params ++ motives ++ ys let premise := - mkAppN + mkAppN (mkConst ctx.belowNames[idx.val] levels) args let conclusion := mkAppN motives[idx] ys @@ -359,22 +359,22 @@ partial def getBelowIndices (ctorName : Name) : MetaM $ Array Nat := do let belowCtorInfo ← getConstInfoCtor (ctorName.updatePrefix $ ctorInfo.induct ++ `below) let belowInductInfo ← getConstInfoInduct belowCtorInfo.induct forallTelescope ctorInfo.type fun xs t => do - loop xs belowCtorInfo.type #[] 0 0 + loop xs belowCtorInfo.type #[] 0 0 -where - loop - (xs : Array Expr) - (rest : Expr) - (belowIndices : Array Nat) - (xIdx yIdx : Nat) : MetaM $ Array Nat := do +where + loop + (xs : Array Expr) + (rest : Expr) + (belowIndices : Array Nat) + (xIdx yIdx : Nat) : MetaM $ Array Nat := do if xIdx ≥ xs.size then belowIndices else let x := xs[xIdx] let xTy ← inferType x let yTy := rest.bindingDomain! - if ←isDefEq xTy yTy then + if ←isDefEq xTy yTy then let rest ← instantiateForall rest #[x] loop xs rest (belowIndices.push yIdx) (xIdx + 1) (yIdx + 1) - else + else forallBoundedTelescope rest (some 1) fun ys rest => loop xs rest belowIndices xIdx (yIdx + 1) @@ -389,33 +389,33 @@ private def belowType (motive : Expr) (xs : Array Expr) (idx : Nat) : MetaM $ Na /-- This function adds an additional `below` discriminant to a matcher application. It is used for modifying the patterns, such that the structural recursion can use the new `below` predicate instead of the original one and thus be used prove structural recursion. - + It takes as parameters: - matcherApp: a matcher application - belowMotive: the motive, that the `below` type should carry - below: an expression from the local context that is the `below` version of a predicate and can be used for structural recursion - idx: the index of the original predicate discriminant. - + It returns: - A matcher application as an expression - A side-effect for adding the matcher to the environment -/ partial def mkBelowMatcher - (matcherApp : MatcherApp) - (belowMotive : Expr) + (matcherApp : MatcherApp) + (belowMotive : Expr) (below : Expr) (idx : Nat) : MetaM $ Expr × MetaM Unit := do let mkMatcherInput ← getMkMatcherInputInContext matcherApp - let (indName, belowType, motive, matchType) ← + let (indName, belowType, motive, matchType) ← forallBoundedTelescope mkMatcherInput.matchType mkMatcherInput.numDiscrs fun xs t => do let (indName, belowType) ← belowType belowMotive xs idx - let matchType ← + let matchType ← withLocalDeclD (←mkFreshUserName `h_below) belowType fun h_below => do mkForallFVars (xs.push h_below) t let motive ← newMotive belowType xs (indName, belowType.replaceFVars xs matcherApp.discrs, motive, matchType) - let lhss ← mkMatcherInput.lhss.mapM $ addBelowPattern indName + let lhss ← mkMatcherInput.lhss.mapM $ addBelowPattern indName let alts ← mkMatcherInput.lhss.zip lhss |>.toArray.zip matcherApp.alts |>.mapIdxM fun idx ((oldLhs, lhs), alt) => do withExistingLocalDecls (oldLhs.fvarDecls ++ lhs.fvarDecls) do lambdaTelescope alt fun xs t => do @@ -427,8 +427,8 @@ partial def mkBelowMatcher | 0, n+1 => xs[1:] | _, _ => xs let t := t.replaceFVars xs[:oldFVars.size] fvars[:oldFVars.size] - trace[Meta.IndPredBelow.match] "xs = {xs}; oldFVars = {oldFVars.map (·.toExpr)}; fvars = {fvars}; new = {fvars[:oldFVars.size].toArray ++ xs[oldFVars.size:] ++ fvars[oldFVars.size:].toArray}" - let newAlt ← mkLambdaFVars (fvars[:oldFVars.size].toArray ++ xs[oldFVars.size:] ++ fvars[oldFVars.size:].toArray) t + trace[Meta.IndPredBelow.match] "xs = {xs}; oldFVars = {oldFVars.map (·.toExpr)}; fvars = {fvars}; new = {fvars[:oldFVars.size] ++ xs[oldFVars.size:] ++ fvars[oldFVars.size:].toArray}" + let newAlt ← mkLambdaFVars (fvars[:oldFVars.size] ++ xs[oldFVars.size:] ++ fvars[oldFVars.size:].toArray) t trace[Meta.IndPredBelow.match] "alt {idx}:\n{alt} ↦ {newAlt}" newAlt @@ -447,20 +447,20 @@ partial def mkBelowMatcher let newApp := mkAppN newApp alts (newApp, res.addMatcher) -where +where addBelowPattern (indName : Name) (lhs : AltLHS) : MetaM AltLHS := do withExistingLocalDecls lhs.fvarDecls do let patterns := lhs.patterns.toArray let originalPattern := patterns[idx] let (fVars, belowPattern) ← convertToBelow indName patterns[idx] withExistingLocalDecls fVars.toList do - let patterns := patterns.push belowPattern + let patterns := patterns.push belowPattern let patterns := patterns.set! idx (←toInaccessible originalPattern) { lhs with patterns := patterns.toList, fvarDecls := lhs.fvarDecls ++ fVars.toList } - + /-- this function changes the type of the pattern from the original type to the `below` version thereof. - Most of the cases don't apply. In order to change the type and the pattern to be type correct, we don't + Most of the cases don't apply. In order to change the type and the pattern to be type correct, we don't simply recursively change all occurrences, but rather, we recursively change occurences of the constructor. As such there are only a few cases: - the pattern is a constructor from the original type. Here we need to: @@ -471,20 +471,20 @@ where - it is an `as` pattern. Here the contstructor could be hidden inside of it. - it is a variable. Here you we need to introduce a fresh variable of a different type. -/ - convertToBelow (indName : Name) - (originalPattern : Pattern) : MetaM $ Array LocalDecl × Pattern := do + convertToBelow (indName : Name) + (originalPattern : Pattern) : MetaM $ Array LocalDecl × Pattern := do match originalPattern with - | Pattern.ctor ctorName us params fields => + | Pattern.ctor ctorName us params fields => let ctorInfo ← getConstInfoCtor ctorName - + let belowCtor ← getConstInfoCtor $ ctorName.updatePrefix $ ctorInfo.induct ++ `below let belowIndices ← IndPredBelow.getBelowIndices ctorName let belowIndices := belowIndices[ctorInfo.numParams:].toArray.map (· - belowCtor.numParams) -- belowFieldOpts starts off with an array of empty fields. -- We then go over pattern's fields and set the appropriate fields to values. - -- In general, there are fewer `fields` than `belowFieldOpts`, because the - -- `belowCtor` carries a `below`, a non-`below` and a `motive` version of each + -- In general, there are fewer `fields` than `belowFieldOpts`, because the + -- `belowCtor` carries a `below`, a non-`below` and a `motive` version of each -- field that occurs in a recursive application of the inductive predicate. -- `belowIndices` is a mapping from non-`below` to the `below` version of each field. let mut belowFieldOpts := mkArray belowCtor.numFields none @@ -494,32 +494,32 @@ where let belowParams := params.toArray.push belowMotive let belowCtorExpr := mkAppN (mkConst belowCtor.name us) belowParams - let (additionalFVars, belowFields) ← transformFields belowCtorExpr indName belowFieldOpts - + let (additionalFVars, belowFields) ← transformFields belowCtorExpr indName belowFieldOpts + withExistingLocalDecls additionalFVars.toList do let ctor := Pattern.ctor belowCtor.name us belowParams.toList belowFields.toList trace[Meta.IndPredBelow.match] "{originalPattern.toMessageData} ↦ {ctor.toMessageData}" - (additionalFVars, ctor) - | Pattern.as varId p => + (additionalFVars, ctor) + | Pattern.as varId p => let (additionalFVars, p) ← convertToBelow indName p (additionalFVars, Pattern.as varId p) - | Pattern.var varId => + | Pattern.var varId => let var := mkFVar varId (←inferType var).withApp fun ind args => do let (_, tgtType) ← belowType belowMotive #[var] 0 withLocalDeclD (←mkFreshUserName `h) tgtType fun h => do let localDecl ← getFVarLocalDecl h (#[localDecl], Pattern.var h.fvarId!) - | p => (#[], p) + | p => (#[], p) - transformFields belowCtor indName belowFieldOpts := + transformFields belowCtor indName belowFieldOpts := let rec loop - (belowCtor : Expr) + (belowCtor : Expr) (belowFieldOpts : Array $ Option Pattern) - (belowFields : Array Pattern) + (belowFields : Array Pattern) (additionalFVars : Array LocalDecl) : MetaM (Array LocalDecl × Array Pattern) := do if belowFields.size ≥ belowFieldOpts.size then (additionalFVars, belowFields) else - if let some belowField := belowFieldOpts[belowFields.size] then + if let some belowField := belowFieldOpts[belowFields.size] then let belowFieldExpr ← belowField.toExpr let belowCtor := mkApp belowCtor belowFieldExpr let patTy ← inferType belowFieldExpr @@ -529,54 +529,54 @@ where let (fvars, transformedField) ← convertToBelow indName belowField withExistingLocalDecls fvars.toList do let belowFieldOpts := belowFieldOpts.set! (belowFields.size + 1) transformedField - let belowField := - match belowField with - | Pattern.ctor .. => Pattern.inaccessible belowFieldExpr + let belowField := + match belowField with + | Pattern.ctor .. => Pattern.inaccessible belowFieldExpr | _ => belowField loop belowCtor belowFieldOpts (belowFields.push belowField) (additionalFVars ++ fvars) else - loop belowCtor belowFieldOpts (belowFields.push belowField) additionalFVars + loop belowCtor belowFieldOpts (belowFields.push belowField) additionalFVars else let ctorType ← inferType belowCtor withLocalDeclD (←mkFreshUserName `a) ctorType.bindingDomain! fun a => do let localDecl ← getFVarLocalDecl a - loop (mkApp belowCtor a) belowFieldOpts (belowFields.push $ Pattern.var a.fvarId!) (additionalFVars.push localDecl) + loop (mkApp belowCtor a) belowFieldOpts (belowFields.push $ Pattern.var a.fvarId!) (additionalFVars.push localDecl) loop belowCtor belowFieldOpts #[] #[] - - toInaccessible : Pattern → MetaM Pattern + + toInaccessible : Pattern → MetaM Pattern | Pattern.inaccessible p => Pattern.inaccessible p | Pattern.var v => Pattern.var v | p => do Pattern.inaccessible $ ←p.toExpr - newMotive (belowType : Expr) (ys : Array Expr) : MetaM Expr := + newMotive (belowType : Expr) (ys : Array Expr) : MetaM Expr := lambdaTelescope matcherApp.motive fun xs t => do let numDiscrs := matcherApp.discrs.size withLocalDeclD (←mkFreshUserName `h_below) (←belowType.replaceFVars ys xs) fun h_below => do let motive ← mkLambdaFVars (xs[:numDiscrs] ++ #[h_below] ++ xs[numDiscrs:]) t trace[Meta.IndPredBelow.match] "motive := {motive}" motive - + def findBelowIdx (xs : Array Expr) (motive : Expr) : MetaM $ Option (Expr × Nat) := do xs.findSomeM? fun x => do let xTy ← inferType x - xTy.withApp fun f args => + xTy.withApp fun f args => match f.constName?, xs.indexOf? x with | some name, some idx => do if ←isInductivePredicate name then let (_, belowTy) ← belowType motive xs idx let below ← mkFreshExprSyntheticOpaqueMVar belowTy - try + try trace[Meta.IndPredBelow.match] "{←Meta.ppGoal below.mvarId!}" if ←backwardsChaining below.mvarId! 10 then trace[Meta.IndPredBelow.match] "Found below term in the local context: {below}" if ←xs.anyM (isDefEq below) then none else (below, idx.val) - else + else trace[Meta.IndPredBelow.match] "could not find below term in the local context" none catch _ => none else none | _, _ => none - + def mkBelow (declName : Name) : MetaM Unit := do if (←isInductivePredicate declName) then let x ← getConstInfoInduct declName @@ -598,4 +598,4 @@ builtin_initialize registerTraceClass `Meta.IndPredBelow registerTraceClass `Meta.IndPredBelow.match -end Lean.Meta.IndPredBelow \ No newline at end of file +end Lean.Meta.IndPredBelow