copilot-core 3.13 → 3.14

raw patch · 10 files changed

+15/−965 lines, 10 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG +7/−2
• copilot-core.cabal +1/−5
• src/Copilot/Core.hs +1/−2
• src/Copilot/Core/Error.hs +0/−6
• src/Copilot/Core/Interpret.hs +0/−35
• src/Copilot/Core/Interpret/Eval.hs +0/−352
• src/Copilot/Core/Interpret/Render.hs +0/−127
• src/Copilot/Core/PrettyDot.hs +0/−306
• src/Copilot/Core/Type/Array.hs +5/−42
• tests/Test/Copilot/Core/Type/Array.hs +1/−88

@@ -1,9 +1,14 @@+2023-03-07+        * Version bump (3.14). (#422)+        * Remove Copilot.Core.PrettyDot. (#409)+        * Fix formatting error in CHANGELOG. (#414)+        * Remove module space Copilot.Core.Interpret. (#410)+        * Remove unused definitions from Copilot.Core.Type.Array. (#411)+ 2023-01-07         * Version bump (3.13). (#406)         * Implement missing cases of type equality for arrays and structs.           (#400)--2022-12-27         * Remove Copilot.Core.External. (#391)         * Fix bug in definition of simpleType for Int8. (#393)         * Hide module Copilot.Core.Type.Show. (#392)

@@ -1,6 +1,6 @@ cabal-version:       >=1.10 name:                copilot-core-version:             3.13+version:             3.14 synopsis:            An intermediate representation for Copilot. description:   Intermediate representation for Copilot.@@ -49,20 +49,16 @@      Copilot.Core     Copilot.Core.Expr-    Copilot.Core.Interpret-    Copilot.Core.Interpret.Eval     Copilot.Core.Operators     Copilot.Core.Spec     Copilot.Core.Type     Copilot.Core.Type.Array     Copilot.Core.Type.Equality     Copilot.Core.PrettyPrint-    Copilot.Core.PrettyDot    other-modules:      Copilot.Core.Error-    Copilot.Core.Interpret.Render     Copilot.Core.Type.Show  test-suite unit-tests

@@ -16,8 +16,7 @@ -- Electronic Notes in Theoretical Computer Science vol. 174, p. 23-39, 2007. -- -- For examples of how to traverse a Copilot specification see--- the source code of the interpreter--- ("Copilot.Core.Interpret")+-- the source code of the interpreter (@copilot-interpreter@) -- and the pretty-printer -- ("Copilot.Core.PrettyPrint"). module Copilot.Core

@@ -5,7 +5,6 @@ -- Copyright:   (c) 2011 National Institute of Aerospace / Galois, Inc. module Copilot.Core.Error     ( impossible-    , badUsage     )   where @@ -19,8 +18,3 @@     ++ ". Please file an issue at "     ++ "https://github.com/Copilot-Language/copilot/issues"     ++ "or email the maintainers at <ivan.perezdominguez@nasa.gov>"---- | 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

@@ -1,35 +0,0 @@--- The following warning is enabled in this module so that the import of--- Copilot.Core.Interpret.Eval and Render do not give rise to warnings.-{-# OPTIONS_GHC -fno-warn-deprecations #-}---- Copyright © 2011 National Institute of Aerospace / Galois, Inc.---- | An interpreter for Copilot specifications.--{-# LANGUAGE Safe #-}--module Copilot.Core.Interpret-  {-# DEPRECATED "This module is deprecated in Copilot 3.11. Use copilot-interpreter instead." #-}-  ( Format (..)-  , interpret-  ) where--import Copilot.Core-import Copilot.Core.Interpret.Eval-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---- | 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-    CSV   -> renderAsCSV e-  where-    e = eval Haskell k spec

@@ -1,352 +0,0 @@--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.---- | A tagless interpreter for Copilot specifications.--{-# LANGUAGE BangPatterns       #-}-{-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE GADTs              #-}-{-# LANGUAGE Safe               #-}--module Copilot.Core.Interpret.Eval-  {-# DEPRECATED "This module is deprecated in Copilot 3.11. Use copilot-interpreter instead." #-}-  ( Env-  , Output-  , ExecTrace (..)-  , eval-  , ShowType (..)-  ) where--import Copilot.Core           (Expr (..), Field (..), Id, Name, Observer (..),-                               Op1 (..), Op2 (..), Op3 (..), Spec, Stream (..),-                               Trigger (..), Type (Struct), UExpr (..),-                               arrayelems, specObservers, specStreams,-                               specTriggers)-import Copilot.Core.Error     (badUsage)-import Copilot.Core.Type.Show (ShowType (..), showWithType)--import           Prelude hiding (id)-import qualified Prelude as P--import Control.Exception (Exception, throw)-import Data.Bits         (complement, shiftL, shiftR, xor, (.&.), (.|.))-import Data.Dynamic      (Dynamic, fromDynamic, toDyn)-import Data.List         (transpose)-import Data.Maybe        (fromJust)-import Data.Typeable     (Typeable)---- | Exceptions that may be thrown during interpretation of a Copilot--- specification.-data InterpException-  = 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.-  | 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 (ArrayWrongSize name expectedSize)                                      =-    badUsage $ "in the environment for external array " ++ name-      ++ ", we expect a list of length " ++ show expectedSize-      ++ ", but the length of the array you supplied is of a different length."-  ----------------------------------------  show (ArrayIdxOutofBounds name index size)                                   =-    badUsage $ "in the environment for external array " ++ name-      ++ ", you gave an index of " ++ show index-      ++ " where the size of the array is " ++ show size ++ "; the size must "-      ++ " be strictly greater than the index."-  ----------------------------------------  show DivideByZero                                                            =-    badUsage "divide by zero."-  ----------------------------------------  show (NotEnoughValues name k)                                                =-    badUsage $ "on the " ++ show k ++ "th iteration, we ran out of "-      ++ "values for simulating the external element " ++ name ++ "."-  ----------------------------------------  show (NoExtsInterp name)                                                     =-    badUsage $ "in a call of external symbol " ++ name ++ ", you did not "-      ++ "provide an expression for interpretation.  In your external "-      ++ "declaration, you need to provide a 'Just strm', where 'strm' is "-      ++ "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)]---- | 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-  { interpTriggers  :: [(String, [Maybe [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---- 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.---- | 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 initStrms = map initStrm (specStreams spec)             in--  let strms = evalStreams k (specStreams spec) initStrms      in--  let trigs = map (evalTrigger showType k strms)-                  (specTriggers spec)                         in--  let obsvs = map (evalObserver showType k strms)-                  (specObservers spec)                        in--  strms `seq` ExecTrace-                { interpTriggers  =-                    zip (map triggerName  (specTriggers  spec)) trigs-                , interpObservers =-                    zip (map observerName (specObservers spec)) obsvs-                }---- | 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-  Drop t i id                        ->-    let Just buff = lookup id strms >>= fromDynamic in-    reverse buff !! (fromIntegral i + k)-  Local t1 _ name e1 e2              ->-    let x     = evalExpr_ k e1 locs strms in-    let locs' = (name, toDyn x) : locs  in-    x `seq` locs' `seq` evalExpr_ k e2  locs' strms-  Var t name                         -> fromJust $ lookup name locs >>= fromDynamic-  ExternVar _ name xs                -> evalExternVar k name xs-  Op1 op e1                          ->-    let ev1 = evalExpr_ k e1 locs strms in-    let op1 = evalOp1 op                in-    ev1 `seq` op1 `seq` op1 ev1-  Op2 op e1 e2                       ->-    let ev1 = evalExpr_ k e1 locs strms in-    let ev2 = evalExpr_ k e2 locs strms in-    let op2 = evalOp2 op                in-    ev1 `seq` ev2 `seq` op2 `seq` op2 ev1 ev2-  Op3 op e1 e2 e3                    ->-    let ev1 = evalExpr_ k e1 locs strms in-    let ev2 = evalExpr_ k e2 locs strms in-    let ev3 = evalExpr_ k e3 locs strms in-    let op3 = evalOp3 op                in-    ev1 `seq` ev2 `seq` ev3 `seq` op3 `seq` op3 ev1 ev2 ev3-  Label _ _ e1                         ->-    let ev1 = evalExpr_ k e1 locs strms in-    ev1---- | 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-    Nothing -> throw (NoExtsInterp name)-    Just xs ->-      case safeIndex k xs of-        Nothing -> throw (NotEnoughValues name k)-        Just x  -> x---- | 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-    Abs _      -> P.abs-    Sign _     -> P.signum-    Recip _    -> P.recip-    Exp _      -> P.exp-    Sqrt _     -> P.sqrt-    Log _      -> P.log-    Sin _      -> P.sin-    Tan _      -> P.tan-    Cos _      -> P.cos-    Asin _     -> P.asin-    Atan _     -> P.atan-    Acos _     -> P.acos-    Sinh _     -> P.sinh-    Tanh _     -> P.tanh-    Cosh _     -> P.cosh-    Asinh _    -> P.asinh-    Atanh _    -> P.atanh-    Acosh _    -> P.acosh-    Ceiling _  -> P.fromIntegral . idI . P.ceiling-    Floor _    -> P.fromIntegral . idI . P.floor-    BwNot _    -> complement-    Cast _ _   -> P.fromIntegral-    GetField (Struct _) _ f -> unfield . f-  where-    -- Used to help GHC pick a return type for ceiling/floor-    idI :: Integer -> Integer-    idI = P.id--    -- Extract value from field-    unfield (Field v) = v---- | 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          -> (&&)-  Or           -> (||)-  Add _        -> (+)-  Sub _        -> (-)-  Mul _        -> (*)-  Mod _        -> (catchZero P.mod)-  Div _        -> (catchZero P.quot)-  Fdiv _       -> (P./)-  Pow _        -> (P.**)-  Logb _       -> P.logBase-  Atan2 _      -> P.atan2-  Eq _         -> (==)-  Ne _         -> (/=)-  Le _         -> (<=)-  Ge _         -> (>=)-  Lt _         -> (<)-  Gt _         -> (>)-  BwAnd _      -> (.&.)-  BwOr  _      -> (.|.)-  BwXor _      -> (xor)-  BwShiftL _ _ -> ( \ !a !b -> shiftL a $! fromIntegral b )-  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))---- | 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-  evalStreams_ k strms | k == top  = strms-  evalStreams_ k strms | otherwise =-    evalStreams_ (k+1) $! strms_-    where-    strms_ = map evalStream specStrms-    evalStream Stream { streamId       = id-                      , streamExpr     = e-                      , streamExprType = t } =-      let xs = fromJust $ lookup id strms >>= fromDynamic      in-      let x  = evalExpr_ k e [] strms                          in-      let ls = x `seq` (x:xs)                                  in-      (id, toDyn ls)---- | 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-    , triggerArgs  = args-    } = map tag (zip bs vs)--  where-  tag :: (Bool, a) -> Maybe a-  tag (True,  x) = Just x-  tag (False, _) = Nothing--  -- Is the guard true?-  bs :: [Bool]-  bs = evalExprs_ k e strms--  -- The argument outputs.-  vs :: [[Output]]-  vs = if null args then replicate k []  -- might be 0 args.-         else transpose $ map evalUExpr args--  evalUExpr :: UExpr -> [Output]-  evalUExpr (UExpr t e1) =-    map (showWithType showType t) (evalExprs_ k e1 strms)---- | 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-    , observerExprType = t }-  = map (showWithType showType t) (evalExprs_ k e strms)---- | 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)]---- | Safe indexing (!!) on possibly infininite lists.-safeIndex :: Int -> [a] -> Maybe a-safeIndex i ls =-  let ls' = take (i+1) ls in-  if length ls' > i then Just (ls' !! i)-    else Nothing

@@ -1,127 +0,0 @@--- The following warning is enabled in this module so that the import of--- Copilot.Core.Interpret.Eval does not give rise to a warning.-{-# OPTIONS_GHC -fno-warn-deprecations #-}---- Copyright © 2011 National Institute of Aerospace / Galois, Inc.---- | Pretty-print the results of a simulation.--{-# LANGUAGE Safe #-}--module Copilot.Core.Interpret.Render-  {-# DEPRECATED "This module is deprecated in Copilot 3.11. Use copilot-interpreter instead." #-}-  ( renderAsTable-  , renderAsCSV-  ) where--import Data.List (intersperse, transpose, foldl')-import Data.Maybe (catMaybes)-import Copilot.Core.Interpret.Eval (Output, ExecTrace (..))-import Text.PrettyPrint--import Prelude hiding ((<>))---- | Render an execution trace as a table, formatted to faciliate readability.-renderAsTable :: ExecTrace -> String-renderAsTable-  ExecTrace-    { interpTriggers  = trigs-    , interpObservers = obsvs } = ( render-                                  . asColumns-                                  . transpose-                                  . (:) (ppTriggerNames ++ ppObserverNames)-                                  . transpose-                                  ) (ppTriggerOutputs ++ ppObserverOutputs)-     where--     ppTriggerNames :: [Doc]-     ppTriggerNames  = map (text . (++ ":")) (map fst trigs)--     ppObserverNames :: [Doc]-     ppObserverNames = map (text . (++ ":")) (map fst obsvs)--     ppTriggerOutputs :: [[Doc]]-     ppTriggerOutputs = map (map ppTriggerOutput) (map snd trigs)--     ppTriggerOutput :: Maybe [Output] -> Doc-     ppTriggerOutput (Just vs) = text $ "(" ++ concat (intersperse "," vs) ++ ")"-     ppTriggerOutput Nothing   = text "--"--     ppObserverOutputs :: [[Doc]]-     ppObserverOutputs = map (map text) (map snd obsvs)---- | 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-       } =-  if null trigs then (empty, Nothing)-    else (foldl' ($$) empty (text "#" : ppTriggerOutputs), tails)--  where--  ppTriggerOutputs :: [Doc]-  ppTriggerOutputs =-      catMaybes-    . fmap ppTriggerOutput-    . map (fmap head)-    $ trigs--  ppTriggerOutput :: (String, Maybe [Output]) -> Maybe Doc-  ppTriggerOutput (_,  Nothing) = Nothing-  ppTriggerOutput (cs, Just xs) = Just $-    text cs <> text "," <>-      (foldr (<>) empty . map text . intersperse ",") xs--  tails :: Maybe ExecTrace-  tails =-    if any null (fmap (tail.snd) trigs)-      then Nothing-      else Just-        ExecTrace-          { interpTriggers  = map (fmap tail) trigs-          , interpObservers = []-          }---- Copied from pretty-ncols because of incompatibility with newer GHC versions.-asColumns :: [[Doc]] -> Doc-asColumns = flip asColumnsWithBuff $ 1--asColumnsWithBuff :: [[Doc]] -> Int -> Doc-asColumnsWithBuff lls q = normalize-        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---- | 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-        where-          buf x = x <> (hcat $ replicate q space) <> (hcat $ replicate (mx - (docLen x)) space)

@@ -1,306 +0,0 @@--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.---- | A pretty printer for Copilot specifications as GraphViz/dot graphs.--{-# LANGUAGE GADTs #-}-{-# LANGUAGE Safe  #-}--module Copilot.Core.PrettyDot-  {-# DEPRECATED "This module is deprecated in Copilot 3.11." #-}-  ( prettyPrintDot-  , prettyPrintExprDot-  ) where--import Copilot.Core-import Copilot.Core.Type.Show (showWithType, ShowType(..), showType)-import Prelude hiding (id, (<>))-import Text.PrettyPrint.HughesPJ-import Data.List (intersperse)-import Text.Printf---- | Create a temporary/internal name from an extern variable name.-mkExtTmpVar :: String -> String-mkExtTmpVar = ("ext_" ++)---- | 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)-  Drop _ 0 id                -> (text (printf "%s [label=\"stream: %s\",color=crimson, style=filled]\n" (show ii::String) (show id::String) )-                  <> 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)))-                  ,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-                                in (text (printf "%s [label=\"local:\",color=blue, style=filled]\n" (show ii::String) )-                  <> text (printf "%s -> %s\n" (show pere::String) (show ii::String))-                  <> text (printf "%s [label=\"def: %s\",color=blue, style=filled]\n" ((show $ ii+1)::String) (name::String) )-                  <> text (printf "%s -> %s\n" (show ii::String) (show $ ii+1::String))-                  <> r1-                  <> r2, i2)--  Var _ name                 -> (text (printf "%s [label=\"var: %s\",color=blue, style=filled]\n" (show ii::String) (name::String) )-                  <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)),ii+1)--  Op1 op e                   -> let (r1,i1) = ppExprDot (ii+1) ii bb e-           in (text (printf "%s [label=\"op1: %s\",color=green4, style=filled]\n" (show ii::String) (ppOp1 op::String))-                  <> text (printf "%s -> %s\n" (show pere::String) (show ii::String))-                  <> r1,i1)--  Op2 op e1 e2               -> let (r1,i1) = ppExprDot (ii+1) ii bb e1-                                in let (r2,i2) = ppExprDot i1 ii bb e2-           in (text (printf "%s [label=\"op2: %s\",color=green4, style=filled]\n" (show ii::String) (ppOp2 op::String))-                  <> text (printf "%s -> %s\n" (show pere::String) (show ii::String))-                  <> r1-                  <> r2, i2)-  Op3 op e1 e2 e3            -> let (r1,i1) = ppExprDot (ii+1) ii bb e1-                                in let (r2,i2) = ppExprDot i1 ii bb e2-                                in let (r3,i3) = ppExprDot i2 ii bb e3-           in (text (printf "%s [label=\"op3: %s\",color=green4, style=filled]\n" (show ii::String) (ppOp3 op::String))-                  <> text (printf "%s -> %s\n" (show pere::String) (show ii::String))-                  <> r1-                  <> r2-                  <> r3, i3)--  Label _ s e                -> let (r1,i1) = ppExprDot (ii+1) ii bb e-           in (text (printf "%s [label=\"label: %s\",color=plum, style=filled]\n" (show ii::String) (s::String))-                  <> text (printf "%s -> %s\n" (show pere::String) (show ii::String))-                  <> r1,i1)---- | 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"-  Abs _     -> "abs"-  Sign _    -> "signum"-  Recip _   -> "recip"-  Exp _     -> "exp"-  Sqrt _    -> "sqrt"-  Log _     -> "log"-  Sin _     -> "sin"-  Tan _     -> "tan"-  Cos _     -> "cos"-  Asin _    -> "asin"-  Atan _    -> "atan"-  Acos _    -> "acos"-  Sinh _    -> "sinh"-  Tanh _    -> "tanh"-  Cosh _    -> "cosh"-  Asinh _   -> "asinh"-  Atanh _   -> "atanh"-  Acosh _   -> "acosh"-  Ceiling _ -> "ceiling"-  Floor _   -> "floor"-  BwNot _   -> "~"-  Cast _ _  -> "(cast)"---- | Pretty print a binary operator.-ppOp2 :: Op2 a b c -> String-ppOp2 op = case op of-  And          -> "&&"-  Or           -> "||"-  Add      _   -> "+"-  Sub      _   -> "-"-  Mul      _   -> "*"-  Div      _   -> "div"-  Mod      _   -> "mod"-  Fdiv     _   -> "/"-  Pow      _   -> "**"-  Logb     _   -> "logBase"-  Atan2    _   -> "atan2"-  Eq       _   -> "=="-  Ne       _   -> "/="-  Le       _   -> "<="-  Ge       _   -> ">="-  Lt       _   -> "<"-  Gt       _   -> ">"-  BwAnd    _   -> "&"-  BwOr     _   -> "|"-  BwXor    _   -> "^"-  BwShiftL _ _ -> "<<"-  BwShiftR _ _ -> ">>"---- | Pretty print a ternary operator.-ppOp3 :: Op3 a b c d -> String-ppOp3 op = case op of-  Mux _    -> "mux"---- | 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-    , streamBuffer   = buffer-    , streamExpr     = e-    , streamExprType = t-    }-      =-  (text (printf "%s [label=\"stream: %s\ntype: %s\",color=mediumblue, style=filled]\n" (show i::String) (show id::String) (showType t::String))-    <> text (printf "%s [label=\"++\",color=yellow, style=filled]\n" ((show $ i+1)::String))-    <> text (printf "%s -> %s\n" (show i::String) ((show $ i+1)::String))-    <> text (printf "%s [label=\"[%s]\",color=green, style=filled]\n" ((show $ i+2)::String) ((concat $ intersperse "," $ map (showWithType Haskell t) buffer )) ::String)-    <> text (printf "%s -> %s\n" (show (i+1)::String) ((show $ i+2)::String))-    <> r1, i1)-    where-      (r1, i1) = ppExprDot (i+3) (i+1) True e---- | 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-    , triggerGuard = e-    , triggerArgs  = args }-  =  ( text (printf "%s [label=\"trigger: %s\",color=mediumblue, style=filled]\n" (show i::String) (name::String) )-  <> text (printf "%s [label=\"guard\",color=yellow, style=filled]\n" ((show $ i+1)::String))-  <> text (printf "%s -> %s\n" (show i::String) ((show $ i+1)::String))-  <> r1-  <> text (printf "%s [label=\"args\",color=yellow, style=filled]\n" (show i1::String))-  <> text (printf "%s -> %s\n" (show i::String) (show i1::String))-  <>  (vcat (r2))-  ,i2)-  where-    (r1, i1) = ppExprDot (i+2) (i+1) True e-    (r2, i2) = ppUExprL (i1+1) (i1) True args---- | 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)-  where-    (r1, i1) = ppUExpr i pere bb a-    (r2, i2) = ppUExprL i1 pere bb b---- | 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-    , observerExpr     = e }-  =-  (text (printf "%s [label=\"observer: \n%s\",color=mediumblue, style=filled]\n" (show i::String) name::String)-  <> r1, i1)-  where-    (r1, i1) = ppExprDot (i+1) i True e---- | 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-    , propertyExpr     = e }-  =-  (text (printf "%s [label=\"property: \n%s\",color=mediumblue, style=filled]\n" (show i::String) name::String)-  <> r1, i1)-  where-    (r1, i1) = ppExprDot (i+1) i True e---- | 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))-  where-    (s1,i1) = ppStream i a-    (s2,i2) = ppStreamL i1 b---- | 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))-  where-    (s1,i1) = ppTrigger i a-    (s2,i2) = ppTriggerL i1 b---- | 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))-  where-    (s1,i1) = ppObserver i a-    (s2,i2) = ppObserverL i1 b---- | 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))-  where-    (s1,i1) = ppProperty i a-    (s2,i2) = ppPropertyL i1 b---- | 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-    aa = text "digraph G {\nnode [shape=box]\n"-    (cs, i1) = ppStreamL i    (specStreams    spec)-    (ds, i2) = ppTriggerL i1  (specTriggers   spec)-    (es, i3) = ppObserverL i2 (specObservers  spec)-    (fs, i4) = ppPropertyL i3 (specProperties spec)-    bb = text "\n}\n"---- | 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-print a Copilot specification as a GraphViz/dot graph.-prettyPrintDot :: Spec -> String-prettyPrintDot s = render r1-  where-    (r1, _) = ppSpecDot 0 s

@@ -1,11 +1,8 @@-{-# LANGUAGE DataKinds             #-}-{-# LANGUAGE FlexibleInstances     #-}-{-# LANGUAGE GADTs                 #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE Safe                  #-}-{-# LANGUAGE ScopedTypeVariables   #-}-{-# LANGUAGE TypeFamilies          #-}-{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE GADTs               #-}+{-# LANGUAGE Safe                #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies        #-}  -- | -- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.@@ -16,10 +13,6 @@ module Copilot.Core.Type.Array     ( Array     , array-    , flatten-    , size-    , Flatten-    , InnerType     , arrayelems     )   where@@ -45,36 +38,6 @@     typelen = fromIntegral $ natVal (Proxy :: Proxy n)     errmsg = "Length of data (" ++ show datalen ++              ") does not match length of type (" ++ show typelen ++ ")."---- | Association between an array and the type of the elements it contains.-{-# DEPRECATED InnerType "This type family is deprecated in Copilot 3.11." #-}-type family InnerType x where-  InnerType (Array _ x) = InnerType x-  InnerType x           = x---- | Flattening or conversion of arrays to lists.-{-# DEPRECATED Flatten "This class is deprecated in Copilot 3.11." #-}-{-# DEPRECATED flatten "This function is deprecated in Copilot 3.11." #-}-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---- | This instance is deprecated in Copilot 3.11.-instance Foldable (Array n) where-  foldr f base (Array xs) = foldr f base xs---- | Total number of elements in a possibly nested array.-{-# DEPRECATED size "This function is deprecated in Copilot 3.11." #-}-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]

@@ -13,7 +13,7 @@                                              vectorOf)  -- Internal imports: library modules being tested-import Copilot.Core.Type.Array (Array, array, arrayelems, flatten, size)+import Copilot.Core.Type.Array (Array, array, arrayelems)  -- | All unit tests for copilot-core:Copilot.Core.Array. tests :: Test.Framework.Test@@ -25,30 +25,6 @@         (testArrayElemsLeft (Proxy :: Proxy 5))     , testProperty "arrayElems . array (identity; 200)"         (testArrayElemsLeft (Proxy :: Proxy 200))-    , testProperty "arrayFlatten . array (identity; 0)"-        (testArrayFlattenLeft (Proxy :: Proxy 0))-    , testProperty "arrayFlatten . array (identity; 1)"-        (testArrayFlattenLeft (Proxy :: Proxy 1))-    , testProperty "arrayFlatten . array (identity; 2)"-        (testArrayFlattenLeft (Proxy :: Proxy 2))-    , testProperty "arrayFlatten . array (identity; 22)"-        (testArrayFlattenLeft (Proxy :: Proxy 22))-    , testProperty "arrayFlatten . array (identity; 50)"-        (testArrayFlattenLeft (Proxy :: Proxy 50))-    , testProperty "arrayFlatten . array (identity; nested; nested; 2x6)"-        (testArrayFlattenNestedLeft (Proxy :: Proxy 2) (Proxy :: Proxy 6))-    , testProperty "arrayFlatten . array (identity; nested; nested; 10x2)"-        (testArrayFlattenNestedLeft (Proxy :: Proxy 10) (Proxy :: Proxy 2))-    , testProperty "arrayFlatten . array (identity; nested; nested; 38x20)"-        (testArrayFlattenNestedLeft (Proxy :: Proxy 38) (Proxy :: Proxy 20))-    , testProperty "arrayFlatten . array (identity; nested; nested; 125x100)"-        (testArrayFlattenNestedLeft (Proxy :: Proxy 125) (Proxy :: Proxy 100))-    , testProperty "arraySize . array (identity; 0)"-        (testArraySizeLeft (Proxy :: Proxy 0))-    , testProperty "arraySize . array (identity; 45)"-        (testArraySizeLeft (Proxy :: Proxy 45))-    , testProperty "arraySize . array (identity; 100)"-        (testArraySizeLeft (Proxy :: Proxy 100))     ]  -- * Individual tests@@ -61,69 +37,6 @@       let array' :: Array n Int64           array' = array ls       in arrayelems array' == ls--  where--    -- Generator for lists of Int64 of known length.-    xsInt64 :: Gen [Int64]-    xsInt64 = vectorOf (fromIntegral (natVal len)) arbitrary---- | Test that building an array from a list and extracting the elements with--- the function 'flatten' will result in the same list.------ This test tests only plain arrays (no nesting).-testArrayFlattenLeft :: forall n . KnownNat n => Proxy n -> Property-testArrayFlattenLeft len =-    forAll xsInt64 $ \ls ->-      let array' :: Array n Int64-          array' = array ls-      in flatten array' == ls--  where--    -- Generator for lists of Int64 of known length.-    xsInt64 :: Gen [Int64]-    xsInt64 = vectorOf (fromIntegral (natVal len)) arbitrary---- | Test that building a nested array of a known size and extracting the--- elements with the function 'flatten' will result in a list with a size that--- is the product of the sizes provided.-testArrayFlattenNestedLeft :: forall n1 n2-                           .  (KnownNat n1, KnownNat n2)-                           => Proxy n1-                           -> Proxy n2-                           -> Property-testArrayFlattenNestedLeft len1 len2 =-    forAll xsArrays $ \array' ->-      length (flatten array' :: [Int64]) == expectedSize--  where--    -- Expected size of the matrix / array.-    expectedSize :: Int-    expectedSize = fromIntegral $ natVal len1 * natVal len2--    -- Generator for nested matrices of Int64 of known size.-    xsArrays :: Gen (Array n1 (Array n2 Int64))-    xsArrays =-      array <$> vectorOf (fromIntegral (natVal len1)) xsArrayInt64--    -- Generator for arrays of Int64 of known length.-    xsArrayInt64 :: Gen (Array n2 Int64)-    xsArrayInt64 = array <$> xsInt64--    -- Generator for lists of Int64 of known length.-    xsInt64 :: Gen [Int64]-    xsInt64 = vectorOf (fromIntegral (natVal len2)) arbitrary---- | Test that building an array from a list and calculating the size will--- return the length of the list.-testArraySizeLeft :: forall n . KnownNat n => Proxy n -> Property-testArraySizeLeft len =-    forAll xsInt64 $ \ls ->-      let array' :: Array n Int64-          array' = array ls-      in size array' == length ls    where