--Michael Aiello
--Programming Languages FALL 2004
--Unification Project
--Basic and more extensive version (with nesting)

-----------------BEGIN CODE INCLUDED WITH THE PROJECT--------------

import Numeric(readDec); -- Shortcut for converting integers
import Char(isDigit);

-- Extended to allow nested lists 
data MyElement = MyNum Int | MyAtom String | MyNested [MyElement] deriving (Show, Eq)

{- Type for recording a binding: a pair consisting of a list of
   variables all to be bound to a common value, and the value itself,
   except that the value might be empty.  -}

type MyBinding = ([String],Maybe MyElement)  -- actually, should not
-- allow a MyAtom on the RHS of a binding
type MyBindings = [MyBinding]
type MySingleBinding = (String,Maybe MyElement)

-- primitive version, deals with two elements
unify2 :: MyElement -> MyElement -> MyBindings
unify2 (MyNum x) (MyNum y) 
  | x == y = []  -- no variable bindings
-- Next line for prettier error msgs only.
  | x /= y = error ("Unification: " ++ (show x) ++ "!=" ++ (show y))
-- If first num then atom or list, just swap them.
unify2 (MyNum x) y = unify2 y (MyNum x)
-- variable x is bound to value y
unify2 (MyAtom x) (MyNum y) = [([x],Just (MyNum y))]
unify2 (MyNested x) (MyNum y) -- Should probably print x nicer.
  = error ("Cannot unify number " ++ (show y) ++ " with list " ++ (show x))
unify2 (MyAtom x) (MyAtom y) 
-- binding a variable to itself is pretty useless, return empty binding
  | x == y = []
-- create a single binding that identifies x with y, no value is recorded.
  | x /= y = [([x,y],Nothing)]
-- list and atom, swap
unify2 (MyNested x) (MyAtom y) = unify2 (MyAtom y) (MyNested x) 
-- atom and list: BROKEN, should probably do a unify of y and the 
-- previous binding for x, if any.  Not possible in the current set
-- up, as unify2 carries no information about any other bindings.
-- So this processing has to be delayed to merge_bindings.
unify2 (MyAtom x) (MyNested y) = 
    [([x],Just (MyNested y))]
-- finally, list and list: hand over to the list unify function
unify2 (MyNested x) (MyNested y) = unify2lists x y 

-- Unify two lists of elements, or a list of pairs.
unify2lists :: [MyElement] -> [MyElement] -> MyBindings
unify_pairs :: [(MyElement,MyElement)] -> MyBindings

unify2lists x y  -- check that lists have equal lengths and reduce to unify_pairs 
  | length x == length y = unify_pairs (zip x y)
  | otherwise = error ("Unequal length lists " ++ (show x) ++ " and " ++ (show y))
  
-- nothing to do for an empty list, else handle the first pair,
-- handle the rest recursively, combine the bindings by merge_bindings
unify_pairs [] = []
unify_pairs ((x,y):rest) = merge_bindings (unify2 x y) (unify_pairs rest)


-------------------- Some stuff for nicety's sake -----------

-- A more convenient version of unify2 for interactive use, say in
-- HUGS,  as it does not take awkward MyElement type data as
-- parameters, but plain old strings and converts them via strToMyElement.
nice_unify2 :: String -> String -> MyBindings
nice_unify2 x y = unify2 (strToMyElement x) (strToMyElement y)

-- Conversion from String to MyElement.  Primitive.   Should be fixed.
-- Converts anything with a digit to an Int, treats any other string
-- as a variable name.
strToMyElement :: String -> MyElement
strToMyElement s@(firstchar:_)
-- Assumes it is an unsigned number, uses readDec from Numeric module
-- Does not check if readDec consumes the entire string
  | isDigit firstchar = MyNum (fst (head (Numeric.readDec s)))
-- Otherwise takes the whole thing as an Atom (string).  This is where
-- the extensions to more hairy objects is to be inserted.
-- MISSING: Needs to handle lists of MyElements.
-- Code of readList and relatives in the Prelude is a good place to
-- start. 
  | otherwise = MyAtom s
  
  
------------------END CODE INCLUDED WITH THE PROJECT----------------


------------------PROJECT CONTENT-----------------------------------

merge_bindings :: MyBindings -> MyBindings -> MyBindings
merge_bindings a [] = a
merge_bindings [] b = b
merge_bindings  ((a,aelm):at) ((b,belm):bt)
	| genericLength (intersect a b) == 0 = ((a,aelm):at) ++ ((b,belm):bt)
	| genericLength (intersect a b) /= 0 && ( aelm == belm || aelm == Nothing) = (( (union a b) ,belm):bt)
	| genericLength (intersect a b) /= 0 && ( belm == Nothing ) = (( (union a b) ,aelm):bt)
	| otherwise = error ("Can Not Unify " ++ (show a) ++ " to two different things!")


------------------Standard Haskell List Library Functions From------
------------------http://www.haskell.org/onlinereport/list.html-----

genericLength           :: (Integral a) => [b] -> a
genericLength []        =  0
genericLength (x:xs)    =  1 + genericLength xs

union                   :: Eq a => [a] -> [a] -> [a]
union                   =  unionBy (==)    

unionBy                 :: (a -> a -> Bool) -> [a] -> [a] -> [a]
unionBy eq xs ys        =  xs ++ deleteFirstsBy eq (nubBy eq ys) xs

deleteBy                :: (a -> a -> Bool) -> a -> [a] -> [a]
deleteBy eq x []        = []
deleteBy eq x (y:ys)    = if x `eq` y then ys else y : deleteBy eq x ys

deleteFirstsBy          :: (a -> a -> Bool) -> [a] -> [a] -> [a]
deleteFirstsBy eq       =  foldl (flip (deleteBy eq))


intersect               :: Eq a => [a] -> [a] -> [a]
intersect               =  intersectBy (==)
intersectBy             :: (a -> a -> Bool) -> [a] -> [a] -> [a]
intersectBy eq xs ys    =  [x | x <- xs, any (eq x) ys]

nub                     :: Eq a => [a] -> [a]
nub                     =  nubBy (==)

nubBy                   :: (a -> a -> Bool) -> [a] -> [a]
nubBy eq []             =  []
nubBy eq (x:xs)         =  x : nubBy eq (filter (\y -> not (eq x y)) xs)
------------------End Standard Haskell List Functions From-----------