The Metalanguage ML

Writing  complicated tactics requires a thorough knowledge of the ML  programming language [Gordon, Milner, & Wadsworth 79] and the information contained in chapter 9. It is an easy matter, however, to write simple tactics and to combine existing tactics with a minimal subset of ML. ML is a functional programming language with three important characteristics which make it a good language for expressing tactics:

1. ML has an extensible, polymorphic 

   type discipline with secure types. This allows type constraints on the arguments and results of functions to be expressed and enforced. For example, the result of a function may be constrained to be of type proof.

2. ML has a mechanism for raising and handling exceptions (or, in the terminology of ML, throwing and catching failures). This is a convenient way to incorporate backtracking into tactics.

3. ML is fully higher--order; functions are objects in the language. This allows tactics (which are functions) to be combined using combining forms called tacticals, all of which are written in ML.

In order to understand the example tactics presented below it is not necessary to know many of the details of ML. The following summarizes some of the more important and less obvious language constructs. Functions in ML  are defined as in

        let divides x y = ((x/y)*y = x);;

This function has type 

intintbool; that is, it maps integers to functions from integers to boolean values. There is also an explicit abstraction operator, , which stands for the more conventional . The previous function could have been defined as

        let divides = \ x . \ y  . ((x/y)*y = x);;

Exceptions  are raised using the expression `` fail'' and handled ( caught) using ``?''. The result of evaluating exp1?exp2 is the result of evaluating exp1 unless a failure is encountered, in which case it is the result of evaluating exp2. For example, the following function returns false if y = 0.

        let divides x y = (if y = 0 then fail
                          else (y*(x/y)=x)
                          ) ? false;;

In fact, because dividing by 0 causes a failure, we could define the same function with

        let divides x y = (y*(x/y)=x)?false;;