name:               tamarin-prover-theory

cabal-version:      >= 1.8
build-type:         Simple
version:            0.8.6.0
license:            GPL
license-file:       LICENSE
category:           Theorem Provers
author:             Benedikt Schmidt <benedikt.schmidt@inf.ethz.ch>,
                    Simon Meier <simon.meier@inf.ethz.ch>
maintainer:         Benedikt Schmidt <benedikt.schmidt@inf.ethz.ch>
copyright:          Benedikt Schmidt, Simon Meier, ETH Zurich, 2010-2012

synopsis:           Term manipulation library for the tamarin prover.

description:        This is an internal library of the Tamarin prover for
                    security protocol verification
                    (<hackage.haskell.org/package/tamarin-prover>).
                    .
                    This library provides the types to represent security
                    protocol, and it implements the constraint solver.

homepage:           http://www.infsec.ethz.ch/research/software/tamarin


source-repository head
  type:     git
  location: https://github.com/tamarin-prover/tamarin-prover.git

----------------------
-- library stanzas
----------------------

library
    ghc-options:       -Wall -fwarn-tabs

    ghc-prof-options:  -auto-all

    build-depends:
        base              == 4.*
      , bytestring        >= 0.9
      , deepseq           >= 1.3
      , array             >= 0.3  
      , containers        >= 0.4.2
      , dlist             >= 0.5
      , mtl               >= 2.1
      , cmdargs           == 0.10.*
      , filepath          >= 1.1
      , directory         >= 1.0
      , process           >= 1.1
      , parsec            == 3.1.*
      , safe              >= 0.2  && < 0.4
      , transformers      >= 0.3
      , fclabels          == 1.*
      , uniplate          == 1.6.*
      , syb               >= 0.3.3
      , binary            == 0.5.*
      , derive            == 2.5.*
      , time              >= 1.2 
      , parallel          >= 3.2
      , HUnit             >= 1.2

      , tamarin-prover-utils >= 0.8.5.1  && < 0.9
      , tamarin-prover-term  >= 0.8.5.1  && < 0.9


    hs-source-dirs: src

    exposed-modules:
      Theory
      Theory.Proof

      Theory.Constraint.Solver
      Theory.Constraint.Solver.CaseDistinctions
      Theory.Constraint.Solver.Contradictions
      Theory.Constraint.Solver.Goals
      Theory.Constraint.Solver.ProofMethod
      Theory.Constraint.Solver.Reduction
      Theory.Constraint.Solver.Simplify
      Theory.Constraint.Solver.Types

      Theory.Constraint.System
      Theory.Constraint.System.Constraints
      Theory.Constraint.System.Dot
      Theory.Constraint.System.Guarded

      Theory.Model
      Theory.Model.Atom
      Theory.Model.Fact
      Theory.Model.Formula
      Theory.Model.Rule
      Theory.Model.Signature

      Theory.Text.Pretty
      Theory.Text.Parser
      Theory.Text.Parser.Token

      Theory.Tools.AbstractInterpretation
      Theory.Tools.EquationStore
      Theory.Tools.InjectiveFactInstances
      Theory.Tools.IntruderRules
      Theory.Tools.LoopBreakers
      Theory.Tools.RuleVariants
      Theory.Tools.Wellformedness

    other-modules: