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

Last change on this file since 779 was 725, checked in by campbell, 10 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.