gcl-verifier.cabal

cabal-version: 3.6

name: gcl-verifier
version: 0.0.0.0
synopsis: WLP-based GCL verifier
description: Please see the README on GitHub at <https://github.com/aionescu/gcl-verifier#readme>
homepage: https://github.com/aionescu/gcl-verifier#readme
bug-reports: https://github.com/aionescu/gcl-verifier/issues
license: GPL-3.0-only
license-file: LICENSE.txt
build-type: Simple
extra-source-files: README.md

executable gcl-verifier
  hs-source-dirs: src
  main-is: Main.hs

  other-modules:
    Language.GCL.Opts
    Language.GCL.Parser
    Language.GCL.Syntax
    Language.GCL.Syntax.Helpers
    Language.GCL.Syntax.Mutation
    Language.GCL.Syntax.Preprocess
    Language.GCL.TypeChecking
    Language.GCL.Utils
    Language.GCL.Verification
    Language.GCL.Verification.Linearization
    Language.GCL.Verification.Simplification
    Language.GCL.Verification.WLP
    Language.GCL.Verification.Z3

  build-depends:
    base >=4.15 && <5
    , containers ^>= 0.6.4
    , data-fix ^>= 0.3.2
    , megaparsec ^>= 9.2
    , mtl ^>= 2.3
    , optparse-applicative ^>= 0.17
    , parser-combinators ^>= 1.3
    , recursion-schemes ^>= 5.2.2.2
    , text ^>= 2
    , z3 ^>= 408.2

  ghc-options:
    -- -threaded
    -- -rtsopts
    -- -with-rtsopts=-N
    -Wall
    -Wcompat
    -Widentities
    -Wincomplete-record-updates
    -Wincomplete-uni-patterns
    -Wno-name-shadowing
    -Wno-unticked-promoted-constructors
    -Wredundant-constraints
    -Wunused-packages

  default-language: Haskell2010

  default-extensions:
    -- GHC2021
    BangPatterns
    BinaryLiterals
    ConstrainedClassMethods
    ConstraintKinds
    DeriveDataTypeable
    DeriveFoldable
    DeriveFunctor
    DeriveGeneric
    DeriveLift
    DeriveTraversable
    DoAndIfThenElse
    EmptyCase
    EmptyDataDecls
    EmptyDataDeriving
    ExistentialQuantification
    ExplicitForAll
    FlexibleContexts
    FlexibleInstances
    ForeignFunctionInterface
    GADTSyntax
    GeneralisedNewtypeDeriving
    HexFloatLiterals
    ImplicitPrelude
    ImportQualifiedPost
    InstanceSigs
    KindSignatures
    MonomorphismRestriction
    MultiParamTypeClasses
    NamedFieldPuns
    NamedWildCards
    NumericUnderscores
    PatternGuards
    PolyKinds
    PostfixOperators
    RankNTypes
    RelaxedPolyRec
    ScopedTypeVariables
    StandaloneDeriving
    StandaloneKindSignatures
    StarIsType
    TraditionalRecordSyntax
    TupleSections
    TypeApplications
    TypeOperators
    TypeSynonymInstances

    ApplicativeDo
    BlockArguments
    DataKinds
    DefaultSignatures
    DeriveAnyClass
    DerivingStrategies
    DerivingVia
    DuplicateRecordFields
    FunctionalDependencies
    GADTs
    GeneralizedNewtypeDeriving
    LambdaCase
    LexicalNegation
    MagicHash
    MultiWayIf
    NegativeLiterals
    NoMonomorphismRestriction
    NoStarIsType
    OverloadedStrings
    PartialTypeSignatures
    PatternSynonyms
    QuantifiedConstraints
    RecordWildCards
    RecursiveDo
    TypeFamilies
    TypeFamilyDependencies
    UnboxedTuples
    UndecidableInstances
    ViewPatterns