Changeset 1082 for src/ERTL/ERTLToLTL.ma


Ignore:
Timestamp:
Jul 20, 2011, 5:17:38 PM (9 years ago)
Author:
mulligan
Message:

work from today on ertl -> ltl pass

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r759 r1082  
    11include "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 *)
     2include "LTL/LTL.ma".
Note: See TracChangeset for help on using the changeset viewer.