diff --git a/hgen.cabal b/hgen.cabal --- a/hgen.cabal +++ b/hgen.cabal @@ -1,5 +1,6 @@ +cabal-version: 2.0 Name: hgen -Version: 1.4.0 +Version: 1.5.0 Synopsis: Random generation of modal and hybrid logic formulas Description: Random generation of modal and hybrid logic formulas Category: Theorem Provers @@ -9,7 +10,6 @@ Maintainer: areces@loria.fr Homepage: http://www.glyc.dc.uba.ar/intohylo/hgen.php Build-type: Simple -Cabal-version: >= 1.6 Flag static Description: Build a static binary @@ -18,14 +18,18 @@ Executable hgen Main-is: hgen.hs other-modules: Params + Paths_hgen + autogen-modules: + Paths_hgen hs-source-dirs: src - ghc-options: -Wall + ghc-options: -O2 -Wall -rtsopts Build-Depends: base >= 4, base < 5, random >= 1, random < 2, mtl >= 2, mtl < 3, - filepath >= 1, filepath < 2, - directory >= 1, directory < 2, - hylolib == 1.4.* + hylolib >= 1.5, + cmdargs >= 0.10.14 + default-language: Haskell2010 + default-extensions: DeriveDataTypeable if flag(static) ghc-options: -static -optl-static -optl-pthread diff --git a/src/Params.hs b/src/Params.hs --- a/src/Params.hs +++ b/src/Params.hs @@ -1,291 +1,71 @@ +{-# OPTIONS_GHC -fno-warn-missing-fields #-} module Params where -import System.Console.GetOpt ( OptDescr(..), ArgDescr(..), ArgOrder(..), - getOpt, usageInfo ) -import Control.Monad.Error (MonadError(..)) -import Control.Applicative ( (<$>) ) -import System.Directory ( getHomeDirectory, doesFileExist ) -import System.FilePath ( () ) -import System.Environment ( getArgs ) - - - -getParams :: IO (Either ParsingErrMsg Params) -getParams = - do let clp_0 = defaultParams - m_rcfile <- findRc - parse_clp_1 <- case m_rcfile of - Nothing -> return $ return clp_0 - Just f -> do rc_args <- words <$> readFile f - return $ parseCmds rc_args clp_0 - `catchError` - (\e -> fail $ f ++ ":\n" ++ e) - -- - cmdline_args <- getArgs - -- - return $ do clp_1 <- parse_clp_1 - parseCmds cmdline_args clp_1 - - - -rcfile :: FilePath -rcfile = ".hgenrc" - - -findRc :: IO (Maybe FilePath) -findRc = - do existsInCurrent <- doesFileExist rcfile - if existsInCurrent - then return (Just rcfile) - else do - home <- getHomeDirectory - let inHome = home rcfile - -- - existsInHome <- doesFileExist inHome - if existsInHome then return (Just inHome) else return Nothing - - -usage :: String -> String -usage header = unlines [ - usageInfo header options, - "", - "If a file called `" ++ "." rcfile ++ "' or `" ++ "~" rcfile - ++ "' exists, it will be scanned for arguments first" - ] - - -type ParamsModifier = Params -> Either ParsingErrMsg Params -type ParsingErrMsg = String - -parseCmds :: [String] -> Params -> Either ParsingErrMsg Params -parseCmds argv params = - case getOpt RequireOrder options argv of - (pMods, [], []) -> thread pMods params - ( _, unk, []) -> fail $ "Unknown option: " ++ unwords unk - ( _, _,errs) -> fail $ unlines errs - - -thread :: Monad m => [a -> m a] -> a -> m a -thread = foldr (\f g -> \a -> f a >>= g) return - -options :: [OptDescr ParamsModifier] -options = - [Option ['h','?'] - ["help"] - (NoArg $ \p -> return p{showHelp = True}) - "display this help and exit", - Option ['H'] - ["hide-summary"] - (NoArg $ \p -> return p{hidesummary = True}) - "hide summary of the options used", - Option ['#'] - ["num-inst"] - (ReqArg ((not . null) ?-> \s p -> return p{numinst = read s}) "INT") - "number of formulas to generate", - Option ['c'] - ["num-clauses"] - (ReqArg ((not . null) ?-> \s p -> return p{numclauses = read s}) "INT") - "number of clauses per formula", - Option [] - ["clause-size"] - (ReqArg ((not . null) ?-> \s p -> return p{csize = read s}) "[INT]") - "size of a clause (ie [1,1,1] means same chance for length 1,2 or 3)", - Option [] - ["mods"] - (ReqArg ((not . null) ?-> \s p -> return p{mods = read s}) "INT") - "number of modalities", - Option [] - ["global-depth"] - (ReqArg ((not .null) ?-> \s p -> return p{gdepth = read s}) "INT") - "global (maximum) depth", - Option [] - ["force-depths"] - (NoArg $ \p -> return p{forceDepths = True}) - "wether or not to impose strict maximum depth per operator", - Option [] - ["modal-depth"] - (ReqArg ((not . null) ?-> \s p -> return p{mdepth = read s}) "INT") - "modal depth", - Option [] - ["at-depth"] - (ReqArg ((not . null) ?-> \s p -> return p{atdepth = read s}) "INT") - "@ depth", - Option [] - ["down-arrow-depth"] - (ReqArg ((not . null) ?-> \s p -> return p{dwdepth = read s}) "INT") - "down arrow depth", - Option [] - ["univ-mod-depth"] - (ReqArg ((not . null) ?-> \s p -> return p{umdepth = read s}) "INT") - "universal modality depth", - Option [] - ["diff-univ-mod-depth"] - (ReqArg ((not . null) ?-> \s p -> return p{dumdepth = read s}) "INT") - "difference universal modality depth", - Option [] - ["inv-mod-depth"] - (ReqArg ((not . null) ?-> \s p -> return p{invdepth = read s}) "INT") - "inverse modality depth", - Option [] - ["prop-vars"] - (ReqArg ((not . null) ?-> \s p -> return p{pvars = read s}) "INT") - "number of propositional variables", - Option [] - ["nom-vars"] - (ReqArg ((not . null) ?-> \s p -> return p{nomvars = read s}) "INT") - "number of nominal variables", - Option [] - ["state-vars"] - (ReqArg ((not . null) ?-> \s p -> return p{stvars = read s}) "INT") - "number of state variables", - Option [] - ["proba-mod"] - (ReqArg ((not . null) ?-> \s p -> return p{pmod = read s}) "INT") - "probability of a modal operator", - Option [] - ["proba-at"] - (ReqArg ((not . null) ?-> \s p -> return p{pat = read s}) "INT") - "probability of a @ operator", - Option [] - ["proba-down"] - (ReqArg ((not . null) ?-> \s p -> return p{pdown = read s}) "INT") - "probability of a down arrow operator", - Option [] - ["proba-univ"] - (ReqArg ((not . null) ?-> \s p -> return p{puniv = read s}) "INT") - "probability of a universal modality", - Option [] - ["proba-diff-univ"] - (ReqArg ((not . null) ?-> \s p -> return p{pduniv = read s}) "INT") - "probability of a difference universal modality", - Option [] - ["proba-inv"] - (ReqArg ((not . null) ?-> \s p -> return p{pinv = read s}) "INT") - "probability of an inverse modality", - Option [] - ["proba-prop"] - (ReqArg ((not . null) ?-> \s p -> return p{pprop = read s}) "INT") - "probability of a proposition", - Option [] - ["proba-nom"] - (ReqArg ((not . null) ?-> \s p -> return p{pnom = read s}) "INT") - "probability of a nominal", - Option [] - ["proba-state"] - (ReqArg ((not . null) ?-> \s p -> return p{psvar = read s}) "INT") - "probability of a state variable", - Option [] - ["proba-neg"] - (ReqArg ((not . null) ?-> \s p -> return p{pneg = read s}) "INT") - "probability of a negation", - Option [] - ["proba-op"] - (ReqArg ((not . null) ?-> \s p -> return p{pop = read s}) "INT") - "probability of an operator" - ] - - -(?->) :: (String -> Bool) -> (String -> ParamsModifier) -> String -> ParamsModifier -p ?-> m = \s -> if not (null s) && p s - then m s - else \_ -> throwError ("Invalid argument: '" ++ s ++ "'") - +import System.Console.CmdArgs -defaultParams :: Params -defaultParams - = Prms {numinst = 1, -- Number of Instances to Generate. - numclauses = 5, -- Number of Clauses to Generate per Instance. - csize = [0,0,1], -- Size of a Clause. (ie [1,1,1] means same chance for length 1,2 or 3) - mods = 1, -- Number of Modalities. - gdepth = 6, -- Global (maximum) depth - forceDepths = False, -- Force global max depth (ignore max depth per operator) - mdepth = 2, -- Modal Depth. - atdepth = 2, -- @ Depth. - dwdepth = 0, -- Downarrow Depth. - umdepth = 0, -- Universal Modality Depth. - dumdepth = 0, -- Difference Universal Modality Depth. - invdepth = 0, -- Inverse Modality Depth. - pvars = 5, -- Number of prop vars. - nomvars = 5, -- Number of nominals. - stvars = 0, -- Number of state variables. - pmod = 1, -- Probability of a modal operator. - pat = 1, -- Probability of an @ operator - pdown = 0, -- Probability of a downarrow operator - puniv = 0, -- Probability of an univ. modality - pduniv = 0, -- Probability of an diff. univ. modality - pinv = 0, -- Probability of an inv. modality - pprop = 1, -- Probability of a proposition - pnom = 1, -- Probability of a nominal - psvar = 0, -- Probability of a state variable - pneg = 50, -- Probability of a negation - pop = 50, -- Probability of an operator - simpleFormat = False, - stdout = False, -- Wether to save formulas in file or just display the first one on stdout - hidesummary = False, -- Wether to hide or not the summary of parameters used - showHelp = False -- Wether to display help instead of running - } +defaultParams :: Annotate Ann +defaultParams = record Params{} + [ numinst := 1 += name "#" += help "Number of Instances to Generate" + , numclauses := 5 += name "c" += name "num-clauses" += help "Number of Clauses to Generate per Instance" + , csize := "[0,0,1]" += name "clause-size" += help "Size of a Clause (ie [1,1,1] means same chance for length 1,2 or 3). Default: [0,0,1]" + , mods := 1 += help "Number of Modalities" + , gdepth := 6 += name "global-depth" += help "Global (maximum) depth" + , forceDepths := False += name "force-depths" += help "Force global max depth (ignore max depth per operator)" + , mdepth := 2 += name "modal-depth" += help "Modal Depth" + , atdepth := 2 += name "at-depth" += help "@ Depth" + , dwdepth := 0 += name "down-arrow-depth" += help "Downarrow Depth" + , umdepth := 0 += name "univ-mod-depth" += help "Universal Modality Depth" + , dumdepth := 0 += name "diff-univ-mod-depth" += help "Difference Universal Modality Depth" + , invdepth := 0 += name "inv-mod-depth" += help "Inverse Modality Depth" + , pvars := 5 += name "prop-vars" += help "Number of prop vars" + , nomvars := 5 += name "nom-vars" += help "Number of nominals" + , stvars := 0 += name "state-vars" += help "Number of state variables" + , pmod := 1 += name "proba-mod" += help "Probability of a modal operator" + , pat := 1 += name "proba-at" += help "Probability of an @ operator" + , pdown := 0 += name "proba-down" += help "Probability of a downarrow operator" + , puniv := 0 += name "proba-univ" += help "Probability of an univ. modality" + , pduniv := 0 += name "proba-diff-univ" += help "Probability of an diff. univ. modality" + , pinv := 0 += name "proba-inv" += help "Probability of an inv. modality" + , pprop := 1 += name "proba-prop" += help "Probability of a proposition" + , pnom := 1 += name "proba-nom" += help "Probability of a nominal" + , psvar := 0 += name "proba-state" += help "Probability of a state variable" + , pneg := 50 += name "proba-neg" += help "Probability of a negation" + , pop := 50 += name "proba-op" += help "Probability of an operator" + , hidesummary := False += name "H" += name "hide-summary" += help "Hide summary of parameters used" + , gendefaults := False += name "gen-defaults" += help "Generate deftab formula (normal default)" + ] -data Params = Prms{ - numinst ::Int, -- Number of Instances to Generate. - numclauses ::Int, -- Number of Clauses to Generate per Instance. - csize ::[Int], -- Size of a Clause. (ie [1,1,1] means same chance for length 1,2 or 3) - mods ::Int, -- Number of Modalities. - gdepth ::Int, -- Global (maximum) Depth - forceDepths ::Bool, -- whether or not to impose strict maximum depths per operator - mdepth ::Int, -- Modal Depth. - atdepth ::Int, -- @ Depth. - dwdepth ::Int, -- Downarrow Depth. - umdepth ::Int, -- Universal Modality Depth. - dumdepth ::Int, -- Difference Universal Modality Depth. - invdepth ::Int, -- Inverse Modality Depth. - pvars ::Int, -- Number of prop vars. - nomvars ::Int, -- Number of nominals. - stvars ::Int, -- Number of state variables. - pmod ::Int, -- Probability of a modal operator. - pat ::Int, -- Probability of an @ operator - pdown ::Int, -- Probability of a downarrow operator - puniv ::Int, -- Probability of an universal modality - pduniv ::Int, -- Probability of an diff. univ. modality - pinv ::Int, -- Probability of an inverse modality - pprop ::Int, -- Probability of a proposition - pnom ::Int, -- Probability of a nominal - psvar ::Int, -- Probability of a state variable - pneg ::Int, -- Probability of a negation - pop ::Int, -- Probability of an operator - simpleFormat ::Bool, - stdout ::Bool, -- Wether to save formulas in file or just display the first one on stdout - hidesummary ::Bool, -- Wether to hide or not the summary of parameters used - showHelp ::Bool -- Wether to display help instead of running - } +data Params = Params{ + numinst ::Int, -- Number of Instances to Generate. + numclauses ::Int, -- Number of Clauses to Generate per Instance. + csize ::String, -- Size of a Clause. (ie [1,1,1] means same chance for length 1,2 or 3) + mods ::Int, -- Number of Modalities. + gdepth ::Int, -- Global (maximum) Depth + forceDepths ::Bool, -- whether or not to impose strict maximum depths per operator + mdepth ::Int, -- Modal Depth. + atdepth ::Int, -- @ Depth. + dwdepth ::Int, -- Downarrow Depth. + umdepth ::Int, -- Universal Modality Depth. + dumdepth ::Int, -- Difference Universal Modality Depth. + invdepth ::Int, -- Inverse Modality Depth. + pvars ::Int, -- Number of prop vars. + nomvars ::Int, -- Number of nominals. + stvars ::Int, -- Number of state variables. + pmod ::Int, -- Probability of a modal operator. + pat ::Int, -- Probability of an @ operator + pdown ::Int, -- Probability of a downarrow operator + puniv ::Int, -- Probability of an universal modality + pduniv ::Int, -- Probability of an diff. univ. modality + pinv ::Int, -- Probability of an inverse modality + pprop ::Int, -- Probability of a proposition + pnom ::Int, -- Probability of a nominal + psvar ::Int, -- Probability of a state variable + pneg ::Int, -- Probability of a negation + pop ::Int, -- Probability of an operator + hidesummary ::Bool, -- Wether to hide or not the summary of parameters used + gendefaults ::Bool + } deriving (Show, Data, Typeable) -instance Show Params where - show p = - unlines ["Number of Instances to Generate : numinst = " ++ show (numinst p), - "Number of Clauses to Generate per Instance: numclauses = " ++ show (numclauses p), - "Size of a Clause : csize = " ++ show (csize p), - "Number of Modalities : mods = " ++ show (mods p), - "Global (maximum) Depth : gdepth = " ++ show (gdepth p), - "Enformce maximum depths? : force-depths = " ++ show (forceDepths p), - "Modal Depth : mdepth = " ++ show (mdepth p), - "@ Depth : atdepth = " ++ show (atdepth p), - "Downarrow Depth : dwdepth = " ++ show (dwdepth p), - "Universal Modality Depth : umdepth = " ++ show (umdepth p), - "Difference Universal Modality Depth : dumdepth = " ++ show (dumdepth p), - "Inverse Modality Depth : invdepth = " ++ show (invdepth p), - "Number of propositional variables : pvars = " ++ show (pvars p), - "Number of nominals : nomvars = " ++ show (nomvars p), - "Number of state variables : stvars = " ++ show (stvars p), - "Probability of a modal operator : pmod = " ++ show (pmod p), - "Probability of an @ operator : pat = " ++ show (pat p), - "Probability of a downarrow operator : pdown = " ++ show (pdown p), - "Probability of an universal modality : puniv = " ++ show (puniv p), - "Probability of a diff. universal modality : pduniv = " ++ show (pduniv p), - "Probability of an inverse modality : pinv = " ++ show (pinv p), - "Probability of a propositional variable : pprop = " ++ show (pprop p), - "Probability of a nominal : pnom = " ++ show (pnom p), - "Probability of a state variable : psvar = " ++ show (psvar p), - "Probability of a negation : pneg = " ++ show (pneg p), - "Probability of an operator : pop = " ++ show (pop p)] diff --git a/src/hgen.hs b/src/hgen.hs --- a/src/hgen.hs +++ b/src/hgen.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE CPP #-} + -- 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 @@ -13,11 +15,13 @@ import Debug.Trace(trace) import System.Random(StdGen,randomR,newStdGen) import Control.Monad.State(get,put,State,evalState) -import Control.Monad(unless) +import Control.Monad(unless, when) import qualified HyLo.Formula as F (Formula(..)) -import System.Environment( getProgName ) import Prelude hiding ( mod ) +import System.Console.CmdArgs + ( details, summary, (+=), cmdArgs_ ) + import Data.Version ( showVersion ) import Paths_hgen ( version ) @@ -73,36 +77,25 @@ 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 +main = do params <- cmdArgs_ $ defaultParams += summary header += details gplTag + 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 - writeList (getName params) (numinst params) frmList + do unless (hidesummary params) $ putStrLn $ "Setting the following parameters:\n" ++ show params + (frmList,d1frmList,d2frmList) <- evalState (generateFormulaList (numinst params) params) `fmap` newStdGen + let name = getName params + let d1name = "d1" ++ name + let d2name = "d2" ++ name + writeList name (numinst params) frmList + when (gendefaults params) $ writeList d1name (numinst params) d1frmList + when (gendefaults params) $ writeList d2name (numinst params) d2frmList getName :: Params -> String getName params = "hcnf" ++ "C" ++ show (numclauses params) ++ "-" ++ - "S" ++ show (csize params) ++ "-" ++ + "S" ++ (csize params) ++ "-" ++ "M" ++ show (mods params) ++ "-" ++ "GD" ++ show (gdepth params) ++ "-" ++ -- "@D" ++ show (atdepth params) ++ "-" ++ @@ -116,10 +109,11 @@ header :: String header = unlines ["hgen " ++ showVersion version, - "C. Areces, D. Gorin, G. Hoffmann and J. Heguiabehere. (c) 2002-2009."] + "Compiled on " ++ __DATE__ ++ ", at " ++ __TIME__, + "C. Areces, D. Gorin, G. Hoffmann and J. Heguiabehere."] -gplTag :: String -gplTag = unlines [ +gplTag :: [String] +gplTag = [ "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", @@ -154,13 +148,13 @@ genShape 0 _ _ = return [] genShape n 0 p = do r <- nextR - let numDisj = choose (csize p) r + let numDisj = choose (read $ 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 numDisj = choose (read $ csize p) r let pc = fromIntegral (pop p * numDisj) * (0.01::Double) let floorpc = floor pc let ceilingpc = ceiling pc @@ -356,12 +350,13 @@ rdisj <- genDisjunctList shapes p return (disj:rdisj) -generateFormula :: Params -> State StdGen String +generateFormula :: Params -> State StdGen (String,String,String) generateFormula p = do shapes <- genShape (numclauses p) (gdepth p) p gd <- genDisjunctList shapes p newf <- mapM (sanitize2 p) gd - return $ write $ map toHyLoFormula newf + let forms = map toHyLoFormula newf + return (simpleOutput forms, defaultOutput1 forms,defaultOutput2 forms) hmpro :: Formula -> Int hmpro (Fprop _) = 1 @@ -520,12 +515,12 @@ | otherwise = For (changeAt pos n f1:(f2:fl)) changeAt _ _ _ = error "changeAt" -generateFormulaList :: Int -> Params -> State StdGen [String] -generateFormulaList 0 _ = return [] +generateFormulaList :: Int -> Params -> State StdGen ([String],[String],[String]) +generateFormulaList 0 _ = return ([],[],[]) generateFormulaList n p = - do frm <- generateFormula p - lfrm <- generateFormulaList (n-1) p - return (frm:lfrm) + do (frm, d1frm, d2frm) <- generateFormula p + (lfrm, ld1frm, ld2frm) <- generateFormulaList (n-1) p + return (frm:lfrm, d1frm:ld1frm, d2frm:ld2frm) -- writeList : Given a filename, and a list of strings, -- writes the strings to a file with that name @@ -585,8 +580,27 @@ show (RelSymbol i) = 'R' : show i show (InvRelSymbol i) = "-R" ++ show i -write :: [HyLoFormula] -> String -write input = unlines $ "begin":addSemicolon (map show input) ++ ["end"] - where addSemicolon (x:xs@(_:_)) = (x ++ ";") : addSemicolon xs - addSemicolon xs = xs +simpleOutput :: [HyLoFormula] -> String +simpleOutput input = unlines $ "begin":addSemicolon (map show input) ++ ["end"] +defaultOutput2 :: [HyLoFormula] -> String +defaultOutput2 fs + | length fs < 3 = error "For default output, at least 3 clauses needed." + | otherwise = unlines $ + "classical":"facts:":"true":["defaults:"] ++ toDefs1 fs ++ toDefs2 fs ++ ["consequence:", show $ last fs ] + where + toDefs1 fs = map (\(x,y) -> "T --> " ++ show (x F.:|: y) ++ ";") $ zip fs $ tail fs + toDefs2 fs = map (\(x,y) -> show (x F.:|: y) ++ " --> " ++ show (x F.:&: y) ++ ";") $ zip fs $ tail fs + +defaultOutput1 :: [HyLoFormula] -> String +defaultOutput1 fs + | length fs < 3 = error "For default output, at least 3 clauses needed." + | otherwise = unlines $ + "classical":"facts:":"true":"defaults:":toDefault (map show fs) ++ ["consequence:","false"] + + +addSemicolon :: [String] -> [String] +addSemicolon xs = map (\x -> x ++ ";") xs + +toDefault :: [String] -> [String] +toDefault xs = map (\x -> "T --> " ++ x ++ ";") xs