inversion-plugin.cabal

cabal-version: 3.0
name:          inversion-plugin
synopsis:      A compiler plugin to provide automatic inversion
version:       2.0
license:       BSD-3-Clause
license-file:  LICENSE
copyright:     (c) 2020-2023, Finn Teegen, Kai-Oliver Prott, Niels Bunkenburg
maintainer:    fte@informatik.uni-kiel.de
author:        Finn Teegen, Kai-Oliver Prott, Niels Bunkenburg
category:      Language
build-type:    Simple
stability:     experimental
description:   A very nice plugin for the GHC that automatically derives inverse functions.

extra-source-files:
  README.md

source-repository head
  type:     git
  location: https://github.com/cau-placc/inversion-plugin

flag use-sbv {
  Description: Use SBV
  Default:     False
  Manual:      True
}
flag use-what4 {
  Description: Use What4
  Default:     True
  Manual:      True
}

flag use-cvc {
  Description: Use CVC4/5
  Default:     False
  Manual:      True
}

flag use-z3 {
  Description: Use Z3
  Default:     True
  Manual:      True
}

flag use-dfs {
  Description: Perform depth-first search
  Default:     False
  Manual:      True
}

flag use-iddfs {
  Description: Perform iterative-deepening depth-first search
  Default:     False
  Manual:      True
}

flag use-bfs {
  Description: Perform breadth-first search
  Default:     True
  Manual:      True
}

flag use-cs {
  Description: Perform concurrent search
  Default:     False
  Manual:      True
}

flag use-ps {
  Description: Perform parallel search
  Default:     False
  Manual:      True
}

common deps
  hs-source-dirs: src
  build-depends:
    base                ^>= 4.16.1.0,
    ghc                 ^>= 9.2.2,
    ghc-prim            -any,
    template-haskell    -any,
    bytestring          -any,
    containers          -any,
    deque               ^>= 0.4.3,
    transformers        -any,
    ghc-tcplugin-api    -any,
    mtl                 -any,
    syb                 -any,
    extra               -any,
    split               -any,
    tree-monad          -any,
    parallel-tree-search -any,
    ChasingBottoms      -any,
    kan-extensions      -any,
    sbv                 -any,
    what4               -any,
    parameterized-utils -any,
    libBF               -any,
    text                -any,
    bv-sized            -any,
    OneTuple            -any
  ghc-options: -Wall -Wincomplete-uni-patterns
  if flag(use-sbv)
    cpp-options: -DUSE_SBV -UUSE_WHAT4
  if flag(use-what4)
    cpp-options: -DUSE_WHAT4 -UUSE_SBV
  if flag(use-cvc)
    cpp-options: -DUSE_CVC -UUSE_Z3
  if flag(use-z3)
    cpp-options: -DUSE_Z3 -UUSE_CVC
  if flag(use-dfs)
    cpp-options: -DUSE_DFS -UUSE_IDDFS -UUSE_BFS -UUSE_CS -UUSE_PS
  if flag(use-iddfs)
    cpp-options: -DUSE_IDDFS -UUSE_DFS -UUSE_BFS -UUSE_CS -UUSE_PS
  if flag(use-bfs)
    cpp-options: -DUSE_BFS -UUSE_DFS -UUSE_IDDFS -UUSE_CS -UUSE_PS
  if flag(use-cs)
    cpp-options: -DUSE_CS -UUSE_DFS -UUSE_IDDFS -UUSE_BFS -UUSE_PS
  if flag(use-ps)
    cpp-options: -DUSE_PS -UUSE_CS -UUSE_DFS -UUSE_IDDFS -UUSE_BFS
  default-language: Haskell2010
  other-extensions:
    DefaultSignatures,
    DeriveAnyClass,
    DeriveDataTypeable,
    DeriveFunctor,
    DeriveGeneric,
    EmptyCase,
    EmptyDataDeriving,
    ExistentialQuantification,
    FlexibleContexts,
    FlexibleInstances,
    FunctionalDependencies,
    GeneralizedNewtypeDeriving,
    LambdaCase,
    MultiParamTypeClasses,
    OverloadedStrings,
    RankNTypes,
    RecursiveDo,
    ScopedTypeVariables,
    StandaloneDeriving,
    TemplateHaskell,
    TupleSections,
    TypeFamilies,
    TypeOperators,
    UndecidableInstances
  other-modules:
    Plugin.Dump
    Plugin.Effect.SolverLibrary.SBV
    Plugin.Effect.SolverLibrary.What4
    Plugin.Effect.TH
    Plugin.Effect.Tree
    Plugin.Effect.Util
    Plugin.Primitives
    Plugin.Trans.Class
    Plugin.Trans.ClsInst
    Plugin.Trans.Coerce
    Plugin.Trans.Constr
    Plugin.Trans.CreateSyntax
    Plugin.Trans.DictInstFun
    Plugin.Trans.Expr
    Plugin.Trans.FunWiredIn
    Plugin.Trans.Import
    Plugin.Trans.LExprEQ
    Plugin.Trans.Pat
    Plugin.Trans.PatternMatching
    Plugin.Trans.Preprocess
    Plugin.Trans.Record
    Plugin.Trans.TyCon
    Plugin.Trans.Type
    Plugin.Trans.Util
    Plugin.Trans.Var
    SBVTest
    What4Test

library
  import: deps
  exposed-modules:
    Plugin.BuiltIn
    Plugin.BuiltIn.Char
    Plugin.BuiltIn.Identity
    Plugin.BuiltIn.Primitive
    Plugin.Effect.Annotation
    Plugin.Effect.Monad
    Plugin.InversionPlugin
    Plugin.Lifted
    Plugin.Prelude
    Plugin.Trans.TysWiredIn

test-suite tests
  import:         deps
  type:           detailed-0.9
  hs-source-dirs: test
  test-module:    Tests
  other-modules:
    SemanticTests
    Tests.Definitions
    Tests.QuickCheckInverse

    Plugin.BuiltIn
    Plugin.Effect.Monad
    Plugin.Effect.Annotation
    Plugin.InversionPlugin
    Plugin.Prelude
  build-depends:
    inversion-plugin,
    process    ^>= 1.6.5.0,
    filepath   ^>= 1.4.2.1,
    directory  ^>= 1.3.3.0,
    Cabal      ^>= 3.2.0.0,
    QuickCheck ^>= 2.14.2