Changeset 1245 for src/RTL


Ignore:
Timestamp:
Sep 21, 2011, 10:22:13 PM (9 years ago)
Author:
sacerdot
Message:

RTLtoERTL and LINToASM: porting to new Joint data type in progress.
However, it seems better to go back to a Joint representation where
the "mapping" from label to internal functions is more concrete.
To be done.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLtoERTL.ma

    r1149 r1245  
    1 include "RTL/RTL.ma".
    21include "RTL/RTLTailcall.ma".
    32include "utilities/RegisterSet.ma".
    43include "common/Identifiers.ma".
    54include "ERTL/ERTL.ma".
    6 
    7 definition change_exit_label ≝
    8   λl: label.
    9   λp: ertl_internal_function.
    10   λprf: lookup ? ? (ertl_if_graph p) l ≠ None ?.
    11   let ertl_if_luniverse' ≝ ertl_if_luniverse p in
    12   let ertl_if_runiverse' ≝ ertl_if_runiverse p in
    13   let ertl_if_params' ≝ ertl_if_params p in
    14   let ertl_if_locals' ≝ ertl_if_locals p in
    15   let ertl_if_stacksize' ≝ ertl_if_stacksize p in
    16   let ertl_if_graph' ≝ ertl_if_graph p in
    17   let ertl_if_entry' ≝ ertl_if_entry p in
    18   let ertl_if_exit' ≝ l in
    19     mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
    20                               ertl_if_params' ertl_if_locals' ertl_if_stacksize'
    21                               ertl_if_graph' ertl_if_entry' ertl_if_exit'.
    22   @prf
    23 qed.
    24 
    25 definition change_entry_label ≝
    26   λl: label.
    27   λp: ertl_internal_function.
    28   λprf: lookup ? ? (ertl_if_graph p) l ≠ None ?.
    29   let ertl_if_luniverse' ≝ ertl_if_luniverse p in
    30   let ertl_if_runiverse' ≝ ertl_if_runiverse p in
    31   let ertl_if_params' ≝ ertl_if_params p in
    32   let ertl_if_locals' ≝ ertl_if_locals p in
    33   let ertl_if_stacksize' ≝ ertl_if_stacksize p in
    34   let ertl_if_graph' ≝ ertl_if_graph p in
    35   let ertl_if_entry' ≝ l in
    36   let ertl_if_exit' ≝ ertl_if_exit p in
    37     mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
    38                               ertl_if_params' ertl_if_locals' ertl_if_stacksize'
    39                               ertl_if_graph' ertl_if_entry' ertl_if_exit'.
    40   @prf
    41 qed.
    42                              
     5                     
    436definition add_graph ≝
    447  λl: label.
     
    7740  ]
    7841qed.
    79                             
     42                           
    8043definition fresh_label ≝
    8144  λdef.
     
    351314    in
    352315    let def ≝ add_graph tmp_lbl last_stmt def in
    353       change_exit_label tmp_lbl def ?
     316      set_joint_if_exit … tmp_lbl def ?
    354317  ] ?.
    355318  cases not_implemented (* dep types here, bug in matita too! *)
Note: See TracChangeset for help on using the changeset viewer.