source: C-semantics/test/io.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: 1.9 KB
Line 
1include "CexecIO.ma".
2
3ndefinition 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 :(
21notation < "maction ('Interact' T f args 'WHATEVER') ('Interact' T f args k)" with precedence 1 for @{ 'interact $T $f $args $k }.
22interpretation "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. *)
26ndefinition ts ≝ (
27 ! s0 ← make_initial_state myprog;
28 ! 〈t,s〉 ← exec_steps 7 (globalenv Genv ?? myprog) s0;
29   ret ? 〈t,s〉).
30
31ninductive result (T:Type) : T → Prop ≝
32| witness : ∀t:T. result T t.
33
34ndefinition do_int : ∀T:Type.∀o:io_out. (io_in o → IO io_out io_in T) → int → IO io_out io_in T ≝
35λT,o,k,i. (match io_in_typ o return λt'.(eventval_type t' → IO io_out io_in T) → IO io_out io_in T with
36[ Tint ⇒ λk'.k' i
37| Tfloat ⇒ λk'.Wrong ???
38]) k.
39
40(* The trick to being able to normalize the term is to avoid looking at the
41   continuations! *)
42nremark exec_OK:
43    match match ts with [ Interact call k ⇒ do_int ? call k (repr 6)
44                 | Value v ⇒ Wrong ???
45                 | Wrong ⇒ Wrong ??? ] with
46    [ Interact _ _ ⇒ False
47    | Value v ⇒ result ? v
48    | Wrong ⇒ False
49    ].
50nnormalize; //; nqed.
Note: See TracBrowser for help on using the repository browser.