{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Control.FAlternative where

import Data.List.NonEmpty (NonEmpty(..))


data Fallible = Fallible | Infallible
  deriving (Show)

data SFallible fail where
  SFallible :: SFallible 'Fallible
  SInfallible :: SFallible 'Infallible

class KnownFallible fail where knownFallible :: SFallible fail
instance KnownFallible 'Fallible where knownFallible = SFallible
instance KnownFallible 'Infallible where knownFallible = SInfallible


infixr 3 <|>>

class (forall fail. Applicative (f fail)) => FAlternative f where
  faempty :: f 'Fallible a
  (<|>>) :: f 'Fallible a -> f fail a -> f fail a
  noFail :: f 'Infallible a -> f fail a

toFallible :: forall fail f a. (FAlternative f, KnownFallible fail) => f fail a -> f 'Fallible a
toFallible = case knownFallible @fail of
               SFallible -> id
               SInfallible -> noFail

faasum :: FAlternative f => [f 'Fallible a] -> f fail a -> f fail a
faasum l p = foldr (<|>>) p l

faasum' :: FAlternative f => [f 'Fallible a] -> f 'Fallible a
faasum' l = faasum l faempty

famany :: FAlternative f => f 'Fallible a -> f 'Infallible [a]
famany p = ((:) <$> p <*> noFail (famany p)) <|>> pure []

fasome :: FAlternative f => f 'Fallible a -> f 'Fallible (NonEmpty a)
fasome p = (:|) <$> p <*> noFail (famany p)

faguard :: FAlternative f => Bool -> f 'Fallible ()
faguard True = pure ()
faguard False = faempty

faguardM :: (FAlternative f, Monad (f 'Fallible), KnownFallible fail)
         => f fail Bool -> f 'Fallible ()
faguardM p = toFallible p >>= faguard

faoptional :: FAlternative f => f 'Fallible a -> f 'Infallible (Maybe a)
faoptional p = (Just <$> p) <|>> pure Nothing

facatch :: FAlternative f => f fail a -> f 'Fallible a -> f fail a
facatch = flip (<|>>)