source: Deliverables/D3.1/C-semantics/test/trivial.ma @ 409

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

Update a couple of examples; put support for animation in its own file.

File size: 1.5 KB
Line 
1
2include "Csyntax.ma".
3include "Csem.ma".
4include "Cexec.ma".
5
6ndefinition main : ident ≝ succ_pos_of_nat O.
7naxiom ident_eq_eq: ∀i. ident_eq i i = inl ?? (refl ? i).
8
9ndefinition trivial : program.
10@ [ 〈main, Internal ?〉 ] main [];
11@ (Tint I32 Signed) [ ] [ ] (Sreturn (Some ??));
12@ ? (Tint I32 Signed); napply (Econst_int zero);
13nqed.
14
15nremark 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
38nlemma 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
41nremark trivial_init : ∃s. initial_state trivial s.
42napply (nab ?? (make_initial_state trivial) ? (refl ??));
43nqed.
44
45nremark hacktonormalize : True.
46nletin s ≝ (err_eject ?? (make_initial_state trivial)).
47nnormalize in s.
48//; nqed.
49
50nremark trivial_executes : True.
51nletin ts ≝ (s ← make_initial_state trivial;:
52             exec_steps 10 (globalenv Genv ?? trivial) s);
53nnormalize in ts;
54//; nqed.
Note: See TracBrowser for help on using the repository browser.