cabal-version:          3.8
name:                   claferIG
Version:                0.5.8
Synopsis:               claferIG is an interactive tool that generates instances of Clafer models.
Description:            Clafer is a powerful (equivalent to first-order predicate logic) yet lightweight structural modeling language. Despite simplicity and conciseness of Clafer, writing correct models remains challenging due to hard-to-predict interactions among all constraints expressed in the model. Clafer instance generator (ClaferIG) is an interactive tool that generates instances and counter examples of concrete clafers in a Clafer model. If the concrete clafers do not have contradicting constraints, the generator produces valid instance data. Otherwise, the generator produces an unsatisfiable core which included all contradicting constraints and generates a counter example by removing one constraint from the core. The generator can potentially produce many instances if the concrete clafers are not fully specialized. The generator produces different instances on-demand. With these capabilities, the instance generator can be used for debugging models: checking the consistency of the model and detecting under- and overconstraining of the model. The instance generator can also be used programmatically via API (the command line and interactive session interfaces only use the API).
Homepage:               http://clafer.org
License:                MIT
License-file:           LICENSE
Author:                 Jimmy Liang, Michal Antkiewicz, Luke Michael Brown
Maintainer:             Michal Antkiewicz <michal.antkiewicz@uwaterloo.ca>
Stability:              Experimental
Category:               Model
Build-type:             Simple
Tested-with:            GHC == 9.6.7 || == 9.12.4
data-files:             README.md
                      , alloyIG.jar
                      , Makefile
                      , stack.yaml
extra-doc-files:        CHANGES.md
source-repository head
    type:               git
    location:           https://github.com/gsdlab/claferIG.git

flag model-tests
    description:        Build the model-tests test suite, which generates instances of the models in
                        test/positive with Alloy. The models and alloy6.2.0.jar are not part of the
                        package, so it can only be built in a checkout of the repository.
    default:            False
    manual:             True

common shared-deps
    default-language:   Haskell2010
    ghc-options:        -Wall
    build-depends:      base >= 4.18.3.0 && < 5
                      , containers >= 0.5.5.1
                      , directory >= 1.2.1.0

executable claferIG
    import:             shared-deps
    Main-is:            Main.hs
    Build-depends:      filepath >= 1.3.0.2
                      , cmdargs >= 0.10.12
                      , clafer == 0.5.8
                      , claferIG == 0.5.8
    other-modules:      Paths_claferIG
    autogen-modules:    Paths_claferIG
    Hs-Source-Dirs:     src-cmd
    ghc-options:        -Wall -fno-warn-orphans

library
    import:             shared-deps
    build-depends:      transformers >= 0.6
                      , mtl >= 2.1.3.1
                      , executable-path >= 0.0.3
                      , haskeline >= 0.8
                      , process >= 1.2.0.0
                      , parsec >= 3.1.5
                      , exceptions >= 0.10
                      , aeson >= 1.1.2.0
                      , string-conversions >= 0.3.0.3
                      , clafer == 0.5.8

    if os(windows)
      build-depends:  HaXml == 1.24
    else
      build-depends:  HaXml >= 1.25.3

    hs-source-dirs:     src
    ghc-options:        -Wall -fno-warn-orphans
    exposed-modules:    Language.Clafer.IG.AlloyIGInterface
                      , Language.Clafer.IG.ClaferIG
                      , Language.Clafer.IG.ClaferModel
                      , Language.Clafer.IG.CommandLine
                      , Language.Clafer.IG.CommandLineParser
                      , Language.Clafer.IG.Constraints
                      , Language.Clafer.IG.JSONGenerator
                      , Language.Clafer.IG.Process
                      , Language.Clafer.IG.Solution
                      , Language.Clafer.IG.SolutionView
                      , Language.Clafer.IG.Sugarer
    other-modules:      Paths_claferIG
    autogen-modules:    Paths_claferIG
Test-Suite test-suite
    type:               exitcode-stdio-1.0
    default-language:   Haskell2010
    main-is:            test-suite.hs
    hs-source-dirs:     test
    build-depends:      base >= 4.18.3.0 && < 5
                      , tasty >= 0.10.1.2
                      , tasty-hunit >= 0.9.2
                      , tasty-th >= 0.1.3
                      , claferIG == 0.5.8
    other-modules:      Paths_claferIG
    autogen-modules:    Paths_claferIG
    ghc-options:        -Wall -fno-warn-orphans

Test-Suite model-tests
    type:               exitcode-stdio-1.0
    default-language:   Haskell2010
    main-is:            model-tests.hs
    hs-source-dirs:     test
    if !flag(model-tests)
        buildable:      False
    build-depends:      base >= 4.18.3.0 && < 5
                      , directory >= 1.2.1.0
                      , containers >= 0.5.5.1
                      , filepath >= 1.3.0.2
                      , cmdargs >= 0.10.12
                      , tasty >= 0.10.1.2
                      , tasty-hunit >= 0.9.2
                      , tasty-th >= 0.1.3
                      , clafer == 0.5.8
                      , claferIG == 0.5.8
    -- the tests run in parallel, on 8 cores: with GHC 9.12 and 16 or more, the parallel GC hangs
    ghc-options:        -Wall -fno-warn-orphans -threaded -rtsopts "-with-rtsopts=-N8"