source: extracted/translateUtils.ml @ 2746

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

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

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