Changeset 1451 for src/LIN/joint_LTL_LIN_semantics.ma
 Timestamp:
 Oct 22, 2011, 4:18:11 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/LIN/joint_LTL_LIN_semantics.ma
r1415 r1451 5 5 definition hw_reg_retrieve ≝ λl,r. OK … (hwreg_retrieve l r). 6 6 7 (*CSC: reorganize 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. 7 definition ltl_lin_more_sem_params: ∀succT. more_sem_params (mk_params_ ltl_lin_params__ succT) := 8 λsuccT. 10 9 mk_more_sem_params ? 11 unit it hw_register_env init_hw_register_env 0 it succ10 unit it hw_register_env init_hw_register_env 0 it 12 11 hw_reg_store hw_reg_retrieve (λ_.hw_reg_store RegisterA) (λe.λ_.hw_reg_retrieve e RegisterA) 13 12 (λ_.hw_reg_store RegisterB) (λe.λ_.hw_reg_retrieve e RegisterB) … … 21 20  to_acc reg ⇒ 22 21 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 ]). 25 23 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). 24 definition ltl_lin_sem_params: ∀succT. sem_params ≝ 25 λsuccT.mk_sem_params … (ltl_lin_more_sem_params succT). 29 26 30 27 31 28 definition ltl_lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e. 32 29 definition ltl_lin_pop_frame: 33 ∀succT, succ,pointer_of_label,codeT,lookup.30 ∀succT,codeT,lookup. 34 31 ∀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. 37 34 definition 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. 40 37 41 38 (* The following implementation only works for functions that return 32 bits *) 42 39 definition ltl_lin_result_regs: 43 ∀succT, succ,pointer_of_label,codeT,lookup.40 ∀succT,codeT,lookup. 44 41 ∀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. 47 44 48 45 (*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)).46 axiom ltl_lin_fetch_external_args: ∀succT.external_function → state (ltl_lin_sem_params succT) → res (list val). 47 axiom ltl_lin_set_result: ∀succT.list val → state (ltl_lin_sem_params succT) → res (state (ltl_lin_sem_params succT)). 51 48 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. ⊥.49 definition 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. ⊥. 54 51 @abs qed. 55 52 56 53 definition 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). 58 58 ∀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. 60 60 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 …) 63 63 ltl_lin_init_locals (ltl_lin_save_frame …) (ltl_lin_pop_frame …) 64 64 (ltl_lin_fetch_external_args …) (ltl_lin_set_result …)) (ltl_lin_exec_extended …). 65 65 66 66 definition 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.