Last change
on this file since 1088 was
1088,
checked in by mulligan, 10 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.