language.v 2.16 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
Require Export modures.cofe.
Ralf Jung's avatar
Ralf Jung committed
2

3 4 5 6 7 8 9 10
Structure language := Language {
  expr : Type;
  val : Type;
  state : Type;
  of_val : val  expr;
  to_val : expr  option val;
  atomic : expr  Prop;
  prim_step : expr  state  expr  state  option expr  Prop;
Robbert Krebbers's avatar
Robbert Krebbers committed
11 12 13
  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;
14
  atomic_not_val e : atomic e  to_val e = None;
Ralf Jung's avatar
Ralf Jung committed
15 16
  atomic_step e1 σ1 e2 σ2 ef :
    atomic e1 
Ralf Jung's avatar
Ralf Jung committed
17
    prim_step e1 σ1 e2 σ2 ef 
Robbert Krebbers's avatar
Robbert Krebbers committed
18
    is_Some (to_val e2)
Ralf Jung's avatar
Ralf Jung committed
19
}.
20 21 22 23 24 25 26
Arguments of_val {_} _.
Arguments to_val {_} _.
Arguments atomic {_} _.
Arguments prim_step {_} _ _ _ _ _.
Arguments to_of_val {_} _.
Arguments of_to_val {_} _ _ _.
Arguments values_stuck {_} _ _ _ _ _ _.
27
Arguments atomic_not_val {_} _ _.
28 29 30 31 32
Arguments atomic_step {_} _ _ _ _ _ _ _.

Canonical Structure istateC Σ := leibnizC (state Σ).

Definition cfg (Λ : language) := (list (expr Λ) * state Λ)%type.
Ralf Jung's avatar
Ralf Jung committed
33

34
Section language.
35 36
  Context {Λ : language}.
  Implicit Types v : val Λ.
Ralf Jung's avatar
Ralf Jung committed
37

38
  Definition reducible (e : expr Λ) (σ : state Λ) :=
39
     e' σ' ef, prim_step e σ e' σ' ef.
40 41 42 43 44 45 46
  Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
    | step_atomic e1 σ1 e2 σ2 ef t1 t2 :
       ρ1 = (t1 ++ e1 :: t2, σ1) 
       ρ2 = (t1 ++ e2 :: t2 ++ option_list ef, σ2) 
       prim_step e1 σ1 e2 σ2 ef 
       step ρ1 ρ2.

47 48
  Lemma reducible_not_val e σ : reducible e σ  to_val e = None.
  Proof. intros (?&?&?&?); eauto using values_stuck. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
49
  Lemma atomic_of_val v : ¬atomic (of_val v).
50
  Proof. by intros Hat%atomic_not_val; rewrite to_of_val in Hat. Qed.
51
  Global Instance: Injective (=) (=) (@of_val Λ).
Robbert Krebbers's avatar
Robbert Krebbers committed
52
  Proof. by intros v v' Hv; apply (injective Some); rewrite -!to_of_val Hv. Qed.
53
End language.
Ralf Jung's avatar
Ralf Jung committed
54

55 56 57 58
Class LanguageCtx (Λ : language) (K : expr Λ  expr Λ) := {
  fill_not_val e :
    to_val e = None  to_val (K e) = None;
  fill_step e1 σ1 e2 σ2 ef :
59
    prim_step e1 σ1 e2 σ2 ef 
60 61 62 63
    prim_step (K e1) σ1 (K e2) σ2 ef;
  fill_step_inv 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
64
}.