Changeset 3043 for extracted/bind_new.ml


Ignore:
Timestamp:
Mar 29, 2013, 6:38:26 PM (7 years ago)
Author:
sacerdot
Message:

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/bind_new.ml

    r2951 r3043  
    3535    ('a1, 'a2) bind_new -> 'a3 **)
    3636let rec bind_new_rect_Type4 h_bret h_bnew = function
    37 | Bret x_18232 -> h_bret x_18232
    38 | Bnew x_18234 ->
    39   h_bnew x_18234 (fun x_18233 ->
    40     bind_new_rect_Type4 h_bret h_bnew (x_18234 x_18233))
     37| Bret x_18260 -> h_bret x_18260
     38| Bnew x_18262 ->
     39  h_bnew x_18262 (fun x_18261 ->
     40    bind_new_rect_Type4 h_bret h_bnew (x_18262 x_18261))
    4141
    4242(** val bind_new_rect_Type3 :
     
    4444    ('a1, 'a2) bind_new -> 'a3 **)
    4545let rec bind_new_rect_Type3 h_bret h_bnew = function
    46 | Bret x_18244 -> h_bret x_18244
    47 | Bnew x_18246 ->
    48   h_bnew x_18246 (fun x_18245 ->
    49     bind_new_rect_Type3 h_bret h_bnew (x_18246 x_18245))
     46| Bret x_18272 -> h_bret x_18272
     47| Bnew x_18274 ->
     48  h_bnew x_18274 (fun x_18273 ->
     49    bind_new_rect_Type3 h_bret h_bnew (x_18274 x_18273))
    5050
    5151(** val bind_new_rect_Type2 :
     
    5353    ('a1, 'a2) bind_new -> 'a3 **)
    5454let rec bind_new_rect_Type2 h_bret h_bnew = function
    55 | Bret x_18250 -> h_bret x_18250
    56 | Bnew x_18252 ->
    57   h_bnew x_18252 (fun x_18251 ->
    58     bind_new_rect_Type2 h_bret h_bnew (x_18252 x_18251))
     55| Bret x_18278 -> h_bret x_18278
     56| Bnew x_18280 ->
     57  h_bnew x_18280 (fun x_18279 ->
     58    bind_new_rect_Type2 h_bret h_bnew (x_18280 x_18279))
    5959
    6060(** val bind_new_rect_Type1 :
     
    6262    ('a1, 'a2) bind_new -> 'a3 **)
    6363let rec bind_new_rect_Type1 h_bret h_bnew = function
    64 | Bret x_18256 -> h_bret x_18256
    65 | Bnew x_18258 ->
    66   h_bnew x_18258 (fun x_18257 ->
    67     bind_new_rect_Type1 h_bret h_bnew (x_18258 x_18257))
     64| Bret x_18284 -> h_bret x_18284
     65| Bnew x_18286 ->
     66  h_bnew x_18286 (fun x_18285 ->
     67    bind_new_rect_Type1 h_bret h_bnew (x_18286 x_18285))
    6868
    6969(** val bind_new_rect_Type0 :
     
    7171    ('a1, 'a2) bind_new -> 'a3 **)
    7272let rec bind_new_rect_Type0 h_bret h_bnew = function
    73 | Bret x_18262 -> h_bret x_18262
    74 | Bnew x_18264 ->
    75   h_bnew x_18264 (fun x_18263 ->
    76     bind_new_rect_Type0 h_bret h_bnew (x_18264 x_18263))
     73| Bret x_18290 -> h_bret x_18290
     74| Bnew x_18292 ->
     75  h_bnew x_18292 (fun x_18291 ->
     76    bind_new_rect_Type0 h_bret h_bnew (x_18292 x_18291))
    7777
    7878(** val bind_new_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.