source: C-semantics/test/io2.c.ma @ 366

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

Make I/O type safe, removing a discrepancy between the executable and
inductive semantics.

File size: 2.2 KB
Line 
1include "CexecIO.ma".
2
3ndefinition myprog := mk_program fundef type
4  [
5  mk_pair ?? (succ_pos_of_nat 17) (External (succ_pos_of_nat 17) (Tcons (Tint I32 Signed  ) Tnil) (Tint I32 Signed  ));
6  mk_pair ?? (succ_pos_of_nat 20) (Internal (
7    mk_function (Tint I32 Signed  ) [] [mk_pair ?? (succ_pos_of_nat 18) (Tint I32 Signed  ); mk_pair ?? (succ_pos_of_nat 19) (Tint I32 Signed  )]
8      (Ssequence
9      (Sassign (Expr (Evar (succ_pos_of_nat 18)) (Tint I32 Signed  ))
10        (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
11      (Ssequence
12      (Ssequence
13      (Scall (Some ? (Expr (Evar (succ_pos_of_nat 19)) (Tint I32 Signed  )))
14        (Expr (Evar (succ_pos_of_nat 17)) (Tfunction (Tcons (Tint I32 Signed  ) Tnil) (Tint I32 Signed  )))
15        [(Expr (Econst_int (repr 10)) (Tint I32 Signed  ))])
16      (Sassign (Expr (Evar (succ_pos_of_nat 18)) (Tint I32 Signed  ))
17        (Expr (Ebinop Oadd
18          (Expr (Evar (succ_pos_of_nat 18)) (Tint I32 Signed  ))
19          (Expr (Evar (succ_pos_of_nat 19)) (Tint I32 Signed  ))) (Tint I32 Signed  ))))
20      (Sreturn (Some ? (Expr (Evar (succ_pos_of_nat 18)) (Tint I32 Signed  ))))))
21   
22   
23   
24  ))]
25  (succ_pos_of_nat 20)
26  []
27.
28
29(* ndefinition works fine for this, whereas nletin during proof seems to blow up. *)
30ndefinition s ≝ (
31 ! s0 ← make_initial_state myprog;
32 ! 〈t,s〉 ← exec_steps 13 (globalenv Genv ?? myprog) s0;
33   ret ? s).
34
35notation < "'MEM'" with precedence 1 for @{ 'mem }.
36interpretation "hide memory" 'mem = (mk_mem ???).
37
38ninductive result (T:Type) : T → Prop ≝
39| witness : ∀t:T. result T t.
40
41ndefinition do_int : ∀o:io_out. (io_in o → IO io_out io_in state) → int → IO io_out io_in state ≝
42λo,k,i. (match io_in_typ o return λt'.(eventval_type t' → IO io_out io_in state) → IO io_out io_in state with
43[ Tint ⇒ λk'.k' i
44| Tfloat ⇒ λk'.Wrong ???
45]) k.
46
47(* The trick to being able to normalize the term is to avoid looking at the
48   continuations! *)
49nremark foo:
50    match match s with [ Interact call k ⇒ do_int call k (repr 10)
51                 | Value v ⇒ Wrong ???
52                 | Wrong ⇒ Wrong ??? ] with
53    [ Interact _ _ ⇒ False
54    | Value v ⇒ result ? v
55    | Wrong ⇒ False
56    ].
57nnormalize; //; nqed.
Note: See TracBrowser for help on using the repository browser.