From 056068abd228fefab4951a61700aa6d54fb88287 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 29 Jan 2013 09:10:29 +0000 Subject: Ported to Coq 8.4pl1. Merge of branches/coq-8.4. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/SimplExprspec.v | 212 +++++++++++++++++++++++----------------------- 1 file changed, 106 insertions(+), 106 deletions(-) (limited to 'cfrontend/SimplExprspec.v') diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v index 571a9373..5cb0f189 100644 --- a/cfrontend/SimplExprspec.v +++ b/cfrontend/SimplExprspec.v @@ -35,9 +35,9 @@ Local Open Scope gensym_monad_scope. (** This specification covers: - all cases of [transl_lvalue] and [transl_rvalue]; -- two additional cases for [C.Eparen], so that reductions of [C.Econdition] +- two additional cases for [Csyntax.Eparen], so that reductions of [Csyntax.Econdition] expressions are properly tracked; -- three additional cases allowing [C.Eval v] C expressions to match +- three additional cases allowing [Csyntax.Eval v] C expressions to match any Clight expression [a] that evaluates to [v] in any environment matching the given temporary environment [le]. *) @@ -57,69 +57,69 @@ Inductive tr_rvalof: type -> expr -> list statement -> expr -> list ident -> Pro type_is_volatile ty = true -> In t tmp -> tr_rvalof ty a (make_set t a :: nil) (Etempvar t ty) tmp. -Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr -> list ident -> Prop := +Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement -> expr -> list ident -> Prop := | tr_var: forall le dst id ty tmp, - tr_expr le dst (C.Evar id ty) + tr_expr le dst (Csyntax.Evar id ty) (final dst (Evar id ty)) (Evar id ty) tmp | tr_deref: forall le dst e1 ty sl1 a1 tmp, tr_expr le For_val e1 sl1 a1 tmp -> - tr_expr le dst (C.Ederef e1 ty) + tr_expr le dst (Csyntax.Ederef e1 ty) (sl1 ++ final dst (Ederef a1 ty)) (Ederef a1 ty) tmp | tr_field: forall le dst e1 f ty sl1 a1 tmp, tr_expr le For_val e1 sl1 a1 tmp -> - tr_expr le dst (C.Efield e1 f ty) + tr_expr le dst (Csyntax.Efield e1 f ty) (sl1 ++ final dst (Efield a1 f ty)) (Efield a1 f ty) tmp | tr_val_effect: forall le v ty any tmp, - tr_expr le For_effects (C.Eval v ty) nil any tmp + tr_expr le For_effects (Csyntax.Eval v ty) nil any tmp | tr_val_value: forall le v ty a tmp, typeof a = ty -> (forall tge e le' m, (forall id, In id tmp -> le'!id = le!id) -> eval_expr tge e le' m a v) -> - tr_expr le For_val (C.Eval v ty) + tr_expr le For_val (Csyntax.Eval v ty) nil a tmp | tr_val_set: forall le tyl t v ty a any tmp, typeof a = ty -> (forall tge e le' m, (forall id, In id tmp -> le'!id = le!id) -> eval_expr tge e le' m a v) -> - tr_expr le (For_set tyl t) (C.Eval v ty) + tr_expr le (For_set tyl t) (Csyntax.Eval v ty) (do_set t tyl a) any tmp | tr_sizeof: forall le dst ty' ty tmp, - tr_expr le dst (C.Esizeof ty' ty) + tr_expr le dst (Csyntax.Esizeof ty' ty) (final dst (Esizeof ty' ty)) (Esizeof ty' ty) tmp | tr_alignof: forall le dst ty' ty tmp, - tr_expr le dst (C.Ealignof ty' ty) + tr_expr le dst (Csyntax.Ealignof ty' ty) (final dst (Ealignof ty' ty)) (Ealignof ty' ty) tmp | tr_valof: forall le dst e1 ty tmp sl1 a1 tmp1 sl2 a2 tmp2, tr_expr le For_val e1 sl1 a1 tmp1 -> - tr_rvalof (C.typeof e1) a1 sl2 a2 tmp2 -> + tr_rvalof (Csyntax.typeof e1) a1 sl2 a2 tmp2 -> list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp -> - tr_expr le dst (C.Evalof e1 ty) + tr_expr le dst (Csyntax.Evalof e1 ty) (sl1 ++ sl2 ++ final dst a2) a2 tmp | tr_addrof: forall le dst e1 ty tmp sl1 a1, tr_expr le For_val e1 sl1 a1 tmp -> - tr_expr le dst (C.Eaddrof e1 ty) + tr_expr le dst (Csyntax.Eaddrof e1 ty) (sl1 ++ final dst (Eaddrof a1 ty)) (Eaddrof a1 ty) tmp | tr_unop: forall le dst op e1 ty tmp sl1 a1, tr_expr le For_val e1 sl1 a1 tmp -> - tr_expr le dst (C.Eunop op e1 ty) + tr_expr le dst (Csyntax.Eunop op e1 ty) (sl1 ++ final dst (Eunop op a1 ty)) (Eunop op a1 ty) tmp | tr_binop: forall le dst op e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 tmp, tr_expr le For_val e1 sl1 a1 tmp1 -> tr_expr le For_val e2 sl2 a2 tmp2 -> list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp -> - tr_expr le dst (C.Ebinop op e1 e2 ty) + tr_expr le dst (Csyntax.Ebinop op e1 e2 ty) (sl1 ++ sl2 ++ final dst (Ebinop op a1 a2 ty)) (Ebinop op a1 a2 ty) tmp | tr_cast: forall le dst e1 ty sl1 a1 tmp, tr_expr le For_val e1 sl1 a1 tmp -> - tr_expr le dst (C.Ecast e1 ty) + tr_expr le dst (Csyntax.Ecast e1 ty) (sl1 ++ final dst (Ecast a1 ty)) (Ecast a1 ty) tmp | tr_seqand_val: forall le e1 e2 ty sl1 a1 tmp1 t sl2 a2 tmp2 tmp, @@ -127,7 +127,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - tr_expr le (For_set (type_bool :: ty :: nil) t) e2 sl2 a2 tmp2 -> list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp -> In t tmp -> - tr_expr le For_val (C.Eseqand e1 e2 ty) + tr_expr le For_val (Csyntax.Eseqand e1 e2 ty) (sl1 ++ makeif a1 (makeseq sl2) (Sset t (Econst_int Int.zero ty)) :: nil) (Etempvar t ty) tmp @@ -136,7 +136,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - tr_expr le For_effects e2 sl2 a2 tmp2 -> list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp -> - tr_expr le For_effects (C.Eseqand e1 e2 ty) + tr_expr le For_effects (Csyntax.Eseqand e1 e2 ty) (sl1 ++ makeif a1 (makeseq sl2) Sskip :: nil) any tmp | tr_seqand_set: forall le tyl t e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 any tmp, @@ -144,7 +144,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - tr_expr le (For_set (type_bool :: ty :: tyl) t) e2 sl2 a2 tmp2 -> list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp -> In t tmp -> - tr_expr le (For_set tyl t) (C.Eseqand e1 e2 ty) + tr_expr le (For_set tyl t) (Csyntax.Eseqand e1 e2 ty) (sl1 ++ makeif a1 (makeseq sl2) (makeseq (do_set t tyl (Econst_int Int.zero ty))) :: nil) any tmp @@ -153,7 +153,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - tr_expr le (For_set (type_bool :: ty :: nil) t) e2 sl2 a2 tmp2 -> list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp -> In t tmp -> - tr_expr le For_val (C.Eseqor e1 e2 ty) + tr_expr le For_val (Csyntax.Eseqor e1 e2 ty) (sl1 ++ makeif a1 (Sset t (Econst_int Int.one ty)) (makeseq sl2) :: nil) (Etempvar t ty) tmp @@ -162,7 +162,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - tr_expr le For_effects e2 sl2 a2 tmp2 -> list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp -> - tr_expr le For_effects (C.Eseqor e1 e2 ty) + tr_expr le For_effects (Csyntax.Eseqor e1 e2 ty) (sl1 ++ makeif a1 Sskip (makeseq sl2) :: nil) any tmp | tr_seqor_set: forall le tyl t e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 any tmp, @@ -170,7 +170,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - tr_expr le (For_set (type_bool :: ty :: tyl) t) e2 sl2 a2 tmp2 -> list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp -> In t tmp -> - tr_expr le (For_set tyl t) (C.Eseqor e1 e2 ty) + tr_expr le (For_set tyl t) (Csyntax.Eseqor e1 e2 ty) (sl1 ++ makeif a1 (makeseq (do_set t tyl (Econst_int Int.one ty))) (makeseq sl2) :: nil) any tmp @@ -181,7 +181,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - list_disjoint tmp1 tmp2 -> list_disjoint tmp1 tmp3 -> incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp -> In t tmp -> - tr_expr le For_val (C.Econdition e1 e2 e3 ty) + tr_expr le For_val (Csyntax.Econdition e1 e2 e3 ty) (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil) (Etempvar t ty) tmp | tr_condition_effects: forall le e1 e2 e3 ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 any tmp, @@ -191,7 +191,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - list_disjoint tmp1 tmp2 -> list_disjoint tmp1 tmp3 -> incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp -> - tr_expr le For_effects (C.Econdition e1 e2 e3 ty) + tr_expr le For_effects (Csyntax.Econdition e1 e2 e3 ty) (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil) any tmp | tr_condition_set: forall le tyl t e1 e2 e3 ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 any tmp, @@ -201,7 +201,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - list_disjoint tmp1 tmp2 -> list_disjoint tmp1 tmp3 -> incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp -> In t tmp -> - tr_expr le (For_set tyl t) (C.Econdition e1 e2 e3 ty) + tr_expr le (For_set tyl t) (Csyntax.Econdition e1 e2 e3 ty) (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil) any tmp | tr_assign_effects: forall le e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 any tmp, @@ -209,7 +209,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - tr_expr le For_val e2 sl2 a2 tmp2 -> list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp -> - tr_expr le For_effects (C.Eassign e1 e2 ty) + tr_expr le For_effects (Csyntax.Eassign e1 e2 ty) (sl1 ++ sl2 ++ make_assign a1 a2 :: nil) any tmp | tr_assign_val: forall le dst e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 t tmp ty1 ty2, @@ -218,9 +218,9 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - incl tmp1 tmp -> incl tmp2 tmp -> list_disjoint tmp1 tmp2 -> In t tmp -> ~In t tmp1 -> ~In t tmp2 -> - ty1 = C.typeof e1 -> - ty2 = C.typeof e2 -> - tr_expr le dst (C.Eassign e1 e2 ty) + ty1 = Csyntax.typeof e1 -> + ty2 = Csyntax.typeof e2 -> + tr_expr le dst (Csyntax.Eassign e1 e2 ty) (sl1 ++ sl2 ++ Sset t a2 :: make_assign a1 (Etempvar t ty2) :: @@ -229,11 +229,11 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - | tr_assignop_effects: forall le op e1 e2 tyres ty ty1 sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 any tmp, tr_expr le For_val e1 sl1 a1 tmp1 -> tr_expr le For_val e2 sl2 a2 tmp2 -> - ty1 = C.typeof e1 -> + ty1 = Csyntax.typeof e1 -> tr_rvalof ty1 a1 sl3 a3 tmp3 -> list_disjoint tmp1 tmp2 -> list_disjoint tmp1 tmp3 -> list_disjoint tmp2 tmp3 -> incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp -> - tr_expr le For_effects (C.Eassignop op e1 e2 tyres ty) + tr_expr le For_effects (Csyntax.Eassignop op e1 e2 tyres ty) (sl1 ++ sl2 ++ sl3 ++ make_assign a1 (Ebinop op a3 a2 tyres) :: nil) any tmp | tr_assignop_val: forall le dst op e1 e2 tyres ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 t tmp ty1, @@ -243,8 +243,8 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - list_disjoint tmp1 tmp2 -> list_disjoint tmp1 tmp3 -> list_disjoint tmp2 tmp3 -> incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp -> In t tmp -> ~In t tmp1 -> ~In t tmp2 -> ~In t tmp3 -> - ty1 = C.typeof e1 -> - tr_expr le dst (C.Eassignop op e1 e2 tyres ty) + ty1 = Csyntax.typeof e1 -> + tr_expr le dst (Csyntax.Eassignop op e1 e2 tyres ty) (sl1 ++ sl2 ++ sl3 ++ Sset t (Ebinop op a3 a2 tyres) :: make_assign a1 (Etempvar t tyres) :: @@ -253,17 +253,17 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - | tr_postincr_effects: forall le id e1 ty ty1 sl1 a1 tmp1 sl2 a2 tmp2 any tmp, tr_expr le For_val e1 sl1 a1 tmp1 -> tr_rvalof ty1 a1 sl2 a2 tmp2 -> - ty1 = C.typeof e1 -> + ty1 = Csyntax.typeof e1 -> incl tmp1 tmp -> incl tmp2 tmp -> list_disjoint tmp1 tmp2 -> - tr_expr le For_effects (C.Epostincr id e1 ty) + tr_expr le For_effects (Csyntax.Epostincr id e1 ty) (sl1 ++ sl2 ++ make_assign a1 (transl_incrdecr id a2 ty1) :: nil) any tmp | tr_postincr_val: forall le dst id e1 ty sl1 a1 tmp1 t ty1 tmp, tr_expr le For_val e1 sl1 a1 tmp1 -> incl tmp1 tmp -> In t tmp -> ~In t tmp1 -> - ty1 = C.typeof e1 -> - tr_expr le dst (C.Epostincr id e1 ty) + ty1 = Csyntax.typeof e1 -> + tr_expr le dst (Csyntax.Epostincr id e1 ty) (sl1 ++ make_set t a1 :: make_assign a1 (transl_incrdecr id (Etempvar t ty1) ty1) :: final dst (Etempvar t ty1)) @@ -273,13 +273,13 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - tr_expr le dst e2 sl2 a2 tmp2 -> list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp -> - tr_expr le dst (C.Ecomma e1 e2 ty) (sl1 ++ sl2) a2 tmp + tr_expr le dst (Csyntax.Ecomma e1 e2 ty) (sl1 ++ sl2) a2 tmp | tr_call_effects: forall le e1 el2 ty sl1 a1 tmp1 sl2 al2 tmp2 any tmp, tr_expr le For_val e1 sl1 a1 tmp1 -> tr_exprlist le el2 sl2 al2 tmp2 -> list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp -> - tr_expr le For_effects (C.Ecall e1 el2 ty) + tr_expr le For_effects (Csyntax.Ecall e1 el2 ty) (sl1 ++ sl2 ++ Scall None a1 al2 :: nil) any tmp | tr_call_val: forall le dst e1 el2 ty sl1 a1 tmp1 sl2 al2 tmp2 t tmp, @@ -288,45 +288,45 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - tr_exprlist le el2 sl2 al2 tmp2 -> list_disjoint tmp1 tmp2 -> In t tmp -> incl tmp1 tmp -> incl tmp2 tmp -> - tr_expr le dst (C.Ecall e1 el2 ty) + tr_expr le dst (Csyntax.Ecall e1 el2 ty) (sl1 ++ sl2 ++ Scall (Some t) a1 al2 :: final dst (Etempvar t ty)) (Etempvar t ty) tmp | tr_builtin_effects: forall le ef tyargs el ty sl al tmp1 any tmp, tr_exprlist le el sl al tmp1 -> incl tmp1 tmp -> - tr_expr le For_effects (C.Ebuiltin ef tyargs el ty) + tr_expr le For_effects (Csyntax.Ebuiltin ef tyargs el ty) (sl ++ Sbuiltin None ef tyargs al :: nil) any tmp | tr_builtin_val: forall le dst ef tyargs el ty sl al tmp1 t tmp, dst <> For_effects -> tr_exprlist le el sl al tmp1 -> In t tmp -> incl tmp1 tmp -> - tr_expr le dst (C.Ebuiltin ef tyargs el ty) + tr_expr le dst (Csyntax.Ebuiltin ef tyargs el ty) (sl ++ Sbuiltin (Some t) ef tyargs al :: final dst (Etempvar t ty)) (Etempvar t ty) tmp | tr_paren_val: forall le e1 ty sl1 a1 t tmp, tr_expr le (For_set (ty :: nil) t) e1 sl1 a1 tmp -> In t tmp -> - tr_expr le For_val (C.Eparen e1 ty) + tr_expr le For_val (Csyntax.Eparen e1 ty) sl1 (Etempvar t ty) tmp | tr_paren_effects: forall le e1 ty sl1 a1 tmp any, tr_expr le For_effects e1 sl1 a1 tmp -> - tr_expr le For_effects (C.Eparen e1 ty) sl1 any tmp + tr_expr le For_effects (Csyntax.Eparen e1 ty) sl1 any tmp | tr_paren_set: forall le tyl t e1 ty sl1 a1 tmp any, tr_expr le (For_set (ty::tyl) t) e1 sl1 a1 tmp -> In t tmp -> - tr_expr le (For_set tyl t) (C.Eparen e1 ty) sl1 any tmp + tr_expr le (For_set tyl t) (Csyntax.Eparen e1 ty) sl1 any tmp -with tr_exprlist: temp_env -> C.exprlist -> list statement -> list expr -> list ident -> Prop := +with tr_exprlist: temp_env -> Csyntax.exprlist -> list statement -> list expr -> list ident -> Prop := | tr_nil: forall le tmp, - tr_exprlist le C.Enil nil nil tmp + tr_exprlist le Csyntax.Enil nil nil tmp | tr_cons: forall le e1 el2 sl1 a1 tmp1 sl2 al2 tmp2 tmp, tr_expr le For_val e1 sl1 a1 tmp1 -> tr_exprlist le el2 sl2 al2 tmp2 -> list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp -> - tr_exprlist le (C.Econs e1 el2) (sl1 ++ sl2) (a1 :: al2) tmp. + tr_exprlist le (Csyntax.Econs e1 el2) (sl1 ++ sl2) (a1 :: al2) tmp. Scheme tr_expr_ind2 := Minimality for tr_expr Sort Prop with tr_exprlist_ind2 := Minimality for tr_exprlist Sort Prop. @@ -372,11 +372,11 @@ Qed. (** The "top-level" translation is equivalent to [tr_expr] above for source terms. It brings additional flexibility in the matching - between C values and Cminor expressions: in the case of + between Csyntax values and Cminor expressions: in the case of [tr_expr], the Cminor expression must not depend on memory, while in the case of [tr_top] it can depend on the current memory state. This special case is extended to values occurring under - one or several [C.Eparen]. *) + one or several [Csyntax.Eparen]. *) Section TR_TOP. @@ -385,14 +385,14 @@ Variable e: env. Variable le: temp_env. Variable m: mem. -Inductive tr_top: destination -> C.expr -> list statement -> expr -> list ident -> Prop := +Inductive tr_top: destination -> Csyntax.expr -> list statement -> expr -> list ident -> Prop := | tr_top_val_val: forall v ty a tmp, typeof a = ty -> eval_expr ge e le m a v -> - tr_top For_val (C.Eval v ty) nil a tmp + tr_top For_val (Csyntax.Eval v ty) nil a tmp (* | tr_top_val_set: forall t tyl v ty a any tmp, typeof a = ty -> eval_expr ge e le m a v -> - tr_top (For_set tyl t) (C.Eval v ty) (Sset t (fold_left Ecast tyl a) :: nil) any tmp + tr_top (For_set tyl t) (Csyntax.Eval v ty) (Sset t (fold_left Ecast tyl a) :: nil) any tmp *) | tr_top_base: forall dst r sl a tmp, tr_expr le dst r sl a tmp -> @@ -400,92 +400,92 @@ Inductive tr_top: destination -> C.expr -> list statement -> expr -> list ident (* | tr_top_paren_test: forall tyl t r ty sl a tmp, tr_top (For_set (ty :: tyl) t) r sl a tmp -> - tr_top (For_set tyl t) (C.Eparen r ty) sl a tmp. + tr_top (For_set tyl t) (Csyntax.Eparen r ty) sl a tmp. *) End TR_TOP. (** ** Translation of statements *) -Inductive tr_expression: C.expr -> statement -> expr -> Prop := +Inductive tr_expression: Csyntax.expr -> statement -> expr -> Prop := | tr_expression_intro: forall r sl a tmps, (forall ge e le m, tr_top ge e le m For_val r sl a tmps) -> tr_expression r (makeseq sl) a. -Inductive tr_expr_stmt: C.expr -> statement -> Prop := +Inductive tr_expr_stmt: Csyntax.expr -> statement -> Prop := | tr_expr_stmt_intro: forall r sl a tmps, (forall ge e le m, tr_top ge e le m For_effects r sl a tmps) -> tr_expr_stmt r (makeseq sl). -Inductive tr_if: C.expr -> statement -> statement -> statement -> Prop := +Inductive tr_if: Csyntax.expr -> statement -> statement -> statement -> Prop := | tr_if_intro: forall r s1 s2 sl a tmps, (forall ge e le m, tr_top ge e le m For_val r sl a tmps) -> tr_if r s1 s2 (makeseq (sl ++ makeif a s1 s2 :: nil)). -Inductive tr_stmt: C.statement -> statement -> Prop := +Inductive tr_stmt: Csyntax.statement -> statement -> Prop := | tr_skip: - tr_stmt C.Sskip Sskip + tr_stmt Csyntax.Sskip Sskip | tr_do: forall r s, tr_expr_stmt r s -> - tr_stmt (C.Sdo r) s + tr_stmt (Csyntax.Sdo r) s | tr_seq: forall s1 s2 ts1 ts2, tr_stmt s1 ts1 -> tr_stmt s2 ts2 -> - tr_stmt (C.Ssequence s1 s2) (Ssequence ts1 ts2) + tr_stmt (Csyntax.Ssequence s1 s2) (Ssequence ts1 ts2) | tr_ifthenelse: forall r s1 s2 s' a ts1 ts2, tr_expression r s' a -> tr_stmt s1 ts1 -> tr_stmt s2 ts2 -> - tr_stmt (C.Sifthenelse r s1 s2) (Ssequence s' (Sifthenelse a ts1 ts2)) + tr_stmt (Csyntax.Sifthenelse r s1 s2) (Ssequence s' (Sifthenelse a ts1 ts2)) | tr_while: forall r s1 s' ts1, tr_if r Sskip Sbreak s' -> tr_stmt s1 ts1 -> - tr_stmt (C.Swhile r s1) + tr_stmt (Csyntax.Swhile r s1) (Sloop (Ssequence s' ts1) Sskip) | tr_dowhile: forall r s1 s' ts1, tr_if r Sskip Sbreak s' -> tr_stmt s1 ts1 -> - tr_stmt (C.Sdowhile r s1) + tr_stmt (Csyntax.Sdowhile r s1) (Sloop ts1 s') | tr_for_1: forall r s3 s4 s' ts3 ts4, tr_if r Sskip Sbreak s' -> tr_stmt s3 ts3 -> tr_stmt s4 ts4 -> - tr_stmt (C.Sfor C.Sskip r s3 s4) + tr_stmt (Csyntax.Sfor Csyntax.Sskip r s3 s4) (Sloop (Ssequence s' ts4) ts3) | tr_for_2: forall s1 r s3 s4 s' ts1 ts3 ts4, tr_if r Sskip Sbreak s' -> - s1 <> C.Sskip -> + s1 <> Csyntax.Sskip -> tr_stmt s1 ts1 -> tr_stmt s3 ts3 -> tr_stmt s4 ts4 -> - tr_stmt (C.Sfor s1 r s3 s4) + tr_stmt (Csyntax.Sfor s1 r s3 s4) (Ssequence ts1 (Sloop (Ssequence s' ts4) ts3)) | tr_break: - tr_stmt C.Sbreak Sbreak + tr_stmt Csyntax.Sbreak Sbreak | tr_continue: - tr_stmt C.Scontinue Scontinue + tr_stmt Csyntax.Scontinue Scontinue | tr_return_none: - tr_stmt (C.Sreturn None) (Sreturn None) + tr_stmt (Csyntax.Sreturn None) (Sreturn None) | tr_return_some: forall r s' a, tr_expression r s' a -> - tr_stmt (C.Sreturn (Some r)) (Ssequence s' (Sreturn (Some a))) + tr_stmt (Csyntax.Sreturn (Some r)) (Ssequence s' (Sreturn (Some a))) | tr_switch: forall r ls s' a tls, tr_expression r s' a -> tr_lblstmts ls tls -> - tr_stmt (C.Sswitch r ls) (Ssequence s' (Sswitch a tls)) + tr_stmt (Csyntax.Sswitch r ls) (Ssequence s' (Sswitch a tls)) | tr_label: forall lbl s ts, tr_stmt s ts -> - tr_stmt (C.Slabel lbl s) (Slabel lbl ts) + tr_stmt (Csyntax.Slabel lbl s) (Slabel lbl ts) | tr_goto: forall lbl, - tr_stmt (C.Sgoto lbl) (Sgoto lbl) + tr_stmt (Csyntax.Sgoto lbl) (Sgoto lbl) -with tr_lblstmts: C.labeled_statements -> labeled_statements -> Prop := +with tr_lblstmts: Csyntax.labeled_statements -> labeled_statements -> Prop := | tr_default: forall s ts, tr_stmt s ts -> - tr_lblstmts (C.LSdefault s) (LSdefault ts) + tr_lblstmts (Csyntax.LSdefault s) (LSdefault ts) | tr_case: forall n s ls ts tls, tr_stmt s ts -> tr_lblstmts ls tls -> - tr_lblstmts (C.LScase n s ls) (LScase n ts tls). + tr_lblstmts (Csyntax.LScase n s ls) (LScase n ts tls). (** * Correctness proof with respect to the specification. *) @@ -504,7 +504,7 @@ Proof. Qed. Remark bind2_inversion: - forall (A B C: Type) (f: mon (A*B)) (g: A -> B -> mon C) (y: C) (z1 z3: generator) I, + forall (A B Csyntax: Type) (f: mon (A*B)) (g: A -> B -> mon Csyntax) (y: Csyntax) (z1 z3: generator) I, bind2 f g z1 = Res y z3 I -> exists x1, exists x2, exists z2, exists I1, exists I2, f z1 = Res (x1,x2) z2 I1 /\ g x1 x2 z2 = Res y z3 I2. @@ -632,7 +632,7 @@ Lemma contained_disjoint: contained l1 g1 g2 -> contained l2 g2 g3 -> list_disjoint l1 l2. Proof. intros; red; intros. red; intro; subst y. - exploit H; eauto. intros [A B]. exploit H0; eauto. intros [C D]. + exploit H; eauto. intros [A B]. exploit H0; eauto. intros [Csyntax D]. elim (Plt_strict x). apply Plt_Ple_trans with (gen_next g2); auto. Qed. @@ -640,7 +640,7 @@ Lemma contained_notin: forall g1 l g2 id g3, contained l g1 g2 -> within id g2 g3 -> ~In id l. Proof. - intros; red; intros. exploit H; eauto. intros [C D]. destruct H0 as [A B]. + intros; red; intros. exploit H; eauto. intros [Csyntax D]. destruct H0 as [A B]. elim (Plt_strict id). apply Plt_Ple_trans with (gen_next g2); auto. Qed. @@ -737,13 +737,13 @@ Lemma transl_valof_meets_spec: exists tmps, tr_rvalof ty a sl b tmps /\ contained tmps g g'. Proof. unfold transl_valof; intros. - destruct (type_is_volatile ty) as []_eqn; monadInv H. + destruct (type_is_volatile ty) eqn:?; monadInv H. exists (x :: nil); split; eauto with gensym. econstructor; eauto with coqlib. exists (@nil ident); split; eauto with gensym. constructor; auto. Qed. -Scheme expr_ind2 := Induction for C.expr Sort Prop - with exprlist_ind2 := Induction for C.exprlist Sort Prop. +Scheme expr_ind2 := Induction for Csyntax.expr Sort Prop + with exprlist_ind2 := Induction for Csyntax.exprlist Sort Prop. Combined Scheme expr_exprlist_ind from expr_ind2, exprlist_ind2. Lemma transl_meets_spec: @@ -775,7 +775,7 @@ Opaque makeif. econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto. (* valof *) monadInv H0. exploit H; eauto. intros [tmp1 [A B]]. - exploit transl_valof_meets_spec; eauto. intros [tmp2 [C D]]. UseFinish. + exploit transl_valof_meets_spec; eauto. intros [tmp2 [Csyntax D]]. UseFinish. exists (tmp1 ++ tmp2); split. intros; apply tr_expr_add_dest. econstructor; eauto with gensym. eauto with gensym. @@ -790,7 +790,7 @@ Opaque makeif. econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto. (* binop *) monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. - exploit H0; eauto. intros [tmp2 [C D]]. UseFinish. + exploit H0; eauto. intros [tmp2 [Csyntax D]]. UseFinish. exists (tmp1 ++ tmp2); split. intros; apply tr_expr_add_dest. econstructor; eauto with gensym. eauto with gensym. @@ -801,7 +801,7 @@ Opaque makeif. monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. destruct dst; monadInv EQ0. (* for value *) - exploit H0; eauto with gensym. intros [tmp2 [C D]]. + exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]]. simpl add_dest in *. exists (x0 :: tmp1 ++ tmp2); split. intros; eapply tr_seqand_val; eauto with gensym. @@ -809,13 +809,13 @@ Opaque makeif. apply contained_cons. eauto with gensym. apply contained_app; eauto with gensym. (* for effects *) - exploit H0; eauto with gensym. intros [tmp2 [C D]]. + exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]]. simpl add_dest in *. exists (tmp1 ++ tmp2); split. intros; eapply tr_seqand_effects; eauto with gensym. apply contained_app; eauto with gensym. (* for set *) - exploit H0; eauto with gensym. intros [tmp2 [C D]]. + exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]]. simpl add_dest in *. exists (tmp1 ++ tmp2); split. intros; eapply tr_seqand_set; eauto with gensym. @@ -825,7 +825,7 @@ Opaque makeif. monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. destruct dst; monadInv EQ0. (* for value *) - exploit H0; eauto with gensym. intros [tmp2 [C D]]. + exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]]. simpl add_dest in *. exists (x0 :: tmp1 ++ tmp2); split. intros; eapply tr_seqor_val; eauto with gensym. @@ -833,13 +833,13 @@ Opaque makeif. apply contained_cons. eauto with gensym. apply contained_app; eauto with gensym. (* for effects *) - exploit H0; eauto with gensym. intros [tmp2 [C D]]. + exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]]. simpl add_dest in *. exists (tmp1 ++ tmp2); split. intros; eapply tr_seqor_effects; eauto with gensym. apply contained_app; eauto with gensym. (* for set *) - exploit H0; eauto with gensym. intros [tmp2 [C D]]. + exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]]. simpl add_dest in *. exists (tmp1 ++ tmp2); split. intros; eapply tr_seqor_set; eauto with gensym. @@ -849,7 +849,7 @@ Opaque makeif. monadInv H2. exploit H; eauto. intros [tmp1 [A B]]. destruct dst; monadInv EQ0. (* for value *) - exploit H0; eauto with gensym. intros [tmp2 [C D]]. + exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]]. exploit H1; eauto with gensym. intros [tmp3 [E F]]. simpl add_dest in *. exists (x0 :: tmp1 ++ tmp2 ++ tmp3); split. @@ -860,14 +860,14 @@ Opaque makeif. apply contained_app. eauto with gensym. apply contained_app; eauto with gensym. (* for effects *) - exploit H0; eauto. intros [tmp2 [C D]]. + exploit H0; eauto. intros [tmp2 [Csyntax D]]. exploit H1; eauto. intros [tmp3 [E F]]. simpl add_dest in *. exists (tmp1 ++ tmp2 ++ tmp3); split. intros; eapply tr_condition_effects; eauto with gensym. apply contained_app; eauto with gensym. (* for test *) - exploit H0; eauto with gensym. intros [tmp2 [C D]]. + exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]]. exploit H1; eauto with gensym. intros [tmp3 [E F]]. simpl add_dest in *. exists (tmp1 ++ tmp2 ++ tmp3); split. @@ -883,7 +883,7 @@ Opaque makeif. exists (@nil ident); split; auto with gensym. constructor. (* assign *) monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. - exploit H0; eauto. intros [tmp2 [C D]]. + exploit H0; eauto. intros [tmp2 [Csyntax D]]. destruct dst; monadInv EQ2; simpl add_dest in *. (* for value *) exists (x1 :: tmp1 ++ tmp2); split. @@ -902,7 +902,7 @@ Opaque makeif. apply contained_app; eauto with gensym. (* assignop *) monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. - exploit H0; eauto. intros [tmp2 [C D]]. + exploit H0; eauto. intros [tmp2 [Csyntax D]]. exploit transl_valof_meets_spec; eauto. intros [tmp3 [E F]]. destruct dst; monadInv EQ3; simpl add_dest in *. (* for value *) @@ -928,7 +928,7 @@ Opaque makeif. econstructor; eauto with gensym. apply contained_cons; eauto with gensym. (* for effects *) - exploit transl_valof_meets_spec; eauto. intros [tmp2 [C D]]. + exploit transl_valof_meets_spec; eauto. intros [tmp2 [Csyntax D]]. exists (tmp1 ++ tmp2); split. econstructor; eauto with gensym. eauto with gensym. @@ -939,7 +939,7 @@ Opaque makeif. apply contained_cons; eauto with gensym. (* comma *) monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. - exploit H0; eauto with gensym. intros [tmp2 [C D]]. + exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]]. exists (tmp1 ++ tmp2); split. econstructor; eauto with gensym. destruct dst; simpl; eauto with gensym. @@ -949,7 +949,7 @@ Opaque makeif. apply contained_app; eauto with gensym. (* call *) monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. - exploit H0; eauto. intros [tmp2 [C D]]. + exploit H0; eauto. intros [tmp2 [Csyntax D]]. destruct dst; monadInv EQ2; simpl add_dest in *. (* for value *) exists (x1 :: tmp1 ++ tmp2); split. @@ -988,7 +988,7 @@ Opaque makeif. monadInv H; exists (@nil ident); split; auto with gensym. constructor. (* cons *) monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. - exploit H0; eauto. intros [tmp2 [C D]]. + exploit H0; eauto. intros [tmp2 [Csyntax D]]. exists (tmp1 ++ tmp2); split. econstructor; eauto with gensym. eauto with gensym. @@ -1054,13 +1054,13 @@ Qed. Theorem transl_function_spec: forall f tf, transl_function f = OK tf -> - tr_stmt f.(C.fn_body) tf.(fn_body) - /\ fn_return tf = C.fn_return f - /\ fn_params tf = C.fn_params f - /\ fn_vars tf = C.fn_vars f. + tr_stmt f.(Csyntax.fn_body) tf.(fn_body) + /\ fn_return tf = Csyntax.fn_return f + /\ fn_params tf = Csyntax.fn_params f + /\ fn_vars tf = Csyntax.fn_vars f. Proof. intros until tf. unfold transl_function. - case_eq (transl_stmt (C.fn_body f) (initial_generator tt)); intros; inv H0. + case_eq (transl_stmt (Csyntax.fn_body f) (initial_generator tt)); intros; inv H0. simpl. intuition. eapply transl_stmt_meets_spec; eauto. Qed. -- cgit