Merge branch 'main' into qpfExpr-abstraction

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 Qpf.Macro.QpfExpr
 
@@ -50,7 +51,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
@@ -88,10 +89,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 =>
@@ -107,8 +107,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⟩
 
 def List.indexOf' {α : Type} [BEq α] :  α → (as : List α) → Option (Fin2 (as.length))
@@ -160,6 +159,7 @@ partial def handleApp (vars : Vector FVarId arity) (target : Q(Type u)) : TermEl
     return F
   else
     let G ← args.mmap (elabQpf vars · none false)
+    let Fqpf ← synthInstanceQ q(@MvQPF _ $F)
     let G : Vec _ numArgs := fun i => G.get i.inv
 
     let C := QpfExpr.comp F G
@@ -255,8 +255,6 @@ structure QpfCompositionView where
   (type?      : Option Term := none)
   (target     : Term)
 
-#synth CoreM MetaM
-
 /--
   Given the description of a QPF composition (`QpfCompositionView`), add a declaration for the
   desired functor (in both curried form as the `F` and uncurried form as `F.typefun`)
@@ -305,20 +303,7 @@ def elabQpfComposition (view: QpfCompositionView) : CommandElabM Unit := do
   --     def $F:ident $deadBinders:bracketedBinder* : CurriedTypeFun $live_arity :=
   --       TypeFun.curried $F_internal_applied
 
-  --     $modifiers:declModifiers
-  --     instance $deadBinders:bracketedBinder* : MvQPF ($F_internal_applied) := $qpf:term
-  -- )
-  -- trace[QPF] "cmd: {cmd}"
-  -- elabCommand cmd
-
-
-  -- 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

Qpf/Macro/Data.lean

@@ -301,8 +301,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 -/
@@ -379,33 +379,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`

Qpf/PFunctor/Multivariate/Constructions/Arrow.lean

@@ -36,8 +36,8 @@ namespace Arrow
 
 
 
-  def box (f : Arrow' α Γ) : (QpfArrow' α Γ)
-    := ⟨(), fun | 0 => f⟩
+  def box (f : Arrow'.{u} α Γ) : (QpfArrow' α Γ)
+    := ⟨⟨⟩, fun | 0 => f⟩
 
   def unbox : QpfArrow' α Γ → Arrow' α Γ
     | ⟨_, f⟩ => f 0
@@ -60,7 +60,7 @@ namespace Arrow
   instance : MvFunctor (Arrow' x) where
     map f a     := unbox <| (ArrowPFunctor x).map f <| box a
 
-  instance : MvQPF (Arrow' x) where
+  instance instMvQPF : MvQPF (Arrow' x) where
     P           := ArrowPFunctor x
     abs         := @unbox x
     repr        := @box x

Qpf/PFunctor/Multivariate/Constructions/Prod.lean

@@ -6,33 +6,28 @@ 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 2
-  := .mk Unit fun _ _ => PFin2 1
+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' Γ
-  := ⟨
-      (),
+/-- Constructor for `QpfProd'` -/
+def mk (a : Γ 1) (b : Γ 0) : QpfProd'.{u} Γ :=
+  ⟨
+      ⟨⟩,
       fun
       | 1, _ => a
       | 0, _ => b
@@ -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
 

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
 

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

Qpf/Qpf/Multivariate/Basic.lean

@@ -2,87 +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 _) [MvFunctor F] 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]
-    · exact HEq.symm (eqRec_heq ..)
+instance instQPF_ofCurried_curried [q : MvQPF F] :
+    MvQPF <| TypeFun.ofCurried <| F.curried :=
+  TypeFun.ofCurried_curried_involution ▸ q
 
 end MvQPF