let is_var_term t =

match t with Id _ -> true | _ -> false

let unit_subst i t =

extend_subst i t (empty_subst ())

let rec compose_substs s1 s2 =

match s1 with

EmptySub -> s2

| ExtendedSub (i, t, s) -> ExtendedSub (i, t, compose_substs s s2)

let rec unify_term t u =

match t with

Id tid -> if (is_var_term u) ||

(not (List.mem tid (term_all_ids u))) then

Some (unit_subst tid u)

else

None

| _ -> match u with

Id _ -> unify_term u t

| Constant udat ->

(match t with

Constant tdat when tdat = udat -> Some (empty_subst ())

| _ -> None)

| App us -> (match t with

App ts -> unify_terms ts us

| _ -> None)

and unify_terms ts us =

match ts, us with

[], [] -> Some (empty_subst ())

| ([], _) -> None

| (_, []) -> None

| (t :: ts', u :: us') ->

let subst_car = unify_term t u in

match subst_car with

None -> None

| Some s -> let new_ts = subst_in_terms ts' s in

let new_us = subst_in_terms us' s in

let subst_cdr = unify_terms new_ts new_us in

match subst_cdr with

None -> None

| Some s' -> Some (compose_substs s s')

The occurs check is necessary, of course, to avoid infinity. I won't say more than that, to force people that arrive here looking for solutions to EOPL's exercises to think a little about it, at least.

And this concludes Chapter 2.

## No comments:

Post a Comment