1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory Value_Abbreviation
8
9imports Main
10
11keywords "value_abbreviation" :: thy_decl
12
13begin
14
15text \<open>Computing values and saving as abbreviations.
16
17Useful in program verification to handle some configuration constant
18(e.g. n = 4) which may change. This mechanism can be used to give
19names (abbreviations) to other related constants (e.g. 2 ^ n, 2 ^ n - 1,
20[1 .. n], rev [1 .. n]) which may appear repeatedly.
21\<close>
22
23ML \<open>
24structure Value_Abbreviation = struct
25fun value_and_abbreviation mode name expr int ctxt = let
26    val decl = (name, NONE, Mixfix.NoSyn)
27    val expr = Syntax.read_term ctxt expr
28    val eval_expr =Value_Command.value ctxt expr
29    val lhs = Free (Binding.name_of name, fastype_of expr)
30    val eq = Logic.mk_equals (lhs, eval_expr)
31    val ctxt = Specification.abbreviation mode (SOME decl) [] eq int ctxt
32    val pretty_eq = Syntax.pretty_term ctxt eq
33  in Pretty.writeln pretty_eq; ctxt end
34
35val _ =
36  Outer_Syntax.local_theory' @{command_keyword value_abbreviation}
37    "setup abbreviation for evaluated value"
38    (Parse.syntax_mode -- Parse.binding -- Parse.term
39      >> (fn ((mode, name), expr) => value_and_abbreviation mode name expr));
40
41end
42\<close>
43
44text \<open>Testing it out.
45Unfortunately locale/experiment/notepad all won't work here because
46the code equation setup is all global.
47\<close>
48
49definition
50  "value_abbreviation_test_config_constant_1 = (24 :: nat)"
51
52definition
53  "value_abbreviation_test_config_constant_2 = (5 :: nat)"
54
55value_abbreviation (input)
56  value_abbreviation_test_important_magic_number
57    "((2 :: int) ^ value_abbreviation_test_config_constant_1)
58     - (2 ^ value_abbreviation_test_config_constant_2)"
59
60value_abbreviation (input)
61  value_abbreviation_test_range_of_options
62    "rev [int value_abbreviation_test_config_constant_2
63          .. int value_abbreviation_test_config_constant_1]"
64
65end
66