extracted/vector.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 Div_and_mod
  22
  23 open Jmeq
  24
  25 open Russell
  26
  27 open Util
  28
  29 open Setoids
  30
  31 open Monad
  32
  33 open Option
  34
  35 open Extranat
  36
  37 type 'a vector =
  38 | VEmpty
  39 | VCons of Nat.nat * 'a * 'a vector
  40
  41 (** val vector_rect_Type4 :
  42     'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
  43     vector -> 'a2 **)
  44 let rec vector_rect_Type4 h_VEmpty h_VCons x_1293 = function
  45 | VEmpty -> h_VEmpty
  46 | VCons (n, x_1296, x_1295) ->
  47   h_VCons n x_1296 x_1295 (vector_rect_Type4 h_VEmpty h_VCons n x_1295)
  48
  49 (** val vector_rect_Type3 :
  50     'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
  51     vector -> 'a2 **)
  52 let rec vector_rect_Type3 h_VEmpty h_VCons x_1305 = function
  53 | VEmpty -> h_VEmpty
  54 | VCons (n, x_1308, x_1307) ->
  55   h_VCons n x_1308 x_1307 (vector_rect_Type3 h_VEmpty h_VCons n x_1307)
  56
  57 (** val vector_rect_Type2 :
  58     'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
  59     vector -> 'a2 **)
  60 let rec vector_rect_Type2 h_VEmpty h_VCons x_1311 = function
  61 | VEmpty -> h_VEmpty
  62 | VCons (n, x_1314, x_1313) ->
  63   h_VCons n x_1314 x_1313 (vector_rect_Type2 h_VEmpty h_VCons n x_1313)
  64
  65 (** val vector_rect_Type1 :
  66     'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
  67     vector -> 'a2 **)
  68 let rec vector_rect_Type1 h_VEmpty h_VCons x_1317 = function
  69 | VEmpty -> h_VEmpty
  70 | VCons (n, x_1320, x_1319) ->
  71   h_VCons n x_1320 x_1319 (vector_rect_Type1 h_VEmpty h_VCons n x_1319)
  72
  73 (** val vector_rect_Type0 :
  74     'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
  75     vector -> 'a2 **)
  76 let rec vector_rect_Type0 h_VEmpty h_VCons x_1323 = function
  77 | VEmpty -> h_VEmpty
  78 | VCons (n, x_1326, x_1325) ->
  79   h_VCons n x_1326 x_1325 (vector_rect_Type0 h_VEmpty h_VCons n x_1325)
  80
  81 (** val vector_inv_rect_Type4 :
  82     Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1
  83     vector -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2 **)
  84 let vector_inv_rect_Type4 x2 hterm h1 h2 =
  85   let hcut = vector_rect_Type4 h1 h2 x2 hterm in hcut __ __
  86
  87 (** val vector_inv_rect_Type3 :
  88     Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1
  89     vector -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2 **)
  90 let vector_inv_rect_Type3 x2 hterm h1 h2 =
  91   let hcut = vector_rect_Type3 h1 h2 x2 hterm in hcut __ __
  92
  93 (** val vector_inv_rect_Type2 :
  94     Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1
  95     vector -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2 **)
  96 let vector_inv_rect_Type2 x2 hterm h1 h2 =
  97   let hcut = vector_rect_Type2 h1 h2 x2 hterm in hcut __ __
  98
  99 (** val vector_inv_rect_Type1 :
 100     Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1
 101     vector -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2 **)
 102 let vector_inv_rect_Type1 x2 hterm h1 h2 =
 103   let hcut = vector_rect_Type1 h1 h2 x2 hterm in hcut __ __
 104
 105 (** val vector_inv_rect_Type0 :
 106     Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1
 107     vector -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2 **)
 108 let vector_inv_rect_Type0 x2 hterm h1 h2 =
 109   let hcut = vector_rect_Type0 h1 h2 x2 hterm in hcut __ __
 110
 111 (** val vector_discr : Nat.nat -> 'a1 vector -> 'a1 vector -> __ **)
 112 let vector_discr a2 x y =
 113   Logic.eq_rect_Type2 x
 114     (match x with
 115      | VEmpty -> Obj.magic (fun _ dH -> dH)
 116      | VCons (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)) y
 117
 118 (** val vector_jmdiscr : Nat.nat -> 'a1 vector -> 'a1 vector -> __ **)
 119 let vector_jmdiscr a2 x y =
 120   Logic.eq_rect_Type2 x
 121     (match x with
 122      | VEmpty -> Obj.magic (fun _ dH -> dH)
 123      | VCons (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)) y
 124
 125 (** val get_index_v : Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 **)
 126 let rec get_index_v n v m =
 127   (match m with
 128    | Nat.O ->
 129      (match v with
 130       | VEmpty -> (fun _ -> assert false (* absurd case *))
 131       | VCons (p, hd, tl) -> (fun _ -> hd))
 132    | Nat.S o ->
 133      (match v with
 134       | VEmpty -> (fun _ -> assert false (* absurd case *))
 135       | VCons (p, hd, tl) -> (fun _ -> get_index_v p tl o))) __
 136
 137 (** val get_index' : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 **)
 138 let get_index' n m b =
 139   get_index_v (Nat.S (Nat.plus n m)) b n
 140
 141 (** val get_index_weak_v :
 142     Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 Types.option **)
 143 let rec get_index_weak_v n v = function
 144 | Nat.O ->
 145   (match v with
 146    | VEmpty -> Types.None
 147    | VCons (p, hd, tl) -> Types.Some hd)
 148 | Nat.S o ->
 149   (match v with
 150    | VEmpty -> Types.None
 151    | VCons (p, hd, tl) -> get_index_weak_v p tl o)
 152
 153 (** val set_index : Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 -> 'a1 vector **)
 154 let rec set_index n v m a =
 155   (match m with
 156    | Nat.O ->
 157      (match v with
 158       | VEmpty -> (fun _ -> VEmpty)
 159       | VCons (p, hd, tl) -> (fun _ -> VCons (p, a, tl)))
 160    | Nat.S o ->
 161      (match v with
 162       | VEmpty -> (fun _ -> VEmpty)
 163       | VCons (p, hd, tl) -> (fun _ -> VCons (p, hd, (set_index p tl o a)))))
 164     __
 165
 166 (** val set_index_weak :
 167     Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 -> 'a1 vector Types.option **)
 168 let rec set_index_weak n v m a =
 169   match m with
 170   | Nat.O ->
 171     (match v with
 172      | VEmpty -> Types.None
 173      | VCons (o, hd, tl) -> Types.Some v)
 174   | Nat.S o ->
 175     (match v with
 176      | VEmpty -> Types.None
 177      | VCons (p, hd, tl) ->
 178        let settail = set_index_weak p tl o a in
 179        (match settail with
 180         | Types.None -> Types.None
 181         | Types.Some j -> Types.Some v))
 182
 183 (** val drop :
 184     Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 vector Types.option **)
 185 let rec drop n v = function
 186 | Nat.O -> Types.Some v
 187 | Nat.S o ->
 188   (match v with
 189    | VEmpty -> Types.None
 190    | VCons (p, hd, tl) -> Types.None)
 191
 192 (** val head' : Nat.nat -> 'a1 vector -> 'a1 **)
 193 let head' n = function
 194 | VEmpty -> Obj.magic __
 195 | VCons (x, hd, x0) -> hd
 196
 197 (** val tail : Nat.nat -> 'a1 vector -> 'a1 vector **)
 198 let tail n = function
 199 | VEmpty -> Obj.magic __
 200 | VCons (m, hd, tl) -> tl
 201
 202 (** val vsplit' :
 203     Nat.nat -> Nat.nat -> 'a1 vector -> ('a1 vector, 'a1 vector) Types.prod **)
 204 let rec vsplit' m n =
 205   match m with
 206   | Nat.O -> (fun v -> { Types.fst = VEmpty; Types.snd = v })
 207   | Nat.S m' ->
 208     (fun v ->
 209       let { Types.fst = l; Types.snd = r } =
 210         vsplit' m' n (tail (Nat.plus m' n) v)
 211       in
 212       { Types.fst = (VCons (m', (head' (Nat.plus m' n) v), l)); Types.snd =
 213       r })
 214
 215 (** val vsplit :
 216     Nat.nat -> Nat.nat -> 'a1 vector -> ('a1 vector, 'a1 vector) Types.prod **)
 217 let rec vsplit m n v =
 218   vsplit' m n v
 219
 220 (** val head : Nat.nat -> 'a1 vector -> ('a1, 'a1 vector) Types.prod **)
 221 let head n v =
 222   (match v with
 223    | VEmpty -> (fun _ -> assert false (* absurd case *))
 224    | VCons (o, he, tl) -> (fun _ -> { Types.fst = he; Types.snd = tl })) __
 225
 226 (** val from_singl : 'a1 vector -> 'a1 **)
 227 let from_singl v =
 228   (head Nat.O v).Types.fst
 229
 230 (** val fold_right :
 231     Nat.nat -> ('a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 vector -> 'a2 **)
 232 let rec fold_right n f x = function
 233 | VEmpty -> x
 234 | VCons (n0, hd, tl) -> f hd (fold_right n0 f x tl)
 235
 236 (** val fold_right_i :
 237     Nat.nat -> (Nat.nat -> 'a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 vector -> 'a2 **)
 238 let rec fold_right_i n f x = function
 239 | VEmpty -> x
 240 | VCons (n0, hd, tl) -> f n0 hd (fold_right_i n0 f x tl)
 241
 242 (** val fold_right2_i :
 243     (Nat.nat -> 'a1 -> 'a2 -> 'a3 -> 'a3) -> 'a3 -> Nat.nat -> 'a1 vector ->
 244     'a2 vector -> 'a3 **)
 245 let rec fold_right2_i f c n v q =
 246   (match v with
 247    | VEmpty ->
 248      (match q with
 249       | VEmpty -> (fun _ -> c)
 250       | VCons (o, hd, tl) -> (fun _ -> assert false (* absurd case *)))
 251    | VCons (o, hd, tl) ->
 252      (match q with
 253       | VEmpty -> (fun _ -> assert false (* absurd case *))
 254       | VCons (p, hd', tl') ->
 255         (fun _ -> f o hd hd' (fold_right2_i f c o tl tl')))) __
 256
 257 (** val fold_left :
 258     Nat.nat -> ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 vector -> 'a1 **)
 259 let rec fold_left n f x = function
 260 | VEmpty -> x
 261 | VCons (n0, hd, tl) -> fold_left n0 f (f x hd) tl
 262
 263 (** val map : Nat.nat -> ('a1 -> 'a2) -> 'a1 vector -> 'a2 vector **)
 264 let rec map n f = function
 265 | VEmpty -> VEmpty
 266 | VCons (n0, hd, tl) -> VCons (n0, (f hd), (map n0 f tl))
 267
 268 (** val zip_with :
 269     Nat.nat -> ('a1 -> 'a2 -> 'a3) -> 'a1 vector -> 'a2 vector -> 'a3 vector **)
 270 let rec zip_with n f v q =
 271   (match v with
 272    | VEmpty -> (fun _ -> VEmpty)
 273    | VCons (n0, hd, tl) ->
 274      (match q with
 275       | VEmpty -> (fun _ -> Obj.magic Nat.nat_discr (Nat.S n0) Nat.O __)
 276       | VCons (m, hd', tl') ->
 277         (fun _ -> VCons (n0, (f hd hd'),
 278           (zip_with n0 f tl (Util.eq_rect_Type0_r m tl' n0)))))) __
 279
 280 (** val zip :
 281     Nat.nat -> 'a1 vector -> 'a2 vector -> ('a1, 'a2) Types.prod vector **)
 282 let zip n v q =
 283   zip_with n (fun x x0 -> { Types.fst = x; Types.snd = x0 }) v q
 284
 285 (** val replicate : Nat.nat -> 'a1 -> 'a1 vector **)
 286 let rec replicate n h =
 287   match n with
 288   | Nat.O -> VEmpty
 289   | Nat.S m -> VCons (m, h, (replicate m h))
 290
 291 (** val append :
 292     Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector -> 'a1 vector **)
 293 let rec append n m v q =
 294   match v with
 295   | VEmpty -> q
 296   | VCons (o, hd, tl) -> VCons ((Nat.plus o m), hd, (append o m tl q))
 297
 298 (** val scan_left :
 299     Nat.nat -> ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 vector -> 'a1 vector **)
 300 let rec scan_left n f a v =
 301   VCons (n, a,
 302     (match v with
 303      | VEmpty -> VEmpty
 304      | VCons (o, hd, tl) -> scan_left o f (f a hd) tl))
 305
 306 (** val scan_right :
 307     Nat.nat -> ('a1 -> 'a2 -> 'a1) -> 'a2 -> 'a1 vector -> 'a1 List.list **)
 308 let rec scan_right n f b = function
 309 | VEmpty -> List.Nil
 310 | VCons (o, hd, tl) -> List.Cons ((f hd b), (scan_right o f b tl))
 311
 312 (** val revapp :
 313     Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector -> 'a1 vector **)
 314 let rec revapp n m v acc =
 315   match v with
 316   | VEmpty -> acc
 317   | VCons (o, hd, tl) -> revapp o (Nat.S m) tl (VCons (m, hd, acc))
 318
 319 (** val reverse : Nat.nat -> 'a1 vector -> 'a1 vector **)
 320 let rec reverse n v =
 321   revapp n Nat.O v VEmpty
 322
 323 (** val pad_vector :
 324     'a1 -> Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector **)
 325 let rec pad_vector a n m v =
 326   match n with
 327   | Nat.O -> v
 328   | Nat.S n' -> VCons ((Nat.plus n' m), a, (pad_vector a n' m v))
 329
 330 (** val list_of_vector : Nat.nat -> 'a1 vector -> 'a1 List.list **)
 331 let rec list_of_vector n = function
 332 | VEmpty -> List.Nil
 333 | VCons (o, hd, tl) -> List.Cons (hd, (list_of_vector o tl))
 334
 335 (** val vector_of_list : 'a1 List.list -> 'a1 vector **)
 336 let rec vector_of_list = function
 337 | List.Nil -> VEmpty
 338 | List.Cons (hd, tl) -> VCons ((List.length tl), hd, (vector_of_list tl))
 339
 340 (** val rotate_left : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector **)
 341 let rec rotate_left n m v =
 342   match m with
 343   | Nat.O -> v
 344   | Nat.S o ->
 345     (match v with
 346      | VEmpty -> VEmpty
 347      | VCons (p, hd, tl) ->
 348        rotate_left (Nat.S p) o
 349          (append p (Nat.S Nat.O) tl (VCons (Nat.O, hd, VEmpty))))
 350
 351 (** val rotate_right : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector **)
 352 let rotate_right n m v =
 353   reverse n (rotate_left n m (reverse n v))
 354
 355 (** val shift_left_1 : Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector **)
 356 let shift_left_1 n v a =
 357   (match v with
 358    | VEmpty -> (fun _ -> assert false (* absurd case *))
 359    | VCons (o, hd, tl) ->
 360      (fun _ -> reverse (Nat.S o) (VCons (o, a, (reverse o tl))))) __
 361
 362 (** val switch_bv_plus : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector **)
 363 let switch_bv_plus n m i =
 364   i
 365
 366 (** val shift_right_1 : Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector **)
 367 let shift_right_1 n v a =
 368   let { Types.fst = v'; Types.snd = dropped } =
 369     vsplit n (Nat.S Nat.O) (switch_bv_plus (Nat.S Nat.O) n v)
 370   in
 371   VCons (n, a, v')
 372
 373 (** val shift_left :
 374     Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector **)
 375 let shift_left n m =
 376   match Extranat.nat_compare n m with
 377   | Extranat.Nat_lt (x, x0) -> (fun v a -> replicate x a)
 378   | Extranat.Nat_eq x -> (fun v a -> replicate x a)
 379   | Extranat.Nat_gt (d, m0) ->
 380     (fun v a ->
 381       let { Types.fst = v0; Types.snd = v' } = vsplit m0 (Nat.S d) v in
 382       switch_bv_plus (Nat.S d) m0 (append (Nat.S d) m0 v' (replicate m0 a)))
 383
 384 (** val shift_right :
 385     Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector **)
 386 let shift_right n m v a =
 387   Util.iterate (fun x -> shift_right_1 n x a) v m
 388
 389 (** val eq_v :
 390     Nat.nat -> ('a1 -> 'a1 -> Bool.bool) -> 'a1 vector -> 'a1 vector ->
 391     Bool.bool **)
 392 let rec eq_v n f b c =
 393   (match b with
 394    | VEmpty ->
 395      (fun c0 ->
 396        match c0 with
 397        | VEmpty -> Bool.True
 398        | VCons (x, x0, x1) -> Obj.magic __ x x0 x1)
 399    | VCons (m, hd, tl) ->
 400      (fun c0 -> Bool.andb (f hd (head' m c0)) (eq_v m f tl (tail m c0)))) c
 401
 402 (** val vector_inv_n : Nat.nat -> 'a1 vector -> __ **)
 403 let vector_inv_n n v =
 404   (match v with
 405    | VEmpty -> (fun _ -> Obj.magic (fun auto -> auto))
 406    | VCons (n0, auto, auto') ->
 407      (fun _ -> Obj.magic (fun auto'' -> auto'' auto auto'))) __
 408
 409 (** val eq_v_elim :
 410     ('a2 -> 'a2 -> Bool.bool) -> (__ -> 'a2 -> 'a2 -> (__ -> __) -> (__ ->
 411     __) -> __) -> Nat.nat -> 'a2 vector -> 'a2 vector -> (__ -> 'a1) -> (__
 412     -> 'a1) -> 'a1 **)
 413 let eq_v_elim f f_elim n x =
 414   vector_rect_Type0 (fun y ->
 415     Obj.magic vector_inv_n Nat.O y (fun auto auto' -> auto __))
 416     (fun m h t iH y ->
 417     Obj.magic vector_inv_n (Nat.S m) y (fun h' t' ht hf ->
 418       Obj.magic f_elim __ h h' (fun _ ->
 419         iH (tail m (VCons (m, h', t'))) (fun _ -> ht __) (fun _ -> hf __))
 420         (fun _ -> hf __))) n x
 421
 422 (** val mem :
 423     ('a1 -> 'a1 -> Bool.bool) -> Nat.nat -> 'a1 vector -> 'a1 -> Bool.bool **)
 424 let mem eq_a n l x =
 425   fold_right n (fun y v -> Bool.orb (eq_a x y) v) Bool.False l
 426
 427 (** val subvector_with :
 428     Nat.nat -> Nat.nat -> ('a1 -> 'a1 -> Bool.bool) -> 'a1 vector -> 'a1
 429     vector -> Bool.bool **)
 430 let rec subvector_with n m eq sub sup =
 431   match sub with
 432   | VEmpty -> Bool.True
 433   | VCons (n', hd, tl) ->
 434     (match mem eq m sup hd with
 435      | Bool.True -> subvector_with n' m eq tl sup
 436      | Bool.False -> Bool.False)
 437
 438 (** val vprefix :
 439     Nat.nat -> Nat.nat -> ('a1 -> 'a1 -> Bool.bool) -> 'a1 vector -> 'a1
 440     vector -> Bool.bool **)
 441 let rec vprefix n m test v1 v2 =
 442   match v1 with
 443   | VEmpty -> Bool.True
 444   | VCons (n', hd1, tl1) ->
 445     (match v2 with
 446      | VEmpty -> Bool.False
 447      | VCons (m', hd2, tl2) ->
 448        Bool.andb (test hd1 hd2) (vprefix n' m' test tl1 tl2))
 449
 450 (** val vsuffix :
 451     Nat.nat -> Nat.nat -> ('a1 -> 'a1 -> Bool.bool) -> 'a1 vector -> 'a1
 452     vector -> Bool.bool **)
 453 let rec vsuffix n m test v1 v2 =
 454   Util.if_then_else_safe (Nat.leb (Nat.S n) m) (fun _ ->
 455     (match v2 with
 456      | VEmpty -> (fun _ -> assert false (* absurd case *))
 457      | VCons (m', hd2, tl2) -> (fun _ -> vsuffix n m' test v1 tl2)) __)
 458     (fun _ ->
 459     match Nat.eqb n m with
 460     | Bool.True -> vprefix n m test v1 v2
 461     | Bool.False -> Bool.False)
 462
 463 (** val rvsplit : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector vector **)
 464 let rec rvsplit n m =
 465   match n with
 466   | Nat.O -> (fun x -> VEmpty)
 467   | Nat.S k ->
 468     (fun v ->
 469       let { Types.fst = pre; Types.snd = post } = vsplit m (Nat.times k m) v
 470       in
 471       VCons (k, pre, (rvsplit k m post)))
 472
 473 (** val vflatten : Nat.nat -> Nat.nat -> 'a1 vector vector -> 'a1 vector **)
 474 let rec vflatten n m = function
 475 | VEmpty -> VEmpty
 476 | VCons (n', hd, tl) -> append m (Nat.times n' m) hd (vflatten n' m tl)
 477