source: src/Clight/test/transform1.ma @ 725

Last change on this file since 725 was 725, checked in by campbell, 9 years ago

Do some light manual disambiguation to make Clight examples go through more
easily.

File size: 3.7 KB
Line 
1(*
2include "Csyntax.ma".
3include "AST.ma".
4
5nlet rec skippy_s (s:statement) : statement ≝
6match s with
7[ Ssequence s1 s2 ⇒ Ssequence (skippy_s s1) (skippy_s s2)
8| Scall _ _ _ ⇒ Ssequence Sskip s
9| _ ⇒ s
10].
11
12ndefinition skippy_f : function → function ≝ λf.
13mk_function
14  (fn_return f)
15  (fn_params f)
16  (fn_vars f)
17  (skippy_s (fn_body f)).
18
19ndefinition skippy_fd : fundef → fundef ≝ λf.
20match f with
21[ CL_Internal fd ⇒ Internal (skippy_f fd)
22| CL_External id args res ⇒ External id args res
23].
24
25ndefinition skippy : program → program ≝ transform_program … skippy_fd.
26nremark rewrite_skippy : skippy = transform_program … skippy_fd.
27//; nqed.
28(*
29ndefinition skippy : program → program ≝
30λp.
31mk_program ??
32  (map ?? (λfd. match snd ?? fd with
33             [ CL_Internal f ⇒
34               〈fst ?? fd,
35                CL_Internal
36                 (mk_function (fn_return f) (fn_params f) (fn_vars f) (skippy_s (fn_body f)))〉
37             | CL_External _ _ _ ⇒ fd ])
38    (prog_funct ?? p))
39  (prog_main ?? p)
40  (prog_vars ?? p).
41*)
42include "SmallstepExec.ma".
43include "CexecIO.ma".
44
45ndefinition Csem ≝ λp:program.mk_execstep
46  ?
47  ?
48  ?
49  ?
50  (initial_state p)
51  final_state
52  exec_step.
53
54nlet rec skippy_k (k:cont) : cont ≝
55match k with
56[ Kstop ⇒ Kstop
57| Kseq s k' ⇒ Kseq (skippy_s s) (skippy_k k')
58| Kwhile e s k' ⇒ Kwhile e (skippy_s s) (skippy_k k')
59| Kdowhile e s k' ⇒ Kdowhile e (skippy_s s) (skippy_k k')
60| Kfor2 e s1 s2 k' ⇒ Kfor2 e (skippy_s s1) (skippy_s s2) (skippy_k k')
61| Kfor3 e s1 s2 k' ⇒ Kfor3 e (skippy_s s1) (skippy_s s2) (skippy_k k')
62| Kswitch k' ⇒ Kswitch (skippy_k k')
63| Kcall r f e k' ⇒ Kcall r f e (skippy_k k')
64].
65
66
67include "Plogic/equality.ma".
68include "Plogic/connectives.ma".
69
70ndefinition skippy_state : state → state ≝ λs:state.
71match s with
72[ State f s k e m ⇒ State (skippy_f f) (skippy_s s) (skippy_k k) e m
73| Callstate fd args k m ⇒ Callstate (skippy_fd fd) args (skippy_k k) m
74| Returnstate res k m ⇒ Returnstate res (skippy_k k) m
75].
76(*
77ndefinition skippyeq : state → state → Prop ≝ λs,s':state.
78match s with
79[ State f s k e m ⇒
80  match s' with
81  [ State f' s' k' e' m' ⇒ (skippy_f f) = f' ∧ (skippy_s s) = s' ∧ (skippy_k k) = k' ∧ m = m'
82  | _ ⇒ False
83  ]
84| Callstate fd args k m ⇒
85  match s' with
86  [ Callstate fd' args' k' m' ⇒ (skippy_fd fd) = fd' ∧ args = args' ∧ (skippy_k k) = k' ∧ m = m'
87  | _ ⇒ False
88  ]
89| Returnstate res k m ⇒
90  match s' with
91  [ Returnstate res' k' m' ⇒ res = res' ∧ (skippy_k k) = k' ∧ m = m'
92  | _ ⇒ False
93  ]
94].
95*)
96ndefinition skippy_eq : state → state → Prop ≝ λs,s':state. (skippy_state s) = s'.
97
98ndefinition skippysim ≝ λp:program.
99mk_simulation
100  (mk_related_semantics
101    (Csem p)
102    (Csem (skippy p))
103    (globalenv Genv ?? p)
104    (globalenv Genv ?? (skippy p))
105    ?
106    ?
107    ?)
108  ?.
109##[ ##3: napply skippy_eq;
110##| #st1 st2 r e H; ninversion H; #i m e1 e2; ndestruct; //;
111##| #st1 H; ninversion H; #b f H1 H2 e1; @ (skippy_state st1);
112    nrewrite > e1; @; //;
113    nwhd; nwhd in ⊢ (??%); napply (initial_state_intro … b);
114    nrewrite > rewrite_skippy;
115    ##[ nrewrite > (find_symbol_transf Genv …); napply H1;
116    ##| nrewrite > (find_funct_ptr_transf Genv …); //;
117    ##]
118##| #st1 st2 t st1' H e;
119    @ (skippy_state st1');
120    @; //;
121    (* simulation proof *)
122    (* First, get a hold of the states being executed. *)
123    nelim st1 in H e ⊢ %;
124    ##[ #f1 s1 k1 e1 m1; nelim s1;
125     ##[ nelim k1;
126       ##[ nelim f1; #ty args vars body; ncases ty;
127         ##[ #H e; nwhd in H;
128             nnormalize in e; @ (1); nrewrite < e; nwhd; ndestruct; //;
129         ##| ##2,5,6,7,8: #A B H; nwhd in H; napply (False_ind … H);
130         ##| ##3,4,9: #A H; nwhd in H; napply (False_ind … H);
131         ##]
132       ##|
133
134*)
Note: See TracBrowser for help on using the repository browser.