[Added operators that treat computations that time out as bottoms.
nad**20041022154344] {
hunk ./ChasingBottoms/SemanticOrd.hs 21
+-- Some functions take the implicit parameters @?approxDepth@ and
+-- @?timeOutLimit@. They have the following meaning:
+--
+-- [@'?approxDepth'@] If equal to @'Just' n@, an @'approxAll' n@ is
+-- performed on all arguments before doing whatever the function is
+-- supposed to be doing.
+--
+-- [@'?timeOutLimit'@] If equal to @'Just' n@, then all computations
+-- that take more than @n@ seconds to complete are considered to be
+-- equal to 'bottom'. This functionality is implemented using
+-- 'isBottomTimeOut'.
+--
hunk ./ChasingBottoms/SemanticOrd.hs 46
+import ChasingBottoms.Nat
+import ChasingBottoms.Approx
hunk ./ChasingBottoms/SemanticOrd.hs 50
+infix 4 <?, <=?, ==?, >=?, >?, /=?
hunk ./ChasingBottoms/SemanticOrd.hs 62
+  (==?), (/=?) :: ( ?approxDepth :: Maybe Nat
+                  , ?timeOutLimit :: Maybe Int
+                  ) => a -> a -> Bool
+
+  (/=?) = \x y -> not (x ==? y)
hunk ./ChasingBottoms/SemanticOrd.hs 69
+
+  (==!) = bindImpl (==?)
hunk ./ChasingBottoms/SemanticOrd.hs 77
+  (<?), (<=?), (>=?), (>?) ::
+    ( ?approxDepth :: Maybe Nat
+    , ?timeOutLimit :: Maybe Int
+    ) => a -> a -> Bool
hunk ./ChasingBottoms/SemanticOrd.hs 82
-  -- | @'semanticCompare' x y@ returns 'Nothing' if @x@ and @y@ are
+  semanticCompare :: a -> a -> Maybe Ordering
+  semanticCompare' :: ( ?approxDepth :: Maybe Nat
+                      , ?timeOutLimit :: Maybe Int
+                      ) => a -> a -> Maybe Ordering
+  -- ^ @'semanticCompare' x y@ returns 'Nothing' if @x@ and @y@ are
hunk ./ChasingBottoms/SemanticOrd.hs 89
-  semanticCompare :: a -> a -> Maybe Ordering
hunk ./ChasingBottoms/SemanticOrd.hs 92
+  (\/?) :: ( ?approxDepth :: Maybe Nat
+           , ?timeOutLimit :: Maybe Int
+           ) => a -> a -> Maybe a
+  (/\?) :: ( ?approxDepth :: Maybe Nat
+           , ?timeOutLimit :: Maybe Int
+           ) => a -> a -> a
hunk ./ChasingBottoms/SemanticOrd.hs 109
+
+  (>=?) = flip (<=?)
+  (<?)  = \x y -> x <=? y && x /=? y
+  (>?)  = \x y -> x >=? y && x /=? y
+
+  (<=!) = bindImpl (<=?)
+
+  semanticCompare = bindImpl semanticCompare'
+
+  semanticCompare' x y | x <?  y   = Just LT
+                       | x ==? y   = Just EQ
+                       | x >?  y   = Just GT
+                       | otherwise = Nothing
+
+  x <=? y = case semanticCompare' x y of
+    Just LT -> True
+    Just EQ -> True
+    _       -> False
+
+  (\/!) = bindImpl (\/?)
hunk ./ChasingBottoms/SemanticOrd.hs 130
-  semanticCompare x y | x <!  y   = Just LT
-                      | x ==! y   = Just EQ
-                      | x >!  y   = Just GT
-                      | otherwise = Nothing
+  (/\!) = bindImpl (/\?)
hunk ./ChasingBottoms/SemanticOrd.hs 133
-  (==!) = (==!!)
+  (==?) = liftAppr (==??)
hunk ./ChasingBottoms/SemanticOrd.hs 136
-  (<=!) = (<=!!)
-  (/\!)  = (/\!!)
-  (\/!)  = (\/!!)
+  (<=?) = liftAppr (<=??)
+  (/\?)  = liftAppr (/\??)
+  (\/?)  = liftAppr (\/??)
+
+liftAppr op x y = appr x `op` appr y
+  where appr = maybe id approxAll ?approxDepth
+
+-- Non-trivial type...
+
+bindImpl ::
+  (forall . (?approxDepth :: Maybe Nat, ?timeOutLimit :: Maybe Int) => a) -> a
+bindImpl f = let ?approxDepth = Nothing
+                 ?timeOutLimit = Nothing
+             in f
hunk ./ChasingBottoms/SemanticOrd.hs 153
-type Rel = (Data a, Data b) => a -> b -> Bool
+type Rel = (?timeOutLimit :: Maybe Int, Data a, Data b) => a -> b -> Bool
hunk ./ChasingBottoms/SemanticOrd.hs 155
-(==!!), (<=!!) :: Rel
+(==??), (<=??) :: Rel
hunk ./ChasingBottoms/SemanticOrd.hs 157
-a ==!! b = case (isBottom a, isBottom b) of
+a ==?? b = case (isBottomTimeOut a, isBottomTimeOut b) of
hunk ./ChasingBottoms/SemanticOrd.hs 159
-  (False, False) -> allOK (==!!) a b
+  (False, False) -> allOK (==??) a b
hunk ./ChasingBottoms/SemanticOrd.hs 162
-a <=!! b = case (isBottom a, isBottom b) of
+a <=?? b = case (isBottomTimeOut a, isBottomTimeOut b) of
hunk ./ChasingBottoms/SemanticOrd.hs 164
-  (False, False) -> allOK (<=!!) a b
+  (False, False) -> allOK (<=??) a b
hunk ./ChasingBottoms/SemanticOrd.hs 189
-(/\!!) :: (Data a, Data b) => a -> b -> b
-a /\!! (b :: b) =
-  if isBottom a || isBottom b then
+(/\??) :: (?timeOutLimit :: Maybe Int, Data a, Data b) => a -> b -> b
+a /\?? (b :: b) =
+  if isBottomTimeOut a || isBottomTimeOut b then
hunk ./ChasingBottoms/SemanticOrd.hs 198
-    tmapT (/\!!) a b
+    tmapT (/\??) a b
hunk ./ChasingBottoms/SemanticOrd.hs 200
-(\/!!) :: (Data a, Data b) => a -> b -> Maybe b
-a \/!! (b :: b) =
-  case (isBottom a, isBottom b) of
+(\/??) :: (?timeOutLimit :: Maybe Int, Data a, Data b) => a -> b -> Maybe b
+a \/?? (b :: b) =
+  case (isBottomTimeOut a, isBottomTimeOut b) of
hunk ./ChasingBottoms/SemanticOrd.hs 210
-      | otherwise                    -> tmapM (\/!!) a b
+      | otherwise                    -> tmapM (\/??) a b
}