Permalink
Browse files

All the necessary Copilot files.

  • Loading branch information...
1 parent 43acf46 commit d98561b59ad9d7b2d8646e5dcfb0a19a01aeedf9 @leepike committed Sep 19, 2010
View
29 LICENSE
@@ -0,0 +1,29 @@
+2009
+BSD3 License terms
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+Redistributions of source code must retain the above copyright
+notice, this list of conditions and the following disclaimer.
+
+Redistributions in binary form must reproduce the above copyright
+notice, this list of conditions and the following disclaimer in the
+documentation and/or other materials provided with the distribution.
+
+Neither the name of the developers nor the names of its contributors
+may be used to endorse or promote products derived from this software
+without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR
+CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
View
@@ -0,0 +1,36 @@
+module Language.Copilot
+ ( module Language.Copilot.Core
+ , module Language.Copilot.Analyser
+ , module Language.Copilot.Interpreter
+ , module Language.Copilot.Help
+ , module Language.Copilot.AtomToC
+ , module Language.Copilot.Compiler
+ , module Language.Copilot.Language
+ -- , module Language.Copilot.Dispatch
+ , module Language.Copilot.Interface
+ , module Language.Copilot.Tests.Random
+ , module Language.Copilot.Libs.Indexes
+ , module Language.Copilot.Libs.LTL
+ , module Language.Copilot.Libs.PTLTL
+ -- , module Language.Copilot.Examples.Examples
+ -- , module Language.Copilot.Examples.LTLExamples
+ -- , module Language.Copilot.Examples.PTLTLExamples
+ ) where
+
+import Language.Copilot.Core
+import Language.Copilot.Analyser
+import Language.Copilot.Interpreter
+import Language.Copilot.Help
+import Language.Copilot.AtomToC
+import Language.Copilot.Compiler
+import Language.Copilot.Language (opsF, opsF2, opsF3)
+import Language.Copilot.PrettyPrinter()
+import Language.Copilot.Tests.Random
+import Language.Copilot.Dispatch
+import Language.Copilot.Interface
+import Language.Copilot.Libs.Indexes
+import Language.Copilot.Libs.LTL
+import Language.Copilot.Libs.PTLTL
+-- import Language.Copilot.Examples.Examples
+-- import Language.Copilot.Examples.LTLExamples
+-- import Language.Copilot.Examples.PTLTLExamples
View
@@ -0,0 +1,45 @@
+-- TODO-Robin : Improve a lot that -> new package in Hackage ?
+-- generate C-Code with combinators, high-level, safe haskell.
+
+-- | Helper functions for writing free-form C code.
+module Language.Copilot.AdHocC (
+ varDecl, includeBracket, includeQuote,
+ printf, printfNewline
+ ) where
+
+import Data.List (intersperse)
+import Language.Atom (Type(..))
+import Language.Atom.Code (cType) -- C99
+
+-- | Takes a type and a list of variable names and declares them.
+varDecl :: Type -> [String] -> String
+varDecl t vars =
+ cType' t ++ " " ++ (unwords (intersperse "," vars)) ++ ";"
+ where
+ cType' Bool = "int"
+ cType' typ = cType typ
+
+
+-- | Add an include of a library
+includeBracket :: String -> String
+includeBracket lib = "#include <" ++ lib ++ ">"
+
+-- | Add an include of a header file
+includeQuote :: String -> String
+includeQuote lib = "#include \"" ++ lib ++ "\""
+
+printfPre :: String -> String
+printfPre = ("printf(\"" ++)
+
+printfPost :: [String] -> String
+printfPost vars =
+ let sep = if null vars then " " else ", "
+ in "\"" ++ sep ++ unwords (intersperse "," vars) ++ ");"
+
+newline :: String
+newline = "\\n"
+
+-- | printf, with and without a newline (nl) character.
+printf, printfNewline :: String -> [String] -> String
+printfNewline text vars = (printfPre text) ++ newline ++ (printfPost vars)
+printf text vars = (printfPre text) ++ (printfPost vars)
@@ -0,0 +1,238 @@
+{-# OPTIONS_GHC -XRelaxedPolyRec #-}
+
+-- | This module provides a way to check that a /Copilot/ specification is compilable
+module Language.Copilot.Analyser(
+ -- * Main error checking functions
+ check, Error(..), SpecSet(..),
+ -- * Varied other things
+ getExternalVars, getAtomType
+ {-
+ -- * Dependency Graphs (experimental)
+ Weight, Node(..), DependencyGraph,
+ mkDepGraph, showDG -}
+ ) where
+
+import Language.Copilot.Core
+
+import qualified Language.Atom as A
+
+import Data.List
+
+type Weight = Int
+
+-- | Used for representing an error in the specification, detected by @'check'@
+data Error =
+ BadSyntax String Var -- ^ the BNF is not respected
+ | BadDrop Int Var -- ^ A drop expression of less than 0 is used
+ | BadSamplingPhase Var Var Phase -- ^ if an external variable is sampled at phase 0 then there is no time for the stream to be updated
+ | BadType Var Var -- ^ either a variable is not defined, or not with the good type ; there is no implicit conversion of types in /Copilot/
+ | NonNegativeWeightedClosedPath [Var] Weight -- ^ The algorithm to compile /Copilot/ specification can only work if there is no negative weighted closed path in the specification, as described in the original research paper
+ | DependsOnClosePast [Var] Var Weight Weight -- ^ Could be compiled, but would need bigger prophecyArrays
+ | DependsOnFuture [Var] Var Weight-- ^ If an output depends of a future of an input it will be hard to compile to say the least
+
+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 a /Copilot/ specification.
+-- If it is not compilable, then returns an error describing the issue.
+-- Else, returns @Nothing@
+check :: StreamableMaps Spec -> Maybe Error
+check streams =
+ syntaxCheck streams &&> defCheck streams
+
+-- Represents all the kind of specs that are authorized after a given operator
+data SpecSet = AllSpecSet | FunSpecSet | DropSpecSet deriving Eq
+
+-- Check that the AST of the copilot specification match the BNF
+-- Could have been verified by the type checker if the type of Spec had been cut
+-- But then there would have been quite a lot construction/deconstruction to do everywhere.
+-- Hence the compact type for Spec and this extra check.
+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)
+
+-- checks that streams are well defined (ie can be compiled)
+-- Currently very inefficient (for simplicity's sake),
+-- could probably be optimized if need be
+-- by keeping weights of paths in a matrix and doing some linear algebra
+-- (fast exponentiation could give some nice results)
+-- could also reuse the dependency graph (see below)
+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 -- to help the typechecker
+ 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
+
+---- Dependency graphs (for next version of nNWCP, and for scheduling)
+{-
+type Weight = Int
+data Node =
+ InternalVar Var [(Weight, Node)]
+ | ExternalVar Var Phase
+ deriving Show -- for debug
+
+instance Eq Node where
+ InternalVar v _ == InternalVar v' _ = v == v'
+ ExternalVar v ph == ExternalVar v' ph' = v == v' && ph == ph'
+ _ == _ = False
+
+type DependencyGraph = [Node]
+
+showDG :: DependencyGraph -> [String]
+showDG dG = map show dG
+
+mkDepGraph :: StreamableMaps Spec -> DependencyGraph
+mkDepGraph streams =
+ dGFixpoint
+ where
+ dGFixpoint :: DependencyGraph
+ dGFixpoint = foldStreamableMaps mkNode streams []
+ mkNode :: Streamable a => Var -> Spec a -> DependencyGraph -> DependencyGraph
+ mkNode v s dG =
+ let edges = mkEdges 0 s
+ externalNodes = mkExternalNodes s in
+ (InternalVar v edges) : (nub $ externalNodes ++ dG)
+ -- TODO : the following functions can probably be fused together
+ mkExternalNodes :: Spec a -> [Node]
+ mkExternalNodes s =
+ case s of
+ PVar _ v ph -> [ExternalVar v ph]
+ Var _ -> []
+ Const _ -> []
+ F _ _ s0 -> mkExternalNodes s0
+ F2 _ _ s0 s1 -> mkExternalNodes s0 ++ mkExternalNodes s1
+ F3 _ _ s0 s1 s2 -> mkExternalNodes s0 ++ mkExternalNodes s1 ++ mkExternalNodes s2
+ Append _ s0 -> mkExternalNodes s0
+ Drop _ s0 -> mkExternalNodes s0
+ mkEdges :: Weight -> Spec a -> [(Weight, Node)]
+ mkEdges w s =
+ case s of
+ PVar _ v ph -> [(w, getNode v $ Just ph)]
+ Var v -> [(w, getNode v Nothing)]
+ Const _ -> []
+ F _ _ s0 -> mkEdges w s0
+ F2 _ _ s0 s1 -> mkEdges w s0 ++ mkEdges w s1
+ F3 _ _ s0 s1 s2 -> mkEdges w s0 ++ mkEdges w s1 ++ mkEdges w s2
+ Append ls s0 -> mkEdges (w - length ls) s0
+ Drop i s0 -> mkEdges (w + i) s0
+ getNode :: Var -> Maybe Phase -> Node
+ getNode v mp =
+ case mp of
+ Nothing -> fromJust $ find ((==) (InternalVar v [])) dGFixpoint
+ Just ph -> fromJust $ find ((==) (ExternalVar v ph)) dGFixpoint -}
Oops, something went wrong.

0 comments on commit d98561b

Please sign in to comment.