Filter
Top Products
Chapter 3
Further CAML
In this chapter, we consolidate the previous examples by specifying the basic facil-
ities of CAML and the syntax of phrases more precisely, and then go on to treat
some additional features such as recursive types. We might start by saying more
about interaction with the system.
So far, we have just been typing phrases into CAML’s toplevel read-eval-print
loop and observing the result. However this is not a good method for writing
nontrivial programs. Typically, you should write the expressions and declarations
in a file. To try things out as you go, they can be inserted in the CAML window
using ‘cut and paste’. This operation can be performed using X-windows and similar
systems, or in an editor like Emacs with multiple buffers. However, this becomes
laborious and time-consuming for large programs. Instead, you can use CAML’s
include function to read in the file directly. For example, if the file myprog.ml
contains:
let pythag x y z =
x * x + y * y = z * z;;
pythag 3 4 5;;
pythag 5 12 13;;
pythag 1 2 3;;
then the toplevel phrase include "myprog.ml";; results in:
#include "myprog.ml";;
pythag : int -> int -> int -> bool = <fun>
- : bool = true
- : bool = true
- : bool = false
- : unit = ()
That is, the CAML system responds just as if the phrases had been entered at
the top level. The final line is the result of evaluating the include expression itself.
HOL Light runs a filter in front of CAML to expand backquotes into calls of term
and type parser and typechecker. In order to make this happen when loading a file,
use loadt instead of include.
In large programs, it is often helpful to include comments. In CAML, these are
written between the symbols (* and *), e.g.
19