source: driver/extracted/bitVectorTrieSet.ml @ 3106

Last change on this file since 3106 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 3.1 KB
Line 
1open Preamble
2
3open Deqsets
4
5open Setoids
6
7open Monad
8
9open Option
10
11open Extranat
12
13open Vector
14
15open Div_and_mod
16
17open Jmeq
18
19open Russell
20
21open List
22
23open Util
24
25open FoldStuff
26
27open Bool
28
29open Relations
30
31open Nat
32
33open BitVector
34
35open Hints_declaration
36
37open Core_notation
38
39open Pts
40
41open Logic
42
43open Types
44
45open BitVectorTrie
46
47type bitVectorTrieSet = Types.unit0 BitVectorTrie.bitVectorTrie
48
49(** val set_member :
50    Nat.nat -> Bool.bool Vector.vector -> bitVectorTrieSet -> Bool.bool **)
51let 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 **)
71let 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 **)
86let 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 **)
109let set_insert n b s =
110  BitVectorTrie.insert n b Types.It s
111
112(** val set_empty : Nat.nat -> Types.unit0 BitVectorTrie.bitVectorTrie **)
113let set_empty n =
114  BitVectorTrie.Stub n
115
116(** val set_singleton :
117    Nat.nat -> BitVector.bitVector -> Types.unit0 BitVectorTrie.bitVectorTrie **)
118let set_singleton n b =
119  BitVectorTrie.insert n b Types.It (set_empty n)
120
Note: See TracBrowser for help on using the repository browser.