extracted/bitVectorTrieSet.ml

   1 open Preamble
   2
   3 open Deqsets
   4
   5 open Setoids
   6
   7 open Monad
   8
   9 open Option
  10
  11 open Extranat
  12
  13 open Vector
  14
  15 open Div_and_mod
  16
  17 open Jmeq
  18
  19 open Russell
  20
  21 open List
  22
  23 open Util
  24
  25 open FoldStuff
  26
  27 open Bool
  28
  29 open Relations
  30
  31 open Nat
  32
  33 open BitVector
  34
  35 open Hints_declaration
  36
  37 open Core_notation
  38
  39 open Pts
  40
  41 open Logic
  42
  43 open Types
  44
  45 open BitVectorTrie
  46
  47 type bitVectorTrieSet = Types.unit0 BitVectorTrie.bitVectorTrie
  48
  49 (** val set_member :
  50     Nat.nat -> Bool.bool Vector.vector -> bitVectorTrieSet -> Bool.bool **)
  51 let rec set_member n p b =
  52   (match p with
  53    | Vector.VEmpty ->
  54      (match b with
  55       | BitVectorTrie.Leaf x -> (fun _ -> Bool.True)
  56       | BitVectorTrie.Node (x, x0, x1) ->
  57         (fun _ -> Obj.magic Nat.nat_discr (Nat.S x) Nat.O __)
  58       | BitVectorTrie.Stub x -> (fun _ -> Bool.False))
  59    | Vector.VCons (o, hd, tl) ->
  60      (match b with
  61       | BitVectorTrie.Leaf x ->
  62         (fun _ -> Obj.magic Nat.nat_discr Nat.O (Nat.S o) __)
  63       | BitVectorTrie.Node (p0, l, r) ->
  64         (match hd with
  65          | Bool.True -> (fun _ -> set_member o tl r)
  66          | Bool.False -> (fun _ -> set_member o tl l))
  67       | BitVectorTrie.Stub x -> (fun _ -> Bool.False))) __
  68
  69 (** val set_union :
  70     Nat.nat -> bitVectorTrieSet -> bitVectorTrieSet -> bitVectorTrieSet **)
  71 let rec set_union n = function
  72 | BitVectorTrie.Leaf l -> (fun c -> BitVectorTrie.Leaf l)
  73 | BitVectorTrie.Node (p, l, r) ->
  74   (fun c ->
  75     (match c with
  76      | BitVectorTrie.Leaf x ->
  77        (fun _ -> Obj.magic Nat.nat_discr Nat.O (Nat.S p) __)
  78      | BitVectorTrie.Node (p', l', r') ->
  79        (fun _ -> BitVectorTrie.Node (p, (set_union p l l'),
  80          (set_union p r r')))
  81      | BitVectorTrie.Stub x -> (fun _ -> BitVectorTrie.Node (p, l, r))) __)
  82 | BitVectorTrie.Stub x -> (fun c -> c)
  83
  84 (** val set_eq :
  85     Nat.nat -> bitVectorTrieSet -> bitVectorTrieSet -> Bool.bool **)
  86 let rec set_eq n b c =
  87   (match b with
  88    | BitVectorTrie.Leaf l ->
  89      (match c with
  90       | BitVectorTrie.Leaf l' -> (fun _ -> Bool.True)
  91       | BitVectorTrie.Node (x, x0, x1) -> (fun _ -> Bool.False)
  92       | BitVectorTrie.Stub x -> (fun _ -> Bool.False))
  93    | BitVectorTrie.Node (h, l, r) ->
  94      (match c with
  95       | BitVectorTrie.Leaf x -> (fun _ -> Bool.False)
  96       | BitVectorTrie.Node (h', l', r') ->
  97         (fun _ ->
  98           Bool.andb (set_eq h l r) (set_eq h r (Logic.eq_rect_Type0 h' r' h)))
  99       | BitVectorTrie.Stub x -> (fun _ -> Bool.False))
 100    | BitVectorTrie.Stub s ->
 101      (match c with
 102       | BitVectorTrie.Leaf x -> (fun _ -> Bool.False)
 103       | BitVectorTrie.Node (x, x0, x1) -> (fun _ -> Bool.False)
 104       | BitVectorTrie.Stub s' -> (fun _ -> Util.eq_nat s s'))) __
 105
 106 (** val set_insert :
 107     Nat.nat -> BitVector.bitVector -> bitVectorTrieSet -> Types.unit0
 108     BitVectorTrie.bitVectorTrie **)
 109 let set_insert n b s =
 110   BitVectorTrie.insert n b Types.It s
 111
 112 (** val set_empty : Nat.nat -> Types.unit0 BitVectorTrie.bitVectorTrie **)
 113 let set_empty n =
 114   BitVectorTrie.Stub n
 115
 116 (** val set_singleton :
 117     Nat.nat -> BitVector.bitVector -> Types.unit0 BitVectorTrie.bitVectorTrie **)
 118 let set_singleton n b =
 119   BitVectorTrie.insert n b Types.It (set_empty n)
 120