module Data.Maybe.Properties

import Control.Function
import Data.Maybe

public export
data IsNothing : Maybe a -> Type where
  ItIsNothing : IsNothing Nothing

%inline
export
mapFusion : (s : Maybe a) -> (f . g) <$> s = f <$> [| g s |]
mapFusion Nothing = Refl
mapFusion (Just x) = Refl

%inline
export
extractIsJust : {x : Maybe a} -> (0 _ : IsJust x) -> (y ** x = Just y)
extractIsJust ItIsJust = (_ ** Refl)

%inline
export
extractIsNothing : {x : Maybe a} -> (0 _ : IsNothing x) -> x = Nothing
extractIsNothing ItIsNothing = Refl

%inline
export
mapIsJust : (0 f : a -> b) -> IsJust x -> IsJust (map f x)
mapIsJust f ItIsJust = ItIsJust

%inline
export
mapJustInverse :
  (0 f : a -> b) ->
  (x : Maybe a) ->
  (0 _ : map f x = Just y) ->
  (z ** (x = Just z, y = f z))
mapJustInverse f (Just x) prf = (x ** (Refl, sym $ injective prf))

%inline
export
mapNothing : (0 f : a -> b) -> IsNothing x -> IsNothing (map f x)
mapNothing f ItIsNothing = ItIsNothing

%inline
export
mapNothingInverse :
  (0 f : a -> b) ->
  (x : Maybe a) ->
  (0 _ : IsNothing (map f x)) ->
  IsNothing x
mapNothingInverse f Nothing prf = ItIsNothing

%inline
export
appIsJust : IsJust f -> IsJust x -> IsJust (f <*> x)
appIsJust ItIsJust ItIsJust = ItIsJust

%inline
export
appJustInverse :
  (f : Maybe (a -> b)) ->
  (x : Maybe a) ->
  (0 _ : f <*> x = Just y) ->
  (f' ** x' ** (f = Just f', x = Just x', y = f' x'))
appJustInverse (Just f) (Just x) prf = (f ** x ** (Refl, Refl, sym $ injective prf))

%inline
export
appLeftNothingIsNothing : IsNothing f -> (0 x : Maybe a) -> IsNothing (f <*> x)
appLeftNothingIsNothing ItIsNothing x = ItIsNothing

%inline
export
appRightNothingIsNothing : (f : Maybe (a -> b)) -> IsNothing x -> IsNothing (f <*> x)
appRightNothingIsNothing Nothing prf = ItIsNothing
appRightNothingIsNothing (Just f) ItIsNothing = ItIsNothing

%inline
export
appNothingInverse :
  (f : Maybe (a -> b)) ->
  (x : Maybe a) ->
  (0 _ : IsNothing (f <*> x)) ->
  Either (IsNothing f) (IsNothing x)
appNothingInverse Nothing x prf = Left ItIsNothing
appNothingInverse (Just f) Nothing prf = Right ItIsNothing

%inline
export
bindNothing : {x : Maybe a} -> (0 ok : IsNothing x) -> (f : a -> Maybe b) -> IsNothing (x >>= f)
bindNothing ItIsNothing f = ItIsNothing