source: driver/extracted/pointers.mli @ 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: 4.6 KB
Line 
1open Preamble
2
3open Division
4
5open Exp
6
7open Arithmetic
8
9open Setoids
10
11open Monad
12
13open Option
14
15open Extranat
16
17open Vector
18
19open Div_and_mod
20
21open Jmeq
22
23open Russell
24
25open List
26
27open Util
28
29open FoldStuff
30
31open BitVector
32
33open Types
34
35open Bool
36
37open Relations
38
39open Nat
40
41open Hints_declaration
42
43open Core_notation
44
45open Pts
46
47open Logic
48
49open Positive
50
51open Z
52
53open BitVectorZ
54
55open Proper
56
57open PositiveMap
58
59open Deqsets
60
61open ErrorMessages
62
63open PreIdentifiers
64
65open Errors
66
67open Extralib
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.