Ignore:
Timestamp:
Feb 23, 2013, 1:16:55 AM (7 years ago)
Author:
sacerdot
Message:

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/positiveMap.ml

    r2649 r2717  
    2828
    2929open Util
     30
     31open Setoids
     32
     33open Monad
     34
     35open Option
    3036
    3137type 'a positive_map =
     
    3844let rec positive_map_rect_Type4 h_pm_leaf h_pm_node = function
    3945| Pm_leaf -> h_pm_leaf
    40 | Pm_node (x_3092, x_3091, x_3090) ->
    41   h_pm_node x_3092 x_3091 x_3090
    42     (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3091)
    43     (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3090)
     46| Pm_node (x_3118, x_3117, x_3116) ->
     47  h_pm_node x_3118 x_3117 x_3116
     48    (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3117)
     49    (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3116)
    4450
    4551(** val positive_map_rect_Type3 :
     
    4854let rec positive_map_rect_Type3 h_pm_leaf h_pm_node = function
    4955| Pm_leaf -> h_pm_leaf
    50 | Pm_node (x_3104, x_3103, x_3102) ->
    51   h_pm_node x_3104 x_3103 x_3102
    52     (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3103)
    53     (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3102)
     56| Pm_node (x_3130, x_3129, x_3128) ->
     57  h_pm_node x_3130 x_3129 x_3128
     58    (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3129)
     59    (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3128)
    5460
    5561(** val positive_map_rect_Type2 :
     
    5864let rec positive_map_rect_Type2 h_pm_leaf h_pm_node = function
    5965| Pm_leaf -> h_pm_leaf
    60 | Pm_node (x_3110, x_3109, x_3108) ->
    61   h_pm_node x_3110 x_3109 x_3108
    62     (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3109)
    63     (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3108)
     66| Pm_node (x_3136, x_3135, x_3134) ->
     67  h_pm_node x_3136 x_3135 x_3134
     68    (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3135)
     69    (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3134)
    6470
    6571(** val positive_map_rect_Type1 :
     
    6874let rec positive_map_rect_Type1 h_pm_leaf h_pm_node = function
    6975| Pm_leaf -> h_pm_leaf
    70 | Pm_node (x_3116, x_3115, x_3114) ->
    71   h_pm_node x_3116 x_3115 x_3114
    72     (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3115)
    73     (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3114)
     76| Pm_node (x_3142, x_3141, x_3140) ->
     77  h_pm_node x_3142 x_3141 x_3140
     78    (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3141)
     79    (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3140)
    7480
    7581(** val positive_map_rect_Type0 :
     
    7884let rec positive_map_rect_Type0 h_pm_leaf h_pm_node = function
    7985| Pm_leaf -> h_pm_leaf
    80 | Pm_node (x_3122, x_3121, x_3120) ->
    81   h_pm_node x_3122 x_3121 x_3120
    82     (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3121)
    83     (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3120)
     86| Pm_node (x_3148, x_3147, x_3146) ->
     87  h_pm_node x_3148 x_3147 x_3146
     88    (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3147)
     89    (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3146)
    8490
    8591(** val positive_map_inv_rect_Type4 :
     
    201207let domain_of_pm t =
    202208  fold0 (fun p a b -> insert p Types.It b) t Pm_leaf
    203 
    204 open Setoids
    205 
    206 open Monad
    207 
    208 open Option
    209209
    210210(** val is_none : 'a1 Types.option -> Bool.bool **)
Note: See TracChangeset for help on using the changeset viewer.