lang.v 32.3 KB
Newer Older
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
1 2 3 4 5 6
From iris.program_logic Require Export language ectx_language ectxi_language.
From iris.algebra Require Export ofe.
From stdpp Require Export strings.
From stdpp Require Import gmap.
Set Default Proof Using "Type".

7
Module dist_lang.
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
8 9 10 11 12
Open Scope Z_scope.

(** Expressions and vals. *)
Definition loc := positive. (* Really, any countable type. *)

13 14 15
Inductive side : Set :=
  | Left
  | Right.
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
16
Inductive base_lit : Set :=
17
  | LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitLoc (l : loc) | LitChan (l : loc) (s : side) (* | LitBuf (l : list Z) (r : list Z) *).
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69
Inductive un_op : Set :=
  | NegOp | MinusUnOp.
Inductive bin_op : Set :=
  | PlusOp | MinusOp | MultOp | QuotOp | RemOp (* Arithmetic *)
  | AndOp | OrOp | XorOp (* Bitwise *)
  | ShiftLOp | ShiftROp (* Shifts *)
  | LeOp | LtOp | EqOp. (* Relations *)

Inductive binder := BAnon | BNamed : string  binder.
Delimit Scope binder_scope with bind.
Bind Scope binder_scope with binder.
Definition cons_binder (mx : binder) (X : list string) : list string :=
  match mx with BAnon => X | BNamed x => x :: X end.
Infix ":b:" := cons_binder (at level 60, right associativity).
Instance binder_eq_dec_eq : EqDecision binder.
Proof. solve_decision. Defined.

Instance set_unfold_cons_binder x mx X P :
  SetUnfold (x  X) P  SetUnfold (x  mx :b: X) (BNamed x = mx  P).
Proof.
  constructor. rewrite -(set_unfold (x  X) P).
  destruct mx; rewrite /= ?elem_of_cons; naive_solver.
Qed.

Inductive expr :=
  (* Base lambda calculus *)
  | Var (x : string)
  | Rec (f x : binder) (e : expr)
  | App (e1 e2 : expr)
  (* Base types and their operations *)
  | Lit (l : base_lit)
  | UnOp (op : un_op) (e : expr)
  | BinOp (op : bin_op) (e1 e2 : expr)
  | If (e0 e1 e2 : expr)
  (* Products *)
  | Pair (e1 e2 : expr)
  | Fst (e : expr)
  | Snd (e : expr)
  (* Sums *)
  | InjL (e : expr)
  | InjR (e : expr)
  | Case (e0 : expr) (e1 : expr) (e2 : expr)
  (* Concurrency *)
  | Fork (e : expr)
  (* Heap *)
  | Alloc (e : expr)
  | Load (e : expr)
  | Store (e1 : expr) (e2 : expr)
  | CAS (e0 : expr) (e1 : expr) (e2 : expr)
  | FAA (e1 : expr) (e2 : expr)
  (* Process *)
  | Start (e : expr)
70 71 72 73 74 75 76
  (* Channels *)
  | NewChan
  | Send (c e : expr)
  | Recv (c : expr).
  (* (* Lists *) *)
  (* | Cons (x : expr) (xs : expr) *)
  (* | Nil. *)
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
77 78 79 80 81 82 83

Bind Scope expr_scope with expr.

Fixpoint is_closed (X : list string) (e : expr) : bool :=
  match e with
  | Var x => bool_decide (x  X)
  | Rec f x e => is_closed (f :b: x :b: X) e
84 85 86 87 88
  | Lit _ | NewChan (* | Nil *) => true
  | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e | Start e | Recv e =>
                                                                             is_closed X e
  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 | Send e1 e2 (* | Cons e1 e2 *) =>
                                                           is_closed X e1 && is_closed X e2
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
89
  | If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
90
                                  is_closed X e0 && is_closed X e1 && is_closed X e2 
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
91 92 93 94 95 96
  end.

Class Closed (X : list string) (e : expr) := closed : is_closed X e.
Instance closed_proof_irrel X e : ProofIrrel (Closed X e).
Proof. rewrite /Closed. apply _. Qed.
Instance closed_dec X e : Decision (Closed X e).
97
Proof. rewrite /Closed. apply _. Defined.
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
98 99 100 101 102 103

Inductive val :=
  | RecV (f x : binder) (e : expr) `{!Closed (f :b: x :b: []) e} (* This is a restriction *)
  | LitV (l : base_lit)
  | PairV (v1 v2 : val)
  | InjLV (v : val)
104 105
  | InjRV (v : val)
  (* | ListV (l : list val) *).
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
106 107 108 109 110 111 112 113 114 115

Bind Scope val_scope with val.

Fixpoint of_val (v : val) : expr :=
  match v with
  | RecV f x e => Rec f x e
  | LitV l => Lit l
  | PairV v1 v2 => Pair (of_val v1) (of_val v2)
  | InjLV v => InjL (of_val v)
  | InjRV v => InjR (of_val v)
116 117 118 119
  (* | ListV l => match l with *)
  (*              | [] => Nil  *)
  (*              | x::xs => Cons (of_val x) (of_val xs) *)
  (*              end *)
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
120 121
  end.

122 123
Fixpoint to_val (e : expr) : option val := 
   match e with
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
124 125 126 127 128 129 130 131 132 133 134
  | Rec f x e =>
     if decide (Closed (f :b: x :b: []) e) then Some (RecV f x e) else None
  | Lit l => Some (LitV l)
  | Pair e1 e2 => v1  to_val e1; v2  to_val e2; Some (PairV v1 v2)
  | InjL e => InjLV <$> to_val e
  | InjR e => InjRV <$> to_val e
  | _ => None
  end.

(** The state: heaps of vals. *)
Definition heap := gmap loc val.
135
Definition state := heap.
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151

(** Equality and other typeclass stuff *)
Lemma to_of_val v : to_val (of_val v) = Some v.
Proof.
  by induction v; simplify_option_eq; repeat f_equal; try apply (proof_irrel _).
Qed.

Lemma of_to_val e v : to_val e = Some v  of_val v = e.
Proof.
  revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
Qed.

Instance of_val_inj : Inj (=) (=) of_val.
Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.


152 153 154 155 156 157 158 159 160 161 162 163
Global Instance side_eq_dec : EqDecision side.
Proof. solve_decision. Qed.
Global Instance side_countable: Countable side.
Proof.
  pose (encode := (λ s, match s with Left => 1 | _ => 2 end)%positive).
  pose (decode := (λ s, match s with 1 => Some Left | _ => Some Right end)%positive).
  eapply (Build_Countable _ _ encode decode).
  by intros [|].
Qed.
(* Global Instance list_eq_dec' : (forall x y:A, Decision (x = y)) -> forall xs ys : list A, Decision (xs = ys). *)
(* Proof. solve_decision. Qed.  *)

Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181
Instance base_lit_eq_dec : EqDecision base_lit.
Proof. solve_decision. Defined.
Instance un_op_eq_dec : EqDecision un_op.
Proof. solve_decision. Defined.
Instance bin_op_eq_dec : EqDecision bin_op.
Proof. solve_decision. Defined.
Instance expr_eq_dec : EqDecision expr.
Proof. solve_decision. Defined.
Instance val_eq_dec : EqDecision val.
Proof.
 refine (λ v v', cast_if (decide (of_val v = of_val v'))); abstract naive_solver.
Defined.

Instance base_lit_countable : Countable base_lit.
Proof.
 refine (inj_countable' (λ l, match l with
  | LitInt n => inl (inl (inl n)) | LitBool b => inl (inl (inr b))
  | LitUnit => inl (inr (inl ())) | LitLoc l => inl (inr (inr l))
182
  | LitChan l c  => inr ((l,c)) (* Correct? *)
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
183 184 185
  end) (λ l, match l with
  | inl (inl (inl n)) => LitInt n | inl (inl (inr b)) => LitBool b
  | inl (inr (inl ())) => LitUnit | inl (inr (inr l)) => LitLoc l
186
  | inr ((l,c)) => LitChan l c (* Correct? *)
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234
  end) _); by intros [].
Qed.
Instance un_op_finite : Countable un_op.
Proof.
 refine (inj_countable' (λ op, match op with NegOp => 0 | MinusUnOp => 1 end)
  (λ n, match n with 0 => NegOp | _ => MinusUnOp end) _); by intros [].
Qed.
Instance bin_op_countable : Countable bin_op.
Proof.
 refine (inj_countable' (λ op, match op with
  | PlusOp => 0 | MinusOp => 1 | MultOp => 2 | QuotOp => 3 | RemOp => 4
  | AndOp => 5 | OrOp => 6 | XorOp => 7 | ShiftLOp => 8 | ShiftROp => 9
  | LeOp => 10 | LtOp => 11 | EqOp => 12
  end) (λ n, match n with
  | 0 => PlusOp | 1 => MinusOp | 2 => MultOp | 3 => QuotOp | 4 => RemOp
  | 5 => AndOp | 6 => OrOp | 7 => XorOp | 8 => ShiftLOp | 9 => ShiftROp
  | 10 => LeOp | 11 => LtOp | _ => EqOp
  end) _); by intros [].
Qed.
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 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))
  | UnOp op e => GenNode 2 [GenLeaf (inr (inr (inl op))); go e]
  | BinOp op e1 e2 => GenNode 3 [GenLeaf (inr (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]
  | FAA e1 e2 => GenNode 16 [go e1; go e2]
  | Start e => GenNode 17 [go e] (* Added *)
235 236 237
  | NewChan => GenNode 18 []
  | Send e1 e2 => GenNode 19 [go e1; go e2]
  | Recv e => GenNode 20 [go e]
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260
  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 [GenLeaf (inr (inr (inl op))); e] => UnOp op (go e)
  | GenNode 3 [GenLeaf (inr (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 [e1; e2] => FAA (go e1) (go e2)
  | GenNode 17 [e] => Start (go e) (* Added *)
261 262 263
  | GenNode 18 [] => NewChan
  | GenNode 19 [e1; e2] => Send (go e1) (go e2)
  | GenNode 20 [e] => Recv (go e)
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301
  | _ => Lit LitUnit (* 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.

Instance expr_inhabited : Inhabited expr := populate (Lit LitUnit).
Instance val_inhabited : Inhabited val := populate (LitV LitUnit).

Canonical Structure stateC := leibnizC state.
Canonical Structure valC := leibnizC val.
Canonical Structure exprC := leibnizC expr.

(** Evaluation contexts *)
Inductive ectx_item :=
  | AppLCtx (e2 : expr)
  | AppRCtx (v1 : val)
  | UnOpCtx (op : un_op)
  | BinOpLCtx (op : bin_op) (e2 : expr)
  | BinOpRCtx (op : bin_op) (v1 : val)
  | IfCtx (e1 e2 : expr)
  | PairLCtx (e2 : expr)
  | PairRCtx (v1 : val)
  | FstCtx
  | SndCtx
  | InjLCtx
  | InjRCtx
  | CaseCtx (e1 : expr) (e2 : expr)
  | AllocCtx
  | LoadCtx
  | StoreLCtx (e2 : expr)
  | StoreRCtx (v1 : val)
  | CasLCtx (e1 : expr) (e2 : expr)
  | CasMCtx (v0 : val) (e2 : expr)
  | CasRCtx (v0 : val) (v1 : val)
  | FaaLCtx (e2 : expr)
  | FaaRCtx (v1 : val)
302 303 304 305
  | StartCtx
  | SendLCtx (e2 : expr)
  | SendRCtx (v1 : val)
  | RecvCtx.
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330

Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
  match Ki with
  | AppLCtx e2 => App e e2
  | AppRCtx v1 => App (of_val v1) e
  | UnOpCtx op => UnOp op e
  | BinOpLCtx op e2 => BinOp op e e2
  | BinOpRCtx op v1 => BinOp op (of_val v1) e
  | IfCtx e1 e2 => If e e1 e2
  | PairLCtx e2 => Pair e e2
  | PairRCtx v1 => Pair (of_val v1) e
  | FstCtx => Fst e
  | SndCtx => Snd e
  | InjLCtx => InjL e
  | InjRCtx => InjR e
  | CaseCtx e1 e2 => Case e e1 e2
  | AllocCtx => Alloc e
  | LoadCtx => Load e
  | StoreLCtx e2 => Store e e2 
  | StoreRCtx v1 => Store (of_val v1) e
  | CasLCtx e1 e2 => CAS e e1 e2
  | CasMCtx v0 e2 => CAS (of_val v0) e e2
  | CasRCtx v0 v1 => CAS (of_val v0) (of_val v1) e
  | FaaLCtx e2 => FAA e e2
  | FaaRCtx v1 => FAA (of_val v1) e
331
  | StartCtx => Start e
332
  | SendLCtx e2  => Send e e2
333 334
  | SendRCtx v1 => Send (of_val v1) e
  | RecvCtx => Recv e
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
335 336 337
  end.

(** Substitution *)
338
Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
339 340 341
  match e with
  | Var y => if decide (x = y) then es else Var y
  | Rec f y e =>
342
    Rec f y $ if decide (BNamed x  f  BNamed x  y) then subst x es e else e
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360
  | App e1 e2 => App (subst x es e1) (subst x es e2)
  | Lit l => Lit l
  | UnOp op e => UnOp op (subst x es e)
  | BinOp op e1 e2 => BinOp op (subst x es e1) (subst x es e2)
  | If e0 e1 e2 => If (subst x es e0) (subst x es e1) (subst x es e2)
  | Pair e1 e2 => Pair (subst x es e1) (subst x es e2)
  | Fst e => Fst (subst x es e)
  | Snd e => Snd (subst x es e)
  | InjL e => InjL (subst x es e)
  | InjR e => InjR (subst x es e)
  | Case e0 e1 e2 => Case (subst x es e0) (subst x es e1) (subst x es e2)
  | Fork e => Fork (subst x es e)
  | Alloc e => Alloc (subst x es e)
  | Load e => Load (subst x es e)
  | Store e1 e2 => Store (subst x es e1) (subst x es e2)
  | CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2)
  | FAA e1 e2 => FAA (subst x es e1) (subst x es e2)
  | Start e => Start (subst x es e)
361 362 363
  | NewChan => NewChan
  | Send e1 e2 => Send (subst x es e1) (subst x es e2)
  | Recv e => Recv (subst x es e)
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412
  end.

Definition subst' (mx : binder) (es : expr) : expr  expr :=
  match mx with BNamed x => subst x es | BAnon => id end.

(** The stepping relation *)
Definition un_op_eval (op : un_op) (v : val) : option val :=
  match op, v with
  | NegOp, LitV (LitBool b) => Some $ LitV $ LitBool (negb b)
  | NegOp, LitV (LitInt n) => Some $ LitV $ LitInt (Z.lnot n)
  | MinusUnOp, LitV (LitInt n) => Some $ LitV $ LitInt (- n)
  | _, _ => None
  end.

Definition bin_op_eval_int (op : bin_op) (n1 n2 : Z) : base_lit :=
  match op with
  | PlusOp => LitInt (n1 + n2)
  | MinusOp => LitInt (n1 - n2)
  | MultOp => LitInt (n1 * n2)
  | QuotOp => LitInt (n1 `quot` n2)
  | RemOp => LitInt (n1 `rem` n2)
  | AndOp => LitInt (Z.land n1 n2)
  | OrOp => LitInt (Z.lor n1 n2)
  | XorOp => LitInt (Z.lxor n1 n2)
  | ShiftLOp => LitInt (n1  n2)
  | ShiftROp => LitInt (n1  n2)
  | LeOp => LitBool (bool_decide (n1  n2))
  | LtOp => LitBool (bool_decide (n1 < n2))
  | EqOp => LitBool (bool_decide (n1 = n2))
  end.

Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit :=
  match op with
  | PlusOp | MinusOp | MultOp | QuotOp | RemOp => None (* Arithmetic *)
  | AndOp => Some (LitBool (b1 && b2))
  | OrOp => Some (LitBool (b1 || b2))
  | XorOp => Some (LitBool (xorb b1 b2))
  | ShiftLOp | ShiftROp => None (* Shifts *)
  | LeOp | LtOp => None (* InEquality *)
  | EqOp => Some (LitBool (bool_decide (b1 = b2)))
  end.

Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
  match v1, v2 with
  | LitV (LitInt n1), LitV (LitInt n2) => Some $ LitV $ bin_op_eval_int op n1 n2
  | LitV (LitBool b1), LitV (LitBool b2) => LitV <$> bin_op_eval_bool op b1 b2
  | v1, v2 => guard (op = EqOp); Some $ LitV $ LitBool $ bool_decide (v1 = v2)
  end.

413 414 415 416 417 418
Definition bin_op_eval2 (op : bin_op) (v1 v2 : val) : option val :=
  match v1, v2 with
  | LitV (LitInt n1), LitV (LitInt n2) => Some $ LitV $ bin_op_eval_int op n1 n2
  | LitV (LitBool b1), LitV (LitBool b2) => LitV <$> bin_op_eval_bool op b1 b2
  | v1, v2 => guard (op = EqOp); Some $ LitV $ LitBool $ bool_decide (v1 = v2)
  end.
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
419 420

Inductive head_step : expr  state  expr  state  list (expr)  Prop :=
421
  | Betas f x e1 e2 v2 e' σ :
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471
     to_val e2 = Some v2 
     Closed (f :b: x :b: []) e1 
     e' = subst' x (of_val v2) (subst' f (Rec f x e1) e1) 
     head_step (App (Rec f x e1) e2) σ e' σ []
  | UnOpS op e v v' σ :
     to_val e = Some v 
     un_op_eval op v = Some v'  
     head_step (UnOp op e) σ (of_val v') σ []
  | BinOpS op e1 e2 v1 v2 v' σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     bin_op_eval op v1 v2 = Some v'  
     head_step (BinOp op e1 e2) σ (of_val v') σ []
  | IfTrueS e1 e2 σ :
     head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ []
  | IfFalseS e1 e2 σ :
     head_step (If (Lit $ LitBool false) e1 e2) σ e2 σ []
  | FstS e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     head_step (Fst (Pair e1 e2)) σ e1 σ []
  | SndS e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     head_step (Snd (Pair e1 e2)) σ e2 σ []
  | CaseLS e0 v0 e1 e2 σ :
     to_val e0 = Some v0 
     head_step (Case (InjL e0) e1 e2) σ (App e1 e0) σ []
  | CaseRS e0 v0 e1 e2 σ :
     to_val e0 = Some v0 
     head_step (Case (InjR e0) e1 e2) σ (App e2 e0) σ []
  | ForkS e σ:
     head_step (Fork e) σ (Lit LitUnit) σ [e]
  | AllocS e v σ l :
     to_val e = Some v  σ !! l = None 
     head_step (Alloc e) σ (Lit $ LitLoc l) (<[l:=v]>σ) []
  | LoadS l v σ :
     σ !! l = Some v 
     head_step (Load (Lit $ LitLoc l)) σ (of_val v) σ []
  | StoreS l e v σ :
     to_val e = Some v  is_Some (σ !! l) 
     head_step (Store (Lit $ LitLoc l) e) σ (Lit LitUnit) (<[l:=v]>σ) []
  | CasFailS l e1 v1 e2 v2 vl σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     σ !! l = Some vl  vl  v1 
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool false) σ []
  | CasSucS l e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     σ !! l = Some v1 
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) []
  | FaaS l i1 e2 i2 σ :
     to_val e2 = Some (LitV (LitInt i2)) 
     σ !! l = Some (LitV (LitInt i1)) 
472
     head_step (FAA (Lit $ LitLoc l) e2) σ (Lit $ LitInt i1) (<[l:=LitV (LitInt (i1 + i2))]>σ) [].
473 474 475 476 477 478 479 480 481 482 483 484
  (* | NewChanS' l σ : *)
  (*    σ !! l = None → *)
  (*    head_step NewChan σ (Pair (Lit $ LitChan l Left) (Lit $ LitChan l Right)) (<[l:=LitV $ LitBuf [] []]>σ) [] *)
  (* | Sendlefts l l' r' σ e v : *)
  (*    σ !! l = Some (LitV $ LitBuf l' r') → *)
  (*    to_val e = Some $ LitV $ LitInt $ v → *)
  (*    head_step (Send (Lit $ LitChan l Left) e) σ (Lit $ LitUnit) (<[l:=LitV $ LitBuf (l' ++ [v]) r']>σ) [] *)
  (* | RecvLeftS l l' r' rval rs rexpr σ e v : *)
  (*    σ !! l = Some (LitV $ LitBuf l' r') → *)
  (*    to_val e = Some v → *)
  (*    rval::rs = r' → *)
  (*    rexpr = of_val (LitV $ LitInt $ rval) → *)
485
  (*    head_step (Recv (Lit $ LitChan l Left)) σ (rexpr) (<[l:= LitV $ LitBuf (l') (rs)]>σ) []. *)
486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504

(** Work done here *)
Inductive buffer : Set :=
  Buffer (l : list val) (r : list val).

Definition channels := gmap loc buffer.
Definition state' := prod heap channels.

Inductive head_step' : expr  state'  expr  state'  list (expr)  Prop :=
  | ExprS e σ σs e' σ' σs' es :
     fst σ = σs 
     fst σ' = σs' 
     head_step e σs e' σs' es 
     head_step' e σ e' σ' es
  | NewChanS l σ σs σc :
     fst σ = σs 
     snd σ = σc 
     σc !! l = None 
     head_step' NewChan σ (Pair (Lit $ LitChan l Left) (Lit $ LitChan l Right)) (σs, <[l:=Buffer [] []]>σc) []
505
  | SendLS σ σs σc l l' r' e v:
506 507 508 509 510
     fst σ = σs 
     snd σ = σc 
     σc !! l = Some (Buffer l' r') 
     to_val e = Some $ v 
     head_step' (Send (Lit $ LitChan l Left) e) σ (Lit $ LitUnit) (σs, <[l:=Buffer (l' ++ [v]) r']>σc) []
511
  | SendRS σ σs σc l l' r' e v:
512 513 514
     fst σ = σs 
     snd σ = σc 
     σc !! l = Some (Buffer l' r') 
515 516 517 518
     to_val e = Some $ v 
     head_step' (Send (Lit $ LitChan l Right) e) σ (Lit $ LitUnit) (σs, <[l:=Buffer l' (r' ++ [v])]>σc) []
  | RecvLSucS l l' r' rv σ σs σc :
     fst σ = σs 
519
     snd σ = σc 
520 521 522 523 524 525 526 527 528 529 530 531 532 533 534
     σc !! l = Some (Buffer l' (rv::r')) 
     head_step' (Recv (Lit $ LitChan l Left)) σ (of_val rv) (σs, <[l:= Buffer l' r']>σc) []
  | RecvRSucS l l' r' lv σ σs σc :
     fst σ = σs 
     snd σ = σc 
     σc !! l = Some (Buffer (lv::l') r') 
     head_step' (Recv (Lit $ LitChan l Right)) σ (of_val lv) (σs, <[l:= Buffer l' r']>σc) []
  | RecvLFailS l l' σ σc :
     snd σ = σc 
     σc !! l = Some (Buffer l' []) 
     head_step' (Recv (Lit $ LitChan l Left)) σ (Recv (Lit $ LitChan l Left)) σ []
  | RecvRFailS l r' σ σc :
     snd σ = σc 
     σc !! l = Some (Buffer [] r') 
     head_step' (Recv (Lit $ LitChan l Right)) σ (Recv (Lit $ LitChan l Right)) σ [].
535

536 537
(* Process extension *)

538 539 540
Definition processes := gmap loc heap.
Definition state'' := prod processes channels.

541 542 543
(* Inductive pexpr := PExpr (l : loc) (e : expr). *)
Definition pexpr := prod loc expr.
Definition pexpr_to_expr (pe : pexpr) : expr := pe.2.
544

545 546 547
(* Inductive pval := PVal (l: loc) (v : val). *)
Definition pval := prod loc val.
Definition pval_to_val (pv : pval) : val := pv.2.
548

549 550 551 552 553 554
Definition of_val'' (v : pval) : pexpr := (v.1, of_val (pval_to_val v)).

Definition to_val'' (e : pexpr) : option pval := 
  match to_val (pexpr_to_expr e) with
  | Some v => Some (e.1, v)
  | None => None
555
  end.
556

557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642
(* Lemma to_val_val'' e : option_map (pval_to_val) (to_val'' e) = to_val (pexpr_to_expr e). *)
(* Proof. *)
(*   unfold to_val''. *)
(*   destruct (to_val (pexpr_to_expr e)); reflexivity. *)
(* Qed. *)

(* Lemma to_val_val''' e : is_Some (to_val'' e) = is_Some (to_val (pexpr_to_expr e)). *)
(* Proof. *)
(*   destruct e. *)
(*   unfold to_val''. *)
(*   simpl. *)
(*   destruct (to_val e). *)
(*   - admit. *)
(*   - apply is_Some_alt (@None A). *)

(* assert(is_Some (Some (l,v)) = True).  apply <- is_Some_dec. rewrite <- is_Some_alt. eq_dec. apply is_Some_alt. *)
  
(* exists (x := x').  reflexivity.   *)


Lemma to_val_val'' e : is_Some (to_val (pexpr_to_expr e))  is_Some (to_val'' e) .
Proof.
  split.
  - intros.  
    unfold to_val''.
    simpl.
    inversion H.
    rewrite H0.
    eauto. 
  - unfold to_val''.
    simpl.
    intros.
    inversion H.
    destruct (to_val (pexpr_to_expr e)).
    + eauto.
    + inversion H0.
Qed.

Lemma to_val_val''_none e : to_val (pexpr_to_expr e) = None  to_val'' e = None.
Proof.
  unfold to_val''; destruct (to_val (pexpr_to_expr e)); split; intros; inversion H; reflexivity.
Qed.
 
Lemma to_of_val'' v : to_val'' (of_val'' v) = Some v.
Proof.
  destruct v. unfold to_val''.  unfold of_val''. simpl. rewrite to_of_val. reflexivity.
Qed.

(* Lemma prod_eq a a' b b' : a = a' → b = b' → (a,b) = (a',b'). *)
(* Proof. *)
 

Lemma of_to_val'' e v : to_val'' e = Some v  of_val'' v = e.
Proof.
  destruct e, v.
  unfold to_val'', of_val''.
  simpl.
  intros.
  assert (to_val e = Some v). remember (to_val e) as tve. destruct tve in *. inversion H. subst. reflexivity. inversion H.
  assert (l = l0). destruct (to_val e). simplify_option_eq. reflexivity. inversion H.
  subst.
  simplify_option_eq.
  apply injective_projections; simpl.
  - reflexivity.
  - generalize dependent H0. apply of_to_val.
Qed.

Instance of_val_inj'' : Inj (=) (=) of_val''.
Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val'' Hv. Qed.

Definition fill_item'' (Ki : ectx_item) (e : pexpr) : pexpr := (e.1, fill_item Ki e.2).

Lemma fill_item_item'' Ki e : fill_item Ki (pexpr_to_expr e) = pexpr_to_expr (fill_item'' Ki e).
Proof.
  unfold pexpr_to_expr.
  simpl. 
  reflexivity.
Qed.

(* Definition lift_expr (i : loc) (e : expr) : pexpr := PExpr i e. *)

Definition unpack_expr (e:pexpr) : expr := snd e.
  (* match e with *)
  (* | PExpr i e => e *)
  (* end. *)

643 644 645 646 647 648 649 650
(* Definition unpack_state (s:processes) (i:loc) : heap := *)
(*   match s !! i with *)
(*   | Some(h) => h *)
(*   | None => ∅ *)
(*   end. *)

(*Definition lift_expr (i : nat) (e : expr) : expr := Expr i e.*)

651 652 653 654 655 656 657
(* Fixpoint forPairs (i : loc) (pes : list pexpr) (es : list expr) : Prop := *)
(*   match (pes, es) with *)
(*   | (pe::pes, e::es) => pe = PExpr i e /\ forPairs i pes es *)
(*   | ([],[]) => True *)
(*   | (_,_) => False *)
(*   end. *)

658 659
Fixpoint forPairs (i : loc) (pes : list pexpr) (es : list expr) : Prop :=
  match (pes, es) with
660
  | (pe::pes, e::es) => pe = (i, e) /\ forPairs i pes es
661 662 663 664 665
  | ([],[]) => True
  | (_,_) => False
  end.

Inductive head_step'' : pexpr  state''  pexpr  state''  list (pexpr)  Prop :=
666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683
    (* | ExprS'' p pe pσ pσs pσc e σ  *)
    (*            pe' pσ' pσs' pσc' e' σ' *)
    (*            pes es : *)
    (*   (* pe = PExpr p e → *) *)
    (*   pe = (p, e) → *)
    (*   fst pσ = pσs → *)
    (*   snd pσ = pσc → *)
    (*   pσs !! p = Some(σ) → *)
    (*   (* pe' = PExpr p e' → *) *)
    (*   pe' = (p, e') → *)
    (*   fst pσ' = pσs' → *)
    (*   snd pσ' = pσc' → *)
    (*   pσs' !! p = Some(σ') → *)
    (*   forPairs p pes es → *)
    (*   head_step' e (σ,pσc) e' (σ',pσc') es → *)
    (*   head_step'' pe pσ pe' pσ' pes *)
    | ExprS' p pσs pσc e σ 
                pσs' pσc' e' σ'
684
               pes es :
685
      pσs  !! p = Some(σ) 
686 687 688
      pσs' !! p = Some(σ') 
      forPairs p pes es 
      head_step' e (σ,pσc) e' (σ',pσc') es 
689
      head_step'' (p,e) (pσs, pσc) (p,e') (pσs', pσc') pes
690
    | StartS p e σ σp σc p' v :
691 692 693
      fst σ = σp 
      snd σ = σc 
      σp !! p' = None 
694
      to_val e = Some $ v 
695 696
      (* head_step'' (PExpr p (Start e)) σ (PExpr p (Lit $ LitUnit)) (<[p':=∅]>σp, σc) [PExpr p' e]. *)
      head_step'' (p, (Start e)) σ (p, (Lit $ LitUnit)) (<[p':=]>σp, σc) [(p', e)].
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
697 698 699 700 701

(** Basic properties about the language *)
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.

702 703 704 705 706 707 708
Instance fill_item_inj'' Ki : Inj (=) (=) (fill_item'' Ki).
Proof. 
  unfold fill_item''. intros ???. inversion H. destruct x, y. apply injective_projections; simpl in *.
  - subst. reflexivity.
  - generalize dependent H2. apply fill_item_inj.
Qed.

Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
709 710 711 712
Lemma fill_item_val Ki e :
  is_Some (to_val (fill_item Ki e))  is_Some (to_val e).
Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.

713 714 715 716 717
Lemma fill_item_val'' Ki e :
  is_Some (to_val'' (fill_item'' Ki e))  is_Some (to_val'' e).
Proof. intros. apply to_val_val'' in H. apply to_val_val''. destruct e. simpl in *. generalize dependent H. 
       apply fill_item_val. Qed.

Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
718 719 720
Lemma val_head_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs  to_val e1 = None.
Proof. destruct 1; naive_solver. Qed.

721 722 723 724 725
Lemma val_head_stuck' e1 σ1 e2 σ2 efs : head_step' e1 σ1 e2 σ2 efs  to_val e1 = None.
Proof.
  destruct 1; try naive_solver. generalize H1. apply val_head_stuck.
Qed.

726
Lemma val_head_stuck'' e1 σ1 e2 σ2 efs : head_step'' e1 σ1 e2 σ2 efs  to_val'' e1 = None.
727
Proof.
728
  destruct 1; try naive_solver. apply val_head_stuck' in H2. unfold to_val''. subst. simpl. rewrite H2. reflexivity. Qed.
729

Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
730 731 732 733
Lemma head_ctx_step_val Ki e σ1 e2 σ2 efs :
  head_step (fill_item Ki e) σ1 e2 σ2 efs  is_Some (to_val e).
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.

734 735 736 737 738 739 740 741
Lemma head_ctx_step_val' Ki e σ1 e2 σ2 efs :
  head_step' (fill_item Ki e) σ1 e2 σ2 efs  is_Some (to_val e).
Proof. 
  inversion 1; 
    first (generalize dependent H2; apply head_ctx_step_val);
    repeat (generalize dependent H; destruct Ki; inversion_clear 1; simplify_option_eq; by eauto).
Qed.

742 743
Lemma head_ctx_step_val'' Ki e σ1 e2 σ2 efs :
  head_step'' (fill_item'' Ki e) σ1 e2 σ2 efs  is_Some (to_val'' e).
744
Proof.
745 746 747
  inversion 1.
  - apply to_val_val''. generalize dependent H9. apply head_ctx_step_val'.
  - apply to_val_val''. generalize dependent H; destruct Ki; inversion_clear 1; unfold pexpr_to_expr; simplify_option_eq; by eauto.
748 749
Qed.

Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
750 751 752 753 754 755 756 757 758 759
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
  to_val e1 = None  to_val e2 = None 
  fill_item Ki1 e1 = fill_item Ki2 e2  Ki1 = Ki2.
Proof.
  destruct Ki1, Ki2; intros; try discriminate; simplify_eq/=;
    repeat match goal with
    | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
    end; auto.
Qed.

760 761 762 763 764 765 766 767 768 769 770 771 772 773 774
Lemma fill_item_no_val_inj'' Ki1 Ki2 e1 e2 :
  to_val'' e1 = None  to_val'' e2 = None 
  fill_item'' Ki1 e1 = fill_item'' Ki2 e2  Ki1 = Ki2.
Proof.
  intros.
  apply to_val_val''_none in H.
  apply to_val_val''_none in H0.
  unfold fill_item'' in H1.
  inversion H1.
  generalize dependent H4.
  generalize dependent H0.
  generalize dependent H.
  apply fill_item_no_val_inj.
Qed.

Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
775 776 777 778 779
Lemma alloc_fresh e v σ :
  let l := fresh (dom (gset loc) σ) in
  to_val e = Some v  head_step (Alloc e) σ (Lit (LitLoc l)) (<[l:=v]>σ) [].
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset loc)), is_fresh. Qed.

780 781 782 783 784
Lemma alloc_fresh' σ σs σc :
  let l := fresh (dom (gset loc) σc) in
  fst σ = σs  snd σ = σc  head_step' NewChan σ (Pair (Lit $ LitChan l Left) (Lit $ LitChan l Right)) (σs, <[l:=Buffer [] []]>σc) [].
Proof. by intros; apply NewChanS, (not_elem_of_dom (D:=gset loc)), is_fresh. Qed.

Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856
(* Misc *)
Lemma to_val_rec f x e `{!Closed (f :b: x :b: []) e} :
  to_val (Rec f x e) = Some (RecV f x e).
Proof. rewrite /to_val. case_decide=> //. do 2 f_equal; apply proof_irrel. Qed.

(** Closed expressions *)
Lemma is_closed_weaken X Y e : is_closed X e  X  Y  is_closed Y e.
Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.

Lemma is_closed_weaken_nil X e : is_closed [] e  is_closed X e.
Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.

Lemma is_closed_of_val X v : is_closed X (of_val v).
Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed.

Lemma is_closed_to_val X e v : to_val e = Some v  is_closed X e.
Proof. intros <-%of_to_val. apply is_closed_of_val. Qed.

Lemma is_closed_subst X e x es :
  is_closed [] es  is_closed (x :: X) e  is_closed X (subst x es e).
Proof.
  intros ?. 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.
Lemma is_closed_do_subst' X e x es :
  is_closed [] es  is_closed (x :b: X) e  is_closed X (subst' x es e).
Proof. destruct x; eauto using is_closed_subst. Qed.

(* Substitution *)
Lemma subst_is_closed X e x es : is_closed 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.

Lemma subst_is_closed_nil e x es : is_closed [] e  subst x es e = e.
Proof. intros. apply subst_is_closed with []; set_solver. Qed.

Lemma subst_subst e x es es' :
  Closed [] es'  subst x es (subst x es' e) = subst x es' e.
Proof.
  intros. induction e; simpl; try (f_equal; by auto);
    simplify_option_eq; auto using subst_is_closed_nil with f_equal.
Qed.
Lemma subst_subst' e x es es' :
  Closed [] es'  subst' x es (subst' x es' e) = subst' x es' e.
Proof. destruct x; simpl; auto using subst_subst. Qed.

Lemma subst_subst_ne e x y es es' :
  Closed [] es  Closed [] es'  x  y 
  subst x es (subst y es' e) = subst y es' (subst x es e).
Proof.
  intros. induction e; simpl; try (f_equal; by auto);
    simplify_option_eq; auto using eq_sym, subst_is_closed_nil with f_equal.
Qed.
Lemma subst_subst_ne' e x y es es' :
  Closed [] es  Closed [] es'  x  y 
  subst' x es (subst' y es' e) = subst' y es' (subst' x es e).
Proof. destruct x, y; simpl; auto using subst_subst_ne with congruence. Qed.

Lemma subst_rec' f y e x es :
  x = f  x = y  x = BAnon 
  subst' x es (Rec f y e) = Rec f y e.
Proof. intros. destruct x; simplify_option_eq; naive_solver. Qed.
Lemma subst_rec_ne' f y e x es :
  (x  f  f = BAnon)  (x  y  y = BAnon) 
  subst' x es (Rec f y e) = Rec f y (subst' x es e).
Proof. intros. destruct x; simplify_option_eq; naive_solver. Qed.

857
Lemma dist_lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
858 859 860 861
Proof.
  split; apply _ || eauto using to_of_val, of_to_val, val_head_stuck,
    fill_item_val, fill_item_no_val_inj, head_ctx_step_val.
Qed.
862 863 864 865 866 867 868 869 870 871 872 873 874

Lemma dist_lang_mixin' : EctxiLanguageMixin of_val to_val fill_item head_step'.
Proof.
  split; apply _ || eauto using to_of_val, of_to_val, val_head_stuck',
    fill_item_val, fill_item_no_val_inj, head_ctx_step_val'.
Qed.

Lemma dist_lang_mixin'' : EctxiLanguageMixin of_val'' to_val'' fill_item'' head_step''.
Proof.
  split; apply _ || eauto using to_of_val'', of_to_val'', val_head_stuck'',
    fill_item_val'', fill_item_no_val_inj'', head_ctx_step_val''.
Qed.

875
End dist_lang.
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
876 877

(** Language *)
878 879 880
Canonical Structure dist_ectxi_lang := EctxiLanguage dist_lang.dist_lang_mixin.
Canonical Structure dist_ectx_lang := EctxLanguageOfEctxi dist_ectxi_lang.
Canonical Structure dist_lang := LanguageOfEctx dist_ectx_lang.
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
881

882 883 884 885 886 887 888 889 890 891
(** Language' *)
Canonical Structure dist_ectxi_lang' := EctxiLanguage dist_lang.dist_lang_mixin'.
Canonical Structure dist_ectx_lang' := EctxLanguageOfEctxi dist_ectxi_lang'.
Canonical Structure dist_lang' := LanguageOfEctx dist_ectx_lang'.

(** Language'' *)
Canonical Structure dist_ectxi_lang'' := EctxiLanguage dist_lang.dist_lang_mixin''.
Canonical Structure dist_ectx_lang'' := EctxLanguageOfEctxi dist_ectxi_lang''.
Canonical Structure dist_lang'' := LanguageOfEctx dist_ectx_lang''.

892 893
(* Prefer dist_lang names over ectx_language names. *)
Export dist_lang.
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
894 895 896 897 898 899 900 901 902 903

(** Define some derived forms *)
Notation Lam x e := (Rec BAnon x e).
Notation Let x e1 e2 := (App (Lam x e2) e1).
Notation Seq e1 e2 := (Let BAnon e1 e2).
Notation LamV x e := (RecV BAnon x e).
Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
Notation SeqCtx e2 := (LetCtx BAnon e2).
Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)).