Changeset 2205 for src

Timestamp:

Jul 18, 2012, 12:27:01 PM (9 years ago)

Author:

campbell

Message:

Get correctness.ma type checking again.

Location:

src

Files:

• LTL/LTLToLIN.ma (modified) (3 diffs)
• compiler.ma (modified) (2 diffs)
• correctness.ma (modified) (1 diff)

src/LTL/LTLToLIN.ma

@@ -26 +26 @@
   [ O ⇒ ⊥ (* CSC: Case to be made impossible; use dummy value? *)
   | S n' ⇒
-    if mem_set … visited l then
+    if l∈visited then
      〈add_set ? required l, 〈None …, GOTO … globals l〉 :: generated〉
     else
@@ -42 +42 @@
              visit globals g required visited' generated' l2 n' in
             let required'' ≝ add_set ? required' l1 in
-             if mem_set … visited' l1 then
+             if l1 ∈ visited' then
                〈required', generated''〉
              else
@@ -71 +71 @@
        [ None ⇒ 〈None …,x〉
        | Some l ⇒
-          〈if mem_set … required' l then Some ? l else None ?,
+          〈if l ∈ required' then Some ? l else None ?,
            x〉])
     reversed.

src/compiler.ma

@@ -41 +41 @@
 include "ASM/ASMCostsSplit.ma".
 
+axiom assembler : pseudo_assembly_program → res (object_code × costlabel_map). (*
 definition assembler : pseudo_assembly_program → res (object_code × costlabel_map) ≝
 λp.
@@ -51 +52 @@
   OK ? (assembly p sigma pol).
 cases daemon
-qed.
+qed.*)
 
 include "RTLabs/semantics.ma".

src/correctness.ma

@@ -11 +11 @@
   ∀input_program.
 
-  not_wrong (exec_inf … clight_fullexec input_program) →
+  not_wrong … (exec_inf … clight_fullexec input_program) →
   
   ∀object_code,costlabel_map,labelled,cost_map.