Ignore:
Timestamp:
Apr 1, 2011, 1:35:18 PM (9 years ago)
Author:
campbell
Message:

Common definition for animation semantics, and factor out IO definitions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/SmallstepExec.ma

    r702 r731  
    66include "common/Mem.ma".
    77
    8 record execstep : Type[1] ≝
     8record execstep (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
    99{ genv  : Type[0]
    1010; state : Type[0]
    11 ; output : Type[0]
    12 ; input : output → Type[0]
    1311; is_final : state → option int
    1412; mem_of_state : state → mem
    15 ; step : genv → state → IO output input (trace×state)
     13; step : genv → state → IO outty inty (trace×state)
    1614}.
    1715
    18 let rec repeat (n:nat) (exec:execstep) (g:genv exec) (s:state exec)
    19  : IO (output exec) (input exec) (trace × (state exec)) ≝
     16let rec repeat (n:nat) (outty:Type[0]) (inty:outty → Type[0]) (exec:execstep outty inty)
     17               (g:genv ?? exec) (s:state ?? exec)
     18 : IO outty inty (trace × (state ?? exec)) ≝
    2019match n with
    2120[ O ⇒ Value ??? 〈E0, s〉
    22 | S n' ⇒ ! 〈t1,s1〉 ← step exec g s;
    23          repeat n' exec g s1
     21| S n' ⇒ ! 〈t1,s1〉 ← step ?? exec g s;
     22         repeat n' ?? exec g s1
    2423].
    2524
     
    3534   state. *)
    3635
    37 let corec exec_inf_aux (exec:execstep) (ge:genv exec)
    38                        (s:IO (output exec) (input exec) (trace×(state exec)))
     36let corec exec_inf_aux (output:Type[0]) (input:output → Type[0])
     37                       (exec:execstep output input) (ge:genv ?? exec)
     38                       (s:IO output input (trace×(state ?? exec)))
    3939                       : execution ??? ≝
    4040match s with
    4141[ Wrong ⇒ e_wrong ???
    4242| Value v ⇒ match v with [ pair t s' ⇒
    43     match is_final exec s' with
    44     [ Some r ⇒ e_stop ??? t r (mem_of_state exec s')
    45     | None ⇒ e_step ??? t s' (exec_inf_aux ? ge (step exec ge s')) ] ]
    46 | Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ? ge (k' v))
     43    match is_final ?? exec s' with
     44    [ Some r ⇒ e_stop ??? t r (mem_of_state ?? exec s')
     45    | None ⇒ e_step ??? t s' (exec_inf_aux ??? ge (step ?? exec ge s')) ] ]
     46| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? ge (k' v))
    4747].
    4848
    49 lemma execution_cases: ∀ex.∀e:execution (state ex) (output ex) (input ex).
     49lemma execution_cases: ∀o,i,s.∀e:execution s o i.
    5050 e = match e with [ e_stop tr r m ⇒ e_stop ??? tr r m
    5151 | e_step tr s e ⇒ e_step ??? tr s e
    5252 | e_wrong ⇒ e_wrong ??? | e_interact o k ⇒ e_interact ??? o k ].
    53 #ex #e cases e; //; qed.
     53#o #i #s #e cases e; //; qed.
    5454
    55 axiom exec_inf_aux_unfold: ∀exec,ge,s. exec_inf_aux exec ge s =
     55axiom exec_inf_aux_unfold: ∀o,i,exec,ge,s. exec_inf_aux o i exec ge s =
    5656match s with
    5757[ Wrong ⇒ e_wrong ???
    5858| Value v ⇒ match v with [ pair t s' ⇒
    59     match is_final exec s' with
    60     [ Some r ⇒ e_stop ??? t r (mem_of_state exec s')
    61     | None ⇒ e_step ??? t s' (exec_inf_aux ? ge (step exec ge s')) ] ]
    62 | Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ? ge (k' v))
     59    match is_final ?? exec s' with
     60    [ Some r ⇒ e_stop ??? t r (mem_of_state ?? exec s')
     61    | None ⇒ e_step ??? t s' (exec_inf_aux ??? ge (step ?? exec ge s')) ] ]
     62| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? ge (k' v))
    6363].
    6464(*
     
    7171*)
    7272
    73 record execstep' : Type[1] ≝
    74 { es0 :> execstep
    75 ; initial : state es0 → Prop
     73record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
     74{ es1 :> execstep outty inty
     75; program : Type[0]
     76; make_initial_state : program → res (genv ?? es1 × (state ?? es1))
     77}.
     78
     79definition exec_inf : ∀o,i.∀fx:fullexec o i. ∀p:program ?? fx. execution (state ?? fx) o i ≝
     80λo,i,fx,p.
     81  match make_initial_state ?? fx p with
     82  [ OK gs ⇒ exec_inf_aux ?? fx (\fst gs) (Value … 〈E0,\snd gs〉)
     83  | _ ⇒ e_wrong ???
     84  ].
     85
     86
     87record execstep' (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
     88{ es0 :> execstep outty inty
     89; initial : state ?? es0 → Prop
    7690}.
    7791
     
    7993alias symbol "and" (instance 2) = "logical and".
    8094record related_semantics : Type[1] ≝
    81 { sem1 : execstep'
    82 ; sem2 : execstep'
    83 ; ge1 : genv sem1
    84 ; ge2 : genv sem2
    85 ; match_states : state sem1 → state sem2 → Prop
    86 ; match_initial_states : ∀st1. (initial sem1) st1 → ∃st2. (initial sem2) st2 ∧ match_states st1 st2
    87 ; match_final_states : ∀st1,st2,r. match_states st1 st2 → (is_final sem1) st1 = Some ? r → (is_final sem2) st2 = Some ? r
     95{ output : Type[0]
     96; input : output → Type[0]
     97; sem1 : execstep' output input
     98; sem2 : execstep' output input
     99; ge1 : genv ?? sem1
     100; ge2 : genv ?? sem2
     101; match_states : state ?? sem1 → state ?? sem2 → Prop
     102; match_initial_states : ∀st1. (initial ?? sem1) st1 → ∃st2. (initial ?? sem2) st2 ∧ match_states st1 st2
     103; match_final_states : ∀st1,st2,r. match_states st1 st2 → (is_final ?? sem1) st1 = Some ? r → (is_final ?? sem2) st2 = Some ? r
    88104}.
    89105
     
    93109{ sems :> related_semantics
    94110; sim : ∀st1,st2,t,st1'.
    95         P_io' ?? (trace × (state (sem1 sems))) (λr. r = 〈t,st1'〉) (step (sem1 sems) (ge1 sems) st1) →
     111        P_io' ?? (trace × (state ?? (sem1 sems))) (λr. r = 〈t,st1'〉) (step ?? (sem1 sems) (ge1 sems) st1) →
    96112        match_states sems st1 st2 →
    97         ∃st2':(state (sem2 sems)).(∃n:nat.P_io' ?? (trace × (state (sem2 sems))) (λr. r = 〈t,st2'〉) (repeat n (sem2 sems) (ge2 sems) st2)) ∧
     113        ∃st2':(state ?? (sem2 sems)).(∃n:nat.P_io' ?? (trace × (state ?? (sem2 sems))) (λr. r = 〈t,st2'〉) (repeat n ?? (sem2 sems) (ge2 sems) st2)) ∧
    98114          match_states sems st1' st2'
    99115}.
Note: See TracChangeset for help on using the changeset viewer.