diff --git a/CHANGELOG b/CHANGELOG new file mode 100644 --- /dev/null +++ b/CHANGELOG @@ -0,0 +1,194 @@ +2026-07-07 + * Version bump (4.8). (#745) + +2026-05-07 + * Version bump (4.7.1). (#730) + +2026-03-07 + * Version bump (4.7). (#714) + +2026-01-07 + * Version bump (4.6.1). (#705) + +2025-11-07 + * Version bump (4.6). (#679) + +2025-09-07 + * Version bump (4.5.1). (#666) + +2025-07-07 + * Version bump (4.5). (#642) + * Remove deprecated fields of Copilot.Core.Expr.UExpr. (#636) + +2025-05-07 + * Version bump (4.4). (#618) + * Remove deprecated Copilot.Core.Type.uTypeType. (#615) + +2025-03-07 + * Version bump (4.3). (#604) + * Fix typo in documentation. (#587) + * Add a Show instance for Type. (#589) + * Add a Prop type to capture how a property is quantified. (#254) + +2025-01-07 + * Version bump (4.2). (#577) + * Deprecate fields of Copilot.Core.Expr.UExpr. (#565) + * Increase test coverage. (#555) + * Define generic implementations of Struct and Typed methods. (#564) + +2024-11-07 + * Version bump (4.1). (#561) + * Add Haddocks for updateField. (#525) + * Standardize changelog format. (#550) + * Deprecate Copilot.Core.Type.UType.uTypeType. (#484) + +2024-09-07 + * Version bump (4.0). (#532) + * Update Op3, Array to support array updates. (#36) + +2024-07-07 + * Version bump (3.20). (#522) + * Update Op2, Struct to support struct field updates. (#520) + +2024-05-07 + * Version bump (3.19.1). (#512) + +2024-03-07 + * Version bump (3.19). (#504) + * Remove deprecated functions in Copilot.Core.Type and + Copilot.Core.Type.Array. (#500) + * Increase test coverage. (#502) + +2024-01-07 + * Version bump (3.18.1). (#493) + +2024-01-07 + * Version bump (3.18). (#487) + +2023-11-07 + * Version bump (3.17). (#466) + * Compliance with style guide. (#457) + +2023-09-07 + * Version bump (3.16.1). (#455) + +2023-07-07 + * Version bump (3.16). (#448) + +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) + * Fix formatting error in CHANGELOG. (#414) + * Remove module space Copilot.Core.Interpret. (#410) + * Remove unused definitions from Copilot.Core.Type.Array. (#411) + +2023-01-07 + * Version bump (3.13). (#406) + * Implement missing cases of type equality for arrays and structs. + (#400) + * Remove Copilot.Core.External. (#391) + * Fix bug in definition of simpleType for Int8. (#393) + * Hide module Copilot.Core.Type.Show. (#392) + +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) + * Remove Copilot.Core.Type.Dynamic. (#360) + * Split copilot-interpreter into separate library. (#361) + * Deprecate unused classes, functions from Array module. (#369) + +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) + * Hide module Copilot.Core.Interpret.Render. (#303) + * Remove Copilot.Core.Type.Dynamic.fromDynF,toDynF. (#301) + * Hide module Copilot.Core.Error. (#300) + * Remove Copilot.Core.Type.Uninitialized. (#302) + * Remove Copilot.Core.Expr.Tag. (#304) + +2022-03-07 + * Version bump (3.8). (#298) + * Replaces uses of the internal Dynamic with base:Data.Dynamic. (#266) + * Mark package as uncurated to avoid modification. (#288) + +2022-01-07 + * Version bump (3.7). (#287) + * Make imports explicit, reorganize imports. (#277) + * Remove Copilot.Core.Type.Read. (#286) + * Remove Copilot.Core.Type.Eq. (#285) + * Remove Copilot.Core.Locals. (#284) + * Deprecate Copilot.Core.Type.Show.ShowWit. (#283) + * Remove Copilot.Core.Type.Show.showWit. (#282) + +2021-11-07 + * Version bump (3.6). (#264) + * Deprecate Copilot.Core.Type.Dynamic.toDynF and fromDynF. (#269) + * Deprecate copilot-core:Copilot.Core.Type.Uninitialized. (#270) + * Deprecate export of copilot-core:Copilot.Core.Interpret.Render. (#268) + * Replace uses of copilot-core's error reporting functions. (#267) + * Introduce new ops atan2, ceiling, floor. (#246) + * Add initial support for unit testing. (#256) + * Deprecate unused type. (#260) + * Remove deprecated module. (#250) + * Fix outdated/broken links. (#252) + +2021-08-19 + * Version bump (3.5). (#247) + * Update travis domain in README. (#222) + * Remove commented code. (#15) + * Update official maintainer. (#236) + * Update source repo location. (#241) + * Add I. Perez to author list. (#243) + +2021-07-07 + * Version bump (3.4). (#231) + * Deprecated `Copilot.Core.Locals`. (#141) + * Deprecated `Copilot.Core.Type.Read` module. (#144) + * Deprecated `showWit`. (#140) + * Deprecated `Copilot.Core.Type.Eq`. (#143) + * Remove unused module `Copilot.Core.StructMarshal`. (#139) + +2021-05-07 + * Version bump (3.3). (#217) + * Fix URL in bug-reports field in cabal file. (#215) + * Deprecate unused module Copilot.Core.MakeTags. (#142) + * Deprecate unused functions in Copilot.Core.PrettyDot. (#137) + +2021-03-05 + * Version bump (3.2.1). (#136) + * Completed the documentation. (#145) + +2020-12-06 + * Version bump (3.2). (#65) + * Fixed implementation of tysize for n-dimensional arrays. (#147) + * Removed sorting of interpreter output. (#148) + * Minor documentation fixes. (#149, #151) + * Credits: @fdedden. + +2019-11-22 + * Version bump (3.1). (#46) + * Eliminate random modules and generators. (#157) + * Updated contact information for 'impossible' error. (#154) + * Implement missing pretty printer for Index operator. (#155) diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,61 +1,33 @@ -[![Build Status](https://travis-ci.org/Copilot-Language/copilot-core.svg?branch=master)](https://travis-ci.org/Copilot-Language/copilot-core) +[![Build Status](https://travis-ci.com/Copilot-Language/copilot.svg?branch=master)](https://app.travis-ci.com/github/Copilot-Language/copilot) -Overview -======== -[copilot-core](http://hackage.haskell.org/package/copilot-core) The core -language, which efficiently represents Copilot expressions. The core is only of -interest to implementers wishing to add a new back-end to Copilot. +# Copilot: a stream DSL +The core language, which efficiently represents Copilot expressions. The core +is only of interest to implementers wishing to add a new back-end to Copilot. -Copilot is a stream (i.e., infinite lists) domain-specific language (DSL) in -Haskell that compiles into embedded C. Copilot is similar in spirit to -languages like Lustre. Copilot contains an interpreter, multiple back-end -compilers, and other verification tools. +Copilot is a runtime verification framework written in Haskell. It allows the +user to write programs in a simple but powerful way using a stream-based +approach. -Installation -============ -The Copilot library is cabalized. Assuming you have cabal and the GHC compiler -installed (the [Haskell Platform](http://hackage.haskell.org/platform/) is the -easiest way to obtain these), it should merely be a matter of running - - cabal install copilot-core +Programs can be interpreted for testing, or translated C99 code to be +incorporated in a project, or as a standalone application. The C99 backend +ensures us that the output is constant in memory and time, making it suitable +for systems with hard realtime requirements. -However, we strongly recommend you install Copilot, which installs copilot-c99 -and other packages automatically. Execute - cabal install copilot +## Installation +Copilot-core can be found on +[Hackage](https://hackage.haskell.org/package/copilot-core). It is typically +only installed as part of the complete Copilot distribution. For installation +instructions, please refer to the [Copilot +website](https://copilot-language.github.io). -Resources -========= -To understand our use of Dynamic typing, please consult the following, -particularly the last document: -+ Carette, Jacques and Kiselyov, Oleg and Shan, Chung-chieh, - "*Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages*", - Journal of Functional Programming vol. 19, p. 509-543, 2009. +## Further information +For further information, install instructions and documentation, please visit +the Copilot website: +[https://copilot-language.github.io](https://copilot-language.github.io) -+ Guillemette, Louis-Julien and Monnier, Stefan, - "*Type-Safe Code Transformations in Haskell*", - Electronic Notes in Theoretical Computer Science vol. 174, p. 23-39, 2007. -+ Baars, Arthur I. and Swierstra, S. Doaitse, - "*Typing dynamic typing*", - ACM SIGPLAN Notices vol. 37, p. 157-166, 2002 - -Resources -========= -[copilot-core](http://hackage.haskell.org/package/copilot-core) is available on -Hackage. - -**Sources** for each package are available on Github as well. Just go to -[Github](github.com) and search for the package of interest. Feel free to fork! - -Copyright, License -================== -Copilot is distributed with the BSD3 license. The license file contains the -[BSD3](http://en.wikipedia.org/wiki/BSD_licenses) verbiage. - -Thanks -====== -We are grateful for NASA Contract NNL08AD13T to [Galois, -Inc](http://corp.galois.com/) and the [National Institute of -Aerospace](http://www.nianet.org/), which partially supported this work. +## License +Copilot is distributed under the BSD-3-Clause license, which can be found +[here](https://raw.githubusercontent.com/Copilot-Language/copilot/master/copilot-core/LICENSE). diff --git a/copilot-core.cabal b/copilot-core.cabal --- a/copilot-core.cabal +++ b/copilot-core.cabal @@ -1,32 +1,35 @@ cabal-version: >=1.10 name: copilot-core -version: 2.2.1 +version: 4.8 synopsis: An intermediate representation for Copilot. description: Intermediate representation for Copilot. . Copilot is a stream (i.e., infinite lists) domain-specific language (DSL) in Haskell that compiles into embedded C. Copilot contains an interpreter, - multiple back-end compilers, and other verification tools. A tutorial, bug - reports, and todos are available at - . + multiple back-end compilers, and other verification tools. . - Examples are available at - . + A tutorial, examples, and other information are available at + . -author: Lee Pike, Robin Morisset, Alwyn Goodloe, - Sebastian Niller, Nis Nordbyop Wegmann +author: Frank Dedden, Lee Pike, Robin Morisset, Alwyn Goodloe, + Sebastian Niller, Nis Nordbyop Wegmann, Ivan Perez license: BSD3 license-file: LICENSE -maintainer: leepike@gmail.com +maintainer: Ivan Perez +homepage: https://copilot-language.github.io +bug-reports: https://github.com/Copilot-Language/copilot/issues stability: Experimental category: Language, Embedded build-type: Simple -extra-source-files: README.md +extra-source-files: README.md, CHANGELOG +x-curation: uncurated + source-repository head type: git - location: git://github.com/leepike/copilot-core.git + location: https://github.com/Copilot-Language/copilot.git + subdir: copilot-core library @@ -36,49 +39,47 @@ ghc-options: -Wall - -fwarn-tabs - -auto-all - -caf-all -fno-warn-orphans - -fpackage-trust - -trust=array - -trust=base - -trust=containers - -trust=random - build-depends: - containers >= 0.4, - base >= 4.0 && < 5, - pretty >= 1.0, - random > 1.0, - pretty-ncols >= 0.1, - mtl >= 2.0, - dlist + base >= 4.9 && < 5 exposed-modules: - Copilot.Compile.Header.C99 Copilot.Core - Copilot.Core.Error Copilot.Core.Expr - Copilot.Core.External - Copilot.Core.Interpret - Copilot.Core.Interpret.Eval - Copilot.Core.Interpret.Render - Copilot.Core.MakeTags Copilot.Core.Operators Copilot.Core.Spec - Copilot.Core.Locals - Copilot.Core.Random - Copilot.Core.Random.Gen - Copilot.Core.Random.Weights Copilot.Core.Type - Copilot.Core.Type.Dynamic - Copilot.Core.Type.Equality - Copilot.Core.Type.Eq - Copilot.Core.Type.Show - Copilot.Core.Type.Read - Copilot.Core.Type.Uninitialized - Copilot.Core.PrettyPrint - Copilot.Core.PrettyDot + Copilot.Core.Type.Array + +test-suite unit-tests + type: + exitcode-stdio-1.0 + + main-is: + Main.hs + + other-modules: + Test.Extra + Test.Copilot.Core.Type + Test.Copilot.Core.Type.Array + + build-depends: + base + , HUnit + , QuickCheck + , test-framework + , test-framework-hunit + , test-framework-quickcheck2 + + , copilot-core + + hs-source-dirs: + tests + + default-language: + Haskell2010 + + ghc-options: + -Wall diff --git a/src/Copilot/Compile/Header/C99.hs b/src/Copilot/Compile/Header/C99.hs deleted file mode 100644 --- a/src/Copilot/Compile/Header/C99.hs +++ /dev/null @@ -1,223 +0,0 @@ --------------------------------------------------------------------------------- --- Copyright © 2011 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - --- | Generates a C99 header from a copilot-specification. The functionality --- provided by the header must be implemented by back-ends targetting C99. - -{-# LANGUAGE Safe #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE Rank2Types #-} - -module Copilot.Compile.Header.C99 - ( genC99Header - , c99HeaderName - ) where - -import Copilot.Core -import Data.List (intersperse, nubBy) -import Text.PrettyPrint.HughesPJ -import Prelude hiding (unlines) - --------------------------------------------------------------------------------- - -genC99Header :: Maybe String -> FilePath -> Spec -> IO () -genC99Header mprefix path spec = - let - filePath = path ++ "/" ++ prefix ++ "copilot.h" - prefix = case mprefix of - Just cs -> cs ++ "_" - _ -> "" - in - writeFile filePath (c99Header prefix spec) - -c99HeaderName :: Maybe String -> String -c99HeaderName (Just cs) = cs ++ "_" ++ "copilot.h" -c99HeaderName _ = "copilot.h" - -c99Header :: String -> Spec -> String -c99Header prefix spec = render $ vcat $ - [ text "/* Generated by Copilot Core." <+> text "*/" - , text "" - , ppHeaders - , text "" - , text "/* Observers (defined by Copilot): */" - , text "" - , ppObservers prefix (specObservers spec) - , text "" - , text "/* Triggers (must be defined by user): */" - , text "" - , ppTriggerPrototypes prefix (specTriggers spec) - , text "" - , text "/* External structs (must be defined by user): */" - , text "" - , ppExternalStructs (externStructs spec) - , text "" - , text "/* External variables (must be defined by user): */" - , text "" - , ppExternalVariables (externVars spec) - , text "" - , text "/* External arrays (must be defined by user): */" - , text "" - , ppExternalArrays (externArrays spec) - , text "" - , text "/* External functions (must be defined by user): */" - , text "" - , ppExternalFunctions (externFuns spec) - , text "" - , text "/* Step function: */" - , text "" - , ppStep prefix - ] - --------------------------------------------------------------------------------- - -ppHeaders :: Doc -ppHeaders = unlines - [ "#include " - , "#include " - ] - --------------------------------------------------------------------------------- - -ppObservers :: String -> [Observer] -> Doc -ppObservers prefix = vcat . map ppObserver - - where - - ppObserver :: Observer -> Doc - ppObserver - Observer - { observerName = name - , observerExprType = t } = - text "extern" <+> text (typeSpec (UType t)) <+> - text (prefix ++ name) <> text ";" - --------------------------------------------------------------------------------- - -ppTriggerPrototypes :: String -> [Trigger] -> Doc -ppTriggerPrototypes prefix = vcat . map ppTriggerPrototype - - where - - ppTriggerPrototype :: Trigger -> Doc - ppTriggerPrototype - Trigger - { triggerName = name - , triggerArgs = args } = - text "void" <+> text (prefix ++ name) <> - text "(" <> ppArgs args <> text ");" - - where - ppArgs :: [UExpr] -> Doc - ppArgs = hcat . intersperse (text ", ") . map ppArg - - ppArg :: UExpr -> Doc - ppArg UExpr { uExprType = t } = text (typeSpec (UType t)) - --------------------------------------------------------------------------------- - -ppExternalVariables :: [ExtVar] -> Doc -ppExternalVariables = vcat . map ppExternalVariable - -ppExternalVariable :: ExtVar -> Doc -ppExternalVariable - ExtVar - { externVarName = name - , externVarType = t } = - text "extern" <+> text (typeSpec t) <+> text name <> text ";" - --------------------------------------------------------------------------------- - -ppExternalArrays :: [ExtArray] -> Doc -ppExternalArrays = vcat . map ppExternalArray . nubBy eq - where - eq ExtArray { externArrayName = name1 } ExtArray { externArrayName = name2 } = - name1 == name2 - -ppExternalArray :: ExtArray -> Doc -ppExternalArray - ExtArray - { externArrayName = name - , externArrayElemType = t - , externArraySize = size } - = - text "extern" <+> text (typeSpec (UType t)) - <+> text name <> lbrack <> int size <> rbrack - <> text ";" - --------------------------------------------------------------------------------- - -ppExternalFunctions :: [ExtFun] -> Doc -ppExternalFunctions = vcat . map ppExternalFunction . nubBy eq - where - eq ExtFun { externFunName = name1 } ExtFun { externFunName = name2 } = - name1 == name2 - -ppExternalFunction :: ExtFun -> Doc -ppExternalFunction - ExtFun - { externFunName = name - , externFunType = t - , externFunArgs = args } = - text (typeSpec (UType t)) <+> text name <> - text "(" <> ppArgs args <> text ");" - - where - ppArgs :: [UExpr] -> Doc - ppArgs = hcat . intersperse (text ",") . map ppArg - - ppArg :: UExpr -> Doc - ppArg UExpr { uExprType = t1 } = text (typeSpec (UType t1)) - --------------------------------------------------------------------------------- - -ppExternalStructs :: [ExtStruct] -> Doc -ppExternalStructs = vcat . map ppExternalStruct . nubBy eq - where - eq ExtStruct { externStructName = name1 } ExtStruct { externStructName = name2 } = - name1 == name2 - -ppExternalStruct :: ExtStruct -> Doc -ppExternalStruct - ExtStruct - { externStructName = name - , externStructArgs = args } = - hang (hang (text "struct" <+> text name <+> text "{") 1 (nest 1 (ppStructArgs args))) 1 (text "};") - - where - ppStructArgs :: [(Name, UExpr)] -> Doc - ppStructArgs = vcat . map ppStructArg - - ppStructArg :: (Name, UExpr) -> Doc - ppStructArg (name', UExpr { uExprType = t1 }) = text (typeSpec (UType t1)) <+> - text name' <> text ";" - --------------------------------------------------------------------------------- - -typeSpec :: UType -> String -typeSpec UType { uTypeType = t } - = case t of - Bool -> "bool" - Int8 -> "int8_t" - Int16 -> "int16_t" - Int32 -> "int32_t" - Int64 -> "int64_t" - Word8 -> "uint8_t" - Word16 -> "uint16_t" - Word32 -> "uint32_t" - Word64 -> "uint64_t" - Float -> "float" - Double -> "double" - --------------------------------------------------------------------------------- - -ppStep :: String -> Doc -ppStep prefix = text "void" <+> text (prefix ++ "step") <> text "(void);" - --------------------------------------------------------------------------------- - -unlines :: [String] -> Doc -unlines = vcat . map text - --------------------------------------------------------------------------------- diff --git a/src/Copilot/Core.hs b/src/Copilot/Core.hs --- a/src/Copilot/Core.hs +++ b/src/Copilot/Core.hs @@ -1,49 +1,41 @@ --------------------------------------------------------------------------------- --- Copyright © 2011 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- +{-# LANGUAGE Safe #-} --- | Intermediate representation for Copilot specifications. --- The form of the representation is based on this paper: +-- | +-- 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, -- \"/Finally tagless, partially evaluated: Tagless staged/ -- /interpreters for simpler typed languages/\", -- Journal of Functional Programming vol. 19, p. 509-543, 2009. -- --- The following article might also be useful: --- -- * Guillemette, Louis-Julien and Monnier, Stefan, -- \"/Type-Safe Code Transformations in Haskell/\", -- Electronic Notes in Theoretical Computer Science vol. 174, p. 23-39, 2007. -- -- For examples of how to traverse a Copilot specification see --- the source code of the interpreter --- ("Copilot.Core.Interpret") --- and the pretty-printer --- ("Copilot.Core.PrettyPrint"). - -{-# LANGUAGE Safe #-} - +-- the source code of the interpreter (@copilot-interpreter@) +-- and the pretty-printer (@copilot-prettyprinter@). module Copilot.Core - ( module Copilot.Core.Error - , module Copilot.Core.Expr - , module Copilot.Core.External - , module Copilot.Core.MakeTags - , module Copilot.Core.Operators - , module Copilot.Core.Spec - , module Copilot.Core.Type - , module Copilot.Core.Type.Uninitialized - , module Data.Int - , module Data.Word - ) where + ( module Copilot.Core.Expr + , module Copilot.Core.Operators + , module Copilot.Core.Spec + , module Copilot.Core.Type + , module Copilot.Core.Type.Array + , module Data.Int + , module Data.Word + ) + where -import Copilot.Core.Error +-- External imports +import Data.Int +import Data.Word + +-- Internal imports import Copilot.Core.Expr -import Copilot.Core.External -import Copilot.Core.MakeTags import Copilot.Core.Operators import Copilot.Core.Spec import Copilot.Core.Type -import Copilot.Core.Type.Uninitialized -import Data.Int -import Data.Word +import Copilot.Core.Type.Array diff --git a/src/Copilot/Core/Error.hs b/src/Copilot/Core/Error.hs deleted file mode 100644 --- a/src/Copilot/Core/Error.hs +++ /dev/null @@ -1,19 +0,0 @@ --------------------------------------------------------------------------------- --- Copyright © 2011 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - -{-# LANGUAGE Safe #-} - -module Copilot.Core.Error - ( impossible - , badUsage ) where - -impossible :: String -> String -> a -impossible function package = - error $ "\"Impossible\" error in function " - ++ function ++ ", in package " ++ package - ++ ". Please email Lee Pike at " ++ - "(remove spaces) or file a bug report on github.com." - -badUsage :: String -> a -badUsage msg = error $ "Copilot error: " ++ msg diff --git a/src/Copilot/Core/Expr.hs b/src/Copilot/Core/Expr.hs --- a/src/Copilot/Core/Expr.hs +++ b/src/Copilot/Core/Expr.hs @@ -1,69 +1,70 @@ --------------------------------------------------------------------------------- --- Copyright © 2011 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - -{-# LANGUAGE Safe #-} -{-# LANGUAGE GADTs, ExistentialQuantification #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE Safe #-} +-- | +-- Description: Internal representation of Copilot stream expressions. +-- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc. module Copilot.Core.Expr - ( Id - , Name - , Expr (..) - , UExpr (..) - , SExpr (..) - , DropIdx - , Tag - ) where + ( Id + , Name + , Expr (..) + , UExpr (..) + , DropIdx + ) + where -import Copilot.Core.Operators (Op1, Op2, Op3) -import Copilot.Core.Type (Type) -import Data.Word (Word32) +-- 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 --------------------------------------------------------------------------------- - -- | A name of a trigger, an external variable, or an external function. type Name = String --------------------------------------------------------------------------------- - -- | An index for the drop operator. type DropIdx = Word32 --------------------------------------------------------------------------------- +-- | Internal representation of Copilot stream expressions. +-- +-- The Core representation mimics the high-level Copilot stream, but the Core +-- representation contains information about the types of elements in the +-- stream. +data Expr a where + Const :: Typeable a + => Type a -> a -> Expr a --- | A unique tag for external arrays/function calls. -type Tag = Int + Drop :: Typeable a + => Type a -> DropIdx -> Id -> Expr a --------------------------------------------------------------------------------- + Local :: Typeable a + => Type a -> Type b -> Name -> Expr a -> Expr b -> Expr b -data Expr a where - Const :: Type a -> a -> Expr a - Drop :: Type a -> DropIdx -> Id -> Expr a - Local :: Type a -> Type b -> Name -> Expr a -> Expr b -> Expr b - Var :: Type a -> Name -> Expr a - ExternVar :: Type a -> Name -> Maybe [a] -> Expr a - ExternFun :: Type a -> Name -> [UExpr] -> Maybe (Expr a) - -> Maybe Tag -> Expr a - ExternArray :: Integral a => Type a -> Type b -> Name -> Int -> Expr a - -> Maybe [[b]] -> Maybe Tag -> Expr b - ExternStruct :: Type a -> Name -> [(Name, UExpr)] -> Maybe Tag -> Expr a - GetField :: Type a -> Type b -> Expr a -> Name -> Expr b - Op1 :: Op1 a b -> Expr a -> Expr b - Op2 :: Op2 a b c -> Expr a -> Expr b -> Expr c - Op3 :: Op3 a b c d -> Expr a -> Expr b -> Expr c -> Expr d - Label :: Type a -> String -> Expr a -> Expr a + Var :: Typeable a + => Type a -> Name -> Expr a --------------------------------------------------------------------------------- + ExternVar :: Typeable a + => Type a -> Name -> Maybe [a] -> Expr a --- | A untyped expression (no phantom type). -data UExpr = forall a. UExpr - { uExprType :: Type a - , uExprExpr :: Expr a } + Op1 :: Typeable a + => Op1 a b -> Expr a -> Expr b --- | An expression for Struct args -data SExpr = SExpr { sname :: String, uexpr :: UExpr } + 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 (Type a) (Expr a) diff --git a/src/Copilot/Core/External.hs b/src/Copilot/Core/External.hs deleted file mode 100644 --- a/src/Copilot/Core/External.hs +++ /dev/null @@ -1,174 +0,0 @@ --------------------------------------------------------------------------------- --- Copyright © 2011 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - -{-# LANGUAGE Trustworthy #-} -{-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE Rank2Types #-} - -module Copilot.Core.External - ( ExtVar (..), ExtArray (..), ExtFun (..), ExtStruct (..) - , externVars, externArrays, externFuns, externStructs - ) where - -import Copilot.Core.Expr -import Copilot.Core.Type -import Copilot.Core.Spec -import Data.DList (DList, empty, singleton, append, concat, toList) -import Data.List (nubBy) -import Prelude hiding (all, concat, foldr) - --------------------------------------------------------------------------------- - -data ExtVar = ExtVar - { externVarName :: Name - , externVarType :: UType } - -data ExtArray = forall a b . Integral a => ExtArray - { externArrayName :: Name - , externArrayElemType :: Type b - , externArrayIdx :: Expr a - , externArrayIdxType :: Type a - , externArraySize :: Int - , externArrayTag :: Maybe Tag } - -data ExtFun = forall a . ExtFun - { externFunName :: Name - , externFunType :: Type a - , externFunArgs :: [UExpr] - , externFunTag :: Maybe Tag } - -data ExtStruct = ExtStruct - { externStructName :: Name - , externStructArgs :: [(Name, UExpr)] - , externStructTag :: Maybe Tag } - --------------------------------------------------------------------------------- - -externVars :: Spec -> [ExtVar] -externVars = nubBy eqExt . toList . all externVarsExpr - where - eqExt :: ExtVar -> ExtVar -> Bool - eqExt ExtVar { externVarName = name1 } ExtVar { externVarName = name2 } = - name1 == name2 - -externVarsExpr :: Expr a -> DList ExtVar -externVarsExpr e0 = case e0 of - Const _ _ -> empty - Drop _ _ _ -> empty - Local _ _ _ e1 e2 -> externVarsExpr e1 `append` externVarsExpr e2 - Var _ _ -> empty - ExternVar t name _ -> singleton (ExtVar name (UType t)) - ExternArray _ _ _ _ e _ _ -> externVarsExpr e - ExternFun _ _ ues _ _ -> concat (map externVarsUExpr ues) - ExternStruct _ _ _ _ -> empty - GetField _ _ _ _ -> empty - Op1 _ e -> externVarsExpr e - Op2 _ e1 e2 -> externVarsExpr e1 `append` externVarsExpr e2 - Op3 _ e1 e2 e3 -> externVarsExpr e1 `append` - externVarsExpr e2 `append` - externVarsExpr e3 - Label _ _ e -> externVarsExpr e - -externVarsUExpr :: UExpr -> DList ExtVar -externVarsUExpr UExpr { uExprExpr = e } = externVarsExpr e - --------------------------------------------------------------------------------- - -externArrays :: Spec -> [ExtArray] -externArrays = toList . all externArraysExpr - -externArraysExpr :: Expr a -> DList ExtArray -externArraysExpr e0 = case e0 of - Const _ _ -> empty - Drop _ _ _ -> empty - Local _ _ _ e1 e2 -> externArraysExpr e1 `append` externArraysExpr e2 - Var _ _ -> empty - ExternVar _ _ _ -> empty - ExternArray t1 t2 name - size idx _ tag -> singleton (ExtArray name t2 idx t1 size tag) - ExternFun _ _ ues _ _ -> concat (map externArraysUExpr ues) - ExternStruct _ _ _ _ -> empty - GetField _ _ _ _ -> empty - Op1 _ e -> externArraysExpr e - Op2 _ e1 e2 -> externArraysExpr e1 `append` externArraysExpr e2 - Op3 _ e1 e2 e3 -> externArraysExpr e1 `append` - externArraysExpr e2 `append` - externArraysExpr e3 - Label _ _ e -> externArraysExpr e - -externArraysUExpr :: UExpr -> DList ExtArray -externArraysUExpr UExpr { uExprExpr = e } = externArraysExpr e - --------------------------------------------------------------------------------- - -externFuns :: Spec -> [ExtFun] -externFuns = toList . all externFunsExpr - -externFunsExpr :: Expr a -> DList ExtFun -externFunsExpr e0 = case e0 of - Const _ _ -> empty - Drop _ _ _ -> empty - Local _ _ _ e1 e2 -> externFunsExpr e1 `append` externFunsExpr e2 - Var _ _ -> empty - ExternVar _ _ _ -> empty - ExternArray _ _ _ _ idx _ _ -> externFunsExpr idx - ExternFun t name ues _ tag -> concat $ singleton (ExtFun name t ues tag) : (map externFunsUExpr ues) - ExternStruct _ _ _ _ -> empty - GetField _ _ _ _ -> empty - Op1 _ e -> externFunsExpr e - Op2 _ e1 e2 -> externFunsExpr e1 `append` externFunsExpr e2 - Op3 _ e1 e2 e3 -> externFunsExpr e1 `append` - externFunsExpr e2 `append` - externFunsExpr e3 - Label _ _ e -> externFunsExpr e - -externFunsUExpr :: UExpr -> DList ExtFun -externFunsUExpr UExpr { uExprExpr = e } = externFunsExpr e - - --------------------------------------------------------------------------------- - -externStructs :: Spec -> [ExtStruct] -externStructs = toList . all externStructsExpr - -externStructsExpr :: Expr a -> DList ExtStruct -externStructsExpr e0 = case e0 of - Const _ _ -> empty - Drop _ _ _ -> empty - Local _ _ _ _ _ -> empty - Var _ _ -> empty - ExternVar _ _ _ -> empty - ExternArray _ _ _ _ _ _ _ -> empty - ExternFun _ _ _ _ _ -> empty - ExternStruct _ name ses tag -> singleton (ExtStruct name ses tag) - -- all expressions in a struct are typed - GetField _ _ _ _ -> empty - Op1 _ _ -> empty - Op2 _ _ _ -> empty - Op3 _ _ _ _ -> empty - Label _ _ e -> externStructsExpr e - --------------------------------------------------------------------------------- - -all :: (forall a . Expr a -> DList b) -> Spec -> DList b -all f spec = - concat (fmap (allStream) (specStreams spec)) `append` - concat (fmap allTrigger (specTriggers spec)) `append` - concat (fmap allObserver (specObservers spec)) - - where - - allStream - Stream { streamExpr = e } = f e - - allTrigger - Trigger - { triggerGuard = e - , triggerArgs = args } = f e `append` concat (fmap allUExpr args) - - allUExpr - (UExpr _ e1) = f e1 - - allObserver - Observer { observerExpr = e } = f e diff --git a/src/Copilot/Core/Interpret.hs b/src/Copilot/Core/Interpret.hs deleted file mode 100644 --- a/src/Copilot/Core/Interpret.hs +++ /dev/null @@ -1,27 +0,0 @@ --------------------------------------------------------------------------------- --- Copyright © 2011 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - --- | An interpreter for Copilot specifications. - -{-# LANGUAGE Safe #-} - -module Copilot.Core.Interpret - ( Format (..) - , interpret - ) where - -import Copilot.Core -import Copilot.Core.Interpret.Eval -import Copilot.Core.Interpret.Render -import Copilot.Core.Type.Show (ShowType(..)) - -data Format = Table | CSV - --- | Interprets a Copilot specification. -interpret :: Format -> Int -> Spec -> String -interpret format k spec = - case format of - Table -> renderAsTable e - CSV -> renderAsCSV e - where e = eval Haskell k spec diff --git a/src/Copilot/Core/Interpret/Eval.hs b/src/Copilot/Core/Interpret/Eval.hs deleted file mode 100644 --- a/src/Copilot/Core/Interpret/Eval.hs +++ /dev/null @@ -1,391 +0,0 @@ --------------------------------------------------------------------------------- --- Copyright © 2011 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - --- | A tagless interpreter for Copilot specifications. - -{-# LANGUAGE Safe #-} -{-# LANGUAGE GADTs, BangPatterns, DeriveDataTypeable #-} - -module Copilot.Core.Interpret.Eval - ( --ExtEnv (..) - Env - , Output - , ExecTrace (..) - , eval - ) where - -import Copilot.Core -import Copilot.Core.Type.Dynamic -import Copilot.Core.Type.Show (showWithType, ShowType) - -import Prelude hiding (id) -import qualified Prelude as P - -import Data.List (transpose) -import qualified Data.Map as M -import Data.Map (Map) -import Data.Maybe (fromJust) -import Data.Bits -import Control.Exception (Exception, throw) -import Data.Typeable - --------------------------------------------------------------------------------- - -data InterpException - = -- NoValues Name --- | BadType Name - ArrayWrongSize Name Int - | ArrayIdxOutofBounds Name Int Int - | DivideByZero - | NotEnoughValues Name Int --- | NoExtFunEval Name - | NoExtsInterp Name - deriving Typeable - -instance Show InterpException where - --------------------------------------- - -- show (NoValues name) = - -- badUsage $ "you need to supply a list of values for interpreting " - -- ++ "external element " ++ name ++ "." - --------------------------------------- - - -- -- Should always be caught by Analyze.hs in copilot-language. - -- show (BadType name) = - -- badUsage $ "you probably gave the wrong type for external element " - -- ++ name ++ ". Recheck your types and re-evaluate." - --------------------------------------- - show (ArrayWrongSize name expectedSize) = - badUsage $ "in the environment for external array " ++ name - ++ ", we expect a list of length " ++ show expectedSize - ++ ", but the length of the array you supplied is of a different length." - --------------------------------------- - show (ArrayIdxOutofBounds name index size) = - badUsage $ "in the environment for external array " ++ name - ++ ", you gave an index of " ++ show index - ++ " where the size of the array is " ++ show size ++ "; the size must " - ++ " be strictly greater than the index." - --------------------------------------- - show DivideByZero = - badUsage "divide by zero." - --------------------------------------- - show (NotEnoughValues name k) = - badUsage $ "on the " ++ show k ++ "th iteration, we ran out of " - ++ "values for simulating the external element " ++ name ++ "." - --------------------------------------- - show (NoExtsInterp name) = - badUsage $ "in a call of external symbol " ++ name ++ ", you did not " - ++ "provide an expression for interpretation. In your external " - ++ "declaration, you need to provide a 'Just strm', where 'strm' is " - ++ "some stream with which to simulate the function." - --------------------------------------- - -instance Exception InterpException - --------------------------------------------------------------------------------- - -type Env nm = [(nm, DynamicF [] Type)] - --- -- | External arrays environment. --- type ArrEnv = [(Name, [DynamicF [] Type])] - --- -- | Environment for simulation. --- data ExtEnv = ExtEnv { varEnv :: Env Name --- , arrEnv :: ArrEnv --- -- , funcEnv :: [(Name, Spec)] --- } - --------------------------------------------------------------------------------- - -type Output = String - -data ExecTrace = ExecTrace - -- map from trigger names to their maybe output, which is a list of strings - -- representing their values. (Nothing output if the guard for the trigger - -- is false). The order is important, since we compare the arg lists - -- between the interpreter and backends. - { interpTriggers :: Map String [Maybe [Output]] - -- map from observer names to their outputs. We also show observer outputs. - , interpObservers :: Map String [Output] } - deriving Show - --------------------------------------------------------------------------------- - -{- -eval :: Int -> Env Name -> Spec -> ExecTrace -eval k exts spec = - let - strms = fmap (evalStream exts strms) (specStreams spec) - trigs = fmap (evalTrigger k exts strms) (specTriggers spec) - obsvs = fmap (evalObserver k exts strms) (specObservers spec) - in - ExecTrace - { interpTriggers = M.fromList $ - zip (fmap triggerName (specTriggers spec)) trigs - , interpObservers = M.fromList $ - zip (fmap observerName (specObservers spec)) obsvs - } --} - --- We could write this in a beautiful lazy style like above, but that creates a --- space leak in the interpreter that is hard to fix while maintaining laziness. --- We take a more brute-force appraoch below. -eval :: ShowType -> Int -> Spec -> ExecTrace -eval showType k spec = --- let exts = take k $ reverse exts' in - - let initStrms = map initStrm (specStreams spec) in - - let strms = evalStreams k (specStreams spec) initStrms in - - let trigs = map (evalTrigger showType k strms) - (specTriggers spec) in - - let obsvs = map (evalObserver showType k strms) - (specObservers spec) in - - strms `seq` ExecTrace - { interpTriggers = M.fromList $ - zip (map triggerName (specTriggers spec)) trigs - , interpObservers = M.fromList $ - zip (map observerName (specObservers spec)) obsvs - } - --------------------------------------------------------------------------------- - -type LocalEnv = [(Name, Dynamic Type)] - -evalExpr_ :: Int -> Expr a -> LocalEnv -> Env Id -> a -evalExpr_ k e0 locs strms = case e0 of - Const _ x -> x - Drop t i id -> - let Just xs = lookup id strms >>= fromDynF t in - reverse xs !! (fromIntegral i + k) - Local t1 _ name e1 e2 -> - let x = evalExpr_ k e1 locs strms in - let locs' = (name, toDyn t1 x) : locs in - x `seq` locs' `seq` evalExpr_ k e2 locs' strms - Var t name -> fromJust $ lookup name locs >>= fromDyn t - ExternVar _ name xs -> evalExternVar k name xs - ExternFun _ name _ expr _ -> --evalFunc k t name expr - case expr of - Nothing -> throw (NoExtsInterp name) - Just e -> evalExpr_ k e locs strms - ExternArray _ _ name size idx xs _ -> evalArray k name evalIdx xs size - where evalIdx = evalExpr_ k idx locs strms - ExternStruct _ _ _ _ -> error "unimplemented" - GetField _ _ _ _ -> error "unimplemented" - Op1 op e1 -> - let ev1 = evalExpr_ k e1 locs strms in - let op1 = evalOp1 op in - ev1 `seq` op1 `seq` op1 ev1 - Op2 op e1 e2 -> - let ev1 = evalExpr_ k e1 locs strms in - let ev2 = evalExpr_ k e2 locs strms in - let op2 = evalOp2 op in - ev1 `seq` ev2 `seq` op2 `seq` op2 ev1 ev2 - Op3 op e1 e2 e3 -> - let ev1 = evalExpr_ k e1 locs strms in - let ev2 = evalExpr_ k e2 locs strms in - let ev3 = evalExpr_ k e3 locs strms in - let op3 = evalOp3 op in - ev1 `seq` ev2 `seq` ev3 `seq` op3 `seq` op3 ev1 ev2 ev3 - Label _ _ e1 -> - let ev1 = evalExpr_ k e1 locs strms in - ev1 - --------------------------------------------------------------------------------- - -evalExternVar :: Int -> Name -> Maybe [a] -> a -evalExternVar k name exts = - case exts of - Nothing -> throw (NoExtsInterp name) - Just xs -> - case safeIndex k xs of - Nothing -> throw (NotEnoughValues name k) - Just x -> x - --------------------------------------------------------------------------------- - --- evalFunc :: Int -> Type a -> Name -> Expr a -> ExtEnv -> a --- evalFunc k t name expr exts = --- evalExpr k expr - --- case lookup name (funcEnv exts) of --- Nothing -> throw (NoValues name) - --- -- We created this spec in Interpreter.hs, copilot-language, so it should --- -- contain no triggers and exactly one observer. --- Just Spec { specStreams = specStrms --- , specObservers = obsLs } -> --- let initStrms = map initStrm specStrms in --- let strms = evalStreams k exts specStrms initStrms in --- case obsLs of --- [Observer { observerExpr = expr_ --- , observerExprType = t1 }] -> --- let dyn = toDynF t1 expr_ in --- case fromDynF t dyn of --- Nothing -> throw (BadType name) --- Just expr -> evalExpr_ k expr exts [] strms --- _ -> throw (BadType name) - --------------------------------------------------------------------------------- - -evalArray :: Integral b => Int -> Name -> b -> Maybe [[a]] -> Int -> a -evalArray k name idx exts size = - case exts of - Nothing -> throw (NoExtsInterp name) - Just xs -> - case safeIndex k xs of - Nothing -> throw (NotEnoughValues name k) - Just arr -> -- convoluted form in case the array is env of infinite - -- length. - if length (take size arr) == size - && length (take (size+1) arr) == size - then case safeIndex (fromIntegral idx) arr of - Nothing -> throw (ArrayIdxOutofBounds - name (fromIntegral idx) size) - Just x -> x - else throw (ArrayWrongSize name size) - --------------------------------------------------------------------------------- - -evalOp1 :: Op1 a b -> (a -> b) -evalOp1 op = case op of - Not -> P.not - Abs _ -> P.abs - Sign _ -> P.signum - Recip _ -> P.recip - Exp _ -> P.exp - Sqrt _ -> P.sqrt - Log _ -> P.log - Sin _ -> P.sin - Tan _ -> P.tan - Cos _ -> P.cos - Asin _ -> P.asin - Atan _ -> P.atan - Acos _ -> P.acos - Sinh _ -> P.sinh - Tanh _ -> P.tanh - Cosh _ -> P.cosh - Asinh _ -> P.asinh - Atanh _ -> P.atanh - Acosh _ -> P.acosh - BwNot _ -> complement - Cast _ _ -> P.fromIntegral - --------------------------------------------------------------------------------- - -evalOp2 :: Op2 a b c -> (a -> b -> c) -evalOp2 op = case op of - And -> (&&) - Or -> (||) - Add _ -> (+) - Sub _ -> (-) - Mul _ -> (*) - Mod _ -> (catchZero P.mod) - Div _ -> (catchZero P.div) - Fdiv _ -> (P./) - Pow _ -> (P.**) - Logb _ -> P.logBase - Eq _ -> (==) - Ne _ -> (/=) - Le _ -> (<=) - Ge _ -> (>=) - Lt _ -> (<) - Gt _ -> (>) - BwAnd _ -> (.&.) - BwOr _ -> (.|.) - BwXor _ -> (xor) - BwShiftL _ _ -> ( \ !a !b -> shiftL a $! fromIntegral b ) - BwShiftR _ _ -> ( \ !a !b -> shiftR a $! fromIntegral b ) - -catchZero :: Integral a => (a -> a -> a) -> (a -> a -> a) -catchZero _ _ 0 = throw DivideByZero -catchZero f x y = f x y - --------------------------------------------------------------------------------- - -evalOp3 :: Op3 a b c d -> (a -> b -> c -> d) -evalOp3 (Mux _) = \ !v !x !y -> if v then x else y - --------------------------------------------------------------------------------- - -initStrm :: Stream -> (Id, DynamicF [] Type) -initStrm Stream { streamId = id - , streamBuffer = buffer - , streamExprType = t } = - (id, toDynF t (reverse buffer)) - --- XXX actually only need to compute until shortest stream is of length k --- XXX this should just be a foldl' over [0,1..k] -evalStreams :: Int -> [Stream] -> Env Id -> Env Id -evalStreams top specStrms initStrms = - evalStreams_ 0 initStrms - where - evalStreams_ :: Int -> Env Id -> Env Id - evalStreams_ k strms | k == top = strms - evalStreams_ k strms | otherwise = - evalStreams_ (k+1) $! strms_ - where - strms_ = map evalStream specStrms - evalStream Stream { streamId = id - , streamExpr = e - , streamExprType = t } = - let xs = fromJust $ lookup id strms >>= fromDynF t in - let x = evalExpr_ k e [] strms in - let ls = x `seq` (x:xs) in - (id, toDynF t ls) - --------------------------------------------------------------------------------- - -evalTrigger :: - ShowType -> Int -> Env Id -> Trigger -> [Maybe [Output]] -evalTrigger showType k strms - Trigger - { triggerGuard = e - , triggerArgs = args - } = map tag (zip bs vs) - - where - tag :: (Bool, a) -> Maybe a - tag (True, x) = Just x - tag (False, _) = Nothing - - -- Is the guard true? - bs :: [Bool] - bs = evalExprs_ k e strms - - -- The argument outputs. - vs :: [[Output]] - vs = if null args then replicate k [] -- might be 0 args. - else transpose $ map evalUExpr args - - evalUExpr :: UExpr -> [Output] - evalUExpr (UExpr t e1) = - map (showWithType showType t) (evalExprs_ k e1 strms) - --------------------------------------------------------------------------------- -evalObserver :: ShowType -> Int -> Env Id -> Observer -> [Output] -evalObserver showType k strms - Observer - { observerExpr = e - , observerExprType = t } - = map (showWithType showType t) (evalExprs_ k e strms) - --------------------------------------------------------------------------------- - -evalExprs_ :: Int -> Expr a -> Env Id -> [a] -evalExprs_ k e strms = - map (\i -> evalExpr_ i e [] strms) [0..(k-1)] - --------------------------------------------------------------------------------- - --- | Safe indexing (!!) on possibly infininite lists. -safeIndex :: Int -> [a] -> Maybe a -safeIndex i ls = - let ls' = take (i+1) ls in - if length ls' > i then Just (ls' !! i) - else Nothing - --------------------------------------------------------------------------------- diff --git a/src/Copilot/Core/Interpret/Render.hs b/src/Copilot/Core/Interpret/Render.hs deleted file mode 100644 --- a/src/Copilot/Core/Interpret/Render.hs +++ /dev/null @@ -1,97 +0,0 @@ --------------------------------------------------------------------------------- --- Copyright © 2011 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - --- | An tagless interpreter for Copilot specifications. - -{-# LANGUAGE Safe #-} - -module Copilot.Core.Interpret.Render - ( renderAsTable - , renderAsCSV - ) where - -import Data.List (intersperse, transpose, foldl') -import Data.Maybe (catMaybes) -import Copilot.Core.Interpret.Eval (Output, ExecTrace (..)) -import qualified Data.Map as M -import Text.PrettyPrint.NCol (asColumns) -import Text.PrettyPrint (Doc, ($$), (<>), text, render, empty) - --------------------------------------------------------------------------------- - -renderAsTable :: ExecTrace -> String -renderAsTable - ExecTrace - { interpTriggers = trigs - , interpObservers = obsvs } = - ( render - . asColumns - . transpose - . (:) (ppTriggerNames ++ ppObserverNames) - . transpose - ) (ppTriggerOutputs ++ ppObserverOutputs) - - where - - ppTriggerNames :: [Doc] - ppTriggerNames = map (text . (++ ":")) (M.keys trigs) - - ppObserverNames :: [Doc] - ppObserverNames = map (text . (++ ":")) (M.keys obsvs) - - ppTriggerOutputs :: [[Doc]] - ppTriggerOutputs = map (map ppTriggerOutput) (M.elems trigs) - - ppTriggerOutput :: Maybe [Output] -> Doc - ppTriggerOutput (Just vs) = text $ "(" ++ concat (intersperse "," vs) ++ ")" - ppTriggerOutput Nothing = text "--" - - ppObserverOutputs :: [[Doc]] - ppObserverOutputs = map (map text) (M.elems obsvs) - --------------------------------------------------------------------------------- - -renderAsCSV :: ExecTrace -> String -renderAsCSV = render . unfold - -unfold :: ExecTrace -> Doc -unfold r = - case step r of - (cs, Nothing) -> cs - (cs, Just r') -> cs $$ unfold r' - -step :: ExecTrace -> (Doc, Maybe ExecTrace) -step ExecTrace - { interpTriggers = trigs - } = - if M.null trigs then (empty, Nothing) - else (foldl' ($$) empty (text "#" : ppTriggerOutputs), tails) - - where - - ppTriggerOutputs :: [Doc] - ppTriggerOutputs = - catMaybes - . fmap ppTriggerOutput - . M.assocs - . fmap head - $ trigs - - ppTriggerOutput :: (String, Maybe [Output]) -> Maybe Doc - ppTriggerOutput (_, Nothing) = Nothing - ppTriggerOutput (cs, Just xs) = Just $ - text cs <> text "," <> - (foldr (<>) empty . map text . intersperse ",") xs - - tails :: Maybe ExecTrace - tails = - if any null (M.elems (fmap tail trigs)) - then Nothing - else Just - ExecTrace - { interpTriggers = fmap tail trigs - , interpObservers = M.empty - } - --------------------------------------------------------------------------------- diff --git a/src/Copilot/Core/Locals.hs b/src/Copilot/Core/Locals.hs deleted file mode 100644 --- a/src/Copilot/Core/Locals.hs +++ /dev/null @@ -1,90 +0,0 @@ --------------------------------------------------------------------------------- --- Copyright © 2011 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - --- | Let expressions. - -{-# LANGUAGE Trustworthy #-} -{-# LANGUAGE ExistentialQuantification #-} - -module Copilot.Core.Locals - ( Loc (..) - , locals - ) where - -import Copilot.Core -import Data.DList (DList, empty, singleton, append, concat, toList) -import Data.List (nubBy) -import Prelude hiding (concat, foldr) - --------------------------------------------------------------------------------- - -data Loc = forall a . Loc - { localName :: Name - , localType :: Type a } - -instance Show Loc where - show Loc { localName = name } = name - --------------------------------------------------------------------------------- - -locals :: Spec -> [Loc] -locals - Spec - { specStreams = streams - , specTriggers = triggers - , specObservers = observers - } = nubBy eqLoc . toList $ - concat (fmap locsStream streams) `append` - concat (fmap locsTrigger triggers) `append` - concat (fmap locsObserver observers) - - where - - eqLoc :: Loc -> Loc -> Bool - eqLoc Loc { localName = name1 } Loc { localName = name2 } = - name1 == name2 - --------------------------------------------------------------------------------- - -locsStream :: Stream -> DList Loc -locsStream Stream { streamExpr = e } = locsExpr e - --------------------------------------------------------------------------------- - -locsTrigger :: Trigger -> DList Loc -locsTrigger Trigger { triggerGuard = e, triggerArgs = args } = - locsExpr e `append` concat (fmap locsUExpr args) - - where - - locsUExpr :: UExpr -> DList Loc - locsUExpr (UExpr _ e1) = locsExpr e1 - --------------------------------------------------------------------------------- - -locsObserver :: Observer -> DList Loc -locsObserver Observer { observerExpr = e } = locsExpr e - --------------------------------------------------------------------------------- - -locsExpr :: Expr a -> DList Loc -locsExpr e0 = case e0 of - Const _ _ -> empty - Drop _ _ _ -> empty - Local t _ name e1 e2 -> singleton (Loc name t) - `append` locsExpr e1 - `append` locsExpr e2 - Var _ _ -> empty - ExternVar _ _ _ -> empty - ExternFun _ _ _ _ _ -> empty - ExternArray _ _ _ _ _ _ _ -> empty - ExternStruct _ _ _ _ -> empty - GetField _ _ _ _ -> empty - Op1 _ e -> locsExpr e - Op2 _ e1 e2 -> locsExpr e1 `append` locsExpr e2 - Op3 _ e1 e2 e3 -> locsExpr e1 `append` locsExpr e2 - `append` locsExpr e3 - Label _ _ e -> locsExpr e - --------------------------------------------------------------------------------- diff --git a/src/Copilot/Core/MakeTags.hs b/src/Copilot/Core/MakeTags.hs deleted file mode 100644 --- a/src/Copilot/Core/MakeTags.hs +++ /dev/null @@ -1,127 +0,0 @@ --------------------------------------------------------------------------------- --- Copyright © 2011 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - --- | Sets a unique tags for each external array/function/struct call. - -{-# LANGUAGE Safe #-} - -module Copilot.Core.MakeTags (makeTags) where - -import Copilot.Core.Expr -import Copilot.Core.Spec -import Control.Monad.State -import Prelude hiding (id) - -next :: State Int Int -next = do - k <- get - put (succ k) - return k - -makeTags :: Spec -> Spec -makeTags spec = evalState (mkTagsSpec spec) 0 - -mkTagsSpec :: Spec -> State Int Spec -mkTagsSpec - Spec - { specStreams = strms - , specObservers = obsvs - , specTriggers = trigs - , specProperties = props - } = - liftM4 Spec - (mkTagsStrms strms) - (mkTagsObsvs obsvs) - (mkTagsTrigs trigs) - (mkTagsProps props) - -mkTagsStrms :: [Stream] -> State Int [Stream] -mkTagsStrms = mapM mkTagsStrm - - where - mkTagsStrm Stream - { streamId = id - , streamBuffer = xs - , streamExpr = e - , streamExprType = t } = - do - e' <- mkTagsExpr e - return $ Stream - { streamId = id - , streamBuffer = xs - , streamExpr = e' - , streamExprType = t } - -mkTagsObsvs :: [Observer] -> State Int [Observer] -mkTagsObsvs = mapM mkTagsObsv - - where - mkTagsObsv Observer - { observerName = name - , observerExpr = e - , observerExprType = t } = - do - e' <- mkTagsExpr e - return $ Observer - { observerName = name - , observerExpr = e' - , observerExprType = t } - -mkTagsTrigs :: [Trigger] -> State Int [Trigger] -mkTagsTrigs = mapM mkTagsTrig - - where - mkTagsTrig Trigger - { triggerName = name - , triggerGuard = g - , triggerArgs = args } = - do - g' <- mkTagsExpr g - args' <- mapM mkTagsUExpr args - return $ Trigger - { triggerName = name - , triggerGuard = g' - , triggerArgs = args' } - -mkTagsProps :: [Property] -> State Int [Property] -mkTagsProps = mapM mkTagsProp - - where mkTagsProp p = do - e' <- mkTagsExpr (propertyExpr p) - return $ p { propertyExpr = e' } - -mkTagsSExpr :: (Name, UExpr) -> State Int (Name, UExpr) -mkTagsSExpr (name, UExpr { uExprExpr = e, uExprType = t }) = - do - e' <- mkTagsExpr e - return (name, UExpr { uExprExpr = e', uExprType = t }) - -mkTagsUExpr :: UExpr -> State Int UExpr -mkTagsUExpr UExpr { uExprExpr = e, uExprType = t } = - do - e' <- mkTagsExpr e - return $ UExpr { uExprExpr = e', uExprType = t } - -mkTagsExpr :: Expr a -> State Int (Expr a) -mkTagsExpr e0 = case e0 of - Const t x -> return $ Const t x - Drop t k id -> return $ Drop t k id - Local t1 t2 name e1 e2 -> liftM2 (Local t1 t2 name) (mkTagsExpr e1) (mkTagsExpr e2) - Var t name -> return $ Var t name - ExternVar t name e -> return $ ExternVar t name e - ExternFun t name args expr _ -> do args' <- mapM mkTagsUExpr args - k <- next - return $ ExternFun t name args' expr (Just k) - ExternArray t1 t2 name - size idx e _ -> do idx' <- mkTagsExpr idx - k <- next - return $ ExternArray t1 t2 name size idx' e (Just k) - ExternStruct t name sargs _ -> do args' <- mapM mkTagsSExpr sargs - k <- next - return $ ExternStruct t name args' (Just k) - GetField ts tf id name -> return $ GetField ts tf id name - Op1 op e -> liftM (Op1 op) (mkTagsExpr e) - Op2 op e1 e2 -> liftM2 (Op2 op) (mkTagsExpr e1) (mkTagsExpr e2) - Op3 op e1 e2 e3 -> liftM3 (Op3 op) (mkTagsExpr e1) (mkTagsExpr e2) (mkTagsExpr e3) - Label t s e -> liftM (Label t s) (mkTagsExpr e) diff --git a/src/Copilot/Core/Operators.hs b/src/Copilot/Core/Operators.hs --- a/src/Copilot/Core/Operators.hs +++ b/src/Copilot/Core/Operators.hs @@ -1,22 +1,28 @@ --------------------------------------------------------------------------------- --- Copyright © 2011 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - -{-# LANGUAGE Safe #-} -{-# LANGUAGE GADTs, Rank2Types #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE Safe #-} +-- | +-- 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 Copilot.Core.Type (Type) -import Data.Bits +-- External imports +import Data.Bits (Bits) +import Data.Typeable (Typeable) +import Data.Word (Word32) +import GHC.TypeLits (KnownSymbol) --------------------------------------------------------------------------------- +-- Internal imports +import Copilot.Core.Type (Field (..), Type (..)) +import Copilot.Core.Type.Array (Array) --- Unary operators. +-- | Unary operators. data Op1 a b where -- Boolean operators. Not :: Op1 Bool Bool @@ -41,11 +47,19 @@ Asinh :: Floating a => Type a -> Op1 a a Atanh :: Floating a => Type a -> Op1 a a Acosh :: Floating a => Type a -> Op1 a a + -- RealFrac operators + 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. + -- Struct operator. + GetField :: KnownSymbol s => Type a -> Type b -> (a -> Field s b) -> Op1 a b + -- ^ Projection of a struct field. + -- | Binary operators. data Op2 a b c where -- Boolean operators. @@ -63,6 +77,8 @@ -- Floating operators. Pow :: Floating a => Type a -> Op2 a a a Logb :: Floating a => Type a -> Op2 a a a + -- RealFloat operators. + Atan2 :: RealFloat a => Type a -> Op2 a a a -- Equality operators. Eq :: Eq a => Type a -> Op2 a a Bool Ne :: Eq a => Type a -> Op2 a a Bool @@ -75,10 +91,21 @@ 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. + -- Struct operator. + UpdateField :: (Typeable b, KnownSymbol s, Show b) + => Type a -> Type b -> (a -> Field s b) -> Op2 a b a + -- ^ Update a field of a struct. + -- | 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 + -- Array operator. + UpdateArray :: Type (Array n t) -> Op3 (Array n t) Word32 t (Array n t) + -- ^ Update an element of an array. diff --git a/src/Copilot/Core/PrettyDot.hs b/src/Copilot/Core/PrettyDot.hs deleted file mode 100644 --- a/src/Copilot/Core/PrettyDot.hs +++ /dev/null @@ -1,294 +0,0 @@ --------------------------------------------------------------------------------- --- Copyright © 2011 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - --- | A pretty printer for Copilot specifications. - -{-# LANGUAGE Safe #-} -{-# LANGUAGE GADTs #-} - -module Copilot.Core.PrettyDot - ( prettyPrintDot - , prettyPrintExprDot - ) where - -import Copilot.Core -import Copilot.Core.Type.Show (showWithType, ShowType(..), showType) -import Prelude hiding (id) -import Text.PrettyPrint.HughesPJ -import Data.List (intersperse) -import Text.Printf - -mkExtTmpVar :: String -> String -mkExtTmpVar = ("ext_" ++) - -mkExtTmpTag :: String -> Maybe Tag -> String -mkExtTmpTag name tag = "ext_" ++ name ++ "_" ++ show (tagExtract tag) - -tagExtract :: Maybe Tag -> Tag -tagExtract Nothing = impossible "tagExtract" "copilot-sbv" -tagExtract (Just tag) = tag - --------------------------------------------------------------------------------- - -ppExprDot :: Int -> Int -> Bool -> Expr a -> (Doc,Int) -ppExprDot ii pere bb e0 = case e0 of - Const t x -> (text (printf "%s [label=\"const: %s\",color=red1, style=filled]\n" (show ii::String) ((showWithType Haskell t x)::String) ) - <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)),ii+1) - Drop _ 0 id -> (text (printf "%s [label=\"stream: %s\",color=crimson, style=filled]\n" (show ii::String) (show id::String) ) - <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)),ii+1) - Drop _ i id -> (text (printf "%s [label=\"drop %s: \nstream: %s\",color=crimson, style=filled]\n" (show ii::String) (show i::String) (show id::String) ) - <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)),ii+1) - ExternVar _ name _ -> (if bb then (text (printf "%s [label=\"externV: %s\",color=cyan1, style=filled]\n" (show ii::String) (name::String)) <> text (printf "%s -> %s\n" (show pere::String) (show ii::String))) else (text (printf "%s [label=\"%s\",color=cyan1, style=filled]\n" (show ii::String) (mkExtTmpVar name)) <> text (printf "%s -> %s\n" (show pere::String) (show ii::String))) - ,ii+1) - ExternFun _ name args _ tag -> let (r1, i1) = ppUExprL (ii+1) ii bb args in - (if bb then (text (printf "%s [label=\"externF: %s\",color=cyan4, style=filled]\n" (show ii::String) (name::String)) <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)) - <> (hcat (r1))) else (text (printf "%s [label=\"%s\",color=cyan4, style=filled]\n" (show ii::String) (mkExtTmpTag name tag))<> text (printf "%s -> %s\n" (show pere::String) (show ii::String))) - ,i1) - ExternArray _ _ name - _ idx _ tag -> let (r1,i1) = ppExprDot (ii+1) ii bb idx - in (if bb then (text (printf "%s [label=\"externA: %s\",color=cyan3, style=filled]\n" (show ii::String) (name::String)) <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)) - <> r1) else (text (printf "%s [label=\"%s\",color=cyan3, style=filled]\n" (show ii::String) (mkExtTmpTag name tag)) <> text (printf "%s -> %s\n" (show pere::String) (show ii::String))) - ,i1) - - ExternStruct _ name args _ -> let (r1, i1) = ppUExprL (ii+1) ii bb (map snd $args) in - (text (printf "%s [label=\"externS: %s\",color=dodgerblue2, style=filled]\n" (show ii::String) (name::String)) - <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)) - <> (hcat (r1)),i1) - - GetField _ _ _ name -> (text (printf "%s [label=\"field: %s\",color=dodgerblue3, style=filled]\n" (show ii::String) (name::String) ) - <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)),ii+1) - - Local _ _ name e1 e2 -> let (r1, i1) = ppExprDot (ii+2) (ii+1) bb e1 - in let (r2, i2) = ppExprDot (i1) ii bb e2 - in (text (printf "%s [label=\"local:\",color=blue, style=filled]\n" (show ii::String) ) - <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)) - <> text (printf "%s [label=\"def: %s\",color=blue, style=filled]\n" ((show $ ii+1)::String) (name::String) ) - <> text (printf "%s -> %s\n" (show ii::String) (show $ ii+1::String)) - <> r1 - <> r2 ,i2) - - Var _ name -> (text (printf "%s [label=\"var: %s\",color=blue, style=filled]\n" (show ii::String) (name::String) ) - <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)),ii+1) - - Op1 op e -> let (r1,i1) = ppExprDot (ii+1) ii bb e - in (text (printf "%s [label=\"op1: %s\",color=green4, style=filled]\n" (show ii::String) (ppOp1 op::String)) - <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)) - <> r1,i1) - - Op2 op e1 e2 -> let (r1,i1) = ppExprDot (ii+1) ii bb e1 - in let (r2,i2) = ppExprDot i1 ii bb e2 - in (text (printf "%s [label=\"op2: %s\",color=green4, style=filled]\n" (show ii::String) (ppOp2 op::String)) - <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)) - <> r1 - <> r2 ,i2) - Op3 op e1 e2 e3 -> let (r1,i1) = ppExprDot (ii+1) ii bb e1 - in let (r2,i2) = ppExprDot i1 ii bb e2 - in let (r3,i3) = ppExprDot i2 ii bb e3 - in (text (printf "%s [label=\"op3: %s\",color=green4, style=filled]\n" (show ii::String) (ppOp3 op::String)) - <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)) - <> r1 - <> r2 - <> r3 ,i3) - - Label _ s e -> let (r1,i1) = ppExprDot (ii+1) ii bb e - in (text (printf "%s [label=\"label: %s\",color=plum, style=filled]\n" (show ii::String) (s::String)) - <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)) - <> r1,i1) - -ppUExpr :: Int -> Int -> Bool -> UExpr -> (Doc, Int) -ppUExpr i pere bb UExpr { uExprExpr = e0 } = ppExprDot i pere bb e0 - -ppOp1 :: Op1 a b -> String -ppOp1 op = case op of - Not -> "not" - Abs _ -> "abs" - Sign _ -> "signum" - Recip _ -> "recip" - Exp _ -> "exp" - Sqrt _ -> "sqrt" - Log _ -> "log" - Sin _ -> "sin" - Tan _ -> "tan" - Cos _ -> "cos" - Asin _ -> "asin" - Atan _ -> "atan" - Acos _ -> "acos" - Sinh _ -> "sinh" - Tanh _ -> "tanh" - Cosh _ -> "cosh" - Asinh _ -> "asinh" - Atanh _ -> "atanh" - Acosh _ -> "acosh" - BwNot _ -> "~" - Cast _ _ -> "(cast)" - -ppOp2 :: Op2 a b c -> String -ppOp2 op = case op of - And -> "&&" - Or -> "||" - Add _ -> "+" - Sub _ -> "-" - Mul _ -> "*" - Div _ -> "div" - Mod _ -> "mod" - Fdiv _ -> "/" - Pow _ -> "**" - Logb _ -> "logBase" - Eq _ -> "==" - Ne _ -> "/=" - Le _ -> "<=" - Ge _ -> ">=" - Lt _ -> "<" - Gt _ -> ">" - BwAnd _ -> "&" - BwOr _ -> "|" - BwXor _ -> "^" - BwShiftL _ _ -> "<<" - BwShiftR _ _ -> ">>" - -ppOp3 :: Op3 a b c d -> String -ppOp3 op = case op of - Mux _ -> "mux" - --------------------------------------------------------------------------------- - -ppStream :: Int -> Stream -> (Doc, Int) -ppStream i - Stream - { streamId = id - , streamBuffer = buffer - , streamExpr = e - , streamExprType = t - } - = - (text (printf "%s [label=\"stream: %s\ntype: %s\",color=mediumblue, style=filled]\n" (show i::String) (show id::String) (showType t::String)) - <> text (printf "%s [label=\"++\",color=yellow, style=filled]\n" ((show $ i+1)::String)) - <> text (printf "%s -> %s\n" (show i::String) ((show $ i+1)::String)) - <> text (printf "%s [label=\"[%s]\",color=green, style=filled]\n" ((show $ i+2)::String) ((concat $ intersperse "," $ map (showWithType Haskell t) buffer )) ::String) - <> text (printf "%s -> %s\n" (show (i+1)::String) ((show $ i+2)::String)) - <> r1, i1) - where (r1, i1) = ppExprDot (i+3) (i+1) True e --------------------------------------------------------------------------------- - -ppTrigger :: Int -> Trigger -> (Doc, Int) -ppTrigger i - Trigger - { triggerName = name - , triggerGuard = e - , triggerArgs = args } - = ( text (printf "%s [label=\"trigger: %s\",color=mediumblue, style=filled]\n" (show i::String) (name::String) ) - <> text (printf "%s [label=\"guard\",color=yellow, style=filled]\n" ((show $ i+1)::String)) - <> text (printf "%s -> %s\n" (show i::String) ((show $ i+1)::String)) - <> r1 - <> text (printf "%s [label=\"args\",color=yellow, style=filled]\n" (show i1::String)) - <> text (printf "%s -> %s\n" (show i::String) (show i1::String)) - <> (vcat (r2)) - ,i2) - where - (r1, i1) = ppExprDot (i+2) (i+1) True e - (r2, i2) = ppUExprL (i1+1) (i1) True args - -ppUExprL :: Int -> Int -> Bool -> [UExpr] -> ([Doc], Int) -ppUExprL i _ _ [] = ([], i) - -ppUExprL i pere bb (a:b) = ((r1:r2), i2) - where - (r1, i1) = ppUExpr i pere bb a - (r2, i2) = ppUExprL i1 pere bb b - --------------------------------------------------------------------------------- - -ppObserver :: Int -> Observer -> (Doc, Int) -ppObserver i - Observer - { observerName = name - , observerExpr = e } - = - (text (printf "%s [label=\"observer: \n%s\",color=mediumblue, style=filled]\n" (show i::String) name::String) - <> r1, i1) - where (r1, i1) = ppExprDot (i+1) i True e --------------------------------------------------------------------------------- - -ppProperty :: Int -> Property -> (Doc, Int) -ppProperty i - Property - { propertyName = name - , propertyExpr = e } - = - (text (printf "%s [label=\"property: \n%s\",color=mediumblue, style=filled]\n" (show i::String) name::String) - <> r1, i1) - where (r1, i1) = ppExprDot (i+1) i True e - --------------------------------------------------------------------------------- - - --------------------------------------------------------------------------------- - -ppStreamL :: Int -> [Stream] -> (Doc, Int) -ppStreamL i [] = (empty,i) - -ppStreamL i (a:b) = ((s1$$s2),(i2)) - where - (s1,i1) = ppStream i a - (s2,i2) = ppStreamL i1 b - --------------------------------------------------------------------------------- - -ppTriggerL :: Int -> [Trigger] -> (Doc, Int) -ppTriggerL i [] = (empty,i) - -ppTriggerL i (a:b) = ((s1$$s2),(i2)) - where - (s1,i1) = ppTrigger i a - (s2,i2) = ppTriggerL i1 b - --------------------------------------------------------------------------------- - -ppObserverL :: Int -> [Observer] -> (Doc, Int) -ppObserverL i [] = (empty,i) - -ppObserverL i (a:b) = ((s1$$s2),(i2)) - where - (s1,i1) = ppObserver i a - (s2,i2) = ppObserverL i1 b - - --------------------------------------------------------------------------------- - -ppPropertyL :: Int -> [Property] -> (Doc, Int) -ppPropertyL i [] = (empty,i) - -ppPropertyL i (a:b) = ((s1$$s2),(i2)) - where - (s1,i1) = ppProperty i a - (s2,i2) = ppPropertyL i1 b - --------------------------------------------------------------------------------- - -ppSpecDot :: Int -> Spec -> (Doc, Int) -ppSpecDot i spec = - ((aa $$ cs $$ ds $$ es $$ fs $$ bb),i4) - where - aa = text "digraph G {\nnode [shape=box]\n" - (cs, i1) = ppStreamL i (specStreams spec) - (ds, i2) = ppTriggerL i1 (specTriggers spec) - (es, i3) = ppObserverL i2 (specObservers spec) - (fs, i4) = ppPropertyL i3 (specProperties spec) - bb = text "\n}\n" - --------------------------------------------------------------------------------- - --- | Pretty-prints a Copilot expression. -prettyPrintExprDot :: Bool -> Expr a -> String -prettyPrintExprDot bb s = render rr - where - (r1, _) = ppExprDot 1 0 bb s - rr = text "digraph G {\nnode [shape=box]\n" $$ (text "0 [label=\"file: \n?????\",color=red, style=filled]\n") <> r1 $$ text "\n}\n" - --- | Pretty-prints a Copilot specification. -prettyPrintDot :: Spec -> String -prettyPrintDot s = render r1 - where (r1, _) = ppSpecDot 0 s - --------------------------------------------------------------------------------- diff --git a/src/Copilot/Core/PrettyPrint.hs b/src/Copilot/Core/PrettyPrint.hs deleted file mode 100644 --- a/src/Copilot/Core/PrettyPrint.hs +++ /dev/null @@ -1,196 +0,0 @@ --------------------------------------------------------------------------------- --- Copyright © 2011 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - --- | A pretty printer for Copilot specifications. - -{-# LANGUAGE Safe #-} -{-# LANGUAGE GADTs #-} - -module Copilot.Core.PrettyPrint - ( prettyPrint - , ppExpr - ) where - -import Copilot.Core -import Copilot.Core.Type.Show (showWithType, ShowType(..), showType) -import Prelude hiding (id) -import Text.PrettyPrint.HughesPJ -import Data.List (intersperse) - --------------------------------------------------------------------------------- - -strmName :: Int -> Doc -strmName id = text "s" <> int id - --------------------------------------------------------------------------------- - -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) - ExternFun _ name args _ _ -> - text "Extf_" <> (text name) <> lparen <> - (hcat (punctuate (comma <> space) (map ppUExpr args)) - <> rparen) - ExternArray _ _ name - _ idx _ _ -> text "Exta_" <> (text name) <> lbrack - <> ppExpr idx <> rbrack - ExternStruct _ name args _ -> text "struct" <+> doubleQuotes (text name <> lbrace - <> vcat (punctuate (semi <> space) (map ppSExpr $ args)) <> rbrace) - GetField _ _ _ name -> text "field" <+> doubleQuotes (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) - -ppSExpr :: (Name, UExpr) -> Doc -ppSExpr (_, UExpr { uExprExpr = e0 }) = ppExpr e0 - -ppUExpr :: UExpr -> Doc -ppUExpr UExpr { uExprExpr = e0 } = ppExpr e0 - -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" - BwNot _ -> ppPrefix "~" - Cast _ _ -> ppPrefix "(cast)" - -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" - Eq _ -> ppInfix "==" - Ne _ -> ppInfix "/=" - Le _ -> ppInfix "<=" - Ge _ -> ppInfix ">=" - Lt _ -> ppInfix "<" - Gt _ -> ppInfix ">" - BwAnd _ -> ppInfix "&" - BwOr _ -> ppInfix "|" - BwXor _ -> ppInfix "^" - BwShiftL _ _ -> ppInfix "<<" - BwShiftR _ _ -> ppInfix ">>" - --GetField _ _ -> ppInfix "." - -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 ")" - --------------------------------------------------------------------------------- - -ppInfix :: String -> Doc -> Doc -> Doc -ppInfix cs doc1 doc2 = parens $ doc1 <+> text cs <+> doc2 - -ppPrefix :: String -> Doc -> Doc -ppPrefix cs = (text cs <+>) - --------------------------------------------------------------------------------- - -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 - --------------------------------------------------------------------------------- - -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 - --------------------------------------------------------------------------------- - -ppObserver :: Observer -> Doc -ppObserver - Observer - { observerName = name - , observerExpr = e } - = text "observer \"" <> text name <> text "\"" - <+> text "=" - <+> ppExpr e - --------------------------------------------------------------------------------- - -ppProperty :: Property -> Doc -ppProperty - Property - { propertyName = name - , propertyExpr = e } - = text "property \"" <> text name <> text "\"" - <+> text "=" - <+> ppExpr e - --------------------------------------------------------------------------------- - -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-prints a Copilot specification. -prettyPrint :: Spec -> String -prettyPrint = render . ppSpec - --------------------------------------------------------------------------------- diff --git a/src/Copilot/Core/Random.hs b/src/Copilot/Core/Random.hs deleted file mode 100644 --- a/src/Copilot/Core/Random.hs +++ /dev/null @@ -1,334 +0,0 @@ --------------------------------------------------------------------------------- --- Copyright © 2011 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - --- | Random spec generator. - -{-# LANGUAGE Safe #-} -{-# LANGUAGE GADTs, ExistentialQuantification #-} - -module Copilot.Core.Random - ( randomSpec ) where - -import Copilot.Core -import Copilot.Core.Random.Gen -import Copilot.Core.Random.Weights -import Copilot.Core.Type.Dynamic -import Copilot.Core.Type.Equality ((=~=)) - -import Control.Monad -import Data.List (foldl') -import Prelude hiding (id) -import System.Random (StdGen) -import Control.Monad.Reader - --------------------------------------------------------------------------------- - -randomSpec :: Int -> Weights -> StdGen -> Spec -randomSpec rnds = runGen (genSpec rnds) 0 - --------------------------------------------------------------------------------- - -genSpec :: Int -> Gen Spec -genSpec rnds = do - ws <- weights - numTriggers <- choose (1, maxTriggers ws) - ss <- genStreamInfo's - extVars <- genExtVars - streams <- runReaderT (mapM (genStream ss) ss) extVars - triggers <- - runReaderT (mapM (genTrigger ss) (map mkTriggerName [0..numTriggers-1])) - extVars - return Spec { specStreams = streams - , specObservers = [] - , specTriggers = triggers - , specProperties = [] } - where - mkTriggerName :: Int -> Name - mkTriggerName k = "f" ++ show k - - -- Possibly generate external variables to be shared among streams. - genExtVars :: Gen [DynExtVar] - genExtVars = do - ws <- weights - n <- choose (0, maxExtVars ws) - let lst = [1..n] -- empty list if n == 0 - mapM genExtVar lst - where - genExtVar :: Int -> Gen DynExtVar - genExtVar i = do - ws <- weights - WrapType t <- genType ws - evalExpr <- randomReplicate rnds t - let expr = ExternVar t ("ext" ++ show i) (Just evalExpr) - return $ toDynF t expr - --------------------------------------------------------------------------------- - -data StreamInfo = forall a . (Eq a, Ord a, Typed a) => StreamInfo - { streamInfoId :: Id - , streamInfoType :: Type a - , streamInfoBufferSize :: Int } - --------------------------------------------------------------------------------- - -data WrapType = forall a . (Eq a, Ord a, Typed a) => WrapType (Type a) - -genType :: Weights -> Gen WrapType -genType ws = freq - [ (boolFreq ws, return $ WrapType (typeOf :: Type Bool )) - , (int8Freq ws, return $ WrapType (typeOf :: Type Int8 )) - , (int16Freq ws, return $ WrapType (typeOf :: Type Int16 )) - , (int32Freq ws, return $ WrapType (typeOf :: Type Int32 )) - , (int64Freq ws, return $ WrapType (typeOf :: Type Int64 )) - , (word8Freq ws, return $ WrapType (typeOf :: Type Word8 )) - , (word16Freq ws, return $ WrapType (typeOf :: Type Word16)) - , (word32Freq ws, return $ WrapType (typeOf :: Type Word32)) - , (word64Freq ws, return $ WrapType (typeOf :: Type Word64)) - , (floatFreq ws, return $ WrapType (typeOf :: Type Float )) - , (floatFreq ws, return $ WrapType (typeOf :: Type Double)) ] - -genTypeFromStreamInfo's :: [StreamInfo] -> Gen WrapType -genTypeFromStreamInfo's = elements . map (\(StreamInfo _ t _) -> WrapType t) - --------------------------------------------------------------------------------- - -genStreamInfo's :: Gen [StreamInfo] -genStreamInfo's = do - let s0 = StreamInfo 0 (typeOf :: Type Bool) 1 - ws <- weights - ss <- mapM genStreamInfo [1 .. numStreams ws - 1] - return (s0 : ss) - - where - genStreamInfo :: Int -> Gen StreamInfo - genStreamInfo id = do - ws <- weights - k <- choose (1, maxBuffSize ws) - WrapType t <- genType ws - return - StreamInfo - { streamInfoId = id - , streamInfoType = t - , streamInfoBufferSize = k } - --------------------------------------------------------------------------------- - --- External variables -type DynExtVar = DynamicF Expr Type - -type StreamEnv = ReaderT [DynExtVar] Gen - --------------------------------------------------------------------------------- - -genStream :: [StreamInfo] -> StreamInfo -> StreamEnv Stream -genStream ss - StreamInfo - { streamInfoId = id - , streamInfoType = t - , streamInfoBufferSize = k } - = do - xs <- lift $ replicateM k (randomFromType t) - extVars <- ask - w <- lift $ genExpr extVars ss t - return - Stream - { streamId = id - , streamBuffer = xs - , streamExpr = w - , streamExprType = t } - --------------------------------------------------------------------------------- - -genTrigger :: [StreamInfo] -> Name -> StreamEnv Trigger -genTrigger ss name = do - extVars <- ask - w <- lift $ genExpr extVars ss (typeOf :: Type Bool) - ws <- lift $ weights - i <- lift $ choose (1, maxTrigArgs ws) - args <- replicateM i genArg - return - Trigger - { triggerName = name - , triggerGuard = w - , triggerArgs = args } - - where - genArg :: StreamEnv UExpr - genArg = do - WrapType t <- lift $ genTypeFromStreamInfo's ss - extVars <- ask - w <- lift $ genExpr extVars ss t - return - UExpr - { uExprExpr = w - , uExprType = t } - --------------------------------------------------------------------------------- - -genExpr :: [DynExtVar] -> [StreamInfo] -> Type a -> Gen (Expr a) -genExpr extVars ss t = do - dp <- depth - ws <- weights - if dp >= maxExprDepth ws - then freq (terminalLst ws) - else freq $ - terminalLst ws ++ - [ (op1Freq ws, genOp1) - , (op2Freq ws, genOp2) - , (op3Freq ws, genOp3) ] - - where - terminalLst ws = - (extVarFreq' ws, genExtVar) : [ (constFreq ws, genConst) - , (dropFreq ws, genDrop) ] - - extVarFreq' ws = if null typedExtVars then 0 else extVarFreq ws - - genExtVar = do - let vars = typedExtVars - r <- choose (0, length vars - 1) - return (vars !! r) - - typedExtVars = foldl' typedExtVar [] extVars - where typedExtVar vars dyn = - case fromDynF t dyn of - Nothing -> vars - Just expr -> expr:vars - - genConst = do - x <- randomFromType t - return $ Const t x - - genDrop = do - s <- findStreamInfoWithMatchingType - k <- choose (0, streamInfoBufferSize s - 1) - return $ Drop t (fromIntegral k) (streamInfoId s) - where - findStreamInfoWithMatchingType = - let p (StreamInfo _ t1 _) = case t =~= t1 of - Just _ -> True - _ -> False - in elements (filter p ss) - - genOp3 = incDepth (genOp3Mux extVars ss t) - - genOp1 = incDepth $ case t of - Bool -> genOp1Bool extVars ss - Int8 -> genOp1Num extVars ss t - Int16 -> genOp1Num extVars ss t - Int32 -> genOp1Num extVars ss t - Int64 -> genOp1Num extVars ss t - Word8 -> genOp1Num extVars ss t - Word16 -> genOp1Num extVars ss t - Word32 -> genOp1Num extVars ss t - Word64 -> genOp1Num extVars ss t - Float -> genOp1Num extVars ss t - Double -> genOp1Num extVars ss t - - genOp2 = incDepth $ case t of - Bool -> oneOf [ genOp2Bool extVars ss - , genOp2Eq extVars ss - , genOp2Ord extVars ss - ] - Int8 -> intOrWord NumWit IntegralWit - Int16 -> intOrWord NumWit IntegralWit - Int32 -> intOrWord NumWit IntegralWit - Int64 -> intOrWord NumWit IntegralWit - Word8 -> intOrWord NumWit IntegralWit - Word16 -> intOrWord NumWit IntegralWit - Word32 -> intOrWord NumWit IntegralWit - Word64 -> intOrWord NumWit IntegralWit - Float -> floatOrDouble NumWit - Double -> floatOrDouble NumWit - - where - floatOrDouble numWit = oneOf [ genOp2Num extVars ss t numWit ] - - intOrWord numWit integralWit = do - ws <- weights - if divModFreq ws - then oneOf $ num ++ [ genOp2Integral extVars ss t integralWit ] - else oneOf num - where - num = [ genOp2Num extVars ss t numWit ] - - --------------------------------------------------------------------------------- - -genOp1Bool :: [DynExtVar] -> [StreamInfo] -> Gen (Expr Bool) -genOp1Bool extVars ss = do - ew <- genExpr extVars ss (typeOf :: Type Bool) - return $ Op1 Not ew - -genOp1Num :: Num a => [DynExtVar] -> [StreamInfo] -> Type a -> Gen (Expr a) -genOp1Num extVars ss t = do - ew <- genExpr extVars ss t - opw <- elements [Abs t, Sign t] - return $ Op1 opw ew - -genOp2Bool :: [DynExtVar] -> [StreamInfo] -> Gen (Expr Bool) -genOp2Bool extVars ss = do - ew1 <- genExpr extVars ss (typeOf :: Type Bool) - ew2 <- genExpr extVars ss (typeOf :: Type Bool) - opw <- elements [And, Or] - return $ Op2 opw ew1 ew2 - -genOp2Eq :: [DynExtVar] -> [StreamInfo] -> Gen (Expr Bool) -genOp2Eq extVars ss = do - WrapType t <- genTypeFromStreamInfo's ss - ew1 <- genExpr extVars ss t - ew2 <- genExpr extVars ss t - opw <- elements [Eq t, Ne t] - return $ Op2 opw ew1 ew2 - -genOp2Ord :: [DynExtVar] -> [StreamInfo] -> Gen (Expr Bool) -genOp2Ord extVars ss = - let ss' = findStreamOmittingType Bool in - if (null ss') then genExpr extVars ss Bool - else do - WrapType t <- genTypeFromStreamInfo's ss' - ew1 <- genExpr extVars ss t - ew2 <- genExpr extVars ss t - opw <- elements [ (Lt t) - , (Gt t) - , (Le t) - , (Ge t) ] - return $ Op2 opw ew1 ew2 - where - findStreamOmittingType :: Type a -> [StreamInfo] - findStreamOmittingType t0 = - let p (StreamInfo _ t1 _) = case t0 =~= t1 of - Just _ -> True - _ -> False - in filter (not . p) ss - -genOp2Num :: [DynExtVar] -> [StreamInfo] -> Type a -> NumWit a -> Gen (Expr a) -genOp2Num extVars ss t NumWit = do - ew1 <- genExpr extVars ss t - ew2 <- genExpr extVars ss t - opw <- elements [ (Add t) - , (Sub t) - , (Mul t) ] - return $ Op2 opw ew1 ew2 - -genOp2Integral :: - [DynExtVar] -> [StreamInfo] -> Type a -> IntegralWit a -> Gen (Expr a) -genOp2Integral extVars ss t IntegralWit = do - ew1 <- genExpr extVars ss t - ew2 <- genExpr extVars ss t - opw <- elements [ (Div t) - , (Mod t) ] - return $ Op2 opw ew1 ew2 - -genOp3Mux :: [DynExtVar] -> [StreamInfo] -> Type a -> Gen (Expr a) -genOp3Mux extVars ss t = do - ew1 <- genExpr extVars ss (typeOf :: Type Bool) - ew2 <- genExpr extVars ss t - ew3 <- genExpr extVars ss t - return $ Op3 (Mux t) ew1 ew2 ew3 - -data NumWit a = Num a => NumWit - -data IntegralWit a = Integral a => IntegralWit - diff --git a/src/Copilot/Core/Random/Gen.hs b/src/Copilot/Core/Random/Gen.hs deleted file mode 100644 --- a/src/Copilot/Core/Random/Gen.hs +++ /dev/null @@ -1,136 +0,0 @@ --------------------------------------------------------------------------------- --- Copyright © 2011 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - -{-# LANGUAGE Safe #-} -{-# LANGUAGE GADTs, ExistentialQuantification #-} - -module Copilot.Core.Random.Gen - ( Gen - , runGen - , randomFromType - , oneOf - , freq - , choose - , elements - , depth - , weights - , incDepth - , randomReplicate - ) where - -import Copilot.Core.Random.Weights -import Copilot.Core.Error -import Copilot.Core.Type - -import Control.Applicative -import Control.Monad -import System.Random (StdGen, Random, random, randomR, split) - --------------------------------------------------------------------------------- - --- | @runGen@ takes a @Gen a@, a max depth of the expression, the weights, and --- the standard random generator. -newtype Gen a = MkGen { runGen :: Depth -> Weights -> StdGen -> a } - -instance Functor Gen where - fmap f (MkGen h) = MkGen (\ d ws r -> f (h d ws r)) - -instance Applicative Gen where - pure = return - (<*>) = ap - -instance Monad Gen where - return x = MkGen (\ _ _ _ -> x) - MkGen m >>= k = MkGen $ \ d ws r -> - let (r1, r2) = split r in - let MkGen m' = k (m d ws r1) in - m' d ws r2 - --------------------------------------------------------------------------------- - -stdGen :: Gen StdGen -stdGen = MkGen $ \ _ _ g -> g - -depth :: Gen Depth -depth = MkGen $ \ d _ _ -> d - -weights :: Gen Weights -weights = MkGen $ \ _ ws _ -> ws - -incDepth :: Gen a -> Gen a -incDepth gen = MkGen $ \ d ws g -> runGen gen (succ d) ws g - --------------------------------------------------------------------------------- - -randomFromType :: Type a -> Gen a -randomFromType t = - case t of - Bool -> genBool - Int8 -> genBoundedIntegral - Int16 -> genBoundedIntegral - Int32 -> genBoundedIntegral - Int64 -> genBoundedIntegral - Word8 -> genBoundedIntegral - Word16 -> genBoundedIntegral - Word32 -> genBoundedIntegral - Word64 -> genBoundedIntegral - Float -> genFractional - Double -> genFractional - - where - - genBool :: Gen Bool - genBool = do - g <- stdGen - return $ fst (random g) - - genBoundedIntegral :: (Bounded a, Integral a) => Gen a - genBoundedIntegral = do - let mn = minBound - mx = maxBound `asTypeOf` mn - n <- choose (toInteger mn, toInteger mx) - return (fromInteger n `asTypeOf` mn) - - genFractional :: Random a => Gen a - genFractional = do - g <- stdGen - return $ fst (random g) - --------------------------------------------------------------------------------- - --- Given an int i and type t, make a list of length i containing random values --- over the type. -randomReplicate :: Int -> Type a -> Gen [a] -randomReplicate i t = mapM (\_ -> randomFromType t) [1..i] - --------------------------------------------------------------------------------- - -choose :: Random a => (a, a) -> Gen a -choose rng = do - g <- stdGen - return $ fst (randomR rng g) - -oneOf :: [Gen a] -> Gen a -oneOf [] = impossible "oneof" "copilot-core" -oneOf gs = choose (0,length gs - 1) >>= (gs !!) - --- | Takes a list of pairs (weight, Gen), and choose the Gen based on the --- weights. To get the frequency of choosing a Gen, sum up all the weights, and --- choose c between 1 and the total. Now recurse down the list, choosing an --- item only when c <= weight. If not, subtract the current weight from c. -freq :: [(Int, Gen a)] -> Gen a -freq [] = impossible "feq" "copilot-core" -freq xs0 = choose (1, tot) >>= (`pick` xs0) - where - tot = sum (map fst xs0) - pick n ((k,x):xs) - | n <= k = x - | otherwise = pick (n-k) xs - pick _ _ = impossible "pick" "copilot-core" - -elements :: [a] -> Gen a -elements [] = impossible "elements" "copilot-core" -elements xs = (xs !!) `fmap` choose (0, length xs - 1) - --------------------------------------------------------------------------------- diff --git a/src/Copilot/Core/Random/Weights.hs b/src/Copilot/Core/Random/Weights.hs deleted file mode 100644 --- a/src/Copilot/Core/Random/Weights.hs +++ /dev/null @@ -1,75 +0,0 @@ --------------------------------------------------------------------------------- --- Copyright © 2011 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - -{-# LANGUAGE Safe #-} - -module Copilot.Core.Random.Weights - ( Depth - , Weights (..) - , simpleWeights ) where - -type Depth = Int - -data Weights = Weights - { maxExprDepth :: Int - , maxBuffSize :: Int - , maxTriggers :: Int - , maxTrigArgs :: Int - , maxExtVars :: Int - , maxObservers :: Int - , numStreams :: Int - -- Expression frequencies: - , constFreq :: Int - , extVarFreq :: Int - , drop0Freq :: Int - , dropFreq :: Int - , externFreq :: Int - , op1Freq :: Int - , op2Freq :: Int - , op3Freq :: Int - -- Type frequencies: - , boolFreq :: Int - , int8Freq :: Int - , int16Freq :: Int - , int32Freq :: Int - , int64Freq :: Int - , word8Freq :: Int - , word16Freq :: Int - , word32Freq :: Int - , word64Freq :: Int - , floatFreq :: Int - , doubleFreq :: Int - , divModFreq :: Bool } - -simpleWeights :: Weights -simpleWeights = Weights - { maxExprDepth = 10 - , maxBuffSize = 8 - , maxTriggers = 5 - , maxTrigArgs = 5 - , maxExtVars = 5 - , maxObservers = 8 - , numStreams = 10 - -- Expression frequencies: - , constFreq = 1 - , extVarFreq = 1 - , drop0Freq = 1 - , dropFreq = 1 - , externFreq = 1 - , op1Freq = 1 - , op2Freq = 1 - , op3Freq = 1 - -- Type frequencies: - , boolFreq = 1 - , int8Freq = 1 - , int16Freq = 1 - , int32Freq = 1 - , int64Freq = 1 - , word8Freq = 1 - , word16Freq = 1 - , word32Freq = 1 - , word64Freq = 1 - , floatFreq = 1 - , doubleFreq = 1 - , divModFreq = True } diff --git a/src/Copilot/Core/Spec.hs b/src/Copilot/Core/Spec.hs --- a/src/Copilot/Core/Spec.hs +++ b/src/Copilot/Core/Spec.hs @@ -1,70 +1,94 @@ --------------------------------------------------------------------------------- --- Copyright © 2011 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - -{-# LANGUAGE Safe #-} -{-# LANGUAGE ExistentialQuantification, GADTs #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE Safe #-} +-- | +-- 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. +-- +-- In order to be executed, high-level Copilot Language Spec must be turned +-- 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 (..) - , StructData (..) - ) where - -import Copilot.Core.Expr (Name, Id, Expr, UExpr) -import Copilot.Core.Type (Type, Typed) + ( Stream (..) + , Observer (..) + , Trigger (..) + , Spec (..) + , Property (..) + , Prop (..) + , extractProp + ) + where --------------------------------------------------------------------------------- +-- External imports +import Data.Typeable (Typeable) --- | A stream. -data Stream = forall a. Typed a => Stream - { streamId :: Id - , streamBuffer :: [a] - , streamExpr :: Expr a - , streamExprType :: Type a } +-- 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 + } --- | An observer. -data Observer = forall a. Observer +-- | An observer, representing a stream that we observe during interpretation +-- at every sample. +data Observer = forall a . Typeable a => Observer { observerName :: Name , observerExpr :: Expr a - , observerExprType :: Type a } - --------------------------------------------------------------------------------- + , observerExprType :: Type a + } --- | A trigger. +-- | 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. +-- | A property, representing a boolean stream that is existentially or +-- universally quantified over time. data Property = Property - { propertyName :: Name - , propertyExpr :: Expr Bool } - --------------------------------------------------------------------------------- + { propertyName :: Name + , propertyProp :: Prop + } --- | Struct representation as a bit array. -data StructData = StructData - { structName :: Name - , structFields :: [(Name, UExpr)] } +-- | A proposition, representing a boolean stream that is existentially or +-- universally quantified over time. +data Prop + = Forall (Expr Bool) + | Exists (Expr Bool) --------------------------------------------------------------------------------- +-- | Extract the underlying stream from a quantified proposition. +-- +-- Think carefully before using this function, as this function will remove the +-- quantifier from a proposition. Universally quantified streams usually require +-- separate treatment from existentially quantified ones, so carelessly using +-- this function to remove quantifiers can result in hard-to-spot soundness +-- bugs. +extractProp :: Prop -> Expr Bool +extractProp (Forall e) = e +extractProp (Exists e) = e --- | A Copilot specification consists of a list of variables bound to anonymous --- streams, a list of anomymous streams, a list of observers, a list of --- triggers, and a list of structs. +-- | 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] + } diff --git a/src/Copilot/Core/Type.hs b/src/Copilot/Core/Type.hs --- a/src/Copilot/Core/Type.hs +++ b/src/Copilot/Core/Type.hs @@ -1,110 +1,455 @@ --------------------------------------------------------------------------------- --- Copyright © 2011 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE Trustworthy #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +-- | +-- 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 (..) + , typeOfDefault + , UType (..) + , SimpleType (..) --- | Typing for Core. + , typeSize + , typeLength -{-# LANGUAGE Safe #-} -{-# LANGUAGE ExistentialQuantification, GADTs, KindSignatures #-} + , Value (..) + , toValues + , toValuesDefault + , Field (..) + , typeName + , typeNameDefault -module Copilot.Core.Type - ( Type (..) - , Typed (..) - , UType (..) - , SimpleType(..) - ) where + , Struct + , fieldName + , accessorName + , updateField + , updateFieldDefault + ) + where -import Data.Int -import Data.Word -import Copilot.Core.Type.Equality +-- External imports +import Data.Char (isLower, isUpper, toLower) +import Data.Coerce (coerce) +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, eqT, typeRep) +import Data.Word (Word16, Word32, Word64, Word8) +import GHC.Generics (Datatype (..), D1, Generic (..), K1 (..), M1 (..), + U1 (..), (:*:) (..)) +import GHC.TypeLits (KnownNat, KnownSymbol, Symbol, natVal, sameNat, + sameSymbol, symbolVal) +-- Internal imports +import Copilot.Core.Type.Array (Array) + +-- | The value of that is a product or struct, defined as a constructor with +-- several fields. +class Struct a where + -- | Returns the name of struct in the target language. + typeName :: a -> String + + -- | Transforms all the struct's fields into a list of values. + toValues :: a -> [Value a] + + -- | Update the value of a struct field. This is only used by the Copilot + -- interpreter. + -- + -- If you do not plan to use the interpreter, you can omit an implementation + -- of this method. If you do so, it is recommended that you derive a 'Generic' + -- instance for the struct data type. This is because in a future release, the + -- default implementation of 'updateField' (which will be picked if there is + -- not a manually written implementation) will be changed to require a + -- 'Generic' instance. + -- + -- In order to implement 'updateField', pick one of the following approaches: + -- + -- * Derive a 'Generic' instance for the struct data type and then define + -- @'updateField' = 'updateFieldDefault'@ in the 'Struct' instance. + -- + -- * Manually implement 'updateField' by doing the following for each 'Field' + -- in a struct: + -- + -- 1. Check that the name of the 'Field' matches the name of the supplied + -- 'Value' (using 'GHC.TypeLits.sameSymbol'). + -- + -- 2. Check that the type of the 'Field' matches the 'Type' of the supplied + -- 'Value' (using 'DE.testEquality'). + -- + -- 3. If both (1) and (2) succeed, update the corresponding struct field + -- using a record update. + -- + -- For a complete end-to-end example that demonstrates how to manually + -- implement 'updateField' and use it in the Copilot interpreter, see the + -- @examples/StructsUpdateField.hs@ example in the @copilot@ library. + updateField :: a -> Value t -> a + updateField = error $ unlines + [ "Field updates not supported for this type." + , "(Perhaps you need to implement 'updateField' for a 'Struct' instance?)" + ] + +-- | 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) + +-- | 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 _ = 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 _ = symbolVal (Proxy :: Proxy s) + +instance (KnownSymbol s, Show t) => Show (Field s t) where + show f@(Field v) = fieldName f ++ ":" ++ show v + +instance {-# OVERLAPPABLE #-} (Typed t, Struct t) => Show t where + show t = "<" ++ fields ++ ">" + where + fields = intercalate "," $ map showfield (toValues t) + showfield (Value _ field) = show field + +-- | A Type representing the types of expressions or values handled by +-- Copilot Core. +-- +-- Note that both arrays and structs use dependently typed features. In the +-- 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 + 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 +deriving instance Show (Type a) -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 - (=~=) _ _ = Nothing +-- | Return the length of an array from its type +typeLength :: forall n t . KnownNat n => Type (Array n t) -> Int +typeLength _ = fromIntegral $ natVal (Proxy :: Proxy n) --------------------------------------------------------------------------------- +-- | Return the total (nested) size of an array from its type +typeSize :: forall n t . KnownNat n => Type (Array n t) -> Int +typeSize ty@(Array ty'@(Array _)) = typeLength ty * typeSize ty' +typeSize ty@(Array _ ) = typeLength ty -data SimpleType = SBool - | SInt8 - | SInt16 - | SInt32 - | SInt64 - | SWord8 - | SWord16 - | SWord32 - | SWord64 - | SFloat - | SDouble - deriving Eq +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 (Array t1) (Array t2) = + testArrayEquality t1 t2 + where + testArrayEquality :: forall n1 a1 n2 a2. + (KnownNat n1, KnownNat n2) + => Type a1 + -> Type a2 + -> Maybe (Array n1 a1 :~: Array n2 a2) + testArrayEquality ty1 ty2 + | Just DE.Refl <- sameNat (Proxy :: Proxy n1) (Proxy :: Proxy n2) + , Just DE.Refl <- testEquality ty1 ty2 + = Just DE.Refl + | otherwise + = Nothing + testEquality (Struct _) (Struct _) = eqT + testEquality _ _ = Nothing --------------------------------------------------------------------------------- +-- | A simple, monomorphic representation of types that facilitates putting +-- variables in heterogeneous lists and environments in spite of their types +-- being different. +data SimpleType where + SBool :: SimpleType + SInt8 :: SimpleType + SInt16 :: SimpleType + SInt32 :: SimpleType + SInt64 :: SimpleType + SWord8 :: SimpleType + SWord16 :: SimpleType + SWord32 :: SimpleType + SWord64 :: SimpleType + SFloat :: SimpleType + SDouble :: SimpleType + SArray :: Type t -> SimpleType + SStruct :: SimpleType -class Typed a where - typeOf :: Type a - simpleType :: Type a -> SimpleType +-- | 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 DE.Refl <- testEquality t1 t2 = True + | otherwise = False + SStruct == SStruct = True + _ == _ = False -instance Typed Bool where +-- | A typed expression, from which we can obtain the two type representations +-- used by Copilot: 'Type' and 'SimpleType'. +class (Show a, Typeable a) => Typed a where + typeOf :: Type a + simpleType :: Type a -> SimpleType + simpleType _ = SStruct + +instance Typed Bool where typeOf = Bool simpleType _ = SBool -instance Typed Int8 where + +instance Typed Int8 where typeOf = Int8 - simpleType _ = SBool -instance Typed Int16 where + simpleType _ = SInt8 + +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 -- | A untyped type (no phantom type). -data UType = forall a . UType { uTypeType :: Type a } +data UType = forall a . Typeable a => UType (Type a) --------------------------------------------------------------------------------- +instance Eq UType where + UType ty1 == UType ty2 = typeRep ty1 == typeRep ty2 + +-- * GHC.Generics-based defaults + +-- | A default implementation of 'typeName' that leverages 'Generic'. In order +-- to use this, make sure you derive a 'Generic' instance for your data type and +-- then define @'typeName' = 'typeNameDefault'@ in its 'Struct' instance. +-- +-- This generates a struct name that consists of the name of the original +-- Haskell data type, but converted to snake_case. +typeNameDefault :: (Generic a, GDatatype (Rep a)) => a -> String +typeNameDefault = convert . gTypeName . from + where + convert :: String -> String + convert = convert' True True + + convert' :: Bool -- ^ Is this the first letter + -> Bool -- ^ Was the previous letter capital + -> String -- ^ Remainder of the string + -> String + convert' _ _ [] = [] + convert' _ v [x] + | v && isUpper x = toLower x : [] + | isUpper x = '_' : toLower x : [] + | otherwise = x : [] + convert' b v (x1:x2:xs) + | not b && isUpper x1 && (isLower x2 || not v) + = '_' : toLower x1 : convert' False (isUpper x1) (x2:xs) + | otherwise + = toLower x1 : convert' False (isUpper x1) (x2:xs) + +-- | A default implementation of 'toValues' that leverages 'Generic'. In order +-- to use this, make sure you derive a 'Generic' instance for your data type and +-- then define @'toValues' = 'toValuesDefault'@ in its 'Struct' instance. +toValuesDefault :: (Generic a, GStruct (Rep a)) => a -> [Value a] +toValuesDefault x = coerce $ gToValues $ from x + +-- | A default implementation of 'updateField' that leverages 'Generic'. In +-- order to use this, make sure you derive a 'Generic' instance for your data +-- type and then define @'updateField' = 'updateFieldDefault'@ in its 'Struct' +-- instance. +updateFieldDefault :: (Generic a, GStruct (Rep a)) => a -> Value t -> a +updateFieldDefault a v@(Value _ field) + | updated = to a' + | otherwise = error $ "Unexpected field: " ++ show field + where + (a', updated) = gUpdateField (from a) v + +-- | A default implementation of 'typeOf' that leverages 'Generic'. In order to +-- use this, make sure you derive a 'Generic' instance for your data type and +-- then define @'typeOf' = 'typeOfDefault'@ in its 'Typed' instance. +typeOfDefault :: + forall a. (Typed a, Struct a, Generic a, GTypedStruct (Rep a)) => Type a +typeOfDefault = Struct $ to $ gStructPlaceholder @(Rep a) @() + +-- ** Generic-based classes (not exported) + +-- | Capture the name of a Haskell data type from its 'Generic' metadata. +class GDatatype f where + -- | Returns the name of a Haskell data type. (Note that this differs from + -- 'typeName', which is expected to return the name of the struct in the + -- /target/ language). + gTypeName :: f p -> String + +-- | The only 'GDatatype' instance we need is for 'D1', which describes +-- 'Datatype' metadata (@d@). We ignore all other metadata (@_f@). +instance Datatype d => GDatatype (D1 d _f) where + gTypeName = datatypeName + +-- | Perform struct-related operations on 'Generic' representation types. +class GStruct f where + -- | Transforms all the struct representation's fields into a list of values. + gToValues :: f p -> [Value (f p)] + + -- | Update the value of a struct representation's field. This returns two + -- things: + -- + -- 1. @f p@: The struct representation, but with the field updated. + -- + -- 2. 'Bool': This is 'True' if the field was successfully updated and 'False' + -- otherwise. If this returns 'False', it is the responsibility of the + -- caller to raise an error. + gUpdateField :: f p -> Value t -> (f p, Bool) + +-- | 'U1' represents a data constructor with no fields. As such, 'gToValues' +-- returns an empty list of 'Value's, and 'gUpdateField' does not update +-- anything. +instance GStruct U1 where + gToValues U1 = [] + gUpdateField u _ = (u, False) + +-- | 'M1' is only used to store metadata, which the 'GStruct' class does not +-- make use of. As such, this instance discards the metadata and recurses. +instance GStruct f => GStruct (M1 _i _c f) where + gToValues (M1 x) = coerce (gToValues x) + gUpdateField (M1 x) v = (M1 x', updated) + where + (x', updated) = gUpdateField x v + +-- | @(':*:')@ represents a data constructor with multiple fields. +instance (GStruct f, GStruct g) => GStruct (f :*: g) where + -- Recursively compute two lists of Values and append them. + gToValues (f :*: g) = coerce (gToValues f) ++ coerce (gToValues g) + -- Recursively attempt to update the field in both branches and combine the + -- updated branches. We will have successfully updated the field if either + -- branch was successfully updated. + gUpdateField (f :*: g) v = (f' :*: g', updatedF || updatedG) + where + (f', updatedF) = gUpdateField f v + (g', updatedG) = gUpdateField g v + +-- | 'K1' represents a single field in a data constructor. This is the base +-- case. +instance (KnownSymbol name, Typed ty, c ~ Field name ty) => + GStruct (K1 _i c) where + -- Now that we have the field, return it in a singleton list. + gToValues (K1 field) = [Value typeOf field] + -- In order to update the field, we check that the field names and types + -- match. If they do, return the updated field and declare the update as + -- successful. Otherwise, return the old field and declare the update as + -- unsuccessful. + gUpdateField (K1 oldField) (Value newTy (newField :: Field newName newTy)) = + case (sameSymbol pName pNewName, testEquality ty newTy) of + (Just Refl, Just Refl) -> (K1 newField, True) + _ -> (K1 oldField, False) + where + pName = Proxy @name + pNewName = Proxy @newName + ty = typeOf @ty + +-- | Compute a 'Generic' placeholder value to use for a struct type. +class GTypedStruct f where + -- | A placeholder value to supply to use in a generic implementation of + -- 'typeOf' for a struct type. + gStructPlaceholder :: f p + +-- | 'U1' represents a data constructor with no fields. As such, +-- 'gStructPlaceholder' simply returns the data constructor with no other +-- information. +instance GTypedStruct U1 where + gStructPlaceholder = U1 + +-- | 'M1' is only used to store metadata, which the 'GTypedStruct' class does +-- not make use of. As such, this instance recursively computes a placeholder +-- value without inspecting the metadata. +instance GTypedStruct f => GTypedStruct (M1 _i _c f) where + gStructPlaceholder = M1 gStructPlaceholder + +-- | @(':*:')@ represents a data constructor with multiple fields. As such, +-- 'gStructPlaceholder' recursively computes placeholders for each field and +-- combines them into the overall data constructor. +instance (GTypedStruct f, GTypedStruct g) => GTypedStruct (f :*: g) where + gStructPlaceholder = gStructPlaceholder :*: gStructPlaceholder + +-- | 'K1' represents a single field in a data constructor. This is the base +-- case. This instance computes a placeholder value that works for any field of +-- any type. +instance (c ~ Field name ty) => GTypedStruct (K1 _i c) where + -- We use 'undefined' as the actual value for the 'Field' because Copilot + -- never inspects the value. + gStructPlaceholder = K1 $ Field undefined diff --git a/src/Copilot/Core/Type/Array.hs b/src/Copilot/Core/Type/Array.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Core/Type/Array.hs @@ -0,0 +1,64 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE Safe #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} + +-- | +-- 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 + , arrayElems + , arrayUpdate + ) + where + +-- External imports +import Data.Proxy (Proxy (..)) +import GHC.TypeLits (KnownNat, Nat, natVal, type(-)) + +-- | Implementation of an array that uses type literals to store length. +data Array (n :: Nat) t where + Array :: [t] -> Array n t + +instance Show t => Show (Array n t) where + show (Array xs) = show xs + +-- | Smart array constructor that only type checks if the length of the given +-- list matches the length of the array at type level. +array :: forall n t. KnownNat n => [t] -> Array n t +array xs | datalen == typelen = Array xs + | otherwise = error errmsg + where + datalen = length xs + typelen = fromIntegral $ natVal (Proxy :: Proxy n) + errmsg = "Length of data (" ++ show datalen ++ + ") does not match length of type (" ++ show typelen ++ ")." + +-- | Return the elements of an array. +arrayElems :: Array n a -> [a] +arrayElems (Array xs) = xs + +-- | Update element of array to given element. +-- +-- PRE: the second argument denotes a valid index in the array. +arrayUpdate :: Array n a -> Int -> a -> Array n a +arrayUpdate (Array []) _ _ = error errMsg + where + errMsg = "copilot-core: arrayUpdate: Attempt to update empty array" + +arrayUpdate (Array (x:xs)) 0 y = Array (y:xs) + +arrayUpdate (Array (x:xs)) n y = + arrayAppend x (arrayUpdate (Array xs) (n - 1) y) + where + -- | Append to an array while preserving length information at the type + -- level. + arrayAppend :: a -> Array (n - 1) a -> Array n a + arrayAppend x (Array xs) = Array (x:xs) diff --git a/src/Copilot/Core/Type/Dynamic.hs b/src/Copilot/Core/Type/Dynamic.hs deleted file mode 100644 --- a/src/Copilot/Core/Type/Dynamic.hs +++ /dev/null @@ -1,53 +0,0 @@ --------------------------------------------------------------------------------- --- Copyright © 2011 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - -{-# LANGUAGE Safe #-} -{-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE Rank2Types #-} - --- | An implementation of dynamic types using "Copilot.Core.Type.Equality". --- The theory behind this technique is described the following paper: --- --- * Baars, Arthur I. and Swierstra, S. Doaitse, --- \"/Typing dynamic typing/\", --- ACM SIGPLAN Notices vol. 37, p. 157-166, 2002 - -{-# LANGUAGE GADTs, KindSignatures, ScopedTypeVariables #-} - -module Copilot.Core.Type.Dynamic - ( Dynamic (..) - , DynamicF (..) - , toDyn - , fromDyn - , toDynF - , fromDynF - ) where - -import Copilot.Core.Type.Equality - --------------------------------------------------------------------------------- - -data Dynamic :: (* -> *) -> * where - Dynamic :: a -> t a -> Dynamic t - -data DynamicF :: (* -> *) -> (* -> *) -> * where - DynamicF :: f a -> t a -> DynamicF f t - -toDyn :: t a -> a -> Dynamic t -toDyn t x = Dynamic x t - -fromDyn :: EqualType t => t a -> Dynamic t -> Maybe a -fromDyn t1 (Dynamic x t2) = - case t1 =~= t2 of - Just Refl -> return x - Nothing -> Nothing - -toDynF :: t a -> f a -> DynamicF f t -toDynF t fx = DynamicF fx t - -fromDynF :: EqualType t => t a -> DynamicF f t -> Maybe (f a) -fromDynF t1 (DynamicF fx t2) = - case t1 =~= t2 of - Just Refl -> return fx - Nothing -> Nothing diff --git a/src/Copilot/Core/Type/Eq.hs b/src/Copilot/Core/Type/Eq.hs deleted file mode 100644 --- a/src/Copilot/Core/Type/Eq.hs +++ /dev/null @@ -1,78 +0,0 @@ --------------------------------------------------------------------------------- --- Copyright © 2011 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - -{-# LANGUAGE Safe #-} -{-# LANGUAGE ExistentialQuantification, GADTs #-} - -module Copilot.Core.Type.Eq - ( EqWit (..) - , eqWit - , UVal (..) - ) where - -import Copilot.Core.Error (impossible) -import Copilot.Core.Type -import Copilot.Core.Type.Dynamic (fromDyn, toDyn) - --------------------------------------------------------------------------------- - -data EqWit a = Eq a => EqWit - --------------------------------------------------------------------------------- - -eqWit :: Type a -> EqWit a -eqWit t = - case t of - Bool -> EqWit - Int8 -> EqWit - Int16 -> EqWit - Int32 -> EqWit - Int64 -> EqWit - Word8 -> EqWit - Word16 -> EqWit - Word32 -> EqWit - Word64 -> EqWit - Float -> EqWit - Double -> EqWit - --------------------------------------------------------------------------------- - -data UVal = forall a. UVal - { uType :: Type a - , uVal :: a - } - --------------------------------------------------------------------------------- - -instance Eq UVal where - (==) UVal { uType = t1 - , uVal = a } - UVal { uType = t2 - , uVal = b } - = case eqWit t1 of - EqWit -> - case eqWit t2 of - EqWit -> - let dyn1 = toDyn t1 a in - case fromDyn t2 dyn1 of - Nothing -> False - Just x -> - case t1 of - -- Hacks for QuickChecking between C and Haskell - Float -> case t2 of - Float -> approx floatErr x b - _ -> impossible "instance Eq UVal" - "copilot-core" - Double -> case t2 of - Double -> approx doubleErr x b - _ -> impossible "instance Eq UVal" - "copilot-core" - _ -> x == b - where - approx :: (Num a, Ord a) => a -> a -> a -> Bool - approx err x y = x - y < err && y - x < err - floatErr = 0.0001 :: Float - doubleErr = 0.0001 :: Double - --------------------------------------------------------------------------------- diff --git a/src/Copilot/Core/Type/Equality.hs b/src/Copilot/Core/Type/Equality.hs deleted file mode 100644 --- a/src/Copilot/Core/Type/Equality.hs +++ /dev/null @@ -1,37 +0,0 @@ --------------------------------------------------------------------------------- --- Copyright © 2011 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - -{-# LANGUAGE Safe #-} -{-# LANGUAGE GADTs, KindSignatures #-} - -module Copilot.Core.Type.Equality - ( Equal (..) - , EqualType (..) - , coerce - , refl - , trans - , symm - , cong - ) where - -data Equal :: * -> * -> * where - Refl :: Equal a a - -class EqualType t where - (=~=) :: t a -> t b -> Maybe (Equal a b) - -coerce :: Equal a b -> a -> b -coerce Refl x = x - -refl :: Equal a a -refl = Refl - -symm :: Equal a b -> Equal b a -symm Refl = Refl - -trans :: Equal a b -> Equal b c -> Equal a c -trans Refl Refl = Refl - -cong :: Equal a b -> Equal (f a) (f b) -cong Refl = Refl diff --git a/src/Copilot/Core/Type/Read.hs b/src/Copilot/Core/Type/Read.hs deleted file mode 100644 --- a/src/Copilot/Core/Type/Read.hs +++ /dev/null @@ -1,52 +0,0 @@ --------------------------------------------------------------------------------- --- Copyright © 2011 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - -{-# LANGUAGE Safe #-} -{-# LANGUAGE ExistentialQuantification, GADTs #-} - -module Copilot.Core.Type.Read - ( ReadWit (..) - , readWit - , readWithType - ) where - -import Copilot.Core.Type -import Copilot.Core.Error (badUsage) - --------------------------------------------------------------------------------- - -data ReadWit a = Read a => ReadWit - --------------------------------------------------------------------------------- - -readWit :: Type a -> ReadWit a -readWit t = - case t of - Bool -> ReadWit - Int8 -> ReadWit - Int16 -> ReadWit - Int32 -> ReadWit - Int64 -> ReadWit - Word8 -> ReadWit - Word16 -> ReadWit - Word32 -> ReadWit - Word64 -> ReadWit - Float -> ReadWit - Double -> ReadWit - --------------------------------------------------------------------------------- - -readWithType :: Type a -> String -> a -readWithType t str = - case t of - Bool -> case str of - "0" -> False - "1" -> True - x -> badUsage $ "in readWithType in copilot-core: expecting a \"0\" or \"1\" when reading a Boolean value " ++ show x ++ "." - _ -> rd - where - rd = case readWit t of - ReadWit -> read str - --------------------------------------------------------------------------------- diff --git a/src/Copilot/Core/Type/Show.hs b/src/Copilot/Core/Type/Show.hs deleted file mode 100644 --- a/src/Copilot/Core/Type/Show.hs +++ /dev/null @@ -1,77 +0,0 @@ --------------------------------------------------------------------------------- --- Copyright © 2011 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - -{-# LANGUAGE Safe #-} -{-# LANGUAGE ExistentialQuantification, GADTs #-} - -module Copilot.Core.Type.Show - ( ShowWit (..) - , showWit - , showWithType - , ShowType(..) - , showType - ) where - -import Copilot.Core.Type - --------------------------------------------------------------------------------- - -data ShowWit a = Show a => ShowWit - --------------------------------------------------------------------------------- - -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 - --------------------------------------------------------------------------------- - -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" - --------------------------------------------------------------------------------- - --- Are we proving equivalence with a C backend, in which case we want to show --- Booleans as '0' and '1'. -data ShowType = C | Haskell - --------------------------------------------------------------------------------- - -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 - --------------------------------------------------------------------------------- diff --git a/src/Copilot/Core/Type/Uninitialized.hs b/src/Copilot/Core/Type/Uninitialized.hs deleted file mode 100644 --- a/src/Copilot/Core/Type/Uninitialized.hs +++ /dev/null @@ -1,31 +0,0 @@ --------------------------------------------------------------------------------- --- Copyright © 2011 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - --- | Initial values for give types. - -{-# LANGUAGE Safe #-} -{-# LANGUAGE GADTs #-} - -module Copilot.Core.Type.Uninitialized - ( uninitialized - ) where - -import Copilot.Core.Type - --------------------------------------------------------------------------------- - -uninitialized :: Type a -> a -uninitialized t = - case t of - Bool -> False - Int8 -> 0 - Int16 -> 0 - Int32 -> 0 - Int64 -> 0 - Word8 -> 0 - Word16 -> 0 - Word32 -> 0 - Word64 -> 0 - Float -> 0 - Double -> 0 diff --git a/tests/Main.hs b/tests/Main.hs new file mode 100644 --- /dev/null +++ b/tests/Main.hs @@ -0,0 +1,20 @@ +-- | Test copilot-core. +module Main where + +-- External imports +import Test.Framework (Test, defaultMain) + +-- Internal library modules being tested +import qualified Test.Copilot.Core.Type +import qualified Test.Copilot.Core.Type.Array + +-- | Run all unit tests on copilot-core. +main :: IO () +main = defaultMain tests + +-- | All unit tests in copilot-core. +tests :: [Test.Framework.Test] +tests = + [ Test.Copilot.Core.Type.tests + , Test.Copilot.Core.Type.Array.tests + ] diff --git a/tests/Test/Copilot/Core/Type.hs b/tests/Test/Copilot/Core/Type.hs new file mode 100644 --- /dev/null +++ b/tests/Test/Copilot/Core/Type.hs @@ -0,0 +1,451 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +-- | Test copilot-core:Copilot.Core.Type. +module Test.Copilot.Core.Type where + +-- External imports +import Data.Int (Int16, Int32, Int64, Int8) +import Data.Maybe (isJust) +import Data.Proxy (Proxy (..)) +import Data.Type.Equality (TestEquality (..), testEquality, + (:~:) (..)) +import Data.Word (Word16, Word32, Word64, Word8) +import GHC.TypeLits (sameSymbol) +import Prelude as P +import Test.Framework (Test, testGroup) +import Test.Framework.Providers.QuickCheck2 (testProperty) +import Test.QuickCheck (Gen, Property, arbitrary, elements, + expectFailure, forAll, forAllBlind, + property, shuffle, (==>)) + +-- Internal imports: library modules being tested +import Copilot.Core.Type (Field (..), SimpleType (..), Struct (..), + Type (..), Typed, UType (..), Value (..), + accessorName, fieldName, simpleType, typeLength, + typeOf, typeSize) +import Copilot.Core.Type.Array (Array) + +-- | All unit tests for copilot-core:Copilot.Core.Type. +tests :: Test.Framework.Test +tests = + testGroup "Copilot.Core.Type" + [ testProperty "simpleType preserves inequality" + testSimpleTypesInequality + , testProperty "reflexivity of equality of simple types" + testSimpleTypesEqualityReflexive + , testProperty "symmetry of equality of simple types" + testSimpleTypesEqualitySymmetric + , testProperty "transitivity of equality of simple types" + testSimpleTypesEqualityTransitive + , testProperty "uniqueness of equality of simple types" + testSimpleTypesEqualityUniqueness + , testProperty "typeLength matches array size for 1-dimensional arrays" + testTypeLength1 + , testProperty "typeLength matches array size for 2-dimensional arrays" + testTypeLength2 + , testProperty "typeSize matches full array size for 1-dimensional arrays" + testTypeSize1 + , testProperty "typeSize matches full array size for 2-dimensional arrays" + testTypeSize2 + , testProperty "equality of types" + testUTypesEqualitySymmetric + , testProperty "equality of utype" + testUTypesEq + , testProperty "inequality of utype" + testUTypesInequality + , testProperty "inequality of utype via typeOf" + testUTypesTypeOfInequality + , testProperty "inequality of different types" + testTypesInequality + , testProperty "fieldName matches field name (positive)" + testFieldNameOk + , testProperty "fieldName matches field name (negative)" + testFieldNameFail + , testProperty "Show field name" + testShowField + , testProperty "Show struct" + testShowStruct + , testProperty "Update struct" + testUpdateStruct + , testProperty "Update struct" + testUpdateStructFail + , testProperty "accessorName matches field name (positive)" + testAccessorNameOk + , testProperty "accessorName matches field name (negative)" + testAccessorNameFail + , testProperty "typeName matches struct type name (positive)" + testTypeNameOk + , testProperty "typeName matches struct type name (negative)" + testTypeNameFail + ] + +-- | Test that the function simpleTypes preserves inequality, that is, it +-- returns different values for different types. This test is limited; we do +-- not test structs or arrays. +testSimpleTypesInequality :: Property +testSimpleTypesInequality = forAllBlind twoDiffTypes $ \(t1, t2) -> + t1 /= t2 + where + twoDiffTypes :: Gen (SimpleType, SimpleType) + twoDiffTypes = do + shuffled <- shuffle diffTypes + case shuffled of + (t1:t2:_) -> return (t1, t2) + _ -> return (SBool, SBool) + + -- | A list of types that should all be different. + diffTypes :: [SimpleType] + diffTypes = [ simpleType Bool + , simpleType Int8 + , simpleType Int16 + , simpleType Int32 + , simpleType Int64 + , simpleType Word8 + , simpleType Word16 + , simpleType Word32 + , simpleType Word64 + , simpleType Float + , simpleType Double + , simpleType (Array Int8 :: Type (Array 3 Int8)) + , simpleType (Struct (S (Field 0) (Field 0))) + ] + +-- | Test that the equality relation for simple types is reflexive. +testSimpleTypesEqualityReflexive :: Property +testSimpleTypesEqualityReflexive = + forAllBlind (elements simpleTypes) $ \t -> + t == t + +-- | Test that the equality relation for simple types is symmetric. +testSimpleTypesEqualitySymmetric :: Property +testSimpleTypesEqualitySymmetric = + forAllBlind (elements simpleTypes) $ \t1 -> + forAllBlind (elements simpleTypes) $ \t2 -> + t1 == t2 ==> t2 == t1 + +-- | Test that the equality relation for simple types is transitive. +testSimpleTypesEqualityTransitive :: Property +testSimpleTypesEqualityTransitive = + forAllBlind (elements simpleTypes) $ \t1 -> + forAllBlind (elements simpleTypes) $ \t2 -> + forAllBlind (elements simpleTypes) $ \t3 -> + (t1 == t2 && t2 == t3) ==> (t1 == t3) + +-- | Test that each type is only equal to itself. +testSimpleTypesEqualityUniqueness :: Property +testSimpleTypesEqualityUniqueness = + forAllBlind (shuffle simpleTypes) $ \(t:ts) -> + notElem t ts + +-- | Simple types tested. +simpleTypes :: [SimpleType] +simpleTypes = + [ SBool + , SInt8 + , SInt16 + , SInt32 + , SInt64 + , SWord8 + , SWord16 + , SWord32 + , SWord64 + , SFloat + , SDouble + , SStruct + , SArray Int8 + , SArray Int16 + ] + +-- | Test that the length of an array is as expected. +testTypeLength1 :: Property +testTypeLength1 = property $ typeLength a == 3 + where + a :: Type (Array 3 Int8) + a = Array Int8 + +-- | Test that the length of an multi-dimensional array is as expected. +testTypeLength2 :: Property +testTypeLength2 = property $ typeLength a == 3 + where + a :: Type (Array 3 (Array 12 Int8)) + a = Array (Array Int8) + +-- | Test that the size of an array is as expected. +testTypeSize1 :: Property +testTypeSize1 = property $ typeLength a == 3 + where + a :: Type (Array 3 Int8) + a = Array Int8 + +-- | Test that the size of a multi-dimensional array is as expected (flattens +-- the array). +testTypeSize2 :: Property +testTypeSize2 = property $ typeSize a == 36 + where + a :: Type (Array 3 (Array 12 Int8)) + a = Array (Array Int8) + +-- | Test that equality is symmetric for UTypes via testEquality. +testUTypesEqualitySymmetric :: Property +testUTypesEqualitySymmetric = + forAllBlind (elements utypes) $ \(UType t1) -> testEquality t1 t1 == Just Refl + +-- | Test that testEquality implies equality for UTypes. +testUTypesEq :: Property +testUTypesEq = + forAllBlind (elements utypes) $ \t@(UType t1) -> (testEquality t1 t1 == Just Refl) ==> t == t + +-- | Test that any two different UTypes are not equal. +-- +-- This function pre-selects two UTypes from a list of different UTypes, which +-- guarantees that they will be different. +testUTypesInequality :: Property +testUTypesInequality = forAllBlind twoDiffTypes $ \(t1, t2) -> + t1 /= t2 + where + twoDiffTypes :: Gen (UType, UType) + twoDiffTypes = do + shuffled <- shuffle utypes + case shuffled of + (t1:t2:_) -> return (t1, t2) + _ -> return (UType Bool, UType Bool) + +-- | Test that any two different Types are not equal. +-- +-- This function pre-selects two Types from a list of different UTypes, which +-- guarantees that they will be different. +testTypesInequality :: Property +testTypesInequality = forAllBlind twoDiffTypes $ \(UType t1, UType t2) -> + testEquality t1 t2 == Nothing + where + twoDiffTypes :: Gen (UType, UType) + twoDiffTypes = do + shuffled <- shuffle utypes + case shuffled of + (t1:t2:_) -> return (t1, t2) + _ -> return (UType Bool, UType Bool) + +-- | Different UTypes. +utypes :: [UType] +utypes = + [ UType Bool + , UType Int8 + , UType Int16 + , UType Int32 + , UType Int64 + , UType Word8 + , UType Word16 + , UType Word32 + , UType Word64 + , UType Float + , UType Double + , UType a1 + , UType a2 + , UType a3 + , UType a4 + , UType b1 + , UType b2 + , UType b3 + , UType b4 + , UType c + ] + where + a1 :: Type (Array 3 Int8) + a1 = Array Int8 + + a2 :: Type (Array 4 Int8) + a2 = Array Int8 + + a3 :: Type (Array 5 Int8) + a3 = Array Int8 + + a4 :: Type (Array 6 Int8) + a4 = Array Int8 + + b1 :: Type (Array 3 Int16) + b1 = Array Int16 + + b2 :: Type (Array 4 Int16) + b2 = Array Int16 + + b3 :: Type (Array 5 Int16) + b3 = Array Int16 + + b4 :: Type (Array 6 Int16) + b4 = Array Int16 + + c :: Type S + c = Struct (S (Field 0) (Field 0)) + +-- | Test that any two different UTypes are not equal. +-- +-- This function pre-selects two UTypes from a list of different UTypes built +-- via the function typeOf, which guarantees that they will be different. +testUTypesTypeOfInequality :: Property +testUTypesTypeOfInequality = forAllBlind twoDiffTypes $ \(t1@(UType t1'), t2@(UType t2')) -> + -- The seqs are important: otherwise, the coverage goes down drastically + -- because the typeOf function is not really executed. + t1' `seq` t2' `seq` t1 /= t2 + where + twoDiffTypes :: Gen (UType, UType) + twoDiffTypes = do + shuffled <- shuffle uTypesTypeOf + case shuffled of + (t1:t2:_) -> t1 `seq` t2 `seq` return (t1, t2) + _ -> return (UType Bool, UType Bool) + +-- | Different UTypes, produced by using the function typeOf. +uTypesTypeOf :: [UType] +uTypesTypeOf = + [ UType (typeOf :: Type Bool) + , UType (typeOf :: Type Int8) + , UType (typeOf :: Type Int16) + , UType (typeOf :: Type Int32) + , UType (typeOf :: Type Int64) + , UType (typeOf :: Type Word8) + , UType (typeOf :: Type Word16) + , UType (typeOf :: Type Word32) + , UType (typeOf :: Type Word64) + , UType (typeOf :: Type Float) + , UType (typeOf :: Type Double) + , UType (typeOf :: Type (Array 3 Int8)) + , UType (typeOf :: Type (Array 3 Int16)) + , UType (typeOf :: Type (Array 3 Int32)) + , UType (typeOf :: Type (Array 3 Int64)) + , UType (typeOf :: Type (Array 3 Word8)) + , UType (typeOf :: Type (Array 3 Word16)) + , UType (typeOf :: Type (Array 3 Word32)) + , UType (typeOf :: Type (Array 3 Word64)) + , UType (typeOf :: Type (Array 3 Double)) + , UType (typeOf :: Type (Array 3 Float)) + , UType (typeOf :: Type S) + ] + +-- | Test the fieldName function (should succeed). +testFieldNameOk :: Property +testFieldNameOk = forAll arbitrary $ \k1 -> + forAll arbitrary $ \k2 -> + fieldName (s1 (S (Field k1) (Field k2))) == s1FieldName + where + s1FieldName = "field1" + +-- | Test the fieldName function (should fail). +testFieldNameFail :: Property +testFieldNameFail = expectFailure $ property $ + fieldName (s1 sampleS) == s1FieldName + where + sampleS = S (Field 0) (Field 0) + s1FieldName = "Field" + +-- | Test showing a field of a struct. +testShowField :: Property +testShowField = forAll arbitrary $ \k -> + show (s1 (S (Field k) (Field 0))) == ("field1:" ++ show k) + +-- | Test showing a struct. +testShowStruct :: Property +testShowStruct = forAll arbitrary $ \k1 -> + forAll arbitrary $ \k2 -> + show (S (Field k1) (Field k2)) == "" + +-- | Test showing a struct. +testUpdateStruct :: Property +testUpdateStruct = + forAll arbitrary $ \k1 -> + forAll arbitrary $ \k2 -> + let f :: Field "field1" Int8 + f = Field k2 + v :: Value Int8 + v = Value Int8 f + in unField (s1 (updateField (S (Field k1) (Field 0)) v)) == k2 + + where + unField (Field x) = x + +-- | Test showing a struct. +testUpdateStructFail :: Property +testUpdateStructFail = expectFailure $ + forAll arbitrary $ \k1 -> + forAll arbitrary $ \k3 -> + let f :: Field "field" Int8 + f = Field k3 + v :: Value Int8 + v = Value Int8 f + in unField (s3 (updateField (S3 (Field k1)) v)) == k3 + + where + unField (Field x) = x + +-- | Test the accessorName of a field of a struct (should succeed). +testAccessorNameOk :: Property +testAccessorNameOk = property $ + accessorName s1 == s1FieldName + where + s1FieldName = "field1" + +-- | Test the accessorName of a field of a struct (should fail). +testAccessorNameFail :: Property +testAccessorNameFail = expectFailure $ property $ + accessorName s1 == s1FieldName + where + s1FieldName = "Field1" + +-- | Test the typeName of a struct (should succeed). +testTypeNameOk :: Property +testTypeNameOk = property $ + typeName sampleS == s1TypeName + + where + + sampleS :: S + sampleS = S (Field 0) (Field 0) + + s1TypeName :: String + s1TypeName = "S" + +-- | Test the typeName of a struct (should fail). +testTypeNameFail :: Property +testTypeNameFail = expectFailure $ property $ + typeName sampleS == s1TypeName + + where + + sampleS :: S + sampleS = S (Field 0) (Field 0) + + s1TypeName :: String + s1TypeName = "s" + +-- | Auxiliary struct defined for testing purposes. +data S = S { s1 :: Field "field1" Int8, s2 :: Field "field2" Word8 } + +instance Struct S where + typeName _ = "S" + + toValues s = [ Value Int8 (s1 s), Value Word8 (s2 s) ] + + updateField s (Value fieldTy (field :: Field fieldName a)) + | Just Refl <- sameSymbol (Proxy @"field1") (Proxy @fieldName) + , Just Refl <- testEquality Int8 fieldTy + = s { s1 = field } + | Just Refl <- sameSymbol (Proxy @"field2") (Proxy @fieldName) + , Just Refl <- testEquality Word8 fieldTy + = s { s2 = field } + | otherwise + = error $ "Unexpected field: " P.++ show field + +instance Typed S where + typeOf = Struct (S (Field 0) (Field 0)) + +-- | Auxiliary struct defined for testing purposes. +data S3 = S3 { s3 :: Field "field" Int8 } + +instance Struct S3 where + typeName _ = "S3" + + toValues s = [ Value Int8 (s3 s) ] + +instance Typed S3 where + typeOf = Struct (S3 (Field 0)) diff --git a/tests/Test/Copilot/Core/Type/Array.hs b/tests/Test/Copilot/Core/Type/Array.hs new file mode 100644 --- /dev/null +++ b/tests/Test/Copilot/Core/Type/Array.hs @@ -0,0 +1,186 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +-- | Test copilot-core:Copilot.Core.Type.Array. +module Test.Copilot.Core.Type.Array where + +-- External imports +import Data.Int (Int64) +import Data.Proxy (Proxy (..)) +import GHC.TypeNats (KnownNat, natVal) +import Test.Framework (Test, testGroup) +import Test.Framework.Providers.QuickCheck2 (testProperty) +import Test.QuickCheck (Gen, Property, arbitrary, + chooseInt, expectFailure, forAll, + getNegative, getNonNegative, oneof, + property, vector, vectorOf) + +-- Internal imports: library modules being tested +import Copilot.Core.Type.Array (Array, array, arrayElems, arrayUpdate) + +-- | All unit tests for copilot-core:Copilot.Core.Array. +tests :: Test.Framework.Test +tests = + testGroup "Copilot.Core.Type.Array" + [ testProperty "arrayElems . array (identity; 0)" + (testArrayElemsLeft (Proxy :: Proxy 0)) + , testProperty "arrayElems . array (identity; 5)" + (testArrayElemsLeft (Proxy :: Proxy 5)) + , testProperty "arrayElems . array (identity; 200)" + (testArrayElemsLeft (Proxy :: Proxy 200)) + , testProperty "array of incorrect length" + testArrayElemsFail + , testProperty "Show for arrays" + testShowArray + , testProperty "arrayElems (arrayUpdate x i v) !! i == v" + (testArrayUpdateElem (Proxy :: Proxy 5)) + , testProperty "arrayUpdate x i ((arrayElems x) !! i) == x" + (testArrayUpdateElems (Proxy :: Proxy 5)) + , testProperty "arrayUpdate fails if out of range of array" + (testArrayUpdateWrong (Proxy :: Proxy 5)) + , testProperty "array fails length is wrong" + (testArrayMakeWrongLength (Proxy :: Proxy 5)) + ] + +-- * Individual tests + +-- | Test that building an array from a list and extracting the elements with +-- the function 'arrayElems' will result in the same list. +testArrayElemsLeft :: forall n . KnownNat n => Proxy n -> Property +testArrayElemsLeft len = + forAll xsInt64 $ \ls -> + let array' :: Array n Int64 + array' = array ls + in arrayElems array' == ls + + where + + -- Generator for lists of Int64 of known length. + xsInt64 :: Gen [Int64] + xsInt64 = vectorOf (fromIntegral (natVal len)) arbitrary + +-- | Test that arrays cannot be properly evaluated if their length does not +-- match their type. +testArrayElemsFail :: Property +testArrayElemsFail = expectFailure $ forAll (vector 3) $ \l -> + let v = array l :: Array 4 Int64 + in arrayElems v == l + +-- | Test show for arrays. +testShowArray :: Property +testShowArray = forAll (vector 3) $ \l -> property $ + show (array l :: Array 3 Int64) == show (l :: [Int64]) + +-- | Test that updating an array updates the element appropriately (if we +-- project that element we get the value we put in). +testArrayUpdateElem :: forall n . KnownNat n => Proxy n -> Property +testArrayUpdateElem len = + forAll xsInt64 $ \ls -> + forAll position $ \p -> + forAll xInt64 $ \v -> + let -- Original array + array' :: Array n Int64 + array' = array ls + + -- Updated array + array'' :: Array n Int64 + array'' = arrayUpdate array' p v + + in arrayElems array'' !! p == v + + where + + -- Generator for lists of Int64 of known length. + xsInt64 :: Gen [Int64] + xsInt64 = vectorOf (fromIntegral (natVal len)) arbitrary + + -- Generator for element of type Int64. + xInt64 :: Gen Int64 + xInt64 = arbitrary + + -- Generator for positions within the list. + position :: Gen Int + position = chooseInt (0, fromIntegral (natVal len) - 1) + +-- | Test that updating an array updates the element appropriately (if we +-- project that element we get the value we put in). +testArrayUpdateWrong :: forall n . KnownNat n => Proxy n -> Property +testArrayUpdateWrong len = + expectFailure $ + forAll xsInt64 $ \ls -> + forAll position $ \p -> + forAll xInt64 $ \v -> + let -- Original array + array' :: Array n Int64 + array' = array ls + + -- Updated array + array'' :: Array n Int64 + array'' = arrayUpdate array' (p + 10) v + + in arrayElems array'' !! p == v + + where + + -- Generator for lists of Int64 of known length. + xsInt64 :: Gen [Int64] + xsInt64 = vectorOf (fromIntegral (natVal len)) arbitrary + + -- Generator for element of type Int64. + xInt64 :: Gen Int64 + xInt64 = arbitrary + + -- Generator for positions within the list. + position :: Gen Int + position = oneof + [ (fromIntegral (natVal len) +) . getNonNegative <$> arbitrary + , getNegative <$> arbitrary + ] + +-- | Test that making an array of a specific length fails if the list of +-- elements supplied doesn't have the same length. +testArrayMakeWrongLength :: forall n . KnownNat n => Proxy n -> Property +testArrayMakeWrongLength len = + expectFailure $ + forAll wrongLength $ \length -> + forAll (xsInt64 length) $ \ls -> + let array' :: Array n Int64 + array' = array ls + in arrayElems array' == ls + where + xsInt64 length = vectorOf length arbitrary + expectedLength = fromIntegral (natVal len) + wrongLength = (expectedLength +) . getNonNegative <$> arbitrary + +-- | Test that updating an array updates the element appropriately (if we +-- project that element we get the value we put in). +testArrayUpdateElems :: forall n . KnownNat n => Proxy n -> Property +testArrayUpdateElems len = + forAll xsInt64 $ \ls -> + forAll position $ \p -> + forAll xInt64 $ \v -> + let -- Original array + array' :: Array n Int64 + array' = array ls + + -- Updated array + e :: Int64 + e = arrayElems array' !! p + + array'' :: Array n Int64 + array'' = arrayUpdate array' p e + + in arrayElems array'' == ls + + where + + -- Generator for lists of Int64 of known length. + xsInt64 :: Gen [Int64] + xsInt64 = vectorOf (fromIntegral (natVal len)) arbitrary + + -- Generator for element of type Int64. + xInt64 :: Gen Int64 + xInt64 = arbitrary + + -- Generator for positions within the list. + position :: Gen Int + position = chooseInt (0, fromIntegral (natVal len) - 1) diff --git a/tests/Test/Extra.hs b/tests/Test/Extra.hs new file mode 100644 --- /dev/null +++ b/tests/Test/Extra.hs @@ -0,0 +1,31 @@ +-- | Auxiliary testing helper functions. +module Test.Extra where + +-- External imports +import Control.Arrow ((***)) + +-- * Function application + +-- | Apply a tuple with two functions to a tuple of arguments. +apply1 :: (a1 -> b1, a2 -> b2) -- ^ Pair with functions + -> (a1, a2) -- ^ Pair with arguments + -> (b1, b2) -- ^ Pair with results +apply1 = uncurry (***) + +-- | Apply a tuple with two functions on two arguments to their tupled +-- arguments. +apply2 :: (a1 -> b1 -> c1, a2 -> b2 -> c2) -- ^ Pair with functions + -> (a1, a2) -- ^ Pair with first arguments + -> (b1, b2) -- ^ Pair with second arguments + -> (c1, c2) -- ^ Pair with results +apply2 fs = apply1 . apply1 fs + +-- | Apply a tuple with two functions on three arguments to their tupled +-- arguments. +apply3 :: (a1 -> b1 -> c1 -> d1, a2 -> b2 -> c2 -> d2) + -- ^ Pair with functions + -> (a1, a2) -- ^ Pair with first arguments + -> (b1, b2) -- ^ Pair with second arguments + -> (c1, c2) -- ^ Pair with third arguments + -> (d1, d2) -- ^ Pair with results +apply3 fs = apply2 . apply1 fs