We recall here some basic constructions about OCaml. Some good and more detailed references are
In order to edit OCaml files, you are strongly advised to use Emacs. There are better looking editors for OCaml, but you will have to use Emacs for Agda anyway, so that it is better to get used to it right now. Have a look at the shortcuts.
Declaring values:
let x = 2 * 3
Local declarations:
let x =
let y = 2 + 2 in
y * y
Commands:
let () =
print_endline "Hello, world!";
print_endline "Bye."
Defining functions:
let f x = 2 * x
With multiple arguments:
let f b x y =
if b then x else y
With a unit argument:
let f () =
print_endline
"Time since the beginning of execution: "
(string_of_float (Sys.time ()) ^ " seconds") ^
Recursive:
let rec fact n =
if n = 0 then 1 else n * (fact (n-1))
Mutually recursive:
let rec even n =
if n = 0 then true
else odd (n-1)
and odd n =
if n = 0 then false
else even (n-1)
Unnamed functions:
let twice f =
fun f x -> f (f x)) f (
Conditional branching:
let () =
print_endline (if Random.bool () then "true" else "false")
While loops:
let syracuse n =
let r = ref n in
while !r <> 1 do
if !r mod 2 = 0 then r := !r / 2
else r := 3 * !r + 1
done
The usual boolean operations are
Equality | = |
Inequality | <> |
Conjunction | && |
Disjunction | || |
Negation | not |
You should never use ==
or !=
to compare things.
A pair can be created with
3, "hello") (
A function taking a pair as argument
let fst (x, y) = x
The empty list
[]
A non-empty list
1; 2; 3] [
Appending an element:
let one_more l = 1::l
Length of a list:
let rec length =
match l with
0
| [] -> 1 + (length l) | x::l ->
See the documentation of the List module for (much) more.
Binary trees can be defined by
type 'a tree =
of 'a tree * 'a tree
| Node of 'a | Leaf
The maximal depth of a leaf is
let rec depth t =
match t with
max (depth t) (depth u)
| Node (t, u) -> 0 | Leaf _ ->
let () =
print_endline "hello!"
let () =
let r = ref 0 in
while !r < 10 do
print_int !r;
1;
r := !r + print_endline ""
done
The counter:
let count =
let r = ref 0 in
fun () ->
1;
r := !r + !r
An exception can be defined with:
exception My_exception
It can be raised by
let f () =
raise My_exception
It can be catched with
let test () =
try
f ();print_endline "not raised"
with
"raised" | My_exception ->
You can add tests in your code with
let () =
assert (fact 5 = 120)
A failed test will raise
Assert_failure (...)
Some types:
let x = 5;;
# val x : int = 5
let s = "hello";;
# val s : string = "hello"
let double x = 2 * x;;
# val double : int -> int = <fun>
let f () =
# print_endline "hello";;
val f : unit -> unit = <fun>
let f x =
# print_endline ("The argument is " ^ string_of_int x);;
val f : int -> unit = <fun>
let app f x = f x;;
# val app : ('a -> 'b) -> 'a -> 'b = <fun>
let fst (x, y) = x;;
# val fst : 'a * 'b -> 'a = <fun>
let rec map f l =
# match l with
| [] -> []
| x::l -> (f x)::(map f l);;val map : ('a -> 'b) -> 'a list -> 'b list = <fun>
An OCaml file prog.ml
can be compiled with
ocamlopt prog.ml -o prog
and the resulting program can be executed with
./prog