Changeset 2475 for src/compiler.ma


Ignore:
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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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".
Note: See TracChangeset for help on using the changeset viewer.