fcf-containers 0.6.0 → 0.8.2
raw patch · 48 files changed
Files
- CHANGELOG.md +90/−0
- README.md +42/−4
- TODO.md +13/−3
- default.nix +20/−5
- examples/Crabcombat.hs +3/−2
- examples/Haiku.hs +15/−1
- examples/Orbits.hs +1/−1
- fcf-containers.cabal +42/−10
- flake.lock +44/−0
- flake.nix +72/−0
- shell.nix +0/−9
- src/Fcf/Alg/List.hs +31/−38
- src/Fcf/Alg/Morphism.hs +15/−27
- src/Fcf/Alg/Nat.hs +0/−2
- src/Fcf/Alg/Other.hs +7/−17
- src/Fcf/Alg/Sort.hs +8/−20
- src/Fcf/Alg/Symbol.hs +22/−25
- src/Fcf/Alg/Tree.hs +23/−25
- src/Fcf/Control/Monad.hs +431/−0
- src/Fcf/Data/Bitree.hs +2/−5
- src/Fcf/Data/Char.hs +200/−0
- src/Fcf/Data/List/Utils.hs +59/−0
- src/Fcf/Data/MapC.hs +97/−92
- src/Fcf/Data/NatMap.hs +91/−90
- src/Fcf/Data/NewText.hs +1035/−0
- src/Fcf/Data/OldText.hs +753/−0
- src/Fcf/Data/Reflect.hs +228/−0
- src/Fcf/Data/Set.hs +76/−84
- src/Fcf/Data/Symbol.hs +142/−0
- src/Fcf/Data/Text.hs +16/−10
- src/Fcf/Data/Text/Internal.hs +2/−5
- src/Fcf/Data/Tree.hs +50/−7
- src/Fcf/Data/Tuple.hs +59/−0
- test/Test/Alg.hs +22/−0
- test/Test/Alg/List.hs +171/−0
- test/Test/Alg/Morphism.hs +85/−0
- test/Test/Alg/Nat.hs +66/−0
- test/Test/Alg/Other.hs +54/−0
- test/Test/Alg/Sort.hs +56/−0
- test/Test/Alg/Symbol.hs +157/−0
- test/Test/Alg/Tree.hs +129/−0
- test/Test/Control.hs +9/−0
- test/Test/Control/Monad.hs +140/−0
- test/Test/Data.hs +12/−0
- test/Test/Data/Reflect.hs +328/−0
- test/Test/Data/Set.hs +221/−0
- test/doctest.hs +12/−4
- test/test.hs +16/−11
CHANGELOG.md view
@@ -1,4 +1,94 @@++# 0.8.2++Thank you again to Skyfold (Martin P.)++- Deprecation warning for the KnownNats class and its instances: the KnownVal+ can be used instead.+- Instances to IntMap, Map and Set to convert directly from '[a] or '[ '(key,val) ]+- The ErrorMessage instance for KnownVal to show information about types +- Add KnownVal instance for typeable types, this can be used as Show for+ the types presented at the kind level. +- Fix the Test.Alg test description+- Remove doc-tests from all Fcf.Alg modules and write the corresponding test modules+- Some cleaning+- Add depracation and warning pragmas to text modules.+++# 0.8.1++20230410++Thank you to Skyfold (Martin P.)++- Generalized KnownVal instances+- Initialized the HSpec use and test directory organization+- Added flake definitions+- Updated stack version (not tested with stack)+- Removed shell.nix+- Fcf.Data.Set doctests removed and replaced with Test.Data.Set+- Fcf.Alg.List doctests removed and replaced with Test.Alg.List+++# 0.8.0++20230226++- Fcf.Data.Char for GHC 9.2.X or higher, the Text will start using this.+- Fcf.Data.Tuple with Swap method+- Fcf.Data.Reflect gives methods to turn type-level structures into value-level.+ These include instances for trees, natMaps, maps, lists, and text. Text instances+ are only for GHC 9.2.X or higher.+- Fcf.Data.Symbol for GHC 9.2.x or higher, the Text will start using this.+- Deprecate the current Text and Text.Internal modules and introduce new using+ the Symbol module (these are for GHC 9.2.x or higher).+- Add new dependencies, containers and text (for the Reflect module).+- Several hlint suggestion fixes included++The "NewText" module could have more methods that the counterpart already has.+Also, the Reflect module could have more typical instances.++The test will be moved into the test directory and away from the doctests, which+in turn, will be deprecated. The doctests would be otherwise nice, but they are+difficult (laborous) to support for several different ghc versions.++This also includes Data.List.Utils and there Foldl and MaybeToList methods.+++# 0.7.2++2023015++- Add notes about defunctionalization and associated code examples+- Add helper module for Foldl method (it would be better at first-class-families lib).++# 0.7.1++20220601++ - Clean up several modules (remove extra spaces and paranthesis)+ - Update doctest function and remove Glob dependency+ - Update ci pipeline to do tests with 9.0 and 9.2++# 0.7.0++20220424++ - Add preliminary support for Applicative and Monadic computations+ - Small whitespace fixes+ - Added dependency for mtl (to get Identity)+ - Add new compiler versions for tests and drop some old+ - Start referring to cabal version 3.0++# 0.6.1++20210130++Start using the github actions and remove travis CI.+ # 0.6.0++20210130 - use symbol as text representation (we can split predefined char-sets, as shown by the Csongor at https://kcsongor.github.io/symbol-parsing-haskell/ see also
README.md view
@@ -56,14 +56,38 @@ cabal test ``` -The doc-tests both document and work as main testing mechanism for this lib. +If you are flakes user, `nix develop -c zsh` (or without that `-c zsh`) works as well. +The doc-tests both document and work partly as testing mechanism for this lib. Please +do note that we are moving away from the doc-tests and building the testing modules +under `test` directory.+ If you don't use nix, `cabal install fcf-containers` should be enough. This package has almost as good number of dependencies as the first-class-families. ## Example ++### Test cases as examples++The +[test directory](https://github.com/gspia/fcf-containers/blob/master/test)+contains a lot of useful examples. There you will find out, how to apply most+of the methods: examples that only work on "compile time", and examples on how+to get the results from type level calculations to value level (see the Reflect+test module and the `fromType` method applications, also in some other testing+modules).+++### Three example programs calculating something++These are a bit larger examples, but not yet too large: somewhat convenient small +module size. Idea was to take an algorithm, and convert it to a type-level +computation, or in some other way give an example of methods that this library+provides.++ See [Orbits.hs](https://github.com/gspia/fcf-containers/blob/master/examples/Orbits.hs). It shows how to solve a real problem, what PRAGMAs are probably needed etc.@@ -72,7 +96,10 @@ cabal run orbits ``` -There is also another example that show how to use MapC, see+There is also another Advent of Code problem, see the Carbcombat file.+++To see, how to use MapC, take a look at [Haiku.hs](https://github.com/gspia/fcf-containers/blob/master/examples/Haiku.hs) ```@@ -80,6 +107,16 @@ ``` +### Other example material++Please, do take a look of the notes made for the Helsinki Haskell meetup+on 11th January 2023+[notes](https://github.com/gspia/fcf-containers/blob/master/examples/20230111_hhslides.md)+and the associated +[code examples](https://github.com/gspia/fcf-containers/blob/master/examples/20230111_hhmeetup.hs).+++ ## Random Notes ### Partiality and anonymous functions@@ -91,7 +128,7 @@ We don't have lambdas, but if you can write the helper function in point-free form, it might can be used directly without any global function definition. Remember, that `(<=<)` corresponds to term-level `(.)` and `(=<<)` to -term-level function application `($)`. See also Maguire's book +term-level function application `($)`. See also Maguire's book (Thinking with Types). @@ -167,6 +204,7 @@ Source also contains a lot of examples, see [fcf-containers](https://github.com/gspia/fcf-containers/tree/master/src/Fcf).-+The examples will be left near the code, even thou the doctest runs will be +removed and replaced with real tests at the test-directory. Happy :kinding!
TODO.md view
@@ -1,18 +1,28 @@ # TODO -## Examples:+## Examples and tests: -E.g. add examples using the other data structures.+E.g. add examples using the other data structures. Start building the+tests in the test-directory. The doc-tests are hard to keep working for+several GHC versions at the same time and deprecate them. +This will also mean that the code modules will be come a bit cleaner.++ ## Data structures: -Add the missing methods and doctests.+Add the missing methods and tests. Move doctests under tests. - Set - NatMap - Graphs - MapB (Map data structure) but implemented with the balanced trees - MapC +- Text (e.g. those folding methods)+++The test structuring requires a bit thinking. New dependencies or some +simple structure to help here? ## Morphisms:
default.nix view
@@ -1,5 +1,13 @@ { - # compiler ? "ghc881" + # compiler ? "ghc884" + # compiler ? "ghc8107"+ # compiler ? "ghc902"+ # compiler ? "ghc922"+ # compiler ? "ghc924"+ # compiler ? "ghc925" # listlike-tests are extremely slow+ # compiler ? "ghc926" # not yet+ # compiler ? "ghc942"+ # compiler ? "ghc943" } : let config = {@@ -16,12 +24,18 @@ # }); first-class-families = self.callCabal2nix "first-class-families" # ~/gito/first-class-families {}; - (pkgs.fetchFromGitHub { # 0.8+ (pkgs.fetchFromGitHub { # 0.8.0.1 owner = "Lysxia"; repo = "first-class-families";- rev = "4a0bf3ea9c125bb4009b61ce70b1a5339b7b2072";- sha256 = "14387mpfvds226iynkpay3aaqamvxznxjsmg2qcwdxafdvxmyq9z";+ rev = "933c2527de9bfcb162e0eebcbcdac4f28a39bd3b";+ sha256 = "0k66s3bg71pm890zgr5w88zv7vcrxfwd74c0dcn945k91nzn41b2"; }) {};+ # (pkgs.fetchFromGitHub { # 0.8.0.1+ # owner = "Lysxia";+ # repo = "first-class-families";+ # rev = "d4780864ed9b11343b7b26050e39b2048a8e61f6";+ # sha256 = "1iw0dryz66z4k9lsj1kayf17xs38i8bdk9aqi2qz49vcbhnfw8pd";+ # }) {}; # something for the next version? # rev = "9fe4ce36cf1cd4b0f5af59c923c15b9085c48cd6"; # sha256 = "1677ylhhf1mwwfs6j2p6gbn2f6mzsx4zmaihz8v9v07h845wz8l7";@@ -47,7 +61,8 @@ adjust-for-ghc = drv: { executableSystemDepends = [ hpkgs.ghcid- hpkgs.ghcide+ # hpkgs.ghcide+ hpkgs.haskell-language-server hpkgs.cabal-install ]; buildDepends = [
examples/Crabcombat.hs view
@@ -101,7 +101,7 @@ ( Foldr (N.+) 0 =<< Uncurry (ZipWith (N.*))- =<< Bimap ((MToN 1) <=< Length) Reverse+ =<< Bimap (MToN 1 <=< Length) Reverse =<< AsPair =<< Fst =<< PlayGame '[] input@@ -114,6 +114,7 @@ -- Does not compile on my machine (not even with the -freduction-depth=0 at cabal), -- not enough memory -- Ghci also gets 'Killed'.+{- type Input = '( '[21, 50, 9, 45, 16, 47, 27, 38, 29, 48, 10, 42, 32, 31, 41, 11, 8, 33, 25, 30, 12, 40, 7, 23, 46] , '[22, 20, 44, 2, 26, 17, 34, 37, 43, 5, 15, 18, 36, 19, 24, 35, 3, 13, 14, 1, 6, 39, 49, 4, 28]@@ -136,7 +137,7 @@ '( '[21, 50, 9, 45, 16, 47, 27, 38, 29, 48, 10, 40, 7, 23, 46] , '[22, 20, 44, 2, 26, 17, 34, 37, 43, 5, 15, 39, 49, 4, 28] ) -- :: ([Nat], [Nat])-+-}
examples/Haiku.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -16,9 +17,14 @@ This exemplifies the use of @MapC@ and @Text@. +Idea of the type-level program. We want to check that the given type-level+Haiku is correctly composed. As inputs, we get the Haiku as words written+in syllables. The allowed Haiku-structure, that is, the number of expected+syllables per line, is given separetely. We require 5, 7 and 5 syllables.+ Exercises: - Write a method for structurally wrong Haiku's and output something other in those cases- - Vocabulary with syllables is somewhat parameterized (except WSmap) but + - Vocabulary with syllables is somewhat parameterized (except WSmap) but not the other half. Change CheckHaiku to accepts the vocabulary to use and the haiku the check. @@ -36,7 +42,11 @@ import Fcf.Data.List as L import Fcf.Data.MapC as M+#if __GLASGOW_HASKELL__ >= 902+import Fcf.Data.NewText as T+#else import Fcf.Data.Text as T+#endif import Fcf.Alg.List (Equal) @@ -124,7 +134,11 @@ -- | We left something here as well. We don't want this executable to compile -- if the Haiku is not ok. showHaiku+#if __GLASGOW_HASKELL__ >= 902+ :: forall symbol. (symbol ~ Eval (Unpack =<< Haiku), 'True ~ Eval CheckHaiku)+#else :: forall symbol. (symbol ~ Eval (ToSymbol =<< Haiku), 'True ~ Eval CheckHaiku)+#endif => String showHaiku = TL.symbolVal @symbol Proxy
examples/Orbits.hs view
@@ -14,7 +14,7 @@ Example on how to do compile-time (ie type-level) computations and how to get the results into use on term-level (ie runtime). -The original problem is described in +The original problem is described in [aoc 19 d6](https://adventofcode.com/2019/day/6). We use the described example input data in a bit different form. See the link for the original data and answer.
fcf-containers.cabal view
@@ -1,3 +1,4 @@+Cabal-version: 3.0 Name: fcf-containers Synopsis: Data structures and algorithms for first-class-families Description:@@ -6,28 +7,35 @@ contents of containers-package and show how these can be used. Everything is based on the ideas given in the first-class-families -package. Homepage: https://github.com/gspia/fcf-containers-Version: 0.6.0+Version: 0.8.2 Build-type: Simple Author: gspia Maintainer: iahogsp@gmail.com-License: BSD3+License: BSD-3-Clause License-file: LICENSE Category: Other Copyright: gspia (c) 2020--Extra-source-files: README.md, TODO.md, CHANGELOG.md, default.nix, shell.nix-Cabal-version: 1.24-Tested-With: GHC ==8.10.3 || ==8.8.4 || ==8.6.5 || ==8.4.4+Extra-source-files: README.md, TODO.md, CHANGELOG.md, default.nix, flake.nix, flake.lock+Tested-With: GHC ==9.2.4 || ==9.0.2 || ==8.10.7 library hs-source-dirs: src- exposed-modules: Fcf.Data.MapC+ exposed-modules: Fcf.Control.Monad , Fcf.Data.Bitree+ , Fcf.Data.Char+ , Fcf.Data.List.Utils+ , Fcf.Data.MapC , Fcf.Data.NatMap+ , Fcf.Data.Reflect , Fcf.Data.Set- , Fcf.Data.Text+ , Fcf.Data.Symbol , Fcf.Data.Text.Internal+ , Fcf.Data.Text+ , Fcf.Data.NewText+ , Fcf.Data.OldText , Fcf.Data.Tree+ , Fcf.Data.Tuple , Fcf.Alg.List , Fcf.Alg.Morphism , Fcf.Alg.Nat@@ -35,8 +43,11 @@ , Fcf.Alg.Sort , Fcf.Alg.Symbol , Fcf.Alg.Tree- build-depends: base >= 4.9 && < 4.18+ build-depends: base >= 4.9 && < 4.22+ , containers , first-class-families >= 0.8 && < 0.9+ , ghc-prim+ , text ghc-options: -Wall default-language: Haskell2010 -- ghc-options:@@ -61,6 +72,9 @@ build-depends: base , first-class-families , fcf-containers+ ghc-options:+ -Wall+ -freduction-depth=0 Executable crabcombat hs-source-dirs: examples@@ -80,10 +94,28 @@ hs-source-dirs: test main-is: test.hs default-language: Haskell2010+ other-modules: Test.Alg+ , Test.Alg.List+ , Test.Alg.Morphism+ , Test.Alg.Nat+ , Test.Alg.Other+ , Test.Alg.Sort+ , Test.Alg.Symbol+ , Test.Alg.Tree+ , Test.Control+ , Test.Control.Monad+ , Test.Data+ , Test.Data.Reflect+ , Test.Data.Set build-depends: base , first-class-families , fcf-containers+ , hspec+ , containers+ , text+-- ghc-options:+-- -freduction-depth=0 test-suite fcf-doctest type: exitcode-stdio-1.0@@ -93,10 +125,10 @@ if impl(ghc >= 8.6) build-depends: base+ , doctest , first-class-families , fcf-containers- , doctest- , Glob+ , ghc-prim else buildable: False
+ flake.lock view
@@ -0,0 +1,44 @@+{+ "nodes": {+ "nix-filter": {+ "locked": {+ "lastModified": 1666547822,+ "narHash": "sha256-razwnAybPHyoAyhkKCwXdxihIqJi1G6e1XP4FQOJTEs=",+ "owner": "numtide",+ "repo": "nix-filter",+ "rev": "1a3b735e13e90a8d2fd5629f2f8363bd7ffbbec7",+ "type": "github"+ },+ "original": {+ "owner": "numtide",+ "ref": "master",+ "repo": "nix-filter",+ "type": "github"+ }+ },+ "nixpkgs": {+ "locked": {+ "lastModified": 1674990008,+ "narHash": "sha256-4zOyp+hFW2Y7imxIpZqZGT8CEqKmDjwgfD6BzRUE0mQ=",+ "owner": "nixos",+ "repo": "nixpkgs",+ "rev": "d2bbcbe6c626d339b25a4995711f07625b508214",+ "type": "github"+ },+ "original": {+ "owner": "nixos",+ "ref": "nixpkgs-unstable",+ "repo": "nixpkgs",+ "type": "github"+ }+ },+ "root": {+ "inputs": {+ "nix-filter": "nix-filter",+ "nixpkgs": "nixpkgs"+ }+ }+ },+ "root": "root",+ "version": 7+}
+ flake.nix view
@@ -0,0 +1,72 @@+{+ description = "Data structures and algorithms for first-class-families";++ inputs = {+ nixpkgs.url = "github:nixos/nixpkgs/nixpkgs-unstable";+ nix-filter.url = "github:numtide/nix-filter/master";+ };++ outputs = { self, nixpkgs, nix-filter }: + let+ pkgs = import nixpkgs { system = "x86_64-linux"; };++ # filter = import nix-filter { };++ ghcVersion = "925";+ # ghcVersion = "92";+ # ghcVersion = "902";++ src = nix-filter.lib {+ root = ./.;+ include = [+ (nix-filter.lib.inDirectory "src")+ (nix-filter.lib.inDirectory "examples")+ (nix-filter.lib.inDirectory "test")+ (nix-filter.lib.matchExt "hs")+ ./fcf-containers.cabal+ ./cabal.project+ ./LICENSE+ ];+ };++ fcf-containers = hself: hself.callCabal2nix "fcf-containers" src {};++ myHaskellPackages = pkgs.haskell.packages."ghc${ghcVersion}".override {+ overrides = hself: hsuper: {+ # fcf-containers = hself.callCabal2nix "fcf-containers" sources.fcf-containers {};+ # fcf-containers = (import sources.fcf-containers {});+ fcf-containers = fcf-containers hself;+ # ListLike = pkgs.haskell.lib.dontCheck hsuper.ListLike;+ # type-of-html = pkgs.haskell.lib.doBenchmark (hself.callPackage ./nix/type-of-html.nix {inherit src;});+ # type-of-html = hself.callCabal2nix "type-of-html" src {};+ # optics-core = hsuper.optics-core.overrideAttrs(old: {+ # configureFlags = "-f explicit-generic-labels";+ # patches = [./optics-core.patch];+ # });+ };+ };++ shell = myHaskellPackages.shellFor {+ packages = p: [+ p.fcf-containers+ ];+ buildInputs = with pkgs.haskell.packages."ghc${ghcVersion}"; [+ myHaskellPackages.cabal-install+ ghcid+ (pkgs.haskell-language-server.override { supportedGhcVersions = [ "${ghcVersion}" ]; })+ hlint+ # implicit-hie+ # cabal2nix+ ];+ withHoogle = true;+ doBenchmark = true;+ };++ in+ {+ library = fcf-containers;+ # packages.x86_64-linux.default = ;+ devShell.x86_64-linux = shell;+ inherit pkgs;+ };+}
− shell.nix
@@ -1,9 +0,0 @@-{ nixpkgs ? import <nixpkgs> {}-/* , compiler ? "ghc822" */-} : -let- inherit (nixpkgs) pkgs;- /* drv = import ./. { inherit compiler; }; */- drv = import ./. { };-in-if pkgs.lib.inNixShell then drv.env else drv
src/Fcf/Alg/List.hs view
@@ -1,5 +1,3 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-}@@ -21,6 +19,8 @@ This module also contains other list-related functions (that might move to other place some day). +To see examples, please do take a look of the respective test module.+ -} --------------------------------------------------------------------------------@@ -41,13 +41,6 @@ -------------------------------------------------------------------------------- --- For the doctests:---- $setup--- >>> import Fcf.Combinators----------------------------------------------------------------------------------- -- | Base functor for a list of type @[a]@. data ListF a b = ConsF a b | NilF @@ -57,7 +50,7 @@ -------------------------------------------------------------------------------- --- | ListToFix can be used to turn a norma type-level list into the base+-- | ListToFix can be used to turn a normal type-level list into the base -- functor type ListF, to be used with e.g. Cata. For examples in use, see -- 'LenAlg' and 'SumAlg'. --@@ -67,8 +60,8 @@ -- -- === __Example__ ----- >>> :kind! Eval (ListToFix '[1,2,3])--- Eval (ListToFix '[1,2,3]) :: Fix (ListF Nat)+-- > :kind! Eval (ListToFix '[1,2,3])+-- Eval (ListToFix '[1,2,3]) :: Fix (ListF TL.Natural) -- = 'Fix ('ConsF 1 ('Fix ('ConsF 2 ('Fix ('ConsF 3 ('Fix 'NilF)))))) data ListToFix :: [a] -> Exp (Fix (ListF a)) type instance Eval (ListToFix '[]) = 'Fix 'NilF@@ -78,8 +71,8 @@ -- -- === __Example__ ----- >>> :kind! Eval (Cata LenAlg =<< ListToFix '[1,2,3])--- Eval (Cata LenAlg =<< ListToFix '[1,2,3]) :: Nat+-- > :kind! Eval (Cata LenAlg =<< ListToFix '[1,2,3])+-- Eval (Cata LenAlg =<< ListToFix '[1,2,3]) :: TL.Natural -- = 3 data LenAlg :: Algebra (ListF a) Nat type instance Eval (LenAlg 'NilF) = 0@@ -89,8 +82,8 @@ -- -- === __Example__ ----- >>> :kind! Eval (Cata SumAlg =<< ListToFix '[1,2,3,4])--- Eval (Cata SumAlg =<< ListToFix '[1,2,3,4]) :: Nat+-- > :kind! Eval (Cata SumAlg =<< ListToFix '[1,2,3,4])+-- Eval (Cata SumAlg =<< ListToFix '[1,2,3,4]) :: TL.Natural -- = 10 data SumAlg :: Algebra (ListF Nat) Nat type instance Eval (SumAlg 'NilF) = 0@@ -100,8 +93,8 @@ -- -- === __Example__ ----- >>> :kind! Eval (Cata ProdAlg =<< ListToFix '[1,2,3,4])--- Eval (Cata ProdAlg =<< ListToFix '[1,2,3,4]) :: Nat+-- > :kind! Eval (Cata ProdAlg =<< ListToFix '[1,2,3,4])+-- Eval (Cata ProdAlg =<< ListToFix '[1,2,3,4]) :: TL.Natural -- = 24 data ProdAlg :: Algebra (ListF Nat) Nat type instance Eval (ProdAlg 'NilF) = 1@@ -113,8 +106,9 @@ -- -- === __Example__ ----- >>> :kind! Eval (ListToParaFix '[1,2,3])--- Eval (ListToParaFix '[1,2,3]) :: Fix (ListF (Nat, [Nat]))+-- > :kind! Eval (ListToParaFix '[1,2,3])+-- Eval (ListToParaFix '[1,2,3]) :: Fix+-- (ListF (TL.Natural, [TL.Natural])) -- = 'Fix -- ('ConsF -- '(1, '[2, 3])@@ -130,8 +124,8 @@ -- -- === __Example__ ----- >>> :kind! Eval (Para DedupAlg =<< ListToParaFix '[1,1,3,2,5,1,3,2])--- Eval (Para DedupAlg =<< ListToParaFix '[1,1,3,2,5,1,3,2]) :: [Nat]+-- > :kind! Eval (Para DedupAlg =<< ListToParaFix '[1,1,3,2,5,1,3,2])+-- Eval (Para DedupAlg =<< ListToParaFix '[1,1,3,2,5,1,3,2]) :: [TL.Natural] -- = '[5, 1, 3, 2] data DedupAlg :: RAlgebra (ListF (a,[a])) [a] type instance Eval (DedupAlg 'NilF) = '[]@@ -146,8 +140,8 @@ -- -- === __Example__ ----- >>> :kind! Eval (Sliding 3 '[1,2,3,4,5,6])--- Eval (Sliding 3 '[1,2,3,4,5,6]) :: [[Nat]]+-- > :kind! Eval (Sliding 3 '[1,2,3,4,5,6])+-- Eval (Sliding 3 '[1,2,3,4,5,6]) :: [[TL.Natural]] -- = '[ '[1, 2, 3], '[2, 3, 4], '[3, 4, 5], '[4, 5, 6], '[5, 6], '[6]] data Sliding :: Nat -> [a] -> Exp [[a]] type instance Eval (Sliding n lst) =@@ -172,14 +166,14 @@ type instance Eval (EvensAlg 'NilF) = '[] type instance Eval (EvensAlg ('ConsF _ rst )) = Eval (EvensStrip =<< Strip rst) --- | This picks up the elements on even positions on a list and is an +-- | This picks up the elements on even positions on a list and is an -- example on how to use Histo. This example is -- from Tim Williams, Recursion Schemes by example. -- -- === __Example__ ----- >>> :kind! Eval (Evens =<< RunInc 8)--- Eval (Evens =<< RunInc 8) :: [Nat]+-- > :kind! Eval (Evens =<< RunInc 8)+-- Eval (Evens =<< RunInc 8) :: [TL.Natural] -- = '[2, 4, 6, 8] data Evens :: [a] -> Exp [a] type instance Eval (Evens lst) = Eval (Histo EvensAlg =<< ListToFix lst)@@ -200,8 +194,8 @@ -- -- === __Example__ ----- >>> :kind! Eval (RunInc 8)--- Eval (RunInc 8) :: [Nat]+-- > :kind! Eval (RunInc 8)+-- Eval (RunInc 8) :: [TL.Natural] -- = '[1, 2, 3, 4, 5, 6, 7, 8] data RunInc :: Nat -> Exp [Nat] type instance Eval (RunInc n) = Eval (Reverse =<< Unfoldr ListRunAlg n)@@ -213,8 +207,8 @@ -- -- === __Example__ ----- >>> :kind! Eval (Sum '[1,2,3])--- Eval (Sum '[1,2,3]) :: Nat+-- > :kind! Eval (Sum '[1,2,3])+-- Eval (Sum '[1,2,3]) :: TL.Natural -- = 6 data Sum :: [Nat] -> Exp Nat type instance Eval (Sum ns) = Eval (Foldr (+) 0 ns)@@ -234,8 +228,8 @@ -- -- === __Example__ ----- >>> :kind! Eval (MToN 1 3)--- Eval (MToN 1 3) :: [Nat]+-- > :kind! Eval (MToN 1 3)+-- Eval (MToN 1 3) :: [TL.Natural] -- = '[1, 2, 3] data MToN :: Nat -> Nat -> Exp [Nat] type instance Eval (MToN m n) = Eval (Unfoldr (MToNHelp n) m)@@ -246,8 +240,8 @@ -- -- === __Example__ ----- >>> :kind! Eval (ToList 1)--- Eval (ToList 1) :: [Nat]+-- > :kind! Eval (ToList 1)+-- Eval (ToList 1) :: [TL.Natural] -- = '[1] data ToList :: a -> Exp [a] type instance Eval (ToList a) = '[a]@@ -257,13 +251,12 @@ -- -- === __Example__ ----- >>> :kind! Eval (Equal '[1,2,3] '[1,2,3])+-- > :kind! Eval (Equal '[1,2,3] '[1,2,3]) -- Eval (Equal '[1,2,3] '[1,2,3]) :: Bool -- = 'True ----- >>> :kind! Eval (Equal '[1,2,3] '[1,3,2])+-- > :kind! Eval (Equal '[1,2,3] '[1,3,2]) -- Eval (Equal '[1,2,3] '[1,3,2]) :: Bool -- = 'False data Equal :: [a] -> [a] -> Exp Bool type instance Eval (Equal as bs) = Eval (And =<< ZipWith TyEq as bs)-
src/Fcf/Alg/Morphism.hs view
@@ -1,5 +1,3 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-}@@ -34,17 +32,8 @@ -------------------------------------------------------------------------------- --- For the doctests:---- $setup--- >>> import qualified GHC.TypeLits as TL--- >>> import Fcf.Alg.List--- >>> import Fcf.Data.Nat----------------------------------------------------------------------------------- -- | Structure that 'Cata' can fold and that is a result structure of 'Ana'.-data Fix f = Fix (f (Fix f))+newtype Fix f = Fix (f (Fix f)) -- | Commonly used name describing the method 'Cata' eats. type Algebra f a = f a -> Exp a@@ -64,22 +53,22 @@ -- Check Fcf.Alg.List to see example algebras in use. There we have e.g. -- ListToFix-function. data Cata :: Algebra f a -> Fix f -> Exp a-type instance Eval (Cata alg ('Fix b)) = alg @@ (Eval (Map (Cata alg) b))+type instance Eval (Cata alg ('Fix b)) = alg @@ Eval (Map (Cata alg) b) -- | Ana can also be used to build a 'Fix' structure. -- -- === __Example__ ----- >>> data NToOneCoA :: CoAlgebra (ListF Nat) Nat--- >>> :{+-- > data NToOneCoA :: CoAlgebra (ListF Nat) Nat+-- > :{ -- type instance Eval (NToOneCoA b) = -- If (Eval (b < 1) ) -- 'NilF -- ('ConsF b ( b TL.- 1)) -- :} ----- >>> :kind! Eval (Ana NToOneCoA 3)--- Eval (Ana NToOneCoA 3) :: Fix (ListF Nat)+-- > :kind! Eval (Ana NToOneCoA 3)+-- Eval (Ana NToOneCoA 3) :: Fix (ListF TL.Natural) -- = 'Fix ('ConsF 3 ('Fix ('ConsF 2 ('Fix ('ConsF 1 ('Fix 'NilF)))))) data Ana :: CoAlgebra f a -> a -> Exp (Fix f) type instance Eval (Ana coalg a) = 'Fix (Eval (Map (Ana coalg) (Eval (coalg a))))@@ -91,16 +80,16 @@ -- -- === __Example__ ----- >>> data NToOneCoA :: CoAlgebra (ListF Nat) Nat--- >>> :{+-- > data NToOneCoA :: CoAlgebra (ListF Nat) Nat+-- > :{ -- type instance Eval (NToOneCoA b) = -- If (Eval (b < 1) ) -- 'NilF -- ('ConsF b ( b TL.- 1)) -- :} ----- >>> :kind! Eval (Hylo SumAlg NToOneCoA 5)--- Eval (Hylo SumAlg NToOneCoA 5) :: Nat+-- > :kind! Eval (Hylo SumAlg NToOneCoA 5)+-- Eval (Hylo SumAlg NToOneCoA 5) :: TL.Natural -- = 15 data Hylo :: Algebra f a -> CoAlgebra f b -> b -> Exp a type instance Eval (Hylo alg coalg a) = Eval (Cata alg =<< Ana coalg a)@@ -117,7 +106,7 @@ -- Check Fcf.Alg.List to see example algebras in use. There we have e.g. -- ListToParaFix-function. data Para :: RAlgebra f a -> Fix f -> Exp a-type instance Eval (Para ralg ('Fix a)) = ralg @@ (Eval (Map (Fanout ralg) a))+type instance Eval (Para ralg ('Fix a)) = ralg @@ Eval (Map (Fanout ralg) a) -------------------------------------------------------------------------------- @@ -185,8 +174,8 @@ -- -- === __Example__ ----- >>> :kind! Eval (First ((+) 1) '(3,"a"))--- Eval (First ((+) 1) '(3,"a")) :: (Nat, TL.Symbol)+-- > :kind! Eval (First ((+) 1) '(3,"a"))+-- Eval (First ((+) 1) '(3,"a")) :: (TL.Natural, TL.Symbol) -- = '(4, "a") data First :: (a -> Exp b) -> f a c -> Exp (f b c) @@ -201,8 +190,8 @@ -- -- === __Example__ ----- >>> :kind! Eval (Second ((+) 1) '("a",3))--- Eval (Second ((+) 1) '("a",3)) :: (TL.Symbol, Nat)+-- > :kind! Eval (Second ((+) 1) '("a",3))+-- Eval (Second ((+) 1) '("a",3)) :: (TL.Symbol, TL.Natural) -- = '("a", 4) data Second :: (c -> Exp d) -> f a c -> Exp (f a d) @@ -212,4 +201,3 @@ -- Either type instance Eval (Second f ('Left a)) = 'Left a type instance Eval (Second f ('Right b)) = 'Right (f @@ b)-
src/Fcf/Alg/Nat.hs view
@@ -1,5 +1,3 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-}
src/Fcf/Alg/Other.hs view
@@ -1,8 +1,5 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-}-{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wall #-} {-# OPTIONS_GHC -Werror=incomplete-patterns #-}@@ -25,23 +22,17 @@ module Fcf.Alg.Other where -import Fcf as Fcf-------------------------------------------------------------------------------------- For the doctests:---- $setup+import Fcf -------------------------------------------------------------------------------- -- | Helper. ----- === __Evample__+-- === __Example__ ----- >>> :kind! Eval (PairMaybeToMaybePair '( 'Just "txt", 'Just 1))+-- > :kind! Eval (PairMaybeToMaybePair '( 'Just "txt", 'Just 1)) -- Eval (PairMaybeToMaybePair '( 'Just "txt", 'Just 1)) :: Maybe--- (GHC.Types.Symbol, GHC.Types.Nat)+-- (Symbol, TL.Natural) -- = 'Just '("txt", 1) data PairMaybeToMaybePair :: (Maybe a, Maybe b) -> Exp (Maybe (a,b)) type instance Eval (PairMaybeToMaybePair '( 'Nothing, _)) = 'Nothing@@ -51,11 +42,10 @@ -- | Id function. ----- === __Evample__+-- === __Example__ ----- >>> :kind! Eval (Id "id")--- Eval (Id "id") :: GHC.Types.Symbol+-- > :kind! Eval (Id "id")+-- Eval (Id "id") :: Symbol -- = "id" data Id :: a -> Exp a type instance Eval (Id a) = a-
src/Fcf/Alg/Sort.hs view
@@ -1,5 +1,3 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-}@@ -22,13 +20,13 @@ module Fcf.Alg.Sort where +import GHC.TypeLits (Symbol) import qualified GHC.TypeLits as TL import Fcf ( If, Eval, Exp, type (<=<), type (=<<) , Flip, Not, TyEq, Pure ) import Fcf.Data.List ( ZipWith, Filter, type (++) ) import Fcf.Data.Nat (Nat)-import Fcf.Data.Symbol (Symbol) -------------------------------------------------------------------------------- @@ -38,14 +36,6 @@ -------------------------------------------------------------------------------- --- For the doctests:---- $setup--- >>> import qualified Fcf.Data.Nat as N ( type (<) )--- >>> import qualified Fcf.Alg.Symbol as S ( type (<) )----------------------------------------------------------------------------------- -- helper for the ListCmp data ListCmpFnd :: [Ordering] -> Exp Ordering type instance Eval (ListCmpFnd '[]) = 'EQ@@ -69,7 +59,7 @@ ) -- | Comparison for the Nats.--- +-- -- TODO: Would this fit to Fcf.Data.Nat on first-class-families? data NatOrd :: Nat -> Nat -> Exp Ordering type instance Eval (NatOrd a b) = TL.CmpNat a b@@ -100,19 +90,19 @@ -- helper data Inord :: Algebra (BTreeF a) [a] type instance Eval (Inord 'BEmptyF) = '[]-type instance Eval (Inord ('BNodeF v l r)) = Eval (l ++ (Eval ('[v] ++ r)))+type instance Eval (Inord ('BNodeF v l r)) = Eval (l ++ Eval ('[v] ++ r)) -- | Qsort - give the comparison function @a -> a -> Exp Bool@ comparing your -- list elements and then Qsort will order the list.--- +-- -- __Example__ ----- >>> :kind! Eval (Qsort (N.<) '[5,3,1,9,4,6,3])--- Eval (Qsort (N.<) '[5,3,1,9,4,6,3]) :: [Nat]+-- > :kind! Eval (Qsort (N.<) '[5,3,1,9,4,6,3])+-- Eval (Qsort (N.<) '[5,3,1,9,4,6,3]) :: [TL.Natural] -- = '[1, 3, 3, 4, 5, 6, 9] ----- >>> :kind! Eval (Qsort (S.<) '[ "bb", "e", "a", "e", "d" ])+-- > :kind! Eval (Qsort (S.<) '[ "bb", "e", "a", "e", "d" ]) -- Eval (Qsort (S.<) '[ "bb", "e", "a", "e", "d" ]) :: [Symbol] -- = '["a", "bb", "d", "e", "e"] data Qsort :: (a -> a -> Exp Bool) -> [a] -> Exp [a]@@ -120,9 +110,7 @@ -- Helper ----- We use the Flip version so that using <-comparison will give an inreasing +-- We use the Flip version so that using <-comparison will give an inreasing -- Nat-list. Sorting would work without PartCmp. data PartCmp :: (a -> a -> Exp Bool) -> CoAlgebra (BTreeF a) [a] type instance Eval (PartCmp cmp coalg) = Eval (PartHlp (Flip cmp) coalg)--
src/Fcf/Alg/Symbol.hs view
@@ -1,5 +1,3 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-}@@ -56,7 +54,7 @@ -------------------------------------------------------------------------------- --- import GHC.TypeLits (Symbol)+import GHC.TypeLits (Symbol) import qualified GHC.TypeLits as TL import Fcf.Core (Eval, Exp)@@ -73,7 +71,7 @@ -- -- === __Example__ ----- >>> :kind! Eval (Append "hmm" " ok")+-- > :kind! Eval (Append "hmm" " ok") -- Eval (Append "hmm" " ok") :: Symbol -- = "hmm ok" data Append :: Symbol -> Symbol -> Exp Symbol@@ -84,15 +82,15 @@ -- -- === __Example__ ----- >>> :kind! Eval (Intercalate "+" '["aa", "bb", "cc"])+-- > :kind! Eval (Intercalate "+" '["aa", "bb", "cc"]) -- Eval (Intercalate "+" '["aa", "bb", "cc"]) :: Symbol -- = "aa+bb+cc" ----- >>> :kind! Eval (Intercalate "+" '["aa"])+-- > :kind! Eval (Intercalate "+" '["aa"]) -- Eval (Intercalate "+" '["aa"]) :: Symbol -- = "aa" ----- >>> :kind! Eval (Intercalate "+" '[])+-- > :kind! Eval (Intercalate "+" '[]) -- Eval (Intercalate "+" '[]) :: Symbol -- = "" data Intercalate :: Symbol -> [Symbol] -> Exp Symbol@@ -109,11 +107,11 @@ -- -- === __Example__ ----- >>> :kind! Eval (IsSpace "a")+-- > :kind! Eval (IsSpace "a") -- Eval (IsSpace "a") :: Bool -- = 'False ----- >>> :kind! Eval (IsSpace " ")+-- > :kind! Eval (IsSpace " ") -- Eval (IsSpace " ") :: Bool -- = 'True data IsSpace :: Symbol -> Exp Bool@@ -124,11 +122,11 @@ -- -- === __Example__ ----- >>> :kind! Eval (IsNewLine "a")+-- > :kind! Eval (IsNewLine "a") -- Eval (IsNewLine "a") :: Bool -- = 'False ----- >>> :kind! Eval (IsNewLine "\n")+-- > :kind! Eval (IsNewLine "\n") -- Eval (IsNewLine "\n") :: Bool -- = 'True data IsNewLine :: Symbol -> Exp Bool@@ -139,11 +137,11 @@ -- -- === __Example__ ----- >>> :kind! Eval (IsTab "a")+-- > :kind! Eval (IsTab "a") -- Eval (IsTab "a") :: Bool -- = 'False ----- >>> :kind! Eval (IsTab "\t")+-- > :kind! Eval (IsTab "\t") -- Eval (IsTab "\t") :: Bool -- = 'True data IsTab :: Symbol -> Exp Bool@@ -154,27 +152,27 @@ -- -- === __Example__ ----- >>> :kind! Eval (IsSpaceDelim "a")+-- > :kind! Eval (IsSpaceDelim "a") -- Eval (IsSpaceDelim "a") :: Bool -- = 'False ----- >>> :kind! Eval (IsSpaceDelim "\n")+-- > :kind! Eval (IsSpaceDelim "\n") -- Eval (IsSpaceDelim "\n") :: Bool -- = 'True data IsSpaceDelim :: Symbol -> Exp Bool type instance Eval (IsSpaceDelim s) =- Eval (Eval (IsSpace s) || (Eval (Eval (IsNewLine s) || Eval (IsTab s))))+ Eval (Eval (IsSpace s) || Eval (Eval (IsNewLine s) || Eval (IsTab s))) -- | IsDigit -- -- === __Example__ ----- >>> :kind! Eval (IsDigit "3")+-- > :kind! Eval (IsDigit "3") -- Eval (IsDigit "3") :: Bool -- = 'True ----- >>> :kind! Eval (IsDigit "a")+-- > :kind! Eval (IsDigit "a") -- Eval (IsDigit "a") :: Bool -- = 'False data IsDigit :: Symbol -> Exp Bool@@ -191,7 +189,7 @@ -- -- === __Example__ ----- >>> :kind! Eval (SymbolOrd "a" "b")+-- > :kind! Eval (SymbolOrd "a" "b") -- Eval (SymbolOrd "a" "b") :: Ordering -- = 'LT data SymbolOrd :: Symbol -> Symbol -> Exp Ordering@@ -201,10 +199,9 @@ -- -- === __Example__ ----- >>> :kind! Eval ("b" <= "a")+-- > :kind! Eval ("b" <= "a") -- Eval ("b" <= "a") :: Bool -- = 'False--- data (<=) :: Symbol -> Symbol -> Exp Bool type instance Eval ((<=) a b) = Eval (Eval (TyEq (TL.CmpSymbol a b) 'LT) || Eval (TyEq (TL.CmpSymbol a b) 'EQ))@@ -213,7 +210,7 @@ -- -- === __Example__ ----- >>> :kind! Eval ("b" >= "a")+-- > :kind! Eval ("b" >= "a") -- Eval ("b" >= "a") :: Bool -- = 'True data (>=) :: Symbol -> Symbol -> Exp Bool@@ -224,7 +221,7 @@ -- -- === __Example__ ----- >>> :kind! Eval ("a" < "b")+-- > :kind! Eval ("a" < "b") -- Eval ("a" < "b") :: Bool -- = 'True data (<) :: Symbol -> Symbol -> Exp Bool@@ -234,7 +231,7 @@ -- -- === __Example__ ----- >>> :kind! Eval ("b" > "a")+-- > :kind! Eval ("b" > "a") -- Eval ("b" > "a") :: Bool -- = 'True data (>) :: Symbol -> Symbol -> Exp Bool@@ -244,7 +241,7 @@ -- -- === __Example__ ----- >>> :kind! Eval ("b" == "a")+-- > :kind! Eval ("b" == "a") -- Eval ("b" == "a") :: Bool -- = 'False data (==) :: Symbol -> Symbol -> Exp Bool
src/Fcf/Alg/Tree.hs view
@@ -1,5 +1,3 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-}@@ -46,7 +44,7 @@ -- | A function to transform a Tree into fixed structure that can be used -- by Cata and Ana.--- +-- -- See the implementation of 'Size' for an example. data TreeToFix :: Tree a -> Exp (Fix (TreeF a)) type instance Eval (TreeToFix ('Node a '[])) = 'Fix ('NodeF a '[])@@ -55,38 +53,38 @@ -------------------------------------------------------------------------------- --- | Sum the nodes of TreeF containing Nats. --- +-- | Sum the nodes of TreeF containing Nats.+-- -- See the implementation of 'Fib' for an example. data SumNodesAlg :: Algebra (TreeF Nat) Nat type instance Eval (SumNodesAlg ('NodeF x '[])) = x-type instance Eval (SumNodesAlg ('NodeF x (b ': bs))) = x TL.+ (Eval (Sum (b ': bs)))+type instance Eval (SumNodesAlg ('NodeF x (b ': bs))) = x TL.+ Eval (Sum (b ': bs)) -- | Count the nodes of TreeF. --- +-- -- See the 'Size' for an example. data CountNodesAlg :: Algebra (TreeF a) Nat type instance Eval (CountNodesAlg ('NodeF x '[])) = 1-type instance Eval (CountNodesAlg ('NodeF x (b ': bs))) = 1 TL.+ (Eval (Sum (b ': bs)))+type instance Eval (CountNodesAlg ('NodeF x (b ': bs))) = 1 TL.+ Eval (Sum (b ': bs)) -- | Size of the Tree is the number of nodes in it.--- +-- -- __Example__ -- -- Size is defined as @ Cata CountNodesAlg =<< TreeToFix tr @--- and can be used with the following. +-- and can be used with the following. ----- >>> data BuildNode :: Nat -> Exp (Nat,[Nat])--- >>> :{+-- > data BuildNode :: Nat -> Exp (Nat,[Nat])+-- > :{ -- type instance Eval (BuildNode x) = -- If (Eval ((2 TL.* x TL.+ 1) >= 8)) -- '(x, '[]) -- '(x, '[ 2 TL.* x, (2 TL.* x) TL.+ 1 ]) -- :} ----- >>> :kind! Eval (Size =<< UnfoldTree BuildNode 1)--- Eval (Size =<< UnfoldTree BuildNode 1) :: Nat+-- > :kind! Eval (Size =<< UnfoldTree BuildNode 1)+-- Eval (Size =<< UnfoldTree BuildNode 1) :: TL.Natural -- = 7 data Size :: Tree a -> Exp Nat type instance Eval (Size tr) = Eval (Cata CountNodesAlg =<< TreeToFix tr)@@ -113,11 +111,11 @@ -- | Fibonaccis with Hylo, not efficient--- +-- -- __Example__ ----- >>> :kind! Eval (FibHylo 10)--- Eval (FibHylo 10) :: Nat+-- > :kind! Eval (FibHylo 10)+-- Eval (FibHylo 10) :: TL.Natural -- = 55 data FibHylo :: Nat -> Exp Nat type instance Eval (FibHylo n) = Eval (Hylo SumNodesAlg BuildFibTreeCoA n)@@ -143,13 +141,15 @@ type instance Eval (FSum ('NodeF a '[])) = 0 type instance Eval (FSum ('NodeF a (b ': bs))) = Eval (Sum (b ': bs)) + -- | Sizes example from Recursion Schemes by example, Tim Williams. This annotes -- each node with the size of its subtree. -- -- __Example__ ----- >>> :kind! Eval (Sizes =<< Ana BuildNodeCoA 1)--- Eval (Sizes =<< Ana BuildNodeCoA 1) :: Fix (AnnF (TreeF Nat) Nat)+-- > :kind! Eval (Sizes =<< Ana BuildNodeCoA 1)+-- Eval (Sizes =<< Ana BuildNodeCoA 1) :: Fix+-- (AnnF (TreeF TL.Natural) TL.Natural) -- = 'Fix -- ('AnnF -- '( 'NodeF@@ -169,7 +169,7 @@ -- 'Fix ('AnnF '( 'NodeF 7 '[], 1))], -- 3))], -- 7))-type instance Eval (Sizes fx) = Eval (Synthesize ( ( (+) 1) <=< FSum) fx)+type instance Eval (Sizes fx) = Eval (Synthesize ( (+) 1 <=< FSum) fx) data Sizes :: Fix f -> Exp (Ann f Nat) --------------------------------------------------------------------------------@@ -203,15 +203,13 @@ type instance Eval (FibAlgebra ('Succ ('Fix ('AnnF '( 'Succ ('Fix ('AnnF '( _, n))) , m) )))) = Eval (n + m) -- | Efficient Fibonacci type-level function--- (from Recursion Schemes by example, Tim Williams). Compare this to +-- (from Recursion Schemes by example, Tim Williams). Compare this to -- 'FibHylo'. -- -- __Example__ ----- >>> :kind! Eval (FibHisto 100)--- Eval (FibHisto 100) :: Nat+-- > :kind! Eval (FibHisto 100)+-- Eval (FibHisto 100) :: TL.Natural -- = 354224848179261915075 data FibHisto :: Nat -> Exp Nat type instance Eval (FibHisto n) = Eval (Histo FibAlgebra =<< NatToFix n)--
+ src/Fcf/Control/Monad.hs view
@@ -0,0 +1,431 @@+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wall #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{-|+Module : Fcf.Control.Monad+Description : Monad definitions+Copyright : (c) gspia 2020-+License : BSD+Maintainer : gspia++= Fcf.Control.Monad+++-}++--------------------------------------------------------------------------------++module Fcf.Control.Monad where++import Data.Functor.Identity+import GHC.TypeNats as TN++import Fcf hiding (type (<*>))+import Fcf.Class.Monoid (type (<>), MEmpty)+import Fcf.Data.Tuple++--------------------------------------------------------------------------------++-- For the doctests:++-- $setup+-- >>> import qualified GHC.TypeLits as TL+-- >>> import qualified Fcf.Combinators as C++--------------------------------------------------------------------------------+-- Functor instances++type instance Eval (Map f ('Identity a)) = 'Identity (Eval (f a))++--------------------------------------------------------------------------------+-- Common methods for both Applicative and Monad+++-- | Return corresponds to the 'return' at Monad+-- or 'pure' of Applicative.+--+--+-- :kind! Eval (Return 1) :: Maybe Nat+-- :kind! Eval (Return 1) :: Either Symbol Nat+data Return :: a -> Exp (m a)+type instance Eval (Return a) = '[a]+type instance Eval (Return a) = 'Just a+type instance Eval (Return a) = 'Right a+type instance Eval (Return a) = 'Identity a+type instance Eval (Return a) = '(MEmpty, a)+type instance Eval (Return a) = '(MEmpty, MEmpty, a)+type instance Eval (Return a) = '(MEmpty, MEmpty, MEmpty, a)+++--------------------------------------------------------------------------------+-- Applicative++-- | (<*>) corresponds to the value level '<*>'. Note that this clashes with+-- the definition given at Fcf.Combinators.((<*>)).+--+-- Applicatives that we define include:+--+-- - Identity+-- - []+-- - Maybe+-- - Either+-- - (,)+-- - (,,)+-- - (,,,)+--+-- === __Example__+--+-- >>> :kind! Eval ('Identity Plus2 <*> 'Identity 5)+-- Eval ('Identity Plus2 <*> 'Identity 5) :: Identity Natural+-- = 'Identity 7+--+-- >>> :kind! Eval ( (<*>) '[ (Fcf.+) 1, (Fcf.*) 10] '[4,5,6,7])+-- Eval ( (<*>) '[ (Fcf.+) 1, (Fcf.*) 10] '[4,5,6,7]) :: [Natural]+-- = '[5, 6, 7, 8, 40, 50, 60, 70]+-- >>> :kind! Eval ( (<*>) '[ (Fcf.+) 1, (Fcf.*) 10] '[])+-- Eval ( (<*>) '[ (Fcf.+) 1, (Fcf.*) 10] '[]) :: [Natural]+-- = '[]+-- >>> :kind! Eval ( (<*>) '[] '[4,5,6,7])+-- Eval ( (<*>) '[] '[4,5,6,7]) :: [b]+-- = '[]+--+--+data (<*>) :: f (a -> Exp b) -> f a -> Exp (f b)++type instance Eval ('Identity f <*> m) = Eval (Map f m)++type instance Eval ('[] <*> _) = '[]+type instance Eval (_ <*> '[]) = '[]+type instance Eval ((f ': fs) <*> (a ': as)) =+ Eval ((++) (Eval (Star_ f (a ': as))) (Eval ((<*>) fs (a ':as))))++-- Maybe+type instance Eval ('Nothing <*> _) = 'Nothing+type instance Eval ('Just f <*> m) = Eval (Map f m)++-- Either+type instance Eval ('Left e <*> _) = 'Left e+type instance Eval ('Right f <*> m) = Eval (Map f m)++-- | For tuples, the 'Monoid' constraint determines how the first values merge.+-- For example, 'Symbol's concatenate:+--+-- >>> :kind! Eval ('("hello", (Fcf.+) 15) <*> '("world!", 2002))+-- Eval ('("hello", (Fcf.+) 15) <*> '("world!", 2002)) :: (TL.Symbol,+-- Natural)+-- = '("helloworld!", 2017)+type instance Eval ('(u, f) <*> '(v, x)) = '(u <> v, Eval (f x))++-- ((,,) a b)+type instance Eval ('(a, b, f) <*> '(a', b', x)) = '(a <> a', b <> b', Eval (f x))++-- ((,,,) a b)+type instance Eval ('(a, b, c, f) <*> '(a', b', c', x)) = '(a <> a', b <> b', c <> c', Eval (f x))++-- | Type level LiftA2.+--+-- === __Example__+--+-- >>> :kind! Eval (LiftA2 (Fcf.+) '[1,2] '[3,4])+-- Eval (LiftA2 (Fcf.+) '[1,2] '[3,4]) :: [Natural]+-- = '[4, 5, 5, 6]+--+--+data LiftA2 :: (a -> b -> Exp c) -> f a -> f b -> Exp (f c)+type instance Eval (LiftA2 f fa fb) = Eval (Eval (Map (App2 f) fa) <*> fb)++-- | Type level LiftA3.+--+-- === __Example__+-- +-- >>> :kind! Eval (LiftA3 Tuple3 '[1,2] '[3,4] '[5,6])+-- Eval (LiftA3 Tuple3 '[1,2] '[3,4] '[5,6]) :: [(Natural, Natural,+-- Natural)]+-- = '[ '(1, 3, 5), '(1, 3, 6), '(1, 4, 5), '(1, 4, 6), '(2, 3, 5),+-- '(2, 3, 6), '(2, 4, 5), '(2, 4, 6)]+--+-- >>> :kind! Eval (LiftA3 Tuple3 ('Right 5) ('Right 6) ('Left "fail"))+-- Eval (LiftA3 Tuple3 ('Right 5) ('Right 6) ('Left "fail")) :: Either+-- TL.Symbol (Natural, Natural, c)+-- = 'Left "fail"+--+data LiftA3 :: (a -> b -> c -> Exp d) -> f a -> f b -> f c -> Exp (f d)+type instance Eval (LiftA3 f fa fb fc) = Eval (Eval (Eval (Map (App3 f) fa) <*> fb) <*> fc)++-- | Type level LiftA4.+data LiftA4 :: (a -> b -> c -> d -> Exp e) -> f a -> f b -> f c -> f d -> Exp (f e)+type instance Eval (LiftA4 f fa fb fc fd) = Eval (Eval (Eval (Eval (Map (App4 f) fa) <*> fb) <*> fc) <*> fd)++-- | Type level LiftA5.+data LiftA5 :: (a -> b -> c -> d -> e -> Exp g) -> f a -> f b -> f c -> f d -> f e -> Exp (f g)+type instance Eval (LiftA5 f fa fb fc fd fe) = Eval (Eval (Eval (Eval (Eval (Map (App5 f) fa) <*> fb) <*> fc) <*> fd) <*> fe)++--------------------------------------------------------------------------------+-- Monad+++-- | Type level Bind corresponding to the value level bind '>>=' operator.+-- Note that name (>>=) clashes with the definition given at+-- Fcf.Combinators.(>>=). (It doesn't export it yet, though.)+--+-- Monads that we define include:+--+-- - Identity+-- - []+-- - Maybe+-- - Either+-- - (,)+-- - (,,)+-- - (,,,)+--+-- === __Example__+--+-- Example: double the length of the input list and increase the numbers at+-- the same time.+--+-- >>> :kind! Eval ('[5,6,7] >>= Plus2M)+-- Eval ('[5,6,7] >>= Plus2M) :: [Natural]+-- = '[7, 8, 8, 9, 9, 10]+--+--+-- >>> :kind! Eval (XsPlusYsMonadic '[1,2,3] '[4,5,6])+-- Eval (XsPlusYsMonadic '[1,2,3] '[4,5,6]) :: [Natural]+-- = '[5, 6, 7, 6, 7, 8, 7, 8, 9]+data (>>=) :: m a -> (a -> Exp (m b)) -> Exp (m b)++-- Maybe+type instance Eval ('Nothing >>= f) = 'Nothing+type instance Eval ('Just a >>= f) = Eval (f a)++-- Either+type instance Eval ('Left a >>= _) = 'Left a+type instance Eval ('Right a >>= f) = Eval (f a)++-- Identity+type instance Eval ('Identity a >>= f) = Eval (f a)++-- Lists+type instance Eval ('[] >>= _) = '[]+type instance Eval ((x ': xs) >>= f) = Eval ((f @@ x) ++ Eval (xs >>= f))++-- (,)+type instance Eval ('(u, a) >>= k) = Eval ('(u, Id) <*> Eval (k a))++-- (,,)+type instance Eval ('(u, v, a) >>= k) = Eval ('(u, v, Id) <*> Eval (k a))++-- (,,,)+type instance Eval ('(u, v, w, a) >>= k) = Eval ('(u, v, w, Id) <*> Eval (k a))++-- | Type level >> +--+-- === __Example__+--+--+-- >>> :kind! Eval ( 'Just 1 >> 'Just 2)+-- Eval ( 'Just 1 >> 'Just 2) :: Maybe Natural+-- = 'Just 2+-- >>> :kind! Eval ( 'Nothing >> 'Just 2)+-- Eval ( 'Nothing >> 'Just 2) :: Maybe Natural+-- = 'Nothing+--+data (>>) :: m a -> m b -> Exp (m b)+type instance Eval (m >> k) = Eval (m >>= ConstFn k)++--------------------------------------------------------------------------------+-- MapM++-- | MapM+--+-- === __Example__+--+-- >>> :kind! Eval (MapM (ConstFn '[ 'True, 'False]) '["a","b","c"])+-- Eval (MapM (ConstFn '[ 'True, 'False]) '["a","b","c"]) :: [[Bool]]+-- = '[ '[ 'True, 'True, 'True], '[ 'True, 'True, 'False],+-- '[ 'True, 'False, 'True], '[ 'True, 'False, 'False],+-- '[ 'False, 'True, 'True], '[ 'False, 'True, 'False],+-- '[ 'False, 'False, 'True], '[ 'False, 'False, 'False]]+--+--+data MapM :: (a -> Exp (m b)) -> t a -> Exp (m (t b))+type instance Eval (MapM f ta) = Eval (Sequence (Map f @@ ta))+-- Above one is same as:+-- type instance Eval (MapM f ta) = Eval (Sequence (Eval (Map f ta)))+++-- | ForM = Flip MapM+data ForM :: t a -> (a -> Exp (m b)) -> Exp (m (t b))+type instance Eval (ForM ta f) = Eval (MapM f ta)+++--------------------------------------------------------------------------------+-- FoldlM++-- | FoldlM+--+-- === __Example__+--+-- >>> import GHC.TypeLits as TL (Symbol, type (-))+-- >>> data Lambda :: Nat -> Nat -> Exp (Either Symbol Natural)+-- >>> type instance Eval (Lambda a b) = If (Eval (a >= b)) ('Right (a TL.- b)) ('Left "Nat cannot be negative")+-- >>> :kind! Eval (FoldlM Lambda 5 '[1,1,1])+-- Eval (FoldlM Lambda 5 '[1,1,1]) :: Either Symbol Natural+-- = 'Right 2+-- >>> :kind! Eval (FoldlM Lambda 5 '[1,4,1])+-- Eval (FoldlM Lambda 5 '[1,4,1]) :: Either Symbol Natural+-- = 'Left "Nat cannot be negative"+--+data FoldlM :: (b -> a -> Exp (m b)) -> b -> t a -> Exp (m b)+type instance Eval (FoldlM f z0 xs) = Eval ((Eval (Foldr (FoldlMHelper f) Return xs)) z0)++--------------------------------------------------------------------------------+-- Traversable+++-- | Traverse+--+-- === __Example__+--+-- >>> :kind! Eval (Traverse Id '[ '[1,2], '[3,4]])+-- Eval (Traverse Id '[ '[1,2], '[3,4]]) :: [[Natural]]+-- = '[ '[1, 3], '[1, 4], '[2, 3], '[2, 4]]+--+--+data Traverse :: (a -> Exp (f b)) -> t a -> Exp (f (t b))+-- type instance Eval (Traverse f ta) = Eval (SequenceA =<< Map f ta)+-- Could the above one just be made to work? At the moment, the computation+-- diverges (we need to give the Traverse instances).++-- []+type instance Eval (Traverse f lst) =+ Eval (Foldr (ConsHelper f) (Eval (Return '[])) lst)++-- Maybe+type instance Eval (Traverse f 'Nothing) = Eval (Return 'Nothing)+type instance Eval (Traverse f ('Just x)) = Eval (Map (Pure1 'Just) (Eval (f x)))++-- Either+type instance Eval (Traverse f ('Left e)) = Eval (Return ('Left e))+type instance Eval (Traverse f ('Right x)) = Eval (Map (Pure1 'Right) (Eval (f x)))++-- ((,) a)+type instance Eval (Traverse f '(x, y)) = Eval (Map (Tuple2 x) (Eval (f y)))+++-- | Sequence+--+-- === __Example__+--+-- >>> :kind! Eval (Sequence ('Just ('Right 5)))+-- Eval (Sequence ('Just ('Right 5))) :: Either a (Maybe Natural)+-- = 'Right ('Just 5)+--+-- >>> :kind! Eval (Sequence '[ 'Just 3, 'Just 5, 'Just 7])+-- Eval (Sequence '[ 'Just 3, 'Just 5, 'Just 7]) :: Maybe [Natural]+-- = 'Just '[3, 5, 7]+--+-- >>> :kind! Eval (Sequence '[ 'Just 3, 'Nothing, 'Just 7])+-- Eval (Sequence '[ 'Just 3, 'Nothing, 'Just 7]) :: Maybe [Natural]+-- = 'Nothing+--+-- >>> :kind! Eval (Sequence '[ '[1,2], '[3,4]])+-- Eval (Sequence '[ '[1,2], '[3,4]]) :: [[Natural]]+-- = '[ '[1, 3], '[1, 4], '[2, 3], '[2, 4]]+--+--+data Sequence :: t (f a) -> Exp (f (t a))+type instance Eval (Sequence tfa) = Eval (Traverse Id tfa)++--------------------------------------------------------------------------------+-- Utility++-- | Id function correspondes to term level 'id'-function.+data Id :: a -> Exp a+type instance Eval (Id a) = a++--------------------------------------------------------------------------------+-- Helper Functions++-- | Needed by LiftA2 instance to partially apply function+data App2 :: (a -> b -> c) -> a -> Exp (b -> c)+type instance Eval (App2 f a) = f a++-- | Needed by LiftA3 instance to partially apply function+data App3 :: (a -> b -> c -> d) -> a -> Exp (b -> Exp (c -> d))+type instance Eval (App3 f a) = Pure2 f a++-- | Needed by LiftA4 instance to partially apply function+data App4 :: (a -> b -> c -> d -> e) -> a -> Exp (b -> Exp (c -> Exp (d -> e)))+type instance Eval (App4 f a) = App3 (f a)++-- | Needed by LiftA5 instance to partially apply function+data App5 :: (a -> b -> c -> d -> e -> g) -> a -> Exp (b -> Exp (c -> Exp (d -> Exp (e -> g))))+type instance Eval (App5 f a) = App4 (f a)++-- | Helper for the [] applicative instance.+data Star_ :: (a -> Exp b) -> f a -> Exp (f b)+type instance Eval (Star_ _ '[]) = '[]+type instance Eval (Star_ f (a ': as)) =+ Eval (f a) ': Eval (Star_ f as)++-- | Helper for 'FoldlM'+data FoldlMHelper :: (b -> a -> Exp (m b)) -> a -> (b -> Exp (m b)) -> Exp (b -> Exp (m b))+type instance Eval (FoldlMHelper f a b) = Flip (>>=) b <=< Flip f a++-- | Helper for [] traverse+data ConsHelper :: (a -> Exp (f b)) -> a -> f [b] -> Exp (f [b])+type instance Eval (ConsHelper f x ys) = Eval (LiftA2 (Pure2 '(:)) (Eval (f x)) ys)+-- The following would need an extra import line:+-- type instance Eval (Cons_f f x ys) = Eval (LiftA2 Cons (Eval (f x)) ys)+++--------------------------------------------------------------------------------+-- For Examples++-- | For Applicative documentation example+data Plus1 :: Nat -> Exp Nat+type instance Eval (Plus1 n) = n TN.+ 1++-- | For Applicative documentation example+data Plus2 :: Nat -> Exp Nat+type instance Eval (Plus2 n) = n TN.+ 2++-- | For the example. Turn an input number to list of two numbers of a bit+-- larger numbers.+data Plus2M :: Nat -> Exp [Nat]+type instance Eval (Plus2M n) = '[n TN.+ 2, n TN.+3]++-- | Part of an example+data PureXPlusY :: Nat -> Nat -> Exp [Nat]+type instance Eval (PureXPlusY x y) = Eval (Return ((TN.+) x y))++-- | Part of an example+data XPlusYs :: Nat -> [Nat] -> Exp [Nat]+type instance Eval (XPlusYs x ys) = Eval (ys >>= PureXPlusY x)++-- | An example implementing+--+-- sumM xs ys = do+-- x <- xs+-- y <- ys+-- return (x + y)+--+-- or+--+-- sumM xs ys = xs >>= (\x -> ys >>= (\y -> pure (x+y)))+--+-- Note the use of helper functions. This is a bit awkward, a type level+-- lambda would be nice.+data XsPlusYsMonadic :: [Nat] -> [Nat] -> Exp [Nat]+type instance Eval (XsPlusYsMonadic xs ys) = Eval (xs >>= Flip XPlusYs ys)++-- data Sumnd :: [Nat] -> [Nat] -> Exp [Nat]+-- type instance Eval (Sumnd xs ys) = xs >>=++-- data Sum2 :: Nat -> Nat -> Exp Nat+-- type instance Eval (Sum2 x y) = x TN.+ y
src/Fcf/Data/Bitree.hs view
@@ -1,5 +1,3 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-}@@ -26,8 +24,7 @@ module Fcf.Data.Bitree where import qualified GHC.TypeLits as TL-import Fcf as Fcf--- import Fcf.Data.List as Fcf+import Fcf import Fcf.Data.Nat as N --------------------------------------------------------------------------------@@ -101,7 +98,7 @@ data Flatten :: Tree a -> Exp [a] type instance Eval (Flatten ('Leaf a)) = '[a] type instance Eval (Flatten ('Node tr1 a tr2)) =- a ': Eval ((Eval (Flatten tr1)) ++ (Eval (Flatten tr2)))+ a ': Eval (Eval (Flatten tr1) ++ Eval (Flatten tr2)) -- | Get the root node from a 'Tree'. data GetRoot :: Tree a -> Exp a
+ src/Fcf/Data/Char.hs view
@@ -0,0 +1,200 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wall #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{-|+Module : Fcf.Data.Char+Description : Type-level Char data methods+Copyright : (c) gspia 2020-+License : BSD+Maintainer : gspia++= Fcf.Data.Char++-}++--------------------------------------------------------------------------------++module Fcf.Data.Char+ where+++-- Version should be larger than 9.2.x. Note the two digit space for the+-- minor.+#if __GLASGOW_HASKELL__ >= 902++import qualified GHC.TypeLits as TL+import Fcf.Core (Eval, Exp)+import Fcf.Data.Bool (type (||))+import Fcf.Data.List (Elem)+import Fcf.Utils (TyEq)++--------------------------------------------------------------------------------+++-- For the doctests:++-- $setup+ +--------------------------------------------------------------------------------++-- | IsSpace+--+-- === __Example__+--+-- >>> :kind! Eval (IsSpace 'a')+-- Eval (IsSpace 'a') :: Bool+-- = 'False+--+-- >>> :kind! Eval (IsSpace ' ')+-- Eval (IsSpace ' ') :: Bool+-- = 'True+data IsSpace :: Char -> Exp Bool+type instance Eval (IsSpace s) = Eval (s == ' ')+++-- | IsNewline+--+-- === __Example__+--+-- >>> :kind! Eval (IsNewLine 'a')+-- Eval (IsNewLine 'a') :: Bool+-- = 'False+--+-- >>> :kind! Eval (IsNewLine '\n')+-- Eval (IsNewLine '\n') :: Bool+-- = 'True+data IsNewLine :: Char -> Exp Bool+type instance Eval (IsNewLine s) = Eval (s == '\n')+++-- | IsTab+--+-- === __Example__+--+-- >>> :kind! Eval (IsTab 'a')+-- Eval (IsTab 'a') :: Bool+-- = 'False+--+-- >>> :kind! Eval (IsTab '\t')+-- Eval (IsTab '\t') :: Bool+-- = 'True+data IsTab :: Char -> Exp Bool+type instance Eval (IsTab s) = Eval (s == '\t')+++-- | IsSpaceDelim+--+-- === __Example__+--+-- >>> :kind! Eval (IsSpaceDelim 'a')+-- Eval (IsSpaceDelim 'a') :: Bool+-- = 'False+--+-- >>> :kind! Eval (IsSpaceDelim '\n')+-- Eval (IsSpaceDelim '\n') :: Bool+-- = 'True+data IsSpaceDelim :: Char -> Exp Bool+type instance Eval (IsSpaceDelim s) =+ Eval (Eval (IsSpace s) || Eval (Eval (IsNewLine s) || Eval (IsTab s)))+++-- | IsDigit+--+-- === __Example__+--+-- >>> :kind! Eval (IsDigit '3')+-- Eval (IsDigit '3') :: Bool+-- = 'True+--+-- >>> :kind! Eval (IsDigit 'a')+-- Eval (IsDigit 'a') :: Bool+-- = 'False+data IsDigit :: Char -> Exp Bool+type instance Eval (IsDigit s)+ = Eval (Elem s '[ '0','1','2','3','4','5','6','7','8','9'])+++--------------------------------------------------------------------------------+++-- | CharOrd - compare two symbols and give type-level Ordering+-- ( $ 'LT $, $ 'EQ $ or $ 'GT $ ).+--+-- === __Example__+--+-- >>> :kind! Eval (CharOrd 'a' 'b')+-- Eval (CharOrd 'a' 'b') :: Ordering+-- = 'LT+data CharOrd :: Char -> Char -> Exp Ordering+type instance Eval (CharOrd a b) = TL.CmpChar a b+ ++-- | Less-than-or-equal comparison for symbols.+--+-- === __Example__+--+-- >>> :kind! Eval ('b' <= 'a')+-- Eval ('b' <= 'a') :: Bool+-- = 'False+--+data (<=) :: Char -> Char -> Exp Bool+type instance Eval ((<=) a b) =+ Eval (Eval (TyEq (TL.CmpChar a b) 'LT) || Eval (TyEq (TL.CmpChar a b) 'EQ))++-- | Larger-than-or-equal comparison for symbols.+--+-- === __Example__+--+-- >>> :kind! Eval ('b' >= 'a')+-- Eval ('b' >= 'a') :: Bool+-- = 'True+data (>=) :: Char -> Char -> Exp Bool+type instance Eval ((>=) a b) =+ Eval (Eval (TyEq (TL.CmpChar a b) 'GT) || Eval (TyEq (TL.CmpChar a b) 'EQ))++-- | Less-than comparison for symbols.+--+-- === __Example__+--+-- >>> :kind! Eval ('a' < 'b')+-- Eval ('a' < 'b') :: Bool+-- = 'True+data (<) :: Char -> Char -> Exp Bool+type instance Eval ((<) a b) = Eval (TyEq (TL.CmpChar a b) 'LT)++-- | Larger-than comparison for symbols.+--+-- === __Example__+--+-- >>> :kind! Eval ('b' > 'a')+-- Eval ('b' > 'a') :: Bool+-- = 'True+data (>) :: Char -> Char -> Exp Bool+type instance Eval ((>) a b) = Eval (TyEq (TL.CmpChar a b) 'GT)++-- | Equality of symbols+--+-- === __Example__+--+-- >>> :kind! Eval ('b' == 'a')+-- Eval ('b' == 'a') :: Bool+-- = 'False+data (==) :: Char -> Char -> Exp Bool+type instance Eval ((==) a b) = Eval (TyEq (TL.CmpChar a b) 'EQ)++--------------------------------------------------------------------------------++#else++--------------------------------------------------------------------------------+++#endif++--------------------------------------------------------------------------------+
+ src/Fcf/Data/List/Utils.hs view
@@ -0,0 +1,59 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wall #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{-|+Module : Fcf.Data.List.Utils+Description : List helpers / utils+Copyright : (c) gspia 2023-+License : BSD+Maintainer : gspia++= Fcf.Data.List.Utils++Some of the following methods would probably have better place at the+first-class-families library. That is, polish and make a PR.++-}++--------------------------------------------------------------------------------++module Fcf.Data.List.Utils where++import Fcf+import Fcf.Data.List as Fcf++--------------------------------------------------------------------------------++-- For the doctests:++-- $setup+-- >>> import qualified GHC.TypeLits as TL+-- >>> import Fcf.Data.Nat++--------------------------------------------------------------------------------++-- | Foldl in terms of Foldr.+--+-- === __Example__+--+-- >>> :kind! Eval (Foldl (Fcf.-) 10 '[3,2,1])+-- Eval (Foldl (Fcf.-) 10 '[3,2,1]) :: TL.Natural+-- = 4+data Foldl :: (b -> a -> Exp b) -> b -> t a -> Exp b+type instance Eval (Foldl f b ta) = Eval (Foldr (Flip f) b (Eval (Reverse ta)))+++-- | Turn Maybe into a list.+--+-- === __Example__+--+-- >>> :kind! Eval (MaybeToList ('Just 1))+-- Eval (MaybeToList ('Just 1)) :: [TL.Natural]+-- = '[1]+data MaybeToList :: Maybe a -> Exp [a]+type instance Eval (MaybeToList 'Nothing) = '[]+type instance Eval (MaybeToList ('Just a)) = '[a]+
src/Fcf/Data/MapC.hs view
@@ -1,5 +1,3 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-}@@ -81,7 +79,7 @@ import Fcf ( Eval, Exp, Fst, Snd, type (=<<), type (<=<), type (@@) , type (++), Not, If , Pure, TyEq, Length, Uncurry)-import qualified Fcf as Fcf (Map, Foldr, Filter)+import qualified Fcf (Map, Foldr, Filter) import qualified Fcf.Data.List as L (Elem, Partition) import Fcf.Alg.Morphism@@ -94,42 +92,42 @@ -- $setup -- >>> import Fcf (type (>=)) -- >>> import Fcf.Data.Nat--- >>> import Fcf.Alg.Symbol (Symbol,Append)+-- >>> import Fcf.Data.Symbol -------------------------------------------------------------------------------- -- | A type corresponding to Map in the containers. We call this MapC because -- name Map is reserved to the map-function in Fcf-package.--- +-- -- The representation is based on type-level lists. Please, do not use--- that fact but rather use the exposed API. (We hope to change the +-- that fact but rather use the exposed API. (We hope to change the -- internal data type to balanced tree similar to the one used in containers. -- See TODO.md.)-data MapC k v = MapC [(k,v)]+newtype MapC k v = MapC [(k,v)] -- | Empty--- +-- -- === __Example__--- --- >>> :kind! (Eval Empty :: MapC Nat Symbol)--- (Eval Empty :: MapC Nat Symbol) :: MapC Nat Symbol+--+-- >>> :kind! (Eval Empty :: MapC Nat TL.Symbol)+-- (Eval Empty :: MapC Nat TL.Symbol) :: MapC TL.Natural TL.Symbol -- = 'MapC '[] -- -- >>> :kind! (Eval Empty :: MapC Int String) -- (Eval Empty :: MapC Int String) :: MapC Int [Char] -- = 'MapC '[]--- +-- -- See also the other examples in this module. data Empty :: Exp (MapC k v) type instance Eval Empty = 'MapC '[] -- | Singleton--- +-- -- === __Example__--- +-- -- >>> :kind! Eval (Singleton 1 "haa")--- Eval (Singleton 1 "haa") :: MapC Nat Symbol+-- Eval (Singleton 1 "haa") :: MapC TL.Natural TL.Symbol -- = 'MapC '[ '(1, "haa")] data Singleton :: k -> v -> Exp (MapC k v) type instance Eval (Singleton k v) = 'MapC '[ '(k,v)]@@ -137,9 +135,10 @@ -- | Use FromList to construct a MapC from type-level list. -- -- === __Example__--- +-- -- >>> :kind! Eval (FromList '[ '(1,"haa"), '(2,"hoo")])--- Eval (FromList '[ '(1,"haa"), '(2,"hoo")]) :: MapC Nat Symbol+-- Eval (FromList '[ '(1,"haa"), '(2,"hoo")]) :: MapC+-- TL.Natural TL.Symbol -- = 'MapC '[ '(1, "haa"), '(2, "hoo")] data FromList :: [(k,v)] -> Exp (MapC k v) type instance Eval (FromList lst) = 'MapC lst@@ -149,8 +148,8 @@ -- === __Example__ -- -- >>> :kind! Eval (Insert 3 "hih" =<< FromList '[ '(1,"haa"), '(2,"hoo")])--- Eval (Insert 3 "hih" =<< FromList '[ '(1,"haa"), '(2,"hoo")]) :: MapC --- Nat Symbol+-- Eval (Insert 3 "hih" =<< FromList '[ '(1,"haa"), '(2,"hoo")]) :: MapC+-- TL.Natural TL.Symbol -- = 'MapC '[ '(3, "hih"), '(1, "haa"), '(2, "hoo")] data Insert :: k -> v -> MapC k v -> Exp (MapC k v) type instance Eval (Insert k v ('MapC lst)) =@@ -164,18 +163,19 @@ -- if no old, add -- -- === __Example__--- --- >>> :kind! Eval (InsertWith Append 5 "xxx" =<< FromList '[ '(5,"a"), '(3,"b")])--- Eval (InsertWith Append 5 "xxx" =<< FromList '[ '(5,"a"), '(3,"b")]) :: MapC--- Nat Symbol+--+-- >>> :kind! Eval (InsertWith AppendSymbol 5 "xxx" =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (InsertWith AppendSymbol 5 "xxx" =<< FromList '[ '(5,"a"), '(3,"b")]) :: MapC+-- TL.Natural TL.Symbol -- = 'MapC '[ '(5, "xxxa"), '(3, "b")] ----- >>> :kind! Eval (InsertWith Append 7 "xxx" =<< FromList '[ '(5,"a"), '(3,"b")])--- Eval (InsertWith Append 7 "xxx" =<< FromList '[ '(5,"a"), '(3,"b")]) :: MapC--- Nat Symbol+-- >>> :kind! Eval (InsertWith AppendSymbol 7 "xxx" =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (InsertWith AppendSymbol 7 "xxx" =<< FromList '[ '(5,"a"), '(3,"b")]) :: MapC+-- TL.Natural TL.Symbol -- = 'MapC '[ '(5, "a"), '(3, "b"), '(7, "xxx")]--- >>> :kind! Eval (InsertWith Append 7 "xxx" =<< Empty)--- Eval (InsertWith Append 7 "xxx" =<< Empty) :: MapC Nat Symbol+-- >>> :kind! Eval (InsertWith AppendSymbol 7 "xxx" =<< Empty)+-- Eval (InsertWith AppendSymbol 7 "xxx" =<< Empty) :: MapC+-- TL.Natural TL.Symbol -- = 'MapC '[ '(7, "xxx")] data InsertWith :: (v -> v -> Exp v) -> k -> v -> MapC k v -> Exp (MapC k v) type instance Eval (InsertWith f k v ('MapC lst)) =@@ -192,42 +192,43 @@ -- | Delete--- +-- -- === __Example__--- +-- -- >>> :kind! Eval (Delete 5 =<< FromList '[ '(5,"a"), '(3,"b")]) -- Eval (Delete 5 =<< FromList '[ '(5,"a"), '(3,"b")]) :: MapC--- Nat Symbol+-- TL.Natural TL.Symbol -- = 'MapC '[ '(3, "b")] -- -- >>> :kind! Eval (Delete 7 =<< FromList '[ '(5,"a"), '(3,"b")]) -- Eval (Delete 7 =<< FromList '[ '(5,"a"), '(3,"b")]) :: MapC--- Nat Symbol+-- TL.Natural TL.Symbol -- = 'MapC '[ '(5, "a"), '(3, "b")] -- -- >>> :kind! Eval (Delete 7 =<< Empty)--- Eval (Delete 7 =<< Empty) :: MapC Nat v+-- Eval (Delete 7 =<< Empty) :: MapC TL.Natural v -- = 'MapC '[] data Delete :: k -> MapC k v -> Exp (MapC k v) type instance Eval (Delete k ('MapC lst)) = 'MapC (Eval (Fcf.Filter (Not <=< TyEq k <=< Fst) lst)) -- | Adjust--- +-- -- === __Example__--- --- >>> :kind! Eval (Adjust (Append "new ") 5 =<< FromList '[ '(5,"a"), '(3,"b")])--- Eval (Adjust (Append "new ") 5 =<< FromList '[ '(5,"a"), '(3,"b")]) :: MapC--- Nat Symbol+--+-- >>> :kind! Eval (Adjust (AppendSymbol "new ") 5 =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (Adjust (AppendSymbol "new ") 5 =<< FromList '[ '(5,"a"), '(3,"b")]) :: MapC+-- TL.Natural TL.Symbol -- = 'MapC '[ '(5, "new a"), '(3, "b")] ----- >>> :kind! Eval (Adjust (Append "new ") 7 =<< FromList '[ '(5,"a"), '(3,"b")])--- Eval (Adjust (Append "new ") 7 =<< FromList '[ '(5,"a"), '(3,"b")]) :: MapC--- Nat Symbol+-- >>> :kind! Eval (Adjust (AppendSymbol "new ") 7 =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (Adjust (AppendSymbol "new ") 7 =<< FromList '[ '(5,"a"), '(3,"b")]) :: MapC+-- TL.Natural TL.Symbol -- = 'MapC '[ '(5, "a"), '(3, "b")] ----- >>> :kind! Eval (Adjust (Append "new ") 7 =<< Empty)--- Eval (Adjust (Append "new ") 7 =<< Empty) :: MapC Nat Symbol+-- >>> :kind! Eval (Adjust (AppendSymbol "new ") 7 =<< Empty)+-- Eval (Adjust (AppendSymbol "new ") 7 =<< Empty) :: MapC+-- TL.Natural TL.Symbol -- = 'MapC '[] data Adjust :: (v -> Exp v) -> k -> MapC k v -> Exp (MapC k v) type instance Eval (Adjust f k ('MapC lst)) =@@ -244,13 +245,15 @@ -- | Lookup -- -- === __Example__--- +-- -- >>> :kind! Eval (Lookup 5 =<< FromList '[ '(5,"a"), '(3,"b")])--- Eval (Lookup 5 =<< FromList '[ '(5,"a"), '(3,"b")]) :: Maybe Symbol+-- Eval (Lookup 5 =<< FromList '[ '(5,"a"), '(3,"b")]) :: Maybe+-- TL.Symbol -- = 'Just "a" -- -- >>> :kind! Eval (Lookup 7 =<< FromList '[ '(5,"a"), '(3,"b")])--- Eval (Lookup 7 =<< FromList '[ '(5,"a"), '(3,"b")]) :: Maybe Symbol+-- Eval (Lookup 7 =<< FromList '[ '(5,"a"), '(3,"b")]) :: Maybe+-- TL.Symbol -- = 'Nothing data Lookup :: k -> MapC k v -> Exp (Maybe v) type instance Eval (Lookup k ('MapC '[])) = 'Nothing@@ -263,7 +266,7 @@ -- | Member -- -- === __Example__--- +-- -- >>> :kind! Eval (Member 5 =<< FromList '[ '(5,"a"), '(3,"b")]) -- Eval (Member 5 =<< FromList '[ '(5,"a"), '(3,"b")]) :: Bool -- = 'True@@ -277,7 +280,7 @@ -- | NotMember -- -- === __Example__--- +-- -- >>> :kind! Eval (NotMember 5 =<< FromList '[ '(5,"a"), '(3,"b")]) -- Eval (NotMember 5 =<< FromList '[ '(5,"a"), '(3,"b")]) :: Bool -- = 'False@@ -291,7 +294,7 @@ -- | Null -- -- === __Example__--- +-- -- >>> :kind! Eval (Null =<< FromList '[ '(5,"a"), '(3,"b")]) -- Eval (Null =<< FromList '[ '(5,"a"), '(3,"b")]) :: Bool -- = 'False@@ -305,9 +308,9 @@ -- | Size -- -- === __Example__--- +-- -- >>> :kind! Eval (Size =<< FromList '[ '(5,"a"), '(3,"b")])--- Eval (Size =<< FromList '[ '(5,"a"), '(3,"b")]) :: Nat+-- Eval (Size =<< FromList '[ '(5,"a"), '(3,"b")]) :: TL.Natural -- = 2 data Size :: MapC k v -> Exp TL.Nat type instance Eval (Size ('MapC lst)) = Eval (Length lst)@@ -315,11 +318,11 @@ -- | Union -- -- === __Example__--- +-- -- >>> :kind! Eval (Union (Eval (FromList '[ '(5,"a"), '(3,"b")])) (Eval (FromList '[ '(5,"A"), '(7,"c")])) )--- Eval (Union (Eval (FromList '[ '(5,"a"), '(3,"b")])) (Eval (FromList '[ '(5,"A"), '(7,"c")])) ) :: MapC --- Nat --- Symbol+-- Eval (Union (Eval (FromList '[ '(5,"a"), '(3,"b")])) (Eval (FromList '[ '(5,"A"), '(7,"c")])) ) :: MapC+-- TL.Natural+-- TL.Symbol -- = 'MapC '[ '(7, "c"), '(5, "a"), '(3, "b")] data Union :: MapC k v -> MapC k v -> Exp (MapC k v) type instance Eval (Union ('MapC lst1) ('MapC lst2)) =@@ -333,13 +336,13 @@ -- | Difference--- +-- -- === __Example__--- +-- -- >>> :kind! Eval (Difference (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(5,"B"), '(7,"C")])))--- Eval (Difference (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(5,"B"), '(7,"C")]))) :: MapC --- Nat --- Symbol+-- Eval (Difference (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(5,"B"), '(7,"C")]))) :: MapC+-- TL.Natural+-- TL.Symbol -- = 'MapC '[ '(3, "a")] data Difference :: MapC k v -> MapC k v -> Exp (MapC k v) type instance Eval (Difference mp1 mp2) =@@ -354,11 +357,11 @@ -- | Intersection -- -- === __Example__--- +-- -- >>> :kind! Eval (Intersection (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(5,"B"), '(7,"C")])))--- Eval (Intersection (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(5,"B"), '(7,"C")]))) :: MapC --- Nat --- Symbol+-- Eval (Intersection (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(5,"B"), '(7,"C")]))) :: MapC+-- TL.Natural+-- TL.Symbol -- = 'MapC '[ '(5, "b")] data Intersection :: MapC k v -> MapC k v -> Exp (MapC k v) type instance Eval (Intersection mp1 mp2) =@@ -372,7 +375,7 @@ -- | Disjoint -- -- === __Example__--- +-- -- >>> :kind! Eval (Disjoint (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(5,"B"), '(7,"C")]))) -- Eval (Disjoint (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(5,"B"), '(7,"C")]))) :: Bool -- = 'False@@ -388,21 +391,24 @@ Eval (Null =<< Intersection mp1 mp2) --- Map +-- | Map -- -- === __Example__ ----- >>> :kind! Eval (Fcf.Data.MapC.Map (Append "x") =<< FromList '[ '(5,"a"), '(3,"b")])--- Eval (Fcf.Data.MapC.Map (Append "x") =<< FromList '[ '(5,"a"), '(3,"b")]) :: MapC Nat Symbol+-- >>> :kind! Eval (Fcf.Data.MapC.Map (AppendSymbol "x") =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (Fcf.Data.MapC.Map (AppendSymbol "x") =<< FromList '[ '(5,"a"), '(3,"b")]) :: MapC+-- TL.Natural+-- TL.Symbol -- = 'MapC '[ '(5, "xa"), '(3, "xb")] data Map :: (v -> Exp w) -> MapC k v -> Exp (MapC k w) type instance Eval (Map f mp) = 'MapC (Eval (Fcf.Map (Second f) =<< Assocs mp)) --- MapWithKey ++-- | MapWithKey -- -- === __Example__--- +-- data MapWithKey :: (k -> v -> Exp w) -> MapC k v -> Exp (MapC k w) type instance Eval (MapWithKey f mp) = 'MapC (Eval (Fcf.Map (Second (Uncurry f))@@ -416,15 +422,15 @@ -- | Foldr ----- Fold the values in the map using the given right-associative binary operator, +-- Fold the values in the map using the given right-associative binary operator, -- such that 'foldr f z == foldr f z . elems'. -- -- Note: the order of values in MapC is not well defined at the moment. -- -- === __Example__--- +-- -- >>> :kind! Eval (Fcf.Data.MapC.Foldr (+) 0 =<< (FromList '[ '(1,1), '(2,2)]))--- Eval (Fcf.Data.MapC.Foldr (+) 0 =<< (FromList '[ '(1,1), '(2,2)])) :: Nat+-- Eval (Fcf.Data.MapC.Foldr (+) 0 =<< (FromList '[ '(1,1), '(2,2)])) :: TL.Natural -- = 3 data Foldr :: (v -> w -> Exp w) -> w -> MapC k v -> Exp w type instance Eval (Foldr f w mp) = Eval (Fcf.Foldr f w =<< Elems mp)@@ -433,9 +439,9 @@ -- | Elems -- -- === __Example__--- +-- -- >>> :kind! Eval (Elems =<< FromList '[ '(5,"a"), '(3,"b")])--- Eval (Elems =<< FromList '[ '(5,"a"), '(3,"b")]) :: [Symbol]+-- Eval (Elems =<< FromList '[ '(5,"a"), '(3,"b")]) :: [TL.Symbol] -- = '["a", "b"] -- >>> :kind! Eval (Elems =<< Empty) -- Eval (Elems =<< Empty) :: [v]@@ -446,9 +452,9 @@ -- | Keys -- -- === __Example__--- +-- -- >>> :kind! Eval (Keys =<< FromList '[ '(5,"a"), '(3,"b")])--- Eval (Keys =<< FromList '[ '(5,"a"), '(3,"b")]) :: [Nat]+-- Eval (Keys =<< FromList '[ '(5,"a"), '(3,"b")]) :: [TL.Natural] -- = '[5, 3] -- >>> :kind! Eval (Keys =<< Empty) -- Eval (Keys =<< Empty) :: [k]@@ -459,10 +465,10 @@ -- | Assocs -- -- === __Example__--- +-- -- >>> :kind! Eval (Assocs =<< FromList '[ '(5,"a"), '(3,"b")])--- Eval (Assocs =<< FromList '[ '(5,"a"), '(3,"b")]) :: [(Nat, --- Symbol)]+-- Eval (Assocs =<< FromList '[ '(5,"a"), '(3,"b")]) :: [(TL.Natural,+-- TL.Symbol)] -- = '[ '(5, "a"), '(3, "b")] -- >>> :kind! Eval (Assocs =<< Empty) -- Eval (Assocs =<< Empty) :: [(k, v)]@@ -473,10 +479,10 @@ -- | ToList -- -- === __Example__--- +-- -- >>> :kind! Eval (ToList =<< FromList '[ '(5,"a"), '(3,"b")])--- Eval (ToList =<< FromList '[ '(5,"a"), '(3,"b")]) :: [(Nat, --- Symbol)]+-- Eval (ToList =<< FromList '[ '(5,"a"), '(3,"b")]) :: [(TL.Natural,+-- TL.Symbol)] -- = '[ '(5, "a"), '(3, "b")] -- >>> :kind! Eval (ToList =<< Empty) -- Eval (ToList =<< Empty) :: [(k, v)]@@ -487,10 +493,10 @@ -- | Filter -- -- === __Example__--- +-- -- >>> :kind! Eval (Filter ((>=) 35) =<< FromList '[ '(5,50), '(3,30)])--- Eval (Filter ((>=) 35) =<< FromList '[ '(5,50), '(3,30)]) :: MapC --- Nat Nat+-- Eval (Filter ((>=) 35) =<< FromList '[ '(5,50), '(3,30)]) :: MapC+-- TL.Natural TL.Natural -- = 'MapC '[ '(3, 30)] data Filter :: (v -> Exp Bool) -> MapC k v -> Exp (MapC k v) type instance Eval (Filter f ('MapC lst)) =@@ -502,7 +508,7 @@ -- -- >>> :kind! Eval (FilterWithKey (>=) =<< FromList '[ '(3,5), '(6,4)]) -- Eval (FilterWithKey (>=) =<< FromList '[ '(3,5), '(6,4)]) :: MapC--- Nat Nat+-- TL.Natural TL.Natural -- = 'MapC '[ '(6, 4)] data FilterWithKey :: (k -> v -> Exp Bool) -> MapC k v -> Exp (MapC k v) type instance Eval (FilterWithKey f ('MapC lst)) =@@ -511,11 +517,11 @@ -- | Partition -- -- === __Example__--- +-- -- >>> :kind! Eval (Partition ((>=) 35) =<< FromList '[ '(5,50), '(3,30)])--- Eval (Partition ((>=) 35) =<< FromList '[ '(5,50), '(3,30)]) :: (MapC --- Nat Nat, --- MapC Nat Nat)+-- Eval (Partition ((>=) 35) =<< FromList '[ '(5,50), '(3,30)]) :: (MapC+-- TL.Natural TL.Natural,+-- MapC TL.Natural TL.Natural) -- = '( 'MapC '[ '(3, 30)], 'MapC '[ '(5, 50)]) data Partition :: (v -> Exp Bool) -> MapC k v -> Exp (MapC k v, MapC k v) type instance Eval (Partition f ('MapC lst)) =@@ -523,5 +529,4 @@ data PartitionHlp :: ([(k,v)],[(k,v)]) -> Exp (MapC k v, MapC k v) type instance Eval (PartitionHlp '(xs,ys)) = '( 'MapC xs, 'MapC ys)-
src/Fcf/Data/NatMap.hs view
@@ -1,5 +1,3 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-}@@ -74,7 +72,7 @@ import Fcf ( Eval, Exp, Fst, Snd, type (=<<), type (<=<), type (@@) , type (++), Not, If , Pure, TyEq, Length, Uncurry)-import qualified Fcf as Fcf (Map, Foldr, Filter)+import qualified Fcf (Map, Foldr, Filter) import qualified Fcf.Data.List as L (Elem, Partition) import Fcf.Data.Nat@@ -85,43 +83,44 @@ -- For the doctests: -- $setup+-- >>> import qualified GHC.TypeLits as TL -- >>> import Fcf (type (>=)) -- >>> import Fcf.Data.Nat--- >>> import Fcf.Alg.Symbol (Symbol,Append)+-- >>> import Fcf.Data.Symbol -------------------------------------------------------------------------------- -- | A type corresponding to IntMap in the containers.--- +-- -- The representation is based on type-level lists. Please, do not use--- that fact but rather use the exposed API. (We hope to change the +-- that fact but rather use the exposed API. (We hope to change the -- internal data type to balanced tree similar to the one used in containers. -- See TODO.md.)-data NatMap v = NatMap [(Nat,v)]+newtype NatMap v = NatMap [(Nat,v)] -- | Empty--- +-- -- === __Example__--- --- >>> :kind! (Eval Empty :: NatMap Symbol)--- (Eval Empty :: NatMap Symbol) :: NatMap Symbol+--+-- >>> :kind! (Eval Empty :: NatMap TL.Symbol)+-- (Eval Empty :: NatMap TL.Symbol) :: NatMap TL.Symbol -- = 'NatMap '[] -- -- >>> :kind! (Eval Empty :: NatMap String) -- (Eval Empty :: NatMap String) :: NatMap [Char] -- = 'NatMap '[]--- +-- -- See also the other examples in this module. data Empty :: Exp (NatMap v) type instance Eval Empty = 'NatMap '[] -- | Singleton--- +-- -- === __Example__--- +-- -- >>> :kind! Eval (Singleton 1 "haa")--- Eval (Singleton 1 "haa") :: NatMap Symbol+-- Eval (Singleton 1 "haa") :: NatMap TL.Symbol -- = 'NatMap '[ '(1, "haa")] data Singleton :: Nat -> v -> Exp (NatMap v) type instance Eval (Singleton k v) = 'NatMap '[ '(k,v)]@@ -129,9 +128,9 @@ -- | Use FromList to construct a NatMap from type-level list. -- -- === __Example__--- +-- -- >>> :kind! Eval (FromList '[ '(1,"haa"), '(2,"hoo")])--- Eval (FromList '[ '(1,"haa"), '(2,"hoo")]) :: NatMap Symbol+-- Eval (FromList '[ '(1,"haa"), '(2,"hoo")]) :: NatMap TL.Symbol -- = 'NatMap '[ '(1, "haa"), '(2, "hoo")] data FromList :: [(Nat,v)] -> Exp (NatMap v) type instance Eval (FromList lst) = 'NatMap lst@@ -141,8 +140,8 @@ -- === __Example__ -- -- >>> :kind! Eval (Insert 3 "hih" =<< FromList '[ '(1,"haa"), '(2,"hoo")])--- Eval (Insert 3 "hih" =<< FromList '[ '(1,"haa"), '(2,"hoo")]) :: NatMap --- Symbol+-- Eval (Insert 3 "hih" =<< FromList '[ '(1,"haa"), '(2,"hoo")]) :: NatMap+-- TL.Symbol -- = 'NatMap '[ '(3, "hih"), '(1, "haa"), '(2, "hoo")] data Insert :: Nat -> v -> NatMap v -> Exp (NatMap v) type instance Eval (Insert k v ('NatMap lst)) =@@ -158,19 +157,20 @@ -- if no old, add -- -- === __Example__--- --- >>> :kind! Eval (InsertWith Append 5 "xxx" =<< FromList '[ '(5,"a"), '(3,"b")])--- Eval (InsertWith Append 5 "xxx" =<< FromList '[ '(5,"a"), '(3,"b")]) :: NatMap--- Symbol+--+-- >>> :kind! Eval (InsertWith AppendSymbol 5 "xxx" =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (InsertWith AppendSymbol 5 "xxx" =<< FromList '[ '(5,"a"), '(3,"b")]) :: NatMap+-- TL.Symbol -- = 'NatMap '[ '(5, "xxxa"), '(3, "b")] ----- >>> :kind! Eval (InsertWith Append 7 "xxx" =<< FromList '[ '(5,"a"), '(3,"b")])--- Eval (InsertWith Append 7 "xxx" =<< FromList '[ '(5,"a"), '(3,"b")]) :: NatMap--- Symbol+-- >>> :kind! Eval (InsertWith AppendSymbol 7 "xxx" =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (InsertWith AppendSymbol 7 "xxx" =<< FromList '[ '(5,"a"), '(3,"b")]) :: NatMap+-- TL.Symbol -- = 'NatMap '[ '(5, "a"), '(3, "b"), '(7, "xxx")] ----- >>> :kind! Eval (InsertWith Append 7 "xxx" =<< Empty)--- Eval (InsertWith Append 7 "xxx" =<< Empty) :: NatMap Symbol+-- >>> :kind! Eval (InsertWith AppendSymbol 7 "xxx" =<< Empty)+-- Eval (InsertWith AppendSymbol 7 "xxx" =<< Empty) :: NatMap+-- TL.Symbol -- = 'NatMap '[ '(7, "xxx")] data InsertWith :: (v -> v -> Exp v) -> Nat -> v -> NatMap v -> Exp (NatMap v) type instance Eval (InsertWith f k v ('NatMap lst)) =@@ -187,17 +187,17 @@ -- | Delete--- +-- -- === __Example__--- +-- -- >>> :kind! Eval (Delete 5 =<< FromList '[ '(5,"a"), '(3,"b")]) -- Eval (Delete 5 =<< FromList '[ '(5,"a"), '(3,"b")]) :: NatMap--- Symbol+-- TL.Symbol -- = 'NatMap '[ '(3, "b")] -- -- >>> :kind! Eval (Delete 7 =<< FromList '[ '(5,"a"), '(3,"b")]) -- Eval (Delete 7 =<< FromList '[ '(5,"a"), '(3,"b")]) :: NatMap--- Symbol+-- TL.Symbol -- = 'NatMap '[ '(5, "a"), '(3, "b")] -- -- >>> :kind! Eval (Delete 7 =<< Empty)@@ -208,21 +208,21 @@ 'NatMap (Eval (Fcf.Filter (Not <=< TyEq k <=< Fst) lst)) -- | Adjust--- +-- -- === __Example__--- --- >>> :kind! Eval (Adjust (Append "new ") 5 =<< FromList '[ '(5,"a"), '(3,"b")])--- Eval (Adjust (Append "new ") 5 =<< FromList '[ '(5,"a"), '(3,"b")]) :: NatMap--- Symbol+--+-- >>> :kind! Eval (Adjust (AppendSymbol "new ") 5 =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (Adjust (AppendSymbol "new ") 5 =<< FromList '[ '(5,"a"), '(3,"b")]) :: NatMap+-- TL.Symbol -- = 'NatMap '[ '(5, "new a"), '(3, "b")] ----- >>> :kind! Eval (Adjust (Append "new ") 7 =<< FromList '[ '(5,"a"), '(3,"b")])--- Eval (Adjust (Append "new ") 7 =<< FromList '[ '(5,"a"), '(3,"b")]) :: NatMap--- Symbol+-- >>> :kind! Eval (Adjust (AppendSymbol "new ") 7 =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (Adjust (AppendSymbol "new ") 7 =<< FromList '[ '(5,"a"), '(3,"b")]) :: NatMap+-- TL.Symbol -- = 'NatMap '[ '(5, "a"), '(3, "b")] ----- >>> :kind! Eval (Adjust (Append "new ") 7 =<< Empty)--- Eval (Adjust (Append "new ") 7 =<< Empty) :: NatMap Symbol+-- >>> :kind! Eval (Adjust (AppendSymbol "new ") 7 =<< Empty)+-- Eval (Adjust (AppendSymbol "new ") 7 =<< Empty) :: NatMap TL.Symbol -- = 'NatMap '[] data Adjust :: (v -> Exp v) -> Nat -> NatMap v -> Exp (NatMap v) type instance Eval (Adjust f k ('NatMap lst)) =@@ -239,13 +239,15 @@ -- | Lookup -- -- === __Example__--- +-- -- >>> :kind! Eval (Lookup 5 =<< FromList '[ '(5,"a"), '(3,"b")])--- Eval (Lookup 5 =<< FromList '[ '(5,"a"), '(3,"b")]) :: Maybe Symbol+-- Eval (Lookup 5 =<< FromList '[ '(5,"a"), '(3,"b")]) :: Maybe+-- TL.Symbol -- = 'Just "a" -- -- >>> :kind! Eval (Lookup 7 =<< FromList '[ '(5,"a"), '(3,"b")])--- Eval (Lookup 7 =<< FromList '[ '(5,"a"), '(3,"b")]) :: Maybe Symbol+-- Eval (Lookup 7 =<< FromList '[ '(5,"a"), '(3,"b")]) :: Maybe+-- TL.Symbol -- = 'Nothing data Lookup :: Nat -> NatMap v -> Exp (Maybe v) type instance Eval (Lookup k ('NatMap '[])) = 'Nothing@@ -258,7 +260,7 @@ -- | Member -- -- === __Example__--- +-- -- >>> :kind! Eval (Member 5 =<< FromList '[ '(5,"a"), '(3,"b")]) -- Eval (Member 5 =<< FromList '[ '(5,"a"), '(3,"b")]) :: Bool -- = 'True@@ -272,7 +274,7 @@ -- | NotMember -- -- === __Example__--- +-- -- >>> :kind! Eval (NotMember 5 =<< FromList '[ '(5,"a"), '(3,"b")]) -- Eval (NotMember 5 =<< FromList '[ '(5,"a"), '(3,"b")]) :: Bool -- = 'False@@ -286,7 +288,7 @@ -- | Null -- -- === __Example__--- +-- -- >>> :kind! Eval (Null =<< FromList '[ '(5,"a"), '(3,"b")]) -- Eval (Null =<< FromList '[ '(5,"a"), '(3,"b")]) :: Bool -- = 'False@@ -300,9 +302,9 @@ -- | Size -- -- === __Example__--- +-- -- >>> :kind! Eval (Size =<< FromList '[ '(5,"a"), '(3,"b")])--- Eval (Size =<< FromList '[ '(5,"a"), '(3,"b")]) :: Nat+-- Eval (Size =<< FromList '[ '(5,"a"), '(3,"b")]) :: TL.Natural -- = 2 data Size :: NatMap v -> Exp Nat type instance Eval (Size ('NatMap lst)) = Eval (Length lst)@@ -310,10 +312,10 @@ -- | Union -- -- === __Example__--- +-- -- >>> :kind! Eval (Union (Eval (FromList '[ '(5,"a"), '(3,"b")])) (Eval (FromList '[ '(5,"A"), '(7,"c")])) )--- Eval (Union (Eval (FromList '[ '(5,"a"), '(3,"b")])) (Eval (FromList '[ '(5,"A"), '(7,"c")])) ) :: NatMap --- Symbol+-- Eval (Union (Eval (FromList '[ '(5,"a"), '(3,"b")])) (Eval (FromList '[ '(5,"A"), '(7,"c")])) ) :: NatMap+-- TL.Symbol -- = 'NatMap '[ '(7, "c"), '(5, "a"), '(3, "b")] data Union :: NatMap v -> NatMap v -> Exp (NatMap v) type instance Eval (Union ('NatMap lst1) ('NatMap lst2)) =@@ -327,12 +329,12 @@ -- | Difference--- +-- -- === __Example__--- +-- -- >>> :kind! Eval (Difference (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(5,"B"), '(7,"C")])))--- Eval (Difference (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(5,"B"), '(7,"C")]))) :: NatMap --- Symbol+-- Eval (Difference (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(5,"B"), '(7,"C")]))) :: NatMap+-- TL.Symbol -- = 'NatMap '[ '(3, "a")] data Difference :: NatMap v -> NatMap v -> Exp (NatMap v) type instance Eval (Difference mp1 mp2) =@@ -347,10 +349,10 @@ -- | Intersection -- -- === __Example__--- +-- -- >>> :kind! Eval (Intersection (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(5,"B"), '(7,"C")])))--- Eval (Intersection (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(5,"B"), '(7,"C")]))) :: NatMap --- Symbol+-- Eval (Intersection (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(5,"B"), '(7,"C")]))) :: NatMap+-- TL.Symbol -- = 'NatMap '[ '(5, "b")] data Intersection :: NatMap v -> NatMap v -> Exp (NatMap v) type instance Eval (Intersection mp1 mp2) =@@ -364,7 +366,7 @@ -- | Disjoint -- -- === __Example__--- +-- -- >>> :kind! Eval (Disjoint (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(5,"B"), '(7,"C")]))) -- Eval (Disjoint (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(5,"B"), '(7,"C")]))) :: Bool -- = 'False@@ -384,9 +386,9 @@ -- -- === __Example__ ----- >>> :kind! Eval (Fcf.Data.NatMap.Map (Append "x") =<< FromList '[ '(5,"a"), '(3,"b")])--- Eval (Fcf.Data.NatMap.Map (Append "x") =<< FromList '[ '(5,"a"), '(3,"b")]) :: NatMap --- Symbol+-- >>> :kind! Eval (Fcf.Data.NatMap.Map (AppendSymbol "x") =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (Fcf.Data.NatMap.Map (AppendSymbol "x") =<< FromList '[ '(5,"a"), '(3,"b")]) :: NatMap+-- TL.Symbol -- = 'NatMap '[ '(5, "xa"), '(3, "xb")] data Map :: (v -> Exp w) -> NatMap v -> Exp (NatMap w) type instance Eval (Map f mp) =@@ -395,7 +397,7 @@ -- | NatMapWithKey -- -- === __Example__--- +-- data NatMapWithKey :: (Nat -> v -> Exp w) -> NatMap v -> Exp (NatMap w) type instance Eval (NatMapWithKey f mp) = 'NatMap (Eval (Fcf.Map (Second (Uncurry f))@@ -409,15 +411,15 @@ -- | Foldr ----- Fold the values in the map using the given right-associative binary operator, +-- Fold the values in the map using the given right-associative binary operator, -- such that 'foldr f z == foldr f z . elems'. -- -- Note: the order of values in NatMap is not well defined at the moment. -- -- === __Example__--- +-- -- >>> :kind! Eval (Fcf.Data.NatMap.Foldr (+) 0 =<< (FromList '[ '(1,1), '(2,2)]))--- Eval (Fcf.Data.NatMap.Foldr (+) 0 =<< (FromList '[ '(1,1), '(2,2)])) :: Nat+-- Eval (Fcf.Data.NatMap.Foldr (+) 0 =<< (FromList '[ '(1,1), '(2,2)])) :: TL.Natural -- = 3 data Foldr :: (v -> w -> Exp w) -> w -> NatMap v -> Exp w type instance Eval (Foldr f w mp) = Eval (Fcf.Foldr f w =<< Elems mp)@@ -426,9 +428,9 @@ -- | Elems -- -- === __Example__--- +-- -- >>> :kind! Eval (Elems =<< FromList '[ '(5,"a"), '(3,"b")])--- Eval (Elems =<< FromList '[ '(5,"a"), '(3,"b")]) :: [Symbol]+-- Eval (Elems =<< FromList '[ '(5,"a"), '(3,"b")]) :: [TL.Symbol] -- = '["a", "b"] -- >>> :kind! Eval (Elems =<< Empty) -- Eval (Elems =<< Empty) :: [v]@@ -439,12 +441,12 @@ -- | Keys -- -- === __Example__--- +-- -- >>> :kind! Eval (Keys =<< FromList '[ '(5,"a"), '(3,"b")])--- Eval (Keys =<< FromList '[ '(5,"a"), '(3,"b")]) :: [Nat]+-- Eval (Keys =<< FromList '[ '(5,"a"), '(3,"b")]) :: [TL.Natural] -- = '[5, 3] -- >>> :kind! Eval (Keys =<< Empty)--- Eval (Keys =<< Empty) :: [Nat]+-- Eval (Keys =<< Empty) :: [TL.Natural] -- = '[] data Keys :: NatMap v -> Exp [Nat] type instance Eval (Keys ('NatMap lst)) = Eval (Fcf.Map Fst lst)@@ -452,13 +454,13 @@ -- | Assocs -- -- === __Example__--- +-- -- >>> :kind! Eval (Assocs =<< FromList '[ '(5,"a"), '(3,"b")])--- Eval (Assocs =<< FromList '[ '(5,"a"), '(3,"b")]) :: [(Nat, --- Symbol)]+-- Eval (Assocs =<< FromList '[ '(5,"a"), '(3,"b")]) :: [(TL.Natural,+-- TL.Symbol)] -- = '[ '(5, "a"), '(3, "b")] -- >>> :kind! Eval (Assocs =<< Empty)--- Eval (Assocs =<< Empty) :: [(Nat, v)]+-- Eval (Assocs =<< Empty) :: [(TL.Natural, v)] -- = '[] data Assocs :: NatMap v -> Exp [(Nat,v)] type instance Eval (Assocs ('NatMap lst)) = lst@@ -466,13 +468,13 @@ -- | ToList -- -- === __Example__--- +-- -- >>> :kind! Eval (ToList =<< FromList '[ '(5,"a"), '(3,"b")])--- Eval (ToList =<< FromList '[ '(5,"a"), '(3,"b")]) :: [(Nat, --- Symbol)]+-- Eval (ToList =<< FromList '[ '(5,"a"), '(3,"b")]) :: [(TL.Natural,+-- TL.Symbol)] -- = '[ '(5, "a"), '(3, "b")] -- >>> :kind! Eval (ToList =<< Empty)--- Eval (ToList =<< Empty) :: [(Nat, v)]+-- Eval (ToList =<< Empty) :: [(TL.Natural, v)] -- = '[] data ToList :: NatMap v -> Exp [(Nat,v)] type instance Eval (ToList ('NatMap lst)) = lst@@ -480,10 +482,10 @@ -- | Filter -- -- === __Example__--- +-- -- >>> :kind! Eval (Filter ((>=) 35) =<< FromList '[ '(5,50), '(3,30)])--- Eval (Filter ((>=) 35) =<< FromList '[ '(5,50), '(3,30)]) :: NatMap --- Nat+-- Eval (Filter ((>=) 35) =<< FromList '[ '(5,50), '(3,30)]) :: NatMap+-- TL.Natural -- = 'NatMap '[ '(3, 30)] data Filter :: (v -> Exp Bool) -> NatMap v -> Exp (NatMap v) type instance Eval (Filter f ('NatMap lst)) =@@ -495,7 +497,7 @@ -- -- >>> :kind! Eval (FilterWithKey (>=) =<< FromList '[ '(3,5), '(6,4)]) -- Eval (FilterWithKey (>=) =<< FromList '[ '(3,5), '(6,4)]) :: NatMap--- Nat+-- TL.Natural -- = 'NatMap '[ '(6, 4)] data FilterWithKey :: (Nat -> v -> Exp Bool) -> NatMap v -> Exp (NatMap v) type instance Eval (FilterWithKey f ('NatMap lst)) =@@ -504,11 +506,11 @@ -- | Partition -- -- === __Example__--- +-- -- >>> :kind! Eval (Partition ((>=) 35) =<< FromList '[ '(5,50), '(3,30)])--- Eval (Partition ((>=) 35) =<< FromList '[ '(5,50), '(3,30)]) :: (NatMap --- Nat, --- NatMap Nat)+-- Eval (Partition ((>=) 35) =<< FromList '[ '(5,50), '(3,30)]) :: (NatMap+-- TL.Natural,+-- NatMap TL.Natural) -- = '( 'NatMap '[ '(3, 30)], 'NatMap '[ '(5, 50)]) data Partition :: (v -> Exp Bool) -> NatMap v -> Exp (NatMap v, NatMap v) type instance Eval (Partition f ('NatMap lst)) =@@ -516,5 +518,4 @@ data PartitionHlp :: ([(Nat,v)],[(Nat,v)]) -> Exp (NatMap v, NatMap v) type instance Eval (PartitionHlp '(xs,ys)) = '( 'NatMap xs, 'NatMap ys)-
+ src/Fcf/Data/NewText.hs view
@@ -0,0 +1,1035 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wall #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{-|+Module : Fcf.Data.NewText+Description : Type-level Text data structure with methods+Copyright : (c) gspia 2020-+License : BSD+Maintainer : gspia++= Fcf.Data.NewText++We mimick Data.Text but on type level. The current internal representation+of Fcf.Data.Text is based+on type level lists. The current (as of early 2023) implementation of this+Fcf.Data.Text will be deprecated and replaced with the contents of Fcf.Data.NewText+later 2023 as newer version GHC become more widespread.++The old version working with 9.0.x or less will be kept at Fcf.Data.OldText for+some time. Similarly, the module Fcf.Data.NewText contains the functions+and definitions for better Text type, which will be taken into use after some time.++The Fcf.Data.NewText will replace Fcf.Data.Text eventually.++-}++--------------------------------------------------------------------------------++module Fcf.Data.NewText+#if __GLASGOW_HASKELL__ >= 902+ ( Text (..)++ -- * Creation+ , Empty+ , Singleton+ , FromList+ , FromSymbolList+ , FromSymbol+ , ToList+ , ToSymbolList+ , ToCharList+ , Unpack++ -- * Basic Interface+ , Null+ , Length+ , Append+ , Cons+ , ConsSymbol+ , Snoc+ , SnocSymbol+ , Uncons+ , Unsnoc+ , Head+ , Last+ , Tail+ , Init+ , CompareLength++ -- * Transformation+ , FMap+ , FMapSymbol+ , FMapT+ , Intercalate+ , Intersperse+ , IntersperseSymbol+ , Reverse+ , Replace++ -- * Special Folds+ , Concat+ , ConcatMap+ , ConcatMapSymbol+ , ConcatMapCS+ , Any+ , AnySymbol+ , All+ , AllSymbol++ -- * Substrings+ , Take+ , TakeEnd+ , Drop+ , DropEnd+ , TakeWhile+ , TakeWhileSymbol+ , TakeWhileEnd+ , TakeWhileEndSymbol+ , DropWhile+ , DropWhileEnd+ , DropWhileEndSymbol+ , DropAround+ , DropAroundSymbol+ , Strip++ -- * Breaking etc+ , SplitOn+ , Split+ , Lines+ , Words+ , Unlines+ , Unwords++ -- * Predicates+ , IsPrefixOf+ , IsSuffixOf+ , IsInfixOf+ )+#endif+ where++-- Version should be larger than 9.2.x. Note the two digit space for the+-- minor.+#if __GLASGOW_HASKELL__ >= 902++import GHC.TypeLits (Symbol)+import qualified GHC.TypeLits as TL++import Fcf ( If, Eval, Exp, type (=<<), type (@@)+ , Flip, Pure, IsNothing, Fst, Snd)+import qualified Fcf.Class.Foldable as F (All, Any)+import Fcf.Data.List ( type (++) )+import qualified Fcf.Data.List as F+ ( Length, Init, Reverse, Take, Drop, TakeWhile, DropWhile+ , Intercalate, Intersperse, IsPrefixOf, IsSuffixOf, IsInfixOf, Snoc)++import qualified Fcf.Class.Functor as F ( FMap )+++import Fcf.Data.Nat (Nat)+import qualified Fcf.Data.Symbol as S+import Fcf.Data.Tuple (Swap)+import Fcf.Alg.Other ( PairMaybeToMaybePair )+import Fcf.Alg.Morphism (First,Second)+-- import Fcf.Alg.Nat (type (==))+import qualified Fcf.Alg.Symbol as Sym++--------------------------------------------------------------------------------+++-- For the doctests:++-- $setup+-- >>> import Fcf (type (<=<), Not)+-- >>> import Fcf.Data.Char as C++--------------------------------------------------------------------------------++-- | 'Text' is a data structure, that is, a list to hold type-level symbols of+-- length one.+data Text = Text Symbol++--------------------------------------------------------------------------------++-- | Empty+--+-- === __Example__+--+-- >>> :kind! (Eval Empty :: Text)+-- (Eval Empty :: Text) :: Text+-- = 'Text ""+--+-- See also the other examples in this module.+data Empty :: Exp Text+type instance Eval Empty = 'Text ""++-- | Singleton+--+-- >>> :kind! Eval (Singleton 'a')+-- Eval (Singleton 'a') :: Text+-- = 'Text "a"+data Singleton :: Char -> Exp Text+type instance Eval (Singleton c) = Eval (FromSymbol =<< S.CharToSymbol c)+++-- | FromSymbol+--+-- === __Example__+--+-- >>> :kind! Eval (FromSymbol "some text")+-- Eval (FromSymbol "some text") :: Text+-- = 'Text "some text"+data FromSymbol :: Symbol -> Exp Text+type instance Eval (FromSymbol s) = 'Text s+++-- | Use FromList to construct a Text from type-level list.+--+-- === __Example__+--+-- :kind! Eval (FromSymbolList '["h", "e", "l", "l", "u", "r", "e", "i"])+-- Eval (FromSymbolList '["h", "e", "l", "l", "u", "r", "e", "i"]) :: Text+-- = 'Text "hellurei"+data FromSymbolList :: [Symbol] -> Exp Text+type instance Eval (FromSymbolList sym) = Eval (FromSymbol =<< S.Concat sym)+++data FromList :: [Text] -> Exp Text+type instance Eval (FromList txt) =+ Eval (FromSymbol =<< S.Concat =<< F.FMap Unpack txt)+-- hmm, this is also a Monoid, so we should be able to use Concat+ ++-- | Get the type-level list out of the 'Text'.+--+-- === __Example__+--+-- >>> :kind! Eval (ToSymbolList =<< FromSymbolList '["a", "b"])+-- Eval (ToSymbolList =<< FromSymbolList '["a", "b"]) :: [Symbol]+-- = '["a", "b"]+data ToSymbolList :: Text -> Exp [Symbol]+type instance Eval (ToSymbolList ('Text sym)) =+ Eval (F.FMap S.CharToSymbol =<< S.ToCharList sym)+++++-- | Split text to characters and give them as Char list.+--+-- > :kind! Eval (ToCharList =<< FromSymbol "abc")+-- Eval (ToCharList =<< FromSymbol "abc") :: [Char]+-- = '['a', 'b', 'c']+data ToCharList :: Text -> Exp [Char]+type instance Eval (ToCharList ('Text sym)) = S.ToCharList @@ sym+++-- | Split text to characters and give them as Text list.+--+-- > :kind! Eval (ToList =<< FromSymbol "abc")+-- Eval (ToList =<< FromSymbol "abc") :: [Text]+-- = '[ 'Text "a", 'Text "b", 'Text "c"]+data ToList :: Text -> Exp [Text]+type instance Eval (ToList txt) =+ Eval (F.FMap Singleton =<< ToCharList txt)+++-- | Unpack+--+-- === __Example__+--+-- >>> :kind! Eval (Unpack =<< FromSymbol "word")+-- Eval (Unpack =<< FromSymbol "word") :: Symbol+-- = "word"+data Unpack :: Text -> Exp Symbol+type instance Eval (Unpack ('Text sym)) = sym++++-- | Null+--+-- === __Example__+--+-- >>> :kind! Eval (Null ('Text "ab"))+-- Eval (Null ('Text "ab")) :: Bool+-- = 'False+--+-- >>> :kind! Eval (Null =<< Empty)+-- Eval (Null =<< Empty) :: Bool+-- = 'True+data Null :: Text -> Exp Bool+type instance Eval (Null txt) = Eval+ (If (Eval (IsNothing =<< NullHelper txt))+ (Pure 'True)+ (Pure 'False)+ )++-- > :kind! Eval (NullHelper =<< (Singleton "koe"))+-- Eval (NullHelper =<< (Singleton "koe")) :: Maybe+-- (Char, Text)+-- = 'Just '('k', 'Text "oe")+data NullHelper :: Text -> Exp (Maybe (Char, Text))+type instance Eval (NullHelper ('Text symbol)) =+ Eval (F.FMap (Second FromSymbol) =<< S.UnconsSymbol symbol)+++-- | Length+--+-- === __Example__+--+-- >>> :kind! Eval (Length =<< FromSymbol "ab")+-- Eval (Length =<< FromSymbol "ab") :: TL.Natural+-- = 2+data Length :: Text -> Exp Nat+type instance Eval (Length txt) = Eval (F.Length =<< ToCharList txt)+++-- | Add a Char to the beginning of a type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Cons 'h' ('Text "aamu"))+-- Eval (Cons 'h' ('Text "aamu")) :: Text+-- = 'Text "haamu"+data Cons :: Char -> Text -> Exp Text+type instance Eval (Cons c ('Text sym)) =+ 'Text (TL.AppendSymbol (Eval (S.CharToSymbol c)) sym)+++-- | Add a Symbol to the beginning of a type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (ConsSymbol "h" ('Text "aamu"))+-- Eval (ConsSymbol "h" ('Text "aamu")) :: Text+-- = 'Text "haamu"+data ConsSymbol :: Symbol -> Text -> Exp Text+type instance Eval (ConsSymbol s ('Text sym)) = 'Text (TL.AppendSymbol s sym)+++-- | Add a Char to the end of a type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Snoc ('Text "aam") 'u')+-- Eval (Snoc ('Text "aam") 'u') :: Text+-- = 'Text "aamu"+data Snoc :: Text -> Char -> Exp Text+type instance Eval (Snoc ('Text sym) c) =+ 'Text (TL.AppendSymbol sym (Eval (S.CharToSymbol c)))++-- | Add a Symbol to the end of a type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (SnocSymbol ('Text "aam") "u")+-- Eval (SnocSymbol ('Text "aam") "u") :: Text+-- = 'Text "aamu"+data SnocSymbol :: Text -> Symbol -> Exp Text+type instance Eval (SnocSymbol ('Text sym) s) = 'Text (TL.AppendSymbol sym s)+++-- | Append two type-level texts.+--+-- === __Example__+--+-- >>> :kind! Eval (Append ('Text "aa") ('Text "mu"))+-- Eval (Append ('Text "aa") ('Text "mu")) :: Text+-- = 'Text "aamu"+data Append :: Text -> Text -> Exp Text+type instance Eval (Append ('Text s1) ('Text s2)) = 'Text (TL.AppendSymbol s1 s2)+++-- | Get the first Char from type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Uncons ('Text "haamu"))+-- Eval (Uncons ('Text "haamu")) :: Maybe (Char, Text)+-- = 'Just '('h', 'Text "aamu")+--+-- >>> :kind! Eval (Uncons ('Text ""))+-- Eval (Uncons ('Text "")) :: Maybe (Char, Text)+-- = 'Nothing+data Uncons :: Text -> Exp (Maybe (Char, Text))+type instance Eval (Uncons txt) =+ Eval (PairMaybeToMaybePair '( Eval (Head txt), Eval (Tail txt) ))+++-- | Get the last Char from type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Unsnoc ('Text "aamun"))+-- Eval (Unsnoc ('Text "aamun")) :: Maybe (Text, Char)+-- = 'Just '( 'Text "aamu", 'n')+--+-- >>> :kind! Eval (Unsnoc ('Text ""))+-- Eval (Unsnoc ('Text "")) :: Maybe (Text, Char)+-- = 'Nothing+data Unsnoc :: Text -> Exp (Maybe (Text, Char))+type instance Eval (Unsnoc txt) = + Eval (F.FMap Swap =<< F.FMap (Second Reverse) =<< Uncons =<< Reverse txt)+++-- | Get the first Char of type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Head ('Text "aamu"))+-- Eval (Head ('Text "aamu")) :: Maybe Char+-- = 'Just 'a'+--+-- >>> :kind! Eval (Head ('Text ""))+-- Eval (Head ('Text "")) :: Maybe Char+-- = 'Nothing+data Head :: Text -> Exp (Maybe Char)+type instance Eval (Head ('Text sym)) =+ Eval (F.FMap Fst =<< S.UnconsSymbol sym)+++-- | Get the last Char of type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Last ('Text "aamu"))+-- Eval (Last ('Text "aamu")) :: Maybe Char+-- = 'Just 'u'+--+-- >>> :kind! Eval (Last ('Text ""))+-- Eval (Last ('Text "")) :: Maybe Char+-- = 'Nothing+data Last :: Text -> Exp (Maybe Char)+type instance Eval (Last txt) = Eval (F.FMap Snd =<< Unsnoc txt)+++-- | Get the tail of a type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Tail ('Text "haamu"))+-- Eval (Tail ('Text "haamu")) :: Maybe Text+-- = 'Just ('Text "aamu")+--+-- >>> :kind! Eval (Tail ('Text ""))+-- Eval (Tail ('Text "")) :: Maybe Text+-- = 'Nothing+data Tail :: Text -> Exp (Maybe Text)+type instance Eval (Tail ('Text sym)) =+ Eval (F.FMap FromSymbol =<< F.FMap Snd =<< S.UnconsSymbol sym)+++-- | Take all except the last Char from type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Init ('Text "aamun"))+-- Eval (Init ('Text "aamun")) :: Maybe Text+-- = 'Just ('Text "aamu")+--+-- >>> :kind! Eval (Init ('Text ""))+-- Eval (Init ('Text "")) :: Maybe Text+-- = 'Nothing+data Init :: Text -> Exp (Maybe Text)+type instance Eval (Init ('Text sym)) = Eval+ (F.FMap FromSymbol =<< F.FMap S.ConcatChars =<< F.Init =<< S.ToCharList sym)+++-- | Compare the length of type-level text to given Nat and give+-- the Ordering.+--+-- === __Example__+--+-- >>> :kind! Eval (CompareLength ('Text "aamu") 3)+-- Eval (CompareLength ('Text "aamu") 3) :: Ordering+-- = 'GT+data CompareLength :: Text -> Nat -> Exp Ordering+type instance Eval (CompareLength txt n) = TL.CmpNat (Length @@ txt) n++++-- | FMapSymbol for type-level text.+--+-- === __Example__+--+-- >>> :{+-- data IsIsymb :: Symbol -> Exp Bool+-- type instance Eval (IsIsymb s) = Eval ("i" Sym.== s)+-- data Isymb2e :: Symbol -> Exp Symbol+-- type instance Eval (Isymb2e s) = Eval+-- (If (IsIsymb @@ s)+-- (Pure "e")+-- (Pure s)+-- )+-- :}+--+-- >>> :kind! Eval (FMapSymbol Isymb2e ('Text "imu"))+-- Eval (FMapSymbol Isymb2e ('Text "imu")) :: Text+-- = 'Text "emu"+data FMapSymbol :: (Symbol -> Exp Symbol) -> Text -> Exp Text+type instance Eval (FMapSymbol f txt) =+ Eval (FromSymbol =<< S.Concat =<< F.FMap f =<< F.FMap Unpack =<< ToList txt)+++-- | FMap for type-level text.+--+-- === __Example__+--+-- >>> :{+-- data DigitsToX :: Char -> Exp Char+-- type instance Eval (DigitsToX c) = Eval+-- (If (IsDigit @@ c)+-- (Pure 'X')+-- (Pure c)+-- )+-- :}+--+-- >>> :kind! Eval (FMap DigitsToX ('Text "Some4text5oh9."))+-- Eval (FMap DigitsToX ('Text "Some4text5oh9.")) :: Text+-- = 'Text "SomeXtextXohX."+data FMap :: (Char -> Exp Char) -> Text -> Exp Text+type instance Eval (FMap f ('Text sym)) =+ Eval (FromSymbol =<< S.ConcatChars =<< F.FMap f =<< S.ToCharList sym)+++data FMapT :: (Text -> Exp Text) -> Text -> Exp Text+type instance Eval (FMapT f txt) = Eval+ (FromList =<< F.FMap f =<< ToList txt)+-- is this too much+++-- | Intercalate for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Intercalate ('Text " & ") ('[ 'Text "aamu", 'Text "valo"]))+-- Eval (Intercalate ('Text " & ") ('[ 'Text "aamu", 'Text "valo"])) :: Text+-- = 'Text "aamu & valo"+data Intercalate :: Text -> [Text] -> Exp Text+type instance Eval (Intercalate txt txts) = + Eval (FromList =<< F.Intercalate '[txt] =<< F.FMap ToList txts)+++-- | Intersperse Char for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Intersperse '.' ('Text "aamu"))+-- Eval (Intersperse '.' ('Text "aamu")) :: Text+-- = 'Text "a.a.m.u"+data Intersperse :: Char -> Text -> Exp Text+type instance Eval (Intersperse c ('Text sym)) = Eval+ (FromSymbolList =<< F.Intersperse (S.CharToSymbol @@c) =<< F.FMap S.CharToSymbol =<< S.ToCharList sym)++-- | Intersperse Symbol for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (IntersperseSymbol "." ('Text "aamu"))+-- Eval (IntersperseSymbol "." ('Text "aamu")) :: Text+-- = 'Text "a.a.m.u"+data IntersperseSymbol :: Symbol -> Text -> Exp Text+type instance Eval (IntersperseSymbol s ('Text sym)) = Eval+ (FromSymbolList =<< F.Intersperse s =<< F.FMap S.CharToSymbol =<< S.ToCharList sym)+++-- | Reverse for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Reverse ('Text "aamu"))+-- Eval (Reverse ('Text "aamu")) :: Text+-- = 'Text "umaa"+--+-- >>> :kind! Eval (Reverse =<< Reverse ('Text "aamu"))+-- Eval (Reverse =<< Reverse ('Text "aamu")) :: Text+-- = 'Text "aamu"+data Reverse :: Text -> Exp Text+type instance Eval (Reverse ('Text sym)) =+ Eval (FromSymbol =<< S.ConcatChars =<< F.Reverse =<< S.ToCharList sym)++ +-- | Replace for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Replace ('Text "tu") ('Text "la") ('Text "tuututtaa"))+-- Eval (Replace ('Text "tu") ('Text "la") ('Text "tuututtaa")) :: Text+-- = 'Text "laulattaa"+data Replace :: Text -> Text -> Text -> Exp Text+type instance Eval (Replace orig new txt) =+ Eval (Intercalate new =<< SplitOn orig txt)+++-- | Concat for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Concat '[ 'Text "la", 'Text "kana"])+-- Eval (Concat '[ 'Text "la", 'Text "kana"]) :: Text+-- = 'Text "lakana"+data Concat :: [Text] -> Exp Text+type instance Eval (Concat lst) = Eval (FromSymbol =<< S.Concat =<< F.FMap Unpack lst)+++-- | FConcatMapSymbol for type-level text. This takes Symbol to Text function.+--+-- === __Example__+--+-- >>> :{+-- data IsIsymb :: Symbol -> Exp Bool+-- type instance Eval (IsIsymb s) = Eval ("i" Sym.== s)+-- data Isymb2aa :: Symbol -> Exp Text+-- type instance Eval (Isymb2aa s) = Eval+-- (If (IsIsymb @@ s)+-- (Pure ('Text "aa"))+-- (Pure ('Text s))+-- )+-- :}+--+-- >>> :kind! Eval (ConcatMapSymbol Isymb2aa ('Text "imu ih"))+-- Eval (ConcatMapSymbol Isymb2aa ('Text "imu ih")) :: Text+-- = 'Text "aamu aah"+data ConcatMapSymbol :: (Symbol -> Exp Text) -> Text -> Exp Text+type instance Eval (ConcatMapSymbol f ('Text sym)) =+ Eval (Concat =<< F.FMap f =<< F.FMap S.CharToSymbol =<< S.ToCharList sym)+++-- | ConcatMap for type-level text. This takes Char to Text function.+--+-- === __Example__+--+-- >>> :{+-- data DigitsToHoo :: Char -> Exp Text+-- type instance Eval (DigitsToHoo c) = Eval+-- (If (IsDigit @@ c)+-- (Pure ( 'Text "hoo"))+-- (Singleton c)+-- )+-- :}+--+-- >>> :kind! Eval (ConcatMap DigitsToHoo ('Text "haa2hui2"))+-- Eval (ConcatMap DigitsToHoo ('Text "haa2hui2")) :: Text+-- = 'Text "haahoohuihoo"+data ConcatMap :: (Char -> Exp Text) -> Text -> Exp Text+type instance Eval (ConcatMap f ('Text sym)) =+ Eval (Concat =<< F.FMap f =<< S.ToCharList sym)++-- | ConcatMap for type-level text. This takes Char to Symbol function.+data ConcatMapCS :: (Char -> Exp Symbol) -> Text -> Exp Text+type instance Eval (ConcatMapCS f ('Text sym)) =+ Eval (FromSymbol =<< S.Concat =<< F.FMap f =<< S.ToCharList sym)+++-- | Any for type-level text. This takes Char to Bool function.+--+-- === __Example__+--+-- >>> :kind! Eval (Any IsDigit ('Text "aamu1"))+-- Eval (Any IsDigit ('Text "aamu1")) :: Bool+-- = 'True+--+-- >>> :kind! Eval (Any IsDigit ('Text "aamu"))+-- Eval (Any IsDigit ('Text "aamu")) :: Bool+-- = 'False+data Any :: (Char -> Exp Bool) -> Text -> Exp Bool+type instance Eval (Any f ('Text sym)) = Eval (F.Any f =<< S.ToCharList sym)+++-- | AnySymbol for type-level text. This takes Symbol to Bool function.+-- Note that the given function needs to be compatible... (i.e. operating+-- with symbols of length 1.+--+-- === __Example__+--+-- >>> :kind! Eval (AnySymbol Sym.IsDigit ('Text "aamu1"))+-- Eval (AnySymbol Sym.IsDigit ('Text "aamu1")) :: Bool+-- = 'True+--+-- >>> :kind! Eval (AnySymbol Sym.IsDigit ('Text "aamu"))+-- Eval (AnySymbol Sym.IsDigit ('Text "aamu")) :: Bool+-- = 'False+data AnySymbol :: (Symbol -> Exp Bool) -> Text -> Exp Bool+type instance Eval (AnySymbol f ('Text sym)) =+ Eval (F.Any f =<< F.FMap S.CharToSymbol =<< S.ToCharList sym)+++-- | All for type-level text. This takes Char to Bool function.+--+-- === __Example__+--+-- >>> :kind! Eval (All IsDigit ('Text "aamu1"))+-- Eval (All IsDigit ('Text "aamu1")) :: Bool+-- = 'False+--+-- >>> :kind! Eval (All IsDigit ('Text "321"))+-- Eval (All IsDigit ('Text "321")) :: Bool+-- = 'True+data All :: (Char -> Exp Bool) -> Text -> Exp Bool+type instance Eval (All f ('Text sym)) = Eval (F.All f =<< S.ToCharList sym)+++-- | AllSymbol for type-level text. This takes Symbol to Bool function.+--+-- === __Example__+--+-- >>> :kind! Eval (AllSymbol Sym.IsDigit ('Text "aamu1"))+-- Eval (AllSymbol Sym.IsDigit ('Text "aamu1")) :: Bool+-- = 'False+--+-- >>> :kind! Eval (AllSymbol Sym.IsDigit ('Text "321"))+-- Eval (AllSymbol Sym.IsDigit ('Text "321")) :: Bool+-- = 'True+data AllSymbol :: (Symbol -> Exp Bool) -> Text -> Exp Bool+type instance Eval (AllSymbol f ('Text sym)) =+ Eval (F.All f =<< F.FMap S.CharToSymbol =<< S.ToCharList sym)+++-- | Take for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Take 4 ('Text "aamun"))+-- Eval (Take 4 ('Text "aamun")) :: Text+-- = 'Text "aamu"+data Take :: Nat -> Text -> Exp Text+type instance Eval (Take n txt) = Eval (FromList =<< F.Take n =<< ToList txt)++-- | TakeEnd for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (TakeEnd 4 ('Text "haamu"))+-- Eval (TakeEnd 4 ('Text "haamu")) :: Text+-- = 'Text "aamu"+data TakeEnd :: Nat -> Text -> Exp Text+type instance Eval (TakeEnd n txt) =+ Eval (FromList =<< F.Reverse =<< F.Take n =<< F.Reverse =<< ToList txt)+++-- | Drop for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Drop 2 ('Text "aamuna"))+-- Eval (Drop 2 ('Text "aamuna")) :: Text+-- = 'Text "muna"+data Drop :: Nat -> Text -> Exp Text+type instance Eval (Drop n txt) = Eval (FromList =<< F.Drop n =<< ToList txt)+++-- | DropEnd for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (DropEnd 2 ('Text "aamuna"))+-- Eval (DropEnd 2 ('Text "aamuna")) :: Text+-- = 'Text "aamu"+data DropEnd :: Nat -> Text -> Exp Text+type instance Eval (DropEnd n txt) =+ Eval (FromList =<< F.Reverse =<< F.Drop n =<< F.Reverse =<< ToList txt)++-- | TakeWhile for type-level text. This takes Char to Bool function.+--+-- === __Example__+--+-- >>> :kind! Eval (TakeWhile (Not <=< IsDigit) ('Text "aamu12"))+-- Eval (TakeWhile (Not <=< IsDigit) ('Text "aamu12")) :: Text+-- = 'Text "aamu"+data TakeWhile :: (Char -> Exp Bool) -> Text -> Exp Text+type instance Eval (TakeWhile f ('Text sym)) =+ Eval (FromSymbol =<< S.ConcatChars =<< F.TakeWhile f =<< S.ToCharList sym)+++-- | TakeWhileSymbol for type-level text. This takes Symbol to Bool function.+--+-- === __Example__+--+-- >>> :kind! Eval (TakeWhileSymbol (Not <=< Sym.IsDigit) ('Text "aamu12"))+-- Eval (TakeWhileSymbol (Not <=< Sym.IsDigit) ('Text "aamu12")) :: Text+-- = 'Text "aamu"+data TakeWhileSymbol :: (Symbol -> Exp Bool) -> Text -> Exp Text+type instance Eval (TakeWhileSymbol f txt) = Eval+ (FromSymbolList =<< F.TakeWhile f =<< ToSymbolList txt)+++-- | TakeWhileEnd for type-level text. This takes Char to Bool function.+--+-- === __Example__+--+-- >>> :kind! Eval (TakeWhileEnd (Not <=< IsDigit) ('Text "12aamu"))+-- Eval (TakeWhileEnd (Not <=< IsDigit) ('Text "12aamu")) :: Text+-- = 'Text "aamu"+data TakeWhileEnd :: (Char -> Exp Bool) -> Text -> Exp Text+type instance Eval (TakeWhileEnd f ('Text sym)) = Eval+ (FromSymbol+ =<< S.ConcatChars =<< F.Reverse =<< F.TakeWhile f =<< F.Reverse+ =<< S.ToCharList sym)+++-- | TakeWhileEndSymbol for type-level text. This takes Symbol to Bool function.+--+-- === __Example__+--+-- >>> :kind! Eval (TakeWhileEndSymbol (Not <=< Sym.IsDigit) ('Text "12aamu"))+-- Eval (TakeWhileEndSymbol (Not <=< Sym.IsDigit) ('Text "12aamu")) :: Text+-- = 'Text "aamu"+data TakeWhileEndSymbol :: (Symbol -> Exp Bool) -> Text -> Exp Text+type instance Eval (TakeWhileEndSymbol f txt) = Eval+ (FromSymbolList =<< F.Reverse =<< F.TakeWhile f =<< F.Reverse =<< ToSymbolList txt)+++-- | DropWhile for type-level text. This takes Char to Bool function.+--+-- === __Example__+--+-- >>> :kind! Eval (DropWhile IsDigit ('Text "12aamu"))+-- Eval (DropWhile IsDigit ('Text "12aamu")) :: Text+-- = 'Text "aamu"+data DropWhile :: (Char -> Exp Bool) -> Text -> Exp Text+type instance Eval (DropWhile f ('Text sym)) = Eval+ (FromSymbol =<< S.ConcatChars =<< F.DropWhile f =<< S.ToCharList sym)+++-- | DropWhileSymbol for type-level text. This takes Symbol to Bool function.+--+-- === __Example__+--+-- >>> :kind! Eval (DropWhileSymbol Sym.IsDigit ('Text "12aamu"))+-- Eval (DropWhileSymbol Sym.IsDigit ('Text "12aamu")) :: Text+-- = 'Text "aamu"+data DropWhileSymbol :: (Symbol -> Exp Bool) -> Text -> Exp Text+type instance Eval (DropWhileSymbol f txt) = Eval+ (FromSymbolList =<< F.DropWhile f =<< ToSymbolList txt)+++-- | DropWhileEnd for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (DropWhileEnd IsDigit ('Text "aamu12"))+-- Eval (DropWhileEnd IsDigit ('Text "aamu12")) :: Text+-- = 'Text "aamu"+data DropWhileEnd :: (Char -> Exp Bool) -> Text -> Exp Text+type instance Eval (DropWhileEnd f ('Text sym)) = Eval+ (FromSymbol =<< S.ConcatChars =<< F.Reverse =<< F.DropWhile f+ =<< F.Reverse =<< S.ToCharList sym)+++-- | DropWhileEndSymbol for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (DropWhileEndSymbol Sym.IsDigit ('Text "aamu12"))+-- Eval (DropWhileEndSymbol Sym.IsDigit ('Text "aamu12")) :: Text+-- = 'Text "aamu"+data DropWhileEndSymbol :: (Symbol -> Exp Bool) -> Text -> Exp Text+type instance Eval (DropWhileEndSymbol f txt) = Eval+ (FromSymbolList =<< F.Reverse =<< F.DropWhile f =<< F.Reverse =<< ToSymbolList txt)+++-- | DropAround for type-level text. This takes Char to Bool function.+--+-- === __Example__+--+-- >>> :kind! Eval (DropAround IsDigit ('Text "34aamu12"))+-- Eval (DropAround IsDigit ('Text "34aamu12")) :: Text+-- = 'Text "aamu"+data DropAround :: (Char -> Exp Bool) -> Text -> Exp Text+type instance Eval (DropAround f txt) = Eval (DropWhile f =<< DropWhileEnd f txt)+++-- | DropAroundSymbol for type-level text. This takes Symbol to Bool function.+--+-- === __Example__+--+-- >>> :kind! Eval (DropAroundSymbol Sym.IsDigit ('Text "34aamu12"))+-- Eval (DropAroundSymbol Sym.IsDigit ('Text "34aamu12")) :: Text+-- = 'Text "aamu"+data DropAroundSymbol :: (Symbol -> Exp Bool) -> Text -> Exp Text+type instance Eval (DropAroundSymbol f txt) =+ Eval (DropWhileSymbol f =<< DropWhileEndSymbol f txt)+++-- | Strip the space, newline and tab -symbols from the beginning and and+-- of type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Strip ('Text " aamu \n"))+-- Eval (Strip ('Text " aamu \n")) :: Text+-- = 'Text "aamu"+data Strip :: Text -> Exp Text+type instance Eval (Strip txt) = Eval (DropAroundSymbol Sym.IsSpaceDelim txt)+++-- | SplitOn for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (SplitOn ('Text "ab") ('Text "cdabfgabh"))+-- Eval (SplitOn ('Text "ab") ('Text "cdabfgabh")) :: [Text]+-- = '[ 'Text "cd", 'Text "fg", 'Text "h"]+data SplitOn :: Text -> Text -> Exp [Text]+type instance Eval (SplitOn ('Text sep) ('Text txt)) = Eval+ -- (F.FMap FromSymbolList+ (F.FMap FromSymbol =<< F.FMap S.ConcatChars+ =<< SOLoop (Eval (S.ToCharList sep)) '( '[], Eval (S.ToCharList txt)))+++-- | Helper for SplitOn+--+-- >>> :kind! Eval (SOTake '[ 'a', 'b'] '[ 'c', 'd', 'a', 'b', 'f', 'g'] '[])+-- Eval (SOTake '[ 'a', 'b'] '[ 'c', 'd', 'a', 'b', 'f', 'g'] '[]) :: ([Char],+-- [Char])+-- = '( '['c', 'd'], '['f', 'g'])+data SOTake :: [Char] -> [Char] -> [Char] -> Exp ([Char], [Char])+type instance Eval (SOTake sep '[] accum) = '(accum, '[])+type instance Eval (SOTake sep (t ': txt) accum) = Eval+ (If (Eval (F.IsPrefixOf sep (t ': txt)))+ (Pure '(accum, Eval (F.Drop (Eval (F.Length sep)) (t ': txt))))+ (SOTake sep txt (Eval (accum ++ '[t])))+ )++-- | Helper for SplitOn+data SOLoop :: [Char] -> ([[Char]],[Char]) -> Exp [[Char]]+type instance Eval (SOLoop sep '(acc, '[])) = acc+type instance Eval (SOLoop sep '(acc, (t ': txt))) =+ Eval (SOLoop sep =<< First (F.Snoc acc) =<< SOTake sep (t ': txt) '[])+++-- | Split for type-level text. This takes Char to Bool function.+--+-- === __Example__+--+-- >>> :kind! Eval (Split C.IsSpace (Eval (FromSymbol "cd bf abh")))+-- Eval (Split C.IsSpace (Eval (FromSymbol "cd bf abh"))) :: [Text]+-- = '[ 'Text "cd", 'Text "bf", 'Text "abh"]+data Split :: (Char -> Exp Bool) -> Text -> Exp [Text]+type instance Eval (Split p ('Text sym)) = Eval+ (F.FMap FromSymbol =<< F.FMap S.ConcatChars+ =<< SplitLoop p '( '[], Eval (S.ToCharList sym)))+++-- | SplitSymbol for type-level text. This takes Symbol to Bool function.+--+-- === __Example__+--+-- >>> :kind! Eval (SplitSymbol Sym.IsSpace (Eval (FromSymbol "cd bf abh")))+-- Eval (SplitSymbol Sym.IsSpace (Eval (FromSymbol "cd bf abh"))) :: [Text]+-- = '[ 'Text "cd", 'Text "bf", 'Text "abh"]+data SplitSymbol :: (Symbol -> Exp Bool) -> Text -> Exp [Text]+type instance Eval (SplitSymbol p txt) =+ Eval (F.FMap FromSymbolList =<< SplitLoop p '( '[], Eval (ToSymbolList txt)))++-- | Helper for Split+data SplitTake :: (a -> Exp Bool) -> [a] -> [a] -> Exp ([a], [a])+type instance Eval (SplitTake p '[] accum) = '(accum, '[])+type instance Eval (SplitTake p (t ': txt) accum) = Eval+ (If (Eval (p t))+ (Pure '(accum, txt))+ (SplitTake p txt (Eval (accum ++ '[t])))+ )++-- | Helper for Split+data SplitLoop :: (a -> Exp Bool) -> ([[a]],[a]) -> Exp [[a]]+type instance Eval (SplitLoop p '(acc, '[])) = acc+type instance Eval (SplitLoop p '(acc, (t ': txt))) = + Eval (SplitLoop p =<< First (F.Snoc acc) =<< SplitTake p (t ': txt) '[])+++-- | Lines for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Lines =<< FromSymbol "ok\nhmm\nab")+-- Eval (Lines =<< FromSymbol "ok\nhmm\nab") :: [Text]+-- = '[ 'Text "ok", 'Text "hmm", 'Text "ab"]+data Lines :: Text -> Exp [Text]+type instance Eval (Lines txt) = Eval (SplitSymbol Sym.IsNewLine txt)+++-- | Words for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Words =<< FromSymbol "ok hmm\nab")+-- Eval (Words =<< FromSymbol "ok hmm\nab") :: [Text]+-- = '[ 'Text "ok", 'Text "hmm", 'Text "ab"]+data Words :: Text -> Exp [Text]+type instance Eval (Words txt) = Eval (SplitSymbol Sym.IsSpaceDelim txt)++-- | Unlines for type-level text. This adds a newline to each Text and then+-- concats them.+--+-- === __Example__+--+-- >>> :kind! Eval (Unlines '[ 'Text "ok", 'Text "hmm", 'Text "ab"])+-- Eval (Unlines '[ 'Text "ok", 'Text "hmm", 'Text "ab"]) :: Text+-- = 'Text "ok\nhmm\nab\n"+data Unlines :: [Text] -> Exp Text+type instance Eval (Unlines txts) = + Eval (Concat =<< F.FMap (Flip Append (FromSymbol @@ "\n")) txts)++-- | Unwords for type-level text. This uses 'Intercalate' to add space-symbol+-- between the given texts.+--+-- === __Example__+--+-- >>> :kind! Eval (Unwords '[ 'Text "ok", 'Text "hmm", 'Text "ab"])+-- Eval (Unwords '[ 'Text "ok", 'Text "hmm", 'Text "ab"]) :: Text+-- = 'Text "ok hmm ab"+data Unwords :: [Text] -> Exp Text+type instance Eval (Unwords txts) = Eval (Intercalate ('Text " ") txts)+++-- | IsPrefixOf for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (IsPrefixOf ('Text "aa") ('Text "aamiainen"))+-- Eval (IsPrefixOf ('Text "aa") ('Text "aamiainen")) :: Bool+-- = 'True+data IsPrefixOf :: Text -> Text -> Exp Bool+type instance Eval (IsPrefixOf l1 l2) =+ Eval (F.IsPrefixOf (Eval (ToList l1)) (Eval (ToList l2)))+++-- | IsSuffixOf for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (IsSuffixOf ('Text "nen") ('Text "aamiainen"))+-- Eval (IsSuffixOf ('Text "nen") ('Text "aamiainen")) :: Bool+-- = 'True+data IsSuffixOf :: Text -> Text -> Exp Bool+type instance Eval (IsSuffixOf l1 l2) =+ Eval (F.IsSuffixOf (Eval (ToList l1)) (Eval (ToList l2)))+++-- | IsInfixOf for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (IsInfixOf ('Text "mia") ('Text "aamiainen"))+-- Eval (IsInfixOf ('Text "mia") ('Text "aamiainen")) :: Bool+-- = 'True+data IsInfixOf :: Text -> Text -> Exp Bool+type instance Eval (IsInfixOf l1 l2) =+ Eval (F.IsInfixOf (Eval (ToList l1)) (Eval (ToList l2)))+++--------------------------------------------------------------------------------++#else++--------------------------------------------------------------------------------++#endif++--------------------------------------------------------------------------------
+ src/Fcf/Data/OldText.hs view
@@ -0,0 +1,753 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wall #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{-|+Module : Fcf.Data.OldText+Description : Type-level Text data structure with methods+Copyright : (c) gspia 2020-+License : BSD+Maintainer : gspia++= Fcf.Data.OldText++We mimick Data.Text but on type level. The internal representation is based on+type level lists. This module is for GHC version 9.0.x or less. The current+(as of early 2023) implementation of Fcf.Data.Text will be deprecated and replaced+with the contents of Fcf.Data.NewText later 2023 as newer version GHC become more+widespread.++-}++--------------------------------------------------------------------------------++module Fcf.Data.OldText+ {-# DEPRECATED "Use Fcf.Data.NewText instead" #-}+ ( Text (..)++ -- * Creation+ , Empty+ , Singleton+ , FromList+ , FromSymbolList+ , ToList+ , ToSymbol+ , ToSymbolList++ -- * Basic Interface+ , Null+ , Length+ , Append+ , Cons+ , Snoc+ , Uncons+ , Unsnoc+ , Head+ , Tail+ , Init+ , CompareLength++ -- * Transformation+ , FMap+ , Intercalate+ , Intersperse+ , Reverse+ , Replace++ -- * Special Folds+ , Concat+ , FConcatMap+ , Any+ , All++ -- * Substrings+ , Take+ , TakeEnd+ , Drop+ , DropEnd+ , TakeWhile+ , TakeWhileEnd+ , DropWhile+ , DropWhileEnd+ , DropAround+ , Strip++ -- * Breaking etc+ , SplitOn+ , Split+ , Lines+ , Words+ , Unlines+ , Unwords++ -- * Predicates+ , IsPrefixOf+ , IsSuffixOf+ , IsInfixOf+ )+ where++import GHC.TypeLits (Symbol)+import qualified GHC.TypeLits as TL++import Fcf ( If, Eval, Exp, type (=<<), type (@@)+ , Flip, Pure)+import qualified Fcf.Class.Foldable as F (All, Any)+import Fcf.Data.List ( type (++) )+import qualified Fcf.Data.List as F+ ( Length, Init, Reverse, Take, Drop, TakeWhile, DropWhile+ , Intercalate, Intersperse, IsPrefixOf, IsSuffixOf, IsInfixOf, Snoc)++import qualified Fcf.Class.Functor as F ( FMap )+++import Fcf.Data.Nat (Nat)+import qualified Fcf.Data.Text.Internal as T+import Fcf.Alg.Other ( PairMaybeToMaybePair )+import Fcf.Alg.Morphism (First,Second)+import qualified Fcf.Alg.Symbol as S+import Fcf.Alg.Nat (type (==))++--------------------------------------------------------------------------------+++-- For the doctests:++-- $setup+-- >>> import Fcf (type (<=<), Not)++--------------------------------------------------------------------------------++-- | 'Text' is a data structure, that is, a list to hold type-level symbols of+-- length one.+newtype Text = Text Symbol++--------------------------------------------------------------------------------++-- | Empty+--+-- === __Example__+--+-- >>> :kind! (Eval Empty :: Text)+-- (Eval Empty :: Text) :: Text+-- = 'Text ""+--+-- See also the other examples in this module.+data Empty :: Exp Text+type instance Eval Empty = 'Text ""++-- | Singleton+--+-- === __Example__+--+-- >>> :kind! Eval (Singleton "a")+-- Eval (Singleton "a") :: Text+-- = 'Text "a"+data Singleton :: Symbol -> Exp Text+type instance Eval (Singleton s) = 'Text s++++-- | Use FromList to construct a Text from type-level list.+--+-- === __Example__+--+-- :kind! Eval (FromSymbolList '["h", "e", "l", "l", "u", "r", "e", "i"])+-- Eval (FromSymbolList '["h", "e", "l", "l", "u", "r", "e", "i"]) :: Text+-- = 'Text "hellurei"+data FromSymbolList :: [Symbol] -> Exp Text+type instance Eval (FromSymbolList sym) = 'Text (T.ToSymbol2 @@ sym)+++-- hmm, this is also a Monoid, so we should be able to use Concat+data FromList :: [Text] -> Exp Text+type instance Eval (FromList txt) =+ 'Text (T.ToSymbol2 @@ Eval (F.FMap ToSymbol txt))++-- | Get the type-level list out of the 'Text'.+--+-- === __Example__+--+-- >>> :kind! Eval (ToSymbolList =<< FromSymbolList '["a", "b"])+-- Eval (ToSymbolList =<< FromSymbolList '["a", "b"]) :: [Symbol]+-- = '["a", "b"]+data ToSymbolList :: Text -> Exp [Symbol]+type instance Eval (ToSymbolList ('Text sym)) = T.ToListA @@ sym+++-- | Split 'Text' to single character 'Text' list.+--+-- === __Example__+--+-- >>> :kind! Eval (ToList =<< FromSymbolList '["a", "b"])+-- Eval (ToList =<< FromSymbolList '["a", "b"]) :: [Text]+-- = '[ 'Text "a", 'Text "b"]+data ToList :: Text -> Exp [Text]+type instance Eval (ToList txt) = Eval (F.FMap Singleton =<< ToSymbolList txt)+++-- | ToSymbol+--+-- === __Example__+--+-- >>> :kind! Eval (ToSymbol =<< FromSymbolList '["w", "o", "r", "d"])+-- Eval (ToSymbol =<< FromSymbolList '["w", "o", "r", "d"]) :: Symbol+-- = "word"+data ToSymbol :: Text -> Exp Symbol+type instance Eval (ToSymbol ('Text sym)) = sym++++-- | Null+--+-- === __Example__+--+-- >>> :kind! Eval (Null ('Text "ab"))+-- Eval (Null ('Text "ab")) :: Bool+-- = 'False+--+-- >>> :kind! Eval (Null =<< Empty)+-- Eval (Null =<< Empty) :: Bool+-- = 'True+data Null :: Text -> Exp Bool+type instance Eval (Null txt) = Eval+ (If (Eval (Eval (Length txt) == 0))+ (Pure 'True)+ (Pure 'False)+ )+++-- | Length+--+-- === __Example__+--+-- >>> :kind! Eval (Length =<< Singleton "ab")+-- Eval (Length =<< Singleton "ab") :: TL.Natural+-- = 2+data Length :: Text -> Exp Nat+type instance Eval (Length ('Text sym)) = Eval (F.Length (T.ToList sym))+++-- | Add a symbol to the beginning of a type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Cons "h" ('Text "aamu"))+-- Eval (Cons "h" ('Text "aamu")) :: Text+-- = 'Text "haamu"+data Cons :: Symbol -> Text -> Exp Text+type instance Eval (Cons s ('Text sym)) = 'Text (TL.AppendSymbol s sym)++-- | Add a symbol to the end of a type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Snoc ('Text "aam") "u")+-- Eval (Snoc ('Text "aam") "u") :: Text+-- = 'Text "aamu"+data Snoc :: Text -> Symbol -> Exp Text+type instance Eval (Snoc ('Text sym) s) = 'Text (TL.AppendSymbol sym s)++-- | Append two type-level texts.+--+-- === __Example__+--+-- >>> :kind! Eval (Append ('Text "aa") ('Text "mu"))+-- Eval (Append ('Text "aa") ('Text "mu")) :: Text+-- = 'Text "aamu"+data Append :: Text -> Text -> Exp Text+type instance Eval (Append ('Text s1) ('Text s2)) = 'Text (TL.AppendSymbol s1 s2)+++-- | Get the first symbol from type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Uncons ('Text "haamu"))+-- Eval (Uncons ('Text "haamu")) :: Maybe (Symbol, Text)+-- = 'Just '("h", 'Text "aamu")+--+-- >>> :kind! Eval (Uncons ('Text ""))+-- Eval (Uncons ('Text "")) :: Maybe (Symbol, Text)+-- = 'Nothing+data Uncons :: Text -> Exp (Maybe (TL.Symbol, Text))+type instance Eval (Uncons txt) =+ Eval (PairMaybeToMaybePair '( Eval (Head txt), Eval (Tail txt) ))+++++-- | Get the last symbol from type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Unsnoc ('Text "aamun"))+-- Eval (Unsnoc ('Text "aamun")) :: Maybe (Symbol, Text)+-- = 'Just '("n", 'Text "aamu")+--+-- >>> :kind! Eval (Unsnoc ('Text ""))+-- Eval (Unsnoc ('Text "")) :: Maybe (Symbol, Text)+-- = 'Nothing+data Unsnoc :: Text -> Exp (Maybe (Symbol, Text))+type instance Eval (Unsnoc txt) = + Eval (F.FMap (Second Reverse) =<< Uncons =<< Reverse txt)+++-- | Get the first symbol of type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Head ('Text "aamu"))+-- Eval (Head ('Text "aamu")) :: Maybe Symbol+-- = 'Just "a"+--+-- >>> :kind! Eval (Head ('Text ""))+-- Eval (Head ('Text "")) :: Maybe Symbol+-- = 'Nothing+data Head :: Text -> Exp (Maybe Symbol)+type instance Eval (Head ('Text sym)) = Eval+ (If (Eval (Eval (Length ('Text sym)) == 0))+ (Pure 'Nothing)+ (Pure ('Just (T.Head1 sym (TL.CmpSymbol sym "\128"))))+ )++-- | Get the tail of a type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Tail ('Text "haamu"))+-- Eval (Tail ('Text "haamu")) :: Maybe Text+-- = 'Just ('Text "aamu")+--+-- >>> :kind! Eval (Tail ('Text ""))+-- Eval (Tail ('Text "")) :: Maybe Text+-- = 'Nothing+data Tail :: Text -> Exp (Maybe Text)+type instance Eval (Tail ('Text sym)) = Eval (F.FMap Singleton =<< T.Uncons sym)++-- | Take all except the last symbol from type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Init ('Text "aamun"))+-- Eval (Init ('Text "aamun")) :: Maybe Text+-- = 'Just ('Text "aamu")+--+-- >>> :kind! Eval (Init ('Text ""))+-- Eval (Init ('Text "")) :: Maybe Text+-- = 'Nothing+data Init :: Text -> Exp (Maybe Text)+type instance Eval (Init txt) = Eval (F.FMap FromList =<< F.Init =<< ToList txt)+++-- | Compare the length of type-level text to given Nat and give+-- the Ordering.+--+-- === __Example__+--+-- >>> :kind! Eval (CompareLength ('Text "aamu") 3)+-- Eval (CompareLength ('Text "aamu") 3) :: Ordering+-- = 'GT+data CompareLength :: Text -> Nat -> Exp Ordering+type instance Eval (CompareLength txt n) = TL.CmpNat (Length @@ txt) n++++-- | FMap for type-level text.+--+-- === __Example__+--+-- >>> :{+-- data IsIsymb :: Symbol -> Exp Bool+-- type instance Eval (IsIsymb s) = Eval ("i" S.== s)+-- data Isymb2e :: Symbol -> Exp Symbol+-- type instance Eval (Isymb2e s) = Eval+-- (If (IsIsymb @@ s)+-- (Pure "e")+-- (Pure s)+-- )+-- :}+--+-- >>> :kind! Eval (FMap Isymb2e ('Text "imu"))+-- Eval (FMap Isymb2e ('Text "imu")) :: Text+-- = 'Text "emu"+data FMap :: (Symbol -> Exp Symbol) -> Text -> Exp Text+type instance Eval (FMap f txt) = Eval (FromSymbolList =<< F.FMap f =<< ToSymbolList txt)++data FMapT :: (Text -> Exp Text) -> Text -> Exp Text+type instance Eval (FMapT f txt) = Eval (FromList =<< F.FMap f =<< ToList txt)+++-- | Intercalate for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Intercalate ('Text " & ") ('[ 'Text "aamu", 'Text "valo"]))+-- Eval (Intercalate ('Text " & ") ('[ 'Text "aamu", 'Text "valo"])) :: Text+-- = 'Text "aamu & valo"+data Intercalate :: Text -> [Text] -> Exp Text+type instance Eval (Intercalate txt txts) = + Eval (FromList =<< F.Intercalate '[txt] =<< F.FMap ToList txts)+++-- | Intersperse for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Intersperse "." ('Text "aamu"))+-- Eval (Intersperse "." ('Text "aamu")) :: Text+-- = 'Text "a.a.m.u"+data Intersperse :: Symbol -> Text -> Exp Text+type instance Eval (Intersperse s ('Text txt)) =+ Eval (FromSymbolList =<< F.Intersperse s (T.ToList txt))++-- | Reverse for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Reverse ('Text "aamu"))+-- Eval (Reverse ('Text "aamu")) :: Text+-- = 'Text "umaa"+--+-- >>> :kind! Eval (Reverse =<< Reverse ('Text "aamu"))+-- Eval (Reverse =<< Reverse ('Text "aamu")) :: Text+-- = 'Text "aamu"+data Reverse :: Text -> Exp Text+type instance Eval (Reverse txt) = Eval (FromList =<< F.Reverse =<< ToList txt)++-- | Replace for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Replace ('Text "tu") ('Text "la") ('Text "tuututtaa"))+-- Eval (Replace ('Text "tu") ('Text "la") ('Text "tuututtaa")) :: Text+-- = 'Text "laulattaa"+data Replace :: Text -> Text -> Text -> Exp Text+type instance Eval (Replace orig new txt) =+ Eval (Intercalate new =<< SplitOn orig txt)+++-- | Concat for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Concat '[ 'Text "la", 'Text "kana"])+-- Eval (Concat '[ 'Text "la", 'Text "kana"]) :: Text+-- = 'Text "lakana"+data Concat :: [Text] -> Exp Text+type instance Eval (Concat lst) = + 'Text (T.ToSymbol2 @@ Eval (F.FMap ToSymbol lst))++++-- | FConcatMap for type-level text.+--+-- === __Example__+--+-- >>> :{+-- data IsIsymb :: Symbol -> Exp Bool+-- type instance Eval (IsIsymb s) = Eval ("i" S.== s)+-- data Isymb2aa :: Symbol -> Exp Text+-- type instance Eval (Isymb2aa s) = Eval+-- (If (IsIsymb @@ s)+-- (Pure ('Text "aa"))+-- (Pure ('Text s))+-- )+-- :}+--+-- >>> :kind! Eval (FConcatMap Isymb2aa ('Text "imu ih"))+-- Eval (FConcatMap Isymb2aa ('Text "imu ih")) :: Text+-- = 'Text "aamu aah"+data FConcatMap :: (Symbol -> Exp Text) -> Text -> Exp Text+type instance Eval (FConcatMap f ('Text lst)) = Eval (Concat =<< F.FMap f (T.ToList lst))++-- | Any for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Any S.IsDigit ('Text "aamu1"))+-- Eval (Any S.IsDigit ('Text "aamu1")) :: Bool+-- = 'True+--+-- >>> :kind! Eval (Any S.IsDigit ('Text "aamu"))+-- Eval (Any S.IsDigit ('Text "aamu")) :: Bool+-- = 'False+data Any :: (Symbol -> Exp Bool) -> Text -> Exp Bool+type instance Eval (Any f ('Text sym)) = Eval (F.Any f (T.ToList sym))+++-- | All for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (All S.IsDigit ('Text "aamu1"))+-- Eval (All S.IsDigit ('Text "aamu1")) :: Bool+-- = 'False+--+-- >>> :kind! Eval (All S.IsDigit ('Text "321"))+-- Eval (All S.IsDigit ('Text "321")) :: Bool+-- = 'True+data All :: (Symbol -> Exp Bool) -> Text -> Exp Bool+type instance Eval (All f ('Text lst)) = Eval (F.All f (T.ToList lst))++++++-- | Take for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Take 4 ('Text "aamun"))+-- Eval (Take 4 ('Text "aamun")) :: Text+-- = 'Text "aamu"+data Take :: Nat -> Text -> Exp Text+type instance Eval (Take n ('Text lst)) = Eval (FromSymbolList =<< F.Take n (T.ToList lst))+++-- | TakeEnd for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (TakeEnd 4 ('Text "haamu"))+-- Eval (TakeEnd 4 ('Text "haamu")) :: Text+-- = 'Text "aamu"+data TakeEnd :: Nat -> Text -> Exp Text+type instance Eval (TakeEnd n ('Text lst)) =+ Eval (FromSymbolList =<< F.Reverse =<< F.Take n =<< F.Reverse (T.ToList lst))+++-- | Drop for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Drop 2 ('Text "aamuna"))+-- Eval (Drop 2 ('Text "aamuna")) :: Text+-- = 'Text "muna"+data Drop :: Nat -> Text -> Exp Text+type instance Eval (Drop n ('Text lst)) = Eval (FromSymbolList =<< F.Drop n (T.ToList lst))++-- | DropEnd for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (DropEnd 2 ('Text "aamuna"))+-- Eval (DropEnd 2 ('Text "aamuna")) :: Text+-- = 'Text "aamu"+data DropEnd :: Nat -> Text -> Exp Text+type instance Eval (DropEnd n ('Text lst)) =+ Eval (FromSymbolList =<< F.Reverse =<< F.Drop n =<< F.Reverse (T.ToList lst))+++-- | TakeWhile for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (TakeWhile (Not <=< S.IsDigit) ('Text "aamu12"))+-- Eval (TakeWhile (Not <=< S.IsDigit) ('Text "aamu12")) :: Text+-- = 'Text "aamu"+data TakeWhile :: (Symbol -> Exp Bool) -> Text -> Exp Text+type instance Eval (TakeWhile f ('Text lst)) = Eval (FromSymbolList =<< F.TakeWhile f (T.ToList lst))+++-- | TakeWhileEnd for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (TakeWhileEnd (Not <=< S.IsDigit) ('Text "12aamu"))+-- Eval (TakeWhileEnd (Not <=< S.IsDigit) ('Text "12aamu")) :: Text+-- = 'Text "aamu"+data TakeWhileEnd :: (Symbol -> Exp Bool) -> Text -> Exp Text+type instance Eval (TakeWhileEnd f ('Text lst)) =+ Eval (FromSymbolList =<< F.Reverse =<< F.TakeWhile f =<< F.Reverse (T.ToList lst))+++-- | DropWhile for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (DropWhile S.IsDigit ('Text "12aamu"))+-- Eval (DropWhile S.IsDigit ('Text "12aamu")) :: Text+-- = 'Text "aamu"+data DropWhile :: (Symbol -> Exp Bool) -> Text -> Exp Text+type instance Eval (DropWhile f ('Text lst)) = Eval (FromSymbolList =<< F.DropWhile f (T.ToList lst))+++-- | DropWhileEnd for type-level text.+-- === __Example__+--+-- >>> :kind! Eval (DropWhileEnd S.IsDigit ('Text "aamu12"))+-- Eval (DropWhileEnd S.IsDigit ('Text "aamu12")) :: Text+-- = 'Text "aamu"+data DropWhileEnd :: (Symbol -> Exp Bool) -> Text -> Exp Text+type instance Eval (DropWhileEnd f ('Text lst)) =+ Eval (FromSymbolList =<< F.Reverse =<< F.DropWhile f =<< F.Reverse (T.ToList lst))+++-- | DropAround for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (DropAround S.IsDigit ('Text "34aamu12"))+-- Eval (DropAround S.IsDigit ('Text "34aamu12")) :: Text+-- = 'Text "aamu"+data DropAround :: (Symbol -> Exp Bool) -> Text -> Exp Text+type instance Eval (DropAround f txt) = Eval (DropWhile f =<< DropWhileEnd f txt)++++-- | Strip the space, newline and tab -symbols from the beginning and and+-- of type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Strip ('Text " aamu \n"))+-- Eval (Strip ('Text " aamu \n")) :: Text+-- = 'Text "aamu"+data Strip :: Text -> Exp Text+type instance Eval (Strip txt) = Eval (DropAround S.IsSpaceDelim txt)+++-- | SplitOn for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (SplitOn ('Text "ab") ('Text "cdabfgabh"))+-- Eval (SplitOn ('Text "ab") ('Text "cdabfgabh")) :: [Text]+-- = '[ 'Text "cd", 'Text "fg", 'Text "h"]+data SplitOn :: Text -> Text -> Exp [Text]+type instance Eval (SplitOn ('Text sep) ('Text txt)) =+ Eval (F.FMap FromSymbolList =<< SOLoop (T.ToList sep) '( '[], T.ToList txt))+++-- | Helper for SplitOn+--+-- >>> :kind! Eval (SOTake '["a", "b"] '[ "c", "d", "a", "b", "f", "g"] '[])+-- Eval (SOTake '["a", "b"] '[ "c", "d", "a", "b", "f", "g"] '[]) :: ([Symbol],+-- [Symbol])+-- = '( '["c", "d"], '["f", "g"])+data SOTake :: [Symbol] -> [Symbol] -> [Symbol] -> Exp ([Symbol], [Symbol])+type instance Eval (SOTake sep '[] accum) = '(accum, '[])+type instance Eval (SOTake sep (t ': txt) accum) = Eval+ (If (Eval (F.IsPrefixOf sep (t ': txt)))+ (Pure '(accum, Eval (F.Drop (Eval (F.Length sep)) (t ': txt))))+ (SOTake sep txt (Eval (accum ++ '[t])))+ )++-- | Helper for SplitOn+data SOLoop :: [Symbol] -> ([[Symbol]],[Symbol]) -> Exp [[Symbol]]+type instance Eval (SOLoop sep '(acc, '[])) = acc+type instance Eval (SOLoop sep '(acc, t ': txt)) =+ Eval (SOLoop sep =<< First (F.Snoc acc) =<< SOTake sep (t ': txt) '[])++++-- | Split for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Split S.IsSpace (Eval (Singleton "cd bf abh")))+-- Eval (Split S.IsSpace (Eval (Singleton "cd bf abh"))) :: [Text]+-- = '[ 'Text "cd", 'Text "bf", 'Text "abh"]+data Split :: (Symbol -> Exp Bool) -> Text -> Exp [Text]+type instance Eval (Split p ('Text txt)) =+ Eval (F.FMap FromSymbolList =<< SplitLoop p '( '[], T.ToList txt))++-- | Helper for Split+data SplitTake :: (Symbol -> Exp Bool) -> [Symbol] -> [Symbol] -> Exp ([Symbol], [Symbol])+type instance Eval (SplitTake p '[] accum) = '(accum, '[])+type instance Eval (SplitTake p (t ': txt) accum) = Eval+ (If (Eval (p t))+ (Pure '(accum, txt))+ (SplitTake p txt (Eval (accum ++ '[t])))+ )++-- | Helper for Split+data SplitLoop :: (Symbol -> Exp Bool) -> ([[Symbol]],[Symbol]) -> Exp [[Symbol]]+type instance Eval (SplitLoop p '(acc, '[])) = acc+type instance Eval (SplitLoop p '(acc, t ': txt)) = + Eval (SplitLoop p =<< First (F.Snoc acc) =<< SplitTake p (t ': txt) '[])++++-- | Lines for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Lines =<< Singleton "ok\nhmm\nab")+-- Eval (Lines =<< Singleton "ok\nhmm\nab") :: [Text]+-- = '[ 'Text "ok", 'Text "hmm", 'Text "ab"]+data Lines :: Text -> Exp [Text]+type instance Eval (Lines txt) = Eval (Split S.IsNewLine txt)++-- | Words for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (Words =<< Singleton "ok hmm\nab")+-- Eval (Words =<< Singleton "ok hmm\nab") :: [Text]+-- = '[ 'Text "ok", 'Text "hmm", 'Text "ab"]+data Words :: Text -> Exp [Text]+type instance Eval (Words txt) = Eval (Split S.IsSpaceDelim txt)++-- | Unlines for type-level text. This adds a newline to each Text and then+-- concats them.+--+-- === __Example__+--+-- >>> :kind! Eval (Unlines '[ 'Text "ok", 'Text "hmm", 'Text "ab"])+-- Eval (Unlines '[ 'Text "ok", 'Text "hmm", 'Text "ab"]) :: Text+-- = 'Text "ok\nhmm\nab\n"+data Unlines :: [Text] -> Exp Text+type instance Eval (Unlines txts) = + Eval (Concat =<< F.FMap (Flip Append (Singleton @@ "\n")) txts)++-- | Unwords for type-level text. This uses 'Intercalate' to add space-symbol+-- between the given texts.+--+-- === __Example__+--+-- >>> :kind! Eval (Unwords '[ 'Text "ok", 'Text "hmm", 'Text "ab"])+-- Eval (Unwords '[ 'Text "ok", 'Text "hmm", 'Text "ab"]) :: Text+-- = 'Text "ok hmm ab"+data Unwords :: [Text] -> Exp Text+type instance Eval (Unwords txts) = Eval (Intercalate ('Text " ") txts)+++-- | IsPrefixOf for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (IsPrefixOf ('Text "aa") ('Text "aamiainen"))+-- Eval (IsPrefixOf ('Text "aa") ('Text "aamiainen")) :: Bool+-- = 'True+data IsPrefixOf :: Text -> Text -> Exp Bool+type instance Eval (IsPrefixOf ('Text l1) ('Text l2) ) =+ Eval (F.IsPrefixOf (T.ToList l1) (T.ToList l2))+++-- | IsSuffixOf for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (IsSuffixOf ('Text "nen") ('Text "aamiainen"))+-- Eval (IsSuffixOf ('Text "nen") ('Text "aamiainen")) :: Bool+-- = 'True+data IsSuffixOf :: Text -> Text -> Exp Bool+type instance Eval (IsSuffixOf ('Text l1) ('Text l2) ) =+ Eval (F.IsSuffixOf (T.ToList l1) (T.ToList l2))+++-- | IsInfixOf for type-level text.+--+-- === __Example__+--+-- >>> :kind! Eval (IsInfixOf ('Text "mia") ('Text "aamiainen"))+-- Eval (IsInfixOf ('Text "mia") ('Text "aamiainen")) :: Bool+-- = 'True+data IsInfixOf :: Text -> Text -> Exp Bool+type instance Eval (IsInfixOf ('Text l1) ('Text l2) ) =+ Eval (F.IsInfixOf (T.ToList l1) (T.ToList l2))
+ src/Fcf/Data/Reflect.hs view
@@ -0,0 +1,228 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# OPTIONS_GHC -Wall #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{-|+Module : Fcf.Data.Reflect+Description : List helpers / utils+Copyright : (c) gspia 2023-+License : BSD+Maintainer : gspia++= Fcf.Data.Reflect++Helpers to get results from type-level computations into the fromType-level.++-}++--------------------------------------------------------------------------------++module Fcf.Data.Reflect where++import qualified GHC.TypeLits as TL+import GHC.TypeLits (Nat, Symbol, KnownNat, KnownSymbol)+import Data.String (fromString, IsString)+import Data.Proxy+import Data.Typeable (Typeable, typeRep)+import Data.Kind (Type)+import qualified Data.Map as DM+import qualified Data.IntMap.Strict as IMS+import qualified Data.Set as S+-- #if __GLASGOW_HASKELL__ >= 902+-- #endif+import qualified Data.Tree as T++import qualified Fcf.Data.MapC as MC+import qualified Fcf.Data.NatMap as NM+import qualified Fcf.Data.Set as FS+#if __GLASGOW_HASKELL__ >= 902+import qualified Fcf.Data.NewText as FTxt+#endif+import qualified Fcf.Data.Tree as FT++--------------------------------------------------------------------------------++-- | Reflect a list of Nats+--+-- Note that you may also use the KnownVal methods given below.+--+-- This method is taken from+-- https://hackage.haskell.org/package/numhask-array-0.10.1/docs/src/NumHask.Array.Shape.html#natVals+--+-- === __Example__+--+-- > :{+-- afun :: forall n. (n ~ '[1,2,3,4]) => [Int]+-- afun = natVals @n Proxy+-- :}+--+-- > afun+-- [1,2,3,4]+class KnownNats (ns :: [Nat]) where+ natVals :: Proxy ns -> [Int]++{-# DEPRECATED KnownNats "Replaced with KnownVal" #-}++instance KnownNats '[] where+ natVals _ = []++instance (TL.KnownNat n, KnownNats ns) => KnownNats (n : ns) where+ natVals _ = fromInteger (TL.natVal (Proxy @n)) : natVals (Proxy @ns)+++--------------------------------------------------------------------------------++class KnownVal val kind where+ fromType :: Proxy kind -> val++instance (KnownNat n, Num a) => KnownVal a (n :: Nat) where+ fromType _ = fromInteger $ TL.natVal (Proxy @n)++instance KnownVal Bool 'True where fromType _ = True+instance KnownVal Bool 'False where fromType _ = False+instance KnownVal () '() where fromType _ = ()++instance (IsString str, KnownSymbol s) => KnownVal str (s :: Symbol) where+ fromType _ = fromString $ TL.symbolVal (Proxy @s)++#if __GLASGOW_HASKELL__ >= 920+instance (TL.KnownChar c) => KnownVal Char c where+ fromType _ = TL.charVal (Proxy @c)+#endif++instance (IsString str, Typeable typ) => KnownVal str (typ :: Type) where+ fromType = fromString . show . typeRep++#if __GLASGOW_HASKELL__ >= 902++-- | Text instance.+--+-- === __Example__+--+-- > import qualified Data.Text as Txt+-- > :{+-- afun :: forall r. (r ~ 'FTxt.Text "hmm") => Txt.Text+-- afun = fromType (Proxy @r)+-- :}+--+-- > afun+-- "hmm"+instance (IsString str, KnownSymbol sym) => KnownVal str ('FTxt.Text sym)+ where+ fromType _ = fromType @str (Proxy @sym) ++#endif++--------------------------------------------------------------------------------++-- List instances++instance KnownVal [a] '[] where+ fromType _ = []++instance (KnownVal val x, KnownVal [val] xs) => KnownVal [val] (x ': xs) where+ fromType _ = fromType (Proxy @x) : fromType (Proxy @xs)++--------------------------------------------------------------------------------++-- Trees+--+instance (KnownVal val k, KnownVal (T.Forest val) trees) => KnownVal (T.Tree val) ('FT.Node k trees)+ where+ fromType _ = T.Node (fromType (Proxy @k)) (fromType (Proxy @trees))++--------------------------------------------------------------------------------++-- NatMaps / IntMaps+--+instance (KnownVal [(Int,val)] pairs) => KnownVal (IMS.IntMap val) ('NM.NatMap pairs)+ where+ fromType _ = IMS.fromList (fromType (Proxy @pairs))++instance (KnownVal [(Int,val)] pairs) => KnownVal (IMS.IntMap val) (pairs :: [(Nat, val')])+ where+ fromType _ = IMS.fromList (fromType (Proxy @pairs))++--------------------------------------------------------------------------------++-- Maps++instance (Ord key, KnownVal [(key,val)] pairs) => KnownVal (DM.Map key val) ('MC.MapC pairs)+ where+ fromType _ = DM.fromList (fromType (Proxy @pairs))++instance (Ord key, KnownVal [(key,val)] pairs) => KnownVal (DM.Map key val) (pairs :: [(key',val')])+ where+ fromType _ = DM.fromList (fromType (Proxy @pairs))++--------------------------------------------------------------------------------++-- Set++instance (Ord val, KnownVal [val] kind) => KnownVal (S.Set val) ('FS.Set kind)+ where+ fromType _ = S.fromList (fromType (Proxy @kind))++instance (Ord val, KnownVal [val] kind) => KnownVal (S.Set val) (kind :: [kind'])+ where+ fromType _ = S.fromList (fromType (Proxy @kind))+ +--------------------------------------------------------------------------------++-- Either++instance (KnownVal a1 a) => KnownVal (Either a1 b1) ('Left a) where+ fromType _ = Left (fromType @a1 (Proxy @a))++instance (KnownVal b1 b) => KnownVal (Either a1 b1) ('Right b) where+ fromType _ = Right (fromType @b1 (Proxy @b))++--------------------------------------------------------------------------------++-- Maybe++instance (KnownVal a1 a) => KnownVal (Maybe a1) ('Just a) where+ fromType _ = Just (fromType @a1 (Proxy @a))++instance KnownVal (Maybe a1) 'Nothing where+ fromType _ = Nothing++--------------------------------------------------------------------------------++-- Tuples++instance (KnownVal a1 a, KnownVal b1 b) => KnownVal (a1,b1) '(a,b) where+ fromType _ = (fromType @a1 (Proxy @a), fromType @b1 (Proxy @b))++instance (KnownVal a1 a, KnownVal b1 b, KnownVal c1 c) => KnownVal (a1,b1,c1) '(a,b,c) where+ fromType _ = (fromType @a1 (Proxy @a), fromType @b1 (Proxy @b), fromType @c1 (Proxy @c))++instance (KnownVal a1 a, KnownVal b1 b, KnownVal c1 c, KnownVal d1 d) => KnownVal (a1,b1,c1,d1) '(a,b,c,d) where+ fromType _ = (fromType @a1 (Proxy @a), fromType @b1 (Proxy @b), fromType @c1 (Proxy @c), fromType @d1 (Proxy @d))++instance (KnownVal a1 a, KnownVal b1 b, KnownVal c1 c, KnownVal d1 d, KnownVal e1 e) => KnownVal (a1,b1,c1,d1,e1) '(a,b,c,d,e) where+ fromType _ = (fromType @a1 (Proxy @a), fromType @b1 (Proxy @b), fromType @c1 (Proxy @c), fromType @d1 (Proxy @d), fromType @e1 (Proxy @e))++--------------------------------------------------------------------------------++-- ErrorMessage from GHC.TypeLits++instance (IsString str, KnownSymbol sym) => KnownVal str ('TL.Text sym) where+ fromType _ = fromType @str (Proxy @sym)++instance (IsString str, Typeable typ) => KnownVal str ('TL.ShowType typ) where+ fromType _ = fromString $ show $ typeRep (Proxy @typ)++instance (IsString str, KnownVal str err1, KnownVal str err2, Semigroup str) => KnownVal str (err1 'TL.:<>: err2) where+ fromType _ = fromType (Proxy @err1) <> fromType (Proxy @err2)++instance (IsString str, KnownVal str err1, KnownVal str err2, Semigroup str) => KnownVal str (err1 'TL.:$$: err2) where+ fromType _ = fromType (Proxy @err1) <> fromString "\n" <> fromType (Proxy @err2)
src/Fcf/Data/Set.hs view
@@ -1,5 +1,3 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-}@@ -63,7 +61,7 @@ import Fcf ( Eval, Exp, type (=<<), type (<=<), type (&&) , Not, If, Map, Flip, TyEq )-import qualified Fcf as Fcf (Foldr, Filter)+import qualified Fcf (Foldr, Filter) import Fcf.Class.Foldable (All, Any) import Fcf.Data.List ( Elem, Cons, Concat, Reverse, Length, type (++) , ZipWith, Replicate)@@ -75,28 +73,18 @@ -------------------------------------------------------------------------------- --- For the doctests:---- $setup--- >>> import qualified GHC.TypeLits as TL--- >>> import Fcf.Data.Nat--- >>> import Fcf.Data.Symbol--- >>> import Fcf.Alg.Sort----------------------------------------------------------------------------------- -- | Set-definition.-data Set a = Set [a]+newtype Set a = Set [a] -------------------------------------------------------------------------------- -- | Empty--- +-- -- === __Example__--- --- >>> :kind! (Eval Empty :: Set Nat)--- (Eval Empty :: Set Nat) :: Set Nat+--+-- > :kind! (Eval Empty :: Set Nat)+-- (Eval Empty :: Set Nat) :: Set TL.Natural -- = 'Set '[] -- -- See also the other examples in this module.@@ -104,11 +92,11 @@ type instance Eval Empty = 'Set '[] -- | Singleton--- +-- -- === __Example__--- --- >>> :kind! Eval (Singleton 1)--- Eval (Singleton 1) :: Set Nat+--+-- > :kind! Eval (Singleton 1)+-- Eval (Singleton 1) :: Set TL.Natural -- = 'Set '[1] data Singleton :: v -> Exp (Set v) type instance Eval (Singleton v) = 'Set '[v]@@ -118,12 +106,12 @@ -- -- === __Example__ ----- >>> :kind! Eval (Insert 3 =<< FromList '[1, 2])--- Eval (Insert 3 =<< FromList '[1, 2]) :: Set Nat+-- > :kind! Eval (Insert 3 =<< FromList '[1, 2])+-- Eval (Insert 3 =<< FromList '[1, 2]) :: Set TL.Natural -- = 'Set '[3, 1, 2] ----- >>> :kind! Eval (Insert 2 =<< FromList '[1, 2])--- Eval (Insert 2 =<< FromList '[1, 2]) :: Set Nat+-- > :kind! Eval (Insert 2 =<< FromList '[1, 2])+-- Eval (Insert 2 =<< FromList '[1, 2]) :: Set TL.Natural -- = 'Set '[1, 2] data Insert :: v -> Set v -> Exp (Set v) type instance Eval (Insert v ('Set lst)) =@@ -132,15 +120,15 @@ ('Set (v ': lst)) -- | Delete--- +-- -- === __Example__--- --- >>> :kind! Eval (Delete 5 =<< FromList '[5, 3])--- Eval (Delete 5 =<< FromList '[5, 3]) :: Set Nat+--+-- > :kind! Eval (Delete 5 =<< FromList '[5, 3])+-- Eval (Delete 5 =<< FromList '[5, 3]) :: Set TL.Natural -- = 'Set '[3] ----- >>> :kind! Eval (Delete 7 =<< FromList '[5, 3])--- Eval (Delete 7 =<< FromList '[5, 3]) :: Set Nat+-- > :kind! Eval (Delete 7 =<< FromList '[5, 3])+-- Eval (Delete 7 =<< FromList '[5, 3]) :: Set TL.Natural -- = 'Set '[5, 3] data Delete :: v -> Set v -> Exp (Set v) type instance Eval (Delete v ('Set lst)) =@@ -149,11 +137,12 @@ -- | Member -- -- === __Example__--- --- >>> :kind! Eval (Member 5 =<< FromList '[5, 3])+--+-- > :kind! Eval (Member 5 =<< FromList '[5, 3]) -- Eval (Member 5 =<< FromList '[5, 3]) :: Bool -- = 'True--- >>> :kind! Eval (Member 7 =<< FromList '[5, 3])+--+-- > :kind! Eval (Member 7 =<< FromList '[5, 3]) -- Eval (Member 7 =<< FromList '[5, 3]) :: Bool -- = 'False data Member :: v -> Set v -> Exp Bool@@ -162,11 +151,12 @@ -- | NotMember -- -- === __Example__--- --- >>> :kind! Eval (NotMember 5 =<< FromList '[5, 3])+--+-- > :kind! Eval (NotMember 5 =<< FromList '[5, 3]) -- Eval (NotMember 5 =<< FromList '[5, 3]) :: Bool -- = 'False--- >>> :kind! Eval (NotMember 7 =<< FromList '[5, 3])+--+-- > :kind! Eval (NotMember 7 =<< FromList '[5, 3]) -- Eval (NotMember 7 =<< FromList '[5, 3]) :: Bool -- = 'True data NotMember :: v -> Set v -> Exp Bool@@ -177,11 +167,12 @@ -- | Null -- -- === __Example__--- --- >>> :kind! Eval (Null =<< FromList '[5, 3])+--+-- > :kind! Eval (Null =<< FromList '[5, 3]) -- Eval (Null =<< FromList '[5, 3]) :: Bool -- = 'False--- >>> :kind! Eval (Null =<< Empty)+-- +-- > :kind! Eval (Null =<< Empty) -- Eval (Null =<< Empty) :: Bool -- = 'True data Null :: Set v -> Exp Bool@@ -192,31 +183,31 @@ -- | Size -- -- === __Example__--- --- >>> :kind! Eval (Size =<< FromList '[5, 3])--- Eval (Size =<< FromList '[5, 3]) :: Nat+--+-- > :kind! Eval (Size =<< FromList '[5, 3])+-- Eval (Size =<< FromList '[5, 3]) :: TL.Natural -- = 2 data Size :: Set v -> Exp TL.Nat type instance Eval (Size ('Set lst)) = Eval (Length lst) --- | IsSubsetOf +-- | IsSubsetOf -- -- === __Example__--- --- >>> :kind! Eval (IsSubsetOf ('Set '[]) ('Set '[0,1,2,3,4]))+--+-- > :kind! Eval (IsSubsetOf ('Set '[]) ('Set '[0,1,2,3,4])) -- Eval (IsSubsetOf ('Set '[]) ('Set '[0,1,2,3,4])) :: Bool -- = 'True ----- >>> :kind! Eval (IsSubsetOf ('Set '[0,1]) ('Set '[0,1,2,3,4]))+-- > :kind! Eval (IsSubsetOf ('Set '[0,1]) ('Set '[0,1,2,3,4])) -- Eval (IsSubsetOf ('Set '[0,1]) ('Set '[0,1,2,3,4])) :: Bool -- = 'True ----- >>> :kind! Eval (IsSubsetOf ('Set '[0,2,1,3,4]) ('Set '[0,1,2,3,4]))+-- > :kind! Eval (IsSubsetOf ('Set '[0,2,1,3,4]) ('Set '[0,1,2,3,4])) -- Eval (IsSubsetOf ('Set '[0,2,1,3,4]) ('Set '[0,1,2,3,4])) :: Bool -- = 'True ----- >>> :kind! Eval (IsSubsetOf ('Set '[0,1,2,3,4,5]) ('Set '[0,1,2,3,4]))+-- > :kind! Eval (IsSubsetOf ('Set '[0,1,2,3,4,5]) ('Set '[0,1,2,3,4])) -- Eval (IsSubsetOf ('Set '[0,1,2,3,4,5]) ('Set '[0,1,2,3,4])) :: Bool -- = 'False data IsSubsetOf :: Set a -> Set a -> Exp Bool@@ -224,15 +215,15 @@ Eval (All (Flip Elem s2) s1) --- | IsProperSubsetOf +-- | IsProperSubsetOf -- -- === __Example__--- --- >>> :kind! Eval (IsProperSubsetOf ('Set '[0,1,2,3,4]) ('Set '[0,1,2,3,4]))+--+-- > :kind! Eval (IsProperSubsetOf ('Set '[0,1,2,3,4]) ('Set '[0,1,2,3,4])) -- Eval (IsProperSubsetOf ('Set '[0,1,2,3,4]) ('Set '[0,1,2,3,4])) :: Bool -- = 'False ----- >>> :kind! Eval (IsProperSubsetOf ('Set '[0,2,1,3]) ('Set '[0,1,2,3,4]))+-- > :kind! Eval (IsProperSubsetOf ('Set '[0,2,1,3]) ('Set '[0,1,2,3,4])) -- Eval (IsProperSubsetOf ('Set '[0,2,1,3]) ('Set '[0,1,2,3,4])) :: Bool -- = 'True data IsProperSubsetOf :: Set a -> Set a -> Exp Bool@@ -245,10 +236,10 @@ -- | Type-level set union. -- -- === __Example__--- --- >>> :kind! Eval (Union (Eval (FromList '[5, 3])) (Eval (FromList '[5, 7])) )--- Eval (Union (Eval (FromList '[5, 3])) (Eval (FromList '[5, 7])) ) :: Set --- Nat+--+-- > :kind! Eval (Union (Eval (FromList '[5, 3])) (Eval (FromList '[5, 7])) )+-- Eval (Union (Eval (FromList '[5, 3])) (Eval (FromList '[5, 7])) ) :: Set+-- TL.Natural -- = 'Set '[7, 5, 3] data Union :: Set v -> Set v -> Exp (Set v) type instance Eval (Union ('Set lst1) ('Set lst2)) =@@ -262,12 +253,12 @@ -- | Type-level set difference.--- +-- -- === __Example__--- --- >>> :kind! Eval (Difference (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7])))--- Eval (Difference (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7]))) :: Set --- Nat+--+-- > :kind! Eval (Difference (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7])))+-- Eval (Difference (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7]))) :: Set+-- TL.Natural -- = 'Set '[3] data Difference :: Set v -> Set v -> Exp (Set v) type instance Eval (Difference ('Set lst1) ('Set lst2)) =@@ -281,10 +272,10 @@ -- | Type-level set intersection. -- -- === __Example__--- --- >>> :kind! Eval (Intersection (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7])))--- Eval (Intersection (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7]))) :: Set --- Nat+--+-- > :kind! Eval (Intersection (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7])))+-- Eval (Intersection (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7]))) :: Set+-- TL.Natural -- = 'Set '[5] data Intersection :: Set v -> Set v -> Exp (Set v) type instance Eval (Intersection ('Set lst1) ('Set lst2)) =@@ -307,10 +298,10 @@ -- helper for PowerSet data ExtendBitList :: [[Bool]] -> Exp [[Bool]] type instance Eval (ExtendBitList lst) =- Eval ((Eval (AddFalses lst)) ++ (Eval (AddTrues =<< Map Reverse lst)))+ Eval (Eval (AddFalses lst) ++ Eval (AddTrues =<< Map Reverse lst)) -- helper for PowerSet--- :kind! Eval (Cata BuildGrayBitListsAlg=<< ListToFix =<< Replicate 3 '[])+-- :kind! Eval (Cata BuildGrayBitListsAlg =<< ListToFix =<< Replicate 3 '[]) data BuildGrayBitListsAlg :: Algebra (ListF [[Bool]]) [[Bool]] type instance Eval (BuildGrayBitListsAlg 'NilF) = '[ '[] ] type instance Eval (BuildGrayBitListsAlg ('ConsF _ lst)) = Eval (ExtendBitList lst)@@ -330,20 +321,22 @@ type instance Eval (SelectWithBools elms bls) = Eval (Concat =<< ZipWith SelWithBool elms bls) --- | Calculate the power sets of a given type-level list. The algorithm is based +-- | Calculate the power sets of a given type-level list. The algorithm is based -- on Gray codes. -- -- === __Example__ ----- >>> :kind! Eval (PowerSet =<< FromList '["a", "b", "c"])--- Eval (PowerSet =<< FromList '["a", "b", "c"]) :: Set (Set Symbol)+-- > :kind! Eval (PowerSet =<< FromList '["a", "b", "c"])+-- Eval (PowerSet =<< FromList '["a", "b", "c"]) :: Set+-- (Set TL.Symbol) -- = 'Set -- '[ 'Set '[], 'Set '["c"], 'Set '["b"], 'Set '["b", "c"], -- 'Set '["a"], 'Set '["a", "b"], 'Set '["a", "c"], -- 'Set '["a", "b", "c"]] ----- >>> :kind! Eval (PowerSet =<< FromList '[Int, Char, Maybe Int])--- Eval (PowerSet =<< FromList '[Int, Char, Maybe Int]) :: Set (Set *)+-- > :kind! Eval (PowerSet =<< FromList '[Int, Char, Maybe Int])+-- Eval (PowerSet =<< FromList '[Int, Char, Maybe Int]) :: Set+-- (Set (*)) -- = 'Set -- '[ 'Set '[], 'Set '[Maybe Int], 'Set '[Char], -- 'Set '[Char, Maybe Int], 'Set '[Int], 'Set '[Int, Char],@@ -360,9 +353,9 @@ -- | Use FromList to construct a Set from type-level list. -- -- === __Example__--- --- >>> :kind! Eval (FromList '[1, 2])--- Eval (FromList '[1, 2]) :: Set Nat+--+-- > :kind! Eval (FromList '[1, 2])+-- Eval (FromList '[1, 2]) :: Set TL.Natural -- = 'Set '[1, 2] data FromList :: [v] -> Exp (Set v) type instance Eval (FromList lst) = 'Set lst@@ -370,16 +363,15 @@ -- | Get the type-level list out of the 'Set'. -- -- === __Example__--- --- >>> :kind! Eval (ToList =<< PowerSet =<< FromList '[1,2,3])--- Eval (ToList =<< PowerSet =<< FromList '[1,2,3]) :: [Set Nat]+--+-- > :kind! Eval (ToList =<< PowerSet =<< FromList '[1,2,3])+-- Eval (ToList =<< PowerSet =<< FromList '[1,2,3]) :: [Set+-- TL.Natural] -- = '[ 'Set '[], 'Set '[3], 'Set '[2], 'Set '[2, 3], 'Set '[1], -- 'Set '[1, 2], 'Set '[1, 3], 'Set '[1, 2, 3]] ----- >>> :kind! Eval (Qsort NatListOrd =<< Map ToList =<< ToList =<< PowerSet =<< FromList '[1,2,3])--- Eval (Qsort NatListOrd =<< Map ToList =<< ToList =<< PowerSet =<< FromList '[1,2,3]) :: [[Nat]]+-- > :kind! Eval (Qsort NatListOrd =<< Map ToList =<< ToList =<< PowerSet =<< FromList '[1,2,3])+-- Eval (Qsort NatListOrd =<< Map ToList =<< ToList =<< PowerSet =<< FromList '[1,2,3]) :: [[TL.Natural]] -- = '[ '[], '[1], '[1, 2], '[1, 2, 3], '[1, 3], '[2], '[2, 3], '[3]] data ToList :: Set v -> Exp [v] type instance Eval (ToList ('Set lst)) = lst--
+ src/Fcf/Data/Symbol.hs view
@@ -0,0 +1,142 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wall #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{-|+Module : Fcf.Data.Symbol+Description : Type-level Symbol helpers for Fcf libs+Copyright : (c) gspia 2023-+License : BSD+Maintainer : gspia++= Fcf.Data.Symbol++This might should go to first-class-families.++-}++--------------------------------------------------------------------------------++module Fcf.Data.Symbol+ where+++import Fcf.Core +import qualified GHC.TypeLits as TL+++--------------------------------------------------------------------------------++-- Version should be larger than 9.2.x. Note the two digit space for the+-- minor.+#if __GLASGOW_HASKELL__ >= 902++import Fcf ( type (=<<), Foldr )+import Fcf.Data.List ( type (++) )+++data AppendSymbol :: TL.Symbol -> TL.Symbol -> Exp TL.Symbol+type instance Eval (AppendSymbol a b) = TL.AppendSymbol a b++data CmpSymbol :: TL.Symbol -> TL.Symbol -> Exp Ordering+type instance Eval (CmpSymbol a b) = TL.CmpSymbol a b++data CmpChar :: Char -> Char -> Exp Ordering+type instance Eval (CmpChar a b) = TL.CmpChar a b++data ConsChar :: Char -> TL.Symbol -> Exp TL.Symbol+type instance Eval (ConsChar a b) = TL.ConsSymbol a b++data UnconsSymbol :: TL.Symbol -> Exp (Maybe (Char, TL.Symbol))+type instance Eval (UnconsSymbol a) = TL.UnconsSymbol a++data CharToNat :: Char -> Exp TL.Nat+type instance Eval (CharToNat c) = TL.CharToNat c++data NatToChar :: TL.Nat -> Exp Char+type instance Eval (NatToChar n) = TL.NatToChar n+++-- Helper for ToCharList method.+data HandlePair :: Maybe (Char, TL.Symbol) -> Exp [Char]+type instance Eval (HandlePair 'Nothing) = '[]+type instance Eval (HandlePair ('Just '(c, sym))) =+ Eval ('[c] ++ (Eval (ToCharList sym)))++data ToCharList :: TL.Symbol -> Exp [Char]+type instance Eval (ToCharList sym) = Eval (HandlePair =<< UnconsSymbol sym)+++data CharToSymbol :: Char -> Exp TL.Symbol+type instance Eval (CharToSymbol c) = TL.ConsSymbol c ""++-- > :k! Eval (Concat '[ "aa", "bb", "cc"])+-- Eval (Concat '[ "aa", "bb", "cc"]) :: TL.Symbol+-- = "aabbcc"+-- > :k! Eval (Concat '[ ])+-- Eval (Concat '[ ]) :: TL.Symbol+-- = ""+data Concat :: [TL.Symbol] -> Exp TL.Symbol+type instance Eval (Concat syms) = Eval (Foldr AppendSymbol "" syms)+++data ConcatChars :: [Char] -> Exp TL.Symbol+type instance Eval (ConcatChars chrs) = Eval (Foldr ConsChar "" chrs)+++--------------------------------------------------------------------------------++#else++--------------------------------------------------------------------------------+++-- These methods are not available on ghc 9.0 or lower (base 4.16 introduced).++data CmpSymbol :: TL.Symbol -> TL.Symbol -> Exp Ordering+type instance Eval (CmpSymbol a b) =+ TL.TypeError ('TL.Text "CmpSymbol in 9.2.x or higher")++data CmpChar :: Char -> Char -> Exp Ordering+type instance Eval (CmpChar a b) =+ TL.TypeError ('TL.Text "CmpChar in 9.2.x or higher")++data UnconsSymbol :: TL.Symbol -> Exp (Maybe (Char, TL.Symbol))+type instance Eval (UnconsSymbol a) =+ TL.TypeError ('TL.Text "UnconsSymbol in 9.2.x or higher")++data CharToNat :: Char -> Exp TL.Nat+type instance Eval (CharToNat c) =+ TL.TypeError ('TL.Text "CharToNat in 9.2.x or higher")++data NatToChar :: TL.Nat -> Exp Char+type instance Eval (NatToChar n) =+ TL.TypeError ('TL.Text "NatToChar in 9.2.x or higher")++data ConsChar :: Char -> TL.Symbol -> Exp TL.Symbol+type instance Eval (ConsChar a b) =+ TL.TypeError ('TL.Text "ConsChar in 9.2.x or higher")++data ToCharList :: TL.Symbol -> Exp [Char]+type instance Eval (ToCharList sym) =+ TL.TypeError ('TL.Text "ToCharList in 9.2.x or higher")++data CharToSymbol :: Char -> Exp TL.Symbol+type instance Eval (CharToSymbol c) =+ TL.TypeError ('TL.Text "CharToSymbol in 9.2.x or higher")++data Concat :: [TL.Symbol] -> Exp TL.Symbol+type instance Eval (Concat lst) =+ TL.TypeError ('TL.Text "Concat in 9.2.x or higher")++data ConcatChars :: [Char] -> Exp TL.Symbol+type instance Eval (ConcatChars lst) =+ TL.TypeError ('TL.Text "ConcatChars in 9.2.x or higher")++#endif++--------------------------------------------------------------------------------
src/Fcf/Data/Text.hs view
@@ -1,5 +1,3 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-}@@ -16,22 +14,31 @@ = Fcf.Data.Text -We mimick Data.Text but on type level. The internal representation is based on-type level lists.+We mimick Data.Text but on type level. The current internal representation is based+on type level lists. The current (as of early 2023) implementation of this+Fcf.Data.Text will be deprecated and replaced with the contents of Fcf.Data.NewText+later 2023 as newer version GHC become more widespread. +The old version working with 9.0.x or less will be kept at Fcf.Data.OldText for+some time. Similarly, the module Fcf.Data.NewText contains the functions+and definitions for better Text type, which will be taken into use after some time.+ -} -------------------------------------------------------------------------------- module Fcf.Data.Text+ {-# WARNING "This still uses the OldText implementaion, which will be replaced with NewText implementation." #-} ( Text (..) -- * Creation , Empty , Singleton , FromList+ , FromSymbolList , ToList , ToSymbol+ , ToSymbolList -- * Basic Interface , Null@@ -86,6 +93,7 @@ ) where +import GHC.TypeLits (Symbol) import qualified GHC.TypeLits as TL import Fcf ( If, Eval, Exp, type (=<<), type (@@)@@ -95,8 +103,6 @@ import qualified Fcf.Data.List as F ( Length, Init, Reverse, Take, Drop, TakeWhile, DropWhile , Intercalate, Intersperse, IsPrefixOf, IsSuffixOf, IsInfixOf, Snoc)-import Fcf.Data.Symbol (Symbol)--- import qualified Fcf.Data.Symbol as FS import qualified Fcf.Class.Functor as F ( FMap ) @@ -120,7 +126,7 @@ -- | 'Text' is a data structure, that is, a list to hold type-level symbols of -- length one.-data Text = Text Symbol+newtype Text = Text Symbol -------------------------------------------------------------------------------- @@ -222,7 +228,7 @@ -- === __Example__ -- -- >>> :kind! Eval (Length =<< Singleton "ab")--- Eval (Length =<< Singleton "ab") :: Nat+-- Eval (Length =<< Singleton "ab") :: TL.Natural -- = 2 data Length :: Text -> Exp Nat type instance Eval (Length ('Text sym)) = Eval (F.Length (T.ToList sym))@@ -637,7 +643,7 @@ -- | Helper for SplitOn data SOLoop :: [Symbol] -> ([[Symbol]],[Symbol]) -> Exp [[Symbol]] type instance Eval (SOLoop sep '(acc, '[])) = acc-type instance Eval (SOLoop sep '(acc, (t ': txt))) =+type instance Eval (SOLoop sep '(acc, t ': txt)) = Eval (SOLoop sep =<< First (F.Snoc acc) =<< SOTake sep (t ': txt) '[]) @@ -665,7 +671,7 @@ -- | Helper for Split data SplitLoop :: (Symbol -> Exp Bool) -> ([[Symbol]],[Symbol]) -> Exp [[Symbol]] type instance Eval (SplitLoop p '(acc, '[])) = acc-type instance Eval (SplitLoop p '(acc, (t ': txt))) = +type instance Eval (SplitLoop p '(acc, t ': txt)) = Eval (SplitLoop p =<< First (F.Snoc acc) =<< SplitTake p (t ': txt) '[])
src/Fcf/Data/Text/Internal.hs view
@@ -1,7 +1,5 @@-{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-}@@ -20,7 +18,7 @@ This is from https://kcsongor.github.io/symbol-parsing-haskell/ -Ks. symbols library+Please do also check the symbols library at Hackage. -} @@ -29,7 +27,6 @@ module Fcf.Data.Text.Internal where import Data.Char (chr)--- import Data.Proxy import qualified GHC.TypeLits as TL import qualified Fcf.Data.List as L@@ -51,7 +48,7 @@ type family ToList (sym :: TL.Symbol) :: [TL.Symbol] where ToList sym = ToList1 sym "" --- Helper. +-- Helper. data ToSymbol2 :: [TL.Symbol] -> Exp TL.Symbol type instance Eval (ToSymbol2 lst) = Eval (Foldr S.Append "" lst)
src/Fcf/Data/Tree.hs view
@@ -1,5 +1,3 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-}@@ -34,9 +32,11 @@ module Fcf.Data.Tree where -import Fcf as Fcf+import Fcf import Fcf.Data.List as Fcf +import Fcf.Control.Monad as M+ -------------------------------------------------------------------------------- -- For the doctests:@@ -55,6 +55,50 @@ -- in this module. type Forest a = [Tree a] ++type ExT1r =+ 'Node 1 '[ 'Node 2 '[ 'Node 3 '[ 'Node 4 '[]]], 'Node 5 '[ 'Node 6 '[]]]++type ExTr2 =+ 'Node ('Just 1)+ '[ 'Node ('Just 2)+ '[ 'Node ('Just 3)+ '[ 'Node ('Just 4) '[]]+ ]+ , 'Node ('Just 5)+ '[ 'Node ('Just 6) '[]+ ]+ ]+++-- map for trees+type instance Eval (Map f ('Node a tr)) = 'Node (f @@ a) (Eval (Map (Map f) tr))++-- pure/return for trees+type instance Eval (M.Return a) = 'Node a '[]++-- M.<*> instance (applicative)+type instance Eval ('Node f tfs M.<*> 'Node x txs) =+ 'Node (Eval (f x))+ (Eval ( Eval (Map (Map f) txs)+ +++ Eval (Map (StarTx ('Node x txs)) tfs)+ -- (Eval (Map ( M.<*> ('Node x txs)) tfs))+ ))++-- Helper for M.<*>+data StarTx :: Tree a -> Tree (a -> Exp b) -> Exp (Tree b)+type instance Eval (StarTx fa fab) = Eval (fab M.<*> fa)+++-- :kind! Eval (Sequence ExTr2)+type instance Eval (Traverse f ('Node x ts)) =+ Eval (LiftA2 (Pure2 'Node) (Eval (f x)) (Eval (Traverse (Traverse f) ts)))+++--------------------------------------------------------------------------------++ -- | Fold a type-level 'Tree'. data FoldTree :: (a -> [b] -> Exp b) -> Tree a -> Exp b type instance Eval (FoldTree f ('Node a '[])) = Eval (f a '[])@@ -76,7 +120,7 @@ -- :} -- -- >>> :kind! Eval (UnfoldTree BuildNode 1)--- Eval (UnfoldTree BuildNode 1) :: Tree Nat+-- Eval (UnfoldTree BuildNode 1) :: Tree TL.Natural -- = 'Node -- 1 -- '[ 'Node 2 '[ 'Node 4 '[], 'Node 5 '[]],@@ -95,7 +139,7 @@ -- === __Example__ -- -- >>> :kind! Eval (Flatten ('Node 1 '[ 'Node 2 '[ 'Node 3 '[ 'Node 4 '[]]], 'Node 5 '[ 'Node 6 '[]]]))--- Eval (Flatten ('Node 1 '[ 'Node 2 '[ 'Node 3 '[ 'Node 4 '[]]], 'Node 5 '[ 'Node 6 '[]]])) :: [Nat]+-- Eval (Flatten ('Node 1 '[ 'Node 2 '[ 'Node 3 '[ 'Node 4 '[]]], 'Node 5 '[ 'Node 6 '[]]])) :: [TL.Natural] -- = '[1, 2, 3, 4, 5, 6] data Flatten :: Tree a -> Exp [a] type instance Eval (Flatten ('Node a fs )) = a ': Eval (ConcatMap Flatten fs)@@ -127,9 +171,8 @@ -- === __Example__ -- -- >>> :kind! Eval (Levels ('Node 1 '[ 'Node 2 '[ 'Node 3 '[ 'Node 4 '[]]], 'Node 5 '[ 'Node 6 '[]]]))--- Eval (Levels ('Node 1 '[ 'Node 2 '[ 'Node 3 '[ 'Node 4 '[]]], 'Node 5 '[ 'Node 6 '[]]])) :: [[Nat]]+-- Eval (Levels ('Node 1 '[ 'Node 2 '[ 'Node 3 '[ 'Node 4 '[]]], 'Node 5 '[ 'Node 6 '[]]])) :: [[TL.Natural]] -- = '[ '[1], '[2, 5], '[3, 6], '[4]] data Levels :: Tree a -> Exp [[a]] type instance Eval (Levels tr) = Eval (Unfoldr SubFLevels '[tr])-
+ src/Fcf/Data/Tuple.hs view
@@ -0,0 +1,59 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wall #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{-|+Module : Fcf.Data.Tuple+Description : Type-level tuple functions+Copyright : (c) gspia 2020-+License : BSD+Maintainer : gspia++= Fcf.Data.Tuple+++-}++--------------------------------------------------------------------------------++module Fcf.Data.Tuple where++import Fcf (Eval, Exp)++--------------------------------------------------------------------------------++-- For the doctests:++-- $setup+-- >>> import qualified GHC.TypeLits as TL++--------------------------------------------------------------------------------++-- | Swap+--+-- === __Example__+--+-- >>> :kind! Eval (Swap '(1, 2))+-- Eval (Swap '(1, 2)) :: (TL.Natural, TL.Natural)+-- = '(2, 1)+data Swap :: (a, b) -> Exp (b, a)+type instance Eval (Swap '(a,b)) = '(b,a)++-- | 2-tuple to allow for partial application of 2-tuple at the type level+data Tuple2 :: a -> b -> Exp (a, b)+type instance Eval (Tuple2 a b) = '(a,b)++-- | 3-tuple to allow for partial application of 3-tuple at the type level+data Tuple3 :: a -> b -> c -> Exp (a, b, c)+type instance Eval (Tuple3 a b c) = '(a,b,c)++-- | 4-tuple to allow for partial application of 4-tuple at the type level+data Tuple4 :: a -> b -> c -> d -> Exp (a, b, c, d)+type instance Eval (Tuple4 a b c d) = '(a,b,c,d)++-- | 5-tuple to allow for partial application of 4-tuple at the type level+data Tuple5 :: a -> b -> c -> d -> e -> Exp (a, b, c, d, e)+type instance Eval (Tuple5 a b c d e) = '(a,b,c,d,e)+
+ test/Test/Alg.hs view
@@ -0,0 +1,22 @@++module Test.Alg where++import Test.Alg.List as L (spec)+import Test.Alg.Morphism as M (spec)+import Test.Alg.Nat as N (spec)+import Test.Alg.Other as O (spec)+import Test.Alg.Sort as So (spec)+import Test.Alg.Symbol as Sy (spec)+import Test.Alg.Tree as T (spec)+import Test.Hspec (describe, Spec)++spec :: Spec+spec = describe "Alg" $ do+ L.spec+ M.spec+ N.spec+ O.spec+ So.spec+ Sy.spec+ T.spec+
+ test/Test/Alg/List.hs view
@@ -0,0 +1,171 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wall #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{- +In this module, we test mainly Fcf.Alg.List module. In couple of +places, we use the "spec" and Reflect. ++Many of the tests are such that if the answer is not correct, the+whole test module refuses to compile. Please do try to change some +of the values to see. ++Note that in a way, the spec tests are not needed. If testing just +the type level behaviour, the module would refuse to compile if +test is not ok (and thus, guard the quality earlier than what the +test framework can do). ++Anyhow, as these also work as examples, it is probably ok to have different +ways of reaching the results. (E.g. to see, how to get the type level +values to value level.)++-}+module Test.Alg.List where++import Data.Proxy+import Data.Type.Equality ((:~:)(Refl))+import Test.Hspec (describe, it, shouldBe, Spec)++import Fcf.Core (Eval)+import Fcf.Combinators (type (=<<))+import Fcf.Alg.List+import Fcf.Alg.Morphism+import Fcf.Data.Reflect (fromType)++--------------------------------------------------------------------------------++-- This module won't compile, if the Refl doesn't give the correct answer.+--+-- > :kind! Eval (ListToFix '[1,2,3])+-- Eval (ListToFix '[1,2,3]) :: Fix (ListF TL.Natural)+-- = 'Fix ('ConsF 1 ('Fix ('ConsF 2 ('Fix ('ConsF 3 ('Fix 'NilF))))))+_ = Refl :: Eval (ListToFix '[1,2,3])+ :~: 'Fix ('ConsF 1 ('Fix ('ConsF 2 ('Fix ('ConsF 3 ('Fix 'NilF))))))+++-- This module won't compile, if the Refl doesn't give the correct answer.+-- +-- > :kind! Eval (ListToParaFix '[1,2,3])+-- Eval (ListToParaFix '[1,2,3]) :: Fix+-- (ListF (TL.Natural, [TL.Natural]))+-- = 'Fix+-- ('ConsF+-- '(1, '[2, 3])+-- ('Fix ('ConsF '(2, '[3]) ('Fix ('ConsF '(3, '[]) ('Fix 'NilF))))))+_ = Refl :: Eval (ListToParaFix '[1,2,3])+ :~: 'Fix ('ConsF+ '(1, '[2, 3])+ ('Fix ('ConsF '(2, '[3]) ('Fix ('ConsF '(3, '[]) ('Fix 'NilF))))))+++-- This module won't compile, if the Refl doesn't give the correct answer.+-- +-- > :kind! Eval (Para DedupAlg =<< ListToParaFix '[1,1,3,2,5,1,3,2])+-- Eval (Para DedupAlg =<< ListToParaFix '[1,1,3,2,5,1,3,2]) :: [TL.Natural]+-- = '[5, 1, 3, 2]+_ = Refl :: Eval (Para DedupAlg =<< ListToParaFix '[1,1,3,2,5,1,3,2])+ :~: '[5, 1, 3, 2]+++-- This module won't compile, if the Refl doesn't give the correct answer.+-- +-- > :kind! Eval (Sliding 3 '[1,2,3,4,5,6])+-- Eval (Sliding 3 '[1,2,3,4,5,6]) :: [[TL.Natural]]+-- = '[ '[1, 2, 3], '[2, 3, 4], '[3, 4, 5], '[4, 5, 6], '[5, 6], '[6]]+_ = Refl :: Eval (Sliding 3 '[1,2,3,4,5,6])+ :~: '[ '[1, 2, 3], '[2, 3, 4], '[3, 4, 5], '[4, 5, 6], '[5, 6], '[6]]+++-- This module won't compile, if the Refl doesn't give the correct answer.+-- +-- > :kind! Eval (Evens =<< RunInc 8)+-- Eval (Evens =<< RunInc 8) :: [TL.Natural]+-- = '[2, 4, 6, 8]+_ = Refl :: Eval (Evens =<< RunInc 8)+ :~: '[2, 4, 6, 8]+++-- This module won't compile, if the Refl doesn't give the correct answer.+-- +-- > :kind! Eval (RunInc 8)+-- Eval (RunInc 8) :: [TL.Natural]+-- = '[1, 2, 3, 4, 5, 6, 7, 8]+_ = Refl :: Eval (RunInc 8)+ :~: '[1, 2, 3, 4, 5, 6, 7, 8]+++-- This module won't compile, if the Refl doesn't give the correct answer.+-- +-- > :kind! Eval (MToN 1 3)+-- Eval (MToN 1 3) :: [TL.Natural]+-- = '[1, 2, 3]+_ = Refl :: Eval (MToN 1 3)+ :~: '[1, 2, 3]++-- This module won't compile, if the Refl doesn't give the correct answer.+-- +-- > :kind! Eval (ToList 1)+-- Eval (ToList 1) :: [TL.Natural]+-- = '[1]+_ = Refl :: Eval (ToList 1)+ :~: '[1]++ +--------------------------------------------------------------------------------++-- > :kind! Eval (Cata LenAlg =<< ListToFix '[1,2,3])+-- Eval (Cata LenAlg =<< ListToFix '[1,2,3]) :: TL.Natural+-- = 3++-- > :kind! Eval (Cata SumAlg =<< ListToFix '[1,2,3,4])+-- Eval (Cata SumAlg =<< ListToFix '[1,2,3,4]) :: TL.Natural+-- = 10++-- > :kind! Eval (Cata ProdAlg =<< ListToFix '[1,2,3,4])+-- Eval (Cata ProdAlg =<< ListToFix '[1,2,3,4]) :: TL.Natural+-- = 24++-- > :kind! Eval (Sum '[1,2,3])+-- Eval (Sum '[1,2,3]) :: TL.Natural+-- = 6++-- > :kind! Eval (Equal '[1,2,3] '[1,2,3])+-- Eval (Equal '[1,2,3] '[1,2,3]) :: Bool+-- = 'True++-- > :kind! Eval (Equal '[1,2,3] '[1,3,2])+-- Eval (Equal '[1,2,3] '[1,3,2]) :: Bool+-- = 'False++spec :: Spec+spec = describe "List" $ do+ it "Cata LenAlg" $ do+ let test :: forall r. (r ~ Eval (Cata LenAlg =<< ListToFix '[1,2,3])) => Int+ test = fromType (Proxy @r)+ test `shouldBe` 3+ it "Cata SumAlg" $ do+ let test :: forall r. (r ~ Eval (Cata SumAlg =<< ListToFix '[1,2,3,4])) => Int+ test = fromType (Proxy @r)+ test `shouldBe` 10+ it "Cata ProdAlg" $ do+ let test :: forall r. (r ~ Eval (Cata ProdAlg =<< ListToFix '[1,2,3,4])) => Int+ test = fromType (Proxy @r)+ test `shouldBe` 24+ it "Sum" $ do+ let test :: forall r. (r ~ Eval (Sum '[1,2,3])) => Int+ test = fromType (Proxy @r)+ test `shouldBe` 6+ it "Equal, True" $ do+ let test :: forall r. (r ~ Eval (Equal '[1,2,3] '[1,2,3])) => Bool+ test = fromType (Proxy @r)+ test `shouldBe` True+ it "Equal, False" $ do+ let test :: forall r. (r ~ Eval (Equal '[1,2,3] '[1,3,2])) => Bool+ test = fromType (Proxy @r)+ test `shouldBe` False+
+ test/Test/Alg/Morphism.hs view
@@ -0,0 +1,85 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wall #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{- +In this module, we test mainly Fcf.Alg.Morphism module. In couple of +places, we use the "spec" and Reflect. ++Many of the tests are such that if the answer is not correct, the+whole test module refuses to compile. Please do try to change some +of the values to see. ++Note that in a way, the spec tests are not needed. If testing just +the type level behaviour, the module would refuse to compile if +test is not ok (and thus, guard the quality earlier than what the +test framework can do). ++Anyhow, as these also work as examples, it is probably ok to have different +ways of reaching the results. (E.g. to see, how to get the type level +values to value level.)++-}+module Test.Alg.Morphism where++import qualified GHC.TypeLits as TL++import Data.Proxy+import Data.Type.Equality ((:~:)(Refl))+import Test.Hspec (describe, it, shouldBe, Spec)++import Fcf.Core (Eval)+import Fcf.Utils (If)+import Fcf.Alg.List+import Fcf.Alg.Morphism+import Fcf.Data.Nat+import Fcf.Data.Reflect (fromType)++--------------------------------------------------------------------------------++-- For the Ana and Hylo tests made below.+data NToOneCoA :: CoAlgebra (ListF Nat) Nat+type instance Eval (NToOneCoA b) =+ If (Eval (b < 1) )+ 'NilF+ ('ConsF b ( b TL.- 1))+++-- This module won't compile, if the Refl doesn't give the correct answer.+--+-- > :kind! Eval (Ana NToOneCoA 3)+-- Eval (Ana NToOneCoA 3) :: Fix (ListF TL.Natural)+-- = 'Fix ('ConsF 3 ('Fix ('ConsF 2 ('Fix ('ConsF 1 ('Fix 'NilF))))))+_ = Refl :: Eval (Ana NToOneCoA 3)+ :~: 'Fix ('ConsF 3 ('Fix ('ConsF 2 ('Fix ('ConsF 1 ('Fix 'NilF))))))++-- > :kind! Eval (Second ((+) 1) '("a",3))+-- Eval (Second ((+) 1) '("a",3)) :: (TL.Symbol, TL.Natural)+-- = '("a", 4)+_ = Refl :: Eval (Second ((+) 1) '("a",3))+ :~: '("a", 4)+++-- > :kind! Eval (Hylo SumAlg NToOneCoA 5)+-- Eval (Hylo SumAlg NToOneCoA 5) :: TL.Natural+-- = 15++-- > :kind! Eval (First ((+) 1) '(3,"a"))+-- Eval (First ((+) 1) '(3,"a")) :: (TL.Natural, TL.Symbol)+-- = '(4, "a")++spec :: Spec+spec = describe "Morphism" $ do+ it "Hylo SumAlg" $ do+ let test :: forall r. (r ~ Eval (Hylo SumAlg NToOneCoA 5)) => Int+ test = fromType (Proxy @r)+ test `shouldBe` 15+ it "First" $ do+ let test :: forall r. (r ~ Eval (First ((+) 1) '(3,"a"))) => (Int, String)+ test = fromType (Proxy @r)+ test `shouldBe` (4,"a")
+ test/Test/Alg/Nat.hs view
@@ -0,0 +1,66 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wall #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{- +In this module, we test mainly Fcf.Alg.Nat module. In couple of +places, we use the "spec" and Reflect. ++Many of the tests are such that if the answer is not correct, the+whole test module refuses to compile. Please do try to change some +of the values to see. ++Note that in a way, the spec tests are not needed. If testing just +the type level behaviour, the module would refuse to compile if +test is not ok (and thus, guard the quality earlier than what the +test framework can do). ++Anyhow, as these also work as examples, it is probably ok to have different +ways of reaching the results. (E.g. to see, how to get the type level +values to value level.)++-}++module Test.Alg.Nat where++import Data.Proxy+import Data.Type.Equality ((:~:)(Refl))+import Test.Hspec (describe, it, shouldBe, Spec)++import Fcf.Core (Eval)+import Fcf.Alg.Nat+import Fcf.Data.Reflect (fromType)++-- > :kind! Eval (2 == 2)+-- Eval (2 == 2) :: Bool+-- = 'True+_ = Refl :: Eval (2==2) :~: 'True++-- > :kind! Eval (2 == 3)+-- Eval (2 == 3) :: Bool+-- = 'False+_ = Refl :: Eval (2==3) :~: 'False+++-- > :kind! Eval (2 /= 2)+-- Eval (2 /= 2) :: Bool+-- = 'False+--+-- > :kind! Eval (2 /= 3)+-- Eval (2 /= 3) :: Bool+-- = 'True+spec :: Spec+spec = describe "Nat" $ do+ it "In-equality, false" $ do+ let test :: forall r. (r ~ Eval (2 /= 2)) => Bool+ test = fromType (Proxy @r)+ test `shouldBe` False+ it "In-equality, true" $ do+ let test :: forall r. (r ~ Eval (2 /= 3)) => Bool+ test = fromType (Proxy @r)+ test `shouldBe` True
+ test/Test/Alg/Other.hs view
@@ -0,0 +1,54 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wall #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{- +In this module, we test mainly Fcf.Alg.Other module. In couple of +places, we use the "spec" and Reflect. ++Many of the tests are such that if the answer is not correct, the+whole test module refuses to compile. Please do try to change some +of the values to see. ++Note that in a way, the spec tests are not needed. If testing just +the type level behaviour, the module would refuse to compile if +test is not ok (and thus, guard the quality earlier than what the +test framework can do). ++Anyhow, as these also work as examples, it is probably ok to have different +ways of reaching the results. (E.g. to see, how to get the type level +values to value level.)++-}+module Test.Alg.Other where++import Data.Proxy+import Data.Type.Equality ((:~:)(Refl))+import Test.Hspec (describe, it, shouldBe, Spec)++import Fcf.Core (Eval)+import Fcf.Alg.Other+import Fcf.Data.Reflect (fromType)++-- > :kind! Eval (PairMaybeToMaybePair '( 'Just "txt", 'Just 1))+-- Eval (PairMaybeToMaybePair '( 'Just "txt", 'Just 1)) :: Maybe+-- (Symbol, TL.Natural)+-- = 'Just '("txt", 1)+_ = Refl :: Eval (PairMaybeToMaybePair '( 'Just "txt", 'Just 1)) + :~: 'Just '("txt", 1)+++-- > :kind! Eval (Id "id")+-- Eval (Id "id") :: Symbol+-- = "id"+spec :: Spec+spec = describe "Other" $ do+ it "Id" $ do+ let test :: forall r. (r ~ Eval (Id "id")) => String+ test = fromType (Proxy @r)+ test `shouldBe` "id"
+ test/Test/Alg/Sort.hs view
@@ -0,0 +1,56 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wall #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{- +In this module, we test mainly Fcf.Alg.Sort module. In couple of +places, we use the "spec" and Reflect. ++Many of the tests are such that if the answer is not correct, the+whole test module refuses to compile. Please do try to change some +of the values to see. ++Note that in a way, the spec tests are not needed. If testing just +the type level behaviour, the module would refuse to compile if +test is not ok (and thus, guard the quality earlier than what the +test framework can do). ++Anyhow, as these also work as examples, it is probably ok to have different +ways of reaching the results. (E.g. to see, how to get the type level +values to value level.)++-}++module Test.Alg.Sort where++import Data.Proxy+import Data.Type.Equality ((:~:)(Refl))+import Test.Hspec (describe, it, shouldBe, Spec)++import Fcf.Core (Eval)+import Fcf.Alg.Sort+import qualified Fcf.Alg.Symbol as S ( type (<) )+import qualified Fcf.Data.Nat as N ( type (<) )+import Fcf.Data.Reflect (fromType)++-- > :kind! Eval (Qsort (N.<) '[5,3,1,9,4,6,3])+-- Eval (Qsort (N.<) '[5,3,1,9,4,6,3]) :: [TL.Natural]+-- = '[1, 3, 3, 4, 5, 6, 9]+spec :: Spec+spec = describe "Sort" $ do+ it "QSort (<)" $ do+ let test :: forall r. (r ~ Eval (Qsort (N.<) '[5,3,1,9,4,6,3])) => [Int]+ test = fromType (Proxy @r)+ test `shouldBe` [1, 3, 3, 4, 5, 6, 9]++-- > :kind! Eval (Qsort (S.<) '[ "bb", "e", "a", "e", "d" ])+-- Eval (Qsort (S.<) '[ "bb", "e", "a", "e", "d" ]) :: [Symbol]+-- = '["a", "bb", "d", "e", "e"]+_ = Refl :: Eval (Qsort (S.<) '[ "bb", "e", "a", "e", "d" ])+ :~: '["a", "bb", "d", "e", "e"]+
+ test/Test/Alg/Symbol.hs view
@@ -0,0 +1,157 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wall #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{- +In this module, we test mainly Fcf.Alg.Symbol module. In couple of +places, we use the "spec" and Reflect. ++Many of the tests are such that if the answer is not correct, the+whole test module refuses to compile. Please do try to change some +of the values to see. ++Note that in a way, the spec tests are not needed. If testing just +the type level behaviour, the module would refuse to compile if +test is not ok (and thus, guard the quality earlier than what the +test framework can do). ++Anyhow, as these also work as examples, it is probably ok to have different +ways of reaching the results. (E.g. to see, how to get the type level +values to value level.)++-}++module Test.Alg.Symbol where++import Data.Proxy+import Data.Type.Equality ((:~:)(Refl))+import Test.Hspec (describe, it, shouldBe, Spec)++import Fcf.Core (Eval)+import Fcf.Alg.Symbol+import Fcf.Data.Reflect (fromType)++-- > :kind! Eval (Append "hmm" " ok")+-- Eval (Append "hmm" " ok") :: Symbol+-- = "hmm ok"+_ = Refl :: Eval (Append "hmm" " ok") :~: "hmm ok"++-- > :kind! Eval (Intercalate "+" '["aa", "bb", "cc"])+-- Eval (Intercalate "+" '["aa", "bb", "cc"]) :: Symbol+-- = "aa+bb+cc"+_ = Refl :: Eval (Intercalate "+" '["aa", "bb", "cc"]) :~: "aa+bb+cc"++-- > :kind! Eval (Intercalate "+" '["aa"])+-- Eval (Intercalate "+" '["aa"]) :: Symbol+-- = "aa"+_ = Refl :: Eval (Intercalate "+" '["aa"]) :~: "aa"++-- > :kind! Eval (Intercalate "+" '[])+-- Eval (Intercalate "+" '[]) :: Symbol+-- = ""+_ = Refl :: Eval (Intercalate "+" '[]) :~: ""++-- > :kind! Eval (IsSpace "a")+-- Eval (IsSpace "a") :: Bool+-- = 'False+_ = Refl :: Eval (IsSpace "a") :~: 'False+--+-- > :kind! Eval (IsSpace " ")+-- Eval (IsSpace " ") :: Bool+-- = 'True+_ = Refl :: Eval (IsSpace " ") :~: 'True++-- > :kind! Eval (IsNewLine "a")+-- Eval (IsNewLine "a") :: Bool+-- = 'False+_ = Refl :: Eval (IsNewLine "a") :~: 'False++-- > :kind! Eval (IsNewLine "\n")+-- Eval (IsNewLine "\n") :: Bool+-- = 'True+_ = Refl :: Eval (IsNewLine "\n") :~: 'True++-- > :kind! Eval (IsTab "a")+-- Eval (IsTab "a") :: Bool+-- = 'False+_ = Refl :: Eval (IsTab "a") :~: 'False+--+-- > :kind! Eval (IsTab "\t")+-- Eval (IsTab "\t") :: Bool+-- = 'True+_ = Refl :: Eval (IsTab "\t") :~: 'True++-- > :kind! Eval (IsSpaceDelim "a")+-- Eval (IsSpaceDelim "a") :: Bool+-- = 'False+_ = Refl :: Eval (IsSpaceDelim "a") :~: 'False+--+-- > :kind! Eval (IsSpaceDelim "\n")+-- Eval (IsSpaceDelim "\n") :: Bool+-- = 'True+_ = Refl :: Eval (IsSpaceDelim "\n") :~: 'True++-- > :kind! Eval (IsDigit "3")+-- Eval (IsDigit "3") :: Bool+-- = 'True+_ = Refl :: Eval (IsDigit "3") :~: 'True+--+-- > :kind! Eval (IsDigit "a")+-- Eval (IsDigit "a") :: Bool+-- = 'False+_ = Refl :: Eval (IsDigit "a") :~: 'False++-- > :kind! Eval (SymbolOrd "a" "b")+-- Eval (SymbolOrd "a" "b") :: Ordering+-- = 'LT+_ = Refl :: Eval (SymbolOrd "a" "b") :~: 'LT++--------------------------------------------------------------------------------++-- > :kind! Eval ("b" <= "a")+-- Eval ("b" <= "a") :: Bool+-- = 'False+--+-- > :kind! Eval ("b" >= "a")+-- Eval ("b" >= "a") :: Bool+-- = 'True+--+-- > :kind! Eval ("a" < "b")+-- Eval ("a" < "b") :: Bool+-- = 'True+--+-- > :kind! Eval ("b" > "a")+-- Eval ("b" > "a") :: Bool+-- = 'True+--+-- > :kind! Eval ("b" == "a")+-- Eval ("b" == "a") :: Bool+-- = 'False+spec :: Spec+spec = describe "Symbol" $ do+ it "<=" $ do+ let test :: forall r. (r ~ Eval ("b" <= "a")) => Bool+ test = fromType (Proxy @r)+ test `shouldBe` False+ it ">=" $ do+ let test :: forall r. (r ~ Eval ("b" >= "a")) => Bool+ test = fromType (Proxy @r)+ test `shouldBe` True+ it "<" $ do+ let test :: forall r. (r ~ Eval ("b" < "a")) => Bool+ test = fromType (Proxy @r)+ test `shouldBe` False+ it ">" $ do+ let test :: forall r. (r ~ Eval ("b" > "a")) => Bool+ test = fromType (Proxy @r)+ test `shouldBe` True+ it "==" $ do+ let test :: forall r. (r ~ Eval ("b" == "a")) => Bool+ test = fromType (Proxy @r)+ test `shouldBe` False+
+ test/Test/Alg/Tree.hs view
@@ -0,0 +1,129 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wall #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{- +In this module, we test mainly Fcf.Alg.Tree module. In couple of +places, we use the "spec" and Reflect. ++Many of the tests are such that if the answer is not correct, the+whole test module refuses to compile. Please do try to change some +of the values to see. ++Note that in a way, the spec tests are not needed. If testing just +the type level behaviour, the module would refuse to compile if +test is not ok (and thus, guard the quality earlier than what the +test framework can do). ++Anyhow, as these also work as examples, it is probably ok to have different +ways of reaching the results. (E.g. to see, how to get the type level +values to value level.)++-}++module Test.Alg.Tree where++import qualified GHC.TypeLits as TL++import Data.Proxy+import Data.Type.Equality ((:~:)(Refl))+import Test.Hspec (describe, it, shouldBe, Spec)++import Fcf.Data.Nat++import Fcf.Alg.Morphism +import Fcf.Alg.Tree+import Fcf.Combinators (type (=<<))+import Fcf.Core (Eval, Exp)+import Fcf.Utils (If)+import Fcf.Data.Reflect (fromType)+import Fcf.Data.Tree++data BuildNode :: Nat -> Exp (Nat,[Nat])+type instance Eval (BuildNode x) =+ If (Eval ((2 TL.* x TL.+ 1) >= 8))+ '(x, '[])+ '(x, '[ 2 TL.* x, (2 TL.* x) TL.+ 1 ])++-- > :kind! Eval (Size =<< UnfoldTree BuildNode 1)+-- Eval (Size =<< UnfoldTree BuildNode 1) :: TL.Natural+-- = 7+_ = Refl :: Eval (Size =<< UnfoldTree BuildNode 1) :~: 7+++-- :kind! Eval (Ana BuildNodeCoA 1)+-- :kind! Eval (Hylo CountNodesAlg BuildNodeCoA 1)+++-- > :kind! Eval (Sizes =<< Ana BuildNodeCoA 1)+-- Eval (Sizes =<< Ana BuildNodeCoA 1) :: Fix+-- (AnnF (TreeF TL.Natural) TL.Natural)+-- = 'Fix+-- ('AnnF+-- '( 'NodeF+-- 1+-- '[ 'Fix+-- ('AnnF+-- '( 'NodeF+-- 2+-- '[ 'Fix ('AnnF '( 'NodeF 4 '[], 1)),+-- 'Fix ('AnnF '( 'NodeF 5 '[], 1))],+-- 3)),+-- 'Fix+-- ('AnnF+-- '( 'NodeF+-- 3+-- '[ 'Fix ('AnnF '( 'NodeF 6 '[], 1)),+-- 'Fix ('AnnF '( 'NodeF 7 '[], 1))],+-- 3))],+-- 7))+_ = Refl :: Eval (Sizes =<< Ana BuildNodeCoA 1)+ :~: 'Fix+ ('AnnF+ '( 'NodeF+ 1+ '[ 'Fix+ ('AnnF+ '( 'NodeF+ 2+ '[ 'Fix ('AnnF '( 'NodeF 4 '[], 1)),+ 'Fix ('AnnF '( 'NodeF 5 '[], 1))],+ 3)),+ 'Fix+ ('AnnF+ '( 'NodeF+ 3+ '[ 'Fix ('AnnF '( 'NodeF 6 '[], 1)),+ 'Fix ('AnnF '( 'NodeF 7 '[], 1))],+ 3))],+ 7))++-- Turning this off, because of the slowness. In practice, this would+-- also require turning on ghc-options (-freduction-depth=0). +-- Please, do try on ghci.+-- > :kind! Eval (FibHisto 100)+-- Eval (FibHisto 100) :: TL.Natural+-- = 354224848179261915075+-- _ = Refl :: Eval (FibHisto 100) :~: 354224848179261915075++-- > :kind! Eval (FibHylo 10)+-- Eval (FibHylo 10) :: TL.Natural+-- = 55+spec :: Spec+spec = describe "Tree" $ do+ it "FibHisto" $ do+ let test :: forall r. (r ~ Eval (FibHylo 10)) => Int+ test = fromType (Proxy @r)+ test `shouldBe` 55+ -- The following is very slow and would require turning on ghc-options+ -- (-freduction-depth=0). + -- it "FibHisto" $ do+ -- let test :: forall r. (r ~ Eval (FibHisto 100)) => Integer+ -- test = fromType (Proxy @r)+ -- test `shouldBe` 354224848179261915075+
+ test/Test/Control.hs view
@@ -0,0 +1,9 @@++module Test.Control where++import Test.Control.Monad as M (spec)+import Test.Hspec (describe, Spec)++spec :: Spec+spec = describe "Control" $ do+ M.spec
+ test/Test/Control/Monad.hs view
@@ -0,0 +1,140 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wall #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++module Test.Control.Monad where++import Data.Functor ((<&>))+import Data.Proxy+import Control.Applicative+import Test.Hspec (describe, it, shouldBe, Spec)+import GHC.TypeLits (Nat, Symbol)++import Fcf hiding (type (<*>))+import Fcf.Data.Tuple+import Fcf.Data.List (Cons)+import Fcf.Control.Monad+import Fcf.Class.Monoid (type (.<>))+import Fcf.Data.Reflect (fromType)++-- data TraversableTest = TraversableTest Symbol [(Symbol, Nat)]++data SafeMinus :: Nat -> Nat -> Exp (Either Symbol Nat)+type instance Eval (SafeMinus a b) = If (Eval (a >= b)) ('Right (Eval (a - b))) ('Left "Nat cannot be negative")+++spec :: Spec+spec = describe "Monad" $ do+ it "liftA2 (,) instance" $ do+ let test :: forall r. (r ~ Eval (LiftA2 Tuple2 '("hello ", 5) '("world", 6))) => (String, (Int, Int))+ test = fromType (Proxy @r)+ test + `shouldBe` + liftA2 (,) ("hello ", 5) ("world", 6)+ it "<*> (,) instance" $ do+ let test :: forall r. (r ~ Eval ('("hello ", (+) 15) <*> '("world!", 2002))) => (String,Int)+ test = fromType (Proxy @r)+ test + `shouldBe` + ("hello ", (+) 15) <*> ("world!", 2002)+ it ">>= (,) instance" $ do+ let test :: forall r. (r ~ Eval ('("age", 5) >>= (Return <=< (+) 1))) => (String,Int)+ test = fromType (Proxy @r)+ test + `shouldBe` + (("age",5) <&> (+) 1)+ -- Above was suggested by hlint for the following:+ -- (("age",5) >>= return . (+) 1)+ it "liftA3 (,,) instance" $ do+ let test :: forall r. (r ~ Eval (LiftA3 Tuple3 '("hello ", "<", 6) '("world", " ", 8) '("!", ">", 10))) => (String, String, (Int, Int, Int))+ test = fromType (Proxy @r)+ test + `shouldBe` + liftA3 (,,) ("hello ","<",6) ("world"," ",8) ("!",">",10)+ it ">>= (,,) instance" $ do+ let test :: forall r. (r ~ Eval ('("he","wo",19) >>= (Tuple3 "llo" "rld" <=< Flip (-) 1))) => (String,String,Int)+ test = fromType (Proxy @r)+ test + `shouldBe` + (("he","wo",19) >>= ("llo","rld",) . flip (-) 1)+ it "liftA4 Either instance test Left" $ do+ let test :: forall r. (r ~ Eval (LiftA4 Tuple4 ('Right 5) ('Right 6) ('Right 7) ('Left "fail"))) => Either String (Int,Int,Int,Int)+ test = fromType (Proxy @r)+ test + `shouldBe` + (,,,) <$> Right 5 <*> Right 6 <*> Right 7 <*> Left "fail"+ it "liftA4 Either instance test Right" $ do+ let test :: forall r. (r ~ Eval (LiftA4 Tuple4 ('Right 5) ('Right 6) ('Right 7) ('Right 0))) => Either String (Int,Int,Int,Int)+ test = fromType (Proxy @r)+ test + `shouldBe` + (,,,) <$> Right 5 <*> Right 6 <*> Right 7 <*> Right 0+ it "Traversable Either instance, test with MapM" $ do+ let typeLevelFunc :: forall (list :: [(Symbol,Nat)]) r. + (r ~ Eval + (Map + (Flip Cons '[] <=< Tuple2 "test") + (MapM+ (MapM (Flip SafeMinus 1))+ @@ list+ )+ )+ ) => Proxy r+ typeLevelFunc = Proxy @r+ let safeMinus a b = if a >= b then Right (a - b) else Left "Nat cannot be negative"+ let valTest :: [(String,Int)] -> Either String [(String, [(String, Int)])]+ valTest list = fmap (flip (:) [] . ("test",)) (mapM (mapM (`safeMinus` 1)) list)+ fromType (typeLevelFunc @'[ '("key1",1), '("key2",2)])+ `shouldBe` + valTest [("key1",1),("key2",2)]+ fromType (typeLevelFunc @'[ '("key1",0), '("key2",2)])+ `shouldBe` + valTest [("key1",0),("key2",2)]+ it "liftA5 [] instance" $ do+ let test :: forall r. (r ~ Eval (LiftA5 Tuple5 '[1,5] '[2,4] '[6,7,8] '[9,11,10] '[0] )) => [(Int,Int,Int,Int,Int)]+ test = fromType (Proxy @r)+ test + `shouldBe` + (,,,,) <$> [1,5] <*> [2,4] <*> [6,7,8] <*> [9,11,10] <*> [0]+ it "<*> [] instance" $ do+ let test :: forall r. (r ~ Eval ('[(+) 1,(+) 2] <*> '[3,4])) => [Int]+ test = fromType (Proxy @r)+ test + `shouldBe` + [(+) 1,(+) 2] <*> [3,4]+ it ">>= [] instance" $ do+ let test :: forall r. (r ~ Eval ('[5,6,7] >>= Plus2M)) => [Int]+ test = fromType (Proxy @r)+ test + `shouldBe` + ([5,6,7] >>= (\n -> [n + 2, n + 3]))+ it ">>= Maybe instance test Just" $ do+ let test :: forall r. (r ~ Eval ('Just "hello" >>= (Return <=< Flip (.<>) " world"))) => Maybe String+ test = fromType (Proxy @r)+ test + `shouldBe` + (Just "hello" <&> flip (<>) " world")+ -- Above was suggested by hlint for the following:+ -- (Just "hello" >>= (return . flip (<>) " world"))+ it ">>= Maybe instance test Nothing" $ do+ let test :: forall r. (r ~ Eval ('Nothing >>= (Return <=< Flip (.<>) " world"))) => Maybe String+ test = fromType (Proxy @r)+ test + `shouldBe` + (Nothing <&> flip (<>) " world")+ -- Above was suggested by hlint for the following:+ -- (Nothing >>= (return . flip (<>) " world"))+ it ">> Maybe instance" $ do+ let test :: forall r. (r ~ Eval ('Just 5 >> 'Just "hello world")) => Maybe String+ test = fromType (Proxy @r)+ test + `shouldBe` + (Just (5 :: Int) >> Just "hello world")
+ test/Test/Data.hs view
@@ -0,0 +1,12 @@++module Test.Data where++import Test.Data.Reflect as R (spec)+import Test.Data.Set as S (spec)+import Test.Hspec (describe, Spec)++spec :: Spec+spec = describe "Data" $ do + R.spec+ S.spec+
+ test/Test/Data/Reflect.hs view
@@ -0,0 +1,328 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeOperators #-}+{-# OPTIONS_GHC -Wall #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++module Test.Data.Reflect where++import qualified Data.IntMap as IM+import qualified Data.Map as DM+import qualified Data.Set as DS+import qualified Data.Tree as DT+import qualified Data.Text as DTxt+import qualified GHC.TypeLits as TL+import Data.Proxy+import Test.Hspec (describe, it, shouldBe, Spec)++import Fcf (Eval, type (=<<))+import qualified Fcf.Data.Set as FS+import qualified Fcf.Data.NatMap as FNM+import qualified Fcf.Data.MapC as FNMC+#if __GLASGOW_HASKELL__ >= 902+import qualified Fcf.Data.NewText as FTxt+#endif+import qualified Fcf.Data.Tree as FT+import Fcf.Data.Reflect++--------------------------------------------------------------------------------++spec :: Spec+spec = describe "Reflect" $ do+ specTrees+ specMaybe+ specEither+ specMaybeEither+ specStructures+ specShowTypeable+ specErrorMessage+ +specBool :: Spec+specBool = describe "Bool" $ do+ it "Bool, True" $ do+ let test :: forall r. (r ~ 'True) => Bool+ test = fromType (Proxy @r)+ test `shouldBe` True+ it "Bool, False" $ do+ let test :: forall r. (r ~ 'False) => Bool+ test = fromType (Proxy @r)+ test `shouldBe` False++specMaybe :: Spec+specMaybe = describe "Maybe" $ do+ it "Maybe Int, Just" $ do+ let test :: forall r. (r ~ 'Just 5) + => Maybe Int+ test = fromType (Proxy @r)+ test `shouldBe` Just 5+ it "Maybe Int, Nothing" $ do+ let test :: forall r. (r ~ 'Nothing) + => Maybe Int+ test = fromType (Proxy @r)+ test `shouldBe` Nothing+ it "Maybe String, Just" $ do+ let test :: forall r. (r ~ 'Just "just") + => Maybe String+ test = fromType (Proxy @r)+ test `shouldBe` Just "just"+ it "Maybe String, Nothing" $ do+ let test :: forall r. (r ~ 'Nothing) + => Maybe String+ test = fromType (Proxy @r)+ test `shouldBe` Nothing++specEither :: Spec+specEither = describe "Either" $ do+ it "Either Int String, Left" $ do+ let test :: forall r. (r ~ 'Left 5) + => Either Int String+ test = fromType (Proxy @r)+ test `shouldBe` Left 5+ it "Either Int String, Right" $ do+ let test :: forall r. (r ~ 'Right "right") + => Either Int String+ test = fromType (Proxy @r)+ test `shouldBe` Right "right"+ it "Either Int (Either Int String), Right Right" $ do+ let test :: forall r. (r ~ 'Right ('Right "right"))+ => Either Int (Either Int String)+ test = fromType (Proxy @r)+ test `shouldBe` Right (Right "right")+ it "Either (Either Int String) String, Left Left" $ do+ let test :: forall r. (r ~ 'Left ('Left 5)) + => Either (Either Int String) String+ test = fromType (Proxy @r)+ test `shouldBe` Left (Left 5)++specMaybeEither :: Spec+specMaybeEither = describe "Maybe Either and Either Maybe" $ do+ it "Either Int (Maybe String), Right Just" $ do+ let test :: forall r. (r ~ 'Right ('Just "right just"))+ => Either Int (Maybe String)+ test = fromType (Proxy @r)+ test `shouldBe` Right (Just "right just")+ it "Either Int (Maybe String), Right Nothing" $ do+ let test :: forall r. (r ~ 'Right 'Nothing)+ => Either Int (Maybe String)+ test = fromType (Proxy @r)+ test `shouldBe` Right Nothing+ it "Maybe (Either Int String), Just Right" $ do+ let test :: forall r. (r ~ 'Just ('Right "just right"))+ => Maybe (Either Int String)+ test = fromType (Proxy @r)+ test `shouldBe` Just (Right "just right")+ it "Maybe (Either Int String), Nothing" $ do+ let test :: forall r. (r ~ 'Nothing)+ => Maybe (Either Int String)+ test = fromType (Proxy @r)+ test `shouldBe` Nothing+++specStructures :: Spec+specStructures = describe "Maps and other structures" $ do+ describe "[]" $ do+ it "[]" $ do+ let test :: forall r. (r ~ '[]) => [()]+ test = fromType (Proxy @r)+ test `shouldBe` []+ it "[(Bool,Int)]" $ do+ let test :: forall r. (r ~ '[ '( 'True,5), '( 'False,6)]) => [(Bool,Int)]+ test = fromType (Proxy @r)+ test `shouldBe` [(True,5),(False,6)]+ describe "IntMap" $ do+#if __GLASGOW_HASKELL__ >= 920+ it "IntMap char, from '[ '(Nat,Char) ]" $ do+ let test :: forall r. (r ~ '[ '(1,'H'), '(2,'e'), '(5,'o'), '(3,'b'), '(4,'l'), '(3,'l')]) => IM.IntMap Char+ test = fromType (Proxy @r)+ test `shouldBe` IM.fromList [(1,'H'),(2,'e'),(5,'o'),(4,'l'),(3,'l')]+#endif+ it "IntMap String, from NatMap" $ do+ let test :: forall r. (r ~ Eval (FNM.FromList '[ '(1,"H"), '(4,"b"), '(2,"e"), '(5,"o"), '(4,"l"), '(3,"l")])) => IM.IntMap String+ test = fromType (Proxy @r)+ test `shouldBe` IM.fromList [(2,"e"),(1,"H"),(4,"l"),(3,"l"),(5,"o")]+ it "IntMap String, with insert" $ do+ let test :: forall r. (r ~ Eval (+ FNM.Insert 3 "hih" =<< FNM.FromList '[ '(1,"haa"), '(2,"hoo")]+ )) + => IM.IntMap String+ test = fromType (Proxy @r)+ test + `shouldBe` + IM.fromList [ (3, "hih"), (1, "haa"), (2, "hoo")]+ describe "Map" $ do+#if __GLASGOW_HASKELL__ >= 920+ it "Map Int char, from '[ '(Nat,Char) ]" $ do+ let test :: forall r. (r ~ '[ '(1,'H'), '(2,'e'), '(5,'o'), '(4,'l'), '(3,'b'), '(3,'l')]) => DM.Map Int Char+ test = fromType (Proxy @r)+ test `shouldBe` DM.fromList [(1,'H'),(2,'e'),(5,'o'),(4,'l'),(3,'l')]+#endif+ it "Map Int String, from MapC" $ do+ let test :: forall r. (r ~ Eval (FNMC.FromList '[ '(1,"H"), '(2,"e"), '(3,"c"), '(5,"o"), '(4,"l"), '(3,"l")])) => DM.Map Int String+ test = fromType (Proxy @r)+ test `shouldBe` DM.fromList [(2,"e"),(1,"H"),(4,"l"),(3,"l"),(5,"o")]+ it "Map Int String, with insert" $ do+ let test :: forall r. (r ~ Eval (+ FNMC.Insert 3 "hih" =<< FNMC.FromList '[ '(1,"haa"), '(2,"hoo")]+ )) + => DM.Map Int String+ test = fromType (Proxy @r)+ test + `shouldBe` + DM.fromList [ (3, "hih"), (1, "haa"), (2, "hoo")]+ describe "Set" $ do+#if __GLASGOW_HASKELL__ >= 920+ it "Set char, from '[Char]" $ do+ let test :: forall r. (r ~ '[ 'H','e','o','l','l' ]) => DS.Set Char+ test = fromType (Proxy @r)+ test `shouldBe` DS.fromList ['H','e','o','l','l']+#endif+ it "Set String, from Set" $ do+ let test :: forall r. (r ~ Eval (FS.FromList '["H","e","o","l","l"])) => DS.Set String+ test = fromType (Proxy @r)+ test `shouldBe` DS.fromList ["e","H","l","l","o"]+ it "Set Int" $ do+ let test :: forall r. (r ~ Eval (FS.FromList '[5, 9, 1, 8, 3, 5])) + => DS.Set Int+ test = fromType (Proxy @r)+ test + `shouldBe` + DS.fromList [1, 3, 5, 8, 9]+#if __GLASGOW_HASKELL__ >= 902+ it "text" $ do+ let test :: forall r. (r ~ 'FTxt.Text "trial") => DTxt.Text+ test = fromType (Proxy @r)+ test + `shouldBe` + DTxt.pack "trial"+#endif++type ExTr1 =+ 'FT.Node 1 + '[ 'FT.Node 2 + '[ 'FT.Node 3 '[ 'FT.Node 4 '[]]]+ , 'FT.Node 5 '[ 'FT.Node 6 '[]]+ ]++type ExTr2 =+ 'FT.Node ('Just 1)+ '[ 'FT.Node ('Just 2)+ '[ 'FT.Node ('Just 3)+ '[ 'FT.Node ('Just 4) '[]]+ ]+ , 'FT.Node ('Just 5)+ '[ 'FT.Node ('Just 6) '[]+ ]+ ]++type ExTr3 =+ 'FT.Node ('Just 1)+ '[ 'FT.Node ('Just 2)+ '[ 'FT.Node ('Just 3)+ '[ 'FT.Node ('Just 4) '[]]+ ]+ , 'FT.Node ('Just 5)+ '[ 'FT.Node 'Nothing '[]+ ]+ ]++type ExTr4 =+ 'FT.Node ('Left 1)+ '[ 'FT.Node ('Right "two")+ '[ 'FT.Node ('Left 3)+ '[ 'FT.Node ('Right "four") '[]]+ ]+ , 'FT.Node ('Left 5)+ '[ 'FT.Node ('Right "six") '[]+ ]+ ]+ +specTrees :: Spec+specTrees = describe "Tree structures" $ do+ it "tree 1" $ do+ let test :: forall r. (r ~ ExTr1) + => DT.Tree Int+ test = fromType (Proxy @r)+ test + `shouldBe` + DT.Node 1 [DT.Node 2 [DT.Node 3 [DT.Node 4 []]], DT.Node 5 [DT.Node 6 []]]+ it "tree 2" $ do+ let test :: forall r. (r ~ ExTr2) + => DT.Tree (Maybe Int)+ test = fromType (Proxy @r)+ test + `shouldBe` + DT.Node (Just 1) + [ DT.Node (Just 2) + [ DT.Node (Just 3) + [ DT.Node (Just 4) []+ ]+ ]+ , DT.Node (Just 5) + [DT.Node (Just 6) []+ ]+ ]+ it "tree 3" $ do+ let test :: forall r. (r ~ ExTr3) + => DT.Tree (Maybe Int)+ test = fromType (Proxy @r)+ test + `shouldBe` + DT.Node (Just 1) + [ DT.Node (Just 2) + [ DT.Node (Just 3) + [ DT.Node (Just 4) []+ ]+ ]+ , DT.Node (Just 5) + [DT.Node Nothing []+ ]+ ]+ it "tree 4" $ do+ let test :: forall r. (r ~ ExTr4) + => DT.Tree (Either Int String)+ test = fromType (Proxy @r)+ test + `shouldBe` + DT.Node (Left 1) + [ DT.Node (Right "two") + [ DT.Node (Left 3) + [ DT.Node (Right "four") []+ ]+ ]+ , DT.Node (Left 5) + [DT.Node (Right "six") []+ ]+ ]++specShowTypeable :: Spec+specShowTypeable = describe "Show Type represented at the Kind level" $ do+ it "Show Int" $ do+ fromType @String (Proxy @Int)+ `shouldBe`+ "Int"+ it "Show Set of Types" $ do+ let test :: forall r. (r ~ Eval (FS.FromList '[Int, Maybe String, (), [Integer], IO ()])) + => DS.Set String+ test = fromType (Proxy @r)+ test + `shouldBe` + DS.fromList ["Int", "Maybe [Char]", "()", "[Integer]", "IO ()"]++specErrorMessage :: Spec+specErrorMessage = describe "show GHC.TypeLits.ErrorMessage" $ do+ it "text error" $ do+ (fromType @DTxt.Text $ Proxy @('TL.Text "I am error"))+ `shouldBe`+ DTxt.pack "I am error"+ it "ShowType 'True" $ do+ (fromType @DTxt.Text $ Proxy @('TL.ShowType '()))+ `shouldBe`+ DTxt.pack "'()"+ it "with Kinds" $ do+ (fromType @DTxt.Text $ Proxy @('TL.Text "Kind: " 'TL.:<>: 'TL.ShowType 'True 'TL.:$$: 'TL.Text "Type: " 'TL.:<>: 'TL.ShowType Bool))+ `shouldBe`+ DTxt.pack "Kind: 'True\nType: Bool"
+ test/Test/Data/Set.hs view
@@ -0,0 +1,221 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE DataKinds #-}+{-# OPTIONS_GHC -Wall #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++module Test.Data.Set where++import Data.Proxy+import Data.Type.Equality ((:~:)(Refl))+import Test.Hspec (describe, it, shouldBe, Spec)+import qualified Data.Set as DS++import Fcf (Eval, type (=<<), Map)+import Fcf.Data.Nat+import Fcf.Data.Set+import Fcf.Data.Reflect (fromType)+import Fcf.Alg.Sort++--------------------------------------------------------------------------------++-- > :kind! Eval (Size =<< FromList '[5, 3])+-- Eval (Size =<< FromList '[5, 3]) :: TL.Natural+-- = 2++spec :: Spec+spec = describe "Set" $ do+ it "PowerSet" $ do+ let test :: forall r. (r ~ Eval (PowerSet =<< FromList '[1,2,9,5])) => DS.Set (DS.Set Int)+ test = fromType (Proxy @r)+ test + `shouldBe` + DS.powerSet (DS.fromList [1,2,9,5])+ it "Size" $ do+ let test :: forall r. (r ~ Eval (Size =<< FromList '[5,3])) => Int+ test = fromType (Proxy @r)+ test `shouldBe` 2++--------------------------------------------------------------------------------++-- This module won't compile, if the Refl doesn't give the correct answer.+--+-- > :kind! (Eval Empty :: Set Nat)+-- (Eval Empty :: Set Nat) :: Set TL.Natural+-- = 'Set '[]+_ = Refl :: (Eval Empty :: Set Nat)+ :~: 'Set '[]+++-- This module won't compile, if the Refl doesn't give the correct answer.+--+-- > :kind! Eval (Singleton 1)+-- Eval (Singleton 1) :: Set TL.Natural+-- = 'Set '[1]+_ = Refl :: Eval (Singleton 1)+ :~: 'Set '[1]+++-- > :kind! Eval (Insert 3 =<< FromList '[1, 2])+-- Eval (Insert 3 =<< FromList '[1, 2]) :: Set TL.Natural+-- = 'Set '[3, 1, 2]+_ = Refl :: Eval (Insert 3 =<< FromList '[1, 2])+ :~: 'Set '[3, 1, 2]++-- > :kind! Eval (Insert 2 =<< FromList '[1, 2])+-- Eval (Insert 2 =<< FromList '[1, 2]) :: Set TL.Natural+-- = 'Set '[1, 2]+_ = Refl :: Eval (Insert 2 =<< FromList '[1, 2])+ :~: 'Set '[1, 2]++-- > :kind! Eval (Delete 5 =<< FromList '[5, 3])+-- Eval (Delete 5 =<< FromList '[5, 3]) :: Set TL.Natural+-- = 'Set '[3]+_ = Refl :: Eval (Delete 5 =<< FromList '[5, 3])+ :~: 'Set '[3]++-- > :kind! Eval (Delete 7 =<< FromList '[5, 3])+-- Eval (Delete 7 =<< FromList '[5, 3]) :: Set TL.Natural+-- = 'Set '[5, 3]+_ = Refl :: Eval (Delete 7 =<< FromList '[5, 3])+ :~: 'Set '[5, 3]++-- > :kind! Eval (Member 5 =<< FromList '[5, 3])+-- Eval (Member 5 =<< FromList '[5, 3]) :: Bool+-- = 'True+_ = Refl :: Eval (Member 5 =<< FromList '[5, 3])+ :~: 'True++-- > :kind! Eval (Member 7 =<< FromList '[5, 3])+-- Eval (Member 7 =<< FromList '[5, 3]) :: Bool+-- = 'False+_ = Refl :: Eval (Member 7 =<< FromList '[5, 3])+ :~: 'False++-- > :kind! Eval (NotMember 5 =<< FromList '[5, 3])+-- Eval (NotMember 5 =<< FromList '[5, 3]) :: Bool+-- = 'False+_ = Refl :: Eval (NotMember 5 =<< FromList '[5, 3])+ :~: 'False+++-- > :kind! Eval (NotMember 7 =<< FromList '[5, 3])+-- Eval (NotMember 7 =<< FromList '[5, 3]) :: Bool+-- = 'True+_ = Refl :: Eval (NotMember 7 =<< FromList '[5, 3])+ :~: 'True++-- > :kind! Eval (Null =<< FromList '[5, 3])+-- Eval (Null =<< FromList '[5, 3]) :: Bool+-- = 'False+_ = Refl :: Eval (Null =<< FromList '[5, 3])+ :~: 'False++-- > :kind! Eval (Null =<< Empty)+-- Eval (Null =<< Empty) :: Bool+-- = 'True+_ = Refl :: Eval (Null =<< Empty)+ :~: 'True++-- > :kind! Eval (IsSubsetOf ('Set '[]) ('Set '[0,1,2,3,4]))+-- Eval (IsSubsetOf ('Set '[]) ('Set '[0,1,2,3,4])) :: Bool+-- = 'True+_ = Refl :: Eval (IsSubsetOf ('Set '[]) ('Set '[0,1,2,3,4]))+ :~: 'True++-- > :kind! Eval (IsSubsetOf ('Set '[0,1]) ('Set '[0,1,2,3,4]))+-- Eval (IsSubsetOf ('Set '[0,1]) ('Set '[0,1,2,3,4])) :: Bool+-- = 'True+_ = Refl :: Eval (IsSubsetOf ('Set '[0,1]) ('Set '[0,1,2,3,4]))+ :~: 'True++-- > :kind! Eval (IsSubsetOf ('Set '[0,2,1,3,4]) ('Set '[0,1,2,3,4]))+-- Eval (IsSubsetOf ('Set '[0,2,1,3,4]) ('Set '[0,1,2,3,4])) :: Bool+-- = 'True+_ = Refl :: Eval (IsSubsetOf ('Set '[0,1,2,3,4]) ('Set '[0,1,2,3,4]))+ :~: 'True++-- > :kind! Eval (IsSubsetOf ('Set '[0,1,2,3,4,5]) ('Set '[0,1,2,3,4]))+-- Eval (IsSubsetOf ('Set '[0,1,2,3,4,5]) ('Set '[0,1,2,3,4])) :: Bool+-- = 'False+_ = Refl :: Eval (IsSubsetOf ('Set '[0,1,2,3,4,5]) ('Set '[0,1,2,3,4]))+ :~: 'False++-- > :kind! Eval (IsProperSubsetOf ('Set '[0,1,2,3,4]) ('Set '[0,1,2,3,4]))+-- Eval (IsProperSubsetOf ('Set '[0,1,2,3,4]) ('Set '[0,1,2,3,4])) :: Bool+-- = 'False+_ = Refl :: Eval (IsProperSubsetOf ('Set '[0,1,2,3,4]) ('Set '[0,1,2,3,4]))+ :~: 'False++-- > :kind! Eval (IsProperSubsetOf ('Set '[0,2,1,3]) ('Set '[0,1,2,3,4]))+-- Eval (IsProperSubsetOf ('Set '[0,2,1,3]) ('Set '[0,1,2,3,4])) :: Bool+-- = 'True+_ = Refl :: Eval (IsProperSubsetOf ('Set '[0,2,1,3]) ('Set '[0,1,2,3,4]))+ :~: 'True++-- > :kind! Eval (Union (Eval (FromList '[5, 3])) (Eval (FromList '[5, 7])) )+-- Eval (Union (Eval (FromList '[5, 3])) (Eval (FromList '[5, 7])) ) :: Set+-- TL.Natural+-- = 'Set '[7, 5, 3]+_ = Refl :: Eval (Union (Eval (FromList '[5, 3])) (Eval (FromList '[5, 7])) )+ :~: 'Set '[7, 5, 3]++-- > :kind! Eval (Difference (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7])))+-- Eval (Difference (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7]))) :: Set+-- TL.Natural+-- = 'Set '[3]+_ = Refl :: Eval (Difference (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7])))+ :~: 'Set '[3]++-- > :kind! Eval (Intersection (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7])))+-- Eval (Intersection (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7]))) :: Set+-- TL.Natural+-- = 'Set '[5]+_ = Refl :: Eval (Intersection (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7]))) + :~: 'Set '[5]++-- > :kind! Eval (PowerSet =<< FromList '["a", "b", "c"])+-- Eval (PowerSet =<< FromList '["a", "b", "c"]) :: Set+-- (Set TL.Symbol)+-- = 'Set+-- '[ 'Set '[], 'Set '["c"], 'Set '["b"], 'Set '["b", "c"],+-- 'Set '["a"], 'Set '["a", "b"], 'Set '["a", "c"],+-- 'Set '["a", "b", "c"]]+--+-- > :kind! Eval (PowerSet =<< FromList '[Int, Char, Maybe Int])+-- Eval (PowerSet =<< FromList '[Int, Char, Maybe Int]) :: Set+-- (Set (*))+-- = 'Set+-- '[ 'Set '[], 'Set '[Maybe Int], 'Set '[Char],+-- 'Set '[Char, Maybe Int], 'Set '[Int], 'Set '[Int, Char],+-- 'Set '[Int, Maybe Int], 'Set '[Int, Char, Maybe Int]]+_ = Refl :: Eval (PowerSet =<< FromList '[Int, Char, Maybe Int])+ :~: 'Set+ '[ 'Set '[], 'Set '[Maybe Int], 'Set '[Char],+ 'Set '[Char, Maybe Int], 'Set '[Int], 'Set '[Int, Char],+ 'Set '[Int, Maybe Int], 'Set '[Int, Char, Maybe Int]]++-- > :kind! Eval (FromList '[1, 2])+-- Eval (FromList '[1, 2]) :: Set TL.Natural+-- = 'Set '[1, 2]+_ = Refl :: Eval (FromList '[1, 2])+ :~: 'Set '[1, 2]++-- > :kind! Eval (ToList =<< PowerSet =<< FromList '[1,2,3])+-- Eval (ToList =<< PowerSet =<< FromList '[1,2,3]) :: [Set+-- TL.Natural]+-- = '[ 'Set '[], 'Set '[3], 'Set '[2], 'Set '[2, 3], 'Set '[1],+-- 'Set '[1, 2], 'Set '[1, 3], 'Set '[1, 2, 3]]+_ = Refl :: Eval (ToList =<< PowerSet =<< FromList '[1,2,3])+ :~: '[ 'Set '[], 'Set '[3], 'Set '[2], 'Set '[2, 3], 'Set '[1],+ 'Set '[1, 2], 'Set '[1, 3], 'Set '[1, 2, 3]]++-- > :kind! Eval (Qsort NatListOrd =<< Map ToList =<< ToList =<< PowerSet =<< FromList '[1,2,3])+-- Eval (Qsort NatListOrd =<< Map ToList =<< ToList =<< PowerSet =<< FromList '[1,2,3]) :: [[TL.Natural]]+-- = '[ '[], '[1], '[1, 2], '[1, 2, 3], '[1, 3], '[2], '[2, 3], '[3]]+_ = Refl :: Eval (Qsort NatListOrd =<< Map ToList =<< ToList =<< PowerSet =<< FromList '[1,2,3])+ :~: '[ '[], '[1], '[1, 2], '[1, 2, 3], '[1, 3], '[2], '[2, 3], '[3]]
test/doctest.hs view
@@ -1,6 +1,9 @@-import System.FilePath.Glob (glob)+{-# LANGUAGE CPP #-}+ import Test.DocTest +#if __GLASGOW_HASKELL__ >= 902+ exts :: [String] exts = [ "-XDataKinds"@@ -11,6 +14,11 @@ ] main :: IO ()-main = do- xs <- glob "src/**/*.hs"- doctest (exts ++ xs)+main = doctest $ exts ++ ["src"]++#else++main :: IO ()+main = pure ()++#endif
test/test.hs view
@@ -1,28 +1,33 @@ {-# LANGUAGE DataKinds, KindSignatures,+ TypeFamilies,+ UndecidableInstances, TypeOperators #-} -------------------------------------------------------------------------------- import Data.Type.Equality ((:~:)(Refl))-import GHC.TypeLits (Nat)-import Fcf+import GHC.TypeLits (Nat, Symbol)+import Fcf hiding (type (<*>)) -------------------------------------------------------------------------------- import Fcf.Data.Set+import Fcf.Control.Monad+import Fcf.Data.Tuple+import Fcf.Class.Monoid+import Fcf.Data.List -------------------------------------------------------------------------------- ---- Compile-time tests--_ = Refl :: Eval (ToList =<< PowerSet =<< FromList '[1,2])- :~: '[ 'Set '[], 'Set '[2], 'Set '[1], 'Set '[1,2]]---- Dummy+import Test.Alg as A (spec)+import Test.Data as D (spec)+import Test.Control as C (spec)+import Test.Hspec (hspec, parallel) main :: IO ()-main = pure ()-+main = hspec $ parallel $ do+ D.spec+ C.spec+ A.spec