Commit ed056390 authored by Hai Dang's avatar Hai Dang

fix build in lambda-rust-weak

parent 0de6e4af
Pipeline #33651 passed with stage
in 4 minutes
......@@ -338,6 +338,7 @@ End map_Difference.
Class Wellformed A := Wf : A Prop.
Existing Class Wf.
Hint Mode Wellformed ! : typeclass_instances.
Class WellformedPreserving `{Wellformed A} `{Wellformed B} (R : A B Prop) := {
wf_pre_proper a b : R a b Wf a Wf b;
......@@ -576,6 +577,7 @@ Global Instance lat_meet_bottom_rightabsorb_L `{!LeibnizEquiv Lat} `{!LatBottom
Proof. intros ?. solve_lat. Qed.
End Lat.
Hint Resolve lat_bottom_sqsubseteq : lat.
(** Lattice for product **)
......
......@@ -10,7 +10,8 @@ Class LocFacts (loc: Type) := {
loc_eqdec :> EqDecision loc;
loc_count :> Countable loc;
}.
Hint Mode LocFacts ! : typeclass_instances.
(* The next line is commented out to avoid TC divergence in lambda-rust-weak. *)
(* Hint Mode LocFacts ! : typeclass_instances. *)
Class Shift (loc: Type) := {
shift : loc Z loc;
......@@ -25,17 +26,17 @@ Notation "(>>)" := shift (only parsing) : stdpp_scope.
Notation "( l >>)" := (shift l) (only parsing) : stdpp_scope.
Arguments shift : simpl never.
Class StateFacts `{LocFacts loc} (state: Type) := {
Class StateFacts (loc state: Type) `{!LocFacts loc} := {
state_dom :> Dom state (gset loc);
state_wf :> Wellformed state;
state_dealloc : state gset loc;
state_dealloc_sub σ : state_dealloc σ dom (gset loc) σ;
}.
Arguments StateFacts _ {_} _.
(* Hint Mode StateFacts + + ! : typeclass_instances. *)
Arguments StateFacts _ _ {_}.
(* Hint Mode StateFacts ! ! : typeclass_instances. *)
Class Allocator `{StateFacts loc state} `{!Shift loc} := {
Class Allocator (loc state: Type)
`{!LocFacts loc} `{!StateFacts loc state} `{!Shift loc} := {
alloc : state nat loc Prop;
dealloc : state nat loc Prop;
alloc_add_fresh σ l n:
......@@ -46,7 +47,7 @@ Class Allocator `{StateFacts loc state} `{!Shift loc} := {
(n' : nat), n' < n
l >> n' (dom (gset _) σ state_dealloc σ);
}.
Arguments Allocator _ {_} _ {_ _}.
Arguments Allocator _ _ {_ _ _}.
Arguments alloc {_ _ _ _ _ _}.
Arguments dealloc {_ _ _ _ _ _}.
......@@ -211,11 +212,11 @@ Section LocBlock.
intros l Hn. constructor; [by assumption|].
intros i. apply (is_fresh_block _ i).
Qed.
End LocBlock.
Program Instance lblock_allocator `{!StateFacts lblock state}
: Allocator lblock state :=
{| alloc := lblock_alloc;
dealloc := lblock_dealloc; |}.
Next Obligation. intros ????? Hl ??. inversion Hl. by apply MAX. Qed.
Next Obligation. intros ????? Hl ??. inversion Hl. by apply ALLOC. Qed.
Global Program Instance lblock_allocator : Allocator lblock state :=
{| alloc := lblock_alloc;
dealloc := lblock_dealloc; |}.
Next Obligation. intros ??? Hl ??. inversion Hl. by apply MAX. Qed.
Next Obligation. intros ??? Hl ??. inversion Hl. by apply ALLOC. Qed.
End LocBlock.
......@@ -6,7 +6,7 @@ Section Memory.
Context `{!LocFacts loc} `{CVAL: Countable VAL}.
Notation val := (@val VAL).
Notation view := (view loc).
Notation view := (@view loc _).
Implicit Types (V: view).
(** Base messages do not have loc and to fields *)
......
......@@ -11,8 +11,8 @@ Section Wellformedness.
Notation global := (@global loc _ VAL).
Notation config := (@config loc _ VAL).
Notation val := (@val VAL).
Notation view := (view loc).
Notation threadView := (threadView loc).
Notation view := (@view loc _).
Notation threadView := (@threadView loc _).
Implicit Type (𝑚: message) (M: memory) (𝓝: view) (𝓥: threadView)
(l: loc) (G: global) (c: config).
......@@ -913,8 +913,8 @@ Section Steps.
Notation message := (message loc VAL).
Notation event := (event loc VAL).
Notation machine_step := (@machine_step _ _ VAL _ _).
Notation view := (view loc).
Notation threadView := (threadView loc).
Notation view := (@view loc _).
Notation threadView := (@threadView loc _).
Implicit Types (M: memory) (𝑚: message).
......
......@@ -10,8 +10,8 @@ Section Thread.
Notation memory := (memory loc VAL).
Notation message := (message loc VAL).
Notation event := (event loc VAL).
Notation view := (view loc).
Notation threadView := (threadView loc).
Notation view := (@view loc _).
Notation threadView := (@threadView loc).
Record global := mkGB {
sc: view;
......
......@@ -5,8 +5,7 @@ Set Default Proof Using "Type".
Section ThreadView.
Context `{!LocFacts loc} `{CVAL: Countable VAL}.
Notation view := (view loc).
Notation view_Lat := (view_Lat loc).
Notation view := (@view loc _).
Implicit Types (V: view).
Global Instance all_gmap_sqsubseteq_decision (M: gmap loc view) (V: option view) :
......@@ -530,6 +529,3 @@ Section ThreadView.
Qed.
End ThreadView.
Arguments threadView _ {_}.
Arguments tview_Lat _ {_}.
......@@ -75,7 +75,8 @@ Section View.
Context `{!LocFacts loc}.
Definition view := gmap loc timeInfo.
(* this is not canonical, as it overlaps [gmap_Lat]. This is to avoid TC divergence. *)
(* this is not canonical, as it overlaps [gmap_Lat].
This is to avoid TC divergence in lambda-rust-weak. *)
Canonical Structure view_Lat := gmap_Lat loc timeInfo_Lat.
Implicit Type (V: view).
......@@ -89,8 +90,8 @@ Section View.
Definition view_lookup_aread: Lookup loc time_ids view
:= fun l V => fmap taread (V !! l).
End View.
Arguments view _ {_}.
Arguments view_Lat _ {_}.
Arguments view {_ _}.
Arguments view_Lat {_ _}.
Notation "V !!w i" := (view_lookup_write i V) (at level 20) : stdpp_scope.
......@@ -100,7 +101,7 @@ Notation "V !!nr i" := (view_lookup_nread i V) (at level 20) : stdpp_scope.
Section ViewLookup.
Context `{!LocFacts loc}.
Implicit Types (V: view loc) (l : loc) (t: time).
Implicit Types (l : loc) (t: time).
Lemma view_lookup_w' V l o:
V !! l = o V !!w l = twrite <$> o.
......@@ -326,7 +327,7 @@ Tactic Notation "simplify_view":= repeat
end.
Lemma view_sqsubseteq `{!LocFacts loc} (V1 V2 : view loc) (l : loc) :
Lemma view_sqsubseteq `{!LocFacts loc} (V1 V2 : view) (l : loc) :
V1 !! l V2 !! l
V1 !!w l V2 !!w l V1 !!aw l V2 !!aw l
V1 !!nr l V2 !!nr l V1 !!ar l V2 !!ar l.
......
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