diff options
Diffstat (limited to 'contrib/correctness/pcicenv.ml')
-rw-r--r-- | contrib/correctness/pcicenv.ml | 118 |
1 files changed, 0 insertions, 118 deletions
diff --git a/contrib/correctness/pcicenv.ml b/contrib/correctness/pcicenv.ml deleted file mode 100644 index 368d0281..00000000 --- a/contrib/correctness/pcicenv.ml +++ /dev/null @@ -1,118 +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: pcicenv.ml 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Names -open Term -open Sign - -open Pmisc -open Putil -open Ptype -open Past - -(* on redéfinit add_sign pour éviter de construire des environnements - * avec des doublons (qui font planter la résolution des implicites !) *) - -(* VERY UGLY!! find some work around *) -let modify_sign id t s = - fold_named_context - (fun ((x,b,ty) as d) sign -> - if x=id then add_named_decl (x,b,t) sign else add_named_decl d sign) - s ~init:empty_named_context - -let add_sign (id,t) s = - try - let _ = lookup_named id s in - modify_sign id t s - with Not_found -> - add_named_decl (id,None,t) s - -let cast_set c = mkCast (c, mkSet) - -let set = mkCast (mkSet, mkType Univ.prop_univ) - -(* [cci_sign_of env] construit un environnement pour CIC ne comprenant que - * les objets fonctionnels de l'environnement de programes [env] - *) - -let cci_sign_of ren env = - Penv.fold_all - (fun (id,v) sign -> - match v with - | Penv.TypeV (Ref _ | Array _) -> sign - | Penv.TypeV v -> - let ty = Pmonad.trad_ml_type_v ren env v in - add_sign (id,cast_set ty) sign - | Penv.Set -> add_sign (id,set) sign) - env (Global.named_context ()) - -(* [sign_meta ren env fadd ini] - * construit un environnement pour CIC qui prend en compte les variables - * de programme. - * pour cela, cette fonction parcours tout l'envrionnement (global puis - * local [env]) et pour chaque déclaration, ajoute ce qu'il faut avec la - * fonction [fadd] s'il s'agit d'un mutable et directement sinon, - * en partant de [ini]. - *) - -let sign_meta ren env fast ini = - Penv.fold_all - (fun (id,v) sign -> - match v with - | Penv.TypeV (Ref _ | Array _ as v) -> - let ty = Pmonad.trad_imp_type ren env v in - fast sign id ty - | Penv.TypeV v -> - let ty = Pmonad.trad_ml_type_v ren env v in - add_sign (id,cast_set ty) sign - | Penv.Set -> add_sign (id,set) sign) - env ini - -let add_sign_d dates (id,c) sign = - let sign = - List.fold_left (fun sign d -> add_sign (at_id id d,c) sign) sign dates - in - add_sign (id,c) sign - -let sign_of add ren env = - sign_meta ren env - (fun sign id c -> let c = cast_set c in add (id,c) sign) - (Global.named_context ()) - -let result_of sign = function - None -> sign - | Some (id,c) -> add_sign (id, cast_set c) sign - -let before_after_result_sign_of res ren env = - let dates = "" :: Prename.all_dates ren in - result_of (sign_of (add_sign_d dates) ren env) res - -let before_after_sign_of ren = - let dates = "" :: Prename.all_dates ren in - sign_of (add_sign_d dates) ren - -let before_sign_of ren = - let dates = Prename.all_dates ren in - sign_of (add_sign_d dates) ren - -let now_sign_of = - sign_of (add_sign_d []) - - -(* environnement après traduction *) - -let trad_sign_of ren = - sign_of - (fun (id,c) sign -> add_sign (Prename.current_var ren id,c) sign) - ren - - |