Fix Notation with Var coercion problem

theories/examples/lock/code_ticket_lock.v

@@ -19,7 +19,7 @@ Section code.
       let: "i"  := !ʳˡˣ "x" in
       let: "i'" := ("i" + #1) `mod` #(Z.pos C) in
         if: casʳᵃ("x", "i", "i'")
-        then (Var "i") (* TODO: coercion *)
+        then "i"
         else "FAI" ["x"]
     .
 

theories/examples/queue/code_ms.v

 From gpfsl.lang Require Export notation.
 From gpfsl.logic Require Import repeat_loop new_delete.
 
+Require Import iris.prelude.options.
+
 Notation link := 0 (only parsing).
 Notation data := 1 (only parsing).
 Notation head := 0 (only parsing).
@@ -25,7 +27,7 @@ Definition find_tail : val :=
     let: "n"  := !ᵃᶜ ("q" +ₗ #tail) in
     let: "n'" := !ᵃᶜ ("n" +ₗ #link) in
       if: "n'" = #null
-      then (Var "n") (* TODO: problem with coercion Var *)
+      then "n"
       else
         "q" +ₗ #tail <-ʳᵉˡ "n'" ;;
         #false
@@ -65,7 +67,10 @@ Definition try_deq : val :=
 Definition dequeue : val :=
   rec: "try" ["q"] :=
     let: "n" := try_deq ["q"] in
+      (* FIXME: our language doesn't have comparison for arbitrary literals, so
+        the next line is limited to integer comparison, which means that
+        the queue is only intended for use with integers. *)
       if: #EMPTY ≤ "n"
-      then (Var "n") (* TODO: problem with coercion Var *)
+      then "n"
       else "try" ["q"]
   .

theories/examples/stack/code_treiber.v

@@ -74,5 +74,5 @@ Definition pop : val :=
     let: "v" := try_pop ["s"] in
     if: "v" = #FAIL_RACE
     then "try" ["s"]
-    else (Var "v")
+    else "v"
   .

theories/lang/lang.v

+From stdpp Require Export binders strings.
 From iris.program_logic Require Export language ectx_language ectxi_language.
-From stdpp Require Export strings binders gmap.
 From iris.algebra Require Import ofe.
+
 From orc11 Require Export progress.
 
+Require Import iris.prelude.options.
+
 (* Note: We consider that reading uninitialized memory can return poison.
    This is not what Rust does, but LLVM considers that reading
    from undefined memory returns the undef value.
@@ -10,8 +13,6 @@ From orc11 Require Export progress.
    https://doc.rust-lang.org/std/mem/fn.uninitialized.html#undefined-behavior
 *)
 
-Require Import iris.prelude.options.
-
 (** Locations **)
 Notation loc := lblock.
 
@@ -33,14 +34,6 @@ Inductive un_op := | NegOp | MinusUnOp.
 
 Inductive bin_op := | PlusOp | MinusOp | ModOp | LeOp | LtOp | EqOp | OffsetOp.
 
-Notation "[ ]" := (@nil binder) : binder_scope.
-Notation "a :: b" := (@cons binder a%binder b%binder)
-  (at level 60, right associativity) : binder_scope.
-Notation "[ x1 ; x2 ; .. ; xn ]" :=
-  (@cons binder x1%binder (@cons binder x2%binder
-        (..(@cons binder xn%binder (@nil binder))..))) : binder_scope.
-Notation "[ x ]" := (@cons binder x%binder (@nil binder)) : binder_scope.
-
 Module base.
   (** Base expression language without views *)
   Inductive expr :=
@@ -686,16 +679,6 @@ Module base.
     | Fork _ | FenceRel | FenceAcq | FenceSC => True
     | _ => False
     end.
-
-  (* Some derived forms *)
-  Notation Lam xl e := (Rec BAnon xl e).
-  Notation Let x e1 e2 := (App (Lam [x] e2) [e1]).
-  Notation Seq e1 e2 := (Let BAnon e1 e2).
-  Notation LamV xl e := (RecV BAnon xl e).
-  Notation LetCtx x e2 := (AppRCtx (LamV [x] e2) [] []).
-  Notation SeqCtx e2 := (LetCtx BAnon e2).
-  Notation Skip := (Seq (Lit LitPoison) (Lit LitPoison)).
-  Notation If e0 e1 e2 := (Case e0 [e2;e1]).
 End base.
 
 Export base.

theories/lang/notation.v

+From iris.program_logic Require Import language.
+
 From gpfsl Require Export lang.
 
+From iris.prelude Require Import options.
+
 Coercion App : expr >-> Funclass.
+
 Coercion nopro_lang.of_val : nopro_lang.val >-> nopro_lang.expr.
 Coercion of_val : val >-> expr.
 
 Coercion Var : string >-> expr.
 
+Notation "[ ]" := (@nil binder) : binder_scope.
+Notation "a :: b" := (@cons binder a%binder b%binder)
+  (at level 60, right associativity) : binder_scope.
+Notation "[ x1 ; x2 ; .. ; xn ]" :=
+  (@cons binder x1%binder (@cons binder x2%binder
+        (..(@cons binder xn%binder (@nil binder))..))) : binder_scope.
+Notation "[ x ]" := (@cons binder x%binder (@nil binder)) : binder_scope.
+
 Notation "[ ]" := (@nil expr) : expr_scope.
 Notation "[ x ]" := (@cons expr x%E (@nil expr)) : expr_scope.
 Notation "[ x1 ; x2 ; .. ; xn ]" :=
   (@cons expr x1%E (@cons expr x2%E
         (..(@cons expr xn%E (@nil expr))..))) : expr_scope.
 
+(* Some derived forms *)
+Notation Lam xl e := (Rec BAnon xl e) (only parsing).
+Notation Let x e1 e2 := (App (Lam [x] e2) [e1]) (only parsing).
+Notation Seq e1 e2 := (Let BAnon e1 e2) (only parsing).
+Notation LamV xl e := (RecV BAnon xl e) (only parsing).
+Notation LetCtx x e2 := (AppRCtx (LamV [x] e2) [] []) (only parsing).
+Notation SeqCtx e2 := (LetCtx BAnon e2) (only parsing).
+Notation Skip := (Seq (Lit LitPoison) (Lit LitPoison)).
+Notation If e0 e1 e2 := (Case e0 [e2;e1]).
+
 (* No scope for the values, does not conflict and scope is often not inferred
 properly. *)
 Notation "# l" := (LitV l%Z%V%L) (at level 8, format "# l").
 Notation "# l" := (Lit l%Z%V%L) (at level 8, format "# l") : expr_scope.
 
-
 (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
     first. *)
 Notation "'case:' e0 'of' el" := (Case e0%E el%E)

theories/logic/arith.v

@@ -6,10 +6,10 @@ From gpfsl.logic Require Export lifting proofmode.
 Require Import iris.prelude.options.
 
 Definition minimum : val :=
-  λ: ["m"; "n"], if: "m" < "n" then (Var "m") else (Var "n").
+  λ: ["m"; "n"], if: "m" < "n" then "m" else "n".
 
 Definition maximum : val :=
-  λ: ["m"; "n"], if: "m" < "n" then (Var "n") else (Var "m").
+  λ: ["m"; "n"], if: "m" < "n" then "n" else "m".
 
 Section spec_proof.
 Context `{!noprolG Σ}.

theories/logic/atomic_exchange.v

@@ -11,7 +11,7 @@ Definition XCHG_aux (or ow : memOrder) (f : val) : val :=
   rec: "XCHG" ["x"; "vn"] :=
     let: "vo"  := !ʳˡˣ "x" in
       if: CAS "x" "vo" (f ["vo"; "vn"]) Relaxed or ow (* the failure case is a relaxed read by default *)
-      then (Var "vo") (* return the old value. TODO: coercion *)
+      then "vo"
       else "XCHG" ["x"; "vn"]
   .
 

theories/logic/repeat_loop.v

@@ -9,10 +9,10 @@ Require Import iris.prelude.options.
 (* Repeat-until loop: repeat doing [e] until it returns true *)
 Notation "'repeat:' e" :=
   ((rec: "f" []%binder :=
-    let: "v" := e%E in
-    if: "v" = #false then "f" [] else (Var "v")) [])%E
+    let: "v" := e%E in if: "v" = #false then "f" [] else "v") [])%E
   (at level 102, e at level 200) : expr_scope.
 
+(* TODO : improve these specs *)
 Lemma wp_repeat_2 `{!noprolG Σ} tid E e `{Closed [] e} Φ (SUB: ↑histN ⊆ E) :
   WP e @ tid; E {{ v, ∃ (z: lit), ⌜v = #z ∧ z ≠ ☠%V⌝ ∧
                       if bool_decide (z = 0)