Library EVMOpSem.Lem.lem_maybe

Require Import Arith.
Require Import Bool.
Require Import List.
Require Import String.
Require Import Program.Wf.

Require Import coqharness.

Open Scope nat_scope.
Open Scope string_scope.


Require Import lem_bool.
Require Export lem_bool.
Require Import lem_basic_classes.
Require Export lem_basic_classes.
Require Import lem_function.
Require Export lem_function.



Definition maybeEqualBy {a : Type} (eq : a -> a -> bool ) (x : option a ) (y : option a ) : bool := match ( (x,y)) with
  | (None, None) => true
  | (None, Some _) => false
  | (Some _, None) => false
  | (Some x', Some y') => (eq x' y')
end.

Instance x22_Eq{a: Type} `{Eq a}: Eq (option a ):= {
   isEqual := (maybeEqualBy (fun x y => x = y));
   isInequal x y := negb ((maybeEqualBy (fun x y => x = y) x y))
}.

Definition maybeCompare {a b : Type} (cmp : b -> a -> ordering ) (x : option b ) (y : option a ) : ordering := match ( (x,y)) with
  | (None, None) => EQ
  | (None, Some _) => LT
  | (Some _, None) => GT
  | (Some x', Some y') => cmp x' y'
end.

Instance x21_SetType{a: Type} `{SetType a}: SetType (option a ):= {
   setElemCompare := maybeCompare setElemCompare
}.

Instance x20_Ord{a: Type} `{Ord a}: Ord (option a ):= {
     compare := maybeCompare compare;
     isLess := fun m1 => (fun m2 => (ordering_equal (maybeCompare compare m1 m2) LT));
     isLessEqual := fun m1 => (fun m2 => (let r := maybeCompare compare m1 m2 in (ordering_equal r LT) || (ordering_equal r EQ)));
     isGreater := fun m1 => (fun m2 => (ordering_equal (maybeCompare compare m1 m2) GT));
     isGreaterEqual := fun m1 => (fun m2 => (let r := maybeCompare compare m1 m2 in (ordering_equal r GT) || (ordering_equal r EQ)))
}.


Definition maybe {a b : Type} (d : b) (f : a -> b) (mb : option a ) : b:= match ( mb) with
  | Some a1 => f a1
  | None => d
end.

Definition isJust {a : Type} (mb : option a ) : bool := match ( mb) with
  | Some _ => true
  | None => false
end.

Definition isNothing {a : Type} (mb : option a ) : bool := match ( mb) with
  | Some _ => false
  | None => true
end.

Definition fromMaybe {a : Type} (d : a) (mb : option a ) : a:= match ( mb) with
   | Some v => v
   | None => d
end.


Definition bind {a b : Type} (mb : option a ) (f : a -> option b ) : option b := maybe None f mb.