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/SimplExprproof.v | 112 ++++++++++++++++++++++----------------------- 1 file changed, 56 insertions(+), 56 deletions(-) (limited to 'cfrontend/SimplExprproof.v') diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 59fc9bc7..150ed760 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -33,7 +33,7 @@ Require Import SimplExprspec. Section PRESERVATION. -Variable prog: C.program. +Variable prog: Csyntax.program. Variable tprog: Clight.program. Hypothesis TRANSL: transl_program prog = OK tprog. @@ -76,20 +76,20 @@ Qed. Lemma type_of_fundef_preserved: forall f tf, transl_fundef f = OK tf -> - type_of_fundef tf = C.type_of_fundef f. + type_of_fundef tf = Csyntax.type_of_fundef f. Proof. intros. destruct f; monadInv H. exploit transl_function_spec; eauto. intros [A [B [C D]]]. - simpl. unfold type_of_function, C.type_of_function. congruence. + simpl. unfold type_of_function, Csyntax.type_of_function. congruence. auto. Qed. Lemma function_return_preserved: forall f tf, transl_function f = OK tf -> - fn_return tf = C.fn_return f. + fn_return tf = Csyntax.fn_return f. Proof. intros. unfold transl_function in H. - destruct (transl_stmt (C.fn_body f) (initial_generator tt)); inv H. + destruct (transl_stmt (Csyntax.fn_body f) (initial_generator tt)); inv H. auto. Qed. @@ -190,11 +190,11 @@ Lemma tr_simple: forall le dst sl a tmps, tr_expr le dst r sl a tmps -> match dst with - | For_val => sl = nil /\ C.typeof r = typeof a /\ eval_expr tge e le m a v + | For_val => sl = nil /\ Csyntax.typeof r = typeof a /\ eval_expr tge e le m a v | For_effects => sl = nil | For_set tyl t => exists b, sl = do_set t tyl b - /\ C.typeof r = typeof b + /\ Csyntax.typeof r = typeof b /\ eval_expr tge e le m b v end) /\ @@ -202,7 +202,7 @@ Lemma tr_simple: eval_simple_lvalue ge e m l b ofs -> forall le sl a tmps, tr_expr le For_val l sl a tmps -> - sl = nil /\ C.typeof l = typeof a /\ eval_lvalue tge e le m a b ofs). + sl = nil /\ Csyntax.typeof l = typeof a /\ eval_lvalue tge e le m a b ofs). Proof. Opaque makeif. intros e m. @@ -275,11 +275,11 @@ Lemma tr_simple_rvalue: forall le dst sl a tmps, tr_expr le dst r sl a tmps -> match dst with - | For_val => sl = nil /\ C.typeof r = typeof a /\ eval_expr tge e le m a v + | For_val => sl = nil /\ Csyntax.typeof r = typeof a /\ eval_expr tge e le m a v | For_effects => sl = nil | For_set tyl t => exists b, sl = do_set t tyl b - /\ C.typeof r = typeof b + /\ Csyntax.typeof r = typeof b /\ eval_expr tge e le m b v end. Proof. @@ -291,7 +291,7 @@ Lemma tr_simple_lvalue: eval_simple_lvalue ge e m l b ofs -> forall le sl a tmps, tr_expr le For_val l sl a tmps -> - sl = nil /\ C.typeof l = typeof a /\ eval_lvalue tge e le m a b ofs. + sl = nil /\ Csyntax.typeof l = typeof a /\ eval_lvalue tge e le m a b ofs. Proof. intros e m. exact (proj2 (tr_simple e m)). Qed. @@ -315,8 +315,8 @@ Qed. Lemma typeof_context: forall k1 k2 C, leftcontext k1 k2 C -> - forall e1 e2, C.typeof e1 = C.typeof e2 -> - C.typeof (C e1) = C.typeof (C e2). + forall e1 e2, Csyntax.typeof e1 = Csyntax.typeof e2 -> + Csyntax.typeof (C e1) = Csyntax.typeof (C e2). Proof. induction 1; intros; auto. Qed. @@ -337,7 +337,7 @@ Lemma tr_expr_leftcontext_rec: /\ (forall le' e' sl3, tr_expr le' dst' e' sl3 a' tmp' -> (forall id, ~In id tmp' -> le'!id = le!id) -> - C.typeof e' = C.typeof e -> + Csyntax.typeof e' = Csyntax.typeof e -> tr_expr le' dst (C e') (sl3 ++ sl2) a tmps) ) /\ ( forall from C, leftcontextlist from C -> @@ -350,7 +350,7 @@ Lemma tr_expr_leftcontext_rec: /\ (forall le' e' sl3, tr_expr le' dst' e' sl3 a' tmp' -> (forall id, ~In id tmp' -> le'!id = le!id) -> - C.typeof e' = C.typeof e -> + Csyntax.typeof e' = Csyntax.typeof e -> tr_exprlist le' (C e') (sl3 ++ sl2) a tmps) ). Proof. @@ -695,7 +695,7 @@ Theorem tr_expr_leftcontext: /\ (forall le' r' sl3, tr_expr le' dst' r' sl3 a' tmp' -> (forall id, ~In id tmp' -> le'!id = le!id) -> - C.typeof r' = C.typeof r -> + Csyntax.typeof r' = Csyntax.typeof r -> tr_expr le' dst (C r') (sl3 ++ sl2) a tmps). Proof. intros. eapply (proj1 tr_expr_leftcontext_rec); eauto. @@ -714,7 +714,7 @@ Theorem tr_top_leftcontext: /\ (forall le' m' r' sl3, tr_expr le' dst' r' sl3 a' tmp' -> (forall id, ~In id tmp' -> le'!id = le!id) -> - C.typeof r' = C.typeof r -> + Csyntax.typeof r' = Csyntax.typeof r -> tr_top tge e le' m' dst (C r') (sl3 ++ sl2) a tmps). Proof. induction 1; intros. @@ -895,7 +895,7 @@ Inductive match_cont : Csem.cont -> cont -> Prop := | match_Kcall: forall f e C ty k optid tf le sl tk a dest tmps, transl_function f = Errors.OK tf -> leftcontext RV RV C -> - (forall v m, tr_top tge e (set_opttemp optid v le) m dest (C (C.Eval v ty)) sl a tmps) -> + (forall v m, tr_top tge e (set_opttemp optid v le) m dest (C (Csyntax.Eval v ty)) sl a tmps) -> match_cont_exp dest a k tk -> match_cont (Csem.Kcall f e C ty k) (Kcall optid tf e le (Kseqlist sl tk)) @@ -1220,10 +1220,10 @@ Proof. (* for not skip *) rename s' into sr. rewrite (tr_find_label_if _ _ H3); auto. - exploit (IHs1 (Csem.Kseq (C.Sfor C.Sskip e s2 s3) k)); eauto. + exploit (IHs1 (Csem.Kseq (Csyntax.Sfor Csyntax.Sskip e s2 s3) k)); eauto. econstructor; eauto. econstructor; eauto. destruct (Csem.find_label lbl s1 - (Csem.Kseq (C.Sfor C.Sskip e s2 s3) k)) as [[s' k'] | ]. + (Csem.Kseq (Csyntax.Sfor Csyntax.Sskip e s2 s3) k)) as [[s' k'] | ]. intros [ts' [tk' [A [B C]]]]. rewrite A. exists ts'; exists tk'; intuition. intro EQ; rewrite EQ. exploit (IHs3 (Csem.Kfor3 e s2 s3 k)); eauto. econstructor; eauto. @@ -1265,49 +1265,49 @@ End FIND_LABEL. Sdo a, k ---> a, Kdo k ---> rval v, Kdo k ---> Sskip, k >> but the translation, which is [Sskip], makes no transitions. -- The reduction [C.Ecomma (C.Eval v) r2 --> r2]. -- The reduction [C.Eparen (C.Eval v) --> C.Eval v] in a [For_effects] context. +- The reduction [Ecomma (Eval v) r2 --> r2]. +- The reduction [Eparen (Eval v) --> Eval v] in a [For_effects] context. The following measure decreases for these stuttering steps. *) -Fixpoint esize (a: C.expr) : nat := +Fixpoint esize (a: Csyntax.expr) : nat := match a with - | C.Eloc _ _ _ => 1%nat - | C.Evar _ _ => 1%nat - | C.Ederef r1 _ => S(esize r1) - | C.Efield l1 _ _ => S(esize l1) - | C.Eval _ _ => O - | C.Evalof l1 _ => S(esize l1) - | C.Eaddrof l1 _ => S(esize l1) - | C.Eunop _ r1 _ => S(esize r1) - | C.Ebinop _ r1 r2 _ => S(esize r1 + esize r2)%nat - | C.Ecast r1 _ => S(esize r1) - | C.Eseqand r1 _ _ => S(esize r1) - | C.Eseqor r1 _ _ => S(esize r1) - | C.Econdition r1 _ _ _ => S(esize r1) - | C.Esizeof _ _ => 1%nat - | C.Ealignof _ _ => 1%nat - | C.Eassign l1 r2 _ => S(esize l1 + esize r2)%nat - | C.Eassignop _ l1 r2 _ _ => S(esize l1 + esize r2)%nat - | C.Epostincr _ l1 _ => S(esize l1) - | C.Ecomma r1 r2 _ => S(esize r1 + esize r2)%nat - | C.Ecall r1 rl2 _ => S(esize r1 + esizelist rl2)%nat - | C.Ebuiltin ef _ rl _ => S(esizelist rl)%nat - | C.Eparen r1 _ => S(esize r1) + | Csyntax.Eloc _ _ _ => 1%nat + | Csyntax.Evar _ _ => 1%nat + | Csyntax.Ederef r1 _ => S(esize r1) + | Csyntax.Efield l1 _ _ => S(esize l1) + | Csyntax.Eval _ _ => O + | Csyntax.Evalof l1 _ => S(esize l1) + | Csyntax.Eaddrof l1 _ => S(esize l1) + | Csyntax.Eunop _ r1 _ => S(esize r1) + | Csyntax.Ebinop _ r1 r2 _ => S(esize r1 + esize r2)%nat + | Csyntax.Ecast r1 _ => S(esize r1) + | Csyntax.Eseqand r1 _ _ => S(esize r1) + | Csyntax.Eseqor r1 _ _ => S(esize r1) + | Csyntax.Econdition r1 _ _ _ => S(esize r1) + | Csyntax.Esizeof _ _ => 1%nat + | Csyntax.Ealignof _ _ => 1%nat + | Csyntax.Eassign l1 r2 _ => S(esize l1 + esize r2)%nat + | Csyntax.Eassignop _ l1 r2 _ _ => S(esize l1 + esize r2)%nat + | Csyntax.Epostincr _ l1 _ => S(esize l1) + | Csyntax.Ecomma r1 r2 _ => S(esize r1 + esize r2)%nat + | Csyntax.Ecall r1 rl2 _ => S(esize r1 + esizelist rl2)%nat + | Csyntax.Ebuiltin ef _ rl _ => S(esizelist rl)%nat + | Csyntax.Eparen r1 _ => S(esize r1) end -with esizelist (el: C.exprlist) : nat := +with esizelist (el: Csyntax.exprlist) : nat := match el with - | C.Enil => O - | C.Econs r1 rl2 => (esize r1 + esizelist rl2)%nat + | Csyntax.Enil => O + | Csyntax.Econs r1 rl2 => (esize r1 + esizelist rl2)%nat end. Definition measure (st: Csem.state) : nat := match st with | Csem.ExprState _ r _ _ _ => (esize r + 1)%nat - | Csem.State _ C.Sskip _ _ _ => 0%nat - | Csem.State _ (C.Sdo r) _ _ _ => (esize r + 2)%nat - | Csem.State _ (C.Sifthenelse r _ _) _ _ _ => (esize r + 2)%nat + | Csem.State _ Csyntax.Sskip _ _ _ => 0%nat + | Csem.State _ (Csyntax.Sdo r) _ _ _ => (esize r + 2)%nat + | Csem.State _ (Csyntax.Sifthenelse r _ _) _ _ _ => (esize r + 2)%nat | _ => 0%nat end. @@ -1338,7 +1338,7 @@ Lemma tr_val_gen: (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 dst (C.Eval v ty) (final dst a) a tmp. + tr_expr le dst (Csyntax.Eval v ty) (final dst a) a tmp. Proof. intros. destruct dst; simpl; econstructor; auto. Qed. @@ -1378,7 +1378,7 @@ Proof. econstructor; split. left. eapply plus_two. constructor. eapply step_make_set; eauto. traceEq. econstructor; eauto. - change (final dst' (Etempvar t0 (C.typeof l)) ++ sl2) with (nil ++ (final dst' (Etempvar t0 (C.typeof l)) ++ sl2)). + change (final dst' (Etempvar t0 (Csyntax.typeof l)) ++ sl2) with (nil ++ (final dst' (Etempvar t0 (Csyntax.typeof l)) ++ sl2)). apply S. apply tr_val_gen. auto. intros. constructor. rewrite H5; auto. apply PTree.gss. intros. apply PTree.gso. red; intros; subst; elim H5; auto. @@ -1784,7 +1784,7 @@ Proof. left. eapply plus_left. constructor. apply star_one. econstructor. econstructor; eauto. rewrite <- TY1; eauto. traceEq. econstructor; eauto. - change sl2 with (final For_val (Etempvar t (C.typeof r)) ++ sl2). apply S. + change sl2 with (final For_val (Etempvar t (Csyntax.typeof r)) ++ sl2). apply S. constructor. auto. intros. constructor. rewrite H2; auto. apply PTree.gss. intros. apply PTree.gso. intuition congruence. auto. @@ -1877,7 +1877,7 @@ Qed. Lemma tr_top_val_for_val_inv: forall e le m v ty sl a tmps, - tr_top tge e le m For_val (C.Eval v ty) sl a tmps -> + tr_top tge e le m For_val (Csyntax.Eval v ty) sl a tmps -> sl = nil /\ typeof a = ty /\ eval_expr tge e le m a v. Proof. intros. inv H. auto. inv H0. auto. @@ -2087,7 +2087,7 @@ Proof. inv H9. exploit tr_top_val_for_val_inv; eauto. intros [A [B C]]. subst. econstructor; split. left. eapply plus_two. constructor. econstructor. eauto. - replace (fn_return tf) with (C.fn_return f). eauto. + replace (fn_return tf) with (Csyntax.fn_return f). eauto. exploit transl_function_spec; eauto. intuition congruence. eauto. traceEq. constructor. apply match_cont_call; auto. -- cgit