extracted/list.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 type 'a list =
  20 | Nil
  21 | Cons of 'a * 'a list
  22
  23 (** val list_rect_Type4 :
  24     'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2 **)
  25 let rec list_rect_Type4 h_nil h_cons = function
  26 | Nil -> h_nil
  27 | Cons (x_723, x_722) ->
  28   h_cons x_723 x_722 (list_rect_Type4 h_nil h_cons x_722)
  29
  30 (** val list_rect_Type3 :
  31     'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2 **)
  32 let rec list_rect_Type3 h_nil h_cons = function
  33 | Nil -> h_nil
  34 | Cons (x_733, x_732) ->
  35   h_cons x_733 x_732 (list_rect_Type3 h_nil h_cons x_732)
  36
  37 (** val list_rect_Type2 :
  38     'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2 **)
  39 let rec list_rect_Type2 h_nil h_cons = function
  40 | Nil -> h_nil
  41 | Cons (x_738, x_737) ->
  42   h_cons x_738 x_737 (list_rect_Type2 h_nil h_cons x_737)
  43
  44 (** val list_rect_Type1 :
  45     'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2 **)
  46 let rec list_rect_Type1 h_nil h_cons = function
  47 | Nil -> h_nil
  48 | Cons (x_743, x_742) ->
  49   h_cons x_743 x_742 (list_rect_Type1 h_nil h_cons x_742)
  50
  51 (** val list_rect_Type0 :
  52     'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2 **)
  53 let rec list_rect_Type0 h_nil h_cons = function
  54 | Nil -> h_nil
  55 | Cons (x_748, x_747) ->
  56   h_cons x_748 x_747 (list_rect_Type0 h_nil h_cons x_747)
  57
  58 (** val list_inv_rect_Type4 :
  59     'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2)
  60     -> 'a2 **)
  61 let list_inv_rect_Type4 hterm h1 h2 =
  62   let hcut = list_rect_Type4 h1 h2 hterm in hcut __
  63
  64 (** val list_inv_rect_Type3 :
  65     'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2)
  66     -> 'a2 **)
  67 let list_inv_rect_Type3 hterm h1 h2 =
  68   let hcut = list_rect_Type3 h1 h2 hterm in hcut __
  69
  70 (** val list_inv_rect_Type2 :
  71     'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2)
  72     -> 'a2 **)
  73 let list_inv_rect_Type2 hterm h1 h2 =
  74   let hcut = list_rect_Type2 h1 h2 hterm in hcut __
  75
  76 (** val list_inv_rect_Type1 :
  77     'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2)
  78     -> 'a2 **)
  79 let list_inv_rect_Type1 hterm h1 h2 =
  80   let hcut = list_rect_Type1 h1 h2 hterm in hcut __
  81
  82 (** val list_inv_rect_Type0 :
  83     'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2)
  84     -> 'a2 **)
  85 let list_inv_rect_Type0 hterm h1 h2 =
  86   let hcut = list_rect_Type0 h1 h2 hterm in hcut __
  87
  88 (** val list_discr : 'a1 list -> 'a1 list -> __ **)
  89 let list_discr x y =
  90   Logic.eq_rect_Type2 x
  91     (match x with
  92      | Nil -> Obj.magic (fun _ dH -> dH)
  93      | Cons (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
  94
  95 (** val append : 'a1 list -> 'a1 list -> 'a1 list **)
  96 let rec append l1 l2 =
  97   match l1 with
  98   | Nil -> l2
  99   | Cons (hd, tl) -> Cons (hd, (append tl l2))
 100
 101 (** val hd : 'a1 list -> 'a1 -> 'a1 **)
 102 let hd l d =
 103   match l with
 104   | Nil -> d
 105   | Cons (a, x) -> a
 106
 107 (** val tail : 'a1 list -> 'a1 list **)
 108 let tail = function
 109 | Nil -> Nil
 110 | Cons (hd0, tl) -> tl
 111
 112 (** val option_hd : 'a1 list -> 'a1 Types.option **)
 113 let option_hd = function
 114 | Nil -> Types.None
 115 | Cons (a, x) -> Types.Some a
 116
 117 (** val option_cons : 'a1 Types.option -> 'a1 list -> 'a1 list **)
 118 let option_cons c l =
 119   match c with
 120   | Types.None -> l
 121   | Types.Some c0 -> Cons (c0, l)
 122
 123 (** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **)
 124 let rec map f = function
 125 | Nil -> Nil
 126 | Cons (x, tl) -> Cons ((f x), (map f tl))
 127
 128 (** val foldr : ('a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 list -> 'a2 **)
 129 let rec foldr f b = function
 130 | Nil -> b
 131 | Cons (a, l0) -> f a (foldr f b l0)
 132
 133 (** val filter : ('a1 -> Bool.bool) -> 'a1 list -> 'a1 list **)
 134 let filter p =
 135   foldr (fun x l0 ->
 136     match p x with
 137     | Bool.True -> Cons (x, l0)
 138     | Bool.False -> l0) Nil
 139
 140 (** val compose : ('a1 -> 'a2 -> 'a3) -> 'a1 list -> 'a2 list -> 'a3 list **)
 141 let compose f l1 l2 =
 142   foldr (fun i acc -> append (map (f i) l2) acc) Nil l1
 143
 144 (** val rev_append : 'a1 list -> 'a1 list -> 'a1 list **)
 145 let rec rev_append l1 l2 =
 146   match l1 with
 147   | Nil -> l2
 148   | Cons (a, tl) -> rev_append tl (Cons (a, l2))
 149
 150 (** val reverse : 'a1 list -> 'a1 list **)
 151 let reverse l =
 152   rev_append l Nil
 153
 154 (** val length : 'a1 list -> Nat.nat **)
 155 let rec length = function
 156 | Nil -> Nat.O
 157 | Cons (a, tl) -> Nat.S (length tl)
 158
 159 (** val split_rev :
 160     'a1 list -> 'a1 list -> Nat.nat -> ('a1 list, 'a1 list) Types.prod **)
 161 let rec split_rev l acc = function
 162 | Nat.O -> { Types.fst = acc; Types.snd = l }
 163 | Nat.S m ->
 164   (match l with
 165    | Nil -> { Types.fst = acc; Types.snd = Nil }
 166    | Cons (a, tl) -> split_rev tl (Cons (a, acc)) m)
 167
 168 (** val split : 'a1 list -> Nat.nat -> ('a1 list, 'a1 list) Types.prod **)
 169 let split l n =
 170   let { Types.fst = l1; Types.snd = l2 } = split_rev l Nil n in
 171   { Types.fst = (reverse l1); Types.snd = l2 }
 172
 173 (** val flatten : 'a1 list list -> 'a1 list **)
 174 let flatten l =
 175   foldr append Nil l
 176
 177 (** val nth : Nat.nat -> 'a1 list -> 'a1 -> 'a1 **)
 178 let rec nth n l d =
 179   match n with
 180   | Nat.O -> hd l d
 181   | Nat.S m -> nth m (tail l) d
 182
 183 (** val nth_opt : Nat.nat -> 'a1 list -> 'a1 Types.option **)
 184 let rec nth_opt n = function
 185 | Nil -> Types.None
 186 | Cons (h, t) ->
 187   (match n with
 188    | Nat.O -> Types.Some h
 189    | Nat.S m -> nth_opt m t)
 190
 191 (** val fold :
 192     ('a2 -> 'a2 -> 'a2) -> 'a2 -> ('a1 -> Bool.bool) -> ('a1 -> 'a2) -> 'a1
 193     list -> 'a2 **)
 194 let rec fold op b p f = function
 195 | Nil -> b
 196 | Cons (a, l0) ->
 197   (match p a with
 198    | Bool.True -> op (f a) (fold op b p f l0)
 199    | Bool.False -> fold op b p f l0)
 200
 201 type 'a aop =
 202   'a -> 'a -> 'a
 203   (* singleton inductive, whose constructor was mk_Aop *)
 204
 205 (** val aop_rect_Type4 :
 206     'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
 207 let rec aop_rect_Type4 nil h_mk_Aop x_783 =
 208   let op = x_783 in h_mk_Aop op __ __ __
 209
 210 (** val aop_rect_Type5 :
 211     'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
 212 let rec aop_rect_Type5 nil h_mk_Aop x_785 =
 213   let op = x_785 in h_mk_Aop op __ __ __
 214
 215 (** val aop_rect_Type3 :
 216     'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
 217 let rec aop_rect_Type3 nil h_mk_Aop x_787 =
 218   let op = x_787 in h_mk_Aop op __ __ __
 219
 220 (** val aop_rect_Type2 :
 221     'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
 222 let rec aop_rect_Type2 nil h_mk_Aop x_789 =
 223   let op = x_789 in h_mk_Aop op __ __ __
 224
 225 (** val aop_rect_Type1 :
 226     'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
 227 let rec aop_rect_Type1 nil h_mk_Aop x_791 =
 228   let op = x_791 in h_mk_Aop op __ __ __
 229
 230 (** val aop_rect_Type0 :
 231     'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
 232 let rec aop_rect_Type0 nil h_mk_Aop x_793 =
 233   let op = x_793 in h_mk_Aop op __ __ __
 234
 235 (** val op : 'a1 -> 'a1 aop -> 'a1 -> 'a1 -> 'a1 **)
 236 let rec op nil xxx =
 237   let yyy = xxx in yyy
 238
 239 (** val aop_inv_rect_Type4 :
 240     'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
 241     'a2 **)
 242 let aop_inv_rect_Type4 x2 hterm h1 =
 243   let hcut = aop_rect_Type4 x2 h1 hterm in hcut __
 244
 245 (** val aop_inv_rect_Type3 :
 246     'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
 247     'a2 **)
 248 let aop_inv_rect_Type3 x2 hterm h1 =
 249   let hcut = aop_rect_Type3 x2 h1 hterm in hcut __
 250
 251 (** val aop_inv_rect_Type2 :
 252     'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
 253     'a2 **)
 254 let aop_inv_rect_Type2 x2 hterm h1 =
 255   let hcut = aop_rect_Type2 x2 h1 hterm in hcut __
 256
 257 (** val aop_inv_rect_Type1 :
 258     'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
 259     'a2 **)
 260 let aop_inv_rect_Type1 x2 hterm h1 =
 261   let hcut = aop_rect_Type1 x2 h1 hterm in hcut __
 262
 263 (** val aop_inv_rect_Type0 :
 264     'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
 265     'a2 **)
 266 let aop_inv_rect_Type0 x2 hterm h1 =
 267   let hcut = aop_rect_Type0 x2 h1 hterm in hcut __
 268
 269 (** val aop_discr : 'a1 -> 'a1 aop -> 'a1 aop -> __ **)
 270 let aop_discr a2 x y =
 271   Logic.eq_rect_Type2 x
 272     (let a0 = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y
 273
 274 (** val dpi1__o__op :
 275     'a1 -> ('a1 aop, 'a2) Types.dPair -> 'a1 -> 'a1 -> 'a1 **)
 276 let dpi1__o__op x1 x3 =
 277   op x1 x3.Types.dpi1
 278
 279 (** val lhd : 'a1 list -> Nat.nat -> 'a1 list **)
 280 let rec lhd l = function
 281 | Nat.O -> Nil
 282 | Nat.S n0 ->
 283   (match l with
 284    | Nil -> Nil
 285    | Cons (a, l0) -> Cons (a, (lhd l0 n0)))
 286
 287 (** val ltl : 'a1 list -> Nat.nat -> 'a1 list **)
 288 let rec ltl l = function
 289 | Nat.O -> l
 290 | Nat.S n0 -> ltl (tail l) n0
 291
 292 (** val find : ('a1 -> 'a2 Types.option) -> 'a1 list -> 'a2 Types.option **)
 293 let rec find f = function
 294 | Nil -> Types.None
 295 | Cons (h, t) ->
 296   (match f h with
 297    | Types.None -> find f t
 298    | Types.Some b -> Types.Some b)
 299
 300 (** val position_of_aux :
 301     ('a1 -> Bool.bool) -> 'a1 list -> Nat.nat -> Nat.nat Types.option **)
 302 let rec position_of_aux found l acc =
 303   match l with
 304   | Nil -> Types.None
 305   | Cons (h, t) ->
 306     (match found h with
 307      | Bool.True -> Types.Some acc
 308      | Bool.False -> position_of_aux found t (Nat.S acc))
 309
 310 (** val position_of :
 311     ('a1 -> Bool.bool) -> 'a1 list -> Nat.nat Types.option **)
 312 let position_of found l =
 313   position_of_aux found l Nat.O
 314
 315 (** val make_list : 'a1 -> Nat.nat -> 'a1 list **)
 316 let rec make_list a = function
 317 | Nat.O -> Nil
 318 | Nat.S m -> Cons (a, (make_list a m))
 319