From 65a36dac0de3123b2e9663a6cb1b4d891fc244ac Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Thu, 29 Nov 2018 12:02:23 +0100 Subject: [PATCH] Git rid of dLocUnknown. --- theories/vcgen/dcexpr.v | 70 +++++++++--------------------------- theories/vcgen/reification.v | 5 +-- theories/vcgen/vcg.v | 10 +++--- 3 files changed, 22 insertions(+), 63 deletions(-) diff --git a/theories/vcgen/dcexpr.v b/theories/vcgen/dcexpr.v index 4a53a36..f087ab6 100644 --- a/theories/vcgen/dcexpr.v +++ b/theories/vcgen/dcexpr.v @@ -13,14 +13,7 @@ Proof. solve_decision. Defined. Instance dint_eq_dec : EqDecision dint. Proof. solve_decision. Defined. -Inductive dbase_loc := - | dLocKnown : nat → dbase_loc - | dLocUnknown : cloc → dbase_loc. - -Instance dbase_loc_eq_dec : EqDecision dbase_loc. -Proof. solve_decision. Defined. - -Record dloc := dLoc { dloc_base : dbase_loc; dloc_offset : dint }. +Record dloc := dLoc { dloc_base : nat; dloc_offset : dint }. Instance dloc_eq_dec : EqDecision dloc. Proof. solve_decision. Defined. @@ -95,7 +88,7 @@ Definition dknown_bool_of_dval (dv : dval) : option bool := Definition dloc_var_of_dloc (dl : dloc) : option nat := match dl with - | dLoc (dLocKnown i) (dInt 0 None) => Some i + | dLoc i (dInt 0 None) => Some i | _ => None end. Definition dloc_var_of_dval (dv : dval) : option nat := @@ -120,11 +113,8 @@ Definition succ_nat_of_dval (dv : dval) : option dint := Definition dloc_var_wf (E : known_locs) (i : nat) : bool := bool_decide (is_Some (E !! i)). -Definition dbase_loc_wf (E : known_locs) (dl : dbase_loc) : bool := - match dl with dLocKnown i => dloc_var_wf E i | _ => true end. - Definition dloc_wf (E : known_locs) (dl : dloc) : bool := - dbase_loc_wf E (dloc_base dl). + dloc_var_wf E (dloc_base dl). Fixpoint dval_wf (E : known_locs) (dv : dval) : bool := match dv with @@ -184,24 +174,17 @@ Definition dloc_var_interp (E : known_locs) (i : nat) : cloc := default inhabitant (E !! i). Arguments dloc_var_interp !_ !_ /. -Definition dbase_loc_interp (E : known_locs) (dl : dbase_loc) : cloc := - match dl with - | dLocKnown i => dloc_var_interp E i - | dLocUnknown cl => cl - end. -Arguments dbase_loc_interp _ !_ / : simpl nomatch. - Definition dloc_interp (E : known_locs) (dl : dloc) : cloc := match dl with | dLoc i dj => match dint_interp' dj with - | Some j => dbase_loc_interp E i +∗ j - | None => dbase_loc_interp E i + | Some j => dloc_var_interp E i +∗ j + | None => dloc_var_interp E i end end. Arguments dloc_interp _ !_ / : simpl nomatch. Lemma dloc_interp_alt E dl : - dloc_interp E dl = dbase_loc_interp E (dloc_base dl) +∗ dint_interp (dloc_offset dl). + dloc_interp E dl = dloc_var_interp E (dloc_base dl) +∗ dint_interp (dloc_offset dl). Proof. destruct dl as [? [[] [[]|]]]=> //=. Qed. Definition dbool_interp (db : dbool) : bool := @@ -357,13 +340,6 @@ Definition dint_eq (di1 di2 : dint) : dbool := end. Arguments dint_eq !_ !_ / : simpl nomatch. -Definition dbase_loc_strong_eq (dl1 dl2 : dbase_loc) : bool := - match dl1, dl2 with - | dLocKnown i1, dLocKnown i2 => bool_decide (i1 = i2) - | _, _ => false - end. -Arguments dbase_loc_strong_eq !_ !_ / : simpl nomatch. - Definition dloc_plus (dl : dloc) (dj : dint) : dloc := match dl with | dLoc dl di => dLoc dl (dint_plus di dj) @@ -371,13 +347,13 @@ Definition dloc_plus (dl : dloc) (dj : dint) : dloc := Arguments dloc_plus !_ !_ / : simpl nomatch. Definition dloc_eq (E : known_locs) (dl1 dl2 : dloc) : dbool := - if dbase_loc_strong_eq (dloc_base dl1) (dloc_base dl2) + if decide (dloc_base dl1 = dloc_base dl2) then dint_eq (dloc_offset dl1) (dloc_offset dl2) else dBoolUnknown (bool_decide (dloc_interp E dl1 = dloc_interp E dl2)). Arguments dloc_eq _ !_ !_ / : simpl nomatch. Definition dloc_lt (E : known_locs) (dl1 dl2 : dloc) : dbool := - if dbase_loc_strong_eq (dloc_base dl1) (dloc_base dl2) + if decide (dloc_base dl1 = dloc_base dl2) then dint_lt (dloc_offset dl1) (dloc_offset dl2) else dBoolUnknown (cloc_lt (dloc_interp E dl1) (dloc_interp E dl2)). Arguments dloc_lt _ !_ !_ / : simpl nomatch. @@ -477,12 +453,12 @@ Lemma dknown_bool_of_dval_correct E dv b : Proof. by intros ->%dknown_bool_of_dval_Some. Qed. Lemma dloc_var_of_dloc_Some dl i : - dloc_var_of_dloc dl = Some i → dl = dLoc (dLocKnown i) (dInt 0 None). + dloc_var_of_dloc dl = Some i → dl = dLoc i (dInt 0 None). Proof. rewrite /dloc_var_of_dloc. intros; by repeat (simplify_eq/= || case_match). Qed. Lemma dloc_var_of_dval_Some dv i : - dloc_var_of_dval dv = Some i → dv = dLocV (dLoc (dLocKnown i) (dInt 0 None)). + dloc_var_of_dval dv = Some i → dv = dLocV (dLoc i (dInt 0 None)). Proof. by intros (dl&->%dloc_of_dval_Some&->%dloc_var_of_dloc_Some)%bind_Some. Qed. Lemma dloc_var_of_dval_wf E dv i : dloc_var_of_dval dv = Some i → dval_wf E dv → dloc_var_wf E i. @@ -563,9 +539,6 @@ Proof. destruct di1 as [? [[]|]], di2 as [? [[]|]]; simpl; repeat case_bool_decide; auto with lia. Qed. -Lemma dbase_loc_strong_eq_correct E dl1 dl2 : - dbase_loc_strong_eq dl1 dl2 = true → dbase_loc_interp E dl1 = dbase_loc_interp E dl2. -Proof. intros; destruct dl1, dl2; by simplify_option_eq. Qed. Lemma dloc_plus_correct E dl di : dloc_interp E (dloc_plus dl di) = dloc_interp E dl +∗ dint_interp di. Proof. @@ -574,18 +547,16 @@ Qed. Lemma dloc_lt_correct E dl1 dl2 : dbool_interp (dloc_lt E dl1 dl2) = cloc_lt (dloc_interp E dl1) (dloc_interp E dl2). Proof. - unfold dloc_lt. destruct (dbase_loc_strong_eq _ _) eqn:H; last done. + unfold dloc_lt. destruct (decide _) as [H|]; last done. rewrite dint_lt_correct /cloc_lt !dloc_interp_alt /=. - apply (dbase_loc_strong_eq_correct E) in H as ->. - repeat case_bool_decide; naive_solver eauto with lia. + rewrite H. repeat case_bool_decide; naive_solver eauto with lia. Qed. Lemma dloc_eq_correct E dl1 dl2 : dbool_interp (dloc_eq E dl1 dl2) = bool_decide (dloc_interp E dl1 = dloc_interp E dl2). Proof. - unfold dloc_eq. destruct (dbase_loc_strong_eq _ _) eqn:H; last done. + unfold dloc_eq. destruct (decide _) as [H|]; last done. rewrite dint_eq_correct !dloc_interp_alt /=. - apply (dbase_loc_strong_eq_correct E) in H as ->. - apply bool_decide_iff; split; [by intros ->|by intros ?%(inj _)]. + rewrite H. apply bool_decide_iff; split; [by intros ->|by intros ?%(inj _)]. Qed. Lemma dbin_op_eval_int_correct op di1 di2 : @@ -668,13 +639,9 @@ Proof. intros [v ?] [E'' ->]. exists v; by apply lookup_app_l_Some. Qed. -Lemma dbase_loc_wf_mono E E' dl : - dbase_loc_wf E dl → E `prefix_of` E' → dbase_loc_wf E' dl. -Proof. destruct dl; simpl; eauto using dloc_var_wf_mono. Qed. - Lemma dloc_wf_mono E E' dl : dloc_wf E dl → E `prefix_of` E' → dloc_wf E' dl. -Proof. apply dbase_loc_wf_mono. Qed. +Proof. apply dloc_var_wf_mono. Qed. Lemma dval_wf_mono E E' dv : dval_wf E dv → E `prefix_of` E' → dval_wf E' dv. @@ -723,17 +690,12 @@ Proof. intros [v ?] [E'' ->]. rewrite lookup_app_l; eauto using lookup_lt_is_Some_1. Qed. -Lemma dbase_loc_interp_mono E E' dl : - dbase_loc_wf E dl → E `prefix_of` E' → - dbase_loc_interp E dl = dbase_loc_interp E' dl. -Proof. destruct dl; simpl; eauto using dloc_var_interp_mono. Qed. - Lemma dloc_interp_mono E E' dl : dloc_wf E dl → E `prefix_of` E' → dloc_interp E dl = dloc_interp E' dl. Proof. rewrite !dloc_interp_alt=> ??. destruct dl as [dl i]. - f_equal. by apply dbase_loc_interp_mono. + f_equal. by apply dloc_var_interp_mono. Qed. Lemma dval_interp_mono E E' dv : diff --git a/theories/vcgen/reification.v b/theories/vcgen/reification.v index ef5015c..7d43416 100644 --- a/theories/vcgen/reification.v +++ b/theories/vcgen/reification.v @@ -71,7 +71,7 @@ Class IntoDLoc (E E' : known_locs) (cl : cloc) (dl : dloc) := { }. Instance into_dloc_lookup E E' cl i : - LocLookup E E' cl i → IntoDLoc E E' cl (dLoc (dLocKnown i) (dInt 0 None)) | 10. + LocLookup E E' cl i → IntoDLoc E E' cl (dLoc i (dInt 0 None)) | 10. Proof. intros [Hi ?]. split=> //=. - by rewrite /dloc_var_interp Hi. @@ -85,9 +85,6 @@ Proof. - by rewrite dloc_plus_correct. - by apply dloc_plus_wf. Qed. -Instance into_dloc_default E cl : - IntoDLoc E E cl (dLoc (dLocUnknown cl) (dInt 0 None)) | 100. -Proof. done. Qed. (** ** IntoDBaseLit *) Class IntoDBaseLit (l : base_lit) (dl : dbase_lit) := diff --git a/theories/vcgen/vcg.v b/theories/vcgen/vcg.v index 84c353a..e88bc47 100644 --- a/theories/vcgen/vcg.v +++ b/theories/vcgen/vcg.v @@ -27,7 +27,7 @@ Section vcg. let i := length E in block_info cl true (S (Z.to_nat (dint_interp di))) -∗ (cl +∗ 1) ↦C∗ replicate (Z.to_nat (dint_interp di)) (dval_interp E dv2) -∗ - Φ (E ++ [cl]) (denv_insert i ULvl 1 dv2 m) (dLocV (dLoc (dLocKnown i) (dInt 0 None))) + Φ (E ++ [cl]) (denv_insert i ULvl 1 dv2 m) (dLocV (dLoc i (dInt 0 None))) | _ => wand_denv_interp E m (∃ n : nat, ⌜ dval_interp E dv1 = #n ⌝ ∧ ⌜ n ≠ O ⌝ ∧ ∀ cl, @@ -143,7 +143,7 @@ Section vcg. | dCMutBind mx de1 de2, S n => vcg E n m de1 R \$ λ E m dv1, ∀ cl, let i := length E in - let dlv := dLocV (dLoc (dLocKnown i) (dInt 0 None)) in + let dlv := dLocV (dLoc i (dInt 0 None)) in vcg (E ++ [cl]) n (denv_insert i ULvl 1 dv1 (denv_unlock m)) (dce_subst' (E ++ [cl]) mx dlv de2) R \$ λ E m dv2, @@ -322,7 +322,7 @@ Section vcg_spec. iSplit; first done. iIntros (cl) "Hinfo [Hcl Hcls]". assert (dloc_var_interp (E ++ [cl]) (length E) = cl) as Hcl. { by rewrite /dloc_var_interp (list_lookup_middle _ []). } - iExists (E ++ [cl]), (dLocV (dLoc (dLocKnown (length E)) (dInt 0 None))), + iExists (E ++ [cl]), (dLocV (dLoc (length E) (dInt 0 None))), (denv_insert (length E) ULvl 1 dv2 m); simpl. iSplit; first by rewrite Hcl. iSplit; first by eauto using prefix_app_r. @@ -458,9 +458,9 @@ Section vcg_spec. iIntros (cl) "Hcl". iSpecialize ("H" \$! cl). assert (E' `prefix_of` E' ++ [cl]) by eauto using prefix_app_r. set (i := length E'). - set (dlv := dLocV (dLoc (dLocKnown i) (dInt 0 None))). + set (dlv := dLocV (dLoc i (dInt 0 None))). assert (dval_wf (E' ++ [cl]) dlv). - { rewrite /dlv /= /dloc_wf /dbase_loc_wf /= /dloc_var_wf. + { rewrite /dlv /= /dloc_wf /= /dloc_var_wf. by rewrite (list_lookup_middle _ []). } iDestruct ("IH" with "[%] [%] [Hm Hcl] H") as "H". { eauto using dcexpr_wf_mono. } -- GitLab