Changeset 1603 for src/Clight
 Timestamp:
 Dec 13, 2011, 5:37:40 PM (8 years ago)
 Location:
 src/Clight
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/Cexec.ma
r1599 r1603 53 53 54 54 lemma sig_bind_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:res (Sig A P). ∀f:Sig A P → res B. 55 (∀v:A. ∀p:P v. match f ( dpA P v p) with [ Error _ ⇒ True  OK v' ⇒ P' v'] ) →55 (∀v:A. ∀p:P v. match f (mk_Sig A P v p) with [ Error _ ⇒ True  OK v' ⇒ P' v'] ) → 56 56 match bind (Sig A P) B e f with [ Error _ ⇒ True  OK v' ⇒ P' v' ]. 57 57 #A #B #P #P' #e #f elim e; 
src/Clight/CexecComplete.ma
r1566 r1603 12 12 13 13 definition yields_sig : ∀A,P. res (Sig A P) → A → Prop ≝ 14 λA,P,e,v. match e with [ OK v' ⇒ match v' with [ dpv'' _ ⇒ v = v'' ]  _ ⇒ False].14 λA,P,e,v. match e with [ OK v' ⇒ match v' with [ mk_Sig v'' _ ⇒ v = v'' ]  _ ⇒ False]. 15 15 16 16 let rec yieldsIO_sig (A:Type[0]) (P:A → Prop) (e:IO io_out io_in (Sig A P)) (v:A) on e : Prop ≝ 17 17 match e with 18 [ Value v' ⇒ match v' with [ dpv'' _ ⇒ v = v'' ]18 [ Value v' ⇒ match v' with [ mk_Sig v'' _ ⇒ v = v'' ] 19 19  Interact _ k ⇒ ∃r.yieldsIO_sig A P (k r) v 20 20  _ ⇒ False]. … … 33 33 qed. 34 34 35 lemma yields_sig_eq: ∀A,P,e,v. yields_sig A P e v → ∃p. e = OK ? ( dp… v p).35 lemma yields_sig_eq: ∀A,P,e,v. yields_sig A P e v → ∃p. e = OK ? (mk_Sig … v p). 36 36 #A #P #e #v cases e; 37 37 [ #vp cases vp; #v' #p #H whd in H; >H %{ p} @refl
Note: See TracChangeset
for help on using the changeset viewer.