From fd9be5e8ae3c2651ed271ae7ca47ac0fac3e86fb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 6 Aug 2020 15:37:00 -0700 Subject: [PATCH] feat: add `caseValues` tactic It is an auxiliary tactic for compiling pattern matching. --- src/Lean/Meta/EqnCompiler.lean | 1 + src/Lean/Meta/EqnCompiler/CaseValues.lean | 91 +++++++++++++++++++++++ src/Lean/Meta/EqnCompiler/DepElim.lean | 15 ++-- src/Lean/Meta/Tactic/Intro.lean | 3 +- src/Lean/Meta/Tactic/Subst.lean | 10 ++- src/Lean/Meta/Tactic/Util.lean | 4 + tests/lean/run/meta6.lean | 22 ++++++ tmp/eqns/matchVal.lean | 11 ++- 8 files changed, 142 insertions(+), 15 deletions(-) create mode 100644 src/Lean/Meta/EqnCompiler/CaseValues.lean diff --git a/src/Lean/Meta/EqnCompiler.lean b/src/Lean/Meta/EqnCompiler.lean index ae15f4417e..5efe05753b 100644 --- a/src/Lean/Meta/EqnCompiler.lean +++ b/src/Lean/Meta/EqnCompiler.lean @@ -5,6 +5,7 @@ Authors: Leonardo de Moura -/ import Lean.Meta.EqnCompiler.MatchPattern import Lean.Meta.EqnCompiler.DepElim +import Lean.Meta.EqnCompiler.CaseValues namespace Lean diff --git a/src/Lean/Meta/EqnCompiler/CaseValues.lean b/src/Lean/Meta/EqnCompiler/CaseValues.lean new file mode 100644 index 0000000000..5ad327ca91 --- /dev/null +++ b/src/Lean/Meta/EqnCompiler/CaseValues.lean @@ -0,0 +1,91 @@ +/- +Copyright (c) 2020 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +import Lean.Meta.Tactic.Subst +import Lean.Meta.Tactic.Clear + +namespace Lean +namespace Meta + +structure CaseValueSubgoal := +(mvarId : MVarId) +(newH : FVarId) +(subst : FVarSubst := {}) + +instance CaseValueSubgoal.inhabited : Inhabited CaseValueSubgoal := +⟨{ mvarId := arbitrary _, newH := arbitrary _ }⟩ + +/-- + Split goal `... |- C x` into two subgoals + `..., (h : x = value) |- C value` + `..., (h : x != value) |- C x` + The type of `x` must have decidable equality. -/ +def caseValueAux (mvarId : MVarId) (fvarId : FVarId) (value : Expr) (hName : Name := `h) (subst : FVarSubst := {}) + : MetaM (CaseValueSubgoal × CaseValueSubgoal) := +withMVarContext mvarId $ do + tag ← getMVarTag mvarId; + checkNotAssigned mvarId `caseValue; + target ← getMVarType mvarId; + xEqValue ← mkEq (mkFVar fvarId) value; + let xNeqValue := mkApp (mkConst `Not) xEqValue; + let thenTarget := Lean.mkForall hName BinderInfo.default xEqValue target; + let elseTarget := Lean.mkForall hName BinderInfo.default xNeqValue target; + thenMVar ← mkFreshExprSyntheticOpaqueMVar thenTarget tag; + elseMVar ← mkFreshExprSyntheticOpaqueMVar elseTarget tag; + val ← mkAppOptM `dite #[none, xEqValue, none, thenMVar, elseMVar]; + assignExprMVar mvarId val; + (elseH, elseMVarId) ← intro1 elseMVar.mvarId! false; + let elseSubgoal := { mvarId := elseMVarId, newH := elseH, subst := subst : CaseValueSubgoal }; + (thenH, thenMVarId) ← intro1 thenMVar.mvarId! false; + let symm := false; + let clearH := false; + (thenSubst, thenMVarId) ← substCore thenMVarId thenH symm subst clearH; + let thenSubgoal := { mvarId := thenMVarId, newH := (thenSubst.get thenH).fvarId!, subst := thenSubst : CaseValueSubgoal }; + pure (thenSubgoal, elseSubgoal) + +def caseValue (mvarId : MVarId) (fvarId : FVarId) (value : Expr) : MetaM (CaseValueSubgoal × CaseValueSubgoal) := do +s ← caseValueAux mvarId fvarId value; +appendTagSuffix s.1.mvarId `thenBranch; +appendTagSuffix s.2.mvarId `elseBranch; +pure s + +structure CaseValuesSubgoal := +(mvarId : MVarId) +(newHs : Array FVarId := #[]) +(subst : FVarSubst := {}) + +instance CaseValueSubgoals.inhabited : Inhabited CaseValuesSubgoal := +⟨{ mvarId := arbitrary _ }⟩ + +private def caseValuesAux (hNamePrefix : Name) (fvarId : FVarId) : Nat → MVarId → List Expr → Array FVarId → Array CaseValuesSubgoal → MetaM (Array CaseValuesSubgoal) +| i, mvarId, [], hs, subgoals => throwTacticEx `caseValues mvarId "list of values must not be empty" +| i, mvarId, v::vs, hs, subgoals => do + (thenSubgoal, elseSubgoal) ← caseValueAux mvarId fvarId v (hNamePrefix.appendIndexAfter i) {}; + appendTagSuffix thenSubgoal.mvarId ((`case).appendIndexAfter i); + thenMVarId ← hs.foldlM + (fun thenMVarId h => match thenSubgoal.subst.get h with + | Expr.fvar fvarId _ => tryClear thenMVarId fvarId + | _ => pure thenMVarId) + thenSubgoal.mvarId; + let subgoals := subgoals.push { mvarId := thenMVarId, newHs := #[thenSubgoal.newH], subst := thenSubgoal.subst }; + match vs with + | [] => do + appendTagSuffix elseSubgoal.mvarId ((`case).appendIndexAfter (i+1)); + pure $ subgoals.push { mvarId := elseSubgoal.mvarId, newHs := hs.push elseSubgoal.newH, subst := {} } + | _ => caseValuesAux (i+1) elseSubgoal.mvarId vs (hs.push elseSubgoal.newH) subgoals + +/-- + Split goal `... |- C x` into values.size + 1 subgoals + 1) `..., (h_1 : x = value[0]) |- C value[0]` + ... + n) `..., (h_n : x = value[n - 1]) |- C value[n - 1]` + n+1) `..., (h_1 : x != value[0]) ... (h_n : x != value[n-1]) |- C x` + where `n = values.size` + The type of `x` must have decidable equality. -/ +def caseValues (mvarId : MVarId) (fvarId : FVarId) (values : Array Expr) (hNamePrefix := `h) : MetaM (Array CaseValuesSubgoal) := +caseValuesAux hNamePrefix fvarId 1 mvarId values.toList #[] #[] + +end Meta +end Lean diff --git a/src/Lean/Meta/EqnCompiler/DepElim.lean b/src/Lean/Meta/EqnCompiler/DepElim.lean index 998958e1a1..9a5711c5b3 100644 --- a/src/Lean/Meta/EqnCompiler/DepElim.lean +++ b/src/Lean/Meta/EqnCompiler/DepElim.lean @@ -349,7 +349,7 @@ let (ok, hasVar, hasVal) := p.alts.foldl ok && hasVar && hasVal private def processNonVariable (process : Problem → State → MetaM State) (p : Problem) (s : State) : MetaM State := do -trace! `Meta.EqnCompiler.match ("process non variable"); +trace! `Meta.EqnCompiler.match ("non variable step"); match p.vars with | x :: xs => let alts := p.alts.map fun alt => match alt.patterns with @@ -369,7 +369,7 @@ match p.alts with pure { s with used := s.used.insert alt.idx } private def processVariable (process : Problem → State → MetaM State) (p : Problem) (s : State) : MetaM State := do -trace! `Meta.EqnCompiler.match ("process variable"); +trace! `Meta.EqnCompiler.match ("variable step"); match p.vars with | x :: xs => do alts ← p.alts.mapM fun alt => match alt.patterns with @@ -393,7 +393,7 @@ match alt.patterns with | _ => false private def processConstructor (process : Problem → State → MetaM State) (p : Problem) (s : State) : MetaM State := do -trace! `Meta.EqnCompiler.match ("process constructor"); +trace! `Meta.EqnCompiler.match ("constructor step"); match p.vars with | x :: xs => do subgoals ← cases p.goal.mvarId! x.fvarId!; @@ -479,7 +479,7 @@ matchConst env expectedType.getAppFn (fun _ => throwInductiveTypeExpected expect | _ => throwInductiveTypeExpected expectedType private def processComplete (process : Problem → State → MetaM State) (p : Problem) (s : State) : MetaM State := do -trace! `Meta.EqnCompiler.match ("process complete"); +trace! `Meta.EqnCompiler.match ("complete step"); withGoalOf p do env ← getEnv; newAlts ← p.alts.foldlM @@ -495,7 +495,12 @@ newAlts ← p.alts.foldlM process { p with alts := newAlts.reverse } s private def processValue (process : Problem → State → MetaM State) (p : Problem) (s : State) : MetaM State := do -throwOther "WIP" +trace! `Meta.EqnCompiler.match ("value step"); +match p.vars with +| [] => unreachable! +| x :: xs => do + + throwOther "WIP" private partial def process : Problem → State → MetaM State | p, s => withIncRecDepth do diff --git a/src/Lean/Meta/Tactic/Intro.lean b/src/Lean/Meta/Tactic/Intro.lean index 0459d4e498..992b486a9b 100644 --- a/src/Lean/Meta/Tactic/Intro.lean +++ b/src/Lean/Meta/Tactic/Intro.lean @@ -64,7 +64,8 @@ def mkAuxName (useUnusedNames : Bool) (lctx : LocalContext) (defaultName : Name) | n :: rest => (if n != "_" then n else if useUnusedNames then lctx.getUnusedName defaultName else defaultName, rest) def introN (mvarId : MVarId) (n : Nat) (givenNames : List Name := []) (useUnusedNames := true) : MetaM (Array FVarId × MVarId) := -introNCore mvarId n (mkAuxName useUnusedNames) givenNames +if n == 0 then pure (#[], mvarId) +else introNCore mvarId n (mkAuxName useUnusedNames) givenNames def intro (mvarId : MVarId) (name : Name) : MetaM (FVarId × MVarId) := do (fvarIds, mvarId) ← introN mvarId 1 [name]; diff --git a/src/Lean/Meta/Tactic/Subst.lean b/src/Lean/Meta/Tactic/Subst.lean index cb706dcb70..e99288a326 100644 --- a/src/Lean/Meta/Tactic/Subst.lean +++ b/src/Lean/Meta/Tactic/Subst.lean @@ -14,7 +14,7 @@ import Lean.Meta.Tactic.FVarSubst namespace Lean namespace Meta -def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst : FVarSubst := {}) : MetaM (FVarSubst × MVarId) := +def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst : FVarSubst := {}) (clearH := true) : MetaM (FVarSubst × MVarId) := withMVarContext mvarId $ do tag ← getMVarTag mvarId; checkNotAssigned mvarId `subst; @@ -57,8 +57,12 @@ withMVarContext mvarId $ do newVal ← if depElim then mkEqRec motive minor major else mkEqNDRec motive minor major; assignExprMVar mvarId newVal; let mvarId := newMVar.mvarId!; - mvarId ← clear mvarId hFVarId; - mvarId ← clear mvarId aFVarId; + mvarId ← + if clearH then do + mvarId ← clear mvarId hFVarId; + clear mvarId aFVarId + else + pure mvarId; (newFVars, mvarId) ← introN mvarId (vars.size - 2) [] false; fvarSubst ← newFVars.size.foldM (fun i (fvarSubst : FVarSubst) => diff --git a/src/Lean/Meta/Tactic/Util.lean b/src/Lean/Meta/Tactic/Util.lean index 0923c14cf7..778d141a91 100644 --- a/src/Lean/Meta/Tactic/Util.lean +++ b/src/Lean/Meta/Tactic/Util.lean @@ -18,6 +18,10 @@ pure mvarDecl.userName def setMVarTag (mvarId : MVarId) (tag : Name) : MetaM Unit := do modify $ fun s => { s with mctx := s.mctx.setMVarUserName mvarId tag } +def appendTagSuffix (mvarId : MVarId) (suffix : Name) : MetaM Unit := do +tag ← getMVarTag mvarId; +setMVarTag mvarId (tag ++ suffix) + def mkFreshExprSyntheticOpaqueMVar (type : Expr) (userName : Name := Name.anonymous) : MetaM Expr := mkFreshExprMVar type userName MetavarKind.syntheticOpaque diff --git a/tests/lean/run/meta6.lean b/tests/lean/run/meta6.lean index 16de8629f1..7ceb791603 100644 --- a/tests/lean/run/meta6.lean +++ b/tests/lean/run/meta6.lean @@ -57,3 +57,25 @@ pure () set_option pp.all true #eval tst3 + +inductive Vec.{u} (α : Type u) : Nat → Type u +| nil : Vec 0 +| cons {n : Nat} : α → Vec n → Vec (n+1) + +def tst4 : MetaM Unit := +withLocalDecl `x nat BinderInfo.default fun x => +withLocalDecl `y nat BinderInfo.default fun y => do +vType ← mkAppM `Vec #[nat, x]; +withLocalDecl `v vType BinderInfo.default fun v => do +m ← mkFreshExprSyntheticOpaqueMVar vType; +subgoals ← caseValues m.mvarId! x.fvarId! #[mkNatLit 2, mkNatLit 3, mkNatLit 5]; +subgoals.forM fun s => do { + print (MessageData.ofGoal s.mvarId); + assumption s.mvarId +}; +t ← instantiateMVars m; +print t; +Meta.check t; +pure () + +#eval tst4 diff --git a/tmp/eqns/matchVal.lean b/tmp/eqns/matchVal.lean index 2bf3e853a3..e4fdada066 100644 --- a/tmp/eqns/matchVal.lean +++ b/tmp/eqns/matchVal.lean @@ -11,12 +11,11 @@ def matchString (C : String → Sort v) (s : String) (h₂ : Unit → C "world") (h₃ : ∀ s, C s) : C s := -if h : s = "hello" then - @Eq.rec _ _ (fun x _ => C x) (h₁ ()) _ h.symm -else if h : s = "world" then - @Eq.rec _ _ (fun x _ => C x) (h₂ ()) _ h.symm -else - h₃ s +dite (s = "hello") + (fun h => @Eq.ndrec _ _ (fun x => C x) (h₁ ()) _ h.symm) + (fun _ => dite (s = "world") + (fun h => @Eq.ndrec _ _ (fun x => C x) (h₂ ()) _ h.symm) + (fun _ => h₃ s)) theorem matchString.Eq1 (C : String → Sort v) (h₁ : Unit → C "hello")