Overview  Index  Help 

ProofInfer


The First-Order LoopW Type Inference proof inference. The proof inference builds a complete proof structure from a source code.

Opened structures

CoreAst

CoreAstUtils

Terms

TermMatchUnif

ProofEnvironment

           
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.

 
DataConstructor summary

constructor ERROR
            : env *
              env *
              (ident list * env) option *
              string *
              Error.region option ->
                result

constructor OK : result

 
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.

 

   
Datatype detail

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.

 
DataConstructor detail

OK

constructor OK : result


ERROR

constructor ERROR
            : env *
              env *
              (ident list * env) option *
              string *
              Error.region option ->
                result

 
Value detail

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.

 


Overview  Index  Help