source: extracted/rTL.ml @ 2890

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

Extracted again.

File size: 7.6 KB
Line 
1open Preamble
2
3open String
4
5open Sets
6
7open Listb
8
9open LabelledObjects
10
11open BitVectorTrie
12
13open Graphs
14
15open I8051
16
17open Order
18
19open Registers
20
21open CostLabel
22
23open Hide
24
25open Proper
26
27open PositiveMap
28
29open Deqsets
30
31open ErrorMessages
32
33open PreIdentifiers
34
35open Errors
36
37open Extralib
38
39open Lists
40
41open Identifiers
42
43open Integers
44
45open AST
46
47open Division
48
49open Exp
50
51open Arithmetic
52
53open Setoids
54
55open Monad
56
57open Option
58
59open Extranat
60
61open Vector
62
63open Div_and_mod
64
65open Jmeq
66
67open Russell
68
69open List
70
71open Util
72
73open FoldStuff
74
75open BitVector
76
77open Types
78
79open Bool
80
81open Relations
82
83open Nat
84
85open Hints_declaration
86
87open Core_notation
88
89open Pts
90
91open Logic
92
93open Positive
94
95open Z
96
97open BitVectorZ
98
99open Pointers
100
101open ByteValues
102
103open BackEndOps
104
105open Joint
106
107type rtl_seq =
108| Rtl_stack_address of Registers.register * Registers.register
109
110(** val rtl_seq_rect_Type4 :
111    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
112let rec rtl_seq_rect_Type4 h_rtl_stack_address = function
113| Rtl_stack_address (x_21075, x_21074) -> h_rtl_stack_address x_21075 x_21074
114
115(** val rtl_seq_rect_Type5 :
116    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
117let rec rtl_seq_rect_Type5 h_rtl_stack_address = function
118| Rtl_stack_address (x_21079, x_21078) -> h_rtl_stack_address x_21079 x_21078
119
120(** val rtl_seq_rect_Type3 :
121    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
122let rec rtl_seq_rect_Type3 h_rtl_stack_address = function
123| Rtl_stack_address (x_21083, x_21082) -> h_rtl_stack_address x_21083 x_21082
124
125(** val rtl_seq_rect_Type2 :
126    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
127let rec rtl_seq_rect_Type2 h_rtl_stack_address = function
128| Rtl_stack_address (x_21087, x_21086) -> h_rtl_stack_address x_21087 x_21086
129
130(** val rtl_seq_rect_Type1 :
131    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
132let rec rtl_seq_rect_Type1 h_rtl_stack_address = function
133| Rtl_stack_address (x_21091, x_21090) -> h_rtl_stack_address x_21091 x_21090
134
135(** val rtl_seq_rect_Type0 :
136    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
137let rec rtl_seq_rect_Type0 h_rtl_stack_address = function
138| Rtl_stack_address (x_21095, x_21094) -> h_rtl_stack_address x_21095 x_21094
139
140(** val rtl_seq_inv_rect_Type4 :
141    rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1 **)
142let rtl_seq_inv_rect_Type4 hterm h1 =
143  let hcut = rtl_seq_rect_Type4 h1 hterm in hcut __
144
145(** val rtl_seq_inv_rect_Type3 :
146    rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1 **)
147let rtl_seq_inv_rect_Type3 hterm h1 =
148  let hcut = rtl_seq_rect_Type3 h1 hterm in hcut __
149
150(** val rtl_seq_inv_rect_Type2 :
151    rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1 **)
152let rtl_seq_inv_rect_Type2 hterm h1 =
153  let hcut = rtl_seq_rect_Type2 h1 hterm in hcut __
154
155(** val rtl_seq_inv_rect_Type1 :
156    rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1 **)
157let rtl_seq_inv_rect_Type1 hterm h1 =
158  let hcut = rtl_seq_rect_Type1 h1 hterm in hcut __
159
160(** val rtl_seq_inv_rect_Type0 :
161    rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1 **)
162let rtl_seq_inv_rect_Type0 hterm h1 =
163  let hcut = rtl_seq_rect_Type0 h1 hterm in hcut __
164
165(** val rtl_seq_discr : rtl_seq -> rtl_seq -> __ **)
166let rtl_seq_discr x y =
167  Logic.eq_rect_Type2 x
168    (let Rtl_stack_address (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __))
169    y
170
171(** val rtl_seq_jmdiscr : rtl_seq -> rtl_seq -> __ **)
172let rtl_seq_jmdiscr x y =
173  Logic.eq_rect_Type2 x
174    (let Rtl_stack_address (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __))
175    y
176
177(** val rTL_uns : Joint.unserialized_params **)
178let rTL_uns =
179  { Joint.ext_seq_labels = (fun x -> List.Nil); Joint.has_tailcalls =
180    Bool.False }
181
182(** val rTL_functs : Joint.get_pseudo_reg_functs **)
183let rTL_functs =
184  { Joint.acc_a_regs = (fun r -> List.Cons ((Obj.magic r), List.Nil));
185    Joint.acc_b_regs = (fun r -> List.Cons ((Obj.magic r), List.Nil));
186    Joint.acc_a_args = (fun a ->
187    match Obj.magic a with
188    | Joint.Reg r -> List.Cons (r, List.Nil)
189    | Joint.Imm x -> List.Nil); Joint.acc_b_args = (fun a ->
190    match Obj.magic a with
191    | Joint.Reg r -> List.Cons (r, List.Nil)
192    | Joint.Imm x -> List.Nil); Joint.dpl_regs = (fun r -> List.Cons
193    ((Obj.magic r), List.Nil)); Joint.dph_regs = (fun r -> List.Cons
194    ((Obj.magic r), List.Nil)); Joint.dpl_args = (fun a ->
195    match Obj.magic a with
196    | Joint.Reg r -> List.Cons (r, List.Nil)
197    | Joint.Imm x -> List.Nil); Joint.dph_args = (fun a ->
198    match Obj.magic a with
199    | Joint.Reg r -> List.Cons (r, List.Nil)
200    | Joint.Imm x -> List.Nil); Joint.snd_args = (fun a ->
201    match Obj.magic a with
202    | Joint.Reg r -> List.Cons (r, List.Nil)
203    | Joint.Imm x -> List.Nil); Joint.pair_move_regs = (fun x ->
204    List.append (List.Cons ((Obj.magic x).Types.fst, List.Nil))
205      (match (Obj.magic x).Types.snd with
206       | Joint.Reg r -> List.Cons (r, List.Nil)
207       | Joint.Imm x0 -> List.Nil)); Joint.f_call_args = (fun l ->
208    Util.foldl (fun l1 a ->
209      List.append l1
210        (match a with
211         | Joint.Reg r -> List.Cons (r, List.Nil)
212         | Joint.Imm x -> List.Nil)) List.Nil (Obj.magic l));
213    Joint.f_call_dest = (fun x -> Obj.magic x); Joint.ext_seq_regs =
214    (fun ext ->
215    let Rtl_stack_address (r1, r2) = Obj.magic ext in
216    List.Cons (r1, (List.Cons (r2, List.Nil)))); Joint.params_regs =
217    (fun x -> Obj.magic x) }
218
219(** val rTL : Joint.graph_params **)
220let rTL =
221  { Joint.u_pars = rTL_uns; Joint.functs = rTL_functs }
222
223type rtl_program = Joint.joint_program
224
225(** val dpi1__o__reg_to_rtl_snd_argument__o__inject :
226    (Registers.register, 'a1) Types.dPair -> Joint.psd_argument Types.sig0 **)
227let dpi1__o__reg_to_rtl_snd_argument__o__inject x2 =
228  Joint.psd_argument_from_reg x2.Types.dpi1
229
230(** val eject__o__reg_to_rtl_snd_argument__o__inject :
231    Registers.register Types.sig0 -> Joint.psd_argument Types.sig0 **)
232let eject__o__reg_to_rtl_snd_argument__o__inject x2 =
233  Joint.psd_argument_from_reg (Types.pi1 x2)
234
235(** val reg_to_rtl_snd_argument__o__inject :
236    Registers.register -> Joint.psd_argument Types.sig0 **)
237let reg_to_rtl_snd_argument__o__inject x1 =
238  Joint.psd_argument_from_reg x1
239
240(** val dpi1__o__reg_to_rtl_snd_argument :
241    (Registers.register, 'a1) Types.dPair -> Joint.psd_argument **)
242let dpi1__o__reg_to_rtl_snd_argument x1 =
243  Joint.psd_argument_from_reg x1.Types.dpi1
244
245(** val eject__o__reg_to_rtl_snd_argument :
246    Registers.register Types.sig0 -> Joint.psd_argument **)
247let eject__o__reg_to_rtl_snd_argument x1 =
248  Joint.psd_argument_from_reg (Types.pi1 x1)
249
250(** val dpi1__o__byte_to_rtl_snd_argument__o__inject :
251    (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument Types.sig0 **)
252let dpi1__o__byte_to_rtl_snd_argument__o__inject x2 =
253  Joint.psd_argument_from_byte x2.Types.dpi1
254
255(** val eject__o__byte_to_rtl_snd_argument__o__inject :
256    BitVector.byte Types.sig0 -> Joint.psd_argument Types.sig0 **)
257let eject__o__byte_to_rtl_snd_argument__o__inject x2 =
258  Joint.psd_argument_from_byte (Types.pi1 x2)
259
260(** val byte_to_rtl_snd_argument__o__inject :
261    BitVector.byte -> Joint.psd_argument Types.sig0 **)
262let byte_to_rtl_snd_argument__o__inject x1 =
263  Joint.psd_argument_from_byte x1
264
265(** val dpi1__o__byte_to_rtl_snd_argument :
266    (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument **)
267let dpi1__o__byte_to_rtl_snd_argument x1 =
268  Joint.psd_argument_from_byte x1.Types.dpi1
269
270(** val eject__o__byte_to_rtl_snd_argument :
271    BitVector.byte Types.sig0 -> Joint.psd_argument **)
272let eject__o__byte_to_rtl_snd_argument x1 =
273  Joint.psd_argument_from_byte (Types.pi1 x1)
274
Note: See TracBrowser for help on using the repository browser.