Changeset 1640 for src/common
- Timestamp:
- Jan 11, 2012, 5:41:45 PM (9 years ago)
- Location:
- src/common
- Files:
-
- 3 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/AST.ma
r1516 r1640 196 196 197 197 lemma typesize_pos: ∀ty. typesize ty > 0. 198 *; try *; try * /2 / qed.198 *; try *; try * /2 by le_n/ qed. 199 199 200 200 lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2). … … 343 343 definition map_partial : ∀A,B,C:Type[0]. (B → res C) → 344 344 list (A × B) → res (list (A × C)) ≝ 345 λA,B,C,f. m map?? (λab. let 〈a,b〉 ≝ ab in do c ← f b; OK ? 〈a,c〉).345 λA,B,C,f. m_mmap ??? (λab. let 〈a,b〉 ≝ ab in do c ← f b; OK ? 〈a,c〉). 346 346 347 347 lemma map_partial_preserves_first: -
src/common/Errors.ma
r1626 r1640 19 19 include "common/PreIdentifiers.ma". 20 20 include "basics/russell.ma". 21 include "utilities/monad.ma". 21 22 22 23 (* * Error reporting and the error monad. *) … … 48 49 (*Implicit Arguments Error [A].*) 49 50 50 (* * To automate the propagation of errors, we use a monadic style 51 with the following [bind] operation. *) 52 53 definition bind ≝ λA,B:Type[0]. λf: res A. λg: A → res B. 54 match f with 55 [ OK x ⇒ g x 56 | Error msg ⇒ Error ? msg 57 ]. 58 59 definition bind2 ≝ λA,B,C: Type[0]. λf: res (A × B). λg: A → B → res C. 60 match f with 61 [ OK v ⇒ g (fst … v) (snd … v) 62 | Error msg => Error ? msg 63 ]. 64 65 definition bind3 ≝ λA,B,C,D: Type[0]. λf: res (A × B × C). λg: A → B → C → res D. 66 match f with 67 [ OK v ⇒ g (fst … (fst … v)) (snd … (fst … v)) (snd … v) 68 | Error msg => Error ? msg 69 ]. 70 71 (* Not sure what level to use *) 72 notation > "vbox('do' ident v ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v}.${e'})}. 73 notation > "vbox('do' ident v : ty ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v} : ${ty}.${e'})}. 74 notation < "vbox('do' \nbsp ident v ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v}.${e'})}. 75 notation < "vbox('do' \nbsp ident v : ty ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v} : ${ty}.${e'})}. 76 interpretation "error monad bind" 'bind e f = (bind ?? e f). 77 notation > "vbox('do' 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}. 78 notation > "vbox('do' 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}. 79 notation < "vbox('do' \nbsp 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}. 80 notation < "vbox('do' \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}. 81 interpretation "error monad Prod bind" 'bind2 e f = (bind2 ??? e f). 82 notation > "vbox('do' 〈ident v1, ident v2, ident v3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1}.λ${ident v2}.λ${ident v3}.${e'})}. 83 notation > "vbox('do' 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.λ${ident v3} : ${ty3}.${e'})}. 84 notation < "vbox('do' \nbsp 〈ident v1, ident v2, ident v3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1}.λ${ident v2}.λ${ident v3}.${e'})}. 85 notation < "vbox('do' \nbsp 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.λ${ident v3} : ${ty3}.${e'})}. 86 interpretation "error monad triple bind" 'bind3 e f = (bind3 ???? e f). 87 (*interpretation "error monad ret" 'ret e = (ret ? e). 88 notation "'ret' e" non associative with precedence 45 for @{'ret ${e}}.*) 89 90 (* Dependent pair version. *) 51 definition Res : Monad ≝ MakeMonad (mk_MonadDefinition 52 (* the monad *) 53 res 54 (* return *) 55 (λX.OK X) 56 (* bind *) 57 (λX,Y,m,f. match m with [ OK x ⇒ f x | Error msg ⇒ Error ? msg]) 58 ???). 59 // 60 [(* bind_bind *) 61 #X#Y#Z*normalize // 62 |(* bind_ret *) 63 #X*normalize // 64 ] 65 qed. 66 67 include "hints_declaration.ma". 68 unification hint 0 ≔ X; 69 M ≟ m_def Res 70 (*---------------*) ⊢ 71 res X ≡ monad M X 72 . 73 74 (*(* Dependent pair version. *) 91 75 notation > "vbox('do' « ident v , ident p » ← e; break e')" with precedence 40 92 76 for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ mk_Sig ${ident v} ${ident p} ⇒ ${e'} ]) }. … … 110 94 111 95 notation > "vbox('do' «ident v1, ident v2, ident H» ← e; break e')" with precedence 40 for @{'sigbind2 ${e} (λ${ident v1}.λ${ident v2}.λ${ident H}.${e'})}. 112 interpretation "error monad sig Prod bind" 'sigbind2 e f = (sigbind2 ???? e f). 113 114 (* 115 (** The [do] notation, inspired by Haskell's, keeps the code readable. *) 116 117 Notation "'do' X <- A ; B" := (bind A (fun X => B)) 118 (at level 200, X ident, A at level 100, B at level 200) 119 : error_monad_scope. 120 121 Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B)) 122 (at level 200, X ident, Y ident, A at level 100, B at level 200) 123 : error_monad_scope. 124 *) 125 lemma bind_inversion: 96 interpretation "error monad sig Prod bind" 'sigbind2 e f = (sigbind2 ???? e f).*) 97 98 lemma res_bind_inversion: 126 99 ∀A,B: Type[0]. ∀f: res A. ∀g: A → res B. ∀y: B. 127 bind ?? f g = OK ? y→128 ∃x. f = OK ? x ∧ g x = OK ? y.129 #A #B #f #g #y cases f ;130 [ #a #e %{a} whd in e:(??%?); /2/;131 | #m #H whd in H:(??%?); destruct (H);100 (f »= g = return y) → 101 ∃x. (f = return x) ∧ (g x = return y). 102 #A #B #f #g #y cases f normalize 103 [ #a #e %{a} /2 by conj/ 104 | #m #H destruct (H) 132 105 ] qed. 133 106 134 107 lemma bind2_inversion: 135 108 ∀A,B,C: Type[0]. ∀f: res (A×B). ∀g: A → B → res C. ∀z: C. 136 bind2 ??? f g = OK ?z →137 ∃x. ∃y. f = OK ? 〈x, y〉 ∧ g x y = OK ?z.138 #A #B #C #f #g #z cases f ;139 [ #ab cases ab; #a #b #e %{a} %{b} whd in e:(??%?); /2/;140 | #m #H whd in H:(??%?); destruct109 m_bind2 ???? f g = return z → 110 ∃x. ∃y. f = return 〈x, y〉 ∧ g x y = return z. 111 #A #B #C #f #g #z cases f normalize 112 [ * #a #b normalize #e %{a} %{b} /2 by conj/ 113 | #m #H destruct (H) 141 114 ] qed. 142 115 143 116 (* 144 Open Local Scope error_monad_scope. 145 146 (** This is the familiar monadic map iterator. *) 147 *) 148 149 let rec mmap (A, B: Type[0]) (f: A → res B) (l: list A) on l : res (list B) ≝ 150 match l with 151 [ nil ⇒ OK ? [] 152 | cons hd tl ⇒ do hd' ← f hd; do tl' ← mmap ?? f tl; OK ? (hd'::tl') 153 ]. 154 155 (* And mmap coupled with proofs. *) 156 157 let rec mmap_sigma (A,B:Type[0]) (P:B → Prop) (f:A → res (Σx:B.P x)) (l:list A) on l : res (Σl':list B.All B P l') ≝ 158 match l with 159 [ nil ⇒ OK ? «nil B, ?» 160 | cons h t ⇒ 161 do h' ← f h; 162 do t' ← mmap_sigma A B P f t; 163 OK ? «cons B h' t', ?» 164 ]. 165 whd // % 166 [ @(pi2 … h') 167 | cases t' #l' #p @p 168 ] qed. 117 Open Local Scope error_monad_scope.*) 169 118 170 119 (* … … 189 138 [ nil ⇒ x 190 139 | cons hd tl ⇒ 191 dox ← x ;140 ! x ← x ; 192 141 mfold_left_i_aux A B f (f i x hd) (S i) tl 193 142 ]. … … 213 162 [ nil ⇒ Error ? (msg WrongLength) 214 163 | cons hd' tl' ⇒ 215 doaccu ← accu;164 ! accu ← accu; 216 165 mfold_left2 … f (f accu hd hd') tl tl' 217 166 ] … … 301 250 ] (refl ? f). 302 251 303 notation > "vbox(' do' ident v 'as' ident E ← e; break e')" with precedence 40 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.252 notation > "vbox('!' ident v 'as' ident E ← e; break e')" with precedence 40 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}. 304 253 305 254 definition bind2_eq ≝ λA,B,C:Type[0]. λf: res (A×B). λg: ∀a:A.∀b:B. f = OK ? 〈a,b〉 → res C. … … 309 258 ] (refl ? f). 310 259 311 notation > "vbox(' do' 〈ident v1, ident v2〉 'as' ident E ← e; break e')" with precedence 40 for @{ bind2_eq ??? ${e} (λ${ident v1}.λ${ident v2}.λ${ident E}.${e'})}.260 notation > "vbox('!' 〈ident v1, ident v2〉 'as' ident E ← e; break e')" with precedence 40 for @{ bind2_eq ??? ${e} (λ${ident v1}.λ${ident v2}.λ${ident E}.${e'})}. 312 261 313 262 definition res_to_opt : ∀A:Type[0]. res A → option A ≝ -
src/common/IOMonad.ma
r1601 r1640 8 8 | Value : T → IO output input T 9 9 | Wrong : errmsg → IO output input T. 10 11 include "utilities/proper.ma". 12 (* a weak form of extensionality *) 13 axiom interact_proper : 14 ∀O,I,T,o.∀f,g : I o → IO O I T.(∀i. f i = g i) → Interact … o f = Interact … o g. 10 15 11 16 let rec bindIO (O:Type[0]) (I:O → Type[0]) (T,T':Type[0]) (v:IO O I T) (f:T → IO O I T') on v : IO O I T' ≝ … … 16 21 ]. 17 22 18 let rec bindIO2 (O:Type[0]) (I:O → Type[0]) (T1,T2,T':Type[0]) (v:IO O I (T1×T2)) (f:T1 → T2 → IO O I T') on v : IO O I T' ≝ 19 match v with 20 [ Interact out k ⇒ (Interact ??? out (λres. bindIO2 ?? T1 T2 T' (k res) f)) 21 | Value v' ⇒ let 〈v1,v2〉 ≝ v' in f v1 v2 22 | Wrong m ⇒ Wrong ?? T' m 23 ]. 23 include "utilities/monad.ma". 24 25 definition IOMonad ≝ λO,I. 26 MakeMonad (mk_MonadDefinition 27 (* the monad *) 28 (IO O I) 29 (* return *) 30 (λX.Value … X) 31 (* bind *) 32 (bindIO O I) 33 ???). / by / 34 [(* bind_bind *) 35 #X#Y#Z#m#f#g elim m normalize [2,3://] 36 (* Interact *) 37 #o#f #Hi @interact_proper // 38 |(* bind_ret *) 39 #X#m elim m normalize // #o#f#Hi @interact_proper // 40 ] 41 qed. 42 43 definition bindIO2 ≝ λO,I. m_bind2 (IOMonad O I). 44 45 include "hints_declaration.ma". 46 47 unification hint 0 ≔ O, I, T; 48 N ≟ IOMonad O I, M ≟ m_def N 49 (*******************************************) ⊢ 50 IO O I T ≡ monad M T 51 . 52 24 53 25 54 definition err_to_io : ∀O,I,T. res T → IO O I T ≝ 26 55 λO,I,T,v. match v with [ OK v' ⇒ Value O I T v' | Error m ⇒ Wrong O I T m ]. 56 27 57 coercion err_to_io : ∀O,I,A.∀c:res A.IO O I A ≝ err_to_io on _c:res ? to IO ???. 58 28 59 definition err_to_io_sig : ∀O,I,T.∀P:T → Prop. res (Sig T P) → IO O I (Sig T P) ≝ 29 60 λO,I,T,P,v. match v with [ OK v' ⇒ Value O I (Sig T P) v' | Error m ⇒ Wrong O I (Sig T P) m ]. 30 61 (*coercion err_to_io_sig : ∀O,I,A.∀P:A → Prop.∀c:res (Sig A P).IO O I (Sig A P) ≝ err_to_io_sig on _c:res (Sig ??) to IO ?? (Sig ??).*) 31 62 32 33 (* If the original definitions are vague enough, do I need to do this? *)34 notation > "! ident v ← e; e'" with precedence 40 for @{'bindIO ${e} (λ${ident v}.${e'})}.35 notation > "! ident v : ty ← e; e'" with precedence 40 for @{'bindIO ${e} (λ${ident v} : ${ty}.${e'})}.36 notation < "vbox(! \nbsp ident v ← e; break e')" with precedence 40 for @{'bindIO ${e} (λ${ident v}.${e'})}.37 notation < "vbox(! \nbsp ident v : ty ← e; break e')" with precedence 40 for @{'bindIO ${e} (λ${ident v} : ${ty}.${e'})}.38 notation > "! 〈ident v1, ident v2〉 ← e; e'" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.39 notation > "! 〈ident v1 : ty1, ident v2 : ty2〉 ← e; e'" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.40 notation < "vbox(! \nbsp 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.41 notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.42 interpretation "IO monad bind" 'bindIO e f = (bindIO ???? e f).43 interpretation "IO monad Prod bind" 'bindIO2 e f = (bindIO2 ????? e f).44 (**)45 63 let rec P_io O I (A:Type[0]) (P:A → Prop) (v:IO O I A) on v : Prop ≝ 46 64 match v return λ_.Prop with … … 176 194 177 195 (* Is there a way to prove this without extensionality? *) 178 196 (* 179 197 lemma bind_assoc_r: ∀O,I,A,B,C,e,f,g. 180 198 ∀ext:(∀T1,T2:Type[0].∀f,f':T1 → T2.(∀x.f x = f' x) → f = f'). … … 186 204 | #m @refl 187 205 ] qed. 206 *) 207 definition bind_assoc_r ≝ λO,I.m_bind_bind (IOMonad O I). 188 208 189 209 (*
Note: See TracChangeset
for help on using the changeset viewer.