summaryrefslogtreecommitdiff
path: root/contrib/correctness/pmlize.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/correctness/pmlize.ml')
-rw-r--r--contrib/correctness/pmlize.ml320
1 files changed, 320 insertions, 0 deletions
diff --git a/contrib/correctness/pmlize.ml b/contrib/correctness/pmlize.ml
new file mode 100644
index 00000000..f899366d
--- /dev/null
+++ b/contrib/correctness/pmlize.ml
@@ -0,0 +1,320 @@
+(************************************************************************)
+(* 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,v 1.7.2.1 2004/07/16 19:30:01 herbelin Exp $ *)
+
+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
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 14:45:41 +0000