refactor: thunk field-less alternatives of casesOnSameCtor (#11254)
This RP adds a `Unit` argument to `casesOnSameCtor` to make it behave moere similar to a matcher. Follow up in spirit to #11239.
This commit is contained in:
Joachim Breitner
GitHub
parent
52d05b6972
commit
75570f327f
6 changed files with 21 additions and 9 deletions
|
|
@ -164,6 +164,9 @@ def mkMatchNew (header : Header) (indVal : InductiveVal) (auxFunName : Name) : T
|
|||
rhs_empty := false
|
||||
else
|
||||
rhs ← `($a:ident == $b:ident && $rhs)
|
||||
if ctorArgs1.isEmpty then
|
||||
-- Unit thunking argument
|
||||
ctorArgs1 := ctorArgs1.push (← `(()))
|
||||
`(@fun $ctorArgs1.reverse:term* $ctorArgs2.reverse:term* =>$rhs:term)
|
||||
if indVal.numCtors == 1 then
|
||||
`( $(mkCIdent casesOnSameCtorName) $x1:term $x2:term rfl $alts:term* )
|
||||
|
|
|
|||
|
|
@ -140,6 +140,9 @@ def mkMatchNew (ctx : Context) (header : Header) (indVal : InductiveVal) : TermE
|
|||
let recField := indValNum.map (ctx.auxFunNames[·]!)
|
||||
let isProof ← isProp xType
|
||||
todo := todo.push (a, b, recField, isProof)
|
||||
if ctorArgs1.isEmpty then
|
||||
-- Unit thunking argument
|
||||
ctorArgs1 := ctorArgs1.push (← `(()))
|
||||
let rhs ← mkSameCtorRhs todo.toList
|
||||
`(@fun $ctorArgs1:term* $ctorArgs2:term* =>$rhs:term)
|
||||
if indVal.numCtors == 1 then
|
||||
|
|
|
|||
|
|
@ -118,6 +118,9 @@ def mkMatchNew (header : Header) (indVal : InductiveVal) : TermElabM Term := do
|
|||
else
|
||||
rhsCont := fun rhs => `(Ordering.then (compare $a $b) $rhs) >>= rhsCont
|
||||
let rhs ← rhsCont (← `(Ordering.eq))
|
||||
if ctorArgs1.isEmpty then
|
||||
-- Unit thunking argument
|
||||
ctorArgs1 := ctorArgs1.push (← `(()))
|
||||
`(@fun $ctorArgs1:term* $ctorArgs2:term* =>$rhs:term)
|
||||
if indVal.numCtors == 1 then
|
||||
`( $(mkCIdent casesOnSameCtorName) $x1:term $x2:term rfl $alts:term* )
|
||||
|
|
|
|||
|
|
@ -160,6 +160,7 @@ public def mkCasesOnSameCtor (declName : Name) (indName : Name) : MetaM Unit :=
|
|||
let ctorApp2 := mkAppN ctor fields2
|
||||
let e := mkAppN motive (is ++ #[ctorApp1, ctorApp2, (← mkEqRefl (mkNatLit i))])
|
||||
let e ← mkForallFVars zs12 e
|
||||
let e ← if zs12.isEmpty then mkArrow (mkConst ``Unit) e else pure e
|
||||
let name := match ctorName with
|
||||
| Name.str _ s => Name.mkSimple s
|
||||
| _ => Name.mkSimple s!"alt{i+1}"
|
||||
|
|
@ -190,8 +191,10 @@ public def mkCasesOnSameCtor (declName : Name) (indName : Name) : MetaM Unit :=
|
|||
let goal := alt.mvarId!
|
||||
let some (goal, _) ← Cases.unifyEqs? newRefls.size goal {}
|
||||
| throwError "unifyEqns? unexpectedly closed goal"
|
||||
let [] ← goal.apply alts[i]!
|
||||
| throwError "could not apply {alts[i]!} to close\n{goal}"
|
||||
let hyp := alts[i]!
|
||||
let hyp := if zs1.isEmpty && zs2.isEmpty then mkApp hyp (mkConst ``Unit.unit) else hyp
|
||||
let [] ← goal.apply hyp
|
||||
| throwError "could not apply {hyp} to close\n{goal}"
|
||||
mkLambdaFVars (zs1 ++ zs2) (← instantiateMVars alt)
|
||||
let casesOn2 := mkAppN casesOn2 alts'
|
||||
let casesOn2 := mkAppN casesOn2 newRefls
|
||||
|
|
|
|||
|
|
@ -65,7 +65,7 @@
|
|||
def instDecidableEqListTree.decEq_2 (x✝² : @B.ListTree✝) (x✝³ : @B.ListTree✝) : Decidable✝ (x✝² = x✝³) :=
|
||||
match decEq✝ (B.ListTree.ctorIdx✝ x✝²) (B.ListTree.ctorIdx✝ x✝³) with
|
||||
| .isTrue✝¹ h✝¹ =>
|
||||
B.ListTree.match_on_same_ctor✝ x✝² x✝³ h✝¹ (@fun => isTrue✝¹ rfl✝)
|
||||
B.ListTree.match_on_same_ctor✝ x✝² x✝³ h✝¹ (@fun () => isTrue✝¹ rfl✝)
|
||||
@fun a✝¹ a✝² b✝¹ b✝² =>
|
||||
let inst✝¹ := instDecidableEqListTree.decEq_1 @a✝¹ @b✝¹;
|
||||
if h✝² : @a✝¹ = @b✝¹ then by subst h✝²;
|
||||
|
|
@ -84,7 +84,7 @@
|
|||
def instDecidableEqFoo₁.decEq_1 (x✝ : @B.Foo₁✝) (x✝¹ : @B.Foo₁✝) : Decidable✝ (x✝ = x✝¹) :=
|
||||
match decEq✝ (B.Foo₁.ctorIdx✝ x✝) (B.Foo₁.ctorIdx✝ x✝¹) with
|
||||
| .isTrue✝ h✝ =>
|
||||
B.Foo₁.match_on_same_ctor✝ x✝ x✝¹ h✝ (@fun => isTrue✝ rfl✝)
|
||||
B.Foo₁.match_on_same_ctor✝ x✝ x✝¹ h✝ (@fun () => isTrue✝ rfl✝)
|
||||
@fun a✝ b✝ =>
|
||||
let inst✝ := instDecidableEqFoo₁.decEq_2 @a✝ @b✝;
|
||||
if h✝¹ : @a✝ = @b✝ then by subst h✝¹; exact isTrue✝¹ rfl✝¹
|
||||
|
|
|
|||
|
|
@ -27,7 +27,7 @@ info: Vec.match_on_same_ctor.het.{u_1, u} {α : Type u} {motive : {a : Nat} →
|
|||
/--
|
||||
info: Vec.match_on_same_ctor.{u_1, u} {α : Type u}
|
||||
{motive : {a : Nat} → (t t_1 : Vec α a) → t.ctorIdx = t_1.ctorIdx → Sort u_1} {a✝ : Nat} (t t✝ : Vec α a✝)
|
||||
(h : t.ctorIdx = t✝.ctorIdx) (nil : motive nil nil ⋯)
|
||||
(h : t.ctorIdx = t✝.ctorIdx) (nil : Unit → motive nil nil ⋯)
|
||||
(cons : (a : α) → {n : Nat} → (a_1 : Vec α n) → (a' : α) → (a'_1 : Vec α n) → motive (cons a a_1) (cons a' a'_1) ⋯) :
|
||||
motive t t✝ h
|
||||
-/
|
||||
|
|
@ -54,10 +54,10 @@ info: Vec.match_on_same_ctor.splitter.{u_1, u} {α : Type u}
|
|||
/--
|
||||
info: Vec.match_on_same_ctor.eq_2.{u_1, u} {α : Type u}
|
||||
{motive : {a : Nat} → (t t_1 : Vec α a) → t.ctorIdx = t_1.ctorIdx → Sort u_1} (a✝ : α) (n : Nat) (a✝¹ : Vec α n)
|
||||
(a'✝ : α) (a'✝¹ : Vec α n) (nil : motive nil nil ⋯)
|
||||
(a'✝ : α) (a'✝¹ : Vec α n) (nil : Unit → motive nil nil ⋯)
|
||||
(cons : (a : α) → {n : Nat} → (a_1 : Vec α n) → (a' : α) → (a'_1 : Vec α n) → motive (cons a a_1) (cons a' a'_1) ⋯) :
|
||||
(match n + 1, Vec.cons a✝ a✝¹, Vec.cons a'✝ a'✝¹ with
|
||||
| 0, Vec.nil, Vec.nil, ⋯ => nil
|
||||
| 0, Vec.nil, Vec.nil, ⋯ => nil ()
|
||||
| n + 1, Vec.cons a a_1, Vec.cons a' a'_1, ⋯ => cons a a_1 a' a'_1) =
|
||||
cons a✝ a✝¹ a'✝ a'✝¹
|
||||
-/
|
||||
|
|
@ -72,7 +72,7 @@ info: Vec.match_on_same_ctor.eq_2.{u_1, u} {α : Type u}
|
|||
|
||||
def decEqVec {α} {a} [DecidableEq α] (x : @Vec α a) (x_1 : @Vec α a) : Decidable (x = x_1) :=
|
||||
if h : Vec.ctorIdx x = Vec.ctorIdx x_1 then
|
||||
Vec.match_on_same_ctor x x_1 h (isTrue rfl)
|
||||
Vec.match_on_same_ctor x x_1 h (fun _ => isTrue rfl)
|
||||
@fun a_1 _ a_2 b b_1 =>
|
||||
if h_1 : @a_1 = @b then by
|
||||
subst h_1
|
||||
|
|
@ -137,7 +137,7 @@ run_meta mkCasesOnSameCtor `List.match_on_same_ctor ``List
|
|||
|
||||
/--
|
||||
info: List.match_on_same_ctor.{u_1, u} {α : Type u} {motive : (t t_1 : List α) → t.ctorIdx = t_1.ctorIdx → Sort u_1}
|
||||
(t t✝ : List α) (h : t.ctorIdx = t✝.ctorIdx) (nil : motive [] [] ⋯)
|
||||
(t t✝ : List α) (h : t.ctorIdx = t✝.ctorIdx) (nil : Unit → motive [] [] ⋯)
|
||||
(cons : (head : α) → (tail : List α) → (head' : α) → (tail' : List α) → motive (head :: tail) (head' :: tail') ⋯) :
|
||||
motive t t✝ h
|
||||
-/
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue