diff options
author | 2008-07-25 15:12:53 +0200 | |
---|---|---|
committer | 2008-07-25 15:12:53 +0200 | |
commit | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch) | |
tree | dabcac548e299fee1da464c93b3dba98484f45b1 /contrib/correctness/pmonad.mli | |
parent | 2281410e38ef99d025ea77194585a9bc019fdaa9 (diff) |
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'contrib/correctness/pmonad.mli')
-rw-r--r-- | contrib/correctness/pmonad.mli | 106 |
1 files changed, 0 insertions, 106 deletions
diff --git a/contrib/correctness/pmonad.mli b/contrib/correctness/pmonad.mli deleted file mode 100644 index a46a040e..00000000 --- a/contrib/correctness/pmonad.mli +++ /dev/null @@ -1,106 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* Certification of Imperative Programs / Jean-Christophe Filli�tre *) - -(* $Id: pmonad.mli 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Names -open Term - -open Ptype -open Past -open Penv - -(* Main part of the translation of imperative programs into functional ones - * (with mlise.ml) *) - -(* Here we translate the specification into a CIC specification *) - -val trad_ml_type_v : Prename.t -> local_env -> type_v -> constr -val trad_ml_type_c : Prename.t -> local_env -> type_c -> constr -val trad_imp_type : Prename.t -> local_env -> type_v -> constr -val trad_type_in_env : Prename.t -> local_env -> identifier -> constr - -val binding_of_alist : Prename.t -> local_env - -> (identifier * identifier) list - -> cc_binder list -val make_abs : cc_binder list -> cc_term -> cc_term -val abs_pre : Prename.t -> local_env -> cc_term * constr -> - constr precondition list -> cc_term - -(* The following functions translate the main constructions *) - -val make_tuple : (cc_term * cc_type) list -> predicate option - -> Prename.t -> local_env -> string - -> cc_term - -val result_tuple : Prename.t -> string -> local_env - -> (cc_term * constr) -> (Peffect.t * predicate option) - -> cc_term * constr - -val let_in_pre : constr -> constr precondition -> cc_term -> cc_term - -val make_let_in : Prename.t -> local_env -> cc_term - -> constr precondition list - -> ((identifier * identifier) list * predicate option) - -> identifier * constr - -> cc_term * constr -> cc_term - -val make_block : Prename.t -> local_env - -> (Prename.t -> (identifier * constr) option -> cc_term * constr) - -> (cc_term * type_c, constr) block - -> cc_term - -val make_app : local_env - -> Prename.t -> (cc_term * type_c) list - -> Prename.t -> cc_term * type_c - -> ((type_v binder list) * type_c) - * ((identifier*identifier) list) - * type_c - -> type_c - -> cc_term - -val make_if : Prename.t -> local_env - -> cc_term * type_c - -> Prename.t - -> cc_term * type_c - -> cc_term * type_c - -> type_c - -> cc_term - -val make_while : Prename.t -> local_env - -> (constr * constr * constr) (* typed variant *) - -> cc_term * type_c - -> (cc_term * type_c, constr) block - -> constr assertion option * type_c - -> cc_term - -val make_letrec : Prename.t -> local_env - -> (identifier * (constr * constr * constr)) (* typed variant *) - -> identifier (* the name of the function *) - -> (cc_binder list) - -> (cc_term * type_c) - -> type_c - -> cc_term - -(* Functions to translate array operations *) - -val array_info : - Prename.t -> local_env -> identifier -> constr * constr * constr - -val make_raw_access : - Prename.t -> local_env -> identifier * identifier -> constr -> constr - -val make_raw_store : - Prename.t -> local_env -> identifier * identifier - -> constr -> constr -> constr - -val make_pre_access : - Prename.t -> local_env -> identifier -> constr -> constr - |