Overview  Index  Help 

ProofChecker


The First-Order LoopW Proof Checker proof checking. The proof checker verify that the given program respresents a correct proof.

Opened structures

ProofAst

ProofAstUtils

ProofEnvironment

Terms

BasePrettyPrinter

               
Value summary

val checkClosedProg : ProofAst.program -> bool
           check that the given program represents a correct proof.

val checkExp
           check that the given expression represents a correct proof.

val checkInSequence

val checkSequence
           check that the given sequence represents a correct proof.

val checkValue
           check that the given value represents a correct proof.

val typeFailureExp

val typeFailureInSeq

val typeFailureSeq
           displays an error message with the current proof checking environment and the source code region.

 

       
Value detail

typeFailureSeq

fun typeFailureSeq gamma omega (j, omega') seq reg msg

displays an error message with the current proof checking environment and the source code region.

Parameters:
gamma
the constant proof checking environment.
omega
the variable proof checking environment.
j
the out type existential quantified variables.
omega'
the out type.
seq
the sequence that generates the error.
k
the seq out type existential quantified variables.
delta
the seq out type.
reg
the region.
msg
the error message.

typeFailureInSeq

val typeFailureInSeq


typeFailureExp

val typeFailureExp


checkSequence

fun checkSequence gamma omega (j, omega') reg seq

check that the given sequence represents a correct proof.

Parameters:
gamma
the constant proof checking environment.
omega
the variable proof checking environment.
j
the out type existential quantified variables.
omega'
the out type.
reg
the region.
seq
the sequence to check.
Returns:
true if and only if seq is a correct proof.

checkInSequence

val checkInSequence


checkExp

fun checkExp gamma omega typ reg (expression, tau)

check that the given expression represents a correct proof.

Parameters:
gamma
the constant proof checking environment.
omega
the variable proof checking environment.
typ
the requiered type.
reg
the region.
expression
the expression to check.
tau
the given type.
Returns:
true if and only if expression is a correct proof of formula tau.

checkValue

fun checkValue v reg

check that the given value represents a correct proof.

Parameters:
v
the value.
Returns:
true if and only if p is a correct proof.

checkClosedProg

fun checkClosedProg p : ProofAst.program -> bool

check that the given program represents a correct proof.

Parameters:
p
the program.
Returns:
true if and only if p is a correct proof.

 


Overview  Index  Help