## 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 |