Ignore:
Timestamp:
Mar 24, 2013, 11:29:01 AM (7 years ago)
Author:
tranquil
Message:

main novelties:

  • there is an in-built stack_usage nat in joint states, at the base of the new division of RTL's semantics (with separate stacks, with separate stacks but with an artificial overflow error, with a unique stack)
  • a premain is added semantically to the global env, so initial cost label and main call and return are observed
  • proper initialization is now in LINToASM (to be sure, endianess should be checked ;-)

The update breaks proofs of back end atm. compiler.ma should be okay, but I have not had time to complete its compilation.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/TranslateUtils.ma

    r2855 r2946  
    480480@hide_prf
    481481cases def in abs; -def #def #good_def
    482 cases (entry_costed … good_def) #c * #nxt' #EQ >EQ #ABS destruct
     482cases (entry_is_cost … good_def) #nxt' * #c #EQ >EQ #ABS destruct
    483483qed.
    484484
     
    600600  joint_program dst_g_pars ≝
    601601  λsrc,dst,init,p.
    602   transform_program ??? p
    603     (λvarnames.transf_fundef ?? (λdef_in.
    604       b_graph_translate … (init varnames def_in) def_in)).
     602  mk_joint_program ?
     603    (transform_program ??? p
     604      (λvarnames.transf_fundef ?? (λdef_in.
     605        b_graph_translate … (init varnames def_in) def_in)))
     606    (init_cost_label … p).
    605607
    606608definition added_registers :
Note: See TracChangeset for help on using the changeset viewer.