Changeset 2475 for src

Timestamp:

Nov 19, 2012, 5:13:21 PM (8 years ago)

Author:

campbell

Message:

Get compiler.ma and correctness.ma checking again. Note that the back-end
is in a state of flux at the moment, so is axiomatised out.

Location:

src

Files:

• ASM/ASMCosts.ma (modified) (1 diff)
• ASM/ASMCostsSplit.ma (modified) (1 diff)
• RTLabs/semantics.ma (modified) (1 diff)
• compiler.ma (modified) (3 diffs)
• correctness.ma (modified) (1 diff)

src/ASM/ASMCosts.ma

@@ -13 +13 @@
       word_deqset
       (program_counter …)
-      (λs,class. ASM_classify … s = class)
+      (λs. ASM_classify … s)
       (λpc.lookup_opt ?? pc cost_labels)
       (next_instruction_properly_relates_program_counters code_memory)
+      ?
       ?.
-  cases daemon (* XXX: is final predicate *)
+  cases daemon (* XXX: is final predicate, call ident function *)
 qed.
 

src/ASM/ASMCostsSplit.ma

@@ -22 +22 @@
     | Some lbl ⇒ λlookup_refl.
       let cost ≝ block_cost code_memory program_counter cost_labels in
-        cic:/matita/cerco/common/Identifiers/add.fix(0,2,2) ?? cost_mapping lbl cost
+        cic:/matita/cerco/common/Identifiers/add.fix(0,2,3) ?? cost_mapping lbl cost
     ] (refl … (lookup_opt … program_counter cost_labels))
   ] (refl … program_size).

src/RTLabs/semantics.ma

@@ -319 +319 @@
     [ %{v} @Efd
     | cases v in Efd;
-      [ 5: * #b #off #Efd %{b} whd in Efd:(??(???%)?); cases (eq_offset ??) in Efd;
+      [ 4: * #b #off #Efd %{b} whd in Efd:(??(???%)?); cases (eq_offset ??) in Efd;
            [ #E @E | #E normalize in E; destruct ]
       | *: normalize #A try #B try #C destruct

src/compiler.ma

@@ -2 +2 @@
 include "Clight/label.ma".
 include "Clight/SimplifyCasts.ma".
-(*include "Clight/switchRemoval.ma".*)
+include "Clight/switchRemoval.ma".
 include "Clight/toCminor.ma".
 include "Cminor/initialisation.ma".
@@ -9 +9 @@
 definition front_end : clight_program → res (costlabel × clight_program × RTLabs_program) ≝
 λp.
+  let p ≝ program_switch_removal p in
   let 〈p',init_cost〉 ≝ clight_label p in
   let p ≝ simplify_program p' in
-(*  let p ≝ program_switch_removal p in*)
   ! p ← clight_to_cminor p;
   let p ≝ cminor_to_rtlabs init_cost p in
   return 〈init_cost,p',p〉.
 
+(* Recent changes have temporarily stopped the back-end from checking, so
+   axiomatise it for a little while.
 include "RTLabs/RTLabsToRTL.ma".
 include "RTL/RTLToERTL.ma".
@@ -33 +35 @@
   let p ≝ ltl_to_lin p in
           lin_to_asm p.
+*)
+include "ASM/ASM.ma".
+axiom back_end : RTLabs_program → pseudo_assembly_program.
 
 include "ASM/Assembly.ma".

src/correctness.ma

@@ -31 +31 @@
 
 %
-[ @labelling_sim @NOT_WRONG
+[ (* Needs switch removal too, now
+     @labelling_sim @NOT_WRONG
+   *) cases daemon
 | @I
 ] qed.