Skip to content

Instantly share code, notes, and snippets.

@lemmy
Created March 5, 2022 18:32
Show Gist options
  • Save lemmy/22c7d1a3f463d38fb552d51b6c736dcb to your computer and use it in GitHub Desktop.
Save lemmy/22c7d1a3f463d38fb552d51b6c736dcb to your computer and use it in GitHub Desktop.
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)
=====
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment