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/io2.c.ma

    r227 r366  
    3939| witness : ∀t:T. result T t.
    4040
     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
    4147(* The trick to being able to normalize the term is to avoid looking at the
    4248   continuations! *)
    4349nremark foo:
    44     match match s with [ Interact call k ⇒ k (EVint (repr 10))
     50    match match s with [ Interact call k ⇒ do_int call k (repr 10)
    4551                 | Value v ⇒ Wrong ???
    4652                 | Wrong ⇒ Wrong ??? ] with
Note: See TracChangeset for help on using the changeset viewer.