Ignore:
Timestamp:
Mar 7, 2013, 12:10:42 PM (7 years ago)
Author:
tranquil
Message:
  • added global notation for existence in Type[1] (\exists[1] x.P)
  • in Arithmetic, reimplemented efficient nat_to_bitvector, but still commented out
  • in joint_semantics, moved out and around some parameters in primitive semantics functions
  • fixed all back end semantics
  • added skeleton files for single passes correctness proofs
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semanticsUtils.ma

    r2783 r2796  
    5050}.
    5151
    52 definition reg_store ≝ λreg,v,locals. OK ? (add RegisterTag beval locals reg v).
     52definition reg_store ≝ λreg,v,locals.add RegisterTag beval locals reg v.
    5353
    5454definition reg_retrieve : register_env beval → register → res beval ≝
     
    5656
    5757definition reg_sp_store ≝ λreg,v,locals.
    58 ! locals' ← reg_store reg v (reg_sp_env locals) ;
    59 return mk_reg_sp locals' (stackp locals).
    60 
    61 definition reg_sp_retrieve ≝ λlocals.reg_retrieve locals.
    62 
     58let locals' ≝ reg_store reg v (reg_sp_env locals) in
     59mk_reg_sp locals' (stackp locals).
     60
     61unification hint 0 ≔ X ⊢ register_env X ≡ identifier_map RegisterTag X.
     62
     63definition reg_sp_retrieve ≝ λlocals : reg_sp.reg_retrieve locals.
     64
     65definition reg_sp_init ≝ mk_reg_sp (empty_map …).
    6366(*** Store/retrieve on hardware registers ***)
    6467
Note: See TracChangeset for help on using the changeset viewer.