-- TODO : deep binding of downarrow -- TODO : Maximum depth exceded (check arguments prob=0 => maxdepth=0) -- TODO : Whe one operator reaches maximum depth we distribute its probability -- to the other operators. Other possibility is to also increase the probability -- of atoms. -- TODO : We are not checking for repeated clauses. We may have to come up with a normal form -- that sorts the atoms, or maybe reuse the trie functions module Main (main) where import Debug.Trace(trace) import System.Random(StdGen,randomR,newStdGen) import Control.Monad.State(get,put,State,evalState) import Control.Monad(unless) import qualified HyLo.Formula as F (Formula(..)) import System.Environment( getProgName ) import Prelude hiding ( mod ) import Data.Version ( showVersion ) import Paths_hgen ( version ) import Params data Formula = Fprop Int | Fnom Int | Fvar Int | Fnot Formula | Fand [Formula] | For [Formula] | Fbox Int Formula | Fubox Formula | Fdubox Formula | Fibox Int Formula | Fat Int Formula | Fatv Int Formula | Fdown Int Formula deriving Show data Shape = Shp Int [Shape] deriving Show -- probsOp : Given the set of parameters (which varies as the formula grows) -- it returns the probability of appearance for every operator -- TODO:Downarrow requires another operator as argument: if we run out, no downarrow. -- This can cause downarrow depth problems! probsOp :: Params -> [Int] probsOp p = let dzero x = if x==0 then 0 else 1 in if not (forceDepths p) then [dzero (mdepth p) * pmod p, dzero (atdepth p) * pat p, dzero (dwdepth p) * pdown p, dzero (umdepth p) * puniv p, dzero (dumdepth p) * pduniv p, dzero (invdepth p) * pinv p] else [pmod p, pat p, pdown p, pduniv p, pinv p] -- probsProp : Given the set of parameters (which varies as the -- formula grows) and a list of atoms, it returns the probability of an -- atom of being of each type, the probability being zero if all the -- possible different atoms of that type are already present on the list probsProp :: Params -> [Formula] -> [Int] -> [Int] probsProp p flist vlist = let dzero x = if x<=0 then 0 else 1 stillPs = dzero $ (pvars p) - (sum $ map hmpro flist) stillNs = dzero $ (nomvars p) - (sum $ map hmnom flist) stillVs = dzero $ (length vlist) - (sum $ map isVar flist) in [ pprop p * stillPs, pnom p * stillNs, psvar p * stillVs] main :: IO () main = do p <- getParams case p of Left err -> do putStrLn header putStrLn err progName <- getProgName putStrLn $ "Try `" ++ progName ++ " --help' " ++ "for more information" return () -- Right params -> if showHelp params then do putStrLn header progName <- getProgName putStrLn $ usage (progName ++ " [OPTIONS]") putStrLn gplTag return () -- else runWithParams params runWithParams :: Params -> IO () runWithParams params = do unless (hidesummary params) $ putStr $ "Setting the following parameters:\n" ++ show params frmList <- evalState (generateFormulaList (numinst params) params) `fmap` newStdGen let output = if stdout params then putStrLn . unwords else writeList (getName params) (numinst params) output $ if simpleFormat params then frmList else map ("signature { automatic }\n\ntheory" ++) frmList getName :: Params -> String getName params = "hcnf" ++ "C" ++ show (numclauses params) ++ "-" ++ "S" ++ show (csize params) ++ "-" ++ "M" ++ show (mods params) ++ "-" ++ "GD" ++ show (gdepth params) ++ "-" ++ -- "@D" ++ show (atdepth params) ++ "-" ++ -- "DD" ++ show (dwdepth params) ++ "-" ++ -- "UD" ++ show (umdepth params) ++ "-" ++ -- "ID" ++ show (invdepth params) ++ "-" ++ "NP" ++ show (pvars params) ++ "-" ++ "NN" ++ show (nomvars params) ++ "-" ++ "NS" ++ show (stvars params) header :: String header = unlines ["hgen " ++ showVersion version, "C. Areces, D. Gorin, G. Hoffmann and J. Heguiabehere. (c) 2002-2009."] gplTag :: String gplTag = unlines [ "This program is distributed in the hope that it will be useful,", "but WITHOUT ANY WARRANTY; without even the implied warranty of", "MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the", "GNU General Public License for more details."] {- choose: Given - a list of natural numbers l - an integer n in [1:100] returns the index in l corresponding to n, when we consider l as a probability distribution and n is a random number -} choose :: [Int] -> Int -> Int choose l n = let select arg@(what,idx) here | what<=0 = arg | here>=what = (0,idx) | otherwise = (what-here,idx+1) maxProb = sum l indexValue = ceiling $ fromIntegral (n * maxProb) * (0.01::Double) in snd $ foldl select (indexValue,1) l {- genShape: Given the number of disjuncts wanted, the remaining depth to go, and the current set of parameters, it returns a list of structures (shapes) containing - the number of atoms - a list of arguments for operators (also shapes) -} genShape:: Int -> Int -> Params -> State StdGen [Shape] genShape 0 _ _ = return [] genShape n 0 p = do r <- nextR let numDisj = choose (csize p) r rest <- genShape (n-1) 0 p return $ (Shp numDisj []):rest genShape n maxdepth p = do r <- nextR r2 <- nextR let numDisj = choose (csize p) r let pc = fromIntegral (pop p * numDisj) * (0.01::Double) let floorpc = floor pc let ceilingpc = ceiling pc let numProps = if floorpc == ceilingpc || ((fromIntegral r2 * 0.01) < (fromIntegral ceilingpc - pc)) then floorpc else ceilingpc rest <- genShape (n-1) maxdepth p restint <- genShape (numDisj - numProps) (maxdepth-1) p return $ (Shp numProps restint):rest {- genDisjunct : Given a shape, the current set of parameters, a list of available variables and an atom, it chooses the atoms and the operators to fill the shape and turn it into a formula, which will not include said atom in its top level -} genDisjunct:: Shape -> Params -> [Int] -> Formula -> State StdGen Formula genDisjunct (Shp nump sh) p l bannedAtom = let end = sum (probsOp p) == 0 finalnump = if end then nump + length sh else nump finalsh = if end then [] else sh in do props <- genProp finalnump p l bannedAtom ops <- genOps finalsh p l return $ For (props++ops) {- genProp : given the number of atoms wanted, the set of parameters the available variables, and an atom which is not allowed, it returns the required number of atoms -} genProp :: Int -> Params -> [Int] -> Formula -> State StdGen [Formula] genProp 0 _ _ _ = return [] genProp nump p vlist bannedAtom = do rn <- nextR rn2 <- nextR res <- genProp (nump-1) p vlist bannedAtom posVar <- nextRn $ length vlist let probs = probsProp p res vlist -- only symbols for available categories if sum probs == 0 then return (trace "Too few atomic symbols!!\n" res) else case choose probs rn of -- [prop, nom, svar] 1 -> do let avail = takeUsedP (replicate (pvars p) 1) (bannedAtom:res) let prop = choose avail rn2 f <- randNeg (Fprop prop) (pneg p) return (f:res) 2 -> do let avail = takeUsedN (replicate (nomvars p) 1) (bannedAtom:res) let nom = choose avail rn2 f <- randNeg (Fnom nom) (pneg p) return (f:res) 3 -> do let avail = takeUsedV (addPresent (replicate (stvars p) 0) vlist) (bannedAtom:res) let var = if all (== 0) avail then vlist !! (posVar - 1) else choose avail rn2 f<- randNeg (Fvar var) (pneg p) return (f:res) _ -> error "genProp" -- takeUsedP : Removes from the bitmap of all possible proposition symbols those already used takeUsedP :: [Int] -> [Formula] -> [Int] takeUsedP l [] = l takeUsedP l (Fprop n:fl) = takeUsedP ( take (n-1) l ++(0:drop n l)) fl takeUsedP l (Fnot (Fprop n):fl) = takeUsedP ( take (n-1) l ++ (0:drop n l)) fl takeUsedP l (_:fl) = takeUsedP l fl -- takeUsedN : Removes from the bitmap of all possible nominals those already used takeUsedN :: [Int] -> [Formula] -> [Int] takeUsedN l [] = l takeUsedN l (Fnom n:fl) = takeUsedN ( take (n-1) l ++(0:drop n l)) fl takeUsedN l (Fnot (Fnom n):fl) = takeUsedN (take (n-1) l ++(0:drop n l)) fl takeUsedN l (_:fl) = takeUsedN l fl -- takeUsedV : Removes from the bitmap of all possible variables symbols those already used takeUsedV :: [Int] -> [Formula] -> [Int] takeUsedV l [] = l takeUsedV l (Fvar n:fl) = takeUsedV (take (n-1) l ++(0:drop n l)) fl takeUsedV l (Fnot (Fvar n):fl) = takeUsedV (take (n-1) l ++(0:drop n l)) fl takeUsedV l (_:fl) = takeUsedV l fl remove :: [Int] -> [Int] -> [Int] remove l [] = l remove list (n:nl) = remove ( take (n-1) list ++ (0:drop n list)) nl -- addPresent : Adds to a bitmap addPresent :: [Int] -> [Int] -> [Int] addPresent l [] = l addPresent list (n:l) = if n==0 || n > length list then addPresent list l else addPresent ( take (n-1) list ++ (1:drop n list)) l -- genOps : Given a list of shapes (formula structures), returns the -- formulas resulting from filling in the blanks in the shapes. genOps :: [Shape] -> Params -> [Int] -> State StdGen [Formula] genOps [] _ _ = return [] genOps sh@(s:shapes) p vlist = do rn <- nextR rn2 <- nextR posVar <- nextRn $ length vlist let probs = probsOp p if sum probs == 0 then return [] else case choose probs rn of 1 -> do -- BOX Case let p' = p{mdepth = mdepth p -1} orform <- genDisjunct s p' vlist (For []) mod <- nextRn (mods p) f <- randNeg (Fbox mod orform) (pneg p) res <- genOps shapes p' vlist return (f:res) 2 -> do -- AT Case let p' = p{atdepth = atdepth p -1} nom <- nextRn (nomvars p) chanceV' <- nextR let chanceV = if (pnom p == 0) || (nomvars p == 0) then 100 else chanceV' let atV = (pdown p /= 0) && (chanceV > 50) let avail = addPresent (replicate (stvars p) 0) vlist let var = if all (== 0) avail then vlist !! (posVar - 1) else choose avail rn2 let forbAtom = if atV && (sum avail /= 0) then Fvar var else Fnom nom let orf = genDisjunct s p' vlist forbAtom if atV && (sum avail /= 0) then do orform <- orf f <- randNeg (Fatv var orform) (pneg p) res <- genOps shapes p' vlist return (f:res) else if not ((pnom p == 0) || (nomvars p == 0)) then do orform <- orf f <- randNeg (Fat nom orform) (pneg p) res <- genOps shapes p' vlist return (f:res) else genOps sh p vlist 3 -> do -- DOWN Case -- the generation of \down x.\down y. is allowed let p' = p{dwdepth = dwdepth p - 1} let avail = remove (replicate (stvars p) 1) vlist let var = choose avail rn2 orform <- genDisjunct s p' (var:vlist) (For []) f <- randNeg (Fdown var orform) (pneg p) res <- genOps shapes p' vlist return (f:res) 4 -> do -- UNIV Case let p' = p{umdepth = umdepth p - 1} orform <- genDisjunct s p' vlist (For []) f <- randNeg (Fubox orform)(pneg p) res <- genOps shapes p' vlist return (f:res) 5 -> do -- DIFF UNIV Case let p' = p{dumdepth = dumdepth p - 1} orform <- genDisjunct s p' vlist (For []) f <- randNeg (Fdubox orform)(pneg p) res <- genOps shapes p' vlist return (f:res) 6 -> do -- INV Case let p' = p{invdepth = invdepth p - 1} orform <- genDisjunct s p' vlist (For []) mod <- nextRn (mods p) f <- randNeg (Fibox mod orform) (pneg p) res <- genOps shapes p' vlist return (f:res) other -> error $ "Operator unknown: " ++ show other randNeg:: Formula -> Int -> State StdGen Formula randNeg f n = do rn <- nextR return $ if n > rn then f else Fnot f genDisjunctList :: [Shape] -> Params -> State StdGen [Formula] genDisjunctList [] _ = return [] genDisjunctList (s:shapes) p = do disj <- genDisjunct s p [] (For []) rdisj <- genDisjunctList shapes p return (disj:rdisj) generateFormula :: Params -> State StdGen String generateFormula p = do shapes <- genShape (numclauses p) (gdepth p) p gd <- genDisjunctList shapes p newf <- mapM (sanitize2 p) gd return $ write p $ map toHyLoFormula newf hmpro :: Formula -> Int hmpro (Fprop _) = 1 hmpro (Fnom _) = 0 hmpro (Fvar _) = 0 hmpro (Fnot f) = hmpro f hmpro (Fubox f) = hmpro f hmpro (Fdubox f) = hmpro f hmpro (For fl) = sum (map hmpro fl) hmpro (Fbox _ f) = hmpro f hmpro (Fat _ f) = hmpro f hmpro (Fatv _ f) = hmpro f hmpro (Fdown _ f) = hmpro f hmpro _ = error "hmpro" hmnom :: Formula -> Int hmnom (Fprop _) = 0 hmnom (Fnom _) = 1 hmnom (Fvar _) = 0 hmnom (Fnot f) = hmnom f hmnom (Fubox f) = hmnom f hmnom (Fdubox f) = hmnom f hmnom (For fl) = sum (map hmnom fl) hmnom (Fbox _ f) = hmnom f hmnom (Fat _ f) = hmnom f hmnom (Fatv _ f) = hmnom f hmnom (Fdown _ f) = hmnom f hmnom _ = error "hmnom" hmat :: Formula -> Int hmat (Fprop _) = 0 hmat (Fnom _) = 0 hmat (Fvar _) = 0 hmat (Fnot f) = hmat f hmat (Fubox f) = hmat f hmat (Fdubox f) = hmat f hmat (For fl) = sum (map hmat fl) hmat (Fbox _ f) = hmat f hmat (Fat _ f) = 1 + hmat f hmat (Fatv _ f) = hmat f hmat (Fdown _ f) = hmat f hmat _ = error "hmat" -- isVar:: Whether an atom is a state variable (1 if yes, 0 if no) isVar :: Formula -> Int isVar (Fvar _) = 1 isVar (Fnot (Fvar _)) = 1 isVar _ = 0 -- If a variable at a downarrow operator does not appear -- in the scope, a prop. variable, nominal, or at is changed sanitize2 :: Params -> Formula -> State StdGen Formula sanitize2 p (Fdown n f) = if looseVar n f then do rn <- nextR let c = [hmpro f, hmnom f, hmat f] let nz x = if x == 0 then 0 else 1 let nzc = map nz c let ch = choose nzc rn rnp <- nextRn (c!!0) rnn <- nextRn (c!!1) rna <- nextRn (c!!2) case ch of 1 -> return (Fdown n (changeProp rnp n f)) 2 -> return (Fdown n (changeNom rnn n f)) 3 -> return (Fdown n (changeAt rna n f)) _ -> error "sanitize2" else Fdown n `fmap` sanitize2 p f sanitize2 p (Fnot f) = Fnot `fmap` sanitize2 p f sanitize2 p (Fubox f) = Fubox `fmap` sanitize2 p f sanitize2 p (Fdubox f) = Fdubox `fmap` sanitize2 p f sanitize2 p (Fibox n f)= Fibox n `fmap` sanitize2 p f sanitize2 p (Fbox n f) = Fbox n `fmap` sanitize2 p f sanitize2 p (Fat n f) = Fat n `fmap` sanitize2 p f sanitize2 p (Fatv n f) = Fatv n `fmap` sanitize2 p f sanitize2 p (For fl) = For `fmap` mapM (sanitize2 p) fl sanitize2 _ f = return f looseVar :: Int -> Formula -> Bool looseVar n f = n `notElem` listVars f listVars :: Formula -> [Int] listVars (Fprop _) = [] listVars (Fnom _) = [] listVars (Fvar n) = [n] listVars (Fnot f) = listVars f listVars (Fubox f) = listVars f listVars (Fdubox f) = listVars f listVars (Fibox _ f) = listVars f listVars (For fl) = concatMap listVars fl listVars (Fbox _ f) = listVars f listVars (Fat _ f) = listVars f listVars (Fatv n f) = n:listVars f listVars (Fdown _ f) = listVars f listVars _ = error "listVars" changeProp :: Int -> Int -> Formula -> Formula changeProp _ n (Fprop _) = Fvar n changeProp _ _ (Fnom n) = Fnom n changeProp _ _ (Fvar n) = Fvar n changeProp pos n (Fnot f) = Fnot (changeProp pos n f) changeProp pos n (Fbox m f) = Fbox m (changeProp pos n f) changeProp pos n (Fubox f) = Fubox (changeProp pos n f) changeProp pos n (Fdubox f) = Fdubox (changeProp pos n f) changeProp pos n (Fibox m f) = Fibox m (changeProp pos n f) changeProp pos n (Fat m f) = Fat m (changeProp pos n f) changeProp pos n (Fatv m f) = Fatv m (changeProp pos n f) changeProp pos n (Fdown m f) = Fdown m (changeProp pos n f) changeProp pos n (For [f1]) = For [changeProp pos n f1] changeProp pos n (For (f1:(f2:fl))) | hmpro f1 < pos = For (f1:[changeProp (pos - hmpro f1) n (For (f2:fl))]) | otherwise = For (changeProp pos n f1:(f2:fl)) changeProp _ _ _ = error "changeProp" changeNom :: Int -> Int -> Formula -> Formula changeNom _ n (Fnom _) = Fvar n changeNom _ _ (Fprop n) = Fprop n changeNom _ _ (Fvar n) = Fvar n changeNom pos n (Fnot f) = Fnot (changeNom pos n f) changeNom pos n (Fbox m f) = Fbox m (changeNom pos n f) changeNom pos n (Fubox f) = Fubox (changeNom pos n f) changeNom pos n (Fdubox f) = Fdubox (changeNom pos n f) changeNom pos n (Fibox m f) = Fibox m (changeNom pos n f) changeNom pos n (Fat m f) = Fat m (changeNom pos n f) changeNom pos n (Fatv m f) = Fatv m (changeNom pos n f) changeNom pos n (Fdown m f) = Fdown m (changeNom pos n f) changeNom pos n (For [f1]) = For [changeNom pos n f1] changeNom pos n (For (f1:(f2:fl))) | hmnom f1 < pos = For (f1:[changeNom (pos - hmnom f1) n (For (f2:fl))]) | otherwise = For (changeNom pos n f1:(f2:fl)) changeNom _ _ _ = error "changeNom" changeAt :: Int -> Int -> Formula -> Formula changeAt _ _ (Fnom n) = Fvar n changeAt _ _ (Fprop n) = Fprop n changeAt _ _ (Fvar n) = Fvar n changeAt pos n (Fnot f) = Fnot (changeAt pos n f) changeAt pos n (Fbox m f) = Fbox m (changeAt pos n f) changeAt pos n (Fubox f) = Fubox (changeAt pos n f) changeAt pos n (Fdubox f) = Fdubox (changeAt pos n f) changeAt pos n (Fibox m f) = Fibox m (changeAt pos n f) changeAt _ n (Fat _ f) = Fatv n f changeAt pos n (Fatv m f) = Fatv m (changeAt pos n f) changeAt pos n (Fdown m f) = Fdown m (changeAt pos n f) changeAt pos n (For [f1]) = For [changeAt pos n f1] changeAt pos n (For (f1:(f2:fl))) | hmat f1 < pos = For (f1:[changeAt (pos - hmat f1) n (For (f2:fl))]) | otherwise = For (changeAt pos n f1:(f2:fl)) changeAt _ _ _ = error "changeAt" generateFormulaList :: Int -> Params -> State StdGen [String] generateFormulaList 0 _ = return [] generateFormulaList n p = do frm <- generateFormula p lfrm <- generateFormulaList (n-1) p return (frm:lfrm) -- writeList : Given a filename, and a list of strings, -- writes the strings to a file with that name writeList :: String -> Int -> [String] -> IO () writeList _ _ [] = return () writeList fname n (f:fl) = do writeFile (fname ++ "." ++ show n ++ ".cnf") f writeList fname (n-1) fl -- nextR : Returns a fresh random number, range 1-100 nextR :: State StdGen Int nextR = do gen <- get let (num, newgen) = randomR (1,100) gen put newgen return num -- nextR : Returns a fresh random number, range 1-n nextRn :: Int -> State StdGen Int nextRn n = do gen <- get let (num, newgen) = randomR (1,n) gen put newgen return num type HyLoFormula = F.Formula NomSymbol PropSymbol RelSymbol toHyLoFormula :: Formula -> HyLoFormula toHyLoFormula (Fprop v) = F.Prop (PropSymbol v) toHyLoFormula (Fnom v) = F.Nom (NomSymbol v) toHyLoFormula (Fvar v) = F.Nom (NomSymbol v) toHyLoFormula (Fand fs) = foldr1 (F.:&:) $ map toHyLoFormula fs toHyLoFormula (For fs) = foldr1 (F.:|:) $ map toHyLoFormula fs toHyLoFormula (Fnot f) = F.Neg $ toHyLoFormula f toHyLoFormula (Fubox f) = F.A $ toHyLoFormula f toHyLoFormula (Fdubox f) = F.D $ toHyLoFormula f toHyLoFormula (Fbox i f) = F.Box (RelSymbol i) $ toHyLoFormula f toHyLoFormula (Fibox i f) = F.Box (InvRelSymbol i) $ toHyLoFormula f toHyLoFormula (Fat i f) = F.At (NomSymbol i) $ toHyLoFormula f toHyLoFormula (Fatv i f) = F.At (NomSymbol i) $ toHyLoFormula f toHyLoFormula (Fdown i f) = F.Down (NomSymbol i) $ toHyLoFormula f -- special signature so that formulas are printed with N1, P1 and R1 names newtype PropSymbol = PropSymbol Int deriving(Eq, Ord) instance Show PropSymbol where show (PropSymbol i) = 'P':show i newtype NomSymbol = NomSymbol Int deriving(Eq, Ord) instance Show NomSymbol where show (NomSymbol i) = 'N':show i data RelSymbol = RelSymbol Int | InvRelSymbol Int deriving(Eq, Ord) instance Show RelSymbol where show (RelSymbol i) = 'R' : show i show (InvRelSymbol i) = "-R" ++ show i write :: Params -> [HyLoFormula] -> String write params input = unlines $ beginMark:addSemicolon (map show input) ++ [endMark] where addSemicolon (x:xs@(_:_)) = (x ++ ";") : addSemicolon xs addSemicolon xs = xs (beginMark,endMark) = if simpleFormat params then ("begin","end") else ("{","}")