author  wenzelm 
Thu, 20 Feb 2014 21:27:14 +0100  
changeset 55635  00e900057b38 
parent 55014  a93f496f6c30 
child 55948  bb21b380f65d 
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 is_body: Proof.context > bool 
10 
val set_body: bool > Proof.context > Proof.context 

11 
val restore_body: Proof.context > Proof.context > Proof.context 

12 
val names_of: Proof.context > Name.context 

13 
val binds_of: Proof.context > (typ * term) Vartab.table 

24765  14 
val maxidx_of: Proof.context > int 
28625  15 
val sorts_of: Proof.context > sort list 
20303  16 
val constraints_of: Proof.context > typ Vartab.table * sort Vartab.table 
17 
val is_declared: Proof.context > string > bool 

42494  18 
val check_name: binding > string 
20303  19 
val default_type: Proof.context > string > typ option 
20 
val def_type: Proof.context > bool > indexname > typ option 

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

27280  22 
val declare_names: term > Proof.context > Proof.context 
20303  23 
val declare_constraints: term > Proof.context > Proof.context 
24 
val declare_term: term > Proof.context > Proof.context 

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

36603
d5d6111761a6
renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;
wenzelm
parents:
33957
diff
changeset

28 
val global_thm_context: thm > Proof.context 
20303  29 
val variant_frees: Proof.context > term list > (string * 'a) list > (string * 'a) list 
30756  30 
val bind_term: indexname * term option > Proof.context > Proof.context 
20303  31 
val expand_binds: Proof.context > term > term 
25325  32 
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

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

36 
val revert_bounds: Proof.context > term > term 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

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

38 
val 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

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

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

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

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

43 
val revert_fixed: Proof.context > string > string 
42482  44 
val add_fixed_names: Proof.context > term > string list > string list 
45 
val add_fixed: Proof.context > term > (string * typ) list > (string * typ) list 

46 
val add_free_names: Proof.context > term > string list > string list 

47 
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

48 
val add_fixes_binding: binding list > Proof.context > string list * Proof.context 
20303  49 
val add_fixes: string list > Proof.context > string list * Proof.context 
50 
val add_fixes_direct: string list > Proof.context > Proof.context 

21369  51 
val auto_fixes: term > Proof.context > Proof.context 
20797
c1f0bc7e7d80
renamed Variable.invent_fixes to Variable.variant_fixes;
wenzelm
parents:
20579
diff
changeset

52 
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

53 
val dest_fixes: Proof.context > (string * string) list 
20303  54 
val invent_types: sort list > Proof.context > (string * sort) list * Proof.context 
55 
val export_terms: Proof.context > Proof.context > term list > term list 

56 
val exportT_terms: Proof.context > Proof.context > term list > term list 

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

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

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

21522  60 
val export_morphism: Proof.context > Proof.context > morphism 
20303  61 
val importT_inst: term list > Proof.context > ((indexname * sort) * typ) list * Proof.context 
62 
val import_inst: bool > term list > Proof.context > 

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

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

65 
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

66 
val importT: thm list > Proof.context > ((ctyp * ctyp) list * thm list) * Proof.context 
20303  67 
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

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

69 
(((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context 
21287  70 
val tradeT: (Proof.context > thm list > thm list) > Proof.context > thm list > thm list 
71 
val trade: (Proof.context > thm list > thm list) > Proof.context > thm list > thm list 

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

72 
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

73 
val focus_cterm: cterm > Proof.context > ((string * cterm) list * cterm) * Proof.context 
32199  74 
val focus_subgoal: int > thm > Proof.context > ((string * cterm) list * cterm) * Proof.context 
20303  75 
val warn_extra_tfrees: Proof.context > Proof.context > unit 
24694  76 
val polymorphic_types: Proof.context > term list > (indexname * sort) list * term list 
20303  77 
val polymorphic: Proof.context > term list > term list 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

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

79 

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

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

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

82 

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

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

84 

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

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

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

87 

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

88 
datatype data = Data of 
20102  89 
{is_body: bool, (*inner body mode*) 
20162  90 
names: Name.context, (*type/term variable names*) 
25325  91 
consts: string Symtab.table, (*consts within the local scope*) 
55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

92 
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

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

101 

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

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

103 
(is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) = 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

104 
Data {is_body = is_body, names = names, consts = consts, bounds = bounds, fixes = fixes, 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

105 
binds = binds, type_occs = type_occs, maxidx = maxidx, sorts = sorts, constraints = constraints}; 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

106 

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

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

109 
type T = data; 
32784  110 
fun init _ = 
55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

111 
make_data (false, Name.context, Symtab.empty, (0, []), empty_fixes, Vartab.empty, 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

112 
Symtab.empty, ~1, [], (Vartab.empty, Vartab.empty)); 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

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

114 

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

115 
fun map_data f = 
55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

116 
Data.map (fn 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

117 
Data {is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints} => 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

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

119 
(f (is_body, 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

120 

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

121 
fun map_names f = 
55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

122 
map_data (fn 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

123 
(is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

124 
(is_body, 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

125 

25325  126 
fun map_consts f = 
55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

127 
map_data (fn 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

128 
(is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

129 
(is_body, names, f consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints)); 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

130 

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

131 
fun map_bounds f = 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

132 
map_data (fn 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

133 
(is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

134 
(is_body, names, consts, f bounds, fixes, binds, type_occs, maxidx, sorts, constraints)); 
20162  135 

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

136 
fun map_fixes f = 
55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

137 
map_data (fn 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

138 
(is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

139 
(is_body, 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

140 

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

141 
fun map_binds f = 
55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

142 
map_data (fn 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

143 
(is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

144 
(is_body, 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 = 
55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

147 
map_data (fn 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

148 
(is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

149 
(is_body, 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

150 

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

151 
fun map_maxidx f = 
55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

152 
map_data (fn 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

153 
(is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

154 
(is_body, names, consts, bounds, fixes, binds, type_occs, f maxidx, sorts, constraints)); 
28625  155 

156 
fun map_sorts f = 

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

157 
map_data (fn 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

158 
(is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

159 
(is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, f sorts, constraints)); 
20102  160 

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

161 
fun map_constraints f = 
55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

162 
map_data (fn 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

163 
(is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

164 
(is_body, 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

165 

45650  166 
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

167 

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

168 
val is_body = #is_body o rep_data; 
24765  169 

28625  170 
fun set_body b = 
55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

171 
map_data (fn (_, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

172 
(b, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints)); 
24765  173 

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

174 
fun restore_body ctxt = set_body (is_body ctxt); 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

175 

20102  176 
val names_of = #names o rep_data; 
177 
val fixes_of = #fixes o rep_data; 

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

178 
val fixes_space = #1 o fixes_of; 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

179 
val binds_of = #binds o rep_data; 
20162  180 
val type_occs_of = #type_occs o rep_data; 
24765  181 
val maxidx_of = #maxidx o rep_data; 
28625  182 
val sorts_of = #sorts o rep_data; 
20162  183 
val constraints_of = #constraints o rep_data; 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

184 

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

186 

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

187 
val check_name = Name_Space.base_name o tap Binding.check; 
42357  188 

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

189 

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

190 

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

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

192 

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

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

194 

20162  195 
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

196 

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

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

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

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

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

202 
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

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

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

205 

20162  206 
val def_sort = Vartab.lookup o #2 o constraints_of; 
207 

208 

209 
(* names *) 

210 

24765  211 
fun declare_type_names t = 
29279  212 
map_names (fold_types (fold_atyps Term.declare_typ_names) t) #> 
24765  213 
map_maxidx (fold_types Term.maxidx_typ t); 
20162  214 

215 
fun declare_names t = 

216 
declare_type_names t #> 

29279  217 
map_names (fold_aterms Term.declare_term_frees t) #> 
24765  218 
map_maxidx (Term.maxidx_term t); 
20162  219 

220 

221 
(* type occurrences *) 

222 

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

223 
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

224 

22671  225 
val decl_type_occs = fold_term_types 
20162  226 
(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

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

228 

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

229 
val declare_type_occsT = map_type_occs o fold_types decl_type_occsT; 
22671  230 
val declare_type_occs = map_type_occs o decl_type_occs; 
231 

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

232 

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

234 

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

235 
fun constrain_tvar (xi, raw_S) = 
49688  236 
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

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

20162  239 
fun declare_constraints t = map_constraints (fn (types, sorts) => 
240 
let 

241 
val types' = fold_aterms 

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

243 
 Var v => Vartab.update v 

244 
 _ => I) t types; 

45426  245 
val sorts' = (fold_types o fold_atyps) 
21355  246 
(fn TFree (x, S) => constrain_tvar ((x, ~1), S) 
247 
 TVar v => constrain_tvar v 

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

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

252 

20162  253 

254 
(* common declarations *) 

255 

256 
fun declare_internal t = 

257 
declare_names t #> 

28625  258 
declare_type_occs t #> 
259 
map_sorts (Sorts.insert_term t); 

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

260 

20162  261 
fun declare_term t = 
262 
declare_internal t #> 

263 
declare_constraints t; 

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

264 

27280  265 
val declare_typ = declare_term o Logic.mk_type; 
266 

20303  267 
val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type); 
268 

22691  269 
val declare_thm = Thm.fold_terms declare_internal; 
42360  270 
fun global_thm_context th = declare_thm th (Proof_Context.init_global (Thm.theory_of_thm th)); 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

271 

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 
(* renaming term/type frees *) 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

274 

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

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

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

280 

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

281 

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

282 

20303  283 
(** term bindings **) 
284 

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

20303  287 
let 
25051  288 
val u = Term.close_schematic_term t; 
289 
val U = Term.fastype_of u; 

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

20303  291 

292 
fun expand_binds ctxt = 

293 
let 

294 
val binds = binds_of ctxt; 

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

20303  297 

298 

299 

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

301 

25325  302 
val lookup_const = Symtab.lookup o #consts o rep_data; 
303 
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

304 

25325  305 
val declare_fixed = map_consts o Symtab.delete_safe; 
306 
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

307 

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

308 

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

309 

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

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

311 

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

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

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

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

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

317 

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

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

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

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

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

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

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

324 
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

325 
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

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

327 

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

328 

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

329 

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

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

331 

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

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

333 

46869  334 
val is_fixed = Name_Space.defined_entry o fixes_space; 
335 
fun 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

336 

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

337 
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

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

339 

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

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

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

342 
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

343 

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

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

345 
(case Symtab.lookup (#2 (fixes_of ctxt)) x of 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

346 
SOME x' => if intern_fixed ctxt x' = x then x' else x 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

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

348 

45472  349 
fun markup_fixed ctxt x = 
350 
Name_Space.markup (fixes_space ctxt) x 

351 
> Markup.name (revert_fixed ctxt x); 

352 

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

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

354 
let val (space, tab) = fixes_of ctxt 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

355 
in sort (Name_Space.entry_ord space o pairself #2) (map swap (Symtab.dest tab)) end; 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

356 

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

357 

42482  358 
(* collect variables *) 
359 

360 
fun add_free_names ctxt = 

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

362 

363 
fun add_frees ctxt = 

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

365 

366 
fun add_fixed_names ctxt = 

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

368 

369 
fun add_fixed ctxt = 

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

371 

372 

373 
(* declarations *) 

374 

20084  375 
local 
376 

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

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

378 
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

379 

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

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

381 
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

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

383 
let val context = Context.Proof ctxt > Name_Space.map_naming (K Name_Space.default_naming) in 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
46869
diff
changeset

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

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

386 
(Name_Space.define context true (Binding.make (x', pos), x) #> snd #>> 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
46869
diff
changeset

387 
Name_Space.alias Name_Space.default_naming (Binding.make (x, pos)) x') 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
46869
diff
changeset

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

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

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

391 

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

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

394 
fold new_fixed ((xs ~~ xs') ~~ ps) #> 
20084  395 
pair xs'; 
396 

397 
in 

398 

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

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

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

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

402 
(case filter (can Name.dest_skolem o Binding.name_of) bs of 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

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

404 
 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

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

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

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

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

409 

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

413 
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

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

415 
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

416 

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

417 
fun variant_fixes raw_xs ctxt = 
20084  418 
let 
20102  419 
val names = names_of ctxt; 
26714
4773b832f1b1
variant_fixes: preserve internal state, mark skolem only for body mode;
wenzelm
parents:
25573
diff
changeset

420 
val xs = map (fn x => Name.clean x > can Name.dest_internal x ? Name.internal) raw_xs; 
43326
47cf4bc789aa
simplified Name.variant  discontinued builtin fold_map;
wenzelm
parents:
42495
diff
changeset

421 
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

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

424 
end; 

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

425 

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

426 
val add_fixes = add_fixes_binding o map Binding.name; 
20251  427 

428 
fun add_fixes_direct xs ctxt = ctxt 

429 
> set_body false 

430 
> (snd o add_fixes xs) 

431 
> restore_body ctxt; 

432 

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

20251  435 
> declare_term t; 
436 

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

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

438 
let 
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
43326
diff
changeset

439 
val tfrees = Name.invent (names_of ctxt) Name.aT (length Ss) ~~ Ss; 
20162  440 
val ctxt' = fold (declare_constraints o Logic.mk_type o TFree) tfrees ctxt; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

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

442 

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

443 

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

444 

22671  445 
(** 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

446 

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

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

448 
let 
20162  449 
val declared_outer = is_declared outer; 
46869  450 
val still_fixed = not o newly_fixed inner outer; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

451 

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

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

453 
Symtab.fold (fn (y, _) => not (is_fixed outer y) ? cons y) 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

454 
(#2 (fixes_of inner)) []; 
22671  455 

456 
val type_occs_inner = type_occs_of inner; 

457 
fun gen_fixesT ts = 

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

458 
Symtab.fold (fn (a, xs) => 
20162  459 
if declared_outer a orelse exists still_fixed xs 
22671  460 
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

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

462 

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

463 
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

464 

22671  465 
fun exportT_terms inner outer = 
466 
let val mk_tfrees = exportT_inst inner outer in 

467 
fn ts => ts > map 

31977  468 
(Term_Subst.generalize (mk_tfrees ts, []) 
22671  469 
(fold (Term.fold_types Term.maxidx_typ) ts ~1 + 1)) 
470 
end; 

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

471 

22671  472 
fun export_terms inner outer = 
473 
let val (mk_tfrees, tfrees) = export_inst inner outer in 

474 
fn ts => ts > map 

31977  475 
(Term_Subst.generalize (mk_tfrees ts, tfrees) 
22671  476 
(fold Term.maxidx_term ts ~1 + 1)) 
477 
end; 

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

478 

20303  479 
fun export_prf inner outer prf = 
480 
let 

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

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

484 
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

485 
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

486 
in Same.commit (Proofterm.map_proof_terms_same gen_term gen_typ) prf end; 
20303  487 

22671  488 

489 
fun gen_export (mk_tfrees, frees) ths = 

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

490 
let 
22671  491 
val tfrees = mk_tfrees (map Thm.full_prop_of ths); 
492 
val maxidx = fold Thm.maxidx_thm ths ~1; 

493 
in map (Thm.generalize (tfrees, frees) (maxidx + 1)) ths end; 

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

494 

22671  495 
fun exportT inner outer = gen_export (exportT_inst inner outer, []); 
496 
fun export inner outer = gen_export (export_inst inner outer); 

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

497 

21522  498 
fun export_morphism inner outer = 
499 
let 

500 
val fact = export inner outer; 

501 
val term = singleton (export_terms inner outer); 

502 
val typ = Logic.type_map term; 

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

505 
end; 

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

506 

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

507 

24765  508 

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

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

510 

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

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

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

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

514 
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

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

516 

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

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

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

519 
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

520 
val (instT, ctxt') = importT_inst ts ctxt; 
31977  521 
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

522 
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

523 
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

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

525 

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

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

527 
let val (instT, ctxt') = importT_inst ts ctxt 
31977  528 
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

529 

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

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

531 
let val (inst, ctxt') = import_inst is_open ts ctxt 
31977  532 
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

533 

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

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

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

537 
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

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

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

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

541 

20303  542 
fun import_prf is_open prf ctxt = 
543 
let 

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

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

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

547 

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

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

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

551 
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

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

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

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

555 

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

556 

19926  557 
(* import/export *) 
558 

21287  559 
fun gen_trade imp exp f ctxt ths = 
20220  560 
let val ((_, ths'), ctxt') = imp ths ctxt 
21287  561 
in exp ctxt' ctxt (f ctxt' ths') end; 
19926  562 

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

563 
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

564 
val trade = gen_trade (import true) export; 
19926  565 

566 

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

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

568 

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

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

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

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

572 
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

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

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

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

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

577 

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

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

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

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

581 
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

582 
in (((xs ~~ ps), t'), ctxt') end; 
20149  583 

584 
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

585 
Thm.beta_conversion false (Thm.apply (Thm.dest_arg prop) t) 
20579  586 
> Thm.cprop_of > Thm.dest_arg; 
20149  587 

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

588 
fun focus_cterm goal ctxt = 
20149  589 
let 
590 
val cert = Thm.cterm_of (Thm.theory_of_cterm goal); 

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

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

592 
val ps' = map (cert o Free) ps; 
20220  593 
val goal' = fold forall_elim_prop ps' goal; 
42495
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

594 
in ((xs ~~ ps', goal'), ctxt') end; 
20149  595 

20303  596 
fun focus_subgoal i st = 
597 
let 

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

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

603 
focus_cterm (Thm.cprem_of st i) 
20303  604 
end; 
605 

606 

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

607 

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

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

609 

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

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

611 

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

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

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

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

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

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

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

619 

20162  620 
val occs1 = type_occs_of ctxt1; 
621 
val occs2 = type_occs_of ctxt2; 

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

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

623 
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

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

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

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

627 
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

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

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

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

631 

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

632 

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

634 

24694  635 
fun polymorphic_types ctxt ts = 
20003  636 
let 
637 
val ctxt' = fold declare_term ts ctxt; 

20162  638 
val occs = type_occs_of ctxt; 
639 
val occs' = type_occs_of ctxt'; 

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

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

31977  644 
(case Term_Subst.generalizeT types idx T of TVar v => insert (op =) v  _ => I) 
24694  645 
 _ => I) ts []; 
31977  646 
val ts' = map (Term_Subst.generalize (types, []) idx) ts; 
24694  647 
in (rev Ts', ts') end; 
648 

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

20003  650 

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

651 
end; 