classes.v 2.07 KB
Newer Older
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
1 2 3 4 5 6 7 8 9 10
From iris.algebra Require Export upred.
Import uPred.

Section classes.
Context {M : ucmraT}.
Implicit Types P Q : uPred M.

Class FromAssumption (p : bool) (P Q : uPred M) := from_assumption : ?p P  Q.
Global Arguments from_assumption _ _ _ {_}.

11 12 13 14 15
Class IntoPure (P : uPred M) (φ : Prop) := into_pure : P   φ.
Global Arguments into_pure : clear implicits.

Class FromPure (P : uPred M) (φ : Prop) := from_pure : φ  True  P.
Global Arguments from_pure : clear implicits.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
16 17 18 19 20 21

Class IntoPersistentP (P Q : uPred M) := into_persistentP : P   Q.
Global Arguments into_persistentP : clear implicits.

Class IntoLater (P Q : uPred M) := into_later : P   Q.
Global Arguments into_later _ _ {_}.
22

Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
23 24 25 26 27 28 29 30 31 32 33 34 35 36
Class FromLater (P Q : uPred M) := from_later :  Q  P.
Global Arguments from_later _ _ {_}.

Class IntoWand (R P Q : uPred M) := into_wand : R  P - Q.
Global Arguments into_wand : clear implicits.

Class FromAnd (P Q1 Q2 : uPred M) := from_and : Q1  Q2  P.
Global Arguments from_and : clear implicits.

Class FromSep (P Q1 Q2 : uPred M) := from_sep : Q1  Q2  P.
Global Arguments from_sep : clear implicits.

Class IntoSep (p: bool) (P Q1 Q2 : uPred M) := into_sep : ?p P  ?p (Q1  Q2).
Global Arguments into_sep : clear implicits.
37

Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56
Class IntoOp {A : cmraT} (a b1 b2 : A) := into_op : a  b1  b2.
Global Arguments into_op {_} _ _ _ {_}.

Class Frame (R P Q : uPred M) := frame : R  Q  P.
Global Arguments frame : clear implicits.

Class FromOr (P Q1 Q2 : uPred M) := from_or : Q1  Q2  P.
Global Arguments from_or : clear implicits.

Class IntoOr P Q1 Q2 := into_or : P  Q1  Q2.
Global Arguments into_or : clear implicits.

Class FromExist {A} (P : uPred M) (Φ : A  uPred M) :=
  from_exist : ( x, Φ x)  P.
Global Arguments from_exist {_} _ _ {_}.

Class IntoExist {A} (P : uPred M) (Φ : A  uPred M) :=
  into_exist : P   x, Φ x.
Global Arguments into_exist {_} _ _ {_}.
57 58

Class TimelessElim (Q : uPred M) :=
59
  timeless_elim `{!TimelessP P} :  P  (P - Q)  Q.
60
Global Arguments timeless_elim _ {_} _ {_}.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
61
End classes.