spectacle.cabal

cabal-version:       3.0

name:                spectacle
version:             1.0.1
category:            Testing, Concurrency
synopsis:            Embedded specification language & model checker in Haskell.
description:
  Spectacle is an embedded domain-specific language that provides a family
  of type-level combinators for authoring specifications of program behavior
  along with a model checker for verifying that user implementations of a
  program satisfy written specifications.

author:              Arista Networks
maintainer:          opensource@awakesecurity.com
homepage:            https://github.com/awakesecurity/spectacle
bug-reports:         https://github.com/awakesecurity/spectacle/issues
license:             Apache-2.0
license-file:        LICENSE
copyright:           2021 Arista Networks
build-type:          Simple
tested-with:
  GHC == 8.10.7
  GHC == 9.0.2
  GHC == 9.2.4

extra-source-files:
  README.md
  CHANGELOG.md

common common
  default-language: Haskell2010

  ghc-options:
    -Wall
    -Wcompat
    -Wincomplete-record-updates
    -Wincomplete-uni-patterns
    -Wmissing-fields
    -Wpartial-fields
    -Widentities
    -Wmissing-home-modules
    -Wredundant-constraints
    -fshow-warning-groups

  build-depends:
      base           >= 4.14 && < 4.18
    , comonad        >= 5
    , containers     >= 0.6
    , hashable       >= 1.3.4.0
    , logict         >= 0.8
    , microlens      >= 0.4
    , microlens-mtl  >= 0.2
    , mtl            >= 2.2
    , transformers   >= 0.5

  default-extensions:
     BangPatterns BlockArguments ConstraintKinds DataKinds DefaultSignatures
     DeriveFunctor DeriveGeneric DerivingVia FlexibleContexts FlexibleInstances
     GADTs ImportQualifiedPost LambdaCase MagicHash MultiParamTypeClasses
     PatternSynonyms PolyKinds RankNTypes RoleAnnotations ScopedTypeVariables
     StandaloneDeriving StandaloneKindSignatures TypeApplications TypeOperators
     UnicodeSyntax ViewPatterns

library
  import:         common
  hs-source-dirs: src

  build-depends:
    , optparse-applicative
    , prettyprinter
    , prettyprinter-ansi-terminal
    , text

  exposed-modules:
      Control.Applicative.Day
    , Control.Applicative.Phases
    , Control.Applicative.Queue
    , Control.Comonad.Tape
    , Control.Hyper
    , Control.Mealy
    , Control.Monad.Ref
    , Control.Natural
    , Data.Ascript
    , Data.Bag
    , Data.Fingerprint
    , Data.Functor.Loom
    , Data.Functor.Tree
    , Data.Name
    , Data.Node
    , Data.Type.List
    , Data.Type.Rec
    , Data.World
    , Language.Spectacle
    , Language.Spectacle.AST
    , Language.Spectacle.AST.Action
    , Language.Spectacle.AST.Temporal
    , Language.Spectacle.Exception.RuntimeException
    , Language.Spectacle.Fairness
    , Language.Spectacle.Interaction
    , Language.Spectacle.Interaction.CLI
    , Language.Spectacle.Interaction.Diagram
    , Language.Spectacle.Interaction.Doc
    , Language.Spectacle.Interaction.Options
    , Language.Spectacle.Interaction.Paths
    , Language.Spectacle.Interaction.Point
    , Language.Spectacle.Interaction.Pos
    , Language.Spectacle.Model
    , Language.Spectacle.Model.ModelAction
    , Language.Spectacle.Model.ModelEnv
    , Language.Spectacle.Model.ModelError
    , Language.Spectacle.Model.ModelNode
    , Language.Spectacle.Model.ModelState
    , Language.Spectacle.Model.ModelTemporal
    , Language.Spectacle.Model.Monad
    , Language.Spectacle.Lang
    , Language.Spectacle.Lang.Member
    , Language.Spectacle.Lang.Op
    , Language.Spectacle.Lang.Scoped
    , Language.Spectacle.RTS.Registers
    , Language.Spectacle.Specification
    , Language.Spectacle.Specification.Action
    , Language.Spectacle.Specification.Prop
    , Language.Spectacle.Specification.Variable
    , Language.Spectacle.Syntax
    , Language.Spectacle.Syntax.Closure
    , Language.Spectacle.Syntax.Enabled
    , Language.Spectacle.Syntax.Env
    , Language.Spectacle.Syntax.Error
    , Language.Spectacle.Syntax.Logic
    , Language.Spectacle.Syntax.NonDet
    , Language.Spectacle.Syntax.Plain
    , Language.Spectacle.Syntax.Prime
    , Language.Spectacle.Syntax.Quantifier

  other-modules:
    , Language.Spectacle.Lang.Internal
    , Language.Spectacle.Syntax.Closure.Internal
    , Language.Spectacle.Syntax.Enabled.Internal
    , Language.Spectacle.Syntax.Env.Internal
    , Language.Spectacle.Syntax.Error.Internal
    , Language.Spectacle.Syntax.Logic.Internal
    , Language.Spectacle.Syntax.NonDet.Internal
    , Language.Spectacle.Syntax.Plain.Internal
    , Language.Spectacle.Syntax.Prime.Internal
    , Language.Spectacle.Syntax.Quantifier.Internal

test-suite unit-tests
  import:              common
  type:                exitcode-stdio-1.0
  hs-source-dirs:      test/unit-tests
  main-is:             Main.hs

  other-modules:
    Test.Control.Comonad.Tape
    Test.Gen
    Test.Gen.Rec
    Test.Language.Spectacle.Interaction
    Test.Language.Spectacle.Interaction.Paths
    Test.Language.Spectacle.Interaction.Pos
    Test.Laws.Lens
    Test.Laws.Ord

  build-depends:
      spectacle
    , hedgehog
    , tasty
    , tasty-hedgehog

test-suite integration-tests
  import:              common
  type:                exitcode-stdio-1.0
  hs-source-dirs:      test/integration
  main-is:             Main.hs

  other-modules:
    Specifications.BitClock
    Specifications.Diehard
    Specifications.RateLimit
    Specifications.SimpleClock
    Specifications.SpanningTree
    Specifications.Status

  build-depends:
      spectacle
    , hedgehog
    , tasty
    , tasty-hedgehog