extracted/bitVectorTrie.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 Setoids
  14
  15 open Monad
  16
  17 open Option
  18
  19 open Extranat
  20
  21 open Vector
  22
  23 open Div_and_mod
  24
  25 open Jmeq
  26
  27 open Russell
  28
  29 open List
  30
  31 open Util
  32
  33 open FoldStuff
  34
  35 open Bool
  36
  37 open Relations
  38
  39 open Nat
  40
  41 open BitVector
  42
  43 type 'a bitVectorTrie =
  44 | Leaf of 'a
  45 | Node of Nat.nat * 'a bitVectorTrie * 'a bitVectorTrie
  46 | Stub of Nat.nat
  47
  48 (** val bitVectorTrie_rect_Type4 :
  49     ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
  50     -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2 **)
  51 let rec bitVectorTrie_rect_Type4 h_Leaf h_Node h_Stub x_14760 = function
  52 | Leaf x_14762 -> h_Leaf x_14762
  53 | Node (n, x_14764, x_14763) ->
  54   h_Node n x_14764 x_14763
  55     (bitVectorTrie_rect_Type4 h_Leaf h_Node h_Stub n x_14764)
  56     (bitVectorTrie_rect_Type4 h_Leaf h_Node h_Stub n x_14763)
  57 | Stub n -> h_Stub n
  58
  59 (** val bitVectorTrie_rect_Type3 :
  60     ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
  61     -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2 **)
  62 let rec bitVectorTrie_rect_Type3 h_Leaf h_Node h_Stub x_14776 = function
  63 | Leaf x_14778 -> h_Leaf x_14778
  64 | Node (n, x_14780, x_14779) ->
  65   h_Node n x_14780 x_14779
  66     (bitVectorTrie_rect_Type3 h_Leaf h_Node h_Stub n x_14780)
  67     (bitVectorTrie_rect_Type3 h_Leaf h_Node h_Stub n x_14779)
  68 | Stub n -> h_Stub n
  69
  70 (** val bitVectorTrie_rect_Type2 :
  71     ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
  72     -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2 **)
  73 let rec bitVectorTrie_rect_Type2 h_Leaf h_Node h_Stub x_14784 = function
  74 | Leaf x_14786 -> h_Leaf x_14786
  75 | Node (n, x_14788, x_14787) ->
  76   h_Node n x_14788 x_14787
  77     (bitVectorTrie_rect_Type2 h_Leaf h_Node h_Stub n x_14788)
  78     (bitVectorTrie_rect_Type2 h_Leaf h_Node h_Stub n x_14787)
  79 | Stub n -> h_Stub n
  80
  81 (** val bitVectorTrie_rect_Type1 :
  82     ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
  83     -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2 **)
  84 let rec bitVectorTrie_rect_Type1 h_Leaf h_Node h_Stub x_14792 = function
  85 | Leaf x_14794 -> h_Leaf x_14794
  86 | Node (n, x_14796, x_14795) ->
  87   h_Node n x_14796 x_14795
  88     (bitVectorTrie_rect_Type1 h_Leaf h_Node h_Stub n x_14796)
  89     (bitVectorTrie_rect_Type1 h_Leaf h_Node h_Stub n x_14795)
  90 | Stub n -> h_Stub n
  91
  92 (** val bitVectorTrie_rect_Type0 :
  93     ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
  94     -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2 **)
  95 let rec bitVectorTrie_rect_Type0 h_Leaf h_Node h_Stub x_14800 = function
  96 | Leaf x_14802 -> h_Leaf x_14802
  97 | Node (n, x_14804, x_14803) ->
  98   h_Node n x_14804 x_14803
  99     (bitVectorTrie_rect_Type0 h_Leaf h_Node h_Stub n x_14804)
 100     (bitVectorTrie_rect_Type0 h_Leaf h_Node h_Stub n x_14803)
 101 | Stub n -> h_Stub n
 102
 103 (** val bitVectorTrie_inv_rect_Type4 :
 104     Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat ->
 105     'a1 bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __
 106     -> 'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2 **)
 107 let bitVectorTrie_inv_rect_Type4 x2 hterm h1 h2 h3 =
 108   let hcut = bitVectorTrie_rect_Type4 h1 h2 h3 x2 hterm in hcut __ __
 109
 110 (** val bitVectorTrie_inv_rect_Type3 :
 111     Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat ->
 112     'a1 bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __
 113     -> 'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2 **)
 114 let bitVectorTrie_inv_rect_Type3 x2 hterm h1 h2 h3 =
 115   let hcut = bitVectorTrie_rect_Type3 h1 h2 h3 x2 hterm in hcut __ __
 116
 117 (** val bitVectorTrie_inv_rect_Type2 :
 118     Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat ->
 119     'a1 bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __
 120     -> 'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2 **)
 121 let bitVectorTrie_inv_rect_Type2 x2 hterm h1 h2 h3 =
 122   let hcut = bitVectorTrie_rect_Type2 h1 h2 h3 x2 hterm in hcut __ __
 123
 124 (** val bitVectorTrie_inv_rect_Type1 :
 125     Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat ->
 126     'a1 bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __
 127     -> 'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2 **)
 128 let bitVectorTrie_inv_rect_Type1 x2 hterm h1 h2 h3 =
 129   let hcut = bitVectorTrie_rect_Type1 h1 h2 h3 x2 hterm in hcut __ __
 130
 131 (** val bitVectorTrie_inv_rect_Type0 :
 132     Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat ->
 133     'a1 bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __
 134     -> 'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2 **)
 135 let bitVectorTrie_inv_rect_Type0 x2 hterm h1 h2 h3 =
 136   let hcut = bitVectorTrie_rect_Type0 h1 h2 h3 x2 hterm in hcut __ __
 137
 138 (** val bitVectorTrie_discr :
 139     Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> __ **)
 140 let bitVectorTrie_discr a2 x y =
 141   Logic.eq_rect_Type2 x
 142     (match x with
 143      | Leaf a0 -> Obj.magic (fun _ dH -> dH __)
 144      | Node (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
 145      | Stub a0 -> Obj.magic (fun _ dH -> dH __)) y
 146
 147 (** val bitVectorTrie_jmdiscr :
 148     Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> __ **)
 149 let bitVectorTrie_jmdiscr a2 x y =
 150   Logic.eq_rect_Type2 x
 151     (match x with
 152      | Leaf a0 -> Obj.magic (fun _ dH -> dH __)
 153      | Node (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
 154      | Stub a0 -> Obj.magic (fun _ dH -> dH __)) y
 155
 156 (** val fold :
 157     Nat.nat -> (BitVector.bitVector -> 'a1 -> 'a2 -> 'a2) -> 'a1
 158     bitVectorTrie -> 'a2 -> 'a2 **)
 159 let rec fold n f t b =
 160   (match t with
 161    | Leaf l -> (fun _ -> f (BitVector.zero n) l b)
 162    | Node (h, l, r) ->
 163      (fun _ ->
 164        fold h (fun x -> f (Vector.VCons (h, Bool.False, x))) l
 165          (fold h (fun x -> f (Vector.VCons (h, Bool.True, x))) r b))
 166    | Stub x -> (fun _ -> b)) __
 167
 168 (** val bvtfold_aux :
 169     (BitVector.bitVector -> 'a1 -> 'a2 -> 'a2) -> 'a2 -> Nat.nat -> 'a1
 170     bitVectorTrie -> BitVector.bitVector -> 'a2 **)
 171 let rec bvtfold_aux f seed n x x0 =
 172   (match n with
 173    | Nat.O ->
 174      (fun _ trie path ->
 175        (match trie with
 176         | Leaf l -> (fun _ -> f path l seed)
 177         | Node (n', l, r) -> (fun _ -> assert false (* absurd case *))
 178         | Stub s -> (fun _ -> seed)) __)
 179    | Nat.S n' ->
 180      (fun _ trie path ->
 181        (match trie with
 182         | Leaf l -> (fun _ -> assert false (* absurd case *))
 183         | Node (n'', l, r) ->
 184           (fun _ ->
 185             bvtfold_aux f
 186               (bvtfold_aux f seed n' l (Vector.VCons
 187                 ((Nat.minus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 188                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 189                    (Nat.S Nat.O)))))))))))))))) (Nat.S n')), Bool.False,
 190                 path))) n' r (Vector.VCons
 191               ((Nat.minus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 192                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 193                  (Nat.S Nat.O)))))))))))))))) (Nat.S n')), Bool.True, path)))
 194         | Stub s -> (fun _ -> seed)) __)) __ x x0
 195
 196 (** val lookup_opt :
 197     Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> 'a1 Types.option **)
 198 let rec lookup_opt n b t =
 199   (match t with
 200    | Leaf l -> (fun x -> Types.Some l)
 201    | Node (h, l, r) ->
 202      (fun b0 ->
 203        lookup_opt h (Vector.tail h b0)
 204          (match Vector.head' h b0 with
 205           | Bool.True -> r
 206           | Bool.False -> l))
 207    | Stub x -> (fun x0 -> Types.None)) b
 208
 209 (** val member :
 210     Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> Bool.bool **)
 211 let member n b t =
 212   match lookup_opt n b t with
 213   | Types.None -> Bool.False
 214   | Types.Some x -> Bool.True
 215
 216 (** val lookup :
 217     Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> 'a1 -> 'a1 **)
 218 let rec lookup n b t a =
 219   (match b with
 220    | Vector.VEmpty ->
 221      (match t with
 222       | Leaf l -> (fun _ -> l)
 223       | Node (h, l, r) -> (fun _ -> assert false (* absurd case *))
 224       | Stub s -> (fun _ -> a))
 225    | Vector.VCons (o, hd, tl) ->
 226      (match t with
 227       | Leaf l -> (fun _ -> assert false (* absurd case *))
 228       | Node (h, l, r) ->
 229         (match hd with
 230          | Bool.True -> (fun _ -> lookup h tl r a)
 231          | Bool.False -> (fun _ -> lookup h tl l a))
 232       | Stub s -> (fun _ -> a))) __
 233
 234 (** val prepare_trie_for_insertion :
 235     Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie **)
 236 let rec prepare_trie_for_insertion n b a =
 237   match b with
 238   | Vector.VEmpty -> Leaf a
 239   | Vector.VCons (o, hd, tl) ->
 240     (match hd with
 241      | Bool.True -> Node (o, (Stub o), (prepare_trie_for_insertion o tl a))
 242      | Bool.False -> Node (o, (prepare_trie_for_insertion o tl a), (Stub o)))
 243
 244 (** val insert :
 245     Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie -> 'a1
 246     bitVectorTrie **)
 247 let rec insert n b a =
 248   match b with
 249   | Vector.VEmpty -> (fun x -> Leaf a)
 250   | Vector.VCons (o, hd, tl) ->
 251     (fun t ->
 252       (match t with
 253        | Leaf l -> (fun _ -> assert false (* absurd case *))
 254        | Node (p, l, r) ->
 255          (fun _ ->
 256            match hd with
 257            | Bool.True -> Node (o, l, (insert o tl a r))
 258            | Bool.False -> Node (o, (insert o tl a l), r))
 259        | Stub p ->
 260          (fun _ ->
 261            prepare_trie_for_insertion (Nat.S o) (Vector.VCons (o, hd, tl)) a))
 262         __)
 263
 264 (** val update :
 265     Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie -> 'a1
 266     bitVectorTrie Types.option **)
 267 let rec update n b a =
 268   match b with
 269   | Vector.VEmpty ->
 270     (fun t ->
 271       (match t with
 272        | Leaf x -> (fun _ -> Types.Some (Leaf a))
 273        | Node (x, x0, x1) -> (fun _ -> assert false (* absurd case *))
 274        | Stub x -> (fun _ -> Types.None)) __)
 275   | Vector.VCons (o, hd, tl) ->
 276     (fun t ->
 277       (match t with
 278        | Leaf l -> (fun _ -> assert false (* absurd case *))
 279        | Node (p, l, r) ->
 280          (fun _ ->
 281            match hd with
 282            | Bool.True ->
 283              Types.option_map (fun v -> Node (o, l, v)) (update o tl a r)
 284            | Bool.False ->
 285              Types.option_map (fun v -> Node (o, v, r)) (update o tl a l))
 286        | Stub p -> (fun _ -> Types.None)) __)
 287
 288 (** val merge :
 289     Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie **)
 290 let rec merge n = function
 291 | Leaf l ->
 292   (fun c ->
 293     match c with
 294     | Leaf a -> Leaf a
 295     | Node (x, x0, x1) -> Leaf l
 296     | Stub x -> Leaf l)
 297 | Node (p, l, r) ->
 298   (fun c ->
 299     (match c with
 300      | Leaf x -> (fun _ -> Obj.magic Nat.nat_discr Nat.O (Nat.S p) __)
 301      | Node (p', l', r') ->
 302        (fun _ -> Node (p, (merge p l l'), (merge p r r')))
 303      | Stub x -> (fun _ -> Node (p, l, r))) __)
 304 | Stub x -> (fun c -> c)
 305
 306 open Deqsets
 307
 308 type strong_decidable = (__, __) Types.sum
 309
 310 (** val strong_decidable_in_codomain :
 311     Deqsets.deqSet -> Nat.nat -> __ bitVectorTrie -> __ -> strong_decidable **)
 312 let strong_decidable_in_codomain a n m =
 313   bitVectorTrie_rect_Type0 (fun a' a0 ->
 314     Bool.bool_inv_rect_Type0 (Deqsets.eqb a a' a0) (fun _ -> Types.Inl __)
 315       (fun _ -> Types.Inr __)) (fun n0 l r hl hr a0 ->
 316     match hl a0 with
 317     | Types.Inl _ -> Types.Inl __
 318     | Types.Inr _ ->
 319       (match hr a0 with
 320        | Types.Inl _ -> Types.Inl __
 321        | Types.Inr _ -> Types.Inr __)) (fun n0 a0 -> Types.Inr __) n m
 322