Changeset 757 for src/ERTL/ERTLToLTL.ma

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:

• src/ERTL/ERTLToLTL.ma (modified) (1 diff)

src/ERTL/ERTLToLTL.ma

@@ -3 +3 @@
  
 axiom translate_ERTL_func:
-  ∀globals: list Identifier.
-    list (Identifier × ERTLFunction) → list (Identifier × (LTLFunctionDefinition globals)).
+  ∀globals: list ident.
+    list (ident × ertl_function) → list (ident × (ltl_function_definition globals)).
   
-definition translate: ∀e: ERTLProgram. LTLProgram (ERTL_Pr_Vars e) ≝
+definition translate: ∀e: ertl_program. ltl_program (ertl_pr_vars e) ≝
   λp.
-    let globals ≝ map ? ? \fst (ERTL_Pr_Vars p) in
-    let ltl_pr_funcs ≝ map ? ? ? (ERTL_Pr_Funcs p) in
-      mk_LTLProgram (ERTL_Pr_Vars p) ltl_pr_funcs (ERTL_Pr_Main p).
+    let globals ≝ map ? ? \fst (ertl_pr_vars p) in
+    let ltl_pr_funcs ≝ map ? ? ? (ertl_pr_funcs p) in
+      mk_ltl_program (ertl_pr_vars p) ltl_pr_funcs (ertl_pr_main p).
     # H1
-    @ (translate_ERTL_func globals) in ⊢ (? × %) (* dpm here *)
+    @ (translate_ertl_func globals) in ⊢ (? × %) (* dpm here *)