copilot-core 3.14 → 3.15

raw patch · 8 files changed

+9/−372 lines, 8 filesdep −prettyPVP ok

version bump matches the API change (PVP)

Dependencies removed: pretty

API changes (from Hackage documentation)

Files

• CHANGELOG +5/−0
• copilot-core.cabal +2/−11
• src/Copilot/Core.hs +1/−2
• src/Copilot/Core/Error.hs +0/−20
• src/Copilot/Core/PrettyPrint.hs +0/−195
• src/Copilot/Core/Type.hs +1/−21
• src/Copilot/Core/Type/Equality.hs +0/−46
• src/Copilot/Core/Type/Show.hs +0/−77

@@ -1,3 +1,8 @@+2023-05-07+        * Version bump (3.15). (#438)+        * Remove Copilot.Core.Type.Equality. (#427)+        * Remove Copilot.Core.PrettyPrint. (#426)+ 2023-03-07         * Version bump (3.14). (#422)         * Remove Copilot.Core.PrettyDot. (#409)

@@ -1,6 +1,6 @@ cabal-version:       >=1.10 name:                copilot-core-version:             3.14+version:             3.15 synopsis:            An intermediate representation for Copilot. description:   Intermediate representation for Copilot.@@ -42,8 +42,7 @@     -fno-warn-orphans    build-depends:-    base       >= 4.9 && < 5,-    pretty     >= 1.0 && < 1.2+    base >= 4.9 && < 5    exposed-modules: @@ -53,14 +52,7 @@     Copilot.Core.Spec     Copilot.Core.Type     Copilot.Core.Type.Array-    Copilot.Core.Type.Equality-    Copilot.Core.PrettyPrint -  other-modules:--    Copilot.Core.Error-    Copilot.Core.Type.Show- test-suite unit-tests   type:     exitcode-stdio-1.0@@ -77,7 +69,6 @@       base     , HUnit     , QuickCheck-    , pretty     , test-framework     , test-framework-hunit     , test-framework-quickcheck2

@@ -17,8 +17,7 @@ -- -- For examples of how to traverse a Copilot specification see -- the source code of the interpreter (@copilot-interpreter@)--- and the pretty-printer--- ("Copilot.Core.PrettyPrint").+-- and the pretty-printer (@copilot-prettyprinter@). module Copilot.Core     ( module Copilot.Core.Expr     , module Copilot.Core.Operators

@@ -1,20 +0,0 @@-{-# LANGUAGE Safe #-}---- |--- Description: Custom functions to report error messages to users.--- Copyright:   (c) 2011 National Institute of Aerospace / Galois, Inc.-module Copilot.Core.Error-    ( impossible-    )-  where---- | Report an error due to a bug in Copilot.-impossible :: String -- ^ Name of the function in which the error was detected.-           -> String -- ^ Name of the package in which the function is located.-           -> a-impossible function package =-  error $ "\"Impossible\" error in function "-    ++ function ++ ", in package " ++ package-    ++ ". Please file an issue at "-    ++ "https://github.com/Copilot-Language/copilot/issues"-    ++ "or email the maintainers at <ivan.perezdominguez@nasa.gov>"

@@ -1,195 +0,0 @@--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.---- | A pretty printer for Copilot specifications.--{-# LANGUAGE GADTs #-}-{-# LANGUAGE Safe  #-}--module Copilot.Core.PrettyPrint-  {-# DEPRECATED "This module is deprecated in Copilot 3.12. Use copilot-prettyprinter instead." #-}-  ( prettyPrint-  , ppExpr-  ) where--import Copilot.Core-import Copilot.Core.Error (impossible)-import Copilot.Core.Type.Show (showWithType, ShowType(..), showType)-import Prelude hiding (id, (<>))-import Text.PrettyPrint.HughesPJ-import Data.List (intersperse)---- | Create a unique stream name by prefixing the given ID by a lowercase--- letter @"s"@.-strmName :: Int -> Doc-strmName id = text "s" <> int id---- | Pretty-print a Copilot expression.------ The type is ignored, and only the expression is pretty-printed.-ppExpr :: Expr a -> Doc-ppExpr e0 = case e0 of-  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 "Ext_" <> (text name)-  Local _ _ name e1 e2       -> text "local" <+> doubleQuotes (text name) <+> equals-                                          <+> ppExpr e1 $$ text "in" <+> ppExpr e2-  Var _ name                 -> text "var" <+> doubleQuotes (text name)-  Op1 op e                   -> ppOp1 op (ppExpr e)-  Op2 op e1 e2               -> ppOp2 op (ppExpr e1) (ppExpr e2)-  Op3 op e1 e2 e3            -> ppOp3 op (ppExpr e1) (ppExpr e2) (ppExpr e3)-  Label _ s e                -> text "label "<> doubleQuotes (text s) <+> (ppExpr e)---- | Pretty-print an untyped expression.------ The type is ignored, and only the expression is pretty-printed.-ppUExpr :: UExpr -> Doc-ppUExpr UExpr { uExprExpr = e0 } = ppExpr e0---- | Pretty-print a unary operation.-ppOp1 :: Op1 a b -> Doc -> Doc-ppOp1 op = case op of-  Not                     -> ppPrefix "not"-  Abs _                   -> ppPrefix "abs"-  Sign _                  -> ppPrefix "signum"-  Recip _                 -> ppPrefix "recip"-  Exp _                   -> ppPrefix "exp"-  Sqrt _                  -> ppPrefix "sqrt"-  Log _                   -> ppPrefix "log"-  Sin _                   -> ppPrefix "sin"-  Tan _                   -> ppPrefix "tan"-  Cos _                   -> ppPrefix "cos"-  Asin _                  -> ppPrefix "asin"-  Atan _                  -> ppPrefix "atan"-  Acos _                  -> ppPrefix "acos"-  Sinh _                  -> ppPrefix "sinh"-  Tanh _                  -> ppPrefix "tanh"-  Cosh _                  -> ppPrefix "cosh"-  Asinh _                 -> ppPrefix "asinh"-  Atanh _                 -> ppPrefix "atanh"-  Acosh _                 -> ppPrefix "acosh"-  Ceiling _               -> ppPrefix "ceiling"-  Floor _                 -> ppPrefix "floor"-  BwNot _                 -> ppPrefix "~"-  Cast _ _                -> ppPrefix "(cast)"-  GetField (Struct _) _ f -> \e -> ppInfix "#" e (text $ accessorname f)-  GetField _ _ _          -> impossible "ppOp1" "Copilot.Core.PrettyPrint"---- | Pretty-print a binary operation.-ppOp2 :: Op2 a b c -> Doc -> Doc -> Doc-ppOp2 op = case op of-  And          -> ppInfix "&&"-  Or           -> ppInfix "||"-  Add      _   -> ppInfix "+"-  Sub      _   -> ppInfix "-"-  Mul      _   -> ppInfix "*"-  Div      _   -> ppInfix "div"-  Mod      _   -> ppInfix "mod"-  Fdiv     _   -> ppInfix "/"-  Pow      _   -> ppInfix "**"-  Logb     _   -> ppInfix "logBase"-  Atan2    _   -> ppInfix "atan2"-  Eq       _   -> ppInfix "=="-  Ne       _   -> ppInfix "/="-  Le       _   -> ppInfix "<="-  Ge       _   -> ppInfix ">="-  Lt       _   -> ppInfix "<"-  Gt       _   -> ppInfix ">"-  BwAnd    _   -> ppInfix "&"-  BwOr     _   -> ppInfix "|"-  BwXor    _   -> ppInfix "^"-  BwShiftL _ _ -> ppInfix "<<"-  BwShiftR _ _ -> ppInfix ">>"-  Index    _   -> ppInfix ".!!"---- | Pretty-print a ternary operation.-ppOp3 :: Op3 a b c d -> Doc -> Doc -> Doc -> Doc-ppOp3 op = case op of-  Mux _    -> \ doc1 doc2 doc3 ->-    text "(if"   <+> doc1 <+>-    text "then" <+> doc2 <+>-    text "else" <+> doc3 <> text ")"---- | Parenthesize two 'Doc's, separated by an infix 'String'.-ppInfix :: String -> Doc -> Doc -> Doc-ppInfix cs doc1 doc2 = parens $ doc1 <+> text cs <+> doc2---- | Prefix a 'Doc' by a 'String'.-ppPrefix :: String -> Doc -> Doc-ppPrefix cs = (text cs <+>)---- | Pretty-print a Copilot stream as a case of a top-level function for--- streams of that type, by pattern matching on the stream name.-ppStream :: Stream -> Doc-ppStream-  Stream-    { streamId       = id-    , streamBuffer   = buffer-    , streamExpr     = e-    , streamExprType = t-    }-      = (parens . text . showType) t-          <+> strmName id-    <+> text "="-    <+> text ("["-              ++ ( concat $ intersperse ","-                              $ map (showWithType Haskell t) buffer )-              ++ "]")-    <+> text "++"-    <+> ppExpr e---- | Pretty-print a Copilot trigger as a case of a top-level @trigger@--- function, by pattern matching on the trigger name.-ppTrigger :: Trigger -> Doc-ppTrigger-  Trigger-    { triggerName  = name-    , triggerGuard = e-    , triggerArgs  = args }-  =   text "trigger" <+> text "\"" <> text name <> text "\""-  <+> text "="-  <+> ppExpr e-  <+> lbrack-  $$  (nest 2 $ vcat (punctuate comma $-                          map (\a -> text "arg" <+> ppUExpr a) args))-  $$  nest 2 rbrack---- | Pretty-print a Copilot observer as a case of a top-level @observer@--- function, by pattern matching on the observer name.-ppObserver :: Observer -> Doc-ppObserver-  Observer-    { observerName     = name-    , observerExpr     = e }-  =   text "observer \"" <> text name <> text "\""-  <+> text "="-  <+> ppExpr e---- | Pretty-print a Copilot property as a case of a top-level @property@--- function, by pattern matching on the property name.-ppProperty :: Property -> Doc-ppProperty-  Property-    { propertyName     = name-    , propertyExpr     = e }-  =   text "property \"" <> text name <> text "\""-  <+> text "="-  <+> ppExpr e---- | Pretty-print a Copilot specification, in the following order:------ - Streams definitions--- - Trigger definitions--- - Observer definitions--- - Property definitions-ppSpec :: Spec -> Doc-ppSpec spec = cs $$ ds $$ es $$ fs-  where-    cs = foldr (($$) . ppStream)   empty (specStreams   spec)-    ds = foldr (($$) . ppTrigger)  empty (specTriggers  spec)-    es = foldr (($$) . ppObserver) empty (specObservers spec)-    fs = foldr (($$) . ppProperty) empty (specProperties spec)---- | Pretty-print a Copilot specification.-prettyPrint :: Spec -> String-prettyPrint = render . ppSpec

@@ -8,11 +8,6 @@ {-# LANGUAGE ScopedTypeVariables       #-} {-# LANGUAGE TypeOperators             #-} {-# LANGUAGE UndecidableInstances      #-}---- The following flag is disabled in this module so that the import of--- Copilot.Core.Type.Equality does not give rise to warnings.-{-# OPTIONS_GHC -fno-warn-deprecations #-}- -- | -- Description: Typing for Core. -- Copyright:   (c) 2011 National Institute of Aerospace / Galois, Inc.@@ -53,8 +48,7 @@                            symbolVal)  -- Internal imports-import Copilot.Core.Type.Array    (Array)-import Copilot.Core.Type.Equality as CE+import Copilot.Core.Type.Array (Array)  -- | The value of that is a product or struct, defined as a constructor with -- several fields.@@ -122,20 +116,6 @@ tysize :: forall n t . KnownNat n => Type (Array n t) -> Int tysize ty@(Array ty'@(Array _)) = tylength ty * tysize ty' tysize ty@(Array _            ) = tylength ty--instance EqualType Type where-  (=~=) Bool   Bool   = Just CE.Refl-  (=~=) Int8   Int8   = Just CE.Refl-  (=~=) Int16  Int16  = Just CE.Refl-  (=~=) Int32  Int32  = Just CE.Refl-  (=~=) Int64  Int64  = Just CE.Refl-  (=~=) Word8  Word8  = Just CE.Refl-  (=~=) Word16 Word16 = Just CE.Refl-  (=~=) Word32 Word32 = Just CE.Refl-  (=~=) Word64 Word64 = Just CE.Refl-  (=~=) Float  Float  = Just CE.Refl-  (=~=) Double Double = Just CE.Refl-  (=~=) _ _ = Nothing  instance TestEquality Type where   testEquality Bool   Bool   = Just DE.Refl

@@ -1,46 +0,0 @@--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.--{-# LANGUAGE GADTs          #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE Safe           #-}---- | Propositional equality and type equality.-module Copilot.Core.Type.Equality-  {-# DEPRECATED "This module is deprecated in Copilot 3.12. Use base:Data.Type.Equality instead." #-}-  ( Equal (..)-  , EqualType (..)-  , coerce-  , refl-  , trans-  , symm-  , cong-  ) where---- | Propositional equality.-data Equal :: * -> * -> * where-  Refl :: Equal a a---- | Type equality. If the value of @x =~= y@ is @Just Refl@, then the two--- types @x@ and @y@ are equal.-class EqualType t where-  (=~=) :: t a -> t b -> Maybe (Equal a b)---- | Safe coercion, which requires proof of equality.-coerce :: Equal a b -> a -> b-coerce Refl x = x---- | Proof of propositional equality.-refl :: Equal a a-refl = Refl---- | Symmetry.-symm :: Equal a b -> Equal b a-symm Refl = Refl---- | Transitivity.-trans :: Equal a b -> Equal b c -> Equal a c-trans Refl Refl = Refl---- | Congruence.-cong :: Equal a b -> Equal (f a) (f b)-cong Refl = Refl

@@ -1,77 +0,0 @@-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE GADTs                     #-}-{-# LANGUAGE Safe                      #-}---- |--- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.------ Show Copilot Core types and typed values.-module Copilot.Core.Type.Show-    ( showWithType-    , ShowType (..)-    , showType-    )-  where---- Internal imports-import Copilot.Core.Type (Type (..))---- | 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