author  paulson 
Fri, 21 Jan 2005 18:00:18 +0100  
changeset 15452  e2a721567f67 
parent 14981  e73f8140af78 
child 15456  956d6acacf89 
permissions  rwrr 
5819  1 
(* Title: Pure/Isar/proof_context.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 

5 
Proof context information. 

6 
*) 

7 

15452  8 
(*Jia: changed: datatype context 
9 
affected files: make_context, map_context, init, put_data, add_syntax, map_defaults, del_bind, upd_bind, qualified, hide_thms, put_thms, reset_thms, gen_assms, map_fixes, add_cases 

10 

11 
added: put_delta, get_delta 

12 
06/01/05 

13 
*) 

14 

14707  15 
val show_structs = ref false; 
16 

5819  17 
signature PROOF_CONTEXT = 
18 
sig 

19 
type context 

9470  20 
type exporter 
5819  21 
exception CONTEXT of string * context 
22 
val theory_of: context > theory 

23 
val sign_of: context > Sign.sg 

14828  24 
val is_fixed: context > string > bool 
12057  25 
val fixed_names_of: context > string list 
26 
val assumptions_of: context > (cterm list * exporter) list 

7557  27 
val prems_of: context > thm list 
5819  28 
val print_proof_data: theory > unit 
5874  29 
val init: theory > context 
14828  30 
val pretty_term: context > term > Pretty.T 
31 
val pretty_typ: context > typ > Pretty.T 

32 
val pretty_sort: context > sort > Pretty.T 

33 
val pp: context > Pretty.pp 

34 
val pretty_thm: context > thm > Pretty.T 

35 
val pretty_thms: context > thm list > Pretty.T 

36 
val pretty_fact: context > string * thm list > Pretty.T 

37 
val string_of_term: context > term > string 

12414  38 
val default_type: context > string > typ option 
12504  39 
val used_types: context > string list 
5819  40 
val read_typ: context > string > typ 
14780  41 
val read_typ_raw: context > string > typ 
5819  42 
val cert_typ: context > typ > typ 
14780  43 
val cert_typ_raw: context > typ > typ 
10583  44 
val get_skolem: context > string > string 
9133  45 
val extern_skolem: context > term > term 
14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

46 
val read_termTs: context > (string > bool) > (indexname > typ option) 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

47 
> (indexname > sort option) > string list > (string * typ) list 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

48 
> term list * (indexname * typ) list 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

49 
val read_termTs_schematic: context > (string > bool) > (indexname > typ option) 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

50 
> (indexname > sort option) > string list > (string * typ) list 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

51 
> term list * (indexname * typ) list 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

52 
val read_term_liberal: context > string > term 
5819  53 
val read_term: context > string > term 
54 
val read_prop: context > string > term 

11925  55 
val read_prop_schematic: context > string > term 
10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

56 
val read_terms: context > string list > term list 
8096  57 
val read_term_pats: typ > context > string list > term list 
58 
val read_prop_pats: context > string list > term list 

5819  59 
val cert_term: context > term > term 
60 
val cert_prop: context > term > term 

8096  61 
val cert_term_pats: typ > context > term list > term list 
62 
val cert_prop_pats: context > term list > term list 

5819  63 
val declare_term: term > context > context 
64 
val declare_terms: term list > context > context 

7925  65 
val warn_extra_tfrees: context > context > context 
12550
32843ad8160a
generalize type variables properly: start with occurrences in objects
wenzelm
parents:
12530
diff
changeset

66 
val generalize: context > context > term list > term list 
9470  67 
val find_free: term > string > term option 
12008  68 
val export: bool > context > context > thm > thm Seq.seq 
13415  69 
val export_standard: cterm list > context > context > thm > thm 
10810  70 
val drop_schematic: indexname * term option > indexname * term option 
71 
val add_binds: (indexname * string option) list > context > context 

72 
val add_binds_i: (indexname * term option) list > context > context 

12147  73 
val auto_bind_goal: term list > context > context 
74 
val auto_bind_facts: term list > context > context 

8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

75 
val match_bind: bool > (string list * string) list > context > context 
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

76 
val match_bind_i: bool > (term list * term) list > context > context 
10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

77 
val read_propp: context * (string * (string list * string list)) list list 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

78 
> context * (term * (term list * term list)) list list 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

79 
val cert_propp: context * (term * (term list * term list)) list list 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

80 
> context * (term * (term list * term list)) list list 
10554  81 
val read_propp_schematic: context * (string * (string list * string list)) list list 
82 
> context * (term * (term list * term list)) list list 

83 
val cert_propp_schematic: context * (term * (term list * term list)) list list 

84 
> context * (term * (term list * term list)) list list 

10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

85 
val bind_propp: context * (string * (string list * string list)) list list 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

86 
> context * (term list list * (context > context)) 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

87 
val bind_propp_i: context * (term * (term list * term list)) list list 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

88 
> context * (term list list * (context > context)) 
10554  89 
val bind_propp_schematic: context * (string * (string list * string list)) list list 
90 
> context * (term list list * (context > context)) 

91 
val bind_propp_schematic_i: context * (term * (term list * term list)) list list 

92 
> context * (term list list * (context > context)) 

6091  93 
val get_thm: context > string > thm 
9566  94 
val get_thm_closure: context > string > thm 
6091  95 
val get_thms: context > string > thm list 
9566  96 
val get_thms_closure: context > string > thm list 
12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

97 
val cond_extern: context > string > xstring 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13378
diff
changeset

98 
val qualified: bool > context > context 
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13378
diff
changeset

99 
val restore_qualified: context > context > context 
13425
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
13415
diff
changeset

100 
val hide_thms: bool > string list > context > context 
6091  101 
val put_thm: string * thm > context > context 
102 
val put_thms: string * thm list > context > context 

103 
val put_thmss: (string * thm list) list > context > context 

7606  104 
val reset_thms: string > context > context 
14564  105 
val note_thmss: 
12711  106 
((bstring * context attribute list) * (xstring * context attribute list) list) list > 
107 
context > context * (bstring * thm list) list 

14564  108 
val note_thmss_i: 
12711  109 
((bstring * context attribute list) * (thm list * context attribute list) list) list > 
110 
context > context * (bstring * thm list) list 

11918
dfdf0798d7b8
added export_assume, export_presume, export_def (from proof.ML);
wenzelm
parents:
11915
diff
changeset

111 
val export_assume: exporter 
dfdf0798d7b8
added export_assume, export_presume, export_def (from proof.ML);
wenzelm
parents:
11915
diff
changeset

112 
val export_presume: exporter 
12086  113 
val cert_def: context > term > string * term 
11918
dfdf0798d7b8
added export_assume, export_presume, export_def (from proof.ML);
wenzelm
parents:
11915
diff
changeset

114 
val export_def: exporter 
9470  115 
val assume: exporter 
10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

116 
> ((string * context attribute list) * (string * (string list * string list)) list) list 
12835  117 
> context > context * (bstring * thm list) list 
9470  118 
val assume_i: exporter 
10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

119 
> ((string * context attribute list) * (term * (term list * term list)) list) list 
12835  120 
> context > context * (bstring * thm list) list 
14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

121 
val read_vars: context * (string list * string option) 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

122 
> context * (string list * typ option) 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

123 
val cert_vars: context * (string list * typ option) 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

124 
> context * (string list * typ option) 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

125 
val read_vars_liberal: context * (string list * string option) 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

126 
> context * (string list * typ option) 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

127 
val cert_vars_liberal: context * (string list * typ option) 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

128 
> context * (string list * typ option) 
7411  129 
val fix: (string list * string option) list > context > context 
7663  130 
val fix_i: (string list * typ option) list > context > context 
14643  131 
val add_fixes: (string * typ option * Syntax.mixfix option) list > context > context 
14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

132 
val add_fixes_liberal: (string * typ option * Syntax.mixfix option) list > context > context 
12016  133 
val fix_frees: term list > context > context 
9291
23705d14be8f
"_i" arguments now expected to have skolems already internalized;
wenzelm
parents:
9274
diff
changeset

134 
val bind_skolem: context > string list > term > term 
11793
5f0ab6f5c280
support impromptu terminology of cases parameters;
wenzelm
parents:
11764
diff
changeset

135 
val get_case: context > string > string option list > RuleCases.T 
8373
e7237c8fe29e
handling of local contexts: print_cases, get_case, add_cases;
wenzelm
parents:
8186
diff
changeset

136 
val add_cases: (string * RuleCases.T) list > context > context 
13425
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
13415
diff
changeset

137 
val apply_case: RuleCases.T > context 
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
13415
diff
changeset

138 
> context * ((indexname * term option) list * (string * term list) list) 
10810  139 
val verbose: bool ref 
140 
val setmp_verbose: ('a > 'b) > 'a > 'b 

12072
4281198fb8cd
local syntax: add_syntax, proper read/pretty functions;
wenzelm
parents:
12066
diff
changeset

141 
val print_syntax: context > unit 
10810  142 
val print_binds: context > unit 
12057  143 
val print_lthms: context > unit 
10810  144 
val print_cases: context > unit 
145 
val prems_limit: int ref 

12057  146 
val pretty_asms: context > Pretty.T list 
10810  147 
val pretty_context: context > Pretty.T list 
13284  148 
val thms_containing_limit: int ref 
149 
val print_thms_containing: context > int option > string list > unit 

5819  150 
val setup: (theory > theory) list 
15452  151 

152 
val get_delta: context > Object.T Symtab.table (* Jia: (claset, simpset) *) 

153 
val put_delta: Object.T Symtab.table > context > context 

154 
val get_delta_count_incr: context > int 

155 

5819  156 
end; 
157 

8151  158 
signature PRIVATE_PROOF_CONTEXT = 
5819  159 
sig 
160 
include PROOF_CONTEXT 

161 
val init_data: Object.kind > (theory > Object.T) * (context > Object.T > unit) 

162 
> theory > theory 

163 
val print_data: Object.kind > context > unit 

164 
val get_data: Object.kind > (Object.T > 'a) > context > 'a 

165 
val put_data: Object.kind > ('a > Object.T) > 'a > context > context 

166 
end; 

167 

8151  168 
structure ProofContext: PRIVATE_PROOF_CONTEXT = 
5819  169 
struct 
170 

171 

172 
(** datatype context **) 

173 

11816  174 
type exporter = bool > cterm list > thm > thm Seq.seq; 
9470  175 

15452  176 
(* note: another field added to context. *) 
5819  177 
datatype context = 
178 
Context of 

12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

179 
{thy: theory, (*current theory*) 
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

180 
syntax: Syntax.syntax * string list * string list, (*syntax with structs and mixfixed*) 
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

181 
data: Object.T Symtab.table, (*user data*) 
5819  182 
asms: 
12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

183 
((cterm list * exporter) list * (*assumes: A ==> _*) 
14697  184 
(string * thm list) list) * (*prems: A  A *) 
12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

185 
(string * string) list, (*fixes: !!x. _*) 
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

186 
binds: (term * typ) option Vartab.table, (*term bindings*) 
13278
b62514fcbcab
print_thms_containing: index variables, refer to local facts as well;
wenzelm
parents:
12863
diff
changeset

187 
thms: bool * NameSpace.T * thm list option Symtab.table 
b62514fcbcab
print_thms_containing: index variables, refer to local facts as well;
wenzelm
parents:
12863
diff
changeset

188 
* FactIndex.T, (*local thms*) 
14697  189 
(*thms is of the form (q, n, t, i) where 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14287
diff
changeset

190 
q: indicates whether theorems with qualified names may be stored; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14287
diff
changeset

191 
this is initially forbidden (false); flag may be changed with 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14287
diff
changeset

192 
qualified and restore_qualified; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14287
diff
changeset

193 
n: theorem namespace; 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14287
diff
changeset

194 
t: table of theorems; 
14697  195 
i: index for theorem lookup (cf. thms_containing) *) 
12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

196 
cases: (string * RuleCases.T) list, (*local contexts*) 
5819  197 
defs: 
12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

198 
typ Vartab.table * (*type constraints*) 
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

199 
sort Vartab.table * (*default sorts*) 
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

200 
string list * (*used type variables*) 
15452  201 
term list Symtab.table, 
202 
delta: Object.T Symtab.table (* difference between local and global claset and simpset*), 

203 
delta_count: int ref (* number of local anonymous thms *) 

204 
}; (*type variable occurrences*) 

5819  205 

206 
exception CONTEXT of string * context; 

207 

208 

15452  209 
fun make_context (thy, syntax, data, asms, binds, thms, cases, defs, delta, delta_count) = 
12072
4281198fb8cd
local syntax: add_syntax, proper read/pretty functions;
wenzelm
parents:
12066
diff
changeset

210 
Context {thy = thy, syntax = syntax, data = data, asms = asms, binds = binds, 
15452  211 
thms = thms, cases = cases, defs = defs, delta = delta, delta_count = delta_count}; 
5819  212 

15452  213 
fun map_context f (Context {thy, syntax, data, asms, binds, thms, cases, defs, delta, delta_count}) = 
214 
make_context (f (thy, syntax, data, asms, binds, thms, cases, defs, delta, delta_count)); 

5819  215 

216 
fun theory_of (Context {thy, ...}) = thy; 

217 
val sign_of = Theory.sign_of o theory_of; 

12072
4281198fb8cd
local syntax: add_syntax, proper read/pretty functions;
wenzelm
parents:
12066
diff
changeset

218 
fun syntax_of (Context {syntax, ...}) = syntax; 
5819  219 

12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

220 
fun fixes_of (Context {asms = (_, fixes), ...}) = fixes; 
12057  221 
val fixed_names_of = map #2 o fixes_of; 
12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

222 
fun is_fixed ctxt x = exists (equal x o #2) (fixes_of ctxt); 
13278
b62514fcbcab
print_thms_containing: index variables, refer to local facts as well;
wenzelm
parents:
12863
diff
changeset

223 
fun is_known (ctxt as Context {defs = (types, _, _, _), ...}) x = 
b62514fcbcab
print_thms_containing: index variables, refer to local facts as well;
wenzelm
parents:
12863
diff
changeset

224 
is_some (Vartab.lookup (types, (x, ~1))) orelse is_fixed ctxt x; 
12291  225 
fun type_occs (Context {defs = (_, _, _, tab), ...}) = tab; 
12057  226 

227 
fun assumptions_of (Context {asms = ((asms, _), _), ...}) = asms; 

228 
fun prems_of (Context {asms = ((_, prems), _), ...}) = flat (map #2 prems); 

229 

7270  230 

5819  231 

232 
(** user data **) 

233 

234 
(* errors *) 

235 

236 
fun of_theory thy = "\nof theory " ^ Sign.str_of_sg (Theory.sign_of thy); 

237 

238 
fun err_inconsistent kinds = 

239 
error ("Attempt to merge different versions of " ^ commas_quote kinds ^ " proof data"); 

240 

241 
fun err_dup_init thy kind = 

242 
error ("Duplicate initialization of " ^ quote kind ^ " proof data" ^ of_theory thy); 

243 

244 
fun err_undef ctxt kind = 

245 
raise CONTEXT ("Tried to access undefined " ^ quote kind ^ " proof data", ctxt); 

246 

247 
fun err_uninit ctxt kind = 

248 
raise CONTEXT ("Tried to access uninitialized " ^ quote kind ^ " proof data" ^ 

249 
of_theory (theory_of ctxt), ctxt); 

250 

251 
fun err_access ctxt kind = 

252 
raise CONTEXT ("Unauthorized access to " ^ quote kind ^ " proof data" ^ 

253 
of_theory (theory_of ctxt), ctxt); 

254 

255 

256 
(* data kind 'Isar/proof_data' *) 

257 

258 
structure ProofDataDataArgs = 

259 
struct 

260 
val name = "Isar/proof_data"; 

261 
type T = (Object.kind * ((theory > Object.T) * (context > Object.T > unit))) Symtab.table; 

262 

263 
val empty = Symtab.empty; 

6550  264 
val copy = I; 
5819  265 
val prep_ext = I; 
266 
fun merge tabs = Symtab.merge (Object.eq_kind o pairself fst) tabs 

267 
handle Symtab.DUPS kinds => err_inconsistent kinds; 

268 
fun print _ tab = Pretty.writeln (Pretty.strs (map #1 (Symtab.dest tab))); 

269 
end; 

270 

271 
structure ProofDataData = TheoryDataFun(ProofDataDataArgs); 

272 
val print_proof_data = ProofDataData.print; 

273 

274 

275 
(* init proof data *) 

276 

277 
fun init_data kind meths thy = 

278 
let 

279 
val name = Object.name_of_kind kind; 

280 
val tab = Symtab.update_new ((name, (kind, meths)), ProofDataData.get thy) 

281 
handle Symtab.DUP _ => err_dup_init thy name; 

282 
in thy > ProofDataData.put tab end; 

283 

284 

285 
(* access data *) 

286 

287 
fun lookup_data (ctxt as Context {data, ...}) kind = 

288 
let 

289 
val thy = theory_of ctxt; 

290 
val name = Object.name_of_kind kind; 

291 
in 

292 
(case Symtab.lookup (ProofDataData.get thy, name) of 

293 
Some (k, meths) => 

294 
if Object.eq_kind (kind, k) then 

295 
(case Symtab.lookup (data, name) of 

296 
Some x => (x, meths) 

297 
 None => err_undef ctxt name) 

298 
else err_access ctxt name 

299 
 None => err_uninit ctxt name) 

300 
end; 

301 

302 
fun get_data kind f ctxt = 

303 
let val (x, _) = lookup_data ctxt kind 

304 
in f x handle Match => Object.kind_error kind end; 

305 

306 
fun print_data kind ctxt = 

307 
let val (x, (_, prt)) = lookup_data ctxt kind 

308 
in prt ctxt x end; 

309 

310 
fun put_data kind f x ctxt = 

8373
e7237c8fe29e
handling of local contexts: print_cases, get_case, add_cases;
wenzelm
parents:
8186
diff
changeset

311 
(lookup_data ctxt kind; 
15452  312 
map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs, delta,delta_count) => 
12072
4281198fb8cd
local syntax: add_syntax, proper read/pretty functions;
wenzelm
parents:
12066
diff
changeset

313 
(thy, syntax, Symtab.update ((Object.name_of_kind kind, f x), data), 
15452  314 
asms, binds, thms, cases, defs, delta, delta_count)) ctxt); 
315 

316 

317 
(* added get_delta and put_delta *) 

318 

319 
fun get_delta (ctxt as Context {delta, ...}) = delta; 

320 

321 
fun get_delta_count (ctxt as Context {delta_count, ...}) = !delta_count; 

322 

323 
fun get_delta_count_incr (ctxt as Context {delta_count, ...}) = 

324 
let val current_delta_count = !delta_count 

325 
in 

326 
(delta_count:=(!delta_count)+1;current_delta_count) 

327 
end; 

328 

329 
fun incr_delta_count (ctxt as Context {delta_count, ...}) = (delta_count:=(!delta_count)+1); 

330 

331 
(* replace the old delta by new delta *) 

332 
(* count not changed! *) 

333 
fun put_delta new_delta ctxt = 

334 
map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs,delta, delta_count) => 

335 
(thy, syntax, data, asms, binds, thms, cases, defs, new_delta,delta_count)) ctxt; 

5819  336 

337 

338 
(* init context *) 

339 

5874  340 
fun init thy = 
341 
let val data = Symtab.map (fn (_, (f, _)) => f thy) (ProofDataData.get thy) in 

12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

342 
make_context (thy, (Theory.syn_of thy, [], []), data, (([], []), []), Vartab.empty, 
13278
b62514fcbcab
print_thms_containing: index variables, refer to local facts as well;
wenzelm
parents:
12863
diff
changeset

343 
(false, NameSpace.empty, Symtab.empty, FactIndex.empty), [], 
15452  344 
(Vartab.empty, Vartab.empty, [], Symtab.empty), Symtab.empty, ref 0) 
5819  345 
end; 
346 

347 

8096  348 

12093  349 
(** local syntax **) 
350 

351 
val fixedN = "\\<^fixed>"; 

352 
val structN = "\\<^struct>"; 

353 

12100  354 

14697  355 
(* translation functions *) 
14665
d2e5df3d1201
index syntax: support for general expressions (input only);
wenzelm
parents:
14643
diff
changeset

356 

d2e5df3d1201
index syntax: support for general expressions (input only);
wenzelm
parents:
14643
diff
changeset

357 
fun fixed_tr x = (fixedN ^ x, curry Term.list_comb (Syntax.free x)); 
d2e5df3d1201
index syntax: support for general expressions (input only);
wenzelm
parents:
14643
diff
changeset

358 

12100  359 
fun context_tr' ctxt = 
360 
let 

361 
val (_, structs, mixfixed) = syntax_of ctxt; 

362 

363 
fun tr' (t $ u) = tr' t $ tr' u 

364 
 tr' (Abs (x, T, t)) = Abs (x, T, tr' t) 

365 
 tr' (t as Free (x, T)) = 

14697  366 
let val i = Library.find_index_eq x structs + 1 in 
367 
if i = 0 andalso x mem_string mixfixed then Const (fixedN ^ x, T) 

14707  368 
else if i = 1 andalso not (! show_structs) then 
369 
Syntax.const "_struct" $ Syntax.const "_indexdefault" 

12100  370 
else t 
371 
end 

372 
 tr' a = a; 

373 
in tr' end; 

374 

375 

12576
9fd10052c3f7
added add_fixes: derives mssing type scheme from mixfix;
wenzelm
parents:
12550
diff
changeset

376 
(* add syntax *) 
9fd10052c3f7
added add_fixes: derives mssing type scheme from mixfix;
wenzelm
parents:
12550
diff
changeset

377 

9fd10052c3f7
added add_fixes: derives mssing type scheme from mixfix;
wenzelm
parents:
12550
diff
changeset

378 
fun mixfix_type mx = replicate (Syntax.mixfix_args mx) TypeInfer.logicT > TypeInfer.logicT; 
12093  379 

380 
local 

381 

14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

382 
fun mixfix x None mx = (fixedN ^ x, mixfix_type mx, Syntax.fix_mixfix x mx) 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

383 
 mixfix x (Some T) mx = (fixedN ^ x, T, Syntax.fix_mixfix x mx); 
12093  384 

385 
fun prep_mixfix (_, _, None) = None 

386 
 prep_mixfix (x, opt_T, Some mx) = Some (mixfix x opt_T mx); 

387 

388 
fun prep_mixfix' (_, _, None) = None 

389 
 prep_mixfix' (x, _, Some Syntax.NoSyn) = None 

12863  390 
 prep_mixfix' (x, opt_T, _) = Some (x, mixfix x opt_T (Syntax.literal x)); 
12093  391 

392 
fun prep_struct (x, _, None) = Some x 

393 
 prep_struct _ = None; 

394 

395 
in 

396 

397 
fun add_syntax decls = 

15452  398 
map_context (fn (thy, (syn, structs, mixfixed), data, asms, binds, thms, cases, defs, delta, delta_count) => 
12093  399 
let 
14901  400 
val is_logtype = Sign.is_logtype (Theory.sign_of thy); 
12093  401 
val structs' = structs @ mapfilter prep_struct decls; 
402 
val mxs = mapfilter prep_mixfix decls; 

403 
val (fixed, mxs_output) = Library.split_list (mapfilter prep_mixfix' decls); 

404 
val trs = map fixed_tr fixed; 

405 
val syn' = syn 

14901  406 
> Syntax.extend_const_gram is_logtype ("", false) mxs_output 
407 
> Syntax.extend_const_gram is_logtype ("", true) mxs 

12093  408 
> Syntax.extend_trfuns ([], trs, [], []); 
15452  409 
in (thy, (syn', structs', fixed @ mixfixed), data, asms, binds, thms, cases, defs, delta, delta_count) end) 
12093  410 

411 
fun syn_of (Context {syntax = (syn, structs, _), ...}) = 

14697  412 
syn > Syntax.extend_trfuns (Syntax.struct_trfuns structs); 
413 

12093  414 
end; 
415 

416 

417 

14828  418 
(** pretty printing **) 
419 

14974
b1ecb7859c99
avoid premature evaluation of syn_of (wastes time in conjunction with pp);
wenzelm
parents:
14901
diff
changeset

420 
fun pretty_term ctxt t = Sign.pretty_term' (syn_of ctxt) (sign_of ctxt) (context_tr' ctxt t); 
b1ecb7859c99
avoid premature evaluation of syn_of (wastes time in conjunction with pp);
wenzelm
parents:
14901
diff
changeset

421 
fun pretty_typ ctxt T = Sign.pretty_typ (sign_of ctxt) T; 
b1ecb7859c99
avoid premature evaluation of syn_of (wastes time in conjunction with pp);
wenzelm
parents:
14901
diff
changeset

422 
fun pretty_sort ctxt S = Sign.pretty_sort (sign_of ctxt) S; 
b1ecb7859c99
avoid premature evaluation of syn_of (wastes time in conjunction with pp);
wenzelm
parents:
14901
diff
changeset

423 
fun pretty_classrel ctxt cs = Sign.pretty_classrel (sign_of ctxt) cs; 
b1ecb7859c99
avoid premature evaluation of syn_of (wastes time in conjunction with pp);
wenzelm
parents:
14901
diff
changeset

424 
fun pretty_arity ctxt ar = Sign.pretty_arity (sign_of ctxt) ar; 
14828  425 

14974
b1ecb7859c99
avoid premature evaluation of syn_of (wastes time in conjunction with pp);
wenzelm
parents:
14901
diff
changeset

426 
fun pp ctxt = Pretty.pp (pretty_term ctxt, pretty_typ ctxt, pretty_sort ctxt, 
b1ecb7859c99
avoid premature evaluation of syn_of (wastes time in conjunction with pp);
wenzelm
parents:
14901
diff
changeset

427 
pretty_classrel ctxt, pretty_arity ctxt); 
14828  428 

429 
val string_of_term = Pretty.string_of oo pretty_term; 

430 

431 
fun pretty_thm ctxt thm = 

432 
if ! Display.show_hyps then 

14876  433 
Display.pretty_thm_aux (pp ctxt) false thm 
14828  434 
else pretty_term ctxt (Thm.prop_of thm); 
435 

436 
fun pretty_thms ctxt [th] = pretty_thm ctxt th 

437 
 pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths)); 

438 

439 
fun pretty_fact ctxt ("", ths) = pretty_thms ctxt ths 

440 
 pretty_fact ctxt (a, [th]) = 

441 
Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, pretty_thm ctxt th] 

442 
 pretty_fact ctxt (a, ths) = 

443 
Pretty.block (Pretty.fbreaks (Pretty.str (a ^ ":") :: map (pretty_thm ctxt) ths)); 

444 

445 

446 

7663  447 
(** default sorts and types **) 
448 

12291  449 
fun def_sort (Context {defs = (_, sorts, _, _), ...}) xi = Vartab.lookup (sorts, xi); 
7663  450 

14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

451 
fun def_type (Context {binds, defs = (types, _, _, _), ...}) pattern xi = 
7663  452 
(case Vartab.lookup (types, xi) of 
453 
None => 

14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

454 
if pattern then None else 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

455 
(case Vartab.lookup (binds, xi) of 
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

456 
Some (Some (_, T)) => Some (TypeInfer.polymorphicT T) 
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

457 
 _ => None) 
7663  458 
 some => some); 
459 

12504  460 
fun default_type (Context {defs = (types, _, _, _), ...}) x = Vartab.lookup (types, (x, ~1)); 
461 
fun used_types (Context {defs = (_, _, used, _), ...}) = used; 

12414  462 

7663  463 

5819  464 

465 
(** prepare types **) 

466 

9504  467 
local 
468 

469 
fun read_typ_aux read ctxt s = 

12093  470 
transform_error (read (syn_of ctxt) (sign_of ctxt, def_sort ctxt)) s 
7663  471 
handle ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt); 
5819  472 

10554  473 
fun cert_typ_aux cert ctxt raw_T = 
474 
cert (sign_of ctxt) raw_T 

475 
handle TYPE (msg, _, _) => raise CONTEXT (msg, ctxt); 

9504  476 

477 
in 

478 

14287
f630017ed01c
Isar: where attribute supports instantiation of type variables.
ballarin
parents:
14257
diff
changeset

479 
(* Read/certify type, using default sort information from context. *) 
f630017ed01c
Isar: where attribute supports instantiation of type variables.
ballarin
parents:
14257
diff
changeset

480 

14780  481 
val read_typ = read_typ_aux Sign.read_typ'; 
482 
val read_typ_raw = read_typ_aux Sign.read_typ_raw'; 

483 
val cert_typ = cert_typ_aux Sign.certify_typ; 

484 
val cert_typ_raw = cert_typ_aux Sign.certify_typ_raw; 

9504  485 

486 
end; 

487 

5819  488 

7679  489 
(* internalize Skolem constants *) 
490 

10583  491 
fun lookup_skolem ctxt x = assoc (fixes_of ctxt, x); 
492 
fun get_skolem ctxt x = if_none (lookup_skolem ctxt x) x; 

7679  493 

12504  494 
fun no_skolem internal ctxt x = 
9291
23705d14be8f
"_i" arguments now expected to have skolems already internalized;
wenzelm
parents:
9274
diff
changeset

495 
if can Syntax.dest_skolem x then 
7679  496 
raise CONTEXT ("Illegal reference to internal Skolem constant: " ^ quote x, ctxt) 
12504  497 
else if not internal andalso can Syntax.dest_internal x then 
9291
23705d14be8f
"_i" arguments now expected to have skolems already internalized;
wenzelm
parents:
9274
diff
changeset

498 
raise CONTEXT ("Illegal reference to internal variable: " ^ quote x, ctxt) 
7679  499 
else x; 
500 

14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

501 
fun intern_skolem ctxt internal = 
7679  502 
let 
503 
fun intern (t as Free (x, T)) = 

14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

504 
if internal x then t 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

505 
else 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

506 
(case lookup_skolem ctxt (no_skolem false ctxt x) of 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

507 
Some x' => Free (x', T) 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

508 
 None => t) 
7679  509 
 intern (t $ u) = intern t $ intern u 
510 
 intern (Abs (x, T, t)) = Abs (x, T, intern t) 

511 
 intern a = a; 

512 
in intern end; 

513 

514 

9133  515 
(* externalize Skolem constants  for printing purposes only *) 
516 

517 
fun extern_skolem ctxt = 

518 
let 

519 
val rev_fixes = map Library.swap (fixes_of ctxt); 

520 

521 
fun extern (t as Free (x, T)) = 

522 
(case assoc (rev_fixes, x) of 

10583  523 
Some x' => Free (if lookup_skolem ctxt x' = Some x then x' else NameSpace.hidden x', T) 
9133  524 
 None => t) 
525 
 extern (t $ u) = extern t $ extern u 

526 
 extern (Abs (x, T, t)) = Abs (x, T, extern t) 

527 
 extern a = a; 

528 
in extern end 

529 

8096  530 

5819  531 
(** prepare terms and propositions **) 
532 

533 
(* 

534 
(1) read / certify wrt. signature of context 

535 
(2) intern Skolem constants 

536 
(3) expand term bindings 

537 
*) 

538 

539 

540 
(* read / certify wrt. signature *) (*exception ERROR*) (*exception TERM*) 

541 

14828  542 
fun read_def_termTs freeze pp syn sg (types, sorts, used) sTs = 
14901  543 
Sign.read_def_terms' pp (Sign.is_logtype sg) syn (sg, types, sorts) used freeze sTs; 
5874  544 

14828  545 
fun read_def_termT freeze pp syn sg defs sT = 
546 
apfst hd (read_def_termTs freeze pp syn sg defs [sT]); 

547 

548 
fun read_term_sg freeze pp syn sg defs s = 

549 
#1 (read_def_termT freeze pp syn sg defs (s, TypeInfer.logicT)); 

5874  550 

14828  551 
fun read_prop_sg freeze pp syn sg defs s = 
552 
#1 (read_def_termT freeze pp syn sg defs (s, propT)); 

12072
4281198fb8cd
local syntax: add_syntax, proper read/pretty functions;
wenzelm
parents:
12066
diff
changeset

553 

14828  554 
fun read_terms_sg freeze pp syn sg defs = 
555 
#1 o read_def_termTs freeze pp syn sg defs o map (rpair TypeInfer.logicT); 

12072
4281198fb8cd
local syntax: add_syntax, proper read/pretty functions;
wenzelm
parents:
12066
diff
changeset

556 

14828  557 
fun read_props_sg freeze pp syn sg defs = 
558 
#1 o read_def_termTs freeze pp syn sg defs o map (rpair propT); 

5819  559 

560 

14828  561 
fun cert_term_sg pp sg t = #1 (Sign.certify_term pp sg t); 
5819  562 

14828  563 
fun cert_prop_sg pp sg tm = 
564 
let val (t, T, _) = Sign.certify_term pp sg tm 

10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

565 
in if T = propT then t else raise TERM ("Term not of type prop", [t]) end; 
5819  566 

567 

568 
(* norm_term *) 

569 

570 
(*beta normal form for terms (not eta normal form), chase variables in 

571 
bindings environment (code taken from Pure/envir.ML)*) 

572 

8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

573 
fun unifyT ctxt (T, U) = 
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

574 
let val maxidx = Int.max (Term.maxidx_of_typ T, Term.maxidx_of_typ U) 
12530  575 
in #1 (Type.unify (Sign.tsig_of (sign_of ctxt)) (Vartab.empty, maxidx) (T, U)) end; 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

576 

14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

577 
fun norm_term (ctxt as Context {binds, ...}) schematic = 
5819  578 
let 
579 
(*raised when norm has no effect on a term, to do sharing instead of copying*) 

580 
exception SAME; 

581 

582 
fun norm (t as Var (xi, T)) = 

583 
(case Vartab.lookup (binds, xi) of 

7606  584 
Some (Some (u, U)) => 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

585 
let 
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

586 
val env = unifyT ctxt (T, U) handle Type.TUNIFY => 
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13629
diff
changeset

587 
raise TYPE ("norm_term: illtyped variable assignment", [T, U], [t, u]); 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

588 
val u' = Term.subst_TVars_Vartab env u; 
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

589 
in norm u' handle SAME => u' end 
10554  590 
 _ => 
591 
if schematic then raise SAME 

592 
else raise CONTEXT ("Unbound schematic variable: " ^ Syntax.string_of_vname xi, ctxt)) 

5819  593 
 norm (Abs (a, T, body)) = Abs (a, T, norm body) 
594 
 norm (Abs (_, _, body) $ t) = normh (subst_bound (t, body)) 

595 
 norm (f $ t) = 

596 
((case norm f of 

597 
Abs (_, _, body) => normh (subst_bound (t, body)) 

598 
 nf => nf $ (norm t handle SAME => t)) handle SAME => f $ norm t) 

599 
 norm _ = raise SAME 

600 
and normh t = norm t handle SAME => t 

601 
in normh end; 

602 

603 

6550  604 
(* dummy patterns *) 
605 

9540  606 
fun prepare_dummies t = #2 (Term.replace_dummy_patterns (1, t)); 
6762  607 

9540  608 
fun reject_dummies ctxt t = Term.no_dummy_patterns t 
609 
handle TERM _ => raise CONTEXT ("Illegal dummy pattern(s) in term", ctxt); 

6550  610 

611 

5819  612 
(* read terms *) 
613 

10554  614 
local 
615 

14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

616 
fun append_env e1 e2 x = (case e2 x of None => e1 x  some => some); 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

617 

ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

618 
fun gen_read' read app pattern dummies schematic 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

619 
ctxt internal more_types more_sorts more_used s = 
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13629
diff
changeset

620 
let 
14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

621 
val types = append_env (def_type ctxt pattern) more_types; 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

622 
val sorts = append_env (def_sort ctxt) more_sorts; 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

623 
val used = used_types ctxt @ more_used; 
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13629
diff
changeset

624 
in 
14828  625 
(transform_error (read (pp ctxt) (syn_of ctxt) (sign_of ctxt) (types, sorts, used)) s 
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13629
diff
changeset

626 
handle TERM (msg, _) => raise CONTEXT (msg, ctxt) 
14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

627 
 ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt)) 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

628 
> app (intern_skolem ctxt internal) 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

629 
> app (if pattern then I else norm_term ctxt schematic) 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

630 
> app (if pattern then prepare_dummies else if dummies then I else reject_dummies ctxt) 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

631 
end; 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

632 

ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

633 
fun gen_read read app pattern dummies schematic ctxt = 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

634 
gen_read' read app pattern dummies schematic ctxt (K false) (K None) (K None) []; 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

635 

10554  636 
in 
637 

14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

638 
val read_termTs = gen_read' (read_def_termTs false) (apfst o map) false false false; 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

639 
val read_termTs_schematic = gen_read' (read_def_termTs false) (apfst o map) false false true; 
8096  640 

14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

641 
fun read_term_pats T ctxt = 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

642 
#1 o gen_read (read_def_termTs false) (apfst o map) true false false ctxt o map (rpair T); 
8096  643 
val read_prop_pats = read_term_pats propT; 
644 

14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

645 
fun read_term_liberal ctxt = 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

646 
gen_read' (read_term_sg true) I false false false ctxt (K true) (K None) (K None) []; 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

647 

ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

648 
val read_term = gen_read (read_term_sg true) I false false false; 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

649 
val read_term_dummies = gen_read (read_term_sg true) I false true false; 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

650 
val read_prop = gen_read (read_prop_sg true) I false false false; 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

651 
val read_prop_schematic = gen_read (read_prop_sg true) I false false true; 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

652 
val read_terms = gen_read (read_terms_sg true) map false false false; 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

653 
fun read_props schematic = gen_read (read_props_sg true) map false false schematic; 
5819  654 

10554  655 
end; 
656 

5819  657 

658 
(* certify terms *) 

659 

10554  660 
local 
661 

14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

662 
fun gen_cert cert pattern schematic ctxt t = t 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

663 
> (if pattern then I else norm_term ctxt schematic) 
14828  664 
> (fn t' => cert (pp ctxt) (sign_of ctxt) t' 
665 
handle TERM (msg, _) => raise CONTEXT (msg, ctxt)); 

5819  666 

10554  667 
in 
8096  668 

10554  669 
val cert_term = gen_cert cert_term_sg false false; 
670 
val cert_prop = gen_cert cert_prop_sg false false; 

671 
val cert_props = map oo gen_cert cert_prop_sg false; 

672 

673 
fun cert_term_pats _ = map o gen_cert cert_term_sg true false; 

674 
val cert_prop_pats = map o gen_cert cert_prop_sg true false; 

675 

676 
end; 

5819  677 

678 

679 
(* declare terms *) 

680 

10381  681 
local 
682 

5819  683 
val ins_types = foldl_aterms 
684 
(fn (types, Free (x, T)) => Vartab.update (((x, ~1), T), types) 

685 
 (types, Var v) => Vartab.update (v, types) 

686 
 (types, _) => types); 

687 

688 
val ins_sorts = foldl_types (foldl_atyps 

689 
(fn (sorts, TFree (x, S)) => Vartab.update (((x, ~1), S), sorts) 

690 
 (sorts, TVar v) => Vartab.update (v, sorts) 

691 
 (sorts, _) => sorts)); 

692 

8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

693 
val ins_used = foldl_term_types (fn t => foldl_atyps 
12504  694 
(fn (used, TFree (x, _)) => x ins_string used 
695 
 (used, _) => used)); 

12291  696 

697 
val ins_occs = foldl_term_types (fn t => foldl_atyps 

698 
(fn (tab, TFree (x, _)) => Symtab.update_multi ((x, t), tab)  (tab, _) => tab)); 

5819  699 

7663  700 
fun ins_skolem def_ty = foldr 
5994  701 
(fn ((x, x'), types) => 
7663  702 
(case def_ty x' of 
5994  703 
Some T => Vartab.update (((x, ~1), T), types) 
704 
 None => types)); 

705 

15452  706 
fun map_defaults f = map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs, delta, delta_count) => 
707 
(thy, syntax, data, asms, binds, thms, cases, f defs, delta, delta_count)); 

5819  708 

10381  709 
fun declare_syn (ctxt, t) = 
5819  710 
ctxt 
12291  711 
> map_defaults (fn (types, sorts, used, occ) => (ins_types (types, t), sorts, used, occ)) 
712 
> map_defaults (fn (types, sorts, used, occ) => (types, ins_sorts (sorts, t), used, occ)) 

713 
> map_defaults (fn (types, sorts, used, occ) => (types, sorts, ins_used (used, t), occ)); 

10381  714 

12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

715 
fun declare_occ (ctxt as Context {asms = (_, fixes), ...}, t) = 
10381  716 
declare_syn (ctxt, t) 
12291  717 
> map_defaults (fn (types, sorts, used, occ) => (types, sorts, used, ins_occs (occ, t))) 
718 
> map_defaults (fn (types, sorts, used, occ) => 

719 
(ins_skolem (fn x => Vartab.lookup (types, (x, ~1))) (fixes, types), sorts, used, occ)); 

5819  720 

10381  721 
in 
5819  722 

10381  723 
fun declare_term t ctxt = declare_occ (ctxt, t); 
724 
fun declare_terms ts ctxt = foldl declare_occ (ctxt, ts); 

12130
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

725 
fun declare_terms_syntax ts ctxt = foldl declare_syn (ctxt, ts); 
10381  726 

727 
end; 

5819  728 

729 

8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

730 

90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

731 
(** HindleyMilner polymorphism **) 
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

732 

7925  733 
(* warn_extra_tfrees *) 
734 

12130
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

735 
fun warn_extra_tfrees 
12291  736 
(ctxt1 as Context {defs = (_, _, _, occ1), ...}) 
737 
(ctxt2 as Context {defs = (_, _, _, occ2), ...}) = 

12130
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

738 
let 
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

739 
fun known_tfree a (Type (_, Ts)) = exists (known_tfree a) Ts 
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

740 
 known_tfree a (TFree (a', _)) = a = a' 
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

741 
 known_tfree _ _ = false; 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

742 

12130
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

743 
val extras = 
12291  744 
Library.gen_rems Library.eq_fst (Symtab.dest occ2, Symtab.dest occ1) 
12130
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

745 
> map (fn (a, ts) => map (pair a) (mapfilter (try (#1 o Term.dest_Free)) ts)) > flat 
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

746 
> mapfilter (fn (a, x) => 
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

747 
(case def_type ctxt1 false (x, ~1) of None => Some (a, x) 
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

748 
 Some T => if known_tfree a T then None else Some (a, x))); 
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

749 
val tfrees = map #1 extras > Library.sort_strings > Library.unique_strings; 
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

750 
val frees = map #2 extras > Library.sort_strings > Library.unique_strings; 
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

751 
in 
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

752 
if null extras then () 
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

753 
else warning ("Just introduced free type variable(s): " ^ commas tfrees ^ " in " ^ 
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

754 
space_implode " or " frees); 
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

755 
ctxt2 
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

756 
end; 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

757 

90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

758 

90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

759 
(* generalize type variables *) 
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

760 

12550
32843ad8160a
generalize type variables properly: start with occurrences in objects
wenzelm
parents:
12530
diff
changeset

761 
fun generalize_tfrees inner outer = 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

762 
let 
12057  763 
val extra_fixes = fixed_names_of inner \\ fixed_names_of outer; 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

764 
fun still_fixed (Free (x, _)) = not (x mem_string extra_fixes) 
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

765 
 still_fixed _ = false; 
12550
32843ad8160a
generalize type variables properly: start with occurrences in objects
wenzelm
parents:
12530
diff
changeset

766 
val occs_inner = type_occs inner; 
32843ad8160a
generalize type variables properly: start with occurrences in objects
wenzelm
parents:
12530
diff
changeset

767 
val occs_outer = type_occs outer; 
32843ad8160a
generalize type variables properly: start with occurrences in objects
wenzelm
parents:
12530
diff
changeset

768 
fun add (gen, a) = 
32843ad8160a
generalize type variables properly: start with occurrences in objects
wenzelm
parents:
12530
diff
changeset

769 
if is_some (Symtab.lookup (occs_outer, a)) orelse 
32843ad8160a
generalize type variables properly: start with occurrences in objects
wenzelm
parents:
12530
diff
changeset

770 
exists still_fixed (Symtab.lookup_multi (occs_inner, a)) 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

771 
then gen else a :: gen; 
12550
32843ad8160a
generalize type variables properly: start with occurrences in objects
wenzelm
parents:
12530
diff
changeset

772 
in fn tfrees => foldl add ([], tfrees) end; 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

773 

12550
32843ad8160a
generalize type variables properly: start with occurrences in objects
wenzelm
parents:
12530
diff
changeset

774 
fun generalize inner outer ts = 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

775 
let 
12550
32843ad8160a
generalize type variables properly: start with occurrences in objects
wenzelm
parents:
12530
diff
changeset

776 
val tfrees = generalize_tfrees inner outer (foldr Term.add_term_tfree_names (ts, [])); 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

777 
fun gen (x, S) = if x mem_string tfrees then TVar ((x, 0), S) else TFree (x, S); 
12550
32843ad8160a
generalize type variables properly: start with occurrences in objects
wenzelm
parents:
12530
diff
changeset

778 
in map (Term.map_term_types (Term.map_type_tfree gen)) ts end; 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

779 

90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

780 

9553  781 

782 
(** export theorems **) 

8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

783 

90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

784 
fun get_free x (None, t as Free (y, _)) = if x = y then Some t else None 
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

785 
 get_free _ (opt, _) = opt; 
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

786 

90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

787 
fun find_free t x = foldl_aterms (get_free x) (None, t); 
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

788 

13415  789 
fun export_view view is_goal inner outer = 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

790 
let 
12550
32843ad8160a
generalize type variables properly: start with occurrences in objects
wenzelm
parents:
12530
diff
changeset

791 
val gen = generalize_tfrees inner outer; 
12057  792 
val fixes = fixed_names_of inner \\ fixed_names_of outer; 
793 
val asms = Library.drop (length (assumptions_of outer), assumptions_of inner); 

11816  794 
val exp_asms = map (fn (cprops, exp) => exp is_goal cprops) asms; 
12550
32843ad8160a
generalize type variables properly: start with occurrences in objects
wenzelm
parents:
12530
diff
changeset

795 
in fn thm => thm 
12804  796 
> Tactic.norm_hhf_rule 
11816  797 
> Seq.EVERY (rev exp_asms) 
13415  798 
> Seq.map (Drule.implies_intr_list view) 
11816  799 
> Seq.map (fn rule => 
800 
let 

801 
val {sign, prop, ...} = Thm.rep_thm rule; 

802 
val frees = map (Thm.cterm_of sign) (mapfilter (find_free prop) fixes); 

12550
32843ad8160a
generalize type variables properly: start with occurrences in objects
wenzelm
parents:
12530
diff
changeset

803 
val tfrees = gen (Term.add_term_tfree_names (prop, [])); 
11816  804 
in 
805 
rule 

806 
> Drule.forall_intr_list frees 

12804  807 
> Tactic.norm_hhf_rule 
12504  808 
> (#1 o Drule.tvars_intr_list tfrees) 
11816  809 
end) 
810 
end; 

8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

811 

13415  812 
val export = export_view []; 
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13378
diff
changeset

813 

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

814 
fun export_standard view inner outer = 
13415  815 
let val exp = export_view view false inner outer in 
13378  816 
fn th => 
817 
(case Seq.pull (exp th) of 

818 
Some (th', _) => th' > Drule.local_standard 

819 
 None => raise CONTEXT ("Internal failure while exporting theorem", inner)) 

820 
end; 

12704  821 

7925  822 

5819  823 

824 
(** bindings **) 

825 

826 
(* update_binds *) 

827 

7606  828 
fun del_bind (ctxt, xi) = 
829 
ctxt 

15452  830 
> map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs, delta, delta_count) => 
831 
(thy, syntax, data, asms, Vartab.update ((xi, None), binds), thms, cases, defs, delta, delta_count)); 

7606  832 

8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

833 
fun upd_bind (ctxt, ((x, i), t)) = 
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

834 
let 
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

835 
val T = Term.fastype_of t; 
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

836 
val t' = 
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

837 
if null (Term.term_tvars t \\ Term.typ_tvars T) then t 
8637  838 
else Var ((x ^ "_has_extra_type_vars_on_rhs", i), T); 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

839 
in 
5819  840 
ctxt 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

841 
> declare_term t' 
15452  842 
> map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs, delta, delta_count) => 
843 
(thy, syntax, data, asms, Vartab.update (((x, i), Some (t', T)), binds), thms, cases, defs, delta, delta_count)) 

5819  844 
end; 
845 

7606  846 
fun del_upd_bind (ctxt, (xi, None)) = del_bind (ctxt, xi) 
847 
 del_upd_bind (ctxt, (xi, Some t)) = upd_bind (ctxt, (xi, t)); 

848 

5819  849 
fun update_binds bs ctxt = foldl upd_bind (ctxt, bs); 
7606  850 
fun delete_update_binds bs ctxt = foldl del_upd_bind (ctxt, bs); 
851 

5819  852 

8096  853 
(* simult_matches *) 
854 

8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

855 
fun simult_matches ctxt [] = [] 
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

856 
 simult_matches ctxt pairs = 
8096  857 
let 
10554  858 
fun fail () = raise CONTEXT ("Pattern match failed!", ctxt); 
859 

8096  860 
val maxidx = foldl (fn (i, (t1, t2)) => 
861 
Int.max (i, Int.max (Term.maxidx_of_term t1, Term.maxidx_of_term t2))) (~1, pairs); 

10554  862 
val envs = Unify.smash_unifiers (sign_of ctxt, Envir.empty maxidx, 
863 
map swap pairs); (*prefer assignment of variables from patterns*) 

864 
val env = 

8096  865 
(case Seq.pull envs of 
10554  866 
None => fail () 
867 
 Some (env, _) => env); (*ignore further results*) 

12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

868 
val domain = 
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

869 
filter_out Term.is_replaced_dummy_pattern (map #1 (Drule.vars_of_terms (map #1 pairs))); 
10554  870 
val _ = (*may not assign variables from text*) 
12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

871 
if null (map #1 (Envir.alist_of env) inter (map #1 (Drule.vars_of_terms (map #2 pairs)))) 
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

872 
then () else fail (); 
10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

873 
fun norm_bind (xi, t) = if xi mem domain then Some (xi, Envir.norm_term env t) else None; 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

874 
in mapfilter norm_bind (Envir.alist_of env) end; 
8096  875 

876 

877 
(* add_binds(_i) *) 

5819  878 

7925  879 
local 
880 

5819  881 
fun gen_bind prep (ctxt, (xi as (x, _), raw_t)) = 
7606  882 
ctxt > delete_update_binds [(xi, apsome (prep ctxt) raw_t)]; 
5819  883 

8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

884 
fun gen_binds prep binds ctxt = foldl (gen_bind prep) (ctxt, binds); 
7925  885 

10810  886 
in 
887 

10554  888 
fun drop_schematic (b as (xi, Some t)) = if null (Term.term_vars t) then b else (xi, None) 
889 
 drop_schematic b = b; 

890 

5819  891 
val add_binds = gen_binds read_term; 
892 
val add_binds_i = gen_binds cert_term; 

8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

893 

12147  894 
fun auto_bind f ts ctxt = ctxt > add_binds_i (map drop_schematic (f (sign_of ctxt) ts)); 
895 
val auto_bind_goal = auto_bind AutoBind.goal; 

896 
val auto_bind_facts = auto_bind AutoBind.facts; 

7925  897 

898 
end; 

5819  899 

900 

8096  901 
(* match_bind(_i) *) 
5819  902 

8096  903 
local 
904 

10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

905 
fun prep_bind prep_pats (ctxt, (raw_pats, t)) = 
5819  906 
let 
8096  907 
val ctxt' = declare_term t ctxt; 
908 
val pats = prep_pats (fastype_of t) ctxt' raw_pats; 

8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

909 
val binds = simult_matches ctxt' (map (rpair t) pats); 
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

910 
in (ctxt', binds) end; 
7670  911 

10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

912 
fun gen_binds prep_terms prep_pats gen raw_binds ctxt = 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

913 
let 
10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

914 
val ts = prep_terms ctxt (map snd raw_binds); 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

915 
val (ctxt', binds) = 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

916 
apsnd flat (foldl_map (prep_bind prep_pats) (ctxt, map fst raw_binds ~~ ts)); 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

917 
val binds' = 
12550
32843ad8160a
generalize type variables properly: start with occurrences in objects
wenzelm
parents:
12530
diff
changeset

918 
if gen then map #1 binds ~~ generalize ctxt' ctxt (map #2 binds) 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

919 
else binds; 
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

920 
val binds'' = map (apsnd Some) binds'; 
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

921 
in 
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

922 
warn_extra_tfrees ctxt 
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

923 
(if gen then ctxt (*sic!*) > declare_terms (map #2 binds') > add_binds_i binds'' 
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

924 
else ctxt' > add_binds_i binds'') 
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

925 
end; 
8096  926 

927 
in 

5935  928 

10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

929 
val match_bind = gen_binds read_terms read_term_pats; 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

930 
val match_bind_i = gen_binds (map o cert_term) cert_term_pats; 
8096  931 

932 
end; 

5935  933 

934 

10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

935 
(* propositions with patterns *) 
5935  936 

10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

937 
local 
8096  938 

10554  939 
fun prep_propp schematic prep_props prep_pats (context, args) = 
10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

940 
let 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

941 
fun prep ((ctxt, prop :: props), (_, (raw_pats1, raw_pats2))) = 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

942 
let 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

943 
val ctxt' = declare_term prop ctxt; 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

944 
val pats = prep_pats ctxt' (raw_pats1 @ raw_pats2); (*simultaneous type inference!*) 
13629  945 
in ((ctxt', props), (prop, splitAt(length raw_pats1, pats))) end 
10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

946 
 prep _ = sys_error "prep_propp"; 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

947 
val ((context', _), propp) = foldl_map (foldl_map prep) 
10554  948 
((context, prep_props schematic context (flat (map (map fst) args))), args); 
10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

949 
in (context', propp) end; 
5935  950 

10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

951 
fun matches ctxt (prop, (pats1, pats2)) = 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

952 
simult_matches ctxt (map (rpair prop) pats1 @ map (rpair (Logic.strip_imp_concl prop)) pats2); 
8096  953 

10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

954 
fun gen_bind_propp prepp (ctxt, raw_args) = 
8096  955 
let 
10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

956 
val (ctxt', args) = prepp (ctxt, raw_args); 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

957 
val binds = flat (flat (map (map (matches ctxt')) args)); 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

958 
val propss = map (map #1) args; 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

959 

10554  960 
(*generalize result: context evaluated now, binds added later*) 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

961 
val gen = generalize ctxt' ctxt; 
12550
32843ad8160a
generalize type variables properly: start with occurrences in objects
wenzelm
parents:
12530
diff
changeset

962 
fun gen_binds c = c > add_binds_i (map #1 binds ~~ map Some (gen (map #2 binds))); 
10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

963 
in (ctxt' > add_binds_i (map (apsnd Some) binds), (propss, gen_binds)) end; 
8096  964 

10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

965 
in 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

966 

11925  967 
val read_propp = prep_propp false read_props read_prop_pats; 
968 
val cert_propp = prep_propp false cert_props cert_prop_pats; 

10554  969 
val read_propp_schematic = prep_propp true read_props read_prop_pats; 
970 
val cert_propp_schematic = prep_propp true cert_props cert_prop_pats; 

971 

11925  972 
val bind_propp = gen_bind_propp read_propp; 
973 
val bind_propp_i = gen_bind_propp cert_propp; 

974 
val bind_propp_schematic = gen_bind_propp read_propp_schematic; 

10554  975 
val bind_propp_schematic_i = gen_bind_propp cert_propp_schematic; 
6789  976 

10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

977 
end; 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

978 

6789  979 

5819  980 

981 
(** theorems **) 

982 

6091  983 
(* get_thm(s) *) 
5819  984 

9566  985 
(*beware of proper order of evaluation!*) 
13278
b62514fcbcab
print_thms_containing: index variables, refer to local facts as well;
wenzelm
parents:
12863
diff
changeset

986 
fun retrieve_thms f g (ctxt as Context {thy, thms = (_, space, tab, _), ...}) = 
9566  987 
let 
988 
val sg_ref = Sign.self_ref (Theory.sign_of thy); 

989 
val get_from_thy = f thy; 

990 
in 

12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

991 
fn xname => 
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

992 
(case Symtab.lookup (tab, NameSpace.intern space xname) of 
9566  993 
Some (Some ths) => map (Thm.transfer_sg (Sign.deref sg_ref)) ths 
12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

994 
 _ => get_from_thy xname) > g xname 
9566  995 
end; 
5819  996 

9566  997 
val get_thm = retrieve_thms PureThy.get_thms PureThy.single_thm; 
998 
val get_thm_closure = retrieve_thms PureThy.get_thms_closure PureThy.single_thm; 

999 
val get_thms = retrieve_thms PureThy.get_thms (K I); 

1000 
val get_thms_closure = retrieve_thms PureThy.get_thms_closure (K I); 

5819  1001 

1002 

13425
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
13415
diff
changeset

1003 
(* name space operations *) 
12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

1004 

13278
b62514fcbcab
print_thms_containing: index variables, refer to local facts as well;
wenzelm
parents:
12863
diff
changeset

1005 
fun cond_extern (Context {thms = (_, space, _, _), ...}) = NameSpace.cond_extern space; 
12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

1006 

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

1007 
fun qualified q = map_context (fn (thy, syntax, data, asms, binds, 
15452  1008 
(_, space, tab, index), cases, defs, delta, delta_count) => 
1009 
(thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs, delta, delta_count)); 

12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

1010 

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

1011 
fun restore_qualified (Context {thms, ...}) = qualified (#1 thms); 
12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

1012 

13425
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
13415
diff
changeset

1013 
fun hide_thms fully names = 
15452  1014 
map_context (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs, delta, delta_count) => 
13425
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
13415
diff
changeset

1015 
(thy, syntax, data, asms, binds, (q, NameSpace.hide fully (space, names), tab, index), 
15452  1016 
cases, defs, delta, delta_count)); 
13425
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
13415
diff
changeset

1017 

12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

1018 

6091  1019 
(* put_thm(s) *) 
5819  1020 

12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

1021 
fun put_thms ("", _) ctxt = ctxt 
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

1022 
 put_thms (name, ths) ctxt = ctxt > map_context 
15452  1023 
(fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs, delta, delta_count) => 
12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

1024 
if not q andalso NameSpace.is_qualified name then 
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

1025 
raise CONTEXT ("Attempt to declare qualified name " ^ quote name, ctxt) 
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

1026 
else (thy, syntax, data, asms, binds, (q, NameSpace.extend (space, [name]), 
13278
b62514fcbcab
print_thms_containing: index variables, refer to local facts as well;
wenzelm
parents:
12863
diff
changeset

1027 
Symtab.update ((name, Some ths), tab), 
15452  1028 
FactIndex.add (is_known ctxt) (index, (name, ths))), cases, defs, delta, delta_count)); 
5819  1029 

6091  1030 
fun put_thm (name, th) = put_thms (name, [th]); 
5819  1031 

6091  1032 
fun put_thmss [] ctxt = ctxt 
1033 
 put_thmss (th :: ths) ctxt = ctxt > put_thms th > put_thmss ths; 

5819  1034 

1035 

7606  1036 
(* reset_thms *) 
1037 

12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

1038 
fun reset_thms name = 
15452  1039 
map_context (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs, delta, delta_count) => 
13278
b62514fcbcab
print_thms_containing: index variables, refer to local facts as well;
wenzelm
parents:
12863
diff
changeset

1040 
(thy, syntax, data, asms, binds, (q, space, Symtab.update ((name, None), tab), index), 
15452  1041 
cases, defs, delta,delta_count)); 
7606  1042 

1043 

14564  1044 
(* note_thmss *) 
5819  1045 

12711  1046 
local 
1047 

14564  1048 
fun gen_note_thss get (ctxt, ((name, more_attrs), ths_attrs)) = 
5819  1049 
let 
1050 
fun app ((ct, ths), (th, attrs)) = 

12711  1051 
let val (ct', th') = Thm.applys_attributes ((ct, get ctxt th), attrs @ more_attrs) 
1052 
in (ct', th' :: ths) end; 

5819  1053 
val (ctxt', rev_thms) = foldl app ((ctxt, []), ths_attrs); 
9196  1054 
val thms = flat (rev rev_thms); 
6091  1055 
in (ctxt' > put_thms (name, thms), (name, thms)) end; 
5819  1056 

14564  1057 
fun gen_note_thmss get args ctxt = foldl_map (gen_note_thss get) (ctxt, args); 
12711  1058 

1059 
in 

1060 

14564  1061 
val note_thmss = gen_note_thmss get_thms; 
1062 
val note_thmss_i = gen_note_thmss (K I); 

12711  1063 

1064 
end; 

9196  1065 

5819  1066 

1067 

1068 
(** assumptions **) 

1069 

11918
dfdf0798d7b8
added export_assume, export_presume, export_def (from proof.ML);
wenzelm
parents:
11915
diff
changeset

1070 
(* basic exporters *) 
dfdf0798d7b8
added export_assume, export_presume, export_def (from proof.ML);
wenzelm
parents:
11915
diff
changeset

1071 

dfdf0798d7b8
added export_assume, export_presume, export_def (from proof.ML);
wenzelm
parents:
11915
diff
changeset

1072 
fun export_assume true = Seq.single oo Drule.implies_intr_goals 
dfdf0798d7b8
added export_assume, export_presume, export_def (from proof.ML);
wenzelm
parents:
11915
diff
changeset

1073 
 export_assume false = Seq.single oo Drule.implies_intr_list; 
dfdf0798d7b8
added export_assume, export_presume, export_def (from proof.ML);
wenzelm
parents:
11915
diff
changeset

1074 

dfdf0798d7b8
added export_assume, export_presume, export_def (from proof.ML);
wenzelm
parents:
11915
diff
changeset

1075 
fun export_presume _ = export_assume false; 
dfdf0798d7b8
added export_assume, export_presume, export_def (from proof.ML);
wenzelm
parents:
11915
diff
changeset

1076 

dfdf0798d7b8
added export_assume, export_presume, export_def (from proof.ML);
wenzelm
parents:
11915
diff
changeset

1077 

12057  1078 
(* defs *) 
1079 

12066  1080 
fun cert_def ctxt eq = 
12016  1081 
let 
12057  1082 
fun err msg = raise CONTEXT (msg ^ 
1083 
"\nThe error(s) above occurred in local definition: " ^ string_of_term ctxt eq, ctxt); 

1084 
val (lhs, rhs) = Logic.dest_equals (Term.strip_all_body eq) 

1085 
handle TERM _ => err "Not a metaequality (==)"; 

12086  1086 
val (f, xs) = Term.strip_comb lhs; 
1087 
val (c, _) = Term.dest_Free f handle TERM _ => 

13430  1088 
err "Head of lhs must be a free/fixed variable"; 
12057  1089 

12086  1090 
fun is_free (Free (x, _)) = not (is_fixed ctxt x) 
1091 
 is_free _ = false; 

1092 
val extra_frees = filter is_free (term_frees rhs) \\ xs; 

12016  1093 
in 
12086  1094 
conditional (not (forall (is_Bound orf is_free) xs andalso null (duplicates xs))) (fn () => 
13430  1095 
err "Arguments of lhs must be distinct free/bound variables"); 
12086  1096 
conditional (f mem Term.term_frees rhs) (fn () => 
1097 
err "Element to be defined occurs on rhs"); 

1098 
conditional (not (null extra_frees)) (fn () => 

1099 
err ("Extra free variables on rhs: " ^ commas_quote (map (#1 o dest_Free) extra_frees))); 

1100 
(c, Term.list_all_free (mapfilter (try Term.dest_Free) xs, eq)) 

12057  1101 
end; 
1102 

1103 
fun head_of_def cprop = 

1104 
#1 (Term.strip_comb (#1 (Logic.dest_equals (Term.strip_all_body (Thm.term_of cprop))))) 

1105 
> Thm.cterm_of (Thm.sign_of_cterm cprop); 

11918
dfdf0798d7b8
added export_assume, export_presume, export_def (from proof.ML);
wenzelm
parents:
11915
diff
changeset

1106 

dfdf0798d7b8
added export_assume, export_presume, export_def (from proof.ML);
wenzelm
parents:
11915
diff
changeset

1107 
fun export_def _ cprops thm = 
dfdf0798d7b8
added export_assume, export_presume, export_def (from proof.ML);
wenzelm
parents:
11915
diff
changeset

1108 
thm 
dfdf0798d7b8
added export_assume, export_presume, export_def (from proof.ML);
wenzelm
parents:
11915
diff
changeset

1109 
> Drule.implies_intr_list cprops 
12057  1110 
> Drule.forall_intr_list (map head_of_def cprops) 
11918
dfdf0798d7b8
added export_assume, export_presume, export_def (from proof.ML);
wenzelm
parents:
11915
diff
changeset

1111 
> Drule.forall_elim_vars 0 
dfdf0798d7b8
added export_assume, export_presume, export_def (from proof.ML);
wenzelm
parents:
11915
diff
changeset

1112 
> RANGE (replicate (length cprops) (Tactic.rtac Drule.reflexive_thm)) 1; 
dfdf0798d7b8
added export_assume, export_presume, export_def (from proof.ML);
wenzelm
parents:
11915
diff
changeset

1113 

dfdf0798d7b8
added export_assume, export_presume, export_def (from proof.ML);
wenzelm
parents:
11915
diff
changeset

1114 

5819  1115 
(* assume *) 
1116 

7270  1117 
local 
6797  1118 

10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

1119 
fun add_assm (ctxt, ((name, attrs), props)) = 
5819  1120 
let 
10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

1121 
val cprops = map (Thm.cterm_of (sign_of ctxt)) props; 
12804  1122 
val asms = map (Tactic.norm_hhf_rule o Thm.assume) cprops; 
5919  1123 

1124 
val ths = map (fn th => ([th], [])) asms; 

10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

1125 
val (ctxt', [(_, thms)]) = 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

1126 
ctxt 
12147  1127 
> auto_bind_facts props 
14564  1128 
> note_thmss_i [((name, attrs), ths)]; 
10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

1129 
in (ctxt', (cprops, (name, asms), (name, thms))) end; 
5819  1130 

9470  1131 
fun gen_assms prepp exp args ctxt = 
1132 
let 

10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

1133 
val (ctxt1, propss) = prepp (ctxt, map snd args); 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

1134 
val (ctxt2, results) = foldl_map add_assm (ctxt1, map fst args ~~ propss); 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

1135 

9470  1136 
val cprops = flat (map #1 results); 
1137 
val asmss = map #2 results; 

1138 
val thmss = map #3 results; 

12072
4281198fb8cd
local syntax: add_syntax, proper read/pretty functions;
wenzelm
parents:
12066
diff
changeset

1139 
val ctxt3 = ctxt2 > map_context 
15452  1140 
(fn (thy, syntax, data, ((asms_ct, asms_th), fixes), binds, thms, cases, defs, delta, delta_count) => 
12072
4281198fb8cd
local syntax: add_syntax, proper read/pretty functions;
wenzelm
parents:
12066
diff
changeset

1141 
(thy, syntax, data, ((asms_ct @ [(cprops, exp)], asms_th @ asmss), fixes), binds, thms, 
15452  1142 
cases, defs, delta, delta_count)); 
11925  1143 
val ctxt4 = ctxt3 > put_thms ("prems", prems_of ctxt3); 
1144 
in (warn_extra_tfrees ctxt ctxt4, thmss) end; 

5819  1145 

7270  1146 
in 
1147 

8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

1148 
val assume = gen_assms (apsnd #1 o bind_propp); 
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

1149 
val assume_i = gen_assms (apsnd #1 o bind_propp_i); 
7270  1150 

1151 
end; 

5819  1152 

1153 

8096  1154 
(* variables *) 
1155 

10381  1156 
local 
1157 

14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

1158 
fun prep_vars prep_typ internal liberal (ctxt, (xs, raw_T)) = 
8096  1159 
let 
12504  1160 
fun cond_tvars T = 
1161 
if internal then T 

1162 
else Type.no_tvars T handle TYPE (msg, _, _) => raise CONTEXT (msg, ctxt); 

1163 

14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

1164 
val _ = if liberal then () else 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

1165 
(case filter (not o Syntax.is_identifier) (map (no_skolem internal ctxt) xs) of 
8096  1166 
[] => ()  bads => raise CONTEXT ("Bad variable name(s): " ^ commas_quote bads, ctxt)); 
1167 

12504  1168 
val opt_T = apsome (cond_tvars o prep_typ ctxt) raw_T; 
8096  1169 
val T = if_none opt_T TypeInfer.logicT; 
12130
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

1170 
val ctxt' = ctxt > declare_terms_syntax (map (fn x => Free (x, T)) xs); 
8096  1171 
in (ctxt', (xs, opt_T)) end; 
1172 

10381  1173 
in 
1174 

14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

1175 
val read_vars = prep_vars read_typ false false; 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

1176 
val cert_vars = prep_vars cert_typ true false; 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

1177 
val read_vars_liberal = prep_vars read_typ false true; 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

1178 
val cert_vars_liberal = prep_vars cert_typ true true; 
8096  1179 

10381  1180 
end; 
1181 

8096  1182 

5819  1183 
(* fix *) 
1184 

8096  1185 
local 
1186 

12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

1187 
fun map_fixes f = 
15452  1188 
map_context (fn (thy, syntax, data, (assumes, fixes), binds, thms, cases, defs, delta, delta_count) => 
1189 
(thy, syntax, data, (assumes, f fixes), binds, thms, cases, defs, delta, delta_count)); 

5819  1190 

11925  1191 
fun err_dups ctxt xs = raise CONTEXT ("Duplicate variable(s): " ^ commas_quote xs, ctxt); 
1192 

12130
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

1193 
val declare = 
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

1194 
declare_terms_syntax o mapfilter (fn (_, None) => None  (x, Some T) => Some (Free (x, T))); 
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

1195 

30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

1196 
fun add_vars xs Ts ctxt = 
12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

1197 
let val xs' = Term.variantlist (map Syntax.skolem xs, map #2 (fixes_of ctxt)) in 
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

1198 
ctxt 
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

1199 
> declare (xs' ~~ Ts) 
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

1200 
> map_fixes (fn fixes => (xs ~~ xs') @ fixes) 
12130
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

1201 
end; 
11925  1202 

12130
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

1203 
fun add_vars_direct xs Ts ctxt = 
12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

1204 
ctxt 
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

1205 
> declare (xs ~~ Ts) 
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

1206 
> map_fixes (fn fixes => 
12130
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

1207 
(case xs inter_string map #1 fixes of 
12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

1208 
[] => (xs ~~ xs) @ fixes 
12130
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

1209 
 dups => err_dups ctxt dups)); 
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

1210 

11925  1211 

1212 
fun gen_fix prep add raw_vars ctxt = 

8096  1213 
let 
1214 
val (ctxt', varss) = foldl_map prep (ctxt, raw_vars); 

12130
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

1215 
val vars = rev (flat (map (fn (xs, T) => map (rpair T) xs) varss)); 
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

1216 
val xs = map #1 vars; 
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

1217 
val Ts = map #2 vars; 
8096  1218 
in 
11925  1219 
(case Library.duplicates xs of [] => ()  dups => err_dups ctxt dups); 
12130
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

1220 
ctxt' > add xs Ts 
8096  1221 
end; 
5819  1222 

12576
9fd10052c3f7
added add_fixes: derives mssing type scheme from mixfix;
wenzelm
parents:
12550
diff
changeset

1223 
fun prep_type (x, None, Some mx) = ([x], Some (mixfix_type mx)) 
9fd10052c3f7
added add_fixes: derives mssing type scheme from mixfix;
wenzelm
parents:
12550
diff
changeset

1224 
 prep_type (x, opt_T, _) = ([x], opt_T); 
9fd10052c3f7
added add_fixes: derives mssing type scheme from mixfix;
wenzelm
parents:
12550
diff
changeset

1225 

8096  1226 
in 
7679  1227 

11925  1228 
val fix = gen_fix read_vars add_vars; 
1229 
val fix_i = gen_fix cert_vars add_vars; 

14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

1230 

ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

1231 
fun fix_direct liberal = 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

1232 
gen_fix (if liberal then cert_vars_liberal else cert_vars) add_vars_direct; 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

1233 

ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

1234 
fun add_fixes decls = add_syntax decls o fix_direct false (map prep_type decls); 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

1235 
fun add_fixes_liberal decls = add_syntax decls o fix_direct true (map prep_type decls); 
8096  1236 

1237 
end; 

5819  1238 

12048  1239 
fun fix_frees ts ctxt = 
1240 
let 

12504  1241 
val frees = foldl Term.add_frees ([], ts); 
12057  1242 
fun new (x, T) = if is_fixed ctxt x then None else Some ([x], Some T); 
14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

1243 
in fix_direct false (rev (mapfilter new frees)) ctxt end; 
12016  1244 

6895  1245 

9291
23705d14be8f
"_i" arguments now expected to have skolems already internalized;
wenzelm
parents:
9274
diff
changeset

1246 
(*Note: improper use may result in variable capture / dynamic scoping!*) 
23705d14be8f
"_i" arguments now expected to have skolems already internalized;
wenzelm
parents:
9274
diff
changeset

1247 
fun bind_skolem ctxt xs = 
23705d14be8f
"_i" arguments now expected to have skolems already internalized;
wenzelm
parents:
9274
diff
changeset

1248 
let 
23705d14be8f
"_i" arguments now expected to have skolems already internalized;
wenzelm
parents:
9274
diff
changeset

1249 
val ctxt' = ctxt > fix_i [(xs, None)]; 
23705d14be8f
"_i" arguments now expected to have skolems already internalized;
wenzelm
parents:
9274
diff
changeset

1250 
fun bind (t as Free (x, T)) = 
23705d14be8f
"_i" arguments now expected to have skolems already internalized;
wenzelm
parents:
9274
diff
changeset

1251 
if x mem_string xs then 
10583  1252 
(case lookup_skolem ctxt' x of Some x' => Free (x', T)  None => t) 
9291
23705d14be8f
"_i" arguments now expected to have skolems already internalized;
wenzelm
parents:
9274
diff
changeset

1253 
else t 
23705d14be8f
"_i" arguments now expected to have skolems already internalized;
wenzelm
parents:
9274
diff
changeset

1254 
 bind (t $ u) = bind t $ bind u 
23705d14be8f
"_i" arguments now expected to have skolems already internalized;
wenzelm
parents:
9274
diff
changeset

1255 
 bind (Abs (x, T, t)) = Abs (x, T, bind t) 
23705d14be8f
"_i" arguments now expected to have skolems already internalized;
wenzelm
parents:
9274
diff
changeset

1256 
 bind a = a; 
23705d14be8f
"_i" arguments now expected to have skolems already internalized;
wenzelm
parents:
9274
diff
changeset

1257 
in bind end; 
23705d14be8f
"_i" arguments now expected to have skolems already internalized;
wenzelm
parents:
9274
diff
changeset

1258 

23705d14be8f
"_i" arguments now expected to have skolems already internalized;
wenzelm
parents:
9274
diff
changeset

1259 

5819  1260 

8373
e7237c8fe29e
handling of local contexts: print_cases, get_case, add_cases;
wenzelm
parents:
8186
diff
changeset

1261 
(** cases **) 
e7237c8fe29e
handling of local contexts: print_cases, get_case, add_cases;
wenzelm
parents:
8186
diff
changeset

1262 

11793
5f0ab6f5c280
support impromptu terminology of cases parameters;
wenzelm
parents:
11764
diff
changeset

1263 
fun prep_case ctxt name xs {fixes, assumes, binds} = 
5f0ab6f5c280
support impromptu terminology of cases parameters;
wenzelm
parents:
11764
diff
changeset

1264 
let 
5f0ab6f5c280
support impromptu terminology of cases parameters;
wenzelm
parents:
11764
diff
changeset

1265 
fun replace (opt_x :: xs) ((y, T) :: ys) = (if_none opt_x y, T) :: replace xs ys 
5f0ab6f5c280
support impromptu terminology of cases parameters;
wenzelm
parents:
11764
diff
changeset

1266 
 replace [] ys = ys 
5f0ab6f5c280
support impromptu terminology of cases parameters;
wenzelm
parents:
11764
diff
changeset

1267 
 replace (_ :: _) [] = raise CONTEXT ("Too many parameters for case " ^ quote name, ctxt); 
5f0ab6f5c280
support impromptu terminology of cases parameters;
wenzelm
parents:
11764
diff
changeset

1268 
in 
5f0ab6f5c280
support impromptu terminology of cases parameters;
wenzelm
parents:
11764
diff
changeset

1269 
if null (foldr Term.add_typ_tvars (map snd fixes, [])) andalso 
13426  1270 
null (foldr Term.add_term_vars (flat (map snd assumes), [])) then 
11793
