FoldSort.tla

FoldSort.tla

No annotation found for Frob$1. Make sure that you've put one in front of Frob$1. E@18:30:44.591

----- MODULE FoldSort -----
EXTENDS Integers, Sequences, Apalache


\* @type: (Seq(Int), (a => Bool)) => Seq(Int);
FilterSeq(seq, cmp(_)) ==
    LET \* @type: (Seq(Int), Int) => Seq(Int);
        Frob(acc, e) == IF cmp(e) THEN acc \o <<e>> ELSE acc
    IN FoldSeq(Frob, <<>>, seq)

\* @type: (Seq(Int), Int) => Seq(Int);
SortedSeq(sorted, e) == 
    LET \* @type: Int => Bool;
        Gt(a) == a > e
        \* @type: Int => Bool;
        Lt(a) == a < e
    IN FilterSeq(sorted, Lt) \o <<e>> \o FilterSeq(sorted, Gt)

\* @type: (Seq(Int), Seq(Int)) => Seq(Int);
Sort(s1, s2) ==
    FoldSeq(SortedSeq, <<>>, s1 \o s2)
    
=====