author  haftmann 
Mon, 01 Dec 2008 19:41:16 +0100  
changeset 28941  128459bd72d2 
parent 28940  df0cb410be35 
child 28950  b2db06eb214d 
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 

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

44 

16458  45 
val intern: theory > xstring > string 
24751  46 
val intern_expr: theory > expr > expr 
16458  47 
val extern: theory > string > xstring 
19991
0c9650664d47
Locales no longer generate views. The following functions have changed
ballarin
parents:
19984
diff
changeset

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

49 

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

50 
(* The specification of a locale *) 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

51 
val parameters_of: theory > string > ((string * typ) * mixfix) list 
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

52 
val parameters_of_expr: theory > expr > ((string * typ) * mixfix) list 
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

53 
val local_asms_of: theory > string > (Attrib.binding * term list) list 
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

54 
val global_asms_of: theory > string > (Attrib.binding * term list) list 
27716  55 

56 
(* Theorems *) 

25619  57 
val intros: theory > string > thm list * thm list 
58 
val dests: theory > string > thm list 

27716  59 
(* Not part of the official interface. DO NOT USE *) 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

60 
val facts_of: theory > string > (Attrib.binding * (thm list * Attrib.src list) list) list list 
18795
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset

61 

28691  62 
(* Not part of the official interface. DO NOT USE *) 
63 
val declarations_of: theory > string > declaration list * declaration list; 

64 

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

65 
(* Processing of locale statements *) 
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset

66 
val read_context_statement: string option > Element.context list > 
19585  67 
(string * string list) list list > Proof.context > 
19991
0c9650664d47
Locales no longer generate views. The following functions have changed
ballarin
parents:
19984
diff
changeset

68 
string option * Proof.context * Proof.context * (term * term list) list list 
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset

69 
val read_context_statement_cmd: xstring option > Element.context list > 
21035  70 
(string * string list) list list > Proof.context > 
71 
string option * Proof.context * Proof.context * (term * term list) list list 

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

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

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

78 
Element.context_i list * Proof.context 

15596  79 

80 
(* Diagnostic functions *) 

12758  81 
val print_locales: theory > unit 
18137  82 
val print_locale: theory > bool > expr > Element.context list > unit 
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

83 
val print_registrations: bool > string > Proof.context > unit 
18137  84 

28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset

85 
val add_locale: string > bstring > expr > Element.context_i list > theory 
20965  86 
> string * Proof.context 
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset

87 
val add_locale_cmd: bstring > expr > Element.context 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 *) 
28865  94 
val local_note_qualified: string > 
28940  95 
((Name.binding * attribute list) * (thm list * attribute list) list) list > 
96 
Proof.context > (string * thm list) list * Proof.context 

28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

97 
val add_thmss: string > string > (Attrib.binding * (thm list * Attrib.src list) list) list > 
21582  98 
Proof.context > Proof.context 
24020  99 
val add_type_syntax: string > declaration > Proof.context > Proof.context 
100 
val add_term_syntax: string > declaration > Proof.context > Proof.context 

101 
val add_declaration: string > declaration > Proof.context > Proof.context 

18137  102 

28259  103 
(* Interpretation *) 
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset

104 
val get_interpret_morph: theory > (Name.binding > Name.binding) > string * string > 
28259  105 
(Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) > 
106 
string > term list > Morphism.morphism 

28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset

107 
val interpretation: (Proof.context > Proof.context) > 
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset

108 
(Name.binding > Name.binding) > expr > 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

109 
term option list * (Attrib.binding * term) list > 
28259  110 
theory > 
111 
(Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state 

28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset

112 
val interpretation_cmd: string > expr > string option list * (Attrib.binding * string) list > 
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset

113 
theory > Proof.state 
21005  114 
val interpretation_in_locale: (Proof.context > Proof.context) > 
115 
xstring * expr > theory > Proof.state 

28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset

116 
val interpret: (Proof.state > Proof.state Seq.seq) > 
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset

117 
(Name.binding > Name.binding) > expr > 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

118 
term option list * (Attrib.binding * term) list > 
28259  119 
bool > Proof.state > 
120 
(Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state 

28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset

121 
val interpret_cmd: string > expr > string option list * (Attrib.binding * string) list > 
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset

122 
bool > Proof.state > Proof.state 
11896  123 
end; 
12839  124 

12289  125 
structure Locale: LOCALE = 
11896  126 
struct 
127 

23228
05fb9b2b16d7
added gen_merge_lists/merge_lists/merge_alists (legacy operations from library.ML);
wenzelm
parents:
23178
diff
changeset

128 
(* legacy operations *) 
05fb9b2b16d7
added gen_merge_lists/merge_lists/merge_alists (legacy operations from library.ML);
wenzelm
parents:
23178
diff
changeset

129 

27681  130 
fun merge_lists _ xs [] = xs 
131 
 merge_lists _ [] ys = ys 

132 
 merge_lists eq xs ys = xs @ filter_out (member eq xs) ys; 

133 

134 
fun merge_alists eq xs = merge_lists (eq_fst eq) xs; 

19780  135 

20307  136 

28940  137 
(* auxiliary: noting name bindings with qualified base names *) 
138 

139 
fun global_note_qualified kind facts thy = 

28792  140 
thy 
141 
> Sign.qualified_names 

28940  142 
> PureThy.note_thmss kind facts 
28792  143 
> Sign.restore_naming thy; 
144 

28940  145 
fun local_note_qualified kind facts ctxt = 
28792  146 
ctxt 
147 
> ProofContext.qualified_names 

28940  148 
> ProofContext.note_thmss_i kind facts 
28792  149 
> ProofContext.restore_naming ctxt; 
28739  150 

151 

12273  152 
(** locale elements and expressions **) 
11896  153 

18137  154 
datatype ctxt = datatype Element.ctxt; 
17355  155 

12273  156 
datatype expr = 
157 
Locale of string  

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

158 
Rename of expr * (string * mixfix option) option list  
12273  159 
Merge of expr list; 
11896  160 

12273  161 
val empty = Merge []; 
162 

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

164 
Elem of 'a  Expr of expr; 
12273  165 

18137  166 
fun map_elem f (Elem e) = Elem (f e) 
167 
 map_elem _ (Expr e) = Expr e; 

168 

24020  169 
type decl = declaration * stamp; 
21499
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset

170 

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

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

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

19783  176 
elems: (Element.context_i * stamp) list, 
177 
(* Static content, neither Fixes nor Constrains elements *) 

28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

178 
params: ((string * typ) * mixfix) list, (*all term params*) 
21665
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset

179 
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

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

183 
(* Introduction rules: of delta predicate and locale predicate. *) 
25619  184 
dests: thm list} 
27761
b95e9ba0ca1d
Interpretation command (theory/proof context) no longer simplifies goal.
ballarin
parents:
27716
diff
changeset

185 
(* Destruction rules: projections from locale predicate to predicates of fragments. *) 
11896  186 

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

189 

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

191 

192 

193 

27761
b95e9ba0ca1d
Interpretation command (theory/proof context) no longer simplifies goal.
ballarin
parents:
27716
diff
changeset

194 
(** substitutions on Vars  clone from element.ML **) 
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

195 

35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

196 
(* instantiate types *) 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

197 

35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

198 
fun var_instT_type env = 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

199 
if Vartab.is_empty env then I 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

200 
else Term.map_type_tvar (fn (x, S) => the_default (TVar (x, S)) (Vartab.lookup env x)); 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

201 

35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

202 
fun var_instT_term env = 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

203 
if Vartab.is_empty env then I 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

204 
else Term.map_types (var_instT_type env); 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

205 

35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

206 
fun var_inst_term (envT, env) = 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

207 
if Vartab.is_empty env then var_instT_term envT 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

208 
else 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

209 
let 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

210 
val instT = var_instT_type envT; 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

211 
fun inst (Const (x, T)) = Const (x, instT T) 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

212 
 inst (Free (x, T)) = Free(x, instT T) 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

213 
 inst (Var (xi, T)) = 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

214 
(case Vartab.lookup env xi of 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

215 
NONE => Var (xi, instT T) 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

216 
 SOME t => t) 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

217 
 inst (b as Bound _) = b 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

218 
 inst (Abs (x, T, t)) = Abs (x, instT T, inst t) 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

219 
 inst (t $ u) = inst t $ inst u; 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

220 
in Envir.beta_norm o inst end; 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

221 

35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

222 

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

223 
(** management of registrations in theories and proof contexts **) 
11896  224 

28005  225 
type registration = 
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset

226 
{prfx: (Name.binding > Name.binding) * (string * string), 
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset

227 
(* first component: interpretation name morphism; 
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

228 
second component: parameter prefix *) 
28005  229 
exp: Morphism.morphism, 
230 
(* maps content to its originating context *) 

231 
imp: (typ Vartab.table * typ list) * (term Vartab.table * term list), 

232 
(* inverse of exp *) 

233 
wits: Element.witness list, 

234 
(* witnesses of the registration *) 

28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

235 
eqns: thm Termtab.table, 
28005  236 
(* theorems (equations) interpreting derived concepts and indexed by lhs *) 
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

237 
morph: unit 
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

238 
(* interpreting morphism *) 
28005  239 
} 
240 

15837  241 
structure Registrations : 
242 
sig 

243 
type T 

244 
val empty: T 

245 
val join: T * T > T 

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

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

247 
(term list * 
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset

248 
(((Name.binding > Name.binding) * (string * string)) * 
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

249 
(Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

250 
Element.witness list * 
25095
ea8307dac208
Interpretation equations may have name and/or attribute;
ballarin
parents:
25073
diff
changeset

251 
thm Termtab.table)) list 
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

252 
val test: theory > T * term list > bool 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

253 
val lookup: theory > 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

254 
T * (term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) > 
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset

255 
(((Name.binding > Name.binding) * (string * string)) * Element.witness list * thm Termtab.table) option 
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset

256 
val insert: theory > term list > ((Name.binding > Name.binding) * (string * string)) > 
28005  257 
(Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) > 
258 
T > 

28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset

259 
T * (term list * (((Name.binding > Name.binding) * (string * string)) * Element.witness list)) list 
19780  260 
val add_witness: term list > Element.witness > T > T 
25095
ea8307dac208
Interpretation equations may have name and/or attribute;
ballarin
parents:
25073
diff
changeset

261 
val add_equation: term list > thm > T > T 
28259  262 
(* 
263 
val update_morph: term list > Morphism.morphism > T > T 

264 
val get_morph: theory > T > 

265 
term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list)) > 

266 
Morphism.morphism 

267 
*) 

15837  268 
end = 
269 
struct 

28005  270 
(* A registration is indexed by parameter instantiation. 
271 
NB: index is exported whereas content is internalised. *) 

272 
type T = registration Termtab.table; 

273 

28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

274 
fun mk_reg prfx exp imp wits eqns morph = 
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

275 
{prfx = prfx, exp = exp, imp = imp, wits = wits, eqns = eqns, morph = morph}; 
28005  276 

277 
fun map_reg f reg = 

278 
let 

28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

279 
val {prfx, exp, imp, wits, eqns, morph} = reg; 
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

280 
val (prfx', exp', imp', wits', eqns', morph') = f (prfx, exp, imp, wits, eqns, morph); 
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

281 
in mk_reg prfx' exp' imp' wits' eqns' morph' end; 
15837  282 

283 
val empty = Termtab.empty; 

284 

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

286 
fun termify ts = 

18343  287 
Term.list_comb (Const ("", map fastype_of ts > propT), ts); 
15837  288 
fun untermify t = 
289 
let fun ut (Const _) ts = ts 

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

291 
in ut t [] end; 

292 

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

293 
(* joining of registrations: 
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset

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

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

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

297 
eqn of right theory takes precedence *) 
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

298 
fun join (r1, r2) = Termtab.join (fn _ => fn ({eqns = e1, ...}, {prfx = n, exp, imp, wits = w, eqns = e2, morph = m}) => 
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

299 
mk_reg n exp imp w (Termtab.join (fn _ => fn (_, e) => e) (e1, e2)) m) (r1, r2); 
15837  300 

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

301 
fun dest_transfer thy regs = 
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

302 
Termtab.dest regs > map (apsnd (map_reg (fn (n, e, i, ws, es, m) => 
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

303 
(n, e, i, map (Element.transfer_witness thy) ws, Termtab.map (transfer thy) es, m)))); 
28005  304 

305 
fun dest thy regs = dest_transfer thy regs > map (apfst untermify) > 

28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

306 
map (apsnd (fn {prfx, exp, imp, wits, eqns, ...} => (prfx, (exp, imp), wits, eqns))); 
15837  307 

308 
(* registrations that subsume t *) 

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

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

25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

312 
(* test if registration that subsumes the query is present *) 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

313 
fun test thy (regs, ts) = 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

314 
not (null (subsumers thy (termify ts) regs)); 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

315 

15837  316 
(* look up registration, pick one that subsumes the query *) 
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

317 
fun lookup thy (regs, (ts, ((impT, _), (imp, _)))) = 
15837  318 
let 
319 
val t = termify ts; 

19780  320 
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

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

322 
(case subs of 
15837  323 
[] => NONE 
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

324 
 ((t', {prfx, exp = exp', imp = ((impT', domT'), (imp', dom')), wits, eqns, morph}) :: _) => 
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset

325 
let 
19780  326 
val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty); 
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

327 
val tinst' = domT' > map (fn (T as TFree (x, _)) => 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

328 
(x, T > Morphism.typ exp' > Envir.typ_subst_TVars tinst 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

329 
> var_instT_type impT)) > Symtab.make; 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

330 
val inst' = dom' > map (fn (t as Free (x, _)) => 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

331 
(x, t > Morphism.term exp' > Envir.subst_vars (tinst, inst) 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

332 
> var_inst_term (impT, imp))) > Symtab.make; 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

333 
val inst'_morph = Element.inst_morphism thy (tinst', inst'); 
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset

334 
in SOME (prfx, 
28005  335 
map (Element.morph_witness inst'_morph) wits, 
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

336 
Termtab.map (Morphism.thm inst'_morph) eqns) 
23918  337 
end) 
15837  338 
end; 
339 

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

341 
additionally returns registrations that are strictly subsumed *) 

28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset

342 
fun insert thy ts prfx (exp, imp) regs = 
15837  343 
let 
344 
val t = termify ts; 

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

345 
val subs = subsumers thy t regs ; 
15837  346 
in (case subs of 
347 
[] => let 

348 
val sups = 

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

349 
filter (fn (t', _) => Pattern.matches thy (t, t')) (dest_transfer thy regs); 
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset

350 
val sups' = map (apfst untermify) sups > map (fn (ts, {prfx, wits, ...}) => (ts, (prfx, wits))) 
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

351 
in (Termtab.update (t, mk_reg prfx exp imp [] Termtab.empty ()) regs, sups') end 
15837  352 
 _ => (regs, [])) 
353 
end; 

354 

25669  355 
fun gen_add f ts regs = 
23918  356 
let 
357 
val t = termify ts; 

358 
in 

28005  359 
Termtab.update (t, map_reg f (the (Termtab.lookup regs t))) regs 
23918  360 
end; 
361 

15837  362 
(* add witness theorem to registration, 
16169
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset

363 
only if instantiation is exact, otherwise exception Option raised *) 
25669  364 
fun add_witness ts wit regs = 
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

365 
gen_add (fn (x, e, i, wits, eqns, m) => (x, e, i, Element.close_witness wit :: wits, eqns, m)) 
25669  366 
ts regs; 
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

367 

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

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

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

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

371 
fun add_equation ts thm regs = 
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

372 
gen_add (fn (x, e, i, thms, eqns, m) => 
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

373 
(x, e, i, thms, Termtab.update (thm > prop_of > Logic.dest_equals > fst, Thm.close_derivation thm) eqns, m)) 
25669  374 
ts regs; 
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

375 

15837  376 
end; 
377 

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

378 

24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

379 
(** theory data : locales **) 
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

380 

df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

381 
structure LocalesData = TheoryDataFun 
22846  382 
( 
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

383 
type T = NameSpace.T * locale Symtab.table; 
15596  384 
(* 1st entry: locale namespace, 
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

385 
2nd entry: locales of the theory *) 
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

386 

df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

387 
val empty = (NameSpace.empty, Symtab.empty); 
12063  388 
val copy = I; 
16458  389 
val extend = I; 
12289  390 

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

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

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

394 
{axiom = axiom, 
27681  395 
elems = merge_lists (eq_snd (op =)) elems elems', 
16736
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset

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

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

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

399 
Library.merge (eq_snd (op =)) (decls2, decls2')), 
27681  400 
regs = merge_alists (op =) regs regs', 
25619  401 
intros = intros, 
402 
dests = dests}; 

24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

403 
fun merge _ ((space1, locs1), (space2, locs2)) = 
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

404 
(NameSpace.merge (space1, space2), Symtab.join join_locales (locs1, locs2)); 
22846  405 
); 
15801  406 

407 

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

408 

24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

409 
(** context data : registrations **) 
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

410 

df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

411 
structure RegistrationsData = GenericDataFun 
22846  412 
( 
413 
type T = Registrations.T Symtab.table; (*registrations, indexed by locale name*) 

24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

414 
val empty = Symtab.empty; 
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

415 
val extend = I; 
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

416 
fun merge _ = Symtab.join (K Registrations.join); 
22846  417 
); 
12289  418 

12277  419 

24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

420 
(** access locales **) 
12277  421 

24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

422 
val intern = NameSpace.intern o #1 o LocalesData.get; 
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

423 
val extern = NameSpace.extern o #1 o LocalesData.get; 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

424 

27681  425 
fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy)) name; 
426 

427 
fun the_locale thy name = case get_locale thy name 

428 
of SOME loc => loc 

429 
 NONE => error ("Unknown locale " ^ quote name); 

430 

27686  431 
fun register_locale name loc thy = 
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

432 
thy > LocalesData.map (fn (space, locs) => 
27681  433 
(Sign.declare_name thy name space, Symtab.update (name, loc) locs)); 
11896  434 

18806  435 
fun change_locale name f thy = 
436 
let 

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

438 
the_locale thy name; 
27716  439 
val (axiom', elems', params', decls', regs', intros', dests') = 
440 
f (axiom, elems, params, decls, regs, intros, dests); 

18806  441 
in 
27681  442 
thy 
443 
> (LocalesData.map o apsnd) (Symtab.update (name, {axiom = axiom', 

27716  444 
elems = elems', params = params', 
27681  445 
decls = decls', regs = regs', intros = intros', dests = dests'})) 
446 
end; 

447 

448 
fun print_locales thy = 

449 
let val (space, locs) = LocalesData.get thy in 

450 
Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs))) 

451 
> Pretty.writeln 

18806  452 
end; 
453 

12046  454 

15596  455 
(* access registrations *) 
456 

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

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

458 

24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

459 
fun get_registrations ctxt name = 
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

460 
case Symtab.lookup (RegistrationsData.get ctxt) name of 
15696  461 
NONE => [] 
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

462 
 SOME reg => Registrations.dest (Context.theory_of ctxt) reg; 
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

463 

df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

464 
fun get_global_registrations thy = get_registrations (Context.Theory thy); 
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

465 
fun get_local_registrations ctxt = get_registrations (Context.Proof ctxt); 
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

466 

df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

467 

25357
6ea18fd11058
avoid "import" as identifier, which is a keyword in Alice;
wenzelm
parents:
25286
diff
changeset

468 
fun get_registration ctxt imprt (name, ps) = 
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

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

470 
NONE => NONE 
25357
6ea18fd11058
avoid "import" as identifier, which is a keyword in Alice;
wenzelm
parents:
25286
diff
changeset

471 
 SOME reg => Registrations.lookup (Context.theory_of ctxt) (reg, (ps, imprt)); 
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

472 

df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

473 
fun get_global_registration thy = get_registration (Context.Theory thy); 
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

474 
fun get_local_registration ctxt = get_registration (Context.Proof ctxt); 
15596  475 

25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

476 

35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

477 
fun test_registration ctxt (name, ps) = 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

478 
case Symtab.lookup (RegistrationsData.get ctxt) name of 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

479 
NONE => false 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

480 
 SOME reg => Registrations.test (Context.theory_of ctxt) (reg, ps); 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

481 

35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

482 
fun test_global_registration thy = test_registration (Context.Theory thy); 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

483 
fun test_local_registration ctxt = test_registration (Context.Proof ctxt); 
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

484 

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

485 

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

487 

28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

488 
fun put_registration (name, ps) prfx morphs ctxt = 
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

489 
RegistrationsData.map (fn regs => 
15837  490 
let 
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

491 
val thy = Context.theory_of ctxt; 
18343  492 
val reg = the_default Registrations.empty (Symtab.lookup regs name); 
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

493 
val (reg', sups) = Registrations.insert thy ps prfx morphs reg; 
15837  494 
val _ = if not (null sups) then warning 
495 
("Subsumed interpretation(s) of locale " ^ 

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

497 
"\nwith the following prefix(es):" ^ 
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset

498 
commas_quote (map (fn (_, ((_, (_, s)), _)) => s) sups)) 
15837  499 
else (); 
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

500 
in Symtab.update (name, reg') regs end) ctxt; 
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

501 

28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset

502 
fun put_global_registration id prfx morphs = 
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset

503 
Context.theory_map (put_registration id prfx morphs); 
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset

504 
fun put_local_registration id prfx morphs = 
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset

505 
Context.proof_map (put_registration id prfx morphs); 
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

506 

18806  507 
fun put_registration_in_locale name id = 
27716  508 
change_locale name (fn (axiom, elems, params, decls, regs, intros, dests) => 
509 
(axiom, elems, params, decls, regs @ [(id, [])], intros, dests)); 

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

510 

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

511 

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

512 
(* add witness theorem to registration, ignored if registration not present *) 
15596  513 

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

514 
fun add_witness (name, ps) thm = 
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

515 
RegistrationsData.map (Symtab.map_entry name (Registrations.add_witness ps thm)); 
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

516 

df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

517 
fun add_global_witness id thm = Context.theory_map (add_witness id thm); 
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

518 
fun add_local_witness id thm = Context.proof_map (add_witness id thm); 
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

519 

15596  520 

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

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

524 
fun add (id', thms) = 
18806  525 
if id = id' then (id', thm :: thms) else (id', thms); 
27716  526 
in (axiom, elems, params, decls, map add regs, intros, dests) end); 
15596  527 

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

528 

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

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

530 

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

531 
fun add_equation (name, ps) thm = 
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

532 
RegistrationsData.map (Symtab.map_entry name (Registrations.add_equation ps thm)); 
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

533 

df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

534 
fun add_global_equation id thm = Context.theory_map (add_equation id thm); 
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

535 
fun add_local_equation id thm = Context.proof_map (add_equation id thm); 
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

536 

28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

537 
(* 
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

538 
(* update morphism of registration, ignored if registration not present *) 
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

539 

c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

540 
fun update_morph (name, ps) morph = 
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

541 
RegistrationsData.map (Symtab.map_entry name (Registrations.update_morph ps morph)); 
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

542 

c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

543 
fun update_global_morph id morph = Context.theory_map (update_morph id morph); 
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

544 
fun update_local_morph id morph = Context.proof_map (update_morph id morph); 
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

545 
*) 
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

546 

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

547 

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

548 
(* printing of registrations *) 
15596  549 

24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

550 
fun print_registrations show_wits loc ctxt = 
15596  551 
let 
15703  552 
val thy = ProofContext.theory_of ctxt; 
24920  553 
val prt_term = Pretty.quote o Syntax.pretty_term ctxt; 
25095
ea8307dac208
Interpretation equations may have name and/or attribute;
ballarin
parents:
25073
diff
changeset

554 
fun prt_term' t = if !show_types 
ea8307dac208
Interpretation equations may have name and/or attribute;
ballarin
parents:
25073
diff
changeset

555 
then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::", 
ea8307dac208
Interpretation equations may have name and/or attribute;
ballarin
parents:
25073
diff
changeset

556 
Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)] 
ea8307dac208
Interpretation equations may have name and/or attribute;
ballarin
parents:
25073
diff
changeset

557 
else prt_term t; 
23918  558 
val prt_thm = prt_term o prop_of; 
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset

559 
fun prt_inst ts = 
25095
ea8307dac208
Interpretation equations may have name and/or attribute;
ballarin
parents:
25073
diff
changeset

560 
Pretty.enclose "(" ")" (Pretty.breaks (map prt_term' ts)); 
28739  561 
fun prt_prfx ((false, prfx), param_prfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str "(optional)", Pretty.brk 1, Pretty.str param_prfx] 
562 
 prt_prfx ((true, prfx), param_prfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str param_prfx]; 

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

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

564 
 prt_eqns eqns = Pretty.block (Pretty.str "equations:" :: Pretty.brk 1 :: 
23918  565 
Pretty.breaks (map prt_thm eqns)); 
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

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

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

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

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

570 
Pretty.breaks (map (Element.pretty_witness ctxt) witns)) 
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset

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

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

574 
else Pretty.block (prt_core ts eqns) 
15703  575 

16458  576 
val loc_int = intern thy loc; 
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

577 
val regs = RegistrationsData.get (Context.Proof ctxt); 
17412  578 
val loc_regs = Symtab.lookup regs loc_int; 
15596  579 
in 
580 
(case loc_regs of 

24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

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

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

583 
val r' = Registrations.dest thy r; 
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset

584 
val r'' = Library.sort_wrt (fn (_, ((_, (_, prfx)), _, _, _)) => prfx) r'; 
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

585 
in Pretty.big_list ("interpretations:") (map prt_reg r'') end) 
15596  586 
> Pretty.writeln 
587 
end; 

588 

589 

12277  590 
(* diagnostics *) 
12273  591 

12277  592 
fun err_in_locale ctxt msg ids = 
593 
let 

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

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

597 
val prt_ids = flat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids)); 
12502  598 
val err_msg = 
28375  599 
if forall (fn (s, _) => s = "") ids then msg 
12502  600 
else msg ^ "\n" ^ Pretty.string_of (Pretty.block 
601 
(Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids)); 

18678  602 
in error err_msg end; 
12063  603 

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

604 
fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids'); 
12277  605 

606 

19783  607 
fun pretty_ren NONE = Pretty.str "_" 
608 
 pretty_ren (SOME (x, NONE)) = Pretty.str x 

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

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

611 

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

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

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

615 
 pretty_expr thy (Merge es) = 

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

617 

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

619 
 err_in_expr ctxt msg expr = 

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

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

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

623 

12046  624 

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

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

626 

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

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

628 

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

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

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

632 

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

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

634 
let 
18343  635 
fun paramify NONE i = (NONE, i) 
636 
 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

637 

18343  638 
val (Ts', maxidx') = fold_map paramify Ts maxidx; 
639 
val (Us', maxidx'') = fold_map paramify Us maxidx'; 

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

641 

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

644 
 unify _ env = env; 

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

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

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

649 

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

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

651 
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

652 

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

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

654 
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

655 

28862  656 
fun param_prefix locale_name params = (NameSpace.base locale_name ^ "_locale", space_implode "_" params); 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

657 

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

658 

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

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

661 
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

662 

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

663 

19932  664 
fun merge_syntax ctxt ids ss = Symtab.merge (op = : mixfix * mixfix > bool) ss 
23655
d2d1138e0ddc
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents:
23591
diff
changeset

665 
handle Symtab.DUP x => err_in_locale ctxt 
d2d1138e0ddc
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents:
23591
diff
changeset

666 
("Conflicting syntax for parameter: " ^ quote x) (map fst ids); 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

667 

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

668 

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

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

670 
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

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

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

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

675 

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

676 
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

677 

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

678 
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

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

680 

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

681 

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

682 
(* flatten expressions *) 
11896  683 

12510  684 
local 
12502  685 

18137  686 
fun unify_parms ctxt fixed_parms raw_parmss = 
12502  687 
let 
16458  688 
val thy = ProofContext.theory_of ctxt; 
12502  689 
val maxidx = length raw_parmss; 
690 
val idx_parmss = (0 upto maxidx  1) ~~ raw_parmss; 

691 

692 
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

693 
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

694 
val parms = fixed_parms @ maps varify_parms idx_parmss; 
12502  695 

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

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

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

700 
val U' = Envir.norm_type (fst envir) U; 
26948  701 
val prt = Syntax.string_of_typ ctxt; 
22339
0dc6b45e5662
more precise error message in parameter unification
schirmer
parents:
22300
diff
changeset

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

704 
prt U' ^ " and " ^ prt T', [U', T'], []) 
18137  705 
end; 
706 
fun unify_list (T :: Us) = fold (unify T) Us 

707 
 unify_list [] = I; 

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

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

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

714 
fun inst_parms (i, ps) = 

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

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

720 
in map inst_parms idx_parmss end; 

12502  721 

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

722 
in 
12502  723 

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

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

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

726 
 unify_elemss ctxt fixed_parms elemss = 
12502  727 
let 
18137  728 
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

729 
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

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

731 
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

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

733 
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

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

735 
in map inst (elemss ~~ phis) end; 
12502  736 

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

737 

19810  738 
fun renaming xs parms = zip_options parms xs 
739 
handle Library.UnequalLengths => 

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

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

742 

743 

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

746 
*) 

747 

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

749 
let 

750 
val thy = ProofContext.theory_of ctxt; 

751 

752 
fun merge_tenvs fixed tenv1 tenv2 = 

753 
let 

754 
val [env1, env2] = unify_parms ctxt fixed 

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

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

757 
in 

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

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

760 
end; 

761 

762 
fun merge_syn expr syn1 syn2 = 

19932  763 
Symtab.merge (op = : mixfix * mixfix > bool) (syn1, syn2) 
23655
d2d1138e0ddc
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents:
23591
diff
changeset

764 
handle Symtab.DUP x => err_in_expr ctxt 
d2d1138e0ddc
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents:
23591
diff
changeset

765 
("Conflicting syntax for parameter: " ^ quote x) expr; 
20366
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset

766 

19783  767 
fun params_of (expr as Locale name) = 
768 
let 

27716  769 
val {params, ...} = the_locale thy name; 
770 
in (map (fst o fst) params, params > map fst > Symtab.make, 

771 
params > map (apfst fst) > Symtab.make) end 

19783  772 
 params_of (expr as Rename (e, xs)) = 
773 
let 

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

775 
val ren = renaming xs parms'; 

776 
(* renaming may reduce number of parameters *) 

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

28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
28053
diff
changeset

778 
val ren_syn = syn' > Symtab.dest > map (Element.rename_var_name ren); 
19783  779 
val new_syn = fold (Symtab.insert (op =)) ren_syn Symtab.empty 
780 
handle Symtab.DUP x => 

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

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

784 
(Symtab.dest new_syn); 

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

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

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

790 
in (new_parms, new_types, new_syn) end 

791 
 params_of (Merge es) = 

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

793 
let 

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

795 
in 

27681  796 
(merge_lists (op =) parms parms', merge_tenvs [] types types', 
19783  797 
merge_syn e syn syn') 
798 
end) 

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

800 

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

802 
in 

27681  803 
(merge_lists (op =) prev_parms parms, merge_tenvs fixed_params prev_types types, 
19783  804 
merge_syn expr prev_syn syn) 
805 
end; 

806 

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

808 
fun make_raw_params_elemss (params, tenv, syn) = 

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

810 
Int [Fixes (map (fn p => 

28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
28053
diff
changeset

811 
(Name.binding p, Symtab.lookup tenv p, Symtab.lookup syn p > the)) params)])]; 
19783  812 

813 

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

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

817 
identifier). 

818 

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

820 
((name, ps), (ax_ps, axs)) 

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

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

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

824 
hence axioms may contain additional parameters from later fragments: 

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

826 

827 
Elements are enriched by identifierlike information: 

828 
(((name, ax_ps), axs), elems) 

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

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

831 
typeinstantiated. 

832 

833 
*) 

834 

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

835 
fun flatten_expr ctxt ((prev_idents, prev_syntax), expr) = 
12014  836 
let 
837 
val thy = ProofContext.theory_of ctxt; 

12263  838 

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

839 
fun rename_parms top ren ((name, ps), (parms, mode)) = 
19783  840 
((name, map (Element.rename ren) ps), 
841 
if top 

842 
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

843 
map_mode (map (Element.morph_witness (Element.rename_morphism ren))) mode) 
19783  844 
else (parms, mode)); 
12263  845 

27716  846 
(* add (name, pTs) 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

847 

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

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

849 
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

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

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

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

853 
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

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

855 
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

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

857 
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

858 
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

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

860 
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

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

862 
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

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

864 
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

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

866 
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

867 

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

868 
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

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

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

871 
Element.rename_morphism ren $> 
25669  872 
Element.satisfy_morphism wits) 
873 
#> Element.close_witness)); 

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

874 
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

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

876 
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

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

878 
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

879 
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

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

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

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

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

884 

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

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

886 

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

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

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

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

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

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

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

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

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

895 
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

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

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

898 

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

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

900 

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

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

903 
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

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

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

906 
parms is accumulated list of parameters *) 
12289  907 
let 
27716  908 
val {axiom, params, ...} = the_locale thy name; 
19278  909 
val ps = map (#1 o #1) params; 
27716  910 
val (_, ids'', _) = add_with_regs ((name, map #1 params), Assumed []) ([], [], []); 
20167
fe5fd4fd4114
Strict dfs traversal of imported and registered identifiers.
ballarin
parents:
20092
diff
changeset

911 
val ids_ax = if top then fst (fold_map (axiomify ps) ids'' axiom) else ids''; 
27716  912 
in (ids_ax, ps) end 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

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

918 

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

919 
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

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

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

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

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

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

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

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

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

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

930 

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

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

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

934 
val [env] = unify_parms ctxt all_params [ps]; 
18137  935 
val t' = Element.instT_term env t; 
936 
val th' = Element.instT_thm thy env th; 

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

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

938 

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

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

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

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

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

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

944 
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

945 
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

946 
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

947 
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

948 
val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps]; 
28862  949 
val (lprfx, pprfx) = param_prefix name params; 
28941  950 
val add_prefices = pprfx <> "" ? Binding.add_prefix false pprfx 
951 
#> Binding.add_prefix false lprfx; 

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

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

953 
Element.rename_morphism ren $> 
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset

954 
Morphism.name_morphism add_prefices $> 
21499
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset

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

956 
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

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

958 

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

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

960 
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

961 
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

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

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

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

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

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

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

968 
in ((prev_idents @ idents, syntax), final_elemss) end; 
12046  969 

12510  970 
end; 
971 

12070  972 

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

973 
(* activate elements *) 
12273  974 

12510  975 
local 
976 

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

12263  979 

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

980 

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

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

982 

27681  983 
fun activate_elem _ _ (Fixes fixes) (ctxt, mode) = 
984 
([], (ctxt > ProofContext.add_fixes_i fixes > snd, mode)) 

985 
 activate_elem _ _ (Constrains _) (ctxt, mode) = 

986 
([], (ctxt, mode)) 

987 
 activate_elem ax_in_ctxt _ (Assumes asms) (ctxt, Assumed axs) = 

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

988 
let 
18728  989 
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

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

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

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

994 
> ProofContext.add_assms_i (axioms_export (if ax_in_ctxt then ps else [])) asms'; 
27681  995 
in ([], (ctxt', Assumed qs)) end 
996 
 activate_elem _ _ (Assumes asms) (ctxt, Derived ths) = 

997 
([], (ctxt, Derived ths)) 

998 
 activate_elem _ _ (Defines defs) (ctxt, Assumed axs) = 

15596  999 
let 
18728  1000 
val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs; 
19732  1001 
val asms = defs' > map (fn ((name, atts), (t, ps)) => 
1002 
let val ((c, _), t') = LocalDefs.cert_def ctxt t 

28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
28053
diff
changeset

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

1005 
ctxt > fold (Variable.auto_fixes o #1) asms 
19732  1006 
> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms); 
27681  1007 
in ([], (ctxt', Assumed axs)) end 
1008 
 activate_elem _ _ (Defines defs) (ctxt, Derived ths) = 

1009 
([], (ctxt, Derived ths)) 

1010 
 activate_elem _ is_ext (Notes (kind, facts)) (ctxt, mode) = 

15596  1011 
let 
18728  1012 
val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts; 
28940  1013 
val (res, ctxt') = ctxt > local_note_qualified kind facts'; 
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
28053
diff
changeset

1014 
in (if is_ext then (map (#1 o #1) facts' ~~ map #2 res) else [], (ctxt', mode)) end; 
12502  1015 

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

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

1018 
val thy = ProofContext.theory_of ctxt; 
27681  1019 
val (res, (ctxt', _)) = fold_map (activate_elem ax_in_ctxt (name = "")) 
1020 
elems (ProofContext.qualified_names ctxt, mode) 

21441  1021 
handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)]; 
15696  1022 
val ctxt'' = if name = "" then ctxt' 
1023 
else let 

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

24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

1025 
in if test_local_registration ctxt' (name, ps') then ctxt' 
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

1026 
else let 
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset

1027 
val ctxt'' = put_local_registration (name, ps') (I, (NameSpace.base name, "")) 
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

1028 
(Morphism.identity, ((Vartab.empty, []), (Vartab.empty, []) )) ctxt' 
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

1029 
in case mode of 
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

1030 
Assumed axs => 
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

1031 
fold (add_local_witness (name, ps') o 
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

1032 
Element.assume_witness thy o Element.witness_prop) axs ctxt'' 
25669  1033 
 Derived ths => 
1034 
fold (add_local_witness (name, ps')) ths ctxt'' 

24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset

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

1038 

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

1039 
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

1040 
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

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

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

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

1044 
(activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt); 
21530  1045 
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

1046 
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

1047 

12546  1048 
in 
1049 

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

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

1052 
context elements, extends ctxt by the context elements yielding 
27681  1053 
ctxt' and returns ((elemss', facts), ctxt'). 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

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

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

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

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

1060 

27681  1061 
fun activate_facts ax_in_ctxt prep_facts args = 
1062 
activate_elemss ax_in_ctxt prep_facts args 

1063 
#>> (apsnd flat o split_list); 

15703  1064 

12510  1065 
end; 
1066 

12307  1067 

15696  1068 

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

1070 

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

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

1072 

16458  1073 
fun intern_expr thy (Locale xname) = Locale (intern thy xname) 
1074 
 intern_expr thy (Merge exprs) = Merge (map (intern_expr thy) exprs) 

1075 
 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

1076 

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

1077 

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

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

1079 

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

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

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

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

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

1085 
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

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

1087 
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

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

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

1090 

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

1093 
identifierlike information of the element is as follows: 

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

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

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

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

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

1099 

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

1100 
fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let 
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
28053
diff
changeset

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

1102 
in 
18137  1103 
((ids', 
1104 
merge_syntax ctxt ids' 

28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
28053
diff
changeset

1105 
(syn, Symtab.make (map (fn fx => (Name.name_of (#1 fx), #3 fx)) fixes)) 
23655
d2d1138e0ddc
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents:
23591
diff
changeset

1106 
handle Symtab.DUP x => err_in_locale ctxt 
d2d1138e0ddc
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents:
23591
diff
changeset

1107 
("Conflicting syntax for parameter: " ^ quote x) 
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset

1108 
(map #1 ids')), 
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
28053
diff
changeset

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

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

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

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

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

1114 
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

1115 

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

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

1117 

12839  1118 
local 
1119 

27681  1120 
fun declare_int_elem (Fixes fixes) ctxt = 
1121 
([], ctxt > ProofContext.add_fixes_i (map (fn (x, T, mx) => 

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

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

1124 

1125 
fun declare_ext_elem prep_vars (Fixes fixes) ctxt = 

18671  1126 
let val (vars, _) = prep_vars fixes ctxt 
27681  1127 
in ([], ctxt > ProofContext.add_fixes_i vars > snd) end 
1128 
 declare_ext_elem prep_vars (Constrains csts) ctxt = 

28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
28053
diff
changeset

1129 
let val (_, ctxt') = prep_vars (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) csts) ctxt 
27681  1130 
in ([], ctxt') end 
1131 
 declare_ext_elem _ (Assumes asms) ctxt = (map #2 asms, ctxt) 

1132 
 declare_ext_elem _ (Defines defs) ctxt = (map (fn (_, (t, ps)) => [(t, ps)]) defs, ctxt) 

1133 
 declare_ext_elem _ (Notes _) ctxt = ([], ctxt); 

1134 

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

1136 
of Int es => fold_map declare_int_elem es ctxt 

1137 
 Ext e => declare_ext_elem prep_vars e ctxt >> single) 

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

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

12727  1140 

12839  1141 
in 
1142 

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

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

1146 
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

1147 
distinct from types of parameters in target (fixed_params). *) 
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

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

1149 
fold Variable.declare_term (map Free fixed_params) ctxt; 
12727  1150 
val int_elemss = 
1151 
raw_elemss 

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

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

1153 
> unify_elemss ctxt_with_fixed fixed_params; 
27681  1154 
val (raw_elemss', _) = 
1155 
fold_map (curry (fn ((id, Int _), (_, es) :: elemss) => ((id, Int es), elemss)  x => x)) 

1156 
raw_elemss int_elemss; 

1157 
in fold_map (declare_elems prep_vars) raw_elemss' ctxt end; 

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

1158 

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

1160 

12839  1161 
local 
1162 

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

1164 

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

12502  1167 

18190  1168 
fun bind_def ctxt (name, ps) eq (xs, env, ths) = 
12839  1169 
let 
18831  1170 
val ((y, T), b) = LocalDefs.abs_def eq; 
13308  1171 
val b' = norm_term env b; 
16458  1172 
val th = abstract_thm (ProofContext.theory_of ctxt) eq; 
13308  1173 
fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)]; 
12839  1174 
in 
28375  1175 
exists (fn (x, _) => x = y) xs andalso 
21962  1176 
err "Attempt to define previously specified variable"; 
1177 
exists (fn (Free (y', _), _) => y = y'  _ => false) env andalso 

1178 
err "Attempt to redefine variable"; 

16861  1179 
(Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths) 
12839  1180 
end; 
12575  1181 

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

1182 

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

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

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

1185 

18190  1186 
fun eval_text _ _ _ (Fixes _) text = text 
1187 
 eval_text _ _ _ (Constrains _) text = text 

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

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

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

1191 
val ts = maps (map #1 o #2) asms; 
13394  1192 
val ts' = map (norm_term env) ts; 
1193 
val spec' = 

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

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

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

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

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

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

13308  1202 

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

1203 

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

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

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

1206 
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

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

1208 

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

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

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

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

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

1213 

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

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

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

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

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

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

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

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

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

1224 

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

1225 
 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

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

1227 

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

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

1229 

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

12839  1232 
let 
13308  1233 
fun close_frees t = 
26206  1234 
let 
1235 
val rev_frees = 

1236 
Term.fold_aterms (fn Free (x, T) => 

1237 
if Variable.is_fixed ctxt x then I else insert (op =) (x, T)  _ => I) t []; 

26299
2f387f5c0f52
closeup: recover original order of free variables!
wenzelm
parents:
26206
diff
changeset

1238 
in Term.list_all_free (rev rev_frees, t) end; 
13308  1239 

1240 
fun no_binds [] = [] 

18678  1241 
 no_binds _ = error "Illegal term bindings in locale element"; 
13308  1242 
in 
1243 
(case elem of 

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

19585  1245 
(a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps))) 
13308  1246 
 Defines defs => Defines (defs > map (fn (a, (t, ps)) => 
18831  1247 
(a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps)))) 
13308  1248 
 e => e) 
1249 
end; 

12839
