module Language.Copilot.Analyser(
check, Error(..), SpecSet(..),
getExternalVars
) where
import Language.Copilot.Core
import Data.List
import Data.Maybe(mapMaybe)
type Weight = Int
data Error =
BadSyntax String Var
| BadDrop Int Var
| BadPArrSpec Var Ext String
| BadType Var String
| BadTypeExt Ext Var
| NonNegativeWeightedClosedPath [Var] Weight
| DependsOnClosePast [Var] Ext Weight Weight
| DependsOnFuture [Var] Ext Weight
| NoInit Var
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 (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 "
++ show arr ++ "in the definition of stream " ++ v ++ " is not of that "
++ "form.\n"
]
show (BadType v v') =
unlines
[ "Error : the monitor variable " ++ v ++ ", called from "
++ v' ++ ", either"
, "does not exist, or don't have the right type (there is no implicit "
++ "conversion).\n"
]
show (BadTypeExt v v') =
unlines
[ "Error : the external call " ++ show 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 " ++ show 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 " ++ show v
, "which is quoted in the last variable of the path. This is "
++ "obviously impossible."
, "Path : " ++ show (reverse vs) ++ "\n"
]
show (NoInit v) =
"Error : the Copilot variable " ++ v ++ " appears either as an argument in an "
++ "external function that is sampled or an index in an external array being sampled. "
++ "In either case, the stream must have an initial value (that is not drawn from an "
++ "external variable)."
(&&>) :: 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 &&> checkInitsArgs 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
Var _ -> Nothing
Const _ -> Nothing
PVar _ _ -> Nothing
PArr _ (arr,s0) -> checkIndex v arr s0
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 $ BadTypeExt 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 $ BadTypeExt 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
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 -> (t, v, ExtRetV) : ls
PArr t (arr, s0) -> (t, arr
, ExtRetA (case s0 of
Var v -> V v
Const c -> C (show c)
_ -> error "Error in getExternalVars.")
) : 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
checkInitsArgs :: StreamableMaps Spec -> Maybe Error
checkInitsArgs streams =
let checkInits :: Streamable a => Var -> Spec a -> Maybe Error -> Maybe Error
checkInits v s err =
err &&> if checkPath 0 [v] s >= 0 then Just (NoInit v)
else Nothing
where checkPath :: Streamable a => Int -> [Var] -> Spec a -> Int
checkPath n vs s0 =
if (v `elem` samplingFuncs) || (v `elem` arrIndices)
then case s0 of
Var v0 -> if elem v0 vs then n
else checkPath n (v0:vs)
(getElem v0 streams `asTypeOf` s0)
Append ls s1 -> checkPath (n length ls) vs s1
Drop m s1 -> checkPath (m + n) vs s1
_ -> n
else (1)
samplingFuncs =
concatMap (\x -> case x of
(_, Fun _ args, _) ->
mapMaybe (\arg ->
case arg of
C _ -> Nothing
V v0 -> Just v0
) args
(_, ExtV _, _) -> [])
(getExternalVars streams)
arrIndices = mapMaybe (\x -> case x of
(_,_,ExtRetV) -> Nothing
(_,_,ExtRetA idx) ->
case idx of
V v' -> Just v'
C _ -> Nothing)
(getExternalVars streams)
in foldStreamableMaps checkInits streams Nothing