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