language.v 1.57 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
Require Export modures.base.
Ralf Jung's avatar
Ralf Jung committed
2

3
Class Language (E V St : Type) := {
Robbert Krebbers's avatar
Robbert Krebbers committed
4
5
  of_val : V  E;
  to_val : E  option V;
Ralf Jung's avatar
Ralf Jung committed
6
  atomic : E  Prop;
7
  prim_step : E  St  E  St  option E  Prop;
Robbert Krebbers's avatar
Robbert Krebbers committed
8
9
10
11
  to_of_val v : to_val (of_val v) = Some v;
  of_to_val e v : to_val e = Some v  of_val v = e;
  values_stuck e σ e' σ' ef : prim_step e σ e' σ' ef  to_val e = None;
  atomic_not_value e : atomic e  to_val e = None;
Ralf Jung's avatar
Ralf Jung committed
12
13
  atomic_step e1 σ1 e2 σ2 ef :
    atomic e1 
Ralf Jung's avatar
Ralf Jung committed
14
    prim_step e1 σ1 e2 σ2 ef 
Robbert Krebbers's avatar
Robbert Krebbers committed
15
    is_Some (to_val e2)
Ralf Jung's avatar
Ralf Jung committed
16
17
}.

18
Section language.
Ralf Jung's avatar
Ralf Jung committed
19
20
  Context `{Language E V St}.

Robbert Krebbers's avatar
Robbert Krebbers committed
21
22
23
24
25
26
27
  Lemma atomic_of_val v : ¬atomic (of_val v).
  Proof.
    by intros Hat; apply atomic_not_value in Hat; rewrite to_of_val in Hat.
  Qed.
  Global Instance: Injective (=) (=) of_val.
  Proof. by intros v v' Hv; apply (injective Some); rewrite -!to_of_val Hv. Qed.

Ralf Jung's avatar
Ralf Jung committed
28
29
30
31
32
  Definition cfg : Type := (list E * St)%type.
  Inductive step (ρ1 ρ2 : cfg) : Prop :=
    | step_atomic e1 σ1 e2 σ2 ef t1 t2 :
       ρ1 = (t1 ++ e1 :: t2, σ1) 
       ρ1 = (t1 ++ e2 :: t2 ++ option_list ef, σ2) 
Ralf Jung's avatar
Ralf Jung committed
33
       prim_step e1 σ1 e2 σ2 ef 
Ralf Jung's avatar
Ralf Jung committed
34
35
36
37
       step ρ1 ρ2.

  Definition steps := rtc step.
  Definition stepn := nsteps step.
Ralf Jung's avatar
Ralf Jung committed
38

Robbert Krebbers's avatar
Robbert Krebbers committed
39
  Record is_ctx (K : E  E) := IsCtx {
Robbert Krebbers's avatar
Robbert Krebbers committed
40
    is_ctx_value e : to_val e = None  to_val (K e) = None;
Robbert Krebbers's avatar
Robbert Krebbers committed
41
42
43
44
45
46
    is_ctx_step_preserved e1 σ1 e2 σ2 ef :
      prim_step e1 σ1 e2 σ2 ef  prim_step (K e1) σ1 (K e2) σ2 ef;
    is_ctx_step e1' σ1 e2 σ2 ef :
      to_val e1' = None  prim_step (K e1') σ1 e2 σ2 ef 
       e2', e2 = K e2'  prim_step e1' σ1 e2' σ2 ef
  }.
47
End language.
Ralf Jung's avatar
Ralf Jung committed
48