|
Last change
on this file since 939 was
759,
checked in by mulligan, 10 years ago
|
|
More work on the RTL to ERTL pass.
|
|
File size:
529 bytes
|
| Line | |
|---|
| 1 | include "ERTL/ERTL.ma". |
|---|
| 2 | include "LTL/LTL.ma". |
|---|
| 3 | |
|---|
| 4 | axiom translate_ertl_func: |
|---|
| 5 | ∀globals: list ident. |
|---|
| 6 | list (ident × ertl_function) → list (ident × (ltl_function_definition globals)). |
|---|
| 7 | |
|---|
| 8 | definition translate: ∀e: ertl_program. ltl_program (ertl_pr_vars e) ≝ |
|---|
| 9 | λp. |
|---|
| 10 | let globals ≝ map ? ? \fst (ertl_pr_vars p) in |
|---|
| 11 | let ltl_pr_funcs ≝ map ? ? ? (ertl_pr_funcs p) in |
|---|
| 12 | mk_ltl_program (ertl_pr_vars p) ltl_pr_funcs (ertl_pr_main p). |
|---|
| 13 | # H1 |
|---|
| 14 | @ (translate_ertl_func globals) in ⊢ (? × %) (* dpm here *) |
|---|
Note: See
TracBrowser
for help on using the repository browser.
