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