source: extracted/memoryInjections.mli @ 2717

Last change on this file since 2717 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: 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 BitVectorTrie
50
51open CostLabel
52
53open Coqlib
54
55open Proper
56
57open PositiveMap
58
59open Deqsets
60
61open ErrorMessages
62
63open PreIdentifiers
64
65open Errors
66
67open Extralib
68
69open Setoids
70
71open Monad
72
73open Option
74
75open Lists
76
77open Positive
78
79open Identifiers
80
81open Exp
82
83open Arithmetic
84
85open Vector
86
87open Div_and_mod
88
89open Jmeq
90
91open Russell
92
93open List
94
95open Util
96
97open FoldStuff
98
99open BitVector
100
101open Extranat
102
103open Bool
104
105open Relations
106
107open Nat
108
109open Integers
110
111open Hints_declaration
112
113open Core_notation
114
115open Pts
116
117open Logic
118
119open Types
120
121open AST
122
123open Csyntax
124
125open TypeComparison
126
127open Frontend_misc
128
129open MemProperties
130
131val zoo : Pointers.offset -> Z.z
132
133val boo : Z.z -> Pointers.offset
134
135val block_decidable_eq :
136  Pointers.block -> Pointers.block -> (__, __) Types.sum
137
138type embedding =
139  Pointers.block -> (Pointers.block, Pointers.offset) Types.prod Types.option
140
141val offset_plus : Pointers.offset -> Pointers.offset -> Pointers.offset
142
143val pointer_translation :
144  Pointers.pointer -> embedding -> Pointers.pointer Types.option
145
146val memory_inj_rect_Type4 :
147  embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
148  __ -> __ -> 'a1) -> 'a1
149
150val memory_inj_rect_Type5 :
151  embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
152  __ -> __ -> 'a1) -> 'a1
153
154val memory_inj_rect_Type3 :
155  embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
156  __ -> __ -> 'a1) -> 'a1
157
158val memory_inj_rect_Type2 :
159  embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
160  __ -> __ -> 'a1) -> 'a1
161
162val memory_inj_rect_Type1 :
163  embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
164  __ -> __ -> 'a1) -> 'a1
165
166val memory_inj_rect_Type0 :
167  embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
168  __ -> __ -> 'a1) -> 'a1
169
170val memory_inj_inv_rect_Type4 :
171  embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
172  __ -> __ -> __ -> 'a1) -> 'a1
173
174val memory_inj_inv_rect_Type3 :
175  embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
176  __ -> __ -> __ -> 'a1) -> 'a1
177
178val memory_inj_inv_rect_Type2 :
179  embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
180  __ -> __ -> __ -> 'a1) -> 'a1
181
182val memory_inj_inv_rect_Type1 :
183  embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
184  __ -> __ -> __ -> 'a1) -> 'a1
185
186val memory_inj_inv_rect_Type0 :
187  embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
188  __ -> __ -> __ -> 'a1) -> 'a1
189
190val memory_inj_jmdiscr : embedding -> GenMem.mem1 -> GenMem.mem1 -> __
191
192val typesize' : Csyntax.type0 -> Nat.nat
193
Note: See TracBrowser for help on using the repository browser.