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