ProofInfer
-
The First-Order LoopW Type Inference proof inference.
The proof inference builds a complete proof structure from a
source code.
-
Datatype summary
|
datatype result =
OK
| ERROR of
env * env * (ident list * env) option * string * Error.region option
result type, either OK or ERROR with information enough to display an error message.
|
Value summary
|
val getEqualities
collects the equalities in two environment, discarding identities.
|
val getMsg
builds a string with an error message, depending on the exception.
|
val inferExp
infer proof for expressions according to the loopW dependent type system.
|
val inferProg
infer proof for programs according to the loopW dependent type system.
|
val inferSeq
infer proof for sequences according to the loopW dependent type system.
|
val inferVal
infer proof for values according to the loopW dependent type system.
|
val mk_exp_subst_lemma
builds a substitution derivation for an expression.
|
val mk_seq_subst_lemma
builds a substitution derivation for a sequence.
|
val proofInfer : CoreAst.program -> ProofAst.program
returns the complete proof.
|
result
datatype result =
OK
| ERROR of
env * env * (ident list * env) option * string * Error.region option
-
result type, either OK or ERROR with information enough to display an error message.
-
OK
constructor OK : result
ERROR
constructor ERROR
: env *
env *
(ident list * env) option *
string *
Error.region option ->
result
getMsg
fun getMsg ex
-
builds a string with an error message, depending on the exception.
-
- Parameters:
-
-
ex
-
the exception.
- Returns:
-
the string representation of the exception.
getEqualities
fun getEqualities gamma omega
-
collects the equalities in two environment, discarding identities.
-
- Parameters:
-
-
gamma
-
the first environment.
-
omega
-
the second environment.
- Returns:
-
the equalities (n = m) where (n <> m).
mk_seq_subst_lemma
fun mk_seq_subst_lemma gamma omega seq (j, phi_i) eql
-
builds a substitution derivation for a sequence.
-
- Parameters:
-
-
gamma
-
the first typing environment.
-
omega
-
the second typing environment.
-
seq
-
the sequence.
-
j
-
the list of identifier existentially quantified.
-
phi_i
-
the formula phi[i] in which i will be substituted by the terms of the equation.
-
eql
-
the equation list [(i, m = n)].
- Returns:
-
the sequence derivation with the substitution rule.
mk_exp_subst_lemma
fun mk_exp_subst_lemma gamma omega exp phi_i eql
-
builds a substitution derivation for an expression.
-
- Parameters:
-
-
gamma
-
the first typing environment.
-
omega
-
the second typing environment.
-
exp
-
the expression.
-
phi_i
-
the formula phi[i] in which i will be substituted by the terms of the equation.
-
eql
-
the equation list (i, m = n).
- Returns:
-
the expression derivation with the substitution rule.
inferSeq
fun inferSeq gamma omega (j, omega') reg sequence
-
infer proof for sequences according to the loopW dependent type system.
-
- Parameters:
-
-
gamma
-
the constant identifier input typing environment.
-
omega
-
the variable identifier input typing environment.
-
j
-
the identifier list of existential quantification of output environment.
-
omega'
-
the variable identifier output typing environment (existentialy quantified over j).
-
reg
-
the region of the source code containing this sequence (for error messages).
-
sequence
-
the sequence on which to perform proof inference.
- Returns:
-
(seq', result) where seq' is the complete proof representation of sequence
and result is either OK if proof inference suceeded or ERROR with the error data.
inferExp
fun inferExp gamma omega reg exp
-
infer proof for expressions according to the loopW dependent type system.
-
- Parameters:
-
-
gamma
-
the constant identifier input typing environment.
-
omega
-
the variable identifier input typing environment.
-
reg
-
the region of the source code containing this expression (for error messages).
-
exp
-
the expression on which to perform proof inference.
- Returns:
-
(exp', result) where exp' is the complete proof representation of exp
and result is either OK if proof inference suceeded or ERROR with the error data.
inferVal
fun inferVal gamma omega reg val
-
infer proof for values according to the loopW dependent type system.
-
- Parameters:
-
-
gamma
-
the constant identifier input typing environment.
-
omega
-
the variable identifier input typing environment.
-
reg
-
the region of the source code containing this value (for error messages).
-
val
-
the value on which to perform proof inference.
- Returns:
-
(val', result) where val' is the complete proof representation of val
and result is either OK if proof inference suceeded or ERROR with the error data.
inferProg
fun inferProg gamma omega (j, omega') p
-
infer proof for programs according to the loopW dependent type system.
-
- Parameters:
-
-
gamma
-
the constant identifier input typing environment.
-
omega
-
the variable identifier input typing environment.
-
j
-
the identifier list of existential quantification of output environment.
-
omega'
-
the variable identifier output typing environment (existentialy quantified over j).
-
p
-
the program on which to perform proof inference.
- Returns:
-
the complete proof representation of p.
- Exception:
-
-
Fail
-
(via Error.fail) if proof inference did not succed.
proofInfer
fun proofInfer p : CoreAst.program -> ProofAst.program
-
returns the complete proof.
-
- Parameters:
-
-
p
-
the source program.
- Returns:
-
the complete proof representation of p.