Ignore:
Timestamp:
Sep 20, 2011, 7:11:41 PM (9 years ago)
Author:
campbell
Message:

Change SmallstepExec? so that states can depend on global information.
Use less suggestive names for the transition system so that it's obvious
the global information isn't restricted to Genv.
Separate set up of global environment from initialisation so that it never
fails.
Some minimal changes to get Clight execution working; rest to follow.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/SmallstepExec.ma

    r1213 r1231  
    44include "common/Events.ma".
    55
    6 record execstep (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
    7 { mem : Type[0]
    8 ; genv  : Type[0]
    9 ; state : Type[0]
    10 ; is_final : state → option int
    11 ; mem_of_state : state → mem
    12 ; step : genv → state → IO outty inty (trace×state)
     6record trans_system (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
     7{ global : Type[0]
     8; state  : global → Type[0]
     9; is_final : ∀g. state g → option int
     10; step : ∀g. state g → IO outty inty (trace×(state g))
    1311}.
    1412
    15 let rec repeat (n:nat) (outty:Type[0]) (inty:outty → Type[0]) (exec:execstep outty inty)
    16                (g:genv ?? exec) (s:state ?? exec)
    17  : IO outty inty (trace × (state ?? exec)) ≝
     13let rec repeat (n:nat) (outty:Type[0]) (inty:outty → Type[0]) (exec:trans_system outty inty)
     14               (g:global ?? exec) (s:state ?? exec g)
     15 : IO outty inty (trace × (state ?? exec g)) ≝
    1816match n with
    1917[ O ⇒ Value ??? 〈E0, s〉
     
    4442
    4543let corec exec_inf_aux (output:Type[0]) (input:output → Type[0])
    46                        (exec:execstep output input) (ge:genv ?? exec)
    47                        (s:IO output input (trace×(state ?? exec)))
     44                       (exec:trans_system output input) (g:global ?? exec)
     45                       (s:IO output input (trace×(state ?? exec g)))
    4846                       : execution ??? ≝
    4947match s with
    5048[ Wrong m ⇒ e_wrong ??? m
    5149| Value v ⇒ match v with [ pair t s' ⇒
    52     match is_final ?? exec s' with
     50    match is_final ?? exec g s' with
    5351    [ Some r ⇒ e_stop ??? t r s'
    54     | None ⇒ e_step ??? t s' (exec_inf_aux ??? ge (step ?? exec ge s')) ] ]
    55 | Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? ge (k' v))
     52    | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ] ]
     53| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v))
    5654].
    5755
     
    6462  here, used reflexivity instead *)
    6563
    66 axiom exec_inf_aux_unfold: ∀o,i,exec,ge,s. exec_inf_aux o i exec ge s =
     64axiom exec_inf_aux_unfold: ∀o,i,exec,g,s. exec_inf_aux o i exec g s =
    6765match s with
    6866[ Wrong m ⇒ e_wrong ??? m
    6967| Value v ⇒ match v with [ pair t s' ⇒
    70     match is_final ?? exec s' with
     68    match is_final ?? exec g s' with
    7169    [ Some r ⇒ e_stop ??? t r s'
    72     | None ⇒ e_step ??? t s' (exec_inf_aux ??? ge (step ?? exec ge s')) ] ]
    73 | Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? ge (k' v))
     70    | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ] ]
     71| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v))
    7472].
    7573(*
     
    8381
    8482record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
    85 { es1 :> execstep outty inty
    86 ; program : Type[0]
    87 ; make_initial_state : program → res (genv ?? es1 × (state ?? es1))
     83{ program : Type[0]
     84; es1 :> trans_system outty inty
     85; make_global : program → global ?? es1
     86; make_initial_state : ∀p:program. res (state ?? es1 (make_global p))
    8887}.
    8988
    90 definition exec_inf : ∀o,i.∀fx:fullexec o i. ∀p:program ?? fx. execution (state ?? fx) o i ≝
     89definition exec_inf : ∀o,i.∀fx:fullexec o i. ∀p:program ?? fx. execution (state ?? fx (make_global … fx p)) o i ≝
    9190λo,i,fx,p.
    9291  match make_initial_state ?? fx p with
    93   [ OK gs ⇒ exec_inf_aux ?? fx (\fst gs) (Value … 〈E0,\snd gs〉)
     92  [ OK s ⇒ exec_inf_aux ?? fx (make_global … fx p) (Value … 〈E0,s〉)
    9493  | Error m ⇒ e_wrong ??? m
    9594  ].
    9695
    97 
     96(* Some preliminary simulation stuff that's not been used yet.
    9897record execstep' (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
    9998{ es0 :> execstep outty inty
     
    125124          match_states sems st1' st2'
    126125}.
     126*)
Note: See TracChangeset for help on using the changeset viewer.