{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}
{-# OPTIONS_GHC -Wno-unused-type-patterns #-}
module Crem.Topology
( Topology (..)
, TopologySym0
, STopology (..)
, AllowTransition (..)
, AllowedTransition (..)
, trivialTopology
, sTrivialTopology
, TrivialTopology
, allowAllTopology
, sAllowAllTopology
, AllowAllTopology
)
where
import "singletons-base" Data.Singletons.Base.TH
import "singletons-base" Prelude.Singletons
$( singletons
[d|
newtype Topology vertex = Topology
{edges :: [(vertex, [vertex])]}
|]
)
data AllowTransition (topology :: Topology vertex) (initial :: vertex) (final :: vertex) where
AllowIdentityEdge :: AllowTransition topology a a
AllowFirstEdge :: AllowTransition ('Topology ('(a, b ': l1) ': l2)) a b
AllowAddingEdge
:: AllowTransition ('Topology ('(a, l1) ': l2)) a b
-> AllowTransition ('Topology ('(a, x ': l1) ': l2)) a b
AllowAddingVertex
:: AllowTransition ('Topology map) a b
-> AllowTransition ('Topology (x ': map)) a b
class AllowedTransition (topology :: Topology vertex) (initial :: vertex) (final :: vertex) where
allowsTransition :: AllowTransition topology initial final
instance {-# INCOHERENT #-} AllowedTransition ('Topology ('(a, b ': l1) ': l2)) a b where
allowsTransition :: AllowTransition ('Topology ('(a, b : l1) : l2)) a b
allowsTransition = AllowTransition ('Topology ('(a, b : l1) : l2)) a b
forall vertex (a :: vertex) (b :: vertex) (l1 :: [vertex])
(l2 :: [(vertex, [vertex])]).
AllowTransition ('Topology ('(a, b : l1) : l2)) a b
AllowFirstEdge
instance {-# INCOHERENT #-} AllowedTransition ('Topology ('(a, l1) ': l2)) a b => AllowedTransition ('Topology ('(a, x ': l1) ': l2)) a b where
allowsTransition :: AllowTransition ('Topology ('(a, x : l1) : l2)) a b
allowsTransition =
AllowTransition ('Topology ('(a, l1) : l2)) a b
-> AllowTransition ('Topology ('(a, x : l1) : l2)) a b
forall {vertex} (a :: vertex) (k1 :: [vertex])
(m :: [(vertex, [vertex])]) (b :: vertex) (k1 :: vertex).
AllowTransition ('Topology ('(a, k1) : m)) a b
-> AllowTransition ('Topology ('(a, k1 : k1) : m)) a b
AllowAddingEdge (AllowTransition ('Topology ('(a, l1) : l2)) a b
forall vertex (topology :: Topology vertex) (initial :: vertex)
(final :: vertex).
AllowedTransition topology initial final =>
AllowTransition topology initial final
allowsTransition :: AllowTransition ('Topology ('(a, l1) ': l2)) a b)
instance {-# INCOHERENT #-} AllowedTransition ('Topology map) a b => AllowedTransition ('Topology (x ': map)) a b where
allowsTransition :: AllowTransition ('Topology (x : map)) a b
allowsTransition =
AllowTransition ('Topology map) a b
-> AllowTransition ('Topology (x : map)) a b
forall {vertex} (k1 :: [(vertex, [vertex])]) (a :: vertex)
(b :: vertex) (m :: (vertex, [vertex])).
AllowTransition ('Topology k1) a b
-> AllowTransition ('Topology (m : k1)) a b
AllowAddingVertex (AllowTransition ('Topology map) a b
forall vertex (topology :: Topology vertex) (initial :: vertex)
(final :: vertex).
AllowedTransition topology initial final =>
AllowTransition topology initial final
allowsTransition :: AllowTransition ('Topology map) a b)
instance {-# INCOHERENT #-} AllowedTransition topology a a where
allowsTransition :: AllowTransition topology a a
allowsTransition = AllowTransition topology a a
forall vertex (topology :: Topology vertex) (a :: vertex).
AllowTransition topology a a
AllowIdentityEdge
$( singletons
[d|
trivialTopology :: Topology a
trivialTopology = Topology []
|]
)
$( singletons
[d|
allowAllTopology :: (Bounded a, Enum a) => Topology a
allowAllTopology = Topology [(a, [minBound .. maxBound]) | a <- [minBound .. maxBound]]
|]
)