cabal-version: 2.4
name: atp
version: 0.1.0.0
synopsis: Interface to automated theorem provers
description:
  Express theorems in first-order logic and automatically prove them using
  third-party reasoning tools.
homepage: https://github.com/aztek/atp
bug-reports: https://github.com/aztek/atp/issues
license: GPL-3.0-only
license-file: LICENSE
author: Evgenii Kotelnikov
maintainer: evgeny.kotelnikov@gmail.com
category: Theorem Provers, Formal Methods, Logic, Math
tested-with:
  GHC == 7.10.3,
  GHC == 8.0.2,
  GHC == 8.2.2,
  GHC == 8.4.4,
  GHC == 8.6.5,
  GHC == 8.8.4,
  GHC == 8.10.3

extra-source-files:
  CHANGELOG.md
  test/**/*.hs

source-repository head
  type: git
  location: git://github.com/aztek/atp.git

flag Werror
  default: False
  manual: True

-- Build test suites that require some theorem provers to be installed.
flag provers
  default: False
  manual: True

library
  hs-source-dirs: src
  default-language: Haskell2010
  exposed-modules:
    ATP
    ATP.Codec.TPTP
    ATP.Error
    ATP.FOL
    ATP.Pretty.FOL
    ATP.Prove
    ATP.Prover
  other-modules:
    ATP.Internal.Enumeration
    ATP.FirstOrder.Core
    ATP.FirstOrder.Alpha
    ATP.FirstOrder.Smart
    ATP.FirstOrder.Simplification
    ATP.FirstOrder.Occurrence
    ATP.FirstOrder.Conversion
    ATP.FirstOrder.Derivation
  ghc-options:
    -Wall
  if flag(Werror)
    ghc-options: -Werror
  build-depends:
    base           >= 4.8     && < 5.0,
    text           >= 1.2.3   && < 1.3,
    tptp           >= 0.1.3   && < 0.2,
    containers     >= 0.5.11  && < 0.7,
    mtl            >= 2.2     && < 3.0,
    ansi-wl-pprint >= 0.6.6   && < 0.7,
    process        >= 1.6.3   && < 1.7
  if impl(ghc < 8)
    ghc-options:
      -fwarn-incomplete-record-updates -fwarn-incomplete-uni-patterns
    build-depends:
      semigroups   >= 0.18    && < 1.0
  if impl(ghc >= 8)
    ghc-options:
      -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns
      -Wredundant-constraints

test-suite property
  type: exitcode-stdio-1.0
  hs-source-dirs: test
  default-language: Haskell2010
  main-is: Property/Main.hs
  other-modules:
    Property.Generators
    Property.Modifiers.AlphaEquivalent
    Property.Modifiers.Simplified
  ghc-options:
    -Wall -threaded
  if flag(Werror)
    ghc-options: -Werror
  build-depends:
    base,
    containers,
    text,
    mtl,
    generic-random >= 1.2.0.0 && < 1.3,
    QuickCheck     >= 2.4     && < 3.0,
    atp
  if impl(ghc < 8)
    ghc-options:
      -fwarn-incomplete-record-updates -fwarn-incomplete-uni-patterns
    build-depends:
      semigroups   >= 0.18    && < 1.0
  if impl(ghc >= 8)
    ghc-options:
      -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns
      -Wredundant-constraints

test-suite doc
  type: exitcode-stdio-1.0
  hs-source-dirs: test
  default-language: Haskell2010
  main-is: Doc/Main.hs
  other-modules:
    Property.Generators
  ghc-options:
    -Wall -threaded
  if flag(Werror)
    ghc-options: -Werror
  -- TODO: Make it work
  buildable: False
  build-depends:
    base,
    containers,
    text,
    generic-random >= 1.2.0.0 && < 1.3,
    QuickCheck     >= 2.4     && < 3.0,
    atp,
    doctest

test-suite unit
  type: detailed-0.9
  hs-source-dirs: test
  default-language: Haskell2010
  test-module: Unit.Main
  ghc-options:
    -Wall -threaded
  if flag(Werror)
    ghc-options: -Werror
  if flag(provers)
    buildable: True
  else
    buildable: False
  -- TODO: Workaround the pesky bug in ghc 8.0
  -- https://stackoverflow.com/q/39310043/1344648
  if (impl(ghc >= 8.0.0)) && (impl(ghc < 8.1.0))
    buildable: False
  build-depends:
    base,
    Cabal >= 1.16.0,
    atp