source: extracted/memoryInjections.ml @ 2731

Last change on this file since 2731 was 2717, checked in by sacerdot, 8 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
RevLine 
[2601]1open Preamble
2
[2717]3open SmallstepExec
[2601]4
[2717]5open Cexec
6
7open Sets
8
9open Listb
10
11open IO
12
13open IOMonad
14
15open Star
16
[2601]17open ClassifyOp
18
[2717]19open Events
20
[2601]21open Smallstep
22
23open Extra_bool
24
[2717]25open Values
26
[2601]27open FrontEndVal
28
29open Hide
30
31open ByteValues
32
[2717]33open Division
34
35open Z
36
37open BitVectorZ
38
39open Pointers
40
[2601]41open GenMem
42
43open FrontEndMem
44
45open Globalenvs
46
47open Csem
48
[2717]49open BitVectorTrie
[2601]50
51open CostLabel
52
[2717]53open Coqlib
54
55open Proper
56
[2601]57open PositiveMap
58
59open Deqsets
60
[2717]61open ErrorMessages
[2601]62
[2717]63open PreIdentifiers
[2601]64
[2717]65open Errors
[2601]66
[2717]67open Extralib
[2601]68
[2717]69open Setoids
[2601]70
[2717]71open Monad
[2601]72
73open Option
74
[2717]75open Lists
[2601]76
77open Positive
78
[2717]79open Identifiers
[2601]80
[2717]81open Exp
[2601]82
[2717]83open Arithmetic
[2601]84
[2717]85open Vector
[2601]86
87open Div_and_mod
88
89open Jmeq
90
91open Russell
92
[2717]93open List
94
[2601]95open Util
96
[2717]97open FoldStuff
98
99open BitVector
100
101open Extranat
102
[2601]103open Bool
104
105open Relations
106
107open Nat
108
[2717]109open Integers
[2601]110
111open Hints_declaration
112
113open Core_notation
114
115open Pts
116
117open Logic
118
119open Types
120
[2717]121open AST
[2601]122
[2717]123open Csyntax
[2601]124
[2717]125open TypeComparison
[2601]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 =
[2649]142  let a = clearme in
[2601]143  (fun clearme0 ->
[2649]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 __))
[2601]148
149type embedding =
[2649]150  Pointers.block -> (Pointers.block, Pointers.offset) Types.prod Types.option
[2601]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
[2649]162  (match e1 pblock0 with
[2601]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.