{-# LANGUAGE AllowAmbiguousTypes #-} -- For isSort and kIsSort
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# 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
  , hasAnySort
  , kIsSort
  , kHasAnySort
  ) where

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

import GHC.Exts ( Constraint )

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

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

class EmptyConstraint (e :: Family) 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 :: Node) 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 :: forall (e :: Family) b. 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 :: forall (e :: Family) b. Sum fs e b -> Maybe (b :~: l)
kdyncase = forall (cxt :: Node -> Constraint) (fs :: [Node]) (a :: Family) e
       b.
All cxt fs =>
(forall (f :: Node). cxt f => f a e -> b) -> Sum fs a e -> b
caseCxt @(KDynCaseFlip l) f e b -> Maybe (b :~: l)
forall (e :: Family) b. f e b -> Maybe (b :~: l)
forall (f :: Node). KDynCaseFlip l f => f e b -> Maybe (b :~: l)
forall (f :: Node) a (e :: Family) b.
KDynCase f a =>
f e b -> Maybe (b :~: a)
kdyncase

instance {-# OVERLAPPING #-} (KDynCase f l) => KDynCase (f :&: a) l where
  kdyncase :: forall (e :: Family) b. (:&:) f a e b -> Maybe (b :~: l)
kdyncase = f e b -> Maybe (b :~: l)
forall (e :: Family) b. f e b -> Maybe (b :~: l)
forall (f :: Node) a (e :: Family) 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 (a :: Family). (:&:) f a a :-> f a
forall (s :: Node) (s' :: Node) (a :: Family).
RemA s s' =>
s a :-> s' a
remA

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

instance (KDynCase f l, DynCase a l) => DynCase (Cxt h f a) l where
  dyncase :: forall b. Cxt h f a b -> Maybe (b :~: l)
dyncase (Term f (Cxt h f a) b
x) = f (Cxt h f a) b -> Maybe (b :~: l)
forall (e :: Family) b. f e b -> Maybe (b :~: l)
forall (f :: Node) a (e :: Family) b.
KDynCase f a =>
f e b -> Maybe (b :~: a)
kdyncase f (Cxt h f a) b
x
  dyncase (Hole a b
x) = a b -> Maybe (b :~: l)
forall b. a b -> Maybe (b :~: l)
forall (f :: Family) 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 :: forall (f :: Family) l l'. DynCase f l => f l' -> Maybe (f l)
dynProj f l'
x = case (f l' -> Maybe (l' :~: l)
forall b. f b -> Maybe (b :~: l)
forall (f :: Family) a b. DynCase f a => f b -> Maybe (b :~: a)
dyncase f l'
x :: Maybe (l' :~: l)) of
              Just 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
f l'
(l' ~ l) => f l
x)
              Maybe (l' :~: l)
Nothing -> Maybe (f l)
forall a. Maybe a
Nothing

-- | Equivalent to @`fromJust` . `dynProj`@
fromDynProj :: (DynCase f l) => f l' -> f l
fromDynProj :: forall (f :: Family) l l'. DynCase f l => f l' -> f l
fromDynProj 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 :: Family) 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 :: forall (f :: Family) l. DynCase f l => E f -> Maybe (f l)
caseE = (f :=> Maybe (f l)) -> E f -> Maybe (f l)
forall (f :: Family) b. (f :=> b) -> E f -> b
runE f i -> Maybe (f l)
f :=> Maybe (f l)
forall (f :: Family) 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 :: forall (f :: Family) l r i.
DynCase f l =>
(f l -> r) -> f i -> r -> r
caseDyn f l -> r
f f i
t 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 :: Family) 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 :: forall (f :: Node) l l'.
(DynCase (HFix f) l, HFoldable f) =>
HFix f l' -> [HFix f l]
subterms HFix f l'
x = [ HFix f l
y | Just 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 :: Family) 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)]
HFix f :=> [E (HFix f)]
forall (f :: Node) h (a :: Family).
HFoldable f =>
Cxt h f a :=> [E (Cxt h f a)]
subs HFix f l'
x]

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

-- |
-- @hasAnySort \@ls@ returns a boolean function that tests
-- whether a term has any sort in the list of sorts @ls@
-- 
-- Example usage: @hasAnySort \@'[FunctionDefL, FunctionDeclL] t@
hasAnySort :: forall (ls :: [Sort]) e. (All (DynCase e) ls) => forall i. e i -> Bool
hasAnySort :: forall (ls :: [*]) (e :: Family) i.
All (DynCase e) ls =>
e i -> Bool
hasAnySort e i
t = [Bool] -> Bool
forall (t :: Family). Foldable t => t Bool -> Bool
or ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ forall {k} (cxt :: k -> Constraint) (fs :: [k]) a.
All cxt fs =>
(forall (f :: k). cxt f => Proxy f -> a) -> [a]
forall (cxt :: * -> Constraint) (fs :: [*]) a.
All cxt fs =>
(forall f. cxt f => Proxy f -> a) -> [a]
mapAll @(DynCase e) @ls Proxy f -> Bool
forall f. DynCase e f => Proxy f -> Bool
checkSort
  where
    checkSort :: forall j. (DynCase e j) => Proxy j -> Bool
    checkSort :: forall f. DynCase e f => Proxy f -> Bool
checkSort Proxy j
_ = forall l (e :: Family) i. DynCase e l => e i -> Bool
isSort @j e i
t

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

-- |Like `hasAnySort`, but runs on (unwrapped) nodes rather than terms.
kHasAnySort :: forall (ls :: [Sort]) f. (All (KDynCase f) ls) => forall i e. f e i -> Bool
kHasAnySort :: forall (ls :: [*]) (f :: Node) i (e :: Family).
All (KDynCase f) ls =>
f e i -> Bool
kHasAnySort f e i
t = [Bool] -> Bool
forall (t :: Family). Foldable t => t Bool -> Bool
or ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ forall {k} (cxt :: k -> Constraint) (fs :: [k]) a.
All cxt fs =>
(forall (f :: k). cxt f => Proxy f -> a) -> [a]
forall (cxt :: * -> Constraint) (fs :: [*]) a.
All cxt fs =>
(forall f. cxt f => Proxy f -> a) -> [a]
mapAll @(KDynCase f) @ls Proxy f -> Bool
forall f. KDynCase f f => Proxy f -> Bool
checkSort
  where
    checkSort :: forall j. (KDynCase f j) => Proxy j -> Bool
    checkSort :: forall f. KDynCase f f => Proxy f -> Bool
checkSort Proxy j
_ = forall l (f :: Node) i (e :: Family). KDynCase f l => f e i -> Bool
kIsSort @j f e i
t