Ignore:
Timestamp:
Oct 22, 2011, 4:18:11 AM (8 years ago)
Author:
sacerdot
Message:
  1. All axioms in LIN/semantics.ma closed
  2. succ_pc and pointer_of_label moved to more_sem_params1; their type have been changed too to implement LIN/semantics.ma
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/joint_LTL_LIN_semantics.ma

    r1415 r1451  
    55definition hw_reg_retrieve ≝ λl,r. OK … (hwreg_retrieve l r).
    66
    7 (*CSC: re-organize to take succ_pc out of lin_more_sem_params? *)
    8 definition ltl_lin_more_sem_params: ∀succT,succ,pointer_of_label. more_sem_params (mk_params_ ltl_lin_params__ succT) :=
    9  λsuccT,succ,pointer_of_label.
     7definition ltl_lin_more_sem_params: ∀succT. more_sem_params (mk_params_ ltl_lin_params__ succT) :=
     8 λsuccT.
    109 mk_more_sem_params ?
    11   unit it hw_register_env init_hw_register_env 0 it succ
     10  unit it hw_register_env init_hw_register_env 0 it
    1211   hw_reg_store hw_reg_retrieve (λ_.hw_reg_store RegisterA) (λe.λ_.hw_reg_retrieve e RegisterA)
    1312    (λ_.hw_reg_store RegisterB) (λe.λ_.hw_reg_retrieve e RegisterB)
     
    2120       | to_acc reg ⇒
    2221          do v ← hw_reg_retrieve locals reg ;
    23           hw_reg_store RegisterA v locals ])
    24      pointer_of_label.
     22          hw_reg_store RegisterA v locals ]).
    2523
    26 definition ltl_lin_sem_params:
    27  ∀succT,succ,pointer_of_label. sem_params ≝
    28  λsuccT,succ,pointer_of_label.mk_sem_params … (ltl_lin_more_sem_params succT succ pointer_of_label).
     24definition ltl_lin_sem_params: ∀succT. sem_params ≝
     25 λsuccT.mk_sem_params … (ltl_lin_more_sem_params succT).
    2926
    3027
    3128definition ltl_lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
    3229definition ltl_lin_pop_frame:
    33  ∀succT,succ,pointer_of_label,codeT,lookup.
     30 ∀succT,codeT,lookup.
    3431 ∀globals. genv globals (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) →
    35  state … (ltl_lin_sem_params succT succ pointer_of_label) → res (state … (ltl_lin_sem_params … succ pointer_of_label)) ≝
    36  λ_.λ_.λ_.λ_.λ_.λ_.λ_.λt.OK … t.
     32 state … (ltl_lin_sem_params succT) → res (state … (ltl_lin_sem_params …)) ≝
     33 λ_.λ_.λ_.λ_.λ_.λt.OK … t.
    3734definition ltl_lin_save_frame:
    38  ∀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)) ≝
    39  λ_.λ_.λ_.λl.λ_.λ_.λ_.λ_.λst.save_ra … st l.
     35 ∀succT. address → nat → unit → nat → unit → state … (ltl_lin_sem_params succT) → res (state … (ltl_lin_sem_params …)) ≝
     36 λ_.λl.λ_.λ_.λ_.λ_.λst.save_ra … st l.
    4037
    4138(* The following implementation only works for functions that return 32 bits *)
    4239definition ltl_lin_result_regs:
    43  ∀succT,succ,pointer_of_label,codeT,lookup.
     40 ∀succT,codeT,lookup.
    4441 ∀globals. genv globals (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) →
    45  state (ltl_lin_sem_params succT succ pointer_of_label) → res (list Register) ≝
    46  λ_.λ_.λ_.λ_.λ_.λ_.λ_.λ_. OK … RegisterRets.
     42 state (ltl_lin_sem_params succT) → res (list Register) ≝
     43 λ_.λ_.λ_.λ_.λ_.λ_. OK … RegisterRets.
    4744
    4845(*CSC: XXXX, for external functions only*)
    49 axiom ltl_lin_fetch_external_args: ∀succT,succ,pointer_of_label.external_function → state (ltl_lin_sem_params succT succ pointer_of_label) → res (list val).
    50 axiom ltl_lin_set_result: ∀succT,succ,pointer_of_label.list val → state (ltl_lin_sem_params succT succ pointer_of_label) → res (state (ltl_lin_sem_params … succ pointer_of_label)).
     46axiom ltl_lin_fetch_external_args: ∀succT.external_function → state (ltl_lin_sem_params succT) → res (list val).
     47axiom ltl_lin_set_result: ∀succT.list val → state (ltl_lin_sem_params succT) → res (state (ltl_lin_sem_params succT)).
    5148
    52 definition ltl_lin_exec_extended: ∀succT,succ,pointer_of_label.∀p.∀globals. genv globals (p globals) → False → succT → state (ltl_lin_sem_params succT succ pointer_of_label) → IO io_out io_in (trace × (state (ltl_lin_sem_params … succ pointer_of_label)))
    53  ≝ λsuccT,succ,pointer_of_label,p,globals,ge,abs. ⊥.
     49definition ltl_lin_exec_extended: ∀succT.∀p.∀globals. genv globals (p globals) → False → succT → state (ltl_lin_sem_params succT) → IO io_out io_in (trace × (state (ltl_lin_sem_params succT)))
     50 ≝ λsuccT,p,globals,ge,abs. ⊥.
    5451@abs qed.
    5552
    5653definition ltl_lin_more_sem_params2:
    57  ∀succT,succ,pointer_of_label,codeT,lookup,fetch.
     54 ∀succT,codeT,lookup.∀succ: succT → address → res address.∀fetch.
     55 ∀pointer_of_label: ∀globals. genv globals
     56  (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals))
     57  →pointer→label→res (Σp0:pointer.ptype p0=Code).
    5858 ∀globals. more_sem_params2 … (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) ≝
    59  λsuccT,succ,pointer_of_label,codeT,lookup,fetch,globals.
     59 λsuccT,codeT,lookup,succ,fetch,pointer_of_label,globals.
    6060  mk_more_sem_params2 …
    61    (mk_more_sem_params1 … (ltl_lin_more_sem_params … succ pointer_of_label)
    62     (fetch globals) (load_ra …) (ltl_lin_result_regs …)
     61   (mk_more_sem_params1 … (ltl_lin_more_sem_params …)
     62    succ (pointer_of_label …) (fetch globals) (load_ra …) (ltl_lin_result_regs …)
    6363    ltl_lin_init_locals (ltl_lin_save_frame …) (ltl_lin_pop_frame …)
    6464    (ltl_lin_fetch_external_args …) (ltl_lin_set_result …)) (ltl_lin_exec_extended …).
    6565
    6666definition ltl_lin_fullexec ≝
    67  λsuccT,succ,pointer_of_label,codeT,lookup,fetch.
    68   joint_fullexec … (λp. ltl_lin_more_sem_params2 succT succ pointer_of_label codeT lookup fetch (prog_var_names … p)).
     67 λsuccT,codeT,lookup,succ,fetch,pointer_of_label.
     68  joint_fullexec … (λp. ltl_lin_more_sem_params2 succT codeT lookup succ fetch pointer_of_label (prog_var_names … p)).
Note: See TracChangeset for help on using the changeset viewer.