Egisonで文字列書き換え系四則演算

rewriteNat1.egins

-- > Egison Version == 3.9.4
-- > egison -N
-- > loadFile "rewriteNat1.egins"



--
-- Utils
--

flip f x y = f y x

concatString xss =
  foldr (\ xs rs -> appendString xs rs) "" xss

intercalateString = compose intersperse concatString

replaceString before after str =
  intercalateString after (splitString before str)

-- "s"のみを得る
getSucc x = replaceString "o" "" x



-- ex. "sssso" : 4

-- 加算
add x y = flip (\y x -> replaceString "o" y x) x y

-- 減算
sub x y =
  let ans = replaceString y "o" x
  in if x == ans then "o" else ans

-- 乗算
mul x y = replaceString "s" (getSucc y) x

-- 余り
mod x y = replaceString (getSucc y) "" x

-- 除算
div x y = replaceString (getSucc y) "s" (sub x (mod x y))



--
-- Tests
--
-- > egison -N -t rewriteNat1.egins

assertEqual "add"
  (add "sssso" "sso")
  "sssssso"

assertEqual "sub_1"
  (sub "ssssso" "sso")
  "ssso"

assertEqual "sub_2"
  (sub "ssssso" "sssssssssso")
  "o"

assertEqual "mul_1"
  (mul "sssso" "sso")
  "sssssssso"

assertEqual "mul_2"
  (mul "sssso" "o")
  "o"

assertEqual "mul_3"
  (mul "o" "sso")
  "o"

-- 0除算すると落ちますw
assertEqual "mod"
  (mod "ssssso" "sso")
  "so"
assertEqual "div"
  (div "ssssso" "sso")
  "sso"

rewriteNat2.egins

-- > Egison Version == 3.9.4
-- > egison -N
-- > loadFile "rewriteNat2.egins"



--
-- Utils
--

flip f x y = f y x

concatString xss =
  foldr (\ xs rs -> appendString xs rs) "" xss

intercalateString = compose intersperse concatString

replaceString before after str =
  intercalateString after (splitString before str)

convergeList =
  \match as list something with
    | $x : #x  : _ -> x
    | _  : $xs     -> convergeList xs

-- 収束するまで置換を繰り返す
convergeReplaceString before after str =
  convergeList (iterate (\s -> replaceString before after s) str)

reverseString str = pack (reverse (unpack str))



-- ex. "sssso" : 4

-- 加算
add x y = flip (\y x -> replaceString "o" y x) x y

-- 減算
sub x y =
  convergeReplaceString "po" "o"
    (convergeReplaceString "ps" ""
      (replaceString "o" x (replaceString "s" "p" y)) )
sub2 x y =
  convergeReplaceString "os" "o"
    (convergeReplaceString "sos" "o"
      (replaceString "o" (reverseString y) x) )

-- 乗算
mul x y =
  reverseString
    (convergeReplaceString "so" (reverseString y) x)

-- 余り
mod x y = convergeReplaceString y "o" x

-- 除算
div x y =
  reverseString
    (convergeReplaceString y "os" (sub x (mod x y)))



--
-- Tests
--
-- > egison -N -t rewriteNat2.egins

assertEqual "add"
  (add "sssso" "sso")
  "sssssso"

assertEqual "sub_1"
  (sub "ssssso" "sso")
  "ssso"

assertEqual "sub_2"
  (sub "ssssso" "sssssssssso")
  "o"

assertEqual "mul_1"
  (mul "sssso" "sso")
  "sssssssso"

assertEqual "mul_2"
  (mul "sssso" "o")
  "o"

assertEqual "mul_3"
  (mul "o" "sso")
  "o"

assertEqual "mod"
  (mod "ssssso" "sso")
  "so"

assertEqual "div"
  (div "ssssso" "sso")
  "sso"


assertEqual "sub2_1"
  (sub2 "ssssso" "sso")
  "ssso"

assertEqual "sub2_2"
  (sub2 "ssssso" "sssssssssso")
  "o"

rewriteNat2_2.egins

-- Egison Version >= 3.10.0
-- $ egison -N
-- > loadFile "rewriteNat2_2.egins"



--
-- Utils
--

-- ポイントフリースタイルで書けない
concatString xss :=
  foldr (\xs rs -> appendString xs rs) "" xss

intercalateString := compose intersperse concatString

replaceString before after str :=
  intercalateString after (splitString before str)

-- 双子素数の例を参考に
getSameSeries :=
  \match as list something with
    | _ ++ $x :: #x :: _ -> x

-- 収束するまで置換を繰り返す
convergeReplaceString before after str :=
  getSameSeries (iterate (\s -> replaceString before after s) str)

reverseString str := pack (reverse (unpack str))



-- ex. "sssso" : 4

-- 加算
-- flipは、まずfだけを引数にとるので、ポイントフリーっぽく書ける
add := flip (\y x -> replaceString "o" y x)

-- 減算
sub x y :=
  convergeReplaceString "os" "o"
    (convergeReplaceString "sos" "o"
      (replaceString "o" (reverseString y) x) )

-- 乗算
mul x y :=
  reverseString
    (convergeReplaceString "so" (reverseString y) x)

-- 余り
mod x y := convergeReplaceString y "o" x

-- 除算
div x y :=
  reverseString
    (convergeReplaceString y "os" (sub x (mod x y)))



--
-- Tests
--
-- $ egison -N -t rewriteNat2_2.egins

assertEqual "add"
  (add "sssso" "sso")
  "sssssso"

assertEqual "sub_1"
  (sub "ssssso" "sso")
  "ssso"

assertEqual "sub_2"
  (sub "ssssso" "sssssssssso")
  "o"

assertEqual "mul_1"
  (mul "sssso" "sso")
  "sssssssso"

assertEqual "mul_2"
  (mul "sssso" "o")
  "o"

assertEqual "mul_3"
  (mul "o" "sso")
  "o"

assertEqual "mod"
  (mod "ssssso" "sso")
  "so"

assertEqual "div"
  (div "ssssso" "sso")
  "sso"

rewriteNat3.egins

-- > Egison Version == 3.10.0
-- > egison -N
-- > loadFile "rewriteNat3.egins"



--
-- Matcher
--

myNat := matcher
  | o as () with
    | 0 -> [()]
    | _ -> []
  | s $ as myNat with
    | $tgt -> match (compare tgt 0) as ordering with
              | greater -> tgt - 1
              | _       -> []
  -- MatcherをmyNatにできなかった
  | $ ++ $ as (myNat, nat) with
    | $tgt -> matchAll tgt as nat with
              | loop $i (1, $x) (s ...) $rs -> (x, rs)
  | #$val as () with
    | $tgt -> if val = tgt then [()] else []
  | $ as something with
    | $tgt -> [tgt]



--
-- Utils
--



--
-- Codes
--

test1 := matchAll 5 as myNat with
  | _ ++ s $n -> n
test2 := matchAll 7 as myNat with
  | $m ++ s $n -> (m, n)
test3 := \matchAll as myNat with
  | $m ++ s $n -> (m, n)
test4 := matchAll 7 as myNat with
  | $m ++ $n -> (m, n)

-- 減算
sub x y := match x as myNat with
  | #y ++ $n -> n
  | _        -> 0 -- when x < y

-- 大きい方
max x y := match ((sub x y), (sub y x)) as (myNat, myNat) with
  | (#0, #0) -> 0
  | (#0, _)  -> y
  | (_, #0)  -> x

-- 加算
add x y := match (drop (max x y) nats0) as list myNat with
  | _ ++ ((#x ++ #y) & $z) :: _ -> z


rev := \match as list something with
  | []          ++ []          -> []
  | []          ++ ($y :: [])  -> [y]
--  | ($x :: [])  ++ ($y :: [])  -> [y, x]
--  | ($x :: [])  ++ ($y :: $ys) -> append (rev (cons y ys)) [x]
  | ((_ :: _) & $xs) ++ ((_ :: _) & $ys) -> append (rev ys) (rev xs)
-- rev (rev (xs ++ ys))
-- -> rev ((rev ys) `append` (rev xs))
-- -> (rev (rev xs)) `append` (rev (rev ys))
-- xs ++ ys
-- lemma : rev (xs ++ ys) = rev ys ++ rev xs



hoge := \matchAll as list something with
  | $a ++ $b -> (a, b)
hoge2 := match [2] as list something with
  | _ :: [] -> True


--
-- Tests
--
-- > egison -N -t rewriteNat3.egins

assertEqual "1.test1"
  test1
  [4, 3, 2, 1, 0]

assertEqual "2.test2"
  test2
  [(0, 6), (1, 5), (2, 4), (3, 3), (4, 2), (5, 1), (6, 0)]

assertEqual "3.test4"
  test4
  [(0, 7), (1, 6), (2, 5), (3, 4), (4, 3), (5, 2), (6, 1), (7, 0)]


assertEqual "4.sub_1"
  (sub 7 2)
  5

assertEqual "5.sub_2"
  (sub 7 22)
  0

assertEqual "6.sub_3"
  (sub 7 0)
  7

assertEqual "7.sub_4"
  (sub 0 7)
  0


assertEqual "8.add_1"
  (add 1 1)
  2

assertEqual "9.add_2"
  (add 0 0)
  0

assertEqual "10.add_3"
  (add 7 0)
  7

assertEqual "11.add_4"
  (add 0 7)
  7

assertEqual "12.add_5"
  (add 7 4)
  11