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.
  .
  Copilot is a stream (i.e., infinite lists) domain-specific language (DSL) in
  Haskell that compiles into embedded C.  Copilot contains an interpreter,
  multiple back-end compilers, and other verification tools.
  .
  A tutorial, examples, and other information are available at
  <https://copilot-language.github.io>.


version                   : 3.2.1
license                   : BSD3
license-file              : LICENSE
maintainer                : jonathan.laurent@ens.fr
homepage                  : https://copilot-language.github.io
bug-reports               : https://github.com/Copilot-Language/copilot-theorem/issues
stability                 : Experimental
category                  : Language, Embedded
build-type                : Simple
extra-source-files        : README.md
                          , CHANGELOG

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
                            -- -- -trust=parsec
                            -- -trust=bytestring
                            -- -- -trust=text

  build-depends           : base          >= 4.9 && < 5
                          , ansi-terminal >= 0.8 && < 0.10
                          , bimap         >= 0.3 && < 0.4
                          , bv-sized      >= 1.0.2 && < 1.1
                          , containers    >= 0.4 && < 0.7
                          , data-default  >= 0.7 && < 0.8
                          , directory     >= 1.3 && < 1.4
                          , filepath      >= 1.4.2 && < 1.5
                          , mtl           >= 2.0 && < 2.3
                          , panic         >= 0.4.0 && < 0.5
                          , parsec        >= 2.0 && < 3.2
                          , parameterized-utils >= 2.1.1 && < 2.2
                          , pretty        >= 1.0 && < 1.2
                          , process       >= 1.6 && < 1.7
                          , random        >= 1.1 && < 1.2
                          , transformers  >= 0.5 && < 0.6
                          , xml           >= 1.3 && < 1.4
                          , what4         >= 1.0 && < 1.1

                          , copilot-core  >= 3.2.1 && < 3.3

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

  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