source: extracted/translateUtils.ml @ 2890

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

Extracted again.

File size: 27.8 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
107open State
108
109open Bind_new
110
111open BindLists
112
113open Blocks
114
115open Deqsets_extra
116
117(** val fresh_label :
118    Joint.params -> AST.ident List.list -> Graphs.label
119    Monad.smax_def__o__monad **)
120let fresh_label g_pars globals =
121  Obj.magic (fun def ->
122    let { Types.fst = r; Types.snd = luniverse } =
123      Identifiers.fresh PreIdentifiers.LabelTag def.Joint.joint_if_luniverse
124    in
125    { Types.fst = (Joint.set_luniverse g_pars globals def luniverse);
126    Types.snd = r })
127
128(** val fresh_register :
129    Joint.params -> AST.ident List.list -> Registers.register
130    Monad.smax_def__o__monad **)
131let fresh_register g_pars globals =
132  Obj.magic (fun def ->
133    let { Types.fst = r; Types.snd = runiverse } =
134      Identifiers.fresh PreIdentifiers.RegisterTag
135        def.Joint.joint_if_runiverse
136    in
137    { Types.fst = (Joint.set_runiverse g_pars globals def runiverse);
138    Types.snd = r })
139
140(** val adds_graph_pre :
141    Joint.graph_params -> AST.ident List.list -> (Graphs.label -> 'a1 ->
142    Joint.joint_seq) -> 'a1 List.list -> Graphs.label -> Graphs.label
143    Monad.smax_def__o__monad **)
144let rec adds_graph_pre g_pars globals pre_process insts src =
145  match insts with
146  | List.Nil -> Monad.m_return0 (Monad.smax_def State.state_monad) src
147  | List.Cons (i, rest) ->
148    Monad.m_bind0 (Monad.smax_def State.state_monad)
149      (fresh_label (Joint.graph_params_to_params g_pars) globals) (fun mid ->
150      Monad.m_bind0 (Monad.smax_def State.state_monad)
151        (adds_graph_pre g_pars globals pre_process rest mid) (fun dst ->
152        Monad.m_bind0 (Monad.smax_def State.state_monad)
153          (State.state_update
154            (Joint.add_graph g_pars globals src (Joint.Sequential
155              ((Joint.Step_seq (pre_process dst i)), (Obj.magic mid)))))
156          (fun x -> Monad.m_return0 (Monad.smax_def State.state_monad) dst)))
157
158(** val adds_graph_post :
159    Joint.graph_params -> AST.ident List.list -> Joint.joint_seq List.list ->
160    Graphs.label -> Graphs.label Monad.smax_def__o__monad **)
161let rec adds_graph_post g_pars globals insts dst =
162  match insts with
163  | List.Nil -> Monad.m_return0 (Monad.smax_def State.state_monad) dst
164  | List.Cons (i, rest) ->
165    Monad.m_bind0 (Monad.smax_def State.state_monad)
166      (fresh_label (Joint.graph_params_to_params g_pars) globals) (fun src ->
167      Monad.m_bind0 (Monad.smax_def State.state_monad)
168        (adds_graph_post g_pars globals rest dst) (fun mid ->
169        Monad.m_bind0 (Monad.smax_def State.state_monad)
170          (State.state_update
171            (Joint.add_graph g_pars globals src (Joint.Sequential
172              ((Joint.Step_seq i), mid)))) (fun x ->
173          Monad.m_return0 (Monad.smax_def State.state_monad) src)))
174
175(** val adds_graph :
176    Joint.graph_params -> AST.ident List.list -> Blocks.step_block ->
177    Graphs.label -> Graphs.label -> Joint.joint_internal_function ->
178    Joint.joint_internal_function **)
179let adds_graph g_pars globals insts src dst def =
180  let pref = insts.Types.fst.Types.fst in
181  let op = insts.Types.fst.Types.snd in
182  let post = insts.Types.snd in
183  let { Types.fst = def0; Types.snd = mid } =
184    Obj.magic adds_graph_pre g_pars globals (fun lbl inst -> inst lbl)
185      (Obj.magic pref) src def
186  in
187  let { Types.fst = def1; Types.snd = mid' } =
188    Obj.magic adds_graph_post g_pars globals post dst def0
189  in
190  Joint.add_graph g_pars globals mid (Joint.Sequential ((Obj.magic op mid),
191    mid')) def1
192
193(** val fin_adds_graph :
194    Joint.graph_params -> AST.ident List.list -> Blocks.fin_block ->
195    Graphs.label -> Joint.joint_internal_function ->
196    Joint.joint_internal_function **)
197let fin_adds_graph g_pars globals insts src def =
198  let pref = insts.Types.fst in
199  let last = insts.Types.snd in
200  let { Types.fst = def0; Types.snd = mid } =
201    Obj.magic adds_graph_pre g_pars globals (fun x i -> i) pref src def
202  in
203  Joint.add_graph g_pars globals mid (Joint.Final last) def0
204
205(** val append_seq_list :
206    Joint.params -> AST.ident List.list -> Blocks.bind_step_block ->
207    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new ->
208    Blocks.bind_step_block **)
209let append_seq_list p g bbl bl =
210  Obj.magic
211    (Monad.m_bind3 (Monad.max_def Bind_new.bindNew) (Obj.magic bbl)
212      (fun pref op post ->
213      Monad.m_bind0 (Monad.max_def Bind_new.bindNew) (Obj.magic bl) (fun l ->
214        Monad.m_return0 (Monad.max_def Bind_new.bindNew) { Types.fst =
215          { Types.fst = pref; Types.snd = op }; Types.snd =
216          (List.append post l) })))
217
218(** val b_adds_graph :
219    Joint.graph_params -> AST.ident List.list -> Blocks.bind_step_block ->
220    Graphs.label -> Graphs.label -> Joint.joint_internal_function ->
221    Joint.joint_internal_function **)
222let b_adds_graph g_pars globals insts src dst def =
223  let { Types.fst = def0; Types.snd = stmts } =
224    Obj.magic Bind_new.bcompile
225      (fresh_register (Joint.graph_params_to_params g_pars) globals) insts
226      def
227  in
228  adds_graph g_pars globals stmts src dst def0
229
230(** val b_fin_adds_graph :
231    Joint.graph_params -> AST.ident List.list -> Blocks.bind_fin_block ->
232    Graphs.label -> Joint.joint_internal_function ->
233    Joint.joint_internal_function **)
234let b_fin_adds_graph g_pars globals insts src def =
235  let { Types.fst = def0; Types.snd = stmts } =
236    Obj.magic Bind_new.bcompile
237      (fresh_register (Joint.graph_params_to_params g_pars) globals) insts
238      def
239  in
240  fin_adds_graph g_pars globals stmts src def0
241
242(** val step_registers :
243    Joint.uns_params -> AST.ident List.list -> Joint.joint_step ->
244    Registers.register List.list **)
245let step_registers p globals s =
246  Joint.get_used_registers_from_step p.Joint.u_pars globals p.Joint.functs s
247
248(** val fin_step_registers :
249    Joint.uns_params -> Joint.joint_fin_step -> Registers.register List.list **)
250let fin_step_registers p = function
251| Joint.GOTO x -> List.Nil
252| Joint.RETURN -> List.Nil
253| Joint.TAILCALL (x0, r) -> p.Joint.functs.Joint.f_call_args r
254
255type b_graph_translate_data = { init_ret : __; init_params : __;
256                                init_stack_size : Nat.nat;
257                                added_prologue : Joint.joint_seq List.list;
258                                new_regs : Registers.register List.list;
259                                f_step : (Graphs.label -> Joint.joint_step ->
260                                         Blocks.bind_step_block);
261                                f_fin : (Graphs.label -> Joint.joint_fin_step
262                                        -> Blocks.bind_fin_block) }
263
264(** val b_graph_translate_data_rect_Type4 :
265    Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
266    __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
267    List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
268    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
269    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
270let rec b_graph_translate_data_rect_Type4 src dst globals h_mk_b_graph_translate_data x_21201 =
271  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
272    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
273    f_step = f_step0; f_fin = f_fin0 } = x_21201
274  in
275  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
276    added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
277
278(** val b_graph_translate_data_rect_Type5 :
279    Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
280    __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
281    List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
282    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
283    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
284let rec b_graph_translate_data_rect_Type5 src dst globals h_mk_b_graph_translate_data x_21203 =
285  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
286    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
287    f_step = f_step0; f_fin = f_fin0 } = x_21203
288  in
289  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
290    added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
291
292(** val b_graph_translate_data_rect_Type3 :
293    Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
294    __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
295    List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
296    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
297    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
298let rec b_graph_translate_data_rect_Type3 src dst globals h_mk_b_graph_translate_data x_21205 =
299  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
300    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
301    f_step = f_step0; f_fin = f_fin0 } = x_21205
302  in
303  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
304    added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
305
306(** val b_graph_translate_data_rect_Type2 :
307    Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
308    __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
309    List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
310    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
311    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
312let rec b_graph_translate_data_rect_Type2 src dst globals h_mk_b_graph_translate_data x_21207 =
313  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
314    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
315    f_step = f_step0; f_fin = f_fin0 } = x_21207
316  in
317  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
318    added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
319
320(** val b_graph_translate_data_rect_Type1 :
321    Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
322    __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
323    List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
324    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
325    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
326let rec b_graph_translate_data_rect_Type1 src dst globals h_mk_b_graph_translate_data x_21209 =
327  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
328    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
329    f_step = f_step0; f_fin = f_fin0 } = x_21209
330  in
331  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
332    added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
333
334(** val b_graph_translate_data_rect_Type0 :
335    Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
336    __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
337    List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
338    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
339    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
340let rec b_graph_translate_data_rect_Type0 src dst globals h_mk_b_graph_translate_data x_21211 =
341  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
342    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
343    f_step = f_step0; f_fin = f_fin0 } = x_21211
344  in
345  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
346    added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
347
348(** val init_ret :
349    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
350    b_graph_translate_data -> __ **)
351let rec init_ret src dst globals xxx =
352  xxx.init_ret
353
354(** val init_params :
355    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
356    b_graph_translate_data -> __ **)
357let rec init_params src dst globals xxx =
358  xxx.init_params
359
360(** val init_stack_size :
361    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
362    b_graph_translate_data -> Nat.nat **)
363let rec init_stack_size src dst globals xxx =
364  xxx.init_stack_size
365
366(** val added_prologue :
367    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
368    b_graph_translate_data -> Joint.joint_seq List.list **)
369let rec added_prologue src dst globals xxx =
370  xxx.added_prologue
371
372(** val new_regs :
373    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
374    b_graph_translate_data -> Registers.register List.list **)
375let rec new_regs src dst globals xxx =
376  xxx.new_regs
377
378(** val f_step :
379    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
380    b_graph_translate_data -> Graphs.label -> Joint.joint_step ->
381    Blocks.bind_step_block **)
382let rec f_step src dst globals xxx =
383  xxx.f_step
384
385(** val f_fin :
386    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
387    b_graph_translate_data -> Graphs.label -> Joint.joint_fin_step ->
388    Blocks.bind_fin_block **)
389let rec f_fin src dst globals xxx =
390  xxx.f_fin
391
392(** val b_graph_translate_data_inv_rect_Type4 :
393    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
394    b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
395    List.list -> Registers.register List.list -> (Graphs.label ->
396    Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
397    Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
398    __ -> 'a1) -> 'a1 **)
399let b_graph_translate_data_inv_rect_Type4 x1 x2 x3 hterm h1 =
400  let hcut = b_graph_translate_data_rect_Type4 x1 x2 x3 h1 hterm in hcut __
401
402(** val b_graph_translate_data_inv_rect_Type3 :
403    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
404    b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
405    List.list -> Registers.register List.list -> (Graphs.label ->
406    Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
407    Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
408    __ -> 'a1) -> 'a1 **)
409let b_graph_translate_data_inv_rect_Type3 x1 x2 x3 hterm h1 =
410  let hcut = b_graph_translate_data_rect_Type3 x1 x2 x3 h1 hterm in hcut __
411
412(** val b_graph_translate_data_inv_rect_Type2 :
413    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
414    b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
415    List.list -> Registers.register List.list -> (Graphs.label ->
416    Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
417    Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
418    __ -> 'a1) -> 'a1 **)
419let b_graph_translate_data_inv_rect_Type2 x1 x2 x3 hterm h1 =
420  let hcut = b_graph_translate_data_rect_Type2 x1 x2 x3 h1 hterm in hcut __
421
422(** val b_graph_translate_data_inv_rect_Type1 :
423    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
424    b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
425    List.list -> Registers.register List.list -> (Graphs.label ->
426    Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
427    Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
428    __ -> 'a1) -> 'a1 **)
429let b_graph_translate_data_inv_rect_Type1 x1 x2 x3 hterm h1 =
430  let hcut = b_graph_translate_data_rect_Type1 x1 x2 x3 h1 hterm in hcut __
431
432(** val b_graph_translate_data_inv_rect_Type0 :
433    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
434    b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
435    List.list -> Registers.register List.list -> (Graphs.label ->
436    Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
437    Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
438    __ -> 'a1) -> 'a1 **)
439let b_graph_translate_data_inv_rect_Type0 x1 x2 x3 hterm h1 =
440  let hcut = b_graph_translate_data_rect_Type0 x1 x2 x3 h1 hterm in hcut __
441
442(** val b_graph_translate_data_jmdiscr :
443    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
444    b_graph_translate_data -> b_graph_translate_data -> __ **)
445let b_graph_translate_data_jmdiscr a1 a2 a3 x y =
446  Logic.eq_rect_Type2 x
447    (let { init_ret = a0; init_params = a10; init_stack_size = a20;
448       added_prologue = a30; new_regs = a4; f_step = a5; f_fin = a6 } = x
449     in
450    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __)) y
451
452type bound_b_graph_translate_data =
453  (Registers.register, b_graph_translate_data) Bind_new.bind_new Types.sig0
454
455(** val get_first_costlabel :
456    Joint.params -> AST.ident List.list ->
457    Joint.joint_closed_internal_function -> (CostLabel.costlabel, __)
458    Types.prod **)
459let get_first_costlabel p g def =
460  (match p.Joint.stmt_at g (Types.pi1 def).Joint.joint_if_code
461           (Types.pi1 def).Joint.joint_if_entry with
462   | Types.None -> (fun _ -> assert false (* absurd case *))
463   | Types.Some s ->
464     (match s with
465      | Joint.Sequential (s', nxt) ->
466        (match s' with
467         | Joint.COST_LABEL c ->
468           (fun _ -> { Types.fst = c; Types.snd = nxt })
469         | Joint.CALL (x, x0, x1) ->
470           (fun _ -> assert false (* absurd case *))
471         | Joint.COND (x, x0) -> (fun _ -> assert false (* absurd case *))
472         | Joint.Step_seq x -> (fun _ -> assert false (* absurd case *)))
473      | Joint.Final x -> (fun _ -> assert false (* absurd case *))
474      | Joint.FCOND (x0, x1, x2) -> (fun _ -> assert false (* absurd case *))))
475    __
476
477(** val b_graph_translate_props_rect_Type4 :
478    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
479    b_graph_translate_data -> Joint.joint_closed_internal_function ->
480    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
481    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
482    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
483let rec b_graph_translate_props_rect_Type4 src_g_pars dst_g_pars globals data def_in def_out f_lbls f_regs h_mk_b_graph_translate_props =
484  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
485
486(** val b_graph_translate_props_rect_Type5 :
487    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
488    b_graph_translate_data -> Joint.joint_closed_internal_function ->
489    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
490    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
491    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
492let rec b_graph_translate_props_rect_Type5 src_g_pars dst_g_pars globals data def_in def_out f_lbls f_regs h_mk_b_graph_translate_props =
493  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
494
495(** val b_graph_translate_props_rect_Type3 :
496    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
497    b_graph_translate_data -> Joint.joint_closed_internal_function ->
498    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
499    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
500    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
501let rec b_graph_translate_props_rect_Type3 src_g_pars dst_g_pars globals data def_in def_out f_lbls f_regs h_mk_b_graph_translate_props =
502  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
503
504(** val b_graph_translate_props_rect_Type2 :
505    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
506    b_graph_translate_data -> Joint.joint_closed_internal_function ->
507    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
508    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
509    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
510let rec b_graph_translate_props_rect_Type2 src_g_pars dst_g_pars globals data def_in def_out f_lbls f_regs h_mk_b_graph_translate_props =
511  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
512
513(** val b_graph_translate_props_rect_Type1 :
514    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
515    b_graph_translate_data -> Joint.joint_closed_internal_function ->
516    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
517    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
518    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
519let rec b_graph_translate_props_rect_Type1 src_g_pars dst_g_pars globals data def_in def_out f_lbls f_regs h_mk_b_graph_translate_props =
520  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
521
522(** val b_graph_translate_props_rect_Type0 :
523    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
524    b_graph_translate_data -> Joint.joint_closed_internal_function ->
525    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
526    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
527    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
528let rec b_graph_translate_props_rect_Type0 src_g_pars dst_g_pars globals data def_in def_out f_lbls f_regs h_mk_b_graph_translate_props =
529  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
530
531(** val b_graph_translate_props_inv_rect_Type4 :
532    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
533    b_graph_translate_data -> Joint.joint_closed_internal_function ->
534    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
535    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
536    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
537    'a1 **)
538let b_graph_translate_props_inv_rect_Type4 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
539  let hcut = b_graph_translate_props_rect_Type4 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
540  hcut __
541
542(** val b_graph_translate_props_inv_rect_Type3 :
543    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
544    b_graph_translate_data -> Joint.joint_closed_internal_function ->
545    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
546    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
547    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
548    'a1 **)
549let b_graph_translate_props_inv_rect_Type3 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
550  let hcut = b_graph_translate_props_rect_Type3 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
551  hcut __
552
553(** val b_graph_translate_props_inv_rect_Type2 :
554    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
555    b_graph_translate_data -> Joint.joint_closed_internal_function ->
556    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
557    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
558    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
559    'a1 **)
560let b_graph_translate_props_inv_rect_Type2 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
561  let hcut = b_graph_translate_props_rect_Type2 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
562  hcut __
563
564(** val b_graph_translate_props_inv_rect_Type1 :
565    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
566    b_graph_translate_data -> Joint.joint_closed_internal_function ->
567    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
568    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
569    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
570    'a1 **)
571let b_graph_translate_props_inv_rect_Type1 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
572  let hcut = b_graph_translate_props_rect_Type1 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
573  hcut __
574
575(** val b_graph_translate_props_inv_rect_Type0 :
576    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
577    b_graph_translate_data -> Joint.joint_closed_internal_function ->
578    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
579    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
580    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
581    'a1 **)
582let b_graph_translate_props_inv_rect_Type0 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
583  let hcut = b_graph_translate_props_rect_Type0 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
584  hcut __
585
586(** val b_graph_translate_props_jmdiscr :
587    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
588    b_graph_translate_data -> Joint.joint_closed_internal_function ->
589    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
590    List.list) -> (Graphs.label -> Registers.register List.list) -> __ **)
591let b_graph_translate_props_jmdiscr a1 a2 a3 a4 a5 a6 a7 a8 =
592  Logic.eq_rect_Type2 __
593    (Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __)) __
594
595(** val pair_swap : ('a1, 'a2) Types.prod -> ('a2, 'a1) Types.prod **)
596let pair_swap pr =
597  { Types.fst = pr.Types.snd; Types.snd = pr.Types.fst }
598
599(** val b_graph_translate :
600    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
601    bound_b_graph_translate_data -> Joint.joint_closed_internal_function ->
602    Joint.joint_closed_internal_function Types.sig0 **)
603let b_graph_translate src_g_pars dst_g_pars globals data def =
604  let runiv_data =
605    Obj.magic Bind_new.bcompile
606      (Obj.magic
607        (Relations.compose pair_swap
608          (Identifiers.fresh PreIdentifiers.RegisterTag))) (Types.pi1 data)
609      (Types.pi1 def).Joint.joint_if_runiverse
610  in
611  let runiv = runiv_data.Types.fst in
612  let data0 = runiv_data.Types.snd in
613  let entry = (Types.pi1 def).Joint.joint_if_entry in
614  let init = { Joint.joint_if_luniverse =
615    (Types.pi1 def).Joint.joint_if_luniverse; Joint.joint_if_runiverse =
616    runiv; Joint.joint_if_result = data0.init_ret; Joint.joint_if_params =
617    data0.init_params; Joint.joint_if_stacksize = data0.init_stack_size;
618    Joint.joint_if_local_stacksize =
619    (Types.pi1 def).Joint.joint_if_local_stacksize; Joint.joint_if_code =
620    (Obj.magic
621      (Identifiers.add PreIdentifiers.LabelTag
622        (Identifiers.empty_map PreIdentifiers.LabelTag) (Obj.magic entry)
623        (Joint.Final Joint.RETURN))); Joint.joint_if_entry = entry }
624  in
625  let f = fun lbl stmt def0 ->
626    match stmt with
627    | Joint.Sequential (inst, next) ->
628      b_adds_graph dst_g_pars globals (data0.f_step lbl inst) lbl
629        (Obj.magic next) def0
630    | Joint.Final inst ->
631      b_fin_adds_graph dst_g_pars globals (data0.f_fin lbl inst) lbl def0
632    | Joint.FCOND (x, x0, x1) -> assert false (* absurd case *)
633  in
634  let def_out =
635    Identifiers.foldi PreIdentifiers.LabelTag f
636      (Obj.magic (Types.pi1 def).Joint.joint_if_code) init
637  in
638  let init_c_nxt =
639    get_first_costlabel (Joint.graph_params_to_params src_g_pars) globals def
640  in
641  let def_out_nxt =
642    Obj.magic adds_graph_post dst_g_pars globals data0.added_prologue
643      (Obj.magic init_c_nxt).Types.snd def_out
644  in
645  Joint.add_graph dst_g_pars globals (Obj.magic entry) (Joint.Sequential
646    ((Joint.COST_LABEL init_c_nxt.Types.fst), def_out_nxt.Types.snd))
647    def_out_nxt.Types.fst
648
649(** val b_graph_transform_program :
650    Joint.graph_params -> Joint.graph_params -> (AST.ident List.list ->
651    Joint.joint_closed_internal_function -> bound_b_graph_translate_data) ->
652    Joint.joint_program -> Joint.joint_program **)
653let b_graph_transform_program src dst init p =
654  AST.transform_program p (fun varnames ->
655    AST.transf_fundef (fun def_in ->
656      Types.pi1
657        (b_graph_translate src dst varnames (init varnames def_in) def_in)))
658
659(** val added_registers :
660    Joint.graph_params -> AST.ident List.list ->
661    Joint.joint_internal_function -> (Graphs.label -> Registers.register
662    List.list) -> Registers.register List.list **)
663let added_registers p g def f_regs =
664  let f = fun lbl x acc -> List.append (f_regs lbl) acc in
665  Identifiers.foldi PreIdentifiers.LabelTag f
666    (Obj.magic def.Joint.joint_if_code) List.Nil
667
Note: See TracBrowser for help on using the repository browser.