Commit 7f9c5994 authored by Robbert Krebbers's avatar Robbert Krebbers

Modify typing judgments to depend on a description of the types of objects in

memory instead of the whole memory itself.

This has the following advantages:
* Avoid parametrization in {addresses,pointers,pointer_bits,bits}.v
* Make {base_values,values}.v independent of the memory, this makes better
  parallelized compilation possible.
* Allow small memories (e.g. singletons as used in separation logic) with
  addresses to objects in another part to be typed.
* Some proofs become easier, because the memory environments are preserved
  under many operations (insert, force, lock, unlock).

It also as the following disadvantages:
* At all kinds of places we now have explicit casts from memories to memory
  environments. This is kind of ugly. Note, we cannot declare memenv_of as a
  Coercion because it is non-uniform.
* It is a bit inefficient with respect to the interpreter, because memory
  environments are finite functions instead of proper functions, so calling
  memenv_of often (which we do) is not too good.
parent 7040c040
......@@ -12,6 +12,8 @@ Proof. firstorder. Qed.
Lemma Is_true_reflect (b : bool) : reflect b b.
Proof. destruct b. by left. right. intros []. Qed.
Instance: Injective (=) () Is_true.
Proof. intros [] []; simpl; intuition. Qed.
(** We introduce [decide_rel] to avoid inefficienct computation due to eager
evaluation of propositions by [vm_compute]. This inefficiency occurs if
......@@ -105,10 +107,12 @@ Tactic Notation "case_bool_decide" "as" ident (Hd) :=
Tactic Notation "case_bool_decide" :=
let H := fresh in case_bool_decide as H.
Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P P.
Lemma bool_decide_spec (P : Prop) {dec : Decision P} : bool_decide P P.
Proof. unfold bool_decide. by destruct dec. Qed.
Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P P.
Proof. by rewrite bool_decide_spec. Qed.
Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P bool_decide P.
Proof. unfold bool_decide. by destruct dec. Qed.
Proof. by rewrite bool_decide_spec. Qed.
(** * Decidable Sigma types *)
(** Leibniz equality on Sigma types requires the equipped proofs to be
......
......@@ -1342,6 +1342,7 @@ Tactic Notation "simpl_map" "by" tactic3(tac) := repeat
rewrite lookup_delete in H || rewrite lookup_delete_ne in H by tac
| H : context[ {[ _ ]} !! _ ] |- _ =>
rewrite lookup_singleton in H || rewrite lookup_singleton_ne in H by tac
| H : context[ (_ <$> _) !! _ ] |- _ => rewrite lookup_fmap in H
| H : context[ lookup (A:=?A) ?i (?m1 ?m2) ] |- _ =>
let x := fresh in evar (x:A);
let x' := eval unfold x in x in clear x;
......@@ -1357,6 +1358,7 @@ Tactic Notation "simpl_map" "by" tactic3(tac) := repeat
rewrite lookup_delete || rewrite lookup_delete_ne by tac
| |- context[ {[ _ ]} !! _ ] =>
rewrite lookup_singleton || rewrite lookup_singleton_ne by tac
| |- context[ (_ <$> _) !! _ ] => rewrite lookup_fmap
| |- context [ lookup (A:=?A) ?i ?m ] =>
let x := fresh in evar (x:A);
let x' := eval unfold x in x in clear x;
......@@ -1398,6 +1400,9 @@ Tactic Notation "simplify_map_equality" "by" tactic3(tac) :=
apply map_union_cancel_r in H; [|by tac|by tac]
| H : {[?i,?x]} = |- _ => by destruct (map_non_empty_singleton i x)
| H : = {[?i,?x]} |- _ => by destruct (map_non_empty_singleton i x)
| H : ?m !! ?i = Some _, H2 : ?m !! ?j = None |- _ =>
unless (i j) by done;
assert (i j) by (by intros ?; simplify_equality)
end.
Tactic Notation "simplify_map_equality'" "by" tactic3(tac) :=
repeat (progress csimpl in * || simplify_map_equality by tac).
......
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