-{-# OPTIONS_GHC -XModalTypes -XMultiParamTypeClasses -XNoMonoPatBinds -XKindSignatures -XGADTs -XFlexibleContexts -XFlexibleInstances -XTypeOperators -XUndecidableInstances #-}
-module GArrowTikZ (tikz, GArrowTikZ(..))
+{-# LANGUAGE RankNTypes, MultiParamTypeClasses, GADTs, FlexibleContexts, FlexibleInstances, TypeOperators #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module : GArrowTikZ
+-- Copyright : none
+-- License : public domain
+--
+-- Maintainer : Adam Megacz <megacz@acm.org>
+-- Stability : experimental
+--
+-- | Renders a @GArrowSkeleton@ using TikZ; the result is LaTeX code.
+-- You must have lp_solve installed in order for this to work.
+--
+
+module GArrowTikZ (tikz)
where
+import System.Process
import Prelude hiding ( id, (.), lookup )
import Control.Category
+import Control.Monad.State
import GHC.HetMet.GArrow
import Data.List hiding (lookup, insert)
import Data.Map hiding (map, (!))
+import Data.Maybe (catMaybes)
import Unify
+import GArrowSkeleton
+import GArrowPortShape
+import GHC.HetMet.Private
-
-{-
-TO DO:
- - have "resolve" turn a (Diagram UnifVal) into (Diagram Int)
- - custom rendering
- - bias right now is for all edges to be uppermost; try for bias
- towards smallest nodes?
- - curvy boxes (like XOR gates)
--}
-
-
--- a unification value is basically a LISP-ish expression
-data UVal =
- UVVar UVar
- | UVVal [UVal]
-
-instance Unifiable UVal where
- unify' (UVVal vl1) (UVVal vl2)
- | length vl1 /= length vl2 = error "length mismatch during unification"
- | otherwise = foldr mergeU emptyUnifier (map (\(x,y) -> unify x y) $ zip vl1 vl2)
- unify' _ _ = error "impossible"
- inject = UVVar
- project (UVVar v) = Just v
- project _ = Nothing
- occurrences (UVVar v) = [v]
- occurrences (UVVal vl) = concatMap occurrences vl
-
--- | Resolves a unification variable; the answer to this query will change if subsequent unifications are performed
-getU' :: Unifier UVal -> UVal -> UVal
-getU' u (UVVal vl) = UVVal $ map (getU' u) vl
-getU' u x@(UVVar v) = case Unify.getU u v of
- Nothing -> x
- Just x' -> getU' u x'
-
-
-
+------------------------------------------------------------------------------
+-- Tracks
--
--- | Render a fully-polymorphic GArrow term as a boxes-and-wires diagram using TikZ
+-- Figuring out the x-coordinates of the boxes is easy, but we'll need
+-- to use lp_solve to get a nice layout for the y-coordinates of the
+-- wires. A @Track@ is basically just a y-axis position for one of
+-- the horizontal wires in the boxes-and-wires diagram; we will assign
+-- a unique Int to each visual element that has a y-coordinate, then
+-- generate a big pile of constraints on these y-coordinates and have
+-- lp_solve find a solution.
--
+type TrackIdentifier = Int
-type Constraints = [(UVal, Int, UVal)]
+data Tracks = T TrackIdentifier
+ | TU TrackIdentifier -- a track known to be of unit type
+ | TT Tracks Tracks
--- the unification monad
-data UyM t a = UyM (([UVar],Unifier UVal,Constraints) -> ([UVar],Unifier UVal,Constraints,a))
-instance Monad (UyM t)
- where
- return x = UyM $ \(i,u,k) -> (i,u,k,x)
- (UyM f) >>= g = UyM $ \(i,u,k) -> let (i',u',k',x) = f (i,u,k) in let UyM g' = g x in g' (i',u',k')
-
-
-getU = UyM $ \(i,u,k) -> (i,u,k,u)
-getM v = UyM $ \(i,u,k) -> (i,u,k,getU' u v)
-occursU v x = UyM $ \(i,u,k) -> (i,u,k,occurs u v x)
-unifyM :: Eq t => UVal -> UVal -> UyM t ()
-unifyM v1 v2 = UyM $ \(i,u,k) -> (i,mergeU u (unify v1 v2),k,())
-freshU :: UyM t UVar
-freshU = UyM $ \(i:is,u,k) -> (is,u,k,i)
-constrain :: UVal -> Int -> UVal -> UyM t ()
-constrain v1 d v2 = UyM $ \(i,u,k) -> (i,u,((v1,d,v2):k),())
-getK :: UyM t [(UVal, Int, UVal)]
-getK = UyM $ \(i,u,k) -> (i,u,k,k)
-runU :: UyM t a -> ([UVar],Unifier UVal,Constraints,a)
-runU (UyM f) = (f (uvarSupply,emptyUnifier,[]))
-
-data GArrowTikZ :: * -> * -> *
- where
- TikZ_const :: Int -> GArrowTikZ () Int
- TikZ_id :: GArrowTikZ x x
- TikZ_comp :: GArrowTikZ y z -> GArrowTikZ x y -> GArrowTikZ x z
- TikZ_first :: GArrowTikZ x y -> GArrowTikZ (x**z) (y**z)
- TikZ_second :: GArrowTikZ x y -> GArrowTikZ (z**x) (z**y)
- TikZ_cancell :: GArrowTikZ (()**x) x
- TikZ_cancelr :: GArrowTikZ (x**()) x
- TikZ_uncancell :: GArrowTikZ x (()**x)
- TikZ_uncancelr :: GArrowTikZ x (x**())
- TikZ_assoc :: GArrowTikZ ((x**y)**z) (x**(y**z))
- TikZ_unassoc :: GArrowTikZ (x**(y**z)) ((x**y)**z)
- TikZ_drop :: GArrowTikZ x ()
- TikZ_copy :: GArrowTikZ x (x**x)
- TikZ_swap :: GArrowTikZ (x**y) (y**x)
- TikZ_merge :: GArrowTikZ (x**y) z
- TikZ_loopl :: GArrowTikZ (x**z) (y**z) -> GArrowTikZ x y
- TikZ_loopr :: GArrowTikZ (z**x) (z**y) -> GArrowTikZ x y
+instance Show Tracks where
+ show (T ti ) = "(T "++show ti++")"
+ show (TU ti ) = "(TU "++show ti++")"
+ show (TT t1 t2) = "(TT "++show t1++" "++show t2++")"
--
--- Technically this instance violates the laws (and RULEs) for
--- Control.Category; the compiler might choose to optimize (f >>> id)
--- into f, and this optimization would produce a change in behavior
--- below. In practice this means that the user must be prepared for
--- the rendered TikZ diagram to be merely *equivalent to* his/her
--- term, rather than structurally exactly equal to it.
---
-instance Category GArrowTikZ where
- id = TikZ_id
- (.) = TikZ_comp
-
-instance GArrow GArrowTikZ (**) () where
- ga_first = TikZ_first
- ga_second = TikZ_second
- ga_cancell = TikZ_cancell
- ga_cancelr = TikZ_cancelr
- ga_uncancell = TikZ_uncancell
- ga_uncancelr = TikZ_uncancelr
- ga_assoc = TikZ_assoc
- ga_unassoc = TikZ_unassoc
-
-instance GArrowDrop GArrowTikZ (**) () where
- ga_drop = TikZ_drop
-
-instance GArrowCopy GArrowTikZ (**) () where
- ga_copy = TikZ_copy
-
-instance GArrowSwap GArrowTikZ (**) () where
- ga_swap = TikZ_swap
-
-instance GArrowLoop GArrowTikZ (**) () where
- ga_loopl = TikZ_loopl
- ga_loopr = TikZ_loopr
-
-instance GArrowSTKC GArrowTikZ (,) ()
-
-
-name :: GArrowTikZ a b -> String
-name TikZ_id = "id"
-name (TikZ_const i) = "const " ++ show i
-name (TikZ_comp _ _) = "comp"
-name (TikZ_first _ ) = "first"
-name (TikZ_second _ ) = "second"
-name TikZ_cancell = "cancell"
-name TikZ_cancelr = "cancelr"
-name TikZ_uncancell = "uncancell"
-name TikZ_uncancelr = "uncancelr"
-name TikZ_drop = "drop"
-name TikZ_copy = "copy"
-name TikZ_swap = "swap"
-name (TikZ_loopl _ ) = "loopl"
-name (TikZ_loopr _ ) = "loopr"
-name TikZ_assoc = "assoc"
-name TikZ_unassoc = "unassoc"
-
-fresh1 :: UyM () Ports
-fresh1 = do { x <- freshU
- ; return $ UVVar x
- }
-
-fresh2 :: UyM () (Ports,Ports)
-fresh2 = do { x <- freshU
- ; y <- freshU
- ; constrain (UVVar x) 1 (UVVar y)
- ; return $ (UVVar x,UVVar y)
- }
+-- | TrackPositions maps TrackIdentifiers to actual y-axis positions;
+-- this is what lp_solve gives us
+--
+type TrackPositions = TrackIdentifier -> Float
-fresh3 :: UyM () (Ports,Ports,Ports)
-fresh3 = do { x <- freshU
- ; y <- freshU
- ; z <- freshU
- ; constrain (UVVar x) 1 (UVVar y)
- ; constrain (UVVar y) 1 (UVVar z)
- ; return $ (UVVar x,UVVar y,UVVar z)
- }
+(!) :: TrackPositions -> TrackIdentifier -> Float
+tp ! ti = tp ti
-fresh4 :: UyM () (Ports,Ports,Ports,Ports)
-fresh4 = do { x1 <- freshU
- ; x2 <- freshU
- ; x3 <- freshU
- ; x4 <- freshU
- ; constrain (UVVar x1) 1 (UVVar x2)
- ; constrain (UVVar x2) 1 (UVVar x3)
- ; constrain (UVVar x3) 1 (UVVar x4)
- ; return $ (UVVar x1,UVVar x2,UVVar x3,UVVar x4)
- }
+-- | get the uppermost TrackIdentifier in a Tracks
+uppermost (T x) = x
+uppermost (TU x) = x
+uppermost (TT x y) = uppermost x
-fresh5 :: UyM () (Ports,Ports,Ports,Ports,Ports)
-fresh5 = do { x1 <- freshU
- ; x2 <- freshU
- ; x3 <- freshU
- ; x4 <- freshU
- ; x5 <- freshU
- ; constrain (UVVar x1) 1 (UVVar x2)
- ; constrain (UVVar x2) 1 (UVVar x3)
- ; constrain (UVVar x3) 1 (UVVar x4)
- ; constrain (UVVar x4) 1 (UVVar x5)
- ; return $ (UVVar x1,UVVar x2,UVVar x3,UVVar x4,UVVar x5)
- }
+-- | get the lowermost TrackIdentifier in a Tracks
+lowermost (T x) = x
+lowermost (TU x) = x
+lowermost (TT x y) = lowermost y
---example = ga_first ga_drop >>> ga_cancell >>> ga_first id >>> ga_swap >>> ga_first id >>> TikZ_merge
---example :: forall x y z. forall g. (GArrow g (,) (), GArrowCopy g (,) (), GArrowSwap g (,) ()) => g x ((x,x),x)
---example = ga_copy >>> ga_second ga_copy >>> ga_second (ga_first id) >>> ga_unassoc >>> ga_first ga_swap
---example = ga_copy >>> ga_second ga_copy >>> ga_second (ga_second id) >>> ga_unassoc >>> ga_first id >>> ga_first ga_swap
---example :: forall x. forall g. (GArrow g (,) (), GArrowCopy g (,) (), GArrowSwap g (,) ()) => g x x
---example = id >>> id
+------------------------------------------------------------------------------
+-- Diagrams
-data Diagram p = DiagramComp (Diagram p) (Diagram p)
- | DiagramPrim String p p p p (String -> Int -> Int -> Int -> p -> p -> Int -> String)
- | DiagramBypassTop p (Diagram p)
- | DiagramBypassBot (Diagram p) p
- -- | DiagramLoopTop Diagram
- -- | DiagramLoopBot Diagram
+-- | A Diagram is the visual representation of a GArrowSkeleton
+data Diagram
+ = DiagramComp Diagram Diagram
+ | DiagramBox TrackIdentifier Tracks BoxRenderer Tracks TrackIdentifier
+ | DiagramBypassTop Tracks Diagram
+ | DiagramBypassBot Diagram Tracks
+ -- | DiagramLoopTop Tracks Diagram
+ -- | DiagramLoopBot Diagram Tracks
-type Ports = UVal
-
-getOut :: Diagram Ports -> Ports
+-- | get the output tracks of a diagram
+getOut :: Diagram -> Tracks
getOut (DiagramComp f g) = getOut g
-getOut (DiagramPrim s ptop pin pout pbot _) = pout
-getOut (DiagramBypassTop p f) = UVVal [p, (getOut f)]
-getOut (DiagramBypassBot f p) = UVVal [(getOut f), p]
+getOut (DiagramBox ptop pin q pout pbot) = pout
+getOut (DiagramBypassTop p f) = TT p (getOut f)
+getOut (DiagramBypassBot f p) = TT (getOut f) p
-getIn :: Diagram Ports -> Ports
+-- | get the input tracks of a diagram
+getIn :: Diagram -> Tracks
getIn (DiagramComp f g) = getIn f
-getIn (DiagramPrim s ptop pin pout pbot _) = pin
-getIn (DiagramBypassTop p f) = UVVal [p, (getIn f)]
-getIn (DiagramBypassBot f p) = UVVal [(getIn f), p]
+getIn (DiagramBox ptop pin q pout pbot) = pin
+getIn (DiagramBypassTop p f) = TT p (getIn f)
+getIn (DiagramBypassBot f p) = TT (getIn f) p
+
+-- | A BoxRenderer is just a routine that, given the dimensions of a
+-- boxes-and-wires box element, knows how to spit out a bunch of TikZ
+-- code that draws it
+type BoxRenderer =
+ TrackPositions -> -- resolves the TrackIdentifiers to actual y-coordinates
+ Float -> -- x1
+ Float -> -- y1
+ Float -> -- x2
+ Float -> -- y2
+ String -- TikZ code
+
+
+
+
+
+
+------------------------------------------------------------------------------
+-- Constraints
+
+-- | a constraint (to be dealt with by lp_solve) relates two track identifiers
+data Constraint = C TrackIdentifier Ordering TrackIdentifier {- plus -} Float
+ | EqualSpace TrackIdentifier TrackIdentifier TrackIdentifier TrackIdentifier
+
+-- instance Show Constraint where
+-- show (C t1 LT t2 k s) = "x"++(show t1)++" = x"++(show t2)++" + "++(show k) ++ ";\n"
+-- show (C t1 GT t2 k s) = "x"++(show t1)++" = x"++(show t2)++" + "++(show k) ++ ";\n"
+-- show (C t1 EQ t2 k s) = "x"++(show t1)++" = x"++(show t2)++" + "++(show k) ++ ";\n"
+
+instance Show Constraint where
+ show (C t1 LT t2 k) = "x"++(show t1)++" <= x"++(show t2)++" + "++(show k) ++ ";\n"
+ show (C t1 GT t2 k) = "x"++(show t1)++" >= x"++(show t2)++" + "++(show k) ++ ";\n"
+ show (C t1 EQ t2 k) = "x"++(show t1)++" = x"++(show t2)++" + "++(show k) ++ ";\n"
+ show (EqualSpace t1a t1b t2a t2b) = "x"++(show t1a)++" = x"++(show t1b)++
+ " + x"++(show t2a)++" - x"++(show t2b)++ ";\n"
+
+-- | a monad to accumulate constraints and track the largest TrackIdentifier allocated
+type ConstraintM a = State (TrackIdentifier,[Constraint]) a
+
+-- | pull the constraints out of the monad
+getConstraints :: ConstraintM [Constraint]
+getConstraints = do { (_,c) <- get ; return c }
+
+-- | add a constraint
+constrain :: TrackIdentifier -> Ordering -> TrackIdentifier {- plus -} -> Float -> ConstraintM ()
+constrain t1 ord t2 k = do { (t,c) <- get
+ ; put (t, (C t1 ord t2 k):c)
+ ; return ()
+ }
+
+constrainEqualSpace t1a t1b t2a t2b = do { (t,c) <- get
+ ; put (t, (EqualSpace t1a t1b t2a t2b):c)
+ ; return ()
+ }
+
+-- | simple form for equality constraints
+constrainEq (TT t1a t1b) (TT t2a t2b) = do { constrainEq t1a t2a ; constrainEq t1b t2b ; return () }
+constrainEq (T t1 ) (T t2 ) = constrain t1 EQ t2 0
+constrainEq (TU t1 ) (TU t2 ) = constrain t1 EQ t2 0
+constrainEq (TU t1 ) (T t2 ) = constrain t1 EQ t2 0
+constrainEq (T t1 ) (TU t2 ) = constrain t1 EQ t2 0
+constrainEq t1 t2 = error $ "constrainEq mismatch: " ++ show t1 ++ " and " ++ show t2
+
+-- | allocate a TrackIdentifier
+alloc1 :: ConstraintM Tracks
+alloc1 = do { (t,c) <- get
+ ; put (t+1,c)
+ ; return (T t)
+ }
+
+
+mkdiag :: GArrowPortShape m () a b -> ConstraintM Diagram
+mkdiag (GASPortPassthrough inp outp m) = error "not supported"
+mkdiag (GASPortShapeWrapper inp outp x) = mkdiag' x
+ where
+ mkdiag' :: GArrowSkeleton (GArrowPortShape m ()) a b -> ConstraintM Diagram
+
+ mkdiag' (GAS_comp f g) = do { f' <- mkdiag' f; g' <- mkdiag' g
+ ; constrainEq (getOut f') (getIn g') ; return $ DiagramComp f' g' }
+ mkdiag' (GAS_first f) = do { (top,(TT _ x),bot) <- alloc inp; f' <- mkdiag' f ; constrainBot f' 1 (uppermost x)
+ ; return $ DiagramBypassBot f' x }
+ mkdiag' (GAS_second f) = do { (top,(TT x _),bot) <- alloc inp; f' <- mkdiag' f ; constrainTop (lowermost x) 1 f'
+ ; return $ DiagramBypassTop x f' }
+ mkdiag' (GAS_id ) = do { (top, x ,bot) <- alloc inp ; simpleDiag "id" top x x bot [(x,x)] }
+ mkdiag' GAS_cancell = do { (top,(TT x y),bot) <- alloc inp
+ ; let r tp x1 y1 x2 y2 = drawBox x1 y1 x2 y2 "gray!50" "cancell" ++
+ drawWires tp x1 y x2 y "black" ++
+ drawLine x1 (tp!lowermost x) ((x1+x2)/2) (tp!uppermost y) "black" "dashed"
+ ; return $ DiagramBox top (TT x y) r y bot }
+ mkdiag' GAS_cancelr = do { (top,(TT x y),bot) <- alloc inp
+ ; let r tp x1 y1 x2 y2 = drawBox x1 y1 x2 y2 "gray!50" "cancelr" ++
+ drawWires tp x1 x x2 x "black" ++
+ drawLine x1 (tp!uppermost y) ((x1+x2)/2) (tp!lowermost x) "black" "dashed"
+ ; return $ DiagramBox top (TT x y) r x bot }
+ mkdiag' GAS_uncancell = do { (top,(TT x y),bot) <- alloc outp
+ ; let r tp x1 y1 x2 y2 = drawBox x1 y1 x2 y2 "gray!50" "uncancell" ++
+ drawWires tp x1 y x2 y "black" ++
+ drawLine ((x1+x2)/2) (tp!uppermost y) x2 (tp!lowermost x) "black" "dashed"
+ ; return $ DiagramBox top y r (TT x y) bot }
+ mkdiag' GAS_uncancelr = do { (top,(TT x y),bot) <- alloc outp
+ ; let r tp x1 y1 x2 y2 = drawBox x1 y1 x2 y2 "gray!50" "uncancelr" ++
+ drawWires tp x1 x x2 x "black" ++
+ drawLine ((x1+x2)/2) (tp!lowermost x) x2 (tp!uppermost y) "black" "dashed"
+ ; return $ DiagramBox top x r (TT x y) bot }
+ mkdiag' GAS_drop = do { (top, x ,bot) <- alloc inp ; simpleDiag "drop" top x x bot [] }
+ mkdiag' (GAS_const i) = do { (top, x ,bot) <- alloc inp
+ ; (_, y ,_) <- alloc outp
+ ; constrainEq x y
+ ; simpleDiag ("const " ++ show i) top x y bot [] }
+ mkdiag' GAS_copy = do { (top,(TT y z),bot) <- alloc outp
+ ; (_ , x ,_) <- alloc inp
+ ; constrainEqualSpace (lowermost y) (uppermost x) (lowermost x) (uppermost z)
+ ; let r tp x1 y1 x2 y2 = drawBox x1 y1 x2 y2 "gray!50" "copy" ++
+ drawWires tp x1 x ((x1+x2)/2) x "black" ++
+ drawWires tp ((x1+x2)/2) x x2 y "black" ++
+ drawWires tp ((x1+x2)/2) x x2 z "black"
+ ; return $ DiagramBox top x r (TT y z) bot
+ }
+ mkdiag' GAS_merge = do { (top,(TT x y),bot) <- alloc inp
+ ; simpleDiag "times" top (TT x y) x bot [] }
+ mkdiag' GAS_swap = do { (top,(TT x y),bot) <- alloc inp
+ ; (top,(TT x' y'),bot) <- alloc outp
+ ; constrainEq (T (lowermost x)) (T (lowermost x'))
+ ; constrainEq (T (uppermost y)) (T (uppermost y'))
+ ; simpleDiag' "swap" top (TT x y) (TT x' y') bot [(x,y'),(y,x')] "gray!50" }
+ mkdiag' GAS_assoc =
+ do { (top,(TT (TT x y) z),bot) <- alloc inp
+ ; let r tp x1 y1 x2 y2
+ = drawBox (x1+0.2*xscale) y1 (x2-0.2*xscale) y2 "white" "assoc" ++
+ drawLine x1 y1 x2 y1 "gray!50" "-" ++
+ drawLine x1 y2 x2 y2 "gray!50" "-" ++
+ drawLine x1 y1 x1 ((tp ! uppermost x) - 0.5) "gray!50" "-"++
+ drawLine x1 ((tp ! uppermost x) - 0.5) (x1+0.2) ((tp ! uppermost x) - 0.5) "gray!50" "-"++
+ drawLine (x1+0.2) ((tp ! uppermost x) - 0.5) (x1+0.2) ((tp ! lowermost y) + 0.5) "gray!50" "-"++
+ drawLine (x1+0.2) ((tp ! lowermost y) + 0.5) x1 ((tp ! lowermost y) + 0.5) "gray!50" "-"++
+ drawLine x1 ((tp ! lowermost y) + 0.5) x1 y2 "gray!50" "-"++
+ drawLine x2 y2 x2 ((tp ! lowermost z) + 0.5) "gray!50" "-"++
+ drawLine x2 ((tp ! lowermost z) + 0.5) (x2-0.2) ((tp ! lowermost z) + 0.5) "gray!50" "-"++
+ drawLine (x2-0.2) ((tp ! lowermost z) + 0.5) (x2-0.2) ((tp ! uppermost y) - 0.5) "gray!50" "-"++
+ drawLine (x2-0.2) ((tp ! uppermost y) - 0.5) x2 ((tp ! uppermost y) - 0.5) "gray!50" "-"++
+ drawLine x2 ((tp ! uppermost y) - 0.5) x2 y1 "gray!50" "-"++
+ drawWires tp x1 x x2 x "black" ++
+ drawWires tp x1 y x2 y "black" ++
+ drawWires tp x1 z x2 z "black"
+ ; return $ DiagramBox top (TT (TT x y) z) r (TT x (TT y z)) bot
+ }
+ mkdiag' GAS_unassoc =
+ do { (top,(TT x (TT y z)),bot) <- alloc inp
+ ; let r tp x1 y1 x2 y2
+ = drawBox (x1+0.2*xscale) y1 (x2-0.2*xscale) y2 "white" "unassoc" ++
+ drawLine x1 y1 x2 y1 "gray!50" "-" ++
+ drawLine x1 y2 x2 y2 "gray!50" "-" ++
+ drawLine x2 y1 x2 ((tp ! uppermost x) - 0.5) "gray!50" "-"++
+ drawLine x2 ((tp ! uppermost x) - 0.5) (x2-0.2) ((tp ! uppermost x) - 0.5) "gray!50" "-"++
+ drawLine (x2-0.2) ((tp ! uppermost x) - 0.5) (x2-0.2) ((tp ! lowermost y) + 0.5) "gray!50" "-"++
+ drawLine (x2-0.2) ((tp ! lowermost y) + 0.5) x2 ((tp ! lowermost y) + 0.5) "gray!50" "-"++
+ drawLine x2 ((tp ! lowermost y) + 0.5) x2 y2 "gray!50" "-"++
+ drawLine x1 y2 x1 ((tp ! lowermost z) + 0.5) "gray!50" "-"++
+ drawLine x1 ((tp ! lowermost z) + 0.5) (x1+0.2) ((tp ! lowermost z) + 0.5) "gray!50" "-"++
+ drawLine (x1+0.2) ((tp ! lowermost z) + 0.5) (x1+0.2) ((tp ! uppermost y) - 0.5) "gray!50" "-"++
+ drawLine (x1+0.2) ((tp ! uppermost y) - 0.5) x1 ((tp ! uppermost y) - 0.5) "gray!50" "-"++
+ drawLine x1 ((tp ! uppermost y) - 0.5) x1 y1 "gray!50" "-"++
+ drawWires tp x1 x x2 x "black" ++
+ drawWires tp x1 y x2 y "black" ++
+ drawWires tp x1 z x2 z "black"
+ ; return $ DiagramBox top (TT x (TT y z)) r (TT (TT x y) z) bot
+ }
+ mkdiag' (GAS_loopl f) = error "not implemented"
+ mkdiag' (GAS_loopr f) = error "not implemented"
+ mkdiag' (GAS_misc f ) = mkdiag f
+
+ diagramBox :: TrackIdentifier -> Tracks -> BoxRenderer -> Tracks -> TrackIdentifier -> ConstraintM Diagram
+ diagramBox ptop pin r pout pbot = do { constrain ptop LT (uppermost pin) (-1)
+ ; constrain pbot GT (lowermost pin) 1
+ ; constrain ptop LT (uppermost pout) (-1)
+ ; constrain pbot GT (lowermost pout) 1
+ ; constrain ptop LT pbot (-1)
+ ; return $ DiagramBox ptop pin r pout pbot
+ }
+ simpleDiag text ptop pin pout pbot conn = simpleDiag' text ptop pin pout pbot conn "black"
+ simpleDiag' text ptop pin pout pbot conn color = diagramBox ptop pin defren pout pbot
+ where
+ defren tp x1 y1 x2 y2 = drawBox x1 y1 x2 y2 color text ++
+ concat (map (\(x,y) -> drawWires tp x1 x x2 y "black") conn)
+ -- ++ wires (x-1) p1 x "green"
+ -- ++ wires (x+w) p2 (x+w+1) "red"
-- constrain that Ports is at least Int units above the topmost portion of Diagram
-constrainTop :: Ports -> Int -> Diagram Ports -> UyM () ()
+constrainTop :: TrackIdentifier -> Float -> Diagram -> ConstraintM ()
constrainTop v i (DiagramComp d1 d2) = do { constrainTop v i d1 ; constrainTop v i d2 ; return () }
-constrainTop v i (DiagramBypassTop p d) = constrain v 2 p
+constrainTop v i (DiagramBypassTop p d) = constrain v LT (uppermost p) (-1 * i)
constrainTop v i (DiagramBypassBot d p) = constrainTop v (i+1) d
-constrainTop v i (DiagramPrim s ptop pin pout pbot _) = constrain v i ptop
+constrainTop v i (DiagramBox ptop pin r pout pbot) = constrain v LT ptop (-1 * i)
-- constrain that Ports is at least Int units below the bottommost portion of Diagram
-constrainBot :: Diagram Ports -> Int -> Ports -> UyM () ()
+constrainBot :: Diagram -> Float -> TrackIdentifier -> ConstraintM ()
constrainBot (DiagramComp d1 d2) i v = do { constrainBot d1 i v ; constrainBot d2 i v ; return () }
constrainBot (DiagramBypassTop p d) i v = constrainBot d (i+1) v
-constrainBot (DiagramBypassBot d p) i v = constrain p 2 v
-constrainBot (DiagramPrim s ptop pin pout pbot _) i v = constrain pbot i v
-
-ga2diag :: GArrowTikZ a b -> UyM () (Diagram Ports)
-ga2diag (TikZ_id ) = do { (top,x,bot) <- fresh3 ; return $ DiagramPrim "id" top x x bot defren }
-ga2diag (TikZ_comp g f) = do { f' <- ga2diag f
- ; g' <- ga2diag g
- ; unifyM (getOut f') (getIn g')
- ; return $ DiagramComp f' g' }
-ga2diag (TikZ_first f) = do { x <- fresh1; f' <- ga2diag f ; constrainBot f' 1 x ; return $ DiagramBypassBot f' x }
-ga2diag (TikZ_second f) = do { x <- fresh1; f' <- ga2diag f ; constrainTop x 1 f' ; return $ DiagramBypassTop x f' }
-ga2diag TikZ_cancell = do { (top,x,y ,bot) <- fresh4 ; return $ DiagramPrim "cancell" top (UVVal [x,y]) y bot defren }
-ga2diag TikZ_cancelr = do { (top,x,y ,bot) <- fresh4 ; return $ DiagramPrim "cancelr" top (UVVal [x,y]) x bot defren }
-ga2diag TikZ_uncancell = do { (top,x,y ,bot) <- fresh4 ; return $ DiagramPrim "uncancell" top y (UVVal [x,y]) bot defren }
-ga2diag TikZ_uncancelr = do { (top,x,y ,bot) <- fresh4 ; return $ DiagramPrim "uncancelr" top x (UVVal [x,y]) bot defren }
-ga2diag TikZ_drop = do { (top,x ,bot) <- fresh3 ; return $ DiagramPrim "drop" top x x bot defren }
-ga2diag (TikZ_const i) = do { (top,x ,bot) <- fresh3 ; return $ DiagramPrim ("const " ++ show i) top x x bot defren }
-ga2diag TikZ_copy = do { (top,x,y,z,bot) <- fresh5
- ; return $ DiagramPrim "copy" top y (UVVal [x,z]) bot defren }
-ga2diag TikZ_merge = do { (top,x,y,z,bot) <- fresh5
- ; return $ DiagramPrim "merge" top (UVVal [x,z]) y bot defren }
-ga2diag TikZ_swap = do { (top,x,y ,bot) <- fresh4
- ; return $ DiagramPrim "swap" top (UVVal [x,y]) (UVVal [x,y]) bot defren }
-ga2diag TikZ_assoc = do { (top,x,y,z,bot) <- fresh5
- ; return $ DiagramPrim "assoc" top (UVVal [UVVal [x,y],z])(UVVal [x,UVVal [y,z]]) bot defren }
-ga2diag TikZ_unassoc = do { (top,x,y,z,bot) <- fresh5
- ; return $ DiagramPrim "unassoc" top (UVVal [x,UVVal [y,z]])(UVVal [UVVal [x,y],z]) bot defren }
-ga2diag (TikZ_loopl f) = error "not implemented"
-ga2diag (TikZ_loopr f) = error "not implemented"
-
-defren :: String -> Int -> Int -> Int -> Ports -> Ports -> Int -> String
-defren s x w top p1 p2 bot
- = drawBox x top (x+w) bot "black" s
--- ++ wires (x-1) p1 x "green"
--- ++ wires (x+w) p2 (x+w+1) "red"
-
-xscale = 1
-yscale = 1
-
-textc x y text color =
- "\\node[anchor=center,color="++color++"] at ("++show (x*xscale)++"cm,"++show (y*yscale)++"cm) "++
- "{{\\tt{"++text++"}}};\n"
-
-drawBox x1 y1 x2 y2 color text =
- "\\node[anchor=north west] at ("++show (x1*xscale)++"cm,"++show (y1*yscale)++"cm) "++
- "{{\\tt{"++text++"}}};\n"
- ++
- "\\path[draw,color="++color++"]"++
- " ("++show (x1*xscale)++","++show (y1*yscale)++") rectangle ("++
- show (x2*xscale)++","++show (y2*yscale)++");\n"
-
-drawLine x1 y1 x2 y2 color style =
- "\\path[draw,color="++color++","++style++"] "++
- "("++show (x1*xscale)++","++show (y1*yscale)++") -- " ++
- "("++show (x2*xscale)++","++show (y2*yscale)++");\n"
-
-width :: Diagram Ports -> Int
-width (DiagramComp d1 d2) = (width d1) + 1 + (width d2)
-width (DiagramPrim s _ p1 p2 _ _) = 2
-width (DiagramBypassTop p d) = (width d) + 2
-width (DiagramBypassBot d p) = (width d) + 2
-
-(!) :: Map UVar Int -> UVar -> Int
-m ! x = case lookup x m of
- Nothing -> 0
- Just y -> y
-
-tikZ :: Map UVar Int ->
- Diagram Ports ->
- Int -> -- horizontal position
+constrainBot (DiagramBypassBot d p) i v = constrain v GT (lowermost p) 2
+constrainBot (DiagramBox ptop pin r pout pbot) i v = constrain v GT pbot i
+
+-- | The width of a box is easy to calculate
+width :: Diagram -> Float
+width (DiagramComp d1 d2) = (width d1) + 1 + (width d2)
+width (DiagramBox ptop pin x pout pbot) = 2
+width (DiagramBypassTop p d) = (width d) + 2
+width (DiagramBypassBot d p) = (width d) + 2
+
+drawWires :: TrackPositions -> Float -> Tracks -> Float -> Tracks -> String -> String
+drawWires tp x1 (TT a b) x2 (TT a' b') color = drawWires tp x1 a x2 a' color ++ drawWires tp x1 b x2 b' color
+drawWires tp x1 (T a) x2 (T a') color = drawLine x1 (tp!a) x2 (tp!a') color "-"
+drawWires tp x1 (TU a) x2 (TU a') color = drawLine x1 (tp!a) x2 (tp!a') color "dashed"
+drawWires tp _ _ _ _ _ = error "drawwires fail"
+
+tikZ :: TrackPositions ->
+ Diagram ->
+ Float -> -- horizontal position
String
tikZ m = tikZ'
where
tikZ' d@(DiagramComp d1 d2) x = tikZ' d1 x
- ++ wires (x+width d1) (getOut d1) (x+width d1+1) "black"
+ ++ wires' (x+width d1) (getOut d1) (x+width d1+0.5) "black" "->"
+ ++ wires' (x+width d1+0.5) (getOut d1) (x+width d1+1) "black" "-"
++ tikZ' d2 (x + width d1 + 1)
tikZ' d'@(DiagramBypassTop p d) x = let top = getTop d' in
let bot = getBot d' in
drawBox x top (x+width d') bot "gray!50" "second"
- ++ drawLine x (top+1) (x+width d') (top+1) "black" "->"
- ++ wires x (getIn d) (x+1) "black"
+ ++ drawWires m x (getIn d) (x+1) (getIn d) "black"
++ tikZ' d (x+1)
- ++ wires (x+1+width d) (getOut d) (x+1+width d+1) "black"
+ ++ drawWires m (x+1+width d) (getOut d) (x+1+width d+1) (getOut d) "black"
+ ++ drawWires m x p (x+1+width d+1) p "black"
tikZ' d'@(DiagramBypassBot d p) x = let top = getTop d' in
let bot = getBot d' in
drawBox x top (x+width d') bot "gray!50" "first"
- ++ drawLine x (bot-1) (x+width d') (bot-1) "black" "->"
- ++ wires x (getIn d) (x+1) "black"
+ ++ drawWires m x (getIn d) (x+1) (getIn d) "black"
++ tikZ' d (x+1)
- ++ wires (x+1+width d) (getOut d) (x+1+width d+1) "black"
- tikZ' d@(DiagramPrim s (UVVar top) p1 p2 (UVVar bot) r) x = r s x (width d) (m ! top) p1 p2 (m ! bot)
-
- wires :: Int -> Ports -> Int -> String -> String
- wires x1 (UVVar v) x2 color = drawLine x1 (m ! v) x2 (m ! v) color "->"
- -- ++ textc ((x1+x2) `div` 2) (m!v) (show v) "purple"
- wires x1 (UVVal vl) x2 color = foldr (\x y -> x ++ " " ++ y) [] (map (\v -> wires x1 v x2 color) vl)
-
- getTop :: Diagram Ports -> Int
- getTop (DiagramComp d1 d2) = min (getTop d1) (getTop d2)
- getTop (DiagramBypassTop p d) = (m ! getleft p) - 1
- getTop (DiagramBypassBot d p) = getTop d - 1
- getTop (DiagramPrim s (UVVar ptop) _ _ _ _) = m ! ptop
-
- getBot :: Diagram Ports -> Int
- getBot (DiagramComp d1 d2) = max (getBot d1) (getBot d2)
- getBot (DiagramBypassTop p d) = getBot d + 1
- getBot (DiagramBypassBot d p) = (m ! getright p) + 1
- getBot (DiagramPrim s _ _ _ (UVVar pbot) _) = m ! pbot
-
-resolve' (DiagramComp d1 d2) = do { d1' <- resolve' d1 ; d2' <- resolve' d2 ; return $ DiagramComp d1' d2' }
-resolve' (DiagramBypassTop p d) = do { p' <- getM p ; d' <- resolve' d ; return $ DiagramBypassTop p' d' }
-resolve' (DiagramBypassBot d p) = do { p' <- getM p ; d' <- resolve' d ; return $ DiagramBypassBot d' p' }
-resolve' (DiagramPrim s ptop pin pout pbot r)
- = do { ptop' <- getM ptop
- ; pbot' <- getM pbot
- ; pin' <- getM pin
- ; pout' <- getM pout
- ; return $ DiagramPrim s ptop' pin' pout' pbot' r }
-
-getleft (UVVar v) = v
-getleft (UVVal vl) = getleft (head vl)
-
-getright (UVVar v) = v
-getright (UVVal vl) = getright (last vl)
-
-strip :: [(Ports,Int,Ports)] -> [(UVar,Int,UVar)]
-strip = map (\(v1,x,v2) -> (getright v1, x, getleft v2))
-
-
--- must use bubblesort because the ordering isn't transitive
-sortit :: [(UVar,Int,UVar)] -> [(UVar,Int,UVar)]
-sortit x = stupidSort x []
+ ++ drawWires m (x+1+width d) (getOut d) (x+1+width d+1) (getOut d) "black"
+ ++ drawWires m x p (x+1+width d+1) p "black"
+ tikZ' d@(DiagramBox ptop pin r pout pbot) x = r m x (m ! ptop) (x + width d) (m ! pbot)
+
+ wires x1 t x2 c = wires' x1 t x2 c "-"
+
+ wires' :: Float -> Tracks -> Float -> String -> String -> String
+ wires' x1 (TT x y) x2 color st = wires' x1 x x2 color st ++ wires' x1 y x2 color st
+ wires' x1 (T v) x2 color st = drawLine x1 (m ! v) x2 (m ! v) color st -- ++ textc ((x1+x2) / 2) (m!v) (show v) "purple"
+ wires' x1 (TU v) x2 color st = drawLine x1 (m ! v) x2 (m ! v) color "dashed"
+
+ getTop :: Diagram -> Float
+ getTop (DiagramComp d1 d2) = min (getTop d1) (getTop d2)
+ getTop (DiagramBox ptop _ _ _ _) = m ! ptop
+ getTop (DiagramBypassTop p d) = (m ! uppermost p) - 1
+ getTop (DiagramBypassBot d p) = getTop d - 1
+
+ getBot :: Diagram -> Float
+ getBot (DiagramComp d1 d2) = max (getBot d1) (getBot d2)
+ getBot (DiagramBox _ _ _ _ pbot) = m ! pbot
+ getBot (DiagramBypassTop p d) = getBot d + 1
+ getBot (DiagramBypassBot d p) = (m ! lowermost p) + 1
+
+-- allocates multiple tracks, adding constraints that they are at least one unit apart
+alloc :: PortShape a -> ConstraintM (TrackIdentifier,Tracks,TrackIdentifier)
+alloc shape = do { tracks <- alloc' shape
+ ; T ptop <- alloc1
+ ; T pbot <- alloc1
+ ; constrain ptop LT (uppermost tracks) (-1)
+ ; constrain pbot GT (lowermost tracks) 1
+ ; return (ptop,tracks,pbot)
+ }
+ where
+ alloc' :: PortShape a -> ConstraintM Tracks
+ alloc' PortUnit = do { T x <- alloc1 ; return (TU x) }
+ alloc' (PortFree _) = do { x <- alloc1 ; return x }
+ alloc' (PortTensor p1 p2) = do { x1 <- alloc' p1
+ ; x2 <- alloc' p2
+ ; constrain (lowermost x1) LT (uppermost x2) (-1)
+ ; return (TT x1 x2)
+ }
+
+do_lp_solve :: [Constraint] -> IO String
+do_lp_solve c = do { let stdin = "min: x1;\n" ++ (foldl (++) "" (map show c)) ++ "\n"
+ ; putStrLn stdin
+ ; stdout <- readProcess "lp_solve" [] stdin
+ ; return stdout
+ }
+
+splitWs :: String -> [String]
+splitWs s = splitWs' "" s
where
- stupidSort [] x = x
- stupidSort (h:t) x = stupidSort t (stupidInsert h x)
-
- stupidInsert t [] = [t]
- stupidInsert t@(_,_,t') ((a@(_,_,a')):b) = if cmp' x t' a' == LT
- then t:a:b
- else a:(stupidInsert t b)
-
- cmp' :: [(UVar,Int,UVar)] -> UVar -> UVar -> Ordering
- cmp' [] a b = EQ -- compare a b
- cmp' ((v1,_,v2):r) a b = if a == v1 && b==v2
- then LT
- else if a == v2 && b==v1
- then GT
- else cmp' r a b
-
-lookup'' :: Map UVar Int -> UVar -> Int
-lookup'' m x = case lookup x m of
- Nothing -> 0
- Just y -> y
-
-valuatit :: Map UVar Int -> [(UVar,Int,UVar)] -> Map UVar Int
-valuatit m [] = m
-valuatit m ((v1,k,v2):r) = valuatit m' r
- where
- m' = insert v2 v2' m
- v2' = max (lookup'' m v2) (k+(lookup'' m v1))
-
-resolve'k :: UyM () [(Ports,Int,Ports)]
-resolve'k = do { k <- getK
- ; k' <- mapM (\(v1,x,v2) -> do { v1' <- getM v1 ; v2' <- getM v2 ; return (v1',x,v2') }) k
- ; return k'
- }
-
-toTikZ :: GArrowTikZ a b -> String
-toTikZ g = tikZ m d 0
- where
- (_,_,_,(d,k)) = runU $ do { d <- ga2diag g
- ; d' <- resolve' d
- ; k' <- resolve'k
- ; return (d',k') }
- s = sortit (strip k)
- m = valuatit empty s
-toTikZ' :: GArrowTikZ a b -> String
-toTikZ' g = foldr (\x y -> x++"\\\\\n"++y) [] (map foo s)
- where
- (_,_,_,k) = runU $ ga2diag g >>= resolve' >>= \_ -> resolve'k
- foo (v1,v,v2) = "x_{"++show v1++"} + "++show v++" \\leq x_{"++show v2++"} = " ++ (show $ lookup'' m v2)
- s = sortit (strip k)
- m = valuatit empty s
-
-tikz example
+ splitWs' [] [] = []
+ splitWs' acc [] = [acc]
+ splitWs' [] (' ':k) = splitWs' [] k
+ splitWs' acc (' ':k) = acc:(splitWs' [] k)
+ splitWs' acc (x:k) = splitWs' (acc++[x]) k
+
+lp_solve_to_trackpos :: String -> TrackPositions
+lp_solve_to_trackpos s = toTrackPos $ map parse $ catMaybes $ map grab $ lines s
+ where
+ grab ('x':k) = Just k
+ grab _ = Nothing
+ parse :: String -> (Int,Float)
+ parse s = case splitWs s of
+ [a,b] -> (read a, read b)
+ _ -> error "parse: should not happen"
+ toTrackPos :: [(Int,Float)] -> TrackPositions
+ toTrackPos [] tr = 0 -- error $ "could not find track "++show tr
+ toTrackPos ((i,f):rest) tr = if (i==tr) then f else toTrackPos rest tr
+
+toTikZ :: GArrowSkeleton m a b -> IO String
+toTikZ g =
+ let cm = do { let g' = detectShape g
+ ; g'' <- mkdiag g'
+ ; return g''
+ }
+ in do { let (_,constraints) = execState cm (0,[])
+ ; lps <- do_lp_solve $ constraints
+ ; let trackpos = lp_solve_to_trackpos lps
+ ; return $ tikZ trackpos (evalState cm (0,[])) 0
+ }
+
+tikz :: (forall g a .
+ (Int -> PGArrow g (GArrowUnit g) a) ->
+ (
+ forall b . PGArrow g (GArrowTensor g b b) b) ->
+ PGArrow g (GArrowUnit g) a) -> IO ()
+
+tikz x = tikz' $ optimize $ unG (x (\c -> PGArrowD { unG = GAS_const c }) (PGArrowD { unG = GAS_merge }) )
+
+tikz' example
= do putStrLn "\\documentclass{article}"
- putStrLn "\\usepackage[landscape,paperheight=20in,textwidth=19in]{geometry}"
+ putStrLn "\\usepackage[paperwidth=\\maxdimen,paperheight=\\maxdimen]{geometry}"
putStrLn "\\usepackage{tikz}"
putStrLn "\\usepackage{amsmath}"
+ putStrLn "\\usepackage[tightpage,active]{preview}"
putStrLn "\\begin{document}"
+ putStrLn "\\setlength\\PreviewBorder{5pt}"
+ putStrLn "\\begin{preview}"
putStrLn $ "\\begin{tikzpicture}[every on chain/.style={join=by ->},yscale=-1]"
- putStrLn (toTikZ example)
+ tikz <- toTikZ example
+ putStrLn tikz
putStrLn "\\end{tikzpicture}"
--- putStrLn "\\begin{align*}"
--- putStr (toTikZ' example)
--- putStrLn "\\end{align*}"
+ putStrLn "\\end{preview}"
+ --putStrLn "\\pagebreak"
+ --putStrLn "\\begin{align*}"
+ --putStr (toTikZ' example)
+ --putStrLn "\\end{align*}"
putStrLn "\\end{document}"
+
+-- Random TikZ routines
+textc x y text color =
+ "\\node[anchor=center,color="++color++"] at ("++show (x*xscale)++"cm,"++show (y*yscale)++"cm) "++
+ "{{\\tt{"++text++"}}};\n"
+
+drawBox x1 y1 x2 y2 color text =
+ "\\node[anchor=north west] at ("++show (x1*xscale)++"cm,"++show (y1*yscale)++"cm) "++
+ "{{\\tt{"++text++"}}};\n"
+ ++
+ "\\path[draw,color="++color++"]"++
+ " ("++show (x1*xscale)++","++show (y1*yscale)++") rectangle ("++
+ show (x2*xscale)++","++show (y2*yscale)++");\n"
+
+drawLine x1 y1 x2 y2 color style =
+ "\\path[draw,color="++color++","++style++"] "++
+ "("++show (x1*xscale)++","++show (y1*yscale)++") -- " ++
+ "("++show (x2*xscale)++","++show (y2*yscale)++");\n"
+
+-- | x scaling factor for the entire diagram, since TikZ doesn't scale font sizes
+xscale = 1
+
+-- | y scaling factor for the entire diagram, since TikZ doesn't scale font sizes
+yscale = 1
projects / coq-hetmet.git / blobdiff