copilot-core 2.2.1 → 4.8
raw patch · 32 files changed
Files
- CHANGELOG +194/−0
- README.md +24/−52
- copilot-core.cabal +47/−46
- src/Copilot/Compile/Header/C99.hs +0/−223
- src/Copilot/Core.hs +23/−31
- src/Copilot/Core/Error.hs +0/−19
- src/Copilot/Core/Expr.hs +50/−49
- src/Copilot/Core/External.hs +0/−174
- src/Copilot/Core/Interpret.hs +0/−27
- src/Copilot/Core/Interpret/Eval.hs +0/−391
- src/Copilot/Core/Interpret/Render.hs +0/−97
- src/Copilot/Core/Locals.hs +0/−90
- src/Copilot/Core/MakeTags.hs +0/−127
- src/Copilot/Core/Operators.hs +46/−19
- src/Copilot/Core/PrettyDot.hs +0/−294
- src/Copilot/Core/PrettyPrint.hs +0/−196
- src/Copilot/Core/Random.hs +0/−334
- src/Copilot/Core/Random/Gen.hs +0/−136
- src/Copilot/Core/Random/Weights.hs +0/−75
- src/Copilot/Core/Spec.hs +78/−54
- src/Copilot/Core/Type.hs +413/−68
- src/Copilot/Core/Type/Array.hs +64/−0
- src/Copilot/Core/Type/Dynamic.hs +0/−53
- src/Copilot/Core/Type/Eq.hs +0/−78
- src/Copilot/Core/Type/Equality.hs +0/−37
- src/Copilot/Core/Type/Read.hs +0/−52
- src/Copilot/Core/Type/Show.hs +0/−77
- src/Copilot/Core/Type/Uninitialized.hs +0/−31
- tests/Main.hs +20/−0
- tests/Test/Copilot/Core/Type.hs +451/−0
- tests/Test/Copilot/Core/Type/Array.hs +186/−0
- tests/Test/Extra.hs +31/−0
+ CHANGELOG view
@@ -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)
README.md view
@@ -1,61 +1,33 @@-[](https://travis-ci.org/Copilot-Language/copilot-core)+[](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).
copilot-core.cabal view
@@ -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- <https://github.com/leepike/copilot-discussion>.+ multiple back-end compilers, and other verification tools. .- Examples are available at- <https://github.com/leepike/Copilot/tree/master/Examples>.+ A tutorial, examples, and other information are available at+ <https://copilot-language.github.io>. -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 <ivan.perezdominguez@nasa.gov>+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
− src/Copilot/Compile/Header/C99.hs
@@ -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 <stdint.h>"- , "#include <stdbool.h>"- ]------------------------------------------------------------------------------------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----------------------------------------------------------------------------------
src/Copilot/Core.hs view
@@ -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
− src/Copilot/Core/Error.hs
@@ -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 <lee pike @ gmail . com> " ++- "(remove spaces) or file a bug report on github.com."--badUsage :: String -> a-badUsage msg = error $ "Copilot error: " ++ msg
src/Copilot/Core/Expr.hs view
@@ -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)
− src/Copilot/Core/External.hs
@@ -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
− src/Copilot/Core/Interpret.hs
@@ -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
− src/Copilot/Core/Interpret/Eval.hs
@@ -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----------------------------------------------------------------------------------
− src/Copilot/Core/Interpret/Render.hs
@@ -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- }----------------------------------------------------------------------------------
− src/Copilot/Core/Locals.hs
@@ -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----------------------------------------------------------------------------------
− src/Copilot/Core/MakeTags.hs
@@ -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)
src/Copilot/Core/Operators.hs view
@@ -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.
− src/Copilot/Core/PrettyDot.hs
@@ -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----------------------------------------------------------------------------------
− src/Copilot/Core/PrettyPrint.hs
@@ -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----------------------------------------------------------------------------------
− src/Copilot/Core/Random.hs
@@ -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-
− src/Copilot/Core/Random/Gen.hs
@@ -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)----------------------------------------------------------------------------------
− src/Copilot/Core/Random/Weights.hs
@@ -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 }
src/Copilot/Core/Spec.hs view
@@ -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]+ }
src/Copilot/Core/Type.hs view
@@ -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
+ src/Copilot/Core/Type/Array.hs view
@@ -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)
− src/Copilot/Core/Type/Dynamic.hs
@@ -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
− src/Copilot/Core/Type/Eq.hs
@@ -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----------------------------------------------------------------------------------
− src/Copilot/Core/Type/Equality.hs
@@ -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
− src/Copilot/Core/Type/Read.hs
@@ -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----------------------------------------------------------------------------------
− src/Copilot/Core/Type/Show.hs
@@ -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----------------------------------------------------------------------------------
− src/Copilot/Core/Type/Uninitialized.hs
@@ -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
+ tests/Main.hs view
@@ -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+ ]
+ tests/Test/Copilot/Core/Type.hs view
@@ -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)) == "<field1:" ++ show k1 ++ ",field2:" ++ show 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))
+ tests/Test/Copilot/Core/Type/Array.hs view
@@ -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)
+ tests/Test/Extra.hs view
@@ -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