source: extracted/rTLabsToRTL.mli @ 2921

Last change on this file since 2921 was 2921, checked in by sacerdot, 7 years ago

Extracted again.

File size: 10.7 KB
Line 
1open Preamble
2
3open BitVectorTrie
4
5open Graphs
6
7open Order
8
9open Registers
10
11open FrontEndVal
12
13open Hide
14
15open ByteValues
16
17open GenMem
18
19open FrontEndMem
20
21open Division
22
23open Z
24
25open BitVectorZ
26
27open Pointers
28
29open Coqlib
30
31open Values
32
33open FrontEndOps
34
35open CostLabel
36
37open Proper
38
39open PositiveMap
40
41open Deqsets
42
43open ErrorMessages
44
45open PreIdentifiers
46
47open Errors
48
49open Extralib
50
51open Lists
52
53open Positive
54
55open Identifiers
56
57open Exp
58
59open Arithmetic
60
61open Vector
62
63open Div_and_mod
64
65open Util
66
67open FoldStuff
68
69open BitVector
70
71open Jmeq
72
73open Russell
74
75open List
76
77open Setoids
78
79open Monad
80
81open Option
82
83open Extranat
84
85open Bool
86
87open Relations
88
89open Nat
90
91open Integers
92
93open Types
94
95open AST
96
97open Hints_declaration
98
99open Core_notation
100
101open Pts
102
103open Logic
104
105open RTLabs_syntax
106
107open String
108
109open Sets
110
111open Listb
112
113open LabelledObjects
114
115open I8051
116
117open BackEndOps
118
119open Joint
120
121open RTL
122
123open Deqsets_extra
124
125open State
126
127open Bind_new
128
129open BindLists
130
131open Blocks
132
133open TranslateUtils
134
135val size_of_sig_type : AST.typ -> Nat.nat
136
137type register_type =
138| Register_int of Registers.register
139| Register_ptr of Registers.register * Registers.register
140
141val register_type_rect_Type4 :
142  (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
143  'a1) -> register_type -> 'a1
144
145val register_type_rect_Type5 :
146  (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
147  'a1) -> register_type -> 'a1
148
149val register_type_rect_Type3 :
150  (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
151  'a1) -> register_type -> 'a1
152
153val register_type_rect_Type2 :
154  (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
155  'a1) -> register_type -> 'a1
156
157val register_type_rect_Type1 :
158  (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
159  'a1) -> register_type -> 'a1
160
161val register_type_rect_Type0 :
162  (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
163  'a1) -> register_type -> 'a1
164
165val register_type_inv_rect_Type4 :
166  register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
167  -> Registers.register -> __ -> 'a1) -> 'a1
168
169val register_type_inv_rect_Type3 :
170  register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
171  -> Registers.register -> __ -> 'a1) -> 'a1
172
173val register_type_inv_rect_Type2 :
174  register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
175  -> Registers.register -> __ -> 'a1) -> 'a1
176
177val register_type_inv_rect_Type1 :
178  register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
179  -> Registers.register -> __ -> 'a1) -> 'a1
180
181val register_type_inv_rect_Type0 :
182  register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
183  -> Registers.register -> __ -> 'a1) -> 'a1
184
185val register_type_discr : register_type -> register_type -> __
186
187val register_type_jmdiscr : register_type -> register_type -> __
188
189type local_env = Registers.register List.list Identifiers.identifier_map
190
191val find_local_env :
192  PreIdentifiers.identifier -> local_env -> Registers.register List.list
193
194val find_local_env_arg :
195  Registers.register -> local_env -> Joint.psd_argument List.list
196
197val m_iter : Monad.monad -> ('a1 -> __) -> Nat.nat -> __ -> __
198
199val fresh_registers :
200  Joint.params -> AST.ident List.list -> Nat.nat -> Registers.register
201  List.list Monad.smax_def__o__monad
202
203val map_list_local_env :
204  Registers.register List.list Identifiers.identifier_map ->
205  (Registers.register, AST.typ) Types.prod List.list -> Registers.register
206  List.list
207
208val initialize_local_env :
209  AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
210  -> local_env Monad.smax_def__o__monad
211
212val initialize_locals_params_ret :
213  AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
214  -> (Registers.register, AST.typ) Types.prod List.list ->
215  (Registers.register, AST.typ) Types.prod Types.option -> local_env
216  Monad.smax_def__o__monad
217
218val make_addr : 'a1 List.list -> ('a1, 'a1) Types.prod
219
220val find_and_addr :
221  PreIdentifiers.identifier -> local_env -> (Registers.register,
222  Registers.register) Types.prod
223
224val find_and_addr_arg :
225  Registers.register -> local_env -> (Joint.psd_argument, Joint.psd_argument)
226  Types.prod
227
228val rtl_args :
229  Registers.register List.list -> local_env -> Joint.psd_argument List.list
230
231val vrsplit :
232  Nat.nat -> Nat.nat -> 'a1 Vector.vector -> 'a1 Vector.vector List.list
233  Types.sig0
234
235val split_into_bytes :
236  AST.intsize -> AST.bvint -> BitVector.byte List.list Types.sig0
237
238val list_inject_All_aux : 'a1 List.list -> 'a1 Types.sig0 List.list
239
240val translate_op_aux :
241  AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
242  Joint.psd_argument List.list -> Joint.psd_argument List.list ->
243  Joint.joint_seq List.list
244
245val translate_op :
246  AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
247  Joint.psd_argument List.list -> Joint.psd_argument List.list ->
248  Joint.joint_seq List.list
249
250val cast_list : 'a1 -> Nat.nat -> 'a1 List.list -> 'a1 List.list
251
252val translate_op_asym_unsigned :
253  AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
254  Joint.psd_argument List.list -> Joint.psd_argument List.list ->
255  Joint.joint_seq List.list
256
257val zero_args : Nat.nat -> Joint.psd_argument List.list Types.sig0
258
259val one_args : Nat.nat -> Joint.psd_argument List.list Types.sig0
260
261val size_of_cst : AST.typ -> FrontEndOps.constant -> Nat.nat
262
263val translate_cst :
264  AST.typ -> AST.ident List.list -> FrontEndOps.constant Types.sig0 ->
265  Registers.register List.list -> (Registers.register, Joint.joint_seq
266  List.list) Bind_new.bind_new
267
268val translate_move :
269  AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
270  List.list -> Joint.joint_seq List.list
271
272val sign_mask :
273  AST.ident List.list -> Registers.register -> Joint.psd_argument ->
274  Joint.joint_seq List.list
275
276val translate_cast_signed :
277  AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
278  -> (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
279
280val translate_fill_with_zero :
281  AST.ident List.list -> Registers.register List.list -> Joint.joint_seq
282  List.list
283
284val last : 'a1 List.list -> 'a1 Types.option
285
286val translate_op_asym_signed :
287  AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
288  Joint.psd_argument List.list -> Joint.psd_argument List.list ->
289  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
290
291val translate_cast :
292  AST.ident List.list -> AST.signedness -> Registers.register List.list ->
293  Registers.register List.list -> (Registers.register, Joint.joint_seq
294  List.list) Bind_new.bind_new
295
296val translate_notint :
297  AST.ident List.list -> Registers.register List.list -> Registers.register
298  List.list -> Joint.joint_seq List.list
299
300val translate_negint :
301  AST.ident List.list -> Registers.register List.list -> Registers.register
302  List.list -> Joint.joint_seq List.list
303
304val translate_notbool :
305  AST.ident List.list -> Registers.register List.list -> Registers.register
306  List.list -> (Registers.register, Joint.joint_seq List.list)
307  Bind_new.bind_new
308
309val translate_op1 :
310  AST.ident List.list -> AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
311  Registers.register List.list -> Registers.register List.list ->
312  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
313
314val translate_mul_i :
315  AST.ident List.list -> Registers.register -> Registers.register -> Nat.nat
316  -> Registers.register List.list -> Joint.psd_argument List.list ->
317  Joint.psd_argument List.list -> Nat.nat -> Nat.nat Types.sig0 ->
318  Joint.joint_seq List.list -> Joint.joint_seq List.list
319
320val translate_mul :
321  AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
322  List.list -> Joint.psd_argument List.list -> (Registers.register,
323  Joint.joint_seq List.list) Bind_new.bind_new
324
325val translate_divumodu8 :
326  AST.ident List.list -> Bool.bool -> Registers.register List.list ->
327  Joint.psd_argument List.list -> Joint.psd_argument List.list ->
328  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
329
330val foldr2 :
331  ('a1 -> 'a2 -> 'a3 -> 'a3) -> 'a3 -> 'a1 List.list -> 'a2 List.list -> 'a3
332
333val translate_ne :
334  AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
335  List.list -> Joint.psd_argument List.list -> (Registers.register,
336  Joint.joint_seq List.list) Bind_new.bind_new
337
338val translate_toggle_bool :
339  AST.ident List.list -> Registers.register List.list -> (Registers.register,
340  Joint.joint_seq List.list) Bind_new.bind_new
341
342val translate_lt_unsigned :
343  AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
344  List.list -> Joint.psd_argument List.list -> (Registers.register,
345  Joint.joint_seq List.list) Bind_new.bind_new
346
347val shift_signed :
348  AST.ident List.list -> Registers.register -> Joint.psd_argument List.list
349  -> (Joint.psd_argument List.list, Joint.joint_seq List.list) Types.prod
350  Types.sig0
351
352val translate_lt_signed :
353  AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
354  List.list -> Joint.psd_argument List.list -> (Registers.register,
355  Joint.joint_seq List.list) Bind_new.bind_new
356
357val translate_lt :
358  Bool.bool -> AST.ident List.list -> Registers.register List.list ->
359  Joint.psd_argument List.list -> Joint.psd_argument List.list ->
360  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
361
362val translate_cmp :
363  Bool.bool -> AST.ident List.list -> Integers.comparison ->
364  Registers.register List.list -> Joint.psd_argument List.list ->
365  Joint.psd_argument List.list -> (Registers.register, Joint.joint_seq)
366  BindLists.bind_list
367
368val translate_op2 :
369  AST.ident List.list -> AST.typ -> AST.typ -> AST.typ ->
370  FrontEndOps.binary_operation -> Registers.register List.list ->
371  Joint.psd_argument List.list -> Joint.psd_argument List.list ->
372  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
373
374val translate_cond :
375  AST.ident List.list -> Registers.register List.list -> Graphs.label ->
376  Blocks.bind_step_block
377
378val translate_load :
379  AST.ident List.list -> Joint.psd_argument List.list -> Registers.register
380  List.list -> (Registers.register, Joint.joint_seq List.list)
381  Bind_new.bind_new
382
383val translate_store :
384  AST.ident List.list -> Joint.psd_argument List.list -> Joint.psd_argument
385  List.list -> (Registers.register, Joint.joint_seq List.list)
386  Bind_new.bind_new
387
388val ensure_bind_step_block :
389  Joint.params -> AST.ident List.list -> (Registers.register, Joint.joint_seq
390  List.list) Bind_new.bind_new -> Blocks.bind_step_block
391
392val translate_statement :
393  AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
394  -> local_env -> RTLabs_syntax.statement -> ((Blocks.bind_step_block,
395  Blocks.bind_fin_block) Types.sum, __) Types.dPair
396
397val translate_internal :
398  AST.ident List.list -> RTLabs_syntax.internal_function ->
399  Joint.joint_closed_internal_function
400
401val rtlabs_to_rtl : RTLabs_syntax.rTLabs_program -> RTL.rtl_program
402
Note: See TracBrowser for help on using the repository browser.