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/ERTL/ERTL_semantics.ma

    r2783 r2796  
    77definition ps_reg_store: ? → ? → ? → res ? ≝
    88 λr,v.λlocal_env : ertl_reg_env.
    9   do res ← reg_store r v (\fst local_env) ;
     9  let res ≝ reg_store r v (\fst local_env) in
    1010  OK … 〈res, \snd local_env〉.
    1111
     
    6464  〈 add … (\fst lenv) reg BVundef, \snd lenv〉.
    6565
    66 (* TODO move into ErrorMessage *)
    67 axiom FramesEmptyOnPop : ErrorMessage.
    68 axiom BlockInFramesCorrupted : ErrorMessage.
    69 axiom FrameErrorOnPush : ErrorMessage.
    70 axiom FrameErrorOnPop : ErrorMessage.
    71 
    7266definition ertl_save_frame:
    7367 call_kind → unit → state_pc ERTL_state → res (state … ERTL_state) ≝
     
    7973  (〈\fst (regs ERTL_state st'),(pc_block (pc ? st))〉 :: frms)
    8074    (set_regs ERTL_state 〈empty_map …,\snd (regs … st')〉 st')).
    81 
    8275
    8376definition ertl_pop_frame:
     
    165158  (* read_result        ≝ *) (λ_.λ_.λ_.
    166159     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
    167   (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.λ_.eval_ertl_seq F gl ge stm id)
     160  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.eval_ertl_seq F gl ge stm id)
    168161  (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.ertl_pop_frame).
    169162
Note: See TracChangeset for help on using the changeset viewer.