copilot 0.25 → 0.26

raw patch · 11 files changed

+395/−425 lines, 11 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Language/Copilot.hs +0/−2
• Language/Copilot/Examples/Examples.hs +133/−61
• Language/Copilot/Examples/LTLExamples.hs +34/−22
• Language/Copilot/Examples/PTLTLExamples.hs +61/−37
• Language/Copilot/Examples/StatExamples.hs +14/−7
• Language/Copilot/Language.hs +97/−221
• Language/Copilot/Libs/LTL.hs +23/−20
• Language/Copilot/Libs/PTLTL.hs +16/−13
• Language/Copilot/Variables.hs +0/−32
• README +10/−4
• copilot.cabal +7/−6

@@ -2,7 +2,6 @@   ( module Language.Copilot.Core   , module Language.Copilot.Analyser   , module Language.Copilot.Interpreter-  -- , module Language.Copilot.Variables   , module Language.Copilot.Help   , module Language.Copilot.AtomToC   , module Language.Copilot.Compiler@@ -22,7 +21,6 @@ import Language.Copilot.Core import Language.Copilot.Analyser import Language.Copilot.Interpreter--- import Language.Copilot.Variables import Language.Copilot.Help import Language.Copilot.AtomToC import Language.Copilot.Compiler

@@ -14,83 +14,126 @@ import Data.Int  import Language.Copilot -import Language.Copilot.Variables+-- import Language.Copilot.Variables  fib :: Streams fib = do-  "fib" .= [0,1] ++ var "fib" + (drop 1 $ varW64 "fib")-  "t"   .= even (var "fib")+  let f = varW64 "f"+  let t   = varB "t"+  f .= [0,1] ++ f + (drop 1 f)+  t .= even f     where even :: Spec Word64 -> Spec Bool           even w' = w' `mod` 2 == 0  t1 :: Streams-t1 = do-     x .= [0, 1, 2] ++ var x - (drop 1 $ varI32 x)-     y .= [True, False] ++ var y ^ var z-     z .= varI32 "x" <= drop 1 (var x)+t1 = +  let x = varI32 "x"+      y = varB "y"+      z = varB "z"+  in do+    x .= [0, 1, 2] ++ x - (drop 1 x)+    y .= [True, False] ++ y ^ z+    z .= x <= drop 1 x -t2 :: Streams-t2 = do-     a .= [True] ++ not (var a) -     b .= mux (var a) 2 (int8 3) +-- t2 :: Streams+-- t2 = do+--      a .= [True] ++ not (var a) +--      b .= mux (var a) 2 (int8 3)   -- t3 :: use an external variable called ext, typed Word32 t3 :: Streams-t3 = do-     a .= [0,1] ++ (var a) + extW32 "ext" 8 + extW32 "ext" 8 + extW32 "ext" 1-     b .= [True, False] ++ 2 + var a < 5 + extW32 "_ext" 1+t3 = +  let a    = varW32 "a"+      b    = varB "b"+      ext8 = extW32 "ext" 8+      ext1 = extW32 "ext" 1+  in do+      a .= [0,1] ++ a + ext8 + ext8 + ext1+      b .= [True, False] ++ 2 + a < 5 + ext1  t4 :: Streams-t4 = do-     a .= [True,False] ++ not (var a)-     b .= drop 1 (varB a)+t4 = let+    a = varB "a"+    b = varB "b"+  in do+    a .= [True,False] ++ not a+    b .= drop 1 a  t5 :: Streams-t5 = do-    x .= drop 3 (varB y)-    y .= [True, True] ++ not (var z)-    z .= [False, False] ++ not (var z)-    w .= varB x || var y+t5 = +  let x = varB "x"+      y = varB "y"+      w = varB "w"+      z = varB "z"+  in do+      x .= drop 3 y+      y .= [True, True] ++ not z+      z .= [False, False] ++ not z+      w .= x || y  yy :: Streams-yy = do a .= constW64 4  +yy = +  let a = varW64 "a"+  in  do a .= 4    zz :: Streams-zz = do --a .= [0..4] ++ drop 4 (varW32 a) + 1-  a .= (varW32 a) + 1-  b .= drop 3 (varW32 a)+zz = +  let a = varW32 "a"+      b = varW32 "b"+  in do --a .= [0..4] ++ drop 4 (varW32 a) + 1+      a .= a + 1+      b .= drop 3 a  xx :: Streams-xx = do -     a .= extW32 "ext" 5 -     b .= [3] ++ (varW32 a)-     c .= [0, 1, 3, 4] ++ drop 1 (varW32 b)+xx = +  let a = varW32 "a"+      b = varW32 "b"+      c = varW32 "c"+      ext = extW32 "ext" 1+  in do +      a .= ext+      b .= [3] ++ a+      c .= [0, 1, 3, 4] ++ drop 1 b  -- If the temperature rises more than 2.3 degrees within 0.2 seconds, then the -- engine is immediately shut off.  From the paper. engine :: Streams engine = do-   "temps" .= [0, 0, 0] ++ extF "temp" 1-   "overTempRise" .= drop 2 (varF "temps") > 2.3 + var "temps"-   "trigger" .= (var "overTempRise") ==> (extB "shutoff" 2) +  -- external vars+  let temp     = extF "temp" 1      +  let shutoff  = extB "shutoff" 2+  -- Copilot vars+  let temps    = varF "temps"+  let overTemp = varB "overTemp"+  let trigger  = varB "trigger" +  temps    .= [0, 0, 0] ++ temp+  overTemp .= drop 2 temps > 2.3 + temps+  trigger  .= overTemp ==> shutoff+ -- To compile: > let (streams, ss) = dist in interface $ compileOpts streams ss "dist" -- s at phase 2 on port 1.  Not stable. dist :: DistributedStreams dist = -  ( a .= [0,1] ++ (var a) + constW8 1-  ,     sendW8 a (2, 1)-    ..| emptySM-  )+  let a = varW8 "a"+  in +    ( a .= [0,1] ++ a + 1+    ,     sendW8 a (2, 1)+      ..| emptySM+    )  -- greatest common divisor. gcd :: Word16 -> Word16 -> Streams-gcd n0 n1 = do +gcd n0 n1 = do+  let a = varW16 "a"+  let b = varW16 "b"   a .= alg n0 a b   b .= alg n1 b a-  "ans" .= varW16 a == var b-    where alg x0 x1 x2 = [x0] ++ mux (varW16 x1 > var x2) (var x1 - var x2) (var x1) +  let ans = varB "ans"+  ans .= a == b+    where alg x0 x1 x2 = [x0] ++ mux (x1 > x2) (x1 - x2) x1+ -- greatest common divisor of two external vars.  Compare to -- Language.Atom.Example Try  --@@ -101,38 +144,60 @@ -- sample the external variables. gcd' :: Streams gcd' = do -  a .= alg "n" (sub a b)-  b .= alg "m" (sub b a)-  "ans" .= varW16 a == varW16 b && not (var "init")-  "init" .= [True] ++ false-    where sub hi lo = mux (varW16 hi > var lo) (var hi - var lo) (var hi)-          alg ext ex = [0] ++ mux (var "init") (extW16 ext 1) ex+  let n = extW16 "n" 1+  let m = extW16 "m" 1 +  let a = varW16 "a"+  let b = varW16 "b"+  let init = varB "init"+  a .= alg n (sub a b) init+  b .= alg m (sub b a) init++  let ans = varB "ans"+  ans .= a == b && not init++  init .= [True] ++ false++  where sub hi lo = mux (hi > lo) (hi - lo) hi+        alg ext ex init = [0] ++ mux init ext ex+ testCoercions :: Streams testCoercions = do-    "word" .= [1] ++ (varW8 "word") * (-2)-    "int"  .= 1 + castI16 (varW8 "word") +  let word = varW8 "word"+  word .= [1] ++ word * (-2)+  let int = varI16 "int"+  int  .= 1 + cast word  testCoercions2 :: Streams testCoercions2 = do-    b .= [True] ++ not (var b)-    i .= castI8 (varB b)+  let b = varB "b"+  b .= [True] ++ not b+  let i = varI16 "i"+  let j = varI16 "j"+  i .= cast j+  j .= 3  testCoercions3 :: Streams testCoercions3 = do-  x .= [True] ++ not (var x)-  y .= castI32 (varB x) + castI32 (castW8 (varB x)) +  let x = varB "x"+  x .= [True] ++ not x+  let y = varI32 "y"+  y .= cast x + cast x  i8 :: Streams-i8 = do v .= [0, 1] ++ (varI8 v) + 1 +i8 = +  let v = varI8 "v" in v .= [0, 1] ++ v + 1       trap :: Streams trap = do-    "target" .= [0] ++ varW32 "target" + 1 -    "x" .= [0,0] ++ var "y" + varW32 "target" -    "y" .= [0,0] ++ var "x" + varW32 "target" -    +  let target = varW32 "target"+  target .= [0] ++ target + 1  +  let x = varW32 "x"+  let y = varW32 "y"+  x .= [0,0] ++ y + target+  y .= [0,0] ++ x + target+ -- vicious :: Streams -- vicious = do  --     "varExt" .= extW32 "ext" 5 @@ -188,17 +253,24 @@   -- b .= [0] ++ extArrW16 ("gg", varW16 b) 4    -- c .= [True] ++ var c   -- d .= varB c -  e .= [6,7,8] ++ (constW16 3) -- + extArrW16 ("gg", varW16 b) 2+  let e = varW16 "e"+  e .= [6,7,8] ++ 3 -- + extArrW16 ("gg", varW16 b) 2 --  f .= extArrW16 ("gg", varW16 e) 2 + extArrW16 ("gg", varW16 e) 2 -  g .= (extArrW16 ("gg", varW16 e) 1) == (extArrW16 ("gg", varW16 e) 1)+  let g = varB "g"+  let gg = extArrW16 "gg" e +  g .= gg 1 == gg 2   -- h .= [0] ++ drop 1 (varW16 g)   -- t3 :: use an external variable called ext, typed Word32 t99 :: Streams t99 = do-     a .= [0,1] ++ (var a) + extW32 "ext" 8 + extW32 "ext" 8 + extW32 "ext" 1-     b .= [True, False] ++ 2 + var a < 5 + extW32 "_ext" 1+  let ext = extW32 "ext"+  let a = varW32 "a"+  a .= [0,1] ++ a + ext 8 + ext 8 + ext 1++  let b = varB "b"+  b .= [True, False] ++ 2 + a < 5 + ext 1  -- test external idx before after and in the stream it references -- test multiple defs

@@ -8,64 +8,76 @@ import Language.Copilot import Language.Copilot.Libs.Indexes import Language.Copilot.Libs.LTL-import Language.Copilot.Variables  ---------------- -- LTL tests --- ---------------- -testing, output :: Var-testing = "testing"-output = "output"- -- Can be tested with various values of val.  Use the interpreter to see the -- outputs. +testing, output :: Spec Bool+testing = varB "testing"+output = varB "output"+ tSoonest :: Int -> Streams tSoonest val = do    testing .= replicate (val+2) False ++ true-  output  .= soonest val (var testing)+  let out = varI16 "out"+  out     .= soonest val testing  tLatest :: Int -> Streams tLatest val = do    testing .= replicate (val-2) False ++ true-  output  .= latest val (var testing)+  let out = varI16 "out"+  out     .= latest val testing  tAlways :: Int -> Int -> Streams tAlways i1 i2 = do    testing .=    (replicate i1 True P.++ [False]) ++ true-  output  `ltl` always i2 (varB testing)+  output  `ltl` always i2 testing  tNext :: Int -> Streams tNext i1 = do    testing .=    (replicate i1 False P.++ [True]) ++ false-  output  `ltl` next (varB testing)+  output  `ltl` next testing  tFuture :: Int -> Int -> Streams tFuture i1 i2 = do -  testing .=    (replicate i1 False P.++ [True]) ++ varB testing-  output  `ltl` eventually i2 (varB testing)+  testing .=    (replicate i1 False P.++ [True]) ++ testing+  output  `ltl` eventually i2 testing ++c, t0, t1 :: Spec Bool+t0 = varB "t0"+t1 = varB "t1"+c = varB "c"+ tUntil :: Int -> Int -> Int -> Streams tUntil i1 i2 i3 = do -  "t1"   .=    replicate i1 False ++ true-  "t0"   .=    replicate i2 True ++ false-  output `ltl` until i3 (varB "t0") (varB "t1")+  t1   .=    replicate i1 False ++ true+  t0   .=    replicate i2 True ++ false+  output `ltl` until i3 t0 t1  tRelease0 :: Int -> Streams tRelease0 val = output `ltl` release val false true  tRelease1 :: Int -> Int -> Streams tRelease1 i1 i2 = do -  "t1"   .=    replicate i1 True ++ varB c-  c      .=    [False] ++ not (var c)-  "t0"   .=    true-  output `ltl` release i2 (varB "t0") (varB "t1")+  t1   .=    replicate i1 True ++ c+  c    .=    [False] ++ not c+  t0   .=    true+  output `ltl` release i2 t0 t1            testRules :: Streams testRules = do-    "v1" .=    (not true) || Var "v2" -    "v2" .=    [True, False] ++ [True] ++ Var "v3" < extI8 "v4" 5 -    "v3" .=    0 + drop 3 (int8 6) -    "v4" `ltl` always 5 (Var "v1") +  let v1 = varB "v1"+  let v2 = varB "v2"+  let v3 = varI16 "v3"+  let v4 = varB "v4"+  let ext = extI8 "ext" 5 +  v1 .=    (not true) || v2+  v2 .=    [True, False] ++ [True] ++ v3 < cast ext+  v3 .=    0 + drop 3 6+  v4 `ltl` always 5 v1 

@@ -2,101 +2,125 @@  module Language.Copilot.Examples.PTLTLExamples where -import Prelude (($), String, repeat, replicate, IO())+import Prelude (($), repeat, replicate, IO()) import qualified Prelude as P import Data.Map (fromList)  import Language.Copilot import Language.Copilot.Libs.PTLTL-import Language.Copilot.Variables  -- Next examples are for testing of the ptLTL library  -- test of previous tstdatprv :: Streams-tstdatprv = a .= [True, False] ++ varB a +tstdatprv = do+  let a = varB "a"+  a .= [True, False] ++ a                  tprv :: Streams tprv = do+  let c = varB "c"+  let a = varB "a"   tstdatprv -  c `ptltl` (previous $ varB a)+  c `ptltl` previous a  -- test of alwaysBeen tstdatAB ::  Streams-tstdatAB = d .= [True, True, True, True, True, True, True, False] ++ varB d+tstdatAB = do+  let d = varB "d"+  d .= [True, True, True, True, True, True, True, False] ++ d  tAB :: Streams tAB = do+   let f = varB "f"+   let d = varB "d"    tstdatAB -   f `ptltl` (alwaysBeen $ var d)+   f `ptltl` alwaysBeen d  -- test of eventuallyPrev tstdatEP ::  Streams-tstdatEP = g .= [False, False, False, False, False, True, False] ++ varB g +tstdatEP = do+  let g = varB "g"+  g .= [False, False, False, False, False, True, False] ++ g   tEP :: Streams tEP = do+    let h = varB "h"+    let g = varB "g"     tstdatEP -    h `ptltl` (eventuallyPrev $ varB g)+    h `ptltl` eventuallyPrev g +q1, q2, z :: Spec Bool+q1 = varB "q1"+q2 = varB "q2"+z = varB "z"+ -- test of since tstdat1Sin :: Streams-tstdat1Sin = "q1" .= [False, False, False, False, True] ++ true --varB "q1"+tstdat1Sin = q1 .= [False, False, False, False, True] ++ true --varB "q1"  tstdat2Sin :: Streams-tstdat2Sin = "q2" .= [False, False, True, False, False, False, False ] ++ varB "q2"+tstdat2Sin = q2 .= [False, False, True, False, False, False, False ] ++ q2+                    tSince :: Streams  tSince = do     tstdat1Sin      tstdat2Sin -    "z1" `ptltl` (varB "q1" `since` varB "q2")+    z `ptltl` (q1 `since` q2)  -- with external variables -- interface $ setE (emptySM {bMap = fromList [("e1", [True,True ..]), ("e2", [False,False ..])]}) $ interpretOpts tSinExt 20 tSinExt :: Streams  tSinExt = do-  ptltl "z1" $ extB "e1" 2 `since`extB "q2" 3+  let e1 = extB "e1" 2+  let e2 = extB "e2" 3+  z `ptltl` (e1 `since` e2)  tSinExt2 :: Streams  tSinExt2 = do-  a .= not (extB "e1" 2)-  b .= constW16 3 > 2-  s `ptltl` ((extB "e2" 2) `since` (var b))-  t `ptltl` (alwaysBeen $ not (varB a))-  e .= extB "e1" 2 ==> varB d-+  let e1 = extB "e1" 2+  let e2 = extB "e2" 2+  let a = varB "a"+  let s = varB "s"+  let d = varB "d"+  let t = varB "t"+  let e = varB "e" -engineTemp, engineOff, coolerOn, monitor, temp, cooler, off, cnt :: String-engineTemp = "engineTemp"-engineOff  = "engineOff"-coolerOn   = "coolerOn"-monitor    = "trigger"-temp       = "temp"-off        = "off"-cnt        = "cnt"-cooler     = "cooler"+  a .= not e1+  s `ptltl` (e2 `since` d)+  t `ptltl` (alwaysBeen $ not a)+  e .= e1 ==> d  -- "If the engine temperature exeeds 250 degrees, then the engine is shutoff -- within the next 10 periods, and in the period following the shutoff, the -- cooler is engaged and remains engaged." engine :: Streams engine = do-  temp    `ptltl` alwaysBeen (extW8 engineTemp 1 > 250)-  cnt     .=      [0] ++ mux (varB temp && varW8 cnt < 10) -                             (varW8 cnt + 1)-                             (varW8 cnt)-  off     .=      (varW8 cnt >= 10 ==> extB engineOff 1)-  cooler  `ptltl` (extB coolerOn 1 `since` extB engineOff 1)-  monitor .=      varB off && varB cooler+  -- external vars+  let engineTemp = extW8 "engineTemp" 1+  let engineOff  = extB "engineOff" 1+  let coolerOn   = extB "coolerOn" 1+  -- Copilot vars+  let cnt        = varW8 "cnt"+  let temp       = varB "temp"+  let cooler     = varB "cooler"+  let off        = varB "off"+  let monitor    = varB "monitor" +  temp    `ptltl` (alwaysBeen (engineTemp > 250))+  cnt     .=      [0] ++ mux (temp && cnt < 10) (cnt + 1) cnt+  off     .=      cnt >= 10 ==> engineOff+  cooler  `ptltl` (coolerOn `since` engineOff)+  monitor .=      off && cooler+ engineRun :: IO () engineRun =    interpret engine 40 $      setE (emptySM { bMap = fromList -                            [ (engineOff, replicate 8 False P.++ repeat True)-                            , (coolerOn, replicate 9 False P.++ repeat True)+                            [ ("engineOff", replicate 8 False P.++ repeat True)+                            , ("coolerOn", replicate 9 False P.++ repeat True)                             ]-                  , w8Map = fromList [(engineTemp, [99,100..])]+                  , w8Map = fromList [("engineTemp", [99,100..])]                   }) baseOpts 

@@ -4,18 +4,25 @@ import Language.Copilot.Core import Language.Copilot.Language import Language.Copilot.Interface-import Language.Copilot.Variables import Language.Copilot.PrettyPrinter import Language.Copilot.Libs.Statistics  t0 :: Streams t0 = do-  a .= [0..5] ++ (varW16 a) + 6-  "min" .= min 3 (varW16 a)-  "max" .= max 3 (varW16 a)-  "sum" .= sum 3 (varW16 a)+  let minV = varW16 "min"+  let maxV = varW16 "max"+  let sumV = varW16 "sum"+  let a = varW16 "a" +  a .= [0..5] ++ a + 6+  minV .= min 3 a+  maxV .= max 3 a+  sumV .= sum 3 a+ tMean :: Streams tMean = do-  a .= [0..5] ++ (varD a) + 6-  "out" .= mean 4 (varD a)+  let a = varD "a"+  let out = varD "out"++  a .= [0..5] ++ a + 6+  out .= mean 4 a

@@ -16,10 +16,8 @@         -- * Division         Fractional((/)),         mux,---        CastIntTo(..),-        -- * The next functions are used only to coerce the type of their argument-        bool, int8, int16, int32, int64,-        word8, word16, word32, word64, float, double,+        varB, varI8, varI16, varI32, varI64,+        varW8, varW16, varW32, varW64, varF, varD,         -- * The next functions provide easier access to typed external variables.         extB, extI8, extI16, extI32, extI64,         extW8, extW16, extW32, extW64, extF, extD,@@ -29,21 +27,14 @@         -- * Set of operators from which to choose during the generation of random streams         opsF, opsF2, opsF3,         -- * Constructs of the copilot language-        var, drop, (++), (.=), (..|), -        -- * The next functions are typed variable declarations to help the type-checker.-        varB, varI8, varI16, varI32, varI64,-        varW8, varW16, varW32, varW64, varF, varD,+        drop, (++), (.=), (..|),          -- * The next functions help typing the send operations         -- Warning: there is no typechecking of that yet         -- sendB, sendI8, sendI16, sendI32, sendI64,         sendW8, -- , sendW16, sendW32, sendW64, sendF, sendD-        -- * Typed constant declarations.-        constB, constI8, constI16, constI32, constI64,-        constW8, constW16, constW32, constW64, constF, constD,-        -- * Cast functions (the name tells you what you're casting *into*).-        castI8, castI16, castI32, castI64,-        castW8, castW16, castW32, castW64,-        -- * Constants+        -- * Safe casting+        cast,+        -- * Boolean stream constants         true, false     ) where @@ -103,7 +94,8 @@  -- | Cast 'a' into 'b'.  We only allow "safe casts" to larger types. class Streamable a => Castable a where-  cast :: (Streamable b, A.IntegralE b) => Spec a -> Spec b+  castFrom :: (Streamable b, A.IntegralE b) => Spec a -> Spec b+  cast :: (Castable b, Streamable b) => Spec b -> Spec a  castErr :: String -> A.Type -> String castErr toT fromT = "Error: cannot cast type " P.++ show fromT @@ -111,156 +103,84 @@                     P.++ "not to change sign and to larger types are allowed."  instance Castable Bool where-  cast = F (\b -> if b then 1 else 0)+  castFrom = F (\b -> if b then 1 else 0)            (\b -> A.mux b 1 0)+  cast x =  error $ castErr "Bool" (getAtomType x)  instance Castable Word8 where-  cast = F (P.fromInteger . P.toInteger) +  castFrom = F (P.fromInteger . P.toInteger)             (A.Retype . A.ue)+  cast x =  case getAtomType x of+    A.Bool   -> castFrom x+    t        -> error $ castErr "Word8" t  instance Castable Word16 where-  cast = F (P.fromInteger . P.toInteger) +  castFrom = F (P.fromInteger . P.toInteger)             (A.Retype . A.ue)+  cast x =  case getAtomType x of+    A.Bool   -> castFrom x+    A.Word8  -> castFrom x+    t        -> error $ castErr "Word16" t  instance Castable Word32 where-  cast = F (P.fromInteger . P.toInteger) +  castFrom = F (P.fromInteger . P.toInteger)             (A.Retype . A.ue)+  cast x =  case getAtomType x of+    A.Bool   -> castFrom x+    A.Word8  -> castFrom x+    A.Word16 -> castFrom x+    t        -> error $ castErr "Word32" t  instance Castable Word64 where-  cast = F (P.fromInteger . P.toInteger) +  castFrom = F (P.fromInteger . P.toInteger)             (A.Retype . A.ue)+  cast x =   case getAtomType x of+    A.Bool   -> castFrom x+    A.Word8  -> castFrom x+    A.Word16 -> castFrom x+    A.Word32 -> castFrom x+    t        -> error $ castErr "Word64" t  instance Castable Int8 where-  cast = F (P.fromInteger . P.toInteger) +  castFrom = F (P.fromInteger . P.toInteger)             (A.Retype . A.ue)+  cast x =  case getAtomType x of+    A.Bool   -> castFrom x+    t        -> error $ castErr "Int8" t  instance Castable Int16 where-  cast = F (P.fromInteger . P.toInteger) +  castFrom = F (P.fromInteger . P.toInteger)             (A.Retype . A.ue)+  cast x = case getAtomType x of+    A.Bool   -> castFrom x+    A.Int8   -> castFrom x+    A.Word8  -> castFrom x+    t        -> error $ castErr "Int16" t  instance Castable Int32 where-  cast = F (P.fromInteger . P.toInteger) +  castFrom = F (P.fromInteger . P.toInteger)             (A.Retype . A.ue)+  cast x =  case getAtomType x of+    A.Bool   -> castFrom x+    A.Int8  -> castFrom x+    A.Int16 -> castFrom x+    A.Word8  -> castFrom x+    A.Word16  -> castFrom x+    t        -> error $ castErr "Int32" t  instance Castable Int64 where-  cast = F (P.fromInteger . P.toInteger) +  castFrom = F (P.fromInteger . P.toInteger)             (A.Retype . A.ue)--castW8 :: (Streamable a, Castable a) => Spec a -> Spec Word8-castW8 x = -  case getAtomType x of-    A.Bool   -> cast x-    t        -> error $ castErr "Word8" t--castW16 :: (Streamable a, Castable a) => Spec a -> Spec Word16-castW16 x = -  case getAtomType x of-    A.Bool   -> cast x-    A.Word8  -> cast x-    t        -> error $ castErr "Word16" t--castW32 :: (Streamable a, Castable a) => Spec a -> Spec Word32-castW32 x = -  case getAtomType x of-    A.Bool   -> cast x-    A.Word8  -> cast x-    A.Word16 -> cast x-    t        -> error $ castErr "Word32" t--castW64 :: (Streamable a, Castable a) => Spec a -> Spec Word64-castW64 x = -  case getAtomType x of-    A.Bool   -> cast x-    A.Word8  -> cast x-    A.Word16 -> cast x-    A.Word32 -> cast x-    t        -> error $ castErr "Word64" t--castI8 :: (Streamable a, Castable a) => Spec a -> Spec Int8-castI8 x = -  case getAtomType x of-    A.Bool   -> cast x-    t        -> error $ castErr "Int8" t--castI16 :: (Streamable a, Castable a) => Spec a -> Spec Int16-castI16 x = -  case getAtomType x of-    A.Bool   -> cast x-    A.Int8   -> cast x-    A.Word8  -> cast x-    t        -> error $ castErr "Int16" t--castI32 :: (Streamable a, Castable a) => Spec a -> Spec Int32-castI32 x = -  case getAtomType x of-    A.Bool   -> cast x-    A.Int8  -> cast x-    A.Int16 -> cast x-    A.Word8  -> cast x-    A.Word16  -> cast x-    t        -> error $ castErr "Int32" t--castI64 :: (Streamable a, Castable a) => Spec a -> Spec Int64-castI64 x = -  case getAtomType x of-    A.Bool   -> cast x-    A.Int8  -> cast x-    A.Int16 -> cast x-    A.Int32 -> cast x-    A.Word8  -> cast x-    A.Word16  -> cast x-    A.Word32  -> cast x+  cast x =  case getAtomType x of+    A.Bool   -> castFrom x+    A.Int8  -> castFrom x+    A.Int16 -> castFrom x+    A.Int32 -> castFrom x+    A.Word8  -> castFrom x+    A.Word16  -> castFrom x+    A.Word32  -> castFrom x     t        -> error $ castErr "Int64" t --- F (P.fromInteger . P.toInteger) ---             (A.Retype . A.ue . (`A.mod_` (size 16))---                . A.Retype . A.ue)----- instance CastIntTo Word8 where---     cast = F (P.fromInteger . P.toInteger) ---              (A.Retype . A.ue . (`A.mod_` (size 8))---                  . A.Retype . A.ue)--- instance CastIntTo Word16 where---     cast = F (P.fromInteger . P.toInteger) ---              (A.Retype . A.ue . (`A.mod_` (size 16))---                  . A.Retype . A.ue)--- instance CastIntTo Word32 where---     cast = F (P.fromInteger . P.toInteger) ---              (A.Retype . A.ue . (`A.mod_` (size 32))---                  . A.Retype . A.ue)--- instance CastIntTo Word64 where---     cast = F (P.fromInteger . P.toInteger) ---              (A.Retype . A.ue . (`A.mod_` (size 64))---                  . A.Retype . A.ue)---- Ints---- XXX this is how Robin had casts.  Can't we do it more simply?--- instance CastIntTo Int8 where---     cast = F (P.fromInteger . P.toInteger) ---              (A.Retype . A.ue . ---                  (\x -> ((x P.+ sMinOne) `A.mod_` s) P.-  s)---                    . A.Retype . A.ue)---       where s = size 8---             sMinOne = size 7--- instance CastIntTo Int8 where---     cast = F (P.fromInteger . P.toInteger) ---              (A.Retype . A.ue . (`A.mod_` (size 7)) ---                    . A.Retype . A.ue)--- instance CastIntTo Int16 where---     cast = F (P.fromInteger . P.toInteger) ---              (A.Retype . A.ue . (`A.mod_` (size 15)) ---                    . A.Retype . A.ue)--- instance CastIntTo Int32 where---     cast = F (P.fromInteger . P.toInteger) ---              (A.Retype . A.ue . (`A.mod_` (size 31)) ---                    . A.Retype . A.ue)--- instance CastIntTo Int64 where---     cast = F (P.fromInteger . P.toInteger) ---              (A.Retype . A.ue . (`A.mod_` (size 63))---                    . A.Retype . A.ue)- -- | Beware : both sides are executed, even if the result of one is later discarded mux :: (Streamable a) => Spec Bool -> Spec a -> Spec a -> Spec a mux = F3 (\ b x y -> if b then x else y) A.mux@@ -268,29 +188,6 @@ infix 5 ==, /=, <, <=, >=, > infixr 4 ||, &&, ^, ==> --- Used for helping ghc in infering the type of the streams-bool :: Spec Bool -> Spec Bool-int8 :: Spec Int8 -> Spec Int8-int16 :: Spec Int16 -> Spec Int16-int32 :: Spec Int32 -> Spec Int32-int64 :: Spec Int64 -> Spec Int64-word8 :: Spec Word8 -> Spec Word8-word16 :: Spec Word16 -> Spec Word16-word32 :: Spec Word32 -> Spec Word32-word64 :: Spec Word64 -> Spec Word64-float :: Spec Float -> Spec Float-double :: Spec Double -> Spec Double-bool = P.id-int8 = P.id-int16 = P.id-int32 = P.id-int64 = P.id-word8 = P.id-word16 = P.id-word32 = P.id-word64 = P.id-float = P.id-double = P.id  -- Used for easily producing, and coercing PVars @@ -319,28 +216,28 @@ extD = PVar A.Double  -- for arrays -extArrB :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Bool-extArrB = \(v, idx) ph -> PArr A.Bool (v, idx) ph-extArrI8 :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Int8-extArrI8 = \(v, idx) ph -> PArr A.Int8 (v, idx) ph-extArrI16 :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Int16-extArrI16 = \(v, idx) ph -> PArr A.Int16 (v, idx) ph-extArrI32 :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Int32-extArrI32 = \(v, idx) ph -> PArr A.Int32 (v, idx) ph-extArrI64 :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Int64-extArrI64 = \(v, idx) ph -> PArr A.Int64 (v, idx) ph-extArrW8 :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Word8-extArrW8 = \(v, idx) ph -> PArr A.Word8 (v, idx) ph-extArrW16 :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Word16-extArrW16 = \(v, idx) ph -> PArr A.Word16 (v, idx) ph-extArrW32 :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Word32-extArrW32 = \(v, idx) ph -> PArr A.Word32 (v, idx) ph-extArrW64 :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Word64-extArrW64 = \(v, idx) ph -> PArr A.Word64 (v, idx) ph-extArrF :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Float-extArrF = \(v, idx) ph -> PArr A.Float (v, idx) ph-extArrD :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Double-extArrD = \(v, idx) ph -> PArr A.Double (v, idx) ph+extArrB ::  (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Bool+extArrB = \v idx ph -> PArr A.Bool (v, idx) ph+extArrI8 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Int8+extArrI8 = \v idx ph -> PArr A.Int8 (v, idx) ph+extArrI16 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Int16+extArrI16 = \v idx ph -> PArr A.Int16 (v, idx) ph+extArrI32 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Int32+extArrI32 = \v idx ph -> PArr A.Int32 (v, idx) ph+extArrI64 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Int64+extArrI64 = \v idx ph -> PArr A.Int64 (v, idx) ph+extArrW8 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Word8+extArrW8 = \v idx ph -> PArr A.Word8 (v, idx) ph+extArrW16 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Word16+extArrW16 = \v idx ph -> PArr A.Word16 (v, idx) ph+extArrW32 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Word32+extArrW32 = \v idx ph -> PArr A.Word32 (v, idx) ph+extArrW64 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Word64+extArrW64 = \v idx ph -> PArr A.Word64 (v, idx) ph+extArrF :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Float+extArrF = \v idx ph -> PArr A.Float (v, idx) ph+extArrD :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Double+extArrD = \v idx ph -> PArr A.Double (v, idx) ph   ---- Sets of operators for Tests.Random.hs -------------------------------------@@ -532,11 +429,9 @@  ---- Constructs of the language ------------------------------------------------ --- | Stream variable reference-var :: Streamable a => Var -> Spec a-var v = Var v --- If a generic 'var' declaration is insufficient for the type-checker to determine the type, a monomorphic var operator can be used+-- If a generic 'var' declaration is insufficient for the type-checker to+-- determine the type, a monomorphic var operator can be used. varB :: Var -> Spec Bool varB = Var varI8 :: Var -> Spec Int8@@ -571,8 +466,12 @@ sendI32 v (ph, port) = Send (v, ph, port) sendI64 :: Var -> (Phase, Port) -> Send Int64 sendI64 v (ph, port) = Send (v, ph, port) -}-sendW8 :: Var -> (Phase, Port) -> Send Word8-sendW8 v (ph, port) = Send (v, ph, port)+sendW8 :: Spec Word8 -> (Phase, Port) -> Send Word8+sendW8 s (ph, port) = +  case s of+    Var v -> Send (v, ph, port)+    _     -> error $ "You provided spec " P.++ show s +                P.++ " where you needed to give a variable." {- sendW16 :: Var -> (Phase, Port) -> Send Word16 sendW16 v (ph, port) = Send (v, ph, port) sendW32 :: Var -> (Phase, Port) -> Send Word32@@ -585,36 +484,9 @@ sendD v (ph, port) = Send (v, ph, port) -}  --constB :: Bool -> Spec Bool-constB = Const- true, false :: Spec Bool-true = constB True-false = constB False---- | Constant streams-constI8 :: Int8 -> Spec Int8-constI8 = Const-constI16 :: Int16 -> Spec Int16-constI16 = Const-constI32 :: Int32 -> Spec Int32-constI32 = Const-constI64 :: Int64 -> Spec Int64-constI64 = Const-constW8 :: Word8 -> Spec Word8-constW8 = Const -constW16 :: Word16 -> Spec Word16-constW16 = Const-constW32 :: Word32 -> Spec Word32-constW32 = Const-constW64 :: Word64 -> Spec Word64-constW64 = Const-constF :: Float -> Spec Float-constF = Const-constD :: Double -> Spec Double-constD = Const-+true = Const True+false = Const False  -- | Drop @i@ elements from a stream. drop :: Streamable a => Int -> Spec a -> Spec a@@ -625,8 +497,12 @@ ls ++ s = Append ls s  -- | Define a stream variable.-(.=) :: Streamable a => Var -> Spec a -> Streams-v .= s = tell (updateSubMap (M.insert v s) emptySM) +(.=) :: Streamable a => Spec a -> Spec a -> Streams+v .= s = +  case v of+    Var var -> tell (updateSubMap (M.insert var s) emptySM) +    _       -> error $ "Copilot error: you tried to use specification " P.++ show v +                 P.++ " where you need to use a variable."  -- | Allows to build a @'Sends'@ from specification (..|) :: Sendable a => Send a -> Sends -> Sends

@@ -27,7 +27,7 @@   )    where -import Prelude (Int, ($), String)+import Prelude (Int, ($), String, error) import qualified Prelude as P import Data.List (foldl1) @@ -36,11 +36,14 @@ import Language.Copilot.Libs.Indexes import Language.Copilot.Libs.ErrorChks -ltl :: Var -> (Var -> Streams) -> Streams+ltl :: Spec Bool -> (Spec Bool -> Streams) -> Streams ltl v f = f v -tmpName :: Var -> String -> Var-tmpName v name = v P.++ "_" P.++ name+tmpName :: Spec Bool -> String -> Spec Bool+tmpName v name = +  case v of +    Var var -> varB (var P.++ "_" P.++ name)+    _       -> error $ "Copilot: " P.++ "error in tmpName in LTL.hs."  -- | Property @s@ holds for the next @n@ periods.  We require @n >= 0@. If @n == -- 0@, then @s@ holds in the current period.  E.g., if @p = always 2 s@, then we@@ -50,9 +53,9 @@ -- s => T T T F T T T T ... -- p => T F F F T T ... -- @-always :: Int -> Spec Bool -> Var -> Streams+always :: Int -> Spec Bool -> Spec Bool -> Streams always n s v = do-  v .= (nPosChk "always" n $ foldl1 (&&) [drop x (varB s') | x <- [0..n]])+  v .= (nPosChk "always" n $ foldl1 (&&) [drop x s' | x <- [0..n]])   s' .= s   where s' = tmpName v "always" @@ -63,9 +66,9 @@ -- next s => F F T F F T F ... -- @ -- Note: s must have sufficient history to drop a value from it.-next :: Spec Bool -> Var -> Streams+next :: Spec Bool -> Spec Bool -> Streams next s v = do -  v  .= drop 1 (varB s')+  v  .= drop 1 s'   s' .= s   where s' = tmpName v "next" @@ -77,21 +80,21 @@ -- s => F F F T F F F T ... -- p => F T T T F T T T ... -- @-eventually :: Int -> Spec Bool -> Var -> Streams+eventually :: Int -> Spec Bool -> Spec Bool -> Streams eventually n s v = do-  v .= (nPosChk "eventually" n $ foldl1 (||) [drop x (varB s') | x <- [0..n]])+  v .= (nPosChk "eventually" n $ foldl1 (||) [drop x s' | x <- [0..n]])   s' .= s   where s' = tmpName v "eventually"  -- | @until n s0 s1@ means that @eventually n s1@, and up until at least the -- period before @s1@ holds, @s0@ continuously holds.-until :: Int -> Spec Bool -> Spec Bool -> Var -> Streams+until :: Int -> Spec Bool -> Spec Bool -> Spec Bool -> Streams until n s0 s1 v = do   v'  .= (nPosChk "until" n $              (   (whenS0 < 0) -- s0 didn't fail within n periods.-             || (soonest n (varB s1') <= whenS0))) -- s0 failed at some point before n.-  v'' `ltl` eventually n (varB s1') -- guarantees that soonest n s1 >= 0-  v   .= (varB v') && (varB v'')+             || (soonest n s1' <= whenS0))) -- s0 failed at some point before n.+  v'' `ltl` eventually n s1' -- guarantees that soonest n s1 >= 0+  v   .= v' && v''   s0' .= s0   s1' .= s1   where @@ -99,18 +102,18 @@     s1' = tmpName v "until_1"     v''  = tmpName v "until_2"     v' = tmpName v "until3"-    whenS0 = soonestFail n (varB s0')+    whenS0 = soonestFail n s0'  -- | @release n s0 s1@ means that either @always n s1@, or @s1@ holds up to and -- including the period at which @s0@ becomes true.-release :: Int -> Spec Bool -> Spec Bool -> Var -> Streams+release :: Int -> Spec Bool -> Spec Bool -> Spec Bool -> Streams release n s0 s1 v = do   v' .= (nPosChk "release" n $ (   (whenS0 >= 0) -- s0 becomes true at some point                                 && (whenS0 < whenS1))) -- and when s0 becomes true,                                                        -- is strictly sooner than                                                        -- when s1 fails.-  v'' `ltl` always n (varB s1') -- s1 never fails-  v   .= (varB v') || (varB v'')+  v'' `ltl` always n s1' -- s1 never fails+  v   .= v' || v''   s0' .= s0   s1' .= s1   where @@ -118,5 +121,5 @@     s1' = tmpName v "release1"     v''  = tmpName v "release2"     v' = tmpName v "release3"-    whenS1 = soonestFail n (varB s1')-    whenS0 = soonest n (varB s0')+    whenS1 = soonestFail n s1'+    whenS0 = soonest n s0'

@@ -13,47 +13,50 @@   ( ptltl, since, alwaysBeen, eventuallyPrev, previous )    where -import Prelude (String, ($))+import Prelude (String, ($), error) import qualified Prelude as P  import Language.Copilot.Core import Language.Copilot.Language -tmpName :: Var -> String -> Var-tmpName v name = v P.++ "_" P.++ name+tmpName :: Spec Bool -> String -> Spec Bool+tmpName v name = +  case v of+    Var var -> varB (var P.++ "_" P.++ name)+    _       -> error "Copilot error in tmpName in PTLTL.hs." -ptltl :: Var -> (Var -> Streams) -> Streams+ptltl :: Spec Bool -> (Spec Bool -> Streams) -> Streams ptltl v f = f v  -- | Did @s@ hold in the previous period?-previous :: Spec Bool -> Var -> Streams+previous :: Spec Bool -> Spec Bool -> Streams previous s v = v .= [False] ++ s    -- | Has @s@ always held (up to and including the current state)?-alwaysBeen :: Spec Bool -> Var -> Streams+alwaysBeen :: Spec Bool -> Spec Bool -> Streams alwaysBeen s v = do-     tmp .= [True] ++ varB v-     v   .= varB tmp && varB s'+     tmp .= [True] ++ v+     v   .= tmp && s'      s'  .= s   where      tmp = tmpName v "ab_tmp"     s'  = tmpName v "ab"      -- | Did @s@ hold at some time in the past (including the current state)?-eventuallyPrev :: Spec Bool -> Var -> Streams+eventuallyPrev :: Spec Bool -> Spec Bool -> Streams eventuallyPrev s v = do-     tmp .= [False] ++ (var tmp) || varB s'-     v   .= varB s' || varB tmp+     tmp .= [False] ++ tmp || s'+     v   .= s' || tmp      s'  .= s   where      tmp = tmpName v "ep_tmp"     s'  = tmpName v "ep"  -- | Once @s2@ holds, in the following state (period), does @s1@ continuously hold? -since ::  Spec Bool -> Spec Bool -> Var -> Streams+since ::  Spec Bool -> Spec Bool -> Spec Bool -> Streams since s1 s2 v = do     tmp `ptltl` (eventuallyPrev $ [False] ++ s2) -- has s2 been true at some point?-    v   `ptltl` (alwaysBeen $ varB tmp ==> varB s1')+    v   `ptltl` (alwaysBeen $ tmp ==> s1')     s1' .= s1     s2' .= s2   where 

@@ -1,32 +0,0 @@--- | Variable names--module Language.Copilot.Variables where--a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,u,v,w,x,y,z :: String--a = "a"-b = "b"-c = "c"-d = "d"-e = "e"-f = "f"-g = "g"-h = "h"-i = "i"-j = "j"-k = "k"-l = "l"-m = "m"-n = "n"-o = "o"-p = "p"-q = "q"-r = "r"-s = "s"-t = "t"-u = "u"-v = "v"-w = "w"-x = "x"-y = "y"-z = "z"

@@ -4,13 +4,14 @@ Copilot. Here's a Copilot program that computes the Fibonacci sequence (over Word 64s) and tests for even numbers: - fib :: Streams fib = do-  "fib" .= [0,1] ++ var "fib" + (drop 1 $ varW64 "fib")-  "t" .= even (var "fib")+  let f = varW64 "f"+  let t   = varB "t"+  f .= [0,1] ++ f + (drop 1 f)+  t .= even f     where even :: Spec Word64 -> Spec Bool-          even w = w `mod` const 2 == const 0    +          even w' = w' `mod` 2 == 0  Copilot contains an interpreter, a compiler, and uses a model-checker to check the correctness of your program. The compiler generates constant time and@@ -34,6 +35,11 @@  ******************************************************************************* Release notes++* Copilot-0.26+  * Variables are now specs, not strings.  This gives stream expressions a type,+    so no need for constant functions, monomorphic cast functions, or var+    annotations in expressions.  Examples updated to reflect the change.  * Copilot-0.25 

@@ -1,5 +1,5 @@ name:                copilot-version:             0.25+version:             0.26 cabal-version:       >= 1.2 license:             BSD3 license-file:        LICENSE@@ -15,10 +15,12 @@                      .                      > fib :: Streams                      > fib = do-                     >  "fib" .= [0,1] ++ var "fib" + (drop 1 $ varW64 "fib")-                     >  "t" .= even (var "fib")-                     >    where even :: Spec Word64 -> Spec Bool-                     >          even w = w `mod` const 2 == const 0    +                     >  let f = varW64 "fib"+                     >  let t = varB "t"+                     >  f .= [0,1] ++ f + (drop 1 f)+                     >  t .= even f+                     >    where even :: Spaec Word64 -> Spec Bool+                     >          even w' = w' `mod` 2 == 0                      .                      Copilot contains an interpreter, a compiler, and uses a model-checker to check                      the correctness of your program. The compiler generates constant time and@@ -56,7 +58,6 @@                      Language.Copilot.Tests.Random                      Language.Copilot.Dispatch                      Language.Copilot.Interface-                     Language.Copilot.Variables                      Language.Copilot.Libs.ErrorChks                      Language.Copilot.Libs.PTLTL                      Language.Copilot.Libs.LTL