Name:             atp-haskell
Version:          1.14
x-revision: 1
Synopsis:         Translation from Ocaml to Haskell of John Harrison's ATP code
Description:      This package is a liberal translation from OCaml to Haskell of
                  the automated theorem prover written in OCaml in
                  John Harrison's book "Practical Logic and Automated
                  Reasoning".  Click on module ATP below for an overview.
Homepage:         https://github.com/seereason/atp-haskell
License:          BSD3
License-File:     LICENSE.txt
Author:           John Harrison
Maintainer:       David Fox <dsf@seereason.com>
Bug-Reports:      https://github.com/seereason/atp-haskell/issues
Category:         Logic, Theorem Provers
Cabal-version:    >= 1.9
Build-Type:       Simple
Extra-Source-Files: tests/Extra.hs, .travis.yml, .ghci
Tested-With:      GHC == 7.10.3, GHC == 7.11.*

Source-Repository head
  type: git
  location: https://github.com/seereason/atp-haskell

Library
  Build-Depends:
    applicative-extras,
    base >= 4.8 && < 4.13,
    containers,
    extra,
    HUnit,
    mtl,
    parsec,
    pretty >= 1.1.2,
    template-haskell,
    time
  GHC-options: -Wall -O2
  Hs-Source-Dirs: src
  Exposed-Modules:
    Data.Logic.ATP
    Data.Logic.ATP.Lib
    Data.Logic.ATP.Pretty
    Data.Logic.ATP.Formulas
    Data.Logic.ATP.Term
    Data.Logic.ATP.Apply
    Data.Logic.ATP.Equate
    --
    Data.Logic.ATP.Lit
    Data.Logic.ATP.LitWrapper
    Data.Logic.ATP.Prop
    Data.Logic.ATP.PropExamples
    Data.Logic.ATP.DefCNF
    Data.Logic.ATP.DP
    -- Data.Logic.ATP.Stal
    -- Data.Logic.ATP.BDD
    Data.Logic.ATP.Quantified
    Data.Logic.ATP.Parser
    Data.Logic.ATP.FOL
    Data.Logic.ATP.ParserTests
    Data.Logic.ATP.Skolem
    Data.Logic.ATP.Herbrand
    Data.Logic.ATP.Unif
    Data.Logic.ATP.Tableaux
    Data.Logic.ATP.Resolution
    Data.Logic.ATP.Prolog
    Data.Logic.ATP.Meson
    -- Data.Logic.ATP.Skolems
    Data.Logic.ATP.Equal
    -- Data.Logic.ATP.Cong
    -- Data.Logic.ATP.Rewrite
    -- Data.Logic.ATP.Order
    -- Data.Logic.ATP.Completion
    -- Data.Logic.ATP.Eqelim
    -- Data.Logic.ATP.Paramodulation
    --
    -- Data.Logic.ATP.Decidable
    -- Data.Logic.ATP.Qelim
    -- Data.Logic.ATP.Cooper
    -- Data.Logic.ATP.Complex
    -- Data.Logic.ATP.Real
    -- Data.Logic.ATP.Grobner
    -- Data.Logic.ATP.Geom
    -- Data.Logic.ATP.Interpolation
    -- Data.Logic.ATP.Combining

    -- Data.Logic.ATP.Lcf
    -- Data.Logic.ATP.Lcfprop
    -- Data.Logic.ATP.Folderived
    -- Data.Logic.ATP.Lcffol
    -- Data.Logic.ATP.Tactics

    -- Data.Logic.ATP.Limitations

Test-Suite atp-haskell-tests
  Type: exitcode-stdio-1.0
  Hs-Source-Dirs: tests
  Main-Is: Main.hs
  Build-Depends: atp-haskell, base, containers, HUnit, time
  GHC-options: -Wall -O2