Standard library

Every function below is written in Velaris, in stdlib/, and read onto this page by the compiler itself, contracts included. A violated requires is a compile error at your call site.

csv.vel #

fn csv.fields(line: Text) -> List of Text

ensures length(result) >= 1

fn csv.quoted_field(value: Text) -> Text

fn csv.line_of(values: List of Text) -> Text

fn csv.column(line: Text, at: Int) -> Text or fail

fn csv.column_int(line: Text, at: Int) -> Int or fail

fn csv.rows_of(text: Text) -> List of Text

ensures length(result) >= 1

dates.vel #

fn dates.days_in(year: Int, month: Int) -> Int

requires month >= 1

requires month <= 12

ensures result >= 28

ensures result <= 31

fn dates.make(year: Int, month: Int, day: Int) -> Date or fail

fn dates.parse(text: Text) -> Date or fail

fn dates.text_of(d: Date) -> Text

fn dates.before(a: Date, b: Date) -> Bool

fn dates.same(a: Date, b: Date) -> Bool

fn dates.next_day(d: Date) -> Date or fail

requires d.month >= 1

requires d.month <= 12

fn dates.today() -> Date or fail uses ffi

db.vel #

fn db.open(path: Text) -> Handle or fail uses ffi

fn db.run(conn: Handle, sql: Text) -> Text or fail uses ffi

fn db.commit(conn: Handle) or fail uses ffi

fn db.rows_json(conn: Handle, sql: Text) -> Text or fail uses ffi

fn db.count(conn: Handle, table: Text) -> Int or fail uses ffi

ensures result >= 0

fn db.close(conn: Handle) uses ffi

env_tools.vel #

fn env_tools.setting(name: Text, fallback: Text) -> Secret of Text uses env

fn env_tools.public_setting(name: Text, fallback: Text) -> Text uses declassify, env

fn env_tools.number_setting(name: Text, fallback: Int) -> Int uses declassify, env

fn env_tools.succeed() uses io

fn env_tools.give_up(why: Text) uses io

http.vel #

fn http.get(url: Text) -> Text or fail uses net

fn http.status(url: Text) -> Int or fail uses net

ensures result >= 0

fn http.ok(url: Text) -> Bool or fail uses net

fn http.send(url: Text, body: Text) -> Text or fail uses net

fn http.get_json(url: Text, path: Text) -> Text or fail uses net

fn http.call(method: Text, url: Text, body: Text, headers: Text) -> Answer or fail uses net

fn http.body_of(answer: Answer) -> Text

fn http.code_of(answer: Answer) -> Int

fn http.header_of(answer: Answer, name: Text) -> Text or fail

fn http.get_with(url: Text, headers: Text) -> Text or fail uses net

fn http.post_json(url: Text, body: Text) -> Text or fail uses net

log.vel #

fn log.info(message: Text) uses io

fn log.warn(message: Text) uses io

fn log.error(message: Text) uses io

fn log.field(name: Text, value: Text) -> Text

fn log.event(name: Text, details: Text) uses io

fn log.die(message: Text) uses io

fn log.fail_with(message: Text) uses io

money.vel #

fn money.not_negative(m: Money of C) -> Bool for any C

fn money.not_positive(m: Money of C) -> Bool for any C

fn money.split(amount: Money of C, ways: Int) -> List of Money of C for any C

requires ways > 0

ensures length(result) == ways

ensures units_of(result) == units_of(amount)

ensures units_of(amount) < 0 or all_of(result, not_negative)

ensures units_of(amount) > 0 or all_of(result, not_positive)

std.vel #

fn first(xs: List of T) -> T for any T

requires length(xs) > 0

fn last(xs: List of T) -> T for any T

requires length(xs) > 0

fn reverse(xs: List of T) -> List of T for any T

fn index_of(xs: List of T, item: T) -> Int for any T

fn contains_item(xs: List of T, item: T) -> Bool for any T

fn apply_to_each(xs: List of T, f: fn(T) -> T) -> List of T for any T

fn keep_if(xs: List of T, keep: fn(T) -> Bool) -> List of T for any T

fn count_where(xs: List of T, keep: fn(T) -> Bool) -> Int for any T

fn sum_of(xs: List of Int) -> Int

fn max_of(xs: List of Int) -> Int

requires length(xs) > 0

ensures contains_item(xs, result)

fn min_of(xs: List of Int) -> Int

requires length(xs) > 0

ensures contains_item(xs, result)

fn is_sorted(xs: List of Int) -> Bool

fn insert_sorted(xs: List of Int, v: Int) -> List of Int

fn sort(xs: List of Int) -> List of Int

ensures length(result) == length(xs)

ensures is_sorted(result)

fn insert_by(xs: List of T, v: T, key: fn(T) -> Int) -> List of T for any T

fn sort_by(xs: List of T, key: fn(T) -> Int) -> List of T for any T

ensures length(result) == length(xs)

fn join(xs: List of Text, sep: Text) -> Text

fn range_list(a: Int, b: Int) -> List of Int

fn map_to(xs: List of T, f: fn(T) -> R) -> List of R for any T, R

ensures length(result) == length(xs)

time.vel #

fn time.today() -> Text or fail uses ffi

fn time.clock_text() -> Text or fail uses ffi

fn time.seconds() -> Int uses clock

fn time.day_of(when: Text) -> Text or fail

fn time.year_of(date: Text) -> Int or fail

fn time.month_of(date: Text) -> Int or fail

fn time.day_number(date: Text) -> Int or fail

Built-in functions #

Name	Effects	Takes	Gives
`add_or_fail` or fail	pure	Int, Int	Int
`all_of`	pure	Any, Any	Bool
`any_of`	pure	Any, Any	Bool
`args`	io		List of Text
`ask`	io	Text	Text
`chars`	pure	Text	List of Text
`code_at`	pure	Text, Int	Int
`contains`	pure	Text, Text	Bool
`declassify`	declassify	Secret of T, Text	T
`div_or_fail` or fail	pure	Int, Int	Int
`divide_or_fail` or fail	pure	Money of C, Int, Text	Money of C
`env`	env	Text, Text	Secret of Text
`exit_with`	io	Int	Unit
`fetch` or fail	net	Text	Text
`fetch_status` or fail	net	Text	Int
`file_exists`	fs	Text	Bool
`format`	pure	Any	Text
`get`	pure	Any, Any	Any
`get_or`	pure	Any, Any, Any	Any
`has`	pure	Any, Any	Bool
`json_float` or fail	pure	Text, Text	Float
`json_get` or fail	pure	Text, Text	Text
`json_has`	pure	Text, Text	Bool
`json_int` or fail	pure	Text, Text	Int
`json_len` or fail	pure	Text, Text	Int
`json_of`	pure	Any	Text
`keys`	pure	Any	Any
`length`	pure	Any	Int
`log`	io	Any	Unit
`lower`	pure	Text	Text
`mod_or_fail` or fail	pure	Int, Int	Int
`money`	pure	Int, Text	Money of that currency
`mul_or_fail` or fail	pure	Int, Int	Int
`now`	clock		Int
`parse_money` or fail	pure	Text, Text	Money of that currency
`percent_of`	pure	Money of C, Int, Int, Text	Money of C
`pop` or fail	pure	Any	Any
`post` or fail	net	Text, Text	Text
`print`	io	Any	Unit
`push`	pure	Any, Any	Any
`put`	pure	Any, Any, Any	Any
`py` or fail	ffi	Text, Text, List of Text	Text
`py_close`	ffi	Handle	Unit
`py_do` or fail	ffi	Handle, Text, Text	Text
`py_field` or fail	ffi	Handle, Text	Text
`py_float` or fail	ffi	Text, Text, List of Text	Float
`py_int` or fail	ffi	Text, Text, List of Text	Int
`py_json` or fail	ffi	Text, Text, Text	Text
`py_new` or fail	ffi	Text, Text, Text	Handle
`random`	rand	Int	Int
`read_file` or fail	fs	Text	Text
`read_file_secret` or fail	fs	Text	Secret of Text
`read_line`	io		Text
`request` or fail	net	Text, Text, Text, Text	Text
`round`	pure	Float	Int
`set_at` or fail	pure	Any, Int, Any	Any
`slice` or fail	pure	Any, Int, Int	Any
`split`	pure	Text, Text	List of Text
`sub_or_fail` or fail	pure	Int, Int	Int
`text_of`	pure	Money of C	Text
`to_float`	pure	Int	Float
`to_int` or fail	pure	Text	Int
`to_text`	pure	Any	Text
`units_of`	pure	Money of C, or List of Money of C	Int
`upper`	pure	Text	Text
`with_units`	pure	Money of C, Int	Money of C
`write_file`	fs	Text, Any	Unit

get on a map can also fail (missing key); get_or never fails.