author  wenzelm 
Wed, 09 Aug 2006 00:12:38 +0200  
changeset 20366  867696dc64fc 
parent 20317  6e070b33e72b 
child 20548  8ef25fe585a8 
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 

19942
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

8 
Draws 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 
20035
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

10 
metalogic. Furthermore, structured import of contexts (with merge 
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

11 
and rename operations) are provided, 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. 
19942
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

23 
[2] Clemens Ballarin. Interpretation of Locales in Isabelle: Managing 
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

24 
Dependencies between Locales. Technical Report TUMI0607, Technische 
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

25 
Universitaet Muenchen, 2006. 
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

26 
[3] Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and 
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

27 
Proof Contexts. In J.M. Borwein and W.M. Farmer, MKM 2006, LNAI 4108, 
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

28 
pages 3143, 2006. 
11896  29 
*) 
30 

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

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

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

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

34 
 test subsumption of interpretations when merging theories 
16169
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

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

36 

11896  37 
signature LOCALE = 
38 
sig 

12273  39 
datatype expr = 
40 
Locale of string  

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

41 
Rename of expr * (string * mixfix option) option list  
12273  42 
Merge of expr list 
43 
val empty: expr 

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

45 

16458  46 
val intern: theory > xstring > string 
47 
val extern: theory > string > xstring 

19991
0c9650664d47
Locales no longer generate views. The following functions have changed
ballarin
parents:
19984
diff
changeset

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

49 

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

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

51 

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

52 
val parameters_of: theory > string > 
18917  53 
((string * typ) * mixfix) list 
19276  54 
val parameters_of_expr: theory > expr > 
55 
((string * typ) * mixfix) list 

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

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

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

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

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

60 

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

61 
(* Processing of locale statements *) 
18137  62 
val read_context_statement: xstring option > Element.context element list > 
19585  63 
(string * string list) list list > Proof.context > 
19991
0c9650664d47
Locales no longer generate views. The following functions have changed
ballarin
parents:
19984
diff
changeset

64 
string option * Proof.context * Proof.context * (term * term list) list list 
18137  65 
val cert_context_statement: string option > Element.context_i element list > 
19585  66 
(term * term list) list list > Proof.context > 
19991
0c9650664d47
Locales no longer generate views. The following functions have changed
ballarin
parents:
19984
diff
changeset

67 
string option * Proof.context * Proof.context * (term * term list) list list 
19780  68 
val read_expr: expr > Element.context list > Proof.context > 
69 
Element.context_i list * Proof.context 

70 
val cert_expr: expr > Element.context_i list > Proof.context > 

71 
Element.context_i list * Proof.context 

15596  72 

73 
(* Diagnostic functions *) 

12758  74 
val print_locales: theory > unit 
18137  75 
val print_locale: theory > bool > expr > Element.context list > unit 
17138  76 
val print_global_registrations: bool > string > theory > unit 
18617  77 
val print_local_registrations': bool > string > Proof.context > unit 
78 
val print_local_registrations: bool > string > Proof.context > unit 

18137  79 

18917  80 
val add_locale: bool > bstring > expr > Element.context list > theory 
19293  81 
> (string * Proof.context (*body context!*)) * theory 
18917  82 
val add_locale_i: bool > bstring > expr > Element.context_i list > theory 
19293  83 
> (string * Proof.context (*body context!*)) * theory 
15596  84 

15696  85 
(* Storing results *) 
15703  86 
val note_thmss: string > xstring > 
18806  87 
((string * Attrib.src list) * (thmref * Attrib.src list) list) list > 
20366
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

88 
theory > ((string * thm list) list * (string * thm list) list) * Proof.context 
15703  89 
val note_thmss_i: string > string > 
18806  90 
((string * Attrib.src list) * (thm list * Attrib.src list) list) list > 
20366
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

91 
theory > ((string * thm list) list * (string * thm list) list) * Proof.context 
18806  92 
val add_thmss: string > string > 
93 
((string * Attrib.src list) * (thm list * Attrib.src list) list) list > 

19991
0c9650664d47
Locales no longer generate views. The following functions have changed
ballarin
parents:
19984
diff
changeset

94 
Proof.context > 
18806  95 
((string * thm list) list * (string * thm list) list) * Proof.context 
20037  96 
val add_term_syntax: string > (Proof.context > Proof.context) > Proof.context > Proof.context 
18137  97 

20366
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

98 
val theorem: string > Method.text option > 
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

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

100 
string * Attrib.src list > Element.context element list > Element.statement > 
17355  101 
theory > Proof.state 
20366
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

102 
val theorem_i: string > Method.text option > 
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

103 
(thm list list > Proof.context > Proof.context) > 
18907  104 
string * Attrib.src list > Element.context_i element list > Element.statement_i > 
17355  105 
theory > Proof.state 
17856  106 
val theorem_in_locale: string > Method.text option > 
20366
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

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

108 
xstring > string * Attrib.src list > Element.context element list > Element.statement > 
17355  109 
theory > Proof.state 
17856  110 
val theorem_in_locale_i: string > Method.text option > 
20366
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

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

115 
string * Attrib.src list > Element.context element list > Element.statement > 
17355  116 
theory > Proof.state 
20366
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

117 
val interpretation: (Proof.context > Proof.context) > 
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

118 
string * Attrib.src list > expr > string option list > 
17355  119 
theory > Proof.state 
20366
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

120 
val interpretation_in_locale: (Proof.context > Proof.context) > 
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

121 
xstring * expr > theory > Proof.state 
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

122 
val interpret: (Proof.state > Proof.state Seq.seq) > 
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

123 
string * Attrib.src list > expr > string option list > 
17355  124 
bool > Proof.state > Proof.state 
11896  125 
end; 
12839  126 

12289  127 
structure Locale: LOCALE = 
11896  128 
struct 
129 

19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

130 
fun legacy_unvarifyT thm = 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

131 
let 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

132 
val cT = Thm.ctyp_of (Thm.theory_of_thm thm); 
20307  133 
val tvars = rev (Drule.fold_terms Term.add_tvars thm []); 
134 
val tfrees = map (fn ((x, _), S) => SOME (cT (TFree (x, S)))) tvars; 

19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

135 
in Drule.instantiate' tfrees [] thm end; 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

136 

fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

137 
fun legacy_unvarify raw_thm = 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

138 
let 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

139 
val thm = legacy_unvarifyT raw_thm; 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

140 
val ct = Thm.cterm_of (Thm.theory_of_thm thm); 
20307  141 
val vars = rev (Drule.fold_terms Term.add_vars thm []); 
142 
val frees = map (fn ((x, _), T) => SOME (ct (Free (x, T)))) vars; 

19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

143 
in Drule.instantiate' [] frees thm end; 
19780  144 

20307  145 

12273  146 
(** locale elements and expressions **) 
11896  147 

18137  148 
datatype ctxt = datatype Element.ctxt; 
17355  149 

12273  150 
datatype expr = 
151 
Locale of string  

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

152 
Rename of expr * (string * mixfix option) option list  
12273  153 
Merge of expr list; 
11896  154 

12273  155 
val empty = Merge []; 
156 

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

158 
Elem of 'a  Expr of expr; 
12273  159 

18137  160 
fun map_elem f (Elem e) = Elem (f e) 
161 
 map_elem _ (Expr e) = Expr e; 

162 

12070  163 
type locale = 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

164 
{axiom: Element.witness list, 
19942
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

165 
(* For locales that define predicates this is [A [A]], where A is the locale 
20317  166 
specification. Otherwise []. 
167 
Only required to generate the right witnesses for locales with predicates. *) 

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

168 
import: expr, (*dynamic import*) 
19783  169 
elems: (Element.context_i * stamp) list, 
170 
(* Static content, neither Fixes nor Constrains elements *) 

19278  171 
params: ((string * typ) * mixfix) list, (*all params*) 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

172 
lparams: string list, (*local params*) 
19662
2f5d076fde32
replaced abbrevs by term_syntax, which is both simpler and more general;
wenzelm
parents:
19585
diff
changeset

173 
term_syntax: ((Proof.context > Proof.context) * stamp) list, (* FIXME depend on morphism *) 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

174 
regs: ((string * string list) * Element.witness list) list, 
19780  175 
(* Registrations: indentifiers and witnesses of locales interpreted in the locale. *) 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

176 
intros: thm list * thm list} 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

177 
(* Introduction rules: of delta predicate and locale predicate. *) 
11896  178 

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

181 

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

183 

184 

185 

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

186 
(** management of registrations in theories and proof contexts **) 
11896  187 

15837  188 
structure Registrations : 
189 
sig 

190 
type T 

191 
val empty: T 

192 
val join: T * T > T 

20069
77a6b62418bb
Witness theorems of interpretations now transfered to current theory.
ballarin
parents:
20059
diff
changeset

193 
val dest: theory > T > 
77a6b62418bb
Witness theorems of interpretations now transfered to current theory.
ballarin
parents:
20059
diff
changeset

194 
(term list * ((string * Attrib.src list) * Element.witness list)) list 
16458  195 
val lookup: theory > T * term list > 
19780  196 
((string * Attrib.src list) * Element.witness list) option 
16458  197 
val insert: theory > term list * (string * Attrib.src list) > T > 
19780  198 
T * (term list * ((string * Attrib.src list) * Element.witness list)) list 
199 
val add_witness: term list > Element.witness > T > T 

15837  200 
end = 
201 
struct 

20069
77a6b62418bb
Witness theorems of interpretations now transfered to current theory.
ballarin
parents:
20059
diff
changeset

202 
(* a registration consists of theorems (actually, witnesses) instantiating locale 
77a6b62418bb
Witness theorems of interpretations now transfered to current theory.
ballarin
parents:
20059
diff
changeset

203 
assumptions and prefix and attributes, indexed by parameter instantiation *) 
19780  204 
type T = ((string * Attrib.src list) * Element.witness list) Termtab.table; 
15837  205 

206 
val empty = Termtab.empty; 

207 

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

209 
fun termify ts = 

18343  210 
Term.list_comb (Const ("", map fastype_of ts > propT), ts); 
15837  211 
fun untermify t = 
212 
let fun ut (Const _) ts = ts 

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

214 
in ut t [] end; 

215 

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

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

20069
77a6b62418bb
Witness theorems of interpretations now transfered to current theory.
ballarin
parents:
20059
diff
changeset

220 
fun dest_transfer thy regs = 
77a6b62418bb
Witness theorems of interpretations now transfered to current theory.
ballarin
parents:
20059
diff
changeset

221 
Termtab.dest regs > map (apsnd (apsnd (map (Element.transfer_witness thy)))); 
77a6b62418bb
Witness theorems of interpretations now transfered to current theory.
ballarin
parents:
20059
diff
changeset

222 

77a6b62418bb
Witness theorems of interpretations now transfered to current theory.
ballarin
parents:
20059
diff
changeset

223 
fun dest thy regs = dest_transfer thy regs > map (apfst untermify); 
15837  224 

225 
(* registrations that subsume t *) 

17203  226 
fun subsumers thy t regs = 
20069
77a6b62418bb
Witness theorems of interpretations now transfered to current theory.
ballarin
parents:
20059
diff
changeset

227 
filter (fn (t', _) => Pattern.matches thy (t', t)) (dest_transfer thy regs); 
15837  228 

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

19780  230 
fun lookup thy (regs, ts) = 
15837  231 
let 
232 
val t = termify ts; 

19780  233 
val subs = subsumers thy t regs; 
15837  234 
in (case subs of 
235 
[] => NONE 

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

19780  237 
val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty); 
15837  238 
(* thms contain Frees, not Vars *) 
239 
val tinst' = tinst > Vartab.dest 

19810  240 
> map (fn ((x, 0), (_, T)) => (x, Logic.legacy_unvarifyT T)) 
15837  241 
> Symtab.make; 
242 
val inst' = inst > Vartab.dest 

19810  243 
> map (fn ((x, 0), (_, t)) => (x, Logic.legacy_unvarify t)) 
15837  244 
> Symtab.make; 
245 
in 

19780  246 
SOME (attn, map (Element.inst_witness thy (tinst', inst')) thms) 
15837  247 
end) 
248 
end; 

249 

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

251 
additionally returns registrations that are strictly subsumed *) 

20069
77a6b62418bb
Witness theorems of interpretations now transfered to current theory.
ballarin
parents:
20059
diff
changeset

252 
fun insert thy (ts, attn) regs = 
15837  253 
let 
254 
val t = termify ts; 

20069
77a6b62418bb
Witness theorems of interpretations now transfered to current theory.
ballarin
parents:
20059
diff
changeset

255 
val subs = subsumers thy t regs ; 
15837  256 
in (case subs of 
257 
[] => let 

258 
val sups = 

20069
77a6b62418bb
Witness theorems of interpretations now transfered to current theory.
ballarin
parents:
20059
diff
changeset

259 
filter (fn (t', _) => Pattern.matches thy (t, t')) (dest_transfer thy regs); 
15837  260 
val sups' = map (apfst untermify) sups 
17412  261 
in (Termtab.update (t, (attn, [])) regs, sups') end 
15837  262 
 _ => (regs, [])) 
263 
end; 

264 

265 
(* add witness theorem to registration, 

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

266 
only if instantiation is exact, otherwise exception Option raised *) 
15837  267 
fun add_witness ts thm regs = 
268 
let 

269 
val t = termify ts; 

18343  270 
val (x, thms) = the (Termtab.lookup regs t); 
15837  271 
in 
17412  272 
Termtab.update (t, (x, thm::thms)) regs 
15837  273 
end; 
274 
end; 

275 

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

276 

15837  277 
(** theory data **) 
15596  278 

16458  279 
structure GlobalLocalesData = TheoryDataFun 
280 
(struct 

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

15837  285 
3rd entry: registrations, indexed by locale name *) 
11896  286 

15596  287 
val empty = (NameSpace.empty, Symtab.empty, Symtab.empty); 
12063  288 
val copy = I; 
16458  289 
val extend = I; 
12289  290 

19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

291 
fun join_locs _ ({axiom, import, elems, params, lparams, term_syntax, regs, intros}: locale, 
19662
2f5d076fde32
replaced abbrevs by term_syntax, which is both simpler and more general;
wenzelm
parents:
19585
diff
changeset

292 
{elems = elems', term_syntax = term_syntax', regs = regs', ...}: locale) = 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

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

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

296 
params = params, 
19278  297 
lparams = lparams, 
19662
2f5d076fde32
replaced abbrevs by term_syntax, which is both simpler and more general;
wenzelm
parents:
19585
diff
changeset

298 
term_syntax = Library.merge (eq_snd (op =)) (term_syntax, term_syntax'), 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

299 
regs = merge_alists regs regs', 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

300 
intros = intros}; 
16458  301 
fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) = 
15596  302 
(NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2), 
19025  303 
Symtab.join (K Registrations.join) (regs1, regs2)); 
12289  304 

15596  305 
fun print _ (space, locs, _) = 
16346  306 
Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs))) 
12014  307 
> Pretty.writeln; 
16458  308 
end); 
11896  309 

18708  310 
val _ = Context.add_setup GlobalLocalesData.init; 
15801  311 

312 

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

313 

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

314 
(** context data **) 
11896  315 

16458  316 
structure LocalLocalesData = ProofDataFun 
317 
(struct 

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

318 
val name = "Isar/locales"; 
15837  319 
type T = Registrations.T Symtab.table; 
320 
(* registrations, indexed by locale name *) 

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

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

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

324 

18708  325 
val _ = Context.add_setup LocalLocalesData.init; 
12289  326 

12277  327 

328 
(* access locales *) 

329 

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

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

331 

16458  332 
val intern = NameSpace.intern o #1 o GlobalLocalesData.get; 
333 
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

334 

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

16458  337 
(Sign.declare_name thy name space, locs, regs)); 
11896  338 

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

340 
GlobalLocalesData.map (fn (space, locs, regs) => 
17412  341 
(space, Symtab.update (name, loc) locs, regs)); 
342 

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

11896  344 

12014  345 
fun the_locale thy name = 
346 
(case get_locale thy name of 

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

11896  349 

18806  350 
fun change_locale name f thy = 
351 
let 

19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

352 
val {axiom, import, elems, params, lparams, term_syntax, regs, intros} = 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

353 
the_locale thy name; 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

354 
val (axiom', import', elems', params', lparams', term_syntax', regs', intros') = 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

355 
f (axiom, import, elems, params, lparams, term_syntax, regs, intros); 
18806  356 
in 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

357 
put_locale name {axiom = axiom', import = import', elems = elems', 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

358 
params = params', lparams = lparams', term_syntax = term_syntax', regs = regs', 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

359 
intros = intros'} thy 
18806  360 
end; 
361 

12046  362 

15596  363 
(* access registrations *) 
364 

15696  365 
(* Ids of global registrations are varified, 
366 
Ids of local registrations are not. 

367 
Thms of registrations are never varified. *) 

368 

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

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

370 

20069
77a6b62418bb
Witness theorems of interpretations now transfered to current theory.
ballarin
parents:
20059
diff
changeset

371 
fun gen_get_registrations get thy_of thy_ctxt name = 
17412  372 
case Symtab.lookup (get thy_ctxt) name of 
15696  373 
NONE => [] 
20069
77a6b62418bb
Witness theorems of interpretations now transfered to current theory.
ballarin
parents:
20059
diff
changeset

374 
 SOME reg => Registrations.dest (thy_of thy_ctxt) reg; 
15696  375 

376 
val get_global_registrations = 

20069
77a6b62418bb
Witness theorems of interpretations now transfered to current theory.
ballarin
parents:
20059
diff
changeset

377 
gen_get_registrations (#3 o GlobalLocalesData.get) I; 
15696  378 
val get_local_registrations = 
20069
77a6b62418bb
Witness theorems of interpretations now transfered to current theory.
ballarin
parents:
20059
diff
changeset

379 
gen_get_registrations LocalLocalesData.get ProofContext.theory_of; 
15696  380 

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

383 
NONE => NONE 
16458  384 
 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

385 

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

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

388 
val get_local_registration = 
16458  389 
gen_get_registration LocalLocalesData.get ProofContext.theory_of; 
15596  390 

18343  391 
val test_global_registration = is_some oo get_global_registration; 
392 
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

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

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

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

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

397 
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

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

399 

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

400 

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

402 

16458  403 
fun gen_put_registration map_data thy_of (name, ps) attn thy_ctxt = 
15837  404 
map_data (fn regs => 
405 
let 

16458  406 
val thy = thy_of thy_ctxt; 
18343  407 
val reg = the_default Registrations.empty (Symtab.lookup regs name); 
16458  408 
val (reg', sups) = Registrations.insert thy (ps, attn) reg; 
15837  409 
val _ = if not (null sups) then warning 
410 
("Subsumed interpretation(s) of locale " ^ 

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

414 
else (); 

17412  415 
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

416 

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

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

418 
gen_put_registration (fn f => 
16458  419 
GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, f regs))) I; 
15837  420 
val put_local_registration = 
16458  421 
gen_put_registration LocalLocalesData.map ProofContext.theory_of; 
15596  422 

18806  423 
fun put_registration_in_locale name id = 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

424 
change_locale name (fn (axiom, import, elems, params, lparams, term_syntax, regs, intros) => 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

425 
(axiom, import, elems, params, lparams, term_syntax, regs @ [(id, [])], intros)); 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

426 

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

427 

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

428 
(* add witness theorem to registration in theory or context, 
15596  429 
ignored if registration not present *) 
430 

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

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

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

433 

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

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

435 
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

436 

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

437 
val add_local_witness = LocalLocalesData.map oo add_witness; 
15596  438 

18806  439 
fun add_witness_in_locale name id thm = 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

440 
change_locale name (fn (axiom, import, elems, params, lparams, term_syntax, regs, intros) => 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

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

442 
fun add (id', thms) = 
18806  443 
if id = id' then (id', thm :: thms) else (id', thms); 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

444 
in (axiom, import, elems, params, lparams, term_syntax, map add regs, intros) end); 
15596  445 

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

446 

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

447 
(* printing of registrations *) 
15596  448 

17138  449 
fun gen_print_registrations get_regs mk_ctxt msg show_wits loc thy_ctxt = 
15596  450 
let 
15703  451 
val ctxt = mk_ctxt thy_ctxt; 
452 
val thy = ProofContext.theory_of ctxt; 

453 

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

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

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

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

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

458 
Pretty.breaks (Pretty.str prfx :: Args.pretty_attribs ctxt atts); 
19780  459 
fun prt_witns witns = Pretty.enclose "[" "]" 
460 
(Pretty.breaks (map (prt_term o Element.witness_prop) witns)); 

461 
fun prt_reg (ts, (("", []), witns)) = 

17138  462 
if show_wits 
19780  463 
then Pretty.block [prt_inst ts, Pretty.fbrk, prt_witns witns] 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

464 
else prt_inst ts 
19780  465 
 prt_reg (ts, (attn, witns)) = 
17138  466 
if show_wits 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

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

468 
[Pretty.str ":", Pretty.brk 1, prt_inst ts, Pretty.fbrk, 
19780  469 
prt_witns witns])) 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

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

471 
[Pretty.str ":", Pretty.brk 1, prt_inst ts])); 
15703  472 

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

474 
val regs = get_regs thy_ctxt; 
17412  475 
val loc_regs = Symtab.lookup regs loc_int; 
15596  476 
in 
477 
(case loc_regs of 

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

479 
 SOME r => let 
20069
77a6b62418bb
Witness theorems of interpretations now transfered to current theory.
ballarin
parents:
20059
diff
changeset

480 
val r' = Registrations.dest thy r; 
15763
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
15749
diff
changeset

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

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

484 
end) 
15596  485 
> Pretty.writeln 
486 
end; 

487 

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

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

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

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

492 
gen_print_registrations LocalLocalesData.get 
15703  493 
I "context"; 
17138  494 
fun print_local_registrations show_wits loc ctxt = 
495 
(print_global_registrations show_wits loc (ProofContext.theory_of ctxt); 

496 
print_local_registrations' show_wits loc ctxt); 

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

497 

15596  498 

12277  499 
(* diagnostics *) 
12273  500 

12277  501 
fun err_in_locale ctxt msg ids = 
502 
let 

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

504 
fun prt_id (name, parms) = 
16458  505 
[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

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

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

18678  511 
in error err_msg end; 
12063  512 

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

513 
fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids'); 
12277  514 

515 

19783  516 
fun pretty_ren NONE = Pretty.str "_" 
517 
 pretty_ren (SOME (x, NONE)) = Pretty.str x 

518 
 pretty_ren (SOME (x, SOME syn)) = 

519 
Pretty.block [Pretty.str x, Pretty.brk 1, Syntax.pretty_mixfix syn]; 

520 

521 
fun pretty_expr thy (Locale name) = Pretty.str (extern thy name) 

522 
 pretty_expr thy (Rename (expr, xs)) = 

523 
Pretty.block [pretty_expr thy expr, Pretty.brk 1, Pretty.block (map pretty_ren xs > Pretty.breaks)] 

524 
 pretty_expr thy (Merge es) = 

525 
Pretty.separate "+" (map (pretty_expr thy) es) > Pretty.block; 

526 

527 
fun err_in_expr _ msg (Merge []) = error msg 

528 
 err_in_expr ctxt msg expr = 

529 
error (msg ^ "\n" ^ Pretty.string_of (Pretty.block 

530 
[Pretty.str "The error(s) above occured in locale expression:", Pretty.brk 1, 

531 
pretty_expr (ProofContext.theory_of ctxt) expr])); 

532 

12046  533 

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

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

535 

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

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

537 

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

538 
fun frozen_tvars ctxt Ts = 
19914  539 
#1 (Variable.importT_inst (map Logic.mk_type Ts) ctxt) 
19900
21a99d88d925
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19873
diff
changeset

540 
> map (fn ((xi, S), T) => (xi, (S, T))); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

541 

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

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

543 
let 
18343  544 
fun paramify NONE i = (NONE, i) 
545 
 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

546 

18343  547 
val (Ts', maxidx') = fold_map paramify Ts maxidx; 
548 
val (Us', maxidx'') = fold_map paramify Us maxidx'; 

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

550 

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

553 
 unify _ env = env; 

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

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

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

558 

19932  559 
fun params_of elemss = distinct (eq_fst (op = : string * string > bool)) (maps (snd o fst) elemss); 
560 
fun params_of' elemss = distinct (eq_fst (op = : string * string > bool)) (maps (snd o fst o fst) elemss); 

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

561 

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

562 

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

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

565 
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

566 

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

567 

19932  568 
fun merge_syntax ctxt ids ss = Symtab.merge (op = : mixfix * mixfix > bool) ss 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

569 
handle Symtab.DUPS xs => err_in_locale ctxt 
16105  570 
("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

571 

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

572 

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

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

574 
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

575 
assumptions of the specification fragment (for locales with 
19780  576 
predicates). The latter have witnesses relating assumptions of the 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

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

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

579 

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

580 
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

581 

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

582 
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

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

584 

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

585 

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

586 
(* flatten expressions *) 
11896  587 

12510  588 
local 
12502  589 

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

595 

596 
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

597 
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

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

18137  600 
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

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

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

605 
end; 

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

607 
 unify_list [] = I; 

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

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

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

614 
fun inst_parms (i, ps) = 

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

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

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

620 
in map inst_parms idx_parmss end; 

12502  621 

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

622 
in 
12502  623 

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

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

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

626 
 unify_elemss ctxt fixed_parms elemss = 
12502  627 
let 
18137  628 
val thy = ProofContext.theory_of ctxt; 
17756  629 
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

630 
fun inst ((((name, ps), mode), elems), env) = 
18137  631 
(((name, map (apsnd (Option.map (Element.instT_type env))) ps), 
19780  632 
map_mode (map (Element.instT_witness thy env)) mode), 
18137  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 

19810  637 
fun renaming xs parms = zip_options parms xs 
638 
handle Library.UnequalLengths => 

639 
error ("Too many arguments in renaming: " ^ 

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

641 

642 

19783  643 
(* params_of_expr: 
644 
Compute parameters (with types and syntax) of locale expression. 

645 
*) 

646 

647 
fun params_of_expr ctxt fixed_params expr (prev_parms, prev_types, prev_syn) = 

648 
let 

649 
val thy = ProofContext.theory_of ctxt; 

650 

651 
fun merge_tenvs fixed tenv1 tenv2 = 

652 
let 

653 
val [env1, env2] = unify_parms ctxt fixed 

654 
[tenv1 > Symtab.dest > map (apsnd SOME), 

655 
tenv2 > Symtab.dest > map (apsnd SOME)] 

656 
in 

657 
Symtab.merge (op =) (Symtab.map (Element.instT_type env1) tenv1, 

658 
Symtab.map (Element.instT_type env2) tenv2) 

659 
end; 

660 

661 
fun merge_syn expr syn1 syn2 = 

19932  662 
Symtab.merge (op = : mixfix * mixfix > bool) (syn1, syn2) 
19783  663 
handle Symtab.DUPS xs => err_in_expr ctxt 
664 
("Conflicting syntax for parameter(s): " ^ commas_quote xs) expr; 

20366
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

665 

19783  666 
fun params_of (expr as Locale name) = 
667 
let 

668 
val {import, params, ...} = the_locale thy name; 

669 
val parms = map (fst o fst) params; 

670 
val (parms', types', syn') = params_of import; 

671 
val all_parms = merge_lists parms' parms; 

672 
val all_types = merge_tenvs [] types' (params > map fst > Symtab.make); 

673 
val all_syn = merge_syn expr syn' (params > map (apfst fst) > Symtab.make); 

674 
in (all_parms, all_types, all_syn) end 

675 
 params_of (expr as Rename (e, xs)) = 

676 
let 

677 
val (parms', types', syn') = params_of e; 

678 
val ren = renaming xs parms'; 

679 
(* renaming may reduce number of parameters *) 

680 
val new_parms = map (Element.rename ren) parms' > distinct (op =); 

681 
val ren_syn = syn' > Symtab.dest > map (Element.rename_var ren); 

682 
val new_syn = fold (Symtab.insert (op =)) ren_syn Symtab.empty 

683 
handle Symtab.DUP x => 

684 
err_in_expr ctxt ("Conflicting syntax for parameter: " ^ quote x) expr; 

685 
val syn_types = map (apsnd (fn mx => SOME (Type.freeze_type (#1 (TypeInfer.paramify_dummies (TypeInfer.mixfixT mx) 0))))) (Symtab.dest new_syn); 

686 
val ren_types = types' > Symtab.dest > map (apfst (Element.rename ren)); 

20366
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

687 
val (env :: _) = unify_parms ctxt [] 
19783  688 
((ren_types > map (apsnd SOME)) :: map single syn_types); 
689 
val new_types = fold (Symtab.insert (op =)) 

690 
(map (apsnd (Element.instT_type env)) ren_types) Symtab.empty; 

691 
in (new_parms, new_types, new_syn) end 

692 
 params_of (Merge es) = 

693 
fold (fn e => fn (parms, types, syn) => 

694 
let 

695 
val (parms', types', syn') = params_of e 

696 
in 

697 
(merge_lists parms parms', merge_tenvs [] types types', 

698 
merge_syn e syn syn') 

699 
end) 

700 
es ([], Symtab.empty, Symtab.empty) 

701 

702 
val (parms, types, syn) = params_of expr; 

703 
in 

704 
(merge_lists prev_parms parms, merge_tenvs fixed_params prev_types types, 

705 
merge_syn expr prev_syn syn) 

706 
end; 

707 

708 
fun make_params_ids params = [(("", params), ([], Assumed []))]; 

709 
fun make_raw_params_elemss (params, tenv, syn) = 

710 
[((("", map (fn p => (p, Symtab.lookup tenv p)) params), Assumed []), 

711 
Int [Fixes (map (fn p => 

712 
(p, Symtab.lookup tenv p, Symtab.lookup syn p > the)) params)])]; 

713 

714 

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

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

718 
identifier). 

719 

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

721 
((name, ps), (ax_ps, axs)) 

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

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

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

725 
hence axioms may contain additional parameters from later fragments: 

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

727 

728 
Elements are enriched by identifierlike information: 

729 
(((name, ax_ps), axs), elems) 

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

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

732 
typeinstantiated. 

733 

734 
*) 

735 

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

736 
fun flatten_expr ctxt ((prev_idents, prev_syntax), expr) = 
12014  737 
let 
738 
val thy = ProofContext.theory_of ctxt; 

12263  739 

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

740 
fun rename_parms top ren ((name, ps), (parms, mode)) = 
19783  741 
((name, map (Element.rename ren) ps), 
742 
if top 

743 
then (map (Element.rename ren) parms, 

744 
map_mode (map (Element.rename_witness ren)) mode) 

745 
else (parms, mode)); 

12263  746 

20167
fe5fd4fd4114
Strict dfs traversal of imported and registered identifiers.
ballarin
parents:
20092
diff
changeset

747 
(* add (name, ps) and its registrations, recursively; adjust hyps of witnesses *) 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

748 

20167
fe5fd4fd4114
Strict dfs traversal of imported and registered identifiers.
ballarin
parents:
20092
diff
changeset

749 
fun add_with_regs ((name, pTs), mode) (wits, ids, visited) = 
fe5fd4fd4114
Strict dfs traversal of imported and registered identifiers.
ballarin
parents:
20092
diff
changeset

750 
if member (fn (a, (b, _)) => a = b) visited (name, map #1 pTs) 
fe5fd4fd4114
Strict dfs traversal of imported and registered identifiers.
ballarin
parents:
20092
diff
changeset

751 
then (wits, ids, visited) 
fe5fd4fd4114
Strict dfs traversal of imported and registered identifiers.
ballarin
parents:
20092
diff
changeset

752 
else 
20366
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

753 
let 
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

754 
val {params, regs, ...} = the_locale thy name; 
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

755 
val pTs' = map #1 params; 
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

756 
val ren = map #1 pTs' ~~ map (fn (x, _) => (x, NONE)) pTs; 
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

757 
(* dummy syntax, since required by rename *) 
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

758 
val pTs'' = map (fn ((p, _), (_, T)) => (p, T)) (pTs ~~ pTs'); 
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

759 
val [env] = unify_parms ctxt pTs [map (apsnd SOME) pTs'']; 
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

760 
(* propagate parameter types, to keep them consistent *) 
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

761 
val regs' = map (fn ((name, ps), wits) => 
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

762 
((name, map (Element.rename ren) ps), 
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

763 
map (Element.transfer_witness thy) wits)) regs; 
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

764 
val new_regs = regs'; 
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

765 
val new_ids = map fst new_regs; 
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

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

767 

20366
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

768 
val new_wits = new_regs > map (#2 #> map 
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

769 
(Element.instT_witness thy env #> Element.rename_witness ren #> 
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

770 
Element.satisfy_witness wits)); 
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

771 
val new_ids' = map (fn (id, wits) => 
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

772 
(id, ([], Derived wits))) (new_ids ~~ new_wits); 
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

773 
val new_idTs' = map (fn ((n, pTs), (_, ([], mode))) => 
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

774 
((n, pTs), mode)) (new_idTs ~~ new_ids'); 
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

775 
val new_id = ((name, map #1 pTs), ([], mode)); 
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

776 
val (wits', ids', visited') = fold add_with_regs new_idTs' 
20167
fe5fd4fd4114
Strict dfs traversal of imported and registered identifiers.
ballarin
parents:
20092
diff
changeset

777 
(wits @ flat new_wits, ids, visited @ [new_id]); 
20366
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

778 
in 
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

779 
(wits', ids' @ [new_id], visited') 
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

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

781 

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

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

783 

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

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

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

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

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

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

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

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

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

792 
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

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

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

795 

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

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

797 

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

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

800 
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

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

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

803 
parms is accumulated list of parameters *) 
12289  804 
let 
20035
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

805 
val {axiom, import, params, ...} = the_locale thy name; 
19278  806 
val ps = map (#1 o #1) params; 
20035
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

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

808 
(* acyclic import dependencies *) 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

809 

20167
fe5fd4fd4114
Strict dfs traversal of imported and registered identifiers.
ballarin
parents:
20092
diff
changeset

810 
val (_, ids'', _) = add_with_regs ((name, map #1 params), Assumed []) ([], ids', ids'); 
fe5fd4fd4114
Strict dfs traversal of imported and registered identifiers.
ballarin
parents:
20092
diff
changeset

811 
val ids_ax = if top then fst (fold_map (axiomify ps) ids'' axiom) else ids''; 
20035
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

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

813 
 identify top (Rename (e, xs)) = 
12273  814 
let 
20035
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

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

818 

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

819 
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

820 
val parms'' = distinct (op =) (maps (#2 o #1) ids''); 
20035
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

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

822 
 identify top (Merge es) = 
20035
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

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

824 
let 
20035
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

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

826 
in 
20035
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

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

828 
end) 
20035
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

829 
es ([], []); 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

830 

20035
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

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

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

834 
val [env] = unify_parms ctxt all_params [ps]; 
18137  835 
val t' = Element.instT_term env t; 
836 
val th' = Element.instT_thm thy env th; 

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

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

838 

20035
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

839 
fun eval all_params tenv syn ((name, params), (locale_params, mode)) = 
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

840 
let 
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

841 
val {params = ps_mx, elems = elems_stamped, ...} = the_locale thy name; 
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

842 
val elems = map fst elems_stamped; 
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

843 
val ps = map fst ps_mx; 
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

844 
fun lookup_syn x = (case Symtab.lookup syn x of SOME Structure => NONE  opt => opt); 
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

845 
val locale_params' = map (fn p => (p, Symtab.lookup tenv p > the)) locale_params; 
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

846 
val mode' = map_mode (map (Element.map_witness (inst_wit all_params))) mode; 
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

847 
val ren = map fst ps ~~ map (fn p => (p, lookup_syn p)) params; 
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

848 
val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps]; 
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

849 
val elems' = elems 
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

850 
> map (Element.rename_ctxt ren) 
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

851 
> map (Element.map_ctxt {var = I, typ = I, term = I, fact = I, attrib = I, 
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

852 
name = NameSpace.qualified (space_implode "_" params)}) 
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

853 
> map (Element.instT_ctxt thy env) 
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

854 
in (((name, map (apsnd SOME) locale_params'), mode'), elems') end; 
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

855 

80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

856 
(* parameters, their types and syntax *) 
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

857 
val (all_params', tenv, syn) = params_of_expr ctxt [] expr ([], Symtab.empty, Symtab.empty); 
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

858 
val all_params = map (fn p => (p, Symtab.lookup tenv p > the)) all_params'; 
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

859 
(* compute identifiers and syntax, merge with previous ones *) 
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

860 
val (ids, _) = identify true expr; 
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

861 
val idents = gen_rems (eq_fst (op =)) (ids, prev_idents); 
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

862 
val syntax = merge_syntax ctxt ids (syn, prev_syntax); 
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

863 
(* typeinstantiate elements *) 
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset

864 
val final_elemss = map (eval all_params tenv syntax) idents; 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

865 
in ((prev_idents @ idents, syntax), final_elemss) end; 
12046  866 

12510  867 
end; 
868 

12070  869 

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

870 
(* activate elements *) 
12273  871 

12510  872 
local 
873 

18671  874 
fun axioms_export axs _ hyps = 
19780  875 
Element.satisfy_thm axs 
20307  876 
#> Drule.implies_intr_list (Library.drop (length axs, hyps)); 
12263  877 

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

878 

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

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

880 

19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

881 
fun activate_elem _ _ ((ctxt, mode), Fixes fixes) = 
18671  882 
((ctxt > ProofContext.add_fixes_i fixes > snd, mode), []) 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

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

884 
((ctxt, mode), []) 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

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

886 
let 
18728  887 
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

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

889 
val (ps, qs) = chop (length ts) axs; 
17856  890 
val (_, ctxt') = 
20243
8b64a1ea9b1b
renamed ProofContext.fix_frees to Variable.fix_frees;
wenzelm
parents:
20224
diff
changeset

891 
ctxt > fold Variable.fix_frees ts 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

892 
> ProofContext.add_assms_i (axioms_export (if ax_in_ctxt then ps else [])) asms'; 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

893 
in ((ctxt', Assumed qs), []) end 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

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

895 
((ctxt, Derived ths), []) 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

896 
 activate_elem _ _ ((ctxt, Assumed axs), Defines defs) = 
15596  897 
let 
18728  898 
val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs; 
19732  899 
val asms = defs' > map (fn ((name, atts), (t, ps)) => 
900 
let val ((c, _), t') = LocalDefs.cert_def ctxt t 

901 
in (t', ((if name = "" then Thm.def_name c else name, atts), [(t', ps)])) end); 

17856  902 
val (_, ctxt') = 
20243
8b64a1ea9b1b
renamed ProofContext.fix_frees to Variable.fix_frees;
wenzelm
parents:
20224
diff
changeset

903 
ctxt > fold (Variable.fix_frees o #1) asms 
19732  904 
> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms); 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

905 
in ((ctxt', Assumed axs), []) end 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

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

907 
((ctxt, Derived ths), []) 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

908 
 activate_elem _ is_ext ((ctxt, mode), Notes facts) = 
15596  909 
let 
18728  910 
val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts; 
17856  911 
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

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

19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

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

916 
val thy = ProofContext.theory_of ctxt; 
17033  917 
val ((ctxt', _), res) = 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

918 
foldl_map (activate_elem ax_in_ctxt (name = "")) ((ProofContext.qualified_names ctxt, mode), elems) 
18678  919 
handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)] 
15696  920 
val ctxt'' = if name = "" then ctxt' 
921 
else let 

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

923 
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

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

925 
Assumed axs => 
19780  926 
fold (add_local_witness (name, ps') o 
927 
Element.assume_witness thy o Element.witness_prop) axs ctxt'' 

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

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

931 

19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

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

933 
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

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

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

936 
val (ctxt', res) = apsnd flat 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

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

19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

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

941 

12546  942 
in 
943 

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

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

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

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

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

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

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

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

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

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

954 

19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

955 
fun activate_facts ax_in_ctxt prep_facts (ctxt, args) = 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

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

957 
in (ctxt', (elemss, flat factss)) end; 
15703  958 

12510  959 
end; 
960 

12307  961 

15696  962 

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

964 

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

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

966 

16458  967 
fun intern_expr thy (Locale xname) = Locale (intern thy xname) 
968 
 intern_expr thy (Merge exprs) = Merge (map (intern_expr thy) exprs) 

969 
 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

970 

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

971 

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

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

973 

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

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

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

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

977 
to the list ids of already accumulated identifiers. 
19783  978 
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

979 
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

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

981 
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

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

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

984 

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

987 
identifierlike information of the element is as follows: 

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

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

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

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

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

993 

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

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

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

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

1000 
handle Symtab.DUPS xs => err_in_locale ctxt 

19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

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

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

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

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

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

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

1008 
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

1009 

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

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

1011 

12839  1012 
local 
1013 

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

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

1018 

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

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

1022 
 declare_ext_elem prep_vars (ctxt, Constrains csts) = 

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

1024 
in (ctxt', []) end 

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

1025 
 declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms) 
19585  1026 
 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

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

1028 

18671  1029 
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

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

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

1032 
Int es => foldl_map declare_int_elem (ctxt, es) 
18671  1033 
 Ext e => foldl_map (declare_ext_elem prep_vars) (ctxt, [e])) 
18678  1034 
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

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

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

12839  1038 
in 
1039 

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

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

1043 
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

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

1045 
val ctxt_with_fixed = 
19900
21a99d88d925
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19873
diff
changeset

1046 
fold Variable.declare_term (map Free fixed_params) ctxt; 
12727  1047 
val int_elemss = 
1048 
raw_elemss 

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

1049 
> 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

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

1053 
(int_elemss, raw_elemss); 

18671  1054 
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

1055 

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

1057 

12839  1058 
local 
1059 

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

1061 

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

12502  1064 

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

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

1075 
err "Attempt to redefine variable"); 

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

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

1079 

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

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

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

1082 

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

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

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

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

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

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

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

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

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

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

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

13308  1099 

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

1100 

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

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

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

1103 
turn assumptions and definitions into facts, 
19780  1104 
adjust hypotheses of facts using witnesses *) 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1105 

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

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

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

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

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

1110 

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

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

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

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

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

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

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

1119 

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

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

1122 

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

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

1124 

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

12839  1127 
let 
13308  1128 
fun close_frees t = 
19900
21a99d88d925
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19873
diff
changeset

1129 
let val frees = rev (filter_out (Variable.is_fixed ctxt o #1) (Term.add_frees t [])) 
13308  1130 
in Term.list_all_free (frees, t) end; 
1131 

1132 
fun no_binds [] = [] 

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

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

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

12839  1142 

12502  1143 

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

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

1149 
 finish_ext_elem _ close (Defines defs, propp) = 

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

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

1153 

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

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

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

1157 

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

1158 
fun finish_parms parms (((name, ps), mode), elems) = 
19932  1159 
(((name, map (fn (x, _) => (x, AList.lookup (op = : string * string > bool) parms x)) ps), mode), elems); 
12839  1160 

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

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

1163 
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

1164 
val wits' = case mode of Assumed _ => wits  Derived ths => wits @ ths; 
18190  1165 
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

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

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

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

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

18190  1172 
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

1173 
in ((text', wits), (id, [Ext e'])) end 
12839  1174 

1175 
in 

12510  1176 

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

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

1178 

13375  1179 
fun finish_elemss ctxt parms do_close = 
1180 
foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close); 

12839  1181 

1182 
end; 

1183 

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

1184 

19942
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

1185 
(* Remove duplicate Defines elements: temporary workaround to fix Afp/Category. *) 
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

1186 

dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

1187 
fun defs_ord (defs1, defs2) = 
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

1188 
list_ord (fn ((_, (d1, _)), (_, (d2, _))) => 
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

1189 
Term.fast_term_ord (d1, d2)) (defs1, defs2); 
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

1190 
structure Defstab = 
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

1191 
TableFun(type key = ((string * Attrib.src list) * (term * term list)) list 
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

1192 
val ord = defs_ord); 
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

1193 

dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

1194 
fun rem_dup_defs es ds = 
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

1195 
fold_map (fn e as (Defines defs) => (fn ds => 
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

1196 
if Defstab.defined ds defs 
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

1197 
then (Defines [], ds) 
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

1198 
else (e, Defstab.update (defs, ()) ds)) 
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

1199 
 e => (fn ds => (e, ds))) es ds; 
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

1200 
fun rem_dup_elemss (Int es) ds = apfst Int (rem_dup_defs es ds) 
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

1201 
 rem_dup_elemss (Ext e) ds = (Ext e, ds); 
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

1202 
fun rem_dup_defines raw_elemss = 
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

1203 
fold_map (fn (id as (_, (Assumed _)), es) => (fn ds => 
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

1204 
apfst (pair id) (rem_dup_elemss es ds)) 
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

1205 
 (id as (_, (Derived _)), es) => (fn ds => 
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

1206 
((id, es), ds))) raw_elemss Defstab.empty > #1; 
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

1207 

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

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

1209 

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

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

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

1212 
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

1213 
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

1214 

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

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

1216 
*) 
15127  1217 

18671  1218 
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

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

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

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

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

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

1225 
context elements, the latter marked as internal or external. *) 
19942
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset

1226 
val raw_elemss = rem_dup_defines raw_elemss; 
18671  1227 
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

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

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

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

1231 
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

1232 
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

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

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

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

1236 
val (ctxt, all_propp) = 
19900
21a99d88d925
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19873
diff
changeset

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

1238 
(* CB: add type information from conclusion and external elements to context *) 
19900
21a99d88d925
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19873
diff
changeset

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

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

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

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

1243 
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

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

1245 

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

1246 
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

1247 
(fold_burrow o fold_burrow) prep_prop raw_proppss (raw_ctxt, raw_concl); 