diff --git a/.gitignore b/.gitignore index 4d207b7..d7e4614 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,2 @@ .stack-work - +dist-newstyle diff --git a/LICENSE b/LICENSE index 3265aa9..22953c3 100644 --- a/LICENSE +++ b/LICENSE @@ -1,21 +1,291 @@ -MIT License + EUROPEAN UNION PUBLIC LICENCE v. 1.2 + EUPL © the European Union 2007, 2016 -Copyright (c) 2017 Joshua Moerman +This European Union Public Licence (the ‘EUPL’) applies to the Work (as +defined below) which is provided under the terms of this Licence. Any use of +the Work, other than as authorised under this Licence is prohibited (to the +extent such use is covered by a right of the copyright holder of the Work). -Permission is hereby granted, free of charge, to any person obtaining a copy -of this software and associated documentation files (the "Software"), to deal -in the Software without restriction, including without limitation the rights -to use, copy, modify, merge, publish, distribute, sublicense, and/or sell -copies of the Software, and to permit persons to whom the Software is -furnished to do so, subject to the following conditions: +The Work is provided under the terms of this Licence when the Licensor (as +defined below) has placed the following notice immediately following the +copyright notice for the Work: -The above copyright notice and this permission notice shall be included in all -copies or substantial portions of the Software. + Licensed under the EUPL -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR -IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, -FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE -AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER -LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, -OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE -SOFTWARE. +or has expressed by any other means his willingness to license under the EUPL. + +1. Definitions + +In this Licence, the following terms have the following meaning: + +- ‘The Licence’: this Licence. + +- ‘The Original Work’: the work or software distributed or communicated by the + Licensor under this Licence, available as Source Code and also as Executable + Code as the case may be. + +- ‘Derivative Works’: the works or software that could be created by the + Licensee, based upon the Original Work or modifications thereof. This + Licence does not define the extent of modification or dependence on the + Original Work required in order to classify a work as a Derivative Work; + this extent is determined by copyright law applicable in the country + mentioned in Article 15. + +- ‘The Work’: the Original Work or its Derivative Works. + +- ‘The Source Code’: the human-readable form of the Work which is the most + convenient for people to study and modify. + +- ‘The Executable Code’: any code which has generally been compiled and which + is meant to be interpreted by a computer as a program. + +- ‘The Licensor’: the natural or legal person that distributes or communicates + the Work under the Licence. + +- ‘Contributor(s)’: any natural or legal person who modifies the Work under + the Licence, or otherwise contributes to the creation of a Derivative Work. + +- ‘The Licensee’ or ‘You’: any natural or legal person who makes any usage of + the Work under the terms of the Licence. + +- ‘Distribution’ or ‘Communication’: any act of selling, giving, lending, + renting, distributing, communicating, transmitting, or otherwise making + available, online or offline, copies of the Work or providing access to its + essential functionalities at the disposal of any other natural or legal + person. + +2. Scope of the rights granted by the Licence + +The Licensor hereby grants You a worldwide, royalty-free, non-exclusive, +sublicensable licence to do the following, for the duration of copyright +vested in the Original Work: + +- use the Work in any circumstance and for all usage, +- reproduce the Work, +- modify the Work, and make Derivative Works based upon the Work, +- communicate to the public, including the right to make available or display + the Work or copies thereof to the public and perform publicly, as the case + may be, the Work, +- distribute the Work or copies thereof, +- lend and rent the Work or copies thereof, +- sublicense rights in the Work or copies thereof. + +Those rights can be exercised on any media, supports and formats, whether now +known or later invented, as far as the applicable law permits so. + +In the countries where moral rights apply, the Licensor waives his right to +exercise his moral right to the extent allowed by law in order to make +effective the licence of the economic rights here above listed. + +The Licensor grants to the Licensee royalty-free, non-exclusive usage rights +to any patents held by the Licensor, to the extent necessary to make use of +the rights granted on the Work under this Licence. + +3. Communication of the Source Code + +The Licensor may provide the Work either in its Source Code form, or as +Executable Code. If the Work is provided as Executable Code, the Licensor +provides in addition a machine-readable copy of the Source Code of the Work +along with each copy of the Work that the Licensor distributes or indicates, +in a notice following the copyright notice attached to the Work, a repository +where the Source Code is easily and freely accessible for as long as the +Licensor continues to distribute or communicate the Work. + +4. Limitations on copyright + +Nothing in this Licence is intended to deprive the Licensee of the benefits +from any exception or limitation to the exclusive rights of the rights owners +in the Work, of the exhaustion of those rights or of other applicable +limitations thereto. + +5. Obligations of the Licensee + +The grant of the rights mentioned above is subject to some restrictions and +obligations imposed on the Licensee. Those obligations are the following: + +Attribution right: The Licensee shall keep intact all copyright, patent or +trademarks notices and all notices that refer to the Licence and to the +disclaimer of warranties. The Licensee must include a copy of such notices and +a copy of the Licence with every copy of the Work he/she distributes or +communicates. The Licensee must cause any Derivative Work to carry prominent +notices stating that the Work has been modified and the date of modification. + +Copyleft clause: If the Licensee distributes or communicates copies of the +Original Works or Derivative Works, this Distribution or Communication will be +done under the terms of this Licence or of a later version of this Licence +unless the Original Work is expressly distributed only under this version of +the Licence — for example by communicating ‘EUPL v. 1.2 only’. The Licensee +(becoming Licensor) cannot offer or impose any additional terms or conditions +on the Work or Derivative Work that alter or restrict the terms of the +Licence. + +Compatibility clause: If the Licensee Distributes or Communicates Derivative +Works or copies thereof based upon both the Work and another work licensed +under a Compatible Licence, this Distribution or Communication can be done +under the terms of this Compatible Licence. For the sake of this clause, +‘Compatible Licence’ refers to the licences listed in the appendix attached to +this Licence. Should the Licensee's obligations under the Compatible Licence +conflict with his/her obligations under this Licence, the obligations of the +Compatible Licence shall prevail. + +Provision of Source Code: When distributing or communicating copies of the +Work, the Licensee will provide a machine-readable copy of the Source Code or +indicate a repository where this Source will be easily and freely available +for as long as the Licensee continues to distribute or communicate the Work. + +Legal Protection: This Licence does not grant permission to use the trade +names, trademarks, service marks, or names of the Licensor, except as required +for reasonable and customary use in describing the origin of the Work and +reproducing the content of the copyright notice. + +6. Chain of Authorship + +The original Licensor warrants that the copyright in the Original Work granted +hereunder is owned by him/her or licensed to him/her and that he/she has the +power and authority to grant the Licence. + +Each Contributor warrants that the copyright in the modifications he/she +brings to the Work are owned by him/her or licensed to him/her and that he/she +has the power and authority to grant the Licence. + +Each time You accept the Licence, the original Licensor and subsequent +Contributors grant You a licence to their contributions to the Work, under the +terms of this Licence. + +7. Disclaimer of Warranty + +The Work is a work in progress, which is continuously improved by numerous +Contributors. It is not a finished work and may therefore contain defects or +‘bugs’ inherent to this type of development. + +For the above reason, the Work is provided under the Licence on an ‘as is’ +basis and without warranties of any kind concerning the Work, including +without limitation merchantability, fitness for a particular purpose, absence +of defects or errors, accuracy, non-infringement of intellectual property +rights other than copyright as stated in Article 6 of this Licence. + +This disclaimer of warranty is an essential part of the Licence and a +condition for the grant of any rights to the Work. + +8. Disclaimer of Liability + +Except in the cases of wilful misconduct or damages directly caused to natural +persons, the Licensor will in no event be liable for any direct or indirect, +material or moral, damages of any kind, arising out of the Licence or of the +use of the Work, including without limitation, damages for loss of goodwill, +work stoppage, computer failure or malfunction, loss of data or any commercial +damage, even if the Licensor has been advised of the possibility of such +damage. However, the Licensor will be liable under statutory product liability +laws as far such laws apply to the Work. + +9. Additional agreements + +While distributing the Work, You may choose to conclude an additional +agreement, defining obligations or services consistent with this Licence. +However, if accepting obligations, You may act only on your own behalf and on +your sole responsibility, not on behalf of the original Licensor or any other +Contributor, and only if You agree to indemnify, defend, and hold each +Contributor harmless for any liability incurred by, or claims asserted against +such Contributor by the fact You have accepted any warranty or additional +liability. + +10. Acceptance of the Licence + +The provisions of this Licence can be accepted by clicking on an icon ‘I +agree’ placed under the bottom of a window displaying the text of this Licence +or by affirming consent in any other similar way, in accordance with the rules +of applicable law. Clicking on that icon indicates your clear and irrevocable +acceptance of this Licence and all of its terms and conditions. + +Similarly, you irrevocably accept this Licence and all of its terms and +conditions by exercising any rights granted to You by Article 2 of this +Licence, such as the use of the Work, the creation by You of a Derivative Work +or the Distribution or Communication by You of the Work or copies thereof. + +11. Information to the public + +In case of any Distribution or Communication of the Work by means of +electronic communication by You (for example, by offering to download the Work +from a remote location) the distribution channel or media (for example, a +website) must at least provide to the public the information requested by the +applicable law regarding the Licensor, the Licence and the way it may be +accessible, concluded, stored and reproduced by the Licensee. + +12. Termination of the Licence + +The Licence and the rights granted hereunder will terminate automatically upon +any breach by the Licensee of the terms of the Licence. + +Such a termination will not terminate the licences of any person who has +received the Work from the Licensee under the Licence, provided such persons +remain in full compliance with the Licence. + +13. Miscellaneous + +Without prejudice of Article 9 above, the Licence represents the complete +agreement between the Parties as to the Work. + +If any provision of the Licence is invalid or unenforceable under applicable +law, this will not affect the validity or enforceability of the Licence as a +whole. Such provision will be construed or reformed so as necessary to make it +valid and enforceable. + +The European Commission may publish other linguistic versions or new versions +of this Licence or updated versions of the Appendix, so far this is required +and reasonable, without reducing the scope of the rights granted by the +Licence. New versions of the Licence will be published with a unique version +number. + +All linguistic versions of this Licence, approved by the European Commission, +have identical value. Parties can take advantage of the linguistic version of +their choice. + +14. Jurisdiction + +Without prejudice to specific agreement between parties, + +- any litigation resulting from the interpretation of this License, arising + between the European Union institutions, bodies, offices or agencies, as a + Licensor, and any Licensee, will be subject to the jurisdiction of the Court + of Justice of the European Union, as laid down in article 272 of the Treaty + on the Functioning of the European Union, + +- any litigation arising between other parties and resulting from the + interpretation of this License, will be subject to the exclusive + jurisdiction of the competent court where the Licensor resides or conducts + its primary business. + +15. Applicable Law + +Without prejudice to specific agreement between parties, + +- this Licence shall be governed by the law of the European Union Member State + where the Licensor has his seat, resides or has his registered office, + +- this licence shall be governed by Belgian law if the Licensor has no seat, + residence or registered office inside a European Union Member State. + +Appendix + +‘Compatible Licences’ according to Article 5 EUPL are: + +- GNU General Public License (GPL) v. 2, v. 3 +- GNU Affero General Public License (AGPL) v. 3 +- Open Software License (OSL) v. 2.1, v. 3.0 +- Eclipse Public License (EPL) v. 1.0 +- CeCILL v. 2.0, v. 2.1 +- Mozilla Public Licence (MPL) v. 2 +- GNU Lesser General Public Licence (LGPL) v. 2.1, v. 3 +- Creative Commons Attribution-ShareAlike v. 3.0 Unported (CC BY-SA 3.0) for + works other than software +- European Union Public Licence (EUPL) v. 1.1, v. 1.2 +- Québec Free and Open-Source Licence — Reciprocity (LiLiQ-R) or Strong + Reciprocity (LiLiQ-R+). + +The European Commission may update this Appendix to later versions of the +above licences without producing a new version of the EUPL, as long as they +provide the rights granted in Article 2 of this Licence and protect the +covered Source Code from exclusive appropriation. + +All other changes or additions to this Appendix require the production of a +new EUPL version. diff --git a/README.md b/README.md index e6cb117..b484e08 100644 --- a/README.md +++ b/README.md @@ -17,9 +17,10 @@ Nominal sets can be used, for example, to define infinite state systems (nominal automata). Consequently, one can then do reachability analysis, minimisation and other automata-theoretic constructions. -The library uses an interface similar to the one provided by -[ONS](https://github.com/davidv1992/ONS). It provides basic instances and also -allows custom types to be nominal. It is purely functional. +This Haskell library uses an interface similar to the the C++ library +[ONS](https://github.com/davidv1992/ONS) by David Venhoek. Additionally, +`ons-hs` provides a generic way to do nominal computations on custom data +types. It is purely functional. ## Example: Logic Solver @@ -30,10 +31,11 @@ a first order logic solver by trying all values in the domain. In other words, we simply implement Tarski's truth definition: ```Haskell -data Formula = Lit Literal | T | Exists Formula | Or ... +data Formula = Lit Literal | T | Exists Formula | Or ... | Not ... | ... isTrue :: Formula -> Bool -isTrue f = P.not . null $ trueFor (singleOrbit []) f where +isTrue f = P.not . null $ trueFor (singleOrbit []) f + where -- Just check as regular Haskell values trueFor ctx (Lit (Equals i j)) = filter (\w -> w !! i == w !! j) ctx trueFor ctx (Lit (LessThan i j)) = filter (\w -> w !! i < w !! j) ctx @@ -49,8 +51,8 @@ isTrue f = P.not . null $ trueFor (singleOrbit []) f where drop context = map tail context ``` -(Note that `and`, `forAll`, and `implies` can all be expressed with the above -connectives.) Here we use basic Haskell operations, however, the variable `ctx` +Note that `and`, `forAll`, and `implies` can all be expressed with the above +connectives. Here we use basic Haskell operations, however, the variable `ctx` is of type `EquivariantSet [Atom]`. This context is an infinite set of sequences of rational numbers. The `Exists` quantifier introduces those rational numbers. (We are using De Bruijn indices.) @@ -68,14 +70,14 @@ automata. All of the magic is provided by the type class `Nominal`. You will rarely need to implement this yourself, as generic instances are provided. There are two different general instances, and you can choose which one you need -with deriving via. +with `deriving via`. For example, for the most sensible instance, use this: ```Haskell data StateSpace = Store [Atom] | Check [Atom] | Accept | Reject - deriving (Eq, Ord, GHC.Generic) - deriving Nominal via Generic StateSpace + deriving (Eq, Ord, Generic) + deriving Nominal via Generically StateSpace ``` If, however, you want a trivial group action on your data structure. (This is @@ -83,14 +85,14 @@ used for the data structure for equivariant sets.) Then you can use this: ```Haskell newtype EquivariantSet a = ... - deriving Nominal via Trivial (EquivariantSet a) + deriving Nominal via Trivially (EquivariantSet a) ``` The type class `Nominal` provides a type family and operations on them: ```Haskell class Nominal a where - type Orbit a :: * + type Orbit a :: Type toOrbit :: a -> Orbit a getElement :: Orbit a -> Support -> a support :: a -> Support @@ -99,8 +101,8 @@ class Nominal a where ## Documentation -There is none, except this page and the comments in the code. It is on my TODO -list to write proper Haddock documentation. +There is none, except this README and the comments in the code. It is on my +TODO list to write proper Haddock documentation. ## Laziness @@ -108,3 +110,46 @@ list to write proper Haddock documentation. Instead of `EquivariantSet a` it is often useful to use `OrbitList a`, since the latter is a lazy data structure. Especially when searching for certain values, that can be much faster. + + +## Changelog + +version 0.2.0.0 (2024-11-01): +* Resolves compiler warnings. +* Moved from own `Generic` to `GHC.Generically` (needs base 4.17+). If you want + to build this with an older base version, add the generically package. +* Simplifies `ons-hs.cabal` file. +* Tested with GHC 9.4.8 and 9.10.1. +* (Interestingly, GHC 9.4.8 produces faster code.) + +version 0.1.0.0 (2019-02-01): +* Initial version (used in publication). +* Developed with GHC 8.X for some X. + + +## Copyright notice and license + +Copyright 2017-2024 Joshua Moerman, Radboud Universiteit, Open Universiteit, +licensed under the EUPL (European Union Public License). + +You may find the license in the `LICENSE` file. If you want to use this +library in a commercial product, or if the license is not suitable for you, +then please get in touch so that we can change the license. + + +## How to cite + +``` +@article{VenhoekMR22, + author = {David Venhoek and + Joshua Moerman and + Jurriaan Rot}, + title = {Fast computations on ordered nominal sets}, + journal = {Theor. Comput. Sci.}, + volume = {935}, + pages = {82--104}, + year = {2022}, + url = {https://doi.org/10.1016/j.tcs.2022.09.002}, + doi = {10.1016/J.TCS.2022.09.002} +} +``` diff --git a/app/ExampleAutomata.hs b/app/ExampleAutomata.hs index aeb35d4..8502f44 100644 --- a/app/ExampleAutomata.hs +++ b/app/ExampleAutomata.hs @@ -18,7 +18,7 @@ import qualified EquivariantMap as Map import qualified EquivariantSet as Set import Data.Foldable (fold) -import qualified GHC.Generics as GHC +import GHC.Generics (Generic) import Prelude as P hiding (map, product, words, filter, foldr) @@ -35,8 +35,8 @@ ltPair = filter (\(a, b) -> a < b) $ product atoms atoms data DoubleWord = Store [Atom] | Check [Atom] | Accept | Reject - deriving (Eq, Ord, GHC.Generic) - deriving Nominal via Generic DoubleWord + deriving (Eq, Ord, Generic) + deriving Nominal via Generically DoubleWord instance ToStr DoubleWord where toStr (Store w) = "S " ++ toStr w @@ -66,8 +66,8 @@ doubleWordAut n = Automaton {..} where -- alphetbet for the Fifo queue example data FifoA = Put Atom | Get Atom - deriving (Eq, Ord, Show, GHC.Generic) - deriving Nominal via Generic FifoA + deriving (Eq, Ord, Show, Generic) + deriving Nominal via Generically FifoA instance ToStr FifoA where toStr (Put a) = "Put " ++ toStr a @@ -81,8 +81,8 @@ instance FromStr FifoA where fifoAlph = map Put rationals <> map Get rationals data FifoS = FifoS [Atom] [Atom] - deriving (Eq, Ord, GHC.Generic) - deriving Nominal via Generic FifoS + deriving (Eq, Ord, Generic) + deriving Nominal via Generically FifoS instance ToStr FifoS where toStr (FifoS l1 l2) = "F " ++ toStr l1 ++ " - " ++ toStr l2 @@ -105,8 +105,8 @@ fifoAut n = Automaton {..} where data Lint a = Lint_start | Lint_single a | Lint_full a a | Lint_semi a a | Lint_error - deriving (Eq, Ord, Show, GHC.Generic) - deriving Nominal via Generic (Lint a) + deriving (Eq, Ord, Show, Generic) + deriving Nominal via Generically (Lint a) lintExample ::Automaton (Lint Atom) Atom lintExample = Automaton {..} where @@ -133,8 +133,8 @@ lintExample = Automaton {..} where data Lmax a = Lmax_start | Lmax_single a | Lmax_double a a - deriving (Eq, Ord, Show, GHC.Generic) - deriving Nominal via Generic (Lmax a) + deriving (Eq, Ord, Show, Generic) + deriving Nominal via Generically (Lmax a) lmaxExample :: Automaton (Lmax Atom) Atom lmaxExample = Automaton {..} where diff --git a/ons-hs.cabal b/ons-hs.cabal index 39e3bbc..bc2a49d 100644 --- a/ons-hs.cabal +++ b/ons-hs.cabal @@ -1,91 +1,91 @@ +cabal-version: 2.2 name: ons-hs -version: 0.1.0.0 +version: 0.2.0.0 synopsis: Implementation of the ONS (Ordered Nominal Sets) library in Haskell description: Nominal sets are structured infinite sets. They have symmetries which make them finitely representable. This library provides basic manipulation of them for the total order symmetry. It includes: products, sums, maps and sets. Can work with custom data types. -homepage: https://gitlab.science.ru.nl/moerman/ons-hs -license: MIT +homepage: https://github.com/Jaxan/ons-hs +license: EUPL-1.2 license-file: LICENSE author: Joshua Moerman maintainer: haskell@joshuamoerman.nl -copyright: Joshua Moerman -category: Unclassified +copyright: (c) 2017-2024 Joshua Moerman build-type: Simple extra-source-files: README.md -cabal-version: >=1.10 + +common stuff + build-depends: + base >= 4.17 && < 5, + containers + default-language: Haskell2010 library - hs-source-dirs: src - exposed-modules: Automata - , EquivariantMap - , EquivariantSet - , Nominal - , Nominal.Class - , Nominal.Products - , OrbitList - , Quotient - , Support - , Support.Rat - , Support.OrdList - , Support.Set - build-depends: base >= 4.7 && < 5 - , containers - , data-ordlist - , MemoTrie - default-language: Haskell2010 + import: stuff + hs-source-dirs: src + exposed-modules: + Automata, + EquivariantMap, + EquivariantSet, + Nominal, + Nominal.Class, + Nominal.Products, + OrbitList, + Quotient, + Support, + Support.OrdList, + Support.Rat, + Support.Set + build-depends: + data-ordlist, + MemoTrie executable ons-hs-solver - hs-source-dirs: app - main-is: FoSolver.hs - build-depends: base - , ons-hs - ghc-options: -O2 - default-language: Haskell2010 + import: stuff + hs-source-dirs: app + main-is: FoSolver.hs + build-depends: ons-hs executable ons-hs-lstar - hs-source-dirs: app - main-is: LStar.hs - build-depends: base - , mtl - , ons-hs - other-modules: ExampleAutomata - , IO - ghc-options: -O2 - default-language: Haskell2010 + import: stuff + hs-source-dirs: app + main-is: LStar.hs + build-depends: + mtl, + ons-hs + other-modules: + ExampleAutomata, + IO executable ons-hs-minimise - hs-source-dirs: app - main-is: Minimise.hs - build-depends: base - , containers - , megaparsec - , mtl - , ons-hs - , parser-combinators - other-modules: ExampleAutomata - , FileAutomata - , IO - ghc-options: -O2 - default-language: Haskell2010 + import: stuff + hs-source-dirs: app + main-is: Minimise.hs + build-depends: + megaparsec, + mtl, + ons-hs, + parser-combinators + other-modules: + ExampleAutomata, + FileAutomata, + IO benchmark ons-hs-bench - type: exitcode-stdio-1.0 - hs-source-dirs: test - main-is: Bench.hs - build-depends: base - , criterion - , deepseq - , ons-hs - ghc-options: -O2 - default-language: Haskell2010 + import: stuff + type: exitcode-stdio-1.0 + hs-source-dirs: test + main-is: Bench.hs + build-depends: + criterion, + deepseq, + ons-hs test-suite ons-hs-test - type: exitcode-stdio-1.0 - hs-source-dirs: test - main-is: Spec.hs - build-depends: base - , ons-hs - default-language: Haskell2010 + import: stuff + type: exitcode-stdio-1.0 + hs-source-dirs: test + main-is: Spec.hs + build-depends: ons-hs source-repository head - type: git - location: https://gitlab.science.ru.nl/moerman/ons-hs + type: git + location: https://github.com/Jaxan/ons-hs diff --git a/src/EquivariantMap.hs b/src/EquivariantMap.hs index 174d54a..b3d3b06 100644 --- a/src/EquivariantMap.hs +++ b/src/EquivariantMap.hs @@ -31,7 +31,7 @@ import Support -- representation, just like sets. This action is trivial, since equivariant -- maps are equivariant. newtype EquivariantMap k v = EqMap { unEqMap :: Map (Orbit k) (Orbit v, [Bool]) } - deriving Nominal via Trivial (EquivariantMap k v) + deriving Nominal via Trivially (EquivariantMap k v) -- Need undecidableIntances for this deriving instance (Eq (Orbit k), Eq (Orbit v)) => Eq (EquivariantMap k v) diff --git a/src/EquivariantSet.hs b/src/EquivariantSet.hs index 9936491..fc9b036 100644 --- a/src/EquivariantSet.hs +++ b/src/EquivariantSet.hs @@ -25,7 +25,7 @@ import OrbitList (OrbitList(..)) -- representatives are chosen arbitrarily. This action is trivial, since -- equivariant sets are equivariant :-). newtype EquivariantSet a = EqSet { unEqSet :: Set (Orbit a) } - deriving Nominal via Trivial (EquivariantSet a) + deriving Nominal via Trivially (EquivariantSet a) -- Need undecidableIntances for this deriving instance Eq (Orbit a) => Eq (EquivariantSet a) diff --git a/src/Nominal/Class.hs b/src/Nominal/Class.hs index e813c82..b4d696c 100644 --- a/src/Nominal/Class.hs +++ b/src/Nominal/Class.hs @@ -9,16 +9,16 @@ module Nominal.Class ( Nominal(..) -- typeclass - , Trivial(..) -- newtype wrapper for deriving instances - , Generic(..) -- newtype wrapper for deriving instances + , Trivially(..) -- newtype wrapper for deriving instances + , Generically(..) -- newtype wrapper for deriving instances , OrbPair(..) -- need to export? , OrbRec(..) -- need to export? ) where -import Data.Void +import Data.Kind (Type) import Data.Proxy (Proxy(..)) -import GHC.Generics hiding (Generic) -import qualified GHC.Generics as GHC (Generic) +import Data.Void +import GHC.Generics import Support @@ -36,7 +36,7 @@ import Support -- * index . toOrbit == size . support -- * getElement o s is defined if index o == Set.size s class Nominal a where - type Orbit a :: * + type Orbit a :: Type toOrbit :: a -> Orbit a support :: a -> Support getElement :: Orbit a -> Support -> a @@ -76,9 +76,9 @@ instance Nominal Support where -- For the trivial action, each element is its own orbit and is supported -- by the empty set. -newtype Trivial a = Trivial { unTrivial :: a } -instance Nominal (Trivial a) where - type Orbit (Trivial a) = a +newtype Trivially a = Trivial a +instance Nominal (Trivially a) where + type Orbit (Trivially a) = a toOrbit (Trivial a) = a support _ = Support.empty getElement a _ = Trivial a @@ -87,37 +87,39 @@ instance Nominal (Trivial a) where -- We can now define trivial instances for some basic types. (Some of these -- could equivalently be derived with generics.) -deriving via Trivial Void instance Nominal Void -deriving via Trivial () instance Nominal () -deriving via Trivial Bool instance Nominal Bool -deriving via Trivial Char instance Nominal Char -deriving via Trivial Int instance Nominal Int -- NB: Trivial instance! -deriving via Trivial Ordering instance Nominal Ordering +deriving via Trivially Void instance Nominal Void +deriving via Trivially () instance Nominal () +deriving via Trivially Bool instance Nominal Bool +deriving via Trivially Char instance Nominal Char +deriving via Trivially Int instance Nominal Int -- NB: Trivial instance! +deriving via Trivially Ordering instance Nominal Ordering -- The generic instance unfolds the algebraic data type in sums and products, -- these have their own instances defined below. -newtype Generic a = Generic { unGeneric :: a } -instance (GHC.Generic a, GNominal (Rep a)) => Nominal (Generic a) where - type Orbit (Generic a) = GOrbit (Rep a) - toOrbit = gtoOrbit . from . unGeneric - support = gsupport . from . unGeneric - getElement o s = Generic (to (ggetElement o s)) +instance (Generic a, GNominal (Rep a)) => Nominal (Generically a) where + type Orbit (Generically a) = GOrbit (Rep a) + toOrbit = gtoOrbit . from . unGenerically + support = gsupport . from . unGenerically + getElement o s = Generically (to (ggetElement o s)) index _ = gindex (Proxy :: Proxy (Rep a)) +-- Not exported +unGenerically :: Generically a -> a +unGenerically (Generically a) = a -- Some instances we can derive via generics -deriving via Generic (a, b) instance (Nominal a, Nominal b) => Nominal (a, b) -deriving via Generic (a, b, c) instance (Nominal a, Nominal b, Nominal c) => Nominal (a, b, c) -deriving via Generic (a, b, c, d) instance (Nominal a, Nominal b, Nominal c, Nominal d) => Nominal (a, b, c, d) -deriving via Generic (Either a b) instance (Nominal a, Nominal b) => Nominal (Either a b) -deriving via Generic [a] instance Nominal a => Nominal [a] -deriving via Generic (Maybe a) instance Nominal a => Nominal (Maybe a) +deriving via Generically (a, b) instance (Nominal a, Nominal b) => Nominal (a, b) +deriving via Generically (a, b, c) instance (Nominal a, Nominal b, Nominal c) => Nominal (a, b, c) +deriving via Generically (a, b, c, d) instance (Nominal a, Nominal b, Nominal c, Nominal d) => Nominal (a, b, c, d) +deriving via Generically (Either a b) instance (Nominal a, Nominal b) => Nominal (Either a b) +deriving via Generically [a] instance Nominal a => Nominal [a] +deriving via Generically (Maybe a) instance Nominal a => Nominal (Maybe a) -- Generic class, so that custom data types can be derived class GNominal f where - type GOrbit f :: * + type GOrbit f :: Type gtoOrbit :: f a -> GOrbit f gsupport :: f a -> Support ggetElement :: GOrbit f -> Support -> f a @@ -165,7 +167,7 @@ instance (GNominal f, GNominal g) => GNominal (f :+: g) where -- to enumerate the whole product. instance (GNominal f, GNominal g) => GNominal (f :*: g) where type GOrbit (f :*: g) = OrbPair (GOrbit f) (GOrbit g) - gtoOrbit ~(a :*: b) = OrbPair (gtoOrbit a) (gtoOrbit b) (bla sa sb) + gtoOrbit ~(a :*: b) = OrbPair (gtoOrbit a) (gtoOrbit b) (bla sa sb) where sa = toList $ gsupport a sb = toList $ gsupport b @@ -183,7 +185,7 @@ instance (GNominal f, GNominal g) => GNominal (f :*: g) where gindex _ (OrbPair _ _ l) = length l data OrbPair a b = OrbPair !a !b ![Ordering] - deriving (Eq, Ord, Show, GHC.Generic) + deriving (Eq, Ord, Show, Generic) -- Could be in prelude or some other general purpose lib partitionOrd :: (a -> Ordering) -> [a] -> ([a], [a]) @@ -206,7 +208,7 @@ instance Nominal a => GNominal (K1 c a) where gindex _ (OrbRec o) = index (Proxy :: Proxy a) o newtype OrbRec a = OrbRec (Orbit a) - deriving GHC.Generic + deriving Generic deriving instance Eq (Orbit a) => Eq (OrbRec a) deriving instance Ord (Orbit a) => Ord (OrbRec a) deriving instance Show (Orbit a) => Show (OrbRec a) diff --git a/src/OrbitList.hs b/src/OrbitList.hs index b7142a8..943c394 100644 --- a/src/OrbitList.hs +++ b/src/OrbitList.hs @@ -18,7 +18,7 @@ import Support (Rat(..)) -- Similar to EquivariantSet, but merely a list structure. It is an -- equivariant data type, so the Nominal instance is trivial. newtype OrbitList a = OrbitList { unOrbitList :: [Orbit a] } - deriving Nominal via Trivial (OrbitList a) + deriving Nominal via Trivially (OrbitList a) deriving instance Eq (Orbit a) => Eq (OrbitList a) deriving instance Ord (Orbit a) => Ord (OrbitList a) diff --git a/stack.yaml b/stack.yaml deleted file mode 100644 index 644fb92..0000000 --- a/stack.yaml +++ /dev/null @@ -1,66 +0,0 @@ -# This file was automatically generated by 'stack init' -# -# Some commonly used options have been documented as comments in this file. -# For advanced use and comprehensive documentation of the format, please see: -# https://docs.haskellstack.org/en/stable/yaml_configuration/ - -# Resolver to choose a 'specific' stackage snapshot or a compiler version. -# A snapshot resolver dictates the compiler version and the set of packages -# to be used for project dependencies. For example: -# -# resolver: lts-3.5 -# resolver: nightly-2015-09-21 -# resolver: ghc-7.10.2 -# resolver: ghcjs-0.1.0_ghc-7.10.2 -# resolver: -# name: custom-snapshot -# location: "./custom-snapshot.yaml" -resolver: lts-13.1 - -# User packages to be built. -# Various formats can be used as shown in the example below. -# -# packages: -# - some-directory -# - https://example.com/foo/bar/baz-0.0.2.tar.gz -# - location: -# git: https://github.com/commercialhaskell/stack.git -# commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a -# - location: https://github.com/commercialhaskell/stack/commit/e7b331f14bcffb8367cd58fbfc8b40ec7642100a -# extra-dep: true -# subdirs: -# - auto-update -# - wai -# -# A package marked 'extra-dep: true' will only be built if demanded by a -# non-dependency (i.e. a user package), and its test suites and benchmarks -# will not be run. This is useful for tweaking upstream packages. -packages: -- . -# Dependency packages to be pulled from upstream that are not in the resolver -# (e.g., acme-missiles-0.3) -# extra-deps: [] - -# Override default flag values for local packages and extra-deps -# flags: {} - -# Extra package databases containing global packages -# extra-package-dbs: [] - -# Control whether we use the GHC we find on the path -# system-ghc: true -# -# Require a specific version of stack, using version ranges -# require-stack-version: -any # Default -# require-stack-version: ">=1.5" -# -# Override the architecture used by stack, especially useful on Windows -# arch: i386 -# arch: x86_64 -# -# Extra directories used by stack for building -# extra-include-dirs: [/path/to/dir] -# extra-lib-dirs: [/path/to/dir] -# -# Allow a newer minor version of GHC than the snapshot specifies -# compiler-check: newer-minor