Add randcool utility

randcool/randcool.cabal

+-- Initial cool2tatl.cabal generated by cabal init.  For further
+-- documentation, see http://haskell.org/cabal/users-guide/
+
+name:                randcool
+version:             0.1.0.0
+-- synopsis:
+-- description:
+license:             PublicDomain
+license-file:        LICENSE
+author:              Daniel Gorín
+maintainer:          jcpetruzza@gmail.com
+-- copyright:
+-- category:
+build-type:          Simple
+-- extra-source-files:
+cabal-version:       >=1.10
+
+executable randcool
+  main-is:            randcool.hs
+  ghc-options:        -Wall -O2
+  -- other-modules:
+  -- other-extensions:
+  build-depends:       base >=4.6 && <4.7
+                      ,containers
+                      ,rand-vars
+                      ,optparse-applicative
+                      ,random
+                      --,transformers
+                      --,bytestring >= 0.10.2.0
+  -- hs-source-dirs:
+  default-language:    Haskell2010

randcool/randcool.hs

+{-# LANGUAGE BangPatterns #-}
+module Main
+
+where
+
+import Control.Applicative
+import Control.Monad
+import Control.Monad.Random
+
+
+import Data.List
+import Data.Foldable ( for_ )
+import Data.Monoid
+import qualified Data.IntSet as I
+
+import Options.Applicative hiding ( Mod )
+
+import System.Random
+
+
+type Nat = Int  -- for documentation, not enforced
+
+
+data Fm mod
+ =
+   PAt  Nat
+ | NAt  Nat
+ | Con  [Fm mod]
+ | Dis  [Fm mod]
+ | Dia  mod (Fm mod)
+ | Box  mod (Fm mod)
+
+class Mod mod where
+  showDia :: mod -> ShowS
+  showBox :: mod -> ShowS
+
+data K = K
+
+instance Mod K where
+  showDia _ = showString "<r>"
+  showBox _ = showString "[r]"
+
+newtype G = G Nat
+
+instance Mod G where
+  showDia (G n) = showString "{>"  . shows n . showString " r}"
+  showBox (G n) = showString "{<=" . shows n . showString " r}"
+
+
+newtype CL = CL I.IntSet
+
+instance Mod CL where
+  showDia (CL ags) = showString "<{" . sepWith " " (I.toAscList ags) . showString "}>"
+  showBox (CL ags) = showString "[{" . sepWith " " (I.toAscList ags) . showString "}]"
+
+instance Mod mod => Show (Fm mod) where
+  showsPrec _ fm
+   = case fm of
+       PAt n    -> showString  "p" . shows n
+       NAt n    -> showString "~p" . shows n
+
+       Con []   -> showString "True"
+       Con [f]  -> shows f
+       Con fs   -> showParen True $ sepWith " & " fs
+
+       Dis []   -> showString "False"
+       Dis [f]  -> shows f
+       Dis fs   -> showParen True $ sepWith " | " fs
+
+       Dia m f -> showDia m . shows f
+       Box m f -> showBox m . shows f
+
+top,bot :: Fm mod
+top = Con []
+bot = Dis []
+
+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
+   }
+
+
+-- Modality generators
+monoK :: Rand K
+monoK = pure K
+
+
+gradesBetween :: Nat -> Nat -> Rand G
+gradesBetween from to = G <$> inRange (from,to)
+
+
+
+numAgents :: Nat -> Rand CL
+numAgents n = CL <$> buildSet I.empty (n+1)
+  where
+    buildSet !acc m
+      | m <= 0    = pure acc
+      | otherwise = do heads <- rand
+                       let acc' = if heads then acc else I.insert (m-1) acc
+                       buildSet acc' (m-1)
+
+someFormula :: Rand mod -> RandConf -> Rand (Fm mod)
+someFormula modGen conf = go (depth conf)
+  where
+    lits
+     = let as = [1..1+numAts conf] in [top,bot] ++ map PAt as ++ map NAt as
+
+    formulaOfDepth d
+     = do (m,junct,r) <- oneOf [(Dia,Con,(minCon conf,maxCon conf))
+                               ,(Box,Dis,(minDis conf,maxDis conf))]
+          n <- inRange r
+          m <$> modGen <*> (junct <$> exactly n (go d))
+
+    p = max 0 $ min 1 $ probAt conf
+
+    go d
+     | d == 0
+      = oneOf lits
+     | d == depth conf
+      = formulaOfDepth (d-1)
+     | otherwise
+      = join $ fromFreqs [oneOf lits           `withFreq`    p
+                         ,formulaOfDepth (d-1) `withFreq` (1-p)]
+
+exactly :: Nat -> Rand a -> Rand [a]
+exactly n = sequence . take n . repeat
+
+main :: IO ()
+main
+ = do (randFormula,n,m_seed) <- execParser opts_info
+
+      for_ m_seed $ \given_seed ->
+        setStdGen (mkStdGen given_seed)
+
+      sequence_ $ take n $ repeat (putStrLn =<< pick randFormula)
+
+ where
+  opts_info
+   = info (helper <*> (infoOption "0.1" ( long "version" ) <*> opts))
+            ( fullDesc
+         -- <> progDesc "descr"
+            <> header "randcool"
+            )
+
+  opts
+   = (,,) <$> (genSel <*> randConf) <*> numFormulas <*> optional seed
+
+
+genSel :: Parser (RandConf -> 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
+
+  selK
+   = flag' monoK
+       (  long "monomodal-K"
+       <> short 'K'
+       <> help "Language is K with one modality"
+       )
+
+  selG
+   = flag' gradesBetween
+       (  long "monomodal-gml"
+       <> short 'G'
+       <> help "Language is GML with one modality"
+       )
+     <*>
+     option (  value 0
+            <> long "min-grade"
+            <> metavar "NUM"
+            <> help "Minimum possible grade"
+            <> showDefault
+            )
+     <*>
+     option (  value 7
+            <> long "max-grade"
+            <> metavar "NUM"
+            <> help "Maximum possible grade"
+            <> showDefault
+            )
+
+  selCL
+   = flag' numAgents
+       (  long "coalition-logic"
+       <> help "Language is Coalition Logic"
+       )
+     <*>
+     option (  value 5
+            <> long "num-agents"
+            <> short 'A'
+            <> metavar "NUM"
+            <> help "Number of agents"
+            <> showDefault
+            )
+
+randConf :: Parser RandConf
+randConf
+ = RandConf
+    <$> option (  value 3
+               <> long "modal-depth"
+               <> short 'd'
+               <> metavar "NUM"
+               <> help "Modal depth of the formulas"
+               <> 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
+              )
+
+
+
+numFormulas :: Parser Nat
+numFormulas
+ = option (  value 1
+          <> long "num-formulas"
+          <> short 'n'
+          <> metavar "NUM"
+          <> help "Number of formulas to generate"
+          <> showDefault
+          )
+
+seed :: Parser Int
+seed
+ = option (  long "seed"
+          <> metavar "NUM"
+          <> help "Random seed"
+          )
+