From: Adam Megacz Date: Thu, 2 Jun 2011 02:15:25 +0000 (-0700) Subject: very rudimentary support for feedback in GArrowTikZ X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=bc93ead06902db52dfcc229084a42152d4166bdf;hp=3282a2b78028238987a5a49e59d8e8d495aea0e1 very rudimentary support for feedback in GArrowTikZ --- diff --git a/examples/Demo.hs b/examples/Demo.hs index 6d0e69d..74fe4de 100644 --- a/examples/Demo.hs +++ b/examples/Demo.hs @@ -5,11 +5,17 @@ module Demo (demo) where --demo con mer = <[ ~~mer ~~(con (2::Int)) ~~(con (12::Int)) ]> demo const mult = - <[ let twelve = ~~(const (12::Int)) - four = ~~(const ( 4::Int)) - in ~~mult four (~~mult four twelve) + <[ let four = ~~mult four ~~(const 4) +-- twelve = {- {- ~~mult four -} ~~(const 12) -} four + in four ]> +demo :: + forall a c . + (Int -> <[a]>@c) -> + <[a -> a -> a]>@c -> + <[a]>@c + {- demo const mult = <[ let twelve = ~~(const (12::Int)) diff --git a/examples/DemoMain.hs b/examples/DemoMain.hs index cc438ba..e3e56b7 100644 --- a/examples/DemoMain.hs +++ b/examples/DemoMain.hs @@ -1,5 +1,15 @@ import Control.Category import GArrowTikZ +import GHC.HetMet.Private +import GHC.HetMet.GArrow import Demo +{- +demo' :: + (Int -> PGArrow g (GArrowUnit g) (GArrowTensor g (GArrowUnit g) Int) ) -> + ( PGArrow g (GArrowTensor g (GArrowTensor g Int Int) (GArrowUnit g)) Int) -> + (PGArrow g (GArrowUnit g) (GArrowTensor g (GArrowUnit g) Int) ) +demo' = demo +-} + main = tikz $ \const merge -> demo const merge diff --git a/examples/GArrowPortShape.hs b/examples/GArrowPortShape.hs index 34f14c8..e746b5f 100644 --- a/examples/GArrowPortShape.hs +++ b/examples/GArrowPortShape.hs @@ -186,8 +186,24 @@ detect (GAS_const i) = do { x <- freshM; return $ GASPortShapeWrapper PortUnit detect GAS_merge = do { x <- freshM ; y <- freshM ; return $ GASPortShapeWrapper (PortTensor (PortFree x) (PortFree y)) (PortFree x) GAS_merge } -detect (GAS_loopl f) = error "not implemented" -detect (GAS_loopr f) = error "not implemented" +detect (GAS_loopl f) = do { x <- freshM + ; y <- freshM + ; z <- freshM + ; z' <- freshM -- remove once I fix the occurs check + ; f' <- detect f + ; unifyM (fst $ shapes f') (PortTensor (PortFree z) (PortFree x)) + ; unifyM (snd $ shapes f') (PortTensor (PortFree z') (PortFree y)) + ; return $ GASPortShapeWrapper (PortFree x) (PortFree y) (GAS_loopl (GAS_misc f')) + } +detect (GAS_loopr f) = do { x <- freshM + ; y <- freshM + ; z <- freshM + ; z' <- freshM -- remove once I fix the occurs check + ; f' <- detect f + ; unifyM (fst $ shapes f') (PortTensor (PortFree x) (PortFree z)) + ; unifyM (snd $ shapes f') (PortTensor (PortFree y) (PortFree z')) + ; return $ GASPortShapeWrapper (PortFree x) (PortFree y) (GAS_loopr (GAS_misc f')) + } -detect (GAS_misc f) = error "not implemented" +detect (GAS_misc f) = error "GAS_misc: not implemented" diff --git a/examples/GArrowSkeleton.hs b/examples/GArrowSkeleton.hs index 2c53283..14827ec 100644 --- a/examples/GArrowSkeleton.hs +++ b/examples/GArrowSkeleton.hs @@ -81,7 +81,7 @@ type instance GArrowTensor (GArrowSkeleton m) = (,) type instance GArrowUnit (GArrowSkeleton m) = () type instance GArrowExponent (GArrowSkeleton m) = (->) -instance GArrowSTKC (GArrowSkeleton m) +instance GArrowSTKCL (GArrowSkeleton m) -- -- | Simple structural equality on skeletons. NOTE: two skeletons diff --git a/examples/GArrowTikZ.hs b/examples/GArrowTikZ.hs index 9961830..46929ff 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 @@ -264,8 +268,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 +296,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 +305,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,6 +314,8 @@ 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 @@ -335,6 +347,20 @@ tikZ m = tikZ' ++ 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 p (x+1+width d+1) p "black" tikZ' d@(DiagramBox ptop pin r pout pbot) x = r m x (m ! ptop) (x + width d) (m ! pbot) wires x1 t x2 c = wires' x1 t x2 c "-" @@ -349,12 +375,16 @@ tikZ m = tikZ' 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) diff --git a/examples/Makefile b/examples/Makefile index 7926143..f880d81 100644 --- a/examples/Makefile +++ b/examples/Makefile @@ -1,4 +1,4 @@ -ghc_opt := -fwarn-incomplete-patterns -Werror -odir .build -hidir .build +ghc_opt := -fwarn-incomplete-patterns -Werror -odir .build -hidir .build open: make demo