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