Ignore:
Timestamp:
Mar 21, 2011, 6:27:22 PM (9 years ago)
Author:
campbell
Message:

Refine small-step executable semantics abstraction a little.
Some progress on using the new definition in CexecEquiv?, but only partial
because of over-eager normalisation by the destruct tactic.
Whole program semantics for RTLabs using it.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabs-sem.ma

    r693 r702  
    55include "RTLabs/RTLabs-syntax.ma".
    66
    7 include "Values.ma".
    8 include "Errors.ma".
    9 include "Events.ma".
    10 include "Globalenvs.ma".
    11 include "IOMonad.ma".
    12 include "SmallstepExec.ma".
     7include "common/Values.ma".
     8include "common/Errors.ma".
     9include "common/Events.ma".
     10include "common/Globalenvs.ma".
     11include "common/IOMonad.ma".
     12include "common/SmallstepExec.ma".
    1313
    1414definition genv ≝ (genv_t Genv) (fundef internal_function).
     
    287287].
    288288
    289 definition RTLabs_exec : RTLabs_program → execstep ≝
    290 λp. mk_execstep … ? is_final mem_of_state eval_statement.
     289definition RTLabs_exec : execstep ≝
     290  mk_execstep … ? is_final mem_of_state eval_statement.
     291
     292definition make_initial_state : RTLabs_program → res (genv × state) ≝
     293λp.
     294  do ge ← globalenv Genv ?? p;
     295  do m ← init_mem Genv ?? p;
     296  do b ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p));
     297  do f ← opt_to_res ? (find_funct_ptr ? ? ge b);
     298  OK ? 〈ge,Callstate f (nil ?) (dp ??? [[ ]]) (nil ?) m〉.
     299
     300definition exec_inf : ∀p:RTLabs_program. execution state io_out io_in ≝
     301λp.
     302  match make_initial_state p with
     303  [ OK gs ⇒ exec_inf_aux RTLabs_exec (\fst gs) (ret ? 〈E0,\snd gs〉)
     304  | _ ⇒ e_wrong ???
     305  ].
Note: See TracChangeset for help on using the changeset viewer.