From 91ecbb5b5ceaf72d472357c5cb3853e519e03c30 Mon Sep 17 00:00:00 2001 From: Daniel Fabian Date: Tue, 18 May 2021 04:43:19 +0000 Subject: [PATCH] feat: Add `withMkMatcherInput`. This is the inverse function to `mkMatcher`, i.e. a way to turn a matcher into an input. --- src/Lean/Meta/Match/Match.lean | 27 +++++++++++++++++++++++++++ tests/lean/run/match1.lean | 31 +++++++++++++++++++++++++++++++ 2 files changed, 58 insertions(+) diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean index 8de65a6c62..7325a00361 100644 --- a/src/Lean/Meta/Match/Match.lean +++ b/src/Lean/Meta/Match/Match.lean @@ -762,6 +762,33 @@ def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := if s.used.contains i then r else i::r pure { matcher := matcher, counterExamples := s.counterExamples, unusedAltIdxs := unusedAltIdxs.reverse } +def withMkMatcherInput (matcherName : Name) (k : MkMatcherInput → MetaM α) : MetaM α := do + let some matcherInfo ← getMatcherInfo? matcherName | throwError "not a matcher: {matcherName}" + let matcherConst ← getConstInfo matcherName + forallBoundedTelescope matcherConst.type (some matcherInfo.arity) fun xs t => do + let params := xs[:matcherInfo.numParams] + let motive := xs[matcherInfo.numParams] + let discrs := xs[matcherInfo.numParams + 1:matcherInfo.numParams + 1 + matcherInfo.numDiscrs] + let alts := xs[matcherInfo.numParams + 1 + matcherInfo.numDiscrs:] + let u := + if let some idx := matcherInfo.uElimPos? + then mkLevelParam matcherConst.levelParams.toArray[idx] + else levelZero + let matchType ← mkForallFVars discrs (mkConst ``PUnit [u]) + let lhss ← alts.toArray.mapIdxM fun idx t => do + let ty ← inferType t + forallTelescope ty fun xs body => do + let xs ← xs.filterM fun x => dependsOn body x.fvarId! + body.withApp fun f args => do + let ctx ← getLCtx + let localDecls := xs.map ctx.getFVar! + let patterns ← args.mapM Match.toPattern + return { + ref := Syntax.missing + fvarDecls := localDecls.toList + patterns := patterns.toList : Match.AltLHS } + k { matcherName, matchType, numDiscrs := matcherInfo.numDiscrs, lhss := lhss.toList } + end Match /- Auxiliary function for MatcherApp.addArg -/ diff --git a/tests/lean/run/match1.lean b/tests/lean/run/match1.lean index e84d9a3c14..3e56661be7 100644 --- a/tests/lean/run/match1.lean +++ b/tests/lean/run/match1.lean @@ -1,7 +1,26 @@ +import Lean + +def checkWithMkMatcherInput (matcher : Lean.Name) : Lean.MetaM Unit := + Lean.Meta.Match.withMkMatcherInput matcher fun input => do + let res ← Lean.Meta.Match.mkMatcher input + let origMatcher ← Lean.getConstInfo matcher + if not <| input.matcherName == matcher then + throwError "matcher name not reconstructed correctly: {matcher} ≟ {input.matcherName}" + + let lCtx ← Lean.getLCtx + let fvars ← Lean.collectFVars {} res.matcher + let closure ← Lean.Meta.Closure.mkLambda (fvars.fvarSet.toList.toArray.map lCtx.get!) res.matcher + + let origTy := origMatcher.value! + let newTy ← closure + if not <| ←Lean.Meta.isDefEq origTy newTy then + throwError "matcher {matcher} does not round-trip correctly:\n{origTy} ≟ {newTy}" + def f (xs : List Nat) : List Bool := xs.map fun | 0 => true | _ => false +#eval checkWithMkMatcherInput ``f.match_1 #eval f [1, 2, 0, 2] @@ -27,6 +46,7 @@ theorem ex3 {p q r : Prop} : p ∨ q → r → (q ∧ r) ∨ (p ∧ r) := by intro | Or.inl hp, h => { apply Or.inr; apply And.intro; assumption; assumption } | Or.inr hq, h => { apply Or.inl; exact ⟨hq, h⟩ } +#eval checkWithMkMatcherInput ``ex3.match_1 inductive C | mk₁ : Nat → C @@ -35,10 +55,12 @@ inductive C def C.x : C → Nat | C.mk₁ x => x | C.mk₂ x _ => x +#eval checkWithMkMatcherInput ``C.x.match_1 def head : {α : Type} → List α → Option α | _, a::as => some a | _, _ => none +#eval checkWithMkMatcherInput ``head.match_1 theorem ex4 : head [1, 2] = some 1 := rfl @@ -67,10 +89,12 @@ inductive Vec.{u} (α : Type u) : Nat → Type u def Vec.mapHead1 {α β δ} : {n : Nat} → Vec α n → Vec β n → (α → β → δ) → Option δ | _, nil, nil, f => none | _, cons a as, cons b bs, f => some (f a b) +#eval checkWithMkMatcherInput ``Vec.mapHead1.match_1 def Vec.mapHead2 {α β δ} : {n : Nat} → Vec α n → Vec β n → (α → β → δ) → Option δ | _, nil, nil, f => none | _, @cons _ n a as, cons b bs, f => some (f a b) +#eval checkWithMkMatcherInput ``Vec.mapHead2.match_1 def Vec.mapHead3 {α β δ} : {n : Nat} → Vec α n → Vec β n → (α → β → δ) → Option δ | _, nil, nil, f => none @@ -83,6 +107,7 @@ inductive Foo def Foo.z : Foo → Nat | mk₁ (z := z) .. => z | mk₂ (z := z) .. => z +#eval checkWithMkMatcherInput ``Foo.z.match_1 #eval (Foo.mk₁ 10 20 30 40).z @@ -92,6 +117,7 @@ rfl def Foo.addY? : Foo × Foo → Option Nat | (mk₁ (y := y₁) .., mk₁ (y := y₂) ..) => some (y₁ + y₂) | _ => none +#eval checkWithMkMatcherInput ``Foo.addY?.match_1 #eval Foo.addY? (Foo.mk₁ 1 2 3 4, Foo.mk₁ 10 20 30 40) @@ -106,6 +132,7 @@ partial def filter {α} (p : α → Bool) : {n : Nat} → Vec α n → Sigma fun | _, Vec.cons x xs => match p x, filter p xs with | true, ⟨_, ys⟩ => ⟨_, Vec.cons x ys⟩ | false, ys => ys +#eval checkWithMkMatcherInput ``filter.match_1 inductive Bla | ofNat (x : Nat) @@ -114,11 +141,13 @@ inductive Bla def Bla.optional? : Bla → Option Nat | ofNat x => some x | ofBool _ => none +#eval checkWithMkMatcherInput ``Bla.optional?.match_1 def Bla.isNat? (b : Bla) : Option { x : Nat // optional? b = some x } := match b.optional? with | some y => some ⟨y, rfl⟩ | none => none +#eval checkWithMkMatcherInput ``Bla.isNat?.match_1 def foo (b : Bla) : Option Nat := b.optional? theorem fooEq (b : Bla) : foo b = b.optional? := @@ -128,8 +157,10 @@ def Bla.isNat2? (b : Bla) : Option { x : Nat // optional? b = some x } := match h:foo b with | some y => some ⟨y, Eq.trans (fooEq b).symm h⟩ | none => none +#eval checkWithMkMatcherInput ``Bla.isNat2?.match_1 def foo2 (x : Nat) : Nat := match x, rfl : (y : Nat) → x = y → Nat with | 0, h => 0 | x+1, h => 1 +#eval checkWithMkMatcherInput ``foo2.match_1