Commit 0de6e4af authored by Hai Dang's avatar Hai Dang

fix build for 8.11.2

parent 40a7d770
Pipeline #33611 passed with stage
in 3 minutes and 59 seconds
......@@ -46,7 +46,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 {_ _ _ _ _ _}.
......@@ -133,18 +133,15 @@ Section LocPos.
by apply is_fresh_pos_block.
Qed.
End LocPos.
Program Instance pos_allocator `{!StateFacts positive state}
: Allocator state :=
{| alloc := pos_alloc;
Global Program Instance pos_allocator : Allocator positive state :=
{| alloc := pos_alloc;
dealloc := pos_dealloc; |}.
Next Obligation. intros ????? ALL. inversion ALL. by apply NEW. Qed.
Next Obligation.
intros ????? DEL ? Lt. inversion DEL. subst. apply Nat.lt_1_r in Lt. subst.
by apply ALLOC.
Qed.
Next Obligation. intros ??? ALL. inversion ALL. by apply NEW. Qed.
Next Obligation.
intros ??? DEL ? Lt. inversion DEL. subst. apply Nat.lt_1_r in Lt. subst.
by apply ALLOC.
Qed.
End LocPos.
(** Locations as blocks *)
......@@ -214,11 +211,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 state :=
{| alloc := lblock_alloc;
dealloc := lblock_dealloc; |}.
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.
......@@ -1249,7 +1249,7 @@ Section Memory.
Qed.
Section Allocation.
Context `{!Shift loc} `{!Allocator memory}.
Context `{!Shift loc} `{!Allocator loc memory}.
(** Allocation *)
Inductive memory_alloc
(n : nat) l 𝑚s M1 M2 : Prop :=
......@@ -1588,7 +1588,7 @@ Section Memory.
by rewrite (lookup_seq_ge _ _ _ Ge) /=.
Qed.
Lemma memory_alloc_cell_list `{!Allocator memory} n l 𝑚s M1 M2
Lemma memory_alloc_cell_list `{!Allocator loc memory} n l 𝑚s M1 M2
(ALLOC: memory_alloc n l 𝑚s M1 M2):
(n': nat) C,
(cell_list l n M2) !! n' = Some C
......@@ -1615,7 +1615,7 @@ Section Memory.
by eexists.
Qed.
Lemma memory_alloc_cell_list_map `{!Allocator memory} n l 𝑚s M1 M2
Lemma memory_alloc_cell_list_map `{!Allocator loc memory} n l 𝑚s M1 M2
(ALLOC: memory_alloc n l 𝑚s M1 M2):
(cell_list l n M2) = fmap (λ 𝑚, {[𝑚.(mto) := 𝑚.(mbase)]}) 𝑚s.
Proof.
......@@ -1843,7 +1843,7 @@ Section Memory.
lookup_empty // in IN.
Qed.
Lemma mem_cut_memory_alloc `{!Shift loc} `{!Allocator memory} l n M1 M2 𝑚s 𝓝
Lemma mem_cut_memory_alloc `{!Shift loc} `{!Allocator loc memory} l n M1 M2 𝑚s 𝓝
(ALLOC: memory_alloc n l 𝑚s M1 M2) :
mem_cut M2 (alloc_new_na 𝓝 𝑚s) = alloc_new_mem (mem_cut M1 𝓝) 𝑚s.
Proof.
......@@ -1852,7 +1852,7 @@ Section Memory.
- by eapply memory_alloc_fresh_2.
Qed.
Lemma mem_cut_memory_dealloc `{!Shift loc} `{!Allocator memory} l n M1 M2 𝑚s 𝓝
Lemma mem_cut_memory_dealloc `{!Shift loc} `{!Allocator loc memory} l n M1 M2 𝑚s 𝓝
(DEALLOC: memory_dealloc n l 𝑚s M1 M2) :
mem_cut M2 (alloc_new_na 𝓝 𝑚s) = alloc_new_mem (mem_cut M1 𝓝) 𝑚s.
Proof.
......
......@@ -3,7 +3,7 @@ From orc11 Require Export thread.
Set Default Proof Using "Type".
Section Wellformedness.
Context `{!LocFacts loc} `{CVAL: Countable VAL} `{!Shift loc} `{!Allocator (memory loc VAL)}.
Context `{!LocFacts loc} `{CVAL: Countable VAL} `{!Shift loc} `{!Allocator loc (memory loc VAL)}.
Notation memory := (memory loc VAL).
Notation message := (message loc VAL).
......@@ -486,7 +486,7 @@ End Wellformedness.
Section AllocSteps.
Context `{!LocFacts loc} `{CVAL: Countable VAL} `{!Shift loc} `{!Allocator (memory loc VAL)}.
Context `{!LocFacts loc} `{CVAL: Countable VAL} `{!Shift loc} `{!Allocator loc (memory loc VAL)}.
Notation memory := (memory loc VAL).
Notation message := (message loc VAL).
......@@ -907,7 +907,7 @@ Section AllocSteps.
End AllocSteps.
Section Steps.
Context `{!LocFacts loc} `{CVAL: Countable VAL} `{!Shift loc} `{!Allocator (memory loc VAL)}.
Context `{!LocFacts loc} `{CVAL: Countable VAL} `{!Shift loc} `{!Allocator loc (memory loc VAL)}.
Notation memory := (memory loc VAL).
Notation message := (message loc VAL).
......
......@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
Section Thread.
Context `{!LocFacts loc} `{CVAL: Countable VAL} `{!Shift loc} `{!Allocator (memory loc VAL)}.
Context `{!LocFacts loc} `{CVAL: Countable VAL} `{!Shift loc} `{!Allocator loc (memory loc VAL)}.
Notation memory := (memory loc VAL).
Notation message := (message loc VAL).
......
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