Line | |
---|

1 | include "ERTL/ERTL.ma". |
---|

2 | include "ERTL/ERTLToLTLI.ma". |
---|

3 | include "LTL/LTL.ma". |
---|

4 | include "ERTL/spill.ma". |
---|

5 | |
---|

6 | definition 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 | |
---|

38 | definition 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 | |
---|

49 | definition 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.