Changeset 9 for Csemantics/test/trivial.ma
 Timestamp:
 Jun 21, 2010, 4:22:09 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/test/trivial.ma
r3 r9 2 2 include "Csyntax.ma". 3 3 include "Csem.ma". 4 include "Cexec.ma". 4 5 5 n axiom main : ident.6 ndefinition main : ident ≝ O. 6 7 naxiom ident_eq_eq: ∀i. ident_eq i i = inl ?? (refl ? i). 7 8 … … 14 15 nremark trivial_behaves : ∃behaviour. exec_program trivial behaviour. 15 16 @; ##[ ##2: 16 napply program_terminates; 17 napply program_terminates; 17 18 ##[ ##5: @; (* initial state *) 18 19 ##[ ##3: nnormalize; nrewrite > (ident_eq_eq ?); //; … … 22 23 ## ##6: 23 24 @2; ##[ ##4: napply step_internal_function; 24 ##[ ##4: //; ## ##5: //; ## ##*: ##skip ##]25 ##[ ##4: napply alloc_variables_nil; ## ##5: napply bind_parameters_nil; ## ##*: ##skip ##] 25 26 ## ##5: @2; 26 27 ##[ ##4: napply step_return_1; //; napply nmk; #H; ndestruct; … … 35 36 ##] nqed. 36 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 TracChangeset
for help on using the changeset viewer.