{-# LANGUAGE
    AllowAmbiguousTypes,
    ConstraintKinds,
    DataKinds,
    PolyKinds,
    RankNTypes,
    TypeFamilies,
    TypeInType,
    TypeOperators,
    UndecidableInstances #-}

-- | Miscellaneous families.
module Fcf.Utils
  ( Error
  , TError
  , Constraints
  , TyEq
  , Stuck
  , IsBool(_If)
  , Case
  , Match()
  , type (-->)
  , Is
  , Any
  , Else

    -- * From "Data.Type.Bool"
  , If
  ) where

import Data.Kind (Constraint)
import Data.Type.Bool (If)
import GHC.TypeLits (Symbol, TypeError, ErrorMessage(..))

import Fcf.Core
import Fcf.Combinators (Pure)

-- | Type-level 'error'.
data Error :: Symbol -> Exp a
type instance Eval (Error msg) = TypeError ('Text msg)

-- | 'TypeError' as a fcf.
data TError :: ErrorMessage -> Exp a
type instance Eval (TError msg) = TypeError msg

-- | Conjunction of a list of constraints.
data Constraints :: [Constraint] -> Exp Constraint
type instance Eval (Constraints '[]) = (() :: Constraint)
type instance Eval (Constraints (a ': as)) = (a, Eval (Constraints as))

-- | Type equality.
--
-- === __Details__
--
-- The base library also defines a similar @('Type.Equality.==')@;
-- it differs from 'TyEq' in the following ways:
--
-- * 'TyEq' is heterogeneous: its arguments may have different kinds;
-- * 'TyEq' is reflexive: @TyEq a a@ always reduces to 'True' even if @a@ is
--   a variable.
data TyEq :: a -> b -> Exp Bool
type instance Eval (TyEq a b) = TyEqImpl a b

type family TyEqImpl (a :: k) (b :: l) :: Bool where
  TyEqImpl a a = 'True
  TyEqImpl a b = 'False

-- | A stuck type that can be used like a type-level 'undefined'.
type family Stuck :: a

-- * Reification

class IsBool (b :: Bool) where
  _If :: ((b ~ 'True) => r) -> ((b ~ 'False) => r) -> r

instance IsBool 'True  where _If :: (('True ~ 'True) => r) -> (('True ~ 'False) => r) -> r
_If ('True ~ 'True) => r
a ('True ~ 'False) => r
_ = r
('True ~ 'True) => r
a
instance IsBool 'False where _If :: (('False ~ 'True) => r) -> (('False ~ 'False) => r) -> r
_If ('False ~ 'True) => r
_ ('False ~ 'False) => r
b = r
('False ~ 'False) => r
b

-- * Case splitting

infix 0 -->

data Match j k
  = Match_ j k
  | Is_ (j -> Exp Bool) k
  | Any_ k
  | Else_ (j -> Exp k)

-- | (Limited) equivalent of @\\case { .. }@ syntax. Supports matching of exact
-- values ('-->') and final matches for any value ('Any') or for passing value
-- to subcomputation ('Else'). Examples:
--
-- @
-- type BoolToNat = 'Case'
--   [ 'True  '-->' 0
--   , 'False '-->' 1
--   ]
--
-- type NatToBool = 'Case'
--   [ 0 '-->' 'False
--   , 'Any'   'True
--   ]
--
-- type ZeroOneOrSucc = 'Case'
--   [ 0  '-->' 0
--   , 1  '-->' 1
--   , 'Else'   (('+') 1)
--   ]
-- @
data Case :: [Match j k] -> j -> Exp k
type instance Eval (Case ms a) = Case_ ms a

type family Case_ (ms :: [Match j k]) (a :: j) :: k where
  Case_ ('Match_ a' b : ms) a = Eval (If (TyEqImpl a' a) (Pure b) (Case ms a))
  Case_ ('Is_ p b    : ms) a = Case_ [ 'True  --> b
                                     , 'False --> Case_ ms a
                                     ] (p @@ a)
  Case_ ('Any_ b     : _ ) _ = b
  Case_ ('Else_ f    : _ ) a = f @@ a

-- | Match concrete type in 'Case'.
type (-->) = ('Match_ :: j -> k -> Match j k)

-- | Match on predicate being successful with type in 'Case'.
type Is = ('Is_ :: (j -> Exp Bool) -> k -> Match j k)

-- | Match any type in 'Case'. Should be used as a final branch.
--
-- Note: this identifier conflicts with 'Fcf.Class.Foldable.Any' (from "Fcf.Class.Foldable")
-- 'Data.Monoid.Any' (from "Data.Monoid"), and 'GHC.Exts.Any' (from "GHC.Exts").
--
-- We recommend importing this one qualified.
type Any = ('Any_ :: k -> Match j k)

-- | Pass type being matched in 'Case' to subcomputation. Should be used as a
-- final branch.
type Else = ('Else_ :: (j -> Exp k) -> Match j k)