name: tamarin-prover-term
cabal-version: >= 1.8
build-type: Simple
version: 0.8.5.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-options: -Wall -fwarn-tabs
ghc-prof-options: -auto-all
build-depends:
base == 4.*
, mtl == 2.*
, bytestring >= 0.9
, attoparsec == 0.10.*
, containers >= 0.4.2
, dlist == 0.5.*
, safe >= 0.2
, split == 0.1.*
, parsec == 3.1.*
, syb >= 0.3.3
, directory >= 1.1
, process >= 1.1
, deepseq >= 1.3
, binary == 0.*
, derive == 2.*
, HUnit == 1.*
, tamarin-prover-utils >= 0.8.5 && < 0.9
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.Term.Classes
Term.Term.Raw
Term.Term.FunctionSymbols
Term.Narrowing.Narrow
Term.Substitution.SubstVFree
Term.Substitution.SubstVFresh