From 563190b9e98e8947ba5db0e20f1c0aed11c31f9d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?William=20S=C3=B8rensen?= Date: Thu, 25 Jul 2024 15:40:30 +0100 Subject: [PATCH] faet: finish deepThunk generation --- Qpf/Macro/Data.lean | 15 +- Qpf/Macro/Data/Constructors.lean | 21 +- Qpf/Macro/Data/Ind.lean | 227 ++++++++++++++---- Qpf/Macro/Data/RecForm.lean | 66 +++++ .../Multivariate/Constructions/DeepThunk.lean | 97 ++++++++ 5 files changed, 361 insertions(+), 65 deletions(-) create mode 100644 Qpf/Macro/Data/RecForm.lean create mode 100644 Qpf/Qpf/Multivariate/Constructions/DeepThunk.lean diff --git a/Qpf/Macro/Data.lean b/Qpf/Macro/Data.lean index a90f705..fa1a9ca 100644 --- a/Qpf/Macro/Data.lean +++ b/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 diff --git a/Qpf/Macro/Data/Constructors.lean b/Qpf/Macro/Data/Constructors.lean index 9ef1104..c97d5fd 100644 --- a/Qpf/Macro/Data/Constructors.lean +++ b/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 diff --git a/Qpf/Macro/Data/Ind.lean b/Qpf/Macro/Data/Ind.lean index a052154..38ecae5 100644 --- a/Qpf/Macro/Data/Ind.lean +++ b/Qpf/Macro/Data/Ind.lean @@ -1,36 +1,21 @@ +import Mathlib.Data.QPF.Multivariate.Constructions.Fix +import Mathlib.Data.QPF.Multivariate.Constructions.Cofix + +import Qpf.Qpf.Multivariate.Constructions.DeepThunk +import Qpf.Macro.Data.Constructors +import Qpf.Macro.Data.RecForm import Qpf.Macro.Data.View import Qpf.Macro.Common -import Mathlib.Data.QPF.Multivariate.Constructions.Fix -import Mathlib.Tactic.ExtractGoal +import Qpf.Util.Vec open Lean.Parser (Parser) open Lean Meta Elab.Command Elab.Term Parser.Term open Lean.Parser.Tactic (inductionAlt) -/-- - The recursive form encodes how a function argument is recursive. - - Examples ty R α: - α → R α → List (R α) → R α - [nonRec, directRec, composed ] --/ -inductive RecursionForm := - | nonRec (stx: Term) - | directRec - -- | composed -- Not supported yet -deriving Repr, BEq - -partial def getArgTypes (v : Term) : List Term := match v.raw with - | .node _ ``arrow #[arg, _, deeper] => - ⟨arg⟩ :: getArgTypes ⟨deeper⟩ - | rest => [⟨rest⟩] def flattenForArg (n : Name) := Name.str .anonymous $ n.toStringWithSep "_" true -def containsStx (top : Term) (search : Term) : Bool := - (top.raw.find? (· == search)).isSome - /-- Both `bracketedBinder` and `matchAlts` have optional arguments, which cause them to not by recognized as parsers in quotation syntax (that is, ``` `(bracketedBinder| ...) ``` does not work). @@ -44,32 +29,9 @@ we can safely coerce syntax of these categories -/ instance : Coe (TSyntax ``bb) (TSyntax ``bracketedBinder) where coe x := ⟨x.raw⟩ instance : Coe (TSyntax ``matchAltExprs) (TSyntax ``matchAlts) where coe x := ⟨x.raw⟩ -/-- When we want to operate on patterns the names we need must start with shape. -This is done as if theres a constructor called `mk` dot notation breaks. -/ -def addShapeToName : Name → Name - | .anonymous => .str .anonymous "Shape" - | .str a b => .str (addShapeToName a) b - | .num a b => .num (addShapeToName a) b - section variable {m} [Monad m] [MonadQuotation m] [MonadError m] [MonadTrace m] [AddMessageContext m] -/-- Extract takes a constructor and extracts its recursive forms. - -This function assumes the pre-processor has run -It also assumes you don't have polymorphic recursive types such as -data Ql α | nil | l : α → Ql Bool → Ql α -/ -def extract (topName : Name) (view : CtorView) (rec_type : Term) : m $ Name × List RecursionForm := - (view.declName.replacePrefix topName .anonymous , ·) <$> (do - let some type := view.type? | pure [] - let type_ls := (getArgTypes ⟨type⟩).dropLast - - type_ls.mapM fun v => - if v == rec_type then pure .directRec - else if containsStx v rec_type then - throwErrorAt v.raw "Cannot handle composed recursive types" - else pure $ .nonRec v) - /-- Generate the binders for the different recursors -/ def mkRecursorBinder (rec_type : Term) (name : Name) @@ -87,6 +49,7 @@ def mkRecursorBinder let ty ← form.foldlM (fun acc => (match · with | ⟨.nonRec x, name⟩ => `(($name : $x) → $acc) | ⟨.directRec, name⟩ => `(($name : $rec_type) → $acc) + | ⟨.composed x, _⟩ => throwErrorAt x "Cannot handle recursive forms" )) out `(bb | ($(mkIdent $ flattenForArg name) : $ty)) @@ -111,7 +74,7 @@ def seq (f : TSyntax kx → TSyntax kx → m (TSyntax kx)) : List (TSyntax kx) def generateIndBody (ctors : Array (Name × List RecursionForm)) (includeMotive : Bool) : m $ TSyntax ``matchAlts := do let deeper: (TSyntaxArray ``matchAlt) ← ctors.mapM fun ⟨outerCase, form⟩ => do let callName := mkIdent $ flattenForArg outerCase - let outerCaseId := mkIdent $ addShapeToName outerCase + let outerCaseId := mkIdent $ `Shape ++ outerCase let rec_count := form.count .directRec let names ← listToEqLenNames form @@ -165,7 +128,7 @@ def generateIndBody (ctors : Array (Name × List RecursionForm)) (includeMotive def generateRecBody (ctors : Array (Name × List RecursionForm)) (includeMotive : Bool) : m $ TSyntax ``matchAlts := do let deeper: (TSyntaxArray ``matchAlt) ← ctors.mapM fun ⟨outerCase, form⟩ => do let callName := mkIdent $ flattenForArg outerCase - let outerCaseId := mkIdent $ addShapeToName outerCase + let outerCaseId := mkIdent $ `Shape ++ outerCase let names ← listToEqLenNames form let names := names.zip form.toArray @@ -174,6 +137,7 @@ def generateRecBody (ctors : Array (Name × List RecursionForm)) (includeMotive match f with | .directRec => `(⟨_, $nm⟩) | .nonRec _ => `(_) + | .composed _ => throwError "Cannot handle composed" let nonMotiveArgs ← names.mapM fun _ => `(_) let motiveArgs ← if includeMotive then @@ -181,6 +145,7 @@ def generateRecBody (ctors : Array (Name × List RecursionForm)) (includeMotive match f with | .directRec => some <$> `($nm) | .nonRec _ => pure none + | .composed _ => throwError "Cannot handle composed" else pure #[] @@ -191,17 +156,25 @@ def generateRecBody (ctors : Array (Name × List RecursionForm)) (includeMotive `(matchAltExprs| $deeper:matchAlt*) -def genRecursors (view : DataView) : CommandElabM Unit := do +def createVecForArgs : Array Ident → m Term + | ⟨.nil⟩ => `($(mkIdent ``Vec.nil)) + | ⟨.cons hd tl⟩ => do `( ($(mkIdent ``TypeVec.append1) $(←createVecForArgs ⟨tl⟩) $hd) ) + +section + +variable (view : DataView) (shape : Name) + +def genForData : CommandElabM Unit := do let rec_type := view.getExpectedType - let mapped ← view.ctors.mapM (extract view.declName · rec_type) + let mapped := view.ctors.map (RecursionForm.extractWithName view.declName · rec_type) let ih_types ← mapped.mapM fun ⟨name, base⟩ => mkRecursorBinder (rec_type) (name) base true let indDef : Command ← `( @[elab_as_elim, eliminator] - def $(.str view.shortDeclName "ind" |> mkIdent):ident + def $(view.shortDeclName ++ `ind |> mkIdent):ident { motive : $rec_type → Prop} $ih_types* : (val : $rec_type) → motive val @@ -212,7 +185,7 @@ def genRecursors (view : DataView) : CommandElabM Unit := do let recDef : Command ← `( @[elab_as_elim] - def $(.str view.shortDeclName "rec" |> mkIdent):ident + def $(view.shortDeclName ++ `rec |> mkIdent):ident { motive : $rec_type → Type _} $ih_types* : (val : $rec_type) → motive val @@ -224,7 +197,7 @@ def genRecursors (view : DataView) : CommandElabM Unit := do let casesDef : Command ← `( @[elab_as_elim] - def $(.str view.shortDeclName "cases" |> mkIdent):ident + def $(view.shortDeclName ++ `cases |> mkIdent):ident { motive : $rec_type → Prop} $casesOnTypes* : (val : $rec_type) → motive val @@ -234,7 +207,7 @@ def genRecursors (view : DataView) : CommandElabM Unit := do let casesTypeDef : Command ← `( @[elab_as_elim] - def $(.str view.shortDeclName "casesType" |> mkIdent):ident + def $(view.shortDeclName ++ `casesType |> mkIdent):ident { motive : $rec_type → Type} $casesOnTypes* : (val : $rec_type) → motive val @@ -253,3 +226,151 @@ def genRecursors (view : DataView) : CommandElabM Unit := do Elab.Command.elabCommand casesTypeDef pure () + +def genForCoData : CommandElabM Unit := do + if view.deadBinders.size != 0 then + throwError "dead corecursion not supported" + + let corecType := view.getExpectedType + + let base := view.shortDeclName ++ `Base |> mkIdent + + let corecDef : Command ← `( + def $(view.shortDeclName ++ `corec |> mkIdent):ident + { β } + (f : β → $(view.getExpectedTypeWithId base) β) + : β → $corecType + := $(mkIdent ``MvQPF.Cofix.corec) f) + + let binders : Array Ident := (← view.liveBinders.mapM fun + | `(_) => mkIdent <$> mkFreshBinderName + | v => pure ⟨v⟩).reverse + + + let vec ← createVecForArgs binders + + let idTyFunCurried := mkIdent ``TypeFun.curried + let idDeepThunk := mkIdent ``MvQPF.DeepThunk + let idTyFunCurriedAux := mkIdent ``TypeFun.curriedAux + let idRevArgs := mkIdent ``TypeFun.reverseArgs + + let dtId := view.shortDeclName ++ `DeepThunk |> mkIdent + + 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 dtUncurr ← `( $(``MvQPF.DeepThunk.Uncurried |> mkIdent) + $(view.shortDeclName ++ `Base.Uncurried |> mkIdent) + ($(mkIdent ``TypeVec.append1) $vec ζ)) + + let uncA := view.shortDeclName ++ `Unc |> mkIdent + let uncDtA := view.shortDeclName ++ `DeepThunk.Unc |> mkIdent + + let curryUncurryEq ← `(command| + theorem $uncA : + $tCurr = $tUncurr := by + simp only [ + $(view.shortDeclName |> mkIdent):ident, + $idTyFunCurried:ident, + $idTyFunCurriedAux:ident, + $idRevArgs:ident + ] + congr + funext x + congr + fin_cases x <;> rfl + ) + let curryUncurryDeepThunkEq ← `(command| + theorem $uncDtA {ζ} : + $dtCurr = $dtUncurr + := by + simp only [ + $dtId:ident, + $idDeepThunk:ident, + $idTyFunCurried:ident, + $idTyFunCurriedAux:ident, + $idRevArgs:ident + ] + congr + funext x + congr + fin_cases x <;> rfl + ) + + let Coe := mkIdent ``Coe + let lu : Lean.Syntax.Command ← `( + instance : $Coe ($tCurr) ($tUncurr) := + ⟨fun x => by rw [←$uncA]; exact x⟩ + ) + let ru : Lean.Syntax.Command ← `( + instance : $Coe ($tUncurr) ($tCurr) := + ⟨fun x => by rw [$uncA:ident]; exact x⟩ + ) + let lud : Lean.Syntax.Command ← `( + instance {ζ}: $Coe ($dtCurr) ($dtUncurr) := + ⟨fun x => by rw [←$uncDtA]; exact x⟩ + + ) + let rud : Lean.Syntax.Command ← `( + instance {ζ}: $Coe ($dtUncurr) ($dtCurr) := + ⟨fun x => by rw [$uncDtA:ident]; exact x⟩ + ) + let inj : Lean.Syntax.Command ← `( + instance {ζ}: $Coe ($tCurr) ($dtCurr) := + ⟨fun x => + let x : $tUncurr := x + let x : $dtUncurr := $(mkIdent ``MvQPF.DeepThunk.inject) x + x + ⟩ + ) + let dtCorec : Lean.Syntax.Command ← `( + def $(view.shortDeclName ++ `DeepThunk.corec |> mkIdent) { ζ } (f : ζ → $dtCurr) (v : ζ) : $tCurr := + let v : $tUncurr := $(mkIdent ``MvQPF.DeepThunk.corec) (fun v => f v) v + v + ) + + trace[QPF] "Corec definitions:" + trace[QPF] corecDef + trace[QPF] deepThunk + trace[QPF] curryUncurryEq + trace[QPF] curryUncurryDeepThunkEq + + trace[QPF] lu + trace[QPF] ru + trace[QPF] lud + trace[QPF] rud + trace[QPF] inj + + trace[QPF] dtCorec + + elabCommand corecDef + elabCommand deepThunk + elabCommand curryUncurryEq + elabCommand curryUncurryDeepThunkEq + + elabCommand lu + elabCommand ru + elabCommand lud + elabCommand rud + elabCommand inj + + elabCommand dtCorec + + dbg_trace shape + Data.Command.mkConstructorsWithNameAndType view shape (fun ctor => + (view.declName ++ `DeepThunk ++ (Name.stripPrefix2 view.declName ctor.declName) |> mkIdent)) + (← `(ζ ⊕ ($dtCurr))) + dtCurr + (#[(← `(bb|{ ζ : Type }) : TSyntax ``bracketedBinder)]) + +def genRecursors : CommandElabM Unit := match view.command with + | .Data => genForData view + | .Codata => genForCoData view shape + +end +end + diff --git a/Qpf/Macro/Data/RecForm.lean b/Qpf/Macro/Data/RecForm.lean new file mode 100644 index 0000000..1941ef7 --- /dev/null +++ b/Qpf/Macro/Data/RecForm.lean @@ -0,0 +1,66 @@ +import Qpf.Macro.Data.Replace + +open Lean.Parser (Parser) +open Lean Meta Elab.Command Elab.Term Parser.Term +open Lean.Parser.Tactic (inductionAlt) + +/-- + The recursive form encodes how a function argument is recursive. + + Examples ty R α: + + α → R α → List (R α) → R α + [nonRec, directRec, composed ] +-/ +inductive RecursionForm := + | nonRec (stx : Term) + | directRec + | composed (stx : Term) -- Not supported yet +deriving Repr, BEq + +namespace RecursionForm + +variable {m} [Monad m] [MonadQuotation m] + +private def containsStx (top : Term) (search : Term) : Bool := + (top.raw.find? (· == search)).isSome + +partial def getArgTypes (v : Term) : List Term := match v.raw with + | .node _ ``arrow #[arg, _, deeper] => + ⟨arg⟩ :: getArgTypes ⟨deeper⟩ + | rest => [⟨rest⟩] + +partial def toType (retTy : Term) : List Term → m Term + | [] => pure retTy + | hd :: tl => do `($hd → $(← toType retTy tl)) + +/-- Extract takes a constructor and extracts its recursive forms. + +This function assumes the pre-processor has run +It also assumes you don't have polymorphic recursive types such as +data Ql α | nil | l : α → Ql Bool → Ql α -/ +def extract (view : CtorView) (rec_type : Term) : List RecursionForm := do + if let some type := view.type? then + let type_ls := (getArgTypes ⟨type⟩).dropLast + + type_ls.map fun v => + if v == rec_type then .directRec + else if containsStx v rec_type then + .composed v + else .nonRec v + else [] + +def extractWithName (topName : Name) (view : CtorView) (rec_type : Term) : Name × List RecursionForm := + (view.declName.replacePrefix topName .anonymous , extract view rec_type) + +def replaceRec (old new : Term) : RecursionForm → Term + | .nonRec x => x + | .directRec => new + | .composed x => ⟨Replace.replaceAllStx old new x⟩ + +def toTerm (recType : Term) : RecursionForm → Term + | .nonRec x | .composed x => x + | .directRec => recType + +end RecursionForm + diff --git a/Qpf/Qpf/Multivariate/Constructions/DeepThunk.lean b/Qpf/Qpf/Multivariate/Constructions/DeepThunk.lean new file mode 100644 index 0000000..bf57bd4 --- /dev/null +++ b/Qpf/Qpf/Multivariate/Constructions/DeepThunk.lean @@ -0,0 +1,97 @@ +import Mathlib.Data.QPF.Multivariate.Constructions.Comp +import Mathlib.Data.QPF.Multivariate.Constructions.Prj +import Mathlib.Data.QPF.Multivariate.Constructions.Cofix +import Qpf.Macro.Comp + +namespace MvQPF + +namespace DeepThunk +abbrev innerMapper : Vec (TypeFun (n.succ)) n := (fun + | .fz => Comp Sum.Sum' !![Prj 1, Prj 0] + | .fs n => Prj (n.add 2)) + +/-- The actual higher order functor taking `cofix f α in α` to `cofix f (β ⊕ α) in α` -/ +abbrev hoFunctor (F : TypeFun n) : TypeFun (n + 1) := Comp F innerMapper + +instance : MvFunctor (!![Prj 1, @Prj (n + 2) 0] j) := by + rcases j with _|_|_|_ + <;> simp only [Vec.append1] + <;> infer_instance +instance : MvQPF (!![Prj 1, @Prj (n + 2) 0] j) := by + rcases j with _|_|_|_ + <;> simp only [Vec.append1] + <;> infer_instance + +instance {i : Fin2 n} : MvFunctor (innerMapper i) := by cases i <;> infer_instance +instance {i : Fin2 n} : MvQPF (innerMapper i) := by cases i <;> infer_instance + +abbrev Uncurried (F : TypeFun n) [MvFunctor F] [MvQPF F] := Cofix (hoFunctor F) + + + +/-- + Between the original functor and the ⊕-composed functor there is an injection, + it occurs by taking the right step at every point co-recursively. + + The instances of the hof will have this defined as a coercion. +-/ +def inject + {F : TypeFun n.succ} {α : TypeVec n} + [inst : MvFunctor F] [MvQPF F] : Cofix F α → DeepThunk.Uncurried F (α ::: β) := + MvQPF.Cofix.corec fun v => by + let v := Cofix.dest v + + have : (hoFunctor F (α.append1 β ::: Cofix F α)) = F (α.append1 (β ⊕ Cofix F α)) := by + simp only [hoFunctor, Comp] + congr + funext i + simp only [innerMapper, TypeVec.append1] + cases i <;> rfl + rw [this] + + have arr : TypeVec.Arrow (α ::: Cofix F α) (α ::: (β ⊕ Cofix F α)) := + fun | .fz => fun a => by + simp only [TypeVec.append1] at a + simp only [TypeVec.append1] + exact .inr a + | .fs n => id + + exact inst.map arr v + +/-- + `DeepThunk.corec` is a co-recursive principle allowing partially yielding results. + It achives this by changing the recursive point to either the usual argument to the deeper call, + or continuing the structure. +-/ +def corec + {F : TypeFun n.succ} {α : TypeVec n} + [inst : MvFunctor F] [MvQPF F] + (f : β → Uncurried F (α ::: β)) + : β → Cofix F α + := (Cofix.corec fun v => by + have v := Cofix.dest v + + have : hoFunctor F (α.append1 β ::: Cofix (hoFunctor F) (α ::: β)) = F (α ::: (β ⊕ (Cofix (hoFunctor F) (α.append1 β)))) := by + simp only [hoFunctor, Comp] + congr + funext i + simp only [innerMapper, TypeVec.append1] + cases i <;> rfl + rw [this] at v + + have : TypeVec.Arrow (α ::: (β ⊕ (Cofix (hoFunctor F) (α ::: β)))) (α ::: Cofix (hoFunctor F) (α ::: β)) := fun + | .fz => fun | .inl x => f x | .inr x => x + | .fs _ => id + + exact MvFunctor.map this v + ) ∘ f + +end DeepThunk +/-- + `DeepThunk` is a higher-order functor used for partially yielding results in co-recursive principles. + It is defined by taking the cofix-point of the composition of the ⊕-functor and the `Base` functor. + For using this in co-recursive functions see `DeepThunk.corec` + -/ +abbrev DeepThunk (F : TypeFun n) [MvFunctor F] [MvQPF F] := DeepThunk.Uncurried F |> TypeFun.curried + +end MvQPF