Merge remote-tracking branch 'mpi/v2.0' into v2.0

SConstruct

@@ -2,7 +2,7 @@
 # This file is distributed under the terms of the BSD license.
 import os, glob, string
 
-modules = ["prelude", "modures", "iris"]
+modules = ["prelude", "modures", "iris", "barrier"]
 Rs = '-Q . ""'
 env = DefaultEnvironment(ENV = os.environ,tools=['default', 'Coq'], COQFLAGS=Rs)
 

channel/heap_lang.v → barrier/heap_lang.v

 Require Import Autosubst.Autosubst.
-Require Import prelude.option prelude.gmap iris.language.
+Require Import prelude.option prelude.gmap iris.language iris.parameter.
 
 Set Bullet Behavior "Strict Subproofs".
 
@@ -318,7 +318,7 @@ Proof.
     exists K''; by eauto using f_equal, f_equal2, f_equal3, v2e_inj.
 
   intros Hfill Hred Hnval. 
-  Time revert K' Hfill; induction K=>K' /= Hfill;
+  revert K' Hfill; induction K=>K' /= Hfill;
     first (now eexists; reflexivity);
     (destruct K'; simpl;
       (* The first case is: K' is EmpyCtx. *)
@@ -408,12 +408,7 @@ Section Language.
   Definition ectx_step e1 σ1 e2 σ2 (ef: option expr) :=
     exists K e1' e2', e1 = fill K e1' /\ e2 = fill K e2' /\ prim_step e1' σ1 e2' σ2 ef.
 
-  Instance heap_lang : Language expr value state := {|
-    of_val := v2e;
-    to_val := e2v;
-    atomic := atomic;
-    prim_step := ectx_step
-  |}.
+  Instance heap_lang : Language expr value state := Build_Language v2e e2v atomic ectx_step.
   Proof.
     - exact v2v.
     - exact e2e.
@@ -431,7 +426,7 @@ Section Language.
   Lemma fill_is_ctx K: is_ctx (fill K).
   Proof.
     split.
-    - intros ? [v Hval]. eapply fill_value. eassumption.
+    - intros ? Hnval. by eapply fill_not_value.
     - intros ? ? ? ? ? (K' & e1' & e2' & Heq1 & Heq2 & Hstep).
       exists (comp_ctx K K'), e1', e2'. rewrite -!fill_comp Heq1 Heq2.
       split; last split; reflexivity || assumption.
@@ -445,3 +440,9 @@ Section Language.
   Qed.
 
 End Language.
+
+(* This is just to demonstrate that we can instantiate IParam. *)
+Module IParam.
+  Definition Σ := IParamConst heap_lang unitRA.
+  Print Assumptions Σ.
+End IParam.

iris/language.v

@@ -14,6 +14,7 @@ Class Language (E V St : Type) := {
     prim_step e1 σ1 e2 σ2 ef →
     is_Some (to_val e2)
 }.
+Arguments Build_Language {_ _ _} _ _ _ _ {_ _ _ _ _}.
 
 Section language.
   Context `{Language E V St}.

iris/parameter.v

 Require Export modures.cmra iris.language.
 
+Set Bullet Behavior "Strict Subproofs".
+
 Record iParam := IParam {
   iexpr : Type;
   ival : Type;
   istate : Type;
-  icmra : cofeT → cmraT;
   ilanguage : Language iexpr ival istate;
+  icmra : cofeT → cmraT;
   icmra_empty A : Empty (icmra A);
   icmra_empty_spec A : RAIdentity (icmra A);
   icmra_empty_timeless A : Timeless (∅ : icmra A);
@@ -16,6 +18,7 @@ Record iParam := IParam {
     icmra_map (g ◎ f) x ≡ icmra_map g (icmra_map f x);
   icmra_map_mono {A B} (f : A -n> B) : CMRAMonotone (icmra_map f)
 }.
+Arguments IParam {_ _ _} ilanguage icmra {_ _ _} _ {_ _ _ _}.
 Existing Instances ilanguage.
 Existing Instances icmra_empty icmra_empty_spec icmra_empty_timeless.
 Existing Instances icmra_map_ne icmra_map_mono.
@@ -26,4 +29,15 @@ Proof.
   by intros ?; apply equiv_dist=> n; apply icmra_map_ne=> ?; apply equiv_dist.
 Qed.
 
-Canonical Structure istateC Σ := leibnizC (istate Σ).
\ No newline at end of file
+Definition IParamConst {iexpr ival istate : Type}
+           (ilanguage : Language iexpr ival istate)
+           (icmra : cmraT) {icmra_empty : Empty icmra}
+           {icmra_empty_spec : RAIdentity icmra} {icmra_empty_timeless: Timeless (∅ : icmra)}:
+  iParam.
+eapply (IParam ilanguage (fun _ => icmra) (fun _ _ _ => cid)).
+Unshelve.
+- by intros.
+- by intros.
+Defined.
+
+Canonical Structure istateC Σ := leibnizC (istate Σ).

modures/cmra.v

@@ -307,6 +307,9 @@ Section discrete.
 End discrete.
 Arguments discreteRA _ {_ _ _ _ _ _}.
 
+(** CMRA for the unit type *)
+Canonical Structure unitRA : cmraT := discreteRA ().
+
 (** Product *)
 Section prod.
   Context {A B : cmraT}.

modures/ra.v

@@ -238,3 +238,21 @@ Ltac solve_included :=
   ra_reflection.quote;
   apply ra_reflection.flatten_correct, (bool_decide_unpack _);
   vm_compute; apply I.
+
+(** An RA for the unit type *)
+Instance unit_valid : Valid () := λ x, True.
+Instance unit_unit : Unit () := λ x, x.
+Instance unit_op : Op () := λ x y, tt.
+Instance unit_minus : Minus () := λ x y, tt.
+
+Instance unit_ra : RA ().
+Proof.
+  split; done.
+Qed.
+
+
+Instance unit_empty : Empty () := tt.
+Instance unit_empty_ra : RAIdentity().
+Proof.
+  split; done.
+Qed.