Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/positiveMap.ml

    r2743 r2773  
    4444let rec positive_map_rect_Type4 h_pm_leaf h_pm_node = function
    4545| Pm_leaf -> h_pm_leaf
    46 | Pm_node (x_3144, x_3143, x_3142) ->
    47   h_pm_node x_3144 x_3143 x_3142
    48     (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3143)
    49     (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3142)
     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)
    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_3156, x_3155, x_3154) ->
    57   h_pm_node x_3156 x_3155 x_3154
    58     (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3155)
    59     (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3154)
     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)
    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_3162, x_3161, x_3160) ->
    67   h_pm_node x_3162 x_3161 x_3160
    68     (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3161)
    69     (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3160)
     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)
    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_3168, x_3167, x_3166) ->
    77   h_pm_node x_3168 x_3167 x_3166
    78     (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3167)
    79     (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3166)
     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)
    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_3174, x_3173, x_3172) ->
    87   h_pm_node x_3174 x_3173 x_3172
    88     (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3173)
    89     (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3172)
     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)
    9090
    9191(** val positive_map_inv_rect_Type4 :
     
    183183     | Pm_leaf -> Types.None
    184184     | Pm_node (x, l, r) ->
    185        Types.option_map (fun r5 -> Pm_node (x, l, r5)) (update tl a r))
     185       Types.option_map (fun r0 -> Pm_node (x, l, r0)) (update tl a r))
    186186  | Positive.P0 tl ->
    187187    (match t with
     
    190190       Types.option_map (fun l0 -> Pm_node (x, l0, r)) (update tl a l))
    191191
    192 (** val fold0 :
     192(** val fold :
    193193    (Positive.pos -> 'a1 -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 -> 'a2 **)
    194 let rec fold0 f t b =
     194let rec fold f t b =
    195195  match t with
    196196  | Pm_leaf -> b
     
    201201      | Types.Some a0 -> f Positive.One a0 b
    202202    in
    203     let b1 = fold0 (fun x -> f (Positive.P0 x)) l b0 in
    204     fold0 (fun x -> f (Positive.P1 x)) r b1
     203    let b1 = fold (fun x -> f (Positive.P0 x)) l b0 in
     204    fold (fun x -> f (Positive.P1 x)) r b1
    205205
    206206(** val domain_of_pm : 'a1 positive_map -> Types.unit0 positive_map **)
    207207let domain_of_pm t =
    208   fold0 (fun p a b -> insert p Types.It b) t Pm_leaf
     208  fold (fun p a b -> insert p Types.It b) t Pm_leaf
    209209
    210210(** val is_none : 'a1 Types.option -> Bool.bool **)
     
    224224| Pm_node (a, l, r) ->
    225225  let a' =
    226     Monad.m_bind0 (Monad.max_def Option.option0) (Obj.magic a) (fun x ->
     226    Monad.m_bind0 (Monad.max_def Option.option) (Obj.magic a) (fun x ->
    227227      Obj.magic f x)
    228228  in
     
    234234   | Bool.False -> Pm_node ((Obj.magic a'), l', r'))
    235235
    236 (** val map0 : ('a1 -> 'a2) -> 'a1 positive_map -> 'a2 positive_map **)
    237 let map0 f =
     236(** val map : ('a1 -> 'a2) -> 'a1 positive_map -> 'a2 positive_map **)
     237let map f =
    238238  map_opt (fun x -> Types.Some (f x))
    239239
Note: See TracChangeset for help on using the changeset viewer.