{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneDeriving, GeneralizedNewtypeDeriving #-}


-- |

-- Module      : OAlg.Structure.Oriented.Path

-- Description : paths.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

--

-- Paths

module OAlg.Structure.Oriented.Path
  (
    -- * Path

    Path(..), pthLength, pthOne, pthMlt

    
  ) where

import Data.Foldable
import Data.List (map,reverse,(++))

import OAlg.Prelude

import OAlg.Data.Canonical
import OAlg.Structure.Oriented.Definition
import OAlg.Structure.Oriented.Opposite
import OAlg.Structure.Exception

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

-- Path -


-- | a path in a 'Oriented' structure @__q__@ starting at a given point.

--

-- __Definition__ Let @__q__@ be a 'Oriented' structure and @p = 'Path' s [a 0..a (n-1)]@ a

-- path in @__q__@, then @p@ is 'valid' if and only if

--

-- (1) @s@ is 'valid' and @a i@ are 'valid' for all @i = 0..n-1@.

--

-- (2) @'start' (a (n-1)) '==' s@ and @'start' (a i) '==' 'end' (a (n+1))@ for all @i = 0..n-2@.

--

-- furthermore @n@ is called the __/length/__ of @p@.

--

-- __Note__ Paths admit a canonical embedding in to 'OAlg.Entity.Product.Product'.

data Path q = Path (Point q) [q]

deriving instance (Show q, ShowPoint q) => Show (Path q)
deriving instance (Eq q, EqPoint q) => Eq (Path q)

instance Foldable Path where
  foldr :: forall a b. (a -> b -> b) -> b -> Path a -> b
foldr a -> b -> b
op b
b (Path Point a
_ [a]
fs) = (a -> b -> b) -> b -> [a] -> b
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> b -> b
op b
b [a]
fs 

instance Oriented q => Validable (Path q) where
  valid :: Path q -> Statement
valid (Path Point q
s [])     = Point q -> Statement
forall a. Validable a => a -> Statement
valid Point q
s
  valid (Path Point q
s (q
f:[q]
gs)) = Point q -> Statement
forall a. Validable a => a -> Statement
valid Point q
s Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& q -> Statement
forall a. Validable a => a -> Statement
valid q
f Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& Point q -> q -> [q] -> Statement
forall {t}. Oriented t => Point t -> t -> [t] -> Statement
vld Point q
s q
f [q]
gs where
    vld :: Point t -> t -> [t] -> Statement
vld Point t
s t
f []     = t -> Point t
forall q. Oriented q => q -> Point q
start t
f Point t -> Point t -> Statement
forall a. Eq a => a -> a -> Statement
.==. Point t
s
    vld Point t
s t
f (t
g:[t]
gs) = t -> Statement
forall a. Validable a => a -> Statement
valid t
g Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& t -> Point t
forall q. Oriented q => q -> Point q
start t
f Point t -> Point t -> Statement
forall a. Eq a => a -> a -> Statement
.==. t -> Point t
forall q. Oriented q => q -> Point q
end t
g Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& Point t -> t -> [t] -> Statement
vld Point t
s t
g [t]
gs 

type instance Point (Path q) = Point q
instance ShowPoint q => ShowPoint (Path q)
instance EqPoint q => EqPoint (Path q)
instance SingletonPoint q => SingletonPoint (Path q)
instance ValidablePoint q => ValidablePoint (Path q)
instance TypeablePoint q => TypeablePoint (Path q)
instance Oriented q => Oriented (Path q) where
  orientation :: Path q -> Orientation (Point (Path q))
orientation (Path Point q
s [])    = Point q
sPoint q -> Point q -> Orientation (Point q)
forall p. p -> p -> Orientation p
:>Point q
s
  orientation (Path Point q
s (q
f:[q]
_)) = Point q
sPoint q -> Point q -> Orientation (Point q)
forall p. p -> p -> Orientation p
:>q -> Point q
forall q. Oriented q => q -> Point q
end q
f

instance Oriented q => Embeddable q (Path q) where
  inj :: q -> Path q
inj q
f = Point q -> [q] -> Path q
forall q. Point q -> [q] -> Path q
Path (q -> Point q
forall q. Oriented q => q -> Point q
start q
f) [q
f]

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

-- Path - Duality -


type instance Dual (Path q) = Path (Op q)

instance Oriented q => Dualisable (Path q) where
  toDual :: Path q -> Dual (Path q)
toDual p :: Path q
p@(Path Point q
_ [q]
fs)   = Point (Op q) -> [Op q] -> Path (Op q)
forall q. Point q -> [q] -> Path q
Path (Path q -> Point (Path q)
forall q. Oriented q => q -> Point q
end Path q
p) ([Op q] -> [Op q]
forall a. [a] -> [a]
reverse ([Op q] -> [Op q]) -> [Op q] -> [Op q]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (q -> Op q) -> [q] -> [Op q]
forall a b. (a -> b) -> [a] -> [b]
map q -> Op q
forall x. x -> Op x
Op [q]
fs)
  fromDual :: Dual (Path q) -> Path q
fromDual p :: Dual (Path q)
p@(Path Point (Op q)
_ [Op q]
fs) = Point q -> [q] -> Path q
forall q. Point q -> [q] -> Path q
Path (Path (Op q) -> Point (Path (Op q))
forall q. Oriented q => q -> Point q
end Dual (Path q)
Path (Op q)
p) ([q] -> [q]
forall a. [a] -> [a]
reverse ([q] -> [q]) -> [q] -> [q]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (Op q -> q) -> [Op q] -> [q]
forall a b. (a -> b) -> [a] -> [b]
map Op q -> q
forall x. Op x -> x
fromOp [Op q]
fs)

instance Reflexive (Path q) where
  toBidual :: Path q -> Dual (Dual (Path q))
toBidual (Path Point q
s [q]
fs) = Point (Op (Op q)) -> [Op (Op q)] -> Path (Op (Op q))
forall q. Point q -> [q] -> Path q
Path Point q
Point (Op (Op q))
s ((q -> Op (Op q)) -> [q] -> [Op (Op q)]
forall a b. (a -> b) -> [a] -> [b]
map (Op q -> Op (Op q)
forall x. x -> Op x
Op (Op q -> Op (Op q)) -> (q -> Op q) -> q -> Op (Op q)
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. q -> Op q
forall x. x -> Op x
Op) [q]
fs)
  fromBidual :: Dual (Dual (Path q)) -> Path q
fromBidual (Path Point (Op (Op q))
s [Op (Op q)]
fs) = Point q -> [q] -> Path q
forall q. Point q -> [q] -> Path q
Path Point q
Point (Op (Op q))
s ((Op (Op q) -> q) -> [Op (Op q)] -> [q]
forall a b. (a -> b) -> [a] -> [b]
map (Op q -> q
forall x. Op x -> x
fromOp (Op q -> q) -> (Op (Op q) -> Op q) -> Op (Op q) -> q
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Op (Op q) -> Op q
forall x. Op x -> x
fromOp) [Op (Op q)]
fs)

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

-- pthLength -


-- | the length of a path.

pthLength :: Path q -> N
pthLength :: forall q. Path q -> N
pthLength (Path Point q
_ [q]
fs) = [q] -> N
forall {a} {a}. (Num a, Enum a) => [a] -> a
lgth [q]
fs where
  lgth :: [a] -> a
lgth []     = a
0
  lgth (a
_:[a]
fs) = a -> a
forall a. Enum a => a -> a
succ ([a] -> a
lgth [a]
fs)
  
instance LengthN (Path q) where
  lengthN :: Path q -> N
lengthN = Path q -> N
forall q. Path q -> N
pthLength

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

-- pthOne -


-- | path of length 0 at the given point.

pthOne :: Point q -> Path q
pthOne :: forall q. Point q -> Path q
pthOne Point q
s = Point q -> [q] -> Path q
forall q. Point q -> [q] -> Path q
Path Point q
s []

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

-- pthMlt -


-- | composition of two paths.

pthMlt :: Oriented q => Path q -> Path q -> Path q
pthMlt :: forall q. Oriented q => Path q -> Path q -> Path q
pthMlt (Path Point q
s [q]
fs) p :: Path q
p@(Path Point q
t [q]
gs)
  | Point q
s Point q -> Point q -> Bool
forall a. Eq a => a -> a -> Bool
== Path q -> Point (Path q)
forall q. Oriented q => q -> Point q
end Path q
p = Point q -> [q] -> Path q
forall q. Point q -> [q] -> Path q
Path Point q
t ([q]
fs[q] -> [q] -> [q]
forall a. [a] -> [a] -> [a]
++[q]
gs)
  | Bool
otherwise  = ArithmeticException -> Path q
forall a e. Exception e => e -> a
throw ArithmeticException
NotMultiplicable