module Language.Haskell.FreeTheorems.Variations.CounterExamples.Common.AlgCommon 
    (TermVar(..), Term(..), TypedVar, TermCont, Cont(..), TrackCont, M, Rule(..), History(..),
     trace, traceIOStart, traceIOFile, traceIO, traceSimplify, traceTemp,
     first, isFst, second, isSnd, listhead, isHead, fromJust, isFromJust, fromLeft, isFromLeft, fromRight, isFromRight,
     firstApp, isFstApp, secondApp, isSndApp, listheadApp, isHeadApp, fromJustApp, isFromJustApp, fromLeftApp, isFromLeftApp,
     fromRightApp, isFromRightApp,
     emptyCont, emptyTermCont, removeVar, removeVarStar, updateTVarStar, updateTVar, updateVar, updateVarStar,
     unpointed, isElementaryType, findfirstSpecialType, findfirstWithTVars, findallWithTVars,
     findfirst, findall,
     typeCheckArrowListArg, typeCheckArrowMaybeArg, typeCheckList, typeCheckMaybe, typeCheckArrowUnPointedArgPointedRes, typeCheckArrowArgArrow,
     typeCheckArrow, typeCheckInt, typeCheckBrace, typeCheckBool, typeCheckPair, typeCheckArrowPairArg,
     typeCheckArrowEitherArg, typeCheckEither, 
     insertArgument, subst, substAllInt, makePlusPair, makePlusElem, makeFuncPair, 
     initialiseTermCont, mergeTermCont,
     simplifyTerm, simplifyAppOnly, simplifyTermCont, simplifyTrackCont,
     insertTermsInTrackCont, applyTrackCont, assignTypeRelFuncs, getTypeRelFuncNamesNonStrict,
     showVarList, prependRelFunc, getTrackContWithFuncNames, showFuncNames, renumberVariables,
     getVarNums, renumberVars, mapDisRelFuncsToNames, showTermCont, printTermCont, showTermContList,
     printResult, printTyp, showCont, showTerm, showTermWithNames, showTyp, showTrackCont, showRawTrackCont,
     showTrackContApplication, showTrackContApplicationWithNames, getTrackContApplicationSolved, showTrackContApplicationSolved,
     showFuncNamesInt, makeTrackString, trackAll, trackRules) where


import Prelude hiding (Either(..))
import qualified Prelude as E (Either(..))
import Data.List
import qualified Data.Map as Map
import Control.Monad
import Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.M hiding (M)
import qualified Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.M as Mona (M)
import Language.Haskell.FreeTheorems.Variations.CounterExamples.Parser.ParseType
import Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.FTSync

-- * Debugging options
----------------------------------------------------------------------------------------------
--------------------------DEBUG-TOOLS---------------------------------------------------------
----------------------------------------------------------------------------------------------

import System.IO.Unsafe
-- |set debugging functions from the below list
trace :: String -> a -> a
trace = trace_ignore
--trace = trace_toShell

---- OutputFile options ----
-- |set file where debug output of traceIO is send to

--traceIOStart = traceIOStart_makeFile
traceIOStart = traceIOStart_ignore
traceIOFile = "./traceIO.log.hs"

---- traceIO settings ----
-- | trace informations on every rule, gives context and typ before and after rule application
-- exception: Bottom and Var*
traceIO :: String -> Typ -> Cont -> Typ -> Cont -> a -> a
traceIO = traceIO_ignore
--traceIO = traceIO_ordDiff
--traceIO = traceIO_ord2shell
--traceIO = traceIO_checkOrderInc
--traceIO = traceIO_cont2shell
--traceIO = \rule tauIn gammaIn tauOut gammaOut -> (traceIO_order2shell rule tauIn gammaIn tauOut gammaOut).traceIO_checkOrderInc rule tauIn gammaIn tauOut gammaOut

-- |some more special purpose trace functions
--traceSimplify = trace_toShell
traceSimplify = trace_ignore
traceTemp = trace_toShell

---- show settings ---
-- |show settings for the trace functions
showContTrace = showCont


---- trace functions ----
-- |trace functions

---- output file variants ----
traceIOStart_ignore file a = a
traceIOStart_makeFile file a = if unsafePerformIO (writeFile traceIOFile "traceIO-File\n\n") == () then a else a

---- trace and traceIO variants ----
trace_ignore str a = a
trace_toShell str a = if unsafePerformIO (putStr (str++"\n")) == () then a else a

traceIO_ignore rule tauIn gammaIn tauOut gammaOut a = a
traceIO_order2shell rule tauIn gammaIn tauOut gammaOut a = 
    if unsafePerformIO (putStr (rule ++ ":\t" ++ (show (count gammaOut tauOut)) ++ "\n")) == () then a else a
traceIOOutPut rule tauIn gammaIn tauOut gammaOut ordDiff =
    unsafePerformIO (appendFile traceIOFile (rule ++ ":\n\tIN  Type: " ++ (showTyp tauIn) ++ "\n\tIN  Cont: " ++ (showContTrace gammaIn) ++ "\n\tOUT Type: " ++ (showTyp tauOut) ++ "\n\tOUT Cont: " ++ (showContTrace gammaOut) ++"\n\tOrder Difference: " ++ (show ordDiff) ++ "\n"))

--traceIO variants
--outputs a file with input and output types, contexts and the orderdifference (out - in) for every rule applied
traceIO_ordDiff rule tauIn gammaIn tauOut gammaOut a = 
    let (ordIn,ordOut) = makeSameLength (count gammaIn tauIn) (count gammaOut tauOut)
        ordDiff = zipWith (-) ordOut ordIn
	good = firstNegative ordDiff
    in
    if (if traceIOOutPut rule tauIn gammaIn tauOut gammaOut ordDiff == () then good else good)
    then a
    else error ("Order increased by Rule " ++ rule ++ "\n\tInput Type: " ++ (showTyp tauIn) ++ "\n\tInput Cont: " ++ (show gammaIn) ++ "\n\tOutPut Type: " ++ (showTyp tauOut) ++ "\n\tOutput Cont: " ++ (show gammaOut) ++ "\n" ++ "OrderDifference: " ++ (show ordDiff)) 

--outputs pairs of input order ander output order to the shell
traceIO_ord2shell rule tauIn gammaIn tauOut gammaOut a =
    let (ordIn,ordOut) = makeSameLength (count gammaIn tauIn) (count gammaOut tauOut) in
    if unsafePerformIO (putStr ((show ordIn) ++ "\n" ++ (show ordOut) ++ "\n\n")) == () then a else a

--outputs context before and after rule application to the shell
traceIO_cont2shell rule tauIn gammaIn tauOut gammaOut a =
    if unsafePerformIO (putStr (rule ++ ":\n" ++ (showContTrace gammaIn) ++ "\n" ++ (showContTrace gammaOut) ++ "\n\n")) == () then a else a

--stay calm until order increases during a rule and then throw an error
traceIO_checkOrderInc rule tauIn gammaIn tauOut gammaOut a =
    let (ordIn,ordOut) = makeSameLength (count gammaIn tauIn) (count gammaOut tauOut) 
	ordDiff = zipWith (-) ordOut ordIn in
    if firstNegative ordDiff
    then a
    else error ("Order increased by Rule " ++ rule ++ "\n\tInput Type: " ++ (showTyp tauIn) ++ "\n\tInput Cont: " ++ (show gammaIn) ++ "\n\tOutPut Type: " ++ (showTyp tauOut) ++ "\n\tOutput Cont: " ++ (show gammaOut) ++ "\n" ++ "OrderDifference: " ++ (show ordDiff))

-- |helpfunctions for the order check
zeros = 0:zeros

updateAt l idx elem = (take idx l) ++ (elem:(drop (idx+1) l))

getAt l idx = head (drop idx l)

makeSameLength l1 l2 = let len1 = length l1
			   len2 = length l2 in
                       if len1 < len2 
		       then (prependZeros len2 l1,l2)
		       else (l1,prependZeros len1 l2)
  where prependZeros len l = if length l < len
			     then prependZeros len (0:l)
			     else l

count gamma tau = let (l1,l2) = makeSameLength (countCont gamma) ((countTyp tau) ++ [0]) in
	          zipWith (+) l1 l2

countCont :: Cont -> [Int]
countCont gamma = 
    let varlist = ((vars gamma) ++ (varsStar gamma)) in
    (countCont' varlist) ++ [(length varlist)]

countCont' vl = 
    case vl of
    []   -> [0,0,0,0,0]
    x:xs -> let (l1,l2) = makeSameLength (countCont' xs) (countTyp (snd x)) in
            zipWith (+) l1 l2

countTyp :: Typ -> [Int]
countTyp tau = let (d,el,ol) = countTyp' tau 0 in
	       (reverse (take (d+1) el)) ++ ol
 
--           tau    depth eitherlist (maxdepth,(eitherlist,orderlist)) --lists and maybe are counted together.
countTyp' :: Typ -> Int -> (Int,[Int],[Int])
countTyp' tau depth = 
    case tau of
    TVar _            -> (depth,zeros,[0,0,0,0])
    Arrow tau1 tau2   -> let (d1,el1,ol1) = countTyp' tau1 (depth+1)
			     (d2,el2,ol2) = countTyp' tau2 (d1+1) in
			 (max d1 d2, zipWith (+) el1 el2, zipWith (+) (zipWith (+) [0,0,0,1] ol1) ol2)
    All _ tau1        -> let (d,el,ol) = countTyp' tau1 (depth+1) in
			 (d,el,zipWith (+) [1,0,0,0] ol)
    AllStar _ tau1    -> let (d,el,ol) = countTyp' tau1 (depth+1) in
			 (d,el,zipWith (+) [1,0,0,0] ol)
    List tau1         -> let (d,el,ol) = countTyp' tau1 (depth+1) in
			 (d,el,zipWith (+) [0,0,1,0] ol)
    Int               -> (depth,zeros,[0,0,0,0])
    TBrace            -> (depth,zeros,[0,0,0,0])
    TBool             -> (depth,zeros,[0,0,0,0])
    TPair tau1 tau2   -> let (d1,el1,ol1) = countTyp' tau1 (depth+1)
			     (d2,el2,ol2) = countTyp' tau2 (d1+1) in
			 (max d1 d2,zipWith (+) el1 el2, zipWith (+) (zipWith (+) [0,1,0,0] ol1) ol2)
    TEither tau1 tau2 -> let (d1,el1,ol1) = countTyp' tau1 (depth+1)
			     (d2,el2,ol2) = countTyp' tau2 (depth+1) in
			 (max d1 d2,zipWith (+) (updateAt el1 depth ((getAt el1 depth)+1)) el2, zipWith (+) ol1 ol2)
    TMaybe tau1       -> let (d,el,ol) = countTyp' tau1 (depth+1) in
			 (d,el,zipWith (+) [0,0,1,0] ol)

firstNegative l = case l of
	          [] -> False
		  x:xs -> if x == 0 then firstNegative xs
			  else (if x < 0 then True else False) 


----------------------------------------------------------------------------------------------
--------------------------END: DEBUG-TOOLS----------------------------------------------------
----------------------------------------------------------------------------------------------

-- *Data type declarations

-- |Termvariable is taken to be a number. Monad M will keep track of the numbering when new
--  Termvariables are produced.
newtype TermVar = TermVar Int deriving (Show, Eq, Ord)

-- |Syntax of the terms used in the algorithm. The term set is a bit smaller than the whole
--  set of PolyFix*, because Case statements are restricted to make only the kinds used in
--  the algorithm possible.
data Term = Var TermVar   
	  | Abs    TermVar Typ     Term
	  | App    Term    Term
	  | TAbs   TypVar  Term
	  | Nil     Typ
	  | Cons    Term   Term 
	  -- |Case statement for lists
          --  Case l v t1 <==> Case l of {[] => _|_; v:_ => t1}
	  | LCase   Term   TermVar Term
	  | Bottom  Typ               -- statt Fix
          | Brace 
          -- |integer case-statement
          -- ICase t0 t1 <==> Case t0 of {0 => t1; _ => _|_}
	  | ICase   Term   Term
	  -- |brace case-statement
          -- BCase t0 t1 <==> Case t0 of {() => t1}
	  | BCase   Term   Term 
	  -- |bool case-statement
	  -- BoolCase t0 t1 <==> Case t0 of {False => t1; _ => _|_}
	  | BoolCase Term  Term
	  | Fls
	  | Zero
	  | Pair    Term   Term
          -- |case-statement for pairs
          -- PCase p v1 v2 t <==> Case p of {(v1,v2) ==> t}
	  | PCase   Term   TermVar TermVar Term
          -- |case-statement for either
          -- ECase e v1 t1 v2 t2 <==> Case e of {Left(v1) => t1; Right(v2) => t2}
	  | ECase   Term   TermVar Term    TermVar Term
	  | Right   Term
	  | Left    Term
	  -- Terms of TMaybe
	  | MJust   Term
--          | MNothing
          | MCase   Term   TermVar Term
	  deriving (Show, Eq)

-- |abbreviation for the pair (TermVar,Typ)
type TypedVar = (TermVar,Typ)

-- |represents the sigma environments sigma_1 and sigma^+_2. sigma_2 is not tracked.
type TermCont = Map.Map TermVar ((Term,Term),History)

-- |representation of \Gamma and \Sigma, both devided in a stared and unstared part,
--  as necessary regarding an \internalinput.
data Cont = Cont { tVars :: [TypVar], tVarsStar :: [TypVar], vars :: [TypedVar], varsStar :: [TypedVar] } deriving (Show,Eq)

-- |the list of the disrelater. The type has not to be tracked, because it is always clear.
type TrackCont = (Typ,[(Term,Term)])

type M = Mona.M Term

-- we introduce just the rules needed -> where term variables are produced in a non trivial way.
-- if the stared and the unstared variant are equal in historical behaviour, we introduce just the unstared one.
data Rule = WrapTo | MaybeTo | Head | RJust | PairTo | Proj | EitherTo | BottomToStripe | ArrowToStar | Dist1 | Dist2 |BottomTo deriving(Show,Eq)
data History = Branch Rule History | Split Rule History History | Leaf deriving(Show)

-- | some abbreviations for special functions.
-- They are used in the paper as well

-- |\p -> Case p of {(v1,v2) ==> v1}
first :: Typ -> M Term
first tau= do {i<-newInt;
	       j<-newInt;
               k<-newInt;
	       let x = TermVar i
                   y = TermVar j
                   p = TermVar k in
	       return (Abs p tau (PCase (Var p) x y (Var x)))
	      }

-- |Check if a term t is of form "fst"
isFst :: Term -> Bool
isFst t =
    case t of
      Abs _ _ (PCase _ x _ t1) ->
	  if Var x == t1 then True else False
      _                        -> False

-- |\p -> Case p of {(v1,v2) ==> v2}
second :: Typ -> M Term
second tau = do {i<-newInt;
		 j<-newInt;
		 k<-newInt;
		 let x = TermVar i
	             y = TermVar j 
		     p = TermVar k in
	       return (Abs p tau (PCase (Var p) x y (Var y)))
	      }

-- |Check if a term t is of form "snd"
isSnd :: Term -> Bool
isSnd t =
    case t of
      Abs _ _ (PCase _ _ y t1) -> 
	  if Var y == t1 then True else False
      _                        -> False

-- |\l -> Case l of {[] => _|_; x:_ => x}
listhead :: Typ -> M Term
listhead tau = do {i<-newInt;
		   j<-newInt;
		   let x = TermVar i
		       l = TermVar j in
		     return (Abs l (List tau) (LCase (Var l) x (Var x)))
		    }

-- |Check if a term t is of form "head"
isHead :: Term -> Bool
isHead t =
    case t of
      Abs _ _ (LCase _ v t2) -> 
	  if Var v == t2 then True else False
      _                      -> False

-- |\l -> Case l of {Just x => x}
fromJust :: Typ -> M Term
fromJust tau = do {i<-newInt;
		   j<-newInt;
		   let x = TermVar i
		       l = TermVar j in
		     return (Abs l (TMaybe tau) (MCase (Var l) x (Var x)))
		    }

-- |Check if a term t is of form "fromJust"
isFromJust :: Term -> Bool
isFromJust t =
    case t of
      Abs _ _ (MCase _ v t2) -> 
	  if Var v == t2 then True else False
      _                      -> False

-- |\e -> Case e of {Left x => x; Right x => _|_}
fromLeft :: Typ -> Typ -> M Term
fromLeft tau tau' = do {i<-newInt;
			j<-newInt;
			k<-newInt;
		     let x = TermVar i
		         y = TermVar j 
			 e = TermVar k in
		     return (Abs e (TEither tau tau') (ECase (Var e) x (Var x) y (Bottom tau)))
		    }

-- |Check if a term t is of form "fromLeft"
isFromLeft :: Term -> Bool
isFromLeft t =
    case t of
      Abs _ _ (ECase _ v1 t1 _ t2) -> 
	  if Var v1 == t1 
	  then case t2 of
                 Bottom _ -> True
                 _        -> False
	  else False
      _                            -> False

-- |\e -> Case e of {Left x => _|_; Right x => x}
fromRight :: Typ -> Typ -> M Term
fromRight tau tau' = do {i<-newInt;
			 j<-newInt;
			 k<-newInt;
			 let x = TermVar i
		             y = TermVar j
			     e = TermVar k in
		      return (Abs e (TEither tau tau') (ECase (Var e) x (Bottom tau') y (Var y)))
		     }

-- |Check if a term t is of form "fromRight"
isFromRight :: Term -> Bool
isFromRight t =
    case t of
      Abs _ _ (ECase _ _ t1 v2 t2) -> 
	  if Var v2 == t2 
	  then case t1 of
                 Bottom _ -> True
                 _        -> False
	  else False
      _                            -> False


-- | some abbreviations for special cases of the Case-statements.
-- They are used in the paper as well

-- |Case p of {(v1,v2) ==> v1}
firstApp :: Term -> M Term
firstApp p = do {i<-newInt;
		 j<-newInt;
		 let x = TermVar i
	             y = TermVar j in
		 return (PCase p x y (Var x))
		}

-- |Check if a term t is of form "fst t'"
isFstApp :: Term -> Bool
isFstApp t =
    case t of
      PCase _ x _ t1 -> if Var x == t1 then True else False
      _              -> False

-- |Case p of {(v1,v2) ==> v2}
secondApp :: Term -> M Term
secondApp p = do {i<-newInt;
		  j<-newInt;
		  let x = TermVar i
	              y = TermVar j in
		  return (PCase p x y (Var y))
		 }

-- |Check if a term t is of form "snd t'"
isSndApp :: Term -> Bool
isSndApp t =
    case t of
      PCase _ _ y t1 -> if Var y == t1 then True else False
      _              -> False

-- |Case l of {[] => _|_; x:_ => x}
listheadApp :: Term -> Typ -> M Term
listheadApp l tau = do {i<-newInt;
			let x = TermVar i in
			return (LCase l x (Var x))
		       }

-- |Check if a term t is of form "head t'"
isHeadApp :: Term -> Bool
isHeadApp t =
    case t of
      LCase _ v t2 -> if Var v == t2 then True else False
      _            -> False

-- |Case l of {Just x => x}
fromJustApp :: Term -> Typ -> M Term
fromJustApp l tau = do {i<-newInt;
			let x = TermVar i in
			return (MCase l x (Var x))
		       }

-- |Check if a term t is of form "fromJust t'"
isFromJustApp :: Term -> Bool
isFromJustApp t =
    case t of
      MCase _ v t2 -> if Var v == t2 then True else False
      _            -> False

-- |Case e of {Left x => x; Right x => _|_}
fromLeftApp :: Term -> Typ -> M Term
fromLeftApp e tau = do {i<-newInt;
			j<-newInt;
			let x = TermVar i
		            y = TermVar j in
			return (ECase e x (Var x) y (Bottom tau))
		       }

-- |Check if a term t is of form "fromLeft t'"
isFromLeftApp :: Term -> Bool
isFromLeftApp t =
    case t of
      ECase _ v1 t1 _ t2 -> if Var v1 == t1 
			    then case t2 of
                                   Bottom _ -> True
                                   _        -> False
			    else False
      _                  -> False

-- |Case e of {Left x => _|_; Right x => x}
fromRightApp :: Term -> Typ -> M Term
fromRightApp e tau = do {i<-newInt;
			 j<-newInt;
			 let x = TermVar i
		             y = TermVar j in
			 return (ECase e x (Bottom tau) y (Var y))
			}

-- |Check if a term t is of form "fromLeft t'"
isFromRightApp :: Term -> Bool
isFromRightApp t =
    case t of
      ECase _ _ t1 v2 t2 -> if Var v2 == t2 
			    then case t1 of
                                   Bottom _ -> True
                                   _        -> False
			    else False
      _                  -> False


-- *global constants

-- |global constant: the empty context \Gamma;\Sigma
emptyCont :: Cont
emptyCont = Cont [] [] [] []

-- |global constant: the empty term environments
emptyTermCont :: TermCont
emptyTermCont = Map.empty

-- *Context update functions

updateTVarStar (Cont tVars tVarsStar vars varsStar) tv = Cont tVars (tv:tVarsStar) vars varsStar

updateTVar (Cont tVars tVarsStar vars varsStar) tv = Cont (tv:tVars) tVarsStar vars varsStar

updateVar (Cont tVars tVarsStar vars varsStar) v tau = Cont tVars tVarsStar ((v,tau):vars) varsStar
removeVar (Cont tVars tVarsStar vars varsStar) var = Cont tVars tVarsStar (filter ((/= var).fst) vars) varsStar

updateVarStar (Cont tVars tVarsStar vars varsStar) v tau = Cont tVars tVarsStar vars  ((v,tau):varsStar)
removeVarStar (Cont tVars tVarsStar vars varsStar) var = Cont tVars tVarsStar vars  (filter ((/= var).fst) varsStar)


-- |check for pointedness.
--  the function implements the class membership rules for PolyFix*
unpointed :: [TypVar] -> Typ -> Bool
unpointed tvars tau = case tau of
                      TVar tvar      -> case find (== tvar) tvars of
                                          Nothing -> False
                                          _       -> True
                      Arrow _ tau'   -> unpointed tvars tau'
                      All tvar tau'  -> unpointed (tvar:tvars) tau'
                      AllStar _ tau' -> unpointed tvars tau'
                      List _         -> False
		      Int            -> False
                      TPair _ _      -> False
                      TEither _ _    -> False
                      TBool          -> False
                      TBrace         -> False
		      TMaybe _       -> False

isElementaryType :: Typ -> Bool
isElementaryType tau =
    case tau of
    Int    -> True
    TVar _ -> True
    TBrace -> True
    TBool  -> True
    _      -> False

-- *check functions for special typed variables in the term variable part of the context Cont
-- they usually take just one part of the context, i.e. a list [TypedVar]

-- |searches for a variable of type typ in vars

findfirstSpecialType :: [TypedVar] -> Typ -> Maybe TypedVar
findfirstSpecialType vars typ =
    case vars of
      []     -> Nothing
      (x:xs) -> if snd x == typ
		then Just x
		else findfirstSpecialType xs typ

-- |returns the first entry of vars, whose type passes the typecheckfunction
--  It uses the type variables for pointed checks
findfirstWithTVars :: ([TypVar] -> Typ -> Bool) -> [TypVar] -> [TypedVar] -> Maybe TypedVar
findfirstWithTVars typecheckfunction tvars vars =
    case vars of
      []     -> Nothing
      (x:xs) -> if typecheckfunction tvars (snd x)
		then Just x 
		else findfirstWithTVars typecheckfunction tvars xs

-- |returns the list of all entries of vars, whose types pass the typecheckfunction
--  It uses the type variables for pointed checks
findallWithTVars :: ([TypVar] -> Typ -> Bool) -> [TypVar] -> [(TypedVar)] -> [TypedVar]
findallWithTVars typecheckfunction tvars vars = 
    case vars of
      []     -> []
      (x:xs) -> if typecheckfunction tvars (snd x)
		then (x:(findallWithTVars typecheckfunction tvars xs))
		else findallWithTVars typecheckfunction tvars xs

-- |returns the first entry of vars, whose type passes the typecheckfunction
findfirst :: (Typ -> Bool) -> [TypedVar] -> Maybe TypedVar 
findfirst typecheckfunction vars = case vars of
                                     []     -> Nothing
                                     (x:xs) -> if typecheckfunction (snd x) 
               				       then Just x 
				               else findfirst typecheckfunction xs

-- |returns the list of all entries of vars, whose types pass the typecheckfunction
findall :: (Typ -> Bool) -> [TypedVar] -> [TypedVar]
findall typecheckfunction vars = case vars of
                                   []     -> []
                                   (x:xs) -> if typecheckfunction (snd x)
					     then (x:(findall typecheckfunction xs))
			                     else findall typecheckfunction xs

-- ** typecheckfunctions

-- | used for (Wrap->)
typeCheckArrowListArg :: Typ -> Bool
typeCheckArrowListArg tau = case tau of
                              Arrow tau1 _ -> case tau1 of
                                                List _ -> True
                                                _      -> False
			      _            -> False

-- | used for (MaybeWrap->)
typeCheckArrowMaybeArg :: Typ -> Bool
typeCheckArrowMaybeArg tau = case tau of
                              Arrow tau1 _ -> case tau1 of
                                                TMaybe _ -> True
                                                _        -> False
			      _            -> False

-- | used for (Head), (Head*)
typeCheckList :: Typ -> Bool
typeCheckList tau = case tau of
                     List _ -> True
                     _      -> False

-- | used for (Just), (Just*)
typeCheckMaybe :: Typ -> Bool
typeCheckMaybe tau = case tau of
                       TMaybe _ -> True
                       _        -> False

-- | used for (Bottom->*1)
typeCheckArrowUnPointedArgPointedRes :: [TypVar] -> Typ -> Bool
typeCheckArrowUnPointedArgPointedRes tvars tau = case tau of
					           Arrow tau1 tau2 -> unpointed tvars tau1 && (not (unpointed tvars tau2))
                                                   _               -> False
-- | used for (L->->*)
typeCheckArrowArgArrow :: Typ -> Bool
typeCheckArrowArgArrow tau = case tau of
			      Arrow tau1 _ -> case tau1 of
						Arrow _ _ -> True
						_         -> False
			      _            -> False

-- | used for (Bottom->), (Bottom->*2), (App'*)
typeCheckArrow :: Typ -> Bool
typeCheckArrow tau = case tau of
		       Arrow _ _ -> True
		       _         -> False

-- | used for (Drop1)
typeCheckInt :: Typ -> Bool
typeCheckInt tau = case tau of
		     Int -> True
		     _   -> False

-- | used for (Drop2)
typeCheckBrace :: Typ -> Bool
typeCheckBrace tau = case tau of
		     TBrace -> True
		     _      -> False

-- | used for (Drop4)
typeCheckBool :: Typ -> Bool
typeCheckBool tau = case tau of
		     TBool -> True
		     _     -> False

-- | used for (Proj), (Proj*)
typeCheckPair :: Typ -> Bool
typeCheckPair tau = case tau of
		      TPair _ _ -> True
		      _         -> False

-- | used for (Pair->)
typeCheckArrowPairArg :: Typ -> Bool
typeCheckArrowPairArg tau = case tau of
			      Arrow tau1 _ -> case tau1 of
					        TPair _ _ -> True
						_         -> False
			      _            -> False

-- | used for (LE->)
typeCheckArrowEitherArg :: Typ -> Bool
typeCheckArrowEitherArg tau = case tau of
			        Arrow tau1 _ -> case tau1 of
						  TEither _ _ -> True
						  _           -> False
				_            -> False

-- | used for (Dist1), (Dist2), (Dist1*), (Dist2*)
typeCheckEither :: Typ -> Bool
typeCheckEither tau = case tau of
		        TEither _ _ -> True
			_           -> False

-- * support functions

-- | Application of an argument to a function
insertArgument :: Term -> Term -> Term
insertArgument f x = case f of
		     Abs v _ t                 -> subst t x v
		     Bottom (Arrow tau1 tau2)  -> Bottom tau2
		     _ -> error ("unexpected termstructure" ++ (showTerm f))

-- | substitutes new (Term) for old (TermVar) in the term m
subst :: Term -> Term -> TermVar -> Term
subst m new old = case m of
		   Var var              -> if(var == old) then new else m
		   Abs v tau m'         -> Abs v tau (subst m' new old)
                   App m1 m2            -> App (subst m1 new old) (subst m2 new old)
                   TAbs tau m'          -> TAbs tau (subst m' new old)
                   Cons m1 m2           -> Cons (subst m1 new old) (subst m2 new old)
                   LCase m0 v2 m2    -> LCase (subst m0 new old) v2 (subst m2 new old)
		   Pair m1 m2           -> Pair (subst m1 new old) (subst m2 new old)
		   PCase m0 v1 v2 m1    -> PCase (subst m0 new old) v1 v2 (subst m1 new old)
		   Right m              -> Right (subst m new old)
                   Left m               -> Left (subst m new old)
                   ECase m0 v1 m1 v2 m2 -> ECase (subst m0 new old) v1 (subst m1 new old) v2 (subst m2 new old)
		   ICase m0 m1          -> ICase (subst m0 new old) (subst m1 new old)
		   BCase m0 m1          -> BCase (subst m0 new old) (subst m1 new old)					   
		   BoolCase m0 m1       -> BoolCase (subst m0 new old) (subst m1 new old)
                   MJust m0             -> MJust (subst m0 new old)
                   MCase m0 v2 m2       -> MCase (subst m0 new old) v2 (subst m2 new old)
                   _                    -> m

-- | calls subst for a list of termVariables (with according to the numbers) to be substituted
substAllInt :: Term -> [(Int,Term)] -> Term
substAllInt t l =
    case l of
      []        -> t
      (i,t'):xs -> substAllInt (subst t t' (TermVar i)) xs

-- | produces a Pair (p^+,p^+) of the given type, with p+ as described in the plus-term definition of the paper
makePlusPair :: Typ -> M (Maybe (Term, Term))
makePlusPair tau = do {x <- makePlusElem tau; 
		       case x of 
		       Just t -> return (Just (t,t))
		       _      -> return Nothing
		      }

-- | produces a Term p^+ of the given type, as described in the plus-term definition of the paper
makePlusElem :: Typ -> M (Maybe Term)
makePlusElem tau = case tau of
		   TVar  var         -> return (Just Brace)
		   Arrow tau1 tau2   -> do {x <- makePlusElem tau2;
					    i <- newInt;
					    let erg = case x of
						      Just t -> Just (Abs (TermVar i) tau1 t)
						      _      -> Nothing
					    in
					    return erg
					   }
                   List  tau         -> do {x <- makePlusElem tau;
					    let erg = case x of 
						      Just t -> Just (Cons t (Nil tau))
						      _      -> Nothing
					    in
					    return erg
					   }
		   TMaybe tau        -> do {x <- makePlusElem tau;
					    let erg = case x of 
						      Just t -> Just (MJust t)
						      _      -> Nothing
					    in
					    return erg
					   }
		   Int               -> return (Just Zero)
                   TBrace            -> return (Just Brace)
                   TBool             -> return (Just Fls)
                   TPair tau1 tau2   -> do {x <- makePlusElem tau1;
					    y <- makePlusElem tau2;
					    let erg = case x of
						      Just t1 -> case y of
								 Just t2 -> Just (Pair t1 t2)
								 Nothing -> Nothing
                                                      Nothing -> Nothing
					    in
					    return erg
					   }
                   
                   TEither tau1 tau2 -> do {x <- makePlusElem tau1;
					    y <- makePlusElem tau2;
					    let erg = case x of 
					              Just t1 -> Just (Left t1)
					              _       -> case y of
								 Just t2 -> Just (Right t2)
								 _       -> Nothing
					    in
					    return erg
					   }						
		   _                 -> return Nothing

-- |the function equals the lemma about the function construction (g(x_1),g(x_2))^{\Gamma,\tau}_{\varpi}
makeFuncPair :: Typ -> TrackCont -> Cont -> (Term,Term) -> M (Term,Term)
makeFuncPair tau trc' gamma resPair =
    let (z,z')  = resPair 
        (ctau,trc) = trc' in
    case tau of
      TVar beta    -> do {i <- newInt;
			  let w  = TermVar i
		              g' = Abs w tau (BCase (Var w) z') in
			  if unpointed (tVars gamma) tau
			  then return (Abs w tau z, g')
			  else return (Abs w tau (BCase (Var w) z), g')
			 }
      Int          -> do {i <- newInt;
			  let w  = TermVar i in
			  return (Abs w tau (ICase (Var w) z), Abs w tau (ICase (Var w) z'))
			 }

      TBrace       -> do {i <- newInt;
			  let w  = TermVar i in
			  return (Abs w tau (BCase (Var w) z), Abs w tau (BCase (Var w) z'))
			 }

      TBool        -> do {i <- newInt;
			  let w  = TermVar i in
			  return (Abs w tau (BoolCase (Var w) z), Abs w tau (BoolCase (Var w) z'))
			 }

      List tau'    -> case trc of
		        []       -> do{i <- newInt;
				       j <- newInt;
				       let w   = TermVar i
				           h   = TermVar j 
				       in
				       return (Abs w tau (LCase (Var w) h z), Abs w tau (LCase (Var w) h z'))
				      }
			_:xs     -> do{i <- newInt;
				       j <- newInt;				       
				       (g,g') <- makeFuncPair tau' (ctau,xs) gamma resPair;
				       let w   = TermVar i
				           u   = TermVar j in
				       return (Abs w tau (LCase (Var w) u (App g  (Var u))),
					       Abs w tau (LCase (Var w) u (App g' (Var u))))
				      }
      TMaybe tau'  -> case trc of
		        []       -> do{i <- newInt;
				       j <- newInt;
				       let w   = TermVar i
				           h   = TermVar j 
				       in
				       return (Abs w tau (MCase (Var w) h z), Abs w tau (MCase (Var w) h z'))
				      }
			_:xs     -> do{i <- newInt;
				       j <- newInt;				       
				       (g,g') <- makeFuncPair tau' (ctau,xs) gamma resPair;
				       let w   = TermVar i
				           u   = TermVar j in
				       return (Abs w tau (MCase (Var w) u (App g  (Var u))),
					       Abs w tau (MCase (Var w) u (App g' (Var u))))
				      }
      TPair tau' tau'' -> case trc of
	                   []       -> do{i <- newInt;
					  j <- newInt;
					  k <- newInt;
					  let w = TermVar i 
					      x = TermVar j
					      y = TermVar k
					  in
					  return (Abs w tau (PCase (Var w) x y z), Abs w tau (PCase (Var w) x y z'))
					 }
                           (Abs _ _ (PCase _ v _ (Var v')),_):xs ->
			       if v == v' then
				       do{i <- newInt;
					  j <- newInt;
					  m <- newInt;
					  n <- newInt;
					  let x = TermVar j
 					      y = TermVar m
					      u = TermVar n
					      w = TermVar i
                                              (k,k') = (Abs u tau'' z, Abs u tau'' z')
					  in				 
					  do{(h,h') <- makeFuncPair tau' (ctau,xs) gamma (k,k');
					     return (Abs w tau (PCase (Var w) x y (App (App h (Var x)) (Var y))), Abs w tau (PCase (Var w) x y (App (App h' (Var x)) (Var y))))
					    }
					 }
			       else
				       do{i <- newInt;
					  j <- newInt;
					  m <- newInt;
					  n <- newInt;
					  (k,k') <- makeFuncPair tau'' (ctau,xs) gamma resPair;
					  let x = TermVar j
					      y = TermVar m
					      u = TermVar n
					      w = TermVar i
					      (h,h') = (Abs x tau' (Abs y tau'' (App k (Var y))), Abs x tau' (Abs y tau'' (App k' (Var y))))
					  in
					  return (Abs w tau (PCase (Var w) x y (App (App h (Var x)) (Var y))), Abs w tau (PCase (Var w) x y (App (App h' (Var x)) (Var y))))
					 }
      TEither tau' tau'' -> do{i <- newInt;
			      j <- newInt;
			      let w = TermVar i
			          x = TermVar j
			      in
			      case trc of
                                []       -> return (Abs w tau (ECase (Var w) x (fst resPair) x (fst resPair)),
					            Abs w tau (ECase (Var w) x (fst resPair) x (snd resPair)))
			        (Abs _ _ (ECase _ _ (Var _) _ _),_):xs  ->
			                    do{(g,g') <- makeFuncPair tau' (ctau,xs) gamma resPair;
			                       return (Abs w tau (ECase (Var w) x (App g (Var x))  x (fst resPair)),
					               Abs w tau (ECase (Var w) x (App g' (Var x)) x (snd resPair)))
					      }			                    
			        (Abs _ _ (ECase _ _ _ _ (Var _)),_):xs  ->
                                            do{(g,g') <- makeFuncPair tau'' (ctau,xs) gamma resPair;
					       return (Abs w tau (ECase (Var w) x (fst resPair) x (App g (Var x))),
					               Abs w tau (ECase (Var w) x (snd resPair) x (App g' (Var x))))
					      }
			     }
      Arrow tau' tau'' -> case trc of
		           []         -> do{ i <- newInt;
					     (g,g') <- makeFuncPair tau'' (ctau,[]) gamma resPair;
					     Just (u,u') <- makePlusPair tau';
					     let x = TermVar i in
					     return (Abs x tau' (App g (App (Var x) u)), Abs x tau' (App g' (App (Var x) u')))
					   }
			   (f,f'):xs  -> do {i <- newInt;
					     (g,g') <- makeFuncPair tau'' (ctau,xs) gamma resPair;				     
					     let x = TermVar i in
					     return (Abs x tau' (App g (App f (Var x))), Abs x tau' (App g' (App f' (Var x))))
					    }

-- |support function for the term variable environment initialisation by the rules (Bottom) and (Ax*)
initialiseTermCont :: [TypedVar] -> M TermCont
initialiseTermCont varlist =
    case varlist of
      []         -> return Map.empty
      (x,tau):xs -> do{map    <- initialiseTermCont xs;
		       Just p <- makePlusPair tau;
		       return (Map.insert x (p,Leaf) map)
		      }

-- |tries to melt down the two TermCont from the premise of Arrow->* to one single suitable context. Uses the history therefore
mergeTermCont :: TermCont -> TermCont -> Maybe TermCont
mergeTermCont c1 c2 =
    let difference   = Map.union (Map.difference c1 c2) (Map.difference c2 c1) in
    if Map.filter (\x->x==False) (Map.intersectionWith checkCompareTerm c1 c2) == Map.empty
    then
      Just (Map.union (Map.intersectionWith compareTerm c1 c2) difference)
    else
      Nothing

compareTerm :: ((Term,Term),History) -> ((Term,Term),History) -> ((Term,Term),History)
compareTerm c1 c2 =
    let (_,his1) = c1
        (_,his2) = c2
    in
    if firstIsBetter his1 his2 then c1 else c2

checkCompareTerm c1 c2 =
   let (_,his1) = c1
       (_,his2) = c2
   in
   if firstIsBetter his1 his2 || firstIsBetter his2 his1 then True else False

firstIsBetter :: History -> History -> Bool
firstIsBetter his1 his2 =
    case his1 of
      Leaf -> case his2 of 
	         Leaf -> True 
		 _     -> False
      Branch rule his ->
               case his2 of
                 Leaf -> True
                 Branch rule' his' -> if rule == rule' then firstIsBetter his his' else False
                 _     -> False
      Split rule hisa hisb ->
               case his2 of
                 Leaf -> True
                 Split rule' hisa' hisb' -> if rule == rule' then (firstIsBetter hisa hisa' && firstIsBetter hisb hisb') else False
		 _     -> False

-- *simplifications

-- |removes App in terms. Resolves case statements if possible. Destroys the typing information.
simplifyTerm :: Term -> Term
simplifyTerm t = 
    case t of
    Abs v tau t1          -> traceSimplify "Simpl: Abs v tau t1" (Abs v tau (simplifyTerm t1))
    App t1 t2             -> let t1' = simplifyTerm t1 in
			     case t1' of
                             Bottom _ -> traceSimplify "Simpl: App _|_ t2" (Bottom (error "Typ not valid anymore."))
			     Abs v tau t1''           -> traceSimplify "Simpl: App (Abs _) t2" (simplifyTerm (subst t1'' (simplifyTerm t2) v))
			     --case-statements can appear.
			     _                        -> traceSimplify "Simpl: App not reduced." (App t1' (simplifyTerm t2))
    TAbs v t1             -> traceSimplify "Simpl: TAbs eliminated." (simplifyTerm t1)
    Cons t1 t2            -> traceSimplify "Simpl: Cons." (Cons (simplifyTerm t1) (simplifyTerm t2))
    LCase t1 v t3      -> let t1' = simplifyTerm t1 in
			     case t1' of
                             Bottom _          -> traceSimplify "Simpl: List Case with _|_ to _|_" (Bottom (error "Typ not valid anymore."))
			     Nil _             -> error "LCase with []! This should not appear!"
			     Cons t (Nil _)    -> traceSimplify "Simpl: List Case with x:_ to t3[t/v]" (simplifyTerm (subst t3 t v))
			     Cons t _          -> error "List with mor than one element! This should not appear!"
                             _                 -> traceSimplify "Simpl: List Case not reduced." (LCase t1' v (simplifyTerm t3))
    ICase t1 t2           -> let t1' = simplifyTerm t1 in
			     case t1' of
			     Bottom tau -> traceSimplify "Simpl: ICase with _|_ to _|_" (Bottom (error "Typ not valid anymore."))
                             Zero     -> traceSimplify "Simpl: ICase with 0 to t1" (simplifyTerm t2)
                             _        -> traceSimplify "Simpl: ICase not reduced." (ICase (simplifyTerm t1) (simplifyTerm t2))
    BCase t1 t2           -> let t1' = simplifyTerm t1 in
			     case t1' of
			     Bottom tau -> traceSimplify "Simpl: BCase with _|_ to _|_" (Bottom (error "Typ not valid anymore."))
                             Brace      -> traceSimplify "Simpl: BCase with () to t1" (simplifyTerm t2)
                             _          -> traceSimplify "Simpl: BCase not reduced." (BCase (simplifyTerm t1) (simplifyTerm t2))
    BoolCase t1 t2        -> let t1' = simplifyTerm t1 in
			     case t1' of
			     Bottom tau -> traceSimplify "Simpl: BoolCase with _|_ to _|_" (Bottom (error "Typ not valid anymore."))
                             Fls        -> traceSimplify "Simpl: BoolCase with Fls to t1" (simplifyTerm t2)
                             _          -> traceSimplify "Simpl: BoolCase not reduced." (BoolCase (simplifyTerm t1) (simplifyTerm t2))
    Pair t1 t2            -> traceSimplify "Simpl: Pair: reducing components." (Pair (simplifyTerm t1) (simplifyTerm t2))
    PCase t1 v1 v2 t2     -> case simplifyTerm t1 of
			     Pair t11 t12 -> traceSimplify "Simpl: PCase with Pair to t2[t11/v1,t12/v2]" (simplifyTerm (subst (subst t2 t11 v1) t12 v2))
                             Bottom _     -> traceSimplify "Simpl: PCase with _|_ to _|_" (Bottom (error "Typ not valid anymore."))
			     _            -> traceSimplify "Simpl: PCase not reduced." (PCase (simplifyTerm t1) v1 v2 (simplifyTerm t2))
    ECase t1 v1 t2 v2 t3  -> case simplifyTerm t1 of
                             Left t1'  -> traceSimplify "Simpl: ECase with Left t1' to t2[t1'/v1]" (simplifyTerm (subst t2 t1' v1))
			     Right t1' -> traceSimplify "Simpl: ECase with Left t1' to t3[t1'/v2]" (simplifyTerm (subst t3 t1' v2))
			     Bottom _  -> traceSimplify "Simpl: ECase with _|_ to _|_" (Bottom (error "Typ not valid anymore."))
		             _         -> traceSimplify "Simpl: ECase not reduced." (ECase (simplifyTerm t1) v1 (simplifyTerm t2) v2 (simplifyTerm t3))
    Right t1              -> traceSimplify "Simpl: Right" (Right (simplifyTerm t1))
    Left t1               -> traceSimplify "Simpl: Left" (Left (simplifyTerm t1))
    Var _                 -> t
    Nil _                 -> t
    Bottom _              -> t
    Zero                  -> Zero
    Brace                 -> Brace
    Fls                   -> Fls
    MJust t1              -> traceSimplify "Simpl: MJust." (MJust (simplifyTerm t1))
    MCase t1 v t2         -> let t1' = simplifyTerm t1 in
			         case t1' of
                                 Bottom _ -> traceSimplify "Simpl: Maybe Case with _|_ to _|_" (Bottom (error "Typ not valid anymore."))
                                 MJust t  -> traceSimplify "Simpl: Maybe Case with Just x to t2[t1/v]" (simplifyTerm (subst t2 t v))
			         _        -> traceSimplify "Simpl: Maybe Case not reduced." (MCase t1' v (simplifyTerm t2))

-- |simplifier for terms, just inserting function arguments, if possible. It does not resolve case-statements, but removes type abstractions.
simplifyAppOnly :: Term -> Term
simplifyAppOnly t =
    case t of
    Abs v tau t1          -> Abs v tau (simplifyAppOnly t1)
    App t1 t2             -> let t1' = simplifyAppOnly t1 in
			     case t1' of
                             Bottom _            -> Bottom (error "Typ not valid anymore.")
			     Abs v tau t1''      -> simplifyAppOnly (subst t1'' (simplifyAppOnly t2) v)
			     _                   -> App t1' (simplifyAppOnly t2) --for App, Var and Case-statements
    TAbs v t1             -> simplifyAppOnly t1
    Cons t1 t2            -> Cons (simplifyAppOnly t1) (simplifyAppOnly t2)
    LCase t1 v t3         -> LCase (simplifyAppOnly t1) v (simplifyAppOnly t3)
    ICase t1 t2           -> ICase (simplifyAppOnly t1) (simplifyAppOnly t2)
    BCase t1 t2           -> BCase (simplifyAppOnly t1) (simplifyAppOnly t2)
    BoolCase t1 t2        -> BoolCase (simplifyAppOnly t1) (simplifyAppOnly t2)
    Pair t1 t2            -> Pair (simplifyAppOnly t1) (simplifyAppOnly t2)
    PCase t1 v1 v2 t2     -> PCase (simplifyAppOnly t1) v1 v2 (simplifyAppOnly t2)
    ECase t1 v1 t2 v2 t3  -> ECase (simplifyAppOnly t1) v1 (simplifyAppOnly t2) v2 (simplifyAppOnly t3)
    Right t1              -> Right (simplifyAppOnly t1)
    Left t1               -> Left (simplifyAppOnly t1)
    Var _                 -> t
    Nil _                 -> t
    Bottom _              -> t
    Zero                  -> Zero
    Brace                 -> Brace
    Fls                   -> Fls
    MJust t1              -> MJust (simplifyAppOnly t1)
    MCase t1 v t2         -> MCase (simplifyAppOnly t1) v (simplifyAppOnly t2)
--    _                     -> error ("unexpected Term structure during simplification: " ++ (showTerm t))

-- |calls simplifyTerm for all Terms in the TermCont (term variable environments)
simplifyTermCont :: TermCont -> TermCont
simplifyTermCont c = 
    let simplifyPair ((t1,t2),his) = ((simplifyTerm t1, simplifyTerm t2),his) in
    Map.map simplifyPair c    


-- | calls simplifyTerm for all Terms in the list of the disrelater, i.e. for all entries of TrackCont
simplifyTrackCont :: TrackCont -> TrackCont
simplifyTrackCont trc =
    let (ctau,l) = trc in
    (ctau,simplifyTrackCont' l)

simplifyTrackCont' trc =
    case trc of 
    []         -> []
    (v1,v2):xs -> (simplifyTerm v1, simplifyTerm v2):(simplifyTrackCont' xs)

-- | replaces term variables in the disrelater by the terms they represent (given in the map)
-- maybe buggy
insertTermsInTrackCont :: TrackCont -> (Map.Map Int Term) -> TrackCont
insertTermsInTrackCont trc substs =
    let (ctau,ls) = trc in
    (ctau,map sub ls)
  where sub t = let (t1,t2) = t in (sub' t1, sub' t2) 
        sub' t =
 	    case t of
 	      Abs x tau (App y (Var (TermVar i))) -> 
		     if Var x == y && Map.member i substs 
		     then Abs x tau (App y (substs Map.! i))
		     else t
              _               -> t

-- | applies the disrelater to a term. This should lead to (p+,_|_) or (_|_._|_) for a term with a corresponding disrelater
--   and all termvariables substituted by the corresponding terms.
applyTrackCont :: Term -> TrackCont -> (Term,Term)
applyTrackCont t trc = 
    let (_,l) = trc in applyTrackCont' (t,t) l

applyTrackCont' :: (Term,Term) -> [(Term,Term)] -> (Term,Term)
applyTrackCont' (t1,t2) trc = 
    case trc of
    []   -> (t1,t2)
    x:xs -> applyTrackCont' (App (fst x) t1, App (snd x) t2) xs

-- *output enhancement and synchronisation with free-theorems package

-- | instantiate type relating functions.
-- | input is the type and a list of functionnames, representing the sequence in which they should be used
assignTypeRelFuncs :: Typ -> [String] -> String
assignTypeRelFuncs tau names = foldr (\x y -> ((getAt names (fst x)) ++ " = " ++ (snd x)) ++ y) "" (sort (assignTypeRelFuncs' tau))

assignTypeRelFuncs' :: Typ -> [(Int,String)]
assignTypeRelFuncs' tau =
    case tau of
    All (TypVar i) tau'     -> (i-1, "const ()\t"):assignTypeRelFuncs' tau'
    AllStar (TypVar i) tau' -> (i-1, "id\t\t"):assignTypeRelFuncs' tau'
    _                       -> []


-- | get a list of names of the type variables that can be interpreted non-strict.
getTypeRelFuncNamesNonStrict :: Typ -> [String] -> [String]
getTypeRelFuncNamesNonStrict tau names =
    snd.unzip.sort.getList $ tau
  where getList tau =
	    case tau of
	      All (TypVar i) tau'     -> (i-1, getAt names (i-1)):getList tau'
              AllStar (TypVar i) tau' -> getList tau'
              _                       -> []
showVarList l =
    case l of
      []   -> ""
      [v]  -> v
      v:vs -> v ++ "," ++ showVarList vs

prependRelFunc :: [String] -> Typ -> String -> String
prependRelFunc names tau str =
    case tau of
    TVar (TypVar i) -> getAt names (i-1) ++ " " ++ str
    _               -> str -- an elementary type (TBool, Int, TBrace). Relation is id and therefore dropped.

getTrackContWithFuncNames :: [String] -> TrackCont -> ([(String,Term)],String)
getTrackContWithFuncNames names trc =
    let (_,l) = trc
        (funcs,dis1,dis2) = getTrackContWithFuncNames' names l in
    (funcs,dis1 ++ " $ t = " ++ dis2 ++ " $ t")

getTrackContWithFuncNames' :: [String] -> [(Term,Term)] -> ([(String,Term)],String,String)
getTrackContWithFuncNames' names l =
    case l of
      []         -> ([],"","")
      [(t1,t2)]  -> if (isHead t1 || isFromLeft t1 || isFromRight t1 || isFst t1 || isSnd t1)
		    then ([], showTerm t1, showTerm t2)
		    else ([(head names,t1),(head (tail names),t2)], head names, head (tail names))
      (t1,t2):xs -> if (isHead t1 || isFromLeft t1 || isFromRight t1 || isFst t1 || isSnd t1)
		    then 
		      let (dis,str1,str2) = getTrackContWithFuncNames' names xs in
                      (dis, showTerm t1 ++ "." ++ str1, showTerm t2 ++ "." ++ str2)
		    else
                      let (dis,str1,str2) = getTrackContWithFuncNames' (drop 2 names) xs in
                      ([(head names,t1),(head (tail names),t2)] ++ dis,str1 ++ " . " ++  head names, str2 ++ " . " ++ head (tail names))


showFuncNames :: [(String,Term)] -> String
showFuncNames funcNames =
    case funcNames of
      []             -> ""
      (name,func):xs -> name ++ "\t = " ++ showTerm (head.renumberVariables $[simplifyTerm func]) ++ "\n" ++ showFuncNames xs

-- | renumbers term variables in a list of terms, such that different numbers stay different, but numbers are
--   decreased as far as possible
renumberVariables::[Term] -> [Term]
renumberVariables input =
    let vars = nub (getNums input)
        varNum = length vars 
        varMap = Map.fromList (zip vars [1..varNum]) in
        renumber input varMap
  where getNums terms =
            case terms of
              []   -> []
              x:xs -> getVarNums x ++ getNums xs
        renumber terms varMap =
            case terms of
              []   -> []
              x:xs -> renumberVars x varMap : renumber xs varMap

-- | returns a list with all variable numbers used in a term.
getVarNums term =
    case term of
      Var (TermVar i)      -> if i == 0 then [] else [i]
      Abs (TermVar i) _ t' -> i:getVarNums t'
      App t1 t2            -> getVarNums t1 ++ getVarNums t2
      Nil _                -> []
      Cons t1 t2           -> getVarNums t1 ++ getVarNums t2
      LCase t0 (TermVar i) t2 -> getVarNums t0 ++ [i] ++ getVarNums t2
      Bottom _             -> []
      TAbs (TypVar i) t    -> getVarNums t
      Brace                -> []
      ICase t1 t2          -> getVarNums t1 ++ getVarNums t2
      BCase t1 t2          -> getVarNums t1 ++ getVarNums t2
      BoolCase t1 t2       -> getVarNums t1 ++ getVarNums t2
      Pair t1 t2           -> getVarNums t1 ++ getVarNums t2
      PCase t0 (TermVar i) (TermVar j) t1 -> getVarNums t0 ++ [i,j] ++ getVarNums t1 
      ECase t0 (TermVar i) t1 (TermVar j) t2 -> getVarNums t0 ++ [i,j] ++ getVarNums t1 ++ getVarNums t2
      Left t               -> getVarNums t
      Right t              -> getVarNums t
      Zero                 -> []
      Fls                  -> []
      MJust t              -> getVarNums t
      MCase t0 (TermVar i) t2 -> getVarNums t0 ++ [i] ++ getVarNums t2

-- | renumbers term variables in a term as stated in the given map.
renumberVars term varMap =
    case term of
      Var (TermVar i)      -> if i == 0 then term else Var (TermVar (varMap Map.! i))
      Abs (TermVar i) tau t' -> Abs (TermVar (varMap Map.! i)) tau (renumberVars t' varMap)
      App t1 t2            -> App (renumberVars t1 varMap) (renumberVars t2 varMap)
      Nil _                -> term
      Cons t1 t2           -> Cons (renumberVars t1 varMap) (renumberVars t2 varMap)
      LCase t0 (TermVar i) t2 -> LCase (renumberVars t0 varMap) (TermVar (varMap Map.! i)) (renumberVars t2 varMap)
      Bottom _             -> term
      TAbs tv t            -> TAbs tv (renumberVars t varMap)
      Brace                -> Brace
      ICase t1 t2          -> ICase (renumberVars t1 varMap) (renumberVars t2 varMap)
      BCase t1 t2          -> BCase (renumberVars t1 varMap) (renumberVars t2 varMap)
      BoolCase t1 t2       -> BoolCase (renumberVars t1 varMap) (renumberVars t2 varMap)
      Pair t1 t2           -> Pair (renumberVars t1 varMap) (renumberVars t2 varMap)
      PCase t0 (TermVar i) (TermVar j) t1 -> PCase (renumberVars t0 varMap) (TermVar (varMap Map.! i)) (TermVar (varMap Map.! j)) (renumberVars t1 varMap)
      ECase t0 (TermVar i) t1 (TermVar j) t2 -> ECase (renumberVars t0 varMap) (TermVar (varMap Map.! i)) (renumberVars t1 varMap) (TermVar (varMap Map.! j)) (renumberVars t2 varMap)
      Left t               -> Left (renumberVars t varMap)
      Right t              -> Right (renumberVars t varMap)
      Zero                 -> Zero
      Fls                  -> Fls
      MJust t1             -> MJust (renumberVars t1 varMap)
      MCase t0 (TermVar i) t2 -> MCase (renumberVars t0 varMap) (TermVar (varMap Map.! i)) (renumberVars t2 varMap)

-- | takes a list with pairs (Int,Term), a list of function names and variable names and returns a list of (Int,String),
--   mapping each Int in the input list to a name out of the function or variable names
mapDisRelFuncsToNames :: [(Int,Term)] -> [String] -> [String] -> [(Int,String)]
mapDisRelFuncsToNames funcList funcs vars =
    case funcList of
     []               -> []
     (i,t1):(j,t2):ls -> case t1 of
                           Abs _ _ _ -> (i,head funcs):(j,head.tail $ funcs):mapDisRelFuncsToNames ls (tail.tail $ funcs) vars
                           _         -> (i,head vars):(j,(head vars ++ "'")):mapDisRelFuncsToNames ls funcs (tail vars)

-- *show and print functions

-- |returns the number of and a string with the term variable environment entries
showTermCont :: TermCont -> String
showTermCont tc = "Number of entries: " ++ (show (Map.size tc)) ++ "\n\n" ++ (showTermContList (Map.toList tc))

-- |prints the number of and the term variable environments entries
printTermCont :: TermCont -> IO() 
printTermCont tc = putStr (showTermCont tc)

-- |returns a string with the term context entries followed by "Nothing left.". It takes the context in form of a list.
showTermContList :: [(TermVar,((Term,Term),History))] -> String
showTermContList l = case l of
		     []                 -> "Nothing left.\n"
		     (v,((x,x'),_)):xs  ->   (showTerm (Var v)) ++ "  = " ++ (showTerm x) ++ "\n"
			                  ++ (showTerm (Var v)) ++ "' = " ++ (showTerm x')  ++ "\n\n"
			                  ++ (showTermContList xs)

-- |prints the term with prefix "result term: "
printResult ::  Term -> IO ()
printResult t = putStr ("result term: " ++ (showTerm t) ++ "\n\n")

-- |prints the typ with prefix "input type:  "
printTyp :: Typ -> IO ()
printTyp t = putStr ("input type:  " ++ showTyp t ++ "\n")

-- |returns a string with the \Gamma and \Sigma - context entries
showCont :: Cont -> String
showCont gamma = let showVars = 
			 let vs = vars gamma in 
			 case vs of
			  [] -> "]"
			  _  -> foldr (\x -> \y -> x ++ "," ++ y) "\b]" (map (\v -> showTerm (Var (fst v)) ++ "::" ++ showTyp (snd v)) (vs))
		     showVarsStar = 
			 let vs = varsStar gamma in
		         case vs of
			   [] -> "]"
			   _  -> foldr (\x -> \y -> x ++ "," ++ y) "\b]" (map (\v -> showTerm (Var (fst v)) ++ "::" ++ showTyp (snd v)) (vs)) 
		in
		"Cont = {vars = [" ++ showVars ++ ", varsStar = [" ++ showVarsStar ++ "}"

-- | pretty printer for Term.
--   All term variables are named by 'x' followed by a number.
showTerm :: Term -> String
showTerm t = showTermWithNames t Map.empty

-- | pretty printer for Term, where a map with special names for term variables can be given.
--   A term variable i with i in the map is is printed as the name provided for i in the map.
--   All other term variables are printed as 'x' followed by their number.
showTermWithNames :: Term -> (Map.Map Int String) -> String
showTermWithNames t m = 
             case t of
	       Var (TermVar i)      -> if i == 0 then termName 
				       else if Map.member i m then m Map.! i else 'x':(show i)
	       Abs v _ t'           -> if isHead t then "head"
				       else if isFst t then "fst"
				       else if isSnd t then "snd"
				       else if isFromLeft t then "fromLeft"
                                       else if isFromRight t then "fromRight"
                                       else if isFromJust t then "fromJust"
				       else "(\\" ++ showTermWithNames (Var v) m ++ " -> " ++ showTermWithNames t' m ++ ")"
               App t1 t2            -> "(" ++ showTermWithNames t1 m ++ " " ++ showTermWithNames t2 m ++ ")"
               Nil _                -> "[]"
               Cons t1 t2           -> case t2 of
					 Nil _ -> "[" ++ showTermWithNames t1 m ++ "]"
                                         _     -> "(" ++ showTermWithNames t1 m ++ ":" ++ showTermWithNames t2 m ++ ")"
               LCase t0 v2 t2    -> if isHeadApp t 
				       then "(head " ++ showTermWithNames t0 m ++ ")" 
                                       else "(case " ++ showTermWithNames t0 m ++ " of {[" ++ showTermWithNames (Var v2) m ++ "] -> " ++ showTermWithNames t2 m ++"})"
	       Bottom _             -> "_|_"
               TAbs (TypVar i) t    -> showTermWithNames t m
	       Brace                -> "()"
               Fls                  -> "False"
	       ICase t1 t2          -> "(case " ++ showTermWithNames t1 m ++ " of {0 -> " ++ showTermWithNames t2 m ++ "})"
	       BCase t1 t2          -> "(case " ++ showTermWithNames t1 m ++ " of {() -> " ++ showTermWithNames t2 m ++ "})"
	       BoolCase t1 t2       -> "(case " ++ showTermWithNames t1 m ++ " of {False -> " ++ showTermWithNames t2 m ++ "})"
               Pair t1 t2           -> "(" ++ showTermWithNames t1 m ++ "," ++ showTermWithNames t2 m ++ ")"
	       PCase t0 v1 v2 t1    -> if isFstApp t 
				       then "(fst " ++ showTermWithNames t0 m ++ ")"
				       else if isSndApp t
					    then "(snd " ++ showTermWithNames t0 m ++ ")"
                                            else "(case " ++ showTermWithNames t0 m ++ " of {(" ++ showTermWithNames (Var v1) m ++ "," ++ showTermWithNames (Var v2) m ++ ") -> " ++ showTermWithNames t1 m ++ "})"
	       ECase t0 v1 t1 v2 t2 -> if isFromLeftApp t
				       then "(fromLeft " ++ showTermWithNames t0 m ++ ")"
                                       else if isFromRightApp t
					    then "(fromRight " ++ showTermWithNames t0 m ++ ")"
                                            else "(case " ++ showTermWithNames t0 m ++ " of {Left " ++ showTermWithNames (Var v1) m ++ " -> " ++ showTermWithNames t1 m ++ "})"
					--right branch should be unnecessary, since pLusVal always returns Left-value and, if
                                        --not fromLeft/fromRight, it should be always "case pLusVal of", and hence Left.
					 -- ; Right " ++ showTermWithNames (Var v2) m ++ " -> " ++ showTermWithNames t2 m ++ "})"
               Left t               -> "Left " ++ showTermWithNames t m
               Right t              -> "Right " ++ showTermWithNames t m
               Zero                 -> "0"
               MJust t1             -> "(Just " ++ showTermWithNames t1 m ++ ")"
               MCase t0 v2 t2    -> if isFromJustApp t 
				       then "(fromJust " ++ showTermWithNames t0 m ++ ")" 
                                       else "(case " ++ showTermWithNames t0 m ++ " of {Just " ++ showTermWithNames (Var v2) m ++ " -> " ++ showTermWithNames t2 m ++"})"

-- |pretty printer for Typ
showTyp :: Typ -> String
showTyp t = case t of
              TVar (TypVar i)    -> ('v':(show i))
              Arrow t1 t2        -> "(" ++ showTyp t1 ++ " -> " ++ showTyp t2 ++ ")"
              All v t1           -> "\\" ++ showTyp (TVar v) ++ "." ++ showTyp t1
              AllStar v t1       -> "\\" ++ showTyp (TVar v) ++ "." ++ showTyp t1
              List t1            -> "[" ++ showTyp t1 ++ "]"
              Int                -> "Int"
              TPair t1 t2        -> "(" ++ showTyp t1 ++ "," ++ showTyp t2 ++ ")"
              TEither t1 t2      -> "(Either " ++ showTyp t1 ++ " " ++ showTyp t2 ++ ")"
	      TBrace             -> "()"
              TBool              -> "Bool"
              TMaybe t1          -> "(Maybe " ++ showTyp t1 ++ ")"

-- | returns a string with the disrelater entries with pretty printing
showTrackCont :: TrackCont -> String
showTrackCont trackCont = 
    let (ctau,trc) = trackCont in 
    showTrackCont' trc ++ "The type is: " ++ showTyp ctau ++ "\n\n"

showTrackCont' trc =
    case trc of
    []         -> ""
    (x1,x2):xs -> (showTerm x1) ++ "\n" ++
		  (showTerm x2) ++ "\n\n" ++
		  showTrackCont' xs


-- | returns a string with the disrelater entries _without_ pretty printing
showRawTrackCont :: TrackCont -> String
showRawTrackCont trackCont = 
    let (ctau,trc) = trackCont in 
    showRawTrackCont' trc ++ "The type is: " ++ show ctau ++ "\n\n"

showRawTrackCont' trc =
    case trc of
    []         -> ""
    (x1,x2):xs -> (show x1) ++ "\n" ++
		  (show x2) ++ "\n\n" ++
		  showRawTrackCont' xs

-- | applies the disrelater to the term and shows the simplified result as equation t1 = t2
showTrackContApplication :: TrackCont -> Term -> String
showTrackContApplication tc t = showTrackContApplicationWithNames tc [] t

-- | applies the disrelater to the term and shows the simplified result as equation t1 = t2
--   Furthermore variables in the nameList are printed by the given name instead of 'x' and
--   there number.
showTrackContApplicationWithNames :: TrackCont ->[(Int,String)] -> Term -> String
showTrackContApplicationWithNames tc nameList t =
    let (t1,t2) = applyTrackCont t tc 
        names   = Map.fromList nameList in
    showTermWithNames (simplifyTerm t1) names ++ " = " ++ showTermWithNames (simplifyTerm t2) names

-- | replaces the term variables with number i by the respective Term given in the (Int,Term)-list
--   and then applies the disrelater to the term and simplifies the result.
getTrackContApplicationSolved :: TrackCont -> [(Int,Term)] -> Term -> (Term,Term)
getTrackContApplicationSolved tc substs t =
    let (t1',t2') = (applyTrackCont t tc)
        (t1,t2)   = (substAllInt t1' substs, substAllInt t2' substs) in
    (simplifyTerm t1,simplifyTerm t2)

showTrackContApplicationSolved :: TrackCont -> [(Int,Term)] -> Term -> String
showTrackContApplicationSolved tc substs t =
    let (t1,t2) = getTrackContApplicationSolved tc substs t in
    showTerm t1 ++ " = " ++ showTerm t2

showFuncNamesInt :: [(Int,Term)] -> String
showFuncNamesInt funcNames =
    case funcNames of
      []             -> ""
      (i,func):xs -> "x"++ show i ++ "\t = " ++ showTerm (head.renumberVariables $[simplifyTerm func]) ++ "\n" ++ showFuncNamesInt xs

-- *Set of functions for calling the algorithm

-- ** Monad features
-- | set the information the monad should return
makeTrackString :: String -> Cont -> Typ -> String
makeTrackString = trackRules 

-- | return the applied rules with input contexts and type
trackAll :: String -> Cont -> Typ -> String
trackAll rule gamma tau = rule ++ ": " ++ showCont gamma ++ ", Type = " ++ showTyp tau

-- | return the applied rules
trackRules :: String -> Cont -> Typ -> String
trackRules rule gamma tau = rule