Changeset 366 for Csemantics/CexecIOcomplete.ma
 Timestamp:
 Dec 2, 2010, 4:41:43 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/CexecIOcomplete.ma
r365 r366 9 9 that one particular one exists corresponding to a derivation in the inductive 10 10 semantics.) *) 11 nlet rec yieldsIO (A:Type) (P:A → Prop) (e:IO eventval io_out(Σx:A. P x)) (v:A) on e : Prop ≝11 nlet rec yieldsIO (A:Type) (P:A → Prop) (e:IO io_out io_in (Σx:A. P x)) (v:A) on e : Prop ≝ 12 12 match e with 13 13 [ Value v' ⇒ match v' with [ sig_intro v'' _ ⇒ v = v'' ] … … 47 47 ##] nqed. 48 48 49 nlet rec yieldsIObare (A:Type) (a:IO eventval io_outA) (v':A) on a : Prop ≝49 nlet rec yieldsIObare (A:Type) (a:IO io_out io_in A) (v':A) on a : Prop ≝ 50 50 match a with [ Value v ⇒ v' = v  Interact _ k ⇒ ∃r.yieldsIObare A (k r) v'  _ ⇒ False ]. 51 51 52 52 nlemma remove_io_sig: ∀A. ∀P:A → Prop. ∀a,v',p. 53 53 yieldsIObare A a v' → 54 yieldsIO A P (io_inject eventval io_outA (λx.P x) (Some ? a) p) v'.54 yieldsIO A P (io_inject io_out io_in A (λx.P x) (Some ? a) p) v'. 55 55 #A P a; nelim a; 56 56 ##[ #a k IH v' p H; nwhd in H ⊢ %; nelim H; #r H'; @ r; napply IH; napply H'; … … 367 367 ##] nqed. 368 368 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 373 369 nlemma eventval_match_complete': ∀ev,ty,v. 374 370 eventval_match ev ty v → yields ?? (check_eventval' v ty) ev. … … 477 473 #H1 H2; 478 474 nelim (yields_eq ???? (eventval_list_match_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?); 479 nwhd; @ erv; nwhd in ⊢ (??%?);480 n elim (yields_eq ???? (eventval_match_complete … H2)); #p2 e2; nrewrite > e2; napply refl475 nwhd; ninversion H2; #x e5 e6 e7; @ x; nwhd in ⊢ (??%?); 476 napply refl 481 477 ## #v f env k m; nwhd in ⊢ (??%?); napply daemon (* FIXME: inductive semantics allows any value ?! *) 482 478 ## #v f env k m1 m2 sp loc ofs ty H; nwhd in ⊢ (??%?);
Note: See TracChangeset
for help on using the changeset viewer.