expressions: Expressions and Formulas a la carte
This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.
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
Properties
| Versions | 0.1.1, 0.1.1, 0.1.2, 0.1.3, 0.1.4, 0.1.5, 0.1.6, 0.1.7, 0.1.8, 0.1.9, 0.2, 0.3, 0.3.1, 0.4, 0.4.1, 0.4.2, 0.5 |
|---|---|
| Change log | ChangeLog.md |
| Dependencies | attoparsec (>=0.13 && <0.14), base (>=4.9 && <4.10), containers (>=0.5.7 && <0.5.8), lattices (>=1.6 && <1.7), singletons (>=2.2 && <2.3), text (>=1.2 && <1.3), transformers (>=0.5.2 && <0.5.3) [details] |
| License | BSD-3-Clause |
| Copyright | Copyright (C) 2017 Jakub Daniel |
| Author | Jakub Daniel |
| Maintainer | jakub.daniel@protonmail.com |
| Category | Data, Logic, Math |
| Source repo | head: git clone https://github.com/jakubdaniel/expressions.git |
| Uploaded | by jakubdaniel at 2017-09-06T13:55:50Z |
Modules
[Index]
Downloads
- expressions-0.1.1.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)
Maintainer's Corner
Package maintainers
For package maintainers and hackage trustees