Merge branch 'coq-extraction-baked-in' of /afs/megacz.com/.pub/software/coq-hetmet
[coq-hetmet.git] / examples / GArrowTikZ.hs
1 {-# LANGUAGE RankNTypes, MultiParamTypeClasses, GADTs, FlexibleContexts, FlexibleInstances, TypeOperators #-}
2 -----------------------------------------------------------------------------
3 -- |
4 -- Module      :  GArrowTikZ
5 -- Copyright   :  none
6 -- License     :  public domain
7 --
8 -- Maintainer  :  Adam Megacz <megacz@acm.org>
9 -- Stability   :  experimental
10 --
11 -- | Renders a @GArrowSkeleton@ using TikZ; the result is LaTeX code.
12 -- You must have lp_solve installed in order for this to work.
13 --
14
15 module GArrowTikZ (tikz)
16 where
17 import System.Process
18 import Prelude hiding ( id, (.), lookup )
19 import Control.Category
20 import Control.Monad.State
21 import GHC.HetMet.GArrow
22 import Data.List hiding (lookup, insert)
23 import Data.Map hiding (map, (!))
24 import Data.Maybe (catMaybes)
25 import Unify
26 import GArrowSkeleton
27 import GArrowPortShape
28 import GHC.HetMet.Private
29
30 ------------------------------------------------------------------------------
31 -- Tracks
32
33 --
34 -- Figuring out the x-coordinates of the boxes is easy, but we'll need
35 -- to use lp_solve to get a nice layout for the y-coordinates of the
36 -- wires.  A @Track@ is basically just a y-axis position for one of
37 -- the horizontal wires in the boxes-and-wires diagram; we will assign
38 -- a unique Int to each visual element that has a y-coordinate, then
39 -- generate a big pile of constraints on these y-coordinates and have
40 -- lp_solve find a solution.
41 --
42 type TrackIdentifier = Int
43
44 data Tracks = T  TrackIdentifier
45             | TU TrackIdentifier  -- a track known to be of unit type
46             | TT Tracks Tracks
47
48 instance Show Tracks where
49  show (T  ti   ) = "(T "++show ti++")"
50  show (TU ti   ) = "(TU "++show ti++")"
51  show (TT t1 t2) = "(TT "++show t1++" "++show t2++")"
52
53 --
54 -- | TrackPositions maps TrackIdentifiers to actual y-axis positions;
55 -- this is what lp_solve gives us
56 -- 
57 type TrackPositions = TrackIdentifier -> Float
58
59 (!) :: TrackPositions -> TrackIdentifier -> Float
60 tp ! ti = tp ti
61
62 -- | get the uppermost TrackIdentifier in a Tracks
63 uppermost  (T x)    = x
64 uppermost  (TU x)    = x
65 uppermost  (TT x y) = uppermost x
66
67 -- | get the lowermost TrackIdentifier in a Tracks
68 lowermost (T x)    = x
69 lowermost (TU x)    = x
70 lowermost (TT x y) = lowermost y
71
72
73
74
75 ------------------------------------------------------------------------------
76 -- Diagrams
77
78 -- | A Diagram is the visual representation of a GArrowSkeleton
79 data Diagram
80   = DiagramComp      Diagram Diagram
81   | DiagramBox       Float TrackIdentifier Tracks BoxRenderer Tracks TrackIdentifier
82   | DiagramBypassTop Tracks Diagram
83   | DiagramBypassBot        Diagram Tracks
84   | DiagramLoopTop   Tracks Diagram
85   | DiagramLoopBot          Diagram Tracks
86
87 -- | get the output tracks of a diagram
88 getOut :: Diagram -> Tracks
89 getOut (DiagramComp f g)                     = getOut g
90 getOut (DiagramBox wid ptop pin q pout pbot)     = pout
91 getOut (DiagramBypassTop p f)                = TT p (getOut f)
92 getOut (DiagramBypassBot f p)                = TT (getOut f) p
93 getOut (DiagramLoopTop t d)                  = case getOut d of { TT z y -> y ; _ -> error "DiagramLoopTop: mismatch" }
94 getOut (DiagramLoopBot d t)                  = case getOut d of { TT y z -> y ; _ -> error "DiagramLoopBot: mismatch" }
95
96 -- | get the input tracks of a diagram
97 getIn :: Diagram -> Tracks
98 getIn (DiagramComp f g)                      = getIn f
99 getIn (DiagramBox wid ptop pin q pout pbot)      = pin
100 getIn (DiagramBypassTop p f)                 = TT p (getIn f)
101 getIn (DiagramBypassBot f p)                 = TT (getIn f) p
102 getIn (DiagramLoopTop t d)                   = case getIn d of { TT z x -> x ; _ -> error "DiagramLoopTop: mismatch" }
103 getIn (DiagramLoopBot d t)                   = case getIn d of { TT x z -> x ; _ -> error "DiagramLoopBot: mismatch" }
104
105 -- | A BoxRenderer is just a routine that, given the dimensions of a
106 -- boxes-and-wires box element, knows how to spit out a bunch of TikZ
107 -- code that draws it
108 type BoxRenderer =
109     TrackPositions ->  -- resolves the TrackIdentifiers to actual y-coordinates
110     Float          ->  -- x1
111     Float          ->  -- y1
112     Float          ->  -- x2
113     Float          ->  -- y2
114     String             -- TikZ code
115 noRender :: BoxRenderer
116 noRender _ _ _ _ _ = ""
117
118
119
120
121 ------------------------------------------------------------------------------
122 -- Constraints
123
124 -- | a constraint (to be dealt with by lp_solve) relates two track identifiers
125 data Constraint = C TrackIdentifier Ordering TrackIdentifier {- plus -} Float
126                 | EqualSpace TrackIdentifier TrackIdentifier TrackIdentifier TrackIdentifier
127
128 -- instance Show Constraint where
129 --  show (C t1 LT t2 k s) = "x"++(show t1)++"  = x"++(show t2)++" + "++(show k) ++ ";\n"
130 --  show (C t1 GT t2 k s) = "x"++(show t1)++"  = x"++(show t2)++" + "++(show k) ++ ";\n"
131 --  show (C t1 EQ t2 k s) = "x"++(show t1)++"  = x"++(show t2)++" + "++(show k) ++ ";\n"
132
133 instance Show Constraint where
134  show (C t1 LT t2 k) = "x"++(show t1)++" <= x"++(show t2)++" + "++(show k) ++ ";\n"
135  show (C t1 GT t2 k) = "x"++(show t1)++" >= x"++(show t2)++" + "++(show k) ++ ";\n"
136  show (C t1 EQ t2 k) = "x"++(show t1)++"  = x"++(show t2)++" + "++(show k) ++ ";\n"
137  show (EqualSpace t1a t1b t2a t2b) = "x"++(show t1a)++" = x"++(show t1b)++
138                                      " + x"++(show t2a)++" - x"++(show t2b)++ ";\n"
139
140 -- | a monad to accumulate constraints and track the largest TrackIdentifier allocated
141 type ConstraintM a = State (TrackIdentifier,[Constraint]) a
142
143 -- | pull the constraints out of the monad
144 getConstraints :: ConstraintM [Constraint]
145 getConstraints = do { (_,c) <- get ; return c }
146
147 -- | add a constraint
148 constrain :: TrackIdentifier -> Ordering -> TrackIdentifier {- plus -} -> Float -> ConstraintM ()
149 constrain t1 ord t2 k = do { (t,c) <- get
150                            ; put (t, (C t1 ord t2 k):c)
151                            ; return ()
152                            }
153
154 constrainEqualSpace t1a t1b t2a t2b = do { (t,c) <- get
155                                          ; put (t, (EqualSpace t1a t1b t2a t2b):c)
156                                          ; return ()
157                                          }
158
159 -- | simple form for equality constraints
160 constrainEq (TT t1a t1b) (TT t2a t2b) = do { constrainEq t1a t2a ; constrainEq t1b t2b ; return () }
161 constrainEq (T  t1     ) (T  t2     ) = constrain t1 EQ t2 0
162 constrainEq (TU t1     ) (TU t2     ) = constrain t1 EQ t2 0
163 constrainEq (TU t1     ) (T  t2     ) = constrain t1 EQ t2 0
164 constrainEq (T  t1     ) (TU t2     ) = constrain t1 EQ t2 0
165 constrainEq t1 t2                     = error $ "constrainEq mismatch: " ++ show t1 ++ " and " ++ show t2
166
167 -- | allocate a TrackIdentifier
168 alloc1 :: ConstraintM Tracks
169 alloc1 = do { (t,c) <- get
170             ; put (t+1,c)
171             ; return (T t)
172             }
173
174 mkdiag :: GArrowPortShape m () a b -> ConstraintM Diagram
175 mkdiag (GASPortPassthrough  inp outp m) = error "not supported"
176 mkdiag (GASPortShapeWrapper inp outp x) = mkdiag' x
177  where
178  mkdiag' :: GArrowSkeleton (GArrowPortShape m ()) a b -> ConstraintM Diagram
179  
180  mkdiag' (GAS_comp f g) = do { f' <- mkdiag' f; g' <- mkdiag' g
181                              ; constrainEq (getOut f') (getIn g') ; return $ DiagramComp f' g' }
182  mkdiag' (GAS_first  f) = do { (top,(TT _ x),bot) <- alloc inp; f' <- mkdiag' f ; constrainBot f' 1 (uppermost x)
183                              ; return $ DiagramBypassBot f' x  }
184  mkdiag' (GAS_second f) = do { (top,(TT x _),bot) <- alloc inp; f' <- mkdiag' f ; constrainTop (lowermost x) 1 f'
185                              ; return $ DiagramBypassTop x f'  }
186  mkdiag' (GAS_id      ) = do { (top,    x   ,bot) <- alloc inp ; simpleDiag'        "id" top x x bot        [(x,x)]  "gray!50"    }
187  mkdiag' GAS_cancell    = do { (top,(TT x y),bot) <- alloc inp
188                              ; let r tp x1 y1 x2 y2 = drawBox x1 y1 x2 y2 "gray!50" "cancell" ++
189                                                       drawWires tp x1 y x2 y "black" ++
190                                                       drawLine  x1 (tp!lowermost x)  ((x1+x2)/2) (tp!uppermost y) "gray!50" "dashed"
191                              ; return $ DiagramBox 2 top (TT x y) r y bot  }
192  mkdiag' GAS_cancelr    = do { (top,(TT x y),bot) <- alloc inp
193                              ; let r tp x1 y1 x2 y2 = drawBox x1 y1 x2 y2 "gray!50" "cancelr" ++
194                                                       drawWires tp x1 x x2 x "black" ++
195                                                       drawLine  x1 (tp!uppermost y) ((x1+x2)/2) (tp!lowermost x) "gray!50" "dashed"
196                              ; return $ DiagramBox 2 top (TT x y) r x bot  }
197  mkdiag' GAS_uncancell  = do { (top,(TT x y),bot) <- alloc outp
198                              ; let r tp x1 y1 x2 y2 = drawBox x1 y1 x2 y2 "gray!50" "uncancell" ++
199                                                       drawWires tp x1 y x2 y "black" ++
200                                                       drawLine  ((x1+x2)/2) (tp!uppermost y) x2 (tp!lowermost x) "gray!50" "dashed"
201                              ; return $ DiagramBox 2 top y r (TT x y) bot  }
202  mkdiag' GAS_uncancelr  = do { (top,(TT x y),bot) <- alloc outp
203                              ; let r tp x1 y1 x2 y2 = drawBox x1 y1 x2 y2 "gray!50" "uncancelr" ++
204                                                       drawWires tp x1 x x2 x "black" ++
205                                                       drawLine  ((x1+x2)/2) (tp!lowermost x) x2 (tp!uppermost y) "gray!50" "dashed"
206                              ; return $ DiagramBox 2 top x r (TT x y) bot  }
207  mkdiag' GAS_drop       = do { (top,    x   ,bot) <- alloc inp ; simpleDiag      "drop" top x x bot [] }
208  mkdiag' (GAS_const i)  = do { (top,    x   ,bot) <- alloc inp
209                              ; (_,      y   ,_)   <- alloc outp
210                              ; constrainEq x y
211                              ; simpleDiag   ("const " ++ show i) top x y bot [] }
212  mkdiag' GAS_copy       = do { (top,(TT y z),bot) <- alloc outp
213                              ; (_  ,      x ,_)   <- alloc inp
214                              ; constrainEqualSpace (lowermost y) (uppermost x) (lowermost x) (uppermost z)
215                              ; let r tp x1 y1 x2 y2 = drawBox x1 y1 x2 y2 "gray!50" "copy" ++
216                                                       drawWires tp x1 x ((x1+x2)/2) x "black" ++
217                                                       drawWires tp ((x1+x2)/2) x x2 y "black" ++
218                                                       drawWires tp ((x1+x2)/2) x x2 z "black"
219                              ; return $ DiagramBox 2 top x r (TT y z) bot
220                              }
221  mkdiag' GAS_merge      = do { (top,(TT x y),bot) <- alloc inp 
222                              ; simpleDiag     "times" top (TT x y) x bot [] }
223  mkdiag' GAS_swap       = do { (top,(TT x y),bot) <- alloc inp
224                              ; (top,(TT x' y'),bot) <- alloc outp
225                              ; constrainEq (T (lowermost x)) (T (lowermost x'))
226                              ; constrainEq (T (uppermost y)) (T (uppermost y'))
227                              ; simpleDiag'    "swap"  top (TT x y) (TT x' y') bot [(x,y'),(y,x')] "gray!50" }
228  mkdiag' GAS_assoc      =
229      do { (top,(TT (TT x y) z),bot) <- alloc inp
230         ; let r tp x1 y1 x2 y2
231                   = drawBox (x1+0.2*xscale) y1 (x2-0.2*xscale) y2 "white" "assoc" ++
232                     drawLine x1 y1 x2 y1 "gray!50" "-" ++
233                     drawLine x1 y2 x2 y2 "gray!50" "-" ++
234                     drawLine  x1      y1                          x1      ((tp ! uppermost x) - 0.5) "gray!50" "-"++
235                     drawLine  x1      ((tp ! uppermost x) - 0.5) (x1+0.2) ((tp ! uppermost x) - 0.5) "gray!50" "-"++
236                     drawLine (x1+0.2) ((tp ! uppermost x) - 0.5) (x1+0.2) ((tp ! lowermost y) + 0.5) "gray!50" "-"++
237                     drawLine (x1+0.2) ((tp ! lowermost y) + 0.5)  x1      ((tp ! lowermost y) + 0.5) "gray!50" "-"++
238                     drawLine  x1      ((tp ! lowermost y) + 0.5)  x1      y2                         "gray!50" "-"++
239                     drawLine  x2      y2                          x2      ((tp ! lowermost z) + 0.5) "gray!50" "-"++
240                     drawLine  x2      ((tp ! lowermost z) + 0.5) (x2-0.2) ((tp ! lowermost z) + 0.5) "gray!50" "-"++
241                     drawLine (x2-0.2) ((tp ! lowermost z) + 0.5) (x2-0.2) ((tp ! uppermost y) - 0.5) "gray!50" "-"++
242                     drawLine (x2-0.2) ((tp ! uppermost y) - 0.5)  x2      ((tp ! uppermost y) - 0.5) "gray!50" "-"++
243                     drawLine  x2      ((tp ! uppermost y) - 0.5)  x2      y1                         "gray!50" "-"++
244                     drawWires tp x1 x x2 x "black" ++
245                     drawWires tp x1 y x2 y "black" ++
246                     drawWires tp x1 z x2 z "black"
247         ; let pin = (TT (TT x y) z)
248         ; let pout = (TT x (TT y z))
249         ; return $ if draw_assoc then DiagramBox 2 top pin r pout bot else DiagramBox 0 top pin noRender pout bot
250         }
251  mkdiag' GAS_unassoc    =
252      do { (top,(TT x (TT y z)),bot) <- alloc inp
253         ; let r tp x1 y1 x2 y2
254                   = drawBox (x1+0.2*xscale) y1 (x2-0.2*xscale) y2 "white" "unassoc" ++
255                     drawLine x1 y1 x2 y1 "gray!50" "-" ++
256                     drawLine x1 y2 x2 y2 "gray!50" "-" ++
257                     drawLine  x2      y1                          x2      ((tp ! uppermost x) - 0.5) "gray!50" "-"++
258                     drawLine  x2      ((tp ! uppermost x) - 0.5) (x2-0.2) ((tp ! uppermost x) - 0.5) "gray!50" "-"++
259                     drawLine (x2-0.2) ((tp ! uppermost x) - 0.5) (x2-0.2) ((tp ! lowermost y) + 0.5) "gray!50" "-"++
260                     drawLine (x2-0.2) ((tp ! lowermost y) + 0.5)  x2      ((tp ! lowermost y) + 0.5) "gray!50" "-"++
261                     drawLine  x2      ((tp ! lowermost y) + 0.5)  x2      y2                         "gray!50" "-"++
262                     drawLine  x1      y2                          x1      ((tp ! lowermost z) + 0.5) "gray!50" "-"++
263                     drawLine  x1      ((tp ! lowermost z) + 0.5) (x1+0.2) ((tp ! lowermost z) + 0.5) "gray!50" "-"++
264                     drawLine (x1+0.2) ((tp ! lowermost z) + 0.5) (x1+0.2) ((tp ! uppermost y) - 0.5) "gray!50" "-"++
265                     drawLine (x1+0.2) ((tp ! uppermost y) - 0.5)  x1      ((tp ! uppermost y) - 0.5) "gray!50" "-"++
266                     drawLine  x1      ((tp ! uppermost y) - 0.5)  x1      y1                         "gray!50" "-"++
267                     drawWires tp x1 x x2 x "black" ++
268                     drawWires tp x1 y x2 y "black" ++
269                     drawWires tp x1 z x2 z "black"
270         ; let pin = (TT x (TT y z))
271         ; let pout = (TT (TT x y) z)
272         ; return $ if draw_assoc then DiagramBox 2 top pin r pout bot else DiagramBox 0 top pin noRender pout bot
273         }
274  mkdiag' (GAS_loopl  f) = do { f' <- mkdiag' f
275                              ; l <- allocLoop (case (getIn f') of (TT z _) -> z ; _ -> error "GAS_loopl: mismatch")
276                              ; constrainTop (lowermost l) loopgap f'
277                              ; return $ DiagramLoopTop l f'  }
278  mkdiag' (GAS_loopr  f) = do { f' <- mkdiag' f
279                              ; l <- allocLoop (case (getIn f') of (TT _ z) -> z ; _ -> error "GAS_loopr: mismatch")
280                              ; constrainBot f' loopgap (uppermost l)
281                              ; return $ DiagramLoopBot f' l  }
282  mkdiag' (GAS_misc f )  = mkdiag f
283
284  diagramBox :: TrackIdentifier -> Tracks -> BoxRenderer -> Tracks -> TrackIdentifier -> ConstraintM Diagram
285  diagramBox ptop pin r pout pbot = do { constrain ptop LT (uppermost pin)  (-1)
286                                       ; constrain pbot GT (lowermost pin)  1
287                                       ; constrain ptop LT (uppermost pout) (-1)
288                                       ; constrain pbot GT (lowermost pout) 1
289                                       ; constrain ptop LT pbot (-1)
290                                       ; return $ DiagramBox 2 ptop pin r pout pbot
291                                       }
292  simpleDiag  text ptop pin pout pbot conn = simpleDiag' text ptop pin pout pbot conn "black"
293  simpleDiag' text ptop pin pout pbot conn color = diagramBox ptop pin defren pout pbot
294   where
295    defren tp x1 y1 x2 y2 = drawBox x1 y1 x2 y2 color text ++
296                            concat (map (\(x,y) -> drawWires tp x1 x x2 y "black") conn)
297    --    ++ wires (x-1) p1  x    "green"
298    --    ++ wires  (x+w) p2 (x+w+1) "red"
299
300 --draw_assoc = False
301 --draw_first_second = False
302 draw_assoc = True
303 draw_first_second = True
304
305 -- constrain that Ports is at least Int units above the topmost portion of Diagram
306 constrainTop :: TrackIdentifier -> Float -> Diagram -> ConstraintM ()
307 constrainTop v i (DiagramComp d1 d2)                  = do { constrainTop v i d1 ; constrainTop v i d2 ; return () }
308 constrainTop v i (DiagramBypassTop p d)               = constrain v LT (uppermost p) (-1 * i)
309 constrainTop v i (DiagramBypassBot d p)               = constrainTop v (i+1) d
310 constrainTop v i (DiagramBox wid ptop pin r pout pbot)    = constrain v LT ptop (-1 * i)
311 constrainTop v i (DiagramLoopTop p d)                 = constrain v LT (uppermost p) (-1 * i)
312 constrainTop v i (DiagramLoopBot d p)                 = constrainTop v (i+1) d
313
314 -- constrain that Ports is at least Int units below the bottommost portion of Diagram
315 constrainBot :: Diagram -> Float -> TrackIdentifier -> ConstraintM ()
316 constrainBot (DiagramComp d1 d2)                  i v = do { constrainBot d1 i v ; constrainBot d2 i v ; return () }
317 constrainBot (DiagramBypassTop p d)               i v = constrainBot d (i+1) v
318 constrainBot (DiagramBypassBot d p)               i v = constrain v GT (lowermost p) 2
319 constrainBot (DiagramBox wid ptop pin r pout pbot)    i v = constrain v GT pbot i
320 constrainBot (DiagramLoopTop p d)                 i v = constrainBot d (i+1) v
321 constrainBot (DiagramLoopBot d p)                 i v = constrain v GT (lowermost p) 2
322
323 -- | The width of a box is easy to calculate
324 width :: TrackPositions -> Diagram -> Float
325 width m (DiagramComp d1 d2)               = (width m d1) + 1 + (width m d2)
326 width m (DiagramBox wid ptop pin x pout pbot) = wid
327 width m (DiagramBypassTop p d)            = (width m d) + (if draw_first_second then 2 else 0)
328 width m (DiagramBypassBot d p)            = (width m d) + (if draw_first_second then 2 else 0)
329 width m (DiagramLoopTop p d)              = (width m d) + 2 + 2 * (loopgap + (m ! lowermost p) - (m ! uppermost p))
330 width m (DiagramLoopBot d p)              = (width m d) + 2 + 2 * (loopgap + (m ! lowermost p) - (m ! uppermost p))
331
332 drawWires :: TrackPositions -> Float -> Tracks -> Float -> Tracks -> String -> String
333 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
334 drawWires tp x1 (T a)    x2 (T a')     color = drawLine x1 (tp!a) x2 (tp!a') color     "-"
335 drawWires tp x1 (TU a)   x2 (TU a')    color = drawLine x1 (tp!a) x2 (tp!a') "gray!50" "dashed"
336 drawWires tp _ _ _ _ _                       = error "drawwires fail"
337
338 wirecos :: TrackPositions -> Tracks -> [(Float,Bool)]
339 wirecos tp (TT a b) = wirecos tp a ++ wirecos tp b
340 wirecos tp (T  a)   = [(tp!a,True)]
341 wirecos tp (TU a)   = [(tp!a,False)]
342
343 wire90 :: Float -> Float -> (Float,Float,Bool) -> String
344 wire90 x y (y1,y2,b) = drawLine' [(x,y1),(x',y1),(x',y2),(x,y2)] color (style++",rounded corners")
345  where
346   color = if b then "black" else "gray!50"
347   style = if b then "-" else "dashed"
348   x'    = x - (y - y1) - loopgap
349
350 wire90' x y (y1,y2,b) = drawLine' [(x,y1),(x',y1),(x',y2),(x,y2)] color (style++",rounded corners")
351  where
352   color = if b then "black" else "gray!50"
353   style = if b then "-" else "dashed"
354   x'    = x + (y - y1) + loopgap
355
356 tikZ :: TrackPositions ->
357         Diagram ->
358         Float ->                -- horizontal position
359         String
360 tikZ m = tikZ'
361  where
362   tikZ'  d@(DiagramComp d1 d2)    x = tikZ' d1 x
363                                       ++ wires' (x+width m d1) (getOut d1) (x+width m d1+0.5) "black" "->"
364                                       ++ wires' (x+width m d1+0.5) (getOut d1) (x+width m d1+1) "black" "-"
365                                       ++ tikZ' d2 (x + width m d1 + 1)
366   tikZ' d'@(DiagramBypassTop p d) x = if not draw_first_second
367                                       then drawWires m x p (x+width m d) p "black" ++ tikZ' d x
368                                       else
369                                       let top = getTop d' in
370                                       let bot = getBot d' in
371                                       drawBox  x top (x+width m d') bot "gray!50" "second"
372                                       ++ drawWires m x (getIn d) (x+1) (getIn d) "black"
373                                       ++ tikZ' d (x+1)
374                                       ++ drawWires m (x+1+width m d) (getOut d) (x+1+width m d+1) (getOut d) "black"
375                                       ++ drawWires m x p (x+1+width m d+1) p "black"
376   tikZ' d'@(DiagramBypassBot d p) x = if not draw_first_second
377                                       then drawWires m x p (x+width m d) p "black" ++ tikZ' d x
378                                       else
379                                       let top = getTop d' in
380                                       let bot = getBot d' in
381                                       drawBox  x top (x+width m d') bot "gray!50" "first"
382                                       ++ drawWires m x (getIn d) (x+1) (getIn d) "black"
383                                       ++ tikZ' d (x+1)
384                                       ++ drawWires m (x+1+width m d) (getOut d) (x+1+width m d+1) (getOut d) "black"
385                                       ++ drawWires m x p (x+1+width m d+1) p "black"
386   tikZ' d'@(DiagramLoopTop p d) x   = let top = getTop d' in
387                                       let bot = getBot d' in
388                                       let gap = loopgap + (m ! lowermost p) - (m ! uppermost p) in
389                                       drawBox  x top (x+width m d') bot "gray!50" "loopl"
390                                       ++ tikZ' d (x+1+gap)
391                                       ++ drawWires m (x+1+gap) p (x+1+gap+width m d) p "black"
392                                       ++ let p'   = case getIn d of TT z _ -> z ; _ -> error "DiagramLoopTop: mismatch"
393                                              pzip = map (\((y,b),(y',_)) -> (y,y',b)) $ zip (wirecos m p) (reverse $ wirecos m p')
394                                          in  concatMap (wire90  (x+1+gap) (m ! lowermost p)) pzip
395                                       ++ let p'   = case getOut d of TT z _ -> z ; _ -> error "DiagramLoopTop: mismatch"
396                                              pzip = map (\((y,b),(y',_)) -> (y,y',b)) $ zip (wirecos m p) (reverse $ wirecos m p')
397                                          in  concatMap (wire90' (x+1+gap+width m d) (m ! lowermost p)) pzip
398                                       ++ let rest = case getIn d of TT _ z -> z ; _ -> error "DiagramLoopTop: mismatch"
399                                          in  drawWires m x rest (x+1+gap) rest "black"
400                                       ++ let rest = case getOut d of TT _ z -> z ; _ -> error "DiagramLoopTop: mismatch"
401                                          in  drawWires m (x+1+gap+width m d) rest (x+width m d') rest "black"
402   tikZ' d'@(DiagramLoopBot d p) x_  = error "not implemented"
403   tikZ' d@(DiagramBox wid ptop pin r pout pbot) x = r m x (m ! ptop) (x + width m d) (m ! pbot)
404
405   wires x1 t x2 c = wires' x1 t x2 c "-"
406
407   wires' :: Float -> Tracks -> Float -> String -> String -> String
408   wires' x1 (TT x y) x2 color st = wires' x1 x x2 color st ++ wires' x1 y x2 color st
409   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"
410   wires' x1 (TU v)   x2 color st = drawLine x1 (m ! v) x2 (m ! v) "gray!50" "dashed"
411
412   getTop :: Diagram -> Float
413   getTop (DiagramComp d1 d2)        = min (getTop d1) (getTop d2)
414   getTop (DiagramBox wid ptop _ _ _ _)  = m ! ptop
415   getTop (DiagramBypassTop p d)     = (m ! uppermost p) - 1
416   getTop (DiagramBypassBot d p)     = getTop d - 1
417   getTop (DiagramLoopTop p d)       = (m ! uppermost p) - 1
418   getTop (DiagramLoopBot d p)       = getTop d - 1
419
420   getBot :: Diagram -> Float
421   getBot (DiagramComp d1 d2)        = max (getBot d1) (getBot d2)
422   getBot (DiagramBox wid _ _ _ _ pbot)  = m ! pbot
423   getBot (DiagramBypassTop p d)     = getBot d + 1
424   getBot (DiagramBypassBot d p)     = (m ! lowermost p) + 1
425   getBot (DiagramLoopTop p d)       = getBot d + 1
426   getBot (DiagramLoopBot d p)       = (m ! lowermost p) + 1
427
428 -- allocates multiple tracks, adding constraints that they are at least one unit apart
429 alloc :: PortShape a -> ConstraintM (TrackIdentifier,Tracks,TrackIdentifier)
430 alloc shape = do { tracks <- alloc' shape
431                  ; T ptop <- alloc1
432                  ; T pbot <- alloc1
433                  ; constrain ptop LT (uppermost tracks) (-1)
434                  ; constrain pbot GT (lowermost tracks) 1
435                  ; return (ptop,tracks,pbot)
436                  }
437  where
438    alloc' :: PortShape a -> ConstraintM Tracks
439    alloc' PortUnit           = do { T x <- alloc1 ; return (TU x) }
440    alloc' (PortFree _)       = do { x <- alloc1 ; return x }
441    alloc' (PortTensor p1 p2) = do { x1 <- alloc' p1
442                                   ; x2 <- alloc' p2
443                                   ; constrain (lowermost x1) LT (uppermost x2) (-1)
444                                   ; return (TT x1 x2)
445                                   }
446
447 -- allocates a second set of tracks identical to the first one but constrained only relative to each other (one unit apart)
448 -- and upside-down
449 allocLoop :: Tracks -> ConstraintM Tracks
450 allocLoop (TU _)       = do { T x <- alloc1 ; return (TU x) }
451 allocLoop (T  _)       = do { x <- alloc1   ; return x }
452 allocLoop (TT t1 t2)   = do { x1 <- allocLoop t2
453                             ; x2 <- allocLoop t1
454                             ; constrain (lowermost x1) LT (uppermost x2) (-1)
455                             ; return (TT x1 x2)
456                             }
457
458 do_lp_solve :: [Constraint] -> IO String
459 do_lp_solve c = do { let stdin = "min: x1;\n" ++ (foldl (++) "" (map show c)) ++ "\n"
460                    ; putStrLn stdin
461                    ; stdout <- readProcess "lp_solve" [] stdin
462                    ; return stdout
463                    }
464
465 splitWs :: String -> [String]
466 splitWs s = splitWs' "" s
467  where
468   splitWs' [] []       = []
469   splitWs' acc []      = [acc]
470   splitWs' []  (' ':k) = splitWs' [] k
471   splitWs' acc (' ':k) = acc:(splitWs' [] k)
472   splitWs' acc (x:k)   = splitWs' (acc++[x]) k
473
474 lp_solve_to_trackpos :: String -> TrackPositions
475 lp_solve_to_trackpos s = toTrackPos $ map parse $ catMaybes $ map grab $ lines s
476  where
477    grab ('x':k) = Just k
478    grab _       = Nothing
479    parse :: String -> (Int,Float)
480    parse s = case splitWs s of
481                [a,b] -> (read a, read b)
482                _     -> error "parse: should not happen"
483    toTrackPos :: [(Int,Float)] -> TrackPositions
484    toTrackPos []           tr = 0 -- error $ "could not find track "++show tr
485    toTrackPos ((i,f):rest) tr = if (i==tr) then f else toTrackPos rest tr
486
487 toTikZ :: GArrowSkeleton m a b -> IO String
488 toTikZ g = 
489     let cm = do { let g' = detectShape g
490                 ; g'' <- mkdiag g'
491                 ; return g''
492                 }
493      in do { let (_,constraints) = execState cm (0,[])
494            ; lps <- do_lp_solve $ constraints
495            ; let m = lp_solve_to_trackpos lps
496            ; let d = evalState cm (0,[])
497            ; let t = tikZ m d 1
498            ; return (t ++ drawWires m 0             (getIn  d) 1             (getIn  d) "black"
499                        ++ drawWires m (width m d+1) (getOut d) (width m d+2) (getOut d) "black")
500            }
501      
502
503 tikz :: forall c .
504     (forall g .
505              (Int -> PGArrow g (GArrowUnit g) Int) ->
506              (PGArrow g (GArrowTensor g c c) c) ->
507              PGArrow g c c)
508      -> IO ()
509 tikz x = tikz' $ beautify $ optimize $ unG (x (\c -> PGArrowD { unG = GAS_const c }) (PGArrowD { unG = GAS_merge }))
510
511 tikz' example
512      = do putStrLn "\\documentclass{article}"
513           putStrLn "\\usepackage[paperwidth=\\maxdimen,paperheight=\\maxdimen]{geometry}"
514           putStrLn "\\usepackage{tikz}"
515           putStrLn "\\usepackage{amsmath}"
516           putStrLn "\\usepackage[tightpage,active]{preview}"
517           putStrLn "\\begin{document}"
518           putStrLn "\\setlength\\PreviewBorder{5pt}"
519           putStrLn "\\begin{preview}"
520           putStrLn $ "\\begin{tikzpicture}[every on chain/.style={join=by ->},yscale=-1]"
521           tikz <- toTikZ example
522           putStrLn tikz
523           putStrLn "\\end{tikzpicture}"
524           putStrLn "\\end{preview}"
525           --putStrLn "\\pagebreak"
526           --putStrLn "\\begin{align*}"
527           --putStr   (toTikZ' example)
528           --putStrLn "\\end{align*}"
529           putStrLn "\\end{document}"
530
531 -- Random TikZ routines
532 textc x y text color = 
533     "\\node[anchor=center,color="++color++"] at ("++show (x*xscale)++"cm,"++show (y*yscale)++"cm) "++
534     "{{\\tt{"++text++"}}};\n"
535
536 drawBox x1 y1 x2 y2 color text =
537     "\\node[anchor=north west] at ("++show (x1*xscale)++"cm,"++show (y1*yscale)++"cm) "++
538     "{{\\tt{"++text++"}}};\n"
539     ++
540     "\\path[draw,color="++color++"]"++
541        " ("++show (x1*xscale)++","++show (y1*yscale)++") rectangle ("++
542            show (x2*xscale)++","++show (y2*yscale)++");\n"
543
544 drawLine x1 y1 x2 y2 color style =
545   "\\path[draw,color="++color++","++style++"] "++
546   "("++show (x1*xscale)++","++show (y1*yscale)++") -- " ++
547   "("++show (x2*xscale)++","++show (y2*yscale)++");\n"
548
549 drawLine' [] color style = ""
550 drawLine' (xy1:xy) color style =
551   "\\path[draw,color="++color++","++style++"] "++
552   foldl (\x y -> x ++ " -- " ++ y) (f xy1) (map f xy)
553   ++ ";\n"
554    where
555      f = (\(x,y) -> "("++show (x*xscale)++","++show (y*yscale)++")")
556
557 -- | x scaling factor for the entire diagram, since TikZ doesn't scale font sizes
558 xscale = 1
559
560 -- | y scaling factor for the entire diagram, since TikZ doesn't scale font sizes
561 yscale = 1
562
563 -- | extra gap placed between loopback wires and the contents of the loop module
564 loopgap = 1