diff options
Diffstat (limited to 'contrib/correctness/ptyping.ml')
-rw-r--r-- | contrib/correctness/ptyping.ml | 600 |
1 files changed, 600 insertions, 0 deletions
diff --git a/contrib/correctness/ptyping.ml b/contrib/correctness/ptyping.ml new file mode 100644 index 00000000..9047a925 --- /dev/null +++ b/contrib/correctness/ptyping.ml @@ -0,0 +1,600 @@ +(************************************************************************) +(* 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,v 1.7.6.1 2004/07/16 19:30:06 herbelin Exp $ *) + +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 + |