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

Add resumption monad based version of the executable semantics with simple I/O.

File size:
1.5 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  (* The trick to being able to normalize the term is to avoid looking at the 

32  continuations! *) 

33  nremark exec_OK: 

34  match match ts with [ Interact f args k ⇒ k (EVint (repr 6)) 

35   Value v ⇒ Wrong ? 

36   Wrong ⇒ Wrong ? ] with 

37  [ Interact _ _ _ ⇒ False 

38   Value v ⇒ v = v 

39   Wrong ⇒ False 

40  ]. 

41  nnormalize; //; nqed. 

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