fcf-containers 0.5.0 → 0.6.0

raw patch · 15 files changed

+1148/−338 lines, 15 filesdep ~basedep ~first-class-familiesnew-component:exe:crabcombatPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base, first-class-families

API changes (from Hackage documentation)

Files

• CHANGELOG.md +10/−0
• default.nix +7/−0
• examples/Crabcombat.hs +157/−0
• examples/Haiku.hs +18/−18
• examples/Orbits.hs +7/−7
• fcf-containers.cabal +32/−21
• src/Fcf/Alg/List.hs +27/−8
• src/Fcf/Alg/Morphism.hs +19/−19
• src/Fcf/Alg/Nat.hs +58/−0
• src/Fcf/Alg/Other.hs +61/−0
• src/Fcf/Alg/Symbol.hs +25/−25
• src/Fcf/Data/Bitree.hs +141/−0
• src/Fcf/Data/Text.hs +271/−235
• src/Fcf/Data/Text/Internal.hs +310/−0
• src/Fcf/Data/Tree.hs +5/−5

@@ -1,3 +1,13 @@+# 0.6.0++ - use symbol as text representation (we can split predefined char-sets, as shown+   by the Csongor at https://kcsongor.github.io/symbol-parsing-haskell/ see also+   the symbols-package)+ - and hie.yaml (for language server)+ - minor documentation fixes+ - add new example that really stresses ghc (Advent-of-code 2020, day 22b)+ - MToN to Alg.List (this generates Nat-list from M to N)+ - Nat equality and inequality test  # 0.5.0 

@@ -22,6 +22,12 @@               rev    = "4a0bf3ea9c125bb4009b61ce70b1a5339b7b2072";               sha256 = "14387mpfvds226iynkpay3aaqamvxznxjsmg2qcwdxafdvxmyq9z";             }) {};+            # something for the next version?+            #  rev    = "9fe4ce36cf1cd4b0f5af59c923c15b9085c48cd6";+            #  sha256 = "1677ylhhf1mwwfs6j2p6gbn2f6mzsx4zmaihz8v9v07h845wz8l7";+            # 0.8.0+            # rev    = "4a0bf3ea9c125bb4009b61ce70b1a5339b7b2072";+            # sha256 = "14387mpfvds226iynkpay3aaqamvxznxjsmg2qcwdxafdvxmyq9z";             # (pkgs.fetchFromGitHub { # 0.7             #   owner  = "Lysxia";             #   repo   = "first-class-families";@@ -41,6 +47,7 @@   adjust-for-ghc = drv: {     executableSystemDepends = [       hpkgs.ghcid+      hpkgs.ghcide       hpkgs.cabal-install     ];     buildDepends = [

@@ -0,0 +1,157 @@+{-# LANGUAGE DataKinds              #-}+{-# LANGUAGE PolyKinds              #-}+{-# LANGUAGE ScopedTypeVariables    #-}+{-# LANGUAGE TypeApplications       #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE TypeInType             #-}+{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE UndecidableInstances   #-}+{-# OPTIONS_GHC -Wall                       #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{-|++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+[aoc 20 d22](https://adventofcode.com/2020/day/22). We use the described+example input data in a bit different form. See the link for the+original data and answer.++We implement the following algorithm on type-level:++>>> playGame2h :: [([Int],[Int])] -> ([Int],[Int]) -> ([Int],Player)+>>> playGame2h _ (p1,[]) = (p1,P1)+>>> playGame2h _ ([],p2) = (p2,P2)+>>> playGame2h hist hs@(v1:r1,v2:r2) =+>>>    if elem hs hist+>>>    then (r1 ++ [v1,v2], P1)+>>>    else+>>>      if length r1 >= v1 && length r2 >= v2+>>>      then+>>>          case playGame2h [] (take v1 r1, take v2 r2) of+>>>            (_,P1) -> playGame2h (hs : hist) (r1 ++ [v1,v2], r2)+>>>            (_,P2) -> playGame2h (hs : hist) (r1, r2 ++ [v2,v1])+>>>      else+>>>         if v1 > v2+>>>         then playGame2h (hs : hist) (r1 ++ [v1,v2], r2)+>>>         else playGame2h (hs : hist) (r1, r2 ++ [v2,v1])+>>>+>>> day22h :: [String] -> Int+>>> day22h strs =+>>>     let (p,_) = playGame2h [] hnds -- 62 min if using <> and 7 s if ++ for list cat+>>>         len = length p+>>>         is =  [1..len]+>>>      in foldl (+) 0 $ zipWith (*) is $ reverse $ p+>>>   where+>>>     hnds = input2handsf strs++-}++--------------------------------------------------------------------------------++import           GHC.TypeLits (natVal)++import           Data.Proxy++import           Fcf (Eval, If, Exp, TyEq, Pure, type (&&), type (<=<), type (=<<)+                     , Uncurry, Bimap, Fst)+import           Fcf.Alg.List (MToN)+import           Fcf.Data.Nat as N+import           Fcf.Data.List (Take, type (++), Elem, Length, Foldr, ZipWith, Reverse)+++--------------------------------------------------------------------------------++-- | Example input for which the answer is 291.+type ExampleInput = '( '[9, 2, 6, 3, 1], '[5, 8, 4, 7, 10]) -- :: ([Nat],[Nat])++data Player = P1 | P2++-- :kind! Eval (PlayGame '[] ExampleInput)+data PlayGame :: [([Nat],[Nat])] -> ([Nat],[Nat]) -> Exp ([Nat],Player)+type instance Eval (PlayGame _ '( p1 ': ps , '[])) = '( p1 ': ps, 'P1)+type instance Eval (PlayGame _ '( '[], p2 ': ps)) = '( p2 ': ps , 'P2)+type instance Eval (PlayGame hist '( v1 ': r1, v2 ': r2)) = Eval+    (If (Eval (Elem '(v1 ': r1, v2 ': r2) hist ))+        (Pure '( Eval (r1 ++ '[v1,v2]), 'P1)  )+        (If ( Eval (Eval (v1 <= Eval (Length r1)) && Eval (v2 <= Eval (Length r2)) ))+            (If (Eval ( TyEq (Eval (PlayGame '[] '( Eval (Take v1 r1), Eval (Take v2 r2)) ) ) 'P1))+                (PlayGame ('( v1 ': r1, v2 ': r2) ': hist) '(Eval (r1 ++ '[v1,v2]), r2))+                (PlayGame ('( v1 ': r1, v2 ': r2) ': hist) '(r1, Eval (r2 ++ '[v2,v1])))+            )+            (If (Eval (v1 > v2))+                (PlayGame ('( v1 ': r1, v2 ': r2) ': hist) '(Eval (r1 ++ '[v1,v2]), r2))+                (PlayGame ('( v1 ': r1, v2 ': r2) ': hist) '(r1, Eval (r2 ++ '[v2,v1])))+            )+        )+    )++-- | Helper.+data AsPair :: a -> Exp (a,a)+type instance Eval (AsPair a) = '(a,a)+++-- | Calculating the result from the winners hand.+--+-- :kind! Eval (Day22 ExampleInput)+data Day22 :: ([Nat],[Nat]) -> Exp Nat+type instance Eval (Day22 input) = Eval+    (+    Foldr (N.+) 0+    =<< Uncurry (ZipWith (N.*))+    =<< Bimap ((MToN 1) <=< Length) Reverse+    =<< AsPair+    =<< Fst+    =<< PlayGame '[] input+    )++-- | The actual larger input. The term-level implementation time consumption+-- is very sensitive to the compiler being able to optimize it.  (E.g. use tail+-- recursion?). Interesting to see, how ghc is doing this on type-level.+--+-- Does not compile on my machine (not even with the -freduction-depth=0 at cabal),+-- not enough memory+-- Ghci also gets 'Killed'.+type Input =+    '( '[21, 50,  9, 45, 16, 47, 27, 38, 29, 48, 10, 42, 32, 31, 41, 11,  8, 33, 25, 30, 12, 40,  7, 23, 46]+     , '[22, 20, 44,  2, 26, 17, 34, 37, 43,  5, 15, 18, 36, 19, 24, 35,  3, 13, 14,  1,  6, 39, 49,  4, 28]+     ) -- :: ([Nat], [Nat])++-- On my machine, the compilation takes about 3 minutes+type Input2 =+    '( '[21, 50,  9, 45, 16, 47, 27, 38, 29, 48, 10,    7, 23, 46]+     , '[22, 20, 44,  2, 26, 17, 34, 37, 43,  5, 15,   49,  4, 28]+     ) -- :: ([Nat], [Nat])++-- On my machine, does not compilate, not enough memory.+type Input3 =+    '( '[21, 50,  9, 45, 16, 47, 27, 38, 29, 48, 10,   12, 40,  7, 23, 46]+     , '[22, 20, 44,  2, 26, 17, 34, 37, 43,  5, 15,    6, 39, 49,  4, 28]+     ) -- :: ([Nat], [Nat])++-- On my machine, does not compilate, not enough memory.+type Input4 =+    '( '[21, 50,  9, 45, 16, 47, 27, 38, 29, 48, 10,   40,  7, 23, 46]+     , '[22, 20, 44,  2, 26, 17, 34, 37, 43,  5, 15,   39, 49,  4, 28]+     ) -- :: ([Nat], [Nat])+++++--------------------------------------------------------------------------------++-- | Bring the result to term-level.+showExampleInputResult :: forall result. (result ~ Eval (Day22 ExampleInput)) => String+showExampleInputResult = show $ natVal @result Proxy++-- showResult :: forall result. (result ~ Eval (Day22 Input2)) => String+-- showResult :: forall result. (result ~ Eval (Day22 Input3)) => String+-- showResult :: forall result. (result ~ Eval (Day22 Input4)) => String+-- showResult = show $ natVal @result Proxy++main :: IO ()+main = putStrLn $ "The result is:\n" ++ showExampleInputResult+-- main = putStrLn $ "The result is:\n" ++ showResult+

@@ -45,15 +45,15 @@ -- | Type-level variable containing vocabulary split in syllables. data HaikuWords :: Exp [[Text]] type instance Eval HaikuWords =-    '[ '[ 'Text '["a","a"], 'Text '["m","u"]]-     , '[ 'Text '["a","a"], 'Text '["m","u","l"], 'Text '["l","a"]]-     , '[ 'Text '["a"], 'Text '["j","a"], 'Text '["t","u","s"]]-     , '[ 'Text '["j","o"], 'Text '["k","i","n"]]-     , '[ 'Text '["k","i","e"], 'Text '["l","i"]]-     , '[ 'Text '["l","o","i"], 'Text '["k","o","i"], 'Text '["l","e"], 'Text '["v","a"]]-     , '[ 'Text '["m","u","u"]]-     , '[ 'Text '["v","a","n"], 'Text '["h","e"], 'Text '["n","e","e"]]-     , '[ 'Text '["u","u"], 'Text '["s","i"]]+    '[ '[ 'Text "aa", 'Text "mu"]+     , '[ 'Text "aa", 'Text "mul", 'Text "la" ]+     , '[ 'Text "a", 'Text "ja", 'Text "tus"]+     , '[ 'Text "jo", 'Text "kin"]+     , '[ 'Text "kie", 'Text "li"]+     , '[ 'Text "loi", 'Text "koi", 'Text "le", 'Text "va"]+     , '[ 'Text "muu"]+     , '[ 'Text "van", 'Text "he", 'Text "nee"]+     , '[ 'Text "uu", 'Text "si"]      ]  -- | Turn syllables into words@@ -75,7 +75,7 @@  -------------------------------------------------------------------------------- --- | The count of syllables per lines and number of lines that is required for +-- | The count of syllables per lines and number of lines that is required for -- correct Haiku. This is used for Haiku structural check. data ReqSyllablesPerLine :: Exp [Nat] type instance Eval ReqSyllablesPerLine = '[5,7,5]@@ -85,12 +85,12 @@ -- | Our executable associated Haiku we want to check. data Haiku :: Exp Text type instance Eval Haiku =-    'Text '[ "k","i","e","l","i"," ","v","a","n","h","e","n","e","e","\n"-           , "l","o","i","k","o","i","l","e","v","a"," ","a","j","a","t","u","s","\n"-           , "a","a","m","u","l","l","a"," ","u","u","s","i"-           -- , "j","o", "k","i","n" -- test with clearly wrong input (won't compile)-           ]+    'Text "kieli vanhenee\nloikoileva ajatus\naamulla uusi"+    -- 'Text "kieli vanhenee\nloikoileva ajatus\naamulla uusi jokin"+    -- -- test with clearly wrong input (won't compile) ++ -- | Split the Haiku into more easily processable form data HaikuAsLineWords :: Exp [[Text]] type instance Eval HaikuAsLineWords = Eval (Fcf.Map Words =<< Lines =<< Haiku)@@ -104,8 +104,8 @@         (SumJusts ns (Eval (acc + (Eval (FromMaybe 0 n) ))))     ) --- | The main method, we list of lines, and on each line a list of words,--- for which we try to find out the syllable count from our map, +-- | The main method, we list lines, and on each line a list of words,+-- for which we try to find out the syllable count from our map, -- and as a last thing we count the syllable sums for each line. data HaikuSyllCountsPerLine :: Exp [Nat] type instance Eval HaikuSyllCountsPerLine =@@ -113,7 +113,7 @@       =<< Fcf.Map (Fcf.Map (Flip M.Lookup (Eval WSmap)))       =<< HaikuAsLineWords) --- | To check the Haiku, compare the correct number of syllables (and at the+-- | To check the Haiku, compare the correct number of syllables (and at the -- same time, number of lines) to the figures we got from the input Haiku. data CheckHaiku :: Exp Bool type instance Eval CheckHaiku =

@@ -58,13 +58,13 @@ data EqPlanet :: TL.Symbol -> TL.Symbol -> Exp Bool type instance Eval (EqPlanet a b) = Eval (TyEq 'EQ (TL.CmpSymbol a b)) --- | :kind! Eval (FindDescs "COM" =<< OrbitInput)+-- | :kind! Eval (FindDescs "COM" =<< OrbitInput) data FindDescs :: TL.Symbol -> [(TL.Symbol, TL.Symbol)] -> Exp [TL.Symbol] type instance Eval (FindDescs p lst) =      Eval (Map Snd =<< (Filter (EqPlanet p <=< Fst) lst))  -- | This is not used in the final solution but worked as a step towards it.--- +-- -- :kind! Eval (Ana BuildOrbTreeCoA "COM") data BuildOrbTreeCoA :: CoAlgebra (TreeF TL.Symbol) TL.Symbol type instance Eval (BuildOrbTreeCoA nd) =@@ -72,7 +72,7 @@         ('NodeF nd '[])         ('NodeF nd (Eval (FindDescs nd =<< OrbitInput))) --- | +-- | -- We need to store the depth of the node along the tree. We use the depth when -- counting paths from root to every node. --@@ -93,16 +93,16 @@   -- | Count paths from root to every node.--- +-- -- If it is a leaf, the number of paths from root to it is the depth.--- If it is an internal node, the number of paths to the subtree rooted +-- If it is an internal node, the number of paths to the subtree rooted -- by it is sum of pathnums of subtrees plus the depth (paths to this one). data CountPathsAlg :: Algebra (TreeF (Nat,TL.Symbol)) Nat type instance Eval (CountPathsAlg ('NodeF '(d,_) '[])) = d type instance Eval (CountPathsAlg ('NodeF '(d,_) (b ': bs))) = d TL.+ (Eval (Sum (b ': bs)))  --- | We initialize this with the known starting node and the depth of it, which +-- | We initialize this with the known starting node and the depth of it, which -- is 0. -- -- :kind! Eval OrbitSolution@@ -111,7 +111,7 @@     Eval (Hylo CountPathsAlg BuildOrbTreeCoA2 '(0,"COM"))  -- | Helper to bring in the result of the type-level computation.--- +-- -- It is a nice exercise to solve this using Tree, UnfoldTree and FoldTree. showResult :: forall n. (n ~ Eval OrbitSolution) => String showResult = show $ TL.natVal @n Proxy

@@ -6,7 +6,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.5.0+Version:             0.6.0 Build-type:          Simple Author:              gspia Maintainer:          iahogsp@gmail.com@@ -16,21 +16,26 @@ Copyright:           gspia (c) 2020- Extra-source-files:  README.md, TODO.md, CHANGELOG.md, default.nix, shell.nix Cabal-version:       1.24-Tested-With:         GHC ==8.8.1 || ==8.6.5 || ==8.4.4 || ==8.2.2+Tested-With:         GHC ==8.10.3 || ==8.8.4 || ==8.6.5 || ==8.4.4 + library   hs-source-dirs:    src   exposed-modules:   Fcf.Data.MapC+                   , Fcf.Data.Bitree                    , Fcf.Data.NatMap-                   , Fcf.Data.Tree                    , Fcf.Data.Set                    , Fcf.Data.Text+                   , Fcf.Data.Text.Internal+                   , Fcf.Data.Tree                    , Fcf.Alg.List+                   , Fcf.Alg.Morphism+                   , Fcf.Alg.Nat+                   , Fcf.Alg.Other                    , Fcf.Alg.Sort                    , Fcf.Alg.Symbol                    , Fcf.Alg.Tree-                   , Fcf.Alg.Morphism-  build-depends:     base >= 4.9 && < 4.14+  build-depends:     base >= 4.9 && < 4.18                    , first-class-families >= 0.8 && < 0.9   ghc-options:      -Wall   default-language:  Haskell2010@@ -39,33 +44,37 @@   Executable orbits-  hs-source-dirs:   examples,src+  hs-source-dirs:   examples   main-is:          Orbits.hs   default-language: Haskell2010-  other-modules:    Fcf.Alg.Morphism-                  , Fcf.Alg.List-                  , Fcf.Alg.Tree-                  , Fcf.Data.Tree   build-depends:    base                   , first-class-families+                  , fcf-containers   -- ghc-options:      --  -ddump-simpl      --  -O2  Executable haiku-  hs-source-dirs:   examples,src+  hs-source-dirs:   examples   main-is:          Haiku.hs   default-language: Haskell2010-  other-modules:    Fcf.Alg.Morphism-                  , Fcf.Alg.List-                  , Fcf.Alg.Symbol-                  , Fcf.Data.Tree-                  , Fcf.Data.MapC-                  , Fcf.Data.Set-                  , Fcf.Data.Text   build-depends:    base                   , first-class-families+                  , fcf-containers +Executable crabcombat+  hs-source-dirs:   examples+  main-is:          Crabcombat.hs+  default-language: Haskell2010+  build-depends:    base+                  , first-class-families+                  , fcf-containers+  ghc-options:+      -freduction-depth=0+     --  -ddump-simpl+     --  -O2++ test-suite fcf-test   type:                exitcode-stdio-1.0   hs-source-dirs:      test@@ -83,9 +92,11 @@   default-language:    Haskell2010   if impl(ghc >= 8.6)     build-depends:-      base,-      doctest,-      Glob+      base+      , first-class-families+      , fcf-containers+      , doctest+      , Glob   else     buildable: False 

@@ -60,7 +60,7 @@ -- | ListToFix can be used to turn a norma type-level list into the base -- functor type ListF, to be used with e.g. Cata. For examples in use, see -- 'LenAlg' and 'SumAlg'.--- +-- -- Ideally, we would have one ToFix type-level function for which we could -- give type instances for different type-level types, like lists, trees -- etc. See TODO.md.@@ -75,7 +75,7 @@ type instance Eval (ListToFix (a ': as)) = 'Fix ('ConsF a (Eval (ListToFix as)))  -- | Example algebra to calculate list length.--- +-- -- === __Example__ -- -- >>> :kind! Eval (Cata LenAlg =<< ListToFix '[1,2,3])@@ -86,7 +86,7 @@ type instance Eval (LenAlg ('ConsF a b)) = 1 TL.+ b  -- | Example algebra to calculate the sum of Nats in a list.--- +-- -- === __Example__ -- -- >>> :kind! Eval (Cata SumAlg =<< ListToFix '[1,2,3,4])@@ -110,7 +110,7 @@ --------------------------------------------------------------------------------  -- | Form a Fix-structure that can be used with Para.--- +-- -- === __Example__ -- -- >>> :kind! Eval (ListToParaFix '[1,2,3])@@ -125,7 +125,7 @@     'Fix ('ConsF '(a,as) (Eval (ListToParaFix as)))  -- | Example from recursion-package by Vanessa McHale.--- +-- -- This removes duplicates from a list (by keeping the right-most one). -- -- === __Example__@@ -221,11 +221,31 @@  -------------------------------------------------------------------------------- +-- | Helper to form Nat lists like [1..5] or [3..10]+--+-- :kind! Eval (Unfoldr ToThree 1)+data MToNHelp :: Nat -> Nat -> Exp (Maybe (Nat, Nat))+type instance Eval (MToNHelp n b) =+    If (Eval (b >= (n TL.+1)))+        'Nothing+        ('Just '(b, b TL.+ 1)) +-- | Function to form Nat lists like [1..5] or [3..10]+--+-- === __Example__+--+-- >>> :kind! Eval (MToN 1 3)+-- Eval (MToN 1 3) :: [Nat]+-- = '[1, 2, 3]+data MToN :: Nat -> Nat -> Exp [Nat]+type instance Eval (MToN m n) = Eval (Unfoldr (MToNHelp n) m)+++ -- | ToList for type-level lists. -- -- === __Example__--- +-- -- >>> :kind! Eval (ToList 1) -- Eval (ToList 1) :: [Nat] -- = '[1]@@ -236,7 +256,7 @@ -- | Equal tests for list equality. We may change the name to (==). -- -- === __Example__--- +-- -- >>> :kind! Eval (Equal '[1,2,3] '[1,2,3]) -- Eval (Equal '[1,2,3] '[1,2,3]) :: Bool -- = 'True@@ -246,5 +266,4 @@ -- = 'False data Equal :: [a] -> [a] -> Exp Bool type instance Eval (Equal as bs) = Eval (And =<< ZipWith TyEq as bs)- 

@@ -60,7 +60,7 @@  -- | Write the function to give a 'Fix', and feed it in together with an -- 'Algebra'.--- +-- -- Check Fcf.Alg.List to see example algebras in use. There we have e.g. -- ListToFix-function. data Cata :: Algebra f a -> Fix f -> Exp a@@ -69,15 +69,15 @@ -- | Ana can also be used to build a 'Fix' structure. -- -- === __Example__--- +-- -- >>> data NToOneCoA :: CoAlgebra (ListF Nat) Nat--- >>> :{ ---   type instance Eval (NToOneCoA b) = +-- >>> :{+--   type instance Eval (NToOneCoA b) = --     If (Eval (b < 1) ) --         'NilF --         ('ConsF b ( b TL.- 1)) -- :}--- +-- -- >>> :kind! Eval (Ana NToOneCoA 3) -- Eval (Ana NToOneCoA 3) :: Fix (ListF Nat) -- = 'Fix ('ConsF 3 ('Fix ('ConsF 2 ('Fix ('ConsF 1 ('Fix 'NilF))))))@@ -85,20 +85,20 @@ type instance Eval (Ana coalg a) = 'Fix (Eval (Map (Ana coalg) (Eval (coalg a))))  --- | +-- | -- Hylomorphism uses first 'Ana' to build a structure (unfold) and then 'Cata' -- to process the structure (fold).--- +-- -- === __Example__--- +-- -- >>> data NToOneCoA :: CoAlgebra (ListF Nat) Nat--- >>> :{ ---   type instance Eval (NToOneCoA b) = +-- >>> :{+--   type instance Eval (NToOneCoA b) = --     If (Eval (b < 1) ) --         'NilF --         ('ConsF b ( b TL.- 1)) -- :}--- +-- -- >>> :kind! Eval (Hylo SumAlg NToOneCoA 5) -- Eval (Hylo SumAlg NToOneCoA 5) :: Nat -- = 15@@ -147,7 +147,7 @@ -- | Synthesized attributes are created in a bottom-up traversal -- using a catamorphism -- (from Recursion Schemes by example, Tim Williams).--- +-- -- This is the algebra that is fed to the cata. data SynthAlg :: (f a -> Exp a) -> f (Ann f a) -> Exp (Ann f a) type instance Eval (SynthAlg alg faf) =@@ -156,7 +156,7 @@ -- | Synthesized attributes are created in a bottom-up traversal -- using a catamorphism -- (from Recursion Schemes by example, Tim Williams).--- +-- -- For the example, see "Fcf.Data.Alg.Tree.Sizes". data Synthesize :: (f a -> Exp a) -> Fix f -> Exp (Ann f a) type instance Eval (Synthesize f fx) = Eval (Cata (SynthAlg f) fx)@@ -165,7 +165,7 @@  -- | Histo takes annotation algebra and takes a Fix-structure -- (from Recursion Schemes by example, Tim Williams).--- +-- -- This is a helper for 'Histo' as it is implemented with 'Cata'. data HistoAlg :: (f (Ann f a) -> Exp a) -> f (Ann f a) -> Exp (Ann f a) type instance Eval (HistoAlg alg faf) =@@ -173,7 +173,7 @@  -- | Histo takes annotation algebra and takes a Fix-structure -- (from Recursion Schemes by example, Tim Williams).--- +-- -- Examples can be found from "Fcf.Data.Alg.Tree" and "Fcf.Data.Alg.List" -- modules. data Histo :: (f (Ann f a) -> Exp a) -> Fix f -> Exp a@@ -182,9 +182,9 @@ --------------------------------------------------------------------------------  -- | Type-level First. Tuples @(,)@ and @Either@ have First-instances.--- +-- -- === __Example__--- +-- -- >>> :kind! Eval (First ((+) 1) '(3,"a")) -- Eval (First ((+) 1) '(3,"a")) :: (Nat, TL.Symbol) -- = '(4, "a")@@ -198,9 +198,9 @@ type instance Eval (First f ('Right b)) = 'Right b  -- | Type-level Second. Tuples @(,)@ and @Either@ have Second-instances.--- +-- -- === __Example__--- +-- -- >>> :kind! Eval (Second ((+) 1) '("a",3)) -- Eval (Second ((+) 1) '("a",3)) :: (TL.Symbol, Nat) -- = '("a", 4)

@@ -0,0 +1,58 @@+{-# LANGUAGE DataKinds              #-}+{-# LANGUAGE PolyKinds              #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE TypeInType             #-}+{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE UndecidableInstances   #-}+{-# OPTIONS_GHC -Wall                       #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{-|+Module      : Fcf.Alg.Nat+Description : Nat helpers+Copyright   : (c) gspia 2020-+License     : BSD+Maintainer  : gspia++= Fcf.Data.Nat+++-}+++--------------------------------------------------------------------------------++module Fcf.Alg.Nat where++import qualified GHC.TypeNats as TN+import           Fcf.Core (Eval, Exp)+import           Fcf.Data.Bool+import           Fcf.Data.Nat (Nat)+import qualified Fcf.Data.Nat as FN++--------------------------------------------------------------------------------++-- | Nat equality.+--+-- >>> :kind! Eval (2 == 2)+-- Eval (2 == 2) :: Bool+-- = 'True+--+-- >>> :kind! Eval (2 == 3)+-- Eval (2 == 3) :: Bool+-- = 'False+data (==) :: Nat -> Nat -> Exp Bool+type instance Eval ((==) a b) = Eval ((a TN.<=? b) && (b TN.<=? a))+++-- | Nat in-equality.+--+-- >>> :kind! Eval (2 /= 2)+-- Eval (2 /= 2) :: Bool+-- = 'False+--+-- >>> :kind! Eval (2 /= 3)+-- Eval (2 /= 3) :: Bool+-- = 'True+data (/=) :: Nat -> Nat -> Exp Bool+type instance Eval ((/=) a b) = Eval (Eval (a FN.< b) || Eval (b FN.< a))

@@ -0,0 +1,61 @@+{-# LANGUAGE DataKinds              #-}+{-# LANGUAGE PolyKinds              #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE TypeInType             #-}+{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE UndecidableInstances   #-}+{-# OPTIONS_GHC -Wall                       #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{-|+Module      : Fcf.Alg.Other+Description : Utility collection (waiting for new place)+Copyright   : (c) gspia 2020-+License     : BSD+Maintainer  : gspia++= Fcf.Alg.Other++To be moved to some other place++-}+++--------------------------------------------------------------------------------++module Fcf.Alg.Other where++import           Fcf as Fcf++--------------------------------------------------------------------------------++-- For the doctests:++-- $setup++--------------------------------------------------------------------------------++-- | Helper.+--+-- === __Evample__+--+-- >>> :kind! Eval (PairMaybeToMaybePair '( 'Just "txt", 'Just 1))+-- Eval (PairMaybeToMaybePair '( 'Just "txt", 'Just 1)) :: Maybe+--                                                           (GHC.Types.Symbol, GHC.Types.Nat)+-- = 'Just '("txt", 1)+data PairMaybeToMaybePair :: (Maybe a, Maybe b) -> Exp (Maybe (a,b))+type instance Eval (PairMaybeToMaybePair '( 'Nothing, _)) = 'Nothing+type instance Eval (PairMaybeToMaybePair '( _, 'Nothing)) = 'Nothing+type instance Eval (PairMaybeToMaybePair '( 'Just a, 'Just b)) = 'Just '(a,b)+++-- | Id function.+--+-- === __Evample__+--+-- >>> :kind! Eval (Id "id")+-- Eval (Id "id") :: GHC.Types.Symbol+-- = "id"+data Id :: a -> Exp a+type instance Eval (Id a) = a+

@@ -55,8 +55,8 @@   where  ---------------------------------------------------------------------------------        -import           GHC.TypeLits (Symbol)++-- import           GHC.TypeLits (Symbol) import qualified GHC.TypeLits as TL  import           Fcf.Core (Eval, Exp)@@ -72,7 +72,7 @@ -- | Append two type-level symbols. -- -- === __Example__--- +-- -- >>> :kind! Eval (Append "hmm" " ok") -- Eval (Append "hmm" " ok") :: Symbol -- = "hmm ok"@@ -81,9 +81,9 @@   -- | Intercalate type-level symbols.--- +-- -- === __Example__--- +-- -- >>> :kind! Eval (Intercalate "+" '["aa", "bb", "cc"]) -- Eval (Intercalate "+" '["aa", "bb", "cc"]) :: Symbol -- = "aa+bb+cc"@@ -108,7 +108,7 @@ -- | IsSpace -- -- === __Example__--- +-- -- >>> :kind! Eval (IsSpace "a") -- Eval (IsSpace "a") :: Bool -- = 'False@@ -123,7 +123,7 @@ -- | IsNewline -- -- === __Example__--- +-- -- >>> :kind! Eval (IsNewLine "a") -- Eval (IsNewLine "a") :: Bool -- = 'False@@ -138,7 +138,7 @@ -- | IsTab -- -- === __Example__--- +-- -- >>> :kind! Eval (IsTab "a") -- Eval (IsTab "a") :: Bool -- = 'False@@ -150,10 +150,10 @@ type instance Eval (IsTab s) = Eval (s == "\t")  --- | IsSpaceDelim+-- | IsSpaceDelim -- -- === __Example__--- +-- -- >>> :kind! Eval (IsSpaceDelim "a") -- Eval (IsSpaceDelim "a") :: Bool -- = 'False@@ -166,10 +166,10 @@     Eval (Eval (IsSpace s) || (Eval (Eval (IsNewLine s) || Eval (IsTab s))))  --- | IsDigit+-- | IsDigit -- -- === __Example__--- +-- -- >>> :kind! Eval (IsDigit "3") -- Eval (IsDigit "3") :: Bool -- = 'True@@ -186,11 +186,11 @@ --------------------------------------------------------------------------------  --- | SymbolOrd - compare two symbols and give type-level Ordering --- ( $ 'LT $, $ 'EQ $ or $ 'GT $ ).+-- | SymbolOrd - compare two symbols and give type-level Ordering+-- ( $ 'LT $, $ 'EQ $ or $ 'GT $ ). -- -- === __Example__--- +-- -- >>> :kind! Eval (SymbolOrd "a" "b") -- Eval (SymbolOrd "a" "b") :: Ordering -- = 'LT@@ -198,9 +198,9 @@ type instance Eval (SymbolOrd a b) = TL.CmpSymbol a b  -- | Less-than-or-equal comparison for symbols.--- +-- -- === __Example__--- +-- -- >>> :kind! Eval ("b" <= "a") -- Eval ("b" <= "a") :: Bool -- = 'False@@ -210,9 +210,9 @@     Eval (Eval (TyEq (TL.CmpSymbol a b) 'LT) || Eval (TyEq (TL.CmpSymbol a b) 'EQ))  -- | Larger-than-or-equal comparison for symbols.--- +-- -- === __Example__--- +-- -- >>> :kind! Eval ("b" >= "a") -- Eval ("b" >= "a") :: Bool -- = 'True@@ -221,9 +221,9 @@     Eval (Eval (TyEq (TL.CmpSymbol a b) 'GT) || Eval (TyEq (TL.CmpSymbol a b) 'EQ))  -- | Less-than comparison for symbols.--- +-- -- === __Example__--- +-- -- >>> :kind! Eval ("a" < "b") -- Eval ("a" < "b") :: Bool -- = 'True@@ -231,9 +231,9 @@ type instance Eval ((<) a b) = Eval (TyEq (TL.CmpSymbol a b) 'LT)  -- | Larger-than comparison for symbols.--- +-- -- === __Example__--- +-- -- >>> :kind! Eval ("b" > "a") -- Eval ("b" > "a") :: Bool -- = 'True@@ -241,9 +241,9 @@ type instance Eval ((>) a b) = Eval (TyEq (TL.CmpSymbol a b) 'GT)  -- | Equality of symbols--- +-- -- === __Example__--- +-- -- >>> :kind! Eval ("b" == "a") -- Eval ("b" == "a") :: Bool -- = 'False

@@ -0,0 +1,141 @@+{-# LANGUAGE DataKinds              #-}+{-# LANGUAGE PolyKinds              #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE TypeInType             #-}+{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE UndecidableInstances   #-}+{-# OPTIONS_GHC -Wall                       #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{-|+Module      : Fcf.Data.Bitree+Description : Binary tree data-structure for type-level programming+Copyright   : (c) gspia 2020-+License     : BSD+Maintainer  : gspia++= Fcf.Data.Bitree++Binary trees++-}+++--------------------------------------------------------------------------------++module Fcf.Data.Bitree where++import qualified GHC.TypeLits as TL+import           Fcf as Fcf+-- import           Fcf.Data.List as Fcf+import           Fcf.Data.Nat as N++--------------------------------------------------------------------------------++-- For the doctests:++-- $setup+-- >>> import qualified GHC.TypeLits as TL+-- >>> import           Fcf.Data.Nat++--------------------------------------------------------------------------------++-- | Binary tree type.+data Tree a = Leaf a | Node (Tree a) a (Tree a)+    deriving Show++-- type Forest a = (Tree a, Tree a)+-- type Forest a = [Tree a]++-- | Fold a type-level 'Tree'.+data FoldTree :: (a -> [b] -> Exp b) -> Tree a -> Exp b+type instance Eval (FoldTree f ('Leaf a)) = Eval (f a '[])+type instance Eval (FoldTree f ('Node tr1 a tr2)) =+    Eval (f a (Eval (Map (FoldTree f) '[ tr1, tr2])))+++data CountSizeHelp :: Nat -> [Nat] -> Exp Nat+type instance Eval (CountSizeHelp tr '[]) = 1+-- type instance Eval (CountSizeHelp tr '[n]) = 1+type instance Eval (CountSizeHelp tr '[n1,n2]) = 1 TL.+ (n1 TL.+ n2)++type ExampleTree1 = 'Leaf 1+type ExampleTree2 = 'Node ('Leaf 2) 1 ('Leaf 3)+type ExampleTree3 = 'Node ('Node ('Leaf 4) 2 ('Leaf 5) ) 1 ('Node ('Leaf 6) 3 ('Leaf 7))+type ExampleTree4 = 'Node ('Node ('Leaf 4) 2 ('Leaf 5) ) 1 ('Leaf 3)+++{-++-- | Unfold for a 'Tree'.+--+-- === __Example__+--+-- > >> data BuildNode :: Nat -> Exp (Nat,[Nat])+-- > >> :{+--   type instance Eval (BuildNode x) =+--       If (Eval ((2 TL.* x TL.+ 1) >= 8))+--           '(x, '[])+--           '(x, '[2 TL.* x, (2 TL.* x) TL.+ 1 ])+-- :}+--+-- > >> :kind! Eval (UnfoldTree BuildNode 1)+-- Eval (UnfoldTree BuildNode 1) :: Tree Nat+-- = 'Node+--     1+--     '[ 'Node 2 '[ 'Node 4 '[], 'Node 5 '[]],+--        'Node 3 '[ 'Node 6 '[], 'Node 7 '[]]]+data UnfoldTree :: (b -> Exp (a, [b])) -> b -> Exp (Tree a)+type instance Eval (UnfoldTree f b) =+    'Node (Eval (Fst Fcf.=<< f b)) (Eval (UnfoldForest f (Eval (Snd =<< f b))))++-- | Unfold for a 'Forest'.+data UnfoldForest :: (b -> Exp (a, [b])) -> [b] -> Exp (Forest a)+type instance Eval (UnfoldForest f bs) = Eval (Map (UnfoldTree f) bs)+-}++-- | Flatten a 'Tree'.+--+-- === __Example__+--+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)))++-- | Get the root node from a 'Tree'.+data GetRoot :: Tree a -> Exp a+type instance Eval (GetRoot ('Leaf a )) = a+type instance Eval (GetRoot ('Node _ a _)) = a+++-- | Get the root nodes from a list of 'Tree's.+data GetRoots :: [Tree a] -> Exp [a]+type instance Eval (GetRoots trs) = Eval (Map GetRoot trs)++{-+-- | Get the forest from a 'Tree'.+-- data GetForest :: Tree a -> Exp [Tree a]+-- type instance Eval (GetForest ('Node _ f)) = f+-- | Get the forests from a list of 'Tree's.+data GetForests :: [Tree a] -> Exp [Tree a]+type instance Eval (GetForests ts) = Eval (ConcatMap GetForest ts)++-- helper for the Levels-function+data SubFLevels :: [Tree a] -> Exp (Maybe ([a], [Tree a]))+type instance Eval (SubFLevels '[]) = 'Nothing+type instance Eval (SubFLevels (t ': ts)) =+    'Just '( Eval (GetRoots (t ': ts)), Eval (GetForests (t ': ts)))++-- | Get the levels from a 'Tree'.+--+-- === __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]]+-- = '[ '[1], '[2, 5], '[3, 6], '[4]]+data Levels :: Tree a -> Exp [[a]]+type instance Eval (Levels tr) = Eval (Unfoldr SubFLevels '[tr])+++-}

@@ -89,12 +89,12 @@ import qualified GHC.TypeLits as TL  import           Fcf ( If, Eval, Exp, type (=<<), type (@@)-                     , Flip, Pure )+                     , Flip, Pure) import qualified Fcf.Class.Foldable as F (All, Any) import           Fcf.Data.List ( type (++) ) import qualified Fcf.Data.List as F-    ( Length, Head, Tail, Init, Reverse, Take, Drop, TakeWhile, DropWhile-    , Foldr, Intercalate, Intersperse, IsPrefixOf, IsSuffixOf, IsInfixOf, Snoc)+    ( Length, Init, Reverse, Take, Drop, TakeWhile, DropWhile+    , Intercalate, Intersperse, IsPrefixOf, IsSuffixOf, IsInfixOf, Snoc) import           Fcf.Data.Symbol (Symbol) -- import qualified Fcf.Data.Symbol as FS @@ -102,8 +102,11 @@   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 (==))  -------------------------------------------------------------------------------- @@ -117,155 +120,176 @@  -- | 'Text' is a data structure, that is, a list to hold type-level symbols of -- length one.-data Text = Text [Symbol]+data Text = Text Symbol  --------------------------------------------------------------------------------  -- | Empty--- +-- -- === __Example__--- +-- -- >>> :kind! (Eval Empty :: Text) -- (Eval Empty :: Text) :: Text--- = 'Text '[]+-- = 'Text "" -- -- See also the other examples in this module. data Empty :: Exp Text-type instance Eval Empty = 'Text '[]+type instance Eval Empty = 'Text "" --- | Singleton--- +-- | Singleton+-- -- === __Example__--- +-- -- >>> :kind! Eval (Singleton "a") -- Eval (Singleton "a") :: Text--- = 'Text '["a"]+-- = 'Text "a" data Singleton :: Symbol -> Exp Text-type instance Eval (Singleton s) = 'Text '[s]+type instance Eval (Singleton s) = 'Text s   --- | Use FromList to construct a Text from type-level list.+-- | Use FromList to construct a Text from type-level list. -- -- === __Example__--- --- :kind! Eval (FromList '["h", "e", "l", "l", "u", "r", "e", "i"])--- Eval (FromList '["h", "e", "l", "l", "u", "r", "e", "i"]) :: Text--- = 'Text '["h", "e", "l", "l", "u", "r", "e", "i"]-data FromList :: [Symbol] -> Exp Text-type instance Eval (FromList lst) = 'Text lst+--+-- :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 (ToList =<< FromList '["a", "b"])--- Eval (ToList =<< FromList '["a", "b"]) :: [Symbol]+--+-- >>> :kind! Eval (ToSymbolList =<< FromSymbolList '["a", "b"])+-- Eval (ToSymbolList =<< FromSymbolList '["a", "b"]) :: [Symbol] -- = '["a", "b"]-data ToList :: Text -> Exp [Symbol]-type instance Eval (ToList ('Text lst)) = lst+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 =<< FromList '["w", "o", "r", "d"])--- Eval (ToSymbol =<< FromList '["w", "o", "r", "d"]) :: Symbol+--+-- >>> :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 lst)) = Eval (F.Foldr S.Append "" lst)+type instance Eval (ToSymbol ('Text sym)) = sym    -- | Null -- -- === __Example__--- --- >>> :kind! Eval (Null =<< FromList '["a", "b"])--- Eval (Null =<< FromList '["a", "b"]) :: Bool+--+-- >>> :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 ('Text '[])) = 'True-type instance Eval (Null ('Text (_ ': _))) = 'False+type instance Eval (Null txt) = Eval+    (If (Eval (Eval (Length txt) == 0))+        (Pure 'True)+        (Pure 'False)+    )   -- | Length -- -- === __Example__--- --- >>> :kind! Eval (Length =<< FromList '["a", "b"])--- Eval (Length =<< FromList '["a", "b"]) :: Nat+--+-- >>> :kind! Eval (Length =<< Singleton "ab")+-- Eval (Length =<< Singleton "ab") :: Nat -- = 2 data Length :: Text -> Exp Nat-type instance Eval (Length ('Text lst)) = Eval (F.Length lst)+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 '["a", "a", "m", "u"]))--- Eval (Cons "h" ('Text '["a", "a", "m", "u"])) :: Text--- = 'Text '["h", "a", "a", "m", "u"]+--+-- >>> :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 lst)) = 'Text (s ': lst)+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 '["a", "a", "m"]) "u")--- Eval (Snoc ('Text '["a", "a", "m"]) "u") :: Text--- = 'Text '["a", "a", "m", "u"]+--+-- >>> :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 lst) s) = 'Text (Eval (lst ++ '[s]))+type instance Eval (Snoc ('Text sym) s) = 'Text (TL.AppendSymbol sym s)  -- | Append two type-level texts. -- -- === __Example__ ----- >>> :kind! Eval (Append ('Text '["a", "a"]) ('Text '["m", "u"]))--- Eval (Append ('Text '["a", "a"]) ('Text '["m", "u"])) :: Text--- = 'Text '["a", "a", "m", "u"]+-- >>> :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 l1) ('Text l2)) = 'Text (Eval (l1 ++ l2))+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 '["h", "a", "a", "m", "u"]))--- Eval (Uncons ('Text '["h", "a", "a", "m", "u"])) :: Maybe---                                                       (Symbol, Text)--- = 'Just '("h", 'Text '["a", "a", "m", "u"])+-- >>> :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)+-- >>> :kind! Eval (Uncons ('Text ""))+-- Eval (Uncons ('Text "")) :: Maybe (Symbol, Text) -- = 'Nothing-data Uncons :: Text -> Exp (Maybe (Symbol, Text))-type instance Eval (Uncons ('Text '[])) = 'Nothing-type instance Eval (Uncons ('Text (t ': txt))) = 'Just '(t, 'Text txt)+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 '["a", "a", "m", "u", "n"]))--- Eval (Unsnoc ('Text '["a", "a", "m", "u", "n"])) :: Maybe---                                                       (Symbol, Text)--- = 'Just '("n", 'Text '["a", "a", "m", "u"])+-- >>> :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)+-- >>> :kind! Eval (Unsnoc ('Text ""))+-- Eval (Unsnoc ('Text "")) :: Maybe (Symbol, Text) -- = 'Nothing data Unsnoc :: Text -> Exp (Maybe (Symbol, Text))-type instance Eval (Unsnoc txt) =+type instance Eval (Unsnoc txt) =      Eval (F.FMap (Second Reverse) =<< Uncons =<< Reverse txt)  @@ -273,52 +297,56 @@ -- -- === __Example__ ----- >>> :kind! Eval (Head ('Text '["a", "a", "m", "u"]))--- Eval (Head ('Text '["a", "a", "m", "u"])) :: Maybe Symbol+-- >>> :kind! Eval (Head ('Text "aamu"))+-- Eval (Head ('Text "aamu")) :: Maybe Symbol -- = 'Just "a"--- --- >>> :kind! Eval (Head ('Text '[]))--- Eval (Head ('Text '[])) :: Maybe Symbol+--+-- >>> :kind! Eval (Head ('Text ""))+-- Eval (Head ('Text "")) :: Maybe Symbol -- = 'Nothing data Head :: Text -> Exp (Maybe Symbol)-type instance Eval (Head ('Text lst)) = Eval (F.Head lst)+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 '["h", "a", "a", "m", "u"]))--- Eval (Tail ('Text '["h", "a", "a", "m", "u"])) :: Maybe Text--- = 'Just ('Text '["a", "a", "m", "u"]) ----- >>> :kind! Eval (Tail ('Text '[]))--- Eval (Tail ('Text '[])) :: Maybe Text+-- >>> :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 lst)) = Eval (F.FMap FromList =<< F.Tail lst)+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 '["a", "a", "m", "u", "n"]))--- Eval (Init ('Text '["a", "a", "m", "u", "n"])) :: Maybe Text--- = 'Just ('Text '["a", "a", "m", "u"]) ----- >>> :kind! Eval (Init ('Text '[]))--- Eval (Init ('Text '[])) :: Maybe Text+-- >>> :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 lst)) = Eval (F.FMap FromList =<< F.Init lst)+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 '["a", "a", "m", "u"]) 3)--- Eval (CompareLength ('Text '["a", "a", "m", "u"]) 3) :: Ordering+--+-- >>> :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@@ -328,7 +356,7 @@ -- | FMap for type-level text. -- -- === __Example__--- +-- -- >>> :{ -- data IsIsymb :: Symbol -> Exp Bool -- type instance Eval (IsIsymb s) = Eval ("i" S.== s)@@ -339,57 +367,61 @@ --         (Pure s) --     ) -- :}--- --- >>> :kind! Eval (FMap Isymb2e ('Text '["i","m","u"]))--- Eval (FMap Isymb2e ('Text '["i","m","u"])) :: Text--- = 'Text '["e", "m", "u"]+--+-- >>> :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 ('Text lst)) = 'Text (Eval (F.FMap f lst))+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 '["a", "a", "m", "u"], 'Text '["v", "a", "l", "o"]]))--- Eval (Intercalate ('Text '[" ", "&", " "]) ('[ 'Text '["a", "a", "m", "u"], 'Text '["v", "a", "l", "o"]])) :: Text--- = 'Text '["a", "a", "m", "u", " ", "&", " ", "v", "a", "l", "o"]+--+-- >>> :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 ('Text txt) txts) =-    Eval (FromList =<< F.Intercalate txt =<< F.FMap ToList txts)+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 '["a", "a", "m", "u"]))--- Eval (Intersperse "." ('Text '["a", "a", "m", "u"])) :: Text--- = 'Text '["a", ".", "a", ".", "m", ".", "u"]+--+-- >>> :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 (FromList =<< F.Intersperse s txt)+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 '["a", "a", "m", "u"]))--- Eval (Reverse ('Text '["a", "a", "m", "u"])) :: Text--- = 'Text '["u", "m", "a", "a"] ----- >>> :kind! Eval (Reverse =<< Reverse ('Text '["a", "a", "m", "u"]))--- Eval (Reverse =<< Reverse ('Text '["a", "a", "m", "u"])) :: Text--- = 'Text '["a", "a", "m", "u"]+-- >>> :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 lst)) = 'Text (Eval (F.Reverse lst))+type instance Eval (Reverse txt) =  Eval (FromList =<< F.Reverse =<< ToList txt)  -- | Replace for type-level text. -- -- === __Example__--- --- >>> :kind! Eval (Replace ('Text '["t","u"]) ('Text '["l","a"]) ('Text '["t","u","u","t","u","t","t","a","a"]))--- Eval (Replace ('Text '["t","u"]) ('Text '["l","a"]) ('Text '["t","u","u","t","u","t","t","a","a"])) :: Text--- = 'Text '["l", "a", "u", "l", "a", "t", "t", "a", "a"]+--+-- >>> :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)@@ -398,12 +430,13 @@ -- | Concat for type-level text. -- -- === __Example__--- --- >>> :kind! Eval (Concat '[ 'Text '["l","a"], 'Text '["k","a","n","a"]])--- Eval (Concat '[ 'Text '["l","a"], 'Text '["k","a","n","a"]]) :: Text--- = 'Text '["l", "a", "k", "a", "n", "a"]+--+-- >>> :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 (F.Foldr Append (Eval Empty :: Text) lst)+type instance Eval (Concat lst) = +    'Text (T.ToSymbol2 @@ Eval (F.FMap ToSymbol lst))   @@ -417,45 +450,45 @@ -- data Isymb2aa :: Symbol -> Exp Text -- type instance Eval (Isymb2aa s) = Eval --     (If (IsIsymb @@ s)---         (Pure ('Text '["a","a"]))---         (Pure ('Text '[s]))+--         (Pure ('Text "aa"))+--         (Pure ('Text s)) --     ) -- :} ----- >>> :kind! Eval (FConcatMap Isymb2aa ('Text '["i","m","u"," ","i","h"]))--- Eval (FConcatMap Isymb2aa ('Text '["i","m","u"," ","i","h"])) :: Text--- = 'Text '["a", "a", "m", "u", " ", "a", "a", "h"]+-- >>> :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 lst)+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 '["a","a","m","u","1"]))--- Eval (Any S.IsDigit ('Text '["a","a","m","u","1"])) :: Bool+--+-- >>> :kind! Eval (Any S.IsDigit ('Text "aamu1"))+-- Eval (Any S.IsDigit ('Text "aamu1")) :: Bool -- = 'True ----- >>> :kind! Eval (Any S.IsDigit ('Text '["a","a","m","u"]))--- Eval (Any S.IsDigit ('Text '["a","a","m","u"])) :: Bool+-- >>> :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 lst)) = Eval (F.Any f lst)+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 '["a","a","m","u","1"]))--- Eval (All S.IsDigit ('Text '["a","a","m","u","1"])) :: Bool+--+-- >>> :kind! Eval (All S.IsDigit ('Text "aamu1"))+-- Eval (All S.IsDigit ('Text "aamu1")) :: Bool -- = 'False ----- >>> :kind! Eval (All S.IsDigit ('Text '["3","2","1"]))--- Eval (All S.IsDigit ('Text '["3","2","1"])) :: Bool+-- >>> :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 lst)+type instance Eval (All f ('Text lst)) = Eval (F.All f (T.ToList lst))   @@ -464,100 +497,100 @@ -- | Take for type-level text. -- -- === __Example__--- --- >>> :kind! Eval (Take 4 ('Text '["a", "a", "m", "u", "n"]))--- Eval (Take 4 ('Text '["a", "a", "m", "u", "n"])) :: Text--- = 'Text '["a", "a", "m", "u"]+--+-- >>> :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)) = 'Text (Eval (F.Take n lst))+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 '["h", "a", "a", "m", "u"]))--- Eval (TakeEnd 4 ('Text '["h", "a", "a", "m", "u"])) :: Text--- = 'Text '["a", "a", "m", "u"]+--+-- >>> :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)) =-    'Text (Eval (F.Reverse =<< F.Take n =<< F.Reverse lst))+    Eval (FromSymbolList =<< F.Reverse =<< F.Take n =<< F.Reverse (T.ToList lst))   -- | Drop for type-level text. -- -- === __Example__--- --- >>> :kind! Eval (Drop 2 ('Text '["a", "a", "m", "u", "n", "a"]))--- Eval (Drop 2 ('Text '["a", "a", "m", "u", "n", "a"])) :: Text--- = 'Text '["m", "u", "n", "a"]+--+-- >>> :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)) = 'Text (Eval (F.Drop n lst))+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 '["a", "a", "m", "u", "n", "a"]))--- Eval (DropEnd 2 ('Text '["a", "a", "m", "u", "n", "a"])) :: Text--- = 'Text '["a", "a", "m", "u"]+--+-- >>> :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)) =-    'Text (Eval (F.Reverse =<< F.Drop n =<< F.Reverse 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 '["a","a","m","u","1","2"]))--- Eval (TakeWhile (Not <=< S.IsDigit) ('Text '["a","a","m","u","1","2"])) :: Text--- = 'Text '["a", "a", "m", "u"]+--+-- >>> :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)) = 'Text (Eval (F.TakeWhile f lst))+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 '["1","2","a","a","m","u"]))--- Eval (TakeWhileEnd (Not <=< S.IsDigit) ('Text '["1","2","a","a","m","u"])) :: Text--- = 'Text '["a", "a", "m", "u"]+--+-- >>> :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)) =-    'Text (Eval (F.Reverse =<< F.TakeWhile f =<< F.Reverse 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 '["1","2","a","a","m","u"]))--- Eval (DropWhile S.IsDigit ('Text '["1","2","a","a","m","u"])) :: Text--- = 'Text '["a", "a", "m", "u"]+--+-- >>> :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)) = 'Text (Eval (F.DropWhile f lst))+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 '["a","a","m","u","1","2"]))--- Eval (DropWhileEnd S.IsDigit ('Text '["a","a","m","u","1","2"])) :: Text--- = 'Text '["a", "a", "m", "u"]+--+-- >>> :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)) =-    'Text (Eval (F.Reverse =<< F.DropWhile f =<< F.Reverse 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 '["3","4","a","a","m","u","1","2"]))--- Eval (DropAround S.IsDigit ('Text '["3","4","a","a","m","u","1","2"])) :: Text--- = 'Text '["a", "a", "m", "u"]+--+-- >>> :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) @@ -567,10 +600,10 @@ -- of type-level text. -- -- === __Example__--- --- >>> :kind! Eval (Strip ('Text '[" ", " ", "a", "a", "m", "u", " ", "\n"]))--- Eval (Strip ('Text '[" ", " ", "a", "a", "m", "u", " ", "\n"])) :: Text--- = 'Text '["a", "a", "m", "u"]+--+-- >>> :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) @@ -578,13 +611,13 @@ -- | SplitOn for type-level text. -- -- === __Example__--- --- >>> :kind! Eval (SplitOn (Eval (FromList '["a", "b"])) (Eval (FromList '[ "c", "d", "a", "b", "f", "g", "a", "b", "h"])))--- Eval (SplitOn (Eval (FromList '["a", "b"])) (Eval (FromList '[ "c", "d", "a", "b", "f", "g", "a", "b", "h"]))) :: [Text]--- = '[ 'Text '["c", "d"], 'Text '["f", "g"], 'Text '["h"]]+--+-- >>> :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 FromList =<< SOLoop sep '( '[], txt))+    Eval (F.FMap FromSymbolList =<< SOLoop (T.ToList sep) '( '[], T.ToList txt))   -- | Helper for SplitOn@@ -608,16 +641,17 @@     Eval (SOLoop sep =<< First (F.Snoc acc) =<< SOTake sep (t ': txt) '[])  + -- | Split for type-level text. -- -- === __Example__--- --- >>> :kind! Eval (Split S.IsSpace (Eval (FromList '[ "c", "d", " ", "b", "f", " ", "a", "b", "h"])))--- Eval (Split S.IsSpace (Eval (FromList '[ "c", "d", " ", "b", "f", " ", "a", "b", "h"]))) :: [Text]--- = '[ 'Text '["c", "d"], 'Text '["b", "f"], 'Text '["a", "b", "h"]]+--+-- >>> :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 FromList =<< SplitLoop p '( '[], txt))+    Eval (F.FMap FromSymbolList =<< SplitLoop p '( '[], T.ToList txt))  -- | Helper for Split data SplitTake :: (Symbol -> Exp Bool) -> [Symbol] -> [Symbol] -> Exp ([Symbol], [Symbol])@@ -631,28 +665,28 @@ -- | 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) '[])   --- | Lines for type-level text.+-- | Lines for type-level text. -- -- === __Example__--- --- >>> :kind! Eval (Lines =<< FromList '[ "o", "k", "\n", "h", "m", "m ", "\n", "a", "b"])--- Eval (Lines =<< FromList '[ "o", "k", "\n", "h", "m", "m ", "\n", "a", "b"]) :: [Text]--- = '[ 'Text '["o", "k"], 'Text '["h", "m", "m "], 'Text '["a", "b"]]+--+-- >>> :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 =<< FromList '[ "o", "k", " ", "h", "m", "m ", "\n", "a", "b"])--- Eval (Words =<< FromList '[ "o", "k", " ", "h", "m", "m ", "\n", "a", "b"]) :: [Text]--- = '[ 'Text '["o", "k"], 'Text '["h", "m", "m "], 'Text '["a", "b"]]+--+-- >>> :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) @@ -660,55 +694,57 @@ -- concats them. -- -- === __Example__--- --- >>> :kind! Eval (Unlines '[ 'Text '["o", "k"], 'Text '["h", "m", "m "], 'Text '["a", "b"]])--- Eval (Unlines '[ 'Text '["o", "k"], 'Text '["h", "m", "m "], 'Text '["a", "b"]]) :: Text--- = 'Text '["o", "k", "\n", "h", "m", "m ", "\n", "a", "b", "\n"]+--+-- >>> :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) =+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 '["o", "k"], 'Text '["h", "m", "m "], 'Text '["a", "b"]])--- Eval (Unwords '[ 'Text '["o", "k"], 'Text '["h", "m", "m "], 'Text '["a", "b"]]) :: Text--- = 'Text '["o", "k", " ", "h", "m", "m ", " ", "a", "b"]+--+-- >>> :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)+type instance Eval (Unwords txts) = Eval (Intercalate ('Text " ") txts)   -- | IsPrefixOf for type-level text. -- -- === __Example__--- --- >>> :kind! Eval (IsPrefixOf ('Text '["a", "a"]) ('Text '["a", "a", "m", "i", "a", "i", "n", "e", "n"]))--- Eval (IsPrefixOf ('Text '["a", "a"]) ('Text '["a", "a", "m", "i", "a", "i", "n", "e", "n"])) :: Bool+--+-- >>> :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 l1 l2)+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 '["n", "e", "n"]) ('Text '["a", "a", "m", "i", "a", "i", "n", "e", "n"]))--- Eval (IsSuffixOf ('Text '["n", "e", "n"]) ('Text '["a", "a", "m", "i", "a", "i", "n", "e", "n"])) :: Bool+--+-- >>> :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 l1 l2)+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 '["m", "i", "a"]) ('Text '["a", "a", "m", "i", "a", "i", "n", "e", "n"]))--- Eval (IsInfixOf ('Text '["m", "i", "a"]) ('Text '["a", "a", "m", "i", "a", "i", "n", "e", "n"])) :: Bool+--+-- >>> :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 l1 l2) -+type instance Eval (IsInfixOf ('Text l1) ('Text l2) ) =+    Eval (F.IsInfixOf (T.ToList l1) (T.ToList l2))

@@ -0,0 +1,310 @@+{-# LANGUAGE DataKinds              #-}+{-# LANGUAGE FlexibleInstances      #-}+{-# LANGUAGE MultiParamTypeClasses  #-}+{-# LANGUAGE PolyKinds              #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE TypeInType             #-}+{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE UndecidableInstances   #-}+{-# OPTIONS_GHC -Wall                       #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{-|+Module      : Fcf.Data.Text.Internal+Description : Type-level Text data structure with methods+Copyright   : (c) gspia 2020-+License     : BSD+Maintainer  : gspia++= Fcf.Data.Text.Internal++This is from https://kcsongor.github.io/symbol-parsing-haskell/++Ks. symbols library++-}++--------------------------------------------------------------------------------++module Fcf.Data.Text.Internal where++import Data.Char (chr)+-- import Data.Proxy++import qualified GHC.TypeLits as TL+import qualified Fcf.Data.List as L+import           Fcf.Data.Bitree+import qualified Fcf.Alg.Symbol as S+import Fcf++--------------------------------------------------------------------------------++type LookupTable = Tree (TL.Symbol, TL.Symbol)+++-- :kind! Head2 "hello"+type family Head2 (sym :: TL.Symbol) :: TL.Symbol where+    Head2 ""  = ""+    Head2 sym = Head1 sym (TL.CmpSymbol sym "\128")++-- :kind! ToList "hello"+type family ToList (sym :: TL.Symbol) :: [TL.Symbol] where+    ToList sym = ToList1 sym ""++-- Helper. +data ToSymbol2 :: [TL.Symbol] -> Exp TL.Symbol+type instance Eval (ToSymbol2 lst) = Eval (Foldr S.Append "" lst)++-- :kind! Eval (HeadA "koe")+data HeadA :: TL.Symbol -> Exp TL.Symbol+type instance Eval (HeadA sym) = Head1 sym (TL.CmpSymbol sym "\128")++-- :kind! Eval (ToListA "hello")+-- :kind! Eval (ToListA "")+data ToListA :: TL.Symbol -> Exp [TL.Symbol]+type instance Eval (ToListA sym) = ToList1 sym ""++-- :kind! Eval (Uncons "hello")+-- :kind! Eval (Uncons "")+data Uncons :: TL.Symbol -> Exp (Maybe TL.Symbol)+type instance Eval (Uncons sym) = Eval (Map ToSymbol2 =<< L.Tail =<< ToListA sym)+++-------------------------------------------------------------------------------++-- | Helper, from symbols-package.+type family Head1 (x :: TL.Symbol) (o :: Ordering) :: TL.Symbol where+  Head1 x 'GT = TL.TypeError ('TL.Text "Starts with non-ASCII character " 'TL.:<>: 'TL.ShowType x)+  Head1 x _   = LookupA x "" Chars++-- | Helper, from symbols-package.+type family ToList1 (x :: TL.Symbol) (pfx :: TL.Symbol) :: [TL.Symbol] where+  ToList1 x x   = '[]+  ToList1 x pfx = ToList2 x pfx (TL.CmpSymbol x (TL.AppendSymbol pfx "\128"))++-- | Helper, from symbols-package.+type family ToList2 (x :: TL.Symbol) (pfx :: TL.Symbol) (o :: Ordering) :: [TL.Symbol] where+  ToList2 x pfx 'LT = LookupA x pfx Chars ': ToList1 x (TL.AppendSymbol pfx (LookupA x pfx Chars))+  ToList2 x _   _   = TL.TypeError ('TL.Text "Non-AScII character in " 'TL.:<>: 'TL.ShowType x)++-- | Helper, from symbols-package.+type family LookupA (x :: TL.Symbol) (pfx :: TL.Symbol) (xs :: Tree TL.Symbol) :: TL.Symbol where+  LookupA "" _   _             = ""+  LookupA _  _   ('Leaf x)     = x+  LookupA x  ""  ('Node l c r) = Lookup2 x ""  c (TL.CmpSymbol x c)                    l r+  LookupA x  pfx ('Node l c r) = Lookup2 x pfx c (TL.CmpSymbol x (TL.AppendSymbol pfx c)) l r++-- | Helper, from symbols-package.+type family Lookup2 (x :: TL.Symbol) (pfx :: TL.Symbol) (c :: TL.Symbol) (o :: Ordering) (l :: Tree TL.Symbol) (r :: Tree TL.Symbol) :: TL.Symbol where+  Lookup2 _ _   c 'EQ _ _ = c+  Lookup2 x pfx c 'LT l _ = LookupA x pfx l+  Lookup2 x pfx _ 'GT _ r = LookupA x pfx r+++-- | Helper, from symbols-package. (Generate the character tree.)+chars :: Tree String+chars = buildTree [ chr c | c <- [0..0x7f] ] where+  buildTree []    = error "panic! buildTree []"+  buildTree [c]   = Leaf [c]+  buildTree pairs = Node (buildTree l) c (buildTree r) where+    n      = length pairs+    (l, r) = splitAt (n `div` 2) pairs+    c      = case r of+      []     -> error "panic! buildTree: r is empty"+      (c':_) -> [c']+++-- | Helper, from symbols-package. The character tree that is needed for+-- handling the initial character of a symbol.+type Chars = 'Node+  ('Node+     ('Node+        ('Node+           ('Node+              ('Node+                 ('Node ('Leaf "\NUL") "\SOH" ('Leaf "\SOH"))+                 "\STX"+                 ('Node ('Leaf "\STX") "\ETX" ('Leaf "\ETX")))+              "\EOT"+              ('Node+                 ('Node ('Leaf "\EOT") "\ENQ" ('Leaf "\ENQ"))+                 "\ACK"+                 ('Node ('Leaf "\ACK") "\a" ('Leaf "\a"))))+           "\b"+           ('Node+              ('Node+                 ('Node ('Leaf "\b") "\t" ('Leaf "\t"))+                 "\n"+                 ('Node ('Leaf "\n") "\v" ('Leaf "\v")))+              "\f"+              ('Node+                 ('Node ('Leaf "\f") "\r" ('Leaf "\r"))+                 "\SO"+                 ('Node ('Leaf "\SO") "\SI" ('Leaf "\SI")))))+        "\DLE"+        ('Node+           ('Node+              ('Node+                 ('Node ('Leaf "\DLE") "\DC1" ('Leaf "\DC1"))+                 "\DC2"+                 ('Node ('Leaf "\DC2") "\DC3" ('Leaf "\DC3")))+              "\DC4"+              ('Node+                 ('Node ('Leaf "\DC4") "\NAK" ('Leaf "\NAK"))+                 "\SYN"+                 ('Node ('Leaf "\SYN") "\ETB" ('Leaf "\ETB"))))+           "\CAN"+           ('Node+              ('Node+                 ('Node ('Leaf "\CAN") "\EM" ('Leaf "\EM"))+                 "\SUB"+                 ('Node ('Leaf "\SUB") "\ESC" ('Leaf "\ESC")))+              "\FS"+              ('Node+                 ('Node ('Leaf "\FS") "\GS" ('Leaf "\GS"))+                 "\RS"+                 ('Node ('Leaf "\RS") "\US" ('Leaf "\US"))))))+     " "+     ('Node+        ('Node+           ('Node+              ('Node+                 ('Node ('Leaf " ") "!" ('Leaf "!"))+                 "\""+                 ('Node ('Leaf "\"") "#" ('Leaf "#")))+              "$"+              ('Node+                 ('Node ('Leaf "$") "%" ('Leaf "%"))+                 "&"+                 ('Node ('Leaf "&") "'" ('Leaf "'"))))+           "("+           ('Node+              ('Node+                 ('Node ('Leaf "(") ")" ('Leaf ")"))+                 "*"+                 ('Node ('Leaf "*") "+" ('Leaf "+")))+              ","+              ('Node+                 ('Node ('Leaf ",") "-" ('Leaf "-"))+                 "."+                 ('Node ('Leaf ".") "/" ('Leaf "/")))))+        "0"+        ('Node+           ('Node+              ('Node+                 ('Node ('Leaf "0") "1" ('Leaf "1"))+                 "2"+                 ('Node ('Leaf "2") "3" ('Leaf "3")))+              "4"+              ('Node+                 ('Node ('Leaf "4") "5" ('Leaf "5"))+                 "6"+                 ('Node ('Leaf "6") "7" ('Leaf "7"))))+           "8"+           ('Node+              ('Node+                 ('Node ('Leaf "8") "9" ('Leaf "9"))+                 ":"+                 ('Node ('Leaf ":") ";" ('Leaf ";")))+              "<"+              ('Node+                 ('Node ('Leaf "<") "=" ('Leaf "="))+                 ">"+                 ('Node ('Leaf ">") "?" ('Leaf "?")))))))+  "@"+  ('Node+     ('Node+        ('Node+           ('Node+              ('Node+                 ('Node ('Leaf "@") "A" ('Leaf "A"))+                 "B"+                 ('Node ('Leaf "B") "C" ('Leaf "C")))+              "D"+              ('Node+                 ('Node ('Leaf "D") "E" ('Leaf "E"))+                 "F"+                 ('Node ('Leaf "F") "G" ('Leaf "G"))))+           "H"+           ('Node+              ('Node+                 ('Node ('Leaf "H") "I" ('Leaf "I"))+                 "J"+                 ('Node ('Leaf "J") "K" ('Leaf "K")))+              "L"+              ('Node+                 ('Node ('Leaf "L") "M" ('Leaf "M"))+                 "N"+                 ('Node ('Leaf "N") "O" ('Leaf "O")))))+        "P"+        ('Node+           ('Node+              ('Node+                 ('Node ('Leaf "P") "Q" ('Leaf "Q"))+                 "R"+                 ('Node ('Leaf "R") "S" ('Leaf "S")))+              "T"+              ('Node+                 ('Node ('Leaf "T") "U" ('Leaf "U"))+                 "V"+                 ('Node ('Leaf "V") "W" ('Leaf "W"))))+           "X"+           ('Node+              ('Node+                 ('Node ('Leaf "X") "Y" ('Leaf "Y"))+                 "Z"+                 ('Node ('Leaf "Z") "[" ('Leaf "[")))+              "\\"+              ('Node+                 ('Node ('Leaf "\\") "]" ('Leaf "]"))+                 "^"+                 ('Node ('Leaf "^") "_" ('Leaf "_"))))))+     "`"+     ('Node+        ('Node+           ('Node+              ('Node+                 ('Node ('Leaf "`") "a" ('Leaf "a"))+                 "b"+                 ('Node ('Leaf "b") "c" ('Leaf "c")))+              "d"+              ('Node+                 ('Node ('Leaf "d") "e" ('Leaf "e"))+                 "f"+                 ('Node ('Leaf "f") "g" ('Leaf "g"))))+           "h"+           ('Node+              ('Node+                 ('Node ('Leaf "h") "i" ('Leaf "i"))+                 "j"+                 ('Node ('Leaf "j") "k" ('Leaf "k")))+              "l"+              ('Node+                 ('Node ('Leaf "l") "m" ('Leaf "m"))+                 "n"+                 ('Node ('Leaf "n") "o" ('Leaf "o")))))+        "p"+        ('Node+           ('Node+              ('Node+                 ('Node ('Leaf "p") "q" ('Leaf "q"))+                 "r"+                 ('Node ('Leaf "r") "s" ('Leaf "s")))+              "t"+              ('Node+                 ('Node ('Leaf "t") "u" ('Leaf "u"))+                 "v"+                 ('Node ('Leaf "v") "w" ('Leaf "w"))))+           "x"+           ('Node+              ('Node+                 ('Node ('Leaf "x") "y" ('Leaf "y"))+                 "z"+                 ('Node ('Leaf "z") "{" ('Leaf "{")))+              "|"+              ('Node+                 ('Node ('Leaf "|") "}" ('Leaf "}"))+                 "~"+                 ('Node ('Leaf "~") "\DEL" ('Leaf "\DEL")))))))++

@@ -47,11 +47,11 @@  -------------------------------------------------------------------------------- --- | Same as in containers, except not used for any term-level computation +-- | Same as in containers, except not used for any term-level computation -- in this module. data Tree a = Node a [Tree a] --- | Same as in containers, except not used for any term-level computation +-- | Same as in containers, except not used for any term-level computation -- in this module. type Forest a = [Tree a] @@ -66,7 +66,7 @@ -- | Unfold for a 'Tree'. -- -- === __Example__--- +-- -- >>> data BuildNode :: Nat -> Exp (Nat,[Nat]) -- >>> :{ --   type instance Eval (BuildNode x) =@@ -93,7 +93,7 @@ -- | Flatten a 'Tree'. -- -- === __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] -- = '[1, 2, 3, 4, 5, 6]@@ -125,7 +125,7 @@ -- | Get the levels from a 'Tree'. -- -- === __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]] -- = '[ '[1], '[2, 5], '[3, 6], '[4]]