ProofChecker
-
The First-Order LoopW Proof Checker proof checking.
The proof checker verify that the given program respresents a correct proof.
-
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.