author  wenzelm 
Sun, 26 Jul 2009 13:12:54 +0200  
changeset 32199  82c4c570310a 
parent 31977  e03059ae2d82 
child 32280  4fb3f426052a 
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 fixes_of: Proof.context > (string * string) list 

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

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

19 
val is_fixed: Proof.context > string > bool 

20 
val newly_fixed: Proof.context > Proof.context > string > bool 

21571  21 
val add_fixed: Proof.context > term > (string * typ) list > (string * typ) list 
20303  22 
val default_type: Proof.context > string > typ option 
23 
val def_type: Proof.context > bool > indexname > typ option 

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

27280  25 
val declare_names: term > Proof.context > Proof.context 
20303  26 
val declare_constraints: term > Proof.context > Proof.context 
27 
val declare_term: term > Proof.context > Proof.context 

27280  28 
val declare_typ: typ > Proof.context > Proof.context 
20303  29 
val declare_prf: Proofterm.proof > Proof.context > Proof.context 
30 
val declare_thm: thm > Proof.context > Proof.context 

31 
val thm_context: thm > Proof.context 

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

30756  33 
val bind_term: indexname * term option > Proof.context > Proof.context 
20303  34 
val expand_binds: Proof.context > term > term 
25325  35 
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

36 
val is_const: Proof.context > string > bool 
25325  37 
val declare_const: string * string > Proof.context > Proof.context 
20303  38 
val add_fixes: string list > Proof.context > string list * Proof.context 
39 
val add_fixes_direct: string list > Proof.context > Proof.context 

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

41 
val variant_fixes: string list > Proof.context > string list * Proof.context 
20303  42 
val invent_types: sort list > Proof.context > (string * sort) list * Proof.context 
43 
val export_terms: Proof.context > Proof.context > term list > term list 

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

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

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

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

21522  48 
val export_morphism: Proof.context > Proof.context > morphism 
20303  49 
val importT_inst: term list > Proof.context > ((indexname * sort) * typ) list * Proof.context 
50 
val import_inst: bool > term list > Proof.context > 

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

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

53 
val import_terms: bool > term list > Proof.context > term list * 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

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

56 
val import: bool > thm list > Proof.context > 
20303  57 
((ctyp list * cterm list) * thm list) * Proof.context 
21287  58 
val tradeT: (Proof.context > thm list > thm list) > Proof.context > thm list > thm list 
59 
val trade: (Proof.context > thm list > thm list) > Proof.context > thm list > thm list 

32199  60 
val focus: cterm > Proof.context > ((string * cterm) list * cterm) * Proof.context 
61 
val focus_subgoal: int > thm > Proof.context > ((string * cterm) list * cterm) * Proof.context 

20303  62 
val warn_extra_tfrees: Proof.context > Proof.context > unit 
24694  63 
val polymorphic_types: Proof.context > term list > (indexname * sort) list * term list 
20303  64 
val polymorphic: Proof.context > term list > term list 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

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

66 

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

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

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

69 

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

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

71 

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

72 
datatype data = Data of 
20102  73 
{is_body: bool, (*inner body mode*) 
20162  74 
names: Name.context, (*type/term variable names*) 
25325  75 
consts: string Symtab.table, (*consts within the local scope*) 
20162  76 
fixes: (string * string) list, (*term fixes  extern/intern*) 
20102  77 
binds: (typ * term) Vartab.table, (*term bindings*) 
20162  78 
type_occs: string list Symtab.table, (*type variables  possibly within term variables*) 
24765  79 
maxidx: int, (*maximum var index*) 
28625  80 
sorts: sort OrdList.T, (*declared sort occurrences*) 
20162  81 
constraints: 
20102  82 
typ Vartab.table * (*type constraints*) 
20162  83 
sort Vartab.table}; (*default sorts*) 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

84 

28625  85 
fun make_data (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) = 
25325  86 
Data {is_body = is_body, names = names, consts = consts, fixes = fixes, binds = binds, 
28625  87 
type_occs = type_occs, maxidx = maxidx, sorts = sorts, constraints = constraints}; 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

88 

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

89 
structure Data = ProofDataFun 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

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

91 
type T = data; 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

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

93 
make_data (false, Name.context, Symtab.empty, [], Vartab.empty, Symtab.empty, 
28625  94 
~1, [], (Vartab.empty, Vartab.empty)); 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

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

96 

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

97 
fun map_data f = 
28625  98 
Data.map (fn Data {is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints} => 
99 
make_data (f (is_body, names, consts, 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

100 

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

101 
fun map_names f = 
28625  102 
map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) => 
103 
(is_body, f names, consts, fixes, binds, type_occs, maxidx, sorts, constraints)); 

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

104 

25325  105 
fun map_consts f = 
28625  106 
map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) => 
107 
(is_body, names, f consts, fixes, binds, type_occs, maxidx, sorts, constraints)); 

20162  108 

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

109 
fun map_fixes f = 
28625  110 
map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) => 
111 
(is_body, names, consts, f fixes, binds, type_occs, maxidx, sorts, constraints)); 

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

112 

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

113 
fun map_binds f = 
28625  114 
map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) => 
115 
(is_body, names, consts, fixes, f binds, type_occs, maxidx, sorts, constraints)); 

24765  116 

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

117 
fun map_type_occs f = 
28625  118 
map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) => 
119 
(is_body, names, consts, fixes, binds, f type_occs, maxidx, sorts, constraints)); 

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

120 

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

121 
fun map_maxidx f = 
28625  122 
map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) => 
123 
(is_body, names, consts, fixes, binds, type_occs, f maxidx, sorts, constraints)); 

124 

125 
fun map_sorts f = 

126 
map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) => 

127 
(is_body, names, consts, fixes, binds, type_occs, maxidx, f sorts, constraints)); 

20102  128 

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

129 
fun map_constraints f = 
28625  130 
map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) => 
131 
(is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, f constraints)); 

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

132 

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

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

134 

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

135 
val is_body = #is_body o rep_data; 
24765  136 

28625  137 
fun set_body b = 
138 
map_data (fn (_, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) => 

139 
(b, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints)); 

24765  140 

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

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

142 

20102  143 
val names_of = #names o rep_data; 
144 
val fixes_of = #fixes o rep_data; 

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

145 
val binds_of = #binds o rep_data; 
20162  146 
val type_occs_of = #type_occs o rep_data; 
24765  147 
val maxidx_of = #maxidx o rep_data; 
28625  148 
val sorts_of = #sorts o rep_data; 
20162  149 
val constraints_of = #constraints o rep_data; 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

150 

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

152 
fun is_fixed ctxt x = exists (fn (_, y) => x = y) (fixes_of ctxt); 
20149  153 
fun newly_fixed inner outer x = is_fixed inner x andalso not (is_fixed outer x); 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

154 

21571  155 
fun add_fixed ctxt = Term.fold_aterms 
156 
(fn Free (x, T) => if is_fixed ctxt x then insert (op =) (x, T) else I  _ => I); 

157 

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

158 

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

159 

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

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

161 

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

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

163 

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

165 

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

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

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

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

170 
if pattern then NONE 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

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

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

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

174 

20162  175 
val def_sort = Vartab.lookup o #2 o constraints_of; 
176 

177 

178 
(* names *) 

179 

24765  180 
fun declare_type_names t = 
29279  181 
map_names (fold_types (fold_atyps Term.declare_typ_names) t) #> 
24765  182 
map_maxidx (fold_types Term.maxidx_typ t); 
20162  183 

184 
fun declare_names t = 

185 
declare_type_names t #> 

29279  186 
map_names (fold_aterms Term.declare_term_frees t) #> 
24765  187 
map_maxidx (Term.maxidx_term t); 
20162  188 

189 

190 
(* type occurrences *) 

191 

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

192 
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

193 

22671  194 
val decl_type_occs = fold_term_types 
20162  195 
(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

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

197 

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

198 
val declare_type_occsT = map_type_occs o fold_types decl_type_occsT; 
22671  199 
val declare_type_occs = map_type_occs o decl_type_occs; 
200 

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

201 

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

203 

21355  204 
fun constrain_tvar (xi, S) = 
205 
if S = dummyS then Vartab.delete_safe xi else Vartab.update (xi, S); 

206 

20162  207 
fun declare_constraints t = map_constraints (fn (types, sorts) => 
208 
let 

209 
val types' = fold_aterms 

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

211 
 Var v => Vartab.update v 

212 
 _ => I) t types; 

213 
val sorts' = fold_types (fold_atyps 

21355  214 
(fn TFree (x, S) => constrain_tvar ((x, ~1), S) 
215 
 TVar v => constrain_tvar v 

20162  216 
 _ => I)) t sorts; 
217 
in (types', sorts') end) 

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

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

220 

20162  221 

222 
(* common declarations *) 

223 

224 
fun declare_internal t = 

225 
declare_names t #> 

28625  226 
declare_type_occs t #> 
227 
map_sorts (Sorts.insert_term t); 

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

228 

20162  229 
fun declare_term t = 
230 
declare_internal t #> 

231 
declare_constraints t; 

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

232 

27280  233 
val declare_typ = declare_term o Logic.mk_type; 
234 

20303  235 
val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type); 
236 

22691  237 
val declare_thm = Thm.fold_terms declare_internal; 
21522  238 
fun thm_context th = declare_thm th (ProofContext.init (Thm.theory_of_thm th)); 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

239 

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

240 

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

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

242 

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

244 
let 
20162  245 
val names = names_of (fold declare_names ts ctxt); 
20084  246 
val xs = fst (Name.variants (map #1 frees) names); 
247 
in xs ~~ map snd frees end; 

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

248 

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

249 

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

250 

20303  251 
(** term bindings **) 
252 

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

20303  255 
let 
25051  256 
val u = Term.close_schematic_term t; 
257 
val U = Term.fastype_of u; 

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

20303  259 

260 
fun expand_binds ctxt = 

261 
let 

262 
val binds = binds_of ctxt; 

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

20303  265 

266 

267 

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

269 

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

272 

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

275 

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

276 

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

277 

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

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

279 

20084  280 
local 
281 

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

282 
fun no_dups [] = () 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

283 
 no_dups dups = error ("Duplicate fixed variable(s): " ^ commas_quote dups); 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

284 

20102  285 
fun new_fixes names' xs xs' = 
286 
map_names (K names') #> 

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

287 
fold declare_fixed xs #> 
20102  288 
map_fixes (fn fixes => (rev (xs ~~ xs') @ fixes)) #> 
20162  289 
fold (declare_constraints o Syntax.free) xs' #> 
20084  290 
pair xs'; 
291 

292 
in 

293 

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

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

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

296 
val _ = 
20084  297 
(case filter (can Name.dest_skolem) xs of [] => () 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

298 
 bads => error ("Illegal internal Skolem constant(s): " ^ commas_quote bads)); 
20084  299 
val _ = no_dups (duplicates (op =) xs); 
300 
val (ys, zs) = split_list (fixes_of ctxt); 

20102  301 
val names = names_of ctxt; 
20084  302 
val (xs', names') = 
20149  303 
if is_body ctxt then Name.variants xs names >> map Name.skolem 
20084  304 
else (no_dups (xs inter_string ys); no_dups (xs inter_string zs); 
305 
(xs, fold Name.declare xs names)); 

20102  306 
in ctxt > new_fixes names' xs xs' end; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

307 

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

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

311 
val xs = map (fn x => Name.clean x > can Name.dest_internal x ? Name.internal) raw_xs; 
4773b832f1b1
variant_fixes: preserve internal state, mark skolem only for body mode;
wenzelm
parents:
25573
diff
changeset

312 
val (xs', names') = Name.variants xs names >> (is_body ctxt ? map Name.skolem); 
20102  313 
in ctxt > new_fixes names' xs xs' end; 
20084  314 

315 
end; 

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

316 

20251  317 

318 
fun add_fixes_direct xs ctxt = ctxt 

319 
> set_body false 

320 
> (snd o add_fixes xs) 

321 
> restore_body ctxt; 

322 

323 
fun fix_frees t ctxt = ctxt 

324 
> add_fixes_direct 

325 
(rev (fold_aterms (fn Free (x, _) => 

21369  326 
if is_fixed ctxt x then I else insert (op =) x  _ => I) t [])); 
327 

328 
fun auto_fixes t ctxt = 

329 
(if is_body ctxt then ctxt else fix_frees t ctxt) 

20251  330 
> declare_term t; 
331 

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

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

333 
let 
24848  334 
val tfrees = Name.invents (names_of ctxt) Name.aT (length Ss) ~~ Ss; 
20162  335 
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

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

337 

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

338 

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

339 

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

341 

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

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

343 
let 
20162  344 
val declared_outer = is_declared outer; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

345 
val fixes_inner = fixes_of inner; 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

346 
val fixes_outer = fixes_of outer; 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

347 

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

348 
val gen_fixes = map #2 (Library.take (length fixes_inner  length fixes_outer, fixes_inner)); 
20162  349 
val still_fixed = not o member (op =) gen_fixes; 
22671  350 

351 
val type_occs_inner = type_occs_of inner; 

352 
fun gen_fixesT ts = 

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

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

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

357 

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

358 
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

359 

22671  360 
fun exportT_terms inner outer = 
361 
let val mk_tfrees = exportT_inst inner outer in 

362 
fn ts => ts > map 

31977  363 
(Term_Subst.generalize (mk_tfrees ts, []) 
22671  364 
(fold (Term.fold_types Term.maxidx_typ) ts ~1 + 1)) 
365 
end; 

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

366 

22671  367 
fun export_terms inner outer = 
368 
let val (mk_tfrees, tfrees) = export_inst inner outer in 

369 
fn ts => ts > map 

31977  370 
(Term_Subst.generalize (mk_tfrees ts, tfrees) 
22671  371 
(fold Term.maxidx_term ts ~1 + 1)) 
372 
end; 

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

373 

20303  374 
fun export_prf inner outer prf = 
375 
let 

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

20303  378 
val idx = Proofterm.maxidx_proof prf ~1 + 1; 
31977  379 
val gen_term = Term_Subst.generalize_option (tfrees, frees) idx; 
380 
val gen_typ = Term_Subst.generalizeT_option tfrees idx; 

20303  381 
in Proofterm.map_proof_terms_option gen_term gen_typ prf end; 
382 

22671  383 

384 
fun gen_export (mk_tfrees, frees) ths = 

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

385 
let 
22671  386 
val tfrees = mk_tfrees (map Thm.full_prop_of ths); 
387 
val maxidx = fold Thm.maxidx_thm ths ~1; 

388 
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

389 

22671  390 
fun exportT inner outer = gen_export (exportT_inst inner outer, []); 
391 
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

392 

21522  393 
fun export_morphism inner outer = 
394 
let 

395 
val fact = export inner outer; 

396 
val term = singleton (export_terms inner outer); 

397 
val typ = Logic.type_map term; 

29605  398 
in Morphism.morphism {binding = I, typ = typ, term = term, fact = fact} end; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

399 

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

400 

24765  401 

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

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

403 

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

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

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

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

407 
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

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

409 

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

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

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

412 
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

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

415 
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

416 
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

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

418 

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

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

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

422 

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

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

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

426 

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

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

428 
let 
21522  429 
val thy = ProofContext.theory_of ctxt; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

430 
val certT = Thm.ctyp_of thy; 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

431 
val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt; 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

432 
val instT' = map (fn (v, T) => (certT (TVar v), certT T)) instT; 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

433 
val ths' = map (Thm.instantiate (instT', [])) ths; 
20220  434 
in ((map #2 instT', ths'), ctxt') end; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

435 

20303  436 
fun import_prf is_open prf ctxt = 
437 
let 

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

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

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

441 

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

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

443 
let 
21522  444 
val thy = ProofContext.theory_of ctxt; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

445 
val cert = Thm.cterm_of thy; 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

446 
val certT = Thm.ctyp_of thy; 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

447 
val ((instT, inst), ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt; 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

448 
val instT' = map (fn (v, T) => (certT (TVar v), certT T)) instT; 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

449 
val inst' = map (fn (v, t) => (cert (Var v), cert t)) inst; 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

450 
val ths' = map (Thm.instantiate (instT', inst')) ths; 
20220  451 
in (((map #2 instT', map #2 inst'), ths'), ctxt') end; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

452 

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

453 

19926  454 
(* import/export *) 
455 

21287  456 
fun gen_trade imp exp f ctxt ths = 
20220  457 
let val ((_, ths'), ctxt') = imp ths ctxt 
21287  458 
in exp ctxt' ctxt (f ctxt' ths') end; 
19926  459 

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

460 
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

461 
val trade = gen_trade (import true) export; 
19926  462 

463 

20162  464 
(* focus on outermost parameters *) 
20149  465 

466 
fun forall_elim_prop t prop = 

20579  467 
Thm.beta_conversion false (Thm.capply (Thm.dest_arg prop) t) 
468 
> Thm.cprop_of > Thm.dest_arg; 

20149  469 

470 
fun focus goal ctxt = 

471 
let 

472 
val cert = Thm.cterm_of (Thm.theory_of_cterm goal); 

473 
val t = Thm.term_of goal; 

20162  474 
val ps = Term.variant_frees t (Term.strip_all_vars t); (*as they are printed :*) 
20149  475 
val (xs, Ts) = split_list ps; 
20797
c1f0bc7e7d80
renamed Variable.invent_fixes to Variable.variant_fixes;
wenzelm
parents:
20579
diff
changeset

476 
val (xs', ctxt') = variant_fixes xs ctxt; 
20220  477 
val ps' = ListPair.map (cert o Free) (xs', Ts); 
478 
val goal' = fold forall_elim_prop ps' goal; 

27119
c36c88fcdd22
focus: actually declare constraints for local parameters;
wenzelm
parents:
26714
diff
changeset

479 
val ctxt'' = ctxt' > fold (declare_constraints o Thm.term_of) ps'; 
32199  480 
in ((xs ~~ ps', goal'), ctxt'') end; 
20149  481 

20303  482 
fun focus_subgoal i st = 
483 
let 

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

30756  487 
fold bind_term no_binds #> 
20303  488 
fold (declare_constraints o Var) all_vars #> 
489 
focus (Thm.cprem_of st i) 

490 
end; 

491 

492 

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

493 

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

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

495 

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

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

497 

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

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

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

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

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

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

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

505 

20162  506 
val occs1 = type_occs_of ctxt1; 
507 
val occs2 = type_occs_of ctxt2; 

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

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

509 
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

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

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

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

513 
if null extras then () 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

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

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

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

517 

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

518 

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

520 

24694  521 
fun polymorphic_types ctxt ts = 
20003  522 
let 
523 
val ctxt' = fold declare_term ts ctxt; 

20162  524 
val occs = type_occs_of ctxt; 
525 
val occs' = type_occs_of ctxt'; 

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

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

31977  530 
(case Term_Subst.generalizeT types idx T of TVar v => insert (op =) v  _ => I) 
24694  531 
 _ => I) ts []; 
31977  532 
val ts' = map (Term_Subst.generalize (types, []) idx) ts; 
24694  533 
in (rev Ts', ts') end; 
534 

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

20003  536 

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

537 
end; 