X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=examples%2FGArrowTikZ.hs;h=1b15fab89aaf0b59fc7b8247cd4be13d60563459;hp=b090c859986e90902279debc02ff3a3ae0bcd7a5;hb=c700f5a65d664d4c0a3e76d33aa3769266bf330c;hpb=5632630c3828941a4c3b3d4f5706261d775dfe1a diff --git a/examples/GArrowTikZ.hs b/examples/GArrowTikZ.hs index b090c85..1b15fab 100644 --- a/examples/GArrowTikZ.hs +++ b/examples/GArrowTikZ.hs @@ -12,13 +12,13 @@ -- You must have lp_solve installed in order for this to work. -- -module GArrowTikZ (tikz) +module GArrowTikZ (tikz,Opaque(..),toTikZ,tikz_header,tikz_footer,skelify',skelify'') where import System.Process import Prelude hiding ( id, (.), lookup ) import Control.Category import Control.Monad.State -import GHC.HetMet.GArrow +import Control.GArrow import Data.List hiding (lookup, insert) import Data.Map hiding (map, (!)) import Data.Maybe (catMaybes) @@ -27,6 +27,13 @@ import GArrowSkeleton import GArrowPortShape import GHC.HetMet.Private +skelify' :: (forall g . (GArrowCopy g (,) (), GArrowDrop g (,) (), GArrowSwap g (,) (), GArrowLoop g (,) ()) => g x y) -> + GArrowSkeleton Opaque x y +skelify' = \g -> g + +skelify'' :: GArrowSkeleton Opaque x y -> GArrowSkeleton Opaque x y +skelify'' = \g -> g + ------------------------------------------------------------------------------ -- Tracks @@ -70,6 +77,28 @@ lowermost (TU x) = x lowermost (TT x y) = lowermost y +class ToDiagram g where + toDiagram :: GArrowPortShape g () x y -> ConstraintM Diagram + +instance (Detect m, ToDiagram m) => ToDiagram (GArrowSkeleton m) where + toDiagram s = mkdiag s + +data Opaque x y where + MkOpaque :: String -> DetectM (GArrowPortShape Opaque UVar x y) -> Opaque x y + +instance Detect Opaque where + detect' (MkOpaque _ dm) = dm + +instance ToDiagram Opaque where + toDiagram (GASPortPassthrough inp outp (MkOpaque s _)) = + do { (top, x ,bot) <- alloc inp + ; (_, y ,_) <- alloc outp + --; constrainEq x y + ; simpleDiag'' s top x y bot [] "black" } + toDiagram q = mkdiag q + +-- do (top, x ,bot) <- alloc inp +-- simpleDiag' s top x x bot [(x,x)] "gray!50" ------------------------------------------------------------------------------ @@ -171,11 +200,11 @@ alloc1 = do { (t,c) <- get ; return (T t) } -mkdiag :: GArrowPortShape m () a b -> ConstraintM Diagram -mkdiag (GASPortPassthrough inp outp m) = error "not supported" +mkdiag :: ToDiagram m => GArrowPortShape m () a b -> ConstraintM Diagram +mkdiag (GASPortPassthrough inp outp m) = toDiagram (GASPortPassthrough inp outp m) mkdiag (GASPortShapeWrapper inp outp x) = mkdiag' x where - mkdiag' :: GArrowSkeleton (GArrowPortShape m ()) a b -> ConstraintM Diagram + mkdiag' :: ToDiagram m => 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' } @@ -188,30 +217,26 @@ mkdiag (GASPortShapeWrapper inp outp x) = mkdiag' x ; 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) "gray!50" "dashed" - ; return $ DiagramBox 2 top (TT x y) r y bot } + ; return $ DiagramBox 2.4 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) "gray!50" "dashed" - ; return $ DiagramBox 2 top (TT x y) r x bot } + ; return $ DiagramBox 2.4 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) "gray!50" "dashed" - ; return $ DiagramBox 2 top y r (TT x y) bot } + ; return $ DiagramBox 2.8 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) "gray!50" "dashed" - ; return $ DiagramBox 2 top x r (TT x y) bot } + ; return $ DiagramBox 2.8 top x r (TT x y) bot } mkdiag' GAS_drop = do { (top, x ,bot) <- alloc inp ; (_, y ,_) <- alloc outp ; constrainEq x y ; simpleDiag "drop" top x y 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) @@ -219,10 +244,8 @@ mkdiag (GASPortShapeWrapper inp outp x) = mkdiag' x 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 2 top x r (TT y z) bot + ; return $ DiagramBox defaultWidth 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')) @@ -249,7 +272,7 @@ mkdiag (GASPortShapeWrapper inp outp x) = mkdiag' x drawWires tp x1 z x2 z "black" ; let pin = (TT (TT x y) z) ; let pout = (TT x (TT y z)) - ; return $ if draw_assoc then DiagramBox 2 top pin r pout bot else DiagramBox 0 top pin noRender pout bot + ; return $ if draw_assoc then DiagramBox defaultWidth top pin r pout bot else DiagramBox 0 top pin noRender pout bot } mkdiag' GAS_unassoc = do { (top,(TT x (TT y z)),bot) <- alloc inp @@ -272,7 +295,7 @@ mkdiag (GASPortShapeWrapper inp outp x) = mkdiag' x drawWires tp x1 z x2 z "black" ; let pin = (TT x (TT y z)) ; let pout = (TT (TT x y) z) - ; return $ if draw_assoc then DiagramBox 2 top pin r pout bot else DiagramBox 0 top pin noRender pout bot + ; return $ if draw_assoc then DiagramBox defaultWidth top pin r pout bot else DiagramBox 0 top pin noRender pout bot } mkdiag' (GAS_loopl f) = do { f' <- mkdiag' f ; l <- allocLoop (case (getIn f') of (TT z _) -> z ; _ -> error "GAS_loopl: mismatch") @@ -284,26 +307,34 @@ mkdiag (GASPortShapeWrapper inp outp x) = mkdiag' x ; return $ DiagramLoopBot f' l } 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) +defaultWidth = 2 + +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 2 ptop pin r pout pbot + ; return $ DiagramBox defaultWidth 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 +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" +simpleDiag'' text ptop pin pout pbot conn color = diagramBox ptop pin defren pout pbot + where + defren tp x1 y1 x2 y2 = drawBoxC 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" ---draw_assoc = False ---draw_first_second = False -draw_assoc = True -draw_first_second = True +draw_assoc = False +draw_first_second = False +--draw_assoc = True +--draw_first_second = True -- constrain that Ports is at least Int units above the topmost portion of Diagram constrainTop :: TrackIdentifier -> Float -> Diagram -> ConstraintM () @@ -460,7 +491,7 @@ allocLoop (TT t1 t2) = do { x1 <- allocLoop t2 do_lp_solve :: [Constraint] -> IO String do_lp_solve c = do { let stdin = "min: x1;\n" ++ (foldl (++) "" (map show c)) ++ "\n" - ; putStrLn stdin +-- ; putStrLn stdin ; stdout <- readProcess "lp_solve" [] stdin ; return stdout } @@ -487,7 +518,8 @@ lp_solve_to_trackpos s = toTrackPos $ map parse $ catMaybes $ map grab $ lines s 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 :: (ToDiagram m, Detect m) => GArrowSkeleton m a b -> IO String toTikZ g = let cm = do { let g' = detectShape g ; g'' <- mkdiag g' @@ -501,35 +533,28 @@ toTikZ g = ; 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 c . - (forall g . - (Int -> PGArrow g (GArrowUnit g) Int) -> - (PGArrow g (GArrowTensor g c c) c) -> - PGArrow g c c) - -> IO () -tikz x = tikz' $ beautify $ optimize $ unG (x (\c -> PGArrowD { unG = GAS_const c }) (PGArrowD { unG = GAS_merge })) - -tikz' example - = do putStrLn "\\documentclass{article}" - 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]" - tikz <- toTikZ example - putStrLn tikz - putStrLn "\\end{tikzpicture}" - putStrLn "\\end{preview}" - --putStrLn "\\pagebreak" - --putStrLn "\\begin{align*}" - --putStr (toTikZ' example) - --putStrLn "\\end{align*}" - putStrLn "\\end{document}" + +tikz_header = + "\\documentclass{article}\n" ++ + "\\usepackage[paperwidth=\\maxdimen,paperheight=\\maxdimen]{geometry}\n" ++ + "\\usepackage{tikz}\n" ++ + "\\usepackage{amsmath}\n" ++ + "\\usepackage[tightpage,active]{preview}\n" ++ + "\\begin{document}\n" ++ + "\\setlength\\PreviewBorder{5pt}\n" ++ + "\\begin{preview}\n" ++ + "\\begin{tikzpicture}[every on chain/.style={join=by ->},yscale=-1]\n" + +tikz_footer = + "\\end{tikzpicture}\n" ++ + "\\end{preview}\n" ++ + "\\end{document}\n" + +tikz example = + do putStrLn tikz_header + tikz <- toTikZ example + putStrLn tikz + putStrLn tikz_footer -- Random TikZ routines textc x y text color = @@ -544,6 +569,14 @@ drawBox x1 y1 x2 y2 color text = " ("++show (x1*xscale)++","++show (y1*yscale)++") rectangle ("++ show (x2*xscale)++","++show (y2*yscale)++");\n" +drawBoxC x1 y1 x2 y2 color text = + "\\node[anchor=center] at ("++show ((x1+x2)*xscale/2)++"cm,"++show ((y1+y2)*yscale/2)++"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)++") -- " ++