Skip to content

Commit

Permalink
fix failing Comp test
Browse files Browse the repository at this point in the history
By reviving some instances from deleted file
  • Loading branch information
alexkeizer committed Dec 4, 2024
1 parent 08c6879 commit 3a9cd03
Show file tree
Hide file tree
Showing 2 changed files with 24 additions and 9 deletions.
18 changes: 9 additions & 9 deletions Qpf/Macro/Comp.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -310,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
Expand Down Expand Up @@ -382,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
Expand Down
15 changes: 15 additions & 0 deletions Qpf/Qpf/Multivariate/Basic.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
import Mathlib.Data.QPF.Multivariate.Basic
import Qpf.Util.TypeFun

namespace MvQPF
variable {n} {F : TypeFun n}

instance instMvFunctor_ofCurried_curried [f : MvFunctor F] :
MvFunctor <| TypeFun.ofCurried <| F.curried :=
TypeFun.ofCurried_curried_involution ▸ f

instance instQPF_ofCurried_curried [q : MvQPF F] :
MvQPF <| TypeFun.ofCurried <| F.curried :=
TypeFun.ofCurried_curried_involution ▸ q

end MvQPF

0 comments on commit 3a9cd03

Please sign in to comment.