Ignore:
Timestamp:
Jun 21, 2010, 4:22:09 PM (10 years ago)
Author:
campbell
Message:

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:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/test/trivial.ma

    r3 r9  
    22include "Csyntax.ma".
    33include "Csem.ma".
     4include "Cexec.ma".
    45
    5 naxiom main : ident.
     6ndefinition main : ident ≝ O.
    67naxiom ident_eq_eq: ∀i. ident_eq i i = inl ?? (refl ? i).
    78
     
    1415nremark trivial_behaves : ∃behaviour. exec_program trivial behaviour.
    1516@; ##[ ##2:
    16   napply program_terminates;
     17  napply program_terminates; 
    1718  ##[ ##5: @; (* initial state *)
    1819    ##[ ##3: nnormalize; nrewrite > (ident_eq_eq ?); //;
     
    2223  ##| ##6:
    2324    @2; ##[ ##4: napply step_internal_function;
    24           ##[ ##4: //;  ##| ##5: //; ##| ##*: ##skip ##]
     25          ##[ ##4: napply alloc_variables_nil; ##| ##5: napply bind_parameters_nil; ##| ##*: ##skip ##]
    2526        ##| ##5: @2;
    2627          ##[ ##4: napply step_return_1; //; napply nmk; #H; ndestruct;
     
    3536##] nqed.
    3637
     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 TracChangeset for help on using the changeset viewer.