Functional

Persistent functional operations used by the paper benchmark ports. All folds take the function, initial accumulator, then collection.
Imports
open Seq; open Maybe; open Pair;
Table of Contents

Functions

identity

def identity (x : a) : a

compose

def compose (f : (y : b) → c) (g : (x : a) → b) (x : a) : c

constant

def constant (x : a) (y : b) : a

flip

def flip (f : (x : a) → (y : b) → c) (y : b) (x : a) : c

foldl

def foldl (f : (acc : b) → (x : a) → b) (z : b) (xs : (Seq a)) : b

filter

def filter (p : (x : a) → Bool) (xs : (Seq a)) : (Seq a)

any

def any (p : (x : a) → Bool) (xs : (Seq a)) : Bool

take

def take (n : Int) (xs : (Seq a)) : (Seq a)

drop

def drop (n : Int) (xs : (Seq a)) : (Seq a)

takeWhile

def takeWhile (p : (x : a) → Bool) (xs : (Seq a)) : (Seq a)

dropWhile

def dropWhile (p : (x : a) → Bool) (xs : (Seq a)) : (Seq a)

concat

def concat (xss : (Seq (Seq a))) : (Seq a)

concatMap

def concatMap (f : (x : a) → (Seq b)) (xs : (Seq a)) : (Seq b)

head

def head (xs : (Seq a)) : (Maybe a)

last

def last (xs : (Seq a)) : (Maybe a)

nth

def nth (n : Int) (xs : (Seq a)) : (Maybe a)

zipWith

def zipWith (f : (x : a) → (y : b) → c) (xs : (Seq a)) (ys : (Seq b)) : (Seq c)

zip

def zip (xs : (Seq a)) (ys : (Seq b)) : (Seq (Pair a b))

replicate

def replicate (n : Int) (x : a) : (Seq a)

range

Half-open interval, including negative endpoints.
def range (lo : Int) (hi : Int) : (Seq Int)

scanl

def scanl (f : (acc : b) → (x : a) → b) (z : b) (xs : (Seq a)) : (Seq b)

equal

Equality is supplied explicitly, so these operations work on nested ADTs.
def equal (eq : (x : a) → (y : a) → Bool) (xs : (Seq a)) (ys : (Seq a)) : Bool

member

def member (eq : (x : a) → (y : a) → Bool) (x : a) (xs : (Seq a)) : Bool

unique

def unique (eq : (x : a) → (y : a) → Bool) (xs : (Seq a)) : (Seq a)

insertBy

def insertBy (le : (x : a) → (y : a) → Bool) (x : a) (xs : (Seq a)) : (Seq a)

sortBy

def sortBy (le : (x : a) → (y : a) → Bool) (xs : (Seq a)) : (Seq a)