packages feed

Monocle (empty) → 0.0.0

raw patch · 9 files changed

+889/−0 lines, 9 filesdep +basesetup-changed

Dependencies added: base

Files

+ LICENSE view
@@ -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.+
+ Monocle.cabal view
@@ -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+
+ Monocle.hs view
@@ -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+
+ Monocle/Core.hs view
@@ -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)
+ Monocle/Markup.hs view
@@ -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++
+ Monocle/Tex.hs view
@@ -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
+ Monocle/Utils.hs view
@@ -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+
+ Setup.lhs view
@@ -0,0 +1,4 @@+#! /usr/bin/env runhaskell+ +> import Distribution.Simple+> main = defaultMain
+ monocle-test.hs view
@@ -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++++