faet: finish deepThunk generation

Author: William Sørensen

Qpf/Macro/Data.lean

@@ -419,10 +419,11 @@ def isPolynomial (view : DataView) (F: Term) : CommandElabM (Option Term) := do
 -/
 def mkType (view : DataView) (base : Term × Term × Term) : CommandElabM Unit := do
   trace[QPF] "mkType"
-  let uncurriedIdent ← addSuffixToDeclIdent view.declId "Uncurried"
-  let baseIdent ← addSuffixToDeclIdent view.declId "Base"
+  let uncurriedIdent   ← addSuffixToDeclIdent view.declId "Uncurried"
+  let baseIdExt        ← addSuffixToDeclIdent view.declId "Base"
+  let baseIdent        ← addSuffixToDeclIdent baseIdExt "Uncurried"
   let baseFunctorIdent ← addSuffixToDeclIdent baseIdent "instMvFunctor"
-  let baseQPFIdent ← addSuffixToDeclIdent baseIdent "instQPF"
+  let baseQPFIdent     ← addSuffixToDeclIdent baseIdent "instQPF"
 
   let deadBinderNamedArgs ← view.deadBinderNames.mapM fun n =>
         `(namedArgument| ($n:ident := $n:term))
@@ -438,6 +439,9 @@ def mkType (view : DataView) (base : Term × Term × Term) : CommandElabM Unit :
     abbrev $baseIdent:ident $view.deadBinders:bracketedBinder* : TypeFun $(quote <| arity + 1) :=
       $base
 
+    abbrev $baseIdExt $view.deadBinders:bracketedBinder*
+      := TypeFun.curried $baseApplied
+
     instance $baseFunctorIdent:ident : MvFunctor ($baseApplied) := $functor
     instance $baseQPFIdent:ident : MvQPF ($baseApplied) := $q
 
@@ -484,9 +488,8 @@ def elabData : CommandElab := fun stx => do
   mkType view base
   mkConstructors view shape
 
-  if let .Data := view.command then
-    try genRecursors view
-    catch e => trace[QPF] (← e.toMessageData.toString)
+  try genRecursors view shape
+  catch e => trace[QPF] (← e.toMessageData.toString)
 
 
 end Data.Command

Qpf/Macro/Data/Constructors.lean

@@ -1,4 +1,5 @@
 import Qpf.Macro.Data.Replace
+import Qpf.Macro.Data.RecForm
 import Qpf.Macro.Data.View
 import Qpf.Macro.NameUtils
 
@@ -15,7 +16,12 @@ partial def countConstructorArgs : Syntax → Nat
   | _                                         => 0
 
 
-def mkConstructorsWithNameAndType (view : DataView) (shape : Name) (nameGen : CtorView → Ident) (ty : Term) := do
+def mkConstructorsWithNameAndType
+    (view : DataView) (shape : Name)
+    (nameGen : CtorView → Ident) (argTy retTy : Term)
+    (binders : TSyntaxArray ``Parser.Term.bracketedBinder)
+
+  := do
   for ctor in view.ctors do
     trace[QPF] "mkConstructors\n{ctor.declName} : {ctor.type?}"
     let n_args := (ctor.type?.map countConstructorArgs).getD 0
@@ -36,8 +42,12 @@ def mkConstructorsWithNameAndType (view : DataView) (shape : Name) (nameGen : Ct
         `(fun $args:ident* => $mk ($shapeCtor $args:ident*))
     let body ← body
 
-    let type : Term := TSyntax.mk <|
-      (ctor.type?.map fun type => Replace.replaceAllStx view.getExpectedType ty type).getD ty
+    let recType := view.getExpectedType
+    let forms := RecursionForm.extract ctor recType
+
+    let x := forms.map $ RecursionForm.replaceRec view.getExpectedType argTy
+    let type ← RecursionForm.toType retTy x
+
     let modifiers : Modifiers := {
       isNoncomputable := view.modifiers.isNoncomputable
       attrs := #[{
@@ -48,7 +58,7 @@ def mkConstructorsWithNameAndType (view : DataView) (shape : Name) (nameGen : Ct
 
     let cmd ← `(
       $(quote modifiers):declModifiers
-      def $declId:ident : $type := $body:term
+      def $declId:ident $binders*: $type := $body:term
     )
 
     trace[QPF] "mkConstructor.cmd = {cmd}"
@@ -62,7 +72,6 @@ def mkConstructors (view : DataView) (shape : Name) : CommandElabM Unit := do
   let explicit ← view.getExplicitExpectedType
   let nameGen := (mkIdent <| Name.stripPrefix2 (←getCurrNamespace) ·.declName)
 
-  mkConstructorsWithNameAndType view shape nameGen explicit
-
+  mkConstructorsWithNameAndType view shape nameGen explicit explicit #[]
 
 end Data.Command