author  wenzelm 
Fri, 17 Jun 2005 18:35:27 +0200  
changeset 16458  4c6fd0c01d28 
parent 16346  baa7b5324fc1 
child 16620  2a7f46324218 
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 

16169
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

21 
(* TODO: 
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

22 
 betaeta normalisation of interpretation parameters 
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

23 
 no beta reduction of interpretation witnesses 
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

24 
 dangling type frees in locales 
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

25 
*) 
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

26 

11896  27 
signature LOCALE = 
28 
sig 

12046  29 
type context 
15703  30 
datatype ('typ, 'term, 'fact) elem = 
12058  31 
Fixes of (string * 'typ option * mixfix option) list  
16169
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

32 
Constrains of (string * 'typ) list  
15703  33 
Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list  
34 
Defines of ((string * Attrib.src list) * ('term * 'term list)) list  

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

12273  36 
datatype expr = 
37 
Locale of string  

16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

38 
Rename of expr * (string * mixfix option) option list  
12273  39 
Merge of expr list 
40 
val empty: expr 

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

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

42 

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

43 
(* Abstract interface to locales *) 
15703  44 
type element 
45 
type element_i 

12046  46 
type locale 
16458  47 
val intern: theory > xstring > string 
48 
val extern: theory > string > xstring 

12502  49 
val the_locale: theory > string > locale 
15703  50 
val intern_attrib_elem: theory > 
51 
('typ, 'term, 'fact) elem > ('typ, 'term, 'fact) elem 

52 
val intern_attrib_elem_expr: theory > 

53 
('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

54 

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

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

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

59 
(term * (term list * term list)) list list 
15703  60 
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

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

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

63 
(term * (term list * term list)) list list 
15596  64 

65 
(* Diagnostic functions *) 

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

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

70 
val print_local_registrations: string > context > unit 
15596  71 

15696  72 
(* Storing results *) 
15703  73 
val add_locale: bool > bstring > expr > element list > theory > theory 
74 
val add_locale_i: bool > bstring > expr > element_i list > theory > theory 

75 
val smart_note_thmss: string > string option > 

12958  76 
((bstring * theory attribute list) * (thm list * theory attribute list) list) list > 
77 
theory > theory * (bstring * thm list) list 

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

12711  80 
theory > theory * (bstring * thm list) list 
15703  81 
val note_thmss_i: string > string > 
82 
((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list > 

12711  83 
theory > theory * (bstring * thm list) list 
15703  84 
val add_thmss: string > string > ((string * thm list) * Attrib.src list) list > 
13375  85 
theory * context > (theory * context) * (string * thm list) list 
15596  86 

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

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

88 
val prep_global_registration: 
15703  89 
string * Attrib.src list > expr > string option list > theory > 
15596  90 
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

91 
val prep_local_registration: 
15703  92 
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

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

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

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

97 
string * term list > thm > context > context 
11896  98 
end; 
12839  99 

12289  100 
structure Locale: LOCALE = 
11896  101 
struct 
102 

12273  103 
(** locale elements and expressions **) 
11896  104 

12014  105 
type context = ProofContext.context; 
11896  106 

15703  107 
datatype ('typ, 'term, 'fact) elem = 
12058  108 
Fixes of (string * 'typ option * mixfix option) list  
16169
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

109 
Constrains of (string * 'typ) list  
15703  110 
Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list  
111 
Defines of ((string * Attrib.src list) * ('term * 'term list)) list  

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

12273  113 

114 
datatype expr = 

115 
Locale of string  

16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

116 
Rename of expr * (string * mixfix option) option list  
12273  117 
Merge of expr list; 
11896  118 

12273  119 
val empty = Merge []; 
120 

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

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

122 
Elem of 'a  Expr of expr; 
12273  123 

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

12070  126 

127 
type locale = 

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

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

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

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

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

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

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

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

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

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

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

138 
import: expr, (*dynamic import*) 
15703  139 
elems: (element_i * stamp) list, (*static content*) 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

140 
params: ((string * typ option) * mixfix option) list * string list} 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

141 
(*all/local params*) 
12063  142 

11896  143 

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

146 

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

148 

149 

150 

15837  151 
(** term and type instantiation, using symbol tables **) 
152 

153 
(* instantiate TFrees *) 

154 

155 
fun tinst_tab_type tinst T = if Symtab.is_empty tinst 

156 
then T 

157 
else Term.map_type_tfree 

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

159 

160 
fun tinst_tab_term tinst t = if Symtab.is_empty tinst 

161 
then t 

162 
else Term.map_term_types (tinst_tab_type tinst) t; 

163 

16458  164 
fun tinst_tab_thm thy tinst thm = if Symtab.is_empty tinst 
15837  165 
then thm 
166 
else let 

16458  167 
val cert = Thm.cterm_of thy; 
168 
val certT = Thm.ctyp_of thy; 

15837  169 
val {hyps, prop, ...} = Thm.rep_thm thm; 
170 
val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps); 

171 
val tinst' = Symtab.dest tinst > 

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

173 
in 

174 
if null tinst' then thm 

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

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

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

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

179 
[])) 

180 
> (fn th => Drule.implies_elim_list th 

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

182 
end; 

183 

184 

185 
(* instantiate TFrees and Frees *) 

186 

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

188 
then tinst_tab_term tinst 

189 
else (* instantiate terms and types simultaneously *) 

190 
let 

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

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

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

194 
 SOME t => t) 

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

196 
 instf (b as Bound _) = b 

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

198 
 instf (s $ t) = instf s $ instf t 

199 
in instf end; 

200 

16458  201 
fun inst_tab_thm thy (inst, tinst) thm = if Symtab.is_empty inst 
202 
then tinst_tab_thm thy tinst thm 

15837  203 
else let 
16458  204 
val cert = Thm.cterm_of thy; 
205 
val certT = Thm.ctyp_of thy; 

15837  206 
val {hyps, prop, ...} = Thm.rep_thm thm; 
207 
(* type instantiations *) 

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

209 
val tinst' = Symtab.dest tinst > 

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

211 
(* term instantiations; 

212 
note: lhss are type instantiated, because 

213 
type insts will be done first*) 

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

215 
val inst' = Symtab.dest inst > 

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

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

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

219 
else NONE) frees); 

220 
in 

16458  221 
if null tinst' andalso null inst' then tinst_tab_thm thy tinst thm 
15837  222 
else thm > Drule.implies_intr_list (map cert hyps) 
223 
> Drule.tvars_intr_list (map #1 tinst') 

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

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

226 
[])) 

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

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

229 
> (fn th => Drule.implies_elim_list th 

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

231 
end; 

232 

233 

234 
(** registration management **) 

11896  235 

15837  236 
structure Registrations : 
237 
sig 

238 
type T 

239 
val empty: T 

240 
val join: T * T > T 

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

16458  242 
val lookup: theory > T * term list > 
15837  243 
((string * Attrib.src list) * thm list) option 
16458  244 
val insert: theory > term list * (string * Attrib.src list) > T > 
15837  245 
T * (term list * ((string * Attrib.src list) * thm list)) list 
246 
val add_witness: term list > thm > T > T 

247 
end = 

248 
struct 

249 
(* a registration consists of theorems instantiating locale assumptions 

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

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

252 

253 
val empty = Termtab.empty; 

254 

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

256 
fun termify ts = 

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

258 
fun untermify t = 

259 
let fun ut (Const _) ts = ts 

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

261 
in ut t [] end; 

262 

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

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

16458  265 
fun join (r1, r2) = Termtab.join (fn _ => fn (reg, _) => SOME reg) (r1, r2); 
15837  266 

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

268 

269 
(* registrations that subsume t *) 

270 
fun subsumers tsig t regs = 

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

272 

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

274 
fun lookup sign (regs, ts) = 

275 
let 

276 
val tsig = Sign.tsig_of sign; 

277 
val t = termify ts; 

278 
val subs = subsumers tsig t regs; 

279 
in (case subs of 

280 
[] => NONE 

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

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

283 
(* thms contain Frees, not Vars *) 

284 
val tinst' = tinst > Vartab.dest 

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

286 
> Symtab.make; 

287 
val inst' = inst > Vartab.dest 

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

289 
> Symtab.make; 

290 
in 

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

292 
end) 

293 
end; 

294 

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

296 
additionally returns registrations that are strictly subsumed *) 

297 
fun insert sign (ts, attn) regs = 

298 
let 

299 
val tsig = Sign.tsig_of sign; 

300 
val t = termify ts; 

301 
val subs = subsumers tsig t regs ; 

302 
in (case subs of 

303 
[] => let 

304 
val sups = 

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

306 
val sups' = map (apfst untermify) sups 

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

308 
 _ => (regs, [])) 

309 
end; 

310 

311 
(* add witness theorem to registration, 

16169
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

312 
only if instantiation is exact, otherwise exception Option raised *) 
15837  313 
fun add_witness ts thm regs = 
314 
let 

315 
val t = termify ts; 

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

317 
in 

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

319 
end; 

320 
end; 

321 

322 
(** theory data **) 

15596  323 

16458  324 
structure GlobalLocalesData = TheoryDataFun 
325 
(struct 

12014  326 
val name = "Isar/locales"; 
15837  327 
type T = NameSpace.T * locale Symtab.table * Registrations.T Symtab.table; 
15596  328 
(* 1st entry: locale namespace, 
329 
2nd entry: locales of the theory, 

15837  330 
3rd entry: registrations, indexed by locale name *) 
11896  331 

15596  332 
val empty = (NameSpace.empty, Symtab.empty, Symtab.empty); 
12063  333 
val copy = I; 
16458  334 
val extend = I; 
12289  335 

16458  336 
fun join_locs _ ({predicate, import, elems, params}: locale, 
15596  337 
{elems = elems', ...}: locale) = 
338 
SOME {predicate = predicate, import = import, 

339 
elems = gen_merge_lists eq_snd elems elems', 

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

340 
params = params}; 
16458  341 
fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) = 
15596  342 
(NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2), 
16458  343 
Symtab.join (K (SOME o Registrations.join)) (regs1, regs2)); 
12289  344 

15596  345 
fun print _ (space, locs, _) = 
16346  346 
Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs))) 
12014  347 
> Pretty.writeln; 
16458  348 
end); 
11896  349 

15801  350 
val _ = Context.add_setup [GlobalLocalesData.init]; 
351 

352 

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

353 

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

354 
(** context data **) 
11896  355 

16458  356 
structure LocalLocalesData = ProofDataFun 
357 
(struct 

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

358 
val name = "Isar/locales"; 
15837  359 
type T = Registrations.T Symtab.table; 
360 
(* registrations, indexed by locale name *) 

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

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

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

364 

15801  365 
val _ = Context.add_setup [LocalLocalesData.init]; 
12289  366 

12277  367 

368 
(* access locales *) 

369 

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

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

371 

16458  372 
val intern = NameSpace.intern o #1 o GlobalLocalesData.get; 
373 
val extern = NameSpace.extern o #1 o GlobalLocalesData.get; 

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

374 

16144  375 
fun declare_locale name thy = 
376 
thy > GlobalLocalesData.map (fn (space, locs, regs) => 

16458  377 
(Sign.declare_name thy name space, locs, regs)); 
11896  378 

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

380 
GlobalLocalesData.map (fn (space, locs, regs) => 
15596  381 
(space, Symtab.update ((name, loc), locs), regs)); 
382 

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

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

12014  385 
fun the_locale thy name = 
386 
(case get_locale thy name of 

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

11896  389 

12046  390 

15596  391 
(* access registrations *) 
392 

15696  393 
(* Ids of global registrations are varified, 
394 
Ids of local registrations are not. 

395 
Thms of registrations are never varified. *) 

396 

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

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

398 

15696  399 
fun gen_get_registrations get thy_ctxt name = 
400 
case Symtab.lookup (get thy_ctxt, name) of 

401 
NONE => [] 

15837  402 
 SOME reg => Registrations.dest reg; 
15696  403 

404 
val get_global_registrations = 

405 
gen_get_registrations (#3 o GlobalLocalesData.get); 

406 
val get_local_registrations = 

407 
gen_get_registrations LocalLocalesData.get; 

408 

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

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

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

413 

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

414 
val get_global_registration = 
16458  415 
gen_get_registration (#3 o GlobalLocalesData.get) I; 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

416 
val get_local_registration = 
16458  417 
gen_get_registration LocalLocalesData.get ProofContext.theory_of; 
15596  418 

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

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

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

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

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

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

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

425 
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

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

427 

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

428 

15837  429 
(* 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

430 

16458  431 
fun gen_put_registration map_data thy_of (name, ps) attn thy_ctxt = 
15837  432 
map_data (fn regs => 
433 
let 

16458  434 
val thy = thy_of thy_ctxt; 
15837  435 
val reg = getOpt (Symtab.lookup (regs, name), Registrations.empty); 
16458  436 
val (reg', sups) = Registrations.insert thy (ps, attn) reg; 
15837  437 
val _ = if not (null sups) then warning 
438 
("Subsumed interpretation(s) of locale " ^ 

16458  439 
quote (extern thy name) ^ 
15837  440 
"\nby interpretation(s) with the following prefix(es):\n" ^ 
441 
commas_quote (map (fn (_, ((s, _), _)) => s) sups)) 

442 
else (); 

443 
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

444 

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

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

446 
gen_put_registration (fn f => 
16458  447 
GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, f regs))) I; 
15837  448 
val put_local_registration = 
16458  449 
gen_put_registration LocalLocalesData.map ProofContext.theory_of; 
15596  450 

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

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

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

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

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

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

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

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

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

462 

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

463 
(* add witness theorem to registration in theory or context, 
15596  464 
ignored if registration not present *) 
465 

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

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

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

468 
let 
15837  469 
val reg = valOf (Symtab.lookup (regs, name)); 
15596  470 
in 
15837  471 
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

472 
end handle Option => regs); 
15596  473 

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

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

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

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

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

478 
val add_local_witness = gen_add_witness LocalLocalesData.map; 
15596  479 

480 

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

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

482 
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

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

484 

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

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

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

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

488 
(case get_locale thy name of 
15531  489 
NONE => false 
490 
 SOME {import, ...} => imps import low) 

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

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

492 
 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

493 
in 
16458  494 
imps (Locale (intern thy upper)) (intern thy lower) 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

496 

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

497 

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

498 
(* printing of registrations *) 
15596  499 

15703  500 
fun gen_print_registrations get_regs mk_ctxt msg loc thy_ctxt = 
15596  501 
let 
15703  502 
val ctxt = mk_ctxt thy_ctxt; 
503 
val thy = ProofContext.theory_of ctxt; 

504 

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

506 
val prt_atts = Args.pretty_attribs ctxt; 

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

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

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

15837  510 
Pretty.block ( 
511 
(Pretty.breaks (Pretty.str prfx :: prt_atts atts) @ 

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

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

15703  514 

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

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

519 
(case loc_regs of 

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

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

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

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

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

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

526 
end) 
15596  527 
> Pretty.writeln 
528 
end; 

529 

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

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

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

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

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

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

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

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

539 

15596  540 

12277  541 
(* diagnostics *) 
12273  542 

12277  543 
fun err_in_locale ctxt msg ids = 
544 
let 

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

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

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

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

12063  554 

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

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

556 

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

557 
fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids'); 
12277  558 

559 

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

560 
(** primitives **) 
12046  561 

15703  562 
(* map elements *) 
563 

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

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

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

16169
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

567 
 Constrains csts => Constrains (csts > map (fn (x, T) => 
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

568 
let val (x', _) = var (x, SOME Syntax.NoSyn) in (x', typ T) end)) 
15703  569 
 Assumes asms => Assumes (asms > map (fn ((a, atts), propps) => 
570 
((name a, map attrib atts), propps > map (fn (t, (ps, qs)) => 

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

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

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

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

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

576 

577 
fun map_values typ term thm = map_elem 

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

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

580 

581 

582 
(* map attributes *) 

583 

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

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

586 

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

588 

16458  589 
fun intern_attrib_elem thy = map_attrib_elem (Attrib.intern_src thy); 
15703  590 

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

592 
 intern_attrib_elem_expr _ (Expr expr) = Expr expr; 

593 

594 

12277  595 
(* renaming *) 
12263  596 

16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

597 
(* ren maps names to (new) names and syntax; represented as association list *) 
12263  598 

15703  599 
fun rename_var ren (x, mx) = 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

600 
case assoc_string (ren, x) of 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

601 
NONE => (x, mx) 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

602 
 SOME (x', NONE) => 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

603 
(x', if mx = NONE then mx else SOME Syntax.NoSyn) (*drop syntax*) 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

604 
 SOME (x', SOME mx') => 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

605 
if mx = NONE then raise ERROR_MESSAGE 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

606 
("Attempt to change syntax of structure parameter " ^ quote x) 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

607 
else (x', SOME mx'); (*change syntax*) 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

608 

c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

609 
fun rename ren x = 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

610 
case assoc_string (ren, x) of 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

611 
NONE => x 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

612 
 SOME (x', _) => x'; (*ignore syntax*) 
15703  613 

12263  614 
fun rename_term ren (Free (x, T)) = Free (rename ren x, T) 
615 
 rename_term ren (t $ u) = rename_term ren t $ rename_term ren u 

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

617 
 rename_term _ a = a; 

618 

619 
fun rename_thm ren th = 

620 
let 

16458  621 
val {thy, hyps, prop, maxidx, ...} = Thm.rep_thm th; 
622 
val cert = Thm.cterm_of thy; 

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

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

627 
in 

628 
if xs = xs' then th 

629 
else 

630 
th 

631 
> Drule.implies_intr_list (map cert hyps) 

632 
> Drule.forall_intr_list (cert_frees xs) 

633 
> Drule.forall_elim_list (cert_vars xs) 

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

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

636 
end; 

637 

15703  638 
fun rename_elem ren = 
639 
map_values I (rename_term ren) (rename_thm ren) o 

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

12263  641 

16144  642 
fun rename_facts prfx = 
643 
map_elem {var = I, typ = I, term = I, fact = I, attrib = I, name = NameSpace.qualified prfx}; 

12307  644 

12263  645 

12502  646 
(* type instantiation *) 
647 

648 
fun inst_type [] T = T 

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

651 
fun inst_term [] t = t 

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

653 

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

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

655 
 inst_thm ctxt env th = 
12502  656 
let 
16458  657 
val thy = ProofContext.theory_of ctxt; 
658 
val cert = Thm.cterm_of thy; 

659 
val certT = Thm.ctyp_of thy; 

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

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

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

665 
else 

666 
th 

667 
> Drule.implies_intr_list (map cert hyps) 

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

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

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

674 
end; 

675 

15703  676 
fun inst_elem ctxt env = 
677 
map_values (inst_type env) (inst_term env) (inst_thm ctxt env); 

12502  678 

679 

15696  680 
(* term and type instantiation, variant using symbol tables *) 
681 

682 
(* instantiate TFrees *) 

683 

16458  684 
fun tinst_tab_elem thy tinst = 
685 
map_values (tinst_tab_type tinst) (tinst_tab_term tinst) (tinst_tab_thm thy tinst); 

15749  686 

15696  687 
(* instantiate TFrees and Frees *) 
688 

16458  689 
fun inst_tab_elem thy (inst as (_, tinst)) = 
690 
map_values (tinst_tab_type tinst) (inst_tab_term inst) (inst_tab_thm thy inst); 

15696  691 

16458  692 
fun inst_tab_elems thy inst ((n, ps), elems) = 
693 
((n, map (inst_tab_term inst) ps), map (inst_tab_elem thy inst) elems); 

15696  694 

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

695 

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

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

697 

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

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

699 

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

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

701 
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

702 

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

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

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

706 
val tfrees = map TFree 
14695  707 
(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

708 
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

709 

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

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

711 
let 
15531  712 
fun paramify (i, NONE) = (i, NONE) 
713 
 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

714 

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

715 
val (maxidx', Ts') = foldl_map paramify (maxidx, Ts); 
12727  716 
val (maxidx'', Us') = foldl_map paramify (maxidx', Us); 
16458  717 
val tsig = Sign.tsig_of (ProofContext.theory_of ctxt); 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

718 

15531  719 
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

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

721 
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

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

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

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

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

727 

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

16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

730 
fun params_syn_of syn elemss = 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

731 
gen_distinct eq_fst (List.concat (map (snd o fst) elemss)) > 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

732 
map (apfst (fn x => (x, valOf (Symtab.lookup (syn, x))))); 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

733 

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

734 

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

735 
(* CB: param_types has the following type: 
15531  736 
('a * 'b option) list > ('a * 'b) list *) 
15570  737 
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

738 

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

739 

16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

740 
fun merge_syntax ctxt ids ss = Symtab.merge (op =) ss 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

741 
handle Symtab.DUPS xs => err_in_locale ctxt 
16105  742 
("Conflicting syntax for parameter(s): " ^ commas_quote xs) (map fst ids); 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

743 

c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

744 

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

745 
(* flatten expressions *) 
11896  746 

12510  747 
local 
12502  748 

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

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

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

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

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

753 

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

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

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

756 
val param_decls = 
15570  757 
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

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

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

760 
(case find_first (fn (_, ids) => length ids > 1) param_decls of 
15531  761 
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

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

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

765 

16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

766 
fun unify_parms ctxt (fixed_parms : (string * typ) list) 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

767 
(raw_parmss : (string * typ option) list list) = 
12502  768 
let 
16458  769 
val thy = ProofContext.theory_of ctxt; 
770 
val tsig = Sign.tsig_of thy; 

12502  771 
val maxidx = length raw_parmss; 
772 
val idx_parmss = (0 upto maxidx  1) ~~ raw_parmss; 

773 

774 
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

775 
fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps); 
15570  776 
val parms = fixed_parms @ List.concat (map varify_parms idx_parmss); 
12502  777 

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

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

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

780 
handle Type.TUNIFY => 
16458  781 
let val prt = Sign.string_of_typ thy 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

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

784 
end 
15570  785 
fun unify_list (envir, T :: Us) = Library.foldl (unify T) (envir, Us) 
12502  786 
 unify_list (envir, []) = envir; 
15570  787 
val (unifier, _) = Library.foldl unify_list 
12502  788 
((Vartab.empty, maxidx), map #2 (Symtab.dest (Symtab.make_multi parms))); 
789 

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

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

792 

793 
fun inst_parms (i, ps) = 

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

794 
foldr Term.add_typ_tfrees [] (List.mapPartial snd ps) 
15570  795 
> List.mapPartial (fn (a, S) => 
12502  796 
let val T = Envir.norm_type unifier' (TVar ((a, i), S)) 
15531  797 
in if T = TFree (a, S) then NONE else SOME ((a, S), T) end) 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

798 
in map inst_parms idx_parmss end : ((string * Term.sort) * Term.typ) list list; 
12502  799 

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

800 
in 
12502  801 

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

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

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

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

806 
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

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

809 
map (inst_thm ctxt env) axs), map (inst_elem ctxt env) elems); 
12839  810 
in map inst (elemss ~~ envs) end; 
12502  811 

16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

812 
(* like unify_elemss, but does not touch axioms, 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

813 
additional parameter for enforcing further constraints (eg. syntax) *) 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

814 

c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

815 
fun unify_elemss' _ _ [] [] = [] 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

816 
 unify_elemss' _ [] [elems] [] = [elems] 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

817 
 unify_elemss' ctxt fixed_parms elemss c_parms = 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

818 
let 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

819 
val envs = unify_parms ctxt fixed_parms (map (#2 o #1 o #1) elemss @ map single c_parms); 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

820 
fun inst ((((name, ps), axs), elems), env) = 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

821 
(((name, map (apsnd (Option.map (inst_type env))) ps), axs), 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

822 
map (inst_elem ctxt env) elems); 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

823 
in map inst (elemss ~~ (Library.take (length elemss, envs))) end; 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

824 

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

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

828 
identifier). 

829 

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

831 
((name, ps), (ax_ps, axs)) 

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

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

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

835 
hence axioms may contain additional parameters from later fragments: 

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

837 

838 
Elements are enriched by identifierlike information: 

839 
(((name, ax_ps), axs), elems) 

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

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

842 
typeinstantiated. 

843 

844 
*) 

845 

16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

846 
fun flatten_expr ctxt ((prev_idents, prev_syntax), expr) = 
12014  847 
let 
848 
val thy = ProofContext.theory_of ctxt; 

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

851 
of axioms *) 

12263  852 

15531  853 
fun renaming (SOME x :: xs) (y :: ys) = (y, x) :: renaming xs ys 
854 
 renaming (NONE :: xs) (y :: ys) = renaming xs ys 

12273  855 
 renaming [] _ = [] 
12289  856 
 renaming xs [] = raise ERROR_MESSAGE ("Too many arguments in renaming: " ^ 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

857 
commas (map (fn NONE => "_"  SOME x => quote (fst x)) xs)); 
12289  858 

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

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

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

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

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

12263  866 

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

867 
fun identify top (Locale name) = 
15596  868 
(* 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

869 
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

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

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

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

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

875 
the_locale thy name; 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

876 
val ps = map (#1 o #1) (#1 params); 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

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

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

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

880 
val ids_ax = if top then snd 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

881 
(* get the right axioms, only if at top level *) 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

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

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

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

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

888 
else ids''; 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

889 
val syn = Symtab.make (map (apfst fst) (#1 params)); 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

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

891 
 identify top (Rename (e, xs)) = 
12273  892 
let 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

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

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

896 
val ids'' = gen_distinct eq_fst (map (rename_parms top ren) ids'); 
15570  897 
val parms'' = distinct (List.concat (map (#2 o #1) ids'')); 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

898 
val syn'' = syn' > Symtab.dest > map (rename_var ren) > 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

899 
Symtab.make; 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

900 
(* check for conflicting syntax? *) 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

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

902 
 identify top (Merge es) = 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

903 
Library.foldl (fn ((ids, parms, syn), e) => let 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

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

905 
in (gen_merge_lists eq_fst ids ids', 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

906 
merge_lists parms parms', 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

907 
merge_syntax ctxt ids' (syn, syn')) end) 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

908 
(([], [], Symtab.empty), es); 
12014  909 

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

910 
(* CB: enrich identifiers by parameter types and 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

911 
the corresponding elements (with renamed parameters), 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

912 
also takes care of parameter syntax *) 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

913 

16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

914 
fun eval syn ((name, xs), axs) = 
12273  915 
let 
13308  916 
val {params = (ps, qs), elems, ...} = the_locale thy name; 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

917 
val ps' = map #1 ps; 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

918 
val ren = map #1 ps' ~~ 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

919 
map (fn x => (x, valOf (Symtab.lookup (syn, x)))) xs; 
13308  920 
val (params', elems') = 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

921 
if null ren then ((ps', qs), map #1 elems) 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

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

925 
in (((name, params'), axs), elems'') end; 
12307  926 

16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

927 
(* type constraint for renamed parameter with syntax *) 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

928 
fun type_syntax NONE = NONE 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

929 
 type_syntax (SOME mx) = let 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

930 
val Ts = map (fn x => TFree (x, [])) (Term.invent_names [] "'mxa" 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

931 
(Syntax.mixfix_args mx + 1)) 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

932 
in Ts > Library.split_last > op > > SOME end; 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

933 

c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

934 
(* compute identifiers and syntax, merge with previous ones *) 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

935 
val (ids, _, syn) = identify true expr; 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

936 
val idents = gen_rems eq_fst (ids, prev_idents); 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

937 
val syntax = merge_syntax ctxt ids (syn, prev_syntax); 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

938 
(* add types to params, check for unique params and unify them *) 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

939 
val raw_elemss = unique_parms ctxt (map (eval syntax) idents); 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

940 
val elemss = unify_elemss' ctxt [] raw_elemss 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

941 
(map (apsnd type_syntax) (Symtab.dest syntax)); 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

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

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

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

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

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

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

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

950 
val {hyps, prop, ...} = Thm.rep_thm th; 
15570  951 
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

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

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

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

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

956 
((id, map inst_ax axs), elems)) elemss'; 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

957 
in ((prev_idents @ idents, syntax), final_elemss) end; 
12046  958 

12510  959 
end; 
960 

12070  961 

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

962 
(* activate elements *) 
12273  963 

12510  964 
local 
965 

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

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

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

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

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

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

971 
> Seq.single 
12263  972 

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

16169
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

975 
 activate_elem _ ((ctxt, axs), Constrains _) = ((ctxt, axs), []) 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

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

977 
let 
15703  978 
val asms' = map_attrib_specs (Attrib.context_attribute_i ctxt) asms; 
979 
val ts = List.concat (map (map #1 o #2) asms'); 

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

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

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

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

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

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

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

994 
 activate_elem is_ext ((ctxt, axs), Notes facts) = 
15596  995 
let 
15703  996 
val facts' = map_attrib_facts (Attrib.context_attribute_i ctxt) facts; 
997 
val (ctxt', res) = ctxt > ProofContext.note_thmss_i facts'; 

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

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

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

1001 
let val ((ctxt', _), res) = 
16144  1002 
foldl_map (activate_elem (name = "")) ((ProofContext.qualified_names ctxt, axs), elems) 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

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

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

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

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

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

1010 
end 

16144  1011 
in (ProofContext.restore_naming ctxt ctxt'', res) end; 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

1012 

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

1013 
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

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

1015 
val elems = map (prep_facts ctxt) raw_elems; 
15570  1016 
val (ctxt', res) = apsnd List.concat (activate_elems (((name, ps), axs), elems) ctxt); 
15703  1017 
val elems' = map (map_attrib_elem Args.closure) elems; 
1018 
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

1019 

12546  1020 
in 
1021 

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

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

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

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

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

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

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

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

1029 
from elemss and the intermediate context with prep_facts. 
15703  1030 
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

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

1032 

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

1033 
fun activate_facts prep_facts arg = 
15570  1034 
apsnd (apsnd List.concat o Library.split_list) (activate_elemss prep_facts arg); 
12546  1035 

15703  1036 
fun activate_note prep_facts (ctxt, args) = 
1037 
let 

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

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

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

1041 

12510  1042 
end; 
1043 

12307  1044 

15696  1045 
(* register elements *) 
1046 

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

1048 
if name = "" then ctxt 

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

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

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

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

1053 
end; 

1054 

1055 
fun register_elemss id_elemss ctxt = 

1056 
foldl register_elems ctxt id_elemss; 

1057 

1058 

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

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

1060 

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

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

1062 

16458  1063 
fun intern_expr thy (Locale xname) = Locale (intern thy xname) 
1064 
 intern_expr thy (Merge exprs) = Merge (map (intern_expr thy) exprs) 

1065 
 intern_expr thy (Rename (expr, xs)) = Rename (intern_expr thy expr, xs); 

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

1066 

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

1067 

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

1068 
(* parameters *) 
12502  1069 

1070 
local 

1071 

16169
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

1072 
fun prep_parms prep_vars ctxt parms = 
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

1073 
let val vars = snd (foldl_map prep_vars (ctxt, map (fn (x, T) => ([x], T)) parms)) 
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

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

1075 

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

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

1077 

16169
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

1078 
fun read_parms x = prep_parms ProofContext.read_vars x; 
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

1079 
fun cert_parms x = prep_parms ProofContext.cert_vars x; 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

1080 

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

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

1082 

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

1083 

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

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

1085 

16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

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

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

1088 
to the list ids of already accumulated identifiers. 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

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

1090 
with identifiers generated for expr, and elemss is the list of 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

1091 
context elements generated from expr. 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

1092 
syn and syn' are symtabs mapping parameter names to their syntax. syn' 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

1093 
is an extension of syn. 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

1094 
For details, see flatten_expr. 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

1095 

15596  1096 
Additionally, for a locale expression, the elems are grouped into a single 
1097 
Int; individual context elements are marked Ext. In this case, the 

1098 
identifierlike information of the element is as follows: 

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

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

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

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

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

1104 

16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

1105 
fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

1106 
val ids' = ids @ [(("", map #1 fixes), ([], []))] 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

1107 
in 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

1108 
((ids', 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

1109 
merge_syntax ctxt ids' 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

1110 
(syn, Symtab.make (map (fn fx => (#1 fx, #3 fx)) fixes)) 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

1111 
handle Symtab.DUPS xs => err_in_locale ctxt 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

1112 
("Conflicting syntax for parameters: " ^ commas_quote xs) 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

1113 
(map #1 ids')), 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

1114 
[((("", map (rpair NONE o #1) fixes), []), Ext (Fixes fixes))]) 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

1115 
end 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

1116 
 flatten _ ((ids, syn), Elem elem) = 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

1117 
((ids @ [(("", []), ([], []))], syn), [((("", []), []), Ext elem)]) 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

1118 
 flatten (ctxt, prep_expr) ((ids, syn), Expr expr) = 
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

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

1120 

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

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

1122 

12839  1123 
local 
1124 

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

1129 

16169
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

1130 
fun declare_ext_elem prep_parms (ctxt, Fixes fixes) = 
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

1131 
let 
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

1132 
val parms = map (fn (x, T, _) => (x, T)) fixes; 
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

1133 
val parms' = prep_parms ctxt parms; 
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

1134 
val fixes' = map (fn ((x, T), (_, _, mx)) => (x, T, mx)) (parms' ~~ fixes); 
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

1135 
in (ctxt > ProofContext.add_fixes fixes', []) end 
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

1136 
 declare_ext_elem prep_parms (ctxt, Constrains csts) = 
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

1137 
let 
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

1138 
val parms = map (fn (x, T) => (x, SOME T)) csts; 
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

1139 
val parms' = prep_parms ctxt parms; 
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

1140 
val ts = map (fn (x, SOME T) => Free (x, T)) parms'; 
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

1141 
in (Library.fold ProofContext.declare_term ts ctxt, []) end 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

1143 
 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

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

1145 

16169
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

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

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

1148 
(case elems of 
13308  1149 
Int es => foldl_map declare_int_elem (ctxt, es) 
16169
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

1150 
 Ext e => foldl_map (declare_ext_elem prep_parms) (ctxt, [e])) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

12839  1154 
in 
1155 

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

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

1157 

16169
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

1158 
fun declare_elemss prep_parms fixed_params raw_elemss ctxt = 
12727  1159 
let 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

1160 
(* 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

1161 
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

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

1163 
val ctxt_with_fixed = 
16028  1164 
fold ProofContext.declare_term (map Free fixed_params) ctxt; 
12727  1165 
val int_elemss = 
1166 
raw_elemss 

15570  1167 
> 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

1168 
> unify_elemss ctxt_with_fixed fixed_params; 
12727  1169 
val (_, raw_elemss') = 
1170 
foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es))  x => x) 

1171 
(int_elemss, raw_elemss); 

16169
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

1172 
in foldl_map (declare_elems prep_parms) (ctxt, raw_elemss') end; 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

1173 

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

1175 

12839  1176 
local 
1177 

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

1179 

12839  1180 
val norm_term = Envir.beta_norm oo Term.subst_atomic; 
1181 

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

1184 

13336  1185 
fun abstract_term eq = (*assumes wellformedness according to ProofContext.cert_def*) 
12839  1186 
let 
1187 
val body = Term.strip_all_body eq; 

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

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

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

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

1193 

16458  1194 
fun abstract_thm thy eq = 
1195 
Thm.assume (Thm.cterm_of thy eq) > Drule.gen_all > Drule.abs_def; 

12502  1196 

13336  1197 
fun bind_def ctxt (name, ps) ((xs, env, ths), eq) = 
12839  1198 
let 
13336  1199 
val ((y, T), b) = abstract_term eq; 
13308  1200 
val b' = norm_term env b; 
16458  1201 
val th = abstract_thm (ProofContext.theory_of ctxt) eq; 
13308  1202 
fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)]; 
12839  1203 
in 
13308  1204 
conditional (exists (equal y o #1) xs) (fn () => 
1205 
err "Attempt to define previously specified variable"); 

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

1207 
err "Attempt to redefine variable"); 

13336  1208 
(Term.add_frees (xs, b'), (Free (y, T), b') :: env, th :: ths) 
12839  1209 
end; 
12575  1210 

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

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

1212 

13308  1213 
fun eval_text _ _ _ (text, Fixes _) = text 
16169
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

1214 
 eval_text _ _ _ (text, Constrains _) = text 
13394  1215 
 eval_text _ _ is_ext ((((exts, exts'), (ints, ints')), (xs, env, defs)), Assumes asms) = 
1216 
let 

15570  1217 
val ts = List.concat (map (map #1 o #2) asms); 
13394  1218 
val ts' = map (norm_term env) ts; 
1219 
val spec' = 

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

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

15570  1222 
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

1223 
 eval_text ctxt (id, _) _ ((spec, binds), Defines defs) = 
15570  1224 
(spec, Library.foldl (bind_def ctxt id) (binds, map (#1 o #2) defs)) 
13308  1225 
 eval_text _ _ _ (text, Notes _) = text; 
1226 

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

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

1228 

13308  1229 
fun closeup _ false elem = elem 
1230 
 closeup ctxt true elem = 

12839  1231 
let 
13308  1232 
fun close_frees t = 
1233 
let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1) 

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

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

1236 

1237 
fun no_binds [] = [] 

1238 
 no_binds _ = 

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

1240 
in 

1241 
(case elem of 

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

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

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

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

1246 
 e => e) 

1247 
end; 

12839  1248 

12502  1249 

12839  1250 
fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) => 
12727  1251 
(x, assoc_string (parms, x), mx)) fixes) 
16169
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

1252 
 finish_ext_elem parms _ (Constrains csts, _) = 
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

1253 
Constrains (map (fn (x, _) => (x, valOf (assoc_string (parms, x)))) csts) 
12839  1254 
 finish_ext_elem _ close (Assumes asms, propp) = 
1255 
close (Assumes (map #1 asms ~~ propp)) 

1256 
 finish_ext_elem _ close (Defines defs, propp) = 

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

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

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

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

1263 

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

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

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

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

1269 
val [(id', es)] = unify_elemss ctxt parms [(id, e)]; 