1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory Eval_Bool 8 9imports Try_Methods 10 11begin 12 13text \<open>The eval_bool method/simproc uses the code generator setup to 14reduce terms of boolean type to True or False. Reducing booleans to 15True or False is nearly always desirable, and is a fairly good heuristic 16for when to make use of definitions/code-equations. 17 18Additional simprocs exist to reduce other types. 19\<close> 20 21ML \<open> 22structure Eval_Simproc = struct 23 24exception Failure 25 26fun mk_constname_tab ts = fold Term.add_const_names ts [] 27 |> Symtab.make_set 28 29fun is_built_from tab t = case Term.strip_comb t of 30 (Const (cn, _), ts) => Symtab.defined tab cn 31 andalso forall (is_built_from tab) ts 32 | _ => false 33 34fun eval tab ctxt ct = let 35 val t = Thm.term_of ct 36 val _ = Term.fold_aterms (fn Free _ => raise Failure 37 | Var _ => raise Failure | _ => ignore) t () 38 val _ = not (is_built_from tab t) orelse raise Failure 39 val ev = the (try (Code_Simp.dynamic_conv ctxt) ct) 40 in if is_built_from tab (Thm.term_of (Thm.rhs_of ev)) 41 then SOME ev else NONE end 42 handle Failure => NONE | Option => NONE 43 44val eval_bool = eval (mk_constname_tab [@{term "True"}, @{term "False"}]) 45val eval_nat = eval (mk_constname_tab [@{term "Suc 0"}, @{term "Suc 1"}, 46 @{term "Suc 9"}]) 47val eval_int = eval (mk_constname_tab [@{term "0 :: int"}, @{term "1 :: int"}, 48 @{term "18 :: int"}, @{term "(-9) :: int"}]) 49 50val eval_bool_simproc = Simplifier.make_simproc @{context} "eval_bool" 51 { lhss = [@{term "b :: bool"}], proc = K eval_bool } 52val eval_nat_simproc = Simplifier.make_simproc @{context} "eval_nat" 53 { lhss = [@{term "n :: nat"}], proc = K eval_nat } 54val eval_int_simproc = Simplifier.make_simproc @{context} "eval_int" 55 { lhss = [@{term "i :: int"}], proc = K eval_int } 56 57end 58\<close> 59 60method_setup eval_bool = \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' 61 (CHANGED o full_simp_tac (clear_simpset ctxt 62 addsimprocs [Eval_Simproc.eval_bool_simproc])))\<close> 63 "use code generator setup to simplify booleans in goals to True or False" 64 65method_setup eval_int_nat = \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' 66 (CHANGED o full_simp_tac (clear_simpset ctxt 67 addsimprocs [Eval_Simproc.eval_nat_simproc, Eval_Simproc.eval_int_simproc])))\<close> 68 "use code generator setup to simplify nats and ints in goals to values" 69 70add_try_method eval_bool 71 72text \<open>Testing.\<close> 73definition 74 eval_bool_test_seq :: "int list" 75where 76 "eval_bool_test_seq = [2, 3, 4, 5, 6, 7, 8]" 77 78lemma 79 "eval_bool_test_seq ! 4 = 6 \<and> (3 :: nat) < 4 80 \<and> sorted eval_bool_test_seq" 81 by eval_bool 82 83text \<open> 84A related gadget for installing constant definitions from locales 85as code equations. Useful where locales are being used to "hide" 86constants from the global state rather than to do anything tricky 87with interpretations. 88 89Installing the global definitions in this way will allow eval_bool 90etc to "see through" the hiding and decide questions about these 91constants. 92\<close> 93 94ML \<open> 95structure Add_Locale_Code_Defs = struct 96 97fun get_const_defs thy nm = Sign.consts_of thy 98 |> Consts.dest |> #constants 99 |> map fst 100 |> filter (fn s => case Long_Name.explode s of 101 [_, nm', _] => nm' = nm | _ => false) 102 |> map_filter (try (suffix "_def" #> Global_Theory.get_thm thy)) 103 |> filter (Thm.strip_shyps #> Thm.shyps_of #> null) 104 |> tap (fn xs => tracing ("Installing " ^ string_of_int (length xs) ^ " code defs")) 105 106fun setup nm thy = fold (fn t => Code.add_eqn_global (t, true)) 107 (get_const_defs thy nm) thy 108 109end 110\<close> 111 112locale eval_bool_test_locale begin 113 114definition 115 "x == (12 :: int)" 116 117definition 118 "y == (13 :: int)" 119 120definition 121 "z = (x * y) + x + y" 122 123end 124 125setup \<open>Add_Locale_Code_Defs.setup "eval_bool_test_locale"\<close> 126 127setup \<open>Add_Locale_Code_Defs.setup "eval_bool_test_locale"\<close> 128 129lemma "eval_bool_test_locale.z > 150" 130 by eval_bool 131 132end 133