----------------------------------------------------------------
-- examples
{-
Unification examples for the following three datatypes:
  - binary trees
  - cons lists
  - simple types 
-}
module Main where
import List(nub,intersperse)
import Unify
import Start

main = do print test1
          print test2
          print test3

test1 = testUnify ex1 :: (Bool, FuncSubst (VarTree Int))
test2 = testUnify ex2 :: (Bool, FuncSubst (VarList Char))
test3 = testUnify ex3 :: (Bool, FuncSubst (SimpleType String))

unifyList   :: (Term t,Subst s) => [(t,t)] -> Maybe (s t)
unifyList'  :: (Term t,Subst s) => [(t,t)] -> s t -> Maybe (s t)
unifyList ps = unifyList' ps idSubst
unifyList'   = threadList . map (uncurry unify') 

testUnify :: (Subst s, Term t, Eq t) => [(t,t)] -> (Bool,s t)
testUnify ex = (b,s) 
  where s = unJust (unifyList ex)
        b = all (uncurry (==)) (mapLP (appSubst s) ex)

----------------------------------------------------------------
type LP a = [(a,a)]
mapLP f = map (\(x,y) -> (f x, f y))
----------------------------------------------------------------
-- Unification on trees

ex1 :: LP (VarTree Int)
ex1 = [( (v 1 /\ l 3) /\     v 2 
       ,     v 3      /\ (l 5 /\ v 4)
       )
      ,(     v 2
       , l 5 /\ l 3
       )
      ,(     v 1     /\ (v 6 /\ l 6)
       ,(l 5 /\ l 4) /\ (l 7 /\ l 6)
       )
      ,(     v 1
       , l 5 /\ v 7
       )
      ]
  where v = VarTree
        (/\) = VBin
        l = VLeaf
----------------------------------------------------------------------
-- Unification on lists with variables

ex2 :: LP (VarList Char)
ex2 = [( 'a' & ('c' & v 1)
       , 'a' & v 2
       )
      ,( '2' & ('1' & VNil)
       , v 1
       )
      ]
  where (&) = VCons
        v   = VarList

----------------------------------------------------------------
-- Unification on type expressions

ex3 :: LP (SimpleType String)
ex3 = eqns eTwice

----------------------------------------------------------------
instance Eq a => Term (VarList a)
instance Eq a => Term (SimpleType a)
instance Eq a => Term (VarTree a)
--  Gofer variant:
-- instance (VarCheck t, TopEq t, Children t) => Term t

unJust (Just x) = x
----------------------------------------------------------------
-- end of essentials

----------------------------------------------------------------
-- Using the unifier as a type checker
-- The lambda calculus:
data Exp = Var String
         | Lam String Exp
         | Appl Exp Exp deriving (Eq, Show)

type Vari a = SimpleType a

-- Generate the type equations - one per subexpression
eqns :: Exp -> [(Vari a,SimpleType a)]
eqns e = eqns' (V . find (number (subTerms e))) e []

eqns' :: (Exp -> Vari a) -> Exp -> 
         [(Vari a,SimpleType a)]-> [(Vari a,SimpleType a)]
eqns' f p = case p of 
  (Var s)      -> id
  (Lam s e)    -> ((f p,Arrow (f (Var s)) (f e)):) . eqns' f e
  (Appl e e')  -> ((f e,Arrow (f e') (f p)):) . eqns' f e . eqns' f e'

-- Test expressions to be type checked
ePow n = Lam "f" (Lam "x" (body n))
  where body 0 = Var "x"
        body n = Appl (Var "f") (body (n-1))

eTwice = Lam "f" (Lam "x" (Appl (Var "f") (Appl (Var "f") (Var "x"))))
eomega = Lam "x" (Appl (Var "x") (Var "x"))
eK = Lam "x" (Lam "y" (Var "x"))
eS = Lam "x" 
      (Lam "y" 
        (Lam "z" 
          (Appl (Appl (Var "x") (Var "z"))
                 (Appl (Var "y") (Var "z"))
          )
        )
      )

typecheck :: Exp -> SimpleType ()
typecheck e = typecheck' (findtypesubst e)

typecheck' :: (Eq b, Subst a) => Maybe (a (SimpleType b)) -> SimpleType b
typecheck' Nothing  = error "type error"
typecheck' (Just s) = appSubst s (V 1)

findtypesubst :: Exp -> Maybe (FuncSubst (SimpleType ()))
findtypesubst e = unifyList (eqns e)

-- help functions
number :: Eq t => [t] -> [(t,Int)]
number l = zip (nub l) [1..]

find :: Eq a => [(a,b)] -> a -> b
find env key = head [b | (k,b) <- env, k==key]

instance Children Exp where
  children (Lam x e)   = [(Var x),e] -- special case for x
  children (Appl e e') = [e,e']
  children _           = []

----------------------------------------------------------------
showSubst :: (Subst s, Term a, Show a) => Maybe (s a) -> [a] -> String
showSubst x vs = unlines (map (show.appSubst (unJust x)) vs)

-- SimpleType
instance (Show a) => Show (SimpleType a) where
  showsPrec p (V i)      = showChar (toEnum (fromEnum 'a'+i))
  showsPrec p (TApp a ts)= showParen (p>=10) $
			     cmp (intersperse (showChar ' ') 
			           (map (showsPrec 10) ts))
  showsPrec p (Arrow l r)= showParen (p>=2)  
                             ( showsPrec 2 l 
                             . showString " -> " 
                             . showsPrec 1 r
                             )

instance Show t => Show (FuncSubst t) where
  showsPrec p (FSub s) = showsFSub 1 10 s
-- *** Gotyckligt val 1 och 10

showsFSub m n s = cmp (intersperse (showString ", ") 
                       [ shows i . showString " |-> " . shows t 
                       | (i,Just t) <- zip [m..n] (map s [m..n]) ])

cmp :: [a->a] -> (a->a)
cmp = foldr (.) id

instance Functor FuncSubst where
  fmap f (FSub s) = FSub (mapMaybe f . s)