author  ballarin 
Thu, 24 Mar 2005 17:03:37 +0100  
changeset 15624  484178635bd8 
parent 15623  8b40f741597c 
child 15696  1da4ce092c0b 
permissions  rwrr 
12014  1 
(* Title: Pure/Isar/locale.ML 
11896  2 
ID: $Id$ 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

3 
Author: Clemens Ballarin, TU Muenchen; Markus Wenzel, LMU/TU Muenchen 
11896  4 

12058  5 
Locales  Isar proof contexts as metalevel predicates, with local 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

6 
syntax and implicit structures. 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

7 

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

8 
Draws some basic ideas from Florian Kammueller's original version of 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

9 
locales, but uses the richer infrastructure of Isar instead of the raw 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

10 
metalogic. Furthermore, we provide structured import of contexts 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

11 
(with merge and rename operations), as well as typeinference of the 
13375  12 
signature parts, and predicate definitions of the specification text. 
14446  13 

14 
See also: 

15 

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

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

15099  18 
Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 3450, 2004. 
11896  19 
*) 
20 

21 
signature LOCALE = 

22 
sig 

12046  23 
type context 
15596  24 
type multi_attribute 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

25 

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

26 
(* Constructors for elem, expr and elem_expr are 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

27 
currently only used for inputting locales (outer_parse.ML). *) 
12046  28 
datatype ('typ, 'term, 'fact, 'att) elem = 
12058  29 
Fixes of (string * 'typ option * mixfix option) list  
12046  30 
Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list  
31 
Defines of ((string * 'att list) * ('term * 'term list)) list  

12273  32 
Notes of ((string * 'att list) * ('fact * 'att list) list) list 
33 
datatype expr = 

34 
Locale of string  

35 
Rename of expr * string option list  

36 
Merge of expr list 

37 
val empty: expr 

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

38 
datatype 'a elem_expr = Elem of 'a  Expr of expr 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

39 

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

40 
(* Abstract interface to locales *) 
12046  41 
type 'att element 
42 
type 'att element_i 

43 
type locale 

44 
val intern: Sign.sg > xstring > string 

12014  45 
val cond_extern: Sign.sg > string > xstring 
12502  46 
val the_locale: theory > string > locale 
15596  47 
val map_attrib_element: ('att > multi_attribute) > 'att element > 
48 
multi_attribute element 

49 
val map_attrib_element_i: ('att > multi_attribute) > 'att element_i > 

50 
multi_attribute element_i 

51 
val map_attrib_elem_or_expr: ('att > multi_attribute) > 

52 
'att element elem_expr > multi_attribute element elem_expr 

53 
val map_attrib_elem_or_expr_i: ('att > multi_attribute) > 

54 
'att element_i elem_expr > multi_attribute element_i elem_expr 

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

55 

15596  56 
(* Processing of locale statements *) 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

57 
val read_context_statement: xstring option > 
15596  58 
multi_attribute element elem_expr list > 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

59 
(string * (string list * string list)) list list > context > 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

60 
string option * (cterm list * cterm list) * context * context * 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

61 
(term * (term list * term list)) list list 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

62 
val cert_context_statement: string option > 
15596  63 
multi_attribute element_i elem_expr list > 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

64 
(term * (term list * term list)) list list > context > 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

65 
string option * (cterm list * cterm list) * context * context * 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

66 
(term * (term list * term list)) list list 
15596  67 

68 
(* Diagnostic functions *) 

12758  69 
val print_locales: theory > unit 
15596  70 
val print_locale: theory > expr > multi_attribute element list > unit 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

71 
val print_global_registrations: string > theory > unit 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

72 
val print_local_registrations: string > context > unit 
15596  73 

74 
val add_locale: bool > bstring > expr > multi_attribute element list > theory > theory 

75 
val add_locale_i: bool > bstring > expr > multi_attribute element_i list 

13394  76 
> theory > theory 
15531  77 
val smart_note_thmss: string > (string * 'a) option > 
12958  78 
((bstring * theory attribute list) * (thm list * theory attribute list) list) list > 
79 
theory > theory * (bstring * thm list) list 

14564  80 
val note_thmss: string > xstring > 
15596  81 
((bstring * multi_attribute list) * (thmref * multi_attribute list) list) list > 
12711  82 
theory > theory * (bstring * thm list) list 
14564  83 
val note_thmss_i: string > string > 
15596  84 
((bstring * multi_attribute list) * (thm list * multi_attribute list) list) list > 
12711  85 
theory > theory * (bstring * thm list) list 
15596  86 
val add_thmss: string > ((string * thm list) * multi_attribute list) list > 
13375  87 
theory * context > (theory * context) * (string * thm list) list 
15596  88 

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

89 
(* Locale interpretation *) 
14528
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

90 
val instantiate: string > string * context attribute list 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

91 
> thm list option > context > context 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

92 
val prep_global_registration: 
15596  93 
string * theory attribute list > expr > string option list > theory > 
94 
theory * ((string * term list) * term list) list * (theory > theory) 

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

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

96 
string * context attribute list > expr > string option list > context > 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

97 
context * ((string * term list) * term list) list * (context > context) 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

98 
val add_global_witness: 
15596  99 
string * term list > thm > theory > theory 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

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

101 
string * term list > thm > context > context 
15596  102 

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

103 
(* Theory setup for locales *) 
11896  104 
val setup: (theory > theory) list 
105 
end; 

12839  106 

12289  107 
structure Locale: LOCALE = 
11896  108 
struct 
109 

12273  110 
(** locale elements and expressions **) 
11896  111 

12014  112 
type context = ProofContext.context; 
11896  113 

15596  114 
(* Locales store theory attributes (for activation in theories) 
115 
and context attributes (for activation in contexts) *) 

116 
type multi_attribute = theory attribute * context attribute; 

117 

12046  118 
datatype ('typ, 'term, 'fact, 'att) elem = 
12058  119 
Fixes of (string * 'typ option * mixfix option) list  
12046  120 
Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list  
121 
Defines of ((string * 'att list) * ('term * 'term list)) list  

12273  122 
Notes of ((string * 'att list) * ('fact * 'att list) list) list; 
123 

124 
datatype expr = 

125 
Locale of string  

126 
Rename of expr * string option list  

127 
Merge of expr list; 

11896  128 

12273  129 
val empty = Merge []; 
130 

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

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

132 
Elem of 'a  Expr of expr; 
12273  133 

15456
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15212
diff
changeset

134 
type 'att element = (string, string, thmref, 'att) elem; 
15127  135 
type 'att element_i = (typ, term, thm list, 'att) elem; 
12070  136 

137 
type locale = 

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

138 
{predicate: cterm list * thm list, 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

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

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

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

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

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

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

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

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

148 
import: expr, (*dynamic import*) 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

149 
elems: (multi_attribute element_i * stamp) list, (*static content*) 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

150 
params: (string * typ option) list * string list} (*all/local params*) 
12063  151 

11896  152 

153 
(** theory data **) 

154 

15596  155 
structure Termlisttab = TableFun(type key = term list 
156 
val ord = Library.list_ord Term.term_ord); 

157 

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

158 
structure GlobalLocalesArgs = 
11896  159 
struct 
12014  160 
val name = "Isar/locales"; 
15596  161 
type T = NameSpace.T * locale Symtab.table * 
162 
((string * theory attribute list) * thm list) Termlisttab.table 

163 
Symtab.table; 

164 
(* 1st entry: locale namespace, 

165 
2nd entry: locales of the theory, 

166 
3rd entry: registrations: theorems instantiating locale assumptions, 

167 
with prefix and attributes, indexed by locale name and parameter 

168 
instantiation *) 

11896  169 

15596  170 
val empty = (NameSpace.empty, Symtab.empty, Symtab.empty); 
12063  171 
val copy = I; 
12118  172 
val prep_ext = I; 
12289  173 

15596  174 
fun join_locs ({predicate, import, elems, params}: locale, 
175 
{elems = elems', ...}: locale) = 

176 
SOME {predicate = predicate, import = import, 

177 
elems = gen_merge_lists eq_snd elems elems', 

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

178 
params = params}; 
15596  179 
(* joining of registrations: prefix and attributes of left theory, 
180 
thmsss are equal *) 

181 
fun join_regs (reg, _) = SOME reg; 

182 
fun merge ((space1, locs1, regs1), (space2, locs2, regs2)) = 

183 
(NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2), 

184 
Symtab.join (SOME o Termlisttab.join join_regs) (regs1, regs2)); 

12289  185 

15596  186 
fun print _ (space, locs, _) = 
12273  187 
Pretty.strs ("locales:" :: map (NameSpace.cond_extern space o #1) (Symtab.dest locs)) 
12014  188 
> Pretty.writeln; 
11896  189 
end; 
190 

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

191 
structure GlobalLocalesData = TheoryDataFun(GlobalLocalesArgs); 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

192 

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

193 
(** context data **) 
11896  194 

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

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

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

197 
val name = "Isar/locales"; 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

198 
type T = ((string * context attribute list) * thm list) Termlisttab.table 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

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

200 
(* registrations: theorems instantiating locale assumptions, 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

201 
with prefix and attributes, indexed by locale name and parameter 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

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

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

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

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

206 

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

207 
structure LocalLocalesData = ProofDataFun(LocalLocalesArgs); 
12289  208 

12277  209 

210 
(* access locales *) 

211 

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

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

213 

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

214 
val intern = NameSpace.intern o #1 o GlobalLocalesData.get_sg; 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

215 
val cond_extern = NameSpace.cond_extern o #1 o GlobalLocalesData.get_sg; 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

216 

12063  217 
fun declare_locale name = 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

218 
GlobalLocalesData.map (fn (space, locs, regs) => 
15596  219 
(NameSpace.extend (space, [name]), locs, regs)); 
11896  220 

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

222 
GlobalLocalesData.map (fn (space, locs, regs) => 
15596  223 
(space, Symtab.update ((name, loc), locs), regs)); 
224 

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

225 
fun get_locale thy name = Symtab.lookup (#2 (GlobalLocalesData.get thy), name); 
11896  226 

12014  227 
fun the_locale thy name = 
228 
(case get_locale thy name of 

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

11896  231 

12046  232 

15596  233 
(* access registrations *) 
234 

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

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

236 

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

237 
fun gen_get_registration get thy_ctxt (name, ps) = 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

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

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

240 
 SOME tab => Termlisttab.lookup (tab, ps); 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

241 

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

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

243 
gen_get_registration (#3 o GlobalLocalesData.get); 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

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

245 
gen_get_registration LocalLocalesData.get; 
15596  246 

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

247 
val test_global_registration = isSome oo get_global_registration; 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

248 
val test_local_registration = isSome oo get_local_registration; 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

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

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

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

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

253 
test_global_registration thy id orelse test_local_registration ctxt id 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

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

255 

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

256 

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

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

258 

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

259 
fun gen_put_registration map (name, ps) attn = 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

260 
map (fn regs => 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

261 
let 
15596  262 
val tab = getOpt (Symtab.lookup (regs, name), Termlisttab.empty); 
263 
in 

264 
Symtab.update ((name, Termlisttab.update_new ((ps, (attn, [])), tab)), 

265 
regs) 

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

266 
end handle Termlisttab.DUP _ => regs); 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

267 

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

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

269 
gen_put_registration (fn f => 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

270 
GlobalLocalesData.map (fn (space, locs, regs) => 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

271 
(space, locs, f regs))); 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

272 
val put_local_registration = gen_put_registration LocalLocalesData.map; 
15596  273 

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

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

275 
(* ignore registration if already present in theory *) 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

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

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

278 
in case get_global_registration thy id of 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

279 
NONE => put_local_registration id attn ctxt 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

280 
 SOME _ => ctxt 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

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

282 

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

283 

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

284 
(* add witness theorem to registration in theory or context, 
15596  285 
ignored if registration not present *) 
286 

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

287 
fun gen_add_witness map (name, ps) thm = 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

288 
map (fn regs => 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

289 
let 
15596  290 
val tab = valOf (Symtab.lookup (regs, name)); 
291 
val (x, thms) = valOf (Termlisttab.lookup (tab, ps)); 

292 
in 

293 
Symtab.update ((name, Termlisttab.update ((ps, (x, thm::thms)), tab)), 

294 
regs) 

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

295 
end handle Option => regs); 
15596  296 

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

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

298 
gen_add_witness (fn f => 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

299 
GlobalLocalesData.map (fn (space, locs, regs) => 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

300 
(space, locs, f regs))); 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

301 
val add_local_witness = gen_add_witness LocalLocalesData.map; 
15596  302 

303 

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

304 
(* import hierarchy 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

305 
implementation could be more efficient, eg. by maintaining a database 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

306 
of dependencies *) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

307 

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

308 
fun imports thy (upper, lower) = 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

310 
val sign = sign_of thy; 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

311 
fun imps (Locale name) low = (name = low) orelse 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

312 
(case get_locale thy name of 
15531  313 
NONE => false 
314 
 SOME {import, ...} => imps import low) 

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

315 
 imps (Rename (expr, _)) low = imps expr low 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

316 
 imps (Merge es) low = exists (fn e => imps e low) es; 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

318 
imps (Locale (intern sign upper)) (intern sign lower) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

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

320 

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

321 

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

322 
(* printing of registrations *) 
15596  323 

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

324 
fun gen_print_registrations get_regs get_sign msg loc thy_ctxt = 
15596  325 
let 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

326 
val sg = get_sign thy_ctxt; 
15596  327 
val loc_int = intern sg loc; 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

328 
val regs = get_regs thy_ctxt; 
15596  329 
val prt_term = Pretty.quote o Sign.pretty_term sg; 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

330 
fun prt_inst (ts, ((prfx, _), thms)) = 
15596  331 
Pretty.block [Pretty.str prfx, Pretty.str ":", Pretty.brk 1, 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

332 
Pretty.list "(" ")" (map prt_term ts)]; 
15596  333 
val loc_regs = Symtab.lookup (regs, loc_int); 
334 
in 

335 
(case loc_regs of 

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

336 
NONE => Pretty.str ("No interpretations in " ^ msg ^ ".") 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

337 
 SOME r => Pretty.big_list ("Interpretations in " ^ msg ^ ":") 
15596  338 
(map prt_inst (Termlisttab.dest r))) 
339 
> Pretty.writeln 

340 
end; 

341 

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

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

343 
gen_print_registrations (#3 o GlobalLocalesData.get) 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

344 
Theory.sign_of "theory"; 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

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

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

347 
ProofContext.sign_of "context"; 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

348 
fun print_local_registrations loc ctxt = 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

349 
(print_global_registrations loc (ProofContext.theory_of ctxt); 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

350 
print_local_registrations' loc ctxt); 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset

351 

15596  352 

12277  353 
(* diagnostics *) 
12273  354 

12277  355 
fun err_in_locale ctxt msg ids = 
356 
let 

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

357 
val sign = ProofContext.sign_of ctxt; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

358 
fun prt_id (name, parms) = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

359 
[Pretty.block (Pretty.breaks (map Pretty.str (cond_extern sign name :: parms)))]; 
15570  360 
val prt_ids = List.concat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids)); 
12502  361 
val err_msg = 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

365 
in raise ProofContext.CONTEXT (err_msg, ctxt) end; 

12063  366 

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

367 
(* Version for identifiers with axioms *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

368 

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

369 
fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids'); 
12277  370 

371 

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

372 
(** primitives **) 
12046  373 

12277  374 
(* renaming *) 
12263  375 

15570  376 
fun rename ren x = getOpt (assoc_string (ren, x), x); 
12263  377 

378 
fun rename_term ren (Free (x, T)) = Free (rename ren x, T) 

379 
 rename_term ren (t $ u) = rename_term ren t $ rename_term ren u 

380 
 rename_term ren (Abs (x, T, t)) = Abs (x, T, rename_term ren t) 

381 
 rename_term _ a = a; 

382 

383 
fun rename_thm ren th = 

384 
let 

385 
val {sign, hyps, prop, maxidx, ...} = Thm.rep_thm th; 

386 
val cert = Thm.cterm_of sign; 

15570  387 
val (xs, Ts) = Library.split_list (Library.foldl Term.add_frees ([], prop :: hyps)); 
12263  388 
val xs' = map (rename ren) xs; 
389 
fun cert_frees names = map (cert o Free) (names ~~ Ts); 

390 
fun cert_vars names = map (cert o Var o apfst (rpair (maxidx + 1))) (names ~~ Ts); 

391 
in 

392 
if xs = xs' then th 

393 
else 

394 
th 

395 
> Drule.implies_intr_list (map cert hyps) 

396 
> Drule.forall_intr_list (cert_frees xs) 

397 
> Drule.forall_elim_list (cert_vars xs) 

398 
> Thm.instantiate ([], cert_vars xs ~~ cert_frees xs') 

399 
> (fn th' => Drule.implies_elim_list th' (map (Thm.assume o cert o rename_term ren) hyps)) 

400 
end; 

401 

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

402 
fun rename_elem ren (Fixes fixes) = Fixes (fixes > map (fn (x, T, mx) => 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

403 
let val x' = rename ren x in 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

404 
if x = x' then (x, T, mx) 
15531  405 
else (x', T, if mx = NONE then mx else SOME Syntax.NoSyn) (*drop syntax*) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

406 
end)) 
12263  407 
 rename_elem ren (Assumes asms) = Assumes (map (apsnd (map (fn (t, (ps, qs)) => 
408 
(rename_term ren t, (map (rename_term ren) ps, map (rename_term ren) qs))))) asms) 

409 
 rename_elem ren (Defines defs) = Defines (map (apsnd (fn (t, ps) => 

410 
(rename_term ren t, map (rename_term ren) ps))) defs) 

12273  411 
 rename_elem ren (Notes facts) = Notes (map (apsnd (map (apfst (map (rename_thm ren))))) facts); 
12263  412 

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

413 
fun rename_facts prfx elem = 
12307  414 
let 
12323  415 
fun qualify (arg as ((name, atts), x)) = 
13394  416 
if prfx = "" orelse name = "" then arg 
13375  417 
else ((NameSpace.pack [prfx, name], atts), x); 
12307  418 
in 
419 
(case elem of 

420 
Fixes fixes => Fixes fixes 

421 
 Assumes asms => Assumes (map qualify asms) 

422 
 Defines defs => Defines (map qualify defs) 

423 
 Notes facts => Notes (map qualify facts)) 

424 
end; 

425 

12263  426 

12502  427 
(* type instantiation *) 
428 

429 
fun inst_type [] T = T 

15570  430 
 inst_type env T = Term.map_type_tfree (fn v => getOpt (assoc (env, v), TFree v)) T; 
12502  431 

432 
fun inst_term [] t = t 

433 
 inst_term env t = Term.map_term_types (inst_type env) t; 

434 

13211
aabdb4b33625
BUG FIX in inst_thm: use current context instead of that of thm!!!
wenzelm
parents:
12958
diff
changeset

435 
fun inst_thm _ [] th = th 
aabdb4b33625
BUG FIX in inst_thm: use current context instead of that of thm!!!
wenzelm
parents:
12958
diff
changeset

436 
 inst_thm ctxt env th = 
12502  437 
let 
13211
aabdb4b33625
BUG FIX in inst_thm: use current context instead of that of thm!!!
wenzelm
parents:
12958
diff
changeset

438 
val sign = ProofContext.sign_of ctxt; 
12575  439 
val cert = Thm.cterm_of sign; 
440 
val certT = Thm.ctyp_of sign; 

13211
aabdb4b33625
BUG FIX in inst_thm: use current context instead of that of thm!!!
wenzelm
parents:
12958
diff
changeset

441 
val {hyps, prop, maxidx, ...} = Thm.rep_thm th; 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

442 
val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps); 
15570  443 
val env' = List.filter (fn ((a, _), _) => a mem_string tfrees) env; 
12502  444 
in 
445 
if null env' then th 

446 
else 

447 
th 

448 
> Drule.implies_intr_list (map cert hyps) 

12575  449 
> Drule.tvars_intr_list (map (#1 o #1) env') 
12502  450 
> (fn (th', al) => th' > 
15570  451 
Thm.instantiate ((map (fn ((a, _), T) => (valOf (assoc (al, a)), certT T)) env'), [])) 
12502  452 
> (fn th'' => Drule.implies_elim_list th'' 
453 
(map (Thm.assume o cert o inst_term env') hyps)) 

454 
end; 

455 

13211
aabdb4b33625
BUG FIX in inst_thm: use current context instead of that of thm!!!
wenzelm
parents:
12958
diff
changeset

456 
fun inst_elem _ env (Fixes fixes) = 
15570  457 
Fixes (map (fn (x, T, mx) => (x, Option.map (inst_type env) T, mx)) fixes) 
13211
aabdb4b33625
BUG FIX in inst_thm: use current context instead of that of thm!!!
wenzelm
parents:
12958
diff
changeset

458 
 inst_elem _ env (Assumes asms) = Assumes (map (apsnd (map (fn (t, (ps, qs)) => 
12502  459 
(inst_term env t, (map (inst_term env) ps, map (inst_term env) qs))))) asms) 
13211
aabdb4b33625
BUG FIX in inst_thm: use current context instead of that of thm!!!
wenzelm
parents:
12958
diff
changeset

460 
 inst_elem _ env (Defines defs) = Defines (map (apsnd (fn (t, ps) => 
12502  461 
(inst_term env t, map (inst_term env) ps))) defs) 
13211
aabdb4b33625
BUG FIX in inst_thm: use current context instead of that of thm!!!
wenzelm
parents:
12958
diff
changeset

462 
 inst_elem ctxt env (Notes facts) = 
aabdb4b33625
BUG FIX in inst_thm: use current context instead of that of thm!!!
wenzelm
parents:
12958
diff
changeset

463 
Notes (map (apsnd (map (apfst (map (inst_thm ctxt env))))) facts); 
12502  464 

465 

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

466 

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

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

468 

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

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

470 

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

471 
(* CB: frozen_tvars has the following type: 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

472 
ProofContext.context > Term.typ list > (Term.indexname * Term.typ) list *) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

473 

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

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

475 
let 
15570  476 
val tvars = rev (Library.foldl Term.add_tvarsT ([], Ts)); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

477 
val tfrees = map TFree 
14695  478 
(Term.invent_names (ProofContext.used_types ctxt) "'a" (length tvars) ~~ map #2 tvars); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

479 
in map #1 tvars ~~ tfrees end; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

480 

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

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

482 
let 
15531  483 
fun paramify (i, NONE) = (i, NONE) 
484 
 paramify (i, SOME T) = apsnd SOME (TypeInfer.paramify_dummies (i, T)); 

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

485 

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

486 
val (maxidx', Ts') = foldl_map paramify (maxidx, Ts); 
12727  487 
val (maxidx'', Us') = foldl_map paramify (maxidx', Us); 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

488 
val tsig = Sign.tsig_of (ProofContext.sign_of ctxt); 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

489 

15531  490 
fun unify (env, (SOME T, SOME U)) = (Type.unify tsig env (U, T) 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

491 
handle Type.TUNIFY => 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

492 
raise TYPE ("unify_frozen: failed to unify types", [U, T], [])) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

493 
 unify (env, _) = env; 
15570  494 
val (unifier, _) = Library.foldl unify ((Vartab.empty, maxidx''), Ts' ~~ Us'); 
495 
val Vs = map (Option.map (Envir.norm_type unifier)) Us'; 

496 
val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (List.mapPartial I Vs)); 

497 
in map (Option.map (Envir.norm_type unifier')) Vs end; 

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

498 

15570  499 
fun params_of elemss = gen_distinct eq_fst (List.concat (map (snd o fst) elemss)); 
500 
fun params_of' elemss = gen_distinct eq_fst (List.concat (map (snd o fst o fst) elemss)); 

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

501 

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

502 
(* CB: param_types has the following type: 
15531  503 
('a * 'b option) list > ('a * 'b) list *) 
15570  504 
fun param_types ps = List.mapPartial (fn (_, NONE) => NONE  (x, SOME T) => SOME (x, T)) ps; 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

505 

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

506 

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

507 
(* flatten expressions *) 
11896  508 

12510  509 
local 
12502  510 

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

511 
(* CB: OUTDATED unique_parms has the following type: 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

513 
(('b * (('c * 'd) list * Symtab.key list)) * 'e) list > 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

514 
(('b * ('c * 'd) list) * 'e) list *) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

515 

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

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

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

518 
val param_decls = 
15570  519 
List.concat (map (fn (((name, (ps, qs)), _), _) => map (rpair (name, ps)) qs) elemss) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

520 
> Symtab.make_multi > Symtab.dest; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

522 
(case find_first (fn (_, ids) => length ids > 1) param_decls of 
15531  523 
SOME (q, ids) => err_in_locale ctxt ("Multiple declaration of parameter " ^ quote q) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

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

527 

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

528 
(* CB: unify_parms has the following type: 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

529 
ProofContext.context > 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

530 
(string * Term.typ) list > 
15531  531 
(string * Term.typ option) list list > 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

532 
((string * Term.sort) * Term.typ) list list *) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

533 

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

534 
fun unify_parms ctxt fixed_parms raw_parmss = 
12502  535 
let 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

536 
val sign = ProofContext.sign_of ctxt; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

537 
val tsig = Sign.tsig_of sign; 
12502  538 
val maxidx = length raw_parmss; 
539 
val idx_parmss = (0 upto maxidx  1) ~~ raw_parmss; 

540 

541 
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

542 
fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps); 
15570  543 
val parms = fixed_parms @ List.concat (map varify_parms idx_parmss); 
12502  544 

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

545 
fun unify T ((env, maxidx), U) = 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

546 
Type.unify tsig (env, maxidx) (U, T) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

547 
handle Type.TUNIFY => 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

548 
let val prt = Sign.string_of_typ sign 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

549 
in raise TYPE ("unify_parms: failed to unify types " ^ 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

550 
prt U ^ " and " ^ prt T, [U, T], []) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

551 
end 
15570  552 
fun unify_list (envir, T :: Us) = Library.foldl (unify T) (envir, Us) 
12502  553 
 unify_list (envir, []) = envir; 
15570  554 
val (unifier, _) = Library.foldl unify_list 
12502  555 
((Vartab.empty, maxidx), map #2 (Symtab.dest (Symtab.make_multi parms))); 
556 

557 
val parms' = map (apsnd (Envir.norm_type unifier)) (gen_distinct eq_fst parms); 

558 
val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms')); 

559 

560 
fun inst_parms (i, ps) = 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

561 
foldr Term.add_typ_tfrees [] (List.mapPartial snd ps) 
15570  562 
> List.mapPartial (fn (a, S) => 
12502  563 
let val T = Envir.norm_type unifier' (TVar ((a, i), S)) 
15531  564 
in if T = TFree (a, S) then NONE else SOME ((a, S), T) end) 
12502  565 
in map inst_parms idx_parmss end; 
566 

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

567 
in 
12502  568 

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

569 
(* like unify_elemss, but does not touch axioms *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

570 

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

571 
fun unify_elemss' _ _ [] = [] 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

572 
 unify_elemss' _ [] [elems] = [elems] 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

573 
 unify_elemss' ctxt fixed_parms elemss = 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

575 
val envs = unify_parms ctxt fixed_parms (map (#2 o #1 o #1) elemss); 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

576 
fun inst ((((name, ps), axs), elems), env) = 
15570  577 
(((name, map (apsnd (Option.map (inst_type env))) ps), axs), 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

578 
map (inst_elem ctxt env) elems); 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

579 
in map inst (elemss ~~ envs) end; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

580 

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

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

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

583 
 unify_elemss ctxt fixed_parms elemss = 
12502  584 
let 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

585 
val envs = unify_parms ctxt fixed_parms (map (#2 o #1 o #1) elemss); 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

586 
fun inst ((((name, ps), axs), elems), env) = 
15570  587 
(((name, map (apsnd (Option.map (inst_type env))) ps), 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

588 
map (inst_thm ctxt env) axs), map (inst_elem ctxt env) elems); 
12839  589 
in map inst (elemss ~~ envs) end; 
12502  590 

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

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

594 
identifier). 

595 

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

597 
((name, ps), (ax_ps, axs)) 

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

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

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

601 
hence axioms may contain additional parameters from later fragments: 

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

603 

604 
Elements are enriched by identifierlike information: 

605 
(((name, ax_ps), axs), elems) 

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

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

608 
typeinstantiated. 

609 

610 
*) 

611 

12575  612 
fun flatten_expr ctxt (prev_idents, expr) = 
12014  613 
let 
614 
val thy = ProofContext.theory_of ctxt; 

15596  615 
(* thy used for retrieval of locale info, 
616 
ctxt for error messages, parameter unification and instantiation 

617 
of axioms *) 

618 
(* TODO: consider err_in_locale with thy argument *) 

12263  619 

15531  620 
fun renaming (SOME x :: xs) (y :: ys) = (y, x) :: renaming xs ys 
621 
 renaming (NONE :: xs) (y :: ys) = renaming xs ys 

12273  622 
 renaming [] _ = [] 
12289  623 
 renaming xs [] = raise ERROR_MESSAGE ("Too many arguments in renaming: " ^ 
15531  624 
commas (map (fn NONE => "_"  SOME x => quote x) xs)); 
12289  625 

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

626 
fun rename_parms top ren ((name, ps), (parms, axs)) = 
12289  627 
let val ps' = map (rename ren) ps in 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

628 
(case duplicates ps' of [] => ((name, ps'), 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

629 
if top then (map (rename ren) parms, map (rename_thm ren) axs) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

630 
else (parms, axs)) 
12289  631 
 dups => err_in_locale ctxt ("Duplicate parameters: " ^ commas_quote dups) [(name, ps')]) 
632 
end; 

12263  633 

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

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

636 
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

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

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

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

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

642 
the_locale thy name; 
12289  643 
val ps = map #1 (#1 params); 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

645 
(* acyclic import dependencies *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

646 
val ids'' = ids' @ [((name, ps), ([], []))]; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

647 
val ids_ax = if top then snd 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

648 
(foldl_map (fn (axs, ((name, parms), _)) => let 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

649 
val {elems, ...} = the_locale thy name; 
15570  650 
val ts = List.concat (List.mapPartial (fn (Assumes asms, _) => 
651 
SOME (List.concat (map (map #1 o #2) asms))  _ => NONE) elems); 

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

652 
val (axs1, axs2) = splitAt (length ts, axs); 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

653 
in (axs2, ((name, parms), (ps, axs1))) end) (axioms, ids'')) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

654 
else ids''; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

656 
 identify top (Rename (e, xs)) = 
12273  657 
let 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

658 
val (ids', parms') = identify top e; 
12839  659 
val ren = renaming xs parms' 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

660 
handle ERROR_MESSAGE msg => err_in_locale' ctxt msg ids'; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

661 
val ids'' = gen_distinct eq_fst (map (rename_parms top ren) ids'); 
15570  662 
val parms'' = distinct (List.concat (map (#2 o #1) ids'')); 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

664 
 identify top (Merge es) = 
15570  665 
Library.foldl (fn ((ids, parms), e) => let 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

666 
val (ids', parms') = identify top e 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

667 
in (gen_merge_lists eq_fst ids ids', 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

668 
merge_lists parms parms') end) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

669 
(([], []), es); 
12014  670 

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

671 
(* CB: enrich identifiers by parameter types and 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

672 
the corresponding elements (with renamed parameters) *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

673 

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

674 
fun eval ((name, xs), axs) = 
12273  675 
let 
13308  676 
val {params = (ps, qs), elems, ...} = the_locale thy name; 
12307  677 
val ren = filter_out (op =) (map #1 ps ~~ xs); 
13308  678 
val (params', elems') = 
679 
if null ren then ((ps, qs), map #1 elems) 

12502  680 
else ((map (apfst (rename ren)) ps, map (rename ren) qs), 
13308  681 
map (rename_elem ren o #1) elems); 
13375  682 
val elems'' = map (rename_facts (space_implode "_" xs)) elems'; 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

683 
in (((name, params'), axs), elems'') end; 
12307  684 

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

685 
(* compute identifiers, merge with previous ones *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

686 
val idents = gen_rems eq_fst (#1 (identify true expr), prev_idents); 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

687 
(* add types to params, check for unique params and unify them *) 
12575  688 
val raw_elemss = unique_parms ctxt (map eval idents); 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

689 
val elemss = unify_elemss' ctxt [] raw_elemss; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

690 
(* replace params in ids by params from axioms, 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

691 
adjust types in axioms *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

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

694 
val elemss' = map (fn (((name, _), (ps, axs)), elems) => 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

695 
(((name, map (fn p => (p, assoc (all_params, p))) ps), axs), elems)) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

697 
fun inst_ax th = let 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

700 
val [env] = unify_parms ctxt all_params [ps]; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

701 
val th' = inst_thm ctxt env th; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

702 
in th' end; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

703 
val final_elemss = map (fn ((id, axs), elems) => 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

704 
((id, map inst_ax axs), elems)) elemss'; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

705 
in (prev_idents @ idents, final_elemss) end; 
12046  706 

12510  707 
end; 
708 

12070  709 

15596  710 
(* attributes *) 
711 

712 
local 

713 

714 
fun read_att attrib (x, srcs) = (x, map attrib srcs) 

715 

716 
(* CB: Map attrib over 

717 
* A context element: add attrib to attribute lists of assumptions, 

718 
definitions and facts (on both sides for facts). 

719 
* Locale expression: no effect. *) 

720 

721 
fun gen_map_attrib_elem _ (Fixes fixes) = Fixes fixes 

722 
 gen_map_attrib_elem attrib (Assumes asms) = Assumes (map (apfst (read_att attrib)) asms) 

723 
 gen_map_attrib_elem attrib (Defines defs) = Defines (map (apfst (read_att attrib)) defs) 

724 
 gen_map_attrib_elem attrib (Notes facts) = 

725 
Notes (map (apfst (read_att attrib) o apsnd (map (read_att attrib))) facts) 

726 

727 
fun gen_map_attrib_elem_expr attrib (Elem elem) = Elem (gen_map_attrib_elem attrib elem) 

728 
 gen_map_attrib_elem_expr _ (Expr expr) = Expr expr; 

729 

730 
in 

731 

732 
val map_attrib_element = gen_map_attrib_elem; 

733 
val map_attrib_element_i = gen_map_attrib_elem; 

734 
val map_attrib_elem_or_expr = gen_map_attrib_elem_expr; 

735 
val map_attrib_elem_or_expr_i = gen_map_attrib_elem_expr; 

736 

737 
end; 

738 

739 

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

740 
(* activate elements *) 
12273  741 

12510  742 
local 
743 

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

744 
fun export_axioms axs _ hyps th = 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

745 
th > Drule.satisfy_hyps axs 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

746 
(* CB: replace metahyps, using axs, by a single metahyp. *) 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

747 
> Drule.implies_intr_list (Library.drop (length axs, hyps)) 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

748 
(* CB: turn remaining hyps into assumptions. *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

749 
> Seq.single 
12263  750 

14643  751 
fun activate_elem _ ((ctxt, axs), Fixes fixes) = 
752 
((ctxt > ProofContext.add_fixes fixes, axs), []) 

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

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

754 
let 
15596  755 
(* extract context attributes *) 
756 
val (Assumes asms) = map_attrib_element_i snd (Assumes asms); 

15570  757 
val ts = List.concat (map (map #1 o #2) asms); 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

758 
val (ps,qs) = splitAt (length ts, axs); 
13420  759 
val (ctxt', _) = 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

760 
ctxt > ProofContext.fix_frees ts 
13629  761 
> ProofContext.assume_i (export_axioms ps) asms; 
762 
in ((ctxt', qs), []) end 

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

763 
 activate_elem _ ((ctxt, axs), Defines defs) = 
15596  764 
let 
765 
(* extract context attributes *) 

766 
val (Defines defs) = map_attrib_element_i snd (Defines defs); 

767 
val (ctxt', _) = 

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

768 
ctxt > ProofContext.assume_i ProofContext.export_def 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

769 
(defs > map (fn ((name, atts), (t, ps)) => 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

770 
let val (c, t') = ProofContext.cert_def ctxt t 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

771 
in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end)) 
13420  772 
in ((ctxt', axs), []) end 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

773 
 activate_elem is_ext ((ctxt, axs), Notes facts) = 
15596  774 
let 
775 
(* extract context attributes *) 

776 
val (Notes facts) = map_attrib_element_i snd (Notes facts); 

777 
val (ctxt', res) = ctxt > ProofContext.note_thmss_i facts 

13420  778 
in ((ctxt', axs), if is_ext then res else []) end; 
12502  779 

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

780 
fun activate_elems (((name, ps), axs), elems) ctxt = 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

781 
let val ((ctxt', _), res) = 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

782 
foldl_map (activate_elem (name = "")) ((ProofContext.qualified true ctxt, axs), elems) 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

783 
handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)] 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

784 
in (ProofContext.restore_qualified ctxt ctxt', res) end; 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

785 

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

786 
fun activate_elemss prep_facts = foldl_map (fn (ctxt, (((name, ps), axs), raw_elems)) => 
12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

787 
let 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

788 
val elems = map (prep_facts ctxt) raw_elems; 
15570  789 
val (ctxt', res) = apsnd List.concat (activate_elems (((name, ps), axs), elems) ctxt); 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

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

791 

12546  792 
in 
793 

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

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

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

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

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

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

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

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

801 
from elemss and the intermediate context with prep_facts. 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

802 
If get_facts or get_facts_i is used for prep_facts, these also remove 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

804 

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

805 
fun activate_facts prep_facts arg = 
15570  806 
apsnd (apsnd List.concat o Library.split_list) (activate_elemss prep_facts arg); 
12546  807 

12510  808 
end; 
809 

12307  810 

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

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

812 

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

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

814 

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

815 
fun intern_expr sg (Locale xname) = Locale (intern sg xname) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

816 
 intern_expr sg (Merge exprs) = Merge (map (intern_expr sg) exprs) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

817 
 intern_expr sg (Rename (expr, xs)) = Rename (intern_expr sg expr, xs); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

818 

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

819 

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

820 
(* parameters *) 
12502  821 

822 
local 

823 

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

824 
fun prep_fixes prep_vars ctxt fixes = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

825 
let val vars = snd (foldl_map prep_vars (ctxt, map (fn (x, T, _) => ([x], T)) fixes)) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

826 
in map (fn (([x'], T'), (_, _, mx)) => (x', T', mx)) (vars ~~ fixes) end; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

827 

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

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

829 

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

830 
fun read_fixes x = prep_fixes ProofContext.read_vars x; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

831 
fun cert_fixes x = prep_fixes ProofContext.cert_vars x; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

832 

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

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

834 

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

835 

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

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

837 

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

838 
(* CB: an internal (Int) locale element was either imported or included, 
15104  839 
an external (Ext) element appears directly in the locale. *) 
840 

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

841 
datatype ('a, 'b) int_ext = Int of 'a  Ext of 'b; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

842 

15596  843 
(* flatten (ids, expr) normalises expr (which is either a locale 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

845 
to the list ids of already accumulated identifiers. 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

847 
with identifiers generated for expr, and elemss is the list of 
15596  848 
context elements generated from expr. For details, see flatten_expr. 
849 
Additionally, for a locale expression, the elems are grouped into a single 

850 
Int; individual context elements are marked Ext. In this case, the 

851 
identifierlike information of the element is as follows: 

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

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

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

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

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

857 

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

858 
fun flatten _ (ids, Elem (Fixes fixes)) = 
15531  859 
(ids, [((("", map (rpair NONE o #1) fixes), []), Ext (Fixes fixes))]) 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

860 
 flatten _ (ids, Elem elem) = (ids, [((("", []), []), Ext elem)]) 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

861 
 flatten (ctxt, prep_expr) (ids, Expr expr) = 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

863 

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

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

865 

12839  866 
local 
867 

12727  868 
fun declare_int_elem (ctxt, Fixes fixes) = 
12575  869 
(ctxt > ProofContext.add_fixes (map (fn (x, T, mx) => 
15570  870 
(x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes), []) 
12727  871 
 declare_int_elem (ctxt, _) = (ctxt, []); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

872 

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

873 
fun declare_ext_elem prep_fixes (ctxt, Fixes fixes) = 
12575  874 
(ctxt > ProofContext.add_fixes (prep_fixes ctxt fixes), []) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

875 
 declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

876 
 declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

878 

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

879 
fun declare_elems prep_fixes (ctxt, (((name, ps), _), elems)) = 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

880 
let val (ctxt', propps) = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

881 
(case elems of 
13308  882 
Int es => foldl_map declare_int_elem (ctxt, es) 
12546  883 
 Ext e => foldl_map (declare_ext_elem prep_fixes) (ctxt, [e])) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

884 
handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)] 
12727  885 
in (ctxt', propps) end; 
886 

12839  887 
in 
888 

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

889 
(* CB: only called by prep_elemss. *) 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

890 

12727  891 
fun declare_elemss prep_fixes fixed_params raw_elemss ctxt = 
892 
let 

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

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

894 
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

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

896 
val ctxt_with_fixed = 
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

897 
ProofContext.declare_terms (map Free fixed_params) ctxt; 
12727  898 
val int_elemss = 
899 
raw_elemss 

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

901 
> unify_elemss ctxt_with_fixed fixed_params; 
12727  902 
val (_, raw_elemss') = 
903 
foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es))  x => x) 

904 
(int_elemss, raw_elemss); 

905 
in foldl_map (declare_elems prep_fixes) (ctxt, raw_elemss') end; 

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

906 

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

908 

12839  909 
local 
910 

15596  911 
(* CB: normalise Assumes and Defines wrt. previous definitions *) 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

912 

12839  913 
val norm_term = Envir.beta_norm oo Term.subst_atomic; 
914 

15596  915 
(* CB: following code (abstract_term, abstract_thm, bind_def) 
916 
used in eval_text for Defines elements. *) 

917 

13336  918 
fun abstract_term eq = (*assumes wellformedness according to ProofContext.cert_def*) 
12839  919 
let 
920 
val body = Term.strip_all_body eq; 

921 
val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq)); 

922 
val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (vars, body)); 

923 
val (f, xs) = Term.strip_comb lhs; 

13336  924 
val eq' = Term.list_abs_free (map Term.dest_Free xs, rhs); 
925 
in (Term.dest_Free f, eq') end; 

926 

927 
fun abstract_thm sign eq = 

928 
Thm.assume (Thm.cterm_of sign eq) > Drule.gen_all > Drule.abs_def; 

12502  929 

13336  930 
fun bind_def ctxt (name, ps) ((xs, env, ths), eq) = 
12839  931 
let 
13336  932 
val ((y, T), b) = abstract_term eq; 
13308  933 
val b' = norm_term env b; 
13336  934 
val th = abstract_thm (ProofContext.sign_of ctxt) eq; 
13308  935 
fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)]; 
12839  936 
in 
13308  937 
conditional (exists (equal y o #1) xs) (fn () => 
938 
err "Attempt to define previously specified variable"); 

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

940 
err "Attempt to redefine variable"); 

13336  941 
(Term.add_frees (xs, b'), (Free (y, T), b') :: env, th :: ths) 
12839  942 
end; 
12575  943 

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

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

945 

13308  946 
fun eval_text _ _ _ (text, Fixes _) = text 
13394  947 
 eval_text _ _ is_ext ((((exts, exts'), (ints, ints')), (xs, env, defs)), Assumes asms) = 
948 
let 

15570  949 
val ts = List.concat (map (map #1 o #2) asms); 
13394  950 
val ts' = map (norm_term env) ts; 
951 
val spec' = 

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

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

15570  954 
in (spec', (Library.foldl Term.add_frees (xs, ts'), env, defs)) end 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

955 
 eval_text ctxt (id, _) _ ((spec, binds), Defines defs) = 
15570  956 
(spec, Library.foldl (bind_def ctxt id) (binds, map (#1 o #2) defs)) 
13308  957 
 eval_text _ _ _ (text, Notes _) = text; 
958 

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

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

960 

13308  961 
fun closeup _ false elem = elem 
962 
 closeup ctxt true elem = 

12839  963 
let 
13308  964 
fun close_frees t = 
965 
let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1) 

966 
(Term.add_frees ([], t))) 

967 
in Term.list_all_free (frees, t) end; 

968 

969 
fun no_binds [] = [] 

970 
 no_binds _ = 

971 
raise ProofContext.CONTEXT ("Illegal term bindings in locale element", ctxt); 

972 
in 

973 
(case elem of 

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

975 
(a, map (fn (t, (ps, qs)) => (close_frees t, (no_binds ps, no_binds qs))) propps))) 

976 
 Defines defs => Defines (defs > map (fn (a, (t, ps)) => 

977 
(a, (close_frees (#2 (ProofContext.cert_def ctxt t)), no_binds ps)))) 

978 
 e => e) 

979 
end; 

12839  980 

12502  981 

12839  982 
fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) => 
12727  983 
(x, assoc_string (parms, x), mx)) fixes) 
12839  984 
 finish_ext_elem _ close (Assumes asms, propp) = 
985 
close (Assumes (map #1 asms ~~ propp)) 

986 
 finish_ext_elem _ close (Defines defs, propp) = 

12727  987 
close (Defines (map #1 defs ~~ map (fn [(t, (ps, []))] => (t, ps)) propp)) 
12839  988 
 finish_ext_elem _ _ (Notes facts, _) = Notes facts; 
989 

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

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

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

993 

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

994 
fun finish_parms parms (((name, ps), axs), elems) = 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

995 
(((name, map (fn (x, _) => (x, assoc (parms, x))) ps), axs), elems); 
12839  996 

13375  997 
fun finish_elems ctxt parms _ (text, ((id, Int e), _)) = 
12839  998 
let 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

999 
val [(id', es)] = unify_elemss ctxt parms [(id, e)]; 
15570  1000 
val text' = Library.foldl (eval_text ctxt id' false) (text, es); 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1001 
in (text', (id', map Int es)) end 
13375  1002 
 finish_elems ctxt parms do_close (text, ((id, Ext e), [propp])) = 
13308  1003 
let 
1004 
val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp); 

13375  1005 
val text' = eval_text ctxt id true (text, e'); 
13308  1006 
in (text', (id, [Ext e'])) end; 
12839  1007 

1008 
in 

12510  1009 

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

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

1011 

13375  1012 
fun finish_elemss ctxt parms do_close = 
1013 
foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close); 

12839  1014 

1015 
end; 

1016 

15127  1017 
(* CB: type inference and consistency checks for locales *) 
1018 

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

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

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

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

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

1025 
(* CB: raw_elemss are list of pairs consisting of identifiers and 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

1028 
(* CB: raw_ctxt is context with additional fixed variables derived from 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

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

1031 
external elements in raw_elemss. *) 
15570  1032 
val raw_propps = map List.concat raw_proppss; 
1033 
val raw_propp = List.concat raw_propps; 

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

1034 

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

1035 
(* CB: add type information from fixed_params to context (declare_terms) *) 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1036 
(* CB: process patterns (conclusion and external elements only) *) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

1037 
val (ctxt, all_propp) = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

1038 
prepp (ProofContext.declare_terms (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp); 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1039 

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

1040 
(* CB: add type information from conclusion and external elements 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1041 
to context *) 
15570  1042 
val ctxt = ProofContext.declare_terms (List.concat (map (map fst) all_propp)) ctxt; 
12502  1043 

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

1044 
(* CB: resolve schematic variables (patterns) in conclusion and external 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1045 
elements. *) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

1046 
val all_propp' = map2 (op ~~) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

1047 
(#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp))), map (map snd) all_propp); 
13629  1048 
val (concl, propp) = splitAt(length raw_concl, all_propp'); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

1049 
val propps = unflat raw_propps propp; 
12839  1050 
val proppss = map (uncurry unflat) (raw_proppss ~~ propps); 
12502  1051 

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

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

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

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

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

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

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

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

1060 
(* CB: extract information from assumes and defines elements 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1061 
(fixes and notes in raw_elemss don't have an effect on text and elemss), 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1062 
compute final form of context elements. *) 
13394  1063 
val (text, elemss) = finish_elemss ctxt parms do_close 
1064 
(((([], []), ([], [])), ([], [], [])), raw_elemss ~~ proppss); 

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

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

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

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

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

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

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

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

1072 
xs: the free variables in exts' and ints' and rhss of definitions, 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

1074 
env: list of term pairs encoding substitutions, where the first term 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1075 
is a free variable; substitutions represent defines elements and 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1076 
the rhs is normalised wrt. the previous env 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1077 
defs: theorems representing the substitutions from defines elements 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1078 
(thms are normalised wrt. env). 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1079 
elemss is an updated version of raw_elemss: 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1080 
 type info added to Fixes 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1081 
 axiom and definition statement replaced by corresponding one 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1082 
from proppss in Assumes and Defines 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

1084 
*) 
13308  1085 
in ((parms, elemss, concl), text) end; 
12502  1086 

1087 
in 

1088 

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

1089 
fun read_elemss x = prep_elemss read_fixes ProofContext.read_propp_schematic x; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

1090 
fun cert_elemss x = prep_elemss cert_fixes ProofContext.cert_propp_schematic x; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

1091 

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

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

1093 

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

1094 

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

1095 
(* facts *) 
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 
local 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

1098 

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

1099 
fun prep_name ctxt (name, atts) = 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1100 
(* CB: reject qualified theorem names in locale declarations *) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

1101 
if NameSpace.is_qualified name then 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

1102 
raise ProofContext.CONTEXT ("Illegal qualified name: " ^ quote name, ctxt) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

1103 
else (name, atts); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

1104 

13375  1105 
fun prep_facts _ _ (Int elem) = elem 
1106 
 prep_facts _ _ (Ext (Fixes fixes)) = Fixes fixes 

1107 
 prep_facts _ ctxt (Ext (Assumes asms)) = Assumes (map (apfst (prep_name ctxt)) asms) 

1108 
 prep_facts _ ctxt (Ext (Defines defs)) = Defines (map (apfst (prep_name ctxt)) defs) 

1109 
 prep_facts get ctxt (Ext (Notes facts)) = Notes (facts > map (fn (a, bs) => 

1110 
(prep_name ctxt a, map (apfst (get ctxt)) bs))); 

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

1111 

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

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

1113 

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

1114 
fun get_facts x = prep_facts ProofContext.get_thms x; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

1115 
fun get_facts_i x = prep_facts (K I) x; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

1116 

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

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

1118 

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

1119 

12546  1120 
(* full context statements: import + elements + conclusion *) 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

1121 

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

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

1123 

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

1124 
fun prep_context_statement prep_expr prep_elemss prep_facts 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1125 
do_close fixed_params import elements raw_concl context = 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

1127 
val sign = ProofContext.sign_of context; 
13375  1128 

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

1129 
val (import_ids, raw_import_elemss) = flatten (context, prep_expr sign) ([], Expr import); 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

1130 
(* CB: normalise "includes" among elements *) 
15570  1131 
val raw_elemss = List.concat (#2 ((foldl_map (flatten (context, prep_expr sign)) 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1132 
(import_ids, elements)))); 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1133 
(* CB: raw_import_elemss @ raw_elemss is the normalised list of 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1134 
context elements obtained from import and elements. *) 
13375  1135 
val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close 
13336  1136 
context fixed_params (raw_import_elemss @ raw_elemss) raw_concl; 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1137 
(* CB: all_elemss and parms contain the correct parameter types *) 
13629  1138 
val (ps,qs) = splitAt(length raw_import_elemss, all_elemss) 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1139 
val (import_ctxt, (import_elemss, _)) = 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1140 
activate_facts prep_facts (context, ps); 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

1141 

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

1142 
val (ctxt, (elemss, _)) = 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1143 
activate_facts prep_facts (import_ctxt, qs); 
15212  1144 
val stmt = gen_distinct Term.aconv 
15570  1145 
(List.concat (map (fn ((_, axs), _) => 
1146 
List.concat (map (#hyps o Thm.rep_thm) axs)) qs)); 

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

1147 
val cstmt = map (cterm_of sign) stmt; 
12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

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

1149 
((((import_ctxt, import_elemss), (ctxt, elemss)), (parms, spec, defs)), (cstmt, concl)) 
12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

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

1151 

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

1152 
val gen_context = prep_context_statement intern_expr read_elemss get_facts; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

1153 
val gen_context_i = prep_context_statement (K I) cert_elemss get_facts_i; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

1154 

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

1155 
fun gen_statement prep_locale prep_ctxt raw_locale elems concl ctxt = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

1157 
val thy = ProofContext.theory_of ctxt; 
15570  1158 
val locale = Option.map (prep_locale (Theory.sign_of thy)) raw_locale; 
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1159 
val (target_stmt, fixed_params, import) = 
15531  1160 
(case locale of NONE => ([], [], empty) 
1161 
 SOME name => 

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

1162 
let val {predicate = (stmt, _), params = (ps, _), ...} = 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1163 
the_locale thy name 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1164 
in (stmt, param_types ps, Locale name) end); 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1165 
val ((((locale_ctxt, _), (elems_ctxt, _)), _), (elems_stmt, concl')) = 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1166 
prep_ctxt false fixed_params import elems concl ctxt; 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1167 
in (locale, (target_stmt, elems_stmt), locale_ctxt, elems_ctxt, concl') end; 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset

1168 

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

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

1170 

15127  1171 
(* CB: processing of locales for add_locale(_i) and print_locale *) 
1172 
(* CB: arguments are: x>import, y>body (elements), z>context *) 

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

1173 
fun read_context x y z = #1 (gen_context true [] x (map Elem y) [] z); 
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset

1174 
fun cert_context x y z = #1 (gen_context_i true [] x (map Elem y) [] z); 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset

1175 

15127  1176 
(* CB: processing of locales for note_thmss(_i), 
1177 
Proof.multi_theorem(_i) and antiquotations with option "locale" *) 

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

1178 
val read_context_statement = gen_statement intern gen_context; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

1179 
val cert_context_statement = gen_statement (K I) gen_context_i; 
12502  1180 

1181 
end; 

11896  1182 

1183 

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

1184 
(** CB: experimental instantiation mechanism **) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1185 

14528
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1186 
fun instantiate loc_name (prfx, attribs) raw_inst ctxt = 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

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

1188 
val thy = ProofContext.theory_of ctxt; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1189 
val sign = Theory.sign_of thy; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1190 
val tsig = Sign.tsig_of sign; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1191 
val cert = cterm_of sign; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1192 

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

1193 
(** process the locale **) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1194 

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

1195 
val {predicate = (_, axioms), params = (ps, _), ...} = 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1196 
the_locale thy (intern sign loc_name); 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1197 
val fixed_params = param_types ps; 
14528
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1198 
val init = ProofContext.init thy; 
15596  1199 
val (_, raw_elemss) = 
14528
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1200 
flatten (init, intern_expr sign) ([], Expr (Locale loc_name)); 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1201 
val ((parms, all_elemss, concl), 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1202 
(spec as (_, (ints, _)), (xs, env, defs))) = 
14528
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1203 
read_elemss false (* do_close *) init 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1204 
fixed_params (* could also put [] here??? *) raw_elemss 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1205 
[] (* concl *); 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1206 

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

1207 
(** analyse the instantiation theorem inst **) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1208 

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

1209 
val inst = case raw_inst of 
15531  1210 
NONE => if null ints 
1211 
then NONE 

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

1212 
else error "Locale has assumptions but no chained fact was found" 
15531  1213 
 SOME [] => if null ints 
1214 
then NONE 

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

1215 
else error "Locale has assumptions but no chained fact was found" 
15531  1216 
 SOME [thm] => if null ints 
1217 
then (warning "Locale has no assumptions: fact ignored"; NONE) 

1218 
else SOME thm 

1219 
 SOME _ => error "Multiple facts are not allowed"; 

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

1220 

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

1221 
val args = case inst of 
15531  1222 
NONE => [] 
1223 
 SOME thm => thm > prop_of > ObjectLogic.drop_judgment sign 

14528
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1224 
> Term.strip_comb 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1225 
>> (fn t as (Const (s, _)) => if (intern sign loc_name = s) 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1226 
then t 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1227 
else error ("Constant " ^ quote loc_name ^ 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1228 
" expected but constant " ^ quote s ^ " was found") 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1229 
 t => error ("Constant " ^ quote loc_name ^ " expected \ 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1230 
\but term " ^ quote (Sign.string_of_term sign t) ^ 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1231 
" was found")) 
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

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

1233 
val cargs = map cert args; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1234 

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

1235 
(* process parameters: match their types with those of arguments *) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1236 

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

1237 
val def_names = map (fn (Free (s, _), _) => s) env; 
15570  1238 
val (defined, assumed) = List.partition 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1239 
(fn (s, _) => s mem def_names) fixed_params; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1240 
val cassumed = map (cert o Free) assumed; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1241 
val cdefined = map (cert o Free) defined; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1242 

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

1243 
val param_types = map snd assumed; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1244 
val v_param_types = map Type.varifyT param_types; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1245 
val arg_types = map Term.fastype_of args; 
15570  1246 
val Tenv = Library.foldl (Type.typ_match tsig) 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1247 
(Vartab.empty, v_param_types ~~ arg_types) 
15570  1248 
handle UnequalLengths => error "Number of parameters does not \ 
14528
1457584110ac
Locale instantiation: label parameter optional, new attribute paramter.
ballarin
parents:
14508
diff
changeset

1249 
\match number of arguments of chained fact"; 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1250 
(* get their sorts *) 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

1251 
val tfrees = foldr Term.add_typ_tfrees [] param_types 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1252 
val Tenv' = map 
15570  1253 
(fn ((a, i), T) => ((a, valOf (assoc_string (tfrees, a))), T)) 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1254 
(Vartab.dest Tenv); 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1255 

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

1256 
(* process (internal) elements *) 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1257 

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

1258 
fun inst_type [] T = T 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset

1259 
 inst_type env T = 