name: tamarin-prover-term
cabal-version: >= 1.8
build-type: Simple
version: 0.1.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
----------------------
-- library stanzas
----------------------
library
build-depends:
base == 4.*
, mtl == 2.0.*
, containers == 0.4.*
, dlist == 0.5.*
, safe == 0.2.*
, split == 0.1.*
, parsec == 3.1.*
, syb >= 0.3.3 && < 0.4
, directory == 1.1.*
, process == 1.0.*
, deepseq == 1.1.*
, binary == 0.5.*
, derive == 2.5.*
, tamarin-prover-utils == 0.1.*
hs-source-dirs: src
exposed-modules:
Term.Unification
Term.LTerm
Term.Positions
Term.SubtermRule
Term.Subsumption
Term.Substitution
Term.Rewriting.Norm
Term.Rewriting.NormAC
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.Types
other-modules:
Term.Term
Term.Classes
Term.Narrowing.Narrow
Term.Substitution.SubstVFree
Term.Substitution.SubstVFresh