Filter
Top Products
60 CHAPTER 6. IMPLEMENTATION IN CAML
#mk_abs(‘x:A‘,‘x:A‘);;
it : term = ‘\x. x‘
#mk_abs(it,it);;
Uncaught exception: Failure "mk_abs: not a variable"
There are now analogous destructor functions dest_var, dest_const, dest_comb
and dest_abs that act as inverses to the above. Strictly speaking dest_const is an
inverse to mk_mconst, since it returns the constant name and type, not the instan-
tiation list. Similarly, there are discriminator functions is_var, is_const, is_abs
and is_comb to test whether a term is in each class.
#dest_comb ‘~p‘;;
it : term * term = ‘(~)‘, ‘p‘
#dest_comb ‘\p. ~p‘;;
Uncaught exception: Failure "dest_comb: not a combination"
#dest_abs ‘\p. ~p‘;;
it : term * term = ‘p‘, ‘~p‘
#is_var ‘x:A‘;;
it : bool = true
#is_var ‘~p‘;;
it : bool = false
As well as the primitive syntax operations on terms, there are various derived
ones, which avoid the need to reduce everything right down to the basic opera-
tions above. For example, rator and rand (the names established lambda-calculus
jargon) take respectively the operator and operand of an application, i.e. return
respectively f and x when applied to a term f x. They can be implemented just
by applying dest comb to get a pair of terms, then applying the CAML functions
fst or snd:
#let rator tm = fst(dest_comb tm);;
rator : term -> term = <fun>
#let rand tm = snd(dest_comb tm);;
rand : term -> term = <fun>
#rand ‘SUC 2‘;;
it : term = ‘2‘
#rator ‘1 + 2‘;;
it : term = ‘(+) 1‘
#rand ‘1 + 2‘;;
it : term = ‘2‘
There are also derived functions to create, break apart and test for equations:
#dest_eq ‘x = 1‘;;
it : term * term = ‘x‘, ‘1‘
#is_eq ‘x = y + 3‘;;
it : bool = true
#is_eq ‘x <= y + 3‘;;
it : bool = false
#is_eq ‘p = q‘;;
it : bool = true
#mk_eq(‘T‘,‘F‘);;
it : term = ‘T = F‘
Similarly, when the other constants are defined, they often have a corresponding
set of functions to create, test, and destroy them. For example, mk imp creates an