Skip to content

Commit

Permalink
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat: structure trace with trace nodes
Browse files Browse the repository at this point in the history
This PR sprinkles `withTraceNode` liberally over the code base. This structures the traces into a hierarchy, making it much more readable.
alexkeizer committed Oct 9, 2024
1 parent 46b75a5 commit afd3b77
Showing 7 changed files with 249 additions and 163 deletions.
107 changes: 61 additions & 46 deletions Qpf/Macro/Common.lean
Original file line number Diff line number Diff line change
@@ -10,12 +10,25 @@ namespace Macro
registerTraceClass `QPF


variable [MonadControlT MetaM n] [Monad n] [MonadLiftT MetaM n]
variable [MonadControlT MetaM n] [Monad n] [MonadLiftT MetaM n]
[MonadError n] [MonadLog n] [AddMessageContext n]
[MonadQuotation n] [MonadTrace n] [MonadOptions n]
[MonadLiftT IO n]


[MonadLiftT IO n] [MonadAlwaysExcept ε n] [MonadLiftT BaseIO n]

/-- Add trace node with the `QPF` trace class -/
def withQPFTraceNode (header : MessageData) (k : n α)
(collapsed : Bool := true) (tag : String := "")
: n α := do
Lean.withTraceNode `QPF (fun _ => pure header) k collapsed tag

/-- Wrapper around `elabCommand` which first traces the command syntax
(in a `QPF` trace node), before elaborating the command -/
def elabCommandAndTrace (stx : Syntax)
(header : MessageData := "elaborating command …") :
CommandElabM Unit := do
withQPFTraceNode header <| do
trace[QPF] stx
Lean.Elab.Command.elabCommand stx

/--
Takes an expression `e` of type `CurriedTypeFun n` and returns an expression of type `TypeFun n`
@@ -34,20 +47,20 @@ namespace Macro
-- let F_inner ← mkFreshExprMVar (kind:=MetavarKind.synthetic) none
-- let us ← mkFreshLevelMVars 2
-- let app := mkApp2 (mkConst ``TypeFun.curried us) n F_inner

-- trace[QPF] "\nChecking defEq of {F} and {app}"
-- if (←isDefEq F app) then
-- if let some F' := (← getExprMVarAssignment? F_inner.mvarId!) then
-- trace[QPF] "yes: {F'}"
-- return F'

-- trace[QPF] "no"
-- mkAppM ``TypeFun.ofCurried #[F]



def withLiveBinders [Inhabited α]
(binders : Array Syntax)
(binders : Array Syntax)
(f : Array Expr → n α) : n α
:= do
let u := mkLevelSucc <|← mkFreshLevelMVar;
@@ -56,25 +69,27 @@ namespace Macro
α[0]
else
α
α.getId,
α.getId,
fun _ => pure (mkSort u)
)

withLocalDeclsD decls f



/--
Takes an array of bracketed binders, and allocate a fresh identifier for each hole in the binders.
Returns a pair of the binder syntax with all holes replaced, and an array of all bound identifiers,
both pre-existing and newly created
-/
def mkFreshNamesForBinderHoles (binders : Array Syntax) :
n ((TSyntaxArray ``bracketedBinder) × (Array Ident))
:= do
def mkFreshNamesForBinderHoles (binders : Array Syntax) :
n ((TSyntaxArray ``bracketedBinder) × (Array Ident)) :=
withQPFTraceNode "mkFreshNamesForBinderHoles"
(tag := "mkFreshNamesForBinderHoles") (collapsed := false) do

let mut bindersNoHoles := #[]
let mut binderNames := #[]

for stx in binders do
let mut newArgStx := Syntax.missing
let kind := stx.getKind
@@ -85,7 +100,7 @@ namespace Macro
-- let id := mkIdentFrom stx (← mkFreshBinderName)
-- binderNames := binderNames.push id
-- newArgStx := stx[1].setArgs #[id, Syntax.atom SourceInfo.none ":"]
else
else
trace[QPF] stx[1]
let id := stx[1][0]
binderNames := binderNames.push ⟨id⟩
@@ -100,11 +115,11 @@ namespace Macro
return id
else if kind == ``Lean.Parser.Term.hole then
return mkIdentFrom id (← mkFreshBinderName)
else
else
throwErrorAt id "identifier or `_` expected, found {kind}"

for id in ids do
binderNames := binderNames.push ⟨id⟩
binderNames := binderNames.push ⟨id⟩
newArgStx := stx[1].setArgs ids

let newStx := stx.setArg 1 newArgStx
@@ -125,12 +140,12 @@ namespace Macro
def BinderKind.ofSyntaxKind (kind : SyntaxNodeKind) : BinderKind :=
if kind == ``implicitBinder then
.implicit
else if kind == ``Lean.binderIdent
|| kind == ``Lean.Parser.Term.binderIdent
else if kind == ``Lean.binderIdent
|| kind == ``Lean.Parser.Term.binderIdent
|| kind == ``Lean.Parser.Term.ident
|| kind == ``Lean.Parser.ident
-- HACK: this one should be just a single backquote
|| kind == `ident
-- HACK: this one should be just a single backquote
|| kind == `ident
then
.ident
else if kind == ``explicitBinder then
@@ -142,10 +157,10 @@ namespace Macro
open Lean.Parser.Term in
/--
Takes a list of binders, and split it into live and dead binders, respectively.
For the live binders, return an array of with syntax of kind `binderIdent`, unwrapping
For the live binders, return an array of with syntax of kind `binderIdent`, unwrapping
`simpleBinder` nodes if needed (while asserting that there were no type annotations)
-/
def splitLiveAndDeadBinders (binders : Array Syntax)
def splitLiveAndDeadBinders (binders : Array Syntax)
: n (TSyntaxArray ``Lean.Parser.Term.binderIdent × TSyntaxArray ``bracketedBinder) := do
let mut liveVars := #[]
let mut deadBinders := #[]
@@ -156,7 +171,7 @@ namespace Macro

if kind == .ident then
isLive := true
liveVars := liveVars.push ⟨binder⟩
liveVars := liveVars.push ⟨binder⟩

-- else if kind == .explicit then
-- isLive := true
@@ -170,38 +185,38 @@ namespace Macro
else if isLive then
throwErrorAt binder f!"Unexpected bracketed binder, dead arguments must precede all live arguments.\nPlease reorder your arguments or mark this binder as live by removing brackets and/or type ascriptions"

else
else
deadBinders := deadBinders.push ⟨binder⟩

return (liveVars, deadBinders)








/--
Takes a list of binders, and returns an array of just the bound identifiers,
Takes a list of binders, and returns an array of just the bound identifiers,
for use in applications
-/
def getBinderIdents (binders : Array Syntax) (includeImplicits := true)
: Array Term :=
def getBinderIdents (binders : Array Syntax) (includeImplicits := true)
: Array Term :=
Id.run do
let mut idents : Array Term := #[]

for binder in binders do
let kind := BinderKind.ofSyntaxKind binder.getKind

if kind == .implicit && !includeImplicits then
continue

else if kind == .ident then
idents := idents.push ⟨binder⟩
idents := idents.push ⟨binder⟩

else
else
for id in binder[1].getArgs do
idents := idents.push ⟨id⟩
idents := idents.push ⟨id⟩


-- dbg_trace "idents = {idents}"
pure idents
@@ -212,10 +227,10 @@ namespace Macro
open Parser.Command in
instance : Quote Modifiers (k := ``declModifiers) where
quote mod :=
let isNoncomputable : Syntax :=
if mod.isNoncomputable then
let isNoncomputable : Syntax :=
if mod.isNoncomputable then
mkNode ``«noncomputable» #[mkAtom "noncomputable "]
else
else
mkNullNode

let visibility := match mod.visibility with
@@ -232,12 +247,12 @@ instance : Quote Modifiers (k := ``declModifiers) where
mkNullNode -- partial / nonrec
]


-- open Lean.Parser.Term in
-- elab "#dbg_syntax " t:term : command => do
-- dbg_trace t


-- open Lean.Parser.Term Elab.Command in
-- elab "#dbg_expr " t:term : command => do
-- let expr ← liftTermElabM none $ elabTerm t none
@@ -251,16 +266,16 @@ end Macro

-- set_option pp.raw true

-- open Lean in
-- open Lean in
-- elab "#dbg_ident" id:binderIdent : command => do
-- dbg_trace "{id}"
-- let id := id.raw
-- dbg_trace "kind: {id.getKind}"
-- dbg_trace "args: {id.getArgs}"
-- dbg_trace "args[0].getKind: {id.getArgs[0]!.getKind}"

-- #dbg_ident x
-- #dbg_ident _
-- #dbg_ident x
-- #dbg_ident _

-- example : ``Lean.binderIdent = ``Lean.Parser.Term.binderIdent :=
-- by rfl
-- example : ``Lean.binderIdent = ``Lean.Parser.Term.binderIdent :=
-- by rfl
51 changes: 30 additions & 21 deletions Qpf/Macro/Comp.lean
Original file line number Diff line number Diff line change
@@ -37,6 +37,8 @@ open Syntax
open Parser.Term (bracketedBinder)
open Parser.Command (declModifiers definition)

open Macro (withQPFTraceNode)

open Qq

-- TODO: make everything work without this compatibility coercion
@@ -275,12 +277,15 @@ structure QpfCompositionBinders where
-/
def elabQpfCompositionBody (view: QpfCompositionBodyView) :
CommandElabM (Term × Term) := do
trace[QPF] "elabQpfCompositionBody ::
type? := {view.type?}
target := {view.target}
liveBinders := {view.liveBinders}
deadBinders := {view.deadBinders}
"
withQPFTraceNode "composition pipeline"
(tag := "elabQpfCompositionBody") <| do

withQPFTraceNode "arguments" <| do
trace[QPF] "type? := {view.type?}"
trace[QPF] "target := {view.target}"
trace[QPF] "liveBinders := {view.liveBinders}"
trace[QPF] "deadBinders := {view.deadBinders}"

runTermElabM fun _ => do
let u : Level ←
if let some typeStx := view.type? then
@@ -293,25 +298,29 @@ def elabQpfCompositionBody (view: QpfCompositionBodyView) :
mkFreshLevelMVar

withAutoBoundImplicit <|
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)
let arity := vars.toList.length
let vars : Vector _ arity := ⟨vars.toList, rfl⟩
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)
let arity := vars.toList.length
let vars : Vector _ arity := ⟨vars.toList, rfl⟩

let some vars := vars.mmap Expr.fvarId? |
throwError "Expected all args to be fvars" -- TODO: throwErrorAt

let some vars := vars.mmap Expr.fvarId? |
throwError "Expected all args to be fvars" -- TODO: throwErrorAt
let res ← elabQpf vars target_expr view.target

let res ← elabQpf vars target_expr view.target
res.F.check
res.qpf.check

res.F.check
res.qpf.check
withOptions (fun opt => opt.insert `pp.explicit true) <| do
let F ← delab res.F
let qpf ← delab res.qpf

withOptions (fun opt => opt.insert `pp.explicit true) <| do
let F ← delab res.F
let qpf ← delab res.qpf
return ⟨F, qpf⟩
withQPFTraceNode "results …" <| do
trace[QPF] "Functor := {F}"
trace[QPF] "MvQPF instance := {qpf}"
return ⟨F, qpf⟩


structure QpfCompositionView where
142 changes: 79 additions & 63 deletions Qpf/Macro/Data.lean
Original file line number Diff line number Diff line change
@@ -14,6 +14,8 @@ open Elab (Modifiers elabModifiers)
open Parser.Term (namedArgument)
open PrettyPrinter (delab)

open Macro (withQPFTraceNode elabCommandAndTrace)

private def Array.enum (as : Array α) : Array (Nat × α) :=
(Array.range as.size).zip as

@@ -97,7 +99,8 @@ open Parser in
That is, it defines a type with exactly as many constructor as the input type, but such that
all constructors are constants (take no arguments).
-/
def mkHeadT (view : InductiveView) : CommandElabM Name := do
def mkHeadT (view : InductiveView) : CommandElabM Name :=
withQPFTraceNode "mkHeadT" (tag := "mkHeadT") <| do
-- If the original declId was `MyType`, we want to register the head type under `MyType.HeadT`
let (declName, declId, shortDeclName) ← addSuffixToDeclId view.declId "HeadT"

@@ -132,8 +135,8 @@ def mkHeadT (view : InductiveView) : CommandElabM Name := do
: InductiveView
}

trace[QPF] "mkHeadT :: elabInductiveViews"
elabInductiveViews #[view]
withQPFTraceNode "elabInductiveViews" <|
elabInductiveViews #[view]
pure declName

open Parser Parser.Term Parser.Command in
@@ -144,7 +147,9 @@ open Parser Parser.Term Parser.Command in
`ChildT a i` corresponds to the times that constructor `a` takes an argument of the `i`-th type
argument
-/
def mkChildT (view : InductiveView) (r : Replace) (headTName : Name) : CommandElabM Name := do
def mkChildT (view : InductiveView) (r : Replace) (headTName : Name) : CommandElabM Name :=
withQPFTraceNode "mkChildT" (tag := "mkChildT") <| do

-- If the original declId was `MyType`, we want to register the child type under `MyType.ChildT`
let (declName, declId, _shortDeclName) ← addSuffixToDeclId view.declId "ChildT"

@@ -164,14 +169,11 @@ def mkChildT (view : InductiveView) (r : Replace) (headTName : Name) : CommandEl
)
let headT := mkIdent headTName

let cmd ← `(
elabCommandAndTrace <|← `(
def $declId : $headT → $target_type
$body:declValEqns
)

-- trace[QPF] "mkChildT :: elabCommand"
elabCommand cmd

pure declName


@@ -181,6 +183,8 @@ open Parser.Term in
Show that the `Shape` type is a qpf, through an isomorphism with the `Shape.P` pfunctor
-/
def mkQpf (shapeView : InductiveView) (ctorArgs : Array CtorArgs) (headT P : Ident) (arity : Nat) : CommandElabM Unit := do
withQPFTraceNode "mkQPF" (tag := "mkQPF") <| do

let (shapeN, _) := Elab.expandDeclIdCore shapeView.declId
let eqv := mkIdent $ Name.mkStr shapeN "equiv"
let functor := mkIdent $ Name.mkStr shapeN "functor"
@@ -273,7 +277,7 @@ def mkQpf (shapeView : InductiveView) (ctorArgs : Array CtorArgs) (headT P : Ide
$unboxBody:matchAlt*
)

let cmd ← `(
elabCommandAndTrace <|← `(
def $eqv:ident {Γ} : (@TypeFun.ofCurried $(quote arity) $shape) Γ ≃ ($P).Obj Γ where
toFun := $box
invFun := $unbox
@@ -299,18 +303,8 @@ def mkQpf (shapeView : InductiveView) (ctorArgs : Array CtorArgs) (headT P : Ide
instance $q:ident : MvQPF.IsPolynomial (@TypeFun.ofCurried $(quote arity) $shape) :=
.ofEquiv $P $eqv
)
trace[QPF] "qpf: {cmd}\n"
elabCommand cmd

pure ()








/-! ## mkShape -/

structure MkShapeResult where
(r : Replace)
@@ -319,7 +313,9 @@ structure MkShapeResult where
(effects : CommandElabM Unit)

open Parser in
def mkShape (view: DataView) : TermElabM MkShapeResult := do
def mkShape (view : DataView) : TermElabM MkShapeResult :=
withQPFTraceNode "mkShape" (tag := "mkShape") <| do

-- If the original declId was `MyType`, we want to register the shape type under `MyType.Shape`
let (declName, declId, shortDeclName) ← addSuffixToDeclId view.declId "Shape"

@@ -329,16 +325,16 @@ def mkShape (view: DataView) : TermElabM MkShapeResult := do
let ((ctors, ctorArgs), r) ← Replace.shapeOfCtors view shapeIdent
let ctors := ctors.map (CtorView.declReplacePrefix view.declName declName)

trace[QPF] "mkShape :: r.getBinders = {←r.getBinders}"
trace[QPF] "mkShape :: r.expr = {r.expr}"
trace[QPF] "r.getBinders = {←r.getBinders}"
trace[QPF] "r.expr = {r.expr}"

-- Assemble it back together, into the shape inductive type
let binders ← r.getBinders
let binders := view.binders.setArgs #[binders]
let modifiers : Modifiers := {
isUnsafe := view.modifiers.isUnsafe
}
let view := {
let view : InductiveView := {
ctors, declId, declName, shortDeclName, modifiers, binders,
levelNames := []

@@ -350,10 +346,12 @@ def mkShape (view: DataView) : TermElabM MkShapeResult := do
: InductiveView
}

trace[QPF] "mkShape :: elabInductiveViews :: binders = {view.binders}"

withQPFTraceNode "shape view …" <| do
trace[QPF] m!"{view}"
let PName := Name.mkStr declName "P"
return ⟨r, declName, PName, do
withQPFTraceNode "mkShape effects" <| do

elabInductiveViews #[view]

let headTName ← mkHeadT view
@@ -372,7 +370,7 @@ def mkShape (view: DataView) : TermElabM MkShapeResult := do
let headTId := mkIdent headTName
let childTId := mkIdent childTName

elabCommand <|<- `(
elabCommandAndTrace <| `(
def $PDeclId:declId :=
MvPFunctor.mk $headTId $childTId
)
@@ -385,32 +383,35 @@ 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) := do
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] "isPolynomial::F = {F}"
let inst_type ← `(MvQPF.IsPolynomial $F:term)
trace[QPF] "isPolynomial :: inst_type_stx: {inst_type}"
let inst_type ← elabTerm inst_type none
trace[QPF] "isPolynomial :: inst_type: {inst_type}"

try
let _ ← synthInstance inst_func
let inst ← synthInstance inst_type
return some <|<- delab inst
catch e =>
trace[QPF] "{e.toMessageData}"
return none
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`
-/
def mkType (view : DataView) (base : Term × Term) : CommandElabM Unit := do
trace[QPF] "mkType"
def mkType (view : DataView) (base : Term × Term) : CommandElabM Unit :=
withQPFTraceNode m!"defining (co)datatype {view.declId}" (tag := "mkType") <| do

let uncurriedIdent ← addSuffixToDeclIdent view.declId "Uncurried"
let baseIdExt ← addSuffixToDeclIdent view.declId "Base"
let baseIdent ← addSuffixToDeclIdent baseIdExt "Uncurried"
@@ -425,30 +426,45 @@ def mkType (view : DataView) (base : Term × Term) : CommandElabM Unit := do
let fix_or_cofix := DataCommand.fixOrCofix view.command

let ⟨base, q⟩ := base
let cmd ← `(
abbrev $baseIdent:ident $view.deadBinders:bracketedBinder* : TypeFun $(quote <| arity + 1) :=
$base

abbrev $baseIdExt $view.deadBinders:bracketedBinder* :=
TypeFun.curried $baseApplied
elabCommandAndTrace
(header := m!"elaborating uncurried base functor {baseIdent} …") <|← `(
abbrev $baseIdent:ident $view.deadBinders:bracketedBinder* :
TypeFun $(quote <| arity + 1) :=
$base
)

instance $baseQPFIdent:ident : MvQPF ($baseApplied) := $q
elabCommandAndTrace
(header := m!"elaborating *curried* base functor {baseIdExt} …") <|← `(
abbrev $baseIdExt $view.deadBinders:bracketedBinder* :=
TypeFun.curried $baseApplied
)

abbrev $uncurriedIdent:ident $view.deadBinders:bracketedBinder* : TypeFun $(quote arity) := $fix_or_cofix $base
elabCommandAndTrace
(header := m!"elaborating qpf instance for {baseIdent} …") <|← `(
instance $baseQPFIdent:ident : MvQPF ($baseApplied) := $q
)

abbrev $(view.declId) $view.deadBinders:bracketedBinder*
:= TypeFun.curried $uncurriedApplied
elabCommandAndTrace
(header := m!"elaborating uncurried (co)fixpoint {uncurriedIdent} …") <|← `(
abbrev $uncurriedIdent:ident $view.deadBinders:bracketedBinder* :
TypeFun $(quote arity) :=
$fix_or_cofix $base
)

trace[QPF] "elabData.cmd = {cmd}"
elabCommand cmd
elabCommandAndTrace
(header := m!"elaborating *curried* (co)fixpoint {view.declId} …") <|← `(
abbrev $(view.declId) $view.deadBinders:bracketedBinder* :=
TypeFun.curried $uncurriedApplied
)

open Macro Comp in
/--
Top-level elaboration for both `data` and `codata` declarations
-/
@[command_elab declaration]
def elabData : CommandElab := fun stx => do
def elabData : CommandElab := fun stx =>
withQPFTraceNode "elabData" (tag := "elabData") (collapsed := false) <| do

let modifiers ← elabModifiers stx[0]
let decl := stx[1]

@@ -457,7 +473,6 @@ def elabData : CommandElab := fun stx => do

let (nonRecView, ⟨r, shape, _P, eff⟩) ← runTermElabM fun _ => do
let (nonRecView, _rho) ← makeNonRecursive view;
trace[QPF] "nonRecView: {nonRecView}"
pure (nonRecView, ←mkShape nonRecView)

/- Execute the `ComandElabM` side-effects prescribed by `mkShape` -/
@@ -472,14 +487,15 @@ def elabData : CommandElab := fun stx => do
$(mkIdent shape):ident $r.expr:term*
)
}
trace[QPF] "base = {base}"

mkType view base
mkConstructors view shape

if let .Data := view.command then
try genRecursors view
catch e => trace[QPF] (← e.toMessageData.toString)
catch e =>
trace[QPF] m!"Failed to generate recursors.\
\n\n{e.toMessageData}"


end Data.Command
16 changes: 9 additions & 7 deletions Qpf/Macro/Data/Constructors.lean
Original file line number Diff line number Diff line change
@@ -5,6 +5,8 @@ import Qpf.Macro.Data.View
open Lean Meta Elab Elab.Command
open PrettyPrinter (delab)

open Macro (withQPFTraceNode elabCommandAndTrace)

namespace Data.Command
open Parser in
/--
@@ -18,15 +20,16 @@ partial def countConstructorArgs : Syntax → Nat
Add definitions for constructors
that are generic across two input types shape and name.
Additionally we allow the user to control how names are generated.
Any binders passed in `binders` are added as parameters to the generated constructor
Any binders passed in `binders` are added as parameters to the generated constructor
-/
def mkConstructorsWithNameAndType
(view : DataView) (shape : Name)
(nameGen : CtorView → Name) (argTy retTy : Term)
(binders : TSyntaxArray ``Parser.Term.bracketedBinder := #[])
: CommandElabM Unit := do
for ctor in view.ctors do
trace[QPF] "mkConstructors\n{ctor.declName} : {ctor.type?}"
withQPFTraceNode "define constructor {ctor.declName}" <| do
trace[QPF] "type := {ctor.type?}"
let n_args := (ctor.type?.map countConstructorArgs).getD 0

let args := (← (List.range n_args).mapM
@@ -53,20 +56,19 @@ def mkConstructorsWithNameAndType
}
let declId := mkIdent $ nameGen ctor

let cmd ← `(
elabCommandAndTrace <|← `(
$(quote modifiers):declModifiers
def $declId:ident $binders*: $type := $body:term
)

trace[QPF] "mkConstructor.cmd = {cmd}"
elabCommand cmd

return

/--
Add convenient constructor functions to the environment
-/
def mkConstructors (view : DataView) (shape : Name) : CommandElabM Unit := do
def mkConstructors (view : DataView) (shape : Name) : CommandElabM Unit :=
withQPFTraceNode "deriving constructors" (tag := "mkConstructors") <| do

let explicit ← view.getExplicitExpectedType
let nameGen := (·.declName.replacePrefix (←getCurrNamespace) .anonymous)

30 changes: 11 additions & 19 deletions Qpf/Macro/Data/Ind.lean
Original file line number Diff line number Diff line change
@@ -8,6 +8,8 @@ open Lean.Parser (Parser)
open Lean Meta Elab.Command Elab.Term Parser.Term
open Lean.Parser.Tactic (inductionAlt)

open Macro (withQPFTraceNode elabCommandAndTrace)

def flattenForArg (n : Name) := Name.str .anonymous $ n.toStringWithSep "_" true

/-- Both `bracketedBinder` and `matchAlts` have optional arguments,
@@ -148,15 +150,18 @@ def generateRecBody (ctors : Array (Name × List RecursionForm)) (includeMotive

`(matchAltExprs| $deeper:matchAlt*)

def genRecursors (view : DataView) : CommandElabM Unit := do
def genRecursors (view : DataView) : CommandElabM Unit :=
withQPFTraceNode "attempting to generate recursors for datatype"
(tag := "genRecursors") <| do

let rec_type := view.getExpectedType

let mapped := view.ctors.map (RecursionForm.extractWithName view.declName · rec_type)

let ih_types ← mapped.mapM fun ⟨name, base⟩ =>
mkRecursorBinder (rec_type) (name) base true

let indDef : Command ← `(
elabCommandAndTrace (header := "elaborating induction principle …") <|← `(
@[elab_as_elim, induction_eliminator]
def $(view.shortDeclName ++ `ind |> mkIdent):ident
{ motive : $rec_type → Prop}
@@ -167,7 +172,7 @@ def genRecursors (view : DataView) : CommandElabM Unit := do
($(mkIdent `p) := motive)
(match ·,· with $(← generateIndBody mapped true)))

let recDef : Command ← `(
elabCommandAndTrace (header := "elaborating recursor …") <|← `(
@[elab_as_elim]
def $(view.shortDeclName ++ `rec |> mkIdent):ident
{ motive : $rec_type → Type _}
@@ -179,8 +184,8 @@ def genRecursors (view : DataView) : CommandElabM Unit := do
let casesOnTypes ← mapped.mapM fun ⟨name, base⟩ =>
mkRecursorBinder (rec_type) (name) base false

let casesDef : Command ← `(
@[elab_as_elim]
elabCommandAndTrace (header := "elaborating casesOn (Prop) eliminator …") <|← `(
@[elab_as_elim, cases_eliminator]
def $(view.shortDeclName ++ `cases |> mkIdent):ident
{ motive : $rec_type → Prop}
$casesOnTypes*
@@ -189,24 +194,11 @@ def genRecursors (view : DataView) : CommandElabM Unit := do
($(mkIdent `p) := motive)
(match ·,· with $(← generateIndBody mapped false)))

let casesTypeDef : Command ← `(
elabCommandAndTrace (header := "elaborating casesOn (Type _) eliminator …") <|← `(
@[elab_as_elim]
def $(view.shortDeclName ++ `casesType |> mkIdent):ident
{ motive : $rec_type → Type}
$casesOnTypes*
: (val : $rec_type) → motive val
:= $(mkIdent ``_root_.MvQPF.Fix.drec)
(match · with $(← generateRecBody mapped false)))

trace[QPF] "Rec definitions:"
trace[QPF] indDef
trace[QPF] recDef
Elab.Command.elabCommand indDef
Elab.Command.elabCommand recDef

trace[QPF] casesDef
trace[QPF] casesTypeDef
Elab.Command.elabCommand casesDef
Elab.Command.elabCommand casesTypeDef

pure ()
5 changes: 4 additions & 1 deletion Qpf/Macro/Data/Replace.lean
Original file line number Diff line number Diff line change
@@ -4,6 +4,7 @@ import Qpf.Macro.Common
import Qpf.Macro.Data.View

open Lean Meta Elab.Command Elab.Term
open Macro (withQPFTraceNode)

/-
This file contains the core "shape" extraction logic.
@@ -279,7 +280,8 @@ open Parser
Simultaneously checks that each constructor type, if given, is indeed a sequence of arrows
... → ... → ... culminating in the type to be defined.
-/
def makeNonRecursive (view : DataView) : MetaM (DataView × Name) := do
def makeNonRecursive (view : DataView) : MetaM (DataView × Name) :=
withQPFTraceNode "makeNonRecursive" <| do
let expected := view.getExpectedType

let rec ← mkFreshBinderName
@@ -292,4 +294,5 @@ def makeNonRecursive (view : DataView) : MetaM (DataView × Name) := do
return CtorView.withType? ctor type?

let view := view.setCtors ctors
trace[QPF] "non-recursive view: {view}"
pure (view, rec)
61 changes: 55 additions & 6 deletions Qpf/Macro/Data/View.lean
Original file line number Diff line number Diff line change
@@ -6,11 +6,10 @@ import Qpf.Macro.Common

open Lean
open Meta Elab Elab.Command

open Parser.Term (bracketedBinder)
open Parser.Command (declId)


open Macro (withQPFTraceNode)

inductive DataCommand where
| Data
@@ -140,16 +139,63 @@ def DataView.getExplicitExpectedType (view : DataView) : CommandElabM Term
@$(mkIdent view.shortDeclName):ident $args:term*
)

/-! ## MessageData -/

instance : ToMessageData CtorView where
toMessageData ctor := m!"\{\
modifiers := {ctor.modifiers},
declName := {ctor.declName},
binders := {ctor.binders},
type? := {ctor.type?},
}"

instance : ToMessageData InductiveView where
toMessageData view := m!"\{\
declId := {view.declId},
modifiers := {view.modifiers},
ref := {view.ref },
declId := {view.declId },
modifiers := {view.modifiers },
shortDeclName := {view.shortDeclName },
declName := {view.declName },
levelNames := {view.levelNames },
binders := {view.binders },
type? := {view.type?},
ctors := {view.ctors},
derivingClasses := <not able to be printed>,
}"

instance : ToMessageData DataView where
toMessageData view := m!"\{\
declId := {view.declId},
modifiers := {view.modifiers},
ref := {view.ref },
declId := {view.declId },
modifiers := {view.modifiers },
shortDeclName := {view.shortDeclName },
declName := {view.declName },
levelNames := {view.levelNames },
binders := {view.binders },
type? := {view.type?},
ctors := {view.ctors},
derivingClasses := <not able to be printed>,
command := {view.command },
liveBinders := {view.liveBinders },
deadBinders := {view.deadBinders },
deadBinderNames := {view.deadBinderNames },
}"


@[deprecated]
def CtorView.debug (ctor: CtorView) : String :=
s!"\{
(s!"\{
modifiers := {ctor.modifiers},
declName := {ctor.declName},
binders := {ctor.binders},
type? := {ctor.type?},
}"
}")

@[deprecated]
def DataView.debug (view : DataView) : String :=
let ctors := view.ctors.map CtorView.debug
s!"\{
@@ -210,7 +256,9 @@ def DataView.doSanityChecks (view : DataView) : CommandElabM Unit := do
/-
Heavily based on `inductiveSyntaxToView` from Lean.Elab.Declaration
-/
def dataSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM DataView := do
def dataSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM DataView :=
withQPFTraceNode "dataSyntaxToView" (tag := "dataSyntaxToView") <| do

-- `data`/`codata` declarations may be noncomputable (not sure about partial, but we allow it for now)
-- checkValidInductiveModifier modifiers

@@ -254,7 +302,8 @@ def dataSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM Data
binders, type?, ctors,
command, liveBinders, deadBinders, deadBinderNames
}
trace[Qpf.Data] "{view.debug}"
withQPFTraceNode "elaborated view …" <| do
trace[QPF] m!"{view}"

view.doSanityChecks
return view

0 comments on commit afd3b77

Please sign in to comment.