Last change
on this file since 125 was
125,
checked in by campbell, 11 years ago

Unify memory space / pointer types.
Implement global variable initialisation and lookup.
Global variables get memory spaces, local variables could be anywhere (for now).

File size:
1.6 KB

Line  

1  include "CexecIO.ma". 

2  

3  ndefinition myprog := mk_program fundef type 

4  [ mk_pair ?? (succ_pos_of_nat 17) (External (succ_pos_of_nat 17) (Tcons (Tint I32 Signed ) Tnil) (Tint I32 Signed )); 

5  mk_pair ?? (succ_pos_of_nat 19) (Internal ( 

6  mk_function (Tint I32 Signed ) [] [mk_pair ?? (succ_pos_of_nat 18) (Tint I32 Signed )] 

7  (Ssequence 

8  (Scall (Some ? (Expr (Evar (succ_pos_of_nat 18)) (Tint I32 Signed ))) 

9  (Expr (Evar (succ_pos_of_nat 17)) (Tfunction (Tcons (Tint I32 Signed ) Tnil) (Tint I32 Signed ))) 

10  [(Expr (Econst_int (repr 10)) (Tint I32 Signed ))]) 

11  (Sreturn (Some ? (Expr (Evar (succ_pos_of_nat 18)) (Tint I32 Signed ))))) 

12  

13  

14  

15  ))] 

16  (succ_pos_of_nat 19) 

17  [] 

18  . 

19  

20  (* not useful :( 

21  notation < "maction ('Interact' T f args 'WHATEVER') ('Interact' T f args k)" with precedence 1 for @{ 'interact $T $f $args $k }. 

22  interpretation "interaction" 'interact T f args k = (Interact T f args k). 

23  *) 

24  

25  (* ndefinition works fine for this, whereas nletin during proof seems to blow up. *) 

26  ndefinition ts ≝ ( 

27  ! s0 ← make_initial_state myprog;: 

28  ! 〈t,s〉 ← exec_steps 7 (globalenv Genv ?? myprog) s0;: 

29  ret ? 〈t,s〉). 

30  

31  ninductive result (T:Type) : T → Prop ≝ 

32   witness : ∀t:T. result T t. 

33  

34  (* The trick to being able to normalize the term is to avoid looking at the 

35  continuations! *) 

36  nremark exec_OK: 

37  match match ts with [ Interact call k ⇒ k (EVint (repr 6)) 

38   Value v ⇒ Wrong ??? 

39   Wrong ⇒ Wrong ??? ] with 

40  [ Interact _ _ ⇒ False 

41   Value v ⇒ result ? v 

42   Wrong ⇒ False 

43  ]. 

44  nnormalize; //; nqed. 

Note: See
TracBrowser
for help on using the repository browser.