7 Options, Pairs, and Characters
Liquid Shplait supports options, pairs, and characters. A predicate can test an option with is_none and is_some, which Liquid Shplait adds to Shplait’s built-in functions, and can take a pair apart with fst and snd:
fun try_div(n :: Int, d :: Int) :: {o :: Optionof(Int) | is_none(o) == (d == 0)}:
| none()
fun swap(p :: Int * Int) :: {q :: Int * Int | fst(q) == snd(p) && snd(q) == fst(p)}:
A match on an option knows which case it is in, so a function that needs a some can rule out the other case:
fun try_div(n :: Int, d :: Int) :: {o :: Optionof(Int) | is_none(o) == (d == 0)}:
| none()
fun content({o :: Optionof(Int) | is_some(o)}) :: Int:
match o
| none(): unreachable()
| some(v): v
content(try_div(7, 2)) // accepted
content(try_div(7, 0)) // rejected: try_div(7, 0) is none()
A predicate has no way to name the value inside a some by itself (because none() has no such value); it can compare the whole option instead, as in o == some(n).
What the checker knows about a string or a list is its length, and that is lost when the string or list is put in an option or a pair: in match some(s) | some(t): ..., the length of t is unknown.
A pair’s components are taken apart in a body with def values(x, y) = p. A predicate cannot refer to the components of a tuple of another size.
A character literal is written Char"a"; characters may be compared with == and !=.