source: C-semantics/test/transform1.ma @ 24

Last change on this file since 24 was 24, checked in by campbell, 10 years ago

Separate out IOMonad from the rest of the executable semantics.
Start adding simulation results.

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[ Internal fd ⇒ Internal (skippy_f fd)
22| 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             [ Internal f ⇒
34               〈fst ?? fd,
35                Internal
36                 (mk_function (fn_return f) (fn_params f) (fn_vars f) (skippy_s (fn_body f)))〉
37             | 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  (initial_state p)
50  final_state
51  exec_step.
52
53nlet rec skippy_k (k:cont) : cont ≝
54match k with
55[ Kstop ⇒ Kstop
56| Kseq s k' ⇒ Kseq (skippy_s s) (skippy_k k')
57| Kwhile e s k' ⇒ Kwhile e (skippy_s s) (skippy_k k')
58| Kdowhile e s k' ⇒ Kdowhile e (skippy_s s) (skippy_k k')
59| Kfor2 e s1 s2 k' ⇒ Kfor2 e (skippy_s s1) (skippy_s s2) (skippy_k k')
60| Kfor3 e s1 s2 k' ⇒ Kfor3 e (skippy_s s1) (skippy_s s2) (skippy_k k')
61| Kswitch k' ⇒ Kswitch (skippy_k k')
62| Kcall r f e k' ⇒ Kcall r f e (skippy_k k')
63].
64
65
66include "Plogic/equality.ma".
67include "Plogic/connectives.ma".
68
69ndefinition skippy_state : state → state ≝ λs:state.
70match s with
71[ State f s k e m ⇒ State (skippy_f f) (skippy_s s) (skippy_k k) e m
72| Callstate fd args k m ⇒ Callstate (skippy_fd fd) args (skippy_k k) m
73| Returnstate res k m ⇒ Returnstate res (skippy_k k) m
74].
75(*
76ndefinition skippyeq : state → state → Prop ≝ λs,s':state.
77match s with
78[ State f s k e m ⇒
79  match s' with
80  [ State f' s' k' e' m' ⇒ (skippy_f f) = f' ∧ (skippy_s s) = s' ∧ (skippy_k k) = k' ∧ m = m'
81  | _ ⇒ False
82  ]
83| Callstate fd args k m ⇒
84  match s' with
85  [ Callstate fd' args' k' m' ⇒ (skippy_fd fd) = fd' ∧ args = args' ∧ (skippy_k k) = k' ∧ m = m'
86  | _ ⇒ False
87  ]
88| Returnstate res k m ⇒
89  match s' with
90  [ Returnstate res' k' m' ⇒ res = res' ∧ (skippy_k k) = k' ∧ m = m'
91  | _ ⇒ False
92  ]
93].
94*)
95ndefinition skippy_eq : state → state → Prop ≝ λs,s':state. (skippy_state s) = s'.
96
97ndefinition skippysim ≝ λp:program.
98mk_simulation
99  (mk_related_semantics
100    (Csem p)
101    (Csem (skippy p))
102    (globalenv Genv ?? p)
103    (globalenv Genv ?? (skippy p))
104    ?
105    ?
106    ?)
107  ?.
108##[ ##3: napply skippy_eq;
109##| #st1 st2 r e H; ninversion H; #i m e1 e2; ndestruct; //;
110##| #st1 H; ninversion H; #b f H1 H2 e1; @ (skippy_state st1);
111    nrewrite > e1; @; //;
112    nwhd; nwhd in ⊢ (??%); napply (initial_state_intro … b);
113    nrewrite > rewrite_skippy;
114    ##[ nrewrite > (find_symbol_transf Genv …); napply H1;
115    ##| nrewrite > (find_funct_ptr_transf Genv …); //;
116    ##]
117##| #st1 st2 t st1' H e;
118    @ (skippy_state st1');
119    @; //;
120    (* simulation proof *)
121    (* First, get a hold of the states being executed. *)
122    nelim st1 in H e ⊢ %;
123    ##[ #f1 s1 k1 e1 m1; nelim s1;
124     ##[ nelim k1;
125       ##[ nelim f1; #ty args vars body; ncases ty;
126         ##[ #H e; nwhd in H;
127             nnormalize in e; @ (1); nrewrite < e; nwhd; ndestruct; //;
128         ##| ##2,5,6,7,8: #A B H; nwhd in H; napply (False_ind … H);
129         ##| ##3,4,9: #A H; nwhd in H; napply (False_ind … H);
130         ##]
131       ##|
Note: See TracBrowser for help on using the repository browser.