{-# LANGUAGE CPP #-}

-- #define NoOptimizeCircuit

-- #define NoHashCons

-- #define NoIfBotOpt
-- #define NoIdempotence

-- -- Improves hash consing, but can obscure equivalent circuits
-- #define NoCommute

-- #define NoBusLabel

#define MealyToArrow

-- -- Whether a delay/cons element is considered further from input
-- #define ShallowDelay

-- #define NoMend

{-# LANGUAGE TypeFamilies, TypeOperators, ConstraintKinds #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts, MultiParamTypeClasses #-}
{-# LANGUAGE ViewPatterns, TupleSections #-}
{-# LANGUAGE GeneralizedNewtypeDeriving, StandaloneDeriving #-}
{-# LANGUAGE ExistentialQuantification, TypeSynonymInstances, GADTs #-}
{-# LANGUAGE Rank2Types, ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-} -- see below
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-} -- for LU & BU
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RecursiveDo #-}
{-# LANGUAGE DeriveFunctor, DeriveDataTypeable #-}
{-# LANGUAGE TypeApplications, AllowAmbiguousTypes #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE UndecidableSuperClasses #-}  -- GenBuses

-- TODO: trim language extensions

#ifdef ChurchSums
{-# LANGUAGE LiberalTypeSynonyms, ImpredicativeTypes, EmptyDataDecls #-}
#endif

{-# LANGUAGE NoStarIsType #-}

{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_GHC -fno-warn-orphans #-} -- for OkayArr
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}

-- {-# OPTIONS_GHC -fdefer-typed-holes #-}  -- TEMP
-- {-# OPTIONS_GHC -fdefer-type-errors #-}  -- TEMP

-- This module compiles pretty slowly. Some of my pattern matching style led to
-- the following warning:
--
--        Pattern match checker exceeded (2000000) iterations in
--        a case alternative. (Use -fmax-pmcheck-iterations=n
--        to set the maximun number of iterations to n)
--
-- I've simplified my style by replacing uses of the Eql macro by explicit
-- equality checks. To find at least some problematic definitions, lower
-- -fmax-pmcheck-iterations from default of 2000000. I'd like to simplify
-- further. Ideally, use constructor pattern matching in the rewrites, instead
-- of comparing strings.

{-# OPTIONS_GHC -fmax-pmcheck-iterations=1000000 #-}

{-# OPTIONS_GHC -fno-warn-unused-imports #-} -- TEMP
{-# OPTIONS_GHC -fno-warn-unused-binds   #-} -- TEMP

----------------------------------------------------------------------
-- |
-- Module      :  ConCat.Circuit
-- Copyright   :  (c) 2016 Conal Elliott
-- License     :  BSD3
--
-- Maintainer  :  conal@conal.net
-- Stability   :  experimental
--
-- Circuit representation
----------------------------------------------------------------------

module ConCat.Circuit
  ( CircuitM, (:>)
  , Bus(..),Comp(..),Input,Output, Ty(..), busTy, Source(..), Template(..)
  , GenBuses(..), GS, genBusesRep', tyRep
  -- , delayCRep, unDelayName
  , namedC, constC -- , constS
  , genUnflattenB'
  , SourceToBuses(..), CompS(..), simpleComp
  , mkGraph
  , Attr
  , graphDot, writeDot, displayDot,Name,Report,Graph
  -- , simpleComp
  , tagged
  , systemSuccess
  -- For AbsTy
  , BusesM, abstB,abstC,reprC,Buses(..)
  , OkCAR
  -- , Ty(..)
  ) where

import Prelude hiding (id,(.),curry,uncurry,const,sequence,zip)

import Data.Monoid ({-mempty,-}(<>),Sum,Product,All,Any)
-- import Data.Newtypes.PrettyDouble
-- import Data.Functor ((<$>))
import Control.Applicative ({-Applicative(..),-}liftA2)
import Control.Monad (unless)
import Control.Arrow (arr,Kleisli(..))
import Data.Foldable ({-foldMap,-}toList)
import qualified GHC.Generics as G
import Data.Functor.Classes (Show1,showsPrec1)
import Data.Void (Void)
import Data.Function (on)
import Data.Maybe (fromMaybe,isJust,maybeToList)
import Data.List (intercalate,group,sort,stripPrefix)
import Data.Char (isAscii)
import Data.Complex (Complex)
import Data.Proxy
import GHC.TypeLits -- (natVal)
#ifndef MealyToArrow
import Data.List (partition)
#endif
import Data.Map (Map)
import qualified Data.Map as M  -- accidental qualifier clash with mtl. Change one.
-- import Data.Set (Set)
import qualified Data.Set as S
import Data.Sequence (Seq,singleton)
import Text.Printf (printf)
import Debug.Trace (trace)
-- import Data.Coerce                      -- TODO: imports
import Unsafe.Coerce
-- import GHC.Exts (Coercible) -- ,coerce
import Data.Typeable (TypeRep,Typeable,eqT,cast) -- ,Proxy(..),typeOf
import Data.Type.Equality ((:~:)(..))
import GHC.Types (Constraint)
import Data.Kind (Type)

import Data.Constraint (Dict(..),(:-)(..),(\\))
import Data.Pointed (Pointed)
import Data.Key (Zip(..))
import Data.Distributive (Distributive)
import Data.Distributive (distribute)
import Data.Functor.Rep (Representable(tabulate,index))
import qualified Data.Functor.Rep as R

import qualified System.Info as SI
import System.Process (system) -- ,readProcess
import System.Directory (createDirectoryIfMissing)
import System.Exit (ExitCode(ExitSuccess))

#define WithArr

#ifdef VectorSized
import GHC.TypeLits (Nat,KnownNat)
import Data.Vector.Sized (Vector)
#endif
#ifdef WithArr
import ConCat.TArr (HasFin',Arr)
#endif
import ConCat.Known

-- mtl
import Control.Monad.State (State,execState,StateT)

-- For AbsTy
import qualified Data.Functor.Identity as M
import qualified Control.Monad.Trans.Reader as M
import qualified Control.Monad.Trans.Writer as M
import qualified Control.Monad.State as M

-- import TypeUnary.Vec hiding (get)

import ConCat.Misc ((:*),(:+),Unop,Binop,Yes1,typeR,transpose)
-- import ConCat.Complex (Complex(..))
import ConCat.Rep
import ConCat.Additive (Additive(..),Add)
import qualified ConCat.Category
import ConCat.AltCat  -- for AbsTy
-- import ConCat.AltCat (Uncurriable(..),funIf,repIf,unitIf,prodIf,Finite)

{--------------------------------------------------------------------
    Buses
--------------------------------------------------------------------}

-- Component (primitive) type
data Ty = Void | Unit | Bool | Int | Integer | Float | Double
        | Finite Integer  -- Remove?
        | Vector Integer Ty
        | Prod Ty Ty
        | Sum Ty Ty
        | Fun Ty Ty
  deriving (Ty -> Ty -> Bool
(Ty -> Ty -> Bool) -> (Ty -> Ty -> Bool) -> Eq Ty
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Ty -> Ty -> Bool
== :: Ty -> Ty -> Bool
$c/= :: Ty -> Ty -> Bool
/= :: Ty -> Ty -> Bool
Eq,Eq Ty
Eq Ty
-> (Ty -> Ty -> Ordering)
-> (Ty -> Ty -> Bool)
-> (Ty -> Ty -> Bool)
-> (Ty -> Ty -> Bool)
-> (Ty -> Ty -> Bool)
-> (Ty -> Ty -> Ty)
-> (Ty -> Ty -> Ty)
-> Ord Ty
Ty -> Ty -> Bool
Ty -> Ty -> Ordering
Ty -> Ty -> Ty
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Ty -> Ty -> Ordering
compare :: Ty -> Ty -> Ordering
$c< :: Ty -> Ty -> Bool
< :: Ty -> Ty -> Bool
$c<= :: Ty -> Ty -> Bool
<= :: Ty -> Ty -> Bool
$c> :: Ty -> Ty -> Bool
> :: Ty -> Ty -> Bool
$c>= :: Ty -> Ty -> Bool
>= :: Ty -> Ty -> Bool
$cmax :: Ty -> Ty -> Ty
max :: Ty -> Ty -> Ty
$cmin :: Ty -> Ty -> Ty
min :: Ty -> Ty -> Ty
Ord)

instance Show Ty where
  showsPrec :: Int -> Ty -> String -> String
showsPrec Int
_ Ty
Void    = String -> String -> String
showString String
"Void"
  showsPrec Int
_ Ty
Unit    = String -> String -> String
showString String
"()"
  showsPrec Int
_ Ty
Bool    = String -> String -> String
showString String
"Bool"
  showsPrec Int
_ Ty
Int     = String -> String -> String
showString String
"Int"
  showsPrec Int
_ Ty
Integer = String -> String -> String
showString String
"Integer"
  showsPrec Int
_ Ty
Float   = String -> String -> String
showString String
"Float"
  showsPrec Int
_ Ty
Double  = String -> String -> String
showString String
"Double" -- "R"
  showsPrec Int
p (Sum Ty
a Ty
b) = Bool -> (String -> String) -> String -> String
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
6) ((String -> String) -> String -> String)
-> (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$
    Int -> Ty -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec Int
6 Ty
a (String -> String) -> (String -> String) -> String -> String
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. String -> String -> String
showString String
" + " (String -> String) -> (String -> String) -> String -> String
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Int -> Ty -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec Int
6 Ty
b
  showsPrec Int
p (Prod Ty
a Ty
b) = Bool -> (String -> String) -> String -> String
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
7) ((String -> String) -> String -> String)
-> (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$
    Int -> Ty -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec Int
7 Ty
a (String -> String) -> (String -> String) -> String -> String
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. String -> String -> String
showString String
" × " (String -> String) -> (String -> String) -> String -> String
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Int -> Ty -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec Int
7 Ty
b
  showsPrec Int
p (Finite Integer
n) = Bool -> (String -> String) -> String -> String
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
9) ((String -> String) -> String -> String)
-> (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$
    String -> String -> String
showString String
"Finite " (String -> String) -> (String -> String) -> String -> String
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Int -> Integer -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec Int
9 Integer
n
  showsPrec Int
p (Vector Integer
n Ty
b) = Bool -> (String -> String) -> String -> String
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
9) ((String -> String) -> String -> String)
-> (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$
    String -> String -> String
showString String
"Vector " (String -> String) -> (String -> String) -> String -> String
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Int -> Integer -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec Int
9 Integer
n (String -> String) -> (String -> String) -> String -> String
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. String -> String -> String
showString String
" " (String -> String) -> (String -> String) -> String -> String
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Int -> Ty -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec Int
9 Ty
b
  showsPrec Int
p (Fun Ty
a Ty
b) = Bool -> (String -> String) -> String -> String
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
1) ((String -> String) -> String -> String)
-> (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$
    Int -> Ty -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec Int
1 Ty
a (String -> String) -> (String -> String) -> String -> String
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. String -> String -> String
showString String
" → " (String -> String) -> (String -> String) -> String -> String
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Int -> Ty -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec Int
0 Ty
b

-- Data bus: component id, output index, type; *or* subgraph ID
data Bus = Bus CompId Int Ty deriving Int -> Bus -> String -> String
[Bus] -> String -> String
Bus -> String
(Int -> Bus -> String -> String)
-> (Bus -> String) -> ([Bus] -> String -> String) -> Show Bus
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Bus -> String -> String
showsPrec :: Int -> Bus -> String -> String
$cshow :: Bus -> String
show :: Bus -> String
$cshowList :: [Bus] -> String -> String
showList :: [Bus] -> String -> String
Show

type Input  = Bus
type Output = Bus

-- Identifying information for a bus. Faster comparisons without the type.
busId :: Bus -> (CompId,Int)
busId :: Bus -> (Int, Int)
busId (Bus Int
c Int
o Ty
_) = (Int
c,Int
o)

busTy :: Bus -> Ty
busTy :: Bus -> Ty
busTy (Bus Int
_ Int
_ Ty
t) = Ty
t

instance Eq  Bus where == :: Bus -> Bus -> Bool
(==) = (Int, Int) -> (Int, Int) -> Bool
forall a. Eq a => a -> a -> Bool
(==) ((Int, Int) -> (Int, Int) -> Bool)
-> (Bus -> (Int, Int)) -> Bus -> Bus -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Bus -> (Int, Int)
busId
instance Ord Bus where compare :: Bus -> Bus -> Ordering
compare = (Int, Int) -> (Int, Int) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ((Int, Int) -> (Int, Int) -> Ordering)
-> (Bus -> (Int, Int)) -> Bus -> Bus -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Bus -> (Int, Int)
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 $mPSource :: forall {r}.
Source -> (Bus -> String -> [Source] -> r) -> ((# #) -> r) -> r
$bPSource :: Bus -> String -> [Source] -> Source
PSource b p ss = Source b (Prim p) ss

deriving instance Show Source

sourceBus :: Source -> Bus
sourceBus :: Source -> Bus
sourceBus (Source Bus
b Template a b
_ [Source]
_) = Bus
b

instance Eq  Source where == :: Source -> Source -> Bool
(==) = Bus -> Bus -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Bus -> Bus -> Bool) -> (Source -> Bus) -> Source -> Source -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Source -> Bus
sourceBus
instance Ord Source where compare :: Source -> Source -> Ordering
compare = Bus -> Bus -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Bus -> Bus -> Ordering)
-> (Source -> Bus) -> Source -> Source -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Source -> Bus
sourceBus

newBus :: Ty -> Int -> CircuitM Bus
newBus :: Ty -> Int -> CircuitM Bus
newBus Ty
t Int
o = -- trace "newBus" $
              (\ Int
c -> Int -> Int -> Ty -> Bus
Bus Int
c Int
o Ty
t) (Int -> Bus) -> StateT (Int, CompInfo) Identity Int -> CircuitM Bus
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Int, CompInfo) -> Int) -> StateT (Int, CompInfo) Identity Int
forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
M.gets (Int, CompInfo) -> Int
forall a b. (a, b) -> a
fst

newSource ::  Ty -> Template a b -> [Source] -> Int -> CircuitM Source
newSource :: forall a b.
Ty -> Template a b -> [Source] -> Int -> CircuitM Source
newSource Ty
t Template a b
templ [Source]
ins Int
o = -- trace "newSource" $
                         (\ Bus
b -> Bus -> Template a b -> [Source] -> Source
forall a b. Bus -> Template a b -> [Source] -> Source
Source Bus
b Template a b
templ [Source]
ins) (Bus -> Source) -> CircuitM Bus -> CircuitM Source
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Ty -> Int -> CircuitM Bus
newBus Ty
t Int
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 :: Int -> Buses a -> String -> String
showsPrec Int
_ Buses a
UnitB        = String -> String -> String
showString String
"UnitB"
  showsPrec Int
p (PrimB Source
s)    = Int -> String -> Source -> String -> String
forall a. Show a => Int -> String -> a -> String -> String
showsApp1 Int
p String
"PrimB" Source
s
  showsPrec Int
p (ProdB Buses a
a Buses b
b)  = Int -> String -> Buses a -> Buses b -> String -> String
forall a b.
(Show a, Show b) =>
Int -> String -> a -> b -> String -> String
showsApp2 Int
p String
"ProdB" Buses a
a Buses b
b
  showsPrec Int
p (IxProdB h (Buses a)
as) = Int -> String -> h (Buses a) -> String -> String
forall (h :: Type -> Type) a.
(Show1 h, Show a) =>
Int -> String -> h a -> String -> String
showsAppF Int
p String
"IxProdB " h (Buses a)
as
  showsPrec Int
p (ConvertB Buses a
a) = Int -> String -> Buses a -> String -> String
forall a. Show a => Int -> String -> a -> String -> String
showsApp1 Int
p String
"ConvertB " Buses a
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 :: Int -> (String -> String) -> String -> String
appParen Int
p = Bool -> (String -> String) -> String -> String
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
10)

shap :: Show a => a -> ShowS
shap :: forall a. Show a => a -> String -> String
shap a
a = Char -> String -> String
showChar Char
' ' (String -> String) -> (String -> String) -> String -> String
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Int -> a -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec Int
10 a
a

showsApp1 :: Show a => Int -> String -> a -> ShowS
showsApp1 :: forall a. Show a => Int -> String -> a -> String -> String
showsApp1 Int
p String
f a
a = Int -> (String -> String) -> String -> String
appParen Int
p ((String -> String) -> String -> String)
-> (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String -> String
showString String
f (String -> String) -> (String -> String) -> String -> String
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. a -> String -> String
forall a. Show a => a -> String -> String
shap a
a

showsApp2 :: (Show a, Show b) => Int -> String -> a -> b -> ShowS
showsApp2 :: forall a b.
(Show a, Show b) =>
Int -> String -> a -> b -> String -> String
showsApp2 Int
p String
f a
a b
b = Int -> (String -> String) -> String -> String
appParen Int
p ((String -> String) -> String -> String)
-> (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String -> String
showString String
f (String -> String) -> (String -> String) -> String -> String
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. a -> String -> String
forall a. Show a => a -> String -> String
shap a
a (String -> String) -> (String -> String) -> String -> String
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. b -> String -> String
forall a. Show a => a -> String -> String
shap b
b

showsAppF :: (Show1 h, Show a) => Int -> String -> h a -> ShowS
showsAppF :: forall (h :: Type -> Type) a.
(Show1 h, Show a) =>
Int -> String -> h a -> String -> String
showsAppF Int
p String
f h a
as = Int -> (String -> String) -> String -> String
appParen Int
p ((String -> String) -> String -> String)
-> (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String -> String
showString String
f (String -> String) -> (String -> String) -> String -> String
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Char -> String -> String
showChar Char
' ' (String -> String) -> (String -> String) -> String -> String
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Int -> h a -> String -> String
forall (f :: Type -> Type) a.
(Show1 f, Show a) =>
Int -> f a -> String -> String
showsPrec1 Int
10 h a
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 :: forall b a.
GenBuses b =>
Template a b -> [Source] -> CircuitM (Buses b)
genBuses Template a b
templ [Source]
ins = -- trace ("genBuses " ++ show templ ++ " " ++ show ins) $
                     StateT Int (StateT (Int, CompInfo) Identity) (Buses b)
-> Int -> StateT (Int, CompInfo) Identity (Buses b)
forall (m :: Type -> Type) s a. Monad m => StateT s m a -> s -> m a
M.evalStateT (Template a b
-> [Source]
-> StateT Int (StateT (Int, CompInfo) Identity) (Buses b)
forall a u v.
GenBuses a =>
Template u v -> [Source] -> BusesM (Buses a)
forall u v.
Template u v
-> [Source]
-> StateT Int (StateT (Int, CompInfo) Identity) (Buses b)
genBuses' Template a b
templ [Source]
ins) Int
0

type BusesM = StateT Int CircuitM

class GenBuses a where
  genBuses' :: Template u v -> [Source] -> BusesM (Buses a)
  -- delay :: a -> (a :> a)
  ty :: Ty
  unflattenB' :: State [Source] (Buses a)

type GS a = (GenBuses a, Show a)

genBus :: (Source -> Buses a) -> Ty
       -> Template u v -> [Source] -> BusesM (Buses a)
-- Without this @seq (show t)@, I'm getting non-termination with
-- `id @(Vector 4 Bool :* Bool)`. I don't know why @seq t@ isn't enough.
genBus :: forall a u v.
(Source -> Buses a)
-> Ty -> Template u v -> [Source] -> BusesM (Buses a)
genBus Source -> Buses a
wrap Ty
t Template u v
templ [Source]
ins = String -> BusesM (Buses a) -> BusesM (Buses a)
forall a b. a -> b -> b
seq (Ty -> String
forall a. Show a => a -> String
show Ty
t) (BusesM (Buses a) -> BusesM (Buses a))
-> BusesM (Buses a) -> BusesM (Buses a)
forall a b. (a -> b) -> a -> b
$
                          -- seq t $
                          -- trace ("genBus " ++ show t) $
                          do Int
o <- StateT Int (StateT (Int, CompInfo) Identity) Int
forall s (m :: Type -> Type). MonadState s m => m s
M.get
                             Source
src <- CircuitM Source
-> StateT Int (StateT (Int, CompInfo) Identity) Source
forall (m :: Type -> Type) a. Monad m => m a -> StateT Int m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
M.lift (Ty -> Template u v -> [Source] -> Int -> CircuitM Source
forall a b.
Ty -> Template a b -> [Source] -> Int -> CircuitM Source
newSource Ty
t Template u v
templ [Source]
ins Int
o)
                             Int -> StateT Int (StateT (Int, CompInfo) Identity) ()
forall s (m :: Type -> Type). MonadState s m => s -> m ()
M.put (Int
oInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
                             Buses a -> BusesM (Buses a)
forall a. a -> StateT Int (StateT (Int, CompInfo) Identity) a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Source -> Buses a
wrap Source
src)


unflattenB :: GenBuses a => [Source] -> Buses a
unflattenB :: forall a. GenBuses a => [Source] -> Buses a
unflattenB [Source]
sources | [] <- [Source]
rest = Buses a
a
                   | Bool
otherwise  = String -> Buses a
forall a. HasCallStack => String -> a
error (String
"unflattenB: extra sources " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Source] -> String
forall a. Show a => a -> String
show [Source]
rest)
 where
   (Buses a
a,[Source]
rest) = State [Source] (Buses a) -> [Source] -> (Buses a, [Source])
forall s a. State s a -> s -> (a, s)
M.runState State [Source] (Buses a)
forall a. GenBuses a => State [Source] (Buses a)
unflattenB' [Source]
sources

-- TODO: Remove this instance when we stop needing GenBuses for Vector index
instance GenBuses Void where
  genBuses' :: forall u v. Template u v -> [Source] -> BusesM (Buses Void)
genBuses' = String -> Template u v -> [Source] -> BusesM (Buses Void)
forall a. HasCallStack => String -> a
error String
"genBuses' for Void"
  ty :: Ty
ty = Ty
Void
  unflattenB' :: State [Source] (Buses Void)
unflattenB' = String -> State [Source] (Buses Void)
forall a. HasCallStack => String -> a
error String
"unflattenB' for Void"

instance GenBuses () where
  genBuses' :: forall u v. Template u v -> [Source] -> BusesM (Buses ())
genBuses' Template u v
_ [Source]
_ = Buses () -> BusesM (Buses ())
forall a. a -> StateT Int (StateT (Int, CompInfo) Identity) a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Buses ()
UnitB
  -- delay () = id
  ty :: Ty
ty = Ty
Unit
  unflattenB' :: State [Source] (Buses ())
unflattenB' = Buses () -> State [Source] (Buses ())
forall a. a -> StateT [Source] Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Buses ()
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 :: forall a u v.
GenBuses a =>
Template u v -> [Source] -> BusesM (Buses a)
genPrimBus = (Source -> Buses a)
-> Ty -> Template u v -> [Source] -> BusesM (Buses a)
forall a u v.
(Source -> Buses a)
-> Ty -> Template u v -> [Source] -> BusesM (Buses a)
genBus Source -> Buses a
forall b. Source -> Buses b
PrimB (forall a. GenBuses a => Ty
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 :: forall a. State [Source] (Buses a)
unflattenPrimB = do [Source]
ss0 <- StateT [Source] Identity [Source]
forall s (m :: Type -> Type). MonadState s m => m s
M.get
                    case [Source]
ss0 of
                      Source
s:[Source]
ss -> do [Source] -> StateT [Source] Identity ()
forall s (m :: Type -> Type). MonadState s m => s -> m ()
M.put [Source]
ss
                                 Buses a -> State [Source] (Buses a)
forall a. a -> StateT [Source] Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Source -> Buses a
forall b. Source -> Buses b
PrimB Source
s)
                      []   -> String -> State [Source] (Buses a)
forall a. HasCallStack => String -> a
error String
"unflattenPrimB: expected non-empty list"
                                -- TODO: can we do better than raise an error here?

instance GenBuses Bool where
  genBuses' :: forall u v. Template u v -> [Source] -> BusesM (Buses Bool)
genBuses' = Template u v -> [Source] -> BusesM (Buses Bool)
forall a u v.
GenBuses a =>
Template u v -> [Source] -> BusesM (Buses a)
genPrimBus
  -- delay = primDelay
  ty :: Ty
ty = Ty
Bool
  unflattenB' :: State [Source] (Buses Bool)
unflattenB' = State [Source] (Buses Bool)
forall a. State [Source] (Buses a)
unflattenPrimB

instance GenBuses Int  where
  genBuses' :: forall u v. Template u v -> [Source] -> BusesM (Buses Int)
genBuses' = Template u v -> [Source] -> BusesM (Buses Int)
forall a u v.
GenBuses a =>
Template u v -> [Source] -> BusesM (Buses a)
genPrimBus
  -- delay = primDelay
  ty :: Ty
ty = Ty
Int
  unflattenB' :: State [Source] (Buses Int)
unflattenB' = State [Source] (Buses Int)
forall a. State [Source] (Buses a)
unflattenPrimB

instance GenBuses Integer  where
  genBuses' :: forall u v. Template u v -> [Source] -> BusesM (Buses Integer)
genBuses' = Template u v -> [Source] -> BusesM (Buses Integer)
forall a u v.
GenBuses a =>
Template u v -> [Source] -> BusesM (Buses a)
genPrimBus
  -- delay = primDelay
  ty :: Ty
ty = Ty
Integer
  unflattenB' :: State [Source] (Buses Integer)
unflattenB' = State [Source] (Buses Integer)
forall a. State [Source] (Buses a)
unflattenPrimB

instance GenBuses Float  where
  genBuses' :: forall u v. Template u v -> [Source] -> BusesM (Buses Float)
genBuses' = Template u v -> [Source] -> BusesM (Buses Float)
forall a u v.
GenBuses a =>
Template u v -> [Source] -> BusesM (Buses a)
genPrimBus
  -- delay = primDelay
  ty :: Ty
ty = Ty
Float
  unflattenB' :: State [Source] (Buses Float)
unflattenB' = State [Source] (Buses Float)
forall a. State [Source] (Buses a)
unflattenPrimB

instance GenBuses Double  where
  genBuses' :: forall u v. Template u v -> [Source] -> BusesM (Buses Double)
genBuses' = Template u v -> [Source] -> BusesM (Buses Double)
forall a u v.
GenBuses a =>
Template u v -> [Source] -> BusesM (Buses a)
genPrimBus
  -- delay = primDelay
  ty :: Ty
ty = Ty
Double
  unflattenB' :: State [Source] (Buses Double)
unflattenB' = State [Source] (Buses Double)
forall a. State [Source] (Buses a)
unflattenPrimB

instance KnownNat n => GenBuses (Finite n) where
  genBuses' :: forall u v. Template u v -> [Source] -> BusesM (Buses (Finite n))
genBuses' = Template u v -> [Source] -> BusesM (Buses (Finite n))
forall a u v.
GenBuses a =>
Template u v -> [Source] -> BusesM (Buses a)
genPrimBus
  -- delay = primDelay
  ty :: Ty
ty = Integer -> Ty
Finite (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n))
  unflattenB' :: State [Source] (Buses (Finite n))
unflattenB' = State [Source] (Buses (Finite n))
forall a. State [Source] (Buses a)
unflattenPrimB

instance (KnownNat n, GenBuses b) => GenBuses (Vector n b)  where
  genBuses' :: forall u v. Template u v -> [Source] -> BusesM (Buses (Vector n b))
genBuses' = Template u v -> [Source] -> BusesM (Buses (Vector n b))
forall a u v.
GenBuses a =>
Template u v -> [Source] -> BusesM (Buses a)
genPrimBus
  -- delay = primDelay
  ty :: Ty
ty = Integer -> Ty -> Ty
Vector (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)) (forall a. GenBuses a => Ty
ty @b)
  unflattenB' :: State [Source] (Buses (Vector n b))
unflattenB' = State [Source] (Buses (Vector n b))
forall a. State [Source] (Buses a)
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' :: forall u v. Template u v -> [Source] -> BusesM (Buses (a :+ b))
genBuses' = Template u v -> [Source] -> BusesM (Buses (a :+ b))
forall a u v.
GenBuses a =>
Template u v -> [Source] -> BusesM (Buses a)
genPrimBus
  -- delay = primDelay
  ty :: Ty
ty = Ty -> Ty -> Ty
Sum (forall a. GenBuses a => Ty
ty @a) (forall a. GenBuses a => Ty
ty @b)
  unflattenB' :: State [Source] (Buses (a :+ b))
unflattenB' = State [Source] (Buses (a :+ b))
forall a. State [Source] (Buses a)
unflattenPrimB

instance (GenBuses a, GenBuses b) => GenBuses (a :* b) where
  genBuses' :: forall u v. Template u v -> [Source] -> BusesM (Buses (a :* b))
genBuses' Template u v
templ [Source]
ins =
    -- trace ("genBuses' @ " ++ show (ty (undefined :: a :* b))) $
    Buses a -> Buses b -> Buses (a :* b)
forall h a. Ok2 (:>) h a => Buses h -> Buses a -> Buses (h :* a)
ProdB (Buses a -> Buses b -> Buses (a :* b))
-> StateT Int (StateT (Int, CompInfo) Identity) (Buses a)
-> StateT
     Int (StateT (Int, CompInfo) Identity) (Buses b -> Buses (a :* b))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Template u v
-> [Source]
-> StateT Int (StateT (Int, CompInfo) Identity) (Buses a)
forall a u v.
GenBuses a =>
Template u v -> [Source] -> BusesM (Buses a)
forall u v.
Template u v
-> [Source]
-> StateT Int (StateT (Int, CompInfo) Identity) (Buses a)
genBuses' Template u v
templ [Source]
ins StateT
  Int (StateT (Int, CompInfo) Identity) (Buses b -> Buses (a :* b))
-> StateT Int (StateT (Int, CompInfo) Identity) (Buses b)
-> BusesM (Buses (a :* b))
forall a b.
StateT Int (StateT (Int, CompInfo) Identity) (a -> b)
-> StateT Int (StateT (Int, CompInfo) Identity) a
-> StateT Int (StateT (Int, CompInfo) Identity) b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Template u v
-> [Source]
-> StateT Int (StateT (Int, CompInfo) Identity) (Buses b)
forall a u v.
GenBuses a =>
Template u v -> [Source] -> BusesM (Buses a)
forall u v.
Template u v
-> [Source]
-> StateT Int (StateT (Int, CompInfo) Identity) (Buses b)
genBuses' Template u v
templ [Source]
ins
  -- delay (a,b) = delay a *** delay b
  ty :: Ty
ty = Ty -> Ty -> Ty
Prod (forall a. GenBuses a => Ty
ty @a) (forall a. GenBuses a => Ty
ty @b)
  unflattenB' :: State [Source] (Buses (a :* b))
unflattenB' = (Buses a -> Buses b -> Buses (a :* b))
-> StateT [Source] Identity (Buses a)
-> StateT [Source] Identity (Buses b)
-> State [Source] (Buses (a :* b))
forall a b c.
(a -> b -> c)
-> StateT [Source] Identity a
-> StateT [Source] Identity b
-> StateT [Source] Identity c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Buses a -> Buses b -> Buses (a :* b)
forall h a. Ok2 (:>) h a => Buses h -> Buses a -> Buses (h :* a)
ProdB StateT [Source] Identity (Buses a)
forall a. GenBuses a => State [Source] (Buses a)
unflattenB' StateT [Source] Identity (Buses b)
forall a. GenBuses a => State [Source] (Buses a)
unflattenB'

instance (GenBuses a, GenBuses b) => GenBuses (a -> b) where
  genBuses' :: forall u v. Template u v -> [Source] -> BusesM (Buses (a -> b))
genBuses' = Template u v -> [Source] -> BusesM (Buses (a -> b))
forall a u v.
GenBuses a =>
Template u v -> [Source] -> BusesM (Buses a)
genPrimBus
  -- delay = error "delay for functions: not yet implemented"
  ty :: Ty
ty = forall a. GenBuses a => Ty
ty @a Ty -> Ty -> Ty
`Fun` forall a. GenBuses a => Ty
ty @b
  unflattenB' :: State [Source] (Buses (a -> b))
unflattenB' = State [Source] (Buses (a -> b))
forall a. State [Source] (Buses a)
unflattenPrimB

flattenB :: Buses a -> [Source]
flattenB :: forall a. Buses a -> [Source]
flattenB = Seq Source -> [Source]
forall a. Seq a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList (Seq Source -> [Source])
-> (Buses a -> Seq Source) -> Buses a -> [Source]
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Buses a -> Seq Source
forall c. Buses c -> Seq Source
flat
 where
   flat :: Buses c -> Seq Source
   flat :: forall c. Buses c -> Seq Source
flat Buses c
UnitB        = Seq Source
forall a. Monoid a => a
mempty
   flat (PrimB Source
s)    = Source -> Seq Source
forall a. a -> Seq a
singleton Source
s
   flat (ProdB Buses a
a Buses b
b)  = Buses a -> Seq Source
forall c. Buses c -> Seq Source
flat Buses a
a Seq Source -> Seq Source -> Seq Source
forall a. Semigroup a => a -> a -> a
<> Buses b -> Seq Source
forall c. Buses c -> Seq Source
flat Buses b
b
   flat (IxProdB h (Buses a)
as) = (Buses a -> Seq Source) -> h (Buses a) -> Seq Source
forall m a. Monoid m => (a -> m) -> h a -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Buses a -> Seq Source
forall c. Buses c -> Seq Source
flat h (Buses a)
as
   flat (ConvertB Buses a
b) = Buses a -> Seq Source
forall c. Buses c -> Seq Source
flat Buses a
b

badBuses :: forall a x. Ok (:>) a => String -> Buses a -> x
badBuses :: forall a x. Ok (:>) a => String -> Buses a -> x
badBuses String
nm Buses a
bs = String -> x
forall a. HasCallStack => String -> a
error (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" got unexpected bus " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Buses a -> String
forall a. Show a => a -> String
show Buses a
bs)

unProdB :: Ok2 (:>) a b => Buses (a :* b) -> Buses a :* Buses b
unProdB :: forall a b. Ok2 (:>) a b => Buses (a :* b) -> Buses a :* Buses b
unProdB (ProdB Buses a
a Buses b
b)            = (Buses a
Buses a
a,Buses b
Buses b
b)
unProdB (ConvertB (ProdB Buses a
c Buses b
d)) = (Buses a -> Buses a
forall a b. Ok2 (:>) a b => Buses a -> Buses b
convertB Buses a
c, Buses b -> Buses b
forall a b. Ok2 (:>) a b => Buses a -> Buses b
convertB Buses b
d)
unProdB Buses (a :* b)
b                      = String -> Buses (a :* b) -> Buses a :* Buses b
forall a x. Ok (:>) a => String -> Buses a -> x
badBuses String
"unProdB" Buses (a :* b)
b

exlB :: Ok2 (:>) a b => Buses (a :* b) -> Buses a
exlB :: forall a b. Ok2 (:>) a b => Buses (a :* b) -> Buses a
exlB = (Buses a, Buses b) -> Buses a
forall a b. (a, b) -> a
fst ((Buses a, Buses b) -> Buses a)
-> (Buses (a :* b) -> (Buses a, Buses b))
-> Buses (a :* b)
-> Buses a
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Buses (a :* b) -> (Buses a, Buses b)
forall a b. Ok2 (:>) a b => Buses (a :* b) -> Buses a :* Buses b
unProdB

exrB :: Ok2 (:>) a b => Buses (a :* b) -> Buses b
exrB :: forall a b. Ok2 (:>) a b => Buses (a :* b) -> Buses b
exrB = (Buses a, Buses b) -> Buses b
forall a b. (a, b) -> b
snd ((Buses a, Buses b) -> Buses b)
-> (Buses (a :* b) -> (Buses a, Buses b))
-> Buses (a :* b)
-> Buses b
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Buses (a :* b) -> (Buses a, Buses b)
forall a b. Ok2 (:>) a b => Buses (a :* b) -> Buses a :* Buses b
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 :: forall a. OkCAR a => Buses (Rep a) -> Buses a
abstB = Buses (Rep a) -> Buses a
forall a b. Ok2 (:>) a b => Buses a -> Buses b
convertB

reprB :: OkCAR a => Buses a -> Buses (Rep a)
reprB :: forall a. OkCAR a => Buses a -> Buses (Rep a)
reprB = Buses a -> Buses (Rep a)
forall a b. Ok2 (:>) a b => Buses a -> Buses b
convertB

convertC :: forall a b. Ok2 (:>) a b => a :> b
convertC :: forall a b. Ok2 (:>) a b => a :> b
convertC = (a :+> b) -> a :> b
forall a b. (a :+> b) -> a :> b
C ((Buses a -> Buses b) -> a :+> b
forall b c.
(b -> c) -> Kleisli (StateT (Int, CompInfo) Identity) b c
forall (a :: Type -> Type -> Type) b c.
Arrow a =>
(b -> c) -> a b c
arr Buses a -> Buses b
forall a b. Ok2 (:>) a b => Buses a -> Buses b
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 :: forall a b. Ok2 (:>) a b => Buses a -> Buses b
convertB (ConvertB Buses a
p) = Buses a -> Buses b
forall a b. Ok2 (:>) a b => Buses a -> Buses b
mkConvertB Buses a
p  -- coalesce
convertB Buses a
a            = Buses a -> Buses b
forall a b. Ok2 (:>) a b => Buses a -> Buses b
mkConvertB Buses a
a

-- Make a ConvertB if source and target types differ; otherwise id
mkConvertB :: forall a b. Ok2 (:>) a b => Buses a -> Buses b
mkConvertB :: forall a b. Ok2 (:>) a b => Buses a -> Buses b
mkConvertB Buses a
a -- \| Just Refl <- eqT @a @b = a
             | Bool
otherwise              = Buses a -> Buses b
forall a b. Ok2 (:>) a b => Buses a -> Buses b
ConvertB Buses a
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 :: Template a b -> String
show (Prim String
p) = String
p
  show (Subgraph Graph
comps BCirc a b
_) = String
"Template:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Graph -> String
forall a. Show a => a -> String
show Graph
comps

-- Transform a subgraph if any. Must preserve meaning, since we leave the
-- generator unchanged.
onCompSubgraph :: Unop Graph -> Unop Comp
onCompSubgraph :: Unop Graph -> Unop Comp
onCompSubgraph Unop Graph
h (Comp Int
nc (Subgraph Graph
g BCirc a b
circ) Buses a
a Buses b
b) =
  Int -> Template () (a -> b) -> Buses () -> Buses (a -> b) -> Comp
forall a b.
Ok (:>) b =>
Int -> Template a b -> Buses a -> Buses b -> Comp
Comp Int
nc (Graph -> BCirc a b -> Template () (a -> b)
forall h a. Graph -> BCirc h a -> Template () (h -> a)
Subgraph (Unop Graph
h Graph
g) BCirc a b
circ) Buses a
Buses ()
a Buses b
Buses (a -> b)
b
onCompSubgraph Unop Graph
_ Comp
c = Comp
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 -> Int
compId (Comp Int
n Template a b
_ Buses a
_ Buses b
_) = Int
n

instance Eq  Comp where == :: Comp -> Comp -> Bool
(==) = Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Int -> Int -> Bool) -> (Comp -> Int) -> Comp -> Comp -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Comp -> Int
compId
instance Ord Comp where compare :: Comp -> Comp -> Ordering
compare = Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> (Comp -> Int) -> Comp -> Comp -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Comp -> Int
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 :: StateT (Int, CompInfo) Identity Int
genId = do Int
n <- ((Int, CompInfo) -> Int) -> StateT (Int, CompInfo) Identity Int
forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
M.gets (Int, CompInfo) -> Int
forall a b. (a, b) -> a
fst
           ((Int, CompInfo) -> (Int, CompInfo))
-> StateT (Int, CompInfo) Identity ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
M.modify ((Int -> Int) -> (Int, CompInfo) -> (Int, CompInfo)
forall (k :: Type -> Type -> Type) a c b.
(MonoidalPCat k, Ok3 k a b c) =>
k a c -> k (Prod k a b) (Prod k c b)
first Int -> Int
forall a. Enum a => a -> a
succ)
           Int -> StateT (Int, CompInfo) Identity Int
forall a. a -> StateT (Int, CompInfo) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Int
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 :: forall a b. Ok (:>) b => Template a b -> BCirc a b
genComp Template a b
templ Buses a
a =
  -- trace ("genComp " ++ name ++ ". b == " ++ show (ty @b)) $
  do Maybe Comp
mb <- ((Int, CompInfo) -> Maybe Comp)
-> StateT (Int, CompInfo) Identity (Maybe Comp)
forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
M.gets ((String, [Source], Ty) -> CompInfo -> Maybe Comp
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (String, [Source], Ty)
key (CompInfo -> Maybe Comp)
-> ((Int, CompInfo) -> CompInfo) -> (Int, CompInfo) -> Maybe Comp
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (Int, CompInfo) -> CompInfo
forall a b. (a, b) -> b
snd)
     case Maybe Comp
mb of
       Just (Comp Int
_ Template a b
_ Buses a
_ Buses b
b') ->
         -- trace ("genComp " ++ name ++ ": hit --> " ++ show b') $
         Buses b -> CircuitM (Buses b)
forall a. a -> StateT (Int, CompInfo) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Buses b -> Buses b
forall a b. a -> b
unsafeCoerce Buses b
b')
       Maybe Comp
Nothing               ->
         -- trace ("genComp " ++ name ++ ": ins == " ++ show ins) $
         do Buses b
b <- Template a b -> [Source] -> CircuitM (Buses b)
forall b a.
GenBuses b =>
Template a b -> [Source] -> CircuitM (Buses b)
genBuses Template a b
templ [Source]
ins
            -- trace ("genComp: genBuses --> " ++ show b) (return ())
            Int
c <- StateT (Int, CompInfo) Identity Int
genId
            let comp :: Comp
comp = Int -> Template a b -> Buses a -> Buses b -> Comp
forall a b.
Ok (:>) b =>
Int -> Template a b -> Buses a -> Buses b -> Comp
Comp Int
c Template a b
templ Buses a
a Buses b
b
            ((Int, CompInfo) -> (Int, CompInfo))
-> StateT (Int, CompInfo) Identity ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
M.modify ((CompInfo -> CompInfo) -> (Int, CompInfo) -> (Int, CompInfo)
forall (k :: Type -> Type -> Type) a b d.
(MonoidalPCat k, Ok3 k a b d) =>
k b d -> k (Prod k a b) (Prod k a d)
second ((String, [Source], Ty) -> Comp -> CompInfo -> CompInfo
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (String, [Source], Ty)
key Comp
comp))
            -- trace ("genComp " ++ name ++ ": miss --> " ++ show b) $
            Buses b -> CircuitM (Buses b)
forall a. a -> StateT (Int, CompInfo) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Buses b
b
 where
   ins :: [Source]
ins  = Buses a -> [Source]
forall a. Buses a -> [Source]
flattenB Buses a
a
   name :: String
name = Template a b -> String
forall a. Show a => a -> String
show Template a b
templ
   key :: (String, [Source], Ty)
key  = (String
name,[Source]
ins,forall a. GenBuses a => Ty
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' :: forall b. GenBuses b => String -> CircuitM (Buses b)
constComp' String
str = -- trace ("constComp' " ++ str) $
                 Template () b -> BCirc () b
forall a b. Ok (:>) b => Template a b -> BCirc a b
genComp (String -> Template () b
forall a b. String -> Template a b
Prim ({- "const " ++ -} String
str)) Buses ()
UnitB

constComp :: GenBuses b => PrimName -> BCirc a b
constComp :: forall b a. GenBuses b => String -> BCirc a b
constComp String
str = CircuitM (Buses b) -> Buses a -> CircuitM (Buses b)
forall (k :: Type -> Type -> Type) b a.
(ConstCat k b, Ok k a) =>
b -> k a b
const (String -> CircuitM (Buses b)
forall b. GenBuses b => String -> CircuitM (Buses b)
constComp' String
str)

-- TODO: maybe have constComp and constComp' take a template, and use for curry as well.

constM :: GS b => b -> BCirc a b
constM :: forall b a. GS b => b -> BCirc a b
constM b
b = String -> BCirc a b
forall b a. GenBuses b => String -> BCirc a b
constComp (b -> String
forall a. Show a => a -> String
constName b
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 :: forall a. Show a => a -> String
constName = b -> String
forall a. Show a => a -> String
show
#endif


{--------------------------------------------------------------------
    Circuit category
--------------------------------------------------------------------}

infixl 1 :>, :+>

-- | Internal representation for '(:>)'.
type a :+> b = Kleisli CircuitM (Buses a) (Buses b)

-- | Circuit category
newtype a :> b = C { forall a b. (a :> b) -> a :+> b
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 :: a :> r
reprC = (a :+> r) -> a :> r
forall a b. (a :+> b) -> a :> b
C ((Buses a -> Buses r) -> a :+> r
forall b c.
(b -> c) -> Kleisli (StateT (Int, CompInfo) Identity) b c
forall (a :: Type -> Type -> Type) b c.
Arrow a =>
(b -> c) -> a b c
arr Buses a -> Buses r
Buses a -> Buses (Rep a)
forall a. OkCAR a => Buses a -> Buses (Rep a)
reprB)
  abstC :: r :> a
abstC = (r :+> a) -> r :> a
forall a b. (a :+> b) -> a :> b
C ((Buses r -> Buses a) -> r :+> a
forall b c.
(b -> c) -> Kleisli (StateT (Int, CompInfo) Identity) b c
forall (a :: Type -> Type -> Type) b c.
Arrow a =>
(b -> c) -> a b c
arr Buses r -> Buses a
Buses (Rep a) -> Buses a
forall a. OkCAR a => Buses (Rep a) -> Buses a
abstB)
#endif

instance Ok2 (:>) a b => CoerceCat (:>) a b where coerceC :: a :> b
coerceC = a :> b
forall a b. Ok2 (:>) a b => a :> b
convertC

-- instance CoerceCat (:>) where
--   coerceC = C (arr coerce)

-- pattern CK bc = C (Kleisli bc)

mkCK :: BCirc a b -> (a :> b)
mkCK :: forall a b. BCirc a b -> a :> b
mkCK = (a :+> b) -> a :> b
forall a b. (a :+> b) -> a :> b
C ((a :+> b) -> a :> b)
-> (BCirc a b -> a :+> b) -> BCirc a b -> a :> b
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. BCirc a b -> a :+> b
forall (m :: Type -> Type) a b. (a -> m b) -> Kleisli m a b
Kleisli

unmkCK :: (a :> b) -> BCirc a b
unmkCK :: forall a b. (a :> b) -> BCirc a b
unmkCK = Kleisli (StateT (Int, CompInfo) Identity) (Buses a) (Buses b)
-> BCirc a b
forall (m :: Type -> Type) a b. Kleisli m a b -> a -> m b
runKleisli (Kleisli (StateT (Int, CompInfo) Identity) (Buses a) (Buses b)
 -> BCirc a b)
-> ((a :> b)
    -> Kleisli (StateT (Int, CompInfo) Identity) (Buses a) (Buses b))
-> (a :> b)
-> BCirc a b
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (a :> b)
-> Kleisli (StateT (Int, CompInfo) Identity) (Buses a) (Buses b)
forall a b. (a :> b) -> a :+> b
unC

-- TODO: Eliminate mkCK in favor of CK

inCK :: (BCirc a a' -> BCirc b b')
     -> ((a :> a') -> (b :> b'))
inCK :: forall a a' b b'.
(BCirc a a' -> BCirc b b') -> (a :> a') -> b :> b'
inCK = BCirc b b' -> b :> b'
forall a b. BCirc a b -> a :> b
mkCK (BCirc b b' -> b :> b')
-> ((a :> a') -> BCirc a a')
-> (BCirc a a' -> BCirc b b')
-> (a :> a')
-> b :> b'
forall (k :: Type -> Type -> Type) a b a' b'.
(Category k, Oks k '[a, b, a', b']) =>
k b b' -> k a' a -> k a b -> k a' b'
<~ (a :> a') -> BCirc a a'
forall a b. (a :> b) -> BCirc a b
unmkCK

inCK2 :: (BCirc a a' -> BCirc b b' -> BCirc c c')
      -> ((a :> a') -> (b :> b') -> (c :> c'))
inCK2 :: forall a a' b b' c c'.
(BCirc a a' -> BCirc b b' -> BCirc c c')
-> (a :> a') -> (b :> b') -> c :> c'
inCK2 = (BCirc b b' -> BCirc c c') -> (b :> b') -> c :> c'
forall a a' b b'.
(BCirc a a' -> BCirc b b') -> (a :> a') -> b :> b'
inCK ((BCirc b b' -> BCirc c c') -> (b :> b') -> c :> c')
-> ((a :> a') -> BCirc a a')
-> (BCirc a a' -> BCirc b b' -> BCirc c c')
-> (a :> a')
-> (b :> b')
-> c :> c'
forall (k :: Type -> Type -> Type) a b a' b'.
(Category k, Oks k '[a, b, a', b']) =>
k b b' -> k a' a -> k a b -> k a' b'
<~ (a :> a') -> BCirc a a'
forall a b. (a :> b) -> BCirc a b
unmkCK

inCKF1 :: Functor h => (h (BCirc a a') -> BCirc b b') -> (h (a :> a') -> (b :> b'))
inCKF1 :: forall (h :: Type -> Type) a a' b b'.
Functor h =>
(h (BCirc a a') -> BCirc b b') -> h (a :> a') -> b :> b'
inCKF1 = BCirc b b' -> b :> b'
forall a b. BCirc a b -> a :> b
mkCK (BCirc b b' -> b :> b')
-> (h (a :> a') -> h (BCirc a a'))
-> (h (BCirc a a') -> BCirc b b')
-> h (a :> a')
-> b :> b'
forall (k :: Type -> Type -> Type) a b a' b'.
(Category k, Oks k '[a, b, a', b']) =>
k b b' -> k a' a -> k a b -> k a' b'
<~ ((a :> a') -> BCirc a a') -> h (a :> a') -> h (BCirc a a')
forall a b. (a -> b) -> h a -> h b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (a :> a') -> BCirc a a'
forall a b. (a :> b) -> BCirc a b
unmkCK

namedC :: Ok (:>) b => PrimName -> a :> b
-- namedC name = primOpt name noOpt
namedC :: forall b a. Ok (:>) b => String -> a :> b
namedC String
name = -- trace ("namedC " ++ name) $
              BCirc a b -> a :> b
forall a b. BCirc a b -> a :> b
mkCK (Template a b -> BCirc a b
forall a b. Ok (:>) b => Template a b -> BCirc a b
genComp (String -> Template a b
forall a b. String -> Template a b
Prim String
name))

type Opt b = [Source] -> CircuitM (Maybe (Buses b))

justA :: Applicative f => a -> f (Maybe a)
justA :: forall (f :: Type -> Type) a. Applicative f => a -> f (Maybe a)
justA = Maybe a -> f (Maybe a)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Maybe a -> f (Maybe a)) -> (a -> Maybe a) -> a -> f (Maybe a)
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. a -> Maybe a
forall a. a -> Maybe a
Just

nothingA :: Applicative f => f (Maybe a)
nothingA :: forall (f :: Type -> Type) a. Applicative f => f (Maybe a)
nothingA = Maybe a -> f (Maybe a)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Maybe a
forall a. Maybe a
Nothing

newComp :: (a :> b) -> Buses a -> CircuitM (Maybe (Buses b))
newComp :: forall a b. (a :> b) -> Buses a -> CircuitM (Maybe (Buses b))
newComp a :> b
cir = (Buses b -> Maybe (Buses b))
-> StateT (Int, CompInfo) Identity (Buses b)
-> CircuitM (Maybe (Buses b))
forall a b.
(a -> b)
-> StateT (Int, CompInfo) Identity a
-> StateT (Int, CompInfo) Identity b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Buses b -> Maybe (Buses b)
forall a. a -> Maybe a
Just (StateT (Int, CompInfo) Identity (Buses b)
 -> CircuitM (Maybe (Buses b)))
-> (Buses a -> StateT (Int, CompInfo) Identity (Buses b))
-> Buses a
-> CircuitM (Maybe (Buses b))
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (a :> b) -> Buses a -> StateT (Int, CompInfo) Identity (Buses b)
forall a b. (a :> b) -> BCirc a b
unmkCK a :> b
cir

newComp1 :: SourceToBuses a => (a :> b) -> Source -> CircuitM (Maybe (Buses b))
newComp1 :: forall a b.
SourceToBuses a =>
(a :> b) -> Source -> CircuitM (Maybe (Buses b))
newComp1 a :> b
cir Source
a = (a :> b) -> Buses a -> CircuitM (Maybe (Buses b))
forall a b. (a :> b) -> Buses a -> CircuitM (Maybe (Buses b))
newComp a :> b
cir (Source -> Buses a
forall a. SourceToBuses a => Source -> Buses a
toBuses Source
a)

newComp2 :: (SourceToBuses a, SourceToBuses b) =>
            (a :* b :> c) -> Source -> Source -> CircuitM (Maybe (Buses c))
newComp2 :: forall a b c.
(SourceToBuses a, SourceToBuses b) =>
((a :* b) :> c) -> Source -> Source -> CircuitM (Maybe (Buses c))
newComp2 (a :* b) :> c
cir Source
a Source
b = ((a :* b) :> c) -> Buses (a :* b) -> CircuitM (Maybe (Buses c))
forall a b. (a :> b) -> Buses a -> CircuitM (Maybe (Buses b))
newComp (a :* b) :> c
cir (Buses a -> Buses b -> Buses (a :* b)
forall h a. Ok2 (:>) h a => Buses h -> Buses a -> Buses (h :* a)
ProdB (Source -> Buses a
forall a. SourceToBuses a => Source -> Buses a
toBuses Source
a) (Source -> Buses b
forall a. SourceToBuses a => Source -> Buses a
toBuses Source
b))

newComp3L :: (SourceToBuses a, SourceToBuses b, SourceToBuses c) =>
             ((a :* b) :* c :> d) -> Source -> Source -> Source -> CircuitM (Maybe (Buses d))
newComp3L :: forall a b c d.
(SourceToBuses a, SourceToBuses b, SourceToBuses c) =>
(((a :* b) :* c) :> d)
-> Source -> Source -> Source -> CircuitM (Maybe (Buses d))
newComp3L ((a :* b) :* c) :> d
cir Source
a Source
b Source
c = (((a :* b) :* c) :> d)
-> Buses ((a :* b) :* c) -> CircuitM (Maybe (Buses d))
forall a b. (a :> b) -> Buses a -> CircuitM (Maybe (Buses b))
newComp ((a :* b) :* c) :> d
cir (Buses (a :* b) -> Buses c -> Buses ((a :* b) :* c)
forall h a. Ok2 (:>) h a => Buses h -> Buses a -> Buses (h :* a)
ProdB (Buses a -> Buses b -> Buses (a :* b)
forall h a. Ok2 (:>) h a => Buses h -> Buses a -> Buses (h :* a)
ProdB (Source -> Buses a
forall a. SourceToBuses a => Source -> Buses a
toBuses Source
a) (Source -> Buses b
forall a. SourceToBuses a => Source -> Buses a
toBuses Source
b)) (Source -> Buses c
forall a. SourceToBuses a => Source -> Buses a
toBuses Source
c))

newComp3R :: (SourceToBuses a, SourceToBuses b, SourceToBuses c) =>
             (a :* (b :* c) :> d) -> Source -> Source -> Source -> CircuitM (Maybe (Buses d))
newComp3R :: forall a b c d.
(SourceToBuses a, SourceToBuses b, SourceToBuses c) =>
((a :* (b :* c)) :> d)
-> Source -> Source -> Source -> CircuitM (Maybe (Buses d))
newComp3R (a :* (b :* c)) :> d
cir Source
a Source
b Source
c = ((a :* (b :* c)) :> d)
-> Buses (a :* (b :* c)) -> CircuitM (Maybe (Buses d))
forall a b. (a :> b) -> Buses a -> CircuitM (Maybe (Buses b))
newComp (a :* (b :* c)) :> d
cir (Buses a -> Buses (b :* c) -> Buses (a :* (b :* c))
forall h a. Ok2 (:>) h a => Buses h -> Buses a -> Buses (h :* a)
ProdB (Source -> Buses a
forall a. SourceToBuses a => Source -> Buses a
toBuses Source
a) (Buses b -> Buses c -> Buses (b :* c)
forall h a. Ok2 (:>) h a => Buses h -> Buses a -> Buses (h :* a)
ProdB (Source -> Buses b
forall a. SourceToBuses a => Source -> Buses a
toBuses Source
b) (Source -> Buses c
forall a. SourceToBuses a => Source -> Buses a
toBuses Source
c)))

newVal :: GS b => b -> CircuitM (Maybe (Buses b))
newVal :: forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal b
b = Buses b -> Maybe (Buses b)
forall a. a -> Maybe a
Just (Buses b -> Maybe (Buses b))
-> StateT (Int, CompInfo) Identity (Buses b)
-> StateT (Int, CompInfo) Identity (Maybe (Buses b))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> StateT (Int, CompInfo) Identity (Buses b)
forall b. GS b => b -> CircuitM (Buses b)
constM' b
b

constM' :: GS b => b -> CircuitM (Buses b)
constM' :: forall b. GS b => b -> CircuitM (Buses b)
constM' b
b = String -> CircuitM (Buses b)
forall b. GenBuses b => String -> CircuitM (Buses b)
constComp' (b -> String
forall a. Show a => a -> String
constName b
b)

-- noOpt :: Opt b
-- noOpt = const nothingA

orOpt :: Binop (Opt b)
orOpt :: forall b. Binop (Opt b)
orOpt Opt b
f Opt b
g [Source]
a = do Maybe (Buses b)
mb <- Opt b
f [Source]
a
                 case Maybe (Buses b)
mb of
                   Maybe (Buses b)
Nothing -> Opt b
g [Source]
a
                   Just Buses b
_  -> Maybe (Buses b) -> CircuitM (Maybe (Buses b))
forall a. a -> StateT (Int, CompInfo) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe (Buses b)
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 :: forall b a. Ok (:>) b => String -> Opt b -> a :> b
primOpt String
name Opt b
opt =
  BCirc a b -> a :> b
forall a b. BCirc a b -> a :> b
mkCK (BCirc a b -> a :> b) -> BCirc a b -> a :> b
forall a b. (a -> b) -> a -> b
$ \ Buses a
a -> let plain :: CircuitM (Buses b)
plain = Template a b -> BCirc a b
forall a b. Ok (:>) b => Template a b -> BCirc a b
genComp (String -> Template a b
forall a b. String -> Template a b
Prim String
name) Buses a
a in
                  Opt b
opt (Buses a -> [Source]
forall a. Buses a -> [Source]
flattenB Buses a
a) StateT (Int, CompInfo) Identity (Maybe (Buses b))
-> (Maybe (Buses b) -> CircuitM (Buses b)) -> CircuitM (Buses b)
forall a b.
StateT (Int, CompInfo) Identity a
-> (a -> StateT (Int, CompInfo) Identity b)
-> StateT (Int, CompInfo) Identity b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= CircuitM (Buses b)
-> (Buses b -> CircuitM (Buses b))
-> Maybe (Buses b)
-> CircuitM (Buses b)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe CircuitM (Buses b)
plain Buses b -> CircuitM (Buses b)
forall a. a -> StateT (Int, CompInfo) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return

tryCommute :: a :> a
tryCommute :: forall a. a :> a
tryCommute = BCirc a a -> a :> a
forall a b. BCirc a b -> a :> b
mkCK BCirc a a
forall {m :: Type -> Type} {a}. Monad m => Buses a -> m (Buses a)
try
 where
#if !defined NoCommute
   -- TODO: Add an Ord constraint to PrimB for this line
   try :: Buses a -> m (Buses a)
try (ProdB (PrimB Source
a) (PrimB Source
a')) | Source
a Source -> Source -> Bool
forall a. Ord a => a -> a -> Bool
> Source
a' = Buses (a, b) -> m (Buses (a, b))
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Buses a -> Buses b -> Buses (a, b)
forall h a. Ok2 (:>) h a => Buses h -> Buses a -> Buses (h :* a)
ProdB (Source -> Buses a
forall b. Source -> Buses b
PrimB Source
a') (Source -> Buses b
forall b. Source -> Buses b
PrimB Source
a))
#endif
   try Buses a
b = Buses a -> m (Buses a)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Buses a
b

-- Like primOpt, but sorts. Use for commutative operations to improve reuse
-- (cache hits).
primOptSort :: forall a b. Ok2 (:>) a b => String -> Opt b -> a :> b
primOptSort String
name Opt b
opt = String -> Opt b -> a :> b
forall b a. Ok (:>) b => String -> Opt b -> a :> b
primOpt String
name Opt b
opt (a :> b) -> (a :> a) -> a :> b
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. a :> a
forall a. a :> a
tryCommute
#else
primOpt name _ = namedC name
primOptSort = primOpt
#endif

primNoOpt1 :: (Ok2 (:>) a b, Read a, Show b)
           => PrimName -> (a -> b) -> a :> b
primNoOpt1 :: forall a b.
(Ok2 (:>) a b, Read a, Show b) =>
String -> (a -> b) -> a :> b
primNoOpt1 String
name a -> b
fun =
  String -> Opt b -> a :> b
forall b a. Ok (:>) b => String -> Opt b -> a :> b
primOpt String
name (Opt b -> a :> b) -> Opt b -> a :> b
forall a b. (a -> b) -> a -> b
$
    \ case [Val a
x] -> b -> CircuitM (Maybe (Buses b))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal (a -> b
fun a
x)
           [Source]
_       -> CircuitM (Maybe (Buses b))
forall (f :: Type -> Type) a. Applicative f => f (Maybe a)
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 :: forall b a. GS b => b -> a :> b
constC = BCirc a b -> a :> b
forall a b. BCirc a b -> a :> b
mkCK (BCirc a b -> a :> b) -> (b -> BCirc a b) -> b -> a :> b
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. b -> BCirc a b
forall b a. GS b => b -> BCirc a b
constM

inC :: (a :+> b -> a' :+> b') -> (a :> b -> a' :> b')
inC :: forall a b a' b'. ((a :+> b) -> a' :+> b') -> (a :> b) -> a' :> b'
inC = (a' :+> b') -> a' :> b'
forall a b. (a :+> b) -> a :> b
C ((a' :+> b') -> a' :> b')
-> ((a :> b) -> a :+> b)
-> ((a :+> b) -> a' :+> b')
-> (a :> b)
-> a' :> b'
forall (k :: Type -> Type -> Type) a b a' b'.
(Category k, Oks k '[a, b, a', b']) =>
k b b' -> k a' a -> k a b -> k a' b'
<~ (a :> b) -> a :+> b
forall a b. (a :> b) -> a :+> b
unC

inC2 :: (a :+> b -> a' :+> b' -> a'' :+> b'')
     -> (a :>  b -> a' :>  b' -> a'' :>  b'')
inC2 :: forall a b a' b' a'' b''.
((a :+> b) -> (a' :+> b') -> a'' :+> b'')
-> (a :> b) -> (a' :> b') -> a'' :> b''
inC2 = ((a' :+> b') -> a'' :+> b'') -> (a' :> b') -> a'' :> b''
forall a b a' b'. ((a :+> b) -> a' :+> b') -> (a :> b) -> a' :> b'
inC (((a' :+> b') -> a'' :+> b'') -> (a' :> b') -> a'' :> b'')
-> ((a :> b) -> a :+> b)
-> ((a :+> b) -> (a' :+> b') -> a'' :+> b'')
-> (a :> b)
-> (a' :> b')
-> a'' :> b''
forall (k :: Type -> Type -> Type) a b a' b'.
(Category k, Oks k '[a, b, a', b']) =>
k b b' -> k a' a -> k a b -> k a' b'
<~ (a :> b) -> a :+> b
forall a b. (a :> b) -> a :+> b
unC

instance Category (:>) where
  type Ok (:>) = GenBuses
  id :: forall a. Ok (:>) a => a :> a
id  = (a :+> a) -> a :> a
forall a b. (a :+> b) -> a :> b
C a :+> a
forall (k :: Type -> Type -> Type) a. (Category k, Ok k a) => k a a
id
  . :: forall b c a. Ok3 (:>) a b c => (b :> c) -> (a :> b) -> a :> c
(.) = ((b :+> c) -> (a :+> b) -> a :+> c)
-> (b :> c) -> (a :> b) -> a :> c
forall a b a' b' a'' b''.
((a :+> b) -> (a' :+> b') -> a'' :+> b'')
-> (a :> b) -> (a' :> b') -> a'' :> b''
inC2 (b :+> c) -> (a :+> b) -> a :+> c
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
(.)

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 :: forall (m :: Type -> Type) a b c d.
(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 Buses a -> m (Buses c)
f Buses b -> m (Buses d)
g = (\ ~(Buses a
a,Buses b
b) -> (Buses c -> Buses d -> Buses (c :* d))
-> m (Buses c) -> m (Buses d) -> m (Buses (c :* d))
forall a b c. (a -> b -> c) -> m a -> m b -> m c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Buses c -> Buses d -> Buses (c :* d)
forall h a. Ok2 (:>) h a => Buses h -> Buses a -> Buses (h :* a)
ProdB (Buses a -> m (Buses c)
f Buses a
a) (Buses b -> m (Buses d)
g Buses b
b)) ((Buses a, Buses b) -> m (Buses (c :* d)))
-> (Buses (a :* b) -> (Buses a, Buses b))
-> Buses (a :* b)
-> m (Buses (c :* d))
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Buses (a :* b) -> (Buses a, Buses b)
forall a b. Ok2 (:>) a b => Buses (a :* b) -> Buses a :* Buses 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 :: forall (m :: Type -> Type) a c d.
(Applicative m, Ok3 (:>) a c d) =>
(Buses a -> m (Buses c))
-> (Buses a -> m (Buses d)) -> Buses a -> m (Buses (c :* d))
forkB Buses a -> m (Buses c)
f Buses a -> m (Buses d)
g Buses a
a = (Buses c -> Buses d -> Buses (c :* d))
-> m (Buses c) -> m (Buses d) -> m (Buses (c :* d))
forall a b c. (a -> b -> c) -> m a -> m b -> m c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Buses c -> Buses d -> Buses (c :* d)
forall h a. Ok2 (:>) h a => Buses h -> Buses a -> Buses (h :* a)
ProdB (Buses a -> m (Buses c)
f Buses a
a) (Buses a -> m (Buses d)
g Buses a
a)

-- or drop forkB in favor of dupB and crossB

dupB :: (Applicative m, Ok (:>) a) =>
        Buses a -> m (Buses (a :* a))
dupB :: forall (m :: Type -> Type) a.
(Applicative m, Ok (:>) a) =>
Buses a -> m (Buses (a :* a))
dupB Buses a
a = Buses (a :* a) -> m (Buses (a :* a))
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Buses a -> Buses a -> Buses (a :* a)
forall h a. Ok2 (:>) h a => Buses h -> Buses a -> Buses (h :* a)
ProdB Buses a
a Buses a
a)

instance OpCon (:*) (Sat GenBuses) where inOp :: forall a b.
(Sat GenBuses a && Sat GenBuses b) |- Sat GenBuses (a :* b)
inOp = (Con (Sat GenBuses a && Sat GenBuses b)
 :- Con (Sat GenBuses (a :* b)))
-> (Sat GenBuses a && Sat GenBuses b) |- Sat GenBuses (a :* b)
forall a b. (Con a :- Con b) -> a |- b
Entail (((GenBuses a, GenBuses b) => Dict (GenBuses (a :* b)))
-> (GenBuses a, GenBuses b) :- GenBuses (a :* b)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict (GenBuses (a :* b))
(GenBuses a, GenBuses b) => Dict (GenBuses (a :* b))
forall (a :: Constraint). a => Dict a
Dict)

instance MonoidalPCat (:>) where
  *** :: forall a b c d.
Ok4 (:>) a b c d =>
(a :> c) -> (b :> d) -> Prod (:>) a b :> Prod (:>) c d
(***) = (BCirc a c -> BCirc b d -> BCirc (Prod (:>) a b) (Prod (:>) c d))
-> (a :> c) -> (b :> d) -> Prod (:>) a b :> Prod (:>) c d
forall a a' b b' c c'.
(BCirc a a' -> BCirc b b' -> BCirc c c')
-> (a :> a') -> (b :> b') -> c :> c'
inCK2 BCirc a c -> BCirc b d -> BCirc (Prod (:>) a b) (Prod (:>) c d)
forall (m :: Type -> Type) a b c d.
(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  -- or default

instance AssociativePCat (:>)
instance BraidedPCat     (:>)

instance ProductCat (:>) where
  -- type Prod (:>) = (:*)
  exl :: forall a b. Ok2 (:>) a b => Prod (:>) a b :> a
exl = (Prod (:>) a b :+> a) -> Prod (:>) a b :> a
forall a b. (a :+> b) -> a :> b
C ((Buses (Prod (:>) a b) -> Buses a) -> Prod (:>) a b :+> a
forall b c.
(b -> c) -> Kleisli (StateT (Int, CompInfo) Identity) b c
forall (a :: Type -> Type -> Type) b c.
Arrow a =>
(b -> c) -> a b c
arr Buses (Prod (:>) a b) -> Buses a
forall a b. Ok2 (:>) a b => Buses (a :* b) -> Buses a
exlB)
  exr :: forall a b. Ok2 (:>) a b => Prod (:>) a b :> b
exr = (Prod (:>) a b :+> b) -> Prod (:>) a b :> b
forall a b. (a :+> b) -> a :> b
C ((Buses (Prod (:>) a b) -> Buses b) -> Prod (:>) a b :+> b
forall b c.
(b -> c) -> Kleisli (StateT (Int, CompInfo) Identity) b c
forall (a :: Type -> Type -> Type) b c.
Arrow a =>
(b -> c) -> a b c
arr Buses (Prod (:>) a b) -> Buses b
forall a b. Ok2 (:>) a b => Buses (a :* b) -> Buses b
exrB)
  dup :: forall a. Ok (:>) a => a :> Prod (:>) a a
dup = BCirc a (Prod (:>) a a) -> a :> Prod (:>) a a
forall a b. BCirc a b -> a :> b
mkCK BCirc a (Prod (:>) a a)
forall (m :: Type -> Type) a.
(Applicative m, Ok (:>) a) =>
Buses a -> m (Buses (a :* a))
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 :: forall a b. Ok2 (:>) a b => a :> CoprodP (:>) a b
inlP   = String -> a :> CoprodP (:>) a b
forall b a. Ok (:>) b => String -> a :> b
namedC String
"inlP"
  inrP :: forall a b. Ok2 (:>) a b => b :> CoprodP (:>) a b
inrP   = String -> b :> CoprodP (:>) a b
forall b a. Ok (:>) b => String -> a :> b
namedC String
"inrP"
  jamP :: forall a. Ok (:>) a => CoprodP (:>) a a :> a
jamP   = String -> CoprodP (:>) a a :> a
forall b a. Ok (:>) b => String -> a :> b
namedC String
"jamP"
  -- swapPS = swapP

{--------------------------------------------------------------------
    Misc
--------------------------------------------------------------------}

instance (Ok (:>) a, IfCat (:>) b) => IfCat (:>) (a -> b) where
  ifC :: IfT (:>) (a -> b)
ifC = IfT (:>) (a -> b)
forall (k :: Type -> Type -> Type) a b.
(MonoidalPCat k, ClosedCat k, Ok k a, IfCat k b) =>
IfT k (a -> b)
funIf

instance OpCon (->) (Sat GenBuses) where inOp :: forall a b.
(Sat GenBuses a && Sat GenBuses b) |- Sat GenBuses (a -> b)
inOp = (Con (Sat GenBuses a && Sat GenBuses b)
 :- Con (Sat GenBuses (a -> b)))
-> (Sat GenBuses a && Sat GenBuses b) |- Sat GenBuses (a -> b)
forall a b. (Con a :- Con b) -> a |- b
Entail (((GenBuses a, GenBuses b) => Dict (GenBuses (a -> b)))
-> (GenBuses a, GenBuses b) :- GenBuses (a -> b)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict (GenBuses (a -> b))
(GenBuses a, GenBuses b) => Dict (GenBuses (a -> b))
forall (a :: Constraint). a => Dict a
Dict)

genSubgraph :: Ok2 (:>) b c => BCirc b c -> CircuitM (Buses (b -> c))
genSubgraph :: forall b c. Ok2 (:>) b c => BCirc b c -> CircuitM (Buses (b -> c))
genSubgraph BCirc b c
bcirc =
  do Int
supply <- ((Int, CompInfo) -> Int) -> StateT (Int, CompInfo) Identity Int
forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
M.gets (Int, CompInfo) -> Int
forall a b. (a, b) -> a
fst
     let (Graph
g,Int
supply') = (b :> c) -> Int -> (Graph, Int)
forall a b. Ok2 (:>) a b => (a :> b) -> Int -> (Graph, Int)
mkGraph' (BCirc b c -> b :> c
forall a b. BCirc a b -> a :> b
mkCK BCirc b c
bcirc) Int
supply
     ((Int, CompInfo) -> (Int, CompInfo))
-> StateT (Int, CompInfo) Identity ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
M.modify ((Int -> Int) -> (Int, CompInfo) -> (Int, CompInfo)
forall (k :: Type -> Type -> Type) a c b.
(MonoidalPCat k, Ok3 k a b c) =>
k a c -> k (Prod k a b) (Prod k c b)
first (Int -> Int -> Int
forall (k :: Type -> Type -> Type) b a.
(ConstCat k b, Ok k a) =>
b -> k a b
const Int
supply'))
     Template () (b -> c) -> BCirc () (b -> c)
forall a b. Ok (:>) b => Template a b -> BCirc a b
genComp (Graph -> BCirc b c -> Template () (b -> c)
forall h a. Graph -> BCirc h a -> Template () (h -> a)
Subgraph Graph
g BCirc b c
bcirc) Buses ()
UnitB

curryB :: Ok3 (:>) a b c => BCirc (a :* b) c -> BCirc a (b -> c)
curryB :: forall a b c.
Ok3 (:>) a b c =>
BCirc (a :* b) c -> BCirc a (b -> c)
curryB BCirc (a :* b) c
f Buses a
a = BCirc b c -> CircuitM (Buses (b -> c))
forall b c. Ok2 (:>) b c => BCirc b c -> CircuitM (Buses (b -> c))
genSubgraph (\ Buses b
b -> BCirc (a :* b) c
f (Buses a -> Buses b -> Buses (a :* b)
forall h a. Ok2 (:>) h a => Buses h -> Buses a -> Buses (h :* a)
ProdB Buses a
a Buses b
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 :: forall a b. Ok2 (:>) a b => Prod (:>) (Exp (:>) a b) a :> b
apply = String -> Opt b -> ((a -> b) :* a) :> b
forall b a. Ok (:>) b => String -> Opt b -> a :> b
primOpt String
"apply" (Opt b -> ((a -> b) :* a) :> b) -> Opt b -> ((a -> b) :* a) :> b
forall a b. (a -> b) -> a -> b
$ \ case
            (Source Bus
_ (Subgraph Graph
_ BCirc a b
gen) [Source]
_ : [Source]
rest)
              -> Buses b -> Maybe (Buses b)
forall a. a -> Maybe a
Just (Buses b -> Maybe (Buses b))
-> StateT (Int, CompInfo) Identity (Buses b)
-> StateT (Int, CompInfo) Identity (Maybe (Buses b))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (BCirc a b -> BCirc a b
forall a b. a -> b
unsafeCoerce BCirc a b
gen :: BCirc a b) ([Source] -> Buses a
forall a. GenBuses a => [Source] -> Buses a
unflattenB [Source]
rest)
            [Source]
_ -> StateT (Int, CompInfo) Identity (Maybe (Buses b))
forall (f :: Type -> Type) a. Applicative f => f (Maybe a)
nothingA
  curry :: forall a b c.
Ok3 (:>) a b c =>
(Prod (:>) a b :> c) -> a :> Exp (:>) b c
curry = BCirc a (b -> c) -> a :> (b -> c)
forall a b. BCirc a b -> a :> b
mkCK (BCirc a (b -> c) -> a :> (b -> c))
-> (((a :* b) :> c) -> BCirc a (b -> c))
-> ((a :* b) :> c)
-> a :> (b -> c)
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. BCirc (a :* b) c -> BCirc a (b -> c)
forall a b c.
Ok3 (:>) a b c =>
BCirc (a :* b) c -> BCirc a (b -> c)
curryB (BCirc (a :* b) c -> BCirc a (b -> c))
-> (((a :* b) :> c) -> BCirc (a :* b) c)
-> ((a :* b) :> c)
-> BCirc a (b -> c)
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. ((a :* b) :> c) -> BCirc (a :* b) c
forall a b. (a :> b) -> BCirc a b
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 :: forall a. Ok' (:>) a |- Ok' (:>) (U1 a)
okIxProd = (Con (Sat GenBuses a) :- Con (Sat GenBuses (U1 a)))
-> Sat GenBuses a |- Sat GenBuses (U1 a)
forall a b. (Con a :- Con b) -> a |- b
Entail ((GenBuses a => Dict (GenBuses (U1 a)))
-> GenBuses a :- GenBuses (U1 a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict (GenBuses (U1 a))
GenBuses a => Dict (GenBuses (U1 a))
forall (a :: Constraint). a => Dict a
Dict)
instance OkIxProd (:>) G.Par1 where okIxProd :: forall a. Ok' (:>) a |- Ok' (:>) (Par1 a)
okIxProd = (Con (Sat GenBuses a) :- Con (Sat GenBuses (Par1 a)))
-> Sat GenBuses a |- Sat GenBuses (Par1 a)
forall a b. (Con a :- Con b) -> a |- b
Entail ((GenBuses a => Dict (GenBuses (Par1 a)))
-> GenBuses a :- GenBuses (Par1 a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict (GenBuses (Par1 a))
GenBuses a => Dict (GenBuses (Par1 a))
forall (a :: Constraint). a => Dict a
Dict)

instance (OkIxProd (:>) f, OkIxProd (:>) g)
      => OkIxProd (:>) (f G.:*: g) where
  okIxProd :: forall a. Ok' (:>) a |- Ok' (:>) ((f G.:*: g) a)
  okIxProd :: forall a. Ok' (:>) a |- Ok' (:>) ((:*:) f g a)
okIxProd = (Con (Sat GenBuses a) :- Con (Sat GenBuses ((:*:) f g a)))
-> Sat GenBuses a |- Sat GenBuses ((:*:) f g a)
forall a b. (Con a :- Con b) -> a |- b
Entail ((GenBuses a => Dict (GenBuses ((:*:) f g a)))
-> GenBuses a :- GenBuses ((:*:) f g a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (Dict (GenBuses ((:*:) f g a))
Con (Sat GenBuses (f a)) => Dict (GenBuses ((:*:) f g a))
forall (a :: Constraint). a => Dict a
Dict (Con (Sat GenBuses (f a)) => Dict (GenBuses ((:*:) f g a)))
-> (Sat GenBuses a |- Sat GenBuses (f a))
-> Dict (GenBuses ((:*:) f g a))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkIxProd k h =>
Ok' k a |- Ok' k (h a)
okIxProd @(:>) @f @a (Con (Sat GenBuses (g a)) => Dict (GenBuses ((:*:) f g a)))
-> (Sat GenBuses a |- Sat GenBuses (g a))
-> Dict (GenBuses ((:*:) f g a))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkIxProd k h =>
Ok' k a |- Ok' k (h 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 :: forall a. Ok' (:>) a |- Ok' (:>) ((:.:) g f a)
okIxProd = (Con (Sat GenBuses a) :- Con (Sat GenBuses ((:.:) g f a)))
-> Sat GenBuses a |- Sat GenBuses ((:.:) g f a)
forall a b. (Con a :- Con b) -> a |- b
Entail ((GenBuses a => Dict (GenBuses ((:.:) g f a)))
-> GenBuses a :- GenBuses ((:.:) g f a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (Dict (GenBuses ((:.:) g f a))
Con (Sat GenBuses (g (f a))) => Dict (GenBuses ((:.:) g f a))
forall (a :: Constraint). a => Dict a
Dict (Con (Sat GenBuses (g (f a))) => Dict (GenBuses ((:.:) g f a)))
-> (Sat GenBuses (f a) |- Sat GenBuses (g (f a)))
-> Dict (GenBuses ((:.:) g f a))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkIxProd k h =>
Ok' k a |- Ok' k (h a)
okIxProd @(:>) @g @(f a) (Con (Sat GenBuses (f a)) => Dict (GenBuses ((:.:) g f a)))
-> (Sat GenBuses a |- Sat GenBuses (f a))
-> Dict (GenBuses ((:.:) g f a))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkIxProd k h =>
Ok' k a |- Ok' k (h a)
okIxProd @(:>) @f @a))

instance KnownNat i => OkIxProd (:>) (Vector i) where
  okIxProd :: forall a. Ok' (:>) a |- Ok' (:>) (Vector i a)
okIxProd = (Con (Sat GenBuses a) :- Con (Sat GenBuses (Vector Vector i a)))
-> Sat GenBuses a |- Sat GenBuses (Vector Vector i a)
forall a b. (Con a :- Con b) -> a |- b
Entail ((GenBuses a => Dict (GenBuses (Vector Vector i a)))
-> GenBuses a :- GenBuses (Vector Vector i a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict (GenBuses (Vector Vector i a))
GenBuses a => Dict (GenBuses (Vector Vector i a))
forall (a :: Constraint). a => Dict a
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 :: forall a b. Ok2 (:>) a b => h (a :> b) -> h a :> h b
crossF = (h (BCirc a b) -> BCirc (h a) (h b)) -> h (a :> b) -> h a :> h b
forall (h :: Type -> Type) a a' b b'.
Functor h =>
(h (BCirc a a') -> BCirc b b') -> h (a :> a') -> b :> b'
inCKF1 h (BCirc a b) -> BCirc (h a) (h b)
forall (h :: Type -> Type) a b (m :: Type -> Type).
(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

instance (IxMonoidalPCat (:>) h, Representable h, Show (R.Rep h))
      => IxProductCat (:>) h where
  exF :: forall a . Ok (:>) a => h (h a :> a)
  exF :: forall a. Ok (:>) a => h (h a :> a)
exF = (Rep h -> h a :> a) -> h (h a :> a)
forall a. (Rep h -> a) -> h a
forall (f :: Type -> Type) a.
Representable f =>
(Rep f -> a) -> f a
tabulate ((Rep h -> h a :> a) -> h (h a :> a))
-> (Rep h -> h a :> a) -> h (h a :> a)
forall a b. (a -> b) -> a -> b
$ \ Rep h
i -> String -> h a :> a
forall b a. Ok (:>) b => String -> a :> b
namedC (String
"ex " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> Rep h -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec Int
10 Rep h
i String
"") (Con (Sat GenBuses (h a)) => h a :> a)
-> (Sat GenBuses a |- Sat GenBuses (h a)) -> h a :> a
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkIxProd k h =>
Ok' k a |- Ok' k (h a)
okIxProd @(:>) @h @a
  replF :: forall a . Ok (:>) a => a :> h a
  replF :: forall a. Ok (:>) a => a :> h a
replF = String -> a :> h a
forall b a. Ok (:>) b => String -> a :> b
namedC String
"replF" (Con (Sat GenBuses (h a)) => a :> h a)
-> (Sat GenBuses a |- Sat GenBuses (h a)) -> a :> h a
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkIxProd k h =>
Ok' k a |- Ok' k (h a)
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 :: forall a. Ok (:>) a => h (a :> h a)
inPF = (Rep h -> a :> h a) -> h (a :> h a)
forall a. (Rep h -> a) -> h a
forall (f :: Type -> Type) a.
Representable f =>
(Rep f -> a) -> f a
tabulate ((Rep h -> a :> h a) -> h (a :> h a))
-> (Rep h -> a :> h a) -> h (a :> h a)
forall a b. (a -> b) -> a -> b
$ \ Rep h
i -> String -> a :> h a
forall b a. Ok (:>) b => String -> a :> b
namedC (String
"inP " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> Rep h -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec Int
10 Rep h
i String
"") (Con (Sat GenBuses (h a)) => a :> h a)
-> (Sat GenBuses a |- Sat GenBuses (h a)) -> a :> h a
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkIxProd k h =>
Ok' k a |- Ok' k (h a)
okIxProd @(:>) @h @a
  jamPF :: forall a. Ok (:>) a => h a :> a
  jamPF :: forall a. Ok (:>) a => h a :> a
jamPF = String -> h a :> a
forall b a. Ok (:>) b => String -> a :> b
namedC String
"jamPF" (Con (Sat GenBuses (h a)) => h a :> a)
-> (Sat GenBuses a |- Sat GenBuses (h a)) -> h a :> a
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkIxProd k h =>
Ok' k a |- Ok' k (h a)
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 :: forall (h :: Type -> Type) a. Buses (h a) -> h (Buses a)
unIxProdB (IxProdB h (Buses a)
bs) = h (Buses a)
h (Buses a)
bs
unIxProdB Buses (h a)
b = String -> h (Buses a)
forall a. HasCallStack => String -> a
error (String
"unIxProdB: unexpected bus: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Buses (h a) -> String
forall a. Show a => a -> String
show Buses (h a)
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 :: forall (h :: Type -> Type) a b (m :: Type -> Type).
(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 h (Buses a -> m (Buses b))
fs = (h (Buses b) -> Buses (h b)) -> m (h (Buses b)) -> m (Buses (h b))
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap h (Buses b) -> Buses (h b)
forall (h :: Type -> Type) a.
(OkIxProd (:>) h, Show1 h, Foldable h, Ok (:>) a) =>
h (Buses a) -> Buses (h a)
IxProdB (m (h (Buses b)) -> m (Buses (h b)))
-> (Buses (h a) -> m (h (Buses b)))
-> Buses (h a)
-> m (Buses (h b))
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. h (m (Buses b)) -> m (h (Buses b))
forall (t :: Type -> Type) (f :: Type -> Type) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
transpose (h (m (Buses b)) -> m (h (Buses b)))
-> (Buses (h a) -> h (m (Buses b)))
-> Buses (h a)
-> m (h (Buses b))
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. h (Buses a -> m (Buses b)) -> h (Buses a) -> h (m (Buses b))
forall a b. h (a -> b) -> h a -> h b
forall (f :: Type -> Type) a b. Zip f => f (a -> b) -> f a -> f b
zap h (Buses a -> m (Buses b))
fs (h (Buses a) -> h (m (Buses b)))
-> (Buses (h a) -> h (Buses a)) -> Buses (h a) -> h (m (Buses b))
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Buses (h a) -> h (Buses a)
forall (h :: Type -> Type) a. Buses (h a) -> h (Buses a)
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 :: forall a. Ok' (:>) a |- Ok' (:>) (U1 a)
okFunctor = (Con (Sat GenBuses a) :- Con (Sat GenBuses (U1 a)))
-> Sat GenBuses a |- Sat GenBuses (U1 a)
forall a b. (Con a :- Con b) -> a |- b
Entail ((GenBuses a => Dict (GenBuses (U1 a)))
-> GenBuses a :- GenBuses (U1 a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict (GenBuses (U1 a))
GenBuses a => Dict (GenBuses (U1 a))
forall (a :: Constraint). a => Dict a
Dict)
instance OkFunctor (:>) G.Par1 where okFunctor :: forall a. Ok' (:>) a |- Ok' (:>) (Par1 a)
okFunctor = (Con (Sat GenBuses a) :- Con (Sat GenBuses (Par1 a)))
-> Sat GenBuses a |- Sat GenBuses (Par1 a)
forall a b. (Con a :- Con b) -> a |- b
Entail ((GenBuses a => Dict (GenBuses (Par1 a)))
-> GenBuses a :- GenBuses (Par1 a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict (GenBuses (Par1 a))
GenBuses a => Dict (GenBuses (Par1 a))
forall (a :: Constraint). a => Dict a
Dict)

instance (OkFunctor (:>) f, OkFunctor (:>) g)
      => OkFunctor (:>) (f G.:*: g) where
  okFunctor :: forall a. Ok' (:>) a |- Ok' (:>) ((f G.:*: g) a)
  okFunctor :: forall a. Ok' (:>) a |- Ok' (:>) ((:*:) f g a)
okFunctor = (Con (Sat GenBuses a) :- Con (Sat GenBuses ((:*:) f g a)))
-> Sat GenBuses a |- Sat GenBuses ((:*:) f g a)
forall a b. (Con a :- Con b) -> a |- b
Entail ((GenBuses a => Dict (GenBuses ((:*:) f g a)))
-> GenBuses a :- GenBuses ((:*:) f g a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (Dict (GenBuses ((:*:) f g a))
Con (Sat GenBuses (f a)) => Dict (GenBuses ((:*:) f g a))
forall (a :: Constraint). a => Dict a
Dict
                             (Con (Sat GenBuses (f a)) => Dict (GenBuses ((:*:) f g a)))
-> (Sat GenBuses a |- Sat GenBuses (f a))
-> Dict (GenBuses ((:*:) f g a))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor' @(:>) @f @a
                             (Con (Sat GenBuses (g a)) => Dict (GenBuses ((:*:) f g a)))
-> (Sat GenBuses a |- Sat GenBuses (g a))
-> Dict (GenBuses ((:*:) f g a))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h 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 :: forall a. Ok' (:>) a |- Ok' (:>) ((:.:) g f a)
okFunctor = (Con (Sat GenBuses a) :- Con (Sat GenBuses ((:.:) g f a)))
-> Sat GenBuses a |- Sat GenBuses ((:.:) g f a)
forall a b. (Con a :- Con b) -> a |- b
Entail ((GenBuses a => Dict (GenBuses ((:.:) g f a)))
-> GenBuses a :- GenBuses ((:.:) g f a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (Dict (GenBuses ((:.:) g f a))
Con (Sat GenBuses (g (f a))) => Dict (GenBuses ((:.:) g f a))
forall (a :: Constraint). a => Dict a
Dict
                             (Con (Sat GenBuses (g (f a))) => Dict (GenBuses ((:.:) g f a)))
-> (Sat GenBuses (f a) |- Sat GenBuses (g (f a)))
-> Dict (GenBuses ((:.:) g f a))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor' @(:>) @g @(f a)
                             (Con (Sat GenBuses (f a)) => Dict (GenBuses ((:.:) g f a)))
-> (Sat GenBuses a |- Sat GenBuses (f a))
-> Dict (GenBuses ((:.:) g f a))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor' @(:>) @f @a))

instance KnownNat i => OkFunctor (:>) (Vector i) where
  okFunctor :: forall a. Ok' (:>) a |- Ok' (:>) (Vector i a)
okFunctor = (Con (Sat GenBuses a) :- Con (Sat GenBuses (Vector Vector i a)))
-> Sat GenBuses a |- Sat GenBuses (Vector Vector i a)
forall a b. (Con a :- Con b) -> a |- b
Entail ((GenBuses a => Dict (GenBuses (Vector Vector i a)))
-> GenBuses a :- GenBuses (Vector Vector i a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict (GenBuses (Vector Vector i a))
GenBuses a => Dict (GenBuses (Vector Vector i a))
forall (a :: Constraint). a => Dict a
Dict)

#ifdef WithArr
instance HasFin' a => OkFunctor (:>) (Arr a) where
  okFunctor :: forall a. Ok' (:>) a |- Ok' (:>) (Arr a a)
okFunctor = (Con (Sat GenBuses a) :- Con (Sat GenBuses (Arr a a)))
-> Sat GenBuses a |- Sat GenBuses (Arr a a)
forall a b. (Con a :- Con b) -> a |- b
Entail ((GenBuses a => Dict (GenBuses (Arr a a)))
-> GenBuses a :- GenBuses (Arr a a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict (GenBuses (Arr a a))
GenBuses a => Dict (GenBuses (Arr a a))
forall (a :: Constraint). a => Dict a
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 :: forall a b. Ok2 (:>) a b => (a :> b) -> h a :> h b
fmapC = (BCirc a b -> BCirc (h a) (h b)) -> (a :> b) -> h a :> h b
forall a a' b b'.
(BCirc a a' -> BCirc b b') -> (a :> a') -> b :> b'
inCK ((BCirc a b -> BCirc (h a) (h b)) -> (a :> b) -> h a :> h b)
-> (BCirc a b -> BCirc (h a) (h b)) -> (a :> b) -> h a :> h b
forall a b. (a -> b) -> a -> b
$ \ BCirc a b
f Buses (h a)
as ->
            do Buses (a -> b)
ab <- BCirc a b -> CircuitM (Buses (a -> b))
forall b c. Ok2 (:>) b c => BCirc b c -> CircuitM (Buses (b -> c))
genSubgraph BCirc a b
f
               Template ((a -> b) :* h a) (h b) -> BCirc ((a -> b) :* h a) (h b)
forall a b. Ok (:>) b => Template a b -> BCirc a b
genComp (String -> Template ((a -> b) :* h a) (h b)
forall a b. String -> Template a b
Prim String
"fmap") (Buses (a -> b) -> Buses (h a) -> Buses ((a -> b) :* h a)
forall h a. Ok2 (:>) h a => Buses h -> Buses a -> Buses (h :* a)
ProdB Buses (a -> b)
ab Buses (h a)
as)
                 (Con (Sat GenBuses (h a)) => CircuitM (Buses (h b)))
-> (Sat GenBuses a |- Sat GenBuses (h a)) -> CircuitM (Buses (h b))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor' @(:>) @h @a
                 (Con (Sat GenBuses (h b)) => CircuitM (Buses (h b)))
-> (Sat GenBuses b |- Sat GenBuses (h b)) -> CircuitM (Buses (h b))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor' @(:>) @h @b
  unzipC :: forall a b. Ok2 (:>) a b => h (a :* b) :> (h a :* h b)
  unzipC :: forall a b. Ok2 (:>) a b => h (a :* b) :> (h a :* h b)
unzipC = String -> h (a :* b) :> (h a :* h b)
forall b a. Ok (:>) b => String -> a :> b
namedC String
"unzip"
             (Con (Sat GenBuses (h (a :* b))) => h (a :* b) :> (h a :* h b))
-> (Sat GenBuses (a :* b) |- Sat GenBuses (h (a :* b)))
-> h (a :* b) :> (h a :* h b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor' @(:>) @h @(a :* b)
             (Con (Sat GenBuses (h a)) => h (a :* b) :> (h a :* h b))
-> (Sat GenBuses a |- Sat GenBuses (h a))
-> h (a :* b) :> (h a :* h b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor' @(:>) @h @a
             (Con (Sat GenBuses (h b)) => h (a :* b) :> (h a :* h b))
-> (Sat GenBuses b |- Sat GenBuses (h b))
-> h (a :* b) :> (h a :* h b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (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 :: forall a b. Ok2 (:>) a b => (h a :* h b) :> h (a :* b)
zipC = String -> (h a :* h b) :> h (a :* b)
forall b a. Ok (:>) b => String -> a :> b
namedC String
"zip"
           (Con (Sat GenBuses (h (a :* b))) => (h a :* h b) :> h (a :* b))
-> (Sat GenBuses (a :* b) |- Sat GenBuses (h (a :* b)))
-> (h a :* h b) :> h (a :* b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor' @(:>) @h @(a :* b)
           (Con (Sat GenBuses (h a)) => (h a :* h b) :> h (a :* b))
-> (Sat GenBuses a |- Sat GenBuses (h a))
-> (h a :* h b) :> h (a :* b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor' @(:>) @h @a
           (Con (Sat GenBuses (h b)) => (h a :* h b) :> h (a :* b))
-> (Sat GenBuses b |- Sat GenBuses (h b))
-> (h a :* h b) :> h (a :* b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (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 :: a :> h a
pointC = String -> a :> h a
forall b a. Ok (:>) b => String -> a :> b
namedC String
"point"
             (Con (Sat GenBuses (h a)) => a :> h a)
-> (Sat GenBuses a |- Sat GenBuses (h a)) -> a :> h a
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor' @(:>) @h @a

instance (OkFunctor (:>) h, Additive a, Ok (:>) a) => AddCat (:>) h a where
  sumAC :: h a :> a
  sumAC :: h a :> a
sumAC = String -> h a :> a
forall b a. Ok (:>) b => String -> a :> b
namedC String
"sumA" (Con (Sat GenBuses (h a)) => h a :> a)
-> (Sat GenBuses a |- Sat GenBuses (h a)) -> h a :> a
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor' @(:>) @h @a

instance (OkFunctor (:>) h, Ord a, Ok (:>) a) => MinMaxFunctorCat (:>) h a where
  minimumC :: h a :> a
  minimumC :: h a :> a
minimumC = String -> h a :> a
forall b a. Ok (:>) b => String -> a :> b
namedC String
"minimum" (Con (Sat GenBuses (h a)) => h a :> a)
-> (Sat GenBuses a |- Sat GenBuses (h a)) -> h a :> a
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor' @(:>) @h @a
  maximumC :: h a :> a
  maximumC :: h a :> a
maximumC = String -> h a :> a
forall b a. Ok (:>) b => String -> a :> b
namedC String
"maximum" (Con (Sat GenBuses (h a)) => h a :> a)
-> (Sat GenBuses a |- Sat GenBuses (h a)) -> h a :> a
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor' @(:>) @h @a

instance (OkFunctor (:>) h, Foldable h, Ord a, Ok (:>) a) => MinMaxFFunctorCat (:>) h a where
  minimumCF :: h a -> (a :* (h a :> a))
  minimumCF :: h a -> a :* (h a :> a)
minimumCF h a
h = (h a -> a
forall a. Ord a => h a -> a
forall (t :: Type -> Type) a. (Foldable t, Ord a) => t a -> a
minimum h a
h, String -> h a :> a
forall b a. Ok (:>) b => String -> a :> b
namedC String
"minimumF" (Con (Sat GenBuses (h a)) => h a :> a)
-> (Sat GenBuses a |- Sat GenBuses (h a)) -> h a :> a
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor' @(:>) @h @a)
  maximumCF :: h a -> (a :* (h a :> a))
  maximumCF :: h a -> a :* (h a :> a)
maximumCF h a
h = (h a -> a
forall a. Ord a => h a -> a
forall (t :: Type -> Type) a. (Foldable t, Ord a) => t a -> a
maximum h a
h, String -> h a :> a
forall b a. Ok (:>) b => String -> a :> b
namedC String
"maximumF" (Con (Sat GenBuses (h a)) => h a :> a)
-> (Sat GenBuses a |- Sat GenBuses (h a)) -> h a :> a
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
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' :: forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor' = {- trace "" $ -} forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
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 :: forall a. Ok (:>) a => f (g a) :> g (f a)
distributeC = String -> f (g a) :> g (f a)
forall b a. Ok (:>) b => String -> a :> b
namedC String
"distribute"
                  (Con (Sat GenBuses (g (f a))) => f (g a) :> g (f a))
-> (Sat GenBuses (f a) |- Sat GenBuses (g (f a)))
-> f (g a) :> g (f a)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor' @(:>) @g @(f a) (Con (Sat GenBuses (f a)) => f (g a) :> g (f a))
-> (Sat GenBuses a |- Sat GenBuses (f a)) -> f (g a) :> g (f a)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor' @(:>) @f @a
                  (Con (Sat GenBuses (f (g a))) => f (g a) :> g (f a))
-> (Sat GenBuses (g a) |- Sat GenBuses (f (g a)))
-> f (g a) :> g (f a)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor' @(:>) @f @(g a) (Con (Sat GenBuses (g a)) => f (g a) :> g (f a))
-> (Sat GenBuses a |- Sat GenBuses (g a)) -> f (g a) :> g (f a)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h 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 :: forall a. Ok (:>) a => (Rep f -> a) :> f a
tabulateC = -- trace "tabulateC @(:>)" $
              String -> (Rep f -> a) :> f a
forall b a. Ok (:>) b => String -> a :> b
namedC String
"tabulate" (Con (Sat GenBuses (f a)) => (Rep f -> a) :> f a)
-> (Sat GenBuses a |- Sat GenBuses (f a)) -> (Rep f -> a) :> f a
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor' @(:>) @f @a
  indexC :: forall a. Ok (:>) a => f a :> (R.Rep f -> a)
  indexC :: forall a. Ok (:>) a => f a :> (Rep f -> a)
indexC = String -> f a :> (Rep f -> a)
forall b a. Ok (:>) b => String -> a :> b
namedC String
"index" (Con (Sat GenBuses (f a)) => f a :> (Rep f -> a))
-> (Sat GenBuses a |- Sat GenBuses (f a)) -> f a :> (Rep f -> a)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
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 :: forall a b. Ok2 (:>) a b => a :> b
bottomG = -- trace "bottomG called" $
          String -> z :> b
forall b a. Ok (:>) b => String -> a :> b
namedC String
"⊥" -- "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 :: a :> b
bottomC = a :> b
forall a b. Ok2 (:>) a b => a :> b
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 :: Source -> Buses ()
toBuses = Buses () -> Source -> Buses ()
forall (k :: Type -> Type -> Type) b a.
(ConstCat k b, Ok k a) =>
b -> k a b
const Buses ()
UnitB
instance SourceToBuses Bool    where toBuses :: Source -> Buses Bool
toBuses = Source -> Buses Bool
forall b. Source -> Buses b
PrimB
instance SourceToBuses Int     where toBuses :: Source -> Buses Int
toBuses = Source -> Buses Int
forall b. Source -> Buses b
PrimB
instance SourceToBuses Integer where toBuses :: Source -> Buses Integer
toBuses = Source -> Buses Integer
forall b. Source -> Buses b
PrimB
instance SourceToBuses Float   where toBuses :: Source -> Buses Float
toBuses = Source -> Buses Float
forall b. Source -> Buses b
PrimB
instance SourceToBuses Double  where toBuses :: Source -> Buses Double
toBuses = Source -> Buses Double
forall b. Source -> Buses b
PrimB

instance KnownNat n => SourceToBuses (Finite n) where toBuses :: Source -> Buses (Finite n)
toBuses = Source -> Buses (Finite n)
forall b. Source -> Buses b
PrimB

#ifdef VectorSized
instance (KnownNat n, GenBuses b) => SourceToBuses (Vector n b) where
  toBuses :: Source -> Buses (Vector n b)
toBuses = Source -> Buses (Vector n b)
forall b. Source -> Buses b
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 :: forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB = Buses a -> CircuitM (Maybe (Buses a))
forall (f :: Type -> Type) a. Applicative f => a -> f (Maybe a)
justA (Buses a -> CircuitM (Maybe (Buses a)))
-> (Source -> Buses a) -> Source -> CircuitM (Maybe (Buses a))
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Source -> Buses a
forall a. SourceToBuses a => Source -> Buses a
toBuses

unknownName :: PrimName
unknownName :: String
unknownName = String
"??"

instance Ok2 (:>) a b => UnknownCat (:>) a b where
  unknownC :: a :> b
unknownC = String -> a :> b
forall b a. Ok (:>) b => String -> a :> b
namedC String
unknownName

#define Sat(pred) ((pred) -> True)
#define Eql(x) Sat(==(x))

pattern Read :: Read a => a -> String
pattern $mRead :: forall {r} {a}. Read a => String -> (a -> r) -> ((# #) -> r) -> r
Read x <- (reads -> [(x,"")])

pattern ConstS :: PrimName -> Source
pattern $mConstS :: forall {r}. Source -> (String -> r) -> ((# #) -> r) -> r
ConstS name <- PSource _ name []

pattern Val :: Read a => a -> Source
pattern $mVal :: forall {r} {a}. Read a => Source -> (a -> r) -> ((# #) -> r) -> r
Val x <- ConstS (Read x)

-- pattern Val x       <- ConstS (reads -> [(x,"")])

pattern TrueS :: Source
pattern $mTrueS :: forall {r}. Source -> ((# #) -> r) -> ((# #) -> r) -> r
TrueS  <- ConstS("True")

pattern FalseS :: Source
pattern $mFalseS :: forall {r}. Source -> ((# #) -> r) -> ((# #) -> r) -> r
FalseS <- ConstS("False")

pattern NotS :: Source -> Source
pattern $mNotS :: forall {r}. Source -> (Source -> r) -> ((# #) -> r) -> r
NotS a <- PSource _ "not" [a]

pattern XorS :: Source -> Source -> Source
pattern $mXorS :: forall {r}. Source -> (Source -> Source -> r) -> ((# #) -> r) -> r
XorS a b <- PSource _ "xor" [a,b]

pattern EqS :: Source -> Source -> Source
pattern $mEqS :: forall {r}. Source -> (Source -> Source -> r) -> ((# #) -> r) -> r
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 :: Bool :> Bool
notC = String -> Opt Bool -> Bool :> Bool
forall b a. Ok (:>) b => String -> Opt b -> a :> b
primOpt String
"not" (Opt Bool -> Bool :> Bool) -> Opt Bool -> Bool :> Bool
forall a b. (a -> b) -> a -> b
$ \ case
           [NotS Source
a]  -> Source -> CircuitM (Maybe (Buses Bool))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
a
           [Val Bool
x]   -> Bool -> CircuitM (Maybe (Buses Bool))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal (Bool -> Bool
not Bool
x)
           [Source]
_         -> CircuitM (Maybe (Buses Bool))
forall (f :: Type -> Type) a. Applicative f => f (Maybe a)
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 :: (Bool :* Bool) :> Bool
andC = String -> Opt Bool -> (Bool :* Bool) :> Bool
forall a b. Ok2 (:>) a b => String -> Opt b -> a :> b
primOptSort String
"&&" (Opt Bool -> (Bool :* Bool) :> Bool)
-> Opt Bool -> (Bool :* Bool) :> Bool
forall a b. (a -> b) -> a -> b
$ \ case
           [Source
TrueS ,Source
y]            -> Source -> CircuitM (Maybe (Buses Bool))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
y
           [Source
x,Source
TrueS ]            -> Source -> CircuitM (Maybe (Buses Bool))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
x
           [x :: Source
x@Source
FalseS,Source
_]          -> Source -> CircuitM (Maybe (Buses Bool))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
x
           [Source
_,y :: Source
y@Source
FalseS]          -> Source -> CircuitM (Maybe (Buses Bool))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
y
#if !defined NoIdempotence
           [Source
x,Source
x']      | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x -> Source -> CircuitM (Maybe (Buses Bool))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
x
#endif
           [Source
x,NotS Source
x'] | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x -> Bool -> CircuitM (Maybe (Buses Bool))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal Bool
False
           [NotS Source
x,Source
x'] | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x -> Bool -> CircuitM (Maybe (Buses Bool))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal Bool
False
           [Source]
_                     -> CircuitM (Maybe (Buses Bool))
forall (f :: Type -> Type) a. Applicative f => f (Maybe a)
nothingA
  orC :: (Bool :* Bool) :> Bool
orC  = String -> Opt Bool -> (Bool :* Bool) :> Bool
forall a b. Ok2 (:>) a b => String -> Opt b -> a :> b
primOptSort String
"||" (Opt Bool -> (Bool :* Bool) :> Bool)
-> Opt Bool -> (Bool :* Bool) :> Bool
forall a b. (a -> b) -> a -> b
$ \ case
           [Source
FalseS,Source
y]            -> Source -> CircuitM (Maybe (Buses Bool))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
y
           [Source
x,Source
FalseS]            -> Source -> CircuitM (Maybe (Buses Bool))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
x
           [x :: Source
x@Source
TrueS ,Source
_]          -> Source -> CircuitM (Maybe (Buses Bool))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
x
           [Source
_,y :: Source
y@Source
TrueS ]          -> Source -> CircuitM (Maybe (Buses Bool))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
y
#if !defined NoIdempotence
           [Source
x,Source
x']      | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x -> Source -> CircuitM (Maybe (Buses Bool))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
x
#endif
           [Source
x,NotS Source
x'] | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x -> Bool -> CircuitM (Maybe (Buses Bool))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal Bool
True
           [NotS Source
x,Source
x'] | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x -> Bool -> CircuitM (Maybe (Buses Bool))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal Bool
True
           -- not a    || not b == not (a && b)
           -- TODO: Handle more elegantly.
           [NotS Source
x, NotS Source
y]      ->
             do Buses Bool
o <- ((Bool :* Bool) :> Bool) -> BCirc (Bool :* Bool) Bool
forall a b. (a :> b) -> BCirc a b
unmkCK (Bool :* Bool) :> Bool
forall (k :: Type -> Type -> Type).
BoolCat k =>
k (Bool :* Bool) Bool
andC (Buses Bool -> Buses Bool -> Buses (Bool :* Bool)
forall h a. Ok2 (:>) h a => Buses h -> Buses a -> Buses (h :* a)
ProdB (Source -> Buses Bool
forall b. Source -> Buses b
PrimB Source
x) (Source -> Buses Bool
forall b. Source -> Buses b
PrimB Source
y))
                (Bool :> Bool) -> Buses Bool -> CircuitM (Maybe (Buses Bool))
forall a b. (a :> b) -> Buses a -> CircuitM (Maybe (Buses b))
newComp Bool :> Bool
forall (k :: Type -> Type -> Type). BoolCat k => k Bool Bool
notC Buses Bool
o
           [Source]
_                     -> CircuitM (Maybe (Buses Bool))
forall (f :: Type -> Type) a. Applicative f => f (Maybe a)
nothingA
  xorC :: (Bool :* Bool) :> Bool
xorC = String -> Opt Bool -> (Bool :* Bool) :> Bool
forall a b. Ok2 (:>) a b => String -> Opt b -> a :> b
primOptSort String
"xor" (Opt Bool -> (Bool :* Bool) :> Bool)
-> Opt Bool -> (Bool :* Bool) :> Bool
forall a b. (a -> b) -> a -> b
$ \ case
           [Source
FalseS,Source
y]            -> Source -> CircuitM (Maybe (Buses Bool))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
y
           [Source
x,Source
FalseS]            -> Source -> CircuitM (Maybe (Buses Bool))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
x
           [Source
TrueS,Source
y ]            -> (Bool :> Bool) -> Source -> CircuitM (Maybe (Buses Bool))
forall a b.
SourceToBuses a =>
(a :> b) -> Source -> CircuitM (Maybe (Buses b))
newComp1 Bool :> Bool
forall (k :: Type -> Type -> Type). BoolCat k => k Bool Bool
notC Source
y
           [Source
x,Source
TrueS ]            -> (Bool :> Bool) -> Source -> CircuitM (Maybe (Buses Bool))
forall a b.
SourceToBuses a =>
(a :> b) -> Source -> CircuitM (Maybe (Buses b))
newComp1 Bool :> Bool
forall (k :: Type -> Type -> Type). BoolCat k => k Bool Bool
notC Source
x
           [Source
x,Source
x']      | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x -> Bool -> CircuitM (Maybe (Buses Bool))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal Bool
False
           [Source
x,NotS Source
x'] | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x -> Bool -> CircuitM (Maybe (Buses Bool))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal Bool
True
           [NotS Source
x,Source
x'] | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x -> Bool -> CircuitM (Maybe (Buses Bool))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal Bool
True
#if 1
           -- not x `xor` y == not (x `xor` y)
           [NotS Source
x, Source
y]                -> ((Bool :* Bool) :> Bool)
-> Source -> Source -> CircuitM (Maybe (Buses Bool))
forall a b c.
(SourceToBuses a, SourceToBuses b) =>
((a :* b) :> c) -> Source -> Source -> CircuitM (Maybe (Buses c))
newComp2 (Bool :> Bool
forall (k :: Type -> Type -> Type). BoolCat k => k Bool Bool
notC (Bool :> Bool)
-> ((Bool :* Bool) :> Bool) -> (Bool :* Bool) :> Bool
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (Bool :* Bool) :> Bool
forall (k :: Type -> Type -> Type).
BoolCat k =>
k (Bool :* Bool) Bool
xorC) Source
x Source
y
           [Source
x, NotS Source
y]                -> ((Bool :* Bool) :> Bool)
-> Source -> Source -> CircuitM (Maybe (Buses Bool))
forall a b c.
(SourceToBuses a, SourceToBuses b) =>
((a :* b) :> c) -> Source -> Source -> CircuitM (Maybe (Buses c))
newComp2 (Bool :> Bool
forall (k :: Type -> Type -> Type). BoolCat k => k Bool Bool
notC (Bool :> Bool)
-> ((Bool :* Bool) :> Bool) -> (Bool :* Bool) :> Bool
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (Bool :* Bool) :> Bool
forall (k :: Type -> Type -> Type).
BoolCat k =>
k (Bool :* Bool) Bool
xorC) Source
x Source
y
           -- x `xor` (x `xor` y) == y
           [Source
x, Source
x' `XorS` Source
y] | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x -> Source -> CircuitM (Maybe (Buses Bool))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
y
           [Source
x, Source
y `XorS` Source
x'] | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x -> Source -> CircuitM (Maybe (Buses Bool))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
y
           [Source
x `XorS` Source
y, Source
x'] | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x -> Source -> CircuitM (Maybe (Buses Bool))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
y
           [Source
y `XorS` Source
x, Source
x'] | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x -> Source -> CircuitM (Maybe (Buses Bool))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
y
#endif
           [Source]
_                          -> CircuitM (Maybe (Buses Bool))
forall (f :: Type -> Type) a. Applicative f => f (Maybe a)
nothingA

boolToIntC :: Bool :> Int
boolToIntC :: Bool :> Int
boolToIntC = String -> Bool :> Int
forall b a. Ok (:>) b => String -> a :> b
namedC String
"boolToInt"

#if 1

-- noOpt :: Opt b
-- noOpt = const nothingA

eqOpt, neOpt :: forall a. (Read a, Eq a) => Opt Bool
eqOpt :: forall a. (Read a, Eq a) => Opt Bool
eqOpt = \ case
  [Val (a
x :: a), Val a
y] -> Bool -> CircuitM (Maybe (Buses Bool))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal (a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y)
  [Source
a,Source
b] | Source
a Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
b -> Bool -> CircuitM (Maybe (Buses Bool))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal Bool
True
  [Source]
_              -> CircuitM (Maybe (Buses Bool))
forall (f :: Type -> Type) a. Applicative f => f (Maybe a)
nothingA
neOpt :: forall a. (Read a, Eq a) => Opt Bool
neOpt = \ case
  [Val (a
x :: a), Val a
y] -> Bool -> CircuitM (Maybe (Buses Bool))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal (a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
y)
  [Source
a,Source
b] | Source
a Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
b -> Bool -> CircuitM (Maybe (Buses Bool))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal Bool
False
  [Source]
_              -> CircuitM (Maybe (Buses Bool))
forall (f :: Type -> Type) a. Applicative f => f (Maybe a)
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 :: forall (k :: Type -> Type -> Type).
EqCat k Bool =>
k (Bool :* Bool) Bool
iffC = k (Bool :* Bool) Bool
forall (k :: Type -> Type -> Type) a.
EqCat k a =>
k (Prod k a a) Bool
equal

eqOptB, neOptB :: Opt Bool
-- eqOptB = noOpt
-- neOptB = noOpt

eqOptB :: Opt Bool
eqOptB = \ case
  [Source
TrueS,Source
y]                           -> Source -> CircuitM (Maybe (Buses Bool))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
y
  [Source
x,Source
TrueS]                           -> Source -> CircuitM (Maybe (Buses Bool))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
x
  [Source
FalseS,Source
y ]                         -> (Bool :> Bool) -> Source -> CircuitM (Maybe (Buses Bool))
forall a b.
SourceToBuses a =>
(a :> b) -> Source -> CircuitM (Maybe (Buses b))
newComp1 Bool :> Bool
forall (k :: Type -> Type -> Type). BoolCat k => k Bool Bool
notC Source
y
  [Source
x,Source
FalseS ]                         -> (Bool :> Bool) -> Source -> CircuitM (Maybe (Buses Bool))
forall a b.
SourceToBuses a =>
(a :> b) -> Source -> CircuitM (Maybe (Buses b))
newComp1 Bool :> Bool
forall (k :: Type -> Type -> Type). BoolCat k => k Bool Bool
notC Source
x
  [Source
x,NotS Source
x']      | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x          -> Bool -> CircuitM (Maybe (Buses Bool))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal Bool
False
  [NotS Source
x,Source
x']      | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x          -> Bool -> CircuitM (Maybe (Buses Bool))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal Bool
False
  -- not x == y == not (x == y)
  [NotS Source
x, Source
y]                         -> ((Bool :* Bool) :> Bool)
-> Source -> Source -> CircuitM (Maybe (Buses Bool))
forall a b c.
(SourceToBuses a, SourceToBuses b) =>
((a :* b) :> c) -> Source -> Source -> CircuitM (Maybe (Buses c))
newComp2 (Bool :> Bool
forall (k :: Type -> Type -> Type). BoolCat k => k Bool Bool
notC (Bool :> Bool)
-> ((Bool :* Bool) :> Bool) -> (Bool :* Bool) :> Bool
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (Bool :* Bool) :> Bool
forall (k :: Type -> Type -> Type).
EqCat k Bool =>
k (Bool :* Bool) Bool
iffC) Source
x Source
y
  [Source
x, NotS Source
y]                         -> ((Bool :* Bool) :> Bool)
-> Source -> Source -> CircuitM (Maybe (Buses Bool))
forall a b c.
(SourceToBuses a, SourceToBuses b) =>
((a :* b) :> c) -> Source -> Source -> CircuitM (Maybe (Buses c))
newComp2 (Bool :> Bool
forall (k :: Type -> Type -> Type). BoolCat k => k Bool Bool
notC (Bool :> Bool)
-> ((Bool :* Bool) :> Bool) -> (Bool :* Bool) :> Bool
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (Bool :* Bool) :> Bool
forall (k :: Type -> Type -> Type).
EqCat k Bool =>
k (Bool :* Bool) Bool
iffC) Source
x Source
y
  -- x == (x /= y) == not y
  [Source
x, Source
x' `XorS` Source
y] | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x          -> (Bool :> Bool) -> Source -> CircuitM (Maybe (Buses Bool))
forall a b.
SourceToBuses a =>
(a :> b) -> Source -> CircuitM (Maybe (Buses b))
newComp1 Bool :> Bool
forall (k :: Type -> Type -> Type). BoolCat k => k Bool Bool
notC Source
y
  [Source
x, Source
y `XorS` Source
x'] | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x          -> (Bool :> Bool) -> Source -> CircuitM (Maybe (Buses Bool))
forall a b.
SourceToBuses a =>
(a :> b) -> Source -> CircuitM (Maybe (Buses b))
newComp1 Bool :> Bool
forall (k :: Type -> Type -> Type). BoolCat k => k Bool Bool
notC Source
y
  [Source
x `XorS` Source
y, Source
x'] | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x          -> (Bool :> Bool) -> Source -> CircuitM (Maybe (Buses Bool))
forall a b.
SourceToBuses a =>
(a :> b) -> Source -> CircuitM (Maybe (Buses b))
newComp1 Bool :> Bool
forall (k :: Type -> Type -> Type). BoolCat k => k Bool Bool
notC Source
y
  [Source
y `XorS` Source
x, Source
x'] | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x          -> (Bool :> Bool) -> Source -> CircuitM (Maybe (Buses Bool))
forall a b.
SourceToBuses a =>
(a :> b) -> Source -> CircuitM (Maybe (Buses b))
newComp1 Bool :> Bool
forall (k :: Type -> Type -> Type). BoolCat k => k Bool Bool
notC Source
y
  -- x == (x == y) == y
  [Source
x, Source
x' `EqS` Source
y]  | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x          -> Source -> CircuitM (Maybe (Buses Bool))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
y
  [Source
x, Source
y `EqS` Source
x']  | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x          -> Source -> CircuitM (Maybe (Buses Bool))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
y
  [Source
x `EqS` Source
y, Source
z]   | Source
z Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x Bool -> Bool -> Bool
|| Source
z Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
y -> Source -> CircuitM (Maybe (Buses Bool))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
y
  [Source]
_                                   -> CircuitM (Maybe (Buses Bool))
forall (f :: Type -> Type) a. Applicative f => f (Maybe a)
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 :: Opt Bool
neOptB = \ case
  [Source
FalseS,Source
y]                          -> Source -> CircuitM (Maybe (Buses Bool))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
y
  [Source
x,Source
FalseS]                          -> Source -> CircuitM (Maybe (Buses Bool))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
x
  [Source
TrueS,Source
y ]                          -> (Bool :> Bool) -> Source -> CircuitM (Maybe (Buses Bool))
forall a b.
SourceToBuses a =>
(a :> b) -> Source -> CircuitM (Maybe (Buses b))
newComp1 Bool :> Bool
forall (k :: Type -> Type -> Type). BoolCat k => k Bool Bool
notC Source
y
  [Source
x,Source
TrueS ]                          -> (Bool :> Bool) -> Source -> CircuitM (Maybe (Buses Bool))
forall a b.
SourceToBuses a =>
(a :> b) -> Source -> CircuitM (Maybe (Buses b))
newComp1 Bool :> Bool
forall (k :: Type -> Type -> Type). BoolCat k => k Bool Bool
notC Source
x
  [Source
x,Source
x']           | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x          -> Bool -> CircuitM (Maybe (Buses Bool))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal Bool
False
  [Source
x,NotS Source
x']      | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x          -> Bool -> CircuitM (Maybe (Buses Bool))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal Bool
True
  [NotS Source
x,Source
x']      | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x          -> Bool -> CircuitM (Maybe (Buses Bool))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal Bool
True
  -- not x `xor` y == not (x `xor` y)
  [NotS Source
x, Source
y]                         -> ((Bool :* Bool) :> Bool)
-> Source -> Source -> CircuitM (Maybe (Buses Bool))
forall a b c.
(SourceToBuses a, SourceToBuses b) =>
((a :* b) :> c) -> Source -> Source -> CircuitM (Maybe (Buses c))
newComp2 (Bool :> Bool
forall (k :: Type -> Type -> Type). BoolCat k => k Bool Bool
notC (Bool :> Bool)
-> ((Bool :* Bool) :> Bool) -> (Bool :* Bool) :> Bool
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (Bool :* Bool) :> Bool
forall (k :: Type -> Type -> Type).
BoolCat k =>
k (Bool :* Bool) Bool
xorC) Source
x Source
y
  [Source
x, NotS Source
y]                         -> ((Bool :* Bool) :> Bool)
-> Source -> Source -> CircuitM (Maybe (Buses Bool))
forall a b c.
(SourceToBuses a, SourceToBuses b) =>
((a :* b) :> c) -> Source -> Source -> CircuitM (Maybe (Buses c))
newComp2 (Bool :> Bool
forall (k :: Type -> Type -> Type). BoolCat k => k Bool Bool
notC (Bool :> Bool)
-> ((Bool :* Bool) :> Bool) -> (Bool :* Bool) :> Bool
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (Bool :* Bool) :> Bool
forall (k :: Type -> Type -> Type).
BoolCat k =>
k (Bool :* Bool) Bool
xorC) Source
x Source
y
  -- x `xor` (x `xor` y) == y
  [Source
x, Source
x' `XorS` Source
y] | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x          -> Source -> CircuitM (Maybe (Buses Bool))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
y
  [Source
x, Source
y `XorS` Source
x'] | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x          -> Source -> CircuitM (Maybe (Buses Bool))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
y
  [Source
x `XorS` Source
y, Source
x'] | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x          -> Source -> CircuitM (Maybe (Buses Bool))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
y
  [Source
y `XorS` Source
x, Source
x'] | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x          -> Source -> CircuitM (Maybe (Buses Bool))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
y
  -- x `xor` (x == y) == not y
  [Source
x, Source
x' `EqS` Source
y]  | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x          -> (Bool :> Bool) -> Source -> CircuitM (Maybe (Buses Bool))
forall a b.
SourceToBuses a =>
(a :> b) -> Source -> CircuitM (Maybe (Buses b))
newComp1 Bool :> Bool
forall (k :: Type -> Type -> Type). BoolCat k => k Bool Bool
notC Source
y
  [Source
x, Source
y `EqS` Source
x']  | Source
x' Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x          -> (Bool :> Bool) -> Source -> CircuitM (Maybe (Buses Bool))
forall a b.
SourceToBuses a =>
(a :> b) -> Source -> CircuitM (Maybe (Buses b))
newComp1 Bool :> Bool
forall (k :: Type -> Type -> Type). BoolCat k => k Bool Bool
notC Source
y
  [Source
x `EqS` Source
y, Source
z]   | Source
z Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
x Bool -> Bool -> Bool
|| Source
z Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
y -> (Bool :> Bool) -> Source -> CircuitM (Maybe (Buses Bool))
forall a b.
SourceToBuses a =>
(a :> b) -> Source -> CircuitM (Maybe (Buses b))
newComp1 Bool :> Bool
forall (k :: Type -> Type -> Type). BoolCat k => k Bool Bool
notC Source
y
  [Source]
_                                   -> CircuitM (Maybe (Buses Bool))
forall (f :: Type -> Type) a. Applicative f => f (Maybe a)
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 :: (Bool :* Bool) :> Bool
equal    = String -> Opt Bool -> (Bool :* Bool) :> Bool
forall a b. Ok2 (:>) a b => String -> Opt b -> a :> b
primOptSort String
"=="  (forall a. (Read a, Eq a) => Opt Bool
eqOpt @Bool Binop (Opt Bool)
forall b. Binop (Opt b)
`orOpt` Opt Bool
eqOptB)
  notEqual :: (Bool :* Bool) :> Bool
notEqual = String -> Opt Bool -> (Bool :* Bool) :> Bool
forall a b. Ok2 (:>) a b => String -> Opt b -> a :> b
primOptSort String
"xor" (forall a. (Read a, Eq a) => Opt Bool
neOpt @Bool Binop (Opt Bool)
forall b. Binop (Opt b)
`orOpt` Opt Bool
neOptB)

instance EqCat (:>) () where
  equal :: Prod (:>) () () :> Bool
equal = Bool -> Prod (:>) () () :> Bool
forall b a. GS b => b -> a :> b
constC Bool
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 :: forall a. (Read a, Ord a) => Opt Bool
ltOpt = \ case
  [Val (a
x :: a), Val a
y] -> Bool -> CircuitM (Maybe (Buses Bool))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal (a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
y)
  [Source
a,Source
b] | Source
a Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
b        -> Bool -> CircuitM (Maybe (Buses Bool))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal Bool
False
  [Source]
_                     -> CircuitM (Maybe (Buses Bool))
forall (f :: Type -> Type) a. Applicative f => f (Maybe a)
nothingA
gtOpt :: forall a. (Read a, Ord a) => Opt Bool
gtOpt = \ case
  [Val (a
x :: a), Val a
y] -> Bool -> CircuitM (Maybe (Buses Bool))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal (a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
y)
  [Source
a,Source
b] | Source
a Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
b        -> Bool -> CircuitM (Maybe (Buses Bool))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal Bool
False
  [Source]
_                     -> CircuitM (Maybe (Buses Bool))
forall (f :: Type -> Type) a. Applicative f => f (Maybe a)
nothingA
leOpt :: forall a. (Read a, Ord a) => Opt Bool
leOpt = \ case
  [Val (a
x :: a), Val a
y] -> Bool -> CircuitM (Maybe (Buses Bool))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal (a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
y)
  [Source
a,Source
b] | Source
a Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
b        -> Bool -> CircuitM (Maybe (Buses Bool))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal Bool
True
  [Source]
_                     -> CircuitM (Maybe (Buses Bool))
forall (f :: Type -> Type) a. Applicative f => f (Maybe a)
nothingA
geOpt :: forall a. (Read a, Ord a) => Opt Bool
geOpt = \ case
  [Val (a
x :: a), Val a
y] -> Bool -> CircuitM (Maybe (Buses Bool))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal (a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
y)
  [Source
a,Source
b] | Source
a Source -> Source -> Bool
forall a. Eq a => a -> a -> Bool
== Source
b        -> Bool -> CircuitM (Maybe (Buses Bool))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal Bool
True
  [Source]
_                     -> CircuitM (Maybe (Buses Bool))
forall (f :: Type -> Type) a. Applicative f => f (Maybe a)
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 :: Prod (:>) () () :> Bool
lessThan = Bool -> Prod (:>) () () :> Bool
forall b a. GS b => b -> a :> b
constC Bool
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 :: Prod (:>) a a :> a
minC = String -> Prod (:>) a a :> a
forall b a. Ok (:>) b => String -> a :> b
namedC String
"min"
  maxC :: Prod (:>) a a :> a
maxC = String -> Prod (:>) a a :> a
forall b a. Ok (:>) b => String -> a :> b
namedC String
"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 $mNegateS :: forall {r}. Source -> (Source -> r) -> ((# #) -> r) -> r
NegateS a <- PSource _ "negate" [a]

pattern RecipS  :: Source -> Source
pattern $mRecipS :: forall {r}. Source -> (Source -> r) -> ((# #) -> r) -> r
RecipS  a <- PSource _ "recip"  [a]

instance (Num a, Read a, GS a, Eq a, SourceToBuses a)
      => NumCat (:>) a where
  negateC :: a :> a
negateC = String -> Opt a -> a :> a
forall b a. Ok (:>) b => String -> Opt b -> a :> b
primOpt String
"negate" (Opt a -> a :> a) -> Opt a -> a :> a
forall a b. (a -> b) -> a -> b
$ \ case
              [Val a
x]         -> a -> CircuitM (Maybe (Buses a))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal (a -> a
forall a. Num a => a -> a
negate a
x)
              [NegateS Source
x]     -> Source -> CircuitM (Maybe (Buses a))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
x
              [Source]
_               -> CircuitM (Maybe (Buses a))
forall (f :: Type -> Type) a. Applicative f => f (Maybe a)
nothingA
  addC :: Prod (:>) a a :> a
addC    = String -> Opt a -> Prod (:>) a a :> a
forall a b. Ok2 (:>) a b => String -> Opt b -> a :> b
primOptSort String
"+" (Opt a -> Prod (:>) a a :> a) -> Opt a -> Prod (:>) a a :> a
forall a b. (a -> b) -> a -> b
$ \ case
              [Val a
x, Val a
y]  -> a -> CircuitM (Maybe (Buses a))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal (a
x a -> a -> a
forall a. Num a => a -> a -> a
+ a
y)
              [ZeroT(a),y]    -> sourceB y
              [Source
x,ZeroT(a)]    -> sourceB x
              [Source
x,NegateS Source
y]   -> (Prod (:>) a a :> a)
-> Source -> Source -> CircuitM (Maybe (Buses a))
forall a b c.
(SourceToBuses a, SourceToBuses b) =>
((a :* b) :> c) -> Source -> Source -> CircuitM (Maybe (Buses c))
newComp2 Prod (:>) a a :> a
forall (k :: Type -> Type -> Type) a.
NumCat k a =>
k (Prod k a a) a
subC Source
x Source
y
              [NegateS Source
x,Source
y]   -> (Prod (:>) a a :> a)
-> Source -> Source -> CircuitM (Maybe (Buses a))
forall a b c.
(SourceToBuses a, SourceToBuses b) =>
((a :* b) :> c) -> Source -> Source -> CircuitM (Maybe (Buses c))
newComp2 Prod (:>) a a :> a
forall (k :: Type -> Type -> Type) a.
NumCat k a =>
k (Prod k a a) a
subC Source
y Source
x
              [Source]
_               -> CircuitM (Maybe (Buses a))
forall (f :: Type -> Type) a. Applicative f => f (Maybe a)
nothingA
  subC :: Prod (:>) a a :> a
subC    = String -> Opt a -> Prod (:>) a a :> a
forall b a. Ok (:>) b => String -> Opt b -> a :> b
primOpt     String
"-" (Opt a -> Prod (:>) a a :> a) -> Opt a -> Prod (:>) a a :> a
forall a b. (a -> b) -> a -> b
$ \ case
              [Val a
x, Val a
y]  -> a -> CircuitM (Maybe (Buses a))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal (a
x a -> a -> a
forall a. Num a => a -> a -> a
- a
y)
              [ZeroT(a),y]    -> newComp1 negateC y
              [Source
x,ZeroT(a)]    -> sourceB x
              [Source
x,NegateS Source
y]   -> (Prod (:>) a a :> a)
-> Source -> Source -> CircuitM (Maybe (Buses a))
forall a b c.
(SourceToBuses a, SourceToBuses b) =>
((a :* b) :> c) -> Source -> Source -> CircuitM (Maybe (Buses c))
newComp2 Prod (:>) a a :> a
forall (k :: Type -> Type -> Type) a.
NumCat k a =>
k (Prod k a a) a
addC Source
x Source
y
              [NegateS Source
x,Source
y]   -> (Prod (:>) a a :> a)
-> Source -> Source -> CircuitM (Maybe (Buses a))
forall a b c.
(SourceToBuses a, SourceToBuses b) =>
((a :* b) :> c) -> Source -> Source -> CircuitM (Maybe (Buses c))
newComp2 (a :> a
forall (k :: Type -> Type -> Type) a. NumCat k a => k a a
negateC (a :> a) -> (Prod (:>) a a :> a) -> Prod (:>) a a :> a
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Prod (:>) a a :> a
forall (k :: Type -> Type -> Type) a.
NumCat k a =>
k (Prod k a a) a
addC) Source
x Source
y
              [Source]
_               -> CircuitM (Maybe (Buses a))
forall (f :: Type -> Type) a. Applicative f => f (Maybe a)
nothingA
  mulC :: Prod (:>) a a :> a
mulC    = String -> Opt a -> Prod (:>) a a :> a
forall a b. Ok2 (:>) a b => String -> Opt b -> a :> b
primOptSort String
"*" (Opt a -> Prod (:>) a a :> a) -> Opt a -> Prod (:>) a a :> a
forall a b. (a -> b) -> a -> b
$ \ case
              [Val a
x, Val a
y]  -> a -> CircuitM (Maybe (Buses a))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal (a
x a -> a -> a
forall a. Num a => a -> a -> a
* a
y)
              [OneT(a),y]     -> sourceB y
              [Source
x,OneT(a)]     -> sourceB x
              [x :: Source
x@ZeroT(a),_]  -> sourceB x
              [Source
_,y :: Source
y@ZeroT(a)]  -> sourceB y
              [NegOneT(a) ,y] -> newComp1 negateC y
              [Source
x,NegOneT(a) ] -> newComp1 negateC x
              [NegateS Source
x,Source
y]   -> (Prod (:>) a a :> a)
-> Source -> Source -> CircuitM (Maybe (Buses a))
forall a b c.
(SourceToBuses a, SourceToBuses b) =>
((a :* b) :> c) -> Source -> Source -> CircuitM (Maybe (Buses c))
newComp2 (a :> a
forall (k :: Type -> Type -> Type) a. NumCat k a => k a a
negateC (a :> a) -> (Prod (:>) a a :> a) -> Prod (:>) a a :> a
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Prod (:>) a a :> a
forall (k :: Type -> Type -> Type) a.
NumCat k a =>
k (Prod k a a) a
mulC) Source
x Source
y
              [Source
x,NegateS Source
y]   -> (Prod (:>) a a :> a)
-> Source -> Source -> CircuitM (Maybe (Buses a))
forall a b c.
(SourceToBuses a, SourceToBuses b) =>
((a :* b) :> c) -> Source -> Source -> CircuitM (Maybe (Buses c))
newComp2 (a :> a
forall (k :: Type -> Type -> Type) a. NumCat k a => k a a
negateC (a :> a) -> (Prod (:>) a a :> a) -> Prod (:>) a a :> a
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Prod (:>) a a :> a
forall (k :: Type -> Type -> Type) a.
NumCat k a =>
k (Prod k a a) a
mulC) Source
x Source
y
              [Source]
_               -> CircuitM (Maybe (Buses a))
forall (f :: Type -> Type) a. Applicative f => f (Maybe a)
nothingA
  powIC :: Ok (:>) Int => Prod (:>) a Int :> a
powIC   = String -> Opt a -> Prod (:>) a Int :> a
forall b a. Ok (:>) b => String -> Opt b -> a :> b
primOpt     String
"^" (Opt a -> Prod (:>) a Int :> a) -> Opt a -> Prod (:>) a Int :> a
forall a b. (a -> b) -> a -> b
$ \ case
              [Val a
x, Val Int
y]  -> a -> CircuitM (Maybe (Buses a))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal (a
x a -> Int -> a
forall a b. (Num a, Integral b) => a -> b -> a
^ (Int
y :: Int))
              [x :: Source
x@OneT(a) ,_]  -> sourceB x
              [Source
x,   OneT(a)]  -> sourceB x
              [x :: Source
x@ZeroT(a),_]  -> sourceB x
              [Source
_,  ZeroT(a)]  -> newVal (fromInteger 1)
              [Source]
_               -> CircuitM (Maybe (Buses a))
forall (f :: Type -> Type) a. Applicative f => f (Maybe a)
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 :: Prod (:>) a a :> a
divC = String -> Opt a -> Prod (:>) a a :> a
forall b a. Ok (:>) b => String -> Opt b -> a :> b
primOpt String
"div" (Opt a -> Prod (:>) a a :> a) -> Opt a -> Prod (:>) a a :> a
forall a b. (a -> b) -> a -> b
$ \case
              [Val a
x, Val a
y] -> a -> CircuitM (Maybe (Buses a))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal (a
x a -> a -> a
forall a. Integral a => a -> a -> a
`div` a
y)
              [Source
x,OneT(a)]    -> sourceB x
              [x :: Source
x@ZeroT(a),_] -> sourceB x
              [Source]
_              -> CircuitM (Maybe (Buses a))
forall (f :: Type -> Type) a. Applicative f => f (Maybe a)
nothingA
  modC :: Prod (:>) a a :> a
modC = String -> Opt a -> Prod (:>) a a :> a
forall b a. Ok (:>) b => String -> Opt b -> a :> b
primOpt String
"mod" (Opt a -> Prod (:>) a a :> a) -> Opt a -> Prod (:>) a a :> a
forall a b. (a -> b) -> a -> b
$ \case
              [Val a
x, Val a
y] -> a -> CircuitM (Maybe (Buses a))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal (a
x a -> a -> a
forall a. Integral a => a -> a -> a
`mod` a
y)
              [Source
_,OneT(a)]    -> newVal 0
              [x :: Source
x@ZeroT(a),_] -> sourceB x
              [Source]
_              -> CircuitM (Maybe (Buses a))
forall (f :: Type -> Type) a. Applicative f => f (Maybe a)
nothingA

instance (Fractional a, Read a, Eq a, GS a, SourceToBuses a)
      => FractionalCat (:>) a where
  recipC :: a :> a
recipC  = String -> Opt a -> a :> a
forall b a. Ok (:>) b => String -> Opt b -> a :> b
primOpt String
"recip" (Opt a -> a :> a) -> Opt a -> a :> a
forall a b. (a -> b) -> a -> b
$ \ case
              [Val a
x]        -> a -> CircuitM (Maybe (Buses a))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal (a -> a
forall a. Fractional a => a -> a
recip a
x)
              [RecipS Source
x]     -> Source -> CircuitM (Maybe (Buses a))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
x
              [NegateS Source
x]    -> (a :> a) -> Source -> CircuitM (Maybe (Buses a))
forall a b.
SourceToBuses a =>
(a :> b) -> Source -> CircuitM (Maybe (Buses b))
newComp1 (a :> a
forall (k :: Type -> Type -> Type) a. NumCat k a => k a a
negateC (a :> a) -> (a :> a) -> a :> a
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. a :> a
forall (k :: Type -> Type -> Type) a. FractionalCat k a => k a a
recipC) Source
x
              [Source]
_              -> CircuitM (Maybe (Buses a))
forall (f :: Type -> Type) a. Applicative f => f (Maybe a)
nothingA
  divideC :: Prod (:>) a a :> a
divideC = String -> Opt a -> Prod (:>) a a :> a
forall b a. Ok (:>) b => String -> Opt b -> a :> b
primOpt String
"/" (Opt a -> Prod (:>) a a :> a) -> Opt a -> Prod (:>) a a :> a
forall a b. (a -> b) -> a -> b
$ \ case
              [Val a
x, Val a
y] -> a -> CircuitM (Maybe (Buses a))
forall b. GS b => b -> CircuitM (Maybe (Buses b))
newVal (a
x a -> a -> a
forall a. Fractional a => a -> a -> a
/ a
y)
              [z :: Source
z@ZeroT(a),_] -> sourceB z
              [Source
x,OneT(a)]    -> sourceB x
              [Source
x,NegateS Source
y]  -> (Prod (:>) a a :> a)
-> Source -> Source -> CircuitM (Maybe (Buses a))
forall a b c.
(SourceToBuses a, SourceToBuses b) =>
((a :* b) :> c) -> Source -> Source -> CircuitM (Maybe (Buses c))
newComp2 (a :> a
forall (k :: Type -> Type -> Type) a. NumCat k a => k a a
negateC (a :> a) -> (Prod (:>) a a :> a) -> Prod (:>) a a :> a
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Prod (:>) a a :> a
forall (k :: Type -> Type -> Type) a.
FractionalCat k a =>
k (Prod k a a) a
divideC) Source
x Source
y
              [Source]
_              -> CircuitM (Maybe (Buses a))
forall (f :: Type -> Type) a. Applicative f => f (Maybe a)
nothingA

instance (RealFrac a, Integral b, GS a, GS b, Read a)
      => RealFracCat (:>) a b where
  floorC :: a :> b
floorC    = String -> (a -> b) -> a :> b
forall a b.
(Ok2 (:>) a b, Read a, Show b) =>
String -> (a -> b) -> a :> b
primNoOpt1 String
"floor"   a -> b
forall b. Integral b => a -> b
forall a b. (RealFrac a, Integral b) => a -> b
floor
  ceilingC :: a :> b
ceilingC  = String -> (a -> b) -> a :> b
forall a b.
(Ok2 (:>) a b, Read a, Show b) =>
String -> (a -> b) -> a :> b
primNoOpt1 String
"ceiling" a -> b
forall b. Integral b => a -> b
forall a b. (RealFrac a, Integral b) => a -> b
ceiling
  truncateC :: a :> b
truncateC = String -> (a -> b) -> a :> b
forall a b.
(Ok2 (:>) a b, Read a, Show b) =>
String -> (a -> b) -> a :> b
primNoOpt1 String
"truncate" a -> b
forall b. Integral b => a -> b
forall a b. (RealFrac a, Integral b) => a -> b
truncate

instance (Floating a, Read a, GS a) => FloatingCat (:>) a where
  expC :: a :> a
expC = String -> (a -> a) -> a :> a
forall a b.
(Ok2 (:>) a b, Read a, Show b) =>
String -> (a -> b) -> a :> b
primNoOpt1 String
"exp" a -> a
forall a. Floating a => a -> a
exp
  cosC :: a :> a
cosC = String -> (a -> a) -> a :> a
forall a b.
(Ok2 (:>) a b, Read a, Show b) =>
String -> (a -> b) -> a :> b
primNoOpt1 String
"cos" a -> a
forall a. Floating a => a -> a
cos
  sinC :: a :> a
sinC = String -> (a -> a) -> a :> a
forall a b.
(Ok2 (:>) a b, Read a, Show b) =>
String -> (a -> b) -> a :> b
primNoOpt1 String
"sin" a -> a
forall a. Floating a => a -> a
sin
  logC :: a :> a
logC = String -> (a -> a) -> a :> a
forall a b.
(Ok2 (:>) a b, Read a, Show b) =>
String -> (a -> b) -> a :> b
primNoOpt1 String
"log" a -> a
forall a. Floating a => a -> a
log
  sqrtC :: a :> a
sqrtC = String -> (a -> a) -> a :> a
forall a b.
(Ok2 (:>) a b, Read a, Show b) =>
String -> (a -> b) -> a :> b
primNoOpt1 String
"sqrt" a -> a
forall a. Floating a => a -> a
sqrt

-- TODO: optimizations, e.g., sin & cos of negative angles.

instance (Ok (:>) a, Integral a, Num b, Read a, GS b)
      => FromIntegralCat (:>) a b where
  fromIntegralC :: a :> b
fromIntegralC = String -> (a -> b) -> a :> b
forall a b.
(Ok2 (:>) a b, Read a, Show b) =>
String -> (a -> b) -> a :> b
primNoOpt1 String
"fromIntegral" a -> b
forall a b. (Integral a, Num b) => a -> b
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 :: Opt Bool
ifOptB = \ case
  [Source
c,Source
TrueS,Source
FalseS]       -> Source -> CircuitM (Maybe (Buses Bool))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
c
  [Source
c,Source
FalseS,Source
TrueS]       -> (Bool :> Bool) -> Source -> CircuitM (Maybe (Buses Bool))
forall a b.
SourceToBuses a =>
(a :> b) -> Source -> CircuitM (Maybe (Buses b))
newComp1 Bool :> Bool
forall (k :: Type -> Type -> Type). BoolCat k => k Bool Bool
notC Source
c
  [Source
a,Source
b,Source
FalseS]           -> ((Bool :* Bool) :> Bool)
-> Source -> Source -> CircuitM (Maybe (Buses Bool))
forall a b c.
(SourceToBuses a, SourceToBuses b) =>
((a :* b) :> c) -> Source -> Source -> CircuitM (Maybe (Buses c))
newComp2 (Bool :* Bool) :> Bool
forall (k :: Type -> Type -> Type).
BoolCat k =>
k (Bool :* Bool) Bool
andC Source
a Source
b
  [Source
a,Source
FalseS,Source
b]           -> ((Bool :* Bool) :> Bool)
-> Source -> Source -> CircuitM (Maybe (Buses Bool))
forall a b c.
(SourceToBuses a, SourceToBuses b) =>
((a :* b) :> c) -> Source -> Source -> CircuitM (Maybe (Buses c))
newComp2 ((Bool :* Bool) :> Bool
forall (k :: Type -> Type -> Type).
BoolCat k =>
k (Bool :* Bool) Bool
andC ((Bool :* Bool) :> Bool)
-> ((Bool :* Bool) :> (Bool :* Bool)) -> (Bool :* Bool) :> Bool
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (Bool :> Bool) -> (Bool :* Bool) :> (Bool :* Bool)
forall (k :: Type -> Type -> Type) a c b.
(MonoidalPCat k, Ok3 k a b c) =>
k a c -> k (Prod k a b) (Prod k c b)
first Bool :> Bool
forall (k :: Type -> Type -> Type). BoolCat k => k Bool Bool
notC) Source
a Source
b -- not a && b
  [Source
a,Source
TrueS, Source
b]           -> ((Bool :* Bool) :> Bool)
-> Source -> Source -> CircuitM (Maybe (Buses Bool))
forall a b c.
(SourceToBuses a, SourceToBuses b) =>
((a :* b) :> c) -> Source -> Source -> CircuitM (Maybe (Buses c))
newComp2 (Bool :* Bool) :> Bool
forall (k :: Type -> Type -> Type).
BoolCat k =>
k (Bool :* Bool) Bool
orC  Source
a Source
b
  [Source
a,Source
b ,Source
TrueS]           -> ((Bool :* Bool) :> Bool)
-> Source -> Source -> CircuitM (Maybe (Buses Bool))
forall a b c.
(SourceToBuses a, SourceToBuses b) =>
((a :* b) :> c) -> Source -> Source -> CircuitM (Maybe (Buses c))
newComp2 ((Bool :* Bool) :> Bool
forall (k :: Type -> Type -> Type).
BoolCat k =>
k (Bool :* Bool) Bool
orC  ((Bool :* Bool) :> Bool)
-> ((Bool :* Bool) :> (Bool :* Bool)) -> (Bool :* Bool) :> Bool
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (Bool :> Bool) -> (Bool :* Bool) :> (Bool :* Bool)
forall (k :: Type -> Type -> Type) a c b.
(MonoidalPCat k, Ok3 k a b c) =>
k a c -> k (Prod k a b) (Prod k c b)
first Bool :> Bool
forall (k :: Type -> Type -> Type). BoolCat k => k Bool Bool
notC) Source
a Source
b -- not a || b
  [Source
c,NotS Source
a,Eql(a)]      -> newComp2 xorC c a
  [Source
c,Source
a,b :: Source
b@(NotS(Eql(a)))] -> newComp2 xorC c b
  [Source
b,Source
c `XorS` Source
a,Eql(a)]  -> newComp3L (xorC . first andC) b c a -- (b && c) `xor` a
  [Source
b,Source
a `XorS` Source
c,Eql(a)]  -> newComp3L (xorC . first andC) b c a -- ''
  [Source]
_                      -> CircuitM (Maybe (Buses Bool))
forall (f :: Type -> Type) a. Applicative f => f (Maybe a)
nothingA

#if !defined NoIfBotOpt
pattern BottomS :: Source
pattern $mBottomS :: forall {r}. Source -> ((# #) -> r) -> ((# #) -> r) -> r
BottomS <- ConstS "undefined"
#endif

ifOpt :: (IfCat (:>) a, SourceToBuses a) => Opt a
ifOpt :: forall a. (IfCat (:>) a, SourceToBuses a) => Opt a
ifOpt = \ case
  [Source
FalseS,Source
_,Source
a]  -> Source -> CircuitM (Maybe (Buses a))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
a
  [ Source
TrueS,Source
b,Source
_]  -> Source -> CircuitM (Maybe (Buses a))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
b
  [NotS Source
a,Source
b,Source
c]  -> ((Bool :* (a :* a)) :> a)
-> Source -> Source -> Source -> CircuitM (Maybe (Buses a))
forall a b c d.
(SourceToBuses a, SourceToBuses b, SourceToBuses c) =>
((a :* (b :* c)) :> d)
-> Source -> Source -> Source -> CircuitM (Maybe (Buses d))
newComp3R (Bool :* (a :* a)) :> a
forall (k :: Type -> Type -> Type) a.
IfCat k a =>
k (Prod k Bool (Prod k a a)) a
ifC Source
a Source
c Source
b
  [Source
_,Source
a,Eql(a)]  -> sourceB a
#if !defined NoIfBotOpt
  [Source
_,Source
b,Source
BottomS] -> Source -> CircuitM (Maybe (Buses a))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
b
  [Source
_,Source
BottomS,Source
c] -> Source -> CircuitM (Maybe (Buses a))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
c
#endif
  [Source]
_             -> CircuitM (Maybe (Buses a))
forall (f :: Type -> Type) a. Applicative f => f (Maybe a)
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 $mZeroS :: forall {r}. Source -> ((# #) -> r) -> ((# #) -> r) -> r
ZeroS <- ConstS "0"

pattern OneS :: Source
pattern $mOneS :: forall {r}. Source -> ((# #) -> r) -> ((# #) -> r) -> r
OneS <- ConstS "1"

-- (if c then 1 else 0) = boolToInt c
-- (if c then 0 else 1) = boolToInt (not c)
ifOptI :: Opt Int
ifOptI = \ case
  -- [c,OneS,ZeroS] -> newComp1 boolToIntC c
  -- [c,ZeroS,OneS] -> newComp1 (boolToIntC . notC) c
  [Source]
_              -> StateT (Int, CompInfo) Identity (Maybe (Buses Int))
forall (f :: Type -> Type) a. Applicative f => f (Maybe a)
nothingA
#endif

instance IfCat (:>) Bool    where ifC :: IfT (:>) Bool
ifC = String -> Opt Bool -> IfT (:>) Bool
forall b a. Ok (:>) b => String -> Opt b -> a :> b
primOpt String
"if" (Opt Bool
forall a. (IfCat (:>) a, SourceToBuses a) => Opt a
ifOpt Binop (Opt Bool)
forall b. Binop (Opt b)
`orOpt` Opt Bool
ifOptB)
instance IfCat (:>) Int     where ifC :: IfT (:>) Int
ifC = String -> Opt Int -> IfT (:>) Int
forall b a. Ok (:>) b => String -> Opt b -> a :> b
primOpt String
"if" (Opt Int
forall a. (IfCat (:>) a, SourceToBuses a) => Opt a
ifOpt Binop (Opt Int)
forall b. Binop (Opt b)
`orOpt` Opt Int
ifOptI)
instance IfCat (:>) Integer where ifC :: IfT (:>) Integer
ifC = String -> Opt Integer -> IfT (:>) Integer
forall b a. Ok (:>) b => String -> Opt b -> a :> b
primOpt String
"if" Opt Integer
forall a. (IfCat (:>) a, SourceToBuses a) => Opt a
ifOpt
instance IfCat (:>) Float   where ifC :: IfT (:>) Float
ifC = String -> Opt Float -> IfT (:>) Float
forall b a. Ok (:>) b => String -> Opt b -> a :> b
primOpt String
"if" Opt Float
forall a. (IfCat (:>) a, SourceToBuses a) => Opt a
ifOpt
instance IfCat (:>) Double  where ifC :: IfT (:>) Double
ifC = String -> Opt Double -> IfT (:>) Double
forall b a. Ok (:>) b => String -> Opt b -> a :> b
primOpt String
"if" Opt Double
forall a. (IfCat (:>) a, SourceToBuses a) => Opt a
ifOpt

instance KnownNat n => IfCat (:>) (Finite n) where ifC :: IfT (:>) (Finite n)
ifC = String -> Opt (Finite n) -> IfT (:>) (Finite n)
forall b a. Ok (:>) b => String -> Opt b -> a :> b
primOpt String
"if" Opt (Finite n)
forall a. (IfCat (:>) a, SourceToBuses a) => Opt a
ifOpt
-- TODO: refactor

-- TODO: Would we rather zip the conditional over the vector?
instance (GenBuses b, KnownNat n) => IfCat (:>) (Vector n b) where
  ifC :: IfT (:>) (Vector n b)
ifC = String -> Opt (Vector n b) -> IfT (:>) (Vector n b)
forall b a. Ok (:>) b => String -> Opt b -> a :> b
primOpt String
"if" Opt (Vector n b)
forall a. (IfCat (:>) a, SourceToBuses a) => Opt a
ifOpt

instance IfCat (:>) () where ifC :: IfT (:>) ()
ifC = IfT (:>) ()
forall (k :: Type -> Type -> Type).
(TerminalCat k, BoolCat k) =>
IfT k ()
unitIf

instance (IfCat (:>) a, IfCat (:>) b) => IfCat (:>) (a :* b) where
  ifC :: IfT (:>) (a :* b)
ifC = IfT (:>) (a :* b)
forall (k :: Type -> Type -> Type) a b.
(MonoidalPCat k, IfCat k a, IfCat k b) =>
IfT k (a :* b)
prodIf

pattern UnsafeFiniteS :: Source -> Source
pattern $mUnsafeFiniteS :: forall {r}. Source -> (Source -> r) -> ((# #) -> r) -> r
UnsafeFiniteS a <- PSource _ "unsafeFinite" [a]

instance FiniteCat (:>) where
  unsafeFinite :: forall (n :: Nat). KnownNat n => Int :> Finite n
unsafeFinite = String -> Int :> Finite n
forall b a. Ok (:>) b => String -> a :> b
namedC String
"unsafeFinite"
  -- unFinite     = namedC "unFinite"
  unFinite :: forall n. KnownNat n => Finite n :> Int
  unFinite :: forall (n :: Nat). KnownNat n => Finite n :> Int
unFinite = String -> Opt Int -> Finite n :> Int
forall b a. Ok (:>) b => String -> Opt b -> a :> b
primOpt String
"unFinite" (Opt Int -> Finite n :> Int) -> Opt Int -> Finite n :> Int
forall a b. (a -> b) -> a -> b
$ \case
               [ValT(x,Finite n)] -> newVal (unFinite x)
               [UnsafeFiniteS Source
x]  -> Source -> StateT (Int, CompInfo) Identity (Maybe (Buses Int))
forall a. SourceToBuses a => Source -> CircuitM (Maybe (Buses a))
sourceB Source
x
               [Source]
_                  -> StateT (Int, CompInfo) Identity (Maybe (Buses Int))
forall (f :: Type -> Type) a. Applicative f => f (Maybe a)
nothingA

{--------------------------------------------------------------------
    Running
--------------------------------------------------------------------}

instance (GenBuses a, Ok2 (:>) a b) => Show (a :> b) where
  -- show = show . mkGraph -- runC
  show :: (a :> b) -> String
show = [CompS] -> String
forall a. Show a => a -> String
show ([CompS] -> String) -> ((a :> b) -> [CompS]) -> (a :> b) -> String
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (Comp -> CompS) -> Graph -> [CompS]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Comp -> CompS
simpleComp (Graph -> [CompS]) -> ((a :> b) -> Graph) -> (a :> b) -> [CompS]
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (a :> b) -> Graph
forall a b. Ok2 (:>) a b => (a :> b) -> Graph
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' :: (() :> ()) -> Int -> (Graph, Int)
runU' () :> ()
cir Int
supply = (CompInfo -> Graph
forall {k} {a}. Map k a -> [a]
getComps CompInfo
compInfo, Int
supply')
 where
   compInfo :: CompInfo
   (Int
supply',CompInfo
compInfo) = State (Int, CompInfo) (Buses ())
-> (Int, CompInfo) -> (Int, CompInfo)
forall s a. State s a -> s -> s
execState ((() :> ()) -> BCirc () ()
forall a b. (a :> b) -> BCirc a b
unmkCK () :> ()
cir Buses ()
UnitB) (Int
supply,CompInfo
forall a. Monoid a => a
mempty)
#if !defined NoHashCons
   getComps :: Map k a -> [a]
getComps = Map k a -> [a]
forall {k} {a}. Map k a -> [a]
M.elems
#else
   getComps = id
#endif

-- Wrap a circuit with fake input and output
unitize :: (GenBuses a, Ok (:>) b) => (a :> b) -> UU
unitize :: forall a b. (GenBuses a, Ok (:>) b) => (a :> b) -> () :> ()
unitize = String -> b :> ()
forall b a. Ok (:>) b => String -> a :> b
namedC String
"Out" (b :> ()) -> (() :> a) -> (a :> b) -> () :> ()
forall (k :: Type -> Type -> Type) a b a' b'.
(Category k, Oks k '[a, b, a', b']) =>
k b b' -> k a' a -> k a b -> k a' b'
<~ String -> () :> a
forall b a. Ok (:>) b => String -> a :> b
namedC String
"In"

-- uuGraph :: UU -> Graph
-- uuGraph uu = fst (uuGraph' uu 0)

uuGraph' :: UU -> IdSupply -> (Graph,IdSupply)
uuGraph' :: (() :> ()) -> Int -> (Graph, Int)
uuGraph' = (() :> ()) -> Int -> (Graph, Int)
runU'  -- for now

mkGraph :: Ok2 (:>) a b => (a :> b) -> Graph

-- mkGraph g = sort $ trimGraph $ fst (mkGraph' g 0)

mkGraph :: forall a b. Ok2 (:>) a b => (a :> b) -> Graph
mkGraph a :> b
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))) $
            Unop Graph
forall a. Ord a => [a] -> [a]
sort Unop Graph -> Unop Graph
forall a b. (a -> b) -> a -> b
$ Unop Graph
trimGraph Unop Graph -> Unop Graph
forall a b. (a -> b) -> a -> b
$ (Graph, Int) -> Graph
forall a b. (a, b) -> a
fst ((a :> b) -> Int -> (Graph, Int)
forall a b. Ok2 (:>) a b => (a :> b) -> Int -> (Graph, Int)
mkGraph' a :> b
g Int
0)

mkGraph' :: Ok2 (:>) a b => (a :> b) -> IdSupply -> (Graph,IdSupply)
mkGraph' :: forall a b. Ok2 (:>) a b => (a :> b) -> Int -> (Graph, Int)
mkGraph' a :> b
g Int
n = (() :> ()) -> Int -> (Graph, Int)
uuGraph' ((a :> b) -> () :> ()
forall a b. (GenBuses a, Ok (:>) b) => (a :> b) -> () :> ()
unitize a :> b
g) Int
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 :: String -> IO ()
systemSuccess String
cmd =
  do ExitCode
status <- String -> IO ExitCode
system String
cmd
     case ExitCode
status of
       ExitCode
ExitSuccess -> () -> IO ()
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
       ExitCode
_ -> String -> IO ()
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"command \"%s\" failed." String
cmd)


type Attr = (String,String)

-- Some options:
--
-- ("pdf","")
-- ("svg","")
-- ("png","-Gdpi=200")
-- ("jpg","-Gdpi=200")

renameC :: Unop String
renameC :: String -> String
renameC = String -> String
forall (k :: Type -> Type -> Type) a. (Category k, Ok k a) => k a a
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 :: String
outDir = String
"out"

outFile :: String -> String -> String
outFile :: String -> String -> String
outFile String
name String
suff = String
outDirString -> String -> String
forall a. [a] -> [a] -> [a]
++String
"/"String -> String -> String
forall a. [a] -> [a] -> [a]
++String
nameString -> String -> String
forall a. [a] -> [a] -> [a]
++String
"."String -> String -> String
forall a. [a] -> [a] -> [a]
++String
suff

writeDot :: String -> [Attr] -> Graph -> IO ()
writeDot :: String -> [Attr] -> Graph -> IO ()
writeDot (String -> String
renameC -> String
name) [Attr]
attrs Graph
g =
  do Bool -> String -> IO ()
createDirectoryIfMissing Bool
False String
outDir
     String -> String -> IO ()
writeFile (String -> String -> String
outFile String
name String
"dot")
       (String -> [Attr] -> Graph -> String
graphDot String
name [Attr]
attrs Graph
g {- ++"// "++ report -})
     String -> IO ()
putStrLn (String
"Wrote " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name)
     -- putStr report

displayDot :: (String,String) -> String -> IO ()
displayDot :: Attr -> String -> IO ()
displayDot (String
outType,String
res) (String -> String
renameC -> String
name) =
  do String -> IO ()
putStrLn String
dotCommand
     String -> IO ()
systemSuccess String
dotCommand
     -- printf "Wrote %s\n" picFile
     String -> IO ()
systemSuccess (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s %s" String
open String
picFile
 where
   dotCommand :: String
dotCommand = String -> String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"dot %s -T%s %s -o %s" String
res String
outType String
dotFile String
picFile
   dotFile :: String
dotFile = String -> String -> String
outFile String
name String
"dot"
   picFile :: String
picFile = String -> String -> String
outFile String
name String
outType
   open :: String
open = case String
SI.os of
            String
"darwin" -> String
"open"
            String
"linux"  -> String
"display" -- was "xdg-open"
            String
_        -> String -> String
forall a. HasCallStack => String -> a
error String
"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 :: Unop Graph
trimGraph Graph
g = Unop Graph
go Graph
g
 where
   isUsed :: Int -> Bool
isUsed = (Int -> Set Int -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Graph -> Set Int
usedComps Graph
g)
   go :: Unop Graph
go = Unop Comp -> Unop Graph
forall a b. (a -> b) -> [a] -> [b]
map (Unop Graph -> Unop Comp
onCompSubgraph Unop Graph
go) Unop Graph -> Unop Graph -> Unop Graph
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (Comp -> Bool) -> Unop Graph
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> Bool
isUsed (Int -> Bool) -> (Comp -> Int) -> Comp -> Bool
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Comp -> Int
compId)

usedComps :: Graph -> S.Set CompId
usedComps :: Graph -> Set Int
usedComps Graph
g = (Int -> [Int]) -> [Int] -> Set Int
forall a. Ord a => (a -> [a]) -> [a] -> Set a
transitiveClosure (Graph -> Int -> [Int]
compUses Graph
g) [Graph -> Int
outId Graph
g]

compUses :: Graph -> CompId -> [CompId]
compUses :: Graph -> Int -> [Int]
compUses Graph
g = -- trace (printf "compUses: gmap == %s" (show gmap))
             Map Int [Int] -> Int -> [Int]
forall k a. Ord k => Map k a -> k -> a
(M.!) (Comp -> [Int]
preds (Comp -> [Int]) -> Map Int Comp -> Map Int [Int]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Int Comp
gmap)
  where
    gmap :: Map Int Comp
gmap = Graph -> Map Int Comp
graphMap Graph
g
    preds :: Comp -> [Int]
preds (Comp Int
_ Template a b
templ (Buses a -> [Bus]
forall c. Buses c -> [Bus]
flatB -> [Bus]
ins) Buses b
_) =
      [Int
c | Bus Int
c Int
_ Ty
_ <- [Bus]
ins] [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++
      case Template a b
templ of Prim String
_ -> []
                    Subgraph Graph
g' BCirc a b
_ -> [Graph -> Int
outId Graph
g']

graphMap :: Graph -> Map Id Comp
graphMap :: Graph -> Map Int Comp
graphMap Graph
comps =
     [(Int, Comp)] -> Map Int Comp
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Comp -> Int
compId Comp
c,Comp
c) | Comp
c <- Graph
comps]
  Map Int Comp -> Map Int Comp -> Map Int Comp
forall a. Semigroup a => a -> a -> a
<> [Map Int Comp] -> Map Int Comp
forall (f :: Type -> Type) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
M.unions (Graph -> Map Int Comp
graphMap (Graph -> Map Int Comp) -> [Graph] -> [Map Int Comp]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Graph
g | Comp Int
_ (Subgraph Graph
g BCirc a b
_) Buses a
_ Buses b
_ <- Graph
comps])

transitiveClosure :: forall a. ({- Show a, -} Ord a) => (a -> [a]) -> [a] -> S.Set a
transitiveClosure :: forall a. Ord a => (a -> [a]) -> [a] -> Set a
transitiveClosure a -> [a]
nexts = Set a -> [a] -> Set a
go Set a
forall a. Monoid a => a
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 :: Set a -> [a] -> Set a
go Set a
seen     [] = Set a
seen
   go Set a
seen (a
a:[a]
as) | a
a a -> Set a -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set a
seen = Set a -> [a] -> Set a
go Set a
seen [a]
as
                  | Bool
otherwise         = Set a -> [a] -> Set a
go (a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
S.insert a
a Set a
seen) (a -> [a]
nexts a
a [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
as)

graphDot :: String -> [Attr] -> Graph -> Dot
graphDot :: String -> [Attr] -> Graph -> String
graphDot String
name [Attr]
attrs Graph
comps =
  String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"digraph %s {\n%s}\n" (Char -> Char
tweak (Char -> Char) -> String -> String
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> String
name)
         ([String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String
indent ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$
          (  [String]
prelude
          [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ Graph -> [String]
recordDots Graph
comps
          -- ++ concatMap subgraphDot (M.toList subgraphs)
          ))
 where
   prelude :: [String]
prelude = [ String
"margin=0"
             , String
"compound=true"
             , String
"rankdir=LR"
             , String
"node [shape=Mrecord]"
             , String
"edge [fontsize=8,fontcolor=indigo]"
             , String
"bgcolor=transparent"
             , String
"nslimit=20"  -- helps with very large rank graphs
             -- , "ratio=1"
             -- , "ranksep=1.0"
             -- , fixedsize=true
             ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
v | (String
a,String
v) <- [Attr]
attrs]
   tweak :: Char -> Char
tweak Char
'-' = Char
'_'
   tweak Char
c   = Char
c

indent :: Unop String
indent :: String -> String
indent = (String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++)

subgraphDot :: CompId -> Graph -> [Statement]
subgraphDot :: Int -> Graph -> [String]
subgraphDot Int
nc Graph
comps =
     [String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"subgraph cluster_%d {" Int
nc]
  [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String
indent ([String]
prelude [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ Graph -> [String]
recordDots Graph
comps)
  [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"}"]
 where
   prelude :: [String]
prelude = [ String
"margin=8" , String
"fontsize=20", String
"labeljust=r", String
"color=DarkGreen" ]

-- TODO: refactor graphDot & subgraphDot

type Statement = String

data CompS = CompS CompId PrimName [Input] [Output] deriving Int -> CompS -> String -> String
[CompS] -> String -> String
CompS -> String
(Int -> CompS -> String -> String)
-> (CompS -> String) -> ([CompS] -> String -> String) -> Show CompS
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> CompS -> String -> String
showsPrec :: Int -> CompS -> String -> String
$cshow :: CompS -> String
show :: CompS -> String
$cshowList :: [CompS] -> String -> String
showList :: [CompS] -> String -> String
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 -> CompS
simpleComp (Comp Int
n Template a b
prim Buses a
a Buses b
b) = Int -> String -> [Bus] -> [Bus] -> CompS
CompS Int
n (Template a b -> String
forall a. Show a => a -> String
show Template a b
prim) (Buses a -> [Bus]
forall c. Buses c -> [Bus]
flatB Buses a
a) (Buses b -> [Bus]
forall c. Buses c -> [Bus]
flatB Buses b
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 :: forall c. Buses c -> [Bus]
flatB = (Source -> Bus) -> [Source] -> [Bus]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Source -> Bus
sourceBus ([Source] -> [Bus]) -> (Buses c -> [Source]) -> Buses c -> [Bus]
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Buses c -> [Source]
forall a. Buses a -> [Source]
flattenB

data Dir = In | Out deriving Int -> Dir -> String -> String
[Dir] -> String -> String
Dir -> String
(Int -> Dir -> String -> String)
-> (Dir -> String) -> ([Dir] -> String -> String) -> Show Dir
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Dir -> String -> String
showsPrec :: Int -> Dir -> String -> String
$cshow :: Dir -> String
show :: Dir -> String
$cshowList :: [Dir] -> String -> String
showList :: [Dir] -> String -> String
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 :: forall a. Int -> [a] -> [(Int, a)]
taggedFrom Int
n = [Int] -> [a] -> [(Int, a)]
forall a b. [a] -> [b] -> [(a, b)]
forall (f :: Type -> Type) a b. Zip f => f a -> f b -> f (a, b)
zip [Int
n ..]

tagged :: [a] -> [(Int,a)]
tagged :: forall a. [a] -> [(Int, a)]
tagged = Int -> [a] -> [(Int, a)]
forall a. Int -> [a] -> [(Int, a)]
taggedFrom Int
0

hideNoPorts :: Bool
hideNoPorts :: Bool
hideNoPorts = Bool
False

-- Prettier names for graph display
prettyName :: Unop String
prettyName :: String -> String
prettyName String
str = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
str (String -> Map String String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
str Map String String
prettyNames)

prettyNames :: Map String String
prettyNames :: Map String String
prettyNames = [Attr] -> Map String String
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
 [ (String
"not",String
"¬") , (String
"&&",String
"∧") , (String
"||",String
"∨") , (String
"xor",String
"⊕")
 , (String
"==",String
"≡") , (String
"/=",String
"≢")
 , (String
"<=",String
"≤") , (String
">=",String
"≥")
 , (String
"-",String
"−"), (String
"*",String
"×") , (String
"^",String
"↑") , (String
"/",String
"÷")
 , (String
"undefined",String
"⊥")
 , (String
"boolToInt", String
"Bool→Int")
 , (String
"arrAt",String
"!")
 ]

outId :: Graph -> CompId
outId :: Graph -> Int
outId ((Comp -> Bool) -> Unop Graph
forall a. (a -> Bool) -> [a] -> [a]
filter Comp -> Bool
isOut -> [Comp Int
cid Template a b
_ Buses a
_ Buses b
_]) = Int
cid
outId Graph
g = String -> Int
forall a. HasCallStack => String -> a
error (String
"outId: no Out found in graph: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Graph -> String
forall a. Show a => a -> String
show Graph
g)

isOut :: Comp -> Bool
isOut :: Comp -> Bool
isOut (Comp Int
_ (Prim String
"Out") Buses a
_ Buses b
_) = Bool
True
isOut Comp
_                         = Bool
False

recordDots :: [Comp] -> [Statement]
recordDots :: Graph -> [String]
recordDots Graph
comps = [String]
nodes [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
edges
 where
   nodes :: [String]
nodes = (Comp -> [String]) -> Graph -> [String]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap Comp -> [String]
node Graph
comps
    where
      node :: Comp -> [Statement]
      node :: Comp -> [String]
node (Comp Int
nc (Subgraph Graph
g BCirc a b
_) Buses a
UnitB (PrimB Source
_)) = Int -> Graph -> [String]
subgraphDot Int
nc Graph
g
      node (Comp -> CompS
simpleComp -> CompS Int
nc (String -> String
prettyName -> String
prim) [Bus]
ins [Bus]
outs) =
        [String
prefix String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
mbCluster
         (String -> String -> String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s [label=\"{%s%s%s}\"%s]"
           (Int -> String
compLab Int
nc)
           (String -> String -> String -> String
forall {t} {t}.
(PrintfArg t, PrintfArg t) =>
t -> String -> t -> String
ports String
"" (Dir -> [Bus] -> String
labs Dir
In [Bus]
ins) String
"|")
           (String -> String
escape String
prim)
           (String -> String -> String -> String
forall {t} {t}.
(PrintfArg t, PrintfArg t) =>
t -> String -> t -> String
ports String
"|" (Dir -> [Bus] -> String
labs Dir
Out [Bus]
outs) String
"")
           String
extras)]
       where
         isSubgraph :: Template a b -> Bool
isSubgraph (Subgraph {}) = Bool
True
         isSubgraph Template a b
_ = Bool
False
         wrapNodes :: Bool
wrapNodes = (Comp -> Bool) -> Graph -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
any (\ (Comp Int
_ Template a b
p Buses a
_ Buses b
_) -> Template a b -> Bool
forall {a} {b}. Template a b -> Bool
isSubgraph Template a b
p) Graph
comps
         mbCluster :: Unop String
         mbCluster :: String -> String
mbCluster | Bool
wrapNodes =
           String -> Int -> String -> String
forall r. PrintfType r => String -> r
printf String
"subgraph clusterc%d { label=\"\"; color=white; margin=0; %s }" Int
nc
                   | Bool
otherwise = String -> String
forall (k :: Type -> Type -> Type) a. (Category k, Ok k a) => k a a
id
         extras :: String
extras | String
prim String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
unknownName = String
",fontcolor=red,color=red,style=bold"
                | Bool
otherwise = String
""
         prefix :: String
prefix =
           if Bool
hideNoPorts Bool -> Bool -> Bool
&& [Bus] -> Bool
forall a. [a] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [Bus]
ins Bool -> Bool -> Bool
&& [Bus] -> Bool
forall a. [a] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [Bus]
outs then String
"// " else String
""
         ports :: t -> String -> t -> String
ports t
_ String
"" t
_ = String
""
         ports t
l String
s t
r = String -> t -> String -> t -> String
forall r. PrintfType r => String -> r
printf String
"%s{%s}%s" t
l String
s t
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 -> [Bus] -> String
labs Dir
dir [Bus]
bs = String -> String
segmentedDotString (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$
                       String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"|" ((Int, Bus) -> String
portSticker ((Int, Bus) -> String) -> [(Int, Bus)] -> [String]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Bus] -> [(Int, Bus)]
forall a. [a] -> [(Int, a)]
tagged [Bus]
bs)
          where
            portSticker :: (Int,Bus) -> String
            portSticker :: (Int, Bus) -> String
portSticker (Int
p,Bus
_) = String -> String
bracket (Dir -> Int -> String
portLab Dir
dir Int
p)
         -- Escape angle brackets, "|", and other non-ascii
         escape :: Unop String
         escape :: String -> String
escape [] = []
         escape (Char
c:String
cs) = String -> String
mbEsc (Char
c Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
escape String
cs)
          where
             mbEsc :: String -> String
mbEsc | (Char
c Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`elem` String
"<>|{}") Bool -> Bool -> Bool
|| Bool -> Bool
not (Char -> Bool
isAscii Char
c)  = (Char
'\\' Char -> String -> String
forall a. a -> [a] -> [a]
:)
                   | Bool
otherwise     = String -> String
forall (k :: Type -> Type -> Type) a. (Category k, Ok k a) => k a a
id
      -- node comp = error ("recordDots/node: unexpected comp " ++ show comp)
   bracket :: String -> String
bracket = (String
"<"String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (String -> String) -> String -> String
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (String -> String -> String
forall a. [a] -> [a] -> [a]
++String
">")
   edges :: [String]
edges = (Comp -> [String]) -> Graph -> [String]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap Comp -> [String]
forall {b}. PrintfType b => Comp -> [b]
compEdges Graph
comps
    where
      compEdges :: Comp -> [b]
compEdges _c :: Comp
_c@(Comp Int
cnum Template a b
_ Buses a
a Buses b
_) = (Int, Source) -> b
edge ((Int, Source) -> b) -> [(Int, Source)] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Source] -> [(Int, Source)]
forall a. [a] -> [(Int, a)]
tagged (Buses a -> [Source]
forall a. Buses a -> [Source]
flattenB Buses a
a)
       where
         edge :: (Int, Source) -> b
edge (Int
ni, Source (Bus Int
ocnum Int
opnum Ty
t) Template a b
templ [Source]
_) =
           String -> String -> String -> String -> b
forall r. PrintfType r => String -> r
printf String
"%s -> %s [%s]"
             (String -> (Int -> String) -> Maybe Int -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Dir -> (Int, Int) -> String
port Dir
Out (Int
ocnum,Int
opnum)) Int -> String
compLab Maybe Int
mbSubOut)
             (Dir -> (Int, Int) -> String
port Dir
In (Int
cnum,Int
ni))
             (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," [String]
attrs)
          where
            mbSubOut :: Maybe CompId  -- Output component if a subgraph
            mbSubOut :: Maybe Int
mbSubOut = case Template a b
templ of Prim String
_       -> Maybe Int
forall a. Maybe a
Nothing
                                     Subgraph Graph
g BCirc a b
_ -> Int -> Maybe Int
forall a. a -> Maybe a
Just (Graph -> Int
outId Graph
g)
            attrs :: [String]
attrs = (if Maybe Int -> Bool
forall a. Maybe a -> Bool
isJust Maybe Int
mbSubOut then [String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"ltail=cluster_%d" Int
ocnum] else []) [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
                    [String]
label [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
forall a. [a]
constraint
#ifdef ShallowDelay
            constraint | isDelay _c = ["constraint=false" ]
                       | otherwise  = []
#else
            constraint :: [a]
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 :: [String]
label = [String -> String -> String
forall r. PrintfType r => String -> r
printf String
"label=\"%s\"" (Ty -> String
forall a. Show a => a -> String
show Ty
t)]
#endif
   port :: Dir -> (CompId,PortNum) -> String
   port :: Dir -> (Int, Int) -> String
port Dir
dir (Int
cnum,Int
np) =
     String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s:%s" (Int -> String
compLab Int
cnum) (Dir -> Int -> String
portLab Dir
dir Int
np)
   compLab :: CompId -> String
   compLab :: Int -> String
compLab Int
nc = Char
'c' Char -> String -> String
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show Int
nc
   portLab :: Dir -> PortNum -> String
   portLab :: Dir -> Int -> String
portLab Dir
dir Int
np = String -> String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"%s%d" (Dir -> String
forall a. Show a => a -> String
show Dir
dir) Int
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 :: String -> String
segmentedDotString = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\"+\"" ([String] -> String) -> (String -> [String]) -> String -> String
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. String -> [String]
divvy
 where
   divvy :: String -> [String]
divvy [] = []
   divvy (Int -> String -> Attr
forall a. Int -> [a] -> ([a], [a])
splitAt Int
yy_buf_size -> (String
pre,String
suf)) = String
pre String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String -> [String]
divvy String
suf
   yy_buf_size :: Int
yy_buf_size = Int
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' :: forall a u v.
(OkCAR a, GenBuses (Rep a)) =>
Template u v -> [Source] -> BusesM (Buses a)
genBusesRep' Template u v
templ [Source]
ins = Buses (Rep a) -> Buses a
forall a. OkCAR a => Buses (Rep a) -> Buses a
abstB (Buses (Rep a) -> Buses a)
-> StateT Int (StateT (Int, CompInfo) Identity) (Buses (Rep a))
-> StateT Int (StateT (Int, CompInfo) Identity) (Buses a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Template u v
-> [Source]
-> StateT Int (StateT (Int, CompInfo) Identity) (Buses (Rep a))
forall a u v.
GenBuses a =>
Template u v -> [Source] -> BusesM (Buses a)
forall u v.
Template u v
-> [Source]
-> StateT Int (StateT (Int, CompInfo) Identity) (Buses (Rep a))
genBuses' Template u v
templ [Source]
ins

-- tweakValRep :: (HasRep a, Tweakable (Rep a)) => Unop a
-- tweakValRep = abst . tweakVal . repr

tyRep :: forall a. GenBuses (Rep a) => Ty
tyRep :: forall a. GenBuses (Rep a) => Ty
tyRep = forall a. GenBuses a => Ty
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' :: forall a.
(GenBuses a, GenBuses (Rep a)) =>
State [Source] (Buses a)
genUnflattenB' = Buses (Rep a) -> Buses a
forall a. OkCAR a => Buses (Rep a) -> Buses a
abstB (Buses (Rep a) -> Buses a)
-> StateT [Source] Identity (Buses (Rep a))
-> StateT [Source] Identity (Buses a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT [Source] Identity (Buses (Rep a))
forall a. GenBuses a => State [Source] (Buses a)
unflattenB'

-- Omit temporarily for faster compilation
#if 1

#include "ConCat/AbsTy.inc"

instance GenBuses (Proxy a) where
  genBuses' :: forall u v. Template u v -> [Source] -> BusesM (Buses (Proxy a))
genBuses' = Template u v -> [Source] -> BusesM (Buses (Proxy a))
forall a u v.
(OkCAR a, GenBuses (Rep a)) =>
Template u v -> [Source] -> BusesM (Buses a)
genBusesRep'
  ty :: Ty
ty = forall a. GenBuses (Rep a) => Ty
tyRep @(Proxy a)
  unflattenB' :: State [Source] (Buses (Proxy a))
unflattenB' = State [Source] (Buses (Proxy a))
forall a.
(GenBuses a, GenBuses (Rep a)) =>
State [Source] (Buses a)
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