source: src/ERTL/ERTLToLTL.ma @ 759

Last change on this file since 759 was 759, checked in by mulligan, 9 years ago

More work on the RTL to ERTL pass.

File size: 529 bytes
Line 
1include "ERTL/ERTL.ma".
2include "LTL/LTL.ma".
3 
4axiom translate_ertl_func:
5  ∀globals: list ident.
6    list (ident × ertl_function) → list (ident × (ltl_function_definition globals)).
7 
8definition 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.