1 | include "Clight/test/sum.c.ma". |
---|

2 | |
---|

3 | example exec: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec myprog 1000 [ ]). |
---|

4 | normalize (* you can examine the result here *) |
---|

5 | @refl |
---|

6 | qed. |
---|

7 | |
---|

8 | include "Clight/SimplifyCasts.ma". |
---|

9 | |
---|

10 | example es: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec (simplify_program myprog) 1000 [ ]). |
---|

11 | normalize (* you can examine the result here *) |
---|

12 | @refl |
---|

13 | qed. |
---|

14 | |
---|

15 | include "Clight/toCminor.ma". |
---|

16 | include "Cminor/semantics.ma". |
---|

17 | |
---|

18 | example e1: finishes_with (repr I32 74) ? |
---|

19 | (bind ? (snapshot state) (clight_to_cminor (simplify_program myprog)) |
---|

20 | (λp. exec_up_to Cminor_fullexec p 1000 [ ])). |
---|

21 | normalize |
---|

22 | @refl |
---|

23 | qed. |
---|

24 | |
---|

25 | include "Cminor/toRTLabs.ma". |
---|

26 | include "RTLabs/semantics.ma". |
---|

27 | |
---|

28 | example e2: finishes_with (repr I32 74) ? ( |
---|

29 | bind ? (snapshot state) (clight_to_cminor (simplify_program myprog)) |
---|

30 | (λp1. bind ? (snapshot state) (cminor_to_rtlabs p1) |
---|

31 | (λp2. exec_up_to RTLabs_fullexec p2 1000 [ ]))). |
---|

32 | normalize |
---|

33 | @refl |
---|

34 | qed. |
---|

35 | |
---|

36 | include "RTLabs/RTLabsToRTL.ma". |
---|

37 | include alias "basics/lists/list.ma". |
---|

38 | |
---|

39 | definition take_out: ∀A. res A → A ≝ |
---|

40 | λA,a. match a with [ OK x ⇒ x | Error _ ⇒ ?]. |
---|

41 | cases daemon |
---|

42 | qed. |
---|

43 | |
---|

44 | example CSC: True. |
---|

45 | letin xxx ≝ |
---|

46 | (let p ≝ take_out … (clight_to_cminor myprog) in |
---|

47 | let p ≝ take_out … (cminor_to_rtlabs p) in |
---|

48 | (* (map … (λx. match (\snd x) with [External _ ⇒ ? | Internal f ⇒ f_graph … f]) (prog_funct … p)) *) |
---|

49 | let p ≝ rtlabs_to_rtl p in |
---|

50 | (map … (λx. match (\snd x) with [External _ ⇒ ? | Internal f ⇒ joint_if_code … f]) (prog_funct … p)) |
---|

51 | ) |
---|

52 | [2: cases daemon] |
---|

53 | normalize in xxx; |
---|

54 | |
---|

55 | |
---|

56 | [2: |
---|

57 | OK (list (codeT (prog_var_names … p) (rtl_params (prog_var_names … p)))) (list_map … (λx. match (\snd x) return λ_.codeT (prog_var_names … p) (rtl_params ?) with [External _ ⇒ ? | Internal f ⇒ ?(*joint_if_code ? (rtl_params ?) f*)]) (prog_funct … p))) |
---|

58 | (* OK ? (map … (λx. match (\snd x) with [External _ ⇒ ? | Internal f ⇒ f_graph … f]) (prog_funct … p))) |
---|

59 | *) |
---|

60 | [2: check (joint_if_code (prog_var_names … p) ? f) |3: cases daemon ] |
---|

61 | normalize in xxx |
---|

62 | |
---|