WIP stash

Qpf/Macro/Comp.lean

@@ -280,8 +280,8 @@ def elabQpfComposition (view: QpfCompositionView) : CommandElabM Unit := do
   let F_internal := Name.mkStr view.F "Uncurried";
   let F := view.F;
 
-
-  qpfExpr.addToEnvironment F_internal []
+  liftCoreM <| do
+    qpfExpr.addToEnvironment F_internal []
   return ()
   -- let modifiers := quote (k := ``declModifiers) view.modifiers;
 

Qpf/Macro/Data.lean

@@ -383,7 +383,7 @@ def mkShape (view : DataView) : TermElabM MkShapeResult := do
   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`
 -/
-def mkType (view : DataView) (base : Term × Term) : CommandElabM Unit :=
+def mkType {u n} (view : DataView) (base : QpfExpr' u n) : CommandElabM Unit :=
   withQPFTraceNode m!"defining (co)datatype {view.declId}" (tag := "mkType") <| do
 
   let uncurriedIdent ← addSuffixToDeclIdent view.declId "Uncurried"
@@ -399,37 +399,38 @@ def mkType (view : DataView) (base : Term × Term) : CommandElabM Unit :=
   let arity := view.liveBinders.size
   let fix_or_cofix := DataCommand.fixOrCofix view.command
 
-  let ⟨base, q⟩ := base
-  elabCommandAndTrace
-    (header := m!"elaborating uncurried base functor {baseIdent} …") <|← `(
-      abbrev $baseIdent:ident $view.deadBinders:bracketedBinder* :
-          TypeFun $(quote <| arity + 1) :=
-        $base
-  )
-
-  elabCommandAndTrace
-    (header := m!"elaborating *curried* base functor {baseIdExt} …") <|← `(
-      abbrev $baseIdExt $view.deadBinders:bracketedBinder* :=
-        TypeFun.curried $baseApplied
-  )
-
-  elabCommandAndTrace
-    (header := m!"elaborating qpf instance for {baseIdent} …") <|← `(
-      instance $baseQPFIdent:ident : MvQPF ($baseApplied) := $q
-  )
-
-  elabCommandAndTrace
-    (header := m!"elaborating uncurried (co)fixpoint {uncurriedIdent} …") <|← `(
-      abbrev $uncurriedIdent:ident $view.deadBinders:bracketedBinder* :
-          TypeFun $(quote arity) :=
-        $fix_or_cofix $base
-  )
-
-  elabCommandAndTrace
-    (header := m!"elaborating *curried* (co)fixpoint {view.declId} …")  <|← `(
-      abbrev $(view.declId) $view.deadBinders:bracketedBinder* :=
-        TypeFun.curried $uncurriedApplied
-  )
+  return ()
+  -- let ⟨base, q⟩ := base
+  -- elabCommandAndTrace
+  --   (header := m!"elaborating uncurried base functor {baseIdent} …") <|← `(
+  --     abbrev $baseIdent:ident $view.deadBinders:bracketedBinder* :
+  --         TypeFun $(quote <| arity + 1) :=
+  --       $base
+  -- )
+
+  -- elabCommandAndTrace
+  --   (header := m!"elaborating *curried* base functor {baseIdExt} …") <|← `(
+  --     abbrev $baseIdExt $view.deadBinders:bracketedBinder* :=
+  --       TypeFun.curried $baseApplied
+  -- )
+
+  -- elabCommandAndTrace
+  --   (header := m!"elaborating qpf instance for {baseIdent} …") <|← `(
+  --     instance $baseQPFIdent:ident : MvQPF ($baseApplied) := $q
+  -- )
+
+  -- elabCommandAndTrace
+  --   (header := m!"elaborating uncurried (co)fixpoint {uncurriedIdent} …") <|← `(
+  --     abbrev $uncurriedIdent:ident $view.deadBinders:bracketedBinder* :
+  --         TypeFun $(quote arity) :=
+  --       $fix_or_cofix $base
+  -- )
+
+  -- elabCommandAndTrace
+  --   (header := m!"elaborating *curried* (co)fixpoint {view.declId} …")  <|← `(
+  --     abbrev $(view.declId) $view.deadBinders:bracketedBinder* :=
+  --       TypeFun.curried $uncurriedApplied
+  -- )
 
 open Macro Comp in
 /--
@@ -453,7 +454,7 @@ def elabData : CommandElab := fun stx =>
   let _ ← eff
 
   /- Composition pipeline -/
-  let base ← elabQpfCompositionBody {
+  let ⟨u, n, base⟩ ← elabQpfCompositionBody {
     liveBinders := nonRecView.liveBinders,
     deadBinders := nonRecView.deadBinders,
     type?   := none,

Qpf/Macro/QpfExpr.lean

@@ -8,6 +8,7 @@ import Mathlib.Data.QPF.Multivariate.Constructions.Cofix
 import Mathlib.Data.QPF.Multivariate.Constructions.Fix
 
 import Qpf.Util.TypeFun
+import Qpf.Macro.Common
 
 /-!
 ## QpfExpr
@@ -17,7 +18,7 @@ the corresponding `MvQPF` instance, and define methods for the various
 constructions under which QPFs are closed ((co)fixpoints, composition, etc.).
 -/
 
-open Lean Qq
+open Lean Qq Macro
 
 /-- A Lean expression of type `TypeFun n`, with a bundled `MvQPF` instance -/
 inductive QpfExpr (u : Level) (n : Nat)
@@ -187,28 +188,39 @@ def qpfInstance {n : Nat} : (q : QpfExpr' u n) → Q(MvQPF $q.typeFun)
 
 /-! ### Environment Manipulation -/
 
-variable {m} [Monad m] [MonadLiftT CoreM m]
 /-- Add the typefunction of a `QpfExpr'` to the environment under the given
 name, together with the corresponding QPF instance as `$name.instMvQPF`. -/
 def addToEnvironment
     (e : QpfExpr' u n)
     (name : Name) (levelParams : List Name)
     (hints : ReducibilityHints := .regular 0)
     (safety : DefinitionSafety := .safe)
-    : m Unit := do
-  addAndCompile <| Declaration.defnDecl {
-    name,
-    levelParams
-    type := q(TypeFun.{u, u} $n)
-    value := e.typeFun
-    hints, safety
-  }
-  let F : Q(TypeFun.{u, u} $n) :=
-    Expr.const name (levelParams.map Level.param)
-  addAndCompile <| Declaration.defnDecl {
-    name := Name.str name "instMvQPF"
-    levelParams := levelParams
-    type := q(MvQPF $F)
-    value := e.qpfInstance
-    hints, safety
-  }
+    : MetaM Unit :=
+  withQPFTraceNode m!"adding QpfExpr {name} to environment" <| do
+
+  let levelParams := match (← instantiateLevelMVars u) with
+    | .mvar id =>
+    _
+    | .param u => u :: levelParams
+    | _ => levelParams
+
+  withQPFTraceNode m!"uncurried declaration ({name}): …" <| do
+    let type := q(TypeFun.{u, u} $n)
+    trace[QPF] m!"value := {e.typeFun}"
+    trace[QPF] m!"type  := {type}"
+    addAndCompile <| Declaration.defnDecl {
+      name,
+      levelParams,
+      type,
+      value := e.typeFun
+      hints, safety
+    }
+  -- let F : Q(TypeFun.{u, u} $n) :=
+  --   Expr.const name (levelParams.map Level.param)
+  -- addAndCompile <| Declaration.defnDecl {
+  --   name := Name.str name "instMvQPF"
+  --   levelParams := levelParams
+  --   type := q(MvQPF $F)
+  --   value := e.qpfInstance
+  --   hints, safety
+  -- }

Test/Comp.lean

@@ -8,7 +8,13 @@ import Qpf
   # Composition pipeline
 -/
 
+set_option trace.QPF true
 qpf P₁ α β := α
+#check P₁
+#check P₁.Uncurried
+
+#exit
+
 qpf P₂ α β := β
 
 qpf C₁ α β := Nat