Changeset 366 for C-semantics/CexecIOcomplete.ma

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:

• C-semantics/CexecIOcomplete.ma (modified) (4 diffs)

C-semantics/CexecIOcomplete.ma

@@ -9 +9 @@
    that one particular one exists corresponding to a derivation in the inductive
    semantics.) *)
-nlet rec yieldsIO (A:Type) (P:A → Prop) (e:IO eventval io_out (Σx:A. P x)) (v:A) on e : Prop ≝
+nlet rec yieldsIO (A:Type) (P:A → Prop) (e:IO io_out io_in (Σx:A. P x)) (v:A) on e : Prop ≝
 match e with
 [ Value v' ⇒ match v' with [ sig_intro v'' _ ⇒ v = v'' ]
@@ -47 +47 @@
 ##] nqed.
 
-nlet rec yieldsIObare (A:Type) (a:IO eventval io_out A) (v':A) on a : Prop ≝
+nlet rec yieldsIObare (A:Type) (a:IO io_out io_in A) (v':A) on a : Prop ≝
 match a with [ Value v ⇒ v' = v | Interact _ k ⇒ ∃r.yieldsIObare A (k r) v' | _ ⇒ False ].
 
 nlemma remove_io_sig: ∀A. ∀P:A → Prop. ∀a,v',p.
 yieldsIObare A a v' →
-yieldsIO A P (io_inject eventval io_out A (λx.P x) (Some ? a) p) v'.
+yieldsIO A P (io_inject io_out io_in A (λx.P x) (Some ? a) p) v'.
 #A P a; nelim a;
 ##[ #a k IH v' p H; nwhd in H ⊢ %; nelim H; #r H'; @ r; napply IH; napply H';
@@ -367 +367 @@
 ##] nqed.
 
-nlemma eventval_match_complete: ∀ev,ty,v.
-  eventval_match ev ty v → yields ?? (check_eventval ev ty) v.
-#ev ty v H; nelim H; //; nqed.
-
 nlemma eventval_match_complete': ∀ev,ty,v.
   eventval_match ev ty v → yields ?? (check_eventval' v ty) ev.
@@ -477 +473 @@
     #H1 H2;
     nelim (yields_eq ???? (eventval_list_match_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
-    nwhd; @ erv; nwhd in ⊢ (??%?);
-    nelim (yields_eq ???? (eventval_match_complete … H2)); #p2 e2; nrewrite > e2; napply refl
+    nwhd; ninversion H2; #x e5 e6 e7; @ x; nwhd in ⊢ (??%?);
+    napply refl
 ##| #v f env k m; nwhd in ⊢ (??%?); napply daemon (* FIXME: inductive semantics allows any value ?! *)
 ##| #v f env k m1 m2 sp loc ofs ty H; nwhd in ⊢ (??%?);