VCGen Planner Core

Shared planning infrastructure for the unary and relational VCGen tactics.

opaque OracleComp.ProgramLogic.vcvio.vcgen.maxPasses : Lean.Option ℕ

opaque OracleComp.ProgramLogic.vcvio.vcgen.traceSteps : Lean.Option Bool

opaque OracleComp.ProgramLogic.vcvio.vcgen.time : Lean.Option Bool

opaque OracleComp.ProgramLogic.vcvio.vcgen.traceCachedRules : Lean.Option Bool

structure OracleComp.ProgramLogic.VCGenTimingData : Type

• previewNs : UInt64
• structuralNs : UInt64
• wpStepNs : UInt64
• probPlannerNs : UInt64
• localHintNs : UInt64
• registeredNs : UInt64
• cachedRuleBuildNs : UInt64
• cachedRuleHits : ℕ
• cachedRuleMisses : ℕ
• closeNs : UInt64
• passNs : UInt64
• finishNs : UInt64

@[implicit_reducible]

instance OracleComp.ProgramLogic.instInhabitedVCGenTimingData : Inhabited VCGenTimingData

def OracleComp.ProgramLogic.instInhabitedVCGenTimingData.default : VCGenTimingData

opaque OracleComp.ProgramLogic.vcGenTimingRef : IO.Ref VCGenTimingData

def OracleComp.ProgramLogic.timeNs {m : Type → Type} {α : Type} [Monad m] [MonadLiftT BaseIO m] (k : m α) : m (α × UInt64)

def OracleComp.ProgramLogic.addCachedRuleBuildTime (ns : UInt64) : BaseIO Unit

def OracleComp.ProgramLogic.addCachedRuleHit : BaseIO Unit

def OracleComp.ProgramLogic.addCachedRuleMiss : BaseIO Unit

def OracleComp.ProgramLogic.withVCGenTiming {α : Type} (add : UInt64 → BaseIO Unit) (k : Lean.Elab.Tactic.TacticM α) : Lean.Elab.Tactic.TacticM α

def OracleComp.ProgramLogic.withVCGenPreviewTiming {α : Type} (k : Lean.Elab.Tactic.TacticM α) : Lean.Elab.Tactic.TacticM α

def OracleComp.ProgramLogic.withVCGenStructuralTiming {α : Type} (k : Lean.Elab.Tactic.TacticM α) : Lean.Elab.Tactic.TacticM α

def OracleComp.ProgramLogic.withVCGenWpStepTiming {α : Type} (k : Lean.Elab.Tactic.TacticM α) : Lean.Elab.Tactic.TacticM α

def OracleComp.ProgramLogic.withVCGenProbPlannerTiming {α : Type} (k : Lean.Elab.Tactic.TacticM α) : Lean.Elab.Tactic.TacticM α

def OracleComp.ProgramLogic.withVCGenLocalHintTiming {α : Type} (k : Lean.Elab.Tactic.TacticM α) : Lean.Elab.Tactic.TacticM α

def OracleComp.ProgramLogic.withVCGenRegisteredTiming {α : Type} (k : Lean.Elab.Tactic.TacticM α) : Lean.Elab.Tactic.TacticM α

def OracleComp.ProgramLogic.withVCGenCloseTiming {α : Type} (k : Lean.Elab.Tactic.TacticM α) : Lean.Elab.Tactic.TacticM α

def OracleComp.ProgramLogic.withVCGenPassTiming {α : Type} (k : Lean.Elab.Tactic.TacticM α) : Lean.Elab.Tactic.TacticM α

def OracleComp.ProgramLogic.withVCGenFinishTiming {α : Type} (k : Lean.Elab.Tactic.TacticM α) : Lean.Elab.Tactic.TacticM α

def OracleComp.ProgramLogic.resetVCGenTimingIfEnabled : Lean.Elab.Tactic.TacticM Unit

def OracleComp.ProgramLogic.logVCGenTimingIfEnabled (label : String) : Lean.Elab.Tactic.TacticM Unit

def OracleComp.ProgramLogic.withVCGenRunTiming {α : Type} (label : String) (k : Lean.Elab.Tactic.TacticM α) : Lean.Elab.Tactic.TacticM α

structure OracleComp.ProgramLogic.PlannedStep : Type

• label : String
• replayText : String
• run : Lean.Elab.Tactic.TacticM Bool
• notes : List String

structure OracleComp.ProgramLogic.PreviewResult : Type

• ok : Bool
• goalCount : ℕ

def OracleComp.ProgramLogic.withStepNotes (step : PlannedStep) (notes : List String) : PlannedStep

def OracleComp.ProgramLogic.formatCandidateNames (names : Array Lean.Name) : String

def OracleComp.ProgramLogic.previewAction (action : Lean.Elab.Tactic.TacticM Bool) : Lean.Elab.Tactic.TacticM Bool

def OracleComp.ProgramLogic.previewActionWithGoals (action : Lean.Elab.Tactic.TacticM Bool) : Lean.Elab.Tactic.TacticM PreviewResult

def OracleComp.ProgramLogic.previewPlannedStep (step : PlannedStep) : Lean.Elab.Tactic.TacticM Bool

def OracleComp.ProgramLogic.previewPlannedStepWithGoals (step : PlannedStep) : Lean.Elab.Tactic.TacticM PreviewResult

def OracleComp.ProgramLogic.renderPlannedStepPreview (step : PlannedStep) (preview : PreviewResult) : String

def OracleComp.ProgramLogic.attachPlannerChoiceNotes (step : PlannedStep) (preview : PreviewResult) (alternatives : Array String) : PlannedStep

def OracleComp.ProgramLogic.chooseBestPlannedStepCandidate? (steps : Array PlannedStep) : Lean.Elab.Tactic.TacticM (Option (PlannedStep × PreviewResult))

def OracleComp.ProgramLogic.logPlannedStep (step : PlannedStep) (beforeGoals afterGoals : ℕ) : Lean.Elab.Tactic.TacticM Unit

def OracleComp.ProgramLogic.executePlannedStep (step : PlannedStep) : Lean.Elab.Tactic.TacticM Bool

def OracleComp.ProgramLogic.renderPassReplayLine (steps : Array PlannedStep) : Option String

def OracleComp.ProgramLogic.whnfReducible (e : Lean.Expr) : Lean.MetaM Lean.Expr

def OracleComp.ProgramLogic.headConstName? (e : Lean.Expr) : Option Lean.Name

def OracleComp.ProgramLogic.trailingArgs? (e : Lean.Expr) (n : ℕ) : Option (Array Lean.Expr)

def OracleComp.ProgramLogic.findAppWithHead? (head : Lean.Name) (e : Lean.Expr) : Option Lean.Expr

def OracleComp.ProgramLogic.relTripleGoalParts? (target : Lean.Expr) : Option (Lean.Expr × Lean.Expr × Lean.Expr)

def OracleComp.ProgramLogic.relWPGoalParts? (target : Lean.Expr) : Option (Lean.Expr × Lean.Expr × Lean.Expr)

def OracleComp.ProgramLogic.stdDoRelTripleGoalParts? (target : Lean.Expr) : Option (Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr)

def OracleComp.ProgramLogic.wpGoalComp? (target : Lean.Expr) : Option Lean.Expr

def OracleComp.ProgramLogic.wpGoalParts? (target : Lean.Expr) : Option (Lean.Expr × Lean.Expr)

def OracleComp.ProgramLogic.rawWPGoalParts? (target : Lean.Expr) : Option (Lean.Expr × Lean.Expr × Lean.Expr)

def OracleComp.ProgramLogic.tripleGoalComp? (target : Lean.Expr) : Option Lean.Expr

def OracleComp.ProgramLogic.tripleGoalParts? (target : Lean.Expr) : Option (Lean.Expr × Lean.Expr × Lean.Expr)

def OracleComp.ProgramLogic.isSimulateQAction (e : Lean.Expr) : Bool

def OracleComp.ProgramLogic.hasStateTRunExpr (e : Lean.Expr) : Bool

def OracleComp.ProgramLogic.hasStateTRun'Expr (e : Lean.Expr) : Bool

def OracleComp.ProgramLogic.hasStateTRunLike (e : Lean.Expr) : Bool

def OracleComp.ProgramLogic.hasSimulateQRunLike (e : Lean.Expr) : Bool

def OracleComp.ProgramLogic.isEqRelPost (e : Lean.Expr) : Bool

def OracleComp.ProgramLogic.isBindExpr (e : Lean.Expr) : Bool

def OracleComp.ProgramLogic.isPureExpr (e : Lean.Expr) : Bool

def OracleComp.ProgramLogic.isIfExpr (e : Lean.Expr) : Bool

def OracleComp.ProgramLogic.isMapExpr (e : Lean.Expr) : Bool

def OracleComp.ProgramLogic.isReplicateExpr (e : Lean.Expr) : Bool

def OracleComp.ProgramLogic.isListMapMExpr (e : Lean.Expr) : Bool

def OracleComp.ProgramLogic.isListFoldlMExpr (e : Lean.Expr) : Bool

def OracleComp.ProgramLogic.isReplicateHead (e : Lean.Expr) : Bool

def OracleComp.ProgramLogic.isListMapMHead (e : Lean.Expr) : Bool

def OracleComp.ProgramLogic.isListFoldlMHead (e : Lean.Expr) : Bool

def OracleComp.ProgramLogic.isGameEquivGoal (target : Lean.Expr) : Bool

def OracleComp.ProgramLogic.isEvalDistEqGoal (target : Lean.Expr) : Bool

def OracleComp.ProgramLogic.isProbEqGoal (target : Lean.Expr) : Bool

Check if a goal is an equality with probability expressions on both sides.

def OracleComp.ProgramLogic.tryEvalTacticSyntax (stx : Lean.Syntax) : Lean.Elab.Tactic.TacticM Bool

def OracleComp.ProgramLogic.focusFirstGoalSatisfying (pred : Lean.Expr → Bool) : Lean.Elab.Tactic.TacticM Bool

def OracleComp.ProgramLogic.runBoundedPasses (label : String) (step : Lean.Elab.Tactic.TacticM Bool) : Lean.Elab.Tactic.TacticM ℕ

def OracleComp.ProgramLogic.runBoundedPassesCollect {α : Type} (label : String) (step : Lean.Elab.Tactic.TacticM (Array α)) : Lean.Elab.Tactic.TacticM (Array (Array α))