diff options
Diffstat (limited to 'contrib/correctness')
37 files changed, 1 insertions, 6501 deletions
diff --git a/contrib/correctness/ProgramsExtraction.v b/contrib/correctness/ProgramsExtraction.v index 5f7dfdbf..70f4b730 100644 --- a/contrib/correctness/ProgramsExtraction.v +++ b/contrib/correctness/ProgramsExtraction.v @@ -8,9 +8,7 @@ (* Certification of Imperative Programs / Jean-Christophe Filliâtre *) -(* $Id: ProgramsExtraction.v 5920 2004-07-16 20:01:26Z herbelin $ *) - -Require Export Extraction. +(* $Id: ProgramsExtraction.v 10290 2007-11-06 01:27:17Z letouzey $ *) Extract Inductive unit => unit [ "()" ]. Extract Inductive bool => bool [ true false ]. diff --git a/contrib/correctness/past.mli b/contrib/correctness/past.mli deleted file mode 100644 index 70328704..00000000 --- a/contrib/correctness/past.mli +++ /dev/null @@ -1,97 +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: past.mli 5920 2004-07-16 20:01:26Z herbelin $ *) - -(*s Abstract syntax of imperative programs. *) - -open Names -open Ptype -open Topconstr - -type termination = - | RecArg of int - | Wf of constr_expr * constr_expr - -type variable = identifier - -type pattern = - | PatVar of identifier - | PatConstruct of identifier * ((kernel_name * int) * int) - | PatAlias of pattern * identifier - | PatPair of pattern * pattern - | PatApp of pattern list - -type epattern = - | ExnConstant of identifier - | ExnBind of identifier * identifier - -type ('a, 'b) block_st = - | Label of string - | Assert of 'b Ptype.assertion - | Statement of 'a - -type ('a, 'b) block = ('a, 'b) block_st list - -type ('a, 'b) t = { - desc : ('a, 'b) t_desc; - pre : 'b Ptype.precondition list; - post : 'b Ptype.postcondition option; - loc : Util.loc; - info : 'a -} - -and ('a, 'b) t_desc = - | Variable of variable - | Acc of variable - | Aff of variable * ('a, 'b) t - | TabAcc of bool * variable * ('a, 'b) t - | TabAff of bool * variable * ('a, 'b) t * ('a, 'b) t - | Seq of (('a, 'b) t, 'b) block - | While of ('a, 'b) t * 'b Ptype.assertion option * ('b * 'b) * - (('a, 'b) t, 'b) block - | If of ('a, 'b) t * ('a, 'b) t * ('a, 'b) t - | Lam of 'b Ptype.ml_type_v Ptype.binder list * ('a, 'b) t - | Apply of ('a, 'b) t * ('a, 'b) arg list - | SApp of ('a, 'b) t_desc list * ('a, 'b) t list - | LetRef of variable * ('a, 'b) t * ('a, 'b) t - | Let of variable * ('a, 'b) t * ('a, 'b) t - | LetRec of variable * 'b Ptype.ml_type_v Ptype.binder list * - 'b Ptype.ml_type_v * ('b * 'b) * ('a, 'b) t - | PPoint of string * ('a, 'b) t_desc - | Expression of Term.constr - | Debug of string * ('a, 'b) t - -and ('a, 'b) arg = - | Term of ('a, 'b) t - | Refarg of variable - | Type of 'b Ptype.ml_type_v - -type program = (unit, Topconstr.constr_expr) t - -(*s Intermediate type for CC terms. *) - -type cc_type = Term.constr - -type cc_bind_type = - | CC_typed_binder of cc_type - | CC_untyped_binder - -type cc_binder = variable * cc_bind_type - -type cc_term = - | CC_var of variable - | CC_letin of bool * cc_type * cc_binder list * cc_term * cc_term - | CC_lam of cc_binder list * cc_term - | CC_app of cc_term * cc_term list - | CC_tuple of bool * cc_type list * cc_term list - | CC_case of cc_type * cc_term * cc_term list - | CC_expr of Term.constr - | CC_hole of cc_type diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml deleted file mode 100644 index 041cd81f..00000000 --- a/contrib/correctness/pcic.ml +++ /dev/null @@ -1,231 +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: pcic.ml 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Util -open Names -open Nameops -open Libnames -open Term -open Termops -open Nametab -open Declarations -open Indtypes -open Sign -open Rawterm -open Typeops -open Entries -open Topconstr - -open Pmisc -open Past - - -(* Here we translate intermediates terms (cc_term) into CCI terms (constr) *) - -let make_hole c = mkCast (isevar, c) - -(* Tuples are defined in file Tuples.v - * and their constructors are called Build_tuple_n or exists_n, - * wether they are dependant (last element only) or not. - * If necessary, tuples are generated ``on the fly''. *) - -let tuple_exists id = - try let _ = Nametab.locate (make_short_qualid id) in true - with Not_found -> false - -let ast_set = CSort (dummy_loc,RProp Pos) - -let tuple_n n = - let id = make_ident "tuple_" (Some n) in - let l1n = Util.interval 1 n in - let params = - List.map (fun i -> - (LocalRawAssum ([dummy_loc,Name (make_ident "T" (Some i))], ast_set))) - l1n in - let fields = - List.map - (fun i -> - let id = make_ident ("proj_" ^ string_of_int n ^ "_") (Some i) in - let id' = make_ident "T" (Some i) in - (false, Vernacexpr.AssumExpr ((dummy_loc,Name id), mkIdentC id'))) - l1n - in - let cons = make_ident "Build_tuple_" (Some n) in - Record.definition_structure - ((false, (dummy_loc,id)), params, fields, cons, mk_Set) - -(*s [(sig_n n)] generates the inductive - \begin{verbatim} - Inductive sig_n [T1,...,Tn:Set; P:T1->...->Tn->Prop] : Set := - exist_n : (x1:T1)...(xn:Tn)(P x1 ... xn) -> (sig_n T1 ... Tn P). - \end{verbatim} *) - -let sig_n n = - let id = make_ident "sig_" (Some n) in - let l1n = Util.interval 1 n in - let lT = List.map (fun i -> make_ident "T" (Some i)) l1n in - let lx = List.map (fun i -> make_ident "x" (Some i)) l1n in - let idp = make_ident "P" None in - let params = - let typ = List.fold_right (fun _ c -> mkArrow (mkRel n) c) lT mkProp in - (idp, LocalAssum typ) :: - (List.rev_map (fun id -> (id, LocalAssum mkSet)) lT) - in - let lc = - let app_sig = mkApp(mkRel (2*n+3), - Array.init (n+1) (fun i -> mkRel (2*n+2-i))) in - let app_p = mkApp(mkRel (n+1), - Array.init n (fun i -> mkRel (n-i))) in - let c = mkArrow app_p app_sig in - List.fold_right (fun id c -> mkProd (Name id, mkRel (n+1), c)) lx c - in - let cname = make_ident "exist_" (Some n) in - Declare.declare_mind - { mind_entry_finite = true; - mind_entry_inds = - [ { mind_entry_params = params; - mind_entry_typename = id; - mind_entry_arity = mkSet; - mind_entry_consnames = [ cname ]; - mind_entry_lc = [ lc ] } ] } - -(*s On the fly generation of needed (possibly dependent) tuples. *) - -let check_product_n n = - if n > 2 then - let s = Printf.sprintf "tuple_%d" n in - if not (tuple_exists (id_of_string s)) then tuple_n n - -let check_dep_product_n n = - if n > 1 then - let s = Printf.sprintf "sig_%d" n in - if not (tuple_exists (id_of_string s)) then ignore (sig_n n) - -(*s Constructors for the tuples. *) - -let pair = ConstructRef ((coq_constant ["Init"; "Datatypes"] "prod",0),1) -let exist = ConstructRef ((coq_constant ["Init"; "Specif"] "sig",0),1) - -let tuple_ref dep n = - if n = 2 & not dep then - pair - else - let n = n - (if dep then 1 else 0) in - if dep then - if n = 1 then - exist - else begin - let id = make_ident "exist_" (Some n) in - if not (tuple_exists id) then ignore (sig_n n); - Nametab.locate (make_short_qualid id) - end - else begin - let id = make_ident "Build_tuple_" (Some n) in - if not (tuple_exists id) then tuple_n n; - Nametab.locate (make_short_qualid id) - end - -(* Binders. *) - -let trad_binder avoid nenv id = function - | CC_untyped_binder -> RHole (dummy_loc,BinderType (Name id)) - | CC_typed_binder ty -> Detyping.detype (false,Global.env()) avoid nenv ty - -let rec push_vars avoid nenv = function - | [] -> ([],avoid,nenv) - | (id,b) :: bl -> - let b' = trad_binder avoid nenv id b in - let bl',avoid',nenv' = - push_vars (id :: avoid) (add_name (Name id) nenv) bl - in - ((id,b') :: bl', avoid', nenv') - -let rec raw_lambda bl v = match bl with - | [] -> - v - | (id,ty) :: bl' -> - RLambda (dummy_loc, Name id, ty, raw_lambda bl' v) - -(* The translation itself is quite easy. - letin are translated into Cases constructions *) - -let rawconstr_of_prog p = - let rec trad avoid nenv = function - | CC_var id -> - RVar (dummy_loc, id) - - (*i optimisation : let x = <constr> in e2 => e2[x<-constr] - | CC_letin (_,_,[id,_],CC_expr c,e2) -> - real_subst_in_constr [id,c] (trad e2) - | CC_letin (_,_,([_] as b),CC_expr e1,e2) -> - let (b',avoid',nenv') = push_vars avoid nenv b in - let c1 = Detyping.detype avoid nenv e1 - and c2 = trad avoid' nenv' e2 in - let id = Name (fst (List.hd b')) in - RLetIn (dummy_loc, id, c1, c2) - i*) - - | CC_letin (_,_,([_] as b),e1,e2) -> - let (b',avoid',nenv') = push_vars avoid nenv b in - let c1 = trad avoid nenv e1 - and c2 = trad avoid' nenv' e2 in - RApp (dummy_loc, raw_lambda b' c2, [c1]) - - | CC_letin (dep,ty,bl,e1,e2) -> - let (bl',avoid',nenv') = push_vars avoid nenv bl in - let c1 = trad avoid nenv e1 - and c2 = trad avoid' nenv' e2 in - ROrderedCase (dummy_loc, LetStyle, None, c1, [| raw_lambda bl' c2 |], ref None) - - | CC_lam (bl,e) -> - let bl',avoid',nenv' = push_vars avoid nenv bl in - let c = trad avoid' nenv' e in - raw_lambda bl' c - - | CC_app (f,args) -> - let c = trad avoid nenv f - and cargs = List.map (trad avoid nenv) args in - RApp (dummy_loc, c, cargs) - - | CC_tuple (_,_,[e]) -> - trad avoid nenv e - - | CC_tuple (false,_,[e1;e2]) -> - let c1 = trad avoid nenv e1 - and c2 = trad avoid nenv e2 in - RApp (dummy_loc, RRef (dummy_loc,pair), - [RHole (dummy_loc,ImplicitArg (pair,1)); - RHole (dummy_loc,ImplicitArg (pair,2));c1;c2]) - - | CC_tuple (dep,tyl,l) -> - let n = List.length l in - let cl = List.map (trad avoid nenv) l in - let tuple = tuple_ref dep n in - let tyl = List.map (Detyping.detype (false,Global.env()) avoid nenv) tyl in - let args = tyl @ cl in - RApp (dummy_loc, RRef (dummy_loc, tuple), args) - - | CC_case (ty,b,el) -> - let c = trad avoid nenv b in - let cl = List.map (trad avoid nenv) el in - let ty = Detyping.detype (false,Global.env()) avoid nenv ty in - ROrderedCase (dummy_loc, RegularStyle, Some ty, c, Array.of_list cl, ref None) - - | CC_expr c -> - Detyping.detype (false,Global.env()) avoid nenv c - - | CC_hole c -> - RCast (dummy_loc, RHole (dummy_loc, QuestionMark), - Detyping.detype (false,Global.env()) avoid nenv c) - - in - trad [] empty_names_context p diff --git a/contrib/correctness/pcic.mli b/contrib/correctness/pcic.mli deleted file mode 100644 index 67b152f3..00000000 --- a/contrib/correctness/pcic.mli +++ /dev/null @@ -1,24 +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 *) - -(*i $Id: pcic.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) - -open Past -open Rawterm - -(* On-the-fly generation of needed (possibly dependent) tuples. *) - -val check_product_n : int -> unit -val check_dep_product_n : int -> unit - -(* transforms intermediate functional programs into (raw) CIC terms *) - -val rawconstr_of_prog : cc_term -> rawconstr - 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 - - diff --git a/contrib/correctness/pcicenv.mli b/contrib/correctness/pcicenv.mli deleted file mode 100644 index 365fa960..00000000 --- a/contrib/correctness/pcicenv.mli +++ /dev/null @@ -1,38 +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.mli 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Penv -open Names -open Term -open Sign - -(* Translation of local programs environments into Coq signatures. - * It is mainly used to type the pre/post conditions in the good - * environment *) - -(* cci_sign_of: uniquement les objets purement fonctionnels de l'env. *) -val cci_sign_of : Prename.t -> local_env -> named_context - -(* env. Coq avec seulement les variables X de l'env. *) -val now_sign_of : Prename.t -> local_env -> named_context - -(* + les variables X@d pour toutes les dates de l'env. *) -val before_sign_of : Prename.t -> local_env -> named_context - -(* + les variables `avant' X@ *) -val before_after_sign_of : Prename.t -> local_env -> named_context -val before_after_result_sign_of : ((identifier * constr) option) - -> Prename.t -> local_env -> named_context - -(* env. des programmes traduits, avec les variables rennomées *) -val trad_sign_of : Prename.t -> local_env -> named_context - diff --git a/contrib/correctness/pdb.ml b/contrib/correctness/pdb.ml deleted file mode 100644 index 759e9133..00000000 --- a/contrib/correctness/pdb.ml +++ /dev/null @@ -1,165 +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: pdb.ml 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Names -open Term -open Termops -open Nametab -open Constrintern - -open Ptype -open Past -open Penv - -let cci_global id = - try - global_reference id - with - _ -> raise Not_found - -let lookup_var ids locop id = - if List.mem id ids then - None - else begin - try Some (cci_global id) - with Not_found -> Perror.unbound_variable id locop - end - -let check_ref idl loc id = - if (not (List.mem id idl)) & (not (Penv.is_global id)) then - Perror.unbound_reference id loc - -(* db types : only check the references for the moment *) - -let rec check_type_v refs = function - | Ref v -> - check_type_v refs v - | Array (c,v) -> - check_type_v refs v - | Arrow (bl,c) -> - check_binder refs c bl - | TypePure _ -> - () - -and check_type_c refs ((_,v),e,_,_) = - check_type_v refs v; - List.iter (check_ref refs None) (Peffect.get_reads e); - List.iter (check_ref refs None) (Peffect.get_writes e) - (* TODO: check_condition on p and q *) - -and check_binder refs c = function - | [] -> - check_type_c refs c - | (id, BindType (Ref _ | Array _ as v)) :: bl -> - check_type_v refs v; - check_binder (id :: refs) c bl - | (_, BindType v) :: bl -> - check_type_v refs v; - check_binder refs c bl - | _ :: bl -> - check_binder refs c bl - -(* db binders *) - -let rec db_binders ((tids,pids,refs) as idl) = function - | [] -> - idl, [] - | (id, BindType (Ref _ | Array _ as v)) as b :: rem -> - check_type_v refs v; - let idl',rem' = db_binders (tids,pids,id::refs) rem in - idl', b :: rem' - | (id, BindType v) as b :: rem -> - check_type_v refs v; - let idl',rem' = db_binders (tids,id::pids,refs) rem in - idl', b :: rem' - | ((id, BindSet) as t) :: rem -> - let idl',rem' = db_binders (id::tids,pids,refs) rem in - idl', t :: rem' - | a :: rem -> - let idl',rem' = db_binders idl rem in idl', a :: rem' - - -(* db programs *) - -let db_prog e = - (* tids = type identifiers, ids = variables, refs = references and arrays *) - let rec db_desc ((tids,ids,refs) as idl) = function - | (Variable x) as t -> - (match lookup_var ids (Some e.loc) x with - None -> t - | Some c -> Expression c) - | (Acc x) as t -> - check_ref refs (Some e.loc) x; - t - | Aff (x,e1) -> - check_ref refs (Some e.loc) x; - Aff (x, db idl e1) - | TabAcc (b,x,e1) -> - check_ref refs (Some e.loc) x; - TabAcc(b,x,db idl e1) - | TabAff (b,x,e1,e2) -> - check_ref refs (Some e.loc) x; - TabAff (b,x, db idl e1, db idl e2) - | Seq bl -> - Seq (List.map (function - Statement p -> Statement (db idl p) - | x -> x) bl) - | If (e1,e2,e3) -> - If (db idl e1, db idl e2, db idl e3) - | While (b,inv,var,bl) -> - let bl' = List.map (function - Statement p -> Statement (db idl p) - | x -> x) bl in - While (db idl b, inv, var, bl') - - | Lam (bl,e) -> - let idl',bl' = db_binders idl bl in Lam(bl', db idl' e) - | Apply (e1,l) -> - Apply (db idl e1, List.map (db_arg idl) l) - | SApp (dl,l) -> - SApp (dl, List.map (db idl) l) - | LetRef (x,e1,e2) -> - LetRef (x, db idl e1, db (tids,ids,x::refs) e2) - | Let (x,e1,e2) -> - Let (x, db idl e1, db (tids,x::ids,refs) e2) - - | LetRec (f,bl,v,var,e) -> - let (tids',ids',refs'),bl' = db_binders idl bl in - check_type_v refs' v; - LetRec (f, bl, v, var, db (tids',f::ids',refs') e) - - | Debug (s,e1) -> - Debug (s, db idl e1) - - | Expression _ as x -> x - | PPoint (s,d) -> PPoint (s, db_desc idl d) - - and db_arg ((tids,_,refs) as idl) = function - | Term ({ desc = Variable id } as t) -> - if List.mem id refs then Refarg id else Term (db idl t) - | Term t -> Term (db idl t) - | Type v as ty -> check_type_v refs v; ty - | Refarg _ -> assert false - - and db idl e = - { desc = db_desc idl e.desc ; - pre = e.pre; post = e.post; - loc = e.loc; info = e.info } - - in - let ids = Termops.ids_of_named_context (Global.named_context ()) in - (* TODO: separer X:Set et x:V:Set - virer le reste (axiomes, etc.) *) - let vars,refs = all_vars (), all_refs () in - db ([],vars@ids,refs) e -;; - diff --git a/contrib/correctness/pdb.mli b/contrib/correctness/pdb.mli deleted file mode 100644 index d6e647b7..00000000 --- a/contrib/correctness/pdb.mli +++ /dev/null @@ -1,25 +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: pdb.mli 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Ptype -open Past - - -(* Here we separate local and global variables, we check the use of - * references and arrays w.r.t the local and global environments, etc. - * These functions directly raise UserError exceptions on bad programs. - *) - -val check_type_v : Names.identifier list -> 'a ml_type_v -> unit - -val db_prog : program -> program - diff --git a/contrib/correctness/peffect.ml b/contrib/correctness/peffect.ml deleted file mode 100644 index faf5f3d3..00000000 --- a/contrib/correctness/peffect.ml +++ /dev/null @@ -1,159 +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: peffect.ml 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Names -open Nameops -open Pmisc - -(* The type of effects. - * - * An effect is composed of two lists (r,w) of variables. - * The first one is the list of read-only variables - * and the second one is the list of read-write variables. - * - * INVARIANT: 1. each list is sorted in decreasing order for Pervasives.compare - * 2. there are no duplicate elements in each list - * 3. the two lists are disjoint - *) - -type t = identifier list * identifier list - - -(* the empty effect *) - -let bottom = ([], []) - -(* basic operations *) - -let push x l = - let rec push_rec = function - [] -> [x] - | (y::rem) as l -> - if x = y then l else if x > y then x::l else y :: push_rec rem - in - push_rec l - -let basic_remove x l = - let rec rem_rec = function - [] -> [] - | y::l -> if x = y then l else y :: rem_rec l - in - rem_rec l - -let mem x (r,w) = (List.mem x r) or (List.mem x w) - -let rec basic_union = function - [], s2 -> s2 - | s1, [] -> s1 - | ((v1::l1) as s1), ((v2::l2) as s2) -> - if v1 > v2 then - v1 :: basic_union (l1,s2) - else if v1 < v2 then - v2 :: basic_union (s1,l2) - else - v1 :: basic_union (l1,l2) - -(* adds reads and writes variables *) - -let add_read id ((r,w) as e) = - (* if the variable is already a RW it is ok, otherwise adds it as a RO. *) - if List.mem id w then - e - else - push id r, w - -let add_write id (r,w) = - (* if the variable is a RO then removes it from RO. Adds it to RW. *) - if List.mem id r then - basic_remove id r, push id w - else - r, push id w - -(* access *) - -let get_reads = basic_union -let get_writes = snd -let get_repr e = (get_reads e, get_writes e) - -(* tests *) - -let is_read (r,_) id = List.mem id r -let is_write (_,w) id = List.mem id w - -(* union and disjunction *) - -let union (r1,w1) (r2,w2) = basic_union (r1,r2), basic_union (w1,w2) - -let rec diff = function - [], s2 -> [] - | s1, [] -> s1 - | ((v1::l1) as s1), ((v2::l2) as s2) -> - if v1 > v2 then - v1 :: diff (l1,s2) - else if v1 < v2 then - diff (s1,l2) - else - diff (l1,l2) - -let disj (r1,w1) (r2,w2) = - let w1_w2 = diff (w1,w2) and w2_w1 = diff (w2,w1) in - let r = basic_union (basic_union (r1,r2), basic_union (w1_w2,w2_w1)) - and w = basic_union (w1,w2) in - r,w - -(* comparison relation *) - -let le e1 e2 = failwith "effects: le: not yet implemented" - -let inf e1 e2 = failwith "effects: inf: not yet implemented" - -(* composition *) - -let compose (r1,w1) (r2,w2) = - let r = basic_union (r1, diff (r2,w1)) in - let w = basic_union (w1,w2) in - r,w - -(* remove *) - -let remove (r,w) name = basic_remove name r, basic_remove name w - -(* substitution *) - -let subst_list (x,x') l = - if List.mem x l then push x' (basic_remove x l) else l - -let subst_one (r,w) s = subst_list s r, subst_list s w - -let subst s e = List.fold_left subst_one e s - -(* pretty-print *) - -open Pp -open Util -open Himsg - -let pp (r,w) = - hov 0 (if r<>[] then - (str"reads " ++ - prlist_with_sep (fun () -> (str"," ++ spc ())) pr_id r) - else (mt ()) ++ - spc () ++ - if w<>[] then - (str"writes " ++ - prlist_with_sep (fun ()-> (str"," ++ spc ())) pr_id w) - else (mt ()) -) - -let ppr e = - Pp.pp (pp e) - diff --git a/contrib/correctness/peffect.mli b/contrib/correctness/peffect.mli deleted file mode 100644 index 9a10dea4..00000000 --- a/contrib/correctness/peffect.mli +++ /dev/null @@ -1,42 +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: peffect.mli 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Names - -(* The abstract type of effects *) - -type t - -val bottom : t -val add_read : identifier -> t -> t -val add_write : identifier -> t -> t - -val get_reads : t -> identifier list -val get_writes : t -> identifier list -val get_repr : t -> (identifier list) * (identifier list) - -val is_read : t -> identifier -> bool (* read-only *) -val is_write : t -> identifier -> bool (* read-write *) - -val compose : t -> t -> t - -val union : t -> t -> t -val disj : t -> t -> t - -val remove : t -> identifier -> t - -val subst : (identifier * identifier) list -> t -> t - - -val pp : t -> Pp.std_ppcmds -val ppr : t -> unit - 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 -> () - diff --git a/contrib/correctness/penv.mli b/contrib/correctness/penv.mli deleted file mode 100644 index 6743b465..00000000 --- a/contrib/correctness/penv.mli +++ /dev/null @@ -1,87 +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.mli 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Ptype -open Past -open Names -open Libnames -open Term - -(* Environment for imperative programs. - * - * Here we manage the global environment, which is imperative, - * and we provide a functional local environment. - * - * The most important functions, is_in_env, type_in_env and fold_all - * first look in the local environment then in the global one. - *) - -(* local environments *) - -type local_env - -val empty : local_env -val add : (identifier * type_v) -> local_env -> local_env -val add_set : identifier -> local_env -> local_env -val is_local : local_env -> identifier -> bool -val is_local_set : local_env -> identifier -> bool - -(* typed programs *) - -type typing_info = { - env : local_env; - kappa : constr ml_type_c -} - -type typed_program = (typing_info, constr) t - -(* global environment *) - -val add_global : identifier -> type_v -> typed_program option -> object_name -val add_global_set : identifier -> object_name -val is_global : identifier -> bool -val is_global_set : identifier -> bool -val lookup_global : identifier -> type_v - -val all_vars : unit -> identifier list -val all_refs : unit -> identifier list - -(* a table keeps the program (for extraction) *) - -val find_pgm : identifier -> typed_program option - -(* a table keeps the initializations of mutable objects *) - -val initialize : identifier -> constr -> unit -val find_init : identifier -> constr - -(* access in env (local then global) *) - -val type_in_env : local_env -> identifier -> type_v -val is_in_env : local_env -> identifier -> bool - -type type_info = Set | TypeV of type_v -val fold_all : (identifier * type_info -> 'a -> 'a) -> local_env -> 'a -> 'a - -(* local environnements also contains a list of recursive functions - * with the associated variant *) - -val add_recursion : identifier * (identifier*variant) -> local_env -> local_env -val find_recursion : identifier -> local_env -> identifier * variant - -(* 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 *) - -val new_edited : identifier -> type_v * typed_program -> unit -val is_edited : identifier -> bool -val register : identifier -> identifier -> unit - diff --git a/contrib/correctness/perror.ml b/contrib/correctness/perror.ml deleted file mode 100644 index 8415e96d..00000000 --- a/contrib/correctness/perror.ml +++ /dev/null @@ -1,172 +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: perror.ml 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Pp -open Util -open Names -open Nameops -open Term -open Himsg - -open Ptype -open Past - -let is_mutable = function Ref _ | Array _ -> true | _ -> false -let is_pure = function TypePure _ -> true | _ -> false - -let raise_with_loc = function - | None -> raise - | Some loc -> Stdpp.raise_with_loc loc - -let unbound_variable id loc = - raise_with_loc loc - (UserError ("Perror.unbound_variable", - (hov 0 (str"Unbound variable" ++ spc () ++ pr_id id ++ fnl ())))) - -let unbound_reference id loc = - raise_with_loc loc - (UserError ("Perror.unbound_reference", - (hov 0 (str"Unbound reference" ++ spc () ++ pr_id id ++ fnl ())))) - -let clash id loc = - raise_with_loc loc - (UserError ("Perror.clash", - (hov 0 (str"Clash with previous constant" ++ spc () ++ - str(string_of_id id) ++ fnl ())))) - -let not_defined id = - raise - (UserError ("Perror.not_defined", - (hov 0 (str"The object" ++ spc () ++ pr_id id ++ spc () ++ - str"is not defined" ++ fnl ())))) - -let check_for_reference loc id = function - Ref _ -> () - | _ -> Stdpp.raise_with_loc loc - (UserError ("Perror.check_for_reference", - hov 0 (pr_id id ++ spc () ++ - str"is not a reference"))) - -let check_for_array loc id = function - Array _ -> () - | _ -> Stdpp.raise_with_loc loc - (UserError ("Perror.check_for_array", - hov 0 (pr_id id ++ spc () ++ - str"is not an array"))) - -let is_constant_type s = function - TypePure c -> - let id = id_of_string s in - let c' = Constrintern.global_reference id in - Reductionops.is_conv (Global.env()) Evd.empty c c' - | _ -> false - -let check_for_index_type loc v = - let is_index = is_constant_type "Z" v in - if not is_index then - Stdpp.raise_with_loc loc - (UserError ("Perror.check_for_index", - hov 0 (str"This expression is an index" ++ spc () ++ - str"and should have type int (Z)"))) - -let check_no_effect loc ef = - if not (Peffect.get_writes ef = []) then - Stdpp.raise_with_loc loc - (UserError ("Perror.check_no_effect", - hov 0 (str"A boolean should not have side effects" -))) - -let should_be_boolean loc = - Stdpp.raise_with_loc loc - (UserError ("Perror.should_be_boolean", - hov 0 (str"This expression is a test:" ++ spc () ++ - str"it should have type bool"))) - -let test_should_be_annotated loc = - Stdpp.raise_with_loc loc - (UserError ("Perror.test_should_be_annotated", - hov 0 (str"This test should be annotated"))) - -let if_branches loc = - Stdpp.raise_with_loc loc - (UserError ("Perror.if_branches", - hov 0 (str"The two branches of an `if' expression" ++ spc () ++ - str"should have the same type"))) - -let check_for_not_mutable loc v = - if is_mutable v then - Stdpp.raise_with_loc loc - (UserError ("Perror.check_for_not_mutable", - hov 0 (str"This expression cannot be a mutable"))) - -let check_for_pure_type loc v = - if not (is_pure v) then - Stdpp.raise_with_loc loc - (UserError ("Perror.check_for_pure_type", - hov 0 (str"This expression must be pure" ++ spc () ++ - str"(neither a mutable nor a function)"))) - -let check_for_let_ref loc v = - if not (is_pure v) then - Stdpp.raise_with_loc loc - (UserError ("Perror.check_for_let_ref", - hov 0 (str"References can only be bound in pure terms"))) - -let informative loc s = - Stdpp.raise_with_loc loc - (UserError ("Perror.variant_informative", - hov 0 (str s ++ spc () ++ str"must be informative"))) - -let variant_informative loc = informative loc "Variant" -let should_be_informative loc = informative loc "This term" - -let app_of_non_function loc = - Stdpp.raise_with_loc loc - (UserError ("Perror.app_of_non_function", - hov 0 (str"This term cannot be applied" ++ spc () ++ - str"(either it is not a function" ++ spc () ++ - str"or it is applied to non pure arguments)"))) - -let partial_app loc = - Stdpp.raise_with_loc loc - (UserError ("Perror.partial_app", - hov 0 (str"This function does not have" ++ - spc () ++ str"the right number of arguments"))) - -let expected_type loc s = - Stdpp.raise_with_loc loc - (UserError ("Perror.expected_type", - hov 0 (str"Argument is expected to have type" ++ spc () ++ s))) - -let expects_a_type id loc = - Stdpp.raise_with_loc loc - (UserError ("Perror.expects_a_type", - hov 0 (str"The argument " ++ pr_id id ++ spc () ++ - str"in this application is supposed to be a type"))) - -let expects_a_term id = - raise - (UserError ("Perror.expects_a_type", - hov 0 (str"The argument " ++ pr_id id ++ spc () ++ - str"in this application is supposed to be a term"))) - -let should_be_a_variable loc = - Stdpp.raise_with_loc loc - (UserError ("Perror.should_be_a_variable", - hov 0 (str"Argument should be a variable"))) - -let should_be_a_reference loc = - Stdpp.raise_with_loc loc - (UserError ("Perror.should_be_a_reference", - hov 0 (str"Argument of function should be a reference"))) - - diff --git a/contrib/correctness/perror.mli b/contrib/correctness/perror.mli deleted file mode 100644 index 45b2acdc..00000000 --- a/contrib/correctness/perror.mli +++ /dev/null @@ -1,47 +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: perror.mli 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Pp -open Util -open Names -open Ptype -open Past - -val unbound_variable : identifier -> loc option -> 'a -val unbound_reference : identifier -> loc option -> 'a - -val clash : identifier -> loc option -> 'a -val not_defined : identifier -> 'a - -val check_for_reference : loc -> identifier -> type_v -> unit -val check_for_array : loc -> identifier -> type_v -> unit - -val check_for_index_type : loc -> type_v -> unit -val check_no_effect : loc -> Peffect.t -> unit -val should_be_boolean : loc -> 'a -val test_should_be_annotated : loc -> 'a -val if_branches : loc -> 'a - -val check_for_not_mutable : loc -> type_v -> unit -val check_for_pure_type : loc -> type_v -> unit -val check_for_let_ref : loc -> type_v -> unit - -val variant_informative : loc -> 'a -val should_be_informative : loc -> 'a - -val app_of_non_function : loc -> 'a -val partial_app : loc -> 'a -val expected_type : loc -> std_ppcmds -> 'a -val expects_a_type : identifier -> loc -> 'a -val expects_a_term : identifier -> 'a -val should_be_a_variable : loc -> 'a -val should_be_a_reference : loc -> 'a diff --git a/contrib/correctness/pextract.ml b/contrib/correctness/pextract.ml deleted file mode 100644 index 407567ad..00000000 --- a/contrib/correctness/pextract.ml +++ /dev/null @@ -1,473 +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: pextract.ml 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Pp_control -open Pp -open Util -open System -open Names -open Term -open Himsg -open Reduction - -open Putil -open Ptype -open Past -open Penv -open Putil - -let extraction env c = - let ren = initial_renaming env in - let sign = Pcicenv.now_sign_of ren env in - let fsign = Mach.fsign_of_sign (Evd.mt_evd()) sign in - match Mach.infexecute (Evd.mt_evd()) (sign,fsign) c with - | (_,Inf j) -> j._VAL - | (_,Logic) -> failwith "Prog_extract.pp: should be informative" - -(* les tableaux jouent un role particulier, puisqu'ils seront extraits - * vers des tableaux ML *) - -let sp_access = coq_constant ["correctness"; "Arrays"] "access" -let access = ConstRef sp_access - -let has_array = ref false - -let pp_conversions () = - (str"\ -let rec int_of_pos = function - XH -> 1 - | XI p -> 2 * (int_of_pos p) + 1 - | XO p -> 2 * (int_of_pos p) - ++ ++ - -let int_of_z = function - ZERO -> 0 - | POS p -> int_of_pos p - | NEG p -> -(int_of_pos p) - ++ ++ -") (* '"' *) - -(* collect all section-path in a CIC constant *) - -let spset_of_cci env c = - let spl = Fw_env.collect (extraction env c) in - let sps = List.fold_left (fun e x -> SpSet.add x e) SpSet.empty spl in - has_array := !has_array or (SpSet.mem sp_access sps) ++ - SpSet.remove sp_access sps - - -(* collect all Coq constants and all pgms appearing in a given program *) - -let add_id env ((sp,ids) as s) id = - if is_local env id then - s - else if is_global id then - (sp,IdSet.add id ids) - else - try (SpSet.add (Nametab.sp_of_id FW id) sp,ids) with Not_found -> s - -let collect env = - let rec collect_desc env s = function - | Var x -> add_id env s x - | Acc x -> add_id env s x - | Aff (x,e1) -> add_id env (collect_rec env s e1) x - | TabAcc (_,x,e1) -> - has_array := true ++ - add_id env (collect_rec env s e1) x - | TabAff (_,x,e1,e2) -> - has_array := true ++ - add_id env (collect_rec env (collect_rec env s e1) e2) x - | Seq bl -> - List.fold_left (fun s st -> match st with - Statement p -> collect_rec env s p - | _ -> s) s bl - | If (e1,e2,e3) -> - collect_rec env (collect_rec env (collect_rec env s e1) e2) e3 - | While (b,_,_,bl) -> - let s = List.fold_left (fun s st -> match st with - Statement p -> collect_rec env s p - | _ -> s) s bl in - collect_rec env s b - | Lam (bl,e) -> - collect_rec (traverse_binders env bl) s e - | App (e1,l) -> - let s = List.fold_left (fun s a -> match a with - Term t -> collect_rec env s t - | Type _ | Refarg _ -> s) s l in - collect_rec env s e1 - | SApp (_,l) -> - List.fold_left (fun s a -> collect_rec env s a) s l - | LetRef (x,e1,e2) -> - let (_,v),_,_,_ = e1.info.kappa in - collect_rec (add (x,Ref v) env) (collect_rec env s e1) e2 - | LetIn (x,e1,e2) -> - let (_,v),_,_,_ = e1.info.kappa in - collect_rec (add (x,v) env) (collect_rec env s e1) e2 - | LetRec (f,bl,_,_,e) -> - let env' = traverse_binders env bl in - let env'' = add (f,make_arrow bl e.info.kappa) env' in - collect_rec env'' s e - | Debug (_,e1) -> collect_rec env s e1 - | PPoint (_,d) -> collect_desc env s d - | Expression c -> - let (sp,ids) = s in - let sp' = spset_of_cci env c in - SpSet.fold - (fun s (es,ei) -> - let id = basename s in - if is_global id then (*SpSet.add s*)es,IdSet.add id ei - else SpSet.add s es,ei) - sp' (sp,ids) - - and collect_rec env s p = collect_desc env s p.desc - - in - collect_rec env (SpSet.empty,IdSet.empty) - - -(* On a besoin de faire du renommage, tout comme pour l'extraction des - * termes Coq. En ce qui concerne les globaux, on utilise la table de - * Fwtoml. Pour les objects locaux, on introduit la structure de - * renommage rename_struct - *) - -module Ocaml_ren = Ocaml.OCaml_renaming - -let rename_global id = - let id' = Ocaml_ren.rename_global_term !Fwtoml.globals (Name id) in - Fwtoml.add_global_renaming (id,id') ++ - id' - -type rename_struct = { rn_map : identifier IdMap.t; - rn_avoid : identifier list } - -let rn_empty = { rn_map = IdMap.empty; rn_avoid = [] } - -let rename_local rn id = - let id' = Ocaml_ren.rename_term (!Fwtoml.globals@rn.rn_avoid) (Name id) in - { rn_map = IdMap.add id id' rn.rn_map; rn_avoid = id' :: rn.rn_avoid }, - id' - -let get_local_name rn id = IdMap.find id rn.rn_map - -let get_name env rn id = - if is_local env id then - get_local_name rn id - else - Fwtoml.get_global_name id - -let rec rename_binders rn = function - | [] -> rn - | (id,_) :: bl -> let rn',_ = rename_local rn id in rename_binders rn' bl - -(* on a bespoin d'un pretty-printer de constr particulier, qui reconnaisse - * les acces a des references et dans des tableaux, et qui de plus n'imprime - * pas de GENTERM lorsque des identificateurs ne sont pas visibles. - * Il est simplifie dans la mesure ou l'on a ici que des constantes et - * des applications. - *) - -let putpar par s = - if par then (str"(" ++ s ++ str")") else s - -let is_ref env id = - try - (match type_in_env env id with Ref _ -> true | _ -> false) - with - Not_found -> false - -let rec pp_constr env rn = function - | VAR id -> - if is_ref env id then - (str"!" ++ pID (get_name env rn id)) - else - pID (get_name env rn id) - | DOPN((Const _|MutInd _|MutConstruct _) as oper, _) -> - pID (Fwtoml.name_of_oper oper) - | DOPN(AppL,v) -> - if Array.length v = 0 then - (mt ()) - else begin - match v.(0) with - DOPN(Const sp,_) when sp = sp_access -> - (pp_constr env rn v.(3) ++ - str".(int_of_z " ++ pp_constr env rn v.(4) ++ str")") - | _ -> - hov 2 (putpar true (prvect_with_sep (fun () -> (spc ())) - (pp_constr env rn) v)) - end - | DOP2(Cast,c,_) -> pp_constr env rn c - | _ -> failwith "Prog_extract.pp_constr: unexpected constr" - - -(* pretty-print of imperative programs *) - -let collect_lambda = - let rec collect acc p = match p.desc with - | Lam(bl,t) -> collect (bl@acc) t - | x -> acc,p - in - collect [] - -let pr_binding rn = - prlist_with_sep (fun () -> (mt ())) - (function - | (id,(Untyped | BindType _)) -> - (str" " ++ pID (get_local_name rn id)) - | (id,BindSet) -> (mt ())) - -let pp_prog id = - let rec pp_d env rn par = function - | Var x -> pID (get_name env rn x) - | Acc x -> (str"!" ++ pID (get_name env rn x)) - | Aff (x,e1) -> (pID (get_name env rn x) ++ - str" := " ++ hov 0 (pp env rn false e1)) - | TabAcc (_,x,e1) -> - (pID (get_name env rn x) ++ - str".(int_of_z " ++ hov 0 (pp env rn true e1) ++ str")") - | TabAff (_,x,e1,e2) -> - (pID (get_name env rn x) ++ - str".(int_of_z " ++ hov 0 (pp env rn true e1) ++ str")" ++ - str" <-" ++ spc () ++ hov 2 (pp env rn false e2)) - | Seq bl -> - (str"begin" ++ fnl () ++ - str" " ++ hov 0 (pp_block env rn bl) ++ fnl () ++ - str"end") - | If (e1,e2,e3) -> - putpar par (str"if " ++ (pp env rn false e1) ++ - str" then" ++ fnl () ++ - str" " ++ hov 0 (pp env rn false e2) ++ fnl () ++ - str"else" ++ fnl () ++ - str" " ++ hov 0 (pp env rn false e3)) - (* optimisations : then begin .... end else begin ... end *) - | While (b,inv,_,bl) -> - (str"while " ++ (pp env rn false b) ++ str" do" ++ fnl () ++ - str" " ++ - hov 0 ((match inv with - None -> (mt ()) - | Some c -> (str"(* invariant: " ++ pTERM c.a_value ++ - str" *)" ++ fnl ())) ++ - pp_block env rn bl) ++ fnl () ++ - str"done") - | Lam (bl,e) -> - let env' = traverse_binders env bl in - let rn' = rename_binders rn bl in - putpar par - (hov 2 (str"fun" ++ pr_binding rn' bl ++ str" ->" ++ - spc () ++ pp env' rn' false e)) - | SApp ((Var id)::_, [e1; e2]) - when id = connective_and or id = connective_or -> - let conn = if id = connective_and then "&" else "or" in - putpar par - (hov 0 (pp env rn true e1 ++ spc () ++ str conn ++ spc () ++ - pp env rn true e2)) - | SApp ((Var id)::_, [e]) when id = connective_not -> - putpar par - (hov 0 (str"not" ++ spc () ++ pp env rn true e)) - | SApp _ -> - invalid_arg "Prog_extract.pp_prog (SApp)" - | App(e1,[]) -> - hov 0 (pp env rn false e1) - | App (e1,l) -> - putpar true - (hov 2 (pp env rn true e1 ++ - prlist (function - Term p -> (spc () ++ pp env rn true p) - | Refarg x -> (spc () ++ pID (get_name env rn x)) - | Type _ -> (mt ())) - l)) - | LetRef (x,e1,e2) -> - let (_,v),_,_,_ = e1.info.kappa in - let env' = add (x,Ref v) env in - let rn',x' = rename_local rn x in - putpar par - (hov 0 (str"let " ++ pID x' ++ str" = ref " ++ pp env rn false e1 ++ - str" in" ++ fnl () ++ pp env' rn' false e2)) - | LetIn (x,e1,e2) -> - let (_,v),_,_,_ = e1.info.kappa in - let env' = add (x,v) env in - let rn',x' = rename_local rn x in - putpar par - (hov 0 (str"let " ++ pID x' ++ str" = " ++ pp env rn false e1 ++ - str" in" ++ fnl () ++ pp env' rn' false e2)) - | LetRec (f,bl,_,_,e) -> - let env' = traverse_binders env bl in - let rn' = rename_binders rn bl in - let env'' = add (f,make_arrow bl e.info.kappa) env' in - let rn'',f' = rename_local rn' f in - putpar par - (hov 0 (str"let rec " ++ pID f' ++ pr_binding rn' bl ++ str" =" ++ fnl () ++ - str" " ++ hov 0 (pp env'' rn'' false e) ++ fnl () ++ - str"in " ++ pID f')) - | Debug (_,e1) -> pp env rn par e1 - | PPoint (_,d) -> pp_d env rn par d - | Expression c -> - pp_constr env rn (extraction env c) - - and pp_block env rn bl = - let bl = - map_succeed (function Statement p -> p | _ -> failwith "caught") bl - in - prlist_with_sep (fun () -> (str";" ++ fnl ())) - (fun p -> hov 0 (pp env rn false p)) bl - - and pp env rn par p = - (pp_d env rn par p.desc) - - and pp_mut v c = match v with - | Ref _ -> - (str"ref " ++ pp_constr empty rn_empty (extraction empty c)) - | Array (n,_) -> - (str"Array.create " ++ cut () ++ - putpar true - (str"int_of_z " ++ - pp_constr empty rn_empty (extraction empty n)) ++ - str" " ++ pp_constr empty rn_empty (extraction empty c)) - | _ -> invalid_arg "pp_mut" - in - let v = lookup_global id in - let id' = rename_global id in - if is_mutable v then - try - let c = find_init id in - hov 0 (str"let " ++ pID id' ++ str" = " ++ pp_mut v c) - with Not_found -> - errorlabstrm "Prog_extract.pp_prog" - (str"The variable " ++ pID id ++ - str" must be initialized first !") - else - match find_pgm id with - | None -> - errorlabstrm "Prog_extract.pp_prog" - (str"The program " ++ pID id ++ - str" must be realized first !") - | Some p -> - let bl,p = collect_lambda p in - let rn = rename_binders rn_empty bl in - let env = traverse_binders empty bl in - hov 0 (str"let " ++ pID id' ++ pr_binding rn bl ++ str" =" ++ fnl () ++ - str" " ++ hov 2 (pp env rn false p)) - -(* extraction des programmes impératifs/fonctionnels vers ocaml *) - -(* Il faut parfois importer des modules non ouverts, sinon - * Ocaml.OCaml_pp_file.pp echoue en disant "machin is not a defined - * informative object". Cela dit, ce n'est pas tres satisfaisant, vu que - * la constante existe quand meme: il vaudrait mieux contourner l'echec - * de ml_import.fwsp_of_id - *) - -let import sp = match repr_path sp with - | [m],_,_ -> - begin - try Library.import_export_module m true - with _ -> () - end - | _ -> () - -let pp_ocaml file prm = - has_array := false ++ - (* on separe objects Coq et programmes *) - let cic,pgms = - List.fold_left - (fun (sp,ids) id -> - if is_global id then (sp,IdSet.add id ids) else (IdSet.add id sp,ids)) - (IdSet.empty,IdSet.empty) prm.needed - in - (* on met les programmes dans l'ordre et pour chacun on recherche les - * objects Coq necessaires, que l'on rajoute a l'ensemble cic *) - let cic,_,pgms = - let o_pgms = fold_all (fun (id,_) l -> id::l) empty [] in - List.fold_left - (fun (cic,pgms,pl) id -> - if IdSet.mem id pgms then - let spl,pgms' = - try - (match find_pgm id with - | Some p -> collect empty p - | None -> - (try - let c = find_init id in - spset_of_cci empty c,IdSet.empty - with Not_found -> - SpSet.empty,IdSet.empty)) - with Not_found -> SpSet.empty,IdSet.empty - in - let cic' = - SpSet.fold - (fun sp cic -> import sp ++ IdSet.add (basename sp) cic) - spl cic - in - (cic',IdSet.union pgms pgms',id::pl) - else - (cic,pgms,pl)) - (cic,pgms,[]) o_pgms - in - let cic = IdSet.elements cic in - (* on pretty-print *) - let prm' = { needed = cic ++ expand = prm.expand ++ - expansion = prm.expansion ++ exact = prm.exact } - in - let strm = (Ocaml.OCaml_pp_file.pp_recursive prm' ++ - fnl () ++ fnl () ++ - if !has_array then pp_conversions() else (mt ()) ++ - prlist (fun p -> (pp_prog p ++ fnl () ++ str";;" ++ fnl () ++ fnl ())) - pgms -) - in - (* puis on ecrit dans le fichier *) - let chan = open_trapping_failure open_out file ".ml" in - let ft = with_output_to chan in - begin - try pP_with ft strm ++ pp_flush_with ft () - with e -> pp_flush_with ft () ++ close_out chan ++ raise e - end ++ - close_out chan - - -(* Initializations of mutable objects *) - -let initialize id com = - let loc = Ast.loc com in - let c = constr_of_com (Evd.mt_evd()) (initial_sign()) com in - let ty = - Reductionops.nf_betaiota (type_of (Evd.mt_evd()) (initial_sign()) c) in - try - let v = lookup_global id in - let ety = match v with - | Ref (TypePure c) -> c | Array (_,TypePure c) -> c - | _ -> raise Not_found - in - if conv (Evd.mt_evd()) ty ety then - initialize id c - else - errorlabstrm "Prog_extract.initialize" - (str"Not the expected type for the mutable " ++ pID id) - with Not_found -> - errorlabstrm "Prog_extract.initialize" - (pr_id id ++ str" is not a mutable") - -(* grammaire *) - -open Vernacinterp - -let _ = vinterp_add "IMPERATIVEEXTRACTION" - (function - | VARG_STRING file :: rem -> - let prm = parse_param rem in (fun () -> pp_ocaml file prm) - | _ -> assert false) - -let _ = vinterp_add "INITIALIZE" - (function - | [VARG_IDENTIFIER id; VARG_COMMAND com] -> - (fun () -> initialize id com) - | _ -> assert false) diff --git a/contrib/correctness/pextract.mli b/contrib/correctness/pextract.mli deleted file mode 100644 index 3492729c..00000000 --- a/contrib/correctness/pextract.mli +++ /dev/null @@ -1,17 +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: pextract.mli 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Names - -val pp_ocaml : string -> unit - - diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml deleted file mode 100644 index 076b11cd..00000000 --- a/contrib/correctness/pmisc.ml +++ /dev/null @@ -1,222 +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: pmisc.ml 8752 2006-04-27 19:37:33Z herbelin $ *) - -open Pp -open Util -open Names -open Nameops -open Term -open Libnames -open Topconstr - -(* debug *) - -let deb_mess s = - if !Options.debug then begin - msgnl s; pp_flush() - end - -let deb_print f x = - if !Options.debug then begin - msgnl (f x); pp_flush() - end - -let list_of_some = function - None -> [] - | Some x -> [x] - -let difference l1 l2 = - let rec diff = function - [] -> [] - | a::rem -> if List.mem a l2 then diff rem else a::(diff rem) - in - diff l1 - -(* TODO: these functions should be moved in the code of Coq *) - -let reraise_with_loc loc f x = - try f x with Util.UserError (_,_) as e -> Stdpp.raise_with_loc loc e - - -(* functions on names *) - -let at = if !Options.v7 then "@" else "'at'" - -let at_id id d = id_of_string ((string_of_id id) ^ at ^ d) - -let is_at id = - try - let _ = string_index_from (string_of_id id) 0 at in true - with Not_found -> - false - -let un_at id = - let s = string_of_id id in - try - let n = string_index_from s 0 at in - id_of_string (String.sub s 0 n), - String.sub s (n + String.length at) - (String.length s - n - String.length at) - with Not_found -> - invalid_arg "un_at" - -let renaming_of_ids avoid ids = - let rec rename avoid = function - [] -> [], avoid - | x::rem -> - let al,avoid = rename avoid rem in - let x' = next_ident_away x avoid in - (x,x')::al, x'::avoid - in - rename avoid ids - -let result_id = id_of_string "result" - -let adr_id id = id_of_string ("adr_" ^ (string_of_id id)) - -(* hypotheses names *) - -let next s r = function - Anonymous -> incr r; id_of_string (s ^ string_of_int !r) - | Name id -> id - -let reset_names,pre_name,post_name,inv_name, - test_name,bool_name,var_name,phi_name,for_name,label_name = - let pre = ref 0 in - let post = ref 0 in - let inv = ref 0 in - let test = ref 0 in - let bool = ref 0 in - let var = ref 0 in - let phi = ref 0 in - let forr = ref 0 in - let label = ref 0 in - (fun () -> - pre := 0; post := 0; inv := 0; test := 0; - bool := 0; var := 0; phi := 0; label := 0), - (next "Pre" pre), - (next "Post" post), - (next "Inv" inv), - (next "Test" test), - (fun () -> next "Bool" bool Anonymous), - (next "Variant" var), - (fun () -> next "rphi" phi Anonymous), - (fun () -> next "for" forr Anonymous), - (fun () -> string_of_id (next "Label" label Anonymous)) - -let default = id_of_string "x_" -let id_of_name = function Name id -> id | Anonymous -> default - - -(* functions on CIC terms *) - -let isevar = Evarutil.new_evar_in_sign (Global.env ()) - -(* Substitutions of variables by others. *) -let subst_in_constr alist = - let alist' = List.map (fun (id,id') -> (id, mkVar id')) alist in - replace_vars alist' - -(* -let subst_in_ast alist ast = - let rec subst = function - Nvar(l,s) -> Nvar(l,try List.assoc s alist with Not_found -> s) - | Node(l,s,args) -> Node(l,s,List.map subst args) - | Slam(l,so,a) -> Slam(l,so,subst a) (* TODO:enlever so de alist ? *) - | x -> x - in - subst ast -*) -(* -let subst_ast_in_ast alist ast = - let rec subst = function - Nvar(l,s) as x -> (try List.assoc s alist with Not_found -> x) - | Node(l,s,args) -> Node(l,s,List.map subst args) - | Slam(l,so,a) -> Slam(l,so,subst a) (* TODO:enlever so de alist ? *) - | x -> x - in - subst ast -*) - -let rec subst_in_ast alist = function - | CRef (Ident (loc,id)) -> - CRef (Ident (loc,(try List.assoc id alist with Not_found -> id))) - | x -> map_constr_expr_with_binders subst_in_ast List.remove_assoc alist x - -let rec subst_ast_in_ast alist = function - | CRef (Ident (_,id)) as x -> (try List.assoc id alist with Not_found -> x) - | x -> - map_constr_expr_with_binders subst_ast_in_ast List.remove_assoc alist x - -(* subst. of variables by constr *) -let real_subst_in_constr = replace_vars - -(* Coq constants *) - -let coq_constant d s = - Libnames.encode_kn - (make_dirpath (List.rev (List.map id_of_string ("Coq"::d)))) - (id_of_string s) - -let bool_sp = coq_constant ["Init"; "Datatypes"] "bool" -let coq_true = mkConstruct ((bool_sp,0),1) -let coq_false = mkConstruct ((bool_sp,0),2) - -let constant s = - let id = Constrextern.id_of_v7_string s in - Constrintern.global_reference id - -let connective_and = id_of_string "prog_bool_and" -let connective_or = id_of_string "prog_bool_or" -let connective_not = id_of_string "prog_bool_not" - -let is_connective id = - id = connective_and or id = connective_or or id = connective_not - -(* [conj i s] constructs the conjunction of two constr *) - -let conj i s = Term.applist (constant "and", [i; s]) - -(* [n_mkNamedProd v [xn,tn;...;x1,t1]] constructs the type - [(x1:t1)...(xn:tn)v] *) - -let rec n_mkNamedProd v = function - | [] -> v - | (id,ty) :: rem -> n_mkNamedProd (Term.mkNamedProd id ty v) rem - -(* [n_lambda v [xn,tn;...;x1,t1]] constructs the type [x1:t1]...[xn:tn]v *) - -let rec n_lambda v = function - | [] -> v - | (id,ty) :: rem -> n_lambda (Term.mkNamedLambda id ty v) rem - -(* [abstract env idl c] constructs [x1]...[xn]c where idl = [x1;...;xn] *) - -let abstract ids c = n_lambda c (List.rev ids) - -(* substitutivity (of kernel names, for modules management) *) - -open Ptype - -let rec type_v_knsubst s = function - | Ref v -> Ref (type_v_knsubst s v) - | Array (c, v) -> Array (subst_mps s c, type_v_knsubst s v) - | Arrow (bl, c) -> Arrow (List.map (binder_knsubst s) bl, type_c_knsubst s c) - | TypePure c -> TypePure (subst_mps s c) - -and type_c_knsubst s ((id,v),e,pl,q) = - ((id, type_v_knsubst s v), e, - List.map (fun p -> { p with p_value = subst_mps s p.p_value }) pl, - option_map (fun q -> { q with a_value = subst_mps s q.a_value }) q) - -and binder_knsubst s (id,b) = - (id, match b with BindType v -> BindType (type_v_knsubst s v) | _ -> b) diff --git a/contrib/correctness/pmisc.mli b/contrib/correctness/pmisc.mli deleted file mode 100644 index 9d96467f..00000000 --- a/contrib/correctness/pmisc.mli +++ /dev/null @@ -1,81 +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: pmisc.mli 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Names -open Term -open Ptype -open Topconstr - -(* Some misc. functions *) - -val reraise_with_loc : Util.loc -> ('a -> 'b) -> 'a -> 'b - -val list_of_some : 'a option -> 'a list -val difference : 'a list -> 'a list -> 'a list - -val at_id : identifier -> string -> identifier -val un_at : identifier -> identifier * string -val is_at : identifier -> bool - -val result_id : identifier -val adr_id : identifier -> identifier - -val renaming_of_ids : identifier list -> identifier list - -> (identifier * identifier) list * identifier list - -val reset_names : unit -> unit -val pre_name : name -> identifier -val post_name : name -> identifier -val inv_name : name -> identifier -val test_name : name -> identifier -val bool_name : unit -> identifier -val var_name : name -> identifier -val phi_name : unit -> identifier -val for_name : unit -> identifier -val label_name : unit -> string - -val id_of_name : name -> identifier - -(* CIC terms *) - -val isevar : constr - -val subst_in_constr : (identifier * identifier) list -> constr -> constr -val subst_in_ast : (identifier * identifier) list -> constr_expr -> constr_expr -val subst_ast_in_ast : - (identifier * constr_expr) list -> constr_expr -> constr_expr -val real_subst_in_constr : (identifier * constr) list -> constr -> constr - -val constant : string -> constr -val coq_constant : string list -> string -> kernel_name -val conj : constr -> constr -> constr - -val coq_true : constr -val coq_false : constr - -val connective_and : identifier -val connective_or : identifier -val connective_not : identifier -val is_connective : identifier -> bool - -val n_mkNamedProd : constr -> (identifier * constr) list -> constr -val n_lambda : constr -> (identifier * constr) list -> constr -val abstract : (identifier * constr) list -> constr -> constr - -val type_v_knsubst : substitution -> type_v -> type_v -val type_c_knsubst : substitution -> type_c -> type_c - -(* for debugging purposes *) - -val deb_mess : Pp.std_ppcmds -> unit -val deb_print : ('a -> Pp.std_ppcmds) -> 'a -> unit - diff --git a/contrib/correctness/pmlize.ml b/contrib/correctness/pmlize.ml deleted file mode 100644 index e812fa57..00000000 --- a/contrib/correctness/pmlize.ml +++ /dev/null @@ -1,320 +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: pmlize.ml 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Names -open Term -open Termast -open Pattern -open Matching - -open Pmisc -open Ptype -open Past -open Putil -open Prename -open Penv -open Peffect -open Ptyping -open Pmonad - - -let has_proof_part ren env c = - let sign = Pcicenv.trad_sign_of ren env in - let ty = Typing.type_of (Global.env_of_context sign) Evd.empty c in - Hipattern.is_matching_sigma (Reductionops.nf_betaiota ty) - -(* main part: translation of imperative programs into functional ones. - * - * [env] is the environment - * [ren] is the current renamings of variables - * [t] is the imperative program to translate, annotated with type+effects - * - * we return the translated program in type cc_term - *) - -let rec trad ren t = - let env = t.info.env in - trad_desc ren env t.info.kappa t.desc - -and trad_desc ren env ct d = - let (_,tt),eft,pt,qt = ct in - match d with - - | Expression c -> - let ids = get_reads eft in - let al = current_vars ren ids in - let c' = subst_in_constr al c in - if has_proof_part ren env c' then - CC_expr c' - else - let ty = trad_ml_type_v ren env tt in - make_tuple [ CC_expr c',ty ] qt ren env (current_date ren) - - | Variable id -> - if is_mutable_in_env env id then - invalid_arg "Mlise.trad_desc" - else if is_local env id then - CC_var id - else - CC_expr (constant (string_of_id id)) - - | Acc _ -> - failwith "Mlise.trad: pure terms are supposed to be expressions" - - | TabAcc (check, x, e1) -> - let _,ty_elem,_ = array_info ren env x in - let te1 = trad ren e1 in - let (_,ef1,p1,q1) = e1.info.kappa in - let w = get_writes ef1 in - let ren' = next ren w in - let id = id_of_string "index" in - let access = - make_raw_access ren' env (x,current_var ren' x) (mkVar id) - in - let t,ty = result_tuple ren' (current_date ren) env - (CC_expr access, ty_elem) (eft,qt) in - let t = - if check then - let h = make_pre_access ren env x (mkVar id) in - let_in_pre ty (anonymous_pre true h) t - else - t - in - make_let_in ren env te1 p1 - (current_vars ren' w,q1) (id,constant "Z") (t,ty) - - | Aff (x, e1) -> - let tx = trad_type_in_env ren env x in - let te1 = trad ren e1 in - let (_,ef1,p1,q1) = e1.info.kappa in - let w1 = get_writes ef1 in - let ren' = next ren (x::w1) in - let t_ty = result_tuple ren' (current_date ren) env - (CC_expr (constant "tt"), constant "unit") (eft,qt) - in - make_let_in ren env te1 p1 - (current_vars ren' w1,q1) (current_var ren' x,tx) t_ty - - | TabAff (check, x, e1, e2) -> - let _,ty_elem,ty_array = array_info ren env x in - let te1 = trad ren e1 in - let (_,ef1,p1,q1) = e1.info.kappa in - let w1 = get_writes ef1 in - let ren' = next ren w1 in - let te2 = trad ren' e2 in - let (_,ef2,p2,q2) = e2.info.kappa in - let w2 = get_writes ef2 in - let ren'' = next ren' w2 in - let id1 = id_of_string "index" in - let id2 = id_of_string "v" in - let ren''' = next ren'' [x] in - let t,ty = result_tuple ren''' (current_date ren) env - (CC_expr (constant "tt"), constant "unit") (eft,qt) in - let store = make_raw_store ren'' env (x,current_var ren'' x) (mkVar id1) - (mkVar id2) in - let t = make_let_in ren'' env (CC_expr store) [] ([],None) - (current_var ren''' x,ty_array) (t,ty) in - let t = make_let_in ren' env te2 p2 - (current_vars ren'' w2,q2) (id2,ty_elem) (t,ty) in - let t = - if check then - let h = make_pre_access ren' env x (mkVar id1) in - let_in_pre ty (anonymous_pre true h) t - else - t - in - make_let_in ren env te1 p1 - (current_vars ren' w1,q1) (id1,constant "Z") (t,ty) - - | Seq bl -> - let before = current_date ren in - let finish ren = function - Some (id,ty) -> - result_tuple ren before env (CC_var id, ty) (eft,qt) - | None -> - failwith "a block should contain at least one statement" - in - let bl = trad_block ren env bl in - make_block ren env finish bl - - | If (b, e1, e2) -> - let tb = trad ren b in - let _,efb,_,_ = b.info.kappa in - let ren' = next ren (get_writes efb) in - let te1 = trad ren' e1 in - let te2 = trad ren' e2 in - make_if ren env (tb,b.info.kappa) ren' (te1,e1.info.kappa) - (te2,e2.info.kappa) ct - - (* Translation of the while. *) - - | While (b, inv, var, bl) -> - let ren' = next ren (get_writes eft) in - let tb = trad ren' b in - let tbl = trad_block ren' env bl in - let var' = typed_var ren env var in - make_while ren env var' (tb,b.info.kappa) tbl (inv,ct) - - | Lam (bl, e) -> - let bl' = trad_binders ren env bl in - let env' = traverse_binders env bl in - let ren' = initial_renaming env' in - let te = trans ren' e in - CC_lam (bl', te) - - | SApp ([Variable id; Expression q1; Expression q2], [e1; e2]) - when id = connective_and or id = connective_or -> - let c = constant (string_of_id id) in - let te1 = trad ren e1 - and te2 = trad ren e2 in - let q1' = apply_post ren env (current_date ren) (anonymous q1) - and q2' = apply_post ren env (current_date ren) (anonymous q2) in - CC_app (CC_expr c, [CC_expr q1'.a_value; CC_expr q2'.a_value; te1; te2]) - - | SApp ([Variable id; Expression q], [e]) when id = connective_not -> - let c = constant (string_of_id id) in - let te = trad ren e in - let q' = apply_post ren env (current_date ren) (anonymous q) in - CC_app (CC_expr c, [CC_expr q'.a_value; te]) - - | SApp _ -> - invalid_arg "mlise.trad (SApp)" - - | Apply (f, args) -> - let trad_arg (ren,args) = function - | Term a -> - let ((_,tya),efa,_,_) as ca = a.info.kappa in - let ta = trad ren a in - let w = get_writes efa in - let ren' = next ren w in - ren', ta::args - | Refarg _ -> - ren, args - | Type v -> - let c = trad_ml_type_v ren env v in - ren, (CC_expr c)::args - in - let ren',targs = List.fold_left trad_arg (ren,[]) args in - let tf = trad ren' f in - let cf = f.info.kappa in - let c,(s,_,_),capp = effect_app ren env f args in - let tc_args = - List.combine - (List.rev targs) - (Util.map_succeed - (function - | Term x -> x.info.kappa - | Refarg _ -> failwith "caught" - | Type _ -> - (result_id,TypePure mkSet),Peffect.bottom,[],None) - args) - in - make_app env ren tc_args ren' (tf,cf) (c,s,capp) ct - - | LetRef (x, e1, e2) -> - let (_,v1),ef1,p1,q1 = e1.info.kappa in - let te1 = trad ren e1 in - let tv1 = trad_ml_type_v ren env v1 in - let env' = add (x,Ref v1) env in - let ren' = next ren [x] in - let (_,v2),ef2,p2,q2 = e2.info.kappa in - let tv2 = trad_ml_type_v ren' env' v2 in - let te2 = trad ren' e2 in - let ren'' = next ren' (get_writes ef2) in - let t,ty = result_tuple ren'' (current_date ren) env - (CC_var result_id, tv2) (eft,qt) in - let t = make_let_in ren' env' te2 p2 - (current_vars ren'' (get_writes ef2),q2) - (result_id,tv2) (t,ty) in - let t = make_let_in ren env te1 p1 - (current_vars ren' (get_writes ef1),q1) (x,tv1) (t,ty) - in - t - - | Let (x, e1, e2) -> - let (_,v1),ef1,p1,q1 = e1.info.kappa in - let te1 = trad ren e1 in - let tv1 = trad_ml_type_v ren env v1 in - let env' = add (x,v1) env in - let ren' = next ren (get_writes ef1) in - let (_,v2),ef2,p2,q2 = e2.info.kappa in - let tv2 = trad_ml_type_v ren' env' v2 in - let te2 = trad ren' e2 in - let ren'' = next ren' (get_writes ef2) in - let t,ty = result_tuple ren'' (current_date ren) env - (CC_var result_id, tv2) (eft,qt) in - let t = make_let_in ren' env' te2 p2 - (current_vars ren'' (get_writes ef2),q2) - (result_id,tv2) (t,ty) in - let t = make_let_in ren env te1 p1 - (current_vars ren' (get_writes ef1),q1) (x,tv1) (t,ty) - in - t - - | LetRec (f,bl,v,var,e) -> - let (_,ef,_,_) as c = - match tt with Arrow(_,c) -> c | _ -> assert false in - let bl' = trad_binders ren env bl in - let env' = traverse_binders env bl in - let ren' = initial_renaming env' in - let (phi0,var') = find_recursion f e.info.env in - let te = trad ren' e in - let t = make_letrec ren' env' (phi0,var') f bl' (te,e.info.kappa) c in - CC_lam (bl', t) - - | PPoint (s,d) -> - let ren' = push_date ren s in - trad_desc ren' env ct d - - | Debug _ -> failwith "Mlise.trad: Debug: not implemented" - - -and trad_binders ren env = function - | [] -> - [] - | (_,BindType (Ref _ | Array _))::bl -> - trad_binders ren env bl - | (id,BindType v)::bl -> - let tt = trad_ml_type_v ren env v in - (id, CC_typed_binder tt) :: (trad_binders ren env bl) - | (id,BindSet)::bl -> - (id, CC_typed_binder mkSet) :: (trad_binders ren env bl) - | (_,Untyped)::_ -> invalid_arg "trad_binders" - - -and trad_block ren env = function - | [] -> - [] - | (Assert c)::block -> - (Assert c)::(trad_block ren env block) - | (Label s)::block -> - let ren' = push_date ren s in - (Label s)::(trad_block ren' env block) - | (Statement e)::block -> - let te = trad ren e in - let _,efe,_,_ = e.info.kappa in - let w = get_writes efe in - let ren' = next ren w in - (Statement (te,e.info.kappa))::(trad_block ren' env block) - - -and trans ren e = - let env = e.info.env in - let _,ef,p,_ = e.info.kappa in - let ty = trad_ml_type_c ren env e.info.kappa in - let ids = get_reads ef in - let al = current_vars ren ids in - let c = trad ren e in - let c = abs_pre ren env (c,ty) p in - let bl = binding_of_alist ren env al in - make_abs (List.rev bl) c - diff --git a/contrib/correctness/pmlize.mli b/contrib/correctness/pmlize.mli deleted file mode 100644 index 1f8936f0..00000000 --- a/contrib/correctness/pmlize.mli +++ /dev/null @@ -1,20 +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: pmlize.mli 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Past -open Penv -open Names - -(* translation of imperative programs into intermediate functional programs *) - -val trans : Prename.t -> typed_program -> cc_term - diff --git a/contrib/correctness/pmonad.ml b/contrib/correctness/pmonad.ml deleted file mode 100644 index 8f1b5946..00000000 --- a/contrib/correctness/pmonad.ml +++ /dev/null @@ -1,665 +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.ml 8752 2006-04-27 19:37:33Z herbelin $ *) - -open Util -open Names -open Term -open Termast - -open Pmisc -open Putil -open Ptype -open Past -open Prename -open Penv -open Pcic -open Peffect - - -(* [product ren [y1,z1;...;yk,zk] q] constructs - * the (possibly dependent) tuple type - * - * z1 x ... x zk if no post-condition - * or \exists. y1:z1. ... yk:zk. (Q x1 ... xn) otherwise - * - * where the xi are given by the renaming [ren]. - *) - -let product_name = function - | 2 -> "prod" - | n -> check_product_n n; Printf.sprintf "tuple_%d" n - -let dep_product_name = function - | 1 -> "sig" - | n -> check_dep_product_n n; Printf.sprintf "sig_%d" n - -let product ren env before lo = function - | None -> (* non dependent case *) - begin match lo with - | [_,v] -> v - | _ -> - let s = product_name (List.length lo) in - Term.applist (constant s, List.map snd lo) - end - | Some q -> (* dependent case *) - let s = dep_product_name (List.length lo) in - let a' = apply_post ren env before q in - Term.applist (constant s, (List.map snd lo) @ [a'.a_value]) - -(* [arrow ren v pl] abstracts the term v over the pre-condition if any - * i.e. computes - * - * (P1 x1 ... xn) -> ... -> (Pk x1 ... xn) -> v - * - * where the xi are given by the renaming [ren]. - *) - -let arrow ren env v pl = - List.fold_left - (fun t p -> - if p.p_assert then t else Term.mkArrow (apply_pre ren env p).p_value t) - v pl - -(* [abstract_post ren env (e,q) (res,v)] abstract a post-condition q - * over the write-variables of e *) - -let rec abstract_post ren env (e,q) = - let after_id id = id_of_string ((string_of_id id) ^ "'") in - let (_,go) = Peffect.get_repr e in - let al = List.map (fun id -> (id,after_id id)) go in - let q = option_map (named_app (subst_in_constr al)) q in - let tgo = List.map (fun (id,aid) -> (aid, trad_type_in_env ren env id)) al in - option_map (named_app (abstract tgo)) q - -(* Translation of effects types in cic types. - * - * [trad_ml_type_v] and [trad_ml_type_c] translate types with effects - * into cic types. - *) - -and prod ren env g = - List.map - (fun id -> (current_var ren id, trad_type_in_env ren env id)) - g - -and input ren env e = - let i,_ = Peffect.get_repr e in - prod ren env i - -and output ren env ((id,v),e) = - let tv = trad_ml_type_v ren env v in - let _,o = Peffect.get_repr e in - (prod ren env o) @ [id,tv] - -and input_output ren env c = - let ((res,v),e,_,_) = c in - input ren env e, output ren env ((res,v),e) - -(* The function t -> \barre{t} on V and C. *) - -and trad_ml_type_c ren env c = - let ((res,v),e,p,q) = c in - let q = abstract_post ren env (e,q) in - let lo = output ren env ((res,v),e) in - let ty = product ren env (current_date ren) lo q in - let ty = arrow ren env ty p in - let li = input ren env e in - n_mkNamedProd ty li - -and trad_ml_type_v ren env = function - - | Ref _ | Array _ -> invalid_arg "Monad.trad_ml_type_v" - - | Arrow (bl, c) -> - let bl',ren',env' = - List.fold_left - (fun (bl,ren,env) b -> match b with - | (id,BindType ((Ref _ | Array _) as v)) -> - let env' = add (id,v) env in - let ren' = initial_renaming env' in - (bl,ren',env') - | (id,BindType v) -> - let tt = trad_ml_type_v ren env v in - let env' = add (id,v) env in - let ren' = initial_renaming env' in - (id,tt)::bl,ren',env' - | (id, BindSet) -> - (id,mkSet) :: bl,ren,env - | _ -> failwith "Monad: trad_ml_type_v: not yet implemented" - ) - ([],ren,env) bl - in - n_mkNamedProd (trad_ml_type_c ren' env' c) bl' - - | TypePure c -> - (apply_pre ren env (anonymous_pre false c)).p_value - -and trad_imp_type ren env = function - | Ref v -> trad_ml_type_v ren env v - | Array (c,v) -> Term.applist (constant "array", - [c; trad_ml_type_v ren env v]) - | _ -> invalid_arg "Monad.trad_imp_type" - -and trad_type_in_env ren env id = - let v = type_in_env env id in trad_imp_type ren env v - - - -(* bindings *) - -let binding_of_alist ren env al = - List.map - (fun (id,id') -> (id', CC_typed_binder (trad_type_in_env ren env id))) - al - - -(* [make_abs bl t p] abstracts t w.r.t binding list bl., that is - * [x1:t1]...[xn:tn]t. Returns t if the binding is empty. *) - -let make_abs bl t = match bl with - | [] -> t - | _ -> CC_lam (bl, t) - - -(* [result_tuple ren before env (res,v) (ef,q)] constructs the tuple - * - * (y1,...,yn,res,?::(q/ren y1 ... yn res)) - * - * where the yi are the values of the output of ef. - * if there is no yi and no post-condition, it is simplified in res itself. - *) - -let simple_constr_of_prog = function - | CC_expr c -> c - | CC_var id -> mkVar id - | _ -> assert false - -let make_tuple l q ren env before = match l with - | [e,_] when q = None -> - e - | _ -> - let tl = List.map snd l in - let dep,h,th = match q with - | None -> false,[],[] - | Some c -> - let args = List.map (fun (e,_) -> simple_constr_of_prog e) l in - let c = apply_post ren env before c in - true, - [ CC_hole (Term.applist (c.a_value, args)) ], (* hole *) - [ c.a_value ] (* type of the hole *) - in - CC_tuple (dep, tl @ th, (List.map fst l) @ h) - -let result_tuple ren before env (res,v) (ef,q) = - let ids = get_writes ef in - let lo = - (List.map (fun id -> - let id' = current_var ren id in - CC_var id', trad_type_in_env ren env id) ids) - @ [res,v] - in - let q = abstract_post ren env (ef,q) in - make_tuple lo q ren env before, - product ren env before lo q - - -(* [make_let_in ren env fe p (vo,q) (res,v) t] constructs the term - - [ let h1 = ?:P1 in ... let hn = ?:Pm in ] - let y1,y2,...,yn, res [,q] = fe in - t - - vo=[_,y1;...;_,ym] are list of renamings. - v is the type of res - *) - -let let_in_pre ty p t = - let h = p.p_value in - CC_letin (false, ty, [pre_name p.p_name,CC_typed_binder h], CC_hole h, t) - -let multiple_let_in_pre ty hl t = - List.fold_left (fun t h -> let_in_pre ty h t) t hl - -let make_let_in ren env fe p (vo,q) (res,tyres) (t,ty) = - let b = [res, CC_typed_binder tyres] in - let b',dep = match q with - | None -> [],false - | Some q -> [post_name q.a_name, CC_untyped_binder],true - in - let bl = (binding_of_alist ren env vo) @ b @ b' in - let tyapp = - let n = succ (List.length vo) in - let name = match q with None -> product_name n | _ -> dep_product_name n in - constant name - in - let t = CC_letin (dep, ty, bl, fe, t) in - multiple_let_in_pre ty (List.map (apply_pre ren env) p) t - - -(* [abs_pre ren env (t,ty) pl] abstracts a term t with respect to the - * list of pre-conditions [pl]. Some of them are real pre-conditions - * and others are assertions, according to the boolean field p_assert, - * so we construct the term - * [h1:P1]...[hn:Pn]let h'1 = ?:P'1 in ... let H'm = ?:P'm in t - *) - -let abs_pre ren env (t,ty) pl = - List.fold_left - (fun t p -> - if p.p_assert then - let_in_pre ty (apply_pre ren env p) t - else - let h = pre_name p.p_name in - CC_lam ([h,CC_typed_binder (apply_pre ren env p).p_value],t)) - t pl - - -(* [make_block ren env finish bl] builds the translation of a block - * finish is the function that is applied to the result at the end of the - * block. *) - -let make_block ren env finish bl = - let rec rec_block ren result = function - | [] -> - finish ren result - | (Assert c) :: block -> - let t,ty = rec_block ren result block in - let c = apply_assert ren env c in - let p = { p_assert = true; p_name = c.a_name; p_value = c.a_value } in - let_in_pre ty p t, ty - | (Label s) :: block -> - let ren' = push_date ren s in - rec_block ren' result block - | (Statement (te,info)) :: block -> - let (_,tye),efe,pe,qe = info in - let w = get_writes efe in - let ren' = next ren w in - let id = result_id in - let tye = trad_ml_type_v ren env tye in - let t = rec_block ren' (Some (id,tye)) block in - make_let_in ren env te pe (current_vars ren' w,qe) (id,tye) t, - snd t - in - let t,_ = rec_block ren None bl in - t - - -(* [make_app env ren args ren' (tf,cf) (cb,s,capp) c] - * constructs the application of [tf] to [args]. - * capp is the effect of application, after substitution (s) and cb before - *) - -let eq ty e1 e2 = - Term.applist (constant "eq", [ty; e1; e2]) - -let lt r e1 e2 = - Term.applist (r, [e1; e2]) - -let is_recursive env = function - | CC_var x -> - (try let _ = find_recursion x env in true with Not_found -> false) - | _ -> false - -let if_recursion env f = function - | CC_var x -> - (try let v = find_recursion x env in (f v x) with Not_found -> []) - | _ -> [] - -let dec_phi ren env s svi = - if_recursion env - (fun (phi0,(cphi,r,_)) f -> - let phi = subst_in_constr svi (subst_in_constr s cphi) in - let phi = (apply_pre ren env (anonymous_pre true phi)).p_value in - [CC_expr phi; CC_hole (lt r phi (mkVar phi0))]) - -let eq_phi ren env s svi = - if_recursion env - (fun (phi0,(cphi,_,a)) f -> - let phi = subst_in_constr svi (subst_in_constr s cphi) in - let phi = (apply_pre ren env (anonymous_pre true phi)).p_value in - [CC_hole (eq a phi phi)]) - -let is_ref_binder = function - | (_,BindType (Ref _ | Array _)) -> true - | _ -> false - -let make_app env ren args ren' (tf,cf) ((bl,cb),s,capp) c = - let ((_,tvf),ef,pf,qf) = cf in - let (_,eapp,papp,qapp) = capp in - let ((_,v),e,p,q) = c in - let bl = List.filter (fun b -> not (is_ref_binder b)) bl in - let recur = is_recursive env tf in - let before = current_date ren in - let ren'' = next ren' (get_writes ef) in - let ren''' = next ren'' (get_writes eapp) in - let res = result_id in - let vi,svi = - let ids = List.map fst bl in - let s = fresh (avoid ren ids) ids in - List.map snd s, s - in - let tyres = subst_in_constr svi (trad_ml_type_v ren env v) in - let t,ty = result_tuple ren''' before env (CC_var res, tyres) (e,q) in - let res_f = id_of_string "vf" in - let inf,outf = - let i,o = let _,e,_,_ = cb in get_reads e, get_writes e in - let apply_s = List.map (fun id -> try List.assoc id s with _ -> id) in - apply_s i, apply_s o - in - let fe = - let xi = List.rev (List.map snd (current_vars ren'' inf)) in - let holes = List.map (fun x -> (apply_pre ren'' env x).p_value) - (List.map (pre_app (subst_in_constr svi)) papp) in - CC_app ((if recur then tf else CC_var res_f), - (dec_phi ren'' env s svi tf) - @(List.map (fun id -> CC_var id) (vi @ xi)) - @(eq_phi ren'' env s svi tf) - @(List.map (fun c -> CC_hole c) holes)) - in - let qapp' = option_map (named_app (subst_in_constr svi)) qapp in - let t = - make_let_in ren'' env fe [] (current_vars ren''' outf,qapp') - (res,tyres) (t,ty) - in - let t = - if recur then - t - else - make_let_in ren' env tf pf - (current_vars ren'' (get_writes ef),qf) - (res_f,trad_ml_type_v ren env tvf) (t,ty) - in - let rec eval_args ren = function - | [] -> t - | (vx,(ta,((_,tva),ea,pa,qa)))::args -> - let w = get_writes ea in - let ren' = next ren w in - let t' = eval_args ren' args in - make_let_in ren env ta pa (current_vars ren' (get_writes ea),qa) - (vx,trad_ml_type_v ren env tva) (t',ty) - in - eval_args ren (List.combine vi args) - - -(* [make_if ren env (tb,cb) ren' (t1,c1) (t2,c2)] - * constructs the term corresponding to a if expression, i.e - * - * [p] let o1, b [,q1] = m1 [?::p1] in - * Cases b of - * R => let o2, v2 [,q2] = t1 [?::p2] in - * (proj (o1,o2)), v2 [,?::q] - * | S => let o2, v2 [,q2] = t2 [?::p2] in - * (proj (o1,o2)), v2 [,?::q] - *) - -let make_if_case ren env ty (b,qb) (br1,br2) = - let id_b,ty',ty1,ty2 = match qb with - | Some q -> - let q = apply_post ren env (current_date ren) q in - let (name,t1,t2) = Term.destLambda q.a_value in - q.a_name, - Term.mkLambda (name, t1, mkArrow t2 ty), - Term.mkApp (q.a_value, [| coq_true |]), - Term.mkApp (q.a_value, [| coq_false |]) - | None -> assert false - in - let n = test_name Anonymous in - CC_app (CC_case (ty', b, [CC_lam ([n,CC_typed_binder ty1], br1); - CC_lam ([n,CC_typed_binder ty2], br2)]), - [CC_var (post_name id_b)]) - -let make_if ren env (tb,cb) ren' (t1,c1) (t2,c2) c = - let ((_,tvb),eb,pb,qb) = cb in - let ((_,tv1),e1,p1,q1) = c1 in - let ((_,tv2),e2,p2,q2) = c2 in - let ((_,t),e,p,q) = c in - - let wb = get_writes eb in - let resb = id_of_string "resultb" in - let res = result_id in - let tyb = trad_ml_type_v ren' env tvb in - let tt = trad_ml_type_v ren env t in - - (* une branche de if *) - let branch (tv_br,e_br,p_br,q_br) f_br = - let w_br = get_writes e_br in - let ren'' = next ren' w_br in - let t,ty = result_tuple ren'' (current_date ren') env - (CC_var res,tt) (e,q) in - make_let_in ren' env f_br p_br (current_vars ren'' w_br,q_br) - (res,tt) (t,ty), - ty - in - let t1,ty1 = branch c1 t1 in - let t2,ty2 = branch c2 t2 in - let ty = ty1 in - let qb = force_bool_name qb in - let t = make_if_case ren env ty (CC_var resb,qb) (t1,t2) in - make_let_in ren env tb pb (current_vars ren' wb,qb) (resb,tyb) (t,ty) - - -(* [make_while ren env (cphi,r,a) (tb,cb) (te,ce) c] - * constructs the term corresponding to the while, i.e. - * - * [h:(I x)](well_founded_induction - * A R ?::(well_founded A R) - * [Phi:A] (x) Phi=phi(x)->(I x)-> \exists x'.res.(I x')/\(S x') - * [Phi_0:A][w:(Phi:A)(Phi<Phi_0)-> ...] - * [x][eq:Phi_0=phi(x)][h:(I x)] - * Cases (b x) of - * (left HH) => (x,?::(IS x)) - * | (right HH) => let x1,_,_ = (e x ?) in - * (w phi(x1) ? x1 ? ?) - * phi(x) x ? ?) - *) - -let id_phi = id_of_string "phi" -let id_phi0 = id_of_string "phi0" - -let make_body_while ren env phi_of a r id_phi0 id_w (tb,cb) tbl (i,c) = - let ((_,tvb),eb,pb,qb) = cb in - let (_,ef,_,is) = c in - - let ren' = next ren (get_writes ef) in - let before = current_date ren in - - let ty = - let is = abstract_post ren' env (ef,is) in - let _,lo = input_output ren env c in - product ren env before lo is - in - let resb = id_of_string "resultb" in - let tyb = trad_ml_type_v ren' env tvb in - let wb = get_writes eb in - - (* première branche: le test est vrai => e;w *) - let t1 = - make_block ren' env - (fun ren'' result -> match result with - | Some (id,_) -> - let v = List.rev (current_vars ren'' (get_writes ef)) in - CC_app (CC_var id_w, - [CC_expr (phi_of ren''); - CC_hole (lt r (phi_of ren'') (mkVar id_phi0))] - @(List.map (fun (_,id) -> CC_var id) v) - @(CC_hole (eq a (phi_of ren'') (phi_of ren''))) - ::(match i with - | None -> [] - | Some c -> - [CC_hole (apply_assert ren'' env c).a_value])), - ty - | None -> failwith "a block should contain at least one statement") - tbl - in - - (* deuxième branche: le test est faux => on sort de la boucle *) - let t2,_ = - result_tuple ren' before env - (CC_expr (constant "tt"),constant "unit") (ef,is) - in - - let b_al = current_vars ren' (get_reads eb) in - let qb = force_bool_name qb in - let t = make_if_case ren' env ty (CC_var resb,qb) (t1,t2) in - let t = - make_let_in ren' env tb pb (current_vars ren' wb,qb) (resb,tyb) (t,ty) - in - let t = - let pl = List.map (pre_of_assert false) (list_of_some i) in - abs_pre ren' env (t,ty) pl - in - let t = - CC_lam ([var_name Anonymous, - CC_typed_binder (eq a (mkVar id_phi0) (phi_of ren'))],t) - in - let bl = binding_of_alist ren env (current_vars ren' (get_writes ef)) in - make_abs (List.rev bl) t - - -let make_while ren env (cphi,r,a) (tb,cb) tbl (i,c) = - let (_,ef,_,is) = c in - let phi_of ren = (apply_pre ren env (anonymous_pre true cphi)).p_value in - let wf_a_r = Term.applist (constant "well_founded", [a; r]) in - - let before = current_date ren in - let ren' = next ren (get_writes ef) in - let al = current_vars ren' (get_writes ef) in - let v = - let _,lo = input_output ren env c in - let is = abstract_post ren' env (ef,is) in - match i with - | None -> product ren' env before lo is - | Some ci -> - Term.mkArrow (apply_assert ren' env ci).a_value - (product ren' env before lo is) - in - let v = Term.mkArrow (eq a (mkVar id_phi) (phi_of ren')) v in - let v = - n_mkNamedProd v - (List.map (fun (id,id') -> (id',trad_type_in_env ren env id)) al) - in - let tw = - Term.mkNamedProd id_phi a - (Term.mkArrow (lt r (mkVar id_phi) (mkVar id_phi0)) v) - in - let id_w = id_of_string "loop" in - let vars = List.rev (current_vars ren (get_writes ef)) in - let body = - make_body_while ren env phi_of a r id_phi0 id_w (tb,cb) tbl (i,c) - in - CC_app (CC_expr (constant "well_founded_induction"), - [CC_expr a; CC_expr r; - CC_hole wf_a_r; - CC_expr (Term.mkNamedLambda id_phi a v); - CC_lam ([id_phi0, CC_typed_binder a; - id_w, CC_typed_binder tw], - body); - CC_expr (phi_of ren)] - @(List.map (fun (_,id) -> CC_var id) vars) - @(CC_hole (eq a (phi_of ren) (phi_of ren))) - ::(match i with - | None -> [] - | Some c -> [CC_hole (apply_assert ren env c).a_value])) - - -(* [make_letrec ren env (phi0,(cphi,r,a)) bl (te,ce) c] - * constructs the term corresponding to the let rec i.e. - * - * [x][h:P(x)](well_founded_induction - * A R ?::(well_founded A R) - * [Phi:A] (bl) (x) Phi=phi(x)->(P x)-> \exists x'.res.(Q x x') - * [Phi_0:A][w:(Phi:A)(Phi<Phi_0)-> ...] - * [bl][x][eq:Phi_0=phi(x)][h:(P x)]te - * phi(x) bl x ? ?) - *) - -let make_letrec ren env (id_phi0,(cphi,r,a)) idf bl (te,ce) c = - let (_,ef,p,q) = c in - let phi_of ren = (apply_pre ren env (anonymous_pre true cphi)).p_value in - let wf_a_r = Term.applist (constant "well_founded", [a; r]) in - - let before = current_date ren in - let al = current_vars ren (get_reads ef) in - let v = - let _,lo = input_output ren env c in - let q = abstract_post ren env (ef,q) in - arrow ren env (product ren env (current_date ren) lo q) p - in - let v = Term.mkArrow (eq a (mkVar id_phi) (phi_of ren)) v in - let v = - n_mkNamedProd v - (List.map (fun (id,id') -> (id',trad_type_in_env ren env id)) al) - in - let v = - n_mkNamedProd v - (List.map (function (id,CC_typed_binder c) -> (id,c) - | _ -> assert false) (List.rev bl)) - in - let tw = - Term.mkNamedProd id_phi a - (Term.mkArrow (lt r (mkVar id_phi) (mkVar id_phi0)) v) - in - let vars = List.rev (current_vars ren (get_reads ef)) in - let body = - let al = current_vars ren (get_reads ef) in - let bod = abs_pre ren env (te,v) p in - let bod = CC_lam ([var_name Anonymous, - CC_typed_binder (eq a (mkVar id_phi0) (phi_of ren))], - bod) - in - let bl' = binding_of_alist ren env al in - make_abs (bl@(List.rev bl')) bod - in - let t = - CC_app (CC_expr (constant "well_founded_induction"), - [CC_expr a; CC_expr r; - CC_hole wf_a_r; - CC_expr (Term.mkNamedLambda id_phi a v); - CC_lam ([id_phi0, CC_typed_binder a; - idf, CC_typed_binder tw], - body); - CC_expr (phi_of ren)] - @(List.map (fun (id,_) -> CC_var id) bl) - @(List.map (fun (_,id) -> CC_var id) vars) - @[CC_hole (eq a (phi_of ren) (phi_of ren))] - ) - in - (* on abstrait juste par rapport aux variables de ef *) - let al = current_vars ren (get_reads ef) in - let bl = binding_of_alist ren env al in - make_abs (List.rev bl) t - - -(* [make_access env id c] Access in array id. - * - * Constructs [t:(array s T)](access_g s T t c ?::(lt c s)). - *) - -let array_info ren env id = - let ty = type_in_env env id in - let size,v = dearray_type ty in - let ty_elem = trad_ml_type_v ren env v in - let ty_array = trad_imp_type ren env ty in - size,ty_elem,ty_array - -let make_raw_access ren env (id,id') c = - let size,ty_elem,_ = array_info ren env id in - Term.applist (constant "access", [size; ty_elem; mkVar id'; c]) - -let make_pre_access ren env id c = - let size,_,_ = array_info ren env id in - conj (lt (constant "Zle") (constant "ZERO") c) - (lt (constant "Zlt") c size) - -let make_raw_store ren env (id,id') c1 c2 = - let size,ty_elem,_ = array_info ren env id in - Term.applist (constant "store", [size; ty_elem; mkVar id'; c1; c2]) 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 - diff --git a/contrib/correctness/pred.ml b/contrib/correctness/pred.ml deleted file mode 100644 index 669727fc..00000000 --- a/contrib/correctness/pred.ml +++ /dev/null @@ -1,115 +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: pred.ml 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Pp -open Past -open Pmisc - -let rec cc_subst subst = function - | CC_var id as c -> - (try CC_expr (List.assoc id subst) with Not_found -> c) - | CC_letin (b,ty,bl,c1,c2) -> - CC_letin (b, real_subst_in_constr subst ty, cc_subst_binders subst bl, - cc_subst subst c1, cc_subst (cc_cross_binders subst bl) c2) - | CC_lam (bl, c) -> - CC_lam (cc_subst_binders subst bl, - cc_subst (cc_cross_binders subst bl) c) - | CC_app (c, cl) -> - CC_app (cc_subst subst c, List.map (cc_subst subst) cl) - | CC_tuple (b, tl, cl) -> - CC_tuple (b, List.map (real_subst_in_constr subst) tl, - List.map (cc_subst subst) cl) - | CC_case (ty, c, cl) -> - CC_case (real_subst_in_constr subst ty, cc_subst subst c, - List.map (cc_subst subst) cl) - | CC_expr c -> - CC_expr (real_subst_in_constr subst c) - | CC_hole ty -> - CC_hole (real_subst_in_constr subst ty) - -and cc_subst_binders subst = List.map (cc_subst_binder subst) - -and cc_subst_binder subst = function - | id,CC_typed_binder c -> id,CC_typed_binder (real_subst_in_constr subst c) - | b -> b - -and cc_cross_binders subst = function - | [] -> subst - | (id,_) :: bl -> cc_cross_binders (List.remove_assoc id subst) bl - -(* here we only perform eta-reductions on programs to eliminate - * redexes of the kind - * - * let (x1,...,xn) = e in (x1,...,xn) --> e - * - *) - -let is_eta_redex bl al = - try - List.for_all2 - (fun (id,_) t -> match t with CC_var id' -> id=id' | _ -> false) - bl al - with - Invalid_argument("List.for_all2") -> false - -let rec red = function - | CC_letin (_, _, [id,_], CC_expr c1, e2) -> - red (cc_subst [id,c1] e2) - | CC_letin (dep, ty, bl, e1, e2) -> - begin match red e2 with - | CC_tuple (false,tl,al) -> - if is_eta_redex bl al then - red e1 - else - CC_letin (dep, ty, bl, red e1, - CC_tuple (false,tl,List.map red al)) - | e -> CC_letin (dep, ty, bl, red e1, e) - end - | CC_lam (bl, e) -> - CC_lam (bl, red e) - | CC_app (e, al) -> - CC_app (red e, List.map red al) - | CC_case (ty, e1, el) -> - CC_case (ty, red e1, List.map red el) - | CC_tuple (dep, tl, al) -> - CC_tuple (dep, tl, List.map red al) - | e -> e - - -(* How to reduce uncomplete proof terms when they have become constr *) - -open Term -open Reductionops - -(* Il ne faut pas reduire de redexe (beta/iota) qui impliquerait - * la substitution d'une métavariable. - * - * On commence par rendre toutes les applications binaire (strong bin_app) - * puis on applique la reduction spéciale programmes définie dans - * typing/reduction *) - -(*i -let bin_app = function - | DOPN(AppL,v) as c -> - (match Array.length v with - | 1 -> v.(0) - | 2 -> c - | n -> - let f = DOPN(AppL,Array.sub v 0 (pred n)) in - DOPN(AppL,[|f;v.(pred n)|])) - | c -> c -i*) - -let red_cci c = - (*i let c = strong bin_app c in i*) - strong whd_programs (Global.env ()) Evd.empty c - diff --git a/contrib/correctness/pred.mli b/contrib/correctness/pred.mli deleted file mode 100644 index a5a9549b..00000000 --- a/contrib/correctness/pred.mli +++ /dev/null @@ -1,26 +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: pred.mli 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Term -open Past - -(* reduction on intermediate programs - * get rid of redexes of the kind let (x1,...,xn) = e in (x1,...,xn) *) - -val red : cc_term -> cc_term - - -(* Ad-hoc reduction on partial proof terms *) - -val red_cci : constr -> constr - - diff --git a/contrib/correctness/prename.ml b/contrib/correctness/prename.ml deleted file mode 100644 index 4ef1982d..00000000 --- a/contrib/correctness/prename.ml +++ /dev/null @@ -1,139 +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: prename.ml 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Names -open Nameops -open Util -open Pp -open Himsg -open Pmisc - -(* Variables names management *) - -type date = string - -(* The following data structure keeps the successive names of the variables - * as we traverse the program. A each step a ``date'' and a - * collection of new names is (possibly) given, and updates the - * previous renaming. - * - * Then, we can ask for the name of a variable, at current date or - * at a given date. - * - * It is easily represented by a list of date x assoc list, most recent coming - * first i.e. as follows: - * - * [ date (= current), [ (x,xi); ... ]; - * date , [ (z,zk); ... ]; - * ... - * date (= initial), [ (x,xj); (y,yi); ... ] - * - * We also keep a list of all names already introduced, in order to - * quickly get fresh names. - *) - -type t = - { levels : (date * (identifier * identifier) list) list; - avoid : identifier list; - cpt : int } - - -let empty_ren = { levels = []; avoid = []; cpt = 0 } - -let update r d ids = - let al,av = renaming_of_ids r.avoid ids in - { levels = (d,al) :: r.levels; avoid = av; cpt = r.cpt } - -let push_date r d = update r d [] - -let next r ids = - let al,av = renaming_of_ids r.avoid ids in - let n = succ r.cpt in - let d = string_of_int n in - { levels = (d,al) :: r.levels; avoid = av; cpt = n } - - -let find r x = - let rec find_in_one = function - [] -> raise Not_found - | (y,v)::rem -> if y = x then v else find_in_one rem - in - let rec find_in_all = function - [] -> raise Not_found - | (_,l)::rem -> try find_in_one l with Not_found -> find_in_all rem - in - find_in_all r.levels - - -let current_var = find - -let current_vars r ids = List.map (fun id -> id,current_var r id) ids - - -let avoid r ids = { levels = r.levels; avoid = r.avoid @ ids; cpt = r.cpt } - -let fresh r ids = fst (renaming_of_ids r.avoid ids) - - -let current_date r = - match r.levels with - [] -> invalid_arg "Renamings.current_date" - | (d,_)::_ -> d - -let all_dates r = List.map fst r.levels - -let rec valid_date da r = - let rec valid = function - [] -> false - | (d,_)::rem -> (d=da) or (valid rem) - in - valid r.levels - -(* [until d r] selects the part of the renaming [r] starting from date [d] *) -let rec until da r = - let rec cut = function - [] -> invalid_arg "Renamings.until" - | (d,_)::rem as r -> if d=da then r else cut rem - in - { avoid = r.avoid; levels = cut r.levels; cpt = r.cpt } - -let var_at_date r d id = - try - find (until d r) id - with Not_found -> - raise (UserError ("Renamings.var_at_date", - hov 0 (str"Variable " ++ pr_id id ++ str" is unknown" ++ spc () ++ - str"at date " ++ str d))) - -let vars_at_date r d ids = - let r' = until d r in List.map (fun id -> id,find r' id) ids - - -(* pretty-printers *) - -open Pp -open Util -open Himsg - -let pp r = - hov 2 (prlist_with_sep (fun () -> (fnl ())) - (fun (d,l) -> - (str d ++ str": " ++ - prlist_with_sep (fun () -> (spc ())) - (fun (id,id') -> - (str"(" ++ pr_id id ++ str"," ++ pr_id id' ++ str")")) - l)) - r.levels) - -let ppr e = - Pp.pp (pp e) - diff --git a/contrib/correctness/prename.mli b/contrib/correctness/prename.mli deleted file mode 100644 index 1d3ab669..00000000 --- a/contrib/correctness/prename.mli +++ /dev/null @@ -1,57 +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: prename.mli 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Names - -(* Abstract type for renamings - * - * Records the names of the mutables objets (ref, arrays) at the different - * moments of the evaluation, called dates - *) - -type t - -type date = string - - -val empty_ren : t -val update : t -> date -> identifier list -> t - (* assign new names for the given variables, associated to a new date *) -val next : t -> identifier list -> t - (* assign new names for the given variables, associated to a new - * date which is generated from an internal counter *) -val push_date : t -> date -> t - (* put a new date on top of the stack *) - -val valid_date : date -> t -> bool -val current_date : t -> date -val all_dates : t -> date list - -val current_var : t -> identifier -> identifier -val current_vars : t -> identifier list -> (identifier * identifier) list - (* gives the current names of some variables *) - -val avoid : t -> identifier list -> t -val fresh : t -> identifier list -> (identifier * identifier) list - (* introduces new names to avoid and renames some given variables *) - -val var_at_date : t -> date -> identifier -> identifier - (* gives the name of a variable at a given date *) -val vars_at_date : t -> date -> identifier list - -> (identifier * identifier) list - (* idem for a list of variables *) - -(* pretty-printers *) - -val pp : t -> Pp.std_ppcmds -val ppr : t -> unit - diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4 deleted file mode 100644 index 98d43112..00000000 --- a/contrib/correctness/psyntax.ml4 +++ /dev/null @@ -1,1058 +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: psyntax.ml4 8752 2006-04-27 19:37:33Z herbelin $ *) - -(*i camlp4deps: "parsing/grammar.cma" i*) - -open Options -open Util -open Names -open Nameops -open Vernacentries -open Reduction -open Term -open Libnames -open Topconstr - -open Prename -open Pmisc -open Putil -open Ptype -open Past -open Penv -open Pmonad -open Vernacexpr - - -(* We define new entries for programs, with the use of this module - * Programs. These entries are named Programs.<foo> - *) - -module Gram = Pcoq.Gram -module Constr = Pcoq.Constr -module Tactic = Pcoq.Tactic - -module Programs = - struct - let gec s = Gram.Entry.create ("Programs."^s) - (* types *) - let type_v = gec "type_v" - let type_v0 = gec "type_v0" - let type_v1 = gec "type_v1" - let type_v2 = gec "type_v2" - let type_v3 = gec "type_v3" - let type_v_app = gec "type_v_app" - let type_c = gec "type_c" - let effects = gec "effects" - let reads = gec "reads" - let writes = gec "writes" - let pre_condition = gec "pre_condition" - let post_condition = gec "post_condition" - (* binders *) - let binder = gec "binder" - let binder_type = gec "binder_type" - let binders = gec "binders" - (* programs *) - let program = gec "program" - let prog1 = gec "prog1" - let prog2 = gec "prog2" - let prog3 = gec "prog3" - let prog4 = gec "prog4" - let prog5 = gec "prog5" - let prog6 = gec "prog6" - let prog7 = gec "prog7" - let ast1 = gec "ast1" - let ast2 = gec "ast2" - let ast3 = gec "ast3" - let ast4 = gec "ast4" - let ast5 = gec "ast5" - let ast6 = gec "ast6" - let ast7 = gec "ast7" - let arg = gec "arg" - let block = gec "block" - let block_statement = gec "block_statement" - let relation = gec "relation" - let variable = gec "variable" - let invariant = gec "invariant" - let variant = gec "variant" - let assertion = gec "assertion" - let precondition = gec "precondition" - let postcondition = gec "postcondition" - let predicate = gec "predicate" - let name = gec "name" - end - -open Programs - -let ast_of_int n = - CDelimiters - (dummy_loc, "Z", CNumeral (dummy_loc, Bignat.POS (Bignat.of_string n))) - -let constr_of_int n = - Constrintern.interp_constr Evd.empty (Global.env ()) (ast_of_int n) - -open Util -open Coqast - -let mk_id loc id = mkRefC (Ident (loc, id)) -let mk_ref loc s = mk_id loc (Constrextern.id_of_v7_string s) -let mk_appl loc1 loc2 f args = - CApp (join_loc loc1 loc2, (None,mk_ref loc1 f), List.map (fun a -> a,None) args) - -let conj_assert {a_name=n;a_value=a} {a_value=b} = - let loc1 = constr_loc a in - let loc2 = constr_loc a in - { a_value = mk_appl loc1 loc2 "and" [a;b]; a_name = n } - -let conj = function - None,None -> None - | None,b -> b - | a,None -> a - | Some a,Some b -> Some (conj_assert a b) - -let without_effect loc d = - { desc = d; pre = []; post = None; loc = loc; info = () } - -let isevar = Expression isevar - -let bin_op op loc e1 e2 = - without_effect loc - (Apply (without_effect loc (Expression (constant op)), - [ Term e1; Term e2 ])) - -let un_op op loc e = - without_effect loc - (Apply (without_effect loc (Expression (constant op)), [Term e])) - -let bool_bin op loc a1 a2 = - let w = without_effect loc in - let d = SApp ( [Variable op], [a1; a2]) in - w d - -let bool_or loc = bool_bin connective_or loc -let bool_and loc = bool_bin connective_and loc - -let bool_not loc a = - let w = without_effect loc in - let d = SApp ( [Variable connective_not ], [a]) in - w d - -let ast_zwf_zero loc = mk_appl loc loc "Zwf" [mk_ref loc "Z0"] - -(* program -> Coq AST *) - -let bdize c = - let env = - Global.env_of_context (Pcicenv.cci_sign_of Prename.empty_ren Penv.empty) - in - Constrextern.extern_constr true env c - -let rec coqast_of_program loc = function - | Variable id -> mk_id loc id - | Acc id -> mk_id loc id - | Apply (f,l) -> - let f = coqast_of_program f.loc f.desc in - let args = List.map - (function Term t -> (coqast_of_program t.loc t.desc,None) - | _ -> invalid_arg "coqast_of_program") l - in - CApp (dummy_loc, (None,f), args) - | Expression c -> bdize c - | _ -> invalid_arg "coqast_of_program" - -(* The construction `for' is syntactic sugar. - * - * for i = v1 to v2 do { invariant Inv } block done - * - * ==> (let rec f i { variant v2+1-i } = - * { i <= v2+1 /\ Inv(i) } - * (if i > v2 then tt else begin block; (f (i+1)) end) - * { Inv(v2+1) } - * in (f v1)) { Inv(v2+1) } - *) - -let ast_plus_un loc ast = - let un = ast_of_int "1" in - mk_appl loc loc "Zplus" [ast;un] - -let make_ast_for loc i v1 v2 inv block = - let f = for_name() in - let id_i = id_of_string i in - let var_i = without_effect loc (Variable id_i) in - let var_f = without_effect loc (Variable f) in - let succ_v2 = - let a_v2 = coqast_of_program v2.loc v2.desc in - ast_plus_un loc a_v2 in - let post = named_app (subst_ast_in_ast [ id_i, succ_v2 ]) inv in - let e1 = - let test = bin_op "Z_gt_le_bool" loc var_i v2 in - let br_t = without_effect loc (Expression (constant "tt")) in - let br_f = - let un = without_effect loc (Expression (constr_of_int "1")) in - let succ_i = bin_op "Zplus" loc var_i un in - let f_succ_i = without_effect loc (Apply (var_f, [Term succ_i])) in - without_effect loc (Seq (block @ [Statement f_succ_i])) - in - let inv' = - let i_le_sv2 = mk_appl loc loc "Zle" [mk_ref loc i; succ_v2] in - conj_assert {a_value=i_le_sv2;a_name=inv.a_name} inv - in - { desc = If(test,br_t,br_f); loc = loc; - pre = [pre_of_assert false inv']; post = Some post; info = () } - in - let bl = - let typez = mk_ref loc "Z" in - [(id_of_string i, BindType (TypePure typez))] - in - let fv1 = without_effect loc (Apply (var_f, [Term v1])) in - let v = TypePure (mk_ref loc "unit") in - let var = - let a = mk_appl loc loc "Zminus" [succ_v2;mk_ref loc i] in - (a, ast_zwf_zero loc) - in - Let (f, without_effect loc (LetRec (f,bl,v,var,e1)), fv1) - -let mk_prog loc p pre post = - { desc = p.desc; - pre = p.pre @ pre; - post = conj (p.post,post); - loc = loc; - info = () } - -if !Options.v7 then -GEXTEND Gram - - (* Types ******************************************************************) - type_v: - [ [ t = type_v0 -> t ] ] - ; - type_v0: - [ [ t = type_v1 -> t ] ] - ; - type_v1: - [ [ t = type_v2 -> t ] ] - ; - type_v2: - [ LEFTA - [ v = type_v2; IDENT "ref" -> Ref v - | t = type_v3 -> t ] ] - ; - type_v3: - [ [ IDENT "array"; size = Constr.constr; "of"; v = type_v0 -> - Array (size,v) - | IDENT "fun"; bl = binders; c = type_c -> make_arrow bl c - | c = Constr.constr -> TypePure c - ] ] - ; - type_c: - [ [ IDENT "returns"; id = IDENT; ":"; v = type_v; - e = effects; p = OPT pre_condition; q = OPT post_condition; "end" -> - ((id_of_string id, v), e, list_of_some p, q) - ] ] - ; - effects: - [ [ r = OPT reads; w = OPT writes -> - let r' = match r with Some l -> l | _ -> [] in - let w' = match w with Some l -> l | _ -> [] in - List.fold_left (fun e x -> Peffect.add_write x e) - (List.fold_left (fun e x -> Peffect.add_read x e) Peffect.bottom r') - w' - ] ] - ; - reads: - [ [ IDENT "reads"; l = LIST0 IDENT SEP "," -> List.map id_of_string l ] ] - ; - writes: - [ [ IDENT "writes"; l=LIST0 IDENT SEP "," -> List.map id_of_string l ] ] - ; - pre_condition: - [ [ IDENT "pre"; c = predicate -> pre_of_assert false c ] ] - ; - post_condition: - [ [ IDENT "post"; c = predicate -> c ] ] - ; - - (* Binders (for both types and programs) **********************************) - binder: - [ [ "("; sl = LIST1 IDENT SEP ","; ":"; t = binder_type ; ")" -> - List.map (fun s -> (id_of_string s, t)) sl - ] ] - ; - binder_type: - [ [ "Set" -> BindSet - | v = type_v -> BindType v - ] ] - ; - binders: - [ [ bl = LIST0 binder -> List.flatten bl ] ] - ; - - (* annotations *) - predicate: - [ [ c = Constr.constr; n = name -> { a_name = n; a_value = c } ] ] - ; - name: - [ [ "as"; s = IDENT -> Name (id_of_string s) - | -> Anonymous - ] ] - ; - - (* Programs ***************************************************************) - variable: - [ [ s = IDENT -> id_of_string s ] ] - ; - assertion: - [ [ "{"; c = predicate; "}" -> c ] ] - ; - precondition: - [ [ "{"; c = predicate; "}" -> pre_of_assert false c ] ] - ; - postcondition: - [ [ "{"; c = predicate; "}" -> c ] ] - ; - program: - [ [ p = prog1 -> p ] ] - ; - prog1: - [ [ pre = LIST0 precondition; ast = ast1; post = OPT postcondition -> - mk_prog loc ast pre post ] ] - ; - prog2: - [ [ pre = LIST0 precondition; ast = ast2; post = OPT postcondition -> - mk_prog loc ast pre post ] ] - ; - prog3: - [ [ pre = LIST0 precondition; ast = ast3; post = OPT postcondition -> - mk_prog loc ast pre post ] ] - ; - prog4: - [ [ pre = LIST0 precondition; ast = ast4; post = OPT postcondition -> - mk_prog loc ast pre post ] ] - ; - prog5: - [ [ pre = LIST0 precondition; ast = ast5; post = OPT postcondition -> - mk_prog loc ast pre post ] ] - ; - prog6: - [ [ pre = LIST0 precondition; ast = ast6; post = OPT postcondition -> - mk_prog loc ast pre post ] ] - ; - - ast1: - [ [ x = prog2; IDENT "or"; y = prog1 -> bool_or loc x y - | x = prog2; IDENT "and"; y = prog1 -> bool_and loc x y - | x = prog2 -> x - ] ] - ; - ast2: - [ [ IDENT "not"; x = prog3 -> bool_not loc x - | x = prog3 -> x - ] ] - ; - ast3: - [ [ x = prog4; rel = relation; y = prog4 -> bin_op rel loc x y - | x = prog4 -> x - ] ] - ; - ast4: - [ [ x = prog5; "+"; y = prog4 -> bin_op "Zplus" loc x y - | x = prog5; "-"; y = prog4 -> bin_op "Zminus" loc x y - | x = prog5 -> x - ] ] - ; - ast5: - [ [ x = prog6; "*"; y = prog5 -> bin_op "Zmult" loc x y - | x = prog6 -> x - ] ] - ; - ast6: - [ [ "-"; x = prog6 -> un_op "Zopp" loc x - | x = ast7 -> without_effect loc x - ] ] - ; - ast7: - [ [ v = variable -> - Variable v - | n = INT -> - Expression (constr_of_int n) - | "!"; v = variable -> - Acc v - | "?" -> - isevar - | v = variable; ":="; p = program -> - Aff (v,p) - | v = variable; "["; e = program; "]" -> TabAcc (true,v,e) - | v = variable; "#"; "["; e = program; "]" -> TabAcc (true,v,e) - | v = variable; "["; e = program; "]"; ":="; p = program -> - TabAff (true,v,e,p) - | v = variable; "#"; "["; e = program; "]"; ":="; p = program -> - TabAff (true,v,e,p) - | IDENT "if"; e1 = program; IDENT "then"; e2 = program; - IDENT "else"; e3 = program -> - If (e1,e2,e3) - | IDENT "if"; e1 = program; IDENT "then"; e2 = program -> - If (e1,e2,without_effect loc (Expression (constant "tt"))) - | IDENT "while"; b = program; IDENT "do"; - "{"; inv = OPT invariant; IDENT "variant"; wf = variant; "}"; - bl = block; IDENT "done" -> - While (b, inv, wf, bl) - | IDENT "for"; i = IDENT; "="; v1 = program; IDENT "to"; v2 = program; - IDENT "do"; "{"; inv = invariant; "}"; - bl = block; IDENT "done" -> - make_ast_for loc i v1 v2 inv bl - | IDENT "let"; v = variable; "="; IDENT "ref"; p1 = program; - "in"; p2 = program -> - LetRef (v, p1, p2) - | IDENT "let"; v = variable; "="; p1 = program; "in"; p2 = program -> - Let (v, p1, p2) - | IDENT "begin"; b = block; "end" -> - Seq b - | IDENT "fun"; bl = binders; "->"; p = program -> - Lam (bl,p) - | IDENT "let"; IDENT "rec"; f = variable; - bl = binders; ":"; v = type_v; - "{"; IDENT "variant"; var = variant; "}"; "="; p = program -> - LetRec (f,bl,v,var,p) - | IDENT "let"; IDENT "rec"; f = variable; - bl = binders; ":"; v = type_v; - "{"; IDENT "variant"; var = variant; "}"; "="; p = program; - "in"; p2 = program -> - Let (f, without_effect loc (LetRec (f,bl,v,var,p)), p2) - - | "@"; s = STRING; p = program -> - Debug (s,p) - - | "("; p = program; args = LIST0 arg; ")" -> - match args with - [] -> - if p.pre<>[] or p.post<>None then - Pp.warning "Some annotations are lost"; - p.desc - | _ -> - Apply(p,args) - ] ] - ; - arg: - [ [ "'"; t = type_v -> Type t - | p = program -> Term p - ] ] - ; - block: - [ [ s = block_statement; ";"; b = block -> s::b - | s = block_statement -> [s] ] ] - ; - block_statement: - [ [ IDENT "label"; s = IDENT -> Label s - | IDENT "assert"; c = assertion -> Assert c - | p = program -> Statement p ] ] - ; - relation: - [ [ "<" -> "Z_lt_ge_bool" - | "<=" -> "Z_le_gt_bool" - | ">" -> "Z_gt_le_bool" - | ">=" -> "Z_ge_lt_bool" - | "=" -> "Z_eq_bool" - | "<>" -> "Z_noteq_bool" ] ] - ; - - (* Other entries (invariants, etc.) ***************************************) - invariant: - [ [ IDENT "invariant"; c = predicate -> c ] ] - ; - variant: - [ [ c = Constr.constr; IDENT "for"; r = Constr.constr -> (c, r) - | c = Constr.constr -> (c, ast_zwf_zero loc) ] ] - ; - END -else -GEXTEND Gram - GLOBAL: type_v program; - - (* Types ******************************************************************) - type_v: - [ [ t = type_v0 -> t ] ] - ; - type_v0: - [ [ t = type_v1 -> t ] ] - ; - type_v1: - [ [ t = type_v2 -> t ] ] - ; - type_v2: - [ LEFTA - [ v = type_v2; IDENT "ref" -> Ref v - | t = type_v3 -> t ] ] - ; - type_v3: - [ [ IDENT "array"; size = Constr.constr; IDENT "of"; v = type_v0 -> - Array (size,v) - | "fun"; bl = binders; c = type_c -> make_arrow bl c - | c = Constr.constr -> TypePure c - ] ] - ; - type_c: - [ [ IDENT "returns"; id = IDENT; ":"; v = type_v; - e = effects; p = OPT pre_condition; q = OPT post_condition; "end" -> - ((id_of_string id, v), e, list_of_some p, q) - ] ] - ; - effects: - [ [ r = OPT reads; w = OPT writes -> - let r' = match r with Some l -> l | _ -> [] in - let w' = match w with Some l -> l | _ -> [] in - List.fold_left (fun e x -> Peffect.add_write x e) - (List.fold_left (fun e x -> Peffect.add_read x e) Peffect.bottom r') - w' - ] ] - ; - reads: - [ [ IDENT "reads"; l = LIST0 IDENT SEP "," -> List.map id_of_string l ] ] - ; - writes: - [ [ IDENT "writes"; l=LIST0 IDENT SEP "," -> List.map id_of_string l ] ] - ; - pre_condition: - [ [ IDENT "pre"; c = predicate -> pre_of_assert false c ] ] - ; - post_condition: - [ [ IDENT "post"; c = predicate -> c ] ] - ; - - (* Binders (for both types and programs) **********************************) - binder: - [ [ "("; sl = LIST1 IDENT SEP ","; ":"; t = binder_type ; ")" -> - List.map (fun s -> (id_of_string s, t)) sl - ] ] - ; - binder_type: - [ [ "Set" -> BindSet - | v = type_v -> BindType v - ] ] - ; - binders: - [ [ bl = LIST0 binder -> List.flatten bl ] ] - ; - - (* annotations *) - predicate: - [ [ c = Constr.constr; n = name -> { a_name = n; a_value = c } ] ] - ; - dpredicate: - [ [ c = Constr.lconstr; n = name -> { a_name = n; a_value = c } ] ] - ; - name: - [ [ "as"; s = IDENT -> Name (id_of_string s) - | -> Anonymous - ] ] - ; - - (* Programs ***************************************************************) - variable: - [ [ s = IDENT -> id_of_string s ] ] - ; - assertion: - [ [ "{"; c = dpredicate; "}" -> c ] ] - ; - precondition: - [ [ "{"; c = dpredicate; "}" -> pre_of_assert false c ] ] - ; - postcondition: - [ [ "{"; c = dpredicate; "}" -> c ] ] - ; - program: - [ [ p = prog1 -> p ] ] - ; - prog1: - [ [ pre = LIST0 precondition; ast = ast1; post = OPT postcondition -> - mk_prog loc ast pre post ] ] - ; - prog2: - [ [ pre = LIST0 precondition; ast = ast2; post = OPT postcondition -> - mk_prog loc ast pre post ] ] - ; - prog3: - [ [ pre = LIST0 precondition; ast = ast3; post = OPT postcondition -> - mk_prog loc ast pre post ] ] - ; - prog4: - [ [ pre = LIST0 precondition; ast = ast4; post = OPT postcondition -> - mk_prog loc ast pre post ] ] - ; - prog5: - [ [ pre = LIST0 precondition; ast = ast5; post = OPT postcondition -> - mk_prog loc ast pre post ] ] - ; - prog6: - [ [ pre = LIST0 precondition; ast = ast6; post = OPT postcondition -> - mk_prog loc ast pre post ] ] - ; - - ast1: - [ [ x = prog2; IDENT "or"; y = prog1 -> bool_or loc x y - | x = prog2; IDENT "and"; y = prog1 -> bool_and loc x y - | x = prog2 -> x - ] ] - ; - ast2: - [ [ IDENT "not"; x = prog3 -> bool_not loc x - | x = prog3 -> x - ] ] - ; - ast3: - [ [ x = prog4; rel = relation; y = prog4 -> bin_op rel loc x y - | x = prog4 -> x - ] ] - ; - ast4: - [ [ x = prog5; "+"; y = prog4 -> bin_op "Zplus" loc x y - | x = prog5; "-"; y = prog4 -> bin_op "Zminus" loc x y - | x = prog5 -> x - ] ] - ; - ast5: - [ [ x = prog6; "*"; y = prog5 -> bin_op "Zmult" loc x y - | x = prog6 -> x - ] ] - ; - ast6: - [ [ "-"; x = prog6 -> un_op "Zopp" loc x - | x = ast7 -> without_effect loc x - ] ] - ; - ast7: - [ [ v = variable -> - Variable v - | n = INT -> - Expression (constr_of_int n) - | "!"; v = variable -> - Acc v - | "?" -> - isevar - | v = variable; ":="; p = program -> - Aff (v,p) - | v = variable; "["; e = program; "]" -> TabAcc (true,v,e) - | v = variable; "#"; "["; e = program; "]" -> TabAcc (true,v,e) - | v = variable; "["; e = program; "]"; ":="; p = program -> - TabAff (true,v,e,p) - | v = variable; "#"; "["; e = program; "]"; ":="; p = program -> - TabAff (true,v,e,p) - | "if"; e1 = program; "then"; e2 = program; "else"; e3 = program -> - If (e1,e2,e3) - | "if"; e1 = program; "then"; e2 = program -> - If (e1,e2,without_effect loc (Expression (constant "tt"))) - | IDENT "while"; b = program; IDENT "do"; - "{"; inv = OPT invariant; IDENT "variant"; wf = variant; "}"; - bl = block; IDENT "done" -> - While (b, inv, wf, bl) - | "for"; i = IDENT; "="; v1 = program; IDENT "to"; v2 = program; - IDENT "do"; "{"; inv = invariant; "}"; - bl = block; IDENT "done" -> - make_ast_for loc i v1 v2 inv bl - | "let"; v = variable; "="; IDENT "ref"; p1 = program; - "in"; p2 = program -> - LetRef (v, p1, p2) - | "let"; v = variable; "="; p1 = program; "in"; p2 = program -> - Let (v, p1, p2) - | IDENT "begin"; b = block; "end" -> - Seq b - | "fun"; bl = binders; "=>"; p = program -> - Lam (bl,p) - | "let"; IDENT "rec"; f = variable; - bl = binders; ":"; v = type_v; - "{"; IDENT "variant"; var = variant; "}"; "="; p = program -> - LetRec (f,bl,v,var,p) - | "let"; IDENT "rec"; f = variable; - bl = binders; ":"; v = type_v; - "{"; IDENT "variant"; var = variant; "}"; "="; p = program; - "in"; p2 = program -> - Let (f, without_effect loc (LetRec (f,bl,v,var,p)), p2) - - | "@"; s = STRING; p = program -> - Debug (s,p) - - | "("; p = program; args = LIST0 arg; ")" -> - match args with - [] -> - if p.pre<>[] or p.post<>None then - Pp.warning "Some annotations are lost"; - p.desc - | _ -> - Apply(p,args) - ] ] - ; - arg: - [ [ "'"; t = type_v -> Type t - | p = program -> Term p - ] ] - ; - block: - [ [ s = block_statement; ";"; b = block -> s::b - | s = block_statement -> [s] ] ] - ; - block_statement: - [ [ IDENT "label"; s = IDENT -> Label s - | IDENT "assert"; c = assertion -> Assert c - | p = program -> Statement p ] ] - ; - relation: - [ [ "<" -> "Z_lt_ge_bool" - | "<=" -> "Z_le_gt_bool" - | ">" -> "Z_gt_le_bool" - | ">=" -> "Z_ge_lt_bool" - | "=" -> "Z_eq_bool" - | "<>" -> "Z_noteq_bool" ] ] - ; - - (* Other entries (invariants, etc.) ***************************************) - invariant: - [ [ IDENT "invariant"; c = predicate -> c ] ] - ; - variant: - [ [ c = Constr.constr; "for"; r = Constr.constr -> (c, r) - | c = Constr.constr -> (c, ast_zwf_zero loc) ] ] - ; - END -;; - -let wit_program, globwit_program, rawwit_program = - Genarg.create_arg "program" -let wit_type_v, globwit_type_v, rawwit_type_v = - Genarg.create_arg "type_v" - -open Pp -open Util -open Himsg -open Vernacinterp -open Vernacexpr -open Declare - -let is_assumed global ids = - if List.length ids = 1 then - msgnl (str (if global then "A global variable " else "") ++ - pr_id (List.hd ids) ++ str " is assumed") - else - msgnl (str (if global then "Some global variables " else "") ++ - prlist_with_sep (fun () -> (str ", ")) pr_id ids ++ - str " are assumed") - -open Pcoq - -(* Variables *) - -let wit_variables, globwit_variables, rawwit_variables = - Genarg.create_arg "variables" - -let variables = Gram.Entry.create "Variables" - -GEXTEND Gram - variables: [ [ l = LIST1 Prim.ident SEP "," -> l ] ]; -END - -let pr_variables _prc _prtac l = spc() ++ prlist_with_sep pr_coma pr_id l - -let _ = - Pptactic.declare_extra_genarg_pprule true - (rawwit_variables, pr_variables) - (globwit_variables, pr_variables) - (wit_variables, pr_variables) - -(* then_tac *) - -open Genarg -open Tacinterp - -let pr_then_tac _ prt = function - | None -> mt () - | Some t -> pr_semicolon () ++ prt t - -ARGUMENT EXTEND then_tac - TYPED AS tactic_opt - PRINTED BY pr_then_tac - INTERPRETED BY interp_genarg - GLOBALIZED BY intern_genarg -| [ ";" tactic(t) ] -> [ Some t ] -| [ ] -> [ None ] -END - -(* Correctness *) - -VERNAC COMMAND EXTEND Correctness - [ "Correctness" preident(str) program(pgm) then_tac(tac) ] - -> [ Ptactic.correctness str pgm (option_map Tacinterp.interp tac) ] -END - -(* Show Programs *) - -let show_programs () = - fold_all - (fun (id,v) _ -> - msgnl (pr_id id ++ str " : " ++ - hov 2 (match v with TypeV v -> pp_type_v v - | Set -> (str "Set")) ++ - fnl ())) - Penv.empty () - -VERNAC COMMAND EXTEND ShowPrograms - [ "Show" "Programs" ] -> [ show_programs () ] -END - -(* Global Variable *) - -let global_variable ids v = - List.iter - (fun id -> if Penv.is_global id then - Util.errorlabstrm "PROGVARIABLE" - (str"Clash with previous constant " ++ pr_id id)) - ids; - Pdb.check_type_v (all_refs ()) v; - let env = empty in - let ren = update empty_ren "" [] in - let v = Ptyping.cic_type_v env ren v in - if not (is_mutable v) then begin - let c = - Entries.ParameterEntry (trad_ml_type_v ren env v), - Decl_kinds.IsAssumption Decl_kinds.Definitional in - List.iter - (fun id -> ignore (Declare.declare_constant id c)) ids; - if_verbose (is_assumed false) ids - end; - if not (is_pure v) then begin - List.iter (fun id -> ignore (Penv.add_global id v None)) ids; - if_verbose (is_assumed true) ids - end - -VERNAC COMMAND EXTEND ProgVariable - [ "Global" "Variable" variables(ids) ":" type_v(t) ] - -> [ global_variable ids t] -END - -let pr_id id = pr_id (Constrextern.v7_to_v8_id id) - -(* Type printer *) - -let pr_reads = function - | [] -> mt () - | l -> spc () ++ - hov 0 (str "reads" ++ spc () ++ prlist_with_sep pr_coma pr_id l) - -let pr_writes = function - | [] -> mt () - | l -> spc () ++ - hov 0 (str "writes" ++ spc () ++ prlist_with_sep pr_coma pr_id l) - -let pr_effects x = - let (ro,rw) = Peffect.get_repr x in pr_reads ro ++ pr_writes rw - -let pr_predicate delimited { a_name = n; a_value = c } = - (if delimited then Ppconstr.pr_lconstr else Ppconstr.pr_constr) c ++ - (match n with Name id -> spc () ++ str "as " ++ pr_id id | Anonymous -> mt()) - -let pr_assert b { p_name = x; p_value = v } = - pr_predicate b { a_name = x; a_value = v } - -let pr_pre_condition_list = function - | [] -> mt () - | [pre] -> spc() ++ hov 0 (str "pre" ++ spc () ++ pr_assert false pre) - | _ -> assert false - -let pr_post_condition_opt = function - | None -> mt () - | Some post -> - spc() ++ hov 0 (str "post" ++ spc () ++ pr_predicate false post) - -let rec pr_type_v_v8 = function - | Array (a,v) -> - str "array" ++ spc() ++ Ppconstr.pr_constr a ++ spc() ++ str "of " ++ - pr_type_v_v8 v - | v -> pr_type_v3 v - -and pr_type_v3 = function - | Ref v -> pr_type_v3 v ++ spc () ++ str "ref" - | Arrow (bl,((id,v),e,prel,postl)) -> - str "fun" ++ spc() ++ hov 0 (prlist_with_sep cut pr_binder bl) ++ - spc () ++ str "returns" ++ spc () ++ pr_id id ++ str ":" ++ - pr_type_v_v8 v ++ pr_effects e ++ - pr_pre_condition_list prel ++ pr_post_condition_opt postl ++ - spc () ++ str "end" - | TypePure a -> Ppconstr.pr_constr a - | v -> str "(" ++ pr_type_v_v8 v ++ str ")" - -and pr_binder = function - | (id,BindType c) -> - str "(" ++ pr_id id ++ str ":" ++ pr_type_v_v8 c ++ str ")" - | (id,BindSet) -> - str "(" ++ pr_id id ++ str ":" ++ str "Set" ++ str ")" - | (id,Untyped) -> - str "<<<<< TODO: Untyped binder >>>>" - -let _ = - Pptactic.declare_extra_genarg_pprule true - (rawwit_type_v, fun _ _ -> pr_type_v_v8) - (globwit_type_v, fun _ -> raise Not_found) - (wit_type_v, fun _ -> raise Not_found) - -(* Program printer *) - -let pr_precondition pred = str "{" ++ pr_assert true pred ++ str "}" ++ spc () - -let pr_postcondition pred = str "{" ++ pr_predicate true pred ++ str "}" - -let pr_invariant = function - | None -> mt () - | Some c -> hov 2 (str "invariant" ++ spc () ++ pr_predicate false c) - -let pr_variant (c1,c2) = - Ppconstr.pr_constr c1 ++ - (try Constrextern.check_same_type c2 (ast_zwf_zero dummy_loc); mt () - with _ -> spc() ++ hov 0 (str "for" ++ spc () ++ Ppconstr.pr_constr c2)) - -let rec pr_desc = function - | Variable id -> - (* Unsafe: should distinguish global names and bound vars *) - let vars = (* TODO *) Idset.empty in - let id = try - snd (repr_qualid - (snd (qualid_of_reference - (Constrextern.extern_reference - dummy_loc vars (Nametab.locate (make_short_qualid id)))))) - with _ -> id in - pr_id id - | Acc id -> str "!" ++ pr_id id - | Aff (id,p) -> pr_id id ++ spc() ++ str ":=" ++ spc() ++ pr_prog p - | TabAcc (b,id,p) -> pr_id id ++ str "[" ++ pr_prog p ++ str "]" - | TabAff (b,id,p1,p2) -> - pr_id id ++ str "[" ++ pr_prog p1 ++ str "]" ++ - str ":=" ++ pr_prog p2 - | Seq bll -> - hv 0 (str "begin" ++ spc () ++ pr_block bll ++ spc () ++ str "end") - | While (p1,inv,var,bll) -> - hv 0 ( - hov 0 (str "while" ++ spc () ++ pr_prog p1 ++ spc () ++ str "do") ++ - brk (1,2) ++ - hv 2 ( - str "{ " ++ - pr_invariant inv ++ spc() ++ - hov 0 (str "variant" ++ spc () ++ pr_variant var) - ++ str " }") ++ cut () ++ - hov 0 (pr_block bll) ++ cut () ++ - str "done") - | If (p1,p2,p3) -> - hov 1 (str "if " ++ pr_prog p1) ++ spc () ++ - hov 0 (str "then" ++ spc () ++ pr_prog p2) ++ spc () ++ - hov 0 (str "else" ++ spc () ++ pr_prog p3) - | Lam (bl,p) -> - hov 0 - (str "fun" ++ spc () ++ hov 0 (prlist_with_sep cut pr_binder bl) ++ - spc () ++ str "=>") ++ - pr_prog p - | Apply ({desc=Expression e; pre=[]; post=None} as p,args) when isConst e -> - begin match - string_of_id (snd (repr_path (Nametab.sp_of_global (ConstRef (destConst e))))), - args - with - | "Zmult", [a1;a2] -> - str "(" ++ pr_arg a1 ++ str"*" ++ pr_arg a2 ++ str ")" - | "Zplus", [a1;a2] -> - str "(" ++ pr_arg a1 ++ str"+" ++ pr_arg a2 ++ str ")" - | "Zminus", [a1;a2] -> - str "(" ++ pr_arg a1 ++ str"-" ++ pr_arg a2 ++ str ")" - | "Zopp", [a] -> - str "( -" ++ pr_arg a ++ str ")" - | "Z_lt_ge_bool", [a1;a2] -> - str "(" ++ pr_arg a1 ++ str"<" ++ pr_arg a2 ++ str ")" - | "Z_le_gt_bool", [a1;a2] -> - str "(" ++ pr_arg a1 ++ str"<=" ++ pr_arg a2 ++ str ")" - | "Z_gt_le_bool", [a1;a2] -> - str "(" ++ pr_arg a1 ++ str">" ++ pr_arg a2 ++ str ")" - | "Z_ge_lt_bool", [a1;a2] -> - str "(" ++ pr_arg a1 ++ str">=" ++ pr_arg a2 ++ str ")" - | "Z_eq_bool", [a1;a2] -> - str "(" ++ pr_arg a1 ++ str"=" ++ pr_arg a2 ++ str ")" - | "Z_noteq_bool", [a1;a2] -> - str "(" ++ pr_arg a1 ++ str"<> " ++ pr_arg a2 ++ str ")" - | _ -> - str "(" ++ pr_prog p ++ spc () ++ prlist_with_sep spc pr_arg args ++ - str ")" - end - | Apply (p,args) -> - str "(" ++ pr_prog p ++ spc () ++ prlist_with_sep spc pr_arg args ++ - str ")" - | SApp ([Variable v], args) -> - begin match string_of_id v, args with - | "prog_bool_and", [a1;a2] -> - str"(" ++ pr_prog a1 ++ spc() ++ str"and " ++ pr_prog a2 ++str")" - | "prog_bool_or", [a1;a2] -> - str"(" ++ pr_prog a1 ++ spc() ++ str"or " ++ pr_prog a2 ++ str")" - | "prog_bool_not", [a] -> - str "(not " ++ pr_prog a ++ str ")" - | _ -> failwith "Correctness printer: TODO" - end - | SApp _ -> failwith "Correctness printer: TODO" - | LetRef (v,p1,p2) -> - hov 2 ( - str "let " ++ pr_id v ++ str " =" ++ spc () ++ str "ref" ++ spc () ++ - pr_prog p1 ++ str " in") ++ - spc () ++ pr_prog p2 - | Let (id, {desc=LetRec (f,bl,v,var,p); pre=[]; post=None },p2) when f=id -> - hov 2 ( - str "let rec " ++ pr_id f ++ spc () ++ - hov 0 (prlist_with_sep cut pr_binder bl) ++ spc () ++ - str ":" ++ pr_type_v_v8 v ++ spc () ++ - hov 2 (str "{ variant" ++ spc () ++ pr_variant var ++ str " }") ++ - spc() ++ str "=" ++ spc () ++ pr_prog p ++ - str " in") ++ - spc () ++ pr_prog p2 - | Let (v,p1,p2) -> - hov 2 ( - str "let " ++ pr_id v ++ str " =" ++ spc () ++ pr_prog p1 ++ str" in") - ++ spc () ++ pr_prog p2 - | LetRec (f,bl,v,var,p) -> - str "let rec " ++ pr_id f ++ spc () ++ - hov 0 (prlist_with_sep cut pr_binder bl) ++ spc () ++ - str ":" ++ pr_type_v_v8 v ++ spc () ++ - hov 2 (str "{ variant" ++ spc () ++ pr_variant var ++ str " }") ++ - spc () ++ str "=" ++ spc () ++ pr_prog p - | PPoint _ -> str "TODO: Ppoint" (* Internal use only *) - | Expression c -> - (* Numeral or "tt": use a printer which doesn't globalize *) - Ppconstr.pr_constr - (Constrextern.extern_constr_in_scope false "Z_scope" (Global.env()) c) - | Debug (s,p) -> str "@" ++ Pptactic.qsnew s ++ pr_prog p - -and pr_block_st = function - | Label s -> hov 0 (str "label" ++ spc() ++ str s) - | Assert pred -> - hov 0 (str "assert" ++ spc() ++ hov 0 (pr_postcondition pred)) - | Statement p -> pr_prog p - -and pr_block bl = prlist_with_sep pr_semicolon pr_block_st bl - -and pr_arg = function - | Past.Term p -> pr_prog p - | Past.Type t -> str "'" ++ pr_type_v_v8 t - | Refarg _ -> str "TODO: Refarg" (* Internal use only *) - -and pr_prog0 b { desc = desc; pre = pre; post = post } = - hv 0 ( - prlist pr_precondition pre ++ - hov 0 - (if b & post<>None then str"(" ++ pr_desc desc ++ str")" - else pr_desc desc) - ++ Ppconstr.pr_opt pr_postcondition post) - -and pr_prog x = pr_prog0 true x - -let _ = - Pptactic.declare_extra_genarg_pprule true - (rawwit_program, fun _ _ a -> spc () ++ pr_prog0 false a) - (globwit_program, fun _ -> raise Not_found) - (wit_program, fun _ -> raise Not_found) - diff --git a/contrib/correctness/psyntax.mli b/contrib/correctness/psyntax.mli deleted file mode 100644 index c0f0990b..00000000 --- a/contrib/correctness/psyntax.mli +++ /dev/null @@ -1,25 +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: psyntax.mli 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Pcoq -open Ptype -open Past -open Topconstr - -(* Grammar for the programs and the tactic Correctness *) - -module Programs : - sig - val program : program Gram.Entry.e - val type_v : constr_expr ml_type_v Gram.Entry.e - val type_c : constr_expr ml_type_c Gram.Entry.e - end diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml deleted file mode 100644 index babc607d..00000000 --- a/contrib/correctness/ptactic.ml +++ /dev/null @@ -1,258 +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: ptactic.ml 8759 2006-04-28 12:24:14Z herbelin $ *) - -open Pp -open Options -open Names -open Libnames -open Term -open Pretyping -open Pfedit -open Decl_kinds -open Vernacentries - -open Pmisc -open Putil -open Past -open Penv -open Prename -open Peffect -open Pmonad - -(* [coqast_of_prog: program -> constr * constr] - * Traduction d'un programme impératif en un but (second constr) - * et un terme de preuve partiel pour ce but (premier constr) - *) - -let coqast_of_prog p = - (* 1. db : séparation dB/var/const *) - let p = Pdb.db_prog p in - - (* 2. typage avec effets *) - deb_mess (str"Ptyping.states: Typing with effects..." ++ fnl ()); - let env = Penv.empty in - let ren = initial_renaming env in - let p = Ptyping.states ren env p in - let ((_,v),_,_,_) as c = p.info.kappa in - Perror.check_for_not_mutable p.loc v; - deb_print pp_type_c c; - - (* 3. propagation annotations *) - let p = Pwp.propagate ren p in - - (* 4a. traduction type *) - let ty = Pmonad.trad_ml_type_c ren env c in - deb_print (Printer.pr_lconstr_env (Global.env())) ty; - - (* 4b. traduction terme (terme intermédiaire de type cc_term) *) - deb_mess - (fnl () ++ str"Mlize.trad: Translation program -> cc_term..." ++ fnl ()); - let cc = Pmlize.trans ren p in - let cc = Pred.red cc in - deb_print Putil.pp_cc_term cc; - - (* 5. traduction en constr *) - deb_mess - (fnl () ++ str"Pcic.constr_of_prog: Translation cc_term -> rawconstr..." ++ - fnl ()); - let r = Pcic.rawconstr_of_prog cc in - deb_print Printer.pr_lrawconstr r; - - (* 6. résolution implicites *) - deb_mess (fnl () ++ str"Resolution implicits (? => Meta(n))..." ++ fnl ()); - let oc = understand_gen_tcc Evd.empty (Global.env()) [] None r in - deb_print (Printer.pr_lconstr_env (Global.env())) (snd oc); - - p,oc,ty,v - -(* [automatic : tactic] - * - * Certains buts engendrés par "correctness" (ci-dessous) - * sont réellement triviaux. On peut les résoudre aisément, sans pour autant - * tomber dans la solution trop lourde qui consiste à faire "; Auto." - * - * Cette tactique fait les choses suivantes : - * o elle élimine les hypothèses de nom loop<i> - * o sur G |- (well_founded nat lt) ==> Exact lt_wf. - * o sur G |- (well_founded Z (Zwf c)) ==> Exact (Zwf_well_founded c) - * o sur G |- e = e' ==> Reflexivity. (arg. de decr. des boucles) - * sinon Try Assumption. - * o sur G |- P /\ Q ==> Try (Split; Assumption). (sortie de boucle) - * o sinon, Try AssumptionBis (= Assumption + décomposition /\ dans hyp.) - * (pour entrée dans corps de boucle par ex.) - *) - -open Pattern -open Tacmach -open Tactics -open Tacticals -open Equality -open Nametab - -let nat = IndRef (coq_constant ["Init";"Datatypes"] "nat", 0) -let lt = ConstRef (coq_constant ["Init";"Peano"] "lt") -let well_founded = ConstRef (coq_constant ["Init";"Wf"] "well_founded") -let z = IndRef (coq_constant ["ZArith";"BinInt"] "Z", 0) -let and_ = IndRef (coq_constant ["Init";"Logic"] "and", 0) -let eq = IndRef (coq_constant ["Init";"Logic"] "eq", 0) - -let mkmeta n = Nameops.make_ident "X" (Some n) -let mkPMeta n = PMeta (Some (mkmeta n)) - -(* ["(well_founded nat lt)"] *) -let wf_nat_pattern = - PApp (PRef well_founded, [| PRef nat; PRef lt |]) -(* ["((well_founded Z (Zwf ?1))"] *) -let wf_z_pattern = - let zwf = ConstRef (coq_constant ["ZArith";"Zwf"] "Zwf") in - PApp (PRef well_founded, [| PRef z; PApp (PRef zwf, [| mkPMeta 1 |]) |]) -(* ["(and ?1 ?2)"] *) -let and_pattern = - PApp (PRef and_, [| mkPMeta 1; mkPMeta 2 |]) -(* ["(eq ?1 ?2 ?3)"] *) -let eq_pattern = - PApp (PRef eq, [| mkPMeta 1; mkPMeta 2; mkPMeta 3 |]) - -(* loop_ids: remove loop<i> hypotheses from the context, and rewrite - * using Variant<i> hypotheses when needed. *) - -let (loop_ids : tactic) = fun gl -> - let rec arec hyps gl = - let env = pf_env gl in - let concl = pf_concl gl in - match hyps with - | [] -> tclIDTAC gl - | (id,a) :: al -> - let s = string_of_id id in - let n = String.length s in - if n >= 4 & (let su = String.sub s 0 4 in su="loop" or su="Bool") - then - tclTHEN (clear [id]) (arec al) gl - else if n >= 7 & String.sub s 0 7 = "Variant" then begin - match pf_matches gl eq_pattern (body_of_type a) with - | [_; _,varphi; _] when isVar varphi -> - let phi = destVar varphi in - if Termops.occur_var env phi concl then - tclTHEN (rewriteLR (mkVar id)) (arec al) gl - else - arec al gl - | _ -> assert false end - else - arec al gl - in - arec (pf_hyps_types gl) gl - -(* assumption_bis: like assumption, but also solves ... h:A/\B ... |- A - * (resp. B) *) - -let (assumption_bis : tactic) = fun gl -> - let concl = pf_concl gl in - let rec arec = function - | [] -> Util.error "No such assumption" - | (s,a) :: al -> - let a = body_of_type a in - if pf_conv_x_leq gl a concl then - refine (mkVar s) gl - else if pf_is_matching gl and_pattern a then - match pf_matches gl and_pattern a with - | [_,c1; _,c2] -> - if pf_conv_x_leq gl c1 concl then - exact_check (applistc (constant "proj1") [c1;c2;mkVar s]) gl - else if pf_conv_x_leq gl c2 concl then - exact_check (applistc (constant "proj2") [c1;c2;mkVar s]) gl - else - arec al - | _ -> assert false - else - arec al - in - arec (pf_hyps_types gl) - -(* automatic: see above *) - -let (automatic : tactic) = - tclTHEN - loop_ids - (fun gl -> - let c = pf_concl gl in - if pf_is_matching gl wf_nat_pattern c then - exact_check (constant "lt_wf") gl - else if pf_is_matching gl wf_z_pattern c then - let (_,z) = List.hd (pf_matches gl wf_z_pattern c) in - exact_check (Term.applist (constant "Zwf_well_founded",[z])) gl - else if pf_is_matching gl and_pattern c then - (tclORELSE assumption_bis - (tclTRY (tclTHEN simplest_split assumption))) gl - else if pf_is_matching gl eq_pattern c then - (tclORELSE reflexivity (tclTRY assumption_bis)) gl - else - tclTRY assumption_bis gl) - -(* [correctness s p] : string -> program -> tactic option -> unit - * - * Vernac: Correctness <string> <program> [; <tactic>]. - *) - -let reduce_open_constr (em0,c) = - let existential_map_of_constr = - let rec collect em c = match kind_of_term c with - | Cast (c',t) -> - (match kind_of_term c' with - | Evar (ev,_) -> - if not (Evd.mem em ev) then - Evd.add em ev (Evd.find em0 ev) - else - em - | _ -> fold_constr collect em c) - | Evar _ -> - assert false (* all existentials should be casted *) - | _ -> - fold_constr collect em c - in - collect Evd.empty - in - let c = Pred.red_cci c in - let em = existential_map_of_constr c in - (em,c) - -let register id n = - let id' = match n with None -> id | Some id' -> id' in - Penv.register id id' - - (* On dit à la commande "Save" d'enregistrer les nouveaux programmes *) -let correctness_hook _ ref = - let pf_id = Nametab.id_of_global ref in - register pf_id None - -let correctness s p opttac = - Coqlib.check_required_library ["Coq";"correctness";"Correctness"]; - Pmisc.reset_names(); - let p,oc,cty,v = coqast_of_prog p in - let env = Global.env () in - let sign = Global.named_context () in - let sigma = Evd.empty in - let cty = Reduction.nf_betaiota cty in - let id = id_of_string s in - start_proof id (IsGlobal (Proof Lemma)) sign cty correctness_hook; - Penv.new_edited id (v,p); - if !debug then msg (Pfedit.pr_open_subgoals()); - deb_mess (str"Pred.red_cci: Reduction..." ++ fnl ()); - let oc = reduce_open_constr oc in - deb_mess (str"AFTER REDUCTION:" ++ fnl ()); - deb_print (Printer.pr_lconstr_env (Global.env())) (snd oc); - let tac = (tclTHEN (Extratactics.refine_tac oc) automatic) in - let tac = match opttac with - | None -> tac - | Some t -> tclTHEN tac t - in - solve_nth 1 tac; - if_verbose msg (pr_open_subgoals ()) diff --git a/contrib/correctness/ptactic.mli b/contrib/correctness/ptactic.mli deleted file mode 100644 index 87378cff..00000000 --- a/contrib/correctness/ptactic.mli +++ /dev/null @@ -1,22 +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: ptactic.mli 5920 2004-07-16 20:01:26Z herbelin $ *) - -(* The main tactic: takes a name N, a program P, creates a goal - * of name N with the functional specification of P, then apply the Refine - * tactic with the partial proof term obtained by the translation of - * P into a functional program. - * - * Then an ad-hoc automatic tactic is applied on each subgoal to solve the - * trivial proof obligations *) - -val correctness : string -> Past.program -> Tacmach.tactic option -> unit - diff --git a/contrib/correctness/ptype.mli b/contrib/correctness/ptype.mli deleted file mode 100644 index be181bcc..00000000 --- a/contrib/correctness/ptype.mli +++ /dev/null @@ -1,73 +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: ptype.mli 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Term - -(* Types des valeurs (V) et des calculs (C). - * - * On a C = r:V,E,P,Q - * - * et V = (x1:V1)...(xn:Vn)C | V ref | V array | <type pur> - * - * INVARIANT: l'effet E contient toutes les variables apparaissant dans - * le programme ET les annotations P et Q - * Si E = { x1,...,xn | y1,...,ym }, les variables x sont les - * variables en lecture seule et y1 les variables modifiées - * les xi sont libres dans P et Q, et les yi,result liées dans Q - * i.e. P = p(x) - * et Q = [y1]...[yn][res]q(x,y,res) - *) - -(* pre and post conditions *) - -type 'a precondition = { p_assert : bool; p_name : Names.name; p_value : 'a } - -type 'a assertion = { a_name : Names.name; a_value : 'a } - -type 'a postcondition = 'a assertion - -type predicate = constr assertion - -(* binders *) - -type 'a binder_type = - BindType of 'a - | BindSet - | Untyped - -type 'a binder = Names.identifier * 'a binder_type - -(* variant *) - -type variant = constr * constr * constr (* phi, R, A *) - -(* types des valeurs *) - -type 'a ml_type_v = - Ref of 'a ml_type_v - | Array of 'a * 'a ml_type_v (* size x type *) - | Arrow of 'a ml_type_v binder list * 'a ml_type_c - - | TypePure of 'a - -(* et type des calculs *) - -and 'a ml_type_c = - (Names.identifier * 'a ml_type_v) - * Peffect.t - * ('a precondition list) * ('a postcondition option) - -(* at beginning they contain Coq AST but they become constr after typing *) -type type_v = constr ml_type_v -type type_c = constr ml_type_c - - diff --git a/contrib/correctness/ptyping.ml b/contrib/correctness/ptyping.ml deleted file mode 100644 index 91c1f293..00000000 --- a/contrib/correctness/ptyping.ml +++ /dev/null @@ -1,600 +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: ptyping.ml 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Pp -open Util -open Names -open Term -open Termops -open Environ -open Constrintern -open Himsg -open Proof_trees -open Topconstr - -open Pmisc -open Putil -open Prename -open Ptype -open Past -open Penv -open Peffect -open Pcicenv - -(* Ce module implante le jugement Gamma |-a e : kappa de la thèse. - * Les annotations passent du type CoqAst.t au type Term.constr ici. - * Les post-conditions sont abstraites par rapport au résultat. *) - -let simplify_type_of env sigma t = - Reductionops.nf_betaiota (Typing.type_of env sigma t) - -let just_reads e = - difference (get_reads e) (get_writes e) - -let type_v_sup loc t1 t2 = - if t1 = t2 then - t1 - else - Perror.if_branches loc - -let typed_var ren env (phi,r) = - let sign = Pcicenv.before_after_sign_of ren env in - let a = simplify_type_of (Global.env_of_context sign) Evd.empty phi in - (phi,r,a) - -(* Application de fonction *) - -let rec convert = function - | (TypePure c1, TypePure c2) -> - Reductionops.is_conv (Global.env ()) Evd.empty c1 c2 - | (Ref v1, Ref v2) -> - convert (v1,v2) - | (Array (s1,v1), Array (s2,v2)) -> - (Reductionops.is_conv (Global.env ()) Evd.empty s1 s2) && (convert (v1,v2)) - | (v1,v2) -> v1 = v2 - -let effect_app ren env f args = - let n = List.length args in - let tf = - let ((_,v),_,_,_) = f.info.kappa in - match v with TypePure c -> v_of_constr c | _ -> v - in - let bl,c = - match tf with - Arrow (bl, c) -> - if List.length bl <> n then Perror.partial_app f.loc; - bl,c - | _ -> Perror.app_of_non_function f.loc - in - let check_type loc v t so = - let v' = type_v_rsubst so v in - if not (convert (v',t)) then Perror.expected_type loc (pp_type_v v') - in - let s,so,ok = - (* s est la substitution des références, so celle des autres arg. - * ok nous dit si les arguments sont sans effet i.e. des expressions *) - List.fold_left - (fun (s,so,ok) (b,a) -> - match b,a with - (id,BindType (Ref _ | Array _ as v)), Refarg id' -> - let ta = type_in_env env id' in - check_type f.loc v ta so; - (id,id')::s, so, ok - | _, Refarg _ -> Perror.should_be_a_variable f.loc - | (id,BindType v), Term t -> - let ((_,ta),_,_,_) = t.info.kappa in - check_type t.loc v ta so; - (match t.desc with - Expression c -> s, (id,c)::so, ok - | _ -> s,so,false) - | (id,BindSet), Type v -> - let c = Pmonad.trad_ml_type_v ren env v in - s, (id,c)::so, ok - | (id,BindSet), Term t -> Perror.expects_a_type id t.loc - | (id,BindType _), Type _ -> Perror.expects_a_term id - | (_,Untyped), _ -> invalid_arg "effects_app") - ([],[],true) - (List.combine bl args) - in - let (id,v),ef,pre,post = type_c_subst s c in - (bl,c), (s,so,ok), ((id,type_v_rsubst so v),ef,pre,post) - -(* Execution of a Coq AST. Returns value and type. - * Also returns its variables *) - -let state_coq_ast sign a = - let env = Global.env_of_context sign in - let j = - reraise_with_loc (constr_loc a) (judgment_of_rawconstr Evd.empty env) a in - let ids = global_vars env j.uj_val in - j.uj_val, j.uj_type, ids - -(* [is_pure p] tests wether the program p is an expression or not. *) - -let type_of_expression ren env c = - let sign = now_sign_of ren env in - simplify_type_of (Global.env_of_context sign) Evd.empty c - -let rec is_pure_type_v = function - TypePure _ -> true - | Arrow (bl,c) -> List.for_all is_pure_arg bl & is_pure_type_c c - | Ref _ | Array _ -> false -and is_pure_arg = function - (_,BindType v) -> is_pure_type_v v - | (_,BindSet) -> true - | (_,Untyped) -> false -and is_pure_type_c = function - (_,v),_,[],None -> is_pure_type_v v - | _ -> false - -let rec is_pure_desc ren env = function - Variable id -> - not (is_in_env env id) or (is_pure_type_v (type_in_env env id)) - | Expression c -> - (c = isevar) or (is_pure_cci (type_of_expression ren env c)) - | Acc _ -> true - | TabAcc (_,_,p) -> is_pure ren env p - | Apply (p,args) -> - is_pure ren env p & List.for_all (is_pure_arg ren env) args - | SApp _ | Aff _ | TabAff _ | Seq _ | While _ | If _ - | Lam _ | LetRef _ | Let _ | LetRec _ -> false - | Debug (_,p) -> is_pure ren env p - | PPoint (_,d) -> is_pure_desc ren env d -and is_pure ren env p = - p.pre = [] & p.post = None & is_pure_desc ren env p.desc -and is_pure_arg ren env = function - Term p -> is_pure ren env p - | Type _ -> true - | Refarg _ -> false - -(* [state_var ren env (phi,r)] returns a tuple (e,(phi',r')) - * where e is the effect of the variant phi and phi',r' the corresponding - * constr of phi and r. - *) - -let state_var ren env (phi,r) = - let sign = Pcicenv.before_after_sign_of ren env in - let phi',_,ids = state_coq_ast sign phi in - let ef = List.fold_left - (fun e id -> - if is_mutable_in_env env id then Peffect.add_read id e else e) - Peffect.bottom ids in - let r',_,_ = state_coq_ast (Global.named_context ()) r in - ef,(phi',r') - -(* [state_pre ren env pl] returns a pair (e,c) where e is the effect of the - * pre-conditions list pl and cl the corresponding constrs not yet abstracted - * over the variables xi (i.e. c NOT [x1]...[xn]c !) - *) - -let state_pre ren env pl = - let state e p = - let sign = Pcicenv.before_sign_of ren env in - let cc,_,ids = state_coq_ast sign p.p_value in - let ef = List.fold_left - (fun e id -> - if is_mutable_in_env env id then - Peffect.add_read id e - else if is_at id then - let uid,_ = un_at id in - if is_mutable_in_env env uid then - Peffect.add_read uid e - else - e - else - e) - e ids - in - ef,{ p_assert = p.p_assert; p_name = p.p_name; p_value = cc } - in - List.fold_left - (fun (e,cl) p -> let ef,c = state e p in (ef,c::cl)) - (Peffect.bottom,[]) pl - -let state_assert ren env a = - let p = pre_of_assert true a in - let e,l = state_pre ren env [p] in - e,assert_of_pre (List.hd l) - -let state_inv ren env = function - None -> Peffect.bottom, None - | Some i -> let e,p = state_assert ren env i in e,Some p - -(* [state_post ren env (id,v,ef) q] returns a pair (e,c) - * where e is the effect of the - * post-condition q and c the corresponding constr not yet abstracted - * over the variables xi, yi and result. - * Moreover the RW variables not appearing in ef have been replaced by - * RO variables, and (id,v) is the result - *) - -let state_post ren env (id,v,ef) = function - None -> Peffect.bottom, None - | Some q -> - let v' = Pmonad.trad_ml_type_v ren env v in - let sign = Pcicenv.before_after_result_sign_of (Some (id,v')) ren env in - let cc,_,ids = state_coq_ast sign q.a_value in - let ef,c = - List.fold_left - (fun (e,c) id -> - if is_mutable_in_env env id then - if is_write ef id then - Peffect.add_write id e, c - else - Peffect.add_read id e, - subst_in_constr [id,at_id id ""] c - else if is_at id then - let uid,_ = un_at id in - if is_mutable_in_env env uid then - Peffect.add_read uid e, c - else - e,c - else - e,c) - (Peffect.bottom,cc) ids - in - let c = abstract [id,v'] c in - ef, Some { a_name = q.a_name; a_value = c } - -(* transformation of AST into constr in types V and C *) - -let rec cic_type_v env ren = function - | Ref v -> Ref (cic_type_v env ren v) - | Array (com,v) -> - let sign = Pcicenv.now_sign_of ren env in - let c = interp_constr Evd.empty (Global.env_of_context sign) com in - Array (c, cic_type_v env ren v) - | Arrow (bl,c) -> - let bl',ren',env' = - List.fold_left - (fun (bl,ren,env) b -> - let b' = cic_binder env ren b in - let env' = traverse_binders env [b'] in - let ren' = initial_renaming env' in - b'::bl,ren',env') - ([],ren,env) bl - in - let c' = cic_type_c env' ren' c in - Arrow (List.rev bl',c') - | TypePure com -> - let sign = Pcicenv.cci_sign_of ren env in - let c = interp_constr Evd.empty (Global.env_of_context sign) com in - TypePure c - -and cic_type_c env ren ((id,v),e,p,q) = - let v' = cic_type_v env ren v in - let cv = Pmonad.trad_ml_type_v ren env v' in - let efp,p' = state_pre ren env p in - let efq,q' = state_post ren env (id,v',e) q in - let ef = Peffect.union e (Peffect.union efp efq) in - ((id,v'),ef,p',q') - -and cic_binder env ren = function - | (id,BindType v) -> - let v' = cic_type_v env ren v in - let env' = add (id,v') env in - let ren' = initial_renaming env' in - (id, BindType v') - | (id,BindSet) -> (id,BindSet) - | (id,Untyped) -> (id,Untyped) - -and cic_binders env ren = function - [] -> [] - | b::bl -> - let b' = cic_binder env ren b in - let env' = traverse_binders env [b'] in - let ren' = initial_renaming env' in - b' :: (cic_binders env' ren' bl) - - -(* The case of expressions. - * - * Expressions are programs without neither effects nor pre/post conditions. - * But access to variables are allowed. - * - * Here we transform an expression into the corresponding constr, - * the variables still appearing as VAR (they will be abstracted in - * Mlise.trad) - * We collect the pre-conditions (e<N for t[e]) as we traverse the term. - * We also return the effect, which does contain only *read* variables. - *) - -let states_expression ren env expr = - let rec effect pl = function - | Variable id -> - (if is_global id then constant (string_of_id id) else mkVar id), - pl, Peffect.bottom - | Expression c -> c, pl, Peffect.bottom - | Acc id -> mkVar id, pl, Peffect.add_read id Peffect.bottom - | TabAcc (_,id,p) -> - let c,pl,ef = effect pl p.desc in - let pre = Pmonad.make_pre_access ren env id c in - Pmonad.make_raw_access ren env (id,id) c, - (anonymous_pre true pre)::pl, Peffect.add_read id ef - | Apply (p,args) -> - let a,pl,e = effect pl p.desc in - let args,pl,e = - List.fold_right - (fun arg (l,pl,e) -> - match arg with - Term p -> - let carg,pl,earg = effect pl p.desc in - carg::l,pl,Peffect.union e earg - | Type v -> - let v' = cic_type_v env ren v in - (Pmonad.trad_ml_type_v ren env v')::l,pl,e - | Refarg _ -> assert false) - args ([],pl,e) - in - Term.applist (a,args),pl,e - | _ -> invalid_arg "Ptyping.states_expression" - in - let e0,pl0 = state_pre ren env expr.pre in - let c,pl,e = effect [] expr.desc in - let sign = Pcicenv.before_sign_of ren env in - (*i WAS - let c = (Trad.ise_resolve true empty_evd [] (gLOB sign) c)._VAL in - i*) - let ty = simplify_type_of (Global.env_of_context sign) Evd.empty c in - let v = TypePure ty in - let ef = Peffect.union e0 e in - Expression c, (v,ef), pl0@pl - - -(* We infer here the type with effects. - * The type of types with effects (ml_type_c) is defined in the module ProgAst. - * - * A program of the shape {P} e {Q} has a type - * - * V, E, {None|Some P}, {None|Some Q} - * - * where - V is the type of e - * - E = (I,O) is the effect; the input I contains - * all the input variables appearing in P,e and Q; - * the output O contains variables possibly modified in e - * - P is NOT abstracted - * - Q = [y'1]...[y'k][result]Q where O = {y'j} - * i.e. Q is only abstracted over the output and the result - * the other variables now refer to value BEFORE - *) - -let verbose_fix = ref false - -let rec states_desc ren env loc = function - - Expression c -> - let ty = type_of_expression ren env c in - let v = v_of_constr ty in - Expression c, (v,Peffect.bottom) - - | Acc _ -> - failwith "Ptyping.states: term is supposed not to be pure" - - | Variable id -> - let v = type_in_env env id in - let ef = Peffect.bottom in - Variable id, (v,ef) - - | Aff (x, e1) -> - Perror.check_for_reference loc x (type_in_env env x); - let s_e1 = states ren env e1 in - let _,e,_,_ = s_e1.info.kappa in - let ef = add_write x e in - let v = constant_unit () in - Aff (x, s_e1), (v, ef) - - | TabAcc (check, x, e) -> - let s_e = states ren env e in - let _,efe,_,_ = s_e.info.kappa in - let ef = Peffect.add_read x efe in - let _,ty = dearray_type (type_in_env env x) in - TabAcc (check, x, s_e), (ty, ef) - - | TabAff (check, x, e1, e2) -> - let s_e1 = states ren env e1 in - let s_e2 = states ren env e2 in - let _,ef1,_,_ = s_e1.info.kappa in - let _,ef2,_,_ = s_e2.info.kappa in - let ef = Peffect.add_write x (Peffect.union ef1 ef2) in - let v = constant_unit () in - TabAff (check, x, s_e1, s_e2), (v,ef) - - | Seq bl -> - let bl,v,ef,_ = states_block ren env bl in - Seq bl, (v,ef) - - | While(b, invopt, var, bl) -> - let efphi,(cvar,r') = state_var ren env var in - let ren' = next ren [] in - let s_b = states ren' env b in - let s_bl,_,ef_bl,_ = states_block ren' env bl in - let cb = s_b.info.kappa in - let efinv,inv = state_inv ren env invopt in - let _,efb,_,_ = s_b.info.kappa in - let ef = - Peffect.union (Peffect.union ef_bl efb) (Peffect.union efinv efphi) - in - let v = constant_unit () in - let cvar = - let al = List.map (fun id -> (id,at_id id "")) (just_reads ef) in - subst_in_constr al cvar - in - While (s_b,inv,(cvar,r'),s_bl), (v,ef) - - | Lam ([],_) -> - failwith "Ptyping.states: abs. should have almost one binder" - - | Lam (bl, e) -> - let bl' = cic_binders env ren bl in - let env' = traverse_binders env bl' in - let ren' = initial_renaming env' in - let s_e = states ren' env' e in - let v = make_arrow bl' s_e.info.kappa in - let ef = Peffect.bottom in - Lam(bl',s_e), (v,ef) - - (* Connectives AND and OR *) - | SApp ([Variable id], [e1;e2]) -> - let s_e1 = states ren env e1 - and s_e2 = states ren env e2 in - let (_,ef1,_,_) = s_e1.info.kappa - and (_,ef2,_,_) = s_e2.info.kappa in - let ef = Peffect.union ef1 ef2 in - SApp ([Variable id], [s_e1; s_e2]), - (TypePure (constant "bool"), ef) - - (* Connective NOT *) - | SApp ([Variable id], [e]) -> - let s_e = states ren env e in - let (_,ef,_,_) = s_e.info.kappa in - SApp ([Variable id], [s_e]), - (TypePure (constant "bool"), ef) - - | SApp _ -> invalid_arg "Ptyping.states (SApp)" - - (* ATTENTION: - Si un argument réel de type ref. correspond à une ref. globale - modifiée par la fonction alors la traduction ne sera pas correcte. - Exemple: - f=[x:ref Int]( r := !r+1 ; x := !x+1) modifie r et son argument x - donc si on l'applique à r justement, elle ne modifiera que r - mais le séquencement ne sera pas correct. *) - - | Apply (f, args) -> - let s_f = states ren env f in - let _,eff,_,_ = s_f.info.kappa in - let s_args = List.map (states_arg ren env) args in - let ef_args = - List.map - (function Term t -> let (_,e,_,_) = t.info.kappa in e - | _ -> Peffect.bottom) - s_args - in - let _,_,((_,tapp),efapp,_,_) = effect_app ren env s_f s_args in - let ef = - Peffect.compose (List.fold_left Peffect.compose eff ef_args) efapp - in - Apply (s_f, s_args), (tapp, ef) - - | LetRef (x, e1, e2) -> - let s_e1 = states ren env e1 in - let (_,v1),ef1,_,_ = s_e1.info.kappa in - let env' = add (x,Ref v1) env in - let ren' = next ren [x] in - let s_e2 = states ren' env' e2 in - let (_,v2),ef2,_,_ = s_e2.info.kappa in - Perror.check_for_let_ref loc v2; - let ef = Peffect.compose ef1 (Peffect.remove ef2 x) in - LetRef (x, s_e1, s_e2), (v2,ef) - - | Let (x, e1, e2) -> - let s_e1 = states ren env e1 in - let (_,v1),ef1,_,_ = s_e1.info.kappa in - Perror.check_for_not_mutable e1.loc v1; - let env' = add (x,v1) env in - let s_e2 = states ren env' e2 in - let (_,v2),ef2,_,_ = s_e2.info.kappa in - let ef = Peffect.compose ef1 ef2 in - Let (x, s_e1, s_e2), (v2,ef) - - | If (b, e1, e2) -> - let s_b = states ren env b in - let s_e1 = states ren env e1 - and s_e2 = states ren env e2 in - let (_,tb),efb,_,_ = s_b.info.kappa in - let (_,t1),ef1,_,_ = s_e1.info.kappa in - let (_,t2),ef2,_,_ = s_e2.info.kappa in - let ef = Peffect.compose efb (disj ef1 ef2) in - let v = type_v_sup loc t1 t2 in - If (s_b, s_e1, s_e2), (v,ef) - - | LetRec (f,bl,v,var,e) -> - let bl' = cic_binders env ren bl in - let env' = traverse_binders env bl' in - let ren' = initial_renaming env' in - let v' = cic_type_v env' ren' v in - let efvar,var' = state_var ren' env' var in - let phi0 = phi_name () in - let tvar = typed_var ren env' var' in - (* effect for a let/rec construct is computed as a fixpoint *) - let rec state_rec c = - let tf = make_arrow bl' c in - let env'' = add_recursion (f,(phi0,tvar)) (add (f,tf) env') in - let s_e = states ren' env'' e in - if s_e.info.kappa = c then - s_e - else begin - if !verbose_fix then begin msgnl (pp_type_c s_e.info.kappa) end ; - state_rec s_e.info.kappa - end - in - let s_e = state_rec ((result_id,v'),efvar,[],None) in - let tf = make_arrow bl' s_e.info.kappa in - LetRec (f,bl',v',var',s_e), (tf,Peffect.bottom) - - | PPoint (s,d) -> - let ren' = push_date ren s in - states_desc ren' env loc d - - | Debug _ -> failwith "Ptyping.states: Debug: TODO" - - -and states_arg ren env = function - Term a -> let s_a = states ren env a in Term s_a - | Refarg id -> Refarg id - | Type v -> let v' = cic_type_v env ren v in Type v' - - -and states ren env expr = - (* Here we deal with the pre- and post- conditions: - * we add their effects to the effects of the program *) - let (d,(v,e),p1) = - if is_pure_desc ren env expr.desc then - states_expression ren env expr - else - let (d,ve) = states_desc ren env expr.loc expr.desc in (d,ve,[]) - in - let (ep,p) = state_pre ren env expr.pre in - let (eq,q) = state_post ren env (result_id,v,e) expr.post in - let e' = Peffect.union e (Peffect.union ep eq) in - let p' = p1 @ p in - let tinfo = { env = env; kappa = ((result_id,v),e',p',q) } in - { desc = d; - loc = expr.loc; - pre = p'; post = q; (* on les conserve aussi ici pour prog_wp *) - info = tinfo } - - -and states_block ren env bl = - let rec ef_block ren tyres = function - [] -> - begin match tyres with - Some ty -> [],ty,Peffect.bottom,ren - | None -> failwith "a block should contain at least one statement" - end - | (Assert p)::block -> - let ep,c = state_assert ren env p in - let bl,t,ef,ren' = ef_block ren tyres block in - (Assert c)::bl,t,Peffect.union ep ef,ren' - | (Label s)::block -> - let ren' = push_date ren s in - let bl,t,ef,ren'' = ef_block ren' tyres block in - (Label s)::bl,t,ef,ren'' - | (Statement e)::block -> - let s_e = states ren env e in - let (_,t),efe,_,_ = s_e.info.kappa in - let ren' = next ren (get_writes efe) in - let bl,t,ef,ren'' = ef_block ren' (Some t) block in - (Statement s_e)::bl,t,Peffect.compose efe ef,ren'' - in - ef_block ren None bl - diff --git a/contrib/correctness/ptyping.mli b/contrib/correctness/ptyping.mli deleted file mode 100644 index eaf548b1..00000000 --- a/contrib/correctness/ptyping.mli +++ /dev/null @@ -1,36 +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: ptyping.mli 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Names -open Term -open Topconstr - -open Ptype -open Past -open Penv - -(* This module realizes type and effect inference *) - -val cic_type_v : local_env -> Prename.t -> constr_expr ml_type_v -> type_v - -val effect_app : Prename.t -> local_env - -> (typing_info,'b) Past.t - -> (typing_info,constr) arg list - -> (type_v binder list * type_c) - * ((identifier*identifier) list * (identifier*constr) list * bool) - * type_c - -val typed_var : Prename.t -> local_env -> constr * constr -> variant - -val type_of_expression : Prename.t -> local_env -> constr -> constr - -val states : Prename.t -> local_env -> program -> typed_program diff --git a/contrib/correctness/putil.ml b/contrib/correctness/putil.ml deleted file mode 100644 index 18c3ba35..00000000 --- a/contrib/correctness/putil.ml +++ /dev/null @@ -1,303 +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: putil.ml 8752 2006-04-27 19:37:33Z herbelin $ *) - -open Util -open Names -open Nameops -open Term -open Termops -open Pattern -open Matching -open Hipattern -open Environ - -open Pmisc -open Ptype -open Past -open Penv -open Prename - -let is_mutable = function Ref _ | Array _ -> true | _ -> false -let is_pure = function TypePure _ -> true | _ -> false - -let named_app f x = { a_name = x.a_name; a_value = (f x.a_value) } - -let pre_app f x = - { p_assert = x.p_assert; p_name = x.p_name; p_value = f x.p_value } - -let post_app = named_app - -let anonymous x = { a_name = Anonymous; a_value = x } - -let anonymous_pre b x = { p_assert = b; p_name = Anonymous; p_value = x } - -let force_name f x = - option_map (fun q -> { a_name = Name (f q.a_name); a_value = q.a_value }) x - -let force_post_name x = force_name post_name x - -let force_bool_name x = - force_name (function Name id -> id | Anonymous -> bool_name()) x - -let out_post = function - Some { a_value = x } -> x - | None -> invalid_arg "out_post" - -let pre_of_assert b x = - { p_assert = b; p_name = x.a_name; p_value = x.a_value } - -let assert_of_pre x = - { a_name = x.p_name; a_value = x.p_value } - -(* Some generic functions on programs *) - -let is_mutable_in_env env id = - (is_in_env env id) & (is_mutable (type_in_env env id)) - -let now_vars env c = - Util.map_succeed - (function id -> if is_mutable_in_env env id then id else failwith "caught") - (global_vars (Global.env()) c) - -let make_before_after c = - let ids = global_vars (Global.env()) c in - let al = - Util.map_succeed - (function id -> - if is_at id then - match un_at id with (uid,"") -> (id,uid) | _ -> failwith "caught" - else failwith "caught") - ids - in - subst_in_constr al c - -(* [apply_pre] and [apply_post] instantiate pre- and post- conditions - * according to a given renaming of variables (and a date that means - * `before' in the case of the post-condition). - *) - -let make_assoc_list ren env on_prime ids = - List.fold_left - (fun al id -> - if is_mutable_in_env env id then - (id,current_var ren id)::al - else if is_at id then - let uid,d = un_at id in - if is_mutable_in_env env uid then - (match d with - "" -> (id,on_prime ren uid) - | _ -> (id,var_at_date ren d uid))::al - else - al - else - al) - [] ids - -let apply_pre ren env c = - let ids = global_vars (Global.env()) c.p_value in - let al = make_assoc_list ren env current_var ids in - { p_assert = c.p_assert; p_name = c.p_name; - p_value = subst_in_constr al c.p_value } - -let apply_assert ren env c = - let ids = global_vars (Global.env()) c.a_value in - let al = make_assoc_list ren env current_var ids in - { a_name = c.a_name; a_value = subst_in_constr al c.a_value } - -let apply_post ren env before c = - let ids = global_vars (Global.env()) c.a_value in - let al = - make_assoc_list ren env (fun r uid -> var_at_date r before uid) ids in - { a_name = c.a_name; a_value = subst_in_constr al c.a_value } - -(* [traverse_binder ren env bl] updates renaming [ren] and environment [env] - * as we cross the binders [bl] - *) - -let rec traverse_binders env = function - [] -> env - | (id,BindType v)::rem -> - traverse_binders (add (id,v) env) rem - | (id,BindSet)::rem -> - traverse_binders (add_set id env) rem - | (_,Untyped)::_ -> - invalid_arg "traverse_binders" - -let initial_renaming env = - let ids = Penv.fold_all (fun (id,_) l -> id::l) env [] in - update empty_ren "0" ids - - -(* Substitutions *) - -let rec type_c_subst s ((id,t),e,p,q) = - let s' = s @ List.map (fun (x,x') -> (at_id x "", at_id x' "")) s in - (id, type_v_subst s t), Peffect.subst s e, - List.map (pre_app (subst_in_constr s)) p, - option_map (post_app (subst_in_constr s')) q - -and type_v_subst s = function - Ref v -> Ref (type_v_subst s v) - | Array (n,v) -> Array (n,type_v_subst s v) - | Arrow (bl,c) -> Arrow(List.map (binder_subst s) bl, type_c_subst s c) - | (TypePure _) as v -> v - -and binder_subst s = function - (n, BindType v) -> (n, BindType (type_v_subst s v)) - | b -> b - -(* substitution of constr by others *) - -let rec type_c_rsubst s ((id,t),e,p,q) = - (id, type_v_rsubst s t), e, - List.map (pre_app (real_subst_in_constr s)) p, - option_map (post_app (real_subst_in_constr s)) q - -and type_v_rsubst s = function - Ref v -> Ref (type_v_rsubst s v) - | Array (n,v) -> Array (real_subst_in_constr s n,type_v_rsubst s v) - | Arrow (bl,c) -> Arrow(List.map (binder_rsubst s) bl, type_c_rsubst s c) - | TypePure c -> TypePure (real_subst_in_constr s c) - -and binder_rsubst s = function - | (n, BindType v) -> (n, BindType (type_v_rsubst s v)) - | b -> b - -(* make_arrow bl c = (x1:V1)...(xn:Vn)c *) - -let make_arrow bl c = match bl with - | [] -> invalid_arg "make_arrow: no binder" - | _ -> Arrow (bl,c) - -(* misc. functions *) - -let deref_type = function - | Ref v -> v - | _ -> invalid_arg "deref_type" - -let dearray_type = function - | Array (size,v) -> size,v - | _ -> invalid_arg "dearray_type" - -let constant_unit () = TypePure (constant "unit") - -let id_from_name = function Name id -> id | Anonymous -> (id_of_string "X") - -(* v_of_constr : traduit un type CCI en un type ML *) - -(* TODO: faire un test plus serieux sur le type des objets Coq *) -let rec is_pure_cci c = match kind_of_term c with - | Cast (c,_) -> is_pure_cci c - | Prod(_,_,c') -> is_pure_cci c' - | Rel _ | Ind _ | Const _ -> true (* heu... *) - | App _ -> not (is_matching_sigma c) - | _ -> Util.error "CCI term not acceptable in programs" - -let rec v_of_constr c = match kind_of_term c with - | Cast (c,_) -> v_of_constr c - | Prod _ -> - let revbl,t2 = Term.decompose_prod c in - let bl = - List.map - (fun (name,t1) -> (id_from_name name, BindType (v_of_constr t1))) - (List.rev revbl) - in - let vars = List.rev (List.map (fun (id,_) -> mkVar id) bl) in - Arrow (bl, c_of_constr (substl vars t2)) - | Ind _ | Const _ | App _ -> - TypePure c - | _ -> - failwith "v_of_constr: TODO" - -and c_of_constr c = - if is_matching_sigma c then - let (a,q) = match_sigma c in - (result_id, v_of_constr a), Peffect.bottom, [], Some (anonymous q) - else - (result_id, v_of_constr c), Peffect.bottom, [], None - - -(* pretty printers (for debugging purposes) *) - -open Pp -open Util - -let pr_lconstr x = Printer.pr_lconstr_env (Global.env()) x - -let pp_pre = function - [] -> (mt ()) - | l -> - hov 0 (str"pre " ++ - prlist_with_sep (fun () -> (spc ())) - (fun x -> pr_lconstr x.p_value) l) - -let pp_post = function - None -> (mt ()) - | Some c -> hov 0 (str"post " ++ pr_lconstr c.a_value) - -let rec pp_type_v = function - Ref v -> hov 0 (pp_type_v v ++ spc () ++ str"ref") - | Array (cc,v) -> hov 0 (str"array " ++ pr_lconstr cc ++ str" of " ++ pp_type_v v) - | Arrow (b,c) -> - hov 0 (prlist_with_sep (fun () -> (mt ())) pp_binder b ++ - pp_type_c c) - | TypePure c -> pr_lconstr c - -and pp_type_c ((id,v),e,p,q) = - hov 0 (str"returns " ++ pr_id id ++ str":" ++ pp_type_v v ++ spc () ++ - Peffect.pp e ++ spc () ++ pp_pre p ++ spc () ++ pp_post q ++ - spc () ++ str"end") - -and pp_binder = function - id,BindType v -> (str"(" ++ pr_id id ++ str":" ++ pp_type_v v ++ str")") - | id,BindSet -> (str"(" ++ pr_id id ++ str":Set)") - | id,Untyped -> (str"(" ++ pr_id id ++ str")") - -(* pretty-print of cc-terms (intermediate terms) *) - -let rec pp_cc_term = function - CC_var id -> pr_id id - | CC_letin (_,_,bl,c,c1) -> - hov 0 (hov 2 (str"let " ++ - prlist_with_sep (fun () -> (str",")) - (fun (id,_) -> pr_id id) bl ++ - str" =" ++ spc () ++ - pp_cc_term c ++ - str " in") ++ - fnl () ++ - pp_cc_term c1) - | CC_lam (bl,c) -> - hov 2 (prlist (fun (id,_) -> (str"[" ++ pr_id id ++ str"]")) bl ++ - cut () ++ - pp_cc_term c) - | CC_app (f,args) -> - hov 2 (str"(" ++ - pp_cc_term f ++ spc () ++ - prlist_with_sep (fun () -> (spc ())) pp_cc_term args ++ - str")") - | CC_tuple (_,_,cl) -> - hov 2 (str"(" ++ - prlist_with_sep (fun () -> (str"," ++ cut ())) - pp_cc_term cl ++ - str")") - | CC_case (_,b,[e1;e2]) -> - hov 0 (str"if " ++ pp_cc_term b ++ str" then" ++ fnl () ++ - str" " ++ hov 0 (pp_cc_term e1) ++ fnl () ++ - str"else" ++ fnl () ++ - str" " ++ hov 0 (pp_cc_term e2)) - | CC_case _ -> - hov 0 (str"<Case: not yet implemented>") - | CC_expr c -> - hov 0 (pr_lconstr c) - | CC_hole c -> - (str"(?::" ++ pr_lconstr c ++ str")") - diff --git a/contrib/correctness/putil.mli b/contrib/correctness/putil.mli deleted file mode 100644 index 6c487f3f..00000000 --- a/contrib/correctness/putil.mli +++ /dev/null @@ -1,72 +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: putil.mli 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Pp -open Names -open Term -open Pmisc -open Ptype -open Past -open Penv - -val is_mutable : 'a ml_type_v -> bool -val is_pure : 'a ml_type_v -> bool - -val named_app : ('a -> 'b) -> 'a assertion -> 'b assertion -val pre_app : ('a -> 'b) -> 'a precondition -> 'b precondition -val post_app : ('a -> 'b) -> 'a postcondition -> 'b postcondition - -val anonymous : 'a -> 'a assertion -val anonymous_pre : bool -> 'a -> 'a precondition -val out_post : 'a postcondition option -> 'a -val pre_of_assert : bool -> 'a assertion -> 'a precondition -val assert_of_pre : 'a precondition -> 'a assertion - -val force_post_name : 'a postcondition option -> 'a postcondition option -val force_bool_name : 'a postcondition option -> 'a postcondition option - -val make_before_after : constr -> constr - -val traverse_binders : local_env -> (type_v binder) list -> local_env -val initial_renaming : local_env -> Prename.t - -val apply_pre : Prename.t -> local_env -> constr precondition -> - constr precondition -val apply_post : Prename.t -> local_env -> string -> constr postcondition -> - constr postcondition -val apply_assert : Prename.t -> local_env -> constr assertion -> - constr assertion - -val type_v_subst : (identifier * identifier) list -> type_v -> type_v -val type_c_subst : (identifier * identifier) list -> type_c -> type_c - -val type_v_rsubst : (identifier * constr) list -> type_v -> type_v -val type_c_rsubst : (identifier * constr) list -> type_c -> type_c - -val make_arrow : ('a ml_type_v binder) list -> 'a ml_type_c -> 'a ml_type_v - -val is_mutable_in_env : local_env -> identifier -> bool -val now_vars : local_env -> constr -> identifier list - -val deref_type : 'a ml_type_v -> 'a ml_type_v -val dearray_type : 'a ml_type_v -> 'a * 'a ml_type_v -val constant_unit : unit -> constr ml_type_v -val v_of_constr : constr -> constr ml_type_v -val c_of_constr : constr -> constr ml_type_c -val is_pure_cci : constr -> bool - -(* pretty printers *) - -val pp_type_v : type_v -> std_ppcmds -val pp_type_c : type_c -> std_ppcmds -val pp_cc_term : cc_term -> std_ppcmds - diff --git a/contrib/correctness/pwp.ml b/contrib/correctness/pwp.ml deleted file mode 100644 index f422c5cd..00000000 --- a/contrib/correctness/pwp.ml +++ /dev/null @@ -1,347 +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: pwp.ml 8752 2006-04-27 19:37:33Z herbelin $ *) - -open Util -open Names -open Libnames -open Term -open Termops -open Environ -open Nametab - -open Pmisc -open Ptype -open Past -open Putil -open Penv -open Peffect -open Ptyping -open Prename - -(* In this module: - * - we try to insert more annotations to achieve a greater completeness; - * - we recursively propagate annotations inside programs; - * - we normalize boolean expressions. - * - * The propagation schemas are the following: - * - * 1. (f a1 ... an) -> (f a1 ... an) {Qf} if the ai are functional - * - * 2. (if e1 then e2 else e3) {Q} -> (if e1 then e2 {Q} else e3 {Q}) {Q} - * - * 3. (let x = e1 in e2) {Q} -> (let x = e1 in e2 {Q}) {Q} - *) - -(* force a post-condition *) -let update_post env top ef c = - let i,o = Peffect.get_repr ef in - let al = - List.fold_left - (fun l id -> - if is_mutable_in_env env id then - if is_write ef id then l else (id,at_id id "")::l - else if is_at id then - let (uid,d) = un_at id in - if is_mutable_in_env env uid & d="" then - (id,at_id uid top)::l - else - l - else - l) - [] (global_vars (Global.env()) c) - in - subst_in_constr al c - -let force_post up env top q e = - let (res,ef,p,_) = e.info.kappa in - let q' = - if up then option_map (named_app (update_post env top ef)) q else q - in - let i = { env = e.info.env; kappa = (res,ef,p,q') } in - { desc = e.desc; pre = e.pre; post = q'; loc = e.loc; info = i } - -(* put a post-condition if none is present *) -let post_if_none_up env top q = function - | { post = None } as p -> force_post true env top q p - | p -> p - -let post_if_none env q = function - | { post = None } as p -> force_post false env "" q p - | p -> p - -(* [annotation_candidate p] determines if p is a candidate for a - * post-condition *) - -let annotation_candidate = function - | { desc = If _ | Let _ | LetRef _ ; post = None } -> true - | _ -> false - -(* [extract_pre p] erase the pre-condition of p and returns it *) -let extract_pre pr = - let (v,e,p,q) = pr.info.kappa in - { desc = pr.desc; pre = []; post = pr.post; loc = pr.loc; - info = { env = pr.info.env; kappa = (v,e,[],q) } }, - p - -(* adds some pre-conditions *) -let add_pre p1 pr = - let (v,e,p,q) = pr.info.kappa in - let p' = p1 @ p in - { desc = pr.desc; pre = p'; post = pr.post; loc = pr.loc; - info = { env = pr.info.env; kappa = (v,e,p',q) } } - -(* change the statement *) -let change_desc p d = - { desc = d; pre = p.pre; post = p.post; loc = p.loc; info = p.info } - -let create_bool_post c = - Some { a_value = c; a_name = Name (bool_name()) } - -(* [normalize_boolean b] checks if the boolean expression b (of type bool) is - * annotated, and if it is not the case tries to add the annotation - * (if result then c=true else c=false) if b is an expression c. - *) - -let is_bool = function - | TypePure c -> - (match kind_of_term (strip_outer_cast c) with - | Ind op -> - string_of_id (id_of_global (IndRef op)) = "bool" - | _ -> false) - | _ -> false - -let normalize_boolean ren env b = - let ((res,v),ef,p,q) = b.info.kappa in - Perror.check_no_effect b.loc ef; - if is_bool v then - match q with - | Some _ -> - (* il y a une annotation : on se contente de lui forcer un nom *) - let q = force_bool_name q in - { desc = b.desc; pre = b.pre; post = q; loc = b.loc; - info = { env = b.info.env; kappa = ((res,v),ef,p,q) } } - | None -> begin - (* il n'y a pas d'annotation : on cherche à en mettre une *) - match b.desc with - Expression c -> - let c' = Term.applist (constant "annot_bool",[c]) in - let ty = type_of_expression ren env c' in - let (_,q') = Hipattern.match_sigma ty in - let q' = Some { a_value = q'; a_name = Name (bool_name()) } in - { desc = Expression c'; - pre = b.pre; post = q'; loc = b.loc; - info = { env = b.info.env; kappa = ((res, v),ef,p,q') } } - | _ -> b - end - else - Perror.should_be_boolean b.loc - -(* [decomp_boolean c] returns the specs R and S of a boolean expression *) - -let decomp_boolean = function - | Some { a_value = q } -> - Reductionops.whd_betaiota (Term.applist (q, [constant "true"])), - Reductionops.whd_betaiota (Term.applist (q, [constant "false"])) - | _ -> invalid_arg "Ptyping.decomp_boolean" - -(* top point of a program *) - -let top_point = function - | PPoint (s,_) as p -> s,p - | p -> let s = label_name() in s,PPoint(s,p) - -let top_point_block = function - | (Label s :: _) as b -> s,b - | b -> let s = label_name() in s,(Label s)::b - -let abstract_unit q = abstract [result_id,constant "unit"] q - -(* [add_decreasing env ren ren' phi r bl] adds the decreasing condition - * phi(ren') r phi(ren) - * to the last assertion of the block [bl], which is created if needed - *) - -let add_decreasing env inv (var,r) lab bl = - let ids = now_vars env var in - let al = List.map (fun id -> (id,at_id id lab)) ids in - let var_lab = subst_in_constr al var in - let dec = Term.applist (r, [var;var_lab]) in - let post = match inv with - None -> anonymous dec - | Some i -> { a_value = conj dec i.a_value; a_name = i.a_name } - in - bl @ [ Assert post ] - -(* [post_last_statement env top q bl] annotates the last statement of the - * sequence bl with q if necessary *) - -let post_last_statement env top q bl = - match List.rev bl with - | Statement e :: rem when annotation_candidate e -> - List.rev ((Statement (post_if_none_up env top q e)) :: rem) - | _ -> bl - -(* [propagate_desc] moves the annotations inside the program - * info is the typing information coming from the outside annotations *) -let rec propagate_desc ren info d = - let env = info.env in - let (_,_,p,q) = info.kappa in - match d with - | If (e1,e2,e3) -> - (* propagation number 2 *) - let e1' = normalize_boolean ren env (propagate ren e1) in - if e2.post = None or e3.post = None then - let top = label_name() in - let ren' = push_date ren top in - PPoint (top, If (e1', - propagate ren' (post_if_none_up env top q e2), - propagate ren' (post_if_none_up env top q e3))) - else - If (e1', propagate ren e2, propagate ren e3) - | Aff (x,e) -> - Aff (x, propagate ren e) - | TabAcc (ch,x,e) -> - TabAcc (ch, x, propagate ren e) - | TabAff (ch,x,({desc=Expression c} as e1),e2) -> - let p = Pmonad.make_pre_access ren env x c in - let e1' = add_pre [(anonymous_pre true p)] e1 in - TabAff (false, x, propagate ren e1', propagate ren e2) - | TabAff (ch,x,e1,e2) -> - TabAff (ch, x, propagate ren e1, propagate ren e2) - | Apply (f,l) -> - Apply (propagate ren f, List.map (propagate_arg ren) l) - | SApp (f,l) -> - let l = - List.map (fun e -> normalize_boolean ren env (propagate ren e)) l - in - SApp (f, l) - | Lam (bl,e) -> - Lam (bl, propagate ren e) - | Seq bl -> - let top,bl = top_point_block bl in - let bl = post_last_statement env top q bl in - Seq (propagate_block ren env bl) - | While (b,inv,var,bl) -> - let b = normalize_boolean ren env (propagate ren b) in - let lab,bl = top_point_block bl in - let bl = add_decreasing env inv var lab bl in - While (b,inv,var,propagate_block ren env bl) - | LetRef (x,e1,e2) -> - let top = label_name() in - let ren' = push_date ren top in - PPoint (top, LetRef (x, propagate ren' e1, - propagate ren' (post_if_none_up env top q e2))) - | Let (x,e1,e2) -> - let top = label_name() in - let ren' = push_date ren top in - PPoint (top, Let (x, propagate ren' e1, - propagate ren' (post_if_none_up env top q e2))) - | LetRec (f,bl,v,var,e) -> - LetRec (f, bl, v, var, propagate ren e) - | PPoint (s,d) -> - PPoint (s, propagate_desc ren info d) - | Debug _ | Variable _ - | Acc _ | Expression _ as d -> d - - -(* [propagate] adds new annotations if possible *) -and propagate ren p = - let env = p.info.env in - let p = match p.desc with - | Apply (f,l) -> - let _,(_,so,ok),(_,_,_,qapp) = effect_app ren env f l in - if ok then - let q = option_map (named_app (real_subst_in_constr so)) qapp in - post_if_none env q p - else - p - | _ -> p - in - let d = propagate_desc ren p.info p.desc in - let p = change_desc p d in - match d with - | Aff (x,e) -> - let e1,p1 = extract_pre e in - change_desc (add_pre p1 p) (Aff (x,e1)) - - | TabAff (check, x, ({ desc = Expression _ } as e1), e2) -> - let e1',p1 = extract_pre e1 in - let e2',p2 = extract_pre e2 in - change_desc (add_pre (p1@p2) p) (TabAff (check,x,e1',e2')) - - | While (b,inv,_,_) -> - let _,s = decomp_boolean b.post in - let s = make_before_after s in - let q = match inv with - None -> Some (anonymous s) - | Some i -> Some { a_value = conj i.a_value s; a_name = i.a_name } - in - let q = option_map (named_app abstract_unit) q in - post_if_none env q p - - | SApp ([Variable id], [e1;e2]) - when id = connective_and or id = connective_or -> - let (_,_,_,q1) = e1.info.kappa - and (_,_,_,q2) = e2.info.kappa in - let (r1,s1) = decomp_boolean q1 - and (r2,s2) = decomp_boolean q2 in - let q = - let conn = if id = connective_and then "spec_and" else "spec_or" in - let c = Term.applist (constant conn, [r1; s1; r2; s2]) in - let c = Reduction.whd_betadeltaiota (Global.env()) c in - create_bool_post c - in - let d = - SApp ([Variable id; - Expression (out_post q1); - Expression (out_post q2)], - [e1; e2] ) - in - post_if_none env q (change_desc p d) - - | SApp ([Variable id], [e1]) when id = connective_not -> - let (_,_,_,q1) = e1.info.kappa in - let (r1,s1) = decomp_boolean q1 in - let q = - let c = Term.applist (constant "spec_not", [r1; s1]) in - let c = Reduction.whd_betadeltaiota (Global.env ()) c in - create_bool_post c - in - let d = SApp ([Variable id; Expression (out_post q1)], [ e1 ]) in - post_if_none env q (change_desc p d) - - | _ -> p - -and propagate_arg ren = function - | Type _ | Refarg _ as a -> a - | Term e -> Term (propagate ren e) - - -and propagate_block ren env = function - | [] -> - [] - | (Statement p) :: (Assert q) :: rem when annotation_candidate p -> - (* TODO: plutot p.post = None ? *) - let q' = - let ((id,v),_,_,_) = p.info.kappa in - let tv = Pmonad.trad_ml_type_v ren env v in - named_app (abstract [id,tv]) q - in - let p' = post_if_none env (Some q') p in - (Statement (propagate ren p')) :: (Assert q) - :: (propagate_block ren env rem) - | (Statement p) :: rem -> - (Statement (propagate ren p)) :: (propagate_block ren env rem) - | (Label s as x) :: rem -> - x :: propagate_block (push_date ren s) env rem - | x :: rem -> - x :: propagate_block ren env rem diff --git a/contrib/correctness/pwp.mli b/contrib/correctness/pwp.mli deleted file mode 100644 index 4027a623..00000000 --- a/contrib/correctness/pwp.mli +++ /dev/null @@ -1,18 +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: pwp.mli 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Term -open Penv - -val update_post : local_env -> string -> Peffect.t -> constr -> constr - -val propagate : Prename.t -> typed_program -> typed_program |