1.1 --- a/src/Pure/Isar/locale.ML Tue May 31 11:53:34 2005 +0200
1.2 +++ b/src/Pure/Isar/locale.ML Tue May 31 11:53:35 2005 +0200
1.3 @@ -38,7 +38,7 @@
1.4 type element_i
1.5 type locale
1.6 val intern: Sign.sg -> xstring -> string
1.7 - val cond_extern: Sign.sg -> string -> xstring
1.8 + val extern: Sign.sg -> string -> xstring
1.9 val the_locale: theory -> string -> locale
1.10 val intern_attrib_elem: theory ->
1.11 ('typ, 'term, 'fact) elem -> ('typ, 'term, 'fact) elem
1.12 @@ -337,7 +337,7 @@
1.13 Symtab.join (SOME o Registrations.join) (regs1, regs2));
1.14
1.15 fun print _ (space, locs, _) =
1.16 - Pretty.strs ("locales:" :: map (NameSpace.cond_extern space o #1) (Symtab.dest locs))
1.17 + Pretty.strs ("locales:" :: map (NameSpace.extern space o #1) (Symtab.dest locs))
1.18 |> Pretty.writeln;
1.19 end;
1.20
1.21 @@ -366,11 +366,11 @@
1.22 val print_locales = GlobalLocalesData.print;
1.23
1.24 val intern = NameSpace.intern o #1 o GlobalLocalesData.get_sg;
1.25 -val cond_extern = NameSpace.cond_extern o #1 o GlobalLocalesData.get_sg;
1.26 +val extern = NameSpace.extern o #1 o GlobalLocalesData.get_sg;
1.27
1.28 -fun declare_locale name =
1.29 - GlobalLocalesData.map (fn (space, locs, regs) =>
1.30 - (NameSpace.extend (space, [name]), locs, regs));
1.31 +fun declare_locale name thy =
1.32 + thy |> GlobalLocalesData.map (fn (space, locs, regs) =>
1.33 + (Sign.declare_name (Theory.sign_of thy) name space, locs, regs));
1.34
1.35 fun put_locale name loc =
1.36 GlobalLocalesData.map (fn (space, locs, regs) =>
1.37 @@ -432,7 +432,7 @@
1.38 val (reg', sups) = Registrations.insert sg (ps, attn) reg;
1.39 val _ = if not (null sups) then warning
1.40 ("Subsumed interpretation(s) of locale " ^
1.41 - quote (cond_extern sg name) ^
1.42 + quote (extern sg name) ^
1.43 "\nby interpretation(s) with the following prefix(es):\n" ^
1.44 commas_quote (map (fn (_, ((s, _), _)) => s) sups))
1.45 else ();
1.46 @@ -543,7 +543,7 @@
1.47 let
1.48 val sign = ProofContext.sign_of ctxt;
1.49 fun prt_id (name, parms) =
1.50 - [Pretty.block (Pretty.breaks (map Pretty.str (cond_extern sign name :: parms)))];
1.51 + [Pretty.block (Pretty.breaks (map Pretty.str (extern sign name :: parms)))];
1.52 val prt_ids = List.concat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids));
1.53 val err_msg =
1.54 if forall (equal "" o #1) ids then msg
1.55 @@ -636,18 +636,8 @@
1.56 map_values I (rename_term ren) (rename_thm ren) o
1.57 map_elem {name = I, typ = I, term = I, fact = I, attrib = I, var = rename_var ren};
1.58
1.59 -fun rename_facts prfx elem =
1.60 - let
1.61 - fun qualify (arg as ((name, atts), x)) =
1.62 - if prfx = "" orelse name = "" then arg
1.63 - else ((NameSpace.pack [prfx, name], atts), x);
1.64 - in
1.65 - (case elem of
1.66 - Fixes fixes => Fixes fixes
1.67 - | Assumes asms => Assumes (map qualify asms)
1.68 - | Defines defs => Defines (map qualify defs)
1.69 - | Notes facts => Notes (map qualify facts))
1.70 - end;
1.71 +fun rename_facts prfx =
1.72 + map_elem {var = I, typ = I, term = I, fact = I, attrib = I, name = NameSpace.qualified prfx};
1.73
1.74
1.75 (* type instantiation *)
1.76 @@ -1006,7 +996,7 @@
1.77
1.78 fun activate_elems (((name, ps), axs), elems) ctxt =
1.79 let val ((ctxt', _), res) =
1.80 - foldl_map (activate_elem (name = "")) ((ProofContext.qualified true ctxt, axs), elems)
1.81 + foldl_map (activate_elem (name = "")) ((ProofContext.qualified_names ctxt, axs), elems)
1.82 handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)]
1.83 val ctxt'' = if name = "" then ctxt'
1.84 else let
1.85 @@ -1015,7 +1005,7 @@
1.86 in foldl (fn (ax, ctxt) =>
1.87 add_local_witness (name, ps') (Thm.assume (Thm.cprop_of ax)) ctxt) ctxt'' axs
1.88 end
1.89 - in (ProofContext.restore_qualified ctxt ctxt'', res) end;
1.90 + in (ProofContext.restore_naming ctxt ctxt'', res) end;
1.91
1.92 fun activate_elemss prep_facts = foldl_map (fn (ctxt, (((name, ps), axs), raw_elems)) =>
1.93 let
1.94 @@ -1600,11 +1590,6 @@
1.95 \declared with (open)\n" ^ msg ^ "\n" ^
1.96 cat_lines (map string_of_thm thms));
1.97
1.98 - val prefix_fact =
1.99 - if prfx = "" then I
1.100 - else (fn "" => ""
1.101 - | s => NameSpace.append prfx s);
1.102 -
1.103 fun inst_elem (ctxt, (Ext _)) = ctxt
1.104 | inst_elem (ctxt, (Int (Notes facts))) =
1.105 (* instantiate fact *)
1.106 @@ -1615,22 +1600,22 @@
1.107 val facts' =
1.108 map (apsnd (map (apfst (map inst_thm')))) facts
1.109 (* rename fact *)
1.110 - val facts'' = map (apfst (apfst prefix_fact)) facts'
1.111 + val facts'' = map (apfst (apfst (NameSpace.qualified prfx))) facts'
1.112 (* add attributes *)
1.113 val facts''' = map (apfst (apsnd (fn atts => atts @ attribs))) facts''
1.114 in fst (ProofContext.note_thmss_i facts''' ctxt)
1.115 end
1.116 | inst_elem (ctxt, (Int _)) = ctxt;
1.117
1.118 + (* FIXME fold o fold *)
1.119 fun inst_elems (ctxt, (id, elems)) = Library.foldl inst_elem (ctxt, elems);
1.120
1.121 fun inst_elemss ctxt elemss = Library.foldl inst_elems (ctxt, elemss);
1.122
1.123 (* main part *)
1.124
1.125 - val ctxt' = ProofContext.qualified true ctxt;
1.126 - in ProofContext.restore_qualified ctxt (inst_elemss ctxt' all_elemss)
1.127 - end;
1.128 + val ctxt' = ProofContext.qualified_names ctxt;
1.129 + in ProofContext.restore_naming ctxt (inst_elemss ctxt' all_elemss) end;
1.130
1.131
1.132 (** define locales **)
1.133 @@ -1655,7 +1640,7 @@
1.134 prt_typ T :: Pretty.brk 1 :: prt_syn syn)
1.135 | prt_fix (x, NONE, syn) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_syn syn);
1.136
1.137 - fun prt_name name = Pretty.str (ProofContext.cond_extern ctxt name);
1.138 + fun prt_name name = Pretty.str (ProofContext.extern ctxt name);
1.139 fun prt_name_atts (name, atts) =
1.140 if name = "" andalso null atts then []
1.141 else [Pretty.block (Pretty.breaks (prt_name name :: prt_atts atts @ [Pretty.str ":"]))];
1.142 @@ -1683,59 +1668,58 @@
1.143 end;
1.144
1.145
1.146 -(* store results *)
1.147
1.148 -local
1.149 +(** store results **)
1.150
1.151 -fun hide_bound_names names thy =
1.152 - thy |> PureThy.hide_thms false
1.153 - (map (Sign.full_name (Theory.sign_of thy)) (filter_out (equal "") names));
1.154 -
1.155 -in
1.156 -
1.157 -(* store exported theorem in theory *)
1.158 +(* note_thmss_qualified *)
1.159
1.160 fun note_thmss_qualified kind name args thy =
1.161 thy
1.162 |> Theory.add_path (Sign.base_name name)
1.163 + |> Theory.no_base_names
1.164 |> PureThy.note_thmss_i (Drule.kind kind) args
1.165 - |>> hide_bound_names (map (#1 o #1) args)
1.166 - |>> Theory.parent_path;
1.167 + |>> Theory.restore_naming thy;
1.168 +
1.169
1.170 (* accesses of interpreted theorems *)
1.171
1.172 -(* fully qualified name in theory is T.p.r.n where
1.173 - T: theory name, p: interpretation prefix, r: renaming prefix, n: name *)
1.174 +local
1.175
1.176 -fun global_accesses prfx name =
1.177 - if prfx = "" then
1.178 - case NameSpace.unpack name of
1.179 - [] => [""]
1.180 - | [T, n] => map NameSpace.pack [[T, n], [n]]
1.181 - | [T, r, n] => map NameSpace.pack [[T, r, n], [T, n], [r, n], [n]]
1.182 - | _ => error ("Locale accesses: illegal name " ^ quote name)
1.183 - else case NameSpace.unpack name of
1.184 - [] => [""]
1.185 - | [T, p, n] => map NameSpace.pack [[T, p, n], [p, n]]
1.186 - | [T, p, r, n] => map NameSpace.pack
1.187 - [[T, p, r, n], [T, p, n], [p, r, n], [p, n]]
1.188 - | _ => error ("Locale accesses: illegal name " ^ quote name);
1.189 +(*fully qualified name in theory is T.p.r.n where
1.190 + T: theory name, p: interpretation prefix, r: renaming prefix, n: name*)
1.191 +fun global_accesses _ [] = []
1.192 + | global_accesses "" [T, n] = [[T, n], [n]]
1.193 + | global_accesses "" [T, r, n] = [[T, r, n], [T, n], [r, n], [n]]
1.194 + | global_accesses _ [T, p, n] = [[T, p, n], [p, n]]
1.195 + | global_accesses _ [T, p, r, n] = [[T, p, r, n], [T, p, n], [p, r, n], [p, n]]
1.196 + | global_accesses _ names = error ("Bad name declaration " ^ quote (NameSpace.pack names));
1.197
1.198 -(* fully qualified name in context is p.r.n where
1.199 - p: interpretation prefix, r: renaming prefix, n: name *)
1.200 +(*fully qualified name in context is p.r.n where
1.201 + p: interpretation prefix, r: renaming prefix, n: name*)
1.202 +fun local_accesses _ [] = []
1.203 + | local_accesses "" [n] = [[n]]
1.204 + | local_accesses "" [r, n] = [[r, n], [n]]
1.205 + | local_accesses _ [p, n] = [[p, n]]
1.206 + | local_accesses _ [p, r, n] = [[p, r, n], [p, n]]
1.207 + | local_accesses _ names = error ("Bad name declaration " ^ quote (NameSpace.pack names));
1.208
1.209 -fun local_accesses prfx name =
1.210 - if prfx = "" then
1.211 - case NameSpace.unpack name of
1.212 - [] => [""]
1.213 - | [n] => map NameSpace.pack [[n]]
1.214 - | [r, n] => map NameSpace.pack [[r, n], [n]]
1.215 - | _ => error ("Locale accesses: illegal name " ^ quote name)
1.216 - else case NameSpace.unpack name of
1.217 - [] => [""]
1.218 - | [p, n] => map NameSpace.pack [[p, n]]
1.219 - | [p, r, n] => map NameSpace.pack [[p, r, n], [p, n]]
1.220 - | _ => error ("Locale accesses: illegal name " ^ quote name);
1.221 +in
1.222 +
1.223 +fun global_note_accesses_i kind prfx args thy =
1.224 + thy
1.225 + |> Theory.qualified_names
1.226 + |> Theory.custom_accesses (global_accesses prfx)
1.227 + |> PureThy.note_thmss_i kind args
1.228 + |>> Theory.restore_naming thy;
1.229 +
1.230 +fun local_note_accesses_i prfx args ctxt =
1.231 + ctxt
1.232 + |> ProofContext.qualified_names
1.233 + |> ProofContext.custom_accesses (local_accesses prfx)
1.234 + |> ProofContext.note_thmss_i args
1.235 + |>> ProofContext.restore_naming ctxt;
1.236 +
1.237 +end;
1.238
1.239
1.240 (* store instantiations of args for all registered interpretations
1.241 @@ -1743,14 +1727,11 @@
1.242
1.243 fun note_thmss_registrations kind target args thy =
1.244 let
1.245 - val ctxt = ProofContext.init thy;
1.246 - val sign = Theory.sign_of thy;
1.247 -
1.248 val (parms, parmTs_o) =
1.249 the_locale thy target |> #params |> fst |> map fst |> split_list;
1.250 val parmvTs = map (Type.varifyT o valOf) parmTs_o;
1.251 - val ids = flatten (ctxt, intern_expr sign) (([], Symtab.empty), Expr (Locale target))
1.252 - |> fst |> fst |> map fst;
1.253 + val ids = flatten (ProofContext.init thy, intern_expr (Theory.sign_of thy))
1.254 + (([], Symtab.empty), Expr (Locale target)) |> fst |> fst |> map fst;
1.255
1.256 val regs = get_global_registrations thy target;
1.257
1.258 @@ -1758,9 +1739,10 @@
1.259
1.260 fun activate (thy, (vts, ((prfx, atts2), _))) =
1.261 let
1.262 + val sg = Theory.sign_of thy;
1.263 val ts = map Logic.unvarify vts;
1.264 (* type instantiation *)
1.265 - val vtinst = Library.foldl (Type.typ_match (Sign.tsig_of sign))
1.266 + val vtinst = Library.foldl (Type.typ_match (Sign.tsig_of sg))
1.267 (Vartab.empty, (parmvTs ~~ map Term.fastype_of ts));
1.268 val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T))
1.269 |> Symtab.make;
1.270 @@ -1771,20 +1753,17 @@
1.271 val ids' = map (apsnd vinst_names) ids;
1.272 val prems = List.concat (map (snd o valOf o get_global_registration thy) ids');
1.273 val args' = map (fn ((n, atts), [(ths, [])]) =>
1.274 - ((if prfx = "" orelse n = "" then "" else NameSpace.pack [prfx, n],
1.275 + ((if prfx = "" orelse n = "" then "" else NameSpace.pack [prfx, n], (* FIXME *)
1.276 map (Attrib.global_attribute_i thy) (atts @ atts2)),
1.277 - [(map (Drule.standard o Drule.satisfy_hyps prems o inst_tab_thm sign (inst, tinst)) ths, [])]))
1.278 + [(map (Drule.standard o Drule.satisfy_hyps prems o inst_tab_thm sg (inst, tinst)) ths, [])]))
1.279 args;
1.280 - in
1.281 - PureThy.note_thmss_accesses_i (global_accesses prfx) (Drule.kind kind) args' thy |> fst
1.282 - end;
1.283 + in global_note_accesses_i (Drule.kind kind) prfx args' thy |> fst end;
1.284 in Library.foldl activate (thy, regs) end;
1.285
1.286
1.287 fun smart_note_thmss kind NONE = PureThy.note_thmss_i (Drule.kind kind)
1.288 | smart_note_thmss kind (SOME loc) = note_thmss_qualified kind loc;
1.289
1.290 -end;
1.291
1.292 local
1.293
1.294 @@ -2075,9 +2054,7 @@
1.295 (* discharge hyps *)
1.296 val facts'' = map (apsnd (map (apfst (map disch)))) facts';
1.297 (* prefix names *)
1.298 - val facts''' = map (apfst (apfst (fn name =>
1.299 - if prfx = "" orelse name = "" then name
1.300 - else NameSpace.pack [prfx, name]))) facts'';
1.301 + val facts''' = map (apfst (apfst (NameSpace.qualified prfx))) facts'';
1.302 in
1.303 fst (note_thmss prfx facts''' thy_ctxt)
1.304 end;
1.305 @@ -2107,12 +2084,12 @@
1.306 val global_activate_facts_elemss = gen_activate_facts_elemss
1.307 (fn thy => fn (name, ps) =>
1.308 get_global_registration thy (name, map Logic.varify ps))
1.309 - (fn prfx => PureThy.note_thmss_accesses_i (global_accesses prfx)
1.310 - (Drule.kind ""))
1.311 + (global_note_accesses_i (Drule.kind ""))
1.312 Attrib.global_attribute_i Drule.standard;
1.313 +
1.314 val local_activate_facts_elemss = gen_activate_facts_elemss
1.315 get_local_registration
1.316 - (fn prfx => ProofContext.note_thmss_accesses_i (local_accesses prfx))
1.317 + local_note_accesses_i
1.318 Attrib.context_attribute_i I;
1.319
1.320 fun gen_prep_registration mk_ctxt is_local read_terms test_reg put_reg activate