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/RTL/RTL_semantics.ma

    r2935 r2946  
    247247      rtl_fetch_external_args
    248248      rtl_set_result
    249       [ ] [ ]
     249      [ ]
     250      [an_identifier … one ; an_identifier … (p0 one) ;
     251       an_identifier … (p1 one) ; an_identifier … (p0 (p0 one)) ]
    250252      (λ_.λ_.rtl_read_result) 
    251253      (λ_.λ_.eval_rtl_seq)
    252       (λ_.λ_.λ_.rtl_pop_frame_separate)).
     254      (λ_.λ_.λ_.rtl_pop_frame_separate))
     255    RTL_premain.
    253256
    254257definition RTL_semantics_separate_overflow ≝
     
    268271      rtl_fetch_external_args
    269272      rtl_set_result
    270       [ ] [ ]
     273      [ ]
     274      [an_identifier … one ; an_identifier … (p0 one) ;
     275       an_identifier … (p1 one) ; an_identifier … (p0 (p0 one)) ]
    271276      (λ_.λ_.rtl_read_result) 
    272277      (λ_.λ_.eval_rtl_seq)
    273       (λ_.λ_.λ_.rtl_pop_frame_separate)).
     278      (λ_.λ_.λ_.rtl_pop_frame_separate))
     279    RTL_premain.
    274280
    275281definition RTL_semantics_unique ≝
     
    289295      rtl_fetch_external_args
    290296      rtl_set_result
    291       [ ] [ ]
     297      [ ]
     298      [an_identifier … one ; an_identifier … (p0 one) ;
     299       an_identifier … (p1 one) ; an_identifier … (p0 (p0 one)) ]
    292300      (λ_.λ_.rtl_read_result) 
    293301      (λ_.λ_.eval_rtl_seq)
    294       (λ_.λ_.λ_.rtl_pop_frame_unique)).
     302      (λ_.λ_.λ_.rtl_pop_frame_unique))
     303    RTL_premain.
     304     
Note: See TracChangeset for help on using the changeset viewer.