Ignore:
Timestamp:
Mar 26, 2013, 4:51:40 PM (7 years ago)
Author:
sacerdot
Message:

New extraction, it diverges in RTL execution now.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/interference.ml

    r2951 r2960  
    136136    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    137137let rec decision_rect_Type4 h_decision_spill h_decision_colour = function
    138 | Decision_spill x_19110 -> h_decision_spill x_19110
    139 | Decision_colour x_19111 -> h_decision_colour x_19111
     138| Decision_spill x_281 -> h_decision_spill x_281
     139| Decision_colour x_282 -> h_decision_colour x_282
    140140
    141141(** val decision_rect_Type5 :
    142142    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    143143let rec decision_rect_Type5 h_decision_spill h_decision_colour = function
    144 | Decision_spill x_19115 -> h_decision_spill x_19115
    145 | Decision_colour x_19116 -> h_decision_colour x_19116
     144| Decision_spill x_286 -> h_decision_spill x_286
     145| Decision_colour x_287 -> h_decision_colour x_287
    146146
    147147(** val decision_rect_Type3 :
    148148    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    149149let rec decision_rect_Type3 h_decision_spill h_decision_colour = function
    150 | Decision_spill x_19120 -> h_decision_spill x_19120
    151 | Decision_colour x_19121 -> h_decision_colour x_19121
     150| Decision_spill x_291 -> h_decision_spill x_291
     151| Decision_colour x_292 -> h_decision_colour x_292
    152152
    153153(** val decision_rect_Type2 :
    154154    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    155155let rec decision_rect_Type2 h_decision_spill h_decision_colour = function
    156 | Decision_spill x_19125 -> h_decision_spill x_19125
    157 | Decision_colour x_19126 -> h_decision_colour x_19126
     156| Decision_spill x_296 -> h_decision_spill x_296
     157| Decision_colour x_297 -> h_decision_colour x_297
    158158
    159159(** val decision_rect_Type1 :
    160160    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    161161let rec decision_rect_Type1 h_decision_spill h_decision_colour = function
    162 | Decision_spill x_19130 -> h_decision_spill x_19130
    163 | Decision_colour x_19131 -> h_decision_colour x_19131
     162| Decision_spill x_301 -> h_decision_spill x_301
     163| Decision_colour x_302 -> h_decision_colour x_302
    164164
    165165(** val decision_rect_Type0 :
    166166    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    167167let rec decision_rect_Type0 h_decision_spill h_decision_colour = function
    168 | Decision_spill x_19135 -> h_decision_spill x_19135
    169 | Decision_colour x_19136 -> h_decision_colour x_19136
     168| Decision_spill x_306 -> h_decision_spill x_306
     169| Decision_colour x_307 -> h_decision_colour x_307
    170170
    171171(** val decision_inv_rect_Type4 :
     
    219219    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    220220    __ -> 'a1) -> coloured_graph -> 'a1 **)
    221 let rec coloured_graph_rect_Type4 before h_mk_coloured_graph x_19171 =
    222   let { colouring = colouring0; spilled_no = spilled_no0 } = x_19171 in
     221let rec coloured_graph_rect_Type4 before h_mk_coloured_graph x_342 =
     222  let { colouring = colouring0; spilled_no = spilled_no0 } = x_342 in
    223223  h_mk_coloured_graph colouring0 spilled_no0 __ __
    224224
     
    226226    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    227227    __ -> 'a1) -> coloured_graph -> 'a1 **)
    228 let rec coloured_graph_rect_Type5 before h_mk_coloured_graph x_19173 =
    229   let { colouring = colouring0; spilled_no = spilled_no0 } = x_19173 in
     228let rec coloured_graph_rect_Type5 before h_mk_coloured_graph x_344 =
     229  let { colouring = colouring0; spilled_no = spilled_no0 } = x_344 in
    230230  h_mk_coloured_graph colouring0 spilled_no0 __ __
    231231
     
    233233    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    234234    __ -> 'a1) -> coloured_graph -> 'a1 **)
    235 let rec coloured_graph_rect_Type3 before h_mk_coloured_graph x_19175 =
    236   let { colouring = colouring0; spilled_no = spilled_no0 } = x_19175 in
     235let rec coloured_graph_rect_Type3 before h_mk_coloured_graph x_346 =
     236  let { colouring = colouring0; spilled_no = spilled_no0 } = x_346 in
    237237  h_mk_coloured_graph colouring0 spilled_no0 __ __
    238238
     
    240240    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    241241    __ -> 'a1) -> coloured_graph -> 'a1 **)
    242 let rec coloured_graph_rect_Type2 before h_mk_coloured_graph x_19177 =
    243   let { colouring = colouring0; spilled_no = spilled_no0 } = x_19177 in
     242let rec coloured_graph_rect_Type2 before h_mk_coloured_graph x_348 =
     243  let { colouring = colouring0; spilled_no = spilled_no0 } = x_348 in
    244244  h_mk_coloured_graph colouring0 spilled_no0 __ __
    245245
     
    247247    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    248248    __ -> 'a1) -> coloured_graph -> 'a1 **)
    249 let rec coloured_graph_rect_Type1 before h_mk_coloured_graph x_19179 =
    250   let { colouring = colouring0; spilled_no = spilled_no0 } = x_19179 in
     249let rec coloured_graph_rect_Type1 before h_mk_coloured_graph x_350 =
     250  let { colouring = colouring0; spilled_no = spilled_no0 } = x_350 in
    251251  h_mk_coloured_graph colouring0 spilled_no0 __ __
    252252
     
    254254    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    255255    __ -> 'a1) -> coloured_graph -> 'a1 **)
    256 let rec coloured_graph_rect_Type0 before h_mk_coloured_graph x_19181 =
    257   let { colouring = colouring0; spilled_no = spilled_no0 } = x_19181 in
     256let rec coloured_graph_rect_Type0 before h_mk_coloured_graph x_352 =
     257  let { colouring = colouring0; spilled_no = spilled_no0 } = x_352 in
    258258  h_mk_coloured_graph colouring0 spilled_no0 __ __
    259259
Note: See TracChangeset for help on using the changeset viewer.