name:               tamarin-prover-term

cabal-version:      >= 1.8
build-type:         Simple
version:            0.6.0.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 term manipulation infrastructure
                    (matching, unification, narrowing, finite variants) for
                    the Tamarin prover. It uses maude
                    (<http://maude.cs.uiuc.edu/>) as a backend for
                    normalization, equational matching, and unification.

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-prof-options:  -auto-all

    build-depends:
        base                 == 4.*
      , mtl                  == 2.0.*
      , bytestring           == 0.9.*
      , attoparsec           == 0.10.*
      , containers           >= 0.4.2   && < 0.5
      , dlist                == 0.5.*
      , safe                 >= 0.2     && < 0.4
      , split                == 0.1.*
      , parsec               == 3.1.*
      , syb                  >= 0.3.3   && < 0.4
      , directory            == 1.1.*
      , process              == 1.1.*
      , deepseq              == 1.3.*
      , binary               == 0.5.*
      , derive               == 2.5.*

      , HUnit                == 1.2.*

      , tamarin-prover-utils == 0.6.*


    hs-source-dirs: src

    exposed-modules:
      Term.Unification
      Term.VTerm
      Term.LTerm
      Term.Positions
      Term.SubtermRule
      Term.Subsumption
      Term.Substitution

      Term.Rewriting.Definitions
      Term.Rewriting.Norm

      Term.Narrowing.Variants
      Term.Narrowing.Variants.Check
      Term.Narrowing.Variants.Compute

      Term.Builtin.Convenience
      Term.Builtin.Rules
      Term.Builtin.Signature

      Term.Maude.Process
      Term.Maude.Signature
      Term.Maude.Types
      Term.Maude.Parser

      Term.UnitTests

    other-modules:
      Term.Term
      Term.Classes

      Term.Narrowing.Narrow

      Term.Substitution.SubstVFree
      Term.Substitution.SubstVFresh