phanerozoic/Coq-Iris huggingface dataset:
(* iris_heap_lang/locations.v *)
Instance countable : Countable loc.
Proof. by apply (inj_countable' loc_car Loc); intros []. Defined.
(* iris_heap_lang/locations.v *)
Instance infinite : Infinite loc :=
    inj_infinite (λ p, {| loc_car := p |}) (λ l, Some (loc_car l)) _.
Next Obligation. done. Qed.
(* iris_heap_lang/locations.v *)
Definition add (l : loc) (off : Z) : loc
:=
    {| loc_car := loc_car l + off|}.
(* iris_heap_lang/locations.v *)
Definition le (l1 l2 : loc) : Prop
:= loc_car l1 ≤ loc_car l2.
(* iris_heap_lang/locations.v *)
Definition lt (l1 l2 : loc) : Prop
:= loc_car l1 < loc_car l2.
(* iris_heap_lang/locations.v *)
Notation "l +ₗ off"
:=
      (add l off) (at level 50, left associativity) : stdpp_scope.
(* iris_heap_lang/locations.v *)
Notation "l1 ≤ₗ l2"
:= (le l1 l2) (at level 70) : stdpp_scope.
(* iris_heap_lang/locations.v *)
Notation "l1 <ₗ l2"
:= (lt l1 l2) (at level 70) : stdpp_scope.
(* iris_heap_lang/locations.v *)
Lemma add_assoc l i j : l +ₗ i +ₗ j = l +ₗ (i + j).
Proof. rewrite eq_spec /=. lia. Qed.
(* iris_heap_lang/locations.v *)
Lemma add_0 l : l +ₗ 0 = l.
Proof. rewrite eq_spec /=; lia. Qed.
(* iris_heap_lang/locations.v *)
Instance add_inj l : Inj eq eq (add l).
Proof. intros x1 x2. rewrite eq_spec /=. lia. Qed.
(* iris_heap_lang/locations.v *)
Instance le_dec l1 l2 : Decision (l1 ≤ₗ l2).
Proof. rewrite /le. apply _. Qed.
(* iris_heap_lang/locations.v *)
Instance lt_dec l1 l2 : Decision (l1 <ₗ l2).
Proof. rewrite /lt. apply _. Qed.
(* iris_heap_lang/locations.v *)
Instance le_po : PartialOrder le.
Proof.
    rewrite /le. split; [split|].
    - by intros ?.
    - intros [x] [y] [z]; lia.
    - intros [x] [y] ??; f_equal/=; lia.
  Qed.
(* iris_heap_lang/locations.v *)
Instance le_total : Total le.
Proof. rewrite /Total /le. lia. Qed.
(* iris_heap_lang/locations.v *)
Lemma le_ngt l1 l2 : l1 ≤ₗ l2 ↔ ¬l2 <ₗ l1.
Proof. apply Z.le_ngt. Qed.
(* iris_heap_lang/locations.v *)
Lemma le_lteq l1 l2 : l1 ≤ₗ l2 ↔ l1 <ₗ l2 ∨ l1 = l2.
Proof. rewrite eq_spec. apply Z.le_lteq. Qed.
(* iris_heap_lang/locations.v *)
Lemma add_le_mono l1 l2 i1 i2 :
    l1 ≤ₗ l2 → i1 ≤ i2 → l1 +ₗ i1 ≤ₗ l2 +ₗ i2.
Proof. apply Z.add_le_mono. Qed.
(* iris_heap_lang/locations.v *)
Definition fresh (ls : gset loc) : loc
:=
    {| loc_car := set_fold (λ k r, (1 + loc_car k) `max` r) 1 ls |}.
(* iris_heap_lang/locations.v *)
Lemma fresh_fresh ls i : 0 ≤ i → fresh ls +ₗ i ∉ ls.
Proof.
    intros Hi. cut (∀ l, l ∈ ls → loc_car l < loc_car (fresh ls) + i).
    { intros help Hf%help. simpl in *. lia. }
    apply (set_fold_ind_L (λ r ls, ∀ l, l ∈ ls → (loc_car l < r + i)));
      set_solver by eauto with lia.
  Qed.
(* iris_heap_lang/metatheory.v *)
(* Adding a binder to a set of identifiers. *)
Definition set_binder_insert (x : binder) (X : stringset) : stringset
:=
  match x with
  | BAnon => X
  | BNamed f => {[f]} ∪ X
  end.
(* iris_heap_lang/metatheory.v *)
(* Check if expression [e] is closed w.r.t. the set [X] of variable names,
   and that all the values in [e] are closed *)
Fixpoint is_closed_expr (X : stringset) (e : expr) : bool
:=
  match e with
  | Val v => is_closed_val v
  | Var x => bool_decide (x ∈ X)
  | Rec f x e => is_closed_expr (set_binder_insert f (set_binder_insert x X)) e
  | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Free e | Load e =>
     is_closed_expr X e
  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | AllocN e1 e2 | Store e1 e2 | Xchg e1 e2 | FAA e1 e2 =>
     is_closed_expr X e1 && is_closed_expr X e2
  | If e0 e1 e2 | Case e0 e1 e2 | CmpXchg e0 e1 e2 | Resolve e0 e1 e2 =>
     is_closed_expr X e0 && is_closed_expr X e1 && is_closed_expr X e2
  | NewProph => true
  end
with is_closed_val (v : val) : bool :=
  match v with
  | LitV _ => true
  | RecV f x e => is_closed_expr (set_binder_insert f (set_binder_insert x ∅)) e
  | PairV v1 v2 => is_closed_val v1 && is_closed_val v2
  | InjLV v | InjRV v => is_closed_val v
  end.
(* iris_heap_lang/metatheory.v *)
(* Parallel substitution *)
Fixpoint subst_map (vs : gmap string val) (e : expr) : expr
:=
  match e with
  | Val _ => e
  | Var y => if vs !! y is Some v then Val v else Var y
  | Rec f y e => Rec f y (subst_map (binder_delete y (binder_delete f vs)) e)
  | App e1 e2 => App (subst_map vs e1) (subst_map vs e2)
  | UnOp op e => UnOp op (subst_map vs e)
  | BinOp op e1 e2 => BinOp op (subst_map vs e1) (subst_map vs e2)
  | If e0 e1 e2 => If (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
  | Pair e1 e2 => Pair (subst_map vs e1) (subst_map vs e2)
  | Fst e => Fst (subst_map vs e)
  | Snd e => Snd (subst_map vs e)
  | InjL e => InjL (subst_map vs e)
  | InjR e => InjR (subst_map vs e)
  | Case e0 e1 e2 => Case (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
  | Fork e => Fork (subst_map vs e)
  | AllocN e1 e2 => AllocN (subst_map vs e1) (subst_map vs e2)
  | Free e => Free (subst_map vs e)
  | Load e => Load (subst_map vs e)
  | Store e1 e2 => Store (subst_map vs e1) (subst_map vs e2)
  | Xchg e1 e2 => Xchg (subst_map vs e1) (subst_map vs e2)
  | CmpXchg e0 e1 e2 => CmpXchg (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
  | FAA e1 e2 => FAA (subst_map vs e1) (subst_map vs e2)
  | NewProph => NewProph
  | Resolve e0 e1 e2 => Resolve (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
  end.
(* iris_heap_lang/metatheory.v *)
(* Properties *)
Instance set_unfold_elem_of_insert_binder x y X Q :
  SetUnfoldElemOf y X Q →
  SetUnfoldElemOf y (set_binder_insert x X) (Q ∨ BNamed y = x).
Proof. destruct 1; constructor; destruct x; set_solver. Qed.
(* iris_heap_lang/metatheory.v *)
Lemma is_closed_weaken X Y e : is_closed_expr X e → X ⊆ Y → is_closed_expr Y e.
Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.
(* iris_heap_lang/metatheory.v *)
Lemma is_closed_weaken_empty X e : is_closed_expr ∅ e → is_closed_expr X e.
Proof. intros. by apply is_closed_weaken with ∅, empty_subseteq. Qed.
(* iris_heap_lang/metatheory.v *)
Lemma is_closed_subst X e y v :
  is_closed_val v →
  is_closed_expr ({[y]} ∪ X) e →
  is_closed_expr X (subst y v e).
Proof.
  intros Hv. revert X.
  induction e=> X /= ?; destruct_and?; split_and?; simplify_option_eq;
    try match goal with
    | H : ¬(_ ∧ _) |- _ => apply not_and_l in H as [?%dec_stable|?%dec_stable]
    end; eauto using is_closed_weaken with set_solver.
Qed.
(* iris_heap_lang/metatheory.v *)
Lemma is_closed_subst' X e x v :
  is_closed_val v →
  is_closed_expr (set_binder_insert x X) e →
  is_closed_expr X (subst' x v e).
Proof. destruct x; eauto using is_closed_subst. Qed.
(* iris_heap_lang/metatheory.v *)
Lemma subst_is_closed X e x es : is_closed_expr X e → x ∉ X → subst x es e = e.
Proof.
  revert X. induction e=> X /=;
   rewrite ?bool_decide_spec ?andb_True=> ??;
   repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver.
Qed.
(* iris_heap_lang/metatheory.v *)
Lemma subst_is_closed_empty e x v : is_closed_expr ∅ e → subst x v e = e.
Proof. intros. apply subst_is_closed with (∅:stringset); set_solver. Qed.
(* iris_heap_lang/metatheory.v *)
Lemma subst_subst e x v v' :
  subst x v (subst x v' e) = subst x v' e.
Proof.
  intros. induction e; simpl; try (f_equal; by auto);
    simplify_option_eq; auto using subst_is_closed_empty with f_equal.
Qed.
(* iris_heap_lang/metatheory.v *)
Lemma subst_subst' e x v v' :
  subst' x v (subst' x v' e) = subst' x v' e.
Proof. destruct x; simpl; auto using subst_subst. Qed.
(* iris_heap_lang/metatheory.v *)
Lemma subst_subst_ne e x y v v' :
  x ≠ y → subst x v (subst y v' e) = subst y v' (subst x v e).
Proof.
  intros. induction e; simpl; try (f_equal; by auto);
    simplify_option_eq; auto using eq_sym, subst_is_closed_empty with f_equal.
Qed.
(* iris_heap_lang/metatheory.v *)
Lemma subst_subst_ne' e x y v v' :
  x ≠ y → subst' x v (subst' y v' e) = subst' y v' (subst' x v e).
Proof. destruct x, y; simpl; auto using subst_subst_ne with congruence. Qed.
(* iris_heap_lang/metatheory.v *)
Lemma subst_rec' f y e x v :
  x = f ∨ x = y ∨ x = BAnon →
  subst' x v (Rec f y e) = Rec f y e.
Proof. intros. destruct x; simplify_option_eq; naive_solver. Qed.
(* iris_heap_lang/metatheory.v *)
Lemma subst_rec_ne' f y e x v :
  (x ≠ f ∨ f = BAnon) → (x ≠ y ∨ y = BAnon) →
  subst' x v (Rec f y e) = Rec f y (subst' x v e).
Proof. intros. destruct x; simplify_option_eq; naive_solver. Qed.
(* iris_heap_lang/metatheory.v *)
Lemma bin_op_eval_closed op v1 v2 v' :
  is_closed_val v1 → is_closed_val v2 → bin_op_eval op v1 v2 = Some v' →
  is_closed_val v'.
Proof.
  rewrite /bin_op_eval /bin_op_eval_bool /bin_op_eval_int /bin_op_eval_loc;
    repeat case_match; by naive_solver.
Qed.
(* iris_heap_lang/metatheory.v *)
Lemma heap_closed_alloc σ l n w :
  (0 < n)%Z →
  is_closed_val w →
  map_Forall (λ _ v, from_option is_closed_val true v) (heap σ) →
  (∀ i : Z, (0 ≤ i)%Z → (i < n)%Z → heap σ !! (l +ₗ i) = None) →
  map_Forall (λ _ v, from_option is_closed_val true v)
             (heap_array l (replicate (Z.to_nat n) w) ∪ heap σ).
Proof.
  intros Hn Hw Hσ Hl.
  eapply (map_Forall_ind
            (λ k v, ((heap_array l (replicate (Z.to_nat n) w) ∪ heap σ)
                       !! k = Some v))).
  - apply map_Forall_empty.
  - intros m i x Hi Hix Hkwm Hm.
    apply map_Forall_insert_2; auto.
    apply lookup_union_Some in Hix; last first.
    { eapply heap_array_map_disjoint;
        rewrite length_replicate Z2Nat.id; auto with lia. }
    destruct Hix as [(?&?&?&?&?&[-> Hlt%inj_lt]%lookup_replicate_1)%heap_array_lookup|
                     [j Hj]%elem_of_map_to_list%list_elem_of_lookup_1].
    + simplify_eq/=. rewrite !Z2Nat.id in Hlt; eauto with lia.
    + apply map_Forall_to_list in Hσ.
      by eapply Forall_lookup in Hσ; eauto; simpl in *.
  - apply map_Forall_to_list, Forall_forall.
    intros [? ?]; apply elem_of_map_to_list.
Qed.
(* iris_heap_lang/metatheory.v *)
(* The stepping relation preserves closedness *)
Lemma base_step_is_closed e1 σ1 obs e2 σ2 es :
  is_closed_expr ∅ e1 →
  map_Forall (λ _ v, from_option is_closed_val true v) σ1.(heap) →
  base_step e1 σ1 obs e2 σ2 es →
  is_closed_expr ∅ e2 ∧ Forall (is_closed_expr ∅) es ∧
  map_Forall (λ _ v, from_option is_closed_val true v) σ2.(heap).
Proof.
  intros Cl1 Clσ1 STEP.
  induction STEP; simpl in *; split_and!;
    try apply map_Forall_insert_2; try by naive_solver.
  - subst. repeat apply is_closed_subst'; naive_solver.
  - unfold un_op_eval in *. repeat case_match; naive_solver.
  - eapply bin_op_eval_closed; eauto; naive_solver.
  - by apply heap_closed_alloc.
  - select (_ !! _ = Some _) ltac:(fun H => by specialize (Clσ1 _ _ H)).
  - select (_ !! _ = Some _) ltac:(fun H => by specialize (Clσ1 _ _ H)).
  - select (_ !! _ = Some _) ltac:(fun H => by specialize (Clσ1 _ _ H)).
  - case_match; try apply map_Forall_insert_2; by naive_solver.
Qed.
(* iris_heap_lang/metatheory.v *)
Lemma subst_map_empty e : subst_map ∅ e = e.
Proof.
  assert (∀ x, binder_delete x (∅:gmap string val) = ∅) as Hdel.
  { intros [|x]; by rewrite /= ?delete_empty. }
  induction e; simplify_map_eq; rewrite ?Hdel; auto with f_equal.
Qed.
(* iris_heap_lang/metatheory.v *)
Lemma subst_map_insert x v vs e :
  subst_map (<[x:=v]>vs) e = subst x v (subst_map (delete x vs) e).
Proof.
  revert vs. induction e=> vs; simplify_map_eq; auto with f_equal.
  - match goal with
    | |- context [ <[?x:=_]> _ !! ?y ] =>
       destruct (decide (x = y)); simplify_map_eq=> //
    end. by case (vs !! _); simplify_option_eq.
  - destruct (decide _) as [[??]|[<-%dec_stable|[<-%dec_stable ?]]%not_and_l_alt].
    + rewrite !binder_delete_insert // !binder_delete_delete; eauto with f_equal.
    + by rewrite /= delete_insert_eq delete_delete_eq.
    + by rewrite /= binder_delete_insert // delete_insert_eq
        !binder_delete_delete delete_delete_eq.
Qed.
(* iris_heap_lang/metatheory.v *)
Lemma subst_map_singleton x v e :
  subst_map {[x:=v]} e = subst x v e.
Proof. by rewrite subst_map_insert delete_empty subst_map_empty. Qed.
(* iris_heap_lang/metatheory.v *)
Lemma subst_map_binder_insert b v vs e :
  subst_map (binder_insert b v vs) e =
  subst' b v (subst_map (binder_delete b vs) e).
Proof. destruct b; rewrite ?subst_map_insert //. Qed.
(* iris_heap_lang/metatheory.v *)
Lemma subst_map_binder_insert_empty b v e :
  subst_map (binder_insert b v ∅) e = subst' b v e.
Proof. by rewrite subst_map_binder_insert binder_delete_empty subst_map_empty. Qed.
(* iris_heap_lang/metatheory.v *)
Lemma subst_map_binder_insert_2 b1 v1 b2 v2 vs e :
  subst_map (binder_insert b1 v1 (binder_insert b2 v2 vs)) e =
  subst' b2 v2 (subst' b1 v1 (subst_map (binder_delete b2 (binder_delete b1 vs)) e)).
Proof.
  destruct b1 as [|s1], b2 as [|s2]=> /=; auto using subst_map_insert.
  rewrite subst_map_insert. destruct (decide (s1 = s2)) as [->|].
  - by rewrite delete_delete_eq subst_subst delete_insert_eq.
  - by rewrite delete_insert_ne // subst_map_insert subst_subst_ne.
Qed.
(* iris_heap_lang/metatheory.v *)
Lemma subst_map_binder_insert_2_empty b1 v1 b2 v2 e :
  subst_map (binder_insert b1 v1 (binder_insert b2 v2 ∅)) e =
  subst' b2 v2 (subst' b1 v1 e).
Proof.
  by rewrite subst_map_binder_insert_2 !binder_delete_empty subst_map_empty.
Qed.
(* iris_heap_lang/metatheory.v *)
Lemma subst_map_is_closed X e vs :
  is_closed_expr X e →
  (∀ x, x ∈ X → vs !! x = None) →
  subst_map vs e = e.
Proof.
  revert X vs. assert (∀ x x1 x2 X (vs : gmap string val),
    (∀ x, x ∈ X → vs !! x = None) →
    x ∈ set_binder_insert x2 (set_binder_insert x1 X) →
    binder_delete x1 (binder_delete x2 vs) !! x = None).
  { intros x x1 x2 X vs ??. rewrite !lookup_binder_delete_None. set_solver. }
  induction e=> X vs /= ? HX; repeat case_match; naive_solver eauto with f_equal.
Qed.
(* iris_heap_lang/metatheory.v *)
Lemma subst_map_is_closed_empty e vs : is_closed_expr ∅ e → subst_map vs e = e.
Proof. intros. apply subst_map_is_closed with (∅ : stringset); set_solver. Qed.
(* iris_heap_lang/notation.v *)
(* Coercions to make programs easier to type. *)
Coercion LitInt : Z >-> base_lit.
(* iris_heap_lang/notation.v *)
Coercion LitBool : bool >-> base_lit.
(* iris_heap_lang/notation.v *)
Coercion LitLoc : loc >-> base_lit.
(* iris_heap_lang/notation.v *)
Coercion LitProphecy : proph_id >-> base_lit.
(* iris_heap_lang/notation.v *)
Coercion App : expr >-> Funclass.
(* iris_heap_lang/notation.v *)
Coercion Val : val >-> expr.
(* iris_heap_lang/notation.v *)
Coercion Var : string >-> expr.
(* iris_heap_lang/notation.v *)
(* Define some derived forms. *)
Notation Lam x e
:= (Rec BAnon x e) (only parsing).
(* iris_heap_lang/notation.v *)
Notation Let x e1 e2
:= (App (Lam x e2) e1) (only parsing).
(* iris_heap_lang/notation.v *)
Notation Seq e1 e2
:= (Let BAnon e1 e2) (only parsing).
(* iris_heap_lang/notation.v *)
Notation LamV x e
:= (RecV BAnon x e) (only parsing).
(* iris_heap_lang/notation.v *)
Notation LetCtx x e2
:= (AppRCtx (LamV x e2)) (only parsing).
(* iris_heap_lang/notation.v *)
Notation SeqCtx e2
:= (LetCtx BAnon e2) (only parsing).
(* iris_heap_lang/notation.v *)
Notation Match e0 x1 e1 x2 e2
:= (Case e0 (Lam x1 e1) (Lam x2 e2)) (only parsing).
(* iris_heap_lang/notation.v *)
Notation Alloc e
:= (AllocN (Val $ LitV $ LitInt 1) e) (only parsing).
(* iris_heap_lang/notation.v *)
(* Compare-and-set (CAS) returns just a boolean indicating success or failure. *)
Notation CAS l e1 e2
:= (Snd (CmpXchg l e1 e2)) (only parsing).
(* iris_heap_lang/notation.v *)
(* Skip should be atomic, we sometimes open invariants around
   it. Hence, we need to explicitly use LamV instead of e.g., Seq. *)
Notation Skip
:= (App (Val $ LamV BAnon (Val $ LitV LitUnit)) (Val $ LitV LitUnit)).
(* iris_heap_lang/notation.v *)
(* No scope for the values, does not conflict and scope is often not inferred
properly. *)
Notation "# l"
:= (LitV l%Z%V%stdpp) (at level 8, format "# l").
(* iris_heap_lang/notation.v *)
(* Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
    first. *)
Notation "( e1 , e2 , .. , en )"
:= (Pair .. (Pair e1 e2) .. en) : expr_scope.
(* iris_heap_lang/notation.v *)
Notation "( e1 , e2 , .. , en )"
:= (PairV .. (PairV e1 e2) .. en) : val_scope.
(* iris_heap_lang/notation.v *)
(* Using the '[hv' ']' printing box, we make sure that when the notation for match
does not fit on a single line, line breaks will be inserted for *each* breaking
point '/'. Note that after each breaking point /, one can put n spaces (for
example '/  '). That way, when the breaking point is turned into a line break,
indentation of n spaces will appear after the line break. As such, when the
match does not fit on one line, it will print it like:

  match: e0 with
    InjL x1 => e1
  | InjR x2 => e2
  end

Moreover, if the branches do not fit on a single line, it will be printed as:

  match: e0 with
    InjL x1 =>
    lots of stuff bla bla bla bla bla bla bla bla
  | InjR x2 =>
    even more stuff bla bla bla bla bla bla bla bla
  end *)
Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'"
:=
  (Match e0 x1%binder e1 x2%binder e2)
  (e0, x1, e1, x2, e2 at level 200,
   format "'[hv' 'match:'  e0  'with'  '/  ' '[' 'InjL'  x1  =>  '/  ' e1 ']'  '/' '[' |  'InjR'  x2  =>  '/  ' e2 ']'  '/' 'end' ']'") : expr_scope.
(* iris_heap_lang/notation.v *)
Notation "'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'"
:=
  (Match e0 x2%binder e2 x1%binder e1)
  (e0, x1, e1, x2, e2 at level 200, only parsing) : expr_scope.
(* iris_heap_lang/notation.v *)
Notation "()"
:= LitUnit : val_scope.
(* iris_heap_lang/notation.v *)
Notation "! e"
:= (Load e%E) (at level 9, right associativity) : expr_scope.
(* iris_heap_lang/notation.v *)
Notation "'ref' e"
:= (Alloc e%E) (at level 10) : expr_scope.
(* iris_heap_lang/notation.v *)
Notation "- e"
:= (UnOp MinusUnOp e%E) : expr_scope.
(* iris_heap_lang/notation.v *)
Notation "e1 + e2"
:= (BinOp PlusOp e1%E e2%E) : expr_scope.
(* iris_heap_lang/notation.v *)
Notation "e1 +ₗ e2"
:= (BinOp OffsetOp e1%E e2%E) : expr_scope.
(* iris_heap_lang/notation.v *)
Notation "e1 - e2"
:= (BinOp MinusOp e1%E e2%E) : expr_scope.
(* iris_heap_lang/notation.v *)
Notation "e1 * e2"
:= (BinOp MultOp e1%E e2%E) : expr_scope.
(* iris_heap_lang/notation.v *)
Notation "e1 `quot` e2"
:= (BinOp QuotOp e1%E e2%E) : expr_scope.
(* iris_heap_lang/notation.v *)
Notation "e1 `rem` e2"
:= (BinOp RemOp e1%E e2%E) : expr_scope.
(* iris_heap_lang/notation.v *)
Notation "e1 ≪ e2"
:= (BinOp ShiftLOp e1%E e2%E) : expr_scope.
(* iris_heap_lang/notation.v *)
Notation "e1 ≫ e2"
:= (BinOp ShiftROp e1%E e2%E) : expr_scope.
(* iris_heap_lang/notation.v *)
Notation "e1 ≤ e2"
:= (BinOp LeOp e1%E e2%E) : expr_scope.
(* iris_heap_lang/notation.v *)
Notation "e1 < e2"
:= (BinOp LtOp e1%E e2%E) : expr_scope.
(* iris_heap_lang/notation.v *)
Notation "e1 = e2"
:= (BinOp EqOp e1%E e2%E) : expr_scope.
(* iris_heap_lang/notation.v *)
Notation "e1 ≠ e2"
:= (UnOp NegOp (BinOp EqOp e1%E e2%E)) : expr_scope.
(* iris_heap_lang/notation.v *)
Notation "~ e"
:= (UnOp NegOp e%E) (at level 75, right associativity) : expr_scope.
(* iris_heap_lang/notation.v *)
(* The unicode ← is already part of the notation "_ ← _; _" for bind. *)
Notation "e1 <- e2"
:= (Store e1%E e2%E) (at level 80) : expr_scope.
(* iris_heap_lang/notation.v *)
(* The breaking point '/  ' makes sure that the body of the rec is indented
by two spaces in case the whole rec does not fit on a single line. *)
Notation "'rec:' f x := e"
:= (Rec f%binder x%binder e%E)
  (at level 200, f at level 1, x at level 1, e at level 200,
   format "'[' 'rec:'  f  x  :=  '/  ' e ']'") : expr_scope.
(* iris_heap_lang/notation.v *)
Notation "'rec:' f x := e"
:= (RecV f%binder x%binder e%E)
  (at level 200, f at level 1, x at level 1, e at level 200,
   format "'[' 'rec:'  f  x  :=  '/  ' e ']'") : val_scope.
(* iris_heap_lang/notation.v *)
Notation "'if:' e1 'then' e2 'else' e3"
:= (If e1%E e2%E e3%E)
  (at level 200, e1, e2, e3 at level 200) : expr_scope.
(* iris_heap_lang/notation.v *)
(* Derived notions, in order of declaration. The notations for let and seq
are stated explicitly instead of relying on the Notations Let and Seq as
defined above. This is needed because App is now a coercion, and these
notations are otherwise not pretty printed back accordingly. *)
Notation "'rec:' f x y .. z := e"
:= (Rec f%binder x%binder (Lam y%binder .. (Lam z%binder e%E) ..))
  (at level 200, f, x, y, z at level 1, e at level 200,
   format "'[' 'rec:'  f  x  y  ..  z  :=  '/  ' e ']'") : expr_scope.
(* iris_heap_lang/notation.v *)
Notation "'rec:' f x y .. z := e"
:= (RecV f%binder x%binder (Lam y%binder .. (Lam z%binder e%E) ..))
  (at level 200, f, x, y, z at level 1, e at level 200,
   format "'[' 'rec:'  f  x  y  ..  z  :=  '/  ' e ']'") : val_scope.
(* iris_heap_lang/notation.v *)
(* The breaking point '/  ' makes sure that the body of the λ: is indented
by two spaces in case the whole λ: does not fit on a single line. *)
Notation "λ: x , e"
:= (Lam x%binder e%E)
  (at level 200, x at level 1, e at level 200,
   format "'[' 'λ:'  x ,  '/  ' e ']'") : expr_scope.
(* iris_heap_lang/notation.v *)
Notation "λ: x y .. z , e"
:= (Lam x%binder (Lam y%binder .. (Lam z%binder e%E) ..))
  (at level 200, x, y, z at level 1, e at level 200,
   format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : expr_scope.
(* iris_heap_lang/notation.v *)
Notation "λ: x , e"
:= (LamV x%binder e%E)
  (at level 200, x at level 1, e at level 200,
   format "'[' 'λ:'  x ,  '/  ' e ']'") : val_scope.
(* iris_heap_lang/notation.v *)
Notation "λ: x y .. z , e"
:= (LamV x%binder (Lam y%binder .. (Lam z%binder e%E) .. ))
  (at level 200, x, y, z at level 1, e at level 200,
   format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : val_scope.
(* iris_heap_lang/notation.v *)
Notation "'let:' x := e1 'in' e2"
:= (Lam x%binder e2%E e1%E)
  (at level 200, x at level 1, e1, e2 at level 200,
   format "'[' 'let:'  x  :=  '[' e1 ']'  'in'  '/' e2 ']'") : expr_scope.
(* iris_heap_lang/notation.v *)
Notation "e1 ;; e2"
:= (Lam BAnon e2%E e1%E)
  (at level 100, e2 at level 200,
   format "'[' '[hv' '[' e1 ']' ;;  ']' '/' e2 ']'") : expr_scope.
(* iris_heap_lang/notation.v *)
(* Shortcircuit Boolean connectives *)
Notation "e1 && e2"
:=
  (If e1%E e2%E (LitV (LitBool false))) (only parsing) : expr_scope.
(* iris_heap_lang/notation.v *)
Notation "e1 || e2"
:=
  (If e1%E (LitV (LitBool true)) e2%E) (only parsing) : expr_scope.
(* iris_heap_lang/notation.v *)
(* Notations for option *)
Notation NONE
:= (InjL (LitV LitUnit)) (only parsing).
(* iris_heap_lang/notation.v *)
Notation NONEV
:= (InjLV (LitV LitUnit)) (only parsing).
(* iris_heap_lang/notation.v *)
Notation SOME x
:= (InjR x) (only parsing).
(* iris_heap_lang/notation.v *)
Notation SOMEV x
:= (InjRV x) (only parsing).
(* iris_heap_lang/notation.v *)
Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'"
:=
  (Match e0 BAnon e1 x%binder e2)
  (e0, e1, x, e2 at level 200, only parsing) : expr_scope.
(* iris_heap_lang/notation.v *)
Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'"
:=
  (Match e0 BAnon e1 x%binder e2)
  (e0, e1, x, e2 at level 200, only parsing) : expr_scope.
(* iris_heap_lang/notation.v *)
Notation ResolveProph e1 e2
:= (Resolve Skip e1 e2) (only parsing).
(* iris_heap_lang/notation.v *)
(* Level 99 so that it works to the left of a `;;` which is at level 100. *)
Notation "'resolve_proph:' p 'to:' v"
:= (ResolveProph p v) (at level 99) : expr_scope.
(* iris_heap_lang/pretty.v *)
(* * Pretty printing for HeapLang values *)
Instance pretty_loc : Pretty loc
:=
  λ l, pretty l.(loc_car).
(* iris_heap_lang/pretty.v *)
Instance pretty_base_lit : Pretty base_lit
:=
  λ l, match l with
       | LitInt z => pretty z
       | LitBool b => if b then "true" else "false"
       | LitUnit => "()"
       | LitPoison => "<poison>"
       | LitLoc l => "(loc " +:+ pretty l +:+ ")"
       | LitProphecy i => "(prophecy " +:+ pretty i +:+ ")"
       end.
(* iris_heap_lang/pretty.v *)
Instance pretty_binder : Pretty binder
:=
  λ b, match b with
       | BNamed x => x
       | BAnon => "<>"
       end.