source: extracted/pointers.mli @ 2746

Last change on this file since 2746 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: 4.6 KB
Line 
1open Preamble
2
3open Division
4
5open Exp
6
7open Arithmetic
8
9open Extranat
10
11open Vector
12
13open Div_and_mod
14
15open Jmeq
16
17open Russell
18
19open List
20
21open Util
22
23open FoldStuff
24
25open BitVector
26
27open Types
28
29open Bool
30
31open Relations
32
33open Nat
34
35open Hints_declaration
36
37open Core_notation
38
39open Pts
40
41open Logic
42
43open Positive
44
45open Z
46
47open BitVectorZ
48
49open Proper
50
51open PositiveMap
52
53open Deqsets
54
55open ErrorMessages
56
57open PreIdentifiers
58
59open Errors
60
61open Extralib
62
63open Setoids
64
65open Monad
66
67open Option
68
69open Lists
70
71open Identifiers
72
73open Integers
74
75open AST
76
77type block =
78  Z.z
79  (* singleton inductive, whose constructor was mk_block *)
80
81val block_rect_Type4 : (Z.z -> 'a1) -> block -> 'a1
82
83val block_rect_Type5 : (Z.z -> 'a1) -> block -> 'a1
84
85val block_rect_Type3 : (Z.z -> 'a1) -> block -> 'a1
86
87val block_rect_Type2 : (Z.z -> 'a1) -> block -> 'a1
88
89val block_rect_Type1 : (Z.z -> 'a1) -> block -> 'a1
90
91val block_rect_Type0 : (Z.z -> 'a1) -> block -> 'a1
92
93val block_id : block -> Z.z
94
95val block_inv_rect_Type4 : block -> (Z.z -> __ -> 'a1) -> 'a1
96
97val block_inv_rect_Type3 : block -> (Z.z -> __ -> 'a1) -> 'a1
98
99val block_inv_rect_Type2 : block -> (Z.z -> __ -> 'a1) -> 'a1
100
101val block_inv_rect_Type1 : block -> (Z.z -> __ -> 'a1) -> 'a1
102
103val block_inv_rect_Type0 : block -> (Z.z -> __ -> 'a1) -> 'a1
104
105val block_discr : block -> block -> __
106
107val block_jmdiscr : block -> block -> __
108
109val block_region : block -> AST.region
110
111val dummy_block_code : block
112
113val eq_block : block -> block -> Bool.bool
114
115val block_eq : Deqsets.deqSet
116
117val offset_size : Nat.nat
118
119type offset =
120  BitVector.bitVector
121  (* singleton inductive, whose constructor was mk_offset *)
122
123val offset_rect_Type4 : (BitVector.bitVector -> 'a1) -> offset -> 'a1
124
125val offset_rect_Type5 : (BitVector.bitVector -> 'a1) -> offset -> 'a1
126
127val offset_rect_Type3 : (BitVector.bitVector -> 'a1) -> offset -> 'a1
128
129val offset_rect_Type2 : (BitVector.bitVector -> 'a1) -> offset -> 'a1
130
131val offset_rect_Type1 : (BitVector.bitVector -> 'a1) -> offset -> 'a1
132
133val offset_rect_Type0 : (BitVector.bitVector -> 'a1) -> offset -> 'a1
134
135val offv : offset -> BitVector.bitVector
136
137val offset_inv_rect_Type4 :
138  offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1
139
140val offset_inv_rect_Type3 :
141  offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1
142
143val offset_inv_rect_Type2 :
144  offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1
145
146val offset_inv_rect_Type1 :
147  offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1
148
149val offset_inv_rect_Type0 :
150  offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1
151
152val offset_discr : offset -> offset -> __
153
154val offset_jmdiscr : offset -> offset -> __
155
156val eq_offset : offset -> offset -> Bool.bool
157
158val offset_of_Z : Z.z -> offset
159
160val shift_offset : Nat.nat -> offset -> BitVector.bitVector -> offset
161
162val shift_offset_n :
163  Nat.nat -> offset -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
164  offset
165
166val neg_shift_offset : Nat.nat -> offset -> BitVector.bitVector -> offset
167
168val neg_shift_offset_n :
169  Nat.nat -> offset -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
170  offset
171
172val sub_offset : Nat.nat -> offset -> offset -> BitVector.bitVector
173
174val zero_offset : offset
175
176val lt_offset : offset -> offset -> Bool.bool
177
178type pointer = { pblock : block; poff : offset }
179
180val pointer_rect_Type4 : (block -> offset -> 'a1) -> pointer -> 'a1
181
182val pointer_rect_Type5 : (block -> offset -> 'a1) -> pointer -> 'a1
183
184val pointer_rect_Type3 : (block -> offset -> 'a1) -> pointer -> 'a1
185
186val pointer_rect_Type2 : (block -> offset -> 'a1) -> pointer -> 'a1
187
188val pointer_rect_Type1 : (block -> offset -> 'a1) -> pointer -> 'a1
189
190val pointer_rect_Type0 : (block -> offset -> 'a1) -> pointer -> 'a1
191
192val pblock : pointer -> block
193
194val poff : pointer -> offset
195
196val pointer_inv_rect_Type4 : pointer -> (block -> offset -> __ -> 'a1) -> 'a1
197
198val pointer_inv_rect_Type3 : pointer -> (block -> offset -> __ -> 'a1) -> 'a1
199
200val pointer_inv_rect_Type2 : pointer -> (block -> offset -> __ -> 'a1) -> 'a1
201
202val pointer_inv_rect_Type1 : pointer -> (block -> offset -> __ -> 'a1) -> 'a1
203
204val pointer_inv_rect_Type0 : pointer -> (block -> offset -> __ -> 'a1) -> 'a1
205
206val pointer_discr : pointer -> pointer -> __
207
208val pointer_jmdiscr : pointer -> pointer -> __
209
210val ptype : pointer -> AST.region
211
212val shift_pointer : Nat.nat -> pointer -> BitVector.bitVector -> pointer
213
214val shift_pointer_n :
215  Nat.nat -> pointer -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
216  pointer
217
218val neg_shift_pointer : Nat.nat -> pointer -> BitVector.bitVector -> pointer
219
220val neg_shift_pointer_n :
221  Nat.nat -> pointer -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
222  pointer
223
224val eq_pointer : pointer -> pointer -> Bool.bool
225
Note: See TracBrowser for help on using the repository browser.