extracted/option.ml

   1 open Preamble
   2
   3 open Hints_declaration
   4
   5 open Core_notation
   6
   7 open Pts
   8
   9 open Logic
  10
  11 open Types
  12
  13 open Jmeq
  14
  15 open Russell
  16
  17 open Bool
  18
  19 open Nat
  20
  21 open List
  22
  23 open Setoids
  24
  25 open Relations
  26
  27 open Monad
  28
  29 (** val option : Monad.monadProps **)
  30 let option =
  31   Monad.makeMonadProps (fun _ x -> Types.Some x) (fun _ _ m f ->
  32     match m with
  33     | Types.None -> Types.None
  34     | Types.Some x -> f x)
  35
  36 (** val opt_safe : 'a1 Types.option -> 'a1 **)
  37 let opt_safe m =
  38   (match m with
  39    | Types.None -> (fun _ -> Logic.false_rect_Type0 __)
  40    | Types.Some t -> (fun _ -> t)) __
  41
  42 (** val opt_try_catch : 'a1 Types.option -> (Types.unit0 -> 'a1) -> 'a1 **)
  43 let opt_try_catch m f =
  44   match m with
  45   | Types.None -> f Types.It
  46   | Types.Some x -> x
  47
  48 (** val optPred : Monad.injMonadPred **)
  49 let optPred =
  50   { Monad.im_pred = Monad.Mk_MonadPred; Monad.mp_inject = (fun _ _ m_sig ->
  51     let m = m_sig in
  52     (match Obj.magic m with
  53      | Types.None -> (fun _ -> Obj.magic Types.None)
  54      | Types.Some x -> (fun _ -> Obj.magic (Types.Some x))) __) }
  55