1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7(*
8  Post-hoc qualification of global constants, facts and types using name space aliasing.
9  Can be used to add mandatory qualification to otherwise non-localised commands (i.e. "record",
10  "instantiation").
11
12  This is a hack that should be replaced with proper "context begin ... end" blocks when
13  commands are appropriately localized.
14*)
15
16theory Qualify
17imports Main
18keywords "qualify" :: thy_decl and "end_qualify" :: thy_decl
19begin
20ML \<open>
21
22type qualify_args = {name : string, target_name : string}
23
24structure Data = Theory_Data
25  (
26    type T = (theory * qualify_args) option;
27    val empty = NONE;
28    val extend = I;
29    fun merge ((_, _) : T * T) = NONE;
30  );
31
32fun get_qualify thy = Data.get thy;
33
34fun make_bind space thy nm =
35  let
36    val short_name =
37      Name_Space.extern (Proof_Context.init_global thy |> Config.put Name_Space.names_short true) space nm
38      |> Long_Name.explode |> rev |> tl |> rev;
39    val long_name = Long_Name.explode nm |> tl |> rev |> tl |> rev;
40
41    fun do_make_bind (short_qual :: l) (_ :: l') b = Binding.qualify true short_qual (do_make_bind l l' b)
42      | do_make_bind [] (long_qual :: l) b = Binding.qualify false long_qual (do_make_bind [] l b)
43      | do_make_bind [] [] b = b
44      | do_make_bind _ _ _ =
45        raise Fail ("Mismatched long and short identifiers:\nsource:" ^ nm ^ "\nshort:" ^ (@{make_string} short_name) ^ "\nlong:" ^
46          (@{make_string} long_name))
47
48    val b = do_make_bind short_name long_name (Binding.make (Long_Name.base_name nm, Position.none))
49
50  in b end;
51
52fun get_new_facts old_thy facts =
53  let
54    val space = Facts.space_of facts;
55  in
56     Facts.dest_static false [Global_Theory.facts_of old_thy] facts
57     |> map (fn (nm, _) => `(make_bind space old_thy) nm)
58  end
59
60fun get_new_consts old_thy consts =
61  let
62    val new_consts = #constants (Consts.dest consts)
63    |> map fst;
64
65    val space = #const_space (Consts.dest consts);
66
67    val consts =
68      filter (fn nm => not (can (Consts.the_const (Sign.consts_of old_thy)) nm) andalso
69                       can (Consts.the_const consts) nm) new_consts
70      |> map (fn nm => `(make_bind space old_thy) nm);
71
72  in consts end;
73
74fun get_new_types old_thy types =
75  let
76    val new_types = #types (Type.rep_tsig types);
77    val space = Name_Space.space_of_table new_types;
78
79    val old_types = #types (Type.rep_tsig (Sign.tsig_of old_thy));
80
81    val types = (new_types
82      |> Name_Space.fold_table (fn (nm, _) =>
83           not (Name_Space.defined old_types nm) ? cons nm)) []
84      |> map (fn nm => `(make_bind space old_thy) nm);
85  in types end;
86
87fun add_qualified qual nm =
88  let
89    val nm' = Long_Name.explode nm |> tl |> hd;
90  in if qual = nm' then cons nm else I end
91  handle List.Empty => I
92
93fun make_bind_local nm =
94  let
95    val base = Long_Name.explode nm |> tl |> tl |> rev |> tl |> rev;
96  in fold (Binding.qualify true) base (Binding.make (Long_Name.base_name nm, Position.none)) end;
97
98fun set_global_qualify (args : qualify_args) thy =
99  let
100    val _ = Locale.check thy (#target_name args, Position.none)
101    val _ = case get_qualify thy of SOME _ => error "Already in a qualify block!" | NONE => ();
102
103    val thy' = Data.map (K (SOME (thy,args))) thy;
104
105  in  thy'  end
106
107val _ =
108  Outer_Syntax.command @{command_keyword qualify} "begin global qualification"
109    (Parse.name -- Parse.opt_target>>
110      (fn (str, target) =>
111          Toplevel.theory (set_global_qualify {name = str, target_name = case target of SOME (nm, _) => nm | _ => str})));
112
113fun syntax_alias global_alias local_alias b name =
114  Local_Theory.declaration {syntax = true, pervasive = true} (fn phi =>
115    let val b' = Morphism.binding phi b
116    in Context.mapping (global_alias b' name) (local_alias b' name) end);
117
118val alias_fact = syntax_alias Global_Theory.alias_fact Proof_Context.alias_fact;
119val const_alias = syntax_alias Sign.const_alias Proof_Context.const_alias;
120val type_alias = syntax_alias Sign.type_alias Proof_Context.type_alias;
121
122
123
124fun end_global_qualify thy =
125  let
126    val (old_thy, args) =
127      case get_qualify thy of
128        SOME x => x
129      | NONE => error "Not in a global qualify"
130
131    val nm = #name args
132
133    val facts = get_new_facts old_thy (Global_Theory.facts_of thy);
134
135    val consts = get_new_consts old_thy (Sign.consts_of thy);
136
137    val types = get_new_types old_thy (Sign.tsig_of thy);
138
139    val thy'' = thy
140     |> (fn thy => fold (Global_Theory.hide_fact false o snd) facts thy)
141     |> (fn thy => fold (Sign.hide_const false o snd) consts thy)
142     |> (fn thy => fold (Sign.hide_type false o snd) types thy);
143
144    val lthy = Named_Target.begin (#target_name args, Position.none) thy''
145      |> Local_Theory.map_background_naming (Name_Space.parent_path #> Name_Space.mandatory_path nm);
146
147    val lthy' = lthy
148      |> fold (uncurry alias_fact) facts
149      |> fold (uncurry const_alias) consts
150      |> fold (uncurry type_alias) types;
151
152  in Local_Theory.exit_global lthy' |> Data.map (K NONE) end
153
154val _ =
155  Outer_Syntax.command @{command_keyword end_qualify} "end global qualification"
156    (Scan.succeed
157      (Toplevel.theory end_global_qualify));
158
159
160\<close>
161
162setup \<open>Theory.at_end
163  (fn thy => case get_qualify thy of SOME (_, nm) =>
164    SOME (end_global_qualify thy) | NONE => NONE)\<close>
165
166end
167