packages feed

free-theorems-counterexamples (empty) → 0.3

raw patch · 15 files changed

+3674/−0 lines, 15 filesdep +HUnitdep +basedep +cgisetup-changed

Dependencies added: HUnit, base, cgi, containers, free-theorems, haskell-src, haskell-src-exts, mtl, pretty, syb, utf8-string, xhtml

Files

+ Language/Haskell/FreeTheorems/Variations/CounterExamples/Common/AlgCommon.hs view
@@ -0,0 +1,1419 @@+module Language.Haskell.FreeTheorems.Variations.CounterExamples.Common.AlgCommon +    (TermVar(..), Term(..), TypedVar, TermCont, Cont(..), TrackCont, M, Rule(..), History(..),+     trace, traceIOStart, traceIOFile, traceIO, traceSimplify, traceTemp,+     first, isFst, second, isSnd, listhead, isHead, fromJust, isFromJust, fromLeft, isFromLeft, fromRight, isFromRight,+     firstApp, isFstApp, secondApp, isSndApp, listheadApp, isHeadApp, fromJustApp, isFromJustApp, fromLeftApp, isFromLeftApp,+     fromRightApp, isFromRightApp,+     emptyCont, emptyTermCont, removeVar, removeVarStar, updateTVarStar, updateTVar, updateVar, updateVarStar,+     unpointed, isElementaryType, findfirstSpecialType, findfirstWithTVars, findallWithTVars,+     findfirst, findall,+     typeCheckArrowListArg, typeCheckArrowMaybeArg, typeCheckList, typeCheckMaybe, typeCheckArrowUnPointedArgPointedRes, typeCheckArrowArgArrow,+     typeCheckArrow, typeCheckInt, typeCheckBrace, typeCheckBool, typeCheckPair, typeCheckArrowPairArg,+     typeCheckArrowEitherArg, typeCheckEither, +     insertArgument, subst, substAllInt, makePlusPair, makePlusElem, makeFuncPair, +     initialiseTermCont, mergeTermCont,+     simplifyTerm, simplifyAppOnly, simplifyTermCont, simplifyTrackCont,+     insertTermsInTrackCont, applyTrackCont, assignTypeRelFuncs, getTypeRelFuncNamesNonStrict,+     showVarList, prependRelFunc, getTrackContWithFuncNames, showFuncNames, renumberVariables,+     getVarNums, renumberVars, mapDisRelFuncsToNames, showTermCont, printTermCont, showTermContList,+     printResult, printTyp, showCont, showTerm, showTermWithNames, showTyp, showTrackCont, showRawTrackCont,+     showTrackContApplication, showTrackContApplicationWithNames, getTrackContApplicationSolved, showTrackContApplicationSolved,+     showFuncNamesInt, makeTrackString, trackAll, trackRules) where+++import Prelude hiding (Either(..))+import qualified Prelude as E (Either(..))+import Data.List+import qualified Data.Map as Map+import Control.Monad+import Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.M hiding (M)+import qualified Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.M as Mona (M)+import Language.Haskell.FreeTheorems.Variations.CounterExamples.Parser.ParseType+import Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.FTSync++-- * Debugging options+----------------------------------------------------------------------------------------------+--------------------------DEBUG-TOOLS---------------------------------------------------------+----------------------------------------------------------------------------------------------++import System.IO.Unsafe+-- |set debugging functions from the below list+trace :: String -> a -> a+trace = trace_ignore+--trace = trace_toShell++---- OutputFile options ----+-- |set file where debug output of traceIO is send to++--traceIOStart = traceIOStart_makeFile+traceIOStart = traceIOStart_ignore+traceIOFile = "./traceIO.log.hs"++---- traceIO settings ----+-- | trace informations on every rule, gives context and typ before and after rule application+-- exception: Bottom and Var*+traceIO :: String -> Typ -> Cont -> Typ -> Cont -> a -> a+traceIO = traceIO_ignore+--traceIO = traceIO_ordDiff+--traceIO = traceIO_ord2shell+--traceIO = traceIO_checkOrderInc+--traceIO = traceIO_cont2shell+--traceIO = \rule tauIn gammaIn tauOut gammaOut -> (traceIO_order2shell rule tauIn gammaIn tauOut gammaOut).traceIO_checkOrderInc rule tauIn gammaIn tauOut gammaOut++-- |some more special purpose trace functions+--traceSimplify = trace_toShell+traceSimplify = trace_ignore+traceTemp = trace_toShell++---- show settings ---+-- |show settings for the trace functions+showContTrace = showCont+++---- trace functions ----+-- |trace functions++---- output file variants ----+traceIOStart_ignore file a = a+traceIOStart_makeFile file a = if unsafePerformIO (writeFile traceIOFile "traceIO-File\n\n") == () then a else a++---- trace and traceIO variants ----+trace_ignore str a = a+trace_toShell str a = if unsafePerformIO (putStr (str++"\n")) == () then a else a++traceIO_ignore rule tauIn gammaIn tauOut gammaOut a = a+traceIO_order2shell rule tauIn gammaIn tauOut gammaOut a = +    if unsafePerformIO (putStr (rule ++ ":\t" ++ (show (count gammaOut tauOut)) ++ "\n")) == () then a else a+traceIOOutPut rule tauIn gammaIn tauOut gammaOut ordDiff =+    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"))++--traceIO variants+--outputs a file with input and output types, contexts and the orderdifference (out - in) for every rule applied+traceIO_ordDiff rule tauIn gammaIn tauOut gammaOut a = +    let (ordIn,ordOut) = makeSameLength (count gammaIn tauIn) (count gammaOut tauOut)+        ordDiff = zipWith (-) ordOut ordIn+	good = firstNegative ordDiff+    in+    if (if traceIOOutPut rule tauIn gammaIn tauOut gammaOut ordDiff == () then good else good)+    then a+    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)) ++--outputs pairs of input order ander output order to the shell+traceIO_ord2shell rule tauIn gammaIn tauOut gammaOut a =+    let (ordIn,ordOut) = makeSameLength (count gammaIn tauIn) (count gammaOut tauOut) in+    if unsafePerformIO (putStr ((show ordIn) ++ "\n" ++ (show ordOut) ++ "\n\n")) == () then a else a++--outputs context before and after rule application to the shell+traceIO_cont2shell rule tauIn gammaIn tauOut gammaOut a =+    if unsafePerformIO (putStr (rule ++ ":\n" ++ (showContTrace gammaIn) ++ "\n" ++ (showContTrace gammaOut) ++ "\n\n")) == () then a else a++--stay calm until order increases during a rule and then throw an error+traceIO_checkOrderInc rule tauIn gammaIn tauOut gammaOut a =+    let (ordIn,ordOut) = makeSameLength (count gammaIn tauIn) (count gammaOut tauOut) +	ordDiff = zipWith (-) ordOut ordIn in+    if firstNegative ordDiff+    then a+    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))++-- |helpfunctions for the order check+zeros = 0:zeros++updateAt l idx elem = (take idx l) ++ (elem:(drop (idx+1) l))++getAt l idx = head (drop idx l)++makeSameLength l1 l2 = let len1 = length l1+			   len2 = length l2 in+                       if len1 < len2 +		       then (prependZeros len2 l1,l2)+		       else (l1,prependZeros len1 l2)+  where prependZeros len l = if length l < len+			     then prependZeros len (0:l)+			     else l++count gamma tau = let (l1,l2) = makeSameLength (countCont gamma) ((countTyp tau) ++ [0]) in+	          zipWith (+) l1 l2++countCont :: Cont -> [Int]+countCont gamma = +    let varlist = ((vars gamma) ++ (varsStar gamma)) in+    (countCont' varlist) ++ [(length varlist)]++countCont' vl = +    case vl of+    []   -> [0,0,0,0,0]+    x:xs -> let (l1,l2) = makeSameLength (countCont' xs) (countTyp (snd x)) in+            zipWith (+) l1 l2++countTyp :: Typ -> [Int]+countTyp tau = let (d,el,ol) = countTyp' tau 0 in+	       (reverse (take (d+1) el)) ++ ol+ +--           tau    depth eitherlist (maxdepth,(eitherlist,orderlist)) --lists and maybe are counted together.+countTyp' :: Typ -> Int -> (Int,[Int],[Int])+countTyp' tau depth = +    case tau of+    TVar _            -> (depth,zeros,[0,0,0,0])+    Arrow tau1 tau2   -> let (d1,el1,ol1) = countTyp' tau1 (depth+1)+			     (d2,el2,ol2) = countTyp' tau2 (d1+1) in+			 (max d1 d2, zipWith (+) el1 el2, zipWith (+) (zipWith (+) [0,0,0,1] ol1) ol2)+    All _ tau1        -> let (d,el,ol) = countTyp' tau1 (depth+1) in+			 (d,el,zipWith (+) [1,0,0,0] ol)+    AllStar _ tau1    -> let (d,el,ol) = countTyp' tau1 (depth+1) in+			 (d,el,zipWith (+) [1,0,0,0] ol)+    List tau1         -> let (d,el,ol) = countTyp' tau1 (depth+1) in+			 (d,el,zipWith (+) [0,0,1,0] ol)+    Int               -> (depth,zeros,[0,0,0,0])+    TBrace            -> (depth,zeros,[0,0,0,0])+    TBool             -> (depth,zeros,[0,0,0,0])+    TPair tau1 tau2   -> let (d1,el1,ol1) = countTyp' tau1 (depth+1)+			     (d2,el2,ol2) = countTyp' tau2 (d1+1) in+			 (max d1 d2,zipWith (+) el1 el2, zipWith (+) (zipWith (+) [0,1,0,0] ol1) ol2)+    TEither tau1 tau2 -> let (d1,el1,ol1) = countTyp' tau1 (depth+1)+			     (d2,el2,ol2) = countTyp' tau2 (depth+1) in+			 (max d1 d2,zipWith (+) (updateAt el1 depth ((getAt el1 depth)+1)) el2, zipWith (+) ol1 ol2)+    TMaybe tau1       -> let (d,el,ol) = countTyp' tau1 (depth+1) in+			 (d,el,zipWith (+) [0,0,1,0] ol)++firstNegative l = case l of+	          [] -> False+		  x:xs -> if x == 0 then firstNegative xs+			  else (if x < 0 then True else False) +++----------------------------------------------------------------------------------------------+--------------------------END: DEBUG-TOOLS----------------------------------------------------+----------------------------------------------------------------------------------------------++-- *Data type declarations++-- |Termvariable is taken to be a number. Monad M will keep track of the numbering when new+--  Termvariables are produced.+newtype TermVar = TermVar Int deriving (Show, Eq, Ord)++-- |Syntax of the terms used in the algorithm. The term set is a bit smaller than the whole+--  set of PolyFix*, because Case statements are restricted to make only the kinds used in+--  the algorithm possible.+data Term = Var TermVar   +	  | Abs    TermVar Typ     Term+	  | App    Term    Term+	  | TAbs   TypVar  Term+	  | Nil     Typ+	  | Cons    Term   Term +	  -- |Case statement for lists+          --  Case l v t1 <==> Case l of {[] => _|_; v:_ => t1}+	  | LCase   Term   TermVar Term+	  | Bottom  Typ               -- statt Fix+          | Brace +          -- |integer case-statement+          -- ICase t0 t1 <==> Case t0 of {0 => t1; _ => _|_}+	  | ICase   Term   Term+	  -- |brace case-statement+          -- BCase t0 t1 <==> Case t0 of {() => t1}+	  | BCase   Term   Term +	  -- |bool case-statement+	  -- BoolCase t0 t1 <==> Case t0 of {False => t1; _ => _|_}+	  | BoolCase Term  Term+	  | Fls+	  | Zero+	  | Pair    Term   Term+          -- |case-statement for pairs+          -- PCase p v1 v2 t <==> Case p of {(v1,v2) ==> t}+	  | PCase   Term   TermVar TermVar Term+          -- |case-statement for either+          -- ECase e v1 t1 v2 t2 <==> Case e of {Left(v1) => t1; Right(v2) => t2}+	  | ECase   Term   TermVar Term    TermVar Term+	  | Right   Term+	  | Left    Term+	  -- Terms of TMaybe+	  | MJust   Term+--          | MNothing+          | MCase   Term   TermVar Term+	  deriving (Show, Eq)++-- |abbreviation for the pair (TermVar,Typ)+type TypedVar = (TermVar,Typ)++-- |represents the sigma environments sigma_1 and sigma^+_2. sigma_2 is not tracked.+type TermCont = Map.Map TermVar ((Term,Term),History)++-- |representation of \Gamma and \Sigma, both devided in a stared and unstared part,+--  as necessary regarding an \internalinput.+data Cont = Cont { tVars :: [TypVar], tVarsStar :: [TypVar], vars :: [TypedVar], varsStar :: [TypedVar] } deriving (Show,Eq)++-- |the list of the disrelater. The type has not to be tracked, because it is always clear.+type TrackCont = (Typ,[(Term,Term)])++type M = Mona.M Term++-- we introduce just the rules needed -> where term variables are produced in a non trivial way.+-- if the stared and the unstared variant are equal in historical behaviour, we introduce just the unstared one.+data Rule = WrapTo | MaybeTo | Head | RJust | PairTo | Proj | EitherTo | BottomToStripe | ArrowToStar | Dist1 | Dist2 |BottomTo deriving(Show,Eq)+data History = Branch Rule History | Split Rule History History | Leaf deriving(Show)++-- | some abbreviations for special functions.+-- They are used in the paper as well++-- |\p -> Case p of {(v1,v2) ==> v1}+first :: Typ -> M Term+first tau= do {i<-newInt;+	       j<-newInt;+               k<-newInt;+	       let x = TermVar i+                   y = TermVar j+                   p = TermVar k in+	       return (Abs p tau (PCase (Var p) x y (Var x)))+	      }++-- |Check if a term t is of form "fst"+isFst :: Term -> Bool+isFst t =+    case t of+      Abs _ _ (PCase _ x _ t1) ->+	  if Var x == t1 then True else False+      _                        -> False++-- |\p -> Case p of {(v1,v2) ==> v2}+second :: Typ -> M Term+second tau = do {i<-newInt;+		 j<-newInt;+		 k<-newInt;+		 let x = TermVar i+	             y = TermVar j +		     p = TermVar k in+	       return (Abs p tau (PCase (Var p) x y (Var y)))+	      }++-- |Check if a term t is of form "snd"+isSnd :: Term -> Bool+isSnd t =+    case t of+      Abs _ _ (PCase _ _ y t1) -> +	  if Var y == t1 then True else False+      _                        -> False++-- |\l -> Case l of {[] => _|_; x:_ => x}+listhead :: Typ -> M Term+listhead tau = do {i<-newInt;+		   j<-newInt;+		   let x = TermVar i+		       l = TermVar j in+		     return (Abs l (List tau) (LCase (Var l) x (Var x)))+		    }++-- |Check if a term t is of form "head"+isHead :: Term -> Bool+isHead t =+    case t of+      Abs _ _ (LCase _ v t2) -> +	  if Var v == t2 then True else False+      _                      -> False++-- |\l -> Case l of {Just x => x}+fromJust :: Typ -> M Term+fromJust tau = do {i<-newInt;+		   j<-newInt;+		   let x = TermVar i+		       l = TermVar j in+		     return (Abs l (TMaybe tau) (MCase (Var l) x (Var x)))+		    }++-- |Check if a term t is of form "fromJust"+isFromJust :: Term -> Bool+isFromJust t =+    case t of+      Abs _ _ (MCase _ v t2) -> +	  if Var v == t2 then True else False+      _                      -> False++-- |\e -> Case e of {Left x => x; Right x => _|_}+fromLeft :: Typ -> Typ -> M Term+fromLeft tau tau' = do {i<-newInt;+			j<-newInt;+			k<-newInt;+		     let x = TermVar i+		         y = TermVar j +			 e = TermVar k in+		     return (Abs e (TEither tau tau') (ECase (Var e) x (Var x) y (Bottom tau)))+		    }++-- |Check if a term t is of form "fromLeft"+isFromLeft :: Term -> Bool+isFromLeft t =+    case t of+      Abs _ _ (ECase _ v1 t1 _ t2) -> +	  if Var v1 == t1 +	  then case t2 of+                 Bottom _ -> True+                 _        -> False+	  else False+      _                            -> False++-- |\e -> Case e of {Left x => _|_; Right x => x}+fromRight :: Typ -> Typ -> M Term+fromRight tau tau' = do {i<-newInt;+			 j<-newInt;+			 k<-newInt;+			 let x = TermVar i+		             y = TermVar j+			     e = TermVar k in+		      return (Abs e (TEither tau tau') (ECase (Var e) x (Bottom tau') y (Var y)))+		     }++-- |Check if a term t is of form "fromRight"+isFromRight :: Term -> Bool+isFromRight t =+    case t of+      Abs _ _ (ECase _ _ t1 v2 t2) -> +	  if Var v2 == t2 +	  then case t1 of+                 Bottom _ -> True+                 _        -> False+	  else False+      _                            -> False+++-- | some abbreviations for special cases of the Case-statements.+-- They are used in the paper as well++-- |Case p of {(v1,v2) ==> v1}+firstApp :: Term -> M Term+firstApp p = do {i<-newInt;+		 j<-newInt;+		 let x = TermVar i+	             y = TermVar j in+		 return (PCase p x y (Var x))+		}++-- |Check if a term t is of form "fst t'"+isFstApp :: Term -> Bool+isFstApp t =+    case t of+      PCase _ x _ t1 -> if Var x == t1 then True else False+      _              -> False++-- |Case p of {(v1,v2) ==> v2}+secondApp :: Term -> M Term+secondApp p = do {i<-newInt;+		  j<-newInt;+		  let x = TermVar i+	              y = TermVar j in+		  return (PCase p x y (Var y))+		 }++-- |Check if a term t is of form "snd t'"+isSndApp :: Term -> Bool+isSndApp t =+    case t of+      PCase _ _ y t1 -> if Var y == t1 then True else False+      _              -> False++-- |Case l of {[] => _|_; x:_ => x}+listheadApp :: Term -> Typ -> M Term+listheadApp l tau = do {i<-newInt;+			let x = TermVar i in+			return (LCase l x (Var x))+		       }++-- |Check if a term t is of form "head t'"+isHeadApp :: Term -> Bool+isHeadApp t =+    case t of+      LCase _ v t2 -> if Var v == t2 then True else False+      _            -> False++-- |Case l of {Just x => x}+fromJustApp :: Term -> Typ -> M Term+fromJustApp l tau = do {i<-newInt;+			let x = TermVar i in+			return (MCase l x (Var x))+		       }++-- |Check if a term t is of form "fromJust t'"+isFromJustApp :: Term -> Bool+isFromJustApp t =+    case t of+      MCase _ v t2 -> if Var v == t2 then True else False+      _            -> False++-- |Case e of {Left x => x; Right x => _|_}+fromLeftApp :: Term -> Typ -> M Term+fromLeftApp e tau = do {i<-newInt;+			j<-newInt;+			let x = TermVar i+		            y = TermVar j in+			return (ECase e x (Var x) y (Bottom tau))+		       }++-- |Check if a term t is of form "fromLeft t'"+isFromLeftApp :: Term -> Bool+isFromLeftApp t =+    case t of+      ECase _ v1 t1 _ t2 -> if Var v1 == t1 +			    then case t2 of+                                   Bottom _ -> True+                                   _        -> False+			    else False+      _                  -> False++-- |Case e of {Left x => _|_; Right x => x}+fromRightApp :: Term -> Typ -> M Term+fromRightApp e tau = do {i<-newInt;+			 j<-newInt;+			 let x = TermVar i+		             y = TermVar j in+			 return (ECase e x (Bottom tau) y (Var y))+			}++-- |Check if a term t is of form "fromLeft t'"+isFromRightApp :: Term -> Bool+isFromRightApp t =+    case t of+      ECase _ _ t1 v2 t2 -> if Var v2 == t2 +			    then case t1 of+                                   Bottom _ -> True+                                   _        -> False+			    else False+      _                  -> False+++-- *global constants++-- |global constant: the empty context \Gamma;\Sigma+emptyCont :: Cont+emptyCont = Cont [] [] [] []++-- |global constant: the empty term environments+emptyTermCont :: TermCont+emptyTermCont = Map.empty++-- *Context update functions++updateTVarStar (Cont tVars tVarsStar vars varsStar) tv = Cont tVars (tv:tVarsStar) vars varsStar++updateTVar (Cont tVars tVarsStar vars varsStar) tv = Cont (tv:tVars) tVarsStar vars varsStar++updateVar (Cont tVars tVarsStar vars varsStar) v tau = Cont tVars tVarsStar ((v,tau):vars) varsStar+removeVar (Cont tVars tVarsStar vars varsStar) var = Cont tVars tVarsStar (filter ((/= var).fst) vars) varsStar++updateVarStar (Cont tVars tVarsStar vars varsStar) v tau = Cont tVars tVarsStar vars  ((v,tau):varsStar)+removeVarStar (Cont tVars tVarsStar vars varsStar) var = Cont tVars tVarsStar vars  (filter ((/= var).fst) varsStar)+++-- |check for pointedness.+--  the function implements the class membership rules for PolyFix*+unpointed :: [TypVar] -> Typ -> Bool+unpointed tvars tau = case tau of+                      TVar tvar      -> case find (== tvar) tvars of+                                          Nothing -> False+                                          _       -> True+                      Arrow _ tau'   -> unpointed tvars tau'+                      All tvar tau'  -> unpointed (tvar:tvars) tau'+                      AllStar _ tau' -> unpointed tvars tau'+                      List _         -> False+		      Int            -> False+                      TPair _ _      -> False+                      TEither _ _    -> False+                      TBool          -> False+                      TBrace         -> False+		      TMaybe _       -> False++isElementaryType :: Typ -> Bool+isElementaryType tau =+    case tau of+    Int    -> True+    TVar _ -> True+    TBrace -> True+    TBool  -> True+    _      -> False++-- *check functions for special typed variables in the term variable part of the context Cont+-- they usually take just one part of the context, i.e. a list [TypedVar]++-- |searches for a variable of type typ in vars++findfirstSpecialType :: [TypedVar] -> Typ -> Maybe TypedVar+findfirstSpecialType vars typ =+    case vars of+      []     -> Nothing+      (x:xs) -> if snd x == typ+		then Just x+		else findfirstSpecialType xs typ++-- |returns the first entry of vars, whose type passes the typecheckfunction+--  It uses the type variables for pointed checks+findfirstWithTVars :: ([TypVar] -> Typ -> Bool) -> [TypVar] -> [TypedVar] -> Maybe TypedVar+findfirstWithTVars typecheckfunction tvars vars =+    case vars of+      []     -> Nothing+      (x:xs) -> if typecheckfunction tvars (snd x)+		then Just x +		else findfirstWithTVars typecheckfunction tvars xs++-- |returns the list of all entries of vars, whose types pass the typecheckfunction+--  It uses the type variables for pointed checks+findallWithTVars :: ([TypVar] -> Typ -> Bool) -> [TypVar] -> [(TypedVar)] -> [TypedVar]+findallWithTVars typecheckfunction tvars vars = +    case vars of+      []     -> []+      (x:xs) -> if typecheckfunction tvars (snd x)+		then (x:(findallWithTVars typecheckfunction tvars xs))+		else findallWithTVars typecheckfunction tvars xs++-- |returns the first entry of vars, whose type passes the typecheckfunction+findfirst :: (Typ -> Bool) -> [TypedVar] -> Maybe TypedVar +findfirst typecheckfunction vars = case vars of+                                     []     -> Nothing+                                     (x:xs) -> if typecheckfunction (snd x) +               				       then Just x +				               else findfirst typecheckfunction xs++-- |returns the list of all entries of vars, whose types pass the typecheckfunction+findall :: (Typ -> Bool) -> [TypedVar] -> [TypedVar]+findall typecheckfunction vars = case vars of+                                   []     -> []+                                   (x:xs) -> if typecheckfunction (snd x)+					     then (x:(findall typecheckfunction xs))+			                     else findall typecheckfunction xs++-- ** typecheckfunctions++-- | used for (Wrap->)+typeCheckArrowListArg :: Typ -> Bool+typeCheckArrowListArg tau = case tau of+                              Arrow tau1 _ -> case tau1 of+                                                List _ -> True+                                                _      -> False+			      _            -> False++-- | used for (MaybeWrap->)+typeCheckArrowMaybeArg :: Typ -> Bool+typeCheckArrowMaybeArg tau = case tau of+                              Arrow tau1 _ -> case tau1 of+                                                TMaybe _ -> True+                                                _        -> False+			      _            -> False++-- | used for (Head), (Head*)+typeCheckList :: Typ -> Bool+typeCheckList tau = case tau of+                     List _ -> True+                     _      -> False++-- | used for (Just), (Just*)+typeCheckMaybe :: Typ -> Bool+typeCheckMaybe tau = case tau of+                       TMaybe _ -> True+                       _        -> False++-- | used for (Bottom->*1)+typeCheckArrowUnPointedArgPointedRes :: [TypVar] -> Typ -> Bool+typeCheckArrowUnPointedArgPointedRes tvars tau = case tau of+					           Arrow tau1 tau2 -> unpointed tvars tau1 && (not (unpointed tvars tau2))+                                                   _               -> False+-- | used for (L->->*)+typeCheckArrowArgArrow :: Typ -> Bool+typeCheckArrowArgArrow tau = case tau of+			      Arrow tau1 _ -> case tau1 of+						Arrow _ _ -> True+						_         -> False+			      _            -> False++-- | used for (Bottom->), (Bottom->*2), (App'*)+typeCheckArrow :: Typ -> Bool+typeCheckArrow tau = case tau of+		       Arrow _ _ -> True+		       _         -> False++-- | used for (Drop1)+typeCheckInt :: Typ -> Bool+typeCheckInt tau = case tau of+		     Int -> True+		     _   -> False++-- | used for (Drop2)+typeCheckBrace :: Typ -> Bool+typeCheckBrace tau = case tau of+		     TBrace -> True+		     _      -> False++-- | used for (Drop4)+typeCheckBool :: Typ -> Bool+typeCheckBool tau = case tau of+		     TBool -> True+		     _     -> False++-- | used for (Proj), (Proj*)+typeCheckPair :: Typ -> Bool+typeCheckPair tau = case tau of+		      TPair _ _ -> True+		      _         -> False++-- | used for (Pair->)+typeCheckArrowPairArg :: Typ -> Bool+typeCheckArrowPairArg tau = case tau of+			      Arrow tau1 _ -> case tau1 of+					        TPair _ _ -> True+						_         -> False+			      _            -> False++-- | used for (LE->)+typeCheckArrowEitherArg :: Typ -> Bool+typeCheckArrowEitherArg tau = case tau of+			        Arrow tau1 _ -> case tau1 of+						  TEither _ _ -> True+						  _           -> False+				_            -> False++-- | used for (Dist1), (Dist2), (Dist1*), (Dist2*)+typeCheckEither :: Typ -> Bool+typeCheckEither tau = case tau of+		        TEither _ _ -> True+			_           -> False++-- * support functions++-- | Application of an argument to a function+insertArgument :: Term -> Term -> Term+insertArgument f x = case f of+		     Abs v _ t                 -> subst t x v+		     Bottom (Arrow tau1 tau2)  -> Bottom tau2+		     _ -> error ("unexpected termstructure" ++ (showTerm f))++-- | substitutes new (Term) for old (TermVar) in the term m+subst :: Term -> Term -> TermVar -> Term+subst m new old = case m of+		   Var var              -> if(var == old) then new else m+		   Abs v tau m'         -> Abs v tau (subst m' new old)+                   App m1 m2            -> App (subst m1 new old) (subst m2 new old)+                   TAbs tau m'          -> TAbs tau (subst m' new old)+                   Cons m1 m2           -> Cons (subst m1 new old) (subst m2 new old)+                   LCase m0 v2 m2    -> LCase (subst m0 new old) v2 (subst m2 new old)+		   Pair m1 m2           -> Pair (subst m1 new old) (subst m2 new old)+		   PCase m0 v1 v2 m1    -> PCase (subst m0 new old) v1 v2 (subst m1 new old)+		   Right m              -> Right (subst m new old)+                   Left m               -> Left (subst m new old)+                   ECase m0 v1 m1 v2 m2 -> ECase (subst m0 new old) v1 (subst m1 new old) v2 (subst m2 new old)+		   ICase m0 m1          -> ICase (subst m0 new old) (subst m1 new old)+		   BCase m0 m1          -> BCase (subst m0 new old) (subst m1 new old)					   +		   BoolCase m0 m1       -> BoolCase (subst m0 new old) (subst m1 new old)+                   MJust m0             -> MJust (subst m0 new old)+                   MCase m0 v2 m2       -> MCase (subst m0 new old) v2 (subst m2 new old)+                   _                    -> m++-- | calls subst for a list of termVariables (with according to the numbers) to be substituted+substAllInt :: Term -> [(Int,Term)] -> Term+substAllInt t l =+    case l of+      []        -> t+      (i,t'):xs -> substAllInt (subst t t' (TermVar i)) xs++-- | produces a Pair (p^+,p^+) of the given type, with p+ as described in the plus-term definition of the paper+makePlusPair :: Typ -> M (Maybe (Term, Term))+makePlusPair tau = do {x <- makePlusElem tau; +		       case x of +		       Just t -> return (Just (t,t))+		       _      -> return Nothing+		      }++-- | produces a Term p^+ of the given type, as described in the plus-term definition of the paper+makePlusElem :: Typ -> M (Maybe Term)+makePlusElem tau = case tau of+		   TVar  var         -> return (Just Brace)+		   Arrow tau1 tau2   -> do {x <- makePlusElem tau2;+					    i <- newInt;+					    let erg = case x of+						      Just t -> Just (Abs (TermVar i) tau1 t)+						      _      -> Nothing+					    in+					    return erg+					   }+                   List  tau         -> do {x <- makePlusElem tau;+					    let erg = case x of +						      Just t -> Just (Cons t (Nil tau))+						      _      -> Nothing+					    in+					    return erg+					   }+		   TMaybe tau        -> do {x <- makePlusElem tau;+					    let erg = case x of +						      Just t -> Just (MJust t)+						      _      -> Nothing+					    in+					    return erg+					   }+		   Int               -> return (Just Zero)+                   TBrace            -> return (Just Brace)+                   TBool             -> return (Just Fls)+                   TPair tau1 tau2   -> do {x <- makePlusElem tau1;+					    y <- makePlusElem tau2;+					    let erg = case x of+						      Just t1 -> case y of+								 Just t2 -> Just (Pair t1 t2)+								 Nothing -> Nothing+                                                      Nothing -> Nothing+					    in+					    return erg+					   }+                   +                   TEither tau1 tau2 -> do {x <- makePlusElem tau1;+					    y <- makePlusElem tau2;+					    let erg = case x of +					              Just t1 -> Just (Left t1)+					              _       -> case y of+								 Just t2 -> Just (Right t2)+								 _       -> Nothing+					    in+					    return erg+					   }						+		   _                 -> return Nothing++-- |the function equals the lemma about the function construction (g(x_1),g(x_2))^{\Gamma,\tau}_{\varpi}+makeFuncPair :: Typ -> TrackCont -> Cont -> (Term,Term) -> M (Term,Term)+makeFuncPair tau trc' gamma resPair =+    let (z,z')  = resPair +        (ctau,trc) = trc' in+    case tau of+      TVar beta    -> do {i <- newInt;+			  let w  = TermVar i+		              g' = Abs w tau (BCase (Var w) z') in+			  if unpointed (tVars gamma) tau+			  then return (Abs w tau z, g')+			  else return (Abs w tau (BCase (Var w) z), g')+			 }+      Int          -> do {i <- newInt;+			  let w  = TermVar i in+			  return (Abs w tau (ICase (Var w) z), Abs w tau (ICase (Var w) z'))+			 }++      TBrace       -> do {i <- newInt;+			  let w  = TermVar i in+			  return (Abs w tau (BCase (Var w) z), Abs w tau (BCase (Var w) z'))+			 }++      TBool        -> do {i <- newInt;+			  let w  = TermVar i in+			  return (Abs w tau (BoolCase (Var w) z), Abs w tau (BoolCase (Var w) z'))+			 }++      List tau'    -> case trc of+		        []       -> do{i <- newInt;+				       j <- newInt;+				       let w   = TermVar i+				           h   = TermVar j +				       in+				       return (Abs w tau (LCase (Var w) h z), Abs w tau (LCase (Var w) h z'))+				      }+			_:xs     -> do{i <- newInt;+				       j <- newInt;				       +				       (g,g') <- makeFuncPair tau' (ctau,xs) gamma resPair;+				       let w   = TermVar i+				           u   = TermVar j in+				       return (Abs w tau (LCase (Var w) u (App g  (Var u))),+					       Abs w tau (LCase (Var w) u (App g' (Var u))))+				      }+      TMaybe tau'  -> case trc of+		        []       -> do{i <- newInt;+				       j <- newInt;+				       let w   = TermVar i+				           h   = TermVar j +				       in+				       return (Abs w tau (MCase (Var w) h z), Abs w tau (MCase (Var w) h z'))+				      }+			_:xs     -> do{i <- newInt;+				       j <- newInt;				       +				       (g,g') <- makeFuncPair tau' (ctau,xs) gamma resPair;+				       let w   = TermVar i+				           u   = TermVar j in+				       return (Abs w tau (MCase (Var w) u (App g  (Var u))),+					       Abs w tau (MCase (Var w) u (App g' (Var u))))+				      }+      TPair tau' tau'' -> case trc of+	                   []       -> do{i <- newInt;+					  j <- newInt;+					  k <- newInt;+					  let w = TermVar i +					      x = TermVar j+					      y = TermVar k+					  in+					  return (Abs w tau (PCase (Var w) x y z), Abs w tau (PCase (Var w) x y z'))+					 }+                           (Abs _ _ (PCase _ v _ (Var v')),_):xs ->+			       if v == v' then+				       do{i <- newInt;+					  j <- newInt;+					  m <- newInt;+					  n <- newInt;+					  let x = TermVar j+ 					      y = TermVar m+					      u = TermVar n+					      w = TermVar i+                                              (k,k') = (Abs u tau'' z, Abs u tau'' z')+					  in				 +					  do{(h,h') <- makeFuncPair tau' (ctau,xs) gamma (k,k');+					     return (Abs w tau (PCase (Var w) x y (App (App h (Var x)) (Var y))), Abs w tau (PCase (Var w) x y (App (App h' (Var x)) (Var y))))+					    }+					 }+			       else+				       do{i <- newInt;+					  j <- newInt;+					  m <- newInt;+					  n <- newInt;+					  (k,k') <- makeFuncPair tau'' (ctau,xs) gamma resPair;+					  let x = TermVar j+					      y = TermVar m+					      u = TermVar n+					      w = TermVar i+					      (h,h') = (Abs x tau' (Abs y tau'' (App k (Var y))), Abs x tau' (Abs y tau'' (App k' (Var y))))+					  in+					  return (Abs w tau (PCase (Var w) x y (App (App h (Var x)) (Var y))), Abs w tau (PCase (Var w) x y (App (App h' (Var x)) (Var y))))+					 }+      TEither tau' tau'' -> do{i <- newInt;+			      j <- newInt;+			      let w = TermVar i+			          x = TermVar j+			      in+			      case trc of+                                []       -> return (Abs w tau (ECase (Var w) x (fst resPair) x (fst resPair)),+					            Abs w tau (ECase (Var w) x (fst resPair) x (snd resPair)))+			        (Abs _ _ (ECase _ _ (Var _) _ _),_):xs  ->+			                    do{(g,g') <- makeFuncPair tau' (ctau,xs) gamma resPair;+			                       return (Abs w tau (ECase (Var w) x (App g (Var x))  x (fst resPair)),+					               Abs w tau (ECase (Var w) x (App g' (Var x)) x (snd resPair)))+					      }			                    +			        (Abs _ _ (ECase _ _ _ _ (Var _)),_):xs  ->+                                            do{(g,g') <- makeFuncPair tau'' (ctau,xs) gamma resPair;+					       return (Abs w tau (ECase (Var w) x (fst resPair) x (App g (Var x))),+					               Abs w tau (ECase (Var w) x (snd resPair) x (App g' (Var x))))+					      }+			     }+      Arrow tau' tau'' -> case trc of+		           []         -> do{ i <- newInt;+					     (g,g') <- makeFuncPair tau'' (ctau,[]) gamma resPair;+					     Just (u,u') <- makePlusPair tau';+					     let x = TermVar i in+					     return (Abs x tau' (App g (App (Var x) u)), Abs x tau' (App g' (App (Var x) u')))+					   }+			   (f,f'):xs  -> do {i <- newInt;+					     (g,g') <- makeFuncPair tau'' (ctau,xs) gamma resPair;				     +					     let x = TermVar i in+					     return (Abs x tau' (App g (App f (Var x))), Abs x tau' (App g' (App f' (Var x))))+					    }++-- |support function for the term variable environment initialisation by the rules (Bottom) and (Ax*)+initialiseTermCont :: [TypedVar] -> M TermCont+initialiseTermCont varlist =+    case varlist of+      []         -> return Map.empty+      (x,tau):xs -> do{map    <- initialiseTermCont xs;+		       Just p <- makePlusPair tau;+		       return (Map.insert x (p,Leaf) map)+		      }++-- |tries to melt down the two TermCont from the premise of Arrow->* to one single suitable context. Uses the history therefore+mergeTermCont :: TermCont -> TermCont -> Maybe TermCont+mergeTermCont c1 c2 =+    let difference   = Map.union (Map.difference c1 c2) (Map.difference c2 c1) in+    if Map.filter (\x->x==False) (Map.intersectionWith checkCompareTerm c1 c2) == Map.empty+    then+      Just (Map.union (Map.intersectionWith compareTerm c1 c2) difference)+    else+      Nothing++compareTerm :: ((Term,Term),History) -> ((Term,Term),History) -> ((Term,Term),History)+compareTerm c1 c2 =+    let (_,his1) = c1+        (_,his2) = c2+    in+    if firstIsBetter his1 his2 then c1 else c2++checkCompareTerm c1 c2 =+   let (_,his1) = c1+       (_,his2) = c2+   in+   if firstIsBetter his1 his2 || firstIsBetter his2 his1 then True else False++firstIsBetter :: History -> History -> Bool+firstIsBetter his1 his2 =+    case his1 of+      Leaf -> case his2 of +	         Leaf -> True +		 _     -> False+      Branch rule his ->+               case his2 of+                 Leaf -> True+                 Branch rule' his' -> if rule == rule' then firstIsBetter his his' else False+                 _     -> False+      Split rule hisa hisb ->+               case his2 of+                 Leaf -> True+                 Split rule' hisa' hisb' -> if rule == rule' then (firstIsBetter hisa hisa' && firstIsBetter hisb hisb') else False+		 _     -> False++-- *simplifications++-- |removes App in terms. Resolves case statements if possible. Destroys the typing information.+simplifyTerm :: Term -> Term+simplifyTerm t = +    case t of+    Abs v tau t1          -> traceSimplify "Simpl: Abs v tau t1" (Abs v tau (simplifyTerm t1))+    App t1 t2             -> let t1' = simplifyTerm t1 in+			     case t1' of+                             Bottom _ -> traceSimplify "Simpl: App _|_ t2" (Bottom (error "Typ not valid anymore."))+			     Abs v tau t1''           -> traceSimplify "Simpl: App (Abs _) t2" (simplifyTerm (subst t1'' (simplifyTerm t2) v))+			     --case-statements can appear.+			     _                        -> traceSimplify "Simpl: App not reduced." (App t1' (simplifyTerm t2))+    TAbs v t1             -> traceSimplify "Simpl: TAbs eliminated." (simplifyTerm t1)+    Cons t1 t2            -> traceSimplify "Simpl: Cons." (Cons (simplifyTerm t1) (simplifyTerm t2))+    LCase t1 v t3      -> let t1' = simplifyTerm t1 in+			     case t1' of+                             Bottom _          -> traceSimplify "Simpl: List Case with _|_ to _|_" (Bottom (error "Typ not valid anymore."))+			     Nil _             -> error "LCase with []! This should not appear!"+			     Cons t (Nil _)    -> traceSimplify "Simpl: List Case with x:_ to t3[t/v]" (simplifyTerm (subst t3 t v))+			     Cons t _          -> error "List with mor than one element! This should not appear!"+                             _                 -> traceSimplify "Simpl: List Case not reduced." (LCase t1' v (simplifyTerm t3))+    ICase t1 t2           -> let t1' = simplifyTerm t1 in+			     case t1' of+			     Bottom tau -> traceSimplify "Simpl: ICase with _|_ to _|_" (Bottom (error "Typ not valid anymore."))+                             Zero     -> traceSimplify "Simpl: ICase with 0 to t1" (simplifyTerm t2)+                             _        -> traceSimplify "Simpl: ICase not reduced." (ICase (simplifyTerm t1) (simplifyTerm t2))+    BCase t1 t2           -> let t1' = simplifyTerm t1 in+			     case t1' of+			     Bottom tau -> traceSimplify "Simpl: BCase with _|_ to _|_" (Bottom (error "Typ not valid anymore."))+                             Brace      -> traceSimplify "Simpl: BCase with () to t1" (simplifyTerm t2)+                             _          -> traceSimplify "Simpl: BCase not reduced." (BCase (simplifyTerm t1) (simplifyTerm t2))+    BoolCase t1 t2        -> let t1' = simplifyTerm t1 in+			     case t1' of+			     Bottom tau -> traceSimplify "Simpl: BoolCase with _|_ to _|_" (Bottom (error "Typ not valid anymore."))+                             Fls        -> traceSimplify "Simpl: BoolCase with Fls to t1" (simplifyTerm t2)+                             _          -> traceSimplify "Simpl: BoolCase not reduced." (BoolCase (simplifyTerm t1) (simplifyTerm t2))+    Pair t1 t2            -> traceSimplify "Simpl: Pair: reducing components." (Pair (simplifyTerm t1) (simplifyTerm t2))+    PCase t1 v1 v2 t2     -> case simplifyTerm t1 of+			     Pair t11 t12 -> traceSimplify "Simpl: PCase with Pair to t2[t11/v1,t12/v2]" (simplifyTerm (subst (subst t2 t11 v1) t12 v2))+                             Bottom _     -> traceSimplify "Simpl: PCase with _|_ to _|_" (Bottom (error "Typ not valid anymore."))+			     _            -> traceSimplify "Simpl: PCase not reduced." (PCase (simplifyTerm t1) v1 v2 (simplifyTerm t2))+    ECase t1 v1 t2 v2 t3  -> case simplifyTerm t1 of+                             Left t1'  -> traceSimplify "Simpl: ECase with Left t1' to t2[t1'/v1]" (simplifyTerm (subst t2 t1' v1))+			     Right t1' -> traceSimplify "Simpl: ECase with Left t1' to t3[t1'/v2]" (simplifyTerm (subst t3 t1' v2))+			     Bottom _  -> traceSimplify "Simpl: ECase with _|_ to _|_" (Bottom (error "Typ not valid anymore."))+		             _         -> traceSimplify "Simpl: ECase not reduced." (ECase (simplifyTerm t1) v1 (simplifyTerm t2) v2 (simplifyTerm t3))+    Right t1              -> traceSimplify "Simpl: Right" (Right (simplifyTerm t1))+    Left t1               -> traceSimplify "Simpl: Left" (Left (simplifyTerm t1))+    Var _                 -> t+    Nil _                 -> t+    Bottom _              -> t+    Zero                  -> Zero+    Brace                 -> Brace+    Fls                   -> Fls+    MJust t1              -> traceSimplify "Simpl: MJust." (MJust (simplifyTerm t1))+    MCase t1 v t2         -> let t1' = simplifyTerm t1 in+			         case t1' of+                                 Bottom _ -> traceSimplify "Simpl: Maybe Case with _|_ to _|_" (Bottom (error "Typ not valid anymore."))+                                 MJust t  -> traceSimplify "Simpl: Maybe Case with Just x to t2[t1/v]" (simplifyTerm (subst t2 t v))+			         _        -> traceSimplify "Simpl: Maybe Case not reduced." (MCase t1' v (simplifyTerm t2))++-- |simplifier for terms, just inserting function arguments, if possible. It does not resolve case-statements, but removes type abstractions.+simplifyAppOnly :: Term -> Term+simplifyAppOnly t =+    case t of+    Abs v tau t1          -> Abs v tau (simplifyAppOnly t1)+    App t1 t2             -> let t1' = simplifyAppOnly t1 in+			     case t1' of+                             Bottom _            -> Bottom (error "Typ not valid anymore.")+			     Abs v tau t1''      -> simplifyAppOnly (subst t1'' (simplifyAppOnly t2) v)+			     _                   -> App t1' (simplifyAppOnly t2) --for App, Var and Case-statements+    TAbs v t1             -> simplifyAppOnly t1+    Cons t1 t2            -> Cons (simplifyAppOnly t1) (simplifyAppOnly t2)+    LCase t1 v t3         -> LCase (simplifyAppOnly t1) v (simplifyAppOnly t3)+    ICase t1 t2           -> ICase (simplifyAppOnly t1) (simplifyAppOnly t2)+    BCase t1 t2           -> BCase (simplifyAppOnly t1) (simplifyAppOnly t2)+    BoolCase t1 t2        -> BoolCase (simplifyAppOnly t1) (simplifyAppOnly t2)+    Pair t1 t2            -> Pair (simplifyAppOnly t1) (simplifyAppOnly t2)+    PCase t1 v1 v2 t2     -> PCase (simplifyAppOnly t1) v1 v2 (simplifyAppOnly t2)+    ECase t1 v1 t2 v2 t3  -> ECase (simplifyAppOnly t1) v1 (simplifyAppOnly t2) v2 (simplifyAppOnly t3)+    Right t1              -> Right (simplifyAppOnly t1)+    Left t1               -> Left (simplifyAppOnly t1)+    Var _                 -> t+    Nil _                 -> t+    Bottom _              -> t+    Zero                  -> Zero+    Brace                 -> Brace+    Fls                   -> Fls+    MJust t1              -> MJust (simplifyAppOnly t1)+    MCase t1 v t2         -> MCase (simplifyAppOnly t1) v (simplifyAppOnly t2)+--    _                     -> error ("unexpected Term structure during simplification: " ++ (showTerm t))++-- |calls simplifyTerm for all Terms in the TermCont (term variable environments)+simplifyTermCont :: TermCont -> TermCont+simplifyTermCont c = +    let simplifyPair ((t1,t2),his) = ((simplifyTerm t1, simplifyTerm t2),his) in+    Map.map simplifyPair c    +++-- | calls simplifyTerm for all Terms in the list of the disrelater, i.e. for all entries of TrackCont+simplifyTrackCont :: TrackCont -> TrackCont+simplifyTrackCont trc =+    let (ctau,l) = trc in+    (ctau,simplifyTrackCont' l)++simplifyTrackCont' trc =+    case trc of +    []         -> []+    (v1,v2):xs -> (simplifyTerm v1, simplifyTerm v2):(simplifyTrackCont' xs)++-- | replaces term variables in the disrelater by the terms they represent (given in the map)+-- maybe buggy+insertTermsInTrackCont :: TrackCont -> (Map.Map Int Term) -> TrackCont+insertTermsInTrackCont trc substs =+    let (ctau,ls) = trc in+    (ctau,map sub ls)+  where sub t = let (t1,t2) = t in (sub' t1, sub' t2) +        sub' t =+ 	    case t of+ 	      Abs x tau (App y (Var (TermVar i))) -> +		     if Var x == y && Map.member i substs +		     then Abs x tau (App y (substs Map.! i))+		     else t+              _               -> t++-- | applies the disrelater to a term. This should lead to (p+,_|_) or (_|_._|_) for a term with a corresponding disrelater+--   and all termvariables substituted by the corresponding terms.+applyTrackCont :: Term -> TrackCont -> (Term,Term)+applyTrackCont t trc = +    let (_,l) = trc in applyTrackCont' (t,t) l++applyTrackCont' :: (Term,Term) -> [(Term,Term)] -> (Term,Term)+applyTrackCont' (t1,t2) trc = +    case trc of+    []   -> (t1,t2)+    x:xs -> applyTrackCont' (App (fst x) t1, App (snd x) t2) xs++-- *output enhancement and synchronisation with free-theorems package++-- | instantiate type relating functions.+-- | input is the type and a list of functionnames, representing the sequence in which they should be used+assignTypeRelFuncs :: Typ -> [String] -> String+assignTypeRelFuncs tau names = foldr (\x y -> ((getAt names (fst x)) ++ " = " ++ (snd x)) ++ y) "" (sort (assignTypeRelFuncs' tau))++assignTypeRelFuncs' :: Typ -> [(Int,String)]+assignTypeRelFuncs' tau =+    case tau of+    All (TypVar i) tau'     -> (i-1, "const ()\t"):assignTypeRelFuncs' tau'+    AllStar (TypVar i) tau' -> (i-1, "id\t\t"):assignTypeRelFuncs' tau'+    _                       -> []+++-- | get a list of names of the type variables that can be interpreted non-strict.+getTypeRelFuncNamesNonStrict :: Typ -> [String] -> [String]+getTypeRelFuncNamesNonStrict tau names =+    snd.unzip.sort.getList $ tau+  where getList tau =+	    case tau of+	      All (TypVar i) tau'     -> (i-1, getAt names (i-1)):getList tau'+              AllStar (TypVar i) tau' -> getList tau'+              _                       -> []+showVarList l =+    case l of+      []   -> ""+      [v]  -> v+      v:vs -> v ++ "," ++ showVarList vs++prependRelFunc :: [String] -> Typ -> String -> String+prependRelFunc names tau str =+    case tau of+    TVar (TypVar i) -> getAt names (i-1) ++ " " ++ str+    _               -> str -- an elementary type (TBool, Int, TBrace). Relation is id and therefore dropped.++getTrackContWithFuncNames :: [String] -> TrackCont -> ([(String,Term)],String)+getTrackContWithFuncNames names trc =+    let (_,l) = trc+        (funcs,dis1,dis2) = getTrackContWithFuncNames' names l in+    (funcs,dis1 ++ " $ t = " ++ dis2 ++ " $ t")++getTrackContWithFuncNames' :: [String] -> [(Term,Term)] -> ([(String,Term)],String,String)+getTrackContWithFuncNames' names l =+    case l of+      []         -> ([],"","")+      [(t1,t2)]  -> if (isHead t1 || isFromLeft t1 || isFromRight t1 || isFst t1 || isSnd t1)+		    then ([], showTerm t1, showTerm t2)+		    else ([(head names,t1),(head (tail names),t2)], head names, head (tail names))+      (t1,t2):xs -> if (isHead t1 || isFromLeft t1 || isFromRight t1 || isFst t1 || isSnd t1)+		    then +		      let (dis,str1,str2) = getTrackContWithFuncNames' names xs in+                      (dis, showTerm t1 ++ "." ++ str1, showTerm t2 ++ "." ++ str2)+		    else+                      let (dis,str1,str2) = getTrackContWithFuncNames' (drop 2 names) xs in+                      ([(head names,t1),(head (tail names),t2)] ++ dis,str1 ++ " . " ++  head names, str2 ++ " . " ++ head (tail names))+++showFuncNames :: [(String,Term)] -> String+showFuncNames funcNames =+    case funcNames of+      []             -> ""+      (name,func):xs -> name ++ "\t = " ++ showTerm (head.renumberVariables $[simplifyTerm func]) ++ "\n" ++ showFuncNames xs++-- | renumbers term variables in a list of terms, such that different numbers stay different, but numbers are+--   decreased as far as possible+renumberVariables::[Term] -> [Term]+renumberVariables input =+    let vars = nub (getNums input)+        varNum = length vars +        varMap = Map.fromList (zip vars [1..varNum]) in+        renumber input varMap+  where getNums terms =+            case terms of+              []   -> []+              x:xs -> getVarNums x ++ getNums xs+        renumber terms varMap =+            case terms of+              []   -> []+              x:xs -> renumberVars x varMap : renumber xs varMap++-- | returns a list with all variable numbers used in a term.+getVarNums term =+    case term of+      Var (TermVar i)      -> if i == 0 then [] else [i]+      Abs (TermVar i) _ t' -> i:getVarNums t'+      App t1 t2            -> getVarNums t1 ++ getVarNums t2+      Nil _                -> []+      Cons t1 t2           -> getVarNums t1 ++ getVarNums t2+      LCase t0 (TermVar i) t2 -> getVarNums t0 ++ [i] ++ getVarNums t2+      Bottom _             -> []+      TAbs (TypVar i) t    -> getVarNums t+      Brace                -> []+      ICase t1 t2          -> getVarNums t1 ++ getVarNums t2+      BCase t1 t2          -> getVarNums t1 ++ getVarNums t2+      BoolCase t1 t2       -> getVarNums t1 ++ getVarNums t2+      Pair t1 t2           -> getVarNums t1 ++ getVarNums t2+      PCase t0 (TermVar i) (TermVar j) t1 -> getVarNums t0 ++ [i,j] ++ getVarNums t1 +      ECase t0 (TermVar i) t1 (TermVar j) t2 -> getVarNums t0 ++ [i,j] ++ getVarNums t1 ++ getVarNums t2+      Left t               -> getVarNums t+      Right t              -> getVarNums t+      Zero                 -> []+      Fls                  -> []+      MJust t              -> getVarNums t+      MCase t0 (TermVar i) t2 -> getVarNums t0 ++ [i] ++ getVarNums t2++-- | renumbers term variables in a term as stated in the given map.+renumberVars term varMap =+    case term of+      Var (TermVar i)      -> if i == 0 then term else Var (TermVar (varMap Map.! i))+      Abs (TermVar i) tau t' -> Abs (TermVar (varMap Map.! i)) tau (renumberVars t' varMap)+      App t1 t2            -> App (renumberVars t1 varMap) (renumberVars t2 varMap)+      Nil _                -> term+      Cons t1 t2           -> Cons (renumberVars t1 varMap) (renumberVars t2 varMap)+      LCase t0 (TermVar i) t2 -> LCase (renumberVars t0 varMap) (TermVar (varMap Map.! i)) (renumberVars t2 varMap)+      Bottom _             -> term+      TAbs tv t            -> TAbs tv (renumberVars t varMap)+      Brace                -> Brace+      ICase t1 t2          -> ICase (renumberVars t1 varMap) (renumberVars t2 varMap)+      BCase t1 t2          -> BCase (renumberVars t1 varMap) (renumberVars t2 varMap)+      BoolCase t1 t2       -> BoolCase (renumberVars t1 varMap) (renumberVars t2 varMap)+      Pair t1 t2           -> Pair (renumberVars t1 varMap) (renumberVars t2 varMap)+      PCase t0 (TermVar i) (TermVar j) t1 -> PCase (renumberVars t0 varMap) (TermVar (varMap Map.! i)) (TermVar (varMap Map.! j)) (renumberVars t1 varMap)+      ECase t0 (TermVar i) t1 (TermVar j) t2 -> ECase (renumberVars t0 varMap) (TermVar (varMap Map.! i)) (renumberVars t1 varMap) (TermVar (varMap Map.! j)) (renumberVars t2 varMap)+      Left t               -> Left (renumberVars t varMap)+      Right t              -> Right (renumberVars t varMap)+      Zero                 -> Zero+      Fls                  -> Fls+      MJust t1             -> MJust (renumberVars t1 varMap)+      MCase t0 (TermVar i) t2 -> MCase (renumberVars t0 varMap) (TermVar (varMap Map.! i)) (renumberVars t2 varMap)++-- | takes a list with pairs (Int,Term), a list of function names and variable names and returns a list of (Int,String),+--   mapping each Int in the input list to a name out of the function or variable names+mapDisRelFuncsToNames :: [(Int,Term)] -> [String] -> [String] -> [(Int,String)]+mapDisRelFuncsToNames funcList funcs vars =+    case funcList of+     []               -> []+     (i,t1):(j,t2):ls -> case t1 of+                           Abs _ _ _ -> (i,head funcs):(j,head.tail $ funcs):mapDisRelFuncsToNames ls (tail.tail $ funcs) vars+                           _         -> (i,head vars):(j,(head vars ++ "'")):mapDisRelFuncsToNames ls funcs (tail vars)++-- *show and print functions++-- |returns the number of and a string with the term variable environment entries+showTermCont :: TermCont -> String+showTermCont tc = "Number of entries: " ++ (show (Map.size tc)) ++ "\n\n" ++ (showTermContList (Map.toList tc))++-- |prints the number of and the term variable environments entries+printTermCont :: TermCont -> IO() +printTermCont tc = putStr (showTermCont tc)++-- |returns a string with the term context entries followed by "Nothing left.". It takes the context in form of a list.+showTermContList :: [(TermVar,((Term,Term),History))] -> String+showTermContList l = case l of+		     []                 -> "Nothing left.\n"+		     (v,((x,x'),_)):xs  ->   (showTerm (Var v)) ++ "  = " ++ (showTerm x) ++ "\n"+			                  ++ (showTerm (Var v)) ++ "' = " ++ (showTerm x')  ++ "\n\n"+			                  ++ (showTermContList xs)++-- |prints the term with prefix "result term: "+printResult ::  Term -> IO ()+printResult t = putStr ("result term: " ++ (showTerm t) ++ "\n\n")++-- |prints the typ with prefix "input type:  "+printTyp :: Typ -> IO ()+printTyp t = putStr ("input type:  " ++ showTyp t ++ "\n")++-- |returns a string with the \Gamma and \Sigma - context entries+showCont :: Cont -> String+showCont gamma = let showVars = +			 let vs = vars gamma in +			 case vs of+			  [] -> "]"+			  _  -> foldr (\x -> \y -> x ++ "," ++ y) "\b]" (map (\v -> showTerm (Var (fst v)) ++ "::" ++ showTyp (snd v)) (vs))+		     showVarsStar = +			 let vs = varsStar gamma in+		         case vs of+			   [] -> "]"+			   _  -> foldr (\x -> \y -> x ++ "," ++ y) "\b]" (map (\v -> showTerm (Var (fst v)) ++ "::" ++ showTyp (snd v)) (vs)) +		in+		"Cont = {vars = [" ++ showVars ++ ", varsStar = [" ++ showVarsStar ++ "}"++-- | pretty printer for Term.+--   All term variables are named by 'x' followed by a number.+showTerm :: Term -> String+showTerm t = showTermWithNames t Map.empty++-- | pretty printer for Term, where a map with special names for term variables can be given.+--   A term variable i with i in the map is is printed as the name provided for i in the map.+--   All other term variables are printed as 'x' followed by their number.+showTermWithNames :: Term -> (Map.Map Int String) -> String+showTermWithNames t m = +             case t of+	       Var (TermVar i)      -> if i == 0 then termName +				       else if Map.member i m then m Map.! i else 'x':(show i)+	       Abs v _ t'           -> if isHead t then "head"+				       else if isFst t then "fst"+				       else if isSnd t then "snd"+				       else if isFromLeft t then "fromLeft"+                                       else if isFromRight t then "fromRight"+                                       else if isFromJust t then "fromJust"+				       else "(\\" ++ showTermWithNames (Var v) m ++ " -> " ++ showTermWithNames t' m ++ ")"+               App t1 t2            -> "(" ++ showTermWithNames t1 m ++ " " ++ showTermWithNames t2 m ++ ")"+               Nil _                -> "[]"+               Cons t1 t2           -> case t2 of+					 Nil _ -> "[" ++ showTermWithNames t1 m ++ "]"+                                         _     -> "(" ++ showTermWithNames t1 m ++ ":" ++ showTermWithNames t2 m ++ ")"+               LCase t0 v2 t2    -> if isHeadApp t +				       then "(head " ++ showTermWithNames t0 m ++ ")" +                                       else "(case " ++ showTermWithNames t0 m ++ " of {[" ++ showTermWithNames (Var v2) m ++ "] -> " ++ showTermWithNames t2 m ++"})"+	       Bottom _             -> "_|_"+               TAbs (TypVar i) t    -> showTermWithNames t m+	       Brace                -> "()"+               Fls                  -> "False"+	       ICase t1 t2          -> "(case " ++ showTermWithNames t1 m ++ " of {0 -> " ++ showTermWithNames t2 m ++ "})"+	       BCase t1 t2          -> "(case " ++ showTermWithNames t1 m ++ " of {() -> " ++ showTermWithNames t2 m ++ "})"+	       BoolCase t1 t2       -> "(case " ++ showTermWithNames t1 m ++ " of {False -> " ++ showTermWithNames t2 m ++ "})"+               Pair t1 t2           -> "(" ++ showTermWithNames t1 m ++ "," ++ showTermWithNames t2 m ++ ")"+	       PCase t0 v1 v2 t1    -> if isFstApp t +				       then "(fst " ++ showTermWithNames t0 m ++ ")"+				       else if isSndApp t+					    then "(snd " ++ showTermWithNames t0 m ++ ")"+                                            else "(case " ++ showTermWithNames t0 m ++ " of {(" ++ showTermWithNames (Var v1) m ++ "," ++ showTermWithNames (Var v2) m ++ ") -> " ++ showTermWithNames t1 m ++ "})"+	       ECase t0 v1 t1 v2 t2 -> if isFromLeftApp t+				       then "(fromLeft " ++ showTermWithNames t0 m ++ ")"+                                       else if isFromRightApp t+					    then "(fromRight " ++ showTermWithNames t0 m ++ ")"+                                            else "(case " ++ showTermWithNames t0 m ++ " of {Left " ++ showTermWithNames (Var v1) m ++ " -> " ++ showTermWithNames t1 m ++ "})"+					--right branch should be unnecessary, since pLusVal always returns Left-value and, if+                                        --not fromLeft/fromRight, it should be always "case pLusVal of", and hence Left.+					 -- ; Right " ++ showTermWithNames (Var v2) m ++ " -> " ++ showTermWithNames t2 m ++ "})"+               Left t               -> "Left " ++ showTermWithNames t m+               Right t              -> "Right " ++ showTermWithNames t m+               Zero                 -> "0"+               MJust t1             -> "(Just " ++ showTermWithNames t1 m ++ ")"+               MCase t0 v2 t2    -> if isFromJustApp t +				       then "(fromJust " ++ showTermWithNames t0 m ++ ")" +                                       else "(case " ++ showTermWithNames t0 m ++ " of {Just " ++ showTermWithNames (Var v2) m ++ " -> " ++ showTermWithNames t2 m ++"})"++-- |pretty printer for Typ+showTyp :: Typ -> String+showTyp t = case t of+              TVar (TypVar i)    -> ('v':(show i))+              Arrow t1 t2        -> "(" ++ showTyp t1 ++ " -> " ++ showTyp t2 ++ ")"+              All v t1           -> "\\" ++ showTyp (TVar v) ++ "." ++ showTyp t1+              AllStar v t1       -> "\\" ++ showTyp (TVar v) ++ "." ++ showTyp t1+              List t1            -> "[" ++ showTyp t1 ++ "]"+              Int                -> "Int"+              TPair t1 t2        -> "(" ++ showTyp t1 ++ "," ++ showTyp t2 ++ ")"+              TEither t1 t2      -> "(Either " ++ showTyp t1 ++ " " ++ showTyp t2 ++ ")"+	      TBrace             -> "()"+              TBool              -> "Bool"+              TMaybe t1          -> "(Maybe " ++ showTyp t1 ++ ")"++-- | returns a string with the disrelater entries with pretty printing+showTrackCont :: TrackCont -> String+showTrackCont trackCont = +    let (ctau,trc) = trackCont in +    showTrackCont' trc ++ "The type is: " ++ showTyp ctau ++ "\n\n"++showTrackCont' trc =+    case trc of+    []         -> ""+    (x1,x2):xs -> (showTerm x1) ++ "\n" +++		  (showTerm x2) ++ "\n\n" +++		  showTrackCont' xs+++-- | returns a string with the disrelater entries _without_ pretty printing+showRawTrackCont :: TrackCont -> String+showRawTrackCont trackCont = +    let (ctau,trc) = trackCont in +    showRawTrackCont' trc ++ "The type is: " ++ show ctau ++ "\n\n"++showRawTrackCont' trc =+    case trc of+    []         -> ""+    (x1,x2):xs -> (show x1) ++ "\n" +++		  (show x2) ++ "\n\n" +++		  showRawTrackCont' xs++-- | applies the disrelater to the term and shows the simplified result as equation t1 = t2+showTrackContApplication :: TrackCont -> Term -> String+showTrackContApplication tc t = showTrackContApplicationWithNames tc [] t++-- | applies the disrelater to the term and shows the simplified result as equation t1 = t2+--   Furthermore variables in the nameList are printed by the given name instead of 'x' and+--   there number.+showTrackContApplicationWithNames :: TrackCont ->[(Int,String)] -> Term -> String+showTrackContApplicationWithNames tc nameList t =+    let (t1,t2) = applyTrackCont t tc +        names   = Map.fromList nameList in+    showTermWithNames (simplifyTerm t1) names ++ " = " ++ showTermWithNames (simplifyTerm t2) names++-- | replaces the term variables with number i by the respective Term given in the (Int,Term)-list+--   and then applies the disrelater to the term and simplifies the result.+getTrackContApplicationSolved :: TrackCont -> [(Int,Term)] -> Term -> (Term,Term)+getTrackContApplicationSolved tc substs t =+    let (t1',t2') = (applyTrackCont t tc)+        (t1,t2)   = (substAllInt t1' substs, substAllInt t2' substs) in+    (simplifyTerm t1,simplifyTerm t2)++showTrackContApplicationSolved :: TrackCont -> [(Int,Term)] -> Term -> String+showTrackContApplicationSolved tc substs t =+    let (t1,t2) = getTrackContApplicationSolved tc substs t in+    showTerm t1 ++ " = " ++ showTerm t2++showFuncNamesInt :: [(Int,Term)] -> String+showFuncNamesInt funcNames =+    case funcNames of+      []             -> ""+      (i,func):xs -> "x"++ show i ++ "\t = " ++ showTerm (head.renumberVariables $[simplifyTerm func]) ++ "\n" ++ showFuncNamesInt xs++-- *Set of functions for calling the algorithm++-- ** Monad features+-- | set the information the monad should return+makeTrackString :: String -> Cont -> Typ -> String+makeTrackString = trackRules ++-- | return the applied rules with input contexts and type+trackAll :: String -> Cont -> Typ -> String+trackAll rule gamma tau = rule ++ ": " ++ showCont gamma ++ ", Type = " ++ showTyp tau++-- | return the applied rules+trackRules :: String -> Cont -> Typ -> String+trackRules rule gamma tau = rule++
+ Language/Haskell/FreeTheorems/Variations/CounterExamples/ExFind.hs view
@@ -0,0 +1,168 @@+-- * The module ExFind contains the calling functions for the algorithm.++module Language.Haskell.FreeTheorems.Variations.CounterExamples.ExFind (getTerm, getComplete, getForWebInterface,+     getWithDebug, testTerm, getIt, getContradiction, getItContradiction, getRawContradiction,+     getItRawContradiction, getExample, getItExample, testSimple, webInterface) where++import Language.Haskell.FreeTheorems.Variations.CounterExamples.Common.AlgCommon+import Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.ExFindExtended+import Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.M hiding (M)+import qualified Prelude as E (Either(..))+import Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.FTSync+import Prelude hiding (Either(..))+import Language.Haskell.FreeTheorems.Variations.CounterExamples.Parser.ParseType+import qualified Data.Map as Map++-- ** calling functions for ExFind++-- | takes the input in Typ format and returns the monad's debuging information and the result term+getTerm :: Typ -> IO()+getTerm tau = do printTyp tau+		 putStr "\n"+	         case runM $ alg emptyCont tau emptyTermCont of+	           Nothing             -> putStr "No Term."+		   Just ((term,termCont,trackCont),debug,funcNames) -> do putStr ("    " ++ (foldr (\x -> \y -> x ++ "\n    " ++ y) "\n" debug))+					                                  printResult (term)++-- | takes the input in Typ format and returns the monad's tracking information, the result term t, the disrelater applied to 't' as variable and as term+getComplete :: Typ -> IO()+getComplete tau = do {printTyp tau;+		      putStr "\n";+		      case runM $ alg emptyCont tau emptyTermCont of+		      Nothing             -> putStr "No Term."+		      Just ((term,termCont,trackCont),debug,funcs) -> +		          do {putStr ("    " ++ (foldr (\x -> \y -> x ++ "\n    " ++ y) "\n" debug));+			      printResult (term);+			      putStr ("Like webinterface:\n\n" ++ showTrackContApplication trackCont (Var (TermVar 0)) ++ "\n\n");+			      putStr ("With the disrelater:\n\n" ++ showTrackContApplication trackCont term ++"\n\n");+			      putStr ("And the variables are:\n\n" ++ showFuncNamesInt funcs ++ "\n\n");+			      putStr ("And completely solved: " ++ showTrackContApplicationSolved trackCont funcs term ++ "\n\n");+			     }+		     }++-- | Output for the webinterface defined in polyfix-cgi.hs (second version)+getForWebInterface :: Typ -> E.Either String (Term,TrackCont,[(Int,Term)])+getForWebInterface tau =+    case runM $ alg emptyCont tau emptyTermCont of+      Nothing             -> E.Left "No Term."+      Just ((term,termCont,trackCont),debug,funcs) -> E.Right (term,trackCont,funcs)+++-- | takes the input in Typ format and returns the monad's tracking information, the result term t and all term variable environment entries+getWithDebug :: Typ -> IO()+getWithDebug tau = do {printTyp tau;+		      putStr "\n";+		      case runM $ alg emptyCont tau emptyTermCont of+		      Nothing             -> putStr "No Term."+		      Just ((term,termCont,trackCont),debug,funcs) -> +		          do {putStr ("    " ++ (foldr (\x -> \y -> x ++ "\n    " ++ y) "\n" debug));+			      printResult (term);+			      printTermCont (termCont);+			      putStr (showTrackCont trackCont);+			     }+		     }++-- | takes the input in Typ format and returns the result term+testTerm :: Typ -> Maybe Term+testTerm tau = case runM $ alg emptyCont tau emptyTermCont of+		 Nothing    -> Nothing+                 Just ((term,termCont,trackCont),_,_) -> Just (term)++-- | getComplete with prepended type parsing+getIt :: String -> IO()+getIt typstring = getComplete $ parseType typstring++-- | takes the input in Typ format and returns the monad's tracking information, the disrelater entries, the term environment entries, the result term t and the result of the application of the disrelater to the term t. All in pretty printing.+getContradiction :: Typ -> IO()+getContradiction tau = +    case runM $ alg emptyCont tau emptyTermCont of+    Nothing    -> putStr "No Term.\n"+    Just ((term,termCont,trackCont),debug,funcs) ->+	let (t1',t2') = applyTrackCont term trackCont +	    (t1,t2)   = (simplifyTerm t1', simplifyTerm t2') in+            putStr ("    " ++ (foldr (\x -> \y -> x ++ "\n    " ++ y) "\n" debug) +++		    "TrackCont:\n\n" ++ (showTrackCont trackCont) +++		    "TermCont:\n\n" ++ (showTermCont termCont) +++		    "Term: " ++ (showTerm term) ++ "\n\n" +++		    (showTerm t1) ++ " == " ++ (showTerm t2) ++ "\n")++-- | getContradiction with prepended type parsing+getItContradiction :: String -> IO()+getItContradiction typstring = getContradiction $ parseType typstring+		+-- | takes the input in Typ format and returns the monad's tracking information, the disrelater entries, the term environment entries, the result term t and the result of the application of the disrelater to the term t. All _not_ in pretty printing+getRawContradiction :: Typ -> IO()+getRawContradiction tau = +    case runM $ alg emptyCont tau emptyTermCont of+    Nothing    -> putStr "No Term.\n"+    Just ((term,termCont,trackCont),debug,funcs) ->+	let (t1',t2') = applyTrackCont term trackCont +	    (t1,t2)   = (simplifyTerm t1', simplifyTerm t2') in+            putStr ("    " ++ (foldr (\x -> \y -> x ++ "\n    " ++ y) "\n" debug) +++		    "TrackCont:\n\n" ++ (showRawTrackCont trackCont) +++		    "TermCont:\n\n" ++ (show termCont) +++		    "Term: " ++ (show term) ++ "\n\n" +++		    (showTerm t1) ++ " == " ++ (showTerm t2) ++ "\n")++-- | getRawContradiction with prepended type parsing+getItRawContradiction :: String -> IO()+getItRawContradiction typstring = getRawContradiction $ parseType typstring++-- | takes the input in Typ format and returns the result term, the disrelater and the application of the disrelater to the result term.+getExample:: Typ -> IO()+getExample tau =+    case runM $ alg emptyCont tau emptyTermCont of+    Nothing    -> putStr "No Term.\n"+    Just ((term,termCont,trackCont),debug,funcs) ->+	let (t1',t2') = applyTrackCont term trackCont +	    (t1,t2)   = (simplifyTerm t1', simplifyTerm t2')+	    t         = Var (TermVar 0)+            (td1,td2) = applyTrackCont t trackCont +            [term',td1',td2'] = renumberVariables [term,simplifyAppOnly td1,simplifyAppOnly td2] in+        putStr ("Term: " ++ (showTerm term') ++ "\n\n" +++--		"Disrelater:\n\n" ++ (showTrackCont trackCont) +++		"The disrelater applied to the term leads to: \n\n" ++ (showTerm td1') ++ " == " ++ (showTerm td2') ++ "\n\n" +++		"which is resolved: " ++ (showTerm t1) ++ " == " ++ (showTerm t2) ++ "\n")++-- | getExample with prepended type parsing+getItExample :: String -> IO()+getItExample typstring = getExample $ parseType typstring++-- | test function for QuickCheck. It returns false, if the disrelater is not working properly, i.e. its application to the result term is not in (p+,_|_) or (_|_,_|_). It does not check for Pointedness, thus it would also accept the wrong result (_|_,_|_) on a pointed type.+testSimple :: Typ -> Bool+testSimple tau =+    case runM $ alg emptyCont tau emptyTermCont of+    Nothing    -> True+    Just ((term,termCont,trackCont),debug,funcs) ->+	let (t1,t2) = getTrackContApplicationSolved trackCont funcs term in+            case t2 of+            Bottom _ -> case t1 of+			Zero     -> True+                        Brace    -> True+		        Bottom _ -> True+                        Fls      -> True+		        Cons _ _ -> True+			Pair _ _ -> True+			Left _   -> True+                        MJust _  -> True+                        _        -> error (showTerm t1) False+            _        -> error (showTerm t1) False++-- | simulation of the web interface output of the counterexample+webInterface typString =+    let typ = parseType typString in+  putStr("The counterexample:\n\n" +++	( case getForWebInterface typ of +		E.Left err -> "No term could be derived: " ++ err+		E.Right result ->+	                let (term,trackCont,funcs) = result+                            names = zip (fst.unzip$funcs) drelNames in+	                ("By disregarding the strictness conditions for the chosen "+++                         "relations, setting all selectable types to () and\n\n" +++                         assignTypeRelFuncs typ funcNames +++                         "\n\nthe following term is a counter example:\n\n" +++                         (termName++" = " ++ (showTerm.head.renumberVariables $ [term]))) +++			 ("\n\nWhereas we confute the theorem by regarding:\n\n" +++                         (prependRelFunc funcNames (fst trackCont) (showTrackContApplicationWithNames trackCont names (Var (TermVar 0)))) ++ "\n\n"++ showFuncNames (zip drelNames (snd.unzip$funcs)))+	)+        )
+ Language/Haskell/FreeTheorems/Variations/CounterExamples/Internal/ExFindExtended.hs view
@@ -0,0 +1,1203 @@+-- * The module contains all rules of ExFind and the algorithm itself (the sequence in which the rules are used).++module Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.ExFindExtended (alg) where++import Language.Haskell.FreeTheorems.Variations.CounterExamples.Common.AlgCommon+import Prelude hiding (Either(..))+import qualified Prelude as E (Either(..))+import Data.List+import qualified Data.Map as Map+import Control.Monad+import Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.M hiding (M)+import qualified Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.M as Mona (M)+import Language.Haskell.FreeTheorems.Variations.CounterExamples.Parser.ParseType+import Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.FTSync+-------Regeln der ersten Phase-------------+-- * The rules of the algorithm+--   The rules have at most three parts:+--   - rule == term construction+--   - rule_tc_update == alternation of the term environments (TermCont)+--   - rule_trackCont_update == alternation of the disrelater (TrackCont)++-- | auxiliary function for tc update+pLusVal_tc_update :: TermCont -> TypedVar -> M TermCont+pLusVal_tc_update tc var =+    let (v,tau) = var in+    do {Just p <- makePlusPair tau;+	return (Map.insert v (p,Leaf) tc)+       }++-- ** first phase+-- *** rules without backtracking++bOttom :: Cont -> Typ -> Maybe Term+bOttom gamma tau = if isElementaryType tau && unpointed (tVars gamma) tau+		 then Just (Bottom tau)+		 else Nothing++-- |initialises the term environments with plus-terms for each term variable in the term variable context+bOttom_tc_update :: Cont -> M TermCont+bOttom_tc_update gamma = initialiseTermCont (vars gamma)++rAllStar :: Cont -> Typ -> Maybe (Cont, Typ, Term -> Term)+rAllStar gamma tau = case tau of+		       AllStar tv tau' -> Just (updateTVarStar gamma tv, tau', \m -> TAbs tv m)+		       _               -> Nothing++rAll :: Cont -> Typ -> Maybe (Cont, Typ, Term -> Term)+rAll gamma tau = case tau of+		   All tv tau' -> Just (updateTVar gamma tv, tau', \m -> TAbs tv m)+		   _           -> Nothing++aBs :: Cont -> Typ -> Maybe (M (Cont, TermVar, Term -> Term), Typ)+aBs gamma tau = case tau of+		   Arrow tau1 tau2 -> Just (do {i <- newInt; +						let x = TermVar i in+						return (updateVar gamma x tau1, x, \m -> Abs x tau1 m)		       +					       }+					   , tau2)+		   _               -> Nothing++aBs_tc_update :: TermCont -> TermVar -> TermCont+aBs_tc_update tc v = Map.delete v tc++aBs_trackCont_update :: TrackCont -> Typ -> TermCont -> TermVar -> M TrackCont+aBs_trackCont_update trackCont tau tc v = +    let (tau,trc) = trackCont+        ((x1,x2),_) = trace "Map.! abs_trackCont_update" (tc Map.! v) in+    do{i <- newAux;+       j <- newAux;+       k <- newAux;+       assoc k x2;+       assoc j x1;+       let u = TermVar i in+       return (tau,(Abs u tau (App (Var u) (Var (TermVar j))), Abs u tau (App (Var u) (Var (TermVar k)))):trc)+      }++wRap :: Typ -> Maybe (Typ, Term -> Term)+wRap tau = case tau of+               List tau' -> Just (tau', \m -> Cons m (Nil tau'))+               _         -> Nothing++wRap_trackCont_update :: TrackCont -> Typ -> M TrackCont+wRap_trackCont_update trackCont tau = +    let (ctau,trc) = trackCont+        List tau' = tau in+    do{f <- listhead tau';+       return (ctau,(f,f):trc)+      }++mAybe :: Typ -> Maybe (Typ, Term -> Term)+mAybe tau = case tau of+               TMaybe tau' -> Just (tau', \m -> MJust m)+               _         -> Nothing++mAybe_trackCont_update :: TrackCont -> Typ -> M TrackCont+mAybe_trackCont_update trackCont tau = +    let (ctau,trc) = trackCont+        TMaybe tau' = tau in+    do{f <- fromJust tau';+       return (ctau,(f,f):trc)+      }++wRapTo :: Cont -> Maybe (M ((Cont, Term -> Term),(TypedVar, TypedVar)))+wRapTo gamma = let f = findfirst typeCheckArrowListArg (vars gamma) in+                    case f of+                      Nothing ->      Nothing+		      Just (v, (Arrow (List tau1) tau2)) -> +                           Just (do {i <- newAux; --g in the new context+			             j <- newInt; --y for substitution+			            let g = TermVar i+				        y = TermVar j in				   +				    return ((updateVar (removeVar gamma v) g (Arrow tau1 tau2),+					    \m -> subst m (Abs y tau1 (App (Var v) (Cons (Var y) (Nil tau1)))) g),+					    ((g,Arrow tau1 tau2), (v, Arrow (List tau1) tau2)))+				    })++wRapTo_tc_update :: TermCont -> TermVar -> TermVar -> TypedVar -> TypedVar -> TermCont+wRapTo_tc_update tc l h g f = +    let Arrow (List t1) t2 = snd f+	((x,y),his) = (trace "Map.!-check: wRapTo g" (tc Map.! (fst g)))+    in+    Map.delete (fst g) (Map.insert (fst f) ((Abs l  (List t1) (LCase (Var l) h (App x (Var h))),Abs l (List t1) (LCase (Var l) h (App y (Var h)))),Branch WrapTo his) tc)++mAybeTo :: Cont -> Maybe (M ((Cont, Term -> Term),(TypedVar, TypedVar)))+mAybeTo gamma = let f = findfirst typeCheckArrowMaybeArg (vars gamma) in+                    case f of+                      Nothing ->      Nothing+		      Just (v, (Arrow (TMaybe tau1) tau2)) -> +                           Just (do {i <- newAux; --g in the new context+			             j <- newInt; --y for substitution+			            let g = TermVar i+				        y = TermVar j in				   +				    return ((updateVar (removeVar gamma v) g (Arrow tau1 tau2),+					    \m -> subst m (Abs y tau1 (App (Var v) (MJust (Var y)))) g),+					    ((g,Arrow tau1 tau2), (v, Arrow (TMaybe tau1) tau2)))+				    })++mAybeTo_tc_update :: TermCont -> TermVar -> TermVar -> TypedVar -> TypedVar -> TermCont+mAybeTo_tc_update tc l h g f = +    let Arrow (TMaybe t1) t2 = snd f+	((x,y),his) = (trace "Map.!-check: wRapTo g" (tc Map.! (fst g)))+    in+    Map.delete (fst g) (Map.insert (fst f) ((Abs l  (TMaybe t1) (MCase (Var l) h (App x (Var h))),Abs l (TMaybe t1) (MCase (Var l) h (App y (Var h)))),Branch MaybeTo his) tc)++hEad :: Cont -> Typ -> Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))+hEad gamma tau' = let l = findfirst typeCheckList (vars gamma) in+		case l of+                  Nothing           -> Nothing+                  Just (v,List tau) -> Just (do {lh <- listheadApp (Var v) tau;+						 i <- newInt; --h+						 let h = TermVar i in+						 return ((updateVar (removeVar gamma v) h tau,+							  \m -> subst m lh h),+							 ((h,tau),(v,List tau)))+						})++hEad_tc_update :: TermCont -> TypedVar -> TypedVar -> TermCont+hEad_tc_update tc h l = let ((x,y),his) = (trace "Map.!-check: hEad h" (tc Map.! (fst h))) in+		      Map.delete (fst h) (Map.insert (fst l) ((Cons x (Nil (snd h)), Cons y (Nil (snd h))),Branch Head his) tc)++jUst :: Cont -> Typ -> Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))+jUst gamma tau' = let l = findfirst typeCheckMaybe (vars gamma) in+		case l of+                  Nothing           -> Nothing+                  Just (v,TMaybe tau) -> Just (do {lh <- fromJustApp (Var v) tau;+						 i <- newInt; --h+						 let h = TermVar i in+						 return ((updateVar (removeVar gamma v) h tau,+							  \m -> subst m lh h),+							 ((h,tau),(v,TMaybe tau)))+						})++jUst_tc_update :: TermCont -> TypedVar -> TypedVar -> TermCont+jUst_tc_update tc h l = let ((x,y),his) = (trace "Map.!-check: jUst h" (tc Map.! (fst h))) in+		      Map.delete (fst h) (Map.insert (fst l) ((MJust x, MJust y),Branch RJust his) tc)++dRop1 :: Cont -> Maybe (Cont,TermVar)+dRop1 gamma = let l = findfirst typeCheckInt (vars gamma) in+	       case l of+		 Nothing  -> Nothing+                 Just var -> Just ((removeVar gamma (fst var)),fst var)++dRop1_tc_update :: TermCont -> TermVar -> TermCont+dRop1_tc_update tc v = Map.insert v ((Zero,Zero),Leaf) tc++dRop2 :: Cont -> Maybe (Cont,TermVar)+dRop2 gamma = let l = findfirst typeCheckBrace (vars gamma) in+	       case l of+		 Nothing  -> Nothing+                 Just var -> Just ((removeVar gamma (fst var)),fst var)++dRop2_tc_update :: TermCont -> TermVar -> TermCont+dRop2_tc_update tc v = Map.insert v ((Brace,Brace),Leaf) tc++dRop4 :: Cont -> Maybe (Cont,TermVar)+dRop4 gamma = let l = findfirst typeCheckBool (vars gamma) in+	       case l of+		 Nothing  -> Nothing+                 Just var -> Just ((removeVar gamma (fst var)),fst var)++dRop4_tc_update :: TermCont -> TermVar -> TermCont+dRop4_tc_update tc v = Map.insert v ((Fls,Fls),Leaf) tc++dRop3 :: Cont -> Maybe (Cont,TypedVar)+dRop3 gamma = let l = findfirstWithTVars unpointed (tVars gamma) (vars gamma) in+                 case l of+		   Nothing    -> Nothing+		   Just var   -> Just ((removeVar gamma (fst var)),var)++dRop3_tc_update :: TermCont -> TypedVar -> M TermCont+dRop3_tc_update = pLusVal_tc_update++pAirTo :: Cont -> Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))+pAirTo gamma = let l = findfirst typeCheckArrowPairArg (vars gamma) in+		    case l of+		      Nothing  -> Nothing+		      Just (f, (Arrow (TPair tau1 tau2) tau3)) -> +			   Just (do {i <- newAux; --g in the new context+				     j <- newInt;+				     k <- newInt;+				     let g = TermVar i +				         x = TermVar j+				         y = TermVar k in+				     return ((updateVar (removeVar gamma f) g (Arrow tau1 (Arrow tau2 tau3)),+					     \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))))+				    })++pAirTo_tc_update :: TermCont -> TypedVar -> TypedVar -> M (TermCont)+pAirTo_tc_update tc g f = do {i <- newInt;+			       j <- newInt;+			       k <- newInt;+			       let p = TermVar i+			           x = TermVar j+				   y = TermVar k +			           Arrow tau tau3 = snd f +			           ((z,z'),his) = (trace "Map.!-check: pAirTo g" (tc Map.! (fst g)))+			       in+			       return (Map.delete (fst g) (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)))),Branch PairTo his) tc))+			      }++pRoj :: Cont -> Maybe (M ((Cont, Term -> Term),([TypedVar],TypedVar)))+pRoj gamma = let l = findfirst typeCheckPair (vars gamma) in+	       case l of+		 Nothing -> Nothing+		 Just (p, TPair tau1 tau2) ->+		      Just (do {i <- newInt;+				j <- newInt;+				let x = TermVar i+				    y = TermVar j in+				do {f <- firstApp (Var p);+				    s <- secondApp (Var p);+				    return ((updateVar (updateVar (removeVar gamma p) x tau1) y tau2,+				             \m -> subst (subst m f x) s y),+					    ([(x,tau1),(y,tau2)],(p,TPair tau1 tau2)))+				   }+			       })++pRoj_tc_update :: TermCont -> [TypedVar] -> TypedVar -> TermCont+pRoj_tc_update tc varIn p = +    let [x,y] = varIn +	((z,z'),his1) = (trace "Map.!-check: pRoj x" (tc Map.! (fst x)))+	((u,u'),his2) = (trace "Map.!-check: pRoj y" (tc Map.! (fst y)))+    in+    Map.delete (fst x) (Map.delete (fst y) (Map.insert (fst p) ((Pair z u, Pair z' u'), Split Proj his1 his2) tc))+++eItherTo :: Cont -> Maybe (M ((Cont, Term -> Term),([TypedVar],TypedVar)))+eItherTo gamma = let l = findfirst typeCheckArrowEitherArg (vars gamma) in+	            case l of+		      Nothing -> Nothing+		      Just (f, (Arrow (TEither tau1 tau2) tau3)) ->+			   Just (do {i <- newAux; --g in the new context+				     j <- newAux; --h in the new context+				     k <- newInt; --x in the term+				     l <- newInt; --y in the term+				     let g = TermVar i+				         h = TermVar j+				         x = TermVar k+				         y = TermVar l in+				     return ((updateVar (updateVar (removeVar gamma f) g (Arrow tau1 tau3)) h (Arrow tau2 tau3),+					     \m -> subst (subst m (Abs x tau1 (App (Var f) (Left (Var x)))) g) (Abs y tau2 (App (Var f) (Right (Var y)))) h),+					     ([(g,Arrow tau1 tau3),(h,Arrow tau2 tau3)],(f,(Arrow (TEither tau1 tau2) tau3))))+				    })++eItherTo_tc_update :: TermCont -> [TypedVar] -> TypedVar -> M (TermCont)+eItherTo_tc_update tc varIn f = let [g,h] = varIn in+                               do{i <- newInt;+				  j <- newInt;+				  k <- newInt;+				  let e = TermVar i +				      x = TermVar j+				      y = TermVar k +				      Arrow tau tau3 = snd f +			              ((z,z'),his1) = (trace "Map.!-check: eItherTo g" (tc Map.! (fst g)))+				      ((u,u'),his2) = (trace "Map.!-check: eItherTo h" (tc Map.! (fst h)))+				  in+	  			  return (Map.delete (fst g) (Map.delete (fst h) (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)))),Split EitherTo his1 his2) tc)))+				 }++-- *** rules with backtracking++dIst1 :: Cont -> Typ -> Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))+dIst1 gamma tau = case findfirst typeCheckEither (vars gamma) of+                    Nothing -> Nothing+                    Just (e, TEither tau1 tau2) ->+		         Just (do {i <- newInt;+				   l <- fromLeftApp (Var e) tau1;+				   let x = TermVar i in+				   return ((updateVar (removeVar gamma e) x tau1,+					   \m -> subst m l x),+					   ((x,tau1),(e, TEither tau1 tau2)))+				  })++dIst1_tc_update :: TermCont -> TypedVar -> TypedVar -> TermCont+dIst1_tc_update tc x e = let ((z,z'),his) = (trace "Map.!-check: dIst1 x" (tc Map.! (fst x)))+		       in+		       Map.delete (fst x) (Map.insert (fst e) ((Left z, Left z'),Branch Dist1 his) tc)++dIst2 :: Cont -> Typ -> Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))+dIst2 gamma tau = case findfirst typeCheckEither (vars gamma) of+                    Nothing -> Nothing+                    Just (e, TEither tau1 tau2) ->+		         Just (do {r <- fromRightApp (Var e) tau2;+				   i <- newInt;+				   let y = TermVar i in+				   return ((updateVar (removeVar gamma e) y tau2,+					   \m -> subst m r y),+					   ((y,tau2),(e,TEither tau1 tau2)))+				  })+dIst2_tc_update :: TermCont -> TypedVar -> TypedVar -> TermCont+dIst2_tc_update tc y e = let ((z,z'),his) = (trace "Map.!-check: dIst2 fst y" (tc Map.! (fst y)))+		       in+		       Map.delete (fst y) (Map.insert (fst e) ((Right z, Right z'),Branch Dist2 his) tc)++pAir1 :: Typ -> Maybe (Typ, Term -> Term)+pAir1 tau = case tau of+            TPair tau1 tau2 -> Just (tau1, \m -> Pair m (Bottom tau2))+	    _               -> Nothing++pAir1_trackCont_update :: TrackCont -> Typ -> M TrackCont+pAir1_trackCont_update trackCont tau =+    let (ctau,trc) = trackCont in+    do{f <- first tau;+       return (ctau,(f,f):trc)+      }++pAir2 :: Typ -> Maybe (Typ, Term -> Term)+pAir2 tau = case tau of+            TPair tau1 tau2 -> Just (tau2,\m -> Pair (Bottom tau1) m)+	    _               -> Nothing++pAir2_trackCont_update :: TrackCont -> Typ -> M TrackCont+pAir2_trackCont_update trackCont tau =+    let (ctau,trc) = trackCont in+    do{f <- second tau;+       return (ctau,(f,f):trc)+      }++lEft :: Typ -> Maybe (Typ, Term -> Term)+lEft tau = case tau of+	    TEither tau1 _ -> Just(tau1, \m -> Left m)+            _              -> Nothing++lEft_trackCont_update :: TrackCont -> Typ -> M TrackCont+lEft_trackCont_update trackCont tau =+    let (ctau,trc) = trackCont+	TEither tau' tau'' = tau in+    do{f <- fromLeft tau' tau'';+       return (ctau,(f,f):trc)+      }+++rIght :: Typ -> Maybe (Typ, Term -> Term)+rIght tau = case tau of+	    TEither _ tau2 -> Just(tau2, \m -> Right m)+            _              -> Nothing++rIght_trackCont_update :: TrackCont -> Typ -> M TrackCont+rIght_trackCont_update trackCont tau =+    let (ctau,trc) = trackCont+        TEither tau' tau'' = tau in+    do{f <- fromRight tau' tau'';+       return (ctau,(f,f):trc)+      }++bOttomToStripe :: Cont -> [M ((Cont, Term -> Term),(TypedVar,TypedVar))]+bOttomToStripe gamma = let l = findallWithTVars typeCheckArrowUnPointedArgPointedRes (tVars gamma) (vars gamma) in+                          map makeone l+		          where makeone = \var -> let Arrow tau1 tau2 = snd var in+					               do {i <- newAux;+							    let x = TermVar i in+							    return (((updateVarStar (removeVar gamma (fst var)) x tau2)+							             , \m -> subst m (App (Var (fst var)) (Bottom tau1)) x),((x,tau2),var))+							  }+bOttomToStripe_tc_update :: TermCont -> Cont -> TypedVar -> TypedVar -> M TermCont+bOttomToStripe_tc_update tc gamma x f = let Arrow t1 t2 = snd f +				            ((u,u'),his) =  trace "Map.! bOttomToStripe_tc_update" (tc Map.! (fst x)) +				        in+                                        do{(g,g') <- makeFuncPair t1 (error "type of disrelater used, which is not set",[]) gamma (u,u');+					   return (Map.delete (fst x) (Map.insert (fst f) ((g,g'),Branch BottomToStripe his) tc))+					  }++aRrowToStar :: Cont -> [M (((Cont, Typ), Cont, Term -> Term -> Term), ([TypedVar],TypedVar))]+aRrowToStar gamma = +    let l = findall typeCheckArrowArgArrow (vars gamma) in+    map makeone l+    where makeone var = let Arrow (Arrow tau1 tau2) tau3 = snd var in+	                do {i <- newInt;+			    j <- newInt;+			    let x = TermVar i +			        y = TermVar j in+			    return ((((updateVar (removeVar gamma (fst var)) x tau1),+				     tau2),+				     updateVarStar (removeVar gamma (fst var)) y tau3,+				     \m1 -> \m2 -> subst m2 (App (Var (fst var)) (Abs x tau1 m1)) y),+				    ([(x,tau1),(y,tau3)],var))+			   }+------------------------              TermContext         M_1     w           y           f           TermContext -----+aRrowToStar_tc_update :: TrackCont -> TermCont -> Cont -> Term -> TypedVar -> TypedVar -> TypedVar -> M TermCont+aRrowToStar_tc_update trackCont tc gamma m1 w y f = +    let (_,trc) = trackCont+        Arrow t12 t3 = snd f +	Arrow t1  t2 = t12+	(resPair,hisy) = (trace "Map.!-check: aRrowToStar g-construct y (else)" (tc Map.! (fst y)))+    in+    do {i <- newInt;+	(g,g') <- makeFuncPair t2 trackCont gamma resPair;+	let u = TermVar i +	    ((z,z'),hisw) = (trace "Map.!-check: aRrowToStar w" (tc Map.! (fst w)))+	in+        return (Map.delete (fst w) (Map.delete (fst y) (Map.insert (fst f) ((Abs u t12 (App g (App (Var u) z)), Abs u t12 (App g' (App (Var u) z'))),Split ArrowToStar hisw hisy) tc)))+       }++bOttomTo :: Cont -> [M ((Cont, Term -> Term),(TypedVar,TypedVar))]+bOttomTo gamma = +    let l = findall typeCheckArrow (vars gamma) in+    map makeone l+    where makeone var = let Arrow tau1 tau2 = snd var in+			do {i <- newAux;+			    let x = TermVar i in+			    return ((updateVar (removeVar gamma (fst var)) x tau2,+			            \m -> subst m (App (Var (fst var)) (Bottom tau1)) x),+				    ((x,tau2),var))+		           }++bOttomTo_tc_update :: TermCont -> TermVar -> TypedVar -> TypedVar -> TermCont+bOttomTo_tc_update tc z x f =+    let Arrow t1 t2 = snd f +        ((u,u'),his) = (trace "Map.!-check: bOttomTo x" (tc Map.! (fst x)))+    in +    Map.delete (fst x) (Map.insert (fst f) ((Abs z t1 u, Abs z t1 u'), Branch BottomTo his) tc)+++-- ** rules of the second phase+-- *** rules without backtracking+vArStar :: Cont -> Typ -> Maybe (Term, (TermVar,Typ))+vArStar gamma tau = if isElementaryType tau +		   then case findfirstSpecialType (varsStar gamma) tau of+                        Nothing -> Nothing+		        Just x  -> Just (Var (fst x), x)+		   else Nothing++-- | creates the initial term variable environment.+vArStar_tc_update :: Cont -> M TermCont+vArStar_tc_update gamma = initialiseTermCont ((vars gamma) ++ (varsStar gamma))++bOttomToStar :: Cont -> Maybe (M ((Cont, Term -> Term),((TermVar,Typ),(TermVar,Typ))))+bOttomToStar gamma = case findfirst typeCheckArrow (varsStar gamma) of+                       Nothing                    -> Nothing+                       Just (f, Arrow tau1 tau2)  -> Just (do {i <- newAux;+							       let y = TermVar i in+							       return ((updateVarStar (removeVarStar gamma f) y tau2, \m -> subst m (App (Var f) (Bottom tau1)) y),((y, tau2),(f, Arrow tau1 tau2) ));+							     })+bOttomToStar_tc_update :: TermCont -> TermVar -> TypedVar -> TypedVar -> TermCont+bOttomToStar_tc_update tc x varIn varOut = case (snd varOut) of+					   Arrow tau1 _ ->+					     let ((z,z'),his) = (trace "Map.!-check: bOttomToStar varIn" (tc Map.!(fst varIn)))+					     in+					     Map.delete (fst varIn) (Map.insert (fst varOut) ((Abs x tau1 z, Abs x tau1 z'),Branch BottomTo his) tc)++aPpStripStar :: Cont -> Maybe (M ((Cont, Term -> Term),([TypedVar],TypedVar)))+aPpStripStar gamma = checkall (findall typeCheckArrow (vars gamma)) +		     where checkall xs =+			       case xs of+				 []  -> Nothing+			         ((f, Arrow tau1 tau2):ys) -> if unpointed (tVars gamma) tau2 +							      then checkall ys+							      else case findfirstSpecialType (varsStar gamma) tau1 of+							             Nothing     -> checkall ys+								     Just (x,_)  -> Just (do {i <- newAux;+											      let y = TermVar i in+											      return ((updateVarStar (removeVar gamma f) y tau2, \m -> subst m (App (Var f) (Var x)) y),([(x,tau1),(y,tau2)],(f,Arrow tau1 tau2)))+											})+-----------------------------------                      x*          y*          f           -------- +aPpStripStar_tc_update :: TermCont -> Cont -> TermVar -> TypedVar -> TypedVar -> TypedVar -> M TermCont+aPpStripStar_tc_update tc gamma z x y f = let  ((v,v'),his) = (trace "Map.!-check: aPpStripStar y (TVar)" (tc Map.! (fst y)))+					  in+				          do{fPair <- makeFuncPair (snd x) (error "unset disrelater type used",[]) gamma (v,v');+					     return  (Map.delete (fst y) (Map.insert (fst f) (fPair,Branch BottomToStripe his) tc))+					    }++hEadStar :: Cont -> Typ ->  Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))+hEadStar gamma tau = case findfirst typeCheckList (varsStar gamma) of+                     Nothing           -> Nothing+		     Just (l,List tau') -> Just (do {i <- newInt;+						     lh <- listheadApp (Var l) tau';+						    let h = TermVar i in+						    return ((updateVarStar (removeVarStar gamma l) h tau',+							     \m -> subst m lh h),+							    ((h, tau'),(l,List tau')))+						    })++hEadStar_tc_update tc h l = let ((u,u'),his) = (trace "Map.!-check: hEadStar fst h" (tc Map.!(fst h)))+			  in+			  Map.delete (fst h) (Map.insert (fst l) ((Cons u (Nil (snd h)), Cons u' (Nil (snd h))),Branch Head his) tc)++jUstStar :: Cont -> Typ ->  Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))+jUstStar gamma tau = case findfirst typeCheckList (varsStar gamma) of+                     Nothing           -> Nothing+		     Just (l,TMaybe tau') -> Just (do {i <- newInt;+						       lh <- fromJustApp (Var l) tau';+						       let h = TermVar i in+						       return ((updateVarStar (removeVarStar gamma l) h tau',+								\m -> subst m lh h),+							       ((h, tau'),(l,TMaybe tau')))+						      })++jUstStar_tc_update tc h l = let ((u,u'),his) = (trace "Map.!-check: jUstStar h" (tc Map.!(fst h)))+			  in+			  Map.delete (fst h) (Map.insert (fst l) ((MJust u, MJust u'),Branch RJust his) tc)++pRojStar :: Cont -> Maybe (M ((Cont, Term -> Term),([TypedVar],TypedVar)))+pRojStar gamma = let l = findfirst typeCheckPair (varsStar gamma) in+	            case l of+		      Nothing -> Nothing+		      Just (p, TPair tau1 tau2) ->+		           Just (do {i <- newInt;+			 	     j <- newInt;+				     k <- newInt;+				     l <- newInt;+				     let x = TermVar i+				         y = TermVar j+				         u = TermVar k+				         v = TermVar l in+				     return ((updateVarStar (updateVarStar (removeVarStar gamma p) x tau1) y tau2,+				             \m -> subst (subst m (PCase (Var p) u v (Var u)) x) (PCase (Var p) u v (Var v)) y),+					     ([(x,tau1),(y,tau2)],(p,TPair tau1 tau2)))+				    })++pRojStar_tc_update :: TermCont -> [TypedVar] -> TypedVar -> TermCont+pRojStar_tc_update tc varIn p = +    let [x,y] = varIn +	((z,z'),his1) = (trace "Map.!-check: pRojStar fst x" (tc Map.! (fst x)))+	((u,u'),his2) = (trace "Map.!-check: pRojStar fst y" (tc Map.! (fst y)))+    in+    Map.delete (fst x) (Map.delete (fst y) (Map.insert (fst p) ((Pair z u, Pair z' u'),Split Proj his1 his2) tc))++iNtStar :: Cont -> Maybe (Cont,Term -> Term, TypedVar)+iNtStar gamma = case findfirstSpecialType (varsStar gamma) Int of+		Nothing -> Nothing+		Just x  -> Just (removeVarStar gamma (fst x), \m -> ICase (Var (fst x)) m, x)++iNtStar_tc_update :: TermCont -> TermVar -> TermCont+iNtStar_tc_update tc var = Map.insert var ((Zero,Zero),Leaf) tc++bRaceStar :: Cont -> Maybe (Cont, Term -> Term, TypedVar)+bRaceStar gamma = case findfirstSpecialType (varsStar gamma) Int of+		  Nothing -> Nothing+		  Just x  -> Just (removeVarStar gamma (fst x), \m -> BCase (Var (fst x)) m, x)++bRaceStar_tc_update :: TermCont -> TermVar -> TermCont+bRaceStar_tc_update tc var = Map.insert var ((Brace,Brace),Leaf) tc++bOolStar :: Cont -> Maybe (Cont, Term -> Term, TypedVar)+bOolStar gamma = case findfirstSpecialType (varsStar gamma) Int of+	         Nothing -> Nothing+		 Just x  -> Just (removeVarStar gamma (fst x), \m -> BoolCase (Var (fst x)) m, x)++bOolStar_tc_update :: TermCont -> TermVar -> TermCont+bOolStar_tc_update tc var = Map.insert var ((Fls,Fls),Leaf) tc++lIstStar :: Cont -> Maybe (M (Cont, Term -> Term, TypedVar))+lIstStar gamma = case findfirst typeCheckList (varsStar gamma) of+	         Nothing -> Nothing+		 Just x  -> Just (do {i <- newInt;+				      let y = TermVar i in+				      return (removeVarStar gamma (fst x), \m -> LCase (Var (fst x)) y m, x)+				     })++lIstStar_tc_update :: TermCont -> TypedVar -> M TermCont+lIstStar_tc_update = pLusVal_tc_update++mAybeStar :: Cont -> Maybe (M (Cont, Term -> Term, TypedVar))+mAybeStar gamma = case findfirst typeCheckMaybe (varsStar gamma) of+	         Nothing -> Nothing+		 Just x  -> Just (do {i <- newInt;+				      let y = TermVar i in+				      return (removeVarStar gamma (fst x), \m -> MCase (Var (fst x)) y m, x)+				     })++mAybeStar_tc_update :: TermCont -> TypedVar -> M TermCont+mAybeStar_tc_update = pLusVal_tc_update++pAirStar :: Cont -> Maybe (M (Cont, Term -> Term, TypedVar))+pAirStar gamma = case findfirst typeCheckPair (varsStar gamma) of+	         Nothing -> Nothing+		 Just x  -> Just (do {i <- newInt;+				      j <- newInt;+				      let y = TermVar i +				          z = TermVar j in+				      return (removeVarStar gamma (fst x), \m -> PCase (Var (fst x)) y z m, x)+				     })++pAirStar_tc_update :: TermCont -> TypedVar -> M TermCont+pAirStar_tc_update = pLusVal_tc_update++eItherStar :: Cont -> Typ -> Maybe (M (Cont, Term -> Term, TypedVar))+eItherStar gamma tau = case findfirst typeCheckEither (varsStar gamma) of+	         Nothing -> Nothing+		 Just x  -> Just (do {i <- newInt;+				      j <- newInt;+				      let y = TermVar i +				          z = TermVar j in+				      return (removeVarStar gamma (fst x), \m -> ECase (Var (fst x)) y m z (Bottom tau), x)+				     })++eItherStar_tc_update :: TermCont -> TypedVar -> M TermCont+eItherStar_tc_update = pLusVal_tc_update++-- *** rules with backtracking++dIstStar1 :: Cont -> Typ -> Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))+dIstStar1 gamma tau = case findfirst typeCheckEither (varsStar gamma) of+                    Nothing -> Nothing+                    Just (e, TEither tau1 tau2) ->+		         Just (do {i <- newInt;+			   	   j <- newInt;+				   let x = TermVar i+			               y = TermVar j in+				   return ((updateVarStar (removeVarStar gamma e) x tau1,+					   \m -> subst m (ECase (Var e) x (Var x) y (Bottom tau1)) x),+					   ((x,tau1),(e,TEither tau1 tau2)))+				  })++dIstStar1_tc_update :: TermCont -> TypedVar -> TypedVar -> TermCont+dIstStar1_tc_update tc x e = let ((z,z'),his) = (trace "Map.!-check: dIstStar1 x" (tc Map.! (fst x)))+			   in+			   Map.delete (fst x) (Map.insert (fst e) ((Left z, Left z'),Branch Dist1 his) tc)++dIstStar2 :: Cont -> Typ -> Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))+dIstStar2 gamma tau = case findfirst typeCheckEither (varsStar gamma) of+                    Nothing -> Nothing+                    Just (e, TEither tau1 tau2) ->+		         Just (do {i <- newInt;+			   	   j <- newInt;+				   let x = TermVar i+			               y = TermVar j in+				   return ((updateVarStar (removeVarStar gamma e) y tau2,+					   \m -> subst m (ECase (Var e) x (Bottom tau1) y (Var y)) y),+					   ((y,tau2),(e,TEither tau1 tau2)))+				  })++dIstStar2_tc_update :: TermCont -> TypedVar -> TypedVar -> TermCont+dIstStar2_tc_update tc y e = let ((z,z'),his) = (trace "Map.!-check: dIstStar2 y" (tc Map.! (fst y)))+                           in+			   Map.delete (fst y) (Map.insert (fst e) ((Right z, Right z'),Branch Dist2 his) tc)++-- ** last phase for plus term search++vArStripe :: Cont -> Typ -> Maybe (Term, TypedVar)+vArStripe gamma tau = case findfirstSpecialType (vars gamma) tau of+                     Nothing -> Nothing+		     Just x  -> Just (Var (fst x), x)++iNtStripe :: Typ -> Maybe Term+iNtStripe tau = if tau == Int then Just Zero else Nothing+                     +bRaceStripe :: Typ -> Maybe Term+bRaceStripe tau = if tau == TBrace then Just Brace else Nothing++bOolStripe :: Typ -> Maybe Term+bOolStripe tau = if tau == TBool then Just Fls else Nothing++lIstStripe :: Typ -> Maybe Term+lIstStripe tau = if typeCheckList tau then let List tau' = tau in Just (Cons (Bottom tau') (Nil tau')) else Nothing++mAybeStripe :: Typ -> Maybe Term+mAybeStripe tau = if typeCheckMaybe tau then let TMaybe tau' = tau in Just (MJust (Bottom tau')) else Nothing++pAirStripe :: Typ -> Maybe Term+pAirStripe tau = if typeCheckPair tau then let TPair tau1 tau2 = tau in Just (Pair (Bottom tau1) (Bottom tau2)) else Nothing++eItherStripe :: Typ -> Maybe Term+eItherStripe tau = if typeCheckEither tau then let TEither tau1 tau2  = tau in Just (Left (Bottom tau1)) else Nothing++-- | creates the initial term variable environment.+stripePhase_tc_update :: Cont -> M TermCont+stripePhase_tc_update gamma = initialiseTermCont ((vars gamma) ++ (varsStar gamma))++++-- * The algorithm+--Note: pointed checks are omitted whenever possible, because pointedness is clear out of the rules order, especially because (Drop_3) is used very early++-- ** first phase++alg :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)+alg gamma tau termCont = do track (makeTrackString "Start Conf" gamma tau)+			    (t,tc,trc) <- alg1 gamma tau termCont+--			    return (simplifyTerm t, simplifyTermCont tc, simplifyTrackCont trc) --returns simplified terms+			    return (t, tc, trc)                                --returns the terms without simplification++alg1 :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)+alg1 = traceIOStart traceIOFile alg1_Bottom++alg1_Bottom :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)+alg1_Bottom gamma tau termCont = case bOttom gamma tau of+		               Nothing -> alg1_RAllStar gamma tau termCont+			       Just t  -> do track ((makeTrackString "Bottom" gamma tau) ++ "  !!END OF BRANCH!!")+                                             tc <- bOttom_tc_update gamma+				             return (t,tc,(tau,[]))+				      +alg1_RAllStar :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)+alg1_RAllStar gamma tau termCont = case rAllStar gamma tau of+			           Nothing                -> alg1_RAll gamma tau termCont+			           Just (gamma', tau', f) -> do track (makeTrackString "RAllStar" gamma' tau')+								(t,c,trc) <- (alg1 gamma' tau' termCont)+					              	        traceIO "RAll*" tau gamma tau' gamma' (return (f t, c, trc))+							      +alg1_RAll :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)+alg1_RAll gamma tau termCont = case rAll gamma tau of+		               Nothing                -> alg1_Drop3 gamma tau termCont+			       Just (gamma', tau', f) -> do {track (makeTrackString "RAll" gamma' tau');+							     (t,c, trc) <- (alg1 gamma' tau' termCont);+							     traceIO "RAll" tau gamma tau' gamma' (return (f t,c,trc))+							    }+		+alg1_Drop3 :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)				     +alg1_Drop3 gamma tau termCont = case dRop3 gamma of+                               Nothing         -> alg1_Drop1 gamma tau termCont+                               Just (gamma',v) -> do{track (makeTrackString "Drop_3" gamma' tau);+					             (t,c,trc) <- (traceIO "Drop_3" tau gamma tau gamma' (alg1 gamma' tau termCont));+                                                     tc <- dRop3_tc_update c v;+						     return (t,tc,trc)+						    }++alg1_Drop1 gamma tau termCont = case dRop1 gamma of+		               Nothing         -> alg1_Drop2 gamma tau termCont+			       Just (gamma',v) -> do{track (makeTrackString "Drop_1" gamma' tau);+				                     (t,c,trc) <- (traceIO "Drop_1" tau gamma tau gamma' (alg1 gamma' tau termCont));+						     return (t,dRop1_tc_update c v,trc)+						    }++alg1_Drop2 gamma tau termCont = case dRop2 gamma of+		               Nothing         -> alg1_Drop4 gamma tau termCont+			       Just (gamma',v) -> do{track (makeTrackString "Drop_2" gamma' tau);+				                     (t,c,trc) <- (traceIO "Drop_2" tau gamma tau gamma' (alg1 gamma' tau termCont));+						     return (t,dRop2_tc_update c v,trc)+						    }++alg1_Drop4 gamma tau termCont = case dRop4 gamma of+		               Nothing         -> alg1_Abs gamma tau termCont+			       Just (gamma',v) -> do{track (makeTrackString "Drop_4" gamma' tau);+				                     (t,c,trc) <- (traceIO "Drop_4" tau gamma tau gamma' (alg1 gamma' tau termCont));+						     return (t,dRop4_tc_update c v,trc)+						    }++alg1_Abs :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)+alg1_Abs gamma tau termCont = case aBs gamma tau of +			         Nothing           -> alg1_WrapTo gamma tau termCont+			         Just (comp, tau') -> do {(gamma', x, f) <- comp;+							  track (makeTrackString "Abs" gamma' tau');					+							  (t,c,trc) <- (traceIO "Abs" tau gamma tau' gamma' (alg1 gamma' tau' termCont));+							  trc' <- aBs_trackCont_update trc tau c x;+							  return (f t,aBs_tc_update c x,trc')+							 }+				           +alg1_WrapTo :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)+alg1_WrapTo gamma tau termCont = case wRapTo gamma of+                                  Nothing   -> alg1_MaybeTo gamma tau termCont+			          Just comp -> do {((gamma',f),(g,k)) <- comp;+						   track (makeTrackString "Wrap->" gamma' tau);+                                                   (t,c, trc) <- traceIO "Wrap->" tau gamma tau gamma' (alg1 gamma' tau termCont);+						   i <- newInt;+						   j <- newInt;+						   let l = TermVar i+						       h = TermVar j in+						   return (f t,wRapTo_tc_update c l h g k, trc)+						  }++alg1_MaybeTo :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)+alg1_MaybeTo gamma tau termCont = case mAybeTo gamma of+                                  Nothing   -> alg1_Head gamma tau termCont+			          Just comp -> do {((gamma',f),(g,k)) <- comp;+						   track (makeTrackString "Maybe->" gamma' tau);+                                                   (t,c, trc) <- traceIO "Maybe->" tau gamma tau gamma' (alg1 gamma' tau termCont);+						   i <- newInt;+						   j <- newInt;+						   let l = TermVar i+						       h = TermVar j in+						   return (f t,mAybeTo_tc_update c l h g k, trc)+						  }++alg1_Head :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)+alg1_Head gamma tau termCont = case hEad gamma tau of+                             Nothing     -> alg1_Just gamma tau termCont+                             Just comp -> do {((gamma',f),(h,l)) <- comp;+					      track (makeTrackString "Head" gamma' tau);+					      (t,c,trc) <- traceIO "Head" tau gamma tau gamma' (alg1 gamma' tau termCont);+					      return (f t, hEad_tc_update c h l, trc)+					     }++alg1_Just :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)+alg1_Just gamma tau termCont = case jUst gamma tau of+                             Nothing     -> alg1_PairTo gamma tau termCont+                             Just comp -> do {((gamma',f),(h,l)) <- comp;+					      track (makeTrackString "Just" gamma' tau);+					      (t,c,trc) <- traceIO "Just" tau gamma tau gamma' (alg1 gamma' tau termCont);+					      return (f t, jUst_tc_update c h l, trc)+					     }++alg1_PairTo gamma tau termCont = case pAirTo gamma of+			          Nothing    -> alg1_Proj gamma tau termCont+                                  Just comp  -> do {((gamma',f),(g,h)) <- comp;+						    track(makeTrackString "Pair->" gamma' tau);+						    (t,c,trc) <- traceIO "Pair->" tau gamma tau gamma' (alg1 gamma' tau termCont);+						    termCont' <- pAirTo_tc_update c g h;+						    return (f t, termCont',trc)+						   }++alg1_Proj gamma tau termCont = case pRoj gamma of+		             Nothing    -> alg1_EitherTo gamma tau termCont+                             Just comp  -> do {((gamma',f),(varIn,p)) <- comp;+					       track(makeTrackString "Proj" gamma' tau);+					       (t,c,trc) <- traceIO "Proj" tau gamma tau gamma' (alg1 gamma' tau termCont);+					       return (f t, pRoj_tc_update c varIn p,trc)+					      }++alg1_EitherTo gamma tau termCont = case eItherTo gamma of+                                  Nothing   -> alg1_Dist1 gamma tau termCont+                                  Just comp -> do {((gamma',f),(varIn,g)) <- comp;+						   track (makeTrackString "LE->" gamma' tau);+						   (t,c,trc) <- traceIO "LE->" tau gamma tau gamma' (alg1 gamma' tau termCont);+						   termCont' <- eItherTo_tc_update c varIn g;+						   return (f t, termCont',trc)+						  }++alg1_Dist1 gamma tau termCont = case dIst1 gamma tau of+			      Nothing   -> alg1_BottomToStripe gamma tau termCont+			      Just comp -> do {((gamma',f),(x,e)) <- comp;+					   let subderivation =+					           do  track (makeTrackString "Dist1" gamma' tau)+					               (t,c,trc) <- traceIO "Dist1" tau gamma tau gamma' (alg1 gamma' tau termCont);+					               return (f t, dIst1_tc_update c x e,trc)+					   in+					   choice subderivation (alg1_Dist2 gamma tau termCont);+					  }++alg1_Dist2 gamma tau termCont = case dIst2 gamma tau of+			      Nothing   -> alg1_BottomToStripe gamma tau termCont --should never be reached+			      Just comp -> do {((gamma',f),(y,e)) <- comp;+					       track (makeTrackString "Dist2" gamma' tau);+					       (t,c,trc) <- traceIO "Dist2" tau gamma tau gamma' (alg1 gamma' tau termCont);+					       return (f t, dIst2_tc_update c y e,trc)+					      }++					+alg1_BottomToStripe :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)+alg1_BottomToStripe gamma tau termCont = foldr choice (alg1_ArrowToStar gamma tau termCont) (map trysubderivations (bOttomToStripe gamma))+			              where trysubderivations = \l -> do {((gamma', f),(x,g)) <- l; +									  track (makeTrackString "Bottom->'" gamma' tau);+									  (t,c,trc) <- traceIO "Bottom->'" tau gamma tau gamma' (alg2 gamma' tau termCont);+									  tc <- bOttomToStripe_tc_update c gamma x g;+								          return (f t, tc, trc)+									 }++alg1_ArrowToStar :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)+alg1_ArrowToStar gamma tau termCont = +     foldr choice (alg1_Wrap gamma tau termCont) (map trysubderivations (aRrowToStar gamma))+     where trysubderivations = \l -> do {(((gamma1, tau1), gamma2, f),([w,y],g)) <- l;+					 track (makeTrackString "Arrow->* (fst)" gamma1 tau1);+					 track (makeTrackString "Arrow->* (snd)" gamma2 tau);+					 (t1,c1,trc1) <- traceIO "Arrow->* (fst)" tau gamma tau1 gamma1 (alg1 gamma1 tau1 termCont);+					 (t2,c2,trc2) <- traceIO "Arrow->* (snd)" tau gamma tau gamma2 (alg2 gamma2 tau termCont);+					 let cont = mergeTermCont c1 c2 in+					 (case cont of+                                           Nothing -> abort+                                           Just c  -> do {tc <- aRrowToStar_tc_update trc1 c gamma t1 w y g;+							  return (f t1 t2,tc,trc2)+							 }+					 )+					}++alg1_Wrap :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)+alg1_Wrap gamma tau termCont = case wRap tau of+                               Nothing        -> alg1_Maybe gamma tau termCont+                               Just (tau', f) -> do track (makeTrackString "Wrap" gamma tau')						  +				  		    (t,c,trc) <- traceIO "Wrap" tau gamma tau' gamma (alg1 gamma tau' termCont)+                                                    trc' <- wRap_trackCont_update trc tau+					            return (f t,c,trc')++alg1_Maybe :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)+alg1_Maybe gamma tau termCont = case mAybe tau of+                                Nothing        -> alg1_Pair1 gamma tau termCont+                                Just (tau', f) -> do track (makeTrackString "Maybe" gamma tau')+                                                     (t,c,trc) <- traceIO "Maybe" tau gamma tau' gamma (alg1 gamma tau' termCont)+                                                     trc' <- mAybe_trackCont_update trc tau+					             return (f t,c,trc')++alg1_Pair1 gamma tau termCont = case pAir1 tau of+                              Nothing        -> alg1_Left gamma tau termCont+                              Just (tau', f) -> choice subderivation (alg1_Pair2 gamma tau termCont)+	                                         where subderivation = do {track (makeTrackString "Pair1" gamma tau');+									   (t,c,trc) <- traceIO "Pair1" tau gamma tau' gamma (alg1 gamma tau' termCont);+									   trc' <-pAir1_trackCont_update trc tau;+							                   return (f t, c, trc')+									  }+  +alg1_Pair2 gamma tau termCont = case pAir2 tau of+		              Nothing        -> alg1_Left gamma tau termCont+                              Just (tau', f) -> do {track (makeTrackString "Pair2" gamma tau');+						    (t,c,trc) <- traceIO "Pair2" tau gamma tau' gamma (alg1 gamma tau' termCont);+						    trc' <- pAir2_trackCont_update trc tau;+					            return (f t,c,trc')+						   }++alg1_Left gamma tau termCont = case lEft tau of+                              Nothing        -> alg1_BottomTo gamma tau termCont+                              Just (tau', f) -> choice subderivation (alg1_Right gamma tau termCont)+			                        where subderivation = do {track (makeTrackString "Left" gamma tau');+									  (t,c,trc) <- traceIO "Left" tau gamma tau' gamma (alg1 gamma tau' termCont);+									  trc' <- lEft_trackCont_update trc tau;+							                  return (f t,c, trc')+									 }+									  +alg1_Right gamma tau termCont = case rIght tau of+		              Nothing        -> alg1_BottomTo gamma tau termCont+                              Just (tau', f) -> do {track (makeTrackString "Right" gamma tau');+						    (t,c,trc) <- traceIO "Right" tau gamma tau' gamma (alg1 gamma tau' termCont);+						    trc' <- rIght_trackCont_update trc tau;+					            return (f t,c,trc')+						   }++alg1_BottomTo :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)+alg1_BottomTo gamma tau termCont = +     foldr choice (do {track "Bottom->:  !!FAIL!!"; abort}) (map trysubderivations (bOttomTo gamma))+     where trysubderivations = \l -> do {((gamma', f),(x,g)) <- l;+					 track (makeTrackString "Bottom->" gamma' tau);+					 (t,c,trc) <- traceIO "Bottom->" tau gamma tau gamma' (alg1 gamma' tau termCont);+					 i <- newInt;+					 let z = TermVar i in+					 return (f t,bOttomTo_tc_update c z x g,trc)+					}++-- ** second phase++alg2 :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)+alg2 = alg2_VarStar++alg2_VarStar :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)+alg2_VarStar gamma tau termCont = case vArStar gamma tau of+                                 Nothing     -> alg2_BottomToStar gamma tau termCont+                                 Just (t,v)  -> do track ((makeTrackString "Var*" gamma tau) ++ "  !!END OF BRANCH!!")+                                                   tc <- vArStar_tc_update gamma+                                                   return (t, tc, (tau,[]))++alg2_BottomToStar :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)+alg2_BottomToStar gamma tau termCont = case bOttomToStar gamma of+				       Nothing -> alg2_AppStripStar gamma tau termCont+				       Just (comp) +					       -> do {((gamma', f),(varIn,varOut)) <- comp;+						      track (makeTrackString "Bottom->*" gamma' tau);+						      (t,c,trc) <- traceIO "Bottom->*" tau gamma tau gamma' (alg2 gamma' tau termCont);+						      i <- newInt;+						      let x = TermVar i in+						      return (f t, bOttomToStar_tc_update c x varIn varOut, trc)+						     }++alg2_AppStripStar :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)+alg2_AppStripStar gamma tau termCont = case aPpStripStar gamma of+				       Nothing   -> alg2_IntStar gamma tau termCont+				       Just comp -> do {((gamma', f),([x,y],g)) <- comp;+							track (makeTrackString "App'*" gamma' tau);+							(t,c,trc) <- traceIO "App'*" tau gamma tau gamma' (alg2 gamma' tau termCont);+							i <- newInt;+							let u = TermVar i in+							do{tc <- aPpStripStar_tc_update c gamma u x y g;+							   return (f t, tc,trc)+							  }+						       }++alg2_IntStar gamma tau termCont = +    case iNtStar gamma of+    Nothing           -> alg2_BraceStar gamma tau termCont+    Just (gamma',f,v) -> do {let subderivation =+			            do {track (makeTrackString "Int*" gamma' tau);+					(t,c,trc) <- traceIO "Int*" tau gamma tau gamma' (alg3 gamma' tau termCont);+					return (f t, iNtStar_tc_update c (fst v), trc)+				       }+			     in+			     choice subderivation (alg2_HeadStar gamma tau termCont)+			    }++alg2_BraceStar gamma tau termCont = +    case bRaceStar gamma of+    Nothing           -> alg2_BoolStar gamma tau termCont+    Just (gamma',f,v) -> do {let subderivation =+			            do {track (makeTrackString "Brace*" gamma' tau);+					(t,c,trc) <- traceIO "Brace*" tau gamma tau gamma' (alg3 gamma' tau termCont);+					return (f t, bRaceStar_tc_update c (fst v), trc)+				       }+			     in+			     choice subderivation (alg2_HeadStar gamma tau termCont)+			    }+++alg2_BoolStar gamma tau termCont = +    case bOolStar gamma of+    Nothing           -> alg2_ListStar gamma tau termCont+    Just (gamma',f,v) -> do {let subderivation =+			            do {track (makeTrackString "Bool*" gamma' tau);+					(t,c,trc) <- traceIO "Bool*" tau gamma tau gamma' (alg3 gamma' tau termCont);+					return (f t, bOolStar_tc_update c (fst v), trc)+				       }+			     in+			     choice subderivation (alg2_HeadStar gamma tau termCont)+			    }++alg2_ListStar gamma tau termCont = case lIstStar gamma of+			        Nothing -> alg2_MaybeStar gamma tau termCont+                                Just comp -> do {(gamma',f,v) <- comp;+						 let subderivation =+						        do {track (makeTrackString "List*" gamma' tau);+							    (t,c,trc) <- traceIO "List*" tau gamma tau gamma' (alg3 gamma' tau termCont);+							    cont <- lIstStar_tc_update c v;+							    return (f t, cont, trc)+							   }+						 in+						 choice subderivation (alg2_HeadStar gamma tau termCont)+					}++alg2_MaybeStar gamma tau termCont = case mAybeStar gamma of+			        Nothing -> alg2_PairStar gamma tau termCont+                                Just comp -> do {(gamma',f,v) <- comp;+						 let subderivation =+						        do {track (makeTrackString "Maybe*" gamma' tau);+							    (t,c,trc) <- traceIO "Maybe*" tau gamma tau gamma' (alg3 gamma' tau termCont);+							    cont <- mAybeStar_tc_update c v;+							    return (f t, cont, trc)+							   }+						 in+						 choice subderivation (alg2_JustStar gamma tau termCont)+					}+++alg2_PairStar gamma tau termCont = case pAirStar gamma of+			        Nothing -> alg2_EitherStar gamma tau termCont+                                Just comp -> do {(gamma',f,v) <- comp;+						 let subderivation =+						        do {track (makeTrackString "Pair*" gamma' tau);+							    (t,c,trc) <- traceIO "Pair*" tau gamma tau gamma' (alg3 gamma' tau termCont);+							    cont <- pAirStar_tc_update c v;+							    return (f t, cont, trc)+							   }+						 in+						 choice subderivation (alg2_ProjStar gamma tau termCont)+					}++alg2_EitherStar gamma tau termCont = case eItherStar gamma tau of+			        Nothing -> do {track "abort: Either*";+					       abort+					      }+                                Just comp -> do {(gamma',f,v) <- comp;+						 let subderivation =+						        do {track (makeTrackString "Either*" gamma' tau);+							    (t,c,trc) <- traceIO "Either*" tau gamma tau gamma' (alg3 gamma' tau termCont);+							    cont <- eItherStar_tc_update c v;+							    return (f t, cont, trc)+							   }+						 in+						 choice subderivation (alg2_DistStar1 gamma tau termCont)+					}++alg2_HeadStar :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)+alg2_HeadStar gamma tau termCont = case hEadStar gamma tau of+                                 Nothing   -> alg2_JustStar gamma tau termCont+			         Just comp -> do {((gamma', f),(h,l)) <- comp;+						  track (makeTrackString "Head*" gamma' tau);+						  (t,c,trc) <- traceIO "Head*" tau gamma tau gamma' (alg2 gamma' tau termCont);+						  return (f t, hEadStar_tc_update c h l, trc)+						 }++alg2_JustStar :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)+alg2_JustStar gamma tau termCont = case jUstStar gamma tau of+                                 Nothing   -> alg2_ProjStar gamma tau termCont+			         Just comp -> do {((gamma', f),(h,l)) <- comp;+						  track (makeTrackString "Just*" gamma' tau);+						  (t,c,trc) <- traceIO "Just*" tau gamma tau gamma' (alg2 gamma' tau termCont);+						  return (f t, jUstStar_tc_update c h l, trc)+						 }++alg2_ProjStar gamma tau termCont = case pRojStar gamma of+			          Nothing   -> alg2_DistStar1 gamma tau termCont+			          Just comp -> do {((gamma', f),(h,p)) <- comp;+						   track (makeTrackString "Proj*" gamma' tau);+						   (t,c,trc) <- traceIO "Proj*" tau gamma tau gamma' (alg2 gamma' tau termCont);+						   return (f t, pRojStar_tc_update c h p, trc)+						  }+++alg2_DistStar1 gamma tau termCont = case dIstStar1 gamma tau of+			         Nothing   -> do {track "abort: Dist*1"; --should never be reached+						  abort+						 }+			         Just comp -> do {((gamma',f),(x,e)) <- comp;+						  let subderivation =+					                 do {track (makeTrackString "Dist*1" gamma' tau);+					                     (t,c,trc) <- traceIO "Dist*1" tau gamma tau gamma' (alg2 gamma' tau termCont);+							     return (f t, dIstStar1_tc_update c x e, trc)+							    }+						  in+						  choice subderivation (alg2_DistStar2 gamma tau termCont)+						 }++alg2_DistStar2 gamma tau termCont  = case dIstStar2 gamma tau of+			          Nothing   -> do {track "abort: Dist*2"; --should never be reached+						   abort+						  }+			          Just comp -> do {((gamma',f),(y,e)) <- comp;+						   track (makeTrackString "Dist*2" gamma' tau);+						   (t,c,trc) <- traceIO "Dist*2" tau gamma tau gamma' (alg2 gamma' tau termCont);+						   return (f t, dIstStar2_tc_update c y e, trc)+						  }++-- ** third phase++alg3 = alg3_VarStripe++alg3_VarStripe gamma tau termCont = +    case vArStripe gamma tau of+    Nothing      -> alg3_IntStripe gamma tau termCont+    Just (t,var) -> do {track ((makeTrackString "Var'" gamma tau) ++ "  !!END OF BRANCH!!");+			tc <- stripePhase_tc_update gamma;+                        return (t, tc, (tau,[]))+		       }++alg3_IntStripe gamma tau termCont = +    case iNtStripe tau of+    Nothing  -> alg3_BraceStripe gamma tau termCont+    Just t   -> do {track ((makeTrackString "Int'" gamma tau) ++ "  !!END OF BRANCH!!");+		    tc <- stripePhase_tc_update gamma;+                    return (t, tc, (tau,[]))+		   }++alg3_BraceStripe gamma tau termCont = +    case bRaceStripe tau of+    Nothing -> alg3_BoolStripe gamma tau termCont+    Just t  -> do {track ((makeTrackString "Brace'" gamma tau) ++ "  !!END OF BRANCH!!");+		   tc <- stripePhase_tc_update gamma;+                   return (t, tc, (tau,[]))+		  }++alg3_BoolStripe gamma tau termCont = +    case bOolStripe tau of+    Nothing -> alg3_ListStripe gamma tau termCont+    Just t  -> do {track ((makeTrackString "Bool'" gamma tau) ++ "  !!END OF BRANCH!!");+		   tc <- stripePhase_tc_update gamma;+                   return (t, tc, (tau,[]))+		  }++alg3_ListStripe gamma tau termCont = +    case lIstStripe tau of+    Nothing -> alg3_MaybeStripe gamma tau termCont+    Just t  -> do {track ((makeTrackString "List'" gamma tau) ++ "  !!END OF BRANCH!!");+		   tc <- stripePhase_tc_update gamma;+                   return (t, tc, (tau,[]))+		  }++alg3_MaybeStripe gamma tau termCont = +    case mAybeStripe tau of+    Nothing -> alg3_PairStripe gamma tau termCont+    Just t  -> do {track ((makeTrackString "Maybe'" gamma tau) ++ "  !!END OF BRANCH!!");+		   tc <- stripePhase_tc_update gamma;+                   return (t, tc, (tau,[]))+		  }++alg3_PairStripe gamma tau termCont = +    case pAirStripe tau of+    Nothing -> alg3_EitherStripe gamma tau termCont+    Just t  -> do {track ((makeTrackString "Pair'" gamma tau) ++ "  !!END OF BRANCH!!");+		   tc <- stripePhase_tc_update gamma;+                   return (t, tc, (tau,[]))+		  }++alg3_EitherStripe gamma tau termCont = +    case lIstStripe tau of+    Nothing -> do {track "Either': FAIL";+		   abort+		  }+    Just t  -> do {track ((makeTrackString "Either'" gamma tau) ++ "  !!END OF BRANCH!!");+		   tc <- stripePhase_tc_update gamma;+                   return (t, tc, (tau,[]))+		  }
+ Language/Haskell/FreeTheorems/Variations/CounterExamples/Internal/FTSync.hs view
@@ -0,0 +1,25 @@+-- | functions to provide the same choice of function and variable names+--   as free-theorems does. The functions for name generation are provided+--   by Language.Haskell.FreeTheorems.NameStores. They are accessalbe only+--   from versions >=0.31 of the free-theorems package.+--   Additionally the letter for the term generated by ExFind is set here.++module Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.FTSync (funcNames,drelNames,varNames,termName) where++import Language.Haskell.FreeTheorems.NameStores++-- | name of the term ExFind produces+termName = "f"++-- | function names for type relations+--   termName is filtered because it is used for the output term.+funcNames = filter (/= termName) functionNameStore1++-- | function names for functions in the disrelater+--   termName is filtered because it is used for the output term.+drelNames = filter (/= termName) functionNameStore2++-- | variable names for variables in the disrelater+--   termName is filtered because it is used for the output term.+varNames  = filter (/= termName) variableNameStore+
+ Language/Haskell/FreeTheorems/Variations/CounterExamples/Internal/M.hs view
@@ -0,0 +1,35 @@+module Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.M (M,runM,newInt,newAux,choice,abort,runMAll,track,assoc) where++type State s = (Int,Int,[String],[(Int,s)])++data M s a = M (State s -> [(a,State s)])++instance Monad (M s) where+    return a = M (\s -> [(a,s)])+    M m >>= k = M (\s -> concatMap (\(a,s') -> case k a of M l -> l s') (m s))++runM :: M s a -> Maybe (a, [String], [(Int,s)])+runM (M m) = case m (1,-1,[],[]) of+	       []        -> Nothing+	       ((a,(_,_,ls,as)):_) -> Just (a,reverse ls,as)++runMAll :: M s a -> [(a, [String], [(Int,s)])]+runMAll (M m) = map (\(a,(_,_,ls,as)) -> (a,reverse ls,as)) (m (1,0,[],[]))++newInt :: M s Int+newInt = M (\(i,j,ls,as) -> [(i,(i+1,j,ls,as))])++newAux :: M s Int+newAux = M (\(i,j,ls,as) -> [(j,(i,j-1,ls,as))])++choice :: M s a -> M s a -> M s a+choice (M m) (M l) = M (\s -> m s ++ l s)++abort :: M s a+abort = M (\s -> [])++track :: String -> M s ()+track l = M (\(i,j,ls,as) -> [((),(i,j,l:ls,as))])++assoc :: Int -> s -> M s ()+assoc a s = M (\(i,j,ls,as) -> [((),(i,j,ls,(a,s):as))])
+ Language/Haskell/FreeTheorems/Variations/CounterExamples/Internal/TimeOut.hs view
@@ -0,0 +1,35 @@+module Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.TimeOut where++import Control.Concurrent+--import Distribution.Simple.Utils+watchdogIO :: (Show a) =>+                Int  -- milliseconds+             -> IO a   -- expensive computation+             -> IO a   -- cheap computation+             -> IO a+watchdogIO millis expensive cheap = +    do mvar <- newEmptyMVar+       tid1 <- forkIO $ do x <- expensive+	                   (if (length (show x) >= 0) then x else x) `seq` putMVar mvar (Just x)+       tid2 <- forkIO $ do threadDelay (millis * 1000)+                           putMVar mvar Nothing+       res <- takeMVar mvar+       case res of+           Just x -> +               do --info ("EXPENSIVE was used")+                  killThread tid2 --`catch` (\e -> warn (show e))+                  return x+           Nothing ->+               do --info ("WATCHDOG after " ++ show millis ++ " milliseconds")+                  killThread tid1 --`catch` (\e -> warn (show e))+                  cheap++watchdog1 :: (Show a) => Int -> a -> IO (Maybe a)+watchdog1 millis x =+    watchdogIO millis (return (Just x))+                      (return Nothing)++watchdog2 :: (Show a) => Int -> a -> IO (Maybe a)+watchdog2 millis x =+    watchdogIO millis (x `seq` return (Just x))+                      (return Nothing)
+ Language/Haskell/FreeTheorems/Variations/CounterExamples/Parser/ParseType.hs view
@@ -0,0 +1,113 @@+{-# LANGUAGE ScopedTypeVariables,  FlexibleContexts, DeriveDataTypeable #-}+module Language.Haskell.FreeTheorems.Variations.CounterExamples.Parser.ParseType (+	  parseType+	, parseType'+	, instType+	, unquantify+	, TypVar(..)+	, Typ(..)+	) where++import Language.Haskell.Parser (parseModule, ParseResult(..))+import Language.Haskell.Syntax++import Control.Monad.Error+import Control.Monad.Reader+import Data.List+import qualified Data.Map as M++import Data.Generics+--import Data.Generics.Schemes+import Data.Char+import Data.Maybe++data TypVar = TypVar Int        -- alpha, beta etc.+            | TypInst Int Bool  -- t1,t2 etc+	    | TUnit             -- ()+	deriving (Show, Eq, Typeable, Data)++instType :: Bool -> Typ -> Typ+instType rightSide typ = everywhere (mkT (\(TypVar i) -> TypInst i rightSide)) typ++data Typ    = TVar    TypVar+            | Arrow   Typ     Typ+            | All     TypVar  Typ       --wir geben Typen ohne Quantifier an+            | AllStar TypVar  Typ+            | List    Typ+            --Extensions+            | Int+            | TPair    Typ     Typ+            | TEither  Typ     Typ+	    | TBrace+	    | TBool+	    | TMaybe   Typ+            deriving (Show, Eq, Typeable, Data)++unquantify :: Typ -> Typ+unquantify (All     _ t) = unquantify t+unquantify (AllStar _ t) = unquantify t+unquantify t             = t++parseType :: String -> Typ+parseType = either error id . parseType'++-- | A simple type parser.+--+-- >  parseType "Int -> [Either a b] -> (a,b)" :: Either String Typ+--+--  Right (All (TypVar 3) (All (TypVar 4) (Arrow Int (Arrow (List (TEither (TVar (TypVar 3)) (TVar (TypVar 4)))) (TPair (TVar (TypVar 3)) (TVar (TypVar 4)))))))+--+parseType' :: (MonadError String t) => String -> t Typ+parseType' s =  let (vars,types) = case span (/='.') s of+			(v,'.':t) -> (words v, t)+                        _         -> ([], s)+	 	in case parseModule ("x :: " ++ types) of+		  ParseOk hsModule -> do+			hstype <- extractTheOneType hsModule+			let varmap = createVarMap hstype+			    specials = mapMaybe (flip M.lookup varmap) (map HsIdent vars)+			typ <- runReaderT (simplifiyType hstype) varmap+ 			return (quantify specials typ)+		  ParseFailed l _  -> do+			throwError ("Parse error at (" ++ show (srcLine l) ++ ":" ++ show (srcColumn l) ++ ").")++extractTheOneType :: (MonadError String m) => HsModule -> m HsType+extractTheOneType (HsModule _ _ _ _ [HsTypeSig _ _ (HsQualType [] t)]) = return t+extractTheOneType _  = throwError "parseModule gave unexpected result"++createVarMap :: HsType -> M.Map HsName TypVar+createVarMap hstype = M.fromList $ zip+			(sort (nub (listify isVar hstype)))+			(map TypVar [1..])+  where isVar (HsIdent (x:_)) | isLower x  = True+        isVar _                            =  False+++simplifiyType :: (MonadReader (M.Map HsName TypVar) m, MonadError String m) =>+                 HsType -> m Typ+simplifiyType (HsTyFun t1 t2)+				= liftM2 Arrow (simplifiyType t1) (simplifiyType t2)+simplifiyType (HsTyTuple [t1,t2])+				= liftM2 TPair (simplifiyType t1) (simplifiyType t2)+simplifiyType (HsTyTuple _)	= throwError "Tuple with more than one type not supported."+simplifiyType (HsTyVar name)    = do Just tv <- asks (M.lookup name)+                                     return (TVar tv)+simplifiyType (HsTyCon (UnQual (HsIdent "Int")))+				= return Int+simplifiyType (HsTyCon (UnQual (HsIdent "Bool")))+				= return TBool+simplifiyType (HsTyApp (HsTyApp (HsTyCon (UnQual (HsIdent "Either"))) t1) t2)+				= liftM2 TEither (simplifiyType t1) (simplifiyType t2)+simplifiyType (HsTyApp (HsTyCon (Special HsListCon)) t)+				= liftM  List (simplifiyType t)+simplifiyType (HsTyApp (HsTyCon (UnQual (HsIdent "Maybe"))) t)+				= liftM  TMaybe (simplifiyType t)+simplifiyType (HsTyCon (Special HsUnitCon))+				= return TBrace+simplifiyType t+				= throwError ("Unsupported type " ++ show t)++quantify :: [TypVar] -> Typ -> Typ+quantify special t = foldr allQuant t (nub (listify (\(_::TypVar) -> True) t))+  where allQuant v | v `elem` special = AllStar v+                   | otherwise        = All v
+ Language/Haskell/FreeTheorems/Variations/CounterExamples/Test/TestGen.hs view
@@ -0,0 +1,75 @@+-- |This module uses "Test.Quickcheck" to test the PolyFix package by generating randomly 100 different types+-- running ExFind with that type and then simplifying the generated free theorem+-- to a antilogy of the kind \"() = _|_\" or \"0 = _|_\".+module Language.Haskell.FreeTheorems.Variations.CounterExamples.Test.TestGen where+import Test.QuickCheck+import Language.Haskell.FreeTheorems.Variations.CounterExamples.ExFind (testTerm,testSimple,getComplete)+import Language.Haskell.FreeTheorems.Variations.CounterExamples.Common.AlgCommon (showTyp)+import Language.Haskell.FreeTheorems.Variations.CounterExamples.Parser.ParseType(Typ(..), TypVar(..))+import Data.List (sort,nub)+import Control.Monad (liftM, liftM2)+import Debug.Trace++-- *Generation of example types++-- |TypVar generator+instance Arbitrary TypVar where+--  arbitrary = oneof [UnpointedVar arbitrary, PointedVar arbitrary]+  arbitrary = oneof [return (TypVar 1), return (TypVar 2), return(TypVar 3), return(TypVar 4), return (TypVar 5), return (TypVar 6)]++-- |recursive type generator+instance Arbitrary Typ where+  arbitrary = quantify (sized typ')+    where typ' 0 = frequency [(1, return Int), (6, liftM TVar arbitrary)]+          typ' n | n>0 =+               frequency [(1, liftM TVar arbitrary), (2,liftM2 Arrow subtyp1 subtyp1), (1,liftM List subtyp2), +			  (1,return Int),(1,return TBrace),(1,return TBool), (1,liftM2 TPair subtyp1 subtyp1),+			  (1,liftM2 TEither subtyp1 subtyp1), (1,liftM TMaybe subtyp2)]+	    where subtyp1 = typ' (n `div` 2)+		  subtyp2 = typ' (n-1)+          quantify t = do {tau <- t;+			   return (addquantifiers tau (usedvars tau []))+			  }+	  usedvars tau vars = case tau of+                                TVar (TypVar i) -> (i:vars)+                                Arrow t1 t2     -> (usedvars t1 []) ++ (usedvars t2 []) ++ vars+                                List t1         -> (usedvars t1 []) ++ vars+				Int             -> vars+			        TBool           -> vars+                                TBrace          -> vars+				TPair t1 t2     -> (usedvars t1 []) ++ (usedvars t2 []) ++ vars+				TEither t1 t2   -> (usedvars t1 []) ++ (usedvars t2 []) ++ vars+                                TMaybe t1       -> (usedvars t1 []) ++ vars+--				_               -> vars+	  addquantifiers tau l =  case reverse.sort.nub $ l of+				    []   -> tau+                                    x:xs -> if x < 4 +					    then addquantifiers (AllStar (TypVar x) tau) xs+					    else addquantifiers (All (TypVar x) tau) xs+++-- *test properties++prop_Test typ = trace (showTyp typ) True++prop_PrintTerms typ = trace +		  (if findsTerm +		   then "YES:" ++ showTyp typ ++ "\n\n" +		   else "" --NO: " ++ showTyp typ ++ "\n\n"+		  ) True+    where findsTerm = if (testTerm typ) == Nothing then False else True++prop_HowManyTerms typ =+   classify (findsTerm)  "Term" $+   classify (not findsTerm) "No Term" $+   True+ where findsTerm = if (testTerm typ) == Nothing then False else True++prop_SimpleResult = testSimple+    +-- *test functions++mainTest = quickCheck prop_SimpleResult+howMany  = quickCheck prop_HowManyTerms+genCheck = quickCheck prop_Test+getTerms = quickCheck prop_PrintTerms
+ Language/Haskell/FreeTheorems/Variations/CounterExamples/Test/TestItExt.hs view
@@ -0,0 +1,279 @@+module Language.Haskell.FreeTheorems.Variations.CounterExamples.Test.TestItExt where+import Test.HUnit+import Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.ExFindExtended+import Prelude hiding (Either(..))+import Language.Haskell.FreeTheorems.Variations.CounterExamples.Parser.ParseType (parseType)++-------------------------------------------------------------------------------------------------+---TestBeispiele fuer ExFind---------------------------------------------------------------------+---um alle Tests auszufuehren  runTestTT tests  aufrufen-----------------------------------------+---fuer einzelne Tests runTestTT test1  bzw. die entsprechenden Nummer statt 1-------------------+---fuer Anzeige der bei der Ableitung benutzten Regeln  getTerm bsp1  bzw. entsprechende Nr------+-------------------------------------------------------------------------------------------------++---shortcuts---+fAll i = All (TypVar i)+fAllStar i = AllStar (TypVar i)+tau1 `arrow` tau2 = Arrow tau1 tau2+var i = TVar (TypVar i)++--Beispiele:++-- RFix+bsp1 = fAll 1 (var 1)+-- RAll, R->, RI, RFix+bsp2 = fAll 1 (List (var 1) `arrow` List (var 1))+-- RAll, RAllStar, R->, LFixArrowStar, AxStar+bsp3 = fAll 1 (fAllStar 2 ((var 1 `arrow` var 2) `arrow` var 2))+-- RAll, RAllStar, R->, LIArrow, LFixArrowStar, AxStar+bsp4 = fAll 1 (fAllStar 2 ((List (var 1) `arrow` var 2) `arrow` var 2))++-- test for LI+-- RAll, RAllStar, R->, R->, LI, LFixArrowStar, AxStar+bsp5 = fAll 1 (fAllStar 2 ((List (var 2)) `arrow` ((var 1 `arrow` var 2) `arrow` var 2)))++-- test for LFix+-- RAll, RAllStar, R->, R->, LFix, LFixArrowStar, AxStar+bsp6 = fAll 1 (fAllStar 2 ( var 1 `arrow` ((var 1 `arrow` var 2) `arrow` var 2)))++-- test for L->->+-- RAll, RAllStar, R->, L->-> (fst: LFix->*, Ax*) (snd: Ax*)+bsp7 = fAll 1 (fAllStar 2 (((( var 1 `arrow` var 2) `arrow` var 2) `arrow` var 2) `arrow` var 2))++-- test for La->*1+-- RAll, RAllStar, R->, L->-> (fst: LFix->*, La->*1, Ax*) (snd: Ax*)+bsp8 = fAll 1 (fAllStar 2 (((( var 1 `arrow` (var 2 `arrow` var 2)) `arrow` var 2) `arrow` var 2) `arrow` var 2))++-- test for La->*2+-- RAll, RAllStar, R->, R->, LFix->*, La->*2, Ax*+bsp9 = fAll 1 (fAllStar 2 (fAllStar 3 (((var 1 `arrow` var 2) `arrow` ((var 2 `arrow` var 3) `arrow` var 3)))))++bsp10 = fAll 1 (fAllStar 2 ((var 1 `arrow` (List (var 2))) `arrow` var 2))++-- test for LFix+-- RAll, RAllStar, R->, LFix->, LFix->*, Ax*+bsp11 = fAll 1 (fAllStar 2 ((var 2 `arrow` (var 1 `arrow` var 2)) `arrow` var 2))++bsp12 = fAll 1 (fAllStar 2 (fAllStar 3 (fAllStar 4 ((((var 3 `arrow` (var 1 `arrow` (List (var 2)))) `arrow` var 2) `arrow` var 3) `arrow` (((var 2 `arrow` (List (var 3))) `arrow` (var 3 `arrow` var 4) `arrow` (List (var 4))))))))++-----new examples for the extended algorithm-------+--test for LInt+--RAll, R->, R->, LInt, LFix->*, Ax*+bspEx1 = fAll 1 ((var 1 `arrow` Int) `arrow` (Int `arrow` Int))++--test for LP->+--RAll, R->, LP->, LFix->*, La->*1, Ax*+bspEx2 = fAll 1 (((TPair (var 1) Int) `arrow` Int) `arrow` Int)++--test for LP+--RAll, R->, LP, LInt, LFix->*, Ax*+bspEx3 = fAll 1 ((TPair (var 1 `arrow` Int) Int) `arrow` Int)++--test for LE->+--RAll, R->, LE->, LFix->*, Ax*+bspEx4 = fAll 1 (((TEither (var 1) Int) `arrow` Int) `arrow` Int)++--test for LE->+--RAll, R->, LE->, LFix->*, Ax*+bspEx5 = fAll 1 (((TEither Int (var 1)) `arrow` Int) `arrow` Int)++--test for LE1+bspEx6 = fAll 1 ((TEither (var 1 `arrow` Int) Int) `arrow` Int)++--test for LE2+bspEx7 = fAll 1 ((TEither Int (var 1 `arrow` Int)) `arrow` Int)++--another test for LE1+bspEx8 = fAll 1 (fAllStar 2 ((TEither (var 1 `arrow` var 2) (var 1 `arrow` Int)) `arrow` ((var 2 `arrow` Int) `arrow` Int)))++--test for RP1+bspEx9 = fAll 1 (TPair (var 1) (var 1))++--test for RP2+bspEx10 = fAll 1 (TPair Int (var 1))+++--test for RE1+bspEx11 = fAll 1 (TEither (var 1) (var 1))++--test for RE2+bspEx12 = fAll 1 (TEither Int (var 1))++--test for LP*1+bspEx13 = fAll 1 ((var 1 `arrow` (TPair Int Int)) `arrow` Int)++--test for LP*2+bspEx14 = fAll 1 (fAllStar 2 ((var 1 `arrow` (TPair (var 2) Int)) `arrow` Int))++--test for LE*1+bspEx15 = fAll 1 ((var 1 `arrow` (TEither Int Int)) `arrow` Int)++--test for LE*2+bspEx16 = fAll 1 (fAllStar 2 ((var 1 `arrow` (TEither (var 2) Int)) `arrow` Int))++++-----test cases using HUnit Test--------++run test = runTestTT test+++test1 = TestCase $ assertEqual "a.a: " (Just (Bottom (All (TypVar 1) (TVar (TypVar 1))))) (testTerm bsp1)+test2 = TestCase $ assertEqual +	             "a.[a] -> [a]:" +                     (Just (TAbs (TypVar 1) (Abs (TermVar 1) (List (TVar (TypVar 1))) (Cons (Bottom (TVar (TypVar 1))) (Nil (TVar (TypVar 1)))))))+		     (testTerm bsp2)++test3 = TestCase $ assertEqual +	             "a.b.(a -> b) -> b:"+		     (Just (TAbs (TypVar 1) (TAbs (TypVar 2) (Abs (TermVar 1) (Arrow (TVar (TypVar 1)) (TVar (TypVar 2))) (App (Var (TermVar 1)) (Bottom (TVar (TypVar 1))))))))+		     (testTerm bsp3)++test4 = TestCase $ assertEqual+	             "a.b.([a] -> b) -> b:"+		     (Just (TAbs (TypVar 1) (TAbs (TypVar 2) (Abs (TermVar 1) (Arrow (List (TVar (TypVar 1))) (TVar (TypVar 2))) (App (Abs (TermVar 2) (TVar (TypVar 1)) (App (Var (TermVar 1)) (Cons (Var (TermVar 2)) (Nil (TVar (TypVar 1)))))) (Bottom (TVar (TypVar 1))))))))+		     (testTerm bsp4)++test5 = TestCase $ assertEqual+	             "a.b.[b] -> (a -> b) -> b"+		     (Just (TAbs (TypVar 1) (TAbs (TypVar 2) (Abs (TermVar 1) (List (TVar (TypVar 2))) (Abs (TermVar 2) (Arrow (TVar (TypVar 1)) (TVar (TypVar 2))) (App (Var (TermVar 2)) (Bottom (TVar (TypVar 1)))))))))+		     (testTerm bsp5)++test6 = TestCase $ assertEqual+	             "a.b.a -> (a -> b) -> b"+		     (Just (TAbs (TypVar 1) (TAbs (TypVar 2) (Abs (TermVar 1) (TVar (TypVar 1)) (Abs (TermVar 2) (Arrow (TVar (TypVar 1)) (TVar (TypVar 2))) (App (Var (TermVar 2)) (Bottom (TVar (TypVar 1)))))))))+		     (testTerm bsp6)+		     +test7 = TestCase $ assertEqual+	             "a.b.(((a -> b) -> b) -> b) -> b"+		     (Just (TAbs (TypVar 1) (TAbs (TypVar 2) (Abs (TermVar 1) (Arrow (Arrow (Arrow (TVar (TypVar 1)) (TVar (TypVar 2))) (TVar (TypVar 2))) (TVar (TypVar 2))) (App (Var (TermVar 1)) (Abs (TermVar 2) (Arrow (TVar (TypVar 1)) (TVar (TypVar 2))) (App (Var (TermVar 2)) (Bottom (TVar (TypVar 1))))))))))+		     (testTerm bsp7)++test8 = TestCase $ assertEqual+	             "a.b.(((a -> (b -> b)) -> b) -> b) -> b"+		     (Just (TAbs (TypVar 1) (TAbs (TypVar 2) (Abs (TermVar 1) (Arrow (Arrow (Arrow (TVar (TypVar 1)) (Arrow (TVar (TypVar 2)) (TVar (TypVar 2)))) (TVar (TypVar 2))) (TVar (TypVar 2))) (App (Var (TermVar 1)) (Abs (TermVar 2) (Arrow (TVar (TypVar 1)) (Arrow (TVar (TypVar 2)) (TVar (TypVar 2)))) (App (App (Var (TermVar 2)) (Bottom (TVar (TypVar 1)))) (Bottom (TVar (TypVar 2))))))))))+		     (testTerm bsp8)++test9 = TestCase $ assertEqual+	             "a.b.(a -> b) -> (b -> c) -> c"+		     (Just (TAbs (TypVar 1) (TAbs (TypVar 2) (TAbs (TypVar 3) (Abs (TermVar 1) (Arrow (TVar (TypVar 1)) (TVar (TypVar 2))) (Abs (TermVar 2) (Arrow (TVar (TypVar 2)) (TVar (TypVar 3))) (App (Var (TermVar 2)) (App (Var (TermVar 1)) (Bottom (TVar (TypVar 1)))))))))))+		     (testTerm bsp9)++test10 = TestCase $ assertEqual+	              "a.b.(a -> [b]) -> b"+		      (Just (TAbs (TypVar 1) (TAbs (TypVar 2) (Abs (TermVar 1) (Arrow (TVar (TypVar 1)) (List (TVar (TypVar 2)))) (LCase (App (Var (TermVar 1)) (Bottom (TVar (TypVar 1)))) (Bottom (TVar (TypVar 2))) (TermVar 2) (Var (TermVar 2)))))))+		      (testTerm bsp10)++test11 = TestCase $ assertEqual+	              "a.b.(b -> (a -> b)) -> b"+		      (Just (TAbs (TypVar 1) (TAbs (TypVar 2) (Abs (TermVar 1) (Arrow (TVar (TypVar 2)) (Arrow (TVar (TypVar 1)) (TVar (TypVar 2)))) (App (App (Var (TermVar 1)) (Bottom (TVar (TypVar 2)))) (Bottom (TVar (TypVar 1))))))))+		      (testTerm bsp11)++test12 = TestCase $ assertEqual+	              "a.b.c.d.((c -> (a -> [b]) -> b) -> c) -> (b -> [c]) -> (c -> d) -> [d]"+		      (Just (TAbs (TypVar 1) (TAbs (TypVar 2) (TAbs (TypVar 3) (TAbs (TypVar 4)+			       (Abs (TermVar 1) (Arrow (Arrow (Arrow (TVar (TypVar 3)) (Arrow (TVar (TypVar 1)) (List (TVar (TypVar 2))))) (TVar (TypVar 2))) (TVar (TypVar 3)))+				 (Abs (TermVar 2) (Arrow (Arrow (TVar (TypVar 2)) (List (TVar (TypVar 3)))) (Arrow (TVar (TypVar 3)) (TVar (TypVar 4))))+			       (Cons (App +				       (App (Var (TermVar 2)) +					 (Abs (TermVar 3) (TVar (TypVar 2)) +				           (Cons (App (Var (TermVar 1)) (Abs (TermVar 5) +									  (Arrow (TVar (TypVar 3)) (Arrow (TVar (TypVar 1)) (List (TVar (TypVar 2)))))+									  (LCase (App (App (Var (TermVar 5)) (Bottom (TVar (TypVar 3)))) (Bottom (TVar (TypVar 1)))) (Bottom (TVar (TypVar 2))) (TermVar 7) (Var (TermVar 7)))+									)+						 ) +				  (Nil (TVar (TypVar 3))))+				)) (Bottom (TVar (TypVar 3)))) (Nil (TVar (TypVar 4)))))))))))+		      (testTerm bsp12)++testList = [TestLabel "RFix-Test" test1, TestLabel "RAll,R->,RI-Test" test2, TestLabel "RAll*,LFix->*,Ax*-Test" test3, TestLabel "LI->-Test" test4, TestLabel "LI-Test" test5, TestLabel "LFix-Test" test6, TestLabel "L->->-Test" test7, TestLabel "La->*1" test8, TestLabel "La->*2" test9, TestLabel "LI*-Test" test10, TestLabel "LFix->-Test" test11, TestLabel "complex typ" test12 ]++tests = TestList testList++testEx1 = TestCase $ assertEqual+	               "a.(a -> Int) -> Int -> Int"+		       (Just (TAbs (TypVar 1) (Abs (TermVar 1) (Arrow (TVar (TypVar 1)) Int) (Abs (TermVar 2) Int (App (Var (TermVar 1)) (Bottom (TVar (TypVar 1))))))))+		       (testTerm bspEx1)++testEx2 = TestCase $ assertEqual+	               "a.((a,Int) -> Int) -> Int"+		       (Just (TAbs (TypVar 1) (Abs (TermVar 1) (Arrow (TPair (TVar (TypVar 1)) Int) Int) (App (App (Abs (TermVar 2) (TVar (TypVar 1)) (Abs (TermVar 3) Int (App (Var (TermVar 1))  (Pair (Var (TermVar 2)) (Var (TermVar 3)))))) (Bottom (TVar (TypVar 1)))) (Bottom Int)))))+		       (testTerm bspEx2)+testEx3 = TestCase $ assertEqual+	               "a.((a -> Int),Int) -> Int"+		       (Just (TAbs (TypVar 1) (Abs (TermVar 1) (TPair (Arrow (TVar (TypVar 1)) Int) Int) (App (PCase (Var (TermVar 1)) (TermVar 4) (TermVar 5) (Var (TermVar 4))) (Bottom (TVar (TypVar 1)))))))+		       (testTerm bspEx3)++testEx4 = TestCase $ assertEqual+	               "a.((a+Int) -> Int) -> Int"+		       (Just (TAbs (TypVar 1) (Abs (TermVar 1) (Arrow (TEither (TVar (TypVar 1)) Int) Int) (App (Abs (TermVar 2) (TVar (TypVar 1)) (App (Var (TermVar 1)) (Left (Var (TermVar 2))))) (Bottom (TVar (TypVar 1)))))))+		       (testTerm bspEx4)++testEx5 = TestCase $ assertEqual+	               "a.((Int+a) -> Int) -> Int"+		       (Just (TAbs (TypVar 1) (Abs (TermVar 1) (Arrow (TEither Int (TVar (TypVar 1))) Int) (App (Abs (TermVar 3) (TVar (TypVar 1)) (App (Var (TermVar 1)) (Right (Var (TermVar 3))))) (Bottom (TVar (TypVar 1)))))))+		       (testTerm bspEx5)++testEx6 = TestCase $ assertEqual+	               "a.((a -> Int) + Int) -> Int"+		       (Just (TAbs (TypVar 1) (Abs (TermVar 1) (TEither (Arrow (TVar (TypVar 1)) Int) Int) (App (ECase (Var (TermVar 1)) (TermVar 2) (Var (TermVar 2)) (TermVar 3) (Bottom (Arrow (TVar (TypVar 1)) Int))) (Bottom (TVar (TypVar 1)))))))+		       (testTerm bspEx6)++testEx7 = TestCase $ assertEqual+	               "a.(Int + (a -> Int)) -> Int"+		       (Just (TAbs (TypVar 1) (Abs (TermVar 1) (TEither Int (Arrow (TVar (TypVar 1)) Int)) (App (ECase (Var (TermVar 1)) (TermVar 4) (Bottom (Arrow (TVar (TypVar 1)) Int)) (TermVar 5) (Var (TermVar 5))) (Bottom (TVar (TypVar 1)))))))+		       (testTerm bspEx7)++testEx8 = TestCase $ assertEqual+	               "a.b.((a -> b) + (a -> Int)) -> (b -> Int) -> Int"+		       (Just (TAbs (TypVar 1) (TAbs (TypVar 2) (Abs (TermVar 1) (TEither (Arrow (TVar (TypVar 1)) (TVar (TypVar 2))) (Arrow (TVar (TypVar 1)) Int)) (Abs (TermVar 2) (Arrow (TVar (TypVar 2)) Int) (App (Var (TermVar 2)) (App (ECase (Var (TermVar 1)) (TermVar 3) (Var (TermVar 3)) (TermVar 4) (Bottom (Arrow (TVar (TypVar 1)) (TVar (TypVar 2))))) (Bottom (TVar (TypVar 1))))))))))+		       (testTerm bspEx8)++testEx9 = TestCase $ assertEqual+	               "a.(a,a)"+		       (Just (TAbs (TypVar 1) (Pair (Bottom (TVar (TypVar 1))) (Bottom (TVar (TypVar 1))))))+		       (testTerm bspEx9)++testEx10 = TestCase $ assertEqual+	               "a.(Int,a)"+		       (Just (TAbs (TypVar 1) (Pair (Bottom Int) (Bottom (TVar (TypVar 1))))))+		       (testTerm bspEx10)++testEx11 = TestCase $ assertEqual+	               "a.(a+a)"+		       (Just (TAbs (TypVar 1) (Left (Bottom (TVar (TypVar 1))) )))+		       (testTerm bspEx11)++testEx12 = TestCase $ assertEqual+	               "a.(a+a)"+		       (Just (TAbs (TypVar 1) (Right (Bottom (TVar (TypVar 1))))))+		       (testTerm bspEx12)++testEx13 = TestCase $ assertEqual+	               "a.(a -> (Int,Int)) -> Int"+		       (Just (TAbs (TypVar 1) (Abs (TermVar 1) (Arrow (TVar (TypVar 1)) (TPair Int Int)) (PCase (App (Var (TermVar 1)) (Bottom (TVar (TypVar 1)))) (TermVar 4) (TermVar 5) (Var (TermVar 5))))))+		       (testTerm bspEx13)++testEx14 = TestCase $ assertEqual+	               "a.b.(a -> (b,Int)) -> Int"+		       (Just (TAbs (TypVar 1) (TAbs (TypVar 2) (Abs (TermVar 1) (Arrow (TVar (TypVar 1)) (TPair (TVar (TypVar 2)) Int)) (PCase (App (Var (TermVar 1)) (Bottom (TVar (TypVar 1)))) (TermVar 4) (TermVar 5) (Var (TermVar 5)))))))+		       (testTerm bspEx14)++testEx15 = TestCase $ assertEqual+	               "a.(a -> (Int+Int)) -> Int"+		       (Just (TAbs (TypVar 1) (Abs (TermVar 1) (Arrow (TVar (TypVar 1)) (TEither Int Int)) (ECase (App (Var (TermVar 1)) (Bottom (TVar (TypVar 1)))) (TermVar 2) (Var (TermVar 2)) (TermVar 3) (Bottom Int)))))+		       (testTerm bspEx15)++testEx16 = TestCase $ assertEqual+	               "a.b.(a -> (b+Int)) -> Int"+		       (Just (TAbs (TypVar 1) (TAbs (TypVar 2) (Abs (TermVar 1) (Arrow (TVar (TypVar 1)) (TEither (TVar (TypVar 2)) Int)) (ECase (App (Var (TermVar 1)) (Bottom (TVar (TypVar 1)))) (TermVar 4) (Bottom (TVar (TypVar 2))) (TermVar 5) (Var (TermVar 5)))))))+		       (testTerm bspEx16)++exTestList = [TestLabel "LInt" testEx1, TestLabel "LP->" testEx2, TestLabel "LP" testEx3, TestLabel "LE-> (Left)" testEx4, TestLabel "LE-> (Right)" testEx5, TestLabel "LE1" testEx6, TestLabel "LE2" testEx7 , TestLabel "LE1 complex" testEx8, TestLabel "RP1" testEx9, TestLabel "RP2" testEx10, TestLabel "RE1" testEx11, TestLabel "RE2" testEx12, TestLabel "LP*1" testEx13, TestLabel "LP*2" testEx14, TestLabel "LE*1" testEx15, TestLabel "LE*2" testEx16]++exTests = TestList exTestList++allTests = TestList (testList ++ exTestList)+++testbsp = ( fAll 1 ( ( ((List Int) `arrow` var 1 ) `arrow` Int ) `arrow` Int ) )
+ README view
@@ -0,0 +1,28 @@+The module free-theorems-counterexamples-0.3 can be installed the following way:++runhaskell Setup.hs configure --user+runhaskell Setup.hs build+runhaskell Setup.hs haddock+runhaskell Setup.hs install++runhaskell Setup.hs haddock builds the documentation.+This step is not necessary.++After installation the modules+        Language.Haskell.FreeTheorems.Variations.CounterExamples.ExFind+        Language.Haskell.FreeTheorems.Variations.CounterExamples.Algorithm.ExFindExtended+        Language.Haskell.FreeTheorems.Variations.CounterExamples.Common.AlgCommon+        Language.Haskell.FreeTheorems.Variations.CounterExamples.Parser.ParseType+are available.++To start the webinterface do++$ ./test.sh++then it runs under  http://localhost:8002/++The webinterface can also be found under++http://www-ps.iai.uni-bonn/cgi-bin/exfind.cgi++Enjoy.
+ Setup.hs view
@@ -0,0 +1,5 @@+#!/usr/bin/runhaskell++import Distribution.Simple++main = defaultMain
+ counterexamples-cgi.hs view
@@ -0,0 +1,190 @@+module Main where++import Language.Haskell.FreeTheorems.Variations.CounterExamples.Parser.ParseType (parseType')+import Language.Haskell.FreeTheorems.Variations.CounterExamples.ExFind (getForWebInterface)+import Language.Haskell.FreeTheorems.Variations.CounterExamples.Common.AlgCommon(showTerm, showTrackContApplicationWithNames, showTrackContApplicationSolved, Term(Var), TermVar(..), assignTypeRelFuncs, prependRelFunc, renumberVariables, showFuncNames, showVarList, getTypeRelFuncNamesNonStrict, mapDisRelFuncsToNames)+import Language.Haskell.FreeTheorems.Parser.Haskell98 as FTP+import Language.Haskell.FreeTheorems+	( runChecks+	, check+	, filterSignatures+	, prettyTheorem+	, asTheorem+	, interpret+	, unfoldLifts+	, prettyUnfoldedLift+	, LanguageSubset(SubsetWithFix)+        , TheoremType(EquationalTheorem)+	, PrettyTheoremOption(OmitTypeInstantiations,OmitLanguageSubsets)+        , specialise+        , relationVariables+	)++import Network.CGI+import Data.ByteString.Lazy.UTF8 (fromString)+import Text.XHtml+import Control.Monad+import Data.Maybe+import Text.PrettyPrint.HughesPJ (render)+import qualified Data.Map as M+import Data.Generics+import Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.TimeOut+import Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.FTSync+++askDiv v e =  maindiv << (+	p << ( "Please enter a type. " ++++	       "You can prepend it with a list of type variables " ++++	       "that should not be considered for counterexample generation, e.g. " +++ primHtmlChar "ldquo"  +++ tt << "a b. ((a,c) -> b) -> b" +++ primHtmlChar "rdquo" +++ "." ++++	       p << ( input ! [name "type", value v] +++ " " ++++ 	       submit "submit" "Generate" )) ++++	e+	)+++askTypeForm = askDiv "[a] -> [a]" noHtml++typeError typeStr err = askDiv typeStr (+	p << ("There was a problem parsing your type: " ++++  	      pre << err )+	)++generateResult typeStr typ = +    do counter_example <- counter_exampleM+       return (askDiv typeStr noHtml ++++	maindiv << (+	h3 << "The Free Theorem" ++++	(case ft_full of+		Left err -> p << "The full Free Theorem deriver failed:" ++++                            pre << err+                Right s  -> p << "The theorem generated for functions of the type" ++++	                    pre << (termName ++ " :: " ++ dropedPreFix) ++++	                    "is:" ++++         	            pre << s+	)) ++++	maindiv << (+	h3 << "The Counterexample" ++++	( case counter_example of +		Left err -> p << if err == "_timeOut" +	                         then "Unfortunately the generator for the counterexample timed out. Time was restricted to 3 seconds." +++ ""+	                         else (let nonstrict = getTypeRelFuncNamesNonStrict typ funcNames in+                                       case nonstrict of+				         []  -> "No type variables were made available for consideration for counterexample generation." +++ ""+                                         [x] -> "Even without strictness condition on " +++ tt << x +++ " the algorithm found no counterexample."+				         xs  -> "Even without strictness conditions on " +++ tt <<showVarList xs +++ " the algorithm found no counterexample.")+		Right result ->+	                let (term,trackCont,funcs) = result+                            names = mapDisRelFuncsToNames funcs drelNames varNames +                            nonstricts = getTypeRelFuncNamesNonStrict typ funcNames in+			p << ((if length nonstricts == 1 +			      then ("By disregarding the strictness condition on " +++ tt << showVarList nonstricts +++ " the theorem becomes wrong.")+			      else ("By disregarding the strictness conditions on " +++ tt << showVarList nonstricts +++ " the theorem becomes wrong.")) ++++                             " The term" ++++	        	     pre << tt << (termName ++ " = " ++ (showTerm.head.renumberVariables $ [term])) ++++                             "is a counterexample.") ++++                        p << ("By setting " +++ tt << "t1 = t2 = ... = ()" +++ " and" ++++                             pre << assignTypeRelFuncs typ funcNames) ++++			p << ("the following would be a consequence of the thus " +++ primHtmlChar "ldquo" +++ "naivified" +++ primHtmlChar "rdquo" +++ " free theorem:" ++++                              pre << prependRelFunc funcNames (fst trackCont) ((showTrackContApplicationWithNames trackCont names (Var (TermVar 0))) ++ "\n\nwhere\n\n" ++  showFuncNames (zip (snd.unzip$names) (snd.unzip$funcs)))) ++++			p << ("But this is wrong since with the above " +++ tt << termName +++ " it reduces to:" ++++			      pre << prependRelFunc funcNames (fst trackCont) (showTrackContApplicationSolved trackCont funcs term))+	)))+  where ft_full = let properType = termName ++ " :: " ++ case span (/='.') typeStr of+                                       (t,"")  -> t+                                       (_,_:t) -> t+		      either  = "data Either a b = Left a | Right b"+                      bool    = "data Bool = False | True"+		      maybe   = "data Maybe a = Nothing | Just a"+		      parse_input = unlines [either, bool, maybe, properType]+		      (ds,es) = runChecks (parse parse_input >>= check)+                      [s]     = filterSignatures ds+		  in if null es+                     then case interpret ds (SubsetWithFix  EquationalTheorem) s of+			Nothing -> Left "interpret returned nothing"+			Just i  -> let i' = foldl specialise i (relationVariables i) in+                                   Right $ render (prettyTheorem [OmitTypeInstantiations,OmitLanguageSubsets] (asTheorem i')) +++			      case unfoldLifts ds i' of+				[] -> ""+				ls -> (if length ls == 1 +				       then "\n\nThe structural lifting occuring therein is defined as follows:\n\n "+				       else "\n\nThe structural liftings occuring therein are defined as follows:\n\n") +++				      unlines (map (render . prettyUnfoldedLift []) ls)+                     else Left (unlines (map render es))+		    +        counter_exampleM = do res <- liftIO (watchdog2 3000 (getForWebInterface typ))+			      return (case res of+			                Nothing -> Left "_timeOut"+			                Just x  -> x)+	dropedPreFix = let (prefix,typ) = break (=='.') typeStr in+                       if typ == [] then prefix else tail typ +	+main = runCGI (handleErrors cgiMain)++cgiMain = do+	setHeader "Content-type" "text/xml; charset=UTF-8"+	+	mTypeStr <- getInput "type"++	+	let content = case mTypeStr of +		Nothing      -> return askTypeForm+                Just typeStr -> case parseType' typeStr of+			Left err  -> return (typeError typeStr err)+			Right typ -> generateResult typeStr typ+	con  <- content+	outputFPS $ fromString $ showHtml $+	       header (+		thetitle << "Automatically Generating Counterexamples to Naive Free Theorems" ++++		style ! [ thetype "text/css" ] << cdata cssStyle+	       ) ++++	       body ( form ! [method "POST", action "#"] << (+		thediv ! [theclass "top"] << (+			thespan ! [theclass "title"] << "Haskell" ++++			thespan ! [theclass "subtitle"] << "Automatically Generating Counterexamples to Naive Free Theorems"+		) ++++               maindiv ( p << ("This tool allows you to run the algorithm described in the paper "+	       +++ primHtmlChar "ldquo"+               +++ hotlink "http://www.iai.uni-bonn.de/~jv/paper.pdf" +               << "Automatically Generating Counterexamples to Naive Free Theorems"+	       +++ primHtmlChar "rdquo" +       	       +++ " (FLOPS'10) by Daniel Seidel and " +               +++ hotlink "http://www.iai.uni-bonn.de/~jv"+               << (toHtml "Janis Voigtländer")+                +++ ".") +               +++ p << ("You may also want to try the following related tools:" +                         +++ ulist << [ li << (primHtmlChar "ldquo" +++ hotlink "http://www-ps.iai.uni-bonn.de/ft" << "Automatic Generation of Free Theorems" +++ primHtmlChar "rdquo") +                                      , li << (primHtmlChar "ldquo" +++ hotlink "http://www-ps.iai.uni-bonn.de/cgi-bin/polyseq.cgi" << "Taming Selective Strictness" +++ primHtmlChar "rdquo") +                                      ])) ++++		con ++++		maindiv ( p << ("The source code is available for " +++ +				hotlink "http://hackage.haskell.org/package/free-theorems-counterexamples" << "download" ++++				".") ++++			   p << ("© 2010 Daniel Seidel <" +++ hotlink "mailto:ds@iai.uni-bonn.de" << "ds@iai.uni-bonn.de" +++ "> and Joachim Breitner <" ++++				hotlink "mailto:mail@joachim-breitner.de" << "mail@joachim-breitner.de" ++++				">")+			)       +		))++maindiv = thediv ! [theclass "main"]++cdata s = primHtml ("<![CDATA[\n"++ s ++ "\n]]>")++cssStyle = unlines +        [ "body { padding:0px; margin: 0px; }"+        , "div.top { margin:0px; padding:10px; margin-bottom:20px;"+        , "              background-color:#efefef;"+        , "              border-bottom:1px solid black; }"+        , "span.title { font-size:xx-large; font-weight:bold; }"+        , "span.subtitle { padding-left:30px; font-size:large; }"+        , "div.main { border:1px dotted black;"+        , "                   padding:10px; margin:10px; }"+        , "div.submain { padding:10px; margin:11px; }"+        , "p.subtitle { font-size:large; font-weight:bold; }"+        , "input.type { font-family:monospace; }"+        , "input[type=\"submit\"] { font-family:monospace; background-color:#efefef; }"+        , "span.mono { font-family:monospace; }"+        , "pre { margin:10px; margin-left:20px; padding:10px;"+        , "          border:1px solid black; }"+        , "textarea { margin:10px; margin-left:20px; padding:10px;  }"+        , "p { text-align:justify; }"+        ]
+ free-theorems-counterexamples.cabal view
@@ -0,0 +1,79 @@+name:           free-theorems-counterexamples+version:        0.3+license:        PublicDomain+author:         Daniel Seidel, Joachim Breitner+maintainer:     ds@iai.uni-bonn.de+synopsis:       Automatically Generating Counterexamples to Naive Free Theorems+description:+	This program is to verify (or to put into question) strictness conditions +	on free theorems that arise if a polymorphic lambda calculus is	enriched by +	general recursion.+	Given a type the program either returns an instance of the corresponding+	unrestricted free theorem that does not hold and thereby verifies the need+	of the additional restrictions or it returns without finding such an+	instantiation and thereby suggests (but not proves) that the strictness+	conditions are superfluous.+	The underlying algorithm is described in \"Automatically Generating +	Counterexamples to Naive Free Theorems\" (FLOPS'10) by Daniel Seidel and Janis+	Voigtländer.+	A webinterface for the program is also available at +	<http://www-ps.iai.uni-bonn.de/cgi-bin/exfind.cgi>.+	.+	Related to this package you may be interested in the online free theorem generator+	at <http://www-ps.iai.uni-bonn.de/ft> that is also available offline via+	<http://hackage.haskell.org/cgi-bin/hackage-scripts/package/free-theorems-webui>.+	Also interesting may be the tool polyseq that generates \"optimal\" free theorems in a +	polymorphic lambda calculus with selective strictness.+	Polyseq can be downloaded at +	<http://hackage.haskell.org/cgi-bin/hackage-scripts/package/polyseq>+	but the functionality is as well provided via a webinterface at+	<http://www-ps.iai.uni-bonn.de/cgi-bin/polyseq.cgi>.+	+category:       Language+tested-with:    GHC==6.8.2+build-type:	Simple+cabal-version:  >= 1.2.3++extra-source-files:+    Language/Haskell/FreeTheorems/Variations/CounterExamples/Test/TestItExt.hs+    Language/Haskell/FreeTheorems/Variations/CounterExamples/Test/TestGen.hs+    testcgi.py+    test.sh+    README++library+    build-depends:+        mtl >= 1.0+      , haskell-src >= 1.0+      , haskell-src-exts >= 0.3.9+      , pretty >= 1.0.0.0+      , containers >= 0.1.0.1+      , HUnit >= 1.2+    if impl(ghc >= 6.10)+      build-depends:+          base >= 4+        , syb >= 0.1.0.0+    else+      build-depends:+          base >= 1 && < 4+    exposed-modules:+        Language.Haskell.FreeTheorems.Variations.CounterExamples.ExFind+        Language.Haskell.FreeTheorems.Variations.CounterExamples.Parser.ParseType+        Language.Haskell.FreeTheorems.Variations.CounterExamples.Common.AlgCommon+        Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.ExFindExtended+    other-modules:+        Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.FTSync+        Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.M+        Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.TimeOut++executable counterexamples.cgi+    main-is:+        counterexamples-cgi.hs+    build-depends:+        xhtml, cgi, utf8-string, free-theorems >= 0.3.1++  extensions:+      FlexibleContexts+    , DeriveDataTypeable +    , ScopedTypeVariables+
+ test.sh view
@@ -0,0 +1,2 @@+#!/bin/bash+./testcgi.py ./dist/build/counterexamples.cgi/counterexamples.cgi
+ testcgi.py view
@@ -0,0 +1,18 @@+#!/usr/bin/python++from BaseHTTPServer import HTTPServer+from CGIHTTPServer import CGIHTTPRequestHandler+import sys++class MyRequestHandler(CGIHTTPRequestHandler):+	def is_cgi(self):+		self.cgi_info = ("","")+		return True++	def translate_path(self, path):+		return sys.argv[1]+++server_address = ('', 8002)+http  = HTTPServer(server_address, MyRequestHandler)+http.serve_forever()