name:                liquid-fixpoint
version:             0.2.0.0
synopsis:            Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
homepage:            https://github.com/ucsd-progsys/liquid-fixpoint
license:             BSD3
license-file:        LICENSE
author:              Ranjit Jhala, Niki Vazou, Eric Seidel
maintainer:          jhala@cs.ucsd.edu
category:            Language
build-type:          Custom 
cabal-version:       >=1.8

description:     This package is a Haskell wrapper to the SMTLIB-based
                 Horn-Clause/Logical Implication constraint solver used
                 for Liquid Types. 
                 .
                 The solver itself is written in Ocaml. 
                 .
                 The package includes: 
                 .
                 1. Types for Expressions, Predicates, Constraints, Solutions
                 .
                 2. Code for serializing the above
                 .
                 3. Code for parsing the results from the fixpoint.native binary
                 .
                 4. The Ocaml fixpoint code
                 .
                 5. (Deprecated) Z3 binaries if you want to link against the API.
                 .
                 Requirements
                 .
                 In addition to the .cabal dependencies you require 
                 .
                 - A Recent Ocaml compiler
                 .
                 - A Z3 Binary (<http://z3.codeplex.com>)

Extra-Source-Files: configure
                  , external/fixpoint/Makefile
                  , external/fixpoint/*.ml
                  , external/fixpoint/smtZ3.mem.ml
                  , external/fixpoint/smtZ3.nomem.ml
                  , external/fixpoint/*.mli
                  , external/fixpoint/*.mll
                  , external/fixpoint/*.mly
                  , external/misc/*.ml
                  , external/misc/*.mli
                  , external/ocamlgraph/.depend
                  , external/ocamlgraph/Makefile
                  , external/ocamlgraph/Makefile.in
                  , external/ocamlgraph/META
                  , external/ocamlgraph/META.in
                  , external/ocamlgraph/configure
                  , external/ocamlgraph/configure.in
                  , external/ocamlgraph/lib/*.ml
                  , external/ocamlgraph/lib/*.mli
                  , external/ocamlgraph/src/*.ml
                  , external/ocamlgraph/src/*.mli
                  , external/ocamlgraph/src/*.mll
                  , external/ocamlgraph/src/*.mly
                  , external/z3/include/*.h
                  , external/z3/lib/libz3-a-32b
                  , external/z3/lib/libz3-a-64b
                  , external/z3/lib/libz3-so-32b
                  , external/z3/lib/libz3-so-64b
                  , external/z3/ocaml/build-lib.sh
                  , external/z3/ocaml/z3.ml
                  , external/z3/ocaml/*.c

Flag z3mem
  Description: Link to Z3
  Default:     False

Source-Repository head
  Type:        git
  Location:    https://github.com/ucsd-progsys/liquid-fixpoint/

-- FIXME: This is a terrible hack. We build Fixpoint.hs *twice*, once
-- targeting fixpoint.native so we can then *clobber* it with the
-- OCaml fixpoint.native. This is required for cabal-install to detect
-- fixpoint.native as an executable, and properly symlink it when
-- asked.
Executable fixpoint.native
  Main-is: Fixpoint.hs
  Build-Depends: base >= 4 && < 5
               , array
               , syb
               , cmdargs
               , ansi-terminal
               , bifunctors
               , bytestring
               , containers
               , deepseq
               , directory
               , filemanip
               , filepath
               , mtl
               , parsec
               , pretty
               , process
               , syb
               , text
               , hashable
               , unordered-containers
               , text-format
               , liquid-fixpoint
               

Executable fixpoint
  Main-is:       Fixpoint.hs
  Build-Depends: base >= 4 && < 5
               , array
               , syb
               , cmdargs
               , ansi-terminal
               , bifunctors
               , bytestring
               , containers
               , deepseq
               , directory
               , filemanip
               , filepath
               , mtl
               , parsec
               , pretty
               , process
               , syb
               , text
               , hashable
               , unordered-containers
               , text-format
               , liquid-fixpoint

Library
  hs-source-dirs:  src
  Exposed-Modules: Language.Fixpoint.Names,
                   Language.Fixpoint.Files,
                   Language.Fixpoint.Errors,
                   Language.Fixpoint.Config,
                   Language.Fixpoint.Types,
                   Language.Fixpoint.Sort,
                   Language.Fixpoint.Interface, 
                   Language.Fixpoint.Parse,
                   Language.Fixpoint.PrettyPrint,
                   Language.Fixpoint.SmtLib2,
                   Language.Fixpoint.Misc
  
  Build-Depends: base >= 4 && < 5
               , array
               , attoparsec
               , syb
               , cmdargs
               , ansi-terminal
               , bifunctors
               , bytestring
               , containers
               , deepseq
               , directory
               , filemanip
               , filepath
               , ghc-prim
               , intern
               , mtl
               , parsec
               , pretty
               , process
               , syb
               , text
               , transformers
               , hashable
               , unordered-containers
               , text-format