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

    r2827 r3043  
    4444let rec positive_map_rect_Type4 h_pm_leaf h_pm_node = function
    4545| Pm_leaf -> h_pm_leaf
    46 | Pm_node (x_3287, x_3286, x_3285) ->
    47   h_pm_node x_3287 x_3286 x_3285
    48     (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3286)
    49     (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3285)
     46| Pm_node (x_3300, x_3299, x_3298) ->
     47  h_pm_node x_3300 x_3299 x_3298
     48    (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3299)
     49    (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3298)
    5050
    5151(** val positive_map_rect_Type3 :
     
    5454let rec positive_map_rect_Type3 h_pm_leaf h_pm_node = function
    5555| Pm_leaf -> h_pm_leaf
    56 | Pm_node (x_3299, x_3298, x_3297) ->
    57   h_pm_node x_3299 x_3298 x_3297
    58     (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3298)
    59     (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3297)
     56| Pm_node (x_3312, x_3311, x_3310) ->
     57  h_pm_node x_3312 x_3311 x_3310
     58    (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3311)
     59    (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3310)
    6060
    6161(** val positive_map_rect_Type2 :
     
    6464let rec positive_map_rect_Type2 h_pm_leaf h_pm_node = function
    6565| Pm_leaf -> h_pm_leaf
    66 | Pm_node (x_3305, x_3304, x_3303) ->
    67   h_pm_node x_3305 x_3304 x_3303
    68     (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3304)
    69     (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3303)
     66| Pm_node (x_3318, x_3317, x_3316) ->
     67  h_pm_node x_3318 x_3317 x_3316
     68    (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3317)
     69    (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3316)
    7070
    7171(** val positive_map_rect_Type1 :
     
    7474let rec positive_map_rect_Type1 h_pm_leaf h_pm_node = function
    7575| Pm_leaf -> h_pm_leaf
    76 | Pm_node (x_3311, x_3310, x_3309) ->
    77   h_pm_node x_3311 x_3310 x_3309
    78     (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3310)
    79     (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3309)
     76| Pm_node (x_3324, x_3323, x_3322) ->
     77  h_pm_node x_3324 x_3323 x_3322
     78    (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3323)
     79    (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3322)
    8080
    8181(** val positive_map_rect_Type0 :
     
    8484let rec positive_map_rect_Type0 h_pm_leaf h_pm_node = function
    8585| Pm_leaf -> h_pm_leaf
    86 | Pm_node (x_3317, x_3316, x_3315) ->
    87   h_pm_node x_3317 x_3316 x_3315
    88     (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3316)
    89     (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3315)
     86| Pm_node (x_3330, x_3329, x_3328) ->
     87  h_pm_node x_3330 x_3329 x_3328
     88    (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3329)
     89    (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3328)
    9090
    9191(** val positive_map_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.