99 open Hints_declaration
122 | Rtl_stack_address of Registers.register * Registers.register
124 (** val rtl_seq_rect_Type4 :
125 (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
126 let rec rtl_seq_rect_Type4 h_rtl_stack_address = function
127 | Rtl_stack_address (x_18151, x_18150) -> h_rtl_stack_address x_18151 x_18150
129 (** val rtl_seq_rect_Type5 :
130 (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
131 let rec rtl_seq_rect_Type5 h_rtl_stack_address = function
132 | Rtl_stack_address (x_18155, x_18154) -> h_rtl_stack_address x_18155 x_18154
134 (** val rtl_seq_rect_Type3 :
135 (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
136 let rec rtl_seq_rect_Type3 h_rtl_stack_address = function
137 | Rtl_stack_address (x_18159, x_18158) -> h_rtl_stack_address x_18159 x_18158
139 (** val rtl_seq_rect_Type2 :
140 (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
141 let rec rtl_seq_rect_Type2 h_rtl_stack_address = function
142 | Rtl_stack_address (x_18163, x_18162) -> h_rtl_stack_address x_18163 x_18162
144 (** val rtl_seq_rect_Type1 :
145 (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
146 let rec rtl_seq_rect_Type1 h_rtl_stack_address = function
147 | Rtl_stack_address (x_18167, x_18166) -> h_rtl_stack_address x_18167 x_18166
149 (** val rtl_seq_rect_Type0 :
150 (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
151 let rec rtl_seq_rect_Type0 h_rtl_stack_address = function
152 | Rtl_stack_address (x_18171, x_18170) -> h_rtl_stack_address x_18171 x_18170
154 (** val rtl_seq_inv_rect_Type4 :
155 rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1 **)
156 let rtl_seq_inv_rect_Type4 hterm h1 =
157 let hcut = rtl_seq_rect_Type4 h1 hterm in hcut __
159 (** val rtl_seq_inv_rect_Type3 :
160 rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1 **)
161 let rtl_seq_inv_rect_Type3 hterm h1 =
162 let hcut = rtl_seq_rect_Type3 h1 hterm in hcut __
164 (** val rtl_seq_inv_rect_Type2 :
165 rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1 **)
166 let rtl_seq_inv_rect_Type2 hterm h1 =
167 let hcut = rtl_seq_rect_Type2 h1 hterm in hcut __
169 (** val rtl_seq_inv_rect_Type1 :
170 rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1 **)
171 let rtl_seq_inv_rect_Type1 hterm h1 =
172 let hcut = rtl_seq_rect_Type1 h1 hterm in hcut __
174 (** val rtl_seq_inv_rect_Type0 :
175 rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1 **)
176 let rtl_seq_inv_rect_Type0 hterm h1 =
177 let hcut = rtl_seq_rect_Type0 h1 hterm in hcut __
179 (** val rtl_seq_discr : rtl_seq -> rtl_seq -> __ **)
180 let rtl_seq_discr x y =
181 Logic.eq_rect_Type2 x
182 (let Rtl_stack_address (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __))
185 (** val rtl_seq_jmdiscr : rtl_seq -> rtl_seq -> __ **)
186 let rtl_seq_jmdiscr x y =
187 Logic.eq_rect_Type2 x
188 (let Rtl_stack_address (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __))
191 (** val rTL_uns : Joint.unserialized_params **)
193 { Joint.ext_seq_labels = (fun x -> List.Nil); Joint.has_tailcalls =
196 (** val rTL_functs : Joint.get_pseudo_reg_functs **)
198 { Joint.acc_a_regs = (fun r -> List.Cons ((Obj.magic r), List.Nil));
199 Joint.acc_b_regs = (fun r -> List.Cons ((Obj.magic r), List.Nil));
200 Joint.acc_a_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.acc_b_args = (fun a ->
204 match Obj.magic a with
205 | Joint.Reg r -> List.Cons (r, List.Nil)
206 | Joint.Imm x -> List.Nil); Joint.dpl_regs = (fun r -> List.Cons
207 ((Obj.magic r), List.Nil)); Joint.dph_regs = (fun r -> List.Cons
208 ((Obj.magic r), List.Nil)); Joint.dpl_args = (fun a ->
209 match Obj.magic a with
210 | Joint.Reg r -> List.Cons (r, List.Nil)
211 | Joint.Imm x -> List.Nil); Joint.dph_args = (fun a ->
212 match Obj.magic a with
213 | Joint.Reg r -> List.Cons (r, List.Nil)
214 | Joint.Imm x -> List.Nil); Joint.snd_args = (fun a ->
215 match Obj.magic a with
216 | Joint.Reg r -> List.Cons (r, List.Nil)
217 | Joint.Imm x -> List.Nil); Joint.pair_move_regs = (fun x ->
218 List.append (List.Cons ((Obj.magic x).Types.fst, List.Nil))
219 (match (Obj.magic x).Types.snd with
220 | Joint.Reg r -> List.Cons (r, List.Nil)
221 | Joint.Imm x0 -> List.Nil)); Joint.f_call_args = (fun l ->
222 Util.foldl (fun l1 a ->
225 | Joint.Reg r -> List.Cons (r, List.Nil)
226 | Joint.Imm x -> List.Nil)) List.Nil (Obj.magic l));
227 Joint.f_call_dest = (fun x -> Obj.magic x); Joint.ext_seq_regs =
229 let Rtl_stack_address (r1, r2) = Obj.magic ext in
230 List.Cons (r1, (List.Cons (r2, List.Nil)))); Joint.params_regs =
231 (fun x -> Obj.magic x) }
233 (** val rTL : Joint.graph_params **)
235 { Joint.u_pars = rTL_uns; Joint.functs = rTL_functs }
237 type rtl_program = Joint.joint_program
239 (** val dpi1__o__reg_to_rtl_snd_argument__o__inject :
240 (Registers.register, 'a1) Types.dPair -> Joint.psd_argument Types.sig0 **)
241 let dpi1__o__reg_to_rtl_snd_argument__o__inject x2 =
242 Joint.psd_argument_from_reg x2.Types.dpi1
244 (** val eject__o__reg_to_rtl_snd_argument__o__inject :
245 Registers.register Types.sig0 -> Joint.psd_argument Types.sig0 **)
246 let eject__o__reg_to_rtl_snd_argument__o__inject x2 =
247 Joint.psd_argument_from_reg (Types.pi1 x2)
249 (** val reg_to_rtl_snd_argument__o__inject :
250 Registers.register -> Joint.psd_argument Types.sig0 **)
251 let reg_to_rtl_snd_argument__o__inject x1 =
252 Joint.psd_argument_from_reg x1
254 (** val dpi1__o__reg_to_rtl_snd_argument :
255 (Registers.register, 'a1) Types.dPair -> Joint.psd_argument **)
256 let dpi1__o__reg_to_rtl_snd_argument x1 =
257 Joint.psd_argument_from_reg x1.Types.dpi1
259 (** val eject__o__reg_to_rtl_snd_argument :
260 Registers.register Types.sig0 -> Joint.psd_argument **)
261 let eject__o__reg_to_rtl_snd_argument x1 =
262 Joint.psd_argument_from_reg (Types.pi1 x1)
264 (** val dpi1__o__byte_to_rtl_snd_argument__o__inject :
265 (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument Types.sig0 **)
266 let dpi1__o__byte_to_rtl_snd_argument__o__inject x2 =
267 Joint.psd_argument_from_byte x2.Types.dpi1
269 (** val eject__o__byte_to_rtl_snd_argument__o__inject :
270 BitVector.byte Types.sig0 -> Joint.psd_argument Types.sig0 **)
271 let eject__o__byte_to_rtl_snd_argument__o__inject x2 =
272 Joint.psd_argument_from_byte (Types.pi1 x2)
274 (** val byte_to_rtl_snd_argument__o__inject :
275 BitVector.byte -> Joint.psd_argument Types.sig0 **)
276 let byte_to_rtl_snd_argument__o__inject x1 =
277 Joint.psd_argument_from_byte x1
279 (** val dpi1__o__byte_to_rtl_snd_argument :
280 (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument **)
281 let dpi1__o__byte_to_rtl_snd_argument x1 =
282 Joint.psd_argument_from_byte x1.Types.dpi1
284 (** val eject__o__byte_to_rtl_snd_argument :
285 BitVector.byte Types.sig0 -> Joint.psd_argument **)
286 let eject__o__byte_to_rtl_snd_argument x1 =
287 Joint.psd_argument_from_byte (Types.pi1 x1)
289 (** val rTL_premain : rtl_program -> Joint.joint_closed_internal_function **)
291 let l1 = Positive.One in
292 let l2 = Positive.P0 Positive.One in
293 let l3 = Positive.P1 Positive.One in
294 let rs = List.Cons (Positive.One, (List.Cons ((Positive.P0 Positive.One),
295 (List.Cons ((Positive.P1 Positive.One), (List.Cons ((Positive.P0
296 (Positive.P0 Positive.One)), List.Nil)))))))
298 let res = { Joint.joint_if_luniverse = (Positive.P0 (Positive.P0
299 Positive.One)); Joint.joint_if_runiverse = (Positive.P1 (Positive.P0
300 Positive.One)); Joint.joint_if_result = (Obj.magic List.Nil);
301 Joint.joint_if_params = (Obj.magic rs); Joint.joint_if_stacksize = Nat.O;
302 Joint.joint_if_local_stacksize = Nat.O; Joint.joint_if_code =
303 (Obj.magic (Identifiers.empty_map PreIdentifiers.LabelTag));
304 Joint.joint_if_entry = (Obj.magic l1) }
308 (Joint.prog_names (Joint.graph_params_to_params rTL) p) l1
309 (Joint.Sequential ((Joint.COST_LABEL p.Joint.init_cost_label),
314 (Joint.prog_names (Joint.graph_params_to_params rTL) p) l2
315 (Joint.Sequential ((Joint.CALL ((Types.Inl
316 p.Joint.joint_prog.AST.prog_main), (Obj.magic List.Nil),
317 (Obj.magic rs))), (Obj.magic l3))) res0
321 (Joint.prog_names (Joint.graph_params_to_params rTL) p) l3 (Joint.Final
322 (Joint.GOTO l3)) res1