Merge remote-tracking branch 'origin/master' into codef-3-deepThunk

Qpf/Macro/Data.lean

@@ -59,11 +59,6 @@ end
 -/
 open Elab.Term (TermElabM)
 
-
-
-
-
-
 def CtorView.declReplacePrefix (pref new_pref : Name) (ctor: CtorView) : CtorView :=
   let declName := ctor.declName.replacePrefix pref new_pref
   {
@@ -410,8 +405,6 @@ def isPolynomial (view : DataView) (F: Term) : CommandElabM (Option Term) := do
         trace[QPF] "{e.toMessageData}"
         return none
 
-
-
 /--
   Take either the fixpoint or cofixpoint of `base` to produce an `Internal` uncurried QPF,
   and define the desired type as the curried version of `Internal`

Qpf/Macro/Data/Constructors.lean

@@ -2,7 +2,7 @@ import Qpf.Macro.Data.Replace
 import Qpf.Macro.Data.RecForm
 import Qpf.Macro.Data.View
 
-open Lean Meta Elab Elab.Command 
+open Lean Meta Elab Elab.Command
 open PrettyPrinter (delab)
 
 namespace Data.Command
@@ -14,13 +14,17 @@ partial def countConstructorArgs : Syntax → Nat
   | Syntax.node _ ``Term.arrow #[_, _, tail]  =>  1 + (countConstructorArgs tail)
   | _                                         => 0
 
-
+/--
+  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.
+  The binders param allows for adding constant binders to an expression.
+-/
 def mkConstructorsWithNameAndType
     (view : DataView) (shape : Name)
-    (nameGen : CtorView → Ident) (argTy retTy : Term)
+    (nameGen : CtorView → Name) (argTy retTy : Term)
     (binders : TSyntaxArray ``Parser.Term.bracketedBinder)
-
-  := do
+    : 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
@@ -32,8 +36,6 @@ def mkConstructorsWithNameAndType
     let shapeCtor := mkIdent <| Name.replacePrefix ctor.declName view.declName shape
     trace[QPF] "shapeCtor = {shapeCtor}"
 
-
-
     let body ← if n_args = 0 then
         `($pointConstructor $shapeCtor)
       else
@@ -51,7 +53,7 @@ def mkConstructorsWithNameAndType
         name := `matchPattern
       }]
     }
-    let declId := nameGen ctor
+    let declId := mkIdent $ nameGen ctor
 
     let cmd ← `(
       $(quote modifiers):declModifiers
@@ -67,7 +69,7 @@ def mkConstructorsWithNameAndType
 -/
 def mkConstructors (view : DataView) (shape : Name) : CommandElabM Unit := do
   let explicit ← view.getExplicitExpectedType
-  let nameGen := (mkIdent <| ·.declName.replacePrefix (←getCurrNamespace) .anonymous)
+  let nameGen := (·.declName.replacePrefix (←getCurrNamespace) .anonymous)
 
   mkConstructorsWithNameAndType view shape nameGen explicit explicit #[]
 

Qpf/Macro/Data/Ind.lean

@@ -233,12 +233,12 @@ def genForCoData : CommandElabM Unit := do
 
   let corecType := view.getExpectedType
 
-  let base := view.shortDeclName ++ `Base |> mkIdent
+  let base := view.shortDeclName ++ `Base
 
   let corecDef : Command ← `(
     def $(view.shortDeclName ++ `corec |> mkIdent):ident
         { β }
-        (f : β → $(view.getExpectedTypeWithId base) β)
+        (f : β → $(view.getExpectedTypeWithName base) β)
         : β → $corecType
       := $(mkIdent ``MvQPF.Cofix.corec) f)
 
@@ -254,15 +254,17 @@ def genForCoData : CommandElabM Unit := do
   let idTyFunCurriedAux := mkIdent ``TypeFun.curriedAux
   let idRevArgs := mkIdent ``TypeFun.reverseArgs
 
-  let dtId := view.shortDeclName ++ `DeepThunk |> mkIdent
+  let dtName := view.shortDeclName ++ `DeepThunk
+  let dtId := mkIdent dtName
+
 
   let deepThunk ← `(command|
     abbrev $dtId:ident :=
       $idDeepThunk $(view.shortDeclName ++ `Base.Uncurried |> mkIdent))
 
   let tCurr := view.getExpectedType
   let tUncurr ← `($(view.shortDeclName ++ `Uncurried |> mkIdent) $vec)
-  let dtCurr ← `($(view.getExpectedTypeWithId dtId) ζ)
+  let dtCurr ← `($(view.getExpectedTypeWithName dtName) ζ)
   let dtUncurr ← `( $(``MvQPF.DeepThunk.Uncurried |> mkIdent)
     $(view.shortDeclName ++ `Base.Uncurried |> mkIdent)
     ($(mkIdent ``TypeVec.append1) $vec ζ))
@@ -362,7 +364,7 @@ def genForCoData : CommandElabM Unit := do
 
   dbg_trace shape
   Data.Command.mkConstructorsWithNameAndType view shape (fun ctor =>
-    (view.declName ++ `DeepThunk ++ (ctor.declName.replacePrefix view.declName .anonymous) |> mkIdent))
+    (view.declName ++ `DeepThunk ++ ctor.declName.replacePrefix view.declName .anonymous))
     (← `(ζ ⊕ ($dtCurr)))
     dtCurr
     (#[(← `(bb|{ ζ : Type }) : TSyntax ``bracketedBinder)])

Qpf/Macro/Data/View.lean

@@ -121,15 +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 -/
-def DataView.getExpectedTypeWithId (view : DataView) (id : Ident) : Term
-  := Syntax.mkApp id (
-    (Macro.getBinderIdents view.binders.getArgs false)
-  )  
+/--
+  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
-  := view.getExpectedTypeWithId (mkIdent view.shortDeclName)
+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