Changeset 702 for src/Clight/Cexec.ma


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

    r700 r702  
    719719].
    720720
    721 definition clight_exec : clight_program → execstep ≝
    722 λp. mk_execstep … (initial_state p) is_final mem_of_state exec_step.
    723 
    724 definition exec_inf : ∀p:clight_program. execution (state (clight_exec p)) io_out io_in ≝
     721definition clight_exec : execstep ≝
     722  mk_execstep … is_final mem_of_state exec_step.
     723
     724definition exec_inf : ∀p:clight_program. execution state io_out io_in ≝
    725725λp.
    726726  match make_initial_state p with
    727   [ OK gs ⇒ exec_inf_aux (clight_exec p) (\fst gs) (ret ? 〈E0,\snd gs〉)
     727  [ OK gs ⇒ exec_inf_aux clight_exec (\fst gs) (ret ? 〈E0,\snd gs〉)
    728728  | _ ⇒ e_wrong ???
    729729  ].
Note: See TracChangeset for help on using the changeset viewer.