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