Expressions and Formulae a la carte

Latest on Hackage:0.4.2

This package is not currently in any snapshots. If you're interested in using it, we recommend adding it to Stackage Nightly. Doing so will make builds more reliable, and allow to host generated Haddocks.

BSD3 licensed by Jakub Daniel

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


Change Log


  • Allow a wide range of dynamically sorted values (not just expressions)
  • Utility for extracting array accesses


  • Utility for extracting constants from expressions


  • Cleanup, GHC 8.6


  • Add embed and restrict to convert between expression languages


  • Bump dependencies


  • Bump dependencies


  • Added simple utility function toDynamicallySorted


  • GHC 8.4 compatibility


  • Bump dependencies, fix equality, tweak readme


  • Bump dependencies


  • Extracting variables occurring in expression
  • Distinguish quantifier-free expressions
  • Convert to negation normal form
  • Convert to prenex form
  • Convert to flat form (select and store have only variables or constants as arguments)
  • Replace store with an instance of its axiomatization


  • Foldable with sort index
  • Traversable with sort index


  • Parsing
  • Equality of expressions
  • Expression substitution


  • Sorted Expressions à la Carte
Used by 1 package:
comments powered byDisqus