--
--
-- String
--
--

inductive pattern String :=
  | regexCg String String [String] String
  | regex String String String String
  | s.empty
  | s.cons Char String
  | s.join String String

def string : Matcher String :=
  matcher
--    | regexCg #$regexpr $ $ $ as (string, list string, string) with
--      | $tgt -> regexCg regexpr tgt
--    | regex #$regexpr $ $ $ as (string, string, string) with
--      | $tgt -> regex regexpr tgt
    | s.empty as () with
      | $tgt -> if "" = tgt then [()] else []
    | s.cons $ $ as (char, string) with
      | $tgt -> if "" = tgt then [] else [unconsString tgt]
--    | s.join $ (s.cons #$px $) as (string, string) with
--      | $tgt ->
--        matchAll S.split (pack [px]) tgt as list string with
--          | s.join (!s.empty & $xs) (!s.empty & $ys) ->
--            (xs, ys)
--    | s.join $ (s.join #$pxs $) as (string, string) with
--      | $tgt ->
--        matchAll S.split pxs tgt as list string with
--          | s.join (!s.empty & $xs) (!s.empty & $ys) ->
--            (S.intercalate pxs xs, S.intercalate pxs ys)
    | s.join $ $ as (string, string) with
      | $tgt ->
        matchAll tgt as string with
          | loop $i (1, $n)
              (s.cons $xa_i ...)
              $rs -> (pack (map (\i -> xa_i) (between 1 n)), rs)
    | #$val as () with
      | $tgt -> if val = tgt then [()] else []
    | $ as something with
      | $tgt -> [tgt]

--
-- String as collection
--
def S.isEmpty (xs: String) : Bool := xs = ""

def S.cons (x: Char) (xs: String) : String := appendString (pack [x]) xs

def S.head (xs: String) : Char :=
  match xs as string with
    | s.cons $x _ -> x

def S.tail (xs: String) : String :=
  match xs as string with
    | s.cons _ $r -> r

def S.last (str: String) : Char :=
  match str as string with
    | s.join _ (s.cons $c s.empty) -> c

def S.map (f: Char -> Char) (xs: String) : String := pack (map f (unpack xs))

def S.length : String -> Integer := lengthString
def S.split : String -> String -> [String] := splitString
def S.append : String -> String -> String := appendString

def S.concat (xss: [String]) : String := foldr (\xs rs -> S.append xs rs) "" xss

def S.intercalate (sep: String) (ss: [String]) : String := S.concat (intersperse sep ss)

def S.replace (before: String) (after: String) (str: String) : String := S.intercalate after (S.split before str)

--
-- Alphabet
--
def C.between (c1: Char) (c2: Char) : [Char] := map itoc (between (ctoi c1) (ctoi c2))

def C.isBetween (c1: Char) (c2: Char) (c: Char) : Bool := ctoi c >= ctoi c1 && ctoi c <= ctoi c2

def isAlphabet (c: Char) : Bool := C.isBetween 'a' 'z' c || C.isBetween 'A' 'Z' c

def isAlphabetString (s: String) : Bool := all isAlphabet (unpack s)

def upperCase (c: Char) : Char := if C.isBetween 'a' 'z' c then itoc (ctoi c - 32) else c

def lowerCase (c: Char) : Char := if C.isBetween 'A' 'Z' c then itoc (ctoi c + 32) else c

--
-- Number
--
def showDecimal (c: Integer) (x: Integer) : String :=
  match rtod x as (integer, list integer, list integer) with
    | ($q, $s, $cycle) ->
      let allDigits := s ++ (if isEmpty cycle then [] else cycle ++ cycle ++ cycle)
          sc := take c allDigits
       in foldl S.append (S.append (show q) ".") (map show sc)

def showDecimal' (x: Integer) : String :=
  match rtod x as (integer, list integer, list integer) with
    | ($q, $s, $c) ->
        foldl
          S.append
          ""
          (S.append (show q) "." :: map show s ++ " " :: map show c ++ [" ..."])