Changeset 1084 for src/ERTL/ERTLToLTL.ma

Timestamp:

Jul 21, 2011, 5:00:47 PM (10 years ago)

Author:

mulligan

Message:

more added on ertl pass: not sure how much should be axiomatised wrt register colouring

File:

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

src/ERTL/ERTLToLTL.ma

@@ -1 +1 @@
 include "ERTL/ERTL.ma".
+include "ERTL/ERTLToLTLI.ma".
 include "LTL/LTL.ma".
+
+definition translate_funct ≝
+  λname_def.
+  let 〈name, def〉 ≝ name_def in
+  let def' ≝
+    match def with
+    [ Internal def ⇒ Internal ? (translate_internal name def)
+    | External def ⇒ External ? def
+    ]
+  in
+    〈name, def'〉.
+
+definition translate ≝
+  λp.
+  let functs' ≝ map ? ? translate_funct (ertl_pr_functs p) in
+    mk_ltl_program (ertl_pr_globals p) functs' (ertl_pr_main p).