diff options
Diffstat (limited to 'contrib/correctness/penv.ml')
-rw-r--r-- | contrib/correctness/penv.ml | 240 |
1 files changed, 0 insertions, 240 deletions
diff --git a/contrib/correctness/penv.ml b/contrib/correctness/penv.ml deleted file mode 100644 index 7f89b1e1..00000000 --- a/contrib/correctness/penv.ml +++ /dev/null @@ -1,240 +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: penv.ml 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Pmisc -open Past -open Ptype -open Names -open Nameops -open Libobject -open Library -open Term - -(* Environments for imperative programs. - * - * An environment of programs is an association tables - * from identifiers (Names.identifier) to types of values with effects - * (ProgAst.ml_type_v), together with a list of these associations, since - * the order is relevant (we have dependent types e.g. [x:nat; t:(array x T)]) - *) - -module Env = struct - type 'a t = ('a Idmap.t) - * ((identifier * 'a) list) - * ((identifier * (identifier * variant)) list) - let empty = Idmap.empty, [], [] - let add id v (m,l,r) = (Idmap.add id v m, (id,v)::l, r) - let find id (m,_,_) = Idmap.find id m - let fold f (_,l,_) x0 = List.fold_right f l x0 - let add_rec (id,var) (m,l,r) = (m,l,(id,var)::r) - let find_rec id (_,_,r) = List.assoc id r -end - -(* Local environments *) - -type type_info = Set | TypeV of type_v - -type local_env = type_info Env.t - -let empty = (Env.empty : local_env) - -let add (id,v) = Env.add id (TypeV v) - -let add_set id = Env.add id Set - -let find id env = - match Env.find id env with TypeV v -> v | Set -> raise Not_found - -let is_local env id = - try - match Env.find id env with TypeV _ -> true | Set -> false - with - Not_found -> false - -let is_local_set env id = - try - match Env.find id env with TypeV _ -> false | Set -> true - with - Not_found -> false - - -(* typed programs *) - -type typing_info = { - env : local_env; - kappa : constr ml_type_c -} - -type typed_program = (typing_info, constr) t - - -(* The global environment. - * - * We have a global typing environment env - * We also keep a table of programs for extraction purposes - * and a table of initializations (still for extraction) - *) - -let (env : type_info Env.t ref) = ref Env.empty - -let (pgm_table : (typed_program option) Idmap.t ref) = ref Idmap.empty - -let (init_table : constr Idmap.t ref) = ref Idmap.empty - -let freeze () = (!env, !pgm_table, !init_table) -let unfreeze (e,p,i) = env := e; pgm_table := p; init_table := i -let init () = - env := Env.empty; pgm_table := Idmap.empty; init_table := Idmap.empty -;; - -Summary.declare_summary "programs-environment" - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = false } -;; - -(* Operations on the global environment. *) - -let add_pgm id p = pgm_table := Idmap.add id p !pgm_table - -let cache_global (_,(id,v,p)) = - env := Env.add id v !env; add_pgm id p - -let type_info_app f = function Set -> Set | TypeV v -> TypeV (f v) - -let subst_global (_,s,(id,v,p)) = (id, type_info_app (type_v_knsubst s) v, p) - -let (inProg,outProg) = - declare_object { object_name = "programs-objects"; - cache_function = cache_global; - load_function = (fun _ -> cache_global); - open_function = (fun _ _ -> ()); - classify_function = (fun (_,x) -> Substitute x); - subst_function = subst_global; - export_function = (fun x -> Some x) } - -let is_mutable = function Ref _ | Array _ -> true | _ -> false - -let add_global id v p = - try - let _ = Env.find id !env in - Perror.clash id None - with - Not_found -> begin - let id' = - if is_mutable v then id - else id_of_string ("prog_" ^ (string_of_id id)) - in - Lib.add_leaf id' (inProg (id,TypeV v,p)) - end - -let add_global_set id = - try - let _ = Env.find id !env in - Perror.clash id None - with - Not_found -> Lib.add_leaf id (inProg (id,Set,None)) - -let is_global id = - try - match Env.find id !env with TypeV _ -> true | Set -> false - with - Not_found -> false - -let is_global_set id = - try - match Env.find id !env with TypeV _ -> false | Set -> true - with - Not_found -> false - - -let lookup_global id = - match Env.find id !env with TypeV v -> v | Set -> raise Not_found - -let find_pgm id = Idmap.find id !pgm_table - -let all_vars () = - Env.fold - (fun (id,v) l -> match v with TypeV (Arrow _|TypePure _) -> id::l | _ -> l) - !env [] - -let all_refs () = - Env.fold - (fun (id,v) l -> match v with TypeV (Ref _ | Array _) -> id::l | _ -> l) - !env [] - -(* initializations *) - -let cache_init (_,(id,c)) = - init_table := Idmap.add id c !init_table - -let subst_init (_,s,(id,c)) = (id, subst_mps s c) - -let (inInit,outInit) = - declare_object { object_name = "programs-objects-init"; - cache_function = cache_init; - load_function = (fun _ -> cache_init); - open_function = (fun _ _-> ()); - classify_function = (fun (_,x) -> Substitute x); - subst_function = subst_init; - export_function = (fun x -> Some x) } - -let initialize id c = Lib.add_anonymous_leaf (inInit (id,c)) - -let find_init id = Idmap.find id !init_table - - -(* access in env, local then global *) - -let type_in_env env id = - try find id env with Not_found -> lookup_global id - -let is_in_env env id = - (is_global id) or (is_local env id) - -let fold_all f lenv x0 = - let x1 = Env.fold f !env x0 in - Env.fold f lenv x1 - - -(* recursions *) - -let add_recursion = Env.add_rec - -let find_recursion = Env.find_rec - - -(* We also maintain a table of the currently edited proofs of programs - * in order to add them in the environnement when the user does Save *) - -open Pp -open Himsg - -let (edited : (type_v * typed_program) Idmap.t ref) = ref Idmap.empty - -let new_edited id v = - edited := Idmap.add id v !edited - -let is_edited id = - try let _ = Idmap.find id !edited in true with Not_found -> false - -let register id id' = - try - let (v,p) = Idmap.find id !edited in - let _ = add_global id' v (Some p) in - Options.if_verbose - msgnl (hov 0 (str"Program " ++ pr_id id' ++ spc () ++ str"is defined")); - edited := Idmap.remove id !edited - with Not_found -> () - |