-- * The module contains all rules of ExFind and the algorithm itself (the sequence in which the rules are used).

module Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.ExFindExtended (alg) where

import Language.Haskell.FreeTheorems.Variations.CounterExamples.Common.AlgCommon
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
-------Regeln der ersten Phase-------------
-- * The rules of the algorithm
--   The rules have at most three parts:
--   - rule == term construction
--   - rule_tc_update == alternation of the term environments (TermCont)
--   - rule_trackCont_update == alternation of the disrelater (TrackCont)

-- | auxiliary function for tc update
pLusVal_tc_update :: TermCont -> TypedVar -> M TermCont
pLusVal_tc_update tc var =
    let (v,tau) = var in
    do {Just p <- makePlusPair tau;
	return (Map.insert v (p,Leaf) tc)
       }

-- ** first phase
-- *** rules without backtracking

bOttom :: Cont -> Typ -> Maybe Term
bOttom gamma tau = if isElementaryType tau && unpointed (tVars gamma) tau
		 then Just (Bottom tau)
		 else Nothing

-- |initialises the term environments with plus-terms for each term variable in the term variable context
bOttom_tc_update :: Cont -> M TermCont
bOttom_tc_update gamma = initialiseTermCont (vars gamma)

rAllStar :: Cont -> Typ -> Maybe (Cont, Typ, Term -> Term)
rAllStar gamma tau = case tau of
		       AllStar tv tau' -> Just (updateTVarStar gamma tv, tau', \m -> TAbs tv m)
		       _               -> Nothing

rAll :: Cont -> Typ -> Maybe (Cont, Typ, Term -> Term)
rAll gamma tau = case tau of
		   All tv tau' -> Just (updateTVar gamma tv, tau', \m -> TAbs tv m)
		   _           -> Nothing

aBs :: Cont -> Typ -> Maybe (M (Cont, TermVar, Term -> Term), Typ)
aBs gamma tau = case tau of
		   Arrow tau1 tau2 -> Just (do {i <- newInt; 
						let x = TermVar i in
						return (updateVar gamma x tau1, x, \m -> Abs x tau1 m)		       
					       }
					   , tau2)
		   _               -> Nothing

aBs_tc_update :: TermCont -> TermVar -> TermCont
aBs_tc_update tc v = Map.delete v tc

aBs_trackCont_update :: TrackCont -> Typ -> TermCont -> TermVar -> M TrackCont
aBs_trackCont_update trackCont tau tc v = 
    let (tau,trc) = trackCont
        ((x1,x2),_) = trace "Map.! abs_trackCont_update" (tc Map.! v) in
    do{i <- newAux;
       j <- newAux;
       k <- newAux;
       assoc k x2;
       assoc j x1;
       let u = TermVar i in
       return (tau,(Abs u tau (App (Var u) (Var (TermVar j))), Abs u tau (App (Var u) (Var (TermVar k)))):trc)
      }

wRap :: Typ -> Maybe (Typ, Term -> Term)
wRap tau = case tau of
               List tau' -> Just (tau', \m -> Cons m (Nil tau'))
               _         -> Nothing

wRap_trackCont_update :: TrackCont -> Typ -> M TrackCont
wRap_trackCont_update trackCont tau = 
    let (ctau,trc) = trackCont
        List tau' = tau in
    do{f <- listhead tau';
       return (ctau,(f,f):trc)
      }

mAybe :: Typ -> Maybe (Typ, Term -> Term)
mAybe tau = case tau of
               TMaybe tau' -> Just (tau', \m -> MJust m)
               _         -> Nothing

mAybe_trackCont_update :: TrackCont -> Typ -> M TrackCont
mAybe_trackCont_update trackCont tau = 
    let (ctau,trc) = trackCont
        TMaybe tau' = tau in
    do{f <- fromJust tau';
       return (ctau,(f,f):trc)
      }

wRapTo :: Cont -> Maybe (M ((Cont, Term -> Term),(TypedVar, TypedVar)))
wRapTo gamma = let f = findfirst typeCheckArrowListArg (vars gamma) in
                    case f of
                      Nothing ->      Nothing
		      Just (v, (Arrow (List tau1) tau2)) -> 
                           Just (do {i <- newAux; --g in the new context
			             j <- newInt; --y for substitution
			            let g = TermVar i
				        y = TermVar j in				   
				    return ((updateVar (removeVar gamma v) g (Arrow tau1 tau2),
					    \m -> subst m (Abs y tau1 (App (Var v) (Cons (Var y) (Nil tau1)))) g),
					    ((g,Arrow tau1 tau2), (v, Arrow (List tau1) tau2)))
				    })

wRapTo_tc_update :: TermCont -> TermVar -> TermVar -> TypedVar -> TypedVar -> TermCont
wRapTo_tc_update tc l h g f = 
    let Arrow (List t1) t2 = snd f
	((x,y),his) = (trace "Map.!-check: wRapTo g" (tc Map.! (fst g)))
    in
    Map.delete (fst g) (Map.insert (fst f) ((Abs l  (List t1) (LCase (Var l) h (App x (Var h))),Abs l (List t1) (LCase (Var l) h (App y (Var h)))),Branch WrapTo his) tc)

mAybeTo :: Cont -> Maybe (M ((Cont, Term -> Term),(TypedVar, TypedVar)))
mAybeTo gamma = let f = findfirst typeCheckArrowMaybeArg (vars gamma) in
                    case f of
                      Nothing ->      Nothing
		      Just (v, (Arrow (TMaybe tau1) tau2)) -> 
                           Just (do {i <- newAux; --g in the new context
			             j <- newInt; --y for substitution
			            let g = TermVar i
				        y = TermVar j in				   
				    return ((updateVar (removeVar gamma v) g (Arrow tau1 tau2),
					    \m -> subst m (Abs y tau1 (App (Var v) (MJust (Var y)))) g),
					    ((g,Arrow tau1 tau2), (v, Arrow (TMaybe tau1) tau2)))
				    })

mAybeTo_tc_update :: TermCont -> TermVar -> TermVar -> TypedVar -> TypedVar -> TermCont
mAybeTo_tc_update tc l h g f = 
    let Arrow (TMaybe t1) t2 = snd f
	((x,y),his) = (trace "Map.!-check: wRapTo g" (tc Map.! (fst g)))
    in
    Map.delete (fst g) (Map.insert (fst f) ((Abs l  (TMaybe t1) (MCase (Var l) h (App x (Var h))),Abs l (TMaybe t1) (MCase (Var l) h (App y (Var h)))),Branch MaybeTo his) tc)

hEad :: Cont -> Typ -> Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))
hEad gamma tau' = let l = findfirst typeCheckList (vars gamma) in
		case l of
                  Nothing           -> Nothing
                  Just (v,List tau) -> Just (do {lh <- listheadApp (Var v) tau;
						 i <- newInt; --h
						 let h = TermVar i in
						 return ((updateVar (removeVar gamma v) h tau,
							  \m -> subst m lh h),
							 ((h,tau),(v,List tau)))
						})

hEad_tc_update :: TermCont -> TypedVar -> TypedVar -> TermCont
hEad_tc_update tc h l = let ((x,y),his) = (trace "Map.!-check: hEad h" (tc Map.! (fst h))) in
		      Map.delete (fst h) (Map.insert (fst l) ((Cons x (Nil (snd h)), Cons y (Nil (snd h))),Branch Head his) tc)

jUst :: Cont -> Typ -> Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))
jUst gamma tau' = let l = findfirst typeCheckMaybe (vars gamma) in
		case l of
                  Nothing           -> Nothing
                  Just (v,TMaybe tau) -> Just (do {lh <- fromJustApp (Var v) tau;
						 i <- newInt; --h
						 let h = TermVar i in
						 return ((updateVar (removeVar gamma v) h tau,
							  \m -> subst m lh h),
							 ((h,tau),(v,TMaybe tau)))
						})

jUst_tc_update :: TermCont -> TypedVar -> TypedVar -> TermCont
jUst_tc_update tc h l = let ((x,y),his) = (trace "Map.!-check: jUst h" (tc Map.! (fst h))) in
		      Map.delete (fst h) (Map.insert (fst l) ((MJust x, MJust y),Branch RJust his) tc)

dRop1 :: Cont -> Maybe (Cont,TermVar)
dRop1 gamma = let l = findfirst typeCheckInt (vars gamma) in
	       case l of
		 Nothing  -> Nothing
                 Just var -> Just ((removeVar gamma (fst var)),fst var)

dRop1_tc_update :: TermCont -> TermVar -> TermCont
dRop1_tc_update tc v = Map.insert v ((Zero,Zero),Leaf) tc

dRop2 :: Cont -> Maybe (Cont,TermVar)
dRop2 gamma = let l = findfirst typeCheckBrace (vars gamma) in
	       case l of
		 Nothing  -> Nothing
                 Just var -> Just ((removeVar gamma (fst var)),fst var)

dRop2_tc_update :: TermCont -> TermVar -> TermCont
dRop2_tc_update tc v = Map.insert v ((Brace,Brace),Leaf) tc

dRop4 :: Cont -> Maybe (Cont,TermVar)
dRop4 gamma = let l = findfirst typeCheckBool (vars gamma) in
	       case l of
		 Nothing  -> Nothing
                 Just var -> Just ((removeVar gamma (fst var)),fst var)

dRop4_tc_update :: TermCont -> TermVar -> TermCont
dRop4_tc_update tc v = Map.insert v ((Fls,Fls),Leaf) tc

dRop3 :: Cont -> Maybe (Cont,TypedVar)
dRop3 gamma = let l = findfirstWithTVars unpointed (tVars gamma) (vars gamma) in
                 case l of
		   Nothing    -> Nothing
		   Just var   -> Just ((removeVar gamma (fst var)),var)

dRop3_tc_update :: TermCont -> TypedVar -> M TermCont
dRop3_tc_update = pLusVal_tc_update

pAirTo :: Cont -> Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))
pAirTo gamma = let l = findfirst typeCheckArrowPairArg (vars gamma) in
		    case l of
		      Nothing  -> Nothing
		      Just (f, (Arrow (TPair tau1 tau2) tau3)) -> 
			   Just (do {i <- newAux; --g in the new context
				     j <- newInt;
				     k <- newInt;
				     let g = TermVar i 
				         x = TermVar j
				         y = TermVar k in
				     return ((updateVar (removeVar gamma f) g (Arrow tau1 (Arrow tau2 tau3)),
					     \m -> subst m (Abs x  tau1 (Abs y tau2 (App (Var f) (Pair (Var x) (Var y))))) g),((g,Arrow tau1 (Arrow tau2 tau3)),(f,(Arrow (TPair tau1 tau2) tau3))))
				    })

pAirTo_tc_update :: TermCont -> TypedVar -> TypedVar -> M (TermCont)
pAirTo_tc_update tc g f = do {i <- newInt;
			       j <- newInt;
			       k <- newInt;
			       let p = TermVar i
			           x = TermVar j
				   y = TermVar k 
			           Arrow tau tau3 = snd f 
			           ((z,z'),his) = (trace "Map.!-check: pAirTo g" (tc Map.! (fst g)))
			       in
			       return (Map.delete (fst g) (Map.insert (fst f) ((Abs p tau (PCase (Var p) x y (App (App z (Var x)) (Var y))),Abs p tau (PCase (Var p) x y (App (App z' (Var x)) (Var y)))),Branch PairTo his) tc))
			      }

pRoj :: Cont -> Maybe (M ((Cont, Term -> Term),([TypedVar],TypedVar)))
pRoj gamma = let l = findfirst typeCheckPair (vars gamma) in
	       case l of
		 Nothing -> Nothing
		 Just (p, TPair tau1 tau2) ->
		      Just (do {i <- newInt;
				j <- newInt;
				let x = TermVar i
				    y = TermVar j in
				do {f <- firstApp (Var p);
				    s <- secondApp (Var p);
				    return ((updateVar (updateVar (removeVar gamma p) x tau1) y tau2,
				             \m -> subst (subst m f x) s y),
					    ([(x,tau1),(y,tau2)],(p,TPair tau1 tau2)))
				   }
			       })

pRoj_tc_update :: TermCont -> [TypedVar] -> TypedVar -> TermCont
pRoj_tc_update tc varIn p = 
    let [x,y] = varIn 
	((z,z'),his1) = (trace "Map.!-check: pRoj x" (tc Map.! (fst x)))
	((u,u'),his2) = (trace "Map.!-check: pRoj y" (tc Map.! (fst y)))
    in
    Map.delete (fst x) (Map.delete (fst y) (Map.insert (fst p) ((Pair z u, Pair z' u'), Split Proj his1 his2) tc))


eItherTo :: Cont -> Maybe (M ((Cont, Term -> Term),([TypedVar],TypedVar)))
eItherTo gamma = let l = findfirst typeCheckArrowEitherArg (vars gamma) in
	            case l of
		      Nothing -> Nothing
		      Just (f, (Arrow (TEither tau1 tau2) tau3)) ->
			   Just (do {i <- newAux; --g in the new context
				     j <- newAux; --h in the new context
				     k <- newInt; --x in the term
				     l <- newInt; --y in the term
				     let g = TermVar i
				         h = TermVar j
				         x = TermVar k
				         y = TermVar l in
				     return ((updateVar (updateVar (removeVar gamma f) g (Arrow tau1 tau3)) h (Arrow tau2 tau3),
					     \m -> subst (subst m (Abs x tau1 (App (Var f) (Left (Var x)))) g) (Abs y tau2 (App (Var f) (Right (Var y)))) h),
					     ([(g,Arrow tau1 tau3),(h,Arrow tau2 tau3)],(f,(Arrow (TEither tau1 tau2) tau3))))
				    })

eItherTo_tc_update :: TermCont -> [TypedVar] -> TypedVar -> M (TermCont)
eItherTo_tc_update tc varIn f = let [g,h] = varIn in
                               do{i <- newInt;
				  j <- newInt;
				  k <- newInt;
				  let e = TermVar i 
				      x = TermVar j
				      y = TermVar k 
				      Arrow tau tau3 = snd f 
			              ((z,z'),his1) = (trace "Map.!-check: eItherTo g" (tc Map.! (fst g)))
				      ((u,u'),his2) = (trace "Map.!-check: eItherTo h" (tc Map.! (fst h)))
				  in
	  			  return (Map.delete (fst g) (Map.delete (fst h) (Map.insert (fst f) ((Abs e tau (ECase (Var e) x (App z (Var x)) y (App u (Var y))), Abs e tau (ECase (Var e) x (App z' (Var x)) y (App u' (Var y)))),Split EitherTo his1 his2) tc)))
				 }

-- *** rules with backtracking

dIst1 :: Cont -> Typ -> Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))
dIst1 gamma tau = case findfirst typeCheckEither (vars gamma) of
                    Nothing -> Nothing
                    Just (e, TEither tau1 tau2) ->
		         Just (do {i <- newInt;
				   l <- fromLeftApp (Var e) tau1;
				   let x = TermVar i in
				   return ((updateVar (removeVar gamma e) x tau1,
					   \m -> subst m l x),
					   ((x,tau1),(e, TEither tau1 tau2)))
				  })

dIst1_tc_update :: TermCont -> TypedVar -> TypedVar -> TermCont
dIst1_tc_update tc x e = let ((z,z'),his) = (trace "Map.!-check: dIst1 x" (tc Map.! (fst x)))
		       in
		       Map.delete (fst x) (Map.insert (fst e) ((Left z, Left z'),Branch Dist1 his) tc)

dIst2 :: Cont -> Typ -> Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))
dIst2 gamma tau = case findfirst typeCheckEither (vars gamma) of
                    Nothing -> Nothing
                    Just (e, TEither tau1 tau2) ->
		         Just (do {r <- fromRightApp (Var e) tau2;
				   i <- newInt;
				   let y = TermVar i in
				   return ((updateVar (removeVar gamma e) y tau2,
					   \m -> subst m r y),
					   ((y,tau2),(e,TEither tau1 tau2)))
				  })
dIst2_tc_update :: TermCont -> TypedVar -> TypedVar -> TermCont
dIst2_tc_update tc y e = let ((z,z'),his) = (trace "Map.!-check: dIst2 fst y" (tc Map.! (fst y)))
		       in
		       Map.delete (fst y) (Map.insert (fst e) ((Right z, Right z'),Branch Dist2 his) tc)

pAir1 :: Typ -> Maybe (Typ, Term -> Term)
pAir1 tau = case tau of
            TPair tau1 tau2 -> Just (tau1, \m -> Pair m (Bottom tau2))
	    _               -> Nothing

pAir1_trackCont_update :: TrackCont -> Typ -> M TrackCont
pAir1_trackCont_update trackCont tau =
    let (ctau,trc) = trackCont in
    do{f <- first tau;
       return (ctau,(f,f):trc)
      }

pAir2 :: Typ -> Maybe (Typ, Term -> Term)
pAir2 tau = case tau of
            TPair tau1 tau2 -> Just (tau2,\m -> Pair (Bottom tau1) m)
	    _               -> Nothing

pAir2_trackCont_update :: TrackCont -> Typ -> M TrackCont
pAir2_trackCont_update trackCont tau =
    let (ctau,trc) = trackCont in
    do{f <- second tau;
       return (ctau,(f,f):trc)
      }

lEft :: Typ -> Maybe (Typ, Term -> Term)
lEft tau = case tau of
	    TEither tau1 _ -> Just(tau1, \m -> Left m)
            _              -> Nothing

lEft_trackCont_update :: TrackCont -> Typ -> M TrackCont
lEft_trackCont_update trackCont tau =
    let (ctau,trc) = trackCont
	TEither tau' tau'' = tau in
    do{f <- fromLeft tau' tau'';
       return (ctau,(f,f):trc)
      }


rIght :: Typ -> Maybe (Typ, Term -> Term)
rIght tau = case tau of
	    TEither _ tau2 -> Just(tau2, \m -> Right m)
            _              -> Nothing

rIght_trackCont_update :: TrackCont -> Typ -> M TrackCont
rIght_trackCont_update trackCont tau =
    let (ctau,trc) = trackCont
        TEither tau' tau'' = tau in
    do{f <- fromRight tau' tau'';
       return (ctau,(f,f):trc)
      }

bOttomToStripe :: Cont -> [M ((Cont, Term -> Term),(TypedVar,TypedVar))]
bOttomToStripe gamma = let l = findallWithTVars typeCheckArrowUnPointedArgPointedRes (tVars gamma) (vars gamma) in
                          map makeone l
		          where makeone = \var -> let Arrow tau1 tau2 = snd var in
					               do {i <- newAux;
							    let x = TermVar i in
							    return (((updateVarStar (removeVar gamma (fst var)) x tau2)
							             , \m -> subst m (App (Var (fst var)) (Bottom tau1)) x),((x,tau2),var))
							  }
bOttomToStripe_tc_update :: TermCont -> Cont -> TypedVar -> TypedVar -> M TermCont
bOttomToStripe_tc_update tc gamma x f = let Arrow t1 t2 = snd f 
				            ((u,u'),his) =  trace "Map.! bOttomToStripe_tc_update" (tc Map.! (fst x)) 
				        in
                                        do{(g,g') <- makeFuncPair t1 (error "type of disrelater used, which is not set",[]) gamma (u,u');
					   return (Map.delete (fst x) (Map.insert (fst f) ((g,g'),Branch BottomToStripe his) tc))
					  }

aRrowToStar :: Cont -> [M (((Cont, Typ), Cont, Term -> Term -> Term), ([TypedVar],TypedVar))]
aRrowToStar gamma = 
    let l = findall typeCheckArrowArgArrow (vars gamma) in
    map makeone l
    where makeone var = let Arrow (Arrow tau1 tau2) tau3 = snd var in
	                do {i <- newInt;
			    j <- newInt;
			    let x = TermVar i 
			        y = TermVar j in
			    return ((((updateVar (removeVar gamma (fst var)) x tau1),
				     tau2),
				     updateVarStar (removeVar gamma (fst var)) y tau3,
				     \m1 -> \m2 -> subst m2 (App (Var (fst var)) (Abs x tau1 m1)) y),
				    ([(x,tau1),(y,tau3)],var))
			   }
------------------------              TermContext         M_1     w           y           f           TermContext -----
aRrowToStar_tc_update :: TrackCont -> TermCont -> Cont -> Term -> TypedVar -> TypedVar -> TypedVar -> M TermCont
aRrowToStar_tc_update trackCont tc gamma m1 w y f = 
    let (_,trc) = trackCont
        Arrow t12 t3 = snd f 
	Arrow t1  t2 = t12
	(resPair,hisy) = (trace "Map.!-check: aRrowToStar g-construct y (else)" (tc Map.! (fst y)))
    in
    do {i <- newInt;
	(g,g') <- makeFuncPair t2 trackCont gamma resPair;
	let u = TermVar i 
	    ((z,z'),hisw) = (trace "Map.!-check: aRrowToStar w" (tc Map.! (fst w)))
	in
        return (Map.delete (fst w) (Map.delete (fst y) (Map.insert (fst f) ((Abs u t12 (App g (App (Var u) z)), Abs u t12 (App g' (App (Var u) z'))),Split ArrowToStar hisw hisy) tc)))
       }

bOttomTo :: Cont -> [M ((Cont, Term -> Term),(TypedVar,TypedVar))]
bOttomTo gamma = 
    let l = findall typeCheckArrow (vars gamma) in
    map makeone l
    where makeone var = let Arrow tau1 tau2 = snd var in
			do {i <- newAux;
			    let x = TermVar i in
			    return ((updateVar (removeVar gamma (fst var)) x tau2,
			            \m -> subst m (App (Var (fst var)) (Bottom tau1)) x),
				    ((x,tau2),var))
		           }

bOttomTo_tc_update :: TermCont -> TermVar -> TypedVar -> TypedVar -> TermCont
bOttomTo_tc_update tc z x f =
    let Arrow t1 t2 = snd f 
        ((u,u'),his) = (trace "Map.!-check: bOttomTo x" (tc Map.! (fst x)))
    in 
    Map.delete (fst x) (Map.insert (fst f) ((Abs z t1 u, Abs z t1 u'), Branch BottomTo his) tc)


-- ** rules of the second phase
-- *** rules without backtracking
vArStar :: Cont -> Typ -> Maybe (Term, (TermVar,Typ))
vArStar gamma tau = if isElementaryType tau 
		   then case findfirstSpecialType (varsStar gamma) tau of
                        Nothing -> Nothing
		        Just x  -> Just (Var (fst x), x)
		   else Nothing

-- | creates the initial term variable environment.
vArStar_tc_update :: Cont -> M TermCont
vArStar_tc_update gamma = initialiseTermCont ((vars gamma) ++ (varsStar gamma))

bOttomToStar :: Cont -> Maybe (M ((Cont, Term -> Term),((TermVar,Typ),(TermVar,Typ))))
bOttomToStar gamma = case findfirst typeCheckArrow (varsStar gamma) of
                       Nothing                    -> Nothing
                       Just (f, Arrow tau1 tau2)  -> Just (do {i <- newAux;
							       let y = TermVar i in
							       return ((updateVarStar (removeVarStar gamma f) y tau2, \m -> subst m (App (Var f) (Bottom tau1)) y),((y, tau2),(f, Arrow tau1 tau2) ));
							     })
bOttomToStar_tc_update :: TermCont -> TermVar -> TypedVar -> TypedVar -> TermCont
bOttomToStar_tc_update tc x varIn varOut = case (snd varOut) of
					   Arrow tau1 _ ->
					     let ((z,z'),his) = (trace "Map.!-check: bOttomToStar varIn" (tc Map.!(fst varIn)))
					     in
					     Map.delete (fst varIn) (Map.insert (fst varOut) ((Abs x tau1 z, Abs x tau1 z'),Branch BottomTo his) tc)

aPpStripStar :: Cont -> Maybe (M ((Cont, Term -> Term),([TypedVar],TypedVar)))
aPpStripStar gamma = checkall (findall typeCheckArrow (vars gamma)) 
		     where checkall xs =
			       case xs of
				 []  -> Nothing
			         ((f, Arrow tau1 tau2):ys) -> if unpointed (tVars gamma) tau2 
							      then checkall ys
							      else case findfirstSpecialType (varsStar gamma) tau1 of
							             Nothing     -> checkall ys
								     Just (x,_)  -> Just (do {i <- newAux;
											      let y = TermVar i in
											      return ((updateVarStar (removeVar gamma f) y tau2, \m -> subst m (App (Var f) (Var x)) y),([(x,tau1),(y,tau2)],(f,Arrow tau1 tau2)))
											})
-----------------------------------                      x*          y*          f           -------- 
aPpStripStar_tc_update :: TermCont -> Cont -> TermVar -> TypedVar -> TypedVar -> TypedVar -> M TermCont
aPpStripStar_tc_update tc gamma z x y f = let  ((v,v'),his) = (trace "Map.!-check: aPpStripStar y (TVar)" (tc Map.! (fst y)))
					  in
				          do{fPair <- makeFuncPair (snd x) (error "unset disrelater type used",[]) gamma (v,v');
					     return  (Map.delete (fst y) (Map.insert (fst f) (fPair,Branch BottomToStripe his) tc))
					    }

hEadStar :: Cont -> Typ ->  Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))
hEadStar gamma tau = case findfirst typeCheckList (varsStar gamma) of
                     Nothing           -> Nothing
		     Just (l,List tau') -> Just (do {i <- newInt;
						     lh <- listheadApp (Var l) tau';
						    let h = TermVar i in
						    return ((updateVarStar (removeVarStar gamma l) h tau',
							     \m -> subst m lh h),
							    ((h, tau'),(l,List tau')))
						    })

hEadStar_tc_update tc h l = let ((u,u'),his) = (trace "Map.!-check: hEadStar fst h" (tc Map.!(fst h)))
			  in
			  Map.delete (fst h) (Map.insert (fst l) ((Cons u (Nil (snd h)), Cons u' (Nil (snd h))),Branch Head his) tc)

jUstStar :: Cont -> Typ ->  Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))
jUstStar gamma tau = case findfirst typeCheckList (varsStar gamma) of
                     Nothing           -> Nothing
		     Just (l,TMaybe tau') -> Just (do {i <- newInt;
						       lh <- fromJustApp (Var l) tau';
						       let h = TermVar i in
						       return ((updateVarStar (removeVarStar gamma l) h tau',
								\m -> subst m lh h),
							       ((h, tau'),(l,TMaybe tau')))
						      })

jUstStar_tc_update tc h l = let ((u,u'),his) = (trace "Map.!-check: jUstStar h" (tc Map.!(fst h)))
			  in
			  Map.delete (fst h) (Map.insert (fst l) ((MJust u, MJust u'),Branch RJust his) tc)

pRojStar :: Cont -> Maybe (M ((Cont, Term -> Term),([TypedVar],TypedVar)))
pRojStar gamma = let l = findfirst typeCheckPair (varsStar gamma) in
	            case l of
		      Nothing -> Nothing
		      Just (p, TPair tau1 tau2) ->
		           Just (do {i <- newInt;
			 	     j <- newInt;
				     k <- newInt;
				     l <- newInt;
				     let x = TermVar i
				         y = TermVar j
				         u = TermVar k
				         v = TermVar l in
				     return ((updateVarStar (updateVarStar (removeVarStar gamma p) x tau1) y tau2,
				             \m -> subst (subst m (PCase (Var p) u v (Var u)) x) (PCase (Var p) u v (Var v)) y),
					     ([(x,tau1),(y,tau2)],(p,TPair tau1 tau2)))
				    })

pRojStar_tc_update :: TermCont -> [TypedVar] -> TypedVar -> TermCont
pRojStar_tc_update tc varIn p = 
    let [x,y] = varIn 
	((z,z'),his1) = (trace "Map.!-check: pRojStar fst x" (tc Map.! (fst x)))
	((u,u'),his2) = (trace "Map.!-check: pRojStar fst y" (tc Map.! (fst y)))
    in
    Map.delete (fst x) (Map.delete (fst y) (Map.insert (fst p) ((Pair z u, Pair z' u'),Split Proj his1 his2) tc))

iNtStar :: Cont -> Maybe (Cont,Term -> Term, TypedVar)
iNtStar gamma = case findfirstSpecialType (varsStar gamma) Int of
		Nothing -> Nothing
		Just x  -> Just (removeVarStar gamma (fst x), \m -> ICase (Var (fst x)) m, x)

iNtStar_tc_update :: TermCont -> TermVar -> TermCont
iNtStar_tc_update tc var = Map.insert var ((Zero,Zero),Leaf) tc

bRaceStar :: Cont -> Maybe (Cont, Term -> Term, TypedVar)
bRaceStar gamma = case findfirstSpecialType (varsStar gamma) Int of
		  Nothing -> Nothing
		  Just x  -> Just (removeVarStar gamma (fst x), \m -> BCase (Var (fst x)) m, x)

bRaceStar_tc_update :: TermCont -> TermVar -> TermCont
bRaceStar_tc_update tc var = Map.insert var ((Brace,Brace),Leaf) tc

bOolStar :: Cont -> Maybe (Cont, Term -> Term, TypedVar)
bOolStar gamma = case findfirstSpecialType (varsStar gamma) Int of
	         Nothing -> Nothing
		 Just x  -> Just (removeVarStar gamma (fst x), \m -> BoolCase (Var (fst x)) m, x)

bOolStar_tc_update :: TermCont -> TermVar -> TermCont
bOolStar_tc_update tc var = Map.insert var ((Fls,Fls),Leaf) tc

lIstStar :: Cont -> Maybe (M (Cont, Term -> Term, TypedVar))
lIstStar gamma = case findfirst typeCheckList (varsStar gamma) of
	         Nothing -> Nothing
		 Just x  -> Just (do {i <- newInt;
				      let y = TermVar i in
				      return (removeVarStar gamma (fst x), \m -> LCase (Var (fst x)) y m, x)
				     })

lIstStar_tc_update :: TermCont -> TypedVar -> M TermCont
lIstStar_tc_update = pLusVal_tc_update

mAybeStar :: Cont -> Maybe (M (Cont, Term -> Term, TypedVar))
mAybeStar gamma = case findfirst typeCheckMaybe (varsStar gamma) of
	         Nothing -> Nothing
		 Just x  -> Just (do {i <- newInt;
				      let y = TermVar i in
				      return (removeVarStar gamma (fst x), \m -> MCase (Var (fst x)) y m, x)
				     })

mAybeStar_tc_update :: TermCont -> TypedVar -> M TermCont
mAybeStar_tc_update = pLusVal_tc_update

pAirStar :: Cont -> Maybe (M (Cont, Term -> Term, TypedVar))
pAirStar gamma = case findfirst typeCheckPair (varsStar gamma) of
	         Nothing -> Nothing
		 Just x  -> Just (do {i <- newInt;
				      j <- newInt;
				      let y = TermVar i 
				          z = TermVar j in
				      return (removeVarStar gamma (fst x), \m -> PCase (Var (fst x)) y z m, x)
				     })

pAirStar_tc_update :: TermCont -> TypedVar -> M TermCont
pAirStar_tc_update = pLusVal_tc_update

eItherStar :: Cont -> Typ -> Maybe (M (Cont, Term -> Term, TypedVar))
eItherStar gamma tau = case findfirst typeCheckEither (varsStar gamma) of
	         Nothing -> Nothing
		 Just x  -> Just (do {i <- newInt;
				      j <- newInt;
				      let y = TermVar i 
				          z = TermVar j in
				      return (removeVarStar gamma (fst x), \m -> ECase (Var (fst x)) y m z (Bottom tau), x)
				     })

eItherStar_tc_update :: TermCont -> TypedVar -> M TermCont
eItherStar_tc_update = pLusVal_tc_update

-- *** rules with backtracking

dIstStar1 :: Cont -> Typ -> Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))
dIstStar1 gamma tau = case findfirst typeCheckEither (varsStar gamma) of
                    Nothing -> Nothing
                    Just (e, TEither tau1 tau2) ->
		         Just (do {i <- newInt;
			   	   j <- newInt;
				   let x = TermVar i
			               y = TermVar j in
				   return ((updateVarStar (removeVarStar gamma e) x tau1,
					   \m -> subst m (ECase (Var e) x (Var x) y (Bottom tau1)) x),
					   ((x,tau1),(e,TEither tau1 tau2)))
				  })

dIstStar1_tc_update :: TermCont -> TypedVar -> TypedVar -> TermCont
dIstStar1_tc_update tc x e = let ((z,z'),his) = (trace "Map.!-check: dIstStar1 x" (tc Map.! (fst x)))
			   in
			   Map.delete (fst x) (Map.insert (fst e) ((Left z, Left z'),Branch Dist1 his) tc)

dIstStar2 :: Cont -> Typ -> Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))
dIstStar2 gamma tau = case findfirst typeCheckEither (varsStar gamma) of
                    Nothing -> Nothing
                    Just (e, TEither tau1 tau2) ->
		         Just (do {i <- newInt;
			   	   j <- newInt;
				   let x = TermVar i
			               y = TermVar j in
				   return ((updateVarStar (removeVarStar gamma e) y tau2,
					   \m -> subst m (ECase (Var e) x (Bottom tau1) y (Var y)) y),
					   ((y,tau2),(e,TEither tau1 tau2)))
				  })

dIstStar2_tc_update :: TermCont -> TypedVar -> TypedVar -> TermCont
dIstStar2_tc_update tc y e = let ((z,z'),his) = (trace "Map.!-check: dIstStar2 y" (tc Map.! (fst y)))
                           in
			   Map.delete (fst y) (Map.insert (fst e) ((Right z, Right z'),Branch Dist2 his) tc)

-- ** last phase for plus term search

vArStripe :: Cont -> Typ -> Maybe (Term, TypedVar)
vArStripe gamma tau = case findfirstSpecialType (vars gamma) tau of
                     Nothing -> Nothing
		     Just x  -> Just (Var (fst x), x)

iNtStripe :: Typ -> Maybe Term
iNtStripe tau = if tau == Int then Just Zero else Nothing
                     
bRaceStripe :: Typ -> Maybe Term
bRaceStripe tau = if tau == TBrace then Just Brace else Nothing

bOolStripe :: Typ -> Maybe Term
bOolStripe tau = if tau == TBool then Just Fls else Nothing

lIstStripe :: Typ -> Maybe Term
lIstStripe tau = if typeCheckList tau then let List tau' = tau in Just (Cons (Bottom tau') (Nil tau')) else Nothing

mAybeStripe :: Typ -> Maybe Term
mAybeStripe tau = if typeCheckMaybe tau then let TMaybe tau' = tau in Just (MJust (Bottom tau')) else Nothing

pAirStripe :: Typ -> Maybe Term
pAirStripe tau = if typeCheckPair tau then let TPair tau1 tau2 = tau in Just (Pair (Bottom tau1) (Bottom tau2)) else Nothing

eItherStripe :: Typ -> Maybe Term
eItherStripe tau = if typeCheckEither tau then let TEither tau1 tau2  = tau in Just (Left (Bottom tau1)) else Nothing

-- | creates the initial term variable environment.
stripePhase_tc_update :: Cont -> M TermCont
stripePhase_tc_update gamma = initialiseTermCont ((vars gamma) ++ (varsStar gamma))



-- * The algorithm
--Note: pointed checks are omitted whenever possible, because pointedness is clear out of the rules order, especially because (Drop_3) is used very early

-- ** first phase

alg :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg gamma tau termCont = do track (makeTrackString "Start Conf" gamma tau)
			    (t,tc,trc) <- alg1 gamma tau termCont
--			    return (simplifyTerm t, simplifyTermCont tc, simplifyTrackCont trc) --returns simplified terms
			    return (t, tc, trc)                                --returns the terms without simplification

alg1 :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg1 = traceIOStart traceIOFile alg1_Bottom

alg1_Bottom :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg1_Bottom gamma tau termCont = case bOttom gamma tau of
		               Nothing -> alg1_RAllStar gamma tau termCont
			       Just t  -> do track ((makeTrackString "Bottom" gamma tau) ++ "  !!END OF BRANCH!!")
                                             tc <- bOttom_tc_update gamma
				             return (t,tc,(tau,[]))
				      
alg1_RAllStar :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg1_RAllStar gamma tau termCont = case rAllStar gamma tau of
			           Nothing                -> alg1_RAll gamma tau termCont
			           Just (gamma', tau', f) -> do track (makeTrackString "RAllStar" gamma' tau')
								(t,c,trc) <- (alg1 gamma' tau' termCont)
					              	        traceIO "RAll*" tau gamma tau' gamma' (return (f t, c, trc))
							      
alg1_RAll :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg1_RAll gamma tau termCont = case rAll gamma tau of
		               Nothing                -> alg1_Drop3 gamma tau termCont
			       Just (gamma', tau', f) -> do {track (makeTrackString "RAll" gamma' tau');
							     (t,c, trc) <- (alg1 gamma' tau' termCont);
							     traceIO "RAll" tau gamma tau' gamma' (return (f t,c,trc))
							    }
		
alg1_Drop3 :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)				     
alg1_Drop3 gamma tau termCont = case dRop3 gamma of
                               Nothing         -> alg1_Drop1 gamma tau termCont
                               Just (gamma',v) -> do{track (makeTrackString "Drop_3" gamma' tau);
					             (t,c,trc) <- (traceIO "Drop_3" tau gamma tau gamma' (alg1 gamma' tau termCont));
                                                     tc <- dRop3_tc_update c v;
						     return (t,tc,trc)
						    }

alg1_Drop1 gamma tau termCont = case dRop1 gamma of
		               Nothing         -> alg1_Drop2 gamma tau termCont
			       Just (gamma',v) -> do{track (makeTrackString "Drop_1" gamma' tau);
				                     (t,c,trc) <- (traceIO "Drop_1" tau gamma tau gamma' (alg1 gamma' tau termCont));
						     return (t,dRop1_tc_update c v,trc)
						    }

alg1_Drop2 gamma tau termCont = case dRop2 gamma of
		               Nothing         -> alg1_Drop4 gamma tau termCont
			       Just (gamma',v) -> do{track (makeTrackString "Drop_2" gamma' tau);
				                     (t,c,trc) <- (traceIO "Drop_2" tau gamma tau gamma' (alg1 gamma' tau termCont));
						     return (t,dRop2_tc_update c v,trc)
						    }

alg1_Drop4 gamma tau termCont = case dRop4 gamma of
		               Nothing         -> alg1_Abs gamma tau termCont
			       Just (gamma',v) -> do{track (makeTrackString "Drop_4" gamma' tau);
				                     (t,c,trc) <- (traceIO "Drop_4" tau gamma tau gamma' (alg1 gamma' tau termCont));
						     return (t,dRop4_tc_update c v,trc)
						    }

alg1_Abs :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg1_Abs gamma tau termCont = case aBs gamma tau of 
			         Nothing           -> alg1_WrapTo gamma tau termCont
			         Just (comp, tau') -> do {(gamma', x, f) <- comp;
							  track (makeTrackString "Abs" gamma' tau');					
							  (t,c,trc) <- (traceIO "Abs" tau gamma tau' gamma' (alg1 gamma' tau' termCont));
							  trc' <- aBs_trackCont_update trc tau c x;
							  return (f t,aBs_tc_update c x,trc')
							 }
				           
alg1_WrapTo :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg1_WrapTo gamma tau termCont = case wRapTo gamma of
                                  Nothing   -> alg1_MaybeTo gamma tau termCont
			          Just comp -> do {((gamma',f),(g,k)) <- comp;
						   track (makeTrackString "Wrap->" gamma' tau);
                                                   (t,c, trc) <- traceIO "Wrap->" tau gamma tau gamma' (alg1 gamma' tau termCont);
						   i <- newInt;
						   j <- newInt;
						   let l = TermVar i
						       h = TermVar j in
						   return (f t,wRapTo_tc_update c l h g k, trc)
						  }

alg1_MaybeTo :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg1_MaybeTo gamma tau termCont = case mAybeTo gamma of
                                  Nothing   -> alg1_Head gamma tau termCont
			          Just comp -> do {((gamma',f),(g,k)) <- comp;
						   track (makeTrackString "Maybe->" gamma' tau);
                                                   (t,c, trc) <- traceIO "Maybe->" tau gamma tau gamma' (alg1 gamma' tau termCont);
						   i <- newInt;
						   j <- newInt;
						   let l = TermVar i
						       h = TermVar j in
						   return (f t,mAybeTo_tc_update c l h g k, trc)
						  }

alg1_Head :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg1_Head gamma tau termCont = case hEad gamma tau of
                             Nothing     -> alg1_Just gamma tau termCont
                             Just comp -> do {((gamma',f),(h,l)) <- comp;
					      track (makeTrackString "Head" gamma' tau);
					      (t,c,trc) <- traceIO "Head" tau gamma tau gamma' (alg1 gamma' tau termCont);
					      return (f t, hEad_tc_update c h l, trc)
					     }

alg1_Just :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg1_Just gamma tau termCont = case jUst gamma tau of
                             Nothing     -> alg1_PairTo gamma tau termCont
                             Just comp -> do {((gamma',f),(h,l)) <- comp;
					      track (makeTrackString "Just" gamma' tau);
					      (t,c,trc) <- traceIO "Just" tau gamma tau gamma' (alg1 gamma' tau termCont);
					      return (f t, jUst_tc_update c h l, trc)
					     }

alg1_PairTo gamma tau termCont = case pAirTo gamma of
			          Nothing    -> alg1_Proj gamma tau termCont
                                  Just comp  -> do {((gamma',f),(g,h)) <- comp;
						    track(makeTrackString "Pair->" gamma' tau);
						    (t,c,trc) <- traceIO "Pair->" tau gamma tau gamma' (alg1 gamma' tau termCont);
						    termCont' <- pAirTo_tc_update c g h;
						    return (f t, termCont',trc)
						   }

alg1_Proj gamma tau termCont = case pRoj gamma of
		             Nothing    -> alg1_EitherTo gamma tau termCont
                             Just comp  -> do {((gamma',f),(varIn,p)) <- comp;
					       track(makeTrackString "Proj" gamma' tau);
					       (t,c,trc) <- traceIO "Proj" tau gamma tau gamma' (alg1 gamma' tau termCont);
					       return (f t, pRoj_tc_update c varIn p,trc)
					      }

alg1_EitherTo gamma tau termCont = case eItherTo gamma of
                                  Nothing   -> alg1_Dist1 gamma tau termCont
                                  Just comp -> do {((gamma',f),(varIn,g)) <- comp;
						   track (makeTrackString "LE->" gamma' tau);
						   (t,c,trc) <- traceIO "LE->" tau gamma tau gamma' (alg1 gamma' tau termCont);
						   termCont' <- eItherTo_tc_update c varIn g;
						   return (f t, termCont',trc)
						  }

alg1_Dist1 gamma tau termCont = case dIst1 gamma tau of
			      Nothing   -> alg1_BottomToStripe gamma tau termCont
			      Just comp -> do {((gamma',f),(x,e)) <- comp;
					   let subderivation =
					           do  track (makeTrackString "Dist1" gamma' tau)
					               (t,c,trc) <- traceIO "Dist1" tau gamma tau gamma' (alg1 gamma' tau termCont);
					               return (f t, dIst1_tc_update c x e,trc)
					   in
					   choice subderivation (alg1_Dist2 gamma tau termCont);
					  }

alg1_Dist2 gamma tau termCont = case dIst2 gamma tau of
			      Nothing   -> alg1_BottomToStripe gamma tau termCont --should never be reached
			      Just comp -> do {((gamma',f),(y,e)) <- comp;
					       track (makeTrackString "Dist2" gamma' tau);
					       (t,c,trc) <- traceIO "Dist2" tau gamma tau gamma' (alg1 gamma' tau termCont);
					       return (f t, dIst2_tc_update c y e,trc)
					      }

					
alg1_BottomToStripe :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg1_BottomToStripe gamma tau termCont = foldr choice (alg1_ArrowToStar gamma tau termCont) (map trysubderivations (bOttomToStripe gamma))
			              where trysubderivations = \l -> do {((gamma', f),(x,g)) <- l; 
									  track (makeTrackString "Bottom->'" gamma' tau);
									  (t,c,trc) <- traceIO "Bottom->'" tau gamma tau gamma' (alg2 gamma' tau termCont);
									  tc <- bOttomToStripe_tc_update c gamma x g;
								          return (f t, tc, trc)
									 }

alg1_ArrowToStar :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg1_ArrowToStar gamma tau termCont = 
     foldr choice (alg1_Wrap gamma tau termCont) (map trysubderivations (aRrowToStar gamma))
     where trysubderivations = \l -> do {(((gamma1, tau1), gamma2, f),([w,y],g)) <- l;
					 track (makeTrackString "Arrow->* (fst)" gamma1 tau1);
					 track (makeTrackString "Arrow->* (snd)" gamma2 tau);
					 (t1,c1,trc1) <- traceIO "Arrow->* (fst)" tau gamma tau1 gamma1 (alg1 gamma1 tau1 termCont);
					 (t2,c2,trc2) <- traceIO "Arrow->* (snd)" tau gamma tau gamma2 (alg2 gamma2 tau termCont);
					 let cont = mergeTermCont c1 c2 in
					 (case cont of
                                           Nothing -> abort
                                           Just c  -> do {tc <- aRrowToStar_tc_update trc1 c gamma t1 w y g;
							  return (f t1 t2,tc,trc2)
							 }
					 )
					}

alg1_Wrap :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg1_Wrap gamma tau termCont = case wRap tau of
                               Nothing        -> alg1_Maybe gamma tau termCont
                               Just (tau', f) -> do track (makeTrackString "Wrap" gamma tau')						  
				  		    (t,c,trc) <- traceIO "Wrap" tau gamma tau' gamma (alg1 gamma tau' termCont)
                                                    trc' <- wRap_trackCont_update trc tau
					            return (f t,c,trc')

alg1_Maybe :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg1_Maybe gamma tau termCont = case mAybe tau of
                                Nothing        -> alg1_Pair1 gamma tau termCont
                                Just (tau', f) -> do track (makeTrackString "Maybe" gamma tau')
                                                     (t,c,trc) <- traceIO "Maybe" tau gamma tau' gamma (alg1 gamma tau' termCont)
                                                     trc' <- mAybe_trackCont_update trc tau
					             return (f t,c,trc')

alg1_Pair1 gamma tau termCont = case pAir1 tau of
                              Nothing        -> alg1_Left gamma tau termCont
                              Just (tau', f) -> choice subderivation (alg1_Pair2 gamma tau termCont)
	                                         where subderivation = do {track (makeTrackString "Pair1" gamma tau');
									   (t,c,trc) <- traceIO "Pair1" tau gamma tau' gamma (alg1 gamma tau' termCont);
									   trc' <-pAir1_trackCont_update trc tau;
							                   return (f t, c, trc')
									  }
  
alg1_Pair2 gamma tau termCont = case pAir2 tau of
		              Nothing        -> alg1_Left gamma tau termCont
                              Just (tau', f) -> do {track (makeTrackString "Pair2" gamma tau');
						    (t,c,trc) <- traceIO "Pair2" tau gamma tau' gamma (alg1 gamma tau' termCont);
						    trc' <- pAir2_trackCont_update trc tau;
					            return (f t,c,trc')
						   }

alg1_Left gamma tau termCont = case lEft tau of
                              Nothing        -> alg1_BottomTo gamma tau termCont
                              Just (tau', f) -> choice subderivation (alg1_Right gamma tau termCont)
			                        where subderivation = do {track (makeTrackString "Left" gamma tau');
									  (t,c,trc) <- traceIO "Left" tau gamma tau' gamma (alg1 gamma tau' termCont);
									  trc' <- lEft_trackCont_update trc tau;
							                  return (f t,c, trc')
									 }
									  
alg1_Right gamma tau termCont = case rIght tau of
		              Nothing        -> alg1_BottomTo gamma tau termCont
                              Just (tau', f) -> do {track (makeTrackString "Right" gamma tau');
						    (t,c,trc) <- traceIO "Right" tau gamma tau' gamma (alg1 gamma tau' termCont);
						    trc' <- rIght_trackCont_update trc tau;
					            return (f t,c,trc')
						   }

alg1_BottomTo :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg1_BottomTo gamma tau termCont = 
     foldr choice (do {track "Bottom->:  !!FAIL!!"; abort}) (map trysubderivations (bOttomTo gamma))
     where trysubderivations = \l -> do {((gamma', f),(x,g)) <- l;
					 track (makeTrackString "Bottom->" gamma' tau);
					 (t,c,trc) <- traceIO "Bottom->" tau gamma tau gamma' (alg1 gamma' tau termCont);
					 i <- newInt;
					 let z = TermVar i in
					 return (f t,bOttomTo_tc_update c z x g,trc)
					}

-- ** second phase

alg2 :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg2 = alg2_VarStar

alg2_VarStar :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg2_VarStar gamma tau termCont = case vArStar gamma tau of
                                 Nothing     -> alg2_BottomToStar gamma tau termCont
                                 Just (t,v)  -> do track ((makeTrackString "Var*" gamma tau) ++ "  !!END OF BRANCH!!")
                                                   tc <- vArStar_tc_update gamma
                                                   return (t, tc, (tau,[]))

alg2_BottomToStar :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg2_BottomToStar gamma tau termCont = case bOttomToStar gamma of
				       Nothing -> alg2_AppStripStar gamma tau termCont
				       Just (comp) 
					       -> do {((gamma', f),(varIn,varOut)) <- comp;
						      track (makeTrackString "Bottom->*" gamma' tau);
						      (t,c,trc) <- traceIO "Bottom->*" tau gamma tau gamma' (alg2 gamma' tau termCont);
						      i <- newInt;
						      let x = TermVar i in
						      return (f t, bOttomToStar_tc_update c x varIn varOut, trc)
						     }

alg2_AppStripStar :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg2_AppStripStar gamma tau termCont = case aPpStripStar gamma of
				       Nothing   -> alg2_IntStar gamma tau termCont
				       Just comp -> do {((gamma', f),([x,y],g)) <- comp;
							track (makeTrackString "App'*" gamma' tau);
							(t,c,trc) <- traceIO "App'*" tau gamma tau gamma' (alg2 gamma' tau termCont);
							i <- newInt;
							let u = TermVar i in
							do{tc <- aPpStripStar_tc_update c gamma u x y g;
							   return (f t, tc,trc)
							  }
						       }

alg2_IntStar gamma tau termCont = 
    case iNtStar gamma of
    Nothing           -> alg2_BraceStar gamma tau termCont
    Just (gamma',f,v) -> do {let subderivation =
			            do {track (makeTrackString "Int*" gamma' tau);
					(t,c,trc) <- traceIO "Int*" tau gamma tau gamma' (alg3 gamma' tau termCont);
					return (f t, iNtStar_tc_update c (fst v), trc)
				       }
			     in
			     choice subderivation (alg2_HeadStar gamma tau termCont)
			    }

alg2_BraceStar gamma tau termCont = 
    case bRaceStar gamma of
    Nothing           -> alg2_BoolStar gamma tau termCont
    Just (gamma',f,v) -> do {let subderivation =
			            do {track (makeTrackString "Brace*" gamma' tau);
					(t,c,trc) <- traceIO "Brace*" tau gamma tau gamma' (alg3 gamma' tau termCont);
					return (f t, bRaceStar_tc_update c (fst v), trc)
				       }
			     in
			     choice subderivation (alg2_HeadStar gamma tau termCont)
			    }


alg2_BoolStar gamma tau termCont = 
    case bOolStar gamma of
    Nothing           -> alg2_ListStar gamma tau termCont
    Just (gamma',f,v) -> do {let subderivation =
			            do {track (makeTrackString "Bool*" gamma' tau);
					(t,c,trc) <- traceIO "Bool*" tau gamma tau gamma' (alg3 gamma' tau termCont);
					return (f t, bOolStar_tc_update c (fst v), trc)
				       }
			     in
			     choice subderivation (alg2_HeadStar gamma tau termCont)
			    }

alg2_ListStar gamma tau termCont = case lIstStar gamma of
			        Nothing -> alg2_MaybeStar gamma tau termCont
                                Just comp -> do {(gamma',f,v) <- comp;
						 let subderivation =
						        do {track (makeTrackString "List*" gamma' tau);
							    (t,c,trc) <- traceIO "List*" tau gamma tau gamma' (alg3 gamma' tau termCont);
							    cont <- lIstStar_tc_update c v;
							    return (f t, cont, trc)
							   }
						 in
						 choice subderivation (alg2_HeadStar gamma tau termCont)
					}

alg2_MaybeStar gamma tau termCont = case mAybeStar gamma of
			        Nothing -> alg2_PairStar gamma tau termCont
                                Just comp -> do {(gamma',f,v) <- comp;
						 let subderivation =
						        do {track (makeTrackString "Maybe*" gamma' tau);
							    (t,c,trc) <- traceIO "Maybe*" tau gamma tau gamma' (alg3 gamma' tau termCont);
							    cont <- mAybeStar_tc_update c v;
							    return (f t, cont, trc)
							   }
						 in
						 choice subderivation (alg2_JustStar gamma tau termCont)
					}


alg2_PairStar gamma tau termCont = case pAirStar gamma of
			        Nothing -> alg2_EitherStar gamma tau termCont
                                Just comp -> do {(gamma',f,v) <- comp;
						 let subderivation =
						        do {track (makeTrackString "Pair*" gamma' tau);
							    (t,c,trc) <- traceIO "Pair*" tau gamma tau gamma' (alg3 gamma' tau termCont);
							    cont <- pAirStar_tc_update c v;
							    return (f t, cont, trc)
							   }
						 in
						 choice subderivation (alg2_ProjStar gamma tau termCont)
					}

alg2_EitherStar gamma tau termCont = case eItherStar gamma tau of
			        Nothing -> do {track "abort: Either*";
					       abort
					      }
                                Just comp -> do {(gamma',f,v) <- comp;
						 let subderivation =
						        do {track (makeTrackString "Either*" gamma' tau);
							    (t,c,trc) <- traceIO "Either*" tau gamma tau gamma' (alg3 gamma' tau termCont);
							    cont <- eItherStar_tc_update c v;
							    return (f t, cont, trc)
							   }
						 in
						 choice subderivation (alg2_DistStar1 gamma tau termCont)
					}

alg2_HeadStar :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg2_HeadStar gamma tau termCont = case hEadStar gamma tau of
                                 Nothing   -> alg2_JustStar gamma tau termCont
			         Just comp -> do {((gamma', f),(h,l)) <- comp;
						  track (makeTrackString "Head*" gamma' tau);
						  (t,c,trc) <- traceIO "Head*" tau gamma tau gamma' (alg2 gamma' tau termCont);
						  return (f t, hEadStar_tc_update c h l, trc)
						 }

alg2_JustStar :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg2_JustStar gamma tau termCont = case jUstStar gamma tau of
                                 Nothing   -> alg2_ProjStar gamma tau termCont
			         Just comp -> do {((gamma', f),(h,l)) <- comp;
						  track (makeTrackString "Just*" gamma' tau);
						  (t,c,trc) <- traceIO "Just*" tau gamma tau gamma' (alg2 gamma' tau termCont);
						  return (f t, jUstStar_tc_update c h l, trc)
						 }

alg2_ProjStar gamma tau termCont = case pRojStar gamma of
			          Nothing   -> alg2_DistStar1 gamma tau termCont
			          Just comp -> do {((gamma', f),(h,p)) <- comp;
						   track (makeTrackString "Proj*" gamma' tau);
						   (t,c,trc) <- traceIO "Proj*" tau gamma tau gamma' (alg2 gamma' tau termCont);
						   return (f t, pRojStar_tc_update c h p, trc)
						  }


alg2_DistStar1 gamma tau termCont = case dIstStar1 gamma tau of
			         Nothing   -> do {track "abort: Dist*1"; --should never be reached
						  abort
						 }
			         Just comp -> do {((gamma',f),(x,e)) <- comp;
						  let subderivation =
					                 do {track (makeTrackString "Dist*1" gamma' tau);
					                     (t,c,trc) <- traceIO "Dist*1" tau gamma tau gamma' (alg2 gamma' tau termCont);
							     return (f t, dIstStar1_tc_update c x e, trc)
							    }
						  in
						  choice subderivation (alg2_DistStar2 gamma tau termCont)
						 }

alg2_DistStar2 gamma tau termCont  = case dIstStar2 gamma tau of
			          Nothing   -> do {track "abort: Dist*2"; --should never be reached
						   abort
						  }
			          Just comp -> do {((gamma',f),(y,e)) <- comp;
						   track (makeTrackString "Dist*2" gamma' tau);
						   (t,c,trc) <- traceIO "Dist*2" tau gamma tau gamma' (alg2 gamma' tau termCont);
						   return (f t, dIstStar2_tc_update c y e, trc)
						  }

-- ** third phase

alg3 = alg3_VarStripe

alg3_VarStripe gamma tau termCont = 
    case vArStripe gamma tau of
    Nothing      -> alg3_IntStripe gamma tau termCont
    Just (t,var) -> do {track ((makeTrackString "Var'" gamma tau) ++ "  !!END OF BRANCH!!");
			tc <- stripePhase_tc_update gamma;
                        return (t, tc, (tau,[]))
		       }

alg3_IntStripe gamma tau termCont = 
    case iNtStripe tau of
    Nothing  -> alg3_BraceStripe gamma tau termCont
    Just t   -> do {track ((makeTrackString "Int'" gamma tau) ++ "  !!END OF BRANCH!!");
		    tc <- stripePhase_tc_update gamma;
                    return (t, tc, (tau,[]))
		   }

alg3_BraceStripe gamma tau termCont = 
    case bRaceStripe tau of
    Nothing -> alg3_BoolStripe gamma tau termCont
    Just t  -> do {track ((makeTrackString "Brace'" gamma tau) ++ "  !!END OF BRANCH!!");
		   tc <- stripePhase_tc_update gamma;
                   return (t, tc, (tau,[]))
		  }

alg3_BoolStripe gamma tau termCont = 
    case bOolStripe tau of
    Nothing -> alg3_ListStripe gamma tau termCont
    Just t  -> do {track ((makeTrackString "Bool'" gamma tau) ++ "  !!END OF BRANCH!!");
		   tc <- stripePhase_tc_update gamma;
                   return (t, tc, (tau,[]))
		  }

alg3_ListStripe gamma tau termCont = 
    case lIstStripe tau of
    Nothing -> alg3_MaybeStripe gamma tau termCont
    Just t  -> do {track ((makeTrackString "List'" gamma tau) ++ "  !!END OF BRANCH!!");
		   tc <- stripePhase_tc_update gamma;
                   return (t, tc, (tau,[]))
		  }

alg3_MaybeStripe gamma tau termCont = 
    case mAybeStripe tau of
    Nothing -> alg3_PairStripe gamma tau termCont
    Just t  -> do {track ((makeTrackString "Maybe'" gamma tau) ++ "  !!END OF BRANCH!!");
		   tc <- stripePhase_tc_update gamma;
                   return (t, tc, (tau,[]))
		  }

alg3_PairStripe gamma tau termCont = 
    case pAirStripe tau of
    Nothing -> alg3_EitherStripe gamma tau termCont
    Just t  -> do {track ((makeTrackString "Pair'" gamma tau) ++ "  !!END OF BRANCH!!");
		   tc <- stripePhase_tc_update gamma;
                   return (t, tc, (tau,[]))
		  }

alg3_EitherStripe gamma tau termCont = 
    case lIstStripe tau of
    Nothing -> do {track "Either': FAIL";
		   abort
		  }
    Just t  -> do {track ((makeTrackString "Either'" gamma tau) ++ "  !!END OF BRANCH!!");
		   tc <- stripePhase_tc_update gamma;
                   return (t, tc, (tau,[]))
		  }