inference.hs

module Inference where
-- |recursive subtyping inference program

import TypeUtils
import List (union, (\\), nub)
import Flatten (isTypeFlat,isSysFlat)
import Maybe(fromJust)

-- main function for analysis
uni :: Subst -> Subst
uni s =
	if (not $ isSysFlat s)
		then error "not a flat system"
		else
			clean $ unifyRec s s

-- combine the result on the whole system
unifyRec :: Subst -> Subst -> Subst
unifyRec [] _ = []
unifyRec (x:x1:xs) subst =
	let
		s0 = sys2rec x x1 subst
	in
		case s0 of
			Nothing -> 
				let s0 =  unifyRec (x1 : xs) subst
				in (x : s0)
			Just v -> unifyRec (x1 : xs) (subst `union` v)
-- case of one equation
unifyRec s subst = subst

-- helper function for recursive,
sys2rec :: (Type, Type) -> (Type, Type) -> Subst -> Maybe Subst
sys2rec (s1, s2 :-> s3) (t1, t2 :-> t3) subst = 
	recursive (s1,t1) subst [(s2,t2)] []
sys2rec (s1, s2) (t1, t2) subst = 
	recursive (s1,t2) subst [(s2,t2)] []

-- clean the output of unifyRec
clean :: Subst -> Subst
clean s =
	let s0 = nub s
	in filter (\x -> (fst x) /= (snd x)) s0

recursive :: (Type,Type) -> Subst -> Subst -> Subst -> Maybe Subst
recursive (t1,t2) subst o c = 
	if null o
		then Just c
		else
			let curr = o !! 0
			in 
				case (lookup t1 subst, lookup t2 subst) of
					(Just (x1 :-> x2), Just (y1 :-> y2)) ->
						let 
							onew = (o \\ [curr]) `union` ([(x1,y1),(x2,y2)] \\ c)
							cnew = c `union` [curr]
						in recursive curr subst onew cnew
					(Just x, Just y) ->
						if x == y
							then
								let
									onew = o \\ [curr]
									cnew = c `union` [curr]
								in recursive curr subst onew cnew
							else Nothing
					_ -> Nothing