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