author  wenzelm 
Sun, 07 May 2006 00:22:05 +0200  
changeset 19585  70a1ce3b23ae 
parent 19482  9f11af8f7ef9 
child 19662  2f5d076fde32 
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 

17437  14 
Interpretation enables the reuse of theorems of locales in other 
15 
contexts, namely those defined by theories, structured proofs and 

16 
locales themselves. 

17 

14446  18 
See also: 
19 

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

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

15099  22 
Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 3450, 2004. 
11896  23 
*) 
24 

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

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

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

27 
 dangling type frees in locales 
16620
2a7f46324218
Proper treatment of betaredexes in witness theorems.
ballarin
parents:
16458
diff
changeset

28 
 test subsumption of interpretations when merging theories 
17138  29 
 var vs. fixes in locale to be interpreted (interpretation in locale) 
30 
(implicit locale expressions generated by multiple registrations) 

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

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

32 

11896  33 
signature LOCALE = 
34 
sig 

12273  35 
datatype expr = 
36 
Locale of string  

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

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

18137  40 
datatype 'a element = Elem of 'a  Expr of expr 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

41 

16458  42 
val intern: theory > xstring > string 
43 
val extern: theory > string > xstring 

18806  44 
val init: string > theory > cterm list * Proof.context 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

45 

18795
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset

46 
(* The specification of a locale *) 
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset

47 

303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset

48 
val parameters_of: theory > string > 
18917  49 
((string * typ) * mixfix) list 
19276  50 
val parameters_of_expr: theory > expr > 
51 
((string * typ) * mixfix) list 

18795
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset

52 
val local_asms_of: theory > string > 
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset

53 
((string * Attrib.src list) * term list) list 
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset

54 
val global_asms_of: theory > string > 
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset

55 
((string * Attrib.src list) * term list) list 
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset

56 

18899
a8e913c93578
theorem(_in_locale): Element.statement, Obtain.statement;
wenzelm
parents:
18890
diff
changeset

57 
(* Processing of locale statements *) 
18137  58 
val read_context_statement: xstring option > Element.context element list > 
19585  59 
(string * string list) list list > Proof.context > 
18806  60 
string option * (cterm list * Proof.context) * (cterm list * Proof.context) * 
19585  61 
(term * term list) list list 
18137  62 
val cert_context_statement: string option > Element.context_i element list > 
19585  63 
(term * term list) list list > Proof.context > 
18806  64 
string option * (cterm list * Proof.context) * (cterm list * Proof.context) * 
19585  65 
(term * term list) list list 
15596  66 

67 
(* Diagnostic functions *) 

12758  68 
val print_locales: theory > unit 
18137  69 
val print_locale: theory > bool > expr > Element.context list > unit 
17138  70 
val print_global_registrations: bool > string > theory > unit 
18617  71 
val print_local_registrations': bool > string > Proof.context > unit 
72 
val print_local_registrations: bool > string > Proof.context > unit 

18137  73 

18917  74 
val add_locale: bool > bstring > expr > Element.context list > theory 
19293  75 
> (string * Proof.context (*body context!*)) * theory 
18917  76 
val add_locale_i: bool > bstring > expr > Element.context_i list > theory 
19293  77 
> (string * Proof.context (*body context!*)) * theory 
15596  78 

15696  79 
(* Storing results *) 
15703  80 
val note_thmss: string > xstring > 
18806  81 
((string * Attrib.src list) * (thmref * Attrib.src list) list) list > 
82 
theory > ((string * thm list) list * (string * thm list) list) * (Proof.context * theory) 

15703  83 
val note_thmss_i: string > string > 
18806  84 
((string * Attrib.src list) * (thm list * Attrib.src list) list) list > 
85 
theory > ((string * thm list) list * (string * thm list) list) * (Proof.context * theory) 

86 
val add_thmss: string > string > 

87 
((string * Attrib.src list) * (thm list * Attrib.src list) list) list > 

88 
cterm list * Proof.context > 

89 
((string * thm list) list * (string * thm list) list) * Proof.context 

19370  90 
val add_abbrevs: string > string * bool > (bstring * term * mixfix) list > 
19018
88b4979193d8
added abbreviations: activated by init, no expressions yet;
wenzelm
parents:
18964
diff
changeset

91 
cterm list * Proof.context > Proof.context 
18137  92 

18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

93 
val theorem: string > Method.text option > (thm list list > theory > theory) > 
18899
a8e913c93578
theorem(_in_locale): Element.statement, Obtain.statement;
wenzelm
parents:
18890
diff
changeset

94 
string * Attrib.src list > Element.context element list > Element.statement > 
17355  95 
theory > Proof.state 
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

96 
val theorem_i: string > Method.text option > (thm list list > theory > theory) > 
18907  97 
string * Attrib.src list > Element.context_i element list > Element.statement_i > 
17355  98 
theory > Proof.state 
17856  99 
val theorem_in_locale: string > Method.text option > 
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

100 
(thm list list > thm list list > theory > theory) > 
18899
a8e913c93578
theorem(_in_locale): Element.statement, Obtain.statement;
wenzelm
parents:
18890
diff
changeset

101 
xstring > string * Attrib.src list > Element.context element list > Element.statement > 
17355  102 
theory > Proof.state 
17856  103 
val theorem_in_locale_i: string > Method.text option > 
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

104 
(thm list list > thm list list > theory > theory) > 
18137  105 
string > string * Attrib.src list > Element.context_i element list > 
18907  106 
Element.statement_i > theory > Proof.state 
17355  107 
val smart_theorem: string > xstring option > 
18899
a8e913c93578
theorem(_in_locale): Element.statement, Obtain.statement;
wenzelm
parents:
18890
diff
changeset

108 
string * Attrib.src list > Element.context element list > Element.statement > 
17355  109 
theory > Proof.state 
110 
val interpretation: string * Attrib.src list > expr > string option list > 

111 
theory > Proof.state 

112 
val interpretation_in_locale: xstring * expr > theory > Proof.state 

113 
val interpret: string * Attrib.src list > expr > string option list > 

114 
bool > Proof.state > Proof.state 

11896  115 
end; 
12839  116 

12289  117 
structure Locale: LOCALE = 
11896  118 
struct 
119 

12273  120 
(** locale elements and expressions **) 
11896  121 

18137  122 
datatype ctxt = datatype Element.ctxt; 
17355  123 

12273  124 
datatype expr = 
125 
Locale of string  

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

126 
Rename of expr * (string * mixfix option) option list  
12273  127 
Merge of expr list; 
11896  128 

12273  129 
val empty = Merge []; 
130 

18137  131 
datatype 'a element = 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

132 
Elem of 'a  Expr of expr; 
12273  133 

18137  134 
fun map_elem f (Elem e) = Elem (f e) 
135 
 map_elem _ (Expr e) = Expr e; 

136 

18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

137 
type witness = term * thm; (*hypothesis as fact*) 
12070  138 
type locale = 
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

139 
{predicate: cterm list * witness list, 
16736
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

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

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

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

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

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

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

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

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

148 
*) 
19018
88b4979193d8
added abbreviations: activated by init, no expressions yet;
wenzelm
parents:
18964
diff
changeset

149 
import: expr, (*dynamic import*) 
88b4979193d8
added abbreviations: activated by init, no expressions yet;
wenzelm
parents:
18964
diff
changeset

150 
elems: (Element.context_i * stamp) list, (*static content*) 
19278  151 
params: ((string * typ) * mixfix) list, (*all params*) 
152 
lparams: string list, (*local parmas*) 

19370  153 
abbrevs: (((string * bool) * (bstring * term * mixfix) list) * stamp) list, (*abbreviations*) 
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

154 
regs: ((string * string list) * (term * thm) list) list} 
16736
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

155 
(* Registrations: indentifiers and witness theorems of locales interpreted 
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

156 
in the locale. 
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

157 
*) 
12063  158 

11896  159 

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

162 

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

164 

165 

166 

16736
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

167 
(** management of registrations in theories and proof contexts **) 
11896  168 

15837  169 
structure Registrations : 
170 
sig 

171 
type T 

172 
val empty: T 

173 
val join: T * T > T 

18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

174 
val dest: T > (term list * ((string * Attrib.src list) * witness list)) list 
16458  175 
val lookup: theory > T * term list > 
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

176 
((string * Attrib.src list) * witness list) option 
16458  177 
val insert: theory > term list * (string * Attrib.src list) > T > 
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

178 
T * (term list * ((string * Attrib.src list) * witness list)) list 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

179 
val add_witness: term list > witness > T > T 
15837  180 
end = 
181 
struct 

182 
(* a registration consists of theorems instantiating locale assumptions 

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

18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

184 
type T = ((string * Attrib.src list) * witness list) Termtab.table; 
15837  185 

186 
val empty = Termtab.empty; 

187 

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

189 
fun termify ts = 

18343  190 
Term.list_comb (Const ("", map fastype_of ts > propT), ts); 
15837  191 
fun untermify t = 
192 
let fun ut (Const _) ts = ts 

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

194 
in ut t [] end; 

195 

16620
2a7f46324218
Proper treatment of betaredexes in witness theorems.
ballarin
parents:
16458
diff
changeset

196 
(* joining of registrations: prefix and attributes of left theory, 
15837  197 
thms are equal, no attempt to subsumption testing *) 
19025  198 
fun join (r1, r2) = Termtab.join (fn _ => fn (reg, _) => reg) (r1, r2); 
15837  199 

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

201 

202 
(* registrations that subsume t *) 

17203  203 
fun subsumers thy t regs = 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset

204 
filter (fn (t', _) => Pattern.matches thy (t', t)) (Termtab.dest regs); 
15837  205 

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

207 
fun lookup sign (regs, ts) = 

208 
let 

209 
val t = termify ts; 

17203  210 
val subs = subsumers sign t regs; 
15837  211 
in (case subs of 
212 
[] => NONE 

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

18190  214 
val (tinst, inst) = Pattern.match sign (t', t) (Vartab.empty, Vartab.empty); 
15837  215 
(* thms contain Frees, not Vars *) 
216 
val tinst' = tinst > Vartab.dest 

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

218 
> Symtab.make; 

219 
val inst' = inst > Vartab.dest 

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

221 
> Symtab.make; 

222 
in 

18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

223 
SOME (attn, map (fn (t, th) => 
18137  224 
(Element.inst_term (tinst', inst') t, 
225 
Element.inst_thm sign (tinst', inst') th)) thms) 

15837  226 
end) 
227 
end; 

228 

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

230 
additionally returns registrations that are strictly subsumed *) 

231 
fun insert sign (ts, attn) regs = 

232 
let 

233 
val t = termify ts; 

17203  234 
val subs = subsumers sign t regs ; 
15837  235 
in (case subs of 
236 
[] => let 

237 
val sups = 

19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset

238 
filter (fn (t', _) => Pattern.matches sign (t, t')) (Termtab.dest regs); 
15837  239 
val sups' = map (apfst untermify) sups 
17412  240 
in (Termtab.update (t, (attn, [])) regs, sups') end 
15837  241 
 _ => (regs, [])) 
242 
end; 

243 

244 
(* add witness theorem to registration, 

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

245 
only if instantiation is exact, otherwise exception Option raised *) 
15837  246 
fun add_witness ts thm regs = 
247 
let 

248 
val t = termify ts; 

18343  249 
val (x, thms) = the (Termtab.lookup regs t); 
15837  250 
in 
17412  251 
Termtab.update (t, (x, thm::thms)) regs 
15837  252 
end; 
253 
end; 

254 

16736
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

255 

15837  256 
(** theory data **) 
15596  257 

16458  258 
structure GlobalLocalesData = TheoryDataFun 
259 
(struct 

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

15837  264 
3rd entry: registrations, indexed by locale name *) 
11896  265 

15596  266 
val empty = (NameSpace.empty, Symtab.empty, Symtab.empty); 
12063  267 
val copy = I; 
16458  268 
val extend = I; 
12289  269 

19278  270 
fun join_locs _ ({predicate, import, elems, params, lparams, abbrevs, regs}: locale, 
19018
88b4979193d8
added abbreviations: activated by init, no expressions yet;
wenzelm
parents:
18964
diff
changeset

271 
{elems = elems', abbrevs = abbrevs', regs = regs', ...}: locale) = 
88b4979193d8
added abbreviations: activated by init, no expressions yet;
wenzelm
parents:
18964
diff
changeset

272 
{predicate = predicate, 
88b4979193d8
added abbreviations: activated by init, no expressions yet;
wenzelm
parents:
18964
diff
changeset

273 
import = import, 
17496  274 
elems = gen_merge_lists (eq_snd (op =)) elems elems', 
16736
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

275 
params = params, 
19278  276 
lparams = lparams, 
19018
88b4979193d8
added abbreviations: activated by init, no expressions yet;
wenzelm
parents:
18964
diff
changeset

277 
abbrevs = Library.merge (eq_snd (op =)) (abbrevs, abbrevs'), 
16736
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

278 
regs = merge_alists regs regs'}; 
16458  279 
fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) = 
15596  280 
(NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2), 
19025  281 
Symtab.join (K Registrations.join) (regs1, regs2)); 
12289  282 

15596  283 
fun print _ (space, locs, _) = 
16346  284 
Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs))) 
12014  285 
> Pretty.writeln; 
16458  286 
end); 
11896  287 

18708  288 
val _ = Context.add_setup GlobalLocalesData.init; 
15801  289 

290 

15624
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 
(** context data **) 
11896  293 

16458  294 
structure LocalLocalesData = ProofDataFun 
295 
(struct 

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

296 
val name = "Isar/locales"; 
15837  297 
type T = Registrations.T Symtab.table; 
298 
(* registrations, indexed by locale name *) 

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

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

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

302 

18708  303 
val _ = Context.add_setup LocalLocalesData.init; 
12289  304 

12277  305 

306 
(* access locales *) 

307 

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

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

309 

16458  310 
val intern = NameSpace.intern o #1 o GlobalLocalesData.get; 
311 
val extern = NameSpace.extern o #1 o GlobalLocalesData.get; 

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

312 

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

16458  315 
(Sign.declare_name thy name space, locs, regs)); 
11896  316 

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

318 
GlobalLocalesData.map (fn (space, locs, regs) => 
17412  319 
(space, Symtab.update (name, loc) locs, regs)); 
320 

321 
fun get_locale thy name = Symtab.lookup (#2 (GlobalLocalesData.get thy)) name; 

11896  322 

12014  323 
fun the_locale thy name = 
324 
(case get_locale thy name of 

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

11896  327 

18806  328 
fun change_locale name f thy = 
329 
let 

19278  330 
val {predicate, import, elems, params, lparams, abbrevs, regs} = the_locale thy name; 
331 
val (predicate', import', elems', params', lparams', abbrevs', regs') = 

332 
f (predicate, import, elems, params, lparams, abbrevs, regs); 

18806  333 
in 
334 
put_locale name {predicate = predicate', import = import', elems = elems', 

19278  335 
params = params', lparams = lparams', abbrevs = abbrevs', regs = regs'} thy 
18806  336 
end; 
337 

12046  338 

15596  339 
(* access registrations *) 
340 

15696  341 
(* Ids of global registrations are varified, 
342 
Ids of local registrations are not. 

343 
Thms of registrations are never varified. *) 

344 

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

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

346 

15696  347 
fun gen_get_registrations get thy_ctxt name = 
17412  348 
case Symtab.lookup (get thy_ctxt) name of 
15696  349 
NONE => [] 
15837  350 
 SOME reg => Registrations.dest reg; 
15696  351 

352 
val get_global_registrations = 

353 
gen_get_registrations (#3 o GlobalLocalesData.get); 

354 
val get_local_registrations = 

355 
gen_get_registrations LocalLocalesData.get; 

356 

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

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

361 

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

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

364 
val get_local_registration = 
16458  365 
gen_get_registration LocalLocalesData.get ProofContext.theory_of; 
15596  366 

18343  367 
val test_global_registration = is_some oo get_global_registration; 
368 
val test_local_registration = is_some oo get_local_registration; 

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

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

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

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

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

373 
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

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

375 

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

376 

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

378 

16458  379 
fun gen_put_registration map_data thy_of (name, ps) attn thy_ctxt = 
15837  380 
map_data (fn regs => 
381 
let 

16458  382 
val thy = thy_of thy_ctxt; 
18343  383 
val reg = the_default Registrations.empty (Symtab.lookup regs name); 
16458  384 
val (reg', sups) = Registrations.insert thy (ps, attn) reg; 
15837  385 
val _ = if not (null sups) then warning 
386 
("Subsumed interpretation(s) of locale " ^ 

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

390 
else (); 

17412  391 
in Symtab.update (name, reg') regs end) thy_ctxt; 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

392 

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

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

394 
gen_put_registration (fn f => 
16458  395 
GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, f regs))) I; 
15837  396 
val put_local_registration = 
16458  397 
gen_put_registration LocalLocalesData.map ProofContext.theory_of; 
15596  398 

18806  399 
fun put_registration_in_locale name id = 
19278  400 
change_locale name (fn (predicate, import, elems, params, lparams, abbrevs, regs) => 
401 
(predicate, import, elems, params, lparams, abbrevs, regs @ [(id, [])])); 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

402 

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

403 

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

404 
(* add witness theorem to registration in theory or context, 
15596  405 
ignored if registration not present *) 
406 

18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

407 
fun add_witness (name, ps) thm = 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

408 
Symtab.map_entry name (Registrations.add_witness ps thm); 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

409 

1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

410 
fun add_global_witness id thm = 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

411 
GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, add_witness id thm regs)); 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

412 

1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

413 
val add_local_witness = LocalLocalesData.map oo add_witness; 
15596  414 

18806  415 
fun add_witness_in_locale name id thm = 
19278  416 
change_locale name (fn (predicate, import, elems, params, lparams, abbrevs, regs) => 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

417 
let 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

418 
fun add (id', thms) = 
18806  419 
if id = id' then (id', thm :: thms) else (id', thms); 
19278  420 
in (predicate, import, elems, params, lparams, abbrevs, map add regs) end); 
15596  421 

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

422 

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

423 
(* printing of registrations *) 
15596  424 

17138  425 
fun gen_print_registrations get_regs mk_ctxt msg show_wits loc thy_ctxt = 
15596  426 
let 
15703  427 
val ctxt = mk_ctxt thy_ctxt; 
428 
val thy = ProofContext.theory_of ctxt; 

429 

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

17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

431 
fun prt_inst ts = 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

432 
Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts)); 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

433 
fun prt_attn (prfx, atts) = 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

434 
Pretty.breaks (Pretty.str prfx :: Args.pretty_attribs ctxt atts); 
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

435 
fun prt_thm (_, th) = Pretty.quote (ProofContext.pretty_thm ctxt th); 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

436 
fun prt_thms thms = 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

437 
Pretty.enclose "[" "]" (Pretty.breaks (map prt_thm thms)); 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

438 
fun prt_reg (ts, (("", []), thms)) = 
17138  439 
if show_wits 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

440 
then Pretty.block [prt_inst ts, Pretty.fbrk, prt_thms thms] 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

441 
else prt_inst ts 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

442 
 prt_reg (ts, (attn, thms)) = 
17138  443 
if show_wits 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

444 
then Pretty.block ((prt_attn attn @ 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

445 
[Pretty.str ":", Pretty.brk 1, prt_inst ts, Pretty.fbrk, 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

446 
prt_thms thms])) 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

447 
else Pretty.block ((prt_attn attn @ 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

448 
[Pretty.str ":", Pretty.brk 1, prt_inst ts])); 
15703  449 

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

451 
val regs = get_regs thy_ctxt; 
17412  452 
val loc_regs = Symtab.lookup regs loc_int; 
15596  453 
in 
454 
(case loc_regs of 

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

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

458 
val r'' = Library.sort_wrt (fn (_, ((prfx, _), _)) => prfx) r'; 
17355  459 
in Pretty.big_list ("interpretations in " ^ msg ^ ":") 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

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

461 
end) 
15596  462 
> Pretty.writeln 
463 
end; 

464 

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

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

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

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

469 
gen_print_registrations LocalLocalesData.get 
15703  470 
I "context"; 
17138  471 
fun print_local_registrations show_wits loc ctxt = 
472 
(print_global_registrations show_wits loc (ProofContext.theory_of ctxt); 

473 
print_local_registrations' show_wits loc ctxt); 

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

474 

15596  475 

12277  476 
(* diagnostics *) 
12273  477 

12277  478 
fun err_in_locale ctxt msg ids = 
479 
let 

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

481 
fun prt_id (name, parms) = 
16458  482 
[Pretty.block (Pretty.breaks (map Pretty.str (extern thy name :: parms)))]; 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset

483 
val prt_ids = flat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids)); 
12502  484 
val err_msg = 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

18678  488 
in error err_msg end; 
12063  489 

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

490 
fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids'); 
12277  491 

492 

12046  493 

18137  494 
(** witnesses  protected facts **) 
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

495 

1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

496 
fun assume_protected thy t = 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

497 
(t, Goal.protect (Thm.assume (Thm.cterm_of thy t))); 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

498 

1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

499 
fun prove_protected thy t tac = 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

500 
(t, Goal.prove thy [] [] (Logic.protect t) (fn _ => 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

501 
Tactic.rtac Drule.protectI 1 THEN tac)); 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

502 

1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

503 
val conclude_protected = Goal.conclude #> Goal.norm_hhf; 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

504 

1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

505 
fun satisfy_protected pths thm = 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

506 
let 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

507 
fun satisfy chyp = 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

508 
(case find_first (fn (t, _) => Thm.term_of chyp aconv t) pths of 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

509 
NONE => I 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

510 
 SOME (_, th) => Drule.implies_intr_protected [chyp] #> Goal.comp_hhf th); 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

511 
in fold satisfy (#hyps (Thm.crep_thm thm)) thm end; 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

512 

1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

513 

1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

514 

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

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

516 

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

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

518 

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

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

520 
let 
16861  521 
val tvars = rev (fold Term.add_tvarsT Ts []); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

522 
val tfrees = map TFree 
14695  523 
(Term.invent_names (ProofContext.used_types ctxt) "'a" (length tvars) ~~ map #2 tvars); 
18343  524 
in map (fn ((xi, S), T) => (xi, (S, T))) (tvars ~~ tfrees) end; 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

525 

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

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

527 
let 
18343  528 
fun paramify NONE i = (NONE, i) 
529 
 paramify (SOME T) i = apfst SOME (TypeInfer.paramify_dummies T i); 

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

530 

18343  531 
val (Ts', maxidx') = fold_map paramify Ts maxidx; 
532 
val (Us', maxidx'') = fold_map paramify Us maxidx'; 

16947  533 
val thy = ProofContext.theory_of ctxt; 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

534 

18190  535 
fun unify (SOME T, SOME U) env = (Sign.typ_unify thy (U, T) env 
536 
handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], [])) 

537 
 unify _ env = env; 

538 
val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx''); 

15570  539 
val Vs = map (Option.map (Envir.norm_type unifier)) Us'; 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset

540 
val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map_filter I Vs)); 
15570  541 
in map (Option.map (Envir.norm_type unifier')) Vs end; 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

542 

19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset

543 
fun params_of elemss = distinct (eq_fst (op =)) (maps (snd o fst) elemss); 
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset

544 
fun params_of' elemss = distinct (eq_fst (op =)) (maps (snd o fst o fst) elemss); 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

545 
fun params_syn_of syn elemss = 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset

546 
distinct (eq_fst (op =)) (maps (snd o fst) elemss) > 
18343  547 
map (apfst (fn x => (x, the (Symtab.lookup syn x)))); 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

548 

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

549 

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

550 
(* CB: param_types has the following type: 
15531  551 
('a * 'b option) list > ('a * 'b) list *) 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset

552 
fun param_types ps = map_filter (fn (_, NONE) => NONE  (x, SOME T) => SOME (x, T)) ps; 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

553 

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

554 

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

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

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

558 

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

559 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

560 
(* Distinction of assumed vs. derived identifiers. 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

561 
The former may have axioms relating assumptions of the context to 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

562 
assumptions of the specification fragment (for locales with 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

563 
predicates). The latter have witness theorems relating assumptions of the 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

564 
specification fragment to assumptions of other (assumed) specification 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

565 
fragments. *) 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

566 

552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

567 
datatype 'a mode = Assumed of 'a  Derived of 'a; 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

568 

552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

569 
fun map_mode f (Assumed x) = Assumed (f x) 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

570 
 map_mode f (Derived x) = Derived (f x); 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

571 

18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

572 

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

573 
(* flatten expressions *) 
11896  574 

12510  575 
local 
12502  576 

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

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

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

579 
val param_decls = 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset

580 
maps (fn (((name, (ps, qs)), _), _) => map (rpair (name, ps)) qs) elemss 
18952  581 
> Symtab.make_list > Symtab.dest; 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

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

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

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

588 

18137  589 
fun unify_parms ctxt fixed_parms raw_parmss = 
12502  590 
let 
16458  591 
val thy = ProofContext.theory_of ctxt; 
12502  592 
val maxidx = length raw_parmss; 
593 
val idx_parmss = (0 upto maxidx  1) ~~ raw_parmss; 

594 

595 
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

596 
fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps); 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset

597 
val parms = fixed_parms @ maps varify_parms idx_parmss; 
12502  598 

18137  599 
fun unify T U envir = Sign.typ_unify thy (U, T) envir 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

600 
handle Type.TUNIFY => 
18137  601 
let val prt = Sign.string_of_typ thy in 
602 
raise TYPE ("unify_parms: failed to unify types " ^ 

603 
prt U ^ " and " ^ prt T, [U, T], []) 

604 
end; 

605 
fun unify_list (T :: Us) = fold (unify T) Us 

606 
 unify_list [] = I; 

18952  607 
val (unifier, _) = fold unify_list (map #2 (Symtab.dest (Symtab.make_list parms))) 
18137  608 
(Vartab.empty, maxidx); 
12502  609 

19061
ffbbac0261c9
removed distinct, renamed gen_distinct to distinct;
wenzelm
parents:
19025
diff
changeset

610 
val parms' = map (apsnd (Envir.norm_type unifier)) (distinct (eq_fst (op =)) parms); 
12502  611 
val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms')); 
612 

613 
fun inst_parms (i, ps) = 

19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset

614 
foldr Term.add_typ_tfrees [] (map_filter snd ps) 
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset

615 
> map_filter (fn (a, S) => 
12502  616 
let val T = Envir.norm_type unifier' (TVar ((a, i), S)) 
18137  617 
in if T = TFree (a, S) then NONE else SOME (a, T) end) 
618 
> Symtab.make; 

619 
in map inst_parms idx_parmss end; 

12502  620 

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

621 
in 
12502  622 

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

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

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

625 
 unify_elemss ctxt fixed_parms elemss = 
12502  626 
let 
18137  627 
val thy = ProofContext.theory_of ctxt; 
17756  628 
val envs = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss); 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

629 
fun inst ((((name, ps), mode), elems), env) = 
18137  630 
(((name, map (apsnd (Option.map (Element.instT_type env))) ps), 
631 
map_mode (map (fn (t, th) => 

632 
(Element.instT_term env t, Element.instT_thm thy env th))) mode), 

633 
map (Element.instT_ctxt thy env) elems); 

12839  634 
in map inst (elemss ~~ envs) end; 
12502  635 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

636 
(* like unify_elemss, but does not touch mode, additional 
16736
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

637 
parameter c_parms for enforcing further constraints (eg. syntax) *) 
18343  638 
(* FIXME avoid code duplication *) 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

639 

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

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

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

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

643 
let 
18137  644 
val thy = ProofContext.theory_of ctxt; 
645 
val envs = 

646 
unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss @ map single c_parms); 

17033  647 
fun inst ((((name, ps), (ps', mode)), elems), env) = 
18137  648 
(((name, map (apsnd (Option.map (Element.instT_type env))) ps), (ps', mode)), 
649 
map (Element.instT_ctxt thy env) elems); 

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

651 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

652 

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

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

656 
identifier). 

657 

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

659 
((name, ps), (ax_ps, axs)) 

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

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

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

663 
hence axioms may contain additional parameters from later fragments: 

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

665 

666 
Elements are enriched by identifierlike information: 

667 
(((name, ax_ps), axs), elems) 

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

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

670 
typeinstantiated. 

671 

672 
*) 

673 

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

674 
fun flatten_expr ctxt ((prev_idents, prev_syntax), expr) = 
12014  675 
let 
676 
val thy = ProofContext.theory_of ctxt; 

12263  677 

15531  678 
fun renaming (SOME x :: xs) (y :: ys) = (y, x) :: renaming xs ys 
679 
 renaming (NONE :: xs) (y :: ys) = renaming xs ys 

12273  680 
 renaming [] _ = [] 
18678  681 
 renaming xs [] = error ("Too many arguments in renaming: " ^ 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

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

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

684 
fun rename_parms top ren ((name, ps), (parms, mode)) = 
18137  685 
let val ps' = map (Element.rename ren) ps in 
18964  686 
(case duplicates (op =) ps' of 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

687 
[] => ((name, ps'), 
18137  688 
if top then (map (Element.rename ren) parms, 
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

689 
map_mode (map (fn (t, th) => 
18137  690 
(Element.rename_term ren t, Element.rename_thm ren th))) mode) 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

691 
else (parms, mode)) 
12289  692 
 dups => err_in_locale ctxt ("Duplicate parameters: " ^ commas_quote dups) [(name, ps')]) 
693 
end; 

12263  694 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

695 
(* add registrations of (name, ps), recursively; 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

696 
adjust hyps of witness theorems *) 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

697 

552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

698 
fun add_regs (name, ps) (ths, ids) = 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

699 
let 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

700 
val {params, regs, ...} = the_locale thy name; 
19278  701 
val ps' = map #1 params; 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

702 
val ren = map #1 ps' ~~ map (fn (x, _) => (x, NONE)) ps; 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

703 
(* dummy syntax, since required by rename *) 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

704 
val ps'' = map (fn ((p, _), (_, T)) => (p, T)) (ps ~~ ps'); 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

705 
val [env] = unify_parms ctxt ps [map (apsnd SOME) ps'']; 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

706 
(* propagate parameter types, to keep them consistent *) 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

707 
val regs' = map (fn ((name, ps), ths) => 
18137  708 
((name, map (Element.rename ren) ps), ths)) regs; 
17496  709 
val new_regs = gen_rems (eq_fst (op =)) (regs', ids); 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

710 
val new_ids = map fst new_regs; 
17485  711 
val new_idTs = map (apsnd (map (fn p => (p, (the o AList.lookup (op =) ps) p)))) new_ids; 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

712 

18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

713 
val new_ths = new_regs > map (fn (_, ths') => ths' > map (fn (t, th) => 
18137  714 
(t > Element.instT_term env > Element.rename_term ren, 
715 
th > Element.instT_thm thy env > Element.rename_thm ren > satisfy_protected ths))); 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

716 
val new_ids' = map (fn (id, ths) => 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

717 
(id, ([], Derived ths))) (new_ids ~~ new_ths); 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

718 
in 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset

719 
fold add_regs new_idTs (ths @ flat new_ths, ids @ new_ids') 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

720 
end; 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

721 

552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

722 
(* distribute toplevel axioms over assumed ids *) 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

723 

552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

724 
fun axiomify all_ps ((name, parms), (_, Assumed _)) axioms = 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

725 
let 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

726 
val {elems, ...} = the_locale thy name; 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset

727 
val ts = maps 
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset

728 
(fn (Assumes asms, _) => maps (map #1 o #2) asms 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

729 
 _ => []) 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset

730 
elems; 
19018
88b4979193d8
added abbreviations: activated by init, no expressions yet;
wenzelm
parents:
18964
diff
changeset

731 
val (axs1, axs2) = chop (length ts) axioms; 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

732 
in (((name, parms), (all_ps, Assumed axs1)), axs2) end 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

733 
 axiomify all_ps (id, (_, Derived ths)) axioms = 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

734 
((id, (all_ps, Derived ths)), axioms); 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

735 

17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

736 
(* identifiers of an expression *) 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

737 

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

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

740 
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

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

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

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

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

746 
the_locale thy name; 
19278  747 
val ps = map (#1 o #1) params; 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

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

749 
(* acyclic import dependencies *) 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

750 
val ids'' = ids' @ [((name, ps), ([], Assumed []))]; 
19278  751 
val (_, ids''') = add_regs (name, map #1 params) ([], ids''); 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

752 

552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

753 
val ids_ax = if top then fst 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

754 
(fold_map (axiomify ps) ids''' axioms) 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

755 
else ids'''; 
19278  756 
val syn = Symtab.make (map (apfst fst) params); 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

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

758 
 identify top (Rename (e, xs)) = 
12273  759 
let 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

760 
val (ids', parms', syn') = identify top e; 
12839  761 
val ren = renaming xs parms' 
18678  762 
handle ERROR msg => err_in_locale' ctxt msg ids'; 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

763 

19061
ffbbac0261c9
removed distinct, renamed gen_distinct to distinct;
wenzelm
parents:
19025
diff
changeset

764 
val ids'' = distinct (eq_fst (op =)) (map (rename_parms top ren) ids'); 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset

765 
val parms'' = distinct (op =) (maps (#2 o #1) ids''); 
18137  766 
val syn'' = syn' > Symtab.dest > map (Element.rename_var ren) > Symtab.make; 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

767 
(* check for conflicting syntax? *) 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

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

769 
 identify top (Merge es) = 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

770 
fold (fn e => fn (ids, parms, syn) => 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

771 
let 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

772 
val (ids', parms', syn') = identify top e 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

773 
in 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

774 
(merge_alists ids ids', 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

775 
merge_lists parms parms', 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

776 
merge_syntax ctxt ids' (syn, syn')) 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

777 
end) 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

778 
es ([], [], Symtab.empty); 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

779 

12014  780 

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

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

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

784 

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

785 
fun eval syn ((name, xs), axs) = 
12273  786 
let 
19278  787 
val {params = ps, lparams = qs, elems, ...} = the_locale thy name; 
16620
2a7f46324218
Proper treatment of betaredexes in witness theorems.
ballarin
parents:
16458
diff
changeset

788 
val ps' = map (apsnd SOME o #1) ps; 
18671  789 
fun lookup_syn x = (case Symtab.lookup syn x of SOME Structure => NONE  opt => opt); 
790 
val ren = map #1 ps' ~~ map (fn x => (x, lookup_syn x)) xs; 

13308  791 
val (params', elems') = 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

792 
if null ren then ((ps', qs), map #1 elems) 
18137  793 
else ((map (apfst (Element.rename ren)) ps', map (Element.rename ren) qs), 
794 
map (Element.rename_ctxt ren o #1) elems); 

795 
val elems'' = elems' > map (Element.map_ctxt 

796 
{var = I, typ = I, term = I, fact = I, attrib = I, 

797 
name = NameSpace.qualified (space_implode "_" xs)}); 

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

798 
in (((name, params'), axs), elems'') end; 
12307  799 

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

800 
(* type constraint for renamed parameter with syntax *) 
18343  801 
fun mixfix_type mx = 
18671  802 
SOME (Type.freeze_type (#1 (TypeInfer.paramify_dummies (TypeInfer.mixfixT mx) 0))); 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

803 

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

804 
(* compute identifiers and syntax, merge with previous ones *) 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

805 
val (ids, _, syn) = identify true expr; 
17496  806 
val idents = gen_rems (eq_fst (op =)) (ids, prev_idents); 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

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

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

809 
val raw_elemss = unique_parms ctxt (map (eval syntax) idents); 
18671  810 
val elemss = unify_elemss' ctxt [] raw_elemss (map (apsnd mixfix_type) (Symtab.dest syntax)); 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

811 
(* replace params in ids by params from axioms, 
17033  812 
adjust types in mode *) 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

814 
val all_params = param_types all_params'; 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

815 
val elemss' = map (fn (((name, _), (ps, mode)), elems) => 
17485  816 
(((name, map (fn p => (p, AList.lookup (op =) all_params p)) ps), mode), elems)) 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

817 
elemss; 
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

818 
fun inst_th (t, th) = let 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

821 
val [env] = unify_parms ctxt all_params [ps]; 
18137  822 
val t' = Element.instT_term env t; 
823 
val th' = Element.instT_thm thy env th; 

18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

824 
in (t', th') end; 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

825 
val final_elemss = map (fn ((id, mode), elems) => 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

826 
((id, map_mode (map inst_th) mode), elems)) elemss'; 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

827 

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

828 
in ((prev_idents @ idents, syntax), final_elemss) end; 
12046  829 

12510  830 
end; 
831 

12070  832 

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

833 
(* activate elements *) 
12273  834 

12510  835 
local 
836 

18671  837 
fun axioms_export axs _ hyps = 
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

838 
satisfy_protected axs 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

839 
#> Drule.implies_intr_list (Library.drop (length axs, hyps)) 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

840 
#> Seq.single; 
12263  841 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

842 

552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

843 
(* NB: derived ids contain only facts at this stage *) 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

844 

552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

845 
fun activate_elem _ ((ctxt, mode), Fixes fixes) = 
18671  846 
((ctxt > ProofContext.add_fixes_i fixes > snd, mode), []) 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

847 
 activate_elem _ ((ctxt, mode), Constrains _) = 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

848 
((ctxt, mode), []) 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

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

850 
let 
18728  851 
val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms; 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset

852 
val ts = maps (map #1 o #2) asms'; 
19018
88b4979193d8
added abbreviations: activated by init, no expressions yet;
wenzelm
parents:
18964
diff
changeset

853 
val (ps, qs) = chop (length ts) axs; 
17856  854 
val (_, ctxt') = 
18671  855 
ctxt > fold ProofContext.fix_frees ts 
856 
> ProofContext.add_assms_i (axioms_export ps) asms'; 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

857 
in ((ctxt', Assumed qs), []) end 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

858 
 activate_elem _ ((ctxt, Derived ths), Assumes asms) = 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

859 
((ctxt, Derived ths), []) 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

860 
 activate_elem _ ((ctxt, Assumed axs), Defines defs) = 
15596  861 
let 
18728  862 
val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs; 
17856  863 
val (_, ctxt') = 
18831  864 
ctxt > ProofContext.add_assms_i LocalDefs.def_export 
15703  865 
(defs' > map (fn ((name, atts), (t, ps)) => 
18952  866 
let val ((c, _), t') = LocalDefs.cert_def ctxt t 
19585  867 
in ((if name = "" then Thm.def_name c else name, atts), [(t', ps)]) end)) 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

868 
in ((ctxt', Assumed axs), []) end 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

869 
 activate_elem _ ((ctxt, Derived ths), Defines defs) = 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

870 
((ctxt, Derived ths), []) 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

871 
 activate_elem is_ext ((ctxt, mode), Notes facts) = 
15596  872 
let 
18728  873 
val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts; 
17856  874 
val (res, ctxt') = ctxt > ProofContext.note_thmss_i facts'; 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

875 
in ((ctxt', mode), if is_ext then res else []) end; 
12502  876 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

877 
fun activate_elems (((name, ps), mode), elems) ctxt = 
17033  878 
let 
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

879 
val thy = ProofContext.theory_of ctxt; 
17033  880 
val ((ctxt', _), res) = 
881 
foldl_map (activate_elem (name = "")) ((ProofContext.qualified_names ctxt, mode), elems) 

18678  882 
handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)] 
15696  883 
val ctxt'' = if name = "" then ctxt' 
884 
else let 

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

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

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

887 
in case mode of 
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

888 
Assumed axs => 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

889 
fold (add_local_witness (name, ps') o assume_protected thy o #1) axs ctxt'' 
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset

890 
 Derived ths => fold (add_local_witness (name, ps')) ths ctxt'' 
15696  891 
end 
16144  892 
in (ProofContext.restore_naming ctxt ctxt'', res) end; 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

893 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

894 
fun activate_elemss prep_facts = 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

895 
fold_map (fn (((name, ps), mode), raw_elems) => fn ctxt => 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

896 
let 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

897 
val elems = map (prep_facts ctxt) raw_elems; 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset

898 
val (ctxt', res) = apsnd flat 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

899 
(activate_elems (((name, ps), mode), elems) ctxt); 
18137  900 
val elems' = elems > map (Element.map_ctxt 
901 
{name = I, var = I, typ = I, term = I, fact = I, attrib = Args.closure}); 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

902 
in ((((name, ps), elems'), res), ctxt') end); 
12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

903 

12546  904 
in 
905 

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

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

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

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

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

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

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

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

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

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

916 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

917 
fun activate_facts prep_facts (ctxt, args) = 
18806  918 
let val ((elemss, factss), ctxt') = activate_elemss prep_facts args ctxt >> split_list 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset

919 
in (ctxt', (elemss, flat factss)) end; 
15703  920 

12510  921 
end; 
922 

12307  923 

15696  924 

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

926 

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

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

928 

16458  929 
fun intern_expr thy (Locale xname) = Locale (intern thy xname) 
930 
 intern_expr thy (Merge exprs) = Merge (map (intern_expr thy) exprs) 

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

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

932 

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

933 

19293  934 
(* experimental code for type inference *) 
935 

936 
local 

937 

938 
fun declare_int_elem (ctxt, Fixes fixes) = 

939 
(ctxt > ProofContext.add_fixes_i (map (fn (x, T, mx) => 

940 
(x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes) > snd, []) 

941 
 declare_int_elem (ctxt, _) = (ctxt, []); 

942 

943 
fun declare_ext_elem prep_vars (ctxt, Fixes fixes) = 

944 
let val (vars, _) = prep_vars fixes ctxt 

945 
in (ctxt > ProofContext.add_fixes_i vars > snd, []) end 

946 
 declare_ext_elem prep_vars (ctxt, Constrains csts) = 

947 
let val (_, ctxt') = prep_vars (map (fn (x, T) => (x, SOME T, NoSyn)) csts) ctxt 

948 
in (ctxt', []) end 

949 
 declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms) 

19585  950 
 declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, ps)]) defs) 
19293  951 
 declare_ext_elem _ (ctxt, Notes facts) = (ctxt, []); 
952 

953 
fun declare_elems prep_vars (ctxt, (((name, ps), Assumed _), elems)) = 

954 
let val (ctxt', propps) = 

955 
(case elems of 

956 
Int es => foldl_map declare_int_elem (ctxt, es) 

957 
 Ext e => foldl_map (declare_ext_elem prep_vars) (ctxt, [e])) 

958 
handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)] 

959 
in (ctxt', propps) end 

960 
 declare_elems _ (ctxt, ((_, Derived _), elems)) = (ctxt, []); 

961 

962 
in 

963 

964 
(* The Plan: 

965 
 tell context about parameters and their syntax (possibly also types) 

966 
 add declarations to context 

967 
 retrieve parameter types 

968 
*) 

969 

970 
end; (* local *) 

971 

972 

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

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

974 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

975 
(* flatten (ctxt, prep_expr) ((ids, syn), expr) 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

976 
normalises expr (which is either a locale 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

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

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

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

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

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

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

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

985 

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

988 
identifierlike information of the element is as follows: 

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

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

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

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

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

994 

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

995 
fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let 
18137  996 
val ids' = ids @ [(("", map #1 fixes), ([], Assumed []))] 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

997 
in 
18137  998 
((ids', 
999 
merge_syntax ctxt ids' 

1000 
(syn, Symtab.make (map (fn fx => (#1 fx, #3 fx)) fixes)) 

1001 
handle Symtab.DUPS xs => err_in_locale ctxt 

1002 
("Conflicting syntax for parameters: " ^ commas_quote xs) 

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

1003 
(map #1 ids')), 
18137  1004 
[((("", map (rpair NONE o #1) fixes), Assumed []), Ext (Fixes fixes))]) 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

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

1006 
 flatten _ ((ids, syn), Elem elem) = 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

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

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

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

1010 

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

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

1012 

12839  1013 
local 
1014 

12727  1015 
fun declare_int_elem (ctxt, Fixes fixes) = 
18671  1016 
(ctxt > ProofContext.add_fixes_i (map (fn (x, T, mx) => 
1017 
(x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes) > snd, []) 

12727  1018 
 declare_int_elem (ctxt, _) = (ctxt, []); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

1019 

18671  1020 
fun declare_ext_elem prep_vars (ctxt, Fixes fixes) = 
1021 
let val (vars, _) = prep_vars fixes ctxt 

1022 
in (ctxt > ProofContext.add_fixes_i vars > snd, []) end 

1023 
 declare_ext_elem prep_vars (ctxt, Constrains csts) = 

1024 
let val (_, ctxt') = prep_vars (map (fn (x, T) => (x, SOME T, NoSyn)) csts) ctxt 

1025 
in (ctxt', []) end 

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

1026 
 declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms) 
19585  1027 
 declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, ps)]) defs) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

1029 

18671  1030 
fun declare_elems prep_vars (ctxt, (((name, ps), Assumed _), elems)) = 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1031 
let val (ctxt', propps) = 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1032 
(case elems of 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1033 
Int es => foldl_map declare_int_elem (ctxt, es) 
18671  1034 
 Ext e => foldl_map (declare_ext_elem prep_vars) (ctxt, [e])) 
18678  1035 
handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)] 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1036 
in (ctxt', propps) end 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1037 
 declare_elems _ (ctxt, ((_, Derived _), elems)) = (ctxt, []); 
12727  1038 

12839  1039 
in 
1040 

18671  1041 
fun declare_elemss prep_vars fixed_params raw_elemss ctxt = 
12727  1042 
let 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

1044 
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

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

1046 
val ctxt_with_fixed = 
16028  1047 
fold ProofContext.declare_term (map Free fixed_params) ctxt; 
12727  1048 
val int_elemss = 
1049 
raw_elemss 

19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset

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

1051 
> unify_elemss ctxt_with_fixed fixed_params; 
12727  1052 
val (_, raw_elemss') = 
1053 
foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es))  x => x) 

1054 
(int_elemss, raw_elemss); 

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

1056 

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

1058 

12839  1059 
local 
1060 

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

1062 

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

12502  1065 

18190  1066 
fun bind_def ctxt (name, ps) eq (xs, env, ths) = 
12839  1067 
let 
18831  1068 
val ((y, T), b) = LocalDefs.abs_def eq; 
13308  1069 
val b' = norm_term env b; 
16458  1070 
val th = abstract_thm (ProofContext.theory_of ctxt) eq; 
13308  1071 
fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)]; 
12839  1072 
in 
13308  1073 
conditional (exists (equal y o #1) xs) (fn () => 
1074 
err "Attempt to define previously specified variable"); 

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

1076 
err "Attempt to redefine variable"); 

16861  1077 
(Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths) 
12839  1078 
end; 
12575  1079 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1080 

552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1081 
(* CB: for finish_elems (Int and Ext), 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1082 
extracts specification, only of assumed elements *) 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1083 

18190  1084 
fun eval_text _ _ _ (Fixes _) text = text 
1085 
 eval_text _ _ _ (Constrains _) text = text 

1086 
 eval_text _ (_, Assumed _) is_ext (Assumes asms) 

1087 
(((exts, exts'), (ints, ints')), (xs, env, defs)) = 

13394  1088 
let 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset

1089 
val ts = maps (map #1 o #2) asms; 
13394  1090 
val ts' = map (norm_term env) ts; 
1091 
val spec' = 

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

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

16861  1094 
in (spec', (fold Term.add_frees ts' xs, env, defs)) end 
18190  1095 
 eval_text _ (_, Derived _) _ (Assumes _) text = text 
1096 
 eval_text ctxt (id, Assumed _) _ (Defines defs) (spec, binds) = 

1097 
(spec, fold (bind_def ctxt id o #1 o #2) defs binds) 

1098 
 eval_text _ (_, Derived _) _ (Defines _) text = text 

1099 
 eval_text _ _ _ (Notes _) text = text; 

13308  1100 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1101 

552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1102 
(* for finish_elems (Int), 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1103 
remove redundant elements of derived identifiers, 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1104 
turn assumptions and definitions into facts, 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1105 
adjust hypotheses of facts using witness theorems *) 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1106 

17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

1107 
fun finish_derived _ _ (Assumed _) (Fixes fixes) = SOME (Fixes fixes) 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

1108 
 finish_derived _ _ (Assumed _) (Constrains csts) = SOME (Constrains csts) 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

1109 
 finish_derived _ _ (Assumed _) (Assumes asms) = SOME (Assumes asms) 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

1110 
 finish_derived _ _ (Assumed _) (Defines defs) = SOME (Defines defs) 
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

1111 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1112 
 finish_derived _ _ (Derived _) (Fixes _) = NONE 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1113 
 finish_derived _ _ (Derived _) (Constrains _) = NONE 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1114 
 finish_derived sign wits (Derived _) (Assumes asms) = asms 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

1115 
> map (apsnd (map (fn (a, _) => ([Thm.assume (cterm_of sign a)], [])))) 
18137  1116 
> Notes > Element.map_ctxt_values I I (satisfy_protected wits) > SOME 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1117 
 finish_derived sign wits (Derived _) (Defines defs) = defs 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

1118 
> map (apsnd (fn (d, _) => [([Thm.assume (cterm_of sign d)], [])])) 
18137  1119 
> Notes > Element.map_ctxt_values I I (satisfy_protected wits) > SOME 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1120 

17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

1121 
 finish_derived _ wits _ (Notes facts) = (Notes facts) 
18137  1122 
> Element.map_ctxt_values I I (satisfy_protected wits) > SOME; 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1123 

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

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

1125 

13308  1126 
fun closeup _ false elem = elem 
1127 
 closeup ctxt true elem = 

12839  1128 
let 
13308  1129 
fun close_frees t = 
1130 
let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1) 

16861  1131 
(Term.add_frees t [])) 
13308  1132 
in Term.list_all_free (frees, t) end; 
1133 

1134 
fun no_binds [] = [] 

18678  1135 
 no_binds _ = error "Illegal term bindings in locale element"; 
13308  1136 
in 
1137 
(case elem of 

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

19585  1139 
(a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps))) 
13308  1140 
 Defines defs => Defines (defs > map (fn (a, (t, ps)) => 
18831  1141 
(a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps)))) 
13308  1142 
 e => e) 
1143 
end; 

12839  1144 

12502  1145 

12839  1146 
fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) => 
17271  1147 
(x, AList.lookup (op =) parms x, mx)) fixes) 
18899
a8e913c93578
theorem(_in_locale): Element.statement, Obtain.statement;
wenzelm
parents:
18890
diff
changeset

1148 
 finish_ext_elem parms _ (Constrains _, _) = Constrains [] 
12839  1149 
 finish_ext_elem _ close (Assumes asms, propp) = 
1150 
close (Assumes (map #1 asms ~~ propp)) 

1151 
 finish_ext_elem _ close (Defines defs, propp) = 

19585  1152 
close (Defines (map #1 defs ~~ map (fn [(t, ps)] => (t, ps)) propp)) 
12839  1153 
 finish_ext_elem _ _ (Notes facts, _) = Notes facts; 
1154 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1155 

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

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

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

1159 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1160 
fun finish_parms parms (((name, ps), mode), elems) = 
17485  1161 
(((name, map (fn (x, _) => (x, AList.lookup (op =) parms x)) ps), mode), elems); 
12839  1162 

17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1163 
fun finish_elems ctxt parms _ ((text, wits), ((id, Int e), _)) = 
12839  1164 
let 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1165 
val [(id' as (_, mode), es)] = unify_elemss ctxt parms [(id, e)]; 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1166 
val wits' = case mode of Assumed _ => wits  Derived ths => wits @ ths; 
18190  1167 
val text' = fold (eval_text ctxt id' false) es text; 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset

1168 
val es' = map_filter 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1169 
(finish_derived (ProofContext.theory_of ctxt) wits' mode) es; 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1170 
in ((text', wits'), (id', map Int es')) end 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1171 
 finish_elems ctxt parms do_close ((text, wits), ((id, Ext e), [propp])) = 
13308  1172 
let 
1173 
val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp); 

18190  1174 
val text' = eval_text ctxt id true e' text; 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1175 
in ((text', wits), (id, [Ext e'])) end 
12839  1176 

1177 
in 

12510  1178 

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

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

1180 

13375  1181 
fun finish_elemss ctxt parms do_close = 
1182 
foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close); 

12839  1183 

1184 
end; 

1185 

16736
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

1186 

1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

1187 
(* CB: type inference and consistency checks for locales. 
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

1188 

1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

1189 
Works by building a context (through declare_elemss), extracting the 
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

1190 
required information and adjusting the context elements (finish_elemss). 
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

1191 
Can also universally close free vars in assms and defs. This is only 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1192 
needed for Ext elements and controlled by parameter do_close. 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1193 

552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1194 
Only elements of assumed identifiers are considered. 
16736
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

1195 
*) 
15127  1196 

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

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

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

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

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

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

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

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

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

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

1209 
external elements in raw_elemss. *) 
18550
59b89f625d68
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents:
18546
diff
changeset

1210 
fun prep_prop raw_propp (raw_ctxt, raw_concl) = 
18450
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18421
diff
changeset

1211 
let 
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18421
diff
changeset

1212 
(* CB: add type information from fixed_params to context (declare_term) *) 
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18421
diff
changeset

1213 
(* CB: process patterns (conclusion and external elements only) *) 
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18421
diff
changeset

1214 
val (ctxt, all_propp) = 
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18421
diff
changeset

1215 
prepp (fold ProofContext.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp); 
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18421
diff
changeset

1216 
(* CB: add type information from conclusion and external elements to context *) 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset

1217 
val ctxt = fold ProofContext.declare_term (maps (map fst) all_propp) ctxt; 
18450
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18421
diff
changeset

1218 
(* CB: resolve schematic variables (patterns) in conclusion and external elements. *) 
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18421
diff
changeset

1219 
val all_propp' = map2 (curry (op ~~)) 
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18421
diff
changeset

1220 
(#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp); 
19018
88b4979193d8
added abbreviations: activated by init, no expressions yet;
wenzelm
parents:
18964
diff
changeset

1221 
val (concl, propp) = chop (length raw_concl) all_propp'; 
18550
59b89f625d68
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents:
18546
diff
changeset

1222 
in (propp, (ctxt, concl)) end 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1223 

18550
59b89f625d68
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents:
18546
diff
changeset

1224 
val (proppss, (ctxt, concl)) = 
59b89f625d68
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents:
18546
diff
changeset

1225 
(fold_burrow o fold_burrow) prep_prop raw_proppss (raw_ctxt, raw_concl); 
12502  1226 

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

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

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

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

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

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

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

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

1235 
(* CB: extract information from assumes and defines elements 
16169
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

1236 
(fixes, constrains and notes in raw_elemss don't have an effect on 
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

1237 
text and elemss), compute final form of context elements. *) 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1238 
val ((text, _), elemss) = finish_elemss ctxt parms do_close 
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1239 
((((([], []), ([], [])), ([], [], [])), []), raw_elemss ~~ proppss); 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

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

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

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

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

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

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

1247 
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

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