1(*****************************************************************************) 2(* Create "ExtendedSyntaxTheory" representing abstract syntax of full PSL *) 3(*****************************************************************************) 4 5(*****************************************************************************) 6(* START BOILERPLATE *) 7(*****************************************************************************) 8 9(****************************************************************************** 10* Load theory of syntax, paths and models 11* (commented out for compilation) 12******************************************************************************) 13(* 14quietdec := true; 15map load 16 ["intLib","stringLib","SyntaxTheory","SyntacticSugarTheory"]; 17open intLib stringLib stringTheory SyntaxTheory SyntacticSugarTheory; 18val _ = intLib.deprecate_int(); 19quietdec := false; 20*) 21 22(****************************************************************************** 23* Boilerplate needed for compilation 24******************************************************************************) 25open HolKernel Parse boolLib bossLib; 26 27(****************************************************************************** 28* Open theories 29******************************************************************************) 30open intLib stringLib stringTheory SyntaxTheory SyntacticSugarTheory; 31 32(****************************************************************************** 33* Set default parsing to natural numbers rather than integers 34******************************************************************************) 35val _ = intLib.deprecate_int(); 36 37(*****************************************************************************) 38(* END BOILERPLATE *) 39(*****************************************************************************) 40 41(****************************************************************************** 42* Start a new theory called ExtendedSyntaxTheory 43******************************************************************************) 44val _ = new_theory "ExtendedSyntax"; 45 46(****************************************************************************** 47* Extended boolean expressions 48******************************************************************************) 49val ebexp_def = 50 time 51 Hol_datatype 52 `ebexp = 53 EB_PROP of string (* atomic proposition *) 54 | EB_TRUE (* T *) 55 | EB_FALSE (* F *) 56 | EB_NOT of ebexp (* negation *) 57 | EB_AND of ebexp # ebexp (* conjunction *) 58(*========= Following are defined operators (i.e. syntactic sugar) =========*) 59 | EB_OR of ebexp # ebexp (* disjunction *) 60 | EB_IMP of ebexp # ebexp (* implication *) 61 | EB_IFF of ebexp # ebexp (* logical equivalence *) 62 `; 63 64(****************************************************************************** 65* Specification of an iteration number or range (Count of LRM A.3.6) 66******************************************************************************) 67val _ = type_abbrev("range", ``:num # num option``); 68 69(****************************************************************************** 70* Extended Sequential Extended Regular Expressions (SEREs) 71******************************************************************************) 72val esere_def = 73 time 74 Hol_datatype 75 `esere = 76 ES_BOOL of ebexp (* boolean expression *) 77 | ES_CAT of esere # esere (* r1 ; r2 *) 78 | ES_FUSION of esere # esere (* r1 : r2 *) 79 | ES_OR of esere # esere (* r1 | r2 *) 80 | ES_AND of esere # esere (* r1 && r2 *) 81 | ES_EMPTY (* [*0] *) 82 | ES_REPEAT of esere (* r[*] *) 83 | ES_CLOCK of esere # ebexp (* r@clk *) 84(*========= Following are defined operators (i.e. syntactic sugar) =========*) 85 | ES_FLEX_AND of esere # esere (* r1 & r2 *) 86 | ES_RANGE_REPEAT of esere # count (* r[*i] *) 87 | ES_NON_ZERO_REPEAT of esere (* r[+] *) 88 | ES_RANGE_EQ_REPEAT of ebexp # count (* b[= i] *) 89 | ES_RANGE_GOTO_REPEAT of ebexp # count (* b[-> i] *) 90 `; 91 92(****************************************************************************** 93* Extended Formulas 94* runtime: 589.300s, gctime: 151.590s, systime: 3.800s. (on bass) 95******************************************************************************) 96val efl_def = 97 time 98 Hol_datatype 99 `efl = 100 EF_STRONG_BOOL of ebexp (* strong boolean *) 101 | EF_WEAK_BOOL of ebexp (* weak boolean *) 102 | EF_NOT of efl (* \neg f *) 103 | EF_AND of efl # efl (* f1 \wedge f2 *) 104 | EF_STRONG_SERE of esere (* {r}! *) 105 | EF_WEAK_SERE of esere (* {r} *) 106 | EF_STRONG_X of efl (* X! f *) 107 | EF_U of efl # efl (* [f1 U f2] *) 108 | EF_ABORT of efl # ebexp (* f abort b *) 109 | EF_CLOCK of efl # ebexp (* f@clk *) 110 | EF_SUFFIX_IMP of esere # efl (* {r} |-> f *) 111(*========= Following are defined operators (i.e. syntactic sugar) =========*) 112 | EF_OR of efl # efl (* f1 \vee f2 *) 113 | EF_IMP of efl # efl (* f1 \rightarrow f2 *) 114 | EF_IFF of efl # efl (* f1 \leftrightarrow f2 *) 115 | EF_F of efl (* F f *) 116 | EF_G of efl (* G f *) 117 | EF_WEAK_X of efl (* X f *) 118 | EF_W of efl # efl (* [f1 W f2] *) 119 | EF_ALWAYS of efl (* always f *) 120 | EF_NEVER of efl (* never f *) 121 | EF_STRONG_NEXT of efl (* next! f *) 122 | EF_WEAK_NEXT of efl (* next f *) 123 | EF_STRONG_EVENTUALLY of efl (* next! f *) 124 | EF_STRONG_UNTIL of efl # efl (* [f1 until! f2] *) 125 | EF_WEAK_UNTIL of efl # efl (* [f1 until f2] *) 126 | EF_STRONG_UNTIL_INC of efl # efl (* [f1 until!_ f2] *) 127 | EF_WEAK_UNTIL_INC of efl # efl (* [f1 until_ f2] *) 128 | EF_STRONG_BEFORE of efl # efl (* [f1 before! f2] *) 129 | EF_WEAK_BEFORE of efl # efl (* [f1 before f2] *) 130 | EF_STRONG_BEFORE_INC 131 of efl # efl (* [f1 before!_ f2] *) 132 | EF_WEAK_BEFORE_INC of efl # efl (* [f1 before_ f2] *) 133 | EF_NUM_STRONG_X of num # efl (* X *) 134 | EF_NUM_WEAK_X of num # efl (* X[n](f) *) 135 | EF_NUM_STRONG_NEXT of num # efl (* next *) 136 | EF_NUM_WEAK_NEXT of num # efl (* next[n](f) *) 137 | EF_NUM_STRONG_NEXT_A of range # efl (* next_a *) 138 | EF_NUM_WEAK_NEXT_A of range # efl (* next_a[n](f) *) 139 | EF_NUM_STRONG_NEXT_E of range # efl (* next_e *) 140 | EF_NUM_WEAK_NEXT_E of range # efl (* next_e[n](f) *) 141 | EF_STRONG_NEXT_EVENT of ebexp # efl (* next_event!(b)(f) *) 142 | EF_WEAK_NEXT_EVENT of ebexp # efl (* next_event(b)(f) *) 143 | EF_NUM_STRONG_NEXT_EVENT 144 of ebexp # num # efl (* next_event!(b)[i](f) *) 145 | EF_NUM_WEAK_NEXT_EVENT 146 of ebexp # num # efl (* next_event(b)[i](f) *) 147 | EF_NUM_STRONG_NEXT_EVENT_A 148 of ebexp # range # efl (* next_event_a!(b)[i](f) *) 149 | EF_NUM_WEAK_NEXT_EVENT_A 150 of ebexp # range # efl (* next_event_a(b)[i](f) *) 151 | EF_NUM_STRONG_NEXT_EVENT_E 152 of ebexp # range # efl (* next_event_e!(b)[i](f) *) 153 | EF_NUM_WEAK_NEXT_EVENT_E 154 of ebexp # range # efl (* next_event_e(b)[i](f) *) 155 | EF_SKIP_SUFFIX_IMP of esere # efl (* {r} |=> f *) 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_TRUE = B_TRUE) /\ 166 (B_DESUGAR EB_FALSE = B_FALSE) /\ 167 (B_DESUGAR(EB_NOT b) = B_NOT(B_DESUGAR b)) /\ 168 (B_DESUGAR(EB_AND(b1,b2)) = B_AND(B_DESUGAR b1, B_DESUGAR b2)) /\ 169 (B_DESUGAR(EB_OR(b1,b2)) = B_OR(B_DESUGAR b1, B_DESUGAR b2)) /\ 170 (B_DESUGAR(EB_IMP(b1,b2)) = B_IMP(B_DESUGAR b1, B_DESUGAR b2)) /\ 171 (B_DESUGAR(EB_IFF(b1,b2)) = B_IFF(B_DESUGAR b1, B_DESUGAR b2))`; 172 173(****************************************************************************** 174* Translate extended SEREs into core syntax 175******************************************************************************) 176val S_DESUGAR_def = 177 Define 178 `(S_DESUGAR(ES_BOOL b) = 179 S_BOOL(B_DESUGAR b)) 180 /\ 181 (S_DESUGAR(ES_CAT(r1,r2)) = 182 S_CAT(S_DESUGAR r1, S_DESUGAR r2)) 183 /\ 184 (S_DESUGAR(ES_FUSION(r1,r2)) = 185 S_FUSION(S_DESUGAR r1, S_DESUGAR r2)) 186 /\ 187 (S_DESUGAR(ES_OR(r1,r2)) = 188 S_OR(S_DESUGAR r1, S_DESUGAR r2)) 189 /\ 190 (S_DESUGAR(ES_AND(r1,r2)) = 191 S_AND(S_DESUGAR r1, S_DESUGAR r2)) 192 /\ 193 (S_DESUGAR ES_EMPTY = 194 S_EMPTY) 195 /\ 196 (S_DESUGAR(ES_REPEAT r) = 197 S_REPEAT(S_DESUGAR r)) 198 /\ 199 (S_DESUGAR(ES_CLOCK(r,b)) = 200 S_CLOCK(S_DESUGAR r, B_DESUGAR b)) 201 /\ 202 (S_DESUGAR(ES_FLEX_AND(r1,r2)) = 203 S_FLEX_AND(S_DESUGAR r1, S_DESUGAR r2)) 204 /\ 205 (S_DESUGAR(ES_RANGE_REPEAT(r,cnt)) = 206 S_RANGE_REPEAT(S_DESUGAR r, cnt)) 207 /\ 208 (S_DESUGAR(ES_NON_ZERO_REPEAT r) = 209 S_NON_ZERO_REPEAT(S_DESUGAR r)) 210 /\ 211 (S_DESUGAR(ES_RANGE_EQ_REPEAT(b, cnt)) = 212 S_RANGE_EQ_REPEAT(B_DESUGAR b, cnt)) 213 /\ 214 (S_DESUGAR(ES_RANGE_GOTO_REPEAT(b,cnt)) = 215 S_RANGE_GOTO_REPEAT(B_DESUGAR b, cnt))`; 216 217(****************************************************************************** 218* Definitions connecting syntax-oriented names with semantic constants 219******************************************************************************) 220val F_STRONG_X_def = Define `F_STRONG_X = F_NEXT`; 221 222val F_U_def = Define `F_U = F_UNTIL`; 223 224val F_IMP_def = Define `F_IMP = F_IMPLIES`; 225 226(****************************************************************************** 227* Translate extended formulas into core syntax 228******************************************************************************) 229val F_DESUGAR_def = 230 Define 231 `(F_DESUGAR(EF_STRONG_BOOL b) = 232 F_STRONG_BOOL(B_DESUGAR b)) 233 /\ 234 (F_DESUGAR(EF_WEAK_BOOL b) = 235 F_WEAK_BOOL(B_DESUGAR b)) 236 /\ 237 (F_DESUGAR(EF_NOT f) = 238 F_NOT(F_DESUGAR f)) 239 /\ 240 (F_DESUGAR(EF_AND(f1,f2)) = 241 F_AND(F_DESUGAR f1, F_DESUGAR f2)) 242 /\ 243 (F_DESUGAR(EF_STRONG_SERE r) = 244 F_STRONG_SERE(S_DESUGAR r)) 245 /\ 246 (F_DESUGAR(EF_WEAK_SERE r) = 247 F_WEAK_SERE(S_DESUGAR r)) 248 /\ 249 (F_DESUGAR(EF_STRONG_X f) = 250 F_STRONG_X(F_DESUGAR f)) 251 /\ 252 (F_DESUGAR(EF_U(f1,f2)) = 253 F_U(F_DESUGAR f1, F_DESUGAR f2)) 254 /\ 255 (F_DESUGAR(EF_ABORT(f,b)) = 256 F_ABORT(F_DESUGAR f, B_DESUGAR b)) 257 /\ 258 (F_DESUGAR(EF_CLOCK(f,b)) = 259 F_CLOCK(F_DESUGAR f, B_DESUGAR b)) 260 /\ 261 (F_DESUGAR(EF_SUFFIX_IMP(r,f)) = 262 F_SUFFIX_IMP(S_DESUGAR r, F_DESUGAR f)) 263 /\ 264 (F_DESUGAR(EF_OR(f1,f2)) = 265 F_OR(F_DESUGAR f1, F_DESUGAR f2)) 266 /\ 267 (F_DESUGAR(EF_IMP(f1,f2)) = 268 F_IMP(F_DESUGAR f1, F_DESUGAR f2)) 269 /\ 270 (F_DESUGAR(EF_IFF(f1,f2)) = 271 F_IFF(F_DESUGAR f1, F_DESUGAR f2)) 272 /\ 273 (F_DESUGAR(EF_F f) = 274 F_F(F_DESUGAR f)) 275 /\ 276 (F_DESUGAR(EF_G f) = 277 F_G(F_DESUGAR f)) 278 /\ 279 (F_DESUGAR(EF_WEAK_X f) = 280 F_WEAK_X(F_DESUGAR f)) 281 /\ 282 (F_DESUGAR(EF_W(f1,f2)) = 283 F_W(F_DESUGAR f1, F_DESUGAR f2)) 284 /\ 285 (F_DESUGAR(EF_ALWAYS f) = 286 F_ALWAYS(F_DESUGAR f)) 287 /\ 288 (F_DESUGAR(EF_NEVER f) = 289 F_NEVER(F_DESUGAR f)) 290 /\ 291 (F_DESUGAR(EF_STRONG_NEXT f) = 292 F_STRONG_NEXT(F_DESUGAR f)) 293 /\ 294 (F_DESUGAR(EF_WEAK_NEXT f) = 295 F_WEAK_NEXT(F_DESUGAR f)) 296 /\ 297 (F_DESUGAR(EF_STRONG_EVENTUALLY f) = 298 F_STRONG_EVENTUALLY(F_DESUGAR f)) 299 /\ 300 (F_DESUGAR(EF_STRONG_UNTIL(f1,f2)) = 301 F_STRONG_UNTIL(F_DESUGAR f1, F_DESUGAR f2)) 302 /\ 303 (F_DESUGAR(EF_WEAK_UNTIL(f1,f2)) = 304 F_WEAK_UNTIL(F_DESUGAR f1, F_DESUGAR f2)) 305 /\ 306 (F_DESUGAR(EF_STRONG_UNTIL_INC(f1,f2)) = 307 F_STRONG_UNTIL_INC(F_DESUGAR f1, F_DESUGAR f2)) 308 /\ 309 (F_DESUGAR(EF_WEAK_UNTIL_INC(f1,f2)) = 310 F_WEAK_UNTIL_INC(F_DESUGAR f1, F_DESUGAR f2)) 311 /\ 312 (F_DESUGAR(EF_STRONG_BEFORE(f1,f2)) = 313 F_STRONG_BEFORE(F_DESUGAR f1, F_DESUGAR f2)) 314 /\ 315 (F_DESUGAR(EF_WEAK_BEFORE(f1,f2)) = 316 F_WEAK_BEFORE(F_DESUGAR f1, F_DESUGAR f2)) 317 /\ 318 (F_DESUGAR(EF_STRONG_BEFORE_INC(f1,f2)) = 319 F_STRONG_BEFORE_INC(F_DESUGAR f1, F_DESUGAR f2)) 320 /\ 321 (F_DESUGAR(EF_WEAK_BEFORE_INC(f1,f2)) = 322 F_WEAK_BEFORE_INC(F_DESUGAR f1, F_DESUGAR f2)) 323 /\ 324 (F_DESUGAR(EF_NUM_STRONG_X(n,f)) = 325 F_NUM_STRONG_X(n, F_DESUGAR f)) 326 /\ 327 (F_DESUGAR(EF_NUM_WEAK_X(n,f)) = 328 F_NUM_WEAK_X(n, F_DESUGAR f)) 329 /\ 330 (F_DESUGAR(EF_NUM_STRONG_NEXT(n,f)) = 331 F_NUM_STRONG_NEXT(n, F_DESUGAR f)) 332 /\ 333 (F_DESUGAR(EF_NUM_WEAK_NEXT(n,f)) = 334 F_NUM_WEAK_NEXT(n, F_DESUGAR f)) 335 /\ 336 (F_DESUGAR(EF_NUM_STRONG_NEXT_A(rng,f)) = 337 F_NUM_STRONG_NEXT_A(rng, F_DESUGAR f)) 338 /\ 339 (F_DESUGAR(EF_NUM_WEAK_NEXT_A(rng,f)) = 340 F_NUM_WEAK_NEXT_A(rng, F_DESUGAR f)) 341 /\ 342 (F_DESUGAR(EF_NUM_STRONG_NEXT_E(rng,f)) = 343 F_NUM_STRONG_NEXT_E(rng, F_DESUGAR f)) 344 /\ 345 (F_DESUGAR(EF_NUM_WEAK_NEXT_E(rng,f)) = 346 F_NUM_WEAK_NEXT_E(rng, F_DESUGAR f)) 347 /\ 348 (F_DESUGAR(EF_STRONG_NEXT_EVENT(b,f)) = 349 F_STRONG_NEXT_EVENT(B_DESUGAR b, F_DESUGAR f)) 350 /\ 351 (F_DESUGAR(EF_WEAK_NEXT_EVENT(b,f)) = 352 F_WEAK_NEXT_EVENT(B_DESUGAR b, F_DESUGAR f)) 353 /\ 354 (F_DESUGAR(EF_NUM_STRONG_NEXT_EVENT(b,n,f)) = 355 F_NUM_STRONG_NEXT_EVENT(B_DESUGAR b, n, F_DESUGAR f)) 356 /\ 357 (F_DESUGAR(EF_NUM_WEAK_NEXT_EVENT(b,n,f)) = 358 F_NUM_WEAK_NEXT_EVENT(B_DESUGAR b, n, F_DESUGAR f)) 359 /\ 360 (F_DESUGAR(EF_NUM_STRONG_NEXT_EVENT_A(b,rng,f)) = 361 F_NUM_STRONG_NEXT_EVENT_A(B_DESUGAR b, rng, F_DESUGAR f)) 362 /\ 363 (F_DESUGAR(EF_NUM_WEAK_NEXT_EVENT_A(b,rng,f)) = 364 F_NUM_WEAK_NEXT_EVENT_A(B_DESUGAR b, rng, F_DESUGAR f)) 365 /\ 366 (F_DESUGAR(EF_NUM_STRONG_NEXT_EVENT_E(b,rng,f)) = 367 F_NUM_STRONG_NEXT_EVENT_E(B_DESUGAR b, rng, F_DESUGAR f)) 368 /\ 369 (F_DESUGAR(EF_NUM_WEAK_NEXT_EVENT_E(b,rng,f)) = 370 F_NUM_WEAK_NEXT_EVENT_E(B_DESUGAR b, rng, F_DESUGAR f)) 371 /\ 372 (F_DESUGAR(EF_SKIP_SUFFIX_IMP(r,f)) = 373 F_SKIP_SUFFIX_IMP(S_DESUGAR r, F_DESUGAR f))`; 374 375 376val _ = export_theory(); 377