source: driver/extracted/translateUtils.ml @ 3106

Last change on this file since 3106 was 3059, 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_18277 =
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_18277
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_18279 =
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_18279
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_18281 =
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_18281
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_18283 =
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_18283
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_18285 =
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_18285
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_18287 =
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_18287
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_next :
457    Joint.params -> AST.ident List.list ->
458    Joint.joint_closed_internal_function -> (CostLabel.costlabel, __)
459    Types.prod **)
460let get_first_costlabel_next p g def =
461  (match p.Joint.stmt_at g (Types.pi1 def).Joint.joint_if_code
462           (Types.pi1 def).Joint.joint_if_entry with
463   | Types.None -> (fun _ -> assert false (* absurd case *))
464   | Types.Some s ->
465     (match s with
466      | Joint.Sequential (s', nxt) ->
467        (match s' with
468         | Joint.COST_LABEL c ->
469           (fun _ -> { Types.fst = c; Types.snd = nxt })
470         | Joint.CALL (x, x0, x1) ->
471           (fun _ -> assert false (* absurd case *))
472         | Joint.COND (x, x0) -> (fun _ -> assert false (* absurd case *))
473         | Joint.Step_seq x -> (fun _ -> assert false (* absurd case *)))
474      | Joint.Final x -> (fun _ -> assert false (* absurd case *))
475      | Joint.FCOND (x0, x1, x2) -> (fun _ -> assert false (* absurd case *))))
476    __
477
478(** val get_first_costlabel :
479    Joint.params -> AST.ident List.list ->
480    Joint.joint_closed_internal_function -> CostLabel.costlabel **)
481let get_first_costlabel p g f =
482  (get_first_costlabel_next p g f).Types.fst
483
484(** val not_emptyb : 'a1 List.list -> Bool.bool **)
485let not_emptyb = function
486| List.Nil -> Bool.False
487| List.Cons (x, x0) -> Bool.True
488
489(** val b_graph_translate_props_rect_Type4 :
490    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
491    b_graph_translate_data -> Joint.joint_closed_internal_function ->
492    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
493    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
494    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
495let 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 =
496  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
497
498(** val b_graph_translate_props_rect_Type5 :
499    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
500    b_graph_translate_data -> Joint.joint_closed_internal_function ->
501    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
502    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
503    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
504let 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 =
505  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
506
507(** val b_graph_translate_props_rect_Type3 :
508    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
509    b_graph_translate_data -> Joint.joint_closed_internal_function ->
510    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
511    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
512    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
513let 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 =
514  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
515
516(** val b_graph_translate_props_rect_Type2 :
517    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
518    b_graph_translate_data -> Joint.joint_closed_internal_function ->
519    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
520    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
521    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
522let 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 =
523  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
524
525(** val b_graph_translate_props_rect_Type1 :
526    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
527    b_graph_translate_data -> Joint.joint_closed_internal_function ->
528    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
529    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
530    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
531let 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 =
532  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
533
534(** val b_graph_translate_props_rect_Type0 :
535    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
536    b_graph_translate_data -> Joint.joint_closed_internal_function ->
537    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
538    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
539    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
540let 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 =
541  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
542
543(** val b_graph_translate_props_inv_rect_Type4 :
544    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
545    b_graph_translate_data -> Joint.joint_closed_internal_function ->
546    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
547    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
548    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
549    'a1 **)
550let b_graph_translate_props_inv_rect_Type4 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
551  let hcut = b_graph_translate_props_rect_Type4 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
552  hcut __
553
554(** val b_graph_translate_props_inv_rect_Type3 :
555    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
556    b_graph_translate_data -> Joint.joint_closed_internal_function ->
557    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
558    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
559    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
560    'a1 **)
561let b_graph_translate_props_inv_rect_Type3 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
562  let hcut = b_graph_translate_props_rect_Type3 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
563  hcut __
564
565(** val b_graph_translate_props_inv_rect_Type2 :
566    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
567    b_graph_translate_data -> Joint.joint_closed_internal_function ->
568    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
569    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
570    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
571    'a1 **)
572let b_graph_translate_props_inv_rect_Type2 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
573  let hcut = b_graph_translate_props_rect_Type2 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
574  hcut __
575
576(** val b_graph_translate_props_inv_rect_Type1 :
577    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
578    b_graph_translate_data -> Joint.joint_closed_internal_function ->
579    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
580    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
581    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
582    'a1 **)
583let b_graph_translate_props_inv_rect_Type1 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
584  let hcut = b_graph_translate_props_rect_Type1 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
585  hcut __
586
587(** val b_graph_translate_props_inv_rect_Type0 :
588    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
589    b_graph_translate_data -> Joint.joint_closed_internal_function ->
590    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
591    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
592    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
593    'a1 **)
594let b_graph_translate_props_inv_rect_Type0 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
595  let hcut = b_graph_translate_props_rect_Type0 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
596  hcut __
597
598(** val b_graph_translate_props_jmdiscr :
599    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
600    b_graph_translate_data -> Joint.joint_closed_internal_function ->
601    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
602    List.list) -> (Graphs.label -> Registers.register List.list) -> __ **)
603let b_graph_translate_props_jmdiscr a1 a2 a3 a4 a5 a6 a7 a8 =
604  Logic.eq_rect_Type2 __
605    (Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __)) __
606
607(** val pair_swap : ('a1, 'a2) Types.prod -> ('a2, 'a1) Types.prod **)
608let pair_swap pr =
609  { Types.fst = pr.Types.snd; Types.snd = pr.Types.fst }
610
611(** val set_entry :
612    AST.ident List.list -> Joint.params -> Joint.joint_internal_function ->
613    __ -> Joint.joint_internal_function **)
614let set_entry globals pars int_fun entry =
615  { Joint.joint_if_luniverse = int_fun.Joint.joint_if_luniverse;
616    Joint.joint_if_runiverse = int_fun.Joint.joint_if_runiverse;
617    Joint.joint_if_result = int_fun.Joint.joint_if_result;
618    Joint.joint_if_params = int_fun.Joint.joint_if_params;
619    Joint.joint_if_stacksize = int_fun.Joint.joint_if_stacksize;
620    Joint.joint_if_local_stacksize = int_fun.Joint.joint_if_local_stacksize;
621    Joint.joint_if_code = int_fun.Joint.joint_if_code; Joint.joint_if_entry =
622    entry }
623
624(** val b_graph_translate :
625    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
626    bound_b_graph_translate_data -> Joint.joint_closed_internal_function ->
627    Joint.joint_closed_internal_function Types.sig0 **)
628let b_graph_translate src_g_pars dst_g_pars globals data def =
629  let runiv_data =
630    Obj.magic Bind_new.bcompile
631      (Obj.magic
632        (Relations.compose pair_swap
633          (Identifiers.fresh PreIdentifiers.RegisterTag))) (Types.pi1 data)
634      (Types.pi1 def).Joint.joint_if_runiverse
635  in
636  let runiv = runiv_data.Types.fst in
637  let data0 = runiv_data.Types.snd in
638  let entry = (Types.pi1 def).Joint.joint_if_entry in
639  let init = { Joint.joint_if_luniverse =
640    (Types.pi1 def).Joint.joint_if_luniverse; Joint.joint_if_runiverse =
641    runiv; Joint.joint_if_result = data0.init_ret; Joint.joint_if_params =
642    data0.init_params; Joint.joint_if_stacksize = data0.init_stack_size;
643    Joint.joint_if_local_stacksize =
644    (Types.pi1 def).Joint.joint_if_local_stacksize; Joint.joint_if_code =
645    (Obj.magic (Identifiers.empty_map PreIdentifiers.LabelTag));
646    Joint.joint_if_entry = entry }
647  in
648  let f = fun lbl stmt def0 ->
649    match stmt with
650    | Joint.Sequential (inst, next) ->
651      b_adds_graph dst_g_pars globals (data0.f_step lbl inst) lbl
652        (Obj.magic next) def0
653    | Joint.Final inst ->
654      b_fin_adds_graph dst_g_pars globals (data0.f_fin lbl inst) lbl def0
655    | Joint.FCOND (x, x0, x1) -> assert false (* absurd case *)
656  in
657  let def_out =
658    Identifiers.foldi PreIdentifiers.LabelTag f
659      (Obj.magic (Types.pi1 def).Joint.joint_if_code) init
660  in
661  let prologue = data0.added_prologue in
662  let def_out0 =
663    match not_emptyb prologue with
664    | Bool.True ->
665      let { Types.fst = init_c; Types.snd = nxt } =
666        get_first_costlabel_next (Joint.graph_params_to_params src_g_pars)
667          globals def
668      in
669      let def_out0 =
670        Joint.add_graph dst_g_pars globals (Obj.magic entry)
671          (Joint.Sequential ((Joint.Step_seq
672          (Joint.nOOP
673            (Joint.uns_pars__o__u_pars
674              (Joint.gp_to_p__o__stmt_pars dst_g_pars)) globals)), nxt))
675          def_out
676      in
677      let { Types.fst = def_out1; Types.snd = entry' } =
678        Obj.magic fresh_label (Joint.graph_params_to_params dst_g_pars)
679          globals def_out0
680      in
681      let def_out2 =
682        adds_graph dst_g_pars globals { Types.fst = { Types.fst = List.Nil;
683          Types.snd = (fun x -> Joint.COST_LABEL init_c) }; Types.snd =
684          prologue } entry' (Obj.magic entry) def_out1
685      in
686      set_entry globals (Joint.graph_params_to_params dst_g_pars) def_out2
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 =
697  Joint.transform_joint_program (Joint.graph_params_to_params src)
698    (Joint.graph_params_to_params dst) (fun varnames def_in ->
699    Types.pi1
700      (b_graph_translate src dst varnames (init varnames def_in) def_in))
701
702(** val added_registers :
703    Joint.graph_params -> AST.ident List.list ->
704    Joint.joint_internal_function -> (Graphs.label -> Registers.register
705    List.list) -> Registers.register List.list **)
706let added_registers p g def f_regs =
707  let f = fun lbl x acc -> List.append (f_regs lbl) acc in
708  Identifiers.foldi PreIdentifiers.LabelTag f
709    (Obj.magic def.Joint.joint_if_code) List.Nil
710
Note: See TracBrowser for help on using the repository browser.