-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Showing
81 changed files
with
2,245 additions
and
1,300 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,69 @@ | ||
| >{-# LANGUAGE GADTs, DataKinds, KindSignatures, PolyKinds, TypeOperators #-} | ||
| >{-# LANGUAGE StandaloneDeriving, RankNTypes #-} | ||
| >{-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-} | ||
| >{-# LANGUAGE FunctionalDependencies, FlexibleContexts #-} | ||
| >module Math.Graph.Category where | ||
| >import Data.Set | ||
| >import Math.Tools.NaturalTransformation | ||
| >import Math.Tools.FixedPoint | ||
| >import qualified Control.Category as Cat | ||
| >import Prelude hiding ((.), id, Monad(..)) | ||
| >import qualified Prelude (Monad(..),id,(.)) | ||
|
|
||
| >class (Cat.Category arr, Cat.Category arr') => Adjunction2 arr arr' f g | ||
| > | f -> g, g -> f, arr -> arr', arr' -> arr where | ||
| > lad :: arr (f a) b -> arr' a (g b) | ||
| > rad :: arr' a (g b) -> arr (f a) b | ||
| > unit :: arr' a (g (f a)) | ||
| > counit :: arr (f (g b)) b | ||
|
|
||
| >class Category3 arr where | ||
| > point3 :: arr a a a | ||
| > line3 :: arr a a b | ||
| > rotate3 :: arr a b c -> arr b c a | ||
|
|
||
| compose3 :: arr a b c -> arr b d c -> arr d e c -> arr e f c -> arr f g c | ||
| -> arr ( | ||
|
|
||
| A-----G AC | ||
| /\ / \ | \ | ||
| / \ / \ | \ | ||
| B----C-----F ==> | FC | ||
| \ / \ / | / | ||
| \/ \ / | / | ||
| D----E DC | ||
|
|
||
| >class (Category3 arr, Category3 arr', Category3 arr'') | ||
| > => Adjunction3 arr arr' arr'' f g h | ||
| > | f -> g, g -> h, h -> f, arr -> arr', arr' -> arr'', arr'' -> arr where | ||
| > lad3 :: arr (f a) b c -> arr' a (g b) c | ||
| > mad3 :: arr' a (g b) c -> arr'' a b (h c) | ||
| > rad3 :: arr'' a b (h c) -> arr (f a) b c | ||
| > unit3 :: arr' a (g (f a)) (f a) | ||
| > munit3 :: arr'' (g b) b (h (g b)) | ||
| > counit3 :: arr (f (h c)) (h c) c | ||
|
|
||
| >data Iso (arr :: k -> k -> *) (a :: k) (b :: k) where | ||
| > (:<->:) :: arr a b -> arr b a -> Iso arr a b | ||
|
|
||
| >data NatT f g = NatT { unNatT :: forall a. f a -> g a } | ||
| >data NatIso f g = NatIso { unNatIso :: forall a. Iso (->) (f a) (g a) } | ||
|
|
||
| >data KleisliA a b = KleisliA { unKleisliA :: a -> IO b } | ||
|
|
||
| >instance Cat.Category NatT where | ||
| > id = NatT Cat.id | ||
| > (NatT f) . (NatT g) = NatT (f Cat.. g) | ||
|
|
||
| >instance Cat.Category KleisliA where | ||
| > id = KleisliA Prelude.return | ||
| > (KleisliA f) . (KleisliA g) = KleisliA $ \a -> g a Prelude.>>= f | ||
|
|
||
| >instance (Cat.Category arr) => Cat.Category (Iso arr) where | ||
| > id = Cat.id :<->: Cat.id | ||
| > (f :<->: g) . (f' :<->: g') = (f Cat.. f') :<->: (g' Cat.. g) | ||
|
|
||
| >type family Hom (a :: k) (b :: k) :: * | ||
| >type instance Hom a b = NatT a b | ||
| >type instance Hom a b = KleisliA a b | ||
|
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,5 @@ | ||
| >{-# LANGUAGE Safe, KindSignatures, PolyKinds #-} | ||
| >module Math.Graph.InternalCategory where | ||
| >import Data.Kind | ||
| >import safe Control.Arrow | ||
|
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,51 @@ | ||
| >{-# LANGUAGE Safe #-} | ||
| >module Math.Graph.Tex where | ||
| >import Math.Graph.Reversible | ||
| >import Math.Graph.InGraphMonad | ||
| >import Data.Set | ||
|
|
||
| >packageImports = "\\usepackage{tikz}" | ||
|
|
||
| >data TexToken = EnvToken { envName :: String, | ||
| > envOpts :: [String], | ||
| > contents :: [TexToken] } | ||
| > | NodesToken { nodesList :: [TikzNode] } | ||
| > | EdgesToken { edgesList :: [TikzEdge] } | ||
|
|
||
| >data NodeType = NodeType { | ||
| > style_name :: String, | ||
| > style_def :: String | ||
| > } | ||
|
|
||
| >data TikzNode = TikzNode { | ||
| > node_type :: NodeType, | ||
| > node_name :: String | ||
| > } | ||
| >data TikzEdge = TikzEdge { | ||
| > edge_name :: String, | ||
| > start_node_name :: String, | ||
| > end_node_name :: String, | ||
| > start_node_direction :: NodeDirection, | ||
| > end_node_direction :: NodeDirection | ||
| > } | ||
| > | ||
|
|
||
|
|
||
| >instance Show TexToken where | ||
| > show (EnvToken e o c) = | ||
| > "\\begin{" ++ e ++ "}[" ++ concatMap (++ ',') o ++ "]\n" | ||
| > ++ concatMap (\x -> show x ++ "\n") c | ||
| > ++ "\\end{" ++ e ++ "}\n" | ||
|
|
||
| >tikzEnv :: [String] -> TexToken -> TexToken | ||
| >tikzEnv opts cont = EnvToken "tikzpicture" opts cont | ||
|
|
||
| >graphToTex :: (Monad m) => InGraphM mon e m TexToken | ||
| >graphToTex = do | ||
| > v <- gvertices | ||
| > e <- glinks | ||
| > let links = Set.map linkToTex e | ||
| > vertices = Set.map vertexToTex e | ||
| > return $ tikzEnv [] $ NodesToken $ [ | ||
|
|
||
| >linkToTex :: |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.