text:
{-# 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

#if MIN_VERSION_GLASGOW_HASKELL(8,6,0,0)
{-# LANGUAGE NoStarIsType #-}
#endif

{-# 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)
genBus wrap t templ ins = seq (show t) $  --- * [Note seq]
                          -- 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)

-- [Note seq]: Without this seq, I'm getting non-termination with
-- `id @(Vector 4 Bool :* Bool)`. I don't know why. seq t isn't enough.

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 () => 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

-- 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

max_stars_repo_name: faezs/concat

max_issues_repo_name: faezs/concat

max_forks_repo_name: faezs/concat


text:
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -fno-warn-incomplete-uni-patterns #-}
{-# OPTIONS_GHC -fno-warn-missing-import-lists #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fno-warn-unused-top-binds #-}

module Spec.FDBStreaming.AggrTable
  ( tableProps,
  )
where

import Control.Monad (forM_, when)
import Data.ByteString (ByteString)
import Data.Data (Data)
import Data.Either (fromRight)
import Data.Int
import qualified Data.Map.Strict as Map
import Data.Maybe (fromMaybe)
import Data.Monoid (All, Any, Sum)
import Data.Persist (Persist)
import qualified Data.Persist as Persist
import Data.Semigroup (Max (Max), Min (Min))
import Data.Text (Text)
import Data.Word
import FDBStreaming.AggrTable as AT
import FDBStreaming.Message (Message (fromMessage, toMessage))
import FoundationDB (Database, runTransaction)
import qualified FoundationDB as FDB
import FoundationDB.Layer.Subspace (Subspace, extend)
import qualified FoundationDB.Layer.Tuple as FDB
import GHC.Generics (Generic)
import Numeric.Sum (KBNSum (..))
import Spec.FDBStreaming.Util (extendRand)
import Statistics.Monoid (CalcMean, MeanKBN, StatMonoid (..))
import Test.QuickCheck ((===), Arbitrary, Property, property)
import Test.QuickCheck.Instances.ByteString ()
import Test.QuickCheck.Instances.Text ()
import Test.QuickCheck.Instances.UUID ()
import Test.QuickCheck.Monadic as Monadic
import Test.Tasty
import qualified Test.Tasty.QuickCheck as QC

deriving via Double instance Arbitrary (Max Double)

deriving via Float instance Arbitrary (Min Float)

deriving via Int32 instance Arbitrary (Max Int32)

deriving via Int32 instance Arbitrary (Min Int32)

deriving via Int64 instance Arbitrary (Max Int64)

deriving via Int64 instance Arbitrary (Min Int64)

deriving via Word32 instance Arbitrary (Max Word32)

deriving via Word32 instance Arbitrary (Min Word32)

binaryProperty :: (Show a, Arbitrary a, Show b, Arbitrary b) => (a -> b -> Property) -> Property
binaryProperty x = property $ property x

ternaryProperty ::
  ( Show a,
    Arbitrary a,
    Show b,
    Arbitrary b,
    Show c,
    Arbitrary c
  ) =>
  (a -> b -> c -> Property) ->
  Property
ternaryProperty x = property $ property $ property x

propOrdTableKey :: (OrdTableKey k) => k -> k -> Property
propOrdTableKey k l =
  compare k l === compare (toKeyBytes k) (toKeyBytes l)

ordTableKeyProps :: TestTree
ordTableKeyProps =
  testGroup
    "OrdTableKey"
    [ QC.testProperty "works for ByteString" $ binaryProperty $ propOrdTableKey @ByteString,
      QC.testProperty "works for Text" $ binaryProperty $ propOrdTableKey @Text,
      QC.testProperty "works for Integer" $ binaryProperty $ propOrdTableKey @Integer,
      QC.testProperty "works for Float" $ binaryProperty $ propOrdTableKey @Float,
      QC.testProperty "works for Double" $ binaryProperty $ propOrdTableKey @Double,
      QC.testProperty "works for Bool" $ binaryProperty $ propOrdTableKey @Bool,
      QC.testProperty "works for 2-tuples" $ binaryProperty $ propOrdTableKey @(Bool, Double)
    ]

propMappendTable ::
  forall v.
  (Eq v, TableSemigroup v) =>
  Subspace ->
  Database ->
  ByteString ->
  v ->
  v ->
  Property
propMappendTable ss db tableName v1 v2 = monadicIO $ do
  ss' <- run $ extendRand ss
  let table = AggrTable (extend ss' [FDB.Bytes tableName]) 2 :: AggrTable Bool v
  let k = True
  run $ runTransaction db $ AT.set table 0 k v1
  run $ runTransaction db $ mappendBatch table 0 [(k, v2)]
  (Just v3) <- run $ runTransaction db $ AT.get table 0 k >>= FDB.await
  Monadic.assert (v3 == v1 <> v2)
  -- Test that we combine across partitions correctly when reading. TODO:
  -- refactor into separate test.
  run $ runTransaction db $ mappendBatch table 1 [(k, v1)]
  (Just v4) <- run $ runTransaction db $ AT.getRow table k
  Monadic.assert (v4 == v1 <> v2 <> v1)

mappendTableProps :: Subspace -> Database -> TestTree
mappendTableProps testSS db =
  testGroup
    "mappendTable"
    [ QC.testProperty "Works for (Sum Word32)" $ ternaryProperty (propMappendTable testSS db :: ByteString -> Sum Word32 -> Sum Word32 -> Property),
      QC.testProperty "Works for (Sum Int64)" $ ternaryProperty (propMappendTable testSS db :: ByteString -> Sum Int64 -> Sum Int64 -> Property),
      QC.testProperty "Works for (Max Double)" $ ternaryProperty (propMappendTable testSS db :: ByteString -> Max Double -> Max Double -> Property),
      QC.testProperty "Works for (Max Int32)" $ ternaryProperty (propMappendTable testSS db :: ByteString -> Max Int32 -> Max Int32 -> Property),
      QC.testProperty "Works for (Max Int64)" $ ternaryProperty (propMappendTable testSS db :: ByteString -> Max Int64 -> Max Int64 -> Property),
      QC.testProperty "Works for (Max Word32)" $ ternaryProperty (propMappendTable testSS db :: ByteString -> Max Word32 -> Max Word32 -> Property),
      QC.testProperty "Works for (Min Float)" $ ternaryProperty (propMappendTable testSS db :: ByteString -> Min Float -> Min Float -> Property),
      QC.testProperty "Works for (Min Int32)" $ ternaryProperty (propMappendTable testSS db :: ByteString -> Min Int32 -> Min Int32 -> Property),
      QC.testProperty "Works for (Min Word32)" $ ternaryProperty (propMappendTable testSS db :: ByteString -> Min Word32 -> Min Word32 -> Property),
      QC.testProperty "Works for Any" $ ternaryProperty (propMappendTable testSS db :: ByteString -> Any -> Any -> Property),
      QC.testProperty "Works for All" $ ternaryProperty (propMappendTable testSS db :: ByteString -> All -> All -> Property)
    ]

propTableRange ::
  forall v.
  (TableSemigroup v, RangeAccessibleTable v, Eq v) =>
  Subspace ->
  Database ->
  ByteString ->
  v ->
  Property
propTableRange ss db tableName v = monadicIO $ do
  ss' <- run $ extendRand ss
  let table = AggrTable (extend ss' [FDB.Bytes tableName]) 2 :: AggrTable Integer v
  forM_ [0 .. 10] $ \i -> run $ runTransaction db $ AT.set table 0 i v
  result <- run $ runTransaction db $ AT.getTableRange table 0 0 10
  let expected = Map.fromList [(i, v) | i <- [0 .. 10]]
  Monadic.assert (result == expected)
  -- Test that we combine across partitions correctly when reading. TODO:
  -- refactor into separate test.
  forM_ [0 .. 10] $ \i -> run $ runTransaction db $ AT.mappendBatch table 1 [(i, v)]
  result2 <- run $ runTransaction db $ AT.getRowRange table 0 10
  let expected2 = Map.fromList [(i, v <> v) | i <- [0 .. 10]]
  Monadic.assert (result2 == expected2)

tableRangeProps :: Subspace -> Database -> TestTree
tableRangeProps testSS db =
  testGroup
    "getTableRange"
    [ QC.testProperty "Works for (Sum Word32)" $ binaryProperty (propTableRange testSS db :: ByteString -> Sum Word32 -> Property),
      QC.testProperty "Works for (Sum Int32)" $ binaryProperty (propTableRange testSS db :: ByteString -> Sum Int32 -> Property),
      QC.testProperty "Works for Any" $ binaryProperty (propTableRange testSS db :: ByteString -> Any -> Property),
      QC.testProperty "Works for All" $ binaryProperty (propTableRange testSS db :: ByteString -> All -> Property),
      QC.testProperty "Works for (Max Double)" $ binaryProperty (propTableRange testSS db :: ByteString -> Max Double -> Property),
      QC.testProperty "Works for (Min Int64)" $ binaryProperty (propTableRange testSS db :: ByteString -> Min Int64 -> Property)
    ]

newtype Mean = Mean {unMean :: MeanKBN}
  deriving (Eq, Data, Show, Generic)
  deriving (Semigroup) via MeanKBN
  deriving (Monoid) via MeanKBN
  deriving (CalcMean) via MeanKBN

deriving instance Generic KBNSum

deriving instance Persist KBNSum

deriving instance Persist MeanKBN

deriving instance Persist Mean

instance Real a => StatMonoid Mean a where

  addValue (Mean m) a = Mean (addValue m a)

  singletonMonoid a = Mean (singletonMonoid a)

instance Message Mean where

  toMessage = Persist.encode

  fromMessage = fromRight (error "Failed to decode Mean") . Persist.decode

instance TableSemigroup Mean where

  mappendBatch = mappendMessageBatch

  set = setMessage

  get = getMessage

propNonAtomicSemigroup :: Real v => Subspace -> Database -> ByteString -> [v] -> Property
propNonAtomicSemigroup ss db tableName vs = monadicIO $ do
  ss' <- run $ extendRand ss
  let table = AggrTable (extend ss' [FDB.Bytes tableName]) 2 :: AggrTable () Mean
  let kvs = map (\v -> ((), singletonMonoid v)) vs
  run $ runTransaction db $ mappendBatch table 0 kvs
  run $ runTransaction db $ mappendBatch table 1 kvs
  let expectedResult = foldMap singletonMonoid (vs <> vs)
  result <- fromMaybe mempty <$> run (runTransaction db $ AT.getRow table ())
  when (expectedResult /= result) $ do
    run $ putStrLn $ "expected: " ++ show expectedResult
    run $ putStrLn $ "got: " ++ show result
  Monadic.assert (expectedResult == (result :: Mean))

nonAtomicSemigroupProps :: Subspace -> Database -> TestTree
nonAtomicSemigroupProps testSS db =
  testGroup
    "non-atomic table helper functions"
    [ QC.testProperty "Works for Kahan Mean" $ binaryProperty (propNonAtomicSemigroup testSS db :: ByteString -> [Integer] -> Property)
    ]

tableProps :: Subspace -> Database -> TestTree
tableProps testSS db =
  testGroup
    "AggrTable"
    [ nonAtomicSemigroupProps testSS db,
      ordTableKeyProps,
      mappendTableProps testSS db,
      tableRangeProps testSS db
    ]

ext: hs

max_stars_repo_name: crclark/fdb-streaming

max_issues_repo_name: crclark/fdb-streaming

max_forks_repo_name: crclark/fdb-streaming


text:
{-|
Module      : Example.Mnist
Description : MNIST traning example
Copyright   : (c) Anatoly Yakovenko, 2015-2016
License     : MIT
Maintainer  : aeyakovenko@gmail.com
Stability   : experimental
Portability : POSIX

This module implements an example traning the MNIST data set.  Using
the dataset parsing code from:
<https://github.com/mhwombat/backprop-example/blob/master/Mnist.hs>
-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
module Examples.Mnist (generateTrainBatches
                      ,generateTrainLabels
                      ,generateTestBatches
                      ,mnist
                      )where

import Control.Applicative((<|>))
import Control.Monad.Trans(liftIO)
import Control.Monad(when,forever,forM_, foldM_)
import qualified Data.ByteString.Lazy as BL
import Data.Binary.Get hiding(label)
import qualified Data.Binary as B
import Data.Word
import qualified Data.List.Split as S
import qualified Data.Array.Repa as R
import Codec.Compression.GZip as GZ
import Data.List.Split(chunksOf)
import Statistics.LinearRegression as S

import qualified Data.DNN.Trainer as T
import qualified Data.RBM as RB
import qualified Data.Matrix as M
import qualified Data.ImageUtils as I
import Data.Matrix(Matrix(..)
                  ,U
                  ,B
                  ,I
                  ,H
                  )
{-|
Train a network to recognize digits from the MNIST dataset.  Start by training
each layer as an RBM with the Contrastive Divergence algorithm.  Then finish
up the traning with Back-propagation.  Animate the weights as the traning
progresses.
-}
mnist :: IO ()
mnist = do
   let r1 = RB.new 0 785 530 --dimentions include the bias node
       r2 = RB.new 0 530 530 --sqrt(529) == 23
       r3 = RB.new 0 530 11

   -- train the first layer
   tr1 <- B.decodeFile "dist/rbm1" --decode if this layer is already been trained
      <|> do tr1 <- snd <$> (T.run [r1] $ trainCD "dist/rbm1.gif" 0.01)
             B.encodeFile "dist/rbm1" tr1 --save the layer to a file
             return tr1

   -- train the second layer
   tr2 <- B.decodeFile "dist/rbm2"
      <|> do tr2 <- snd <$> (T.run (tr1++[r2]) $ trainCD "dist/rbm2.gif" 0.001)
             B.encodeFile "dist/rbm2" tr2
             return tr2

   -- train the third layer
   tr3 <- B.decodeFile "dist/rbm3"
      <|> do tr3 <- snd <$> (T.run (tr2++[r3]) $ trainCD "dist/rbm3.gif" 0.001)
             B.encodeFile "dist/rbm3" tr3
             return tr3

   -- backprop
   let train pbp xx = do
            let name = "dist/bp" ++ (show xx)
                gif = name ++ ".gif"
            bp <- B.decodeFile name
               <|> do bp <- snd <$> (T.run pbp $ trainBP gif 0.01 0.001)
                      B.encodeFile name bp
                      return bp
            mapM_ (testBatch bp) [0..9] --print how well our network recognizes the images
            return bp
   foldM_ train tr3 [1::Int ..]  --train forever

-- max number of minibatches
maxCount :: Int
maxCount = 25000
-- how often to check the progress
testCount :: Int
testCount = 1000
-- size of the minibatch
rowCount :: Int
rowCount = 5

-- |train the last layer in the DNN via the CD algorithm
trainCD :: String -> Double ->  T.Trainer IO ()
trainCD file mine = forever $ do
  T.setLearnRate 0.001
  let batchids = [0..468::Int]
  forM_ batchids $ \ ix -> do
     big <- liftIO $ readBatch ix
     small <- mapM M.d2u $ M.splitRows rowCount big
     forM_ small $ \ batch -> do
        T.contraDiv batch
        cnt <- T.getCount
        when (0 == cnt `mod` testCount) $ do
           nns <- T.getDNN
           ww <- M.cast1 <$> M.transpose (last nns)
           liftIO $ I.appendGIF file ww
        when (0 == cnt `mod` testCount) $ do
           err <- T.reconErr big
           liftIO $ print (cnt, err)
           when (cnt >= maxCount || err < mine) $ T.finish_

-- |train the entire DNN via backprop
trainBP :: String -> Double -> Double -> T.Trainer IO ()
trainBP file lr mine = forever $ do
  T.setLearnRate lr
  let batchids = [0..468::Int]
  forM_ batchids $ \ ix -> do
     bbatch <- liftIO $ readBatch ix
     blabel <- liftIO $ readLabel ix
     sbatch <- mapM M.d2u $ M.splitRows rowCount bbatch
     slabel <- mapM M.d2u $ M.splitRows rowCount blabel
     forM_ (zip sbatch slabel) $ \ (batch,label) -> do
        T.backProp batch label
        cnt <- T.getCount
        when (0 == cnt `mod` testCount) $ do
           gen <- T.backward (Matrix $ toLabelM [0..9])
           liftIO $ I.appendGIF file gen
        when (0 == cnt `mod` testCount) $ do
           err <- T.forwardErr bbatch blabel
           liftIO $ print (cnt, err)
           when (cnt >= maxCount || err < mine) $ T.finish_

-- |compute the correlation between the labels and the DNN output
testBatch :: [Matrix U I H] -> Int -> IO ()
testBatch nns ix = do
   let name = "dist/test" ++ (show ix)
   bxi <- Matrix <$> readArray name
   let bxh = M.fromList (M.row bxi, 11) $ concat $ replicate (M.row bxi) $ labelVector ix
   (bxh',_) <- T.run nns $ T.feedForward bxi
   let cor = S.correl (M.toUnboxed bxh') (M.toUnboxed bxh)
   print (ix, cor)

-- |Generate a batch of images with bias values for training.
generateTrainBatches :: IO ()
generateTrainBatches = do
   images <- readImages "dist/train-images-idx3-ubyte.gz"
   let batches = map toMatrix $ chunksOf 128 images
   (flip mapM_) (zip [0::Integer ..] batches) $ \ (ix, bb) -> do
      let name = "dist/train" ++ (show ix)
      writeArray name bb

-- |Generate a batch of of matching labels with bias values.
generateTrainLabels :: IO ()
generateTrainLabels = do
   labels <- readLabels "dist/train-labels-idx1-ubyte.gz"
   let batches = map toLabelM $ chunksOf 128 labels
   (flip mapM_) (zip [0::Integer ..] batches) $ \ (ix, bb) -> do
      let name = "dist/label" ++ (show ix)
      writeArray name bb

-- |Generate a the test images with bias values sorted by label.
generateTestBatches :: IO ()
generateTestBatches = do
   images <- readImages "dist/t10k-images-idx3-ubyte.gz"
   labels <- readLabels "dist/t10k-labels-idx1-ubyte.gz"
   (flip mapM_) ([0..9]) $ \ ix -> do
      let name = "dist/test" ++ (show ix)
      let batch = filter (((==) ix) . fst) $ zip labels images
      let bb = toMatrix $ snd $ unzip batch
      writeArray name bb

-- |generate a 2d array from the list of images
-- |add the bias node as the first node to each image
toMatrix :: [Image] -> R.Array R.U R.DIM2 Double
toMatrix images = m
  where
        m = R.fromListUnboxed (R.Z R.:. len R.:. maxsz) (concatMap pixels images)
        maxsz = 1 + (maximum $ map (\ ii -> (iRows ii) * (iColumns ii)) images)
        len = length images
        pixels im = take maxsz $ 1:((normalisedData im) ++ [0..])

-- |file IO utils
readImages :: FilePath -> IO [Image]
readImages filename = do
  content <- GZ.decompress <$> BL.readFile filename
  let (_, _, r, c, unpackedData) = runGet deserialiseHeader content
  return (map (Image (fromIntegral r) (fromIntegral c)) unpackedData)

writeArray :: String -> R.Array R.U R.DIM2 Double -> IO ()
writeArray fileName array = do
   let (R.Z R.:. r R.:. c) = R.extent array
   B.encodeFile fileName (r,c,R.toList array)

readArray ::String -> IO (R.Array R.U R.DIM2 Double)
readArray fileName = do
   (r,c,ls) <- B.decodeFile fileName
   return $ R.fromListUnboxed  (R.Z R.:. r R.:. c) ls

readBatch :: Int -> IO (Matrix U B I)
readBatch ix = Matrix <$> readArray name
   where name = "dist/train" ++ (show ix)

readLabel :: Int -> IO (Matrix U B H)
readLabel ix = Matrix <$> readArray name
   where name = "dist/label" ++ (show ix)

-- |MNIST image parsing code
-- |from https://github.com/mhwombat/backprop-example/blob/master/Mnist.hs
data Image = Image {
      iRows :: Int
    , iColumns :: Int
    , iPixels :: [Word8]
    } deriving (Eq, Show)

normalisedData :: Image -> [Double]
normalisedData image = map normalisePixel (iPixels image)

normalisePixel :: Word8 -> Double
normalisePixel p = (fromIntegral p) / 255.0

toLabelM :: [Int] -> R.Array R.U R.DIM2 Double
toLabelM labels = m
  where
        m = R.fromListUnboxed (R.Z R.:. len R.:. 11) (concatMap labelVector labels)
        len = length labels

labelVector :: Int -> [Double]
labelVector ll = take 11 $ 1.0:(start ++ end)
   where start = take ll $ repeat 0.0
         end = 1.0 : repeat 0.0

{-|
MNIST label file format

[offset] [type]          [value]          [description]
0000     32 bit integer  0x00000801(2049) magic number (MSB first)
0004     32 bit integer  10000            number of items
0008     unsigned byte   ??               label
0009     unsigned byte   ??               label
........
xxxx     unsigned byte   ??               label

The labels values are 0 to 9.
-}
deserialiseLabels :: Get (Word32, Word32, [Word8])
deserialiseLabels = do
  magicNumber <- getWord32be
  count <- getWord32be
  labelData <- getRemainingLazyByteString
  let labels = BL.unpack labelData
  return (magicNumber, count, labels)

readLabels :: FilePath -> IO [Int]
readLabels filename = do
  content <- GZ.decompress <$> BL.readFile filename
  let (_, _, labels) = runGet deserialiseLabels content
  return (map fromIntegral labels)

{-|
MNIST Image file format

[offset] [type]          [value]          [description]
0000     32 bit integer  0x00000803(2051) magic number
0004     32 bit integer  ??               number of images
0008     32 bit integer  28               number of rows
0012     32 bit integer  28               number of columns
0016     unsigned byte   ??               pixel
0017     unsigned byte   ??               pixel
........
xxxx     unsigned byte   ??               pixel

Pixels are organized row-wise. Pixel values are 0 to 255. 0 means background (white), 255
means foreground (black).
-}
deserialiseHeader :: Get (Word32, Word32, Word32, Word32, [[Word8]])
deserialiseHeader = do
  magicNumber <- getWord32be
  imageCount <- getWord32be
  r <- getWord32be
  c <- getWord32be
  packedData <- getRemainingLazyByteString
  let len = fromIntegral (r * c)
  let unpackedData = S.chunksOf len (BL.unpack packedData)
  return (magicNumber, imageCount, r, c, unpackedData)

max_stars_repo_name: sakridge/rbm

max_issues_repo_name: sakridge/rbm

max_forks_repo_name: sakridge/rbm


text:
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}

{-# LANGUAGE CPP                 #-}
{-# LANGUAGE ConstraintKinds     #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell     #-}
{-# LANGUAGE TypeOperators       #-}

module Test.Grenade.Layers.Add where

import           Data.Constraint
import           Data.Maybe                   (fromJust)
import           Data.Proxy
import           Unsafe.Coerce

import           GHC.TypeLits

import           Grenade.Core
import           Grenade.Layers.Add

import           Numeric.LinearAlgebra        hiding (R, konst, randomVector,
                                               uniformSample, (===), reshape)
import qualified Numeric.LinearAlgebra.Data   as D
import           Numeric.LinearAlgebra.Static (L, R)
import qualified Numeric.LinearAlgebra.Static as H

import           Hedgehog

import           Test.Hedgehog.Compat
import           Test.Hedgehog.Hmatrix

prop_add_zero_does_nothing = property $ do
  height   :: Int <- forAll $ choose 2 100
  width    :: Int <- forAll $ choose 2 100
  channels :: Int <- forAll $ choose 2 100

  case (someNatVal (fromIntegral height), someNatVal (fromIntegral width), someNatVal (fromIntegral channels)) of
    (Just (SomeNat (Proxy :: Proxy h)), Just (SomeNat (Proxy :: Proxy w)), Just (SomeNat (Proxy :: Proxy c))) -> do
      input :: S ('D3 h w c) <- forAll genOfShape

      let layer    = initAdd :: Add c 1 1
          S3D out  = snd $ runForwards layer input :: S ('D3 h w c)
          S3D inp' = input :: S ('D3 h w c)

      H.extract inp' === H.extract out

prop_add_per_channel_words_as_expected = property $ do
  height   :: Int <- forAll $ choose 2 100
  width    :: Int <- forAll $ choose 2 100

  case (someNatVal (fromIntegral height), someNatVal (fromIntegral width)) of
    (Just (SomeNat (Proxy :: Proxy h)), Just (SomeNat (Proxy :: Proxy w))) ->
      case ( unsafeCoerce (Dict :: Dict ()) :: Dict ( (h * 3) ~ (h + h + h) ) ) of
        Dict -> do
          channel_one   :: R (h * w) <- forAll randomVector
          channel_two   :: R (h * w) <- forAll randomVector
          channel_three :: R (h * w) <- forAll randomVector
          bias          :: R 3       <- forAll randomVector

          let reshape = fromJust . H.create . (D.reshape width) . H.extract
              c1      = reshape channel_one   :: L h w
              c2      = reshape channel_two   :: L h w
              c3      = reshape channel_three :: L h w

              bias' = H.extract bias

              o1 = H.dmmap (\a -> a + bias' ! 0) c1 :: L h w
              o2 = H.dmmap (\a -> a + bias' ! 1) c2 :: L h w
              o3 = H.dmmap (\a -> a + bias' ! 2) c3 :: L h w

              out = o1 H.=== o2 H.=== o3 :: L (h * 3) w
              inp = c1 H.=== c2 H.=== c3 :: L (h * 3) w

              layer    = Add bias :: Add 3 1 1
              inp'     = S3D inp :: S ('D3 h w 3)
              S3D out' = snd $ runForwards layer inp' :: S ('D3 h w 3)

          H.extract out === H.extract out'

tests :: IO Bool
tests = checkParallel $$(discover)

max_stars_repo_name: th-char/grenade

max_issues_repo_name: th-char/grenade

max_forks_repo_name: th-char/grenade