author  wenzelm 
Tue, 26 Feb 2002 21:46:03 +0100  
changeset 12958  99f5c4a37b29 
parent 12862  c66cb5591191 
child 13211  aabdb4b33625 
permissions  rwrr 
12014  1 
(* Title: Pure/Isar/locale.ML 
11896  2 
ID: $Id$ 
12958  3 
Author: Markus Wenzel, LMU/TU München 
11896  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
5 

12058  6 
Locales  Isar proof contexts as metalevel predicates, with local 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

7 
syntax and implicit structures. 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

8 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

9 
Draws some basic ideas from Florian Kammüller's original version of 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

10 
locales, but uses the richer infrastructure of Isar instead of the raw 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

11 
metalogic. Furthermore, we provide structured import of contexts 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

12 
(with merge and rename operations), as well as typeinference of the 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

13 
signature parts. 
11896  14 
*) 
15 

16 
signature LOCALE = 

17 
sig 

12046  18 
type context 
19 
datatype ('typ, 'term, 'fact, 'att) elem = 

12058  20 
Fixes of (string * 'typ option * mixfix option) list  
12046  21 
Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list  
22 
Defines of ((string * 'att list) * ('term * 'term list)) list  

12273  23 
Notes of ((string * 'att list) * ('fact * 'att list) list) list 
24 
datatype expr = 

25 
Locale of string  

26 
Rename of expr * string option list  

27 
Merge of expr list 

28 
val empty: expr 

29 
datatype ('typ, 'term, 'fact, 'att) elem_expr = 

30 
Elem of ('typ, 'term, 'fact, 'att) elem  Expr of expr 

12046  31 
type 'att element 
32 
type 'att element_i 

33 
type locale 

34 
val intern: Sign.sg > xstring > string 

12014  35 
val cond_extern: Sign.sg > string > xstring 
12502  36 
val the_locale: theory > string > locale 
12273  37 
val attribute: ('att > context attribute) > ('typ, 'term, 'thm, 'att) elem_expr 
38 
> ('typ, 'term, 'thm, context attribute) elem_expr 

12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

39 
val locale_facts: theory > xstring > thm list 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

40 
val locale_facts_i: theory > string > thm list 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

41 
val read_context_statement: xstring option > context attribute element list > 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

42 
(string * (string list * string list)) list list > context > 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

43 
string option * context * context * (term * (term list * term list)) list list 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

44 
val cert_context_statement: string option > context attribute element_i list > 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

45 
(term * (term list * term list)) list list > context > 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

46 
string option * context * context * (term * (term list * term list)) list list 
12758  47 
val print_locales: theory > unit 
48 
val print_locale: theory > expr > context attribute element list > unit 

12273  49 
val add_locale: bstring > expr > context attribute element list > theory > theory 
50 
val add_locale_i: bstring > expr > context attribute element_i list > theory > theory 

12958  51 
val smart_have_thmss: string > (string * 'a) Library.option > 
52 
((bstring * theory attribute list) * (thm list * theory attribute list) list) list > 

53 
theory > theory * (bstring * thm list) list 

12711  54 
val have_thmss: string > xstring > 
55 
((bstring * context attribute list) * (xstring * context attribute list) list) list > 

56 
theory > theory * (bstring * thm list) list 

57 
val have_thmss_i: string > string > 

58 
((bstring * context attribute list) * (thm list * context attribute list) list) list > 

59 
theory > theory * (bstring * thm list) list 

12958  60 
val add_thmss: string > ((string * thm list) * context attribute list) list > 
61 
context * theory > (context * theory) * thm list list 

11896  62 
val setup: (theory > theory) list 
63 
end; 

12839  64 

12289  65 
structure Locale: LOCALE = 
11896  66 
struct 
67 

12273  68 
(** locale elements and expressions **) 
11896  69 

12014  70 
type context = ProofContext.context; 
11896  71 

12046  72 
datatype ('typ, 'term, 'fact, 'att) elem = 
12058  73 
Fixes of (string * 'typ option * mixfix option) list  
12046  74 
Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list  
75 
Defines of ((string * 'att list) * ('term * 'term list)) list  

12273  76 
Notes of ((string * 'att list) * ('fact * 'att list) list) list; 
77 

12839  78 
datatype fact_kind = Assume  Define  Note; 
79 

12273  80 
datatype expr = 
81 
Locale of string  

82 
Rename of expr * string option list  

83 
Merge of expr list; 

11896  84 

12273  85 
val empty = Merge []; 
86 

87 
datatype ('typ, 'term, 'fact, 'att) elem_expr = 

88 
Elem of ('typ, 'term, 'fact, 'att) elem  Expr of expr; 

89 

90 
type 'att element = (string, string, string, 'att) elem_expr; 

91 
type 'att element_i = (typ, term, thm list, 'att) elem_expr; 

12070  92 

93 
type locale = 

12289  94 
{import: expr, (*dynamic import*) 
95 
elems: ((typ, term, thm list, context attribute) elem * stamp) list, (*static content*) 

12839  96 
text: ((string * typ) list * term list) * ((string * typ) list * (term * term) list), 
97 
(*local predicate specification and definitions*) 

98 
params: (string * typ option) list * string list}; (*all vs. local params*) 

12063  99 

12839  100 
fun make_locale import elems text params = 
101 
{import = import, elems = elems, text = text, params = params}: locale; 

12063  102 

11896  103 

104 

105 
(** theory data **) 

106 

107 
structure LocalesArgs = 

108 
struct 

12014  109 
val name = "Isar/locales"; 
12063  110 
type T = NameSpace.T * locale Symtab.table; 
11896  111 

12063  112 
val empty = (NameSpace.empty, Symtab.empty); 
113 
val copy = I; 

12118  114 
val prep_ext = I; 
12289  115 

116 
(*joining of locale elements: only facts may be added later!*) 

12839  117 
fun join ({import, elems, text, params}: locale, {elems = elems', ...}: locale) = 
118 
Some (make_locale import (gen_merge_lists eq_snd elems elems') text params); 

12273  119 
fun merge ((space1, locs1), (space2, locs2)) = 
12289  120 
(NameSpace.merge (space1, space2), Symtab.join join (locs1, locs2)); 
121 

12273  122 
fun print _ (space, locs) = 
123 
Pretty.strs ("locales:" :: map (NameSpace.cond_extern space o #1) (Symtab.dest locs)) 

12014  124 
> Pretty.writeln; 
11896  125 
end; 
126 

127 
structure LocalesData = TheoryDataFun(LocalesArgs); 

128 
val print_locales = LocalesData.print; 

129 

12289  130 
val intern = NameSpace.intern o #1 o LocalesData.get_sg; 
131 
val cond_extern = NameSpace.cond_extern o #1 o LocalesData.get_sg; 

132 

12277  133 

134 
(* access locales *) 

135 

12063  136 
fun declare_locale name = 
137 
LocalesData.map (apfst (fn space => (NameSpace.extend (space, [name])))); 

11896  138 

12273  139 
fun put_locale name loc = LocalesData.map (apsnd (fn locs => Symtab.update ((name, loc), locs))); 
12063  140 
fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy), name); 
11896  141 

12014  142 
fun the_locale thy name = 
143 
(case get_locale thy name of 

144 
Some loc => loc 

145 
 None => error ("Unknown locale " ^ quote name)); 

11896  146 

12046  147 

12277  148 
(* diagnostics *) 
12273  149 

12277  150 
fun err_in_locale ctxt msg ids = 
151 
let 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

152 
val sign = ProofContext.sign_of ctxt; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

153 
fun prt_id (name, parms) = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

154 
[Pretty.block (Pretty.breaks (map Pretty.str (cond_extern sign name :: parms)))]; 
12289  155 
val prt_ids = flat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids)); 
12502  156 
val err_msg = 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

157 
if forall (equal "" o #1) ids then msg 
12502  158 
else msg ^ "\n" ^ Pretty.string_of (Pretty.block 
159 
(Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids)); 

160 
in raise ProofContext.CONTEXT (err_msg, ctxt) end; 

12063  161 

12277  162 

163 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

164 
(** primitives **) 
12046  165 

12277  166 
(* renaming *) 
12263  167 

168 
fun rename ren x = if_none (assoc_string (ren, x)) x; 

169 

170 
fun rename_term ren (Free (x, T)) = Free (rename ren x, T) 

171 
 rename_term ren (t $ u) = rename_term ren t $ rename_term ren u 

172 
 rename_term ren (Abs (x, T, t)) = Abs (x, T, rename_term ren t) 

173 
 rename_term _ a = a; 

174 

175 
fun rename_thm ren th = 

176 
let 

177 
val {sign, hyps, prop, maxidx, ...} = Thm.rep_thm th; 

178 
val cert = Thm.cterm_of sign; 

12502  179 
val (xs, Ts) = Library.split_list (foldl Term.add_frees ([], prop :: hyps)); 
12263  180 
val xs' = map (rename ren) xs; 
181 
fun cert_frees names = map (cert o Free) (names ~~ Ts); 

182 
fun cert_vars names = map (cert o Var o apfst (rpair (maxidx + 1))) (names ~~ Ts); 

183 
in 

184 
if xs = xs' then th 

185 
else 

186 
th 

187 
> Drule.implies_intr_list (map cert hyps) 

188 
> Drule.forall_intr_list (cert_frees xs) 

189 
> Drule.forall_elim_list (cert_vars xs) 

190 
> Thm.instantiate ([], cert_vars xs ~~ cert_frees xs') 

191 
> (fn th' => Drule.implies_elim_list th' (map (Thm.assume o cert o rename_term ren) hyps)) 

192 
end; 

193 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

194 
fun rename_elem ren (Fixes fixes) = Fixes (fixes > map (fn (x, T, mx) => 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

195 
let val x' = rename ren x in 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

196 
if x = x' then (x, T, mx) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

197 
else (x', T, if mx = None then mx else Some Syntax.NoSyn) (*drop syntax*) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

198 
end)) 
12263  199 
 rename_elem ren (Assumes asms) = Assumes (map (apsnd (map (fn (t, (ps, qs)) => 
200 
(rename_term ren t, (map (rename_term ren) ps, map (rename_term ren) qs))))) asms) 

201 
 rename_elem ren (Defines defs) = Defines (map (apsnd (fn (t, ps) => 

202 
(rename_term ren t, map (rename_term ren) ps))) defs) 

12273  203 
 rename_elem ren (Notes facts) = Notes (map (apsnd (map (apfst (map (rename_thm ren))))) facts); 
12263  204 

12839  205 
fun rename_text ren ((xs, body), (ys, defs)) = 
206 
((map (apfst (rename ren)) xs, map (rename_term ren) body), 

207 
(map (apfst (rename ren)) ys, map (pairself (rename_term ren)) defs)); 

208 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

209 
fun rename_facts prfx elem = 
12307  210 
let 
12323  211 
fun qualify (arg as ((name, atts), x)) = 
212 
if name = "" then arg 

213 
else ((NameSpace.pack (filter_out (equal "") (prfx @ [name])), atts), x); 

12307  214 
in 
215 
(case elem of 

216 
Fixes fixes => Fixes fixes 

217 
 Assumes asms => Assumes (map qualify asms) 

218 
 Defines defs => Defines (map qualify defs) 

219 
 Notes facts => Notes (map qualify facts)) 

220 
end; 

221 

12263  222 

12502  223 
(* type instantiation *) 
224 

225 
fun inst_type [] T = T 

226 
 inst_type env T = Term.map_type_tfree (fn v => if_none (assoc (env, v)) (TFree v)) T; 

227 

228 
fun inst_term [] t = t 

229 
 inst_term env t = Term.map_term_types (inst_type env) t; 

230 

231 
fun inst_thm [] th = th 

232 
 inst_thm env th = 

233 
let 

234 
val {sign, hyps, prop, maxidx, ...} = Thm.rep_thm th; 

12575  235 
val cert = Thm.cterm_of sign; 
236 
val certT = Thm.ctyp_of sign; 

12579  237 
val tfrees = foldr Term.add_term_tfree_names (prop :: hyps, []); 
238 
val env' = filter (fn ((a, _), _) => a mem_string tfrees) env; 

12502  239 
in 
240 
if null env' then th 

241 
else 

242 
th 

243 
> Drule.implies_intr_list (map cert hyps) 

12575  244 
> Drule.tvars_intr_list (map (#1 o #1) env') 
12502  245 
> (fn (th', al) => th' > 
246 
Thm.instantiate ((map (fn ((a, _), T) => (the (assoc (al, a)), certT T)) env'), [])) 

247 
> (fn th'' => Drule.implies_elim_list th'' 

248 
(map (Thm.assume o cert o inst_term env') hyps)) 

249 
end; 

250 

251 
fun inst_elem env (Fixes fixes) = 

252 
Fixes (map (fn (x, T, mx) => (x, apsome (inst_type env) T, mx)) fixes) 

253 
 inst_elem env (Assumes asms) = Assumes (map (apsnd (map (fn (t, (ps, qs)) => 

254 
(inst_term env t, (map (inst_term env) ps, map (inst_term env) qs))))) asms) 

255 
 inst_elem env (Defines defs) = Defines (map (apsnd (fn (t, ps) => 

256 
(inst_term env t, map (inst_term env) ps))) defs) 

257 
 inst_elem env (Notes facts) = Notes (map (apsnd (map (apfst (map (inst_thm env))))) facts); 

258 

12839  259 
fun inst_text env ((xs, body), (ys, defs)) = 
260 
((map (apsnd (inst_type env)) xs, map (inst_term env) body), 

261 
(map (apsnd (inst_type env)) ys, map (pairself (inst_term env)) defs)); 

262 

12502  263 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

264 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

265 
(** structured contexts: rename + merge + implicit type instantiation **) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

266 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

267 
(* parameter types *) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

268 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

269 
fun frozen_tvars ctxt Ts = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

270 
let 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

271 
val tvars = rev (foldl Term.add_tvarsT ([], Ts)); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

272 
val tfrees = map TFree 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

273 
(Term.invent_type_names (ProofContext.used_types ctxt) (length tvars) ~~ map #2 tvars); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

274 
in map #1 tvars ~~ tfrees end; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

275 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

276 
fun unify_frozen ctxt maxidx Ts Us = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

277 
let 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

278 
val tsig = Sign.tsig_of (ProofContext.sign_of ctxt); 
12546  279 
fun unify (env, (Some T, Some U)) = (Type.unify tsig env (U, T) 
280 
handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], [])) 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

281 
 unify (env, _) = env; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

282 
fun paramify (i, None) = (i, None) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

283 
 paramify (i, Some T) = apsnd Some (Type.paramify_dummies (i, T)); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

284 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

285 
val (maxidx', Ts') = foldl_map paramify (maxidx, Ts); 
12727  286 
val (maxidx'', Us') = foldl_map paramify (maxidx', Us); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

287 
val (unifier, _) = foldl unify ((Vartab.empty, maxidx''), Ts' ~~ Us'); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

288 
val Vs = map (apsome (Envir.norm_type unifier)) Us'; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

289 
val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (mapfilter I Vs)); 
12532  290 
in map (apsome (Envir.norm_type unifier')) Vs end; 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

291 

12730  292 
fun params_of elemss = gen_distinct eq_fst (flat (map (snd o fst) elemss)); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

293 
fun param_types ps = mapfilter (fn (_, None) => None  (x, Some T) => Some (x, T)) ps; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

294 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

295 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

296 
(* flatten expressions *) 
11896  297 

12510  298 
local 
12502  299 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

300 
fun unique_parms ctxt elemss = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

301 
let 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

302 
val param_decls = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

303 
flat (map (fn ((name, (ps, qs)), _) => map (rpair (name, ps)) qs) elemss) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

304 
> Symtab.make_multi > Symtab.dest; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

305 
in 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

306 
(case find_first (fn (_, ids) => length ids > 1) param_decls of 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

307 
Some (q, ids) => err_in_locale ctxt ("Multiple declaration of parameter " ^ quote q) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

308 
(map (apsnd (map fst)) ids) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

309 
 None => map (apfst (apsnd #1)) elemss) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

310 
end; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

311 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

312 
fun unify_parms ctxt fixed_parms raw_parmss = 
12502  313 
let 
314 
val tsig = Sign.tsig_of (ProofContext.sign_of ctxt); 

315 
val maxidx = length raw_parmss; 

316 
val idx_parmss = (0 upto maxidx  1) ~~ raw_parmss; 

317 

318 
fun varify i = Term.map_type_tfree (fn (a, S) => TVar ((a, i), S)); 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

319 
fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

320 
val parms = fixed_parms @ flat (map varify_parms idx_parmss); 
12502  321 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

322 
fun unify T ((env, maxidx), U) = Type.unify tsig (env, maxidx) (U, T) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

323 
handle Type.TUNIFY => raise TYPE ("unify_parms: failed to unify types", [U, T], []); 
12502  324 
fun unify_list (envir, T :: Us) = foldl (unify T) (envir, Us) 
325 
 unify_list (envir, []) = envir; 

326 
val (unifier, _) = foldl unify_list 

327 
((Vartab.empty, maxidx), map #2 (Symtab.dest (Symtab.make_multi parms))); 

328 

329 
val parms' = map (apsnd (Envir.norm_type unifier)) (gen_distinct eq_fst parms); 

330 
val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms')); 

331 

332 
fun inst_parms (i, ps) = 

333 
foldr Term.add_typ_tfrees (mapfilter snd ps, []) 

334 
> mapfilter (fn (a, S) => 

335 
let val T = Envir.norm_type unifier' (TVar ((a, i), S)) 

336 
in if T = TFree (a, S) then None else Some ((a, S), T) end); 

337 
in map inst_parms idx_parmss end; 

338 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

339 
in 
12502  340 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

341 
fun unify_elemss _ _ [] = [] 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

342 
 unify_elemss _ [] [elems] = [elems] 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

343 
 unify_elemss ctxt fixed_parms elemss = 
12502  344 
let 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

345 
val envs = unify_parms ctxt fixed_parms (map (#2 o #1) elemss); 
12839  346 
fun inst (((name, ps), (elems, text)), env) = 
347 
((name, map (apsnd (apsome (inst_type env))) ps), 

348 
(map (inst_elem env) elems, inst_text env text)); 

349 
in map inst (elemss ~~ envs) end; 

12502  350 

12575  351 
fun flatten_expr ctxt (prev_idents, expr) = 
12014  352 
let 
353 
val thy = ProofContext.theory_of ctxt; 

12263  354 

12289  355 
fun renaming (Some x :: xs) (y :: ys) = (y, x) :: renaming xs ys 
356 
 renaming (None :: xs) (y :: ys) = renaming xs ys 

12273  357 
 renaming [] _ = [] 
12289  358 
 renaming xs [] = raise ERROR_MESSAGE ("Too many arguments in renaming: " ^ 
359 
commas (map (fn None => "_"  Some x => quote x) xs)); 

360 

361 
fun rename_parms ren (name, ps) = 

362 
let val ps' = map (rename ren) ps in 

363 
(case duplicates ps' of [] => (name, ps') 

364 
 dups => err_in_locale ctxt ("Duplicate parameters: " ^ commas_quote dups) [(name, ps')]) 

365 
end; 

12263  366 

12273  367 
fun identify ((ids, parms), Locale name) = 
12289  368 
let 
369 
val {import, params, ...} = the_locale thy name; 

370 
val ps = map #1 (#1 params); 

371 
in 

12273  372 
if (name, ps) mem ids then (ids, parms) 
12277  373 
else 
12289  374 
let val (ids', parms') = identify ((ids, parms), import); (*acyclic dependencies!*) 
375 
in (ids' @ [(name, ps)], merge_lists parms' ps) end 

12273  376 
end 
377 
 identify ((ids, parms), Rename (e, xs)) = 

378 
let 

379 
val (ids', parms') = identify (([], []), e); 

12839  380 
val ren = renaming xs parms' 
381 
handle ERROR_MESSAGE msg => err_in_locale ctxt msg ids'; 

12289  382 
val ids'' = distinct (map (rename_parms ren) ids'); 
383 
val parms'' = distinct (flat (map #2 ids'')); 

384 
in (merge_lists ids ids'', merge_lists parms parms'') end 

12273  385 
 identify (arg, Merge es) = foldl identify (arg, es); 
12014  386 

12307  387 
fun eval (name, xs) = 
12273  388 
let 
12839  389 
val {params = (ps, qs), elems, text, ...} = the_locale thy name; 
12307  390 
val ren = filter_out (op =) (map #1 ps ~~ xs); 
12839  391 
val (params', elems', text') = 
392 
if null ren then ((ps, qs), map #1 elems, text) 

12502  393 
else ((map (apfst (rename ren)) ps, map (rename ren) qs), 
12839  394 
map (rename_elem ren o #1) elems, rename_text ren text); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

395 
val elems'' = map (rename_facts [NameSpace.base name, space_implode "_" xs]) elems'; 
12839  396 
in ((name, params'), (elems'', text')) end; 
12307  397 

12575  398 
val idents = gen_rems (op =) (#1 (identify (([], []), expr)), prev_idents); 
399 
val raw_elemss = unique_parms ctxt (map eval idents); 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

400 
val elemss = unify_elemss ctxt [] raw_elemss; 
12575  401 
in (prev_idents @ idents, elemss) end; 
12046  402 

12510  403 
end; 
404 

12070  405 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

406 
(* activate elements *) 
12273  407 

12510  408 
local 
409 

12839  410 
fun activate_elem (ctxt, Fixes fixes) = 
411 
(ctxt > ProofContext.add_fixes fixes, []) 

12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

412 
 activate_elem (ctxt, Assumes asms) = 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

413 
ctxt > ProofContext.fix_frees (flat (map (map #1 o #2) asms)) 
12839  414 
> ProofContext.assume_i ProofContext.export_assume asms 
415 
> apsnd (map (pair Assume)) 

12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

416 
 activate_elem (ctxt, Defines defs) = 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

417 
ctxt > ProofContext.assume_i ProofContext.export_def 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

418 
(map (fn ((name, atts), (t, ps)) => 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

419 
let val (c, t') = ProofContext.cert_def ctxt t 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

420 
in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end) defs) 
12839  421 
> apsnd (map (pair Define)) 
422 
 activate_elem (ctxt, Notes facts) = 

423 
ctxt > ProofContext.have_thmss_i facts 

424 
> apsnd (map (pair Note)); 

12263  425 

12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

426 
fun activate_elems ((name, ps), elems) = ProofContext.qualified_result (fn ctxt => 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

427 
foldl_map activate_elem (ctxt, elems) handle ProofContext.CONTEXT (msg, ctxt) => 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

428 
err_in_locale ctxt msg [(name, map fst ps)]); 
12502  429 

12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

430 
fun activate_elemss prep_facts = foldl_map (fn (ctxt, ((name, ps), raw_elems)) => 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

431 
let 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

432 
val elems = map (prep_facts ctxt) raw_elems; 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

433 
val res = ((name, ps), elems); 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

434 
val (ctxt', facts) = apsnd flat (activate_elems res ctxt); 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

435 
in (ctxt', (res, facts)) end); 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

436 

12546  437 
in 
438 

12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

439 
fun activate_facts prep_facts ctxt_elemss = 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

440 
let val (ctxt', (elemss', factss)) = apsnd split_list (activate_elemss prep_facts ctxt_elemss) 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

441 
in (ctxt', (elemss', flat factss)) end; 
12546  442 

12958  443 
fun apply_facts name (ctxt, facts) = 
444 
let val (ctxt', (_, facts')) = activate_facts (K I) (ctxt, [((name, []), [Notes facts])]) 

445 
in (ctxt', map (#2 o #2) facts') end; 

446 

12510  447 
end; 
448 

12307  449 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

450 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

451 
(** prepare context elements **) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

452 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

453 
(* expressions *) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

454 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

455 
fun intern_expr sg (Locale xname) = Locale (intern sg xname) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

456 
 intern_expr sg (Merge exprs) = Merge (map (intern_expr sg) exprs) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

457 
 intern_expr sg (Rename (expr, xs)) = Rename (intern_expr sg expr, xs); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

458 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

459 

12546  460 
(* attributes *) 
461 

462 
local fun read_att attrib (x, srcs) = (x, map attrib srcs) in 

463 

464 
fun attribute _ (Elem (Fixes fixes)) = Elem (Fixes fixes) 

465 
 attribute attrib (Elem (Assumes asms)) = Elem (Assumes (map (apfst (read_att attrib)) asms)) 

466 
 attribute attrib (Elem (Defines defs)) = Elem (Defines (map (apfst (read_att attrib)) defs)) 

467 
 attribute attrib (Elem (Notes facts)) = 

468 
Elem (Notes (map (apfst (read_att attrib) o apsnd (map (read_att attrib))) facts)) 

469 
 attribute _ (Expr expr) = Expr expr; 

470 

471 
end; 

472 

473 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

474 
(* parameters *) 
12502  475 

476 
local 

477 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

478 
fun prep_fixes prep_vars ctxt fixes = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

479 
let val vars = snd (foldl_map prep_vars (ctxt, map (fn (x, T, _) => ([x], T)) fixes)) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

480 
in map (fn (([x'], T'), (_, _, mx)) => (x', T', mx)) (vars ~~ fixes) end; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

481 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

482 
in 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

483 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

484 
fun read_fixes x = prep_fixes ProofContext.read_vars x; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

485 
fun cert_fixes x = prep_fixes ProofContext.cert_vars x; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

486 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

487 
end; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

488 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

489 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

490 
(* propositions and bindings *) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

491 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

492 
datatype ('a, 'b) int_ext = Int of 'a  Ext of 'b; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

493 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

494 
local 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

495 

12839  496 
local 
497 

12727  498 
fun declare_int_elem (ctxt, Fixes fixes) = 
12575  499 
(ctxt > ProofContext.add_fixes (map (fn (x, T, mx) => 
12727  500 
(x, apsome (Term.map_type_tfree (Type.param 0)) T, mx)) fixes), []) 
501 
 declare_int_elem (ctxt, _) = (ctxt, []); 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

502 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

503 
fun declare_ext_elem prep_fixes (ctxt, Fixes fixes) = 
12575  504 
(ctxt > ProofContext.add_fixes (prep_fixes ctxt fixes), []) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

505 
 declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

506 
 declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

507 
 declare_ext_elem _ (ctxt, Notes facts) = (ctxt, []); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

508 

12727  509 
fun declare_elems prep_fixes (ctxt, ((name, ps), elems)) = 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

510 
let val (ctxt', propps) = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

511 
(case elems of 
12839  512 
Int (es, _) => foldl_map declare_int_elem (ctxt, es) 
12546  513 
 Ext e => foldl_map (declare_ext_elem prep_fixes) (ctxt, [e])) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

514 
handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)] 
12727  515 
in (ctxt', propps) end; 
516 

12839  517 
in 
518 

12727  519 
fun declare_elemss prep_fixes fixed_params raw_elemss ctxt = 
520 
let 

521 
val int_elemss = 

522 
raw_elemss 

523 
> mapfilter (fn (id, Int es) => Some (id, es)  _ => None) 

524 
> unify_elemss ctxt fixed_params; 

525 
val (_, raw_elemss') = 

526 
foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es))  x => x) 

527 
(int_elemss, raw_elemss); 

528 
in foldl_map (declare_elems prep_fixes) (ctxt, raw_elemss') end; 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

529 

12839  530 
end; 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

531 

12839  532 
val empty_text = (([], []), ([], [])); 
533 

534 
fun merge_text (((xs1, spec1), (ys1, env1)), ((xs2, spec2), (ys2, env2))) = 

535 
((gen_merge_lists eq_fst xs1 xs2, spec1 @ spec2), (ys1 @ ys2, env1 @ env2)); 

536 

537 
local 

538 

539 
val norm_term = Envir.beta_norm oo Term.subst_atomic; 

540 

541 
fun abstract_def eq = (*assumes wellformedness according to ProofContext.cert_def*) 

542 
let 

543 
val body = Term.strip_all_body eq; 

544 
val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq)); 

545 
val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (vars, body)); 

546 
val (f, xs) = Term.strip_comb lhs; 

547 
in (Term.dest_Free f, Term.list_abs_free (map Term.dest_Free xs, rhs)) end; 

12502  548 

12839  549 
fun bind_def ctxt (name, ps) ((all_text, text), eq) = 
550 
let 

551 
val ((all_xs, _), (all_ys, all_env)) = all_text; 

552 
val (y, b) = abstract_def eq; 

553 
val b' = norm_term all_env b; 

554 
val txt = ((Term.add_frees ([], b'), []), ([y], [(Free y, b')])); 

555 
fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote (#1 y)) [(name, map fst ps)]; 

556 
in 

557 
conditional (y mem all_xs) (fn () => err "Attempt to define previously specified variable"); 

558 
conditional (y mem all_ys) (fn () => err "Attempt to redefine variable"); 

559 
(merge_text (all_text, txt), merge_text (text, txt)) 

560 
end; 

12575  561 

12839  562 
fun eval_text _ _ (all_text, Fixes _) = (all_text, empty_text) 
563 
 eval_text _ _ (all_text, Assumes asms) = 

564 
let 

565 
val ts = map (norm_term (#2 (#2 all_text))) (flat (map (map #1 o #2) asms)); 

566 
val txt = ((foldl Term.add_frees ([], ts), ts), ([], [])); 

567 
in (merge_text (all_text, txt), txt) end 

568 
 eval_text ctxt id (all_text, Defines defs) = 

569 
foldl (bind_def ctxt id) ((all_text, empty_text), map (#1 o #2) defs) 

570 
 eval_text _ _ (all_text, Notes _) = (all_text, empty_text); 

571 

12502  572 

12839  573 
fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) => 
12727  574 
(x, assoc_string (parms, x), mx)) fixes) 
12839  575 
 finish_ext_elem _ close (Assumes asms, propp) = 
576 
close (Assumes (map #1 asms ~~ propp)) 

577 
 finish_ext_elem _ close (Defines defs, propp) = 

12727  578 
close (Defines (map #1 defs ~~ map (fn [(t, (ps, []))] => (t, ps)) propp)) 
12839  579 
 finish_ext_elem _ _ (Notes facts, _) = Notes facts; 
580 

581 
fun finish_parms parms ((name, ps), elems) = 

582 
((name, map (fn (x, _) => (x, assoc (parms, x))) ps), elems); 

583 

584 
fun finish_elems ctxt parms _ ((all_text, int_text, ext_text), ((id, Int e), _)) = 

585 
let val [(_, (es, txt))] = unify_elemss ctxt parms [(id, e)] 

586 
in ((merge_text (all_text, txt), merge_text (int_text, txt), ext_text), (id, map Int es)) end 

587 
 finish_elems ctxt parms close ((all_text, int_text, ext_text), ((id, Ext e), [propp])) = 

588 
let 

589 
val e' = finish_ext_elem parms close (e, propp); 

590 
val (all_text', txt) = eval_text ctxt id (all_text, e'); 

591 
in ((all_text', int_text, merge_text (ext_text, txt)), (id, [Ext e'])) end; 

592 

593 
in 

12510  594 

12839  595 
fun finish_elemss ctxt parms close = 
596 
foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms close); 

597 

598 
end; 

599 

600 
fun closeup ctxt elem = 

12502  601 
let 
12839  602 
fun close_frees t = 
603 
let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1) (Term.add_frees ([], t))) 

604 
in Term.list_all_free (frees, t) end; 

12510  605 

12839  606 
fun no_binds ps = 
607 
if null ps then ps 

608 
else raise ProofContext.CONTEXT ("Illegal term bindings in locale element", ctxt); 

609 
in 

610 
(case elem of 

611 
Assumes asms => Assumes (asms > map (fn (a, propps) => 

612 
(a, map (fn (t, (ps, qs)) => (close_frees t, (no_binds ps, no_binds qs))) propps))) 

613 
 Defines defs => Defines (defs > map (fn (a, (t, ps)) => 

614 
(a, (close_frees (#2 (ProofContext.cert_def ctxt t)), no_binds ps)))) 

615 
 e => e) 

616 
end; 

12277  617 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

618 
fun prep_elemss prep_fixes prepp do_close context fixed_params raw_elemss raw_concl = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

619 
let 
12727  620 
val (raw_ctxt, raw_proppss) = declare_elemss prep_fixes fixed_params raw_elemss context; 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

621 
val raw_propps = map flat raw_proppss; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

622 
val raw_propp = flat raw_propps; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

623 
val (ctxt, all_propp) = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

624 
prepp (ProofContext.declare_terms (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

625 
val ctxt = ProofContext.declare_terms (flat (map (map fst) all_propp)) ctxt; 
12502  626 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

627 
val all_propp' = map2 (op ~~) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

628 
(#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp))), map (map snd) all_propp); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

629 
val n = length raw_concl; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

630 
val concl = take (n, all_propp'); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

631 
val propp = drop (n, all_propp'); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

632 
val propps = unflat raw_propps propp; 
12839  633 
val proppss = map (uncurry unflat) (raw_proppss ~~ propps); 
12502  634 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

635 
val xs = map #1 (params_of raw_elemss); 
12727  636 
val typing = unify_frozen ctxt 0 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

637 
(map (ProofContext.default_type raw_ctxt) xs) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

638 
(map (ProofContext.default_type ctxt) xs); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

639 
val parms = param_types (xs ~~ typing); 
12273  640 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

641 
val close = if do_close then closeup ctxt else I; 
12839  642 
val ((_, int_text, ext_text), elemss) = finish_elemss ctxt parms close 
643 
((empty_text, empty_text, empty_text), raw_elemss ~~ proppss); 

644 
in (parms, elemss, (merge_text (int_text, ext_text), ext_text), concl) end; 

12502  645 

646 
in 

647 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

648 
fun read_elemss x = prep_elemss read_fixes ProofContext.read_propp_schematic x; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

649 
fun cert_elemss x = prep_elemss cert_fixes ProofContext.cert_propp_schematic x; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

650 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

651 
end; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

652 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

653 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

654 
(* facts *) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

655 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

656 
local 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

657 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

658 
fun prep_name ctxt (name, atts) = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

659 
if NameSpace.is_qualified name then 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

660 
raise ProofContext.CONTEXT ("Illegal qualified name: " ^ quote name, ctxt) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

661 
else (name, atts); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

662 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

663 
fun prep_facts _ _ (Int elem) = elem 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

664 
 prep_facts _ _ (Ext (Fixes fixes)) = Fixes fixes 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

665 
 prep_facts _ ctxt (Ext (Assumes asms)) = Assumes (map (apfst (prep_name ctxt)) asms) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

666 
 prep_facts _ ctxt (Ext (Defines defs)) = Defines (map (apfst (prep_name ctxt)) defs) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

667 
 prep_facts get ctxt (Ext (Notes facts)) = Notes (facts > map (fn (a, bs) => 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

668 
(prep_name ctxt a, map (apfst (get ctxt)) bs))); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

669 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

670 
in 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

671 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

672 
fun get_facts x = prep_facts ProofContext.get_thms x; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

673 
fun get_facts_i x = prep_facts (K I) x; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

674 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

675 
end; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

676 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

677 

12546  678 
(* full context statements: import + elements + conclusion *) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

679 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

680 
local 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

681 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

682 
fun prep_context_statement prep_expr prep_elemss prep_facts 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

683 
close fixed_params import elements raw_concl context = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

684 
let 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

685 
val sign = ProofContext.sign_of context; 
12575  686 
fun flatten (ids, Elem (Fixes fixes)) = 
687 
(ids, [(("", map (rpair None o #1) fixes), Ext (Fixes fixes))]) 

688 
 flatten (ids, Elem elem) = (ids, [(("", []), Ext elem)]) 

689 
 flatten (ids, Expr expr) = 

690 
let val (ids', elemss) = flatten_expr context (ids, prep_expr sign expr) 

691 
in (ids', map (apsnd Int) elemss) end 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

692 

12575  693 
val (import_ids, raw_import_elemss) = flatten ([], Expr import); 
694 
val raw_elemss = flat (#2 ((foldl_map flatten (import_ids, elements)))); 

12839  695 
val (parms, all_elemss, texts, concl) = 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

696 
prep_elemss close context fixed_params (raw_import_elemss @ raw_elemss) raw_concl; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

697 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

698 
val n = length raw_import_elemss; 
12839  699 
val (import_ctxt, (import_elemss, import_facts)) = 
700 
activate_facts prep_facts (context, take (n, all_elemss)); 

701 
val (ctxt, (elemss, facts)) = 

702 
activate_facts prep_facts (import_ctxt, drop (n, all_elemss)); 

12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

703 
in 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

704 
((((import_ctxt, (import_elemss, import_facts)), 
12839  705 
(ctxt, (elemss, facts))), texts), concl) 
12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

706 
end; 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

707 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

708 
val gen_context = prep_context_statement intern_expr read_elemss get_facts; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

709 
val gen_context_i = prep_context_statement (K I) cert_elemss get_facts_i; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

710 

12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

711 
fun gen_facts prep_locale thy name = 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

712 
let val ((((_, (_, facts)), _), _), _) = thy > ProofContext.init 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

713 
> gen_context_i false [] (Locale (prep_locale (Theory.sign_of thy) name)) [] []; 
12839  714 
in flat (map (#2 o #2) facts) end; 
12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

715 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

716 
fun gen_statement prep_locale prep_ctxt raw_locale elems concl ctxt = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

717 
let 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

718 
val thy = ProofContext.theory_of ctxt; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

719 
val locale = apsome (prep_locale (Theory.sign_of thy)) raw_locale; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

720 
val (fixed_params, import) = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

721 
(case locale of None => ([], empty) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

722 
 Some name => (param_types (#1 (#params (the_locale thy name))), Locale name)); 
12730  723 
val ((((locale_ctxt, _), (elems_ctxt, _)), _), concl') = 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

724 
prep_ctxt false fixed_params import elems concl ctxt; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

725 
in (locale, locale_ctxt, elems_ctxt, concl') end; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

726 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

727 
in 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

728 

d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

729 
fun read_context x y z = #1 (gen_context true [] x y [] z); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

730 
fun cert_context x y z = #1 (gen_context_i true [] x y [] z); 
12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

731 
val locale_facts = gen_facts intern; 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

732 
val locale_facts_i = gen_facts (K I); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

733 
val read_context_statement = gen_statement intern gen_context; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

734 
val cert_context_statement = gen_statement (K I) gen_context_i; 
12502  735 

736 
end; 

11896  737 

738 

739 

12070  740 
(** print locale **) 
741 

12758  742 
fun print_locale thy import body = 
12070  743 
let 
744 
val sg = Theory.sign_of thy; 

12289  745 
val thy_ctxt = ProofContext.init thy; 
12839  746 
val (((_, (import_elemss, _)), (ctxt, (elemss, _))), (((pred_xs, pred_ts), _), _)) = 
12758  747 
read_context import body thy_ctxt; 
748 
val all_elems = flat (map #2 (import_elemss @ elemss)); 

12070  749 

12307  750 
val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt; 
751 
val prt_term = Pretty.quote o ProofContext.pretty_term ctxt; 

752 
val prt_thm = Pretty.quote o ProofContext.pretty_thm ctxt; 

12070  753 

754 
fun prt_syn syn = 

755 
let val s = (case syn of None => "(structure)"  Some mx => Syntax.string_of_mixfix mx) 

12575  756 
in if s = "" then [] else [Pretty.brk 2, Pretty.str s] end; 
12070  757 
fun prt_fix (x, Some T, syn) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 :: 
758 
prt_typ T :: Pretty.brk 1 :: prt_syn syn) 

759 
 prt_fix (x, None, syn) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_syn syn); 

760 

12307  761 
fun prt_name "" = [Pretty.brk 1] 
762 
 prt_name name = [Pretty.str (ProofContext.cond_extern ctxt name ^ ":"), Pretty.brk 1]; 

763 
fun prt_asm ((a, _), ts) = Pretty.block (prt_name a @ Pretty.breaks (map (prt_term o fst) ts)); 

764 
fun prt_def ((a, _), (t, _)) = Pretty.block (prt_name a @ [prt_term t]); 

765 
fun prt_fact ((a, _), ths) = Pretty.block 

766 
(prt_name a @ Pretty.breaks (map prt_thm (flat (map fst ths)))); 

12070  767 

12289  768 
fun items _ [] = [] 
769 
 items prfx (x :: xs) = Pretty.block [Pretty.str prfx, Pretty.brk 1, x] :: items " and" xs; 

770 
fun prt_elem (Fixes fixes) = items "fixes" (map prt_fix fixes) 

771 
 prt_elem (Assumes asms) = items "assumes" (map prt_asm asms) 

772 
 prt_elem (Defines defs) = items "defines" (map prt_def defs) 

773 
 prt_elem (Notes facts) = items "notes" (map prt_fact facts); 

12730  774 

775 
val prt_pred = 

776 
if null pred_ts then Pretty.str "" 

777 
else 

778 
Library.foldr1 Logic.mk_conjunction pred_ts 

12806
1f54c65fca5d
ObjectLogic.atomize_term replaces ObjectLogic.atomize_cterm;
wenzelm
parents:
12758
diff
changeset

779 
> ObjectLogic.atomize_term sg 
12730  780 
> curry Term.list_abs_free pred_xs 
781 
> prt_term; 

12277  782 
in 
12758  783 
[Pretty.big_list "context elements:" (map (Pretty.chunks o prt_elem) all_elems), 
12730  784 
Pretty.big_list "predicate text:" [prt_pred]] > Pretty.chunks > Pretty.writeln 
12277  785 
end; 
12070  786 

787 

788 

11896  789 
(** define locales **) 
790 

12063  791 
(* add_locale(_i) *) 
11896  792 

12502  793 
local 
794 

12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

795 
fun gen_add_locale prep_ctxt prep_expr bname raw_import raw_body thy = 
12063  796 
let 
797 
val sign = Theory.sign_of thy; 

11896  798 
val name = Sign.full_name sign bname; 
12502  799 
val _ = conditional (is_some (get_locale thy name)) (fn () => 
800 
error ("Duplicate definition of locale " ^ quote name)); 

11896  801 

12273  802 
val thy_ctxt = ProofContext.init thy; 
12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

803 
val (((import_ctxt, (import_elemss, _)), (body_ctxt, (body_elemss, _))), 
12839  804 
(int_ext_text, ext_text)) = prep_ctxt raw_import raw_body thy_ctxt; 
805 

806 
val import_parms = params_of import_elemss; 

807 
val body_parms = params_of body_elemss; 

808 
val all_parms = import_parms @ body_parms; 

809 

810 
(* FIXME *) 

811 
val ((_, spec), defs) = int_ext_text; 

812 
val ((xs, _), _) = int_ext_text; 

813 
val xs' = all_parms > mapfilter (fn (p, _) => 

814 
(case assoc_string (xs, p) of None => None  Some T => Some (p, T))); 

815 

12730  816 
val import = prep_expr sign raw_import; 
12510  817 
val elems = flat (map snd body_elemss); 
12063  818 
in 
819 
thy 

820 
> declare_locale name 

12289  821 
> put_locale name (make_locale import (map (fn e => (e, stamp ())) elems) 
12839  822 
((xs', spec), defs) (all_parms, map fst body_parms)) 
12063  823 
end; 
824 

12502  825 
in 
826 

12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

827 
val add_locale = gen_add_locale read_context intern_expr; 
12502  828 
val add_locale_i = gen_add_locale cert_context (K I); 
829 

830 
end; 

12063  831 

11896  832 

12730  833 
(* store results *) 
11896  834 

12706  835 
local 
836 

12702  837 
fun hide_bound_names names thy = 
838 
thy > PureThy.hide_thms false 

839 
(map (Sign.full_name (Theory.sign_of thy)) (filter_out (equal "") names)); 

840 

12958  841 
in 
842 

12706  843 
fun have_thmss_qualified kind loc args thy = 
844 
thy 

845 
> Theory.add_path (Sign.base_name loc) 

12711  846 
> PureThy.have_thmss_i (Drule.kind kind) args 
12706  847 
>> hide_bound_names (map (#1 o #1) args) 
848 
>> Theory.parent_path; 

849 

12958  850 
fun smart_have_thmss kind None = PureThy.have_thmss_i (Drule.kind kind) 
851 
 smart_have_thmss kind (Some (loc, _)) = have_thmss_qualified kind loc; 

852 

853 
end; 

854 

855 
local 

856 

857 
fun put_facts loc args thy = 

858 
let 

859 
val {import, elems, text, params} = the_locale thy loc; 

860 
val note = Notes (map (fn ((a, more_atts), th_atts) => 

861 
((a, more_atts), map (apfst (map (curry Thm.name_thm a))) th_atts)) args); 

862 
in thy > put_locale loc (make_locale import (elems @ [(note, stamp ())]) text params) end; 

863 

12706  864 
fun gen_have_thmss prep_locale get_thms kind raw_loc raw_args thy = 
865 
let 

866 
val thy_ctxt = ProofContext.init thy; 

867 
val loc = prep_locale (Theory.sign_of thy) raw_loc; 

12730  868 
val loc_ctxt = #1 (#1 (#1 (cert_context (Locale loc) [] thy_ctxt))); 
12706  869 
val args = map (apsnd (map (apfst (get_thms loc_ctxt)))) raw_args; 
870 
val export = Drule.local_standard o ProofContext.export_single loc_ctxt thy_ctxt; 

12711  871 
val results = map (map export o #2) (#2 (ProofContext.have_thmss_i args loc_ctxt)); 
12706  872 
val args' = map (rpair [] o #1 o #1) args ~~ map (single o Thm.no_attributes) results; 
873 
in 

874 
thy 

875 
> put_facts loc args 

876 
> have_thmss_qualified kind loc args' 

877 
end; 

878 

879 
in 

880 

12711  881 
val have_thmss = gen_have_thmss intern ProofContext.get_thms; 
882 
val have_thmss_i = gen_have_thmss (K I) (K I); 

883 

12958  884 
fun add_thmss loc args (ctxt, thy) = 
885 
let 

886 
val args' = map (fn ((a, ths), atts) => ((a, atts), [(ths, [])])) args; 

887 
val (ctxt', facts') = apply_facts loc (ctxt, args'); 

888 
in ((ctxt', thy > put_facts loc args'), facts') end; 

12702  889 

12706  890 
end; 
12063  891 

11896  892 

12730  893 

11896  894 
(** locale theory setup **) 
12063  895 

11896  896 
val setup = 
897 
[LocalesData.init]; 

898 

899 
end; 