extracted/positiveMap.ml

   1 open Preamble
   2
   3 open Hints_declaration
   4
   5 open Core_notation
   6
   7 open Pts
   8
   9 open Logic
  10
  11 open Types
  12
  13 open Bool
  14
  15 open Relations
  16
  17 open Nat
  18
  19 open Positive
  20
  21 open Div_and_mod
  22
  23 open Jmeq
  24
  25 open Russell
  26
  27 open List
  28
  29 open Util
  30
  31 open Setoids
  32
  33 open Monad
  34
  35 open Option
  36
  37 type 'a positive_map =
  38 | Pm_leaf
  39 | Pm_node of 'a Types.option * 'a positive_map * 'a positive_map
  40
  41 (** val positive_map_rect_Type4 :
  42     'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2
  43     -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **)
  44 let rec positive_map_rect_Type4 h_pm_leaf h_pm_node = function
  45 | Pm_leaf -> h_pm_leaf
  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)
  50
  51 (** val positive_map_rect_Type3 :
  52     'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2
  53     -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **)
  54 let rec positive_map_rect_Type3 h_pm_leaf h_pm_node = function
  55 | Pm_leaf -> h_pm_leaf
  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)
  60
  61 (** val positive_map_rect_Type2 :
  62     'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2
  63     -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **)
  64 let rec positive_map_rect_Type2 h_pm_leaf h_pm_node = function
  65 | Pm_leaf -> h_pm_leaf
  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)
  70
  71 (** val positive_map_rect_Type1 :
  72     'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2
  73     -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **)
  74 let rec positive_map_rect_Type1 h_pm_leaf h_pm_node = function
  75 | Pm_leaf -> h_pm_leaf
  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)
  80
  81 (** val positive_map_rect_Type0 :
  82     'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2
  83     -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **)
  84 let rec positive_map_rect_Type0 h_pm_leaf h_pm_node = function
  85 | Pm_leaf -> h_pm_leaf
  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)
  90
  91 (** val positive_map_inv_rect_Type4 :
  92     'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map
  93     -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
  94 let positive_map_inv_rect_Type4 hterm h1 h2 =
  95   let hcut = positive_map_rect_Type4 h1 h2 hterm in hcut __
  96
  97 (** val positive_map_inv_rect_Type3 :
  98     'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map
  99     -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
 100 let positive_map_inv_rect_Type3 hterm h1 h2 =
 101   let hcut = positive_map_rect_Type3 h1 h2 hterm in hcut __
 102
 103 (** val positive_map_inv_rect_Type2 :
 104     'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map
 105     -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
 106 let positive_map_inv_rect_Type2 hterm h1 h2 =
 107   let hcut = positive_map_rect_Type2 h1 h2 hterm in hcut __
 108
 109 (** val positive_map_inv_rect_Type1 :
 110     'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map
 111     -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
 112 let positive_map_inv_rect_Type1 hterm h1 h2 =
 113   let hcut = positive_map_rect_Type1 h1 h2 hterm in hcut __
 114
 115 (** val positive_map_inv_rect_Type0 :
 116     'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map
 117     -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
 118 let positive_map_inv_rect_Type0 hterm h1 h2 =
 119   let hcut = positive_map_rect_Type0 h1 h2 hterm in hcut __
 120
 121 (** val positive_map_discr : 'a1 positive_map -> 'a1 positive_map -> __ **)
 122 let positive_map_discr x y =
 123   Logic.eq_rect_Type2 x
 124     (match x with
 125      | Pm_leaf -> Obj.magic (fun _ dH -> dH)
 126      | Pm_node (a0, a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
 127
 128 (** val positive_map_jmdiscr : 'a1 positive_map -> 'a1 positive_map -> __ **)
 129 let positive_map_jmdiscr x y =
 130   Logic.eq_rect_Type2 x
 131     (match x with
 132      | Pm_leaf -> Obj.magic (fun _ dH -> dH)
 133      | Pm_node (a0, a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
 134
 135 (** val lookup_opt : Positive.pos -> 'a1 positive_map -> 'a1 Types.option **)
 136 let rec lookup_opt b = function
 137 | Pm_leaf -> Types.None
 138 | Pm_node (a, l, r) ->
 139   (match b with
 140    | Positive.One -> a
 141    | Positive.P1 tl -> lookup_opt tl r
 142    | Positive.P0 tl -> lookup_opt tl l)
 143
 144 (** val lookup : Positive.pos -> 'a1 positive_map -> 'a1 -> 'a1 **)
 145 let lookup b t x =
 146   match lookup_opt b t with
 147   | Types.None -> x
 148   | Types.Some r -> r
 149
 150 (** val pm_set :
 151     Positive.pos -> 'a1 Types.option -> 'a1 positive_map -> 'a1 positive_map **)
 152 let rec pm_set b a t =
 153   match b with
 154   | Positive.One ->
 155     (match t with
 156      | Pm_leaf -> Pm_node (a, Pm_leaf, Pm_leaf)
 157      | Pm_node (x, l, r) -> Pm_node (a, l, r))
 158   | Positive.P1 tl ->
 159     (match t with
 160      | Pm_leaf -> Pm_node (Types.None, Pm_leaf, (pm_set tl a Pm_leaf))
 161      | Pm_node (x, l, r) -> Pm_node (x, l, (pm_set tl a r)))
 162   | Positive.P0 tl ->
 163     (match t with
 164      | Pm_leaf -> Pm_node (Types.None, (pm_set tl a Pm_leaf), Pm_leaf)
 165      | Pm_node (x, l, r) -> Pm_node (x, (pm_set tl a l), r))
 166
 167 (** val insert :
 168     Positive.pos -> 'a1 -> 'a1 positive_map -> 'a1 positive_map **)
 169 let insert p a =
 170   pm_set p (Types.Some a)
 171
 172 (** val update :
 173     Positive.pos -> 'a1 -> 'a1 positive_map -> 'a1 positive_map Types.option **)
 174 let rec update b a t =
 175   match b with
 176   | Positive.One ->
 177     (match t with
 178      | Pm_leaf -> Types.None
 179      | Pm_node (x, l, r) ->
 180        Types.option_map (fun x0 -> Pm_node ((Types.Some a), l, r)) x)
 181   | Positive.P1 tl ->
 182     (match t with
 183      | Pm_leaf -> Types.None
 184      | Pm_node (x, l, r) ->
 185        Types.option_map (fun r0 -> Pm_node (x, l, r0)) (update tl a r))
 186   | Positive.P0 tl ->
 187     (match t with
 188      | Pm_leaf -> Types.None
 189      | Pm_node (x, l, r) ->
 190        Types.option_map (fun l0 -> Pm_node (x, l0, r)) (update tl a l))
 191
 192 (** val fold :
 193     (Positive.pos -> 'a1 -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 -> 'a2 **)
 194 let rec fold f t b =
 195   match t with
 196   | Pm_leaf -> b
 197   | Pm_node (a, l, r) ->
 198     let b0 =
 199       match a with
 200       | Types.None -> b
 201       | Types.Some a0 -> f Positive.One a0 b
 202     in
 203     let b1 = fold (fun x -> f (Positive.P0 x)) l b0 in
 204     fold (fun x -> f (Positive.P1 x)) r b1
 205
 206 (** val domain_of_pm : 'a1 positive_map -> Types.unit0 positive_map **)
 207 let domain_of_pm t =
 208   fold (fun p a b -> insert p Types.It b) t Pm_leaf
 209
 210 (** val is_none : 'a1 Types.option -> Bool.bool **)
 211 let is_none = function
 212 | Types.None -> Bool.True
 213 | Types.Some x -> Bool.False
 214
 215 (** val is_pm_leaf : 'a1 positive_map -> Bool.bool **)
 216 let is_pm_leaf = function
 217 | Pm_leaf -> Bool.True
 218 | Pm_node (x, x0, x1) -> Bool.False
 219
 220 (** val map_opt :
 221     ('a1 -> 'a2 Types.option) -> 'a1 positive_map -> 'a2 positive_map **)
 222 let rec map_opt f = function
 223 | Pm_leaf -> Pm_leaf
 224 | Pm_node (a, l, r) ->
 225   let a' =
 226     Monad.m_bind0 (Monad.max_def Option.option) (Obj.magic a) (fun x ->
 227       Obj.magic f x)
 228   in
 229   let l' = map_opt f l in
 230   let r' = map_opt f r in
 231   (match Bool.andb (Bool.andb (is_none (Obj.magic a')) (is_pm_leaf l'))
 232            (is_pm_leaf r') with
 233    | Bool.True -> Pm_leaf
 234    | Bool.False -> Pm_node ((Obj.magic a'), l', r'))
 235
 236 (** val map : ('a1 -> 'a2) -> 'a1 positive_map -> 'a2 positive_map **)
 237 let map f =
 238   map_opt (fun x -> Types.Some (f x))
 239
 240 (** val merge :
 241     ('a1 Types.option -> 'a2 Types.option -> 'a3 Types.option) -> 'a1
 242     positive_map -> 'a2 positive_map -> 'a3 positive_map **)
 243 let rec merge choice a b =
 244   match a with
 245   | Pm_leaf -> map_opt (fun x -> choice Types.None (Types.Some x)) b
 246   | Pm_node (o, l, r) ->
 247     (match b with
 248      | Pm_leaf -> map_opt (fun x -> choice (Types.Some x) Types.None) a
 249      | Pm_node (o', l', r') ->
 250        let o'' = choice o o' in
 251        let l'' = merge choice l l' in
 252        let r'' = merge choice r r' in
 253        (match Bool.andb (Bool.andb (is_none o'') (is_pm_leaf l''))
 254                 (is_pm_leaf r'') with
 255         | Bool.True -> Pm_leaf
 256         | Bool.False -> Pm_node (o'', l'', r'')))
 257
 258 (** val domain_size : 'a1 positive_map -> Nat.nat **)
 259 let rec domain_size = function
 260 | Pm_leaf -> Nat.O
 261 | Pm_node (a, l, r) ->
 262   Nat.plus
 263     (Nat.plus
 264       (match a with
 265        | Types.None -> Nat.O
 266        | Types.Some x -> Nat.S Nat.O) (domain_size l)) (domain_size r)
 267
 268 (** val pm_all_aux :
 269     'a1 positive_map -> 'a1 positive_map -> (Positive.pos -> Positive.pos) ->
 270     (Positive.pos -> 'a1 -> __ -> Bool.bool) -> Bool.bool **)
 271 let rec pm_all_aux m t pre x =
 272   (match t with
 273    | Pm_leaf -> (fun _ x0 -> Bool.True)
 274    | Pm_node (a, l, r) ->
 275      (fun _ f ->
 276        Bool.andb
 277          (Bool.andb (pm_all_aux m l (fun x0 -> pre (Positive.P0 x0)) f)
 278            ((match a with
 279              | Types.None -> (fun _ -> Bool.True)
 280              | Types.Some a' -> (fun _ -> f (pre Positive.One) a' __)) __))
 281          (pm_all_aux m r (fun x0 -> pre (Positive.P1 x0)) f))) __ x
 282
 283 (** val pm_all :
 284     'a1 positive_map -> (Positive.pos -> 'a1 -> __ -> Bool.bool) -> Bool.bool **)
 285 let pm_all m f =
 286   pm_all_aux m m (fun x -> x) f
 287
 288 (** val pm_choose :
 289     'a1 positive_map -> ((Positive.pos, 'a1) Types.prod, 'a1 positive_map)
 290     Types.prod Types.option **)
 291 let rec pm_choose = function
 292 | Pm_leaf -> Types.None
 293 | Pm_node (a, l, r) ->
 294   (match pm_choose l with
 295    | Types.None ->
 296      (match pm_choose r with
 297       | Types.None ->
 298         (match a with
 299          | Types.None -> Types.None
 300          | Types.Some a0 ->
 301            Types.Some { Types.fst = { Types.fst = Positive.One; Types.snd =
 302              a0 }; Types.snd = Pm_leaf })
 303       | Types.Some x ->
 304         Types.Some { Types.fst = { Types.fst = (Positive.P1
 305           x.Types.fst.Types.fst); Types.snd = x.Types.fst.Types.snd };
 306           Types.snd = (Pm_node (a, l, x.Types.snd)) })
 307    | Types.Some x ->
 308      Types.Some { Types.fst = { Types.fst = (Positive.P0
 309        x.Types.fst.Types.fst); Types.snd = x.Types.fst.Types.snd };
 310        Types.snd = (Pm_node (a, x.Types.snd, r)) })
 311
 312 (** val pm_try_remove :
 313     Positive.pos -> 'a1 positive_map -> ('a1, 'a1 positive_map) Types.prod
 314     Types.option **)
 315 let rec pm_try_remove b t =
 316   match b with
 317   | Positive.One ->
 318     (match t with
 319      | Pm_leaf -> Types.None
 320      | Pm_node (x, l, r) ->
 321        Types.option_map (fun x0 -> { Types.fst = x0; Types.snd = (Pm_node
 322          (Types.None, l, r)) }) x)
 323   | Positive.P1 tl ->
 324     (match t with
 325      | Pm_leaf -> Types.None
 326      | Pm_node (x, l, r) ->
 327        Types.option_map (fun xr -> { Types.fst = xr.Types.fst; Types.snd =
 328          (Pm_node (x, l, xr.Types.snd)) }) (pm_try_remove tl r))
 329   | Positive.P0 tl ->
 330     (match t with
 331      | Pm_leaf -> Types.None
 332      | Pm_node (x, l, r) ->
 333        Types.option_map (fun xl -> { Types.fst = xl.Types.fst; Types.snd =
 334          (Pm_node (x, xl.Types.snd, r)) }) (pm_try_remove tl l))
 335
 336 (** val pm_fold_inf_aux :
 337     'a1 positive_map -> (Positive.pos -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a1
 338     positive_map -> (Positive.pos -> Positive.pos) -> 'a2 -> 'a2 **)
 339 let rec pm_fold_inf_aux t f t' pre b =
 340   (match t' with
 341    | Pm_leaf -> (fun _ -> b)
 342    | Pm_node (a, l, r) ->
 343      (fun _ ->
 344        let b0 =
 345          (match a with
 346           | Types.None -> (fun _ -> b)
 347           | Types.Some a0 -> (fun _ -> f (pre Positive.One) a0 __ b)) __
 348        in
 349        let b1 = pm_fold_inf_aux t f l (fun x -> pre (Positive.P0 x)) b0 in
 350        pm_fold_inf_aux t f r (fun x -> pre (Positive.P1 x)) b1)) __
 351
 352 (** val pm_fold_inf :
 353     'a1 positive_map -> (Positive.pos -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a2 ->
 354     'a2 **)
 355 let pm_fold_inf t f b =
 356   pm_fold_inf_aux t f t (fun x -> x) b
 357
 358 (** val pm_find_aux :
 359     (Positive.pos -> Positive.pos) -> 'a1 positive_map -> (Positive.pos ->
 360     'a1 -> Bool.bool) -> (Positive.pos, 'a1) Types.prod Types.option **)
 361 let rec pm_find_aux pre t p =
 362   match t with
 363   | Pm_leaf -> Types.None
 364   | Pm_node (a, l, r) ->
 365     let x =
 366       match a with
 367       | Types.None -> Types.None
 368       | Types.Some a0 ->
 369         (match p (pre Positive.One) a0 with
 370          | Bool.True ->
 371            Types.Some { Types.fst = (pre Positive.One); Types.snd = a0 }
 372          | Bool.False -> Types.None)
 373     in
 374     (match x with
 375      | Types.None ->
 376        (match pm_find_aux (fun x0 -> pre (Positive.P0 x0)) l p with
 377         | Types.None -> pm_find_aux (fun x0 -> pre (Positive.P1 x0)) r p
 378         | Types.Some y -> Types.Some y)
 379      | Types.Some x0 -> Types.Some x0)
 380
 381 (** val pm_find :
 382     'a1 positive_map -> (Positive.pos -> 'a1 -> Bool.bool) -> (Positive.pos,
 383     'a1) Types.prod Types.option **)
 384 let pm_find x x0 =
 385   pm_find_aux (fun x1 -> x1) x x0
 386