extracted/bitVectorTrie.mli

   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
  52 val bitVectorTrie_rect_Type3 :
  53   ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
  54   -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2
  55
  56 val bitVectorTrie_rect_Type2 :
  57   ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
  58   -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2
  59
  60 val bitVectorTrie_rect_Type1 :
  61   ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
  62   -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2
  63
  64 val bitVectorTrie_rect_Type0 :
  65   ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
  66   -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2
  67
  68 val bitVectorTrie_inv_rect_Type4 :
  69   Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
  70   bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
  71   'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2
  72
  73 val bitVectorTrie_inv_rect_Type3 :
  74   Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
  75   bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
  76   'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2
  77
  78 val bitVectorTrie_inv_rect_Type2 :
  79   Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
  80   bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
  81   'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2
  82
  83 val bitVectorTrie_inv_rect_Type1 :
  84   Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
  85   bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
  86   'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2
  87
  88 val bitVectorTrie_inv_rect_Type0 :
  89   Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
  90   bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
  91   'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2
  92
  93 val bitVectorTrie_discr :
  94   Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> __
  95
  96 val bitVectorTrie_jmdiscr :
  97   Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> __
  98
  99 val fold :
 100   Nat.nat -> (BitVector.bitVector -> 'a1 -> 'a2 -> 'a2) -> 'a1 bitVectorTrie
 101   -> 'a2 -> 'a2
 102
 103 val bvtfold_aux :
 104   (BitVector.bitVector -> 'a1 -> 'a2 -> 'a2) -> 'a2 -> Nat.nat -> 'a1
 105   bitVectorTrie -> BitVector.bitVector -> 'a2
 106
 107 val lookup_opt :
 108   Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> 'a1 Types.option
 109
 110 val member : Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> Bool.bool
 111
 112 val lookup :
 113   Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> 'a1 -> 'a1
 114
 115 val prepare_trie_for_insertion :
 116   Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie
 117
 118 val insert :
 119   Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie -> 'a1
 120   bitVectorTrie
 121
 122 val update :
 123   Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie -> 'a1
 124   bitVectorTrie Types.option
 125
 126 val merge :
 127   Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie
 128
 129 open Deqsets
 130
 131 type strong_decidable = (__, __) Types.sum
 132
 133 val strong_decidable_in_codomain :
 134   Deqsets.deqSet -> Nat.nat -> __ bitVectorTrie -> __ -> strong_decidable
 135