Some useful instances for the language

theories/F_mu_ref_conc/binder.v

@@ -12,6 +12,11 @@ Definition cons_binder (mx : binder) (X : stringset) : stringset :=
 Infix ":b:" := cons_binder (at level 60, right associativity).
 Instance binder_eq_dec_eq : EqDecision binder.
 Proof. solve_decision. Defined.
+Instance binder_countable : Countable binder.
+Proof.
+ refine (inj_countable' (λ b, match b with BNamed s => Some s | BAnon => None end)
+  (λ b, match b with Some s => BNamed s | None => BAnon end) _); by intros [].
+Qed.
 
 Instance set_unfold_cons_binder x mx X P :
   SetUnfold (x ∈ X) P → SetUnfold (x ∈ mx :b: X) (BNamed x = mx ∨ P).

theories/F_mu_ref_conc/lang.v

@@ -8,12 +8,12 @@ Module lang.
   (** * Syntax and syntactic categories *)
   Definition loc := positive.
 
-  Instance loc_dec_eq (l l' : loc) : Decision (l = l') := _.
+  Instance loc_dec_eq : EqDecision loc := _.
 
   (** ** Expressions *)
   Inductive binop := Add | Sub | Eq | Le | Lt | Xor.
   
-  Instance binop_dec_eq (op op' : binop) : Decision (op = op').
+  Instance binop_dec_eq : EqDecision binop.
   Proof. solve_decision. Defined.
 
   Inductive literal := Unit | Nat (n : nat) | Bool (b : bool) | Loc (l : loc).
@@ -55,10 +55,10 @@ Module lang.
   | CAS (e0 : expr) (e1 : expr) (e2 : expr).
   Bind Scope expr_scope with expr.
 
-  Instance literal_dec_eq (l l' : literal) : Decision (l = l').
+  Instance literal_dec_eq : EqDecision literal.
   Proof. solve_decision. Defined.
 
-  Instance expr_dec_eq (e e' : expr) : Decision (e = e').
+  Instance expr_dec_eq : EqDecision expr.
   Proof. solve_decision. Defined.
 
   (** ** Closed expressions *)
@@ -160,11 +160,92 @@ Module lang.
   Instance of_val_inj : Inj (=) (=) of_val.
   Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
 
-  Instance val_dec_eq (v v' : val) : Decision (v = v').
+  Instance val_dec_eq : EqDecision val.
   Proof.
-    refine (cast_if (decide (of_val v = of_val v'))); abstract naive_solver.
+    refine (fun v v' => cast_if (decide (of_val v = of_val v'))); abstract naive_solver.
   Defined.
-    
+
+  Instance literal_countable : Countable literal.
+  Proof.
+    refine (inj_countable' (λ l, match l with
+    | Nat n => inl (inl n) | Bool b => inl (inr b)
+    | Unit => inr (inl ()) | Loc l => inr (inr l)
+    end) (λ l, match l with
+    | inl (inl n) => Nat n | inl (inr b) => Bool b
+    | inr (inl ()) => Unit | inr (inr l) => Loc l
+    end) _); by intros [].
+  Qed.
+
+  Instance binop_countable : Countable binop.
+  Proof.
+   refine (inj_countable' (λ op, match op with
+    | Add => 0 | Sub => 1 | Eq => 2 | Le => 3 | Lt => 4 | Xor => 5
+    end) (λ n, match n with
+    | 0 => Add | 1 => Sub | 2 => Eq | 3 => Le | 4 => Lt | _ => Xor
+    end) _); by intros [].
+  Qed.
+
+  Instance expr_countable : Countable expr.
+  Proof.
+    set (enc := fix go e :=
+           match e with
+           | Var x => GenLeaf (inl (inl x))
+           | Rec f x e => GenNode 0 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); go e]
+           | App e1 e2 => GenNode 1 [go e1; go e2]
+           | Lit l => GenLeaf (inr (inl l))
+           | Fold e => GenNode 2 [go e]
+           | BinOp op e1 e2 => GenNode 3 [GenLeaf (inr (inr op)); go e1; go e2]
+           | If e0 e1 e2 => GenNode 4 [go e0; go e1; go e2]
+           | Pair e1 e2 => GenNode 5 [go e1; go e2]
+           | Fst e => GenNode 6 [go e]
+           | Snd e => GenNode 7 [go e]
+           | InjL e => GenNode 8 [go e]
+           | InjR e => GenNode 9 [go e]
+           | Case e0 e1 e2 => GenNode 10 [go e0; go e1; go e2]
+           | Fork e => GenNode 11 [go e]
+           | Alloc e => GenNode 12 [go e]
+           | Load e => GenNode 13 [go e]
+           | Store e1 e2 => GenNode 14 [go e1; go e2]
+           | CAS e0 e1 e2 => GenNode 15 [go e0; go e1; go e2]
+           | Unfold e => GenNode 16 [go e]
+           | TLam e => GenNode 17 [go e]
+           | TApp e => GenNode 18 [go e]
+           | Pack e => GenNode 19 [go e]
+           | Unpack e1 e2 => GenNode 20 [go e1; go e2]
+           end).
+    set (dec := fix go e :=
+           match e with
+           | GenLeaf (inl (inl x)) => Var x
+           | GenNode 0 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); e] => Rec f x (go e)
+           | GenNode 1 [e1; e2] => App (go e1) (go e2)
+           | GenLeaf (inr (inl l)) => Lit l
+           | GenNode 2 [e] => Fold (go e)
+           | GenNode 3 [GenLeaf (inr (inr op)); e1; e2] => BinOp op (go e1) (go e2)
+           | GenNode 4 [e0; e1; e2] => If (go e0) (go e1) (go e2)
+           | GenNode 5 [e1; e2] => Pair (go e1) (go e2)
+           | GenNode 6 [e] => Fst (go e)
+           | GenNode 7 [e] => Snd (go e)
+           | GenNode 8 [e] => InjL (go e)
+           | GenNode 9 [e] => InjR (go e)
+           | GenNode 10 [e0; e1; e2] => Case (go e0) (go e1) (go e2)
+           | GenNode 11 [e] => Fork (go e)
+           | GenNode 12 [e] => Alloc (go e)
+           | GenNode 13 [e] => Load (go e)
+           | GenNode 14 [e1; e2] => Store (go e1) (go e2)
+           | GenNode 15 [e0; e1; e2] => CAS (go e0) (go e1) (go e2)
+           | GenNode 16 [e] => Unfold (go e)
+           | GenNode 17 [e] => TLam (go e)
+           | GenNode 18 [e] => TApp (go e)
+           | GenNode 19 [e] => Pack (go e)
+           | GenNode 20 [e1; e2] => Unpack (go e1) (go e2)
+           | _ => Lit Unit (* dummy *)
+           end).
+    refine (inj_countable' enc dec _). intros e. induction e; f_equal/=; auto.
+  Qed.
+
+  Instance val_countable : Countable val.
+  Proof. refine (inj_countable of_val to_val _); auto using to_of_val. Qed.
+
   (** ** Evaluation contexts *)
   Inductive ectx_item :=
   | AppLCtx (e2 : expr)
@@ -344,6 +425,8 @@ Module lang.
   Canonical Structure stateC := leibnizC state.
   Canonical Structure valC := leibnizC val.
   Canonical Structure exprC := leibnizC expr.
+  Canonical Structure locC := leibnizC loc.
+  Canonical Structure ectx_itemC := leibnizC ectx_item.
 
   Lemma fill_item_val Ki e :
     is_Some (to_val (fill_item Ki e)) → is_Some (to_val e).

theories/examples/stack/helping.v

@@ -52,8 +52,6 @@ Section refinement.
        let: "st" := ref Nile in
        (CG_locked_pop "st" "l", CG_locked_push "st" "l").
 
-  Canonical Structure ectx_itemC := leibnizC ectx_item.
-  Canonical Structure locC := leibnizC loc.
   Canonical Structure gnameC := leibnizC gname.
 
   Definition offerReg := gmap loc (val * gname * nat * (list ectx_item)).