fcf-containers 0.7.2 → 0.8.0

raw patch · 32 files changed

+3019/−314 lines, 32 filesdep +containersdep +textdep ~basePVP ok

version bump matches the API change (PVP)

Dependencies added: containers, text

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• CHANGELOG.md +25/−0
• TODO.md +13/−3
• default.nix +13/−2
• examples/Haiku.hs +15/−1
• examples/Orbits.hs +1/−1
• fcf-containers.cabal +20/−5
• src/Fcf/Alg/List.hs +13/−14
• src/Fcf/Alg/Morphism.hs +5/−7
• src/Fcf/Alg/Nat.hs +0/−2
• src/Fcf/Alg/Other.hs +2/−1
• src/Fcf/Alg/Sort.hs +3/−5
• src/Fcf/Alg/Symbol.hs +1/−3
• src/Fcf/Alg/Tree.hs +9/−9
• src/Fcf/Control/Monad.hs +52/−23
• src/Fcf/Data/Bitree.hs +2/−5
• src/Fcf/Data/Char.hs +200/−0
• src/Fcf/Data/List/Utils.hs +16/−9
• 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 +752/−0
• src/Fcf/Data/Reflect.hs +304/−0
• src/Fcf/Data/Set.hs +24/−23
• src/Fcf/Data/Symbol.hs +142/−0
• src/Fcf/Data/Text.hs +13/−9
• src/Fcf/Data/Text/Internal.hs +0/−2
• src/Fcf/Data/Tree.hs +4/−6
• src/Fcf/Data/Tuple.hs +42/−0
• test/Test/Data.hs +7/−0
• test/Test/Data/Reflect.hs +99/−0
• test/doctest.hs +12/−1
• test/test.hs +7/−1

@@ -1,4 +1,29 @@ +# 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

@@ -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:

@@ -3,6 +3,11 @@   # 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 = {@@ -22,9 +27,15 @@             (pkgs.fetchFromGitHub { # 0.8.0.1               owner  = "Lysxia";               repo   = "first-class-families";-              rev    = "d4780864ed9b11343b7b26050e39b2048a8e61f6";-              sha256 = "1iw0dryz66z4k9lsj1kayf17xs38i8bdk9aqi2qz49vcbhnfw8pd";+              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";

@@ -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 

@@ -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.

@@ -7,7 +7,7 @@     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.7.2+Version:             0.8.0 Build-type:          Simple Author:              gspia Maintainer:          iahogsp@gmail.com@@ -16,20 +16,26 @@ Category:            Other Copyright:           gspia (c) 2020- Extra-source-files:  README.md, TODO.md, CHANGELOG.md, default.nix, shell.nix-Tested-With:         GHC ==9.2.2 || ==9.0.2 || ==8.10.7+Tested-With:         GHC ==9.2.4 || ==9.0.2 || ==8.10.7   library   hs-source-dirs:    src   exposed-modules:   Fcf.Control.Monad-                   , Fcf.Data.MapC                    , 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@@ -37,10 +43,12 @@                    , 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                    , mtl+                   , text   ghc-options:      -Wall   default-language:  Haskell2010   -- ghc-options:@@ -65,6 +73,9 @@   build-depends:    base                   , first-class-families                   , fcf-containers+  ghc-options:+      -Wall+      -freduction-depth=0  Executable crabcombat   hs-source-dirs:   examples@@ -84,10 +95,14 @@   hs-source-dirs:      test   main-is:             test.hs   default-language:    Haskell2010+  other-modules:       Test.Data+                     , Test.Data.Reflect   build-depends:       base     , first-class-families     , fcf-containers+    , containers+    , text  test-suite fcf-doctest   type:                exitcode-stdio-1.0

@@ -1,5 +1,3 @@-{-# LANGUAGE DataKinds              #-}-{-# LANGUAGE PolyKinds              #-} {-# LANGUAGE TypeFamilies           #-} {-# LANGUAGE TypeInType             #-} {-# LANGUAGE TypeOperators          #-}@@ -68,7 +66,7 @@ -- === __Example__ -- -- >>> :kind! Eval (ListToFix '[1,2,3])--- Eval (ListToFix '[1,2,3]) :: Fix (ListF Nat)+-- 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@@ -79,7 +77,7 @@ -- === __Example__ -- -- >>> :kind! Eval (Cata LenAlg =<< ListToFix '[1,2,3])--- Eval (Cata LenAlg =<< ListToFix '[1,2,3]) :: Nat+-- Eval (Cata LenAlg =<< ListToFix '[1,2,3]) :: TL.Natural -- = 3 data LenAlg :: Algebra (ListF a) Nat type instance Eval (LenAlg 'NilF) = 0@@ -90,7 +88,7 @@ -- === __Example__ -- -- >>> :kind! Eval (Cata SumAlg =<< ListToFix '[1,2,3,4])--- Eval (Cata SumAlg =<< ListToFix '[1,2,3,4]) :: Nat+-- Eval (Cata SumAlg =<< ListToFix '[1,2,3,4]) :: TL.Natural -- = 10 data SumAlg :: Algebra (ListF Nat) Nat type instance Eval (SumAlg 'NilF) = 0@@ -101,7 +99,7 @@ -- === __Example__ -- -- >>> :kind! Eval (Cata ProdAlg =<< ListToFix '[1,2,3,4])--- Eval (Cata ProdAlg =<< ListToFix '[1,2,3,4]) :: Nat+-- Eval (Cata ProdAlg =<< ListToFix '[1,2,3,4]) :: TL.Natural -- = 24 data ProdAlg :: Algebra (ListF Nat) Nat type instance Eval (ProdAlg 'NilF) = 1@@ -114,7 +112,8 @@ -- === __Example__ -- -- >>> :kind! Eval (ListToParaFix '[1,2,3])--- Eval (ListToParaFix '[1,2,3]) :: Fix (ListF (Nat, [Nat]))+-- Eval (ListToParaFix '[1,2,3]) :: Fix+--                                    (ListF (TL.Natural, [TL.Natural])) -- = 'Fix --     ('ConsF --        '(1, '[2, 3])@@ -131,7 +130,7 @@ -- === __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]+-- 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) = '[]@@ -147,7 +146,7 @@ -- === __Example__ -- -- >>> :kind! Eval (Sliding 3 '[1,2,3,4,5,6])--- Eval (Sliding 3 '[1,2,3,4,5,6]) :: [[Nat]]+-- 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) =@@ -179,7 +178,7 @@ -- === __Example__ -- -- >>> :kind! Eval (Evens =<< RunInc 8)--- Eval (Evens =<< RunInc 8) :: [Nat]+-- 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)@@ -201,7 +200,7 @@ -- === __Example__ -- -- >>> :kind! Eval (RunInc 8)--- Eval (RunInc 8) :: [Nat]+-- 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)@@ -214,7 +213,7 @@ -- === __Example__ -- -- >>> :kind! Eval (Sum '[1,2,3])--- Eval (Sum '[1,2,3]) :: Nat+-- Eval (Sum '[1,2,3]) :: TL.Natural -- = 6 data Sum :: [Nat] -> Exp Nat type instance Eval (Sum ns) = Eval (Foldr (+) 0 ns)@@ -235,7 +234,7 @@ -- === __Example__ -- -- >>> :kind! Eval (MToN 1 3)--- Eval (MToN 1 3) :: [Nat]+-- 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)@@ -247,7 +246,7 @@ -- === __Example__ -- -- >>> :kind! Eval (ToList 1)--- Eval (ToList 1) :: [Nat]+-- Eval (ToList 1) :: [TL.Natural] -- = '[1] data ToList :: a -> Exp [a] type instance Eval (ToList a) = '[a]

@@ -1,5 +1,3 @@-{-# LANGUAGE DataKinds              #-}-{-# LANGUAGE PolyKinds              #-} {-# LANGUAGE TypeFamilies           #-} {-# LANGUAGE TypeInType             #-} {-# LANGUAGE TypeOperators          #-}@@ -44,7 +42,7 @@ --------------------------------------------------------------------------------  -- | 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@@ -79,7 +77,7 @@ -- :} -- -- >>> :kind! Eval (Ana NToOneCoA 3)--- Eval (Ana NToOneCoA 3) :: Fix (ListF Nat)+-- 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))))@@ -100,7 +98,7 @@ -- :} -- -- >>> :kind! Eval (Hylo SumAlg NToOneCoA 5)--- Eval (Hylo SumAlg NToOneCoA 5) :: Nat+-- 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)@@ -186,7 +184,7 @@ -- === __Example__ -- -- >>> :kind! Eval (First ((+) 1) '(3,"a"))--- Eval (First ((+) 1) '(3,"a")) :: (Nat, TL.Symbol)+-- Eval (First ((+) 1) '(3,"a")) :: (TL.Natural, TL.Symbol) -- = '(4, "a") data First :: (a -> Exp b) -> f a c -> Exp (f b c) @@ -202,7 +200,7 @@ -- === __Example__ -- -- >>> :kind! Eval (Second ((+) 1) '("a",3))--- Eval (Second ((+) 1) '("a",3)) :: (TL.Symbol, Nat)+-- Eval (Second ((+) 1) '("a",3)) :: (TL.Symbol, TL.Natural) -- = '("a", 4) data Second :: (c -> Exp d) -> f a c -> Exp (f a d) 

@@ -1,5 +1,3 @@-{-# LANGUAGE DataKinds              #-}-{-# LANGUAGE PolyKinds              #-} {-# LANGUAGE TypeFamilies           #-} {-# LANGUAGE TypeInType             #-} {-# LANGUAGE TypeOperators          #-}

@@ -30,6 +30,7 @@  -- $setup -- >>> import           GHC.Types+-- >>> import qualified GHC.TypeLits as TL  -------------------------------------------------------------------------------- @@ -39,7 +40,7 @@ -- -- >>> :kind! Eval (PairMaybeToMaybePair '( 'Just "txt", 'Just 1)) -- Eval (PairMaybeToMaybePair '( 'Just "txt", 'Just 1)) :: Maybe---                                                           (Symbol, Nat)+--                                                           (Symbol, TL.Natural) -- = 'Just '("txt", 1) data PairMaybeToMaybePair :: (Maybe a, Maybe b) -> Exp (Maybe (a,b)) type instance Eval (PairMaybeToMaybePair '( 'Nothing, _)) = 'Nothing

@@ -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)  -------------------------------------------------------------------------------- @@ -69,7 +67,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@@ -109,7 +107,7 @@ -- __Example__ -- -- >>> :kind! Eval (Qsort (N.<) '[5,3,1,9,4,6,3])--- Eval (Qsort (N.<) '[5,3,1,9,4,6,3]) :: [Nat]+-- 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" ])

@@ -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)

@@ -1,5 +1,3 @@-{-# LANGUAGE DataKinds              #-}-{-# LANGUAGE PolyKinds              #-} {-# LANGUAGE TypeFamilies           #-} {-# LANGUAGE TypeInType             #-} {-# LANGUAGE TypeOperators          #-}@@ -60,14 +58,14 @@ -- 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.@@ -86,7 +84,7 @@ -- :} -- -- >>> :kind! Eval (Size =<< UnfoldTree BuildNode 1)--- Eval (Size =<< UnfoldTree BuildNode 1) :: Nat+-- Eval (Size =<< UnfoldTree BuildNode 1) :: TL.Natural -- = 7 data Size :: Tree a -> Exp Nat type instance Eval (Size tr) = Eval (Cata CountNodesAlg =<< TreeToFix tr)@@ -117,7 +115,7 @@ -- __Example__ -- -- >>> :kind! Eval (FibHylo 10)--- Eval (FibHylo 10) :: Nat+-- 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)+-- Eval (Sizes =<< Ana BuildNodeCoA 1) :: Fix+--                                          (AnnF (TreeF TL.Natural) TL.Natural) -- = 'Fix --     ('AnnF --        '( 'NodeF@@ -203,13 +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+-- Eval (FibHisto 100) :: TL.Natural -- = 354224848179261915075 data FibHisto :: Nat -> Exp Nat type instance Eval (FibHisto n) = Eval (Histo FibAlgebra =<< NatToFix n)

@@ -1,5 +1,3 @@-{-# LANGUAGE DataKinds              #-}-{-# LANGUAGE PolyKinds              #-} {-# LANGUAGE RankNTypes             #-} {-# LANGUAGE TypeFamilies           #-} {-# LANGUAGE TypeInType             #-}@@ -27,9 +25,17 @@ import           Control.Monad.Identity import           GHC.TypeNats as TN -import           Fcf as Fcf hiding (type (<*>))+import           Fcf hiding (type (<*>))  --------------------------------------------------------------------------------++-- 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))@@ -69,14 +75,14 @@ -- === __Example__ -- -- >>> :kind! Eval ('Identity Plus2 <*> 'Identity 5)--- Eval ('Identity Plus2 <*> 'Identity 5) :: Identity Nat+-- 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]) :: [Nat]+-- 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] '[]) :: [Nat]+-- Eval ( (<*>) '[ (Fcf.+) 1, (Fcf.*) 10] '[]) :: [Natural] -- = '[] -- >>> :kind! Eval ( (<*>) '[] '[4,5,6,7]) -- Eval ( (<*>) '[] '[4,5,6,7]) :: [b]@@ -95,8 +101,7 @@ -- | 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))+type instance Eval (Star_ f (a ': as)) = Eval (f a) ': Eval (Star_ f as)   -- Example@@ -121,7 +126,7 @@ -- === __Example__ -- -- >>> :kind! Eval (LiftA2 (Fcf.+) '[1,2] '[3,4])--- Eval (LiftA2 (Fcf.+) '[1,2] '[3,4]) :: [Nat]+-- Eval (LiftA2 (Fcf.+) '[1,2] '[3,4]) :: [Natural] -- = '[4, 5, 5, 6] -- --@@ -149,7 +154,7 @@ data LiftA2_ :: (a -> b -> Exp c) -> a -> f b -> Exp (f c) type instance Eval (LiftA2_ f a '[]) = '[] type instance Eval (LiftA2_ f a (b ': bs)) =-    Eval (f a b) ': (Eval (LiftA2_ f a bs))+    Eval (f a b) ': Eval (LiftA2_ f a bs)   --------------------------------------------------------------------------------@@ -173,12 +178,12 @@ -- the same time. -- -- >>> :kind! Eval ('[5,6,7] >>= Plus2M)--- Eval ('[5,6,7] >>= Plus2M) :: [Nat]+-- 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]) :: [Nat]+-- 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) @@ -241,10 +246,10 @@ -- -- -- >>> :kind! Eval ( 'Just 1 >> 'Just 2)--- Eval ( 'Just 1 >> 'Just 2) :: Maybe Nat+-- Eval ( 'Just 1 >> 'Just 2) :: Maybe Natural -- = 'Just 2 -- >>> :kind! Eval ( 'Nothing >> 'Just 2)--- Eval ( 'Nothing >> 'Just 2) :: Maybe Nat+-- Eval ( 'Nothing >> 'Just 2) :: Maybe Natural -- = 'Nothing -- --@@ -290,6 +295,30 @@   --------------------------------------------------------------------------------+-- 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)++-- | 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++-------------------------------------------------------------------------------- -- Traversable  @@ -298,7 +327,7 @@ -- === __Example__ -- -- >>> :kind! Eval (Traverse Id '[ '[1,2], '[3,4]])--- Eval (Traverse Id '[ '[1,2], '[3,4]]) :: [[Nat]]+-- Eval (Traverse Id '[ '[1,2], '[3,4]]) :: [[Natural]] -- = '[ '[1, 3], '[1, 4], '[2, 3], '[2, 4]] -- --@@ -309,13 +338,13 @@  -- [] type instance Eval (Traverse f lst) =-    Eval (Foldr (Cons_f f) (Eval (Return '[])) lst)+    Eval (Foldr (ConsHelper f) (Eval (Return '[])) lst)  -- | Helper for [] traverse-data Cons_f :: (a -> Exp (f b)) -> a -> f [b] -> Exp (f [b])-type instance Eval (Cons_f f x ys) = Eval (LiftA2 (Pure2 '(:)) (Eval (f x)) ys)+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)+-- type instance Eval (ConsHelper f x ys) = Eval (LiftA2 Cons (Eval (f x)) ys)   -- Maybe@@ -337,19 +366,19 @@ -- === __Example__ -- -- >>> :kind! Eval (Sequence ('Just ('Right 5)))--- Eval (Sequence ('Just ('Right 5))) :: Either a (Maybe Nat)+-- 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 [Nat]+-- 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 [Nat]+-- Eval (Sequence '[ 'Just 3, 'Nothing, 'Just 7]) :: Maybe [Natural] -- = 'Nothing -- -- >>> :kind! Eval (Sequence '[ '[1,2], '[3,4]])--- Eval (Sequence '[ '[1,2], '[3,4]]) :: [[Nat]]+-- Eval (Sequence '[ '[1,2], '[3,4]]) :: [[Natural]] -- = '[ '[1, 3], '[1, 4], '[2, 3], '[2, 4]] -- --

@@ -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

@@ -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++--------------------------------------------------------------------------------+

@@ -1,8 +1,5 @@-{-# LANGUAGE DataKinds              #-}-{-# LANGUAGE PolyKinds              #-} {-# LANGUAGE TypeFamilies           #-} {-# LANGUAGE TypeInType             #-}-{-# LANGUAGE TypeOperators          #-} {-# LANGUAGE UndecidableInstances   #-} {-# OPTIONS_GHC -Wall                       #-} {-# OPTIONS_GHC -Werror=incomplete-patterns #-}@@ -16,17 +13,16 @@  = Fcf.Data.List.Utils -The following would probably have better place at the first-class-families-library.  That is, polish and make a PR.+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 as Fcf+import           Fcf import           Fcf.Data.List as Fcf  --------------------------------------------------------------------------------@@ -44,9 +40,20 @@ -- === __Example__ -- -- >>> :kind! Eval (Foldl (Fcf.-) 10 '[3,2,1])--- Eval (Foldl (Fcf.-) 10 '[3,2,1]) :: Nat+-- 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] 

@@ -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)- 

@@ -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)- 

@@ -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++--------------------------------------------------------------------------------

@@ -0,0 +1,752 @@+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE TypeInType             #-}+{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE UndecidableInstances   #-}+{-# OPTIONS_GHC -Wall                       #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{-|+Module      : Fcf.Data.Text+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+    ( 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))

@@ -0,0 +1,304 @@+{-# LANGUAGE CPP                    #-}+{-# LANGUAGE FlexibleContexts       #-}+{-# LANGUAGE FlexibleInstances      #-}+{-# LANGUAGE MultiParamTypeClasses  #-}+{-# LANGUAGE ScopedTypeVariables    #-}+{-# LANGUAGE TypeApplications       #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE TypeInType             #-}+{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE UndecidableInstances   #-}+{-# 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.Proxy+import qualified Data.Map.Strict as MS+import qualified Data.IntMap.Strict as IMS+import qualified Data.Set as S+#if __GLASGOW_HASKELL__ >= 902+import qualified Data.Text as Txt+#endif+import qualified Data.Tree as T++-- import qualified Fcf.Core as C (Eval)+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++--------------------------------------------------------------------------------++-- For the doctests:++-- $setup+-- >>> import qualified GHC.TypeLits as TL+-- >>> import           Fcf.Data.Nat++--------------------------------------------------------------------------------+++-- | 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]++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 typeval val where+    fromType :: Proxy typeval -> val++instance KnownNat n => KnownVal (n :: Nat) Integer where+    fromType _ = TL.natVal (Proxy @n)++instance KnownNat n => KnownVal (n :: Nat) Int where+    fromType _ = fromInteger $ TL.natVal (Proxy @n)++instance KnownSymbol s => KnownVal (s :: Symbol) String where+    fromType _ = TL.symbolVal (Proxy @s)++--------------------------------------------------------------------------------++-- List instances++instance KnownVal ('[] :: [Nat]) [Integer] where+    fromType _ = []++instance (KnownNat n, KnownVal ns [Integer]) => KnownVal (n : ns :: [Nat]) [Integer] where+    fromType _ = TL.natVal (Proxy @n) : fromType (Proxy @ns)+++instance KnownVal ('[] :: [Nat]) [Int] where+    fromType _ = []++instance (KnownNat n, KnownVal ns [Int]) => KnownVal (n : ns :: [Nat]) [Int] where+    fromType _ = fromInteger (TL.natVal (Proxy @n)) : fromType (Proxy @ns)+++instance KnownVal ('[] :: [Symbol]) [String] where+    fromType _ = []++instance (KnownSymbol sym, KnownVal syms [String])+    => KnownVal (sym : syms :: [Symbol]) [String]+  where+    fromType _ = TL.symbolVal (Proxy @sym) : fromType (Proxy @syms)+++instance KnownVal ('[] :: [(Nat,Nat)]) [(Int,Int)] where+    fromType _ = []+-- This helps with NatMap instances++instance (KnownNat n, KnownNat m, KnownVal nms [(Int,Int)])+    => KnownVal ( '(n,m) : nms :: [(Nat,Nat)]) [(Int,Int)]+  where+    fromType _ =+        (fromInteger (TL.natVal (Proxy @n)), fromInteger (TL.natVal (Proxy @m)))+        : fromType (Proxy @nms)+-- This helps with NatMap instances++instance KnownVal ('[] :: [(Nat,Symbol)]) [(Int,String)] where+    fromType _ = []+-- This helps with NatMap instances++instance (KnownNat n, KnownSymbol m, KnownVal nms [(Int,String)])+    => KnownVal ( '(n,m) : nms :: [(Nat,Symbol)]) [(Int,String)]+  where+    fromType _ =+        (fromInteger (TL.natVal (Proxy @n)), TL.symbolVal (Proxy @m))+        : fromType (Proxy @nms)+-- This helps with NatMap instances++--------------------------------------------------------------------------------++-- Trees++-- instances for Forests, that is, lists of Trees.+instance KnownVal '[] [T.Tree Int] where fromType _ = []++-- instances for Forests+instance (KnownVal t (T.Tree Int), KnownVal trees [T.Tree Int])+    => KnownVal (t : trees) [T.Tree Int]+  where+    fromType _ = fromType @t Proxy : fromType @trees Proxy++-- instance for Trees (using forest definition).+instance (KnownNat n, KnownVal trees [T.Tree Int])+    => KnownVal ('FT.Node (n :: Nat) trees) (T.Tree Int)+  where+    fromType _ = T.Node (fromType @n Proxy) (fromType @trees Proxy)+++instance KnownVal '[] [T.Tree Integer] where fromType _ = []++instance (KnownVal t (T.Tree Integer), KnownVal trees [T.Tree Integer])+    => KnownVal (t : trees) [T.Tree Integer]+  where+    fromType _ = fromType @t Proxy : fromType @trees Proxy++instance (KnownNat n, KnownVal trees [T.Tree Integer])+    => KnownVal ('FT.Node (n :: Nat) trees) (T.Tree Integer)+  where+    fromType _ = T.Node (fromType @n Proxy) (fromType @trees Proxy)+++instance KnownVal '[] [T.Tree String] where fromType _ = []++instance (KnownVal t (T.Tree String), KnownVal trees [T.Tree String])+    => KnownVal (t : trees) [T.Tree String]+  where+    fromType _ = fromType @t Proxy : fromType @trees Proxy++instance (KnownSymbol n, KnownVal trees [T.Tree String])+    => KnownVal ('FT.Node (n :: Symbol) trees) (T.Tree String)+  where+    fromType _ = T.Node (fromType @n Proxy) (fromType @trees Proxy)+++--------------------------------------------------------------------------------++-- NatMaps / IntMaps++instance (KnownVal (pairs :: [(Nat,Nat)]) [(Int,Int)])+    => KnownVal ('NM.NatMap pairs) (IMS.IntMap Int)+  where+    fromType _ = IMS.fromList (fromType @pairs Proxy)++instance (KnownVal (pairs :: [(Nat,Integer)]) [(Int,Integer)])+    => KnownVal ('NM.NatMap pairs) (IMS.IntMap Integer)+  where+    fromType _ = IMS.fromList (fromType @pairs Proxy)++instance (KnownVal (pairs :: [(Nat,Symbol)]) [(Int,String)])+    => KnownVal ('NM.NatMap pairs) (IMS.IntMap String)+  where+    fromType _ = IMS.fromList (fromType @pairs Proxy)+++--------------------------------------------------------------------------------++-- Maps++instance (KnownVal (pairs :: [(Nat,Nat)]) [(Int,Int)])+    => KnownVal ('MC.MapC pairs) (MS.Map Int Int)+  where+    fromType _ = MS.fromList (fromType @pairs Proxy)++instance (KnownVal (pairs :: [(Nat,Integer)]) [(Int,Integer)])+    => KnownVal ('MC.MapC pairs) (MS.Map Int Integer)+  where+    fromType _ = MS.fromList (fromType @pairs Proxy)++instance (KnownVal (pairs :: [(Nat,Symbol)]) [(Int,String)])+    => KnownVal ('MC.MapC pairs) (MS.Map Int String)+  where+    fromType _ = MS.fromList (fromType @pairs Proxy)+++instance (KnownVal (pairs :: [(Symbol,Nat)]) [(String,Int)])+    => KnownVal ('MC.MapC pairs) (MS.Map String Int)+  where+    fromType _ = MS.fromList (fromType @pairs Proxy)++instance (KnownVal (pairs :: [(Symbol,Integer)]) [(String,Integer)])+    => KnownVal ('MC.MapC pairs) (MS.Map String Integer)+  where+    fromType _ = MS.fromList (fromType @pairs Proxy)++instance (KnownVal (pairs :: [(Symbol,Symbol)]) [(String,String)])+    => KnownVal ('MC.MapC pairs) (MS.Map String String)+  where+    fromType _ = MS.fromList (fromType @pairs Proxy)+++--------------------------------------------------------------------------------++-- Set+ +instance (KnownVal (mems :: [Nat]) [Int]) => KnownVal ('FS.Set mems) (S.Set Int)+  where+    fromType _ = S.fromList (fromType @mems Proxy)++instance (KnownVal (mems :: [Nat]) [Integer]) => KnownVal ('FS.Set mems) (S.Set Integer)+  where+    fromType _ = S.fromList (fromType @mems Proxy)++instance (KnownVal (mems :: [Symbol]) [String]) => KnownVal ('FS.Set mems) (S.Set String)+  where+    fromType _ = S.fromList (fromType @mems Proxy)+++--------------------------------------------------------------------------------++#if __GLASGOW_HASKELL__ >= 902++-- Text++-- instance (KnownVal (sym :: Symbol) String) => KnownVal ('FTxt.Text sym) Txt.Text+--   where+--     fromType _ = Txt.pack $ fromType @sym Proxy+++-- | Text instance.+--+-- === __Example__+--+-- >>> :{+-- afun :: forall r. (r ~ 'FTxt.Text "hmm") => Txt.Text+-- afun = fromType @r Proxy+-- :}+--+-- >>> afun+-- "hmm"+instance KnownSymbol sym => KnownVal ('FTxt.Text sym) Txt.Text+  where+    fromType _ = Txt.pack $ fromType @sym Proxy++++#else++#endif++

@@ -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)@@ -86,7 +84,7 @@ --------------------------------------------------------------------------------  -- | Set-definition.-data Set a = Set [a]+newtype Set a = Set [a]   --------------------------------------------------------------------------------@@ -96,7 +94,7 @@ -- === __Example__ -- -- >>> :kind! (Eval Empty :: Set Nat)--- (Eval Empty :: Set Nat) :: Set Nat+-- (Eval Empty :: Set Nat) :: Set TL.Natural -- = 'Set '[] -- -- See also the other examples in this module.@@ -108,7 +106,7 @@ -- === __Example__ -- -- >>> :kind! Eval (Singleton 1)--- Eval (Singleton 1) :: Set Nat+-- Eval (Singleton 1) :: Set TL.Natural -- = 'Set '[1] data Singleton :: v -> Exp (Set v) type instance Eval (Singleton v) = 'Set '[v]@@ -119,11 +117,11 @@ -- === __Example__ -- -- >>> :kind! Eval (Insert 3 =<< FromList '[1, 2])--- Eval (Insert 3 =<< FromList '[1, 2]) :: Set Nat+-- 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+-- 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)) =@@ -136,11 +134,11 @@ -- === __Example__ -- -- >>> :kind! Eval (Delete 5 =<< FromList '[5, 3])--- Eval (Delete 5 =<< FromList '[5, 3]) :: Set Nat+-- 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+-- 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)) =@@ -194,7 +192,7 @@ -- === __Example__ -- -- >>> :kind! Eval (Size =<< FromList '[5, 3])--- Eval (Size =<< FromList '[5, 3]) :: Nat+-- Eval (Size =<< FromList '[5, 3]) :: TL.Natural -- = 2 data Size :: Set v -> Exp TL.Nat type instance Eval (Size ('Set lst)) = Eval (Length lst)@@ -247,8 +245,8 @@ -- === __Example__ -- -- >>> :kind! Eval (Union (Eval (FromList '[5, 3])) (Eval (FromList '[5, 7])) )--- Eval (Union (Eval (FromList '[5, 3])) (Eval (FromList '[5, 7])) ) :: Set ---                                                                        Nat+-- 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)) =@@ -266,8 +264,8 @@ -- === __Example__ -- -- >>> :kind! Eval (Difference (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7])))--- Eval (Difference (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7]))) :: Set ---                                                                            Nat+-- 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 +279,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+-- 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)) =@@ -336,14 +334,16 @@ -- === __Example__ -- -- >>> :kind! Eval (PowerSet =<< FromList '["a", "b", "c"])--- Eval (PowerSet =<< FromList '["a", "b", "c"]) :: Set (Set Symbol)+-- 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 *)+-- 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],@@ -362,7 +362,7 @@ -- === __Example__ -- -- >>> :kind! Eval (FromList '[1, 2])--- Eval (FromList '[1, 2]) :: Set Nat+-- Eval (FromList '[1, 2]) :: Set TL.Natural -- = 'Set '[1, 2] data FromList :: [v] -> Exp (Set v) type instance Eval (FromList lst) = 'Set lst@@ -372,12 +372,13 @@ -- === __Example__ -- -- >>> :kind! Eval (ToList =<< PowerSet =<< FromList '[1,2,3])--- Eval (ToList =<< PowerSet =<< FromList '[1,2,3]) :: [Set Nat]+-- 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]]+-- 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

@@ -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++--------------------------------------------------------------------------------

@@ -1,5 +1,3 @@-{-# LANGUAGE DataKinds              #-}-{-# LANGUAGE PolyKinds              #-} {-# LANGUAGE TypeFamilies           #-} {-# LANGUAGE TypeInType             #-} {-# LANGUAGE TypeOperators          #-}@@ -16,9 +14,15 @@  = 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.+ -}  --------------------------------------------------------------------------------@@ -88,6 +92,7 @@     )   where +import           GHC.TypeLits (Symbol) import qualified GHC.TypeLits as TL  import           Fcf ( If, Eval, Exp, type (=<<), type (@@)@@ -97,7 +102,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.Class.Functor as F ( FMap ) @@ -121,7 +125,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  -------------------------------------------------------------------------------- @@ -223,7 +227,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))@@ -638,7 +642,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) '[])  @@ -666,7 +670,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) '[])  

@@ -1,7 +1,5 @@-{-# LANGUAGE DataKinds              #-} {-# LANGUAGE FlexibleInstances      #-} {-# LANGUAGE MultiParamTypeClasses  #-}-{-# LANGUAGE PolyKinds              #-} {-# LANGUAGE TypeFamilies           #-} {-# LANGUAGE TypeInType             #-} {-# LANGUAGE TypeOperators          #-}

@@ -1,5 +1,3 @@-{-# LANGUAGE DataKinds              #-}-{-# LANGUAGE PolyKinds              #-} {-# LANGUAGE TypeFamilies           #-} {-# LANGUAGE TypeInType             #-} {-# LANGUAGE TypeOperators          #-}@@ -34,7 +32,7 @@  module Fcf.Data.Tree where -import           Fcf as Fcf+import           Fcf import           Fcf.Data.List as Fcf  import           Fcf.Control.Monad as M@@ -122,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 '[]],@@ -141,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)@@ -173,7 +171,7 @@ -- === __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])

@@ -0,0 +1,42 @@+{-# 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)

@@ -0,0 +1,7 @@++module Test.Data where++import           Test.Data.Reflect as R (tests)++tests = R.tests+

@@ -0,0 +1,99 @@+{-# LANGUAGE CPP                    #-}+{-# LANGUAGE ScopedTypeVariables    #-}+{-# LANGUAGE TypeApplications       #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE TypeInType             #-}+{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE UndecidableInstances   #-}+{-# 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+#if __GLASGOW_HASKELL__ >= 902+import qualified Data.Text as DTxt+#endif+import           Data.Proxy++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++tests :: Bool+tests = +     testNatMap+  && testMap+  && testSet+#if __GLASGOW_HASKELL__ >= 902+  && testText+#endif+  && testTree++testNatMap +  :: forall r. (r ~ Eval (FNM.Insert 3 "hih" =<< FNM.FromList '[ '(1,"haa"), '(2,"hoo")])) +  => Bool+testNatMap = result == expected+  where+    result   = fromType @r Proxy :: IM.IntMap String+    expected = IM.fromList [ (3, "hih"), (1, "haa"), (2, "hoo")]++testMap +  :: forall r. (r ~ Eval (FNMC.Insert 3 "hih" =<< FNMC.FromList '[ '(1,"haa"), '(2,"hoo")])) +  => Bool+testMap = result == expected+  where+    result   = fromType @r Proxy :: DM.Map Int String+    expected = DM.fromList [ (3, "hih"), (1, "haa"), (2, "hoo")]++testSet+  :: forall r. (r ~ Eval (FS.FromList '[5, 9, 1, 8, 3, 5]))+  => Bool+testSet = result == expected+  where+    result   = fromType @r Proxy :: DS.Set Int+    expected = DS.fromList [1, 3, 5, 8, 9]+  ++type ExT1r =+    'FT.Node 1 +       '[ 'FT.Node 2 +          '[ 'FT.Node 3 '[ 'FT.Node 4 '[]]]+        , 'FT.Node 5 '[ 'FT.Node 6 '[]]+        ]++-- type ExTr2 =+--     'Node ('Just 1)+--         '[ 'Node ('Just 2)+--             '[ 'Node ('Just 3)+--                 '[ 'Node ('Just 4) '[]]+--              ]+--          , 'Node ('Just 5)+--             '[ 'Node ('Just 6) '[]+--              ]+--          ]+++testTree :: forall r. (r ~ ExT1r) => Bool+testTree = result == expected+  where+    result   = fromType @r Proxy :: DT.Tree Int+    expected = DT.Node 1 [DT.Node 2 [DT.Node 3 [DT.Node 4 []]], DT.Node 5 [DT.Node 6 []]]+    +    +#if __GLASGOW_HASKELL__ >= 902+testText :: forall r. (r ~ 'FTxt.Text "trial") => Bool+testText = result == expected+  where+    result   = fromType @r Proxy :: DTxt.Text+    expected = DTxt.pack "trial"+#endif

@@ -1,5 +1,9 @@+{-# LANGUAGE CPP                    #-}+ import Test.DocTest +#if __GLASGOW_HASKELL__ >= 902+ exts :: [String] exts =   [ "-XDataKinds"@@ -10,4 +14,11 @@   ]  main :: IO ()-main = doctest $ exts ++ ["-isrc"]+main = doctest $ exts ++ ["src"]++#else++main :: IO ()+main = pure ()++#endif

@@ -15,7 +15,10 @@  -------------------------------------------------------------------------------- +import           Test.Data (tests) ++ -- Compile-time tests  _ = Refl :: Eval (ToList =<< PowerSet  =<< FromList '[1,2])@@ -24,5 +27,8 @@ -- Dummy  main :: IO ()-main = pure ()+main = +  if tests +    then pure ()+    else error "Tests not ok."