Source

xilocaml / Unification.hs

Full commit
module Unification where
import Control.Monad.State
import ErrM
import TypeEnvironment
import PrettyShow


unify :: String -> UType -> UType -> EnvType UType
unify errorPrefix t1 t2 = do
		t1' <- convertPolyToTerm t1
		t2' <- convertPolyToTerm t2
		unifyImpl t1' t2'
	where
		unifyImpl t1 t2 = do
			t1 <- lookupType t1
			t2 <- lookupType t2
			case (t1,t2) of
				(t1', t2') | t1' == t2' -> return t1'
				(UTerm _, _) ->
					if occurs t1 t2 then
						failure "recursive types not supported"
					else
						assignType t1 t2
				(_, UTerm _) -> unifyImpl t2 t1
				(UList t1', UList t2') -> liftM UList $ unifyImpl t1' t2'
				(UFun t1' t1'', UFun t2' t2'') ->
					liftM2 UFun (unifyImpl t1' t2') (unifyImpl t1'' t2'')
				_ -> failure "conflicting types"
			where
				failure :: String -> EnvType UType
				failure message = lift $ Bad $ errorPrefix ++
					" Unification of " ++ (prettyShow t1) ++ " and " ++
					(prettyShow t2) ++ " failed: " ++ message ++ "."


occurs :: UType -> UType -> Bool
occurs term t = case t of
	UFun t1 t2 -> occurs term t1 || occurs term t2
	UList t' -> occurs term t'
	UTerm _ -> term == t
	_ -> False