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/CexecIOcomplete.ma

    r365 r366  
    99   that one particular one exists corresponding to a derivation in the inductive
    1010   semantics.) *)
    11 nlet rec yieldsIO (A:Type) (P:A → Prop) (e:IO eventval io_out (Σx:A. P x)) (v:A) on e : Prop ≝
     11nlet rec yieldsIO (A:Type) (P:A → Prop) (e:IO io_out io_in (Σx:A. P x)) (v:A) on e : Prop ≝
    1212match e with
    1313[ Value v' ⇒ match v' with [ sig_intro v'' _ ⇒ v = v'' ]
     
    4747##] nqed.
    4848
    49 nlet rec yieldsIObare (A:Type) (a:IO eventval io_out A) (v':A) on a : Prop ≝
     49nlet rec yieldsIObare (A:Type) (a:IO io_out io_in A) (v':A) on a : Prop ≝
    5050match a with [ Value v ⇒ v' = v | Interact _ k ⇒ ∃r.yieldsIObare A (k r) v' | _ ⇒ False ].
    5151
    5252nlemma remove_io_sig: ∀A. ∀P:A → Prop. ∀a,v',p.
    5353yieldsIObare A a v' →
    54 yieldsIO A P (io_inject eventval io_out A (λx.P x) (Some ? a) p) v'.
     54yieldsIO A P (io_inject io_out io_in A (λx.P x) (Some ? a) p) v'.
    5555#A P a; nelim a;
    5656##[ #a k IH v' p H; nwhd in H ⊢ %; nelim H; #r H'; @ r; napply IH; napply H';
     
    367367##] nqed.
    368368
    369 nlemma eventval_match_complete: ∀ev,ty,v.
    370   eventval_match ev ty v → yields ?? (check_eventval ev ty) v.
    371 #ev ty v H; nelim H; //; nqed.
    372 
    373369nlemma eventval_match_complete': ∀ev,ty,v.
    374370  eventval_match ev ty v → yields ?? (check_eventval' v ty) ev.
     
    477473    #H1 H2;
    478474    nelim (yields_eq ???? (eventval_list_match_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
    479     nwhd; @ erv; nwhd in ⊢ (??%?);
    480     nelim (yields_eq ???? (eventval_match_complete … H2)); #p2 e2; nrewrite > e2; napply refl
     475    nwhd; ninversion H2; #x e5 e6 e7; @ x; nwhd in ⊢ (??%?);
     476    napply refl
    481477##| #v f env k m; nwhd in ⊢ (??%?); napply daemon (* FIXME: inductive semantics allows any value ?! *)
    482478##| #v f env k m1 m2 sp loc ofs ty H; nwhd in ⊢ (??%?);
Note: See TracChangeset for help on using the changeset viewer.