Changeset 3377


Ignore:
Timestamp:
Jul 2, 2013, 11:37:46 AM (4 years ago)
Author:
sacerdot
Message:
  • emit l removed

+ io l1 l2

The semantics has been changed so that one step can now emit a sequence of
labels (to implement io l1 l2).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Imp.ma

    r3376 r3377  
    1 include "arithmetics/nat.ma".
    2 include "basics/types.ma".
    3 include "basics/lists/list.ma".
    4 
    5 (*************************)
    6 
    7 axiom ltb: nat → nat → bool.
    8 
    9 (*************************)
    10 
    11 record label: Type[0] ≝ {label_name: nat}.
    12 
    13 record ident: Type[0] ≝ {ident_name: nat}.
    14 
    15 record fname: Type[0] ≝ {function_name: nat}.
    16 
    17 definition label_of_fname: fname → label ≝
    18  λf. mk_label (function_name f).
    19  
    20 coercion label_of_fname.
    21 
    22 record storeT: Type[1] ≝
    23  { store:> Type[0]
    24  ; get: store → option ident → nat
    25  ; set: store → option ident → nat → store
    26  ; get_set_hit: ∀s,x,v. get (set s x v) x = v
    27  ; get_set_miss: ∀s,x,y,v. get (set s x v) y = get s y
    28  }.
     1include "Common.ma".
    292
    303inductive expr : Type[0] :=
     
    4417| Cifthenelse: bool_expr → label → cmd → label → cmd → cmd
    4518| Cwhile: bool_expr → label → cmd → label → cmd
    46 | Clabel: label → cmd → cmd
     19| Cio: label → label → cmd
    4720| Ccall: ident → fname → expr → option label → cmd
    4821| Cret: expr → cmd.
     
    7043definition fetchT ≝ fname → cmd.
    7144
    72 inductive step (S: storeT) (fetch: fetchT) : state S → state S → option label → Prop :=
     45inductive step (S: storeT) (fetch: fetchT) : state S → state S → list label → Prop :=
    7346| step_assign: ∀x,e,k,K,s.
    7447   step …
    7548    〈Cassign x e, k, K, s〉
    7649    〈Cskip, k, K, set … s (Some … x) (eval_expr … s e)〉
    77     (None …)
     50    []
    7851| step_skip: ∀c,k,K,s.
    7952   step …
    8053    〈Cskip, c::k, K, s〉
    81     〈c, k, K, s〉
    82     (None …)
     54    〈c,        k, K, s〉
     55    []
    8356| step_seq: ∀c,c',k,K,s.
    8457   step …
    85     〈Cseq c c', k, K, s〉
    86     〈c, c'::k, K, s〉
    87     (None …)
     58    〈Cseq c c',     k, K, s〉
     59    〈        c, c'::k, K, s〉
     60    []
    8861| step_if_true:
    8962   ∀b,l1,c1,l2,c2,k,K,s. eval_bool_expr ? s b = true →
    9063    step …
    9164     〈Cifthenelse b l1 c1 l2 c2, k, K, s〉
    92      〈c1, k, K, s〉
    93      (Some … l1)
     65     〈                       c1, k, K, s〉
     66     [l1]
    9467| step_if_false:
    9568   ∀b,l1,c1,l2,c2,k,K,s. eval_bool_expr ? s b = false →
    9669    step …
    9770     〈Cifthenelse b l1 c1 l2 c2, k, K, s〉
    98      〈c2, k, K, s〉
    99      (Some … l2)
     71     〈                       c2, k, K, s〉
     72     [l2]
    10073| step_while_true: ∀b,l1,c,l2,k,K,s. eval_bool_expr ? s b = true →
    10174   step …
    102     〈Cwhile b l1 c l2, k, K,s〉
    103     〈c, (Cwhile b l1 c l2)::k, K, s〉
    104     (Some … l1)
     75    〈Cwhile b l1 c l2,                     k, K,s〉
     76    〈               c, (Cwhile b l1 c l2)::k, K, s〉
     77    [l1]
    10578| step_while_false: ∀b,l1,c,l2,k,K,s. eval_bool_expr ? s b = false →
    10679   step …
    10780    〈Cwhile b l1 c l2, k, K, s〉
    108     〈Cskip, k, K, s〉
    109     (Some … l2)
    110 | step_label: ∀c,l,k,K,s.
     81    〈           Cskip, k, K, s〉
     82    [l2]
     83| step_label: ∀l1,l2,k,K,s.
    11184   step …
    112     〈Clabel l c,k,K,s〉
    113     〈c,k,K,s〉
    114     (Some … l)
     85    〈Cio l1 l2, k, K, s〉
     86    〈    Cskip, k, K, s〉
     87    [l1;l2]
    11588| step_call: ∀x,f,e,l,c,k,K,s. fetch f = c →
    11689   step …
    117     〈Ccall x f e l, k, K, s〉
    118     〈c, [], 〈get ? s (None …),x,l,k〉::K, set ? s (None …) (eval_expr ? s e)〉
    119     (Some … f)
     90    〈Ccall x f e l,  k, K,                                                            s〉
     91    〈            c, [], 〈get ? s (None …),x,l,k〉::K, set ? s (None …) (eval_expr ? s e)〉
     92    [f]
    12093| step_return: ∀e,k1,v,x,l,k2,K,s.
    12194   step …
    122     〈Cret e, k1, 〈v,x,l,k2〉::K, s〉
    123     〈Cskip, k2, K, set ? (set ? s (Some … x) (eval_expr ? s e)) (None …) v〉
    124     l.
     95    〈Cret e, k1, 〈v,x,l,k2〉::K,                                                       s〉
     96    〈 Cskip, k2,            K, set ? (set ? s (Some … x) (eval_expr ? s e)) (None …) v〉
     97    (match l with [ None ⇒ [] | Some l ⇒ [l]]).
    12598
    12699(*
Note: See TracChangeset for help on using the changeset viewer.