Changeset 2773 for extracted/positiveMap.ml
 Timestamp:
 Mar 4, 2013, 10:03:33 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/positiveMap.ml
r2743 r2773 44 44 let rec positive_map_rect_Type4 h_pm_leaf h_pm_node = function 45 45  Pm_leaf > h_pm_leaf 46  Pm_node (x_3 144, x_3143, x_3142) >47 h_pm_node x_3 144 x_3143 x_314248 (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3 143)49 (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3 142)46  Pm_node (x_3404, x_3403, x_3402) > 47 h_pm_node x_3404 x_3403 x_3402 48 (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3403) 49 (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3402) 50 50 51 51 (** val positive_map_rect_Type3 : … … 54 54 let rec positive_map_rect_Type3 h_pm_leaf h_pm_node = function 55 55  Pm_leaf > h_pm_leaf 56  Pm_node (x_3 156, x_3155, x_3154) >57 h_pm_node x_3 156 x_3155 x_315458 (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3 155)59 (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3 154)56  Pm_node (x_3416, x_3415, x_3414) > 57 h_pm_node x_3416 x_3415 x_3414 58 (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3415) 59 (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3414) 60 60 61 61 (** val positive_map_rect_Type2 : … … 64 64 let rec positive_map_rect_Type2 h_pm_leaf h_pm_node = function 65 65  Pm_leaf > h_pm_leaf 66  Pm_node (x_3 162, x_3161, x_3160) >67 h_pm_node x_3 162 x_3161 x_316068 (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3 161)69 (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3 160)66  Pm_node (x_3422, x_3421, x_3420) > 67 h_pm_node x_3422 x_3421 x_3420 68 (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3421) 69 (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3420) 70 70 71 71 (** val positive_map_rect_Type1 : … … 74 74 let rec positive_map_rect_Type1 h_pm_leaf h_pm_node = function 75 75  Pm_leaf > h_pm_leaf 76  Pm_node (x_3 168, x_3167, x_3166) >77 h_pm_node x_3 168 x_3167 x_316678 (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3 167)79 (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3 166)76  Pm_node (x_3428, x_3427, x_3426) > 77 h_pm_node x_3428 x_3427 x_3426 78 (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3427) 79 (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3426) 80 80 81 81 (** val positive_map_rect_Type0 : … … 84 84 let rec positive_map_rect_Type0 h_pm_leaf h_pm_node = function 85 85  Pm_leaf > h_pm_leaf 86  Pm_node (x_3 174, x_3173, x_3172) >87 h_pm_node x_3 174 x_3173 x_317288 (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3 173)89 (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3 172)86  Pm_node (x_3434, x_3433, x_3432) > 87 h_pm_node x_3434 x_3433 x_3432 88 (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3433) 89 (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3432) 90 90 91 91 (** val positive_map_inv_rect_Type4 : … … 183 183  Pm_leaf > Types.None 184 184  Pm_node (x, l, r) > 185 Types.option_map (fun r 5 > Pm_node (x, l, r5)) (update tl a r))185 Types.option_map (fun r0 > Pm_node (x, l, r0)) (update tl a r)) 186 186  Positive.P0 tl > 187 187 (match t with … … 190 190 Types.option_map (fun l0 > Pm_node (x, l0, r)) (update tl a l)) 191 191 192 (** val fold 0:192 (** val fold : 193 193 (Positive.pos > 'a1 > 'a2 > 'a2) > 'a1 positive_map > 'a2 > 'a2 **) 194 let rec fold 0f t b =194 let rec fold f t b = 195 195 match t with 196 196  Pm_leaf > b … … 201 201  Types.Some a0 > f Positive.One a0 b 202 202 in 203 let b1 = fold 0(fun x > f (Positive.P0 x)) l b0 in204 fold 0(fun x > f (Positive.P1 x)) r b1203 let b1 = fold (fun x > f (Positive.P0 x)) l b0 in 204 fold (fun x > f (Positive.P1 x)) r b1 205 205 206 206 (** val domain_of_pm : 'a1 positive_map > Types.unit0 positive_map **) 207 207 let domain_of_pm t = 208 fold 0(fun p a b > insert p Types.It b) t Pm_leaf208 fold (fun p a b > insert p Types.It b) t Pm_leaf 209 209 210 210 (** val is_none : 'a1 Types.option > Bool.bool **) … … 224 224  Pm_node (a, l, r) > 225 225 let a' = 226 Monad.m_bind0 (Monad.max_def Option.option 0) (Obj.magic a) (fun x >226 Monad.m_bind0 (Monad.max_def Option.option) (Obj.magic a) (fun x > 227 227 Obj.magic f x) 228 228 in … … 234 234  Bool.False > Pm_node ((Obj.magic a'), l', r')) 235 235 236 (** val map 0: ('a1 > 'a2) > 'a1 positive_map > 'a2 positive_map **)237 let map 0f =236 (** val map : ('a1 > 'a2) > 'a1 positive_map > 'a2 positive_map **) 237 let map f = 238 238 map_opt (fun x > Types.Some (f x)) 239 239
Note: See TracChangeset
for help on using the changeset viewer.