packages feed

copilot-core 3.2 → 3.2.1

raw patch · 21 files changed

+353/−66 lines, 21 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

CHANGELOG view
@@ -1,3 +1,7 @@+2021-03-05+        * Version bump (3.2.1). (#31)+        * Completed the documentation. (#22)+ 2020-12-06 Ivan Perez <ivan.perez@acm.org>         * Version bump (3.2).         * Fixed implementation of tysize for n-dimensional arrays. (#20).
copilot-core.cabal view
@@ -1,6 +1,6 @@ cabal-version:       >=1.10 name:                copilot-core-version:             3.2+version:             3.2.1 synopsis:            An intermediate representation for Copilot. description:   Intermediate representation for Copilot.
src/Copilot/Core.hs view
@@ -3,14 +3,12 @@ --------------------------------------------------------------------------------  -- | Intermediate representation for Copilot specifications.--- The form of the representation is based on this paper:+-- The following articles might also be useful: -- -- * Carette, Jacques and Kiselyov, Oleg and Shan, Chung-chieh, -- \"/Finally tagless, partially evaluated: Tagless staged/ -- /interpreters for simpler typed languages/\", -- Journal of Functional Programming vol. 19, p. 509-543, 2009.------ The following article might also be useful: -- -- * Guillemette, Louis-Julien and Monnier, Stefan, -- \"/Type-Safe Code Transformations in Haskell/\",
src/Copilot/Core/Error.hs view
@@ -4,11 +4,15 @@  {-# LANGUAGE Safe #-} +-- | Custom functions to report error messages to users. module Copilot.Core.Error   ( impossible   , badUsage ) where -impossible :: String -> String -> a+-- | Report an error due to a bug in Copilot.+impossible :: String -- ^ Name of the function in which the error was detected.+           -> String -- ^ Name of the package in which the function is located.+           -> a impossible function package =   error $ "\"Impossible\" error in function "     ++ function ++ ", in package " ++ package@@ -16,5 +20,7 @@     ++ "https://github.com/Copilot-Language/copilot/issues"     ++ "or email the maintainers at <dev@dedden.net>" -badUsage :: String -> a+-- | Report an error due to an error detected by Copilot (e.g., user error).+badUsage :: String -- ^ Description of the error.+         -> a badUsage msg = error $ "Copilot error: " ++ msg
src/Copilot/Core/Expr.hs view
@@ -5,6 +5,7 @@ {-# LANGUAGE Safe #-} {-# LANGUAGE GADTs, ExistentialQuantification #-} +-- | Internal representation of Copilot stream expressions. module Copilot.Core.Expr   ( Id   , Name@@ -42,6 +43,11 @@  -------------------------------------------------------------------------------- +-- | Internal representation of Copilot stream expressions.+--+-- The Core representation mimics the high-level Copilot stream, but the Core+-- representation contains information about the types of elements in the+-- stream. data Expr a where   Const        :: Typeable a => Type a -> a -> Expr a   Drop         :: Typeable a => Type a -> DropIdx -> Id -> Expr a@@ -55,7 +61,9 @@  -------------------------------------------------------------------------------- --- | A untyped expression (no phantom type).+-- | A untyped expression that carries the information about the type of the+-- expression as a value, as opposed to exposing it at type level (using an+-- existential). data UExpr = forall a. Typeable a => UExpr   { uExprType :: Type a   , uExprExpr :: Expr a }
src/Copilot/Core/External.hs view
@@ -6,6 +6,7 @@ {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE Rank2Types #-} +-- | Internal Copilot Core representation of Copilot externs. module Copilot.Core.External   ( ExtVar (..)   , externVars@@ -22,12 +23,15 @@  -------------------------------------------------------------------------------- +-- | An extern variable declaration, together with the type of the underlying+-- extern. data ExtVar = ExtVar   { externVarName :: Name   , externVarType :: UType }  -------------------------------------------------------------------------------- +-- | List of all externs used in a specification. externVars :: Spec -> [ExtVar] externVars = nubBy eqExt . toList . all externVarsExpr   where@@ -35,6 +39,7 @@   eqExt ExtVar { externVarName = name1 } ExtVar { externVarName = name2 } =     name1 == name2 +-- | Extract all externs used in a Copilot expression. externVarsExpr :: Expr a -> DList ExtVar externVarsExpr e0 = case e0 of   Const  _ _                -> empty@@ -49,11 +54,14 @@                                externVarsExpr e3   Label _ _ e               -> externVarsExpr e +-- | Extract all expressions used in an untyped Copilot expression. externVarsUExpr :: UExpr -> DList ExtVar externVarsUExpr UExpr { uExprExpr = e } = externVarsExpr e  -------------------------------------------------------------------------------- +-- | Apply a function to all expressions in a specification, concatenating the+-- results. all :: (forall a . Expr a -> DList b) -> Spec -> DList b all f spec =   concat (fmap (allStream) (specStreams   spec)) `append`
src/Copilot/Core/Interpret.hs view
@@ -16,10 +16,14 @@ import Copilot.Core.Interpret.Render import Copilot.Core.Type.Show (ShowType(..)) +-- | Output format for the results of a Copilot spec interpretation. data Format = Table | CSV --- | Interprets a Copilot specification.-interpret :: Format -> Int -> Spec -> String+-- | Interpret a Copilot specification.+interpret :: Format  -- ^ Format to be used for the output.+          -> Int     -- ^ Number of steps to interpret.+          -> Spec    -- ^ Specification to interpret.+          -> String interpret format k spec =   case format of     Table -> renderAsTable e
src/Copilot/Core/Interpret/Eval.hs view
@@ -31,17 +31,25 @@  -------------------------------------------------------------------------------- +-- | Exceptions that may be thrown during interpretation of a Copilot+-- specification. data InterpException   = -- NoValues Name --  | BadType Name-    ArrayWrongSize Name Int-  | ArrayIdxOutofBounds Name Int Int-  | DivideByZero-  | NotEnoughValues Name Int+    ArrayWrongSize Name Int           -- ^ Extern array has incorrect size.+  | ArrayIdxOutofBounds Name Int Int  -- ^ Index out-of-bounds exception.+  | DivideByZero                      -- ^ Division by zero.+  | NotEnoughValues Name Int          -- ^ For one or more streams, not enough+                                      --   values are available to simulate the+                                      --   number of steps requested. --  | NoExtFunEval Name-  | NoExtsInterp Name+  | NoExtsInterp Name                 -- ^ One of the externs used by the+                                      --   specification does not declare+                                      --   sample values to be used during+                                      --   simulation.   deriving Typeable +-- | Show a descriptive message of the exception. instance Show InterpException where   ---------------------------------------   -- show (NoValues name)                                                         =@@ -79,10 +87,14 @@       ++ "some stream with which to simulate the function."   --------------------------------------- +-- | Allow throwing and catching 'InterpException' using Haskell's standard+-- exception mechanisms. instance Exception InterpException  -------------------------------------------------------------------------------- +-- | An environment that contains an association between (stream or extern)+-- names and their values. type Env nm = [(nm, Dynamic)]  -- -- | External arrays environment.@@ -96,16 +108,23 @@  -------------------------------------------------------------------------------- +-- | The simulation output is defined as a string. Different backends may+-- choose to format their results differently. type Output = String +-- | An execution trace, containing the traces associated to each individual+-- monitor trigger and observer. data ExecTrace = ExecTrace-    -- map from trigger names to their maybe output, which is a list of strings-    -- representing their values.  (Nothing output if the guard for the trigger-    -- is false).  The order is important, since we compare the arg lists-    -- between the interpreter and backends.   { interpTriggers  :: [(String, [Maybe [Output]])]-    -- map from observer names to their outputs.  We also show observer outputs.-  , interpObservers :: [(String, [Output])] }++    -- ^ Map from trigger names to their optional output, which is a list of+    -- strings representing their values. The output may be 'Nothing' if the+    -- guard for the trigger was false. The order is important, since we+    -- compare the arg lists between the interpreter and backends.++  , interpObservers :: [(String, [Output])]+    -- ^ Map from observer names to their outputs.+  }   deriving Show  --------------------------------------------------------------------------------@@ -129,7 +148,13 @@ -- We could write this in a beautiful lazy style like above, but that creates a -- space leak in the interpreter that is hard to fix while maintaining laziness. -- We take a more brute-force appraoch below.-eval :: ShowType -> Int -> Spec -> ExecTrace++-- | Evaluate a specification for a number of steps.+eval :: ShowType   -- ^ Show booleans as @0@\/@1@ (C) or @True@\/@False@+                   --   (Haskell).+     -> Int        -- ^ Number of steps to evaluate.+     -> Spec       -- ^ Specification to evaluate.+     -> ExecTrace eval showType k spec = --  let exts  = take k $ reverse exts'                          in @@ -152,8 +177,12 @@  -------------------------------------------------------------------------------- +-- | An environment that contains an association between (stream or extern)+-- names and their values. type LocalEnv = [(Name, Dynamic)] +-- | Evaluate an expression for a number of steps, obtaining the value+-- of the sample at that time. evalExpr_ :: Typeable a => Int -> Expr a -> LocalEnv -> Env Id -> a evalExpr_ k e0 locs strms = case e0 of   Const _ x                          -> x@@ -187,6 +216,8 @@  -------------------------------------------------------------------------------- +-- | Evaluate an extern stream for a number of steps, obtaining the value of+-- the sample at that time. evalExternVar :: Int -> Name -> Maybe [a] -> a evalExternVar k name exts =   case exts of@@ -222,6 +253,9 @@  -------------------------------------------------------------------------------- +-- | Evaluate an 'Copilot.Core.Operators.Op1' by producing an equivalent+-- Haskell function operating on the same types as the+-- 'Copilot.Core.Operators.Op1'. evalOp1 :: Op1 a b -> (a -> b) evalOp1 op = case op of   Not        -> P.not@@ -250,6 +284,9 @@  -------------------------------------------------------------------------------- +-- | Evaluate an 'Copilot.Core.Operators.Op2' by producing an equivalent+-- Haskell function operating on the same types as the+-- 'Copilot.Core.Operators.Op2'. evalOp2 :: Op2 a b c -> (a -> b -> c) evalOp2 op = case op of   And          -> (&&)@@ -275,27 +312,39 @@   BwShiftR _ _ -> ( \ !a !b -> shiftR a $! fromIntegral b )   Index    _   -> \xs n -> (arrayelems xs) !! (fromIntegral n) +-- | Apply a function to two numbers, so long as the second one is+-- not zero.+--+-- Used to detect attempts at dividing by zero and produce the appropriate+-- 'InterpException'. catchZero :: Integral a => (a -> a -> a) -> (a -> a -> a) catchZero _ _ 0 = throw DivideByZero catchZero f x y = f x y  -------------------------------------------------------------------------------- +-- | Evaluate an 'Copilot.Core.Operators.Op3' by producing an equivalent+-- Haskell function operating on the same types as the+-- 'Copilot.Core.Operators.Op3'. evalOp3 :: Op3 a b c d -> (a -> b -> c -> d) evalOp3 (Mux _) = \ !v !x !y -> if v then x else y  -------------------------------------------------------------------------------- +-- | Turn a stream into a key-value pair that can be added to an 'Env' for+-- simulation. initStrm :: Stream -> (Id, Dynamic) initStrm Stream { streamId       = id                 , streamBuffer   = buffer                 , streamExprType = t } =   (id, toDyn (reverse buffer)) --- XXX actually only need to compute until shortest stream is of length k--- XXX this should just be a foldl' over [0,1..k]+-- | Evaluate several streams for a number of steps, producing the environment+-- at the end of the evaluation. evalStreams :: Int -> [Stream] -> Env Id -> Env Id evalStreams top specStrms initStrms =+  -- XXX actually only need to compute until shortest stream is of length k+  -- XXX this should just be a foldl' over [0,1..k]   evalStreams_ 0 initStrms   where   evalStreams_ :: Int -> Env Id -> Env Id@@ -314,8 +363,14 @@  -------------------------------------------------------------------------------- -evalTrigger ::-  ShowType -> Int -> Env Id -> Trigger -> [Maybe [Output]]+-- | Evaluate a trigger for a number of steps.+evalTrigger :: ShowType          -- ^ Show booleans as @0@/@1@ (C) or+                                 --   @True@/@False@ (Haskell).+            -> Int               -- ^ Number of steps to evaluate.+            -> Env Id            -- ^ Environment to use with known+                                 --   stream-value associations.+            -> Trigger           -- ^ Trigger to evaluate.+            -> [Maybe [Output]] evalTrigger showType k strms   Trigger     { triggerGuard = e@@ -341,7 +396,15 @@     map (showWithType showType t) (evalExprs_ k e1 strms)  ---------------------------------------------------------------------------------evalObserver :: ShowType -> Int -> Env Id -> Observer -> [Output]++-- | Evaluate an observer for a number of steps.+evalObserver :: ShowType  -- ^ Show booleans as @0@/@1@ (C) or @True@/@False@+                          --   (Haskell).+             -> Int       -- ^ Number of steps to evaluate.+             -> Env Id    -- ^ Environment to use with known stream-value+                          --   associations.+             -> Observer  -- ^ Observer to evaluate.+             -> [Output] evalObserver showType k strms   Observer     { observerExpr     = e@@ -350,6 +413,8 @@  -------------------------------------------------------------------------------- +-- | Evaluate an expression for a number of steps, producing a list with the+-- changing value of the expression until that time. evalExprs_ :: Typeable a => Int -> Expr a -> Env Id -> [a] evalExprs_ k e strms =   map (\i -> evalExpr_ i e [] strms) [0..(k-1)]
src/Copilot/Core/Interpret/Render.hs view
@@ -2,7 +2,7 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- --- | An tagless interpreter for Copilot specifications.+-- | Pretty-print the results of a simulation.  {-# LANGUAGE Safe #-} @@ -20,6 +20,7 @@  -------------------------------------------------------------------------------- +-- | Render an execution trace as a table, formatted to faciliate readability. renderAsTable :: ExecTrace -> String renderAsTable   ExecTrace@@ -50,15 +51,20 @@  -------------------------------------------------------------------------------- +-- | Render an execution trace as using comma-separate value (CSV) format. renderAsCSV :: ExecTrace -> String renderAsCSV = render . unfold +-- | Pretty print all the steps of the execution trace and concatenate the+-- results. unfold :: ExecTrace -> Doc unfold r =   case step r of     (cs, Nothing) -> cs     (cs, Just r') -> cs $$ unfold r' +-- | Pretty print the state of the triggers, and provide a continuation+-- for the execution trace at the next point in time. step :: ExecTrace -> (Doc, Maybe ExecTrace) step ExecTrace        { interpTriggers  = trigs@@ -101,18 +107,24 @@  asColumnsWithBuff :: [[Doc]] -> Int -> Doc asColumnsWithBuff lls q = normalize-        where normalize = vcat $ map hsep -                        $ map (\x -> pad (length x) longColumnLen empty x) +        where normalize = vcat $ map hsep+                        $ map (\x -> pad (length x) longColumnLen empty x)                         $ pad' longEntryLen q                         $ transpose lls -- normalize column height               longColumnLen = maximum (map length lls)               longEntryLen = maximum $ map docLen (concat lls) -docLen d = length $ render d +docLen d = length $ render d +-- | Pad a string on the right to reach an expected length. pad :: Int -> Int -> a -> [a] -> [a] pad lx max b ls = ls ++ replicate (max - lx) b +-- | Pad a list of strings on the right with spaces.+pad' :: Int      -- ^ Mininum number of spaces to add+     -> Int      -- ^ Maximum number of spaces to add+     -> [[Doc]]  -- ^ List of documents to pad+     -> [[Doc]] pad' _ _ []       = []-pad' mx q (ls:xs) = map buf ls : pad' mx q xs +pad' mx q (ls:xs) = map buf ls : pad' mx q xs         where buf x = x <> (hcat $ replicate q space) <> (hcat $ replicate (mx - (docLen x)) space)
src/Copilot/Core/Locals.hs view
@@ -3,6 +3,11 @@ --------------------------------------------------------------------------------  -- | Let expressions.+--+-- Although Copilot is a DSL embedded in Haskell and Haskell does support let+-- expressions, we want Copilot to be able to implement explicit sharing, to+-- detect when the same stream is being used in multiple places in a+-- specification and avoid recomputing it unnecessarily.  {-# LANGUAGE Trustworthy #-} {-# LANGUAGE ExistentialQuantification #-}@@ -19,15 +24,18 @@  -------------------------------------------------------------------------------- +-- | A local definition, with a given stream name and stream type. data Loc = forall a . Loc   { localName :: Name   , localType :: Type a } +-- | Show the underlying stream name. instance Show Loc where   show Loc { localName = name } = name  -------------------------------------------------------------------------------- +-- | Obtain all the local definitions in a specification. locals :: Spec -> [Loc] locals   Spec@@ -47,11 +55,13 @@  -------------------------------------------------------------------------------- +-- | Obtain all the local definitions in a stream. locsStream :: Stream -> DList Loc locsStream Stream { streamExpr = e } = locsExpr e  -------------------------------------------------------------------------------- +-- | Obtain all the local definitions in a trigger. locsTrigger :: Trigger -> DList Loc locsTrigger Trigger { triggerGuard = e, triggerArgs = args } =   locsExpr e `append` concat (fmap locsUExpr args)@@ -63,11 +73,13 @@  -------------------------------------------------------------------------------- +-- | Obtain all the local definitions in an observer. locsObserver :: Observer -> DList Loc locsObserver Observer { observerExpr = e } = locsExpr e  -------------------------------------------------------------------------------- +-- | Obtain all the local definitions in an expression. locsExpr :: Expr a -> DList Loc locsExpr e0 = case e0 of   Const  _ _             -> empty
src/Copilot/Core/MakeTags.hs view
@@ -2,7 +2,7 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- --- | Sets a unique tags for each external array/function/struct call.+-- | Sets a unique tags for each external array\/function\/struct call.  {-# LANGUAGE Safe #-}
src/Copilot/Core/Operators.hs view
@@ -5,6 +5,7 @@ {-# LANGUAGE Safe #-} {-# LANGUAGE GADTs, Rank2Types #-} +-- | Internal representation of Copilot operators. module Copilot.Core.Operators   ( Op1 (..)   , Op2 (..)@@ -20,7 +21,7 @@  -------------------------------------------------------------------------------- --- Unary operators.+-- | Unary operators. data Op1 a b where   -- Boolean operators.   Not      :: Op1 Bool Bool@@ -49,8 +50,11 @@   BwNot    :: Bits     a => Type a -> Op1 a a   -- Casting operator.   Cast     :: (Integral a, Num b) => Type a -> Type b -> Op1 a b+              -- ^ Casting operator.+   -- Struct operator.   GetField :: KnownSymbol s => Type a -> Type b -> (a -> Field s b) -> Op1 a b+              -- ^ Projection of a struct field.  -- | Binary operators. data Op2 a b c where@@ -84,7 +88,9 @@   BwShiftL :: ( Bits a, Integral b ) => Type a -> Type b -> Op2 a b a   BwShiftR :: ( Bits a, Integral b ) => Type a -> Type b -> Op2 a b a   -- Array operator.+   Index    :: Type (Array n t) -> Op2 (Array n t) Word32 t+              -- ^ Array access/projection of an array element.  -- | Ternary operators. data Op3 a b c d where
src/Copilot/Core/PrettyDot.hs view
@@ -2,7 +2,7 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- --- | A pretty printer for Copilot specifications.+-- | A pretty printer for Copilot specifications as GraphViz/dot graphs.  {-# LANGUAGE Safe #-} {-# LANGUAGE GADTs #-}@@ -19,6 +19,7 @@ import Data.List (intersperse) import Text.Printf +-- | Create a temporary/internal name from an extern variable name. mkExtTmpVar :: String -> String mkExtTmpVar = ("ext_" ++) @@ -31,7 +32,15 @@  -------------------------------------------------------------------------------- -ppExprDot :: Int -> Int -> Bool -> Expr a -> (Doc,Int)+-- | Pretty print a Copilot Expression as a GraphViz graph part.+--+-- See the+-- <https://github.com/Copilot-Language/copilot-discussion/tree/master/TutorialAndDevGuide/DevGuide development guide> for details.+ppExprDot :: Int       -- ^ Index or ID of the next node in the graph.+          -> Int       -- ^ Index or ID of the parent node in the graph.+          -> Bool      -- ^ Mark externs with the prefix @externV:@.+          -> Expr a    -- ^ The expression to pretty print.+          -> (Doc,Int) ppExprDot ii pere bb e0 = case e0 of   Const t x                  -> (text (printf "%s [label=\"const: %s\",color=red1, style=filled]\n" (show ii::String) ((showWithType Haskell t x)::String) )                   <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)),ii+1)@@ -39,7 +48,9 @@                   <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)),ii+1)   Drop _ i id                ->  (text (printf "%s [label=\"drop %s: \nstream: %s\",color=crimson, style=filled]\n" (show ii::String) (show i::String) (show id::String) )                   <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)),ii+1)-  ExternVar _ name _         -> (if bb then (text (printf "%s [label=\"externV: %s\",color=cyan1, style=filled]\n" (show ii::String) (name::String)) <> text (printf "%s -> %s\n" (show pere::String) (show ii::String))) else (text (printf "%s [label=\"%s\",color=cyan1, style=filled]\n" (show ii::String) (mkExtTmpVar name)) <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)))+  ExternVar _ name _         -> (if bb+                                   then (text (printf "%s [label=\"externV: %s\",color=cyan1, style=filled]\n" (show ii::String) (name::String)) <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)))+                                   else (text (printf "%s [label=\"%s\",color=cyan1, style=filled]\n" (show ii::String) (mkExtTmpVar name))      <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)))                   ,ii+1)   Local _ _ name e1 e2       -> let (r1, i1) = ppExprDot (ii+2) (ii+1) bb e1                                 in let (r2, i2) = ppExprDot (i1) ii bb e2@@ -78,9 +89,18 @@                   <> text (printf "%s -> %s\n" (show pere::String) (show ii::String))                   <> r1,i1) -ppUExpr :: Int -> Int -> Bool -> UExpr -> (Doc, Int)+-- | Pretty print an untyped Copilot Expression as a graphiViz graph part.+--+-- See the+-- <https://github.com/Copilot-Language/copilot-discussion/tree/master/TutorialAndDevGuide/DevGuide development guide> for details.+ppUExpr :: Int        -- ^ Index or ID of the next node in the graph.+        -> Int        -- ^ Index or ID of the parent node in the graph.+        -> Bool       -- ^ Mark externs with the prefix @externV:@.+        -> UExpr      -- ^ The expression to pretty print.+        -> (Doc, Int) ppUExpr i pere bb UExpr { uExprExpr = e0 } = ppExprDot i pere bb e0 +-- | Pretty print a unary operator. ppOp1 :: Op1 a b -> String ppOp1 op = case op of   Not      -> "not"@@ -105,6 +125,7 @@   BwNot _  -> "~"   Cast _ _ -> "(cast)" +-- | Pretty print a binary operator. ppOp2 :: Op2 a b c -> String ppOp2 op = case op of   And          -> "&&"@@ -129,13 +150,17 @@   BwShiftL _ _ -> "<<"   BwShiftR _ _ -> ">>" +-- | Pretty print a ternary operator. ppOp3 :: Op3 a b c d -> String ppOp3 op = case op of   Mux _    -> "mux"  -------------------------------------------------------------------------------- -ppStream :: Int -> Stream -> (Doc, Int)+-- | Pretty print a stream as a GraphViz graph part.+ppStream :: Int        -- ^ Index or ID of the next node in the graph.+         -> Stream     -- ^ Stream to pretty print+         -> (Doc, Int) ppStream i   Stream     { streamId       = id@@ -153,7 +178,10 @@     where (r1, i1) = ppExprDot (i+3) (i+1) True e -------------------------------------------------------------------------------- -ppTrigger :: Int -> Trigger -> (Doc, Int)+-- | Pretty print a trigger as a GraphViz graph part.+ppTrigger :: Int        -- ^ Index or ID of the next node in the graph.+          -> Trigger    -- ^ Trigger to pretty print+          -> (Doc, Int) ppTrigger i   Trigger     { triggerName  = name@@ -171,7 +199,13 @@     (r1, i1) = ppExprDot (i+2) (i+1) True e     (r2, i2) = ppUExprL (i1+1) (i1) True args -ppUExprL :: Int -> Int -> Bool -> [UExpr] -> ([Doc], Int)+-- | Pretty print a list of untyped Copilot Expressions as a GraphViz graph+-- part.+ppUExprL :: Int           -- ^ Index or ID of the next node in the graph.+         -> Int           -- ^ Index or ID of the parent node in the graph.+         -> Bool          -- ^ Mark externs with the prefix @externV:@.+         -> [UExpr]       -- ^ The list of expressions to pretty print.+         -> ([Doc], Int) ppUExprL i _ _ [] = ([], i)  ppUExprL i pere bb (a:b) = ((r1:r2), i2)@@ -181,7 +215,10 @@  -------------------------------------------------------------------------------- -ppObserver :: Int -> Observer -> (Doc, Int)+-- | Pretty print an observer as a GraphViz graph part.+ppObserver :: Int         -- ^ Index or ID of the next node in the graph.+           -> Observer    -- ^ Observer to pretty print+           -> (Doc, Int) ppObserver i   Observer     { observerName     = name@@ -192,7 +229,10 @@   where (r1, i1) = ppExprDot (i+1) i True e -------------------------------------------------------------------------------- -ppProperty :: Int -> Property -> (Doc, Int)+-- | Pretty print a property as a GraphViz graph part.+ppProperty :: Int         -- ^ Index or ID of the next node in the graph.+           -> Property    -- ^ Property to pretty print+           -> (Doc, Int) ppProperty i   Property     { propertyName     = name@@ -207,7 +247,10 @@  -------------------------------------------------------------------------------- -ppStreamL :: Int -> [Stream] -> (Doc, Int)+-- | Pretty print a list of streams as a GraphViz graph part.+ppStreamL :: Int        -- ^ Index or ID of the next node in the graph.+          -> [Stream]   -- ^ List of streams to pretty print+          -> (Doc, Int) ppStreamL i [] = (empty,i)  ppStreamL i (a:b) = ((s1$$s2),(i2))@@ -217,7 +260,10 @@  -------------------------------------------------------------------------------- -ppTriggerL :: Int -> [Trigger] -> (Doc, Int)+-- | Pretty print a list of triggers as a GraphViz graph part.+ppTriggerL :: Int        -- ^ Index or ID of the next node in the graph.+           -> [Trigger]  -- ^ List of triggers to pretty print+           -> (Doc, Int) ppTriggerL i [] = (empty,i)  ppTriggerL i (a:b) = ((s1$$s2),(i2))@@ -227,7 +273,10 @@  -------------------------------------------------------------------------------- -ppObserverL :: Int -> [Observer] -> (Doc, Int)+-- | Pretty print a list of observers as a GraphViz graph part.+ppObserverL :: Int         -- ^ Index or ID of the next node in the graph.+            -> [Observer]  -- ^ List of observers to pretty print+            -> (Doc, Int) ppObserverL i [] = (empty,i)  ppObserverL i (a:b) = ((s1$$s2),(i2))@@ -238,7 +287,10 @@  -------------------------------------------------------------------------------- -ppPropertyL :: Int -> [Property] -> (Doc, Int)+-- | Pretty print a list of properties as a GraphViz graph part.+ppPropertyL :: Int         -- ^ Index or ID of the next node in the graph.+            -> [Property]  -- ^ List of properties to pretty print+            -> (Doc, Int) ppPropertyL i [] = (empty,i)  ppPropertyL i (a:b) = ((s1$$s2),(i2))@@ -248,7 +300,10 @@  -------------------------------------------------------------------------------- -ppSpecDot :: Int -> Spec -> (Doc, Int)+-- | Pretty-print a Copilot specification as a GraphViz/dot graph.+ppSpecDot :: Int        -- ^ Index or ID of the next node in the graph.+          -> Spec       -- ^ Spec to pretty print.+          -> (Doc, Int) ppSpecDot i spec =   ((aa $$ cs $$ ds $$ es $$ fs $$ bb),i4)   where@@ -261,14 +316,16 @@  -------------------------------------------------------------------------------- --- | Pretty-prints a Copilot expression.-prettyPrintExprDot :: Bool -> Expr a -> String+-- | Pretty-print a Copilot expression as a GraphViz/dot graph.+prettyPrintExprDot :: Bool     -- ^ Mark externs with the prefix @externV:@.+                   -> Expr a   -- ^ The expression to pretty print.+                   -> String prettyPrintExprDot bb s = render rr   where     (r1, _) = ppExprDot 1 0 bb s     rr = text "digraph G {\nnode [shape=box]\n" $$ (text "0 [label=\"file: \n?????\",color=red, style=filled]\n") <> r1 $$ text "\n}\n" --- | Pretty-prints a Copilot specification.+-- | Pretty-print a Copilot specification as a GraphViz/dot graph. prettyPrintDot :: Spec -> String prettyPrintDot s = render r1   where (r1, _) = ppSpecDot 0 s
src/Copilot/Core/PrettyPrint.hs view
@@ -20,11 +20,16 @@  -------------------------------------------------------------------------------- +-- | Create a unique stream name by prefixing the given ID by a lowercase+-- letter @"s"@. strmName :: Int -> Doc strmName id = text "s" <> int id  -------------------------------------------------------------------------------- +-- | Pretty-print a Copilot expression.+--+-- The type is ignored, and only the expression is pretty-printed. ppExpr :: Expr a -> Doc ppExpr e0 = case e0 of   Const t x                  -> text (showWithType Haskell t x)@@ -39,9 +44,13 @@   Op3 op e1 e2 e3            -> ppOp3 op (ppExpr e1) (ppExpr e2) (ppExpr e3)   Label _ s e                -> text "label "<> doubleQuotes (text s) <+> (ppExpr e) +-- | Pretty-print an untyped expression.+--+-- The type is ignored, and only the expression is pretty-printed. ppUExpr :: UExpr -> Doc ppUExpr UExpr { uExprExpr = e0 } = ppExpr e0 +-- | Pretty-print a unary operation. ppOp1 :: Op1 a b -> Doc -> Doc ppOp1 op = case op of   Not                     -> ppPrefix "not"@@ -68,6 +77,7 @@   GetField (Struct _) _ f -> \e -> ppInfix "#" e (text $ accessorname f)   GetField _ _ _          -> impossible "ppOp1" "Copilot.Core.PrettyPrint" +-- | Pretty-print a binary operation. ppOp2 :: Op2 a b c -> Doc -> Doc -> Doc ppOp2 op = case op of   And          -> ppInfix "&&"@@ -93,6 +103,7 @@   BwShiftR _ _ -> ppInfix ">>"   Index    _   -> ppInfix ".!!" +-- | Pretty-print a ternary operation. ppOp3 :: Op3 a b c d -> Doc -> Doc -> Doc -> Doc ppOp3 op = case op of   Mux _    -> \ doc1 doc2 doc3 ->@@ -102,14 +113,18 @@  -------------------------------------------------------------------------------- +-- | Parenthesize two 'Doc's, separated by an infix 'String'. ppInfix :: String -> Doc -> Doc -> Doc ppInfix cs doc1 doc2 = parens $ doc1 <+> text cs <+> doc2 +-- | Prefix a 'Doc' by a 'String'. ppPrefix :: String -> Doc -> Doc ppPrefix cs = (text cs <+>)  -------------------------------------------------------------------------------- +-- | Pretty-print a Copilot stream as a case of a top-level function for+-- streams of that type, by pattern matching on the stream name. ppStream :: Stream -> Doc ppStream   Stream@@ -130,6 +145,8 @@  -------------------------------------------------------------------------------- +-- | Pretty-print a Copilot trigger as a case of a top-level @trigger@+-- function, by pattern matching on the trigger name. ppTrigger :: Trigger -> Doc ppTrigger   Trigger@@ -146,6 +163,8 @@  -------------------------------------------------------------------------------- +-- | Pretty-print a Copilot observer as a case of a top-level @observer@+-- function, by pattern matching on the observer name. ppObserver :: Observer -> Doc ppObserver   Observer@@ -157,6 +176,8 @@  -------------------------------------------------------------------------------- +-- | Pretty-print a Copilot property as a case of a top-level @property@+-- function, by pattern matching on the property name. ppProperty :: Property -> Doc ppProperty   Property@@ -168,6 +189,12 @@  -------------------------------------------------------------------------------- +-- | Pretty-print a Copilot specification, in the following order:+--+-- - Streams definitions+-- - Trigger definitions+-- - Observer definitions+-- - Property definitions ppSpec :: Spec -> Doc ppSpec spec = cs $$ ds $$ es $$ fs   where@@ -178,7 +205,7 @@  -------------------------------------------------------------------------------- --- | Pretty-prints a Copilot specification.+-- | Pretty-print a Copilot specification. prettyPrint :: Spec -> String prettyPrint = render . ppSpec
src/Copilot/Core/Spec.hs view
@@ -5,6 +5,15 @@ {-# LANGUAGE Safe #-} {-# LANGUAGE ExistentialQuantification, GADTs #-} +-- | Copilot specifications constitute the main declaration of Copilot modules.+--+-- A specification normally contains the association between streams to monitor+-- and their handling functions, or streams to observe, or a theorem that must+-- be proved.+--+-- In order to be executed, high-level Copilot Language Spec must be turned+-- into Copilot Core's 'Spec'. This module defines the low-level Copilot Core+-- representations for Specs and the main types of element in a spec.. module Copilot.Core.Spec   ( Stream (..)   , Observer (..)@@ -19,7 +28,11 @@  -------------------------------------------------------------------------------- --- | A stream.+-- | A stream in an infinite succession of values of the same type.+--+-- Stream can carry different types of data. Boolean streams play a special+-- role: they are used by other parts (e.g., 'Trigger') to detect when the+-- properties being monitored are violated. data Stream = forall a. (Typeable a, Typed a) => Stream   { streamId         :: Id   , streamBuffer     :: [a]@@ -28,7 +41,8 @@  -------------------------------------------------------------------------------- --- | An observer.+-- | An observer, representing a stream that we observe during interpretation+-- at every sample. data Observer = forall a. Typeable a => Observer   { observerName     :: Name   , observerExpr     :: Expr a@@ -36,7 +50,8 @@  -------------------------------------------------------------------------------- --- | A trigger.+-- | A trigger, representing a function we execute when a boolean stream becomes+-- true at a sample. data Trigger = Trigger   { triggerName      :: Name   , triggerGuard     :: Expr Bool@@ -44,16 +59,16 @@  -------------------------------------------------------------------------------- --- | A property.+-- | A property, representing a boolean stream that is existentially or+-- universally quantified over time. data Property = Property   { propertyName     :: Name   , propertyExpr     :: Expr Bool }  -------------------------------------------------------------------------------- --- | A Copilot specification consists of a list of variables bound to anonymous--- streams, a list of anomymous streams, a list of observers, a list of--- triggers, and a list of structs.+-- | A Copilot specification is a list of streams, together with monitors on+-- these streams implemented as observers, triggers or properties. data Spec = Spec   { specStreams      :: [Stream]   , specObservers    :: [Observer]
src/Copilot/Core/Type.hs view
@@ -3,6 +3,12 @@ --------------------------------------------------------------------------------  -- | Typing for Core.+--+-- All expressions and streams in Core are accompanied by a representation of+-- the types of the underlying expressions used or carried by the streams.+-- This information is needed by the compiler to generate code, since it must+-- initialize variables and equivalent representations for those types in+-- the target languages.  {-# LANGUAGE Safe #-} {-# LANGUAGE  ExistentialQuantification@@ -46,18 +52,27 @@  import Data.List (intercalate) -+-- | The value of that is a product or struct, defined as a constructor with+-- several fields. class Struct a where+  -- | Returns the name of struct in the target language.   typename :: a -> String+  -- | Transforms all the struct's fields into a list of values.   toValues :: a -> [Value a] +-- | The field of a struct, together with a representation of its type. data Value a = forall s t. (Typeable t, KnownSymbol s, Show t) => Value (Type t) (Field s t) +-- | A field in a struct. The name of the field is a literal at the type+-- level. data Field (s :: Symbol) t = Field t +-- | Extract the name of a field. fieldname :: forall s t. KnownSymbol s => Field s t -> String fieldname _ = symbolVal (Proxy :: Proxy s) +-- | Extract the name of an accessor (a function that returns a field of a+-- struct). accessorname :: forall a s t. (Struct a, KnownSymbol s) => (a -> Field s t) -> String accessorname _ = symbolVal (Proxy :: Proxy s) @@ -69,7 +84,12 @@     fields = intercalate "," $ map showfield (toValues t)     showfield (Value _ field) = show field -+-- | A Type representing the types of expressions or values handled by+-- Copilot Core.+--+-- Note that both arrays and structs use dependently typed features. In the+-- former, the length of the array is part of the type. In the latter, the+-- names of the fields are part of the type. data Type :: * -> * where   Bool    :: Type Bool   Int8    :: Type Int8@@ -89,11 +109,11 @@                          ) => Type t -> Type (Array n t)   Struct  :: (Typed a, Struct a) => a -> Type a --- Get the length of an array from its type+-- | Return the length of an array from its type tylength :: forall n t. KnownNat n => Type (Array n t) -> Int tylength _ = fromIntegral $ natVal (Proxy :: Proxy n) --- Get the total (nested) size of an array from its type+-- | Return the total (nested) size of an array from its type tysize :: forall n t. KnownNat n => Type (Array n t) -> Int tysize ty@(Array ty'@(Array _)) = tylength ty * tysize ty' tysize ty@(Array _            ) = tylength ty@@ -114,6 +134,9 @@  -------------------------------------------------------------------------------- +-- | A simple, monomorphic representation of types that facilitates putting+-- variables in heterogeneous lists and environments in spite of their types+-- being different. data SimpleType where   SBool   :: SimpleType   SInt8   :: SimpleType@@ -129,7 +152,10 @@   SArray  :: Type t -> SimpleType   SStruct :: SimpleType +-- | Type equality, used to help type inference.+ {- This instance is necessary, otherwise the type of SArray can't be inferred -}+ instance Eq SimpleType where   SBool   == SBool    = True   SInt8   == SInt8    = True@@ -149,6 +175,8 @@  -------------------------------------------------------------------------------- +-- | A typed expression, from which we can obtain the two type representations+-- used by Copilot: 'Type' and 'SimpleType'. class (Show a, Typeable a) => Typed a where   typeOf     :: Type a   simpleType :: Type a -> SimpleType
src/Copilot/Core/Type/Array.hs view
@@ -30,12 +30,15 @@ import GHC.TypeLits     (Nat, KnownNat, natVal) import Data.Proxy       (Proxy (..)) +-- | Implementation of an array that uses type literals to store length. data Array (n :: Nat) t where   Array :: [t] -> Array n t  instance Show t => Show (Array n t) where   show (Array xs) = show xs +-- | Smart array constructor that only type checks if the length of the given+-- list matches the length of the array at type level. array :: forall n t. KnownNat n => [t] -> Array n t array xs | datalen == typelen = Array xs          | otherwise          = error errmsg where@@ -45,26 +48,31 @@            ") does not match length of type (" ++ show typelen ++ ")."  +-- | Association between an array and the type of the elements it contains. type family InnerType x where   InnerType (Array _ x) = InnerType x   InnerType x           = x -+-- | Flattening or conversion of arrays to lists. class Flatten a b where+  -- | Flatten an array to a list.   flatten :: Array n a -> [b] +-- | Flattening of plain arrays. instance Flatten a a where   flatten (Array xs) = xs +-- | Flattening of nested arrays. instance Flatten a b => Flatten (Array n a) b where   flatten (Array xss) = concat $ map flatten xss  instance Foldable (Array n) where   foldr f base (Array xs) = foldr f base xs -+-- | Total number of elements in a possibly nested array. size :: forall a n b. (Flatten a b, b ~ InnerType a) => Array n a -> Int size xs = length $ (flatten xs :: [b]) +-- | Return the elemts of an array. arrayelems :: Array n a -> [a] arrayelems (Array xs) = xs
src/Copilot/Core/Type/Dynamic.hs view
@@ -28,24 +28,32 @@  -------------------------------------------------------------------------------- +-- | Representation of a value accompanied by its type. data Dynamic :: (* -> *) -> * where   Dynamic :: a -> t a -> Dynamic t +-- | Representation of a function accompanied by its type. data DynamicF :: (* -> *) -> (* -> *) -> * where   DynamicF :: f a -> t a -> DynamicF f t +-- | Enclose a value and its type in a container. toDyn :: t a -> a -> Dynamic t toDyn t x = Dynamic x t +-- | Extract a value from a dynamic. Return 'Nothing' if the value is not of+-- the given type. fromDyn :: EqualType t => t a -> Dynamic t -> Maybe a fromDyn t1 (Dynamic x t2) =   case t1 =~= t2 of     Just Refl -> return x     Nothing   -> Nothing +-- | Enclose a function and its type in a container. toDynF :: t a -> f a -> DynamicF f t toDynF t fx = DynamicF fx t +-- | Extract a value from a dynamic function container. Return 'Nothing' if+-- the value is not of the given type. fromDynF :: EqualType t => t a -> DynamicF f t -> Maybe (f a) fromDynF t1 (DynamicF fx t2) =   case t1 =~= t2 of
src/Copilot/Core/Type/Equality.hs view
@@ -5,6 +5,7 @@ {-# LANGUAGE Safe #-} {-# LANGUAGE GADTs, KindSignatures #-} +-- | Propositional equality and type equality. module Copilot.Core.Type.Equality   ( Equal (..)   , EqualType (..)@@ -15,23 +16,31 @@   , cong   ) where +-- | Propositional equality. data Equal :: * -> * -> * where   Refl :: Equal a a +-- | Type equality. If the value of @x =~= y@ is @Just Refl@, then the two+-- types @x@ and @y@ are equal. class EqualType t where   (=~=) :: t a -> t b -> Maybe (Equal a b) +-- | Safe coercion, which requires proof of equality. coerce :: Equal a b -> a -> b coerce Refl x = x +-- | Proof of propositional equality. refl :: Equal a a refl = Refl +-- | Symmetry. symm :: Equal a b -> Equal b a symm Refl = Refl +-- | Transitivity. trans :: Equal a b -> Equal b c -> Equal a c trans Refl Refl = Refl +-- | Congruence. cong :: Equal a b -> Equal (f a) (f b) cong Refl = Refl
src/Copilot/Core/Type/Show.hs view
@@ -5,6 +5,7 @@ {-# LANGUAGE Safe #-} {-# LANGUAGE ExistentialQuantification, GADTs #-} +-- | Show Copilot Core types and typed values. module Copilot.Core.Type.Show   ( ShowWit (..)   , showWit@@ -17,10 +18,12 @@  -------------------------------------------------------------------------------- +-- | Witness datatype for showing a value, used by 'showWithType'. data ShowWit a = Show a => ShowWit  -------------------------------------------------------------------------------- +-- | Turn a type into a show witness. showWit :: Type a -> ShowWit a showWit t =   case t of@@ -40,6 +43,7 @@  -------------------------------------------------------------------------------- +-- | Show Copilot Core type. showType :: Type a -> String showType t =   case t of@@ -61,10 +65,15 @@  -- Are we proving equivalence with a C backend, in which case we want to show -- Booleans as '0' and '1'.++-- | Target language for showing a typed value. Used to adapt the+-- representation of booleans. data ShowType = C | Haskell  -------------------------------------------------------------------------------- +-- | Show a value. The representation depends on the type and the target+-- language. Booleans are represented differently depending on the backend. showWithType :: ShowType -> Type a -> a -> String showWithType showT t x =   case showT of@@ -73,7 +82,7 @@                    _    -> sw     Haskell   -> case t of                    Bool -> if x then "true" else "false"-                   _    -> sw                   +                   _    -> sw   where   sw = case showWit t of          ShowWit -> show x
src/Copilot/Core/Type/Uninitialized.hs view
@@ -2,7 +2,7 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- --- | Initial values for give types.+-- | Initial values for a given type.  {-# LANGUAGE Safe #-} {-# LANGUAGE GADTs #-}@@ -15,6 +15,9 @@  -------------------------------------------------------------------------------- +-- | Initial value for a given type.+--+-- Does not support structs or arrays. uninitialized :: Type a -> a uninitialized t =   case t of