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