diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,24 @@ +Copyright (c) 2009, Osman Bineev (bineev AT gmail DOT com) +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + * Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. + * The names of the contributors may be used to endorse or promote products + derived from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY OSMAN BINEEV ''AS IS'' AND ANY +EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED +WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL OSMAN BINEEV BE LIABLE FOR ANY +DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES +(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; +LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND +ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + diff --git a/Monocle.cabal b/Monocle.cabal new file mode 100644 --- /dev/null +++ b/Monocle.cabal @@ -0,0 +1,21 @@ +Name: Monocle +Cabal-Version: >= 1.2 +Version: 0.0.0 +Synopsis: Symbolic computations in strict monoidal categories with LaTeX output. +Description: Symbolic computations in strict monoidal categories with LaTeX output. + See monocle-test.hs. + 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). +License: BSD3 +License-file: LICENSE +Author: Osman Bineev +Maintainer: Osman Bineev (bineev AT gmail DOT com) +Category: Math +Build-type: Simple +Extra-source-files: monocle-test.hs +Stability: alpha + +Library + exposed-modules: Monocle.Utils, Monocle.Core, Monocle.Markup, Monocle.Tex, Monocle + build-depends: base >= 3 && < 5 + diff --git a/Monocle.hs b/Monocle.hs new file mode 100644 --- /dev/null +++ b/Monocle.hs @@ -0,0 +1,102 @@ +module Monocle where + +import Monocle.Core +import Monocle.Markup +import Monocle.Tex + +obA = object "A" +obB = object "B" +obC = object "C" +obD = object "D" + + +-- Duality: + +ldual'of x = Func "ldual" [x] Function +ldual x = ldual'of x +ldual'r x = ldual'of x + +rdual'of x = Func "rdual" [x] Function +rdual x = rdual'of x +rdual'r x = rdual'of x + +unit'of nm x y = if (x == ldual y) || (y == rdual x) + then let f = (element nm (y \* x)) in Transform "unit" f [x, y] + else error "unit'of: not a dual pair" +unit x y = unit'of "\\eta" x y +unit'r x y = let f = (element "*\\eta" (y \* x)) in Transform "unit" f [x, y] + +counit'of nm x y = if (x == ldual y) || (y == rdual x) + then let f = (coelement nm (x \* y)) in Transform "counit" f [x, y] + else error "counit'of: not a dual pair" +counit x y = counit'of "\\epsilon" x y +counit'r x y = let f = (coelement "*\\epsilon" (x \* y)) in Transform "counit" f [x, y] + +zigzag'rule'Left = (counit'r obA obB) \* obA \. obA \* (unit'r obA obB) \== obA +zigzag'rule'Right = obB \* (counit'r obA obB) \. (unit'r obA obB) \* obB \== obB + +-- Braiding: + +braid'of nm x y = let f = (arrow nm (x \* y) (y \* x)) in + Transform "braid" f [x, y] +braid x y = braid'of "\\beta" x y +braid'r x y = braid'of ("*\\beta") x y + +unbraid'of nm x y = let f = (arrow nm (x \* y) (y \* x)) in + Transform "unbraid" f [x, y] +unbraid x y = unbraid'of "\\beta^{-1}" x y +unbraid'r x y = unbraid'of ("*\\beta^{-1}") x y + +braid'rule'Iso'Left = (unbraid'r obB obA) \. (braid'r obA obB) \== obA \* obB + +braid'rule'Iso'Right = (braid'r obB obA) \. (unbraid'r obA obB) \== obA \* obB + +braid'rule'Nat'Left = let f = arrow "f" obA obA in + (braid'r obA obB) \. f \* obB \== obB \* f \. (braid'r obA obB) + +braid'rule'Nat'Right = let f = arrow "f" obB obB in + (braid'r obA obB) \. obA \* f \== f \* obA \. (braid'r obA obB) + +braid'rule'Hex'Braid = + obB \* (braid'r obA obC) \. (braid'r obA obB) \* obC \== braid'r obA (obB \* obC) + +braid'rule'Hex'Unbraid = + obB \* (unbraid'r obA obC) \. (unbraid'r obA obB) \* obC \== unbraid'r obA (obB \* obC) + +-- Symmetry: + +cross'rule = braid'r obA obB \== unbraid'r obA obB + +-- Twisting: + +twist'of nm x = let f = (arrow nm x x) in Transform "twist" f [x] +twist x = twist'of "\\theta" x +twist'r x = twist'of ("*\\theta") x + +untwist'of nm x = let f = (arrow nm x x) in Transform "untwist" f [x] +untwist x = untwist'of "\\theta^{-1}" x +untwist'r x = untwist'of ("*\\theta^{-1}") x + +untwist'rule'Iso'Left = (untwist'r obA) \. (twist'r obA) \== obA \* obB +untwist'rule'Iso'Right = (twist'r obA) \. (untwist'r obA) \== obA + +twist'rule'Id = (twist'r tid) \== tid + +twist'rule'Natural = let f = arrow "f" obA obA in + (twist'r obA) \. f \== f \. (twist'r obA) + +twist'rule'Braid = + (braid'r obB obA) \. (twist'r obB) \* (twist'r obA) \. (braid'r obA obB) \== twist'r (obA \* obB) + +-- Dagger: + +dagger'of f = Func "dagger" [f] Cofunctor + +dagger f = dagger'of f +dagger'r f = dagger'of f + +dagger'rule'Id = (dagger'r obA) \== obA +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'rule'Inv = (dagger'r $ dagger'r obA) \== obA + diff --git a/Monocle/Core.hs b/Monocle/Core.hs new file mode 100644 --- /dev/null +++ b/Monocle/Core.hs @@ -0,0 +1,369 @@ +module Monocle.Core where + +import Monocle.Utils +import Control.Monad.State +import qualified Data.Map as Map + +class (Eq a) => Morphism a where + dom :: a -> a + cod :: a -> a + isId :: a -> Bool + (\.) :: a -> a -> a + (\*) :: a -> a -> a + +infixl 7 \* +infixl 6 \. + +data ArrowData a = ArrowData { dom' :: Mor a, cod' :: Mor a, isId' :: Bool } deriving (Eq, Ord) +data FuncT = Function | Functor | Cofunctor deriving (Eq, Ord) + +data Mor a = + Arrow a (ArrowData a) | + Id a | + Tensor [Mor a] | + Composition [Mor a] | + Func String [Mor a] FuncT | + Transform String (Mor a) [Mor a] + deriving (Eq, Ord) + +instance (Eq a) => Morphism (Mor a) where + dom x = case x of + Arrow _ dt -> dom' dt + Id _ -> x + Tensor [] -> Tensor [] + Tensor y -> nrm (Tensor (map dom y)) + Composition y -> (dom . head) y + Func y xs t -> case t of + Function -> x + Functor -> Func y (map dom xs) Functor + Cofunctor -> Func y (map cod xs) Cofunctor + Transform _ f _ -> dom f + cod x = case x of + Arrow _ dt -> cod' dt + Id _ -> x + Tensor [] -> Tensor [] + Tensor y -> nrm (Tensor (map cod y)) + Composition y -> (cod . last) y + Func y xs t -> case t of + Function -> x + Functor -> Func y (map cod xs) Functor + Cofunctor -> Func y (map dom xs) Cofunctor + Transform _ f _ -> cod f + isId x = case x of + Arrow _ dt -> isId' dt + Id _ -> True + Tensor [] -> True + Tensor y -> and (map isId y) + Composition y -> and (map isId y) + Func _ xs t -> case t of + Function -> True + Functor -> and (map isId xs) + Cofunctor -> and (map isId xs) + Transform _ f _ -> isId f + f \. g + | dom(f) == cod(g) = if isId f then g else if isId g then f else + case f of + Composition x -> case g of + Composition y -> Composition (y++x) + _ -> Composition (g:x) + _ -> case g of + Composition y -> Composition (y++[f]) + _ -> Composition [g, f] + | otherwise = error "compose: domain and codomain of composing arrows do not coincide" + + f \* g = case f of + Tensor [] -> g + Tensor x -> case g of + Tensor [] -> f + Tensor y -> Tensor (x++y) + _ -> Tensor (x++[g]) + _ -> case g of + Tensor [] -> f + Tensor y -> Tensor ([f]++y) + _ -> Tensor [f, g] + +-- Basic functions on morphisms: + +nrm f = case f of + Arrow ff (ArrowData d c ii) -> Arrow ff (ArrowData (nrm d) (nrm c) ii) + Tensor [x] -> x + Tensor x -> untens (map nrm x) + Composition [x] -> x + Composition x -> uncomp (map nrm x) + Func nm xs t -> Func nm (map nrm xs) t + Transform nm x xs -> Transform nm (nrm x) (map nrm xs) + _ -> f + where + untens x = case x of + y:ys -> y \* (untens ys) + _ -> Tensor x + uncomp x = case x of + y:[] -> y + y:ys -> (uncomp ys) \. y + _ -> Composition x + +terminal f = case f of + Arrow _ _ -> True + Id _ -> True + Transform _ _ _ -> True + Tensor [] -> True + _ -> False + +getInfo f = case f of + Arrow x _ -> [x] + Id x -> [x] + Tensor [] -> [] + Func x _ _ -> [x] + Transform x _ _ -> [x] + _ -> error "getName: wrong argument" + +getData (Arrow _ dt) = dt +getData s@(Id _) = ArrowData s s True +getData s@_ = ArrowData (dom s) (cod s) (isId s) + +arrow nm adom acod = Arrow nm (ArrowData adom acod False) +element nm acod = arrow nm (Tensor []) acod +coelement nm adom = arrow nm adom (Tensor []) +object nm = Id nm +objectId nm = Id nm +tid = Tensor [] + +width :: (Eq a) => Mor a -> Int +width f = case f of + Id _ -> 1 + Tensor [] -> 0 + Tensor x -> sum (map width x) + Composition x -> maximum (map width x) + _ -> max (width(dom f)) (width(cod f)) + +height :: (Eq a) => Mor a -> Int +height f = case f of + Id _ -> 0 + Tensor [] -> 0 + Tensor x -> maximum (map height x) + Composition x -> sum (map height x) + Transform _ x _ -> height x + _ -> 1 + +-- Tensor product functoriality: + +vert :: (Eq a) => Mor a -> Mor a +vert f = case f of + Composition (y1:y2:[]) -> vertPair y1 y2 + Composition (y1:y2:ys) -> case (vertPair y1 y2) of + s@(Tensor _) -> vert ((Composition ys) \. s) + _ -> (vert ((Composition ys) \. y2)) \. y1 + _ -> vertInside f + where + vertPair f g = case f of + Tensor (x1':x2:xs) -> case g of + Tensor (y1':y2:ys) -> let x1 = vert x1'; y1 = vert y1' in + if x1 /= x1' || y1 /= y1' then + vertPair (x1 \* (Tensor (x2:xs))) (y1 \* (Tensor (y2:ys))) + else let wx = width (cod x1); wy = width (dom y1) in + if wx == wy + then (y1 \. x1) \* + nrm (vertPair (Tensor (x2:xs)) (Tensor (y2:ys))) + else if wx > wy + then nrm (vertPair f (Tensor ((y1 \* y2) : ys))) + else nrm (vertPair (Tensor ((x1 \* x2) : xs)) g) + _ -> g \. f + _ -> g \. f + vertInside f = case f of + Tensor y -> Tensor (map vert y) + Transform s x xs -> Transform s (vert x) xs + Func s xs t -> Func s (map vert xs) t + _ -> f + +horz :: (Eq a) => Mor a -> Mor a +horz f = case f of + Tensor (y1:y2:[]) -> horzPair y1 y2 + Tensor (y1:y2:ys) -> case (horzPair y1 y2) of + s@(Composition _) -> horz (s \* (Tensor ys)) + _ -> y1 \* (horz (y2 \* (Tensor ys))) + _ -> horzInside f + where + horzPair f g = case f of + Composition (x1':x2:xs) -> case g of + Composition (y1':y2:ys) -> let x1 = horz x1'; y1 = horz y1' in + if x1 /= x1' || y1 /= y1' then + horzPair ((Composition (x2:xs)) \. x1) + ((Composition (y2:ys)) \. y1) + else let hx = height x1; hy = height y1 in + if hx == hy + then nrm (horzPair (Composition (x2:xs)) (Composition (y2:ys))) \. + (x1 \* y1) + else if hx > hy + then nrm (horzPair f (Composition ((y2 \. y1) : ys))) + else nrm (horzPair (Composition ((x2 \. x1) : xs)) g) + _ -> f \* g + _ -> f \* g + horzInside f = case f of + Composition y -> Composition (map horz y) + Transform s x xs -> Transform s (horz x) xs + Func s xs t -> Func s (map horz xs) t + _ -> f + +-- Monad.State support: + +mapMorM :: (Eq a, Monad m) => m () -> (Mor a -> m (Mor a)) -> Mor a -> m (Mor a) +mapMorM prep func f = case f of + Tensor xs@(_:_) -> do + prep; xs' <- mapM (mapMorM prep func) xs + func $ nrm $ Tensor xs' + Composition xs -> do + prep; xs' <- mapM (mapMorM prep func) xs + func $ nrm $ Composition xs' + Func ff xs t -> do + prep; xs' <- mapM (mapMorM prep func) xs + func $ nrm $ Func ff xs' t + Transform ff x xs -> do + prep; + x' <- mapMorM prep func x + xs' <- mapM (mapMorM prep func) xs + func $ nrm $ Transform ff x' xs' + _ -> func f + +mapMorM' :: (Eq a, Eq b, Monad m) => (Mor a -> m (Mor b)) -> Mor a -> m (Mor b) +mapMorM' func f = case f of + Tensor xs@(_:_) -> do + xs' <- mapM (mapMorM' func) xs + return $ nrm $ Tensor xs' + Composition xs -> do + xs' <- mapM (mapMorM' func) xs + return $ nrm $ Composition xs' + Func ff xs t -> do + xs' <- mapM (mapMorM' func) xs + return $ nrm $ Func ff xs' t + Transform ff x xs -> do + x' <- mapMorM' func x + xs' <- mapM (mapMorM' func) xs + return $ nrm $ Transform ff x' xs' + _ -> func f + +transMor mor inits wlk = evalState ((mapMorM (return ()) wlk) mor) inits +calcMor mor inits wlk = execState ((mapMorM (return ()) wlk) mor) inits +transMorP mor inits prep wlk = evalState ((mapMorM prep wlk) mor) inits +calcMorP mor inits prep wlk = execState ((mapMorM prep wlk) mor) inits +transMor' mor inits wlk = evalState ((mapMorM' wlk) mor) inits +calcMor' mor inits wlk = execState ((mapMorM' wlk) mor) inits + +-- Show + +instance (Printable a, Eq a) => Printable (Mor a) where + str f = case f of + Arrow fx _ -> str $ nm fx + Id fx -> str $ nm fx + Tensor [] -> "I" + Tensor xs -> close $ op " * " (map show xs) + Composition xs -> close $ op " . " (map show xs) + Func nm xs t -> nm ++ (close $ op ", " (map show xs)) + Transform nm x xs -> nm ++ (close1 $ op ", " (map show xs)) ++ (close $ show x) + where + nm x = let s = str x in if (head s == '*') then tail s else s + op s [] = "" + op s (x:xs) = foldl (\x' y' -> x'++s++y') x xs + close x = "(" ++ x ++ ")" + close1 x = "[" ++ x ++ "]" + +instance (Printable a, Eq a) => Show (Mor a) where + show f = str f + +-- Match, substitute etc. + +merge :: (Eq a, Eq b) => Mor a -> Mor b -> Maybe (Mor (Mor a, b)) +merge m1 m2 = case (m1, m2) of + (_, Id f2) -> Just (Id (m1, f2)) + (_, Arrow f2 (ArrowData d2 c2 ii2)) -> + let d1 = dom m1; c1 = cod m1 in do + d' <- merge d1 d2; c' <- merge c1 c2 + return $ Arrow (m1, f2) (ArrowData d' c' ii2) + (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) + 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) + 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) + 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) + return $ Composition xs' + _ -> Nothing + +match f g = case merge f g of + Nothing -> (False, Map.empty) + Just h -> calcMor h (True, Map.empty) $ + \x -> case x of + Arrow (x1, x2) _ -> cmp x1 x2 x + Id (x1, x2) -> cmp x1 x2 x + _ -> return x + where + cmp x1 x2 x' = do + (tv, mp) <- get + put $ if not tv || (head x2)=='*' then (tv, mp) else + if Map.member x2 mp + then (tv && (mp Map.! x2) == x1, mp) + else + (tv, Map.insert x2 x1 mp) + return x' + +subst :: (Ord a, Eq b) => Map.Map a (Mor b) -> Mor a -> Mor b +subst mp f = transMor' f () $ \x -> + case x of + Arrow f _ -> return $ mp Map.! f + Id f -> return $ mp Map.! f + +subst' :: (Ord a, Eq b, Printable b) => Map.Map a (Mor b) -> Mor a -> Mor b +subst' mp f = transMor' f () $ \x -> + case x of + Arrow f _ -> let arr' = mp Map.! f in + case arr' of + Arrow f' _ -> return arr' + _ -> error $ "subst': no match in" ++ (show arr') + Id f -> let arr' = mp Map.! f in + case arr' of + Id f' -> return arr' + _ -> error $ "subst': no match in " ++ (show arr') + +collect f = fst $ calcMor' f (Map.empty, 1) $ \x -> + case x of + Arrow _ _ -> do + (mp, n) <- get + put $ (Map.insert x n mp, n+1) + return x + Id _ -> do + (mp, n) <- get + put $ (Map.insert x n mp, n+1) + return x + _ -> return x + +-- Rules: + +data Rule a = DefEqual (Mor a) (Mor a) +x \== y = DefEqual x y + +infix 4 \== + +r'left (DefEqual x _) = x +r'right (DefEqual _ x) = x + +apply (DefEqual l r) f = + let (tv, mp) = match f l in + if not tv then let (tv, mp) = match f r in + if not tv then error "apply: no match" + else subst mp r + else subst mp r + +instance (Printable a, Eq a) => Show (Rule a) where + show (DefEqual l r) = (show l)++" == "++(show r) diff --git a/Monocle/Markup.hs b/Monocle/Markup.hs new file mode 100644 --- /dev/null +++ b/Monocle/Markup.hs @@ -0,0 +1,127 @@ +module Monocle.Markup where + +import Monocle.Core +import Control.Monad.State + + +data Lab a = + MArrow (Mor a) String | + MId (Mor a) String | + MTensor [Lab a] String | + MComposition [Lab a] String | + MFunc String [Lab a] FuncT String | + MTransform String (Lab a) [Mor a] String + deriving (Eq, Ord) + +instance (Eq a) => Morphism (Lab a) where + dom f = markup $ dom $ unmark f + cod f = markup $ cod $ unmark f + isId f = isId $ unmark f + f \. g = markup $ (unmark f) \. (unmark g) + f \* g = markup $ (unmark f) \* (unmark g) + +makeLab f = case f of + Arrow _ _ -> MArrow f "" + Id _ -> MId f "" + Tensor xs -> MTensor (map makeLab xs) "" + Composition xs -> MComposition (map makeLab xs) "" + Func nm xs t -> MFunc nm (map makeLab xs) t "" + Transform nm x xs -> MTransform nm (makeLab x) xs "" + +unmark lf = nrm $ case lf of + MArrow f _ -> f + MId f _ -> f + MTensor xs _ -> Tensor (map unmark xs) + MComposition xs _ -> Composition (map unmark xs) + MFunc nm xs t _ -> Func nm (map unmark xs) t + MTransform nm x xs _ -> Transform nm (unmark x) xs + +mapLabM prep func lf = case lf of + MTensor xs@(_:_) lab -> do + prep; xs' <- mapM (mapLabM prep func) xs + func $ MTensor xs' lab + MComposition xs lab -> do + prep; xs' <- mapM (mapLabM prep func) xs + func $ MComposition xs' lab + MFunc nm xs t lab -> do + prep; xs' <- mapM (mapLabM prep func) xs + func $ MFunc nm xs' t lab + MTransform nm x xs lab -> do + prep; x' <- mapLabM prep func x + func $ MTransform nm x' xs lab + _ -> func lf + +getLabel lf = case lf of + MArrow _ lab -> lab + MId _ lab -> lab + MTensor _ lab -> lab + MComposition _ lab -> lab + MFunc _ _ _ lab -> lab + MTransform _ _ _ lab -> lab + +setLabel nlab lf = case lf of + MArrow f _ -> MArrow f nlab + MId f _ -> MId f nlab + MTensor xs _ -> MTensor xs nlab + MComposition xs _ -> MComposition xs nlab + MFunc nm xs t _ -> MFunc nm xs t nlab + MTransform nm x xs _ -> MTransform nm x xs nlab + + +transLab mor inits wlk = evalState ((mapLabM (return ()) wlk) mor) inits +calcLab mor inits wlk = execState ((mapLabM (return ()) wlk) mor) inits +transLabP mor inits prep wlk = evalState ((mapLabM prep wlk) mor) inits +calcLabP mor inits prep wlk = execState ((mapLabM prep wlk) mor) inits + +modifLab s lf op = transLab lf () $ \x -> + let xlab = getLabel x in + if xlab == s then + return $ op x + else return x + +modif' s lf op = transLab lf () $ \x -> + let xlab = getLabel x in + if xlab == s then + return $ setLabel xlab $ makeLab $ nrm $ op $ unmark x + else return x + +modif s lf op = unmark $ modif' s lf op + +getByLab s f = calcLab f Nothing $ \x -> + let xlab = getLabel x in + if xlab == s then do + ls <- get + put $ Just (unmark x) + return x + else return x + +labels f = calcLab f [] $ \x -> do + ls <- get + put $ (getLabel x, unmark x):ls + return x + +choose nlab start end f = case f of + MTensor xs lab -> let ((xs1, xs2), xs3) = (let (x1, x2) = splitAt end xs in (splitAt (start-1) x1, x2)) in + MTensor (xs1 ++ [MTensor xs2 nlab] ++ xs3) lab + MComposition xs lab -> let s' = length xs - end; e' = length xs - start + 1 in + let ((xs1, xs2), xs3) = (let (x1, x2) = splitAt e' xs in (splitAt s' x1, x2)) in + MComposition (xs1 ++ [MComposition xs2 nlab] ++ xs3) lab + _ -> error "choose: arrow is not composition or tensor" + +markup f = transLab (makeLab f) 1 $ \x -> + case x of + MComposition _ _ -> do + n <- get; put (n+1) + return $ setLabel ("lab:" ++ show n) x + MTensor _ _ -> do + n <- get; put (n+1) + return $ setLabel ("lab:" ++ show n) x + MFunc _ _ _ _ -> do + n <- get; put (n+1) + return $ setLabel ("lab:" ++ show n) x + MTransform _ _ _ _ -> do + n <- get; put (n+1) + return $ setLabel ("lab:" ++ show n) x + _ -> return x + + diff --git a/Monocle/Tex.hs b/Monocle/Tex.hs new file mode 100644 --- /dev/null +++ b/Monocle/Tex.hs @@ -0,0 +1,150 @@ +module Monocle.Tex where + +import Monocle.Core +import Monocle.Utils +import Monocle.Markup + +import IO +import Control.Monad.State +import qualified Data.Map as Map + +class Texified a where + tex :: a -> String + doc :: a -> String + +-- TeX utilities + +s'join inf [] = "" +s'join inf (x:xs) = foldl (\x y -> x++inf++y) x xs + +t'sub x = "_{" ++ x ++ "}" +t'sup x = "^{" ++ x ++ "}" + +t'id x = " id" ++ (t'sub x) + +t'op op [] = "" +t'op op (z:[]) = z +t'op op (z:zs) = (foldl (\x y -> x++op++" "++y) z zs) + +t'rop op [] = "" +t'rop op x = t'op op $ reverse x + +t'open x = + if not $ null x then + if head x == '(' && last x == ')' + then init $ tail x + else x + else x +t'close x = + if not $ null x then + if head x /= '(' || last x /= ')' + then "(" ++ x ++ ")" + else x + else x + +t'cmd cmd x = " \\" ++ cmd ++ "{" ++ x ++ "}" +t'sf x = t'cmd "textsf" x + +t'begin x = t'cmd "begin" x +t'end x = t'cmd "end" x + +t'endl = "\n" +t'math f = "$" ++ f ++ "$" + + +-- TeX primitives + +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'itemize [] = "" +t'itemize items = 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'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) + +-- TeXify Mor + +t'texMor f = case f of + Arrow y _ -> str y + Func nm xs t -> case t of + Function -> t'texF_ t'texMor nm xs + Functor -> t'texF_ t'texMor nm xs + 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 y -> t'close $ t'op "\\otimes" $ map t'texMor y + Composition y -> t'close $ t'rop "\\circ" $ map t'texMor y + +t'objMor f = case f of + Func nm xs t -> case t of + Function -> t'texF_ t'objMor nm xs + Functor -> t'texF_ t'objMor nm xs + Cofunctor -> t'texF_ t'objMor nm xs + Id y -> str y + Tensor y -> t'close $ t'op "\\otimes" $ map t'objMor y + _ -> error "texObj: not an object" + + +instance (Printable a, Ord a) => Texified (Mor a) where + tex f = t'math $ t'open $ t'texMor f + + doc f = if terminal f then + 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 + +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") + +-- TeXify Lab + +t'mblab lab x = + if null lab then x + else (t'close x) ++ (t'sub lab) + +t'texLab f = case f of + MFunc nm xs t lab -> t'mblab lab $ case t of + Function -> t'texF_ t'texLab nm xs + 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 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 + +t'objLab f = case f of + MFunc nm xs t lab -> t'mblab lab $ case t of + Function -> t'texF_ t'objLab nm xs + Functor -> t'texF_ t'objLab nm xs + Cofunctor -> t'texF_ t'objLab nm xs + MId f lab -> t'mblab lab $ texObj f + MTensor xs lab -> t'mblab lab $ t'op "\\otimes" $ map t'objLab xs + _ -> error "texObjLab: not an object" + +texObjLab f = t'open (t'objLab f) + +instance (Printable a, Ord a) => Texified (Lab a) where + tex f = t'math $ t'open $ t'texLab f + + doc f = if terminal $ unmark f then + if not $ isId f then t'docHead_ t'texLab t'objLab "marked morphism " f else "" + else t'doc_ t'texLab t'objLab "marked morphism " f $ collect $ unmark f + +-- IO + +ptex f = do putStrLn $ tex f +pobj f = do putStrLn $ texObj f +pdoc f = do putStrLn $ doc f diff --git a/Monocle/Utils.hs b/Monocle/Utils.hs new file mode 100644 --- /dev/null +++ b/Monocle/Utils.hs @@ -0,0 +1,34 @@ +{-# OPTIONS -XMultiParamTypeClasses -XFlexibleInstances -XTypeSynonymInstances#-} + +module Monocle.Utils where + +import Data.Monoid + +class (Monoid monoid) => MStack stack monoid where + pop :: stack -> (stack, monoid) + push :: monoid -> stack -> stack + tappend :: monoid -> stack -> stack + tcombine :: (monoid -> monoid) -> stack -> stack + +instance (Monoid monoid) => MStack [monoid] monoid where + pop s = case s of + [] -> ([], mempty) + x:xs -> (xs, x) + push m s = m:s + tappend m s = let (s', m') = pop s in push (mappend m m') s' + tcombine f s = let (s', m') = pop s in tappend (f m') s' + +class Printable a where + str :: a -> String + +data Wrap a = Wrap a + +instance Printable String where + str x = if (head x) == '*' then (tail x) else x + +instance (Printable a, Printable b) => Printable (a, b) where + str (x, y) = "(" ++ (str x) ++ ", " ++ (str y) ++ ")" + +instance (Show a) => Printable (Wrap a) where + str (Wrap x) = show x + diff --git a/Setup.lhs b/Setup.lhs new file mode 100644 --- /dev/null +++ b/Setup.lhs @@ -0,0 +1,4 @@ +#! /usr/bin/env runhaskell + +> import Distribution.Simple +> main = defaultMain diff --git a/monocle-test.hs b/monocle-test.hs new file mode 100644 --- /dev/null +++ b/monocle-test.hs @@ -0,0 +1,58 @@ +module Test where + +import Monocle.Core +import Monocle.Tex +import Monocle.Markup +import Monocle + +main = do + + -- create object $A$ and $B$, arrows $f: A \to B$ and $g: (B\otimes A) \to (B\otimes A)$ : + let a = object "A"; b = object "B" + let f = arrow "f" a b; g = arrow "g" (b \* a) (b \* a) + + -- create arrow $g \circ (f \otimes id_A)$ : + let h = g \. f \* a + + -- show \LaTeX form of $h$ : + ptex h + + -- 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 : + pdoc br + pdoc ub + + -- show unbraid rule : + pdoc braid'rule'Iso'Left + + -- apply it to $\beta^{-1} \circ \beta$ : + let r = apply braid'rule'Iso'Left (ub \. br) + ptex r + + + -- create arrow $h: (A\otimes B) \to (A\otimes B)$ : + let h = arrow "h" (a \* b) (a \* b) + + -- create arrow $(h \circ \beta^{-1} \circ \beta \circ h) \otimes h$ : + let h1 = (h \. ub \. br \. h) \* h + + -- markup it : + let h2 = markup h1 + 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 + ptex h3 + + -- apply unbraid rule to the selected components : + pdoc $ modif "lab" h3 $ apply braid'rule'Iso'Left + + + +