Commit 65a36dac authored by Robbert Krebbers's avatar Robbert Krebbers

Git rid of dLocUnknown.

parent f501885f
......@@ -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 :
......
......@@ -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) :=
......
......@@ -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. }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment