content: {-# LANGUAGE CPP #-}
  
  -- #define NoOptimizeCircuit
  
  -- #define NoHashCons
  
  -- #define NoIfBotOpt
  -- #define NoIdempotence
  
  -- -- Improves hash consing, but can obscure equivalent circuits
  -- #define NoCommute
  
  -- #define NoBusLabel
  
  #define MealyToArrow
  
  -- -- Whether a delay/cons element is considered further from input
  -- #define ShallowDelay
  
  -- #define NoMend
  
  {-# LANGUAGE TypeFamilies, TypeOperators, ConstraintKinds #-}
  {-# LANGUAGE FlexibleInstances, FlexibleContexts, MultiParamTypeClasses #-}
  {-# LANGUAGE ViewPatterns, TupleSections #-}
  {-# LANGUAGE GeneralizedNewtypeDeriving, StandaloneDeriving #-}
  {-# LANGUAGE ExistentialQuantification, TypeSynonymInstances, GADTs #-}
  {-# LANGUAGE Rank2Types, ScopedTypeVariables #-}
  {-# LANGUAGE UndecidableInstances #-} -- see below
  {-# LANGUAGE LambdaCase #-}
  {-# LANGUAGE PolyKinds #-}
  {-# LANGUAGE DataKinds #-} -- for LU & BU
  {-# LANGUAGE PatternSynonyms #-}
  {-# LANGUAGE RecursiveDo #-}
  {-# LANGUAGE DeriveFunctor, DeriveDataTypeable #-}
  {-# LANGUAGE TypeApplications, AllowAmbiguousTypes #-}
  {-# LANGUAGE InstanceSigs #-}
  {-# LANGUAGE UndecidableSuperClasses #-}  -- GenBuses
  
  -- TODO: trim language extensions
  
  #ifdef ChurchSums
  {-# LANGUAGE LiberalTypeSynonyms, ImpredicativeTypes, EmptyDataDecls #-}
  #endif
  
  {-# LANGUAGE NoStarIsType #-}
  
  {-# OPTIONS_GHC -Wall #-}
  {-# OPTIONS_GHC -fno-warn-orphans #-} -- for OkayArr
  {-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
  
  -- {-# OPTIONS_GHC -fdefer-typed-holes #-}  -- TEMP
  -- {-# OPTIONS_GHC -fdefer-type-errors #-}  -- TEMP
  
  -- This module compiles pretty slowly. Some of my pattern matching style led to
  -- the following warning:
  --
  --        Pattern match checker exceeded (2000000) iterations in
  --        a case alternative. (Use -fmax-pmcheck-iterations=n
  --        to set the maximun number of iterations to n)
  --
  -- I've simplified my style by replacing uses of the Eql macro by explicit
  -- equality checks. To find at least some problematic definitions, lower
  -- -fmax-pmcheck-iterations from default of 2000000. I'd like to simplify
  -- further. Ideally, use constructor pattern matching in the rewrites, instead
  -- of comparing strings.
  
  {-# OPTIONS_GHC -fmax-pmcheck-iterations=1000000 #-}
  
  {-# OPTIONS_GHC -fno-warn-unused-imports #-} -- TEMP
  {-# OPTIONS_GHC -fno-warn-unused-binds   #-} -- TEMP
  
  ----------------------------------------------------------------------
  -- |
  -- Module      :  ConCat.Circuit
  -- Copyright   :  (c) 2016 Conal Elliott
  -- License     :  BSD3
  --
  -- Maintainer  :  conal@conal.net
  -- Stability   :  experimental
  --
  -- Circuit representation
  ----------------------------------------------------------------------
  
  module ConCat.Circuit
    ( CircuitM, (:>)
    , Bus(..),Comp(..),Input,Output, Ty(..), busTy, Source(..), Template(..)
    , GenBuses(..), GS, genBusesRep', tyRep
    -- , delayCRep, unDelayName
    , namedC, constC -- , constS
    , genUnflattenB'
    , SourceToBuses(..), CompS(..), simpleComp
    , mkGraph
    , Attr
    , graphDot, writeDot, displayDot,Name,Report,Graph
    -- , simpleComp
    , tagged
    , systemSuccess
    -- For AbsTy
    , BusesM, abstB,abstC,reprC,Buses(..)
    , OkCAR
    -- , Ty(..)
    ) where
  
  import Prelude hiding (id,(.),curry,uncurry,const,sequence,zip)
  
  import Data.Monoid ({-mempty,-}(<>),Sum,Product,All,Any)
  -- import Data.Newtypes.PrettyDouble
  -- import Data.Functor ((<$>))
  import Control.Applicative ({-Applicative(..),-}liftA2)
  import Control.Monad (unless)
  import Control.Arrow (arr,Kleisli(..))
  import Data.Foldable ({-foldMap,-}toList)
  import qualified GHC.Generics as G
  import Data.Functor.Classes (Show1,showsPrec1)
  import Data.Void (Void)
  import Data.Function (on)
  import Data.Maybe (fromMaybe,isJust,maybeToList)
  import Data.List (intercalate,group,sort,stripPrefix)
  import Data.Char (isAscii)
  import Data.Complex (Complex)
  import Data.Proxy
  import GHC.TypeLits -- (natVal)
  #ifndef MealyToArrow
  import Data.List (partition)
  #endif
  import Data.Map (Map)
  import qualified Data.Map as M  -- accidental qualifier clash with mtl. Change one.
  -- import Data.Set (Set)
  import qualified Data.Set as S
  import Data.Sequence (Seq,singleton)
  import Text.Printf (printf)
  import Debug.Trace (trace)
  -- import Data.Coerce                      -- TODO: imports
  import Unsafe.Coerce
  -- import GHC.Exts (Coercible) -- ,coerce
  import Data.Typeable (TypeRep,Typeable,eqT,cast) -- ,Proxy(..),typeOf
  import Data.Type.Equality ((:~:)(..))
  import GHC.Types (Constraint)
  import Data.Kind (Type)
  
  import Data.Constraint (Dict(..),(:-)(..),(\\))
  import Data.Pointed (Pointed)
  import Data.Key (Zip(..))
  import Data.Distributive (Distributive)
  import Data.Distributive (distribute)
  import Data.Functor.Rep (Representable(tabulate,index))
  import qualified Data.Functor.Rep as R
  
  import qualified System.Info as SI
  import System.Process (system) -- ,readProcess
  import System.Directory (createDirectoryIfMissing)
  import System.Exit (ExitCode(ExitSuccess))
  
  #define WithArr
  
  #ifdef VectorSized
  import GHC.TypeLits (Nat,KnownNat)
  import Data.Vector.Sized (Vector)
  #endif
  #ifdef WithArr
  import ConCat.TArr (HasFin',Arr)
  #endif
  import ConCat.Known
  
  -- mtl
  import Control.Monad.State (State,execState,StateT)
  
  -- For AbsTy
  import qualified Data.Functor.Identity as M
  import qualified Control.Monad.Trans.Reader as M
  import qualified Control.Monad.Trans.Writer as M
  import qualified Control.Monad.State as M
  
  -- import TypeUnary.Vec hiding (get)
  
  import ConCat.Misc ((:*),(:+),Unop,Binop,Yes1,typeR,transpose)
  -- import ConCat.Complex (Complex(..))
  import ConCat.Rep
  import ConCat.Additive (Additive(..),Add)
  import qualified ConCat.Category
  import ConCat.AltCat  -- for AbsTy
  -- import ConCat.AltCat (Uncurriable(..),funIf,repIf,unitIf,prodIf,Finite)
  
  {--------------------------------------------------------------------
      Buses
  --------------------------------------------------------------------}
  
  -- Component (primitive) type
  data Ty = Void | Unit | Bool | Int | Integer | Float | Double
          | Finite Integer  -- Remove?
          | Vector Integer Ty
          | Prod Ty Ty
          | Sum Ty Ty
          | Fun Ty Ty
    deriving (Eq,Ord)
  
  instance Show Ty where
    showsPrec _ Void    = showString "Void"
    showsPrec _ Unit    = showString "()"
    showsPrec _ Bool    = showString "Bool"
    showsPrec _ Int     = showString "Int"
    showsPrec _ Integer = showString "Integer"
    showsPrec _ Float   = showString "Float"
    showsPrec _ Double  = showString "Double" -- "R"
    showsPrec p (Sum a b) = showParen (p >= 6) $
      showsPrec 6 a . showString " + " . showsPrec 6 b
    showsPrec p (Prod a b) = showParen (p >= 7) $
      showsPrec 7 a . showString " × " . showsPrec 7 b
    showsPrec p (Finite n) = showParen (p >= 9) $
      showString "Finite " . showsPrec 9 n
    showsPrec p (Vector n b) = showParen (p >= 9) $
      showString "Vector " . showsPrec 9 n . showString " " . showsPrec 9 b
    showsPrec p (Fun a b) = showParen (p >= 1) $
      showsPrec 1 a . showString " → " . showsPrec 0 b
  
  -- Data bus: component id, output index, type; *or* subgraph ID
  data Bus = Bus CompId Int Ty deriving Show
  
  type Input  = Bus
  type Output = Bus
  
  -- Identifying information for a bus. Faster comparisons without the type.
  busId :: Bus -> (CompId,Int)
  busId (Bus c o _) = (c,o)
  
  busTy :: Bus -> Ty
  busTy (Bus _ _ t) = t
  
  instance Eq  Bus where (==) = (==) `on` busId
  instance Ord Bus where compare = compare `on` busId
  
  -- type Sources = [Source]
  
  -- | An information source: its bus and a description of its construction, which
  -- contains the primitive and argument sources.
  data Source = forall a b. Source Bus (Template a b) [Source]
  
  pattern PSource :: Bus -> PrimName -> [Source] -> Source
  pattern PSource b p ss = Source b (Prim p) ss
  
  deriving instance Show Source
  
  sourceBus :: Source -> Bus
  sourceBus (Source b _ _) = b
  
  instance Eq  Source where (==) = (==) `on` sourceBus
  instance Ord Source where compare = compare `on` sourceBus
  
  newBus :: Ty -> Int -> CircuitM Bus
  newBus t o = -- trace "newBus" $
                (\ c -> Bus c o t) <$> M.gets fst
  
  newSource ::  Ty -> Template a b -> [Source] -> Int -> CircuitM Source
  newSource t templ ins o = -- trace "newSource" $
                           (\ b -> Source b templ ins) <$> newBus t o
  
  {--------------------------------------------------------------------
      Buses representing a given type
  --------------------------------------------------------------------}
  
  -- | Typed aggregate of buses. @'Buses' a@ carries a value of type @a@.
  -- 'AbstB' is for isomorphic forms. Note: b must not have one of the standard
  -- forms. If it does, we'll get a run-time error when consuming.
  data Buses :: Type -> Type where
    UnitB    :: Buses ()
    PrimB    :: Source -> Buses b
    ProdB    :: Ok2 (:>) a b => Buses a -> Buses b -> Buses (a :* b)
    IxProdB  :: (OkIxProd (:>) h, Show1 h, Foldable h, Ok (:>) a) => h (Buses a) -> Buses (h a)
    -- FunB     :: SubgraphId -> Buses (a -> b)
    ConvertB :: Ok2 (:>) a b => Buses a -> Buses b
    -- AbstB :: Buses (Rep b) -> Buses b
  
  -- deriving instance Show (Buses a) -- not with IxProdB
  
  instance Show (Buses a) where
    showsPrec _ UnitB        = showString "UnitB"
    showsPrec p (PrimB s)    = showsApp1 p "PrimB" s
    showsPrec p (ProdB a b)  = showsApp2 p "ProdB" a b
    showsPrec p (IxProdB as) = showsAppF p "IxProdB " as
    showsPrec p (ConvertB a) = showsApp1 p "ConvertB " a
  
  -- TODO: use operations from Data.Functor.Classes, such as showsUnaryWith.
  -- Give a Show1 instance for Buses in the style below, and then use
  --
  --   showsPrec1 :: (Show1 f, Show a) => Int -> f a -> ShowS
  
  {- From Data.Functor.Classes:
  
  > data T f a = Zero a | One (f a) | Two a (f a)
  
  a standard 'Read1' instance may be defined as
  
  > instance (Read1 f) => Read1 (T f) where
  >     liftReadsPrec rp rl = readsData $
  >         readsUnaryWith rp "Zero" Zero `mappend`
  >         readsUnaryWith (liftReadsPrec rp rl) "One" One `mappend`
  >         readsBinaryWith rp (liftReadsPrec rp rl) "Two" Two
  
  and the corresponding 'Show1' instance as
  
  > instance (Show1 f) => Show1 (T f) where
  >     liftShowsPrec sp _ d (Zero x) =
  >         showsUnaryWith sp "Zero" d x
  >     liftShowsPrec sp sl d (One x) =
  >         showsUnaryWith (liftShowsPrec sp sl) "One" d x
  >     liftShowsPrec sp sl d (Two x y) =
  >         showsBinaryWith sp (liftShowsPrec sp sl) "Two" d x y
  
  -}
  
  appParen :: Int -> Unop ShowS
  appParen p = showParen (p >= 10)
  
  shap :: Show a => a -> ShowS
  shap a = showChar ' ' . showsPrec 10 a
  
  showsApp1 :: Show a => Int -> String -> a -> ShowS
  showsApp1 p f a = appParen p $ showString f . shap a
  
  showsApp2 :: (Show a, Show b) => Int -> String -> a -> b -> ShowS
  showsApp2 p f a b = appParen p $ showString f . shap a . shap b
  
  showsAppF :: (Show1 h, Show a) => Int -> String -> h a -> ShowS
  showsAppF p f as = appParen p $ showString f . showChar ' ' . showsPrec1 10 as
  
  -- TODO: move these showsApp* functions elsewhere.
  
  #if 0
  
  -- Currently unused.
  instance Eq (Buses a) where
    UnitB      == UnitB       = True
    PrimB s    == PrimB s'    = s == s'
    ProdB a b  == ProdB a' b' = a == a' && b == b'
    -- FunB _     == FunB _      = False             -- TODO: reconsider
    ConvertB a == ConvertB b  = case cast a of
                                  Just a' -> a' == b
                                  Nothing -> False
    _          == _           = False
  
  -- If I need Eq, handle ConvertB. I'll probably have to switch to heterogeneous
  -- equality, perhaps via `TestEquality` in `Data.Type.Equality`.
  
  #endif
  
  genBuses :: GenBuses b => Template a b -> [Source] -> CircuitM (Buses b)
  genBuses templ ins = -- trace ("genBuses " ++ show templ ++ " " ++ show ins) $
                       M.evalStateT (genBuses' templ ins) 0
  
  type BusesM = StateT Int CircuitM
  
  class GenBuses a where
    genBuses' :: Template u v -> [Source] -> BusesM (Buses a)
    -- delay :: a -> (a :> a)
    ty :: Ty
    unflattenB' :: State [Source] (Buses a)
  
  type GS a = (GenBuses a, Show a)
  
  genBus :: (Source -> Buses a) -> Ty
         -> Template u v -> [Source] -> BusesM (Buses a)
  -- Without this @seq (show t)@, I'm getting non-termination with
  -- `id @(Vector 4 Bool :* Bool)`. I don't know why @seq t@ isn't enough.
  genBus wrap t templ ins = seq (show t) $
                            -- seq t $
                            -- trace ("genBus " ++ show t) $
                            do o <- M.get
                               src <- M.lift (newSource t templ ins o)
                               M.put (o+1)
                               return (wrap src)
  
  
  unflattenB :: GenBuses a => [Source] -> Buses a
  unflattenB sources | [] <- rest = a
                     | otherwise  = error ("unflattenB: extra sources " ++ show rest)
   where
     (a,rest) = M.runState unflattenB' sources
  
  -- TODO: Remove this instance when we stop needing GenBuses for Vector index
  instance GenBuses Void where
    genBuses' = error "genBuses' for Void"
    ty = Void
    unflattenB' = error "unflattenB' for Void"
  
  instance GenBuses () where
    genBuses' _ _ = return UnitB
    -- delay () = id
    ty = Unit
    unflattenB' = return UnitB
  
  -- delayPrefix :: String
  -- delayPrefix = "Cons "
  --               -- "delay "
  
  -- delayName :: String -> String
  -- delayName = (delayPrefix ++)
  
  -- unDelayName :: String -> Maybe String
  -- unDelayName = stripPrefix delayPrefix
  
  -- isDelayTemplate :: Template a b -> Bool
  -- isDelayTemplate = isJust . unDelayName . primName
  
  genPrimBus :: forall a u v. GenBuses a => Template u v -> [Source] -> BusesM (Buses a)
  genPrimBus = genBus PrimB (ty @a)
  
  -- TODO: Combine genBus and genPrimBus.
  
  -- flattenB :: GenBuses a => Buses a -> [Source]
  -- flattenB = toList . flat
  --  where
  --    flat :: forall a. GenBuses a => Buses a -> Seq Source
  --    flat UnitB        = mempty
  --    flat (PrimB s)    = singleton s
  --    flat (ProdB a b)  = flat a <> flat b
  --    flat (ConvertB b) = flat b
  
  unflattenPrimB :: State [Source] (Buses a)
  unflattenPrimB = do ss0 <- M.get
                      case ss0 of
                        s:ss -> do M.put ss
                                   return (PrimB s)
                        []   -> error "unflattenPrimB: expected non-empty list"
                                  -- TODO: can we do better than raise an error here?
  
  instance GenBuses Bool where
    genBuses' = genPrimBus
    -- delay = primDelay
    ty = Bool
    unflattenB' = unflattenPrimB
  
  instance GenBuses Int  where
    genBuses' = genPrimBus
    -- delay = primDelay
    ty = Int
    unflattenB' = unflattenPrimB
  
  instance GenBuses Integer  where
    genBuses' = genPrimBus
    -- delay = primDelay
    ty = Integer
    unflattenB' = unflattenPrimB
  
  instance GenBuses Float  where
    genBuses' = genPrimBus
    -- delay = primDelay
    ty = Float
    unflattenB' = unflattenPrimB
  
  instance GenBuses Double  where
    genBuses' = genPrimBus
    -- delay = primDelay
    ty = Double
    unflattenB' = unflattenPrimB
  
  instance KnownNat n => GenBuses (Finite n) where
    genBuses' = genPrimBus
    -- delay = primDelay
    ty = Finite (natVal (Proxy @n))
    unflattenB' = unflattenPrimB
  
  instance (KnownNat n, GenBuses b) => GenBuses (Vector n b)  where
    genBuses' = genPrimBus
    -- delay = primDelay
    ty = Vector (natVal (Proxy @n)) (ty @b)
    unflattenB' = unflattenPrimB
  
  -- TODO: perhaps give default definitions for genBuses', delay, and unflattenB',
  -- and eliminate the definitions in Bool,...,Double,Vector a.
  
  
  instance (GenBuses a, GenBuses b) => GenBuses (a :+ b)  where
    genBuses' = genPrimBus
    -- delay = primDelay
    ty = Sum (ty @a) (ty @b)
    unflattenB' = unflattenPrimB
  
  instance (GenBuses a, GenBuses b) => GenBuses (a :* b) where
    genBuses' templ ins =
      -- trace ("genBuses' @ " ++ show (ty (undefined :: a :* b))) $
      ProdB <$> genBuses' templ ins <*> genBuses' templ ins
    -- delay (a,b) = delay a *** delay b
    ty = Prod (ty @a) (ty @b)
    unflattenB' = liftA2 ProdB unflattenB' unflattenB'
  
  instance (GenBuses a, GenBuses b) => GenBuses (a -> b) where
    genBuses' = genPrimBus
    -- delay = error "delay for functions: not yet implemented"
    ty = ty @a `Fun` ty @b
    unflattenB' = unflattenPrimB
  
  flattenB :: Buses a -> [Source]
  flattenB = toList . flat
   where
     flat :: Buses c -> Seq Source
     flat UnitB        = mempty
     flat (PrimB s)    = singleton s
     flat (ProdB a b)  = flat a <> flat b
     flat (IxProdB as) = foldMap flat as
     flat (ConvertB b) = flat b
  
  badBuses :: forall a x. Ok (:>) a => String -> Buses a -> x
  badBuses nm bs = error (nm ++ " got unexpected bus " ++ show bs)
  
  unProdB :: Ok2 (:>) a b => Buses (a :* b) -> Buses a :* Buses b
  unProdB (ProdB a b)            = (a,b)
  unProdB (ConvertB (ProdB c d)) = (convertB c, convertB d)
  unProdB b                      = badBuses "unProdB" b
  
  exlB :: Ok2 (:>) a b => Buses (a :* b) -> Buses a
  exlB = fst . unProdB
  
  exrB :: Ok2 (:>) a b => Buses (a :* b) -> Buses b
  exrB = snd . unProdB
  
  type OkCAR a = Ok2 (:>) a (Rep a)
  
  -- TODO: if this experiment works out, eliminate AbstB, and rename ConvertB.
  abstB :: OkCAR a => Buses (Rep a) -> Buses a
  abstB = convertB
  
  reprB :: OkCAR a => Buses a -> Buses (Rep a)
  reprB = convertB
  
  convertC :: forall a b. Ok2 (:>) a b => a :> b
  convertC = C (arr convertB)
  
  convertB :: forall a b. Ok2 (:>) a b => Buses a -> Buses b
  -- convertB a | trace ("convertB " ++ show (typeRep (Proxy :: Proxy (a -> b))) ++ ": " ++ show a ++ "\n") False = undefined
  convertB (ConvertB p) = mkConvertB p  -- coalesce
  convertB a            = mkConvertB a
  
  -- Make a ConvertB if source and target types differ; otherwise id
  mkConvertB :: forall a b. Ok2 (:>) a b => Buses a -> Buses b
  mkConvertB a -- \| Just Refl <- eqT @a @b = a
               | otherwise              = ConvertB a
  
  {--------------------------------------------------------------------
      The circuit monad
  --------------------------------------------------------------------}
  
  type PrimName = String
  
  -- | Primitive of type @a -> b@
  data Template :: Type -> Type -> Type where
    Prim :: PrimName -> Template a b
    Subgraph :: Graph -> BCirc a b -> Template () (a -> b)
  
  -- TODO: maybe add (a :> b) as a Subgraph argument for easier optimization later.
  -- If so, change the Show instance to show only the graph.
  
  instance Show (Template a b) where
    show (Prim p) = p
    show (Subgraph comps _) = "Template:" ++ show comps
  
  -- Transform a subgraph if any. Must preserve meaning, since we leave the
  -- generator unchanged.
  onCompSubgraph :: Unop Graph -> Unop Comp
  onCompSubgraph h (Comp nc (Subgraph g circ) a b) =
    Comp nc (Subgraph (h g) circ) a b
  onCompSubgraph _ c = c
  
  type Id = Int
  
  type CompId = Id
  
  type IdSupply = Id
  
  -- Component: primitive instance with inputs & outputs. Numbered consistently
  -- with dependency partial ordering.
  data Comp = forall a b. Ok (:>) b => Comp CompId (Template a b) (Buses a) (Buses b)
  
  deriving instance Show Comp
  
  compId :: Comp -> CompId
  compId (Comp n _ _ _) = n
  
  instance Eq  Comp where (==) = (==) `on` compId
  instance Ord Comp where compare = compare `on` compId
  
  
  #if !defined NoHashCons
  -- Tracks prim applications (including output type) and reuses per component.
  type CompInfo = Map (PrimName,[Source],Ty) Comp
  #else
  type CompInfo = [Comp]
  #endif
  
  type Graph = [Comp]
  
  -- The circuit monad.
  type CircuitM = State (IdSupply,CompInfo)
  
  genId :: CircuitM Id
  genId = do n <- M.gets fst
             M.modify (first succ)
             return n
  
  type BCirc a b = Buses a -> CircuitM (Buses b)
  
  -- Instantiate a 'Prim'
  genComp :: forall a b. Ok (:>) b => Template a b -> BCirc a b
  #if !defined NoHashCons
  genComp templ a =
    -- trace ("genComp " ++ name ++ ". b == " ++ show (ty @b)) $
    do mb <- M.gets (M.lookup key . snd)
       case mb of
         Just (Comp _ _ _ b') ->
           -- trace ("genComp " ++ name ++ ": hit --> " ++ show b') $
           return (unsafeCoerce b')
         Nothing               ->
           -- trace ("genComp " ++ name ++ ": ins == " ++ show ins) $
           do b <- genBuses templ ins
              -- trace ("genComp: genBuses --> " ++ show b) (return ())
              c <- genId
              let comp = Comp c templ a b
              M.modify (second (M.insert key comp))
              -- trace ("genComp " ++ name ++ ": miss --> " ++ show b) $
              return b
   where
     ins  = flattenB a
     name = show templ
     key  = (name,ins,ty @b)
  
  -- TODO: maybe look for cache hits only on Prim templates.
  
  #else
  genComp templ a = -- trace (printf "genComp %s %s --> %s"
                    --         (show templ) (show a) (show (ty (undefined :: b)))) $
                    do b <- genBuses templ (flattenB a)
                       -- trace (printf "gen'd buses %s" (show b)) (return ())
                       c <- genId
                       M.modify (second (Comp c templ a b :))
                       -- trace (printf "added comp %s" (show (Comp templ a b))) (return ())
                       return b
  #endif
  
  constComp' :: GenBuses b => PrimName -> CircuitM (Buses b)
  constComp' str = -- trace ("constComp' " ++ str) $
                   genComp (Prim ({- "const " ++ -} str)) UnitB
  
  constComp :: GenBuses b => PrimName -> BCirc a b
  constComp str = const (constComp' str)
  
  -- TODO: maybe have constComp and constComp' take a template, and use for curry as well.
  
  constM :: GS b => b -> BCirc a b
  constM b = constComp (constName b)
  
  #if 0
  
  class Tweakable a where
    tweakVal :: a -> a
    tweakVal = id
  
  instance Tweakable ()
  instance Tweakable Bool
  instance Tweakable Int
  instance Tweakable Float  where tweakVal = pullZero 1e-7
  instance Tweakable Double where tweakVal = pullZero 1e-14
  -- TODO: tune the deltas
  
  -- Hack to help eliminate numeric errors involved
  pullZero :: (Ord a, Num a) => a -> a -> a
  pullZero delta a | abs a < delta = 0
                   | otherwise     = a
  
  constName :: (Tweakable b, Show b) => b -> String
  constName = show . tweakVal
  
  #else
  
  constName :: Show b => b -> String
  constName = show
  #endif
  
  
  {--------------------------------------------------------------------
      Circuit category
  --------------------------------------------------------------------}
  
  infixl 1 :>, :+>
  
  -- | Internal representation for '(:>)'.
  type a :+> b = Kleisli CircuitM (Buses a) (Buses b)
  
  -- | Circuit category
  newtype a :> b = C { unC :: a :+> b }
  
  -- type a :> b =~ Buses a -> CircuitM (Buses b)
  
  -- #define ShowRep
  
  #ifdef ShowRep
  
  pattern AbstS :: Source -> Source
  pattern AbstS a <- PSource _ "abst" [a]
  
  -- Temporary alias to mark an experiment
  type STB  r = SourceToBuses r
  type STBR a = STB (Rep a)
  
  instance (OkCAR a, r ~ Rep a, STB r) => RepCat (:>) a r where
    -- reprC = namedC "repr"
    -- The SourceToBuses above is for sourceB
    reprC = primOpt "reprC" $ \ case
             [AbstS a] -> sourceB a
             _         -> nothingA
    abstC = namedC "abst"
  -- TODO: coerceC also.
  #else
  -- Temporary alias to mark an experiment
  type STB  r = (() :: Constraint)
  type STBR a = STB (Rep a)
  
  instance (OkCAR a, r ~ Rep a) => RepCat (:>) a r where
    reprC = C (arr reprB)
    abstC = C (arr abstB)
  #endif
  
  instance Ok2 (:>) a b => CoerceCat (:>) a b where coerceC = convertC
  
  -- instance CoerceCat (:>) where
  --   coerceC = C (arr coerce)
  
  -- pattern CK bc = C (Kleisli bc)
  
  mkCK :: BCirc a b -> (a :> b)
  mkCK = C . Kleisli
  
  unmkCK :: (a :> b) -> BCirc a b
  unmkCK = runKleisli . unC
  
  -- TODO: Eliminate mkCK in favor of CK
  
  inCK :: (BCirc a a' -> BCirc b b')
       -> ((a :> a') -> (b :> b'))
  inCK = mkCK <~ unmkCK
  
  inCK2 :: (BCirc a a' -> BCirc b b' -> BCirc c c')
        -> ((a :> a') -> (b :> b') -> (c :> c'))
  inCK2 = inCK <~ unmkCK
  
  inCKF1 :: Functor h => (h (BCirc a a') -> BCirc b b') -> (h (a :> a') -> (b :> b'))
  inCKF1 = mkCK <~ fmap unmkCK
  
  namedC :: Ok (:>) b => PrimName -> a :> b
  -- namedC name = primOpt name noOpt
  namedC name = -- trace ("namedC " ++ name) $
                mkCK (genComp (Prim name))
  
  type Opt b = [Source] -> CircuitM (Maybe (Buses b))
  
  justA :: Applicative f => a -> f (Maybe a)
  justA = pure . Just
  
  nothingA :: Applicative f => f (Maybe a)
  nothingA = pure Nothing
  
  newComp :: (a :> b) -> Buses a -> CircuitM (Maybe (Buses b))
  newComp cir = fmap Just . unmkCK cir
  
  newComp1 :: SourceToBuses a => (a :> b) -> Source -> CircuitM (Maybe (Buses b))
  newComp1 cir a = newComp cir (toBuses a)
  
  newComp2 :: (SourceToBuses a, SourceToBuses b) =>
              (a :* b :> c) -> Source -> Source -> CircuitM (Maybe (Buses c))
  newComp2 cir a b = newComp cir (ProdB (toBuses a) (toBuses b))
  
  newComp3L :: (SourceToBuses a, SourceToBuses b, SourceToBuses c) =>
               ((a :* b) :* c :> d) -> Source -> Source -> Source -> CircuitM (Maybe (Buses d))
  newComp3L cir a b c = newComp cir (ProdB (ProdB (toBuses a) (toBuses b)) (toBuses c))
  
  newComp3R :: (SourceToBuses a, SourceToBuses b, SourceToBuses c) =>
               (a :* (b :* c) :> d) -> Source -> Source -> Source -> CircuitM (Maybe (Buses d))
  newComp3R cir a b c = newComp cir (ProdB (toBuses a) (ProdB (toBuses b) (toBuses c)))
  
  newVal :: GS b => b -> CircuitM (Maybe (Buses b))
  newVal b = Just <$> constM' b
  
  constM' :: GS b => b -> CircuitM (Buses b)
  constM' b = constComp' (constName b)
  
  -- noOpt :: Opt b
  -- noOpt = const nothingA
  
  orOpt :: Binop (Opt b)
  orOpt f g a = do mb <- f a
                   case mb of
                     Nothing -> g a
                     Just _  -> return mb
  
  primOpt     :: Ok  (:>)   b => PrimName -> Opt b -> a :> b
  primOptSort :: Ok2 (:>) a b => PrimName -> Opt b -> a :> b
  #if !defined NoOptimizeCircuit
  
  -- primOpt name _ = mkCK (genComp (Template name))
  
  primOpt name opt =
    mkCK $ \ a -> let plain = genComp (Prim name) a in
                    opt (flattenB a) >>= maybe plain return
  
  tryCommute :: a :> a
  tryCommute = mkCK try
   where
  #if !defined NoCommute
     -- TODO: Add an Ord constraint to PrimB for this line
     try (ProdB (PrimB a) (PrimB a')) | a > a' = return (ProdB (PrimB a') (PrimB a))
  #endif
     try b = return b
  
  -- Like primOpt, but sorts. Use for commutative operations to improve reuse
  -- (cache hits).
  primOptSort name opt = primOpt name opt . tryCommute
  #else
  primOpt name _ = namedC name
  primOptSort = primOpt
  #endif
  
  primNoOpt1 :: (Ok2 (:>) a b, Read a, Show b)
             => PrimName -> (a -> b) -> a :> b
  primNoOpt1 name fun =
    primOpt name $
      \ case [Val x] -> newVal (fun x)
             _       -> nothingA
  
  -- -- | Constant circuit from source generator (experimental)
  -- constSM :: CircuitM (Buses b) -> (a :> b)
  -- constSM mkB = mkCK (const mkB)
  
  -- -- | Constant circuit from source
  -- constS :: Buses b -> (a :> b)
  -- constS b = constSM (return b)
  
  constC :: GS b => b -> a :> b
  constC = mkCK . constM
  
  inC :: (a :+> b -> a' :+> b') -> (a :> b -> a' :> b')
  inC = C <~ unC
  
  inC2 :: (a :+> b -> a' :+> b' -> a'' :+> b'')
       -> (a :>  b -> a' :>  b' -> a'' :>  b'')
  inC2 = inC <~ unC
  
  instance Category (:>) where
    type Ok (:>) = GenBuses
    id  = C id
    (.) = inC2 (.)
  
  crossB :: (Applicative m, Ok4 (:>) a b c d)
         => (Buses a -> m (Buses c)) -> (Buses b -> m (Buses d))
         -> (Buses (a :* b) -> m (Buses (c :* d)))
  crossB f g = (\ ~(a,b) -> liftA2 ProdB (f a) (g b)) . unProdB
  
  -- or drop crossB in favor of forkB with fstB and sndB
  
  forkB :: (Applicative m, Ok3 (:>) a c d) =>
           (Buses a -> m (Buses c)) -> (Buses a -> m (Buses d))
        -> (Buses a -> m (Buses (c :* d)))
  forkB f g a = liftA2 ProdB (f a) (g a)
  
  -- or drop forkB in favor of dupB and crossB
  
  dupB :: (Applicative m, Ok (:>) a) =>
          Buses a -> m (Buses (a :* a))
  dupB a = pure (ProdB a a)
  
  instance OpCon (:*) (Sat GenBuses) where inOp = Entail (Sub Dict)
  
  instance MonoidalPCat (:>) where
    (***) = inCK2 crossB  -- or default
  
  instance AssociativePCat (:>)
  instance BraidedPCat     (:>)
  
  instance ProductCat (:>) where
    -- type Prod (:>) = (:*)
    exl = C (arr exlB)
    exr = C (arr exrB)
    dup = mkCK dupB
  
  instance UnitCat (:>)
  
  -- instance OpCon (:+) (Sat GenBuses) where inOp = Entail (Sub Dict)
  
  -- instance CoproductCat (:>) where
  --   inl = namedC "inl"
  --   inr = namedC "inr"
  --   f ||| g = namedC "|||"
  
  instance CoproductPCat (:>) where
    inlP   = namedC "inlP"
    inrP   = namedC "inrP"
    jamP   = namedC "jamP"
    -- swapPS = swapP
  
  {--------------------------------------------------------------------
      Misc
  --------------------------------------------------------------------}
  
  instance (Ok (:>) a, IfCat (:>) b) => IfCat (:>) (a -> b) where
    ifC = funIf
  
  instance OpCon (->) (Sat GenBuses) where inOp = Entail (Sub Dict)
  
  genSubgraph :: Ok2 (:>) b c => BCirc b c -> CircuitM (Buses (b -> c))
  genSubgraph bcirc =
    do supply <- M.gets fst
       let (g,supply') = mkGraph' (mkCK bcirc) supply
       M.modify (first (const supply'))
       genComp (Subgraph g bcirc) UnitB
  
  curryB :: Ok3 (:>) a b c => BCirc (a :* b) c -> BCirc a (b -> c)
  curryB f a = genSubgraph (\ b -> f (ProdB a b))
  
  -- primOpt, primOptSort :: Ok2 (:>) a b => PrimName -> Opt b -> a :> b
  -- type Opt b = [Source] -> CircuitM (Maybe (Buses b))
  
  -- data Source = forall a b. Source Bus (Template a b) [Source]
  
  instance ClosedCat (:>) where
    -- type Exp (:>) = (->)
    -- apply = namedC "apply"
    apply :: forall a b. Ok2 (:>) a b => (a -> b) :* a :> b
    apply = primOpt "apply" $ \ case
              (Source _ (Subgraph _ gen) _ : rest)
                -> Just <$> (unsafeCoerce gen :: BCirc a b) (unflattenB rest)
              _ -> nothingA
    curry = mkCK . curryB . unmkCK
  
  -- TODO: Try to make Source keep the unflattened bus structures instead of or in
  -- addition to the untyped sources. Then eliminate this unsafeCoerce and
  -- flattening and unflattening.
  
  -- TODO: use Newtype and inNew in curry and elsewhere.
  
  instance TerminalCat (:>)
  
  {--------------------------------------------------------------------
      Indexed co/products
  --------------------------------------------------------------------}
  
  instance OkIxProd (:>) G.U1   where okIxProd = Entail (Sub Dict)
  instance OkIxProd (:>) G.Par1 where okIxProd = Entail (Sub Dict)
  
  instance (OkIxProd (:>) f, OkIxProd (:>) g)
        => OkIxProd (:>) (f G.:*: g) where
    okIxProd :: forall a. Ok' (:>) a |- Ok' (:>) ((f G.:*: g) a)
    okIxProd = Entail (Sub (Dict <+ okIxProd @(:>) @f @a <+ okIxProd @(:>) @g @a))
  
  instance (OkIxProd (:>) f, OkIxProd (:>) g)
        => OkIxProd (:>) (g G.:.: f) where
    okIxProd :: forall a. Ok' (:>) a |- Ok' (:>) ((g G.:.: f) a)
    okIxProd = Entail (Sub (Dict <+ okIxProd @(:>) @g @(f a) <+ okIxProd @(:>) @f @a))
  
  instance KnownNat i => OkIxProd (:>) (Vector i) where
    okIxProd = Entail (Sub Dict)
  
  instance (OkIxProd (:>) h, Functor h, Zip h, Traversable h, Show1 h)
        => IxMonoidalPCat (:>) h where
    crossF :: forall a b. Ok2 (:>) a b => h (a :> b) -> (h a :> h b)
    crossF = inCKF1 crossFB
  
  instance (IxMonoidalPCat (:>) h, Representable h, Show (R.Rep h))
        => IxProductCat (:>) h where
    exF :: forall a . Ok (:>) a => h (h a :> a)
    exF = tabulate $ \ i -> namedC ("ex " ++ showsPrec 10 i "") <+ okIxProd @(:>) @h @a
    replF :: forall a . Ok (:>) a => a :> h a
    replF = namedC "replF" <+ okIxProd @(:>) @h @a
  
  instance ( OkIxProd (:>) h, Representable h, Zip h, Traversable h
           , Show (R.Rep h), Show1 h )
        => IxCoproductPCat (:>) h where
    inPF :: forall a. Ok (:>) a => h (a :> h a)
    inPF = tabulate $ \ i -> namedC ("inP " ++ showsPrec 10 i "") <+ okIxProd @(:>) @h @a
    jamPF :: forall a. Ok (:>) a => h a :> a
    jamPF = namedC "jamPF" <+ okIxProd @(:>) @h @a
    -- plusPF :: forall a b. Ok2 (:>) a b => h (a :> b) -> (h a :> h b)
    -- plusPF = crossF
  
  unIxProdB :: Buses (h a) -> h (Buses a)
  unIxProdB (IxProdB bs) = bs
  unIxProdB b = error ("unIxProdB: unexpected bus: " ++ show b)
  
  crossFB :: ( OkIxProd (:>) h, Zip h, Traversable h, Show1 h
             , Ok (:>) a, GenBuses b, Applicative m)
          => h (Buses a -> m (Buses b)) -> (Buses (h a) -> m (Buses (h b)))
  crossFB fs = fmap IxProdB . transpose . zap fs . unIxProdB
  
  --                                    fs             :: h (Buses a -> m (Buses b))
  --                              cross fs             :: h (Buses a) -> h (m (Buses b))
  --                  transpose . cross fs             :: h (Buses a) -> m (h (Buses b))
  --                  transpose . cross fs . toIxProdB :: Buses (h a) -> m (h (Buses b))
  -- fmap unIxProdB . transpose . cross fs . toIxProdB :: Buses (h a) -> m (Buses (h b))
  
  
  
  {--------------------------------------------------------------------
      Ad hoc Functor-level operations, to be removed
  --------------------------------------------------------------------}
  
  instance OkFunctor (:>) G.U1   where okFunctor = Entail (Sub Dict)
  instance OkFunctor (:>) G.Par1 where okFunctor = Entail (Sub Dict)
  
  instance (OkFunctor (:>) f, OkFunctor (:>) g)
        => OkFunctor (:>) (f G.:*: g) where
    okFunctor :: forall a. Ok' (:>) a |- Ok' (:>) ((f G.:*: g) a)
    okFunctor = Entail (Sub (Dict
                               <+ okFunctor' @(:>) @f @a
                               <+ okFunctor' @(:>) @g @a))
  
  instance (OkFunctor (:>) f, OkFunctor (:>) g)
        => OkFunctor (:>) (g G.:.: f) where
    okFunctor :: forall a. Ok' (:>) a |- Ok' (:>) ((g G.:.: f) a)
    okFunctor = Entail (Sub (Dict
                               <+ okFunctor' @(:>) @g @(f a)
                               <+ okFunctor' @(:>) @f @a))
  
  instance KnownNat i => OkFunctor (:>) (Vector i) where
    okFunctor = Entail (Sub Dict)
  
  #ifdef WithArr
  instance HasFin' a => OkFunctor (:>) (Arr a) where
    okFunctor = Entail (Sub Dict)
  #endif
  
  -- Use *uncurried* fmap and zipWith primitives.
  
  instance (Functor h, OkFunctor (:>) h) => FunctorCat (:>) h where
    fmapC :: forall a b. Ok2 (:>) a b => (a :> b) -> (h a :> h b)
    fmapC = inCK $ \ f as ->
              do ab <- genSubgraph f
                 genComp (Prim "fmap") (ProdB ab as)
                   <+ okFunctor' @(:>) @h @a
                   <+ okFunctor' @(:>) @h @b
    unzipC :: forall a b. Ok2 (:>) a b => h (a :* b) :> (h a :* h b)
    unzipC = namedC "unzip"
               <+ okFunctor' @(:>) @h @(a :* b)
               <+ okFunctor' @(:>) @h @a
               <+ okFunctor' @(:>) @h @b
  
  -- genSubgraph :: BCirc a b -> CircuitM (Buses (a -> b))
  -- f :: BCirc a b
  -- genSubgraph f :: CircuitM (Buses (a -> b))
  
  instance (Zip h, OkFunctor (:>) h) => ZipCat (:>) h where
  #if 0
    zipWithC  :: forall a b c. Ok3 (:>) a b c => (a :* b -> c) :> (h a :* h b -> h c)
    zipWithC = curry (namedC "zipWith")
                 <+ okFunctor' @(:>) @h @a
                 <+ okFunctor' @(:>) @h @b
                 <+ okFunctor' @(:>) @h @c
  #else
    zipC  :: forall a b. Ok2 (:>) a b => (h a :* h b) :> h (a :* b)
    zipC = namedC "zip"
             <+ okFunctor' @(:>) @h @(a :* b)
             <+ okFunctor' @(:>) @h @a
             <+ okFunctor' @(:>) @h @b
  #endif
  
  -- TODO: ZapCat instance? I don't think so, but we'll see.
  
  instance ({- Pointed h, -} OkFunctor (:>) h, Ok (:>) a) => PointedCat (:>) h a where
    pointC :: a :> h a
    pointC = namedC "point"
               <+ okFunctor' @(:>) @h @a
  
  instance (OkFunctor (:>) h, Additive a, Ok (:>) a) => AddCat (:>) h a where
    sumAC :: h a :> a
    sumAC = namedC "sumA" <+ okFunctor' @(:>) @h @a
  
  instance (OkFunctor (:>) h, Ord a, Ok (:>) a) => MinMaxFunctorCat (:>) h a where
    minimumC :: h a :> a
    minimumC = namedC "minimum" <+ okFunctor' @(:>) @h @a
    maximumC :: h a :> a
    maximumC = namedC "maximum" <+ okFunctor' @(:>) @h @a
  
  instance (OkFunctor (:>) h, Foldable h, Ord a, Ok (:>) a) => MinMaxFFunctorCat (:>) h a where
    minimumCF :: h a -> (a :* (h a :> a))
    minimumCF h = (minimum h, namedC "minimumF" <+ okFunctor' @(:>) @h @a)
    maximumCF :: h a -> (a :* (h a :> a))
    maximumCF h = (maximum h, namedC "maximumF" <+ okFunctor' @(:>) @h @a)
  
  -- instance () => IxSummableCat (:>) n a where
  --   -- ixSumC :: forall a. (Additive a, Ok (:>) a) => a :^ n :> a
  --   ixSumC = namedC "ixSum" -- <+ okFunctor' @(:>) @n @a
  
  -- instance (Functor h, OkFunctor (:>) h) => Strong (:>) h where
  --   strength :: forall a b. Ok2 (:>) a b => (a :* h b) :> h (a :* b)
  --   strength = namedC "strength"
  --               <+ okFunctor' @(:>) @h @(a :* b)
  --               <+ okFunctor' @(:>) @h @b
  
  okFunctor' :: forall k h a. OkFunctor k h => Ok' k a |- Ok' k (h a)
  okFunctor' = {- trace "" $ -} okFunctor @k @h @a
  {-# INLINE okFunctor' #-}
  
  -- okFunctor' :: forall k h a. (k ~ (:>), OkFunctor k h, Ok k a) => Ok' k a |- Ok' k (h a)
  -- okFunctor' = trace ("okFunctor: " ++ show (ty @(h a) <+ ok)) $
  --              (case ok of Entail (Sub Dict) -> trace  "(okFunctor evaluated)") $
  --              ok
  --  where
  --    ok = okFunctor @k @h @a
  -- {-# INLINE okFunctor' #-}
  
  -- Without the trace, `distributeC (:>) @Pair @(Vector n) @R` fails to terminate.
  -- Ditto for `distributeC (:>) @(Vector n) @Pair @R`. Other combinations seem fine.
  -- TODO: track down the cause.
  
  instance (OkFunctor (:>) g, OkFunctor (:>) f) => DistributiveCat (:>) g f where
    distributeC :: forall a. Ok (:>) a => f (g a) :> g (f a)
    distributeC = namedC "distribute"
                    <+ okFunctor' @(:>) @g @(f a) <+ okFunctor' @(:>) @f @a
                    <+ okFunctor' @(:>) @f @(g a) <+ okFunctor' @(:>) @g @a
  
  instance (GenBuses (R.Rep f), OkFunctor (:>) f) => RepresentableCat (:>) f where
    tabulateC :: forall a. Ok (:>) a => (R.Rep f -> a) :> f a
    tabulateC = -- trace "tabulateC @(:>)" $
                namedC "tabulate" <+ okFunctor' @(:>) @f @a
    indexC :: forall a. Ok (:>) a => f a :> (R.Rep f -> a)
    indexC = namedC "index" <+ okFunctor' @(:>) @f @a
  
  #if 0
  
  instance GS b => ConstCat (:>) b where
    const b = -- trace ("circuit const " ++ show b) $
              constC b
  
  #else
  
  #define LitConst(ty) instance GS (ty) => ConstCat (:>) (ty) where const = constC
  
  LitConst(())
  LitConst(Bool)
  LitConst(Int)
  LitConst(Integer)
  LitConst(Float)
  LitConst(Double)
  LitConst(Finite n)
  LitConst(Vector n a)
  
  -- -- This instance is problematic with Maybe / sums, since it leads to evaluating bottom.
  -- -- See notes from 2016-01-13.
  -- instance (ConstCat (:>) a, ConstCat (:>) b) => ConstCat (:>) (a :* b) where
  --   const = pairConst
  
  #endif
  
  #if 0
  class MaybeCat k where
    nothing :: () `k` Maybe a
    just    :: a `k` Maybe a
    maybe   :: (() `k` c) -> (a `k` c) -> (Maybe a `k` c)
  
  type Maybe a = a :* Bool
  
  nothing = (undefined,False)
  just a  = (a,True )
  
  maybe n j (a,p) = if p then n else j a
  
  newtype a :> b = C { unC :: a :+> b }
  type a :+> b = Kleisli CircuitM (Buses a) (Buses b)
  
  constM' :: GS b => b -> CircuitM (Buses b)
  
  #endif
  
  #if 1
  
  bottomG :: Ok2 (:>) z b => z :> b
  bottomG = -- trace "bottomG called" $
            namedC "⊥" -- "bottom"
            -- mkCK (constComp "undefined")
  
  #if 0
  
  #define BottomTemplate(ty) \
   instance BottomCat (:>) z (ty) where { bottomC = bottomG }
  
  BottomTemplate(Bool)
  BottomTemplate(Int)
  BottomTemplate(Integer)
  BottomTemplate(Float)
  BottomTemplate(Double)
  -- BottomTemplate(Vector n)
  
  #endif
  
  #if 0
  
  instance BottomCat (:>) z () where
  --   bottomC = mkCK (const (return UnitB))
    bottomC = C (arr (const UnitB))
  
  instance (BottomCat (:>) a, BottomCat (:>) b) => BottomCat (:>) (a :* b) where
    bottomC = bottomC &&& bottomC
  
  #if defined TypeDerivation
  bottomC :: () :> b
  bottomC . exl :: () :* a :> b
  curry (bottomC . exl) :: () :> (a -> b)
  #endif
  
  #elif 1
  instance Ok2 (:>) a b => BottomCat (:>) a b where
    bottomC = bottomG
  #elif 0
  instance GenBuses a => BottomCat (:>) a where
    bottomC = mkCK (const mkBot)
  #elif 0
  instance BottomCat (:>) where
    type BottomKon (:>) a = GenBuses a
    bottomC = mkCK (const (genBuses (Template "undefined") []))
  -- See the note at BottomCat
  #elif 0
  instance BottomCat (:>) where
    type BottomKon (:>) a = GenBuses a
    bottomC = mkCK (const mkBot)
  #endif
  
  #endif
  
  -- TODO: state names like "⊕" and "≡" just once.
  
  class GenBuses a => SourceToBuses a where toBuses :: Source -> Buses a
  instance SourceToBuses ()      where toBuses = const UnitB
  instance SourceToBuses Bool    where toBuses = PrimB
  instance SourceToBuses Int     where toBuses = PrimB
  instance SourceToBuses Integer where toBuses = PrimB
  instance SourceToBuses Float   where toBuses = PrimB
  instance SourceToBuses Double  where toBuses = PrimB
  
  instance KnownNat n => SourceToBuses (Finite n) where toBuses = PrimB
  
  #ifdef VectorSized
  instance (KnownNat n, GenBuses b) => SourceToBuses (Vector n b) where
    toBuses = PrimB
  #else
  instance (GenBuses i {-Typeable i-}, GenBuses b) => SourceToBuses (Vector i b) where
    toBuses = PrimB
  #endif
  
  sourceB :: SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
  sourceB = justA . toBuses
  
  unknownName :: PrimName
  unknownName = "??"
  
  instance Ok2 (:>) a b => UnknownCat (:>) a b where
    unknownC = namedC unknownName
  
  #define Sat(pred) ((pred) -> True)
  #define Eql(x) Sat(==(x))
  
  pattern Read :: Read a => a -> String
  pattern Read x <- (reads -> [(x,"")])
  
  pattern ConstS :: PrimName -> Source
  pattern ConstS name <- PSource _ name []
  
  pattern Val :: Read a => a -> Source
  pattern Val x <- ConstS (Read x)
  
  -- pattern Val x       <- ConstS (reads -> [(x,"")])
  
  pattern TrueS :: Source
  pattern TrueS  <- ConstS("True")
  
  pattern FalseS :: Source
  pattern FalseS <- ConstS("False")
  
  pattern NotS :: Source -> Source
  pattern NotS a <- PSource _ "not" [a]
  
  pattern XorS :: Source -> Source -> Source
  pattern XorS a b <- PSource _ "xor" [a,b]
  
  pattern EqS :: Source -> Source -> Source
  pattern EqS a b <- PSource _ "==" [a,b]
  
  -- pattern NeS :: Source -> Source -> Source
  -- pattern NeS a b <- PSource _ "/=" [a,b]
  
  -- primDelay :: (SourceToBuses a, GS a) => a -> (a :> a)
  -- primDelay a0 = primOpt (delayName a0s) $ \ case
  --                  [c@(ConstS (Eql(a0s)))] -> sourceB c
  --                  _ -> nothingA
  --  where
  --    a0s = show a0
  
  -- primDelay a0 = namedC (delayName (show a0))
  
  instance BoolCat (:>) where
    -- type BoolOf (:>) = Bool
    notC = primOpt "not" $ \ case
             [NotS a]  -> sourceB a
             [Val x]   -> newVal (not x)
             _         -> nothingA
    -- TODO: I want to add more like the following:
    --
    --      [EqS a b] -> newComp2 notEqual a b
    --
    -- But
    --
    --   Ambiguous type variable ‘b0’ arising from a use of ‘newComp2’
    --   prevents the constraint ‘(SourceToBuses b0)’ from being solved.
    --
    -- Optimizations are limited by not having static access to source types. I
    -- think I can fix it by adding a statically typed type GADT to
    -- `Source`. Or maybe a simpler version for primitive types only.
    andC = primOptSort "&&" $ \ case
             [TrueS ,y]            -> sourceB y
             [x,TrueS ]            -> sourceB x
             [x@FalseS,_]          -> sourceB x
             [_,y@FalseS]          -> sourceB y
  #if !defined NoIdempotence
             [x,x']      | x' == x -> sourceB x
  #endif
             [x,NotS x'] | x' == x -> newVal False
             [NotS x,x'] | x' == x -> newVal False
             _                     -> nothingA
    orC  = primOptSort "||" $ \ case
             [FalseS,y]            -> sourceB y
             [x,FalseS]            -> sourceB x
             [x@TrueS ,_]          -> sourceB x
             [_,y@TrueS ]          -> sourceB y
  #if !defined NoIdempotence
             [x,x']      | x' == x -> sourceB x
  #endif
             [x,NotS x'] | x' == x -> newVal True
             [NotS x,x'] | x' == x -> newVal True
             -- not a    || not b == not (a && b)
             -- TODO: Handle more elegantly.
             [NotS x, NotS y]      ->
               do o <- unmkCK andC (ProdB (PrimB x) (PrimB y))
                  newComp notC o
             _                     -> nothingA
    xorC = primOptSort "xor" $ \ case
             [FalseS,y]            -> sourceB y
             [x,FalseS]            -> sourceB x
             [TrueS,y ]            -> newComp1 notC y
             [x,TrueS ]            -> newComp1 notC x
             [x,x']      | x' == x -> newVal False
             [x,NotS x'] | x' == x -> newVal True
             [NotS x,x'] | x' == x -> newVal True
  #if 1
             -- not x `xor` y == not (x `xor` y)
             [NotS x, y]                -> newComp2 (notC . xorC) x y
             [x, NotS y]                -> newComp2 (notC . xorC) x y
             -- x `xor` (x `xor` y) == y
             [x, x' `XorS` y] | x' == x -> sourceB y
             [x, y `XorS` x'] | x' == x -> sourceB y
             [x `XorS` y, x'] | x' == x -> sourceB y
             [y `XorS` x, x'] | x' == x -> sourceB y
  #endif
             _                          -> nothingA
  
  boolToIntC :: Bool :> Int
  boolToIntC = namedC "boolToInt"
  
  #if 1
  
  -- noOpt :: Opt b
  -- noOpt = const nothingA
  
  eqOpt, neOpt :: forall a. (Read a, Eq a) => Opt Bool
  eqOpt = \ case
    [Val (x :: a), Val y] -> newVal (x == y)
    [a,b] | a == b -> newVal True
    _              -> nothingA
  neOpt = \ case
    [Val (x :: a), Val y] -> newVal (x /= y)
    [a,b] | a == b -> newVal False
    _              -> nothingA
  
  #define EqTemplate(ty) \
   instance (Read (ty), Eq (ty), GenBuses (ty)) => EqCat (:>) (ty) where { \
      equal    = primOptSort "==" (eqOpt @(ty)) ;\
      notEqual = primOptSort "/=" (neOpt @(ty))  \
    }
  
  -- TODO: give one overlappable EqCat instance and one or more overlapping.
  
  iffC :: EqCat k (BoolOf k) => Prod k (BoolOf k) (BoolOf k) `k` BoolOf k
  iffC = equal
  
  eqOptB, neOptB :: Opt Bool
  -- eqOptB = noOpt
  -- neOptB = noOpt
  
  eqOptB = \ case
    [TrueS,y]                           -> sourceB y
    [x,TrueS]                           -> sourceB x
    [FalseS,y ]                         -> newComp1 notC y
    [x,FalseS ]                         -> newComp1 notC x
    [x,NotS x']      | x' == x          -> newVal False
    [NotS x,x']      | x' == x          -> newVal False
    -- not x == y == not (x == y)
    [NotS x, y]                         -> newComp2 (notC . iffC) x y
    [x, NotS y]                         -> newComp2 (notC . iffC) x y
    -- x == (x /= y) == not y
    [x, x' `XorS` y] | x' == x          -> newComp1 notC y
    [x, y `XorS` x'] | x' == x          -> newComp1 notC y
    [x `XorS` y, x'] | x' == x          -> newComp1 notC y
    [y `XorS` x, x'] | x' == x          -> newComp1 notC y
    -- x == (x == y) == y
    [x, x' `EqS` y]  | x' == x          -> sourceB y
    [x, y `EqS` x']  | x' == x          -> sourceB y
    [x `EqS` y, z]   | z == x || z == y -> sourceB y
    _                                   -> nothingA
  
  --   [x `EqS` y, Eql(x)]  -> sourceB y
  --   [y `EqS` x, Eql(x)]  -> sourceB y
  --
  --     Pattern match checker exceeded (2000000) iterations in
  --     a case alternative.
  
  neOptB = \ case
    [FalseS,y]                          -> sourceB y
    [x,FalseS]                          -> sourceB x
    [TrueS,y ]                          -> newComp1 notC y
    [x,TrueS ]                          -> newComp1 notC x
    [x,x']           | x' == x          -> newVal False
    [x,NotS x']      | x' == x          -> newVal True
    [NotS x,x']      | x' == x          -> newVal True
    -- not x `xor` y == not (x `xor` y)
    [NotS x, y]                         -> newComp2 (notC . xorC) x y
    [x, NotS y]                         -> newComp2 (notC . xorC) x y
    -- x `xor` (x `xor` y) == y
    [x, x' `XorS` y] | x' == x          -> sourceB y
    [x, y `XorS` x'] | x' == x          -> sourceB y
    [x `XorS` y, x'] | x' == x          -> sourceB y
    [y `XorS` x, x'] | x' == x          -> sourceB y
    -- x `xor` (x == y) == not y
    [x, x' `EqS` y]  | x' == x          -> newComp1 notC y
    [x, y `EqS` x']  | x' == x          -> newComp1 notC y
    [x `EqS` y, z]   | z == x || z == y -> newComp1 notC y
    _                                   -> nothingA
  
  --   [x `EqS` y, Eql(x)]  -> newComp1 notC y
  --   [y `EqS` x, Eql(x)]  -> newComp1 notC y
  --
  --     Pattern match checker exceeded (2000000) iterations in
  --     a case alternative.
  
  -- EqTemplate(Bool)
  EqTemplate(Int)
  EqTemplate(Integer)
  EqTemplate(Float)
  EqTemplate(Double)
  EqTemplate(a :+ b)
  
  instance EqCat (:>) Bool where
    equal    = primOptSort "=="  (eqOpt @Bool `orOpt` eqOptB)
    notEqual = primOptSort "xor" (neOpt @Bool `orOpt` neOptB)
  
  instance EqCat (:>) () where
    equal = constC True
  
  -- instance (EqCat (:>) a, EqCat (:>) b) => EqCat (:>) (a :* b) where
  --   equal = andC . (equal *** equal) . transposeP
  
  -- Use EqTemplate for (a :* b) ?
  
  -- TODO: optimizations.
  ltOpt, gtOpt, leOpt, geOpt :: forall a. (Read a, Ord a) => Opt Bool
  -- ltOpt = noOpt
  -- gtOpt = noOpt
  -- leOpt = noOpt
  -- geOpt = noOpt
  
  ltOpt = \ case
    [Val (x :: a), Val y] -> newVal (x < y)
    [a,b] | a == b        -> newVal False
    _                     -> nothingA
  gtOpt = \ case
    [Val (x :: a), Val y] -> newVal (x > y)
    [a,b] | a == b        -> newVal False
    _                     -> nothingA
  leOpt = \ case
    [Val (x :: a), Val y] -> newVal (x <= y)
    [a,b] | a == b        -> newVal True
    _                     -> nothingA
  geOpt = \ case
    [Val (x :: a), Val y] -> newVal (x >= y)
    [a,b] | a == b        -> newVal True
    _                     -> nothingA
  
  -- ltOpt = \ case
  --   [Val x, Val y] -> newVal (x < y)
  --   _              -> nothingA
  
  --     No instance for (Read a0) arising from a pattern
  --     The type variable ‘a0’ is ambiguous
  
  #define OrdTemplate(ty) \
   instance OrdCat (:>) (ty) where { \
     lessThan           = primOpt "<" (ltOpt @(ty)) ; \
     greaterThan        = primOpt ">" (gtOpt @(ty)) ; \
     lessThanOrEqual    = primOpt "<=" (leOpt @(ty)) ; \
     greaterThanOrEqual = primOpt ">=" (geOpt @(ty)) ; \
   }
  
  OrdTemplate(Bool)
  OrdTemplate(Int)
  OrdTemplate(Integer)
  OrdTemplate(Float)
  OrdTemplate(Double)
  
  instance OrdCat (:>) () where
    lessThan = constC False
  
  -- TODO:
  --
  -- instance (OrdCat (:>) a, OrdCat (:>) b) => OrdCat (:>) (a,b) where
  --   ...
  
  -- TODO: Move to a general definition in ConCat.Classes, and reference here.
  
  #else
  
  instance (Read a, Eq a) => EqCat (:>) a where
      equal    = primOptSort "==" $ \ case
                   [Val (x :: a), Val y] -> newVal (x == y)
                   [a,b] | a == b -> newVal True
                   _              -> nothingA
      notEqual = primOptSort "/=" $ \ case
                   [Val (x :: a), Val y] -> newVal (x /= y)
                   [a,b] | a == b -> newVal False
                   _              -> nothingA
  
  instance (Read a, Ord a) => OrdCat (:>) a where
     lessThan           = primOpt "<" $ \ case
                            [Val (x :: a), Val y] -> newVal (x < y)
                            [a,b] | a == b        -> newVal False
                            _                     -> nothingA
     greaterThan        = primOpt ">" $ \ case
                            [Val (x :: a), Val y] -> newVal (x > y)
                            [a,b] | a == b        -> newVal False
                            _                     -> nothingA
     lessThanOrEqual    = primOpt "<=" $ \ case
                            [Val (x :: a), Val y] -> newVal (x <= y)
                            [a,b] | a == b        -> newVal True
                            _                     -> nothingA
     greaterThanOrEqual = primOpt ">=" $ \ case
                            [Val (x :: a), Val y] -> newVal (x >= y)
                            [a,b] | a == b        -> newVal True
                            _                     -> nothingA
  
  
  #endif
  
  instance Ok (:>) a => MinMaxCat (:>) a where
    minC = namedC "min"
    maxC = namedC "max"
  
  -- TODO: Move to a general definition in ConCat.Classes, and reference here.
  
  -- instance NumCat (:>) Int  where { add = namedC "+" ; mul = namedC "×" }
  
  -- More robust (works for Double as well):
  
  #define ValT(x,ty) (Val ((x) :: ty))
  
  #define   ZeroT(ty) ValT(0,ty)
  #define    OneT(ty) ValT(1,ty)
  #define NegOneT(ty) ValT((-1),ty)
  
  pattern NegateS :: Source -> Source
  pattern NegateS a <- PSource _ "negate" [a]
  
  pattern RecipS  :: Source -> Source
  pattern RecipS  a <- PSource _ "recip"  [a]
  
  instance (Num a, Read a, GS a, Eq a, SourceToBuses a)
        => NumCat (:>) a where
    negateC = primOpt "negate" $ \ case
                [Val x]         -> newVal (negate x)
                [NegateS x]     -> sourceB x
                _               -> nothingA
    addC    = primOptSort "+" $ \ case
                [Val x, Val y]  -> newVal (x + y)
                [ZeroT(a),y]    -> sourceB y
                [x,ZeroT(a)]    -> sourceB x
                [x,NegateS y]   -> newComp2 subC x y
                [NegateS x,y]   -> newComp2 subC y x
                _               -> nothingA
    subC    = primOpt     "-" $ \ case
                [Val x, Val y]  -> newVal (x - y)
                [ZeroT(a),y]    -> newComp1 negateC y
                [x,ZeroT(a)]    -> sourceB x
                [x,NegateS y]   -> newComp2 addC x y
                [NegateS x,y]   -> newComp2 (negateC . addC) x y
                _               -> nothingA
    mulC    = primOptSort "*" $ \ case
                [Val x, Val y]  -> newVal (x * y)
                [OneT(a),y]     -> sourceB y
                [x,OneT(a)]     -> sourceB x
                [x@ZeroT(a),_]  -> sourceB x
                [_,y@ZeroT(a)]  -> sourceB y
                [NegOneT(a) ,y] -> newComp1 negateC y
                [x,NegOneT(a) ] -> newComp1 negateC x
                [NegateS x,y]   -> newComp2 (negateC . mulC) x y
                [x,NegateS y]   -> newComp2 (negateC . mulC) x y
                _               -> nothingA
    powIC   = primOpt     "^" $ \ case
                [Val x, Val y]  -> newVal (x ^ (y :: Int))
                [x@OneT(a) ,_]  -> sourceB x
                [x,   OneT(a)]  -> sourceB x
                [x@ZeroT(a),_]  -> sourceB x
                [_,  ZeroT(a)]  -> newVal (fromInteger 1)
                _               -> nothingA
  
  -- instance Integral a => IntegralCat (:>) a where
  --   divC = primNoOpt1 "div" div
  --   modC = primNoOpt1 "mod" mod
  
  instance (Integral a, Read a, GS a, SourceToBuses a) => IntegralCat (:>) a where
    divC = primOpt "div" $ \case
                [Val x, Val y] -> newVal (x `div` y)
                [x,OneT(a)]    -> sourceB x
                [x@ZeroT(a),_] -> sourceB x
                _              -> nothingA
    modC = primOpt "mod" $ \case
                [Val x, Val y] -> newVal (x `mod` y)
                [_,OneT(a)]    -> newVal 0
                [x@ZeroT(a),_] -> sourceB x
                _              -> nothingA
  
  instance (Fractional a, Read a, Eq a, GS a, SourceToBuses a)
        => FractionalCat (:>) a where
    recipC  = primOpt "recip" $ \ case
                [Val x]        -> newVal (recip x)
                [RecipS x]     -> sourceB x
                [NegateS x]    -> newComp1 (negateC . recipC) x
                _              -> nothingA
    divideC = primOpt "/" $ \ case
                [Val x, Val y] -> newVal (x / y)
                [z@ZeroT(a),_] -> sourceB z
                [x,OneT(a)]    -> sourceB x
                [x,NegateS y]  -> newComp2 (negateC . divideC) x y
                _              -> nothingA
  
  instance (RealFrac a, Integral b, GS a, GS b, Read a)
        => RealFracCat (:>) a b where
    floorC    = primNoOpt1 "floor"   floor
    ceilingC  = primNoOpt1 "ceiling" ceiling
    truncateC = primNoOpt1 "truncate" truncate
  
  instance (Floating a, Read a, GS a) => FloatingCat (:>) a where
    expC = primNoOpt1 "exp" exp
    cosC = primNoOpt1 "cos" cos
    sinC = primNoOpt1 "sin" sin
    logC = primNoOpt1 "log" log
    sqrtC = primNoOpt1 "sqrt" sqrt
  
  -- TODO: optimizations, e.g., sin & cos of negative angles.
  
  instance (Ok (:>) a, Integral a, Num b, Read a, GS b)
        => FromIntegralCat (:>) a b where
    fromIntegralC = primNoOpt1 "fromIntegral" fromIntegral
  
  instance (ConstCat (:>) a, NumCat (:>) a, Num a) => EnumCat (:>) a
  
  -- Simplifications for all types:
  --
  --   if' (False,(_,a))     = a
  --   if' (True ,(b,_))     = b
  --   if' (not a,(b,c))     = if' (a,(c,b))
  --   if' (_    ,(a,a))     = a
  --   if' (a,(b,bottom))    = b
  --   if' (a,(bottom,c))    = c
  --
  -- Simplifications for Bool values:
  --
  --   if' (c,(True,False))  = c
  --   if' (c,(False,True))  = not c
  --   if' (a,(b,False))     =     a && b
  --   if' (a,(False,b))     = not a && b
  --   if' (a,(True ,b))     =     a || b
  --   if' (a,(b,True ))     = not a || b
  --   if' (c,(not a,a))     = c `xor` a
  --   if' (c,(a,not a))     = c `xor` not a
  --   if' (b,(c `xor` a,a)) = (b && c) `xor` a
  --   if' (b,(a `xor` c,a)) = (b && c) `xor` a
  
  ifOptB :: Opt Bool
  ifOptB = \ case
    [c,TrueS,FalseS]       -> sourceB c
    [c,FalseS,TrueS]       -> newComp1 notC c
    [a,b,FalseS]           -> newComp2 andC a b
    [a,FalseS,b]           -> newComp2 (andC . first notC) a b -- not a && b
    [a,TrueS, b]           -> newComp2 orC  a b
    [a,b ,TrueS]           -> newComp2 (orC  . first notC) a b -- not a || b
    [c,NotS a,Eql(a)]      -> newComp2 xorC c a
    [c,a,b@(NotS(Eql(a)))] -> newComp2 xorC c b
    [b,c `XorS` a,Eql(a)]  -> newComp3L (xorC . first andC) b c a -- (b && c) `xor` a
    [b,a `XorS` c,Eql(a)]  -> newComp3L (xorC . first andC) b c a -- ''
    _                      -> nothingA
  
  #if !defined NoIfBotOpt
  pattern BottomS :: Source
  pattern BottomS <- ConstS "undefined"
  #endif
  
  ifOpt :: (IfCat (:>) a, SourceToBuses a) => Opt a
  ifOpt = \ case
    [FalseS,_,a]  -> sourceB a
    [ TrueS,b,_]  -> sourceB b
    [NotS a,b,c]  -> newComp3R ifC a c b
    [_,a,Eql(a)]  -> sourceB a
  #if !defined NoIfBotOpt
    [_,b,BottomS] -> sourceB b
    [_,BottomS,c] -> sourceB c
  #endif
    _             -> nothingA
  
  ifOptI :: Opt Int
  
  #if 0
  
  -- Zero or one, yielding the False or True, respectively.
  pattern BitS :: Bool -> Source
  pattern BitS b <- PSource _ (readBit -> Just b) []
  
  readBit :: String -> Maybe Bool
  readBit "0" = Just False
  readBit "1" = Just True
  readBit _   = Nothing
  
  pattern BToIS :: Source -> Source
  pattern BToIS a <- PSource _ BooloInt [a]
  
  -- if c then 0 else b == if c then boolToInt False else b
  -- if c then 1 else b == if c then boolToInt True  else b
  --
  -- if c then a else 0 == if c then a else boolToInt False
  -- if c then a else 1 == if c then a else boolToInt True
  --
  -- if c then boolToInt a else boolToInt b = boolToInt (if c then a else b)
  ifOptI = \ case
    [c,BitS x,b]         -> newComp2 (ifC . second (bToIConst x &&& id)) c b
    [c,a,BitS y]         -> newComp2 (ifC . second (id &&& bToIConst y)) c a
    [c,BToIS a, BToIS b] -> newComp3R (boolToIntC . ifC) c a b
    _                    -> nothingA
  
  bToIConst :: Bool -> (a :> Int)
  bToIConst x = boolToIntC . constC x
  
  #else
  
  pattern ZeroS :: Source
  pattern ZeroS <- ConstS "0"
  
  pattern OneS :: Source
  pattern OneS <- ConstS "1"
  
  -- (if c then 1 else 0) = boolToInt c
  -- (if c then 0 else 1) = boolToInt (not c)
  ifOptI = \ case
    -- [c,OneS,ZeroS] -> newComp1 boolToIntC c
    -- [c,ZeroS,OneS] -> newComp1 (boolToIntC . notC) c
    _              -> nothingA
  #endif
  
  instance IfCat (:>) Bool    where ifC = primOpt "if" (ifOpt `orOpt` ifOptB)
  instance IfCat (:>) Int     where ifC = primOpt "if" (ifOpt `orOpt` ifOptI)
  instance IfCat (:>) Integer where ifC = primOpt "if" ifOpt
  instance IfCat (:>) Float   where ifC = primOpt "if" ifOpt
  instance IfCat (:>) Double  where ifC = primOpt "if" ifOpt
  
  instance KnownNat n => IfCat (:>) (Finite n) where ifC = primOpt "if" ifOpt
  -- TODO: refactor
  
  -- TODO: Would we rather zip the conditional over the vector?
  instance (GenBuses b, KnownNat n) => IfCat (:>) (Vector n b) where
    ifC = primOpt "if" ifOpt
  
  instance IfCat (:>) () where ifC = unitIf
  
  instance (IfCat (:>) a, IfCat (:>) b) => IfCat (:>) (a :* b) where
    ifC = prodIf
  
  pattern UnsafeFiniteS :: Source -> Source
  pattern UnsafeFiniteS a <- PSource _ "unsafeFinite" [a]
  
  instance FiniteCat (:>) where
    unsafeFinite = namedC "unsafeFinite"
    -- unFinite     = namedC "unFinite"
    unFinite :: forall n. KnownNat n => Finite n :> Int
    unFinite = primOpt "unFinite" $ \case
                 [ValT(x,Finite n)] -> newVal (unFinite x)
                 [UnsafeFiniteS x]  -> sourceB x
                 _                  -> nothingA
  
  {--------------------------------------------------------------------
      Running
  --------------------------------------------------------------------}
  
  instance (GenBuses a, Ok2 (:>) a b) => Show (a :> b) where
    -- show = show . mkGraph -- runC
    show = show . fmap simpleComp . mkGraph
  
  --     Application is no smaller than the instance head
  --       in the type family application: RepT :> a
  --     (Use -XUndecidableInstances to permit this)
  
  -- -- Turn a circuit into a list of components, including fake In & Out.
  -- runC :: (GenBuses a, Ok (:>) b) => (a :> b) -> Graph
  -- runC = runU . unitize
  
  type UU = () :> ()
  
  -- runU :: UU -> Graph
  -- runU cir = fst (runU' cir 0)
  
  runU' :: UU -> IdSupply -> (Graph,IdSupply)
  runU' cir supply = (getComps compInfo, supply')
   where
     compInfo :: CompInfo
     (supply',compInfo) = execState (unmkCK cir UnitB) (supply,mempty)
  #if !defined NoHashCons
     getComps = M.elems
  #else
     getComps = id
  #endif
  
  -- Wrap a circuit with fake input and output
  unitize :: (GenBuses a, Ok (:>) b) => (a :> b) -> UU
  unitize = namedC "Out" <~ namedC "In"
  
  -- uuGraph :: UU -> Graph
  -- uuGraph uu = fst (uuGraph' uu 0)
  
  uuGraph' :: UU -> IdSupply -> (Graph,IdSupply)
  uuGraph' = runU'  -- for now
  
  mkGraph :: Ok2 (:>) a b => (a :> b) -> Graph
  
  -- mkGraph g = sort $ trimGraph $ fst (mkGraph' g 0)
  
  mkGraph g = -- trace "mkGraph" $
              -- trace ("fst (mkGraph' g 0)" ++ show (fst (mkGraph' g 0))) $
              -- trace ("trimGraph --> " ++ show (trimGraph $ fst (mkGraph' g 0))) $
              -- trace ("sort --> " ++ show (sort $ trimGraph $ fst (mkGraph' g 0))) $
              sort $ trimGraph $ fst (mkGraph' g 0)
  
  mkGraph' :: Ok2 (:>) a b => (a :> b) -> IdSupply -> (Graph,IdSupply)
  mkGraph' g n = uuGraph' (unitize g) n
  
  
  {--------------------------------------------------------------------
      Visualize circuit as dot graph
  --------------------------------------------------------------------}
  
  -- I could use the language-dot API, but it's easier not to.
  -- TODO: Revisit this choice if the string manipulation gets complicated.
  
  systemSuccess :: String -> IO ()
  systemSuccess cmd =
    do status <- system cmd
       case status of
         ExitSuccess -> return ()
         _ -> fail (printf "command \"%s\" failed." cmd)
  
  
  type Attr = (String,String)
  
  -- Some options:
  --
  -- ("pdf","")
  -- ("svg","")
  -- ("png","-Gdpi=200")
  -- ("jpg","-Gdpi=200")
  
  renameC :: Unop String
  renameC = id
  #if defined NoOptimizeCircuit
          . (++"-no-opt")
  #else
  #if defined NoIdempotence
          . (++"-no-idem")
  #endif
  #if defined NoCommute
          . (++"-no-commute")
  #endif
  #if defined NoIfBotOpt
          . (++"-no-ifbot")
  #endif
  #endif
  #if defined NoHashCons
          . (++"-no-hash")
  #endif
  #if defined NoMend
          . (++"-no-mend")
  #endif
  #if defined ShallowDelay
          . (++"-shallow-delay")
  #endif
  
  -- Remove while I'm sorting things out
  #if 1
  
  type Name = String
  type Report = String
  
  outDir :: String
  outDir = "out"
  
  outFile :: String -> String -> String
  outFile name suff = outDir++"/"++name++"."++suff
  
  writeDot :: String -> [Attr] -> Graph -> IO ()
  writeDot (renameC -> name) attrs g =
    do createDirectoryIfMissing False outDir
       writeFile (outFile name "dot")
         (graphDot name attrs g {- ++"// "++ report -})
       putStrLn ("Wrote " ++ name)
       -- putStr report
  
  displayDot :: (String,String) -> String -> IO ()
  displayDot (outType,res) (renameC -> name) =
    do putStrLn dotCommand
       systemSuccess dotCommand
       -- printf "Wrote %s\n" picFile
       systemSuccess $ printf "%s %s" open picFile
   where
     dotCommand = printf "dot %s -T%s %s -o %s" res outType dotFile picFile
     dotFile = outFile name "dot"
     picFile = outFile name outType
     open = case SI.os of
              "darwin" -> "open"
              "linux"  -> "display" -- was "xdg-open"
              _        -> error "unknown open for OS"
  
  #if 0
  
  showCounts :: [(PrimName,Int)] -> String
  showCounts = intercalate ", "
             . map (\ (nm,num) -> printf "%d %s" num nm)
             . (\ ps -> if length ps <= 1 then ps
                         else ps ++ [("total",sum (snd <$> ps))])
             . filter (\ (nm,n) -> n > 0 && not (isOuterTemplate nm))
  
  summary :: Graph -> String
  summary = showCounts
          . histogram
          . map compName
          . gather
   where
     gather :: Graph -> [Comp]
     gather (Graph comps) = comps
  
  histogram :: Ord a => [a] -> [(a,Int)]
  histogram = map (head &&& length) . group . sort
  
  -- TODO: Instead of failing, emit a message about the generated file. Perhaps
  -- simply use "echo".
  
  #endif
  
  type Dot = String
  
  #if 0
  
  -- type Depth = Int
  
  type CompDepths = Map CompS Depth
  
  -- | Longest paths excluding delay/Cons elements.
  longestPaths :: Graph -> CompDepths
  longestPaths g = distances
   where
     sComp = sourceComp g
     distances :: Map CompS Depth
     distances = M.fromList ((id &&& dist) <$> g)
     memoDist, dist :: CompS -> Depth
     memoDist = (distances M.!)
     -- Greatest distances a starting point.
     dist c | isStart c = 0
            | otherwise = 1 + maximumD ((memoDist . sComp) <$> compIns c)
     isStart c = null (compIns c) || isDelay c
  
  -- longestPath is adapted from the linear-time algorithm for *acyclic* longest
  -- path, using lazy evaluation in place of (explicit) topological sort. See
  -- <https://en.wikipedia.org/wiki/Longest_path_problem#Acyclic_graphs_and_critical_paths>.
  
  -- Note: if we measured the depth *before* mending, we wouldn't have to be take
  -- care about cycles.
  
  sourceComp :: Graph -> (Output -> Comp)
  sourceComp g = \ o -> fromMaybe (error (msg o)) (M.lookup o comps)
   where
     msg o = printf "sourceComp: mystery output %s in graph %s."
               (show o) (show g)
     comps = foldMap (\ c -> M.fromList [(o,c) | o <- compOuts c]) g
  
  -- The pred eliminates counting both In (constants) *and* Out.
  
  maximumD :: [Depth] -> Depth
  maximumD [] = 0
  maximumD ds = maximum ds
  
  -- Greatest depth over components with outputs
  longestPath :: CompDepths -> Depth
  longestPath = maximumD . M.elems . withOuts
   where
     withOuts = M.filterWithKey (\ c _ -> not (null (compOuts c)))
  
  isDelay :: CompS -> Bool
  isDelay = isJust . unDelayName . compName
  
  #endif
  
  -- Trim unused components. Construct the transitive closure of immediate
  -- dependencies starting from the top-level graph's output component. For each
  -- key/value pair in the map, find the immediate predecessor IDs.
  
  trimGraph :: Unop Graph
  -- trimGraph g | trace (printf "trimGraph %s" (show g)) False = undefined
  trimGraph g = go g
   where
     isUsed = (`S.member` usedComps g)
     go = map (onCompSubgraph go) . filter (isUsed . compId)
  
  usedComps :: Graph -> S.Set CompId
  usedComps g = transitiveClosure (compUses g) [outId g]
  
  compUses :: Graph -> CompId -> [CompId]
  compUses g = -- trace (printf "compUses: gmap == %s" (show gmap))
               (M.!) (preds <$> gmap)
    where
      gmap = graphMap g
      preds (Comp _ templ (flatB -> ins) _) =
        [c | Bus c _ _ <- ins] ++
        case templ of Prim _ -> []
                      Subgraph g' _ -> [outId g']
  
  graphMap :: Graph -> Map Id Comp
  graphMap comps =
       M.fromList [(compId c,c) | c <- comps]
    <> M.unions (graphMap <$> [g | Comp _ (Subgraph g _) _ _ <- comps])
  
  transitiveClosure :: forall a. ({- Show a, -} Ord a) => (a -> [a]) -> [a] -> S.Set a
  transitiveClosure nexts = go mempty
   where
     go :: S.Set a -> [a] -> S.Set a
     -- go seen as | trace (printf "go %s %s" (show (S.toList seen)) (show as)) False = undefined
     go seen     [] = seen
     go seen (a:as) | a `S.member` seen = go seen as
                    | otherwise         = go (S.insert a seen) (nexts a ++ as)
  
  graphDot :: String -> [Attr] -> Graph -> Dot
  graphDot name attrs comps =
    printf "digraph %s {\n%s}\n" (tweak <$> name)
           (unlines $ map indent $
            (  prelude
            ++ recordDots comps
            -- ++ concatMap subgraphDot (M.toList subgraphs)
            ))
   where
     prelude = [ "margin=0"
               , "compound=true"
               , "rankdir=LR"
               , "node [shape=Mrecord]"
               , "edge [fontsize=8,fontcolor=indigo]"
               , "bgcolor=transparent"
               , "nslimit=20"  -- helps with very large rank graphs
               -- , "ratio=1"
               -- , "ranksep=1.0"
               -- , fixedsize=true
               ] ++ [a ++ "=" ++ show v | (a,v) <- attrs]
     tweak '-' = '_'
     tweak c   = c
  
  indent :: Unop String
  indent = ("  " ++)
  
  subgraphDot :: CompId -> Graph -> [Statement]
  subgraphDot nc comps =
       [printf "subgraph cluster_%d {" nc]
    ++ map indent (prelude ++ recordDots comps)
    ++ ["}"]
   where
     prelude = [ "margin=8" , "fontsize=20", "labeljust=r", "color=DarkGreen" ]
  
  -- TODO: refactor graphDot & subgraphDot
  
  type Statement = String
  
  data CompS = CompS CompId PrimName [Input] [Output] deriving Show
  
  #if 0
  
  compSId :: CompS -> CompId
  compSId (CompS n _ _ _) = n
  compSName :: CompS -> PrimName
  compSName (CompS _ nm _ _) = nm
  compSIns :: CompS -> [Input]
  compSIns (CompS _ _ ins _) = ins
  compSOuts :: CompS -> [Output]
  compSOuts (CompS _ _ _ outs) = outs
  
  instance Eq  CompS where (==)    = (==)    `on` compSId
  instance Ord CompS where compare = compare `on` compSId
  
  #endif
  
  simpleComp :: Comp -> CompS
  simpleComp (Comp n prim a b) = CompS n (show prim) (flatB a) (flatB b)
  
  -- pattern CompS :: CompId -> String -> [Bus] -> [Bus] -> Comp
  -- pattern CompS cid name ins outs <- Comp cid (Prim name) (flatB -> ins) (flatB -> outs)
  
  flatB :: {- GenBuses c => -} Buses c -> [Bus]
  flatB = fmap sourceBus . flattenB
  
  data Dir = In | Out deriving Show
  type PortNum = Int
  
  -- -- For more succinct labels, so as not to stress Graphviz so much.
  -- -- TODO: also compact the port numbers to base 64.
  -- instance Show Dir where
  --   show In  = "I"
  --   show Out = "O"
  
  taggedFrom :: Int -> [a] -> [(Int,a)]
  taggedFrom n = zip [n ..]
  
  tagged :: [a] -> [(Int,a)]
  tagged = taggedFrom 0
  
  hideNoPorts :: Bool
  hideNoPorts = False
  
  -- Prettier names for graph display
  prettyName :: Unop String
  prettyName str = fromMaybe str (M.lookup str prettyNames)
  
  prettyNames :: Map String String
  prettyNames = M.fromList
   [ ("not","¬") , ("&&","∧") , ("||","∨") , ("xor","⊕")
   , ("==","≡") , ("/=","≢")
   , ("<=","≤") , (">=","≥")
   , ("-","−"), ("*","×") , ("^","↑") , ("/","÷")
   , ("undefined","⊥")
   , ("boolToInt", "Bool→Int")
   , ("arrAt","!")
   ]
  
  outId :: Graph -> CompId
  outId (filter isOut -> [Comp cid _ _ _]) = cid
  outId g = error ("outId: no Out found in graph: " ++ show g)
  
  isOut :: Comp -> Bool
  isOut (Comp _ (Prim "Out") _ _) = True
  isOut _                         = False
  
  recordDots :: [Comp] -> [Statement]
  recordDots comps = nodes ++ edges
   where
     nodes = concatMap node comps
      where
        node :: Comp -> [Statement]
        node (Comp nc (Subgraph g _) UnitB (PrimB _)) = subgraphDot nc g
        node (simpleComp -> CompS nc (prettyName -> prim) ins outs) =
          [prefix ++ mbCluster
           (printf "%s [label=\"{%s%s%s}\"%s]"
             (compLab nc)
             (ports "" (labs In ins) "|")
             (escape prim)
             (ports "|" (labs Out outs) "")
             extras)]
         where
           isSubgraph (Subgraph {}) = True
           isSubgraph _ = False
           wrapNodes = any (\ (Comp _ p _ _) -> isSubgraph p) comps
           mbCluster :: Unop String
           mbCluster | wrapNodes =
             printf "subgraph clusterc%d { label=\"\"; color=white; margin=0; %s }" nc
                     | otherwise = id
           extras | prim == unknownName = ",fontcolor=red,color=red,style=bold"
                  | otherwise = ""
           prefix =
             if hideNoPorts && null ins && null outs then "// " else ""
           ports _ "" _ = ""
           ports l s r = printf "%s{%s}%s" l s r
           labs :: Dir -> [Bus] -> String
           -- Labels. Use Dot string concat operator to avoid lexer buffer size limit.
           -- See https://github.com/ellson/graphviz/issues/71 .
           labs dir bs = segmentedDotString $
                         intercalate "|" (portSticker <$> tagged bs)
            where
              portSticker :: (Int,Bus) -> String
              portSticker (p,_) = bracket (portLab dir p)
           -- Escape angle brackets, "|", and other non-ascii
           escape :: Unop String
           escape [] = []
           escape (c:cs) = mbEsc (c : escape cs)
            where
               mbEsc | (c `elem` "<>|{}") || not (isAscii c)  = ('\\' :)
                     | otherwise     = id
        -- node comp = error ("recordDots/node: unexpected comp " ++ show comp)
     bracket = ("<"++) . (++">")
     edges = concatMap compEdges comps
      where
        compEdges _c@(Comp cnum _ a _) = edge <$> tagged (flattenB a)
         where
           edge (ni, Source (Bus ocnum opnum t) templ _) =
             printf "%s -> %s [%s]"
               (maybe (port Out (ocnum,opnum)) compLab mbSubOut)
               (port In (cnum,ni))
               (intercalate "," attrs)
            where
              mbSubOut :: Maybe CompId  -- Output component if a subgraph
              mbSubOut = case templ of Prim _       -> Nothing
                                       Subgraph g _ -> Just (outId g)
              attrs = (if isJust mbSubOut then [printf "ltail=cluster_%d" ocnum] else []) ++
                      label ++ constraint
  #ifdef ShallowDelay
              constraint | isDelay _c = ["constraint=false" ]
                         | otherwise  = []
  #else
              constraint = []
  #endif
  #ifdef NoBusLabel
              label = const [] t -- []
  #else
              -- Show the type per edge. I think I'd rather show in the output
              -- ports, but I don't know how to use a small font for those port
              -- labels but not for the operation label.
              -- label | t == Bool = []
              label = [printf "label=\"%s\"" (show t)]
  #endif
     port :: Dir -> (CompId,PortNum) -> String
     port dir (cnum,np) =
       printf "%s:%s" (compLab cnum) (portLab dir np)
     compLab :: CompId -> String
     compLab nc = 'c' : show nc
     portLab :: Dir -> PortNum -> String
     portLab dir np = printf "%s%d" (show dir) np
  
  -- sourceMap :: [Comp] -> SourceMap
  -- sourceMap = foldMap $ \ (Comp nc _ _ b) ->
  --               M.fromList [ (o,(busTy o,nc,np))
  --                          | (np,o) <- tagged (flatB b) ]
  
  segmentedDotString :: Unop String
  segmentedDotString = intercalate "\"+\"" . divvy
   where
     divvy [] = []
     divvy (splitAt yy_buf_size -> (pre,suf)) = pre : divvy suf
     yy_buf_size = 16370 -- 16384 - some overhead
  
  -- showBool :: Bool -> String
  -- showBool False = "F"
  -- showBool True  = "T"
  
  #endif
  
  {--------------------------------------------------------------------
      Type-specific support
  --------------------------------------------------------------------}
  
  -- GenBuses needed for data types appearing the external interfaces (and hence
  -- not removed during compilation).
  
  genBusesRep' :: (OkCAR a, GenBuses (Rep a)) =>
                  Template u v -> [Source] -> BusesM (Buses a)
  genBusesRep' templ ins = abstB <$> genBuses' templ ins
  
  -- tweakValRep :: (HasRep a, Tweakable (Rep a)) => Unop a
  -- tweakValRep = abst . tweakVal . repr
  
  tyRep :: forall a. GenBuses (Rep a) => Ty
  tyRep = ty @(Rep a)
  
  -- delayCRep :: (HasRep a, OkCAR a, GenBuses a, GenBuses (Rep a)) => a -> (a :> a)
  -- delayCRep a0 = abstC . delay (repr a0) . reprC
  
  genUnflattenB' :: (GenBuses a, GenBuses (Rep a)) => State [Source] (Buses a)
  genUnflattenB' = abstB <$> unflattenB'
  
  -- Omit temporarily for faster compilation
  #if 1
  
  #include "ConCat/AbsTy.inc"
  
  instance GenBuses (Proxy a) where
    genBuses' = genBusesRep'
    ty = tyRep @(Proxy a)
    unflattenB' = genUnflattenB'
  
  -- AbsTy(Proxy a)
  
  AbsTy((a,b,c))
  AbsTy((a,b,c,d))
  AbsTy(Maybe a)  -- Problematic ConstCat. See 2016-01-13 notes.
  -- AbsTy(Either a b)
  AbsTy(Complex a)
  
  -- Moving types to ShapedTypes
  
  -- AbsTy(Pair a)  -- See below
  -- AbsTy(RTree.Tree Z a)
  -- AbsTy(RTree.Tree (S n) a)
  -- AbsTy(LTree.Tree Z a)
  -- AbsTy(LTree.Tree (S n) a)
  -- AbsTy(Rag.Tree LU a)
  -- AbsTy(Rag.Tree (BU p q) a)
  -- AbsTy(Vec Z a)
  -- AbsTy(Vec (S n) a)
  -- TODO: Remove Vec instances & import. Switching to ShapedTypes.Vec
  -- Newtypes. Alternatively, don't use them in external interfaces.
  
  AbsTy(Sum a)
  AbsTy(Product a)
  AbsTy(All)
  AbsTy(Any)
  
  -- TODO: Rework instances for Vec n as well, since it has the same redundancy
  -- issue as Pair, in a subtler form. Probably also Ragged.
  
  -- Better yet, rework the Pair instances in a more generic form, e.g., using
  -- Traversable for genBuses', so that they become easy to generalize and apply
  -- easily and efficiently to Vec n and others.
  
  AbsTy(G.U1 p)
  AbsTy(G.Par1 p)
  AbsTy(G.K1 i c p)
  AbsTy(G.M1 i c f p)
  AbsTy((G.:+:) f g p)
  AbsTy((G.:*:) f g p)
  AbsTy((G.:.:) f g p)
  
  AbsTy(M.Identity a)
  AbsTy(M.ReaderT e m a)
  AbsTy(M.WriterT w m a)
  AbsTy(M.StateT s m a)
  
  AbsTy(Add a)
  
  #ifdef WithArr
  AbsTy(Arr a b)
  #endif
  
  #endif
  