1272343Sngie(*****************************************************************************) 2272343Sngie(* Create "ExtendedSyntaxTheory" representing abstract syntax of full PSL *) 3272343Sngie(*****************************************************************************) 4272343Sngie 5272343Sngie(*****************************************************************************) 6272343Sngie(* START BOILERPLATE *) 7272343Sngie(*****************************************************************************) 8272343Sngie 9272343Sngie(****************************************************************************** 10272343Sngie* Boilerplate needed for compilation 11272343Sngie******************************************************************************) 12272343Sngieopen HolKernel Parse boolLib bossLib; 13272343Sngie 14272343Sngie(****************************************************************************** 15272343Sngie* Open theories 16272343Sngie******************************************************************************) 17272343Sngieopen intLib stringLib stringTheory SyntaxTheory SyntacticSugarTheory; 18272343Sngie 19272343Sngie(****************************************************************************** 20272343Sngie* Set default parsing to natural numbers rather than integers 21272343Sngie******************************************************************************) 22272343Sngieval _ = intLib.deprecate_int(); 23272343Sngie 24272343Sngie(*****************************************************************************) 25272343Sngie(* END BOILERPLATE *) 26272343Sngie(*****************************************************************************) 27272343Sngie 28272343Sngie(****************************************************************************** 29272343Sngie* Start a new theory called ExtendedSyntaxTheory 30272343Sngie******************************************************************************) 31272343Sngieval _ = new_theory "ExtendedSyntax"; 32272343Sngie 33272343Sngie(****************************************************************************** 34272343Sngie* Extended boolean expressions 35272343Sngie******************************************************************************) 36272343Sngieval ebexp_def = 37272343Sngie time 38272343Sngie Hol_datatype 39272343Sngie `ebexp = 40272343Sngie EB_PROP of string (* atomic proposition *) 41272343Sngie | EB_NOT of ebexp (* negation *) 42272343Sngie | EB_AND of ebexp # ebexp (* conjunction *) 43272343Sngie(*========= Following are defined operators (i.e. syntactic sugar) =========*) 44272343Sngie | EB_OR of ebexp # ebexp (* disjunction *) 45272343Sngie | EB_IMP of ebexp # ebexp (* implication *) 46272343Sngie | EB_IFF of ebexp # ebexp (* logical equivalence *) 47272343Sngie | EB_TRUE (* T *) 48272343Sngie | EB_FALSE (* F *) 49272343Sngie `; 50272343Sngie 51272343Sngie(****************************************************************************** 52272343Sngie* Specification of an iteration number or range (Count of LRM A.3.6) 53272343Sngie******************************************************************************) 54272343Sngieval _ = type_abbrev("range", ``:num # num option``); 55272343Sngie 56272343Sngie(****************************************************************************** 57272343Sngie* Extended Sequential Extended Regular Expressions (SEREs) 58272343Sngie******************************************************************************) 59272343Sngieval esere_def = 60 time 61 Hol_datatype 62 `esere = 63 ES_BOOL of ebexp (* boolean expression *) 64 | ES_CAT of esere # esere (* r1 ; r2 *) 65 | ES_FUSION of esere # esere (* r1 : r2 *) 66 | ES_OR of esere # esere (* r1 | r2 *) 67 | ES_AND of esere # esere (* r1 && r2 *) 68 | ES_REPEAT of esere (* r[*] *) 69 | ES_CLOCK of esere # ebexp (* r@clk *) 70(*========= Following are defined operators (i.e. syntactic sugar) =========*) 71 | ES_FLEX_AND of esere # esere (* r1 & r2 *) 72 | ES_RANGE_REPEAT of esere # range (* r[* i] *) 73 | ES_NON_ZERO_REPEAT of esere (* r[+] *) 74 | ES_RANGE_EQ_REPEAT of ebexp # range (* b[= i] *) 75 | ES_RANGE_GOTO_REPEAT of ebexp # range (* b[-> i] *) 76 `; 77 78(****************************************************************************** 79* Extended Formulas 80* runtime: 589.300s, gctime: 151.590s, systime: 3.800s. (on bass) 81******************************************************************************) 82val efl_def = 83 time 84 Hol_datatype 85 `efl = 86 EF_BOOL of ebexp (* boolean expression *) 87 | EF_NOT of efl (* \neg f *) 88 | EF_AND of efl # efl (* f1 \wedge f2 *) 89 | EF_STRONG_X of efl (* X! f *) 90 | EF_U of efl # efl (* [f1 U f2] *) 91 | EF_SUFFIX_IMP of esere # efl (* {r}(f) *) 92 | EF_STRONG_IMP of esere # esere (* {r1} |-> {r2}! *) 93 | EF_WEAK_IMP of esere # esere (* {r1} |-> {r2} *) 94 | EF_ABORT of efl # ebexp (* f abort b *) 95 | EF_STRONG_CLOCK of efl # ebexp (* f@clk! *) 96(*========= Following are defined operators (i.e. syntactic sugar) =========*) 97 | EF_WEAK_CLOCK of efl # ebexp (* f@clk *) 98 | EF_OR of efl # efl (* f1 \vee f2 *) 99 | EF_IMP of efl # efl (* f1 \rightarrow f2 *) 100 | EF_IFF of efl # efl (* f1 \leftrightarrow f2 *) 101 | EF_WEAK_X of efl (* X f *) 102 | EF_F of efl (* F f *) 103 | EF_G of efl (* G f *) 104 | EF_W of efl # efl (* [f1 W f2] *) 105 | EF_ALWAYS of efl (* always f *) 106 | EF_NEVER of efl (* never f *) 107 | EF_WEAK_NEXT of efl (* next f *) 108 | EF_STRONG_NEXT of efl (* next! f *) 109 | EF_STRONG_EVENTUALLY of efl (* next! f *) 110 | EF_STRONG_UNTIL of efl # efl (* [f1 until! f2] *) 111 | EF_WEAK_UNTIL of efl # efl (* [f1 until f2] *) 112 | EF_STRONG_UNTIL_INC of efl # efl (* [f1 until!_ f2] *) 113 | EF_WEAK_UNTIL_INC of efl # efl (* [f1 until_ f2] *) 114 | EF_STRONG_BEFORE of efl # efl (* [f1 before! f2] *) 115 | EF_WEAK_BEFORE of efl # efl (* [f1 before f2] *) 116 | EF_STRONG_BEFORE_INC 117 of efl # efl (* [f1 before!_ f2] *) 118 | EF_WEAK_BEFORE_INC of efl # efl (* [f1 before_ f2] *) 119 | EF_NUM_WEAK_X of num # efl (* X[n](f) *) 120 | EF_NUM_STRONG_X of num # efl (* X *) 121 | EF_NUM_WEAK_NEXT of num # efl (* next[n](f) *) 122 | EF_NUM_STRONG_NEXT of num # efl (* next *) 123 | EF_NUM_WEAK_NEXT_A of range # efl (* next_a[n](f) *) 124 | EF_NUM_STRONG_NEXT_A of range # efl (* next_a *) 125 | EF_NUM_WEAK_NEXT_E of range # efl (* next_e[n](f) *) 126 | EF_NUM_STRONG_NEXT_E of range # efl (* next_e *) 127 | EF_STRONG_NEXT_EVENT of ebexp # efl (* next_event!(b)(f) *) 128 | EF_WEAK_NEXT_EVENT of ebexp # efl (* next_event(b)(f) *) 129 | EF_NUM_STRONG_NEXT_EVENT 130 of ebexp # num # efl (* next_event!(b)[i](f) *) 131 | EF_NUM_WEAK_NEXT_EVENT 132 of ebexp # num # efl (* next_event(b)[i](f) *) 133 | EF_NUM_STRONG_NEXT_EVENT_A 134 of ebexp # range # efl (* next_event_a!(b)[i](f) *) 135 | EF_NUM_WEAK_NEXT_EVENT_A 136 of ebexp # range # efl (* next_event_a(b)[i](f) *) 137 | EF_NUM_STRONG_NEXT_EVENT_E 138 of ebexp # range # efl (* next_event_e!(b)[i](f) *) 139 | EF_NUM_WEAK_NEXT_EVENT_E 140 of ebexp # range # efl (* next_event_e(b)[i](f) *) 141 | EF_SKIP_STRONG_IMP of esere # esere (* {r1} |=> {r2}! *) 142 | EF_SKIP_WEAK_IMP of esere # esere (* {r1} |=> {r2} *) 143 | EF_SERE_ALWAYS of esere (* always r *) 144 | EF_SERE_NEVER of esere (* never r *) 145 | EF_SERE_STRONG_EVENTUALLY 146 of esere (* eventually! r *) 147 | EF_STRONG_WITHIN of esere # ebexp # esere (* within!(r1,b)r2 *) 148 | EF_WEAK_WITHIN of esere # ebexp # esere (* within(r1,b)r2 *) 149 | EF_STRONG_WITHIN_INC of esere # ebexp # esere (* within!_(r1,b)r2 *) 150 | EF_WEAK_WITHIN_INC of esere # ebexp # esere (* within_(r1,b)r2 *) 151 | EF_STRONG_WHILENOT of ebexp # esere (* whilenot!(b)r *) 152 | EF_WEAK_WHILENOT of ebexp # esere (* whilenot(b)r *) 153 | EF_STRONG_WHILENOT_INC 154 of ebexp # esere (* whilenot!_(b)r *) 155 | EF_WEAK_WHILENOT_INC of ebexp # esere (* whilenot_(b)r *) 156 `; 157 158 159(****************************************************************************** 160* Translate booleans from extended syntax into core syntax 161******************************************************************************) 162val B_DESUGAR_def = 163 Define 164 `(B_DESUGAR(EB_PROP p) = B_PROP p) /\ 165 (B_DESUGAR(EB_NOT b) = B_NOT(B_DESUGAR b)) /\ 166 (B_DESUGAR(EB_AND(b1,b2)) = B_AND(B_DESUGAR b1, B_DESUGAR b2)) /\ 167 (B_DESUGAR(EB_OR(b1,b2)) = B_OR(B_DESUGAR b1, B_DESUGAR b2)) /\ 168 (B_DESUGAR(EB_IMP(b1,b2)) = B_IMP(B_DESUGAR b1, B_DESUGAR b2)) /\ 169 (B_DESUGAR(EB_IFF(b1,b2)) = B_IFF(B_DESUGAR b1, B_DESUGAR b2)) /\ 170 (B_DESUGAR EB_TRUE = B_TRUE) /\ 171 (B_DESUGAR EB_FALSE = B_FALSE)`; 172 173 174(****************************************************************************** 175* Translate extended SEREs into core syntax 176******************************************************************************) 177val S_DESUGAR_def = 178 Define 179 `(S_DESUGAR(ES_BOOL b) = 180 S_BOOL(B_DESUGAR b)) 181 /\ 182 (S_DESUGAR(ES_CAT(r1,r2)) = 183 S_CAT(S_DESUGAR r1, S_DESUGAR r2)) 184 /\ 185 (S_DESUGAR(ES_FUSION(r1,r2)) = 186 S_FUSION(S_DESUGAR r1, S_DESUGAR r2)) 187 /\ 188 (S_DESUGAR(ES_OR(r1,r2)) = 189 S_OR(S_DESUGAR r1, S_DESUGAR r2)) 190 /\ 191 (S_DESUGAR(ES_AND(r1,r2)) = 192 S_AND(S_DESUGAR r1, S_DESUGAR r2)) 193 /\ 194 (S_DESUGAR(ES_REPEAT r) = 195 S_REPEAT(S_DESUGAR r)) 196 /\ 197 (S_DESUGAR(ES_CLOCK(r,b)) = 198 S_CLOCK(S_DESUGAR r, B_DESUGAR b)) 199 /\ 200 (S_DESUGAR(ES_FLEX_AND(r1,r2)) = 201 S_FLEX_AND(S_DESUGAR r1, S_DESUGAR r2)) 202 /\ 203 (S_DESUGAR(ES_RANGE_REPEAT(r,rng)) = 204 S_RANGE_REPEAT(S_DESUGAR r, rng)) 205 /\ 206 (S_DESUGAR(ES_NON_ZERO_REPEAT r) = 207 S_NON_ZERO_REPEAT(S_DESUGAR r)) 208 /\ 209 (S_DESUGAR(ES_RANGE_EQ_REPEAT(b, rng)) = 210 S_RANGE_EQ_REPEAT(B_DESUGAR b, rng)) 211 /\ 212 (S_DESUGAR(ES_RANGE_GOTO_REPEAT(b,rng)) = 213 S_RANGE_GOTO_REPEAT(B_DESUGAR b, rng))`; 214 215(****************************************************************************** 216* Definitions connecting syntax-oriented names with semantic constants 217******************************************************************************) 218val F_STRONG_X_def = Define `F_STRONG_X = F_NEXT`; 219 220val F_U_def = Define `F_U = F_UNTIL`; 221 222val F_IMP_def = Define `F_IMP = F_IMPLIES`; 223 224(****************************************************************************** 225* Translate extended formulas into core syntax 226******************************************************************************) 227val F_DESUGAR_def = 228 Define 229 `(F_DESUGAR(EF_BOOL b) = 230 F_BOOL(B_DESUGAR b)) 231 /\ 232 (F_DESUGAR(EF_NOT f) = 233 F_NOT(F_DESUGAR f)) 234 /\ 235 (F_DESUGAR(EF_AND(f1,f2)) = 236 F_AND(F_DESUGAR f1, F_DESUGAR f2)) 237 /\ 238 (F_DESUGAR(EF_STRONG_X f) = 239 F_STRONG_X(F_DESUGAR f)) 240 /\ 241 (F_DESUGAR(EF_U(f1,f2)) = 242 F_U(F_DESUGAR f1, F_DESUGAR f2)) 243 /\ 244 (F_DESUGAR(EF_SUFFIX_IMP(r,f)) = 245 F_SUFFIX_IMP(S_DESUGAR r, F_DESUGAR f)) 246 /\ 247 (F_DESUGAR(EF_STRONG_IMP(r1,r2)) = 248 F_STRONG_IMP(S_DESUGAR r1, S_DESUGAR r2)) 249 /\ 250 (F_DESUGAR(EF_WEAK_IMP(r1,r2)) = 251 F_WEAK_IMP(S_DESUGAR r1, S_DESUGAR r2)) 252 /\ 253 (F_DESUGAR(EF_ABORT(f,b)) = 254 F_ABORT(F_DESUGAR f, B_DESUGAR b)) 255 /\ 256 (F_DESUGAR(EF_STRONG_CLOCK(f,b)) = 257 F_STRONG_CLOCK(F_DESUGAR f, B_DESUGAR b)) 258 /\ 259 (F_DESUGAR(EF_WEAK_CLOCK(f,b)) = 260 F_WEAK_CLOCK(F_DESUGAR f, B_DESUGAR b)) 261 /\ 262 (F_DESUGAR(EF_OR(f1,f2)) = 263 F_OR(F_DESUGAR f1, F_DESUGAR f2)) 264 /\ 265 (F_DESUGAR(EF_IMP(f1,f2)) = 266 F_IMP(F_DESUGAR f1, F_DESUGAR f2)) 267 /\ 268 (F_DESUGAR(EF_IFF(f1,f2)) = 269 F_IFF(F_DESUGAR f1, F_DESUGAR f2)) 270 /\ 271 (F_DESUGAR(EF_WEAK_X f) = 272 F_WEAK_X(F_DESUGAR f)) 273 /\ 274 (F_DESUGAR(EF_F f) = 275 F_F(F_DESUGAR f)) 276 /\ 277 (F_DESUGAR(EF_G f) = 278 F_G(F_DESUGAR f)) 279 /\ 280 (F_DESUGAR(EF_W(f1,f2)) = 281 F_W(F_DESUGAR f1, F_DESUGAR f2)) 282 /\ 283 (F_DESUGAR(EF_ALWAYS f) = 284 F_ALWAYS(F_DESUGAR f)) 285 /\ 286 (F_DESUGAR(EF_NEVER f) = 287 F_NEVER(F_DESUGAR f)) 288 /\ 289 (F_DESUGAR(EF_WEAK_NEXT f) = 290 F_WEAK_NEXT(F_DESUGAR f)) 291 /\ 292 (F_DESUGAR(EF_STRONG_NEXT f) = 293 F_STRONG_NEXT(F_DESUGAR f)) 294 /\ 295 (F_DESUGAR(EF_STRONG_EVENTUALLY f) = 296 F_STRONG_EVENTUALLY(F_DESUGAR f)) 297 /\ 298 (F_DESUGAR(EF_STRONG_UNTIL(f1,f2)) = 299 F_STRONG_UNTIL(F_DESUGAR f1, F_DESUGAR f2)) 300 /\ 301 (F_DESUGAR(EF_WEAK_UNTIL(f1,f2)) = 302 F_WEAK_UNTIL(F_DESUGAR f1, F_DESUGAR f2)) 303 /\ 304 (F_DESUGAR(EF_STRONG_UNTIL_INC(f1,f2)) = 305 F_STRONG_UNTIL_INC(F_DESUGAR f1, F_DESUGAR f2)) 306 /\ 307 (F_DESUGAR(EF_WEAK_UNTIL_INC(f1,f2)) = 308 F_WEAK_UNTIL_INC(F_DESUGAR f1, F_DESUGAR f2)) 309 /\ 310 (F_DESUGAR(EF_STRONG_BEFORE(f1,f2)) = 311 F_STRONG_BEFORE(F_DESUGAR f1, F_DESUGAR f2)) 312 /\ 313 (F_DESUGAR(EF_WEAK_BEFORE(f1,f2)) = 314 F_WEAK_BEFORE(F_DESUGAR f1, F_DESUGAR f2)) 315 /\ 316 (F_DESUGAR(EF_STRONG_BEFORE_INC(f1,f2)) = 317 F_STRONG_BEFORE_INC(F_DESUGAR f1, F_DESUGAR f2)) 318 /\ 319 (F_DESUGAR(EF_WEAK_BEFORE_INC(f1,f2)) = 320 F_WEAK_BEFORE_INC(F_DESUGAR f1, F_DESUGAR f2)) 321 /\ 322 (F_DESUGAR(EF_NUM_WEAK_X(n,f)) = 323 F_NUM_WEAK_X(n, F_DESUGAR f)) 324 /\ 325 (F_DESUGAR(EF_NUM_STRONG_X(n,f)) = 326 F_NUM_STRONG_X(n, F_DESUGAR f)) 327 /\ 328 (F_DESUGAR(EF_NUM_WEAK_NEXT(n,f)) = 329 F_NUM_WEAK_NEXT(n, F_DESUGAR f)) 330 /\ 331 (F_DESUGAR(EF_NUM_STRONG_NEXT(n,f)) = 332 F_NUM_STRONG_NEXT(n, F_DESUGAR f)) 333 /\ 334 (F_DESUGAR(EF_NUM_WEAK_NEXT_A(rng,f)) = 335 F_NUM_WEAK_NEXT_A(rng, F_DESUGAR f)) 336 /\ 337 (F_DESUGAR(EF_NUM_STRONG_NEXT_A(rng,f)) = 338 F_NUM_STRONG_NEXT_A(rng, F_DESUGAR f)) 339 /\ 340 (F_DESUGAR(EF_NUM_WEAK_NEXT_E(rng,f)) = 341 F_NUM_WEAK_NEXT_E(rng, F_DESUGAR f)) 342 /\ 343 (F_DESUGAR(EF_NUM_STRONG_NEXT_E(rng,f)) = 344 F_NUM_STRONG_NEXT_E(rng, F_DESUGAR f)) 345 /\ 346 (F_DESUGAR(EF_STRONG_NEXT_EVENT(b,f)) = 347 F_STRONG_NEXT_EVENT(B_DESUGAR b, F_DESUGAR f)) 348 /\ 349 (F_DESUGAR(EF_WEAK_NEXT_EVENT(b,f)) = 350 F_WEAK_NEXT_EVENT(B_DESUGAR b, F_DESUGAR f)) 351 /\ 352 (F_DESUGAR(EF_NUM_STRONG_NEXT_EVENT(b,n,f)) = 353 F_NUM_STRONG_NEXT_EVENT(B_DESUGAR b, n, F_DESUGAR f)) 354 /\ 355 (F_DESUGAR(EF_NUM_WEAK_NEXT_EVENT(b,n,f)) = 356 F_NUM_WEAK_NEXT_EVENT(B_DESUGAR b, n, F_DESUGAR f)) 357 /\ 358 (F_DESUGAR(EF_NUM_STRONG_NEXT_EVENT_A(b,rng,f)) = 359 F_NUM_STRONG_NEXT_EVENT_A(B_DESUGAR b, rng, F_DESUGAR f)) 360 /\ 361 (F_DESUGAR(EF_NUM_WEAK_NEXT_EVENT_A(b,rng,f)) = 362 F_NUM_WEAK_NEXT_EVENT_A(B_DESUGAR b, rng, F_DESUGAR f)) 363 /\ 364 (F_DESUGAR(EF_NUM_STRONG_NEXT_EVENT_E(b,rng,f)) = 365 F_NUM_STRONG_NEXT_EVENT_E(B_DESUGAR b, rng, F_DESUGAR f)) 366 /\ 367 (F_DESUGAR(EF_NUM_WEAK_NEXT_EVENT_E(b,rng,f)) = 368 F_NUM_WEAK_NEXT_EVENT_E(B_DESUGAR b, rng, F_DESUGAR f)) 369 /\ 370 (F_DESUGAR(EF_SKIP_STRONG_IMP(r1,r2)) = 371 F_SKIP_STRONG_IMP(S_DESUGAR r1, S_DESUGAR r2)) 372 /\ 373 (F_DESUGAR(EF_SKIP_WEAK_IMP(r1,r2)) = 374 F_SKIP_WEAK_IMP(S_DESUGAR r1, S_DESUGAR r2)) 375 /\ 376 (F_DESUGAR(EF_SERE_ALWAYS r) = 377 F_SERE_ALWAYS(S_DESUGAR r)) 378 /\ 379 (F_DESUGAR(EF_SERE_NEVER r) = 380 F_SERE_NEVER(S_DESUGAR r)) 381 /\ 382 (F_DESUGAR(EF_SERE_STRONG_EVENTUALLY r) = 383 F_SERE_STRONG_EVENTUALLY(S_DESUGAR r)) 384 /\ 385 (F_DESUGAR(EF_STRONG_WITHIN(r1,b,r2)) = 386 F_STRONG_WITHIN(S_DESUGAR r1, B_DESUGAR b, S_DESUGAR r2)) 387 /\ 388 (F_DESUGAR(EF_WEAK_WITHIN(r1,b,r2)) = 389 F_WEAK_WITHIN(S_DESUGAR r1, B_DESUGAR b, S_DESUGAR r2)) 390 /\ 391 (F_DESUGAR(EF_STRONG_WITHIN_INC(r1,b,r2)) = 392 F_STRONG_WITHIN_INC(S_DESUGAR r1, B_DESUGAR b, S_DESUGAR r2)) 393 /\ 394 (F_DESUGAR(EF_WEAK_WITHIN_INC(r1,b,r2)) = 395 F_WEAK_WITHIN_INC(S_DESUGAR r1, B_DESUGAR b, S_DESUGAR r2)) 396 /\ 397 (F_DESUGAR(EF_STRONG_WHILENOT(b,r)) = 398 F_STRONG_WHILENOT(B_DESUGAR b, S_DESUGAR r)) 399 /\ 400 (F_DESUGAR(EF_WEAK_WHILENOT(b,r)) = 401 F_WEAK_WHILENOT(B_DESUGAR b, S_DESUGAR r)) 402 /\ 403 (F_DESUGAR(EF_STRONG_WHILENOT_INC(b,r)) = 404 F_STRONG_WHILENOT_INC(B_DESUGAR b, S_DESUGAR r)) 405 /\ 406 (F_DESUGAR(EF_WEAK_WHILENOT_INC(b,r)) = 407 F_WEAK_WHILENOT_INC(B_DESUGAR b, S_DESUGAR r))`; 408 409val _ = export_theory(); 410