copilot-core 0.2.1 → 0.2.2

raw patch · 17 files changed

+570/−379 lines, 17 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• copilot-core.cabal +3/−2
• src/Copilot/Compile/Header/C99.hs +9/−8
• src/Copilot/Core/Error.hs +5/−4
• src/Copilot/Core/Expr.hs +13/−54
• src/Copilot/Core/External.hs +20/−18
• src/Copilot/Core/Interpret.hs +5/−6
• src/Copilot/Core/Interpret/Eval.hs +171/−100
• src/Copilot/Core/MakeTags.hs +19/−24
• src/Copilot/Core/Operators.hs +1/−1
• src/Copilot/Core/PrettyPrint.hs +4/−3
• src/Copilot/Core/Random.hs +125/−128
• src/Copilot/Core/Spec.hs +3/−3
• src/Copilot/Core/Spec/Locals.hs +8/−8
• src/Copilot/Core/Type.hs +56/−11
• src/Copilot/Core/Type/Eq.hs +77/−0
• src/Copilot/Core/Type/Read.hs +51/−0
• src/Copilot/Core/Version.hs +0/−9

@@ -1,6 +1,6 @@ cabal-version:       >=1.10 name:                copilot-core-version:             0.2.1+version:             0.2.2 synopsis:            An intermediate representation for Copilot. description:         Intermediate representation for Copilot.                      Strictly follows Haskell 2010 except for universal@@ -62,7 +62,8 @@     Copilot.Core.Type     Copilot.Core.Type.Dynamic     Copilot.Core.Type.Equality+    Copilot.Core.Type.Eq     Copilot.Core.Type.Show+    Copilot.Core.Type.Read     Copilot.Core.Type.Uninitialized     Copilot.Core.PrettyPrint-    Copilot.Core.Version

@@ -13,7 +13,6 @@   ) where  import Copilot.Core-import Copilot.Core.Version import Data.List (intersperse, nubBy) import Text.PrettyPrint.HughesPJ import Prelude hiding (unlines)@@ -36,7 +35,7 @@  c99Header :: String -> Spec -> String c99Header prefix spec = render $ vcat $-  [ text "/* Generated by Copilot Core v." <+> text version <+> text "*/"+  [ text "/* Generated by Copilot Core." <+> text "*/"   , text ""   , ppHeaders   , text ""@@ -104,9 +103,8 @@           text "(" <> ppArgs args <> text ");"      where-     ppArgs :: [UExpr] -> Doc-    ppArgs = vcat . intersperse (text ",") . map ppArg+    ppArgs = hcat . intersperse (text ", ") . map ppArg      ppArg :: UExpr -> Doc     ppArg UExpr { uExprType = t } = text (typeSpec (UType t))@@ -136,10 +134,13 @@ ppExternalArray :: ExtArray -> Doc ppExternalArray   ExtArray-    { externArrayName = name-    , externArrayElemType = t } =-        text "extern" <+> text (typeSpec (UType t)) <+> text "*" <+>-        text name <> text ";"+    { externArrayName     = name+    , externArrayElemType = t +    , externArraySize     = size } +  =+        text "extern" <+> text (typeSpec (UType t)) +        <+> text name <> lbrack <> int size <> rbrack+        <> text ";"  -------------------------------------------------------------------------------- 

@@ -8,9 +8,10 @@  impossible :: String -> String -> a 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."+  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."  badUsage :: String -> a-badUsage msg = error $ "Copilot error: " ++ msg ++ "."+badUsage msg = error $ "Copilot error: " ++ msg

@@ -40,63 +40,22 @@ --------------------------------------------------------------------------------  data Expr a where-  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-    -> Expr a-  ExternFun-    :: Type a-    -> Name-    -> [UExpr]-    -> Maybe Tag-    -> Expr a-  ExternArray-    :: Integral a-    => Type a-    -> Type b-    -> Name-    -> Expr a-    -> Maybe Tag-    -> 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+  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) +               -> Maybe Tag -> Expr a+  ExternArray  :: Integral a => Type a -> Type b -> Name -> Int -> Expr a+               -> Maybe [[b]] -> Maybe Tag -> 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  --------------------------------------------------------------------------------  -- | A untyped expression (no phantom type).-data UExpr = forall a . UExpr+data UExpr = forall a. UExpr   { uExprType :: Type a   , uExprExpr :: Expr a }

@@ -28,6 +28,7 @@   , externArrayElemType :: Type b   , externArrayIdx      :: Expr a   , externArrayIdxType  :: Type a+  , externArraySize     :: Int   , externArrayTag      :: Maybe Tag }  data ExtFun = forall a . ExtFun@@ -49,18 +50,18 @@  externVarsExpr :: Expr a -> DList ExtVar externVarsExpr e0 = case e0 of-  Const  _ _            -> empty-  Drop   _ _ _          -> empty-  Local _ _ _ e1 e2     -> externVarsExpr e1 `append` externVarsExpr e2-  Var _ _               -> empty-  ExternVar t name      -> singleton (ExtVar name (UType t))-  ExternArray _ _ _ e _ -> externVarsExpr e-  ExternFun _ _ ues _   -> concat (map externVarsUExpr ues)-  Op1 _ e               -> externVarsExpr e-  Op2 _ e1 e2           -> externVarsExpr e1 `append` externVarsExpr e2-  Op3 _ e1 e2 e3        -> externVarsExpr e1 `append`-                           externVarsExpr e2 `append`-                           externVarsExpr e3+  Const  _ _                -> empty+  Drop   _ _ _              -> empty+  Local _ _ _ e1 e2         -> externVarsExpr e1 `append` externVarsExpr e2+  Var _ _                   -> empty+  ExternVar t name _        -> singleton (ExtVar name (UType t))+  ExternArray _ _ _ _ e _ _ -> externVarsExpr e+  ExternFun _ _ ues _ _     -> concat (map externVarsUExpr ues)+  Op1 _ e                   -> externVarsExpr e+  Op2 _ e1 e2               -> externVarsExpr e1 `append` externVarsExpr e2+  Op3 _ e1 e2 e3            -> externVarsExpr e1 `append`+                               externVarsExpr e2 `append`+                               externVarsExpr e3  externVarsUExpr :: UExpr -> DList ExtVar externVarsUExpr UExpr { uExprExpr = e } = externVarsExpr e@@ -76,9 +77,10 @@   Drop   _ _ _                    -> empty   Local _ _ _ e1 e2               -> externArraysExpr e1 `append` externArraysExpr e2   Var _ _                         -> empty-  ExternVar _ _                   -> empty-  ExternArray t1 t2  name idx tag -> singleton (ExtArray name t2 idx t1 tag)-  ExternFun _ _ ues _             -> concat (map externArraysUExpr ues)+  ExternVar _ _ _                 -> empty+  ExternArray t1 t2  name +              size idx _ tag      -> singleton (ExtArray name t2 idx t1 size tag)+  ExternFun _ _ ues _ _           -> concat (map externArraysUExpr ues)   Op1 _ e                         -> externArraysExpr e   Op2 _ e1 e2                     -> externArraysExpr e1 `append` externArraysExpr e2   Op3 _ e1 e2 e3                  -> externArraysExpr e1 `append`@@ -99,9 +101,9 @@   Drop   _ _ _                -> empty   Local _ _ _ e1 e2           -> externFunsExpr e1 `append` externFunsExpr e2   Var _ _                     -> empty-  ExternVar _ _               -> empty-  ExternArray _ _ _ idx _     -> externFunsExpr idx-  ExternFun t name ues tag    -> singleton (ExtFun name t ues tag)+  ExternVar _ _ _             -> empty+  ExternArray _ _ _ _ idx _ _ -> externFunsExpr idx+  ExternFun t name ues _ tag  -> singleton (ExtFun name t ues tag)   Op1 _ e                     -> externFunsExpr e   Op2 _ e1 e2                 -> externFunsExpr e1 `append` externFunsExpr e2   Op3 _ e1 e2 e3              -> externFunsExpr e1 `append`

@@ -5,8 +5,8 @@ -- | An interpreter for Copilot specifications.  module Copilot.Core.Interpret-  ( ExtEnv (..)-  , Format (..)+  ( --ExtEnv (..)+    Format (..)   , interpret   ) where @@ -18,10 +18,9 @@ data Format = Table | CSV  -- | Interprets a Copilot specification.-interpret :: Format -> Int -> ExtEnv -> Spec -> String-interpret format k exts spec =+interpret :: Format -> Int -> Spec -> String+interpret format k spec =   case format of     Table -> renderAsTable e     CSV   -> renderAsCSV e--  where e = eval Haskell k exts spec+  where e = eval Haskell k spec

@@ -4,11 +4,11 @@  -- | A tagless interpreter for Copilot specifications. -{-# LANGUAGE GADTs, BangPatterns #-}+{-# LANGUAGE GADTs, BangPatterns, DeriveDataTypeable #-}  module Copilot.Core.Interpret.Eval-  ( ExtEnv (..)-  , Env +  ( --ExtEnv (..)+    Env    , Output   , ExecTrace (..)   , eval@@ -18,27 +18,81 @@ import Copilot.Core.Type.Dynamic import Copilot.Core.Type.Show (showWithType, ShowType) +import Prelude hiding (id)+import qualified Prelude as P+ import Data.List (transpose) import qualified Data.Map as M import Data.Map (Map)-import Data.Maybe (fromJust, catMaybes)+import Data.Maybe (fromJust) import Data.Bits+import Control.Exception (Exception, throw)+import Data.Typeable -import Prelude hiding (id)-import qualified Prelude as P+-------------------------------------------------------------------------------- +data InterpException+  = -- NoValues Name+--  | BadType Name+    ArrayWrongSize Name Int +  | ArrayIdxOutofBounds Name Int Int+  | DivideByZero+  | NotEnoughValues Name Int+--  | NoExtFunEval Name+  | NoExtsInterp Name+  deriving Typeable++instance Show InterpException where+  ---------------------------------------+  -- show (NoValues name)                                                         =+  --   badUsage $ "you need to supply a list of values for interpreting "+  --     ++ "external element " ++ name ++ "."+  ---------------------------------------++  -- -- Should always be caught by Analyze.hs in copilot-language.+  -- show (BadType name)                                                          =+  --   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 +      ++ ", 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."+  ---------------------------------------++instance Exception InterpException+ --------------------------------------------------------------------------------  type Env nm = [(nm, DynamicF [] Type)] --- | External arrays environment.-type ArrEnv = [(Name, [DynamicF [] Type])] +-- -- | External arrays environment.+-- type ArrEnv = [(Name, [DynamicF [] Type])]  --- | Environment for simulation.-data ExtEnv = ExtEnv { varEnv  :: Env Name-                     , arrEnv  :: ArrEnv -                     , funcEnv :: [(Name, Spec)] -                     }+-- -- | Environment for simulation.+-- data ExtEnv = ExtEnv { varEnv  :: Env Name+--                      , arrEnv  :: ArrEnv +-- --                     , funcEnv :: [(Name, Spec)] +--                      }  -------------------------------------------------------------------------------- @@ -46,8 +100,9 @@  data ExecTrace = ExecTrace     -- map from trigger names to their maybe output, which is a list of strings-    -- representing their valus.  (Nothing output if the guard for the trigger-    -- is false).+    -- representing their values.  (Nothing output if the guard for the trigger+    -- is false).  The order is important, since we compare the arg lists+    -- between the interpreter and backends.   { interpTriggers  :: Map String [Maybe [Output]]     -- map from observer names to their outputs.  We also show observer outputs.   , interpObservers :: Map String [Output] }@@ -74,18 +129,18 @@ -- We could write this in a beautiful lazy style like above, but that creates a -- space leak in the interpreter that is hard to fix while maintaining laziness. -- We take a more brute-force appraoch below.-eval :: ShowType -> Int -> ExtEnv -> Spec -> ExecTrace-eval showType k exts spec =+eval :: ShowType -> Int -> Spec -> ExecTrace+eval showType k spec = --  let exts  = take k $ reverse exts'                          in    let initStrms = map initStrm (specStreams spec)             in -  let strms = evalStreams k exts (specStreams spec) initStrms in+  let strms = evalStreams k (specStreams spec) initStrms      in -  let trigs = map (evalTrigger showType k exts strms) +  let trigs = map (evalTrigger showType k strms)                    (specTriggers spec)                         in -  let obsvs = map (evalObserver showType k exts strms) +  let obsvs = map (evalObserver showType k strms)                    (specObservers spec)                        in     strms `seq` ExecTrace@@ -99,87 +154,93 @@  type LocalEnv = [(Name, Dynamic Type)] -evalExpr_ :: Int -> Expr a -> ExtEnv -> LocalEnv -> Env Id -> a-evalExpr_ k e0 exts locs strms = case e0 of-  Const _ x              -> x -  Drop t i id            -> +evalExpr_ :: Int -> Expr a -> LocalEnv -> Env Id -> a+evalExpr_ k e0 locs strms = case e0 of+  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 -> -    let x     = evalExpr_ k e1 exts locs strms in+  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 exts locs' strms-  Var t name                 -> fromJust $ lookup name locs >>= fromDyn t-  ExternVar t name           -> evalExtern k t name (varEnv exts)-  ExternFun t name _ _       -> evalFunc k t name exts-  ExternArray _ t name idx _ -> evalArray k t name evalIdx (arrEnv exts)-    where evalIdx = evalExpr_ k idx exts locs strms-  Op1 op e1              -> -    let ev1 = evalExpr_ k e1 exts locs strms in -    let op1 = evalOp1 op                     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 +    case expr of+      Nothing -> throw (NoExtsInterp name)+      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+  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 exts locs strms in -    let ev2 = evalExpr_ k e2 exts locs strms in -    let op2 = evalOp2 op                     in+  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 exts locs strms in -    let ev2 = evalExpr_ k e2 exts locs strms in -    let ev3 = evalExpr_ k e3 exts locs strms in -    let op3 = evalOp3 op                     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  -------------------------------------------------------------------------------- -evalExtern :: Int -> Type a -> Name -> Env Name -> a-evalExtern k t name exts = -  case lookup name exts of-    Nothing -> badUsage $ "you need to supply a list of values for interpreting variable " ++ name-    Just dyn ->-      case fromDynF t dyn of-        Nothing -> badUsage $ "you probably gave the wrong type for external variable " ++ name ++ ".  Recheck your types and re-evaluate."-        Just xs -> xs !! k+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  -------------------------------------------------------------------------------- -evalFunc :: Int -> Type a -> Name -> ExtEnv -> a-evalFunc k t name exts  = -  case lookup name (funcEnv exts) of-    Nothing -> -      badUsage $ "to simulate a spec containing the external function "-                   ++ name ++ ", you need to include a stream to simulate it"+-- evalFunc :: Int -> Type a -> Name -> Expr a -> ExtEnv -> a+-- evalFunc k t name expr exts  = +--   evalExpr k expr  -    -- 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 }  -> -     let initStrms = map initStrm specStrms             in-     let strms = evalStreams k exts specStrms initStrms in-     case obsLs of-       [Observer { observerExpr     = expr_-                 , observerExprType = t1 }] -> -         let dyn = toDynF t1 expr_ in-           case fromDynF t dyn of-             Nothing    -> impossible "evalFunc" "copilot-core"-             Just expr  -> evalExpr_ k expr exts [] strms-       _ -> badUsage $ "you probably gave the wrong type for external variable " ++ name ++ ".  Recheck your types and re-evaluate."+--   case lookup name (funcEnv exts) of+--     Nothing -> throw (NoValues name) +--     -- 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 }  -> +--      let initStrms = map initStrm specStrms             in+--      let strms = evalStreams k exts specStrms initStrms in+--      case obsLs of+--        [Observer { observerExpr     = expr_+--                  , 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) + -------------------------------------------------------------------------------- -evalArray :: Integral b => Int -> Type a -> Name -> b -> ArrEnv -> a-evalArray k t name idx exts =-  case lookup name exts of-    Nothing -> badUsage $ "you need to supply a list of finite lists " ++ -                 "for interpreting array " ++ name-    Just dyn ->-      case catMaybes $ map (fromDynF t) dyn of-        [] -> badUsage $ "you probably gave the wrong type for external variable " ++ name ++ ".  Recheck your types and re-evaluate."-        xs -> let arr = (xs !! k) in-              if length arr > fromIntegral idx-                then arr !! fromIntegral idx-                else badUsage $ "in the environment for array " ++ name ++ -                          ", you tried to index out of bounds"+evalArray :: Integral b => Int -> Name -> b -> Maybe [[a]] -> Int -> a+evalArray k name idx exts size =+  case exts of +    Nothing -> throw (NoExtsInterp name)+    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  +                       && 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)    -------------------------------------------------------------------------------- @@ -234,7 +295,7 @@   BwShiftR _ _ -> ( \ !a !b -> shiftR a $! fromIntegral b )  catchZero :: Integral a => (a -> a -> a) -> (a -> a -> a)-catchZero _ _ 0 = badUsage "divide by zero"+catchZero _ _ 0 = throw DivideByZero catchZero f x y = f x y  --------------------------------------------------------------------------------@@ -252,8 +313,8 @@  -- 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 -> ExtEnv -> [Stream] -> Env Id -> Env Id-evalStreams top exts specStrms initStrms = +evalStreams :: Int -> [Stream] -> Env Id -> Env Id+evalStreams top specStrms initStrms =    evalStreams_ 0 initStrms    where    evalStreams_ :: Int -> Env Id -> Env Id@@ -266,15 +327,15 @@                       , streamExpr     = e                       , streamExprType = t } =       let xs = fromJust $ lookup id strms >>= fromDynF t       in-      let x  = evalExpr_ k e exts [] strms                     in+      let x  = evalExpr_ k e [] strms                          in       let ls = x `seq` (x:xs)                                  in       (id, toDynF t ls)  --------------------------------------------------------------------------------  evalTrigger :: -  ShowType -> Int -> ExtEnv -> Env Id -> Trigger -> [Maybe [Output]]-evalTrigger showType k exts strms+  ShowType -> Int -> Env Id -> Trigger -> [Maybe [Output]]+evalTrigger showType k strms   Trigger     { triggerGuard = e     , triggerArgs  = args@@ -286,26 +347,36 @@   tag (False, _) = Nothing    bs :: [Bool]-  bs = evalExprs_ k e exts strms+  bs = evalExprs_ k e strms    vs :: [[Output]]   vs = transpose $ map evalUExpr args     evalUExpr :: UExpr -> [Output]   evalUExpr (UExpr t e1) =-    map (showWithType showType t) (evalExprs_ k e1 exts strms)+    map (showWithType showType t) (evalExprs_ k e1 strms)  ---------------------------------------------------------------------------------evalObserver :: ShowType -> Int -> ExtEnv -> Env Id -> Observer -> [Output]-evalObserver showType k exts strms+evalObserver :: ShowType -> Int -> Env Id -> Observer -> [Output]+evalObserver showType k strms   Observer     { observerExpr     = e     , observerExprType = t }-  = map (showWithType showType t) (evalExprs_ k e exts strms)+  = map (showWithType showType t) (evalExprs_ k e strms)  -------------------------------------------------------------------------------- -evalExprs_ :: Int -> Expr a -> ExtEnv -> Env Id -> [a]-evalExprs_ k e exts strms = -  map (\i -> evalExpr_ i e exts [] strms) [0..(k-1)]-                                       +evalExprs_ :: 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++--------------------------------------------------------------------------------

@@ -12,11 +12,10 @@ import Prelude hiding (id)  next :: State Int Int-next =-  do-    k <- get-    put (succ k)-    return k+next = do+  k <- get+  put (succ k)+  return k  makeTags :: Spec -> Spec makeTags spec = evalState (mkTagsSpec spec) 0@@ -37,7 +36,6 @@ mkTagsStrms = mapM mkTagsStrm    where-     mkTagsStrm Stream       { streamId         = id       , streamBuffer     = xs@@ -57,7 +55,6 @@ mkTagsObsvs = mapM mkTagsObsv    where-     mkTagsObsv Observer       { observerName     = name       , observerExpr     = e@@ -73,7 +70,6 @@ mkTagsTrigs = mapM mkTagsTrig   where-    mkTagsTrig Trigger      { triggerName      = name      , triggerGuard     = g@@ -94,19 +90,18 @@  mkTagsExpr :: Expr a -> State Int (Expr a) mkTagsExpr e0 = case e0 of-  Const t x                     -> return $ Const t x-  Drop t k id                   -> return $ Drop t k id-  Local t1 t2 name e1 e2        -> liftM2 (Local t1 t2 name) (mkTagsExpr e1) (mkTagsExpr e2)-  Var t name                    -> return $ Var t name-  ExternVar t name              -> return $ ExternVar t name-  ExternFun t name args _       -> do-                                     args' <- mapM mkTagsUExpr args-                                     k <- next-                                     return $ ExternFun t name args' (Just k)-  ExternArray t1 t2 name idx _  -> do-                                     idx' <- mkTagsExpr idx-                                     k <- next-                                     return $ ExternArray t1 t2 name idx' (Just k)-  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)+  Const t x                      -> return $ Const t x+  Drop t k id                    -> return $ Drop t k id+  Local t1 t2 name e1 e2         -> liftM2 (Local t1 t2 name) (mkTagsExpr e1) (mkTagsExpr e2)+  Var t name                     -> return $ Var t name+  ExternVar t name e             -> return $ ExternVar t name e+  ExternFun t name args expr _   -> do args' <- mapM mkTagsUExpr args+                                       k <- next+                                       return $ ExternFun t name args' expr (Just k)+  ExternArray t1 t2 name +              size idx e _       -> do idx' <- mkTagsExpr idx+                                       k <- next+                                       return $ ExternArray t1 t2 name size idx' e (Just k)+  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)

@@ -42,7 +42,7 @@   Acosh    :: Floating a => Type a -> Op1 a a   -- Bitwise operators.   BwNot    :: Bits     a => Type a -> Op1 a a-  -- Casting operaators.+  -- Casting operator.   Cast     :: (Integral a, Num b) => Type a -> Type b -> Op1 a b  -- | Binary operators.

@@ -28,13 +28,14 @@   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)-  ExternFun _ name args _    -> +  ExternVar _ name _         -> text "extern" <+> doubleQuotes (text name)+  ExternFun _ name args _ _  ->      text "extern" <+> doubleQuotes        (text name <> lparen <>           hcat (punctuate (comma <> space) (map ppUExpr args))        <> rparen)-  ExternArray _ _ name idx _ -> text "extern" <+> doubleQuotes (text name <> lbrack +  ExternArray _ _ name +              _ idx _ _      -> text "extern" <+> doubleQuotes (text name <> lbrack                                    <> ppExpr idx <> rbrack)   Local _ _ name e1 e2       -> text "local" <+> doubleQuotes (text name) <+> equals                                           <+> ppExpr e1 $$ text "in" <+> ppExpr e2

@@ -2,34 +2,36 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- +-- | Random spec generator.+ {-# LANGUAGE GADTs, ExistentialQuantification #-}  module Copilot.Core.Random-  ( randomSpec-  , randomExtVals ) where+  ( randomSpec ) where+--  , randomExtVals   import Copilot.Core -import Copilot.Core.Interpret.Eval (ExtEnv (..), Env)+--import Copilot.Core.Interpret.Eval (Env) import Copilot.Core.Random.Gen import Copilot.Core.Random.Weights import Copilot.Core.Type.Dynamic import Copilot.Core.Type.Equality ((=~=))  import Control.Monad-import Data.List (foldl', nubBy)+import Data.List (foldl') import Prelude hiding (id) import System.Random (StdGen) import Control.Monad.Reader  -------------------------------------------------------------------------------- -randomSpec :: Weights -> StdGen -> Spec-randomSpec = runGen genSpec 0+randomSpec :: Int -> Weights -> StdGen -> Spec+randomSpec rnds = runGen (genSpec rnds) 0  -------------------------------------------------------------------------------- -genSpec :: Gen Spec-genSpec = do+genSpec :: Int -> Gen Spec+genSpec rnds = do   ws          <- weights   numTriggers <- choose (1, maxTriggers ws)   ss          <- genStreamInfo's@@ -57,19 +59,20 @@     genExtVar i = do        ws <- weights                        WrapType t <- genType ws-      let expr = ExternVar t ("ext" ++ show i)+      evalExpr <- randomReplicate rnds t+      let expr = ExternVar t ("ext" ++ show i) (Just evalExpr)       return $ toDynF t expr  -------------------------------------------------------------------------------- -data StreamInfo = forall a . (Eq a, Ord a) => StreamInfo+data StreamInfo = forall a . (Eq a, Ord a, Typed a) => StreamInfo   { streamInfoId         :: Id   , streamInfoType       :: Type a   , streamInfoBufferSize :: Int }  -------------------------------------------------------------------------------- -data WrapType = forall a . (Eq a, Ord a) => WrapType (Type a)+data WrapType = forall a . (Eq a, Ord a, Typed a) => WrapType (Type a)  genType :: Weights -> Gen WrapType genType ws = freq@@ -86,7 +89,7 @@   , (floatFreq  ws, return $ WrapType (typeOf :: Type Double)) ]  genTypeFromStreamInfo's :: [StreamInfo] -> Gen WrapType-genTypeFromStreamInfo's = elements . map (\ (StreamInfo _ t _) -> WrapType t)+genTypeFromStreamInfo's = elements . map (\(StreamInfo _ t _) -> WrapType t)  -------------------------------------------------------------------------------- @@ -209,6 +212,8 @@                                     _      -> False       in  elements (filter p ss) +  genOp3 = incDepth (genOp3Mux extVars ss t)    +   genOp1 = incDepth $ case t of     Bool   -> genOp1Bool extVars ss     Int8   -> genOp1Num  extVars ss t@@ -223,9 +228,10 @@     Double -> genOp1Num  extVars ss t    genOp2 = incDepth $ case t of--- XXX ---    Bool    -> oneOf [genOp2Bool ss, genOp2Eq ss, genOp2Ord ss]-    Bool    -> oneOf [genOp2Bool extVars ss, genOp2Eq extVars ss]+    Bool    -> oneOf [ genOp2Bool extVars ss+                     , genOp2Eq extVars ss+                     , genOp2Ord extVars ss +                     ]     Int8    -> intOrWord NumWit IntegralWit     Int16   -> intOrWord NumWit IntegralWit     Int32   -> intOrWord NumWit IntegralWit@@ -238,99 +244,90 @@     Double  -> floatOrDouble NumWit      where--      intOrWord numWit integralWit = do -        ws <- weights -        if divModFreq ws -          then oneOf $ num ++ [ genOp2Integral extVars ss t integralWit ]-          else oneOf num-        where num = [ genOp2Num extVars ss t numWit ]--      floatOrDouble numWit = oneOf-        [ genOp2Num extVars ss t numWit ]+    floatOrDouble numWit = oneOf [ genOp2Num extVars ss t numWit ] -  genOp3 = incDepth (genOp3Mux extVars ss t)    +    intOrWord numWit integralWit = do +      ws <- weights +      if divModFreq ws +        then oneOf $ num ++ [ genOp2Integral extVars ss t integralWit ]+        else oneOf num+      where +      num = [ genOp2Num extVars ss t numWit ]+        --------------------------------------------------------------------------------  genOp1Bool :: [DynExtVar] -> [StreamInfo] -> Gen (Expr Bool)-genOp1Bool extVars ss =-  do-    ew <- genExpr extVars ss (typeOf :: Type Bool)-    return $ Op1 Not ew+genOp1Bool extVars ss = do+  ew <- genExpr extVars ss (typeOf :: Type Bool)+  return $ Op1 Not ew  genOp1Num :: Num a => [DynExtVar] -> [StreamInfo] -> Type a -> Gen (Expr a)-genOp1Num extVars ss t =-  do-    ew  <- genExpr extVars ss t-    opw <- elements [Abs t, Sign t]-    return $ Op1 opw ew+genOp1Num extVars ss t = do+  ew  <- genExpr extVars ss t+  opw <- elements [Abs t, Sign t]+  return $ Op1 opw ew  genOp2Bool :: [DynExtVar] -> [StreamInfo] -> Gen (Expr Bool)-genOp2Bool extVars ss =-  do-    ew1 <- genExpr extVars ss (typeOf :: Type Bool)-    ew2 <- genExpr extVars ss (typeOf :: Type Bool)-    opw <- elements [And, Or]-    return $ Op2 opw ew1 ew2+genOp2Bool extVars ss = do+  ew1 <- genExpr extVars ss (typeOf :: Type Bool)+  ew2 <- genExpr extVars ss (typeOf :: Type Bool)+  opw <- elements [And, Or]+  return $ Op2 opw ew1 ew2  genOp2Eq :: [DynExtVar] -> [StreamInfo] -> Gen (Expr Bool)-genOp2Eq extVars ss =-  do-    WrapType t <- genTypeFromStreamInfo's ss-    ew1 <- genExpr extVars ss t-    ew2 <- genExpr extVars ss t-    opw <- elements [Eq t, Ne t]-    return $ Op2 opw ew1 ew2+genOp2Eq extVars ss = do+  WrapType t <- genTypeFromStreamInfo's ss+  ew1 <- genExpr extVars ss t+  ew2 <- genExpr extVars ss t+  opw <- elements [Eq t, Ne t]+  return $ Op2 opw ew1 ew2 --- XXX--- Figure out how to ensure t comes from a Numeric Class--- genOp2Ord :: [StreamInfo] -> Gen (Expr Bool)--- genOp2Ord ss =---   do---     WrapType t <- genTypeFromStreamInfo's ss---     ew1 <- genExpr extVars ss t---     ew2 <- genExpr extVars ss t---     opw <- elements---       [ (Lt t)---       , (Gt t)---       , (Le t)---       , (Ge t) ]---     return $ Op2 opw ew1 ew2+genOp2Ord :: [DynExtVar] -> [StreamInfo] -> Gen (Expr Bool)+genOp2Ord extVars ss = +  let ss' = findStreamOmittingType Bool in+  if (null ss') then genExpr extVars ss Bool +    else do+      WrapType t <- genTypeFromStreamInfo's ss'+      ew1 <- genExpr extVars ss t+      ew2 <- genExpr extVars ss t+      opw <- elements [ (Lt t)+                      , (Gt t)+                      , (Le t)+                      , (Ge t) ]+      return $ Op2 opw ew1 ew2+  where+  findStreamOmittingType :: Type a -> [StreamInfo]+  findStreamOmittingType t0 = +    let p (StreamInfo _ t1 _) = case t0 =~= t1 of+                                  Just _ -> True+                                  _      -> False+    in  filter (not . p) ss  genOp2Num :: [DynExtVar] -> [StreamInfo] -> Type a -> NumWit a -> Gen (Expr a)-genOp2Num extVars ss t NumWit =-  do-    ew1 <- genExpr extVars ss t-    ew2 <- genExpr extVars ss t-    opw <- -      elements-        [ (Add t)-        , (Sub t)-        , (Mul t) ]-    return-      $ Op2 opw ew1 ew2+genOp2Num extVars ss t NumWit = do+  ew1 <- genExpr extVars ss t+  ew2 <- genExpr extVars ss t+  opw <- elements [ (Add t)+                  , (Sub t)+                  , (Mul t) ]+  return $ Op2 opw ew1 ew2  genOp2Integral ::    [DynExtVar] -> [StreamInfo] -> Type a -> IntegralWit a -> Gen (Expr a)-genOp2Integral extVars ss t IntegralWit =-  do-    ew1 <- genExpr extVars ss t-    ew2 <- genExpr extVars ss t-    opw <- -      elements-        [ (Div t)-        , (Mod t) ]-    return-      $ Op2 opw ew1 ew2+genOp2Integral extVars ss t IntegralWit = do+  ew1 <- genExpr extVars ss t+  ew2 <- genExpr extVars ss t+  opw <- elements [ (Div t)+                  , (Mod t) ]+  return $ Op2 opw ew1 ew2  genOp3Mux :: [DynExtVar] -> [StreamInfo] -> Type a -> Gen (Expr a)-genOp3Mux extVars ss t =-  do-    ew1 <- genExpr extVars ss (typeOf :: Type Bool)-    ew2 <- genExpr extVars ss t-    ew3 <- genExpr extVars ss t-    return $ Op3 (Mux t) ew1 ew2 ew3+genOp3Mux extVars ss t = do+  ew1 <- genExpr extVars ss (typeOf :: Type Bool)+  ew2 <- genExpr extVars ss t+  ew3 <- genExpr extVars ss t+  return $ Op3 (Mux t) ew1 ew2 ew3  data NumWit a = Num a => NumWit @@ -338,53 +335,53 @@  -------------------------------------------------------------------------------- -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 = []-                               }+-- 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+-- 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)+--   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+--   strmExts Stream { streamExpr = expr } = extsFromExpr expr -  triggerExts Trigger { triggerGuard = grd-                      , triggerArgs = args } = -    extsFromExpr grd ++ concatMap getExpr args-      where getExpr UExpr { uExprExpr = 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+--   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  --------------------------------------------------------------------------------

@@ -12,12 +12,12 @@   ) where  import Copilot.Core.Expr (Name, Id, Expr, UExpr)-import Copilot.Core.Type (Type)+import Copilot.Core.Type (Type, Typed)  --------------------------------------------------------------------------------  -- | A stream.-data Stream = forall a  . Stream+data Stream = forall a. Typed a => Stream   { streamId         :: Id   , streamBuffer     :: [a]   , streamGuard      :: Expr Bool@@ -27,7 +27,7 @@ --------------------------------------------------------------------------------  -- | An observer.-data Observer = forall a . Observer+data Observer = forall a. Observer   { observerName     :: Name   , observerExpr     :: Expr a   , observerExprType :: Type a }

@@ -74,13 +74,13 @@   Local t _ name e1 e2   -> singleton (Loc name t)                                         `append` locsExpr e1                                         `append` locsExpr e2-  Var _ _                -> empty-  ExternVar _ _          -> empty-  ExternFun _ _ _ _      -> empty-  ExternArray _ _ _ _ _  -> empty-  Op1 _ e                -> locsExpr e-  Op2 _ e1 e2            -> locsExpr e1 `append` locsExpr e2-  Op3 _ e1 e2 e3         -> locsExpr e1 `append` locsExpr e2-                                        `append` locsExpr e3+  Var _ _                    -> empty+  ExternVar _ _ _            -> empty+  ExternFun _ _ _ _ _        -> empty+  ExternArray _ _  _ _ _ _ _ -> empty+  Op1 _ e                    -> locsExpr e+  Op2 _ e1 e2                -> locsExpr e1 `append` locsExpr e2+  Op3 _ e1 e2 e3             -> locsExpr e1 `append` locsExpr e2+                                            `append` locsExpr e3  --------------------------------------------------------------------------------

@@ -10,6 +10,7 @@   ( Type (..)   , Typed (..)   , UType (..)+  , SimpleType(..)   ) where  import Data.Int@@ -43,22 +44,66 @@   (=~=) Double Double = Just Refl   (=~=) _ _ = Nothing +--------------------------------------------------------------------------------++data SimpleType = SBool+                | SInt8 +                | SInt16+                | SInt32+                | SInt64+                | SWord8+                | SWord16+                | SWord32+                | SWord64+                | SFloat +                | SDouble+  deriving Eq++--------------------------------------------------------------------------------+ class Typed a where   typeOf :: Type a+  simpleType :: Type a -> SimpleType -instance Typed Bool   where typeOf = Bool-instance Typed Int8   where typeOf = Int8-instance Typed Int16  where typeOf = Int16-instance Typed Int32  where typeOf = Int32-instance Typed Int64  where typeOf = Int64-instance Typed Word8  where typeOf = Word8-instance Typed Word16 where typeOf = Word16-instance Typed Word32 where typeOf = Word32-instance Typed Word64 where typeOf = Word64-instance Typed Float  where typeOf = Float-instance Typed Double where typeOf = Double+-------------------------------------------------------------------------------- +instance Typed Bool   where +  typeOf       = Bool+  simpleType _ = SBool+instance Typed Int8   where +  typeOf       = Int8+  simpleType _ = SBool+instance Typed Int16  where +  typeOf       = Int16+  simpleType _ = SInt16+instance Typed Int32  where +  typeOf       = Int32+  simpleType _ = SInt32+instance Typed Int64  where +  typeOf       = Int64+  simpleType _ = SInt64+instance Typed Word8  where +  typeOf       = Word8+  simpleType _ = SWord8+instance Typed Word16 where +  typeOf       = Word16+  simpleType _ = SWord16+instance Typed Word32 where +  typeOf       = Word32+  simpleType _ = SWord32+instance Typed Word64 where +  typeOf       = Word64+  simpleType _ = SWord64+instance Typed Float  where +  typeOf       = Float+  simpleType _ = SFloat+instance Typed Double where +  typeOf       = Double+  simpleType _ = SDouble+ --------------------------------------------------------------------------------  -- | A untyped type (no phantom type). data UType = forall a . UType { uTypeType :: Type a }++--------------------------------------------------------------------------------

@@ -0,0 +1,77 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++{-# LANGUAGE ExistentialQuantification, GADTs #-}++module Copilot.Core.Type.Eq+  ( EqWit (..)+  , eqWit+  , UVal (..)+  ) where++import Copilot.Core.Error (impossible)+import Copilot.Core.Type+import Copilot.Core.Type.Dynamic (fromDyn, toDyn)++--------------------------------------------------------------------------------++data EqWit a = Eq a => EqWit++--------------------------------------------------------------------------------++eqWit :: Type a -> EqWit a+eqWit t =+  case t of+    Bool   -> EqWit+    Int8   -> EqWit+    Int16  -> EqWit+    Int32  -> EqWit+    Int64  -> EqWit+    Word8  -> EqWit+    Word16 -> EqWit+    Word32 -> EqWit+    Word64 -> EqWit+    Float  -> EqWit+    Double -> EqWit++--------------------------------------------------------------------------------++data UVal = forall a. UVal+  { uType :: Type a+  , uVal  :: a+  }++--------------------------------------------------------------------------------++instance Eq UVal where+  (==) UVal { uType = t1+            , uVal = a } +       UVal { uType = t2+            , uVal = b }+    = case eqWit t1 of+        EqWit -> +          case eqWit t2 of+            EqWit -> +              let dyn1 = toDyn t1 a in+              case fromDyn t2 dyn1 of+                Nothing -> False+                Just x  -> +                  case t1 of +                    -- Hacks for QuickChecking between C and Haskell+                    Float  -> case t2 of+                                Float -> approx floatErr x b+                                _     -> impossible "instance Eq UVal"+                                                    "copilot-core"+                    Double -> case t2 of+                                Double -> approx doubleErr x b+                                _      -> impossible "instance Eq UVal" +                                                     "copilot-core"+                    _      -> x == b+    where +    approx :: (Num a, Ord a) => a -> a -> a -> Bool+    approx err x y = x - y < err && y - x < err+    floatErr  = 0.0001 :: Float+    doubleErr = 0.0001 :: Double++--------------------------------------------------------------------------------

@@ -0,0 +1,51 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++{-# LANGUAGE ExistentialQuantification, GADTs #-}++module Copilot.Core.Type.Read+  ( ReadWit (..)+  , readWit+  , readWithType+  ) where++import Copilot.Core.Type+import Copilot.Core.Error (badUsage)++--------------------------------------------------------------------------------++data ReadWit a = Read a => ReadWit++--------------------------------------------------------------------------------++readWit :: Type a -> ReadWit a+readWit t =+  case t of+    Bool   -> ReadWit+    Int8   -> ReadWit+    Int16  -> ReadWit+    Int32  -> ReadWit+    Int64  -> ReadWit+    Word8  -> ReadWit+    Word16 -> ReadWit+    Word32 -> ReadWit+    Word64 -> ReadWit+    Float  -> ReadWit+    Double -> ReadWit++--------------------------------------------------------------------------------++readWithType :: Type a -> String -> a+readWithType t str =+  case t of+    Bool -> case str of+              "0" -> False+              "1" -> True+              x   -> badUsage $ "in readWithType in copilot-core: expecting a \"0\" or \"1\" when reading a Boolean value " ++ show x ++ "."+    _    -> rd+  where+  rd = case readWit t of+         ReadWit -> read str++--------------------------------------------------------------------------------

@@ -1,9 +0,0 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.-----------------------------------------------------------------------------------module Copilot.Core.Version (version) where---- | The current version of Copilot Core.-version :: String-version = "0.1"