sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

WIP

Browse Source
This commit is contained in:
Sebastian Graf
2026-03-12 10:03:27 +00:00
parent 8bed0ff972
commit ea0a4ea329
1 changed files with 18 additions and 18 deletions
Download Patch File Download Diff File Expand all files Collapse all files

36
src/Lean/Elab/Tactic/Do/VCGen/Split.lean
View File

@@ -61,10 +61,10 @@ def expr : SplitInfo → Expr
Introduces fvars for all varying parts of a `SplitInfo` and provides the abstract Introduces fvars for all varying parts of a `SplitInfo` and provides the abstract
`SplitInfo` and fvars to the continuation. `SplitInfo` and fvars to the continuation.
For `ite`/`dite`, introduces `c : Prop`, `dec : Decidable c`, `t : mα` (or `t : c → mα`), For `ite`/`dite`, introduces `c : Prop`, `dec : Decidable c`, `t : resTy` (or `t : c → resTy`),
`e : mα` (or `e : ¬c → mα`). `e : resTy` (or `e : ¬c → resTy`).
For `matcher`, introduces discriminant fvars and alternative fvars, builds a non-dependent For `matcher`, introduces discriminant fvars and alternative fvars, builds a non-dependent
motive `fun _ ... _ => mα`, and adjusts matcher universe levels. motive `fun _ ... _ => resTy`, and adjusts matcher universe levels.
The abstract `SplitInfo` satisfies `abstractInfo.toExpr = abstractProgram`. The abstract `SplitInfo` satisfies `abstractInfo.toExpr = abstractProgram`.
@@ -73,39 +73,39 @@ lambda alts (e.g. for `splitWith`/`matcherApp.transform`) should patch them back
`{ abstractMatcherApp with alts := origMatcherApp.alts }`. `{ abstractMatcherApp with alts := origMatcherApp.alts }`.
-/ -/
def withAbstract {n} {α} [MonadLiftT MetaM n] [MonadControlT MetaM n] [Monad n] [Inhabited α] def withAbstract {n} {α} [MonadLiftT MetaM n] [MonadControlT MetaM n] [Monad n] [Inhabited α]
(info : SplitInfo) (mα : Expr) (info : SplitInfo) (resTy : Expr)
(k : (abstractInfo : SplitInfo) → (splitFVars : Array Expr) → n α) : n α := (k : (abstractInfo : SplitInfo) → (splitFVars : Array Expr) → n α) : n α :=
match info with match info with
| .ite _ => | .ite _ =>
withLocalDeclD `c (mkSort 0) fun c => withLocalDeclD `c (mkSort 0) fun c =>
withLocalDeclD `dec (mkApp (mkConst ``Decidable) c) fun dec => withLocalDeclD `dec (mkApp (mkConst ``Decidable) c) fun dec =>
withLocalDeclD `t mα fun t => withLocalDeclD `t resTy fun t =>
withLocalDeclD `e mα fun e => do withLocalDeclD `e resTy fun e => do
let u ← liftMetaM <| getLevel mα let u ← liftMetaM <| getLevel resTy
k (.ite <| mkApp5 (mkConst ``_root_.ite [u]) mα c dec t e) #[c, dec, t, e] k (.ite <| mkApp5 (mkConst ``_root_.ite [u]) resTy c dec t e) #[c, dec, t, e]
| .dite _ => | .dite _ =>
withLocalDeclD `c (mkSort 0) fun c => withLocalDeclD `c (mkSort 0) fun c =>
withLocalDeclD `dec (mkApp (mkConst ``Decidable) c) fun dec => do withLocalDeclD `dec (mkApp (mkConst ``Decidable) c) fun dec => do
let tTy ← liftMetaM <| mkArrow c mα let tTy ← liftMetaM <| mkArrow c resTy
let eTy ← liftMetaM <| mkArrow (mkNot c) mα let eTy ← liftMetaM <| mkArrow (mkNot c) resTy
withLocalDeclD `t tTy fun t => withLocalDeclD `t tTy fun t =>
withLocalDeclD `e eTy fun e => do withLocalDeclD `e eTy fun e => do
let u ← liftMetaM <| getLevel mα let u ← liftMetaM <| getLevel resTy
k (.dite <| mkApp5 (mkConst ``_root_.dite [u]) mα c dec t e) #[c, dec, t, e] k (.dite <| mkApp5 (mkConst ``_root_.dite [u]) resTy c dec t e) #[c, dec, t, e]
| .matcher matcherApp => do | .matcher matcherApp => do
let discrNamesTypes ← matcherApp.discrs.mapIdxM fun i discr => do let discrNamesTypes ← matcherApp.discrs.mapIdxM fun i discr => do
return ((`discr).appendIndexAfter (i+1), ← liftMetaM <| inferType discr) return ((`discr).appendIndexAfter (i+1), ← liftMetaM <| inferType discr)
withLocalDeclsDND discrNamesTypes fun discrs => do withLocalDeclsDND discrNamesTypes fun discrs => do
-- Non-dependent motive: fun _ ... _ => mα -- Non-dependent motive: fun _ ... _ => resTy
let motive ← liftMetaM <| lambdaTelescope matcherApp.motive fun motiveArgs _ => let motive ← liftMetaM <| lambdaTelescope matcherApp.motive fun motiveArgs _ =>
mkLambdaFVars motiveArgs mα mkLambdaFVars motiveArgs resTy
-- The matcher's universe levels include a `uElimPos` slot for the elimination target level. -- The matcher's universe levels include a `uElimPos` slot for the elimination target level.
-- Our abstract motive `fun _ ... _ => mα` may target a different level than the original -- Our abstract motive `fun _ ... _ => resTy` may target a different level than the original
-- dependent motive, so we update `matcherLevels[uElimPos]` to `getLevel mα`. -- dependent motive, so we update `matcherLevels[uElimPos]` to `getLevel resTy`.
let matcherLevels ← match matcherApp.uElimPos? with let matcherLevels ← match matcherApp.uElimPos? with
| none => pure matcherApp.matcherLevels | none => pure matcherApp.matcherLevels
| some pos => do | some pos => do
let uElim ← liftMetaM <| getLevel mα let uElim ← liftMetaM <| getLevel resTy
pure <| matcherApp.matcherLevels.set! pos uElim pure <| matcherApp.matcherLevels.set! pos uElim
-- Build partial application to infer alt types -- Build partial application to infer alt types
let matcherPartial := mkAppN (mkConst matcherApp.matcherName matcherLevels.toList) matcherApp.params let matcherPartial := mkAppN (mkConst matcherApp.matcherName matcherLevels.toList) matcherApp.params
@@ -119,7 +119,7 @@ def withAbstract {n} {α} [MonadLiftT MetaM n] [MonadControlT MetaM n] [Monad n]
matcherLevels := matcherLevels matcherLevels := matcherLevels
discrs := discrs discrs := discrs
motive := motive motive := motive
alts := alts alts := alts -- (← liftMetaM <| alts.mapM etaExpand)
remaining := #[] remaining := #[]
} }
k (.matcher abstractMatcherApp) (discrs ++ alts) k (.matcher abstractMatcherApp) (discrs ++ alts)