source: extracted/translateUtils.ml @ 2974

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

New extraction.

File size: 28.9 KB
Line 
1open Preamble
2
3open Extra_bool
4
5open Coqlib
6
7open Values
8
9open FrontEndVal
10
11open GenMem
12
13open FrontEndMem
14
15open Globalenvs
16
17open String
18
19open Sets
20
21open Listb
22
23open LabelledObjects
24
25open BitVectorTrie
26
27open Graphs
28
29open I8051
30
31open Order
32
33open Registers
34
35open CostLabel
36
37open Hide
38
39open Proper
40
41open PositiveMap
42
43open Deqsets
44
45open ErrorMessages
46
47open PreIdentifiers
48
49open Errors
50
51open Extralib
52
53open Lists
54
55open Identifiers
56
57open Integers
58
59open AST
60
61open Division
62
63open Exp
64
65open Arithmetic
66
67open Setoids
68
69open Monad
70
71open Option
72
73open Extranat
74
75open Vector
76
77open Div_and_mod
78
79open Jmeq
80
81open Russell
82
83open List
84
85open Util
86
87open FoldStuff
88
89open BitVector
90
91open Types
92
93open Bool
94
95open Relations
96
97open Nat
98
99open Hints_declaration
100
101open Core_notation
102
103open Pts
104
105open Logic
106
107open Positive
108
109open Z
110
111open BitVectorZ
112
113open Pointers
114
115open ByteValues
116
117open BackEndOps
118
119open Joint
120
121open State
122
123open Bind_new
124
125open BindLists
126
127open Blocks
128
129open Deqsets_extra
130
131(** val fresh_label :
132    Joint.params -> AST.ident List.list -> Graphs.label
133    Monad.smax_def__o__monad **)
134let fresh_label g_pars globals =
135  Obj.magic (fun def ->
136    let { Types.fst = r; Types.snd = luniverse } =
137      Identifiers.fresh PreIdentifiers.LabelTag def.Joint.joint_if_luniverse
138    in
139    { Types.fst = (Joint.set_luniverse g_pars globals def luniverse);
140    Types.snd = r })
141
142(** val fresh_register :
143    Joint.params -> AST.ident List.list -> Registers.register
144    Monad.smax_def__o__monad **)
145let fresh_register g_pars globals =
146  Obj.magic (fun def ->
147    let { Types.fst = r; Types.snd = runiverse } =
148      Identifiers.fresh PreIdentifiers.RegisterTag
149        def.Joint.joint_if_runiverse
150    in
151    { Types.fst = (Joint.set_runiverse g_pars globals def runiverse);
152    Types.snd = r })
153
154(** val adds_graph_pre :
155    Joint.graph_params -> AST.ident List.list -> (Graphs.label -> 'a1 ->
156    Joint.joint_seq) -> 'a1 List.list -> Graphs.label -> Graphs.label
157    Monad.smax_def__o__monad **)
158let rec adds_graph_pre g_pars globals pre_process insts src =
159  match insts with
160  | List.Nil -> Monad.m_return0 (Monad.smax_def State.state_monad) src
161  | List.Cons (i, rest) ->
162    Monad.m_bind0 (Monad.smax_def State.state_monad)
163      (fresh_label (Joint.graph_params_to_params g_pars) globals) (fun mid ->
164      Monad.m_bind0 (Monad.smax_def State.state_monad)
165        (adds_graph_pre g_pars globals pre_process rest mid) (fun dst ->
166        Monad.m_bind0 (Monad.smax_def State.state_monad)
167          (State.state_update
168            (Joint.add_graph g_pars globals src (Joint.Sequential
169              ((Joint.Step_seq (pre_process dst i)), (Obj.magic mid)))))
170          (fun x -> Monad.m_return0 (Monad.smax_def State.state_monad) dst)))
171
172(** val adds_graph_post :
173    Joint.graph_params -> AST.ident List.list -> Joint.joint_seq List.list ->
174    Graphs.label -> Graphs.label Monad.smax_def__o__monad **)
175let rec adds_graph_post g_pars globals insts dst =
176  match insts with
177  | List.Nil -> Monad.m_return0 (Monad.smax_def State.state_monad) dst
178  | List.Cons (i, rest) ->
179    Monad.m_bind0 (Monad.smax_def State.state_monad)
180      (fresh_label (Joint.graph_params_to_params g_pars) globals) (fun src ->
181      Monad.m_bind0 (Monad.smax_def State.state_monad)
182        (adds_graph_post g_pars globals rest dst) (fun mid ->
183        Monad.m_bind0 (Monad.smax_def State.state_monad)
184          (State.state_update
185            (Joint.add_graph g_pars globals src (Joint.Sequential
186              ((Joint.Step_seq i), mid)))) (fun x ->
187          Monad.m_return0 (Monad.smax_def State.state_monad) src)))
188
189(** val adds_graph :
190    Joint.graph_params -> AST.ident List.list -> Blocks.step_block ->
191    Graphs.label -> Graphs.label -> Joint.joint_internal_function ->
192    Joint.joint_internal_function **)
193let adds_graph g_pars globals insts src dst def =
194  let pref = insts.Types.fst.Types.fst in
195  let op = insts.Types.fst.Types.snd in
196  let post = insts.Types.snd in
197  let { Types.fst = def0; Types.snd = mid } =
198    Obj.magic adds_graph_pre g_pars globals (fun lbl inst -> inst lbl)
199      (Obj.magic pref) src def
200  in
201  let { Types.fst = def1; Types.snd = mid' } =
202    Obj.magic adds_graph_post g_pars globals post dst def0
203  in
204  Joint.add_graph g_pars globals mid (Joint.Sequential ((Obj.magic op mid),
205    mid')) def1
206
207(** val fin_adds_graph :
208    Joint.graph_params -> AST.ident List.list -> Blocks.fin_block ->
209    Graphs.label -> Joint.joint_internal_function ->
210    Joint.joint_internal_function **)
211let fin_adds_graph g_pars globals insts src def =
212  let pref = insts.Types.fst in
213  let last = insts.Types.snd in
214  let { Types.fst = def0; Types.snd = mid } =
215    Obj.magic adds_graph_pre g_pars globals (fun x i -> i) pref src def
216  in
217  Joint.add_graph g_pars globals mid (Joint.Final last) def0
218
219(** val b_adds_graph :
220    Joint.graph_params -> AST.ident List.list -> Blocks.bind_step_block ->
221    Graphs.label -> Graphs.label -> Joint.joint_internal_function ->
222    Joint.joint_internal_function **)
223let b_adds_graph g_pars globals insts src dst def =
224  let { Types.fst = def0; Types.snd = stmts } =
225    Obj.magic Bind_new.bcompile
226      (fresh_register (Joint.graph_params_to_params g_pars) globals) insts
227      def
228  in
229  adds_graph g_pars globals stmts src dst def0
230
231(** val b_fin_adds_graph :
232    Joint.graph_params -> AST.ident List.list -> Blocks.bind_fin_block ->
233    Graphs.label -> Joint.joint_internal_function ->
234    Joint.joint_internal_function **)
235let b_fin_adds_graph g_pars globals insts src def =
236  let { Types.fst = def0; Types.snd = stmts } =
237    Obj.magic Bind_new.bcompile
238      (fresh_register (Joint.graph_params_to_params g_pars) globals) insts
239      def
240  in
241  fin_adds_graph g_pars globals stmts src def0
242
243(** val step_registers :
244    Joint.uns_params -> AST.ident List.list -> Joint.joint_step ->
245    Registers.register List.list **)
246let step_registers p globals s =
247  Joint.get_used_registers_from_step p.Joint.u_pars globals p.Joint.functs s
248
249(** val fin_step_registers :
250    Joint.uns_params -> Joint.joint_fin_step -> Registers.register List.list **)
251let fin_step_registers p = function
252| Joint.GOTO x -> List.Nil
253| Joint.RETURN -> List.Nil
254| Joint.TAILCALL (x0, r) -> p.Joint.functs.Joint.f_call_args r
255
256type b_graph_translate_data = { init_ret : __; init_params : __;
257                                init_stack_size : Nat.nat;
258                                added_prologue : Joint.joint_seq List.list;
259                                new_regs : Registers.register List.list;
260                                f_step : (Graphs.label -> Joint.joint_step ->
261                                         Blocks.bind_step_block);
262                                f_fin : (Graphs.label -> Joint.joint_fin_step
263                                        -> Blocks.bind_fin_block) }
264
265(** val b_graph_translate_data_rect_Type4 :
266    Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
267    __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
268    List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
269    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
270    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
271let rec b_graph_translate_data_rect_Type4 src dst globals h_mk_b_graph_translate_data x_3 =
272  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
273    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
274    f_step = f_step0; f_fin = f_fin0 } = x_3
275  in
276  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
277    added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
278
279(** val b_graph_translate_data_rect_Type5 :
280    Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
281    __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
282    List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
283    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
284    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
285let rec b_graph_translate_data_rect_Type5 src dst globals h_mk_b_graph_translate_data x_5 =
286  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
287    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
288    f_step = f_step0; f_fin = f_fin0 } = x_5
289  in
290  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
291    added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
292
293(** val b_graph_translate_data_rect_Type3 :
294    Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
295    __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
296    List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
297    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
298    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
299let rec b_graph_translate_data_rect_Type3 src dst globals h_mk_b_graph_translate_data x_7 =
300  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
301    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
302    f_step = f_step0; f_fin = f_fin0 } = x_7
303  in
304  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
305    added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
306
307(** val b_graph_translate_data_rect_Type2 :
308    Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
309    __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
310    List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
311    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
312    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
313let rec b_graph_translate_data_rect_Type2 src dst globals h_mk_b_graph_translate_data x_9 =
314  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
315    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
316    f_step = f_step0; f_fin = f_fin0 } = x_9
317  in
318  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
319    added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
320
321(** val b_graph_translate_data_rect_Type1 :
322    Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
323    __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
324    List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
325    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
326    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
327let rec b_graph_translate_data_rect_Type1 src dst globals h_mk_b_graph_translate_data x_11 =
328  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
329    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
330    f_step = f_step0; f_fin = f_fin0 } = x_11
331  in
332  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
333    added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
334
335(** val b_graph_translate_data_rect_Type0 :
336    Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
337    __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
338    List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
339    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
340    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
341let rec b_graph_translate_data_rect_Type0 src dst globals h_mk_b_graph_translate_data x_13 =
342  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
343    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
344    f_step = f_step0; f_fin = f_fin0 } = x_13
345  in
346  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
347    added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
348
349(** val init_ret :
350    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
351    b_graph_translate_data -> __ **)
352let rec init_ret src dst globals xxx =
353  xxx.init_ret
354
355(** val init_params :
356    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
357    b_graph_translate_data -> __ **)
358let rec init_params src dst globals xxx =
359  xxx.init_params
360
361(** val init_stack_size :
362    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
363    b_graph_translate_data -> Nat.nat **)
364let rec init_stack_size src dst globals xxx =
365  xxx.init_stack_size
366
367(** val added_prologue :
368    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
369    b_graph_translate_data -> Joint.joint_seq List.list **)
370let rec added_prologue src dst globals xxx =
371  xxx.added_prologue
372
373(** val new_regs :
374    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
375    b_graph_translate_data -> Registers.register List.list **)
376let rec new_regs src dst globals xxx =
377  xxx.new_regs
378
379(** val f_step :
380    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
381    b_graph_translate_data -> Graphs.label -> Joint.joint_step ->
382    Blocks.bind_step_block **)
383let rec f_step src dst globals xxx =
384  xxx.f_step
385
386(** val f_fin :
387    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
388    b_graph_translate_data -> Graphs.label -> Joint.joint_fin_step ->
389    Blocks.bind_fin_block **)
390let rec f_fin src dst globals xxx =
391  xxx.f_fin
392
393(** val b_graph_translate_data_inv_rect_Type4 :
394    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
395    b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
396    List.list -> Registers.register List.list -> (Graphs.label ->
397    Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
398    Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
399    __ -> 'a1) -> 'a1 **)
400let b_graph_translate_data_inv_rect_Type4 x1 x2 x3 hterm h1 =
401  let hcut = b_graph_translate_data_rect_Type4 x1 x2 x3 h1 hterm in hcut __
402
403(** val b_graph_translate_data_inv_rect_Type3 :
404    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
405    b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
406    List.list -> Registers.register List.list -> (Graphs.label ->
407    Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
408    Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
409    __ -> 'a1) -> 'a1 **)
410let b_graph_translate_data_inv_rect_Type3 x1 x2 x3 hterm h1 =
411  let hcut = b_graph_translate_data_rect_Type3 x1 x2 x3 h1 hterm in hcut __
412
413(** val b_graph_translate_data_inv_rect_Type2 :
414    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
415    b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
416    List.list -> Registers.register List.list -> (Graphs.label ->
417    Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
418    Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
419    __ -> 'a1) -> 'a1 **)
420let b_graph_translate_data_inv_rect_Type2 x1 x2 x3 hterm h1 =
421  let hcut = b_graph_translate_data_rect_Type2 x1 x2 x3 h1 hterm in hcut __
422
423(** val b_graph_translate_data_inv_rect_Type1 :
424    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
425    b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
426    List.list -> Registers.register List.list -> (Graphs.label ->
427    Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
428    Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
429    __ -> 'a1) -> 'a1 **)
430let b_graph_translate_data_inv_rect_Type1 x1 x2 x3 hterm h1 =
431  let hcut = b_graph_translate_data_rect_Type1 x1 x2 x3 h1 hterm in hcut __
432
433(** val b_graph_translate_data_inv_rect_Type0 :
434    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
435    b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
436    List.list -> Registers.register List.list -> (Graphs.label ->
437    Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
438    Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
439    __ -> 'a1) -> 'a1 **)
440let b_graph_translate_data_inv_rect_Type0 x1 x2 x3 hterm h1 =
441  let hcut = b_graph_translate_data_rect_Type0 x1 x2 x3 h1 hterm in hcut __
442
443(** val b_graph_translate_data_jmdiscr :
444    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
445    b_graph_translate_data -> b_graph_translate_data -> __ **)
446let b_graph_translate_data_jmdiscr a1 a2 a3 x y =
447  Logic.eq_rect_Type2 x
448    (let { init_ret = a0; init_params = a10; init_stack_size = a20;
449       added_prologue = a30; new_regs = a4; f_step = a5; f_fin = a6 } = x
450     in
451    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __)) y
452
453type bound_b_graph_translate_data =
454  (Registers.register, b_graph_translate_data) Bind_new.bind_new Types.sig0
455
456(** val get_first_costlabel :
457    Joint.params -> AST.ident List.list ->
458    Joint.joint_closed_internal_function -> CostLabel.costlabel **)
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 -> (fun _ -> c)
468         | Joint.CALL (x, x0, x1) ->
469           (fun _ -> assert false (* absurd case *))
470         | Joint.COND (x, x0) -> (fun _ -> assert false (* absurd case *))
471         | Joint.Step_seq x -> (fun _ -> assert false (* absurd case *)))
472      | Joint.Final x -> (fun _ -> assert false (* absurd case *))
473      | Joint.FCOND (x0, x1, x2) -> (fun _ -> assert false (* absurd case *))))
474    __
475
476(** val not_emptyb : 'a1 List.list -> Bool.bool **)
477let not_emptyb = function
478| List.Nil -> Bool.False
479| List.Cons (x, x0) -> Bool.True
480
481(** val b_graph_translate_props_rect_Type4 :
482    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
483    b_graph_translate_data -> Joint.joint_closed_internal_function ->
484    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
485    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
486    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
487let 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 =
488  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
489
490(** val b_graph_translate_props_rect_Type5 :
491    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
492    b_graph_translate_data -> Joint.joint_closed_internal_function ->
493    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
494    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
495    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
496let 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 =
497  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
498
499(** val b_graph_translate_props_rect_Type3 :
500    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
501    b_graph_translate_data -> Joint.joint_closed_internal_function ->
502    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
503    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
504    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
505let 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 =
506  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
507
508(** val b_graph_translate_props_rect_Type2 :
509    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
510    b_graph_translate_data -> Joint.joint_closed_internal_function ->
511    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
512    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
513    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
514let 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 =
515  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
516
517(** val b_graph_translate_props_rect_Type1 :
518    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
519    b_graph_translate_data -> Joint.joint_closed_internal_function ->
520    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
521    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
522    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
523let 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 =
524  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
525
526(** val b_graph_translate_props_rect_Type0 :
527    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
528    b_graph_translate_data -> Joint.joint_closed_internal_function ->
529    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
530    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
531    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
532let 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 =
533  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
534
535(** val b_graph_translate_props_inv_rect_Type4 :
536    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
537    b_graph_translate_data -> Joint.joint_closed_internal_function ->
538    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
539    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
540    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
541    'a1 **)
542let b_graph_translate_props_inv_rect_Type4 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
543  let hcut = b_graph_translate_props_rect_Type4 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
544  hcut __
545
546(** val b_graph_translate_props_inv_rect_Type3 :
547    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
548    b_graph_translate_data -> Joint.joint_closed_internal_function ->
549    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
550    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
551    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
552    'a1 **)
553let b_graph_translate_props_inv_rect_Type3 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
554  let hcut = b_graph_translate_props_rect_Type3 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
555  hcut __
556
557(** val b_graph_translate_props_inv_rect_Type2 :
558    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
559    b_graph_translate_data -> Joint.joint_closed_internal_function ->
560    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
561    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
562    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
563    'a1 **)
564let b_graph_translate_props_inv_rect_Type2 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
565  let hcut = b_graph_translate_props_rect_Type2 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
566  hcut __
567
568(** val b_graph_translate_props_inv_rect_Type1 :
569    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
570    b_graph_translate_data -> Joint.joint_closed_internal_function ->
571    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
572    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
573    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
574    'a1 **)
575let b_graph_translate_props_inv_rect_Type1 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
576  let hcut = b_graph_translate_props_rect_Type1 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
577  hcut __
578
579(** val b_graph_translate_props_inv_rect_Type0 :
580    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
581    b_graph_translate_data -> Joint.joint_closed_internal_function ->
582    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
583    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
584    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
585    'a1 **)
586let b_graph_translate_props_inv_rect_Type0 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
587  let hcut = b_graph_translate_props_rect_Type0 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
588  hcut __
589
590(** val b_graph_translate_props_jmdiscr :
591    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
592    b_graph_translate_data -> Joint.joint_closed_internal_function ->
593    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
594    List.list) -> (Graphs.label -> Registers.register List.list) -> __ **)
595let b_graph_translate_props_jmdiscr a1 a2 a3 a4 a5 a6 a7 a8 =
596  Logic.eq_rect_Type2 __
597    (Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __)) __
598
599(** val pair_swap : ('a1, 'a2) Types.prod -> ('a2, 'a1) Types.prod **)
600let pair_swap pr =
601  { Types.fst = pr.Types.snd; Types.snd = pr.Types.fst }
602
603(** val set_entry :
604    AST.ident List.list -> Joint.params -> Joint.joint_internal_function ->
605    __ -> Joint.joint_internal_function **)
606let set_entry globals pars int_fun entry =
607  { Joint.joint_if_luniverse = int_fun.Joint.joint_if_luniverse;
608    Joint.joint_if_runiverse = int_fun.Joint.joint_if_runiverse;
609    Joint.joint_if_result = int_fun.Joint.joint_if_result;
610    Joint.joint_if_params = int_fun.Joint.joint_if_params;
611    Joint.joint_if_stacksize = int_fun.Joint.joint_if_stacksize;
612    Joint.joint_if_local_stacksize = int_fun.Joint.joint_if_local_stacksize;
613    Joint.joint_if_code = int_fun.Joint.joint_if_code; Joint.joint_if_entry =
614    entry }
615
616(** val b_graph_translate :
617    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
618    bound_b_graph_translate_data -> Joint.joint_closed_internal_function ->
619    Joint.joint_closed_internal_function Types.sig0 **)
620let b_graph_translate src_g_pars dst_g_pars globals data def =
621  let runiv_data =
622    Obj.magic Bind_new.bcompile
623      (Obj.magic
624        (Relations.compose pair_swap
625          (Identifiers.fresh PreIdentifiers.RegisterTag))) (Types.pi1 data)
626      (Types.pi1 def).Joint.joint_if_runiverse
627  in
628  let runiv = runiv_data.Types.fst in
629  let data0 = runiv_data.Types.snd in
630  let entry = (Types.pi1 def).Joint.joint_if_entry in
631  let init = { Joint.joint_if_luniverse =
632    (Types.pi1 def).Joint.joint_if_luniverse; Joint.joint_if_runiverse =
633    runiv; Joint.joint_if_result = data0.init_ret; Joint.joint_if_params =
634    data0.init_params; Joint.joint_if_stacksize = data0.init_stack_size;
635    Joint.joint_if_local_stacksize =
636    (Types.pi1 def).Joint.joint_if_local_stacksize; Joint.joint_if_code =
637    (Obj.magic (Identifiers.empty_map PreIdentifiers.LabelTag));
638    Joint.joint_if_entry = entry }
639  in
640  let prologue = data0.added_prologue in
641  let { Types.fst = init0; Types.snd = entry' } =
642    Obj.magic adds_graph_pre dst_g_pars globals (fun x i -> i) prologue
643      (Obj.magic entry) init
644  in
645  let f_step0 =
646    match not_emptyb prologue with
647    | Bool.True ->
648      (fun lbl ->
649        match Identifiers.eq_identifier PreIdentifiers.LabelTag lbl
650                (Obj.magic entry) with
651        | Bool.True ->
652          (fun x -> Bind_new.Bret
653            (Blocks.ensure_step_block
654              (Joint.graph_params_to_params dst_g_pars) globals List.Nil))
655        | Bool.False -> data0.f_step lbl)
656    | Bool.False -> data0.f_step
657  in
658  let f = fun lbl stmt def0 ->
659    match stmt with
660    | Joint.Sequential (inst, next) ->
661      b_adds_graph dst_g_pars globals (f_step0 lbl inst) lbl (Obj.magic next)
662        def0
663    | Joint.Final inst ->
664      b_fin_adds_graph dst_g_pars globals (data0.f_fin lbl inst) lbl def0
665    | Joint.FCOND (x, x0, x1) -> assert false (* absurd case *)
666  in
667  let def_out =
668    Identifiers.foldi PreIdentifiers.LabelTag f
669      (Obj.magic (Types.pi1 def).Joint.joint_if_code) init0
670  in
671  let def_out0 =
672    match not_emptyb prologue with
673    | Bool.True ->
674      let init_c =
675        get_first_costlabel (Joint.graph_params_to_params src_g_pars) globals
676          def
677      in
678      let { Types.fst = def_out0; Types.snd = entry'' } =
679        Obj.magic fresh_label (Joint.graph_params_to_params dst_g_pars)
680          globals def_out
681      in
682      let def_out1 =
683        Joint.add_graph dst_g_pars globals entry'' (Joint.Sequential
684          ((Joint.COST_LABEL init_c), entry')) def_out0
685      in
686      set_entry globals (Joint.graph_params_to_params dst_g_pars) def_out1
687        (Obj.magic entry'')
688    | Bool.False -> def_out
689  in
690  def_out0
691
692(** val b_graph_transform_program :
693    Joint.graph_params -> Joint.graph_params -> (AST.ident List.list ->
694    Joint.joint_closed_internal_function -> bound_b_graph_translate_data) ->
695    Joint.joint_program -> Joint.joint_program **)
696let b_graph_transform_program src dst init p =
697  { Joint.joint_prog =
698    (AST.transform_program p.Joint.joint_prog (fun varnames ->
699      AST.transf_fundef (fun def_in ->
700        Types.pi1
701          (b_graph_translate src dst varnames (init varnames def_in) def_in))));
702    Joint.init_cost_label = p.Joint.init_cost_label }
703
704(** val added_registers :
705    Joint.graph_params -> AST.ident List.list ->
706    Joint.joint_internal_function -> (Graphs.label -> Registers.register
707    List.list) -> Registers.register List.list **)
708let added_registers p g def f_regs =
709  let f = fun lbl x acc -> List.append (f_regs lbl) acc in
710  Identifiers.foldi PreIdentifiers.LabelTag f
711    (Obj.magic def.Joint.joint_if_code) List.Nil
712
Note: See TracBrowser for help on using the repository browser.