author  wenzelm 
Wed, 10 Jul 2002 14:51:18 +0200  
changeset 13336  1bd21b082466 
parent 13308  1dbed9ea764b 
child 13375  7cbf2dea46d0 
permissions  rwrr 
12014  1 
(* Title: Pure/Isar/locale.ML 
11896  2 
ID: $Id$ 
12958  3 
Author: Markus Wenzel, LMU/TU München 
11896  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
5 

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

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

8 

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

9 
Draws some basic ideas from Florian Kammüller's original version of 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

10 
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

11 
metalogic. Furthermore, we provide structured import of contexts 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

12 
(with merge and rename operations), as well as typeinference of the 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

13 
signature parts. 
11896  14 
*) 
15 

16 
signature LOCALE = 

17 
sig 

12046  18 
type context 
19 
datatype ('typ, 'term, 'fact, 'att) elem = 

12058  20 
Fixes of (string * 'typ option * mixfix option) list  
12046  21 
Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list  
22 
Defines of ((string * 'att list) * ('term * 'term list)) list  

12273  23 
Notes of ((string * 'att list) * ('fact * 'att list) list) list 
24 
datatype expr = 

25 
Locale of string  

26 
Rename of expr * string option list  

27 
Merge of expr list 

28 
val empty: expr 

29 
datatype ('typ, 'term, 'fact, 'att) elem_expr = 

30 
Elem of ('typ, 'term, 'fact, 'att) elem  Expr of expr 

12046  31 
type 'att element 
32 
type 'att element_i 

33 
type locale 

34 
val intern: Sign.sg > xstring > string 

12014  35 
val cond_extern: Sign.sg > string > xstring 
12502  36 
val the_locale: theory > string > locale 
12273  37 
val attribute: ('att > context attribute) > ('typ, 'term, 'thm, 'att) elem_expr 
38 
> ('typ, 'term, 'thm, context attribute) elem_expr 

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

39 
val locale_facts: theory > xstring > thm list 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

40 
val locale_facts_i: theory > string > thm list 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

41 
val read_context_statement: xstring option > context attribute element list > 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

42 
(string * (string list * string list)) list list > context > 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

43 
string option * context * context * (term * (term list * term list)) list list 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

44 
val cert_context_statement: string option > context attribute element_i list > 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

45 
(term * (term list * term list)) list list > context > 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

46 
string option * context * context * (term * (term list * term list)) list list 
12758  47 
val print_locales: theory > unit 
48 
val print_locale: theory > expr > context attribute element list > unit 

12273  49 
val add_locale: bstring > expr > context attribute element list > theory > theory 
50 
val add_locale_i: bstring > expr > context attribute element_i list > theory > theory 

12958  51 
val smart_have_thmss: string > (string * 'a) Library.option > 
52 
((bstring * theory attribute list) * (thm list * theory attribute list) list) list > 

53 
theory > theory * (bstring * thm list) list 

12711  54 
val have_thmss: string > xstring > 
55 
((bstring * context attribute list) * (xstring * context attribute list) list) list > 

56 
theory > theory * (bstring * thm list) list 

57 
val have_thmss_i: string > string > 

58 
((bstring * context attribute list) * (thm list * context attribute list) list) list > 

59 
theory > theory * (bstring * thm list) list 

12958  60 
val add_thmss: string > ((string * thm list) * context attribute list) list > 
13336  61 
theory * context > (theory * context) * thm list list 
11896  62 
val setup: (theory > theory) list 
63 
end; 

12839  64 

12289  65 
structure Locale: LOCALE = 
11896  66 
struct 
67 

12273  68 
(** locale elements and expressions **) 
11896  69 

12014  70 
type context = ProofContext.context; 
11896  71 

12046  72 
datatype ('typ, 'term, 'fact, 'att) elem = 
12058  73 
Fixes of (string * 'typ option * mixfix option) list  
12046  74 
Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list  
75 
Defines of ((string * 'att list) * ('term * 'term list)) list  

12273  76 
Notes of ((string * 'att list) * ('fact * 'att list) list) list; 
77 

78 
datatype expr = 

79 
Locale of string  

80 
Rename of expr * string option list  

81 
Merge of expr list; 

11896  82 

12273  83 
val empty = Merge []; 
84 

85 
datatype ('typ, 'term, 'fact, 'att) elem_expr = 

86 
Elem of ('typ, 'term, 'fact, 'att) elem  Expr of expr; 

87 

88 
type 'att element = (string, string, string, 'att) elem_expr; 

89 
type 'att element_i = (typ, term, thm list, 'att) elem_expr; 

12070  90 

91 
type locale = 

12289  92 
{import: expr, (*dynamic import*) 
93 
elems: ((typ, term, thm list, context attribute) elem * stamp) list, (*static content*) 

12839  94 
params: (string * typ option) list * string list}; (*all vs. local params*) 
12063  95 

13308  96 
fun make_locale import elems params = 
97 
{import = import, elems = elems, params = params}: locale; 

12063  98 

11896  99 

100 

101 
(** theory data **) 

102 

103 
structure LocalesArgs = 

104 
struct 

12014  105 
val name = "Isar/locales"; 
12063  106 
type T = NameSpace.T * locale Symtab.table; 
11896  107 

12063  108 
val empty = (NameSpace.empty, Symtab.empty); 
109 
val copy = I; 

12118  110 
val prep_ext = I; 
12289  111 

112 
(*joining of locale elements: only facts may be added later!*) 

13308  113 
fun join ({import, elems, params}: locale, {elems = elems', ...}: locale) = 
114 
Some (make_locale import (gen_merge_lists eq_snd elems elems') params); 

12273  115 
fun merge ((space1, locs1), (space2, locs2)) = 
12289  116 
(NameSpace.merge (space1, space2), Symtab.join join (locs1, locs2)); 
117 

12273  118 
fun print _ (space, locs) = 
119 
Pretty.strs ("locales:" :: map (NameSpace.cond_extern space o #1) (Symtab.dest locs)) 

12014  120 
> Pretty.writeln; 
11896  121 
end; 
122 

123 
structure LocalesData = TheoryDataFun(LocalesArgs); 

124 
val print_locales = LocalesData.print; 

125 

12289  126 
val intern = NameSpace.intern o #1 o LocalesData.get_sg; 
127 
val cond_extern = NameSpace.cond_extern o #1 o LocalesData.get_sg; 

128 

12277  129 

130 
(* access locales *) 

131 

12063  132 
fun declare_locale name = 
133 
LocalesData.map (apfst (fn space => (NameSpace.extend (space, [name])))); 

11896  134 

12273  135 
fun put_locale name loc = LocalesData.map (apsnd (fn locs => Symtab.update ((name, loc), locs))); 
12063  136 
fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy), name); 
11896  137 

12014  138 
fun the_locale thy name = 
139 
(case get_locale thy name of 

140 
Some loc => loc 

141 
 None => error ("Unknown locale " ^ quote name)); 

11896  142 

12046  143 

12277  144 
(* diagnostics *) 
12273  145 

12277  146 
fun err_in_locale ctxt msg ids = 
147 
let 

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

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

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

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

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

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

12063  157 

12277  158 

159 

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

160 
(** primitives **) 
12046  161 

12277  162 
(* renaming *) 
12263  163 

164 
fun rename ren x = if_none (assoc_string (ren, x)) x; 

165 

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

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

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

169 
 rename_term _ a = a; 

170 

171 
fun rename_thm ren th = 

172 
let 

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

174 
val cert = Thm.cterm_of sign; 

12502  175 
val (xs, Ts) = Library.split_list (foldl Term.add_frees ([], prop :: hyps)); 
12263  176 
val xs' = map (rename ren) xs; 
177 
fun cert_frees names = map (cert o Free) (names ~~ Ts); 

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

179 
in 

180 
if xs = xs' then th 

181 
else 

182 
th 

183 
> Drule.implies_intr_list (map cert hyps) 

184 
> Drule.forall_intr_list (cert_frees xs) 

185 
> Drule.forall_elim_list (cert_vars xs) 

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

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

188 
end; 

189 

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

190 
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

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

192 
if x = x' then (x, T, mx) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

193 
else (x', T, if mx = None then mx else Some Syntax.NoSyn) (*drop syntax*) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

194 
end)) 
12263  195 
 rename_elem ren (Assumes asms) = Assumes (map (apsnd (map (fn (t, (ps, qs)) => 
196 
(rename_term ren t, (map (rename_term ren) ps, map (rename_term ren) qs))))) asms) 

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

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

12273  199 
 rename_elem ren (Notes facts) = Notes (map (apsnd (map (apfst (map (rename_thm ren))))) facts); 
12263  200 

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

201 
fun rename_facts prfx elem = 
12307  202 
let 
12323  203 
fun qualify (arg as ((name, atts), x)) = 
204 
if name = "" then arg 

205 
else ((NameSpace.pack (filter_out (equal "") (prfx @ [name])), atts), x); 

12307  206 
in 
207 
(case elem of 

208 
Fixes fixes => Fixes fixes 

209 
 Assumes asms => Assumes (map qualify asms) 

210 
 Defines defs => Defines (map qualify defs) 

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

212 
end; 

213 

12263  214 

12502  215 
(* type instantiation *) 
216 

217 
fun inst_type [] T = T 

218 
 inst_type env T = Term.map_type_tfree (fn v => if_none (assoc (env, v)) (TFree v)) T; 

219 

220 
fun inst_term [] t = t 

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

222 

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

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

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

226 
val sign = ProofContext.sign_of ctxt; 
12575  227 
val cert = Thm.cterm_of sign; 
228 
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

229 
val {hyps, prop, maxidx, ...} = Thm.rep_thm th; 
12579  230 
val tfrees = foldr Term.add_term_tfree_names (prop :: hyps, []); 
231 
val env' = filter (fn ((a, _), _) => a mem_string tfrees) env; 

12502  232 
in 
233 
if null env' then th 

234 
else 

235 
th 

236 
> Drule.implies_intr_list (map cert hyps) 

12575  237 
> Drule.tvars_intr_list (map (#1 o #1) env') 
12502  238 
> (fn (th', al) => th' > 
239 
Thm.instantiate ((map (fn ((a, _), T) => (the (assoc (al, a)), certT T)) env'), [])) 

240 
> (fn th'' => Drule.implies_elim_list th'' 

241 
(map (Thm.assume o cert o inst_term env') hyps)) 

242 
end; 

243 

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

244 
fun inst_elem _ env (Fixes fixes) = 
12502  245 
Fixes (map (fn (x, T, mx) => (x, apsome (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

246 
 inst_elem _ env (Assumes asms) = Assumes (map (apsnd (map (fn (t, (ps, qs)) => 
12502  247 
(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

248 
 inst_elem _ env (Defines defs) = Defines (map (apsnd (fn (t, ps) => 
12502  249 
(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

250 
 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

251 
Notes (map (apsnd (map (apfst (map (inst_thm ctxt env))))) facts); 
12502  252 

253 

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

254 

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

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

256 

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

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

258 

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

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

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

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

262 
val tfrees = map TFree 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

263 
(Term.invent_type_names (ProofContext.used_types ctxt) (length tvars) ~~ map #2 tvars); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

265 

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

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

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

268 
val tsig = Sign.tsig_of (ProofContext.sign_of ctxt); 
12546  269 
fun unify (env, (Some T, Some U)) = (Type.unify tsig env (U, T) 
270 
handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], [])) 

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

271 
 unify (env, _) = env; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

272 
fun paramify (i, None) = (i, None) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

273 
 paramify (i, Some T) = apsnd Some (Type.paramify_dummies (i, T)); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

274 

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

275 
val (maxidx', Ts') = foldl_map paramify (maxidx, Ts); 
12727  276 
val (maxidx'', Us') = foldl_map paramify (maxidx', Us); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

277 
val (unifier, _) = foldl unify ((Vartab.empty, maxidx''), Ts' ~~ Us'); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

278 
val Vs = map (apsome (Envir.norm_type unifier)) Us'; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

279 
val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (mapfilter I Vs)); 
12532  280 
in map (apsome (Envir.norm_type unifier')) Vs end; 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

281 

12730  282 
fun params_of elemss = gen_distinct eq_fst (flat (map (snd o fst) elemss)); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

283 
fun param_types ps = mapfilter (fn (_, None) => None  (x, Some T) => Some (x, T)) ps; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

284 

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

285 

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

286 
(* flatten expressions *) 
11896  287 

12510  288 
local 
12502  289 

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

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

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

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

293 
flat (map (fn ((name, (ps, qs)), _) => map (rpair (name, ps)) qs) elemss) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

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

296 
(case find_first (fn (_, ids) => length ids > 1) param_decls of 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

297 
Some (q, ids) => err_in_locale ctxt ("Multiple declaration of parameter " ^ quote q) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

298 
(map (apsnd (map fst)) ids) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

299 
 None => map (apfst (apsnd #1)) elemss) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

301 

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

302 
fun unify_parms ctxt fixed_parms raw_parmss = 
12502  303 
let 
304 
val tsig = Sign.tsig_of (ProofContext.sign_of ctxt); 

305 
val maxidx = length raw_parmss; 

306 
val idx_parmss = (0 upto maxidx  1) ~~ raw_parmss; 

307 

308 
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

309 
fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

310 
val parms = fixed_parms @ flat (map varify_parms idx_parmss); 
12502  311 

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

312 
fun unify T ((env, maxidx), U) = Type.unify tsig (env, maxidx) (U, T) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

313 
handle Type.TUNIFY => raise TYPE ("unify_parms: failed to unify types", [U, T], []); 
12502  314 
fun unify_list (envir, T :: Us) = foldl (unify T) (envir, Us) 
315 
 unify_list (envir, []) = envir; 

316 
val (unifier, _) = foldl unify_list 

317 
((Vartab.empty, maxidx), map #2 (Symtab.dest (Symtab.make_multi parms))); 

318 

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

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

321 

322 
fun inst_parms (i, ps) = 

323 
foldr Term.add_typ_tfrees (mapfilter snd ps, []) 

324 
> mapfilter (fn (a, S) => 

325 
let val T = Envir.norm_type unifier' (TVar ((a, i), S)) 

326 
in if T = TFree (a, S) then None else Some ((a, S), T) end); 

327 
in map inst_parms idx_parmss end; 

328 

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

329 
in 
12502  330 

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

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

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

333 
 unify_elemss ctxt fixed_parms elemss = 
12502  334 
let 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

335 
val envs = unify_parms ctxt fixed_parms (map (#2 o #1) elemss); 
13308  336 
fun inst (((name, ps), elems), env) = 
337 
((name, map (apsnd (apsome (inst_type env))) ps), (map (inst_elem ctxt env) elems)); 

12839  338 
in map inst (elemss ~~ envs) end; 
12502  339 

12575  340 
fun flatten_expr ctxt (prev_idents, expr) = 
12014  341 
let 
342 
val thy = ProofContext.theory_of ctxt; 

12263  343 

12289  344 
fun renaming (Some x :: xs) (y :: ys) = (y, x) :: renaming xs ys 
345 
 renaming (None :: xs) (y :: ys) = renaming xs ys 

12273  346 
 renaming [] _ = [] 
12289  347 
 renaming xs [] = raise ERROR_MESSAGE ("Too many arguments in renaming: " ^ 
348 
commas (map (fn None => "_"  Some x => quote x) xs)); 

349 

350 
fun rename_parms ren (name, ps) = 

351 
let val ps' = map (rename ren) ps in 

352 
(case duplicates ps' of [] => (name, ps') 

353 
 dups => err_in_locale ctxt ("Duplicate parameters: " ^ commas_quote dups) [(name, ps')]) 

354 
end; 

12263  355 

12273  356 
fun identify ((ids, parms), Locale name) = 
12289  357 
let 
358 
val {import, params, ...} = the_locale thy name; 

359 
val ps = map #1 (#1 params); 

360 
in 

12273  361 
if (name, ps) mem ids then (ids, parms) 
12277  362 
else 
12289  363 
let val (ids', parms') = identify ((ids, parms), import); (*acyclic dependencies!*) 
364 
in (ids' @ [(name, ps)], merge_lists parms' ps) end 

12273  365 
end 
366 
 identify ((ids, parms), Rename (e, xs)) = 

367 
let 

368 
val (ids', parms') = identify (([], []), e); 

12839  369 
val ren = renaming xs parms' 
370 
handle ERROR_MESSAGE msg => err_in_locale ctxt msg ids'; 

12289  371 
val ids'' = distinct (map (rename_parms ren) ids'); 
372 
val parms'' = distinct (flat (map #2 ids'')); 

373 
in (merge_lists ids ids'', merge_lists parms parms'') end 

12273  374 
 identify (arg, Merge es) = foldl identify (arg, es); 
12014  375 

12307  376 
fun eval (name, xs) = 
12273  377 
let 
13308  378 
val {params = (ps, qs), elems, ...} = the_locale thy name; 
12307  379 
val ren = filter_out (op =) (map #1 ps ~~ xs); 
13308  380 
val (params', elems') = 
381 
if null ren then ((ps, qs), map #1 elems) 

12502  382 
else ((map (apfst (rename ren)) ps, map (rename ren) qs), 
13308  383 
map (rename_elem ren o #1) elems); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

384 
val elems'' = map (rename_facts [NameSpace.base name, space_implode "_" xs]) elems'; 
13308  385 
in ((name, params'), elems'') end; 
12307  386 

12575  387 
val idents = gen_rems (op =) (#1 (identify (([], []), expr)), prev_idents); 
388 
val raw_elemss = unique_parms ctxt (map eval idents); 

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

389 
val elemss = unify_elemss ctxt [] raw_elemss; 
12575  390 
in (prev_idents @ idents, elemss) end; 
12046  391 

12510  392 
end; 
393 

12070  394 

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

395 
(* activate elements *) 
12273  396 

12510  397 
local 
398 

13297  399 
fun activate_elem (ctxt, Fixes fixes) = (ctxt > ProofContext.add_fixes fixes, []) 
12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

400 
 activate_elem (ctxt, Assumes asms) = 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

401 
ctxt > ProofContext.fix_frees (flat (map (map #1 o #2) asms)) 
12839  402 
> ProofContext.assume_i ProofContext.export_assume asms 
12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

403 
 activate_elem (ctxt, Defines defs) = 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

404 
ctxt > ProofContext.assume_i ProofContext.export_def 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

405 
(map (fn ((name, atts), (t, ps)) => 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

406 
let val (c, t') = ProofContext.cert_def ctxt t 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

407 
in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end) defs) 
13297  408 
 activate_elem (ctxt, Notes facts) = ctxt > ProofContext.have_thmss_i facts; 
12263  409 

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

410 
fun activate_elems ((name, ps), elems) = ProofContext.qualified_result (fn ctxt => 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

411 
foldl_map activate_elem (ctxt, elems) handle ProofContext.CONTEXT (msg, ctxt) => 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

412 
err_in_locale ctxt msg [(name, map fst ps)]); 
12502  413 

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

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

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

416 
val elems = map (prep_facts ctxt) raw_elems; 
13336  417 
val (ctxt', facts) = apsnd flat (activate_elems ((name, ps), map fst elems) ctxt); 
418 
in (ctxt', (((name, ps), elems), facts)) end); 

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

419 

12546  420 
in 
421 

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

422 
fun activate_facts prep_facts ctxt_elemss = 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

423 
let val (ctxt', (elemss', factss)) = apsnd split_list (activate_elemss prep_facts ctxt_elemss) 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

424 
in (ctxt', (elemss', flat factss)) end; 
12546  425 

12510  426 
end; 
427 

12307  428 

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

429 

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

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

431 

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

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

433 

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

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

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

436 
 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

437 

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

438 

12546  439 
(* attributes *) 
440 

441 
local fun read_att attrib (x, srcs) = (x, map attrib srcs) in 

442 

443 
fun attribute _ (Elem (Fixes fixes)) = Elem (Fixes fixes) 

444 
 attribute attrib (Elem (Assumes asms)) = Elem (Assumes (map (apfst (read_att attrib)) asms)) 

445 
 attribute attrib (Elem (Defines defs)) = Elem (Defines (map (apfst (read_att attrib)) defs)) 

446 
 attribute attrib (Elem (Notes facts)) = 

447 
Elem (Notes (map (apfst (read_att attrib) o apsnd (map (read_att attrib))) facts)) 

448 
 attribute _ (Expr expr) = Expr expr; 

449 

450 
end; 

451 

452 

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

453 
(* parameters *) 
12502  454 

455 
local 

456 

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

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

458 
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

459 
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

460 

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

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

462 

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

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

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

465 

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

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

467 

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

470 

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

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

472 

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

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

474 

12839  475 
local 
476 

12727  477 
fun declare_int_elem (ctxt, Fixes fixes) = 
12575  478 
(ctxt > ProofContext.add_fixes (map (fn (x, T, mx) => 
12727  479 
(x, apsome (Term.map_type_tfree (Type.param 0)) T, mx)) fixes), []) 
480 
 declare_int_elem (ctxt, _) = (ctxt, []); 

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

481 

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

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

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

485 
 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

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

487 

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

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

490 
(case elems of 
13308  491 
Int es => foldl_map declare_int_elem (ctxt, es) 
12546  492 
 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

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

12839  496 
in 
497 

12727  498 
fun declare_elemss prep_fixes fixed_params raw_elemss ctxt = 
499 
let 

500 
val int_elemss = 

501 
raw_elemss 

502 
> mapfilter (fn (id, Int es) => Some (id, es)  _ => None) 

503 
> unify_elemss ctxt fixed_params; 

504 
val (_, raw_elemss') = 

505 
foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es))  x => x) 

506 
(int_elemss, raw_elemss); 

507 
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

508 

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

510 

12839  511 
local 
512 

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

514 

13336  515 
fun abstract_term eq = (*assumes wellformedness according to ProofContext.cert_def*) 
12839  516 
let 
517 
val body = Term.strip_all_body eq; 

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

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

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

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

523 

524 
fun abstract_thm sign eq = 

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

12502  526 

13336  527 
fun bind_def ctxt (name, ps) ((xs, env, ths), eq) = 
12839  528 
let 
13336  529 
val ((y, T), b) = abstract_term eq; 
13308  530 
val b' = norm_term env b; 
13336  531 
val th = abstract_thm (ProofContext.sign_of ctxt) eq; 
13308  532 
fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)]; 
12839  533 
in 
13308  534 
conditional (exists (equal y o #1) xs) (fn () => 
535 
err "Attempt to define previously specified variable"); 

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

537 
err "Attempt to redefine variable"); 

13336  538 
(Term.add_frees (xs, b'), (Free (y, T), b') :: env, th :: ths) 
12839  539 
end; 
12575  540 

13308  541 
fun eval_text _ _ _ (text, Fixes _) = text 
13336  542 
 eval_text _ _ do_text ((spec, (xs, env, defs)), Assumes asms) = 
13308  543 
let 
544 
val ts = map (norm_term env) (flat (map (map #1 o #2) asms)); 

545 
val spec' = if do_text then spec @ ts else spec; 

546 
val xs' = foldl Term.add_frees (xs, ts); 

13336  547 
in (spec', (xs', env, defs)) end 
13308  548 
 eval_text ctxt id _ ((spec, binds), Defines defs) = 
549 
(spec, foldl (bind_def ctxt id) (binds, map (#1 o #2) defs)) 

550 
 eval_text _ _ _ (text, Notes _) = text; 

551 

552 
fun closeup _ false elem = elem 

553 
 closeup ctxt true elem = 

12839  554 
let 
13308  555 
fun close_frees t = 
556 
let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1) 

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

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

559 

560 
fun no_binds [] = [] 

561 
 no_binds _ = 

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

563 
in 

564 
(case elem of 

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

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

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

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

569 
 e => e) 

570 
end; 

12839  571 

12502  572 

12839  573 
fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) => 
12727  574 
(x, assoc_string (parms, x), mx)) fixes) 
12839  575 
 finish_ext_elem _ close (Assumes asms, propp) = 
576 
close (Assumes (map #1 asms ~~ propp)) 

577 
 finish_ext_elem _ close (Defines defs, propp) = 

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

581 
fun finish_parms parms ((name, ps), elems) = 

582 
((name, map (fn (x, _) => (x, assoc (parms, x))) ps), elems); 

583 

13308  584 
fun finish_elems ctxt parms _ _ (text, ((id, Int e), _)) = 
12839  585 
let 
13308  586 
val [(_, es)] = unify_elemss ctxt parms [(id, e)]; 
587 
val text' = foldl (eval_text ctxt id false) (text, es); 

588 
in (text', (id, map Int es)) end 

589 
 finish_elems ctxt parms do_close do_text (text, ((id, Ext e), [propp])) = 

590 
let 

591 
val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp); 

592 
val text' = eval_text ctxt id do_text (text, e'); 

593 
in (text', (id, [Ext e'])) end; 

12839  594 

595 
in 

12510  596 

13308  597 
fun finish_elemss ctxt parms do_close do_text = 
598 
foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close do_text); 

12839  599 

600 
end; 

601 

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

603 
let 
12727  604 
val (raw_ctxt, raw_proppss) = declare_elemss prep_fixes fixed_params raw_elemss context; 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

605 
val raw_propps = map flat raw_proppss; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

606 
val raw_propp = flat raw_propps; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

608 
prepp (ProofContext.declare_terms (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

609 
val ctxt = ProofContext.declare_terms (flat (map (map fst) all_propp)) ctxt; 
12502  610 

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

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

612 
(#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp))), map (map snd) all_propp); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

613 
val n = length raw_concl; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

614 
val concl = take (n, all_propp'); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

615 
val propp = drop (n, all_propp'); 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

616 
val propps = unflat raw_propps propp; 
12839  617 
val proppss = map (uncurry unflat) (raw_proppss ~~ propps); 
12502  618 

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

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

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

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

623 
val parms = param_types (xs ~~ typing); 
12273  624 

13308  625 
val (text, elemss) = 
13336  626 
finish_elemss ctxt parms do_close do_text (([], ([], [], [])), raw_elemss ~~ proppss); 
13308  627 
in ((parms, elemss, concl), text) end; 
12502  628 

629 
in 

630 

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

631 
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

632 
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

633 

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

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

635 

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

636 

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

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

638 

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

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

640 

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

641 
fun prep_name ctxt (name, atts) = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

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

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

645 

13336  646 
fun prep_facts _ _ (Int elem) = (elem, false) 
647 
 prep_facts _ _ (Ext (Fixes fixes)) = (Fixes fixes, true) 

648 
 prep_facts _ ctxt (Ext (Assumes asms)) = (Assumes (map (apfst (prep_name ctxt)) asms), true) 

649 
 prep_facts _ ctxt (Ext (Defines defs)) = (Defines (map (apfst (prep_name ctxt)) defs), true) 

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

651 
(prep_name ctxt a, map (apfst (get ctxt)) bs))), true); 

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

652 

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

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

654 

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

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

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

657 

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

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

659 

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

660 

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

662 

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

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

664 

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

665 
fun prep_context_statement prep_expr prep_elemss prep_facts 
13308  666 
do_close do_text fixed_params import elements raw_concl context = 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

668 
val sign = ProofContext.sign_of context; 
12575  669 
fun flatten (ids, Elem (Fixes fixes)) = 
670 
(ids, [(("", map (rpair None o #1) fixes), Ext (Fixes fixes))]) 

671 
 flatten (ids, Elem elem) = (ids, [(("", []), Ext elem)]) 

672 
 flatten (ids, Expr expr) = 

13308  673 
apsnd (map (apsnd Int)) (flatten_expr context (ids, prep_expr sign expr)); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

674 

12575  675 
val (import_ids, raw_import_elemss) = flatten ([], Expr import); 
676 
val raw_elemss = flat (#2 ((foldl_map flatten (import_ids, elements)))); 

13336  677 
val ((parms, all_elemss, concl), (spec, (xs, _, defs))) = prep_elemss do_close do_text 
678 
context fixed_params (raw_import_elemss @ raw_elemss) raw_concl; 

679 
val xs' = parms > mapfilter (fn (p, _) => 

680 
(case assoc_string (xs, p) of None => None  Some T => Some (p, T))); 

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

681 

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

682 
val n = length raw_import_elemss; 
12839  683 
val (import_ctxt, (import_elemss, import_facts)) = 
684 
activate_facts prep_facts (context, take (n, all_elemss)); 

685 
val (ctxt, (elemss, facts)) = 

686 
activate_facts prep_facts (import_ctxt, drop (n, all_elemss)); 

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

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

688 
((((import_ctxt, (import_elemss, import_facts)), 
13336  689 
(ctxt, (elemss, facts))), (xs', spec, defs)), concl) 
12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

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

691 

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

692 
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

693 
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

694 

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

695 
fun gen_facts prep_locale thy name = 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

696 
let val ((((_, (_, facts)), _), _), _) = thy > ProofContext.init 
13308  697 
> gen_context_i false false [] (Locale (prep_locale (Theory.sign_of thy) name)) [] []; 
13297  698 
in flat (map #2 facts) end; 
12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

699 

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

700 
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

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

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

703 
val locale = apsome (prep_locale (Theory.sign_of thy)) raw_locale; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

704 
val (fixed_params, import) = 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

705 
(case locale of None => ([], empty) 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

706 
 Some name => (param_types (#1 (#params (the_locale thy name))), Locale name)); 
12730  707 
val ((((locale_ctxt, _), (elems_ctxt, _)), _), concl') = 
13308  708 
prep_ctxt false false fixed_params import elems concl ctxt; 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

709 
in (locale, locale_ctxt, elems_ctxt, concl') end; 
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

710 

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

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

712 

13308  713 
fun read_context b x y z = #1 (gen_context true b [] x y [] z); 
714 
fun cert_context b x y z = #1 (gen_context_i true b [] x y [] z); 

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

715 
val locale_facts = gen_facts intern; 
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset

716 
val locale_facts_i = gen_facts (K I); 
12529
d99716a53f59
simultaneous typeinference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset

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

718 
val cert_context_statement = gen_statement (K I) gen_context_i; 
12502  719 

720 
end; 

11896  721 

722 

723 

13336  724 
(** define locales **) 
725 

726 
(* print locale *) 

12070  727 

12758  728 
fun print_locale thy import body = 
12070  729 
let 
730 
val sg = Theory.sign_of thy; 

12289  731 
val thy_ctxt = ProofContext.init thy; 
13336  732 
val (((_, (import_elemss, _)), (ctxt, (elemss, _))), _) = 
733 
read_context false import body thy_ctxt; 

734 
val all_elems = map #1 (flat (map #2 (import_elemss @ elemss))); 

12070  735 

12307  736 
val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt; 
737 
val prt_term = Pretty.quote o ProofContext.pretty_term ctxt; 

738 
val prt_thm = Pretty.quote o ProofContext.pretty_thm ctxt; 

12070  739 

740 
fun prt_syn syn = 

741 
let val s = (case syn of None => "(structure)"  Some mx => Syntax.string_of_mixfix mx) 

12575  742 
in if s = "" then [] else [Pretty.brk 2, Pretty.str s] end; 
12070  743 
fun prt_fix (x, Some T, syn) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 :: 
744 
prt_typ T :: Pretty.brk 1 :: prt_syn syn) 

745 
 prt_fix (x, None, syn) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_syn syn); 

746 

12307  747 
fun prt_name "" = [Pretty.brk 1] 
748 
 prt_name name = [Pretty.str (ProofContext.cond_extern ctxt name ^ ":"), Pretty.brk 1]; 

749 
fun prt_asm ((a, _), ts) = Pretty.block (prt_name a @ Pretty.breaks (map (prt_term o fst) ts)); 

750 
fun prt_def ((a, _), (t, _)) = Pretty.block (prt_name a @ [prt_term t]); 

751 
fun prt_fact ((a, _), ths) = Pretty.block 

752 
(prt_name a @ Pretty.breaks (map prt_thm (flat (map fst ths)))); 

12070  753 

12289  754 
fun items _ [] = [] 
755 
 items prfx (x :: xs) = Pretty.block [Pretty.str prfx, Pretty.brk 1, x] :: items " and" xs; 

756 
fun prt_elem (Fixes fixes) = items "fixes" (map prt_fix fixes) 

757 
 prt_elem (Assumes asms) = items "assumes" (map prt_asm asms) 

758 
 prt_elem (Defines defs) = items "defines" (map prt_def defs) 

759 
 prt_elem (Notes facts) = items "notes" (map prt_fact facts); 

12277  760 
in 
13336  761 
Pretty.big_list "context elements:" (map (Pretty.chunks o prt_elem) all_elems) 
762 
> Pretty.writeln 

12277  763 
end; 
12070  764 

765 

12730  766 
(* store results *) 
11896  767 

12706  768 
local 
769 

12702  770 
fun hide_bound_names names thy = 
771 
thy > PureThy.hide_thms false 

772 
(map (Sign.full_name (Theory.sign_of thy)) (filter_out (equal "") names)); 

773 

12958  774 
in 
775 

12706  776 
fun have_thmss_qualified kind loc args thy = 
777 
thy 

778 
> Theory.add_path (Sign.base_name loc) 

12711  779 
> PureThy.have_thmss_i (Drule.kind kind) args 
12706  780 
>> hide_bound_names (map (#1 o #1) args) 
781 
>> Theory.parent_path; 

782 

12958  783 
fun smart_have_thmss kind None = PureThy.have_thmss_i (Drule.kind kind) 
784 
 smart_have_thmss kind (Some (loc, _)) = have_thmss_qualified kind loc; 

785 

786 
end; 

787 

788 
local 

789 

790 
fun put_facts loc args thy = 

791 
let 

13308  792 
val {import, elems, params} = the_locale thy loc; 
12958  793 
val note = Notes (map (fn ((a, more_atts), th_atts) => 
794 
((a, more_atts), map (apfst (map (curry Thm.name_thm a))) th_atts)) args); 

13308  795 
in thy > put_locale loc (make_locale import (elems @ [(note, stamp ())]) params) end; 
12958  796 

12706  797 
fun gen_have_thmss prep_locale get_thms kind raw_loc raw_args thy = 
798 
let 

799 
val thy_ctxt = ProofContext.init thy; 

800 
val loc = prep_locale (Theory.sign_of thy) raw_loc; 

13308  801 
val loc_ctxt = #1 (#1 (#1 (cert_context false (Locale loc) [] thy_ctxt))); 
12706  802 
val args = map (apsnd (map (apfst (get_thms loc_ctxt)))) raw_args; 
803 
val export = Drule.local_standard o ProofContext.export_single loc_ctxt thy_ctxt; 

12711  804 
val results = map (map export o #2) (#2 (ProofContext.have_thmss_i args loc_ctxt)); 
12706  805 
val args' = map (rpair [] o #1 o #1) args ~~ map (single o Thm.no_attributes) results; 
806 
in 

807 
thy 

808 
> put_facts loc args 

809 
> have_thmss_qualified kind loc args' 

810 
end; 

811 

812 
in 

813 

12711  814 
val have_thmss = gen_have_thmss intern ProofContext.get_thms; 
815 
val have_thmss_i = gen_have_thmss (K I) (K I); 

816 

13336  817 
fun add_thmss loc args (thy, ctxt) = 
12958  818 
let 
819 
val args' = map (fn ((a, ths), atts) => ((a, atts), [(ths, [])])) args; 

13336  820 
val thy' = put_facts loc args' thy; 
821 
val (ctxt', (_, facts')) = activate_facts (K I) (ctxt, [((loc, []), [(Notes args', false)])]); 

822 
in ((thy', ctxt'), map #2 facts') end; 

12702  823 

12706  824 
end; 
12063  825 

11896  826 

13336  827 
(* predicate text *) 
828 

829 
val predN = suffix "_axioms"; 

830 

831 
fun define_pred _ _ _ [] thy = thy 

832 
 define_pred bname name xs ts thy = 

833 
let 

834 
val sign = Theory.sign_of thy; 

835 

836 
val body = ObjectLogic.atomize_term sign (Library.foldr1 Logic.mk_conjunction ts); 

837 
val bodyT = Term.fastype_of body; 

838 
val predT = map #2 xs > bodyT; 

839 

840 
val n = length xs; 

841 
fun aprop_tr' c = (c, fn args => 

842 
if length args = n then Syntax.const "_aprop" $ Term.list_comb (Syntax.free c, args) 

843 
else raise Match); 

844 
in 

845 
thy 

846 
> (if bodyT <> propT then I 

847 
else Theory.add_trfuns ([], [], map aprop_tr' (NameSpace.accesses' (predN name)), [])) 

848 
> Theory.add_consts_i [(predN bname, predT, Syntax.NoSyn)] 

849 
> PureThy.add_defs_i false [((Thm.def_name (predN bname), 

850 
Logic.mk_equals (Term.list_comb (Const (predN name, predT), map Free xs), body)), [])] 

851 
> #1 

852 
end; 

853 

854 

13297  855 
(* add_locale(_i) *) 
856 

857 
local 

858 

859 
fun gen_add_locale prep_ctxt prep_expr bname raw_import raw_body thy = 

860 
let 

861 
val sign = Theory.sign_of thy; 

862 
val name = Sign.full_name sign bname; 

863 
val _ = conditional (is_some (get_locale thy name)) (fn () => 

864 
error ("Duplicate definition of locale " ^ quote name)); 

865 

866 
val thy_ctxt = ProofContext.init thy; 

13336  867 
val (((import_ctxt, (import_elemss, _)), (body_ctxt, (body_elemss, _))), 
868 
(pred_xs, pred_ts, defs)) = prep_ctxt true raw_import raw_body thy_ctxt; 

13297  869 

870 
val import_parms = params_of import_elemss; 

871 
val body_parms = params_of body_elemss; 

872 
val all_parms = import_parms @ body_parms; 

873 

874 
val import = prep_expr sign raw_import; 

13336  875 
val elems = map fst (flat (map snd body_elemss)); 
13297  876 
in 
877 
thy 

13336  878 
> define_pred bname name pred_xs pred_ts 
13297  879 
> declare_locale name 
880 
> put_locale name (make_locale import (map (fn e => (e, stamp ())) elems) 

13308  881 
(all_parms, map fst body_parms)) 
13297  882 
end; 
883 

884 
in 

885 

886 
val add_locale = gen_add_locale read_context intern_expr; 

887 
val add_locale_i = gen_add_locale cert_context (K I); 

888 

889 
end; 

890 

891 

12730  892 

11896  893 
(** locale theory setup **) 
12063  894 

11896  895 
val setup = 
896 
[LocalesData.init]; 

897 

898 
end; 