Ignore:
Timestamp:
Dec 2, 2010, 4:41:43 PM (9 years ago)
Author:
campbell
Message:

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/test/io.c.ma

    r125 r366  
    2525(* ndefinition works fine for this, whereas nletin during proof seems to blow up. *)
    2626ndefinition ts ≝ (
    27  ! s0 ← make_initial_state myprog;:
    28  ! 〈t,s〉 ← exec_steps 7 (globalenv Genv ?? myprog) s0;:
     27 ! s0 ← make_initial_state myprog;
     28 ! 〈t,s〉 ← exec_steps 7 (globalenv Genv ?? myprog) s0;
    2929   ret ? 〈t,s〉).
    3030
     
    3232| witness : ∀t:T. result T t.
    3333
     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
    3440(* The trick to being able to normalize the term is to avoid looking at the
    3541   continuations! *)
    3642nremark exec_OK:
    37     match match ts with [ Interact call k ⇒ k (EVint (repr 6))
     43    match match ts with [ Interact call k ⇒ do_int ? call k (repr 6)
    3844                 | Value v ⇒ Wrong ???
    3945                 | Wrong ⇒ Wrong ??? ] with
Note: See TracChangeset for help on using the changeset viewer.