include "utilities/monad.ma".
include "basics/types.ma".

definition Option ≝ MakeMonadProps
  (* the monad *)
  option
  (* return *)
  (λX.Some X)
  (* bind *)
  (λX,Y,m,f. match m with [ Some x ⇒ f x | None ⇒ None ?])
  ????.
// #X[|*:#Y[#Z]]*normalize//qed.

include "hints_declaration.ma".
alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
unification hint 0 ≔ X;
N ≟ max_def Option
(*---------------*) ⊢
option X ≡ monad N X
.

definition opt_safe : ∀X.∀m : option X. m ≠ None X → X ≝
λX,m,prf.match m return λx.m = x → X with
  [ Some t ⇒ λ_.t
  | None ⇒ λeq_m.?
  ] (refl …). elim (absurd … eq_m prf) qed.

lemma opt_to_opt_safe : ∀A,m,prf. m = Some ? (opt_safe A m prf).
#A *
[ #ABS elim (absurd ? (refl ??) ABS)
| //
] qed.

lemma opt_safe_elim : ∀A.∀P : A → Prop.∀m,prf.
  (∀x.m = Some ? x → P x) → P (opt_safe ? m prf).
#A#P*
[#prf elim(absurd … (refl ??) prf)
|#x normalize #_ #H @H @refl
] qed.

lemma opt_safe_proof_irr : ∀A,m,prf1,prf2.
  opt_safe A m prf1 = opt_safe A m prf2.
  #A* // qed.

definition opt_try_catch : ∀X.option X → (unit → X) → X ≝
  λX,m,f.match m with [Some x ⇒ x | None ⇒ f it].

notation > "'Try' m 'catch' opt (ident e opt( : ty)) ⇒ f" with precedence 46 for
  ${ default
    @{ ${ default
      @{'trycatch $m (λ${ident e}:$ty.$f)}
      @{'trycatch $m (λ${ident e}.$f)}
    }}
    @{'trycatch $m (λ_.$f)}
  }.

notation < "hvbox('Try' \nbsp break m \nbsp break 'catch' \nbsp ident e : ty \nbsp ⇒ \nbsp break f)" with precedence 46 for
  @{'trycatch $m (λ${ident e}:$ty.$f)}.
notation < "hvbox('Try' \nbsp break m \nbsp break 'catch' \nbsp ⇒ \nbsp break f)" with precedence 46 for
  @{'trycatch $m (λ_:$ty.$f)}.

interpretation "option try and catch" 'trycatch m f = (opt_try_catch ? m f).

definition OptPred ≝ λPdef : Prop.mk_InjMonadPred Option
  (mk_MonadPred ?
    (λX,P,x.Try ! y ← x ; return P y catch ⇒ Pdef)
    ???)
  (λX,P,m_sig.match m_sig with [ mk_Sig m prf ⇒ match m return λx.Try ! y ← x ; return P y catch ⇒ Pdef → option (Σy.?) with [ Some x ⇒ λprf.Some ? x | None ⇒ λ_.None ? ] prf ])
  ?.
[4: @prf
|*:
#X[2:#Y]#P1[1,2:#P2[2:#H]]
[1,2,4: * [5: *]] normalize /2/
qed.

definition opt_All : ∀X.(X → Prop) → option X → Prop ≝ m_pred … (OptPred True).

lemma opt_All_mp : ∀A,P,Q.(∀x. P x → Q x) → ∀o.opt_All A P o → opt_All ? Q o
  ≝ m_pred_mp ….

definition opt_Exists : ∀X.(X → Prop) → option X → Prop ≝ m_pred … (OptPred False).
 
lemma opt_Exists_mp : ∀A,P,Q.(∀x. P x → Q x) → ∀o.opt_Exists A P o → opt_Exists ? Q o
  ≝ m_pred_mp ….