Commit 188fabd4 authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

Use notation for [void_ptr].

parent e529fa21
......@@ -30,13 +30,13 @@ Section function.
Program Definition function_ptr (fp : A fn_params) : rtype := {|
rty_type := loc;
rty f := {|
ty_own β l := ( fn, l `has_layout_loc` void_ptr l [β] val_of_loc f fntbl_entry f fn typed_function fn fp)%I;
ty_own β l := ( fn, l `has_layout_loc` void* l [β] val_of_loc f fntbl_entry f fn typed_function fn fp)%I;
|} |}.
Next Obligation. iDestruct 1 as (fn) "[? [H [? ?]]]". iExists _. iFrame. by iApply heap_mapsto_own_state_share. Qed.
Global Program Instance rmovable_function_ptr fp : RMovable (function_ptr fp) := {|
rmovable f := {|
ty_layout := void_ptr;
ty_layout := void*;
ty_own_val v := ( fn, v = val_of_loc f fntbl_entry f fn typed_function fn fp)%I;
|} |}.
Next Obligation. iIntros (? f l). by iDestruct 1 as (??) "?". Qed.
......
......@@ -8,7 +8,7 @@ Section own.
(* Separate definition such that we can make it typeclasses opaque later. *)
Program Definition frac_ptr_type (β : own_state) (ty : type) (l' : loc) : type := {|
ty_own β' l := (l `has_layout_loc` void_ptr l [β'] l' (l' ◁ₗ{own_state_min β' β} ty))%I;
ty_own β' l := (l `has_layout_loc` void* l [β'] l' (l' ◁ₗ{own_state_min β' β} ty))%I;
|}.
Next Obligation.
iIntros (β ?????) "($&Hl&H)". rewrite left_id.
......@@ -28,7 +28,7 @@ Section own.
Global Program Instance rmovable_frac_ptr β ty : RMovable (frac_ptr β ty) := {|
rmovable l := {|
ty_layout := void_ptr;
ty_layout := void*;
ty_own_val v := (v = val_of_loc l l ◁ₗ{β} ty)%I;
|} |}.
Next Obligation. iIntros (β ty l l'). by iDestruct 1 as (?) "_". Qed.
......@@ -58,7 +58,7 @@ Section own.
Lemma type_place_frac p β K β1 ty1 T l:
typed_place K p (own_state_min β1 β) ty1 (λ l2 β2 ty2 typ, T l2 β2 ty2 (λ t, (p @ (frac_ptr β (typ t))))) -
typed_place (DerefPCtx Na1Ord void_ptr :: K) l β1 (p @ (frac_ptr β ty1)) T.
typed_place (DerefPCtx Na1Ord void* :: K) l β1 (p @ (frac_ptr β ty1)) T.
Proof.
iIntros "HP" (Φ) "(%&Hm&Hl) HΦ" => /=.
iApply @fupd_wp. iMod (heap_mapsto_own_state_to_mt with "Hm") as (q Hq) "Hm" => //.
......@@ -70,7 +70,7 @@ Section own.
by iApply heap_mapsto_own_state_from_mt.
Qed.
Global Instance type_place_frac_inst p β K β1 ty1 l :
TypedPlace (DerefPCtx Na1Ord void_ptr :: K) l β1 (p @ (frac_ptr β ty1)) :=
TypedPlace (DerefPCtx Na1Ord void* :: K) l β1 (p @ (frac_ptr β ty1)) :=
λ T, i2p (type_place_frac _ _ _ _ _ _ _).
Lemma type_addr_of (T : val _) e:
......@@ -229,7 +229,7 @@ Section own.
( p1 p2, subsume P1 (v1 ◁ᵥ p1 @ frac_ptr Own (place p1)) (
subsume P2 (v2 ◁ᵥ p2 @ frac_ptr Own (place p2)) (
p, normalize_loc (p2.1, p1.2) p
T (val_of_loc p) (t2mt (value void_ptr (val_of_loc p)))))) -
T (val_of_loc p) (t2mt (value void* (val_of_loc p)))))) -
typed_copy_alloc_id v1 P1 v2 P2 T.
Proof.
iIntros "HT Hp1 Hp2" (Φ) "HΦ". iDestruct "HT" as (p1 p2) "HT".
......@@ -316,13 +316,13 @@ Section ptr.
Program Definition ptr : rtype := {|
rty_type := loc;
rty l' := {|
ty_own β l := (l `has_layout_loc` void_ptr l [β] l')%I;
ty_own β l := (l `has_layout_loc` void* l [β] l')%I;
|} |}.
Next Obligation. iIntros (????). iDestruct 1 as "[$ ?]". by iApply heap_mapsto_own_state_share. Qed.
Global Program Instance rmovable_ptr : RMovable ptr := {|
rmovable l := {|
ty_layout := void_ptr;
ty_layout := void*;
ty_own_val v := (v = val_of_loc l)%I;
|} |}.
Next Obligation. iIntros (l l'). by iDestruct 1 as (?) "_". Qed.
......@@ -374,7 +374,7 @@ Section ptr.
(* i2p (type_rounddown_ptr v1 v2 P2 T p). *)
Lemma simplify_ptr_hyp_place (p:loc) l T:
(l ◁ₗ value void_ptr (val_of_loc p) - T) -
(l ◁ₗ value void* (val_of_loc p) - T) -
simplify_hyp (l ◁ₗ p @ ptr) T.
Proof.
iIntros "HT [% Hl]". iApply "HT". by repeat iSplit.
......@@ -418,12 +418,12 @@ End ptr.
Section null.
Context `{!typeG Σ}.
Program Definition null : type := {|
ty_own β l := (l `has_layout_loc` void_ptr l [β] NULL)%I;
ty_own β l := (l `has_layout_loc` void* l [β] NULL)%I;
|}.
Next Obligation. iIntros (???). iDestruct 1 as "[$ ?]". by iApply heap_mapsto_own_state_share. Qed.
Global Program Instance movable_null : Movable null := {|
ty_layout := void_ptr;
ty_layout := void*;
ty_own_val v := v = NULL%I;
|}.
Next Obligation. by iIntros (?) "[% _]". Qed.
......
......@@ -104,7 +104,7 @@ Section value.
End value.
Notation "value< ly , v >" := (value ly v) (only printing, format "'value<' ly ',' v '>'") : printing_sugar.
Notation "value< v >" := (value void_ptr v) (only printing, format "'value<' v '>'") : printing_sugar.
Notation "value< v >" := (value void* v) (only printing, format "'value<' v '>'") : printing_sugar.
Section place.
Context `{!typeG Σ}.
......
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