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

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.eRelTripleGoalParts? (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 α))

def OracleComp.ProgramLogic.runWpStepRules : Lean.Elab.Tactic.TacticM Bool