source: driver/extracted/memoryInjections.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: 2.9 KB
Line 
1open Preamble
2
3open SmallstepExec
4
5open Cexec
6
7open Sets
8
9open Listb
10
11open IO
12
13open IOMonad
14
15open Star
16
17open ClassifyOp
18
19open Events
20
21open Smallstep
22
23open Extra_bool
24
25open Values
26
27open FrontEndVal
28
29open Hide
30
31open ByteValues
32
33open Division
34
35open Z
36
37open BitVectorZ
38
39open Pointers
40
41open GenMem
42
43open FrontEndMem
44
45open Globalenvs
46
47open Csem
48
49open CostLabel
50
51open Coqlib
52
53open Proper
54
55open PositiveMap
56
57open Deqsets
58
59open ErrorMessages
60
61open PreIdentifiers
62
63open Errors
64
65open Extralib
66
67open Lists
68
69open Positive
70
71open Identifiers
72
73open Exp
74
75open Arithmetic
76
77open Vector
78
79open Div_and_mod
80
81open Util
82
83open FoldStuff
84
85open BitVector
86
87open Jmeq
88
89open Russell
90
91open List
92
93open Setoids
94
95open Monad
96
97open Option
98
99open Extranat
100
101open Bool
102
103open Relations
104
105open Nat
106
107open Integers
108
109open Hints_declaration
110
111open Core_notation
112
113open Pts
114
115open Logic
116
117open Types
118
119open AST
120
121open Csyntax
122
123open TypeComparison
124
125open Frontend_misc
126
127open MemProperties
128
129val zoo : Pointers.offset -> Z.z
130
131val boo : Z.z -> Pointers.offset
132
133val block_decidable_eq :
134  Pointers.block -> Pointers.block -> (__, __) Types.sum
135
136type embedding =
137  Pointers.block -> (Pointers.block, Pointers.offset) Types.prod Types.option
138
139val offset_plus : Pointers.offset -> Pointers.offset -> Pointers.offset
140
141val pointer_translation :
142  Pointers.pointer -> embedding -> Pointers.pointer Types.option
143
144val memory_inj_rect_Type4 :
145  embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
146  -> __ -> 'a1) -> 'a1
147
148val memory_inj_rect_Type5 :
149  embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
150  -> __ -> 'a1) -> 'a1
151
152val memory_inj_rect_Type3 :
153  embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
154  -> __ -> 'a1) -> 'a1
155
156val memory_inj_rect_Type2 :
157  embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
158  -> __ -> 'a1) -> 'a1
159
160val memory_inj_rect_Type1 :
161  embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
162  -> __ -> 'a1) -> 'a1
163
164val memory_inj_rect_Type0 :
165  embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
166  -> __ -> 'a1) -> 'a1
167
168val memory_inj_inv_rect_Type4 :
169  embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
170  -> __ -> __ -> 'a1) -> 'a1
171
172val memory_inj_inv_rect_Type3 :
173  embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
174  -> __ -> __ -> 'a1) -> 'a1
175
176val memory_inj_inv_rect_Type2 :
177  embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
178  -> __ -> __ -> 'a1) -> 'a1
179
180val memory_inj_inv_rect_Type1 :
181  embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
182  -> __ -> __ -> 'a1) -> 'a1
183
184val memory_inj_inv_rect_Type0 :
185  embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
186  -> __ -> __ -> 'a1) -> 'a1
187
188val memory_inj_jmdiscr : embedding -> GenMem.mem -> GenMem.mem -> __
189
190val typesize' : Csyntax.type0 -> Nat.nat
191
Note: See TracBrowser for help on using the repository browser.