author  paulson 
Tue, 26 Apr 2005 17:44:24 +0200  
changeset 15842  30a4267c6301 
parent 15839  12b06f56209a 
child 16028  a2c790d145ba 
permissions  rwrr 
12014  1 
(* Title: Pure/Isar/locale.ML 
11896  2 
ID: $Id$ 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

3 
Author: Clemens Ballarin, TU Muenchen; Markus Wenzel, LMU/TU Muenchen 
11896  4 

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

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

7 

14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

8 
Draws some basic ideas from Florian Kammueller's original version of 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

9 
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

10 
metalogic. Furthermore, we provide structured import of contexts 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

11 
(with merge and rename operations), as well as typeinference of the 
13375  12 
signature parts, and predicate definitions of the specification text. 
14446  13 

14 
See also: 

15 

16 
[1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar. 

17 
In Stefano Berardi et al., Types for Proofs and Programs: International 

15099  18 
Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 3450, 2004. 
11896  19 
*) 
20 

21 
signature LOCALE = 

22 
sig 

12046  23 
type context 
15703  24 
datatype ('typ, 'term, 'fact) elem = 
12058  25 
Fixes of (string * 'typ option * mixfix option) list  
15703  26 
Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list  
27 
Defines of ((string * Attrib.src list) * ('term * 'term list)) list  

28 
Notes of ((string * Attrib.src list) * ('fact * Attrib.src list) list) list 

12273  29 
datatype expr = 
30 
Locale of string  

31 
Rename of expr * string option list  

32 
Merge of expr list 

33 
val empty: expr 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

34 
datatype 'a elem_expr = Elem of 'a  Expr of expr 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

35 

09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

36 
(* Abstract interface to locales *) 
15703  37 
type element 
38 
type element_i 

12046  39 
type locale 
40 
val intern: Sign.sg > xstring > string 

12014  41 
val cond_extern: Sign.sg > string > xstring 
12502  42 
val the_locale: theory > string > locale 
15703  43 
val intern_attrib_elem: theory > 
44 
('typ, 'term, 'fact) elem > ('typ, 'term, 'fact) elem 

45 
val intern_attrib_elem_expr: theory > 

46 
('typ, 'term, 'fact) elem elem_expr > ('typ, 'term, 'fact) elem elem_expr 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

47 

15596  48 
(* Processing of locale statements *) 
15703  49 
val read_context_statement: xstring option > element elem_expr list > 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

50 
(string * (string list * string list)) list list > context > 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

51 
string option * (cterm list * cterm list) * context * context * 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

52 
(term * (term list * term list)) list list 
15703  53 
val cert_context_statement: string option > element_i elem_expr list > 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

54 
(term * (term list * term list)) list list > context > 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

55 
string option * (cterm list * cterm list) * context * context * 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

56 
(term * (term list * term list)) list list 
15596  57 

58 
(* Diagnostic functions *) 

12758  59 
val print_locales: theory > unit 
15703  60 
val print_locale: theory > expr > element list > unit 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

61 
val print_global_registrations: string > theory > unit 
15703  62 
val print_local_registrations': string > context > unit 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

63 
val print_local_registrations: string > context > unit 
15596  64 

15696  65 
(* Storing results *) 
15703  66 
val add_locale: bool > bstring > expr > element list > theory > theory 
67 
val add_locale_i: bool > bstring > expr > element_i list > theory > theory 

68 
val smart_note_thmss: string > string option > 

12958  69 
((bstring * theory attribute list) * (thm list * theory attribute list) list) list > 
70 
theory > theory * (bstring * thm list) list 

15703  71 
val note_thmss: string > xstring > 
72 
((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list > 

12711  73 
theory > theory * (bstring * thm list) list 
15703  74 
val note_thmss_i: string > string > 
75 
((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list > 

12711  76 
theory > theory * (bstring * thm list) list 
15703  77 
val add_thmss: string > string > ((string * thm list) * Attrib.src list) list > 
13375  78 
theory * context > (theory * context) * (string * thm list) list 
15596  79 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

80 
(* Locale interpretation *) 
14528
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

81 
val instantiate: string > string * context attribute list 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

82 
> thm list option > context > context 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

83 
val prep_global_registration: 
15703  84 
string * Attrib.src list > expr > string option list > theory > 
15596  85 
theory * ((string * term list) * term list) list * (theory > theory) 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

86 
val prep_local_registration: 
15703  87 
string * Attrib.src list > expr > string option list > context > 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

88 
context * ((string * term list) * term list) list * (context > context) 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

89 
val add_global_witness: 
15596  90 
string * term list > thm > theory > theory 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

91 
val add_local_witness: 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

92 
string * term list > thm > context > context 
11896  93 
end; 
12839  94 

12289  95 
structure Locale: LOCALE = 
11896  96 
struct 
97 

12273  98 
(** locale elements and expressions **) 
11896  99 

12014  100 
type context = ProofContext.context; 
11896  101 

15703  102 
datatype ('typ, 'term, 'fact) elem = 
12058  103 
Fixes of (string * 'typ option * mixfix option) list  
15703  104 
Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list  
105 
Defines of ((string * Attrib.src list) * ('term * 'term list)) list  

106 
Notes of ((string * Attrib.src list) * ('fact * Attrib.src list) list) list; 

12273  107 

108 
datatype expr = 

109 
Locale of string  

110 
Rename of expr * string option list  

111 
Merge of expr list; 

11896  112 

12273  113 
val empty = Merge []; 
114 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

115 
datatype 'a elem_expr = 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

116 
Elem of 'a  Expr of expr; 
12273  117 

15703  118 
type element = (string, string, thmref) elem; 
119 
type element_i = (typ, term, thm list) elem; 

12070  120 

121 
type locale = 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

122 
{predicate: cterm list * thm list, 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

123 
(* CB: For oldstyle locales with "(open)" this entry is ([], []). 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

124 
For newstyle locales, which declare predicates, if the locale declares 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

125 
no predicates, this is also ([], []). 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

126 
If the locale declares predicates, the record field is 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

127 
([statement], axioms), where statement is the locale predicate applied 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

128 
to the (assumed) locale parameters. Axioms contains the projections 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

129 
from the locale predicate to the normalised assumptions of the locale 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

130 
(cf. [1], normalisation of locale expressions.) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

131 
*) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

132 
import: expr, (*dynamic import*) 
15703  133 
elems: (element_i * stamp) list, (*static content*) 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

134 
params: (string * typ option) list * string list} (*all/local params*) 
12063  135 

11896  136 

15703  137 
(* CB: an internal (Int) locale element was either imported or included, 
138 
an external (Ext) element appears directly in the locale text. *) 

139 

140 
datatype ('a, 'b) int_ext = Int of 'a  Ext of 'b; 

141 

142 

143 

15837  144 
(** term and type instantiation, using symbol tables **) 
145 

146 
(* instantiate TFrees *) 

147 

148 
fun tinst_tab_type tinst T = if Symtab.is_empty tinst 

149 
then T 

150 
else Term.map_type_tfree 

151 
(fn (v as (x, _)) => getOpt (Symtab.lookup (tinst, x), (TFree v))) T; 

152 

153 
fun tinst_tab_term tinst t = if Symtab.is_empty tinst 

154 
then t 

155 
else Term.map_term_types (tinst_tab_type tinst) t; 

156 

157 
fun tinst_tab_thm sg tinst thm = if Symtab.is_empty tinst 

158 
then thm 

159 
else let 

160 
val cert = Thm.cterm_of sg; 

161 
val certT = Thm.ctyp_of sg; 

162 
val {hyps, prop, ...} = Thm.rep_thm thm; 

163 
val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps); 

164 
val tinst' = Symtab.dest tinst > 

165 
List.filter (fn (a, _) => a mem_string tfrees); 

166 
in 

167 
if null tinst' then thm 

168 
else thm > Drule.implies_intr_list (map cert hyps) 

169 
> Drule.tvars_intr_list (map #1 tinst') 

170 
> (fn (th, al) => th > Thm.instantiate 

171 
((map (fn (a, T) => (certT (TVar (valOf (assoc (al, a)))), certT T)) tinst'), 

172 
[])) 

173 
> (fn th => Drule.implies_elim_list th 

174 
(map (Thm.assume o cert o tinst_tab_term tinst) hyps)) 

175 
end; 

176 

177 

178 
(* instantiate TFrees and Frees *) 

179 

180 
fun inst_tab_term (inst, tinst) = if Symtab.is_empty inst 

181 
then tinst_tab_term tinst 

182 
else (* instantiate terms and types simultaneously *) 

183 
let 

184 
fun instf (Const (x, T)) = Const (x, tinst_tab_type tinst T) 

185 
 instf (Free (x, T)) = (case Symtab.lookup (inst, x) of 

186 
NONE => Free (x, tinst_tab_type tinst T) 

187 
 SOME t => t) 

188 
 instf (Var (xi, T)) = Var (xi, tinst_tab_type tinst T) 

189 
 instf (b as Bound _) = b 

190 
 instf (Abs (x, T, t)) = Abs (x, tinst_tab_type tinst T, instf t) 

191 
 instf (s $ t) = instf s $ instf t 

192 
in instf end; 

193 

194 
fun inst_tab_thm sg (inst, tinst) thm = if Symtab.is_empty inst 

195 
then tinst_tab_thm sg tinst thm 

196 
else let 

197 
val cert = Thm.cterm_of sg; 

198 
val certT = Thm.ctyp_of sg; 

199 
val {hyps, prop, ...} = Thm.rep_thm thm; 

200 
(* type instantiations *) 

201 
val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps); 

202 
val tinst' = Symtab.dest tinst > 

203 
List.filter (fn (a, _) => a mem_string tfrees); 

204 
(* term instantiations; 

205 
note: lhss are type instantiated, because 

206 
type insts will be done first*) 

207 
val frees = foldr Term.add_term_frees [] (prop :: hyps); 

208 
val inst' = Symtab.dest inst > 

209 
List.mapPartial (fn (a, t) => 

210 
get_first (fn (Free (x, T)) => 

211 
if a = x then SOME (Free (x, tinst_tab_type tinst T), t) 

212 
else NONE) frees); 

213 
in 

214 
if null tinst' andalso null inst' then tinst_tab_thm sg tinst thm 

215 
else thm > Drule.implies_intr_list (map cert hyps) 

216 
> Drule.tvars_intr_list (map #1 tinst') 

217 
> (fn (th, al) => th > Thm.instantiate 

218 
((map (fn (a, T) => (certT (TVar (valOf (assoc (al, a)))), certT T)) tinst'), 

219 
[])) 

220 
> Drule.forall_intr_list (map (cert o #1) inst') 

221 
> Drule.forall_elim_list (map (cert o #2) inst') 

222 
> (fn th => Drule.implies_elim_list th 

223 
(map (Thm.assume o cert o inst_tab_term (inst, tinst)) hyps)) 

224 
end; 

225 

226 

227 
(** registration management **) 

11896  228 

15837  229 
structure Registrations : 
230 
sig 

231 
type T 

232 
val empty: T 

233 
val join: T * T > T 

234 
val dest: T > (term list * ((string * Attrib.src list) * thm list)) list 

235 
val lookup: Sign.sg > T * term list > 

236 
((string * Attrib.src list) * thm list) option 

237 
val insert: Sign.sg > term list * (string * Attrib.src list) > T > 

238 
T * (term list * ((string * Attrib.src list) * thm list)) list 

239 
val add_witness: term list > thm > T > T 

240 
end = 

241 
struct 

242 
(* a registration consists of theorems instantiating locale assumptions 

243 
and prefix and attributes, indexed by parameter instantiation *) 

244 
type T = ((string * Attrib.src list) * thm list) Termtab.table; 

245 

246 
val empty = Termtab.empty; 

247 

248 
(* term list represented as single term, for simultaneous matching *) 

249 
fun termify ts = 

250 
Library.foldl (op $) (Const ("", map fastype_of ts > propT), ts); 

251 
fun untermify t = 

252 
let fun ut (Const _) ts = ts 

253 
 ut (s $ t) ts = ut s (t::ts) 

254 
in ut t [] end; 

255 

256 
(* joining of registrations: prefix and attributs of left theory, 

257 
thms are equal, no attempt to subsumption testing *) 

15842  258 
fun join x = Termtab.join (fn (reg, _) => SOME reg) x; 
15837  259 

260 
fun dest regs = map (apfst untermify) (Termtab.dest regs); 

261 

262 
(* registrations that subsume t *) 

263 
fun subsumers tsig t regs = 

264 
List.filter (fn (t', _) => Pattern.matches tsig (t', t)) (Termtab.dest regs); 

265 

266 
(* look up registration, pick one that subsumes the query *) 

267 
fun lookup sign (regs, ts) = 

268 
let 

269 
val tsig = Sign.tsig_of sign; 

270 
val t = termify ts; 

271 
val subs = subsumers tsig t regs; 

272 
in (case subs of 

273 
[] => NONE 

274 
 ((t', (attn, thms)) :: _) => let 

275 
val (tinst, inst) = Pattern.match tsig (t', t); 

276 
(* thms contain Frees, not Vars *) 

277 
val tinst' = tinst > Vartab.dest 

278 
> map (fn ((x, 0), (_, T)) => (x, Type.unvarifyT T)) 

279 
> Symtab.make; 

280 
val inst' = inst > Vartab.dest 

281 
> map (fn ((x, 0), (_, t)) => (x, Logic.unvarify t)) 

282 
> Symtab.make; 

283 
in 

284 
SOME (attn, map (inst_tab_thm sign (inst', tinst')) thms) 

285 
end) 

286 
end; 

287 

288 
(* add registration if not subsumed by ones already present, 

289 
additionally returns registrations that are strictly subsumed *) 

290 
fun insert sign (ts, attn) regs = 

291 
let 

292 
val tsig = Sign.tsig_of sign; 

293 
val t = termify ts; 

294 
val subs = subsumers tsig t regs ; 

295 
in (case subs of 

296 
[] => let 

297 
val sups = 

298 
List.filter (fn (t', _) => Pattern.matches tsig (t, t')) (Termtab.dest regs); 

299 
val sups' = map (apfst untermify) sups 

300 
in (Termtab.update ((t, (attn, [])), regs), sups') end 

301 
 _ => (regs, [])) 

302 
end; 

303 

304 
(* add witness theorem to registration, 

305 
only if instantiation is exact, otherwise excpetion Option raised *) 

306 
fun add_witness ts thm regs = 

307 
let 

308 
val t = termify ts; 

309 
val (x, thms) = valOf (Termtab.lookup (regs, t)); 

310 
in 

311 
Termtab.update ((t, (x, thm::thms)), regs) 

312 
end; 

313 
end; 

314 

315 
(** theory data **) 

15596  316 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

317 
structure GlobalLocalesArgs = 
11896  318 
struct 
12014  319 
val name = "Isar/locales"; 
15837  320 
type T = NameSpace.T * locale Symtab.table * Registrations.T Symtab.table; 
15596  321 
(* 1st entry: locale namespace, 
322 
2nd entry: locales of the theory, 

15837  323 
3rd entry: registrations, indexed by locale name *) 
11896  324 

15596  325 
val empty = (NameSpace.empty, Symtab.empty, Symtab.empty); 
12063  326 
val copy = I; 
12118  327 
val prep_ext = I; 
12289  328 

15596  329 
fun join_locs ({predicate, import, elems, params}: locale, 
330 
{elems = elems', ...}: locale) = 

331 
SOME {predicate = predicate, import = import, 

332 
elems = gen_merge_lists eq_snd elems elems', 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

333 
params = params}; 
15596  334 
fun merge ((space1, locs1, regs1), (space2, locs2, regs2)) = 
335 
(NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2), 

15837  336 
Symtab.join (SOME o Registrations.join) (regs1, regs2)); 
12289  337 

15596  338 
fun print _ (space, locs, _) = 
12273  339 
Pretty.strs ("locales:" :: map (NameSpace.cond_extern space o #1) (Symtab.dest locs)) 
12014  340 
> Pretty.writeln; 
11896  341 
end; 
342 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

343 
structure GlobalLocalesData = TheoryDataFun(GlobalLocalesArgs); 
15801  344 
val _ = Context.add_setup [GlobalLocalesData.init]; 
345 

346 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

347 

484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

348 
(** context data **) 
11896  349 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

350 
structure LocalLocalesArgs = 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

351 
struct 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

352 
val name = "Isar/locales"; 
15837  353 
type T = Registrations.T Symtab.table; 
354 
(* registrations, indexed by locale name *) 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

355 
fun init _ = Symtab.empty; 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

356 
fun print _ _ = (); 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

357 
end; 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

358 

484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

359 
structure LocalLocalesData = ProofDataFun(LocalLocalesArgs); 
15801  360 
val _ = Context.add_setup [LocalLocalesData.init]; 
12289  361 

12277  362 

363 
(* access locales *) 

364 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

365 
val print_locales = GlobalLocalesData.print; 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

366 

484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

367 
val intern = NameSpace.intern o #1 o GlobalLocalesData.get_sg; 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

368 
val cond_extern = NameSpace.cond_extern o #1 o GlobalLocalesData.get_sg; 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

369 

12063  370 
fun declare_locale name = 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

371 
GlobalLocalesData.map (fn (space, locs, regs) => 
15596  372 
(NameSpace.extend (space, [name]), locs, regs)); 
11896  373 

15596  374 
fun put_locale name loc = 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

375 
GlobalLocalesData.map (fn (space, locs, regs) => 
15596  376 
(space, Symtab.update ((name, loc), locs), regs)); 
377 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

378 
fun get_locale thy name = Symtab.lookup (#2 (GlobalLocalesData.get thy), name); 
11896  379 

12014  380 
fun the_locale thy name = 
381 
(case get_locale thy name of 

15531  382 
SOME loc => loc 
383 
 NONE => error ("Unknown locale " ^ quote name)); 

11896  384 

12046  385 

15596  386 
(* access registrations *) 
387 

15696  388 
(* Ids of global registrations are varified, 
389 
Ids of local registrations are not. 

390 
Thms of registrations are never varified. *) 

391 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

392 
(* retrieve registration from theory or context *) 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

393 

15696  394 
fun gen_get_registrations get thy_ctxt name = 
395 
case Symtab.lookup (get thy_ctxt, name) of 

396 
NONE => [] 

15837  397 
 SOME reg => Registrations.dest reg; 
15696  398 

399 
val get_global_registrations = 

400 
gen_get_registrations (#3 o GlobalLocalesData.get); 

401 
val get_local_registrations = 

402 
gen_get_registrations LocalLocalesData.get; 

403 

15837  404 
fun gen_get_registration get get_sg thy_ctxt (name, ps) = 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

405 
case Symtab.lookup (get thy_ctxt, name) of 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

406 
NONE => NONE 
15837  407 
 SOME reg => Registrations.lookup (get_sg thy_ctxt) (reg, ps); 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

408 

484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

409 
val get_global_registration = 
15837  410 
gen_get_registration (#3 o GlobalLocalesData.get) Theory.sign_of; 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

411 
val get_local_registration = 
15837  412 
gen_get_registration LocalLocalesData.get ProofContext.sign_of; 
15596  413 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

414 
val test_global_registration = isSome oo get_global_registration; 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

415 
val test_local_registration = isSome oo get_local_registration; 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

416 
fun smart_test_registration ctxt id = 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

417 
let 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

418 
val thy = ProofContext.theory_of ctxt; 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

419 
in 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

420 
test_global_registration thy id orelse test_local_registration ctxt id 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

421 
end; 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

422 

484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

423 

15837  424 
(* add registration to theory or context, ignored if subsumed *) 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

425 

15837  426 
fun gen_put_registration map_data get_sg (name, ps) attn thy_ctxt = 
427 
map_data (fn regs => 

428 
let 

429 
val sg = get_sg thy_ctxt; 

430 
val reg = getOpt (Symtab.lookup (regs, name), Registrations.empty); 

431 
val (reg', sups) = Registrations.insert sg (ps, attn) reg; 

432 
val _ = if not (null sups) then warning 

433 
("Subsumed interpretation(s) of locale " ^ 

434 
quote (cond_extern sg name) ^ 

435 
"\nby interpretation(s) with the following prefix(es):\n" ^ 

436 
commas_quote (map (fn (_, ((s, _), _)) => s) sups)) 

437 
else (); 

438 
in Symtab.update ((name, reg'), regs) end) thy_ctxt; 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

439 

484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

440 
val put_global_registration = 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

441 
gen_put_registration (fn f => 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

442 
GlobalLocalesData.map (fn (space, locs, regs) => 
15837  443 
(space, locs, f regs))) Theory.sign_of; 
444 
val put_local_registration = 

445 
gen_put_registration LocalLocalesData.map ProofContext.sign_of; 

15596  446 

15696  447 
(* TODO: needed? *) 
15837  448 
(* 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

449 
fun smart_put_registration id attn ctxt = 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

450 
(* ignore registration if already present in theory *) 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

451 
let 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

452 
val thy = ProofContext.theory_of ctxt; 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

453 
in case get_global_registration thy id of 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

454 
NONE => put_local_registration id attn ctxt 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

455 
 SOME _ => ctxt 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

456 
end; 
15837  457 
*) 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

458 

484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

459 
(* add witness theorem to registration in theory or context, 
15596  460 
ignored if registration not present *) 
461 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

462 
fun gen_add_witness map (name, ps) thm = 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

463 
map (fn regs => 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

464 
let 
15837  465 
val reg = valOf (Symtab.lookup (regs, name)); 
15596  466 
in 
15837  467 
Symtab.update ((name, Registrations.add_witness ps thm reg), regs) 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

468 
end handle Option => regs); 
15596  469 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

470 
val add_global_witness = 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

471 
gen_add_witness (fn f => 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

472 
GlobalLocalesData.map (fn (space, locs, regs) => 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

473 
(space, locs, f regs))); 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

474 
val add_local_witness = gen_add_witness LocalLocalesData.map; 
15596  475 

476 

14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

477 
(* import hierarchy 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

478 
implementation could be more efficient, eg. by maintaining a database 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

479 
of dependencies *) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

480 

ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

481 
fun imports thy (upper, lower) = 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

482 
let 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

483 
val sign = sign_of thy; 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

484 
fun imps (Locale name) low = (name = low) orelse 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

485 
(case get_locale thy name of 
15531  486 
NONE => false 
487 
 SOME {import, ...} => imps import low) 

14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

488 
 imps (Rename (expr, _)) low = imps expr low 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

489 
 imps (Merge es) low = exists (fn e => imps e low) es; 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

490 
in 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

491 
imps (Locale (intern sign upper)) (intern sign lower) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

492 
end; 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

493 

ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

494 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

495 
(* printing of registrations *) 
15596  496 

15703  497 
fun gen_print_registrations get_regs mk_ctxt msg loc thy_ctxt = 
15596  498 
let 
15703  499 
val ctxt = mk_ctxt thy_ctxt; 
500 
val thy = ProofContext.theory_of ctxt; 

501 
val sg = Theory.sign_of thy; 

502 

503 
val prt_term = Pretty.quote o ProofContext.pretty_term ctxt; 

504 
val prt_atts = Args.pretty_attribs ctxt; 

505 
fun prt_inst (ts, (("", []), thms)) = 

506 
Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts)) 

507 
 prt_inst (ts, ((prfx, atts), thms)) = 

15837  508 
Pretty.block ( 
509 
(Pretty.breaks (Pretty.str prfx :: prt_atts atts) @ 

510 
[Pretty.str ":", Pretty.brk 1, 

511 
Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts))])); 

15703  512 

15596  513 
val loc_int = intern sg loc; 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

514 
val regs = get_regs thy_ctxt; 
15596  515 
val loc_regs = Symtab.lookup (regs, loc_int); 
516 
in 

517 
(case loc_regs of 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

518 
NONE => Pretty.str ("No interpretations in " ^ msg ^ ".") 
15763
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
15749
diff
changeset

519 
 SOME r => let 
15837  520 
val r' = Registrations.dest r; 
15763
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
15749
diff
changeset

521 
val r'' = Library.sort_wrt (fn (_, ((prfx, _), _)) => prfx) r'; 
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
15749
diff
changeset

522 
in Pretty.big_list ("Interpretations in " ^ msg ^ ":") 
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
15749
diff
changeset

523 
(map prt_inst r'') 
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
15749
diff
changeset

524 
end) 
15596  525 
> Pretty.writeln 
526 
end; 

527 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

528 
val print_global_registrations = 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

529 
gen_print_registrations (#3 o GlobalLocalesData.get) 
15703  530 
ProofContext.init "theory"; 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

531 
val print_local_registrations' = 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

532 
gen_print_registrations LocalLocalesData.get 
15703  533 
I "context"; 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

534 
fun print_local_registrations loc ctxt = 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

535 
(print_global_registrations loc (ProofContext.theory_of ctxt); 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

536 
print_local_registrations' loc ctxt); 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

537 

15596  538 

12277  539 
(* diagnostics *) 
12273  540 

12277  541 
fun err_in_locale ctxt msg ids = 
542 
let 

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

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

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

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

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

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

12063  552 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

553 
(* Version for identifiers with axioms *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

554 

09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

555 
fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids'); 
12277  556 

557 

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

558 
(** primitives **) 
12046  559 

15703  560 
(* map elements *) 
561 

562 
fun map_elem {name, var, typ, term, fact, attrib} = 

563 
fn Fixes fixes => Fixes (fixes > map (fn (x, T, mx) => 

564 
let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end)) 

565 
 Assumes asms => Assumes (asms > map (fn ((a, atts), propps) => 

566 
((name a, map attrib atts), propps > map (fn (t, (ps, qs)) => 

567 
(term t, (map term ps, map term qs)))))) 

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

569 
((name a, map attrib atts), (term t, map term ps)))) 

570 
 Notes facts => Notes (facts > map (fn ((a, atts), bs) => 

571 
((name a, map attrib atts), bs > map (fn (ths, btts) => (fact ths, map attrib btts))))); 

572 

573 
fun map_values typ term thm = map_elem 

574 
{name = I, var = I, typ = typ, term = term, fact = map thm, 

575 
attrib = Args.map_values I typ term thm}; 

576 

577 

578 
(* map attributes *) 

579 

580 
fun map_attrib_specs f = map (apfst (apsnd (map f))); 

581 
fun map_attrib_facts f = map (apfst (apsnd (map f)) o apsnd (map (apsnd (map f)))); 

582 

583 
fun map_attrib_elem f = map_elem {name = I, var = I, typ = I, term = I, fact = I, attrib = f}; 

584 

585 
fun intern_attrib_elem thy = map_attrib_elem (Attrib.intern_src (Theory.sign_of thy)); 

586 

587 
fun intern_attrib_elem_expr thy (Elem elem) = Elem (intern_attrib_elem thy elem) 

588 
 intern_attrib_elem_expr _ (Expr expr) = Expr expr; 

589 

590 

12277  591 
(* renaming *) 
12263  592 

15570  593 
fun rename ren x = getOpt (assoc_string (ren, x), x); 
12263  594 

15703  595 
fun rename_var ren (x, mx) = 
596 
let val x' = rename ren x in 

597 
if x = x' then (x, mx) 

598 
else (x', if mx = NONE then mx else SOME Syntax.NoSyn) (*drop syntax*) 

599 
end; 

600 

12263  601 
fun rename_term ren (Free (x, T)) = Free (rename ren x, T) 
602 
 rename_term ren (t $ u) = rename_term ren t $ rename_term ren u 

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

604 
 rename_term _ a = a; 

605 

606 
fun rename_thm ren th = 

607 
let 

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

609 
val cert = Thm.cterm_of sign; 

15570  610 
val (xs, Ts) = Library.split_list (Library.foldl Term.add_frees ([], prop :: hyps)); 
12263  611 
val xs' = map (rename ren) xs; 
612 
fun cert_frees names = map (cert o Free) (names ~~ Ts); 

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

614 
in 

615 
if xs = xs' then th 

616 
else 

617 
th 

618 
> Drule.implies_intr_list (map cert hyps) 

619 
> Drule.forall_intr_list (cert_frees xs) 

620 
> Drule.forall_elim_list (cert_vars xs) 

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

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

623 
end; 

624 

15703  625 
fun rename_elem ren = 
626 
map_values I (rename_term ren) (rename_thm ren) o 

627 
map_elem {name = I, typ = I, term = I, fact = I, attrib = I, var = rename_var ren}; 

12263  628 

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

629 
fun rename_facts prfx elem = 
12307  630 
let 
12323  631 
fun qualify (arg as ((name, atts), x)) = 
13394  632 
if prfx = "" orelse name = "" then arg 
13375  633 
else ((NameSpace.pack [prfx, name], atts), x); 
12307  634 
in 
635 
(case elem of 

636 
Fixes fixes => Fixes fixes 

637 
 Assumes asms => Assumes (map qualify asms) 

638 
 Defines defs => Defines (map qualify defs) 

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

640 
end; 

641 

12263  642 

12502  643 
(* type instantiation *) 
644 

645 
fun inst_type [] T = T 

15570  646 
 inst_type env T = Term.map_type_tfree (fn v => getOpt (assoc (env, v), TFree v)) T; 
12502  647 

648 
fun inst_term [] t = t 

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

650 

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

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

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

654 
val sign = ProofContext.sign_of ctxt; 
12575  655 
val cert = Thm.cterm_of sign; 
656 
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

657 
val {hyps, prop, maxidx, ...} = Thm.rep_thm th; 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

658 
val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps); 
15570  659 
val env' = List.filter (fn ((a, _), _) => a mem_string tfrees) env; 
12502  660 
in 
661 
if null env' then th 

662 
else 

663 
th 

664 
> Drule.implies_intr_list (map cert hyps) 

12575  665 
> Drule.tvars_intr_list (map (#1 o #1) env') 
12502  666 
> (fn (th', al) => th' > 
15798
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15763
diff
changeset

667 
Thm.instantiate ((map (fn ((a, _), T) => 
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15763
diff
changeset

668 
(certT (TVar (valOf (assoc (al, a)))), certT T)) env'), [])) 
12502  669 
> (fn th'' => Drule.implies_elim_list th'' 
670 
(map (Thm.assume o cert o inst_term env') hyps)) 

671 
end; 

672 

15703  673 
fun inst_elem ctxt env = 
674 
map_values (inst_type env) (inst_term env) (inst_thm ctxt env); 

12502  675 

676 

15696  677 
(* term and type instantiation, variant using symbol tables *) 
678 

679 
(* instantiate TFrees *) 

680 

15749  681 
fun tinst_tab_elem sg tinst = 
682 
map_values (tinst_tab_type tinst) (tinst_tab_term tinst) (tinst_tab_thm sg tinst); 

683 

15696  684 
(* instantiate TFrees and Frees *) 
685 

15763
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
15749
diff
changeset

686 
fun inst_tab_elem sg (inst as (_, tinst)) = 
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
15749
diff
changeset

687 
map_values (tinst_tab_type tinst) (inst_tab_term inst) (inst_tab_thm sg inst); 
15696  688 

689 
fun inst_tab_elems sign inst ((n, ps), elems) = 

690 
((n, map (inst_tab_term inst) ps), map (inst_tab_elem sign inst) elems); 

691 

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

692 

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

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

694 

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

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

696 

14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

697 
(* CB: frozen_tvars has the following type: 
15798
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15763
diff
changeset

698 
ProofContext.context > Term.typ list > (Term.indexname * (sort * Term.typ)) list *) 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

699 

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

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

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

703 
val tfrees = map TFree 
14695  704 
(Term.invent_names (ProofContext.used_types ctxt) "'a" (length tvars) ~~ map #2 tvars); 
15798
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15763
diff
changeset

705 
in map (fn ((x, S), y) => (x, (S, y))) (tvars ~~ tfrees) end; 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

706 

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

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

708 
let 
15531  709 
fun paramify (i, NONE) = (i, NONE) 
710 
 paramify (i, SOME T) = apsnd SOME (TypeInfer.paramify_dummies (i, T)); 

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

711 

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

712 
val (maxidx', Ts') = foldl_map paramify (maxidx, Ts); 
12727  713 
val (maxidx'', Us') = foldl_map paramify (maxidx', Us); 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

714 
val tsig = Sign.tsig_of (ProofContext.sign_of ctxt); 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

715 

15531  716 
fun unify (env, (SOME T, SOME U)) = (Type.unify tsig env (U, T) 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

717 
handle Type.TUNIFY => 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

718 
raise TYPE ("unify_frozen: failed to unify types", [U, T], [])) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

719 
 unify (env, _) = env; 
15570  720 
val (unifier, _) = Library.foldl unify ((Vartab.empty, maxidx''), Ts' ~~ Us'); 
721 
val Vs = map (Option.map (Envir.norm_type unifier)) Us'; 

722 
val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (List.mapPartial I Vs)); 

723 
in map (Option.map (Envir.norm_type unifier')) Vs end; 

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

724 

15570  725 
fun params_of elemss = gen_distinct eq_fst (List.concat (map (snd o fst) elemss)); 
726 
fun params_of' elemss = gen_distinct eq_fst (List.concat (map (snd o fst o fst) elemss)); 

14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

727 

859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

728 
(* CB: param_types has the following type: 
15531  729 
('a * 'b option) list > ('a * 'b) list *) 
15570  730 
fun param_types ps = List.mapPartial (fn (_, NONE) => NONE  (x, SOME T) => SOME (x, T)) ps; 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

731 

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

732 

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

733 
(* flatten expressions *) 
11896  734 

12510  735 
local 
12502  736 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

737 
(* CB: OUTDATED unique_parms has the following type: 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

738 
'a > 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

739 
(('b * (('c * 'd) list * Symtab.key list)) * 'e) list > 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

740 
(('b * ('c * 'd) list) * 'e) list *) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

741 

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

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

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

744 
val param_decls = 
15570  745 
List.concat (map (fn (((name, (ps, qs)), _), _) => map (rpair (name, ps)) qs) elemss) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

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

748 
(case find_first (fn (_, ids) => length ids > 1) param_decls of 
15531  749 
SOME (q, ids) => err_in_locale ctxt ("Multiple declaration of parameter " ^ quote q) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

750 
(map (apsnd (map fst)) ids) 
15531  751 
 NONE => map (apfst (apfst (apsnd #1))) elemss) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

753 

14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

754 
(* CB: unify_parms has the following type: 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

755 
ProofContext.context > 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

756 
(string * Term.typ) list > 
15531  757 
(string * Term.typ option) list list > 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

758 
((string * Term.sort) * Term.typ) list list *) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

759 

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

760 
fun unify_parms ctxt fixed_parms raw_parmss = 
12502  761 
let 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

762 
val sign = ProofContext.sign_of ctxt; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

763 
val tsig = Sign.tsig_of sign; 
12502  764 
val maxidx = length raw_parmss; 
765 
val idx_parmss = (0 upto maxidx  1) ~~ raw_parmss; 

766 

767 
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

768 
fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps); 
15570  769 
val parms = fixed_parms @ List.concat (map varify_parms idx_parmss); 
12502  770 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

771 
fun unify T ((env, maxidx), U) = 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

772 
Type.unify tsig (env, maxidx) (U, T) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

773 
handle Type.TUNIFY => 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

774 
let val prt = Sign.string_of_typ sign 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

775 
in raise TYPE ("unify_parms: failed to unify types " ^ 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

776 
prt U ^ " and " ^ prt T, [U, T], []) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

777 
end 
15570  778 
fun unify_list (envir, T :: Us) = Library.foldl (unify T) (envir, Us) 
12502  779 
 unify_list (envir, []) = envir; 
15570  780 
val (unifier, _) = Library.foldl unify_list 
12502  781 
((Vartab.empty, maxidx), map #2 (Symtab.dest (Symtab.make_multi parms))); 
782 

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

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

785 

786 
fun inst_parms (i, ps) = 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

787 
foldr Term.add_typ_tfrees [] (List.mapPartial snd ps) 
15570  788 
> List.mapPartial (fn (a, S) => 
12502  789 
let val T = Envir.norm_type unifier' (TVar ((a, i), S)) 
15531  790 
in if T = TFree (a, S) then NONE else SOME ((a, S), T) end) 
12502  791 
in map inst_parms idx_parmss end; 
792 

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

793 
in 
12502  794 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

795 
(* like unify_elemss, but does not touch axioms *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

796 

09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

797 
fun unify_elemss' _ _ [] = [] 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

798 
 unify_elemss' _ [] [elems] = [elems] 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

799 
 unify_elemss' ctxt fixed_parms elemss = 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

800 
let 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

801 
val envs = unify_parms ctxt fixed_parms (map (#2 o #1 o #1) elemss); 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

802 
fun inst ((((name, ps), axs), elems), env) = 
15570  803 
(((name, map (apsnd (Option.map (inst_type env))) ps), axs), 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

804 
map (inst_elem ctxt env) elems); 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

805 
in map inst (elemss ~~ envs) end; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

806 

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

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

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

809 
 unify_elemss ctxt fixed_parms elemss = 
12502  810 
let 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

811 
val envs = unify_parms ctxt fixed_parms (map (#2 o #1 o #1) elemss); 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

812 
fun inst ((((name, ps), axs), elems), env) = 
15570  813 
(((name, map (apsnd (Option.map (inst_type env))) ps), 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

814 
map (inst_thm ctxt env) axs), map (inst_elem ctxt env) elems); 
12839  815 
in map inst (elemss ~~ envs) end; 
12502  816 

15596  817 
(* flatten_expr: 
818 
Extend list of identifiers by those new in locale expression expr. 

819 
Compute corresponding list of lists of locale elements (one entry per 

820 
identifier). 

821 

822 
Identifiers represent locale fragments and are in an extended form: 

823 
((name, ps), (ax_ps, axs)) 

824 
(name, ps) is the locale name with all its parameters. 

825 
(ax_ps, axs) is the locale axioms with its parameters; 

826 
axs are always taken from the top level of the locale hierarchy, 

827 
hence axioms may contain additional parameters from later fragments: 

828 
ps subset of ax_ps. axs is either singleton or empty. 

829 

830 
Elements are enriched by identifierlike information: 

831 
(((name, ax_ps), axs), elems) 

832 
The parameters in ax_ps are the axiom parameters, but enriched by type 

833 
info: now each entry is a pair of string and typ option. Axioms are 

834 
typeinstantiated. 

835 

836 
*) 

837 

12575  838 
fun flatten_expr ctxt (prev_idents, expr) = 
12014  839 
let 
840 
val thy = ProofContext.theory_of ctxt; 

15596  841 
(* thy used for retrieval of locale info, 
842 
ctxt for error messages, parameter unification and instantiation 

843 
of axioms *) 

844 
(* TODO: consider err_in_locale with thy argument *) 

12263  845 

15531  846 
fun renaming (SOME x :: xs) (y :: ys) = (y, x) :: renaming xs ys 
847 
 renaming (NONE :: xs) (y :: ys) = renaming xs ys 

12273  848 
 renaming [] _ = [] 
12289  849 
 renaming xs [] = raise ERROR_MESSAGE ("Too many arguments in renaming: " ^ 
15531  850 
commas (map (fn NONE => "_"  SOME x => quote x) xs)); 
12289  851 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

852 
fun rename_parms top ren ((name, ps), (parms, axs)) = 
12289  853 
let val ps' = map (rename ren) ps in 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

854 
(case duplicates ps' of [] => ((name, ps'), 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

855 
if top then (map (rename ren) parms, map (rename_thm ren) axs) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

856 
else (parms, axs)) 
12289  857 
 dups => err_in_locale ctxt ("Duplicate parameters: " ^ commas_quote dups) [(name, ps')]) 
858 
end; 

12263  859 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

860 
fun identify top (Locale name) = 
15596  861 
(* CB: ids_ax is a list of tuples of the form ((name, ps), axs), 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

862 
where name is a locale name, ps a list of parameter names and axs 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

863 
a list of axioms relating to the identifier, axs is empty unless 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

864 
identify at top level (top = true); 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

865 
parms is accumulated list of parameters *) 
12289  866 
let 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

867 
val {predicate = (_, axioms), import, params, ...} = 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

868 
the_locale thy name; 
12289  869 
val ps = map #1 (#1 params); 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

870 
val (ids', parms') = identify false import; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

871 
(* acyclic import dependencies *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

872 
val ids'' = ids' @ [((name, ps), ([], []))]; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

873 
val ids_ax = if top then snd 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

874 
(foldl_map (fn (axs, ((name, parms), _)) => let 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

875 
val {elems, ...} = the_locale thy name; 
15570  876 
val ts = List.concat (List.mapPartial (fn (Assumes asms, _) => 
877 
SOME (List.concat (map (map #1 o #2) asms))  _ => NONE) elems); 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

878 
val (axs1, axs2) = splitAt (length ts, axs); 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

879 
in (axs2, ((name, parms), (ps, axs1))) end) (axioms, ids'')) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

880 
else ids''; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

881 
in (ids_ax, merge_lists parms' ps) end 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

882 
 identify top (Rename (e, xs)) = 
12273  883 
let 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

884 
val (ids', parms') = identify top e; 
12839  885 
val ren = renaming xs parms' 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

886 
handle ERROR_MESSAGE msg => err_in_locale' ctxt msg ids'; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

887 
val ids'' = gen_distinct eq_fst (map (rename_parms top ren) ids'); 
15570  888 
val parms'' = distinct (List.concat (map (#2 o #1) ids'')); 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

889 
in (ids'', parms'') end 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

890 
 identify top (Merge es) = 
15570  891 
Library.foldl (fn ((ids, parms), e) => let 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

892 
val (ids', parms') = identify top e 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

893 
in (gen_merge_lists eq_fst ids ids', 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

894 
merge_lists parms parms') end) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

895 
(([], []), es); 
12014  896 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

897 
(* CB: enrich identifiers by parameter types and 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

898 
the corresponding elements (with renamed parameters) *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

899 

09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

900 
fun eval ((name, xs), axs) = 
12273  901 
let 
13308  902 
val {params = (ps, qs), elems, ...} = the_locale thy name; 
12307  903 
val ren = filter_out (op =) (map #1 ps ~~ xs); 
13308  904 
val (params', elems') = 
905 
if null ren then ((ps, qs), map #1 elems) 

12502  906 
else ((map (apfst (rename ren)) ps, map (rename ren) qs), 
13308  907 
map (rename_elem ren o #1) elems); 
13375  908 
val elems'' = map (rename_facts (space_implode "_" xs)) elems'; 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

909 
in (((name, params'), axs), elems'') end; 
12307  910 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

911 
(* compute identifiers, merge with previous ones *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

912 
val idents = gen_rems eq_fst (#1 (identify true expr), prev_idents); 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

913 
(* add types to params, check for unique params and unify them *) 
12575  914 
val raw_elemss = unique_parms ctxt (map eval idents); 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

915 
val elemss = unify_elemss' ctxt [] raw_elemss; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

916 
(* replace params in ids by params from axioms, 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

917 
adjust types in axioms *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

918 
val all_params' = params_of' elemss; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

919 
val all_params = param_types all_params'; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

920 
val elemss' = map (fn (((name, _), (ps, axs)), elems) => 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

921 
(((name, map (fn p => (p, assoc (all_params, p))) ps), axs), elems)) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

922 
elemss; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

923 
fun inst_ax th = let 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

924 
val {hyps, prop, ...} = Thm.rep_thm th; 
15570  925 
val ps = map (apsnd SOME) (Library.foldl Term.add_frees ([], prop :: hyps)); 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

926 
val [env] = unify_parms ctxt all_params [ps]; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

927 
val th' = inst_thm ctxt env th; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

928 
in th' end; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

929 
val final_elemss = map (fn ((id, axs), elems) => 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

930 
((id, map inst_ax axs), elems)) elemss'; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

931 
in (prev_idents @ idents, final_elemss) end; 
12046  932 

12510  933 
end; 
934 

12070  935 

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

936 
(* activate elements *) 
12273  937 

12510  938 
local 
939 

13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

940 
fun export_axioms axs _ hyps th = 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

941 
th > Drule.satisfy_hyps axs 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

942 
(* CB: replace metahyps, using axs, by a single metahyp. *) 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

943 
> Drule.implies_intr_list (Library.drop (length axs, hyps)) 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

944 
(* CB: turn remaining hyps into assumptions. *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

945 
> Seq.single 
12263  946 

14643  947 
fun activate_elem _ ((ctxt, axs), Fixes fixes) = 
948 
((ctxt > ProofContext.add_fixes fixes, axs), []) 

13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

949 
 activate_elem _ ((ctxt, axs), Assumes asms) = 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

950 
let 
15703  951 
val asms' = map_attrib_specs (Attrib.context_attribute_i ctxt) asms; 
952 
val ts = List.concat (map (map #1 o #2) asms'); 

953 
val (ps, qs) = splitAt (length ts, axs); 

13420  954 
val (ctxt', _) = 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

955 
ctxt > ProofContext.fix_frees ts 
15703  956 
> ProofContext.assume_i (export_axioms ps) asms'; 
13629  957 
in ((ctxt', qs), []) end 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

958 
 activate_elem _ ((ctxt, axs), Defines defs) = 
15596  959 
let 
15703  960 
val defs' = map_attrib_specs (Attrib.context_attribute_i ctxt) defs; 
15596  961 
val (ctxt', _) = 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

962 
ctxt > ProofContext.assume_i ProofContext.export_def 
15703  963 
(defs' > map (fn ((name, atts), (t, ps)) => 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

964 
let val (c, t') = ProofContext.cert_def ctxt t 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

965 
in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end)) 
13420  966 
in ((ctxt', axs), []) end 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

967 
 activate_elem is_ext ((ctxt, axs), Notes facts) = 
15596  968 
let 
15703  969 
val facts' = map_attrib_facts (Attrib.context_attribute_i ctxt) facts; 
970 
val (ctxt', res) = ctxt > ProofContext.note_thmss_i facts'; 

13420  971 
in ((ctxt', axs), if is_ext then res else []) end; 
12502  972 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

973 
fun activate_elems (((name, ps), axs), elems) ctxt = 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

974 
let val ((ctxt', _), res) = 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

975 
foldl_map (activate_elem (name = "")) ((ProofContext.qualified true ctxt, axs), elems) 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

976 
handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)] 
15696  977 
val ctxt'' = if name = "" then ctxt' 
978 
else let 

979 
val ps' = map (fn (n, SOME T) => Free (n, T)) ps; 

980 
val ctxt'' = put_local_registration (name, ps') ("", []) ctxt' 

981 
in foldl (fn (ax, ctxt) => 

982 
add_local_witness (name, ps') (Thm.assume (Thm.cprop_of ax)) ctxt) ctxt'' axs 

983 
end 

984 
in (ProofContext.restore_qualified ctxt ctxt'', res) end; 

13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

985 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

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

988 
val elems = map (prep_facts ctxt) raw_elems; 
15570  989 
val (ctxt', res) = apsnd List.concat (activate_elems (((name, ps), axs), elems) ctxt); 
15703  990 
val elems' = map (map_attrib_elem Args.closure) elems; 
991 
in (ctxt', (((name, ps), elems'), res)) end); 

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

992 

12546  993 
in 
994 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

995 
(* CB: activate_facts prep_facts (ctxt, elemss), 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

996 
where elemss is a list of pairs consisting of identifiers and 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

997 
context elements, extends ctxt by the context elements yielding 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

998 
ctxt' and returns (ctxt', (elemss', facts)). 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

999 
Identifiers in the argument are of the form ((name, ps), axs) and 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1000 
assumptions use the axioms in the identifiers to set up exporters 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1001 
in ctxt'. elemss' does not contain identifiers and is obtained 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1002 
from elemss and the intermediate context with prep_facts. 
15703  1003 
If read_facts or cert_facts is used for prep_facts, these also remove 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1004 
the internal/external markers from elemss. *) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1005 

13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

1006 
fun activate_facts prep_facts arg = 
15570  1007 
apsnd (apsnd List.concat o Library.split_list) (activate_elemss prep_facts arg); 
12546  1008 

15703  1009 
fun activate_note prep_facts (ctxt, args) = 
1010 
let 

1011 
val (ctxt', ([(_, [Notes args'])], facts)) = 

1012 
activate_facts prep_facts (ctxt, [((("", []), []), [Ext (Notes args)])]); 

1013 
in (ctxt', (args', facts)) end; 

1014 

12510  1015 
end; 
1016 

12307  1017 

15696  1018 
(* register elements *) 
1019 

1020 
fun register_elems (((_, ps), (((name, ax_ps), axs), _)), ctxt) = 

1021 
if name = "" then ctxt 

1022 
else let val ps' = map (fn (n, SOME T) => Free (n, T)) ax_ps 

1023 
val ctxt' = put_local_registration (name, ps') ("", []) ctxt 

1024 
in foldl (fn (ax, ctxt) => 

1025 
add_local_witness (name, ps') ax ctxt) ctxt' axs 

1026 
end; 

1027 

1028 
fun register_elemss id_elemss ctxt = 

1029 
foldl register_elems ctxt id_elemss; 

1030 

1031 

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

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

1033 

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

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

1035 

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

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

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

1038 
 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

1039 

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

1040 

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

1041 
(* parameters *) 
12502  1042 

1043 
local 

1044 

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

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

1046 
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

1047 
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

1048 

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

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

1050 

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

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

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

1053 

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

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

1055 

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

1056 

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

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

1058 

15596  1059 
(* flatten (ids, expr) normalises expr (which is either a locale 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1060 
expression or a single context element) wrt. 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1061 
to the list ids of already accumulated identifiers. 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1062 
It returns (ids', elemss) where ids' is an extension of ids 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1063 
with identifiers generated for expr, and elemss is the list of 
15596  1064 
context elements generated from expr. For details, see flatten_expr. 
1065 
Additionally, for a locale expression, the elems are grouped into a single 

1066 
Int; individual context elements are marked Ext. In this case, the 

1067 
identifierlike information of the element is as follows: 

1068 
 for Fixes: (("", ps), []) where the ps have type info NONE 

1069 
 for other elements: (("", []), []). 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1070 
The implementation of activate_facts relies on identifier names being 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1071 
empty strings for external elements. 
15596  1072 
*) 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1073 

859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1074 
fun flatten _ (ids, Elem (Fixes fixes)) = 
15696  1075 
(ids @ [(("", map #1 fixes), ([], []))], [((("", map (rpair NONE o #1) fixes), []), Ext (Fixes fixes))]) 
1076 
 flatten _ (ids, Elem elem) = (ids @ [(("", []), ([], []))], [((("", []), []), Ext elem)]) 

14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1077 
 flatten (ctxt, prep_expr) (ids, Expr expr) = 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1078 
apsnd (map (apsnd Int)) (flatten_expr ctxt (ids, prep_expr expr)); 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1079 

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

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

1081 

12839  1082 
local 
1083 

12727  1084 
fun declare_int_elem (ctxt, Fixes fixes) = 
12575  1085 
(ctxt > ProofContext.add_fixes (map (fn (x, T, mx) => 
15570  1086 
(x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes), []) 
12727  1087 
 declare_int_elem (ctxt, _) = (ctxt, []); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

1088 

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

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

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

1092 
 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

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

1094 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

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

1097 
(case elems of 
13308  1098 
Int es => foldl_map declare_int_elem (ctxt, es) 
12546  1099 
 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

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

12839  1103 
in 
1104 

14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

1105 
(* CB: only called by prep_elemss. *) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

1106 

12727  1107 
fun declare_elemss prep_fixes fixed_params raw_elemss ctxt = 
1108 
let 

14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

1109 
(* CB: fix of type bug of goal in target with context elements. 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

1110 
Parameters new in context elements must receive types that are 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

1111 
distinct from types of parameters in target (fixed_params). *) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

1112 
val ctxt_with_fixed = 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

1113 
ProofContext.declare_terms (map Free fixed_params) ctxt; 
12727  1114 
val int_elemss = 
1115 
raw_elemss 

15570  1116 
> List.mapPartial (fn (id, Int es) => SOME (id, es)  _ => NONE) 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

1117 
> unify_elemss ctxt_with_fixed fixed_params; 
12727  1118 
val (_, raw_elemss') = 
1119 
foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es))  x => x) 

1120 
(int_elemss, raw_elemss); 

1121 
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

1122 

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

1124 

12839  1125 
local 
1126 

15596  1127 
(* CB: normalise Assumes and Defines wrt. previous definitions *) 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1128 

12839  1129 
val norm_term = Envir.beta_norm oo Term.subst_atomic; 
1130 

15596  1131 
(* CB: following code (abstract_term, abstract_thm, bind_def) 
1132 
used in eval_text for Defines elements. *) 

1133 

13336  1134 
fun abstract_term eq = (*assumes wellformedness according to ProofContext.cert_def*) 
12839  1135 
let 
1136 
val body = Term.strip_all_body eq; 

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

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

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

13336  1140 
val eq' = Term.list_abs_free (map Term.dest_Free xs, rhs); 
1141 
in (Term.dest_Free f, eq') end; 

1142 

1143 
fun abstract_thm sign eq = 

1144 
Thm.assume (Thm.cterm_of sign eq) > Drule.gen_all > Drule.abs_def; 

12502  1145 

13336  1146 
fun bind_def ctxt (name, ps) ((xs, env, ths), eq) = 
12839  1147 
let 
13336  1148 
val ((y, T), b) = abstract_term eq; 
13308  1149 
val b' = norm_term env b; 
13336  1150 
val th = abstract_thm (ProofContext.sign_of ctxt) eq; 
13308  1151 
fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)]; 
12839  1152 
in 
13308  1153 
conditional (exists (equal y o #1) xs) (fn () => 
1154 
err "Attempt to define previously specified variable"); 

1155 
conditional (exists (fn (Free (y', _), _) => y = y'  _ => false) env) (fn () => 

1156 
err "Attempt to redefine variable"); 

13336  1157 
(Term.add_frees (xs, b'), (Free (y, T), b') :: env, th :: ths) 
12839  1158 
end; 
12575  1159 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1160 
(* CB: for finish_elems (Int and Ext) *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1161 

13308  1162 
fun eval_text _ _ _ (text, Fixes _) = text 
13394  1163 
 eval_text _ _ is_ext ((((exts, exts'), (ints, ints')), (xs, env, defs)), Assumes asms) = 
1164 
let 

15570  1165 
val ts = List.concat (map (map #1 o #2) asms); 
13394  1166 
val ts' = map (norm_term env) ts; 
1167 
val spec' = 

1168 
if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints')) 

1169 
else ((exts, exts'), (ints @ ts, ints' @ ts')); 

15570  1170 
in (spec', (Library.foldl Term.add_frees (xs, ts'), env, defs)) end 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1171 
 eval_text ctxt (id, _) _ ((spec, binds), Defines defs) = 
15570  1172 
(spec, Library.foldl (bind_def ctxt id) (binds, map (#1 o #2) defs)) 
13308  1173 
 eval_text _ _ _ (text, Notes _) = text; 
1174 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1175 
(* CB: for finish_elems (Ext) *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1176 

13308  1177 
fun closeup _ false elem = elem 
1178 
 closeup ctxt true elem = 

12839  1179 
let 
13308  1180 
fun close_frees t = 
1181 
let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1) 

1182 
(Term.add_frees ([], t))) 

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

1184 

1185 
fun no_binds [] = [] 

1186 
 no_binds _ = 

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

1188 
in 

1189 
(case elem of 

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

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

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

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

1194 
 e => e) 

1195 
end; 

12839  1196 

12502  1197 

12839  1198 
fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) => 
12727  1199 
(x, assoc_string (parms, x), mx)) fixes) 
12839  1200 
 finish_ext_elem _ close (Assumes asms, propp) = 
1201 
close (Assumes (map #1 asms ~~ propp)) 

1202 
 finish_ext_elem _ close (Defines defs, propp) = 

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

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1206 
(* CB: finish_parms introduces type info from parms to identifiers *) 
15531  1207 
(* CB: only needed for types that have been NONE so far??? 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1208 
If so, which are these??? *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1209 

09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1210 
fun finish_parms parms (((name, ps), axs), elems) = 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1211 
(((name, map (fn (x, _) => (x, assoc (parms, x))) ps), axs), elems); 
12839  1212 

13375  1213 
fun finish_elems ctxt parms _ (text, ((id, Int e), _)) = 
12839  1214 
let 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1215 
val [(id', es)] = unify_elemss ctxt parms [(id, e)]; 
15570  1216 
val text' = Library.foldl (eval_text ctxt id' false) (text, es); 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1217 
in (text', (id', map Int es)) end 
13375  1218 
 finish_elems ctxt parms do_close (text, ((id, Ext e), [propp])) = 
13308  1219 
let 
1220 
val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp); 

13375  1221 
val text' = eval_text ctxt id true (text, e'); 
13308  1222 
in (text', (id, [Ext e'])) end; 
12839  1223 

1224 
in 

12510  1225 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1226 
(* CB: only called by prep_elemss *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1227 

13375  1228 
fun finish_elemss ctxt parms do_close = 
1229 
foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close); 

12839  1230 

1231 
end; 

1232 

15127  1233 
(* CB: type inference and consistency checks for locales *) 
1234 

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

1236 
let 
15127  1237 
(* CB: contexts computed in the course of this function are discarded. 
1238 
They are used for type inference and consistency checks only. *) 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1239 
(* CB: fixed_params are the parameters (with types) of the target locale, 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1240 
empty list if there is no target. *) 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1241 
(* CB: raw_elemss are list of pairs consisting of identifiers and 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1242 
context elements, the latter marked as internal or external. *) 
12727  1243 
val (raw_ctxt, raw_proppss) = declare_elemss prep_fixes fixed_params raw_elemss context; 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1244 
(* CB: raw_ctxt is context with additional fixed variables derived from 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1245 
the fixes elements in raw_elemss, 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1246 
raw_proppss contains assumptions and definitions from the 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1247 
external elements in raw_elemss. *) 
15570  1248 
val raw_propps = map List.concat raw_proppss; 
1249 
val raw_propp = List.concat raw_propps; 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1250 

09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1251 
(* CB: add type information from fixed_params to context (declare_terms) *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1252 
(* CB: process patterns (conclusion and external elements only) *) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

1254 
prepp (ProofContext.declare_terms (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp); 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1255 
(* CB: add type information from conclusion and external elements 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1256 
to context *) 
15570  1257 
val ctxt = ProofContext.declare_terms (List.concat (map (map fst) all_propp)) ctxt; 
12502  1258 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1259 
(* CB: resolve schematic variables (patterns) in conclusion and external 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1260 
elements. *) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

1262 
(#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp))), map (map snd) all_propp); 
13629  1263 
val (concl, propp) = splitAt(length raw_concl, all_propp'); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

1264 
val propps = unflat raw_propps propp; 
12839  1265 
val proppss = map (uncurry unflat) (raw_proppss ~~ propps); 
12502  1266 

15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1267 
(* CB: obtain all parameters from identifier part of raw_elemss *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

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

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

1272 
val parms = param_types (xs ~~ typing); 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1273 
(* CB: parms are the parameters from raw_elemss, with correct typing. *) 
12273  1274 

14508 