mise en place de Correctness (ne compile pas encore)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1501 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 224 insertions, 0 deletions

diff --git a/contrib/correctness/penv.ml b/contrib/correctness/penv.ml
new file mode 100644
index 000000000..fe37f8308
--- /dev/null
+++ b/contrib/correctness/penv.ml
@@ -0,0 +1,224 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \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$ *)
+
+open Pmisc
+open Past
+open Ptype
+open Names
+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_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 (inProg,outProg) =
+  declare_object ("programs-objects",
+                  { load_function = cache_global;
+                    cache_function = cache_global;
+                    open_function = (fun _ -> ());
+		    export_function = (fun x -> Some x) })
+;;
+
+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
+	add_named_object (id',OBJ) (inProg (id,TypeV v,p))
+    end
+
+let add_global_set id =
+  try
+    let _ = Env.find id !env in
+    Prog_errors.clash id None
+  with
+    Not_found -> add_named_object (id,OBJ) (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 (inInit,outInit) =
+  declare_object ("programs-objects-init",
+                  { load_function = (fun _ -> ());
+                    cache_function = cache_init;
+                    specification_function = fun x -> x})
+
+let initialize id c = add_anonymous_object (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
+      add_global id' v (Some p);
+      mSGNL (hOV 0 [< 'sTR"Program "; pID id'; 'sPC; 'sTR"is defined" >]);
+      edited := IdMap.remove id !edited
+  with Not_found -> ()
+