GArrowTikZ: draw input wires before first box, output wires after last

[coq-hetmet.git] / examples / GArrowTikZ.hs

diff --git a/examples/GArrowTikZ.hs b/examples/GArrowTikZ.hs
index 9961830..7339397 100644 (file)
--- a/examples/GArrowTikZ.hs
+++ b/examples/GArrowTikZ.hs
@@ -81,8 +81,8 @@ data Diagram
   | DiagramBox       TrackIdentifier Tracks BoxRenderer Tracks TrackIdentifier
   | DiagramBypassTop Tracks Diagram
   | DiagramBypassBot        Diagram Tracks
   | DiagramBox       TrackIdentifier Tracks BoxRenderer Tracks TrackIdentifier
   | DiagramBypassTop Tracks Diagram
   | DiagramBypassBot        Diagram Tracks

-  -- | DiagramLoopTop   Tracks Diagram
-  -- | DiagramLoopBot          Diagram Tracks
+  | DiagramLoopTop   Tracks Diagram
+  | DiagramLoopBot          Diagram Tracks

 
 -- | get the output tracks of a diagram
 getOut :: Diagram -> Tracks
 
 -- | get the output tracks of a diagram
 getOut :: Diagram -> Tracks

@@ -90,6 +90,8 @@ getOut (DiagramComp f g)                     = getOut g
 getOut (DiagramBox ptop pin q pout pbot)     = pout
 getOut (DiagramBypassTop p f)                = TT p (getOut f)
 getOut (DiagramBypassBot f p)                = TT (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

+getOut (DiagramLoopTop t d)                  = case getOut d of { TT z y -> y ; _ -> error "mismatch" }
+getOut (DiagramLoopBot d t)                  = case getOut d of { TT y z -> y ; _ -> error "mismatch" }

 
 -- | get the input tracks of a diagram
 getIn :: Diagram -> Tracks
 
 -- | get the input tracks of a diagram
 getIn :: Diagram -> Tracks

@@ -97,6 +99,8 @@ getIn (DiagramComp f g)                      = getIn f
 getIn (DiagramBox ptop pin q pout pbot)      = pin
 getIn (DiagramBypassTop p f)                 = TT p (getIn f)
 getIn (DiagramBypassBot f p)                 = TT (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

+getIn (DiagramLoopTop t d)                   = case getIn d of { TT z x -> x ; _ -> error "mismatch" }
+getIn (DiagramLoopBot d t)                   = case getIn d of { TT x z -> x ; _ -> error "mismatch" }

 
 -- | 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
 
 -- | 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

@@ -167,7 +171,6 @@ alloc1 = do { (t,c) <- get
             ; return (T t)
             }
 
             ; 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
 mkdiag :: GArrowPortShape m () a b -> ConstraintM Diagram
 mkdiag (GASPortPassthrough  inp outp m) = error "not supported"
 mkdiag (GASPortShapeWrapper inp outp x) = mkdiag' x

@@ -184,22 +187,22 @@ mkdiag (GASPortShapeWrapper inp outp x) = mkdiag' 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" ++
  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"
+                                                      drawLine  x1 (tp!lowermost x)  ((x1+x2)/2) (tp!uppermost y) "gray!50" "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" ++
                              ; 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"
+                                                      drawLine  x1 (tp!uppermost y) ((x1+x2)/2) (tp!lowermost x) "gray!50" "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" ++
                              ; 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"
+                                                      drawLine  ((x1+x2)/2) (tp!uppermost y) x2 (tp!lowermost x) "gray!50" "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" ++
                              ; 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"
+                                                      drawLine  ((x1+x2)/2) (tp!lowermost x) x2 (tp!uppermost y) "gray!50" "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
                              ; 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

@@ -264,8 +267,10 @@ mkdiag (GASPortShapeWrapper inp outp x) = mkdiag' x
                     drawWires tp x1 z x2 z "black"
         ; return $ DiagramBox top (TT x (TT y z)) r (TT (TT x y) z) bot
         }
                     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_loopr  f) = do { (top,(TT _ x),bot) <- alloc inp; f' <- mkdiag' f ; constrainBot f' 1 (uppermost x)
+                             ; return $ DiagramLoopBot f' x  }
+ mkdiag' (GAS_loopl  f) = do { (top,(TT x _),bot) <- alloc inp; f' <- mkdiag' f ; constrainTop (lowermost x) 1 f'
+                             ; return $ DiagramLoopTop x f'  }

  mkdiag' (GAS_misc f )  = mkdiag f
 
  diagramBox :: TrackIdentifier -> Tracks -> BoxRenderer -> Tracks -> TrackIdentifier -> ConstraintM Diagram
  mkdiag' (GAS_misc f )  = mkdiag f
 
  diagramBox :: TrackIdentifier -> Tracks -> BoxRenderer -> Tracks -> TrackIdentifier -> ConstraintM Diagram

@@ -290,6 +295,8 @@ constrainTop v i (DiagramComp d1 d2)                  = do { constrainTop v i d1
 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 (DiagramBox ptop pin r pout pbot)    = constrain v LT ptop (-1 * i)
 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 (DiagramBox ptop pin r pout pbot)    = constrain v LT ptop (-1 * i)

+constrainTop v i (DiagramLoopTop p d)                 = constrain v LT (uppermost p) (-1 * i)
+constrainTop v i (DiagramLoopBot d p)                 = constrainTop v (i+1) d

 
 -- constrain that Ports is at least Int units below the bottommost portion of Diagram
 constrainBot :: Diagram -> Float -> TrackIdentifier -> ConstraintM ()
 
 -- constrain that Ports is at least Int units below the bottommost portion of Diagram
 constrainBot :: Diagram -> Float -> TrackIdentifier -> ConstraintM ()

@@ -297,6 +304,8 @@ constrainBot (DiagramComp d1 d2)                  i v = do { constrainBot d1 i v
 constrainBot (DiagramBypassTop p d)               i v = constrainBot d (i+1) v
 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
 constrainBot (DiagramBypassTop p d)               i v = constrainBot d (i+1) v
 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

+constrainBot (DiagramLoopTop p d)                 i v = constrainBot d (i+1) v
+constrainBot (DiagramLoopBot d p)                 i v = constrain v GT (lowermost p) 2

 
 -- | The width of a box is easy to calculate
 width :: Diagram -> Float
 
 -- | The width of a box is easy to calculate
 width :: Diagram -> Float

@@ -304,11 +313,13 @@ 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
 width (DiagramBox ptop pin x pout pbot) = 2
 width (DiagramBypassTop p d)            = (width d) + 2
 width (DiagramBypassBot d p)            = (width d) + 2

+width (DiagramLoopTop p d)              = (width d) + 2
+width (DiagramLoopBot 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 :: 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 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') "gray!50" "dashed"

 drawWires tp _ _ _ _ _                       = error "drawwires fail"
 
 tikZ :: TrackPositions ->
 drawWires tp _ _ _ _ _                       = error "drawwires fail"
 
 tikZ :: TrackPositions ->

@@ -323,14 +334,28 @@ tikZ m = tikZ'
                                       ++ tikZ' d2 (x + width d1 + 1)
   tikZ' d'@(DiagramBypassTop p d) x = let top = getTop d' in
                                       let bot = getBot d' in
                                       ++ 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"
+                                      drawBox  x top (x+width m d') bot "gray!50" "second"

                                       ++ drawWires m x (getIn d) (x+1) (getIn d) "black"
                                       ++ tikZ' d (x+1)
                                       ++ 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
                                       ++ drawWires m x (getIn d) (x+1) (getIn d) "black"
                                       ++ tikZ' d (x+1)
                                       ++ 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"
+                                      drawBox  x top (x+width m d') bot "gray!50" "first"
+                                      ++ drawWires m x (getIn d) (x+1) (getIn d) "black"
+                                      ++ tikZ' d (x+1)
+                                      ++ 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'@(DiagramLoopTop p d) x   = let top = getTop d' in
+                                      let bot = getBot d' in
+                                      drawBox  x top (x+width d') bot "gray!50" "loopl"
+                                      ++ drawWires m x (getIn d) (x+1) (getIn d) "black"
+                                      ++ tikZ' d (x+1)
+                                      ++ 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'@(DiagramLoopBot d p) x   = let top = getTop d' in
+                                      let bot = getBot d' in
+                                      drawBox  x top (x+width d') bot "gray!50" "loopr"

                                       ++ drawWires m x (getIn d) (x+1) (getIn d) "black"
                                       ++ tikZ' d (x+1)
                                       ++ drawWires m (x+1+width d) (getOut d) (x+1+width d+1) (getOut d) "black"
                                       ++ drawWires m x (getIn d) (x+1) (getIn d) "black"
                                       ++ tikZ' d (x+1)
                                       ++ drawWires m (x+1+width d) (getOut d) (x+1+width d+1) (getOut d) "black"

@@ -342,19 +367,23 @@ tikZ m = tikZ'
   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' :: 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"
+  wires' x1 (TU v)   x2 color st = drawLine x1 (m ! v) x2 (m ! v) "gray!50" "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
 
   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

+  getTop (DiagramLoopTop p d)       = (m ! uppermost p) - 1
+  getTop (DiagramLoopBot 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
 
   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

+  getBot (DiagramLoopTop p d)       = getBot d + 1
+  getBot (DiagramLoopBot 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)
 
 -- allocates multiple tracks, adding constraints that they are at least one unit apart
 alloc :: PortShape a -> ConstraintM (TrackIdentifier,Tracks,TrackIdentifier)

@@ -412,17 +441,21 @@ toTikZ g =
                 }
      in do { let (_,constraints) = execState cm (0,[])
            ; lps <- do_lp_solve $ constraints
                 }
      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
+           ; let m = lp_solve_to_trackpos lps
+           ; let d = evalState cm (0,[])
+           ; let t = tikZ m d 1
+           ; return (t ++ drawWires m 0             (getIn  d) 1             (getIn  d) "black"
+                       ++ drawWires m (width m d+1) (getOut d) (width m d+2) (getOut d) "black")

            }
            }

-
-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 ::
+    (forall g .
+             (Int -> PGArrow g (GArrowUnit g) Int) ->
+             (forall b . PGArrow g (GArrowTensor g b b) b) ->
+             PGArrow g b c)
+     -> IO ()
+tikz x = tikz' $ optimize $ unG (x (\c -> PGArrowD { unG = GAS_const c }) (PGArrowD { unG = GAS_merge }))

 
 tikz' example
      = do putStrLn "\\documentclass{article}"
 
 tikz' example
      = do putStrLn "\\documentclass{article}"