diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean index 44c09a9..2fff009 100644 --- a/Pantograph/Delate.lean +++ b/Pantograph/Delate.lean @@ -119,11 +119,11 @@ partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := if args.size < fvars.size then throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}" - --if !args.isEmpty then - --IO.println s!"{padding}├── Arguments Begin" + if !args.isEmpty then + trace[Pantograph.Delate] "─ Arguments Begin" let args ← args.mapM self - --if !args.isEmpty then - --IO.println s!"{padding}├── Arguments End" + if !args.isEmpty then + trace[Pantograph.Delate] "─ Arguments End" if !(← mvarIdPending.isAssignedOrDelayedAssigned) then trace[Pantograph.Delate] "T1" let result := mkAppN f args @@ -141,18 +141,18 @@ partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := else assert! !(← mvarId.isAssigned) assert! !(← mvarId.isDelayedAssigned) - --if !args.isEmpty then - -- IO.println s!"{padding}├── Arguments Begin" + if !args.isEmpty then + trace[Pantograph.Delate] "─ Arguments Begin" let args ← args.mapM self - --if !args.isEmpty then - -- IO.println s!"{padding}├── Arguments End" + if !args.isEmpty then + trace[Pantograph.Delate] "─ Arguments End" trace[Pantograph.Delate] "M ?{mvarId.name}" return .done (mkAppN f args)) trace[Pantoraph.Delate] "Result {result}" return result where - self e := instantiateDelayedMVars e --(level := level + 1) + self e := instantiateDelayedMVars e /-- Convert an expression to an equiavlent form with diff --git a/Pantograph/Frontend/MetaTranslate.lean b/Pantograph/Frontend/MetaTranslate.lean index c6592d2..8067d17 100644 --- a/Pantograph/Frontend/MetaTranslate.lean +++ b/Pantograph/Frontend/MetaTranslate.lean @@ -62,7 +62,7 @@ private partial def translateExpr (srcExpr: Expr) : MetaTranslateM Expr := do let sourceMCtx ← getSourceMCtx -- We want to create as few mvars as possible let (srcExpr, _) := instantiateMVarsCore (mctx := sourceMCtx) srcExpr - --IO.println s!"Transform src: {srcExpr}" + trace[Pantograph.Frontend.MetaTranslate] "Transform src: {srcExpr}" let result ← Core.transform srcExpr λ e => do let state ← get match e with @@ -100,10 +100,10 @@ partial def translateLocalDecl (srcLocalDecl: LocalDecl) : MetaTranslateM LocalD addTranslatedFVar srcLocalDecl.fvarId fvarId match srcLocalDecl with | .cdecl index _ userName type bi kind => do - --IO.println s!"[CD] {userName} {toString type}" + trace[Pantograph.Frontend.MetaTranslate] "[CD] {userName} {toString type}" return .cdecl index fvarId userName (← translateExpr type) bi kind | .ldecl index _ userName type value nonDep kind => do - --IO.println s!"[LD] {toString type} := {toString value}" + trace[Pantograph.Frontend.MetaTranslate] "[LD] {toString type} := {toString value}" return .ldecl index fvarId userName (← translateExpr type) (← translateExpr value) nonDep kind partial def translateLCtx : MetaTranslateM LocalContext := do @@ -162,4 +162,7 @@ end MetaTranslate export MetaTranslate (MetaTranslateM) +initialize + registerTraceClass `Pantograph.Frontend.MetaTranslate + end Pantograph.Frontend