Last change
on this file since 1091 was
1091,
checked in by campbell, 10 years ago
|
Merge trunk into id-lookup-branch
|
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.