Ignore:
Timestamp:
Mar 7, 2013, 12:55:34 PM (8 years ago)
Author:
sacerdot
Message:

Extracted again after James's cleanup and the implementation of the
new testing function to be used in the untrusted code.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/interference.ml

    r2775 r2797  
    122122    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    123123let rec decision_rect_Type4 h_decision_spill h_decision_colour = function
    124 | Decision_spill x_21633 -> h_decision_spill x_21633
    125 | Decision_colour x_21634 -> h_decision_colour x_21634
     124| Decision_spill x_21712 -> h_decision_spill x_21712
     125| Decision_colour x_21713 -> h_decision_colour x_21713
    126126
    127127(** val decision_rect_Type5 :
    128128    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    129129let rec decision_rect_Type5 h_decision_spill h_decision_colour = function
    130 | Decision_spill x_21638 -> h_decision_spill x_21638
    131 | Decision_colour x_21639 -> h_decision_colour x_21639
     130| Decision_spill x_21717 -> h_decision_spill x_21717
     131| Decision_colour x_21718 -> h_decision_colour x_21718
    132132
    133133(** val decision_rect_Type3 :
    134134    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    135135let rec decision_rect_Type3 h_decision_spill h_decision_colour = function
    136 | Decision_spill x_21643 -> h_decision_spill x_21643
    137 | Decision_colour x_21644 -> h_decision_colour x_21644
     136| Decision_spill x_21722 -> h_decision_spill x_21722
     137| Decision_colour x_21723 -> h_decision_colour x_21723
    138138
    139139(** val decision_rect_Type2 :
    140140    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    141141let rec decision_rect_Type2 h_decision_spill h_decision_colour = function
    142 | Decision_spill x_21648 -> h_decision_spill x_21648
    143 | Decision_colour x_21649 -> h_decision_colour x_21649
     142| Decision_spill x_21727 -> h_decision_spill x_21727
     143| Decision_colour x_21728 -> h_decision_colour x_21728
    144144
    145145(** val decision_rect_Type1 :
    146146    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    147147let rec decision_rect_Type1 h_decision_spill h_decision_colour = function
    148 | Decision_spill x_21653 -> h_decision_spill x_21653
    149 | Decision_colour x_21654 -> h_decision_colour x_21654
     148| Decision_spill x_21732 -> h_decision_spill x_21732
     149| Decision_colour x_21733 -> h_decision_colour x_21733
    150150
    151151(** val decision_rect_Type0 :
    152152    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    153153let rec decision_rect_Type0 h_decision_spill h_decision_colour = function
    154 | Decision_spill x_21658 -> h_decision_spill x_21658
    155 | Decision_colour x_21659 -> h_decision_colour x_21659
     154| Decision_spill x_21737 -> h_decision_spill x_21737
     155| Decision_colour x_21738 -> h_decision_colour x_21738
    156156
    157157(** val decision_inv_rect_Type4 :
     
    205205    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    206206    __ -> 'a1) -> coloured_graph -> 'a1 **)
    207 let rec coloured_graph_rect_Type4 after h_mk_coloured_graph x_21694 =
    208   let { colouring = colouring0; spilled_no = spilled_no0 } = x_21694 in
     207let rec coloured_graph_rect_Type4 after h_mk_coloured_graph x_21773 =
     208  let { colouring = colouring0; spilled_no = spilled_no0 } = x_21773 in
    209209  h_mk_coloured_graph colouring0 spilled_no0 __ __
    210210
     
    212212    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    213213    __ -> 'a1) -> coloured_graph -> 'a1 **)
    214 let rec coloured_graph_rect_Type5 after h_mk_coloured_graph x_21696 =
    215   let { colouring = colouring0; spilled_no = spilled_no0 } = x_21696 in
     214let rec coloured_graph_rect_Type5 after h_mk_coloured_graph x_21775 =
     215  let { colouring = colouring0; spilled_no = spilled_no0 } = x_21775 in
    216216  h_mk_coloured_graph colouring0 spilled_no0 __ __
    217217
     
    219219    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    220220    __ -> 'a1) -> coloured_graph -> 'a1 **)
    221 let rec coloured_graph_rect_Type3 after h_mk_coloured_graph x_21698 =
    222   let { colouring = colouring0; spilled_no = spilled_no0 } = x_21698 in
     221let rec coloured_graph_rect_Type3 after h_mk_coloured_graph x_21777 =
     222  let { colouring = colouring0; spilled_no = spilled_no0 } = x_21777 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_Type2 after h_mk_coloured_graph x_21700 =
    229   let { colouring = colouring0; spilled_no = spilled_no0 } = x_21700 in
     228let rec coloured_graph_rect_Type2 after h_mk_coloured_graph x_21779 =
     229  let { colouring = colouring0; spilled_no = spilled_no0 } = x_21779 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_Type1 after h_mk_coloured_graph x_21702 =
    236   let { colouring = colouring0; spilled_no = spilled_no0 } = x_21702 in
     235let rec coloured_graph_rect_Type1 after h_mk_coloured_graph x_21781 =
     236  let { colouring = colouring0; spilled_no = spilled_no0 } = x_21781 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_Type0 after h_mk_coloured_graph x_21704 =
    243   let { colouring = colouring0; spilled_no = spilled_no0 } = x_21704 in
     242let rec coloured_graph_rect_Type0 after h_mk_coloured_graph x_21783 =
     243  let { colouring = colouring0; spilled_no = spilled_no0 } = x_21783 in
    244244  h_mk_coloured_graph colouring0 spilled_no0 __ __
    245245
Note: See TracChangeset for help on using the changeset viewer.