|
Last change
on this file since 1088 was
1088,
checked in by mulligan, 9 years ago
|
|
work on liveness analysis: an imperative nightmare
|
|
File size:
749 bytes
|
| Line | |
|---|
| 1 | include "ERTL/ERTL.ma". |
|---|
| 2 | include "ERTL/ERTLToLTLI.ma". |
|---|
| 3 | include "LTL/LTL.ma". |
|---|
| 4 | |
|---|
| 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 | |
|---|
| 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.
