```{-# OPTIONS -Wall #-}
module Data.Logic.Harrison.Unif
( unify
, solve
, fullUnify
, unifyAndApply
) where

import Data.Logic.Classes.Term (Term(..), tsubst)
import Data.Logic.Failing (Failing(..), failing)
import qualified Data.Map as Map
{-
(* ========================================================================= *)
(* Unification for first order terms.                                        *)
(*                                                                           *)
(* Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)  *)
(* ========================================================================= *)

let rec istriv env x t =
match t with
Var y -> y = x or defined env y & istriv env x (apply env y)
| Fn(f,args) -> exists (istriv env x) args & failwith "cyclic";;
-}
isTrivial :: Term term v f => Map.Map v term -> v -> term -> Failing Bool
isTrivial env x t =
foldTerm v f t
where
v y =
if x == y
then Success True
else maybe (Success False) (isTrivial env x) (Map.lookup y env)
f _ args =
if any (failing (const False) id . isTrivial env x) args
then Failure ["cyclic"]
else Success False

{-
foldT (\ y -> y == x || (defined env y && istriv env x (apply env y)))
(\ _ args -> if any (istriv env x) args then error "cyclic" else False)
t
-}
{-

(* ------------------------------------------------------------------------- *)
(* Main unification procedure                                                *)
(* ------------------------------------------------------------------------- *)

let rec unify env eqs =
match eqs with
[] -> env
| (Fn(f,fargs),Fn(g,gargs))::oth ->
if f = g & length fargs = length gargs
then unify env (zip fargs gargs @ oth)
else failwith "impossible unification"
| (Var x,t)::oth | (t,Var x)::oth ->
if defined env x then unify env ((apply env x,t)::oth)
else unify (if istriv env x t then env else (x|->t) env) oth;;
-}
unify :: Term term v f => Map.Map v term -> [(term,term)] -> Failing (Map.Map v term)
unify env [] = Success env
unify env ((a,b):oth) =
foldTerm (vr b) (\ f fargs -> foldTerm (vr a) (fn f fargs) b) a
where
vr t x =
maybe (isTrivial env x t >>= \ trivial -> unify (if trivial then env else Map.insert x t env) oth)
(\ y -> unify env ((y, t) : oth))
(Map.lookup x env)
fn f fargs g gargs =
if f == g && length fargs == length gargs
then unify env (zip fargs gargs ++ oth)
else Failure ["impossible unification"]

{-
(* ------------------------------------------------------------------------- *)
(* Solve to obtain a single instantiation.                                   *)
(* ------------------------------------------------------------------------- *)

let rec solve env =
let env' = mapf (tsubst env) env in
if env' = env then env else solve env';;
-}
solve :: Term term v f => Map.Map v term -> Map.Map v term
solve env =
if env' == env then env else solve env'
where env' = Map.map (tsubst env) env
{-

(* ------------------------------------------------------------------------- *)
(* Unification reaching a final solved form (often this isn't needed).       *)
(* ------------------------------------------------------------------------- *)

let fullunify eqs = solve (unify undefined eqs);;
-}
fullUnify :: Term term v f => [(term,term)] -> Failing (Map.Map v term)
fullUnify eqs = failing Failure (Success . solve) (unify Map.empty eqs)
{-

(* ------------------------------------------------------------------------- *)
(* Examples.                                                                 *)
(* ------------------------------------------------------------------------- *)

let unify_and_apply eqs =
let i = fullunify eqs in
let apply (t1,t2) = tsubst i t1,tsubst i t2 in
map apply eqs;;
-}
unifyAndApply :: Term term v f => [(term, term)] -> Failing [(term, term)]
unifyAndApply eqs =
case fullUnify eqs of
Failure x -> Failure x
Success i -> Success (map (\ (t1, t2) -> (tsubst i t1, tsubst i t2)) eqs)
{-

START_INTERACTIVE;;
unify_and_apply [<<|f(x,g(y))|>>,<<|f(f(z),w)|>>];;

unify_and_apply [<<|f(x,y)|>>,<<|f(y,x)|>>];;

(****  unify_and_apply [<<|f(x,g(y))|>>,<<|f(y,x)|>>];; *****)

unify_and_apply [<<|x_0|>>,<<|f(x_1,x_1)|>>;
<<|x_1|>>,<<|f(x_2,x_2)|>>;
<<|x_2|>>,<<|f(x_3,x_3)|>>];;
END_INTERACTIVE;;
-}
```