diff --git a/Qpf/Macro/Comp.lean b/Qpf/Macro/Comp.lean index acf74d2..517befa 100644 --- a/Qpf/Macro/Comp.lean +++ b/Qpf/Macro/Comp.lean @@ -23,6 +23,7 @@ import Mathlib.Data.QPF.Multivariate.Constructions.Prj import Mathlib.Data.Vector.Basic import Qpf.Qpf +import Qpf.Qpf.Multivariate.Basic import Qpf.Macro.Common import Qq @@ -49,7 +50,7 @@ def synthMvFunctor {n : Nat} (F : Q(TypeFun.{u,u} $n)) : MetaM Q(MvFunctor $F) : q(MvFunctor $F) synthInstanceQ inst_type -def synthQPF {n : Nat} (F : Q(TypeFun.{u,u} $n)) (_ : Q(MvFunctor $F)) : MetaM Q(MvQPF $F) := do +def synthQPF {n : Nat} (F : Q(TypeFun.{u,u} $n)) : MetaM Q(MvQPF $F) := do let inst_type : Q(Type (u+1)) := q(MvQPF $F) synthInstanceQ inst_type @@ -87,10 +88,9 @@ where try -- Only try to infer QPF if `F` contains no live variables if !F.hasAnyFVar isLiveVar then - let F : Q(TypeFun.{u,u} $depth) - := q(TypeFun.ofCurried $F) - let functor ← synthMvFunctor F - let _ ← synthQPF F functor + let F : Q(TypeFun.{u,u} $depth) := + q(TypeFun.ofCurried $F) + let _ ← synthQPF F return ⟨depth, F, args⟩ throwError "Smallest function subexpression still contains live variables:\n {F}\ntry marking more variables as dead" catch e => @@ -106,8 +106,7 @@ where trace[QPF] "F := {F}\nargs := {args.toList}\ndepth := {depth}" let F : Q(TypeFun.{u,u} $depth) := q(TypeFun.ofCurried $F) - let functor ← synthMvFunctor F - let _ ← synthQPF F functor + let _ ← synthQPF F return ⟨depth, F, args⟩ @@ -213,7 +212,6 @@ partial def handleApp (vars : Vector FVarId arity) (target : Q(Type u)) : TermEl else let G ← args.mmap (elabQpf vars · none false) - let Ffunctor ← synthInstanceQ q(MvFunctor $F) let Fqpf ← synthInstanceQ q(@MvQPF _ $F) let G : Vec _ numArgs := fun i => G.get i.inv @@ -313,14 +311,17 @@ def elabQpfCompositionBody (view: QpfCompositionBodyView) : res.F.check res.qpf.check - withOptions (fun opt => opt.insert `pp.explicit true) <| do + let (F, qpf) ← withOptions (fun opt => opt.insert `pp.explicit true) <| do let F ← delab res.F let qpf ← delab res.qpf + pure (F, qpf) - withQPFTraceNode "results …" <| do - trace[QPF] "Functor := {F}" - trace[QPF] "MvQPF instance := {qpf}" - return ⟨F, qpf⟩ + withQPFTraceNode "results …" <| do + trace[QPF] "Functor (expr) := {res.F}" + trace[QPF] "Functor (stx) := {F}" + trace[QPF] "MvQPF (expr) := {res.qpf}" + trace[QPF] "MvQPF (stx) := {qpf}" + return ⟨F, qpf⟩ structure QpfCompositionView where @@ -385,10 +386,6 @@ def elabQpfComposition (view: QpfCompositionView) : CommandElabM Unit := do let F_applied ← `($F $deadBinderNamedArgs:namedArgument*) let cmd ← `( - $modifiers:declModifiers - instance : MvFunctor (TypeFun.ofCurried $F_applied) := - MvQPF.instMvFunctor_ofCurried_curried - $modifiers:declModifiers instance $deadBindersNoHoles:bracketedBinder* : MvQPF (TypeFun.ofCurried $F_applied) := MvQPF.instQPF_ofCurried_curried diff --git a/Qpf/Macro/Data.lean b/Qpf/Macro/Data.lean index a396601..02cc1c8 100644 --- a/Qpf/Macro/Data.lean +++ b/Qpf/Macro/Data.lean @@ -304,8 +304,8 @@ def mkQpf (shapeView : InductiveView) (ctorArgs : Array CtorArgs) (headT P : Ide map f x := ($eqv).invFun <| ($P).map f <| ($eqv).toFun <| x ) elabCommandAndTrace (header := "defining {q}") <|← `( - instance $q:ident : MvQPF.IsPolynomial (@TypeFun.ofCurried $(quote arity) $shape) := - .ofEquiv $P $eqv + instance $q:ident : MvQPF (@TypeFun.ofCurried $(quote arity) $shape) := + .ofEquiv (fun _ => $eqv) ) /-! ## mkShape -/ @@ -382,33 +382,6 @@ def mkShape (view : DataView) : TermElabM MkShapeResult := do mkQpf view ctorArgs headTId PId r.expr.size ⟩ -open Elab.Term Parser.Term in -/-- - Checks whether the given term is a polynomial functor, i.e., whether there is an instance of - `IsPolynomial F`, and return that instance (if it exists). --/ -def isPolynomial (view : DataView) (F: Term) : CommandElabM (Option Term) := - withQPFTraceNode "isPolynomial" (tag := "isPolynomial") <| - runTermElabM fun _ => do - elabBinders view.deadBinders fun _deadVars => do - let inst_func ← `(MvFunctor $F:term) - let inst_func ← elabTerm inst_func none - - trace[QPF] "F = {F}" - let inst_type ← `(MvQPF.IsPolynomial $F:term) - trace[QPF] "inst_type_stx: {inst_type}" - let inst_type ← elabTerm inst_type none - trace[QPF] "inst_type: {inst_type}" - - try - let _ ← synthInstance inst_func - let inst ← synthInstance inst_type - return some <|<- delab inst - catch e => - trace[QPF] "Failed to synthesize `IsPolynomial` instance.\ - \n\n{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` diff --git a/Qpf/PFunctor/Multivariate/Constructions/Prod.lean b/Qpf/PFunctor/Multivariate/Constructions/Prod.lean index 0c36363..91ee803 100644 --- a/Qpf/PFunctor/Multivariate/Constructions/Prod.lean +++ b/Qpf/PFunctor/Multivariate/Constructions/Prod.lean @@ -6,31 +6,26 @@ import Mathlib.Data.QPF.Multivariate.Basic import Mathlib.Tactic.FinCases import Qpf.Util -import Qpf.Qpf.Multivariate.Basic namespace MvQPF namespace Prod open PFin2 (fz fs) -def P : MvPFunctor.{u} 2 := +def P : MvPFunctor.{u} 2 := .mk PUnit fun _ _ => PFin2 1 abbrev QpfProd' := P.Obj abbrev QpfProd := TypeFun.curried QpfProd' -/-- - An uncurried version of the root `Prod` --/ -abbrev Prod' : TypeFun 2 - := @TypeFun.ofCurried 2 Prod +/-- An uncurried version of the root `Prod` -/ +def Prod' : TypeFun 2 := + @TypeFun.ofCurried 2 Prod -/-- - Constructor for `QpfProd'` --/ -def mk (a : Γ 1) (b : Γ 0) : QpfProd'.{u} Γ := +/-- Constructor for `QpfProd'` -/ +def mk (a : Γ 1) (b : Γ 0) : QpfProd'.{u} Γ := ⟨ ⟨⟩, fun @@ -56,8 +51,9 @@ def equiv {Γ} : Prod' Γ ≃ QpfProd' Γ := { instance : MvFunctor Prod' where map f x := equiv.invFun <| P.map f <| equiv.toFun <| x -instance : MvQPF.IsPolynomial Prod' := .ofEquiv _ equiv - +instance : MvQPF Prod' := .ofEquiv (fun _ => equiv) +instance : MvQPF (@TypeFun.ofCurried 2 Prod) := + inferInstanceAs (MvQPF Prod') end Prod diff --git a/Qpf/PFunctor/Multivariate/Constructions/Sum.lean b/Qpf/PFunctor/Multivariate/Constructions/Sum.lean index e62f1bd..d51b988 100644 --- a/Qpf/PFunctor/Multivariate/Constructions/Sum.lean +++ b/Qpf/PFunctor/Multivariate/Constructions/Sum.lean @@ -6,7 +6,6 @@ import Mathlib.Data.QPF.Multivariate.Basic import Mathlib.Tactic.FinCases import Qpf.Util -import Qpf.Qpf.Multivariate.Basic namespace MvQPF namespace Sum @@ -38,7 +37,7 @@ def inr {Γ : TypeVec 2} (b : Γ 0) : QpfSum' Γ ⟩ -abbrev Sum' := @TypeFun.ofCurried 2 Sum +def Sum' := @TypeFun.ofCurried 2 Sum def box {Γ : TypeVec 2} : Sum' Γ → QpfSum' Γ | .inl a => inl a @@ -70,8 +69,9 @@ def equiv {Γ} : Sum' Γ ≃ QpfSum' Γ := instance : MvFunctor Sum' where map f x := equiv.invFun <| SumPFunctor.map f <| equiv.toFun <| x -instance : MvQPF.IsPolynomial Sum' := - .ofEquiv _ equiv +instance : MvQPF Sum' := .ofEquiv @equiv +instance : MvQPF (@TypeFun.ofCurried 2 Sum) := + inferInstanceAs (MvQPF Sum') end Sum diff --git a/Qpf/Qpf.lean b/Qpf/Qpf.lean index 2127c89..c5fb806 100644 --- a/Qpf/Qpf.lean +++ b/Qpf/Qpf.lean @@ -1,6 +1,4 @@ -import Qpf.Qpf.Multivariate.Basic - import Qpf.PFunctor.Multivariate.Basic import Qpf.PFunctor.Multivariate.Constructions.Arrow import Qpf.PFunctor.Multivariate.Constructions.Prod diff --git a/Qpf/Qpf/Multivariate/Basic.lean b/Qpf/Qpf/Multivariate/Basic.lean index f235665..b28c324 100644 --- a/Qpf/Qpf/Multivariate/Basic.lean +++ b/Qpf/Qpf/Multivariate/Basic.lean @@ -2,86 +2,14 @@ import Mathlib.Data.QPF.Multivariate.Basic import Qpf.Util.TypeFun namespace MvQPF - /-- - A QPF is polynomial, if it is equivalent to the underlying `MvPFunctor`. - `repr_abs` is the last property needed to show that `abs` is an isomorphism, with `repr` - its inverse - -/ - class IsPolynomial {n} (F : TypeVec n → Type _) extends MvQPF F where - repr_abs : ∀ {α} (x : P.Obj α), repr (abs x) = x - - - namespace IsPolynomial - variable {n : ℕ} {F : TypeVec n → Type _} - - /-- - Show that the desired equivalence follows from `IsPolynomial` - -/ - def equiv [MvFunctor F] [p : IsPolynomial F] : - ∀ α, F α ≃ p.P.Obj α - := fun _ => { - toFun := p.repr, - invFun := p.abs, - left_inv := p.abs_repr, - right_inv := p.repr_abs, - } - - def ofEquiv (P : MvPFunctor n) (eqv : ∀ {α}, F α ≃ P.Obj α) [functor : MvFunctor F] (map_eq : ∀ (α β : TypeVec n) (f : TypeVec.Arrow α β) (x : F α), functor.map f x = (eqv.invFun <| P.map f <| eqv.toFun <| x) := by intros; rfl) : IsPolynomial F where - P := P - abs := eqv.invFun - repr := eqv.toFun - abs_repr := eqv.left_inv - abs_map := by intros; - simp only [Equiv.invFun_as_coe, map_eq, Equiv.toFun_as_coe, - Equiv.apply_symm_apply, Equiv.symm_apply_apply, EmbeddingLike.apply_eq_iff_eq]; - rfl - repr_abs := eqv.right_inv - - end IsPolynomial - -end MvQPF - -namespace MvPFunctor - variable {n : Nat} (P : MvPFunctor n) - - /-- - Every polynomial functor is trivially a QPF - -/ - instance : MvQPF P.Obj := - { - P := P, - abs := id, - repr := id, - abs_repr := by intros; rfl, - abs_map := by intros; rfl, - } - - /-- - Every polynomial functor is a polynomial QPF - -/ - instance : MvQPF.IsPolynomial P.Obj := - { - repr_abs := by intros; rfl - } - -end MvPFunctor - - variable {n} {F : TypeFun n} -namespace MvQPF - instance instMvFunctor_ofCurried_curried [f : MvFunctor F] : - MvFunctor <| TypeFun.ofCurried <| F.curried := - TypeFun.ofCurried_curried_involution ▸ f - - instance instQPF_ofCurried_curried [MvFunctor F] [q : MvQPF F] : - MvQPF <| TypeFun.ofCurried <| F.curried := - TypeFun.ofCurried_curried_involution ▸ q +instance instMvFunctor_ofCurried_curried [f : MvFunctor F] : + MvFunctor <| TypeFun.ofCurried <| F.curried := + TypeFun.ofCurried_curried_involution ▸ f - instance instIsPolynomial_ofCurried_curried [functor : MvFunctor F] [p : IsPolynomial F] : - IsPolynomial <| TypeFun.ofCurried <| F.curried := by - apply cast ?_ p - congr - · rw [TypeFun.ofCurried_curried_involution] +instance instQPF_ofCurried_curried [q : MvQPF F] : + MvQPF <| TypeFun.ofCurried <| F.curried := + TypeFun.ofCurried_curried_involution ▸ q end MvQPF diff --git a/Qpf/Qpf/Multivariate/Constructions/Comp.lean b/Qpf/Qpf/Multivariate/Constructions/Comp.lean deleted file mode 100644 index 664b414..0000000 --- a/Qpf/Qpf/Multivariate/Constructions/Comp.lean +++ /dev/null @@ -1,85 +0,0 @@ -/- -Copyright (c) 2023 Alex Keizer. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Alex Keizer --/ - -import Mathlib.Data.QPF.Multivariate.Basic -import Mathlib.Data.QPF.Multivariate.Constructions.Comp -import Qpf.Util - -/-! - Show that the composition of polynomial QPFs is itself a polynomial QPF --/ - -universe u - -namespace MvQPF.Comp - -open MvPFunctor MvFunctor - -variable {n m : ℕ} - (F : TypeFun n) - (G : Vec (TypeFun m) n) - [p : IsPolynomial F] - [p' : ∀ i, IsPolynomial <| G i] - - - instance : IsPolynomial (Comp F G) where - repr_abs := by - intros α x; - rcases x with ⟨⟨a', f'⟩, f⟩ - simp only [Comp.get, Comp.mk, Function.comp_apply, repr, abs, ← p.abs_map, p.repr_abs] - simp only [(· <$$> ·), MvPFunctor.map, comp.mk, comp.get, TypeVec.comp] - congr 2 - { - funext i b - rw[(p' i).repr_abs] - } - { - apply HEq.funext - . simp only [IsPolynomial.repr_abs]; rfl - intro i - - have type_eq_α : B (comp (P F) fun i => P (G i)) - { fst := a', - snd := fun x a => - (repr (abs { fst := f' x a, snd := fun j b => f j { fst := x, snd := { fst := a, snd := b } } })).fst } - i = - B (P (Comp F G)) { fst := a', snd := f' } i := - by simp only [IsPolynomial.repr_abs]; rfl - - apply HEq.funext' - case type_eq_β => - intros; rfl - case type_eq_α => - exact type_eq_α - - rintro ⟨b, ⟨b', g'⟩⟩ - simp only [heq_eq_eq] - - have : repr (abs - ⟨ f' b b', - fun j b_1 => - f j ⟨b, ⟨b', b_1⟩⟩ - ⟩) - = ⟨ f' b b', - fun j b_1 => - f j ⟨b, ⟨b', b_1⟩⟩ - ⟩; - { - simp [IsPolynomial.repr_abs] - } - simp[type_eq_α, this] - /- - TODO: properly finish this proof - -/ - sorry - } - - - - - - -end MvQPF.Comp diff --git a/Qpf/Qpf/Multivariate/Constructions/DeepThunk.lean b/Qpf/Qpf/Multivariate/Constructions/DeepThunk.lean index ec3992a..2532d44 100644 --- a/Qpf/Qpf/Multivariate/Constructions/DeepThunk.lean +++ b/Qpf/Qpf/Multivariate/Constructions/DeepThunk.lean @@ -62,8 +62,8 @@ instance : MvFunctor DTSum.Uncurried where map f := equiv.invFun ∘ Sum.SumPFunctor.map f ∘ equiv.toFun open DTSum in -instance : MvQPF.IsPolynomial DTSum.Uncurried := - .ofEquiv _ equiv +instance : MvQPF DTSum.Uncurried := + .ofEquiv (fun _ => equiv) namespace DeepThunk diff --git a/Qpf/Qpf/Multivariate/Scratch.lean b/Qpf/Qpf/Multivariate/Scratch.lean new file mode 100644 index 0000000..a84797d --- /dev/null +++ b/Qpf/Qpf/Multivariate/Scratch.lean @@ -0,0 +1,117 @@ +import Qpf +import Mathlib.Data.QPF.Multivariate.Constructions.Sigma + +#check MvPFunctor + +/-! +# Interaction Trees + +We define interaction trees, a coinductive data-structure used for giving +semantics of side-effecting, possibly non-terminating, programs + +[1] https://arxiv.org/abs/1906.00046 +[2] https://github.com/DeepSpec/InteractionTrees +-/ + +set_option trace.QPF true +-- set_option diagnostics true + +-- codata ITree (E : Type → Type) A where +-- | ret (r : A) +-- | tau (t : ITree E A) +-- | vis (_ : (Ans : Type) × ( E Ans) × ( Ans → ITree E A)) +-- -- vis : {Ans : Type} -> (e : E Ans) -> (k : Ans -> ITree E A) -> ITree E A + +section HeadChild + inductive ITree.HeadT : Type 1 + | ret + | tau + | vis (Ans : Type) + + def ITree.ChildT : ITree.HeadT -> TypeVec.{1} 2 + | .ret => ![PFin2.{1} 1, PFin2.{1} 0] -- One `A`, zero `ρ` + | .tau => ![PFin2.{1} 0, PFin2.{1} 1] -- Zero `A`, one `ρ` (remember, `ρ` intuitively means `ITree E A`) + | .vis Ans => ![PFin2.{1} 0, ULift.{1, 0} Ans] -- Zero `A`, and... `Ans` many `ρ`... -- ! where do we get Ans from? + + abbrev ITree.P : MvPFunctor.{1} 2 := ⟨ITree.HeadT, ITree.ChildT⟩ + abbrev ITree.F : TypeVec.{1} 2 -> Type 1 := ITree.P.Obj + + def ITree.box : F α → P.Obj α := sorry + def ITree.unbox : P.Obj α → F α := sorry + def ITree.box_unbox_id : (x : P.Obj α) -> box (unbox x) = x := sorry + def ITree.unbox_box_id : (x : F α) -> unbox (box x) = x := sorry + instance ITree.instMvQPF : MvQPF ITree.F := MvQPF.ofPolynomial P box unbox box_unbox_id unbox_box_id sorry + + def ITree_ugly := MvQPF.Cofix ITree.F -- you could do it this way, but it will be very unwieldy. Hence shape types. +end HeadChild + +set_option pp.universes true + +section ShapeBase + inductive ITree.Shape (E : Type -> Type) (A : Type 1) (ρ : Type 1) (ν : Type 1) : Type 1 + | ret (r : A) : ITree.Shape E A ρ ν + | tau (t : ρ) : ITree.Shape E A ρ ν + | vis (e : ν) : ITree.Shape .. + -- | vis : (Ans : Type) × E Ans × (Ans → ρ) -> ITree.Shape E A ρ + + -- qpf ITree.Base (E : Type -> Type) (A : Type) ρ := ITree.Shape E A ρ ((Ans : Type) × ULift.{1} (E Ans) × (Ans → ρ)) + -- ! If only we had this instance... life would be so easy + -- instance {E : Type -> Type} : MvQPF (TypeFun.ofCurried (n := 1) (ITree.Shape E A)) := sorry + -- def ITree' (E : Type -> Type) (A : Type 1) : TypeFun.{1} 0 := + -- MvQPF.Cofix (TypeFun.ofCurried <| ITree.Shape E A) + + /-- `qpf G (Ans : Type) (E : Type → Type) A ρ ν := E Ans × (Ans → ρ)`, but universe-polymorphic -/ + abbrev G.Uncurried (Ans : Type 0) (E : Type 0 → Type 0) : TypeFun.{1, 1} 2 := + MvQPF.Comp (n := 2) (m := 2) -- compose two 2-ary (A, ρ) functors `E Ans` and `Ans -> ρ` + (TypeFun.ofCurried Prod.{1, 1}) + -- (MvQPF.Prod.Prod') + ( + (Vec.append1 Vec.nil (MvQPF.Const 2 <| ULift (E Ans))).append1 + (MvQPF.Comp (n := 1) (m := 2) + (TypeFun.ofCurried (MvQPF.Arrow Ans)) + (Vec.append1 Vec.nil (MvQPF.Prj 1)) + ) + ) + + -- Ideally we'd do this directly, but the QPF meta code isn't there yet -- qpf G_vis (E : Type -> Type) A ρ ν := (Ans : Type) × (E Ans × (Ans -> ρ)) + abbrev G_vis.Uncurried (E : Type → Type) : TypeFun.{1,1} 2 := + MvQPF.Sigma.{1} fun (Ans : Type) => (G.Uncurried Ans E) + qpf G_ret (E : Type -> Type) A ρ := A + qpf G_tau (E : Type -> Type) A ρ := ρ + + set_option trace.Meta.synthInstance true + + #check MvQPF.Prod.instMvFunctorProd' + instance : MvQPF (TypeFun.ofCurried (n := 2) @Prod.{u}) := + sorry + + instance (i : PFin2 1) : MvQPF (Vec.append1 Vec.nil (MvQPF.Prj (n:=2) 1) i) := sorry + #synth ∀i : PFin2 1, MvQPF (Vec.append1 Vec.nil (MvQPF.Prj (n:=2) 1) i) + instance {Ans} {E : Type -> Type} : MvQPF.{1, 1} (G.Uncurried Ans E) := inferInstance + instance {Ans} {E : Type -> Type} : MvQPF.{1, 1} (G.Uncurried Ans E) := inferInstance + instance {E : Type -> Type} : MvQPF.{1, 1} (G_vis.Uncurried E) := inferInstance + + abbrev ITree.ConstructorFs (E : Type -> Type) : Fin2 3 -> TypeVec 2 -> Type 1 := + ![G_ret.Uncurried E, G_tau.Uncurried E, G_vis.Uncurried E] + + abbrev ITree.Base.Uncurried (E : Type -> Type) : TypeFun 2 := + MvQPF.Comp (TypeFun.ofCurried (n := 3) (ITree.Shape E)) (ITree.ConstructorFs E) + + -- def ITree.Base.Uncurried' (E : Type -> Type) : TypeFun 2 := fun v => ITree.Shape E (v 1) ((ITree.ConstructorFs E) 0 v) -- what am I even doing + abbrev ITree.Base (E : Type -> Type) (A ρ : Type 1) : Type 1 := + MvQPF.Comp (TypeFun.ofCurried (n := 3) (ITree.Shape E)) (ITree.ConstructorFs E) ![A, ρ] + + instance {E : Type -> Type} : MvQPF.{1, 1} (ITree.Base.Uncurried E) := inferInstance + + def ITree.Uncurried (E : Type -> Type) := + MvQPF.Cofix (ITree.Base.Uncurried E) +end ShapeBase + +instance {E : Type -> Type} : MvQPF (ITree.Base.Uncurried E) := sorry + +def ITree.Uncurried (E : Type -> Type) := MvQPF.Cofix (ITree.Base.Uncurried E) +def ITree (E : Type -> Type) (A : Type 1) : Type 1 := MvQPF.Cofix (ITree.Base.Uncurried E) ![A, A] -- ! why two + +#reduce (types := true) TypeVec.{1} 2 + +#check 1 diff --git a/Test/DeadWrap.lean b/Test/DeadWrap.lean index 4bf8524..7c0ce5d 100644 --- a/Test/DeadWrap.lean +++ b/Test/DeadWrap.lean @@ -18,6 +18,6 @@ data DeadWrap (α : Type) β /-- info: DeadWrap.Shape.qpf -/ #guard_msgs in - #synth MvQPF.IsPolynomial <| @TypeFun.ofCurried 3 DeadWrap.Shape + #synth MvQPF <| @TypeFun.ofCurried 3 DeadWrap.Shape end Test