val ffalse (reason: string) : pbool
let ffalse (reason:string) : pbool = Err reason
val ffalse (reason: string) : pbool
let ffalse (reason: string) : pbool =
Err reason
Vale.Def.PossiblyMonad.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked
Vale.Def.PossiblyMonad.fst
Prims.string Vale.Def.PossiblyMonad.Err Prims.unit Vale.Def.PossiblyMonad.pbool
module Vale.Def.PossiblyMonad

/// Similar to the [maybe] monad in Haskell (which is like the
/// [option] type in F* and OCaml), but instead, we also store the
/// reason for the error when the error occurs.

type possibly 'a =
  | Ok : v:'a -> possibly 'a
  | Err : reason:string -> possibly 'a

unfold let return (#a:Type) (x:a) : possibly a =
  Ok x

unfold let (let+) (#a #b:Type) (x:possibly a) (f:a -> possibly b) : possibly b =
  match x with
  | Err s -> Err s
  | Ok x' -> f x'

unfold let fail_with (#a:Type) (s:string) : possibly a = Err s

unfold let unimplemented (#a:Type) (s:string) : possibly a = fail_with ("Unimplemented: " ^ s)

(** Allows moving to a "looser" monad type, always *)
unfold
let loosen (#t1:Type) (#t2:Type{t1 `subtype_of` t2})
    (x:possibly t1) : possibly t2 =
  match x with
  | Ok x' -> Ok x'
  | Err s -> Err s

(** Allows moving to a "tighter" monad type, as long as the monad is
    guaranteed statically to be within this tighter type *)
unfold
let tighten (#t1:Type) (#t2:Type{t2 `subtype_of` t1})
    (x:possibly t1{Ok? x ==> Ok?.v x `has_type` t2}) : possibly t2 =
  match x with
  | Ok x' -> Ok x'
  | Err s -> Err s

(** [pbool] is a type that can be used instead of [bool] to hold on to
    a reason whenever it is [false]. To convert from a [pbool] to a
    bool, see [!!]. *)
unfold
type pbool = possibly unit

(** [!!x] coerces a [pbool] into a [bool] by discarding any reason it
    holds on to and instead uses it solely as a boolean. *)
unfold
let (!!) (x:pbool) : bool = Ok? x

(** [ttrue] is just the same as [true] but for a [pbool] *)
unfold
let ttrue : pbool = Ok ()

(** [ffalse] is the same as [false] but is for a [pbool] and thus requires a reason for being false. *)
val ffalse (reason: string) : pbool
reason: Prims.string -> Vale.Def.PossiblyMonad.pbool