Ignore:
Timestamp:
Mar 28, 2013, 5:27:46 PM (7 years ago)
Author:
sacerdot
Message:

New extraction after ERTLptr abortion.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/interference.ml

    r3001 r3019  
    9898
    9999open ERTL
    100 
    101 open ERTLptr
    102100
    103101open Div_and_mod
     
    136134    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    137135let rec decision_rect_Type4 h_decision_spill h_decision_colour = function
    138 | Decision_spill x_5765 -> h_decision_spill x_5765
    139 | Decision_colour x_5766 -> h_decision_colour x_5766
     136| Decision_spill x_7 -> h_decision_spill x_7
     137| Decision_colour x_8 -> h_decision_colour x_8
    140138
    141139(** val decision_rect_Type5 :
    142140    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    143141let rec decision_rect_Type5 h_decision_spill h_decision_colour = function
    144 | Decision_spill x_5770 -> h_decision_spill x_5770
    145 | Decision_colour x_5771 -> h_decision_colour x_5771
     142| Decision_spill x_12 -> h_decision_spill x_12
     143| Decision_colour x_13 -> h_decision_colour x_13
    146144
    147145(** val decision_rect_Type3 :
    148146    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    149147let rec decision_rect_Type3 h_decision_spill h_decision_colour = function
    150 | Decision_spill x_5775 -> h_decision_spill x_5775
    151 | Decision_colour x_5776 -> h_decision_colour x_5776
     148| Decision_spill x_17 -> h_decision_spill x_17
     149| Decision_colour x_18 -> h_decision_colour x_18
    152150
    153151(** val decision_rect_Type2 :
    154152    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    155153let rec decision_rect_Type2 h_decision_spill h_decision_colour = function
    156 | Decision_spill x_5780 -> h_decision_spill x_5780
    157 | Decision_colour x_5781 -> h_decision_colour x_5781
     154| Decision_spill x_22 -> h_decision_spill x_22
     155| Decision_colour x_23 -> h_decision_colour x_23
    158156
    159157(** val decision_rect_Type1 :
    160158    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    161159let rec decision_rect_Type1 h_decision_spill h_decision_colour = function
    162 | Decision_spill x_5785 -> h_decision_spill x_5785
    163 | Decision_colour x_5786 -> h_decision_colour x_5786
     160| Decision_spill x_27 -> h_decision_spill x_27
     161| Decision_colour x_28 -> h_decision_colour x_28
    164162
    165163(** val decision_rect_Type0 :
    166164    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    167165let rec decision_rect_Type0 h_decision_spill h_decision_colour = function
    168 | Decision_spill x_5790 -> h_decision_spill x_5790
    169 | Decision_colour x_5791 -> h_decision_colour x_5791
     166| Decision_spill x_32 -> h_decision_spill x_32
     167| Decision_colour x_33 -> h_decision_colour x_33
    170168
    171169(** val decision_inv_rect_Type4 :
     
    219217    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    220218    __ -> 'a1) -> coloured_graph -> 'a1 **)
    221 let rec coloured_graph_rect_Type4 before h_mk_coloured_graph x_5826 =
    222   let { colouring = colouring0; spilled_no = spilled_no0 } = x_5826 in
     219let rec coloured_graph_rect_Type4 before h_mk_coloured_graph x_68 =
     220  let { colouring = colouring0; spilled_no = spilled_no0 } = x_68 in
    223221  h_mk_coloured_graph colouring0 spilled_no0 __ __
    224222
     
    226224    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    227225    __ -> 'a1) -> coloured_graph -> 'a1 **)
    228 let rec coloured_graph_rect_Type5 before h_mk_coloured_graph x_5828 =
    229   let { colouring = colouring0; spilled_no = spilled_no0 } = x_5828 in
     226let rec coloured_graph_rect_Type5 before h_mk_coloured_graph x_70 =
     227  let { colouring = colouring0; spilled_no = spilled_no0 } = x_70 in
    230228  h_mk_coloured_graph colouring0 spilled_no0 __ __
    231229
     
    233231    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    234232    __ -> 'a1) -> coloured_graph -> 'a1 **)
    235 let rec coloured_graph_rect_Type3 before h_mk_coloured_graph x_5830 =
    236   let { colouring = colouring0; spilled_no = spilled_no0 } = x_5830 in
     233let rec coloured_graph_rect_Type3 before h_mk_coloured_graph x_72 =
     234  let { colouring = colouring0; spilled_no = spilled_no0 } = x_72 in
    237235  h_mk_coloured_graph colouring0 spilled_no0 __ __
    238236
     
    240238    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    241239    __ -> 'a1) -> coloured_graph -> 'a1 **)
    242 let rec coloured_graph_rect_Type2 before h_mk_coloured_graph x_5832 =
    243   let { colouring = colouring0; spilled_no = spilled_no0 } = x_5832 in
     240let rec coloured_graph_rect_Type2 before h_mk_coloured_graph x_74 =
     241  let { colouring = colouring0; spilled_no = spilled_no0 } = x_74 in
    244242  h_mk_coloured_graph colouring0 spilled_no0 __ __
    245243
     
    247245    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    248246    __ -> 'a1) -> coloured_graph -> 'a1 **)
    249 let rec coloured_graph_rect_Type1 before h_mk_coloured_graph x_5834 =
    250   let { colouring = colouring0; spilled_no = spilled_no0 } = x_5834 in
     247let rec coloured_graph_rect_Type1 before h_mk_coloured_graph x_76 =
     248  let { colouring = colouring0; spilled_no = spilled_no0 } = x_76 in
    251249  h_mk_coloured_graph colouring0 spilled_no0 __ __
    252250
     
    254252    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    255253    __ -> 'a1) -> coloured_graph -> 'a1 **)
    256 let rec coloured_graph_rect_Type0 before h_mk_coloured_graph x_5836 =
    257   let { colouring = colouring0; spilled_no = spilled_no0 } = x_5836 in
     254let rec coloured_graph_rect_Type0 before h_mk_coloured_graph x_78 =
     255  let { colouring = colouring0; spilled_no = spilled_no0 } = x_78 in
    258256  h_mk_coloured_graph colouring0 spilled_no0 __ __
    259257
Note: See TracChangeset for help on using the changeset viewer.