Last change
on this file since 1091 was
1091,
checked in by campbell, 9 years ago

Merge trunk into idlookupbranch

File size:
749 bytes

Rev  Line  

[733]  1  include "ERTL/ERTL.ma". 

[1084]  2  include "ERTL/ERTLToLTLI.ma". 

 3  include "LTL/LTL.ma". 

 4  

[1091]  5  definition translate_internal ≝ 

 6  λf. 

 7  λint_fun: ertl_internal_function. 

 8  mk_ltl_internal_function ? 

 9  (ertl_if_luniverse int_fun) 

 10  (ertl_if_runiverse int_fun) 

 11  (ertl_if_stacksize int_fun) 

 12  (ertl_if_graph int_fun) 

 13  ? 

 14  ?. 

 15  

[1084]  16  definition translate_funct ≝ 

 17  λname_def. 

 18  let 〈name, def〉 ≝ name_def in 

 19  let def' ≝ 

 20  match def with 

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

 22   External def ⇒ External ? def 

 23  ] 

 24  in 

 25  〈name, def'〉. 

 26  

 27  definition translate ≝ 

 28  λp. 

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

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

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