| Line No. | Rev | Author | Line |
|---|---|---|---|
| 1 | 9 | paulosilva | |
| 2 | |||
| 3 | |||
| 4 | imports Identifier | ||
| 5 | exports | ||
| 6 | sorts Type | ||
| 7 | context-free syntax | ||
| 8 | "TVar" Identifier -> Type | ||
| 9 | "One" -> Type | ||
| 10 | "Bool" -> Type | ||
| 11 | "Char" -> Type | ||
| 12 | "String" -> Type | ||
| 13 | "Int" -> Type | ||
| 14 | "Float" -> Type | ||
| 15 | "Prod" Type Type -> Type | ||
| 16 | "Either" Type Type -> Type | ||
| 17 | "Maybe" Type -> Type | ||
| 18 | "List" Type -> Type | ||
| 19 | "Set" Type -> Type | ||
| 20 | "Map" Type -> Type | ||
| 21 | "Fun" Type Type -> Type | ||
| 22 | "Rel" Type Type -> Type | ||
| 23 | "Ord" Type -> Type | ||
| 24 | "GC" Type -> Type | ||
| 25 | |||
| 26 | |||
| 27 | imports Type | ||
| 28 | imports Identifier | ||
| 29 | exports | ||
| 30 | sorts R | ||
| 31 | context-free syntax | ||
| 32 | "REF" Identifier -> R | ||
| 33 | "BOT" -> R | ||
| 34 | "TOP" -> R | ||
| 35 | "NEG" -> R | ||
| 36 | "MEET" R R -> R | ||
| 37 | "JOIN" R R -> R | ||
| 38 | "ID" -> R | ||
| 39 | "CONV" R -> R | ||
| 40 | "COMP" R R -> R | ||
| 41 | "SPLIT" R R -> R | ||
| 42 | "ORD" R -> R | ||
| 43 | "FUN" R -> R | ||
| 44 | "LEFTSEC" R R -> R | ||
| 45 | "RIGHTSEC" R R -> R | ||
| 46 | "APPLY" R R -> R | ||
| 47 | "DEF" Identifier R Type -> R | ||
| 48 | "Var" Identifier -> R | ||
| 49 | "PROD" R R -> R | ||
| 50 | "EITHER" R R -> R | ||
| 51 | "MAYBE" R -> R | ||
| 52 | "LIST" R -> R | ||
| 53 | "SET" R -> R | ||
| 54 | "MAP" R -> R | ||
| 55 | "REYNOLDS" R R -> R | ||
| 56 | "FId" -> R | ||
| 57 | "FComp" R R -> R | ||
| 58 | "OId" -> R | ||
| 59 | "OComp" R R -> R | ||
| 60 | "OConv" R -> R | ||
| 61 | "OProd" R -> R | ||
| 62 | "OMeet" R -> R | ||
| 63 | "OMax" R -> R | ||
| 64 | "OMin" R -> R | ||
| 65 | "GDef" Identifier R R R R -> R | ||
| 66 | "GId" -> R | ||
| 67 | "GComp" R R -> R | ||
| 68 | "GConv" R -> R | ||
| 69 | "GLAdj" R -> R | ||
| 70 | "GUAdj" R -> R | ||
| 71 | "GLOrd" R -> R | ||
| 72 | "GUOrd" R -> R | ||
| 73 | |||
| 74 | |||
| 75 | imports R | ||
| 76 | imports Step | ||
| 77 | imports Identifier | ||
| 78 | exports | ||
| 79 | sorts Law Theorem | ||
| 80 | context-free syntax | ||
| 81 | "EQUIV" Identifier R R -> Law | ||
| 82 | "IMPL" Identifier R R -> Law | ||
| 83 | |||
| 84 | |||
| 85 | "Theorem" Identifier "IMPL" R R Step -> Theorem | ||
| 86 | |||
| 87 | |||
| 88 | imports R | ||
| 89 | imports Law | ||
| 90 | imports Identifier | ||
| 91 | exports | ||
| 92 | context-free start-symbols Module | ||
| 93 | 10 | paulosilva | sorts Module |
| 94 | 9 | paulosilva | context-free syntax |
| 95 | "module" Identifier {Law | Theorem | R ";"}* -> Module | ||
| 96 | 10 | paulosilva | |
| 97 | 9 | paulosilva | |
| 98 | imports R | ||
| 99 | imports Combinator | ||
| 100 | exports | ||
| 101 | sorts Step | ||
| 102 | context-free syntax | ||
| 103 | Combinator -> Step | ||
| 104 | "indirect" "up" R -> Step | ||
| 105 | "indirect" "low" R -> Step | ||
| 106 | "indirect" "end" -> Step | ||
| 107 | "left" -> Step | ||
| 108 | "qed" -> Step | ||
| 109 | "right" -> Step | ||
| 110 | "seqc" Step Step -> Step | ||
| 111 | |||
| 112 | |||
| 113 | |||
| 114 | imports Law | ||
| 115 | imports Step | ||
| 116 | imports Derivation | ||
| 117 | imports Identifier | ||
| 118 | exports | ||
| 119 | sorts Command | ||
| 120 | context-free syntax | ||
| 121 | "abort" -> Command | ||
| 122 | "assume" Law -> Command | ||
| 123 | "auto" -> Command | ||
| 124 | "browse" Identifier -> Command | ||
| 125 | Step -> Command | ||
| 126 | "define" R -> Command | ||
| 127 | "derive" Derivation -> Command | ||
| 128 | "help" -> Command | ||
| 129 | "hint" -> Command | ||
| 130 | "info" Identifier -> Command | ||
| 131 | "load" Identifier -> Command | ||
| 132 | "modules" -> Command | ||
| 133 | "prove" Law -> Command | ||
| 134 | "quit" -> Command | ||
| 135 | "reload" -> Command | ||
| 136 | "restart" -> Command | ||
| 137 | "rules" -> Command | ||
| 138 | "save" -> Command | ||
| 139 | "show" -> Command | ||
| 140 | "type" -> Command | ||
| 141 | "undo" -> Command | ||
| 142 | "unload" Identifier -> Command | ||
| 143 | |||
| 144 | |||
| 145 | imports Derivation | ||
| 146 | exports | ||
| 147 | sorts Combinator | ||
| 148 | context-free syntax | ||
| 149 | "nop" -> Combinator | ||
| 150 | "fail" -> Combinator | ||
| 151 | "seq" Combinator Combinator -> Combinator | ||
| 152 | "choice" Combinator Combinator -> Combinator | ||
| 153 | "lchoice" Combinator Combinator -> Combinator | ||
| 154 | "many" Combinator -> Combinator | ||
| 155 | "many1" Combinator -> Combinator | ||
| 156 | "try" Combinator -> Combinator | ||
| 157 | "once" Combinator -> Combinator | ||
| 158 | "everywhere" Combinator -> Combinator | ||
| 159 | "everywhere'" Combinator -> Combinator | ||
| 160 | "innermost" Combinator -> Combinator | ||
| 161 | "all" Combinator -> Combinator | ||
| 162 | "one" Combinator -> Combinator | ||
| 163 | Derivation -> Combinator | ||
| 164 | |||
| 165 | |||
| 166 | imports Identifier | ||
| 167 | exports | ||
| 168 | sorts Derivation | ||
| 169 | context-free syntax | ||
| 170 | "inv" Derivation -> Derivation | ||
| 171 | "shunt" Identifier -> Derivation | ||
| 172 | "distr_low" Identifier -> Derivation | ||
| 173 | "distr_up" Identifier -> Derivation | ||
| 174 | "monot_up" Identifier -> Derivation | ||
| 175 | "monot_low" Identifier -> Derivation | ||
| 176 | "top_preserving" Identifier -> Derivation | ||
| 177 | "bot_preserving" Identifier -> Derivation | ||
| 178 | "canc_up" Identifier -> Derivation | ||
| 179 | "canc_low" Identifier -> Derivation | ||
| 180 | "free" Identifier -> Derivation | ||
| 181 | "apply" Identifier -> Derivation | ||
| 182 | |||
| 183 | |||
| 184 | |||
| 185 | exports | ||
| 186 | sorts Identifier | ||
| 187 | |||
| 188 | |||
| 189 | [a-zA-Z\_][a-zA-Z0-9\_] -> Identifier | ||
| 190 | 10 | paulosilva | |
| 191 | |||
| 192 | exports | ||
| 193 | lexical syntax | ||
| 194 | [\ \t\n] -> LAYOUT | ||
| 195 | "--" ~[\n]* "\n" -> LAYOUT | ||
| 196 | "{-" ~"-}"+ "-}" -> LAYOUT | ||
| 197 |