Ignore:
Timestamp:
Aug 27, 2010, 3:29:51 PM (9 years ago)
Author:
campbell
Message:

Simplify the IO monad a little.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/SmallstepExec.ma

    r24 r25  
    88{ genv  : Type
    99; state : Type
    10 ; io : interaction
     10; input : Type
     11; output : Type
    1112; initial : state → Prop
    1213; final : state → int → Prop
    13 ; step : genv → state → IO io (trace×state)
     14; step : genv → state → IO input output (trace×state)
    1415}.
    1516
    1617nlet rec repeat (n:nat) (exec:execstep) (g:genv exec) (s:state exec)
    17  : IO (io exec) (trace × (state exec)) ≝
     18 : IO (input exec) (output exec) (trace × (state exec)) ≝
    1819match n with
    19 [ O ⇒ Value ?? 〈E0, s〉
     20[ O ⇒ Value ??? 〈E0, s〉
    2021| S n' ⇒ ! 〈t1,s1〉 ← step exec g s;:
    2122         repeat n' exec g s1
     
    3839{ sems :> related_semantics
    3940; sim : ∀st1,st2,t,st1'.
    40         P_io' (io (sem1 sems)) (trace × (state (sem1 sems))) (λr. r = 〈t,st1'〉) (step (sem1 sems) (ge1 sems) st1) →
     41        P_io' ?? (trace × (state (sem1 sems))) (λr. r = 〈t,st1'〉) (step (sem1 sems) (ge1 sems) st1) →
    4142        match_states sems st1 st2 →
    42         ∃st2':(state (sem2 sems)).(∃n:nat.P_io' (io (sem2 sems)) (trace × (state (sem2 sems))) (λr. r = 〈t,st2'〉) (repeat n (sem2 sems) (ge2 sems) st2)) ∧
     43        ∃st2':(state (sem2 sems)).(∃n:nat.P_io' ?? (trace × (state (sem2 sems))) (λr. r = 〈t,st2'〉) (repeat n (sem2 sems) (ge2 sems) st2)) ∧
    4344          match_states sems st1' st2'
    4445}.
Note: See TracChangeset for help on using the changeset viewer.