VC Spec Intermediate Representation #

This module defines the intermediate representation used to classify and index program-logic specification rules for tactic lookup and compilation.

source

inductive OracleComp.ProgramLogic.VCSpecKind :

Type

unaryTriple : VCSpecKind
unaryWP : VCSpecKind
relTriple : VCSpecKind
relWP : VCSpecKind
eRelTriple : VCSpecKind

Instances For

source

def OracleComp.ProgramLogic.instInhabitedVCSpecKind.default :

VCSpecKind

Instances For

source

@[implicit_reducible]

instance OracleComp.ProgramLogic.instInhabitedVCSpecKind :

Inhabited VCSpecKind

source

def OracleComp.ProgramLogic.instBEqVCSpecKind.beq :

VCSpecKind → VCSpecKind → Bool

Instances For

source

@[implicit_reducible]

instance OracleComp.ProgramLogic.instBEqVCSpecKind :

BEq VCSpecKind

source

def OracleComp.ProgramLogic.instReprVCSpecKind.repr :

VCSpecKind → ℕ → Std.Format

Instances For

source

@[implicit_reducible]

instance OracleComp.ProgramLogic.instReprVCSpecKind :

Repr VCSpecKind

source

inductive OracleComp.ProgramLogic.VCSpecLookupKey :

Type

unary (head : Lean.Name) : VCSpecLookupKey
relational (leftHead rightHead : Lean.Name) : VCSpecLookupKey

Instances For

source

@[implicit_reducible]

instance OracleComp.ProgramLogic.instInhabitedVCSpecLookupKey :

Inhabited VCSpecLookupKey

source

def OracleComp.ProgramLogic.instInhabitedVCSpecLookupKey.default :

VCSpecLookupKey

Instances For

source

def OracleComp.ProgramLogic.instBEqVCSpecLookupKey.beq :

VCSpecLookupKey → VCSpecLookupKey → Bool

Instances For

source

@[implicit_reducible]

instance OracleComp.ProgramLogic.instBEqVCSpecLookupKey :

BEq VCSpecLookupKey

source

@[implicit_reducible]

instance OracleComp.ProgramLogic.instReprVCSpecLookupKey :

Repr VCSpecLookupKey

source

def OracleComp.ProgramLogic.instReprVCSpecLookupKey.repr :

VCSpecLookupKey → ℕ → Std.Format

Instances For

source

inductive OracleComp.ProgramLogic.VCSpecArgShape :

Type

schematic : VCSpecArgShape
concrete : VCSpecArgShape

Instances For

source

def OracleComp.ProgramLogic.instInhabitedVCSpecArgShape.default :

VCSpecArgShape

Instances For

source

@[implicit_reducible]

instance OracleComp.ProgramLogic.instInhabitedVCSpecArgShape :

Inhabited VCSpecArgShape

source

def OracleComp.ProgramLogic.instBEqVCSpecArgShape.beq :

VCSpecArgShape → VCSpecArgShape → Bool

Instances For

source

@[implicit_reducible]

instance OracleComp.ProgramLogic.instBEqVCSpecArgShape :

BEq VCSpecArgShape

source

def OracleComp.ProgramLogic.instReprVCSpecArgShape.repr :

VCSpecArgShape → ℕ → Std.Format

Instances For

source

@[implicit_reducible]

instance OracleComp.ProgramLogic.instReprVCSpecArgShape :

Repr VCSpecArgShape

source

inductive OracleComp.ProgramLogic.VCSpecCompForm :

Type

bind : VCSpecCompForm
pure : VCSpecCompForm
ite : VCSpecCompForm
map : VCSpecCompForm
replicate : VCSpecCompForm
listMapM : VCSpecCompForm
listFoldlM : VCSpecCompForm
query : VCSpecCompForm
simulateQ : VCSpecCompForm
other : VCSpecCompForm

Instances For

source

@[implicit_reducible]

instance OracleComp.ProgramLogic.instInhabitedVCSpecCompForm :

Inhabited VCSpecCompForm

source

def OracleComp.ProgramLogic.instInhabitedVCSpecCompForm.default :

VCSpecCompForm

Instances For

source

def OracleComp.ProgramLogic.instBEqVCSpecCompForm.beq :

VCSpecCompForm → VCSpecCompForm → Bool

Instances For

source

@[implicit_reducible]

instance OracleComp.ProgramLogic.instBEqVCSpecCompForm :

BEq VCSpecCompForm

source

@[implicit_reducible]

instance OracleComp.ProgramLogic.instReprVCSpecCompForm :

Repr VCSpecCompForm

source

def OracleComp.ProgramLogic.instReprVCSpecCompForm.repr :

VCSpecCompForm → ℕ → Std.Format

Instances For

source

inductive OracleComp.ProgramLogic.VCSpecCompPattern :

Type

unary (form : VCSpecCompForm) : VCSpecCompPattern
relational (leftForm rightForm : VCSpecCompForm) : VCSpecCompPattern

Instances For

source

def OracleComp.ProgramLogic.instInhabitedVCSpecCompPattern.default :

VCSpecCompPattern

Instances For

source

@[implicit_reducible]

instance OracleComp.ProgramLogic.instInhabitedVCSpecCompPattern :

Inhabited VCSpecCompPattern

source

def OracleComp.ProgramLogic.instBEqVCSpecCompPattern.beq :

VCSpecCompPattern → VCSpecCompPattern → Bool

Instances For

source

@[implicit_reducible]

instance OracleComp.ProgramLogic.instBEqVCSpecCompPattern :

BEq VCSpecCompPattern

source

def OracleComp.ProgramLogic.instReprVCSpecCompPattern.repr :

VCSpecCompPattern → ℕ → Std.Format

Instances For

source

@[implicit_reducible]

instance OracleComp.ProgramLogic.instReprVCSpecCompPattern :

Repr VCSpecCompPattern

source

structure OracleComp.ProgramLogic.NormalizedVCSpec :

Type

kind : VCSpecKind
lookupKey : VCSpecLookupKey
compPattern : VCSpecCompPattern
theoremBinderCount : ℕ
preShape : Option VCSpecArgShape
postShape : VCSpecArgShape

Instances For

source

def OracleComp.ProgramLogic.instInhabitedNormalizedVCSpec.default :

NormalizedVCSpec

Instances For

source

@[implicit_reducible]

instance OracleComp.ProgramLogic.instInhabitedNormalizedVCSpec :

Inhabited NormalizedVCSpec

source

@[implicit_reducible]

instance OracleComp.ProgramLogic.instBEqNormalizedVCSpec :

BEq NormalizedVCSpec

source

def OracleComp.ProgramLogic.instBEqNormalizedVCSpec.beq :

NormalizedVCSpec → NormalizedVCSpec → Bool

Instances For

source

def OracleComp.ProgramLogic.instReprNormalizedVCSpec.repr :

NormalizedVCSpec → ℕ → Std.Format

Instances For

source

@[implicit_reducible]

instance OracleComp.ProgramLogic.instReprNormalizedVCSpec :

Repr NormalizedVCSpec

source

def OracleComp.ProgramLogic.VCSpecLookupKey.toLegacyKey :

VCSpecLookupKey → Lean.Name ⊕ Lean.Name × Lean.Name

Instances For

source

def OracleComp.ProgramLogic.classifyVCSpecCompForm (comp : Lean.Expr) :

VCSpecCompForm

Instances For

source

def OracleComp.ProgramLogic.classifyUnaryCompPattern (comp : Lean.Expr) :

VCSpecCompPattern

Instances For

source

def OracleComp.ProgramLogic.classifyRelationalCompPattern (oa ob : Lean.Expr) :

VCSpecCompPattern

Instances For

source

def OracleComp.ProgramLogic.normalizeVCSpecTarget (attrName : Lean.Name) (declTy : Lean.Expr) :

Lean.MetaM NormalizedVCSpec

Instances For

Documentation

VCVio.ProgramLogic.Tactics.Common.SpecIR

VC Spec Intermediate Representation #