Changeset 757 for src/ERTL


Ignore:
Timestamp:
Apr 18, 2011, 12:30:53 PM (10 years ago)
Author:
mulligan
Message:

Lots more fixing to get both front and backends using same conventions and types.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r753 r757  
    33 
    44axiom translate_ERTL_func:
    5   ∀globals: list Identifier.
    6     list (Identifier × ERTLFunction) → list (Identifier × (LTLFunctionDefinition globals)).
     5  ∀globals: list ident.
     6    list (ident × ertl_function) → list (ident × (ltl_function_definition globals)).
    77 
    8 definition translate: ∀e: ERTLProgram. LTLProgram (ERTL_Pr_Vars e) ≝
     8definition translate: ∀e: ertl_program. ltl_program (ertl_pr_vars e) ≝
    99  λp.
    10     let globals ≝ map ? ? \fst (ERTL_Pr_Vars p) in
    11     let ltl_pr_funcs ≝ map ? ? ? (ERTL_Pr_Funcs p) in
    12       mk_LTLProgram (ERTL_Pr_Vars p) ltl_pr_funcs (ERTL_Pr_Main 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).
    1313    # H1
    14     @ (translate_ERTL_func globals) in ⊢ (? × %) (* dpm here *)
     14    @ (translate_ertl_func globals) in ⊢ (? × %) (* dpm here *)
Note: See TracChangeset for help on using the changeset viewer.