Changeset 731 for src/Clight/Cexec.ma


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/Clight/Cexec.ma

    r725 r731  
    22
    33include "utilities/extralib.ma".
    4 include "common/IOMonad.ma".
     4include "common/IO.ma".
    55include "common/SmallstepExec.ma".
    66include "Clight/Csem.ma".
     
    439439qed.
    440440
    441 (* Checking types of values given to / received from an external function call. *)
    442 
    443 definition eventval_type : ∀ty:typ. Type[0] ≝
    444 λty. match ty with [ ASTint ⇒ int | ASTptr _ ⇒ False | ASTfloat ⇒ float ].
    445 
    446 definition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝
    447 λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint ⇒ λv.EVint v | ASTptr r ⇒ ? | ASTfloat ⇒ λv.EVfloat v ].
    448 *; qed.
    449 
    450 definition mk_val: ∀ty:typ. eventval_type ty → val ≝
    451 λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint ⇒ λv.Vint v | ASTptr r ⇒ ? | ASTfloat ⇒ λv.Vfloat v ].
    452 *; qed.
    453 
    454 lemma mk_val_correct: ∀ty:typ. ∀v:eventval_type ty.
    455   eventval_match (mk_eventval ty v) ty (mk_val ty v).
    456 #ty cases ty; normalize; // * *; qed.
    457 
    458 definition convert_eventval : ∀ev:eventval. ∀ty:typ. res val ≝
    459 λev,ty.
    460 match ty with
    461 [ ASTint ⇒ match ev with [ EVint i ⇒ OK ? (Vint i) | _ ⇒ Error ? ]
    462 | ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? (Vfloat f) | _ ⇒ Error ? ]
    463 | _ ⇒ Error ?
    464 ].
    465 
    466 definition check_eventval' : ∀v:val. ∀ty:typ. res eventval ≝
    467 λv,ty.
    468 match ty with
    469 [ ASTint ⇒ match v with [ Vint i ⇒ OK ? (EVint i) | _ ⇒ Error ? ]
    470 | ASTfloat ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? ]
    471 | _ ⇒ Error ?
    472 ].
    473 
    474 let rec check_eventval_list (vs: list val) (tys: list typ) : res (list eventval) ≝
    475 match vs with
    476 [ nil ⇒ match tys with [ nil ⇒ OK ? (nil ?) | _ ⇒ Error ? ]
    477 | cons v vt ⇒
    478   match tys with
    479   [ nil ⇒ Error ?
    480   | cons ty tyt ⇒
    481     do ev ← check_eventval' v ty;
    482     do evt ← check_eventval_list vt tyt;
    483     OK ? (ev::evt)
    484   ]
    485 ].
    486 
    487 (* IO monad *)
    488 
    489 (* Interactions are function calls that return a value and do not change
    490    the rest of the Clight program's state. *)
    491 record io_out : Type[0] ≝
    492 { io_function: ident
    493 ; io_args: list eventval
    494 ; io_in_typ: typ
    495 }.
    496 
    497 definition io_in ≝ λo. eventval_type (io_in_typ o).
    498 
    499 definition do_io : ident → list eventval → ∀t:typ. IO io_out io_in (eventval_type t) ≝
    500 λfn,args,t. Interact ??? (mk_io_out fn args t) (λres. Value ??? res).
    501 
    502 definition ret: ∀T. T → (IO io_out io_in T) ≝
    503 λT,x.(Value ?? T x).
    504441
    505442(* execution *)
     
    729666λs.match s with [ State f s k e m ⇒ m | Callstate f a k m ⇒ m | Returnstate r k m ⇒ m ].
    730667
    731 definition clight_exec : execstep
     668definition clight_exec : execstep io_out io_in
    732669  mk_execstep … is_final mem_of_state exec_step.
    733670
    734 definition exec_inf : ∀p:clight_program. execution state io_out io_in ≝
    735 λp.
    736   match make_initial_state p with
    737   [ OK gs ⇒ exec_inf_aux clight_exec (\fst gs) (ret ? 〈E0,\snd gs〉)
    738   | _ ⇒ e_wrong ???
    739   ].
     671definition clight_fullexec : fullexec io_out io_in ≝
     672  mk_fullexec ?? clight_exec ? make_initial_state.
Note: See TracChangeset for help on using the changeset viewer.