author  ballarin 
Fri, 14 Nov 2008 14:00:52 +0100  
changeset 28794  4493633ab401 
parent 28792  1d80cee865de 
child 28822  7ca11ecbc4fb 
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 *) 
28710  66 
val read_context_statement: xstring 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 
28710  69 
val read_context_statement_i: string 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 

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

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

92 

15696  93 
(* Storing results *) 
28794  94 
val local_note_prefix: string > 
95 
(Name.binding * attribute list) * (thm list * attribute list) list > 

96 
Proof.context > (string * thm 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 *) 
28739  104 
val get_interpret_morph: theory > string > bool * string > string > 
28259  105 
(Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) > 
106 
string > term list > Morphism.morphism 

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

107 
val interpretation_i: (Proof.context > Proof.context) > 
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset

108 
bool * string > 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 

21005  112 
val interpretation: (Proof.context > Proof.context) > 
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset

113 
bool * string > expr > 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

114 
string option list * (Attrib.binding * string) list > 
28259  115 
theory > 
116 
(Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state 

21005  117 
val interpretation_in_locale: (Proof.context > Proof.context) > 
118 
xstring * expr > theory > Proof.state 

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

119 
val interpret_i: (Proof.state > Proof.state Seq.seq) > 
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset

120 
bool * string > expr > 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

121 
term option list * (Attrib.binding * term) list > 
28259  122 
bool > Proof.state > 
123 
(Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state 

21005  124 
val interpret: (Proof.state > Proof.state Seq.seq) > 
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset

125 
bool * string > expr > 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

126 
string option list * (Attrib.binding * string) list > 
28259  127 
bool > Proof.state > 
128 
(Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state 

11896  129 
end; 
12839  130 

12289  131 
structure Locale: LOCALE = 
11896  132 
struct 
133 

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

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

135 

27681  136 
fun merge_lists _ xs [] = xs 
137 
 merge_lists _ [] ys = ys 

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

139 

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

19780  141 

20307  142 

28739  143 
(* auxiliary: noting with structured name bindings *) 
144 

28792  145 
fun global_note_prefix kind ((binding, atts), facts_atts_s) thy = 
28739  146 
(*FIXME belongs to theory_target.ML ?*) 
28792  147 
thy 
148 
> Sign.qualified_names 

149 
> Sign.name_decl (fn (bname, (atts, facts_atts_s)) => 

150 
yield_singleton (PureThy.note_thmss kind) ((Name.binding bname, atts), facts_atts_s)) 

151 
(binding, (atts, facts_atts_s)) 

152 
>> snd 

153 
> Sign.restore_naming thy; 

154 

155 
fun local_note_prefix kind ((binding, atts), facts_atts_s) ctxt = 

156 
(*FIXME belongs to theory_target.ML ?*) 

157 
ctxt 

158 
> ProofContext.qualified_names 

159 
> ProofContext.name_decl (fn (bname, (atts, facts_atts_s)) => 

160 
yield_singleton (ProofContext.note_thmss_i kind) ((Name.binding bname, atts), facts_atts_s)) 

161 
(binding, (atts, facts_atts_s)) 

162 
>> snd 

163 
> ProofContext.restore_naming ctxt; 

28739  164 

165 

12273  166 
(** locale elements and expressions **) 
11896  167 

18137  168 
datatype ctxt = datatype Element.ctxt; 
17355  169 

12273  170 
datatype expr = 
171 
Locale of string  

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

172 
Rename of expr * (string * mixfix option) option list  
12273  173 
Merge of expr list; 
11896  174 

12273  175 
val empty = Merge []; 
176 

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

178 
Elem of 'a  Expr of expr; 
12273  179 

18137  180 
fun map_elem f (Elem e) = Elem (f e) 
181 
 map_elem _ (Expr e) = Expr e; 

182 

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

184 

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

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

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

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

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

192 
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

193 
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

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

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

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

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

203 

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

205 

206 

207 

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

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

209 

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

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

211 

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

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

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

214 
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

215 

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

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

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

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

219 

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

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

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

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

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

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

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

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

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

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

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

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

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

232 
 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

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

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

235 

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

236 

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

237 
(** management of registrations in theories and proof contexts **) 
11896  238 

28005  239 
type registration = 
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

240 
{prfx: (bool * string) * string, 
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

241 
(* first component: interpretation prefix; 
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

242 
if the Boolean flag is set, only accesses containing the prefix are generated, 
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

243 
otherwise the prefix may be omitted when accessing theorems etc.) 
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

244 
second component: parameter prefix *) 
28005  245 
exp: Morphism.morphism, 
246 
(* maps content to its originating context *) 

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

248 
(* inverse of exp *) 

249 
wits: Element.witness list, 

250 
(* witnesses of the registration *) 

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

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

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

254 
(* interpreting morphism *) 
28005  255 
} 
256 

15837  257 
structure Registrations : 
258 
sig 

259 
type T 

260 
val empty: T 

261 
val join: T * T > T 

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

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

263 
(term list * 
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

264 
(((bool * string) * string) * 
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset

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

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

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

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

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

270 
T * (term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) > 
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

271 
(((bool * string) * string) * Element.witness list * thm Termtab.table) option 
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset

272 
val insert: theory > term list > ((bool * string) * string) > 
28005  273 
(Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) > 
274 
T > 

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

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

277 
val add_equation: term list > thm > T > T 
28259  278 
(* 
279 
val update_morph: term list > Morphism.morphism > T > T 

280 
val get_morph: theory > T > 

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

282 
Morphism.morphism 

283 
*) 

15837  284 
end = 
285 
struct 

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

288 
type T = registration Termtab.table; 

289 

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

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

291 
{prfx = prfx, exp = exp, imp = imp, wits = wits, eqns = eqns, morph = morph}; 
28005  292 

293 
fun map_reg f reg = 

294 
let 

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

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

296 
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

297 
in mk_reg prfx' exp' imp' wits' eqns' morph' end; 
15837  298 

299 
val empty = Termtab.empty; 

300 

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

302 
fun termify ts = 

18343  303 
Term.list_comb (Const ("", map fastype_of ts > propT), ts); 
15837  304 
fun untermify t = 
305 
let fun ut (Const _) ts = ts 

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

307 
in ut t [] end; 

308 

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

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

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

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

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

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

314 
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

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

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

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

318 
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

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

321 
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

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

324 
(* registrations that subsume t *) 

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

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

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

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

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

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

331 

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

333 
fun lookup thy (regs, (ts, ((impT, _), (imp, _)))) = 
15837  334 
let 
335 
val t = termify ts; 

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

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

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

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

341 
let 
19780  342 
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

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

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

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

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

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

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

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

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

352 
Termtab.map (Morphism.thm inst'_morph) eqns) 
23918  353 
end) 
15837  354 
end; 
355 

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

357 
additionally returns registrations that are strictly subsumed *) 

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

358 
fun insert thy ts prfx (exp, imp) regs = 
15837  359 
let 
360 
val t = termify ts; 

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

361 
val subs = subsumers thy t regs ; 
15837  362 
in (case subs of 
363 
[] => let 

364 
val sups = 

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

365 
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

366 
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

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

370 

25669  371 
fun gen_add f ts regs = 
23918  372 
let 
373 
val t = termify ts; 

374 
in 

28005  375 
Termtab.update (t, map_reg f (the (Termtab.lookup regs t))) regs 
23918  376 
end; 
377 

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

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

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

383 

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

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

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

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

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

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

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

391 

15837  392 
end; 
393 

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

394 

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

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

396 

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

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

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

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

402 

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

403 
val empty = (NameSpace.empty, Symtab.empty); 
12063  404 
val copy = I; 
16458  405 
val extend = I; 
12289  406 

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

407 
fun join_locales _ 
27716  408 
({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

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

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

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

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

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

415 
Library.merge (eq_snd (op =)) (decls2, decls2')), 
27681  416 
regs = merge_alists (op =) regs regs', 
25619  417 
intros = intros, 
418 
dests = dests}; 

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

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

420 
(NameSpace.merge (space1, space2), Symtab.join join_locales (locs1, locs2)); 
22846  421 
); 
15801  422 

423 

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

424 

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

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

426 

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

427 
structure RegistrationsData = GenericDataFun 
22846  428 
( 
429 
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

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

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

432 
fun merge _ = Symtab.join (K Registrations.join); 
22846  433 
); 
12289  434 

12277  435 

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

436 
(** access locales **) 
12277  437 

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

438 
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

439 
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

440 

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

443 
fun the_locale thy name = case get_locale thy name 

444 
of SOME loc => loc 

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

446 

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

448 
thy > LocalesData.map (fn (space, locs) => 
27681  449 
(Sign.declare_name thy name space, Symtab.update (name, loc) locs)); 
11896  450 

18806  451 
fun change_locale name f thy = 
452 
let 

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

454 
the_locale thy name; 
27716  455 
val (axiom', elems', params', decls', regs', intros', dests') = 
456 
f (axiom, elems, params, decls, regs, intros, dests); 

18806  457 
in 
27681  458 
thy 
459 
> (LocalesData.map o apsnd) (Symtab.update (name, {axiom = axiom', 

27716  460 
elems = elems', params = params', 
27681  461 
decls = decls', regs = regs', intros = intros', dests = dests'})) 
462 
end; 

463 

464 
fun print_locales thy = 

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

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

467 
> Pretty.writeln 

18806  468 
end; 
469 

12046  470 

15596  471 
(* access registrations *) 
472 

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

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

474 

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

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

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

478 
 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

479 

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

480 
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

481 
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

482 

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

483 

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

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

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

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

487 
 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

488 

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

489 
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

490 
fun get_local_registration ctxt = get_registration (Context.Proof ctxt); 
15596  491 

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

492 

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

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

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

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

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

497 

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

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

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

500 

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

501 

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

503 

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

504 
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

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

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

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

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

513 
"\nwith the following prefix(es):" ^ 
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset

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

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

517 

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

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

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

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

521 
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

522 

15596  523 

18806  524 
fun put_registration_in_locale name id = 
27716  525 
change_locale name (fn (axiom, elems, params, decls, regs, intros, dests) => 
526 
(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

527 

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

528 

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

529 
(* add witness theorem to registration, ignored if registration not present *) 
15596  530 

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

531 
fun add_witness (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_witness 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_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

535 
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

536 

15596  537 

18806  538 
fun add_witness_in_locale name id thm = 
27716  539 
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

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

541 
fun add (id', thms) = 
18806  542 
if id = id' then (id', thm :: thms) else (id', thms); 
27716  543 
in (axiom, elems, params, decls, map add regs, intros, dests) end); 
15596  544 

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

545 

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

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

547 

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

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

549 
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

550 

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

551 
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

552 
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

553 

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

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

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

556 

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

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

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

559 

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

560 
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

561 
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

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

563 

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

564 

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

565 
(* printing of registrations *) 
15596  566 

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

567 
fun print_registrations show_wits loc ctxt = 
15596  568 
let 
15703  569 
val thy = ProofContext.theory_of ctxt; 
24920  570 
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

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

572 
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

573 
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

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

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

577 
Pretty.enclose "(" ")" (Pretty.breaks (map prt_term' ts)); 
28739  578 
fun prt_prfx ((false, prfx), param_prfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str "(optional)", Pretty.brk 1, Pretty.str param_prfx] 
579 
 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

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

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

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

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

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

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

587 
Pretty.breaks (map (Element.pretty_witness ctxt) witns)) 
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset

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

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

591 
else Pretty.block (prt_core ts eqns) 
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset

592 
 prt_reg (ts, (prfx, _, witns, eqns)) = 
17138  593 
if show_wits 
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset

594 
then Pretty.block ((prt_prfx prfx @ [Pretty.str ":", Pretty.brk 1] @ 
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

595 
prt_core ts eqns @ [Pretty.fbrk, prt_witns witns])) 
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset

596 
else Pretty.block ((prt_prfx prfx @ 
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset

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

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

600 
val regs = RegistrationsData.get (Context.Proof ctxt); 
17412  601 
val loc_regs = Symtab.lookup regs loc_int; 
15596  602 
in 
603 
(case loc_regs of 

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

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

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

606 
val r' = Registrations.dest thy r; 
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset

607 
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

608 
in Pretty.big_list ("interpretations:") (map prt_reg r'') end) 
15596  609 
> Pretty.writeln 
610 
end; 

611 

612 

12277  613 
(* diagnostics *) 
12273  614 

12277  615 
fun err_in_locale ctxt msg ids = 
616 
let 

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

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

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

18678  625 
in error err_msg end; 
12063  626 

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

627 
fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids'); 
12277  628 

629 

19783  630 
fun pretty_ren NONE = Pretty.str "_" 
631 
 pretty_ren (SOME (x, NONE)) = Pretty.str x 

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

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

634 

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

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

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

638 
 pretty_expr thy (Merge es) = 

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

640 

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

642 
 err_in_expr ctxt msg expr = 

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

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

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

646 

12046  647 

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

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

649 

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

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

651 

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

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

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

655 

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

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

657 
let 
18343  658 
fun paramify NONE i = (NONE, i) 
659 
 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

660 

18343  661 
val (Ts', maxidx') = fold_map paramify Ts maxidx; 
662 
val (Us', maxidx'') = fold_map paramify Us maxidx'; 

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

664 

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

667 
 unify _ env = env; 

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

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

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

672 

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

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

674 
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

675 

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

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

677 
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

678 

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

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

680 

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

681 

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

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

684 
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

685 

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

686 

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

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

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

690 

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

691 

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

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

693 
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

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

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

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

698 

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

699 
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

700 

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

701 
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

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

703 

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

704 

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

705 
(* flatten expressions *) 
11896  706 

12510  707 
local 
12502  708 

18137  709 
fun unify_parms ctxt fixed_parms raw_parmss = 
12502  710 
let 
16458  711 
val thy = ProofContext.theory_of ctxt; 
12502  712 
val maxidx = length raw_parmss; 
713 
val idx_parmss = (0 upto maxidx  1) ~~ raw_parmss; 

714 

715 
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

716 
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

717 
val parms = fixed_parms @ maps varify_parms idx_parmss; 
12502  718 

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

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

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

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

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

727 
prt U' ^ " and " ^ prt T', [U', T'], []) 
18137  728 
end; 
729 
fun unify_list (T :: Us) = fold (unify T) Us 

730 
 unify_list [] = I; 

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

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

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

737 
fun inst_parms (i, ps) = 

23178  738 
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

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

743 
in map inst_parms idx_parmss end; 

12502  744 

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

745 
in 
12502  746 

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

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

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

749 
 unify_elemss ctxt fixed_parms elemss = 
12502  750 
let 
18137  751 
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

752 
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

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

754 
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

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

756 
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

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

758 
in map inst (elemss ~~ phis) end; 
12502  759 

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

760 

19810  761 
fun renaming xs parms = zip_options parms xs 
762 
handle Library.UnequalLengths => 

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

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

765 

766 

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

769 
*) 

770 

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

772 
let 

773 
val thy = ProofContext.theory_of ctxt; 

774 

775 
fun merge_tenvs fixed tenv1 tenv2 = 

776 
let 

777 
val [env1, env2] = unify_parms ctxt fixed 

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

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

780 
in 

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

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

783 
end; 

784 

785 
fun merge_syn expr syn1 syn2 = 

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

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

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

789 

19783  790 
fun params_of (expr as Locale name) = 
791 
let 

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

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

19783  795 
 params_of (expr as Rename (e, xs)) = 
796 
let 

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

798 
val ren = renaming xs parms'; 

799 
(* renaming may reduce number of parameters *) 

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

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

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

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

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

807 
(Symtab.dest new_syn); 

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

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

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

813 
in (new_parms, new_types, new_syn) end 

814 
 params_of (Merge es) = 

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

816 
let 

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

818 
in 

27681  819 
(merge_lists (op =) parms parms', merge_tenvs [] types types', 
19783  820 
merge_syn e syn syn') 
821 
end) 

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

823 

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

825 
in 

27681  826 
(merge_lists (op =) prev_parms parms, merge_tenvs fixed_params prev_types types, 
19783  827 
merge_syn expr prev_syn syn) 
828 
end; 

829 

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

831 
fun make_raw_params_elemss (params, tenv, syn) = 

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

833 
Int [Fixes (map (fn p => 

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

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

836 

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

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

840 
identifier). 

841 

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

843 
((name, ps), (ax_ps, axs)) 

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

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

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

847 
hence axioms may contain additional parameters from later fragments: 

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

849 

850 
Elements are enriched by identifierlike information: 

851 
(((name, ax_ps), axs), elems) 

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

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

854 
typeinstantiated. 

855 

856 
*) 

857 

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

858 
fun flatten_expr ctxt ((prev_idents, prev_syntax), expr) = 
12014  859 
let 
860 
val thy = ProofContext.theory_of ctxt; 

12263  861 

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

862 
fun rename_parms top ren ((name, ps), (parms, mode)) = 
19783  863 
((name, map (Element.rename ren) ps), 
864 
if top 

865 
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

866 
map_mode (map (Element.morph_witness (Element.rename_morphism ren))) mode) 
19783  867 
else (parms, mode)); 
12263  868 

27716  869 
(* 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

870 

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

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

872 
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

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

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

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

876 
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

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

878 
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

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

880 
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

881 
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

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

883 
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

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

885 
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

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

887 
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

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

889 
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

890 

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

891 
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

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

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

894 
Element.rename_morphism ren $> 
25669  895 
Element.satisfy_morphism wits) 
896 
#> Element.close_witness)); 

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

897 
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

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

899 
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

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

901 
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

902 
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

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

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

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

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

907 

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

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

909 

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

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

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

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

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

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

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

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

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

918 
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

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

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

921 

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

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

923 

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

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

926 
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

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

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

929 
parms is accumulated list of parameters *) 
12289  930 
let 
27716  931 
val {axiom, params, ...} = the_locale thy name; 
19278  932 
val ps = map (#1 o #1) params; 
27716  933 
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

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

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

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

941 

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

942 
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

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

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

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

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

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

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

949 
in 
27681  950 
(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

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

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

953 

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

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

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

957 
val [env] = unify_parms ctxt all_params [ps]; 
18137  958 
val t' = Element.instT_term env t; 
959 
val th' = Element.instT_thm thy env th; 

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

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

961 

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

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

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

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

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

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

967 
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

968 
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

969 
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

970 
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

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

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

973 
Element.rename_morphism ren $> 
28739  974 
Morphism.name_morphism (Name.add_prefix false (param_prefix params)) $> 
21499
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset

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

976 
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

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

978 

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

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

980 
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

981 
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

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

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

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

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

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

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

988 
in ((prev_idents @ idents, syntax), final_elemss) end; 
12046  989 

12510  990 
end; 
991 

12070  992 

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

993 
(* activate elements *) 
12273  994 

12510  995 
local 
996 

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

12263  999 

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

1000 

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

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

1002 

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

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

1006 
([], (ctxt, mode)) 

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

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

1008 
let 
18728  1009 
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

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

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

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

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

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

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

15596  1019 
let 
18728  1020 
val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs; 
19732  1021 
val asms = defs' > map (fn ((name, atts), (t, ps)) => 
1022 
let val ((c, _), t') = LocalDefs.cert_def ctxt t 

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

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

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

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

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

15596  1031 
let 
18728  1032 
val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts; 
28739  1033 
val (res, ctxt') = ctxt > fold_map (local_note_prefix kind) facts'; 
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
28053
diff
changeset

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

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

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

1038 
val thy = ProofContext.theory_of ctxt; 
27681  1039 
val (res, (ctxt', _)) = fold_map (activate_elem ax_in_ctxt (name = "")) 
1040 
elems (ProofContext.qualified_names ctxt, mode) 

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

1044 
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

1045 
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

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

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

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

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

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

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

1052 
Element.assume_witness thy o Element.witness_prop) axs ctxt'' 
25669  1053 
 Derived ths => 
1054 
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

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

1058 

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

1059 
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

1060 
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

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

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

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

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

1066 
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

1067 

12546  1068 
in 
1069 

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

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

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

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

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

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

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

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

1080 

27681  1081 
fun activate_facts ax_in_ctxt prep_facts args = 
1082 
activate_elemss ax_in_ctxt prep_facts args 

1083 
#>> (apsnd flat o split_list); 

15703  1084 

12510  1085 
end; 
1086 

12307  1087 

15696  1088 

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

1090 

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

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

1092 

16458  1093 
fun intern_expr thy (Locale xname) = Locale (intern thy xname) 
1094 
 intern_expr thy (Merge exprs) = Merge (map (intern_expr thy) exprs) 

1095 
 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

1096 

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

1097 

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

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

1099 

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

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

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

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

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

1105 
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

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

1107 
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

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

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

1110 

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

1113 
identifierlike information of the element is as follows: 

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

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

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

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

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

1119 

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

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

1121 
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

1122 
in 
18137  1123 
((ids', 
1124 
merge_syntax ctxt ids' 

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

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

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

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

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

1129 
[((("", 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

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

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

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

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

1134 
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

1135 

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

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

1137 

12839  1138 
local 
1139 

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

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

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

1144 

1145 
fun declare_ext_elem prep_vars (Fixes fixes) ctxt = 

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

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

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

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

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

1154 

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

1156 
of Int es => fold_map declare_int_elem es ctxt 

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

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

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

12727  1160 

12839  1161 
in 
1162 

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

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

1166 
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

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

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

1169 
fold Variable.declare_term (map Free fixed_params) ctxt; 
12727  1170 
val int_elemss = 
1171 
raw_elemss 

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

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

1173 
> unify_elemss ctxt_with_fixed fixed_params; 
27681  1174 
val (raw_elemss', _) = 
1175 
fold_map (curry (fn ((id, Int _), (_, es) :: elemss) => ((id, Int es), elemss)  x => x)) 

1176 
raw_elemss int_elemss; 

1177 
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

1178 

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

1180 

12839  1181 
local 
1182 

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

1184 

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

12502  1187 

18190  1188 
fun bind_def ctxt (name, ps) eq (xs, env, ths) = 
12839  1189 
let 
18831  1190 
val ((y, T), b) = LocalDefs.abs_def eq; 
13308  1191 
val b' = norm_term env b; 
16458  1192 
val th = abstract_thm (ProofContext.theory_of ctxt) eq; 
13308  1193 
fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)]; 
12839  1194 
in 
28375  1195 
exists (fn (x, _) => x = y) xs andalso 
21962  1196 
err "Attempt to define previously specified variable"; 
1197 
exists (fn (Free (y', _), _) => y = y'  _ => false) env andalso 

1198 
err "Attempt to redefine variable"; 

16861  1199 
(Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths) 
12839  1200 
end; 
12575  1201 

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

1202 

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

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

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

1205 

18190  1206 
fun eval_text _ _ _ (Fixes _) text = text 
1207 
 eval_text _ _ _ (Constrains _) text = text 

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

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

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

1211 
val ts = maps (map #1 o #2) asms; 
13394  1212 
val ts' = map (norm_term env) ts; 
1213 
val spec' = 

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

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

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

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

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

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

13308  1222 

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

1223 

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

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

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

1226 
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

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

1228 

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

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

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

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

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

1233 

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

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

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

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

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

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

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

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

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

1244 

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

1245 
 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

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

1247 

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

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

1249 

13308 