language.v 1.32 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
2
Require Import prelude.prelude.

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

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

  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
26
       prim_step e1 σ1 e2 σ2 ef 
Ralf Jung's avatar
Ralf Jung committed
27
28
29
30
       step ρ1 ρ2.

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

32
33
34
35
36
37
38
39
  Definition is_ctx (ctx : E  E) : Prop :=
    ( e, is_Some (of_expr (ctx e))  is_Some (of_expr e)) 
    ( e1 σ1 e2 σ2 ef,
      prim_step e1 σ1 e2 σ2 ef -> prim_step (ctx e1) σ1 (ctx e2) σ2 ef) 
    ( e1' σ1 e2 σ2 ef,
      of_expr e1' = None  prim_step (ctx e1') σ1 e2 σ2 ef 
       e2', e2 = ctx e2'  prim_step e1' σ1 e2' σ2 ef).
End language.
Ralf Jung's avatar
Ralf Jung committed
40