35 open Hints_declaration
47 type bitVectorTrieSet = Types.unit0 BitVectorTrie.bitVectorTrie
50 Nat.nat -> Bool.bool Vector.vector -> bitVectorTrieSet -> Bool.bool **)
51 let rec set_member n p b =
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) ->
61 | BitVectorTrie.Leaf x ->
62 (fun _ -> Obj.magic Nat.nat_discr Nat.O (Nat.S o) __)
63 | BitVectorTrie.Node (p0, l, r) ->
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))) __
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) ->
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'),
81 | BitVectorTrie.Stub x -> (fun _ -> BitVectorTrie.Node (p, l, r))) __)
82 | BitVectorTrie.Stub x -> (fun c -> c)
85 Nat.nat -> bitVectorTrieSet -> bitVectorTrieSet -> Bool.bool **)
86 let rec set_eq n b c =
88 | BitVectorTrie.Leaf l ->
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) ->
95 | BitVectorTrie.Leaf x -> (fun _ -> Bool.False)
96 | BitVectorTrie.Node (h', l', r') ->
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 ->
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'))) __
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
112 (** val set_empty : Nat.nat -> Types.unit0 BitVectorTrie.bitVectorTrie **)
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)