- Timestamp:
- Oct 19, 2011, 4:22:52 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/LIN/joint_LTL_LIN_semantics.ma
r1411 r1415 1 1 include "LIN/joint_LTL_LIN.ma". 2 2 include "joint/SemanticUtils.ma". 3 4 definition hw_reg_store ≝ λr,v,e. OK … (hwreg_store r v e). 5 definition hw_reg_retrieve ≝ λl,r. OK … (hwreg_retrieve l r). 3 6 4 7 (*CSC: re-organize to take succ_pc out of lin_more_sem_params? *) … … 6 9 λsuccT,succ,pointer_of_label. 7 10 mk_more_sem_params ? 8 unit it hw_register_env empty_hw_register_env 0 it succ9 hw reg_store hwreg_retrieve (λ_.hwreg_store RegisterA) (λe.λ_.hwreg_retrieve e RegisterA)10 (λ_.hw reg_store RegisterB) (λe.λ_.hwreg_retrieve e RegisterB)11 (λ_.hw reg_store RegisterDPL) (λe.λ_.hwreg_retrieve e RegisterDPL)12 (λ_.hw reg_store RegisterDPH) (λe.λ_.hwreg_retrieve e RegisterDPH)11 unit it hw_register_env init_hw_register_env 0 it succ 12 hw_reg_store hw_reg_retrieve (λ_.hw_reg_store RegisterA) (λe.λ_.hw_reg_retrieve e RegisterA) 13 (λ_.hw_reg_store RegisterB) (λe.λ_.hw_reg_retrieve e RegisterB) 14 (λ_.hw_reg_store RegisterDPL) (λe.λ_.hw_reg_retrieve e RegisterDPL) 15 (λ_.hw_reg_store RegisterDPH) (λe.λ_.hw_reg_retrieve e RegisterDPH) 13 16 (λlocals,dest_src. 14 17 match dest_src with 15 18 [ from_acc reg ⇒ 16 do v ← hw reg_retrieve locals RegisterA ;17 hw reg_store reg v locals19 do v ← hw_reg_retrieve locals RegisterA ; 20 hw_reg_store reg v locals 18 21 | to_acc reg ⇒ 19 do v ← hw reg_retrieve locals reg ;20 hw reg_store RegisterA v locals ])22 do v ← hw_reg_retrieve locals reg ; 23 hw_reg_store RegisterA v locals ]) 21 24 pointer_of_label. 22 25
Note: See TracChangeset
for help on using the changeset viewer.