From b2fc9b55d9c59a9c507786a650377e2f0a1ddad8 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 29 Sep 2020 16:22:18 +0200 Subject: simpl -> cbn --- kvx/Conventions1.v | 34 +++++++++++++++++----------------- 1 file changed, 17 insertions(+), 17 deletions(-) (limited to 'kvx/Conventions1.v') diff --git a/kvx/Conventions1.v b/kvx/Conventions1.v index ab30ded9..0b2cf406 100644 --- a/kvx/Conventions1.v +++ b/kvx/Conventions1.v @@ -108,7 +108,7 @@ Lemma loc_result_type: subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true. Proof. intros. unfold proj_sig_res, loc_result, mreg_type. - destruct (sig_res sig); try destruct Archi.ptr64; simpl; trivial; destruct t; trivial. + destruct (sig_res sig); try destruct Archi.ptr64; cbn; trivial; destruct t; trivial. Qed. (** The result locations are caller-save registers *) @@ -118,7 +118,7 @@ Lemma loc_result_caller_save: forall_rpair (fun r => is_callee_save r = false) (loc_result s). Proof. intros. unfold loc_result, is_callee_save; - destruct (sig_res s); simpl; auto; try destruct Archi.ptr64; simpl; auto; try destruct t; simpl; auto. + destruct (sig_res s); cbn; auto; try destruct Archi.ptr64; cbn; auto; try destruct t; cbn; auto. Qed. (** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *) @@ -296,9 +296,9 @@ Proof. OKREGS regs -> OKF f -> ofs >= 0 -> OK (one_arg regs rn ofs ty f)). { intros until f; intros OR OF OO; red; unfold one_arg; intros. destruct (list_nth_z regs rn) as [r|] eqn:NTH; destruct H. - - subst p; simpl. apply OR. eapply list_nth_z_in; eauto. + - subst p; cbn. apply OR. eapply list_nth_z_in; eauto. - eapply OF; eauto. - - subst p; simpl. auto using align_divides, typealign_pos. + - subst p; cbn. auto using align_divides, typealign_pos. - eapply OF; [idtac|eauto]. generalize (AL ofs ty OO) (SKK ty); omega. } @@ -310,16 +310,16 @@ Proof. assert (OO': ofs' >= 0) by (apply (AL ofs Tlong); auto). assert (DFL: OK (Twolong (S Outgoing (ofs' + 1) Tint) (S Outgoing ofs' Tint) :: f rn' (ofs' + 2))). - { red; simpl; intros. destruct H. - - subst p; simpl. + { red; cbn; intros. destruct H. + - subst p; cbn. repeat split; auto using Z.divide_1_l. omega. - eapply OF; [idtac|eauto]. omega. } destruct (list_nth_z regs rn') as [r1|] eqn:NTH1; destruct (list_nth_z regs (rn' + 1)) as [r2|] eqn:NTH2; try apply DFL. - red; simpl; intros; destruct H. - - subst p; simpl. split; apply OR; eauto using list_nth_z_in. + red; cbn; intros; destruct H. + - subst p; cbn. split; apply OR; eauto using list_nth_z_in. - eapply OF; [idtac|eauto]. auto. } assert (C: forall regs rn ofs ty f, @@ -327,10 +327,10 @@ Proof. { intros until f; intros OR OF OO OTY; unfold hybrid_arg; red; intros. set (rn' := align rn 2) in *. destruct (list_nth_z regs rn') as [r|] eqn:NTH; destruct H. - - subst p; simpl. apply OR. eapply list_nth_z_in; eauto. + - subst p; cbn. apply OR. eapply list_nth_z_in; eauto. - eapply OF; eauto. - - subst p; simpl. rewrite OTY. split. apply (AL ofs Tlong OO). apply Z.divide_1_l. - - eapply OF; [idtac|eauto]. generalize (AL ofs Tlong OO); simpl; omega. + - subst p; cbn. rewrite OTY. split. apply (AL ofs Tlong OO). apply Z.divide_1_l. + - eapply OF; [idtac|eauto]. generalize (AL ofs Tlong OO); cbn; omega. } assert (D: OKREGS param_regs). { red. decide_goal. } @@ -339,8 +339,8 @@ Proof. cut (forall va tyl rn ofs, ofs >= 0 -> OK (loc_arguments_rec va tyl rn ofs)). unfold OK. eauto. - induction tyl as [ | ty1 tyl]; intros until ofs; intros OO; simpl. - - red; simpl; tauto. + induction tyl as [ | ty1 tyl]; intros until ofs; intros OO; cbn. + - red; cbn; tauto. - destruct ty1. + (* int *) apply A; auto. + (* float *) @@ -369,10 +369,10 @@ Remark fold_max_outgoing_above: Proof. assert (A: forall n l, max_outgoing_1 n l >= n). { intros; unfold max_outgoing_1. destruct l as [_ | []]; xomega. } - induction l; simpl; intros. + induction l; cbn; intros. - omega. - eapply Zge_trans. eauto. - destruct a; simpl. apply A. eapply Zge_trans; eauto. + destruct a; cbn. apply A. eapply Zge_trans; eauto. Qed. Lemma size_arguments_above: @@ -392,14 +392,14 @@ Proof. assert (B: forall p n, In (S Outgoing ofs ty) (regs_of_rpair p) -> ofs + typesize ty <= max_outgoing_2 n p). - { intros. destruct p; simpl in H; intuition; subst; simpl. + { intros. destruct p; cbn in H; intuition; subst; cbn. - xomega. - eapply Z.le_trans. 2: apply A. xomega. - xomega. } assert (C: forall l n, In (S Outgoing ofs ty) (regs_of_rpairs l) -> ofs + typesize ty <= fold_left max_outgoing_2 l n). - { induction l; simpl; intros. + { induction l; cbn; intros. - contradiction. - rewrite in_app_iff in H. destruct H. + eapply Z.le_trans. eapply B; eauto. apply Z.ge_le. apply fold_max_outgoing_above. -- cgit