Simple unification-fd test.

Lib.hs

{-# LANGUAGE DeriveTraversable #-}

module Lib where

import Control.Unification
import Control.Unification.IntVar
import Control.Unification.Types

import Control.Monad.Identity
import Control.Monad.Except

data TermF a = Term String [a]
    deriving (Eq, Foldable, Functor, Show, Traversable)

zipExact :: [a] -> [b] -> Maybe [(a, b)]
zipExact [] []         = Just []
zipExact (x:xs) (y:ys) = ((x, y) :) <$> zipExact xs ys
zipExact _ _           = Nothing

instance Unifiable TermF where
    zipMatch (Term t ts) (Term t' ts') =
        if t == t'
            then Term t . map Right <$> zipExact ts ts'
            else Nothing

type Term = UTerm TermF IntVar

atom :: String -> Term
atom t = UTerm $ Term t []

term :: String -> [Term] -> Term
term t ts = UTerm $ Term t ts

type Binding = IntBindingT TermF Identity

test :: ExceptT (UFailure TermF IntVar) Binding Term
test = do
    v <- UVar <$> lift freeVar
    let a = term "a"
    let b = atom "b"
    r <- unify (a [v, v, v]) (a [b, b, b])
    applyBindings r

main :: IO ()
main = print . runIdentity . evalIntBindingT . runExceptT $ test