Skip to main content

Browse the archive

Raw File
liquid-fixpoint.cabal 
name:               liquid-fixpoint
version:            0.8.0.2
synopsis:           Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
description:
  This package implements an SMTLIB based Horn-Clause\/Logical Implication constraint
  solver used for Liquid Types.
  .
  The package includes:
  .
  1. Types for Expressions, Predicates, Constraints, Solutions
  2. Code for solving constraints
  .
  Requirements
  .
  In addition to the .cabal dependencies you require
  .
  * A Z3 (<http://z3.codeplex.com>) or CVC4 (<http://cvc4.cs.nyu.edu>) binary.
license:            BSD3
license-file:       LICENSE
copyright:          2010-17 Ranjit Jhala, University of California, San Diego.
author:             Ranjit Jhala, Niki Vazou, Eric Seidel
maintainer:         jhala@cs.ucsd.edu
tested-with:        GHC == 7.10.3, GHC == 8.0.1, GHC == 8.4.3, GHC == 8.6.4
category:           Language
homepage:           https://github.com/ucsd-progsys/liquid-fixpoint
build-type:         Simple
extra-source-files: tests/neg/*.fq
                    tests/pos/*.fq
                    unix/Language/Fixpoint/Utils/*.hs
                    win/Language/Fixpoint/Utils/*.hs
                    tests/logs/cur/pin
                    Makefile
cabal-version:      >= 1.10

source-repository head
  type:     git
  location: https://github.com/ucsd-progsys/liquid-fixpoint/

flag devel
  default:     False
  manual:      True
  description: turn on stricter error reporting for development

library
  exposed-modules:  Language.Fixpoint.Defunctionalize
                    Language.Fixpoint.Graph
                    Language.Fixpoint.Graph.Deps
                    Language.Fixpoint.Graph.Indexed
                    Language.Fixpoint.Graph.Partition
                    Language.Fixpoint.Graph.Reducible
                    Language.Fixpoint.Graph.Types
                    Language.Fixpoint.Horn.Parse
                    Language.Fixpoint.Horn.Solve
                    Language.Fixpoint.Horn.Types
                    Language.Fixpoint.Horn.Transformations
                    Language.Fixpoint.Horn.Info
                    Language.Fixpoint.Minimize
                    Language.Fixpoint.Misc
                    Language.Fixpoint.Parse
                    Language.Fixpoint.Smt.Bitvector
                    Language.Fixpoint.Smt.Interface
                    Language.Fixpoint.Smt.Serialize
                    Language.Fixpoint.Smt.Theories
                    Language.Fixpoint.Smt.Types
                    Language.Fixpoint.Solver
                    Language.Fixpoint.Solver.Eliminate
                    Language.Fixpoint.Solver.GradualSolution
                    Language.Fixpoint.Solver.Instantiate
                    Language.Fixpoint.Solver.Monad
                    Language.Fixpoint.Solver.Sanitize
                    Language.Fixpoint.Solver.Solution
                    Language.Fixpoint.Solver.Solve
                    Language.Fixpoint.Solver.TrivialSort
                    Language.Fixpoint.Solver.UniqifyBinds
                    Language.Fixpoint.Solver.UniqifyKVars
                    Language.Fixpoint.Solver.Worklist
                    Language.Fixpoint.SortCheck
                    Language.Fixpoint.Types
                    Language.Fixpoint.Types.Config
                    Language.Fixpoint.Types.Constraints
                    Language.Fixpoint.Types.Environments
                    Language.Fixpoint.Types.Errors
                    Language.Fixpoint.Types.Graduals
                    Language.Fixpoint.Types.Names
                    Language.Fixpoint.Types.PrettyPrint
                    Language.Fixpoint.Types.Refinements
                    Language.Fixpoint.Types.Solutions
                    Language.Fixpoint.Types.Sorts
                    Language.Fixpoint.Types.Spans
                    Language.Fixpoint.Types.Substitutions
                    Language.Fixpoint.Types.Templates
                    Language.Fixpoint.Types.Theories
                    Language.Fixpoint.Types.Triggers
                    Language.Fixpoint.Types.Utils
                    Language.Fixpoint.Types.Visitor
                    Language.Fixpoint.Utils.Files
                    Language.Fixpoint.Utils.Progress
                    Language.Fixpoint.Utils.Statistics
                    Language.Fixpoint.Utils.Trie
                    Text.PrettyPrint.HughesPJ.Compat
  other-modules:    Paths_liquid_fixpoint
  hs-source-dirs:   src
  build-depends:    base                 >= 4.9.1.0 && < 5
                  , ansi-terminal
                  , array
                  , async
                  , attoparsec
                  , binary
                  , boxes
                  , cereal
                  , cmdargs
                  , containers
                  , deepseq
                  , directory
                  , fgl
                  , filepath
                  , ghc-prim
                  , hashable
                  , intern
                  , mtl
                  , parallel
                  , parsec
                  , pretty               >= 1.1.3.1
                  , process
                  , syb
                  , syb
                  , text
                  , text-format
                  , transformers
                  , unordered-containers
  default-language: Haskell98
  ghc-options:      -W -fno-warn-missing-methods -fwarn-missing-signatures

  if flag(devel)
    ghc-options: -Werror

  if !os(windows)
    hs-source-dirs: unix
    build-depends:  ascii-progress >= 0.3

  if os(windows)
    hs-source-dirs: win

executable fixpoint
  main-is:          Fixpoint.hs
  hs-source-dirs:   bin
  build-depends:    base >= 4.9.1.0 && < 5, liquid-fixpoint
  default-language: Haskell98
  ghc-options:      -threaded -W -fno-warn-missing-methods

  if flag(devel)
    ghc-options: -Werror

test-suite test
  type:             exitcode-stdio-1.0
  main-is:          test.hs
  other-modules:    Paths_liquid_fixpoint
  hs-source-dirs:   tests
  build-depends:    base          >= 4.9.1.0 && < 5
                  , containers    >= 0.5
                  , directory
                  , filepath
                  , mtl           >= 2.2.2
                  , process
                  , stm           >= 2.4
                  , tasty         >= 0.10
                  , tasty-ant-xml
                  , tasty-hunit
                  , tasty-hunit   >= 0.9
                  , tasty-rerun   >= 1.1.12
                  , transformers  >= 0.5
  default-language: Haskell98
  ghc-options:      -threaded

  if flag(devel)
    ghc-options: -Werror

test-suite testparser
  type:             exitcode-stdio-1.0
  main-is:          testParser.hs
  hs-source-dirs:   tests
  build-depends:    base            >= 4.9.1.0 && < 5
                  , liquid-fixpoint
                  , tasty           >= 0.10
                  , tasty-hunit
                  , tasty-hunit     >= 0.9
  default-language: Haskell98
  ghc-options:      -threaded

  if flag(devel)
    ghc-options: -Werror
back to top