copilot-core 2.1.2 → 2.2.0

raw patch · 13 files changed

+571/−20 lines, 13 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• README.md +2/−0
• copilot-core.cabal +2/−1
• src/Copilot/Compile/Header/C99.hs +80/−2
• src/Copilot/Core/Expr.hs +10/−3
• src/Copilot/Core/External.hs +55/−3
• src/Copilot/Core/Interpret/Eval.hs +5/−0
• src/Copilot/Core/Locals.hs +2/−0
• src/Copilot/Core/MakeTags.hs +28/−1
• src/Copilot/Core/Operators.hs +2/−0
• src/Copilot/Core/PrettyDot.hs +335/−0
• src/Copilot/Core/PrettyPrint.hs +27/−7
• src/Copilot/Core/Random/Gen.hs +6/−0
• src/Copilot/Core/Spec.hs +17/−3

@@ -1,3 +1,5 @@+[![Build Status](https://travis-ci.org/Copilot-Language/copilot-core.svg?branch=master)](https://travis-ci.org/Copilot-Language/copilot-core)+ Overview ======== [copilot-core](http://hackage.haskell.org/package/copilot-core) The core

@@ -1,6 +1,6 @@ cabal-version:       >=1.10 name:                copilot-core-version:             2.1.2+version:             2.2.0 synopsis:            An intermediate representation for Copilot. description:   Intermediate representation for Copilot.@@ -85,3 +85,4 @@     Copilot.Core.Type.Read     Copilot.Core.Type.Uninitialized     Copilot.Core.PrettyPrint+    Copilot.Core.PrettyDot

@@ -49,6 +49,10 @@   , text ""   , ppTriggerPrototypes prefix (specTriggers spec)   , text ""+  , text "/* External structs (must be defined by user): */"+  , text ""+  , ppExternalStructs ({-specStructs-}externStructs spec)+  , text ""   , text "/* External variables (must be defined by user): */"   , text ""   , ppExternalVariables (externVars spec)@@ -102,7 +106,8 @@       { triggerName = name       , triggerArgs = args } =           text "void" <+> text (prefix ++ name) <>-          text "(" <> ppArgs args <> text ");"+          text "(" <> {-nonStructs . -}ppArgs args <> text ");" +            --(buildStruct . getStructs args)      where     ppArgs :: [UExpr] -> Doc@@ -111,6 +116,18 @@     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@@ -168,6 +185,67 @@  -------------------------------------------------------------------------------- +{-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+    eq ExtStruct { externStructName = name1 } ExtStruct { externStructName = name2 } =+      name1 == name2++ppExternalStruct :: ExtStruct -> Doc+ppExternalStruct+  ExtStruct+  { externStructName  = name+  , externStructArgs  = args+  , externStructTag   = tag } =+      --text "struct" <+> text name <> text "{" <> ppStructArgs args <> text "};"+      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 ";"-}++--------------------------------------------------------------------------------+ typeSpec :: UType -> String typeSpec UType { uTypeType = t }   = case t of@@ -186,7 +264,7 @@ --------------------------------------------------------------------------------  ppStep :: String -> Doc-ppStep prefix = text "void" <+> text (prefix ++ "step") <> text "();"+ppStep prefix = text "void" <+> text (prefix ++ "step") <> text "(void);"  -------------------------------------------------------------------------------- 

@@ -10,13 +10,14 @@   , Name   , Expr (..)   , UExpr (..)+  , SExpr (..)   , DropIdx   , Tag   ) where  import Copilot.Core.Operators (Op1, Op2, Op3) import Copilot.Core.Type (Type)-import Data.Word (Word16)+import Data.Word (Word32)  -------------------------------------------------------------------------------- @@ -31,7 +32,7 @@ --------------------------------------------------------------------------------  -- | An index for the drop operator.-type DropIdx = Word16+type DropIdx = Word32  -------------------------------------------------------------------------------- @@ -49,10 +50,13 @@   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 +               -> 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    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  -------------------------------------------------------------------------------- @@ -60,3 +64,6 @@ data UExpr = forall a. UExpr   { uExprType :: Type a   , uExprExpr :: Expr a }++-- | An expression for Struct args+data SExpr = SExpr { sname :: String, uexpr :: UExpr }

@@ -7,8 +7,8 @@ {-# LANGUAGE Rank2Types #-}  module Copilot.Core.External-  ( ExtVar (..), ExtArray (..), ExtFun (..)-  , externVars, externArrays, externFuns+  ( ExtVar (..), ExtArray (..), ExtFun (..), ExtStruct (..)+  , externVars, externArrays, externFuns, externStructs   ) where  import Copilot.Core.Expr@@ -38,6 +38,11 @@   , externFunArgs      :: [UExpr]   , externFunTag       :: Maybe Tag } +data ExtStruct = ExtStruct+  { externStructName  :: Name+  , externStructArgs  :: [(Name, UExpr)]+  , externStructTag   :: Maybe Tag }+ --------------------------------------------------------------------------------  externVars :: Spec -> [ExtVar]@@ -56,11 +61,14 @@   ExternVar t name _        -> singleton (ExtVar name (UType t))   ExternArray _ _ _ _ e _ _ -> externVarsExpr e   ExternFun _ _ ues _ _     -> concat (map externVarsUExpr ues)+  ExternStruct _ _ _ _      -> empty+  GetField _ _ _ _          -> empty   Op1 _ e                   -> externVarsExpr e   Op2 _ e1 e2               -> externVarsExpr e1 `append` externVarsExpr e2   Op3 _ e1 e2 e3            -> externVarsExpr e1 `append`                                externVarsExpr e2 `append`                                externVarsExpr e3+  Label t s e               -> externVarsExpr e  externVarsUExpr :: UExpr -> DList ExtVar externVarsUExpr UExpr { uExprExpr = e } = externVarsExpr e@@ -80,11 +88,14 @@   ExternArray t1 t2  name                size idx _ tag      -> singleton (ExtArray name t2 idx t1 size tag)   ExternFun _ _ ues _ _           -> concat (map externArraysUExpr ues)+  ExternStruct _ _ _ _            -> empty+  GetField _ _ _ _                -> empty   Op1 _ e                         -> externArraysExpr e   Op2 _ e1 e2                     -> externArraysExpr e1 `append` externArraysExpr e2   Op3 _ e1 e2 e3                  -> externArraysExpr e1 `append`                                      externArraysExpr e2 `append`                                      externArraysExpr e3+  Label t s e                     -> externArraysExpr e  externArraysUExpr :: UExpr -> DList ExtArray externArraysUExpr UExpr { uExprExpr = e } = externArraysExpr e@@ -102,15 +113,53 @@   Var _ _                     -> empty   ExternVar _ _ _             -> empty   ExternArray _ _ _ _ idx _ _ -> externFunsExpr idx-  ExternFun t name ues _ tag  -> singleton (ExtFun name t ues tag)+  ExternFun t name ues _ tag  -> concat $ singleton (ExtFun name t ues tag) : (map externFunsUExpr ues)+  ExternStruct _ _ _ _        -> empty+  GetField _ _ _ _            -> empty   Op1 _ e                     -> externFunsExpr e   Op2 _ e1 e2                 -> externFunsExpr e1 `append` externFunsExpr e2   Op3 _ e1 e2 e3              -> externFunsExpr e1 `append`                                  externFunsExpr e2 `append`                                  externFunsExpr e3+  Label t s e                 -> externFunsExpr e +externFunsUExpr :: UExpr -> DList ExtFun+externFunsUExpr UExpr { uExprExpr = e } = externFunsExpr e++ -------------------------------------------------------------------------------- +externStructs :: Spec -> [ExtStruct]+externStructs = toList . all externStructsExpr++externStructsExpr :: Expr a -> DList ExtStruct+externStructsExpr e0 = case e0 of+  Const _ _                       -> empty+  Drop  _ _ _                     -> empty+  Local _ _ _ _ _                 -> empty+  Var   _ _                       -> empty+  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+                      -- 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-}++--------------------------------------------------------------------------------+ all :: (forall a . Expr a -> DList b) -> Spec -> DList b all f spec =   concat (fmap (allStream) (specStreams   spec)) `append`@@ -129,6 +178,9 @@    allUExpr     (UExpr _ e1) = f e1++{-  allSExpr+    (SExpr _ (u)) = allUExpr u-}    allObserver     Observer { observerExpr = e } = f e

@@ -173,6 +173,8 @@       Just e  -> evalExpr_ k e locs strms   ExternArray _ _ name size idx xs _ -> evalArray k name evalIdx xs size     where evalIdx = evalExpr_ k idx locs strms+  ExternStruct _ _ _ _   -> error "unimplemented"+  GetField _ _ _ _       -> error "unimplemented"   Op1 op e1                          ->      let ev1 = evalExpr_ k e1 locs strms in      let op1 = evalOp1 op                in@@ -188,6 +190,9 @@     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                         -> +    let ev1 = evalExpr_ k e1 locs strms in+    ev1  -------------------------------------------------------------------------------- 

@@ -79,6 +79,8 @@   ExternVar _ _ _            -> empty   ExternFun _ _ _ _ _        -> empty   ExternArray _ _  _ _ _ _ _ -> empty+  ExternStruct _ _ _ _       -> empty+  GetField _ _ _ _           -> empty   Op1 _ e                    -> locsExpr e   Op2 _ e1 e2                -> locsExpr e1 `append` locsExpr e2   Op3 _ e1 e2 e3             -> locsExpr e1 `append` locsExpr e2

@@ -2,7 +2,7 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- --- | Sets a unique tags for each external array/function call.+-- | Sets a unique tags for each external array/function/struct call.  {-# LANGUAGE Safe #-} @@ -11,6 +11,7 @@ import Copilot.Core.Expr import Copilot.Core.Spec import Control.Monad.State+import Data.Maybe(fromJust) import Prelude hiding (id)  next :: State Int Int@@ -29,12 +30,14 @@     , 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@@ -91,6 +94,25 @@           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+    e' <- mkTagsExpr e+    return (name, UExpr { uExprExpr = e', uExprType = t })+ mkTagsUExpr :: UExpr -> State Int UExpr mkTagsUExpr UExpr { uExprExpr = e, uExprType = t } =   do@@ -111,6 +133,11 @@               size idx e _       -> do idx' <- mkTagsExpr idx                                        k <- next                                        return $ ExternArray t1 t2 name size idx' e (Just k)+  ExternStruct t name sargs _    -> do args' <- mapM mkTagsSExpr sargs+                                       k <- next+                                       return $ ExternStruct t name args' (Just k)+  GetField ts tf id name         -> return $ GetField ts tf id name   Op1 op e                       -> liftM  (Op1 op) (mkTagsExpr e)   Op2 op e1 e2                   -> liftM2 (Op2 op) (mkTagsExpr e1) (mkTagsExpr e2)   Op3 op e1 e2 e3                -> liftM3 (Op3 op) (mkTagsExpr e1) (mkTagsExpr e2) (mkTagsExpr e3)+  Label t s e                    -> liftM  (Label t s) (mkTagsExpr e)

@@ -77,6 +77,8 @@   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

@@ -0,0 +1,335 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- | A pretty printer for Copilot specifications.++{-# LANGUAGE Safe #-}+{-# LANGUAGE GADTs #-}++module Copilot.Core.PrettyDot+  ( 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++++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++--------------------------------------------------------------------------------++ppExprDot :: Int -> Int -> Bool -> Expr a -> (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)+  ExternFun _ name args _ tag  -> let (r1, i1) = ppUExprL (ii+1) ii bb args in+            (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 +           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)++  ExternStruct _ name args _ -> let (r1, i1) = ppUExprL (ii+1) ii bb (map snd $args) in+            (text (printf "%s [label=\"externS: %s\",color=dodgerblue2, style=filled]\n" (show ii::String) (name::String))+                  <> text (printf "%s -> %s\n" (show pere::String) (show ii::String))+                  <> (hcat (r1)),i1)++  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 +                                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 t 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)++ppUExpr :: Int -> Int -> Bool -> UExpr -> (Doc, Int)+ppUExpr i pere bb UExpr { uExprExpr = e0 } = ppExprDot i pere bb e0++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"+  BwNot _  -> "~"+  Cast _ _ -> "(cast)"++ppOp2 :: Op2 a b c -> String+ppOp2 op = case op of+  And          -> "&&"+  Or           -> "||"+  Add      _   -> "+"+  Sub      _   -> "-"+  Mul      _   -> "*"+  Div      _   -> "div"+  Mod      _   -> "mod"+  Fdiv     _   -> "/"+  Pow      _   -> "**"+  Logb     _   -> "logBase"+  Eq       _   -> "=="+  Ne       _   -> "/="+  Le       _   -> "<="+  Ge       _   -> ">="+  Lt       _   -> "<"+  Gt       _   -> ">"+  BwAnd    _   -> "&"+  BwOr     _   -> "|"+  BwXor    _   -> "^"+  BwShiftL _ _ -> "<<"+  BwShiftR _ _ -> ">>"+  --GetField _ _ -> "."++ppOp3 :: Op3 a b c d -> String+ppOp3 op = case op of+  Mux _    -> "mux"+++--------------------------------------------------------------------------------++ppStream :: Int -> Stream -> (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+--------------------------------------------------------------------------------++ppTrigger :: Int -> Trigger -> (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++ppUExprL :: Int -> Int -> Bool -> [UExpr] -> ([Doc], Int)+ppUExprL i pere bb [] = ([], 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++--------------------------------------------------------------------------------++ppObserver :: Int -> Observer -> (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+--------------------------------------------------------------------------------++ppProperty :: Int -> Property -> (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+++--------------------------------------------------------------------------------+++--------------------------------------------------------------------------------++ppStreamL :: Int -> [Stream] -> (Doc, Int)+ppStreamL i [] = (empty,i)++ppStreamL i (a:b) = ((s1$$s2),(i2))+  where+    (s1,i1) = ppStream i a+    (s2,i2) = ppStreamL i1 b++--------------------------------------------------------------------------------++ppTriggerL :: Int -> [Trigger] -> (Doc, Int)+ppTriggerL i [] = (empty,i)++ppTriggerL i (a:b) = ((s1$$s2),(i2))+  where+    (s1,i1) = ppTrigger i a+    (s2,i2) = ppTriggerL i1 b++--------------------------------------------------------------------------------++ppObserverL :: Int -> [Observer] -> (Doc, Int)+ppObserverL i [] = (empty,i)++ppObserverL i (a:b) = ((s1$$s2),(i2))+  where+    (s1,i1) = ppObserver i a+    (s2,i2) = ppObserverL i1 b+++--------------------------------------------------------------------------------++ppPropertyL :: Int -> [Property] -> (Doc, Int)+ppPropertyL i [] = (empty,i)++ppPropertyL i (a:b) = ((s1$$s2),(i2))+  where+    (s1,i1) = ppProperty i a+    (s2,i2) = ppPropertyL i1 b++--------------------------------------------------------------------------------++++ppSpecDot :: Int -> Spec -> (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-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")++-- | Pretty-prints a Copilot specification.+prettyPrintDot :: Spec -> String+prettyPrintDot s = render r1+  where (r1,i1) = (ppSpecDot 0 s)++--------------------------------------------------------------------------------

@@ -9,6 +9,7 @@  module Copilot.Core.PrettyPrint   ( prettyPrint+  , ppExpr   ) where  import Copilot.Core@@ -29,22 +30,28 @@   Const t x                  -> text (showWithType Haskell t x)   Drop _ 0 id                -> strmName id   Drop _ i id                -> text "drop" <+> text (show i) <+> strmName id-  ExternVar _ name _         -> text "extern" <+> doubleQuotes (text name)+  ExternVar _ name _         -> text "Ext_" <> (text name)   ExternFun _ name args _ _  -> -    text "extern" <+> doubleQuotes -      (text name <> lparen <> -         hcat (punctuate (comma <> space) (map ppUExpr args))+    text "Extf_" <> (text name) <> lparen <> +         (hcat (punctuate (comma <> space) (map ppUExpr args))        <> rparen)   ExternArray _ _ name -              _ idx _ _      -> text "extern" <+> doubleQuotes (text name <> lbrack -                                  <> ppExpr idx <> rbrack)+              _ 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)+  GetField _ _ _ name        -> text "field" <+> doubleQuotes (text name)   Local _ _ name e1 e2       -> text "local" <+> doubleQuotes (text name) <+> equals                                           <+> ppExpr e1 $$ text "in" <+> ppExpr e2   Var _ name                 -> text "var" <+> doubleQuotes (text name)   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) +ppSExpr :: (Name, UExpr) -> Doc+ppSExpr (_, UExpr { uExprExpr = e0 }) = ppExpr e0+ ppUExpr :: UExpr -> Doc ppUExpr UExpr { uExprExpr = e0 } = ppExpr e0 @@ -95,6 +102,7 @@   BwXor    _   -> ppInfix "^"   BwShiftL _ _ -> ppInfix "<<"   BwShiftR _ _ -> ppInfix ">>"+  --GetField _ _ -> ppInfix "."  ppOp3 :: Op3 a b c d -> Doc -> Doc -> Doc -> Doc ppOp3 op = case op of@@ -160,12 +168,24 @@  -------------------------------------------------------------------------------- +ppProperty :: Property -> Doc+ppProperty+  Property+    { propertyName     = name+    , propertyExpr     = e }+  =   text "property \"" <> text name <> text "\""+  <+> text "="+  <+> ppExpr e++--------------------------------------------------------------------------------+ ppSpec :: Spec -> Doc-ppSpec spec = cs $$ ds $$ es+ppSpec spec = cs $$ ds $$ es $$ fs   where     cs = foldr (($$) . ppStream)   empty (specStreams   spec)     ds = foldr (($$) . ppTrigger)  empty (specTriggers  spec)     es = foldr (($$) . ppObserver) empty (specObservers spec)+    fs = foldr (($$) . ppProperty) empty (specProperties spec)  -------------------------------------------------------------------------------- 

@@ -23,6 +23,8 @@ import Copilot.Core.Error import Copilot.Core.Type +import Control.Applicative+import Control.Monad import System.Random (StdGen, Random, random, randomR, split)  --------------------------------------------------------------------------------@@ -33,6 +35,10 @@  instance Functor Gen where   fmap f (MkGen h) = MkGen (\ d ws r -> f (h d ws r))++instance Applicative Gen where+  pure = return+  (<*>) = ap  instance Monad Gen where   return x = MkGen (\ _ _ _ -> x)

@@ -11,13 +11,19 @@   , Trigger (..)   , Spec (..)   , Property (..)+  , StructData (..)   ) where  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@@ -47,16 +53,24 @@ data Property = Property   { propertyName     :: Name   , propertyExpr     :: Expr Bool }-  + -------------------------------------------------------------------------------- +-- | Struct representation as a bit array.+data StructData = StructData+  { structName       :: Name+  , structFields     :: [(Name, UExpr)] }++--------------------------------------------------------------------------------+ -- | A Copilot specification consists of a list of variables bound to anonymous--- streams, a lost of anomymous streams, a list of observers, and a list of--- triggers.+-- streams, a list of anomymous streams, a list of observers, a list of+-- triggers, and a list of structs. data Spec = Spec   { specStreams      :: [Stream]   , specObservers    :: [Observer]   , specTriggers     :: [Trigger]   , specProperties   :: [Property] }+  --, specStructs      :: [StructData] }  --------------------------------------------------------------------------------