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/fixpoints.ml

    r2873 r2951  
    8080    (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
    8181    Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
    82 let rec property_lattice_rect_Type4 h_mk_property_lattice x_21945 =
    83   let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
    84     l_is_maximal = l_is_maximal0 } = x_21945
     82let rec property_lattice_rect_Type4 h_mk_property_lattice x_19049 =
     83  let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
     84    l_is_maximal = l_is_maximal0 } = x_19049
    8585  in
    8686  h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0
     
    8989    (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
    9090    Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
    91 let rec property_lattice_rect_Type5 h_mk_property_lattice x_21947 =
    92   let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
    93     l_is_maximal = l_is_maximal0 } = x_21947
     91let rec property_lattice_rect_Type5 h_mk_property_lattice x_19051 =
     92  let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
     93    l_is_maximal = l_is_maximal0 } = x_19051
    9494  in
    9595  h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0
     
    9898    (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
    9999    Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
    100 let rec property_lattice_rect_Type3 h_mk_property_lattice x_21949 =
    101   let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
    102     l_is_maximal = l_is_maximal0 } = x_21949
     100let rec property_lattice_rect_Type3 h_mk_property_lattice x_19053 =
     101  let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
     102    l_is_maximal = l_is_maximal0 } = x_19053
    103103  in
    104104  h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0
     
    107107    (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
    108108    Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
    109 let rec property_lattice_rect_Type2 h_mk_property_lattice x_21951 =
    110   let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
    111     l_is_maximal = l_is_maximal0 } = x_21951
     109let rec property_lattice_rect_Type2 h_mk_property_lattice x_19055 =
     110  let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
     111    l_is_maximal = l_is_maximal0 } = x_19055
    112112  in
    113113  h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0
     
    116116    (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
    117117    Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
    118 let rec property_lattice_rect_Type1 h_mk_property_lattice x_21953 =
    119   let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
    120     l_is_maximal = l_is_maximal0 } = x_21953
     118let rec property_lattice_rect_Type1 h_mk_property_lattice x_19057 =
     119  let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
     120    l_is_maximal = l_is_maximal0 } = x_19057
    121121  in
    122122  h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0
     
    125125    (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
    126126    Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
    127 let rec property_lattice_rect_Type0 h_mk_property_lattice x_21955 =
    128   let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
    129     l_is_maximal = l_is_maximal0 } = x_21955
     127let rec property_lattice_rect_Type0 h_mk_property_lattice x_19059 =
     128  let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
     129    l_is_maximal = l_is_maximal0 } = x_19059
    130130  in
    131131  h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0
     
    195195
    196196type fixpoint =
    197   equations -> valuation
     197  valuation
    198198  (* singleton inductive, whose constructor was mk_fixpoint *)
    199199
    200200(** val fixpoint_rect_Type4 :
    201     property_lattice -> ((equations -> valuation) -> __ -> 'a1) -> fixpoint
    202     -> 'a1 **)
    203 let rec fixpoint_rect_Type4 latt h_mk_fixpoint x_21976 =
    204   let fix_lfp = x_21976 in h_mk_fixpoint fix_lfp __
     201    property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
     202    'a1 **)
     203let rec fixpoint_rect_Type4 latt eqs h_mk_fixpoint x_19080 =
     204  let fix_lfp = x_19080 in h_mk_fixpoint fix_lfp __
    205205
    206206(** val fixpoint_rect_Type5 :
    207     property_lattice -> ((equations -> valuation) -> __ -> 'a1) -> fixpoint
    208     -> 'a1 **)
    209 let rec fixpoint_rect_Type5 latt h_mk_fixpoint x_21978 =
    210   let fix_lfp = x_21978 in h_mk_fixpoint fix_lfp __
     207    property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
     208    'a1 **)
     209let rec fixpoint_rect_Type5 latt eqs h_mk_fixpoint x_19082 =
     210  let fix_lfp = x_19082 in h_mk_fixpoint fix_lfp __
    211211
    212212(** val fixpoint_rect_Type3 :
    213     property_lattice -> ((equations -> valuation) -> __ -> 'a1) -> fixpoint
    214     -> 'a1 **)
    215 let rec fixpoint_rect_Type3 latt h_mk_fixpoint x_21980 =
    216   let fix_lfp = x_21980 in h_mk_fixpoint fix_lfp __
     213    property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
     214    'a1 **)
     215let rec fixpoint_rect_Type3 latt eqs h_mk_fixpoint x_19084 =
     216  let fix_lfp = x_19084 in h_mk_fixpoint fix_lfp __
    217217
    218218(** val fixpoint_rect_Type2 :
    219     property_lattice -> ((equations -> valuation) -> __ -> 'a1) -> fixpoint
    220     -> 'a1 **)
    221 let rec fixpoint_rect_Type2 latt h_mk_fixpoint x_21982 =
    222   let fix_lfp = x_21982 in h_mk_fixpoint fix_lfp __
     219    property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
     220    'a1 **)
     221let rec fixpoint_rect_Type2 latt eqs h_mk_fixpoint x_19086 =
     222  let fix_lfp = x_19086 in h_mk_fixpoint fix_lfp __
    223223
    224224(** val fixpoint_rect_Type1 :
    225     property_lattice -> ((equations -> valuation) -> __ -> 'a1) -> fixpoint
    226     -> 'a1 **)
    227 let rec fixpoint_rect_Type1 latt h_mk_fixpoint x_21984 =
    228   let fix_lfp = x_21984 in h_mk_fixpoint fix_lfp __
     225    property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
     226    'a1 **)
     227let rec fixpoint_rect_Type1 latt eqs h_mk_fixpoint x_19088 =
     228  let fix_lfp = x_19088 in h_mk_fixpoint fix_lfp __
    229229
    230230(** val fixpoint_rect_Type0 :
    231     property_lattice -> ((equations -> valuation) -> __ -> 'a1) -> fixpoint
    232     -> 'a1 **)
    233 let rec fixpoint_rect_Type0 latt h_mk_fixpoint x_21986 =
    234   let fix_lfp = x_21986 in h_mk_fixpoint fix_lfp __
    235 
    236 (** val fix_lfp : property_lattice -> fixpoint -> equations -> valuation **)
    237 let rec fix_lfp latt xxx =
     231    property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
     232    'a1 **)
     233let rec fixpoint_rect_Type0 latt eqs h_mk_fixpoint x_19090 =
     234  let fix_lfp = x_19090 in h_mk_fixpoint fix_lfp __
     235
     236(** val fix_lfp : property_lattice -> equations -> fixpoint -> valuation **)
     237let rec fix_lfp latt eqs xxx =
    238238  let yyy = xxx in yyy
    239239
    240240(** val fixpoint_inv_rect_Type4 :
    241     property_lattice -> fixpoint -> ((equations -> valuation) -> __ -> __ ->
    242     'a1) -> 'a1 **)
    243 let fixpoint_inv_rect_Type4 x1 hterm h1 =
    244   let hcut = fixpoint_rect_Type4 x1 h1 hterm in hcut __
     241    property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ ->
     242    'a1) -> 'a1 **)
     243let fixpoint_inv_rect_Type4 x1 x2 hterm h1 =
     244  let hcut = fixpoint_rect_Type4 x1 x2 h1 hterm in hcut __
    245245
    246246(** val fixpoint_inv_rect_Type3 :
    247     property_lattice -> fixpoint -> ((equations -> valuation) -> __ -> __ ->
    248     'a1) -> 'a1 **)
    249 let fixpoint_inv_rect_Type3 x1 hterm h1 =
    250   let hcut = fixpoint_rect_Type3 x1 h1 hterm in hcut __
     247    property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ ->
     248    'a1) -> 'a1 **)
     249let fixpoint_inv_rect_Type3 x1 x2 hterm h1 =
     250  let hcut = fixpoint_rect_Type3 x1 x2 h1 hterm in hcut __
    251251
    252252(** val fixpoint_inv_rect_Type2 :
    253     property_lattice -> fixpoint -> ((equations -> valuation) -> __ -> __ ->
    254     'a1) -> 'a1 **)
    255 let fixpoint_inv_rect_Type2 x1 hterm h1 =
    256   let hcut = fixpoint_rect_Type2 x1 h1 hterm in hcut __
     253    property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ ->
     254    'a1) -> 'a1 **)
     255let fixpoint_inv_rect_Type2 x1 x2 hterm h1 =
     256  let hcut = fixpoint_rect_Type2 x1 x2 h1 hterm in hcut __
    257257
    258258(** val fixpoint_inv_rect_Type1 :
    259     property_lattice -> fixpoint -> ((equations -> valuation) -> __ -> __ ->
    260     'a1) -> 'a1 **)
    261 let fixpoint_inv_rect_Type1 x1 hterm h1 =
    262   let hcut = fixpoint_rect_Type1 x1 h1 hterm in hcut __
     259    property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ ->
     260    'a1) -> 'a1 **)
     261let fixpoint_inv_rect_Type1 x1 x2 hterm h1 =
     262  let hcut = fixpoint_rect_Type1 x1 x2 h1 hterm in hcut __
    263263
    264264(** val fixpoint_inv_rect_Type0 :
    265     property_lattice -> fixpoint -> ((equations -> valuation) -> __ -> __ ->
    266     'a1) -> 'a1 **)
    267 let fixpoint_inv_rect_Type0 x1 hterm h1 =
    268   let hcut = fixpoint_rect_Type0 x1 h1 hterm in hcut __
    269 
    270 (** val fixpoint_discr : property_lattice -> fixpoint -> fixpoint -> __ **)
    271 let fixpoint_discr a1 x y =
     265    property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ ->
     266    'a1) -> 'a1 **)
     267let fixpoint_inv_rect_Type0 x1 x2 hterm h1 =
     268  let hcut = fixpoint_rect_Type0 x1 x2 h1 hterm in hcut __
     269
     270(** val fixpoint_discr :
     271    property_lattice -> equations -> fixpoint -> fixpoint -> __ **)
     272let fixpoint_discr a1 a2 x y =
    272273  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y
    273274
    274 (** val fixpoint_jmdiscr : property_lattice -> fixpoint -> fixpoint -> __ **)
    275 let fixpoint_jmdiscr a1 x y =
     275(** val fixpoint_jmdiscr :
     276    property_lattice -> equations -> fixpoint -> fixpoint -> __ **)
     277let fixpoint_jmdiscr a1 a2 x y =
    276278  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y
    277279
     280(** val dpi1__o__fix_lfp__o__inject :
     281    property_lattice -> equations -> (fixpoint, 'a1) Types.dPair -> valuation
     282    Types.sig0 **)
     283let dpi1__o__fix_lfp__o__inject x0 x2 x4 =
     284  fix_lfp x0 x2 x4.Types.dpi1
     285
     286(** val eject__o__fix_lfp__o__inject :
     287    property_lattice -> equations -> fixpoint Types.sig0 -> valuation
     288    Types.sig0 **)
     289let eject__o__fix_lfp__o__inject x0 x2 x4 =
     290  fix_lfp x0 x2 (Types.pi1 x4)
     291
     292(** val fix_lfp__o__inject :
     293    property_lattice -> equations -> fixpoint -> valuation Types.sig0 **)
     294let fix_lfp__o__inject x0 x2 x3 =
     295  fix_lfp x0 x2 x3
     296
    278297(** val dpi1__o__fix_lfp :
    279     property_lattice -> (fixpoint, 'a1) Types.dPair -> equations -> valuation **)
    280 let dpi1__o__fix_lfp x0 x2 =
    281   fix_lfp x0 x2.Types.dpi1
     298    property_lattice -> equations -> (fixpoint, 'a1) Types.dPair -> valuation **)
     299let dpi1__o__fix_lfp x0 x1 x3 =
     300  fix_lfp x0 x1 x3.Types.dpi1
    282301
    283302(** val eject__o__fix_lfp :
    284     property_lattice -> fixpoint Types.sig0 -> equations -> valuation **)
    285 let eject__o__fix_lfp x0 x2 =
    286   fix_lfp x0 (Types.pi1 x2)
    287 
    288 type fixpoint_computer = property_lattice -> fixpoint
    289 
     303    property_lattice -> equations -> fixpoint Types.sig0 -> valuation **)
     304let eject__o__fix_lfp x0 x1 x3 =
     305  fix_lfp x0 x1 (Types.pi1 x3)
     306
     307type fixpoint_computer = property_lattice -> equations -> fixpoint
     308
     309(** val dpi1__o__apply_fixpoint :
     310    property_lattice -> equations -> (fixpoint, 'a1) Types.dPair ->
     311    Graphs.label -> __ **)
     312let dpi1__o__apply_fixpoint x0 x1 x3 =
     313  let latt = x0 in
     314  let eqs = x1 in let f = x3.Types.dpi1 in (fun l -> fix_lfp latt eqs f l)
     315
     316(** val eject__o__apply_fixpoint :
     317    property_lattice -> equations -> fixpoint Types.sig0 -> Graphs.label ->
     318    __ **)
     319let eject__o__apply_fixpoint x0 x1 x3 =
     320  let latt = x0 in
     321  let eqs = x1 in let f = Types.pi1 x3 in (fun l -> fix_lfp latt eqs f l)
     322
Note: See TracChangeset for help on using the changeset viewer.