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

Enough of an executable semantics to execute a notquitetrivial 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.