Ignore:
Timestamp:
Mar 15, 2013, 6:33:18 PM (7 years ago)
Author:
piccolo
Message:

partial commit

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTL.ma

    r2844 r2883  
    2323  the offset does not need the stack size to be computed *)
    2424
     25check ltl_lin_seq
    2526definition preserve_carry_bit :
    26   ∀globals.bool → list (joint_seq LTL globals) → list (joint_seq LTL globals) ≝
     27 (λglobals:list ident
     28  .λdo_it:bool
     29   .λsteps:step_block LTL globals
     30    .if do_it 
     31     then 〈[λ_:code_point LTL.SAVE_CARRY]@ \fst  (\fst  steps),
     32              \snd  (\fst  steps),
     33              \snd  steps@[RESTORE_CARRY]〉 
     34     else steps ).
     35
     36
     37  ∀globals.bool → step_block LTL globals → step_block LTL globals ≝
    2738  λglobals,do_it,steps.
    28   if do_it then SAVE_CARRY :: steps @ [RESTORE_CARRY] else steps.
     39  if do_it then
     40    〈[?] @ (\fst(\fst steps)),
     41     \snd(\fst steps),
     42      (\snd  steps) @ [RESTORE_CARRY]〉
     43  else steps.
     44#_ @SAVE_CARRY
     45qed.
     46check preserve_carry_bit
    2947
    3048(* for notation *)
Note: See TracChangeset for help on using the changeset viewer.