Project

General

Profile

Statistics
| Branch: | Revision:

cool / randcool / randcool.hs @ bb7f1f31

History | View | Annotate | Download (9.71 KB)

1
{-# LANGUAGE BangPatterns, NoMonomorphismRestriction #-}
2
module Main
3

    
4
where
5

    
6
import Control.Applicative
7
import Control.Monad
8
import Control.Monad.Random
9

    
10

    
11
import Data.List
12
import Data.Foldable ( for_ )
13
import Data.Maybe
14
import Data.Monoid
15
import qualified Data.IntSet as I
16

    
17
import Options.Applicative hiding ( Mod )
18

    
19
import System.Random
20

    
21

    
22
type Nat = Int  -- for documentation, not enforced
23

    
24

    
25
data Fm mod
26
 = PAt  Nat
27
 | NAt  Nat
28
 | Con  [Fm mod]
29
 | Dis  [Fm mod]
30
 | Dia  mod (Fm mod)
31
 | Box  mod (Fm mod)
32

    
33
data Query mod
34
 = [Fm mod] :|-: Fm mod
35

    
36

    
37
class Mod mod where
38
  showDia :: mod -> ShowS
39
  showBox :: mod -> ShowS
40

    
41
data K = K
42

    
43
instance Mod K where
44
  showDia _ = showString "<r>"
45
  showBox _ = showString "[r]"
46

    
47
newtype G = G Nat
48

    
49
instance Mod G where
50
  showDia (G n) = showString "{>= " . shows n . showString " r}"
51
  showBox (G n) = showString "{<= " . shows n . showString " r}"
52

    
53

    
54
newtype CL = CL I.IntSet
55

    
56
instance Mod CL where
57
  showDia (CL ags) = showString "<{" . sepWith " " (I.toAscList ags) . showString "}>"
58
  showBox (CL ags) = showString "[{" . sepWith " " (I.toAscList ags) . showString "}]"
59

    
60
instance Mod mod => Show (Fm mod) where
61
  showsPrec _ fm
62
   = case fm of
63
       PAt n    -> showString  "p" . shows n
64
       NAt n    -> showString "~p" . shows n
65

    
66
       Con []   -> showString "True"
67
       Con [f]  -> shows f
68
       Con fs   -> showParen True $ sepWith " & " fs
69

    
70
       Dis []   -> showString "False"
71
       Dis [f]  -> shows f
72
       Dis fs   -> showParen True $ sepWith " | " fs
73

    
74
       Dia m f -> showDia m . shows f
75
       Box m f -> showBox m . shows f
76

    
77
top,bot :: Fm mod
78
top = Con []
79
bot = Dis []
80

    
81
instance Mod mod => Show (Query mod) where
82
  showsPrec _ (tbox :|-: f)
83
   = sepWith "; " tbox . showString " |- " . shows f
84

    
85
sepWith :: Show a => String -> [a] -> ShowS
86
sepWith s = appEndo . mconcat . map Endo . intersperse (showString s) . map shows
87

    
88
data GenFmConf nat bool float
89
 = FmConf {
90
    depth  :: nat      -- modal depth of the resulting formula
91
   ,numAts :: nat      -- number of atoms
92
   ,minCon :: nat      -- min number of conjuncts per conjunction (0 allows for Top)
93
   ,maxCon :: nat      -- max number of conjuncts per conjunction
94
   ,minDis :: nat      -- min number of disjuncts per disjunction (0 allows for Bot)
95
   ,maxDis :: nat      -- max number of disjuncts per disjunction
96
   ,probAt :: float    -- probability of having an atom
97
   ,topCon :: bool     -- allow conjunctions at the top level
98
   ,topDis :: bool     -- allow disjunctions at the top level
99
   }
100

    
101
type FmConf    = GenFmConf Nat Bool Float
102
type CmdFmConf = GenFmConf (Last Nat) (Last Bool) (Last Float)
103

    
104

    
105
instance (Monoid a, Monoid b, Monoid c) => Monoid (GenFmConf a b c) where
106
  mempty
107
   = FmConf mempty mempty mempty mempty mempty mempty mempty mempty mempty
108

    
109
  mappend l r
110
   = FmConf {
111
       depth  = m depth
112
      ,numAts = m numAts
113
      ,minCon = m minCon
114
      ,maxCon = m maxCon
115
      ,minDis = m minDis
116
      ,maxDis = m maxDis
117
      ,probAt = m probAt
118
      ,topCon = m topCon
119
      ,topDis = m topDis
120
     }
121
     where
122
      m f
123
       = f l <> f r
124

    
125
overrideWith :: FmConf -> CmdFmConf -> FmConf
126
overrideWith b o
127
 = FmConf {
128
   depth  = override depth  depth
129
  ,numAts = override numAts numAts
130
  ,minCon = override minCon minCon
131
  ,maxCon = override maxCon maxCon
132
  ,minDis = override minDis minDis
133
  ,maxDis = override maxDis maxDis
134
  ,probAt = override probAt probAt
135
  ,topDis = override topDis topDis
136
  ,topCon = override topCon topCon
137
  }
138
  where
139
    override f g
140
     = fromMaybe (f b) (getLast $ g o)
141

    
142
data QueryConf
143
 = QueryConf {
144
    formConf :: FmConf
145
   ,tboxSize :: Nat
146
   ,tboxConf :: FmConf
147
   }
148

    
149

    
150
-- Modality generators
151
monoK :: Rand K
152
monoK = pure K
153

    
154

    
155
gradesBetween :: Nat -> Nat -> Rand G
156
gradesBetween from to = G <$> inRange (from,to)
157

    
158

    
159

    
160
numAgents :: Nat -> Rand CL
161
numAgents n = CL <$> buildSet I.empty n
162
  where
163
    buildSet !acc m
164
      | m <= 0    = pure acc
165
      | otherwise = do heads <- rand
166
                       let acc' = if heads then acc else I.insert m acc
167
                       buildSet acc' (m-1)
168

    
169
someFormula :: Rand mod -> FmConf -> Rand (Fm mod)
170
someFormula modGen conf = go (depth conf)
171
  where
172
    lits
173
     = let as = [1..1+numAts conf] in [top,bot] ++ map PAt as ++ map NAt as
174

    
175
    juncts junct_type r = \f ->
176
       do n <- inRange r
177
          junct_type <$> exactly n f
178

    
179
    formulaOfDepth d
180
     = do (diabox,xxjuncts) <- oneOf [(Dia,Con `juncts` (minCon conf,maxCon conf))
181
                                     ,(Box,Dis `juncts` (minDis conf,maxDis conf))]
182
          diabox <$> modGen <*> xxjuncts (go d)
183

    
184
    p = max 0 $ min 1 $ probAt conf
185

    
186
    go d
187
     | d == 0
188
      = oneOf lits
189

    
190
     | d == depth conf
191
      = let modal_form = formulaOfDepth (d-1)
192
        in join $ oneOf $ concat
193
            [ [modal_form]
194
            , [Con `juncts` (minCon conf,maxCon conf) $ modal_form | topCon conf]
195
            , [Dis `juncts` (minDis conf,maxDis conf) $ modal_form | topDis conf]
196
            ]
197

    
198
     | otherwise
199
      = join $ fromFreqs [oneOf lits           `withFreq`    p
200
                         ,formulaOfDepth (d-1) `withFreq` (1-p)]
201

    
202
someQuery :: Rand mod -> QueryConf -> Rand (Query mod)
203
someQuery modGen QueryConf{tboxSize = size, tboxConf = tconf, formConf = fconf}
204
 = (:|-:) <$> exactly size (someFm tconf) <*> someFm fconf
205
 where
206
   someFm = someFormula modGen
207

    
208
exactly :: Nat -> Rand a -> Rand [a]
209
exactly n = sequence . take n . repeat
210

    
211
main :: IO ()
212
main
213
 = do (randQuery,n,m_seed) <- execParser opts_info
214

    
215
      for_ m_seed $ \given_seed ->
216
        setStdGen (mkStdGen given_seed)
217

    
218
      sequence_ $ take n $ repeat (putStrLn =<< pick randQuery)
219

    
220
 where
221
  opts_info
222
   = info (helper <*> (infoOption "0.1" ( long "version" ) <*> opts)) mempty
223

    
224
  opts
225
   = (,,) <$> (genSel <*> queryConf) <*> numQueries <*> optional seed
226

    
227

    
228
genSel :: Parser (QueryConf -> Rand String)
229
genSel
230
 = (gen <$> selK) <|> (gen <$> selG) <|> (gen <$> selCL)
231

    
232
 where
233
  gen :: Mod mod => Rand mod -> QueryConf -> Rand String
234
  gen modGen conf = show <$> someQuery modGen conf
235

    
236
  selK
237
   = flag' monoK
238
       (  long "monomodal-K"
239
       <> short 'K'
240
       <> help "Language is K with one modality"
241
       )
242

    
243
  selG
244
   = flag' gradesBetween
245
       (  long "monomodal-gml"
246
       <> short 'G'
247
       <> help "Language is GML with one modality"
248
       )
249
     <*>
250
     option (  value 0
251
            <> long "min-grade"
252
            <> metavar "NUM"
253
            <> help "Minimum possible grade"
254
            <> showDefault
255
            <> hidden
256
            )
257
     <*>
258
     option (  value 7
259
            <> long "max-grade"
260
            <> metavar "NUM"
261
            <> help "Maximum possible grade"
262
            <> showDefault
263
            <> hidden
264
            )
265

    
266
  selCL
267
   = flag' numAgents
268
       (  long "coalition-logic"
269
       <> help "Language is Coalition Logic"
270
       )
271
     <*>
272
     option (  value 5
273
            <> long "num-agents"
274
            <> short 'A'
275
            <> metavar "NUM"
276
            <> help "Number of agents"
277
            <> showDefault
278
            <> hidden
279
            )
280

    
281
queryConf :: Parser QueryConf
282
queryConf
283
 = build
284
    <$> fmConf TgBoth
285
    <*> fmConf TgForm
286
    <*> fmConf TgTBox
287
    <*> option (  value 0
288
               <> long "tbox-formulas"
289
               <> short 'T'
290
               <> metavar "NUM"
291
               <> help "Number of formulas to include on the TBox"
292
               <> showDefault
293
               )
294
 where
295
   build commonConf formOnly tboxOnly size
296
    = QueryConf {
297
       tboxSize = size
298
      ,tboxConf = defaultFmConf `overrideWith` (commonConf <> tboxOnly)
299
      ,formConf = defaultFmConf `overrideWith` (commonConf <> formOnly)
300
      }
301

    
302
data FmConfTarget
303
 = TgForm | TgTBox | TgBoth
304
  deriving Eq
305

    
306
defaultFmConf :: FmConf
307
defaultFmConf
308
 = FmConf {
309
    depth  = 3
310
   ,numAts = 5
311
   ,minCon = 2
312
   ,maxCon = 6
313
   ,minDis = 2
314
   ,maxDis = 6
315
   ,probAt = 0.25
316
   ,topCon = True
317
   ,topDis = True
318
   }
319

    
320
fmConf :: FmConfTarget -> Parser CmdFmConf
321
fmConf tg
322
 = FmConf
323
    <$> _option  depth  "modal-depth"   "Modal depth of the formulas"   (metavar "NUM" <> _short 'd')
324
    <*> _option  numAts "propositions"  "Number of proposition symbols" (metavar "NUM" <> _short 'p')
325
    <*> _option  minCon "min-conjuncts" "Minimum number of conjuncts per conjunction" (metavar "NUM")
326
    <*> _option  maxCon "max-conjuncts" "Maximum number of conjuncts per conjunction" (metavar "NUM")
327
    <*> _option  minDis "min-disjuncts" "Minimum number of disjuncts per disjunction" (metavar "NUM")
328
    <*> _option  maxDis "max-disjuncts" "Maximum number of disjuncts per disjunction" (metavar "NUM")
329
    <*> _option  probAt "prob-atom"     "Probability of an atom occurring instead of a modality" (metavar "[0..1]")
330
    <*> _turnOff "no-toplevel-conj"     "Don't generate conjunctions at the top-level" mempty
331
    <*> _turnOff "no-toplevel-disj"     "Don't generate disjunctions at the top-level" mempty
332
 where
333
  _option field s h mods
334
   = Last <$> (optional $ option (long (mkLong s) <> hidden <> help (mkDescr (Just $ show . field) h) <> mods))
335

    
336
  _turnOff s h mods
337
   = Last <$> (optional $ flag' False (long (mkLong s) <> hidden <> help (mkDescr Nothing h) <> mods))
338

    
339
  mkLong
340
   = case tg of
341
       TgForm -> (++ "-form")
342
       TgTBox -> (++ "-tbox")
343
       TgBoth -> id
344

    
345
  mkDescr mf
346
   = (++ ' ':msg)
347
   where
348
    msg
349
     = case tg of
350
         TgForm -> "(override only for the formula)"
351
         TgTBox -> "(override only for TBox formulas)"
352
         TgBoth -> maybe "" (\f -> "(default " ++ (f defaultFmConf) ++ ")") mf
353

    
354
  _short
355
   = if tg == TgBoth then short else const mempty
356

    
357
numQueries :: Parser Nat
358
numQueries
359
 = option (  value 1
360
          <> long "num-queries"
361
          <> short 'n'
362
          <> metavar "NUM"
363
          <> help "Number of queries to generate"
364
          <> showDefault
365
          )
366

    
367
seed :: Parser Int
368
seed
369
 = option (  long "seed"
370
          <> metavar "NUM"
371
          <> help "Random seed"
372
          )
373