1(*****************************************************************************)
2(* Executing the Sugar2 semantics                                            *)
3(*****************************************************************************)
4
5structure ExecuteTools :> ExecuteTools =
6struct
7
8(*
9quietdec := true;
10loadPath := "../official-semantics"   ::
11            "../executable-semantics" ::
12            "../regexp"               ::
13            !loadPath;
14map load
15 ["bossLib", "metisLib", "matcherTheory", "KripkeTheory", "UnclockedSemanticsTheory",
16  "SyntacticSugarTheory", "ClockedSemanticsTheory", "RewritesTheory",
17  "rich_listTheory", "intLib", "res_quanLib", "res_quanTheory"];
18open KripkeTheory FinitePSLPathTheory PSLPathTheory SyntaxTheory SyntacticSugarTheory
19     UnclockedSemanticsTheory ClockedSemanticsTheory RewritesTheory
20     arithmeticTheory listTheory rich_listTheory res_quanLib res_quanTheory
21     ClockedSemanticsTheory metisLib matcherTheory;
22val _ = intLib.deprecate_int();
23quietdec := false;
24*)
25
26open HolKernel Parse boolLib;
27open bossLib metisLib pairTheory combinTheory listTheory rich_listTheory
28     pred_setTheory arithmeticTheory;
29open regexpLib SyntaxTheory UnclockedSemanticsTheory PropertiesTheory
30     ExecuteSemanticsTheory;
31
32(******************************************************************************
33* Evaluating expressions of the form x IN {y1; y2; ...; yn}
34******************************************************************************)
35
36(* For the current set of Sugar2 example properties, the following INSERT
37   theorems seem to work better than this general conversion.
38val _ =
39 computeLib.add_convs
40  [(``$IN``,
41    2,
42    (pred_setLib.SET_SPEC_CONV ORELSEC pred_setLib.IN_CONV EVAL))];
43*)
44
45val () = computeLib.add_funs
46  [pred_setTheory.IN_INSERT,
47   pred_setTheory.NOT_IN_EMPTY];
48
49(******************************************************************************
50* Evaluating Sugar2 formulas
51******************************************************************************)
52val _ = computeLib.add_funs
53  [PSLPathTheory.SEL_REC_AUX,
54   UF_SEM_F_UNTIL_REC,
55   B_SEM,
56(* Prefer the optimizing version of
57   EVAL_US_SEM,
58*)
59   EVAL_UF_SEM_F_SUFFIX_IMP,
60   EVAL_UF_SEM_F_WEAK_IMP,
61   UF_SEM_F_STRONG_IMP_F_SUFFIX_IMP,
62   S_CLOCK_COMP_ELIM,
63   F_TRUE_CLOCK_COMP_ELIM];
64
65(******************************************************************************
66* For simplification during symbolic evaluation of Sugar2 formulas
67******************************************************************************)
68
69(* Rejected by computeLib.add_funs, but (used to be) useful for simplification.
70val SOME_EL_F =
71 prove
72  (``SOME_EL (\x. F) l = F``,
73   Induct_on `l`
74    THEN RW_TAC std_ss [SOME_EL]);
75*)
76
77val EXISTS_COND = prove
78  (``!p c a b.
79       EXISTS p (if c then a else b) = if c then EXISTS p a else EXISTS p b``,
80   RW_TAC std_ss []);
81
82val COND_SIMP = prove
83  (``!c a b.
84       (COND c a F = c /\ a) /\ (COND c a T = ~c \/ a) /\
85       (COND c T b = c \/ b) /\ (COND c F b = ~c /\ b)``,
86   RW_TAC std_ss [IMP_DISJ_THM]);
87
88val () = computeLib.add_funs
89  [EXISTS_COND,
90   COND_SIMP,
91   DECIDE ``SUC n > 0 = T``];
92
93(*---------------------------------------------------------------------------*)
94(* Executing the US_SEM optimizer.                                           *)
95(*---------------------------------------------------------------------------*)
96
97val US_SEM_tm = ``US_SEM : ('a -> bool) list -> 'a sere -> bool``;
98
99val S_REPEAT_IDEMPOTENT1 = prove
100  (``!w r x.
101       US_SEM w (S_CAT (S_REPEAT r, S_CAT (S_REPEAT r, x))) =
102       US_SEM w (S_CAT (S_REPEAT r, x))``,
103   REWRITE_TAC [GSYM S_CAT_ASSOC]
104   THEN ONCE_REWRITE_TAC [US_SEM_def]
105   THEN REWRITE_TAC [S_REPEAT_IDEMPOTENT]);
106
107val US_SEM_conv =
108  REWRITE_CONV [S_CAT_ASSOC, S_REPEAT_IDEMPOTENT, S_REPEAT_IDEMPOTENT1]
109  THENC REWR_CONV EVAL_US_SEM
110  THENC EVAL;
111
112val () = computeLib.add_convs [(US_SEM_tm, 2, US_SEM_conv)];
113
114end
115