## cool / randcool / randcool.hs @ 123bbbec

History | View | Annotate | Download (7.58 KB)

1 |
{-# LANGUAGE BangPatterns #-} |
---|---|

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.Monoid |

14 |
import qualified Data.IntSet as I |

15 | |

16 |
import Options.Applicative hiding ( Mod ) |

17 | |

18 |
import System.Random |

19 | |

20 | |

21 |
type Nat = Int -- for documentation, not enforced |

22 | |

23 | |

24 |
data Fm mod |

25 |
= |

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 |
class Mod mod where |

34 |
showDia :: mod -> ShowS |

35 |
showBox :: mod -> ShowS |

36 | |

37 |
data K = K |

38 | |

39 |
instance Mod K where |

40 |
showDia _ = showString "<r>" |

41 |
showBox _ = showString "[r]" |

42 | |

43 |
newtype G = G Nat |

44 | |

45 |
instance Mod G where |

46 |
showDia (G n) = showString "{>" . shows n . showString " r}" |

47 |
showBox (G n) = showString "{<=" . shows n . showString " r}" |

48 | |

49 | |

50 |
newtype CL = CL I.IntSet |

51 | |

52 |
instance Mod CL where |

53 |
showDia (CL ags) = showString "<{" . sepWith " " (I.toAscList ags) . showString "}>" |

54 |
showBox (CL ags) = showString "[{" . sepWith " " (I.toAscList ags) . showString "}]" |

55 | |

56 |
instance Mod mod => Show (Fm mod) where |

57 |
showsPrec _ fm |

58 |
= case fm of |

59 |
PAt n -> showString "p" . shows n |

60 |
NAt n -> showString "~p" . shows n |

61 | |

62 |
Con [] -> showString "True" |

63 |
Con [f] -> shows f |

64 |
Con fs -> showParen True $ sepWith " & " fs |

65 | |

66 |
Dis [] -> showString "False" |

67 |
Dis [f] -> shows f |

68 |
Dis fs -> showParen True $ sepWith " | " fs |

69 | |

70 |
Dia m f -> showDia m . shows f |

71 |
Box m f -> showBox m . shows f |

72 | |

73 |
top,bot :: Fm mod |

74 |
top = Con [] |

75 |
bot = Dis [] |

76 | |

77 |
sepWith :: Show a => String -> [a] -> ShowS |

78 |
sepWith s = appEndo . mconcat . map Endo . intersperse (showString s) . map shows |

79 | |

80 |
data RandConf |

81 |
= RandConf { |

82 |
depth :: Nat -- modal depth of the resulting formula |

83 |
,numAts :: Nat -- number of atoms |

84 |
,minCon :: Nat -- min number of conjuncts per conjunction (0 allows for Top) |

85 |
,maxCon :: Nat -- max number of conjuncts per conjunction |

86 |
,minDis :: Nat -- min number of disjuncts per disjunction (0 allows for Bot) |

87 |
,maxDis :: Nat -- max number of disjuncts per disjunction |

88 |
,probAt :: Float -- probability of having an atom |

89 |
,topCon :: Bool -- allow conjunctions at the top level |

90 |
,topDis :: Bool -- allow disjunctions at the top level |

91 |
} |

92 | |

93 | |

94 |
-- Modality generators |

95 |
monoK :: Rand K |

96 |
monoK = pure K |

97 | |

98 | |

99 |
gradesBetween :: Nat -> Nat -> Rand G |

100 |
gradesBetween from to = G <$> inRange (from,to) |

101 | |

102 | |

103 | |

104 |
numAgents :: Nat -> Rand CL |

105 |
numAgents n = CL <$> buildSet I.empty (n+1) |

106 |
where |

107 |
buildSet !acc m |

108 |
| m <= 0 = pure acc |

109 |
| otherwise = do heads <- rand |

110 |
let acc' = if heads then acc else I.insert (m-1) acc |

111 |
buildSet acc' (m-1) |

112 | |

113 |
someFormula :: Rand mod -> RandConf -> Rand (Fm mod) |

114 |
someFormula modGen conf = go (depth conf) |

115 |
where |

116 |
lits |

117 |
= let as = [1..1+numAts conf] in [top,bot] ++ map PAt as ++ map NAt as |

118 | |

119 |
juncts junct_type r = \f -> |

120 |
do n <- inRange r |

121 |
junct_type <$> exactly n f |

122 | |

123 |
formulaOfDepth d |

124 |
= do (diabox,xxjuncts) <- oneOf [(Dia,Con `juncts` (minCon conf,maxCon conf)) |

125 |
,(Box,Dis `juncts` (minDis conf,maxDis conf))] |

126 |
diabox <$> modGen <*> xxjuncts (go d) |

127 | |

128 | |

129 |
p = max 0 $ min 1 $ probAt conf |

130 | |

131 |
go d |

132 |
| d == 0 |

133 |
= oneOf lits |

134 | |

135 |
| d == depth conf |

136 |
= let modal_form = formulaOfDepth (d-1) |

137 |
in join $ oneOf $ concat |

138 |
[ [modal_form] |

139 |
, [Con `juncts` (minCon conf,maxCon conf) $ modal_form | topCon conf] |

140 |
, [Dis `juncts` (minDis conf,maxDis conf) $ modal_form | topDis conf] |

141 |
] |

142 | |

143 |
| otherwise |

144 |
= join $ fromFreqs [oneOf lits `withFreq` p |

145 |
,formulaOfDepth (d-1) `withFreq` (1-p)] |

146 | |

147 |
exactly :: Nat -> Rand a -> Rand [a] |

148 |
exactly n = sequence . take n . repeat |

149 | |

150 |
main :: IO () |

151 |
main |

152 |
= do (randFormula,n,m_seed) <- execParser opts_info |

153 | |

154 |
for_ m_seed $ \given_seed -> |

155 |
setStdGen (mkStdGen given_seed) |

156 | |

157 |
sequence_ $ take n $ repeat (putStrLn =<< pick randFormula) |

158 | |

159 |
where |

160 |
opts_info |

161 |
= info (helper <*> (infoOption "0.1" ( long "version" ) <*> opts)) |

162 |
( fullDesc |

163 |
-- <> progDesc "descr" |

164 |
<> header "randcool" |

165 |
) |

166 | |

167 |
opts |

168 |
= (,,) <$> (genSel <*> randConf) <*> numFormulas <*> optional seed |

169 | |

170 | |

171 |
genSel :: Parser (RandConf -> Rand String) |

172 |
genSel |

173 |
= (gen <$> selK) <|> (gen <$> selG) <|> (gen <$> selCL) |

174 | |

175 |
where |

176 |
gen :: Mod mod => Rand mod -> RandConf -> Rand String |

177 |
gen modGen conf = show <$> someFormula modGen conf |

178 | |

179 |
selK |

180 |
= flag' monoK |

181 |
( long "monomodal-K" |

182 |
<> short 'K' |

183 |
<> help "Language is K with one modality" |

184 |
) |

185 | |

186 |
selG |

187 |
= flag' gradesBetween |

188 |
( long "monomodal-gml" |

189 |
<> short 'G' |

190 |
<> help "Language is GML with one modality" |

191 |
) |

192 |
<*> |

193 |
option ( value 0 |

194 |
<> long "min-grade" |

195 |
<> metavar "NUM" |

196 |
<> help "Minimum possible grade" |

197 |
<> showDefault |

198 |
) |

199 |
<*> |

200 |
option ( value 7 |

201 |
<> long "max-grade" |

202 |
<> metavar "NUM" |

203 |
<> help "Maximum possible grade" |

204 |
<> showDefault |

205 |
) |

206 | |

207 |
selCL |

208 |
= flag' numAgents |

209 |
( long "coalition-logic" |

210 |
<> help "Language is Coalition Logic" |

211 |
) |

212 |
<*> |

213 |
option ( value 5 |

214 |
<> long "num-agents" |

215 |
<> short 'A' |

216 |
<> metavar "NUM" |

217 |
<> help "Number of agents" |

218 |
<> showDefault |

219 |
) |

220 | |

221 |
randConf :: Parser RandConf |

222 |
randConf |

223 |
= RandConf |

224 |
<$> option ( value 3 |

225 |
<> long "modal-depth" |

226 |
<> short 'd' |

227 |
<> metavar "NUM" |

228 |
<> help "Modal depth of the formulas" |

229 |
<> showDefault |

230 |
) |

231 |
<*> option ( value 5 |

232 |
<> long "propositions" |

233 |
<> short 'p' |

234 |
<> metavar "NUM" |

235 |
<> help "Number of proposition symbols" |

236 |
<> showDefault |

237 |
) |

238 |
<*> option ( value 2 |

239 |
<> long "min-conjuncts" |

240 |
<> metavar "NUM" |

241 |
<> help "Minimum number of conjuncts per conjunction" |

242 |
<> showDefault |

243 |
) |

244 |
<*> option ( value 10 |

245 |
<> long "max-conjuncts" |

246 |
<> metavar "NUM" |

247 |
<> help "Maximum number of conjuncts per conjunction" |

248 |
<> showDefault |

249 |
) |

250 |
<*> option ( value 2 |

251 |
<> long "min-disjuncts" |

252 |
<> metavar "NUM" |

253 |
<> help "Minimum number of disjuncts per disjunction" |

254 |
<> showDefault |

255 |
) |

256 |
<*> option ( value 10 |

257 |
<> long "max-disjuncts" |

258 |
<> metavar "NUM" |

259 |
<> help "Maximum number of disjuncts per disjunction" |

260 |
<> showDefault |

261 |
) |

262 |
<*> option ( value 0.25 |

263 |
<> long "probability-atom" |

264 |
<> metavar "[0..1]" |

265 |
<> help "Probability of an atom occurring instead of a modality" |

266 |
<> showDefault |

267 |
) |

268 |
<*> flag True False |

269 |
( long "no-toplevel-conj" |

270 |
<> help "Don't generate conjunctions at the top-level" |

271 |
) |

272 |
<*> flag True False |

273 |
( long "no-toplevel-disj" |

274 |
<> help "Don't generate disjunctions at the top-level" |

275 |
) |

276 | |

277 | |

278 | |

279 | |

280 |
numFormulas :: Parser Nat |

281 |
numFormulas |

282 |
= option ( value 1 |

283 |
<> long "num-formulas" |

284 |
<> short 'n' |

285 |
<> metavar "NUM" |

286 |
<> help "Number of formulas to generate" |

287 |
<> showDefault |

288 |
) |

289 | |

290 |
seed :: Parser Int |

291 |
seed |

292 |
= option ( long "seed" |

293 |
<> metavar "NUM" |

294 |
<> help "Random seed" |

295 |
) |

296 |