Data update

Task/Palindrome-detection/EasyLang/palindrome-detection.easy

@@ -3,7 +3,7 @@ func$ reverse s$ .
    for i = 1 to len a$[] div 2
       swap a$[i] a$[len a$[] - i + 1]
    .
-   return strjoin a$[]
+   return strjoin a$[] ""
 .
 func palin s$ .
    if s$ = reverse s$

Task/Palindrome-detection/Golfscript/palindrome-detection-2.golf

@@ -1,4 +1,3 @@
-"ABBA" pal
-"a" pal
-"13231+464+989=989+464+13231" pal
-"123 456 789 897 654 321" pal
+["ABBA" "a"
+"13231+464+989=989+464+13231"
+"123 456 789 897 654 321"]{pal puts}/

Task/Palindrome-detection/Idris/palindrome-detection-1.idris

@@ -0,0 +1,30 @@
+module Palindromes
+
+import Data.Primitives.Views
+import Data.List
+import Data.List.Views
+import Data.Nat
+
+isPalindromeReverse : String -> Bool
+isPalindromeReverse str = let cs = unpack str in cs == reverse cs
+
+isPalindromeReverseHalf : String -> Bool
+isPalindromeReverseHalf str =
+  let cs = (unpack str)
+      n = (length str) `div` 2
+   in take n cs == (take n $ reverse cs)
+
+isPalindromeSplit : String -> Bool
+isPalindromeSplit str =
+  let cs = unpack str
+      n = length cs `div` 2
+      (left, right) = bimap id reverse $ splitAt n cs
+    in all (uncurry (==)) $ zip left right
+
+isPalindromeSnoc : String -> Bool
+isPalindromeSnoc str =
+  let cs = unpack str in go cs
+  where go : Eq a => List a -> Bool
+        go xs with (snocList xs)
+          go (x :: ys ++ [z]) | Snoc z (x::ys) _ = x == z && go ys
+          go _ | _ = True

Task/Palindrome-detection/Idris/palindrome-detection-2.idris

@@ -0,0 +1,58 @@
+module PalindromesTypeLevel
+
+import Data.List
+import Data.List.Views
+
+
+isPalindromeDirect : (str : String) -> (str = reverse str) => Bool
+isPalindromeDirect _ = True
+
+ipd = isPalindromeDirect "AABBAA"
+
+failing
+  ipdf = isPalindromeDirect "ABCCBB"
+
+
+||| Proof that the list is constructed of consecutive pairs of equal elements.
+||| Last element can be unpaired.
+data EqualPairsInList : List a -> Type where
+  Nil : EqualPairsInList []
+  Single : EqualPairsInList [x]
+  EqualPair : EqualPairsInList xs -> EqualPairsInList (x :: x :: xs)
+
+||| Reorders the list so that the first half is interleaved with a reversed second half.
+interleaveOwnHalfReverse : List a -> List a
+interleaveOwnHalfReverse [] = []
+interleaveOwnHalfReverse [x] = [x]
+interleaveOwnHalfReverse (x :: y :: ys) = let (z, zs) = splitLast (y::ys) in x :: z :: interleaveOwnHalfReverse zs
+  where splitLast : (xs : List a) -> NonEmpty xs => (a, List a)
+        splitLast [x] = (x, [])
+        splitLast (x :: y :: ys) = let (z, zs) = splitLast (y::ys) in (z, x::zs)
+
+||| Precondition for checking if a list is a palindrome.
+IsPalindrome : List a -> Type
+IsPalindrome = EqualPairsInList . interleaveOwnHalfReverse
+
+||| Function for testing palindromes. Typechecks only when applied to a palindrome list.
+isPalindrome : (xs : List a) -> IsPalindrome xs => Bool
+isPalindrome  _ = True
+
+||| Palindrome precondition specialized for strings.
+IsPalindromeStr : String -> Type
+IsPalindromeStr = IsPalindrome . unpack
+
+||| Function for testing string palindromes. Typechecks only when applied to a palindrome list.
+isPalindromeStr : (str : String) -> IsPalindromeStr str => Bool
+isPalindromeStr  _ = True
+
+
+-- Tests
+
+ip = isPalindrome [1, 4, 3, 1, 1, 3, 4, 1]
+ips = isPalindromeStr "ABCDCBA"
+
+failing
+  ipf = isPalindrome [2, 2, 2, 3, 2, 2]
+
+failing
+  ipsf = isPalindromeStr "RBCDCBA"

Task/Palindrome-detection/YAMLScript/palindrome-detection.ys

@@ -1,4 +1,4 @@
-!yamlscript/v0
+!YS-v0
 
 defn main(n=31337):
   not =: when((n:S != n:S:reverse) ' not')