prelude.rev

// appends an item to a list
append: forall A. ([A], A) <=> [A] = 
    forall A. \(l, x) => case l of
        [] => [x];
        y :: r => y :: append{A}(r, x)
// reverses a list
reverse: forall A. [A] <=> [A] =
    forall A. \l => case l of
        [] => [];
        x :: r => append{A}(reverse{A}(r), x)
// applies each element of a list to a function
map: forall A. forall B. (A -> B) -> ([A] -> [B]) =
    forall A. forall B. \f => \l => case l of
        [] => [];
        a :: r => f(a) :: map{A}{B}(f)(r)
// applies each element of a list to a reversible function
mapr: forall A. forall B. (A <=> B) -> ([A] <=> [B]) =
    forall A. forall B. \f => \l => case l of
        [] => [];
        a :: r => f(a) :: mapr{A}{B}(f)(r)

// returns the length of a string
strlen: String -> Int = 
    \splitAt(1)~(c, r) => case c of
        "" => 0;
        x => 1 + strlen(r)
// returns the substring at index [f, t)
substr: String -> (Int, Int) -> String =
    \s => \(f, t) => let (x2, s2) = splitAt(&f)(s); 
                         (s3, x3) = splitAt(t - f)(s2) 
                     in s3
// splits the string at n characters from the right
splitAtRight: Int -> String <=> (String, String) =
    \n => \s => case s of
        splitAt(n)~(s2, "") => ("", s2);
        splitAt(1)~(c, s2) => let (s3, s4) = splitAtRight(n)(s2) in (splitAt(1)~(c, s3), s4)
// reverses a string
strReverse: String <=> String =
    \s => case s of
        "" => "";
        splitAtRight(1)~(r, c) => splitAt(1)~(c, strReverse(r))

// reversible parser type
type Parser = forall A. String <=> (A, String)
type Equ = forall A. A <=> ()
// returns the number of leading whitespaces of a string and the string without leading whitespaces 
scanWS: Parser{Int} =
    \splitAt(1)~(c, r) => case c of
        "" => (0, r);
        " " => let (ws, y) = scanWS(r) in (ws + 1, y);
        y => (0, splitAt(1)~(y, r))
// returns the string without leading whitespaces
skipWS: String <=> String =
    \scanWS~(ws, s) => 
        let () = forget{Int}(0)(ws) in s

// muladd(k)(a, b) = a * k + b. muladd(k)~(y) = (floor(y / k), y mod k) 
muladd: Int -> (Int, Int) <=> Int =
    \k => \(a, b) =>
        let y = a * k + b;
            () = forget{Int}(y - y / k * k)(b)
        in y
str2Int_: String <=> Int =
    \s => case s of
        "" => 0;
        splitAt(1)~("0", r) => muladd(10)(str2Int_(r), 0);
        splitAt(1)~("1", r) => muladd(10)(str2Int_(r), 1);
        splitAt(1)~("2", r) => muladd(10)(str2Int_(r), 2);
        splitAt(1)~("3", r) => muladd(10)(str2Int_(r), 3);
        splitAt(1)~("4", r) => muladd(10)(str2Int_(r), 4);
        splitAt(1)~("5", r) => muladd(10)(str2Int_(r), 5);
        splitAt(1)~("6", r) => muladd(10)(str2Int_(r), 6);
        splitAt(1)~("7", r) => muladd(10)(str2Int_(r), 7);
        splitAt(1)~("8", r) => muladd(10)(str2Int_(r), 8);
        splitAt(1)~("9", r) => muladd(10)(str2Int_(r), 9)
// returns the integer represented by a string ignoring leading zeroes and whitespaces
str2Int: String <=> Int =
    \skipWS~(s) => str2Int_(strReverse(s))

// parses a fixed string
pWord: String -> Parser{()} = 
    \w: String => \splitAt(strlen(&w))~(&w, r) => ((), r)
// parser one of a set of characters given as a string
pChar: String -> Parser{String} =
    \cs => case cs of
        "" => pFail{String}("all characters failed");
        splitAt(1)~(c, rcs) => \s <=> case () of
            () => pMap{()}{String}(pWord(c))(\() <=> &c)(s);
            () => pChar(rcs)(s)
pConst: forall A. String -> Equ{A} -> Parser{A} =
    forall A. \w: String => \a => pMap{()}{A}(pWord(w))(a~)
// parses nothing, always succeeds
pEmpty: Parser{()} = 
    pWord("")
pEmptyList: forall A. Parser{[A]} = 
    forall A. \s => ([], s)
pFail: forall A. String -> Parser{A} = 
    forall A. \msg => \reject{String}(msg)() => reject{(A, String)}(msg)()
pWS_: String <=> (String, String) =
    \s: String => case s of
        splitAt(1)~(" ", r) => 
            let (ws, r2) = pWS_(r) in
            (splitAt(1)~(" ", ws), r2);
        r => ("", r)
// parses (possibly empty) whitespaces
pWS: String -> Parser{()} = 
    \default => pForget{String}(default)(pWS_)

// forgets a parse result by providing a default
pForget: forall A. A -> Parser{A} -> Parser{()} =
    forall A. \a => \p => \s <=> 
        let (x, r) = p(s);
            () = forget{A}(a)(x) in
        ((), r)
// applies a reversible function to a parser
pMap: forall A. forall B. Parser{A} -> (A <=> B) -> Parser{B} =
    forall A. forall B. \pa => \f => \s <=> 
        let (a, r) = pa(s) in (f(a), r)
// monad bind for parsers
pBind: forall A. forall B. Parser{A} -> (A -> Parser{B}) -> Parser{(A, B)} =
    forall A. forall B. \pa => \f => \s <=> 
        let (a, r) = pa(s);
            (b, r2) = f(a)(r)
        in ((a, b), r2)
pRepSepN: forall A. Int -> Parser{A} -> Parser{()} -> Parser{[A]} =
    forall A. \n => case n of
        0      => \p => \ps => pEmptyList{A};
        1      => \p => \ps => \s <=> let (x1, s1) = p(s) in ([x1], s1);
        n2 + 1 => \p => \ps => \s <=> let (x1, s1) = p(s);
                                   ((), s2) = ps(s1);
                                   (l3, s3) = pRepSepN{A}(n2)(p)(ps)(s2)
                               in (x1 :: l3, s3)
// non-empty repeating parser with separator
pRepSep1: forall A. Parser{A} -> Parser{()} -> Parser{[A]} =
    forall A. \p => \pSep => \s => case () of
        () => let (v1, r1) = p(s);
                  ((), r2) = pSep(r1);
                  (l3, r3) = pRepSep1{A}(p)(pSep)(r2) 
              in (v1 :: l3, r3);
        () => let (v1, r1) = p(s) 
              in ([v1], r1)
// possibly empty repeating parser with separator
pRepSep: forall A. Parser{A} -> Parser{()} -> Parser{[A]} =
    forall A. \p => \pSep => \s => case () of
        () => pRepSep1{A}(p)(pSep)(s);
        () => ([], s)
// non-empty repeating parser
pRep1: forall A. Parser{A} -> Parser{[A]} = 
    forall A. \p => pRepSep1{A}(p)(pEmpty)
// possibly empty repeating parser (Kleene-star)
pRep: forall A. Parser{A} -> Parser{[A]} = 
    forall A. \p => pRepSep{A}(p)(pEmpty)
// parsers in sequence
pSeq: forall A. [Parser{A}] -> Parser{[A]} =
    forall A. \ps => case ps of
        [] => \s => ([], s);
        p :: rps => \s => let (x1, s1) = p(s);
                              (l2, s2) = pSeq{A}(rps)(s1)
                          in (x1 :: l2, s2)
pThen: forall A. forall B. (Parser{A}, Parser{B}) -> Parser{(A, B)} =
    forall A. forall B. \(pa, pb) => \s => 
        let (a, s1) = pa(s);
            (b, s2) = pb(s1)
        in ((a, b), s2)
pThenL: forall A. (Parser{A}, Parser{()}) -> Parser{A} =
    forall A. \(pa, pb) => 
        pMap{(A, ())}{A}(pThen{A}{()}(pa, pb))(\(a, ()) => a)
pThenR: forall A. (Parser{()}, Parser{A}) -> Parser{A} =
    forall A. \(pa, pb) => 
        pMap{((), A)}{A}(pThen{()}{A}(pa, pb))(\((), a) => a)
// parser tried in order
pTry: forall A. [Parser{A}] -> Parser{A} =
    forall A. \ps => case ps of 
        p :: rps => \s => (case () of
            () => p(s);
            () => pTry{A}(rps)(s));
        [] => pFail{A}("Out of alternatives")

// parses a single base-10 digit to an integer
pDigit: Parser{Int} =
    pTry{Int}(
        map{(String, Int)}{Parser{Int}}
            (\(d, v) => pMap{()}{Int}(pWord(d))(\() => &v)) 
            ([("0", 0), ("1", 1), ("2", 2), ("3", 3), ("4", 4), 
              ("5", 5), ("6", 6), ("7", 7), ("8", 8), ("9", 9)])
    )
// parses a sequence of digits base-10 into a single integer
pInt: Parser{Int} = pMap{[Int]}{Int}(pRep1{Int}(pDigit))(
    \ds => case ds of 
        [0] => 0;
        ds2 => fix(digits2Int: [Int] <=> Int = 
            \ds3 => case ds3 of
                [] => 0;
                append{Int}(rds, d) => muladd(10)(digits2Int(rds), d))(ds2)
        )

// parses an identifier
pIdent: Parser{String} = pMap{[[String]]}{String}(
    pSeq{[String]}([
        pMap{String}{[String]}(pChar("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"))(\s => [s]), 
        pRep{String}(pChar("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789"))
    ]))(let join = fix(join: [String] <=> String = \ss <=> case ss of
            [] => "";
            s :: rss => splitAt(1)~(s, join(rss)))
      in \[[s], ss] => splitAt(1)~(s, join(ss)))
// parses identifier-integer pairs seperated by comma ignoring spaces
pKeyValue: Parser{[(String, Int)]} = 
    pRepSep{(String, Int)}(
        pThen{String}{Int}(pIdent, pThenR{Int}(pWS(" "), pThenR{Int}(pWord("="), pThenR{Int}(pWS(" "), pInt))))
    )(pThenL{()}(pWS(""), pThenR{()}(pWord(","), pWS(" "))))

// filter function. where{A}(f)(x) returns x, but only if f(x) == True.
// otherwise it fails
where: forall A. (A -> Bool) -> A <=> A =
    forall A. \check => \a => 
        case &(check(a)) of
            &True => a
// absolute value
abs: Int <=> Int = \a => case a of
    where{Int}(\aa => aa >= 0)(aa) => aa;
    aa => aa * (0 - 1)
// example: integer multiplication defined using integer addition
mulFromAdd: Int -> Int <=> Int =
    \k => \x => case x of
        &0 => 
            let y = forget{Int}(0)~() in
            where{Int}(\yy => abs(yy) < k)(y);
        where{Int}(\xx => xx > 0 && k > 0)(xx) => 
            where{Int}(\yy => yy > 0 && k > 0)(mulFromAdd(k)(xx - 1) + k);
        where{Int}(\xx => xx > 0 && k < 0)(xx) => 
            where{Int}(\yy => yy < 0 && k < 0)(mulFromAdd(k)(xx - 1) + k);
        where{Int}(\xx => xx < 0 && k > 0)(xx) => 
            where{Int}(\yy => yy < 0 && k > 0)(mulFromAdd(0 - k)(xx * (0 - 1)));
        where{Int}(\xx => xx < 0 && k < 0)(xx) => 
            where{Int}(\yy => yy > 0 && k < 0)(mulFromAdd(0 - k)(xx * (0 - 1)))