Changeset 1250 for src/RTL


Ignore:
Timestamp:
Sep 22, 2011, 12:02:35 PM (9 years ago)
Author:
sacerdot
Message:
  1. Sigma types projections moved to utilities/extralib.ma
  2. Extended statement turned into extended instructions, decreasing the amount of code in the translations
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLtoERTL.ma

    r1245 r1250  
    33include "common/Identifiers.ma".
    44include "ERTL/ERTL.ma".
     5include "utilities/extralib.ma". (* CSC: Only for Sigma type projections *)
    56                     
    67definition add_graph ≝
    7   λl: label.
    8   λstmt.
    9   λp.
    10   let ertl_if_luniverse' ≝ ertl_if_luniverse p in
    11   let ertl_if_runiverse' ≝ ertl_if_runiverse p in
    12   let ertl_if_params' ≝ ertl_if_params p in
    13   let ertl_if_locals' ≝ ertl_if_locals p in
    14   let ertl_if_stacksize' ≝ ertl_if_stacksize p in
    15   let ertl_if_graph' ≝ add ? ? (ertl_if_graph p) l stmt in
    16   let ertl_if_entry' ≝ ertl_if_entry p in
    17   let ertl_if_exit' ≝ ertl_if_exit p in
    18     mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
    19                               ertl_if_params' ertl_if_locals' ertl_if_stacksize'
    20                               ertl_if_graph' ? ?.
     8  λglobals.λl: label.λstmt.λp: joint_internal_function … (ertl_params globals).
     9   let code ≝ add … (joint_if_code … p) l stmt in
     10    mk_joint_internal_function … (ertl_params globals)
     11     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
     12     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
     13     code (pi1 ?? (joint_if_entry … p)) (pi1 … (joint_if_exit … p)).
    2114  normalize nodelta;
    22   [1: generalize in match ertl_if_entry';
    23       #HYP
    24       cases HYP
    25       #LBL #LBL_PRF
    26       %
    27       [1: @LBL
    28       |2: @graph_add_lookup
    29           @LBL_PRF
    30       ]
    31   |2: generalize in match ertl_if_exit';
    32       #HYP
    33       cases HYP
    34       #LBL #LBL_PRF
    35       %
    36       [1: @LBL
    37       |2: @graph_add_lookup
    38           @LBL_PRF
    39       ]
    40   ]
     15  [ cases (joint_if_entry … p) | cases (joint_if_exit … p)]
     16  #LBL #LBL_PRF @graph_add_lookup @LBL_PRF
    4117qed.
    4218                           
    4319definition fresh_label ≝
    44   λdef.
    45     fresh LabelTag (ertl_if_luniverse def).
     20  λglobals.λdef: joint_internal_function … (ertl_params globals).
     21    fresh LabelTag (joint_if_luniverse … def).
    4622   
    4723definition change_label ≝
    48   λl.
    49   λe: ertl_statement.
     24  λglobals.λe: joint_statement ertl_params_ globals.λl.
    5025  match e with
    51   [ ertl_st_skip _ ⇒ ertl_st_skip l
     26  [ joint_st_goto _ ⇒ joint_st_goto … l
     27  | joint_st_return ⇒ joint_st_return …
     28  | joint_st_sequential instr _ ⇒ joint_st_sequential … instr l
     29  | joint_st_extension ].
    5230  | ertl_st_comment s _ ⇒ ertl_st_comment s l
    5331  | ertl_st_cost c _ ⇒ ertl_st_cost c l
Note: See TracChangeset for help on using the changeset viewer.