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/RTLabs/RTLabs-sem.ma

    r727 r731  
    55include "RTLabs/RTLabs-syntax.ma".
    66
    7 include "common/Values.ma".
    87include "common/Errors.ma".
    9 include "common/Events.ma".
    108include "common/Globalenvs.ma".
    11 include "common/IOMonad.ma".
     9include "common/IO.ma".
    1210include "common/SmallstepExec.ma".
    1311
     
    10199].
    102100
    103 (* XXX below is from Cexec, should have common abstraction. *)
    104 
    105 (* Checking types of values given to / received from an external function call. *)
    106 
    107 definition eventval_type : ∀ty:typ. Type[0] ≝
    108 λty. match ty with [ ASTint ⇒ int | ASTptr _ ⇒ False | ASTfloat ⇒ float ].
    109 
    110 definition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝
    111 λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint ⇒ λv.EVint v | ASTptr r ⇒ ? | ASTfloat ⇒ λv.EVfloat v ].
    112 *; qed.
    113 
    114 definition mk_val: ∀ty:typ. eventval_type ty → val ≝
    115 λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint ⇒ λv.Vint v | ASTptr r ⇒ ? | ASTfloat ⇒ λv.Vfloat v ].
    116 *; qed.
    117 
    118 lemma mk_val_correct: ∀ty:typ. ∀v:eventval_type ty.
    119   eventval_match (mk_eventval ty v) ty (mk_val ty v).
    120 #ty cases ty; normalize; //; * *; qed.
    121 
    122 definition convert_eventval : ∀ev:eventval. ∀ty:typ. res val ≝
    123 λev,ty.
    124 match ty with
    125 [ ASTint ⇒ match ev with [ EVint i ⇒ OK ? (Vint i) | _ ⇒ Error ? ]
    126 | ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? (Vfloat f) | _ ⇒ Error ? ]
    127 | _ ⇒ Error ?
    128 ].
    129 
    130 definition check_eventval' : ∀v:val. ∀ty:typ. res eventval ≝
    131 λv,ty.
    132 match ty with
    133 [ ASTint ⇒ match v with [ Vint i ⇒ OK ? (EVint i) | _ ⇒ Error ? ]
    134 | ASTfloat ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? ]
    135 | _ ⇒ Error ?
    136 ].
    137 
    138 let rec check_eventval_list (vs: list val) (tys: list typ) : res (list eventval) ≝
    139 match vs with
    140 [ nil ⇒ match tys with [ nil ⇒ OK ? (nil ?) | _ ⇒ Error ? ]
    141 | cons v vt ⇒
    142   match tys with
    143   [ nil ⇒ Error ?
    144   | cons ty tyt ⇒
    145     do ev ← check_eventval' v ty;
    146     do evt ← check_eventval_list vt tyt;
    147     OK ? (ev::evt)
    148   ]
    149 ].
    150 
    151 (* IO monad *)
    152 
    153 (* Interactions are function calls that return a value and do not change
    154    the rest of the Clight program's state. *)
    155 record io_out : Type[0] ≝
    156 { io_function: ident
    157 ; io_args: list eventval
    158 ; io_in_typ: typ
    159 }.
    160 
    161 definition io_in ≝ λo. eventval_type (io_in_typ o).
    162 
    163 definition do_io : ident → list eventval → ∀t:typ. IO io_out io_in (eventval_type t) ≝
    164 λfn,args,t. Interact ??? (mk_io_out fn args t) (λres. Value ??? res).
    165 
    166 definition ret: ∀T. T → (IO io_out io_in T) ≝
    167 λT,x.(Value ?? T x).
    168 
    169 (* XXX above is from Cexec, should make common abstraction. *)
    170101
    171102(* XXX put somewhere sensible *)
     
    289220].
    290221
    291 definition RTLabs_exec : execstep
     222definition RTLabs_exec : execstep io_out io_in
    292223  mk_execstep … ? is_final mem_of_state eval_statement.
    293224
     
    300231  OK ? 〈ge,Callstate f (nil ?) (dp ??? [[ ]]) (nil ?) m〉.
    301232
    302 definition exec_inf : ∀p:RTLabs_program. execution state io_out io_in ≝
    303 λp.
    304   match make_initial_state p with
    305   [ OK gs ⇒ exec_inf_aux RTLabs_exec (\fst gs) (ret ? 〈E0,\snd gs〉)
    306   | _ ⇒ e_wrong ???
    307   ].
     233definition RTLabs_fullexec : fullexec io_out io_in ≝
     234  mk_fullexec … RTLabs_exec ? make_initial_state.
     235
Note: See TracChangeset for help on using the changeset viewer.