source: src/Cminor/test/factorial.test.ma @ 1680

Last change on this file since 1680 was 1633, checked in by campbell, 8 years ago

Update Cminor pretty printer and examples.

File size: 505 bytes
Line 
1include "Cminor/test/factorial.Cminor.ma".
2
3example exec: finishes_with (repr 120) ? (exec_up_to Cminor_fullexec myprog 100 [EVint I32 (repr 5)]).
4normalize  (* you can examine the result here *)
5@refl qed.
6
7include "Cminor/toRTLabs.ma".
8include "RTLabs/semantics.ma".
9
10example execRTL: finishes_with (repr 120) ?
11 (bind ? (snapshot state) (cminor_to_rtlabs myprog)
12  (λmyprog'. exec_up_to RTLabs_fullexec myprog' 1000 [EVint I32 (repr 5)])).
13normalize  (* you can examine the result here *)
14@refl
15qed.
16
Note: See TracBrowser for help on using the repository browser.