module Stdlib.Data.Maybe.Base;

import Juvix.Builtin.V1.Maybe open public;
import Juvix.Builtin.V1.Bool open;

--- Extracts the value from a ;Maybe; if present, else returns the given value.
{-# inline: true #-}
fromMaybe {A} (defaultValue : A) (maybeValue : Maybe A) : A :=
  case maybeValue of
    | nothing := defaultValue
    | just a := a;

--- Applies a function to the value from a ;Maybe; if present, else returns the
--- given value.
{-# inline: true, isabelle-function: {name: "case_option"} #-}
maybe {A B} (defaultValue : B) (fun : A -> B) (maybeValue : Maybe A) : B :=
  case maybeValue of
    | nothing := defaultValue
    | just a := fun a;

isJust {A} (maybeValue : Maybe A) : Bool :=
  case maybeValue of
    | nothing := false
    | just _ := true;