Changeset 1385 for src/LIN


Ignore:
Timestamp:
Oct 17, 2011, 1:40:13 AM (8 years ago)
Author:
sacerdot
Message:
  1. fetch_result and pop_frame now takes the genv in input
  2. implementation of fetch_result for RTL completed All RTL axioms but the ones related to external functions are now closed.
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/joint_LTL_LIN_semantics.ma

    r1384 r1385  
    2828definition ltl_lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
    2929definition ltl_lin_pop_frame:
    30  ∀succT,succ,pointer_of_label. state … (ltl_lin_sem_params succT succ pointer_of_label) → res (state … (ltl_lin_sem_params … succ pointer_of_label)) ≝
    31  λ_.λ_.λ_.λt.OK … t.
     30 ∀succT,succ,pointer_of_label,codeT,lookup.
     31 ∀globals. genv globals (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) →
     32 state … (ltl_lin_sem_params succT succ pointer_of_label) → res (state … (ltl_lin_sem_params … succ pointer_of_label)) ≝
     33 λ_.λ_.λ_.λ_.λ_.λ_.λ_.λt.OK … t.
    3234definition ltl_lin_save_frame:
    3335 ∀succT,succ,pointer_of_label. address → nat → unit → nat → unit → state … (ltl_lin_sem_params succT succ pointer_of_label) → res (state … (ltl_lin_sem_params … succ pointer_of_label)) ≝
     
    3739 λsuccT,succ,pointer_of_label.
    3840 mk_more_sem_params1 ? ltl_lin_params1 (ltl_lin_more_sem_params succT succ pointer_of_label)
    39   ltl_lin_init_locals (ltl_lin_pop_frame …) (ltl_lin_save_frame …).
     41  ltl_lin_init_locals (ltl_lin_save_frame …).
    4042
    4143(*CSC: XXXXX, for is_final only *)
    42 axiom ltl_lin_fetch_result: ∀succT,succ,pointer_of_label.state (ltl_lin_sem_params succT succ pointer_of_label) → res (list beval).
     44axiom ltl_lin_fetch_result:
     45 ∀succT,succ,pointer_of_label,codeT,lookup.
     46 ∀globals. genv globals (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) →
     47 state (ltl_lin_sem_params succT succ pointer_of_label) → res (list beval).
    4348
    4449(*CSC: XXXX, for external functions only*)
     
    5560 λsuccT,succ,pointer_of_label,codeT,lookup,fetch,globals.
    5661  mk_more_sem_params2 … (ltl_lin_more_sem_params1 … succ pointer_of_label)
    57    (fetch globals) (load_ra …) (ltl_lin_fetch_result …)
    58    (ltl_lin_fetch_external_args …)
    59    (ltl_lin_set_result …) (ltl_lin_exec_extended …).
     62   (fetch globals) (load_ra …) (ltl_lin_fetch_result …) (ltl_lin_pop_frame …)
     63   (ltl_lin_fetch_external_args …) (ltl_lin_set_result …) (ltl_lin_exec_extended …).
    6064
    6165definition ltl_lin_fullexec ≝
Note: See TracChangeset for help on using the changeset viewer.