:: SETVARIANTS prototype ::
#
(X⟿Y indicates that X is syntactic sugar for Y)
PATTERNS
p ::= `tag (variant w/o argument)
`tag p (variant with argument)
p & p (intersection)
p as x (capture) [ ⟿ p & x]
p | p (union)
(p, p) (pair)
[p; ...; p] (list)
p :: p (consed list)
[] (empty list)
() (unit)
fun (captures any function)
_ (wildcard)
x (capture variable)
b (boolean constant)
n (numeric constant)
EXPRESSIONS
e ::= \ p ... p . e (functions)
fun p ... p -> e
recfun f p ... p -> e (recursive functions)
function p -> e | ... | p -> e (functions by cases)
function | p -> e | ... | p -> e
recfunction f p -> e | ... | p -> e (recursive functions by cases)
recfunction f | p -> e | ... | p -> e
match e with p -> e | ... | p -> e (match)
match e with | p -> e | ... | p -> e
let p = e in e (let)
let f p ... p = e in e (let function)
let rec f p ... p = e in e (let recursive function)
e : {t1; ...; tn} (type annotation:
if e has type ti for all i
then this expression is given type
t1 & ... & tn)
if e then e else e (if then else)
e e (application)
`tag (variant w/o argument)
`tag e (variant with argument)
(e, e) (pair)
[] (empty list) [ ⟿ `Nil]
e :: e (consed list) [ ⟿ `Cons(e,e)]
[e;...; e] (list) [ ⟿ `Cons(e,...,`Cons(e,`Nil))]
() (unit)
b (boolean constant)
n (numeric constant)
x (variable)
p (primitive function)
PRIMITIVE FUNCTIONS (prefixed)
p ::= eq (equality)
not (Boolean negation)
and (Boolean conjunction)
or (Boolean disjunction)
succ (successor function)
add (integer sum)
sub (integer subtraction)
mul (integer multiplication)
div (integer division, fails if dividing by 0)
safe_div ("safe" integer division: 2nd argument must not be 0)
TOP LEVEL DEFINITIONS
e
let x = e
let x : {t; ...; t} = e ⟿ let x = (e : {t; ...; t})
let f p ... p = e ⟿ let f = fun p ... p -> e
let rec f p ... p = e ⟿ let f = recfun f p ... p -> e
let rec f = function ... ⟿ let f = recfunction f ...
TYPES
t ::= 'a (type variables)
Bool (booleans)
Int (arbitrary precision integers)
Caml_Int (integers)
b (singleton [booleans])
n (singleton [integers])
`unit (unit)
`Nil (empty list)
`Cons(t,t) (consed lists)
n--n (intervals of integers)
X (type recursion variable)
t WHERE X = t (recursive type)
t->t (functions)
(t,t) (products)
t|t (union)
t&t (intersection)
t\t (difference)
Empty (empty type)
Any (top type)
Arrow (all functions type) [⟿ Empty->Any]
[* NOTE: an 'a list is encoded as X where X = `Cons('a,X)|`Nil *]
INFO
Enter at the command prompt an expression or statement according to the grammar given below the editor (mostly a subset of OCaml) and end it with a carriage return (SHIFT+enter for a line feed).
You can also click on the examples below to insert them.
(examples from the ICFP 16 paper)
let id x = x
id `A
let f x = match x with `A -> true
f (id `A)
let id2 x = match x with `A | `B -> x
id2 `A
let f x = match id2 x with `A -> `B | y -> y
let g x = match x with `A -> id2 x | _ -> x
let f x = match x with | (`A, _) -> 1 | (`B, _) -> 2 | (_, `A) -> 3 | (_, `B) -> 4
let f = function | `A -> `B | x -> x
let f : { `A -> `B ; 'a\`A -> 'a\`A } = function
| `A -> `B
| x -> x
(example from the ICFP 17 paper)
let f : { true -> Int -> Int ; false -> Bool -> Bool } =
fun condition x ->
if condition then succ x else not x;;
(other examples)
let rec map f = function | [] -> [] | h::t -> (f h)::(map f t);;
map (\x.x);;
map (function `A -> `B | x -> x);;
map (function `A -> `B | x -> x)[`A ; `B ; `B ];;
map (function `A -> `B | x -> x)[`A ; `B ; true ; false ];;
let reverse l =
let rec reverse_aux acc = function
| [] -> acc
| h :: t -> reverse_aux (h :: acc) t
in reverse_aux [] l
reverse [true ; false ; true ; true ]
reverse [1 ; 2 ; 3 ]
reverse [1 ; 2 ; 42 ; 3]
map reverse;;
(* of type ('a list) list -> ('a list) list *)
let l1 = [1; 2; 4] in
let l2 = [ true; false; 3; (\x.x) ] in
map reverse [ l1; l2]
(* of type (( ('a->'a) | Bool | 1--4 ) list) list *)
let g = function
| (`A,`B) -> true
| (`B,`A) -> false;;
map g;;
let g : { (`A,`B) -> true ; (`B,`A) -> false} = function
| (`A,`B) -> true
| (`B,`A) -> false;;
map g;;