source: extracted/genMem.mli @ 2960

Last change on this file since 2960 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.1 KB
RevLine 
[2601]1open Preamble
2
3open Div_and_mod
4
5open Jmeq
6
7open Russell
8
9open Util
10
11open Bool
12
13open Relations
14
15open Nat
16
17open List
18
19open Hints_declaration
20
21open Core_notation
22
23open Pts
24
25open Logic
26
27open Types
28
29open Extralib
30
31open Proper
32
33open PositiveMap
34
35open Deqsets
36
[2649]37open ErrorMessages
38
[2601]39open PreIdentifiers
40
41open Errors
42
43open Lists
44
45open Identifiers
46
47open Integers
48
49open AST
50
51open Division
52
[2717]53open Exp
54
[2601]55open Arithmetic
56
[2773]57open Setoids
58
59open Monad
60
61open Option
62
[2601]63open Extranat
64
65open Vector
66
67open FoldStuff
68
69open BitVector
70
71open Positive
72
73open Z
74
75open BitVectorZ
76
77open Pointers
78
79open Hide
80
81open ByteValues
82
[2773]83val update : Z.z -> 'a1 -> (Z.z -> 'a1) -> Z.z -> 'a1
[2601]84
85val update_block :
86  Pointers.block -> 'a1 -> (Pointers.block -> 'a1) -> Pointers.block -> 'a1
87
88type contentmap = Z.z -> ByteValues.beval
89
90type block_contents = { low : Z.z; high : Z.z; contents : contentmap }
91
92val block_contents_rect_Type4 :
93  (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1
94
95val block_contents_rect_Type5 :
96  (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1
97
98val block_contents_rect_Type3 :
99  (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1
100
101val block_contents_rect_Type2 :
102  (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1
103
104val block_contents_rect_Type1 :
105  (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1
106
107val block_contents_rect_Type0 :
108  (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1
109
110val low : block_contents -> Z.z
111
112val high : block_contents -> Z.z
113
114val contents : block_contents -> contentmap
115
116val block_contents_inv_rect_Type4 :
117  block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1
118
119val block_contents_inv_rect_Type3 :
120  block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1
121
122val block_contents_inv_rect_Type2 :
123  block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1
124
125val block_contents_inv_rect_Type1 :
126  block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1
127
128val block_contents_inv_rect_Type0 :
129  block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1
130
131val block_contents_discr : block_contents -> block_contents -> __
132
133val block_contents_jmdiscr : block_contents -> block_contents -> __
134
[2773]135type mem = { blocks : (Pointers.block -> block_contents); nextblock : Z.z }
[2601]136
137val mem_rect_Type4 :
[2773]138  ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1
[2601]139
140val mem_rect_Type5 :
[2773]141  ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1
[2601]142
143val mem_rect_Type3 :
[2773]144  ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1
[2601]145
146val mem_rect_Type2 :
[2773]147  ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1
[2601]148
149val mem_rect_Type1 :
[2773]150  ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1
[2601]151
152val mem_rect_Type0 :
[2773]153  ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1
[2601]154
[2773]155val blocks : mem -> Pointers.block -> block_contents
[2601]156
[2773]157val nextblock : mem -> Z.z
[2601]158
159val mem_inv_rect_Type4 :
[2773]160  mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
[2601]161  'a1
162
163val mem_inv_rect_Type3 :
[2773]164  mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
[2601]165  'a1
166
167val mem_inv_rect_Type2 :
[2773]168  mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
[2601]169  'a1
170
171val mem_inv_rect_Type1 :
[2773]172  mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
[2601]173  'a1
174
175val mem_inv_rect_Type0 :
[2773]176  mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
[2601]177  'a1
178
[2773]179val mem_discr : mem -> mem -> __
[2601]180
[2773]181val mem_jmdiscr : mem -> mem -> __
[2601]182
183val oneZ : Z.z
184
185val empty_block : Z.z -> Z.z -> block_contents
186
[2773]187val empty : mem
[2601]188
[2773]189val alloc : mem -> Z.z -> Z.z -> (mem, Pointers.block) Types.prod
[2601]190
[2773]191val free : mem -> Pointers.block -> mem
[2601]192
[2773]193val free_list : mem -> Pointers.block List.list -> mem
[2601]194
[2773]195val low_bound : mem -> Pointers.block -> Z.z
[2601]196
[2773]197val high_bound : mem -> Pointers.block -> Z.z
[2601]198
[2773]199val block_region : mem -> Pointers.block -> AST.region
[2601]200
201val do_if_in_bounds :
[2773]202  mem -> Pointers.pointer -> (Pointers.block -> block_contents -> Z.z -> 'a1)
203  -> 'a1 Types.option
[2601]204
[2773]205val beloadv : mem -> Pointers.pointer -> ByteValues.beval Types.option
[2601]206
207val bestorev :
[2773]208  mem -> Pointers.pointer -> ByteValues.beval -> mem Types.option
[2601]209
Note: See TracBrowser for help on using the repository browser.