| 1 | include "utilities/monad.ma". |
|---|
| 2 | include "basics/types.ma". |
|---|
| 3 | |
|---|
| 4 | definition Option ≝ MakeMonadProps |
|---|
| 5 | (* the monad *) |
|---|
| 6 | option |
|---|
| 7 | (* return *) |
|---|
| 8 | (λX.Some X) |
|---|
| 9 | (* bind *) |
|---|
| 10 | (λX,Y,m,f. match m with [ Some x ⇒ f x | None ⇒ None ?]) |
|---|
| 11 | ????. |
|---|
| 12 | // #X[|*:#Y[#Z]]*normalize//qed. |
|---|
| 13 | |
|---|
| 14 | include "hints_declaration.ma". |
|---|
| 15 | unification hint 0 ≔ X; |
|---|
| 16 | N ≟ max_def Option |
|---|
| 17 | (*---------------*) ⊢ |
|---|
| 18 | option X ≡ monad N X |
|---|
| 19 | . |
|---|
| 20 | |
|---|
| 21 | definition opt_safe : ∀X.∀m : option X. m ≠ None X → X ≝ |
|---|
| 22 | λX,m,prf.match m return λx.m = x → X with |
|---|
| 23 | [ Some t ⇒ λ_.t |
|---|
| 24 | | None ⇒ λeq_m.? |
|---|
| 25 | ] (refl …). elim (absurd … eq_m prf) qed. |
|---|
| 26 | |
|---|
| 27 | lemma opt_to_opt_safe : ∀A,m,prf. m = Some ? (opt_safe A m prf). |
|---|
| 28 | #A * |
|---|
| 29 | [ #ABS elim (absurd ? (refl ??) ABS) |
|---|
| 30 | | // |
|---|
| 31 | ] qed. |
|---|
| 32 | |
|---|
| 33 | lemma opt_safe_elim : ∀A.∀P : A → Prop.∀m,prf. |
|---|
| 34 | (∀x.m = Some ? x → P x) → P (opt_safe ? m prf). |
|---|
| 35 | #A#P* |
|---|
| 36 | [#prf elim(absurd … (refl ??) prf) |
|---|
| 37 | |#x normalize #_ #H @H @refl |
|---|
| 38 | ] qed. |
|---|
| 39 | |
|---|
| 40 | definition opt_try_catch : ∀X.option X → (unit → X) → X ≝ |
|---|
| 41 | λX,m,f.match m with [Some x ⇒ x | None ⇒ f it]. |
|---|
| 42 | |
|---|
| 43 | notation > "'Try' m 'catch' opt (ident e opt( : ty)) ⇒ f" with precedence 46 for |
|---|
| 44 | ${ default |
|---|
| 45 | @{ ${ default |
|---|
| 46 | @{'trycatch $m (λ${ident e}:$ty.$f)} |
|---|
| 47 | @{'trycatch $m (λ${ident e}.$f)} |
|---|
| 48 | }} |
|---|
| 49 | @{'trycatch $m (λ_.$f)} |
|---|
| 50 | }. |
|---|
| 51 | |
|---|
| 52 | notation < "hvbox('Try' \nbsp break m \nbsp break 'catch' \nbsp ident e : ty \nbsp ⇒ \nbsp break f)" with precedence 46 for |
|---|
| 53 | @{'trycatch $m (λ${ident e}:$ty.$f)}. |
|---|
| 54 | notation < "hvbox('Try' \nbsp break m \nbsp break 'catch' \nbsp ⇒ \nbsp break f)" with precedence 46 for |
|---|
| 55 | @{'trycatch $m (λ_:$ty.$f)}. |
|---|
| 56 | |
|---|
| 57 | interpretation "option try and catch" 'trycatch m f = (opt_try_catch ? m f). |
|---|
| 58 | |
|---|
| 59 | definition OptPred ≝ λPdef : Prop.mk_MonadPred Option (λX,P,m.Try ! x ← m ; return P x catch ⇒ Pdef) ???. |
|---|
| 60 | #X[2:#Y]#P1[1,3:#P2[2:#H]*] normalize /2/ |
|---|
| 61 | qed. |
|---|
| 62 | |
|---|
| 63 | definition opt_All : ∀X.(X → Prop) → option X → Prop ≝ m_pred … (OptPred True). |
|---|
| 64 | |
|---|
| 65 | lemma opt_All_mp : ∀A,P,Q.(∀x. P x → Q x) → ∀o.opt_All A P o → opt_All ? Q o |
|---|
| 66 | ≝ m_pred_mp …. |
|---|
| 67 | |
|---|
| 68 | definition opt_Exists : ∀X.(X → Prop) → option X → Prop ≝ m_pred … (OptPred False). |
|---|
| 69 | |
|---|
| 70 | lemma opt_Exists_mp : ∀A,P,Q.(∀x. P x → Q x) → ∀o.opt_Exists A P o → opt_Exists ? Q o |
|---|
| 71 | ≝ m_pred_mp …. |
|---|
| 72 | |
|---|
