Changeset 2475


Ignore:
Timestamp:
Nov 19, 2012, 5:13:21 PM (7 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:
5 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1964 r2475  
    1313      word_deqset
    1414      (program_counter …)
    15       (λs,class. ASM_classify … s = class)
     15      (λs. ASM_classify … s)
    1616      (λpc.lookup_opt ?? pc cost_labels)
    1717      (next_instruction_properly_relates_program_counters code_memory)
     18      ?
    1819      ?.
    19   cases daemon (* XXX: is final predicate *)
     20  cases daemon (* XXX: is final predicate, call ident function *)
    2021qed.
    2122
  • src/ASM/ASMCostsSplit.ma

    r2001 r2475  
    2222    | Some lbl ⇒ λlookup_refl.
    2323      let cost ≝ block_cost code_memory program_counter cost_labels in
    24         cic:/matita/cerco/common/Identifiers/add.fix(0,2,2) ?? cost_mapping lbl cost
     24        cic:/matita/cerco/common/Identifiers/add.fix(0,2,3) ?? cost_mapping lbl cost
    2525    ] (refl … (lookup_opt … program_counter cost_labels))
    2626  ] (refl … program_size).
  • src/RTLabs/semantics.ma

    r2395 r2475  
    319319    [ %{v} @Efd
    320320    | cases v in Efd;
    321       [ 5: * #b #off #Efd %{b} whd in Efd:(??(???%)?); cases (eq_offset ??) in Efd;
     321      [ 4: * #b #off #Efd %{b} whd in Efd:(??(???%)?); cases (eq_offset ??) in Efd;
    322322           [ #E @E | #E normalize in E; destruct ]
    323323      | *: normalize #A try #B try #C destruct
  • src/compiler.ma

    r2399 r2475  
    22include "Clight/label.ma".
    33include "Clight/SimplifyCasts.ma".
    4 (*include "Clight/switchRemoval.ma".*)
     4include "Clight/switchRemoval.ma".
    55include "Clight/toCminor.ma".
    66include "Cminor/initialisation.ma".
     
    99definition front_end : clight_program → res (costlabel × clight_program × RTLabs_program) ≝
    1010λp.
     11  let p ≝ program_switch_removal p in
    1112  let 〈p',init_cost〉 ≝ clight_label p in
    1213  let p ≝ simplify_program p' in
    13 (*  let p ≝ program_switch_removal p in*)
    1414  ! p ← clight_to_cminor p;
    1515  let p ≝ cminor_to_rtlabs init_cost p in
    1616  return 〈init_cost,p',p〉.
    1717
     18(* Recent changes have temporarily stopped the back-end from checking, so
     19   axiomatise it for a little while.
    1820include "RTLabs/RTLabsToRTL.ma".
    1921include "RTL/RTLToERTL.ma".
     
    3335  let p ≝ ltl_to_lin p in
    3436          lin_to_asm p.
     37*)
     38include "ASM/ASM.ma".
     39axiom back_end : RTLabs_program → pseudo_assembly_program.
    3540
    3641include "ASM/Assembly.ma".
  • src/correctness.ma

    r2412 r2475  
    3131
    3232%
    33 [ @labelling_sim @NOT_WRONG
     33[ (* Needs switch removal too, now
     34     @labelling_sim @NOT_WRONG
     35   *) cases daemon
    3436| @I
    3537] qed.
Note: See TracChangeset for help on using the changeset viewer.