author  wenzelm 
Thu, 13 Jun 2002 17:22:10 +0200  
changeset 13211  aabdb4b33625 
parent 12958  99f5c4a37b29 
child 13297  e4ae0732e2be 
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 

13211
aabdb4b33625
BUG FIX in inst_thm: use current context instead of that of thm!!!
wenzelm
parents:
12958
diff
changeset

231 
fun inst_thm _ [] th = th 
aabdb4b33625
BUG FIX in inst_thm: use current context instead of that of thm!!!
wenzelm
parents:
12958
diff
changeset

232 
 inst_thm ctxt env th = 
12502  233 
let 
13211
aabdb4b33625
BUG FIX in inst_thm: use current context instead of that of thm!!!
wenzelm
parents:
12958
diff
changeset

234 
val sign = ProofContext.sign_of ctxt; 
12575  235 
val cert = Thm.cterm_of sign; 
236 
val certT = Thm.ctyp_of sign; 

13211
aabdb4b33625
BUG FIX in inst_thm: use current context instead of that of thm!!!
wenzelm
parents:
12958
diff
changeset

237 
val {hyps, prop, maxidx, ...} = Thm.rep_thm th; 
12579  238 
val tfrees = foldr Term.add_term_tfree_names (prop :: hyps, []); 
239 
val env' = filter (fn ((a, _), _) => a mem_string tfrees) env; 

12502  240 
in 
241 
if null env' then th 

242 
else 

243 
th 

244 
> Drule.implies_intr_list (map cert hyps) 

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

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

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

250 
end; 

251 

13211
aabdb4b33625
BUG FIX in inst_thm: use current context instead of that of thm!!!
wenzelm
parents:
12958
diff
changeset

252 
fun inst_elem _ env (Fixes fixes) = 
12502  253 
Fixes (map (fn (x, T, mx) => (x, apsome (inst_type env) T, mx)) fixes) 
13211
aabdb4b33625
BUG FIX in inst_thm: use current context instead of that of thm!!!
wenzelm
parents:
12958
diff
changeset

254 
 inst_elem _ env (Assumes asms) = Assumes (map (apsnd (map (fn (t, (ps, qs)) => 
12502  255 
(inst_term env t, (map (inst_term env) ps, map (inst_term env) qs))))) asms) 
13211
aabdb4b33625
BUG FIX in inst_thm: use current context instead of that of thm!!!
wenzelm
parents:
12958
diff
changeset

256 
 inst_elem _ env (Defines defs) = Defines (map (apsnd (fn (t, ps) => 
12502  257 
(inst_term env t, map (inst_term env) ps))) defs) 
13211
aabdb4b33625
BUG FIX in inst_thm: use current context instead of that of thm!!!
wenzelm
parents:
12958
diff
changeset

258 
 inst_elem ctxt env (Notes facts) = 
aabdb4b33625
BUG FIX in inst_thm: use current context instead of that of thm!!!
wenzelm
parents:
12958
diff
changeset

259 
Notes (map (apsnd (map (apfst (map (inst_thm ctxt env))))) facts); 
12502  260 

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

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

264 

12502  265 

12529
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 
(** structured contexts: rename + merge + implicit type instantiation **) 
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 
(* parameter types *) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

270 

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

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

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

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

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

275 
(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

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

277 

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

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

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

280 
val tsig = Sign.tsig_of (ProofContext.sign_of ctxt); 
12546  281 
fun unify (env, (Some T, Some U)) = (Type.unify tsig env (U, T) 
282 
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

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

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

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

286 

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

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

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

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

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

293 

12730  294 
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

295 
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

296 

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

297 

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

298 
(* flatten expressions *) 
11896  299 

12510  300 
local 
12502  301 

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

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

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

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

305 
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

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

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

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

309 
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

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

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

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

313 

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

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

317 
val maxidx = length raw_parmss; 

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

319 

320 
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

321 
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

322 
val parms = fixed_parms @ flat (map varify_parms idx_parmss); 
12502  323 

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

324 
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

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

328 
val (unifier, _) = foldl unify_list 

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

330 

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

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

333 

334 
fun inst_parms (i, ps) = 

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

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

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

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

339 
in map inst_parms idx_parmss end; 

340 

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

341 
in 
12502  342 

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

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

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

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

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

13211
aabdb4b33625
BUG FIX in inst_thm: use current context instead of that of thm!!!
wenzelm
parents:
12958
diff
changeset

350 
(map (inst_elem ctxt env) elems, inst_text env text)); 
12839  351 
in map inst (elemss ~~ envs) end; 
12502  352 

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

12263  356 

12289  357 
fun renaming (Some x :: xs) (y :: ys) = (y, x) :: renaming xs ys 
358 
 renaming (None :: xs) (y :: ys) = renaming xs ys 

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

362 

363 
fun rename_parms ren (name, ps) = 

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

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

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

367 
end; 

12263  368 

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

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

373 
in 

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

12273  378 
end 
379 
 identify ((ids, parms), Rename (e, xs)) = 

380 
let 

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

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

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

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

12273  387 
 identify (arg, Merge es) = foldl identify (arg, es); 
12014  388 

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

12502  395 
else ((map (apfst (rename ren)) ps, map (rename ren) qs), 
12839  396 
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

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

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

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

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

12510  405 
end; 
406 

12070  407 

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

408 
(* activate elements *) 
12273  409 

12510  410 
local 
411 

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

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

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

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

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

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

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

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

421 
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

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

425 
ctxt > ProofContext.have_thmss_i facts 

426 
> apsnd (map (pair Note)); 

12263  427 

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

428 
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

429 
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

430 
err_in_locale ctxt msg [(name, map fst ps)]); 
12502  431 

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

432 
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

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

434 
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

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

436 
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

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

438 

12546  439 
in 
440 

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

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

442 
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

443 
in (ctxt', (elemss', flat factss)) end; 
12546  444 

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

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

448 

12510  449 
end; 
450 

12307  451 

12529
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 
(** prepare context elements **) 
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 
(* expressions *) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

456 

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

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

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

459 
 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

460 

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

461 

12546  462 
(* attributes *) 
463 

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

465 

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

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

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

469 
 attribute attrib (Elem (Notes facts)) = 

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

471 
 attribute _ (Expr expr) = Expr expr; 

472 

473 
end; 

474 

475 

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

476 
(* parameters *) 
12502  477 

478 
local 

479 

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

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

481 
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

482 
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

483 

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

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

485 

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

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

487 
fun cert_fixes x = prep_fixes ProofContext.cert_vars x; 
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 
end; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

490 

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 
(* propositions and bindings *) 
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 
datatype ('a, 'b) int_ext = Int of 'a  Ext of 'b; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

495 

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

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

497 

12839  498 
local 
499 

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

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

504 

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

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

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

508 
 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

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

510 

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

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

513 
(case elems of 
12839  514 
Int (es, _) => foldl_map declare_int_elem (ctxt, es) 
12546  515 
 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

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

12839  519 
in 
520 

12727  521 
fun declare_elemss prep_fixes fixed_params raw_elemss ctxt = 
522 
let 

523 
val int_elemss = 

524 
raw_elemss 

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

526 
> unify_elemss ctxt fixed_params; 

527 
val (_, raw_elemss') = 

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

529 
(int_elemss, raw_elemss); 

530 
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

531 

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

533 

12839  534 
val empty_text = (([], []), ([], [])); 
535 

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

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

538 

539 
local 

540 

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

542 

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

544 
let 

545 
val body = Term.strip_all_body eq; 

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

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

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

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

12502  550 

12839  551 
fun bind_def ctxt (name, ps) ((all_text, text), eq) = 
552 
let 

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

554 
val (y, b) = abstract_def eq; 

555 
val b' = norm_term all_env b; 

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

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

558 
in 

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

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

561 
(merge_text (all_text, txt), merge_text (text, txt)) 

562 
end; 

12575  563 

12839  564 
fun eval_text _ _ (all_text, Fixes _) = (all_text, empty_text) 
565 
 eval_text _ _ (all_text, Assumes asms) = 

566 
let 

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

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

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

570 
 eval_text ctxt id (all_text, Defines defs) = 

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

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

573 

12502  574 

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

579 
 finish_ext_elem _ close (Defines defs, propp) = 

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

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

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

585 

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

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

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

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

590 
let 

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

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

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

594 

595 
in 

12510  596 

12839  597 
fun finish_elemss ctxt parms close = 
598 
foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms close); 

599 

600 
end; 

601 

602 
fun closeup ctxt elem = 

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

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

12510  607 

12839  608 
fun no_binds ps = 
609 
if null ps then ps 

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

611 
in 

612 
(case elem of 

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

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

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

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

617 
 e => e) 

618 
end; 

12277  619 

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

620 
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

621 
let 
12727  622 
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

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

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

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

626 
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

627 
val ctxt = ProofContext.declare_terms (flat (map (map fst) all_propp)) ctxt; 
12502  628 

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

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

630 
(#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

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

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

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

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

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

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

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

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

641 
val parms = param_types (xs ~~ typing); 
12273  642 

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

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

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

12502  647 

648 
in 

649 

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

650 
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

651 
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

652 

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

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

654 

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 
(* facts *) 
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 
local 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

659 

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

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

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

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

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

664 

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

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

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

667 
 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

668 
 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

669 
 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

670 
(prep_name ctxt a, map (apfst (get ctxt)) bs))); 
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 
in 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

673 

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

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

675 
fun get_facts_i x = prep_facts (K I) x; 
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 
end; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

678 

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

679 

12546  680 
(* full context statements: import + elements + conclusion *) 
12529
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 
local 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

683 

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

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

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

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

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

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

691 
 flatten (ids, Expr expr) = 

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

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

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

694 

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

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

698 
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

699 

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

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

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

704 
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

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

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

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

709 

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

710 
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

711 
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

712 

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

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

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

715 
> gen_context_i false [] (Locale (prep_locale (Theory.sign_of thy) name)) [] []; 
12839  716 
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

717 

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

718 
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

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

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

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

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

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

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

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

727 
in (locale, locale_ctxt, elems_ctxt, concl') end; 
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 
in 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

730 

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

731 
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

732 
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

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

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

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

736 
val cert_context_statement = gen_statement (K I) gen_context_i; 
12502  737 

738 
end; 

11896  739 

740 

741 

12070  742 
(** print locale **) 
743 

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

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

12070  751 

12307  752 
val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt; 
753 
val prt_term = Pretty.quote o ProofContext.pretty_term ctxt; 

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

12070  755 

756 
fun prt_syn syn = 

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

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

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

762 

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

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

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

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

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

12070  769 

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

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

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

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

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

12730  776 

777 
val prt_pred = 

778 
if null pred_ts then Pretty.str "" 

779 
else 

780 
Library.foldr1 Logic.mk_conjunction pred_ts 

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

781 
> ObjectLogic.atomize_term sg 
12730  782 
> curry Term.list_abs_free pred_xs 
783 
> prt_term; 

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

789 

790 

11896  791 
(** define locales **) 
792 

12063  793 
(* add_locale(_i) *) 
11896  794 

12502  795 
local 
796 

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

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

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

11896  803 

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

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

808 
val import_parms = params_of import_elemss; 

809 
val body_parms = params_of body_elemss; 

810 
val all_parms = import_parms @ body_parms; 

811 

812 
(* FIXME *) 

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

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

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

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

817 

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

822 
> declare_locale name 

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

12502  827 
in 
828 

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

829 
val add_locale = gen_add_locale read_context intern_expr; 
12502  830 
val add_locale_i = gen_add_locale cert_context (K I); 
831 

832 
end; 

12063  833 

11896  834 

12730  835 
(* store results *) 
11896  836 

12706  837 
local 
838 

12702  839 
fun hide_bound_names names thy = 
840 
thy > PureThy.hide_thms false 

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

842 

12958  843 
in 
844 

12706  845 
fun have_thmss_qualified kind loc args thy = 
846 
thy 

847 
> Theory.add_path (Sign.base_name loc) 

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

851 

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

854 

855 
end; 

856 

857 
local 

858 

859 
fun put_facts loc args thy = 

860 
let 

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

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

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

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

865 

12706  866 
fun gen_have_thmss prep_locale get_thms kind raw_loc raw_args thy = 
867 
let 

868 
val thy_ctxt = ProofContext.init thy; 

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

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

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

876 
thy 

877 
> put_facts loc args 

878 
> have_thmss_qualified kind loc args' 

879 
end; 

880 

881 
in 

882 

12711  883 
val have_thmss = gen_have_thmss intern ProofContext.get_thms; 
884 
val have_thmss_i = gen_have_thmss (K I) (K I); 

885 

12958  886 
fun add_thmss loc args (ctxt, thy) = 
887 
let 

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

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

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

12702  891 

12706  892 
end; 
12063  893 

11896  894 

12730  895 

11896  896 
(** locale theory setup **) 
12063  897 

11896  898 
val setup = 
899 
[LocalesData.init]; 

900 

901 
end; 

13211
aabdb4b33625
BUG FIX in inst_thm: use current context instead of that of thm!!!
wenzelm
parents:
12958
diff
changeset

902 