refactor: src/Lean/Meta/EqnCompiler ==> src/Lean/Meta/Match

src/Lean/Elab/Match.lean

@@ -3,8 +3,8 @@ 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.EqnCompiler.MatchPatternAttr
-import Lean.Meta.EqnCompiler.Match
+import Lean.Meta.Match.MatchPatternAttr
+import Lean.Meta.Match.Match
 import Lean.Elab.SyntheticMVars
 
 namespace Lean
@@ -198,7 +198,7 @@ match f with
   match env.find? fName with
   | some $ ConstantInfo.ctorInfo val => liftM $ getNumExplicitCtorParams val
   | some $ info =>
-    if EqnCompiler.hasMatchPatternAttribute env fName then pure 0
+    if hasMatchPatternAttribute env fName then pure 0
     else do processVar stx.getId mustBeCtor; pure 0
   | none => throwCtorExpected
 | _ => do processVar stx.getId mustBeCtor; pure 0

src/Lean/Meta.lean

@@ -19,6 +19,6 @@ import Lean.Meta.Tactic
 import Lean.Meta.KAbstract
 import Lean.Meta.RecursorInfo
 import Lean.Meta.GeneralizeTelescope
-import Lean.Meta.EqnCompiler
+import Lean.Meta.Match
 import Lean.Meta.ReduceEval
 import Lean.Meta.Closure

src/Lean/Meta/Match.lean

@@ -3,14 +3,14 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import Lean.Meta.EqnCompiler.MatchPatternAttr
-import Lean.Meta.EqnCompiler.Match
-import Lean.Meta.EqnCompiler.CaseValues
-import Lean.Meta.EqnCompiler.CaseArraySizes
+import Lean.Meta.Match.MatchPatternAttr
+import Lean.Meta.Match.Match
+import Lean.Meta.Match.CaseValues
+import Lean.Meta.Match.CaseArraySizes
 
 namespace Lean
 
 @[init] private def regTraceClasses : IO Unit :=
-registerTraceClass `Meta.EqnCompiler
+registerTraceClass `Meta.Match
 
 end Lean

src/Lean/Meta/Match/CaseArraySizes.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Meta.Tactic.Assert
-import Lean.Meta.EqnCompiler.CaseValues
+import Lean.Meta.Match.CaseValues
 
 namespace Lean
 namespace Meta

src/Lean/Meta/Match/Match.lean

@@ -8,9 +8,9 @@ import Lean.Meta.Check
 import Lean.Meta.Closure
 import Lean.Meta.Tactic.Cases
 import Lean.Meta.GeneralizeTelescope
-import Lean.Meta.EqnCompiler.MVarRenaming
-import Lean.Meta.EqnCompiler.CaseValues
-import Lean.Meta.EqnCompiler.CaseArraySizes
+import Lean.Meta.Match.MVarRenaming
+import Lean.Meta.Match.CaseValues
+import Lean.Meta.Match.CaseArraySizes
 
 namespace Lean
 namespace Meta
@@ -202,7 +202,7 @@ private partial def withAltsAux {α} (motive : Expr) : List AltLHS → List Alt
   let minorType := if minorType.isForall then minorType else mkThunkType minorType;
   let idx       := alts.length;
   let minorName := (`h).appendIndexAfter (idx+1);
-  trace! `Meta.EqnCompiler.matchDebug ("minor premise " ++ minorName ++ " : " ++ minorType);
+  trace! `Meta.Match.debug ("minor premise " ++ minorName ++ " : " ++ minorType);
   withLocalDeclD minorName minorType fun minor => do
     let rhs    := if xs.isEmpty then mkApp minor (mkConst `Unit.unit) else mkAppN minor xs;
     let minors := minors.push minor;
@@ -367,21 +367,21 @@ def occurs (fvarId : FVarId) (v : Expr) : Bool :=
 
 def assign (fvarId : FVarId) (v : Expr) : M Bool :=
 if occurs fvarId v then do
-  trace! `Meta.EqnCompiler.matchUnify ("assign occurs check failed, " ++ mkFVar fvarId ++ " := " ++ v);
+  trace! `Meta.Match.unify ("assign occurs check failed, " ++ mkFVar fvarId ++ " := " ++ v);
   pure false
 else do
   ctx ← read;
   condM (isAltVar fvarId)
     (do
-      trace! `Meta.EqnCompiler.matchUnify (mkFVar fvarId ++ " := " ++ v);
+      trace! `Meta.Match.unify (mkFVar fvarId ++ " := " ++ v);
       modify fun s => { s with fvarSubst := s.fvarSubst.insert fvarId v }; pure true)
     (do
-      trace! `Meta.EqnCompiler.matchUnify ("assign failed variable is not local, " ++ mkFVar fvarId ++ " := " ++ v);
+      trace! `Meta.Match.unify ("assign failed variable is not local, " ++ mkFVar fvarId ++ " := " ++ v);
       pure false)
 
 partial def unify : Expr → Expr → M Bool
 | a, b => do
-  trace! `Meta.EqnCompiler.matchUnify (a ++ " =?= " ++ b);
+  trace! `Meta.Match.unify (a ++ " =?= " ++ b);
   condM (isDefEq a b) (pure true) do
   a' ← expandIfVar a;
   b' ← expandIfVar b;
@@ -394,7 +394,7 @@ partial def unify : Expr → Expr → M Bool
     | a, Expr.fvar bFVarId _ => assign bFVarId a
     | Expr.app aFn aArg _, Expr.app bFn bArg _ => unify aFn bFn <&&> unify aArg bArg
     | _, _ => do
-      trace! `Meta.EqnCompiler.matchUnify ("unify failed @" ++ a ++ " =?= " ++ b);
+      trace! `Meta.Match.unify ("unify failed @" ++ a ++ " =?= " ++ b);
       pure false
 
 end Unify
@@ -450,7 +450,7 @@ match val? with
 | _        => pure false
 
 private def processConstructor (p : Problem) : MetaM (Array Problem) := do
-trace! `Meta.EqnCompiler.match ("constructor step");
+trace! `Meta.Match.match ("constructor step");
 env ← getEnv;
 match p.vars with
 | []      => unreachable!
@@ -493,7 +493,7 @@ match p.vars with
         | Pattern.ctor _ _ _ fields :: ps  => pure $ some { alt with patterns := fields ++ ps }
         | Pattern.var fvarId :: ps         => expandVarIntoCtor? { alt with patterns := ps } fvarId subgoal.ctorName
         | Pattern.inaccessible e :: ps     => do
-          trace! `Meta.EqnCompiler.match ("inaccessible in ctor step " ++ e);
+          trace! `Meta.Match.match ("inaccessible in ctor step " ++ e);
           e ← whnfD e;
           match e.constructorApp? env with
           | some (ctorVal, ctorArgs) => do
@@ -521,7 +521,7 @@ match alt.patterns with
 | _                  => false
 
 private def processValue (p : Problem) : MetaM (Array Problem) := do
-trace! `Meta.EqnCompiler.match ("value step");
+trace! `Meta.Match.match ("value step");
 match p.vars with
 | []      => unreachable!
 | x :: xs => do
@@ -577,7 +577,7 @@ withExistingLocalDecls alt.fvarDecls do
   expandVarIntoArrayLitAux alt fvarId arrayElemType fvarDecl.userName arraySize #[]
 
 private def processArrayLit (p : Problem) : MetaM (Array Problem) := do
-trace! `Meta.EqnCompiler.match ("array literal step");
+trace! `Meta.Match.match ("array literal step");
 match p.vars with
 | []      => unreachable!
 | x :: xs => do
@@ -616,10 +616,10 @@ let alts := p.alts.map fun alt => match alt.patterns with
 { p with alts := alts }
 
 private def traceStep (msg : String) : StateRefT State MetaM Unit :=
-liftM (trace! `Meta.EqnCompiler.match (msg ++ " step") : MetaM Unit)
+liftM (trace! `Meta.Match.match (msg ++ " step") : MetaM Unit)
 
 private def traceState (p : Problem) : MetaM Unit :=
-withGoalOf p (traceM `Meta.EqnCompiler.match p.toMessageData)
+withGoalOf p (traceM `Meta.Match.match p.toMessageData)
 
 private def throwNonSupported (p : Problem) : MetaM Unit := do
 msg ← p.toMessageData;
@@ -664,11 +664,11 @@ private partial def process : Problem → StateRefT State MetaM Unit
 
 def mkElim (elimName : Name) (motiveType : Expr) (numDiscrs : Nat) (lhss : List AltLHS) : MetaM ElimResult :=
 withLocalDeclD `motive motiveType fun motive => do
-trace! `Meta.EqnCompiler.matchDebug ("motiveType: " ++ motiveType);
+trace! `Meta.Match.debug ("motiveType: " ++ motiveType);
 forallBoundedTelescope motiveType numDiscrs fun majors _ => do
 checkNumPatterns majors lhss;
 let mvarType  := mkAppN motive majors;
-trace! `Meta.EqnCompiler.matchDebug ("target: " ++ mvarType);
+trace! `Meta.Match.debug ("target: " ++ mvarType);
 withAlts motive lhss fun alts minors => do
   mvar ← mkFreshExprMVar mvarType;
   let examples := majors.toList.map fun major => Example.var major.fvarId!;
@@ -676,10 +676,10 @@ withAlts motive lhss fun alts minors => do
   let args := #[motive] ++ majors ++ minors;
   type ← mkForallFVars args mvarType;
   val  ← mkLambdaFVars args mvar;
-  trace! `Meta.EqnCompiler.matchDebug ("eliminator value: " ++ val ++ "\ntype: " ++ type);
+  trace! `Meta.Match.debug ("eliminator value: " ++ val ++ "\ntype: " ++ type);
   elim ← mkAuxDefinition elimName type val;
   setInlineAttribute elimName;
-  trace! `Meta.EqnCompiler.matchDebug ("eliminator: " ++ elim);
+  trace! `Meta.Match.debug ("eliminator: " ++ elim);
   let unusedAltIdxs : List Nat := lhss.length.fold
     (fun i r => if s.used.contains i then r else i::r)
     [];
@@ -715,9 +715,9 @@ generalizeTelescope majors.toArray `_d fun majors => do
   mkElim elimName motiveType majors.size lhss
 
 @[init] private def regTraceClasses : IO Unit := do
-registerTraceClass `Meta.EqnCompiler.match;
-registerTraceClass `Meta.EqnCompiler.matchDebug;
-registerTraceClass `Meta.EqnCompiler.matchUnify;
+registerTraceClass `Meta.Match.match;
+registerTraceClass `Meta.Match.debug;
+registerTraceClass `Meta.Match.unify;
 pure ()
 
 end Match

src/Lean/Meta/Match/MatchPatternAttr.lean

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 import Lean.Attributes
 
 namespace Lean
-namespace EqnCompiler
 
 def mkMatchPatternAttr : IO TagAttribute :=
 registerTagAttribute `matchPattern "mark that a definition can be used in a pattern (remark: the dependent pattern matching compiler will unfold the definition)"
@@ -18,5 +17,4 @@ constant matchPatternAttr : TagAttribute := arbitrary _
 def hasMatchPatternAttribute (env : Environment) (n : Name) : Bool :=
 matchPatternAttr.hasTag env n
 
-end EqnCompiler
 end Lean

tests/lean/run/depElim1.lean

@@ -1,4 +1,4 @@
-import Lean.Meta.EqnCompiler.Match
+import Lean.Meta.Match
 
 open Lean
 open Lean.Meta
@@ -213,8 +213,8 @@ def ex6 (α : Type u) (n : Nat) (xs : Vec α n) :
 × LHS (forall (N : Nat) (XS : Vec α N), Pat (inaccessible N) × Pat XS) :=
 arbitrary _
 
-set_option trace.Meta.EqnCompiler.match true
-set_option trace.Meta.EqnCompiler.matchDebug true
+set_option trace.Meta.Match.match true
+set_option trace.Meta.Match.debug true
 
 #eval test `ex6 2 `elimTest6
 #print elimTest6
@@ -321,7 +321,7 @@ def ex14 (x y : Nat) :
 × LHS (forall (x y : Nat), Pat x × Pat y) :=
 arbitrary _
 
-set_option trace.Meta.EqnCompiler true
+set_option trace.Meta.Match true
 
 #eval test `ex14 2 `elimTest14
 #print elimTest14