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