author  wenzelm 
Mon, 23 Apr 2007 20:44:11 +0200  
changeset 22772  e0788ff2e811 
parent 22756  b9b78b90ba47 
child 22796  34c316d7b630 
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 
21035  45 
val map_elem: ('a > 'b) > 'a element > 'b element 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

46 

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

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

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

50 

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

51 
(* The specification of a locale *) 
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 
22523  60 
val intros: theory > string > 
61 
thm list * thm list 

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

62 

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

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

66 
string option * Proof.context * Proof.context * (term * term list) list list 
21035  67 
val read_context_statement_i: string option > Element.context element list > 
68 
(string * string list) list list > Proof.context > 

69 
string option * Proof.context * Proof.context * (term * term list) list list 

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

72 
string option * Proof.context * Proof.context * (term * term list) list list 
19780  73 
val read_expr: expr > Element.context list > Proof.context > 
74 
Element.context_i list * Proof.context 

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

76 
Element.context_i list * Proof.context 

15596  77 

78 
(* Diagnostic functions *) 

12758  79 
val print_locales: theory > unit 
18137  80 
val print_locale: theory > bool > expr > Element.context list > unit 
17138  81 
val print_global_registrations: bool > string > theory > unit 
18617  82 
val print_local_registrations': bool > string > Proof.context > unit 
83 
val print_local_registrations: bool > string > Proof.context > unit 

18137  84 

22351
587845efb4cf
locale: add_locale accepts explicit predicate name, interpretation supports nonmandatory prefixes
haftmann
parents:
22339
diff
changeset

85 
val add_locale: string option > bstring > expr > Element.context list > theory 
20965  86 
> string * Proof.context 
22351
587845efb4cf
locale: add_locale accepts explicit predicate name, interpretation supports nonmandatory prefixes
haftmann
parents:
22339
diff
changeset

87 
val add_locale_i: string option > bstring > expr > Element.context_i list > theory 
20965  88 
> string * Proof.context 
15596  89 

21225  90 
(* Tactics *) 
91 
val intro_locales_tac: bool > Proof.context > thm list > tactic 

92 

15696  93 
(* Storing results *) 
18806  94 
val add_thmss: string > string > 
95 
((string * Attrib.src list) * (thm list * Attrib.src list) list) list > 

21582  96 
Proof.context > Proof.context 
21665
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset

97 
val add_type_syntax: string > (morphism > Context.generic > Context.generic) > 
21499
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset

98 
Proof.context > Proof.context 
21665
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset

99 
val add_term_syntax: string > (morphism > Context.generic > Context.generic) > 
21499
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset

100 
Proof.context > Proof.context 
21665
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset

101 
val add_declaration: string > (morphism > Context.generic > Context.generic) > 
21499
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset

102 
Proof.context > Proof.context 
18137  103 

22300
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset

104 
val interpretation_i: (Proof.context > Proof.context) > 
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

105 
(bool * string) * Attrib.src list > expr > 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

106 
(typ Symtab.table * term Symtab.table) * (term * term) list > 
22300
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset

107 
theory > Proof.state 
21005  108 
val interpretation: (Proof.context > Proof.context) > 
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

109 
(bool * string) * Attrib.src list > expr > 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

110 
string option list * (string * string) list > 
21005  111 
theory > Proof.state 
112 
val interpretation_in_locale: (Proof.context > Proof.context) > 

113 
xstring * expr > theory > Proof.state 

22300
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset

114 
val interpret_i: (Proof.state > Proof.state Seq.seq) > 
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

115 
(bool * string) * Attrib.src list > expr > 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

116 
(typ Symtab.table * term Symtab.table) * (term * term) list > 
22300
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset

117 
bool > Proof.state > Proof.state 
21005  118 
val interpret: (Proof.state > Proof.state Seq.seq) > 
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

119 
(bool * string) * Attrib.src list > expr > 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

120 
string option list * (string * string) list > 
21005  121 
bool > Proof.state > Proof.state 
11896  122 
end; 
12839  123 

12289  124 
structure Locale: LOCALE = 
11896  125 
struct 
126 

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

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

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

129 
val cT = Thm.ctyp_of (Thm.theory_of_thm thm); 
22700  130 
val tvars = rev (Thm.fold_terms Term.add_tvars thm []); 
20307  131 
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

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

133 

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

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

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

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

137 
val ct = Thm.cterm_of (Thm.theory_of_thm thm); 
22700  138 
val vars = rev (Thm.fold_terms Term.add_vars thm []); 
20307  139 
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

140 
in Drule.instantiate' [] frees thm end; 
19780  141 

20307  142 

12273  143 
(** locale elements and expressions **) 
11896  144 

18137  145 
datatype ctxt = datatype Element.ctxt; 
17355  146 

12273  147 
datatype expr = 
148 
Locale of string  

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

149 
Rename of expr * (string * mixfix option) option list  
12273  150 
Merge of expr list; 
11896  151 

12273  152 
val empty = Merge []; 
153 

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

155 
Elem of 'a  Expr of expr; 
12273  156 

18137  157 
fun map_elem f (Elem e) = Elem (f e) 
158 
 map_elem _ (Expr e) = Expr e; 

159 

21665
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset

160 
type decl = (morphism > Context.generic > Context.generic) * stamp; 
21499
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset

161 

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

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

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

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

21499
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset

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

171 
lparams: string list, (*local params*) 
21665
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset

172 
decls: decl list * decl list, (*type/term_syntax declarations*) 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

173 
regs: ((string * string list) * Element.witness list) list, 
19780  174 
(* 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

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

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

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

180 

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

182 

183 

184 

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

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

15837  187 
structure Registrations : 
188 
sig 

189 
type T 

190 
val empty: T 

191 
val join: T * T > T 

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

192 
val dest: theory > T > 
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

193 
(term list * 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

194 
(((bool * string) * Attrib.src list) * Element.witness list * 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

195 
Element.witness Termtab.table)) list 
16458  196 
val lookup: theory > T * term list > 
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

197 
(((bool * string) * Attrib.src list) * Element.witness list * 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

198 
Element.witness Termtab.table) option 
22351
587845efb4cf
locale: add_locale accepts explicit predicate name, interpretation supports nonmandatory prefixes
haftmann
parents:
22339
diff
changeset

199 
val insert: theory > term list * ((bool * string) * Attrib.src list) > T > 
587845efb4cf
locale: add_locale accepts explicit predicate name, interpretation supports nonmandatory prefixes
haftmann
parents:
22339
diff
changeset

200 
T * (term list * (((bool * string) * Attrib.src list) * Element.witness list)) list 
19780  201 
val add_witness: term list > Element.witness > T > T 
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

202 
val add_equation: term list > Element.witness > T > T 
15837  203 
end = 
204 
struct 

22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

205 
(* A registration is indexed by parameter instantiation. Its components are: 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

206 
 parameters and prefix 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

207 
(if the Boolean flag is set, only accesses containing the prefix are generated, 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

208 
otherwise the prefix may be omitted when accessing theorems etc.) 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

209 
 theorems (actually witnesses) instantiating locale assumptions 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

210 
 theorems (equations, actually witnesses) interpreting derived concepts 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

211 
and indexed by lhs 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

212 
*) 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

213 
type T = (((bool * string) * Attrib.src list) * Element.witness list * 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

214 
Element.witness Termtab.table) Termtab.table; 
15837  215 

216 
val empty = Termtab.empty; 

217 

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

219 
fun termify ts = 

18343  220 
Term.list_comb (Const ("", map fastype_of ts > propT), ts); 
15837  221 
fun untermify t = 
222 
let fun ut (Const _) ts = ts 

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

224 
in ut t [] end; 

225 

22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

226 
(* joining of registrations: 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

227 
 prefix and attributes of right theory; 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

228 
 witnesses are equal, no attempt to subsumption testing; 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

229 
 union of equalities, if conflicting (i.e. two eqns with equal lhs) 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

230 
eqn of right theory takes precedence *) 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

231 
fun join (r1, r2) = Termtab.join (fn _ => fn ((_, _, e1), (n, w, e2)) => 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

232 
(n, w, Termtab.join (fn _ => fn (_, e) => e) (e1, e2))) (r1, r2); 
15837  233 

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

234 
fun dest_transfer thy regs = 
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

235 
Termtab.dest regs > map (apsnd (fn (n, ws, es) => 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

236 
(n, map (Element.transfer_witness thy) ws, Termtab.map (Element.transfer_witness thy) es))); 
20069
77a6b62418bb
Witness theorems of interpretations now transfered to current theory.
ballarin
parents:
20059
diff
changeset

237 

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

238 
fun dest thy regs = dest_transfer thy regs > map (apfst untermify); 
15837  239 

240 
(* registrations that subsume t *) 

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

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

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

19780  245 
fun lookup thy (regs, ts) = 
15837  246 
let 
247 
val t = termify ts; 

19780  248 
val subs = subsumers thy t regs; 
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset

249 
in 
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset

250 
(case subs of 
15837  251 
[] => NONE 
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

252 
 ((t', (attn, thms, eqns)) :: _) => 
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset

253 
let 
19780  254 
val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty); 
15837  255 
(* thms contain Frees, not Vars *) 
21665
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset

256 
val tinst' = tinst > Vartab.dest (* FIXME Vartab.map (!?) *) 
19810  257 
> map (fn ((x, 0), (_, T)) => (x, Logic.legacy_unvarifyT T)) 
15837  258 
> Symtab.make; 
259 
val inst' = inst > Vartab.dest 

19810  260 
> map (fn ((x, 0), (_, t)) => (x, Logic.legacy_unvarify t)) 
15837  261 
> Symtab.make; 
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset

262 
val inst_witness = Element.morph_witness (Element.inst_morphism thy (tinst', inst')); 
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

263 
in SOME (attn, map inst_witness thms, Termtab.map inst_witness eqns) end) 
15837  264 
end; 
265 

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

267 
additionally returns registrations that are strictly subsumed *) 

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

268 
fun insert thy (ts, attn) regs = 
15837  269 
let 
270 
val t = termify ts; 

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

271 
val subs = subsumers thy t regs ; 
15837  272 
in (case subs of 
273 
[] => let 

274 
val sups = 

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

275 
filter (fn (t', _) => Pattern.matches thy (t, t')) (dest_transfer thy regs); 
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

276 
val sups' = map (apfst untermify) sups > map (fn (ts, (n, w, d)) => (ts, (n, w))) 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

277 
in (Termtab.update (t, (attn, [], Termtab.empty)) regs, sups') end 
15837  278 
 _ => (regs, [])) 
279 
end; 

280 

281 
(* add witness theorem to registration, 

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

282 
only if instantiation is exact, otherwise exception Option raised *) 
15837  283 
fun add_witness ts thm regs = 
284 
let 

285 
val t = termify ts; 

22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

286 
val (x, thms, eqns) = the (Termtab.lookup regs t); 
15837  287 
in 
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

288 
Termtab.update (t, (x, thm::thms, eqns)) regs 
15837  289 
end; 
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

290 

263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

291 
(* add equation to registration, replaces previous equation with same lhs; 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

292 
only if instantiation is exact, otherwise exception Option raised; 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

293 
exception TERM raised if not a meta equality *) 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

294 
fun add_equation ts thm regs = 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

295 
let 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

296 
val t = termify ts; 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

297 
val (x, thms, eqns) = the (Termtab.lookup regs t); 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

298 
in 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

299 
Termtab.update (t, (x, thms, Termtab.update (thm > Element.witness_prop > Logic.dest_equals > fst, thm) eqns)) regs 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

300 
end; 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

301 
(* TODO: avoid code clone *) 
15837  302 
end; 
303 

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

304 

15837  305 
(** theory data **) 
15596  306 

16458  307 
structure GlobalLocalesData = TheoryDataFun 
308 
(struct 

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

15837  313 
3rd entry: registrations, indexed by locale name *) 
11896  314 

15596  315 
val empty = (NameSpace.empty, Symtab.empty, Symtab.empty); 
12063  316 
val copy = I; 
16458  317 
val extend = I; 
12289  318 

21665
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset

319 
fun join_locales _ 
22573  320 
({axiom, imports, elems, params, lparams, decls = (decls1, decls2), regs, intros}: locale, 
21665
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset

321 
{elems = elems', decls = (decls1', decls2'), regs = regs', ...}: locale) = 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

322 
{axiom = axiom, 
22573  323 
imports = imports, 
17496  324 
elems = gen_merge_lists (eq_snd (op =)) elems elems', 
16736
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

325 
params = params, 
19278  326 
lparams = lparams, 
21499
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset

327 
decls = 
21665
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset

328 
(Library.merge (eq_snd (op =)) (decls1, decls1'), 
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset

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

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

331 
intros = intros}; 
16458  332 
fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) = 
21499
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset

333 
(NameSpace.merge (space1, space2), Symtab.join join_locales (locs1, locs2), 
19025  334 
Symtab.join (K Registrations.join) (regs1, regs2)); 
12289  335 

15596  336 
fun print _ (space, locs, _) = 
16346  337 
Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs))) 
12014  338 
> Pretty.writeln; 
16458  339 
end); 
11896  340 

18708  341 
val _ = Context.add_setup GlobalLocalesData.init; 
15801  342 

343 

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

344 

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

345 
(** context data **) 
11896  346 

16458  347 
structure LocalLocalesData = ProofDataFun 
348 
(struct 

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

349 
val name = "Isar/locales"; 
15837  350 
type T = Registrations.T Symtab.table; 
351 
(* registrations, indexed by locale name *) 

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

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

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

355 

18708  356 
val _ = Context.add_setup LocalLocalesData.init; 
12289  357 

12277  358 

359 
(* access locales *) 

360 

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

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

362 

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

365 

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

16458  368 
(Sign.declare_name thy name space, locs, regs)); 
11896  369 

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

371 
GlobalLocalesData.map (fn (space, locs, regs) => 
17412  372 
(space, Symtab.update (name, loc) locs, regs)); 
373 

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

11896  375 

12014  376 
fun the_locale thy name = 
377 
(case get_locale thy name of 

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

11896  380 

18806  381 
fun change_locale name f thy = 
382 
let 

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

384 
the_locale thy name; 
22573  385 
val (axiom', imports', elems', params', lparams', decls', regs', intros') = 
386 
f (axiom, imports, elems, params, lparams, decls, regs, intros); 

18806  387 
in 
22573  388 
put_locale name {axiom = axiom', imports = imports', elems = elems', 
21499
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset

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

390 
intros = intros'} thy 
18806  391 
end; 
392 

12046  393 

15596  394 
(* access registrations *) 
395 

15696  396 
(* Ids of global registrations are varified, 
397 
Ids of local registrations are not. 

22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

398 
Witness thms of registrations are never varified. 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

399 
Varification of eqns as varification of ids. *) 
15696  400 

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

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

402 

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

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

406 
 SOME reg => Registrations.dest (thy_of thy_ctxt) reg; 
15696  407 

408 
val get_global_registrations = 

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

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

411 
gen_get_registrations LocalLocalesData.get ProofContext.theory_of; 
15696  412 

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

415 
NONE => NONE 
16458  416 
 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

417 

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

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

420 
val get_local_registration = 
16458  421 
gen_get_registration LocalLocalesData.get ProofContext.theory_of; 
15596  422 

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

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

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

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

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

429 
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

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

431 

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

432 

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

434 

16458  435 
fun gen_put_registration map_data thy_of (name, ps) attn thy_ctxt = 
15837  436 
map_data (fn regs => 
437 
let 

16458  438 
val thy = thy_of thy_ctxt; 
18343  439 
val reg = the_default Registrations.empty (Symtab.lookup regs name); 
16458  440 
val (reg', sups) = Registrations.insert thy (ps, attn) reg; 
15837  441 
val _ = if not (null sups) then warning 
442 
("Subsumed interpretation(s) of locale " ^ 

16458  443 
quote (extern thy name) ^ 
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

444 
"\nwith the following prefix(es):" ^ 
22351
587845efb4cf
locale: add_locale accepts explicit predicate name, interpretation supports nonmandatory prefixes
haftmann
parents:
22339
diff
changeset

445 
commas_quote (map (fn (_, (((_, s), _), _)) => s) sups)) 
15837  446 
else (); 
17412  447 
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

448 

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

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

450 
gen_put_registration (fn f => 
16458  451 
GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, f regs))) I; 
15837  452 
val put_local_registration = 
16458  453 
gen_put_registration LocalLocalesData.map ProofContext.theory_of; 
15596  454 

18806  455 
fun put_registration_in_locale name id = 
22573  456 
change_locale name (fn (axiom, imports, elems, params, lparams, decls, regs, intros) => 
457 
(axiom, imports, elems, params, lparams, decls, regs @ [(id, [])], intros)); 

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

458 

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

459 

22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

460 
(* add witness theorem to registration, ignored if registration not present *) 
15596  461 

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

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

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

464 

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

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

466 
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

467 

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

468 
val add_local_witness = LocalLocalesData.map oo add_witness; 
15596  469 

18806  470 
fun add_witness_in_locale name id thm = 
22573  471 
change_locale name (fn (axiom, imports, elems, params, lparams, decls, regs, intros) => 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

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

473 
fun add (id', thms) = 
18806  474 
if id = id' then (id', thm :: thms) else (id', thms); 
22573  475 
in (axiom, imports, elems, params, lparams, decls, map add regs, intros) end); 
15596  476 

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

477 

22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

478 
(* add equation to registration, ignored if registration not present *) 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

479 

263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

480 
fun add_equation (name, ps) thm = 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

481 
Symtab.map_entry name (Registrations.add_equation ps thm); 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

482 

263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

483 
fun add_global_equation id thm = 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

484 
GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, add_equation id thm regs)); 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

485 

263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

486 
val add_local_equation = LocalLocalesData.map oo add_equation; 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

487 

263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

488 

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

489 
(* printing of registrations *) 
15596  490 

17138  491 
fun gen_print_registrations get_regs mk_ctxt msg show_wits loc thy_ctxt = 
15596  492 
let 
15703  493 
val ctxt = mk_ctxt thy_ctxt; 
494 
val thy = ProofContext.theory_of ctxt; 

22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

495 
(* TODO: nice effect of show_wits on equations. *) 
15703  496 
val prt_term = Pretty.quote o ProofContext.pretty_term ctxt; 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

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

498 
Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts)); 
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

499 
fun prt_attn ((false, prfx), atts) = 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

500 
Pretty.breaks (Pretty.str prfx :: Pretty.str "(optional)" :: 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

501 
Attrib.pretty_attribs ctxt atts) 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

502 
 prt_attn ((true, prfx), atts) = 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

503 
Pretty.breaks (Pretty.str prfx :: Attrib.pretty_attribs ctxt atts); 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

504 
fun prt_eqns [] = Pretty.str "no equations." 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

505 
 prt_eqns eqns = Pretty.block (Pretty.str "equations:" :: Pretty.brk 1 :: 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

506 
Pretty.breaks (map (Element.pretty_witness ctxt) eqns)); 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

507 
fun prt_core ts eqns = 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

508 
[prt_inst ts, Pretty.fbrk, prt_eqns (Termtab.dest eqns > map snd)]; 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

509 
fun prt_witns [] = Pretty.str "no witnesses." 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

510 
 prt_witns witns = Pretty.block (Pretty.str "witnesses:" :: Pretty.brk 1 :: 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

511 
Pretty.breaks (map (Element.pretty_witness ctxt) witns)) 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

512 
fun prt_reg (ts, (((_, ""), []), witns, eqns)) = 
17138  513 
if show_wits 
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

514 
then Pretty.block (prt_core ts eqns @ [Pretty.fbrk, prt_witns witns]) 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

515 
else Pretty.block (prt_core ts eqns) 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

516 
 prt_reg (ts, (attn, witns, eqns)) = 
17138  517 
if show_wits 
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

518 
then Pretty.block ((prt_attn attn @ [Pretty.str ":", Pretty.brk 1] @ 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

519 
prt_core ts eqns @ [Pretty.fbrk, prt_witns witns])) 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

520 
else Pretty.block ((prt_attn attn @ 
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

521 
[Pretty.str ":", Pretty.brk 1] @ prt_core ts eqns)); 
15703  522 

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

524 
val regs = get_regs thy_ctxt; 
17412  525 
val loc_regs = Symtab.lookup regs loc_int; 
15596  526 
in 
527 
(case loc_regs of 

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

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

530 
val r' = Registrations.dest thy r; 
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

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

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

534 
end) 
15596  535 
> Pretty.writeln 
536 
end; 

537 

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

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

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

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

542 
gen_print_registrations LocalLocalesData.get 
15703  543 
I "context"; 
17138  544 
fun print_local_registrations show_wits loc ctxt = 
545 
(print_global_registrations show_wits loc (ProofContext.theory_of ctxt); 

546 
print_local_registrations' show_wits loc ctxt); 

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

547 

15596  548 

12277  549 
(* diagnostics *) 
12273  550 

12277  551 
fun err_in_locale ctxt msg ids = 
552 
let 

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

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

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

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

18678  561 
in error err_msg end; 
12063  562 

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

563 
fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids'); 
12277  564 

565 

19783  566 
fun pretty_ren NONE = Pretty.str "_" 
567 
 pretty_ren (SOME (x, NONE)) = Pretty.str x 

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

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

570 

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

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

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

574 
 pretty_expr thy (Merge es) = 

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

576 

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

578 
 err_in_expr ctxt msg expr = 

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

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

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

582 

12046  583 

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

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

585 

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

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

587 

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

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

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

591 

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

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

593 
let 
18343  594 
fun paramify NONE i = (NONE, i) 
595 
 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

596 

18343  597 
val (Ts', maxidx') = fold_map paramify Ts maxidx; 
598 
val (Us', maxidx'') = fold_map paramify Us maxidx'; 

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

600 

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

603 
 unify _ env = env; 

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

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

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

608 

21665
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset

609 
fun params_of elemss = 
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset

610 
distinct (eq_fst (op = : string * string > bool)) (maps (snd o fst) elemss); 
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset

611 

ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset

612 
fun params_of' elemss = 
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset

613 
distinct (eq_fst (op = : string * string > bool)) (maps (snd o fst o fst) elemss); 
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset

614 

ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset

615 

ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset

616 
fun params_prefix params = space_implode "_" params; 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

617 

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

618 

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

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

621 
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

622 

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

623 

19932  624 
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

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

627 

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

628 

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

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

630 
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

631 
assumptions of the specification fragment (for locales with 
19780  632 
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

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

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

635 

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

636 
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

637 

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

638 
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

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

640 

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

641 

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

642 
(* flatten expressions *) 
11896  643 

12510  644 
local 
12502  645 

18137  646 
fun unify_parms ctxt fixed_parms raw_parmss = 
12502  647 
let 
16458  648 
val thy = ProofContext.theory_of ctxt; 
12502  649 
val maxidx = length raw_parmss; 
650 
val idx_parmss = (0 upto maxidx  1) ~~ raw_parmss; 

651 

652 
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

653 
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

654 
val parms = fixed_parms @ maps varify_parms idx_parmss; 
12502  655 

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

657 
handle Type.TUNIFY => 
22339
0dc6b45e5662
more precise error message in parameter unification
schirmer
parents:
22300
diff
changeset

658 
let 
0dc6b45e5662
more precise error message in parameter unification
schirmer
parents:
22300
diff
changeset

659 
val T' = Envir.norm_type (fst envir) T; 
0dc6b45e5662
more precise error message in parameter unification
schirmer
parents:
22300
diff
changeset

660 
val U' = Envir.norm_type (fst envir) U; 
0dc6b45e5662
more precise error message in parameter unification
schirmer
parents:
22300
diff
changeset

661 
val prt = Sign.string_of_typ thy; 
0dc6b45e5662
more precise error message in parameter unification
schirmer
parents:
22300
diff
changeset

662 
in 
18137  663 
raise TYPE ("unify_parms: failed to unify types " ^ 
22339
0dc6b45e5662
more precise error message in parameter unification
schirmer
parents:
22300
diff
changeset

664 
prt U' ^ " and " ^ prt T', [U', T'], []) 
18137  665 
end; 
666 
fun unify_list (T :: Us) = fold (unify T) Us 

667 
 unify_list [] = I; 

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

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

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

674 
fun inst_parms (i, ps) = 

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

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

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

680 
in map inst_parms idx_parmss end; 

12502  681 

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

682 
in 
12502  683 

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

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

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

686 
 unify_elemss ctxt fixed_parms elemss = 
12502  687 
let 
18137  688 
val thy = ProofContext.theory_of ctxt; 
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset

689 
val phis = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss) 
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset

690 
> map (Element.instT_morphism thy); 
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset

691 
fun inst ((((name, ps), mode), elems), phi) = 
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset

692 
(((name, map (apsnd (Option.map (Morphism.typ phi))) ps), 
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset

693 
map_mode (map (Element.morph_witness phi)) mode), 
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset

694 
map (Element.morph_ctxt phi) elems); 
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset

695 
in map inst (elemss ~~ phis) end; 
12502  696 

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

697 

19810  698 
fun renaming xs parms = zip_options parms xs 
699 
handle Library.UnequalLengths => 

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

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

702 

703 

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

706 
*) 

707 

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

709 
let 

710 
val thy = ProofContext.theory_of ctxt; 

711 

712 
fun merge_tenvs fixed tenv1 tenv2 = 

713 
let 

714 
val [env1, env2] = unify_parms ctxt fixed 

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

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

717 
in 

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

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

720 
end; 

721 

722 
fun merge_syn expr syn1 syn2 = 

19932  723 
Symtab.merge (op = : mixfix * mixfix > bool) (syn1, syn2) 
19783  724 
handle Symtab.DUPS xs => err_in_expr ctxt 
725 
("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

726 

19783  727 
fun params_of (expr as Locale name) = 
728 
let 

22573  729 
val {imports, params, ...} = the_locale thy name; 
19783  730 
val parms = map (fst o fst) params; 
22573  731 
val (parms', types', syn') = params_of imports; 
19783  732 
val all_parms = merge_lists parms' parms; 
733 
val all_types = merge_tenvs [] types' (params > map fst > Symtab.make); 

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

735 
in (all_parms, all_types, all_syn) end 

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

737 
let 

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

739 
val ren = renaming xs parms'; 

740 
(* renaming may reduce number of parameters *) 

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

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

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

744 
handle Symtab.DUP x => 

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

22700  746 
val syn_types = map (apsnd (fn mx => 
747 
SOME (Type.freeze_type (#1 (TypeInfer.paramify_dummies (Syntax.mixfixT mx) 0))))) 

748 
(Symtab.dest new_syn); 

19783  749 
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

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

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

754 
in (new_parms, new_types, new_syn) end 

755 
 params_of (Merge es) = 

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

757 
let 

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

759 
in 

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

761 
merge_syn e syn syn') 

762 
end) 

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

764 

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

766 
in 

767 
(merge_lists prev_parms parms, merge_tenvs fixed_params prev_types types, 

768 
merge_syn expr prev_syn syn) 

769 
end; 

770 

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

772 
fun make_raw_params_elemss (params, tenv, syn) = 

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

774 
Int [Fixes (map (fn p => 

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

776 

777 

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

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

781 
identifier). 

782 

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

784 
((name, ps), (ax_ps, axs)) 

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

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

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

788 
hence axioms may contain additional parameters from later fragments: 

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

790 

791 
Elements are enriched by identifierlike information: 

792 
(((name, ax_ps), axs), elems) 

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

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

795 
typeinstantiated. 

796 

797 
*) 

798 

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

799 
fun flatten_expr ctxt ((prev_idents, prev_syntax), expr) = 
12014  800 
let 
801 
val thy = ProofContext.theory_of ctxt; 

12263  802 

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

803 
fun rename_parms top ren ((name, ps), (parms, mode)) = 
19783  804 
((name, map (Element.rename ren) ps), 
805 
if top 

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

21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset

807 
map_mode (map (Element.morph_witness (Element.rename_morphism ren))) mode) 
19783  808 
else (parms, mode)); 
12263  809 

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

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

811 

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

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

813 
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

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

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

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

817 
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

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

819 
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

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

821 
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

822 
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

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

824 
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

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

826 
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

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

828 
val new_ids = map fst new_regs; 
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset

829 
val new_idTs = 
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset

830 
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

831 

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

832 
val new_wits = new_regs > map (#2 #> map 
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset

833 
(Element.morph_witness 
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset

834 
(Element.instT_morphism thy env $> 
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset

835 
Element.rename_morphism ren $> 
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset

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

837 
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

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

839 
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

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

841 
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

842 
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

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

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

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

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

847 

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

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

849 

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

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

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

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

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

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

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

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

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

858 
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

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

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

861 

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

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

863 

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

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

866 
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

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

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

869 
parms is accumulated list of parameters *) 
12289  870 
let 
22573  871 
val {axiom, imports, params, ...} = the_locale thy name; 
19278  872 
val ps = map (#1 o #1) params; 
22573  873 
val (ids', parms') = identify false imports; 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

875 

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

876 
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

877 
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

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

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

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

884 

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

885 
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

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

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

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

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

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

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

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

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

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

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

896 

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

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

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

900 
val [env] = unify_parms ctxt all_params [ps]; 
18137  901 
val t' = Element.instT_term env t; 
902 
val th' = Element.instT_thm thy env th; 

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

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

904 

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

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

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

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

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

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

910 
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

911 
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

912 
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

913 
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

914 
val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps]; 
21499
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset

915 
val elem_morphism = 
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset

916 
Element.rename_morphism ren $> 
21665
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset

917 
Morphism.name_morphism (NameSpace.qualified (params_prefix params)) $> 
21499
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset

918 
Element.instT_morphism thy env; 
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset

919 
val elems' = map (Element.morph_ctxt elem_morphism) elems; 
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset

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

921 

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

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

923 
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

924 
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

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

926 
val (ids, _) = identify true expr; 
20951
868120282837
gen_rem(s) abandoned in favour of remove / subtract
haftmann
parents:
20911
diff
changeset

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

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

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

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

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

12510  933 
end; 
934 

12070  935 

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

936 
(* activate elements *) 
12273  937 

12510  938 
local 
939 

21686  940 
fun axioms_export axs _ As = 
941 
(Element.satisfy_thm axs #> Drule.implies_intr_list (Library.drop (length axs, As)), fn t => t); 

12263  942 

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

943 

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

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

945 

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

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

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

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

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

951 
let 
18728  952 
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

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

954 
val (ps, qs) = chop (length ts) axs; 
17856  955 
val (_, ctxt') = 
21370
d9dd7b4e5e69
replaced Variable.fix_frees by Variable.auto_fixes (depends on body mode);
wenzelm
parents:
21361
diff
changeset

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

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

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

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

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

961 
 activate_elem _ _ ((ctxt, Assumed axs), Defines defs) = 
15596  962 
let 
18728  963 
val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs; 
19732  964 
val asms = defs' > map (fn ((name, atts), (t, ps)) => 
965 
let val ((c, _), t') = LocalDefs.cert_def ctxt t 

20872  966 
in (t', ((Thm.def_name_optional c name, atts), [(t', ps)])) end); 
17856  967 
val (_, ctxt') = 
21370
d9dd7b4e5e69
replaced Variable.fix_frees by Variable.auto_fixes (depends on body mode);
wenzelm
parents:
21361
diff
changeset

968 
ctxt > fold (Variable.auto_fixes o #1) asms 
19732  969 
> 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

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

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

972 
((ctxt, Derived ths), []) 
21441  973 
 activate_elem _ is_ext ((ctxt, mode), Notes (kind, facts)) = 
15596  974 
let 
18728  975 
val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts; 
21441  976 
val (res, ctxt') = ctxt > ProofContext.note_thmss_i kind facts'; 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

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

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

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

981 
val thy = ProofContext.theory_of ctxt; 
17033  982 
val ((ctxt', _), res) = 
21441  983 
foldl_map (activate_elem ax_in_ctxt (name = "")) 
984 
((ProofContext.qualified_names ctxt, mode), elems) 

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

15696  986 
val ctxt'' = if name = "" then ctxt' 
987 
else let 

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

22351
587845efb4cf
locale: add_locale accepts explicit predicate name, interpretation supports nonmandatory prefixes
haftmann
parents:
22339
diff
changeset

989 
val ctxt'' = put_local_registration (name, ps') ((true, ""), []) ctxt' 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

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

991 
Assumed axs => 
19780  992 
fold (add_local_witness (name, ps') o 
993 
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

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

997 

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

998 
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

999 
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

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

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

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

1003 
(activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt); 
21530  1004 
val elems' = elems > map (Element.map_ctxt_attrib Args.closure); 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset

1005 
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

1006 

12546  1007 
in 
1008 

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

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

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

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

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

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

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

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

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

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

1019 

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

1020 
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

1021 
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

1022 
in (ctxt', (elemss, flat factss)) end; 
15703  1023 

12510  1024 
end; 
1025 

12307  1026 

15696  1027 

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

1029 

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

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

1031 

16458  1032 
fun intern_expr thy (Locale xname) = Locale (intern thy xname) 
1033 
 intern_expr thy (Merge exprs) = Merge (map (intern_expr thy) exprs) 

1034 
 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

1035 

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

1036 

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

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

1038 

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

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

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

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

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

1044 
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

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

1046 
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

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

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

1049 

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

1052 
identifierlike information of the element is as follows: 

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

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

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

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

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

1058 

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

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

1061 
in 
18137  1062 
((ids', 
1063 
merge_syntax ctxt ids' 

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

1065 
handle Symtab.DUPS xs => err_in_locale ctxt 

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

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

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

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

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

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

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

1073 
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

1074 

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

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

1076 

12839  1077 
local 
1078 

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

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

1083 

18671  1084 
fun declare_ext_elem prep_vars (ctxt, Fixes fixes) = 
1085 
let val (vars, _) = prep_vars fixes ctxt 

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

1087 
 declare_ext_elem prep_vars (ctxt, Constrains csts) = 

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

1089 
in (ctxt', []) end 

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

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

1093 

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

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

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

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

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

1101 
 declare_elems _ (ctxt, ((_, Derived _), elems)) = (ctxt, []); 
12727  1102 

12839  1103 
in 
1104 

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

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

1108 
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

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

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

1111 
fold Variable.declare_term (map Free fixed_params) ctxt; 
12727  1112 
val int_elemss = 
1113 
raw_elemss 

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

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

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

1118 
(int_elemss, raw_elemss); 

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

1120 

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

1122 

12839  1123 
local 
1124 

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

1126 

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

12502  1129 

18190  1130 
fun bind_def ctxt (name, ps) eq (xs, env, ths) = 
12839  1131 
let 
18831  1132 
val ((y, T), b) = LocalDefs.abs_def eq; 
13308  1133 
val b' = norm_term env b; 
16458  1134 
val th = abstract_thm (ProofContext.theory_of ctxt) eq; 
13308  1135 
fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)]; 
12839  1136 
in 
21962  1137 
exists (equal y o #1) xs andalso 
1138 
err "Attempt to define previously specified variable"; 

1139 
exists (fn (Free (y', _), _) => y = y'  _ => false) env andalso 

1140 
err "Attempt to redefine variable"; 

16861  1141 
(Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths) 
12839  1142 
end; 
12575  1143 

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

1144 

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

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

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

1147 

18190  1148 
fun eval_text _ _ _ (Fixes _) text = text 
1149 
 eval_text _ _ _ (Constrains _) text = text 

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

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

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

1153 
val ts = maps (map #1 o #2) asms; 
13394  1154 
val ts' = map (norm_term env) ts; 
1155 
val spec' = 

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

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

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

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

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

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

13308  1164 

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

1165 

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

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

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

1168 
turn assumptions and definitions into facts, 
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset

1169 
satisfy hypotheses of facts *) 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1170 

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

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

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

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

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

1175 

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

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

1177 
 finish_derived _ _ (Derived _) (Constrains _) = NONE 
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset

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

1179 
> map (apsnd (map (fn (a, _) => ([Thm.assume (cterm_of sign a)], [])))) 
21441  1180 
> pair Thm.assumptionK > Notes 
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset

1181 
> Element.morph_ctxt satisfy > SOME 
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset

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

1183 
> map (apsnd (fn (d, _) => [([Thm.assume (cterm_of sign d)], [])])) 
21441  1184 
> pair Thm.definitionK > Notes 
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset

1185 
> Element.morph_ctxt satisfy > SOME 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1186 

21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset

1187 
 finish_derived _ satisfy _ (Notes facts) = Notes facts 
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset

1188 
> Element.morph_ctxt satisfy > SOME; 
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset

1189 

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

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

1191 

13308  1192 
fun closeup _ false elem = elem 
1193 
 closeup ctxt true elem = 

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

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

1199 
fun no_binds [] = [] 

18678  1200 
 no_binds _ = error "Illegal term bindings in locale element"; 
13308  1201 
in 
1202 
(case elem of 

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

19585  1204 
(a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps))) 
13308  1205 
 Defines defs => Defines (defs > map (fn (a, (t, ps)) => 
18831  1206 
(a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps)))) 
13308  1207 
 e => e) 
1208 
end; 

12839  1209 

12502  1210 

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

1213 
 finish_ext_elem parms _ (Constrains _, _) = Constrains [] 
12839  1214 
 finish_ext_elem _ close (Assumes asms, propp) = 
1215 
close (Assumes (map #1 asms ~~ propp)) 

1216 
 finish_ext_elem _ close (Defines defs, propp) = 

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

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

1220 

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

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

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

1224 

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

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

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

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

1230 
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

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

1233 
val es' = map_filter 
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset

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

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

1236 
 finish_elems ctxt parms do_close ((text, wits), ((id, Ext e), [propp])) = 
13308  1237 
let 
1238 
val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp); 

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

1240 
in ((text', wits), (id, [Ext e'])) end 
12839  1241 

1242 
in 

12510  1243 

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

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

1245 

13375  1246 
fun finish_elemss ctxt parms do_close = 