Changeset 366


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.

Location:
C-semantics
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r321 r366  
    781781##] nqed.
    782782
    783 (* IO monad *)
    784 
    785 (* Interactions are function calls that return a value and do not change
    786    the rest of the Clight program's state. *)
    787 ndefinition io_out ≝ (ident × (list eventval)).
    788 
    789 ndefinition do_io : ident → list eventval → IO eventval io_out eventval ≝
    790 λfn,args. Interact ?? eventval 〈fn,args〉 (λres. Value ?? eventval res).
    791 
    792 ndefinition ret: ∀T. T → (IO eventval io_out T) ≝
    793 λT,x.(Value ?? T x).
    794 
    795783(* Checking types of values given to / received from an external function call. *)
    796784
    797 ndefinition check_eventval : ∀ev:eventval. ∀ty:typ. res (Σv:val. eventval_match ev ty v) ≝
     785ndefinition eventval_type : ∀ty:typ. Type ≝
     786λty. match ty with [ Tint ⇒ int | Tfloat ⇒ float ].
     787
     788ndefinition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝
     789λty:typ. match ty return λty'.eventval_type ty' → eventval with [ Tint ⇒ λv.EVint v | Tfloat ⇒ λv.EVfloat v ].
     790
     791ndefinition mk_val: ∀ty:typ. eventval_type ty → val ≝
     792λty:typ. match ty return λty'.eventval_type ty' → val with [ Tint ⇒ λv.Vint v | Tfloat ⇒ λv.Vfloat v ].
     793
     794nlemma mk_val_correct: ∀ty:typ. ∀v:eventval_type ty.
     795  eventval_match (mk_eventval ty v) ty (mk_val ty v).
     796#ty; ncases ty; nnormalize; //; nqed.
     797
     798ndefinition convert_eventval : ∀ev:eventval. ∀ty:typ. res (Σv:val. eventval_match ev ty v) ≝
    798799λev,ty.
    799800match ty with
     
    828829nqed.
    829830
     831(* IO monad *)
     832
     833(* Interactions are function calls that return a value and do not change
     834   the rest of the Clight program's state. *)
     835nrecord io_out : Type ≝
     836{ io_function: ident
     837; io_args: list eventval
     838; io_in_typ: typ
     839}.
     840
     841ndefinition io_in ≝ λo. eventval_type (io_in_typ o).
     842
     843ndefinition do_io : ident → list eventval → ∀t:typ. IO io_out io_in (eventval_type t) ≝
     844λfn,args,t. Interact ??? (mk_io_out fn args t) (λres. Value ??? res).
     845
     846ndefinition ret: ∀T. T → (IO io_out io_in T) ≝
     847λT,x.(Value ?? T x).
     848
    830849(* execution *)
    831850
     
    836855    store_value_of_type ty m pcl loc ofs v ] ].
    837856
    838 nlet rec exec_step (ge:genv) (st:state) on st : (IO eventval io_out (trace × state)) ≝
     857nlet rec exec_step (ge:genv) (st:state) on st : (IO io_out io_in (trace × state)) ≝
    839858match st with
    840859[ State f s k e m ⇒
     
    966985  | External f argtys retty ⇒
    967986      ! evargs ← err_to_io_sig … (check_eventval_list vargs (typlist_of_typelist argtys));
    968       ! evres ← do_io f evargs;
    969       ! vres ← err_to_io_sig … (check_eventval evres (proj_sig_res (signature_of_type argtys retty)));
    970       ret ? 〈(Eextcall f evargs evres), Returnstate vres k m〉
     987      ! evres ← do_io f evargs (proj_sig_res (signature_of_type argtys retty));
     988      ret ? 〈Eextcall f evargs (mk_eventval ? evres), Returnstate (mk_val ? evres) k m〉
    971989  ]
    972990| Returnstate res k m ⇒
     
    11131131    nwhd; napply (step_internal_function … Halloc Hbind);
    11141132  ##| #id argtys rty; napply sig_bindIO_OK; #evs Hevs;
    1115     napply bindIO_OK; #eres;
    1116     napply sig_bindIO_OK; #res Hres;
    1117     nwhd; napply step_external_function; @; ##[ napply Hevs; ##| napply Hres; ##]
     1133    napply bindIO_OK; #eres; nwhd;
     1134    napply step_external_function; @; ##[ napply Hevs; ##| napply mk_val_correct; ##]
    11181135  ##] 
    11191136##| #v k' m'; nwhd in ⊢ (?????%); ncases k'; //;
     
    11261143nqed.
    11271144
    1128 nlet rec make_initial_state (p:program) : IO eventval io_out state ≝
     1145nlet rec make_initial_state (p:program) : IO io_out io_in state ≝
    11291146  let ge ≝ globalenv Genv ?? p in
    11301147  let m0 ≝ init_mem Genv ?? p in
     
    11631180
    11641181nlet rec exec_steps (n:nat) (ge:genv) (s:state) :
    1165  IO eventval io_out (trace×state) ≝
     1182 IO io_out io_in (trace×state) ≝
    11661183match is_final_state s with
    11671184[ inl _ ⇒ ret ? 〈E0, s〉
     
    12251242| e_step : trace → state → execution → execution
    12261243| e_wrong : execution
    1227 | e_interact : io_out → (eventval → execution) → execution.
     1244| e_interact : ∀o:io_out. (io_in o → execution) → execution.
    12281245
    12291246ndefinition mem_of_state : state → mem ≝
     
    12341251   state. *)
    12351252
    1236 nlet corec exec_inf_aux (ge:genv) (s:IO eventval io_out (trace×state)) : execution ≝
     1253nlet corec exec_inf_aux (ge:genv) (s:IO io_out io_in (trace×state)) : execution ≝
    12371254match s with
    12381255[ Wrong ⇒ e_wrong
     
    13091326    execution_isteps tr' s e s' e' →
    13101327    execution_isteps (tr⧺tr') s0 (e_step tr s e) s' e'
    1311 | isteps_interact : ∀e,e',k,o,i,s,s',s0,tr,tr'.
     1328| isteps_interact : ∀e,e',o,k,i,s,s',s0,tr,tr'.
    13121329    execution_isteps tr' s e s' e' →
    13131330    k i = e_step tr s e →
     
    13781395    ##| #E EXEC'; nwhd in EXEC':(??%?); ndestruct (EXEC');
    13791396    ##]
    1380 ##| #e e' k o i s s' s0 tr tr' H1 H2 H3 IH;
     1397##| #e e' o k i s s' s0 tr tr' H1 H2 H3 IH;
    13811398    nrewrite > (exec_inf_aux_unfold ge ?); nwhd in ⊢ (??%? → ?);
    13821399    ncases (is_final_state s0); #FINAL EXEC; nwhd in EXEC:(??%?); ndestruct;
  • 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 ⊢ (??%?);
  • C-semantics/IOMonad.ma

    r252 r366  
    55(* IO monad *)
    66
    7 ninductive IO (input,output:Type) (T:Type) : Type ≝
    8 | Interact : output → (input → IO input output T) → IO input output T
    9 | Value : T → IO input output T
    10 | Wrong : IO input output T.
     7ninductive IO (output:Type) (input:output → Type) (T:Type) : Type ≝
     8| Interact : ∀o:output. (input o → IO output input T) → IO output input T
     9| Value : T → IO output input T
     10| Wrong : IO output input T.
    1111
    12 nlet rec bindIO (I,O,T,T':Type) (v:IO I O T) (f:T → IO I O T') on v : IO I O T' ≝
     12nlet rec bindIO (O:Type) (I:O → Type) (T,T':Type) (v:IO O I T) (f:T → IO O I T') on v : IO O I T' ≝
    1313match v with
    14 [ Interact out k ⇒ (Interact ??? out (λres. bindIO I O T T' (k res) f))
     14[ Interact out k ⇒ (Interact ??? out (λres. bindIO O I T T' (k res) f))
    1515| Value v' ⇒ (f v')
    16 | Wrong ⇒ Wrong I O T'
     16| Wrong ⇒ Wrong O I T'
    1717].
    1818
    19 nlet rec bindIO2 (I,O,T1,T2,T':Type) (v:IO I O (T1×T2)) (f:T1 → T2 → IO I O T') on v : IO I O T' ≝
     19nlet rec bindIO2 (O:Type) (I:O → Type) (T1,T2,T':Type) (v:IO O I (T1×T2)) (f:T1 → T2 → IO O I T') on v : IO O I T' ≝
    2020match v with
    2121[ Interact out k ⇒ (Interact ??? out (λres. bindIO2 ?? T1 T2 T' (k res) f))
     
    2424].
    2525
    26 ndefinition err_to_io : ∀I,O,T. res T → IO I O T ≝
    27 λI,O,T,v. match v with [ OK v' ⇒ Value I O T v' | Error ⇒ Wrong I O T ].
    28 ncoercion err_to_io : ∀I,O,A.∀c:res A.IO I O A ≝ err_to_io on _c:res ? to IO ???.
    29 ndefinition err_to_io_sig : ∀I,O,T.∀P:T → Prop. res (sigma T P) → IO I O (sigma T P) ≝
    30 λI,O,T,P,v. match v with [ OK v' ⇒ Value I O (sigma T P) v' | Error ⇒ Wrong I O (sigma T P) ].
    31 (*ncoercion err_to_io_sig : ∀I,O,A.∀P:A → Prop.∀c:res (sigma A P).IO I O (sigma A P) ≝ err_to_io_sig on _c:res (sigma ??) to IO ?? (sigma ??).*)
     26ndefinition err_to_io : ∀O,I,T. res T → IO O I T ≝
     27λO,I,T,v. match v with [ OK v' ⇒ Value O I T v' | Error ⇒ Wrong O I T ].
     28ncoercion err_to_io : ∀O,I,A.∀c:res A.IO O I A ≝ err_to_io on _c:res ? to IO ???.
     29ndefinition err_to_io_sig : ∀O,I,T.∀P:T → Prop. res (sigma T P) → IO O I (sigma T P) ≝
     30λO,I,T,P,v. match v with [ OK v' ⇒ Value O I (sigma T P) v' | Error ⇒ Wrong O I (sigma T P) ].
     31(*ncoercion err_to_io_sig : ∀O,I,A.∀P:A → Prop.∀c:res (sigma A P).IO O I (sigma A P) ≝ err_to_io_sig on _c:res (sigma ??) to IO ?? (sigma ??).*)
    3232
    3333
     
    4444interpretation "IO monad pair bind" 'bindIO2 e f = (bindIO2 ????? e f).
    4545(**)
    46 nlet rec P_io (I,O,A:Type) (P:A → Prop) (v:IO I O A) on v : Prop ≝
     46nlet rec P_io O I (A:Type) (P:A → Prop) (v:IO O I A) on v : Prop ≝
    4747match v return λ_.Prop with
    4848[ Wrong ⇒ True
    4949| Value z ⇒ P z
    50 | Interact out k ⇒ ∀v'.P_io I O A P (k v')
     50| Interact out k ⇒ ∀v'.P_io O I A P (k v')
    5151].
    5252
    53 nlet rec P_io' (I,O,A:Type) (P:A → Prop) (v:IO I O A) on v : Prop ≝
     53nlet rec P_io' O I (A:Type) (P:A → Prop) (v:IO O I A) on v : Prop ≝
    5454match v return λ_.Prop with
    5555[ Wrong ⇒ False
    5656| Value z ⇒ P z
    57 | Interact out k ⇒ ∀v'.P_io' I O A P (k v')
     57| Interact out k ⇒ ∀v'.P_io' O I A P (k v')
    5858].
    5959
    60 ndefinition P_to_P_option_io : ∀I,O,A.∀P:A → Prop.option (IO I O A) → Prop ≝
    61   λI,O,A,P,a.match a with
     60ndefinition P_to_P_option_io : ∀O,I,A.∀P:A → Prop.option (IO O I A) → Prop ≝
     61  λO,I,A,P,a.match a with
    6262   [ None ⇒ False
    63    | Some y ⇒ P_io I O A P y
     63   | Some y ⇒ P_io O I A P y
    6464   ].
    6565
    66 nlet rec io_inject_0 (I,O,A:Type) (P:A → Prop) (a:IO I O A) (p:P_io I O A P a) on a : IO I O (sigma A P) ≝
    67 (match a return λa'.P_io I O A P a' → ? with
    68  [ Wrong ⇒ λ_. Wrong I O ?
     66nlet rec io_inject_0 O I (A:Type) (P:A → Prop) (a:IO O I A) (p:P_io O I A P a) on a : IO O I (sigma A P) ≝
     67(match a return λa'.P_io O I A P a' → ? with
     68 [ Wrong ⇒ λ_. Wrong O I ?
    6969 | Value c ⇒ λp'. Value ??? (sig_intro A P c p')
    70  | Interact out k ⇒ λp'. Interact ??? out (λv. io_inject_0 I O A P (k v) (p' v))
     70 | Interact out k ⇒ λp'. Interact ??? out (λv. io_inject_0 O I A P (k v) (p' v))
    7171 ]) p.
    7272
    73 ndefinition io_inject : ∀I,O,A.∀P:A → Prop.∀a:option (IO I O A).∀p:P_to_P_option_io I O A P a.IO I O (sigma A P) ≝
    74   λI,O,A.λP:A → Prop.λa:option (IO I O A).λp:P_to_P_option_io I O A P a.
    75   (match a return λa'.P_to_P_option_io I O A P a' → IO I O (sigma A P) with
     73ndefinition io_inject : ∀O,I,A.∀P:A → Prop.∀a:option (IO O I A).∀p:P_to_P_option_io O I A P a.IO O I (sigma A P) ≝
     74  λO,I,A.λP:A → Prop.λa:option (IO O I A).λp:P_to_P_option_io O I A P a.
     75  (match a return λa'.P_to_P_option_io O I A P a' → IO O I (sigma A P) with
    7676   [ None ⇒ λp'.?
    77    | Some b ⇒ λp'. io_inject_0 I O A P b p'
     77   | Some b ⇒ λp'. io_inject_0 O I A P b p'
    7878   ]) p.
    7979nelim p'; nqed.
    8080
    81 nlet rec io_eject (I,O,A:Type) (P: A → Prop) (a:IO I O (sigma A P)) on a : IO I O A ≝
     81nlet rec io_eject O I (A:Type) (P: A → Prop) (a:IO O I (sigma A P)) on a : IO O I A ≝
    8282match a with
    8383[ Wrong ⇒ Wrong ???
     
    8787
    8888ncoercion io_inject :
    89   ∀I,O,A.∀P:A → Prop.∀a.∀p:P_to_P_option_io I O ? P a.IO I O (sigma A P) ≝ io_inject
     89  ∀O,I,A.∀P:A → Prop.∀a.∀p:P_to_P_option_io O I ? P a.IO O I (sigma A P) ≝ io_inject
    9090  on a:option (IO ???) to IO ?? (sigma ? ?).
    91 ncoercion io_eject : ∀I,O,A.∀P:A → Prop.∀c:IO I O (sigma A P).IO I O A ≝ io_eject
     91ncoercion io_eject : ∀O,I,A.∀P:A → Prop.∀c:IO O I (sigma A P).IO O I A ≝ io_eject
    9292  on _c:IO ?? (sigma ? ?) to IO ???.
    9393
    94 ndefinition opt_to_io : ∀I,O,T.option T → IO I O T ≝
    95 λI,O,T,v. match v with [ None ⇒ Wrong I O T | Some v' ⇒ Value I O T v' ].
    96 ncoercion opt_to_io : ∀I,O,T.∀v:option T. IO I O T ≝ opt_to_io on _v:option ? to IO ???.
     94ndefinition opt_to_io : ∀O,I,T.option T → IO O I T ≝
     95λO,I,T,v. match v with [ None ⇒ Wrong ?? T | Some v' ⇒ Value ??? v' ].
     96ncoercion opt_to_io : ∀O,I,T.∀v:option T. IO O I T ≝ opt_to_io on _v:option ? to IO ???.
    9797
    98 nlemma sig_bindIO_OK: ∀I,O,A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:IO I O (sigma A P). ∀f:sigma A P → IO I O B.
    99   (∀v:A. ∀p:P v. P_io I O ? P' (f (sig_intro A P v p))) →
    100   P_io I O ? P' (bindIO I O (sigma A P) B e f).
    101 #I O A B P P' e f; nelim e;
     98nlemma sig_bindIO_OK: ∀O,I,A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:IO O I (sigma A P). ∀f:sigma A P → IO O I B.
     99  (∀v:A. ∀p:P v. P_io O I ? P' (f (sig_intro A P v p))) →
     100  P_io O I ? P' (bindIO O I (sigma A P) B e f).
     101#O I A B P P' e f; nelim e;
    102102##[ #out k IH; #IH'; nwhd; #res; napply IH; //;
    103103##| #v0; nelim v0; #v Hv IH; nwhd; napply IH;
     
    105105##] nqed.
    106106
    107 nlemma sig_bindIO2_OK: ∀I,O,A,B,C. ∀P:(A×B) → Prop. ∀P':C → Prop. ∀e:IO I O (sigma (A×B) P). ∀f: A → B → IO I O C.
    108   (∀vA:A.∀vB:B. ∀p:P 〈vA,vB〉. P_io I O ? P' (f vA vB)) →
    109   P_io I O ? P' (bindIO2 I O A B C e f).
     107nlemma sig_bindIO2_OK: ∀O,I,A,B,C. ∀P:(A×B) → Prop. ∀P':C → Prop. ∀e:IO O I (sigma (A×B) P). ∀f: A → B → IO O I C.
     108  (∀vA:A.∀vB:B. ∀p:P 〈vA,vB〉. P_io O I ? P' (f vA vB)) →
     109  P_io O I ? P' (bindIO2 O I A B C e f).
    110110#I O A B C P P' e f; nelim e;
    111111##[ #out k IH; #IH'; nwhd; #res; napply IH; napply IH';
     
    114114##] nqed.
    115115
    116 nlemma opt_bindIO_OK: ∀I,O,A,B. ∀P:B → Prop. ∀e:option A. ∀f: A → IO I O B.
    117   (∀v:A. e = Some A v → P_io I O ? P (f v)) →
    118   P_io I O ? P (bindIO I O A B e f).
     116nlemma opt_bindIO_OK: ∀O,I,A,B. ∀P:B → Prop. ∀e:option A. ∀f: A → IO O I B.
     117  (∀v:A. e = Some A v → P_io O I ? P (f v)) →
     118  P_io O I ? P (bindIO O I A B e f).
    119119#I O A B P e; nelim e; //; #v f H; napply H; //;
    120120nqed.
    121121
    122 nlemma opt_bindIO2_OK: ∀I,O,A,B,C. ∀P:C → Prop. ∀e:option (A×B). ∀f: A → B → IO I O C.
    123   (∀vA:A.∀vB:B. e = Some (A×B) 〈vA,vB〉 → P_io I O ? P (f vA vB)) →
    124   P_io I O ? P (bindIO2 I O A B C e f).
     122nlemma opt_bindIO2_OK: ∀O,I,A,B,C. ∀P:C → Prop. ∀e:option (A×B). ∀f: A → B → IO O I C.
     123  (∀vA:A.∀vB:B. e = Some (A×B) 〈vA,vB〉 → P_io O I ? P (f vA vB)) →
     124  P_io O I ? P (bindIO2 O I A B C e f).
    125125#I O A B C P e; nelim e; //; #v; ncases v; #vA vB f H; napply H; //;
    126126nqed.
    127127
    128 nlemma res_bindIO_OK: ∀I,O,A,B. ∀P:B → Prop. ∀e:res A. ∀f: A → IO I O B.
    129   (∀v:A. e = OK A v → P_io I O ? P (f v)) →
    130   P_io I O ? P (bindIO I O A B e f).
     128nlemma res_bindIO_OK: ∀O,I,A,B. ∀P:B → Prop. ∀e:res A. ∀f: A → IO O I B.
     129  (∀v:A. e = OK A v → P_io O I ? P (f v)) →
     130  P_io O I ? P (bindIO O I A B e f).
    131131#I O A B P e; nelim e; //; #v f H; napply H; //;
    132132nqed.
    133133
    134 nlemma res_bindIO2_OK: ∀I,O,A,B,C. ∀P:C → Prop. ∀e:res (A×B). ∀f: A → B → IO I O C.
    135   (∀vA:A.∀vB:B. e = OK (A×B) 〈vA,vB〉 → P_io I O ? P (f vA vB)) →
    136   P_io I O ? P (bindIO2 I O A B C e f).
     134nlemma res_bindIO2_OK: ∀O,I,A,B,C. ∀P:C → Prop. ∀e:res (A×B). ∀f: A → B → IO O I C.
     135  (∀vA:A.∀vB:B. e = OK (A×B) 〈vA,vB〉 → P_io O I ? P (f vA vB)) →
     136  P_io O I ? P (bindIO2 O I A B C e f).
    137137#I O A B C P e; nelim e; //; #v; ncases v; #vA vB f H; napply H; //;
    138138nqed.
    139139
    140 nlemma bindIO_OK: ∀I,O,A,B. ∀P:B → Prop. ∀e:IO I O A. ∀f: A → IO I O B.
    141   (∀v:A. P_io I O ? P (f v)) →
    142   P_io I O ? P (bindIO I O A B e f).
     140nlemma bindIO_OK: ∀O,I,A,B. ∀P:B → Prop. ∀e:IO O I A. ∀f: A → IO O I B.
     141  (∀v:A. P_io O I ? P (f v)) →
     142  P_io O I ? P (bindIO O I A B e f).
    143143#I O A B P e; nelim e;
    144144##[ #out k IH; #f H; nwhd; #res; napply IH; //;
     
    147147##] nqed.
    148148
    149 nlemma bindIO2_OK: ∀I,O,A,B,C. ∀P:C → Prop. ∀e:IO I O (A×B). ∀f: A → B → IO I O C.
    150   (∀v1:A.∀v2:B. P_io I O ? P (f v1 v2)) →
    151   P_io I O ? P (bindIO2 I O A B C e f).
     149nlemma bindIO2_OK: ∀O,I,A,B,C. ∀P:C → Prop. ∀e:IO O I (A×B). ∀f: A → B → IO O I C.
     150  (∀v1:A.∀v2:B. P_io O I ? P (f v1 v2)) →
     151  P_io O I ? P (bindIO2 O I A B C e f).
    152152#I O A B C P e; nelim e;
    153153##[ #out k IH; #f H; nwhd; #res; napply IH; //;
     
    156156##] nqed.
    157157
    158 nlemma P_bindIO_OK: ∀I,O,A,B. ∀P':A → Prop. ∀P:B → Prop. ∀e:IO I O A. ∀f: A → IO I O B.
     158nlemma P_bindIO_OK: ∀O,I,A,B. ∀P':A → Prop. ∀P:B → Prop. ∀e:IO O I A. ∀f: A → IO O I B.
    159159  P_io … P' e →
    160   (∀v:A. P' v → P_io I O ? P (f v)) →
    161   P_io I O ? P (bindIO I O A B e f).
     160  (∀v:A. P' v → P_io O I ? P (f v)) →
     161  P_io O I ? P (bindIO O I A B e f).
    162162#I O A B P' P e; nelim e;
    163163##[ #out k IH f He H; nwhd in He ⊢ %; #res; napply IH; /2/;
     
    166166##] nqed.
    167167
    168 nlemma P_bindIO2_OK: ∀I,O,A,B,C. ∀P':A×B → Prop. ∀P:C → Prop. ∀e:IO I O (A×B). ∀f: A → B → IO I O C.
     168nlemma P_bindIO2_OK: ∀O,I,A,B,C. ∀P':A×B → Prop. ∀P:C → Prop. ∀e:IO O I (A×B). ∀f: A → B → IO O I C.
    169169  P_io … P' e →
    170   (∀v1:A.∀v2:B. P' 〈v1,v2〉 → P_io I O ? P (f v1 v2)) →
    171   P_io I O ? P (bindIO2 I O A B C e f).
     170  (∀v1:A.∀v2:B. P' 〈v1,v2〉 → P_io O I ? P (f v1 v2)) →
     171  P_io O I ? P (bindIO2 O I A B C e f).
    172172#I O A B C P' P e; nelim e;
    173173##[ #out k IH f He H; nwhd in He ⊢ %; #res; napply IH; /2/;
     
    186186*)
    187187
    188 nlemma extract_subset_pair_io: ∀I,O,A,B,C,P. ∀e:{e:A×B | P e}. ∀Q:A→B→IO I O C. ∀R:C→Prop.
    189   (∀a,b. eject ?? e = 〈a,b〉 → P 〈a,b〉 → P_io I O ? R (Q a b)) →
    190   P_io I O ? R (match eject ?? e with [ mk_pair a b ⇒ Q a b ]).
     188nlemma extract_subset_pair_io: ∀O,I,A,B,C,P. ∀e:{e:A×B | P e}. ∀Q:A→B→IO O I C. ∀R:C→Prop.
     189  (∀a,b. eject ?? e = 〈a,b〉 → P 〈a,b〉 → P_io O I ? R (Q a b)) →
     190  P_io O I ? R (match eject ?? e with [ mk_pair a b ⇒ Q a b ]).
    191191#I O A B C P e Q R; ncases e; #e'; ncases e'; nnormalize;
    192192##[ *;
  • C-semantics/test/io.c.ma

    r125 r366  
    2525(* ndefinition works fine for this, whereas nletin during proof seems to blow up. *)
    2626ndefinition ts ≝ (
    27  ! s0 ← make_initial_state myprog;:
    28  ! 〈t,s〉 ← exec_steps 7 (globalenv Genv ?? myprog) s0;:
     27 ! s0 ← make_initial_state myprog;
     28 ! 〈t,s〉 ← exec_steps 7 (globalenv Genv ?? myprog) s0;
    2929   ret ? 〈t,s〉).
    3030
     
    3232| witness : ∀t:T. result T t.
    3333
     34ndefinition do_int : ∀T:Type.∀o:io_out. (io_in o → IO io_out io_in T) → int → IO io_out io_in T ≝
     35λT,o,k,i. (match io_in_typ o return λt'.(eventval_type t' → IO io_out io_in T) → IO io_out io_in T with
     36[ Tint ⇒ λk'.k' i
     37| Tfloat ⇒ λk'.Wrong ???
     38]) k.
     39
    3440(* The trick to being able to normalize the term is to avoid looking at the
    3541   continuations! *)
    3642nremark exec_OK:
    37     match match ts with [ Interact call k ⇒ k (EVint (repr 6))
     43    match match ts with [ Interact call k ⇒ do_int ? call k (repr 6)
    3844                 | Value v ⇒ Wrong ???
    3945                 | Wrong ⇒ Wrong ??? ] with
  • 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.