Changeset 25 for C-semantics/CexecIO.ma


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

Simplify the IO monad a little.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r24 r25  
    614614(* Interactions are function calls that return a value and do not change
    615615   the rest of the Clight program's state. *)
    616 ndefinition io ≝ mk_interaction (ident × (list eventval)) eventval.
    617 
    618 ndefinition do_io : ident → list eventval → IO io eventval ≝
    619 λfn,args. Interact io eventval 〈fn,args〉 (λres. Value io eventval res).
    620 
    621 ndefinition ret: ∀T. T → (IO io T) ≝
    622 λT,x.(Value io T x).
     616ndefinition io_out ≝ (ident × (list eventval)).
     617
     618ndefinition do_io : ident → list eventval → IO eventval io_out eventval ≝
     619λfn,args. Interact ?? eventval 〈fn,args〉 (λres. Value ?? eventval res).
     620
     621ndefinition ret: ∀T. T → (IO eventval io_out T) ≝
     622λT,x.(Value ?? T x).
    623623
    624624(* Checking types of values given to / received from an external function call. *)
     
    659659(* execution *)
    660660
    661 nlet rec exec_step (ge:genv) (st:state) on st : (IO io (Σr:trace × state. step ge st (\fst r) (\snd r))) ≝
     661nlet rec exec_step (ge:genv) (st:state) on st : (IO eventval io_out (Σr:trace × state. step ge st (\fst r) (\snd r))) ≝
    662662match st with
    663663[ State f s k e m ⇒
     
    695695          match fn_return f with
    696696          [ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉)
    697           | _ ⇒ Some ? (Wrong ??)
     697          | _ ⇒ Some ? (Wrong ???)
    698698          ]
    699699      | Kcall _ _ _ _ ⇒
    700700          match fn_return f with
    701701          [ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉)
    702           | _ ⇒ Some ? (Wrong ??)
     702          | _ ⇒ Some ? (Wrong ???)
    703703          ]
    704704      | Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f (Swhile a s') k' e m〉)
     
    713713      | Kfor3 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f (Sfor Sskip a2 a3 s') k' e m〉)
    714714      | Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
    715       | _ ⇒ Some ? (Wrong ??)
     715      | _ ⇒ Some ? (Wrong ???)
    716716      ]
    717717  | Scontinue ⇒
     
    728728      | Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉)
    729729      | Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Scontinue k' e m〉)
    730       | _ ⇒ Some ? (Wrong ??)
     730      | _ ⇒ Some ? (Wrong ???)
    731731      ]
    732732  | Sbreak ⇒
     
    737737      | Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
    738738      | Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
    739       | _ ⇒ Some ? (Wrong ??)
     739      | _ ⇒ Some ? (Wrong ???)
    740740      ]
    741741  | Sifthenelse a s1 s2 ⇒ Some ? (
     
    761761    [ None ⇒ match fn_return f with
    762762      [ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉)
    763       | _ ⇒ Some ? (Wrong ??)
     763      | _ ⇒ Some ? (Wrong ???)
    764764      ]
    765765    | Some a ⇒ Some ? (
     
    771771      ! v ← exec_expr ge e m a;:
    772772      match v with [ Vint n ⇒ ret ? 〈E0, State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m〉
    773                    | _ ⇒ Wrong ?? ])
     773                   | _ ⇒ Wrong ??? ])
    774774  | Slabel lbl s' ⇒ Some ? (ret ? 〈E0, State f s' k e m〉)
    775775  | Sgoto lbl ⇒
    776776      match find_label lbl (fn_body f) (call_cont k) with
    777777      [ Some sk' ⇒ match sk' with [ mk_pair s' k' ⇒ Some ? (ret ? 〈E0, State f s' k' e m〉) ]
    778       | None ⇒ Some ? (Wrong ??)
     778      | None ⇒ Some ? (Wrong ???)
    779779      ]
    780780  ]
     
    799799      match res with
    800800      [ Vundef ⇒ Some ? (ret ? 〈E0, (State f Sskip k' e m)〉)
    801       | _ ⇒ Some ? (Wrong ??)
     801      | _ ⇒ Some ? (Wrong ???)
    802802      ]
    803803    | Some r' ⇒
     
    809809      ]
    810810    ]
    811   | _ ⇒ Some ? (Wrong ??)
     811  | _ ⇒ Some ? (Wrong ???)
    812812  ]
    813813]. nwhd; //;
     
    883883nqed.
    884884
    885 nlet rec make_initial_state (p:program) : IO io (Σs:state. initial_state p s) ≝
     885nlet rec make_initial_state (p:program) : IO eventval io_out (Σs:state. initial_state p s) ≝
    886886  let ge ≝ globalenv Genv ?? p in
    887887  let m0 ≝ init_mem Genv ?? p in
     
    915915
    916916nlet rec exec_steps (n:nat) (ge:genv) (s:state) :
    917  IO io (Σts:trace×state. star (mk_transrel ?? step) ge s (\fst ts) (\snd ts)) ≝
     917 IO eventval io_out (Σts:trace×state. star (mk_transrel ?? step) ge s (\fst ts) (\snd ts)) ≝
    918918match is_final_state s with
    919919[ inl _ ⇒ Some ? (ret ? 〈E0, s〉)
Note: See TracChangeset for help on using the changeset viewer.