Last change
on this file since 1110 was
1110,
checked in by mulligan, 10 years ago

changes to get ltl to lin pass to work properly

File size:
755 bytes

Line  

1  include "ERTL/ERTL.ma". 

2  include "ERTL/ERTLToLTLI.ma". 

3  include "LTL/LTL.ma". 

4  

5  (* 

6  definition translate_internal ≝ 

7  λf. 

8  λint_fun: ertl_internal_function. 

9  mk_ltl_internal_function ? 

10  (ertl_if_luniverse int_fun) 

11  (ertl_if_runiverse int_fun) 

12  (ertl_if_stacksize int_fun) 

13  (ertl_if_graph int_fun) 

14  ? 

15  ?. 

16  *) 

17  

18  definition translate_funct ≝ 

19  λname_def. 

20  let 〈name, def〉 ≝ name_def in 

21  let def' ≝ 

22  match def with 

23  [ Internal def ⇒ Internal ? (translate_internal name def) 

24   External def ⇒ External ? def 

25  ] 

26  in 

27  〈name, def'〉. 

28  

29  definition translate ≝ 

30  λp. 

31  let functs' ≝ map ? ? translate_funct (ertl_pr_functs p) in 

32  mk_ltl_program (ertl_pr_globals p) functs' (ertl_pr_main p). 

Note: See
TracBrowser
for help on using the repository browser.