source: src/ERTL/ERTLToLTL.ma @ 1152

Last change on this file since 1152 was 1152, checked in by mulligan, 9 years ago

more added

File size: 1.4 KB
Line 
1include "ERTL/ERTL.ma".
2include "ERTL/ERTLToLTLI.ma".
3include "LTL/LTL.ma".
4include "ERTL/spill.ma".
5
6definition translate_internal ≝
7  λglobals: list ident.
8  λf.
9  λint_fun: ertl_internal_function.
10  let lookup ≝ λr.
11    match lookup r with
12    | colour_spill ->
13        ERTLToLTLI.Spill (Interference.Vertex.Map.find (Interference.lookup H.graph r) S.coloring)
14    | colour_colour color ->
15        ERTLToLTLI.Color color
16  in
17  let locals ≝ colour_locals + (ertl_if_stacksize int_fun) in
18  let stacksize ≝ (ertl_if_params int_fun) + locals in
19    mk_ltl_internal_function
20      globals
21      (ertl_if_luniverse int_fun)
22      (ertl_if_runiverse int_fun)
23      stacksize.
24
25  let () =
26    Label.Map.iter (fun label stmt ->
27      let stmt =
28        match Liveness.eliminable (G.liveafter label) stmt with
29        | Some successor ->
30            LTL.St_skip successor
31        | None ->
32            I.translate_statement stmt
33      in
34      graph := Label.Map.add label stmt !graph
35    ) int_fun.ERTL.f_graph
36  in
37
38definition translate_funct ≝
39  λname_def.
40  let 〈name, def〉 ≝ name_def in
41  let def' ≝
42    match def with
43    [ Internal def ⇒ Internal ? (translate_internal name def)
44    | External def ⇒ External ? def
45    ]
46  in
47    〈name, def'〉.
48
49definition translate ≝
50  λp.
51  let functs' ≝ map ? ? translate_funct (ertl_pr_functs p) in
52    mk_ltl_program (ertl_pr_globals p) functs' (ertl_pr_main p).
Note: See TracBrowser for help on using the repository browser.