author  ballarin 
Mon, 18 Apr 2005 09:25:23 +0200  
changeset 15763  b901a127ac73 
parent 15749  b57bff155e79 
child 15798  016f3be5a5ec 
permissions  rwrr 
12014  1 
(* Title: Pure/Isar/locale.ML 
11896  2 
ID: $Id$ 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

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

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

7 

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

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

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

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

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

14 
See also: 

15 

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

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

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

21 
signature LOCALE = 

22 
sig 

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

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

12273  29 
datatype expr = 
30 
Locale of string  

31 
Rename of expr * string option list  

32 
Merge of expr list 

33 
val empty: expr 

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

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

35 

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

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

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

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

45 
val intern_attrib_elem_expr: theory > 

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

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

47 

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

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

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

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

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

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

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

58 
(* Diagnostic functions *) 

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

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

63 
val print_local_registrations: string > context > unit 
15596  64 

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

68 
val smart_note_thmss: string > string option > 

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

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

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

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

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

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

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

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

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

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

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

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

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

92 
string * term list > thm > context > context 
15596  93 

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

94 
(* Theory setup for locales *) 
11896  95 
val setup: (theory > theory) list 
96 
end; 

12839  97 

12289  98 
structure Locale: LOCALE = 
11896  99 
struct 
100 

12273  101 
(** locale elements and expressions **) 
11896  102 

12014  103 
type context = ProofContext.context; 
11896  104 

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

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

12273  110 

111 
datatype expr = 

112 
Locale of string  

113 
Rename of expr * string option list  

114 
Merge of expr list; 

11896  115 

12273  116 
val empty = Merge []; 
117 

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

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

119 
Elem of 'a  Expr of expr; 
12273  120 

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

12070  123 

124 
type locale = 

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

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

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

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

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

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

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

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

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

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

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

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

137 
params: (string * typ option) list * string list} (*all/local params*) 
12063  138 

11896  139 

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

142 

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

144 

145 

146 

11896  147 
(** theory data **) 
148 

15596  149 
structure Termlisttab = TableFun(type key = term list 
150 
val ord = Library.list_ord Term.term_ord); 

151 

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

152 
structure GlobalLocalesArgs = 
11896  153 
struct 
12014  154 
val name = "Isar/locales"; 
15596  155 
type T = NameSpace.T * locale Symtab.table * 
15703  156 
((string * Attrib.src list) * thm list) Termlisttab.table 
15596  157 
Symtab.table; 
158 
(* 1st entry: locale namespace, 

159 
2nd entry: locales of the theory, 

160 
3rd entry: registrations: theorems instantiating locale assumptions, 

161 
with prefix and attributes, indexed by locale name and parameter 

162 
instantiation *) 

11896  163 

15596  164 
val empty = (NameSpace.empty, Symtab.empty, Symtab.empty); 
12063  165 
val copy = I; 
12118  166 
val prep_ext = I; 
12289  167 

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

170 
SOME {predicate = predicate, import = import, 

171 
elems = gen_merge_lists eq_snd elems elems', 

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

172 
params = params}; 
15596  173 
(* joining of registrations: prefix and attributes of left theory, 
174 
thmsss are equal *) 

175 
fun join_regs (reg, _) = SOME reg; 

176 
fun merge ((space1, locs1, regs1), (space2, locs2, regs2)) = 

177 
(NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2), 

178 
Symtab.join (SOME o Termlisttab.join join_regs) (regs1, regs2)); 

12289  179 

15596  180 
fun print _ (space, locs, _) = 
12273  181 
Pretty.strs ("locales:" :: map (NameSpace.cond_extern space o #1) (Symtab.dest locs)) 
12014  182 
> Pretty.writeln; 
11896  183 
end; 
184 

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

185 
structure GlobalLocalesData = TheoryDataFun(GlobalLocalesArgs); 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

186 

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

187 
(** context data **) 
11896  188 

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

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

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

191 
val name = "Isar/locales"; 
15703  192 
type T = ((string * Args.src list) * thm list) Termlisttab.table 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

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

194 
(* registrations: theorems instantiating locale assumptions, 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

195 
with prefix and attributes, indexed by locale name and parameter 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

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

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

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

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

200 

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

201 
structure LocalLocalesData = ProofDataFun(LocalLocalesArgs); 
12289  202 

12277  203 

204 
(* access locales *) 

205 

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

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

207 

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

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

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

210 

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

212 
GlobalLocalesData.map (fn (space, locs, regs) => 
15596  213 
(NameSpace.extend (space, [name]), locs, regs)); 
11896  214 

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

216 
GlobalLocalesData.map (fn (space, locs, regs) => 
15596  217 
(space, Symtab.update ((name, loc), locs), regs)); 
218 

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

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

12014  221 
fun the_locale thy name = 
222 
(case get_locale thy name of 

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

11896  225 

12046  226 

15596  227 
(* access registrations *) 
228 

15696  229 
(* Ids of global registrations are varified, 
230 
Ids of local registrations are not. 

231 
Thms of registrations are never varified. *) 

232 

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

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

234 

15696  235 
fun gen_get_registrations get thy_ctxt name = 
236 
case Symtab.lookup (get thy_ctxt, name) of 

237 
NONE => [] 

238 
 SOME tab => Termlisttab.dest tab; 

239 

240 
val get_global_registrations = 

241 
gen_get_registrations (#3 o GlobalLocalesData.get); 

242 
val get_local_registrations = 

243 
gen_get_registrations LocalLocalesData.get; 

244 

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

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

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

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

248 
 SOME tab => Termlisttab.lookup (tab, ps); 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

249 

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

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

251 
gen_get_registration (#3 o GlobalLocalesData.get); 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

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

253 
gen_get_registration LocalLocalesData.get; 
15596  254 

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

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

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

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

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

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

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

261 
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

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

263 

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

264 

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

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

266 

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

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

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

269 
let 
15596  270 
val tab = getOpt (Symtab.lookup (regs, name), Termlisttab.empty); 
271 
in 

272 
Symtab.update ((name, Termlisttab.update_new ((ps, (attn, [])), tab)), 

273 
regs) 

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

274 
end handle Termlisttab.DUP _ => regs); 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

275 

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

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

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

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

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

280 
val put_local_registration = gen_put_registration LocalLocalesData.map; 
15596  281 

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

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

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

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

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

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

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

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

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

291 

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

292 

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

293 
(* add witness theorem to registration in theory or context, 
15596  294 
ignored if registration not present *) 
295 

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

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

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

298 
let 
15596  299 
val tab = valOf (Symtab.lookup (regs, name)); 
300 
val (x, thms) = valOf (Termlisttab.lookup (tab, ps)); 

301 
in 

302 
Symtab.update ((name, Termlisttab.update ((ps, (x, thm::thms)), tab)), 

303 
regs) 

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

304 
end handle Option => regs); 
15596  305 

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

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

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

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

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

310 
val add_local_witness = gen_add_witness LocalLocalesData.map; 
15596  311 

312 

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

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

314 
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

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

316 

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

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

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

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

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

321 
(case get_locale thy name of 
15531  322 
NONE => false 
323 
 SOME {import, ...} => imps import low) 

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

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

325 
 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

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

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

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

329 

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

330 

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

331 
(* printing of registrations *) 
15596  332 

15703  333 
fun gen_print_registrations get_regs mk_ctxt msg loc thy_ctxt = 
15596  334 
let 
15703  335 
val ctxt = mk_ctxt thy_ctxt; 
336 
val thy = ProofContext.theory_of ctxt; 

337 
val sg = Theory.sign_of thy; 

338 

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

340 
val prt_atts = Args.pretty_attribs ctxt; 

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

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

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

344 
Pretty.block (Pretty.breaks 

345 
(Pretty.str prfx :: prt_atts atts @ [Pretty.str ":", Pretty.brk 1, 

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

347 

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

349 
val regs = get_regs thy_ctxt; 
15596  350 
val loc_regs = Symtab.lookup (regs, loc_int); 
351 
in 

352 
(case loc_regs of 

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

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

354 
 SOME r => let 
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
15749
diff
changeset

355 
val r' = Termlisttab.dest r; 
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
15749
diff
changeset

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

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

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

359 
end) 
15596  360 
> Pretty.writeln 
361 
end; 

362 

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

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

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

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

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

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

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

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

372 

15596  373 

12277  374 
(* diagnostics *) 
12273  375 

12277  376 
fun err_in_locale ctxt msg ids = 
377 
let 

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

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

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

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

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

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

12063  387 

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

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

389 

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

390 
fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids'); 
12277  391 

392 

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

393 
(** primitives **) 
12046  394 

15703  395 
(* map elements *) 
396 

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

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

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

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

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

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

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

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

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

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

407 

408 
fun map_values typ term thm = map_elem 

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

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

411 

412 

413 
(* map attributes *) 

414 

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

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

417 

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

419 

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

421 

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

423 
 intern_attrib_elem_expr _ (Expr expr) = Expr expr; 

424 

425 

12277  426 
(* renaming *) 
12263  427 

15570  428 
fun rename ren x = getOpt (assoc_string (ren, x), x); 
12263  429 

15703  430 
fun rename_var ren (x, mx) = 
431 
let val x' = rename ren x in 

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

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

434 
end; 

435 

12263  436 
fun rename_term ren (Free (x, T)) = Free (rename ren x, T) 
437 
 rename_term ren (t $ u) = rename_term ren t $ rename_term ren u 

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

439 
 rename_term _ a = a; 

440 

441 
fun rename_thm ren th = 

442 
let 

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

444 
val cert = Thm.cterm_of sign; 

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

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

449 
in 

450 
if xs = xs' then th 

451 
else 

452 
th 

453 
> Drule.implies_intr_list (map cert hyps) 

454 
> Drule.forall_intr_list (cert_frees xs) 

455 
> Drule.forall_elim_list (cert_vars xs) 

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

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

458 
end; 

459 

15703  460 
fun rename_elem ren = 
461 
map_values I (rename_term ren) (rename_thm ren) o 

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

12263  463 

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

464 
fun rename_facts prfx elem = 
12307  465 
let 
12323  466 
fun qualify (arg as ((name, atts), x)) = 
13394  467 
if prfx = "" orelse name = "" then arg 
13375  468 
else ((NameSpace.pack [prfx, name], atts), x); 
12307  469 
in 
470 
(case elem of 

471 
Fixes fixes => Fixes fixes 

472 
 Assumes asms => Assumes (map qualify asms) 

473 
 Defines defs => Defines (map qualify defs) 

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

475 
end; 

476 

12263  477 

12502  478 
(* type instantiation *) 
479 

480 
fun inst_type [] T = T 

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

483 
fun inst_term [] t = t 

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

485 

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

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

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

489 
val sign = ProofContext.sign_of ctxt; 
12575  490 
val cert = Thm.cterm_of sign; 
491 
val certT = Thm.ctyp_of sign; 

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

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

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

497 
else 

498 
th 

499 
> Drule.implies_intr_list (map cert hyps) 

12575  500 
> Drule.tvars_intr_list (map (#1 o #1) env') 
12502  501 
> (fn (th', al) => th' > 
15570  502 
Thm.instantiate ((map (fn ((a, _), T) => (valOf (assoc (al, a)), certT T)) env'), [])) 
12502  503 
> (fn th'' => Drule.implies_elim_list th'' 
504 
(map (Thm.assume o cert o inst_term env') hyps)) 

505 
end; 

506 

15703  507 
fun inst_elem ctxt env = 
508 
map_values (inst_type env) (inst_term env) (inst_thm ctxt env); 

12502  509 

510 

15696  511 
(* term and type instantiation, variant using symbol tables *) 
512 

513 
(* instantiate TFrees *) 

514 

515 
fun tinst_tab_type tinst T = if Symtab.is_empty tinst 

516 
then T 

517 
else Term.map_type_tfree 

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

519 

520 
fun tinst_tab_term tinst t = if Symtab.is_empty tinst 

521 
then t 

522 
else Term.map_term_types (tinst_tab_type tinst) t; 

523 

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

525 
then thm 

526 
else let 

527 
val cert = Thm.cterm_of sg; 

528 
val certT = Thm.ctyp_of sg; 

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

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

531 
val tinst' = Symtab.dest tinst > 

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

533 
in 

534 
if null tinst' then thm 

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

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

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

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

539 
[])) 

540 
> (fn th => Drule.implies_elim_list th 

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

542 
end; 

543 

15749  544 
fun tinst_tab_elem sg tinst = 
545 
map_values (tinst_tab_type tinst) (tinst_tab_term tinst) (tinst_tab_thm sg tinst); 

546 

15696  547 
(* instantiate TFrees and Frees *) 
548 

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

550 
then tinst_tab_term tinst 

551 
else (* instantiate terms and types simultaneously *) 

552 
let 

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

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

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

556 
 SOME t => t) 

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

558 
 instf (b as Bound _) = b 

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

560 
 instf (s $ t) = instf s $ instf t 

561 
in instf end; 

562 

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

564 
then tinst_tab_thm sg tinst thm 

565 
else let 

566 
val cert = Thm.cterm_of sg; 

567 
val certT = Thm.ctyp_of sg; 

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

569 
(* type instantiations *) 

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

571 
val tinst' = Symtab.dest tinst > 

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

573 
(* term instantiations; 

574 
note: lhss are type instantiated, because 

575 
type insts will be done first*) 

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

577 
val inst' = Symtab.dest inst > 

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

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

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

581 
else NONE) frees); 

582 
in 

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

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

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

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

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

588 
[])) 

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

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

591 
> (fn th => Drule.implies_elim_list th 

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

593 
end; 

594 

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

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

596 
map_values (tinst_tab_type tinst) (inst_tab_term inst) (inst_tab_thm sg inst); 
15696  597 

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

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

600 

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

601 

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

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

603 

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

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

605 

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

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

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

608 

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

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

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

612 
val tfrees = map TFree 
14695  613 
(Term.invent_names (ProofContext.used_types ctxt) "'a" (length tvars) ~~ map #2 tvars); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

615 

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

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

617 
let 
15531  618 
fun paramify (i, NONE) = (i, NONE) 
619 
 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

620 

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

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

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

624 

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

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

627 
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

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

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

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

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

633 

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

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

636 

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

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

640 

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

641 

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

642 
(* flatten expressions *) 
11896  643 

12510  644 
local 
12502  645 

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

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

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

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

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

650 

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

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

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

653 
val param_decls = 
15570  654 
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

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

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

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

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

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

662 

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

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

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

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

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

668 

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

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

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

672 
val tsig = Sign.tsig_of sign; 
12502  673 
val maxidx = length raw_parmss; 
674 
val idx_parmss = (0 upto maxidx  1) ~~ raw_parmss; 

675 

676 
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

677 
fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps); 
15570  678 
val parms = fixed_parms @ List.concat (map varify_parms idx_parmss); 
12502  679 

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

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

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

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

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

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

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

686 
end 
15570  687 
fun unify_list (envir, T :: Us) = Library.foldl (unify T) (envir, Us) 
12502  688 
 unify_list (envir, []) = envir; 
15570  689 
val (unifier, _) = Library.foldl unify_list 
12502  690 
((Vartab.empty, maxidx), map #2 (Symtab.dest (Symtab.make_multi parms))); 
691 

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

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

694 

695 
fun inst_parms (i, ps) = 

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

696 
foldr Term.add_typ_tfrees [] (List.mapPartial snd ps) 
15570  697 
> List.mapPartial (fn (a, S) => 
12502  698 
let val T = Envir.norm_type unifier' (TVar ((a, i), S)) 
15531  699 
in if T = TFree (a, S) then NONE else SOME ((a, S), T) end) 
12502  700 
in map inst_parms idx_parmss end; 
701 

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

702 
in 
12502  703 

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

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

705 

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

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

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

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

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

710 
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

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

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

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

715 

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

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

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

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

720 
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

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

723 
map (inst_thm ctxt env) axs), map (inst_elem ctxt env) elems); 
12839  724 
in map inst (elemss ~~ envs) end; 
12502  725 

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

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

729 
identifier). 

730 

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

732 
((name, ps), (ax_ps, axs)) 

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

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

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

736 
hence axioms may contain additional parameters from later fragments: 

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

738 

739 
Elements are enriched by identifierlike information: 

740 
(((name, ax_ps), axs), elems) 

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

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

743 
typeinstantiated. 

744 

745 
*) 

746 

12575  747 
fun flatten_expr ctxt (prev_idents, expr) = 
12014  748 
let 
749 
val thy = ProofContext.theory_of ctxt; 

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

752 
of axioms *) 

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

12263  754 

15531  755 
fun renaming (SOME x :: xs) (y :: ys) = (y, x) :: renaming xs ys 
756 
 renaming (NONE :: xs) (y :: ys) = renaming xs ys 

12273  757 
 renaming [] _ = [] 
12289  758 
 renaming xs [] = raise ERROR_MESSAGE ("Too many arguments in renaming: " ^ 
15531  759 
commas (map (fn NONE => "_"  SOME x => quote x) xs)); 
12289  760 

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

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

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

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

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

12263  768 

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

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

771 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

804 
(([], []), es); 
12014  805 

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

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

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

808 

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

809 
fun eval ((name, xs), axs) = 
12273  810 
let 
13308  811 
val {params = (ps, qs), elems, ...} = the_locale thy name; 
12307  812 
val ren = filter_out (op =) (map #1 ps ~~ xs); 
13308  813 
val (params', elems') = 
814 
if null ren then ((ps, qs), map #1 elems) 

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

818 
in (((name, params'), axs), elems'') end; 
12307  819 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

840 
in (prev_idents @ idents, final_elemss) end; 
12046  841 

12510  842 
end; 
843 

12070  844 

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

845 
(* activate elements *) 
12273  846 

12510  847 
local 
848 

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

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

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

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

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

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

854 
> Seq.single 
12263  855 

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

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

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

859 
let 
15703  860 
val asms' = map_attrib_specs (Attrib.context_attribute_i ctxt) asms; 
861 
val ts = List.concat (map (map #1 o #2) asms'); 

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

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

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

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

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

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

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

876 
 activate_elem is_ext ((ctxt, axs), Notes facts) = 
15596  877 
let 
15703  878 
val facts' = map_attrib_facts (Attrib.context_attribute_i ctxt) facts; 
879 
val (ctxt', res) = ctxt > ProofContext.note_thmss_i facts'; 

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

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

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

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

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

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

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

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

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

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

892 
end 

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

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

894 

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

895 
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

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

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

901 

12546  902 
in 
903 

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

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

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

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

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

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

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

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

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

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

914 

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

915 
fun activate_facts prep_facts arg = 
15570  916 
apsnd (apsnd List.concat o Library.split_list) (activate_elemss prep_facts arg); 
12546  917 

15703  918 
fun activate_note prep_facts (ctxt, args) = 
919 
let 

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

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

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

923 

12510  924 
end; 
925 

12307  926 

15696  927 
(* register elements *) 
928 

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

930 
if name = "" then ctxt 

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

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

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

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

935 
end; 

936 

937 
fun register_elemss id_elemss ctxt = 

938 
foldl register_elems ctxt id_elemss; 

939 

940 

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

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

942 

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

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

944 

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

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

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

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

948 

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

949 

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

950 
(* parameters *) 
12502  951 

952 
local 

953 

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

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

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

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

957 

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

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

959 

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

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

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

962 

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

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

964 

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

965 

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

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

967 

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

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

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

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

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

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

976 
identifierlike information of the element is as follows: 

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

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

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

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

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

982 

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

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

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

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

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

988 

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

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

990 

12839  991 
local 
992 

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

997 

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

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

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

1001 
 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

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

1003 

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

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

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

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

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

12839  1012 
in 
1013 

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

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

1015 

12727  1016 
fun declare_elemss prep_fixes fixed_params raw_elemss ctxt = 
1017 
let 

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

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

1019 
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

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

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

1022 
ProofContext.declare_terms (map Free fixed_params) ctxt; 
12727  1023 
val int_elemss = 
1024 
raw_elemss 

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

1026 
> unify_elemss ctxt_with_fixed fixed_params; 
12727  1027 
val (_, raw_elemss') = 
1028 
foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es))  x => x) 

1029 
(int_elemss, raw_elemss); 

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

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

1031 

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

1033 

12839  1034 
local 
1035 

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

1037 

12839  1038 
val norm_term = Envir.beta_norm oo Term.subst_atomic; 
1039 

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

1042 

13336  1043 
fun abstract_term eq = (*assumes wellformedness according to ProofContext.cert_def*) 
12839  1044 
let 
1045 
val body = Term.strip_all_body eq; 

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

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

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

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

1051 

1052 
fun abstract_thm sign eq = 

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

12502  1054 

13336  1055 
fun bind_def ctxt (name, ps) ((xs, env, ths), eq) = 
12839  1056 
let 
13336  1057 
val ((y, T), b) = abstract_term eq; 
13308  1058 
val b' = norm_term env b; 
13336  1059 
val th = abstract_thm (ProofContext.sign_of ctxt) eq; 
13308  1060 
fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)]; 
12839  1061 
in 
13308  1062 
conditional (exists (equal y o #1) xs) (fn () => 
1063 
err "Attempt to define previously specified variable"); 

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

1065 
err "Attempt to redefine variable"); 

13336  1066 
(Term.add_frees (xs, b'), (Free (y, T), b') :: env, th :: ths) 
12839  1067 
end; 
12575  1068 

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

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

1070 

13308  1071 
fun eval_text _ _ _ (text, Fixes _) = text 
13394  1072 
 eval_text _ _ is_ext ((((exts, exts'), (ints, ints')), (xs, env, defs)), Assumes asms) = 
1073 
let 

15570  1074 
val ts = List.concat (map (map #1 o #2) asms); 
13394  1075 
val ts' = map (norm_term env) ts; 
1076 
val spec' = 

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

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

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

1080 
 eval_text ctxt (id, _) _ ((spec, binds), Defines defs) = 
15570  1081 
(spec, Library.foldl (bind_def ctxt id) (binds, map (#1 o #2) defs)) 
13308  1082 
 eval_text _ _ _ (text, Notes _) = text; 
1083 

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

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

1085 

13308  1086 
fun closeup _ false elem = elem 
1087 
 closeup ctxt true elem = 

12839  1088 
let 
13308  1089 
fun close_frees t = 
1090 
let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1) 

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

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

1093 

1094 
fun no_binds [] = [] 

1095 
 no_binds _ = 

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

1097 
in 

1098 
(case elem of 

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

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

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

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

1103 
 e => e) 

1104 
end; 

12839  1105 

12502  1106 

12839  1107 
fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) => 
12727  1108 
(x, assoc_string (parms, x), mx)) fixes) 
12839  1109 
 finish_ext_elem _ close (Assumes asms, propp) = 
1110 
close (Assumes (map #1 asms ~~ propp)) 

1111 
 finish_ext_elem _ close (Defines defs, propp) = 

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

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

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

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

1118 

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

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

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

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

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

1126 
in (text', (id', map Int es)) end 
13375  1127 
 finish_elems ctxt parms do_close (text, ((id, Ext e), [propp])) = 
13308  1128 
let 
1129 
val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp); 

13375  1130 
val text' = eval_text ctxt id true (text, e'); 
13308  1131 
in (text', (id, [Ext e'])) end; 
12839  1132 

1133 
in 

12510  1134 

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

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

1136 

13375  1137 
fun finish_elemss ctxt parms do_close = 
1138 
foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close); 

12839  1139 

1140 
end; 

1141 

15127  1142 
(* CB: type inference and consistency checks for locales *) 
1143 

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

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

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

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

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

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

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

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

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

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

1156 
external elements in raw_elemss. *) 
15570  1157 
val raw_propps = map List.concat raw_proppss; 
1158 
val raw_propp = List.concat raw_propps; 

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

1159 

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

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

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

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

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

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

1165 
to context *) 
15570  1166 
val ctxt = ProofContext.declare_terms (List.concat (map (map fst) all_propp)) ctxt; 
12502  1167 

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

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

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

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

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

1173 
val propps = unflat raw_propps propp; 
12839  1174 
val proppss = map (uncurry unflat) (raw_proppss ~~ propps); 
12502  1175 

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

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

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

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

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

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

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

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

1184 
(* CB: extract information from assumes and defines elements 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1185 
(fixes and notes in raw_elemss don't have an effect on text and elemss), 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1186 
compute final form of context elements. *) 
13394  1187 
val (text, elemss) = finish_elemss ctxt parms do_close 
1188 
(((([], []), ([], [])), ([], [], [])), raw_elemss ~~ proppss); 

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

1189 
(* CB: text has the following structure: 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1190 
(((exts, exts'), (ints, ints')), (xs, env, defs)) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

1192 
exts: external assumptions (terms in external assumes elements) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1193 
exts': dito, normalised wrt. env 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1194 
ints: internal assumptions (terms in internal assumes elements) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1195 
ints': dito, normalised wrt. env 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1196 
xs: the free variables in exts' and ints' and rhss of definitions, 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1197 
this includes parameters except defined parameters 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1198 
env: list of term pairs encoding substitutions, where the first term 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1199 
is a free variable; substitutions represent defines elements and 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1200 
the rhs is normalised wrt. the previous env 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1201 
defs: theorems representing the substitutions from defines elements 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1202 
(thms are normalised wrt. env). 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1203 
elemss is an updated version of raw_elemss: 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1204 
 type info added to Fixes 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1205 
 axiom and definition statement replaced by corresponding one 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1206 
from proppss in Assumes and Defines 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

1208 
*) 
13308  1209 
in ((parms, elemss, concl), text) end; 
12502  1210 

1211 
in 

1212 

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

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

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

1215 

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

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

1217 

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

1218 

15703  1219 
(* facts and attributes *) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

1220 

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

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

1222 

15703  1223 
fun prep_name ctxt name = 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1224 
(* CB: reject qualified theorem names in locale declarations *) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

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

1228 

15703  1229 
fun prep_facts _ _ ctxt (Int elem) = 
1230 
map_values I I (Thm.transfer (ProofContext.theory_of ctxt)) elem 

1231 
 prep_facts get intern ctxt (Ext elem) = elem > map_elem 

1232 
{var = I, typ = I, term = I, 

1233 
name = prep_name ctxt, 

1234 
fact = get ctxt, 

1235 
attrib = Args.assignable o intern (ProofContext.sign_of ctxt)}; 

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

1236 

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

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

1238 

15703  1239 
fun read_facts x = prep_facts ProofContext.get_thms Attrib.intern_src x; 
1240 
fun cert_facts x = prep_facts (K I) (K I) x; 

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

1241 

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

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

1243 

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

1244 

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

1246 

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

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

1248 

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

1249 
fun prep_context_statement prep_expr prep_elemss prep_facts 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

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

1252 
val sign = ProofContext.sign_of context; 
13375  1253 

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

1254 
val (import_ids, raw_import_elemss) = flatten (context, prep_expr sign) ([], Expr import); 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

1255 
(* CB: normalise "includes" among elements *) 
15696  1256 
val (ids, raw_elemsss) = foldl_map (flatten (context, prep_expr sign)) 
1257 
(import_ids, elements); 

1258 

1259 
val raw_elemss = List.concat raw_elemsss; 

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

1260 
(* CB: raw_import_elemss @ raw_elemss is the normalised list of 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1261 
context elements obtained from import and elements. *) 
13375  1262 
val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close 
13336  1263 
context fixed_params (raw_import_elemss @ raw_elemss) raw_concl; 
15696  1264 
(* replace extended ids (for axioms) by ids *) 
1265 
val all_elemss' = map (fn (((_, ps), _), (((n, ps'), ax), elems)) => 

1266 
(((n, List.filter (fn (p, _) => p mem ps) ps'), ax), elems)) 

1267 
(ids ~~ all_elemss); 

1268 

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

1269 
(* CB: all_elemss and parms contain the correct parameter types *) 
15696  1270 
val (ps,qs) = splitAt(length raw_import_elemss, all_elemss') 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1271 
val (import_ctxt, (import_elemss, _)) = 