Merge branch 'codef-2' into codef-3-deepThunk

Qpf/Macro/Data.lean

@@ -6,7 +6,6 @@ import Qpf.Macro.Data.Replace
 import Qpf.Macro.Data.Count
 import Qpf.Macro.Data.View
 import Qpf.Macro.Data.Ind
-import Qpf.Macro.NameUtils
 import Qpf.Macro.Common
 import Qpf.Macro.Comp
 
@@ -66,7 +65,7 @@ open Elab.Term (TermElabM)
 
 
 def CtorView.declReplacePrefix (pref new_pref : Name) (ctor: CtorView) : CtorView :=
-  let declName := Name.replacePrefix2 pref new_pref ctor.declName
+  let declName := Name.replacePrefix ctor.declName pref new_pref 
   {
     declName,
     ref := ctor.ref
@@ -113,7 +112,7 @@ def mkHeadT (view : InductiveView) : CommandElabM Name := do
   }
   -- The head type is the same as the original type, but with all constructor arguments removed
   let ctors ← view.ctors.mapM fun ctor => do
-    let declName := Name.replacePrefix2 view.declName declName ctor.declName
+    let declName := ctor.declName.replacePrefix view.declName declName 
     pure {
       modifiers, declName,
       ref := ctor.ref
@@ -157,7 +156,7 @@ def mkChildT (view : InductiveView) (r : Replace) (headTName : Name) : CommandEl
   let target_type := Syntax.mkApp (mkIdent ``TypeVec) #[quote r.arity]
 
   let matchAlts ← view.ctors.mapM fun ctor => do
-    let head := mkIdent $ Name.replacePrefix2 view.declName headTName ctor.declName
+    let head := Lean.mkIdent (ctor.declName.replacePrefix view.declName headTName)
 
     let counts := countVarOccurences r ctor.type?
     let counts := counts.map fun n =>
@@ -221,7 +220,7 @@ def mkQpf (shapeView : InductiveView) (ctorArgs : Array CtorArgs) (headT P : Ide
   let boxBody ← ctors.mapM fun (ctor, args) => do
     let argsId  := args.args.map mkIdent
     let alt     := mkIdent ctor.declName
-    let headAlt := mkIdent $ Name.replacePrefix2 shapeView.declName headT.getId ctor.declName
+    let headAlt := mkIdent $ ctor.declName.replacePrefix shapeView.declName headT.getId 
 
     `(matchAltExpr| | $alt:ident $argsId:ident* => ⟨$headAlt:ident, fun i => match i with
         $(
@@ -258,7 +257,7 @@ def mkQpf (shapeView : InductiveView) (ctorArgs : Array CtorArgs) (headT P : Ide
   let unbox_child := mkIdent <|<- Elab.Term.mkFreshBinderName;
   let unboxBody ← ctors.mapM fun (ctor, args) => do
     let alt     := mkIdent ctor.declName
-    let headAlt := mkIdent $ Name.replacePrefix2 shapeView.declName headT.getId ctor.declName
+    let headAlt := mkIdent $ ctor.declName.replacePrefix shapeView.declName headT.getId
 
     let args : Array Term ← args.args.mapM fun arg => do
       -- find the pair `(i, j)` such that the argument is the `j`-th occurence of the `i`-th type

Qpf/Macro/Data/Constructors.lean

@@ -1,7 +1,6 @@
 import Qpf.Macro.Data.Replace
 import Qpf.Macro.Data.RecForm
 import Qpf.Macro.Data.View
-import Qpf.Macro.NameUtils
 
 open Lean Meta Elab Elab.Command 
 open PrettyPrinter (delab)
@@ -31,7 +30,7 @@ def mkConstructorsWithNameAndType
     let args := args.toArray
 
     let mk := mkIdent ((DataCommand.fixOrCofix view.command).getId ++ `mk)
-    let shapeCtor := mkIdent <| Name.replacePrefix2 view.declName shape ctor.declName
+    let shapeCtor := mkIdent <| Name.replacePrefix ctor.declName view.declName shape
     trace[QPF] "shapeCtor = {shapeCtor}"
 
 
@@ -70,7 +69,7 @@ def mkConstructorsWithNameAndType
 -/
 def mkConstructors (view : DataView) (shape : Name) : CommandElabM Unit := do
   let explicit ← view.getExplicitExpectedType
-  let nameGen := (mkIdent <| Name.stripPrefix2 (←getCurrNamespace) ·.declName)
+  let nameGen := (mkIdent <| ·.declName.replacePrefix (←getCurrNamespace) .anonymous)
 
   mkConstructorsWithNameAndType view shape nameGen explicit explicit #[]
 

Qpf/Macro/Data/Ind.lean

@@ -362,7 +362,7 @@ def genForCoData : CommandElabM Unit := do
 
   dbg_trace shape
   Data.Command.mkConstructorsWithNameAndType view shape (fun ctor =>
-    (view.declName ++ `DeepThunk ++ (Name.stripPrefix2 view.declName ctor.declName) |> mkIdent))
+    (view.declName ++ `DeepThunk ++ (ctor.declName.replacePrefix view.declName .anonymous) |> mkIdent))
     (← `(ζ ⊕ ($dtCurr)))
     dtCurr
     (#[(← `(bb|{ ζ : Type }) : TSyntax ``bracketedBinder)])