1(*****************************************************************************) 2(* Create "SyntaxTheory" representing abstract syntax of PSL Version 1.1 *) 3(*****************************************************************************) 4 5(*****************************************************************************) 6(* START BOILERPLATE *) 7(*****************************************************************************) 8 9(****************************************************************************** 10* Boilerplate needed for compilation 11******************************************************************************) 12open HolKernel Parse boolLib bossLib; 13 14(*****************************************************************************) 15(* END BOILERPLATE *) 16(*****************************************************************************) 17 18(****************************************************************************** 19* Start a new theory called SyntaxTheory 20******************************************************************************) 21val _ = new_theory "Syntax"; 22 23(****************************************************************************** 24* Boolean expressions 25******************************************************************************) 26val bexp_def = 27 Hol_datatype 28 `bexp = B_PROP of 'a (* atomic proposition *) 29 | B_TRUE (* true *) 30 | B_FALSE (* false *) 31 | B_NOT of bexp (* negation *) 32 | B_AND of bexp # bexp`; (* conjunction *) 33 34(****************************************************************************** 35* Sequential Extended Regular Expressions (SEREs) 36******************************************************************************) 37val sere_def = 38 Hol_datatype 39 `sere = S_BOOL of 'a bexp (* boolean expression *) 40 | S_CAT of sere # sere (* r1 ; r2 *) 41 | S_FUSION of sere # sere (* r1 : r2 *) 42 | S_OR of sere # sere (* r1 | r2 *) 43 | S_AND of sere # sere (* r1 && r2 *) 44 | S_EMPTY (* [*0] *) 45 | S_REPEAT of sere (* r[*] *) 46 | S_CLOCK of sere # 'a bexp`; (* r@c *) 47 48(****************************************************************************** 49* Formulas of Sugar Foundation Language (FL) 50******************************************************************************) 51val fl_def = 52 Hol_datatype 53 `fl = F_STRONG_BOOL of 'a bexp (* b! *) 54 | F_WEAK_BOOL of 'a bexp (* b *) 55 | F_NOT of fl (* not f *) 56 | F_AND of fl # fl (* f1 and f2 *) 57 | F_STRONG_SERE of 'a sere (* r! *) 58 | F_WEAK_SERE of 'a sere (* r *) 59 | F_NEXT of fl (* X! f *) 60 | F_UNTIL of fl # fl (* [f1 U f2] *) 61 | F_ABORT of fl # 'a bexp (* f abort b *) 62 | F_CLOCK of fl # 'a bexp (* f@b *) 63 | F_SUFFIX_IMP of 'a sere # fl`; (* r |-> f *) 64 65(****************************************************************************** 66* Formulas of Sugar Optional Branching Extension (OBE) 67******************************************************************************) 68val obe_def = 69 Hol_datatype 70 `obe = O_BOOL of 'a bexp (* boolean expression *) 71 | O_NOT of obe (* not f *) 72 | O_AND of obe # obe (* f1 and f2 *) 73 | O_EX of obe (* EX f *) 74 | O_EU of obe # obe (* E[f1 U f2] *) 75 | O_EG of obe`; (* EG f *) 76 77val _ = export_theory(); 78 79 80 81 82 83 84 85 86