module Language.Copilot.Analyser(
check, Error(..), SpecSet(..),
getExternalVars, ExtVars(..)
) where
import Language.Copilot.Core
import qualified Language.Atom as A
import Data.List
type Weight = Int
data Error =
BadSyntax String Var
| BadDrop Int Var
| BadSamplingPhase Var Var Phase
| BadSamplingArrPhase Var Var Phase
| BadPArrSpec Var Var String
| BadType Var Var
| NonNegativeWeightedClosedPath [Var] Weight
| DependsOnClosePast [Var] Var Weight Weight
| DependsOnFuture [Var] Var Weight
instance Show Error where
show (BadSyntax s v) =
unlines
["Error syntax : " ++ s ++ " is not allowed in that position in stream "
++ v ++ "."]
show (BadDrop i v) =
unlines
[ "Error : a Drop in stream " ++ v ++ " drops the number " ++ show i ++
"of elements.\n"
, show i ++ " is negative, and Drop only accepts positive arguments.\n"
]
show (BadSamplingPhase v v' ph) =
unlines
[ "Error : the external variable " ++ v' ++ " is sampled at phase " ++
show ph ++ " in the stream " ++ v ++ "."
, "Sampling can only occur from phase 1 onwards.\n"
]
show (BadSamplingArrPhase v arr ph) =
unlines
[ "Error : the external array " ++ arr ++ " is sampled at phase " ++
show ph ++ " in the stream " ++ v ++ "."
, " Sampling can only occur from phase 1 onwards.\n"
]
show (BadPArrSpec v arr idx) =
unlines
[ "Error : the index into an external array can only take a "
++ "variable or a constant. The index\n"
, idx ++ "\n\n in external array "
++ arr ++ "in the definition of stream " ++ v ++ " is not of that "
++ "form.\n"
]
show (BadType v v') =
unlines
[ "Error : the monitor variable " ++ v ++ ", called in the stream "
++ v' ++ ", either"
, "does not exist, or don't have the right type (there is no implicit "
++ "conversion).\n"
]
show (NonNegativeWeightedClosedPath vs w) =
unlines
[ "Error : the following path is closed in the dependency graph of the "
++ "specification and has"
, "weight " ++ show w ++ " which is positive (append decreases the weight, "
++ "while drop increases it)."
, "This is forbidden to avoid streams which could take 0 or several different"
++ " values."
, "Try adding some initial elements (e.g., [0,0,0] ++ ...) "
++ "to the offending streams."
, "Path : " ++ show (reverse vs) ++ "\n"
]
show (DependsOnClosePast vs v w len) =
unlines
[ "Error : the following path is of weight " ++ show w ++ " ending in "
++ "the external variable " ++ v
, "while the first variable of that path has a prophecy array of length "
++ show len ++ ","
, "which is strictly greater than the weight. This is forbidden."
, "Path : " ++ show (reverse vs) ++ "\n"
]
show (DependsOnFuture vs v w) =
unlines
[ "Error : the following path is of weight " ++ show w
++ " which is strictly positive."
, "This means that the first variable depends on the future of the "
++ "external variable " ++ v
, "which is quoted in the last variable of the path. This is "
++ "obviously impossible."
, "Path : " ++ show (reverse vs) ++ "\n"
]
(&&>) :: Maybe a -> Maybe a -> Maybe a
m &&> m' =
case m of
Just _ -> m
Nothing -> m'
(||>) :: Bool -> a -> Maybe a
b ||> x =
if b
then Nothing
else Just x
infixr 2 ||>
infixr 1 &&>
check :: StreamableMaps Spec -> Maybe Error
check streams =
syntaxCheck streams &&> defCheck streams
data SpecSet = AllSpecSet | FunSpecSet | DropSpecSet | PArrSet
deriving Eq
syntaxCheck :: StreamableMaps Spec -> Maybe Error
syntaxCheck streams =
foldStreamableMaps (checkSyntaxSpec AllSpecSet) streams Nothing
where
checkSyntaxSpec :: Streamable a
=> SpecSet -> Var -> Spec a -> Maybe Error -> Maybe Error
checkSyntaxSpec set v s e =
e &&>
case s of
Var _ -> Nothing
Const _ -> Nothing
PVar _ v' ph -> ph > 0 ||> BadSamplingPhase v v' ph
PArr _ (arr,s0) ph -> checkIndex v arr s0
&&> ph > 0 ||> BadSamplingArrPhase v arr ph
&&> checkSyntaxSpec PArrSet v s0 Nothing
F _ _ s0 -> set /= DropSpecSet ||> BadSyntax "F" v
&&> checkSyntaxSpec FunSpecSet v s0 Nothing
F2 _ _ s0 s1 -> set /= DropSpecSet ||> BadSyntax "F2" v
&&> checkSyntaxSpec FunSpecSet v s0 Nothing
&&> checkSyntaxSpec FunSpecSet v s1 Nothing
F3 _ _ s0 s1 s2 -> set /= DropSpecSet ||> BadSyntax "F3" v
&&> checkSyntaxSpec FunSpecSet v s0 Nothing
&&> checkSyntaxSpec FunSpecSet v s1 Nothing
&&> checkSyntaxSpec FunSpecSet v s2 Nothing
Append _ s0 -> set == AllSpecSet ||> BadSyntax "Append" v
&&> checkSyntaxSpec AllSpecSet v s0 Nothing
Drop i s0 -> (0 <= i) ||> BadDrop i v
&&> checkSyntaxSpec DropSpecSet v s0 Nothing
checkIndex _ _ (Var _) = Nothing
checkIndex _ _ (Const _) = Nothing
checkIndex v arr idx = Just $ BadPArrSpec v arr (show idx)
defCheck :: StreamableMaps Spec -> Maybe Error
defCheck streams =
let checkPathsFromSpec :: Streamable a => Var -> Spec a -> Maybe Error -> Maybe Error
checkPathsFromSpec v0 s0 e =
e &&> checkPath 0 [v0] s0
where
prophecyArrayLength s =
case s of
Append ls s' -> length ls + prophecyArrayLength s'
_ -> 0
checkPath :: Streamable a => Int -> [Var] -> Spec a -> Maybe Error
checkPath n vs s =
case s of
PVar t v _ -> case () of
() | n > 0 -> Just $ DependsOnFuture vs v n
| n > negate (prophecyArrayLength s0) ->
Just $ DependsOnClosePast vs v n
(prophecyArrayLength s0)
| t /= getAtomType s -> Just $ BadType v (head vs)
_ -> Nothing
PArr t (arr, idx) _
| n > 0 -> Just $ DependsOnFuture vs arr n
| n > negate (prophecyArrayLength idx) ->
Just $ DependsOnClosePast vs arr n
(prophecyArrayLength idx)
| t /= getAtomType s -> Just $ BadType arr (head vs)
| otherwise ->
case idx of
Const _ -> checkPath n vs idx
Var _ -> checkPath n vs idx
_ -> Just $ BadPArrSpec v0 arr (show idx)
Var v ->
if elem v vs
then if n >= 0
then Just $ NonNegativeWeightedClosedPath vs n
else Nothing
else
let spec = getMaybeElem v streams in
case spec of
Nothing -> Just $ BadType v (head vs)
Just s' -> checkPath n (v:vs) (s' `asTypeOf` s)
Const _ -> Nothing
F _ _ s1 -> checkPath n vs s1
F2 _ _ s1 s2 -> checkPath n vs s1 &&> checkPath n vs s2
F3 _ _ s1 s2 s3 -> checkPath n vs s1 &&> checkPath n vs s2
&&> checkPath n vs s3
Append l s' -> checkPath (n length l) vs s'
Drop i s' -> checkPath (n + i) vs s'
in foldStreamableMaps checkPathsFromSpec streams Nothing
type Exs = (A.Type, Var, ExtVars)
data ExtVars = ExtV Phase
| ExtA Phase String
deriving Eq
getExternalVars :: StreamableMaps Spec -> [Exs]
getExternalVars streams =
nub $ foldStreamableMaps decl streams []
where
decl :: Streamable a
=> Var -> Spec a -> [Exs] -> [Exs]
decl _ s ls =
case s of
PVar t v ph -> (t, v, ExtV ph) : ls
PArr t (arr, s0) ph -> (t, arr, ExtA ph (show s0)) : ls
F _ _ s0 -> decl undefined s0 ls
F2 _ _ s0 s1 -> decl undefined s0 $ decl undefined s1 ls
F3 _ _ s0 s1 s2 -> decl undefined s0 $ decl undefined s1
$ decl undefined s2 ls
Drop _ s' -> decl undefined s' ls
Append _ s' -> decl undefined s' ls
_ -> ls