name:                twee-lib
version:             2.4.2
synopsis:            An equational theorem prover
homepage:            http://github.com/nick8325/twee
license:             BSD3
license-file:        LICENSE
author:              Nick Smallbone
maintainer:          nicsma@chalmers.se
category:            Theorem Provers
build-type:          Simple
cabal-version:       >=1.10
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
   http://www.tptp.org). You can use types and quantifiers, but apart
   from that the problem must be equational.
   .
   This package contains only the library part of twee.

source-repository head
  type:     git
  location: git://github.com/nick8325/twee.git
  branch:   master

flag llvm
  description: Build using LLVM backend for faster code.
  default: False
  manual: True

flag bounds-checks
  description: Use bounds checks for all array operations.
  default: False
  manual: True

flag profile
  description: Print a profiling report after every prover run.
  default: False
  manual: True

library
  exposed-modules:
    Twee
    Twee.Base
    Twee.Constraints
    Twee.CP
    Twee.Equation
    Twee.Index
    Twee.Join
    Twee.KBO
    Twee.Pretty
    Twee.Profile
    Twee.Proof
    Twee.Rule
    Twee.Rule.Index
    Twee.Term
    Twee.Task
    Twee.Utils
    Data.Label
  other-modules:
    Data.BatchedQueue
    Data.ChurchList
    Data.DynamicArray
    Data.Heap
    Data.Numbered
    Data.PackedSequence
    Twee.Term.Core

  build-depends:
    base >= 4 && < 5,
    containers,
    transformers,
    dlist,
    pretty >= 1.1.2.0,
    ghc-prim,
    primitive >= 0.7.1.0,
    uglymemo,
    random,
    bytestring,
    cereal
  hs-source-dirs:      .
  ghc-options:         -W -fno-warn-incomplete-patterns -fno-warn-dodgy-imports
  default-language:    Haskell2010

  if flag(llvm)
    cpp-options: -DUSE_LLVM
  if flag(bounds-checks)
    cpp-options: -DBOUNDS_CHECKS
    exposed-modules:
      Data.Primitive.SmallArray.Checked
      Data.Primitive.ByteArray.Checked
      Data.Primitive.Checked
  if flag(profile)
    cpp-options: -DPROFILE
    build-depends: symbol, hashable, unordered-containers, rdtsc