4.1 Syntax

 < Free Open Study > 



4.1 Syntax

Our first job is to define a type of OCaml values representing terms. OCaml's datatype definition mechanism makes this easy: the following declaration is a straightforward transliteration of the grammar on page 24.

   type term =       TmTrue of info     | TmFalse of info     | TmIf of info * term * term * term     | TmZero of info     | TmSucc of info * term     | TmPred of info * term     | TmIsZero of info * term 

The constructors TmTrue to TmIsZero name the different sorts of nodes in the abstract syntax trees of type term; the type following of in each case specifies the number of subtrees that will be attached to that type of node.

Each abstract syntax tree node is annotated with a value of type info, which describes where (what character position in which source file) the node originated. This information is created by the parser when it scans the input file, and it is used by printing functions to indicate to the user where an error occurred. For purposes of understanding the basic algorithms of evaluation, typechecking, etc., this information could just as well be omitted; it is included here only so that readers who wish to experiment with the implementations themselves will see the code in exactly the same form as discussed in the book.

In the definition of the evaluation relation, we'll need to check whether a term is a numeric value:

   let rec isnumericval t = match t with       TmZero(_)  true     | TmSucc(_,t1)  isnumericval t1     | _  false 

This is a typical example of recursive definition by pattern matching in OCaml: isnumericval is defined as the function that, when applied to TmZero, returns true; when applied to TmSucc with subtree t1 makes a recursive call to check whether t1 is a numeric value; and when applied to any other term returns false. The underscores in some of the patterns are "don't care" entries that match anything in the term at that point; they are used in the first two clauses to ignore the info annotations and in the final clause to match any term whatsoever. The rec keyword tells the compiler that this is a recursive function definitioni.e., that the reference to isnumericval in its body refers to the function now being defined, rather than to some earlier binding with the same name.

Note that the ML code in the above definition has been "prettified" in some small ways during typesetting, both for ease of reading and for consistency with the lambda-calculus examples. For instance, we use a real arrow symbol () instead of the two-character sequence ->. A complete list of these prettifications can be found on the book's web site.

The function that checks whether a term is a value is similar:

   let rec isval t = match t with       TmTrue(_)   true     | TmFalse(_)  true     | t when isnumericval t  true     | _  false 

The third clause is a "conditional pattern": it matches any term t, but only so long as the boolean expression isnumericval t yields true.



 < Free Open Study > 



Types and Programming Languages
Types and Programming Languages
ISBN: 0262162091
EAN: 2147483647
Year: 2002
Pages: 262

flylib.com © 2008-2017.
If you may any questions please contact us: flylib@qtcs.net