name:                safe-coupling
category:            Formal Methods
version:             0.1.0.1
synopsis:            Relational proof system for probabilistic algorithms 
description:         Relational proof system for probabilistic algorithms. Supports two proving methods: upper bound Kantorovich distance between two distributions and establish a boolean relation on samples from two distributions (the latter is stronger).
license:             BSD3
license-file:        LICENSE
author:              Lisa Vasilenko, Niki Vazou
maintainer:          Lisa Vasilenko <vasilliza@gmail.com>
homepage:            https://github.com/nikivazou/safe-coupling
bug-reports:         https://github.com/nikivazou/safe-coupling/issues
copyright:           2020-21 Lisa Vasilenko & Niki Vazou, IMDEA Software Institute
build-type:          Simple
extra-source-files:  ChangeLog.md, README.md
cabal-version:       >=1.10

source-repository head
  type:     git
  location: https://github.com/nikivazou/safe-coupling

library
  exposed-modules:     
       Data.Dist
     , Data.List
     , Data.Derivative

     , Monad.PrM
     , Monad.PrM.Predicates
     , Monad.PrM.Laws

     , Monad.PrM.Relational.TCB.Spec
     , Monad.PrM.Relational.TCB.EDist
     , Monad.PrM.Relational.Theorems

     , Misc.ProofCombinators

-- Toy Examples
     , Examples.ExpDist

-- Bins Example
      , Bins.Bins
      , Bins.Theorem

-- Bins Example using Applicatives
      , ApplicativeBins.Bins
      , ApplicativeBins.Theorem

-- TD Case Study      
     , TD.TD0
     , TD.Lemmata.Relational.Update
     , TD.Lemmata.Relational.Sample
     , TD.Lemmata.Relational.Act
     , TD.Lemmata.Relational.Iterate
     , TD.Theorem

-- SGD Case Study      
     , SGD.SGD 
     , SGD.Theorem 

  build-depends:
       liquid-base                       >= 4.14.0 && < 4.16
     , liquidhaskell                     >= 0.8.10 && < 0.9
     , liquid-containers                 >= 0.6.2 && < 0.7
     , liquid-prelude                    >= 0.8.10 && < 0.9
     , probability                       >= 0.2.7 && < 0.3
     , rest-rewrite                      >= 0.1.1 && < 0.2
  hs-source-dirs:      src
  default-language:    Haskell2010
  ghc-options:  -fplugin=LiquidHaskell 

test-suite safe-coupling-test
  type: exitcode-stdio-1.0
  main-is: Spec.hs
  other-modules:
      Spec.TD0
      Spec.SGD
      Spec.Bins
      Spec.Utils
  hs-source-dirs:
      test
  ghc-options: -threaded -rtsopts -with-rtsopts=-N
  build-tool-depends:
      tasty-discover:tasty-discover
  build-depends:
      liquid-base                      
    , safe-coupling
    , HUnit                            >= 1.6.1 && < 1.7
    , tasty                            >= 1.2.3 && < 1.5
    , tasty-hunit                      >= 0.10.0 && < 1.11
    , probability                      >= 0.2.7 && < 0.3
    , sort                             >= 1.0.0 && < 1.1
  default-language: Haskell2010