source: extracted/memoryInjections.ml @ 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: 5.1 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
131(** val zoo : Pointers.offset -> Z.z **)
132let zoo x =
133  BitVectorZ.z_of_unsigned_bitvector Pointers.offset_size (Pointers.offv x)
134
135(** val boo : Z.z -> Pointers.offset **)
136let boo x =
137  BitVectorZ.bitvector_of_Z Pointers.offset_size x
138
139(** val block_decidable_eq :
140    Pointers.block -> Pointers.block -> (__, __) Types.sum **)
141let block_decidable_eq clearme =
142  let a = clearme in
143  (fun clearme0 ->
144  let b = clearme0 in
145  (match Z.decidable_eq_Z_Type a b with
146   | Types.Inl _ -> Types.Inl __
147   | Types.Inr _ -> Types.Inr __))
148
149type embedding =
150  Pointers.block -> (Pointers.block, Pointers.offset) Types.prod Types.option
151
152(** val offset_plus :
153    Pointers.offset -> Pointers.offset -> Pointers.offset **)
154let offset_plus o1 o2 =
155  Arithmetic.addition_n Pointers.offset_size (Pointers.offv o1)
156    (Pointers.offv o2)
157
158(** val pointer_translation :
159    Pointers.pointer -> embedding -> Pointers.pointer Types.option **)
160let pointer_translation p e1 =
161  let { Pointers.pblock = pblock0; Pointers.poff = poff0 } = p in
162  (match e1 pblock0 with
163   | Types.None -> Types.None
164   | Types.Some loc ->
165     let { Types.fst = dest_block; Types.snd = dest_off } = loc in
166     let ptr = { Pointers.pblock = dest_block; Pointers.poff =
167       (offset_plus poff0 dest_off) }
168     in
169     Types.Some ptr)
170
171(** val memory_inj_rect_Type4 :
172    embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
173    __ -> __ -> 'a1) -> 'a1 **)
174let rec memory_inj_rect_Type4 e1 m1 m2 h_mk_memory_inj =
175  h_mk_memory_inj __ __ __ __ __ __ __
176
177(** val memory_inj_rect_Type5 :
178    embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
179    __ -> __ -> 'a1) -> 'a1 **)
180let rec memory_inj_rect_Type5 e1 m1 m2 h_mk_memory_inj =
181  h_mk_memory_inj __ __ __ __ __ __ __
182
183(** val memory_inj_rect_Type3 :
184    embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
185    __ -> __ -> 'a1) -> 'a1 **)
186let rec memory_inj_rect_Type3 e1 m1 m2 h_mk_memory_inj =
187  h_mk_memory_inj __ __ __ __ __ __ __
188
189(** val memory_inj_rect_Type2 :
190    embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
191    __ -> __ -> 'a1) -> 'a1 **)
192let rec memory_inj_rect_Type2 e1 m1 m2 h_mk_memory_inj =
193  h_mk_memory_inj __ __ __ __ __ __ __
194
195(** val memory_inj_rect_Type1 :
196    embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
197    __ -> __ -> 'a1) -> 'a1 **)
198let rec memory_inj_rect_Type1 e1 m1 m2 h_mk_memory_inj =
199  h_mk_memory_inj __ __ __ __ __ __ __
200
201(** val memory_inj_rect_Type0 :
202    embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
203    __ -> __ -> 'a1) -> 'a1 **)
204let rec memory_inj_rect_Type0 e1 m1 m2 h_mk_memory_inj =
205  h_mk_memory_inj __ __ __ __ __ __ __
206
207(** val memory_inj_inv_rect_Type4 :
208    embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
209    __ -> __ -> __ -> 'a1) -> 'a1 **)
210let memory_inj_inv_rect_Type4 x1 x2 x3 h1 =
211  let hcut = memory_inj_rect_Type4 x1 x2 x3 h1 in hcut __
212
213(** val memory_inj_inv_rect_Type3 :
214    embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
215    __ -> __ -> __ -> 'a1) -> 'a1 **)
216let memory_inj_inv_rect_Type3 x1 x2 x3 h1 =
217  let hcut = memory_inj_rect_Type3 x1 x2 x3 h1 in hcut __
218
219(** val memory_inj_inv_rect_Type2 :
220    embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
221    __ -> __ -> __ -> 'a1) -> 'a1 **)
222let memory_inj_inv_rect_Type2 x1 x2 x3 h1 =
223  let hcut = memory_inj_rect_Type2 x1 x2 x3 h1 in hcut __
224
225(** val memory_inj_inv_rect_Type1 :
226    embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
227    __ -> __ -> __ -> 'a1) -> 'a1 **)
228let memory_inj_inv_rect_Type1 x1 x2 x3 h1 =
229  let hcut = memory_inj_rect_Type1 x1 x2 x3 h1 in hcut __
230
231(** val memory_inj_inv_rect_Type0 :
232    embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
233    __ -> __ -> __ -> 'a1) -> 'a1 **)
234let memory_inj_inv_rect_Type0 x1 x2 x3 h1 =
235  let hcut = memory_inj_rect_Type0 x1 x2 x3 h1 in hcut __
236
237(** val memory_inj_jmdiscr :
238    embedding -> GenMem.mem1 -> GenMem.mem1 -> __ **)
239let memory_inj_jmdiscr a1 a2 a3 =
240  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) __
241
242(** val typesize' : Csyntax.type0 -> Nat.nat **)
243let typesize' ty =
244  AST.typesize (Csyntax.typ_of_type ty)
245
Note: See TracBrowser for help on using the repository browser.