### Term matching

Extending one substitution with another can only work if the two substitutions are consistent with each other.

exception Term_match_exc let extend_subst s1 s2 = let f acc (x, t)= try let u = List.assoc x acc in if t = u then acc else raise Term_match_exc with Not_found -> (x, t)::acc in List.fold_left f s1 s2

A pattern match of a term

*u*by a term*t*is a substitution that transforms*t*into*u*. If*t*is a variable*s*then the substitution*(s, u)*is an obvious pattern match for example. More generally though, if*t*is of the form*f (t*, then_{1}, ..., t_{n})*u*must be of the form*f (u*;_{1}, ..., u_{n})- for each
*i*there must exist a match of*u*with_{i}*t*;_{i}

let term_match (t1, t2) = let rec term_match' subst = function | (Var v, t) -> extend_subst [v, t] subst | (t, Var v) -> raise Term_match_exc | (Term (f, l), Term (g, r)) -> if f = g then List.fold_left term_match' subst (List.combine l r) else raise Term_match_exc in term_match' [] (t1, t2)For example, a pattern match of

*h(y(z, k(x, s)))*and*h(y(l(m, n,o()), k(t(), u)))*is*{(x,t()),(z, l(m,n,o()), (s, u)}*.