copilot-core 2.2.0 → 2.2.1

raw patch · 20 files changed

+167/−353 lines, 20 filesnew-uploaderPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• copilot-core.cabal +6/−10
• src/Copilot/Compile/Header/C99.hs +8/−59
• src/Copilot/Core.hs +1/−1
• src/Copilot/Core/Error.hs +4/−4
• src/Copilot/Core/Expr.hs +4/−4
• src/Copilot/Core/External.hs +7/−19
• src/Copilot/Core/Interpret.hs +2/−3
• src/Copilot/Core/Interpret/Eval.hs +50/−50
• src/Copilot/Core/Interpret/Render.hs +6/−6
• src/Copilot/Core/Locals.hs +1/−0
• src/Copilot/Core/MakeTags.hs +1/−17
• src/Copilot/Core/Operators.hs +0/−2
• src/Copilot/Core/PrettyDot.hs +21/−62
• src/Copilot/Core/PrettyPrint.hs +9/−9
• src/Copilot/Core/Random.hs +24/−78
• src/Copilot/Core/Random/Gen.hs +5/−5
• src/Copilot/Core/Random/Weights.hs +3/−3
• src/Copilot/Core/Spec.hs +0/−6
• src/Copilot/Core/Type.hs +13/−13
• src/Copilot/Core/Type/Dynamic.hs +2/−2

@@ -1,6 +1,6 @@ cabal-version:       >=1.10 name:                copilot-core-version:             2.2.0+version:             2.2.1 synopsis:            An intermediate representation for Copilot. description:   Intermediate representation for Copilot.@@ -41,15 +41,11 @@     -caf-all     -fno-warn-orphans -    --enable-library-profiling--    -- -fpackage-trust-    -- -- Trusted packages-    -- -trust base-    -- -trust random-    -- -trust array-    -- -trust dlist-    -- -trust containers+    -fpackage-trust+    -trust=array+    -trust=base+    -trust=containers+    -trust=random    build-depends:     containers >= 0.4,

@@ -51,7 +51,7 @@   , text ""   , text "/* External structs (must be defined by user): */"   , text ""-  , ppExternalStructs ({-specStructs-}externStructs spec)+  , ppExternalStructs (externStructs spec)   , text ""   , text "/* External variables (must be defined by user): */"   , text ""@@ -106,8 +106,7 @@       { triggerName = name       , triggerArgs = args } =           text "void" <+> text (prefix ++ name) <>-          text "(" <> {-nonStructs . -}ppArgs args <> text ");" -            --(buildStruct . getStructs args)+          text "(" <> ppArgs args <> text ");"      where     ppArgs :: [UExpr] -> Doc@@ -116,18 +115,6 @@     ppArg :: UExpr -> Doc     ppArg UExpr { uExprType = t } = text (typeSpec (UType t)) -{-    nonStructs :: [UExpr] -> [UExpr]-    nonStructs = filter (\UExpr { uExprExpr = e } -> e /= ExternStruct _ _ _ _)--    getStructs :: [UExpr] -> [UExpr]-    getStructs = map (\UExpr { uExprExpr = e } -> e)-                  $ filter (\UExpr { uExprExpr = e } -> e == ExternStruct _ _ _ _)--    buildStruct :: [Expr] -> Doc-    buildStruct = vcat . map ppStruct . nubBy eq-      where-        eq ExternStruct -}- --------------------------------------------------------------------------------  ppExternalVariables :: [ExtVar] -> Doc@@ -152,10 +139,10 @@ ppExternalArray   ExtArray     { externArrayName     = name-    , externArrayElemType = t -    , externArraySize     = size } +    , externArrayElemType = t+    , externArraySize     = size }   =-        text "extern" <+> text (typeSpec (UType t)) +        text "extern" <+> text (typeSpec (UType t))         <+> text name <> lbrack <> int size <> rbrack         <> text ";" @@ -185,34 +172,6 @@  -------------------------------------------------------------------------------- -{-ppStructs :: [StructData] -> Doc-ppStructs = vcat . map ppStruct . nubBy eq-  where-    eq StructData { structName = name1 } StructData { structName = name2 } = name1 == name2--ppStruct :: StructData -> Doc-ppStruct-  StructData-  { structName = name-  , structInst = inst } =-    case inst of-      ExternStruct _ _ sargs _ ->-        hang (hang (text "struct" <+> text name <+> text "{") 1 (nest 1 (ppStructArgs sargs))) 1 (text "};")-      _                        -> error "Struct is not of type Struct"--  where-    ppStructArgs :: [SExpr] -> Doc-    ppStructArgs = vcat . map ppStructArg . map (\SExpr { uexpr = u0 } -> u0)--    ppStructArg :: UExpr -> Doc-    ppStructArg UExpr { uExprType = t1, uExprExpr = e1 } = text (typeSpec (UType t1)) <+>-      text ( case e1 of-          Var _ name -> name-          ExternVar _ name _ -> name-          ExternFun _ name _ _ _ -> name-          ExternStruct _ name _ _ -> name-          _ -> "") <> text ";"--} ppExternalStructs :: [ExtStruct] -> Doc ppExternalStructs = vcat . map ppExternalStruct . nubBy eq   where@@ -223,26 +182,16 @@ ppExternalStruct   ExtStruct   { externStructName  = name-  , externStructArgs  = args-  , externStructTag   = tag } =-      --text "struct" <+> text name <> text "{" <> ppStructArgs args <> text "};"+  , externStructArgs  = args } =       hang (hang (text "struct" <+> text name <+> text "{") 1 (nest 1 (ppStructArgs args))) 1 (text "};")    where-    --ppStructArgs :: [SExpr] -> Doc-    --ppStructArgs = vcat . map ppStructArg . map (\SExpr { uexpr = u0 } -> u0)     ppStructArgs :: [(Name, UExpr)] -> Doc     ppStructArgs = vcat . map ppStructArg      ppStructArg :: (Name, UExpr) -> Doc-    ppStructArg (name, UExpr { uExprType = t1, uExprExpr = e1 }) = text (typeSpec (UType t1)) <+>-      text name <> text ";"-      {-text ( case e1 of-          Var _ name -> name-          ExternVar _ name _ -> name-          ExternFun _ name _ _ _ -> name-          ExternStruct _ name _ _ -> name-          _ -> "") <> text ";"-}+    ppStructArg (name', UExpr { uExprType = t1 }) = text (typeSpec (UType t1)) <+>+      text name' <> text ";"  -------------------------------------------------------------------------------- 

@@ -22,7 +22,7 @@ -- and the pretty-printer -- ("Copilot.Core.PrettyPrint"). -{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE Safe #-}  module Copilot.Core   ( module Copilot.Core.Error

@@ -4,14 +4,14 @@  {-# LANGUAGE Safe #-} -module Copilot.Core.Error +module Copilot.Core.Error   ( impossible   , badUsage ) where  impossible :: String -> String -> a-impossible function package = -  error $ "\"Impossible\" error in function " -    ++ function ++ ", in package " ++ package +impossible function package =+  error $ "\"Impossible\" error in function "+    ++ function ++ ", in package " ++ package     ++ ".  Please email Lee Pike at <lee pike @ gmail . com> " ++        "(remove spaces) or file a bug report on github.com." 

@@ -45,15 +45,15 @@   Const        :: Type a -> a -> Expr a   Drop         :: Type a -> DropIdx -> Id -> Expr a   Local        :: Type a -> Type b -> Name -> Expr a -> Expr b -> Expr b-  Var          :: Type a -> Name -> Expr a -  ExternVar    :: Type a -> Name -> Maybe [a] -> Expr a -  ExternFun    :: Type a -> Name -> [UExpr] -> Maybe (Expr a) +  Var          :: Type a -> Name -> Expr a+  ExternVar    :: Type a -> Name -> Maybe [a] -> Expr a+  ExternFun    :: Type a -> Name -> [UExpr] -> Maybe (Expr a)                -> Maybe Tag -> Expr a   ExternArray  :: Integral a => Type a -> Type b -> Name -> Int -> Expr a                -> Maybe [[b]] -> Maybe Tag -> Expr b   ExternStruct :: Type a -> Name -> [(Name, UExpr)] -> Maybe Tag -> Expr a   GetField     :: Type a -> Type b -> Expr a -> Name -> Expr b-  Op1          :: Op1 a b -> Expr a -> Expr b +  Op1          :: Op1 a b -> Expr a -> Expr b   Op2          :: Op2 a b c -> Expr a -> Expr b -> Expr c   Op3          :: Op3 a b c d -> Expr a -> Expr b -> Expr c -> Expr d   Label        :: Type a -> String -> Expr a -> Expr a

@@ -68,7 +68,7 @@   Op3 _ e1 e2 e3            -> externVarsExpr e1 `append`                                externVarsExpr e2 `append`                                externVarsExpr e3-  Label t s e               -> externVarsExpr e+  Label _ _ e               -> externVarsExpr e  externVarsUExpr :: UExpr -> DList ExtVar externVarsUExpr UExpr { uExprExpr = e } = externVarsExpr e@@ -85,7 +85,7 @@   Local _ _ _ e1 e2               -> externArraysExpr e1 `append` externArraysExpr e2   Var _ _                         -> empty   ExternVar _ _ _                 -> empty-  ExternArray t1 t2  name +  ExternArray t1 t2  name               size idx _ tag      -> singleton (ExtArray name t2 idx t1 size tag)   ExternFun _ _ ues _ _           -> concat (map externArraysUExpr ues)   ExternStruct _ _ _ _            -> empty@@ -95,7 +95,7 @@   Op3 _ e1 e2 e3                  -> externArraysExpr e1 `append`                                      externArraysExpr e2 `append`                                      externArraysExpr e3-  Label t s e                     -> externArraysExpr e+  Label _ _ e                     -> externArraysExpr e  externArraysUExpr :: UExpr -> DList ExtArray externArraysUExpr UExpr { uExprExpr = e } = externArraysExpr e@@ -121,7 +121,7 @@   Op3 _ e1 e2 e3              -> externFunsExpr e1 `append`                                  externFunsExpr e2 `append`                                  externFunsExpr e3-  Label t s e                 -> externFunsExpr e+  Label _ _ e                 -> externFunsExpr e  externFunsUExpr :: UExpr -> DList ExtFun externFunsUExpr UExpr { uExprExpr = e } = externFunsExpr e@@ -141,22 +141,13 @@   ExternVar   _ _ _               -> empty   ExternArray _ _ _ _ _ _ _       -> empty   ExternFun   _ _ _ _ _           -> empty-  ExternStruct _ name ses tag     -> {-if t == Struct then -}singleton (ExtStruct name ses tag){- else empty-}-                                      --concat . map externStructsUExpr ues+  ExternStruct _ name ses tag     -> singleton (ExtStruct name ses tag)                       -- all expressions in a struct are typed   GetField _ _ _ _                -> empty   Op1   _ _                       -> empty   Op2   _ _ _                     -> empty   Op3   _ _ _ _                   -> empty-  Label t s e                     -> externStructsExpr e-{-externStructsUExpr :: UExpr -> DList ExtStruct-externStructsUExpr UExpr { uExprExpr = e } =-  case e of-    ExternVar _ _ _           -> externVarsExpr e-    ExternArray _ _ _ _ _ _ _ -> externArraysExpr e-    ExternFun _ _ _ _ _       -> externFunsExpr e-    ExternStruct _ _ _        -> externStructsExpr e-    _                         -> empty-}+  Label _ _ e                     -> externStructsExpr e  -------------------------------------------------------------------------------- @@ -167,7 +158,7 @@   concat (fmap allObserver (specObservers spec))    where-  +   allStream     Stream { streamExpr = e } = f e @@ -178,9 +169,6 @@    allUExpr     (UExpr _ e1) = f e1--{-  allSExpr-    (SExpr _ (u)) = allUExpr u-}    allObserver     Observer { observerExpr = e } = f e

@@ -4,11 +4,10 @@  -- | An interpreter for Copilot specifications. -{-# LANGUAGE Trustworthy #-} -- Because of Containers+{-# LANGUAGE Safe #-}  module Copilot.Core.Interpret-  ( --ExtEnv (..)-    Format (..)+  ( Format (..)   , interpret   ) where 

@@ -4,12 +4,12 @@  -- | A tagless interpreter for Copilot specifications. -{-# LANGUAGE Trustworthy #-} -- Because of Data.Map (Containers)+{-# LANGUAGE Safe #-} {-# LANGUAGE GADTs, BangPatterns, DeriveDataTypeable #-}  module Copilot.Core.Interpret.Eval   ( --ExtEnv (..)-    Env +    Env   , Output   , ExecTrace (..)   , eval@@ -35,7 +35,7 @@ data InterpException   = -- NoValues Name --  | BadType Name-    ArrayWrongSize Name Int +    ArrayWrongSize Name Int   | ArrayIdxOutofBounds Name Int Int   | DivideByZero   | NotEnoughValues Name Int@@ -52,17 +52,17 @@    -- -- Should always be caught by Analyze.hs in copilot-language.   -- show (BadType name)                                                          =-  --   badUsage $ "you probably gave the wrong type for external element " +  --   badUsage $ "you probably gave the wrong type for external element "   --     ++ name ++ ".  Recheck your types and re-evaluate."   ---------------------------------------   show (ArrayWrongSize name expectedSize)                                      =-    badUsage $ "in the environment for external array " ++ name -      ++ ", we expect a list of length " ++ show 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 +    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."   ---------------------------------------@@ -87,12 +87,12 @@ type Env nm = [(nm, DynamicF [] Type)]  -- -- | External arrays environment.--- type ArrEnv = [(Name, [DynamicF [] Type])] +-- type ArrEnv = [(Name, [DynamicF [] Type])]  -- -- | Environment for simulation. -- data ExtEnv = ExtEnv { varEnv  :: Env Name---                      , arrEnv  :: ArrEnv --- --                     , funcEnv :: [(Name, Spec)] +--                      , arrEnv  :: ArrEnv+-- --                     , funcEnv :: [(Name, Spec)] --                      }  --------------------------------------------------------------------------------@@ -138,11 +138,11 @@    let strms = evalStreams k (specStreams spec) initStrms      in -  let trigs = map (evalTrigger showType k strms) +  let trigs = map (evalTrigger showType k strms)                   (specTriggers spec)                         in -  let obsvs = map (evalObserver showType k strms) -                  (specObservers spec)                        in +  let obsvs = map (evalObserver showType k strms)+                  (specObservers spec)                        in    strms `seq` ExecTrace                 { interpTriggers  = M.fromList $@@ -157,17 +157,17 @@  evalExpr_ :: Int -> Expr a -> LocalEnv -> Env Id -> a evalExpr_ k e0 locs strms = case e0 of-  Const _ x                          -> x -  Drop t i id                        -> +  Const _ x                          -> x+  Drop t i id                        ->     let Just xs = lookup id strms >>= fromDynF t in     reverse xs !! (fromIntegral i + k)-  Local t1 _ name e1 e2              -> +  Local t1 _ name e1 e2              ->     let x     = evalExpr_ k e1 locs strms in     let locs' = (name, toDyn t1 x) : locs  in     x `seq` locs' `seq` evalExpr_ k e2  locs' strms   Var t name                         -> fromJust $ lookup name locs >>= fromDyn t   ExternVar _ name xs                -> evalExternVar k name xs-  ExternFun _ name _ expr _          -> --evalFunc k t name expr +  ExternFun _ name _ expr _          -> --evalFunc k t name expr     case expr of       Nothing -> throw (NoExtsInterp name)       Just e  -> evalExpr_ k e locs strms@@ -175,32 +175,32 @@     where evalIdx = evalExpr_ k idx locs strms   ExternStruct _ _ _ _   -> error "unimplemented"   GetField _ _ _ _       -> error "unimplemented"-  Op1 op e1                          -> -    let ev1 = evalExpr_ k e1 locs strms in +  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 +    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 +  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 t s e1                         -> +  Label _ _ e1                         ->     let ev1 = evalExpr_ k e1 locs strms in     ev1  --------------------------------------------------------------------------------  evalExternVar :: Int -> Name -> Maybe [a] -> a-evalExternVar k name exts = +evalExternVar k name exts =   case exts of     Nothing -> throw (NoExtsInterp name)-    Just xs -> +    Just xs ->       case safeIndex k xs of         Nothing -> throw (NotEnoughValues name k)         Just x  -> x@@ -208,8 +208,8 @@ --------------------------------------------------------------------------------  -- evalFunc :: Int -> Type a -> Name -> Expr a -> ExtEnv -> a--- evalFunc k t name expr exts  = ---   evalExpr k expr +-- evalFunc k t name expr exts  =+--   evalExpr k expr  --   case lookup name (funcEnv exts) of --     Nothing -> throw (NoValues name)@@ -217,37 +217,37 @@ --     -- We created this spec in Interpreter.hs, copilot-language, so it should --     -- contain no triggers and exactly one observer. --     Just Spec { specStreams   = specStrms---               , specObservers = obsLs }  -> +--               , specObservers = obsLs }  -> --      let initStrms = map initStrm specStrms             in --      let strms = evalStreams k exts specStrms initStrms in --      case obsLs of --        [Observer { observerExpr     = expr_---                  , observerExprType = t1 }] -> +--                  , observerExprType = t1 }] -> --          let dyn = toDynF t1 expr_ in --            case fromDynF t dyn of --              Nothing    -> throw (BadType name) --              Just expr  -> evalExpr_ k expr exts [] strms---        _ -> throw (BadType name) +--        _ -> throw (BadType name)  --------------------------------------------------------------------------------  evalArray :: Integral b => Int -> Name -> b -> Maybe [[a]] -> Int -> a evalArray k name idx exts size =-  case exts of +  case exts of     Nothing -> throw (NoExtsInterp name)-    Just xs -> +    Just xs ->       case safeIndex k xs of         Nothing  -> throw (NotEnoughValues name k)         Just arr -> -- convoluted form in case the array is env of infinite                     -- length.-                    if    length (take size arr) == size  +                    if    length (take size arr) == size                        && length (take (size+1) arr) == size                       then case safeIndex (fromIntegral idx) arr of                              Nothing -> throw (ArrayIdxOutofBounds                                                  name (fromIntegral idx) size)                              Just x  -> x                       else throw (ArrayWrongSize name size)-  + --------------------------------------------------------------------------------  evalOp1 :: Op1 a b -> (a -> b)@@ -272,7 +272,7 @@   Atanh _    -> P.atanh   Acosh _    -> P.acosh   BwNot _    -> complement-  Cast _ _   -> P.fromIntegral +  Cast _ _   -> P.fromIntegral  -------------------------------------------------------------------------------- @@ -320,14 +320,14 @@ -- 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 :: Int -> [Stream] -> Env Id -> Env Id-evalStreams top specStrms initStrms = -  evalStreams_ 0 initStrms -  where +evalStreams top specStrms initStrms =+  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 +  evalStreams_ k strms | otherwise =+    evalStreams_ (k+1) $! strms_+    where     strms_ = map evalStream specStrms     evalStream Stream { streamId       = id                       , streamExpr     = e@@ -339,13 +339,13 @@  -------------------------------------------------------------------------------- -evalTrigger :: +evalTrigger ::   ShowType -> Int -> Env Id -> Trigger -> [Maybe [Output]] evalTrigger showType k strms   Trigger     { triggerGuard = e     , triggerArgs  = args-    } = map tag (zip bs vs) +    } = map tag (zip bs vs)    where   tag :: (Bool, a) -> Maybe a@@ -376,7 +376,7 @@ --------------------------------------------------------------------------------  evalExprs_ :: Int -> Expr a -> Env Id -> [a]-evalExprs_ k e strms = +evalExprs_ k e strms =   map (\i -> evalExpr_ i e [] strms) [0..(k-1)]  --------------------------------------------------------------------------------

@@ -4,7 +4,7 @@  -- | An tagless interpreter for Copilot specifications. -{-# LANGUAGE Trustworthy #-} -- Because of Data.Map (Containers)+{-# LANGUAGE Safe #-}  module Copilot.Core.Interpret.Render   ( renderAsTable@@ -64,7 +64,7 @@ step :: ExecTrace -> (Doc, Maybe ExecTrace) step ExecTrace        { interpTriggers  = trigs-       } = +       } =   if M.null trigs then (empty, Nothing)     else (foldl' ($$) empty (text "#" : ppTriggerOutputs), tails) @@ -72,10 +72,10 @@    ppTriggerOutputs :: [Doc]   ppTriggerOutputs =-      catMaybes -    . fmap ppTriggerOutput -    . M.assocs -    . fmap head +      catMaybes+    . fmap ppTriggerOutput+    . M.assocs+    . fmap head     $ trigs    ppTriggerOutput :: (String, Maybe [Output]) -> Maybe Doc

@@ -85,5 +85,6 @@   Op2 _ e1 e2                -> locsExpr e1 `append` locsExpr e2   Op3 _ e1 e2 e3             -> locsExpr e1 `append` locsExpr e2                                             `append` locsExpr e3+  Label _ _ e                -> locsExpr e  --------------------------------------------------------------------------------

@@ -11,7 +11,6 @@ import Copilot.Core.Expr import Copilot.Core.Spec import Control.Monad.State-import Data.Maybe(fromJust) import Prelude hiding (id)  next :: State Int Int@@ -30,14 +29,12 @@     , specObservers  = obsvs     , specTriggers   = trigs     , specProperties = props-    --, specStructs    = strts     } =   liftM4 Spec     (mkTagsStrms strms)     (mkTagsObsvs obsvs)     (mkTagsTrigs trigs)     (mkTagsProps props)-    --(mkTagsStrts strts)  mkTagsStrms :: [Stream] -> State Int [Stream] mkTagsStrms = mapM mkTagsStrm@@ -94,19 +91,6 @@           e' <- mkTagsExpr (propertyExpr p)           return $ p { propertyExpr = e' } -{-mkTagsStrts :: [BitStruct] -> State Int [BitStruct]-mkTagsStrts = mapM mkTagsStrt--  where-    mkTagsStrt BitStruct-      { structName      = name-      , structFields    = fields } =-        do--          return $ BitStruct-            { structName      = name-            , structFields    = fields' }--} mkTagsSExpr :: (Name, UExpr) -> State Int (Name, UExpr) mkTagsSExpr (name, UExpr { uExprExpr = e, uExprType = t }) =   do@@ -129,7 +113,7 @@   ExternFun t name args expr _   -> do args' <- mapM mkTagsUExpr args                                        k <- next                                        return $ ExternFun t name args' expr (Just k)-  ExternArray t1 t2 name +  ExternArray t1 t2 name               size idx e _       -> do idx' <- mkTagsExpr idx                                        k <- next                                        return $ ExternArray t1 t2 name size idx' e (Just k)

@@ -77,8 +77,6 @@   BwXor    :: Bits a => Type a -> Op2 a a a   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-  -- Struct operators.-  --GetField :: Type a -> Type b -> Op2 a String b  -- | Ternary operators. data Op3 a b c d where

@@ -19,48 +19,12 @@ import Data.List (intersperse) import Text.Printf ---mkVar :: String -> Id -> String-mkVar str id = str ++ show id--mkTmpStVar :: Id -> String-mkTmpStVar = mkVar "tmp_"--mkUpdateStFn :: Id -> String-mkUpdateStFn = mkVar "update_state_" --mkQueueVar :: Id -> String-mkQueueVar = mkVar "queue_" --mkQueuePtrVar :: Id -> String-mkQueuePtrVar = mkVar "ptr_" - mkExtTmpVar :: String -> String mkExtTmpVar = ("ext_" ++)  mkExtTmpTag :: String -> Maybe Tag -> String mkExtTmpTag name tag = "ext_" ++ name ++ "_" ++ show (tagExtract tag) -mkExtArrFn :: String -> String-mkExtArrFn = (++) "ext_arr_"--mkExtFunArgFn :: Int -> String -> Maybe Tag -> String-mkExtFunArgFn i nm tag = -  "ext_" ++ nm ++ "_" ++ show (tagExtract tag) ++ "_arg" ++ show i--mkObserverFn :: String -> String-mkObserverFn = ("observer_" ++)--mkTriggerGuardFn :: String -> String-mkTriggerGuardFn = ("trigger_guard_" ++)--mkTriggerArgFn :: Int -> String -> String-mkTriggerArgFn i nm = "trigger_" ++ nm ++ "_arg_" ++ show i--mkArgIdx :: [a] -> [(Int, a)]-mkArgIdx args = zip [0,1 ..] args- tagExtract :: Maybe Tag -> Tag tagExtract Nothing = impossible "tagExtract" "copilot-sbv" tagExtract (Just tag) = tag@@ -81,8 +45,8 @@             (if bb then (text (printf "%s [label=\"externF: %s\",color=cyan4, style=filled]\n" (show ii::String) (name::String)) <> text (printf "%s -> %s\n" (show pere::String) (show ii::String))                   <> (hcat (r1))) else (text (printf "%s [label=\"%s\",color=cyan4, style=filled]\n" (show ii::String) (mkExtTmpTag name tag))<> text (printf "%s -> %s\n" (show pere::String) (show ii::String)))                   ,i1)-  ExternArray _ _ name -              _ idx _ tag       -> let (r1,i1) = ppExprDot (ii+1) ii bb idx +  ExternArray _ _ name+              _ idx _ tag       -> let (r1,i1) = ppExprDot (ii+1) ii bb idx            in (if bb then (text (printf "%s [label=\"externA: %s\",color=cyan3, style=filled]\n" (show ii::String) (name::String)) <> text (printf "%s -> %s\n" (show pere::String) (show ii::String))                   <> r1) else (text (printf "%s [label=\"%s\",color=cyan3, style=filled]\n" (show ii::String) (mkExtTmpTag name tag)) <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)))                   ,i1)@@ -95,7 +59,7 @@   GetField _ _ _ name          -> (text (printf "%s [label=\"field: %s\",color=dodgerblue3, style=filled]\n" (show ii::String) (name::String) )                   <> 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 +  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))@@ -107,27 +71,27 @@   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 +  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 +  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 +  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 +                  <> r2                   <> r3 ,i3) -  Label t s e                -> let (r1,i1) = ppExprDot (ii+1) ii bb e +  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)@@ -182,13 +146,11 @@   BwXor    _   -> "^"   BwShiftL _ _ -> "<<"   BwShiftR _ _ -> ">>"-  --GetField _ _ -> "."  ppOp3 :: Op3 a b c d -> String ppOp3 op = case op of   Mux _    -> "mux" - --------------------------------------------------------------------------------  ppStream :: Int -> Stream -> (Doc, Int)@@ -199,7 +161,7 @@     , 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))@@ -223,12 +185,12 @@   <> text (printf "%s -> %s\n" (show i::String) (show i1::String))   <>  (vcat (r2))   ,i2)-  where +  where     (r1, i1) = ppExprDot (i+2) (i+1) True e     (r2, i2) = ppUExprL (i1+1) (i1) True args  ppUExprL :: Int -> Int -> Bool -> [UExpr] -> ([Doc], Int)-ppUExprL i pere bb [] = ([], i)+ppUExprL i _ _ [] = ([], i)  ppUExprL i pere bb (a:b) = ((r1:r2), i2)   where@@ -242,7 +204,7 @@   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@@ -253,12 +215,11 @@   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 - --------------------------------------------------------------------------------  @@ -305,10 +266,8 @@  -------------------------------------------------------------------------------- -- ppSpecDot :: Int -> Spec -> (Doc, Int)-ppSpecDot i spec = +ppSpecDot i spec =   ((aa $$ cs $$ ds $$ es $$ fs $$ bb),i4)   where     aa = text "digraph G {\nnode [shape=box]\n"@@ -323,13 +282,13 @@ -- | Pretty-prints a Copilot expression. prettyPrintExprDot :: Bool -> Expr a -> String prettyPrintExprDot bb s = render rr-  where -    (r1,i1) = (ppExprDot 1 0 bb s)-    rr = (text "digraph G {\nnode [shape=box]\n" $$ (text (printf "%s [label=\"file: \n?????\",color=red, style=filled]\n" (show 0))) <> r1 $$ text "\n}\n")+  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. prettyPrintDot :: Spec -> String prettyPrintDot s = render r1-  where (r1,i1) = (ppSpecDot 0 s)+  where (r1, _) = ppSpecDot 0 s  --------------------------------------------------------------------------------

@@ -31,12 +31,12 @@   Drop _ 0 id                -> strmName id   Drop _ i id                -> text "drop" <+> text (show i) <+> strmName id   ExternVar _ name _         -> text "Ext_" <> (text name)-  ExternFun _ name args _ _  -> -    text "Extf_" <> (text name) <> lparen <> +  ExternFun _ name args _ _  ->+    text "Extf_" <> (text name) <> lparen <>          (hcat (punctuate (comma <> space) (map ppUExpr args))        <> rparen)-  ExternArray _ _ name -              _ idx _ _      -> text "Exta_" <> (text name) <> lbrack +  ExternArray _ _ name+              _ idx _ _      -> text "Exta_" <> (text name) <> lbrack                                   <> ppExpr idx <> rbrack   ExternStruct _ name args _ -> text "struct" <+> doubleQuotes (text name <> lbrace                                     <> vcat (punctuate (semi <> space) (map ppSExpr $ args)) <> rbrace)@@ -47,7 +47,7 @@   Op1 op e                   -> ppOp1 op (ppExpr e)   Op2 op e1 e2               -> ppOp2 op (ppExpr e1) (ppExpr e2)   Op3 op e1 e2 e3            -> ppOp3 op (ppExpr e1) (ppExpr e2) (ppExpr e3)-  Label t s e                -> text "label "<>doubleQuotes (text s) <+> (ppExpr e)+  Label _ s e                -> text "label "<> doubleQuotes (text s) <+> (ppExpr e)  ppSExpr :: (Name, UExpr) -> Doc ppSExpr (_, UExpr { uExprExpr = e0 }) = ppExpr e0@@ -112,7 +112,7 @@     text "else" <+> doc3 <> text ")"  ---------------------------------------------------------------------------------  + ppInfix :: String -> Doc -> Doc -> Doc ppInfix cs doc1 doc2 = parens $ doc1 <+> text cs <+> doc2 @@ -130,10 +130,10 @@     , streamExprType = t     }       = (parens . text . showType) t-          <+> strmName id +          <+> strmName id     <+> text "="     <+> text ("["-              ++ ( concat $ intersperse "," +              ++ ( concat $ intersperse ","                               $ map (showWithType Haskell t) buffer )               ++ "]")     <+> text "++"@@ -151,7 +151,7 @@   <+> text "="   <+> ppExpr e   <+> lbrack-  $$  (nest 2 $ vcat (punctuate comma $ +  $$  (nest 2 $ vcat (punctuate comma $                           map (\a -> text "arg" <+> ppUExpr a) args))   $$  nest 2 rbrack 

@@ -9,10 +9,8 @@  module Copilot.Core.Random   ( randomSpec ) where---  , randomExtVals  -import Copilot.Core ---import Copilot.Core.Interpret.Eval (Env)+import Copilot.Core import Copilot.Core.Random.Gen import Copilot.Core.Random.Weights import Copilot.Core.Type.Dynamic@@ -38,7 +36,7 @@   ss          <- genStreamInfo's   extVars     <- genExtVars   streams     <- runReaderT (mapM (genStream ss) ss) extVars-  triggers    <- +  triggers    <-     runReaderT (mapM (genTrigger ss) (map mkTriggerName [0..numTriggers-1]))                extVars   return Spec { specStreams    = streams@@ -58,8 +56,8 @@     mapM genExtVar lst     where     genExtVar :: Int -> Gen DynExtVar-    genExtVar i = do -      ws <- weights                 +    genExtVar i = do+      ws <- weights       WrapType t <- genType ws       evalExpr <- randomReplicate rnds t       let expr = ExternVar t ("ext" ++ show i) (Just evalExpr)@@ -128,12 +126,12 @@   StreamInfo     { streamInfoId         = id     , streamInfoType       = t-    , streamInfoBufferSize = k } +    , streamInfoBufferSize = k }   = do   xs <- lift $ replicateM k (randomFromType t)   extVars <- ask   w  <- lift $ genExpr extVars ss t-  return +  return       Stream         { streamId       = id         , streamBuffer   = xs@@ -174,32 +172,32 @@   ws <- weights   if dp >= maxExprDepth ws     then freq (terminalLst ws)-    else freq $ +    else freq $       terminalLst ws ++       [ (op1Freq   ws, genOp1)       , (op2Freq   ws, genOp2)       , (op3Freq   ws, genOp3) ]    where-  terminalLst ws = +  terminalLst ws =     (extVarFreq' ws, genExtVar) : [ (constFreq ws, genConst)-                                  , (dropFreq  ws, genDrop) ] +                                  , (dropFreq  ws, genDrop) ]    extVarFreq' ws = if null typedExtVars then 0 else extVarFreq ws-  +   genExtVar = do     let vars = typedExtVars     r <- choose (0, length vars - 1)     return (vars !! r)    typedExtVars = foldl' typedExtVar [] extVars-    where typedExtVar vars dyn = +    where typedExtVar vars dyn =             case fromDynF t dyn of                    Nothing   -> vars                    Just expr -> expr:vars -  genConst = do -    x <- randomFromType t +  genConst = do+    x <- randomFromType t     return $ Const t x    genDrop = do@@ -213,7 +211,7 @@                                     _      -> False       in  elements (filter p ss) -  genOp3 = incDepth (genOp3Mux extVars ss t)    +  genOp3 = incDepth (genOp3Mux extVars ss t)    genOp1 = incDepth $ case t of     Bool   -> genOp1Bool extVars ss@@ -231,7 +229,7 @@   genOp2 = incDepth $ case t of     Bool    -> oneOf [ genOp2Bool extVars ss                      , genOp2Eq extVars ss-                     , genOp2Ord extVars ss +                     , genOp2Ord extVars ss                      ]     Int8    -> intOrWord NumWit IntegralWit     Int16   -> intOrWord NumWit IntegralWit@@ -247,15 +245,15 @@     where     floatOrDouble numWit = oneOf [ genOp2Num extVars ss t numWit ] -    intOrWord numWit integralWit = do -      ws <- weights -      if divModFreq ws +    intOrWord numWit integralWit = do+      ws <- weights+      if divModFreq ws         then oneOf $ num ++ [ genOp2Integral extVars ss t integralWit ]         else oneOf num-      where +      where       num = [ genOp2Num extVars ss t numWit ]-       + --------------------------------------------------------------------------------  genOp1Bool :: [DynExtVar] -> [StreamInfo] -> Gen (Expr Bool)@@ -285,9 +283,9 @@   return $ Op2 opw ew1 ew2  genOp2Ord :: [DynExtVar] -> [StreamInfo] -> Gen (Expr Bool)-genOp2Ord extVars ss = +genOp2Ord extVars ss =   let ss' = findStreamOmittingType Bool in-  if (null ss') then genExpr extVars ss Bool +  if (null ss') then genExpr extVars ss Bool     else do       WrapType t <- genTypeFromStreamInfo's ss'       ew1 <- genExpr extVars ss t@@ -299,7 +297,7 @@       return $ Op2 opw ew1 ew2   where   findStreamOmittingType :: Type a -> [StreamInfo]-  findStreamOmittingType t0 = +  findStreamOmittingType t0 =     let p (StreamInfo _ t1 _) = case t0 =~= t1 of                                   Just _ -> True                                   _      -> False@@ -314,7 +312,7 @@                   , (Mul t) ]   return $ Op2 opw ew1 ew2 -genOp2Integral :: +genOp2Integral ::   [DynExtVar] -> [StreamInfo] -> Type a -> IntegralWit a -> Gen (Expr a) genOp2Integral extVars ss t IntegralWit = do   ew1 <- genExpr extVars ss t@@ -334,55 +332,3 @@  data IntegralWit a = Integral a => IntegralWit ------------------------------------------------------------------------------------- randomExtVals :: Int -> Spec -> Weights -> StdGen -> ExtEnv--- randomExtVals rnds spec = runGen env 0---   where env = do vars <- extVals rnds spec---                  return ExtEnv { varEnv = vars---                                , arrEnv = []--- --                               , funcEnv = []---                                }-------------------------------------------------------------------------------------- Extract the external variables, returning randomly-generated lists for their--- values.--- extVals :: Int -> Spec -> Gen (Env Name)--- extVals rnds Spec { specStreams = strms---                   , specTriggers = triggers } ---   = ---   let vars = nubBy (\a b -> fst a == fst b) $ ---                concatMap strmExts strms ++ ---                concatMap triggerExts triggers  in---   mapM randomLst vars----   where ---   randomLst :: (Name, UType) -> Gen (Name, DynamicF [] Type)---   randomLst (nm, UType { uTypeType = t }) = do---     rnd <- randomReplicate rnds t---     return $ (nm, toDynF t rnd)----   strmExts Stream { streamExpr = expr } = extsFromExpr expr----   triggerExts Trigger { triggerGuard = grd---                       , triggerArgs = args } = ---     extsFromExpr grd ++ concatMap getExpr args---       where getExpr UExpr { uExprExpr = expr } = extsFromExpr expr-  ---   extsFromExpr :: Expr a -> [(Name, UType)]---   extsFromExpr expr =---     case expr of---       Const _ _                  -> []---       Drop _ _ _                 -> []---       Local _ _ _ e1 e2          -> extsFromExpr e1 ++ extsFromExpr e2---       Var _ _                    -> []---       ExternVar t name _         -> [(name, UType { uTypeType = t })]---       ExternFun _ _ _ _ _        -> []---       ExternArray _ _ _ _ _ _ _  -> []---       Op1 _ e                    -> extsFromExpr e---       Op2 _ e1 e2                -> extsFromExpr e1 ++ extsFromExpr e2---       Op3 _ e1 e2 e3             -> extsFromExpr e1 ++ extsFromExpr e2---                                       ++ extsFromExpr e3----------------------------------------------------------------------------------

@@ -92,7 +92,7 @@     n <- choose (toInteger mn, toInteger mx)     return (fromInteger n `asTypeOf` mn) -  genFractional :: (Random a, Fractional a) => Gen a+  genFractional :: Random a => Gen a   genFractional = do     g <- stdGen     return $ fst (random g)@@ -112,7 +112,7 @@   return $ fst (randomR rng g)  oneOf :: [Gen a] -> Gen a-oneOf [] = impossible "oneof" "copilot-core" +oneOf [] = impossible "oneof" "copilot-core" oneOf gs = choose (0,length gs - 1) >>= (gs !!)  -- | Takes a list of pairs (weight, Gen), and choose the Gen based on the@@ -120,17 +120,17 @@ -- choose c between 1 and the total.  Now recurse down the list, choosing an -- item only when c <= weight.  If not, subtract the current weight from c. freq :: [(Int, Gen a)] -> Gen a-freq [] = impossible "feq" "copilot-core" +freq [] = impossible "feq" "copilot-core" freq xs0 = choose (1, tot) >>= (`pick` xs0)   where   tot = sum (map fst xs0)   pick n ((k,x):xs)     | n <= k    = x     | otherwise = pick (n-k) xs-  pick _ _  = impossible "pick" "copilot-core" +  pick _ _  = impossible "pick" "copilot-core"  elements :: [a] -> Gen a-elements [] = impossible "elements" "copilot-core" +elements [] = impossible "elements" "copilot-core" elements xs = (xs !!) `fmap` choose (0, length xs - 1)  --------------------------------------------------------------------------------

@@ -39,11 +39,11 @@   , word32Freq   :: Int   , word64Freq   :: Int   , floatFreq    :: Int-  , doubleFreq   :: Int +  , doubleFreq   :: Int   , divModFreq   :: Bool }  simpleWeights :: Weights-simpleWeights = Weights +simpleWeights = Weights   { maxExprDepth = 10   , maxBuffSize  = 8   , maxTriggers  = 5@@ -71,5 +71,5 @@   , word32Freq   = 1   , word64Freq   = 1   , floatFreq    = 1-  , doubleFreq   = 1 +  , doubleFreq   = 1   , divModFreq   = True }

@@ -16,14 +16,9 @@  import Copilot.Core.Expr (Name, Id, Expr, UExpr) import Copilot.Core.Type (Type, Typed)---import Data.BitArray  -------------------------------------------------------------------------------- ---type StructInfo = [(Name, Int)]----------------------------------------------------------------------------------- -- | A stream. data Stream = forall a. Typed a => Stream   { streamId         :: Id@@ -71,6 +66,5 @@   , specObservers    :: [Observer]   , specTriggers     :: [Trigger]   , specProperties   :: [Property] }-  --, specStructs      :: [StructData] }  --------------------------------------------------------------------------------

@@ -48,7 +48,7 @@ --------------------------------------------------------------------------------  data SimpleType = SBool-                | SInt8 +                | SInt8                 | SInt16                 | SInt32                 | SInt64@@ -56,7 +56,7 @@                 | SWord16                 | SWord32                 | SWord64-                | SFloat +                | SFloat                 | SDouble   deriving Eq @@ -68,37 +68,37 @@  -------------------------------------------------------------------------------- -instance Typed Bool   where +instance Typed Bool   where   typeOf       = Bool   simpleType _ = SBool-instance Typed Int8   where +instance Typed Int8   where   typeOf       = Int8   simpleType _ = SBool-instance Typed Int16  where +instance Typed Int16  where   typeOf       = Int16   simpleType _ = SInt16-instance Typed Int32  where +instance Typed Int32  where   typeOf       = Int32   simpleType _ = SInt32-instance Typed Int64  where +instance Typed Int64  where   typeOf       = Int64   simpleType _ = SInt64-instance Typed Word8  where +instance Typed Word8  where   typeOf       = Word8   simpleType _ = SWord8-instance Typed Word16 where +instance Typed Word16 where   typeOf       = Word16   simpleType _ = SWord16-instance Typed Word32 where +instance Typed Word32 where   typeOf       = Word32   simpleType _ = SWord32-instance Typed Word64 where +instance Typed Word64 where   typeOf       = Word64   simpleType _ = SWord64-instance Typed Float  where +instance Typed Float  where   typeOf       = Float   simpleType _ = SFloat-instance Typed Double where +instance Typed Double where   typeOf       = Double   simpleType _ = SDouble 

@@ -34,7 +34,7 @@ data DynamicF :: (* -> *) -> (* -> *) -> * where   DynamicF :: f a -> t a -> DynamicF f t -toDyn :: EqualType t => t a -> a -> Dynamic t+toDyn :: t a -> a -> Dynamic t toDyn t x = Dynamic x t  fromDyn :: EqualType t => t a -> Dynamic t -> Maybe a@@ -43,7 +43,7 @@     Just Refl -> return x     Nothing   -> Nothing -toDynF :: EqualType t => t a -> f a -> DynamicF f t+toDynF :: t a -> f a -> DynamicF f t toDynF t fx = DynamicF fx t  fromDynF :: EqualType t => t a -> DynamicF f t -> Maybe (f a)