-- $Id: FinFun.hs,v 1.7 1998/06/19 19:48:23 leavens Exp $

---------------------------------------
-- Finite Functions (Appendix E of the BeCecil Tome)
--
-- AUTHOR: Gary T. Leavens
---------------------------------------

module FinFun where

import List

-- some fundamental representation decisions
type Powerset a		= [a]            -- without duplicates

type FiniteFun a b	= Powerset (a,b)
type FiniteRel a b	= Powerset (a, b)
type Nat		= Integer

-- additional operations on sets

eqSet :: (Eq a) => Powerset a -> Powerset a -> Bool
eqSet s1 s2 = subseteq s1 s2 && subseteq s2 s1

subseteq :: (Eq a) => Powerset a -> Powerset a -> Bool
subseteq s1 s2 = all (\x -> x `elem` s2) s1

-- union all the sets in a set of sets
unionSet :: (Eq a) => Powerset(Powerset a) -> Powerset a
unionSet st = nub (foldr union [] st)

setProduct :: (Eq a, Eq b) => Powerset a -> Powerset b -> Powerset (a,b)
setProduct s1 s2 = unionSet (map (adjoin s1) s2)
	         where adjoin st e = map (\x -> (x,e)) st


-- Finite functions

dom :: Eq a => FiniteFun a b -> Powerset a
dom f = (nub [ a | (a,b) <- f ])

-- "range" is used elsewhere in the Haskell prelude, so we shorten it to ran
ran :: Eq b => FiniteFun a b -> Powerset b
ran f = (nub [ b | (a,b) <- f ])

graph :: FiniteFun a b -> Powerset (a,b)
graph f = f


-- Finite relations

maps :: (Eq a, Eq b) => FiniteRel a b -> a -> Powerset b
maps r a = (nub [ b | (x,b) <- r, x == a ])

isFunction :: (Eq a, Eq b) => FiniteRel a b -> Bool
isFunction r = (all (\a -> length (maps r a) == 1) (dom r))

apply :: (Eq a, Eq b) => FiniteRel a b -> a -> Maybe b
apply r a = let bs = (maps r a)
	     in if (length bs == 1) then (Just (head bs))
		else Nothing

toFun :: (Eq a, Eq b) => FiniteRel a b -> FiniteFun a b
toFun r = if (isFunction r) then r else (error "not a function")


-- other notation

update :: Eq a => FiniteFun a b -> a -> b -> FiniteFun a b
update f a b = ((a,b) : [(x,y) | (x,y) <- f, x /= a])

disjoint :: Eq a => FiniteFun a b -> FiniteFun a b -> Bool
disjoint f1 f2 = ((dom f1) `intersect` (dom f2)) == []

unionDot :: Eq a =>
             FiniteFun a b -> FiniteFun a b -> Maybe (FiniteFun a b)
f1 `unionDot` f2 = if (disjoint f1 f2) then (Just (f2 ++ f1))
                   else Nothing

unionMinus :: Eq a =>
               FiniteFun a b -> FiniteFun a b -> FiniteFun a b
f1 `unionMinus` f2 = f2 ++ [(x,y) | (x,y) <- f1, not (x `elem` dom_f2)]
		     where dom_f2 = (dom f2)

bind :: Eq a => [a] -> [b] -> Maybe (FiniteFun a b)
bind as bs = if (length as /= length bs)
	      then (error "bind called with lists of different lengths")
	      else (foldl unionDotUpdate (Just []) (zip as bs))
	    where unionDotUpdate mxys (x,y) =
			(case mxys of
			   Nothing -> Nothing
			   (Just xys) -> [(x,y)] `unionDot` xys)


-- colon notation
colon :: a -> b -> (a,b)
a `colon` b = (a,b)



-- Relations

addToRel :: (Eq a, Eq b) => FiniteRel a b -> a -> b -> FiniteRel a b
addToRel r a b = (a,b) : (r \\ [(a,b)])

composeRel :: (Eq a, Eq b, Eq c) => FiniteRel a b -> FiniteRel b c
				    -> FiniteRel a c
composeRel r1 r2 = nub (map outer (filter linked (noNubSetProduct r1 r2)))
         where linked ((a,b),(c,d)) = (b == c)
               outer  ((a,b),(c,d)) = (a,d)
	       -- the following are used to avoid more nubs than necessary
	       noNubSetProduct s1 s2 = noNubUnionSet (map (adjoin s1) s2)
	       adjoin st e = map (\x -> (x,e)) st
	       noNubUnionSet st = (foldr (++) [] st)

-- The transitiveClosure algorithm is adapted from Simon Thompson,
-- The Craft of Functional Programming, page 335 (and surrounding defs).
transitiveClosure :: Eq a => FiniteRel a a -> FiniteRel a a
transitiveClosure r =   -- REQUIRES: r has no duplicates (as the type says)
	limit addGen r
        where limit f x | (fastEqSet x next) = x
			| otherwise      = limit f next
			  where next = (f x)
              addGen rel = (rel `union` (composeRel rel r))
	      -- since s1 and s2 below have no duplicates, we can use this...
	      fastEqSet s1 s2 = (length s1 == length s2) && (subseteq s1 s2)

reflexiveClosure :: Eq a => FiniteRel a a -> FiniteRel a a
reflexiveClosure r =   -- REQUIRES: r has no duplicates (as the type says)
           -- we don't use dom below, to avoid an excess "nub" call
           -- note that union only removes duplicates from its 2nd argument
           r `union` [(a,a) | a <- (map fst r)]

reflexiveTransitiveClosure :: Eq a => FiniteRel a a -> FiniteRel a a
reflexiveTransitiveClosure r = reflexiveClosure (transitiveClosure r)

cyclic :: Eq a => FiniteRel a a -> Bool
cyclic r = (any (\a -> a `elem` (maps trans_r a)) (dom r))
	    where trans_r = (transitiveClosure r)

nonCyclicUnion :: Eq a => FiniteRel a a -> FiniteRel a a
			  -> Maybe (FiniteRel a a)
r1 `nonCyclicUnion` r2 = if (cyclic r1Ur2) then Nothing else (Just r1Ur2)
			 where r1Ur2 = (r1 `union` r2)