source: extracted/bitVectorTrie.mli @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 8 years ago

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 3.6 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Char
14
15open String
16
17open Extranat
18
19open Vector
20
21open Div_and_mod
22
23open Jmeq
24
25open Russell
26
27open List
28
29open Util
30
31open FoldStuff
32
33open Bool
34
35open Relations
36
37open Nat
38
39open BitVector
40
41type 'a bitVectorTrie =
42| Leaf of 'a
43| Node of Nat.nat * 'a bitVectorTrie * 'a bitVectorTrie
44| Stub of Nat.nat
45
46val bitVectorTrie_rect_Type4 :
47  ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
48  -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2
49
50val bitVectorTrie_rect_Type3 :
51  ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
52  -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2
53
54val bitVectorTrie_rect_Type2 :
55  ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
56  -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2
57
58val bitVectorTrie_rect_Type1 :
59  ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
60  -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2
61
62val bitVectorTrie_rect_Type0 :
63  ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
64  -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2
65
66val bitVectorTrie_inv_rect_Type4 :
67  Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
68  bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
69  'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2
70
71val bitVectorTrie_inv_rect_Type3 :
72  Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
73  bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
74  'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2
75
76val bitVectorTrie_inv_rect_Type2 :
77  Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
78  bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
79  'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2
80
81val bitVectorTrie_inv_rect_Type1 :
82  Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
83  bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
84  'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2
85
86val bitVectorTrie_inv_rect_Type0 :
87  Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
88  bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
89  'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2
90
91val bitVectorTrie_discr :
92  Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> __
93
94val bitVectorTrie_jmdiscr :
95  Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> __
96
97val fold0 :
98  Nat.nat -> (BitVector.bitVector -> 'a1 -> 'a2 -> 'a2) -> 'a1 bitVectorTrie
99  -> 'a2 -> 'a2
100
101val bvtfold_aux :
102  (BitVector.bitVector -> 'a1 -> 'a2 -> 'a2) -> 'a2 -> Nat.nat -> 'a1
103  bitVectorTrie -> BitVector.bitVector -> 'a2
104
105val lookup_opt :
106  Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> 'a1 Types.option
107
108val member0 :
109  Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> Bool.bool
110
111val lookup :
112  Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> 'a1 -> 'a1
113
114val prepare_trie_for_insertion :
115  Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie
116
117val insert :
118  Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie -> 'a1
119  bitVectorTrie
120
121val update :
122  Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie -> 'a1
123  bitVectorTrie Types.option
124
125val merge :
126  Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie
127
Note: See TracBrowser for help on using the repository browser.