diff --git a/Monocle.cabal b/Monocle.cabal --- a/Monocle.cabal +++ b/Monocle.cabal @@ -1,5 +1,5 @@ name: Monocle -version: 0.0.3 +version: 0.0.4 cabal-version: >=1.2 build-type: Simple license: BSD3 @@ -14,17 +14,17 @@ bug-reports: synopsis: Symbolic computations in strict monoidal categories with LaTeX output. description: Symbolic computations in strict monoidal categories with LaTeX output. - See monocle-test.hs. + See 'monocle-usage.pdf' and 'monocle-test.hs' included in package. One of goals of this project is to develop the tool for automatic - drawing of diagrams of morphisms and proofs in form suitable for LaTeX (e.g. for XY-pic). + drawing diagrams of morphisms and proofs in form suitable for LaTeX (e.g. for XY-pic). category: Math author: Osman Bineev tested-with: data-files: data-dir: "" -extra-source-files: monocle-test.hs +extra-source-files: monocle-test.hs monocle-usage.pdf extra-tmp-files: -exposed-modules: Monocle.Core Monocle.Markup Monocle.Rules +exposed-modules: Monocle Monocle.Core Monocle.Markup Monocle.Rules Monocle.Tex Monocle.Utils exposed: True buildable: True diff --git a/Monocle.hs b/Monocle.hs new file mode 100644 --- /dev/null +++ b/Monocle.hs @@ -0,0 +1,11 @@ +module Monocle ( + module Monocle.Core, + module Monocle.Markup, + module Monocle.Tex, + module Monocle.Rules + ) where + +import Monocle.Core +import Monocle.Markup +import Monocle.Tex +import Monocle.Rules diff --git a/Monocle/Core.hs b/Monocle/Core.hs --- a/Monocle/Core.hs +++ b/Monocle/Core.hs @@ -29,9 +29,9 @@ -- | Class of morphisms. class (Eq a) => Morphism a where - -- | Returns domain of the given morphism. + -- | Returns domain of the given morphism (actually its id). dom :: a -> a - -- | Returns codomain of the given morphism. + -- | Returns codomain of the given morphism (actually its id). cod :: a -> a -- | Checks whether morphism is id. isId :: a -> Bool @@ -129,7 +129,7 @@ -- Basic functions on morphisms --- | Normalizes the term representing morphism, e.g. turns @((a \* b) \* c)@ to @(a \* b \* c)@ +-- | Normalizes the term representing morphism, e.g. turns @((a \\* b) \\* c)@ to @(a \\* b \\* c)@ nrm :: (Eq t) => Mor t -> Mor t nrm f = case f of Arrow ff (ArrowData d c ii) -> Arrow ff (ArrowData (nrm d) (nrm c) ii) @@ -174,15 +174,15 @@ arrow :: a -> Mor a -> Mor a -> Mor a arrow nm adom acod = Arrow nm (ArrowData adom acod False) --- | Creates generalized element, i.e. an arrow from the tensorial Id to the given object. +-- | Creates generalized element, i.e. an arrow from the identity object to the given object. element :: a -> Mor a -> Mor a element nm acod = arrow nm (Tensor []) acod --- | Creates generalized coelement, i.e. an arrow from the the given object to the tensorial Id. +-- | Creates generalized coelement, i.e. an arrow from the the given object to the identity object. coelement :: a -> Mor a -> Mor a coelement nm adom = arrow nm adom (Tensor []) --- | Creates object (actually it's id). Same as 'objectId'. +-- | Creates object (actually its id). Same as 'objectId'. object :: a -> Mor a object nm = Id nm @@ -190,7 +190,7 @@ objectId :: a -> Mor a objectId nm = Id nm --- | Tensorial Id, @tid \* f == f@ in strict monoidal category. +-- | Identity object, @tid \\* f == f@ in strict monoidal category. tid :: Mor a tid = Tensor [] @@ -349,23 +349,23 @@ (Func f1 xs1 t1, Func f2 xs2 t2) -> if f1 /= f2 || t1 /= t2 then Nothing else do - xs' <- mapM (\(x', y') -> merge x' y') (zip xs1 xs2) + xs' <- mapM (uncurry $ merge) (zip xs1 xs2) return $ Func f1 xs' t1 (Transform f1 x1 xs1, Transform f2 x2 xs2) -> if f1 /= f2 then Nothing else do x' <- merge x1 x2 - xs' <- mapM (\(xx, yy) -> merge xx yy) (zip xs1 xs2) + xs' <- mapM (uncurry $ merge) (zip xs1 xs2) return $ Transform f1 x' xs' (Tensor xs1, Tensor xs2) -> if length xs1 /= length xs2 then Nothing else do - xs' <- mapM (\(x', y') -> merge x' y') (zip xs1 xs2) + xs' <- mapM (uncurry $ merge) (zip xs1 xs2) return $ Tensor xs' (Composition xs1, Composition xs2) -> if length xs1 /= length xs2 then Nothing else do - xs' <- mapM (\(x', y') -> merge x' y') (zip xs1 xs2) + xs' <- mapM (uncurry $ merge) (zip xs1 xs2) return $ Composition xs' _ -> Nothing diff --git a/Monocle/Markup.hs b/Monocle/Markup.hs --- a/Monocle/Markup.hs +++ b/Monocle/Markup.hs @@ -102,7 +102,7 @@ return $ setLabel xlab $ makeLab $ nrm $ op $ unmark x else return x --- | @'unmark' $ 'modif'' s lf op@ +-- | @modif s lf op == 'unmark' $ 'modif'' s lf op@ modif :: (Eq a) => String -> Lab a -> (Mor a -> Mor a) -> Mor a modif s lf op = unmark $ modif' s lf op diff --git a/Monocle/Rules.hs b/Monocle/Rules.hs --- a/Monocle/Rules.hs +++ b/Monocle/Rules.hs @@ -169,14 +169,14 @@ untwist'r x = untwist'of ("*\\theta^{-1}") x -- | Isomorphism rule: 'untwist' as inverse of 'twist'. -untwist'rule'Iso'Left :: Rule String -untwist'rule'Iso'Left = (untwist'r obA) \. (twist'r obA) \== obA \* obB +twist'rule'Iso'Left :: Rule String +twist'rule'Iso'Left = (untwist'r obA) \. (twist'r obA) \== obA \* obB -- | Isomorphism rule: 'twist' as inverse of 'untwist'. -untwist'rule'Iso'Right :: Rule String -untwist'rule'Iso'Right = (twist'r obA) \. (untwist'r obA) \== obA +twist'rule'Iso'Right :: Rule String +twist'rule'Iso'Right = (twist'r obA) \. (untwist'r obA) \== obA --- | Twisting tensorial Id changes nothing. +-- | Twisting the identity object changes nothing. twist'rule'Id :: Rule String twist'rule'Id = (twist'r tid) \== tid @@ -208,12 +208,12 @@ dagger'rule'Id :: Rule String dagger'rule'Id = (dagger'r obA) \== obA --- | 'dagger' swaps domain and codomain. +-- | 'dagger' is contravariant functor, i.e. inverts composition order. dagger'rule'Cofunctor :: Rule String dagger'rule'Cofunctor = let f = arrow "f" obB obC; g = arrow "g" obA obB in (dagger'r (f \. g)) \== (dagger'r g) \. (dagger'r f) -- | 'dagger' involution rule. dagger'rule'Inv :: Rule String -dagger'rule'Inv = (dagger'r $ dagger'r obA) \== obA +dagger'rule'Inv = let f = arrow "f" obA obA in (dagger'r $ dagger'r f) \== f diff --git a/Monocle/Tex.hs b/Monocle/Tex.hs --- a/Monocle/Tex.hs +++ b/Monocle/Tex.hs @@ -1,4 +1,10 @@ -module Monocle.Tex where +module Monocle.Tex ( + Texified (..), + texObj, + ptex, + pobj, + pdoc + )where import Monocle.Core import Monocle.Utils @@ -8,8 +14,11 @@ import Control.Monad.State import qualified Data.Map as Map +-- | Class providing information in LaTeX form. class Texified a where + -- | Returns short description tex :: a -> String + -- | Returns detailed description doc :: a -> String -- TeX utilities @@ -56,14 +65,14 @@ t'docMap mp = map doc $ filter (not.isId) $ fst $ unzip $ Map.toList mp t'docType_ fobj f = (t'open $ fobj $ dom f)++"\\to "++(t'open $ fobj $ cod f) -t'docHead_ ftex fobj wd f = t'endl ++ (t'sf wd) ++ ( t'math $ (t'open $ ftex f) ++ ": " ++ (t'docType_ fobj f) ) ++ t'endl +t'docHead_ ftex fobj wd f = t'endl ++ (t'sf wd) ++ ( t'math $ (ftex f) ++ ": " ++ (t'docType_ fobj f) ) ++ t'endl t'itemize [] = "" -t'itemize items = t'endl ++ (t'begin "itemize") ++ +t'itemize items = (t'sf " where ") ++ t'endl ++ (t'begin "itemize") ++ (foldl (\x y -> x++"\n\\item "++y) "" items) ++ (t'end "itemize") ++ t'endl -t'doc_ ftex fobj wd f mp = (t'docHead_ ftex fobj wd f) ++ (t'sf " where ") ++ (t'itemize $ t'docMap mp) +t'doc_ ftex fobj wd f mp = (t'docHead_ ftex fobj wd f) ++ (t'itemize $ t'docMap mp) t'texF_ ftex nm xs = nm ++ (t'close $ s'join ", " $ map ftex xs) t'texNaturalTfm_ ftex fobj x xs = (ftex x) ++ (t'sub $ t'op ", " $ map fobj xs) @@ -78,7 +87,7 @@ Cofunctor -> t'texF_ t'texMor nm xs Transform nm x xs -> t'texNaturalTfm_ t'texMor t'objMor x xs Id y -> t'id $ str y - Tensor [] -> "I" + Tensor [] -> "id_I" Tensor y -> t'close $ t'op "\\otimes" $ map t'texMor y Composition y -> t'close $ t'rop "\\circ" $ map t'texMor y @@ -88,6 +97,7 @@ Functor -> t'texF_ t'objMor nm xs Cofunctor -> t'texF_ t'objMor nm xs Id y -> str y + Tensor [] -> "I" Tensor y -> t'close $ t'op "\\otimes" $ map t'objMor y _ -> error "texObj: not an object" @@ -99,14 +109,19 @@ if not $ isId f then t'docHead_ t'texMor t'objMor "morphism " f else "" else t'doc_ t'texMor t'objMor "morphism " f $ collect f +-- | Returns LaTeX description of an object of category +texObj :: Printable t => Mor t -> String texObj f = t'open (t'objMor f) -- TeXify Rule instance (Printable a, Ord a) => Texified (Rule a) where tex (DefEqual l r) = (t'sf "rule ")++ ( t'math ( (t'texMor l) ++ "\\equiv " ++ (t'texMor r) ) ) - doc s@(DefEqual l r) = (tex s) ++ (t'sf " where ") ++ t'endl ++ (t'begin "itemize") ++ "\\item "++ - (doc l) ++ "\\item " ++ (doc r) ++ (t'end "itemize") + doc s@(DefEqual l r) = let dl = doc l; dr = doc r in + (tex s) ++ (t'sf " where ") ++ t'endl ++ (t'begin "itemize") ++ + (if not $ null dl then "\\item "++ dl else "") ++ + (if not $ null dr then "\\item " ++ dr else "") ++ + (t'end "itemize") -- TeXify Lab @@ -120,7 +135,7 @@ Functor -> t'texF_ t'texLab nm xs Cofunctor -> t'texF_ t'texLab nm xs MTransform nm x xs lab -> t'mblab lab $ t'texNaturalTfm_ t'texLab t'objMor x xs - MTensor [] lab -> t'mblab lab "I" + MTensor [] lab -> t'mblab lab "id_I" MTensor xs lab -> t'mblab lab $ t'op "\\otimes" $ map t'texLab xs MComposition xs lab -> t'mblab lab $ t'op "\\circ" $ map t'texLab xs _ -> t'mblab (getLabel f) $ t'texMor $ unmark f @@ -131,6 +146,7 @@ Functor -> t'texF_ t'objLab nm xs Cofunctor -> t'texF_ t'objLab nm xs MId f lab -> t'mblab lab $ texObj f + MTensor [] lab -> t'mblab lab "I" MTensor xs lab -> t'mblab lab $ t'op "\\otimes" $ map t'objLab xs _ -> error "texObjLab: not an object" @@ -145,6 +161,12 @@ -- IO +-- | @ptex f = do 'putStrLn' $ 'tex' f@ +ptex :: (Texified a) => a -> IO () ptex f = do putStrLn $ tex f +-- | @pobj f = do 'putStrLn' $ 'texObj' f@ +pobj :: Printable t => Mor t -> IO () pobj f = do putStrLn $ texObj f +-- | @pdoc f = do 'putStrLn' $ 'doc' f@ +pdoc :: (Texified a) => a -> IO () pdoc f = do putStrLn $ doc f diff --git a/monocle-test.hs b/monocle-test.hs --- a/monocle-test.hs +++ b/monocle-test.hs @@ -1,9 +1,6 @@ module Test where -import Monocle.Core -import Monocle.Tex -import Monocle.Markup -import Monocle.Rules +import Monocle main = do @@ -15,23 +12,28 @@ let h = g \. f \* a -- show \LaTeX form of $h$ : + putStrLn "-- show \\LaTeX form of $h$:" ptex h -- show detailed \LaTeX documentation of $h$ : + putStrLn "-- show detailed \\LaTeX documentation of $h$ :" pdoc h -- create braid $\beta$ and unbraid $\beta^{-1}$ : let br = braid a b; ub = unbraid b a -- show them in \LaTeX : + putStrLn "-- show braid and unbraid in \\LaTeX :" pdoc br pdoc ub -- show unbraid rule : + putStrLn "-- show unbraid rule :" pdoc braid'rule'Iso'Left -- apply it to $\beta^{-1} \circ \beta$ : let r = apply braid'rule'Iso'Left (ub \. br) + putStrLn "-- apply it to $\\beta^{-1} \\circ \\beta$ :" ptex r @@ -43,15 +45,18 @@ -- markup it : let h2 = markup h1 + putStrLn "-- h1 marked :" ptex h2 -- using label "lab:3" select elements 2-3 from -- composition $h \circ \beta^{-1} \circ \beta \circ h$ : let h3 = modifLab "lab:3" h2 $ choose "lab" 2 3 + putStrLn "-- h2 modified by choose :" ptex h3 -- apply unbraid rule to the selected components : - pdoc $ modif "lab" h3 $ apply braid'rule'Iso'Left + putStrLn "-- h3 modified by applying unbraid" + ptex $ modif "lab" h3 $ apply braid'rule'Iso'Left diff --git a/monocle-usage.pdf b/monocle-usage.pdf new file mode 100644 Binary files /dev/null and b/monocle-usage.pdf differ