diff --git a/randcool/randcool.hs b/randcool/randcool.hs
index e09592ffd407250400a8e5cd2bf198ded5e1f687..1cf77804c3d7fa149f481523ef4c987142a86cf6 100644
--- a/randcool/randcool.hs
+++ b/randcool/randcool.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE BangPatterns, NoMonomorphismRestriction #-}
module Main
where
@@ -10,6 +10,7 @@ import Control.Monad.Random
import Data.List
import Data.Foldable ( for_ )
+import Data.Maybe
import Data.Monoid
import qualified Data.IntSet as I
@@ -22,14 +23,17 @@ type Nat = Int -- for documentation, not enforced
data Fm mod
- =
- PAt Nat
+ = PAt Nat
| NAt Nat
| Con [Fm mod]
| Dis [Fm mod]
| Dia mod (Fm mod)
| Box mod (Fm mod)
+data Query mod
+ = [Fm mod] :|-: Fm mod
+
+
class Mod mod where
showDia :: mod -> ShowS
showBox :: mod -> ShowS
@@ -43,7 +47,7 @@ instance Mod K where
newtype G = G Nat
instance Mod G where
- showDia (G n) = showString "{>= " . shows n . showString " r}"
+ showDia (G n) = showString "{>= " . shows n . showString " r}"
showBox (G n) = showString "{<= " . shows n . showString " r}"
@@ -74,20 +78,72 @@ top,bot :: Fm mod
top = Con []
bot = Dis []
+instance Mod mod => Show (Query mod) where
+ showsPrec _ (tbox :|-: f)
+ = sepWith "; " tbox . showString " |- " . shows f
+
sepWith :: Show a => String -> [a] -> ShowS
sepWith s = appEndo . mconcat . map Endo . intersperse (showString s) . map shows
-data RandConf
- = RandConf {
- depth :: Nat -- modal depth of the resulting formula
- ,numAts :: Nat -- number of atoms
- ,minCon :: Nat -- min number of conjuncts per conjunction (0 allows for Top)
- ,maxCon :: Nat -- max number of conjuncts per conjunction
- ,minDis :: Nat -- min number of disjuncts per disjunction (0 allows for Bot)
- ,maxDis :: Nat -- max number of disjuncts per disjunction
- ,probAt :: Float -- probability of having an atom
- ,topCon :: Bool -- allow conjunctions at the top level
- ,topDis :: Bool -- allow disjunctions at the top level
+data GenFmConf nat bool float
+ = FmConf {
+ depth :: nat -- modal depth of the resulting formula
+ ,numAts :: nat -- number of atoms
+ ,minCon :: nat -- min number of conjuncts per conjunction (0 allows for Top)
+ ,maxCon :: nat -- max number of conjuncts per conjunction
+ ,minDis :: nat -- min number of disjuncts per disjunction (0 allows for Bot)
+ ,maxDis :: nat -- max number of disjuncts per disjunction
+ ,probAt :: float -- probability of having an atom
+ ,topCon :: bool -- allow conjunctions at the top level
+ ,topDis :: bool -- allow disjunctions at the top level
+ }
+
+type FmConf = GenFmConf Nat Bool Float
+type CmdFmConf = GenFmConf (Last Nat) (Last Bool) (Last Float)
+
+
+instance (Monoid a, Monoid b, Monoid c) => Monoid (GenFmConf a b c) where
+ mempty
+ = FmConf mempty mempty mempty mempty mempty mempty mempty mempty mempty
+
+ mappend l r
+ = FmConf {
+ depth = m depth
+ ,numAts = m numAts
+ ,minCon = m minCon
+ ,maxCon = m maxCon
+ ,minDis = m minDis
+ ,maxDis = m maxDis
+ ,probAt = m probAt
+ ,topCon = m topCon
+ ,topDis = m topDis
+ }
+ where
+ m f
+ = f l <> f r
+
+overrideWith :: FmConf -> CmdFmConf -> FmConf
+overrideWith b o
+ = FmConf {
+ depth = override depth depth
+ ,numAts = override numAts numAts
+ ,minCon = override minCon minCon
+ ,maxCon = override maxCon maxCon
+ ,minDis = override minDis minDis
+ ,maxDis = override maxDis maxDis
+ ,probAt = override probAt probAt
+ ,topDis = override topDis topDis
+ ,topCon = override topCon topCon
+ }
+ where
+ override f g
+ = fromMaybe (f b) (getLast $ g o)
+
+data QueryConf
+ = QueryConf {
+ formConf :: FmConf
+ ,tboxSize :: Nat
+ ,tboxConf :: FmConf
}
@@ -110,7 +166,7 @@ numAgents n = CL <$> buildSet I.empty n
let acc' = if heads then acc else I.insert m acc
buildSet acc' (m-1)
-someFormula :: Rand mod -> RandConf -> Rand (Fm mod)
+someFormula :: Rand mod -> FmConf -> Rand (Fm mod)
someFormula modGen conf = go (depth conf)
where
lits
@@ -125,7 +181,6 @@ someFormula modGen conf = go (depth conf)
,(Box,Dis `juncts` (minDis conf,maxDis conf))]
diabox <$> modGen <*> xxjuncts (go d)
-
p = max 0 $ min 1 $ probAt conf
go d
@@ -144,37 +199,39 @@ someFormula modGen conf = go (depth conf)
= join $ fromFreqs [oneOf lits `withFreq` p
,formulaOfDepth (d-1) `withFreq` (1-p)]
+someQuery :: Rand mod -> QueryConf -> Rand (Query mod)
+someQuery modGen QueryConf{tboxSize = size, tboxConf = tconf, formConf = fconf}
+ = (:|-:) <$> exactly size (someFm tconf) <*> someFm fconf
+ where
+ someFm = someFormula modGen
+
exactly :: Nat -> Rand a -> Rand [a]
exactly n = sequence . take n . repeat
main :: IO ()
main
- = do (randFormula,n,m_seed) <- execParser opts_info
+ = do (randQuery,n,m_seed) <- execParser opts_info
for_ m_seed $ \given_seed ->
setStdGen (mkStdGen given_seed)
- sequence_ $ take n $ repeat (putStrLn =<< pick randFormula)
+ sequence_ $ take n $ repeat (putStrLn =<< pick randQuery)
where
opts_info
- = info (helper <*> (infoOption "0.1" ( long "version" ) <*> opts))
- ( fullDesc
- -- <> progDesc "descr"
- <> header "randcool"
- )
+ = info (helper <*> (infoOption "0.1" ( long "version" ) <*> opts)) mempty
opts
- = (,,) <$> (genSel <*> randConf) <*> numFormulas <*> optional seed
+ = (,,) <$> (genSel <*> queryConf) <*> numQueries <*> optional seed
-genSel :: Parser (RandConf -> Rand String)
+genSel :: Parser (QueryConf -> Rand String)
genSel
= (gen <$> selK) <|> (gen <$> selG) <|> (gen <$> selCL)
where
- gen :: Mod mod => Rand mod -> RandConf -> Rand String
- gen modGen conf = show <$> someFormula modGen conf
+ gen :: Mod mod => Rand mod -> QueryConf -> Rand String
+ gen modGen conf = show <$> someQuery modGen conf
selK
= flag' monoK
@@ -195,6 +252,7 @@ genSel
<> metavar "NUM"
<> help "Minimum possible grade"
<> showDefault
+ <> hidden
)
<*>
option ( value 7
@@ -202,6 +260,7 @@ genSel
<> metavar "NUM"
<> help "Maximum possible grade"
<> showDefault
+ <> hidden
)
selCL
@@ -216,74 +275,92 @@ genSel
<> metavar "NUM"
<> help "Number of agents"
<> showDefault
+ <> hidden
)
-randConf :: Parser RandConf
-randConf
- = RandConf
- <$> option ( value 3
- <> long "modal-depth"
- <> short 'd'
+queryConf :: Parser QueryConf
+queryConf
+ = build
+ <$> fmConf TgBoth
+ <*> fmConf TgForm
+ <*> fmConf TgTBox
+ <*> option ( value 0
+ <> long "tbox-formulas"
+ <> short 'T'
<> metavar "NUM"
- <> help "Modal depth of the formulas"
+ <> help "Number of formulas to include on the TBox"
<> showDefault
)
- <*> option ( value 5
- <> long "propositions"
- <> short 'p'
- <> metavar "NUM"
- <> help "Number of proposition symbols"
- <> showDefault
- )
- <*> option ( value 2
- <> long "min-conjuncts"
- <> metavar "NUM"
- <> help "Minimum number of conjuncts per conjunction"
- <> showDefault
- )
- <*> option ( value 10
- <> long "max-conjuncts"
- <> metavar "NUM"
- <> help "Maximum number of conjuncts per conjunction"
- <> showDefault
- )
- <*> option ( value 2
- <> long "min-disjuncts"
- <> metavar "NUM"
- <> help "Minimum number of disjuncts per disjunction"
- <> showDefault
- )
- <*> option ( value 10
- <> long "max-disjuncts"
- <> metavar "NUM"
- <> help "Maximum number of disjuncts per disjunction"
- <> showDefault
- )
- <*> option ( value 0.25
- <> long "probability-atom"
- <> metavar "[0..1]"
- <> help "Probability of an atom occurring instead of a modality"
- <> showDefault
- )
- <*> flag True False
- ( long "no-toplevel-conj"
- <> help "Don't generate conjunctions at the top-level"
- )
- <*> flag True False
- ( long "no-toplevel-disj"
- <> help "Don't generate disjunctions at the top-level"
- )
-
-
-
-
-numFormulas :: Parser Nat
-numFormulas
+ where
+ build commonConf formOnly tboxOnly size
+ = QueryConf {
+ tboxSize = size
+ ,tboxConf = defaultFmConf `overrideWith` (commonConf <> tboxOnly)
+ ,formConf = defaultFmConf `overrideWith` (commonConf <> formOnly)
+ }
+
+data FmConfTarget
+ = TgForm | TgTBox | TgBoth
+ deriving Eq
+
+defaultFmConf :: FmConf
+defaultFmConf
+ = FmConf {
+ depth = 3
+ ,numAts = 5
+ ,minCon = 2
+ ,maxCon = 6
+ ,minDis = 2
+ ,maxDis = 6
+ ,probAt = 0.25
+ ,topCon = True
+ ,topDis = True
+ }
+
+fmConf :: FmConfTarget -> Parser CmdFmConf
+fmConf tg
+ = FmConf
+ <$> _option depth "modal-depth" "Modal depth of the formulas" (metavar "NUM" <> _short 'd')
+ <*> _option numAts "propositions" "Number of proposition symbols" (metavar "NUM" <> _short 'p')
+ <*> _option minCon "min-conjuncts" "Minimum number of conjuncts per conjunction" (metavar "NUM")
+ <*> _option maxCon "max-conjuncts" "Maximum number of conjuncts per conjunction" (metavar "NUM")
+ <*> _option minDis "min-disjuncts" "Minimum number of disjuncts per disjunction" (metavar "NUM")
+ <*> _option maxDis "max-disjuncts" "Maximum number of disjuncts per disjunction" (metavar "NUM")
+ <*> _option probAt "prob-atom" "Probability of an atom occurring instead of a modality" (metavar "[0..1]")
+ <*> _turnOff "no-toplevel-conj" "Don't generate conjunctions at the top-level" mempty
+ <*> _turnOff "no-toplevel-disj" "Don't generate disjunctions at the top-level" mempty
+ where
+ _option field s h mods
+ = Last <$> (optional $ option (long (mkLong s) <> hidden <> help (mkDescr (Just $ show . field) h) <> mods))
+
+ _turnOff s h mods
+ = Last <$> (optional $ flag' False (long (mkLong s) <> hidden <> help (mkDescr Nothing h) <> mods))
+
+ mkLong
+ = case tg of
+ TgForm -> (++ "-form")
+ TgTBox -> (++ "-tbox")
+ TgBoth -> id
+
+ mkDescr mf
+ = (++ ' ':msg)
+ where
+ msg
+ = case tg of
+ TgForm -> "(override only for the formula)"
+ TgTBox -> "(override only for TBox formulas)"
+ TgBoth -> maybe "" (\f -> "(default " ++ (f defaultFmConf) ++ ")") mf
+
+ _short
+ = if tg == TgBoth then short else const mempty
+
+numQueries :: Parser Nat
+numQueries
= option ( value 1
- <> long "num-formulas"
+ <> long "num-queries"
<> short 'n'
<> metavar "NUM"
- <> help "Number of formulas to generate"
+ <> help "Number of queries to generate"
<> showDefault
)