1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory Locale_Abbrev
8  imports Main
9  keywords "revert_abbrev" :: thy_decl and "locale_abbrev" :: thy_decl
10begin
11
12(*
13  "Normal" abbreviations in locales provide input syntax only, i.e. they are not contracted on
14  pretty printing. Presumably this is because a) this would not work with fixed variables on locale
15  export and b) one cannot make a global decision whether everything is to be abbreviated only
16  inside the locale or inside and outside, and so the safe option is to provide input only.
17
18  This theory provides two commands:
19    - revert_abbrev (print-mode) name (:: lthy \<Rightarrow> lthy)
20        causes an already defined abbreviation \<open>name\<close> to always be contracted on pretty printing
21        for the specified optional print mode. This only works when the abbreviation does not
22        mention any fixed variables of the locale.
23
24    - locale_abbrev spec (:: lthy \<Rightarrow> lthy)
25        is an alias for the standard abbreviation command, followed by revert_abbrev.
26        This is the command to use for abbreviations that should be contracted inside locales.
27        Contrary to standard abbreviations, this command cannot mention fixed variables of the
28        locale.
29*)
30
31ML \<open>
32local
33
34fun revert_abbrev (mode,name) lthy =
35  let
36    val the_const = (fst o dest_Const) oo Proof_Context.read_const {proper = true, strict = false};
37  in
38    Local_Theory.raw_theory (Sign.revert_abbrev (fst mode) (the_const lthy name)) lthy
39  end
40
41fun name_of spec lthy = Local_Defs.abs_def (Syntax.read_term lthy spec) |> #1 |> #1
42
43in
44
45val _ =
46  Outer_Syntax.local_theory @{command_keyword revert_abbrev}
47    "make an abbreviation available for output"
48    (Parse.syntax_mode -- Parse.const >> revert_abbrev)
49
50val _ =
51  Outer_Syntax.local_theory' @{command_keyword locale_abbrev}
52    "constant abbreviation that provides also provides printing in locales"
53    (Parse.syntax_mode -- Scan.option Parse_Spec.constdecl -- Parse.prop -- Parse.for_fixes
54      >> (fn (((mode, decl), spec), params) => fn restricted => fn lthy =>
55           lthy
56           |> Local_Theory.open_target |> snd
57           |> Specification.abbreviation_cmd mode decl params spec restricted
58           |> Local_Theory.close_target (* commit new abbrev. name *)
59           |> revert_abbrev (mode, name_of spec lthy)));
60
61end
62\<close>
63
64end