diff options
author | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
commit | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch) | |
tree | dabcac548e299fee1da464c93b3dba98484f45b1 /contrib/correctness/pmisc.ml | |
parent | 2281410e38ef99d025ea77194585a9bc019fdaa9 (diff) |
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'contrib/correctness/pmisc.ml')
-rw-r--r-- | contrib/correctness/pmisc.ml | 222 |
1 files changed, 0 insertions, 222 deletions
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) |