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