chore: Version 0.3 #136
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
Loading…
Reference in New Issue