cabal-version:       2.4

name:                spectacle
version:             1.0.0
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.3

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
    -Wmissing-import-lists
    -Wunused-packages

  build-depends:
      base >=4.14 && <4.15

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

library
  import:              common
  hs-source-dirs:      src

  build-depends:
      comonad
    , containers >= 0.6
    , hashable >= 1.3.0.0
    , microlens
    , microlens-mtl
    , mtl >= 2.2
    , optparse-applicative
    , logict
    , prettyprinter
    , prettyprinter-ansi-terminal
    , text
    , transformers >= 0.5

  exposed-modules:
      Control.Applicative.Day
    , Control.Applicative.Phases
    , Control.Applicative.Queue
    , Control.Comonad.Tape
    , Control.Hyper
    , Control.Mealy
    , Control.Monad.Levels
    , Control.Monad.Levels.Internal
    , 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.Internal
    , 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.Closure.Internal
    , Language.Spectacle.Syntax.Enabled
    , Language.Spectacle.Syntax.Enabled.Internal
    , Language.Spectacle.Syntax.Env
    , Language.Spectacle.Syntax.Env.Internal
    , Language.Spectacle.Syntax.Error
    , Language.Spectacle.Syntax.Error.Internal
    , Language.Spectacle.Syntax.NonDet
    , Language.Spectacle.Syntax.NonDet.Internal
    , Language.Spectacle.Syntax.Plain
    , Language.Spectacle.Syntax.Plain.Internal
    , Language.Spectacle.Syntax.Prime
    , Language.Spectacle.Syntax.Prime.Internal
    , Language.Spectacle.Syntax.Quantifier
    , Language.Spectacle.Syntax.Quantifier.Internal
    , Language.Spectacle.Syntax.Logic
    , Language.Spectacle.Syntax.Logic.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:
      comonad
    , containers
    , spectacle
    , hedgehog
    , microlens
    , 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.SimpleClock
    Specifications.Status

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