source: extracted/translateUtils.ml @ 2968

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

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File size: 28.0 KB
RevLine 
[2717]1open Preamble
2
[2951]3open Extra_bool
4
5open Coqlib
6
7open Values
8
9open FrontEndVal
10
11open GenMem
12
13open FrontEndMem
14
15open Globalenvs
16
[2717]17open String
18
19open Sets
20
21open Listb
22
23open LabelledObjects
24
[2773]25open BitVectorTrie
26
[2717]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
[2773]67open Setoids
68
69open Monad
70
71open Option
72
[2717]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
[2730]129open Deqsets_extra
[2717]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
[2773]195  let op = insts.Types.fst.Types.snd in
[2717]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
[2773]204  Joint.add_graph g_pars globals mid (Joint.Sequential ((Obj.magic op mid),
[2717]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 append_seq_list :
220    Joint.params -> AST.ident List.list -> Blocks.bind_step_block ->
221    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new ->
222    Blocks.bind_step_block **)
[2773]223let append_seq_list p g bbl bl =
[2717]224  Obj.magic
225    (Monad.m_bind3 (Monad.max_def Bind_new.bindNew) (Obj.magic bbl)
[2773]226      (fun pref op post ->
[2717]227      Monad.m_bind0 (Monad.max_def Bind_new.bindNew) (Obj.magic bl) (fun l ->
228        Monad.m_return0 (Monad.max_def Bind_new.bindNew) { Types.fst =
[2773]229          { Types.fst = pref; Types.snd = op }; Types.snd =
[2717]230          (List.append post l) })))
231
232(** val b_adds_graph :
233    Joint.graph_params -> AST.ident List.list -> Blocks.bind_step_block ->
234    Graphs.label -> Graphs.label -> Joint.joint_internal_function ->
235    Joint.joint_internal_function **)
236let b_adds_graph g_pars globals insts src dst def =
237  let { Types.fst = def0; Types.snd = stmts } =
238    Obj.magic Bind_new.bcompile
239      (fresh_register (Joint.graph_params_to_params g_pars) globals) insts
240      def
241  in
242  adds_graph g_pars globals stmts src dst def0
243
244(** val b_fin_adds_graph :
245    Joint.graph_params -> AST.ident List.list -> Blocks.bind_fin_block ->
246    Graphs.label -> Joint.joint_internal_function ->
247    Joint.joint_internal_function **)
248let b_fin_adds_graph g_pars globals insts src def =
249  let { Types.fst = def0; Types.snd = stmts } =
250    Obj.magic Bind_new.bcompile
251      (fresh_register (Joint.graph_params_to_params g_pars) globals) insts
252      def
253  in
254  fin_adds_graph g_pars globals stmts src def0
255
[2827]256(** val step_registers :
257    Joint.uns_params -> AST.ident List.list -> Joint.joint_step ->
258    Registers.register List.list **)
259let step_registers p globals s =
260  Joint.get_used_registers_from_step p.Joint.u_pars globals p.Joint.functs s
261
262(** val fin_step_registers :
263    Joint.uns_params -> Joint.joint_fin_step -> Registers.register List.list **)
264let fin_step_registers p = function
265| Joint.GOTO x -> List.Nil
266| Joint.RETURN -> List.Nil
267| Joint.TAILCALL (x0, r) -> p.Joint.functs.Joint.f_call_args r
268
[2717]269type b_graph_translate_data = { init_ret : __; init_params : __;
270                                init_stack_size : Nat.nat;
271                                added_prologue : Joint.joint_seq List.list;
[2827]272                                new_regs : Registers.register List.list;
[2717]273                                f_step : (Graphs.label -> Joint.joint_step ->
274                                         Blocks.bind_step_block);
275                                f_fin : (Graphs.label -> Joint.joint_fin_step
276                                        -> Blocks.bind_fin_block) }
277
278(** val b_graph_translate_data_rect_Type4 :
279    Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
[2827]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 **)
[2951]284let rec b_graph_translate_data_rect_Type4 src dst globals h_mk_b_graph_translate_data x_18305 =
[2717]285  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
[2827]286    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
[2951]287    f_step = f_step0; f_fin = f_fin0 } = x_18305
[2717]288  in
289  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
[2827]290    added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
[2717]291
292(** val b_graph_translate_data_rect_Type5 :
293    Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
[2827]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 **)
[2951]298let rec b_graph_translate_data_rect_Type5 src dst globals h_mk_b_graph_translate_data x_18307 =
[2717]299  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
[2827]300    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
[2951]301    f_step = f_step0; f_fin = f_fin0 } = x_18307
[2717]302  in
303  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
[2827]304    added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
[2717]305
306(** val b_graph_translate_data_rect_Type3 :
307    Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
[2827]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 **)
[2951]312let rec b_graph_translate_data_rect_Type3 src dst globals h_mk_b_graph_translate_data x_18309 =
[2717]313  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
[2827]314    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
[2951]315    f_step = f_step0; f_fin = f_fin0 } = x_18309
[2717]316  in
317  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
[2827]318    added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
[2717]319
320(** val b_graph_translate_data_rect_Type2 :
321    Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
[2827]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 **)
[2951]326let rec b_graph_translate_data_rect_Type2 src dst globals h_mk_b_graph_translate_data x_18311 =
[2717]327  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
[2827]328    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
[2951]329    f_step = f_step0; f_fin = f_fin0 } = x_18311
[2717]330  in
331  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
[2827]332    added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
[2717]333
334(** val b_graph_translate_data_rect_Type1 :
335    Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
[2827]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 **)
[2951]340let rec b_graph_translate_data_rect_Type1 src dst globals h_mk_b_graph_translate_data x_18313 =
[2717]341  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
[2827]342    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
[2951]343    f_step = f_step0; f_fin = f_fin0 } = x_18313
[2717]344  in
345  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
[2827]346    added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
[2717]347
348(** val b_graph_translate_data_rect_Type0 :
349    Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
[2827]350    __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
351    List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
352    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
353    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
[2951]354let rec b_graph_translate_data_rect_Type0 src dst globals h_mk_b_graph_translate_data x_18315 =
[2717]355  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
[2827]356    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
[2951]357    f_step = f_step0; f_fin = f_fin0 } = x_18315
[2717]358  in
359  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
[2827]360    added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
[2717]361
362(** val init_ret :
363    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
364    b_graph_translate_data -> __ **)
365let rec init_ret src dst globals xxx =
366  xxx.init_ret
367
368(** val init_params :
369    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
370    b_graph_translate_data -> __ **)
371let rec init_params src dst globals xxx =
372  xxx.init_params
373
374(** val init_stack_size :
375    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
376    b_graph_translate_data -> Nat.nat **)
377let rec init_stack_size src dst globals xxx =
378  xxx.init_stack_size
379
380(** val added_prologue :
381    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
382    b_graph_translate_data -> Joint.joint_seq List.list **)
383let rec added_prologue src dst globals xxx =
384  xxx.added_prologue
385
[2827]386(** val new_regs :
387    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
388    b_graph_translate_data -> Registers.register List.list **)
389let rec new_regs src dst globals xxx =
390  xxx.new_regs
391
[2717]392(** val f_step :
393    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
394    b_graph_translate_data -> Graphs.label -> Joint.joint_step ->
395    Blocks.bind_step_block **)
396let rec f_step src dst globals xxx =
397  xxx.f_step
398
399(** val f_fin :
400    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
401    b_graph_translate_data -> Graphs.label -> Joint.joint_fin_step ->
402    Blocks.bind_fin_block **)
403let rec f_fin src dst globals xxx =
404  xxx.f_fin
405
406(** val b_graph_translate_data_inv_rect_Type4 :
407    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
408    b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
[2827]409    List.list -> Registers.register List.list -> (Graphs.label ->
410    Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
411    Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
412    __ -> 'a1) -> 'a1 **)
[2717]413let b_graph_translate_data_inv_rect_Type4 x1 x2 x3 hterm h1 =
414  let hcut = b_graph_translate_data_rect_Type4 x1 x2 x3 h1 hterm in hcut __
415
416(** val b_graph_translate_data_inv_rect_Type3 :
417    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
418    b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
[2827]419    List.list -> Registers.register List.list -> (Graphs.label ->
420    Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
421    Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
422    __ -> 'a1) -> 'a1 **)
[2717]423let b_graph_translate_data_inv_rect_Type3 x1 x2 x3 hterm h1 =
424  let hcut = b_graph_translate_data_rect_Type3 x1 x2 x3 h1 hterm in hcut __
425
426(** val b_graph_translate_data_inv_rect_Type2 :
427    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
428    b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
[2827]429    List.list -> Registers.register List.list -> (Graphs.label ->
430    Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
431    Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
432    __ -> 'a1) -> 'a1 **)
[2717]433let b_graph_translate_data_inv_rect_Type2 x1 x2 x3 hterm h1 =
434  let hcut = b_graph_translate_data_rect_Type2 x1 x2 x3 h1 hterm in hcut __
435
436(** val b_graph_translate_data_inv_rect_Type1 :
437    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
438    b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
[2827]439    List.list -> Registers.register List.list -> (Graphs.label ->
440    Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
441    Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
442    __ -> 'a1) -> 'a1 **)
[2717]443let b_graph_translate_data_inv_rect_Type1 x1 x2 x3 hterm h1 =
444  let hcut = b_graph_translate_data_rect_Type1 x1 x2 x3 h1 hterm in hcut __
445
446(** val b_graph_translate_data_inv_rect_Type0 :
447    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
448    b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
[2827]449    List.list -> Registers.register List.list -> (Graphs.label ->
450    Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
451    Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
452    __ -> 'a1) -> 'a1 **)
[2717]453let b_graph_translate_data_inv_rect_Type0 x1 x2 x3 hterm h1 =
454  let hcut = b_graph_translate_data_rect_Type0 x1 x2 x3 h1 hterm in hcut __
455
456(** val b_graph_translate_data_jmdiscr :
457    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
458    b_graph_translate_data -> b_graph_translate_data -> __ **)
459let b_graph_translate_data_jmdiscr a1 a2 a3 x y =
460  Logic.eq_rect_Type2 x
461    (let { init_ret = a0; init_params = a10; init_stack_size = a20;
[2827]462       added_prologue = a30; new_regs = a4; f_step = a5; f_fin = a6 } = x
[2717]463     in
[2827]464    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __)) y
[2717]465
[2827]466type bound_b_graph_translate_data =
467  (Registers.register, b_graph_translate_data) Bind_new.bind_new Types.sig0
468
[2717]469(** val get_first_costlabel :
470    Joint.params -> AST.ident List.list ->
471    Joint.joint_closed_internal_function -> (CostLabel.costlabel, __)
472    Types.prod **)
[2773]473let get_first_costlabel p g def =
474  (match p.Joint.stmt_at g (Types.pi1 def).Joint.joint_if_code
[2827]475           (Types.pi1 def).Joint.joint_if_entry with
[2717]476   | Types.None -> (fun _ -> assert false (* absurd case *))
477   | Types.Some s ->
478     (match s with
479      | Joint.Sequential (s', nxt) ->
480        (match s' with
481         | Joint.COST_LABEL c ->
482           (fun _ -> { Types.fst = c; Types.snd = nxt })
483         | Joint.CALL (x, x0, x1) ->
484           (fun _ -> assert false (* absurd case *))
485         | Joint.COND (x, x0) -> (fun _ -> assert false (* absurd case *))
486         | Joint.Step_seq x -> (fun _ -> assert false (* absurd case *)))
487      | Joint.Final x -> (fun _ -> assert false (* absurd case *))
488      | Joint.FCOND (x0, x1, x2) -> (fun _ -> assert false (* absurd case *))))
489    __
490
491(** val b_graph_translate_props_rect_Type4 :
492    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
[2827]493    b_graph_translate_data -> Joint.joint_closed_internal_function ->
[2717]494    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
[2827]495    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
496    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
497let 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 =
[2717]498  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
499
500(** val b_graph_translate_props_rect_Type5 :
501    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
[2827]502    b_graph_translate_data -> Joint.joint_closed_internal_function ->
[2717]503    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
[2827]504    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
505    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
506let 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 =
[2717]507  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
508
509(** val b_graph_translate_props_rect_Type3 :
510    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
[2827]511    b_graph_translate_data -> Joint.joint_closed_internal_function ->
[2717]512    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
[2827]513    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
514    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
515let 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 =
[2717]516  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
517
518(** val b_graph_translate_props_rect_Type2 :
519    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
[2827]520    b_graph_translate_data -> Joint.joint_closed_internal_function ->
[2717]521    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
[2827]522    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
523    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
524let 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 =
[2717]525  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
526
527(** val b_graph_translate_props_rect_Type1 :
528    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
[2827]529    b_graph_translate_data -> Joint.joint_closed_internal_function ->
[2717]530    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
[2827]531    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
532    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
533let 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 =
[2717]534  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
535
536(** val b_graph_translate_props_rect_Type0 :
537    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
[2827]538    b_graph_translate_data -> Joint.joint_closed_internal_function ->
[2717]539    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
[2827]540    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
541    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
542let 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 =
[2717]543  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
544
545(** val b_graph_translate_props_inv_rect_Type4 :
546    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
[2827]547    b_graph_translate_data -> Joint.joint_closed_internal_function ->
[2717]548    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
[2827]549    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
550    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
551    'a1 **)
552let b_graph_translate_props_inv_rect_Type4 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
553  let hcut = b_graph_translate_props_rect_Type4 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
[2717]554  hcut __
555
556(** val b_graph_translate_props_inv_rect_Type3 :
557    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
[2827]558    b_graph_translate_data -> Joint.joint_closed_internal_function ->
[2717]559    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
[2827]560    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
561    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
562    'a1 **)
563let b_graph_translate_props_inv_rect_Type3 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
564  let hcut = b_graph_translate_props_rect_Type3 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
[2717]565  hcut __
566
567(** val b_graph_translate_props_inv_rect_Type2 :
568    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
[2827]569    b_graph_translate_data -> Joint.joint_closed_internal_function ->
[2717]570    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
[2827]571    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
572    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
573    'a1 **)
574let b_graph_translate_props_inv_rect_Type2 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
575  let hcut = b_graph_translate_props_rect_Type2 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
[2717]576  hcut __
577
578(** val b_graph_translate_props_inv_rect_Type1 :
579    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
[2827]580    b_graph_translate_data -> Joint.joint_closed_internal_function ->
[2717]581    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
[2827]582    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
583    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
584    'a1 **)
585let b_graph_translate_props_inv_rect_Type1 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
586  let hcut = b_graph_translate_props_rect_Type1 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
[2717]587  hcut __
588
589(** val b_graph_translate_props_inv_rect_Type0 :
590    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
[2827]591    b_graph_translate_data -> Joint.joint_closed_internal_function ->
[2717]592    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
[2827]593    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
594    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
595    'a1 **)
596let b_graph_translate_props_inv_rect_Type0 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
597  let hcut = b_graph_translate_props_rect_Type0 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
[2717]598  hcut __
599
600(** val b_graph_translate_props_jmdiscr :
601    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
[2827]602    b_graph_translate_data -> Joint.joint_closed_internal_function ->
[2717]603    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
[2827]604    List.list) -> (Graphs.label -> Registers.register List.list) -> __ **)
605let b_graph_translate_props_jmdiscr a1 a2 a3 a4 a5 a6 a7 a8 =
[2717]606  Logic.eq_rect_Type2 __
607    (Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __)) __
608
609(** val pair_swap : ('a1, 'a2) Types.prod -> ('a2, 'a1) Types.prod **)
610let pair_swap pr =
611  { Types.fst = pr.Types.snd; Types.snd = pr.Types.fst }
612
613(** val b_graph_translate :
614    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
[2827]615    bound_b_graph_translate_data -> Joint.joint_closed_internal_function ->
[2717]616    Joint.joint_closed_internal_function Types.sig0 **)
617let b_graph_translate src_g_pars dst_g_pars globals data def =
618  let runiv_data =
619    Obj.magic Bind_new.bcompile
620      (Obj.magic
621        (Relations.compose pair_swap
[2827]622          (Identifiers.fresh PreIdentifiers.RegisterTag))) (Types.pi1 data)
[2717]623      (Types.pi1 def).Joint.joint_if_runiverse
624  in
625  let runiv = runiv_data.Types.fst in
626  let data0 = runiv_data.Types.snd in
627  let entry = (Types.pi1 def).Joint.joint_if_entry in
628  let init = { Joint.joint_if_luniverse =
629    (Types.pi1 def).Joint.joint_if_luniverse; Joint.joint_if_runiverse =
630    runiv; Joint.joint_if_result = data0.init_ret; Joint.joint_if_params =
631    data0.init_params; Joint.joint_if_stacksize = data0.init_stack_size;
[2827]632    Joint.joint_if_local_stacksize =
633    (Types.pi1 def).Joint.joint_if_local_stacksize; Joint.joint_if_code =
[2717]634    (Obj.magic
635      (Identifiers.add PreIdentifiers.LabelTag
[2827]636        (Identifiers.empty_map PreIdentifiers.LabelTag) (Obj.magic entry)
637        (Joint.Final Joint.RETURN))); Joint.joint_if_entry = entry }
[2717]638  in
639  let f = fun lbl stmt def0 ->
640    match stmt with
641    | Joint.Sequential (inst, next) ->
642      b_adds_graph dst_g_pars globals (data0.f_step lbl inst) lbl
643        (Obj.magic next) def0
644    | Joint.Final inst ->
645      b_fin_adds_graph dst_g_pars globals (data0.f_fin lbl inst) lbl def0
646    | Joint.FCOND (x, x0, x1) -> assert false (* absurd case *)
647  in
648  let def_out =
[2773]649    Identifiers.foldi PreIdentifiers.LabelTag f
[2717]650      (Obj.magic (Types.pi1 def).Joint.joint_if_code) init
651  in
652  let init_c_nxt =
653    get_first_costlabel (Joint.graph_params_to_params src_g_pars) globals def
654  in
655  let def_out_nxt =
656    Obj.magic adds_graph_post dst_g_pars globals data0.added_prologue
657      (Obj.magic init_c_nxt).Types.snd def_out
658  in
[2827]659  Joint.add_graph dst_g_pars globals (Obj.magic entry) (Joint.Sequential
660    ((Joint.COST_LABEL init_c_nxt.Types.fst), def_out_nxt.Types.snd))
661    def_out_nxt.Types.fst
[2717]662
663(** val b_graph_transform_program :
664    Joint.graph_params -> Joint.graph_params -> (AST.ident List.list ->
[2827]665    Joint.joint_closed_internal_function -> bound_b_graph_translate_data) ->
666    Joint.joint_program -> Joint.joint_program **)
[2717]667let b_graph_transform_program src dst init p =
[2951]668  { Joint.joint_prog =
669    (AST.transform_program p.Joint.joint_prog (fun varnames ->
670      AST.transf_fundef (fun def_in ->
671        Types.pi1
672          (b_graph_translate src dst varnames (init varnames def_in) def_in))));
673    Joint.init_cost_label = p.Joint.init_cost_label }
[2717]674
675(** val added_registers :
676    Joint.graph_params -> AST.ident List.list ->
677    Joint.joint_internal_function -> (Graphs.label -> Registers.register
[2854]678    List.list) -> Registers.register List.list **)
[2773]679let added_registers p g def f_regs =
[2854]680  let f = fun lbl x acc -> List.append (f_regs lbl) acc in
[2773]681  Identifiers.foldi PreIdentifiers.LabelTag f
[2717]682    (Obj.magic def.Joint.joint_if_code) List.Nil
683
Note: See TracBrowser for help on using the repository browser.