X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=examples%2FGArrowTikZ.hs;h=7339397dfe26064f1218972a6e66253e1adfca8f;hp=9961830274f6dfa4eca1fa2d362188de55cc8304;hb=8a6325a074907bd0b7aa735eac63d1202da7d5b7;hpb=856ef91d5132ac813631f01420a8291a92bce1ad diff --git a/examples/GArrowTikZ.hs b/examples/GArrowTikZ.hs index 9961830..7339397 100644 --- 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 - -- | DiagramLoopTop Tracks Diagram - -- | DiagramLoopBot Diagram Tracks + | DiagramLoopTop Tracks Diagram + | DiagramLoopBot 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 (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 @@ -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 (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 @@ -167,7 +171,6 @@ alloc1 = do { (t,c) <- get ; 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 @@ -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" ++ - 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" ++ - 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" ++ - 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" ++ - 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 @@ -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 } - 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 @@ -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 (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 () @@ -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 (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 @@ -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 (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 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 -> @@ -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 - 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 - 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" @@ -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' 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 (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 (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) @@ -412,17 +441,21 @@ toTikZ 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 + ; 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}"