Changeset 366 for C-semantics/IOMonad.ma


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/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##[ *;
Note: See TracChangeset for help on using the changeset viewer.