Changeset 1415 for src/LIN


Ignore:
Timestamp:
Oct 19, 2011, 4:22:52 PM (8 years ago)
Author:
sacerdot
Message:
  1. hwreg_store/retrieve no longer returns a res (but it is still axiomatized)
  2. added initialization of local environment that sets the sp in the appropriate way
  3. ASM/I8051 splitted into ASM/I8051bis because of some bugs with disambiguation
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/joint_LTL_LIN_semantics.ma

    r1411 r1415  
    11include "LIN/joint_LTL_LIN.ma".
    22include "joint/SemanticUtils.ma".
     3
     4definition hw_reg_store ≝ λr,v,e. OK … (hwreg_store r v e).
     5definition hw_reg_retrieve ≝ λl,r. OK … (hwreg_retrieve l r).
    36
    47(*CSC: re-organize to take succ_pc out of lin_more_sem_params? *)
     
    69 λsuccT,succ,pointer_of_label.
    710 mk_more_sem_params ?
    8   unit it hw_register_env empty_hw_register_env 0 it succ
    9    hwreg_store hwreg_retrieve (λ_.hwreg_store RegisterA) (λe.λ_.hwreg_retrieve e RegisterA)
    10     (λ_.hwreg_store RegisterB) (λe.λ_.hwreg_retrieve e RegisterB)
    11     (λ_.hwreg_store RegisterDPL) (λe.λ_.hwreg_retrieve e RegisterDPL)
    12     (λ_.hwreg_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)
    1316     (λlocals,dest_src.
    1417       match dest_src with
    1518       [ from_acc reg ⇒
    16           do v ← hwreg_retrieve locals RegisterA ;
    17           hwreg_store reg v locals
     19          do v ← hw_reg_retrieve locals RegisterA ;
     20          hw_reg_store reg v locals
    1821       | to_acc reg ⇒
    19           do v ← hwreg_retrieve locals reg ;
    20           hwreg_store RegisterA v locals ])
     22          do v ← hw_reg_retrieve locals reg ;
     23          hw_reg_store RegisterA v locals ])
    2124     pointer_of_label.
    2225
Note: See TracChangeset for help on using the changeset viewer.