fix infinox & ghc 7.6

Haskell/Form.hs

@@ -29,6 +29,7 @@ import Data.Map as M( Map )
 import qualified Data.Map as M
 import Data.List
 import Data.Maybe
+import Control.Monad.State
 
 import Name
 
@@ -424,6 +425,7 @@ class Symbolic a where
   free      :: a -> Set Symbol
   subterms  :: a -> Set Term
   subst'    :: Subst -> a -> Maybe a
+  occurring :: Symbol -> a -> State [Term] a
 
 {-
   symbols{| Unit |}    Unit      = S.empty
@@ -457,20 +459,31 @@ subst sub a = case subst' sub a of
 isGround :: Symbolic a => a -> Bool
 isGround x = S.null (free x)
 
+takeTerm :: Term -> State [Term] Term
+takeTerm t = do
+  ts <- get
+  case ts of
+    [] -> return t
+    (t':ts') -> do
+      put ts'
+      return t'
+
 instance Symbolic () where
-  symbols    () = S.empty
-  free       () = S.empty
-  subterms   () = S.empty
-  subst' sub () = Nothing
+  symbols     () = S.empty
+  free        () = S.empty
+  subterms    () = S.empty
+  subst' sub  () = Nothing
+  occurring s () = return ()
 
 instance (Symbolic a, Symbolic b) => Symbolic (a,b) where
-  symbols    (x,y) = symbols x `S.union` symbols y
-  free       (x,y) = free x `S.union` free y
-  subterms   (x,y) = subterms x `S.union` subterms y
-  subst' sub (x,y) =
+  symbols     (x,y) = symbols x `S.union` symbols y
+  free        (x,y) = free x `S.union` free y
+  subterms    (x,y) = subterms x `S.union` subterms y
+  subst' sub  (x,y) =
     case (subst' sub x, subst' sub y) of
       (Nothing, Nothing) -> Nothing
       (mx,      my)      -> Just (maybe x id mx, maybe y id my)
+  occurring s (x,y) = liftM2 (,) (occurring s x) (occurring s y)
 
 instance Symbolic a => Symbolic (Signed a) where
   symbols (Pos x) = symbols x
@@ -485,6 +498,9 @@ instance Symbolic a => Symbolic (Signed a) where
   subst' sub (Pos x) = Pos `fmap` subst' sub x
   subst' sub (Neg x) = Neg `fmap` subst' sub x
 
+  occurring s (Pos x) = Pos `fmap` occurring s x
+  occurring s (Neg x) = Neg `fmap` occurring s x
+
 instance Symbolic a => Symbolic [a] where
   symbols []     = S.empty
   symbols (x:xs) = symbols (x,xs)
@@ -498,23 +514,29 @@ instance Symbolic a => Symbolic [a] where
   subst' sub []     = Nothing
   subst' sub (x:xs) = uncurry (:) `fmap` subst' sub (x,xs)
 
+  occurring s [] = return []
+  occurring s (x:xs) = liftM2 (:) (occurring s x) (occurring s xs)
+
 instance (Ord a, Symbolic a) => Symbolic (Set a) where
   symbols s        = symbols (S.toList s)
   free s           = free (S.toList s)
   subterms s       = subterms (S.toList s)
   subst' sub       = (S.fromList `fmap`) . subst' sub . S.toList
+  occurring s set  = fmap S.fromList (occurring s (S.toList set))
 
 instance Symbolic Atom where
-  symbols    (s :=: t) = symbols (s,t)
-  free       (s :=: t) = free (s,t)
-  subterms   (s :=: t) = subterms (s,t)
-  subst' sub (s :=: t) = uncurry (:=:) `fmap` subst' sub (s,t)
+  symbols     (s :=: t) = symbols (s,t)
+  free        (s :=: t) = free (s,t)
+  subterms    (s :=: t) = subterms (s,t)
+  subst' sub  (s :=: t) = uncurry (:=:) `fmap` subst' sub (s,t)
+  occurring u (s :=: t) = liftM2 (:=:) (occurring u s) (occurring u t)
 
 instance Symbolic QClause where
-  symbols    (Uniq q) = symbols q
-  free       (Uniq q) = free q
-  subterms   (Uniq q) = subterms q
-  subst' sub (Uniq q) = Uniq `fmap` subst' sub q
+  symbols     (Uniq q) = symbols q
+  free        (Uniq q) = free q
+  subterms    (Uniq q) = subterms q
+  subst' sub  (Uniq q) = Uniq `fmap` subst' sub q
+  occurring s (Uniq q) = Uniq `fmap` occurring s q
 
 instance Symbolic Form where
   symbols (Atom a)      = symbols a
@@ -549,6 +571,14 @@ instance Symbolic Form where
   subst' sub (ForAll q)    = ForAll `fmap` subst' sub q
   subst' sub (Exists q)    = Exists `fmap` subst' sub q
 
+  occurring s (Atom a)      = Atom `fmap` occurring s a
+  occurring s (And xs)      = And `fmap` occurring s xs
+  occurring s (Or xs)       = Or `fmap` occurring s xs
+  occurring s (x `Equiv` y) = liftM2 Equiv (occurring s x) (occurring s y)
+  occurring s (Not x)       = Not `fmap` occurring s x
+  occurring s (ForAll q)    = ForAll `fmap` occurring s q
+  occurring s (Exists q)    = Exists `fmap` occurring s q
+
 instance Symbolic Term where
   symbols (Fun f xs) = f `S.insert` symbols xs
   symbols (Var x)    = S.singleton x
@@ -567,6 +597,11 @@ instance Symbolic Term where
   subst' sub (Fun f xs) = Fun f `fmap` subst' sub xs
   subst' sub x@(Var v)  = M.lookup v (mapp sub)
 
+  occurring s (Fun f xs) = Fun f `fmap` occurring s xs
+  occurring s x@(Var v)
+    | s == v = takeTerm x
+    | otherwise = return x
+
 instance Symbolic a => Symbolic (Bind a) where
   symbols   (Bind v a) = v `S.insert` symbols a
   free      (Bind v a) = v `S.delete` free a
@@ -630,6 +665,10 @@ instance Symbolic a => Symbolic (Bind a) where
                   ]
                 )
 
+  occurring s x@(Bind v a)
+    | s == v = return x
+    | otherwise = Bind v `fmap` occurring s a
+
 ----------------------------------------------------------------------
 -- input clauses
 

Haskell/Infinox/Auto.hs

@@ -6,7 +6,7 @@ import Name hiding (eq)
 import Data.List
 import Infinox.Conjecture
 import qualified Infinox.Symbols as Sym
-import IO
+import System.IO
 import Infinox.Util
 import Output
 

Haskell/Infinox/Classify.hs

@@ -1,7 +1,7 @@
 module Infinox.Classify where
 
-import IO
-import System (system)
+import System.IO
+import System.Process (system)
 import System.Time 
 import System.Directory (removeFile,createDirectoryIfMissing) 
 import Control.Concurrent (threadDelay)

Haskell/Infinox/Conjecture.hs

@@ -6,6 +6,7 @@ import qualified Data.Set as Set
 import Data.List
 import qualified Infinox.Symbols as Sym
 import Infinox.Types
+import Control.Monad.State 
 
 -----------------------------------------------------------------------------------------
 
@@ -34,9 +35,9 @@ existsPred s t p = existsSymbol s t (\f -> p (\x -> f [x]))
 existsSymbol :: Symbolic a => String -> a -> (([Term] -> a) -> Form) -> Form
 existsSymbol s t p = exist (Bind Sym.x (Bind Sym.y t')) (p f)
  where
-  ts     = [ Var (name (s ++ "_" ++ show i) ::: V top) | i <- [1..] ]
-  (t',_) = occurring Sym.star ts t
-  f      = \xs -> t' @@ xs
+  ts = [ Var (name (s ++ "_" ++ show i) ::: V top) | i <- [1..] ]
+  t' = evalState (occurring Sym.star t) ts
+  f  = \xs -> t' @@ xs
 
 -----------------------------------------------------------------------------------------
 

Haskell/Infinox/InjOnto.hs

@@ -3,7 +3,7 @@ module Infinox.InjOnto where
 import qualified Data.Set as S
 import System.Directory
 
-import IO
+import System.IO
 
 
 import Form
@@ -12,7 +12,7 @@ import Infinox.Generate
 import Infinox.Util
 import Infinox.Conjecture
 import Data.List
-import System (system)
+import System.Process (system)
 import qualified Infinox.Symbols as Sym
 import Infinox.Settings
 import Flags(Method(InjNotSurj,SurjNotInj))

Haskell/Infinox/Leo.hs

@@ -1,6 +1,6 @@
 module Infinox.Leo where
 
-import IO
+import System.IO
 import Infinox.Util
 import Output
 

Haskell/Infinox/Main.hs

@@ -1,6 +1,6 @@
 module Infinox.Main where
 
-import qualified Main
+import Runner
 import Flags
 import Infinox.Classify
 ---------------------------------------------------------------------------
@@ -9,7 +9,7 @@ import Infinox.Classify
 main :: IO ()
 main =
   do putStrLn "Infinox, version 1.0, 2009-07-20."
-     Main.main Infinox classifyProblem
+     runner Infinox classifyProblem
 
 ---------------------------------------------------------------------------
 -- the end.

Haskell/Infinox/Relations.hs

@@ -17,7 +17,7 @@ import Control.Monad.Reader
 import Data.List (nub)
 import Data.Set as S( Set )
 import Output
-import System (system)
+import System.Process (system)
 import qualified Data.Set as S
 
 continueRelations :: Method -> [Relation] -> Settings Result

Haskell/Infinox/Timeout.hs

@@ -31,9 +31,9 @@ import Data.Unique         (Unique, newUnique)
 import Control.Concurrent
 import Control.Concurrent.MVar
 import System.Process
+import System.Exit
 import System.Posix hiding (killProcess)
 import System.IO.Error hiding (try,catch)
-import System
 import System.IO
 
 -- An internal type that is thrown as a dynamic exception to

Haskell/Infinox/Util.hs

@@ -1,14 +1,15 @@
 module Infinox.Util where
 
-import System (system)
-import IO
+import System.Process (system)
+import System.IO
 import System.Directory
 import Infinox.Timeout
 import Infinox.Conjecture
 import Infinox.Settings
 import Data.List (isInfixOf)
 import Form
 import Flags(Method,Prover(..))
+import ParseProblem
 
 import Control.Monad.Reader
 
@@ -57,7 +58,7 @@ proveProperty method (t,r,p) = do
 									else return [] 
 
 prove prover conj provefile timeout = do   
-   h' <- try $ openFile provefile AppendMode			
+   h' <- tryIO $ openFile provefile AppendMode			
    case h' of 
       Left e -> do 
          putStrLn "Error: unable to open provefile"					
@@ -71,7 +72,7 @@ prove prover conj provefile timeout = do
 
 
 leoprove conj provefile = do
-	h' <- try $ openFile provefile AppendMode
+	h' <- tryIO $ openFile provefile AppendMode
 	case h' of 
 		Left e -> do 
 			putStrLn "Error: unable to open provefile"					
@@ -86,7 +87,7 @@ leoprove conj provefile = do
 
 equinoxprove :: String -> FilePath -> IO Bool
 equinoxprove conjecture file = do
-	h' <- try $ openFile file AppendMode
+	h' <- tryIO $ openFile file AppendMode
 	case h' of 
 		Left e -> do 
 			putStrLn "Error: unable to open provefile"					

Haskell/Infinox/Zoom.hs

@@ -1,10 +1,10 @@
 module Infinox.Zoom (zoom,shrink) where
 
-import IO
+import System.IO
 import Form
 import Infinox.Util (finiteModel)
 import Infinox.Conjecture (form2axioms)
-import Random
+import System.Random
 import Data.List
 
 -------------------------------------------------------------------------------