{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE DerivingVia #-}
module Data.InternalQuiver.Path(
  -- * Path
  Path(Path, EmptyPath, NonEmptyPath),

  -- ** Constructing path
  path, emptyPath, singlePath,
  composePath,
  mapPath,
  concatPath,

  -- ** Partial construction functions
  errPath,
  errComposePath,
  errMapPath,

  -- ** Sum and Product of paths
  injectLeftPath, injectRightPath,
  separateSumPath,
  fstPath, sndPath,
  
  -- ** Unsafe
  unsafePath,

) where

import GHC.Stack (HasCallStack)
import Data.Maybe (fromMaybe)
import Control.Applicative ((<|>))
import Data.Functor.Classes (Show1, Show2)
import AutoLift (Reflected1(..), Reflected2(..))

import Data.InternalQuiver

-- * Path
data Path v e = UnsafePath v [e] v
    deriving (Path v e -> Path v e -> Bool
(Path v e -> Path v e -> Bool)
-> (Path v e -> Path v e -> Bool) -> Eq (Path v e)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall v e. (Eq e, Eq v) => Path v e -> Path v e -> Bool
$c== :: forall v e. (Eq e, Eq v) => Path v e -> Path v e -> Bool
== :: Path v e -> Path v e -> Bool
$c/= :: forall v e. (Eq e, Eq v) => Path v e -> Path v e -> Bool
/= :: Path v e -> Path v e -> Bool
Eq, Eq (Path v e)
Eq (Path v e) =>
(Path v e -> Path v e -> Ordering)
-> (Path v e -> Path v e -> Bool)
-> (Path v e -> Path v e -> Bool)
-> (Path v e -> Path v e -> Bool)
-> (Path v e -> Path v e -> Bool)
-> (Path v e -> Path v e -> Path v e)
-> (Path v e -> Path v e -> Path v e)
-> Ord (Path v e)
Path v e -> Path v e -> Bool
Path v e -> Path v e -> Ordering
Path v e -> Path v e -> Path v e
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall v e. (Ord e, Ord v) => Eq (Path v e)
forall v e. (Ord e, Ord v) => Path v e -> Path v e -> Bool
forall v e. (Ord e, Ord v) => Path v e -> Path v e -> Ordering
forall v e. (Ord e, Ord v) => Path v e -> Path v e -> Path v e
$ccompare :: forall v e. (Ord e, Ord v) => Path v e -> Path v e -> Ordering
compare :: Path v e -> Path v e -> Ordering
$c< :: forall v e. (Ord e, Ord v) => Path v e -> Path v e -> Bool
< :: Path v e -> Path v e -> Bool
$c<= :: forall v e. (Ord e, Ord v) => Path v e -> Path v e -> Bool
<= :: Path v e -> Path v e -> Bool
$c> :: forall v e. (Ord e, Ord v) => Path v e -> Path v e -> Bool
> :: Path v e -> Path v e -> Bool
$c>= :: forall v e. (Ord e, Ord v) => Path v e -> Path v e -> Bool
>= :: Path v e -> Path v e -> Bool
$cmax :: forall v e. (Ord e, Ord v) => Path v e -> Path v e -> Path v e
max :: Path v e -> Path v e -> Path v e
$cmin :: forall v e. (Ord e, Ord v) => Path v e -> Path v e -> Path v e
min :: Path v e -> Path v e -> Path v e
Ord)

instance (Show v, Show e) => Show (Path v e) where
  showsPrec :: Int -> Path v e -> ShowS
showsPrec Int
p (UnsafePath v
v0 [e]
es v
v1) =
    Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ (String
"Path " ++) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> v -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 v
v0 ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
space ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [e] -> ShowS
forall a. Show a => [a] -> ShowS
showList [e]
es ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
space ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> v -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 v
v1
      where
        space :: ShowS
space = (String
" " ++) 

deriving via (Reflected1 (Path v))
  instance (Show v) => Show1 (Path v)

deriving via (Reflected2 Path)
  instance Show2 Path

-- Pattern synonyms

pattern Path :: v -> [e] -> v -> Path v e
pattern $mPath :: forall {r} {v} {e}.
Path v e -> (v -> [e] -> v -> r) -> ((# #) -> r) -> r
Path v0 es v1 <- UnsafePath v0 es v1

{-# COMPLETE Path #-}

pattern EmptyPath :: v -> Path v e
pattern $mEmptyPath :: forall {r} {v} {e}. Path v e -> (v -> r) -> ((# #) -> r) -> r
EmptyPath v0 <- UnsafePath v0 [] _

pattern NonEmptyPath :: e -> [e] -> Path v e
pattern $mNonEmptyPath :: forall {r} {e} {v}.
Path v e -> (e -> [e] -> r) -> ((# #) -> r) -> r
NonEmptyPath e es <- UnsafePath _ (e:es) _

{-# COMPLETE EmptyPath, NonEmptyPath #-}

instance IQuiver v (Path v e) where
  src :: Path v e -> v
src (UnsafePath v
v0 [e]
_ v
_) = v
v0
  tgt :: Path v e -> v
tgt (UnsafePath v
_ [e]
_ v
v1) = v
v1

-- Safe constructors

path :: (Eq v, IQuiver v e) => v -> [e] -> v -> Maybe (Path v e)
path :: forall v e.
(Eq v, IQuiver v e) =>
v -> [e] -> v -> Maybe (Path v e)
path v
v0 [e]
edges v
v1
  | Bool
valid     = Path v e -> Maybe (Path v e)
forall a. a -> Maybe a
Just (Path v e -> Maybe (Path v e)) -> Path v e -> Maybe (Path v e)
forall a b. (a -> b) -> a -> b
$ v -> [e] -> v -> Path v e
forall v e. v -> [e] -> v -> Path v e
UnsafePath v
v0 [e]
edges v
v1
  | Bool
otherwise = Maybe (Path v e)
forall a. Maybe a
Nothing
  where
    valid :: Bool
valid = v -> [e] -> Bool
forall {e}. IQuiver v e => v -> [e] -> Bool
go v
v0 [e]
edges
    go :: v -> [e] -> Bool
go v
v []     = v
v v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v1
    go v
v (e
e:[e]
es) = v
v v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== e -> v
forall v e. IQuiver v e => e -> v
src e
e Bool -> Bool -> Bool
&& v -> [e] -> Bool
go (e -> v
forall v e. IQuiver v e => e -> v
tgt e
e) [e]
es

emptyPath :: v -> Path v e
emptyPath :: forall v e. v -> Path v e
emptyPath v
v = v -> [e] -> v -> Path v e
forall v e. v -> [e] -> v -> Path v e
UnsafePath v
v [] v
v

singlePath :: IQuiver v e => e -> Path v e
singlePath :: forall v e. IQuiver v e => e -> Path v e
singlePath e
e = v -> [e] -> v -> Path v e
forall v e. v -> [e] -> v -> Path v e
UnsafePath (e -> v
forall v e. IQuiver v e => e -> v
src e
e) [e
e] (e -> v
forall v e. IQuiver v e => e -> v
tgt e
e)

composePath :: Eq v => Path v e -> Path v e -> Maybe (Path v e)
composePath :: forall v e. Eq v => Path v e -> Path v e -> Maybe (Path v e)
composePath (UnsafePath v
v0 [e]
es v
v1) (UnsafePath v
v1' [e]
es' v
v2')
  | v
v1 v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v1' = Path v e -> Maybe (Path v e)
forall a. a -> Maybe a
Just (Path v e -> Maybe (Path v e)) -> Path v e -> Maybe (Path v e)
forall a b. (a -> b) -> a -> b
$ v -> [e] -> v -> Path v e
forall v e. v -> [e] -> v -> Path v e
UnsafePath v
v0 ([e]
es [e] -> [e] -> [e]
forall a. [a] -> [a] -> [a]
++ [e]
es') v
v2'
  | Bool
otherwise = Maybe (Path v e)
forall a. Maybe a
Nothing

mapPath :: (IQuiver v' e', Eq v') => (v -> v') -> (e -> e') -> Path v e -> Maybe (Path v' e')
mapPath :: forall v' e' v e.
(IQuiver v' e', Eq v') =>
(v -> v') -> (e -> e') -> Path v e -> Maybe (Path v' e')
mapPath v -> v'
f0 e -> e'
f1 (UnsafePath v
v0 [e]
es v
v1) = v' -> [e'] -> v' -> Maybe (Path v' e')
forall v e.
(Eq v, IQuiver v e) =>
v -> [e] -> v -> Maybe (Path v e)
path (v -> v'
f0 v
v0) (e -> e'
f1 (e -> e') -> [e] -> [e']
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [e]
es) (v -> v'
f0 v
v1)

concatPath :: Path v (Path v e) -> Path v e
concatPath :: forall v e. Path v (Path v e) -> Path v e
concatPath (UnsafePath v
v0 [Path v e]
pathes v
v1) = v -> [e] -> v -> Path v e
forall v e. v -> [e] -> v -> Path v e
UnsafePath v
v0 [e]
allEdges v
v1
  where
    allEdges :: [e]
allEdges = [Path v e]
pathes [Path v e] -> (Path v e -> [e]) -> [e]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(UnsafePath v
_ [e]
es v
_) -> [e]
es

-- Partial constructors

errPath :: HasCallStack => (Eq v, Show v, IQuiver v e) => v -> [e] -> v -> Path v e
errPath :: forall v e.
(HasCallStack, Eq v, Show v, IQuiver v e) =>
v -> [e] -> v -> Path v e
errPath v
v0 [e]
edges v
v1 = case v -> [e] -> v -> Maybe (Path v e)
forall v e.
(Eq v, IQuiver v e) =>
v -> [e] -> v -> Maybe (Path v e)
path v
v0 [e]
edges v
v1 of
  Maybe (Path v e)
Nothing -> String -> Path v e
forall a. HasCallStack => String -> a
error String
errMsg
  Just Path v e
p -> Path v e
p
  where
    errMsg :: String
errMsg = String
"Unmatched endpoinds in path: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
pathTypeStr
    pathTypeStr :: String
pathTypeStr = v -> [e] -> String
forall {e}. IQuiver v e => v -> [e] -> String
go v
v0 [e]
edges
    showExpect :: a -> a -> String
showExpect a
v a
v'
      | a
v a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
v'   = a -> String
forall a. Show a => a -> String
show a
v
      | Bool
otherwise = a -> String
forall a. Show a => a -> String
show a
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" (!!) " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
v'
    go :: v -> [e] -> String
go v
v []     = v -> v -> String
forall {a}. (Eq a, Show a) => a -> a -> String
showExpect v
v v
v1
    go v
v (e
e:[e]
es) = v -> v -> String
forall {a}. (Eq a, Show a) => a -> a -> String
showExpect v
v (e -> v
forall v e. IQuiver v e => e -> v
src e
e) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ v -> [e] -> String
go (e -> v
forall v e. IQuiver v e => e -> v
tgt e
e) [e]
es

errMapPath :: HasCallStack => (IQuiver v' e', Eq v') => (v -> v') -> (e -> e') -> Path v e -> Path v' e'
errMapPath :: forall v' e' v e.
(HasCallStack, IQuiver v' e', Eq v') =>
(v -> v') -> (e -> e') -> Path v e -> Path v' e'
errMapPath v -> v'
f0 e -> e'
f1 Path v e
p = Path v' e' -> Maybe (Path v' e') -> Path v' e'
forall a. a -> Maybe a -> a
fromMaybe (String -> Path v' e'
forall a. HasCallStack => String -> a
error String
"Invalid morphism between quiver!") (Maybe (Path v' e') -> Path v' e')
-> Maybe (Path v' e') -> Path v' e'
forall a b. (a -> b) -> a -> b
$ (v -> v') -> (e -> e') -> Path v e -> Maybe (Path v' e')
forall v' e' v e.
(IQuiver v' e', Eq v') =>
(v -> v') -> (e -> e') -> Path v e -> Maybe (Path v' e')
mapPath v -> v'
f0 e -> e'
f1 Path v e
p

errComposePath :: HasCallStack => (Show v, Eq v) => Path v e -> Path v e -> Path v e
errComposePath :: forall v e.
(HasCallStack, Show v, Eq v) =>
Path v e -> Path v e -> Path v e
errComposePath Path v e
p1 Path v e
p2 = case Path v e -> Path v e -> Maybe (Path v e)
forall v e. Eq v => Path v e -> Path v e -> Maybe (Path v e)
composePath Path v e
p1 Path v e
p2 of
  Maybe (Path v e)
Nothing -> String -> Path v e
forall a. HasCallStack => String -> a
error String
errMsg
  Just Path v e
p -> Path v e
p
  where
    showType :: e -> String
showType e
p = a -> String
forall a. Show a => a -> String
show (e -> a
forall v e. IQuiver v e => e -> v
src e
p) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"->" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show (e -> a
forall v e. IQuiver v e => e -> v
tgt e
p)
    errMsg :: String
errMsg = String
"Unmatched endpoints of two paths: (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Path v e -> String
forall {a} {e}. (IQuiver a e, Show a) => e -> String
showType Path v e
p1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") >!> (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Path v e -> String
forall {a} {e}. (IQuiver a e, Show a) => e -> String
showType Path v e
p2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

-- ** Sum and product

injectLeftPath :: Path v e -> Path (Either v w) (Either e f)
injectLeftPath :: forall v e w f. Path v e -> Path (Either v w) (Either e f)
injectLeftPath (UnsafePath v
v0 [e]
es v
v1) = Either v w
-> [Either e f] -> Either v w -> Path (Either v w) (Either e f)
forall v e. v -> [e] -> v -> Path v e
UnsafePath (v -> Either v w
forall a b. a -> Either a b
Left v
v0) (e -> Either e f
forall a b. a -> Either a b
Left (e -> Either e f) -> [e] -> [Either e f]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [e]
es) (v -> Either v w
forall a b. a -> Either a b
Left v
v1)

injectRightPath :: Path w f -> Path (Either v w) (Either e f)
injectRightPath :: forall w f v e. Path w f -> Path (Either v w) (Either e f)
injectRightPath (UnsafePath w
w0 [f]
fs w
w1) = Either v w
-> [Either e f] -> Either v w -> Path (Either v w) (Either e f)
forall v e. v -> [e] -> v -> Path v e
UnsafePath (w -> Either v w
forall a b. b -> Either a b
Right w
w0) (f -> Either e f
forall a b. b -> Either a b
Right (f -> Either e f) -> [f] -> [Either e f]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [f]
fs) (w -> Either v w
forall a b. b -> Either a b
Right w
w1)

separateSumPath :: Path (Either v w) (Either e f) -> Either (Path v e) (Path w f)
separateSumPath :: forall v w e f.
Path (Either v w) (Either e f) -> Either (Path v e) (Path w f)
separateSumPath (UnsafePath Either v w
vw0 [Either e f]
edges Either v w
vw1) = Either (Path v e) (Path w f)
-> Maybe (Either (Path v e) (Path w f))
-> Either (Path v e) (Path w f)
forall a. a -> Maybe a -> a
fromMaybe Either (Path v e) (Path w f)
forall {a}. a
err (Maybe (Either (Path v e) (Path w f))
forall {b}. Maybe (Either (Path v e) b)
leftPath Maybe (Either (Path v e) (Path w f))
-> Maybe (Either (Path v e) (Path w f))
-> Maybe (Either (Path v e) (Path w f))
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe (Either (Path v e) (Path w f))
forall {a}. Maybe (Either a (Path w f))
rightPath)
  where
    err :: a
err = String -> a
forall a. HasCallStack => String -> a
error String
"should not happen for a valid path"
    getLeft :: Either b b -> Maybe b
getLeft Either b b
ab  = do { Left b
a <- Either b b -> Maybe (Either b b)
forall a. a -> Maybe a
Just Either b b
ab; b -> Maybe b
forall a. a -> Maybe a
Just b
a }
    getRight :: Either a b -> Maybe b
getRight Either a b
ab = do { Right b
b <- Either a b -> Maybe (Either a b)
forall a. a -> Maybe a
Just Either a b
ab; b -> Maybe b
forall a. a -> Maybe a
Just b
b }
    leftPath :: Maybe (Either (Path v e) b)
leftPath = Path v e -> Either (Path v e) b
forall a b. a -> Either a b
Left (Path v e -> Either (Path v e) b)
-> Maybe (Path v e) -> Maybe (Either (Path v e) b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (v -> [e] -> v -> Path v e
forall v e. v -> [e] -> v -> Path v e
UnsafePath (v -> [e] -> v -> Path v e)
-> Maybe v -> Maybe ([e] -> v -> Path v e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either v w -> Maybe v
forall {b} {b}. Either b b -> Maybe b
getLeft Either v w
vw0 Maybe ([e] -> v -> Path v e) -> Maybe [e] -> Maybe (v -> Path v e)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Either e f -> Maybe e) -> [Either e f] -> Maybe [e]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Either e f -> Maybe e
forall {b} {b}. Either b b -> Maybe b
getLeft [Either e f]
edges Maybe (v -> Path v e) -> Maybe v -> Maybe (Path v e)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Either v w -> Maybe v
forall {b} {b}. Either b b -> Maybe b
getLeft Either v w
vw1)
    rightPath :: Maybe (Either a (Path w f))
rightPath = Path w f -> Either a (Path w f)
forall a b. b -> Either a b
Right (Path w f -> Either a (Path w f))
-> Maybe (Path w f) -> Maybe (Either a (Path w f))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (w -> [f] -> w -> Path w f
forall v e. v -> [e] -> v -> Path v e
UnsafePath (w -> [f] -> w -> Path w f)
-> Maybe w -> Maybe ([f] -> w -> Path w f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either v w -> Maybe w
forall {a} {b}. Either a b -> Maybe b
getRight Either v w
vw0 Maybe ([f] -> w -> Path w f) -> Maybe [f] -> Maybe (w -> Path w f)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Either e f -> Maybe f) -> [Either e f] -> Maybe [f]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Either e f -> Maybe f
forall {a} {b}. Either a b -> Maybe b
getRight [Either e f]
edges Maybe (w -> Path w f) -> Maybe w -> Maybe (Path w f)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Either v w -> Maybe w
forall {a} {b}. Either a b -> Maybe b
getRight Either v w
vw1)

fstPath :: Path (v,w) (e,f) -> Path v e
fstPath :: forall v w e f. Path (v, w) (e, f) -> Path v e
fstPath (UnsafePath (v, w)
vw0 [(e, f)]
edges (v, w)
vw1) = v -> [e] -> v -> Path v e
forall v e. v -> [e] -> v -> Path v e
UnsafePath ((v, w) -> v
forall a b. (a, b) -> a
fst (v, w)
vw0) ((e, f) -> e
forall a b. (a, b) -> a
fst ((e, f) -> e) -> [(e, f)] -> [e]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(e, f)]
edges) ((v, w) -> v
forall a b. (a, b) -> a
fst (v, w)
vw1)

sndPath :: Path (v,w) (e,f) -> Path w f
sndPath :: forall v w e f. Path (v, w) (e, f) -> Path w f
sndPath (UnsafePath (v, w)
vw0 [(e, f)]
edges (v, w)
vw1) = w -> [f] -> w -> Path w f
forall v e. v -> [e] -> v -> Path v e
UnsafePath ((v, w) -> w
forall a b. (a, b) -> b
snd (v, w)
vw0) ((e, f) -> f
forall a b. (a, b) -> b
snd ((e, f) -> f) -> [(e, f)] -> [f]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(e, f)]
edges) ((v, w) -> w
forall a b. (a, b) -> b
snd (v, w)
vw1)

-- ** Unsafe path construction

unsafePath :: v -> [e] -> v -> Path v e
unsafePath :: forall v e. v -> [e] -> v -> Path v e
unsafePath = v -> [e] -> v -> Path v e
forall v e. v -> [e] -> v -> Path v e
UnsafePath