jukebox 0.2.17 → 0.2.19
raw patch · 12 files changed
+424/−379 lines, 12 files
Files
- LICENSE +1/−1
- dist/build/Jukebox/TPTP/Lexer.hs +35/−33
- executable/Main.hs +69/−56
- jukebox.cabal +2/−2
- src/Jukebox/Form.hs +19/−9
- src/Jukebox/Options.hs +84/−138
- src/Jukebox/Provers/E.hs +5/−5
- src/Jukebox/Provers/SPASS.hs +2/−2
- src/Jukebox/TPTP/Parse.hs +4/−6
- src/Jukebox/TPTP/Parse/Core.hs +1/−1
- src/Jukebox/TPTP/Print.hs +13/−10
- src/Jukebox/Toolbox.hs +189/−116
LICENSE view
@@ -1,4 +1,4 @@-Copyright (c) 2009-2016, Nick Smallbone, Koen Claessen, Ann Lillieström+Copyright (c) 2009-2017, Nick Smallbone, Koen Claessen, Ann Lillieström All rights reserved.
dist/build/Jukebox/TPTP/Lexer.hs view
@@ -48,10 +48,7 @@ alex_deflt :: AlexAddr alex_deflt = AlexA# "\xff\xff\x2f\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x17\x00\x17\x00\x19\x00\x19\x00\x1b\x00\x1b\x00\x20\x00\x20\x00\x29\x00\x29\x00\x2e\x00\x2e\x00\x2f\x00\xff\xff\x2f\x00\x2f\x00\x31\x00\x30\x00\x30\x00\x31\x00\x39\x00\xff\xff\xff\xff\x39\x00\x39\x00\x04\x00\xff\xff\xff\xff\x04\x00\x04\x00\x2f\x00\x40\x00\x3f\x00\x3f\x00\x40\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x42\x00\x41\x00\xff\xff\x42\x00\x41\x00\x42\x00\x41\x00\xff\xff\x42\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff"# -alex_accept = listArray (0::Int,290) [AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccSkip,AlexAccSkip,AlexAccSkip,AlexAccSkip,AlexAcc 221,AlexAcc 220,AlexAcc 219,AlexAcc 218,AlexAcc 217,AlexAcc 216,AlexAcc 215,AlexAcc 214,AlexAcc 213,AlexAcc 212,AlexAcc 211,AlexAcc 210,AlexAcc 209,AlexAcc 208,AlexAcc 207,AlexAcc 206,AlexAcc 205,AlexAcc 204,AlexAcc 203,AlexAcc 202,AlexAcc 201,AlexAcc 200,AlexAcc 199,AlexAcc 198,AlexAcc 197,AlexAcc 196,AlexAcc 195,AlexAcc 194,AlexAcc 193,AlexAcc 192,AlexAcc 191,AlexAcc 190,AlexAcc 189,AlexAcc 188,AlexAcc 187,AlexAcc 186,AlexAcc 185,AlexAcc 184,AlexAcc 183,AlexAcc 182,AlexAcc 181,AlexAcc 180,AlexAcc 179,AlexAcc 178,AlexAcc 177,AlexAcc 176,AlexAcc 175,AlexAcc 174,AlexAcc 173,AlexAcc 172,AlexAcc 171,AlexAcc 170,AlexAcc 169,AlexAcc 168,AlexAcc 167,AlexAcc 166,AlexAcc 165,AlexAcc 164,AlexAcc 163,AlexAcc 162,AlexAcc 161,AlexAcc 160,AlexAcc 159,AlexAcc 158,AlexAcc 157,AlexAcc 156,AlexAcc 155,AlexAcc 154,AlexAcc 153,AlexAcc 152,AlexAcc 151,AlexAcc 150,AlexAcc 149,AlexAcc 148,AlexAcc 147,AlexAcc 146,AlexAcc 145,AlexAcc 144,AlexAcc 143,AlexAcc 142,AlexAcc 141,AlexAcc 140,AlexAcc 139,AlexAcc 138,AlexAcc 137,AlexAcc 136,AlexAcc 135,AlexAcc 134,AlexAcc 133,AlexAcc 132,AlexAcc 131,AlexAcc 130,AlexAcc 129,AlexAcc 128,AlexAcc 127,AlexAcc 126,AlexAcc 125,AlexAcc 124,AlexAcc 123,AlexAcc 122,AlexAcc 121,AlexAcc 120,AlexAcc 119,AlexAcc 118,AlexAcc 117,AlexAcc 116,AlexAcc 115,AlexAcc 114,AlexAcc 113,AlexAcc 112,AlexAcc 111,AlexAcc 110,AlexAcc 109,AlexAcc 108,AlexAcc 107,AlexAcc 106,AlexAcc 105,AlexAcc 104,AlexAcc 103,AlexAcc 102,AlexAcc 101,AlexAcc 100,AlexAcc 99,AlexAcc 98,AlexAcc 97,AlexAcc 96,AlexAcc 95,AlexAcc 94,AlexAcc 93,AlexAcc 92,AlexAcc 91,AlexAcc 90,AlexAcc 89,AlexAcc 88,AlexAcc 87,AlexAcc 86,AlexAcc 85,AlexAcc 84,AlexAcc 83,AlexAcc 82,AlexAcc 81,AlexAcc 80,AlexAcc 79,AlexAcc 78,AlexAcc 77,AlexAcc 76,AlexAcc 75,AlexAcc 74,AlexAcc 73,AlexAcc 72,AlexAcc 71,AlexAcc 70,AlexAcc 69,AlexAcc 68,AlexAcc 67,AlexAcc 66,AlexAcc 65,AlexAcc 64,AlexAcc 63,AlexAcc 62,AlexAcc 61,AlexAcc 60,AlexAcc 59,AlexAcc 58,AlexAcc 57,AlexAcc 56,AlexAcc 55,AlexAcc 54,AlexAcc 53,AlexAcc 52,AlexAcc 51,AlexAcc 50,AlexAcc 49,AlexAcc 48,AlexAcc 47,AlexAcc 46,AlexAcc 45,AlexAcc 44,AlexAcc 43,AlexAcc 42,AlexAccPred 41 (alexRightContext 60)(AlexAccNone),AlexAccPred 40 (alexRightContext 60)(AlexAccNone),AlexAcc 39,AlexAcc 38,AlexAcc 37,AlexAcc 36,AlexAcc 35,AlexAcc 34,AlexAcc 33,AlexAcc 32,AlexAcc 31,AlexAcc 30,AlexAcc 29,AlexAcc 28,AlexAcc 27,AlexAcc 26,AlexAcc 25,AlexAcc 24,AlexAcc 23,AlexAcc 22,AlexAcc 21,AlexAcc 20,AlexAcc 19,AlexAcc 18,AlexAcc 17,AlexAcc 16,AlexAcc 15,AlexAcc 14,AlexAcc 13,AlexAcc 12,AlexAcc 11,AlexAcc 10,AlexAcc 9,AlexAcc 8,AlexAcc 7,AlexAcc 6,AlexAcc 5,AlexAcc 4,AlexAcc 3,AlexAcc 2,AlexAcc 1,AlexAcc 0]--alex_actions = array (0::Int,222) [(221,alex_action_3),(220,alex_action_4),(219,alex_action_5),(218,alex_action_6),(217,alex_action_7),(216,alex_action_8),(215,alex_action_9),(214,alex_action_10),(213,alex_action_11),(212,alex_action_12),(211,alex_action_13),(210,alex_action_14),(209,alex_action_15),(208,alex_action_16),(207,alex_action_17),(206,alex_action_18),(205,alex_action_19),(204,alex_action_20),(203,alex_action_21),(202,alex_action_22),(201,alex_action_23),(200,alex_action_24),(199,alex_action_25),(198,alex_action_26),(197,alex_action_27),(196,alex_action_28),(195,alex_action_28),(194,alex_action_29),(193,alex_action_29),(192,alex_action_30),(191,alex_action_31),(190,alex_action_31),(189,alex_action_31),(188,alex_action_31),(187,alex_action_31),(186,alex_action_31),(185,alex_action_31),(184,alex_action_31),(183,alex_action_31),(182,alex_action_31),(181,alex_action_31),(180,alex_action_31),(179,alex_action_31),(178,alex_action_31),(177,alex_action_31),(176,alex_action_31),(175,alex_action_31),(174,alex_action_31),(173,alex_action_31),(172,alex_action_31),(171,alex_action_31),(170,alex_action_31),(169,alex_action_31),(168,alex_action_31),(167,alex_action_31),(166,alex_action_31),(165,alex_action_31),(164,alex_action_31),(163,alex_action_31),(162,alex_action_31),(161,alex_action_31),(160,alex_action_31),(159,alex_action_31),(158,alex_action_31),(157,alex_action_31),(156,alex_action_31),(155,alex_action_31),(154,alex_action_31),(153,alex_action_31),(152,alex_action_31),(151,alex_action_31),(150,alex_action_31),(149,alex_action_31),(148,alex_action_31),(147,alex_action_31),(146,alex_action_31),(145,alex_action_31),(144,alex_action_31),(143,alex_action_31),(142,alex_action_31),(141,alex_action_31),(140,alex_action_31),(139,alex_action_31),(138,alex_action_31),(137,alex_action_31),(136,alex_action_31),(135,alex_action_31),(134,alex_action_31),(133,alex_action_31),(132,alex_action_31),(131,alex_action_31),(130,alex_action_31),(129,alex_action_31),(128,alex_action_31),(127,alex_action_31),(126,alex_action_31),(125,alex_action_31),(124,alex_action_31),(123,alex_action_31),(122,alex_action_31),(121,alex_action_31),(120,alex_action_31),(119,alex_action_31),(118,alex_action_31),(117,alex_action_31),(116,alex_action_31),(115,alex_action_31),(114,alex_action_31),(113,alex_action_31),(112,alex_action_31),(111,alex_action_31),(110,alex_action_31),(109,alex_action_31),(108,alex_action_31),(107,alex_action_31),(106,alex_action_31),(105,alex_action_31),(104,alex_action_31),(103,alex_action_31),(102,alex_action_31),(101,alex_action_31),(100,alex_action_31),(99,alex_action_31),(98,alex_action_31),(97,alex_action_31),(96,alex_action_31),(95,alex_action_31),(94,alex_action_31),(93,alex_action_31),(92,alex_action_31),(91,alex_action_31),(90,alex_action_31),(89,alex_action_31),(88,alex_action_31),(87,alex_action_31),(86,alex_action_31),(85,alex_action_31),(84,alex_action_31),(83,alex_action_31),(82,alex_action_31),(81,alex_action_31),(80,alex_action_31),(79,alex_action_31),(78,alex_action_31),(77,alex_action_31),(76,alex_action_31),(75,alex_action_31),(74,alex_action_31),(73,alex_action_31),(72,alex_action_31),(71,alex_action_31),(70,alex_action_31),(69,alex_action_31),(68,alex_action_31),(67,alex_action_31),(66,alex_action_31),(65,alex_action_31),(64,alex_action_31),(63,alex_action_31),(62,alex_action_31),(61,alex_action_31),(60,alex_action_31),(59,alex_action_31),(58,alex_action_31),(57,alex_action_31),(56,alex_action_31),(55,alex_action_31),(54,alex_action_31),(53,alex_action_31),(52,alex_action_31),(51,alex_action_31),(50,alex_action_31),(49,alex_action_31),(48,alex_action_31),(47,alex_action_31),(46,alex_action_31),(45,alex_action_31),(44,alex_action_32),(43,alex_action_33),(42,alex_action_34),(41,alex_action_35),(40,alex_action_35),(39,alex_action_36),(38,alex_action_37),(37,alex_action_37),(36,alex_action_38),(35,alex_action_38),(34,alex_action_39),(33,alex_action_40),(32,alex_action_41),(31,alex_action_42),(30,alex_action_43),(29,alex_action_44),(28,alex_action_45),(27,alex_action_46),(26,alex_action_47),(25,alex_action_48),(24,alex_action_49),(23,alex_action_50),(22,alex_action_51),(21,alex_action_52),(20,alex_action_53),(19,alex_action_54),(18,alex_action_55),(17,alex_action_56),(16,alex_action_57),(15,alex_action_58),(14,alex_action_59),(13,alex_action_60),(12,alex_action_61),(11,alex_action_62),(10,alex_action_63),(9,alex_action_64),(8,alex_action_65),(7,alex_action_66),(6,alex_action_67),(5,alex_action_68),(4,alex_action_69),(3,alex_action_70),(2,alex_action_71),(1,alex_action_72),(0,alex_action_73)]-+alex_accept = listArray (0::Int,290) [AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccSkip,AlexAccSkip,AlexAccSkip,AlexAccSkip,AlexAcc (alex_action_3),AlexAcc (alex_action_4),AlexAcc (alex_action_5),AlexAcc (alex_action_6),AlexAcc (alex_action_7),AlexAcc (alex_action_8),AlexAcc (alex_action_9),AlexAcc (alex_action_10),AlexAcc (alex_action_11),AlexAcc (alex_action_12),AlexAcc (alex_action_13),AlexAcc (alex_action_14),AlexAcc (alex_action_15),AlexAcc (alex_action_16),AlexAcc (alex_action_17),AlexAcc (alex_action_18),AlexAcc (alex_action_19),AlexAcc (alex_action_20),AlexAcc (alex_action_21),AlexAcc (alex_action_22),AlexAcc (alex_action_23),AlexAcc (alex_action_24),AlexAcc (alex_action_25),AlexAcc (alex_action_26),AlexAcc (alex_action_27),AlexAcc (alex_action_28),AlexAcc (alex_action_28),AlexAcc (alex_action_29),AlexAcc (alex_action_29),AlexAcc (alex_action_30),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_31),AlexAcc (alex_action_32),AlexAcc (alex_action_33),AlexAcc (alex_action_34),AlexAccPred (alex_action_35) (alexRightContext 60)(AlexAccNone),AlexAccPred (alex_action_35) (alexRightContext 60)(AlexAccNone),AlexAcc (alex_action_36),AlexAcc (alex_action_37),AlexAcc (alex_action_37),AlexAcc (alex_action_38),AlexAcc (alex_action_38),AlexAcc (alex_action_39),AlexAcc (alex_action_40),AlexAcc (alex_action_41),AlexAcc (alex_action_42),AlexAcc (alex_action_43),AlexAcc (alex_action_44),AlexAcc (alex_action_45),AlexAcc (alex_action_46),AlexAcc (alex_action_47),AlexAcc (alex_action_48),AlexAcc (alex_action_49),AlexAcc (alex_action_50),AlexAcc (alex_action_51),AlexAcc (alex_action_52),AlexAcc (alex_action_53),AlexAcc (alex_action_54),AlexAcc (alex_action_55),AlexAcc (alex_action_56),AlexAcc (alex_action_57),AlexAcc (alex_action_58),AlexAcc (alex_action_59),AlexAcc (alex_action_60),AlexAcc (alex_action_61),AlexAcc (alex_action_62),AlexAcc (alex_action_63),AlexAcc (alex_action_64),AlexAcc (alex_action_65),AlexAcc (alex_action_66),AlexAcc (alex_action_67),AlexAcc (alex_action_68),AlexAcc (alex_action_69),AlexAcc (alex_action_70),AlexAcc (alex_action_71),AlexAcc (alex_action_72),AlexAcc (alex_action_73)] {-# LINE 97 "src/Jukebox/TPTP/Lexer.x" #-} data Pos = Pos {-# UNPACK #-} !Word {-# UNPACK #-} !Word deriving Show@@ -279,7 +276,7 @@ {-# LINE 1 "templates/GenericTemplate.hs" #-} {-# LINE 1 "<built-in>" #-} {-# LINE 1 "<command-line>" #-}-{-# LINE 9 "<command-line>" #-}+{-# LINE 11 "<command-line>" #-} # 1 "/usr/include/stdc-predef.h" 1 3 4 # 17 "/usr/include/stdc-predef.h" 3 4@@ -326,8 +323,8 @@ -{-# LINE 9 "<command-line>" #-}-{-# LINE 1 "/usr/lib/ghc-8.0.1/include/ghcversion.h" #-}+{-# LINE 11 "<command-line>" #-}+{-# LINE 1 "/usr/lib/ghc/include/ghcversion.h" #-} @@ -345,8 +342,8 @@ -{-# LINE 9 "<command-line>" #-}-{-# LINE 1 "/tmp/ghc688_0/ghc_2.h" #-}+{-# LINE 11 "<command-line>" #-}+{-# LINE 1 "/tmp/ghc3c55_0/ghc_2.h" #-} @@ -527,7 +524,7 @@ -{-# LINE 9 "<command-line>" #-}+{-# LINE 11 "<command-line>" #-} {-# LINE 1 "templates/GenericTemplate.hs" #-} -- ----------------------------------------------------------------------------- -- ALEX TEMPLATE@@ -579,7 +576,7 @@ {-# INLINE alexIndexInt32OffAddr #-}-alexIndexInt32OffAddr (AlexA# arr) off =+alexIndexInt32OffAddr (AlexA# arr) off = #ifdef WORDS_BIGENDIAN narrow32Int# i where@@ -625,30 +622,30 @@ alexScanUser user input (I# (sc)) = case alex_scan_tkn user input 0# input sc AlexNone of- (AlexNone, input') ->- case alexGetByte input of- Nothing ->+ (AlexNone, input') ->+ case alexGetByte input of+ Nothing -> AlexEOF- Just _ ->+ Just _ -> AlexError input' - (AlexLastSkip input'' len, _) ->+ (AlexLastSkip input'' len, _) -> - AlexSkip input'' len+ AlexSkip input'' len - (AlexLastAcc k input''' len, _) ->+ (AlexLastAcc k input''' len, _) -> - AlexToken input''' len (alex_actions ! k)+ AlexToken input''' len k -- Push the input through the DFA, remembering the most recent accepting@@ -656,13 +653,13 @@ alex_scan_tkn user orig_input len input s last_acc = input `seq` -- strict in the input- let- new_acc = (check_accs (alex_accept `quickIndex` (I# (s))))+ let + new_acc = (check_accs (alex_accept `quickIndex` (I# (s)))) in new_acc `seq` case alexGetByte input of Nothing -> (new_acc, input)- Just (c, new_input) ->+ Just (c, new_input) -> @@ -671,7 +668,7 @@ base = alexIndexInt32OffAddr alex_base s offset = (base +# ord_c) check = alexIndexInt16OffAddr alex_check offset-+ new_s = if GTE(offset,0#) && EQ(check,ord_c) then alexIndexInt16OffAddr alex_table offset else alexIndexInt16OffAddr alex_deflt s@@ -701,18 +698,23 @@ = check_accs rest -data AlexLastAcc+data AlexLastAcc a = AlexNone- | AlexLastAcc !Int !AlexInput !Int- | AlexLastSkip !AlexInput !Int+ | AlexLastAcc a !AlexInput !Int+ | AlexLastSkip !AlexInput !Int -data AlexAcc user+instance Functor AlexLastAcc where+ fmap _ AlexNone = AlexNone+ fmap f (AlexLastAcc x y z) = AlexLastAcc (f x) y z+ fmap _ (AlexLastSkip x y) = AlexLastSkip x y++data AlexAcc a user = AlexAccNone- | AlexAcc Int+ | AlexAcc a | AlexAccSkip - | AlexAccPred Int (AlexAccPred user) (AlexAcc user)- | AlexAccSkipPred (AlexAccPred user) (AlexAcc user)+ | AlexAccPred a (AlexAccPred user) (AlexAcc a user)+ | AlexAccSkipPred (AlexAccPred user) (AlexAcc a user) type AlexAccPred user = user -> AlexInput -> Int -> AlexInput -> Bool @@ -722,16 +724,16 @@ alexAndPred p1 p2 user in1 len in2 = p1 user in1 len in2 && p2 user in1 len in2 ---alexPrevCharIsPred :: Char -> AlexAccPred _+--alexPrevCharIsPred :: Char -> AlexAccPred _ alexPrevCharIs c _ input _ _ = c == alexInputPrevChar input alexPrevCharMatches f _ input _ _ = f (alexInputPrevChar input) ---alexPrevCharIsOneOfPred :: Array Char Bool -> AlexAccPred _+--alexPrevCharIsOneOfPred :: Array Char Bool -> AlexAccPred _ alexPrevCharIsOneOf arr _ input _ _ = arr ! alexInputPrevChar input --alexRightContext :: Int -> AlexAccPred _-alexRightContext (I# (sc)) user _ _ input =+alexRightContext (I# (sc)) user _ _ input = case alex_scan_tkn user input 0# input sc AlexNone of (AlexNone, _) -> False _ -> True
executable/Main.hs view
@@ -8,67 +8,80 @@ import Control.Applicative import Data.Monoid #endif+import Data.List+import System.Exit+import System.Environment -tools = mconcat [fof, cnf, smt, monotonox, guessmodel]+main = do+ prog <- getProgName+ args <- getArgs+ let+ progTool = prog ++ " <toolname>"+ help =+ printHelp ExitSuccess $+ intercalate [""] $+ [usageText progTool "Jukebox, a first-order logic toolbox"] +++ [["<toolname> can be any of the following:"] +++ [ " " ++ name tool ++ " - " ++ description tool+ | tool <- tools, name tool `notElem` map name internal ]] +++ [["For more information about each tool, run " ++ progTool ++ " --help."]]+ usage msg = printError prog msg+ case args of+ [] -> help+ ["--help"] -> help+ ["--version"] ->+ putStrLn $ "Jukebox version " ++ VERSION_jukebox+ (('-':_):_) -> usage "Expected a tool name as first argument"+ (arg:args) ->+ case [tool | tool <- tools, name tool == arg] of+ [] -> usage ("No such tool " ++ arg)+ [tool] ->+ join $+ parseCommandLineWithArgs+ (prog ++ " " ++ name tool) args (description tool) (pipeline tool) -fof = tool info pipeline- where- info = Tool "fof" "Jukebox TFF-to-FOF translator" "1"- "Translate from TFF (typed) to FOF (untyped)"- pipeline =- greetingBox info =>>- allFilesBox <*>- (parseProblemBox =>>=- toFofBox =>>=- prettyPrintProblemBox)+data Tool =+ Tool {+ name :: String,+ description :: String,+ pipeline :: OptionParser (IO ()) } -monotonox = tool info pipeline- where- info = Tool "monotonox" "Monotonox" "1"- "Monotonicity analysis"- pipeline =- greetingBox info =>>- allFilesBox <*>- (parseProblemBox =>>=- clausifyBox =>>=- oneConjectureBox =>>=- monotonicityBox =>>=- writeFileBox)+tools = [fof, cnf, smt, monotonox, guessmodel]+internal = [guessmodel] -smt = tool info pipeline- where- info = Tool "smt" "Jukebox TFF-to-SMTLIB translator" "1"- "Translate from TFF to SMTLIB"- pipeline =- greetingBox info =>>- allFilesBox <*>- (parseProblemBox =>>=- prettyPrintProblemSMTBox)+fof =+ Tool "fof" "Translate a problem from TFF (typed) to FOF (untyped)" $+ forAllFilesBox <*>+ (readProblemBox =>>=+ toFofBox =>>=+ printProblemBox) -cnf = tool info pipeline- where- info = Tool "cnf" "Jukebox clausifier" "1"- "Clausify a problem"- pipeline =- greetingBox info =>>- allFilesBox <*>- (parseProblemBox =>>=- clausifyBox =>>=- oneConjectureBox =>>=- prettyPrintClausesBox)+monotonox =+ Tool "monotonox" "Analyse a problem for monotonicity" $+ forAllFilesBox <*>+ (readProblemBox =>>=+ clausifyBox =>>=+ oneConjectureBox =>>=+ showMonotonicityBox =>>=+ writeFileBox) -guessmodel = tool info pipeline- where- info = Tool "guessmodel" "Infinite model guesser" "1"- "Guess an infinite model"- pipeline =- greetingBox info =>>- allFilesBox <*>- (parseProblemBox =>>=- guessModelBox =>>=- prettyPrintProblemBox)+smt =+ Tool "smt" "Translate a problem from TPTP format to SMTLIB format" $+ forAllFilesBox <*>+ (readProblemBox =>>=+ printProblemSMTBox) -jukebox = Tool "jukebox" "Jukebox" "1"- "A first-order logic toolbox"+cnf =+ Tool "cnf" "Clausify a TPTP (TFF or FOF) problem" $+ forAllFilesBox <*>+ (readProblemBox =>>=+ clausifyBox =>>=+ oneConjectureBox =>>=+ printClausesBox) -main = join (parseCommandLine jukebox tools)+guessmodel =+ Tool "guessmodel" "Guess an infinite model (internal use)" $+ forAllFilesBox <*>+ (readProblemBox =>>=+ guessModelBox =>>=+ printProblemBox)
jukebox.cabal view
@@ -1,10 +1,10 @@ Name: jukebox-Version: 0.2.17+Version: 0.2.19 Cabal-version: >= 1.8 Build-type: Simple Author: Nick Smallbone Maintainer: nicsma@chalmers.se-Copyright: 2009-2016 Nick Smallbone, Koen Claessen, Ann Lillieström+Copyright: 2009-2017 Nick Smallbone, Koen Claessen, Ann Lillieström Category: Logic
src/Jukebox/Form.hs view
@@ -274,13 +274,13 @@ CNF { axioms :: [Input Clause], conjectures :: [[Input Clause]],- satisfiable :: String,- unsatisfiable :: String }+ satisfiable :: Answer,+ unsatisfiable :: Answer } toCNF :: [Input Clause] -> [[Input Clause]] -> CNF-toCNF axioms [] = CNF axioms [[]] "Satisfiable" "Unsatisfiable"-toCNF axioms [conjecture] = CNF axioms [conjecture] "CounterSatisfiable" "Theorem"-toCNF axioms conjectures = CNF axioms conjectures "GaveUp" "Theorem"+toCNF axioms [] = CNF axioms [[]] (Sat Satisfiable) (Unsat Unsatisfiable)+toCNF axioms [conjecture] = CNF axioms [conjecture] (Sat CounterSatisfiable) (Unsat Theorem)+toCNF axioms conjectures = CNF axioms conjectures (NoAnswer GaveUp) (Unsat Theorem) newtype Clause = Clause (Bind [Literal]) @@ -309,15 +309,25 @@ data Kind = Axiom String | Conjecture | Question deriving (Eq, Ord) -data Answer = Satisfiable | Unsatisfiable | NoAnswer NoAnswerReason+data Answer = Sat SatReason | Unsat UnsatReason | NoAnswer NoAnswerReason deriving (Eq, Ord) +data NoAnswerReason = GaveUp | Timeout deriving (Eq, Ord, Show)+data SatReason = Satisfiable | CounterSatisfiable deriving (Eq, Ord, Show)+data UnsatReason = Unsatisfiable | Theorem deriving (Eq, Ord, Show)+ instance Show Answer where- show Satisfiable = "Satisfiable"- show Unsatisfiable = "Unsatisfiable"+ show (Sat reason) = show reason+ show (Unsat reason) = show reason show (NoAnswer x) = show x -data NoAnswerReason = GaveUp | Timeout deriving (Eq, Ord, Show)+explainAnswer :: Answer -> String+explainAnswer (Sat Satisfiable) = "the axioms are consistent"+explainAnswer (Sat CounterSatisfiable) = "the conjecture is false"+explainAnswer (Unsat Unsatisfiable) = "the axioms are contradictory"+explainAnswer (Unsat Theorem) = "the conjecture is true"+explainAnswer (NoAnswer GaveUp) = "couldn't solve the problem"+explainAnswer (NoAnswer Timeout) = "ran out of time while solving the problem" data Input a = Input { tag :: Tag,
src/Jukebox/Options.hs view
@@ -1,8 +1,13 @@+-- Command-line option parsing using applicative functors.+-- Parsers are represented as values of type OptionParser a,+-- and run using the function+-- parseCommandLine :: String -> OptionParser a -> IO a.+-- OptionParsers are built from ArgParsers, which parse a single+-- option (e.g. --verbosity 3).+ {-# LANGUAGE FlexibleContexts, CPP #-} module Jukebox.Options where -import Control.Arrow((***))-import Control.Monad(mplus) import Data.Char import Data.List import System.Environment@@ -33,11 +38,10 @@ Annotated (d `mappend` d') (p `mappend` p') ------------------------------------------------------------------------- Parsing of single arguments (e.g. integers)--- and single flags (e.g. --verbosity 3).+-- The ArgParser type: parsing of single flags. -type ArgParser = Annotated ArgDesc SeqParser-type ArgDesc = String -- description, e.g. "<number>"+type ArgParser = Annotated String SeqParser+ -- annotated with a description, e.g. "<number>" -- Called SeqParser because <*> is sequential composition. data SeqParser a = SeqParser@@ -52,10 +56,13 @@ SeqParser a c <*> SeqParser a' c' = SeqParser (a + a') f where f xs = c xs <*> c' (drop a xs) -arg :: ArgDesc -> String -> (String -> Maybe a) -> ArgParser a+----------------------------------------------------------------------+-- Combinators for building ArgParsers.++arg :: String -> String -> (String -> Maybe a) -> ArgParser a arg desc err f = Annotated desc (SeqParser 1 c) where c [] = Left (Mistake err)- c (x:_) | "--" `isPrefixOf` x = Left (Mistake err)+ c (x:_) | "-" `isPrefixOf` x = Left (Mistake err) c (x:_) = case f x of Nothing -> Left (Mistake err)@@ -81,7 +88,7 @@ w = takeWhile (/= ',') s r = tail (dropWhile (/= ',') s) -argName :: ArgParser FilePath+argName :: ArgParser String argName = arg "<name>" "expected a name" Just argNums :: ArgParser [Int]@@ -116,14 +123,22 @@ argUsage code err = Annotated [] (SeqParser 0 (const (Left (Usage code err)))) ------------------------------------------------------------------------- Parsing of whole command lines.+-- The OptionParser type: parsing of whole command lines. type OptionParser = Annotated [Flag] ParParser +-- The help information for a flag.+data Flag = Flag+ { flagName :: String,+ flagGroup :: String,+ flagHelp :: [String],+ flagArgs :: String } deriving (Eq, Show)+ -- Called ParParser because <*> is parallel composition. -- In other words, in f <*> x, f and x both see the whole command line. -- We want this when parsing command lines because--- it doesn't matter what order we write the options in.+-- it doesn't matter what order we write the options in,+-- and because f and x might understand the same flags. data ParParser a = ParParser { val :: IO a, -- impure so we can put system information in our options records peek :: [String] -> ParseResult a }@@ -183,13 +198,10 @@ await :: String -> a -> ([String] -> ParseResult a) -> ParParser a await flag def f = awaitP (\x -> "--" ++ flag == x) def (const f) -data Flag = Flag- { flagName :: String,- flagGroup :: String,- flagHelp :: [String],- flagArgs :: String } deriving (Eq, Show)+----------------------------------------------------------------------+-- Combinators for building OptionParsers. --- From a flag name and and argument parser, produce an OptionParser.+-- From a flag name and description and argument parser, produce an OptionParser. flag :: String -> [String] -> a -> ArgParser a -> OptionParser a flag name help def (Annotated desc (SeqParser args f)) = Annotated [desc'] (await name def g)@@ -204,6 +216,11 @@ await name () (const (Error (Mistake ("Option --" ++ name ++ " occurred twice")))) +-- A boolean flag.+bool :: String -> [String] -> OptionParser Bool+bool name help = flag name help False (pure True)++-- A variant of 'flag' that allows repeated flags. manyFlags :: String -> [String] -> ArgParser a -> OptionParser [a] manyFlags name help (Annotated desc (SeqParser args f)) = fmap reverse (Annotated [desc'] (go []))@@ -215,11 +232,11 @@ Left (Usage code err) -> Error (Usage code err) Right x -> Yes args (go (x:xs)) --- Read filenames from the command line.+-- A parser that reads all file names from the command line. filenames :: OptionParser [String] filenames = Annotated [] (from []) where from xs = awaitP p xs (f xs)- p x = not ("--" `isPrefixOf` x)+ p x = not ("-" `isPrefixOf` x) || x == "-" f xs y _ = Yes 0 (from (xs ++ [y])) -- Take a value from the environment.@@ -227,143 +244,72 @@ io m = Annotated [] p where p = ParParser m (const (No p)) --- A boolean flag.-bool :: String -> [String] -> OptionParser Bool-bool name help = flag name help False (pure True)-+-- Change the group associated with a set of flags. inGroup :: String -> OptionParser a -> OptionParser a inGroup x (Annotated fls f) = Annotated [fl{ flagGroup = x } | fl <- fls] f -------------------------------------------------------------------------- Selecting a particular tool.--type ToolParser = Annotated [Tool] PrefixParser-data Tool = Tool- { toolProgName :: String,- toolName :: String,- toolVersion :: String,- toolHelp :: String }--newtype PrefixParser a = PrefixParser (String -> Maybe (Tool, ParParser a))--instance Functor PrefixParser where- fmap f (PrefixParser g) = PrefixParser (fmap (id *** fmap f) . g)--instance Monoid (PrefixParser a) where- mempty = PrefixParser (const Nothing)- PrefixParser f `mappend` PrefixParser g =- PrefixParser (\xs -> f xs `mplus` g xs)--runPref :: PrefixParser a -> [String] -> Either Error (IO a)-runPref _ [] = Left (Mistake "Expected a tool name")-runPref (PrefixParser f) (x:xs) =- case f x of- Nothing -> Left (Mistake ("No such tool " ++ x))- Just (t, p) ->- case runPar p xs of- Left (Mistake x) -> Left (Usage (ExitFailure 1) (argError t x))- Left (Usage code x) -> Left (Usage code x)- Right x -> Right x--tool :: Tool -> OptionParser a -> ToolParser a-tool t p =- Annotated [t] (PrefixParser f)- where f x | x == toolProgName t = Just (t, parser p')- f _ = Nothing- p' = p <* versionParser <* helpParser- helpParser =- inGroup "Miscellaneous options" $- flag "help" ["Show this help text."] () (argUsage ExitSuccess (help t p'))- versionParser =- inGroup "Miscellaneous options" $- flag "version" ["Print the version number."] () (argUsage ExitSuccess [greeting t])---- Use the program name as a tool name if possible.-getEffectiveArgs :: ToolParser a -> IO [String]-getEffectiveArgs (Annotated tools _) = do- progName <-- case tools of- [tool] -> return (toolProgName tool)- _ -> getProgName- args <- getArgs- if progName `elem` map toolProgName tools- then return (progName:args)- else return args--parseCommandLine :: Tool -> ToolParser a -> IO a-parseCommandLine t p = do- let p' =- case p of- Annotated [_] _ -> p- _ -> versionTool t `mappend` helpTool t p `mappend` p- args <- getEffectiveArgs p'- case runPref (parser p') args of- Left (Mistake err) -> printHelp (ExitFailure 1) (argError t err)- Left (Usage code err) -> printHelp code err- Right x -> x+-- Add a --version flag.+version :: String -> OptionParser a -> OptionParser a+version x p =+ p <*+ inGroup "Miscellaneous options"+ (flag "version" ["Show the version number."] ()+ (argUsage ExitSuccess [x])) ------------------------------------------------------------------------- Help screens.+-- Help screens, error messages and so on. printHelp :: ExitCode -> [String] -> IO a printHelp code xs = do- mapM_ (hPutStrLn stderr ) xs+ mapM_ (hPutStrLn stderr) xs exitWith code -argError :: Tool -> String -> [String]-argError t err = [- greeting t,- err ++ ". Try --help."- ]--usageTool :: Tool -> String -> [String] -> String -> ToolParser a-usageTool t0 flag msg bit = tool (Tool flag' flag' flag' "0") p- where p = Annotated [] (ParParser (printHelp ExitSuccess msg)- (const (Error (Usage (ExitFailure 1) msg'))))- flag' = "--" ++ flag- msg' = [- greeting t0,- "Didn't expect any arguments after " ++ flag' ++ ".",- "Try " ++ toolProgName t0 ++ " <toolname> " ++ flag' ++ " if you want " ++ bit ++ " a particular tool."- ]--versionTool :: Tool -> ToolParser a-versionTool t0 = usageTool t0 "version" [greeting t0] "the version of"+printError :: String -> String -> IO a+printError name err =+ printHelp (ExitFailure 1) $+ [err ++ ".", "Try " ++ name ++ " --help."] -helpTool :: Tool -> ToolParser a -> ToolParser a-helpTool t0 p = usageTool t0 "help" help "help for"- where help = intercalate [""] [- [greeting t0],- usage t0 "<toolname> ",- ["Please run " ++ toolProgName t0 ++ " <toolname> --help, where <toolname> can be any of the following:"],- intercalate [""] [ justify (toolProgName t) [toolHelp t] | t <- descr p ]]+help :: String -> String -> OptionParser a -> OptionParser a+help name description p = p'+ where+ p' =+ p <*+ (inGroup "Miscellaneous options" $+ flag "help" ["Show this help text."] () (argUsage ExitSuccess (helpText name description p'))) -help :: Tool -> OptionParser a -> [String]-help t p =- intercalate [""]- [[greeting t],- usage t "",- intercalate [""] [- [flagGroup f0 ++ ":"] ++- concat [justify ("--" ++ flagName f ++ " " ++ flagArgs f) (flagHelp f) | f <- fs]- | fs@(f0:_) <- groups (nub (descr p)) ]]+usageText :: String -> String -> [String]+usageText name descr =+ [descr ++ ".",+ "Usage: " ++ name ++ " <option>* <file>*, where <file> should be in TPTP format."] +helpText :: String -> String -> OptionParser a -> [String]+helpText name description p =+ intercalate [""] $+ [usageText name description] +++ [[flagGroup f0 ++ ":"] +++ concat [justify ("--" ++ flagName f ++ " " ++ flagArgs f) (flagHelp f) | f <- fs]+ | fs@(f0:_) <- groups (nub (descr p)) ] where groups [] = [] groups (f:fs) = (f:[f' | f' <- fs, flagGroup f == flagGroup f']): groups [f' | f' <- fs, flagGroup f /= flagGroup f'] -greeting :: Tool -> String-greeting t = toolName t ++ ", version " ++ toolVersion t ++ "."--usage :: Tool -> String -> [String]-usage t opts = [- "Usage: " ++ toolProgName t ++ " " ++ opts ++ "<option>* <file>*",- toolHelp t ++ ".",- "",- "<file> should be in TPTP format."- ]- justify :: String -> [String] -> [String] justify name help = [" " ++ name] ++ map (" " ++) help++----------------------------------------------------------------------+-- Running the parser.++parseCommandLine :: String -> OptionParser a -> IO a+parseCommandLine description p = do+ name <- getProgName+ args <- getArgs+ parseCommandLineWithArgs name args description p++parseCommandLineWithArgs :: String -> [String] -> String -> OptionParser a -> IO a+parseCommandLineWithArgs name args description p = do+ case runPar (parser (help name description p)) args of+ Left (Mistake err) -> printError name err+ Left (Usage code err) -> printHelp code err+ Right x -> x
src/Jukebox/Provers/E.hs view
@@ -10,7 +10,7 @@ import Jukebox.TPTP.Parsec hiding (run) import Jukebox.TPTP.Parse.Core hiding (newFunction, Term) import Jukebox.TPTP.Print-import Jukebox.TPTP.Lexer hiding (Normal, keyword, Axiom, Var)+import Jukebox.TPTP.Lexer hiding (Normal, keyword, Axiom, Var, Theorem) import Data.Maybe import qualified Data.Map.Strict as Map import Data.Map(Map)@@ -69,10 +69,10 @@ funMap = Map.fromList [(show (name x), x) | x <- functions prob] result = lines str status = head $- [Satisfiable | "# SZS status Satisfiable" <- result] ++- [Satisfiable | "# SZS status CounterSatisfiable" <- result] ++- [Unsatisfiable | "# SZS status Unsatisfiable" <- result] ++- [Unsatisfiable | "# SZS status Theorem" <- result] +++ [Sat Satisfiable | "# SZS status Satisfiable" <- result] +++ [Sat CounterSatisfiable | "# SZS status CounterSatisfiable" <- result] +++ [Unsat Unsatisfiable | "# SZS status Unsatisfiable" <- result] +++ [Unsat Theorem | "# SZS status Theorem" <- result] ++ [NoAnswer Timeout | "# SZS status ResourceOut" <- result] ++ [NoAnswer Timeout | "# SZS status Timeout" <- result] ++ [NoAnswer Timeout | "# SZS status MemyOut" <- result] ++
src/Jukebox/Provers/SPASS.hs view
@@ -49,6 +49,6 @@ extractAnswer :: String -> Answer extractAnswer result = head $- [ Unsatisfiable | "SPASS beiseite: Proof found." <- lines result ] ++- [ Satisfiable | "SPASS beiseite: Completion found." <- lines result ] +++ [ Unsat Unsatisfiable | "SPASS beiseite: Proof found." <- lines result ] +++ [ Sat Satisfiable | "SPASS beiseite: Completion found." <- lines result ] ++ [ NoAnswer Timeout ]
src/Jukebox/TPTP/Parse.hs view
@@ -19,11 +19,11 @@ Parser.ParseStalled loc _ _ -> error ("Include directive found at " ++ show loc) -parseProblem :: (FilePath -> IO ()) -> [FilePath] -> FilePath -> IO (Either String (Problem Form))-parseProblem found dirs name = parseProblemWith found (findFileTPTP dirs) name+parseProblem :: [FilePath] -> FilePath -> IO (Either String (Problem Form))+parseProblem dirs name = parseProblemWith (findFileTPTP dirs) name -parseProblemWith :: (FilePath -> IO ()) -> (FilePath -> IO (Maybe FilePath)) -> FilePath -> IO (Either String (Problem Form))-parseProblemWith found findFile name =+parseProblemWith :: (FilePath -> IO (Maybe FilePath)) -> FilePath -> IO (Either String (Problem Form))+parseProblemWith findFile name = runExceptT $ do file <- readInFile (Parser.Location "<command line>" 0 0) name process (Parser.parseProblem name file)@@ -35,7 +35,6 @@ readInFile _ "-" = ExceptT $ do- liftIO (found "standard input") fmap Right getContents `catch` \(e :: IOException) -> return (Left (show e)) readInFile pos name = do@@ -45,7 +44,6 @@ err pos ("File '" ++ name ++ "' not found") Just file -> ExceptT $ do- liftIO (found file) fmap Right (readFile file) `catch` \(e :: IOException) -> return (Left (show e))
src/Jukebox/TPTP/Parse/Core.hs view
@@ -25,7 +25,7 @@ keyword, defined, kind) import qualified Jukebox.TPTP.Lexer as L import qualified Jukebox.Form as Form-import Jukebox.Form hiding (tag, kind, Axiom, Conjecture, Question, newFunction, TypeOf(..), run)+import Jukebox.Form hiding (tag, kind, Axiom, Conjecture, Question, newFunction, TypeOf(..), run, Theorem) import qualified Jukebox.Name as Name -- The parser monad
src/Jukebox/TPTP/Print.hs view
@@ -20,18 +20,19 @@ pPrintClauses :: Problem Clause -> Doc pPrintClauses prob0- | isFof prob = vcat (map (pPrintInput "cnf" pPrint) prob)- | otherwise = pPrintProblem (map (fmap toForm) prob0)+ | isReallyFof prob = vcat (map (pPrintInput "cnf" pPrint) prob)+ | otherwise = pPrintProblem "tcf" (map (fmap toForm) prob) where prob = prettyNames prob0 showClauses :: Problem Clause -> String showClauses = show . pPrintClauses -pPrintProblem :: Problem Form -> Doc-pPrintProblem prob0+pPrintProblem :: String -> Problem Form -> Doc+-- "kind" is only used if the problem is typed+pPrintProblem kind prob0 | isReallyFof prob = vcat (map (pPrintInput "fof" (pPrintFof 0)) prob)- | otherwise = vcat (pPrintDecls prob ++ map (pPrintInput "tff" (pPrintTff 0)) prob)+ | otherwise = vcat (pPrintDecls kind prob ++ map (pPrintInput kind (pPrintTff 0)) prob) where prob = prettyNames prob0 @@ -107,7 +108,7 @@ pPrintAnnotProof :: [(Input Form, (String, [Doc]))] -> Doc pPrintAnnotProof annots0 = vcat $- [ vcat (pPrintDecls inps) | not (isReallyFof inps) ] +++ [ vcat (pPrintDecls "tff" inps) | not (isReallyFof inps) ] ++ [ pPrintClause (family x) (tag inp) k (pp x:rest) | (inp, (k, rest)) <- annots, let x = what inp ]@@ -130,7 +131,7 @@ pPrintTff 0 x showProblem :: Problem Form -> String-showProblem = show . pPrintProblem+showProblem = show . pPrintProblem "tff" isReallyFof :: Symbolic a => a -> Bool isReallyFof = all p . types@@ -140,8 +141,8 @@ p _ = False i = name "$i" -pPrintDecls :: Problem Form -> [Doc]-pPrintDecls prob =+pPrintDecls :: String -> Problem Form -> [Doc]+pPrintDecls kind prob = map typeDecl (usort (types prob)) ++ map funcDecl (usort (functions prob)) where@@ -151,8 +152,10 @@ i = name "$i" funcDecl (f ::: ty) = typeClause f (pPrint ty)++ typeClause :: Show a => a -> Doc -> Doc typeClause name ty =- pPrintClause "tff" "type" "type"+ pPrintClause kind "type" "type" [text (escapeAtom (show name)) <> colon <+> ty] instance Pretty a => Pretty (Input a) where
src/Jukebox/Toolbox.hs view
@@ -1,3 +1,4 @@+-- Components ("boxes") which can be put together to make tools. {-# LANGUAGE RecordWildCards, CPP #-} module Jukebox.Toolbox where @@ -20,7 +21,11 @@ #if __GLASGOW_HASKELL__ < 710 import Control.Applicative #endif+import Data.IORef +----------------------------------------------------------------------+-- Some standard flags.+ data GlobalFlags = GlobalFlags { quiet :: Bool }@@ -33,74 +38,188 @@ bool "quiet" ["Do not print any informational output."] -(=>>=) :: (Monad m, Applicative f) => f (a -> m b) -> f (b -> m c) -> f (a -> m c)-f =>>= g = (>=>) <$> f <*> g-infixl 1 =>>= -- same as >=>+data TSTPFlags =+ TSTPFlags {+ tstp :: Bool }+ deriving Show -(=>>) :: (Monad m, Applicative f) => f (m a) -> f (m b) -> f (m b)-x =>> y = (>>) <$> x <*> y-infixl 1 =>> -- same as >>+tstpFlags :: OptionParser TSTPFlags+tstpFlags =+ inGroup "Output options" $+ TSTPFlags <$>+ bool "tstp"+ ["Produce TSTP-friendly output."] -greetingBox :: Tool -> OptionParser (IO ())-greetingBox t = greetingBoxIO t <$> globalFlags+----------------------------------------------------------------------+-- Printing output messages. -greetingBoxIO :: Tool -> GlobalFlags -> IO ()-greetingBoxIO t globals = message globals (greeting t)+-- Print a message as a TPTP comment.+comment :: String -> IO ()+comment msg = mapM_ putStrLn ["% " ++ line | line <- lines msg] -message :: GlobalFlags -> String -> IO ()-message globals msg =- putStr (comment globals msg)+-- Do something only when output is enabled.+quietly :: GlobalFlags -> IO () -> IO ()+quietly globals action = unless (quiet globals) action -comment :: GlobalFlags -> String -> String-comment globals msg- | quiet globals = ""- | otherwise =- unlines ["% " ++ line | line <- lines msg]+----------------------------------------------------------------------+-- Combinators for boxes. -allFilesBox :: OptionParser ((FilePath -> IO ()) -> IO ())-allFilesBox = flip allFiles <$> filenames+-- Boxes typically have the type OptionParser (a -> IO b).+-- The following two combinators chain boxes together.+(=>>=) :: OptionParser (a -> IO b) -> OptionParser (b -> IO c) -> OptionParser (a -> IO c)+f =>>= g = (>=>) <$> f <*> g+infixl 1 =>>= -- same fixity as >=> -allFiles :: (FilePath -> IO ()) -> [FilePath] -> IO ()-allFiles _ [] = do+(=>>) :: OptionParser (IO a) -> OptionParser (IO b) -> OptionParser (IO b)+x =>> y = (>>) <$> x <*> y+infixl 1 =>> -- same fixity as >>++----------------------------------------------------------------------+-- Process all files that were passed in on the command line.++forAllFilesBox :: OptionParser ((FilePath -> IO ()) -> IO ())+forAllFilesBox = forAllFiles <$> filenames++forAllFiles :: [FilePath] -> (FilePath -> IO ()) -> IO ()+forAllFiles [] _ = do hPutStrLn stderr "No input files specified! Try --help."+ hPutStrLn stderr "You can use \"-\" to read from standard input." exitWith (ExitFailure 1)-allFiles f xs = mapM_ f xs+forAllFiles xs f = mapM_ f xs -parseProblemBox :: OptionParser (FilePath -> IO (Problem Form))-parseProblemBox = parseProblemIO <$> globalFlags <*> findFileFlags+----------------------------------------------------------------------+-- Read in a single problem. -parseProblemIO :: GlobalFlags -> [FilePath] -> FilePath -> IO (Problem Form)-parseProblemIO flags dirs f = do- let found file = message flags $ "Reading " ++ file ++ "..."- r <- parseProblem found dirs f+readProblemBox :: OptionParser (FilePath -> IO (Problem Form))+readProblemBox = readProblem <$> findFileFlags++readProblem :: [FilePath] -> FilePath -> IO (Problem Form)+readProblem dirs f = do+ r <- parseProblem dirs f case r of Left err -> do hPutStrLn stderr err exitWith (ExitFailure 1) Right x -> return x -clausifyBox :: OptionParser (Problem Form -> IO CNF)-clausifyBox = clausifyIO <$> globalFlags <*> clausifyFlags+----------------------------------------------------------------------+-- Write output to a file. -clausifyIO :: GlobalFlags -> ClausifyFlags -> Problem Form -> IO CNF-clausifyIO globals flags prob = do- return $! clausify flags prob+printProblemBox :: OptionParser (Problem Form -> IO ())+printProblemBox = prettyPrintIO showProblem <$> writeFileBox -toFofBox :: OptionParser (Problem Form -> IO (Problem Form))-toFofBox = toFofIO <$> globalFlags <*> clausifyBox <*> schemeBox+printProblemSMTBox :: OptionParser (Problem Form -> IO ())+printProblemSMTBox = prettyPrintIO SMT.showProblem <$> writeFileBox +printClausesBox :: OptionParser (Problem Clause -> IO ())+printClausesBox = prettyPrintIO showClauses <$> writeFileBox++prettyPrintIO :: (a -> String) -> (String -> IO ()) -> a -> IO ()+prettyPrintIO shw write prob = do+ write (shw prob ++ "\n")++writeFileBox :: OptionParser (String -> IO ())+writeFileBox =+ inGroup "Output options" $+ flag "output"+ ["Where to write the output file (defaults to stdout)."]+ putStr+ (fmap myWriteFile argFile)+ where myWriteFile "/dev/null" _ = return ()+ myWriteFile "-" contents = putStr contents+ myWriteFile file contents = writeFile file contents++----------------------------------------------------------------------+-- Clausify a problem.++clausifyBox :: OptionParser (Problem Form -> IO CNF)+clausifyBox =+ (\flags prob -> return $! clausify flags prob) <$> clausifyFlags++----------------------------------------------------------------------+-- Make sure that the problem only has one conjecture.+ oneConjectureBox :: OptionParser (CNF -> IO (Problem Clause))-oneConjectureBox = pure oneConjecture+oneConjectureBox = oneConjecture <$> flags+ where+ flags =+ inGroup "Input and clausifier options" $+ flag "conjecture"+ ["If the problem has multiple conjectures, take only this one",+ "(conjectures are numbered from 1)"]+ Nothing (Just <$> argNum) -oneConjecture :: CNF -> IO (Problem Clause)-oneConjecture cnf = run cnf f- where f (CNF cs [cs'] _ _) = return (return (cs ++ cs'))- f _ = return $ do- hPutStrLn stderr "Error: more than one conjecture found in input problem"- exitWith (ExitFailure 1)+oneConjecture :: Maybe Int -> CNF -> IO (Problem Clause)+oneConjecture conj cnf =+ run cnf $ \(CNF axioms obligs _ _) ->+ case conj of+ Just n ->+ if n <= length obligs then choose axioms (obligs !! (n-1))+ else err ["Conjecture number out of bounds:",+ "problem after clausification has " ++ show (length obligs) ++ " conjectures"]+ Nothing ->+ case obligs of+ [cs] -> choose axioms cs+ _ ->+ err ["Can't handle more than one conjecture in input problem!",+ "This problem has " ++ show (length obligs) ++ " conjectures.",+ "Try using the --conjecture flag."]+ where+ err msgs = return $ do+ mapM_ (hPutStrLn stderr) msgs+ exitWith (ExitFailure 1) -toFofIO :: GlobalFlags -> (Problem Form -> IO CNF) -> Scheme -> Problem Form -> IO (Problem Form)-toFofIO globals clausify scheme f = do+ choose axioms cs = return (return (axioms ++ cs))++----------------------------------------------------------------------+-- Solve all conjectures in a problem and report the final SZS status.++-- A solver is given a problem in CNF and should return an answer.+--+-- It is also given a function of type IO () -> IO ().+-- Wrapping an action in this function delays the action until after+-- the answer is printed; this can be useful for e.g. printing a proof+-- when the prover might be running under a timeout.+type Solver = (IO () -> IO ()) -> Problem Clause -> IO Answer++forAllConjecturesBox :: OptionParser (Solver -> CNF -> IO ())+forAllConjecturesBox = forAllConjectures <$> tstpFlags++forAllConjectures :: TSTPFlags -> Solver -> CNF -> IO ()+forAllConjectures (TSTPFlags tstp) solve CNF{..} = do+ todo <- newIORef (return ())+ loop 1 todo conjectures+ where loop _ todo [] =+ result todo unsatisfiable+ loop i todo (c:cs) = do+ when multi $ do+ join (readIORef todo)+ writeIORef todo (return ())+ answer <- solve (\x -> modifyIORef todo (>> x)) (axioms ++ c)+ when multi $ do+ putStrLn $ "Partial result (" ++ part i ++ "): " ++ show answer+ putStrLn ""+ case answer of+ Sat _ -> result todo satisfiable+ Unsat _ -> loop (i+1) todo cs+ NoAnswer x -> result todo (NoAnswer x)+ multi = length conjectures > 1+ part i = show i ++ "/" ++ show (length conjectures)+ result todo x = do+ when tstp $ do+ putStrLn ("% SZS status " ++ show x)+ putStrLn ""+ join (readIORef todo)+ putStrLn ("RESULT: " ++ show x ++ " (" ++ explainAnswer x ++ ").")++----------------------------------------------------------------------+-- Convert a problem from TFF to FOF.++toFofBox :: OptionParser (Problem Form -> IO (Problem Form))+toFofBox = toFof <$> clausifyBox <*> schemeBox++toFof :: (Problem Form -> IO CNF) -> Scheme -> Problem Form -> IO (Problem Form)+toFof clausify scheme f = do CNF{..} <- clausify f -- In some cases we might get better results by considering each -- problem (axioms + conjecture) separately, but no big deal.@@ -124,56 +243,37 @@ where choose "guards" _flags = guards choose "tags" flags = tags flags -monotonicityBox :: OptionParser (Problem Clause -> IO String)-monotonicityBox = monotonicity <$> globalFlags--monotonicity :: GlobalFlags -> Problem Clause -> IO String-monotonicity globals cs = do- m <- monotone (map what cs)- let info (ty, Nothing) = [base ty ++ ": not monotone"]- info (ty, Just m) =- [prettyShow ty ++ ": monotone"] ++- concat- [ case ext of- CopyExtend -> []- TrueExtend -> [" " ++ base p ++ " true-extended"]- FalseExtend -> [" " ++ base p ++ " false-extended"]- | (p, ext) <- Map.toList m ]-- return (unlines (concat (map info (Map.toList m))))+----------------------------------------------------------------------+-- Analyse monotonicity. +-- Annotate types with monotonicity information. annotateMonotonicityBox :: OptionParser (Problem Clause -> IO (Problem Clause))-annotateMonotonicityBox = (\globals x -> do- annotateMonotonicity x) <$> globalFlags--prettyPrintProblemBox :: OptionParser (Problem Form -> IO ())-prettyPrintProblemBox = prettyPrintIO showProblem <$> globalFlags <*> writeFileBox--prettyPrintProblemSMTBox :: OptionParser (Problem Form -> IO ())-prettyPrintProblemSMTBox = prettyPrintIO SMT.showProblem <$> globalFlags <*> writeFileBox+annotateMonotonicityBox = pure annotateMonotonicity -prettyPrintClausesBox :: OptionParser (Problem Clause -> IO ())-prettyPrintClausesBox = prettyPrintIO showClauses <$> globalFlags <*> writeFileBox+showMonotonicityBox :: OptionParser (Problem Clause -> IO String)+showMonotonicityBox =+ pure $ \cs -> do+ m <- monotone (map what cs)+ let info (ty, Nothing) = [base ty ++ ": not monotone"]+ info (ty, Just m) =+ [prettyShow ty ++ ": monotone"] +++ concat+ [ case ext of+ CopyExtend -> []+ TrueExtend -> [" " ++ base p ++ " true-extended"]+ FalseExtend -> [" " ++ base p ++ " false-extended"]+ | (p, ext) <- Map.toList m ] -prettyPrintIO :: (a -> String) -> GlobalFlags -> (String -> IO ()) -> a -> IO ()-prettyPrintIO shw globals write prob = do- write (shw prob ++ "\n")+ return (unlines (concat (map info (Map.toList m)))) -writeFileBox :: OptionParser (String -> IO ())-writeFileBox =- inGroup "Output options" $- flag "output"- ["Where to write the output file (defaults to stdout)."]- putStr- (fmap myWriteFile argFile)- where myWriteFile "/dev/null" _ = return ()- myWriteFile "-" contents = putStr contents- myWriteFile file contents = writeFile file contents+----------------------------------------------------------------------+-- Guess an infinite model. guessModelBox :: OptionParser (Problem Form -> IO (Problem Form)) guessModelBox = inGroup "Options for the model guesser:" $- guessModelIO <$> expansive <*> universe+ (\expansive univ prob -> return (guessModel expansive univ prob))+ <$> expansive <*> universe where universe = choose <$> flag "universe" ["Which universe to find the model in (defaults to peano)."]@@ -185,38 +285,11 @@ ["Allow a function to construct 'new' terms in its base case."] (arg "<function>" "expected a function name" Just) -guessModelIO :: [String] -> Universe -> Problem Form -> IO (Problem Form)-guessModelIO expansive univ prob = return (guessModel expansive univ prob)--allObligsBox :: OptionParser ((Problem Clause -> IO Answer) -> CNF -> IO ())-allObligsBox = allObligsIO <$> globalFlags--allObligsIO globals solve CNF{..} = loop 1 conjectures- where loop _ [] =- result unsatisfiable- "PROVED.\nThe conjecture is true or the axioms are contradictory."- loop i (c:cs) = do- when multi $ message globals $ "Part " ++ part i- answer <- solve (axioms ++ c)- when multi $ message globals $ "Partial result (" ++ part i ++ "): " ++ show answer- case answer of- Satisfiable ->- result satisfiable- "DISPROVED.\nThe conjecture is not true and the axioms are consistent."- Unsatisfiable -> loop (i+1) cs- NoAnswer x ->- result (show x)- "GAVE UP.\nCouldn't prove or disprove the conjecture."- multi = length conjectures > 1- part i = show i ++ "/" ++ show (length conjectures)- result x hint = do- putStrLn ("% SZS status " ++ x)- unless (quiet globals) $ putStrLn ""- message globals hint+----------------------------------------------------------------------+-- Infer types. inferBox :: OptionParser (Problem Clause -> IO (Problem Clause, Type -> Type))-inferBox = (\globals prob -> do- return (run prob inferTypes)) <$> globalFlags+inferBox = pure (\prob -> return (run prob inferTypes)) printInferredBox :: OptionParser ((Problem Clause, Type -> Type) -> IO (Problem Clause)) printInferredBox = pure $ \(prob, rep) -> do