From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- cfrontend/Cstrategy.v | 524 +++++++++++++++++++++++++------------------------- 1 file changed, 262 insertions(+), 262 deletions(-) (limited to 'cfrontend/Cstrategy.v') diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index b082ea56..b3cbacca 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -40,7 +40,7 @@ Variable ge: genv. (** We now formalize a particular strategy for reducing expressions which is the one implemented by the CompCert compiler. It evaluates effectful - subexpressions first, in leftmost-innermost order, then finishes + subexpressions first, in leftmost-innermost order, then finishes with the evaluation of the remaining simple expression. *) (** Simple expressions are defined as follows. *) @@ -99,7 +99,7 @@ Inductive eval_simple_lvalue: expr -> block -> int -> Prop := eval_simple_lvalue (Ederef r ty) b ofs | esl_field_struct: forall r f ty b ofs id co a delta, eval_simple_rvalue r (Vptr b ofs) -> - typeof r = Tstruct id a -> + typeof r = Tstruct id a -> ge.(genv_cenv)!id = Some co -> field_offset ge f (co_members co) = OK delta -> eval_simple_lvalue (Efield r f ty) b (Int.add ofs (Int.repr delta)) @@ -402,7 +402,7 @@ Hint Resolve context_compose contextlist_compose. (** * Safe executions. *) -(** A state is safe according to the nondeterministic semantics +(** A state is safe according to the nondeterministic semantics if it cannot get stuck by doing silent transitions only. *) Definition safe (s: Csem.state) : Prop := @@ -413,8 +413,8 @@ Lemma safe_steps: forall s s', safe s -> star Csem.step ge s E0 s' -> safe s'. Proof. - intros; red; intros. - eapply H. eapply star_trans; eauto. + intros; red; intros. + eapply H. eapply star_trans; eauto. Qed. Lemma star_safe: @@ -433,7 +433,7 @@ Proof. intros. eapply star_plus_trans; eauto. apply H1. eapply safe_steps; eauto. auto. Qed. -Require Import Classical. +Require Import Classical. Lemma safe_imm_safe: forall f C a k e m K, @@ -442,10 +442,10 @@ Lemma safe_imm_safe: imm_safe ge e K a m. Proof. intros. destruct (classic (imm_safe ge e K a m)); auto. - destruct (H Stuckstate). + destruct (H Stuckstate). apply star_one. left. econstructor; eauto. - destruct H2 as [r F]. inv F. - destruct H2 as [t [s' S]]. inv S. inv H2. inv H2. + destruct H2 as [r F]. inv F. + destruct H2 as [t [s' S]]. inv S. inv H2. inv H2. Qed. (** Safe expressions are well-formed with respect to l-values and r-values. *) @@ -649,11 +649,11 @@ Proof. destruct (C a); auto; contradiction. destruct (C a); auto; contradiction. destruct e1; auto. intros. elim (H0 a m); auto. - intros. elim (H0 a m); auto. + intros. elim (H0 a m); auto. destruct (C a); auto; contradiction. destruct (C a); auto; contradiction. - red; intros. destruct (C a); auto. - red; intros. destruct e1; auto. elim (H0 a m); auto. + red; intros. destruct (C a); auto. + red; intros. destruct e1; auto. elim (H0 a m); auto. Qed. Lemma imm_safe_inv: @@ -666,7 +666,7 @@ Lemma imm_safe_inv: end. Proof. destruct invert_expr_context as [A B]. - intros. inv H. + intros. inv H. auto. auto. assert (invert_expr_prop (C e0) m). @@ -733,7 +733,7 @@ Ltac FinishL := apply star_one; left; apply step_lred; eauto; simpl; try (econst Steps H2 (fun x => C(Ebinop op (Eval v1 (typeof r1)) x ty)). FinishR. (* cast *) - Steps H0 (fun x => C(Ecast x ty)). FinishR. + Steps H0 (fun x => C(Ecast x ty)). FinishR. (* sizeof *) FinishR. (* alignof *) @@ -741,11 +741,11 @@ Ltac FinishL := apply star_one; left; apply step_lred; eauto; simpl; try (econst (* loc *) apply star_refl. (* var local *) - FinishL. + FinishL. (* var global *) FinishL. apply red_var_global; auto. (* deref *) - Steps H0 (fun x => C(Ederef x ty)). FinishL. + Steps H0 (fun x => C(Ederef x ty)). FinishL. (* field struct *) Steps H0 (fun x => C(Efield x f0 ty)). rewrite H1 in *. FinishL. (* field union *) @@ -796,13 +796,13 @@ Ltac StepL REC C' a := let b := fresh "b" in let ofs := fresh "ofs" in let E := fresh "E" in let S := fresh "SAFE" in exploit (REC LV C'); eauto; intros [b [ofs E]]; - assert (S: safe (ExprState f (C' (Eloc b ofs (typeof a))) k e m)) by + assert (S: safe (ExprState f (C' (Eloc b ofs (typeof a))) k e m)) by (eapply (eval_simple_lvalue_safe C'); eauto); simpl in S. Ltac StepR REC C' a := let v := fresh "v" in let E := fresh "E" in let S := fresh "SAFE" in exploit (REC RV C'); eauto; intros [v E]; - assert (S: safe (ExprState f (C' (Eval v (typeof a))) k e m)) by + assert (S: safe (ExprState f (C' (Eval v (typeof a))) k e m)) by (eapply (eval_simple_rvalue_safe C'); eauto); simpl in S. @@ -857,22 +857,22 @@ Ltac StepR REC C' a := Qed. Lemma simple_can_eval_rval: - forall r C, + forall r C, simple r = true -> context RV RV C -> safe (ExprState f (C r) k e m) -> exists v, eval_simple_rvalue e m r v /\ safe (ExprState f (C (Eval v (typeof r))) k e m). Proof. - intros. exploit (simple_can_eval r RV); eauto. intros [v A]. + intros. exploit (simple_can_eval r RV); eauto. intros [v A]. exists v; split; auto. eapply eval_simple_rvalue_safe; eauto. Qed. Lemma simple_can_eval_lval: - forall l C, + forall l C, simple l = true -> context LV RV C -> safe (ExprState f (C l) k e m) -> exists b, exists ofs, eval_simple_lvalue e m l b ofs /\ safe (ExprState f (C (Eloc b ofs (typeof l))) k e m). Proof. - intros. exploit (simple_can_eval l LV); eauto. intros [b [ofs A]]. + intros. exploit (simple_can_eval l LV); eauto. intros [b [ofs A]]. exists b; exists ofs; split; auto. eapply eval_simple_lvalue_safe; eauto. Qed. @@ -892,7 +892,7 @@ Inductive eval_simple_list': exprlist -> list val -> Prop := Lemma eval_simple_list_implies: forall rl tyl vl, - eval_simple_list e m rl tyl vl -> + eval_simple_list e m rl tyl vl -> exists vl', cast_arguments (rval_list vl' rl) tyl vl /\ eval_simple_list' rl vl'. Proof. induction 1. @@ -908,9 +908,9 @@ Lemma can_eval_simple_list: cast_arguments (rval_list vl rl) tyl vl' -> eval_simple_list e m rl tyl vl'. Proof. - induction 1; simpl; intros. + induction 1; simpl; intros. inv H. constructor. - inv H1. econstructor; eauto. + inv H1. econstructor; eauto. Qed. Fixpoint exprlist_app (rl1 rl2: exprlist) : exprlist := @@ -924,7 +924,7 @@ Lemma exprlist_app_assoc: exprlist_app (exprlist_app rl1 rl2) rl3 = exprlist_app rl1 (exprlist_app rl2 rl3). Proof. - induction rl1; auto. simpl. congruence. + induction rl1; auto. simpl. congruence. Qed. Inductive contextlist' : (exprlist -> expr) -> Prop := @@ -939,9 +939,9 @@ Lemma exprlist_app_context: forall rl1 rl2, contextlist RV (fun x => exprlist_app rl1 (Econs x rl2)). Proof. - induction rl1; simpl; intros. + induction rl1; simpl; intros. apply ctx_list_head. constructor. - apply ctx_list_tail. auto. + apply ctx_list_tail. auto. Qed. Lemma contextlist'_head: @@ -949,14 +949,14 @@ Lemma contextlist'_head: contextlist' C -> context RV RV (fun x => C (Econs x rl)). Proof. - intros. inv H. + intros. inv H. set (C' := fun x => Ecall r1 (exprlist_app rl0 (Econs x rl)) ty). assert (context RV RV C'). constructor. apply exprlist_app_context. - change (context RV RV (fun x => C0 (C' x))). + change (context RV RV (fun x => C0 (C' x))). eapply context_compose; eauto. set (C' := fun x => Ebuiltin ef tyargs (exprlist_app rl0 (Econs x rl)) ty). assert (context RV RV C'). constructor. apply exprlist_app_context. - change (context RV RV (fun x => C0 (C' x))). + change (context RV RV (fun x => C0 (C' x))). eapply context_compose; eauto. Qed. @@ -965,14 +965,14 @@ Lemma contextlist'_tail: contextlist' C -> contextlist' (fun x => C (Econs r1 x)). Proof. - intros. inv H. + intros. inv H. replace (fun x => C0 (Ecall r0 (exprlist_app rl0 (Econs r1 x)) ty)) with (fun x => C0 (Ecall r0 (exprlist_app (exprlist_app rl0 (Econs r1 Enil)) x) ty)). - constructor. auto. + constructor. auto. apply extensionality; intros. f_equal. f_equal. apply exprlist_app_assoc. replace (fun x => C0 (Ebuiltin ef tyargs (exprlist_app rl0 (Econs r1 x)) ty)) with (fun x => C0 (Ebuiltin ef tyargs (exprlist_app (exprlist_app rl0 (Econs r1 Enil)) x) ty)). - constructor. auto. + constructor. auto. apply extensionality; intros. f_equal. f_equal. apply exprlist_app_assoc. Qed. @@ -984,7 +984,7 @@ Lemma eval_simple_list_steps: star Csem.step ge (ExprState f (C rl) k e m) E0 (ExprState f (C (rval_list vl rl)) k e m). Proof. - induction 1; intros. + induction 1; intros. (* nil *) apply star_refl. (* cons *) @@ -1003,7 +1003,7 @@ Lemma simple_list_can_eval: Proof. induction rl; intros. econstructor; constructor. - simpl in H. destruct (andb_prop _ _ H). + simpl in H. destruct (andb_prop _ _ H). exploit (simple_can_eval r1 RV (fun x => C(Econs x rl))); eauto. intros [v1 EV1]. exploit (IHrl (fun x => C(Econs (Eval v1 (typeof r1)) x))); eauto. @@ -1015,7 +1015,7 @@ Qed. Lemma rval_list_all_values: forall vl rl, exprlist_all_values (rval_list vl rl). Proof. - induction vl; simpl; intros. auto. + induction vl; simpl; intros. auto. destruct rl; simpl; auto. Qed. @@ -1105,13 +1105,13 @@ Ltac Base := (* comma *) Kind. Rec H RV C (fun x => Ecomma x r2 ty). Base. (* call *) - Kind. Rec H RV C (fun x => Ecall x rargs ty). + Kind. Rec H RV C (fun x => Ecall x rargs ty). destruct (H0 (fun x => C (Ecall r1 x ty))) as [A | [C' [a' [D [A B]]]]]. eapply contextlist'_call with (C := C) (rl0 := Enil). auto. auto. Base. right; exists (fun x => Ecall r1 (C' x) ty); exists a'. rewrite D; simpl; auto. (* builtin *) - Kind. + Kind. destruct (H (fun x => C (Ebuiltin ef tyargs x ty))) as [A | [C' [a' [D [A B]]]]]. eapply contextlist'_builtin with (C := C) (rl0 := Enil). auto. auto. Base. @@ -1123,7 +1123,7 @@ Ltac Base := eapply contextlist'_head; eauto. auto. destruct (H0 (fun x => C (Econs r1 x))) as [A' | [C' [a' [A' [B D]]]]]. eapply contextlist'_tail; eauto. auto. - rewrite A; rewrite A'; auto. + rewrite A; rewrite A'; auto. right; exists (fun x => Econs r1 (C' x)); exists a'. rewrite A'; eauto. right; exists (fun x => Econs (C' x) rl); exists a'. rewrite A; eauto. Qed. @@ -1145,43 +1145,43 @@ Lemma estep_simulation: forall S t S', estep S t S' -> plus Csem.step ge S t S'. Proof. - intros. inv H. + intros. inv H. (* simple *) exploit eval_simple_rvalue_steps; eauto. simpl; intros STEPS. - exploit star_inv; eauto. intros [[EQ1 EQ2] | A]; eauto. + exploit star_inv; eauto. intros [[EQ1 EQ2] | A]; eauto. inversion EQ1. rewrite <- H2 in H1; contradiction. (* valof volatile *) - eapply plus_right. + eapply plus_right. eapply eval_simple_lvalue_steps with (C := fun x => C(Evalof x (typeof l))); eauto. left. apply step_rred; eauto. econstructor; eauto. auto. (* seqand true *) eapply plus_right. - eapply eval_simple_rvalue_steps with (C := fun x => C(Eseqand x r2 ty)); eauto. + eapply eval_simple_rvalue_steps with (C := fun x => C(Eseqand x r2 ty)); eauto. left. apply step_rred; eauto. apply red_seqand_true; auto. traceEq. (* seqand false *) eapply plus_right. - eapply eval_simple_rvalue_steps with (C := fun x => C(Eseqand x r2 ty)); eauto. + eapply eval_simple_rvalue_steps with (C := fun x => C(Eseqand x r2 ty)); eauto. left. apply step_rred; eauto. apply red_seqand_false; auto. traceEq. (* seqor true *) eapply plus_right. - eapply eval_simple_rvalue_steps with (C := fun x => C(Eseqor x r2 ty)); eauto. + eapply eval_simple_rvalue_steps with (C := fun x => C(Eseqor x r2 ty)); eauto. left. apply step_rred; eauto. apply red_seqor_true; auto. traceEq. (* seqor false *) eapply plus_right. - eapply eval_simple_rvalue_steps with (C := fun x => C(Eseqor x r2 ty)); eauto. + eapply eval_simple_rvalue_steps with (C := fun x => C(Eseqor x r2 ty)); eauto. left. apply step_rred; eauto. apply red_seqor_false; auto. traceEq. (* condition *) eapply plus_right. eapply eval_simple_rvalue_steps with (C := fun x => C(Econdition x r2 r3 ty)); eauto. - left; apply step_rred; eauto. constructor; auto. auto. + left; apply step_rred; eauto. constructor; auto. auto. (* assign *) eapply star_plus_trans. eapply eval_simple_lvalue_steps with (C := fun x => C(Eassign x r (typeof l))); eauto. eapply plus_right. eapply eval_simple_rvalue_steps with (C := fun x => C(Eassign (Eloc b ofs (typeof l)) x (typeof l))); eauto. left; apply step_rred; eauto. econstructor; eauto. - reflexivity. auto. -(* assignop *) + reflexivity. auto. +(* assignop *) eapply star_plus_trans. eapply eval_simple_lvalue_steps with (C := fun x => C(Eassignop op x r tyres (typeof l))); eauto. eapply star_plus_trans. @@ -1189,9 +1189,9 @@ Proof. eapply plus_left. left; apply step_rred; auto. econstructor; eauto. eapply star_left. - left; apply step_rred with (C := fun x => C(Eassign (Eloc b ofs (typeof l)) x (typeof l))); eauto. econstructor; eauto. - apply star_one. - left; apply step_rred; auto. econstructor; eauto. + left; apply step_rred with (C := fun x => C(Eassign (Eloc b ofs (typeof l)) x (typeof l))); eauto. econstructor; eauto. + apply star_one. + left; apply step_rred; auto. econstructor; eauto. reflexivity. reflexivity. reflexivity. traceEq. (* assignop stuck *) eapply star_plus_trans. @@ -1202,8 +1202,8 @@ Proof. left; apply step_rred; auto. econstructor; eauto. destruct (sem_binary_operation ge op v1 (typeof l) v2 (typeof r) m) as [v3|] eqn:?. eapply star_left. - left; apply step_rred with (C := fun x => C(Eassign (Eloc b ofs (typeof l)) x (typeof l))); eauto. econstructor; eauto. - apply star_one. + left; apply step_rred with (C := fun x => C(Eassign (Eloc b ofs (typeof l)) x (typeof l))); eauto. econstructor; eauto. + apply star_one. left; eapply step_stuck; eauto. red; intros. exploit imm_safe_inv; eauto. simpl. intros [v4' [m' [t' [A [B D]]]]]. rewrite B in H4. eelim H4; eauto. @@ -1220,12 +1220,12 @@ Proof. left; apply step_rred; auto. econstructor; eauto. eapply star_left. left; apply step_rred with (C := fun x => C (Ecomma (Eassign (Eloc b ofs (typeof l)) x (typeof l)) (Eval v1 (typeof l)) (typeof l))); eauto. - econstructor. instantiate (1 := v2). destruct id; assumption. + econstructor. instantiate (1 := v2). destruct id; assumption. eapply star_left. left; apply step_rred with (C := fun x => C (Ecomma x (Eval v1 (typeof l)) (typeof l))); eauto. econstructor; eauto. apply star_one. - left; apply step_rred; auto. econstructor; eauto. + left; apply step_rred; auto. econstructor; eauto. reflexivity. reflexivity. reflexivity. traceEq. (* postincr stuck *) eapply star_plus_trans. @@ -1248,7 +1248,7 @@ Proof. apply star_one. left; eapply step_stuck with (C := fun x => C (Ecomma (Eassign (Eloc b ofs (typeof l)) x (typeof l)) (Eval v1 (typeof l)) (typeof l))); eauto. red; intros. exploit imm_safe_inv; eauto. simpl. intros [v2 A]. congruence. - reflexivity. + reflexivity. traceEq. (* comma *) eapply plus_right. @@ -1260,7 +1260,7 @@ Proof. left; apply step_rred; eauto. econstructor; eauto. auto. (* call *) exploit eval_simple_list_implies; eauto. intros [vl' [A B]]. - eapply star_plus_trans. + eapply star_plus_trans. eapply eval_simple_rvalue_steps with (C := fun x => C(Ecall x rargs ty)); eauto. eapply plus_right. eapply eval_simple_list_steps with (C := fun x => C(Ecall (Eval vf (typeof rf)) x ty)); eauto. @@ -1273,7 +1273,7 @@ Proof. eapply eval_simple_list_steps with (C := fun x => C(Ebuiltin ef tyargs x ty)); eauto. eapply contextlist'_builtin with (rl0 := Enil); auto. left; apply Csem.step_rred; eauto. econstructor; eauto. - traceEq. + traceEq. Qed. Lemma can_estep: @@ -1285,34 +1285,34 @@ Proof. intros. destruct (decompose_topexpr f k e m a H) as [A | [C [b [P [Q R]]]]]. (* simple expr *) exploit (simple_can_eval f k e m a RV (fun x => x)); auto. intros [v P]. - econstructor; econstructor; eapply step_expr; eauto. + econstructor; econstructor; eapply step_expr; eauto. (* side effect *) - clear H0. subst a. red in Q. destruct b; try contradiction. + clear H0. subst a. red in Q. destruct b; try contradiction. (* valof volatile *) destruct Q. exploit (simple_can_eval_lval f k e m b (fun x => C(Evalof x ty))); eauto. intros [b1 [ofs [E1 S1]]]. exploit safe_inv. eexact S1. eauto. simpl. intros [A [t [v B]]]. - econstructor; econstructor; eapply step_rvalof_volatile; eauto. congruence. + econstructor; econstructor; eapply step_rvalof_volatile; eauto. congruence. (* seqand *) exploit (simple_can_eval_rval f k e m b1 (fun x => C(Eseqand x b2 ty))); eauto. intros [v1 [E1 S1]]. exploit safe_inv. eexact S1. eauto. simpl. intros [b BV]. destruct b. - econstructor; econstructor; eapply step_seqand_true; eauto. - econstructor; econstructor; eapply step_seqand_false; eauto. + econstructor; econstructor; eapply step_seqand_true; eauto. + econstructor; econstructor; eapply step_seqand_false; eauto. (* seqor *) exploit (simple_can_eval_rval f k e m b1 (fun x => C(Eseqor x b2 ty))); eauto. intros [v1 [E1 S1]]. exploit safe_inv. eexact S1. eauto. simpl. intros [b BV]. destruct b. - econstructor; econstructor; eapply step_seqor_true; eauto. - econstructor; econstructor; eapply step_seqor_false; eauto. + econstructor; econstructor; eapply step_seqor_true; eauto. + econstructor; econstructor; eapply step_seqor_false; eauto. (* condition *) exploit (simple_can_eval_rval f k e m b1 (fun x => C(Econdition x b2 b3 ty))); eauto. intros [v1 [E1 S1]]. exploit safe_inv. eexact S1. eauto. simpl. intros [b BV]. - econstructor; econstructor. eapply step_condition; eauto. + econstructor; econstructor. eapply step_condition; eauto. (* assign *) destruct Q. exploit (simple_can_eval_lval f k e m b1 (fun x => C(Eassign x b2 ty))); eauto. @@ -1320,7 +1320,7 @@ Proof. exploit (simple_can_eval_rval f k e m b2 (fun x => C(Eassign (Eloc b ofs (typeof b1)) x ty))); eauto. intros [v [E2 S2]]. exploit safe_inv. eexact S2. eauto. simpl. intros [v' [m' [t [A [B D]]]]]. - econstructor; econstructor; eapply step_assign; eauto. + econstructor; econstructor; eapply step_assign; eauto. (* assignop *) destruct Q. exploit (simple_can_eval_lval f k e m b1 (fun x => C(Eassignop op x b2 tyres ty))); eauto. @@ -1333,11 +1333,11 @@ Proof. destruct (classic (exists t2, exists m', assign_loc ge (typeof b1) m b ofs v4 t2 m')). destruct H2 as [t2 [m' D]]. econstructor; econstructor; eapply step_assignop; eauto. - econstructor; econstructor; eapply step_assignop_stuck; eauto. + econstructor; econstructor; eapply step_assignop_stuck; eauto. rewrite Heqo. rewrite Heqo0. intros; red; intros. elim H2. exists t2; exists m'; auto. - econstructor; econstructor; eapply step_assignop_stuck; eauto. + econstructor; econstructor; eapply step_assignop_stuck; eauto. rewrite Heqo. rewrite Heqo0. auto. - econstructor; econstructor; eapply step_assignop_stuck; eauto. + econstructor; econstructor; eapply step_assignop_stuck; eauto. rewrite Heqo. auto. (* postincr *) exploit (simple_can_eval_lval f k e m b (fun x => C(Epostincr id x ty))); eauto. @@ -1348,11 +1348,11 @@ Proof. destruct (classic (exists t2, exists m', assign_loc ge ty m b1 ofs v3 t2 m')). destruct H0 as [t2 [m' D]]. econstructor; econstructor; eapply step_postincr; eauto. - econstructor; econstructor; eapply step_postincr_stuck; eauto. + econstructor; econstructor; eapply step_postincr_stuck; eauto. rewrite Heqo. rewrite Heqo0. intros; red; intros. elim H0. exists t2; exists m'; congruence. - econstructor; econstructor; eapply step_postincr_stuck; eauto. + econstructor; econstructor; eapply step_postincr_stuck; eauto. rewrite Heqo. rewrite Heqo0. auto. - econstructor; econstructor; eapply step_postincr_stuck; eauto. + econstructor; econstructor; eapply step_postincr_stuck; eauto. rewrite Heqo. auto. (* comma *) exploit (simple_can_eval_rval f k e m b1 (fun x => C(Ecomma x b2 ty))); eauto. @@ -1370,9 +1370,9 @@ Proof. exploit safe_inv. 2: eapply leftcontext_context; eexact R. eapply safe_steps. eexact S1. apply (eval_simple_list_steps f k e m rargs vl E2 C'); auto. - simpl. intros X. exploit X. eapply rval_list_all_values. + simpl. intros X. exploit X. eapply rval_list_all_values. intros [tyargs [tyres [cconv [fd [vargs [P [Q [U V]]]]]]]]. - econstructor; econstructor; eapply step_call; eauto. eapply can_eval_simple_list; eauto. + econstructor; econstructor; eapply step_call; eauto. eapply can_eval_simple_list; eauto. (* builtin *) pose (C' := fun x => C(Ebuiltin ef tyargs x ty)). assert (contextlist' C'). unfold C'; eapply contextlist'_builtin with (rl0 := Enil); auto. @@ -1384,7 +1384,7 @@ Proof. simpl. intros X. exploit X. eapply rval_list_all_values. intros [vargs [t [vres [m' [U V]]]]]. econstructor; econstructor; eapply step_builtin; eauto. - eapply can_eval_simple_list; eauto. + eapply can_eval_simple_list; eauto. (* paren *) exploit (simple_can_eval_rval f k e m b (fun x => C(Eparen x tycast ty))); eauto. intros [v1 [E1 S1]]. @@ -1415,9 +1415,9 @@ Proof. assert (exists t, exists S', estep S t S'). inv H0. (* lred *) - eapply can_estep; eauto. inv H2; auto. + eapply can_estep; eauto. inv H2; auto. (* rred *) - eapply can_estep; eauto. inv H2; auto. inv H1; auto. + eapply can_estep; eauto. inv H2; auto. inv H1; auto. (* callred *) eapply can_estep; eauto. inv H2; auto. inv H1; auto. (* stuck *) @@ -1444,7 +1444,7 @@ Remark deref_loc_trace: deref_loc ge ty m b ofs t v -> match t with nil => True | ev :: nil => True | _ => False end. Proof. - intros. inv H; simpl; auto. inv H2; simpl; auto. + intros. inv H; simpl; auto. inv H2; simpl; auto. Qed. Remark deref_loc_receptive: @@ -1455,7 +1455,7 @@ Remark deref_loc_receptive: Proof. intros. assert (t1 = nil). exploit deref_loc_trace; eauto. destruct t1; simpl; tauto. - inv H. exploit volatile_load_receptive; eauto. intros [v' A]. + inv H. exploit volatile_load_receptive; eauto. intros [v' A]. split; auto; exists v'; econstructor; eauto. Qed. @@ -1464,7 +1464,7 @@ Remark assign_loc_trace: assign_loc ge ty m b ofs v t m' -> match t with nil => True | ev :: nil => output_event ev | _ => False end. Proof. - intros. inv H; simpl; auto. inv H2; simpl; auto. + intros. inv H; simpl; auto. inv H2; simpl; auto. Qed. Remark assign_loc_receptive: @@ -1475,10 +1475,10 @@ Remark assign_loc_receptive: Proof. intros. assert (t1 = nil). exploit assign_loc_trace; eauto. destruct t1; simpl; tauto. - inv H. eapply volatile_store_receptive; eauto. + inv H. eapply volatile_store_receptive; eauto. Qed. -Lemma semantics_strongly_receptive: +Lemma semantics_strongly_receptive: forall p, strongly_receptive (semantics p). Proof. intros. constructor; simpl; intros. @@ -1487,78 +1487,78 @@ Proof. inversion H; subst. inv H1. (* valof volatile *) - exploit deref_loc_receptive; eauto. intros [A [v' B]]. - econstructor; econstructor. left; eapply step_rvalof_volatile; eauto. + exploit deref_loc_receptive; eauto. intros [A [v' B]]. + econstructor; econstructor. left; eapply step_rvalof_volatile; eauto. (* assign *) exploit assign_loc_receptive; eauto. intro EQ; rewrite EQ in H. econstructor; econstructor; eauto. (* assignop *) - destruct t0 as [ | ev0 t0]; simpl in H10. + destruct t0 as [ | ev0 t0]; simpl in H10. subst t2. exploit assign_loc_receptive; eauto. intros EQ; rewrite EQ in H. econstructor; econstructor; eauto. inv H10. exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t0. destruct (sem_binary_operation ge op v1' (typeof l) v2 (typeof r) m) as [v3'|] eqn:?. destruct (sem_cast v3' tyres (typeof l)) as [v4'|] eqn:?. destruct (classic (exists t2', exists m'', assign_loc ge (typeof l) m b ofs v4' t2' m'')). - destruct H1 as [t2' [m'' P]]. - econstructor; econstructor. left; eapply step_assignop with (v1 := v1'); eauto. simpl; reflexivity. - econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto. + destruct H1 as [t2' [m'' P]]. + econstructor; econstructor. left; eapply step_assignop with (v1 := v1'); eauto. simpl; reflexivity. + econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto. rewrite Heqo; rewrite Heqo0. intros; red; intros; elim H1. exists t0; exists m'0; auto. - econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto. + econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto. rewrite Heqo; rewrite Heqo0; auto. - econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto. + econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto. rewrite Heqo; auto. (* assignop stuck *) exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t1. destruct (sem_binary_operation ge op v1' (typeof l) v2 (typeof r) m) as [v3'|] eqn:?. destruct (sem_cast v3' tyres (typeof l)) as [v4'|] eqn:?. destruct (classic (exists t2', exists m'', assign_loc ge (typeof l) m b ofs v4' t2' m'')). - destruct H1 as [t2' [m'' P]]. - econstructor; econstructor. left; eapply step_assignop with (v1 := v1'); eauto. simpl; reflexivity. - econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto. + destruct H1 as [t2' [m'' P]]. + econstructor; econstructor. left; eapply step_assignop with (v1 := v1'); eauto. simpl; reflexivity. + econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto. rewrite Heqo; rewrite Heqo0. intros; red; intros; elim H1. exists t2; exists m'; auto. - econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto. + econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto. rewrite Heqo; rewrite Heqo0; auto. - econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto. + econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto. rewrite Heqo; auto. (* postincr *) - destruct t0 as [ | ev0 t0]; simpl in H9. + destruct t0 as [ | ev0 t0]; simpl in H9. subst t2. exploit assign_loc_receptive; eauto. intros EQ; rewrite EQ in H. econstructor; econstructor; eauto. inv H9. exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t0. destruct (sem_incrdecr ge id v1' (typeof l)) as [v2'|] eqn:?. destruct (sem_cast v2' (incrdecr_type (typeof l)) (typeof l)) as [v3'|] eqn:?. destruct (classic (exists t2', exists m'', assign_loc ge (typeof l) m b ofs v3' t2' m'')). - destruct H1 as [t2' [m'' P]]. - econstructor; econstructor. left; eapply step_postincr with (v1 := v1'); eauto. simpl; reflexivity. - econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto. + destruct H1 as [t2' [m'' P]]. + econstructor; econstructor. left; eapply step_postincr with (v1 := v1'); eauto. simpl; reflexivity. + econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto. rewrite Heqo; rewrite Heqo0. intros; red; intros; elim H1. exists t0; exists m'0; auto. - econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto. + econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto. rewrite Heqo; rewrite Heqo0; auto. - econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto. + econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto. rewrite Heqo; auto. (* postincr stuck *) exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t1. destruct (sem_incrdecr ge id v1' (typeof l)) as [v2'|] eqn:?. destruct (sem_cast v2' (incrdecr_type (typeof l)) (typeof l)) as [v3'|] eqn:?. destruct (classic (exists t2', exists m'', assign_loc ge (typeof l) m b ofs v3' t2' m'')). - destruct H1 as [t2' [m'' P]]. - econstructor; econstructor. left; eapply step_postincr with (v1 := v1'); eauto. simpl; reflexivity. - econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto. + destruct H1 as [t2' [m'' P]]. + econstructor; econstructor. left; eapply step_postincr with (v1 := v1'); eauto. simpl; reflexivity. + econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto. rewrite Heqo; rewrite Heqo0. intros; red; intros; elim H1. exists t2; exists m'; auto. - econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto. + econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto. rewrite Heqo; rewrite Heqo0; auto. - econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto. + econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto. rewrite Heqo; auto. (* builtin *) - exploit external_call_trace_length; eauto. destruct t1; simpl; intros. - exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. + exploit external_call_trace_length; eauto. destruct t1; simpl; intros. + exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. econstructor; econstructor. left; eapply step_builtin; eauto. omegaContradiction. (* external calls *) inv H1. - exploit external_call_trace_length; eauto. destruct t1; simpl; intros. - exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. + exploit external_call_trace_length; eauto. destruct t1; simpl; intros. + exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. exists (Returnstate vres2 k m2); exists E0; right; econstructor; eauto. omegaContradiction. (* well-behaved traces *) @@ -1569,15 +1569,15 @@ Proof. exploit assign_loc_trace; eauto. destruct t; auto. destruct t; simpl; tauto. (* assignop *) exploit deref_loc_trace; eauto. exploit assign_loc_trace; eauto. - destruct t1. destruct t2. simpl; auto. destruct t2; simpl; tauto. - destruct t1. destruct t2. simpl; auto. destruct t2; simpl; tauto. + destruct t1. destruct t2. simpl; auto. destruct t2; simpl; tauto. + destruct t1. destruct t2. simpl; auto. destruct t2; simpl; tauto. tauto. (* assignop stuck *) exploit deref_loc_trace; eauto. destruct t; auto. destruct t; tauto. (* postincr *) exploit deref_loc_trace; eauto. exploit assign_loc_trace; eauto. - destruct t1. destruct t2. simpl; auto. destruct t2; simpl; tauto. - destruct t1. destruct t2. simpl; auto. destruct t2; simpl; tauto. + destruct t1. destruct t2. simpl; auto. destruct t2; simpl; tauto. + destruct t1. destruct t2. simpl; auto. destruct t2; simpl; tauto. tauto. (* postincr stuck *) exploit deref_loc_trace; eauto. destruct t; auto. destruct t; tauto. @@ -1603,9 +1603,9 @@ Proof. (* initial states match *) intros. exists s2; auto. (* final states match *) - intros. subst s2. auto. + intros. subst s2. auto. (* progress *) - intros. subst s2. apply progress. auto. + intros. subst s2. apply progress. auto. (* simulation *) intros. subst s1. exists s2'; split; auto. apply step_simulation; auto. Qed. @@ -1647,7 +1647,7 @@ Definition outcome_result_value (out: outcome) (t: type) (v: val) : Prop := | Out_return None, Tvoid => v = Vundef | Out_return (Some (v', ty')), ty => ty <> Tvoid /\ sem_cast v' ty' ty = Some v | _, _ => False - end. + end. (** [eval_expression ge e m1 a t m2 a'] describes the evaluation of the complex expression e. [v] is the resulting value, [m2] the final @@ -1775,7 +1775,7 @@ with eval_exprlist: env -> mem -> exprlist -> trace -> mem -> exprlist -> Prop : eval_expr e m RV a1 t1 m1 a1' -> eval_exprlist e m1 al t2 m2 al' -> eval_exprlist e m (Econs a1 al) (t1**t2) m2 (Econs a1' al') -(** [exec_stmt ge e m1 s t m2 out] describes the execution of +(** [exec_stmt ge e m1 s t m2 out] describes the execution of the statement [s]. [out] is the outcome for this execution. [m1] is the initial memory state, [m2] the final memory state. [t] is the trace of input/output events performed during this @@ -1856,12 +1856,12 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := eval_expression e m1 a t2 m2 v -> bool_val v (typeof a) m2 = Some true -> exec_stmt e m2 (Sdowhile a s) t3 m3 out -> - exec_stmt e m (Sdowhile a s) + exec_stmt e m (Sdowhile a s) (t1 ** t2 ** t3) m3 out | exec_Sfor_start: forall e m s a1 a2 a3 out m1 m2 t1 t2, exec_stmt e m a1 t1 m1 Out_normal -> exec_stmt e m1 (Sfor Sskip a2 a3 s) t2 m2 out -> - exec_stmt e m (Sfor a1 a2 a3 s) + exec_stmt e m (Sfor a1 a2 a3 s) (t1 ** t2) m2 out | exec_Sfor_false: forall e m s a2 a3 t m' v, eval_expression e m a2 t m' v -> @@ -1998,7 +1998,7 @@ CoInductive evalinf_expr: env -> mem -> kind -> expr -> traceinf -> Prop := evalinf_expr e m RV a1 t1 -> evalinf_expr e m RV (Ecall a1 a2 ty) t1 | evalinf_call_right: forall e m a1 t1 m1 a1' a2 t2 ty, - eval_expr e m RV a1 t1 m1 a1' -> + eval_expr e m RV a1 t1 m1 a1' -> evalinf_exprlist e m1 a2 t2 -> evalinf_expr e m RV (Ecall a1 a2 ty) (t1 *** t2) | evalinf_call: forall e m rf rargs ty t1 m1 rf' t2 m2 rargs' vf vargs @@ -2020,7 +2020,7 @@ with evalinf_exprlist: env -> mem -> exprlist -> traceinf -> Prop := eval_expr e m RV a1 t1 m1 a1' -> evalinf_exprlist e m1 al t2 -> evalinf_exprlist e m (Econs a1 al) (t1***t2) -(** [execinf_stmt ge e m1 s t] describes the diverging execution of +(** [execinf_stmt ge e m1 s t] describes the diverging execution of the statement [s]. *) with execinf_stmt: env -> mem -> statement -> traceinf -> Prop := @@ -2137,7 +2137,7 @@ Inductive outcome_state_match outcome_state_match e m f k Out_continue (State f Scontinue k e m) | osm_return_none: forall k', call_cont k' = call_cont k -> - outcome_state_match e m f k + outcome_state_match e m f k (Out_return None) (State f (Sreturn None) k' e m) | osm_return_some: forall v ty k', call_cont k' = call_cont k -> @@ -2168,16 +2168,16 @@ Lemma exprlist_app_leftcontext: forall rl1 rl2, simplelist rl1 = true -> leftcontextlist RV (fun x => exprlist_app rl1 (Econs x rl2)). Proof. - induction rl1; simpl; intros. + induction rl1; simpl; intros. apply lctx_list_head. constructor. - destruct (andb_prop _ _ H). apply lctx_list_tail. auto. auto. + destruct (andb_prop _ _ H). apply lctx_list_tail. auto. auto. Qed. Lemma exprlist_app_simple: forall rl1 rl2, simplelist (exprlist_app rl1 rl2) = simplelist rl1 && simplelist rl2. Proof. - induction rl1; intros; simpl. auto. rewrite IHrl1. apply andb_assoc. + induction rl1; intros; simpl. auto. rewrite IHrl1. apply andb_assoc. Qed. Lemma bigstep_to_steps: @@ -2212,9 +2212,9 @@ Proof. exploit (H0 (fun x => x) f k). constructor. intros [A [B C]]. assert (match a' with Eval _ _ => False | _ => True end -> star step ge (ExprState f a k e m) t (ExprState f (Eval v (typeof a)) k e m')). - intro. eapply star_right. eauto. left. eapply step_expr; eauto. traceEq. + intro. eapply star_right. eauto. left. eapply step_expr; eauto. traceEq. destruct a'; auto. - simpl in B. rewrite B in C. inv H1. auto. + simpl in B. rewrite B in C. inv H1. auto. (* val *) simpl; intuition. apply star_refl. @@ -2223,7 +2223,7 @@ Proof. (* field *) exploit (H0 (fun x => C(Efield x f ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. - simpl; intuition; eauto. + simpl; intuition; eauto. (* valof *) exploit (H1 (fun x => C(Evalof x ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. @@ -2232,8 +2232,8 @@ Proof. exploit (H1 (fun x => C(Evalof x ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. simpl; intuition. - eapply star_right. eexact D. - left. eapply step_rvalof_volatile; eauto. rewrite H4; eauto. congruence. congruence. + eapply star_right. eexact D. + left. eapply step_rvalof_volatile; eauto. rewrite H4; eauto. congruence. congruence. traceEq. (* deref *) exploit (H0 (fun x => C(Ederef x ty))). @@ -2252,7 +2252,7 @@ Proof. eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. exploit (H2 (fun x => C(Ebinop op a1' x ty))). eapply leftcontext_compose; eauto. repeat constructor. auto. intros [E [F G]]. - simpl; intuition. eapply star_trans; eauto. + simpl; intuition. eapply star_trans; eauto. (* cast *) exploit (H0 (fun x => C(Ecast x ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. @@ -2262,15 +2262,15 @@ Proof. eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. exploit (H4 (fun x => C(Eparen x type_bool ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [E [F G]]. - simpl; intuition. eapply star_trans. eexact D. - eapply star_left. left; eapply step_seqand_true; eauto. rewrite B; auto. + simpl; intuition. eapply star_trans. eexact D. + eapply star_left. left; eapply step_seqand_true; eauto. rewrite B; auto. eapply star_right. eexact G. left; eapply step_paren; eauto. rewrite F; eauto. - eauto. eauto. traceEq. + eauto. eauto. traceEq. (* seqand false *) exploit (H0 (fun x => C(Eseqand x a2 ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. - simpl; intuition. eapply star_right. eexact D. + simpl; intuition. eapply star_right. eexact D. left; eapply step_seqand_false; eauto. rewrite B; auto. traceEq. (* seqor false *) @@ -2278,15 +2278,15 @@ Proof. eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. exploit (H4 (fun x => C(Eparen x type_bool ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [E [F G]]. - simpl; intuition. eapply star_trans. eexact D. - eapply star_left. left; eapply step_seqor_false; eauto. rewrite B; auto. + simpl; intuition. eapply star_trans. eexact D. + eapply star_left. left; eapply step_seqor_false; eauto. rewrite B; auto. eapply star_right. eexact G. left; eapply step_paren; eauto. rewrite F; eauto. - eauto. eauto. traceEq. + eauto. eauto. traceEq. (* seqor true *) exploit (H0 (fun x => C(Eseqor x a2 ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. - simpl; intuition. eapply star_right. eexact D. + simpl; intuition. eapply star_right. eexact D. left; eapply step_seqor_true; eauto. rewrite B; auto. traceEq. (* condition *) @@ -2294,10 +2294,10 @@ Proof. eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. exploit (H4 (fun x => C(Eparen x ty ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [E [F G]]. - simpl. split; auto. split; auto. + simpl. split; auto. split; auto. eapply star_trans. eexact D. - eapply star_left. left; eapply step_condition; eauto. rewrite B; eauto. - eapply star_right. eexact G. left; eapply step_paren; eauto. congruence. + eapply star_left. left; eapply step_condition; eauto. rewrite B; eauto. + eapply star_right. eexact G. left; eapply step_paren; eauto. congruence. reflexivity. reflexivity. traceEq. (* sizeof *) simpl; intuition. apply star_refl. @@ -2309,7 +2309,7 @@ Proof. exploit (H2 (fun x => C(Eassign l' x ty))). eapply leftcontext_compose; eauto. repeat constructor. auto. intros [E [F G]]. simpl; intuition. - eapply star_trans. eexact D. + eapply star_trans. eexact D. eapply star_right. eexact G. left. eapply step_assign; eauto. congruence. rewrite B; eauto. congruence. reflexivity. traceEq. @@ -2319,7 +2319,7 @@ Proof. exploit (H2 (fun x => C(Eassignop op l' x tyres ty))). eapply leftcontext_compose; eauto. repeat constructor. auto. intros [E [F G]]. simpl; intuition. - eapply star_trans. eexact D. + eapply star_trans. eexact D. eapply star_right. eexact G. left. eapply step_assignop; eauto. rewrite B; eauto. rewrite B; rewrite F; eauto. congruence. rewrite B; eauto. congruence. @@ -2328,8 +2328,8 @@ Proof. exploit (H0 (fun x => C(Epostincr id x ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. simpl; intuition. - eapply star_right. eexact D. - left. eapply step_postincr; eauto. congruence. + eapply star_right. eexact D. + left. eapply step_postincr; eauto. congruence. traceEq. (* comma *) exploit (H0 (fun x => C(Ecomma x r2 ty))). @@ -2337,19 +2337,19 @@ Proof. exploit (H3 C). auto. intros [E [F G]]. simpl; intuition. congruence. eapply star_trans. eexact D. - eapply star_left. left; eapply step_comma; eauto. + eapply star_left. left; eapply step_comma; eauto. eexact G. reflexivity. traceEq. (* call *) exploit (H0 (fun x => C(Ecall x rargs ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. exploit (H2 rf' Enil ty C); eauto. intros [E F]. - simpl; intuition. + simpl; intuition. eapply star_trans. eexact D. - eapply star_trans. eexact F. - eapply star_left. left; eapply step_call; eauto. congruence. - eapply star_right. eapply H9. red; auto. - right; constructor. + eapply star_trans. eexact F. + eapply star_left. left; eapply step_call; eauto. congruence. + eapply star_right. eapply H9. red; auto. + right; constructor. reflexivity. reflexivity. reflexivity. traceEq. (* nil *) simpl; intuition. apply star_refl. @@ -2358,18 +2358,18 @@ Proof. eapply leftcontext_compose; eauto. repeat constructor. auto. apply exprlist_app_leftcontext; auto. intros [A [B D]]. exploit (H2 a0 (exprlist_app al2 (Econs a1' Enil))); eauto. - rewrite exprlist_app_simple. simpl. rewrite H5; rewrite A; auto. - repeat rewrite exprlist_app_assoc. simpl. + rewrite exprlist_app_simple. simpl. rewrite H5; rewrite A; auto. + repeat rewrite exprlist_app_assoc. simpl. intros [E F]. - simpl; intuition. + simpl; intuition. eapply star_trans; eauto. (* skip *) econstructor; split. apply star_refl. constructor. (* do *) - econstructor; split. - eapply star_left. right; constructor. + econstructor; split. + eapply star_left. right; constructor. eapply star_right. apply H0. right; constructor. reflexivity. traceEq. constructor. @@ -2379,7 +2379,7 @@ Proof. destruct (H2 f k) as [S2 [A2 B2]]; auto. econstructor; split. eapply star_left. right; econstructor. - eapply star_trans. eexact A1. + eapply star_trans. eexact A1. eapply star_left. right; constructor. eexact A2. reflexivity. reflexivity. traceEq. auto. @@ -2420,7 +2420,7 @@ Proof. econstructor; split. eapply star_left. right; apply step_return_1. eapply H0. traceEq. - econstructor; eauto. + econstructor; eauto. (* break *) econstructor; split. apply star_refl. constructor. @@ -2431,7 +2431,7 @@ Proof. (* while false *) econstructor; split. eapply star_left. right; apply step_while. - eapply star_right. apply H0. right; eapply step_while_false; eauto. + eapply star_right. apply H0. right; eapply step_while_false; eauto. reflexivity. traceEq. constructor. @@ -2448,7 +2448,7 @@ Proof. eapply star_left. right; eapply step_while_true; eauto. eapply star_trans. eexact A1. unfold S2. inversion H4; subst. - inv B1. apply star_one. right; constructor. + inv B1. apply star_one. right; constructor. apply star_refl. reflexivity. reflexivity. reflexivity. traceEq. unfold S2. inversion H4; subst. constructor. inv B1; econstructor; eauto. @@ -2474,9 +2474,9 @@ Proof. eapply star_trans. eexact A1. eapply star_left. inv H1; inv B1; right; eapply step_skip_or_continue_dowhile; eauto. - eapply star_right. apply H3. - right; eapply step_dowhile_false; eauto. - reflexivity. reflexivity. reflexivity. traceEq. + eapply star_right. apply H3. + right; eapply step_dowhile_false; eauto. + reflexivity. reflexivity. reflexivity. traceEq. constructor. (* dowhile stop *) @@ -2487,7 +2487,7 @@ Proof. | _ => S1 end). exists S2; split. - eapply star_left. right; apply step_dowhile. + eapply star_left. right; apply step_dowhile. eapply star_trans. eexact A1. unfold S2. inversion H1; subst. inv B1. apply star_one. right; constructor. @@ -2510,13 +2510,13 @@ Proof. auto. (* for start *) - assert (a1 = Sskip \/ a1 <> Sskip). destruct a1; auto; right; congruence. + assert (a1 = Sskip \/ a1 <> Sskip). destruct a1; auto; right; congruence. destruct H3. subst a1. inv H. apply H2; auto. destruct (H0 f (Kseq (Sfor Sskip a2 a3 s) k)) as [S1 [A1 B1]]; auto. inv B1. destruct (H2 f k) as [S2 [A2 B2]]; auto. exists S2; split. - eapply star_left. right; apply step_for_start; auto. + eapply star_left. right; apply step_for_start; auto. eapply star_trans. eexact A1. eapply star_left. right; constructor. eexact A2. reflexivity. reflexivity. traceEq. @@ -2524,8 +2524,8 @@ Proof. (* for false *) econstructor; split. - eapply star_left. right; apply step_for. - eapply star_right. apply H0. right; eapply step_for_false; eauto. + eapply star_left. right; apply step_for. + eapply star_right. apply H0. right; eapply step_for_false; eauto. reflexivity. traceEq. constructor. @@ -2537,12 +2537,12 @@ Proof. | _ => S1 end). exists S2; split. - eapply star_left. right; apply step_for. - eapply star_trans. apply H0. + eapply star_left. right; apply step_for. + eapply star_trans. apply H0. eapply star_left. right; eapply step_for_true; eauto. - eapply star_trans. eexact A1. + eapply star_trans. eexact A1. unfold S2. inversion H4; subst. - inv B1. apply star_one. right; constructor. + inv B1. apply star_one. right; constructor. apply star_refl. reflexivity. reflexivity. reflexivity. traceEq. unfold S2. inversion H4; subst. constructor. inv B1; econstructor; eauto. @@ -2552,15 +2552,15 @@ Proof. destruct (H6 f (Kfor4 a2 a3 s k)) as [S2 [A2 B2]]; auto. inv B2. destruct (H8 f k) as [S3 [A3 B3]]; auto. exists S3; split. - eapply star_left. right; apply step_for. - eapply star_trans. apply H0. + eapply star_left. right; apply step_for. + eapply star_trans. apply H0. eapply star_left. right; eapply step_for_true; eauto. eapply star_trans. eexact A1. eapply star_trans with (s2 := State f a3 (Kfor4 a2 a3 s k) e m2). inv H4; inv B1. - apply star_one. right; constructor; auto. - apply star_one. right; constructor; auto. - eapply star_trans. eexact A2. + apply star_one. right; constructor; auto. + apply star_one. right; constructor; auto. + eapply star_trans. eexact A2. eapply star_left. right; constructor. eexact A3. reflexivity. reflexivity. reflexivity. reflexivity. @@ -2578,13 +2578,13 @@ Proof. end). exists S2; split. eapply star_left. right; eapply step_switch. - eapply star_trans. apply H0. - eapply star_left. right; eapply step_expr_switch. eauto. - eapply star_trans. eexact A1. + eapply star_trans. apply H0. + eapply star_left. right; eapply step_expr_switch. eauto. + eapply star_trans. eexact A1. unfold S2; inv B1. - apply star_one. right; constructor. auto. - apply star_one. right; constructor. auto. - apply star_one. right; constructor. + apply star_one. right; constructor. auto. + apply star_one. right; constructor. auto. + apply star_one. right; constructor. apply star_refl. apply star_refl. reflexivity. reflexivity. reflexivity. traceEq. @@ -2593,7 +2593,7 @@ Proof. (* call internal *) destruct (H3 f k) as [S1 [A1 B1]]. eapply star_left. right; eapply step_internal_function; eauto. - eapply star_right. eexact A1. + eapply star_right. eexact A1. inv B1; simpl in H4; try contradiction. (* Out_normal *) assert (fn_return f = Tvoid /\ vres = Vundef). @@ -2611,7 +2611,7 @@ Proof. reflexivity. traceEq. (* call external *) - apply star_one. right; apply step_external_function; auto. + apply star_one. right; apply step_external_function; auto. Qed. Lemma eval_expression_to_steps: @@ -2713,7 +2713,7 @@ Lemma evalinf_funcall_steps: Proof. cofix COF. - assert (COS: + assert (COS: forall e m s t f k, execinf_stmt e m s t -> forever_N step lt ge O (State f s k e m) t). @@ -2735,180 +2735,180 @@ Proof. cofix COEL. intros. inv H. (* cons left *) - eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. eapply COE with (C := fun x => C(Ecall a1 (exprlist_app al (Econs x al0)) ty)). - eauto. eapply leftcontext_compose; eauto. constructor. auto. + eauto. eapply leftcontext_compose; eauto. constructor. auto. apply exprlist_app_leftcontext; auto. traceEq. -(* cons right *) - destruct (eval_expr_to_steps _ _ _ _ _ _ _ H3 +(* cons right *) + destruct (eval_expr_to_steps _ _ _ _ _ _ _ H3 (fun x => C(Ecall a1 (exprlist_app al (Econs x al0)) ty)) f k) - as [P [Q R]]. - eapply leftcontext_compose; eauto. repeat constructor. auto. - apply exprlist_app_leftcontext; auto. + as [P [Q R]]. + eapply leftcontext_compose; eauto. repeat constructor. auto. + apply exprlist_app_leftcontext; auto. eapply forever_N_star with (a2 := (esizelist al0)). eexact R. simpl; omega. change (Econs a1' al0) with (exprlist_app (Econs a1' Enil) al0). - rewrite <- exprlist_app_assoc. - eapply COEL. eauto. auto. auto. + rewrite <- exprlist_app_assoc. + eapply COEL. eauto. auto. auto. rewrite exprlist_app_simple. simpl. rewrite H2; rewrite P; auto. auto. intros. inv H. (* field *) eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. - eapply COE with (C := fun x => C(Efield x f0 ty)). eauto. + eapply COE with (C := fun x => C(Efield x f0 ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* valof *) eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. - eapply COE with (C := fun x => C(Evalof x ty)). eauto. + eapply COE with (C := fun x => C(Evalof x ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* deref *) eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. - eapply COE with (C := fun x => C(Ederef x ty)). eauto. + eapply COE with (C := fun x => C(Ederef x ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* addrof *) eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. - eapply COE with (C := fun x => C(Eaddrof x ty)). eauto. + eapply COE with (C := fun x => C(Eaddrof x ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* unop *) eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. - eapply COE with (C := fun x => C(Eunop op x ty)). eauto. + eapply COE with (C := fun x => C(Eunop op x ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* binop left *) eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. - eapply COE with (C := fun x => C(Ebinop op x a2 ty)). eauto. + eapply COE with (C := fun x => C(Ebinop op x a2 ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* binop right *) destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Ebinop op x a2 ty)) f k) - as [P [Q R]]. + as [P [Q R]]. eapply leftcontext_compose; eauto. repeat constructor. eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; omega. - eapply COE with (C := fun x => C(Ebinop op a1' x ty)). eauto. + eapply COE with (C := fun x => C(Ebinop op a1' x ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. auto. traceEq. (* cast *) eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. - eapply COE with (C := fun x => C(Ecast x ty)). eauto. + eapply COE with (C := fun x => C(Ecast x ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* seqand left *) eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. - eapply COE with (C := fun x => C(Eseqand x a2 ty)). eauto. + eapply COE with (C := fun x => C(Eseqand x a2 ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* seqand 2 *) destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Eseqand x a2 ty)) f k) - as [P [Q R]]. + as [P [Q R]]. eapply leftcontext_compose; eauto. repeat constructor. - eapply forever_N_plus. eapply plus_right. eexact R. + eapply forever_N_plus. eapply plus_right. eexact R. left; eapply step_seqand_true; eauto. rewrite Q; eauto. - reflexivity. + reflexivity. eapply COE with (C := fun x => (C (Eparen x type_bool ty))). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* seqor left *) eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. - eapply COE with (C := fun x => C(Eseqor x a2 ty)). eauto. + eapply COE with (C := fun x => C(Eseqor x a2 ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* seqor 2 *) destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Eseqor x a2 ty)) f k) - as [P [Q R]]. + as [P [Q R]]. eapply leftcontext_compose; eauto. repeat constructor. - eapply forever_N_plus. eapply plus_right. eexact R. + eapply forever_N_plus. eapply plus_right. eexact R. left; eapply step_seqor_false; eauto. rewrite Q; eauto. - reflexivity. + reflexivity. eapply COE with (C := fun x => (C (Eparen x type_bool ty))). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* condition top *) eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. - eapply COE with (C := fun x => C(Econdition x a2 a3 ty)). eauto. + eapply COE with (C := fun x => C(Econdition x a2 a3 ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* condition *) destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Econdition x a2 a3 ty)) f k) - as [P [Q R]]. + as [P [Q R]]. eapply leftcontext_compose; eauto. repeat constructor. - eapply forever_N_plus. eapply plus_right. eexact R. + eapply forever_N_plus. eapply plus_right. eexact R. left; eapply step_condition; eauto. rewrite Q; eauto. - reflexivity. + reflexivity. eapply COE with (C := fun x => (C (Eparen x ty ty))). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* assign left *) eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. - eapply COE with (C := fun x => C(Eassign x a2 ty)). eauto. + eapply COE with (C := fun x => C(Eassign x a2 ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* assign right *) destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Eassign x a2 ty)) f k) - as [P [Q R]]. + as [P [Q R]]. eapply leftcontext_compose; eauto. repeat constructor. eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; omega. - eapply COE with (C := fun x => C(Eassign a1' x ty)). eauto. + eapply COE with (C := fun x => C(Eassign a1' x ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. auto. traceEq. (* assignop left *) eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. - eapply COE with (C := fun x => C(Eassignop op x a2 tyres ty)). eauto. + eapply COE with (C := fun x => C(Eassignop op x a2 tyres ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* assignop right *) destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Eassignop op x a2 tyres ty)) f k) - as [P [Q R]]. + as [P [Q R]]. eapply leftcontext_compose; eauto. repeat constructor. eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; omega. - eapply COE with (C := fun x => C(Eassignop op a1' x tyres ty)). eauto. + eapply COE with (C := fun x => C(Eassignop op a1' x tyres ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. auto. traceEq. (* postincr *) eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. - eapply COE with (C := fun x => C(Epostincr id x ty)). eauto. + eapply COE with (C := fun x => C(Epostincr id x ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* comma left *) eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. - eapply COE with (C := fun x => C(Ecomma x a2 ty)). eauto. + eapply COE with (C := fun x => C(Ecomma x a2 ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* comma right *) destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Ecomma x a2 (typeof a2))) f k) - as [P [Q R]]. + as [P [Q R]]. eapply leftcontext_compose; eauto. repeat constructor. - eapply forever_N_plus. eapply plus_right. eexact R. - left; eapply step_comma; eauto. reflexivity. + eapply forever_N_plus. eapply plus_right. eexact R. + left; eapply step_comma; eauto. reflexivity. eapply COE with (C := C); eauto. traceEq. (* call left *) eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. - eapply COE with (C := fun x => C(Ecall x a2 ty)). eauto. + eapply COE with (C := fun x => C(Ecall x a2 ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* call right *) destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Ecall x a2 ty)) f k) - as [P [Q R]]. + as [P [Q R]]. eapply leftcontext_compose; eauto. repeat constructor. eapply forever_N_star with (a2 := (esizelist a2)). eexact R. simpl; omega. eapply COEL with (al := Enil). eauto. auto. auto. auto. traceEq. (* call *) destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Ecall x rargs ty)) f k) - as [P [Q R]]. + as [P [Q R]]. eapply leftcontext_compose; eauto. repeat constructor. destruct (eval_exprlist_to_steps _ _ _ _ _ _ H2 rf' Enil ty C f k) as [S T]. auto. auto. simpl; auto. eapply forever_N_plus. eapply plus_right. eapply star_trans. eexact R. eexact T. reflexivity. - simpl. left; eapply step_call; eauto. congruence. reflexivity. - apply COF. eauto. traceEq. + simpl. left; eapply step_call; eauto. congruence. reflexivity. + apply COF. eauto. traceEq. (* statements *) intros. inv H. (* do *) - eapply forever_N_plus. apply plus_one; right; constructor. + eapply forever_N_plus. apply plus_one; right; constructor. eapply COE with (C := fun x => x); eauto. constructor. traceEq. (* seq 1 *) - eapply forever_N_plus. apply plus_one; right; constructor. + eapply forever_N_plus. apply plus_one; right; constructor. eapply COS; eauto. traceEq. (* seq 2 *) destruct (exec_stmt_to_steps _ _ _ _ _ _ H0 f (Kseq s2 k)) as [S1 [A1 B1]]; auto. inv B1. - eapply forever_N_plus. - eapply plus_left. right; constructor. + eapply forever_N_plus. + eapply plus_left. right; constructor. eapply star_right. eauto. right; constructor. - reflexivity. reflexivity. + reflexivity. reflexivity. eapply COS; eauto. traceEq. (* if test *) - eapply forever_N_plus. apply plus_one; right; constructor. + eapply forever_N_plus. apply plus_one; right; constructor. eapply COE with (C := fun x => x); eauto. constructor. traceEq. (* if true/false *) eapply forever_N_plus. eapply plus_left. right; constructor. eapply star_right. eapply eval_expression_to_steps; eauto. - right. eapply step_ifthenelse_2 with (b := b). auto. + right. eapply step_ifthenelse_2 with (b := b). auto. reflexivity. reflexivity. eapply COS; eauto. traceEq. (* return some *) @@ -2919,7 +2919,7 @@ Proof. eapply COE with (C := fun x => x); eauto. constructor. traceEq. (* while body *) eapply forever_N_plus. - eapply plus_left. right; constructor. + eapply plus_left. right; constructor. eapply star_right. eapply eval_expression_to_steps; eauto. right; apply step_while_true; auto. reflexivity. reflexivity. @@ -2927,10 +2927,10 @@ Proof. (* while loop *) destruct (exec_stmt_to_steps _ _ _ _ _ _ H2 f (Kwhile2 a s0 k)) as [S1 [A1 B1]]; auto. eapply forever_N_plus. - eapply plus_left. right; constructor. + eapply plus_left. right; constructor. eapply star_trans. eapply eval_expression_to_steps; eauto. eapply star_left. right; apply step_while_true; auto. - eapply star_trans. eexact A1. + eapply star_trans. eexact A1. inv H3; inv B1; apply star_one; right; apply step_skip_or_continue_while; auto. reflexivity. reflexivity. reflexivity. reflexivity. eapply COS; eauto. traceEq. @@ -2940,7 +2940,7 @@ Proof. (* dowhile test *) destruct (exec_stmt_to_steps _ _ _ _ _ _ H0 f (Kdowhile1 a s0 k)) as [S1 [A1 B1]]; auto. eapply forever_N_plus. - eapply plus_left. right; constructor. + eapply plus_left. right; constructor. eapply star_trans. eexact A1. eapply star_one. right. inv H1; inv B1; apply step_skip_or_continue_dowhile; auto. reflexivity. reflexivity. @@ -2948,7 +2948,7 @@ Proof. (* dowhile loop *) destruct (exec_stmt_to_steps _ _ _ _ _ _ H0 f (Kdowhile1 a s0 k)) as [S1 [A1 B1]]; auto. eapply forever_N_plus. - eapply plus_left. right; constructor. + eapply plus_left. right; constructor. eapply star_trans. eexact A1. eapply star_left. right. inv H1; inv B1; apply step_skip_or_continue_dowhile; auto. eapply star_right. eapply eval_expression_to_steps; eauto. @@ -2962,9 +2962,9 @@ Proof. (* for start 2 *) destruct (exec_stmt_to_steps _ _ _ _ _ _ H0 f (Kseq (Sfor Sskip a2 a3 s0) k)) as [S1 [A1 B1]]; auto. inv B1. eapply forever_N_plus. - eapply plus_left. right; constructor. auto. + eapply plus_left. right; constructor. auto. eapply star_trans. eexact A1. - apply star_one. right; constructor. + apply star_one. right; constructor. reflexivity. reflexivity. eapply COS; eauto. traceEq. (* for test *) @@ -2983,7 +2983,7 @@ Proof. eapply plus_left. right; apply step_for. eapply star_trans. eapply eval_expression_to_steps; eauto. eapply star_left. right; apply step_for_true; auto. - eapply star_trans. eexact A1. + eapply star_trans. eexact A1. inv H3; inv B1; apply star_one; right; apply step_skip_or_continue_for3; auto. reflexivity. reflexivity. reflexivity. reflexivity. eapply COS; eauto. traceEq. @@ -2997,7 +2997,7 @@ Proof. eapply star_trans. eexact A1. eapply star_left. inv H3; inv B1; right; apply step_skip_or_continue_for3; auto. - eapply star_right. eexact A2. + eapply star_right. eexact A2. right; constructor. reflexivity. reflexivity. reflexivity. reflexivity. reflexivity. reflexivity. eapply COS; eauto. traceEq. @@ -3006,15 +3006,15 @@ Proof. eapply COE with (C := fun x => x); eauto. constructor. traceEq. (* switch body *) eapply forever_N_plus. - eapply plus_left. right; constructor. - eapply star_right. eapply eval_expression_to_steps; eauto. - right; constructor. eauto. - reflexivity. reflexivity. - eapply COS; eauto. traceEq. + eapply plus_left. right; constructor. + eapply star_right. eapply eval_expression_to_steps; eauto. + right; constructor. eauto. + reflexivity. reflexivity. + eapply COS; eauto. traceEq. (* funcalls *) intros. inv H. - eapply forever_N_plus. apply plus_one. right; econstructor; eauto. + eapply forever_N_plus. apply plus_one. right; econstructor; eauto. eapply COS; eauto. traceEq. Qed. @@ -3024,7 +3024,7 @@ End BIGSTEP. Inductive bigstep_program_terminates (p: program): trace -> int -> Prop := | bigstep_program_terminates_intro: forall b f m0 m1 t r, - let ge := globalenv p in + let ge := globalenv p in Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> @@ -3034,7 +3034,7 @@ Inductive bigstep_program_terminates (p: program): trace -> int -> Prop := Inductive bigstep_program_diverges (p: program): traceinf -> Prop := | bigstep_program_diverges_intro: forall b f m0 t, - let ge := globalenv p in + let ge := globalenv p in Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> @@ -3050,7 +3050,7 @@ Theorem bigstep_semantics_sound: Proof. intros; constructor; intros. (* termination *) - inv H. econstructor; econstructor. + inv H. econstructor; econstructor. split. econstructor; eauto. split. apply eval_funcall_to_steps. eauto. red; auto. econstructor. -- cgit