Changeset 753 for src/ERTL

Timestamp:

Apr 14, 2011, 5:54:37 PM (10 years ago)

Author:

mulligan

Message:

Work from today.

Location:

src/ERTL

Files:

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

src/ERTL/ERTL.ma

@@ -58 +58 @@
   ERTL_Pr_Main: option Identifier
 }.
+
+definition ERTL_Pr_Vars: ERTLProgram → list (Identifier × nat).
+  # E
+  cases E
+  # H1 # H2 # H3
+  @ H1
+qed.

src/ERTL/ERTLToLTL.ma

@@ -1 +1 @@
 include "ERTL/ERTL.ma".
-  
-axiom translate_func:
+include "LTL/LTL.ma". 
+ 
+axiom translate_ERTL_func:
   ∀globals: list Identifier.
     list (Identifier × ERTLFunction) → list (Identifier × (LTLFunctionDefinition globals)).
   
-definition translate: ERTLProgram → LTLProgram ≝
+definition translate: ∀e: ERTLProgram. LTLProgram (ERTL_Pr_Vars e) ≝
   λp.
-    let globals ≝ map ? ? \fst (ERTL_Pr_Vars e) in
-    let ltl_pr_var ≝ ERTL_Pr_Vars e in
-    let ltl_pr_funcs ≝ map ? ? (translate_func globals) (ERTL_Pr_Funcs e) in
+    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).
+    # H1
+    @ (translate_ERTL_func globals) in ⊢ (? × %) (* dpm here *)