Overview  Index  Help 

PROOF_ENVIRONMENT

All Known Implementing Modules:

ProofEnvironmentProofChecker


The First-Order LoopW Proof Checker proof environment abstract type. The proof derivation pretty-printer proof environment abstract type provides functions to deal with typing environment.

     
Type summary

type env = (ProofAst.ident * ProofAst.formula) list
           the typing environment.

     
Value summary

val +! : env * (ProofAst.ident * ProofAst.formula) -> env
           adds an identifier typing in an environment.

val ++ : env * env -> env
           adds every typed identifiers of an environment at the end of another environment.

val -! : env * ProofAst.ident -> env
           removes an identifier typing in an environment.

val dom : env -> ProofAst.ident list
           returns the domain of the environment.

val empty : env
           the empty environment.

val envEquals : env -> env -> bool
           test if the enviroment are equals.

val getVarType : ProofAst.ident -> env -> ProofAst.formula option
           returns the type of an identifier in an environment.

val img : env -> ProofAst.formula list
           returns the image of the environment.

val split : env -> ProofAst.ident list -> (env * env) option
           check that an identifier list is included in an environment, returns the partition of it according to that list.

 

 
Type detail

env

type env = (ProofAst.ident * ProofAst.formula) list

the typing environment.

     
Value detail

empty

val empty : env

the empty environment.


getVarType

fun getVarType x env : ProofAst.ident -> env -> ProofAst.formula option

returns the type of an identifier in an environment.

Parameters:
x
the variable.
env
the environment x1:T1, ..., xn:Tn.
Returns:
SOME Ti if there exists i such that x = xi, or NONE.

-!

fun -! x env : env * ProofAst.ident -> env

removes an identifier typing in an environment.

Parameters:
x
the identifier.
env
the environment x1:T1, ..., xn:Tn.
Returns:
env without x:T for any T.

+!

fun +! env (x, t) : env * (ProofAst.ident * ProofAst.formula) -> env

adds an identifier typing in an environment. Ensures that x occurs only once in the environment.

Parameters:
env
the environment x1:T1, ..., xn:Tn.
x
the identifier.
t
the type of the identifier.
Returns:
x:t,(env without x:T for any T).

++

fun ++ env1 env2 : env * env -> env

adds every typed identifiers of an environment at the end of another environment. Ensures that each identifier occurs only once in the resulting environment.

Parameters:
env1
the first environment x1:T1, ..., xn:Tn.
env2
the second environment y1:U1, ..., ym:Um.
Returns:
x1:T1, ..., xn:Tn,(env2 without x1, ..., xn).

split

fun split env xl : env -> ProofAst.ident list -> (env * env) option

check that an identifier list is included in an environment, returns the partition of it according to that list.

Parameters:
env
the environment x1:T1, ..., xn:Tn.
xl
the identifier list y1, ..., ym.
Returns:
SOME((y1:U1, ..., ym:Um), (env without y1, ..., ym)) if y1, ..., ym belongs to env, else NONE.

dom

fun dom env : env -> ProofAst.ident list

returns the domain of the environment.

Parameters:
env
the environment x1:T1, ..., xn:Tn.
Returns:
x1, ..., xn.

img

fun img env : env -> ProofAst.formula list

returns the image of the environment.

Parameters:
env
the environment x1:T1, ..., xn:Tn.
Returns:
T1, ..., Tn.

envEquals

fun envEquals env1 env2 : env -> env -> bool

test if the enviroment are equals.

Parameters:
env1
the first environment.
env2
the second environment.
Returns:
true if the contents of env1 and env2 are equals (independantly of the ordering).

 


Overview  Index  Help