extracted/util.ml

   1 open Preamble
   2
   3 open Bool
   4
   5 open Relations
   6
   7 open Nat
   8
   9 open Hints_declaration
  10
  11 open Core_notation
  12
  13 open Pts
  14
  15 open Logic
  16
  17 open Types
  18
  19 open List
  20
  21 open Jmeq
  22
  23 open Russell
  24
  25 type dAEMONXXX =
  26 | K1DAEMONXXX
  27 | K2DAEMONXXX
  28
  29 (** val dAEMONXXX_rect_Type4 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
  30 let rec dAEMONXXX_rect_Type4 h_K1DAEMONXXX h_K2DAEMONXXX = function
  31 | K1DAEMONXXX -> h_K1DAEMONXXX
  32 | K2DAEMONXXX -> h_K2DAEMONXXX
  33
  34 (** val dAEMONXXX_rect_Type5 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
  35 let rec dAEMONXXX_rect_Type5 h_K1DAEMONXXX h_K2DAEMONXXX = function
  36 | K1DAEMONXXX -> h_K1DAEMONXXX
  37 | K2DAEMONXXX -> h_K2DAEMONXXX
  38
  39 (** val dAEMONXXX_rect_Type3 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
  40 let rec dAEMONXXX_rect_Type3 h_K1DAEMONXXX h_K2DAEMONXXX = function
  41 | K1DAEMONXXX -> h_K1DAEMONXXX
  42 | K2DAEMONXXX -> h_K2DAEMONXXX
  43
  44 (** val dAEMONXXX_rect_Type2 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
  45 let rec dAEMONXXX_rect_Type2 h_K1DAEMONXXX h_K2DAEMONXXX = function
  46 | K1DAEMONXXX -> h_K1DAEMONXXX
  47 | K2DAEMONXXX -> h_K2DAEMONXXX
  48
  49 (** val dAEMONXXX_rect_Type1 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
  50 let rec dAEMONXXX_rect_Type1 h_K1DAEMONXXX h_K2DAEMONXXX = function
  51 | K1DAEMONXXX -> h_K1DAEMONXXX
  52 | K2DAEMONXXX -> h_K2DAEMONXXX
  53
  54 (** val dAEMONXXX_rect_Type0 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
  55 let rec dAEMONXXX_rect_Type0 h_K1DAEMONXXX h_K2DAEMONXXX = function
  56 | K1DAEMONXXX -> h_K1DAEMONXXX
  57 | K2DAEMONXXX -> h_K2DAEMONXXX
  58
  59 (** val dAEMONXXX_inv_rect_Type4 :
  60     dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
  61 let dAEMONXXX_inv_rect_Type4 hterm h1 h2 =
  62   let hcut = dAEMONXXX_rect_Type4 h1 h2 hterm in hcut __
  63
  64 (** val dAEMONXXX_inv_rect_Type3 :
  65     dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
  66 let dAEMONXXX_inv_rect_Type3 hterm h1 h2 =
  67   let hcut = dAEMONXXX_rect_Type3 h1 h2 hterm in hcut __
  68
  69 (** val dAEMONXXX_inv_rect_Type2 :
  70     dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
  71 let dAEMONXXX_inv_rect_Type2 hterm h1 h2 =
  72   let hcut = dAEMONXXX_rect_Type2 h1 h2 hterm in hcut __
  73
  74 (** val dAEMONXXX_inv_rect_Type1 :
  75     dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
  76 let dAEMONXXX_inv_rect_Type1 hterm h1 h2 =
  77   let hcut = dAEMONXXX_rect_Type1 h1 h2 hterm in hcut __
  78
  79 (** val dAEMONXXX_inv_rect_Type0 :
  80     dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
  81 let dAEMONXXX_inv_rect_Type0 hterm h1 h2 =
  82   let hcut = dAEMONXXX_rect_Type0 h1 h2 hterm in hcut __
  83
  84 (** val dAEMONXXX_discr : dAEMONXXX -> dAEMONXXX -> __ **)
  85 let dAEMONXXX_discr x y =
  86   Logic.eq_rect_Type2 x
  87     (match x with
  88      | K1DAEMONXXX -> Obj.magic (fun _ dH -> dH)
  89      | K2DAEMONXXX -> Obj.magic (fun _ dH -> dH)) y
  90
  91 (** val dAEMONXXX_jmdiscr : dAEMONXXX -> dAEMONXXX -> __ **)
  92 let dAEMONXXX_jmdiscr x y =
  93   Logic.eq_rect_Type2 x
  94     (match x with
  95      | K1DAEMONXXX -> Obj.magic (fun _ dH -> dH)
  96      | K2DAEMONXXX -> Obj.magic (fun _ dH -> dH)) y
  97
  98 (** val ltb : Nat.nat -> Nat.nat -> Bool.bool **)
  99 let ltb m n =
 100   Nat.leb (Nat.S m) n
 101
 102 (** val geb : Nat.nat -> Nat.nat -> Bool.bool **)
 103 let geb m n =
 104   Nat.leb n m
 105
 106 (** val gtb : Nat.nat -> Nat.nat -> Bool.bool **)
 107 let gtb m n =
 108   ltb n m
 109
 110 (** val eq_nat : Nat.nat -> Nat.nat -> Bool.bool **)
 111 let rec eq_nat n m =
 112   match n with
 113   | Nat.O ->
 114     (match m with
 115      | Nat.O -> Bool.True
 116      | Nat.S x -> Bool.False)
 117   | Nat.S n' ->
 118     (match m with
 119      | Nat.O -> Bool.False
 120      | Nat.S m' -> eq_nat n' m')
 121
 122 (** val forall : ('a1 -> Bool.bool) -> 'a1 List.list -> Bool.bool **)
 123 let rec forall f = function
 124 | List.Nil -> Bool.True
 125 | List.Cons (hd, tl) -> Bool.andb (f hd) (forall f tl)
 126
 127 (** val prefix : Nat.nat -> 'a1 List.list -> 'a1 List.list **)
 128 let rec prefix k = function
 129 | List.Nil -> List.Nil
 130 | List.Cons (hd, tl) ->
 131   (match k with
 132    | Nat.O -> List.Nil
 133    | Nat.S k' -> List.Cons (hd, (prefix k' tl)))
 134
 135 (** val fold_left2 :
 136     ('a1 -> 'a2 -> 'a3 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a3 List.list ->
 137     'a1 **)
 138 let rec fold_left2 f accu left right =
 139   (match left with
 140    | List.Nil ->
 141      (fun _ ->
 142        (match right with
 143         | List.Nil -> (fun _ -> accu)
 144         | List.Cons (hd, tl) ->
 145           (fun _ ->
 146             Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length tl)) __)) __)
 147    | List.Cons (hd, tl) ->
 148      (fun _ ->
 149        (match right with
 150         | List.Nil ->
 151           (fun _ ->
 152             Obj.magic Nat.nat_discr (Nat.S (List.length tl)) Nat.O __)
 153         | List.Cons (hd', tl') ->
 154           (fun _ -> fold_left2 f (f accu hd hd') tl tl')) __)) __
 155
 156 (** val remove_n_first_internal :
 157     Nat.nat -> 'a1 List.list -> Nat.nat -> 'a1 List.list **)
 158 let rec remove_n_first_internal i l n =
 159   match l with
 160   | List.Nil -> List.Nil
 161   | List.Cons (hd, tl) ->
 162     (match eq_nat i n with
 163      | Bool.True -> l
 164      | Bool.False -> remove_n_first_internal (Nat.S i) tl n)
 165
 166 (** val remove_n_first : Nat.nat -> 'a1 List.list -> 'a1 List.list **)
 167 let remove_n_first n l =
 168   remove_n_first_internal Nat.O l n
 169
 170 (** val foldi_from_until_internal :
 171     Nat.nat -> 'a1 List.list -> 'a1 List.list -> Nat.nat -> (Nat.nat -> 'a1
 172     List.list -> 'a1 -> 'a1 List.list) -> 'a1 List.list **)
 173 let rec foldi_from_until_internal i res rem m f =
 174   match rem with
 175   | List.Nil -> res
 176   | List.Cons (e, tl) ->
 177     (match geb i m with
 178      | Bool.True -> res
 179      | Bool.False -> foldi_from_until_internal (Nat.S i) (f i res e) tl m f)
 180
 181 (** val foldi_from_until :
 182     Nat.nat -> Nat.nat -> (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list)
 183     -> 'a1 List.list -> 'a1 List.list -> 'a1 List.list **)
 184 let foldi_from_until n m f a l =
 185   foldi_from_until_internal Nat.O a (remove_n_first n l) m f
 186
 187 (** val foldi_from :
 188     Nat.nat -> (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1
 189     List.list -> 'a1 List.list -> 'a1 List.list **)
 190 let foldi_from n f a l =
 191   foldi_from_until n (List.length l) f a l
 192
 193 (** val foldi_until :
 194     Nat.nat -> (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1
 195     List.list -> 'a1 List.list -> 'a1 List.list **)
 196 let foldi_until m f a l =
 197   foldi_from_until Nat.O m f a l
 198
 199 (** val foldi :
 200     (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1 List.list ->
 201     'a1 List.list -> 'a1 List.list **)
 202 let foldi f a l =
 203   foldi_from_until Nat.O (List.length l) f a l
 204
 205 (** val hd_safe : 'a1 List.list -> 'a1 **)
 206 let hd_safe l =
 207   (match l with
 208    | List.Nil -> (fun _ -> assert false (* absurd case *))
 209    | List.Cons (hd, tl) -> (fun _ -> hd)) __
 210
 211 (** val tail_safe : 'a1 List.list -> 'a1 List.list **)
 212 let tail_safe l =
 213   (match l with
 214    | List.Nil -> (fun _ -> assert false (* absurd case *))
 215    | List.Cons (hd, tl) -> (fun _ -> tl)) __
 216
 217 (** val safe_split :
 218     'a1 List.list -> Nat.nat -> ('a1 List.list, 'a1 List.list) Types.prod **)
 219 let rec safe_split l index =
 220   (match index with
 221    | Nat.O -> (fun _ -> { Types.fst = List.Nil; Types.snd = l })
 222    | Nat.S index' ->
 223      (fun _ ->
 224        (match l with
 225         | List.Nil -> (fun _ -> assert false (* absurd case *))
 226         | List.Cons (hd, tl) ->
 227           (fun _ ->
 228             let { Types.fst = l1; Types.snd = l2 } = safe_split tl index' in
 229             { Types.fst = (List.Cons (hd, l1)); Types.snd = l2 })) __)) __
 230
 231 (** val nth_safe : Nat.nat -> 'a1 List.list -> 'a1 **)
 232 let rec nth_safe index the_list =
 233   (match index with
 234    | Nat.O ->
 235      (match the_list with
 236       | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
 237       | List.Cons (hd, tl) -> (fun _ -> hd))
 238    | Nat.S index' ->
 239      (match the_list with
 240       | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
 241       | List.Cons (hd, tl) -> (fun _ -> nth_safe index' tl))) __
 242
 243 (** val last_safe : 'a1 List.list -> 'a1 **)
 244 let last_safe the_list =
 245   nth_safe (Nat.minus (List.length the_list) (Nat.S Nat.O)) the_list
 246
 247 (** val reduce :
 248     'a1 List.list -> 'a2 List.list -> (('a1 List.list, 'a1 List.list)
 249     Types.prod, ('a2 List.list, 'a2 List.list) Types.prod) Types.prod **)
 250 let rec reduce left right =
 251   match left with
 252   | List.Nil ->
 253     { Types.fst = { Types.fst = List.Nil; Types.snd = List.Nil }; Types.snd =
 254       { Types.fst = List.Nil; Types.snd = right } }
 255   | List.Cons (hd, tl) ->
 256     (match right with
 257      | List.Nil ->
 258        { Types.fst = { Types.fst = List.Nil; Types.snd = left }; Types.snd =
 259          { Types.fst = List.Nil; Types.snd = List.Nil } }
 260      | List.Cons (hd', tl') ->
 261        let { Types.fst = cleft; Types.snd = cright } = reduce tl tl' in
 262        let { Types.fst = commonl; Types.snd = restl } = cleft in
 263        let { Types.fst = commonr; Types.snd = restr } = cright in
 264        { Types.fst = { Types.fst = (List.Cons (hd, commonl)); Types.snd =
 265        restl }; Types.snd = { Types.fst = (List.Cons (hd', commonr));
 266        Types.snd = restr } })
 267
 268 (** val reduce_strong :
 269     'a1 List.list -> 'a2 List.list -> (('a1 List.list, 'a1 List.list)
 270     Types.prod, ('a2 List.list, 'a2 List.list) Types.prod) Types.prod
 271     Types.sig0 **)
 272 let rec reduce_strong left right =
 273   (match left with
 274    | List.Nil ->
 275      (fun _ -> { Types.fst = { Types.fst = List.Nil; Types.snd = List.Nil };
 276        Types.snd = { Types.fst = List.Nil; Types.snd = right } })
 277    | List.Cons (hd, tl) ->
 278      (fun _ ->
 279        (match right with
 280         | List.Nil ->
 281           (fun _ -> { Types.fst = { Types.fst = List.Nil; Types.snd = left };
 282             Types.snd = { Types.fst = List.Nil; Types.snd = List.Nil } })
 283         | List.Cons (hd', tl') ->
 284           (fun _ ->
 285             (let { Types.fst = cleft; Types.snd = cright } =
 286                Types.pi1 (reduce_strong tl tl')
 287              in
 288             (fun _ ->
 289             (let { Types.fst = commonl; Types.snd = restl } = cleft in
 290             (fun _ ->
 291             (let { Types.fst = commonr; Types.snd = restr } = cright in
 292             (fun _ -> { Types.fst = { Types.fst = (List.Cons (hd, commonl));
 293             Types.snd = restl }; Types.snd = { Types.fst = (List.Cons (hd',
 294             commonr)); Types.snd = restr } })) __)) __)) __)) __)) __
 295
 296 (** val map2_opt :
 297     ('a1 -> 'a2 -> 'a3) -> 'a1 List.list -> 'a2 List.list -> 'a3 List.list
 298     Types.option **)
 299 let rec map2_opt f left right =
 300   match left with
 301   | List.Nil ->
 302     (match right with
 303      | List.Nil -> Types.Some List.Nil
 304      | List.Cons (x, x0) -> Types.None)
 305   | List.Cons (hd, tl) ->
 306     (match right with
 307      | List.Nil -> Types.None
 308      | List.Cons (hd', tl') ->
 309        (match map2_opt f tl tl' with
 310         | Types.None -> Types.None
 311         | Types.Some tail -> Types.Some (List.Cons ((f hd hd'), tail))))
 312
 313 (** val map2 :
 314     ('a1 -> 'a2 -> 'a3) -> 'a1 List.list -> 'a2 List.list -> 'a3 List.list **)
 315 let rec map2 f left right =
 316   (match left with
 317    | List.Nil ->
 318      (match right with
 319       | List.Nil -> (fun _ -> List.Nil)
 320       | List.Cons (x, x0) ->
 321         (fun _ -> Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length x0)) __))
 322    | List.Cons (hd, tl) ->
 323      (match right with
 324       | List.Nil ->
 325         (fun _ -> Obj.magic Nat.nat_discr (Nat.S (List.length tl)) Nat.O __)
 326       | List.Cons (hd', tl') ->
 327         (fun _ -> List.Cons ((f hd hd'), (map2 f tl tl'))))) __
 328
 329 (** val map3 :
 330     ('a1 -> 'a2 -> 'a3 -> 'a4) -> 'a1 List.list -> 'a2 List.list -> 'a3
 331     List.list -> 'a4 List.list **)
 332 let rec map3 f left centre right =
 333   (match left with
 334    | List.Nil ->
 335      (fun _ ->
 336        (match centre with
 337         | List.Nil ->
 338           (fun _ ->
 339             (match right with
 340              | List.Nil -> (fun _ -> List.Nil)
 341              | List.Cons (hd, tl) ->
 342                (fun _ ->
 343                  Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length tl)) __))
 344               __)
 345         | List.Cons (hd, tl) ->
 346           (fun _ ->
 347             Logic.eq_rect_Type0 (List.length centre)
 348               (Logic.eq_rect_Type0 (List.length List.Nil) (fun _ ->
 349                 Obj.magic Nat.nat_discr (Nat.S (List.length tl)) Nat.O __)
 350                 (List.length centre)) (List.length right) __)) __)
 351    | List.Cons (hd, tl) ->
 352      (fun _ ->
 353        (match centre with
 354         | List.Nil ->
 355           (fun _ ->
 356             Logic.eq_rect_Type0 (List.length centre)
 357               (Logic.eq_rect_Type0 (List.length (List.Cons (hd, tl)))
 358                 (fun _ ->
 359                 Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length tl)) __)
 360                 (List.length centre)) (List.length right) __)
 361         | List.Cons (hd', tl') ->
 362           (fun _ ->
 363             (match right with
 364              | List.Nil ->
 365                (fun _ _ ->
 366                  Obj.magic Nat.nat_discr (Nat.S (List.length tl')) Nat.O __)
 367              | List.Cons (hd'', tl'') ->
 368                (fun _ _ -> List.Cons ((f hd hd' hd''), (map3 f tl tl' tl''))))
 369               __ __)) __)) __
 370
 371 (** val eq_rect_Type0_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
 372 let eq_rect_Type0_r a h x =
 373   (fun _ auto -> auto) __ h
 374
 375 (** val safe_nth : Nat.nat -> 'a1 List.list -> 'a1 **)
 376 let rec safe_nth n l =
 377   (match n with
 378    | Nat.O ->
 379      (match l with
 380       | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
 381       | List.Cons (hd, tl) -> (fun _ -> hd))
 382    | Nat.S n' ->
 383      (match l with
 384       | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
 385       | List.Cons (hd, tl) -> (fun _ -> safe_nth n' tl))) __
 386
 387 (** val nub_by_internal :
 388     ('a1 -> 'a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat -> 'a1 List.list **)
 389 let rec nub_by_internal f l = function
 390 | Nat.O ->
 391   (match l with
 392    | List.Nil -> List.Nil
 393    | List.Cons (hd, tl) -> l)
 394 | Nat.S n0 ->
 395   (match l with
 396    | List.Nil -> List.Nil
 397    | List.Cons (hd, tl) ->
 398      List.Cons (hd,
 399        (nub_by_internal f (List.filter (fun y -> Bool.notb (f y hd)) tl) n0)))
 400
 401 (** val nub_by :
 402     ('a1 -> 'a1 -> Bool.bool) -> 'a1 List.list -> 'a1 List.list **)
 403 let nub_by f l =
 404   nub_by_internal f l (List.length l)
 405
 406 (** val member :
 407     ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 List.list -> Bool.bool **)
 408 let rec member eq a = function
 409 | List.Nil -> Bool.False
 410 | List.Cons (hd, tl) -> Bool.orb (eq a hd) (member eq a tl)
 411
 412 (** val take : Nat.nat -> 'a1 List.list -> 'a1 List.list **)
 413 let rec take n l =
 414   match n with
 415   | Nat.O -> List.Nil
 416   | Nat.S n0 ->
 417     (match l with
 418      | List.Nil -> List.Nil
 419      | List.Cons (hd, tl) -> List.Cons (hd, (take n0 tl)))
 420
 421 (** val drop : Nat.nat -> 'a1 List.list -> 'a1 List.list **)
 422 let rec drop n l =
 423   match n with
 424   | Nat.O -> l
 425   | Nat.S n0 ->
 426     (match l with
 427      | List.Nil -> List.Nil
 428      | List.Cons (hd, tl) -> drop n0 tl)
 429
 430 (** val list_split :
 431     Nat.nat -> 'a1 List.list -> ('a1 List.list, 'a1 List.list) Types.prod **)
 432 let list_split n l =
 433   { Types.fst = (take n l); Types.snd = (drop n l) }
 434
 435 (** val mapi_internal :
 436     Nat.nat -> (Nat.nat -> 'a1 -> 'a2) -> 'a1 List.list -> 'a2 List.list **)
 437 let rec mapi_internal n f = function
 438 | List.Nil -> List.Nil
 439 | List.Cons (hd, tl) ->
 440   List.Cons ((f n hd), (mapi_internal (Nat.plus n (Nat.S Nat.O)) f tl))
 441
 442 (** val mapi : (Nat.nat -> 'a1 -> 'a2) -> 'a1 List.list -> 'a2 List.list **)
 443 let mapi f l =
 444   mapi_internal Nat.O f l
 445
 446 (** val zip_pottier :
 447     'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list **)
 448 let rec zip_pottier left right =
 449   match left with
 450   | List.Nil -> List.Nil
 451   | List.Cons (hd, tl) ->
 452     (match right with
 453      | List.Nil -> List.Nil
 454      | List.Cons (hd', tl') ->
 455        List.Cons ({ Types.fst = hd; Types.snd = hd' }, (zip_pottier tl tl')))
 456
 457 (** val zip_safe :
 458     'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list **)
 459 let rec zip_safe left right =
 460   (match left with
 461    | List.Nil ->
 462      (fun _ ->
 463        (match right with
 464         | List.Nil -> (fun _ -> List.Nil)
 465         | List.Cons (hd, tl) ->
 466           (fun _ ->
 467             Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length tl)) __)) __)
 468    | List.Cons (hd, tl) ->
 469      (fun _ ->
 470        (match right with
 471         | List.Nil ->
 472           (fun _ ->
 473             Obj.magic Nat.nat_discr (Nat.S (List.length tl)) Nat.O __)
 474         | List.Cons (hd', tl') ->
 475           (fun _ -> List.Cons ({ Types.fst = hd; Types.snd = hd' },
 476             (zip_safe tl tl')))) __)) __
 477
 478 (** val zip :
 479     'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list
 480     Types.option **)
 481 let rec zip l r =
 482   match l with
 483   | List.Nil -> Types.Some List.Nil
 484   | List.Cons (hd, tl) ->
 485     (match r with
 486      | List.Nil -> Types.None
 487      | List.Cons (hd', tl') ->
 488        (match zip tl tl' with
 489         | Types.None -> Types.None
 490         | Types.Some tail ->
 491           Types.Some (List.Cons ({ Types.fst = hd; Types.snd = hd' }, tail))))
 492
 493 (** val foldl : ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a1 **)
 494 let rec foldl f a = function
 495 | List.Nil -> a
 496 | List.Cons (hd, tl) -> foldl f (f a hd) tl
 497
 498 (** val rev : 'a1 List.list -> 'a1 List.list **)
 499 let rev l =
 500   List.reverse l
 501
 502 (** val fold_left_i_aux :
 503     (Nat.nat -> 'a1 -> 'a2 -> 'a1) -> 'a1 -> Nat.nat -> 'a2 List.list -> 'a1 **)
 504 let rec fold_left_i_aux f x i = function
 505 | List.Nil -> x
 506 | List.Cons (hd, tl) -> fold_left_i_aux f (f i x hd) (Nat.S i) tl
 507
 508 (** val fold_left_i :
 509     (Nat.nat -> 'a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a1 **)
 510 let fold_left_i f x =
 511   fold_left_i_aux f x Nat.O
 512
 513 (** val function_apply : ('a1 -> 'a2) -> 'a1 -> 'a2 **)
 514 let function_apply f a =
 515   f a
 516
 517 (** val iterate : ('a1 -> 'a1) -> 'a1 -> Nat.nat -> 'a1 **)
 518 let rec iterate f a = function
 519 | Nat.O -> a
 520 | Nat.S o -> f (iterate f a o)
 521
 522 (** val division_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat **)
 523 let rec division_aux m n p =
 524   match ltb n (Nat.S p) with
 525   | Bool.True -> Nat.O
 526   | Bool.False ->
 527     (match m with
 528      | Nat.O -> Nat.O
 529      | Nat.S q -> Nat.S (division_aux q (Nat.minus n (Nat.S p)) p))
 530
 531 (** val division : Nat.nat -> Nat.nat -> Nat.nat **)
 532 let division m = function
 533 | Nat.O -> Nat.S m
 534 | Nat.S o -> division_aux m m o
 535
 536 (** val modulus_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat **)
 537 let rec modulus_aux m n p =
 538   match Nat.leb n p with
 539   | Bool.True -> n
 540   | Bool.False ->
 541     (match m with
 542      | Nat.O -> n
 543      | Nat.S o -> modulus_aux o (Nat.minus n (Nat.S p)) p)
 544
 545 (** val modulus : Nat.nat -> Nat.nat -> Nat.nat **)
 546 let modulus m = function
 547 | Nat.O -> m
 548 | Nat.S o -> modulus_aux m m o
 549
 550 (** val divide_with_remainder :
 551     Nat.nat -> Nat.nat -> (Nat.nat, Nat.nat) Types.prod **)
 552 let divide_with_remainder m n =
 553   { Types.fst = (division m n); Types.snd = (modulus m n) }
 554
 555 (** val less_than_or_equal_b_elim :
 556     Nat.nat -> Nat.nat -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 557 let less_than_or_equal_b_elim m n h1 h2 =
 558   (match Nat.leb m n with
 559    | Bool.True -> (fun _ _ -> h1 __)
 560    | Bool.False -> (fun _ _ -> h2 __)) __ __
 561
 562 open Div_and_mod
 563
 564 (** val dpi1__o__bool_to_Prop__o__inject :
 565     (Bool.bool, 'a1) Types.dPair -> __ Types.sig0 **)
 566 let dpi1__o__bool_to_Prop__o__inject x2 =
 567   __
 568
 569 (** val eject__o__bool_to_Prop__o__inject :
 570     Bool.bool Types.sig0 -> __ Types.sig0 **)
 571 let eject__o__bool_to_Prop__o__inject x2 =
 572   __
 573
 574 (** val bool_to_Prop__o__inject : Bool.bool -> __ Types.sig0 **)
 575 let bool_to_Prop__o__inject x1 =
 576   __
 577
 578 (** val dpi1__o__bool_to_Prop_to_eq__o__inject :
 579     Bool.bool -> (__, 'a1) Types.dPair -> __ Types.sig0 **)
 580 let dpi1__o__bool_to_Prop_to_eq__o__inject x0 x3 =
 581   __
 582
 583 (** val eject__o__bool_to_Prop_to_eq__o__inject :
 584     Bool.bool -> __ Types.sig0 -> __ Types.sig0 **)
 585 let eject__o__bool_to_Prop_to_eq__o__inject x0 x3 =
 586   __
 587
 588 (** val bool_to_Prop_to_eq__o__inject : Bool.bool -> __ Types.sig0 **)
 589 let bool_to_Prop_to_eq__o__inject x0 =
 590   __
 591
 592 (** val dpi1__o__not_bool_to_Prop_to_eq__o__inject :
 593     Bool.bool -> (__, 'a1) Types.dPair -> __ Types.sig0 **)
 594 let dpi1__o__not_bool_to_Prop_to_eq__o__inject x0 x3 =
 595   __
 596
 597 (** val eject__o__not_bool_to_Prop_to_eq__o__inject :
 598     Bool.bool -> __ Types.sig0 -> __ Types.sig0 **)
 599 let eject__o__not_bool_to_Prop_to_eq__o__inject x0 x3 =
 600   __
 601
 602 (** val not_bool_to_Prop_to_eq__o__inject : Bool.bool -> __ Types.sig0 **)
 603 let not_bool_to_Prop_to_eq__o__inject x0 =
 604   __
 605
 606 (** val if_then_else_safe :
 607     Bool.bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 608 let if_then_else_safe b f g =
 609   (match b with
 610    | Bool.True -> f
 611    | Bool.False -> g) __
 612
 613 (** val dpi1__o__not_neq_None__o__inject :
 614     'a1 Types.option -> (__, 'a2) Types.dPair -> __ Types.sig0 **)
 615 let dpi1__o__not_neq_None__o__inject x1 x4 =
 616   __
 617
 618 (** val eject__o__not_neq_None__o__inject :
 619     'a1 Types.option -> __ Types.sig0 -> __ Types.sig0 **)
 620 let eject__o__not_neq_None__o__inject x1 x4 =
 621   __
 622
 623 (** val not_neq_None__o__inject : 'a1 Types.option -> __ Types.sig0 **)
 624 let not_neq_None__o__inject x1 =
 625   __
 626
 627 (** val prod_jmdiscr :
 628     ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod -> __ **)
 629 let prod_jmdiscr x y =
 630   Logic.eq_rect_Type2 x
 631     (let { Types.fst = a0; Types.snd = a10 } = x in
 632     Obj.magic (fun _ dH -> dH __ __)) y
 633
 634 (** val eq_rect_Type1_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
 635 let eq_rect_Type1_r a h x =
 636   (fun _ auto -> auto) __ h
 637
 638 (** val some_Some_elim : 'a1 -> 'a1 -> (__ -> 'a2) -> 'a2 **)
 639 let some_Some_elim x y h =
 640   h __
 641
 642 (** val pose : 'a1 -> ('a1 -> __ -> 'a2) -> 'a2 **)
 643 let pose a auto =
 644   auto a __
 645
 646 (** val eq_sum :
 647     ('a1 -> 'a1 -> Bool.bool) -> ('a2 -> 'a2 -> Bool.bool) -> ('a1, 'a2)
 648     Types.sum -> ('a1, 'a2) Types.sum -> Bool.bool **)
 649 let eq_sum leq req left right =
 650   match left with
 651   | Types.Inl l ->
 652     (match right with
 653      | Types.Inl l' -> leq l l'
 654      | Types.Inr x -> Bool.False)
 655   | Types.Inr r ->
 656     (match right with
 657      | Types.Inl x -> Bool.False
 658      | Types.Inr r' -> req r r')
 659
 660 (** val eq_prod :
 661     ('a1 -> 'a1 -> Bool.bool) -> ('a2 -> 'a2 -> Bool.bool) -> ('a1, 'a2)
 662     Types.prod -> ('a1, 'a2) Types.prod -> Bool.bool **)
 663 let eq_prod leq req left right =
 664   let { Types.fst = l; Types.snd = r } = left in
 665   let { Types.fst = l'; Types.snd = r' } = right in
 666   Bool.andb (leq l l') (req r r')
 667