hgen 1.4.0 → 1.5.0
raw patch · 3 files changed
+127/−329 lines, 3 filesdep +cmdargsdep −directorydep −filepathdep ~hylolib
Dependencies added: cmdargs
Dependencies removed: directory, filepath
Dependency ranges changed: hylolib
Files
- hgen.cabal +10/−6
- src/Params.hs +63/−283
- src/hgen.hs +54/−40
hgen.cabal view
@@ -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
src/Params.hs view
@@ -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)]
src/hgen.hs view
@@ -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