cabal-version:       2.2
name:                twee
version:             2.7.1
synopsis:            An equational theorem prover
homepage:            https://twee.smallbone.se
license:             BSD-3-Clause
license-file:        LICENSE
author:              Nick Smallbone
maintainer:          nicsma@chalmers.se
category:            Theorem Provers
build-type:          Simple
extra-source-files:  README.md examples/*.p misc/*.hs misc/*.pl
description:
   Twee is an experimental equational theorem prover based on
   Knuth-Bendix completion.
   .
   Given a set of equational axioms and a set of equational
   conjectures it will try to prove the conjectures.
   It will terminate if the conjectures are true but normally
   fail to terminate if they are false.
   .
   The input problem should be in TPTP format (see
   https://www.tptp.org). You can use types and quantifiers, but apart
   from that the problem must be equational.

source-repository head
  type:     git
  location: https://codeberg.org/nick8325/twee
  branch:   main

flag static
  description: Build a static binary.
  default: False
  manual: True

flag parallel
  description: Build a special parallel version of Twee.
  default: False
  manual: True

flag rtsopts
  description: Enable -rtsopts (e.g. for setting maximum memory use.)
  default: False
  manual: True

common executable-stuff
  hs-source-dirs:      executable
  default-language:    Haskell2010
  build-depends:       base < 5,
                       twee-lib == 2.7.1,
                       containers,
                       pretty,
                       split,
                       jukebox == 0.5.15,
                       ansi-terminal >= 0.9,
                       symbol,
                       hashable,
                       bytestring,
                       binary,
                       process
  other-modules:       SequentialMain
  ghc-options:         -W -fno-warn-incomplete-patterns

  if flag(static)
    ghc-options: -optl -static

  if flag(rtsopts)
    ghc-options: -rtsopts

executable twee
  import: executable-stuff
  main-is: Main.hs

executable twee-lpo
  import: executable-stuff
  main-is: Main.hs
  cpp-options: -DUSE_LPO

executable parallel-twee
  import: executable-stuff
  if !flag(parallel)
    buildable: False

  main-is: ParallelMain.hs
  build-depends: async, unix
  c-sources: executable/link.c

Test-Suite twee-test
    type: exitcode-stdio-1.0
    Default-language: Haskell2010
    hs-source-dirs:
        test
    main-is: Main.hs
    build-depends: base < 5, QuickCheck, twee-lib == 2.7, containers, pretty, tasty, tasty-quickcheck, hashable, binary, bytestring
    other-modules:
        Common
        Index
        Nest
        Ordering
        Serial
        TermOrder
        Terms
    ghc-options:
      -threaded
      -feager-blackholing
      -with-rtsopts=-N