Changeset 2775 for extracted/rTL.ml


Ignore:
Timestamp:
Mar 5, 2013, 9:52:39 PM (7 years ago)
Author:
sacerdot
Message:

The compiler now computes also the stack cost model.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/rTL.ml

    r2773 r2775  
    111111    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    112112let rec rtl_seq_rect_Type4 h_rtl_stack_address = function
    113 | Rtl_stack_address (x_15879, x_15878) -> h_rtl_stack_address x_15879 x_15878
     113| Rtl_stack_address (x_20710, x_20709) -> h_rtl_stack_address x_20710 x_20709
    114114
    115115(** val rtl_seq_rect_Type5 :
    116116    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    117117let rec rtl_seq_rect_Type5 h_rtl_stack_address = function
    118 | Rtl_stack_address (x_15883, x_15882) -> h_rtl_stack_address x_15883 x_15882
     118| Rtl_stack_address (x_20714, x_20713) -> h_rtl_stack_address x_20714 x_20713
    119119
    120120(** val rtl_seq_rect_Type3 :
    121121    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    122122let rec rtl_seq_rect_Type3 h_rtl_stack_address = function
    123 | Rtl_stack_address (x_15887, x_15886) -> h_rtl_stack_address x_15887 x_15886
     123| Rtl_stack_address (x_20718, x_20717) -> h_rtl_stack_address x_20718 x_20717
    124124
    125125(** val rtl_seq_rect_Type2 :
    126126    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    127127let rec rtl_seq_rect_Type2 h_rtl_stack_address = function
    128 | Rtl_stack_address (x_15891, x_15890) -> h_rtl_stack_address x_15891 x_15890
     128| Rtl_stack_address (x_20722, x_20721) -> h_rtl_stack_address x_20722 x_20721
    129129
    130130(** val rtl_seq_rect_Type1 :
    131131    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    132132let rec rtl_seq_rect_Type1 h_rtl_stack_address = function
    133 | Rtl_stack_address (x_15895, x_15894) -> h_rtl_stack_address x_15895 x_15894
     133| Rtl_stack_address (x_20726, x_20725) -> h_rtl_stack_address x_20726 x_20725
    134134
    135135(** val rtl_seq_rect_Type0 :
    136136    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    137137let rec rtl_seq_rect_Type0 h_rtl_stack_address = function
    138 | Rtl_stack_address (x_15899, x_15898) -> h_rtl_stack_address x_15899 x_15898
     138| Rtl_stack_address (x_20730, x_20729) -> h_rtl_stack_address x_20730 x_20729
    139139
    140140(** val rtl_seq_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.