[Branched out the library parts from the data-conversion project. nad**20040615144316] { adddir ./ChasingBottoms addfile ./ChasingBottoms/Approx.hs hunk ./ChasingBottoms/Approx.hs 1 +{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-} + +module ChasingBottoms.Approx(Approx(..), module Nat) where + +import ChasingBottoms.Nat +import Data.Generics +import qualified List + +-- For testing: +import ChasingBottoms.IsBottom +import ChasingBottoms.SemanticOrd + +{-| +'Approx' is a class for approximation functions as described +in The generic approximation lemma, Graham Hutton and Jeremy +Gibbons, Information Processing Letters, 79(4):197-201, Elsevier +Science, August 2001, . + +Instances are provided for all members of the 'Data' type class. Note +that the implementation is only guaranteed to perform correctly (with +respect to the paper) on polynomial datatypes; in particular, nested +or mutually recursive types are not handled correctly. + +In practice the 'approxAll' function can probably be more useful than +'approx'. It traverses down /all/ subterms, and it should be possible +to prove a variant of the approximation lemma which 'approxAll' +satisfies. +-} + +class Approx a where + -- | @'approxAll' n x@ traverses @n@ levels down in @x@ and replaces all + -- values at that level with bottoms. + approxAll :: Nat -> a -> a + + -- | 'approx' works like 'approxAll', but the traversal and + -- replacement is only performed at subterms of the same monomorphic + -- type as the original term. For polynomial datatypes this is + -- exactly what the version of @approx@ described in the paper above + -- does. + approx :: Nat -> a -> a + +instance Data a => Approx a where + approxAll = approxAllGen + approx = approxGen + +-- From The generic approximation lemma (Hutton, Gibbons): + +-- Generic definition for arbitrary datatype \mu F: +-- approx (n+1) = in . F (approx n) . out + +-- Approximation lemma (valid if F is locally continuous), +-- for x, y :: \mu F: +-- x = y <=> forall n in Nat corresponding to natural numbers. +-- approx n x = approx n y + +approxGen :: Data a => Nat -> a -> a +approxGen n | n == 0 = error "approx 0 = _|_" + | otherwise = + \(x :: a) -> gmapT (mkT (approxGen (pred n) :: a -> a)) x + +-- We use mkT to only recurse on the original type. This solution is +-- actually rather nice! But sadly it doesn't work for nested types... + +-- Note that the function is defined in the \n -> \x -> style, not +-- \n x -> which would mean something subtly different. + +------------------------------------------------------------------------ + +-- Recurses on everything... + +approxAllGen :: Data a => Nat -> a -> a +approxAllGen n | n == 0 = error "approx 0 = _|_" + | otherwise = \x -> gmapT (approxAllGen (pred n)) x + +------------------------------------------------------------------------ + +-- Behaves exactly like approxGen. (?) + +approxGen' :: Data a => Nat -> a -> a +approxGen' n + | n == 0 = error "approx 0 = _|_" + | otherwise = \x -> + let d = dataTypeOf x + n' = pred n + fun childTerm = if dataTypeOf childTerm == d then + approxGen' n' childTerm + else + childTerm + in gmapT fun x + +instance Eq DataType where + d1 == d2 = dataTypeCons d1 =|= dataTypeCons d2 + +-- (=|=) implements equality on unordered lists. It is comparable in +-- efficiency to (==) if the two lists are equal as lists. +(=|=) :: Eq a => [a] -> [a] -> Bool +xs =|= ys = case xs of + [] -> null ys + x:xs' -> if x `elem` ys then + xs' =|= List.delete x ys + else + False + +------------------------------------------------------------------------ +-- Tests + +-- Improve the testing here. (Use QuickCheck when there is some proper +-- infrastructure for testing bottoms and infinite stuff. Hmm... This +-- module is part of that infrastructure, so be careful.) + +data Tree = L | B Tree Tree deriving (Typeable, Data) + +leftInfinite = B leftInfinite L +twoLevels = B (B bottom bottom) L +threeLevels = B (B (B bottom bottom) L) L + +data PerfectTree t = PL t | PB (PerfectTree (t, t)) + deriving (Show, Typeable, Data) + +pTree :: PerfectTree Int +pTree = PB (PB (PL ((1, 2), (3, 4)))) + +-- Full form of PerfectTree: PT A = Lift (A + PT (Lift (A x A))). +-- Define F G A = Lift (A + G (Lift (A x A))). + +type F g a = Either a (g (a, a)) + +-- Assume that F is locally continuous. We have PT = mu F = F (mu F), +-- i.e. PT a = F PT a, with operations +-- in :: F PT a -> PT a +-- out :: PT a -> F PT a +-- map :: (forall a . G a -> G' a) -> F G a -> F G' a + +in_PT :: F PerfectTree t -> PerfectTree t +in_PT x = case x of + Left t -> PL t + Right tt -> PB tt + +out_PT :: PerfectTree t -> F PerfectTree t +out_PT x = case x of + PL t -> Left t + PB tt -> Right tt + +map_PT :: (forall t . g t -> g' t) -> F g t -> F g' t +map_PT f x = case x of + Left t -> Left t + Right tt -> Right (f tt) + +-- And now we can define approx for this type: + +approx_PT :: Nat -> PerfectTree a -> PerfectTree a +approx_PT n | n == 0 = error "approx 0 == _|_" + | otherwise = in_PT . map_PT (approx_PT (pred n)) . out_PT + +-- Some types with several parameters. + +data A a b = A0 a | A1 b deriving (Typeable, Data) +data C a b = C0 (C a b) | C1 a b deriving (Typeable, Data) + +tests = + -- approx 0 = bottom. + [ approx 0 ==! (bottom :: Int -> Int) + , approx 0 ==! (bottom :: Char -> Char) + , approx 0 True ==! (bottom :: Bool) + + -- approx (Succ n) /= bottom. + , approx 1 /=! (bottom :: Int -> Int) + , approx 1 /=! (bottom :: Char -> Char) + + -- approx n descends n levels. + , approx 3 "test" ==! "tes" ++ bottom + , approx 3 "tes" ==! "tes" ++ bottom + , approx 3 "te" ==! "te" + , approx 3 "t" ==! "t" + + -- This also works for infinite and multiply branching + -- structures. + , approx 2 leftInfinite ==! twoLevels + , approx 3 leftInfinite ==! threeLevels + + -- Multiple parameter data types shouldn't pose a problem. + , approx 1 (A0 (A1 True) :: A (A Char Bool) Char) ==! A0 (A1 True) + , approx 2 (C0 (C1 'a' True)) ==! C0 (C1 'a' True) + , approx 1 (C0 (C1 'a' True)) ==! C0 bottom + + -- Multiple parameter data types shouldn't pose a problem for + -- approxAll either. + , approxAll 1 (A0 (A1 True) :: A (A Char Bool) Char) ==! A0 bottom + , approxAll 1 (C0 (C1 'a' True)) ==! C0 bottom + + -- approxAll doesn't descend only on the original type... + , approxAll 1 (Just (Just (Just True))) ==! (Just bottom) + + -- ...but approx does... + , approx 1 (Just (Just (Just True))) ==! (Just (Just (Just True))) + + -- ...more or less: + , approx 2 pTree /=! approx_PT 2 pTree + -- Note that a perfect implementation would have an equality + -- here. + ] + +testsOK = and tests + +-- Due to a staging restriction this doesn't work... +-- $(if not testsOK then fail "Tests failed." else return []) addfile ./ChasingBottoms/ApproxShow.hs hunk ./ChasingBottoms/ApproxShow.hs 1 +{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-} + +-- | Functions for converting arbitrary (non-function, partial, +-- possibly infinite) values into strings. + +module ChasingBottoms.ApproxShow(Prec, ApproxShow(..), module Nat) where + +import Data.Generics +import ChasingBottoms.IsBottom +import ChasingBottoms.Nat +import ChasingBottoms.IsType +import qualified List + +-- | Precedence level. +type Prec = Int + +class ApproxShow a where + -- | @'approxShowsPrec' n@ works like 'showsPrec' with the following + -- differences: + -- + -- * After @n@ levels of descent into a term the output is + -- replaced by @\"_\"@. + -- + -- * All detectable occurences of bottoms are replaced by @\"_|_\"@. + -- + -- * Functions are displayed as @\"\\"@. + approxShowsPrec :: Nat -> Prec -> a -> ShowS + approxShows :: Nat -> a -> ShowS + approxShow :: Nat -> a -> String + + approxShows n a = approxShowsPrec n 0 a + approxShow n a = approxShowsPrec n 0 a "" + +instance Data a => ApproxShow a where + approxShowsPrec n p = gShowsPrec False n p + +-- This is a gigantic hack (due to special treatment of lists and +-- strings). Now I realise how I should have written it: +-- A wrapper taking care of n == 0 and bottoms. +-- A generic case treating ordinary data types plus tuples and functions. +-- Type specific extensions for lists and strings. +-- I doubt that it's possible to have a type specific extension that +-- works for all list types, though. +-- +-- Anyway, I don't have time improving this right now. All tests are +-- OK, so this should be fine. + +gShowsPrec :: Data a => Bool -> Nat -> Prec -> a -> ShowS +gShowsPrec insideList n p (a :: a) + | n == 0 = showString "_" + | isBottom a = showString "_|_" + | isFunction a = showString "" + | isTuple a = showParen True $ drive $ + List.intersperse (showString ", ") $ + (continueR (:) [] minPrec a) + | isString a && isAtom a = when' (not insideList) (showString "\"") $ + showString "\"" -- End of string. + | isString a = when' (not insideList) (showString "\"") $ + gmapQr (.) id + ( id -- Dummy. + `mkQ` + (\c -> if n == 1 then showString "_" else + if isBottom c then showString "_|_" + else showChar c) + `extQ` + (\(a :: String) -> if n == 1 then id else + if isBottom a then showString "_|_" + else gShowsPrec True (pred n) minPrec a + ) + ) a + | isList a && isAtom a = when' (not insideList) (showString "[") $ + showString "]" -- End of list. + | isList a = when' (not insideList) (showString "[") $ + gmapQr (.) id + ( gShowsPrec False (pred n) minPrec + `extQ` + (\(a :: a) -> + if n == 1 then id + else if isBottom a then showString "_|_" + else (if not (isAtom a) then showString ", " + else id) . + gShowsPrec True (pred n) minPrec a + ) + ) a + | isInfix a = showParen (not (isAtom a) && p > appPrec) $ + -- We know that we have at least two args, + -- because otherwise we would have a function. + let (arg1:arg2:rest) = + continueR (:) [] (succ appPrec) a + in (showParen (not (null rest)) $ + arg1 .^. showCon a .^. arg2 + ) . drive rest + | otherwise = showParen (not (isAtom a) && p > appPrec) $ + showCon a . + continueL (.^.) nil (succ appPrec) a + + where + continueL f x p = gmapQl f x (gShowsPrec False (pred n) p) + continueR f x p = gmapQr f x (gShowsPrec False (pred n) p) + +drive = foldr (.) id +nil = showString "" +f .^. g = f . showChar ' ' . g +appPrec = 10 +minPrec = 0 + -- Remove the surrounding parentheses for infix constructors. + -- No, don't do that, see the Q test case below. For + -- lists it would have been correct, though. +showCon a = showString -- . (if isInfix a then tail . init else id) + $ conString $ toConstr a +isAtom a = glength a == 0 +isPrimitive a = maxConIndex (dataTypeOf a) == 0 +isInfix a = if isPrimitive a then + False + else + conFixity (toConstr a) == Infix +wrap s = \s' -> s . s' . s +when' b s = if b then (s .) else (id .) + +------------------------------------------------------------------------ +-- Tests + +data T = L | B T T deriving (Typeable, Data) + +left = B left L + +data Q a = Q a ::: a | Q deriving (Typeable, Data) + +pr n x template = do + let s = approxShow n x + putStr $ show (s == template) + putStr " |" + putStr s + putStrLn "|" + +main = do + pr 4 left "B (B (B (B _ _) L) L) L" + pr 4 (bottom :: Bool) "_|_" + pr 4 not "" + pr 4 ('a','b') "('a', 'b')" + pr 1 ('a','b') "(_, _)" + pr 4 (Q ::: 'a' ::: 'b' ::: 'c') "((Q ::: 'a') ::: 'b') ::: 'c'" + pr 2 (Q ::: 'a' ::: 'b' ::: 'c') "(_ ::: _) ::: 'c'" + pr 4 "abc" "\"abc\"" + pr 4 [True, False, False] "[True, False, False]" + pr 2 "abc" "\"a_" + pr 2 [True, False, False] "[True, _" + pr 1 "" "\"\"" + pr 1 ([] :: [Bool]) "[]" + pr 0 "" "_" + pr 0 ([] :: [Bool]) "_" + pr 4 ('a' : bottom : bottom) "\"a_|__|_" + pr 4 ('a' : bottom : bottom : []) "\"a_|__|_\"" + pr 4 [True, bottom] "[True, _|_]" + pr 4 (True : bottom : bottom) "[True, _|__|_" + pr 4 (bottom ::: bottom ::: 'b' ::: 'c') "((_|_ ::: _|_) ::: 'b') ::: 'c'" + pr 2 ('a' : bottom : bottom) "\"a_" + pr 2 [True, bottom] "[True, _" + pr 2 (True : bottom : bottom) "[True, _" + pr 2 (bottom ::: bottom ::: 'b' ::: 'c') "(_ ::: _) ::: 'c'" addfile ./ChasingBottoms/IsBottom.hs hunk ./ChasingBottoms/IsBottom.hs 1 +module ChasingBottoms.IsBottom(isBottom, bottom) where + +import Prelude hiding (catch) +import Control.Exception (catch, throw, Exception(..), evaluate) +import System.IO.Unsafe (unsafePerformIO) + +-- For testing purposes: +import System +import Array + +-- | @'isBottom' a@ returns 'False' if @a@ is distinct from bottom. If +-- @a@ equals bottom and results in an exception which is caught by +-- 'isBottom', and this exception is of a certain kind (see below), +-- then @'isBottom' a = 'True'@. +-- +-- The exceptions that yield 'True' are those that correspond to \"pure +-- bottoms\", i.e. bottoms that can originate in pure code. Assertions +-- are excluded, since their behaviour depends on compiler flags (not +-- pure, and a failed assertion should really yield an exception and +-- nothing else). The same applies to arithmetic exceptions (machine +-- dependent, except possibly for 'DivideByZero', but the value +-- infinity makes that case unclear as well). + +-- Should we use throw or throwIO below? +-- It doesn't seem to matter, and I don't think it matters, but +-- using throw won't give us any problems. + +-- Check out a discussion about evaluate around +-- http://www.haskell.org/pipermail/glasgow-haskell-users/2002-May/003393.html. + +-- From the docs: +-- evaluate undefined `seq` return () ==> return () +-- catch (evaluate undefined) (\e -> return ()) ==> return () + +isBottom :: a -> Bool +isBottom f = unsafePerformIO $ + (evaluate f >> return False) `catch` \e -> case e of + ArithException _ -> throw e + ArrayException _ -> return True + AssertionFailed _ -> throw e + AsyncException _ -> throw e + BlockedOnDeadMVar -> throw e + Deadlock -> throw e + DynException _ -> throw e + ErrorCall _ -> return True + ExitException _ -> throw e + IOException _ -> throw e + NoMethodError _ -> return True + NonTermination -> return True + PatternMatchFail _ -> return True + RecConError _ -> return True + RecSelError _ -> return True + RecUpdError _ -> return True + +-- | 'bottom' generates a bottom that is suitable for testing using +-- 'isBottom'. +bottom :: a +bottom = error "_|_" + + +------------------------------------------------------------------------ +-- Tests + +isException f = unsafePerformIO $ + (f `seq` return False) `catch` const (return True) + +bot = bot +notbot x = notbot x + +data T a = L | B (T a) (T a) deriving Eq + +-- instance Monad T where + +leftInfinite = B leftInfinite L + +infiniteRecursion = leftInfinite == leftInfinite + +data A = A { aaa :: A } | C { ccc :: A } + +tests = and + -- Basic cases. + [ isBottom bottom == True + , isBottom undefined == True + , isBottom (error "...") == True + -- This sometimes leads to a stack overflow. + -- , isBottom bot == True + + -- const bottom /= bottom. + , isBottom notbot == False + , isBottom (const bottom) == False + + -- Other types also lifted. + , isBottom (bottom, bottom) == False + , isBottom (Just bottom) == False + + -- Pattern match failure. + , isBottom (let (x, y) = bottom in x :: Bool) == True + , isBottom (let Just x = Nothing in x :: Char) == True + + -- Nonterminating, but not bottom. + , isBottom [1..] == False + + -- Missing methods. + -- Skip this test to avoid compiler warnings. + -- , (isBottom (L >> L)) == True + + -- Array stuff. + , isBottom (array (1,0) [] ! 0) == True + , isBottom (array (0,0) [] ! 0) == True + + -- Record stuff. + -- First one commented out to avoid compiler warnings. + -- , isBottom (let x = A {} in aaa x) == True + , isBottom (let x = A { aaa = x } in ccc x) == True + , isBottom (let x = A { aaa = x } in x { ccc = x }) == True + + -- Infinite recursion, no data produced, should yield stack + -- overflow... + -- Not a quick test (on some machines, anyway). And the result + -- might be optimisation dependent. + -- , isException (isBottom infiniteRecursion) == True + + -- Some other exceptions that are not caught. + , isException (isBottom (unsafePerformIO $ exitWith ExitSuccess)) == True + , isException (isBottom (1 `div` 0)) == True + ] addfile ./ChasingBottoms/IsType.hs hunk ./ChasingBottoms/IsType.hs 1 +-- | Internal helper functions. + +module ChasingBottoms.IsType( isFunction, isTuple, isList, isString ) where + +import Data.Typeable + +-- isFunction f returns True iff the top level "constructor" of f is a +-- function arrow. +isFunction :: Typeable a => a -> Bool +isFunction f = con f == con not -- TyCon is abstract. + +con :: Typeable a => a -> TyCon +con = typerepTyCon . typeOf + +-- This function is rather fragile, but should be OK. +-- The unit type is not considered to be a tuple. +isTuple :: Typeable a => a -> Bool +isTuple x = if null s then False else head s == ',' + where s = tyconString (con x) + +isString :: Typeable a => a -> Bool +isString x = isList x && typerepArgs (typeOf x) == typerepArgs (typeOf "") + +isList :: Typeable a => a -> Bool +isList x = con x == con "" + +------------------------------------------------------------------------ +-- Tests + +tests = + -- isFunction identifies functions. + [ isFunction (id :: Char -> Char) == True + , isFunction ((==) :: Char -> Char -> Bool) == True + , isFunction 'c' == False + , isFunction [not] == False + + , isTuple [not] == False + , isTuple () == False + , isTuple ('a', 'c') == True + + , isList "" == True + , isList [not] == True + , isList ('a', 'c') == False + + , isString "" == True + , isString [not] == False + , isString ('a', 'c') == False + ] + +testsOK = and tests addfile ./ChasingBottoms/Nat.hs hunk ./ChasingBottoms/Nat.hs 1 +-- | A simple implementation of natural numbers on top of 'Integer's. +-- Note that since 'Integer's are used there is no infinite natural +-- number; in other words, 'succ' is strict. +module ChasingBottoms.Nat(Nat, isSucc, fromSucc, natrec, foldN) where + +-- TODO: Proper tests. + +import Debug.QuickCheck +import Ratio ((%)) + +default (Integer) + +-- | Natural numbers. +newtype Nat = Nat { nat2int :: Integer } deriving (Eq, Ord) + +-- | @'isSucc' 0 == 'False'@, for other total natural numbers it is 'True'. +isSucc :: Nat -> Bool +isSucc (Nat 0) = False +isSucc _ = True + +-- | @'fromSucc' 0 == 'Nothing'@, @'fromSucc' (n+1) == 'Just' n@ for a +-- total natural number @n@. +fromSucc :: Nat -> Maybe Nat +fromSucc (Nat 0) = Nothing +fromSucc n = Just $ pred n + +-- 'natrec' performs primitive recursion on natural numbers. +natrec :: a -> (Nat -> a -> a) -> Nat -> a +natrec g _ (Nat 0) = g +natrec g h n = let p = pred n in h p (natrec g h p) + +-- 'foldN' is a fold on natural numbers. +foldN :: a -> (a -> a) -> Nat -> a +foldN g h = natrec g (curry $ h . snd) + +steal :: (Integer -> Integer -> Integer) -> Nat -> Nat -> Nat +steal op x y = fromInteger $ (nat2int x) `op` (nat2int y) + +instance Num Nat where + (+) = steal (+) + (*) = steal (*) + x - y = let x' = nat2int x; y' = nat2int y + in if x' < y' then + error "Nat: x - y undefined if y > x." + else + fromInteger $ x' - y' + negate = error "Nat: negate undefined." + signum n = if isSucc n then 1 else 0 + abs = id + fromInteger i | i < 0 = error "Nat: No negative natural numbers." + | otherwise = Nat i + +instance Real Nat where + toRational = (%1) . nat2int + +steal2 :: (Integer -> Integer -> (Integer, Integer)) + -> Nat -> Nat -> (Nat, Nat) +steal2 op x y = let (x', y') = (nat2int x) `op` (nat2int y) + in (fromInteger x', fromInteger y') + +instance Integral Nat where + toInteger = toInteger . fromEnum + a `quotRem` b = if b == 0 then + error "Nat: quotRem undefined for zero divisors." + else + steal2 quotRem a b + a `divMod` b = if b == 0 then + error "Nat: divMod undefined for zero divisors." + else + steal2 divMod a b + +instance Enum Nat where + toEnum = fromInteger . toInteger + fromEnum = fromInteger . nat2int + +instance Show Nat where + showsPrec _ = showString . show . nat2int + +instance Arbitrary Nat where + arbitrary = do + n <- arbitrary :: Gen Integer + return $ fromInteger $ abs n + coarbitrary n = variant (fromEnum n `mod` 2) . coarbitrary (n `div` 2) addfile ./ChasingBottoms/SemanticOrd.hs hunk ./ChasingBottoms/SemanticOrd.hs 1 +{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-} + +-- | Generic semantic equality and order. The implementation is based +-- on 'isBottom', and has the same limitations. Note that non-bottom +-- functions are not handled by any of the functions described below. + +module ChasingBottoms.SemanticOrd + ( SemanticEq(..) + , SemanticOrd(..) + , module IsBottom + ) where + +import Data.Generics +import ChasingBottoms.IsBottom +-- import Debug.QuickCheck +import ChasingBottoms.IsType +import qualified Maybe + +infix 4 =!, >!, /=! + +-- | 'SemanticEq' contains methods for testing whether two terms are +-- semantically equal. + +-- Note that we only allow a -> a -> Bool here, not a -> b -> +-- Bool. Otherwise we would allow behaviour like the following: +-- > (bottom : bottom :: [Int]) <=!! ("tr" :: String) +-- True + +class SemanticEq a where + (==!), (/=!) :: a -> a -> Bool + + (/=!) = \x y -> not (x ==! y) + +-- | 'SemanticOrd' contains methods for testing whether two terms are +-- related according to the semantic domain ordering. + +-- We can't implement compare/min/max. Possible interesting +-- variations: lub, glb :: a -> a -> Maybe a, semanticCompare :: a -> +-- a -> Maybe Ordering. + +class SemanticEq a => SemanticOrd a where + (=!), (>!) :: a -> a -> Bool + + -- | @'semanticCompare' x y@ returns 'Nothing' if @x@ and @y@ are + -- incomparable, and @'Just' o@ otherwise, where @o :: 'Ordering'@ + -- represents the relation between @x@ and @y@. + semanticCompare :: a -> a -> Maybe Ordering + + (\/!) :: a -> a -> Maybe a + -- | @x '\/!' y@ and @x '/\!' y@ compute the least upper and greatest + -- lower bounds, respectively, of @x@ and @y@ in the semantical + -- domain ordering. Note that the least upper bound may not always + -- exist. + -- This functionality was implemented just because it was + -- possible (and to provide analogues of 'max' and 'min' in the 'Ord' + -- class). If anyone finds any use for it, please let me know. + (/\!) :: a -> a -> a + + (>=!) = flip (<=!) + ( x <=! y && x /=! y + (>!) = \x y -> x >=! y && x /=! y + + semanticCompare x y | x ! y = Just GT + | otherwise = Nothing + +instance Data a => SemanticEq a where + (==!) = (==!!) + +instance Data a => SemanticOrd a where + (<=!) = (<=!!) + (/\!) = \x y -> x /\!! y + (\/!) = \x y -> x \/!! y + +------------------------------------------------------------------------ + +type Rel = (Data a, Data b) => a -> b -> Bool + +(==!!), (<=!!) :: Rel + +a ==!! b = case (isBottom a, isBottom b) of + (True, True) -> True + (False, False) -> allOK (==!!) a b + _ -> False + +a <=!! b = case (isBottom a, isBottom b) of + (True, _) -> True + (False, False) -> allOK (<=!!) a b + _ -> False + +allOK :: Rel -> Rel +allOK op a b = + -- It's really enough to test just a, since we restrict the types + -- above, but why complicate things? + if isFunction a || isFunction b then + error "The generic versions of (==!) and friends do not accept non-bottom \ + \functions." + else + a =^= b && childrenOK op a b + +-- Check top-level. Note that this test always fails for "function +-- constructors". +(=^=) :: Rel +a =^= b = toConstr a == toConstr b + +-- Check children. +childrenOK :: Rel -> Rel +childrenOK op = tmapQl (&&) True op + +------------------------------------------------------------------------ + +(/\!!) :: (Data a, Data b) => a -> b -> b +a /\!! (b :: b) = + if isBottom a || isBottom b then + bottom + else if isFunction a || isFunction b then + -- This should be possible, in some framework, but I don't know + -- how to do it just yet. + -- cast' (\x -> cast' a x /\!! cast' b x) :: b + error "/\\! does not handle non-bottom functions." + else if not (a =^= b) then + bottom + else + tmapT (/\!!) a b + +(\/!!) :: (Data a, Data b) => a -> b -> Maybe b +a \/!! (b :: b) = + case (isBottom a, isBottom b) of + (True, True) -> Just bottom + (True, False) -> Just b + (False, True) -> cast a + (False, False) + | isFunction a || isFunction b -> + -- This should be possible, in some framework, but I don't + -- know how to do it. + -- cast (\x -> cast' a x \/! cast' b x) :: Maybe b + error "\\/! does not handle non-bottom functions." + | not (a =^= b) -> Nothing + | otherwise -> tmapM (\/!!) a b + +tmkM :: (Typeable a, Typeable b, Typeable c, Monad m) => + (a -> b -> m b) -> a -> c -> m c +tmkM f x y = mkM (f x) y + +cast' :: (Typeable a, Typeable b) => a -> b +cast' = Maybe.fromJust . cast + +------------------------------------------------------------------------ + +-- TODO: Implement a comparison operator which also works for functions. + +-- GenericQ (GenericQ r) = forall a b . (Data a, Data b) => a -> b -> r + +-- tmapQl :: (r -> r -> r) -> r -> GenericQ (GenericQ r) -> GenericQ (GenericQ r) + +-- everywhere :: (forall a . Data a => a -> a) -> forall a . Data a => a -> a +-- everywhere f = f . gmapT (everywhere f) + +-- gmapT :: Data a => (forall b . Data b => b -> b) -> a -> a + +-- teverywhere :: (forall a . Data a => a -> a) -> +-- (forall a . Data a => a -> a) -> +-- forall a . Data a => a -> +-- forall a . Data a => a -> +-- a +-- teverywhere + +-- f ===! g = case (isBottom f, isBottom g) of +-- (True, True) -> property True +-- (False, False) -> forAll arbitrary $ \x -> +-- f x ==! g x +-- _ -> property False + +------------------------------------------------------------------------ +-- Tests + +tests = + [ + + -- We should check that ==! corresponds to an equivalence + -- relation, and so on for the other operators, plus test that + -- they really do what they are supposed to do. + + ] + +testsOK = and tests addfile ./ChasingBottoms/TimeOut.hs hunk ./ChasingBottoms/TimeOut.hs 1 +{-# OPTIONS -fglasgow-exts #-} + +-- | When dealing with \"hard bottoms\", i.e. non-terminating +-- computations that do not result in bottoms, the following functions +-- may be handy. + +module ChasingBottoms.TimeOut( timeOut, timeOutMicro ) where + +import Control.Concurrent +import Control.Exception +import Data.Typeable + +data WakeUp = WakeUp deriving Typeable + +-- | @'timeOut' n c@ runs @c@ for at most @n@ seconds (modulo +-- scheduling issues). If the computation terminates before that, then +-- the resulting value is returned, and otherwise 'Nothing' is returned. +timeOut :: Int -> IO a -> IO (Maybe a) +timeOut = timeOutMicro . (* 10^6) + +-- | 'timeOutMicro' takes a delay in microseconds. Note that the +-- resolution is not too great. +timeOutMicro :: Int -> IO a -> IO (Maybe a) +timeOutMicro delay io = do + id <- myThreadId + mv <- newEmptyMVar + ioThread <- forkIO $ do + a <- io + putMVar mv a + reaper <- forkIO $ do + threadDelay delay + throwDynTo id WakeUp + (fmap Just (takeMVar mv) `catchDyn` \WakeUp -> do + killThread ioThread + return Nothing) + `finally` killThread reaper }