source: extracted/bitVectorTrieSet.ml @ 2717

Last change on this file since 2717 was 2717, checked in by sacerdot, 7 years ago

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

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