1 {-# OPTIONS_GHC -XModalTypes -XMultiParamTypeClasses -XNoMonoPatBinds -XKindSignatures -XGADTs -XFlexibleContexts -XFlexibleInstances -XTypeOperators -XUndecidableInstances #-}
2 module GArrowTikZ (tikz, GArrowTikZ(..))
4 import Prelude hiding ( id, (.), lookup )
5 import Control.Category
6 import GHC.HetMet.GArrow
7 import Data.List hiding (lookup, insert)
8 import Data.Map hiding (map, (!))
14 - have "resolve" turn a (Diagram UnifVal) into (Diagram Int)
16 - bias right now is for all edges to be uppermost; try for bias
17 towards smallest nodes?
18 - curvy boxes (like XOR gates)
22 -- a unification value is basically a LISP-ish expression
27 instance Unifiable UVal where
28 unify' (UVVal vl1) (UVVal vl2)
29 | length vl1 /= length vl2 = error "length mismatch during unification"
30 | otherwise = foldr mergeU emptyUnifier (map (\(x,y) -> unify x y) $ zip vl1 vl2)
31 unify' _ _ = error "impossible"
33 project (UVVar v) = Just v
35 occurrences (UVVar v) = [v]
36 occurrences (UVVal vl) = concatMap occurrences vl
38 -- | Resolves a unification variable; the answer to this query will change if subsequent unifications are performed
39 getU' :: Unifier UVal -> UVal -> UVal
40 getU' u (UVVal vl) = UVVal $ map (getU' u) vl
41 getU' u x@(UVVar v) = case Unify.getU u v of
49 -- | Render a fully-polymorphic GArrow term as a boxes-and-wires diagram using TikZ
52 type Constraints = [(UVal, Int, UVal)]
54 -- the unification monad
55 data UyM t a = UyM (([UVar],Unifier UVal,Constraints) -> ([UVar],Unifier UVal,Constraints,a))
56 instance Monad (UyM t)
58 return x = UyM $ \(i,u,k) -> (i,u,k,x)
59 (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')
62 getU = UyM $ \(i,u,k) -> (i,u,k,u)
63 getM v = UyM $ \(i,u,k) -> (i,u,k,getU' u v)
64 occursU v x = UyM $ \(i,u,k) -> (i,u,k,occurs u v x)
65 unifyM :: Eq t => UVal -> UVal -> UyM t ()
66 unifyM v1 v2 = UyM $ \(i,u,k) -> (i,mergeU u (unify v1 v2),k,())
68 freshU = UyM $ \(i:is,u,k) -> (is,u,k,i)
69 constrain :: UVal -> Int -> UVal -> UyM t ()
70 constrain v1 d v2 = UyM $ \(i,u,k) -> (i,u,((v1,d,v2):k),())
71 getK :: UyM t [(UVal, Int, UVal)]
72 getK = UyM $ \(i,u,k) -> (i,u,k,k)
73 runU :: UyM t a -> ([UVar],Unifier UVal,Constraints,a)
74 runU (UyM f) = (f (uvarSupply,emptyUnifier,[]))
76 data GArrowTikZ :: * -> * -> *
78 TikZ_const :: Int -> GArrowTikZ () Int
79 TikZ_id :: GArrowTikZ x x
80 TikZ_comp :: GArrowTikZ y z -> GArrowTikZ x y -> GArrowTikZ x z
81 TikZ_first :: GArrowTikZ x y -> GArrowTikZ (x**z) (y**z)
82 TikZ_second :: GArrowTikZ x y -> GArrowTikZ (z**x) (z**y)
83 TikZ_cancell :: GArrowTikZ (()**x) x
84 TikZ_cancelr :: GArrowTikZ (x**()) x
85 TikZ_uncancell :: GArrowTikZ x (()**x)
86 TikZ_uncancelr :: GArrowTikZ x (x**())
87 TikZ_assoc :: GArrowTikZ ((x**y)**z) (x**(y**z))
88 TikZ_unassoc :: GArrowTikZ (x**(y**z)) ((x**y)**z)
89 TikZ_drop :: GArrowTikZ x ()
90 TikZ_copy :: GArrowTikZ x (x**x)
91 TikZ_swap :: GArrowTikZ (x**y) (y**x)
92 TikZ_merge :: GArrowTikZ (x**y) z
93 TikZ_loopl :: GArrowTikZ (x**z) (y**z) -> GArrowTikZ x y
94 TikZ_loopr :: GArrowTikZ (z**x) (z**y) -> GArrowTikZ x y
97 -- Technically this instance violates the laws (and RULEs) for
98 -- Control.Category; the compiler might choose to optimize (f >>> id)
99 -- into f, and this optimization would produce a change in behavior
100 -- below. In practice this means that the user must be prepared for
101 -- the rendered TikZ diagram to be merely *equivalent to* his/her
102 -- term, rather than structurally exactly equal to it.
104 instance Category GArrowTikZ where
108 instance GArrow GArrowTikZ (**) () where
109 ga_first = TikZ_first
110 ga_second = TikZ_second
111 ga_cancell = TikZ_cancell
112 ga_cancelr = TikZ_cancelr
113 ga_uncancell = TikZ_uncancell
114 ga_uncancelr = TikZ_uncancelr
115 ga_assoc = TikZ_assoc
116 ga_unassoc = TikZ_unassoc
118 instance GArrowDrop GArrowTikZ (**) () where
121 instance GArrowCopy GArrowTikZ (**) () where
124 instance GArrowSwap GArrowTikZ (**) () where
127 instance GArrowLoop GArrowTikZ (**) () where
128 ga_loopl = TikZ_loopl
129 ga_loopr = TikZ_loopr
131 instance GArrowSTKC GArrowTikZ (,) ()
134 name :: GArrowTikZ a b -> String
136 name (TikZ_const i) = "const " ++ show i
137 name (TikZ_comp _ _) = "comp"
138 name (TikZ_first _ ) = "first"
139 name (TikZ_second _ ) = "second"
140 name TikZ_cancell = "cancell"
141 name TikZ_cancelr = "cancelr"
142 name TikZ_uncancell = "uncancell"
143 name TikZ_uncancelr = "uncancelr"
144 name TikZ_drop = "drop"
145 name TikZ_copy = "copy"
146 name TikZ_swap = "swap"
147 name (TikZ_loopl _ ) = "loopl"
148 name (TikZ_loopr _ ) = "loopr"
149 name TikZ_assoc = "assoc"
150 name TikZ_unassoc = "unassoc"
152 fresh1 :: UyM () Ports
153 fresh1 = do { x <- freshU
157 fresh2 :: UyM () (Ports,Ports)
158 fresh2 = do { x <- freshU
160 ; constrain (UVVar x) 1 (UVVar y)
161 ; return $ (UVVar x,UVVar y)
164 fresh3 :: UyM () (Ports,Ports,Ports)
165 fresh3 = do { x <- freshU
168 ; constrain (UVVar x) 1 (UVVar y)
169 ; constrain (UVVar y) 1 (UVVar z)
170 ; return $ (UVVar x,UVVar y,UVVar z)
173 fresh4 :: UyM () (Ports,Ports,Ports,Ports)
174 fresh4 = do { x1 <- freshU
178 ; constrain (UVVar x1) 1 (UVVar x2)
179 ; constrain (UVVar x2) 1 (UVVar x3)
180 ; constrain (UVVar x3) 1 (UVVar x4)
181 ; return $ (UVVar x1,UVVar x2,UVVar x3,UVVar x4)
184 fresh5 :: UyM () (Ports,Ports,Ports,Ports,Ports)
185 fresh5 = do { x1 <- freshU
190 ; constrain (UVVar x1) 1 (UVVar x2)
191 ; constrain (UVVar x2) 1 (UVVar x3)
192 ; constrain (UVVar x3) 1 (UVVar x4)
193 ; constrain (UVVar x4) 1 (UVVar x5)
194 ; return $ (UVVar x1,UVVar x2,UVVar x3,UVVar x4,UVVar x5)
200 --example = ga_first ga_drop >>> ga_cancell >>> ga_first id >>> ga_swap >>> ga_first id >>> TikZ_merge
201 --example :: forall x y z. forall g. (GArrow g (,) (), GArrowCopy g (,) (), GArrowSwap g (,) ()) => g x ((x,x),x)
202 --example = ga_copy >>> ga_second ga_copy >>> ga_second (ga_first id) >>> ga_unassoc >>> ga_first ga_swap
203 --example = ga_copy >>> ga_second ga_copy >>> ga_second (ga_second id) >>> ga_unassoc >>> ga_first id >>> ga_first ga_swap
204 --example :: forall x. forall g. (GArrow g (,) (), GArrowCopy g (,) (), GArrowSwap g (,) ()) => g x x
205 --example = id >>> id
207 data Diagram p = DiagramComp (Diagram p) (Diagram p)
208 | DiagramPrim String p p p p (String -> Int -> Int -> Int -> p -> p -> Int -> String)
209 | DiagramBypassTop p (Diagram p)
210 | DiagramBypassBot (Diagram p) p
211 -- | DiagramLoopTop Diagram
212 -- | DiagramLoopBot Diagram
216 getOut :: Diagram Ports -> Ports
217 getOut (DiagramComp f g) = getOut g
218 getOut (DiagramPrim s ptop pin pout pbot _) = pout
219 getOut (DiagramBypassTop p f) = UVVal [p, (getOut f)]
220 getOut (DiagramBypassBot f p) = UVVal [(getOut f), p]
222 getIn :: Diagram Ports -> Ports
223 getIn (DiagramComp f g) = getIn f
224 getIn (DiagramPrim s ptop pin pout pbot _) = pin
225 getIn (DiagramBypassTop p f) = UVVal [p, (getIn f)]
226 getIn (DiagramBypassBot f p) = UVVal [(getIn f), p]
228 -- constrain that Ports is at least Int units above the topmost portion of Diagram
229 constrainTop :: Ports -> Int -> Diagram Ports -> UyM () ()
230 constrainTop v i (DiagramComp d1 d2) = do { constrainTop v i d1 ; constrainTop v i d2 ; return () }
231 constrainTop v i (DiagramBypassTop p d) = constrain v 2 p
232 constrainTop v i (DiagramBypassBot d p) = constrainTop v (i+1) d
233 constrainTop v i (DiagramPrim s ptop pin pout pbot _) = constrain v i ptop
235 -- constrain that Ports is at least Int units below the bottommost portion of Diagram
236 constrainBot :: Diagram Ports -> Int -> Ports -> UyM () ()
237 constrainBot (DiagramComp d1 d2) i v = do { constrainBot d1 i v ; constrainBot d2 i v ; return () }
238 constrainBot (DiagramBypassTop p d) i v = constrainBot d (i+1) v
239 constrainBot (DiagramBypassBot d p) i v = constrain p 2 v
240 constrainBot (DiagramPrim s ptop pin pout pbot _) i v = constrain pbot i v
242 ga2diag :: GArrowTikZ a b -> UyM () (Diagram Ports)
243 ga2diag (TikZ_id ) = do { (top,x,bot) <- fresh3 ; return $ DiagramPrim "id" top x x bot defren }
244 ga2diag (TikZ_comp g f) = do { f' <- ga2diag f
246 ; unifyM (getOut f') (getIn g')
247 ; return $ DiagramComp f' g' }
248 ga2diag (TikZ_first f) = do { x <- fresh1; f' <- ga2diag f ; constrainBot f' 1 x ; return $ DiagramBypassBot f' x }
249 ga2diag (TikZ_second f) = do { x <- fresh1; f' <- ga2diag f ; constrainTop x 1 f' ; return $ DiagramBypassTop x f' }
250 ga2diag TikZ_cancell = do { (top,x,y ,bot) <- fresh4 ; return $ DiagramPrim "cancell" top (UVVal [x,y]) y bot defren }
251 ga2diag TikZ_cancelr = do { (top,x,y ,bot) <- fresh4 ; return $ DiagramPrim "cancelr" top (UVVal [x,y]) x bot defren }
252 ga2diag TikZ_uncancell = do { (top,x,y ,bot) <- fresh4 ; return $ DiagramPrim "uncancell" top y (UVVal [x,y]) bot defren }
253 ga2diag TikZ_uncancelr = do { (top,x,y ,bot) <- fresh4 ; return $ DiagramPrim "uncancelr" top x (UVVal [x,y]) bot defren }
254 ga2diag TikZ_drop = do { (top,x ,bot) <- fresh3 ; return $ DiagramPrim "drop" top x x bot defren }
255 ga2diag (TikZ_const i) = do { (top,x ,bot) <- fresh3 ; return $ DiagramPrim ("const " ++ show i) top x x bot defren }
256 ga2diag TikZ_copy = do { (top,x,y,z,bot) <- fresh5
257 ; return $ DiagramPrim "copy" top y (UVVal [x,z]) bot defren }
258 ga2diag TikZ_merge = do { (top,x,y,z,bot) <- fresh5
259 ; return $ DiagramPrim "merge" top (UVVal [x,z]) y bot defren }
260 ga2diag TikZ_swap = do { (top,x,y ,bot) <- fresh4
261 ; return $ DiagramPrim "swap" top (UVVal [x,y]) (UVVal [x,y]) bot defren }
262 ga2diag TikZ_assoc = do { (top,x,y,z,bot) <- fresh5
263 ; return $ DiagramPrim "assoc" top (UVVal [UVVal [x,y],z])(UVVal [x,UVVal [y,z]]) bot defren }
264 ga2diag TikZ_unassoc = do { (top,x,y,z,bot) <- fresh5
265 ; return $ DiagramPrim "unassoc" top (UVVal [x,UVVal [y,z]])(UVVal [UVVal [x,y],z]) bot defren }
266 ga2diag (TikZ_loopl f) = error "not implemented"
267 ga2diag (TikZ_loopr f) = error "not implemented"
269 defren :: String -> Int -> Int -> Int -> Ports -> Ports -> Int -> String
270 defren s x w top p1 p2 bot
271 = drawBox x top (x+w) bot "black" s
272 -- ++ wires (x-1) p1 x "green"
273 -- ++ wires (x+w) p2 (x+w+1) "red"
278 textc x y text color =
279 "\\node[anchor=center,color="++color++"] at ("++show (x*xscale)++"cm,"++show (y*yscale)++"cm) "++
280 "{{\\tt{"++text++"}}};\n"
282 drawBox x1 y1 x2 y2 color text =
283 "\\node[anchor=north west] at ("++show (x1*xscale)++"cm,"++show (y1*yscale)++"cm) "++
284 "{{\\tt{"++text++"}}};\n"
286 "\\path[draw,color="++color++"]"++
287 " ("++show (x1*xscale)++","++show (y1*yscale)++") rectangle ("++
288 show (x2*xscale)++","++show (y2*yscale)++");\n"
290 drawLine x1 y1 x2 y2 color style =
291 "\\path[draw,color="++color++","++style++"] "++
292 "("++show (x1*xscale)++","++show (y1*yscale)++") -- " ++
293 "("++show (x2*xscale)++","++show (y2*yscale)++");\n"
295 width :: Diagram Ports -> Int
296 width (DiagramComp d1 d2) = (width d1) + 1 + (width d2)
297 width (DiagramPrim s _ p1 p2 _ _) = 2
298 width (DiagramBypassTop p d) = (width d) + 2
299 width (DiagramBypassBot d p) = (width d) + 2
301 (!) :: Map UVar Int -> UVar -> Int
302 m ! x = case lookup x m of
306 tikZ :: Map UVar Int ->
308 Int -> -- horizontal position
312 tikZ' d@(DiagramComp d1 d2) x = tikZ' d1 x
313 ++ wires (x+width d1) (getOut d1) (x+width d1+1) "black"
314 ++ tikZ' d2 (x + width d1 + 1)
315 tikZ' d'@(DiagramBypassTop p d) x = let top = getTop d' in
316 let bot = getBot d' in
317 drawBox x top (x+width d') bot "gray!50" "second"
318 ++ drawLine x (top+1) (x+width d') (top+1) "black" "->"
319 ++ wires x (getIn d) (x+1) "black"
321 ++ wires (x+1+width d) (getOut d) (x+1+width d+1) "black"
322 tikZ' d'@(DiagramBypassBot d p) x = let top = getTop d' in
323 let bot = getBot d' in
324 drawBox x top (x+width d') bot "gray!50" "first"
325 ++ drawLine x (bot-1) (x+width d') (bot-1) "black" "->"
326 ++ wires x (getIn d) (x+1) "black"
328 ++ wires (x+1+width d) (getOut d) (x+1+width d+1) "black"
329 tikZ' d@(DiagramPrim s (UVVar top) p1 p2 (UVVar bot) r) x = r s x (width d) (m ! top) p1 p2 (m ! bot)
331 wires :: Int -> Ports -> Int -> String -> String
332 wires x1 (UVVar v) x2 color = drawLine x1 (m ! v) x2 (m ! v) color "->"
333 -- ++ textc ((x1+x2) `div` 2) (m!v) (show v) "purple"
334 wires x1 (UVVal vl) x2 color = foldr (\x y -> x ++ " " ++ y) [] (map (\v -> wires x1 v x2 color) vl)
336 getTop :: Diagram Ports -> Int
337 getTop (DiagramComp d1 d2) = min (getTop d1) (getTop d2)
338 getTop (DiagramBypassTop p d) = (m ! getleft p) - 1
339 getTop (DiagramBypassBot d p) = getTop d - 1
340 getTop (DiagramPrim s (UVVar ptop) _ _ _ _) = m ! ptop
342 getBot :: Diagram Ports -> Int
343 getBot (DiagramComp d1 d2) = max (getBot d1) (getBot d2)
344 getBot (DiagramBypassTop p d) = getBot d + 1
345 getBot (DiagramBypassBot d p) = (m ! getright p) + 1
346 getBot (DiagramPrim s _ _ _ (UVVar pbot) _) = m ! pbot
348 resolve' (DiagramComp d1 d2) = do { d1' <- resolve' d1 ; d2' <- resolve' d2 ; return $ DiagramComp d1' d2' }
349 resolve' (DiagramBypassTop p d) = do { p' <- getM p ; d' <- resolve' d ; return $ DiagramBypassTop p' d' }
350 resolve' (DiagramBypassBot d p) = do { p' <- getM p ; d' <- resolve' d ; return $ DiagramBypassBot d' p' }
351 resolve' (DiagramPrim s ptop pin pout pbot r)
352 = do { ptop' <- getM ptop
356 ; return $ DiagramPrim s ptop' pin' pout' pbot' r }
358 getleft (UVVar v) = v
359 getleft (UVVal vl) = getleft (head vl)
361 getright (UVVar v) = v
362 getright (UVVal vl) = getright (last vl)
364 strip :: [(Ports,Int,Ports)] -> [(UVar,Int,UVar)]
365 strip = map (\(v1,x,v2) -> (getright v1, x, getleft v2))
368 -- must use bubblesort because the ordering isn't transitive
369 sortit :: [(UVar,Int,UVar)] -> [(UVar,Int,UVar)]
370 sortit x = stupidSort x []
373 stupidSort (h:t) x = stupidSort t (stupidInsert h x)
375 stupidInsert t [] = [t]
376 stupidInsert t@(_,_,t') ((a@(_,_,a')):b) = if cmp' x t' a' == LT
378 else a:(stupidInsert t b)
380 cmp' :: [(UVar,Int,UVar)] -> UVar -> UVar -> Ordering
381 cmp' [] a b = EQ -- compare a b
382 cmp' ((v1,_,v2):r) a b = if a == v1 && b==v2
384 else if a == v2 && b==v1
388 lookup'' :: Map UVar Int -> UVar -> Int
389 lookup'' m x = case lookup x m of
393 valuatit :: Map UVar Int -> [(UVar,Int,UVar)] -> Map UVar Int
395 valuatit m ((v1,k,v2):r) = valuatit m' r
398 v2' = max (lookup'' m v2) (k+(lookup'' m v1))
400 resolve'k :: UyM () [(Ports,Int,Ports)]
401 resolve'k = do { k <- getK
402 ; k' <- mapM (\(v1,x,v2) -> do { v1' <- getM v1 ; v2' <- getM v2 ; return (v1',x,v2') }) k
406 toTikZ :: GArrowTikZ a b -> String
407 toTikZ g = tikZ m d 0
409 (_,_,_,(d,k)) = runU $ do { d <- ga2diag g
415 toTikZ' :: GArrowTikZ a b -> String
416 toTikZ' g = foldr (\x y -> x++"\\\\\n"++y) [] (map foo s)
418 (_,_,_,k) = runU $ ga2diag g >>= resolve' >>= \_ -> resolve'k
419 foo (v1,v,v2) = "x_{"++show v1++"} + "++show v++" \\leq x_{"++show v2++"} = " ++ (show $ lookup'' m v2)
424 = do putStrLn "\\documentclass{article}"
425 putStrLn "\\usepackage[landscape,paperheight=20in,textwidth=19in]{geometry}"
426 putStrLn "\\usepackage{tikz}"
427 putStrLn "\\usepackage{amsmath}"
428 putStrLn "\\begin{document}"
429 putStrLn $ "\\begin{tikzpicture}[every on chain/.style={join=by ->},yscale=-1]"
430 putStrLn (toTikZ example)
431 putStrLn "\\end{tikzpicture}"
432 -- putStrLn "\\begin{align*}"
433 -- putStr (toTikZ' example)
434 -- putStrLn "\\end{align*}"
435 putStrLn "\\end{document}"