module Language.Copilot.Analyser(
check, Error(..), SpecSet(..),
getExternalVars, getAtomType
) 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
| BadType Var Var
| NonNegativeWeightedClosedPath [Var] Weight
| DependsOnClosePast [Var] Var Weight Weight
| DependsOnFuture [Var] Var Weight
instance Show Error where
show (BadSyntax s v) =
"Error syntax : " ++ s ++ "is not allowed in that position in stream " ++ v ++ "\n"
show (BadDrop i v) =
"Error : a Drop in stream " ++ v ++ "drops the number " ++ show i ++
"of elements. " ++ show i ++ " is negative, and Drop only accepts positive arguments. \n"
show (BadSamplingPhase v v' ph) =
"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 (BadType v v') =
"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) =
"Error : the following path is closed in the dependency graph of this "
++ "specification and have weight " ++ show w ++ " which is positive (append decrease the weight, "
++ "while drop increase 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. \n"
++ "Path : " ++ show (reverse vs) ++ "\n"
show (DependsOnClosePast vs v w len) =
"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. \n"
++ "Path : " ++ show (reverse vs) ++ "\n"
show (DependsOnFuture vs v w) =
"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. \n"
++ "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 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
PVar _ v' ph -> ph > 0 ||> BadSamplingPhase v v' ph
Var _ -> Nothing
Const _ -> 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)
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
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
getAtomType :: Streamable a => Spec a -> A.Type
getAtomType s =
let unitElem = unit
_ = (Const unitElem) `asTypeOf` s
in atomType unitElem
getExternalVars :: StreamableMaps Spec -> [(A.Type, Var, Phase)]
getExternalVars streams =
nub $ foldStreamableMaps decl streams []
where
decl :: Streamable a => Var -> Spec a -> [(A.Type, Var, Phase)] -> [(A.Type, Var, Phase)]
decl _ s ls =
case s of
PVar t v ph -> (t, v, ph) : 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