Generic small-step evaluator

RunConfig mirrors Config but is parameterized by a generic state type S instead of Env P, so that concrete interpreters (e.g. Core) can thread their own rich environment through the stepper.

inductive Imperative.RunConfig (P : PureExpr) (CmdT S : Type) : Type

Configuration for the generic stepper, parameterized by state S.

• stmt {P : PureExpr} {CmdT S : Type} : Stmt P CmdT → S → RunConfig P CmdT S
• stmts {P : PureExpr} {CmdT S : Type} : List (Stmt P CmdT) → S → RunConfig P CmdT S
• terminal {P : PureExpr} {CmdT S : Type} : S → RunConfig P CmdT S
• exiting {P : PureExpr} {CmdT S : Type} : String → S → RunConfig P CmdT S
• block {P : PureExpr} {CmdT S : Type} : String → RunConfig P CmdT S → RunConfig P CmdT S
• seq {P : PureExpr} {CmdT S : Type} : RunConfig P CmdT S → List (Stmt P CmdT) → RunConfig P CmdT S

def Imperative.RunConfig.state {P : PureExpr} {CmdT S : Type} : RunConfig P CmdT S → S

Equations

• (Imperative.RunConfig.stmt a s).state = s
• (Imperative.RunConfig.stmts a s).state = s
• (Imperative.RunConfig.terminal s).state = s
• (Imperative.RunConfig.exiting a s).state = s
• (Imperative.RunConfig.block a inner).state = inner.state
• (inner.seq a).state = inner.state

structure Imperative.RunOps (P : PureExpr) (CmdT S : Type) : Type

Operations the stepper needs from the state.

• evalExpr : S → P.Expr → Option P.Expr

  Evaluate a expression to a value.

• evalCmd : S → CmdT → S

  Execute a command, producing a new state.

• extendFactory : S → PureFunc P → S

  Extend the evaluator with a function declaration.

• pushScope : S → S

  Push a new variable scope (for blocks).

• popScope : S → S

  Pop a variable scope (for blocks).

• addError : S → String → S

  Produce a new state with an error

• hasError : S → Bool

  Check if the state has an error (to short-circuit execution).

def Imperative.runStep {P : PureExpr} {CmdT S : Type} [BEq P.Expr] [HasBool P] (ops : RunOps P CmdT S) (c : RunConfig P CmdT S) : RunConfig P CmdT S

Equations

• One or more equations did not get rendered due to their size.
• Imperative.runStep ops (Imperative.RunConfig.terminal a) = Imperative.RunConfig.terminal a
• Imperative.runStep ops (Imperative.RunConfig.exiting a a_1) = Imperative.RunConfig.exiting a a_1
• Imperative.runStep ops (Imperative.RunConfig.stmt (Imperative.Stmt.cmd cmd) ρ) = Imperative.RunConfig.terminal (ops.evalCmd ρ cmd)
• Imperative.runStep ops (Imperative.RunConfig.stmt (Imperative.Stmt.block label ss md) ρ) = Imperative.RunConfig.block label (Imperative.RunConfig.stmts ss (ops.pushScope ρ))
• Imperative.runStep ops (Imperative.RunConfig.stmt (Imperative.Stmt.ite Imperative.ExprOrNondet.nondet tss ess md) ρ) = Imperative.RunConfig.stmts tss ρ
• Imperative.runStep ops (Imperative.RunConfig.stmt (Imperative.Stmt.loop Imperative.ExprOrNondet.nondet measure invariants body md) ρ) = Imperative.RunConfig.terminal ρ
• Imperative.runStep ops (Imperative.RunConfig.stmt (Imperative.Stmt.exit label md) ρ) = Imperative.RunConfig.exiting label ρ
• Imperative.runStep ops (Imperative.RunConfig.stmt (Imperative.Stmt.funcDecl decl md) ρ) = Imperative.RunConfig.terminal (ops.extendFactory ρ decl)
• Imperative.runStep ops (Imperative.RunConfig.stmt (Imperative.Stmt.typeDecl tc md) ρ) = Imperative.RunConfig.terminal ρ
• Imperative.runStep ops (Imperative.RunConfig.stmts [] ρ) = Imperative.RunConfig.terminal ρ
• Imperative.runStep ops (Imperative.RunConfig.stmts (s :: ss) ρ) = if ops.hasError ρ = true then Imperative.RunConfig.terminal ρ else (Imperative.RunConfig.stmt s ρ).seq ss
• Imperative.runStep ops ((Imperative.RunConfig.terminal ρ').seq ss) = Imperative.RunConfig.stmts ss ρ'
• Imperative.runStep ops ((Imperative.RunConfig.exiting label ρ').seq ss) = Imperative.RunConfig.exiting label ρ'
• Imperative.runStep ops (inner.seq ss) = (Imperative.runStep ops inner).seq ss
• Imperative.runStep ops (Imperative.RunConfig.block label (Imperative.RunConfig.terminal ρ')) = Imperative.RunConfig.terminal (ops.popScope ρ')
• Imperative.runStep ops (Imperative.RunConfig.block label inner) = Imperative.RunConfig.block label (Imperative.runStep ops inner)

def Imperative.runStmt {P : PureExpr} {CmdT S : Type} [BEq P.Expr] [HasBool P] (ops : RunOps P CmdT S) (fuel : Nat) (c : RunConfig P CmdT S) : RunConfig P CmdT S

Equations

• Imperative.runStmt ops fuel (Imperative.RunConfig.terminal a) = Imperative.RunConfig.terminal a
• Imperative.runStmt ops 0 c = c
• Imperative.runStmt ops fuel_2.succ c = Imperative.runStmt ops fuel_2 (Imperative.runStep ops c)