source: src/compiler.ma @ 1991

Last change on this file since 1991 was 1991, checked in by campbell, 7 years ago

Put the front end transformations together and make an example use it.

File size: 503 bytes
Line 
1
2include "Clight/label.ma".
3(* include "Clight/SimplifyCasts.ma". *)  definition simplify_program : clight_program → clight_program ≝ λp.p.
4include "Clight/switchRemoval.ma".
5include "Clight/toCminor.ma".
6include "Cminor/initialisation.ma".
7include "Cminor/toRTLabs.ma".
8
9definition front_end : clight_program → res RTLabs_program ≝
10λp.
11  let p ≝ clight_label p in
12  let p ≝ simplify_program p in
13  let p ≝ program_switch_removal p in
14  ! p ← clight_to_cminor p;
15  cminor_to_rtlabs p.
Note: See TracBrowser for help on using the repository browser.