:: SETVARIANTS prototype ::

#

(X⟿Y indicates that X is syntactic sugar for Y)

PATTERNSp::= `tag(variant w/o argument) `tagp(variant with argument)p&p(intersection)pasx(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) EXPRESSIONSe::= \p...p.e(functions) funp...p->erecfunfp...p->e(recursive functions) functionp->e| ... |p->e(functions by cases) function |p->e| ... |p->erecfunctionfp->e| ... |p->e(recursive functions by cases) recfunctionf|p->e| ... |p->ematchewithp->e| ... |p->e(match) matchewith |p->e| ... |p->eletp=eine(let) letfp...p=eine(let function) let recfp...p=eine(let recursive function)(e: {t1; ...;tn}type annotation: ifehas typetifor allithen this expression is given typet1& ... &tn) ifetheneelsee(if then else)ee(application) `tag(variant w/o argument) `tage(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 DEFINITIONSeletx=elet⟿ letx: {t; ...;t} = ex= (e : {t; ...;t}) letfp...p=e⟿ letf= funp...p->elet recfp...p=e⟿ letf= recfunfp...p->elet recf= function ... ⟿ letf= recfunctionf... TYPESt::= '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)tWHEREX=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 listis encoded asX 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;;