diff --git a/CHANGELOG b/CHANGELOG --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,7 @@ +2021-03-05 + * Version bump (3.2.1). (#31) + * Completed the documentation. (#22) + 2020-12-06 Ivan Perez * Version bump (3.2). * Fixed implementation of tysize for n-dimensional arrays. (#20). diff --git a/copilot-core.cabal b/copilot-core.cabal --- a/copilot-core.cabal +++ b/copilot-core.cabal @@ -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. diff --git a/src/Copilot/Core.hs b/src/Copilot/Core.hs --- a/src/Copilot/Core.hs +++ b/src/Copilot/Core.hs @@ -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/\", diff --git a/src/Copilot/Core/Error.hs b/src/Copilot/Core/Error.hs --- a/src/Copilot/Core/Error.hs +++ b/src/Copilot/Core/Error.hs @@ -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 " -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 diff --git a/src/Copilot/Core/Expr.hs b/src/Copilot/Core/Expr.hs --- a/src/Copilot/Core/Expr.hs +++ b/src/Copilot/Core/Expr.hs @@ -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 } diff --git a/src/Copilot/Core/External.hs b/src/Copilot/Core/External.hs --- a/src/Copilot/Core/External.hs +++ b/src/Copilot/Core/External.hs @@ -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` diff --git a/src/Copilot/Core/Interpret.hs b/src/Copilot/Core/Interpret.hs --- a/src/Copilot/Core/Interpret.hs +++ b/src/Copilot/Core/Interpret.hs @@ -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 diff --git a/src/Copilot/Core/Interpret/Eval.hs b/src/Copilot/Core/Interpret/Eval.hs --- a/src/Copilot/Core/Interpret/Eval.hs +++ b/src/Copilot/Core/Interpret/Eval.hs @@ -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)] diff --git a/src/Copilot/Core/Interpret/Render.hs b/src/Copilot/Core/Interpret/Render.hs --- a/src/Copilot/Core/Interpret/Render.hs +++ b/src/Copilot/Core/Interpret/Render.hs @@ -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) diff --git a/src/Copilot/Core/Locals.hs b/src/Copilot/Core/Locals.hs --- a/src/Copilot/Core/Locals.hs +++ b/src/Copilot/Core/Locals.hs @@ -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 diff --git a/src/Copilot/Core/MakeTags.hs b/src/Copilot/Core/MakeTags.hs --- a/src/Copilot/Core/MakeTags.hs +++ b/src/Copilot/Core/MakeTags.hs @@ -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 #-} diff --git a/src/Copilot/Core/Operators.hs b/src/Copilot/Core/Operators.hs --- a/src/Copilot/Core/Operators.hs +++ b/src/Copilot/Core/Operators.hs @@ -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 diff --git a/src/Copilot/Core/PrettyDot.hs b/src/Copilot/Core/PrettyDot.hs --- a/src/Copilot/Core/PrettyDot.hs +++ b/src/Copilot/Core/PrettyDot.hs @@ -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 +-- 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 +-- 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 diff --git a/src/Copilot/Core/PrettyPrint.hs b/src/Copilot/Core/PrettyPrint.hs --- a/src/Copilot/Core/PrettyPrint.hs +++ b/src/Copilot/Core/PrettyPrint.hs @@ -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 diff --git a/src/Copilot/Core/Spec.hs b/src/Copilot/Core/Spec.hs --- a/src/Copilot/Core/Spec.hs +++ b/src/Copilot/Core/Spec.hs @@ -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] diff --git a/src/Copilot/Core/Type.hs b/src/Copilot/Core/Type.hs --- a/src/Copilot/Core/Type.hs +++ b/src/Copilot/Core/Type.hs @@ -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 diff --git a/src/Copilot/Core/Type/Array.hs b/src/Copilot/Core/Type/Array.hs --- a/src/Copilot/Core/Type/Array.hs +++ b/src/Copilot/Core/Type/Array.hs @@ -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 diff --git a/src/Copilot/Core/Type/Dynamic.hs b/src/Copilot/Core/Type/Dynamic.hs --- a/src/Copilot/Core/Type/Dynamic.hs +++ b/src/Copilot/Core/Type/Dynamic.hs @@ -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 diff --git a/src/Copilot/Core/Type/Equality.hs b/src/Copilot/Core/Type/Equality.hs --- a/src/Copilot/Core/Type/Equality.hs +++ b/src/Copilot/Core/Type/Equality.hs @@ -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 diff --git a/src/Copilot/Core/Type/Show.hs b/src/Copilot/Core/Type/Show.hs --- a/src/Copilot/Core/Type/Show.hs +++ b/src/Copilot/Core/Type/Show.hs @@ -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 diff --git a/src/Copilot/Core/Type/Uninitialized.hs b/src/Copilot/Core/Type/Uninitialized.hs --- a/src/Copilot/Core/Type/Uninitialized.hs +++ b/src/Copilot/Core/Type/Uninitialized.hs @@ -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