Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (8 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/interference.ml

    r2743 r2773  
    1313open LabelledObjects
    1414
     15open BitVectorTrie
     16
    1517open Graphs
    1618
     
    2123open Registers
    2224
    23 open BitVectorTrie
    24 
    2525open CostLabel
    2626
     
    4141open Extralib
    4242
     43open Lists
     44
     45open Identifiers
     46
     47open Integers
     48
     49open AST
     50
     51open Division
     52
     53open Exp
     54
     55open Arithmetic
     56
    4357open Setoids
    4458
     
    4660
    4761open Option
    48 
    49 open Lists
    50 
    51 open Identifiers
    52 
    53 open Integers
    54 
    55 open AST
    56 
    57 open Division
    58 
    59 open Exp
    60 
    61 open Arithmetic
    6262
    6363open Extranat
     
    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_21583 -> h_decision_spill x_21583
    125 | Decision_colour x_21584 -> h_decision_colour x_21584
     124| Decision_spill x_16893 -> h_decision_spill x_16893
     125| Decision_colour x_16894 -> h_decision_colour x_16894
    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_21588 -> h_decision_spill x_21588
    131 | Decision_colour x_21589 -> h_decision_colour x_21589
     130| Decision_spill x_16898 -> h_decision_spill x_16898
     131| Decision_colour x_16899 -> h_decision_colour x_16899
    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_21593 -> h_decision_spill x_21593
    137 | Decision_colour x_21594 -> h_decision_colour x_21594
     136| Decision_spill x_16903 -> h_decision_spill x_16903
     137| Decision_colour x_16904 -> h_decision_colour x_16904
    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_21598 -> h_decision_spill x_21598
    143 | Decision_colour x_21599 -> h_decision_colour x_21599
     142| Decision_spill x_16908 -> h_decision_spill x_16908
     143| Decision_colour x_16909 -> h_decision_colour x_16909
    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_21603 -> h_decision_spill x_21603
    149 | Decision_colour x_21604 -> h_decision_colour x_21604
     148| Decision_spill x_16913 -> h_decision_spill x_16913
     149| Decision_colour x_16914 -> h_decision_colour x_16914
    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_21608 -> h_decision_spill x_21608
    155 | Decision_colour x_21609 -> h_decision_colour x_21609
     154| Decision_spill x_16918 -> h_decision_spill x_16918
     155| Decision_colour x_16919 -> h_decision_colour x_16919
    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_21644 =
    208   let { colouring = colouring0; spilled_no = spilled_no0 } = x_21644 in
     207let rec coloured_graph_rect_Type4 after h_mk_coloured_graph x_16954 =
     208  let { colouring = colouring0; spilled_no = spilled_no0 } = x_16954 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_21646 =
    215   let { colouring = colouring0; spilled_no = spilled_no0 } = x_21646 in
     214let rec coloured_graph_rect_Type5 after h_mk_coloured_graph x_16956 =
     215  let { colouring = colouring0; spilled_no = spilled_no0 } = x_16956 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_21648 =
    222   let { colouring = colouring0; spilled_no = spilled_no0 } = x_21648 in
     221let rec coloured_graph_rect_Type3 after h_mk_coloured_graph x_16958 =
     222  let { colouring = colouring0; spilled_no = spilled_no0 } = x_16958 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_21650 =
    229   let { colouring = colouring0; spilled_no = spilled_no0 } = x_21650 in
     228let rec coloured_graph_rect_Type2 after h_mk_coloured_graph x_16960 =
     229  let { colouring = colouring0; spilled_no = spilled_no0 } = x_16960 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_21652 =
    236   let { colouring = colouring0; spilled_no = spilled_no0 } = x_21652 in
     235let rec coloured_graph_rect_Type1 after h_mk_coloured_graph x_16962 =
     236  let { colouring = colouring0; spilled_no = spilled_no0 } = x_16962 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_21654 =
    243   let { colouring = colouring0; spilled_no = spilled_no0 } = x_21654 in
     242let rec coloured_graph_rect_Type0 after h_mk_coloured_graph x_16964 =
     243  let { colouring = colouring0; spilled_no = spilled_no0 } = x_16964 in
    244244  h_mk_coloured_graph colouring0 spilled_no0 __ __
    245245
Note: See TracChangeset for help on using the changeset viewer.