module Reader.Bindings
( specBindings
) where
import Utils
( strictSort
, imLookup
)
import Data.Types
( SignalDecType(..)
)
import Data.Binding
( Binding
, BindExpr(..)
)
import Data.Expression
( Expr(..)
, Expr'(..)
, SrcPos(..)
, ExprPos(..)
, subExpressions
)
import Reader.Data
( Specification(..)
, ExpressionTable
, NameTable
, PositionTable
, ArgumentTable
)
import Reader.Error
( Error
, errArgArity
, errConditional
, errCircularDep
)
import Data.Graph
( buildG
, scc
)
import Data.Tree
( flatten
)
import Data.Maybe
( fromJust
)
import Control.Monad.State
( StateT(..)
, execStateT
, put
, get
, when
)
import qualified Data.IntMap.Strict as IM
( IntMap
, map
, insert
, toList
, null
, minViewWithKey
, maxViewWithKey
)
type ArityTable = IM.IntMap Int
type BindingsBuilder a = a -> StateT ST (Either Error) ()
data ST = ST
{ tBinding :: ExpressionTable
, tName :: NameTable
, tPos :: PositionTable
, tArgs :: ArgumentTable
, tAry :: ArityTable
}
specBindings
:: Specification -> Either Error Specification
specBindings spec = do
let
p = SrcPos (1) (1)
pos = ExprPos p p
empty = Expr (SetExplicit []) pos
a =
ST { tBinding = IM.map (const empty) $ names spec
, tName = names spec
, tPos = positions spec
, tArgs = arguments spec
, tAry = IM.map length $ arguments spec
}
a' <- execStateT (specificationBindings spec) a
checkCircularDeps spec
{ bindings = tBinding a'
, dependencies = IM.map deps $ tBinding a'
}
specificationBindings
:: BindingsBuilder Specification
specificationBindings s = do
mapM_ binding $ parameters s
mapM_ binding $ definitions s
mapM_ signalBinding $ inputs s
mapM_ signalBinding $ outputs s
mapM_ exprBindings $ initially s
mapM_ exprBindings $ preset s
mapM_ exprBindings $ requirements s
mapM_ exprBindings $ invariants s
mapM_ exprBindings $ assumptions s
mapM_ exprBindings $ guarantees s
where
signalBinding x = case x of
SDSingle {} -> return ()
SDEnum {} -> return ()
SDBus (y,_) e -> do
addBinding (y,e)
exprBindings e
binding
:: BindingsBuilder Binding
binding b = do
mapM_ (\a -> addBinding (bIdent b,a)) $ bVal b
mapM_ exprBindings $ bVal b
exprBindings
:: BindingsBuilder (Expr Int)
exprBindings e = case expr e of
NumRPlus xs x -> mapM_ conditional xs >> exprBindings x
NumRMul xs x -> mapM_ conditional xs >> exprBindings x
SetRCup xs x -> mapM_ conditional xs >> exprBindings x
SetRCap xs x -> mapM_ conditional xs >> exprBindings x
BlnRAnd xs x -> mapM_ conditional xs >> exprBindings x
BlnROr xs x -> mapM_ conditional xs >> exprBindings x
BaseId x -> checkArity x 0
BaseFml xs x -> checkArity x (length xs)
BaseBus x y -> checkArity y 0 >> exprBindings x
_ -> mapM_ exprBindings $ subExpressions e
where
checkArity x j = do
a <- get
let n = imLookup x $ tAry a
when (n /= j) $
let m = imLookup x $ tName a
p = imLookup x $ tPos a
in errArgArity m n p $ srcPos e
conditional x = case expr x of
BlnElem l s -> case expr l of
BaseId i -> do
a <- get
put a {
tBinding = IM.insert i s $ tBinding a
}
_ -> errConditional $ srcPos e
BlnLE s r -> case expr s of
BlnLE l i -> range i (op NumPlus l) (op NumMinus r) $ srcPos x
BlnLEQ l i -> range i l (op NumMinus r) $ srcPos x
_ -> errConditional $ srcPos e
BlnLEQ s r -> case expr s of
BlnLE l i -> range i (op NumPlus l) r $ srcPos x
BlnLEQ l i -> range i l r $ srcPos x
_ -> errConditional $ srcPos e
_ -> errConditional $ srcPos e
op c x = Expr (c x (Expr (BaseCon 1) (srcPos x))) (srcPos x)
range x l u p = case expr x of
BaseId i -> do
a <- get
let s = Expr (SetRange l (op NumPlus l) u) p
put a {
tBinding = IM.insert i s $ tBinding a
}
_ -> errConditional $ srcPos e
addBinding
:: BindingsBuilder (Int,Expr Int)
addBinding (i,x) = do
a <- get
let y = imLookup i $ tBinding a
z = Expr (SetExplicit [x]) $ srcPos x
s = Expr (SetCup y z) $ srcPos y
put a {
tBinding = IM.insert i s $ tBinding a
}
deps
:: Expr Int -> [Int]
deps = strictSort . deps' []
where
deps' a e = case expr e of
BaseFml xs x -> foldl conditional (x:a) xs
BaseId x -> x:a
BaseBus x y -> deps' (y:a) x
NumRPlus xs x -> foldl conditional (deps' a x) xs
NumRMul xs x -> foldl conditional (deps' a x) xs
SetRCup xs x -> foldl conditional (deps' a x) xs
SetRCap xs x -> foldl conditional (deps' a x) xs
BlnRAnd xs x -> foldl conditional (deps' a x) xs
BlnROr xs x -> foldl conditional (deps' a x) xs
Colon x y -> case expr x of
Pattern z _ -> deps' (deps' a z) y
_ -> deps' (deps' a x) y
_ -> foldl deps' a $ subExpressions e
conditional k x = case expr x of
BlnElem _ y -> deps' k y
_ -> deps' k x
checkCircularDeps
:: Specification -> Either Error Specification
checkCircularDeps s = do
let
ys = concatMap (\(i,zs) -> map (\z -> (i,z)) zs) $
filter isunary $ IM.toList $
dependencies s
minkey =
if IM.null $ dependencies s then 0 else
fst $ fst $ fromJust $ IM.minViewWithKey $ dependencies s
maxkey =
if IM.null $ dependencies s then 0 else
fst $ fst $ fromJust $ IM.maxViewWithKey $ dependencies s
c = map flatten $ scc $ buildG (minkey,maxkey) ys
mapM_ check c
mapM_ checkSingelton ys
return s
where
isunary (x,_) = null $ imLookup x $ arguments s
check xs = when (length xs > 1) $
let
p = imLookup (head xs) $ positions s
ys = map (\i -> (imLookup i $ names s, imLookup i $ positions s)) xs
in
errCircularDep ys p
checkSingelton (i,j) = when (i == j) $
errCircularDep [(imLookup i $ names s, imLookup i $ positions s)] $
imLookup i $ positions s