name:                expressions
version:             0.5
synopsis:            Expressions and Formulae a la carte
description:
  This package is aimed at providing means of fixing a first-order language and
  declaring sorted expressions and formulae, the types ensure the declared
  expressions fall within the language.
  .
  This package pre-defines the common logical symbols for conjunction,
  disjunction, negation, and universal and existential quantification as well
  as some specific non-logical symbols such as equality, addition of linear
  integer arithmetic, and other. Common languages such as Lia and ALia
  (standard linear integer arithmetic and linear integer arithmetic with
  arrays) come included.
  .
  An example of a formula declaration:
  .
  > -- Let's state that zero is successor to no integer (while this would be
  > -- true for non-negative integers, stated this way it is clearly false, but
  > -- it still is a well-formed first-order statement)
  >
  > forall [var "x" :: Var 'IntegralSort] (cnst 0 ./=. var "x" .+. cnst 1) :: Lia 'BooleanSort
  .
  Let's see what declarations the library rejects:
  .
  > (var "x" :: Lia 'BooleanSort) .=. (var "y" :: Lia 'IntegralSort)
  > (var "x" :: Lia 'BooleanSort) .=. (var "y" :: ALia 'BooleanSort)
  > forall [var "x" :: Var 'IntegralSort] true :: QFLia 'BooleanSort

license:             BSD3
license-file:        LICENSE
author:              Jakub Daniel
maintainer:          jakub.daniel@protonmail.com
copyright:           Copyright (C) 2017 Jakub Daniel
category:            Data, Logic, Math
build-type:          Simple
extra-source-files:  ChangeLog.md
cabal-version:       >=1.10

source-repository head
  type:     git
  location: https://github.com/jakubdaniel/expressions.git

library
  exposed-modules:     Data.Expression,
                       Data.Expression.Arithmetic,
                       Data.Expression.Array,
                       Data.Expression.Equality,
                       Data.Expression.IfThenElse,
                       Data.Expression.Parser,
                       Data.Expression.Sort,
                       Data.Expression.Utils.Indexed.Eq,
                       Data.Expression.Utils.Indexed.Foldable,
                       Data.Expression.Utils.Indexed.Functor,
                       Data.Expression.Utils.Indexed.Show,
                       Data.Expression.Utils.Indexed.Sum,
                       Data.Expression.Utils.Indexed.Traversable
  other-extensions:    DataKinds,
                       FlexibleContexts,
                       FlexibleInstances,
                       GADTs,
                       KindSignatures,
                       MultiParamTypeClasses,
                       OverloadedStrings,
                       RankNTypes,
                       ScopedTypeVariables,
                       TemplateHaskell,
                       TypeFamilies,
                       TypeInType,
                       TypeOperators,
                       TypeSynonymInstances,
                       UndecidableInstances
  build-depends:       attoparsec >=0.13 && <0.14,
                       base >=4.11 && <4.13,
                       containers >=0.5.7 && <0.7,
                       free >=4.2 && <5.2,
                       lattices >=2 && <2.1,
                       singletons >=2.2 && <2.6,
                       text >=1.2 && <1.3,
                       transformers >=0.5.2 && <0.6
  hs-source-dirs:      src
  default-language:    Haskell2010
  ghc-options:         -Wall -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns

test-suite test
  type:                exitcode-stdio-1.0
  build-depends:       base,
                       expressions,
                       singletons,
                       text
  hs-source-dirs:      test
  main-is:             Main.hs
  default-language:    Haskell2010
  ghc-options:         -Wall -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns