Last change
on this file since 350 was
9,
checked in by campbell, 11 years ago
|
Enough of an executable semantics to execute a not-quite-trivial program,
plus a patch for compcert to convert C to a matita definition.
|
File size:
1.5 KB
|
Line | |
---|
1 | |
---|
2 | include "Csyntax.ma". |
---|
3 | include "Csem.ma". |
---|
4 | include "Cexec.ma". |
---|
5 | |
---|
6 | ndefinition main : ident ≝ O. |
---|
7 | naxiom ident_eq_eq: ∀i. ident_eq i i = inl ?? (refl ? i). |
---|
8 | |
---|
9 | ndefinition trivial : program. |
---|
10 | @ [ 〈main, Internal ?〉 ] main []; |
---|
11 | @ (Tint I32 Signed) [ ] [ ] (Sreturn (Some ??)); |
---|
12 | @ ? (Tint I32 Signed); napply (Econst_int zero); |
---|
13 | nqed. |
---|
14 | |
---|
15 | nremark trivial_behaves : ∃behaviour. exec_program trivial behaviour. |
---|
16 | @; ##[ ##2: |
---|
17 | napply program_terminates; |
---|
18 | ##[ ##5: @; (* initial state *) |
---|
19 | ##[ ##3: nnormalize; nrewrite > (ident_eq_eq ?); //; |
---|
20 | ##| ##4: nnormalize; //; |
---|
21 | ##| ##*: ##skip |
---|
22 | ##] |
---|
23 | ##| ##6: |
---|
24 | @2; ##[ ##4: napply step_internal_function; |
---|
25 | ##[ ##4: napply alloc_variables_nil; ##| ##5: napply bind_parameters_nil; ##| ##*: ##skip ##] |
---|
26 | ##| ##5: @2; |
---|
27 | ##[ ##4: napply step_return_1; //; napply nmk; #H; ndestruct; |
---|
28 | ##| ##5: @1; |
---|
29 | ##| ##6: //; |
---|
30 | ##| ##*: ##skip ##] |
---|
31 | ##| ##6: //; |
---|
32 | ##| ##*: ##skip |
---|
33 | ##] |
---|
34 | ##| ##7: @; |
---|
35 | ##] |
---|
36 | ##] nqed. |
---|
37 | |
---|
38 | nlemma nab : ∀A,P,e,v. e = OK (Σv:A.P v) v → ∃v:A. P v. |
---|
39 | #A P e v; ncases v; /2/; nqed. |
---|
40 | |
---|
41 | nremark trivial_init : ∃s. initial_state trivial s. |
---|
42 | napply (nab ?? (make_initial_state trivial) ? (refl ??)); |
---|
43 | nqed. |
---|
44 | |
---|
45 | nremark hacktonormalize : True. |
---|
46 | nletin s ≝ (err_eject ?? (make_initial_state trivial)). |
---|
47 | nnormalize in s. |
---|
48 | //; nqed. |
---|
49 | |
---|
50 | nremark trivial_executes : True. |
---|
51 | nletin ts ≝ (s ← make_initial_state trivial;: |
---|
52 | exec_steps 10 (globalenv Genv ?? trivial) s); |
---|
53 | nnormalize in ts; |
---|
54 | //; nqed. |
---|
Note: See
TracBrowser
for help on using the repository browser.