ProofEnvironment
-
The First-Order LoopW Type Inference proof environment abstract type.
The proof derivation pretty-printer proof environment abstract type
provides functions to deal with typing environment.
-
env
type env = (ident * formula) list
-
the typing environment.
-
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 identifier.
-
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 +! (x, t) env : env * (ProofAst.ident * ProofAst.formula) -> env
-
adds an identifier typing in an environment. Ensures that x occurs only once
in the environment.
-
- Parameters:
-
-
x
-
the identifier.
-
t
-
the type of the identifier.
-
env
-
the environment x1:T1, ..., xn:Tn.
- 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).