{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}



-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Comp.Multi.Strategy.Classification
-- Copyright   :  James Koppel, 2013
-- License     :  BSD-style (see the LICENSE file in the distribution)
--
-- This module contains typeclasses and operations allowing dynamic casing on sorts.
-----------------------------------------------------------------------------


module Data.Comp.Multi.Strategy.Classification
  (
    DynCase(..)
  , KDynCase(..)
  , dynProj
  , fromDynProj
  , caseE
  , caseDyn
  , subterms
  , isSort
  , kIsSort
  ) where

import Data.Type.Equality ( (:~:)(..), gcastWith )
import Data.Maybe ( fromJust )
import Data.Proxy

import GHC.Exts ( Constraint )

import Data.Comp.Multi ( HFix, Sum, E, K, runE, caseH, (:&:), remA, Cxt(..), subs, NotSum, All, caseCxt )
import Data.Comp.Multi.HFoldable ( HFoldable )

--------------------------------------------------------------------------------

class EmptyConstraint (e :: * -> *) l
instance EmptyConstraint e l

-- |
-- This operation allows you to rediscover the label giving
-- the sort of a term by inspecting the term. It is mainly used
-- through the 'caseE' and 'dynProj' operators
class DynCase f a where
  -- | Determines whether a node has sort @a@
  dyncase :: f b -> Maybe (b :~: a)

-- | An instance @KDynCase f a@ defines an instance @DynCase (HFix f) a@
class KDynCase (f :: (* -> *) -> * -> *) a where
  kdyncase :: f e b -> Maybe (b :~: a)

-- Stop typeclass resolver from using this when it shouldn't
instance {-# OVERLAPPABLE #-} (NotSum f) => KDynCase f a where
  kdyncase :: f e b -> Maybe (b :~: a)
kdyncase = Maybe (b :~: a) -> f e b -> Maybe (b :~: a)
forall a b. a -> b -> a
const Maybe (b :~: a)
forall a. Maybe a
Nothing

class (KDynCase f l ) => KDynCaseFlip l f
instance (KDynCase f l) => KDynCaseFlip l f

instance {-# OVERLAPPING #-} (All (KDynCaseFlip l) fs) => KDynCase (Sum fs) l where
  kdyncase :: Sum fs e b -> Maybe (b :~: l)
kdyncase = Proxy (KDynCaseFlip l)
-> (forall (f :: (* -> *) -> * -> *).
    KDynCaseFlip l f =>
    f e b -> Maybe (b :~: l))
-> Sum fs e b
-> Maybe (b :~: l)
forall (cxt :: ((* -> *) -> * -> *) -> Constraint)
       (fs :: [(* -> *) -> * -> *]) (a :: * -> *) e b.
All cxt fs =>
Proxy cxt
-> (forall (f :: (* -> *) -> * -> *). cxt f => f a e -> b)
-> Sum fs a e
-> b
caseCxt (Proxy (KDynCaseFlip l)
forall k (t :: k). Proxy t
Proxy :: Proxy (KDynCaseFlip l)) forall (f :: (* -> *) -> * -> *).
KDynCaseFlip l f =>
f e b -> Maybe (b :~: l)
forall (f :: (* -> *) -> * -> *) a (e :: * -> *) b.
KDynCase f a =>
f e b -> Maybe (b :~: a)
kdyncase

instance {-# OVERLAPPING #-} (KDynCase f l) => KDynCase (f :&: a) l where
  kdyncase :: (:&:) f a e b -> Maybe (b :~: l)
kdyncase = f e b -> Maybe (b :~: l)
forall (f :: (* -> *) -> * -> *) a (e :: * -> *) b.
KDynCase f a =>
f e b -> Maybe (b :~: a)
kdyncase (f e b -> Maybe (b :~: l))
-> ((:&:) f a e b -> f e b) -> (:&:) f a e b -> Maybe (b :~: l)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:&:) f a e b -> f e b
forall (s :: (* -> *) -> * -> *) (s' :: (* -> *) -> * -> *)
       (a :: * -> *).
RemA s s' =>
s a :-> s' a
remA

instance DynCase (K a) b where
  dyncase :: K a b -> Maybe (b :~: b)
dyncase _ = Maybe (b :~: b)
forall a. Maybe a
Nothing

instance (KDynCase f l, DynCase a l) => DynCase (Cxt h f a) l where
  dyncase :: Cxt h f a b -> Maybe (b :~: l)
dyncase (Term x :: f (Cxt h f a) b
x) = f (Cxt h f a) b -> Maybe (b :~: l)
forall (f :: (* -> *) -> * -> *) a (e :: * -> *) b.
KDynCase f a =>
f e b -> Maybe (b :~: a)
kdyncase f (Cxt h f a) b
x
  dyncase (Hole x :: a b
x) = a b -> Maybe (b :~: l)
forall (f :: * -> *) a b. DynCase f a => f b -> Maybe (b :~: a)
dyncase a b
x

--------------------------------------------------------------------------------

-- | Takes a term @t@ of unknown sort. Returns @Just t@ if @t@ is of sort @l@, and @Nothing@ otherwise.
dynProj :: forall f l l'. (DynCase f l) => f l' -> Maybe (f l)
dynProj :: f l' -> Maybe (f l)
dynProj x :: f l'
x = case (f l' -> Maybe (l' :~: l)
forall (f :: * -> *) a b. DynCase f a => f b -> Maybe (b :~: a)
dyncase f l'
x :: Maybe (l' :~: l)) of
              Just p :: l' :~: l
p -> f l -> Maybe (f l)
forall a. a -> Maybe a
Just ((l' :~: l) -> ((l' ~ l) => f l) -> f l
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith l' :~: l
p f l'
(l' ~ l) => f l
x)
              Nothing -> Maybe (f l)
forall a. Maybe a
Nothing

-- | Equivalent to @`fromJust` . `dynProj`@
fromDynProj :: (DynCase f l) => f l' -> f l
fromDynProj :: f l' -> f l
fromDynProj x :: f l'
x = Maybe (f l) -> f l
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (f l) -> f l) -> Maybe (f l) -> f l
forall a b. (a -> b) -> a -> b
$ f l' -> Maybe (f l)
forall (f :: * -> *) l l'. DynCase f l => f l' -> Maybe (f l)
dynProj f l'
x

-- | Inspect an existentially-quantified sort to determine if it is of sort @l@
caseE :: (DynCase f l) => E f -> Maybe (f l)
caseE :: E f -> Maybe (f l)
caseE = (f :=> Maybe (f l)) -> E f -> Maybe (f l)
forall (f :: * -> *) b. (f :=> b) -> E f -> b
runE f :=> Maybe (f l)
forall (f :: * -> *) l l'. DynCase f l => f l' -> Maybe (f l)
dynProj

-- | Runs a sort-specific function on a term of unknown sort, returning a default value
--   if it is of the wrong sort
caseDyn :: (DynCase f l)
        => (f l -> r) -- ^ Function to run on term of sort @l@
        -> f i        -- ^ Term of unknown sort
        -> r          -- ^ Default value
        -> r
caseDyn :: (f l -> r) -> f i -> r -> r
caseDyn f :: f l -> r
f t :: f i
t r :: r
r = r -> (f l -> r) -> Maybe (f l) -> r
forall b a. b -> (a -> b) -> Maybe a -> b
maybe r
r f l -> r
f (f i -> Maybe (f l)
forall (f :: * -> *) l l'. DynCase f l => f l' -> Maybe (f l)
dynProj f i
t)

-- | Gives all subterms of any given sort of a term
subterms :: (DynCase (HFix f) l, HFoldable f) => HFix f l' -> [HFix f l]
subterms :: HFix f l' -> [HFix f l]
subterms x :: HFix f l'
x = [ HFix f l
y | Just y :: HFix f l
y <- (E (HFix f) -> Maybe (HFix f l))
-> [E (HFix f)] -> [Maybe (HFix f l)]
forall a b. (a -> b) -> [a] -> [b]
map E (HFix f) -> Maybe (HFix f l)
forall (f :: * -> *) l. DynCase f l => E f -> Maybe (f l)
caseE ([E (HFix f)] -> [Maybe (HFix f l)])
-> [E (HFix f)] -> [Maybe (HFix f l)]
forall a b. (a -> b) -> a -> b
$ HFix f l' -> [E (HFix f)]
forall (f :: (* -> *) -> * -> *).
HFoldable f =>
HFix f :=> [E (HFix f)]
subs HFix f l'
x]

-- | @isSort (Proxy :: Proxy l)@ returns a boolean function that tests whether a term has sort @l@
isSort :: forall e l. (DynCase e l) => Proxy l -> forall i. e i -> Bool
isSort :: Proxy l -> forall i. e i -> Bool
isSort _ x :: e i
x = case (e i -> Maybe (i :~: l)
forall (f :: * -> *) a b. DynCase f a => f b -> Maybe (b :~: a)
dyncase e i
x :: Maybe (_ :~: l)) of
  Just _  -> Bool
True
  Nothing -> Bool
False

-- | Like `isSort`, but runs on (unwrapped) nodes rather than terms.
kIsSort :: forall f l. (KDynCase f l) => Proxy l -> forall i e. f e i -> Bool
kIsSort :: Proxy l -> forall i (e :: * -> *). f e i -> Bool
kIsSort _ x :: f e i
x = case (f e i -> Maybe (i :~: l)
forall (f :: (* -> *) -> * -> *) a (e :: * -> *) b.
KDynCase f a =>
f e b -> Maybe (b :~: a)
kdyncase f e i
x :: Maybe (_ :~: l)) of
  Just _  -> Bool
True
  Nothing -> Bool
False