Last change
on this file since 1136 was
1128,
checked in by mulligan, 8 years ago

fixed ERTLtoLTLI so it type checks again

File size:
774 bytes

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  λ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  definition translate_funct ≝ 

18  λname_def. 

19  let 〈name, def〉 ≝ name_def in 

20  let def' ≝ 

21  match def with 

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

23   External def ⇒ External ? def 

24  ] 

25  in 

26  〈name, def'〉. 

27  

28  definition translate ≝ 

29  λp. 

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

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

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