summaryrefslogtreecommitdiff
path: root/contrib/correctness/putil.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/correctness/putil.ml')
-rw-r--r--contrib/correctness/putil.ml303
1 files changed, 303 insertions, 0 deletions
diff --git a/contrib/correctness/putil.ml b/contrib/correctness/putil.ml
new file mode 100644
index 00000000..48f0781a
--- /dev/null
+++ b/contrib/correctness/putil.ml
@@ -0,0 +1,303 @@
+(************************************************************************)
+(* 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,v 1.10.2.1 2004/07/16 19:30:06 herbelin Exp $ *)
+
+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_app (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_app (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_app (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 prterm x = Printer.prterm_env (Global.env()) x
+
+let pp_pre = function
+ [] -> (mt ())
+ | l ->
+ hov 0 (str"pre " ++
+ prlist_with_sep (fun () -> (spc ()))
+ (fun x -> prterm x.p_value) l)
+
+let pp_post = function
+ None -> (mt ())
+ | Some c -> hov 0 (str"post " ++ prterm 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 " ++ prterm 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 -> prterm 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 (prterm c)
+ | CC_hole c ->
+ (str"(?::" ++ prterm c ++ str")")
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 23:50:54 +0000