free-theorems-counterexamples 0.3.0.2 → 0.3.1.0
raw patch · 7 files changed
+264/−122 lines, 7 filesdep ~free-theorems
Dependency ranges changed: free-theorems
Files
- Language/Haskell/FreeTheorems/Variations/CounterExamples/Common/AlgCommon.hs +92/−46
- Language/Haskell/FreeTheorems/Variations/CounterExamples/Internal/ExFindExtended.hs +55/−5
- Language/Haskell/FreeTheorems/Variations/CounterExamples/Parser/ParseType.hs +8/−3
- Language/Haskell/FreeTheorems/Variations/CounterExamples/Test/TestGen.hs +3/−2
- Language/Haskell/FreeTheorems/Variations/CounterExamples/Test/TestItExt.hs +101/−62
- counterexamples-cgi.hs +3/−2
- free-theorems-counterexamples.cabal +2/−2
Language/Haskell/FreeTheorems/Variations/CounterExamples/Common/AlgCommon.hs view
@@ -8,7 +8,7 @@ unpointed, isElementaryType, findfirstSpecialType, findfirstWithTVars, findallWithTVars, findfirst, findall, typeCheckArrowListArg, typeCheckArrowMaybeArg, typeCheckList, typeCheckMaybe, typeCheckArrowUnPointedArgPointedRes, typeCheckArrowArgArrow,- typeCheckArrow, typeCheckInt, typeCheckBrace, typeCheckBool, typeCheckPair, typeCheckArrowPairArg,+ typeCheckArrow, typeCheckInt, typeCheckNat, typeCheckBrace, typeCheckBool, typeCheckPair, typeCheckArrowPairArg, typeCheckArrowEitherArg, typeCheckEither, insertArgument, subst, substAllInt, makePlusPair, makePlusElem, makeFuncPair, initialiseTermCont, mergeTermCont,@@ -58,12 +58,13 @@ --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+--traceIO = \rule tauIn gammaIn tauOut gammaOut -> (traceIO_ord2shell 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+--traceTemp = trace_toShell+traceTemp = trace_ignore ---- show settings --- -- |show settings for the trace functions@@ -101,7 +102,7 @@ --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+ if unsafePerformIO (putStr (show rule ++ ":\n" ++ (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 =@@ -111,7 +112,7 @@ 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+ if firstNegative ordDiff || (not . and) (map (==0) 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)) @@ -164,6 +165,7 @@ 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])+ TNat -> (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)@@ -208,6 +210,9 @@ -- |integer case-statement -- ICase t0 t1 <==> Case t0 of {0 => t1; _ => _|_} | ICase Term Term+ -- |integer case-statement+ -- NCase t0 t1 <==> Case t0 of {0 => t1; _ => _|_}+ | NCase Term Term -- |brace case-statement -- BCase t0 t1 <==> Case t0 of {() => t1} | BCase Term Term @@ -267,11 +272,14 @@ -- |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+-- isFst t =+-- case t of+-- Abs _ _ (PCase _ x _ t1) ->+-- if Var x == t1 then True else False+-- _ -> False+isFst (Abs v _ (PCase t x _ (Var y))) | x == y && Var v == t = True+ | otherwise = False+isFst _ = False -- |\p -> Case p of {(v1,v2) ==> v2} second :: Typ -> M Term@@ -286,11 +294,14 @@ -- |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+-- isSnd t =+-- case t of+-- Abs _ _ (PCase _ _ y t1) -> +-- if Var y == t1 then True else False+-- _ -> False+isSnd (Abs v _ (PCase t _ x (Var y))) | x == y && Var v == t = True+ | otherwise = False+isSnd _ = False -- |\l -> Case l of {[] => _|_; x:_ => x} listhead :: Typ -> M Term@@ -303,11 +314,14 @@ -- |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+-- isHead t =+-- case t of+-- Abs _ _ (LCase _ v t2) -> +-- if Var v == t2 then True else False+-- _ -> False+isHead (Abs v _ (LCase t x (Var y))) | x == y && Var v == t = True+ | otherwise = False+isHead _ = False -- |\l -> Case l of {Just x => x} fromJust :: Typ -> M Term@@ -320,11 +334,14 @@ -- |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+-- isFromJust t =+-- case t of+-- Abs _ _ (MCase _ v t2) -> +-- if Var v == t2 then True else False+-- _ -> False+isFromJust (Abs v _ (MCase t x (Var y))) | x == y && Var v == t = True+ | otherwise = False+isFromJust _ = False -- |\e -> Case e of {Left x => x; Right x => _|_} fromLeft :: Typ -> Typ -> M Term@@ -339,15 +356,18 @@ -- |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+-- isFromLeft t =+-- case t of+-- Abs _ _ (ECase _ v1 t1 _ t2) -> +-- if Var v1 == t1 +-- then case t2 of+-- Bottom _ -> True+-- _ -> False+-- else False+-- _ -> False+isFromLeft (Abs v _ (ECase t x (Var y) _ _)) | x == y && Var v == t = True+ | otherwise = False+isFromLeft _ = False -- |\e -> Case e of {Left x => _|_; Right x => x} fromRight :: Typ -> Typ -> M Term@@ -362,15 +382,18 @@ -- |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+-- isFromRight t =+-- case t of+-- Abs _ _ (ECase _ _ t1 v2 t2) -> +-- if Var v2 == t2 +-- then case t1 of+-- Bottom _ -> True+-- _ -> False+-- else False+-- _ -> False+isFromRight (Abs v _ (ECase t _ _ x (Var y))) | x == y && Var v == t = True+ | otherwise = False+isFromRight _ = False -- | some abbreviations for special cases of the Case-statements.@@ -512,6 +535,7 @@ AllStar _ tau' -> unpointed tvars tau' List _ -> False Int -> False+ TNat -> False TPair _ _ -> False TEither _ _ -> False TBool -> False@@ -522,6 +546,7 @@ isElementaryType tau = case tau of Int -> True+ TNat -> True TVar _ -> True TBrace -> True TBool -> True@@ -631,6 +656,12 @@ Int -> True _ -> False +-- | used for (Drop5)+typeCheckNat :: Typ -> Bool+typeCheckNat tau = case tau of+ TNat -> True+ _ -> False+ -- | used for (Drop2) typeCheckBrace :: Typ -> Bool typeCheckBrace tau = case tau of@@ -695,6 +726,7 @@ 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)+ NCase m0 m1 -> NCase (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)@@ -743,6 +775,7 @@ return erg } Int -> return (Just Zero)+ TNat -> return (Just Zero) TBrace -> return (Just Brace) TBool -> return (Just Fls) TPair tau1 tau2 -> do {x <- makePlusElem tau1;@@ -785,7 +818,10 @@ let w = TermVar i in return (Abs w tau (ICase (Var w) z), Abs w tau (ICase (Var w) z')) }-+ TNat -> do {i <- newInt;+ let w = TermVar i in+ return (Abs w tau (NCase (Var w) z), Abs w tau (NCase (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'))@@ -977,6 +1013,11 @@ 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))+ NCase t1 t2 -> let t1' = simplifyTerm t1 in+ case t1' of+ Bottom tau -> traceSimplify "Simpl: NCase with _|_ to _|_" (Bottom (error "Typ not valid anymore."))+ Zero -> traceSimplify "Simpl: NCase with 0 to t1" (simplifyTerm t2)+ _ -> traceSimplify "Simpl: NCase not reduced." (NCase (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."))@@ -1026,6 +1067,7 @@ 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)+ NCase t1 t2 -> NCase (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)@@ -1182,6 +1224,7 @@ TAbs (TypVar i) t -> getVarNums t Brace -> [] ICase t1 t2 -> getVarNums t1 ++ getVarNums t2+ NCase 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@@ -1207,6 +1250,7 @@ TAbs tv t -> TAbs tv (renumberVars t varMap) Brace -> Brace ICase t1 t2 -> ICase (renumberVars t1 varMap) (renumberVars t2 varMap)+ NCase t1 t2 -> NCase (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)@@ -1303,6 +1347,7 @@ Brace -> "()" Fls -> "False" ICase t1 t2 -> "(case " ++ showTermWithNames t1 m ++ " of {0 -> " ++ showTermWithNames t2 m ++ "})"+ NCase 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 ++ ")"@@ -1319,8 +1364,8 @@ --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+ 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 @@ -1336,6 +1381,7 @@ AllStar v t1 -> "\\" ++ showTyp (TVar v) ++ "." ++ showTyp t1 List t1 -> "[" ++ showTyp t1 ++ "]" Int -> "Int"+ TNat -> "Nat" TPair t1 t2 -> "(" ++ showTyp t1 ++ "," ++ showTyp t2 ++ ")" TEither t1 t2 -> "(Either " ++ showTyp t1 ++ " " ++ showTyp t2 ++ ")" TBrace -> "()"
Language/Haskell/FreeTheorems/Variations/CounterExamples/Internal/ExFindExtended.hs view
@@ -183,6 +183,16 @@ dRop1_tc_update :: TermCont -> TermVar -> TermCont dRop1_tc_update tc v = Map.insert v ((Zero,Zero),Leaf) tc +dRop5 :: Cont -> Maybe (Cont,TermVar)+dRop5 gamma = let l = findfirst typeCheckNat (vars gamma) in+ case l of+ Nothing -> Nothing+ Just var -> Just ((removeVar gamma (fst var)),fst var)++dRop5_tc_update :: TermCont -> TermVar -> TermCont+dRop5_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@@ -563,8 +573,17 @@ iNtStar_tc_update :: TermCont -> TermVar -> TermCont iNtStar_tc_update tc var = Map.insert var ((Zero,Zero),Leaf) tc +nAtStar :: Cont -> Maybe (Cont,Term -> Term, TypedVar)+nAtStar gamma = case findfirstSpecialType (varsStar gamma) TNat of+ Nothing -> Nothing+ Just x -> Just (removeVarStar gamma (fst x), \m -> NCase (Var (fst x)) m, x)++nAtStar_tc_update :: TermCont -> TermVar -> TermCont+nAtStar_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+bRaceStar gamma = case findfirstSpecialType (varsStar gamma) TBrace of Nothing -> Nothing Just x -> Just (removeVarStar gamma (fst x), \m -> BCase (Var (fst x)) m, x) @@ -572,7 +591,7 @@ 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+bOolStar gamma = case findfirstSpecialType (varsStar gamma) TBool of Nothing -> Nothing Just x -> Just (removeVarStar gamma (fst x), \m -> BoolCase (Var (fst x)) m, x) @@ -674,6 +693,10 @@ iNtStripe :: Typ -> Maybe Term iNtStripe tau = if tau == Int then Just Zero else Nothing++nAtStripe :: Typ -> Maybe Term+nAtStripe tau = if tau == TNat then Just Zero else Nothing+ bRaceStripe :: Typ -> Maybe Term bRaceStripe tau = if tau == TBrace then Just Brace else Nothing@@ -745,12 +768,19 @@ } alg1_Drop1 gamma tau termCont = case dRop1 gamma of- Nothing -> alg1_Drop2 gamma tau termCont+ Nothing -> alg1_Drop5 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_Drop5 gamma tau termCont = case dRop5 gamma of+ Nothing -> alg1_Drop2 gamma tau termCont+ Just (gamma',v) -> do{track (makeTrackString "Drop_5" gamma' tau);+ (t,c,trc) <- (traceIO "Drop_5" tau gamma tau gamma' (alg1 gamma' tau termCont));+ return (t,dRop5_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);@@ -991,7 +1021,7 @@ alg2_IntStar gamma tau termCont = case iNtStar gamma of- Nothing -> alg2_BraceStar gamma tau termCont+ Nothing -> alg2_NatStar 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);@@ -1001,6 +1031,18 @@ choice subderivation (alg2_HeadStar gamma tau termCont) } +alg2_NatStar gamma tau termCont = + case nAtStar gamma of+ Nothing -> alg2_BraceStar gamma tau termCont+ Just (gamma',f,v) -> do {let subderivation =+ do {track (makeTrackString "Nat*" gamma' tau);+ (t,c,trc) <- traceIO "Nat*" tau gamma tau gamma' (alg3 gamma' tau termCont);+ return (f t, nAtStar_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@@ -1146,8 +1188,16 @@ alg3_IntStripe gamma tau termCont = case iNtStripe tau of- Nothing -> alg3_BraceStripe gamma tau termCont+ Nothing -> alg3_NatStripe gamma tau termCont Just t -> do {track ((makeTrackString "Int'" gamma tau) ++ " !!END OF BRANCH!!");+ tc <- stripePhase_tc_update gamma;+ return (t, tc, (tau,[]))+ }++alg3_NatStripe gamma tau termCont = + case nAtStripe tau of+ Nothing -> alg3_BraceStripe gamma tau termCont+ Just t -> do {track ((makeTrackString "Nat'" gamma tau) ++ " !!END OF BRANCH!!"); tc <- stripePhase_tc_update gamma; return (t, tc, (tau,[])) }
Language/Haskell/FreeTheorems/Variations/CounterExamples/Parser/ParseType.hs view
@@ -41,8 +41,11 @@ | TBrace | TBool | TMaybe Typ+ | TNat deriving (Show, Eq, Typeable, Data) +typeDecls = "data Nat = Nat"+ unquantify :: Typ -> Typ unquantify (All _ t) = unquantify t unquantify (AllStar _ t) = unquantify t@@ -61,7 +64,7 @@ parseType' s = let (vars,types) = case span (/='.') s of (v,'.':t) -> (words v, t) _ -> ([], s)- in case parseModule ("x :: " ++ types) of+ in case parseModule (typeDecls ++ "\n\n" ++ "x :: " ++ types) of ParseOk hsModule -> do hstype <- extractTheOneType hsModule let varmap = createVarMap hstype@@ -72,8 +75,8 @@ 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"+extractTheOneType (HsModule _ _ _ _ [_, HsTypeSig _ _ (HsQualType [] t)]) = return t+extractTheOneType x = throwError $ "parseModule gave unexpected result" ++ show x createVarMap :: HsType -> M.Map HsName TypVar createVarMap hstype = M.fromList $ zip@@ -104,6 +107,8 @@ = liftM TMaybe (simplifiyType t) simplifiyType (HsTyCon (Special HsUnitCon)) = return TBrace+simplifiyType (HsTyCon (UnQual (HsIdent "Nat")))+ = return TNat simplifiyType t = throwError ("Unsupported type " ++ show t)
Language/Haskell/FreeTheorems/Variations/CounterExamples/Test/TestGen.hs view
@@ -20,10 +20,10 @@ -- |recursive type generator instance Arbitrary Typ where arbitrary = quantify (sized typ')- where typ' 0 = frequency [(1, return Int), (6, liftM TVar arbitrary)]+ where typ' 0 = frequency [(1, return Int), (1, return TNat), (12, 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,return Int),(1,return TNat),(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)@@ -35,6 +35,7 @@ Arrow t1 t2 -> (usedvars t1 []) ++ (usedvars t2 []) ++ vars List t1 -> (usedvars t1 []) ++ vars Int -> vars+ TNat -> vars TBool -> vars TBrace -> vars TPair t1 t2 -> (usedvars t1 []) ++ (usedvars t2 []) ++ vars
Language/Haskell/FreeTheorems/Variations/CounterExamples/Test/TestItExt.hs view
@@ -1,10 +1,17 @@ module Language.Haskell.FreeTheorems.Variations.CounterExamples.Test.TestItExt where import Test.HUnit import Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.ExFindExtended+import Language.Haskell.FreeTheorems.Variations.CounterExamples.Common.AlgCommon (Term(..), TermVar(..), showTerm)+import Language.Haskell.FreeTheorems.Variations.CounterExamples.ExFind (testTerm) import Prelude hiding (Either(..))-import Language.Haskell.FreeTheorems.Variations.CounterExamples.Parser.ParseType (parseType)+import Language.Haskell.FreeTheorems.Variations.CounterExamples.Parser.ParseType (parseType, Typ(..), TypVar(..)) -------------------------------------------------------------------------------------------------+---ACHTUNG: Auskommentierte Tests sind veraltet.-------------------------------------------------+-- Tests koennen auch mit run allTests ausgefuehrt werden.---------------------------------------+-------------------------------------------------------------------------------------------------++------------------------------------------------------------------------------------------------- ---TestBeispiele fuer ExFind--------------------------------------------------------------------- ---um alle Tests auszufuehren runTestTT tests aufrufen----------------------------------------- ---fuer einzelne Tests runTestTT test1 bzw. die entsprechenden Nummer statt 1-------------------@@ -17,6 +24,10 @@ tau1 `arrow` tau2 = Arrow tau1 tau2 var i = TVar (TypVar i) +mShowTerm :: Maybe Term -> String+mShowTerm (Just t) = showTerm t+mShowTerm _ = error "no Term to show"+ --Beispiele: -- RFix@@ -59,57 +70,57 @@ -----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))+bspEx1 = fAll 1 ((var 1 `arrow` TNat) `arrow` (TNat `arrow` TNat)) --test for LP-> --RAll, R->, LP->, LFix->*, La->*1, Ax*-bspEx2 = fAll 1 (((TPair (var 1) Int) `arrow` Int) `arrow` Int)+bspEx2 = fAll 1 (((TPair (var 1) TNat) `arrow` TNat) `arrow` TNat) --test for LP --RAll, R->, LP, LInt, LFix->*, Ax*-bspEx3 = fAll 1 ((TPair (var 1 `arrow` Int) Int) `arrow` Int)+bspEx3 = fAll 1 ((TPair (var 1 `arrow` TNat) TNat) `arrow` TNat) --test for LE-> --RAll, R->, LE->, LFix->*, Ax*-bspEx4 = fAll 1 (((TEither (var 1) Int) `arrow` Int) `arrow` Int)+bspEx4 = fAll 1 (((TEither (var 1) TNat) `arrow` TNat) `arrow` TNat) --test for LE-> --RAll, R->, LE->, LFix->*, Ax*-bspEx5 = fAll 1 (((TEither Int (var 1)) `arrow` Int) `arrow` Int)+bspEx5 = fAll 1 (((TEither TNat (var 1)) `arrow` TNat) `arrow` TNat) --test for LE1-bspEx6 = fAll 1 ((TEither (var 1 `arrow` Int) Int) `arrow` Int)+bspEx6 = fAll 1 ((TEither (var 1 `arrow` TNat) TNat) `arrow` TNat) --test for LE2-bspEx7 = fAll 1 ((TEither Int (var 1 `arrow` Int)) `arrow` Int)+bspEx7 = fAll 1 ((TEither TNat (var 1 `arrow` TNat)) `arrow` TNat) --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)))+bspEx8 = fAll 1 (fAllStar 2 ((TEither (var 1 `arrow` var 2) (var 1 `arrow` TNat)) `arrow` ((var 2 `arrow` TNat) `arrow` TNat))) --test for RP1 bspEx9 = fAll 1 (TPair (var 1) (var 1)) --test for RP2-bspEx10 = fAll 1 (TPair Int (var 1))+bspEx10 = fAll 1 (TPair TNat (var 1)) --test for RE1 bspEx11 = fAll 1 (TEither (var 1) (var 1)) --test for RE2-bspEx12 = fAll 1 (TEither Int (var 1))+bspEx12 = fAll 1 (TEither TNat (var 1)) --test for LP*1-bspEx13 = fAll 1 ((var 1 `arrow` (TPair Int Int)) `arrow` Int)+bspEx13 = fAll 1 ((var 1 `arrow` (TPair TNat TNat)) `arrow` TNat) --test for LP*2-bspEx14 = fAll 1 (fAllStar 2 ((var 1 `arrow` (TPair (var 2) Int)) `arrow` Int))+bspEx14 = fAll 1 (fAllStar 2 ((var 1 `arrow` (TPair (var 2) TNat)) `arrow` TNat)) --test for LE*1-bspEx15 = fAll 1 ((var 1 `arrow` (TEither Int Int)) `arrow` Int)+bspEx15 = fAll 1 ((var 1 `arrow` (TEither TNat TNat)) `arrow` TNat) --test for LE*2-bspEx16 = fAll 1 (fAllStar 2 ((var 1 `arrow` (TEither (var 2) Int)) `arrow` Int))+bspEx16 = fAll 1 (fAllStar 2 ((var 1 `arrow` (TEither (var 2) TNat)) `arrow` TNat)) @@ -118,7 +129,7 @@ run test = runTestTT test -test1 = TestCase $ assertEqual "a.a: " (Just (Bottom (All (TypVar 1) (TVar (TypVar 1))))) (testTerm bsp1)+test1 = TestCase $ assertEqual "a.a: " (Just (TAbs (TypVar 1) (Bottom (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)))))))@@ -161,8 +172,8 @@ 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)+ (mShowTerm (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)))) (TermVar 2) (Var (TermVar 2))))))))+ (mShowTerm $ testTerm bsp10) test11 = TestCase $ assertEqual "a.b.(b -> (a -> b)) -> b"@@ -171,7 +182,7 @@ 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)+ (mShowTerm (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 @@ -179,55 +190,67 @@ (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)))+ (LCase (App (App (Var (TermVar 5)) (Bottom (TVar (TypVar 3)))) (Bottom (TVar (TypVar 1)))) (TermVar 7) (Var (TermVar 7))) ) ) (Nil (TVar (TypVar 3))))- )) (Bottom (TVar (TypVar 3)))) (Nil (TVar (TypVar 4)))))))))))- (testTerm bsp12)+ )) (Bottom (TVar (TypVar 3)))) (Nil (TVar (TypVar 4))))))))))))+ (mShowTerm $ 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 ]+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))))))))+ "a.(a -> Nat) -> Nat -> Nat"+ (Just (TAbs (TypVar 1) (Abs (TermVar 1) (Arrow (TVar (TypVar 1)) TNat) (Abs (TermVar 2) TNat (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)))))+ "a.((a,Nat) -> Nat) -> Nat"+ (Just (TAbs (TypVar 1) (Abs (TermVar 1) (Arrow (TPair (TVar (TypVar 1)) TNat) TNat) (App (App (Abs (TermVar 2) (TVar (TypVar 1)) (Abs (TermVar 3) TNat (App (Var (TermVar 1)) (Pair (Var (TermVar 2)) (Var (TermVar 3)))))) (Bottom (TVar (TypVar 1)))) (Bottom TNat))))) (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)))))))+ "a.((a -> Nat),Nat) -> Nat"+ (Just (TAbs (TypVar 1) (Abs (TermVar 1) (TPair (Arrow (TVar (TypVar 1)) TNat) TNat) (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)))))))+ "a.((a+Nat) -> Nat) -> Nat"+ (Just (TAbs (TypVar 1) (Abs (TermVar 1) (Arrow (TEither (TVar (TypVar 1)) TNat) TNat) (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)))))))+ "a.((Nat+a) -> Nat) -> Nat"+ (Just (TAbs (TypVar 1) (Abs (TermVar 1) (Arrow (TEither TNat (TVar (TypVar 1))) TNat) (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)+ "a.((a -> Nat) + Nat) -> Nat"+ (mShowTerm (Just (TAbs (TypVar 1) (Abs (TermVar 1) (TEither (Arrow (TVar (TypVar 1)) TNat) TNat) (App (ECase (Var (TermVar 1)) (TermVar 2) (Var (TermVar 2)) (TermVar 3) (Bottom (Arrow (TVar (TypVar 1)) TNat))) (Bottom (TVar (TypVar 1))))))))+ (mShowTerm $ 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)+ "a.(Nat + (a -> Nat)) -> Nat"+ (mShowTerm (Just (TAbs (TypVar 1) (Abs (TermVar 1) (TEither TNat (Arrow (TVar (TypVar 1)) TNat)) (App (ECase (Var (TermVar 1)) (TermVar 4) (Bottom (Arrow (TVar (TypVar 1)) TNat)) (TermVar 5) (Var (TermVar 5))) (Bottom (TVar (TypVar 1))))))))+ (mShowTerm $ 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)+ "a.b.((a -> b) + (a -> Nat)) -> (b -> Nat) -> Nat"+ (mShowTerm (Just (TAbs (TypVar 1) (TAbs (TypVar 2) (Abs (TermVar 1) (TEither (Arrow (TVar (TypVar 1)) (TVar (TypVar 2))) (Arrow (TVar (TypVar 1)) TNat)) (Abs (TermVar 2) (Arrow (TVar (TypVar 2)) TNat) (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)))))))))))+ (mShowTerm $ testTerm bspEx8) testEx9 = TestCase $ assertEqual "a.(a,a)"@@ -235,8 +258,8 @@ (testTerm bspEx9) testEx10 = TestCase $ assertEqual- "a.(Int,a)"- (Just (TAbs (TypVar 1) (Pair (Bottom Int) (Bottom (TVar (TypVar 1))))))+ "a.(Nat,a)"+ (Just (TAbs (TypVar 1) (Pair (Bottom TNat) (Bottom (TVar (TypVar 1)))))) (testTerm bspEx10) testEx11 = TestCase $ assertEqual@@ -249,31 +272,47 @@ (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)+-- testEx13 = TestCase $ assertEqual+-- "a.(a -> (Nat,Nat)) -> Nat"+-- (mShowTerm (Just (TAbs (TypVar 1) (Abs (TermVar 1) (Arrow (TVar (TypVar 1)) (TPair TNat TNat)) (PCase (App (Var (TermVar 1)) (Bottom (TVar (TypVar 1)))) (TermVar 4) (TermVar 5) (Var (TermVar 5)))))))+-- (mShowTerm $ 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)+-- testEx14 = TestCase $ assertEqual+-- "a.b.(a -> (b,Nat)) -> Nat"+-- (mShowTerm (Just (TAbs (TypVar 1) (TAbs (TypVar 2) (Abs (TermVar 1) (Arrow (TVar (TypVar 1)) (TPair (TVar (TypVar 2)) TNat)) (PCase (App (Var (TermVar 1)) (Bottom (TVar (TypVar 1)))) (TermVar 4) (TermVar 5) (Var (TermVar 5))))))))+-- (mShowTerm $ 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)+-- testEx15 = TestCase $ assertEqual+-- "a.(a -> (Nat+Nat)) -> Nat"+-- (mShowTerm (Just (TAbs (TypVar 1) (Abs (TermVar 1) (Arrow (TVar (TypVar 1)) (TEither TNat TNat)) (ECase (App (Var (TermVar 1)) (Bottom (TVar (TypVar 1)))) (TermVar 2) (Var (TermVar 2)) (TermVar 3) (Bottom TNat))))))+-- (mShowTerm $ 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)+-- testEx16 = TestCase $ assertEqual+-- "a.b.(a -> (b+Nat)) -> Nat"+-- (mShowTerm (Just (TAbs (TypVar 1) (TAbs (TypVar 2) (Abs (TermVar 1) (Arrow (TVar (TypVar 1)) (TEither (TVar (TypVar 2)) TNat)) (ECase (App (Var (TermVar 1)) (Bottom (TVar (TypVar 1)))) (TermVar 4) (Bottom (TVar (TypVar 2))) (TermVar 5) (Var (TermVar 5))))))))+-- (mShowTerm $ 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]+exTestList = [ TestLabel "LNat" 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 ) )+testbsp = ( fAll 1 ( ( ((List TNat) `arrow` var 1 ) `arrow` TNat ) `arrow` TNat ) )
counterexamples-cgi.hs view
@@ -95,7 +95,8 @@ 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]+ nat = "type Nat = Int"+ parse_input = unlines [either, bool, maybe, nat, properType] (ds,es) = runChecks (parse parse_input >>= check) [s] = filterSignatures ds in if null es@@ -159,7 +160,7 @@ 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 <" ++++ p << ("© 2010-2013 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" +++ ">") )
free-theorems-counterexamples.cabal view
@@ -1,5 +1,5 @@ name: free-theorems-counterexamples-version: 0.3.0.2+version: 0.3.1.0 license: PublicDomain author: Daniel Seidel, Joachim Breitner maintainer: ds@iai.uni-bonn.de@@ -70,7 +70,7 @@ main-is: counterexamples-cgi.hs build-depends:- xhtml, cgi, utf8-string, free-theorems >= 0.3.2+ xhtml, cgi, utf8-string, free-theorems >= 0.3.1.3 extensions: FlexibleContexts