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 | |
---|