Daniels Stand von 20081110
[darcs-mirror-polyfix.git] / ExFindExtended.hs
1 module ExFindExtended (TypVar(..),Typ(..),TermVar(..),Term,TermCont,TermPlus,PlusElem(..),AbsTerm(..),testTerm,getTerm,getComplete,showTerm,showUsedTermCont,getCompleteRaw,getWithDebug,getIt) where
2
3 import Prelude hiding (Either(..))
4 import qualified Prelude as E (Either(..))
5 import Data.List
6 import qualified Data.Map as Map
7 import Control.Monad
8 import M
9 import ParseType
10 --import Debug.Trace
11 trace string a = a
12 -- newInt :: M Int
13 -- runM :: M a -> a
14
15 type TypedVar = (TermVar,Typ)
16 type TermCont = Map.Map TermVar (TermPlus,TermPlus)
17
18 --newtype TypVar = TypVar Int deriving (Show, Eq)
19
20 --data Typ    = TVar    TypVar
21 --          | Arrow   Typ     Typ
22 --          | All     TypVar  Typ       --wir geben Typen ohne Quantifier an
23 --          | AllStar TypVar  Typ
24 --          | List    Typ
25 --          deriving (Show, Eq)
26
27 newtype TermVar = TermVar Int deriving (Show, Eq, Ord)
28
29 data PlusElem = PlusElem TypVar Int deriving (Show, Eq)
30
31 type Term = AbsTerm ()
32 type TermPlus = AbsTerm PlusElem
33 data AbsTerm a  = Var TermVar   
34             | Abs     TermVar     Typ         (AbsTerm a)
35             | App     (AbsTerm a) (AbsTerm a)
36             | TAbs    TypVar      (AbsTerm a)
37 --          | TApp    Term    Typ       -- nie benutzt
38             | Nil     Typ
39             | Cons    (AbsTerm a) (AbsTerm a) 
40             | Case    (AbsTerm a) (AbsTerm a) TermVar     (AbsTerm a)
41             | Bottom  Typ               -- statt Fix
42 --          | GoalTerm Cont Typ         -- nur temporaer
43 --          | Subst    Term Term TermVar-- nur temporaer
44 --          | Alg2     Cont Typ --nur temporaer
45 --          Erweiterung fuer die Beispielkonstruktion
46             | Extra    a 
47             -- case    x       of {y        ->  z;     _ -> w}
48             | Case1    (AbsTerm a) (AbsTerm a)  (AbsTerm a) (AbsTerm a)
49 ------------Erweiterung fuer Extended Algorithmus
50             | Zero
51             | Pair     (AbsTerm a) (AbsTerm a)
52             | PCase    (AbsTerm a) TermVar      TermVar     (AbsTerm a)
53             | ECase    (AbsTerm a) TermVar      (AbsTerm a) TermVar     (AbsTerm a)
54             | Right    (AbsTerm a)
55             | Left     (AbsTerm a)
56             deriving (Show, Eq)
57
58
59 data Cont   = Cont { tVars :: [TypVar], tVarsStar :: [TypVar], vars :: [(TermVar,Typ)], varsStar :: [(TermVar,Typ)] } deriving (Show,Eq) --TODO: Eq wieder loeschen
60
61 emptyCont :: Cont
62 emptyCont = Cont [] [] [] []
63
64 emptyTermCont :: TermCont
65 emptyTermCont = Map.empty
66
67 term2PlusTerm :: Term -> TermPlus
68 term2PlusTerm t =
69     case t of
70       Var v -> Var v   
71       Abs v tau t1 -> Abs v tau (term2PlusTerm t1) 
72       App t1 t2 -> App (term2PlusTerm t1) (term2PlusTerm t2)
73       TAbs v t1 -> TAbs v (term2PlusTerm t1)
74       Nil tau -> Nil tau
75       Cons t1 t2 -> Cons (term2PlusTerm t1) (term2PlusTerm t2) 
76       Case t1 t2 v t3 -> Case (term2PlusTerm t1) (term2PlusTerm t2) v (term2PlusTerm t3)
77       Bottom  tau -> Bottom tau
78       Case1 t1 t2 t3 t4 -> Case1 (term2PlusTerm t1) (term2PlusTerm t2) (term2PlusTerm t3) (term2PlusTerm t4)
79       Zero -> Zero
80       Pair t1 t2 -> Pair (term2PlusTerm t1) (term2PlusTerm t2)
81       PCase t1 v1 v2 t2 -> PCase (term2PlusTerm t1) v1 v2 (term2PlusTerm t2)
82       ECase t1 v1 t2 v2 t3 -> ECase (term2PlusTerm t1) v1 (term2PlusTerm t2) v2 (term2PlusTerm t3)
83       Right t1 -> term2PlusTerm t1
84       Left  t1 -> term2PlusTerm t1
85
86 updateTVarStar (Cont tVars tVarsStar vars varsStar) tv = Cont tVars (tv:tVarsStar) vars varsStar
87
88 updateTVar (Cont tVars tVarsStar vars varsStar) tv = Cont (tv:tVars) tVarsStar vars varsStar
89
90 updateVar (Cont tVars tVarsStar vars varsStar) v tau = Cont tVars tVarsStar ((v,tau):vars) varsStar
91 removeVar (Cont tVars tVarsStar vars varsStar) var = Cont tVars tVarsStar (filter ((/= var).fst) vars) varsStar
92
93 updateVarStar (Cont tVars tVarsStar vars varsStar) v tau = Cont tVars tVarsStar vars  ((v,tau):varsStar)
94 removeVarStar (Cont tVars tVarsStar vars varsStar) var = Cont tVars tVarsStar vars  (filter ((/= var).fst) varsStar)
95
96 unpointed tvars tau = case tau of
97                       TVar tvar      -> case find (== tvar) tvars of
98                                           Nothing -> False
99                                           _       -> True
100                       Arrow _ tau'   -> unpointed tvars tau'
101                       All tvar tau'  -> unpointed (tvar:tvars) tau'
102                       AllStar _ tau' -> unpointed tvars tau'
103                       List _         -> False
104                       Int            -> False
105                       TPair _ _      -> False
106                       TEither _ _    -> False
107
108 findfirstSpecialType vars typ =
109     case vars of
110       []     -> Nothing
111       (x:xs) -> if snd x == typ
112                 then Just x
113                 else findfirstSpecialType xs typ
114
115 findfirstWithTVars typecheckfunction tvars vars =
116     case vars of
117       []     -> Nothing
118       (x:xs) -> if typecheckfunction tvars (snd x)
119                 then Just x 
120                 else findfirstWithTVars typecheckfunction tvars xs
121
122 findallWithTVars typecheckfunction tvars vars = 
123     case vars of
124       []     -> []
125       (x:xs) -> if typecheckfunction tvars (snd x)
126                 then (x:(findallWithTVars typecheckfunction tvars xs))
127                 else findallWithTVars typecheckfunction tvars xs
128
129 findfirst typecheckfunction vars = case vars of
130                                      []     -> Nothing
131                                      (x:xs) -> if typecheckfunction (snd x) 
132                                                then Just x 
133                                                else findfirst typecheckfunction xs
134
135 findall typecheckfunction vars = case vars of
136                                    []     -> []
137                                    (x:xs) -> if typecheckfunction (snd x)
138                                              then (x:(findall typecheckfunction xs))
139                                              else findall typecheckfunction xs
140
141 -- fuer (lIArrow)
142 typeCheckArrowListArg tau = case tau of
143                               Arrow tau1 _ -> case tau1 of
144                                                 List _ -> True
145                                                 _      -> False
146                               _            -> False
147
148 typeCheckList tau = case tau of
149                      List _ -> True
150                      _      -> False
151
152 typeCheckArrowUnPointedArgPointedRes tvars tau = case tau of
153                                                    Arrow tau1 tau2 -> unpointed tvars tau1 && (not (unpointed tvars tau2))
154                                                    _               -> False
155
156 typeCheckArrowArgArrow tau = case tau of
157                               Arrow tau1 _ -> case tau1 of
158                                                 Arrow _ _ -> True
159                                                 _         -> False
160                               _            -> False
161
162 typeCheckArrow tau = case tau of
163                        Arrow _ _ -> True
164                        _         -> False
165
166 typeCheckInt tau = case tau of
167                      Int -> True
168                      _   -> False
169
170 typeCheckPair tau = case tau of
171                       TPair _ _ -> True
172                       _         -> False
173
174 typeCheckArrowPairArg tau = case tau of
175                               Arrow tau1 _ -> case tau1 of
176                                                 TPair _ _ -> True
177                                                 _         -> False
178                               _            -> False
179
180 typeCheckArrowEitherArg tau = case tau of
181                                 Arrow tau1 _ -> case tau1 of
182                                                   TEither _ _ -> True
183                                                   _           -> False
184                                 _            -> False
185
186 typeCheckEither tau = case tau of
187                         TEither _ _ -> True
188                         _           -> False
189
190 apply :: AbsTerm a -> [AbsTerm a] -> AbsTerm a
191 apply f args = case args of
192                 []    -> f
193                 x:xs  -> apply (App f x) xs
194
195 subst :: Term -> Term -> TermVar -> Term
196 subst m new old = case m of
197                    Var var           -> if(var == old) then new else m
198                    Abs v tau m'      -> Abs v tau (subst m' new old)
199                    App m1 m2         -> App (subst m1 new old) (subst m2 new old)
200                    TAbs tau m'       -> TAbs tau (subst m' new old)
201                    Cons m1 m2        -> Cons (subst m1 new old) (subst m2 new old)
202                    Case m0 m1 v2 m2  -> Case (subst m0 new old) (subst m1 new old) v2 (subst m2 new old)
203                    Pair m1 m2        -> Pair (subst m1 new old) (subst m2 new old)
204                    PCase m0 v1 v2 m1 -> PCase (subst m0 new old) v1 v2 (subst m1 new old)
205                    Right m           -> Right (subst m new old)
206                    Left m            -> Left (subst m new old)
207                    ECase m0 v1 m1 v2 m2 -> ECase (subst m0 new old) v1 (subst m1 new old) v2 (subst m2 new old)
208 --                 GoalTerm _ _  -> Subst m new old
209 --                 Subst _ _ _   -> Subst m new old
210 --                 Alg2 _ _       -> Subst m new old
211                    _                 -> m
212
213 makePlusPair :: Typ -> Maybe (AbsTerm PlusElem, AbsTerm PlusElem)
214 makePlusPair tau = let x = makePlusElem tau in 
215                            case x of 
216                              Just t -> Just (t,t)
217                              _      -> Nothing
218
219 makePlusElem :: Typ -> Maybe (AbsTerm (PlusElem))
220 makePlusElem tau = case tau of
221                    TVar  var         -> Just (Extra (PlusElem var 0))
222                    Arrow tau1 tau2   -> let x = makePlusElem tau2 in
223                                               case x of 
224                                                      Just t -> Just (Abs (TermVar 0) tau1 t)
225                                                      _      -> Nothing
226                    List  tau         -> let x = makePlusElem tau in
227                                               case x of 
228                                                      Just t -> Just (Cons t (Nil tau))
229                                                      _      -> Nothing
230                    Int               -> Just Zero
231                    TPair tau1 tau2   -> let x = makePlusElem tau1 in
232                                                 case x of
233                                                        Just t1 -> let y = makePlusElem tau2 in
234                                                                           case y of
235                                                                             Just t2 -> Just (Pair t1 t2)
236                                                                             Nothing -> Nothing
237                                                        Nothing -> Nothing
238                    
239                    TEither tau1 tau2 -> let x = makePlusElem tau1 in
240                                         case x of 
241                                           Just t1 -> Just (Left t1)
242                                           _       -> let x = makePlusElem tau2 in
243                                                      case x of
244                                                        Just t2 -> Just (Right t2)
245                                                        _       -> Nothing
246                    _                 -> Nothing
247
248 --the function equals the lemma about the function construction g_x(tau,t1), g'_x'(tau,t2)
249 --              (x_tau2,x'_tau2) -> tau -> (t1,t2) -> (g,g')
250 makeFuncPair :: TermCont -> Cont -> (TermPlus,TermPlus) -> Typ -> Typ -> (TermPlus,TermPlus) -> M (TermPlus,TermPlus)
251 makeFuncPair tc gamma resPair resTyp tau terms = makeFuncPair' tc gamma resPair resTyp tau tau ([],[]) terms
252
253 makeFuncPair' :: TermCont -> Cont -> (TermPlus,TermPlus) -> Typ -> Typ -> Typ -> ([TermPlus],[TermPlus]) -> (TermPlus,TermPlus) -> M (TermPlus,TermPlus)
254 makeFuncPair' tc gamma resPair resTyp tauAll tau args terms =
255     let (z,z') = resPair in
256     case tau of
257       TVar beta    -> case makePlusPair tau of
258                        Just (u,v) -> do {i <- newInt;
259                                          let w  = TermVar i
260                                              g' = Abs w tauAll (Case1 (apply (Var w) (snd args)) v z' z') in
261                                          if unpointed (tVars gamma) tau
262                                          then return (Abs w tauAll z, g')
263                                          else return (Abs w tauAll (Case1 (apply (Var w) (fst args)) u z z), g')
264                                         }
265       Int          -> do {i <- newInt;
266                           let w  = TermVar i in
267                           return (Abs w tauAll (Case1 (apply (Var w) (fst args)) Zero z z), Abs w tauAll (Case1 (apply (Var w) (snd args)) Zero z' z'))
268                          }
269
270       List tau'    -> case snd terms of
271                         Bottom _ -> do{i <- newInt;
272                                        j <- newInt;
273                                        let w   = TermVar i
274                                            h   = TermVar j 
275                                        in
276                                        return (Abs w tauAll (Case (apply (Var w) (fst args)) z h z), Abs w tauAll (Case (apply (Var w) (snd args)) z' h z'))
277                                        }
278                         Cons x _ -> let Cons y _ = snd terms in
279                                     do{i <- newInt;
280                                        j <- newInt;                                    
281                                        (g,g') <- makeFuncPair' tc gamma resPair resTyp tauAll tau' ([],[]) (x,y);
282                                        let w   = TermVar i
283                                            u   = TermVar j in
284                                        return (Abs w tauAll (Case1 (apply (Var w) (fst args)) (Cons (Var u) (Nil tau')) (App g  (Var u)) z),
285                                                Abs w tauAll (Case1 (apply (Var w) (snd args)) (Cons (Var u) (Nil tau')) (App g' (Var u)) z'))
286                                       }
287   
288       TPair tau' tau'' -> case snd terms of
289                             Bottom _ -> do{i <- newInt;
290                                            j <- newInt;
291                                            k <- newInt;
292                                            let w = TermVar i 
293                                                x = TermVar j
294                                                y = TermVar k
295                                            in
296                                            return (Abs w tauAll (PCase (apply (Var w) (fst args)) x y (App (App z (Var x)) (Var y))), Abs w tauAll (PCase (apply (Var w) (fst args)) x y (App (App z' (Var x)) (Var y))))
297                                           }
298                             Pair t21 t22 -> let Pair t11 t12 = fst terms in
299                                             do{i <- newInt;
300                                                j <- newInt;
301                                                k <- newInt;
302                                                l <- newInt;
303                                                let x = TermVar j
304                                                    y = TermVar k
305                                                    u = TermVar l
306                                                    w = TermVar i                                               
307                                                in
308                                                do{(k,k') <- case t22 of
309                                                               {Bottom _ -> if (unpointed (tVars gamma) tau'')
310                                                                            then makeFuncPair' tc gamma resPair resTyp tau'' tau'' ([],[]) (t12,t22)
311                                                                            else return (Abs u tau'' z, Abs u tau'' z');
312                                                                _        -> makeFuncPair' tc gamma resPair resTyp tau'' tau'' ([],[]) (t12,t22)};
313                                                   (h,h') <- case t21 of
314                                                               {Bottom _ -> if (unpointed (tVars gamma) tau'')
315                                                                            then makeFuncPair' tc gamma (k,k') (Arrow tau'' resTyp) tau' tau' ([],[]) (t11,t21)
316                                                                            else return (Abs x tau' (Abs y tau'' (App k (Var y))), Abs x tau' (Abs y tau'' (App k' (Var y))));
317                                                                _        -> makeFuncPair' tc gamma (k,k') (Arrow tau'' resTyp) tau' tau' ([],[]) (t11,t21)};   
318                                                   return (Abs w tauAll (PCase(apply (Var w) (fst args)) x y (App (App h (Var x)) (Var y))), Abs w tauAll (PCase (apply (Var w) (fst args)) x y (App (App h' (Var x)) (Var y))))
319                                                  }
320                                               }
321       TEither tau' tau'' -> do{i <- newInt;
322                                j <- newInt;
323                                let w = TermVar i
324                                    x = TermVar j
325                                in
326                                case snd terms of
327                                  Bottom _ -> return (Abs w tauAll (ECase (apply (Var w) (fst args)) x (fst resPair) x (fst resPair)),
328                                                      Abs w tauAll (ECase (apply (Var w) (fst args)) x (fst resPair) x (snd resPair)))
329                                  Left t2  -> case fst terms of
330                                                Left t1  -> do{(g,g') <- makeFuncPair' tc gamma resPair resTyp tau' tau' ([],[]) (t1,t2);
331                                                               return (Abs w tauAll (ECase (apply (Var w) (fst args)) x g  x (fst resPair)),
332                                                                       Abs w tauAll (ECase (apply (Var w) (fst args)) x g' x (snd resPair)))
333                                                              }
334                                                Right t1 -> return (Abs w tauAll (ECase (apply (Var w) (fst args)) x (Bottom resTyp)  x (fst resPair)),
335                                                                    Abs w tauAll (ECase (apply (Var w) (fst args)) x (Bottom resTyp)  x (snd resPair)))
336                                  Right t2  -> case fst terms of
337                                                 Right t1   -> do{(g,g') <- makeFuncPair' tc gamma resPair resTyp tau'' tau'' ([],[]) (t1,t2);
338                                                                  return (Abs w tauAll (ECase (apply (Var w) (fst args)) x (fst resPair) x g),
339                                                                          Abs w tauAll (ECase (apply (Var w) (fst args)) x (snd resPair) x g'))
340                                                                 }
341                                                 Left t1    -> return (Abs w tauAll (ECase (apply (Var w) (fst args)) x (fst resPair) x (Bottom resTyp)),
342                                                                       Abs w tauAll (ECase (apply (Var w) (fst args)) x (snd resPair) x (Bottom resTyp)))
343                               }
344       Arrow tau' tau'' -> let Abs x _ t1 = fst terms
345                               t2 = case snd terms of
346                                      Abs _ _ t  -> t
347                                      Bottom _   -> Bottom tau''
348                               Just (u,u') = if Map.member x tc then Just (fst (trace "Map.!-check: lArrowArrow g-construct fst y (list case Arrow)" (tc Map.! x)),snd (trace "Map.!-check: lArrowArrow g-construct snd y (list case Arrow)" (tc Map.! x)))
349                                             else makePlusPair tau'
350                           in
351                           makeFuncPair' tc gamma resPair resTyp tauAll tau'' (u:(fst args),u':(snd args)) (t1,t2)
352
353
354 -------Regeln der ersten Phase-------------
355
356 rFix :: Cont -> Typ -> Maybe Term
357 rFix gamma tau = if unpointed (tVars gamma) tau
358                  then Just (Bottom tau)
359                  else Nothing
360
361 rAllStar :: Cont -> Typ -> Maybe (Cont, Typ, Term -> Term)
362 rAllStar gamma tau = case tau of
363                        AllStar tv tau' -> Just (updateTVarStar gamma tv, tau', \m -> TAbs tv m)
364                        _               -> Nothing
365
366 rAll :: Cont -> Typ -> Maybe (Cont, Typ, Term -> Term)
367 rAll gamma tau = case tau of
368                    All tv tau' -> Just (updateTVar gamma tv, tau', \m -> TAbs tv m)
369                    _           -> Nothing
370
371 rArrow :: Cont -> Typ -> Maybe (M (Cont, Term -> Term), Typ)
372 rArrow gamma tau = case tau of
373                    Arrow tau1 tau2 -> Just (do {i <- newInt; 
374                                                 let x = TermVar i in
375                                                 return (updateVar gamma x tau1, \m -> Abs x tau1 m)                    
376                                                }
377                                            , tau2)
378                    _               -> Nothing
379
380 rI :: Typ -> Maybe (Typ, Term -> Term)
381 rI tau = case tau of
382                List tau' -> Just (tau', \m -> Cons m (Nil tau'))
383                _         -> Nothing
384
385 lIArrow :: Cont -> Maybe (M ((Cont, Term -> Term),(TypedVar, TypedVar)))
386 lIArrow gamma = let f = findfirst typeCheckArrowListArg (vars gamma) in
387                     case f of
388                       Nothing ->      Nothing
389                       Just (v, (Arrow (List tau1) tau2)) -> 
390                            Just (do {i <- newAux; --g fuer den neuen Kontext
391                                      j <- newInt; --y fuer die Ersetzung
392                                     let g = TermVar i
393                                         y = TermVar j in                                   
394                                     return ((updateVar (removeVar gamma v) g (Arrow tau1 tau2),
395                                             \m -> subst m (Abs y tau1 (App (Var v) (Cons (Var y) (Nil tau1)))) g),
396                                             ((g,Arrow tau1 tau2), (v, Arrow (List tau1) tau2)))
397                                     })
398
399 lIArrow_tc_update :: TermCont -> TermVar -> TermVar -> TypedVar -> TypedVar -> TermCont
400 lIArrow_tc_update tc l h g f = let Arrow (List t1) t2 = snd f
401                                    Just (x,y) = if Map.member (fst g) tc 
402                                                 then Just ((fst (trace "Map.!-check: lIArrow fst g" (tc Map.! (fst g)))),(snd (trace "Map.!-check: lIArrow snd g" (tc Map.! (fst g)))))
403                                                 else trace "lIArrow not used" $ makePlusPair (snd g) 
404                                in
405                                Map.insert (fst f) (Abs l  (List t1) (Case (Var l) (Bottom t2) h (App x (Var h))),Abs l (List t1) (Case (Var l) (Bottom t2) h (App y (Var h)))) tc
406
407 lI :: Cont -> Typ -> Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))
408 lI gamma tau' = let l = findfirst typeCheckList (vars gamma) in
409                 case l of
410                   Nothing           -> Nothing
411                   Just (v,List tau) -> Just (do {i <- newInt; --h
412                                                  let h = TermVar i in
413                                                  return ((updateVar (removeVar gamma v) h tau,
414                                                           \m -> subst m (Case (Var v) (Bottom tau) h (Var h)) h),
415                                                          ((h,tau),(v,List tau)))
416                                                 })
417
418 lI_tc_update :: TermCont -> TypedVar -> TypedVar -> TermCont
419 lI_tc_update tc h l = let Just (x,y) = if Map.member (fst h) tc 
420                                        then Just ((fst (trace "Map.!-check: lI fst h" (tc Map.! (fst h)))),(snd (trace "Map.!-check: lI snd h" (tc Map.! (fst h)))))
421                                        else trace "lI not used" $ makePlusPair (snd h) 
422                       in
423                       Map.insert (fst l) (Cons x (Nil (snd h)), Cons y (Nil (snd h))) tc
424
425 lInt :: Cont -> Maybe Cont
426 lInt gamma = let l = findfirst typeCheckInt (vars gamma) in
427                case l of
428                  Nothing  -> Nothing
429                  Just var -> Just (removeVar gamma (fst var))
430
431 lFix :: Cont -> Maybe Cont
432 lFix gamma = let l = findfirstWithTVars unpointed (tVars gamma) (vars gamma) in
433                  case l of
434                    Nothing    -> Nothing
435                    Just var   -> Just (removeVar gamma (fst var))
436
437 --TODO START--
438 lPArrow :: Cont -> Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))
439 lPArrow gamma = let l = findfirst typeCheckArrowPairArg (vars gamma) in
440                     case l of
441                       Nothing  -> Nothing
442                       Just (f, (Arrow (TPair tau1 tau2) tau3)) -> 
443                            Just (do {i <- newAux; --g fuer den neuen Kontext
444                                      j <- newInt;
445                                      k <- newInt;
446                                      let g = TermVar i 
447                                          x = TermVar j
448                                          y = TermVar k in
449                                      return ((updateVar (removeVar gamma f) g (Arrow tau1 (Arrow tau2 tau3)),
450                                              \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))))
451                                     })
452
453 lPArrow_tc_update :: TermCont -> TypedVar -> TypedVar -> M (TermCont)
454 lPArrow_tc_update tc g f = do {i <- newInt;
455                                j <- newInt;
456                                k <- newInt;
457                                let p = TermVar i
458                                    x = TermVar j
459                                    y = TermVar k 
460                                    Arrow tau tau3 = snd f 
461                                    Just (z,z') = if Map.member (fst g) tc then Just (fst (trace "Map.!-check: lPArrow fst g" (tc Map.! (fst g))), snd (trace "Map.!-check: lPArrow snd g" (tc Map.! (fst g))))
462                                                  else makePlusPair $ snd g 
463                                in
464                                return (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)))) tc)
465                               }
466
467 lP :: Cont -> Maybe (M ((Cont, Term -> Term),([TypedVar],TypedVar)))
468 lP gamma = let l = findfirst typeCheckPair (vars gamma) in
469                case l of
470                  Nothing -> Nothing
471                  Just (p, TPair tau1 tau2) ->
472                       Just (do {i <- newInt;
473                                 j <- newInt;
474                                 k <- newInt;
475                                 l <- newInt;
476                                 let x = TermVar i
477                                     y = TermVar j 
478                                     u = TermVar k
479                                     v = TermVar l in
480                                 return ((updateVar (updateVar (removeVar gamma p) x tau1) y tau2,
481                                          \m -> subst (subst m (PCase (Var p) u v (Var u)) x) (PCase (Var p) u v (Var v)) y),
482                                          ([(x,tau1),(y,tau2)],(p,TPair tau1 tau2)))
483                                })
484
485 lP_tc_update :: TermCont -> [TypedVar] -> TypedVar -> TermCont
486 lP_tc_update tc varIn p = let [x,y] = varIn 
487                               Just (z,z') = if Map.member (fst x) tc then Just (fst (trace "Map.!-check: lP fst x" (tc Map.! (fst x))), snd (trace "Map.!-check: lP snd x" (tc Map.! (fst x))))
488                                             else makePlusPair $ snd x 
489                               Just (u,u') = if Map.member (fst y) tc then Just (fst (trace "Map.!-check: lP fst y" (tc Map.! (fst y))), snd (trace "Map.!-check: lP snd y" (tc Map.! (fst y))))
490                                             else makePlusPair $ snd y
491                           in
492                           Map.insert (fst p) (Pair z u, Pair z' u') tc
493
494
495 lEArrow :: Cont -> Maybe (M ((Cont, Term -> Term),([TypedVar],TypedVar)))
496 lEArrow gamma = let l = findfirst typeCheckArrowEitherArg (vars gamma) in
497                     case l of
498                       Nothing -> Nothing
499                       Just (f, (Arrow (TEither tau1 tau2) tau3)) ->
500                            Just (do {i <- newAux; --g im neuen Kontext
501                                      j <- newAux; --h im neuen Kontext
502                                      k <- newInt; --x im Term
503                                      l <- newInt; --y im Term
504                                      let g = TermVar i
505                                          h = TermVar j
506                                          x = TermVar k
507                                          y = TermVar l in
508                                      return ((updateVar (updateVar (removeVar gamma f) g (Arrow tau1 tau3)) h (Arrow tau2 tau3),
509                                              \m -> subst (subst m (Abs x tau1 (App (Var f) (Left (Var x)))) g) (Abs y tau2 (App (Var f) (Right (Var y)))) h),
510                                              ([(g,Arrow tau1 tau3),(h,Arrow tau2 tau3)],(f,(Arrow (TEither tau1 tau2) tau3))))
511                                     })
512
513 lEArrow_tc_update :: TermCont -> [TypedVar] -> TypedVar -> M (TermCont)
514 lEArrow_tc_update tc varIn f = let [g,h] = varIn in
515                                do{i <- newInt;
516                                   j <- newInt;
517                                   k <- newInt;
518                                   let e = TermVar i 
519                                       x = TermVar j
520                                       y = TermVar k 
521                                       Arrow tau tau3 = snd f 
522                                       Just (z,z') = if Map.member (fst g) tc then Just (fst (trace "Map.!-check: lEArrow fst g" (tc Map.! (fst g))), snd (trace "Map.!-check: lEArrow snd g" (tc Map.! (fst g))))
523                                                     else makePlusPair $ snd g
524                                       Just (u,u') = if Map.member (fst h) tc then Just (fst (trace "Map.!-check: lEArrow fst h" (tc Map.! (fst h))), snd (trace "Map.!-check: lEArrow snd h" (tc Map.! (fst h))))
525                                                     else makePlusPair $ snd h
526                                   in
527                                   return (Map.insert (fst f) (Abs e tau (ECase (Var e) x z y u), Abs e tau (ECase (Var e) x z' y u')) tc)
528                                  }
529
530 ------Regeln mit backtracking -----------------
531
532 lE1 :: Cont -> Typ -> Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))
533 lE1 gamma tau = case findfirst typeCheckEither (vars gamma) of
534                     Nothing -> Nothing
535                     Just (e, TEither tau1 tau2) ->
536                          Just (do {i <- newInt;
537                                    j <- newInt;
538                                    let x = TermVar i
539                                        y = TermVar j in
540                                    return ((updateVar (removeVar gamma e) x tau1,
541                                            \m -> subst m (ECase (Var e) x (Var x) y (Bottom tau1)) x),
542                                            ((x,tau1),(e, TEither tau1 tau2)))
543                                   })
544
545 lE1_tc_update :: TermCont -> TypedVar -> TypedVar -> TermCont
546 lE1_tc_update tc x e = let Just (z,z') = if Map.member (fst x) tc then Just (fst (trace "Map.!-check: lE1 fst x" (tc Map.! (fst x))), snd (trace "Map.!-check: lE1 snd x" (tc Map.! (fst x))))
547                                          else makePlusPair $ snd x
548                        in
549                        Map.insert (fst e) (Left z, Left z') tc
550
551 lE2 :: Cont -> Typ -> Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))
552 lE2 gamma tau = case findfirst typeCheckEither (vars gamma) of
553                     Nothing -> Nothing
554                     Just (e, TEither tau1 tau2) ->
555                          Just (do {i <- newInt;
556                                    j <- newInt;
557                                    let x = TermVar i
558                                        y = TermVar j in
559                                    return ((updateVar (removeVar gamma e) y tau2,
560                                            \m -> subst m (ECase (Var e) x (Bottom tau2) y (Var y)) y),
561                                            ((y,tau2),(e,TEither tau1 tau2)))
562                                   })
563 lE2_tc_update :: TermCont -> TypedVar -> TypedVar -> TermCont
564 lE2_tc_update tc y e = let Just (z,z') = if Map.member (fst y) tc then Just (fst (trace "Map.!-check: lE2 fst y" (tc Map.! (fst y))), snd (trace "Map.!-check: lE2 snd y" (tc Map.! (fst y))))
565                                          else makePlusPair $ snd y
566                        in
567                        Map.insert (fst e) (Right z, Right z') tc
568
569 rP1 :: Typ -> Maybe (Typ, Term -> Term)
570 rP1 tau = case tau of
571             TPair tau1 tau2 -> Just (tau1, \m -> Pair m (Bottom tau2))
572             _               -> Nothing
573
574 rP2 :: Typ -> Maybe (Typ, Term -> Term)
575 rP2 tau = case tau of
576             TPair tau1 tau2 -> Just (tau2,\m -> Pair (Bottom tau1) m)
577             _               -> Nothing
578
579 rE1 :: Typ -> Maybe (Typ, Term -> Term)
580 rE1 tau = case tau of
581             TEither tau1 _ -> Just(tau1, \m -> Left m)
582             _              -> Nothing
583
584 rE2 :: Typ -> Maybe (Typ, Term -> Term)
585 rE2 tau = case tau of
586             TEither _ tau2 -> Just(tau2, \m -> Right m)
587             _              -> Nothing
588 ---TODO END---
589
590 lFixArrowStar :: Cont -> [M ((Cont, Term -> Term),(TypedVar,TypedVar))]
591 lFixArrowStar gamma = let l = findallWithTVars typeCheckArrowUnPointedArgPointedRes (tVars gamma) (vars gamma) in
592                           map makeone l
593                           where makeone = \var -> let Arrow tau1 tau2 = snd var in
594                                                        do {i <- newAux;
595                                                             let x = TermVar i in
596                                                             return (((updateVarStar (removeVar gamma (fst var)) x tau2)
597                                                                      , \m -> subst m (App (Var (fst var)) (Bottom tau1)) x),((x,tau2),var))
598                                                           }
599 lFixArrowStar_tc_update :: TermCont -> Cont -> TermVar -> TypedVar -> TypedVar -> M TermCont
600 lFixArrowStar_tc_update tc gamma x y f = let Arrow t1 t2 = snd f 
601                                              (u,u') = if Map.member (fst y) tc 
602                                                       then trace "LFIXARROWSTAR: y in Map" (tc Map.! (fst y)) 
603                                                       else trace "LFIXARROWSTAR: y NOT in Map"
604                                                            (case makePlusPair (snd y) of 
605                                                             Just p -> p)             in
606                                          do{(g,g') <- makeFuncPair tc gamma (u,u') t2 t1 (Bottom t1, Bottom t1);
607                                             return (Map.insert (fst f) (g,g') tc)
608                                            }
609
610 --lFixArrowStar_typeAnalyse :: Typ -> ([TermPlus],[TermPlus]) -> (([TermPlus],[TermPlus]),Typ)
611 --lFixArrowStar_typeAnalyse tau args = case tau of
612 --                                   TVar t      -> (args,tau)
613 --                                   Arrow t1 t2 -> case makePlusPair t1 of
614 --                                                    Just (x,y) -> lFixArrowStar_typeAnalyse t2 (x:(fst args), y:(snd args))
615
616 --lArrowArrow in der Variante ohne g.
617 lArrowArrow :: Cont -> [M (((Cont, Typ), Cont, Term -> Term -> Term), ([TypedVar],TypedVar))]
618 lArrowArrow gamma = 
619     let l = findall typeCheckArrowArgArrow (vars gamma) in
620     map makeone l
621     where makeone var = let Arrow (Arrow tau1 tau2) tau3 = snd var in
622                         do {i <- newInt;
623                             j <- newInt;
624                             let x = TermVar i 
625                                 y = TermVar j in
626                             return ((((updateVar (removeVar gamma (fst var)) x tau1),
627                                      tau2),
628                                      updateVarStar (removeVar gamma (fst var)) y tau3,
629                                      \m1 -> \m2 -> subst m2 (App (Var (fst var)) (Abs x tau1 m1)) y),
630                                     ([(x,tau1),(y,tau3)],var))
631                            }
632 ------------------------ TermContext         M_1     w           y           f           TermContext -----
633 lArrowArrow_tc_update :: TermCont -> Cont -> Term -> TypedVar -> TypedVar -> TypedVar -> M TermCont
634 lArrowArrow_tc_update tc gamma m1 w y f = 
635     let Arrow t12 t3 = snd f 
636         Arrow t1  t2 = t12
637         Just resPair = if Map.member (fst y) tc then Just (fst (trace "Map.!-check: lArrowArrow g-construct fst y (else)" (tc Map.! (fst y))), snd (trace "Map.!-check: lArrowArrow g-construct snd y" (tc Map.! (fst y))))
638                        else trace "lArrowArrow not used" $ makePlusPair (snd y)
639     in
640     do {i <- newInt;
641         (g,g') <- makeFuncPair tc gamma resPair t3 t2 (term2PlusTerm(m1),term2PlusTerm(m1));
642         let u = TermVar i 
643             Just (z,z') = if Map.member (fst w) tc then Just (fst (trace "Map.!-check: lArrowArrow fst w" (tc Map.! (fst w))), snd (trace "Map.!-check: lArrowArrow snd w" (tc Map.! (fst w))))
644                           else makePlusPair $ snd w
645         in
646         return (Map.insert (fst f) (Abs u t12 (App g (App (Var u) z)), Abs u t12 (App g' (App (Var u) z'))) tc)
647        }
648
649 lFixArrow :: Cont -> [M ((Cont, Term -> Term),(TypedVar,TypedVar))]
650 lFixArrow gamma = 
651     let l = findall typeCheckArrow (vars gamma) in
652     map makeone l
653     where makeone var = let Arrow tau1 tau2 = snd var in
654                         do {i <- newAux;
655                             let x = TermVar i in
656                             return ((updateVar (removeVar gamma (fst var)) x tau2,
657                                     \m -> subst m (App (Var (fst var)) (Bottom tau1)) x),
658                                     ((x,tau2),var))
659                            }
660
661 lFixArrow_tc_update :: TermCont -> TermVar -> TypedVar -> TypedVar -> TermCont
662 lFixArrow_tc_update tc z x f = let Arrow t1 t2 = snd f 
663                                    Just (u,u') = if Map.member (fst x) tc then Just (fst (trace "Map.!-check: lFixArrow fst x" (tc Map.! (fst x))), snd (trace "Map.!-check: lFixArrow snd x" (tc Map.! (fst x))))
664                                                  else makePlusPair (snd x) 
665                                in 
666                                Map.insert (fst f) (Abs z t1 u, Abs z t1 u') tc
667
668 ------Ende Regeln der ersten Phase-------------
669
670 ------Regeln fuer die zweite Phase-------------
671 aXStar :: Cont -> Typ -> Maybe (Term, (TermVar,Typ))
672 aXStar gamma tau = case findfirstSpecialType (varsStar gamma) tau of
673                             Nothing -> Nothing
674                             Just x  -> Just (Var (fst x), x)
675
676 aXStar_tc_update :: TermCont -> (TermVar,Typ) -> Maybe TermCont
677 aXStar_tc_update tc var = case makePlusPair (snd var) of
678                             Nothing -> Nothing
679                             Just p  -> Just (Map.insert (fst var) p tc)
680
681 laArrowStar1 :: Cont -> Maybe (M ((Cont, Term -> Term),((TermVar,Typ),(TermVar,Typ))))
682 laArrowStar1 gamma = case findfirst typeCheckArrow (varsStar gamma) of
683                        Nothing                    -> Nothing
684                        Just (f, Arrow tau1 tau2)  -> Just (do {i <- newAux;
685                                                                let y = TermVar i in
686                                                                return ((updateVarStar (removeVarStar gamma f) y tau2, \m -> subst m (App (Var f) (Bottom tau1)) y),((y, tau2),(f, Arrow tau1 tau2) ));
687                                                              })
688 laArrowStar1_tc_update :: TermCont -> TermVar -> (TermVar,Typ) -> (TermVar,Typ) -> TermCont
689 laArrowStar1_tc_update tc x varIn varOut = case (snd varOut) of
690                                            Arrow tau1 _ ->
691                                              let Just (z,z') = if Map.member (fst varIn) tc then Just (fst (trace "Map.!-check: laArrowStar1 fst varIn" (tc Map.!(fst varIn))), snd (trace "Map.!-check: laArrowStar snd varIn" (tc Map.! (fst varIn))))
692                                                                else makePlusPair $ snd varIn
693                                              in
694                                              Map.insert (fst varOut) (Abs x tau1 z, Abs x tau1 z') tc
695
696 laArrowStar2 :: Cont -> Maybe (M ((Cont, Term -> Term),([TypedVar],TypedVar)))
697 laArrowStar2 gamma = checkall (findall typeCheckArrow (vars gamma)) 
698                      where checkall xs =
699                                case xs of
700                                  []  -> Nothing
701                                  ((f, Arrow tau1 tau2):ys) -> if unpointed (tVars gamma) tau2 
702                                                               then checkall ys
703                                                               else case findfirstSpecialType (varsStar gamma) tau1 of
704                                                                      Nothing     -> checkall ys
705                                                                      Just (x,_)  -> Just (do {i <- newAux;
706                                                                                               let y = TermVar i in
707                                                                                               return ((updateVarStar (removeVar gamma f) y tau2, \m -> subst m (App (Var f) (Var x)) y),([(x,tau1),(y,tau2)],(f,Arrow tau1 tau2)))
708                                                                                         })
709 -----------------------------------                      x*          y*          f           -------- 
710 laArrowStar2_tc_update :: TermCont -> Cont -> TermVar -> TypedVar -> TypedVar -> TypedVar -> M TermCont
711 laArrowStar2_tc_update tc gamma z x y f = let Just (u,u') = if (Map.member (fst x) tc) then Just (fst (trace "Map.!-check: laArrowStar2 fst x (TVar)" (tc Map.! (fst x))), snd (trace "Map.!-check: laArrowStar2 snd x (TVar)" (tc Map.! (fst x))))
712                                                             else makePlusPair (snd x) 
713                                               Just (v,v') = if (Map.member (fst y) tc) then Just (fst (trace "Map.!-check: laArrowStar2 fst y (TVar)" (tc Map.! (fst y))), snd (trace "Map.!-check: laArrowStar2 snd y (TVar)" (tc Map.! (fst y))))
714                                                             else makePlusPair (snd y)
715                                           in
716                                           do{fPair <- (makeFuncPair tc gamma (v,v') (snd y) (snd x) (u,Bottom (snd x)));
717                                              return (Map.insert (fst f) fPair tc)
718                                             }
719
720 laArrowStar2_typeAnalyse :: Typ -> ([TermPlus],[TermPlus]) -> (([TermPlus],[TermPlus]),Typ)
721 laArrowStar2_typeAnalyse tau args = case tau of
722                                     TVar t      -> (args, tau)
723                                     Arrow t1 t2 -> case makePlusPair t1 of
724                                                    Just (x,y) -> laArrowStar2_typeAnalyse t2 (x:(fst args), y:(snd args))
725                                     List t      -> (args, tau)
726
727 lIStar :: Cont -> Typ ->  Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))
728 lIStar gamma tau = case findfirst typeCheckList (varsStar gamma) of
729                      Nothing           -> Nothing
730                      Just (l,List tau') -> Just (do {i <- newInt;
731                                                     let h = TermVar i in
732                                                     return ((updateVarStar (removeVarStar gamma l) h tau',
733                                                              \m -> subst m (Case (Var l) (Bottom tau') h (Var h)) h),
734                                                             ((h, tau'),(l,List tau')))
735                                                     })
736
737 lIStar_tc_update tc h l = let Just (u,u') = if Map.member (fst h) tc then Just (fst (trace "Map.!-check: lIStar fst h" (tc Map.!(fst h))), snd (trace "Map.!-check: lIStar snd h" (tc Map.!(fst h))))
738                                             else makePlusPair $ snd h
739                           in
740                           Map.insert (fst l) (Cons u (Nil (snd h)), Cons u' (Nil (snd h))) tc
741
742 lPStar :: Cont -> Maybe (M ((Cont, Term -> Term),([TypedVar],TypedVar)))
743 lPStar gamma = let l = findfirst typeCheckPair (varsStar gamma) in
744                     case l of
745                       Nothing -> Nothing
746                       Just (p, TPair tau1 tau2) ->
747                            Just (do {i <- newInt;
748                                      j <- newInt;
749                                      k <- newInt;
750                                      l <- newInt;
751                                      let x = TermVar i
752                                          y = TermVar j
753                                          u = TermVar k
754                                          v = TermVar l in
755                                      return ((updateVarStar (updateVarStar (removeVarStar gamma p) x tau1) y tau2,
756                                              \m -> subst (subst m (PCase (Var p) u v (Var u)) x) (PCase (Var p) u v (Var v)) y),
757                                              ([(x,tau1),(y,tau2)],(p,TPair tau1 tau2)))
758                                     })
759
760 lPStar_tc_update :: TermCont -> [TypedVar] -> TypedVar -> TermCont
761 lPStar_tc_update tc varIn p = let [x,y] = varIn 
762                                   Just (z,z') = if Map.member (fst x) tc then Just (fst (trace "Map.!-check: lPStar fst x" (tc Map.! (fst x))), snd (trace "Map.!-check: lPStar snd x" (tc Map.! (fst x))))
763                                                 else makePlusPair $ snd x
764                                   Just (u,u') = if Map.member (fst y) tc then Just (fst (trace "Map.!-check: lPStar fst y" (tc Map.! (fst y))), snd (trace "Map.!-check: lPStar snd y" (tc Map.! (fst y))))
765                                                 else makePlusPair $ snd y
766                               in
767                               Map.insert (fst p) (Pair z u, Pair z' u') tc
768
769 lEStar1 :: Cont -> Typ -> Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))
770 lEStar1 gamma tau = case findfirst typeCheckEither (varsStar gamma) of
771                     Nothing -> Nothing
772                     Just (e, TEither tau1 tau2) ->
773                          Just (do {i <- newInt;
774                                    j <- newInt;
775                                    let x = TermVar i
776                                        y = TermVar j in
777                                    return ((updateVarStar (removeVarStar gamma e) x tau1,
778                                            \m -> subst m (ECase (Var e) x (Var x) y (Bottom tau1)) x),
779                                            ((x,tau1),(e,TEither tau1 tau2)))
780                                   })
781
782 lEStar1_tc_update :: TermCont -> TypedVar -> TypedVar -> TermCont
783 lEStar1_tc_update tc x e = let Just (z,z') = if Map.member (fst x) tc then Just (fst (trace "Map.!-check: lEStar1 fst x" (tc Map.! (fst x))), snd (trace "Map.!-check: lEStar1 snd x" (tc Map.! (fst x))))
784                                              else makePlusPair $ snd x
785                            in
786                            Map.insert (fst e) (Left z, Left z') tc
787
788 lEStar2 :: Cont -> Typ -> Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))
789 lEStar2 gamma tau = case findfirst typeCheckEither (varsStar gamma) of
790                     Nothing -> Nothing
791                     Just (e, TEither tau1 tau2) ->
792                          Just (do {i <- newInt;
793                                    j <- newInt;
794                                    let x = TermVar i
795                                        y = TermVar j in
796                                    return ((updateVarStar (removeVarStar gamma e) y tau2,
797                                            \m -> subst m (ECase (Var e) x (Bottom tau1) y (Var y)) y),
798                                            ((y,tau2),(e,TEither tau1 tau2)))
799                                   })
800
801 lEStar2_tc_update :: TermCont -> TypedVar -> TypedVar -> TermCont
802 lEStar2_tc_update tc y e = let Just (z,z') = if Map.member (fst y) tc then Just (fst (trace "Map.!-check: lEStar2 fst y" (tc Map.! (fst y))), snd (trace "Map.!-check: lEStar2 snd y" (tc Map.! (fst y))))
803                                              else makePlusPair $ snd y
804                            in
805                            Map.insert (fst e) (Right z, Right z') tc
806
807 ------------------- Der Algorithmus -------------------------
808
809 --Bemerkung: Pointed-Checks werden durch die Regelreihenfolge so weit als moeglich vermieden. ((LFix) und (RFix) stehen weit oben)
810
811 alg :: Cont -> Typ -> TermCont -> M (Term,TermCont)
812 alg gamma tau termCont = do track (makeTrackString "Start Conf" gamma tau)
813                             alg1 gamma tau termCont
814
815 alg1 :: Cont -> Typ -> TermCont -> M (Term,TermCont)
816 alg1 = alg1_RFix
817
818 alg1_RFix :: Cont -> Typ -> TermCont -> M (Term,TermCont)
819 alg1_RFix gamma tau termCont = case rFix gamma tau of
820                                Nothing -> alg1_RAllStar gamma tau termCont
821                                Just t  -> do track ((makeTrackString "RFix" gamma tau) ++ "  !!END OF BRANCH!!")
822                                              return (t,termCont)
823                                       
824 alg1_RAllStar :: Cont -> Typ -> TermCont -> M (Term,TermCont)
825 alg1_RAllStar gamma tau termCont = case rAllStar gamma tau of
826                                    Nothing                -> alg1_RAll gamma tau termCont
827                                    Just (gamma', tau', f) -> do track (makeTrackString "RAllStar" gamma' tau')
828                                                                 (t,c) <- (alg1 gamma' tau' termCont)
829                                                                 return (f t, c)
830                                                               
831 alg1_RAll :: Cont -> Typ -> TermCont -> M (Term,TermCont)
832 alg1_RAll gamma tau termCont = case rAll gamma tau of
833                                Nothing                -> alg1_LFix gamma tau termCont
834                                Just (gamma', tau', f) -> do track (makeTrackString "RAll" gamma' tau')
835                                                             (t,c) <- (alg1 gamma' tau' termCont)
836                                                             return (f t,c)
837                 
838 alg1_LFix :: Cont -> Typ -> TermCont -> M (Term,TermCont)                                    
839 alg1_LFix gamma tau termCont = case lFix gamma of
840                                Nothing     -> alg1_LInt gamma tau termCont
841                                Just gamma' -> do track (makeTrackString "LFix" gamma' tau)
842                                                  alg1 gamma' tau termCont
843
844 alg1_LInt gamma tau termCont = case lInt gamma of
845                                Nothing     -> alg1_RArrow gamma tau termCont
846                                Just gamma' -> do track (makeTrackString "LInt" gamma' tau)
847                                                  alg1 gamma' tau termCont
848
849 alg1_RArrow :: Cont -> Typ -> TermCont -> M (Term,TermCont)
850 alg1_RArrow gamma tau termCont = case rArrow gamma tau of 
851                                  Nothing           -> alg1_RI gamma tau termCont
852                                  Just (comp, tau') -> do {(gamma', f) <- comp;
853                                                           track (makeTrackString "R->" gamma' tau');
854                                                           (t,c) <- (alg1 gamma' tau' termCont);
855                                                           return (f t,c)
856                                                          }
857
858 alg1_RI :: Cont -> Typ -> TermCont -> M (Term,TermCont)
859 alg1_RI gamma tau termCont = case rI tau of
860                              Nothing        -> alg1_LIArrow gamma tau termCont
861                              Just (tau', f) -> do track (makeTrackString "RI" gamma tau')
862                                                   (t,c) <- (alg1 gamma tau' termCont)
863                                                   return (f t,c)
864                                            
865 alg1_LIArrow :: Cont -> Typ -> TermCont -> M (Term,TermCont)
866 alg1_LIArrow gamma tau termCont = case lIArrow gamma of
867                                   Nothing   -> alg1_LI gamma tau termCont
868                                   Just comp -> do {((gamma',f),(g,k)) <- comp;
869                                                    track (makeTrackString "LI->" gamma' tau);
870                                                    (t,c) <- (alg1 gamma' tau termCont);
871                                                    i <- newInt;
872                                                    j <- newInt;
873                                                    let l = TermVar i
874                                                        h = TermVar j in
875                                                    return (f t,lIArrow_tc_update c l h g k)
876                                                   }
877
878 alg1_LI :: Cont -> Typ -> TermCont -> M (Term,TermCont)
879 alg1_LI gamma tau termCont = case lI gamma tau of
880                              Nothing     -> alg1_LPArrow gamma tau termCont
881                              Just comp -> do {((gamma',f),(h,l)) <- comp;
882                                               track (makeTrackString "LI" gamma' tau);
883                                               (t,c) <- (alg1 gamma' tau termCont);
884                                               return (f t, lI_tc_update c h l)
885                                              }
886
887 alg1_LPArrow gamma tau termCont = case lPArrow gamma of
888                                   Nothing    -> alg1_LP gamma tau termCont
889                                   Just comp  -> do {((gamma',f),(g,h)) <- comp;
890                                                     track(makeTrackString "LP->" gamma' tau);
891                                                     (t,c) <- (alg1 gamma' tau termCont);
892                                                     termCont' <- lPArrow_tc_update c g h;
893                                                     return (f t, termCont')
894                                                    }
895
896 alg1_LP gamma tau termCont = case lP gamma of
897                              Nothing    -> alg1_LEArrow gamma tau termCont
898                              Just comp  -> do {((gamma',f),(varIn,p)) <- comp;
899                                                track(makeTrackString "LP" gamma' tau);
900                                                (t,c) <- (alg1 gamma' tau termCont);
901                                                return (f t, lP_tc_update c varIn p)
902                                               }
903
904 alg1_LEArrow gamma tau termCont = case lEArrow gamma of
905                                   Nothing   -> alg1_LE1 gamma tau termCont
906                                   Just comp -> do {((gamma',f),(varIn,g)) <- comp;
907                                                    track (makeTrackString "LE->" gamma' tau);
908                                                    (t,c) <- (alg1 gamma' tau termCont);
909                                                    termCont' <- lEArrow_tc_update c varIn g;
910                                                    return (f t, termCont')
911                                                   }
912
913 alg1_LE1 gamma tau termCont = case lE1 gamma tau of
914                               Nothing   -> alg1_RP1 gamma tau termCont
915                               Just comp -> do {((gamma',f),(x,e)) <- comp;
916                                            let subderivation =
917                                                    do  track (makeTrackString "LE1" gamma' tau)
918                                                        (t,c) <- (alg1 gamma' tau termCont);
919                                                        return (f t, lE1_tc_update c x e)
920                                            in
921                                            choice subderivation (alg1_LE2 gamma tau termCont);
922                                           }
923
924 alg1_LE2 gamma tau termCont = case lE2 gamma tau of
925                               Nothing   -> alg1_RP1 gamma tau termCont --should never be reached
926                               Just comp -> do {((gamma',f),(y,e)) <- comp;
927                                                track (makeTrackString "LE2" gamma' tau);
928                                                (t,c) <- (alg1 gamma' tau termCont);
929                                                return (f t, lE2_tc_update c y e)
930                                               }
931
932 alg1_RP1 gamma tau termCont = case rP1 tau of
933                               Nothing        -> alg1_RE1 gamma tau termCont
934                               Just (tau', f) -> choice subderivation (alg1_RP2 gamma tau termCont)
935                                                  where subderivation = do {track (makeTrackString "RP1" gamma tau');
936                                                                            (t,c) <- (alg1 gamma tau' termCont);
937                                                                            return (f t, c)
938                                                                           }
939   
940 alg1_RP2 gamma tau termCont = case rP2 tau of
941                               Nothing        -> alg1_RE1 gamma tau termCont
942                               Just (tau', f) -> do {track (makeTrackString "RP2" gamma tau');
943                                                     (t,c) <- (alg1 gamma tau' termCont);
944                                                     return (f t,c)
945                                                    }
946
947 alg1_RE1 gamma tau termCont = case rE1 tau of
948                               Nothing        -> alg1_LFixArrowStar gamma tau termCont
949                               Just (tau', f) -> choice subderivation (alg1_RE2 gamma tau termCont)
950                                                 where subderivation = do {track (makeTrackString "RE1" gamma tau');
951                                                                           (t,c) <- (alg1 gamma tau' termCont);
952                                                                           return (f t,c)
953                                                                          }
954                                                                           
955 alg1_RE2 gamma tau termCont = case rE2 tau of
956                               Nothing        -> alg1_LFixArrowStar gamma tau termCont
957                               Just (tau', f) -> do {track (makeTrackString "RE2" gamma tau');
958                                                     (t,c) <- (alg1 gamma tau' termCont);
959                                                     return (f t,c)
960                                                    }
961                                         
962 alg1_LFixArrowStar :: Cont -> Typ -> TermCont -> M (Term, TermCont)
963 alg1_LFixArrowStar gamma tau termCont = foldr choice (alg1_LArrowArrow gamma tau termCont) (map trysubderivations (lFixArrowStar gamma))
964                                       where trysubderivations = \l -> do {((gamma', f),(y,g)) <- l; 
965                                                                           track (makeTrackString "LFix->*" gamma' tau);
966                                                                           (t,c) <- (alg2 gamma' tau termCont);
967                                                                           i <- newInt;
968                                                                           let x = TermVar i in
969                                                                           do{tc <- lFixArrowStar_tc_update c gamma x y g;
970                                                                           return (f t, tc)}
971                                                                          }
972
973 alg1_LArrowArrow :: Cont -> Typ -> TermCont -> M (Term,TermCont)
974 alg1_LArrowArrow gamma tau termCont = 
975      foldr choice (alg1_LFixArrow gamma tau termCont) (map trysubderivations (lArrowArrow gamma))
976      where trysubderivations = \l -> do {(((gamma1, tau1), gamma2, f),([w,y],g)) <- l;
977                                          track (makeTrackString "L->-> (fst)" gamma1 tau1);
978                                          track (makeTrackString "L->-> (snd)" gamma2 tau);
979                                          (t1,c1) <- (alg1 gamma1 tau1 termCont);
980                                          (t2,c2) <- (alg2 gamma2 tau termCont);
981                                          termCont' <- lArrowArrow_tc_update (Map.union c1 c2) gamma t1 w y g;
982                                          return (f t1 t2, termCont')
983                                         }
984
985 alg1_LFixArrow :: Cont -> Typ -> TermCont -> M (Term,TermCont)
986 alg1_LFixArrow gamma tau termCont = 
987      foldr choice (do {track "LFix->:  !!FAIL!!"; abort}) (map trysubderivations (lFixArrow gamma))
988      where trysubderivations = \l -> do {((gamma', f),(x,g)) <- l;
989                                          track (makeTrackString "LFix->" gamma' tau);
990                                          (t,c) <- (alg1 gamma' tau termCont);
991                                          i <- newInt;
992                                          let z = TermVar i in
993                                          return (f t,lFixArrow_tc_update c z x g)
994                                         }
995 --alg1_End gamma tau = return (GoalTerm gamma tau)
996
997 alg2 :: Cont -> Typ -> TermCont -> M (Term,TermCont)
998 alg2 = alg2_AXStar
999
1000 alg2_AXStar :: Cont -> Typ -> TermCont -> M (Term,TermCont)
1001 alg2_AXStar gamma tau termCont = case aXStar gamma tau of
1002                                  Nothing     -> alg2_LaArrowStar1 gamma tau termCont
1003                                  Just (t,v)  -> do track ((makeTrackString "AX*" gamma tau) ++ "  !!END OF BRANCH!!")
1004                                                    case aXStar_tc_update termCont v of
1005                                                      Nothing -> abort
1006                                                      Just tc -> return (t, tc)
1007
1008 alg2_LaArrowStar1 :: Cont -> Typ -> TermCont -> M (Term,TermCont)
1009 alg2_LaArrowStar1 gamma tau termCont = case laArrowStar1 gamma of
1010                                        Nothing -> alg2_LaArrowStar2 gamma tau termCont
1011                                        Just (comp) 
1012                                                -> do {((gamma', f),(varIn,varOut)) <- comp;
1013                                                       track (makeTrackString "La->*1" gamma' tau);
1014                                                       (t,c) <- (alg2 gamma' tau termCont);
1015                                                       i <- newInt;
1016                                                       let x = TermVar i in
1017                                                       return (f t, laArrowStar1_tc_update c x varIn varOut)
1018                                                      }
1019
1020 alg2_LaArrowStar2 :: Cont -> Typ -> TermCont -> M (Term,TermCont)
1021 alg2_LaArrowStar2 gamma tau termCont = case laArrowStar2 gamma of
1022                                        Nothing   -> alg2_LIStar gamma tau termCont
1023                                        Just comp -> do {((gamma', f),([x,y],g)) <- comp;
1024                                                         track (makeTrackString "La->*2" gamma' tau);
1025                                                         (t,c) <- (alg2 gamma' tau termCont);
1026                                                         i <- newInt;
1027                                                         let u = TermVar i in
1028                                                         do{tc <- laArrowStar2_tc_update c gamma u x y g;
1029                                                            return (f t, tc)
1030                                                           }
1031                                                        }
1032
1033 alg2_LIStar :: Cont -> Typ -> TermCont -> M (Term,TermCont)
1034 alg2_LIStar gamma tau termCont = case lIStar gamma tau of
1035                                  Nothing   -> alg2_LPStar gamma tau termCont
1036                                  Just comp -> do {((gamma', f),(h,l)) <- comp;
1037                                                   track (makeTrackString "LI*" gamma' tau);
1038                                                   (t,c) <- (alg2 gamma' tau termCont);
1039                                                   return (f t, lIStar_tc_update c h l)
1040                                                  }
1041
1042 alg2_LPStar gamma tau termCont = case lPStar gamma of
1043                                   Nothing   -> alg2_LEStar1 gamma tau termCont
1044                                   Just comp -> do {((gamma', f),(h,p)) <- comp;
1045                                                    track (makeTrackString "LP*" gamma' tau);
1046                                                    (t,c) <- (alg2 gamma' tau termCont);
1047                                                    return (f t, lPStar_tc_update c h p)
1048                                                   }
1049
1050 alg2_LEStar1 gamma tau termCont = case lEStar1 gamma tau of
1051                                  Nothing   -> do {track "LE*1: FAIL";
1052                                                   abort
1053                                                  }
1054                                  Just comp -> do {((gamma',f),(x,e)) <- comp;
1055                                                   let subderivation =
1056                                                          do {track (makeTrackString "LE*1" gamma' tau);
1057                                                              (t,c) <- (alg2 gamma' tau termCont);
1058                                                              return (f t, lEStar1_tc_update c x e)
1059                                                             }
1060                                                   in
1061                                                   choice subderivation (alg2_LEStar2 gamma tau termCont)
1062                                                  }
1063
1064 alg2_LEStar2 gamma tau termCont = case lEStar2 gamma tau of
1065                                   Nothing   -> do {track "LE*2: FAIL";
1066                                                    abort
1067                                                   }
1068                                   Just comp -> do {((gamma',f),(y,e)) <- comp;
1069                                                    track (makeTrackString "LE*2" gamma' tau);
1070                                                    (t,c) <- (alg2 gamma' tau termCont);
1071                                                    return (f t, lEStar2_tc_update c y e)
1072                                                   }
1073
1074 --------END Algorithm ---------
1075
1076 makeTrackString :: String -> Cont -> Typ -> String
1077 makeTrackString = trackRules 
1078
1079 trackAll rule gamma tau = rule ++ ": " ++ showCont gamma ++ ", Type = " ++ showTyp tau
1080 trackRules rule gamma tau = rule
1081
1082 getTerm tau = do printTyp tau
1083                  putStr "\n"
1084                  case runM $ alg emptyCont tau emptyTermCont of
1085                    Nothing             -> putStr "No Term."
1086                    Just (result,debug) -> do putStr ("    " ++ (foldr (\x -> \y -> x ++ "\n    " ++ y) "\n" debug))
1087                                              printResult (fst result)
1088
1089 getComplete tau = do {printTyp tau;
1090                       putStr "\n";
1091                       case runM $ alg emptyCont tau emptyTermCont of
1092                       Nothing             -> putStr "No Term."
1093                       Just (result,debug) -> do {putStr ("    " ++ (foldr (\x -> \y -> x ++ "\n    " ++ y) "\n" debug));
1094                                                  printResult (fst result);
1095                                                  printUsedTermCont result;
1096                                                 }
1097                      }
1098
1099 getCompleteRaw :: Typ -> E.Either String (Term,TermCont)
1100 getCompleteRaw tau = case runM $ alg emptyCont tau emptyTermCont of
1101                       Nothing             -> E.Left "No Term."
1102                       Just (result,debug) -> E.Right (result)
1103
1104
1105 getWithDebug tau = do {printTyp tau;
1106                       putStr "\n";
1107                       case runM $ alg emptyCont tau emptyTermCont of
1108                       Nothing             -> putStr "No Term."
1109                       Just (result,debug) -> do {putStr ("    " ++ (foldr (\x -> \y -> x ++ "\n    " ++ y) "\n" debug));
1110                                                  printResult (fst result);
1111                                                  printTermCont (snd result);
1112                                                  printUsedTermCont result;                                               
1113                                                 }
1114                      }
1115
1116 printUsedTermCont :: (Term, TermCont) -> IO()
1117 printUsedTermCont p =
1118     let (t,tc) = p in
1119     do {putStr "Wahl der abstrahierten Variablen:\n\n";
1120         putStr (showUsedTermCont t tc)
1121        }
1122
1123 showUsedTermCont :: Term -> TermCont -> String
1124 showUsedTermCont t tc =
1125         case t of
1126         TAbs _ t'    -> showUsedTermCont t' tc
1127         Abs v tau t' -> case Map.findWithDefault (Bottom tau,Bottom tau) v tc of
1128                         (Bottom _, Bottom _) -> case makePlusPair tau of
1129                                                 Nothing     -> "ERROR."
1130                                                 Just (x,x') ->    (showTerm (Var v)) ++ "  = " ++ (showTermPlus False x) ++ "\n"
1131                                                                ++ (showTerm (Var v)) ++ "' = " ++ (showTermPlus True x')  ++ "\n\n"
1132                                                                ++ (showUsedTermCont t' tc)
1133                         (x,x')               ->    (showTerm (Var v)) ++ "  = " ++ (showTermPlus False x)  ++ "\n"
1134                                                 ++ (showTerm (Var v)) ++ "' = " ++ (showTermPlus True x')   ++ "\n\n" 
1135                                                 ++ (showUsedTermCont t' tc)
1136 --      Abs v tau t' -> if Map.member v tc 
1137 --                      then case makePlusPair tau of
1138 --                            Nothing     -> "ERROR."
1139 --                             Just (x,x') ->    (showTerm (Var v)) ++ "  = " ++ (showTermPlus False x) ++ "\n"
1140 --                                           ++ (showTerm (Var v)) ++ "' = " ++ (showTermPlus True x')  ++ "\n\n"
1141 --                                            ++ (showUsedTermCont t' tc)
1142 --                      else let (x,x') = (tc Map.! v) in
1143 --                                (showTerm (Var v)) ++ "  = " ++ (showTermPlus False x)  ++ "\n"
1144 --                            ++ (showTerm (Var v)) ++ "' = " ++ (showTermPlus True x')   ++ "\n\n" 
1145 --                             ++ (showUsedTermCont t' tc)
1146
1147         _            -> "Nothing else is required.\n\n"
1148
1149 printTermCont :: TermCont -> IO() 
1150 printTermCont tc = putStr ("Anahl der Eintraege: " ++ (show (Map.size tc)) ++ "\n\n" ++ (showTermContList (Map.toList tc)))
1151
1152 showTermContList :: [(TermVar,(TermPlus,TermPlus))] -> String
1153 showTermContList l = case l of
1154                      []             -> "Nothing left.\n"
1155                      (v,(x,x')):xs  ->   (showTerm (Var v)) ++ "  = " ++ (showTermPlus False x) ++ "\n"
1156                                        ++ (showTerm (Var v)) ++ "' = " ++ (showTermPlus True x')  ++ "\n\n"
1157                                        ++ (showTermContList xs)
1158
1159 --testWithAll tau = do printTyp tau
1160 --                   case runMAll $ alg1 emptyCont tau of
1161 --                     Nothing             -> putStr "No Term."
1162 --                     Just (result,debug) -> do putStr (foldr (\x -> \y -> x ++ "\n" ++ y) "" debug)
1163 --                                               putStr (showTerm result)
1164
1165
1166
1167
1168 printResult ::  Term -> IO ()
1169 printResult t = putStr ("Ausgabe-Term: " ++ (showTerm t) ++ "\n\n")
1170
1171 printTyp :: Typ -> IO ()
1172 printTyp t = putStr ("Eingabe-Typ:  " ++ showTyp t ++ "\n")
1173
1174 showCont :: Cont -> String
1175 showCont gamma = let showVars = 
1176                          let vs = vars gamma in 
1177                          case vs of
1178                           [] -> "]"
1179                           _  -> foldr (\x -> \y -> x ++ "," ++ y) "\b]" (map (\v -> showTerm (Var (fst v)) ++ "::" ++ showTyp (snd v)) (vs))
1180                      showVarsStar = 
1181                          let vs = varsStar gamma in
1182                          case vs of
1183                            [] -> "]"
1184                            _  -> foldr (\x -> \y -> x ++ "," ++ y) "\b]" (map (\v -> showTerm (Var (fst v)) ++ "::" ++ showTyp (snd v)) (vs)) 
1185                 in
1186                 "Cont = {vars = [" ++ showVars ++ ", varsStar = [" ++ showVarsStar ++ "}"
1187
1188 showTerm :: Term -> String
1189 showTerm t = 
1190     case t of
1191     Extra _       -> "ERROR. Extra as Term."
1192     Case1 _ _ _ _ -> "ERROR. Case1 as Term."
1193     _             -> (showAbsTerm t showTerm)
1194
1195 showTermPlus :: Bool -> TermPlus -> String
1196 showTermPlus strip t = 
1197     case t of
1198     Extra (PlusElem (TypVar i) j) -> if strip == False
1199                             then "(p" ++ (show i) ++ "(" ++ show j ++ "))"
1200                             else "(p" ++ (show i) ++ "'(" ++ show j ++ "))"
1201     _                    -> if strip == False 
1202                             then showAbsTerm t (showTermPlus False)
1203                             else showAbsTerm t (showTermPlus True )
1204
1205 showAbsTerm :: (AbsTerm a) -> ((AbsTerm a) -> String) -> String
1206 showAbsTerm t showTerm = case t of
1207                Var (TermVar i)      -> 'x':(show i)
1208                Abs v _ t'           -> "(\\" ++ (showTerm (Var v)) ++ "." ++ (showTerm t') ++ ")"
1209                App t1 t2            -> "(" ++ (showTerm t1) ++ " " ++ (showTerm t2) ++ ")"
1210                Nil _                -> "[]"
1211                Cons t1 t2           -> "(" ++ (showTerm t1) ++ ":" ++ (showTerm t2) ++ ")"
1212                Case t0 t1 v2 t2     -> "(case " ++ (showTerm t0) ++ " of {[] => " ++ (showTerm t1) ++ "; " ++ showTerm (Var v2) ++ ":_ => " ++ (showTerm t2) ++"})" 
1213                Bottom _             -> "_|_"
1214                TAbs (TypVar i) t    -> (showTerm t)
1215                Extra a              -> "No show-function implemented."
1216                Case1 t1 t2 t3 t4    -> "(case " ++ (showTerm t1) ++ " of {" ++ (showTerm t2) ++ " => " ++ (showTerm t3) ++ "; _ => " ++ (showTerm t4) ++ "})"
1217                Pair t1 t2           -> "(" ++ showTerm t1 ++ "," ++ showTerm t2 ++ ")"
1218                PCase t0 v1 v2 t1    -> "(case " ++ showTerm t0 ++ " of {(" ++ showTerm (Var v1) ++ "," ++ showTerm (Var v2) ++ ") => " ++ showTerm t1 ++ "})"
1219                ECase t0 v1 t1 v2 t2 -> "(case " ++ showTerm t0 ++ " of { Left(" ++ showTerm (Var v1) ++ ") => " ++ showTerm t1 ++ "; Right(" ++ showTerm (Var v2) ++ ") => " ++ showTerm t2 ++ "})"
1220                Left t               -> "Left(" ++ showTerm t ++ ")"
1221                Right t              -> "Right(" ++ showTerm t ++ ")"
1222                Zero                 -> "0"                                                                                                                                                      
1223
1224 showTyp :: Typ -> String
1225 showTyp t = case t of
1226               TVar (TypVar i)    -> ('v':(show i))
1227               Arrow t1 t2        -> "(" ++ showTyp t1 ++ " -> " ++ showTyp t2 ++ ")"
1228               All v t            -> "\\" ++ showTyp (TVar v) ++ "." ++ showTyp t
1229               AllStar v t        -> "\\" ++ showTyp (TVar v) ++ "." ++ showTyp t
1230               List t             -> "[" ++ showTyp t ++ "]"
1231               Int                -> "Int"
1232               TPair t1 t2        -> "(" ++ showTyp t1 ++ "," ++ showTyp t2 ++ ")"
1233               TEither t1 t2      -> "(" ++ showTyp t1 ++ "+" ++ showTyp t2 ++ ")"
1234
1235 parseTerm :: String -> Typ
1236 parseTerm str = TVar (TypVar 0) --dummy
1237
1238
1239
1240 --testing fuction
1241 testTerm tau = case runM $ alg emptyCont tau emptyTermCont of
1242                  Nothing    -> Nothing
1243                  Just (x,_) -> Just (fst x)
1244
1245 getIt typstring = getComplete $ parseType typstring
1246