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

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