author  wenzelm 
Tue, 31 Mar 2015 20:07:37 +0200  
changeset 59883  12a89103cae6 
parent 59846  c7b7bca8592c 
child 59884  bbf49d7dfd6f 
permissions  rwrr 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/variable.ML 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

2 
Author: Makarius 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

3 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

4 
Fixed type/term variables and polymorphic term abbreviations. 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

5 
*) 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

6 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

7 
signature VARIABLE = 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

8 
sig 
20303  9 
val names_of: Proof.context > Name.context 
10 
val binds_of: Proof.context > (typ * term) Vartab.table 

24765  11 
val maxidx_of: Proof.context > int 
28625  12 
val sorts_of: Proof.context > sort list 
20303  13 
val constraints_of: Proof.context > typ Vartab.table * sort Vartab.table 
14 
val is_declared: Proof.context > string > bool 

42494  15 
val check_name: binding > string 
20303  16 
val default_type: Proof.context > string > typ option 
17 
val def_type: Proof.context > bool > indexname > typ option 

18 
val def_sort: Proof.context > indexname > sort option 

59646  19 
val declare_maxidx: int > Proof.context > Proof.context 
27280  20 
val declare_names: term > Proof.context > Proof.context 
20303  21 
val declare_constraints: term > Proof.context > Proof.context 
22 
val declare_term: term > Proof.context > Proof.context 

27280  23 
val declare_typ: typ > Proof.context > Proof.context 
20303  24 
val declare_prf: Proofterm.proof > Proof.context > Proof.context 
25 
val declare_thm: thm > Proof.context > Proof.context 

26 
val variant_frees: Proof.context > term list > (string * 'a) list > (string * 'a) list 

30756  27 
val bind_term: indexname * term option > Proof.context > Proof.context 
20303  28 
val expand_binds: Proof.context > term > term 
25325  29 
val lookup_const: Proof.context > string > string option 
25316
17c183417f93
added is_const/declare_const for local scope of fixes/consts;
wenzelm
parents:
25051
diff
changeset

30 
val is_const: Proof.context > string > bool 
25325  31 
val declare_const: string * string > Proof.context > Proof.context 
55635  32 
val next_bound: string * typ > Proof.context > term * Proof.context 
55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

33 
val revert_bounds: Proof.context > term > term 
59798  34 
val is_body: Proof.context > bool 
35 
val set_body: bool > Proof.context > Proof.context 

36 
val restore_body: Proof.context > Proof.context > Proof.context 

59790  37 
val improper_fixes: Proof.context > Proof.context 
38 
val restore_proper_fixes: Proof.context > Proof.context > Proof.context 

39 
val is_improper: Proof.context > string > bool 

42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

40 
val is_fixed: Proof.context > string > bool 
59846  41 
val is_newly_fixed: Proof.context > Proof.context > string > bool 
42493
01430341fc79
more informative markup for fixed variables (via name space entry);
wenzelm
parents:
42488
diff
changeset

42 
val fixed_ord: Proof.context > string * string > order 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

43 
val intern_fixed: Proof.context > string > string 
42493
01430341fc79
more informative markup for fixed variables (via name space entry);
wenzelm
parents:
42488
diff
changeset

44 
val markup_fixed: Proof.context > string > Markup.T 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

45 
val lookup_fixed: Proof.context > string > string option 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

46 
val revert_fixed: Proof.context > string > string 
42482  47 
val add_fixed_names: Proof.context > term > string list > string list 
48 
val add_fixed: Proof.context > term > (string * typ) list > (string * typ) list 

59846  49 
val add_newly_fixed: Proof.context > Proof.context > 
50 
term > (string * typ) list > (string * typ) list 

42482  51 
val add_free_names: Proof.context > term > string list > string list 
52 
val add_frees: Proof.context > term > (string * typ) list > (string * typ) list 

42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

53 
val add_fixes_binding: binding list > Proof.context > string list * Proof.context 
20303  54 
val add_fixes: string list > Proof.context > string list * Proof.context 
55 
val add_fixes_direct: string list > Proof.context > Proof.context 

21369  56 
val auto_fixes: term > Proof.context > Proof.context 
59796  57 
val fix_dummy_patterns: term > Proof.context > term * Proof.context 
20797
c1f0bc7e7d80
renamed Variable.invent_fixes to Variable.variant_fixes;
wenzelm
parents:
20579
diff
changeset

58 
val variant_fixes: string list > Proof.context > string list * Proof.context 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

59 
val dest_fixes: Proof.context > (string * string) list 
20303  60 
val export_terms: Proof.context > Proof.context > term list > term list 
61 
val exportT_terms: Proof.context > Proof.context > term list > term list 

62 
val exportT: Proof.context > Proof.context > thm list > thm list 

63 
val export_prf: Proof.context > Proof.context > Proofterm.proof > Proofterm.proof 

64 
val export: Proof.context > Proof.context > thm list > thm list 

21522  65 
val export_morphism: Proof.context > Proof.context > morphism 
59796  66 
val invent_types: sort list > Proof.context > (string * sort) list * Proof.context 
20303  67 
val importT_inst: term list > Proof.context > ((indexname * sort) * typ) list * Proof.context 
68 
val import_inst: bool > term list > Proof.context > 

69 
(((indexname * sort) * typ) list * ((indexname * typ) * term) list) * Proof.context 

70 
val importT_terms: term list > Proof.context > term list * Proof.context 

71 
val import_terms: bool > term list > Proof.context > term list * Proof.context 

32280
4fb3f426052a
Variable.importT/import: return full instantiations, tuned;
wenzelm
parents:
32199
diff
changeset

72 
val importT: thm list > Proof.context > ((ctyp * ctyp) list * thm list) * Proof.context 
20303  73 
val import_prf: bool > Proofterm.proof > Proof.context > Proofterm.proof * Proof.context 
31794
71af1fd6a5e4
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef  Alice is no longer supported);
wenzelm
parents:
30756
diff
changeset

74 
val import: bool > thm list > Proof.context > 
32280
4fb3f426052a
Variable.importT/import: return full instantiations, tuned;
wenzelm
parents:
32199
diff
changeset

75 
(((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context 
21287  76 
val tradeT: (Proof.context > thm list > thm list) > Proof.context > thm list > thm list 
77 
val trade: (Proof.context > thm list > thm list) > Proof.context > thm list > thm list 

59828
0e9baaf0e0bb
prefer Variable.focus, despite subtle differences of Logic.strip_params vs. Term.strip_all_vars;
wenzelm
parents:
59798
diff
changeset

78 
val focus_params: term > Proof.context > (string list * (string * typ) list) * Proof.context 
42495
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

79 
val focus: term > Proof.context > ((string * (string * typ)) list * term) * Proof.context 
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

80 
val focus_cterm: cterm > Proof.context > ((string * cterm) list * cterm) * Proof.context 
32199  81 
val focus_subgoal: int > thm > Proof.context > ((string * cterm) list * cterm) * Proof.context 
20303  82 
val warn_extra_tfrees: Proof.context > Proof.context > unit 
24694  83 
val polymorphic_types: Proof.context > term list > (indexname * sort) list * term list 
20303  84 
val polymorphic: Proof.context > term list > term list 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

85 
end; 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

86 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

87 
structure Variable: VARIABLE = 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

88 
struct 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

89 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

90 
(** local context data **) 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

91 

59790  92 
type fixes = (string * bool) Name_Space.table; 
50201
c26369c9eda6
Isabellespecific implementation of quasiabstract markup elements  back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49688
diff
changeset

93 
val empty_fixes: fixes = Name_Space.empty_table Markup.fixedN; 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

94 

19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

95 
datatype data = Data of 
59798  96 
{names: Name.context, (*type/term variable names*) 
25325  97 
consts: string Symtab.table, (*consts within the local scope*) 
55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

98 
bounds: int * ((string * typ) * string) list, (*next index, internal name, type, external name*) 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

99 
fixes: fixes, (*term fixes  global name space, intern ~> extern*) 
20102  100 
binds: (typ * term) Vartab.table, (*term bindings*) 
20162  101 
type_occs: string list Symtab.table, (*type variables  possibly within term variables*) 
24765  102 
maxidx: int, (*maximum var index*) 
40124  103 
sorts: sort Ord_List.T, (*declared sort occurrences*) 
20162  104 
constraints: 
20102  105 
typ Vartab.table * (*type constraints*) 
20162  106 
sort Vartab.table}; (*default sorts*) 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

107 

59798  108 
fun make_data (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) = 
109 
Data {names = names, consts = consts, bounds = bounds, fixes = fixes, binds = binds, 

110 
type_occs = type_occs, maxidx = maxidx, sorts = sorts, constraints = constraints}; 

19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

111 

59150  112 
val empty_data = 
59798  113 
make_data (Name.context, Symtab.empty, (0, []), empty_fixes, Vartab.empty, 
59150  114 
Symtab.empty, ~1, [], (Vartab.empty, Vartab.empty)); 
115 

33519  116 
structure Data = Proof_Data 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

117 
( 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

118 
type T = data; 
59150  119 
fun init _ = empty_data; 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

120 
); 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

121 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

122 
fun map_data f = 
59798  123 
Data.map (fn Data {names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints} => 
124 
make_data (f (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints))); 

25316
17c183417f93
added is_const/declare_const for local scope of fixes/consts;
wenzelm
parents:
25051
diff
changeset

125 

17c183417f93
added is_const/declare_const for local scope of fixes/consts;
wenzelm
parents:
25051
diff
changeset

126 
fun map_names f = 
59798  127 
map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => 
128 
(f names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints)); 

19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

129 

25325  130 
fun map_consts f = 
59798  131 
map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => 
132 
(names, f consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints)); 

55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

133 

a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

134 
fun map_bounds f = 
59798  135 
map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => 
136 
(names, consts, f bounds, fixes, binds, type_occs, maxidx, sorts, constraints)); 

20162  137 

25316
17c183417f93
added is_const/declare_const for local scope of fixes/consts;
wenzelm
parents:
25051
diff
changeset

138 
fun map_fixes f = 
59798  139 
map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => 
140 
(names, consts, bounds, f fixes, binds, type_occs, maxidx, sorts, constraints)); 

19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

141 

25316
17c183417f93
added is_const/declare_const for local scope of fixes/consts;
wenzelm
parents:
25051
diff
changeset

142 
fun map_binds f = 
59798  143 
map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => 
144 
(names, consts, bounds, fixes, f binds, type_occs, maxidx, sorts, constraints)); 

24765  145 

25316
17c183417f93
added is_const/declare_const for local scope of fixes/consts;
wenzelm
parents:
25051
diff
changeset

146 
fun map_type_occs f = 
59798  147 
map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => 
148 
(names, consts, bounds, fixes, binds, f type_occs, maxidx, sorts, constraints)); 

19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

149 

25316
17c183417f93
added is_const/declare_const for local scope of fixes/consts;
wenzelm
parents:
25051
diff
changeset

150 
fun map_maxidx f = 
59798  151 
map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => 
152 
(names, consts, bounds, fixes, binds, type_occs, f maxidx, sorts, constraints)); 

28625  153 

154 
fun map_sorts f = 

59798  155 
map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => 
156 
(names, consts, bounds, fixes, binds, type_occs, maxidx, f sorts, constraints)); 

20102  157 

25316
17c183417f93
added is_const/declare_const for local scope of fixes/consts;
wenzelm
parents:
25051
diff
changeset

158 
fun map_constraints f = 
59798  159 
map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => 
160 
(names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, f constraints)); 

19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

161 

45650  162 
fun rep_data ctxt = Data.get ctxt > (fn Data rep => rep); 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

163 

20102  164 
val names_of = #names o rep_data; 
165 
val fixes_of = #fixes o rep_data; 

56025  166 
val fixes_space = Name_Space.space_of_table o fixes_of; 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

167 
val binds_of = #binds o rep_data; 
20162  168 
val type_occs_of = #type_occs o rep_data; 
24765  169 
val maxidx_of = #maxidx o rep_data; 
28625  170 
val sorts_of = #sorts o rep_data; 
20162  171 
val constraints_of = #constraints o rep_data; 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

172 

20162  173 
val is_declared = Name.is_declared o names_of; 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

174 

47021
f35f654f297d
clarified Binding.name_of vs Name_Space.base_name vs Variable.check_name (see also 9bd8d4addd6e, 3305f573294e);
wenzelm
parents:
47005
diff
changeset

175 
val check_name = Name_Space.base_name o tap Binding.check; 
42357  176 

19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

177 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

178 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

179 
(** declarations **) 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

180 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

181 
(* default sorts and types *) 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

182 

20162  183 
fun default_type ctxt x = Vartab.lookup (#1 (constraints_of ctxt)) (x, ~1); 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

184 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

185 
fun def_type ctxt pattern xi = 
20162  186 
let val {binds, constraints = (types, _), ...} = rep_data ctxt in 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

187 
(case Vartab.lookup types xi of 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

188 
NONE => 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

189 
if pattern then NONE 
39290
44e4d8dfd6bf
load type_infer.ML later  proper context for Type_Infer.infer_types;
wenzelm
parents:
38831
diff
changeset

190 
else Vartab.lookup binds xi > Option.map (Type.mark_polymorphic o #1) 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

191 
 some => some) 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

192 
end; 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

193 

20162  194 
val def_sort = Vartab.lookup o #2 o constraints_of; 
195 

196 

59646  197 
(* maxidx *) 
198 

199 
val declare_maxidx = map_maxidx o Integer.max; 

200 

201 

20162  202 
(* names *) 
203 

24765  204 
fun declare_type_names t = 
29279  205 
map_names (fold_types (fold_atyps Term.declare_typ_names) t) #> 
24765  206 
map_maxidx (fold_types Term.maxidx_typ t); 
20162  207 

208 
fun declare_names t = 

209 
declare_type_names t #> 

29279  210 
map_names (fold_aterms Term.declare_term_frees t) #> 
24765  211 
map_maxidx (Term.maxidx_term t); 
20162  212 

213 

214 
(* type occurrences *) 

215 

24719
21d1cdab2d8c
declare_constraints: declare (fix) type variables within constraints, but not terms themselves;
wenzelm
parents:
24694
diff
changeset

216 
fun decl_type_occsT T = fold_atyps (fn TFree (a, _) => Symtab.default (a, [])  _ => I) T; 
21d1cdab2d8c
declare_constraints: declare (fix) type variables within constraints, but not terms themselves;
wenzelm
parents:
24694
diff
changeset

217 

22671  218 
val decl_type_occs = fold_term_types 
20162  219 
(fn Free (x, _) => fold_atyps (fn TFree (a, _) => Symtab.insert_list (op =) (a, x)  _ => I) 
24719
21d1cdab2d8c
declare_constraints: declare (fix) type variables within constraints, but not terms themselves;
wenzelm
parents:
24694
diff
changeset

220 
 _ => decl_type_occsT); 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

221 

24719
21d1cdab2d8c
declare_constraints: declare (fix) type variables within constraints, but not terms themselves;
wenzelm
parents:
24694
diff
changeset

222 
val declare_type_occsT = map_type_occs o fold_types decl_type_occsT; 
22671  223 
val declare_type_occs = map_type_occs o decl_type_occs; 
224 

19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

225 

20162  226 
(* constraints *) 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

227 

49685
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset

228 
fun constrain_tvar (xi, raw_S) = 
49688  229 
let val S = #2 (Term_Position.decode_positionS raw_S) 
49685
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset

230 
in if S = dummyS then Vartab.delete_safe xi else Vartab.update (xi, S) end; 
21355  231 

20162  232 
fun declare_constraints t = map_constraints (fn (types, sorts) => 
233 
let 

234 
val types' = fold_aterms 

235 
(fn Free (x, T) => Vartab.update ((x, ~1), T) 

236 
 Var v => Vartab.update v 

237 
 _ => I) t types; 

45426  238 
val sorts' = (fold_types o fold_atyps) 
21355  239 
(fn TFree (x, S) => constrain_tvar ((x, ~1), S) 
240 
 TVar v => constrain_tvar v 

45426  241 
 _ => I) t sorts; 
20162  242 
in (types', sorts') end) 
24719
21d1cdab2d8c
declare_constraints: declare (fix) type variables within constraints, but not terms themselves;
wenzelm
parents:
24694
diff
changeset

243 
#> declare_type_occsT t 
22711  244 
#> declare_type_names t; 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

245 

20162  246 

247 
(* common declarations *) 

248 

249 
fun declare_internal t = 

250 
declare_names t #> 

28625  251 
declare_type_occs t #> 
252 
map_sorts (Sorts.insert_term t); 

19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

253 

20162  254 
fun declare_term t = 
255 
declare_internal t #> 

256 
declare_constraints t; 

19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

257 

27280  258 
val declare_typ = declare_term o Logic.mk_type; 
259 

20303  260 
val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type); 
261 

22691  262 
val declare_thm = Thm.fold_terms declare_internal; 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

263 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

264 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

265 
(* renaming term/type frees *) 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

266 

20162  267 
fun variant_frees ctxt ts frees = 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

268 
let 
20162  269 
val names = names_of (fold declare_names ts ctxt); 
43326
47cf4bc789aa
simplified Name.variant  discontinued builtin fold_map;
wenzelm
parents:
42495
diff
changeset

270 
val xs = fst (fold_map Name.variant (map #1 frees) names); 
20084  271 
in xs ~~ map snd frees end; 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

272 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

273 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

274 

20303  275 
(** term bindings **) 
276 

30756  277 
fun bind_term (xi, NONE) = map_binds (Vartab.delete_safe xi) 
278 
 bind_term ((x, i), SOME t) = 

20303  279 
let 
25051  280 
val u = Term.close_schematic_term t; 
281 
val U = Term.fastype_of u; 

282 
in declare_term u #> map_binds (Vartab.update ((x, i), (U, u))) end; 

20303  283 

284 
fun expand_binds ctxt = 

285 
let 

286 
val binds = binds_of ctxt; 

21799  287 
val get = fn Var (xi, _) => Vartab.lookup binds xi  _ => NONE; 
288 
in Envir.beta_norm o Envir.expand_term get end; 

20303  289 

290 

291 

25325  292 
(** consts **) 
25316
17c183417f93
added is_const/declare_const for local scope of fixes/consts;
wenzelm
parents:
25051
diff
changeset

293 

25325  294 
val lookup_const = Symtab.lookup o #consts o rep_data; 
295 
val is_const = is_some oo lookup_const; 

25316
17c183417f93
added is_const/declare_const for local scope of fixes/consts;
wenzelm
parents:
25051
diff
changeset

296 

25325  297 
val declare_fixed = map_consts o Symtab.delete_safe; 
298 
val declare_const = map_consts o Symtab.update; 

25316
17c183417f93
added is_const/declare_const for local scope of fixes/consts;
wenzelm
parents:
25051
diff
changeset

299 

17c183417f93
added is_const/declare_const for local scope of fixes/consts;
wenzelm
parents:
25051
diff
changeset

300 

17c183417f93
added is_const/declare_const for local scope of fixes/consts;
wenzelm
parents:
25051
diff
changeset

301 

55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

302 
(** bounds **) 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

303 

a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

304 
fun next_bound (a, T) ctxt = 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

305 
let 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

306 
val b = Name.bound (#1 (#bounds (rep_data ctxt))); 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

307 
val ctxt' = ctxt > map_bounds (fn (next, bounds) => (next + 1, ((b, T), a) :: bounds)); 
55635  308 
in (Free (b, T), ctxt') end; 
55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

309 

a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

310 
fun revert_bounds ctxt t = 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

311 
(case #2 (#bounds (rep_data ctxt)) of 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

312 
[] => t 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

313 
 bounds => 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

314 
let 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

315 
val names = Term.declare_term_names t (names_of ctxt); 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

316 
val xs = rev (#1 (fold_map Name.variant (rev (map #2 bounds)) names)); 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

317 
fun subst ((b, T), _) x' = (Free (b, T), Syntax_Trans.mark_bound_abs (x', T)); 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

318 
in Term.subst_atomic (map2 subst bounds xs) t end); 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

319 

a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

320 

a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

321 

19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

322 
(** fixes **) 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

323 

59798  324 
(* inner body mode *) 
325 

326 
val inner_body = 

327 
Config.bool (Config.declare ("inner_body", @{here}) (K (Config.Bool false))); 

328 

329 
fun is_body ctxt = Config.get ctxt inner_body; 

330 
val set_body = Config.put inner_body; 

331 
fun restore_body ctxt = set_body (is_body ctxt); 

332 

333 

59790  334 
(* proper mode *) 
335 

336 
val proper_fixes = 

337 
Config.bool (Config.declare ("proper_fixes", @{here}) (K (Config.Bool true))); 

338 

339 
val improper_fixes = Config.put proper_fixes false; 

340 
fun restore_proper_fixes ctxt = Config.put proper_fixes (Config.get ctxt proper_fixes); 

341 

342 
fun is_improper ctxt x = 

343 
(case Name_Space.lookup_key (fixes_of ctxt) x of 

344 
SOME (_, (_, proper)) => not proper 

345 
 NONE => false); 

346 

347 

42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

348 
(* specialized name space *) 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

349 

59883  350 
val is_fixed = Name_Space.defined o fixes_of; 
59846  351 
fun is_newly_fixed inner outer = is_fixed inner andf (not o is_fixed outer); 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

352 

42493
01430341fc79
more informative markup for fixed variables (via name space entry);
wenzelm
parents:
42488
diff
changeset

353 
val fixed_ord = Name_Space.entry_ord o fixes_space; 
01430341fc79
more informative markup for fixed variables (via name space entry);
wenzelm
parents:
42488
diff
changeset

354 
val intern_fixed = Name_Space.intern o fixes_space; 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

355 

4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

356 
fun lookup_fixed ctxt x = 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

357 
let val x' = intern_fixed ctxt x 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

358 
in if is_fixed ctxt x' then SOME x' else NONE end; 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

359 

4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

360 
fun revert_fixed ctxt x = 
56025  361 
(case Name_Space.lookup_key (fixes_of ctxt) x of 
59790  362 
SOME (_, (x', _)) => if intern_fixed ctxt x' = x then x' else x 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

363 
 NONE => x); 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

364 

45472  365 
fun markup_fixed ctxt x = 
366 
Name_Space.markup (fixes_space ctxt) x 

367 
> Markup.name (revert_fixed ctxt x); 

368 

42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

369 
fun dest_fixes ctxt = 
59790  370 
Name_Space.fold_table (fn (x, (y, _)) => cons (y, x)) (fixes_of ctxt) [] 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58668
diff
changeset

371 
> sort (Name_Space.entry_ord (fixes_space ctxt) o apply2 #2); 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

372 

4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

373 

42482  374 
(* collect variables *) 
375 

376 
fun add_free_names ctxt = 

377 
fold_aterms (fn Free (x, _) => not (is_fixed ctxt x) ? insert (op =) x  _ => I); 

378 

379 
fun add_frees ctxt = 

380 
fold_aterms (fn Free (x, T) => not (is_fixed ctxt x) ? insert (op =) (x, T)  _ => I); 

381 

382 
fun add_fixed_names ctxt = 

383 
fold_aterms (fn Free (x, _) => is_fixed ctxt x ? insert (op =) x  _ => I); 

384 

385 
fun add_fixed ctxt = 

386 
fold_aterms (fn Free (x, T) => is_fixed ctxt x ? insert (op =) (x, T)  _ => I); 

387 

59846  388 
fun add_newly_fixed ctxt' ctxt = 
389 
fold_aterms (fn Free (x, T) => is_newly_fixed ctxt' ctxt x ? insert (op =) (x, T)  _ => I); 

390 

42482  391 

392 
(* declarations *) 

393 

20084  394 
local 
395 

42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

396 
fun err_dups dups = 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

397 
error ("Duplicate fixed variable(s): " ^ commas (map Binding.print dups)); 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

398 

42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

399 
fun new_fixed ((x, x'), pos) ctxt = 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

400 
if is_some (lookup_fixed ctxt x') then err_dups [Binding.make (x, pos)] 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

401 
else 
59790  402 
let 
403 
val proper = Config.get ctxt proper_fixes; 

404 
val context = Context.Proof ctxt > Name_Space.map_naming (K Name_Space.global_naming); 

405 
in 

47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
46869
diff
changeset

406 
ctxt 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
46869
diff
changeset

407 
> map_fixes 
59790  408 
(Name_Space.define context true (Binding.make (x', pos), (x, proper)) #> snd #> 
58668  409 
Name_Space.alias_table Name_Space.global_naming (Binding.make (x, pos)) x') 
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
46869
diff
changeset

410 
> declare_fixed x 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
46869
diff
changeset

411 
> declare_constraints (Syntax.free x') 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
46869
diff
changeset

412 
end; 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

413 

4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

414 
fun new_fixes names' xs xs' ps = 
20102  415 
map_names (K names') #> 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

416 
fold new_fixed ((xs ~~ xs') ~~ ps) #> 
20084  417 
pair xs'; 
418 

419 
in 

420 

42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

421 
fun add_fixes_binding bs ctxt = 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

422 
let 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

423 
val _ = 
55948  424 
(case filter (Name.is_skolem o Binding.name_of) bs of 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

425 
[] => () 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

426 
 bads => error ("Illegal internal Skolem constant(s): " ^ commas (map Binding.print bads))); 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

427 
val _ = 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58668
diff
changeset

428 
(case duplicates (op = o apply2 Binding.name_of) bs of 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

429 
[] => () 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

430 
 dups => err_dups dups); 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

431 

42494  432 
val xs = map check_name bs; 
20102  433 
val names = names_of ctxt; 
20084  434 
val (xs', names') = 
43326
47cf4bc789aa
simplified Name.variant  discontinued builtin fold_map;
wenzelm
parents:
42495
diff
changeset

435 
if is_body ctxt then fold_map Name.variant xs names >> map Name.skolem 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

436 
else (xs, fold Name.declare xs names); 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

437 
in ctxt > new_fixes names' xs xs' (map Binding.pos_of bs) end; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

438 

20797
c1f0bc7e7d80
renamed Variable.invent_fixes to Variable.variant_fixes;
wenzelm
parents:
20579
diff
changeset

439 
fun variant_fixes raw_xs ctxt = 
20084  440 
let 
20102  441 
val names = names_of ctxt; 
55948  442 
val xs = map (fn x => Name.clean x > Name.is_internal x ? Name.internal) raw_xs; 
43326
47cf4bc789aa
simplified Name.variant  discontinued builtin fold_map;
wenzelm
parents:
42495
diff
changeset

443 
val (xs', names') = fold_map Name.variant xs names >> (is_body ctxt ? map Name.skolem); 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

444 
in ctxt > new_fixes names' xs xs' (replicate (length xs) Position.none) end; 
20084  445 

446 
end; 

19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

447 

42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

448 
val add_fixes = add_fixes_binding o map Binding.name; 
20251  449 

450 
fun add_fixes_direct xs ctxt = ctxt 

451 
> set_body false 

452 
> (snd o add_fixes xs) 

453 
> restore_body ctxt; 

454 

42482  455 
fun auto_fixes t ctxt = ctxt 
456 
> not (is_body ctxt) ? add_fixes_direct (rev (add_free_names ctxt t [])) 

20251  457 
> declare_term t; 
458 

59796  459 

460 
(* dummy patterns *) 

461 

462 
fun fix_dummy_patterns (Const ("Pure.dummy_pattern", T)) ctxt = 

463 
let val ([x], ctxt') = add_fixes [Name.uu_] ctxt 

464 
in (Free (x, T), ctxt') end 

465 
 fix_dummy_patterns (Abs (x, T, b)) ctxt = 

466 
let val (b', ctxt') = fix_dummy_patterns b ctxt 

467 
in (Abs (x, T, b'), ctxt') end 

468 
 fix_dummy_patterns (t $ u) ctxt = 

469 
let 

470 
val (t', ctxt') = fix_dummy_patterns t ctxt; 

471 
val (u', ctxt'') = fix_dummy_patterns u ctxt'; 

472 
in (t' $ u', ctxt'') end 

473 
 fix_dummy_patterns a ctxt = (a, ctxt); 

19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

474 

300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

475 

300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

476 

22671  477 
(** export  generalize type/term variables (beware of closure sizes) **) 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

478 

300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

479 
fun export_inst inner outer = 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

480 
let 
20162  481 
val declared_outer = is_declared outer; 
59846  482 
val still_fixed = not o is_newly_fixed inner outer; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

483 

42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

484 
val gen_fixes = 
56025  485 
Name_Space.fold_table (fn (y, _) => not (is_fixed outer y) ? cons y) 
486 
(fixes_of inner) []; 

22671  487 

488 
val type_occs_inner = type_occs_of inner; 

489 
fun gen_fixesT ts = 

19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

490 
Symtab.fold (fn (a, xs) => 
20162  491 
if declared_outer a orelse exists still_fixed xs 
22671  492 
then I else cons a) (fold decl_type_occs ts type_occs_inner) []; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

493 
in (gen_fixesT, gen_fixes) end; 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

494 

300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

495 
fun exportT_inst inner outer = #1 (export_inst inner outer); 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

496 

22671  497 
fun exportT_terms inner outer = 
59645
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

498 
let 
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

499 
val mk_tfrees = exportT_inst inner outer; 
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

500 
val maxidx = maxidx_of outer; 
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

501 
in 
22671  502 
fn ts => ts > map 
31977  503 
(Term_Subst.generalize (mk_tfrees ts, []) 
59645
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

504 
(fold (Term.fold_types Term.maxidx_typ) ts maxidx + 1)) 
22671  505 
end; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

506 

22671  507 
fun export_terms inner outer = 
59645
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

508 
let 
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

509 
val (mk_tfrees, tfrees) = export_inst inner outer; 
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

510 
val maxidx = maxidx_of outer; 
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

511 
in 
22671  512 
fn ts => ts > map 
31977  513 
(Term_Subst.generalize (mk_tfrees ts, tfrees) 
59645
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

514 
(fold Term.maxidx_term ts maxidx + 1)) 
22671  515 
end; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

516 

20303  517 
fun export_prf inner outer prf = 
518 
let 

22671  519 
val (mk_tfrees, frees) = export_inst (declare_prf prf inner) outer; 
520 
val tfrees = mk_tfrees []; 

59645
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

521 
val maxidx = maxidx_of outer; 
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

522 
val idx = Proofterm.maxidx_proof prf maxidx + 1; 
36620
e6bb250402b5
simplified/unified fundamental operations on types/terms/proofterms  prefer Same.operation over "option" variant;
wenzelm
parents:
36610
diff
changeset

523 
val gen_term = Term_Subst.generalize_same (tfrees, frees) idx; 
e6bb250402b5
simplified/unified fundamental operations on types/terms/proofterms  prefer Same.operation over "option" variant;
wenzelm
parents:
36610
diff
changeset

524 
val gen_typ = Term_Subst.generalizeT_same tfrees idx; 
e6bb250402b5
simplified/unified fundamental operations on types/terms/proofterms  prefer Same.operation over "option" variant;
wenzelm
parents:
36610
diff
changeset

525 
in Same.commit (Proofterm.map_proof_terms_same gen_term gen_typ) prf end; 
20303  526 

22671  527 

59645
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

528 
fun gen_export (mk_tfrees, frees) maxidx ths = 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

529 
let 
22671  530 
val tfrees = mk_tfrees (map Thm.full_prop_of ths); 
59645
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

531 
val idx = fold Thm.maxidx_thm ths maxidx + 1; 
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

532 
in map (Thm.generalize (tfrees, frees) idx) ths end; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

533 

59645
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

534 
fun exportT inner outer = gen_export (exportT_inst inner outer, []) (maxidx_of outer); 
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

535 
fun export inner outer = gen_export (export_inst inner outer) (maxidx_of outer); 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

536 

21522  537 
fun export_morphism inner outer = 
538 
let 

539 
val fact = export inner outer; 

540 
val term = singleton (export_terms inner outer); 

541 
val typ = Logic.type_map term; 

54740  542 
in 
543 
Morphism.morphism "Variable.export" {binding = [], typ = [typ], term = [term], fact = [fact]} 

544 
end; 

19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

545 

300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

546 

24765  547 

19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

548 
(** import  fix schematic type/term variables **) 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

549 

59796  550 
fun invent_types Ss ctxt = 
551 
let 

552 
val tfrees = Name.invent (names_of ctxt) Name.aT (length Ss) ~~ Ss; 

553 
val ctxt' = fold (declare_constraints o Logic.mk_type o TFree) tfrees ctxt; 

554 
in (tfrees, ctxt') end; 

555 

19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

556 
fun importT_inst ts ctxt = 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

557 
let 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

558 
val tvars = rev (fold Term.add_tvars ts []); 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

559 
val (tfrees, ctxt') = invent_types (map #2 tvars) ctxt; 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

560 
in (tvars ~~ map TFree tfrees, ctxt') end; 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

561 

300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

562 
fun import_inst is_open ts ctxt = 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

563 
let 
26714
4773b832f1b1
variant_fixes: preserve internal state, mark skolem only for body mode;
wenzelm
parents:
25573
diff
changeset

564 
val ren = Name.clean #> (if is_open then I else Name.internal); 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

565 
val (instT, ctxt') = importT_inst ts ctxt; 
31977  566 
val vars = map (apsnd (Term_Subst.instantiateT instT)) (rev (fold Term.add_vars ts [])); 
20797
c1f0bc7e7d80
renamed Variable.invent_fixes to Variable.variant_fixes;
wenzelm
parents:
20579
diff
changeset

567 
val (xs, ctxt'') = variant_fixes (map (ren o #1 o #1) vars) ctxt'; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

568 
val inst = vars ~~ map Free (xs ~~ map #2 vars); 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

569 
in ((instT, inst), ctxt'') end; 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

570 

300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

571 
fun importT_terms ts ctxt = 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

572 
let val (instT, ctxt') = importT_inst ts ctxt 
31977  573 
in (map (Term_Subst.instantiate (instT, [])) ts, ctxt') end; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

574 

300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

575 
fun import_terms is_open ts ctxt = 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

576 
let val (inst, ctxt') = import_inst is_open ts ctxt 
31977  577 
in (map (Term_Subst.instantiate inst) ts, ctxt') end; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

578 

31794
71af1fd6a5e4
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef  Alice is no longer supported);
wenzelm
parents:
30756
diff
changeset

579 
fun importT ths ctxt = 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

580 
let 
42360  581 
val thy = Proof_Context.theory_of ctxt; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

582 
val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt; 
32280
4fb3f426052a
Variable.importT/import: return full instantiations, tuned;
wenzelm
parents:
32199
diff
changeset

583 
val insts' as (instT', _) = Thm.certify_inst thy (instT, []); 
4fb3f426052a
Variable.importT/import: return full instantiations, tuned;
wenzelm
parents:
32199
diff
changeset

584 
val ths' = map (Thm.instantiate insts') ths; 
4fb3f426052a
Variable.importT/import: return full instantiations, tuned;
wenzelm
parents:
32199
diff
changeset

585 
in ((instT', ths'), ctxt') end; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

586 

20303  587 
fun import_prf is_open prf ctxt = 
588 
let 

589 
val ts = rev (Proofterm.fold_proof_terms cons (cons o Logic.mk_type) prf []); 

590 
val (insts, ctxt') = import_inst is_open ts ctxt; 

591 
in (Proofterm.instantiate insts prf, ctxt') end; 

592 

31794
71af1fd6a5e4
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef  Alice is no longer supported);
wenzelm
parents:
30756
diff
changeset

593 
fun import is_open ths ctxt = 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

594 
let 
42360  595 
val thy = Proof_Context.theory_of ctxt; 
32280
4fb3f426052a
Variable.importT/import: return full instantiations, tuned;
wenzelm
parents:
32199
diff
changeset

596 
val (insts, ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt; 
4fb3f426052a
Variable.importT/import: return full instantiations, tuned;
wenzelm
parents:
32199
diff
changeset

597 
val insts' = Thm.certify_inst thy insts; 
4fb3f426052a
Variable.importT/import: return full instantiations, tuned;
wenzelm
parents:
32199
diff
changeset

598 
val ths' = map (Thm.instantiate insts') ths; 
4fb3f426052a
Variable.importT/import: return full instantiations, tuned;
wenzelm
parents:
32199
diff
changeset

599 
in ((insts', ths'), ctxt') end; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

600 

300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

601 

19926  602 
(* import/export *) 
603 

21287  604 
fun gen_trade imp exp f ctxt ths = 
20220  605 
let val ((_, ths'), ctxt') = imp ths ctxt 
21287  606 
in exp ctxt' ctxt (f ctxt' ths') end; 
19926  607 

31794
71af1fd6a5e4
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef  Alice is no longer supported);
wenzelm
parents:
30756
diff
changeset

608 
val tradeT = gen_trade importT exportT; 
71af1fd6a5e4
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef  Alice is no longer supported);
wenzelm
parents:
30756
diff
changeset

609 
val trade = gen_trade (import true) export; 
19926  610 

611 

42495
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

612 
(* focus on outermost parameters: !!x y z. B *) 
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

613 

1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

614 
fun focus_params t ctxt = 
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

615 
let 
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

616 
val (xs, Ts) = 
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

617 
split_list (Term.variant_frees t (Term.strip_all_vars t)); (*as they are printed :*) 
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

618 
val (xs', ctxt') = variant_fixes xs ctxt; 
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

619 
val ps = xs' ~~ Ts; 
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

620 
val ctxt'' = ctxt' > fold (declare_constraints o Free) ps; 
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

621 
in ((xs, ps), ctxt'') end; 
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

622 

1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

623 
fun focus t ctxt = 
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

624 
let 
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

625 
val ((xs, ps), ctxt') = focus_params t ctxt; 
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

626 
val t' = Term.subst_bounds (rev (map Free ps), Term.strip_all_body t); 
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

627 
in (((xs ~~ ps), t'), ctxt') end; 
20149  628 

629 
fun forall_elim_prop t prop = 

46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
45666
diff
changeset

630 
Thm.beta_conversion false (Thm.apply (Thm.dest_arg prop) t) 
20579  631 
> Thm.cprop_of > Thm.dest_arg; 
20149  632 

42495
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

633 
fun focus_cterm goal ctxt = 
20149  634 
let 
42495
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

635 
val ((xs, ps), ctxt') = focus_params (Thm.term_of goal) ctxt; 
59623  636 
val ps' = map (Thm.cterm_of ctxt' o Free) ps; 
20220  637 
val goal' = fold forall_elim_prop ps' goal; 
42495
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

638 
in ((xs ~~ ps', goal'), ctxt') end; 
20149  639 

20303  640 
fun focus_subgoal i st = 
641 
let 

22691  642 
val all_vars = Thm.fold_terms Term.add_vars st []; 
20303  643 
val no_binds = map (fn (xi, _) => (xi, NONE)) all_vars; 
644 
in 

30756  645 
fold bind_term no_binds #> 
20303  646 
fold (declare_constraints o Var) all_vars #> 
42495
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

647 
focus_cterm (Thm.cprem_of st i) 
20303  648 
end; 
649 

650 

19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

651 

300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

652 
(** implicit polymorphism **) 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

653 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

654 
(* warn_extra_tfrees *) 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

655 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

656 
fun warn_extra_tfrees ctxt1 ctxt2 = 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

657 
let 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

658 
fun occs_typ a = Term.exists_subtype (fn TFree (b, _) => a = b  _ => false); 
20162  659 
fun occs_free a x = 
660 
(case def_type ctxt1 false (x, ~1) of 

661 
SOME T => if occs_typ a T then I else cons (a, x) 

662 
 NONE => cons (a, x)); 

19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

663 

20162  664 
val occs1 = type_occs_of ctxt1; 
665 
val occs2 = type_occs_of ctxt2; 

19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

666 
val extras = Symtab.fold (fn (a, xs) => 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

667 
if Symtab.defined occs1 a then I else fold (occs_free a) xs) occs2 []; 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

668 
val tfrees = map #1 extras > sort_distinct string_ord; 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

669 
val frees = map #2 extras > sort_distinct string_ord; 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

670 
in 
38831
4933a3dfd745
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
37145
diff
changeset

671 
if null extras orelse not (Context_Position.is_visible ctxt2) then () 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

672 
else warning ("Introduced fixed type variable(s): " ^ commas tfrees ^ " in " ^ 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

673 
space_implode " or " (map quote frees)) 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

674 
end; 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

675 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

676 

20149  677 
(* polymorphic terms *) 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

678 

24694  679 
fun polymorphic_types ctxt ts = 
20003  680 
let 
681 
val ctxt' = fold declare_term ts ctxt; 

20162  682 
val occs = type_occs_of ctxt; 
683 
val occs' = type_occs_of ctxt'; 

684 
val types = Symtab.fold (fn (a, _) => if Symtab.defined occs a then I else cons a) occs' []; 

24765  685 
val idx = maxidx_of ctxt' + 1; 
24694  686 
val Ts' = (fold o fold_types o fold_atyps) 
687 
(fn T as TFree _ => 

31977  688 
(case Term_Subst.generalizeT types idx T of TVar v => insert (op =) v  _ => I) 
24694  689 
 _ => I) ts []; 
31977  690 
val ts' = map (Term_Subst.generalize (types, []) idx) ts; 
24694  691 
in (rev Ts', ts') end; 
692 

693 
fun polymorphic ctxt ts = snd (polymorphic_types ctxt ts); 

20003  694 

19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

695 
end; 