| Line No. | Rev | Author | Line |
|---|---|---|---|
| 1 | 11 | paulosilva | |
| 2 | |||
| 3 | |||
| 4 | imports Module Whitespace Comment | ||
| 5 | 14 | paulosilva | exports |
| 6 | 11 | paulosilva | context-free start-symbols Module |
| 7 | 22 | paulosilva | |
| 8 | 11 | paulosilva | |
| 9 | 12 | paulosilva | imports Identifier Axiom Theorem GaloisDef Definition Strategy |
| 10 | 15 | paulosilva | exports |
| 11 | 12 | paulosilva | sorts Module |
| 12 | context-free syntax | ||
| 13 | Header {Block ";"}* -> Module | ||
| 14 | 16 | paulosilva | |
| 15 | 12 | paulosilva | |
| 16 | |||
| 17 | 16 | paulosilva | |
| 18 | Theorem -> Block | ||
| 19 | GaloisDef -> Block | ||
| 20 | Definition -> Block | ||
| 21 | Strategy -> Block | ||
| 22 | |||
| 23 | 12 | paulosilva | |
| 24 | 11 | paulosilva | imports Identifier |
| 25 | exports | ||
| 26 | sorts Type | ||
| 27 | context-free syntax | ||
| 28 | "(" Type ")" -> Type { bracket } | ||
| 29 | Variable -> Type | ||
| 30 | "One" -> Type | ||
| 31 | "Bool" -> Type | ||
| 32 | "Char" -> Type | ||
| 33 | "String" -> Type | ||
| 34 | "Int" -> Type | ||
| 35 | "Float" -> Type | ||
| 36 | |||
| 37 | |||
| 38 | "Set" Type -> Type | ||
| 39 | "List" Type -> Type | ||
| 40 | Type "<-|" Type -> Type { right } | ||
| 41 | Type "><" Type -> Type { right } | ||
| 42 | Type "-|-" Type -> Type { right } | ||
| 43 | Type "<-" Type -> Type { right } | ||
| 44 | Type "<->" Type -> Type { right } | ||
| 45 | Type "~~" Type -> Type { noassoc } | ||
| 46 | "Ord" Type -> Type | ||
| 47 | "Expr" Type -> Type | ||
| 48 | |||
| 49 | |||
| 50 | "Maybe" Type -> Type > | ||
| 51 | {"Set" Type -> Type | ||
| 52 | "List" Type -> Type} > | ||
| 53 | Type "<-|" Type -> Type > | ||
| 54 | {Type "><" Type -> Type | ||
| 55 | Type "-|-" Type -> Type} > | ||
| 56 | {Type "<-" Type -> Type | ||
| 57 | Type "<->" Type -> Type} > | ||
| 58 | Type "~~" Type -> Type > | ||
| 59 | "Ord" Type -> Type > | ||
| 60 | "Expr" Type -> Type | ||
| 61 | |||
| 62 | |||
| 63 | 12 | paulosilva | imports Fork Identifier Relator Interface |
| 64 | 15 | paulosilva | exports |
| 65 | 12 | paulosilva | sorts Expression |
| 66 | context-free syntax | ||
| 67 | |||
| 68 | |||
| 69 | Fork "<=" Fork -> Expression | ||
| 70 | |||
| 71 | |||
| 72 | |||
| 73 | imports Identifier | ||
| 74 | exports | ||
| 75 | sorts Fork | ||
| 76 | context-free syntax | ||
| 77 | "(" Fork ")" -> Fork { bracket } | ||
| 78 | Identifier -> Fork | ||
| 79 | Variable -> Fork | ||
| 80 | |||
| 81 | |||
| 82 | "Top" -> Fork | ||
| 83 | "Bot" -> Fork | ||
| 84 | "~" Fork -> Fork | ||
| 85 | Fork "*" -> Fork | ||
| 86 | Fork "/\\" Fork -> Fork { left } | ||
| 87 | Fork "\\/" Fork -> Fork { left } | ||
| 88 | Fork "." Fork -> Fork { left } | ||
| 89 | Fork "/*\\" Fork -> Fork { left } | ||
| 90 | |||
| 91 | |||
| 92 | Fork "*" -> Fork > | ||
| 93 | "~" Fork -> Fork > | ||
| 94 | Fork "/*\\" Fork -> Fork > | ||
| 95 | { Fork "/\\" Fork -> Fork | ||
| 96 | Fork "\\/" Fork -> Fork} > | ||
| 97 | Fork "." Fork -> Fork | ||
| 98 | |||
| 99 | |||
| 100 | imports Fork | ||
| 101 | exports | ||
| 102 | sorts Fork | ||
| 103 | context-free syntax | ||
| 104 | Fork "><" Fork -> Fork { left } | ||
| 105 | Fork "-|-" Fork -> Fork { left } | ||
| 106 | "Maybe" Fork -> Fork | ||
| 107 | "List" Fork -> Fork | ||
| 108 | "Set" Fork -> Fork | ||
| 109 | "Map" Fork -> Fork | ||
| 110 | |||
| 111 | |||
| 112 | 16 | paulosilva | Fork "*" -> Fork > |
| 113 | {"Maybe" Fork -> Fork | ||
| 114 | "List" Fork -> Fork | ||
| 115 | "Set" Fork -> Fork | ||
| 116 | "Map" Fork -> Fork} > | ||
| 117 | {Fork "><" Fork -> Fork | ||
| 118 | Fork "-|-" Fork -> Fork} > | ||
| 119 | Fork "." Fork -> Fork | ||
| 120 | |||
| 121 | |||
| 122 | |||
| 123 | 12 | paulosilva | imports Identifier |
| 124 | exports | ||
| 125 | sorts Function | ||
| 126 | context-free syntax | ||
| 127 | "(" Function ")" -> Function { bracket } | ||
| 128 | Identifier -> Function | ||
| 129 | Variable -> Function | ||
| 130 | |||
| 131 | |||
| 132 | Function "." Function -> Function { left } | ||
| 133 | |||
| 134 | |||
| 135 | imports Identifier | ||
| 136 | exports | ||
| 137 | sorts Order | ||
| 138 | context-free syntax | ||
| 139 | "(" Order ")" -> Order { bracket } | ||
| 140 | Identifier -> Order | ||
| 141 | Variable -> Order | ||
| 142 | |||
| 143 | |||
| 144 | Order "." Order -> Order { left } | ||
| 145 | Order "*" -> Order | ||
| 146 | |||
| 147 | |||
| 148 | imports Identifier | ||
| 149 | exports | ||
| 150 | sorts Galois | ||
| 151 | context-free syntax | ||
| 152 | "(" Galois ")" -> Galois { bracket } | ||
| 153 | Identifier -> Galois | ||
| 154 | Variable -> Galois | ||
| 155 | |||
| 156 | |||
| 157 | Galois "." Galois -> Galois { left } | ||
| 158 | Galois "*" -> Galois | ||
| 159 | |||
| 160 | |||
| 161 | 14 | paulosilva | imports Order Function |
| 162 | exports | ||
| 163 | sorts Fork | ||
| 164 | context-free syntax | ||
| 165 | "Ord" Order -> Fork | ||
| 166 | "Fun" Function -> Fork | ||
| 167 | |||
| 168 | |||
| 169 | imports Galois Function Order Identifier | ||
| 170 | exports | ||
| 171 | sorts GaloisDef | ||
| 172 | context-free syntax | ||
| 173 | "Galois" Identifier ":=" Function Function Order Order -> GaloisDef | ||
| 174 | |||
| 175 | |||
| 176 | 12 | paulosilva | imports Identifier Expression |
| 177 | exports | ||
| 178 | sorts Axiom | ||
| 179 | context-free syntax | ||
| 180 | "Axiom" Identifier ":=" Expression -> Axiom | ||
| 181 | |||
| 182 | |||
| 183 | imports Identifier Expression Step | ||
| 184 | 15 | paulosilva | exports |
| 185 | 12 | paulosilva | sorts Theorem |
| 186 | context-free syntax | ||
| 187 | "Theorem" Identifier ":=" Expression Hypothesis? Proof -> Theorem | ||
| 188 | |||
| 189 | |||
| 190 | "{" Step "}" -> Proof | ||
| 191 | |||
| 192 | |||
| 193 | imports Identifier Type Fork | ||
| 194 | exports | ||
| 195 | sorts Definition | ||
| 196 | context-free syntax | ||
| 197 | Identifier ":" Type (":=" Fork)? -> Definition | ||
| 198 | |||
| 199 | |||
| 200 | imports Identifier Step | ||
| 201 | 15 | paulosilva | exports |
| 202 | 12 | paulosilva | sorts Strategy |
| 203 | context-free syntax | ||
| 204 | "Strategy" Identifier ":=" Step -> Strategy | ||
| 205 | |||
| 206 | |||
| 207 | 13 | paulosilva | imports Identifier Galois |
| 208 | exports | ||
| 209 | sorts Derivation | ||
| 210 | context-free syntax | ||
| 211 | "inv" Derivation2 -> Derivation | ||
| 212 | Derivation2 -> Derivation | ||
| 213 | |||
| 214 | |||
| 215 | "distr_low" Galois -> Derivation2 | ||
| 216 | "distr_up" Galois -> Derivation2 | ||
| 217 | "monot_up" Galois -> Derivation2 | ||
| 218 | "monot_low" Galois -> Derivation2 | ||
| 219 | "top_preserving" Galois -> Derivation2 | ||
| 220 | "bot_preserving" Galois -> Derivation2 | ||
| 221 | "cancel_up" Galois -> Derivation2 | ||
| 222 | "cancel_low" Galois -> Derivation2 | ||
| 223 | "free" Function -> Derivation2 | ||
| 224 | Identifier -> Derivation2 | ||
| 225 | |||
| 226 | |||
| 227 | imports Derivation | ||
| 228 | exports | ||
| 229 | sorts Combinator | ||
| 230 | context-free syntax | ||
| 231 | "(" Combinator ")" -> Combinator { bracket } | ||
| 232 | |||
| 233 | |||
| 234 | "fail" -> Combinator | ||
| 235 | Combinator "&" Combinator -> Combinator { right } | ||
| 236 | Combinator "|" Combinator -> Combinator { right } | ||
| 237 | Combinator "||" Combinator -> Combinator { right } | ||
| 238 | "many" Combinator -> Combinator | ||
| 239 | "many1" Combinator -> Combinator | ||
| 240 | "try" Combinator -> Combinator | ||
| 241 | "once" Combinator -> Combinator | ||
| 242 | "top_down" Combinator -> Combinator | ||
| 243 | "bottom_up" Combinator -> Combinator | ||
| 244 | "innermost" Combinator -> Combinator | ||
| 245 | "all" Combinator -> Combinator | ||
| 246 | "one" Combinator -> Combinator | ||
| 247 | Derivation -> Combinator | ||
| 248 | |||
| 249 | |||
| 250 | imports Combinator | ||
| 251 | exports | ||
| 252 | sorts Step | ||
| 253 | context-free syntax | ||
| 254 | Combinator -> Step | ||
| 255 | "ind_left" Order -> Step | ||
| 256 | "ind_right" Order -> Step | ||
| 257 | "left" -> Step | ||
| 258 | "right" -> Step | ||
| 259 | "qed" -> Step | ||
| 260 | Step ">" Step -> Step { right } | ||
| 261 | 22 | paulosilva | |
| 262 | 13 | paulosilva | |
| 263 | 11 | paulosilva | exports |
| 264 | sorts Identifier Variable | ||
| 265 | |||
| 266 | |||
| 267 | [A-Z][A-Za-z\_0-9\']* -> Identifier | ||
| 268 | |||
| 269 | |||
| 270 | |||
| 271 | |||
| 272 | Identifier -/- [A-Za-z\_0-9\'] | ||
| 273 | Variable -/- [A-Za-z\_0-9\'] | ||
| 274 | |||
| 275 | |||
| 276 | 16 | paulosilva | "One" -> Identifier { reject } |
| 277 | "Bool" -> Identifier { reject } | ||
| 278 | "Char" -> Identifier { reject } | ||
| 279 | "String" -> Identifier { reject } | ||
| 280 | "Int" -> Identifier { reject } | ||
| 281 | "Float" -> Identifier { reject } | ||
| 282 | "Maybe" -> Identifier { reject } | ||
| 283 | "Set" -> Identifier { reject } | ||
| 284 | "List" -> Identifier { reject } | ||
| 285 | "Ord" -> Identifier { reject } | ||
| 286 | "Expr" -> Identifier { reject } | ||
| 287 | |||
| 288 | |||
| 289 | "Bot" -> Identifier { reject } | ||
| 290 | "Id" -> Identifier { reject } | ||
| 291 | "Map" -> Identifier { reject } | ||
| 292 | "Ord" -> Identifier { reject } | ||
| 293 | "Fun" -> Identifier { reject } | ||
| 294 | |||
| 295 | |||
| 296 | "module" -> Variable { reject } | ||
| 297 | "import" -> Identifier { reject } | ||
| 298 | "import" -> Variable { reject } | ||
| 299 | "Axiom" -> Identifier { reject } | ||
| 300 | "Theorem" -> Identifier { reject } | ||
| 301 | "Strategy" -> Identifier { reject } | ||
| 302 | |||
| 303 | |||
| 304 | "inv" -> Variable { reject } | ||
| 305 | "shunt" -> Identifier { reject } | ||
| 306 | "shunt" -> Variable { reject } | ||
| 307 | "distr_low" -> Identifier { reject } | ||
| 308 | "distr_low" -> Variable { reject } | ||
| 309 | "distr_up" -> Identifier { reject } | ||
| 310 | "distr_up" -> Variable { reject } | ||
| 311 | "monot_up" -> Identifier { reject } | ||
| 312 | "monot_up" -> Variable { reject } | ||
| 313 | "monot_low" -> Identifier { reject } | ||
| 314 | "monot_low" -> Variable { reject } | ||
| 315 | "top_preserving" -> Identifier { reject } | ||
| 316 | "top_preserving" -> Variable { reject } | ||
| 317 | "bot_preserving" -> Identifier { reject } | ||
| 318 | "bot_preserving" -> Variable { reject } | ||
| 319 | "cancel_up" -> Identifier { reject } | ||
| 320 | "cancel_up" -> Variable { reject } | ||
| 321 | "cancel_low" -> Identifier { reject } | ||
| 322 | "cancel_low" -> Variable { reject } | ||
| 323 | "free" -> Identifier { reject } | ||
| 324 | "free" -> Variable { reject } | ||
| 325 | |||
| 326 | |||
| 327 | "nop" -> Variable { reject } | ||
| 328 | "fail" -> Identifier { reject } | ||
| 329 | "fail" -> Variable { reject } | ||
| 330 | "many" -> Identifier { reject } | ||
| 331 | "many" -> Variable { reject } | ||
| 332 | "many1" -> Identifier { reject } | ||
| 333 | "many1" -> Variable { reject } | ||
| 334 | "try" -> Identifier { reject } | ||
| 335 | "try" -> Variable { reject } | ||
| 336 | "once" -> Identifier { reject } | ||
| 337 | "once" -> Variable { reject } | ||
| 338 | "top_down" -> Identifier { reject } | ||
| 339 | "top_down" -> Variable { reject } | ||
| 340 | "bottom_up" -> Identifier { reject } | ||
| 341 | "bottom_up" -> Variable { reject } | ||
| 342 | "innermost" -> Identifier { reject } | ||
| 343 | "innermost" -> Variable { reject } | ||
| 344 | "all" -> Identifier { reject } | ||
| 345 | "all" -> Variable { reject } | ||
| 346 | "one" -> Identifier { reject } | ||
| 347 | "one" -> Variable { reject } | ||
| 348 | |||
| 349 | |||
| 350 | "ind_left" -> Variable { reject } | ||
| 351 | "ind_right" -> Identifier { reject } | ||
| 352 | "ind_right" -> Variable { reject } | ||
| 353 | "left" -> Identifier { reject } | ||
| 354 | "left" -> Variable { reject } | ||
| 355 | "right" -> Identifier { reject } | ||
| 356 | "right" -> Variable { reject } | ||
| 357 | "qed" -> Identifier { reject } | ||
| 358 | "qed" -> Variable { reject } | ||
| 359 | |||
| 360 | |||
| 361 | "One" "Bool" "Char" "String" "Int" "Float" "Maybe" "Set" | ||
| 362 | "List" "Ord" "Expr" "Top" "Bot" "Id" "Map" "Ord" "Fun" | ||
| 363 | "module" "import" "Axiom" "Theorem" "Strategy" "inv" | ||
| 364 | "shunt" "distr_low" "distr_up" "monot_up" "monot_low" | ||
| 365 | "top_preserving" "bot_preserving" "cancel_up" "cancel_low" | ||
| 366 | "free" "nop" "fail" "many" "many1" "try" "once" "top_down" | ||
| 367 | "bottom_up" "innermost" "all" "one" "ind_left" "ind_right" | ||
| 368 | "left" "right" "qed" -/- [a-zA-Z0-9\_\'] | ||
| 369 | |||
| 370 | |||
| 371 | 11 | paulosilva | exports |
| 372 | lexical syntax | ||
| 373 | [\ \t\n\r] -> LAYOUT | ||
| 374 | |||
| 375 | |||
| 376 | LAYOUT? -/- [\ \t\n\r] | ||
| 377 | |||
| 378 | 14 | paulosilva | |
| 379 | exports | ||
| 380 | lexical syntax | ||
| 381 | "--" ~[\n]* "\n" -> LAYOUT | ||
| 382 | |||
| 383 | 16 | paulosilva | |
| 384 | 22 | paulosilva | [\-] -> Dash |
| 385 | |||
| 386 | 16 | paulosilva | |
| 387 | 22 | paulosilva | Dash -/- [\}] |
| 388 |