packages feed

copilot-core 3.11 → 3.12

raw patch · 12 files changed

+318/−237 lines, 12 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

+ Copilot.Core.Type: instance Data.Type.Equality.TestEquality Copilot.Core.Type.Type

Files

CHANGELOG view
@@ -1,3 +1,10 @@+2022-11-07+        * Version bump (3.12). (#389)+        * Deprecate Copilot.Core.PrettyPrinter. (#383)+        * Replace uses of Copilot.Core.Type.Equality with definitions from+          base:Data.Type.Equality; deprecate Copilot.Core.Type.Equality. (#379)+        * Compliance with style guide. (#332)+ 2022-09-07         * Version bump (3.11). (#376)         * Deprecate Copilot.Core.PrettyDot. (#359)
copilot-core.cabal view
@@ -1,6 +1,6 @@ cabal-version:       >=1.10 name:                copilot-core-version:             3.11+version:             3.12 synopsis:            An intermediate representation for Copilot. description:   Intermediate representation for Copilot.
src/Copilot/Core.hs view
@@ -1,6 +1,14 @@--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+{-# LANGUAGE Safe #-} --- | Intermediate representation for Copilot specifications.+-- 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 #-}++-- |+-- Description: Intermediate representation for Copilot specifications.+-- Copyright:   (c) 2011 National Institute of Aerospace / Galois, Inc.+-- -- The following articles might also be useful: -- -- * Carette, Jacques and Kiselyov, Oleg and Shan, Chung-chieh,@@ -17,29 +25,26 @@ -- ("Copilot.Core.Interpret") -- and the pretty-printer -- ("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-  , module Copilot.Core.External-  , module Copilot.Core.Operators-  , module Copilot.Core.Spec-  , module Copilot.Core.Type-  , module Copilot.Core.Type.Array-  , module Data.Int-  , module Data.Word-  ) where+    ( module Copilot.Core.Expr+    , module Copilot.Core.External+    , module Copilot.Core.Operators+    , module Copilot.Core.Spec+    , module Copilot.Core.Type+    , module Copilot.Core.Type.Array+    , module Data.Int+    , module Data.Word+    )+  where +-- External imports+import Data.Int+import Data.Word++-- Internal imports import Copilot.Core.Expr import Copilot.Core.External -- See GHC flag enabled above import Copilot.Core.Operators import Copilot.Core.Spec import Copilot.Core.Type import Copilot.Core.Type.Array-import Data.Int-import Data.Word
src/Copilot/Core/Error.hs view
@@ -1,11 +1,13 @@--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.- {-# LANGUAGE Safe #-} --- | Custom functions to report error messages to users.+-- |+-- Description: Custom functions to report error messages to users.+-- Copyright:   (c) 2011 National Institute of Aerospace / Galois, Inc. module Copilot.Core.Error-  ( impossible-  , badUsage ) where+    ( impossible+    , badUsage+    )+  where  -- | Report an error due to a bug in Copilot. impossible :: String -- ^ Name of the function in which the error was detected.
src/Copilot/Core/Expr.hs view
@@ -1,24 +1,27 @@--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.- {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE GADTs                     #-} {-# LANGUAGE Safe                      #-} --- | Internal representation of Copilot stream expressions.+-- |+-- Description: Internal representation of Copilot stream expressions.+-- Copyright:   (c) 2011 National Institute of Aerospace / Galois, Inc. module Copilot.Core.Expr-  ( Id-  , Name-  , Expr (..)-  , UExpr (..)-  , DropIdx-  ) where--import Copilot.Core.Operators (Op1, Op2, Op3)-import Copilot.Core.Type (Type)-import Data.Word (Word32)+    ( Id+    , Name+    , Expr (..)+    , UExpr (..)+    , DropIdx+    )+  where +-- External imports import Data.Typeable (Typeable)+import Data.Word     (Word32) +-- Internal imports+import Copilot.Core.Operators (Op1, Op2, Op3)+import Copilot.Core.Type      (Type)+ -- | A stream identifier. type Id = Int @@ -34,19 +37,37 @@ -- representation contains information about the types of elements in the -- stream. data Expr a where-  Const        :: Typeable a => Type a -> a -> Expr a-  Drop         :: Typeable a => Type a -> DropIdx -> Id -> Expr a-  Local        :: Typeable a => Type a -> Type b -> Name -> Expr a -> Expr b -> Expr b-  Var          :: Typeable a => Type a -> Name -> Expr a-  ExternVar    :: Typeable a => Type a -> Name -> Maybe [a] -> Expr a-  Op1          :: Typeable a => Op1 a b -> Expr a -> Expr b-  Op2          :: (Typeable a, Typeable b) => Op2 a b c -> Expr a -> Expr b -> Expr c-  Op3          :: (Typeable a, Typeable b, Typeable c) => Op3 a b c d -> Expr a -> Expr b -> Expr c -> Expr d-  Label        :: Typeable a => Type a -> String -> Expr a -> Expr a+  Const     :: Typeable a+            => Type a -> a -> Expr a +  Drop      :: Typeable a+            => Type a -> DropIdx -> Id -> Expr a++  Local     :: Typeable a+            => Type a -> Type b -> Name -> Expr a -> Expr b -> Expr b++  Var       :: Typeable a+            => Type a -> Name -> Expr a++  ExternVar :: Typeable a+            => Type a -> Name -> Maybe [a] -> Expr a++  Op1       :: Typeable a+            => Op1 a b -> Expr a -> Expr b++  Op2       :: (Typeable a, Typeable b)+            => Op2 a b c -> Expr a -> Expr b -> Expr c++  Op3       :: (Typeable a, Typeable b, Typeable c)+            => Op3 a b c d -> Expr a -> Expr b -> Expr c -> Expr d++  Label     :: Typeable a+            => Type a -> String -> Expr a -> Expr a+ -- | A untyped expression that carries the information about the type of the -- expression as a value, as opposed to exposing it at type level (using an -- existential).-data UExpr = forall a. Typeable a => UExpr+data UExpr = forall a . Typeable a => UExpr   { uExprType :: Type a-  , uExprExpr :: Expr a }+  , uExprExpr :: Expr a+  }
src/Copilot/Core/Operators.hs view
@@ -1,22 +1,25 @@--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.- {-# LANGUAGE GADTs      #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE Safe       #-} --- | Internal representation of Copilot operators.+-- |+-- Description: Internal representation of Copilot operators.+-- Copyright:   (c) 2011 National Institute of Aerospace / Galois, Inc. module Copilot.Core.Operators-  ( Op1 (..)-  , Op2 (..)-  , Op3 (..)-  ) where+    ( Op1 (..)+    , Op2 (..)+    , Op3 (..)+    )+  where -import GHC.TypeLits             (KnownSymbol)+-- External imports+import Data.Bits    (Bits)+import Data.Word    (Word32)+import GHC.TypeLits (KnownSymbol) -import Copilot.Core.Type        (Type(..), Field(..))-import Copilot.Core.Type.Array  (Array)-import Data.Bits-import Data.Word                (Word32)+-- Internal imports+import Copilot.Core.Type       (Field (..), Type (..))+import Copilot.Core.Type.Array (Array)  -- | Unary operators. data Op1 a b where@@ -47,7 +50,7 @@   Ceiling  :: RealFrac a => Type a -> Op1 a a   Floor    :: RealFrac a => Type a -> Op1 a a   -- Bitwise operators.-  BwNot    :: Bits     a => Type a -> Op1 a a+  BwNot    :: Bits a => Type a -> Op1 a a   -- Casting operator.   Cast     :: (Integral a, Num b) => Type a -> Type b -> Op1 a b               -- ^ Casting operator.@@ -87,14 +90,13 @@   BwAnd    :: Bits a => Type a -> Op2 a a a   BwOr     :: Bits a => Type a -> Op2 a a a   BwXor    :: Bits a => Type a -> Op2 a a a-  BwShiftL :: ( Bits a, Integral b ) => Type a -> Type b -> Op2 a b a-  BwShiftR :: ( Bits a, Integral b ) => Type a -> Type b -> Op2 a b a+  BwShiftL :: (Bits a, Integral b) => Type a -> Type b -> Op2 a b a+  BwShiftR :: (Bits a, Integral b) => Type a -> Type b -> Op2 a b a   -- Array operator.-   Index    :: Type (Array n t) -> Op2 (Array n t) Word32 t               -- ^ Array access/projection of an array element.  -- | Ternary operators. data Op3 a b c d where-  -- Conditional operator:-  Mux   :: Type a -> Op3 Bool a a a+  -- Conditional operator.+  Mux :: Type a -> Op3 Bool a a a
src/Copilot/Core/PrettyPrint.hs view
@@ -6,6 +6,7 @@ {-# LANGUAGE Safe  #-}  module Copilot.Core.PrettyPrint+  {-# DEPRECATED "This module is deprecated in Copilot 3.12. Use copilot-prettyprinter instead." #-}   ( prettyPrint   , ppExpr   ) where
src/Copilot/Core/Spec.hs view
@@ -1,11 +1,12 @@--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.- {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE GADTs                     #-} {-# LANGUAGE Safe                      #-} --- | Copilot specifications constitute the main declaration of Copilot modules.+-- |+-- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc. --+-- Copilot specifications constitute the main declaration of Copilot modules.+-- -- A specification normally contains the association between streams to monitor -- and their handling functions, or streams to observe, or a theorem that must -- be proved.@@ -14,52 +15,61 @@ -- into Copilot Core's 'Spec'. This module defines the low-level Copilot Core -- representations for Specs and the main types of element in a spec.. module Copilot.Core.Spec-  ( Stream (..)-  , Observer (..)-  , Trigger (..)-  , Spec (..)-  , Property (..)-  ) where+    ( Stream (..)+    , Observer (..)+    , Trigger (..)+    , Spec (..)+    , Property (..)+    )+  where -import Copilot.Core.Expr (Name, Id, Expr, UExpr)-import Copilot.Core.Type (Type, Typed)+-- External imports import Data.Typeable (Typeable) +-- Internal imports+import Copilot.Core.Expr (Expr, Id, Name, UExpr)+import Copilot.Core.Type (Type, Typed)+ -- | A stream in an infinite succession of values of the same type. -- -- Stream can carry different types of data. Boolean streams play a special -- role: they are used by other parts (e.g., 'Trigger') to detect when the -- properties being monitored are violated.-data Stream = forall a. (Typeable a, Typed a) => Stream-  { streamId         :: Id-  , streamBuffer     :: [a]-  , streamExpr       :: Expr a-  , streamExprType   :: Type a }+data Stream = forall a . (Typeable a, Typed a) => Stream+  { streamId       :: Id+  , streamBuffer   :: [a]+  , streamExpr     :: Expr a+  , streamExprType :: Type a+  }  -- | An observer, representing a stream that we observe during interpretation -- at every sample.-data Observer = forall a. Typeable a => Observer+data Observer = forall a . Typeable a => Observer   { observerName     :: Name   , observerExpr     :: Expr a-  , observerExprType :: Type a }+  , observerExprType :: Type a+  }  -- | A trigger, representing a function we execute when a boolean stream becomes -- true at a sample. data Trigger = Trigger-  { triggerName      :: Name-  , triggerGuard     :: Expr Bool-  , triggerArgs      :: [UExpr] }+  { triggerName  :: Name+  , triggerGuard :: Expr Bool+  , triggerArgs  :: [UExpr]+  }  -- | A property, representing a boolean stream that is existentially or -- universally quantified over time. data Property = Property-  { propertyName     :: Name-  , propertyExpr     :: Expr Bool }+  { propertyName :: Name+  , propertyExpr :: Expr Bool+  }  -- | A Copilot specification is a list of streams, together with monitors on -- these streams implemented as observers, triggers or properties. data Spec = Spec-  { specStreams      :: [Stream]-  , specObservers    :: [Observer]-  , specTriggers     :: [Trigger]-  , specProperties   :: [Property] }+  { specStreams    :: [Stream]+  , specObservers  :: [Observer]+  , specTriggers   :: [Trigger]+  , specProperties :: [Property]+  }
src/Copilot/Core/Type.hs view
@@ -1,13 +1,3 @@--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.---- | Typing for Core.------ All expressions and streams in Core are accompanied by a representation of--- the types of the underlying expressions used or carried by the streams.--- This information is needed by the compiler to generate code, since it must--- initialize variables and equivalent representations for those types in--- the target languages.- {-# LANGUAGE DataKinds                 #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE FlexibleContexts          #-}@@ -18,36 +8,51 @@ {-# LANGUAGE ScopedTypeVariables       #-} {-# LANGUAGE UndecidableInstances      #-} -module Copilot.Core.Type-  ( Type (..)-  , Typed (..)-  , UType (..)-  , SimpleType (..)--  , tysize-  , tylength+-- 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 #-} -  , Value (..)-  , toValues-  , Field (..)-  , typename+-- |+-- Description: Typing for Core.+-- Copyright:   (c) 2011 National Institute of Aerospace / Galois, Inc.+--+-- All expressions and streams in Core are accompanied by a representation of+-- the types of the underlying expressions used or carried by the streams.+-- This information is needed by the compiler to generate code, since it must+-- initialize variables and equivalent representations for those types in+-- the target languages.+module Copilot.Core.Type+    ( Type (..)+    , Typed (..)+    , UType (..)+    , SimpleType (..) -  , Struct-  , fieldname-  , accessorname-  ) where+    , tysize+    , tylength -import Data.Int-import Data.Word-import Copilot.Core.Type.Equality-import Copilot.Core.Type.Array+    , Value (..)+    , toValues+    , Field (..)+    , typename -import Data.Typeable (Typeable, typeRep)+    , Struct+    , fieldname+    , accessorname+    )+  where -import GHC.TypeLits (KnownNat, natVal, Symbol, KnownSymbol, symbolVal)-import Data.Proxy   (Proxy (..))+-- External imports+import Data.Int           (Int16, Int32, Int64, Int8)+import Data.List          (intercalate)+import Data.Proxy         (Proxy (..))+import Data.Type.Equality as DE+import Data.Typeable      (Typeable, typeRep)+import Data.Word          (Word16, Word32, Word64, Word8)+import GHC.TypeLits       (KnownNat, KnownSymbol, Symbol, natVal, symbolVal) -import Data.List (intercalate)+-- Internal imports+import Copilot.Core.Type.Array    (Array)+import Copilot.Core.Type.Equality as CE  -- | The value of that is a product or struct, defined as a constructor with -- several fields.@@ -58,19 +63,21 @@   toValues :: a -> [Value a]  -- | The field of a struct, together with a representation of its type.-data Value a = forall s t. (Typeable t, KnownSymbol s, Show t) => Value (Type t) (Field s t)+data Value a =+  forall s t . (Typeable t, KnownSymbol s, Show t) => Value (Type t) (Field s t)  -- | A field in a struct. The name of the field is a literal at the type -- level. data Field (s :: Symbol) t = Field t  -- | Extract the name of a field.-fieldname :: forall s t. KnownSymbol s => Field s t -> String+fieldname :: forall s t . KnownSymbol s => Field s t -> String fieldname _ = symbolVal (Proxy :: Proxy s)  -- | Extract the name of an accessor (a function that returns a field of a -- struct).-accessorname :: forall a s t. (Struct a, KnownSymbol s) => (a -> Field s t) -> String+accessorname :: forall a s t . (Struct a, KnownSymbol s)+             => (a -> Field s t) -> String accessorname _ = symbolVal (Proxy :: Proxy s)  instance (KnownSymbol s, Show t) => Show (Field s t) where@@ -89,45 +96,59 @@ -- former, the length of the array is part of the type. In the latter, the -- names of the fields are part of the type. data Type :: * -> * where-  Bool    :: Type Bool-  Int8    :: Type Int8-  Int16   :: Type Int16-  Int32   :: Type Int32-  Int64   :: Type Int64-  Word8   :: Type Word8-  Word16  :: Type Word16-  Word32  :: Type Word32-  Word64  :: Type Word64-  Float   :: Type Float-  Double  :: Type Double-  Array   :: forall n t. ( KnownNat n+  Bool   :: Type Bool+  Int8   :: Type Int8+  Int16  :: Type Int16+  Int32  :: Type Int32+  Int64  :: Type Int64+  Word8  :: Type Word8+  Word16 :: Type Word16+  Word32 :: Type Word32+  Word64 :: Type Word64+  Float  :: Type Float+  Double :: Type Double+  Array  :: forall n t . ( KnownNat n                          , Typed t                          ) => Type t -> Type (Array n t)-  Struct  :: (Typed a, Struct a) => a -> Type a+  Struct :: (Typed a, Struct a) => a -> Type a  -- | Return the length of an array from its type-tylength :: forall n t. KnownNat n => Type (Array n t) -> Int+tylength :: forall n t . KnownNat n => Type (Array n t) -> Int tylength _ = fromIntegral $ natVal (Proxy :: Proxy n)  -- | Return the total (nested) size of an array from its type-tysize :: forall n t. KnownNat n => Type (Array n t) -> Int+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 Refl-  (=~=) Int8   Int8   = Just Refl-  (=~=) Int16  Int16  = Just Refl-  (=~=) Int32  Int32  = Just Refl-  (=~=) Int64  Int64  = Just Refl-  (=~=) Word8  Word8  = Just Refl-  (=~=) Word16 Word16 = Just Refl-  (=~=) Word32 Word32 = Just Refl-  (=~=) Word64 Word64 = Just Refl-  (=~=) Float  Float  = Just Refl-  (=~=) Double Double = Just Refl+  (=~=) 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+  testEquality Int8   Int8   = Just DE.Refl+  testEquality Int16  Int16  = Just DE.Refl+  testEquality Int32  Int32  = Just DE.Refl+  testEquality Int64  Int64  = Just DE.Refl+  testEquality Word8  Word8  = Just DE.Refl+  testEquality Word16 Word16 = Just DE.Refl+  testEquality Word32 Word32 = Just DE.Refl+  testEquality Word64 Word64 = Just DE.Refl+  testEquality Float  Float  = Just DE.Refl+  testEquality Double Double = Just DE.Refl+  testEquality _ _ = Nothing+ -- | A simple, monomorphic representation of types that facilitates putting -- variables in heterogeneous lists and environments in spite of their types -- being different.@@ -149,22 +170,21 @@ -- | Type equality, used to help type inference.  -- This instance is necessary, otherwise the type of SArray can't be inferred.- instance Eq SimpleType where-  SBool   == SBool    = True-  SInt8   == SInt8    = True-  SInt16  == SInt16   = True-  SInt32  == SInt32   = True-  SInt64  == SInt64   = True-  SWord8  == SWord8   = True-  SWord16 == SWord16  = True-  SWord32 == SWord32  = True-  SWord64 == SWord64  = True-  SFloat  == SFloat   = True-  SDouble == SDouble  = True-  (SArray t1) == (SArray t2) | Just Refl <- t1 =~= t2 = True-                             | otherwise              = False-  SStruct == SStruct  = True+  SBool   == SBool   = True+  SInt8   == SInt8   = True+  SInt16  == SInt16  = True+  SInt32  == SInt32  = True+  SInt64  == SInt64  = True+  SWord8  == SWord8  = True+  SWord16 == SWord16 = True+  SWord32 == SWord32 = True+  SWord64 == SWord64 = True+  SFloat  == SFloat  = True+  SDouble == SDouble = True+  (SArray t1) == (SArray t2) | Just DE.Refl <- testEquality t1 t2 = True+                             | otherwise                          = False+  SStruct == SStruct = True   _ == _ = False  -- | A typed expression, from which we can obtain the two type representations@@ -174,42 +194,53 @@   simpleType :: Type a -> SimpleType   simpleType _ = SStruct -instance Typed Bool   where+instance Typed Bool where   typeOf       = Bool   simpleType _ = SBool-instance Typed Int8   where++instance Typed Int8 where   typeOf       = Int8   simpleType _ = SBool-instance Typed Int16  where++instance Typed Int16 where   typeOf       = Int16   simpleType _ = SInt16-instance Typed Int32  where++instance Typed Int32 where   typeOf       = Int32   simpleType _ = SInt32-instance Typed Int64  where++instance Typed Int64 where   typeOf       = Int64   simpleType _ = SInt64-instance Typed Word8  where++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++instance Typed Float where   typeOf       = Float   simpleType _ = SFloat+ instance Typed Double where   typeOf       = Double   simpleType _ = SDouble+ instance (Typeable t, Typed t, KnownNat n) => Typed (Array n t) where-  typeOf                = Array typeOf-  simpleType (Array t)  = SArray t+  typeOf               = Array typeOf+  simpleType (Array t) = SArray t  -- | A untyped type (no phantom type). data UType = forall a . Typeable a => UType { uTypeType :: Type a }
src/Copilot/Core/Type/Array.hs view
@@ -1,31 +1,32 @@--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.- {-# LANGUAGE DataKinds             #-} {-# LANGUAGE FlexibleInstances     #-} {-# LANGUAGE GADTs                 #-}-{-# LANGUAGE KindSignatures        #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE Safe                  #-} {-# LANGUAGE ScopedTypeVariables   #-} {-# LANGUAGE TypeFamilies          #-} {-# LANGUAGE TypeOperators         #-} --- | Implementation of an array that uses type literals to store length. No+-- |+-- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.+--+-- Implementation of an array that uses type literals to store length. No -- explicit indexing is used for the input data. Supports arbitrary nesting of -- arrays.- module Copilot.Core.Type.Array-  ( Array-  , array-  , flatten-  , size-  , Flatten-  , InnerType-  , arrayelems-  ) where+    ( Array+    , array+    , flatten+    , size+    , Flatten+    , InnerType+    , arrayelems+    )+  where -import GHC.TypeLits     (Nat, KnownNat, natVal)-import Data.Proxy       (Proxy (..))+-- External imports+import Data.Proxy   (Proxy (..))+import GHC.TypeLits (KnownNat, Nat, natVal)  -- | Implementation of an array that uses type literals to store length. data Array (n :: Nat) t where
src/Copilot/Core/Type/Equality.hs view
@@ -6,6 +6,7 @@  -- | 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
src/Copilot/Core/Type/ShowInternal.hs view
@@ -1,20 +1,20 @@--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.- {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE GADTs                     #-} {-# LANGUAGE Safe                      #-} --- | Show Copilot Core types and typed values.+-- |+-- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.+--+-- Show Copilot Core types and typed values. module Copilot.Core.Type.ShowInternal-  ( showWithType-  , ShowType(..)-  , showType-  ) where--import Copilot.Core.Type+    ( showWithType+    , ShowType (..)+    , showType+    )+  where --- Are we proving equivalence with a C backend, in which case we want to show--- Booleans as '0' and '1'.+-- Internal imports+import Copilot.Core.Type (Type (..))  -- | Target language for showing a typed value. Used to adapt the -- representation of booleans.@@ -24,33 +24,33 @@ -- 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+    case showT of+      C       -> case t of                    Bool -> if x then "1" else "0"                    _    -> sw-    Haskell   -> case t of+      Haskell -> case t of                    Bool -> if x then "true" else "false"                    _    -> sw   where-  sw = case showWit t of-         ShowWit -> show x+    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+    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@@ -62,16 +62,16 @@ 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+    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