module Synthesize(aSynthesize) where

import Data.List(transpose, sort, genericLength, nub)
import Control.Monad.State
import Debug.Trace
import qualified Data.Map as M

import Util(integerToBits, makePairs, log2, itos)
import PPrint
import IntLit
import ErrorUtil
import Flags(Flags, synthesize)
import Position(noPosition)
import FStringCompat(mkFString)
import Id
import Prim
import Pragma(DefProp, defPropsHasNoCSE)
import ASyntax
import ASyntaxUtil(tsortADefs, aType, isConst, aSize, )
import AExpand(aSRemoveUnused)
import AOpt(aOptBoolExpr)
import IOUtil(progArgs)

doTrace :: Bool
doTrace = elem "-trace-syn" progArgs

-- ---------------
-- Naming conventions

synthPref :: String
synthPref = "_dw"

-- ---------------

aSynthesize :: Flags -> ASPackage -> ASPackage
aSynthesize flags p@(ASPackage { aspkg_values = ds }) =
    if not (synthesize flags) then
        p
    else
        -- XXX use some fast removal of unused defs & renamings.
        aImprove (p { aspkg_values = synDefs ds })

-- ---------------

-- Improve by iterating the following steps:
--   remove unused definitions
--   inline variables and constants
--   propagate constants
-- XXX - assuming foreign function calls need not be touched because state variable instantiations are not touched
aImprove :: ASPackage -> ASPackage
aImprove p@(ASPackage { aspkg_values = ds }) =
    let inline :: M.Map AId AExpr
        inline = M.fromList [ (i, e) | ADef i _ e _ <- ds, isSimple e ]
        repl :: AExpr -> AExpr
        repl e@(ASDef _ i) =
                case M.lookup i inline of
                Just e' -> e'
                Nothing -> e
        repl (APrim aid t p es) = APrim aid t p (map repl es)
        repl (ANoInlineFunCall t i f es) = ANoInlineFunCall t i f (map repl es)
        repl (AFunCall t i f isC es) = AFunCall t i f isC (map repl es)
--        repl e = internalError ("aImprove.replE " ++ ppReadable e)
        repl e = e
        -- aOptBoolExpr is overkill...
        ds' = [ ADef i t (aOptBoolExpr (repl e)) p | ADef i t e p <- ds ]
        p'' = aSRemoveUnused False (p { aspkg_values = ds' })
        ds'' = aspkg_values p''
    in  if length ds == length ds'' && ds == ds'' then        -- length check is a fast check for inequality
            (if doTrace then trace "aImprove done" else id)
            p
        else
            (if doTrace then trace ("aImprove iterates, " ++ show (length ds, length ds'')) else id) $
--          trace (ppReadable p'') $
            aImprove p''

--------

data SState = SState {
                -- unique name generator
                uniqueId :: Integer,
                -- definitions processed so far
                -- at the end, these become the defs of the resulting module
                defs :: [(AId, AExpr, [DefProp])],
                -- reverse lookup of defs processed or added so far,
                -- to avoid creating new Ids for exprs which already had Ids
                -- (defs marked NoCSE are not added to this map)
                cse_map :: (M.Map AExpr AId),
                -- map of defs which have been deemed "simple"
                -- (references to these can be inlined with the expression)
                simple_map :: (M.Map AId AExpr)
              }

type S a = State SState a

addDef :: AId -> AExpr -> [DefProp] -> S ()
addDef v e props = do
  state <- get
  ds <- gets defs
  cmap <- gets cse_map
  smap <- gets simple_map
  let ds' = ((v,e,props):ds)
      cmap' = if (defPropsHasNoCSE props)
              then cmap
              else M.insert e v cmap
      smap' = case isSimple e of
                True -> M.insert v e smap
                _ -> smap
  put $ state { defs = ds', cse_map = cmap', simple_map = smap' }

getSimple :: AId -> AExpr -> S AExpr
getSimple v e = do
  smap <- gets simple_map
  return $ M.findWithDefault e v smap

findExpr :: AExpr -> S (Maybe AId)
findExpr e = do
  cmap <- gets cse_map
  return $ M.lookup e cmap

getDefs :: S [(AId, AExpr, [DefProp])]
getDefs = do
  state <- get
  ds <- gets defs
  put $ state { defs = [], cse_map = M.empty }
  return $ reverse ds

newName :: S AId
newName = do
  state <- get
  i <- gets uniqueId
  put $ state { uniqueId = (i+1) }
  return $ mkId noPosition (mkFString ("_ds" ++ itos i))

--------

synDefs :: [ADef] -> [ADef]
synDefs ds =
    let initState = SState { uniqueId = 1,
                             defs = [],
                             cse_map = M.empty,
                             simple_map = M.empty
                           }
    in  fst $ runState (synDefsS (tsortADefs ds)) initState

synDefsS :: [ADef] -> S [ADef]
synDefsS ds = do
    mapM_ toED ds
    ies <- getDefs
    mapM_ synDef ies
    ies' <- getDefs
    when doTrace $ trace ("synDefsS done") $ return ()
    return [ ADef i (aType e) (e) p | (i, e, p) <- ies' ]

toED :: ADef -> S ()
toED (ADef i t e props) = do
    e' <- toE e
    addDefU i e' props

toE :: AExpr -> S AExpr
-- XXX bad code
toE (APrim aid t p [x,y]) | p == PrimSLE || p == PrimSLT =
        let ty@(ATBit n) = aType x
            c = ASInt defaultAId ty (ilHex (2^(n-1)))
            x' = APrim aid ty PrimXor [x, c]
            y' = APrim aid ty PrimXor [y, c]
        in  toE (APrim aid t (if p == PrimSLE then PrimULE else PrimULT) [x',y'])
-- XXX bad code
toE (APrim aid t@(ATBit n) PrimExtract [e, h, l]) | h /= l && not (isConst h && isConst l) =
        let te@(ATBit m) = aType e
            e1 | m > n     = APrim aid t PrimExtract
                                [e1f,
                                 ASInt defaultAId aTNat (ilDec (n-1)),
                                 ASInt defaultAId (aType h) (ilDec 0)]
               | n < m     = APrim aid t PrimZeroExt [e1f]
               | otherwise = e1f
            e1f = APrim aid te PrimSRL [e, l]
            e2 = APrim aid t PrimSub
                        [onesh,
                        ASInt defaultAId t (ilDec 1)]
            onesh = APrim aid t PrimSL
                        [ASInt defaultAId t (ilDec 1),
                         shft]
            shft = APrim aid (aType h) PrimAdd
                        [hml,
                         ASInt defaultAId (aType h) (ilDec 1)]
            hml = APrim aid (aType h) PrimSub [h, l]
            e' = aOptBoolExpr (APrim aid t PrimAnd [e1, e2])
        in  toE e'
toE (APrim aid t p es) = mapM toSE es >>= return . APrim aid t p
toE (ANoInlineFunCall t i f es) = mapM toSE es >>= return . ANoInlineFunCall t i f
toE (AFunCall t i f isC es) = mapM toSE es >>= return . AFunCall t i f isC
toE e = return e

toSE :: AExpr -> S AExpr
toSE (ASAny t _) = return (ASInt defaultAId t (ilDec 0))
toSE e@(ASInt {}) = return e
toSE e@(ASStr {}) = return e
toSE e@(ASDef {}) = return e
toSE e@(ASPort {}) = return e
toSE e@(ASParam {}) = return e
toSE e = do
    e' <- toE e
    i <- addExpr e'
    return (ASDef (aType e') i)

addExpr :: AExpr -> S AId
addExpr e = do
    e' <- normExpr e
    mi <- findExpr e'
    case mi of
     Just i -> return i
     Nothing -> do
        i <- newName
        addDef i e' []
        return i

addDefU :: AId -> AExpr -> [DefProp] -> S ()
addDefU i e p = do
    e' <- normExpr e
    mi <- findExpr e'
    case mi of
     Just oi -> addDef i (ASDef (aType e') oi) p
     Nothing -> addDef i e' p

-- put primops on "normal form", i.e., with sorted operands and simple id inlined
normExpr :: AExpr -> S AExpr
normExpr (APrim aid t op es) = do
    let getSimpleS e@(ASDef _ i) = getSimple i e
        getSimpleS e = return e
    es' <- mapM getSimpleS es
    return (sortExpr (aOptPrim aid t op es'))
normExpr e@(ASDef _ i) = getSimple i e
normExpr e = return e

aOptPrim :: AId -> AType -> PrimOp -> [AExpr] -> AExpr
aOptPrim aid t PrimBAnd es  = aAnds aid es
aOptPrim aid t PrimBOr  es  = aOrs  aid es
aOptPrim aid t PrimXor  es  = aXors aid es
aOptPrim aid t PrimBNot [e] = aNot aid e
aOptPrim aid t p es = APrim aid t p es

sortExpr :: AExpr -> AExpr
sortExpr (APrim aid t op es) | isGate op = APrim aid t op (sort es)
  where isGate op = op `elem` [PrimBAnd, PrimBOr, PrimXor]
sortExpr e = e

wireId :: Id -> Int -> Id
wireId i n = mkIdPre (mkFString (synthPref ++ itos n ++ "_")) i

synDef :: (AId, AExpr, [DefProp]) -> S ()
synDef (i, e, props) = do
    when doTrace $ trace ("synDef " ++ ppReadable (i, e)) $ return ()
    es <- synExp e
    case es of
     [e'] -> addDefU i e' props
     es -> do
        let is = map (wireId i) [0..length es-1]
        zipWithM_ (\i e -> addDefU i e props ) is es
--        trace (ppReadable (is, es)) $ return ()
        addDefU i (APrim i (aType e) PrimConcat (map (ASDef aTBool) (reverse is))) props

synExp :: AExpr -> S [AExpr]
synExp (APrim aid t p es) = synPrim aid t p es
synExp e@(ANoInlineFunCall t _ _ _) = do
        i <- newName
        addDef i e []
        --trace ("synExp: ANoInlineFunCall " ++ ppReadable (i, e)) $ return ()
        return (splitASDef t i)
synExp e@(AFunCall t _ _ _ _) = do
        i <- newName
        addDef i e []
        --trace ("synExp: AFunCall " ++ ppReadable (i, e)) $ return ()
        return (splitASDef t i)

-- task calls and task values do not simplify
synExp e@(ATaskValue { }) = return [ e ]
synExp v@(ASPort (ATBit 1) i) = return [ v ]
synExp (ASPort t i) = return (splitASPort t i)
-- XXX parameters don't need simplifying?
-- XXX if we didn't know "t", we wouldn't be able to split
-- synExp (ASParam t i) = return (splitASParam t i)
synExp v@(ASParam t i) = return [ v ]
--synExp (ASDef t i) = return (splitASDef t i)
synExp v@(ASDef (ATBit 1) i) = return [ v ]
synExp (ASDef (ATBit n) i) = return [ ASDef aTBool (wireId i k) | k <- [0..fromInteger n-1] ]
synExp (ASInt aid (ATBit n) (IntLit _ _ i)) = return [ ASInt aid aTBool (ilSizedBin 1 b) | b <- reverse (integerToBits n i) ]
synExp (ASStr _ _ _) = internalError "Synthesize.synExp: ASStr"
synExp (ASAny t _) = internalError "Synthesize.synExp: ASAny"
synExp _ = internalError( "Synthesize::synExp" )

synExpS :: AExpr -> S [AExpr]
synExpS e = synExp e >>= toSs

-- ---------------

splitASDef :: AType -> AId -> [AExpr]
splitASDef t i = splitVar t i (ASDef t i)

splitASPort :: AType -> AId -> [AExpr]
splitASPort t i = splitVar t i (ASPort t i)

-- Create a list of expressions returning the bits of a variable "v"
-- (the "v" can be either ASDef or ASPort, with name "i")
splitVar :: AType -> AId -> AExpr -> [AExpr]
splitVar t@(ATBit 1) i v = [v]
splitVar t@(ATBit n) i v =
    [ APrim i aTBool PrimExtract [v, aj, aj] | j <- [0..n-1], let aj = aNat j ]
splitVar _ _ _ = internalError( "Synthesize::splitVar" )

-- ---------------

isSimple :: AExpr -> Bool
isSimple (ASInt {}) = True
isSimple (ASStr {}) = True
isSimple (ASPort {}) = True
isSimple (ASParam {}) = True
isSimple (ASDef {}) = True
isSimple (ASAny {}) = True
isSimple _ = False

toS :: AExpr -> S AExpr
toS e | isSimple e = return e
        | True = do
    i <- addExpr e
    return (ASDef (aType e) i)

toS2 :: (AExpr, AExpr) -> S (AExpr, AExpr)
toS2 (x, y) = do
    x' <- toS x
    y' <- toS y
    return (x', y')

toSs :: [AExpr] -> S [AExpr]
toSs = mapM toS

isBoolOp :: PrimOp -> Bool
isBoolOp PrimBAnd = True
isBoolOp PrimBOr = True
isBoolOp PrimBNot = True
isBoolOp _ = False

isBoolVecOp :: PrimOp -> Bool
isBoolVecOp PrimAnd = True
isBoolVecOp PrimOr = True
isBoolVecOp PrimInv = True
isBoolVecOp PrimXor = True
isBoolVecOp _ = False

primToFun :: PrimOp -> AId -> [AExpr] -> AExpr
primToFun PrimAnd = aAnds
primToFun PrimOr = aOrs
primToFun PrimInv = aNots
primToFun PrimXor = aXors
primToFun p =  internalError( "Synthesize::primToFun: " ++ (show p))


shiftOf :: PrimOp -> ShiftFun
shiftOf PrimSL = permSL
shiftOf PrimSRL = permSRL
shiftOf PrimSRA = permSRA
shiftOf p =  internalError( "Synthesize::shiftOf: " ++ (show p))

synPrim :: AId -> AType -> PrimOp -> [AExpr] -> S [AExpr]
synPrim aid t p es | isBoolOp p = return [APrim aid t p es]
synPrim aid _ p es | isBoolVecOp p = do
        ess <- mapM synExpS es
        return (map ((primToFun p) aid) (transpose ess))
--        return (map (APrim _ aTBool (vecToBool p)) (transpose ess))
synPrim aid _ PrimEQ [x, y] = do
        xs <- synExpS x
        ys <- synExpS y
        rs <- toSs (zipWith (aXor aid) xs ys)
        ne <- toS (aOrs aid rs)
        return [aNot aid ne]
synPrim aid ty PrimIf [c, t, e] = do
        notc <- toS (aNot aid c)
        synPrim aid ty PrimMux [c, t, notc, e]
synPrim aid _ PrimMux pes = synMux aid (unzip (makePairs pes))
synPrim aid _ PrimPriMux pes = do
        let (ps, es) = unzip (makePairs pes)
        ps' <- synPriEnc aid [] ps >>= toSs
        synMux aid (ps', es)
synPrim aid _ PrimExtract [e, ASInt _ _ (IntLit _ _ h), ASInt _ _ (IntLit _ _ l)] = do
        es <- synExp e
        return (take (fromInteger (h-l+1)) (drop (fromInteger l) es))
synPrim aid _ PrimExtract [e, x, x'] | x==x' = do
        es <- synExpS e
        xs <- synExpS x
        let n = log2 (length es)
        cs <- synDecode aid (take n xs) >>= toSs
        as <- toSs (zipWith (aAnd aid) cs es)
        return [aOrs aid as]
synPrim aid _ PrimConcat es = do
        ess <- mapM synExp es
        return (concat (reverse ess))
synPrim aid _ PrimRange [_,_,e] = synExp e
synPrim aid (ATBit n) PrimZeroExt [e] = do
        let k = aSize e
        es <- synExp e
        return (es ++ replicate (fromInteger (n-k)) aFalse)
synPrim aid (ATBit n) PrimSignExt [e] = do
        let k = aSize e
        es <- synExp e
        let sign = last es
        return (es ++ replicate (fromInteger (n-k)) sign)
synPrim aid _ PrimCase (c:d:ces) = do
        let n = aSize c
            pown = 2^n
            arms = [ (i,e) | (ASInt _ _ (IntLit _ _ i), e) <- makePairs ces ]
            len = genericLength arms
            missing = pown - len
            ies = if missing * n < len then fill arms [0..pown-1] else arms
            fill []             []              = []
            fill ((i, e) : ces) (k:ks) | i == k = (i, e) : fill ces ks
            fill ces            (k:ks)          = (k, d) : fill ces ks
            fill _              _               = internalError( "Synthesize::synPrim::fill" )

        cs <- synExpS c
        ncs <- mapM (toS . (aNot aid)) cs
        let mkArm bs = toS (aAnds aid (zipWith3 dec1 bs ncs cs))
            dec1 0 n _ = n
            dec1 1 _ c = c
            dec1 _ _ _ = internalError "synthesize.dec1"

        ps <- mapM mkArm (map (reverse . integerToBits n . fst) ies)
        (defp, defe) <-
                if genericLength ies == pown then
                    return ([], [])
                else do
                   o <- toS (aOrs aid ps)
                   a <- toS (aNot aid o)
                   return ([a], [d])
        synMux aid (defp ++ ps, defe ++ map snd ies)
synPrim aid _ PrimAdd [x, y] = do
        xs <- synExpS x
        ys <- synExpS y
        (_, ss) <- synXAdd aid xs ys aFalse
        return ss
synPrim aid _ PrimSub [x, y] = do
        xs <- synExpS x
        ys <- synExpS y
        (_, ss) <- synXSub aid xs ys aTrue
        return ss
synPrim aid (ATBit n) PrimNeg [y] = do
        let xs = replicate (fromInteger n) aFalse
        ys <- synExpS y
        (_, ss) <- synXSub aid xs ys aTrue
        return ss
synPrim aid (ATBit n) PrimMul [x, y] = do
        xs <- synExpS x
        ys <- synExpS y
        ss <- synMul aid xs ys
        return (take (fromInteger n) ss)
synPrim aid _ PrimULT [x, y] = do
        xs <- synExpS x
        ys <- synExpS y
        (le, _) <- synXSub aid ys xs aFalse
        return [le]
synPrim aid _ PrimULE [x, y] = do
        xs <- synExpS x
        ys <- synExpS y
        (le, _) <- synXSub aid ys xs aTrue
        return [le]
synPrim aid (ATBit n) p [x, y] | p == PrimSL || p == PrimSRL || p == PrimSRA = do
        xs <- synExpS x
        ys <- synExpS y
        synShifter aid (shiftOf p) (take (log2 (length xs)) ys) xs
-- scheduler
synPrim aid t@(ATBit n) p es =
        trace ("synPrim: unimplemented " ++ ppReadable (p,t,es)) $
        return (map (const unknown) [1..n])
  where -- XXX using a fake port reference to create a reference to 'z' value
        unknown = ASPort aTBool (mkId noPosition (mkFString "z"))

synPrim aid t p es = internalError ("synPrim: not bit: " ++ ppReadable (p,t,es))

synMux :: AId -> ([AExpr], [AExpr]) -> S [AExpr]
synMux aid (ps, es) = do
        let mux1and :: AExpr -> [AExpr] -> S [AExpr]
            mux1and p es = toSs (map (aAnd aid p) es)
        ess <- mapM synExpS es
        ess' <- zipWithM mux1and ps ess
        return (map (aOrs aid) (transpose ess'))

synPriEnc :: AId -> [AExpr] -> [AExpr] -> S [AExpr]
synPriEnc aid ns [] = return []
synPriEnc aid ns (p:ps) = do
        n <- toS (aNot aid p)
        es <- synPriEnc aid (n:ns) ps
        return (aAnds aid (p:ns) : es)

-- Make a decoder with cs input bits, returns a one-hot list.
synDecode :: AId -> [AExpr] -> S [AExpr]
synDecode aid cs = do
        ncs <- mapM (toS . (aNot aid)) cs
        let n = genericLength cs
            dec bs = (aAnds aid) (zipWith3 dec1 bs ncs cs)
            dec1 0 n _ = n
            dec1 1 _ c = c
            dec1 _ _ _ = internalError "synthesize.dec1"

        return (map (dec . reverse . integerToBits n) [0..2^n-1])

--aXors xs = foldr1 aXor xs
aXors :: AId -> [AExpr] -> AExpr
aXors aid [x, y] = aXor aid x y
aXors _ _ = internalError "Synthesize.aXors: list should be of length 2"

aXor :: AId -> AExpr -> AExpr -> AExpr
aXor aid x y | isFalse x = y
             | isTrue  x = aNot aid y
             | isFalse y = x
             | isTrue  y = aNot aid x
             | x == y    = aFalse
             | otherwise = APrim aid aTBool PrimXor [x, y]

aNots :: AId -> [AExpr] -> AExpr
aNots aid [e] = aNot aid e
aNots _ _ = internalError "Synthesize.aNots"

aNot :: AId -> AExpr -> AExpr
aNot aid e | isTrue e  = aFalse
           | isFalse e = aTrue
           | otherwise = APrim aid aTBool PrimBNot [e]

aAnds :: AId -> [AExpr] -> AExpr
aAnds aid es = if any isFalse es then aFalse else aAnds' (nub (filter (not . isTrue) es))
  where aAnds' []  = aTrue
        aAnds' [e] = e
        aAnds' es  = APrim aid aTBool PrimBAnd es

aAnd :: AId -> AExpr -> AExpr -> AExpr
aAnd aid x y = aAnds aid [x, y]

aOrs :: AId -> [AExpr] -> AExpr
aOrs aid es = if any isTrue es then aTrue else aOrs' (nub (filter (not . isFalse) es))
  where aOrs' []  = aFalse
        aOrs' [e] = e
        aOrs' es  = APrim aid aTBool PrimBOr es

aOr :: AId -> AExpr -> AExpr -> AExpr
aOr aid x y = aOrs aid [x, y]

-----

fAdd :: AId -> AExpr -> AExpr -> AExpr -> S (AExpr, AExpr)
fAdd aid a b c = do
        sab <- toS (aXor aid a b)
        ab <- toS (aAnd aid a b)
        bc <- toS (aAnd aid b c)
        ca <- toS (aAnd aid c a)
        let s = aXor aid sab c
            co = aOrs aid [ab, bc, ca]
        return (co, s)

hAdd :: AId -> AExpr -> AExpr -> S (AExpr, AExpr)
hAdd aid a b = return (aAnd aid a b, aXor aid a b)

type SynArith = AId -> [AExpr] -> [AExpr] -> AExpr -> S (AExpr, [AExpr])

-- Make a ripple carry adder
synRippleAdd :: SynArith
synRippleAdd _    []     [] ci = return (ci, [])
synRippleAdd aid (x:xs) (y:ys) ci = do
                                    (c, s) <- fAdd aid x y ci
                                    c' <- toS c
                                    (co, ss) <- synRippleAdd aid xs ys c'
                                    return (co, s:ss)
synRippleAdd _ _ _ _ = internalError "Synthesize.synRippleAdd - length xs /= length ys"

-- synRippleSub = synSub synRippleAdd

-- Make a subtractor given an adder.
-- The borrow in and borrow out are complemented.
-- Implemented by negating (complement and increment via ci) second operand
-- and then adding.
synSub :: SynArith -> SynArith
synSub f aid xs ys nbi = do
        nys <- mapM (toS . (aNot aid)) ys
        f aid xs nys nbi

rippleMax :: Int
rippleMax = 8

synXAdd :: SynArith
synXAdd aid xs ys ci =
        (if length xs > rippleMax then
            synCLAAdd
         else
            synRippleAdd)
           aid xs ys ci
synXSub :: SynArith
synXSub = synSub synXAdd

--

type PG = (AExpr, AExpr)

combPG :: AId -> PG -> PG -> S PG
combPG aid (p2, g2) (p1, g1) = do
        po <- toS (aAnd aid p1 p2)
        pg <- toS (aAnd aid p1 g2)
        go <- toS (aOr aid g1 pg)
        return (po, go)

synCLAAdd :: SynArith
synCLAAdd aid xs ys ci = do
        pgs <- zipWithM (hAdd aid) xs ys >>= mapM (toS2 . swap)
        opgs <- scanM (combPG aid) ((aFalse, ci) : pgs)
        let cs = map snd opgs
            ss = map fst pgs
            co = last cs
        return (co, zipWith (aXor aid) ss (init cs))
---

nShiftMux :: Int
nShiftMux = 2

nShiftMuxPow :: Int
nShiftMuxPow = 2^nShiftMux

-- Synthesize a barrel shifter
-- Use one mux layer for every nShiftMux control bits.
synShifter :: AId -> ShiftFun -> [AExpr] -> [AExpr] -> S [AExpr]
synShifter aid shft [] xs = return xs
synShifter aid shft cs xs = do
        let (csn, csr) = splitAt nShiftMux cs
        inp' <- synShifter aid (shft . (* nShiftMuxPow)) csr xs >>= toSs
        shiftLayer aid shft csn inp'

shiftLayer :: AId -> ShiftFun -> [AExpr] -> [AExpr] -> S [AExpr]
shiftLayer aid shft cs xs = do
        let n = length cs
            inps = map (flip shft xs) [0..2^n-1]
        ds <- (synDecode aid cs) >>= toSs
        makeMux aid (zip ds inps)

makeMux :: AId -> [(AExpr, [AExpr])] -> S [AExpr]
makeMux aid cxs = do
            tss <- mapM (\ (c, xs) -> mapM (toS . (aAnd aid) c) xs) cxs
            return (map (aOrs aid) (transpose tss))

type ShiftFun = Int -> [AExpr] -> [AExpr]

permSL :: ShiftFun
permSL  n xs = take (length xs) (replicate n aFalse ++ xs)
permSRL :: ShiftFun
permSRL n xs = take (length xs) (drop n xs ++ repeat aFalse)
permSRA :: ShiftFun
permSRA n xs = take (length xs) (drop n xs ++ repeat (last xs))
-- permRL  n xs = rTake n xs ++ rDrop n xs
-- permRR  n xs = drop n xs ++ take n xs

-----------------------------------------------------------------------------

synMul :: AId -> [AExpr] -> [AExpr] -> S [AExpr]
synMul aid xs ys = do
        let gate :: AExpr -> S [AExpr]
            gate x = toSs (map (aAnd aid x) ys)
            n = length xs
            shft :: Int -> [AExpr] -> [AExpr]
            shft k ys = replicate k aFalse ++ ys ++ replicate (n-k) aFalse
            sumPairwise :: [[AExpr]] -> S [[AExpr]]
            sumPairwise (ys1:ys2:yss) = do
                (_, s) <- synXAdd aid ys1 ys2 aFalse
                s' <- toSs s
                ss <- sumPairwise yss
                return (s':ss)
            sumPairwise yss = return yss
            sumTree :: [[AExpr]] -> S [AExpr]
            sumTree [ys] = return ys
            sumTree yss = sumPairwise yss >>= sumTree
        gyss <- mapM gate xs
        let sgyss = zipWith shft [0..] gyss
        sumTree sgyss

-----------------------------------------------------------------------------

-- scan :: (a->a->a) -> [a] -> [a]
-- scan op xs = f 1 xs
--   where f n xs =
--          case splitAt n xs of
--          (ls, []) -> ls
--          (ls, rs) -> f (2*n) (ls ++ zipWith op xs rs)

scanM :: (a -> a -> S a) -> [a] -> S [a]
scanM op xs = f 1 xs
  where f n xs =
            case splitAt n xs of
            (ls, []) -> return ls
            (ls, rs) -> do
                           ys <- zipWithM op xs rs
                           f (2*n) (ls ++ ys)

swap :: (b, a) -> (a, b)
swap (x, y) = (y, x)