WIP: stash commit

Qpf/Macro/Comp.lean

@@ -66,16 +66,16 @@ def synthQPF {n : Nat} (F : Q(TypeFun.{u,u} $n)) (_ : Q(MvFunctor $F)) : MetaM Q
 -/
 protected partial def parseApp (isLiveVar : FVarId → Bool) (F : Q(Type u)) :
     TermElabM ((n : Nat) × Q(TypeFun.{u,u} $n) × Vector Expr n) :=
-  if F.isApp then
-    /-
-      HACK: Technically `F` is *not* an instance of `CurriedTypeFun 0`.
-      However, we know that it is an application, and we only check the type after
-      deconstructing the application
-    -/
-    parseAppAux F ⟨[], rfl⟩ none
-  else
-    throwError "application expected:\n {F}"
-
+  withQPFTraceNode m!"decomposing {F}" <| do
+    if F.isApp then
+      /-
+        HACK: Technically `F` is *not* an instance of `CurriedTypeFun 0`.
+        However, we know that it is an application, and we only check the type after
+        deconstructing the application
+      -/
+      parseAppAux F ⟨[], rfl⟩ none
+    else
+      throwError "application expected:\n {F}"
 where
   parseAppAux : {n : Nat} → Q(CurriedTypeFun.{u,u} $n) → Vector Expr n → Option Exception → _
   | depth', Expr.app F a, args', _ => do
@@ -208,8 +208,8 @@ structure QpfCompositionBinders where
   Given the description of a QPF composition (`QpfCompositionView`), generate the syntax for a term
   that represents the desired functor (in uncurried form)
 -/
-def elabQpfCompositionBody (view: QpfCompositionBodyView) :
-      CommandElabM (Term × Term) := do
+def elabQpfCompositionBody (view : QpfCompositionBodyView) :
+      CommandElabM (Σ u n, QpfExpr' u n) := do
   withQPFTraceNode "composition pipeline"
     (tag := "elabQpfCompositionBody") <| do
 
@@ -231,7 +231,7 @@ def elabQpfCompositionBody (view: QpfCompositionBodyView) :
         mkFreshLevelMVar
 
     withAutoBoundImplicit <|
-    elabBinders view.deadBinders fun _deadVars =>
+    elabBinders view.deadBinders fun deadVars =>
     withLiveBinders view.liveBinders fun vars =>
     withoutAutoBoundImplicit <| do
       let target_expr ← elabTermEnsuringTypeQ (u:=u.succ.succ) view.target q(Type u)
@@ -243,16 +243,10 @@ def elabQpfCompositionBody (view: QpfCompositionBodyView) :
 
       let res ← elabQpf vars target_expr view.target
       res.check
-
-      withOptions (fun opt => opt.insert `pp.explicit true) <| do
-        let F ← delab res.typeFun
-        let qpf ← delab res.qpfInstance
-
-        withQPFTraceNode "results …" <| do
-          trace[QPF] "Functor := {F}"
-          trace[QPF] "MvQPF instance := {qpf}"
-        return ⟨F, qpf⟩
-
+      withQPFTraceNode "results …" <| do
+        trace[QPF] "{res}"
+      let res ← res.mkLambdaFVars deadVars
+      return ⟨_, _, res⟩
 
 structure QpfCompositionView where
   (modifiers  : Modifiers := {})
@@ -261,6 +255,7 @@ 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
@@ -274,7 +269,7 @@ def elabQpfComposition (view: QpfCompositionView) : CommandElabM Unit := do
   /-
     Elaborate body
   -/
-  let ⟨body, qpf⟩ ← elabQpfCompositionBody {
+  let ⟨_, _, qpfExpr⟩ ← elabQpfCompositionBody {
     type?   := view.type?
     target  := view.target
     liveBinders,
@@ -284,48 +279,52 @@ def elabQpfComposition (view: QpfCompositionView) : CommandElabM Unit := do
   /-
     Define the qpf using the elaborated body
   -/
-  let F_internal := mkIdent $ Name.mkStr view.F "Uncurried";
-  let F := mkIdent view.F;
-  let modifiers := quote (k := ``declModifiers) view.modifiers;
-
-  let live_arity := mkNumLit liveBinders.size.repr;
-  trace[QPF] "body: {body}"
-  elabCommand <|← `(
-      $modifiers:declModifiers
-      def $F_internal:ident $deadBinders:bracketedBinder* :
-        TypeFun $live_arity :=
-      $body:term
-  )
-
-  let deadBinderNamedArgs ← deadBinderNames.mapM fun n => `(Parser.Term.namedArgument| ($n:ident := $n:term))
-  let F_internal_applied ← `($F_internal $deadBinderNamedArgs:namedArgument*)
-
-
-  let cmd ← `(
-      $modifiers:declModifiers
-      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
-  )
-  trace[QPF] "cmd₂: {cmd}"
-  elabCommand cmd
+  let F_internal := Name.mkStr view.F "Uncurried";
+  let F := view.F;
+
+
+  qpfExpr.addToEnvironment F_internal []
+  return ()
+  -- let modifiers := quote (k := ``declModifiers) view.modifiers;
+
+  -- let live_arity := mkNumLit liveBinders.size.repr;
+  -- trace[QPF] "body: {body}"
+  -- elabCommand <|← `(
+  --     $modifiers:declModifiers
+  --     def $F_internal:ident $deadBinders:bracketedBinder* :
+  --       TypeFun $live_arity :=
+  --     $body:term
+  -- )
+
+  -- let deadBinderNamedArgs ← deadBinderNames.mapM fun n => `(Parser.Term.namedArgument| ($n:ident := $n:term))
+  -- let F_internal_applied ← `($F_internal $deadBinderNamedArgs:namedArgument*)
+
+
+  -- let cmd ← `(
+  --     $modifiers:declModifiers
+  --     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
+  -- )
+  -- trace[QPF] "cmd₂: {cmd}"
+  -- elabCommand cmd
 
 
 

Qpf/Macro/QpfExpr.lean

@@ -32,6 +32,13 @@ inductive QpfExpr (u : Level) (n : Nat)
   -/
 deriving Inhabited
 
+/-- An analogue of `QpfExpr`, where the expressions have the same types,
+*except* that they may be prefixed by a sequence of lambdas
+(i.e., dead variables) -/
+inductive QpfExpr' (u : Level) (n : Nat)
+  | qpf (F : Expr) (qpf : Expr)
+  deriving Inhabited
+
 /-! ## Preliminaries -/
 section ToExpr
 
@@ -78,7 +85,6 @@ def typeFun {n : Nat} : QpfExpr u n → Q(TypeFun.{u, u} $n)
 def qpfInstance {n : Nat} : (q : QpfExpr u n) → Q(MvQPF $q.typeFun)
   | qpf _ q => q
 
-
 variable {m} [Monad m] [MonadLiftT MetaM m] in
 /-- Construct a `QPFExpr` from an expression of type `TypeFun n`, by
 synthesizing the corresponding MvQPF instance.
@@ -102,6 +108,14 @@ def check : QpfExpr u n → MetaM Unit
     F.check
     q.check
 
+/-- Call `Meta.mkLambdaFVars xs` on the constituent expressions,
+returning a `QpfExpr'` -/
+def mkLambdaFVars (xs : Array Expr) : QpfExpr u n → MetaM (QpfExpr' u n)
+  | qpf F q => do
+    let F ← Meta.mkLambdaFVars xs F
+    let q ← Meta.mkLambdaFVars xs q
+    return .qpf F q
+
 /-! ## Tracing-/
 
 def toMessageData : QpfExpr u n → MessageData
@@ -151,6 +165,50 @@ def comp (F : QpfExpr u n) (Gs : Vec (QpfExpr u m) n) : QpfExpr u m :=
 
   let comp := q(@MvQPF.Comp $n _ $F.typeFun $GExpr)
   let qpfInstance := q(
-    @instMvQPFComp (q := $F.qpfInstance) (qG := $GQpf)
+    instMvQPFComp (q := $F.qpfInstance) (qG := $GQpf)
   )
   qpf comp qpfInstance
+
+end QpfExpr
+
+/-! ## QpfExpr' -/
+
+namespace QpfExpr'
+
+/-! ### Basic Fields -/
+
+/-- The raw type function, i.e., an expression of type `TypeFun n` -/
+def typeFun {n : Nat} : QpfExpr' u n → Q(TypeFun.{u, u} $n)
+  | qpf F _ => F
+
+/-- The bundled QPF instance, i.e., an expression of type `MvQPF ($typeFun)` -/
+def qpfInstance {n : Nat} : (q : QpfExpr' u n) → Q(MvQPF $q.typeFun)
+  | qpf _ q => q
+
+/-! ### 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
+  }

Test/Comp.lean

@@ -1,7 +1,7 @@
 import Qpf
-import Test.List
+-- import Test.List
 
-open Test
+-- open Test
 
 
 /-
@@ -14,4 +14,4 @@ qpf P₂ α β := β
 qpf C₁ α β := Nat
 qpf C₂ (n : Nat) α β := PFin2 n
 
-qpf G₄ α β ρ := QpfList ρ
+qpf G₄ α β ρ := QpfList ρ

Test/DeadWrap.lean

@@ -5,6 +5,7 @@ import Qpf
 
 namespace Test
 
+set_option trace.QPF true
 data DeadWrap (α : Type) β
   | mk : α → DeadWrap α β