-{-# OPTIONS_GHC -XRankNTypes -XScopedTypeVariables -XFlexibleContexts -XModalTypes -XKindSignatures -fcoqpass -XMultiParamTypeClasses -dcore-lint #-}
-import GHC.HetMet.GArrow
-import GHC.HetMet.CodeTypes
-import GHC.HetMet.Private
-import GArrowTikZ
+{-# OPTIONS_GHC -XModalTypes -fcoqpass -dcore-lint #-}
+module Demo (demo) where
-{-
-foo :: (forall g a . <[ () -> a
- PGArrow g (GArrowUnit g) a ->
- (forall b . PGArrow g (GArrowTensor g b b) b) ->
--}
---foo con mer = <[ ~~mer ~~con ~~con ]>
-foo f = <[ ~~f ]>
+demo con mer = <[ ~~mer ~~(con (2::Int)) ~~(con (12::Int)) ]>
+
+-- demo const mult = <[ let q = ~~(const (1::Int)) in ~~mult q q ]>
---tester2 f = <[ \x -> ~~f x x ]>
+--demo const mult =
+-- <[ let twelve = ~~(const (12::Int))
+-- in ~~mult (~~mult twelve twelve) (~~mult twelve twelve) ]>
-main = tikz' $ \a b -> pga_flatten (foo (pga_unflatten a))
+{-
+demo const mult = demo' 3
+ where
+ demo' 0 = const 12
+ demo' 1 = const 12
+ demo' n = <[ ~~mult ~~(demo' (n-1)) ~~(demo' (n-2)) ]>
+-}
\ No newline at end of file
--- /dev/null
+import Control.Category
+import GArrowTikZ
+import Demo
+
+main = tikz $ \const merge -> demo const merge
--- /dev/null
+{-# LANGUAGE MultiParamTypeClasses, GADTs, FlexibleContexts, FlexibleInstances, TypeFamilies #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module : GArrowPortShape
+-- Copyright : none
+-- License : public domain
+--
+-- Maintainer : Adam Megacz <megacz@acm.org>
+-- Stability : experimental
+--
+-- | We cannot, at run time, query to find out the input and output
+-- port types of a GArrowSkeleton since Haskell erases types during
+-- compilation. Using Data.Typeable is problematic here because
+-- GAS_comp and GAS_loop{l,r} have an existential type.
+--
+-- In spite of this, we can determine the "shape" of the ports --
+-- which ports are of unit type, and which ports must be tensors. A
+-- GArrowPortShape is a GArrowSkeleton along with this
+-- information for certain nodes (the inference mechanism below adds
+-- it on every node).
+--
+module GArrowPortShape (GArrowPortShape(..), PortShape(..), detectShape)
+where
+import Prelude hiding ( id, (.), lookup )
+import Control.Category
+import GHC.HetMet.GArrow
+import Unify
+import GArrowSkeleton
+import Control.Monad.State
+
+--
+-- | Please keep in mind that the "shapes" computed below are simply the
+-- least-complicated shapes that could possibly work. Just because a
+-- GArrowPortShape has an input port of shape (x,y)
+-- doesn't mean it couldn't later be used in a context where its input
+-- port had shape ((a,b),y)! However, you can be assured that it
+-- won't be used in a context where the input port has shape ().
+--
+data PortShape a = PortUnit
+ | PortTensor (PortShape a) (PortShape a)
+ | PortFree a
+
+data GArrowPortShape m s a b =
+ GASPortPassthrough
+ (PortShape s)
+ (PortShape s)
+ (m a b)
+ | GASPortShapeWrapper
+ (PortShape s)
+ (PortShape s)
+ (GArrowSkeleton (GArrowPortShape m s) a b)
+
+--
+-- implementation below; none of this is exported
+--
+
+type UPort = PortShape UVar
+
+instance Unifiable UPort where
+ unify' (PortTensor x1 y1) (PortTensor x2 y2) = mergeU (unify x1 x2) (unify y1 y2)
+ unify' PortUnit PortUnit = emptyUnifier
+ unify' s1 s2 = error $ "Unifiable UPort got impossible unification case: "
+-- ++ show s1 ++ " and " ++ show s2
+ inject = PortFree
+ project (PortFree v) = Just v
+ project _ = Nothing
+ occurrences (PortFree v) = [v]
+ occurrences (PortTensor x y) = occurrences x ++ occurrences y
+ occurrences PortUnit = []
+
+-- detection monad
+type DetectM a = State ((Unifier UPort),[UVar]) a
+
+shapes :: GArrowPortShape m UVar a b -> (UPort,UPort)
+shapes (GASPortPassthrough x y _) = (x,y)
+shapes (GASPortShapeWrapper x y _) = (x,y)
+
+unifyM :: UPort -> UPort -> DetectM ()
+unifyM p1 p2 = do { (u,vars) <- get
+ ; put (mergeU u $ unify p1 p2 , vars)
+ }
+
+freshM :: DetectM UVar
+freshM = do { (u,(v:vars)) <- get
+ ; put (u,vars)
+ ; return v
+ }
+
+-- recursive version of getU
+getU' :: Unifier UPort -> UPort -> PortShape ()
+getU' u (PortTensor x y) = PortTensor (getU' u x) (getU' u y)
+getU' _ PortUnit = PortUnit
+getU' u x@(PortFree v) = case Unify.getU u v of
+ Nothing -> PortFree () -- or x
+ Just x' -> getU' u x'
+
+resolveG :: Unifier UPort -> (GArrowPortShape m UVar a b) -> GArrowPortShape m () a b
+resolveG u (GASPortPassthrough x y m) = GASPortPassthrough (getU' u x) (getU' u y) m
+resolveG u (GASPortShapeWrapper x y g) = GASPortShapeWrapper (getU' u x) (getU' u y) (resolveG' g)
+ where
+ resolveG' :: GArrowSkeleton (GArrowPortShape m UVar) a b ->
+ GArrowSkeleton (GArrowPortShape m ()) a b
+ resolveG' (GAS_id ) = GAS_id
+ resolveG' (GAS_comp f g) = GAS_comp (resolveG' f) (resolveG' g)
+ resolveG' (GAS_first f) = GAS_first (resolveG' f)
+ resolveG' (GAS_second f) = GAS_second (resolveG' f)
+ resolveG' GAS_cancell = GAS_cancell
+ resolveG' GAS_cancelr = GAS_cancelr
+ resolveG' GAS_uncancell = GAS_uncancell
+ resolveG' GAS_uncancelr = GAS_uncancelr
+ resolveG' GAS_drop = GAS_drop
+ resolveG' (GAS_const i) = GAS_const i
+ resolveG' GAS_copy = GAS_copy
+ resolveG' GAS_merge = GAS_merge
+ resolveG' GAS_swap = GAS_swap
+ resolveG' GAS_assoc = GAS_assoc
+ resolveG' GAS_unassoc = GAS_unassoc
+ resolveG' (GAS_loopl f) = GAS_loopl (resolveG' f)
+ resolveG' (GAS_loopr f) = GAS_loopr (resolveG' f)
+ resolveG' (GAS_misc g ) = GAS_misc $ resolveG u g
+
+detectShape :: GArrowSkeleton m a b -> GArrowPortShape m () a b
+detectShape g = runM (detect g)
+
+runM :: DetectM (GArrowPortShape m UVar a b) -> GArrowPortShape m () a b
+runM f = let s = (emptyUnifier,uvarSupply)
+ g = evalState f s
+ (u,_) = execState f s
+ in resolveG u g
+
+detect :: GArrowSkeleton m a b -> DetectM (GArrowPortShape m UVar a b)
+detect (GAS_id ) = do { x <- freshM ; return $ GASPortShapeWrapper (PortFree x) (PortFree x) GAS_id }
+detect (GAS_comp f g) = do { f' <- detect f
+ ; g' <- detect g
+ ; unifyM (snd $ shapes f') (fst $ shapes g')
+ ; return $ GASPortShapeWrapper (fst $ shapes f') (snd $ shapes g') (GAS_comp (GAS_misc f') (GAS_misc g'))
+ }
+detect (GAS_first f) = do { x <- freshM
+ ; f' <- detect f
+ ; return $ GASPortShapeWrapper
+ (PortTensor (fst $ shapes f') (PortFree x))
+ (PortTensor (snd $ shapes f') (PortFree x))
+ (GAS_first (GAS_misc f'))
+ }
+detect (GAS_second f) = do { x <- freshM
+ ; f' <- detect f
+ ; return $ GASPortShapeWrapper
+ (PortTensor (PortFree x) (fst $ shapes f'))
+ (PortTensor (PortFree x) (snd $ shapes f'))
+ (GAS_second (GAS_misc f'))
+ }
+detect GAS_cancell = do { x <- freshM; return$GASPortShapeWrapper (PortTensor PortUnit (PortFree x)) (PortFree x) GAS_cancell }
+detect GAS_cancelr = do { x <- freshM; return$GASPortShapeWrapper (PortTensor (PortFree x) PortUnit) (PortFree x) GAS_cancelr }
+detect GAS_uncancell = do { x <- freshM; return$GASPortShapeWrapper (PortFree x) (PortTensor PortUnit (PortFree x)) GAS_uncancell }
+detect GAS_uncancelr = do { x <- freshM; return$GASPortShapeWrapper (PortFree x) (PortTensor (PortFree x) PortUnit) GAS_uncancelr }
+detect GAS_drop = do { x <- freshM; return$GASPortShapeWrapper (PortFree x) PortUnit GAS_drop }
+detect GAS_copy = do { x <- freshM
+ ; return $ GASPortShapeWrapper (PortFree x) (PortTensor (PortFree x) (PortFree x)) GAS_copy }
+detect GAS_swap = do { x <- freshM
+ ; y <- freshM
+ ; let x' = PortFree x
+ ; let y' = PortFree y
+ ; return $ GASPortShapeWrapper (PortTensor x' y') (PortTensor y' x') GAS_swap
+ }
+detect GAS_assoc = do { x <- freshM; y <- freshM; z <- freshM
+ ; let x' = PortFree x
+ ; let y' = PortFree y
+ ; let z' = PortFree z
+ ; return $ GASPortShapeWrapper
+ (PortTensor (PortTensor x' y') z')
+ (PortTensor x' (PortTensor y' z'))
+ GAS_assoc
+ }
+detect GAS_unassoc = do { x <- freshM; y <- freshM; z <- freshM
+ ; let x' = PortFree x
+ ; let y' = PortFree y
+ ; let z' = PortFree z
+ ; return $ GASPortShapeWrapper
+ (PortTensor x' (PortTensor y' z'))
+ (PortTensor (PortTensor x' y') z')
+ GAS_unassoc
+ }
+detect (GAS_const i) = do { x <- freshM; return $ GASPortShapeWrapper PortUnit (PortFree x) (GAS_const i) }
+
+-- FIXME: I need to fix the occurs check before I can make these different again
+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_misc f) = error "not implemented"
+
--- /dev/null
+{-# LANGUAGE MultiParamTypeClasses, GADTs, FlexibleContexts, FlexibleInstances, TypeFamilies #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module : GArrowSkeleton
+-- Copyright : none
+-- License : public domain
+--
+-- Maintainer : Adam Megacz <megacz@acm.org>
+-- Stability : experimental
+--
+-- | Sometimes it is convenient to be able to get your hands on the
+-- explicit boxes-and-wires representation of a GArrow-polymorphic
+-- term. GArrowSkeleton lets you do that.
+--
+-- HOWEVER: technically this instance violates the laws (and RULEs)
+-- for Control.Category; the compiler might choose to optimize (f >>>
+-- id) into f, and this optimization would produce a change in
+-- behavior below -- you'd get (GAS_comp f GAS_id) instead of f. In
+-- practice this means that the user must be prepared for the skeleton
+-- TikZ diagram to be a nondeterministically-chosen boxes-and-wires
+-- diagram which ks *equivalent to* the term, rather than structurally
+-- exactly equal to it.
+--
+module GArrowSkeleton (GArrowSkeleton(..), optimize)
+where
+import Prelude hiding ( id, (.), lookup )
+import Control.Category
+import GHC.HetMet.GArrow
+import Unify
+import Control.Monad.State
+
+data GArrowSkeleton m :: * -> * -> *
+ where
+ GAS_const :: Int -> GArrowSkeleton m () Int
+ GAS_id :: GArrowSkeleton m x x
+ GAS_comp :: GArrowSkeleton m x y -> GArrowSkeleton m y z -> GArrowSkeleton m x z
+ GAS_first :: GArrowSkeleton m x y -> GArrowSkeleton m (x,z) (y,z)
+ GAS_second :: GArrowSkeleton m x y -> GArrowSkeleton m (z,x) (z,y)
+ GAS_cancell :: GArrowSkeleton m ((),x) x
+ GAS_cancelr :: GArrowSkeleton m (x,()) x
+ GAS_uncancell :: GArrowSkeleton m x ((),x)
+ GAS_uncancelr :: GArrowSkeleton m x (x,())
+ GAS_assoc :: GArrowSkeleton m ((x,y),z) (x,(y,z))
+ GAS_unassoc :: GArrowSkeleton m (x,(y,z)) ((x,y),z)
+ GAS_drop :: GArrowSkeleton m x ()
+ GAS_copy :: GArrowSkeleton m x (x,x)
+ GAS_swap :: GArrowSkeleton m (x,y) (y,x)
+ GAS_merge :: GArrowSkeleton m (x,y) z
+ GAS_loopl :: GArrowSkeleton m (x,z) (y,z) -> GArrowSkeleton m x y
+ GAS_loopr :: GArrowSkeleton m (z,x) (z,y) -> GArrowSkeleton m x y
+ GAS_misc :: m x y -> GArrowSkeleton m x y
+
+instance Category (GArrowSkeleton m) where
+ id = GAS_id
+ g . f = GAS_comp f g
+
+instance GArrow (GArrowSkeleton m) (,) () where
+ ga_first = GAS_first
+ ga_second = GAS_second
+ ga_cancell = GAS_cancell
+ ga_cancelr = GAS_cancelr
+ ga_uncancell = GAS_uncancell
+ ga_uncancelr = GAS_uncancelr
+ ga_assoc = GAS_assoc
+ ga_unassoc = GAS_unassoc
+
+instance GArrowDrop (GArrowSkeleton m) (,) () where
+ ga_drop = GAS_drop
+
+instance GArrowCopy (GArrowSkeleton m) (,) () where
+ ga_copy = GAS_copy
+
+instance GArrowSwap (GArrowSkeleton m) (,) () where
+ ga_swap = GAS_swap
+
+instance GArrowLoop (GArrowSkeleton m) (,) () where
+ ga_loopl = GAS_loopl
+ ga_loopr = GAS_loopr
+
+type instance GArrowTensor (GArrowSkeleton m) = (,)
+type instance GArrowUnit (GArrowSkeleton m) = ()
+type instance GArrowExponent (GArrowSkeleton m) = (->)
+
+instance GArrowSTKC (GArrowSkeleton m)
+
+--
+-- | Simple structural equality on skeletons. NOTE: two skeletons
+-- with the same shape but different types will nonetheless be "equal";
+-- there's no way around this since types are gone at runtime.
+--
+instance Eq ((GArrowSkeleton m) a b)
+ where
+ x == y = x === y
+ where
+ (===) :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) c d -> Bool
+ (GAS_id ) === (GAS_id ) = True
+ (GAS_comp g f) === (GAS_comp g' f') = f===f' && g===g'
+ (GAS_first f) === (GAS_first f') = f===f'
+ (GAS_second f) === (GAS_second f') = f===f'
+ GAS_cancell === GAS_cancell = True
+ GAS_cancelr === GAS_cancelr = True
+ GAS_uncancell === GAS_uncancell = True
+ GAS_uncancelr === GAS_uncancelr = True
+ GAS_drop === GAS_drop = True
+ (GAS_const i) === (GAS_const i') = i==i'
+ GAS_copy === GAS_copy = True
+ GAS_merge === GAS_merge = True
+ GAS_swap === GAS_swap = True
+ GAS_assoc === GAS_assoc = True
+ GAS_unassoc === GAS_unassoc = True
+ (GAS_loopl f) === (GAS_loopl f') = f === f'
+ (GAS_loopr f) === (GAS_loopr f') = f === f'
+ _ === _ = False
+ -- FIXME: GAS_misc's are never equal!!!
+
+--
+-- | Performs some very simple-minded optimizations on a
+-- boxes-and-wires diagram. Preserves equivalence up to the GArrow
+-- laws, but no guarantees about which optimizations actually happen.
+--
+optimize :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
+optimize x = let x' = optimize' x in if x == x' then x' else optimize x'
+ where
+ optimize' :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
+
+ -- Some optimizations fail due to misparenthesization; we default to
+ -- left-associativity and hope for the best
+ optimize' (GAS_comp f (GAS_comp g h)) = GAS_comp (GAS_comp f g) h
+ optimize' (GAS_comp (GAS_comp f (GAS_comp g h)) k) = GAS_comp (GAS_comp (GAS_comp f g) h) k
+
+ optimize' (GAS_comp (GAS_comp GAS_unassoc (GAS_second g)) GAS_assoc) = GAS_second (GAS_second g)
+ optimize' (GAS_comp (GAS_comp (GAS_comp f GAS_unassoc) (GAS_second g)) GAS_assoc) = GAS_comp f (GAS_second (GAS_second g))
+
+ optimize' (GAS_comp (GAS_comp f g) h) = case optimize_pair g h of
+ Nothing -> GAS_comp (optimize' (GAS_comp f g)) h'
+ Just ret' -> GAS_comp f' ret'
+ where
+ f' = optimize' f
+ g' = optimize' g
+ h' = optimize' h
+ optimize' (GAS_comp f g ) = case optimize_pair f g of
+ Nothing -> GAS_comp f' g'
+ Just ret' -> ret'
+ where
+ f' = optimize' f
+ g' = optimize' g
+ optimize' (GAS_first GAS_id ) = GAS_id
+ optimize' (GAS_second GAS_id ) = GAS_id
+ optimize' (GAS_first f ) = GAS_first $ optimize' f
+ optimize' (GAS_second f ) = GAS_second $ optimize' f
+ optimize' (GAS_loopl GAS_id) = GAS_id
+ optimize' (GAS_loopr GAS_id) = GAS_id
+ optimize' (GAS_loopl f ) = GAS_loopl $ optimize' f
+ optimize' (GAS_loopr f ) = GAS_loopr $ optimize' f
+ optimize' x = x
+
+ optimize_pair :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) b c -> Maybe ((GArrowSkeleton m) a c)
+
+ optimize_pair f GAS_drop = Just $ GAS_drop
+ optimize_pair GAS_id f = Just $ f
+ optimize_pair f GAS_id = Just $ f
+ optimize_pair GAS_uncancell GAS_cancell = Just $ GAS_id
+ optimize_pair GAS_uncancelr GAS_cancelr = Just $ GAS_id
+ optimize_pair GAS_cancell GAS_uncancell = Just $ GAS_id
+ optimize_pair GAS_cancelr GAS_uncancelr = Just $ GAS_id
+ optimize_pair GAS_uncancelr GAS_cancell = Just $ GAS_id
+ optimize_pair GAS_uncancell GAS_cancelr = Just $ GAS_id
+
+ -- first priority: eliminate GAS_first
+ optimize_pair (GAS_first f) GAS_cancelr = Just $ GAS_comp GAS_cancelr f
+ optimize_pair (GAS_second f) GAS_cancell = Just $ GAS_comp GAS_cancell f
+ optimize_pair GAS_uncancelr (GAS_first f) = Just $ GAS_comp f GAS_uncancelr
+ optimize_pair GAS_uncancell (GAS_second f) = Just $ GAS_comp f GAS_uncancell
+
+ -- second priority: push GAS_swap leftward
+ optimize_pair (GAS_second f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_first f)
+ optimize_pair (GAS_first f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_second f)
+ optimize_pair GAS_swap GAS_swap = Just $ GAS_id
+ optimize_pair GAS_swap GAS_cancell = Just $ GAS_cancelr
+ optimize_pair GAS_swap GAS_cancelr = Just $ GAS_cancell
+
+ optimize_pair (GAS_first f) (GAS_first g) = Just $ GAS_first (GAS_comp f g)
+ optimize_pair (GAS_second f) (GAS_second g) = Just $ GAS_second (GAS_comp f g)
+
+ optimize_pair GAS_assoc GAS_cancell = Just $ GAS_first GAS_cancell
+ optimize_pair GAS_unassoc GAS_cancelr = Just $ GAS_second GAS_cancelr
+ optimize_pair GAS_assoc (GAS_second GAS_cancell) = Just $ GAS_first GAS_cancelr
+ optimize_pair GAS_unassoc (GAS_first GAS_cancell) = Just $ GAS_cancell
+
+
+ -- FIXME: valid only for central morphisms
+ --optimize_pair (GAS_second f) (GAS_first g) = Just $ GAS_comp (GAS_first g) (GAS_second f)
+ optimize_pair (GAS_first g) (GAS_second f) = Just $ GAS_comp (GAS_second f) (GAS_first g)
+
+ optimize_pair _ _ = Nothing
+
+
-{-# OPTIONS_GHC -XModalTypes -XMultiParamTypeClasses -XNoMonoPatBinds -XKindSignatures -XGADTs -XFlexibleContexts -XFlexibleInstances -XTypeOperators -XUndecidableInstances -XTypeFamilies #-}
-module GArrowTikZ (tikz, tikz', GArrowTikZ(..))
+{-# LANGUAGE RankNTypes, MultiParamTypeClasses, GADTs, FlexibleContexts, FlexibleInstances, TypeOperators #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module : GArrowTikZ
+-- Copyright : none
+-- License : public domain
+--
+-- Maintainer : Adam Megacz <megacz@acm.org>
+-- Stability : experimental
+--
+-- | Renders a @GArrowSkeleton@ using TikZ; the result is LaTeX code.
+-- You must have lp_solve installed in order for this to work.
+--
+
+module GArrowTikZ (tikz)
where
+import System.Process
import Prelude hiding ( id, (.), lookup )
import Control.Category
+import Control.Monad.State
import GHC.HetMet.GArrow
import Data.List hiding (lookup, insert)
import Data.Map hiding (map, (!))
+import Data.Maybe (catMaybes)
import Unify
+import GArrowSkeleton
+import GArrowPortShape
import GHC.HetMet.Private
-{-
-TO DO:
- - have "resolve" turn a (Diagram UnifVal) into (Diagram Int)
- - custom rendering
- - bias right now is for all edges to be uppermost; try for bias
- towards smallest nodes?
- - curvy boxes (like XOR gates)
--}
-
-
--- a unification value is basically a LISP-ish expression
-data UVal =
- UVVar UVar
- | UVVal [UVal]
-
-instance Unifiable UVal where
- unify' (UVVal vl1) (UVVal vl2)
- | length vl1 /= length vl2 = error "length mismatch during unification"
- | otherwise = foldr mergeU emptyUnifier (map (\(x,y) -> unify x y) $ zip vl1 vl2)
- unify' _ _ = error "impossible"
- inject = UVVar
- project (UVVar v) = Just v
- project _ = Nothing
- occurrences (UVVar v) = [v]
- occurrences (UVVal vl) = concatMap occurrences vl
-
--- | Resolves a unification variable; the answer to this query will change if subsequent unifications are performed
-getU' :: Unifier UVal -> UVal -> UVal
-getU' u (UVVal vl) = UVVal $ map (getU' u) vl
-getU' u x@(UVVar v) = case Unify.getU u v of
- Nothing -> x
- Just x' -> getU' u x'
-
-
-
+------------------------------------------------------------------------------
+-- Tracks
--
--- | Render a fully-polymorphic GArrow term as a boxes-and-wires diagram using TikZ
+-- Figuring out the x-coordinates of the boxes is easy, but we'll need
+-- to use lp_solve to get a nice layout for the y-coordinates of the
+-- wires. A @Track@ is basically just a y-axis position for one of
+-- the horizontal wires in the boxes-and-wires diagram; we will assign
+-- a unique Int to each visual element that has a y-coordinate, then
+-- generate a big pile of constraints on these y-coordinates and have
+-- lp_solve find a solution.
--
+type TrackIdentifier = Int
-type Constraints = [(UVal, Int, UVal)]
+data Tracks = T TrackIdentifier
+ | TU TrackIdentifier -- a track known to be of unit type
+ | TT Tracks Tracks
--- the unification monad
-data UyM t a = UyM (([UVar],Unifier UVal,Constraints) -> ([UVar],Unifier UVal,Constraints,a))
-instance Monad (UyM t)
- where
- return x = UyM $ \(i,u,k) -> (i,u,k,x)
- (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')
-
-
-getU = UyM $ \(i,u,k) -> (i,u,k,u)
-getM v = UyM $ \(i,u,k) -> (i,u,k,getU' u v)
-occursU v x = UyM $ \(i,u,k) -> (i,u,k,occurs u v x)
-unifyM :: Eq t => UVal -> UVal -> UyM t ()
-unifyM v1 v2 = UyM $ \(i,u,k) -> (i,mergeU u (unify v1 v2),k,())
-freshU :: UyM t UVar
-freshU = UyM $ \(i:is,u,k) -> (is,u,k,i)
-constrain :: UVal -> Int -> UVal -> UyM t ()
-constrain v1 d v2 = UyM $ \(i,u,k) -> (i,u,((v1,d,v2):k),())
-getK :: UyM t [(UVal, Int, UVal)]
-getK = UyM $ \(i,u,k) -> (i,u,k,k)
-runU :: UyM t a -> ([UVar],Unifier UVal,Constraints,a)
-runU (UyM f) = (f (uvarSupply,emptyUnifier,[]))
-
-data GArrowTikZ :: * -> * -> *
- where
- TikZ_const :: Int -> GArrowTikZ () Int
- TikZ_id :: GArrowTikZ x x
- TikZ_comp :: GArrowTikZ y z -> GArrowTikZ x y -> GArrowTikZ x z
- TikZ_first :: GArrowTikZ x y -> GArrowTikZ (x**z) (y**z)
- TikZ_second :: GArrowTikZ x y -> GArrowTikZ (z**x) (z**y)
- TikZ_cancell :: GArrowTikZ (()**x) x
- TikZ_cancelr :: GArrowTikZ (x**()) x
- TikZ_uncancell :: GArrowTikZ x (()**x)
- TikZ_uncancelr :: GArrowTikZ x (x**())
- TikZ_assoc :: GArrowTikZ ((x**y)**z) (x**(y**z))
- TikZ_unassoc :: GArrowTikZ (x**(y**z)) ((x**y)**z)
- TikZ_drop :: GArrowTikZ x ()
- TikZ_copy :: GArrowTikZ x (x**x)
- TikZ_swap :: GArrowTikZ (x**y) (y**x)
- TikZ_merge :: GArrowTikZ (x**y) z
- TikZ_loopl :: GArrowTikZ (x**z) (y**z) -> GArrowTikZ x y
- TikZ_loopr :: GArrowTikZ (z**x) (z**y) -> GArrowTikZ x y
+instance Show Tracks where
+ show (T ti ) = "(T "++show ti++")"
+ show (TU ti ) = "(TU "++show ti++")"
+ show (TT t1 t2) = "(TT "++show t1++" "++show t2++")"
--
--- Technically this instance violates the laws (and RULEs) for
--- Control.Category; the compiler might choose to optimize (f >>> id)
--- into f, and this optimization would produce a change in behavior
--- below. In practice this means that the user must be prepared for
--- the rendered TikZ diagram to be merely *equivalent to* his/her
--- term, rather than structurally exactly equal to it.
---
-instance Category GArrowTikZ where
- id = TikZ_id
- (.) = TikZ_comp
-
-instance GArrow GArrowTikZ (**) () where
- ga_first = TikZ_first
- ga_second = TikZ_second
- ga_cancell = TikZ_cancell
- ga_cancelr = TikZ_cancelr
- ga_uncancell = TikZ_uncancell
- ga_uncancelr = TikZ_uncancelr
- ga_assoc = TikZ_assoc
- ga_unassoc = TikZ_unassoc
-
-instance GArrowDrop GArrowTikZ (**) () where
- ga_drop = TikZ_drop
-
-instance GArrowCopy GArrowTikZ (**) () where
- ga_copy = TikZ_copy
-
-instance GArrowSwap GArrowTikZ (**) () where
- ga_swap = TikZ_swap
-
-instance GArrowLoop GArrowTikZ (**) () where
- ga_loopl = TikZ_loopl
- ga_loopr = TikZ_loopr
-
-type instance GArrowTensor GArrowTikZ = (,)
-type instance GArrowUnit GArrowTikZ = ()
-type instance GArrowExponent GArrowTikZ = (->)
-
-instance GArrowSTKC GArrowTikZ
-
-
-name :: GArrowTikZ a b -> String
-name TikZ_id = "id"
-name (TikZ_const i) = "const " ++ show i
-name (TikZ_comp _ _) = "comp"
-name (TikZ_first _ ) = "first"
-name (TikZ_second _ ) = "second"
-name TikZ_cancell = "cancell"
-name TikZ_cancelr = "cancelr"
-name TikZ_uncancell = "uncancell"
-name TikZ_uncancelr = "uncancelr"
-name TikZ_drop = "drop"
-name TikZ_copy = "copy"
-name TikZ_swap = "swap"
-name (TikZ_loopl _ ) = "loopl"
-name (TikZ_loopr _ ) = "loopr"
-name TikZ_assoc = "assoc"
-name TikZ_unassoc = "unassoc"
-
-fresh1 :: UyM () Ports
-fresh1 = do { x <- freshU
- ; return $ UVVar x
- }
+-- | TrackPositions maps TrackIdentifiers to actual y-axis positions;
+-- this is what lp_solve gives us
+--
+type TrackPositions = TrackIdentifier -> Float
-fresh2 :: UyM () (Ports,Ports)
-fresh2 = do { x <- freshU
- ; y <- freshU
- ; constrain (UVVar x) 1 (UVVar y)
- ; return $ (UVVar x,UVVar y)
- }
+(!) :: TrackPositions -> TrackIdentifier -> Float
+tp ! ti = tp ti
-fresh3 :: UyM () (Ports,Ports,Ports)
-fresh3 = do { x <- freshU
- ; y <- freshU
- ; z <- freshU
- ; constrain (UVVar x) 1 (UVVar y)
- ; constrain (UVVar y) 1 (UVVar z)
- ; return $ (UVVar x,UVVar y,UVVar z)
- }
+-- | get the uppermost TrackIdentifier in a Tracks
+uppermost (T x) = x
+uppermost (TU x) = x
+uppermost (TT x y) = uppermost x
-fresh4 :: UyM () (Ports,Ports,Ports,Ports)
-fresh4 = do { x1 <- freshU
- ; x2 <- freshU
- ; x3 <- freshU
- ; x4 <- freshU
- ; constrain (UVVar x1) 1 (UVVar x2)
- ; constrain (UVVar x2) 1 (UVVar x3)
- ; constrain (UVVar x3) 1 (UVVar x4)
- ; return $ (UVVar x1,UVVar x2,UVVar x3,UVVar x4)
- }
+-- | get the lowermost TrackIdentifier in a Tracks
+lowermost (T x) = x
+lowermost (TU x) = x
+lowermost (TT x y) = lowermost y
-fresh5 :: UyM () (Ports,Ports,Ports,Ports,Ports)
-fresh5 = do { x1 <- freshU
- ; x2 <- freshU
- ; x3 <- freshU
- ; x4 <- freshU
- ; x5 <- freshU
- ; constrain (UVVar x1) 1 (UVVar x2)
- ; constrain (UVVar x2) 1 (UVVar x3)
- ; constrain (UVVar x3) 1 (UVVar x4)
- ; constrain (UVVar x4) 1 (UVVar x5)
- ; return $ (UVVar x1,UVVar x2,UVVar x3,UVVar x4,UVVar x5)
- }
+------------------------------------------------------------------------------
+-- Diagrams
---example = ga_first ga_drop >>> ga_cancell >>> ga_first id >>> ga_swap >>> ga_first id >>> TikZ_merge
---example :: forall x y z. forall g. (GArrow g (,) (), GArrowCopy g (,) (), GArrowSwap g (,) ()) => g x ((x,x),x)
---example = ga_copy >>> ga_second ga_copy >>> ga_second (ga_first id) >>> ga_unassoc >>> ga_first ga_swap
---example = ga_copy >>> ga_second ga_copy >>> ga_second (ga_second id) >>> ga_unassoc >>> ga_first id >>> ga_first ga_swap
---example :: forall x. forall g. (GArrow g (,) (), GArrowCopy g (,) (), GArrowSwap g (,) ()) => g x x
---example = id >>> id
+-- | A Diagram is the visual representation of a GArrowSkeleton
+data Diagram
+ = DiagramComp Diagram Diagram
+ | DiagramBox TrackIdentifier Tracks BoxRenderer Tracks TrackIdentifier
+ | DiagramBypassTop Tracks Diagram
+ | DiagramBypassBot Diagram Tracks
+ -- | DiagramLoopTop Tracks Diagram
+ -- | DiagramLoopBot Diagram Tracks
-data Diagram p = DiagramComp (Diagram p) (Diagram p)
- | DiagramPrim String p p p p (String -> Int -> Int -> Int -> p -> p -> Int -> String)
- | DiagramBypassTop p (Diagram p)
- | DiagramBypassBot (Diagram p) p
- -- | DiagramLoopTop Diagram
- -- | DiagramLoopBot Diagram
-
-type Ports = UVal
-
-getOut :: Diagram Ports -> Ports
+-- | get the output tracks of a diagram
+getOut :: Diagram -> Tracks
getOut (DiagramComp f g) = getOut g
-getOut (DiagramPrim s ptop pin pout pbot _) = pout
-getOut (DiagramBypassTop p f) = UVVal [p, (getOut f)]
-getOut (DiagramBypassBot f p) = UVVal [(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
-getIn :: Diagram Ports -> Ports
+-- | get the input tracks of a diagram
+getIn :: Diagram -> Tracks
getIn (DiagramComp f g) = getIn f
-getIn (DiagramPrim s ptop pin pout pbot _) = pin
-getIn (DiagramBypassTop p f) = UVVal [p, (getIn f)]
-getIn (DiagramBypassBot f p) = UVVal [(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
+
+-- | 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
+-- code that draws it
+type BoxRenderer =
+ TrackPositions -> -- resolves the TrackIdentifiers to actual y-coordinates
+ Float -> -- x1
+ Float -> -- y1
+ Float -> -- x2
+ Float -> -- y2
+ String -- TikZ code
+
+
+
+
+
+
+------------------------------------------------------------------------------
+-- Constraints
+
+-- | a constraint (to be dealt with by lp_solve) relates two track identifiers
+data Constraint = C TrackIdentifier Ordering TrackIdentifier {- plus -} Float
+ | EqualSpace TrackIdentifier TrackIdentifier TrackIdentifier TrackIdentifier
+
+-- instance Show Constraint where
+-- show (C t1 LT t2 k s) = "x"++(show t1)++" = x"++(show t2)++" + "++(show k) ++ ";\n"
+-- show (C t1 GT t2 k s) = "x"++(show t1)++" = x"++(show t2)++" + "++(show k) ++ ";\n"
+-- show (C t1 EQ t2 k s) = "x"++(show t1)++" = x"++(show t2)++" + "++(show k) ++ ";\n"
+
+instance Show Constraint where
+ show (C t1 LT t2 k) = "x"++(show t1)++" <= x"++(show t2)++" + "++(show k) ++ ";\n"
+ show (C t1 GT t2 k) = "x"++(show t1)++" >= x"++(show t2)++" + "++(show k) ++ ";\n"
+ show (C t1 EQ t2 k) = "x"++(show t1)++" = x"++(show t2)++" + "++(show k) ++ ";\n"
+ show (EqualSpace t1a t1b t2a t2b) = "x"++(show t1a)++" = x"++(show t1b)++
+ " + x"++(show t2a)++" - x"++(show t2b)++ ";\n"
+
+-- | a monad to accumulate constraints and track the largest TrackIdentifier allocated
+type ConstraintM a = State (TrackIdentifier,[Constraint]) a
+
+-- | pull the constraints out of the monad
+getConstraints :: ConstraintM [Constraint]
+getConstraints = do { (_,c) <- get ; return c }
+
+-- | add a constraint
+constrain :: TrackIdentifier -> Ordering -> TrackIdentifier {- plus -} -> Float -> ConstraintM ()
+constrain t1 ord t2 k = do { (t,c) <- get
+ ; put (t, (C t1 ord t2 k):c)
+ ; return ()
+ }
+
+constrainEqualSpace t1a t1b t2a t2b = do { (t,c) <- get
+ ; put (t, (EqualSpace t1a t1b t2a t2b):c)
+ ; return ()
+ }
+
+-- | simple form for equality constraints
+constrainEq (TT t1a t1b) (TT t2a t2b) = do { constrainEq t1a t2a ; constrainEq t1b t2b ; return () }
+constrainEq (T t1 ) (T t2 ) = constrain t1 EQ t2 0
+constrainEq (TU t1 ) (TU t2 ) = constrain t1 EQ t2 0
+constrainEq (TU t1 ) (T t2 ) = constrain t1 EQ t2 0
+constrainEq (T t1 ) (TU t2 ) = constrain t1 EQ t2 0
+constrainEq t1 t2 = error $ "constrainEq mismatch: " ++ show t1 ++ " and " ++ show t2
+
+-- | allocate a TrackIdentifier
+alloc1 :: ConstraintM Tracks
+alloc1 = do { (t,c) <- get
+ ; put (t+1,c)
+ ; 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
+ where
+ mkdiag' :: 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' }
+ mkdiag' (GAS_first f) = do { (top,(TT _ x),bot) <- alloc inp; f' <- mkdiag' f ; constrainBot f' 1 (uppermost x)
+ ; return $ DiagramBypassBot f' x }
+ mkdiag' (GAS_second f) = do { (top,(TT x _),bot) <- alloc inp; f' <- mkdiag' f ; constrainTop (lowermost x) 1 f'
+ ; return $ DiagramBypassTop x f' }
+ mkdiag' (GAS_id ) = do { (top, x ,bot) <- alloc inp ; simpleDiag "id" top x x bot [(x,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"
+ ; 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"
+ ; 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"
+ ; 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"
+ ; 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
+ ; (_, 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)
+ ; let r tp x1 y1 x2 y2 = drawBox x1 y1 x2 y2 "gray!50" "copy" ++
+ 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 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'))
+ ; constrainEq (T (uppermost y)) (T (uppermost y'))
+ ; simpleDiag' "swap" top (TT x y) (TT x' y') bot [(x,y'),(y,x')] "gray!50" }
+ mkdiag' GAS_assoc =
+ do { (top,(TT (TT x y) z),bot) <- alloc inp
+ ; let r tp x1 y1 x2 y2
+ = drawBox (x1+0.2*xscale) y1 (x2-0.2*xscale) y2 "white" "assoc" ++
+ drawLine x1 y1 x2 y1 "gray!50" "-" ++
+ drawLine x1 y2 x2 y2 "gray!50" "-" ++
+ drawLine x1 y1 x1 ((tp ! uppermost x) - 0.5) "gray!50" "-"++
+ drawLine x1 ((tp ! uppermost x) - 0.5) (x1+0.2) ((tp ! uppermost x) - 0.5) "gray!50" "-"++
+ drawLine (x1+0.2) ((tp ! uppermost x) - 0.5) (x1+0.2) ((tp ! lowermost y) + 0.5) "gray!50" "-"++
+ drawLine (x1+0.2) ((tp ! lowermost y) + 0.5) x1 ((tp ! lowermost y) + 0.5) "gray!50" "-"++
+ drawLine x1 ((tp ! lowermost y) + 0.5) x1 y2 "gray!50" "-"++
+ drawLine x2 y2 x2 ((tp ! lowermost z) + 0.5) "gray!50" "-"++
+ drawLine x2 ((tp ! lowermost z) + 0.5) (x2-0.2) ((tp ! lowermost z) + 0.5) "gray!50" "-"++
+ drawLine (x2-0.2) ((tp ! lowermost z) + 0.5) (x2-0.2) ((tp ! uppermost y) - 0.5) "gray!50" "-"++
+ drawLine (x2-0.2) ((tp ! uppermost y) - 0.5) x2 ((tp ! uppermost y) - 0.5) "gray!50" "-"++
+ drawLine x2 ((tp ! uppermost y) - 0.5) x2 y1 "gray!50" "-"++
+ drawWires tp x1 x x2 x "black" ++
+ drawWires tp x1 y x2 y "black" ++
+ drawWires tp x1 z x2 z "black"
+ ; return $ DiagramBox top (TT (TT x y) z) r (TT x (TT y z)) bot
+ }
+ mkdiag' GAS_unassoc =
+ do { (top,(TT x (TT y z)),bot) <- alloc inp
+ ; let r tp x1 y1 x2 y2
+ = drawBox (x1+0.2*xscale) y1 (x2-0.2*xscale) y2 "white" "unassoc" ++
+ drawLine x1 y1 x2 y1 "gray!50" "-" ++
+ drawLine x1 y2 x2 y2 "gray!50" "-" ++
+ drawLine x2 y1 x2 ((tp ! uppermost x) - 0.5) "gray!50" "-"++
+ drawLine x2 ((tp ! uppermost x) - 0.5) (x2-0.2) ((tp ! uppermost x) - 0.5) "gray!50" "-"++
+ drawLine (x2-0.2) ((tp ! uppermost x) - 0.5) (x2-0.2) ((tp ! lowermost y) + 0.5) "gray!50" "-"++
+ drawLine (x2-0.2) ((tp ! lowermost y) + 0.5) x2 ((tp ! lowermost y) + 0.5) "gray!50" "-"++
+ drawLine x2 ((tp ! lowermost y) + 0.5) x2 y2 "gray!50" "-"++
+ drawLine x1 y2 x1 ((tp ! lowermost z) + 0.5) "gray!50" "-"++
+ drawLine x1 ((tp ! lowermost z) + 0.5) (x1+0.2) ((tp ! lowermost z) + 0.5) "gray!50" "-"++
+ drawLine (x1+0.2) ((tp ! lowermost z) + 0.5) (x1+0.2) ((tp ! uppermost y) - 0.5) "gray!50" "-"++
+ drawLine (x1+0.2) ((tp ! uppermost y) - 0.5) x1 ((tp ! uppermost y) - 0.5) "gray!50" "-"++
+ drawLine x1 ((tp ! uppermost y) - 0.5) x1 y1 "gray!50" "-"++
+ drawWires tp x1 x x2 x "black" ++
+ drawWires tp x1 y x2 y "black" ++
+ 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_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)
+ ; 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 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
+ 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"
-- constrain that Ports is at least Int units above the topmost portion of Diagram
-constrainTop :: Ports -> Int -> Diagram Ports -> UyM () ()
+constrainTop :: TrackIdentifier -> Float -> Diagram -> ConstraintM ()
constrainTop v i (DiagramComp d1 d2) = do { constrainTop v i d1 ; constrainTop v i d2 ; return () }
-constrainTop v i (DiagramBypassTop p d) = constrain v 2 p
+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 (DiagramPrim s ptop pin pout pbot _) = constrain v i ptop
+constrainTop v i (DiagramBox ptop pin r pout pbot) = constrain v LT ptop (-1 * i)
-- constrain that Ports is at least Int units below the bottommost portion of Diagram
-constrainBot :: Diagram Ports -> Int -> Ports -> UyM () ()
+constrainBot :: Diagram -> Float -> TrackIdentifier -> ConstraintM ()
constrainBot (DiagramComp d1 d2) i v = do { constrainBot d1 i v ; constrainBot d2 i v ; return () }
constrainBot (DiagramBypassTop p d) i v = constrainBot d (i+1) v
-constrainBot (DiagramBypassBot d p) i v = constrain p 2 v
-constrainBot (DiagramPrim s ptop pin pout pbot _) i v = constrain pbot i v
-
-ga2diag :: GArrowTikZ a b -> UyM () (Diagram Ports)
-ga2diag (TikZ_id ) = do { (top,x,bot) <- fresh3 ; return $ DiagramPrim "id" top x x bot defren }
-ga2diag (TikZ_comp g f) = do { f' <- ga2diag f
- ; g' <- ga2diag g
- ; unifyM (getOut f') (getIn g')
- ; return $ DiagramComp f' g' }
-ga2diag (TikZ_first f) = do { x <- fresh1; f' <- ga2diag f ; constrainBot f' 1 x ; return $ DiagramBypassBot f' x }
-ga2diag (TikZ_second f) = do { x <- fresh1; f' <- ga2diag f ; constrainTop x 1 f' ; return $ DiagramBypassTop x f' }
-ga2diag TikZ_cancell = do { (top,x,y ,bot) <- fresh4 ; return $ DiagramPrim "cancell" top (UVVal [x,y]) y bot defren }
-ga2diag TikZ_cancelr = do { (top,x,y ,bot) <- fresh4 ; return $ DiagramPrim "cancelr" top (UVVal [x,y]) x bot defren }
-ga2diag TikZ_uncancell = do { (top,x,y ,bot) <- fresh4 ; return $ DiagramPrim "uncancell" top y (UVVal [x,y]) bot defren }
-ga2diag TikZ_uncancelr = do { (top,x,y ,bot) <- fresh4 ; return $ DiagramPrim "uncancelr" top x (UVVal [x,y]) bot defren }
-ga2diag TikZ_drop = do { (top,x ,bot) <- fresh3 ; return $ DiagramPrim "drop" top x x bot defren }
-ga2diag (TikZ_const i) = do { (top,x ,bot) <- fresh3 ; return $ DiagramPrim ("const " ++ show i) top x x bot defren }
-ga2diag TikZ_copy = do { (top,x,y,z,bot) <- fresh5
- ; return $ DiagramPrim "copy" top y (UVVal [x,z]) bot defren }
-ga2diag TikZ_merge = do { (top,x,y,z,bot) <- fresh5
- ; return $ DiagramPrim "merge" top (UVVal [x,z]) y bot defren }
-ga2diag TikZ_swap = do { (top,x,y ,bot) <- fresh4
- ; return $ DiagramPrim "swap" top (UVVal [x,y]) (UVVal [x,y]) bot defren }
-ga2diag TikZ_assoc = do { (top,x,y,z,bot) <- fresh5
- ; return $ DiagramPrim "assoc" top (UVVal [UVVal [x,y],z])(UVVal [x,UVVal [y,z]]) bot defren }
-ga2diag TikZ_unassoc = do { (top,x,y,z,bot) <- fresh5
- ; return $ DiagramPrim "unassoc" top (UVVal [x,UVVal [y,z]])(UVVal [UVVal [x,y],z]) bot defren }
-ga2diag (TikZ_loopl f) = error "not implemented"
-ga2diag (TikZ_loopr f) = error "not implemented"
-
-defren :: String -> Int -> Int -> Int -> Ports -> Ports -> Int -> String
-defren s x w top p1 p2 bot
- = drawBox x top (x+w) bot "black" s
--- ++ wires (x-1) p1 x "green"
--- ++ wires (x+w) p2 (x+w+1) "red"
-
-xscale = 1
-yscale = 1
-
-textc x y text color =
- "\\node[anchor=center,color="++color++"] at ("++show (x*xscale)++"cm,"++show (y*yscale)++"cm) "++
- "{{\\tt{"++text++"}}};\n"
-
-drawBox x1 y1 x2 y2 color text =
- "\\node[anchor=north west] at ("++show (x1*xscale)++"cm,"++show (y1*yscale)++"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)++") -- " ++
- "("++show (x2*xscale)++","++show (y2*yscale)++");\n"
-
-width :: Diagram Ports -> Int
-width (DiagramComp d1 d2) = (width d1) + 1 + (width d2)
-width (DiagramPrim s _ p1 p2 _ _) = 2
-width (DiagramBypassTop p d) = (width d) + 2
-width (DiagramBypassBot d p) = (width d) + 2
-
-(!) :: Map UVar Int -> UVar -> Int
-m ! x = case lookup x m of
- Nothing -> 0
- Just y -> y
-
-tikZ :: Map UVar Int ->
- Diagram Ports ->
- Int -> -- horizontal position
+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
+
+-- | The width of a box is easy to calculate
+width :: Diagram -> Float
+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
+
+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 _ _ _ _ _ = error "drawwires fail"
+
+tikZ :: TrackPositions ->
+ Diagram ->
+ Float -> -- horizontal position
String
tikZ m = tikZ'
where
tikZ' d@(DiagramComp d1 d2) x = tikZ' d1 x
- ++ wires (x+width d1) (getOut d1) (x+width d1+1) "black"
+ ++ wires' (x+width d1) (getOut d1) (x+width d1+0.5) "black" "->"
+ ++ wires' (x+width d1+0.5) (getOut d1) (x+width d1+1) "black" "-"
++ 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"
- ++ drawLine x (top+1) (x+width d') (top+1) "black" "->"
- ++ wires x (getIn d) (x+1) "black"
+ ++ drawWires m x (getIn d) (x+1) (getIn d) "black"
++ tikZ' d (x+1)
- ++ wires (x+1+width d) (getOut d) (x+1+width d+1) "black"
+ ++ 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"
- ++ drawLine x (bot-1) (x+width d') (bot-1) "black" "->"
- ++ wires x (getIn d) (x+1) "black"
+ ++ drawWires m x (getIn d) (x+1) (getIn d) "black"
++ tikZ' d (x+1)
- ++ wires (x+1+width d) (getOut d) (x+1+width d+1) "black"
- tikZ' d@(DiagramPrim s (UVVar top) p1 p2 (UVVar bot) r) x = r s x (width d) (m ! top) p1 p2 (m ! bot)
-
- wires :: Int -> Ports -> Int -> String -> String
- wires x1 (UVVar v) x2 color = drawLine x1 (m ! v) x2 (m ! v) color "->"
- -- ++ textc ((x1+x2) `div` 2) (m!v) (show v) "purple"
- wires x1 (UVVal vl) x2 color = foldr (\x y -> x ++ " " ++ y) [] (map (\v -> wires x1 v x2 color) vl)
-
- getTop :: Diagram Ports -> Int
- getTop (DiagramComp d1 d2) = min (getTop d1) (getTop d2)
- getTop (DiagramBypassTop p d) = (m ! getleft p) - 1
- getTop (DiagramBypassBot d p) = getTop d - 1
- getTop (DiagramPrim s (UVVar ptop) _ _ _ _) = m ! ptop
-
- getBot :: Diagram Ports -> Int
- getBot (DiagramComp d1 d2) = max (getBot d1) (getBot d2)
- getBot (DiagramBypassTop p d) = getBot d + 1
- getBot (DiagramBypassBot d p) = (m ! getright p) + 1
- getBot (DiagramPrim s _ _ _ (UVVar pbot) _) = m ! pbot
-
-resolve' (DiagramComp d1 d2) = do { d1' <- resolve' d1 ; d2' <- resolve' d2 ; return $ DiagramComp d1' d2' }
-resolve' (DiagramBypassTop p d) = do { p' <- getM p ; d' <- resolve' d ; return $ DiagramBypassTop p' d' }
-resolve' (DiagramBypassBot d p) = do { p' <- getM p ; d' <- resolve' d ; return $ DiagramBypassBot d' p' }
-resolve' (DiagramPrim s ptop pin pout pbot r)
- = do { ptop' <- getM ptop
- ; pbot' <- getM pbot
- ; pin' <- getM pin
- ; pout' <- getM pout
- ; return $ DiagramPrim s ptop' pin' pout' pbot' r }
-
-getleft (UVVar v) = v
-getleft (UVVal vl) = getleft (head vl)
-
-getright (UVVar v) = v
-getright (UVVal vl) = getright (last vl)
-
-strip :: [(Ports,Int,Ports)] -> [(UVar,Int,UVar)]
-strip = map (\(v1,x,v2) -> (getright v1, x, getleft v2))
-
-
--- must use bubblesort because the ordering isn't transitive
-sortit :: [(UVar,Int,UVar)] -> [(UVar,Int,UVar)]
-sortit x = stupidSort x []
+ ++ 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 "-"
+
+ 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"
+
+ 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
+
+ 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
+
+-- allocates multiple tracks, adding constraints that they are at least one unit apart
+alloc :: PortShape a -> ConstraintM (TrackIdentifier,Tracks,TrackIdentifier)
+alloc shape = do { tracks <- alloc' shape
+ ; T ptop <- alloc1
+ ; T pbot <- alloc1
+ ; constrain ptop LT (uppermost tracks) (-1)
+ ; constrain pbot GT (lowermost tracks) 1
+ ; return (ptop,tracks,pbot)
+ }
+ where
+ alloc' :: PortShape a -> ConstraintM Tracks
+ alloc' PortUnit = do { T x <- alloc1 ; return (TU x) }
+ alloc' (PortFree _) = do { x <- alloc1 ; return x }
+ alloc' (PortTensor p1 p2) = do { x1 <- alloc' p1
+ ; x2 <- alloc' p2
+ ; constrain (lowermost x1) LT (uppermost x2) (-1)
+ ; return (TT x1 x2)
+ }
+
+do_lp_solve :: [Constraint] -> IO String
+do_lp_solve c = do { let stdin = "min: x1;\n" ++ (foldl (++) "" (map show c)) ++ "\n"
+ ; putStrLn stdin
+ ; stdout <- readProcess "lp_solve" [] stdin
+ ; return stdout
+ }
+
+splitWs :: String -> [String]
+splitWs s = splitWs' "" s
where
- stupidSort [] x = x
- stupidSort (h:t) x = stupidSort t (stupidInsert h x)
-
- stupidInsert t [] = [t]
- stupidInsert t@(_,_,t') ((a@(_,_,a')):b) = if cmp' x t' a' == LT
- then t:a:b
- else a:(stupidInsert t b)
-
- cmp' :: [(UVar,Int,UVar)] -> UVar -> UVar -> Ordering
- cmp' [] a b = EQ -- compare a b
- cmp' ((v1,_,v2):r) a b = if a == v1 && b==v2
- then LT
- else if a == v2 && b==v1
- then GT
- else cmp' r a b
-
-lookup'' :: Map UVar Int -> UVar -> Int
-lookup'' m x = case lookup x m of
- Nothing -> 0
- Just y -> y
-
-valuatit :: Map UVar Int -> [(UVar,Int,UVar)] -> Map UVar Int
-valuatit m [] = m
-valuatit m ((v1,k,v2):r) = valuatit m' r
- where
- m' = insert v2 v2' m
- v2' = max (lookup'' m v2) (k+(lookup'' m v1))
-
-resolve'k :: UyM () [(Ports,Int,Ports)]
-resolve'k = do { k <- getK
- ; k' <- mapM (\(v1,x,v2) -> do { v1' <- getM v1 ; v2' <- getM v2 ; return (v1',x,v2') }) k
- ; return k'
- }
-
-toTikZ :: GArrowTikZ a b -> String
-toTikZ g = tikZ m d 0
- where
- (_,_,_,(d,k)) = runU $ do { d <- ga2diag g
- ; d' <- resolve' d
- ; k' <- resolve'k
- ; return (d',k') }
- s = sortit (strip k)
- m = valuatit empty s
-toTikZ' :: GArrowTikZ a b -> String
-toTikZ' g = foldr (\x y -> x++"\\\\\n"++y) [] (map foo s)
- where
- (_,_,_,k) = runU $ ga2diag g >>= resolve' >>= \_ -> resolve'k
- foo (v1,v,v2) = "x_{"++show v1++"} + "++show v++" \\leq x_{"++show v2++"} = " ++ (show $ lookup'' m v2)
- s = sortit (strip k)
- m = valuatit empty s
-
-tikz' :: (forall g a .
- PGArrow g (GArrowUnit g) a ->
+ splitWs' [] [] = []
+ splitWs' acc [] = [acc]
+ splitWs' [] (' ':k) = splitWs' [] k
+ splitWs' acc (' ':k) = acc:(splitWs' [] k)
+ splitWs' acc (x:k) = splitWs' (acc++[x]) k
+
+lp_solve_to_trackpos :: String -> TrackPositions
+lp_solve_to_trackpos s = toTrackPos $ map parse $ catMaybes $ map grab $ lines s
+ where
+ grab ('x':k) = Just k
+ grab _ = Nothing
+ parse :: String -> (Int,Float)
+ parse s = case splitWs s of
+ [a,b] -> (read a, read b)
+ _ -> error "parse: should not happen"
+ toTrackPos :: [(Int,Float)] -> TrackPositions
+ 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 g =
+ let cm = do { let g' = detectShape g
+ ; g'' <- mkdiag g'
+ ; return 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
+ }
+
+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 $ unG (x (PGArrowD { unG = TikZ_const 12 }) (PGArrowD { unG = TikZ_merge }) )
-main = do putStrLn "hello"
-tikz example
+
+tikz x = tikz' $ optimize $ unG (x (\c -> PGArrowD { unG = GAS_const c }) (PGArrowD { unG = GAS_merge }) )
+
+tikz' example
= do putStrLn "\\documentclass{article}"
- putStrLn "\\usepackage[landscape,paperheight=20in,textwidth=19in]{geometry}"
+ 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]"
- putStrLn (toTikZ example)
+ tikz <- toTikZ example
+ putStrLn tikz
putStrLn "\\end{tikzpicture}"
--- putStrLn "\\begin{align*}"
--- putStr (toTikZ' example)
--- putStrLn "\\end{align*}"
+ putStrLn "\\end{preview}"
+ --putStrLn "\\pagebreak"
+ --putStrLn "\\begin{align*}"
+ --putStr (toTikZ' example)
+ --putStrLn "\\end{align*}"
putStrLn "\\end{document}"
+
+-- Random TikZ routines
+textc x y text color =
+ "\\node[anchor=center,color="++color++"] at ("++show (x*xscale)++"cm,"++show (y*yscale)++"cm) "++
+ "{{\\tt{"++text++"}}};\n"
+
+drawBox x1 y1 x2 y2 color text =
+ "\\node[anchor=north west] at ("++show (x1*xscale)++"cm,"++show (y1*yscale)++"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)++") -- " ++
+ "("++show (x2*xscale)++","++show (y2*yscale)++");\n"
+
+-- | x scaling factor for the entire diagram, since TikZ doesn't scale font sizes
+xscale = 1
+
+-- | y scaling factor for the entire diagram, since TikZ doesn't scale font sizes
+yscale = 1
+ghc_opt := -fwarn-incomplete-patterns -Werror
+
+open:
+ make demo
+ open .build/test.pdf
+
all:
../../../inplace/bin/ghc-stage2 -dcore-lint -fforce-recomp -fcoqpass -ddump-coqpass -ddump-to-file \
`ls *.hs | grep -v Regex | grep -v Unify.hs | grep -v GArrowTikZ.hs ` +RTS -K500M
../../../inplace/bin/ghc-stage2 -dcore-lint -fforce-recomp \
RegexMatcher.hs Unify.hs GArrowTikZ.hs
-tikz:
+demo:
mkdir -p .build
- ../../../inplace/bin/ghc-stage2 -odir .build -hidir .build GArrowTikZ.hs Unify.hs Demo.hs -o .build/demo
+ ../../../inplace/bin/ghc-stage2 $(ghc_opt) -odir .build -hidir .build -c Demo.hs -fforce-recomp
+ ../../../inplace/bin/ghc-stage2 $(ghc_opt) -odir .build -hidir .build --show-iface .build/Demo.hi
+ ../../../inplace/bin/ghc-stage2 $(ghc_opt) -odir .build -hidir .build GArrowTikZ.hs Demo.hs DemoMain.hs Unify.hs -o .build/demo
./.build/demo > .build/test.tex
cd .build; pdflatex test.tex
- open .build/test.pdf
occurs :: Unifiable t => Unifier t -> UVar -> t -> Bool
occurs u v x = elem v $ concatMap (resolve u) (occurrences x)
--- | Given two unifiables, find their most general unifier. Do not override this.
+-- | Given two unifiables, find their most general unifier.
unify :: Unifiable t => t -> t -> Unifier t
unify v1 v2 | (Just v1') <- project v1, (Just v2') <- project v2, v1'==v2' = emptyUnifier
-unify v1 v2 | (Just v1') <- project v1 = if occurs emptyUnifier v1' v2
+unify v1 v2 | (Just v1') <- project v1 = if occurs emptyUnifier v1' v2
then error "occurs check failed"
else Unifier $ insert v1' v2 empty
unify v1 v2 | (Just v2') <- project v2 = unify v2 v1
+++ /dev/null
-[3 of 3] Compiling Main ( Demo.hs, .build/Main.o )
-
-==================== Desugared, before opt ====================
-@ co_aLI::() ~ ()
-co_aLI = TYPE ()
-
-@ co_aHe::GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ ~ ()
-co_aHe = TYPE trans GArrowTikZ.TFCo:R:GArrowUnitGArrowTikZ co_aLI
-
-Rec {
-$dGArrowSTKC_aHd
- :: GHC.HetMet.GArrow.GArrowSTKC GArrowTikZ.GArrowTikZ
-[LclId]
-$dGArrowSTKC_aHd = GArrowTikZ.$fGArrowSTKCGArrowTikZ
-
-Main.foo
- :: forall (t_aD6 :: * -> * -> *) t_aD7.
- <[t_aD7]>@t_aD6 -> <[t_aD7]>@t_aD6
-[LclId]
-Main.foo =
- \ (@ t_aD6::* -> * -> *) (@ t_aD7) ->
- letrec {
- foo_aD5 :: <[t_aD7]>@t_aD6 -> <[t_aD7]>@t_aD6
- [LclId]
- foo_aD5 =
- \ (x_aD4 :: <[t_aD7]>@t_aD6) ->
- GHC.HetMet.CodeTypes.hetmet_brak
- @ t_aD6
- @ t_aD7
- ((GHC.HetMet.CodeTypes.hetmet_esc @ t_aD6 @ t_aD7 x_aD4)
- `cast` (t_aD7 :: t_aD7 ~ t_aD7)); } in
- foo_aD5
-
-Main.foo'
- :: forall (g_aFo :: * -> * -> *) y_aFp.
- (GHC.HetMet.GArrow.GArrowSTKC g_aFo,
- GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()) =>
- GHC.HetMet.Private.PGArrow g_aFo () y_aFp -> g_aFo () y_aFp
-[LclId]
-Main.foo' =
- \ (@ g_aFo::* -> * -> *)
- (@ y_aFp)
- ($dGArrowSTKC_aFq :: GHC.HetMet.GArrow.GArrowSTKC g_aFo)
- (@ co_aFr::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()) ->
- let {
- @ co_aMM::GHC.HetMet.GArrow.GArrowTensor g_aFo
- ~
- GHC.HetMet.GArrow.GArrowTensor g_aFo
- co_aMM = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in
- let {
- @ co_aML::GHC.HetMet.GArrow.GArrowTensor g_aFo
- ~
- GHC.HetMet.GArrow.GArrowTensor g_aFo
- co_aML = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in
- let {
- @ co_aMK::() ~ ()
- co_aMK = TYPE () } in
- let {
- @ co_aMJ::() ~ ()
- co_aMJ = TYPE () } in
- let {
- @ co_aMI::GHC.HetMet.GArrow.GArrowTensor g_aFo
- ~
- GHC.HetMet.GArrow.GArrowTensor g_aFo
- co_aMI = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in
- let {
- @ co_aMH::GHC.HetMet.GArrow.GArrowTensor g_aFo
- ~
- GHC.HetMet.GArrow.GArrowTensor g_aFo
- co_aMH = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in
- let {
- @ co_aMG::() ~ ()
- co_aMG = TYPE () } in
- let {
- @ co_aMF::() ~ ()
- co_aMF = TYPE () } in
- let {
- @ co_aME::GHC.HetMet.GArrow.GArrowTensor g_aFo
- ~
- GHC.HetMet.GArrow.GArrowTensor g_aFo
- co_aME = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in
- let {
- @ co_aMD::GHC.HetMet.GArrow.GArrowTensor g_aFo
- ~
- GHC.HetMet.GArrow.GArrowTensor g_aFo
- co_aMD = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in
- let {
- @ co_aMC::() ~ ()
- co_aMC = TYPE () } in
- let {
- @ co_aMB::() ~ ()
- co_aMB = TYPE () } in
- let {
- @ co_aMz::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
- co_aMz = TYPE trans co_aFr (sym co_aMB) } in
- let {
- @ co_aMu::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
- co_aMu = TYPE trans co_aFr (sym co_aMF) } in
- let {
- @ co_aMp::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
- co_aMp = TYPE trans co_aFr (sym co_aMJ) } in
- let {
- @ co_aM1::GHC.HetMet.GArrow.GArrowUnit g_aFo
- ~
- GHC.HetMet.GArrow.GArrowUnit g_aFo
- co_aM1 = TYPE GHC.HetMet.GArrow.GArrowUnit g_aFo } in
- let {
- @ co_aM4::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
- co_aM4 = TYPE trans (sym co_aM1) co_aFr } in
- let {
- @ co_aLZ::GHC.HetMet.GArrow.GArrowTensor g_aFo
- ~
- GHC.HetMet.GArrow.GArrowTensor g_aFo
- co_aLZ = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in
- let {
- @ co_aMn::GHC.HetMet.GArrow.GArrowTensor g_aFo
- ~
- GHC.HetMet.GArrow.GArrowTensor g_aFo
- co_aMn = TYPE trans co_aLZ (sym co_aML) } in
- let {
- @ co_aMs::GHC.HetMet.GArrow.GArrowTensor g_aFo
- ~
- GHC.HetMet.GArrow.GArrowTensor g_aFo
- co_aMs = TYPE trans co_aLZ (sym co_aMH) } in
- let {
- @ co_aMx::GHC.HetMet.GArrow.GArrowTensor g_aFo
- ~
- GHC.HetMet.GArrow.GArrowTensor g_aFo
- co_aMx = TYPE trans co_aLZ (sym co_aMD) } in
- let {
- @ co_aLV::GHC.HetMet.GArrow.GArrowUnit g_aFo
- ~
- GHC.HetMet.GArrow.GArrowUnit g_aFo
- co_aLV = TYPE GHC.HetMet.GArrow.GArrowUnit g_aFo } in
- let {
- @ co_aM5::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
- co_aM5 = TYPE trans (sym co_aLV) co_aFr } in
- let {
- @ co_aLT::GHC.HetMet.GArrow.GArrowTensor g_aFo
- ~
- GHC.HetMet.GArrow.GArrowTensor g_aFo
- co_aLT = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in
- let {
- @ co_aM6::GHC.HetMet.GArrow.GArrowTensor g_aFo
- ~
- GHC.HetMet.GArrow.GArrowTensor g_aFo
- co_aM6 = TYPE trans (sym co_aLT) co_aLZ } in
- let {
- @ co_aLP::GHC.HetMet.GArrow.GArrowUnit g_aFo
- ~
- GHC.HetMet.GArrow.GArrowUnit g_aFo
- co_aLP = TYPE GHC.HetMet.GArrow.GArrowUnit g_aFo } in
- let {
- @ co_aM7::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
- co_aM7 = TYPE trans (sym co_aLP) co_aFr } in
- let {
- @ co_aLN::GHC.HetMet.GArrow.GArrowTensor g_aFo
- ~
- GHC.HetMet.GArrow.GArrowTensor g_aFo
- co_aLN = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in
- let {
- @ co_aM8::GHC.HetMet.GArrow.GArrowTensor g_aFo
- ~
- GHC.HetMet.GArrow.GArrowTensor g_aFo
- co_aM8 = TYPE trans (sym co_aLN) co_aLZ } in
- let {
- $dGArrowSwap_aLL
- :: GHC.HetMet.GArrow.GArrowSwap
- g_aFo
- (GHC.HetMet.GArrow.GArrowTensor g_aFo)
- (GHC.HetMet.GArrow.GArrowUnit g_aFo)
- [LclId]
- $dGArrowSwap_aLL =
- GHC.HetMet.GArrow.$p3GArrowSTKC @ g_aFo $dGArrowSTKC_aFq } in
- let {
- $dGArrow_aM2
- :: GHC.HetMet.GArrow.GArrow
- g_aFo
- (GHC.HetMet.GArrow.GArrowTensor g_aFo)
- (GHC.HetMet.GArrow.GArrowUnit g_aFo)
- [LclId]
- $dGArrow_aM2 =
- GHC.HetMet.GArrow.$p1GArrowSwap
- @ g_aFo
- @ (GHC.HetMet.GArrow.GArrowTensor g_aFo)
- @ (GHC.HetMet.GArrow.GArrowUnit g_aFo)
- $dGArrowSwap_aLL } in
- let {
- $dCategory_aM3 :: Control.Category.Category g_aFo
- [LclId]
- $dCategory_aM3 =
- GHC.HetMet.GArrow.$p1GArrow
- @ g_aFo
- @ (GHC.HetMet.GArrow.GArrowTensor g_aFo)
- @ (GHC.HetMet.GArrow.GArrowUnit g_aFo)
- $dGArrow_aM2 } in
- let {
- $dGArrow_aMa
- :: GHC.HetMet.GArrow.GArrow
- g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()
- [LclId]
- $dGArrow_aMa =
- $dGArrow_aM2
- `cast` (GHC.HetMet.GArrow.T:GArrow
- g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) co_aM4
- :: GHC.HetMet.GArrow.T:GArrow
- g_aFo
- (GHC.HetMet.GArrow.GArrowTensor g_aFo)
- (GHC.HetMet.GArrow.GArrowUnit g_aFo)
- ~
- GHC.HetMet.GArrow.T:GArrow
- g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()) } in
- let {
- $dGArrowSwap_aM9
- :: GHC.HetMet.GArrow.GArrowSwap
- g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()
- [LclId]
- $dGArrowSwap_aM9 =
- $dGArrowSwap_aLL
- `cast` (GHC.HetMet.GArrow.T:GArrowSwap
- g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) co_aM4
- :: GHC.HetMet.GArrow.T:GArrowSwap
- g_aFo
- (GHC.HetMet.GArrow.GArrowTensor g_aFo)
- (GHC.HetMet.GArrow.GArrowUnit g_aFo)
- ~
- GHC.HetMet.GArrow.T:GArrowSwap
- g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()) } in
- let {
- $dGArrowCopy_aLK
- :: GHC.HetMet.GArrow.GArrowCopy
- g_aFo
- (GHC.HetMet.GArrow.GArrowTensor g_aFo)
- (GHC.HetMet.GArrow.GArrowUnit g_aFo)
- [LclId]
- $dGArrowCopy_aLK =
- GHC.HetMet.GArrow.$p2GArrowSTKC @ g_aFo $dGArrowSTKC_aFq } in
- let {
- $dGArrow_aLW
- :: GHC.HetMet.GArrow.GArrow
- g_aFo
- (GHC.HetMet.GArrow.GArrowTensor g_aFo)
- (GHC.HetMet.GArrow.GArrowUnit g_aFo)
- [LclId]
- $dGArrow_aLW =
- GHC.HetMet.GArrow.$p1GArrowCopy
- @ g_aFo
- @ (GHC.HetMet.GArrow.GArrowTensor g_aFo)
- @ (GHC.HetMet.GArrow.GArrowUnit g_aFo)
- $dGArrowCopy_aLK } in
- let {
- $dCategory_aLX :: Control.Category.Category g_aFo
- [LclId]
- $dCategory_aLX =
- GHC.HetMet.GArrow.$p1GArrow
- @ g_aFo
- @ (GHC.HetMet.GArrow.GArrowTensor g_aFo)
- @ (GHC.HetMet.GArrow.GArrowUnit g_aFo)
- $dGArrow_aLW } in
- let {
- $dGArrow_aMd
- :: GHC.HetMet.GArrow.GArrow
- g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()
- [LclId]
- $dGArrow_aMd =
- $dGArrow_aLW
- `cast` (GHC.HetMet.GArrow.T:GArrow
- g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) co_aM5
- :: GHC.HetMet.GArrow.T:GArrow
- g_aFo
- (GHC.HetMet.GArrow.GArrowTensor g_aFo)
- (GHC.HetMet.GArrow.GArrowUnit g_aFo)
- ~
- GHC.HetMet.GArrow.T:GArrow
- g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()) } in
- let {
- $dGArrow_aMe
- :: GHC.HetMet.GArrow.GArrow
- g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()
- [LclId]
- $dGArrow_aMe =
- $dGArrow_aMd
- `cast` (GHC.HetMet.GArrow.T:GArrow g_aFo co_aM6 ()
- :: GHC.HetMet.GArrow.T:GArrow
- g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()
- ~
- GHC.HetMet.GArrow.T:GArrow
- g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()) } in
- let {
- $dGArrowCopy_aMb
- :: GHC.HetMet.GArrow.GArrowCopy
- g_aFo
- (GHC.HetMet.GArrow.GArrowTensor g_aFo)
- (GHC.HetMet.GArrow.GArrowUnit g_aFo)
- [LclId]
- $dGArrowCopy_aMb =
- $dGArrowCopy_aLK
- `cast` (GHC.HetMet.GArrow.T:GArrowCopy
- g_aFo co_aM6 (GHC.HetMet.GArrow.GArrowUnit g_aFo)
- :: GHC.HetMet.GArrow.T:GArrowCopy
- g_aFo
- (GHC.HetMet.GArrow.GArrowTensor g_aFo)
- (GHC.HetMet.GArrow.GArrowUnit g_aFo)
- ~
- GHC.HetMet.GArrow.T:GArrowCopy
- g_aFo
- (GHC.HetMet.GArrow.GArrowTensor g_aFo)
- (GHC.HetMet.GArrow.GArrowUnit g_aFo)) } in
- let {
- $dGArrowCopy_aMc
- :: GHC.HetMet.GArrow.GArrowCopy
- g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()
- [LclId]
- $dGArrowCopy_aMc =
- $dGArrowCopy_aMb
- `cast` (GHC.HetMet.GArrow.T:GArrowCopy
- g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) co_aM5
- :: GHC.HetMet.GArrow.T:GArrowCopy
- g_aFo
- (GHC.HetMet.GArrow.GArrowTensor g_aFo)
- (GHC.HetMet.GArrow.GArrowUnit g_aFo)
- ~
- GHC.HetMet.GArrow.T:GArrowCopy
- g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()) } in
- let {
- $dGArrowDrop_aLJ
- :: GHC.HetMet.GArrow.GArrowDrop
- g_aFo
- (GHC.HetMet.GArrow.GArrowTensor g_aFo)
- (GHC.HetMet.GArrow.GArrowUnit g_aFo)
- [LclId]
- $dGArrowDrop_aLJ =
- GHC.HetMet.GArrow.$p1GArrowSTKC @ g_aFo $dGArrowSTKC_aFq } in
- let {
- $dGArrow_aLQ
- :: GHC.HetMet.GArrow.GArrow
- g_aFo
- (GHC.HetMet.GArrow.GArrowTensor g_aFo)
- (GHC.HetMet.GArrow.GArrowUnit g_aFo)
- [LclId]
- $dGArrow_aLQ =
- GHC.HetMet.GArrow.$p1GArrowDrop
- @ g_aFo
- @ (GHC.HetMet.GArrow.GArrowTensor g_aFo)
- @ (GHC.HetMet.GArrow.GArrowUnit g_aFo)
- $dGArrowDrop_aLJ } in
- let {
- $dCategory_aLR :: Control.Category.Category g_aFo
- [LclId]
- $dCategory_aLR =
- GHC.HetMet.GArrow.$p1GArrow
- @ g_aFo
- @ (GHC.HetMet.GArrow.GArrowTensor g_aFo)
- @ (GHC.HetMet.GArrow.GArrowUnit g_aFo)
- $dGArrow_aLQ } in
- let {
- $dGArrow_aMh
- :: GHC.HetMet.GArrow.GArrow
- g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()
- [LclId]
- $dGArrow_aMh =
- $dGArrow_aLQ
- `cast` (GHC.HetMet.GArrow.T:GArrow
- g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) co_aM7
- :: GHC.HetMet.GArrow.T:GArrow
- g_aFo
- (GHC.HetMet.GArrow.GArrowTensor g_aFo)
- (GHC.HetMet.GArrow.GArrowUnit g_aFo)
- ~
- GHC.HetMet.GArrow.T:GArrow
- g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()) } in
- let {
- $dGArrow_aMi
- :: GHC.HetMet.GArrow.GArrow
- g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()
- [LclId]
- $dGArrow_aMi =
- $dGArrow_aMh
- `cast` (GHC.HetMet.GArrow.T:GArrow g_aFo co_aM8 ()
- :: GHC.HetMet.GArrow.T:GArrow
- g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()
- ~
- GHC.HetMet.GArrow.T:GArrow
- g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()) } in
- let {
- $dGArrowDrop_aMf
- :: GHC.HetMet.GArrow.GArrowDrop
- g_aFo
- (GHC.HetMet.GArrow.GArrowTensor g_aFo)
- (GHC.HetMet.GArrow.GArrowUnit g_aFo)
- [LclId]
- $dGArrowDrop_aMf =
- $dGArrowDrop_aLJ
- `cast` (GHC.HetMet.GArrow.T:GArrowDrop
- g_aFo co_aM8 (GHC.HetMet.GArrow.GArrowUnit g_aFo)
- :: GHC.HetMet.GArrow.T:GArrowDrop
- g_aFo
- (GHC.HetMet.GArrow.GArrowTensor g_aFo)
- (GHC.HetMet.GArrow.GArrowUnit g_aFo)
- ~
- GHC.HetMet.GArrow.T:GArrowDrop
- g_aFo
- (GHC.HetMet.GArrow.GArrowTensor g_aFo)
- (GHC.HetMet.GArrow.GArrowUnit g_aFo)) } in
- let {
- $dGArrowDrop_aMg
- :: GHC.HetMet.GArrow.GArrowDrop
- g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()
- [LclId]
- $dGArrowDrop_aMg =
- $dGArrowDrop_aMf
- `cast` (GHC.HetMet.GArrow.T:GArrowDrop
- g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) co_aM7
- :: GHC.HetMet.GArrow.T:GArrowDrop
- g_aFo
- (GHC.HetMet.GArrow.GArrowTensor g_aFo)
- (GHC.HetMet.GArrow.GArrowUnit g_aFo)
- ~
- GHC.HetMet.GArrow.T:GArrowDrop
- g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()) } in
- let {
- @ co_aF3::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
- co_aF3 = TYPE co_aFr } in
- let {
- @ co_aEX::() ~ ()
- co_aEX = TYPE () } in
- let {
- @ co_aEI::GHC.HetMet.GArrow.GArrowTensor g_aFo
- ~
- GHC.HetMet.GArrow.GArrowTensor g_aFo
- co_aEI = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in
- let {
- @ co_aEG::GHC.HetMet.GArrow.GArrowTensor g_aFo
- ~
- GHC.HetMet.GArrow.GArrowTensor g_aFo
- co_aEG = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in
- let {
- @ co_aEF::GHC.HetMet.GArrow.GArrowTensor g_aFo
- ~
- GHC.HetMet.GArrow.GArrowTensor g_aFo
- co_aEF = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in
- let {
- @ co_aEE::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
- co_aEE =
- TYPE trans
- (trans (GHC.HetMet.GArrow.GArrowUnit g_aFo) co_aF3)
- (sym co_aEX) } in
- let {
- @ co_aEz::() ~ ()
- co_aEz = TYPE () } in
- let {
- @ co_aF0::() ~ ()
- co_aF0 = TYPE trans co_aEz co_aEX } in
- let {
- @ co_aEy::() ~ ()
- co_aEy = TYPE () } in
- let {
- @ co_aEx::GHC.HetMet.GArrow.GArrowTensor g_aFo
- ~
- GHC.HetMet.GArrow.GArrowTensor g_aFo
- co_aEx =
- TYPE trans
- (trans (GHC.HetMet.GArrow.GArrowTensor g_aFo) co_aEI)
- (sym co_aEG) } in
- let {
- @ co_aEw::GHC.HetMet.GArrow.GArrowTensor g_aFo
- ~
- GHC.HetMet.GArrow.GArrowTensor g_aFo
- co_aEw = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in
- let {
- @ co_aEH::GHC.HetMet.GArrow.GArrowTensor g_aFo
- ~
- GHC.HetMet.GArrow.GArrowTensor g_aFo
- co_aEH = TYPE trans co_aEw co_aEG } in
- let {
- @ co_aEv::GHC.HetMet.GArrow.GArrowTensor g_aFo
- ~
- GHC.HetMet.GArrow.GArrowTensor g_aFo
- co_aEv = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in
- let {
- @ co_aEu::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
- co_aEu =
- TYPE trans
- (trans (GHC.HetMet.GArrow.GArrowUnit g_aFo) co_aEE)
- (sym co_aEz) } in
- let {
- @ co_aEq::() ~ ()
- co_aEq = TYPE () } in
- let {
- @ co_aEC::() ~ ()
- co_aEC = TYPE trans co_aEq co_aEz } in
- let {
- @ co_aEZ::() ~ ()
- co_aEZ = TYPE trans co_aEC co_aEX } in
- let {
- @ co_aEp::() ~ ()
- co_aEp = TYPE () } in
- let {
- @ co_aEo::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
- co_aEo =
- TYPE trans
- (trans (GHC.HetMet.GArrow.GArrowUnit g_aFo) co_aEu)
- (sym co_aEq) } in
- let {
- @ co_aEl::() ~ ()
- co_aEl = TYPE () } in
- let {
- @ co_aEs::() ~ ()
- co_aEs = TYPE trans co_aEl co_aEq } in
- let {
- @ co_aED::() ~ ()
- co_aED = TYPE trans co_aEs co_aEz } in
- let {
- @ co_aF1::() ~ ()
- co_aF1 = TYPE trans co_aED co_aEX } in
- let {
- @ co_aEk::() ~ ()
- co_aEk = TYPE () } in
- let {
- @ co_aEj::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
- co_aEj =
- TYPE trans
- (trans (GHC.HetMet.GArrow.GArrowUnit g_aFo) co_aEo)
- (sym co_aEl) } in
- let {
- @ co_aEh::() ~ ()
- co_aEh = TYPE () } in
- let {
- @ co_aEn::() ~ ()
- co_aEn = TYPE trans co_aEh co_aEl } in
- let {
- @ co_aEr::() ~ ()
- co_aEr = TYPE trans co_aEn co_aEq } in
- let {
- @ co_aEA::() ~ ()
- co_aEA = TYPE trans co_aEr co_aEz } in
- let {
- @ co_aEY::() ~ ()
- co_aEY = TYPE trans co_aEA co_aEX } in
- let {
- @ co_aEg::() ~ ()
- co_aEg = TYPE () } in
- let {
- @ co_aEf::GHC.HetMet.Private.PGArrow g_aFo () y_aFp
- ~
- GHC.HetMet.Private.PGArrow g_aFo () y_aFp
- co_aEf = TYPE GHC.HetMet.Private.PGArrow g_aFo () y_aFp } in
- let {
- @ co_aEi::GHC.HetMet.Private.PGArrow g_aFo () y_aFp
- ~
- GHC.HetMet.Private.PGArrow g_aFo () y_aFp
- co_aEi =
- TYPE trans
- co_aEf (GHC.HetMet.Private.PGArrow g_aFo co_aEh y_aFp) } in
- let {
- @ co_aEm::GHC.HetMet.Private.PGArrow g_aFo () y_aFp
- ~
- GHC.HetMet.Private.PGArrow g_aFo () y_aFp
- co_aEm =
- TYPE trans
- co_aEi (GHC.HetMet.Private.PGArrow g_aFo co_aEl y_aFp) } in
- let {
- @ co_aEt::GHC.HetMet.Private.PGArrow g_aFo () y_aFp
- ~
- GHC.HetMet.Private.PGArrow g_aFo () y_aFp
- co_aEt =
- TYPE trans
- co_aEm (GHC.HetMet.Private.PGArrow g_aFo co_aEq y_aFp) } in
- let {
- @ co_aEB::GHC.HetMet.Private.PGArrow g_aFo () y_aFp
- ~
- GHC.HetMet.Private.PGArrow g_aFo () y_aFp
- co_aEB =
- TYPE trans
- co_aEt (GHC.HetMet.Private.PGArrow g_aFo co_aEz y_aFp) } in
- let {
- @ co_aF2::GHC.HetMet.Private.PGArrow g_aFo () y_aFp
- ~
- GHC.HetMet.Private.PGArrow g_aFo () y_aFp
- co_aF2 =
- TYPE trans
- co_aEB (GHC.HetMet.Private.PGArrow g_aFo co_aEX y_aFp) } in
- let {
- @ co_aEd::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
- co_aEd = TYPE trans co_aEj (sym co_aEk) } in
- let {
- @ co_aEb::GHC.HetMet.GArrow.GArrowTensor g_aFo
- ~
- GHC.HetMet.GArrow.GArrowTensor g_aFo
- co_aEb =
- TYPE trans
- (trans (GHC.HetMet.GArrow.GArrowTensor g_aFo) co_aEx)
- (sym co_aEw) } in
- let {
- @ co_aE8::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
- co_aE8 = TYPE trans co_aEo (sym co_aEp) } in
- let {
- @ co_aE6::GHC.HetMet.GArrow.GArrowTensor g_aFo
- ~
- GHC.HetMet.GArrow.GArrowTensor g_aFo
- co_aE6 = TYPE trans co_aEb (sym co_aEv) } in
- let {
- @ co_aE3::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
- co_aE3 = TYPE trans co_aEu (sym co_aEy) } in
- let {
- @ co_aE1::GHC.HetMet.GArrow.GArrowTensor g_aFo
- ~
- GHC.HetMet.GArrow.GArrowTensor g_aFo
- co_aE1 = TYPE trans co_aEx (sym co_aEF) } in
- let {
- @ co_aDD::GHC.HetMet.Private.PGArrow g_aFo () y_aFp
- ~
- GHC.HetMet.Private.PGArrow g_aFo () y_aFp
- co_aDD = TYPE GHC.HetMet.Private.PGArrow g_aFo () y_aFp } in
- let {
- @ co_aDC::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
- co_aDC =
- TYPE trans
- (trans (GHC.HetMet.GArrow.GArrowUnit g_aFo) co_aEj)
- (sym co_aEh) } in
- let {
- @ co_aDA::GHC.HetMet.Private.PGArrow g_aFo () y_aFp
- ~
- GHC.HetMet.Private.PGArrow
- g_aFo (GHC.HetMet.GArrow.GArrowUnit g_aFo) y_aFp
- co_aDA =
- TYPE trans
- co_aDD
- (GHC.HetMet.Private.PGArrow
- g_aFo
- (trans (sym co_aDC) (GHC.HetMet.GArrow.GArrowUnit g_aFo))
- y_aFp) } in
- let {
- @ co_aDv::GHC.HetMet.Private.PGArrow
- g_aFo (GHC.HetMet.GArrow.GArrowUnit g_aFo) y_aFp
- ~
- GHC.HetMet.Private.PGArrow g_aFo () y_aFp
- co_aDv = TYPE sym co_aDA } in
- let {
- @ co_aDr::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
- co_aDr = TYPE trans co_aDC (sym co_aEg) } in
- let {
- $dGArrowSTKC_aDm :: GHC.HetMet.GArrow.GArrowSTKC g_aFo
- [LclId]
- $dGArrowSTKC_aDm = $dGArrowSTKC_aFq } in
- letrec {
- foo'_aDw
- :: GHC.HetMet.Private.PGArrow g_aFo () y_aFp -> g_aFo () y_aFp
- [LclId]
- foo'_aDw =
- GHC.Base..
- @ (GHC.HetMet.Private.PGArrow g_aFo () y_aFp)
- @ (g_aFo () y_aFp)
- @ (GHC.HetMet.Private.PGArrow g_aFo () y_aFp)
- (GHC.HetMet.Private.unG @ g_aFo @ () @ y_aFp $dGArrowSTKC_aDm)
- (GHC.Base..
- @ <[y_aFp]>@g_aFo
- @ (GHC.HetMet.Private.PGArrow g_aFo () y_aFp)
- @ (GHC.HetMet.Private.PGArrow g_aFo () y_aFp)
- ((GHC.HetMet.CodeTypes.pga_flatten @ g_aFo @ GHC.Prim.Any @ y_aFp)
- `cast` (<[y_aFp]>@g_aFo
- -> GHC.HetMet.Private.PGArrow g_aFo co_aDr y_aFp
- :: (<[y_aFp]>@g_aFo
- -> GHC.HetMet.Private.PGArrow
- g_aFo (GHC.HetMet.GArrow.GArrowUnit g_aFo) y_aFp)
- ~
- (<[y_aFp]>@g_aFo -> GHC.HetMet.Private.PGArrow g_aFo () y_aFp)))
- (GHC.Base..
- @ <[y_aFp]>@g_aFo
- @ <[y_aFp]>@g_aFo
- @ (GHC.HetMet.Private.PGArrow g_aFo () y_aFp)
- (Main.foo @ g_aFo @ y_aFp)
- ((GHC.HetMet.CodeTypes.pga_unflatten
- @ g_aFo @ GHC.Prim.Any @ y_aFp)
- `cast` (co_aDv -> <[y_aFp]>@g_aFo
- :: (GHC.HetMet.Private.PGArrow
- g_aFo (GHC.HetMet.GArrow.GArrowUnit g_aFo) y_aFp
- -> <[y_aFp]>@g_aFo)
- ~
- (GHC.HetMet.Private.PGArrow g_aFo () y_aFp
- -> <[y_aFp]>@g_aFo))))); } in
- foo'_aDw
-
-Main.main :: GHC.Types.IO ()
-[LclIdX]
-Main.main =
- let {
- @ co_aLu::GHC.Types.Int ~ GHC.Types.Int
- co_aLu = TYPE GHC.Types.Int } in
- let {
- @ co_aLt::GHC.Types.Int ~ GHC.Types.Int
- co_aLt = TYPE GHC.Types.Int } in
- letrec {
- main_aHj :: GHC.Types.IO ()
- [LclId]
- main_aHj =
- GArrowTikZ.tikz
- @ ()
- @ GHC.Types.Int
- (Main.foo'
- @ GArrowTikZ.GArrowTikZ
- @ GHC.Types.Int
- $dGArrowSTKC_aHd
- @ co_aHe
- (GHC.HetMet.Private.PGArrowD
- @ GArrowTikZ.GArrowTikZ
- @ ()
- @ GHC.Types.Int
- (\ ($dGArrowSTKC_aHg
- :: GHC.HetMet.GArrow.GArrowSTKC GArrowTikZ.GArrowTikZ) ->
- let {
- @ co_aHD::GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ
- ~
- GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ
- co_aHD =
- TYPE GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ } in
- let {
- @ co_aHG::GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ ~ ()
- co_aHG =
- TYPE trans (sym co_aHD) GArrowTikZ.TFCo:R:GArrowUnitGArrowTikZ } in
- let {
- @ co_aHB::GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ
- ~
- GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ
- co_aHB =
- TYPE GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ } in
- let {
- @ co_aHH::GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ
- ~
- (,)
- co_aHH =
- TYPE trans
- (sym co_aHB) GArrowTikZ.TFCo:R:GArrowTensorGArrowTikZ } in
- let {
- @ co_aHx::GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ
- ~
- GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ
- co_aHx =
- TYPE GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ } in
- let {
- @ co_aLd::GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ ~ ()
- co_aLd =
- TYPE trans (sym co_aHx) GArrowTikZ.TFCo:R:GArrowUnitGArrowTikZ } in
- let {
- @ co_aHv::GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ
- ~
- GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ
- co_aHv =
- TYPE GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ } in
- let {
- @ co_aLe::GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ
- ~
- (,)
- co_aLe =
- TYPE trans
- (sym co_aHv) GArrowTikZ.TFCo:R:GArrowTensorGArrowTikZ } in
- let {
- @ co_aHr::GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ
- ~
- GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ
- co_aHr =
- TYPE GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ } in
- let {
- @ co_aLf::GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ ~ ()
- co_aLf =
- TYPE trans (sym co_aHr) GArrowTikZ.TFCo:R:GArrowUnitGArrowTikZ } in
- let {
- @ co_aHp::GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ
- ~
- GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ
- co_aHp =
- TYPE GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ } in
- let {
- @ co_aLg::GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ
- ~
- (,)
- co_aLg =
- TYPE trans
- (sym co_aHp) GArrowTikZ.TFCo:R:GArrowTensorGArrowTikZ } in
- let {
- $dGArrowSwap_aHn
- :: GHC.HetMet.GArrow.GArrowSwap
- GArrowTikZ.GArrowTikZ
- (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
- [LclId]
- $dGArrowSwap_aHn =
- GHC.HetMet.GArrow.$p3GArrowSTKC
- @ GArrowTikZ.GArrowTikZ $dGArrowSTKC_aHg } in
- let {
- $dGArrow_aHE
- :: GHC.HetMet.GArrow.GArrow
- GArrowTikZ.GArrowTikZ
- (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
- [LclId]
- $dGArrow_aHE =
- GHC.HetMet.GArrow.$p1GArrowSwap
- @ GArrowTikZ.GArrowTikZ
- @ (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- @ (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
- $dGArrowSwap_aHn } in
- let {
- $dCategory_aHF :: Control.Category.Category GArrowTikZ.GArrowTikZ
- [LclId]
- $dCategory_aHF =
- GHC.HetMet.GArrow.$p1GArrow
- @ GArrowTikZ.GArrowTikZ
- @ (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- @ (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
- $dGArrow_aHE } in
- let {
- $dGArrow_aLj
- :: GHC.HetMet.GArrow.GArrow
- GArrowTikZ.GArrowTikZ
- (,)
- (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
- [LclId]
- $dGArrow_aLj =
- $dGArrow_aHE
- `cast` (GHC.HetMet.GArrow.T:GArrow
- GArrowTikZ.GArrowTikZ
- co_aHH
- (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
- :: GHC.HetMet.GArrow.T:GArrow
- GArrowTikZ.GArrowTikZ
- (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
- ~
- GHC.HetMet.GArrow.T:GArrow
- GArrowTikZ.GArrowTikZ
- (,)
- (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)) } in
- let {
- $dGArrow_aLk
- :: GHC.HetMet.GArrow.GArrow GArrowTikZ.GArrowTikZ (,) ()
- [LclId]
- $dGArrow_aLk =
- $dGArrow_aLj
- `cast` (GHC.HetMet.GArrow.T:GArrow GArrowTikZ.GArrowTikZ (,) co_aHG
- :: GHC.HetMet.GArrow.T:GArrow
- GArrowTikZ.GArrowTikZ
- (,)
- (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
- ~
- GHC.HetMet.GArrow.T:GArrow GArrowTikZ.GArrowTikZ (,) ()) } in
- let {
- $dGArrowSwap_aLh
- :: GHC.HetMet.GArrow.GArrowSwap
- GArrowTikZ.GArrowTikZ
- (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- ()
- [LclId]
- $dGArrowSwap_aLh =
- $dGArrowSwap_aHn
- `cast` (GHC.HetMet.GArrow.T:GArrowSwap
- GArrowTikZ.GArrowTikZ
- (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- co_aHG
- :: GHC.HetMet.GArrow.T:GArrowSwap
- GArrowTikZ.GArrowTikZ
- (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
- ~
- GHC.HetMet.GArrow.T:GArrowSwap
- GArrowTikZ.GArrowTikZ
- (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- ()) } in
- let {
- $dGArrowSwap_aLi
- :: GHC.HetMet.GArrow.GArrowSwap GArrowTikZ.GArrowTikZ (,) ()
- [LclId]
- $dGArrowSwap_aLi =
- $dGArrowSwap_aLh
- `cast` (GHC.HetMet.GArrow.T:GArrowSwap
- GArrowTikZ.GArrowTikZ co_aHH ()
- :: GHC.HetMet.GArrow.T:GArrowSwap
- GArrowTikZ.GArrowTikZ
- (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- ()
- ~
- GHC.HetMet.GArrow.T:GArrowSwap GArrowTikZ.GArrowTikZ (,) ()) } in
- let {
- $dGArrowCopy_aHm
- :: GHC.HetMet.GArrow.GArrowCopy
- GArrowTikZ.GArrowTikZ
- (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
- [LclId]
- $dGArrowCopy_aHm =
- GHC.HetMet.GArrow.$p2GArrowSTKC
- @ GArrowTikZ.GArrowTikZ $dGArrowSTKC_aHg } in
- let {
- $dGArrow_aHy
- :: GHC.HetMet.GArrow.GArrow
- GArrowTikZ.GArrowTikZ
- (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
- [LclId]
- $dGArrow_aHy =
- GHC.HetMet.GArrow.$p1GArrowCopy
- @ GArrowTikZ.GArrowTikZ
- @ (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- @ (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
- $dGArrowCopy_aHm } in
- let {
- $dCategory_aHz :: Control.Category.Category GArrowTikZ.GArrowTikZ
- [LclId]
- $dCategory_aHz =
- GHC.HetMet.GArrow.$p1GArrow
- @ GArrowTikZ.GArrowTikZ
- @ (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- @ (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
- $dGArrow_aHy } in
- let {
- $dGArrow_aLn
- :: GHC.HetMet.GArrow.GArrow
- GArrowTikZ.GArrowTikZ
- (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- ()
- [LclId]
- $dGArrow_aLn =
- $dGArrow_aHy
- `cast` (GHC.HetMet.GArrow.T:GArrow
- GArrowTikZ.GArrowTikZ
- (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- co_aLd
- :: GHC.HetMet.GArrow.T:GArrow
- GArrowTikZ.GArrowTikZ
- (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
- ~
- GHC.HetMet.GArrow.T:GArrow
- GArrowTikZ.GArrowTikZ
- (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- ()) } in
- let {
- $dGArrow_aLo
- :: GHC.HetMet.GArrow.GArrow GArrowTikZ.GArrowTikZ (,) ()
- [LclId]
- $dGArrow_aLo =
- $dGArrow_aLn
- `cast` (GHC.HetMet.GArrow.T:GArrow GArrowTikZ.GArrowTikZ co_aLe ()
- :: GHC.HetMet.GArrow.T:GArrow
- GArrowTikZ.GArrowTikZ
- (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- ()
- ~
- GHC.HetMet.GArrow.T:GArrow GArrowTikZ.GArrowTikZ (,) ()) } in
- let {
- $dGArrowCopy_aLl
- :: GHC.HetMet.GArrow.GArrowCopy
- GArrowTikZ.GArrowTikZ
- (,)
- (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
- [LclId]
- $dGArrowCopy_aLl =
- $dGArrowCopy_aHm
- `cast` (GHC.HetMet.GArrow.T:GArrowCopy
- GArrowTikZ.GArrowTikZ
- co_aLe
- (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
- :: GHC.HetMet.GArrow.T:GArrowCopy
- GArrowTikZ.GArrowTikZ
- (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
- ~
- GHC.HetMet.GArrow.T:GArrowCopy
- GArrowTikZ.GArrowTikZ
- (,)
- (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)) } in
- let {
- $dGArrowCopy_aLm
- :: GHC.HetMet.GArrow.GArrowCopy GArrowTikZ.GArrowTikZ (,) ()
- [LclId]
- $dGArrowCopy_aLm =
- $dGArrowCopy_aLl
- `cast` (GHC.HetMet.GArrow.T:GArrowCopy
- GArrowTikZ.GArrowTikZ (,) co_aLd
- :: GHC.HetMet.GArrow.T:GArrowCopy
- GArrowTikZ.GArrowTikZ
- (,)
- (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
- ~
- GHC.HetMet.GArrow.T:GArrowCopy GArrowTikZ.GArrowTikZ (,) ()) } in
- let {
- $dGArrowDrop_aHl
- :: GHC.HetMet.GArrow.GArrowDrop
- GArrowTikZ.GArrowTikZ
- (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
- [LclId]
- $dGArrowDrop_aHl =
- GHC.HetMet.GArrow.$p1GArrowSTKC
- @ GArrowTikZ.GArrowTikZ $dGArrowSTKC_aHg } in
- let {
- $dGArrow_aHs
- :: GHC.HetMet.GArrow.GArrow
- GArrowTikZ.GArrowTikZ
- (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
- [LclId]
- $dGArrow_aHs =
- GHC.HetMet.GArrow.$p1GArrowDrop
- @ GArrowTikZ.GArrowTikZ
- @ (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- @ (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
- $dGArrowDrop_aHl } in
- let {
- $dCategory_aHt :: Control.Category.Category GArrowTikZ.GArrowTikZ
- [LclId]
- $dCategory_aHt =
- GHC.HetMet.GArrow.$p1GArrow
- @ GArrowTikZ.GArrowTikZ
- @ (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- @ (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
- $dGArrow_aHs } in
- let {
- $dGArrow_aLr
- :: GHC.HetMet.GArrow.GArrow
- GArrowTikZ.GArrowTikZ
- (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- ()
- [LclId]
- $dGArrow_aLr =
- $dGArrow_aHs
- `cast` (GHC.HetMet.GArrow.T:GArrow
- GArrowTikZ.GArrowTikZ
- (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- co_aLf
- :: GHC.HetMet.GArrow.T:GArrow
- GArrowTikZ.GArrowTikZ
- (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
- ~
- GHC.HetMet.GArrow.T:GArrow
- GArrowTikZ.GArrowTikZ
- (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- ()) } in
- let {
- $dGArrow_aLs
- :: GHC.HetMet.GArrow.GArrow GArrowTikZ.GArrowTikZ (,) ()
- [LclId]
- $dGArrow_aLs =
- $dGArrow_aLr
- `cast` (GHC.HetMet.GArrow.T:GArrow GArrowTikZ.GArrowTikZ co_aLg ()
- :: GHC.HetMet.GArrow.T:GArrow
- GArrowTikZ.GArrowTikZ
- (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- ()
- ~
- GHC.HetMet.GArrow.T:GArrow GArrowTikZ.GArrowTikZ (,) ()) } in
- let {
- $dGArrowDrop_aLp
- :: GHC.HetMet.GArrow.GArrowDrop
- GArrowTikZ.GArrowTikZ
- (,)
- (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
- [LclId]
- $dGArrowDrop_aLp =
- $dGArrowDrop_aHl
- `cast` (GHC.HetMet.GArrow.T:GArrowDrop
- GArrowTikZ.GArrowTikZ
- co_aLg
- (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
- :: GHC.HetMet.GArrow.T:GArrowDrop
- GArrowTikZ.GArrowTikZ
- (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
- (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
- ~
- GHC.HetMet.GArrow.T:GArrowDrop
- GArrowTikZ.GArrowTikZ
- (,)
- (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)) } in
- let {
- $dGArrowDrop_aLq
- :: GHC.HetMet.GArrow.GArrowDrop GArrowTikZ.GArrowTikZ (,) ()
- [LclId]
- $dGArrowDrop_aLq =
- $dGArrowDrop_aLp
- `cast` (GHC.HetMet.GArrow.T:GArrowDrop
- GArrowTikZ.GArrowTikZ (,) co_aLf
- :: GHC.HetMet.GArrow.T:GArrowDrop
- GArrowTikZ.GArrowTikZ
- (,)
- (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
- ~
- GHC.HetMet.GArrow.T:GArrowDrop GArrowTikZ.GArrowTikZ (,) ()) } in
- let {
- @ co_aHh::GHC.Types.Int ~ GHC.Types.Int
- co_aHh = TYPE sym co_aLt } in
- (GArrowTikZ.$WTikZ_const (GHC.Types.I# 12))
- `cast` (GArrowTikZ.GArrowTikZ () co_aHh
- :: GArrowTikZ.GArrowTikZ () GHC.Types.Int
- ~
- GArrowTikZ.GArrowTikZ () GHC.Types.Int)))); } in
- main_aHj
-
-:Main.main :: GHC.Types.IO ()
-[LclIdX]
-:Main.main = GHC.TopHandler.runMainIO @ () Main.main
-end Rec }
-
-
-
-
-==================== Desugar ====================
-Main.foo
- :: forall (tv_~N6 :: * -> * -> *) tv_~N7.
- GHC.HetMet.Private.PGArrow
- tv_~N6 (GHC.HetMet.GArrow.GArrowUnit tv_~N6) tv_~N7
- -> GHC.HetMet.Private.PGArrow
- tv_~N6 (GHC.HetMet.GArrow.GArrowUnit tv_~N6) tv_~N7
-[LclId]
-Main.foo =
- \ (@ tv_~N6::* -> * -> *)
- (@ tv_~N7)
- (ev_~N8
- :: GHC.HetMet.Private.PGArrow
- tv_~N6 (GHC.HetMet.GArrow.GArrowUnit tv_~N6) tv_~N7) ->
- let {
- ev_~N9
- :: GHC.HetMet.Private.PGArrow
- tv_~N6
- (GHC.HetMet.GArrow.GArrowUnit tv_~N6)
- (GHC.HetMet.GArrow.GArrowUnit tv_~N6)
- [LclId]
- ev_~N9 =
- GHC.HetMet.Private.pga_id
- @ tv_~N6 @ (GHC.HetMet.GArrow.GArrowUnit tv_~N6) } in
- let {
- ev_~Na
- :: GHC.HetMet.Private.PGArrow
- tv_~N6 (GHC.HetMet.GArrow.GArrowUnit tv_~N6) tv_~N7
- [LclId]
- ev_~Na =
- let {
- ev_~Nh
- :: GHC.HetMet.Private.PGArrow
- tv_~N6
- (GHC.HetMet.GArrow.GArrowUnit tv_~N6)
- (GHC.HetMet.GArrow.GArrowUnit tv_~N6)
- [LclId]
- ev_~Nh =
- GHC.HetMet.Private.pga_id
- @ tv_~N6 @ (GHC.HetMet.GArrow.GArrowUnit tv_~N6) } in
- let {
- ev_~Ni
- :: GHC.HetMet.Private.PGArrow
- tv_~N6 (GHC.HetMet.GArrow.GArrowUnit tv_~N6) tv_~N7
- [LclId]
- ev_~Ni = ev_~N8 } in
- let {
- ev_~Nj
- :: GHC.HetMet.Private.PGArrow
- tv_~N6
- (GHC.HetMet.GArrow.GArrowUnit tv_~N6)
- (GHC.HetMet.GArrow.GArrowUnit tv_~N6)
- [LclId]
- ev_~Nj =
- GHC.HetMet.Private.pga_drop
- @ tv_~N6 @ (GHC.HetMet.GArrow.GArrowUnit tv_~N6) } in
- GHC.HetMet.Private.pga_comp
- @ tv_~N6
- @ (GHC.HetMet.GArrow.GArrowUnit tv_~N6)
- @ (GHC.HetMet.GArrow.GArrowUnit tv_~N6)
- @ tv_~N7
- ev_~Nj
- ev_~Ni } in
- GHC.HetMet.Private.pga_comp
- @ tv_~N6
- @ (GHC.HetMet.GArrow.GArrowUnit tv_~N6)
- @ (GHC.HetMet.GArrow.GArrowUnit tv_~N6)
- @ tv_~N7
- ev_~N9
- ev_~Na
-
-Main.maincoercionKind
- base:GHC.HetMet.GArrow.GArrowUnit{tc 02y}
- main:GArrowTikZ.GArrowTikZ{tc roV}
- ~
- ghc-prim:GHC.Unit.(){(w) tc 40}
-ghc-stage2: coreTypeToWeakType
- hit a bare EqPred
| TCoerc _ t1 t2 t => TCoerc (flatten_rawtype t1) (flatten_rawtype t2) (flatten_rawtype t)
| TArrow => TArrow
| TCode ec e => let e' := flatten_rawtype e
- in ga_mk_raw ec (unleaves' (take_arg_types e')) [drop_arg_types e']
+ in ga_mk_raw ec (unleaves_ (take_arg_types e')) [drop_arg_types e']
| TyFunApp tfc kl k lt => TyFunApp tfc kl k (flatten_rawtype_list _ lt)
end
with flatten_rawtype_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
(mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
(mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) @@ nil]]
with
+ | RId a => let case_RId := tt in ga_id _ _ _ _ _
| RCanL a => let case_RCanL := tt in ga_uncancell _ _ _ _ _
| RCanR a => let case_RCanR := tt in ga_uncancelr _ _ _ _ _
| RuCanL a => let case_RuCanL := tt in ga_cancell _ _ _ _ _
match r as R in Arrange A B return
Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
(mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
+ | RId a => let case_RId := tt in RId _
| RCanL a => let case_RCanL := tt in RCanL _
| RCanR a => let case_RCanR := tt in RCanR _
| RuCanL a => let case_RuCanL := tt in RuCanL _
apply nd_rule.
apply RArrange.
induction r; simpl.
+ apply RId.
apply RCanL.
apply RCanR.
apply RuCanL.
apply IHsucc2.
Defined.
+ Definition arrange_empty_tree : forall {T}{A}(q:Tree A)(t:Tree ??T),
+ t = mapTree (fun _:A => None) q ->
+ Arrange t [].
+ intros T A q.
+ induction q; intros.
+ simpl in H.
+ rewrite H.
+ apply RId.
+ simpl in *.
+ destruct t; try destruct o; inversion H.
+ set (IHq1 _ H1) as x1.
+ set (IHq2 _ H2) as x2.
+ eapply RComp.
+ eapply RRight.
+ rewrite <- H1.
+ apply x1.
+ eapply RComp.
+ apply RCanL.
+ rewrite <- H2.
+ apply x2.
+ Defined.
+
+(* Definition unarrange_empty_tree : forall {T}{A}(t:Tree ??T)(q:Tree A),
+ t = mapTree (fun _:A => None) q ->
+ Arrange [] t.
+ Defined.*)
+
+ Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
+ sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
+ intro T.
+ refine (fix foo t :=
+ match t with
+ | T_Leaf x => _
+ | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
+ end).
+ intros.
+ destruct x.
+ right; apply tt.
+ left.
+ exists (T_Leaf tt).
+ auto.
+ destruct b1'.
+ destruct b2'.
+ destruct s.
+ destruct s0.
+ subst.
+ left.
+ exists (x,,x0).
+ reflexivity.
+ right; auto.
+ right; auto.
+ Defined.
+
Definition arrange_esc : forall Γ Δ ec succ t,
ND Rule
[Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t @@ nil]]
[Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),,
[(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil] |- [t @@ nil]].
intros.
- unfold drop_lev.
set (@arrange _ succ (levelMatch (ec::nil))) as q.
+ set (@drop_lev Γ (ec::nil) succ) as q'.
+ assert (@drop_lev Γ (ec::nil) succ=q') as H.
+ reflexivity.
+ unfold drop_lev in H.
+ unfold mkDropFlags in H.
+ rewrite H in q.
+ clear H.
set (arrangeMap _ _ flatten_leveled_type q) as y.
eapply nd_comp.
eapply nd_rule.
eapply RArrange.
apply y.
- idtac.
clear y q.
+ set (mapOptionTree flatten_leveled_type (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ))) as q.
+ destruct (decide_tree_empty q); [ idtac | apply (Prelude_error "escapifying open code not yet supported") ].
+ destruct s.
+
+ simpl.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
+ set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''.
+ eapply nd_comp; [ idtac | eapply nd_rule; apply q'' ].
+ clear q''.
+ eapply nd_comp; [ apply nd_rlecnac | idtac ].
+ apply nd_prod.
+ apply nd_rule.
+ apply RArrange.
+ eapply RComp; [ idtac | apply RCanR ].
+ apply RLeft.
+ apply (@arrange_empty_tree _ _ _ _ e).
+
+ eapply nd_comp.
+ eapply nd_rule.
+ eapply (@RVar Γ Δ t nil).
+ apply nd_rule.
+ apply RArrange.
+ eapply RComp.
+ apply RuCanL.
+ apply RRight.
+ apply RWeak.
+(*
+ eapply decide_tree_empty.
+
+ simpl.
+ set (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ)) as escapified.
+ destruct (decide_tree_empty escapified).
+
induction succ.
destruct a.
+ unfold drop_lev.
destruct l.
simpl.
unfold mkDropFlags; simpl.
apply RLeft.
apply RWeak.
apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
+*)
Defined.
Lemma mapOptionTree_distributes
reflexivity.
Qed.
- Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
- sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
- intro T.
- refine (fix foo t :=
- match t with
- | T_Leaf x => _
- | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
- end).
- intros.
- destruct x.
- right; apply tt.
- left.
- exists (T_Leaf tt).
- auto.
- destruct b1'.
- destruct b2'.
- destruct s.
- destruct s0.
- subst.
- left.
- exists (x,,x0).
- reflexivity.
- right; auto.
- right; auto.
- Defined.
-
Lemma unlev_relev : forall {Γ}(t:Tree ??(HaskType Γ ★)) lev, mapOptionTree unlev (t @@@ lev) = t.
intros.
induction t.
= @ga_mk Γ (v2t ec)
(mapOptionTree flatten_type (take_arg_types_as_tree t))
[ flatten_type (drop_arg_types_as_tree t)].
-
intros.
unfold flatten_type at 1.
simpl.
unfold ga_mk.
+ apply phoas_extensionality.
+ intros.
unfold v2t.
- admit. (* BIG HUGE CHEAT FIXME *)
+ unfold ga_mk_raw.
+ unfold ga_mk_tree.
+ rewrite <- mapOptionTree_compose.
+ unfold take_arg_types_as_tree.
+ simpl.
+ replace (flatten_type (drop_arg_types_as_tree t) tv ite)
+ with (drop_arg_types (flatten_rawtype (t tv ite))).
+ replace (unleaves_ (take_arg_types (flatten_rawtype (t tv ite))))
+ with ((mapOptionTree (fun x : HaskType Γ ★ => flatten_type x tv ite)
+ (unleaves_
+ (take_trustme (count_arg_types (t (fun _ : Kind => unit) (ite_unit Γ)))
+ (fun TV : Kind → Type => take_arg_types ○ t TV))))).
+ reflexivity.
+ unfold flatten_type.
+ clear hetmet_flatten.
+ clear hetmet_unflatten.
+ clear hetmet_id.
+ clear gar.
+ set (t tv ite) as x.
+ admit.
+ admit.
Qed.
Definition flatten_proof :
(* Figure 3, production $\vdash_E$, Uniform rules *)
Inductive Arrange {T} : Tree ??T -> Tree ??T -> Type :=
+| RId : forall a , Arrange a a
| RCanL : forall a , Arrange ( [],,a ) ( a )
| RCanR : forall a , Arrange ( a,,[] ) ( a )
| RuCanL : forall a , Arrange ( a ) ( [],,a )
Arrange (mapOptionTree f Σ₁) (mapOptionTree f Σ₂).
intros.
induction X; simpl.
+ apply RId.
apply RCanL.
apply RCanR.
apply RuCanL.
match r with
| RLeft _ _ _ r => nd_uruleToRawLatexMath r
| RRight _ _ _ r => nd_uruleToRawLatexMath r
+ | RId _ => "Id"
| RCanL _ => "CanL"
| RCanR _ => "CanR"
| RuCanL _ => "uCanL"
with
| RLeft h c ctx r => let case_RLeft := tt in (fun e => _) (urule2expr _ _ _ r)
| RRight h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ r)
+ | RId a => let case_RId := tt in _
| RCanL a => let case_RCanL := tt in _
| RCanR a => let case_RCanR := tt in _
| RuCanL a => let case_RuCanL := tt in _
| RComp a b c f g => let case_RComp := tt in (fun e1 e2 => _) (urule2expr _ _ _ f) (urule2expr _ _ _ g)
end); clear urule2expr; intros.
+ destruct case_RId.
+ apply X.
+
destruct case_RCanL.
simpl; unfold ujudg2exprType; intros.
simpl in X.
| a::b => mkArrows b (a ---> t)
end.
+(*
Fixpoint unleaves_ {Γ}(t:Tree ??(LeveledHaskType Γ ★))(l:list (HaskType Γ ★)) lev : Tree ??(LeveledHaskType Γ ★) :=
match l with
| nil => t
| a::b => unleaves_ (t,,[a @@ lev]) b lev
end.
+*)
+ (* weak inverse of "leaves" *)
+ Fixpoint unleaves_ {A:Type}(l:list A) : Tree (option A) :=
+ match l with
+ | nil => []
+ | (a::nil) => [a]
+ | (a::b) => [a],,(unleaves_ b)
+ end.
(* rules of skolemized proofs *)
Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end.
end)
end.
+ Axiom phoas_extensionality : forall Γ Q (f g:forall TV, InstantiatedTypeEnv TV Γ -> Q TV),
+ (forall tv ite, f tv ite = g tv ite) -> f=g.
+
Definition take_arg_types_as_tree {Γ}(ht:HaskType Γ ★) : Tree ??(HaskType Γ ★ ) :=
- unleaves
+ unleaves_
(take_trustme
(count_arg_types (ht _ (ite_unit _)))
(fun TV ite => take_arg_types (ht TV ite))).
Implicit Arguments take_arg_types_as_tree [[Γ]].
Implicit Arguments drop_arg_types_as_tree [[Γ]].
- Lemma take_works : forall {Γ}(t1 t2:HaskType Γ ★),
- take_arg_types_as_tree (t1 ---> t2) = [t1],,(take_arg_types_as_tree t2).
+ Definition take_arrange : forall {Γ} (tx te:HaskType Γ ★) lev,
+ Arrange ([tx @@ lev],, take_arg_types_as_tree te @@@ lev)
+ (take_arg_types_as_tree (tx ---> te) @@@ lev).
intros.
- unfold take_arg_types_as_tree at 1.
- simpl.
- admit.
- Qed.
+ destruct (eqd_dec ([tx],, take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
+ rewrite <- e.
+ simpl.
+ apply RId.
+ unfold take_arg_types_as_tree.
+ Opaque take_arg_types_as_tree.
+ simpl.
+ destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))).
+ simpl.
+ replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite).
+ apply RCanR.
+ apply phoas_extensionality.
+ reflexivity.
+ apply (Prelude_error "should not be possible").
+ Defined.
+ Transparent take_arg_types_as_tree.
+
+ Definition take_unarrange : forall {Γ} (tx te:HaskType Γ ★) lev,
+ Arrange (take_arg_types_as_tree (tx ---> te) @@@ lev)
+ ([tx @@ lev],, take_arg_types_as_tree te @@@ lev).
+ intros.
+ destruct (eqd_dec ([tx],, take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
+ rewrite <- e.
+ simpl.
+ apply RId.
+ unfold take_arg_types_as_tree.
+ Opaque take_arg_types_as_tree.
+ simpl.
+ destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))).
+ simpl.
+ replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite).
+ apply RuCanR.
+ apply phoas_extensionality.
+ reflexivity.
+ apply (Prelude_error "should not be possible").
+ Defined.
+ Transparent take_arg_types_as_tree.
Lemma drop_works : forall {Γ}(t1 t2:HaskType Γ ★),
drop_arg_types_as_tree (t1 ---> t2) = (drop_arg_types_as_tree t2).
simpl.
apply RLam.
simpl.
- rewrite take_works.
rewrite drop_works.
apply nd_rule.
apply SFlat.
apply RArrange.
+ eapply RComp.
apply RCossa.
+ apply RLeft.
+ apply take_arrange.
destruct case_RCast.
simpl.
apply nd_rule.
apply SFlat.
apply RApp.
- rewrite take_works.
rewrite drop_works.
set (check_hof tx) as hof_tx.
destruct hof_tx; [ apply (Prelude_error "attempt tp apply a higher-order function at depth>0") | idtac ].
apply SFlat.
apply RArrange.
apply RCanR.
- eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
- apply nd_rule; apply SFlat; apply RArrange; apply RLeft; eapply RExch.
+ apply nd_rule.
+ apply SFlat.
+ apply RArrange.
+ eapply RComp; [ idtac | eapply RAssoc ].
+ apply RLeft.
+ eapply RComp; [ idtac | apply RExch ].
+ apply take_unarrange.
destruct case_RLet.
simpl.
projects / coq-hetmet.git / commitdiff