Ignore:
Timestamp:
Mar 25, 2013, 11:30:01 PM (7 years ago)
Author:
sacerdot
Message:

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/interference.ml

    r2873 r2951  
    44
    55open Set_adt
     6
     7open Extra_bool
     8
     9open Coqlib
     10
     11open Values
     12
     13open FrontEndVal
     14
     15open GenMem
     16
     17open FrontEndMem
     18
     19open Globalenvs
    620
    721open String
     
    122136    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    123137let rec decision_rect_Type4 h_decision_spill h_decision_colour = function
    124 | Decision_spill x_22007 -> h_decision_spill x_22007
    125 | Decision_colour x_22008 -> h_decision_colour x_22008
     138| Decision_spill x_19110 -> h_decision_spill x_19110
     139| Decision_colour x_19111 -> h_decision_colour x_19111
    126140
    127141(** val decision_rect_Type5 :
    128142    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    129143let rec decision_rect_Type5 h_decision_spill h_decision_colour = function
    130 | Decision_spill x_22012 -> h_decision_spill x_22012
    131 | Decision_colour x_22013 -> h_decision_colour x_22013
     144| Decision_spill x_19115 -> h_decision_spill x_19115
     145| Decision_colour x_19116 -> h_decision_colour x_19116
    132146
    133147(** val decision_rect_Type3 :
    134148    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    135149let rec decision_rect_Type3 h_decision_spill h_decision_colour = function
    136 | Decision_spill x_22017 -> h_decision_spill x_22017
    137 | Decision_colour x_22018 -> h_decision_colour x_22018
     150| Decision_spill x_19120 -> h_decision_spill x_19120
     151| Decision_colour x_19121 -> h_decision_colour x_19121
    138152
    139153(** val decision_rect_Type2 :
    140154    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    141155let rec decision_rect_Type2 h_decision_spill h_decision_colour = function
    142 | Decision_spill x_22022 -> h_decision_spill x_22022
    143 | Decision_colour x_22023 -> h_decision_colour x_22023
     156| Decision_spill x_19125 -> h_decision_spill x_19125
     157| Decision_colour x_19126 -> h_decision_colour x_19126
    144158
    145159(** val decision_rect_Type1 :
    146160    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    147161let rec decision_rect_Type1 h_decision_spill h_decision_colour = function
    148 | Decision_spill x_22027 -> h_decision_spill x_22027
    149 | Decision_colour x_22028 -> h_decision_colour x_22028
     162| Decision_spill x_19130 -> h_decision_spill x_19130
     163| Decision_colour x_19131 -> h_decision_colour x_19131
    150164
    151165(** val decision_rect_Type0 :
    152166    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    153167let rec decision_rect_Type0 h_decision_spill h_decision_colour = function
    154 | Decision_spill x_22032 -> h_decision_spill x_22032
    155 | Decision_colour x_22033 -> h_decision_colour x_22033
     168| Decision_spill x_19135 -> h_decision_spill x_19135
     169| Decision_colour x_19136 -> h_decision_colour x_19136
    156170
    157171(** val decision_inv_rect_Type4 :
     
    205219    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    206220    __ -> 'a1) -> coloured_graph -> 'a1 **)
    207 let rec coloured_graph_rect_Type4 after h_mk_coloured_graph x_22068 =
    208   let { colouring = colouring0; spilled_no = spilled_no0 } = x_22068 in
     221let rec coloured_graph_rect_Type4 before h_mk_coloured_graph x_19171 =
     222  let { colouring = colouring0; spilled_no = spilled_no0 } = x_19171 in
    209223  h_mk_coloured_graph colouring0 spilled_no0 __ __
    210224
     
    212226    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    213227    __ -> 'a1) -> coloured_graph -> 'a1 **)
    214 let rec coloured_graph_rect_Type5 after h_mk_coloured_graph x_22070 =
    215   let { colouring = colouring0; spilled_no = spilled_no0 } = x_22070 in
     228let rec coloured_graph_rect_Type5 before h_mk_coloured_graph x_19173 =
     229  let { colouring = colouring0; spilled_no = spilled_no0 } = x_19173 in
    216230  h_mk_coloured_graph colouring0 spilled_no0 __ __
    217231
     
    219233    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    220234    __ -> 'a1) -> coloured_graph -> 'a1 **)
    221 let rec coloured_graph_rect_Type3 after h_mk_coloured_graph x_22072 =
    222   let { colouring = colouring0; spilled_no = spilled_no0 } = x_22072 in
     235let rec coloured_graph_rect_Type3 before h_mk_coloured_graph x_19175 =
     236  let { colouring = colouring0; spilled_no = spilled_no0 } = x_19175 in
    223237  h_mk_coloured_graph colouring0 spilled_no0 __ __
    224238
     
    226240    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    227241    __ -> 'a1) -> coloured_graph -> 'a1 **)
    228 let rec coloured_graph_rect_Type2 after h_mk_coloured_graph x_22074 =
    229   let { colouring = colouring0; spilled_no = spilled_no0 } = x_22074 in
     242let rec coloured_graph_rect_Type2 before h_mk_coloured_graph x_19177 =
     243  let { colouring = colouring0; spilled_no = spilled_no0 } = x_19177 in
    230244  h_mk_coloured_graph colouring0 spilled_no0 __ __
    231245
     
    233247    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    234248    __ -> 'a1) -> coloured_graph -> 'a1 **)
    235 let rec coloured_graph_rect_Type1 after h_mk_coloured_graph x_22076 =
    236   let { colouring = colouring0; spilled_no = spilled_no0 } = x_22076 in
     249let rec coloured_graph_rect_Type1 before h_mk_coloured_graph x_19179 =
     250  let { colouring = colouring0; spilled_no = spilled_no0 } = x_19179 in
    237251  h_mk_coloured_graph colouring0 spilled_no0 __ __
    238252
     
    240254    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    241255    __ -> 'a1) -> coloured_graph -> 'a1 **)
    242 let rec coloured_graph_rect_Type0 after h_mk_coloured_graph x_22078 =
    243   let { colouring = colouring0; spilled_no = spilled_no0 } = x_22078 in
     256let rec coloured_graph_rect_Type0 before h_mk_coloured_graph x_19181 =
     257  let { colouring = colouring0; spilled_no = spilled_no0 } = x_19181 in
    244258  h_mk_coloured_graph colouring0 spilled_no0 __ __
    245259
    246260(** val colouring :
    247261    Fixpoints.valuation -> coloured_graph -> Liveness.vertex -> decision **)
    248 let rec colouring after xxx =
     262let rec colouring before xxx =
    249263  xxx.colouring
    250264
    251265(** val spilled_no : Fixpoints.valuation -> coloured_graph -> Nat.nat **)
    252 let rec spilled_no after xxx =
     266let rec spilled_no before xxx =
    253267  xxx.spilled_no
    254268
Note: See TracChangeset for help on using the changeset viewer.