unify.ml

(* A possibly correct unification algorithm implementaion *)
open Printf

type term = F of string * (term list) | V of string

let rec subst subs = function
  | V x -> List.fold_left (fun acc (s, t) -> if x = s then t else V x) (V x) subs 
  | F (x, args) ->
    F (x, 
       List.map (fun arg -> subst subs arg) args)

(* Return true for X/X substitutions *)
let is_redundant x = function
  | V y -> x = y
  | _ -> false

let rec ssubst subs = function
  | [] -> subs
  | (x, t) :: tl -> 
    let (y, t') = (x, subst subs t) in
    if is_redundant y t'
    then ssubst subs tl
    else (y, t') :: ssubst subs tl

let rec show_term = function
  | V x -> x
  | F (x, []) -> x
  | F (x, l) -> sprintf "%s(%s)" x (show_args l)
and show_args = function
  | [] -> ""
  | [hd] -> show_term hd
  | hd :: tl -> sprintf "%s,%s" (show_term hd) (show_args tl)
let rec show_unifier_args = function
  | [] -> ""
  | [(x, t)] -> sprintf "%s -> %s" x (show_term t)
  | (x, t) :: tl -> sprintf "%s -> %s; %s" x (show_term t) (show_unifier_args tl)
let show_unifier u =
  sprintf "{%s}" (show_unifier_args u)

let (++) hd tl =
  match  List.find_opt (fun x -> x = hd) tl with
  | Some x -> tl
  | None -> hd :: tl

let rec unify t1 t2 acc =
  match t1, t2 with
  | F (x, _), F (y, _) when x <> y -> failwith ("conflict "^x^"<>"^y)
  | F (f1, args1), F (f2, args2) ->
    List.combine args1 args2
    |> List.fold_left
         (fun acc (arg1, arg2) -> unify arg1 arg2 acc)
         acc
  | F (_, _), V _ -> unify t2 t1 acc
  | V x, t ->
    let acc = ssubst [(x, t)] acc in
    (x, t) ++ acc 

let c x = F (x, [])
let f n l = F (n, l)

let () =
  let t1 = f "f" [V "X"; c "b"] in
  let t2 = f "f" [c "a"; c "b"] in
  let s = unify t1 t2 [] in
  show_unifier s |> print_endline;
  let t1 = f "f" [V "X"; c "b"] in
  let t2 = f "f" [c "a"; V "Y"] in
  let s = unify t1 t2 [] in
  show_unifier s |> print_endline;
  let t1 = f "f" [V "X"; V "Y"] in
  let t2 = f "f" [V "Y"; V "X"] in
  let s = unify t1 t2 [] in
  show_unifier s |> print_endline