diff --git a/bower.json b/bower.json index 2ef2de0..ba889df 100644 --- a/bower.json +++ b/bower.json @@ -18,5 +18,9 @@ "dependencies": { "purescript-prelude": "^5.0.0", "purescript-type-equality": "^4.0.0" + }, + "devDependencies": { + "purescript-assert": "^5.0.0", + "purescript-console": "^5.0.0" } } diff --git a/src/Type/Data/Symbol.purs b/src/Type/Data/Symbol.purs index 8ff8564..2af5549 100644 --- a/src/Type/Data/Symbol.purs +++ b/src/Type/Data/Symbol.purs @@ -1,12 +1,18 @@ module Type.Data.Symbol - ( module Prim.Symbol - , module Data.Symbol - , append - , compare - , uncons + ( append , class Equals + , class Reverse + , class ReverseP + , class Snoc + , compare , equals - ) where + , reverse + , module Data.Symbol + , module Prim.Symbol + , snoc + , uncons + ) + where import Prim.Symbol (class Append, class Compare, class Cons) import Data.Symbol (SProxy(..), class IsSymbol, reflectSymbol, reifySymbol) @@ -33,3 +39,47 @@ instance equalsSymbol equals :: forall proxy l r o. Equals l r o => proxy l -> proxy r -> Proxy o equals _ _ = Proxy + + +-- Reverse + +class ReverseP (a :: Symbol) (reversed :: Symbol) | a -> reversed, reversed -> a + +instance reverseEmpty :: ReverseP "" "" +else +instance reverseCons :: + ( Cons head tail sym + , ReverseP tailReverse tail + , ReverseP tail tailReverse + , Append tailReverse head reversed + ) => ReverseP sym reversed + +class Reverse (a :: Symbol) (reversed :: Symbol) | a -> reversed, reversed -> a + +instance reverseReverseP :: (ReverseP a b, ReverseP b a) => Reverse a b + +--| ```purescript +--| > :t reverse (Proxy :: Proxy "symbol") +--| Proxy @Symbol "lobmys" +--| ``` +-- | +reverse :: ∀ proxy a b. Reverse a b => proxy a -> Proxy b +reverse _ = Proxy + +-- Snoc + +--| ```purescript +--| Snoc "symbo" "l" ?x ~~> ?x = "symbol" +--| Snoc ?a ?b "symbol" ~~> ?a = "symbo", ?b = "l" +--| ``` +-- | `end` must be a single character +class Snoc (list :: Symbol) (end :: Symbol) (symbol :: Symbol) | end list -> symbol, symbol -> end list + +instance snocReverse :: (Reverse sym reversed, Cons end listReverse reversed, Reverse listReverse list) => Snoc list end sym + +--| ```purescript +--| > :t snoc (Proxy :: Proxy "symbo") (Proxy :: Proxy "l") +--| Proxy @Symbol "symbol" +--| ``` +snoc :: ∀a b c. Snoc a b c => Proxy a -> Proxy b -> Proxy c +snoc _ _ = Proxy diff --git a/test/Main.purs b/test/Main.purs new file mode 100644 index 0000000..e61c5b4 --- /dev/null +++ b/test/Main.purs @@ -0,0 +1,64 @@ +module Test.Main where + +import Prelude + +import Debug (spy) +import Effect (Effect) +import Effect.Class.Console (log) +import Prim.Symbol (class Cons) +import Test.Assert (assertTrue) +import Type.Data.Symbol (class IsSymbol, class Reverse, class ReverseP, class Snoc, reflectSymbol, reverse, snoc) +import Type.Proxy (Proxy(..)) + +-- reverse +testReverse :: Proxy "lobmys" +testReverse = reverse (Proxy :: Proxy "symbol") + +testReverseForward :: Proxy _ +testReverseForward = reverse (Proxy:: Proxy "symbol") + +testReverseBackward :: Proxy "lobmyys" +testReverseBackward = reverse (Proxy :: Proxy _) + +testReverseSingle :: Proxy "s" +testReverseSingle = reverse $ Proxy :: Proxy "s" + +testReverseEmpty :: Proxy "" +testReverseEmpty = reverse $ Proxy :: Proxy "" + +-- Reversing a reversed Symbol should be the same as the Symbol itself +propReverseIdem :: forall a b . IsSymbol a => IsSymbol b => Reverse a b => Reverse b a => Proxy a -> Boolean +propReverseIdem p = reflectSymbol p == reflectSymbol sameThing + where + sameThing = reverse (reverse p :: Proxy b) + +testUnicode :: Proxy "🍎enip" +testUnicode = reverse (Proxy :: Proxy "pine🍎") + +-- snoc +testSnoc :: Proxy "symbol" +testSnoc = snoc (Proxy :: Proxy "symbo") (Proxy :: Proxy "l") + +testSnocForward :: Proxy _ +testSnocForward = snoc (Proxy :: Proxy "symbo") (Proxy :: Proxy "l") + +testSnocBackwardLeft :: Proxy "symbol" +testSnocBackwardLeft = snoc (Proxy :: Proxy _) (Proxy :: Proxy "l") + +testSnocBackwardRight :: Proxy "symbol" +testSnocBackwardRight = snoc (Proxy :: Proxy "symbo") (Proxy :: Proxy _) + +testSnocBackwardBoth :: Proxy "symbol" +testSnocBackwardBoth = snoc (Proxy :: Proxy _) (Proxy :: Proxy _) + +testSnocEmpty :: Proxy "s" +testSnocEmpty = snoc (Proxy :: Proxy "") (Proxy :: Proxy "s") + +main :: Effect Unit +main = do + assertTrue $ propReverseIdem (Proxy :: Proxy "Test Symbol") + assertTrue $ propReverseIdem (Proxy :: Proxy "Unico∀e") + assertTrue $ propReverseIdem (Proxy :: Proxy "<-<>") + assertTrue $ propReverseIdem (Proxy :: Proxy "") + assertTrue $ propReverseIdem (Proxy :: Proxy "1") + assertTrue $ propReverseIdem (Proxy :: Proxy "pine🍎") \ No newline at end of file