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