copilot-core 3.9 → 3.10

raw patch · 14 files changed

+157/−104 lines, 14 filesdep −mtlPVP ok

version bump matches the API change (PVP)

Dependencies removed: mtl

API changes (from Hackage documentation)

Files

• CHANGELOG +10/−0
• copilot-core.cabal +3/−4
• src/Copilot/Core.hs +5/−1
• src/Copilot/Core/External.hs +1/−0
• src/Copilot/Core/Interpret.hs +1/−1
• src/Copilot/Core/Interpret/Eval.hs +9/−7
• src/Copilot/Core/PrettyDot.hs +1/−1
• src/Copilot/Core/PrettyPrint.hs +1/−1
• src/Copilot/Core/Type/Show.hs +3/−69
• src/Copilot/Core/Type/ShowInternal.hs +77/−0
• tests/Main.hs +2/−3
• tests/Test/Copilot/Core/External.hs +4/−0
• tests/Test/Copilot/Core/Interpret/Eval.hs +36/−17
• tests/Test/Copilot/Core/Type/Show.hs +4/−0

@@ -1,3 +1,13 @@+2022-07-07+        * Version bump (3.10). (#356)+        * Fix error in test case generation; enable CLI args in tests. (#337)+        * Remove unnecessary dependencies from Cabal package. (#324)+        * Deprecate Copilot.Core.External. (#322)+        * Remove duplicated compiler option. (#328)+        * Hide type Copilot.Core.Type.Show.ShowWit. (#348)+        * Deprecate Copilot.Core.Type.Show. (#330)+        * Update repo info in cabal file. (#333)+ 2022-05-06         * Version bump (3.9). (#320)         * Compliance with style guide (partial). (#316)

@@ -1,6 +1,6 @@ cabal-version:       >=1.10 name:                copilot-core-version:             3.9+version:             3.10 synopsis:            An intermediate representation for Copilot. description:   Intermediate representation for Copilot.@@ -29,7 +29,7 @@ source-repository head     type:       git     location:   https://github.com/Copilot-Language/copilot.git-    subdir:     lib/copilot-core+    subdir:     copilot-core  library @@ -39,13 +39,11 @@    ghc-options:     -Wall-    -fwarn-tabs     -fno-warn-orphans    build-depends:     base       >= 4.9 && < 5,     pretty     >= 1.0 && < 1.2,-    mtl        >= 2.0 && < 2.3,     dlist    exposed-modules:@@ -69,6 +67,7 @@      Copilot.Core.Error     Copilot.Core.Interpret.Render+    Copilot.Core.Type.ShowInternal  test-suite unit-tests   type:

@@ -19,6 +19,10 @@ -- ("Copilot.Core.PrettyPrint").  {-# LANGUAGE Safe #-}+-- The following warning is enabled in this module so that the import of+-- Copilot.Core.External does not give rise to a warning. It can be removed+-- when that module is removed from the implementation.+{-# OPTIONS_GHC -fno-warn-deprecations #-}  module Copilot.Core   ( module Copilot.Core.Expr@@ -32,7 +36,7 @@   ) where  import Copilot.Core.Expr-import Copilot.Core.External+import Copilot.Core.External -- See GHC flag enabled above import Copilot.Core.Operators import Copilot.Core.Spec import Copilot.Core.Type

@@ -6,6 +6,7 @@  -- | Internal Copilot Core representation of Copilot externs. module Copilot.Core.External+  {-# DEPRECATED "This module is deprecated in Copilot 3.10." #-}   ( ExtVar (..)   , externVars   ) where

@@ -12,7 +12,7 @@ import Copilot.Core import Copilot.Core.Interpret.Eval import Copilot.Core.Interpret.Render-import Copilot.Core.Type.Show (ShowType(..))+import Copilot.Core.Type.ShowInternal (ShowType(..))  -- | Output format for the results of a Copilot spec interpretation. data Format = Table | CSV

@@ -12,15 +12,17 @@   , Output   , ExecTrace (..)   , eval+  , ShowType (..)   ) where -import Copilot.Core           (Expr (..), Field (..), Id, Name, Observer (..),-                               Op1 (..), Op2 (..), Op3 (..), Spec, Stream (..),-                               Trigger (..), Type (Struct), UExpr (..),-                               arrayelems, specObservers, specStreams,-                               specTriggers)-import Copilot.Core.Error     (badUsage)-import Copilot.Core.Type.Show (ShowType, showWithType)+import Copilot.Core                   (Expr (..), Field (..), Id, Name,+                                       Observer (..), Op1 (..), Op2 (..),+                                       Op3 (..), Spec, Stream (..),+                                       Trigger (..), Type (Struct), UExpr (..),+                                       arrayelems, specObservers, specStreams,+                                       specTriggers)+import Copilot.Core.Error             (badUsage)+import Copilot.Core.Type.ShowInternal (ShowType (..), showWithType)  import           Prelude hiding (id) import qualified Prelude as P

@@ -11,7 +11,7 @@   ) where  import Copilot.Core-import Copilot.Core.Type.Show (showWithType, ShowType(..), showType)+import Copilot.Core.Type.ShowInternal (showWithType, ShowType(..), showType) import Prelude hiding (id, (<>)) import Text.PrettyPrint.HughesPJ import Data.List (intersperse)

@@ -12,7 +12,7 @@  import Copilot.Core import Copilot.Core.Error (impossible)-import Copilot.Core.Type.Show (showWithType, ShowType(..), showType)+import Copilot.Core.Type.ShowInternal (showWithType, ShowType(..), showType) import Prelude hiding (id, (<>)) import Text.PrettyPrint.HughesPJ import Data.List (intersperse)

@@ -1,77 +1,11 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE GADTs                     #-}-{-# LANGUAGE Safe                      #-}- -- | Show Copilot Core types and typed values. module Copilot.Core.Type.Show-  ( ShowWit (..)-  , showWithType+  {-# DEPRECATED "This module is deprecated in Copilot 3.10." #-}+  ( showWithType   , ShowType(..)   , showType   ) where -import Copilot.Core.Type---- | Witness datatype for showing a value, used by 'showWithType'.-{-# DEPRECATED ShowWit "This type is deprecated in Copilot 3.7." #-}-data ShowWit a = Show a => ShowWit---- | Turn a type into a show witness.-showWit :: Type a -> ShowWit a-showWit t =-  case t of-    Bool   -> ShowWit-    Int8   -> ShowWit-    Int16  -> ShowWit-    Int32  -> ShowWit-    Int64  -> ShowWit-    Word8  -> ShowWit-    Word16 -> ShowWit-    Word32 -> ShowWit-    Word64 -> ShowWit-    Float  -> ShowWit-    Double -> ShowWit-    Array t -> ShowWit-    Struct t -> ShowWit---- | Show Copilot Core type.-showType :: Type a -> String-showType t =-  case t of-    Bool   -> "Bool"-    Int8   -> "Int8"-    Int16  -> "Int16"-    Int32  -> "Int32"-    Int64  -> "Int64"-    Word8  -> "Word8"-    Word16 -> "Word16"-    Word32 -> "Word32"-    Word64 -> "Word64"-    Float  -> "Float"-    Double -> "Double"-    Array t -> "Array " ++ showType t-    Struct t -> "Struct"---- Are we proving equivalence with a C backend, in which case we want to show--- Booleans as '0' and '1'.---- | Target language for showing a typed value. Used to adapt the--- representation of booleans.-data ShowType = C | Haskell---- | Show a value. The representation depends on the type and the target--- language. Booleans are represented differently depending on the backend.-showWithType :: ShowType -> Type a -> a -> String-showWithType showT t x =-  case showT of-    C         -> case t of-                   Bool -> if x then "1" else "0"-                   _    -> sw-    Haskell   -> case t of-                   Bool -> if x then "true" else "false"-                   _    -> sw-  where-  sw = case showWit t of-         ShowWit -> show x+import Copilot.Core.Type.ShowInternal (ShowType (..), showType, showWithType)

@@ -0,0 +1,77 @@+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.++{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE GADTs                     #-}+{-# LANGUAGE Safe                      #-}++-- | Show Copilot Core types and typed values.+module Copilot.Core.Type.ShowInternal+  ( showWithType+  , ShowType(..)+  , showType+  ) where++import Copilot.Core.Type++-- Are we proving equivalence with a C backend, in which case we want to show+-- Booleans as '0' and '1'.++-- | Target language for showing a typed value. Used to adapt the+-- representation of booleans.+data ShowType = C | Haskell++-- | Show a value. The representation depends on the type and the target+-- language. Booleans are represented differently depending on the backend.+showWithType :: ShowType -> Type a -> a -> String+showWithType showT t x =+  case showT of+    C         -> case t of+                   Bool -> if x then "1" else "0"+                   _    -> sw+    Haskell   -> case t of+                   Bool -> if x then "true" else "false"+                   _    -> sw+  where+  sw = case showWit t of+         ShowWit -> show x++-- | Show Copilot Core type.+showType :: Type a -> String+showType t =+  case t of+    Bool   -> "Bool"+    Int8   -> "Int8"+    Int16  -> "Int16"+    Int32  -> "Int32"+    Int64  -> "Int64"+    Word8  -> "Word8"+    Word16 -> "Word16"+    Word32 -> "Word32"+    Word64 -> "Word64"+    Float  -> "Float"+    Double -> "Double"+    Array t -> "Array " ++ showType t+    Struct t -> "Struct"++-- * Auxiliary show instance++-- | Witness datatype for showing a value, used by 'showWithType'.+data ShowWit a = Show a => ShowWit++-- | Turn a type into a show witness.+showWit :: Type a -> ShowWit a+showWit t =+  case t of+    Bool   -> ShowWit+    Int8   -> ShowWit+    Int16  -> ShowWit+    Int32  -> ShowWit+    Int64  -> ShowWit+    Word8  -> ShowWit+    Word16 -> ShowWit+    Word32 -> ShowWit+    Word64 -> ShowWit+    Float  -> ShowWit+    Double -> ShowWit+    Array t -> ShowWit+    Struct t -> ShowWit

@@ -2,8 +2,7 @@ module Main where  -- External imports-import Data.Monoid    (mempty)-import Test.Framework (Test, defaultMainWithOpts)+import Test.Framework (Test, defaultMain)  -- Internal library modules being tested import qualified Test.Copilot.Core.External@@ -15,7 +14,7 @@  -- | Run all unit tests on copilot-core. main :: IO ()-main = defaultMainWithOpts tests mempty+main = defaultMain tests  -- | All unit tests in copilot-core. tests :: [Test.Framework.Test]

@@ -1,3 +1,7 @@+-- The following warning is enabled in this module so that the import of+-- Copilot.Core.External does not give rise to a warning.+{-# OPTIONS_GHC -fno-warn-deprecations #-}+ -- | Test copilot-core:Copilot.Core.External. module Test.Copilot.Core.External where 

@@ -1,4 +1,8 @@ {-# LANGUAGE ExistentialQuantification #-}+-- The following warning is disabled in this module so that the import of+-- Copilot.Core.Type.Show does not give rise to a warning.+{-# OPTIONS_GHC -fno-warn-deprecations #-}+ -- | Test copilot-core:Copilot.Core.Interpret.Eval. -- -- The gist of this evaluation is in 'SemanticsP' and 'checkSemanticsP' which@@ -476,27 +480,42 @@ arbitraryBitsIntegralExpr :: (Arbitrary t, Typed t, Bits t, Integral t)                           => Gen (Expr t, [t]) arbitraryBitsIntegralExpr =-  -- We use frequency instead of oneof because the random expression generator-  -- seems to generate expressions that are too large and the test fails due-  -- to running out of memory.-  frequency-    [ (10, arbitraryConst)+      -- We use frequency instead of oneof because the random expression+      -- generator seems to generate expressions that are too large and the+      -- test fails due to running out of memory.+      frequency+        [ (10, arbitraryConst) -    , (2, apply1 <$> arbitraryNumOp1 <*> arbitraryBitsIntegralExpr)+        , (2, apply1 <$> arbitraryNumOp1 <*> arbitraryBitsIntegralExpr) -    , (1, apply2 <$> arbitraryNumOp2-                 <*> arbitraryBitsIntegralExpr-                 <*> arbitraryBitsIntegralExpr)+        , (1, apply2 <$> arbitraryNumOp2+                     <*> arbitraryBitsIntegralExpr+                     <*> arbitraryBitsIntegralExpr) -    , (5, apply2 <$> arbitraryBitsIntegralOp2-                 <*> arbitraryBitsIntegralExpr-                 <*> arbitraryBitsIntegralExpr)+        , (5, apply2 <$> arbitraryBitsIntegralOp2+                     <*> arbitraryBitsIntegralExpr+                     <*> arbitraryBitsIntegralExprConstPos) -    , (1, apply3 <$> arbitraryITEOp3-                 <*> arbitraryBoolExpr-                 <*> arbitraryBitsIntegralExpr-                 <*> arbitraryBitsIntegralExpr)-    ]+        , (1, apply3 <$> arbitraryITEOp3+                     <*> arbitraryBoolExpr+                     <*> arbitraryBitsIntegralExpr+                     <*> arbitraryBitsIntegralExpr)+        ]+  where++    -- Generator for constant bit integral expressions that, when converted to+    -- type 't', result in a positive number. We use a constant generator, as+    -- opposed to a generator based on the more comprehensive+    -- arbitraryBitsIntegralExpr, because the latter runs out of memory easily+    -- when nested and filtered with suchThat.+    arbitraryBitsIntegralExprConstPos =+        (\v -> (Const typeOf v, repeat v)) <$> intThatFits+      where+        -- In this context:+        --+        -- intThatFits :: Gen t+        intThatFits =+          suchThat arbitrary ((> 0) . (\x -> (fromIntegral x) :: Int))  -- ** Operators 

@@ -1,3 +1,7 @@+-- The following warning is disnabled in this module so that the import of+-- Copilot.Core.Type.Show does not give rise to a warning.+{-# OPTIONS_GHC -fno-warn-deprecations #-}+ -- | Test copilot-core:Copilot.Core.Type.Show. module Test.Copilot.Core.Type.Show where