Generalize utility functions previously used for a single purpose

Qpf/Macro/Data/Constructors.lean

@@ -1,7 +1,7 @@
 import Qpf.Macro.Data.Replace
 import Qpf.Macro.Data.View
 
-open Lean Meta Elab.Command
+open Lean Meta Elab Elab.Command
 open PrettyPrinter (delab)
 
 namespace Data.Command
@@ -13,11 +13,13 @@ partial def countConstructorArgs : Syntax → Nat
   | Syntax.node _ ``Term.arrow #[_, _, tail]  =>  1 + (countConstructorArgs tail)
   | _                                         => 0
 
-open Elab
 /--
-  Add convenient constructor functions to the environment
+  Add definitions for constructors
+  that are generic across two input types shape and name.
+  Additionally we allow the user to control how names are generated.
 -/
-def mkConstructors (view : DataView) (shape : Name) : CommandElabM Unit := do
+def mkConstructorsWithNameAndType (view : DataView) (shape : Name)
+    (nameGen : CtorView → Name) (ty : Term) : CommandElabM Unit := do
   for ctor in view.ctors do
     trace[QPF] "mkConstructors\n{ctor.declName} : {ctor.type?}"
     let n_args := (ctor.type?.map countConstructorArgs).getD 0
@@ -34,18 +36,15 @@ def mkConstructors (view : DataView) (shape : Name) : CommandElabM Unit := do
       else
         `(fun $args:ident* => $pointConstructor ($shapeCtor $args:ident*))
 
-    let explicit ← view.getExplicitExpectedType
     let type : Term := TSyntax.mk <|
-      (ctor.type?.map fun type =>
-        Replace.replaceAllStx view.getExpectedType explicit type
-      ).getD explicit
+      (ctor.type?.map fun type => Replace.replaceAllStx view.getExpectedType ty type).getD ty
     let modifiers : Modifiers := {
       isNoncomputable := view.modifiers.isNoncomputable
       attrs := #[{
         name := `matchPattern
       }]
     }
-    let declId := mkIdent <| ctor.declName.replacePrefix (←getCurrNamespace) .anonymous
+    let declId := mkIdent $ nameGen ctor
 
     let cmd ← `(
       $(quote modifiers):declModifiers
@@ -56,4 +55,13 @@ def mkConstructors (view : DataView) (shape : Name) : CommandElabM Unit := do
     elabCommand cmd
   return ()
 
+/--
+  Add convenient constructor functions to the environment
+-/
+def mkConstructors (view : DataView) (shape : Name) : CommandElabM Unit := do
+  let explicit ← view.getExplicitExpectedType
+  let nameGen := (·.declName.replacePrefix (←getCurrNamespace) .anonymous)
+
+  mkConstructorsWithNameAndType view shape nameGen explicit
+
 end Data.Command

Qpf/Macro/Data/View.lean

@@ -121,11 +121,17 @@ def DataView.addDeclNameSuffix (view : DataView) (suffix : String) : DataView
       { view with declName, declId, shortDeclName }
 
 
+/--
+  Returns the fully applied form of the type to be defined.
+  The `name` parameter allows the user to control what the const at the bottom of the type is.
+  This lets the user get types that have the same parameters such as the DeepThunk types.
+-/
+def DataView.getExpectedTypeWithName (view : DataView) (name : Name) : Term :=
+  Macro.getBinderIdents view.binders.getArgs false |> Syntax.mkApp (mkIdent name)
+
 /-- Returns the fully applied form of the type to be defined -/
-def DataView.getExpectedType (view : DataView) : Term
-  := Syntax.mkApp (mkIdent view.shortDeclName) (
-    (Macro.getBinderIdents view.binders.getArgs false)
-  )  
+def DataView.getExpectedType (view : DataView) : Term :=
+  view.getExpectedTypeWithName view.shortDeclName
 
 /-- Returns the fully applied, explicit (`@`) form of the type to be defined -/
 def DataView.getExplicitExpectedType (view : DataView) : CommandElabM Term