copilot-theorem-2.2.1: copilot-theorem.cabal

cabal-version             : >= 1.10
name                      : copilot-theorem
synopsis: k-induction for Copilot.
description:

  Some tools to prove properties on Copilot programs with k-induction model
  checking.

version                   : 2.2.1
license                   : BSD3
license-file              : LICENSE
maintainer                : jonathan.laurent@ens.fr
stability                 : Experimental
category                  : Language, Embedded
build-type                : Simple
extra-source-files        : README.md

author                    : Jonathan Laurent

library
  default-language        : Haskell2010
  hs-source-dirs          : src

  ghc-options             : -Wall -fwarn-tabs
                            -fno-warn-name-shadowing
                            -fno-warn-unused-binds
                            -fno-warn-missing-signatures
                            -fcontext-stack=100

                            -fpackage-trust
                            -trust=array
                            -trust=base
                            -trust=containers
                            -trust=copilot-core
                            -trust=directory
                            -trust=exceptions
                            -trust=process
                            -trust=random
                            -trust=unix

  build-depends           : base >= 4.0 && < 5
                          , copilot-core == 2.2.1
                          , mtl
                          , containers
                          , pretty
                          , process
                          , directory
                          , parsec
                          , data-default
                          , bimap
                          , xml
                          , random
                          , transformers
                          , smtlib2 >= 0.3 && < 1.0
                          , ansi-terminal

  exposed-modules         : Copilot.Theorem
                          , Copilot.Theorem.Prove
                          , Copilot.Theorem.Kind2
                          , Copilot.Theorem.Prover.SMT
                          , Copilot.Theorem.Prover.Z3
                          , Copilot.Theorem.Kind2.Prover

  other-modules           : Copilot.Theorem.Tactics

                          , Copilot.Theorem.IL
                          , Copilot.Theorem.IL.PrettyPrint
                          , Copilot.Theorem.IL.Spec
                          , Copilot.Theorem.IL.Translate
                          , Copilot.Theorem.IL.Transform

                          , Copilot.Theorem.Kind2.AST
                          , Copilot.Theorem.Kind2.Output
                          , Copilot.Theorem.Kind2.PrettyPrint
                          , Copilot.Theorem.Kind2.Translate

                          , Copilot.Theorem.Prover.SMTIO
                          , Copilot.Theorem.Prover.SMTLib
                          , Copilot.Theorem.Prover.TPTP
                          , Copilot.Theorem.Prover.Backend

                          , Copilot.Theorem.Misc.Error
                          , Copilot.Theorem.Misc.SExpr
                          , Copilot.Theorem.Misc.Utils

                          , Copilot.Theorem.TransSys
                          , Copilot.Theorem.TransSys.Cast
                          , Copilot.Theorem.TransSys.PrettyPrint
                          , Copilot.Theorem.TransSys.Renaming
                          , Copilot.Theorem.TransSys.Spec
                          , Copilot.Theorem.TransSys.Transform
                          , Copilot.Theorem.TransSys.Translate
                          , Copilot.Theorem.TransSys.Invariants
                          , Copilot.Theorem.TransSys.Operators
                          , Copilot.Theorem.TransSys.Type