158 end; |
158 end; |
159 |
159 |
160 |
160 |
161 (* zero var indexes *) |
161 (* zero var indexes *) |
162 |
162 |
163 fun zero_var_inst vars = |
163 structure TVars = Table(type key = indexname * sort val ord = Term_Ord.tvar_ord); |
164 fold (fn v as ((x, i), X) => fn (inst, used) => |
164 structure Vars = Table(type key = indexname * typ val ord = Term_Ord.var_ord); |
165 let |
165 |
166 val (x', used') = Name.variant (if Name.is_bound x then "u" else x) used; |
166 fun zero_var_inst mk (v as ((x, i), X)) (inst, used) = |
167 in if x = x' andalso i = 0 then (inst, used') else ((v, ((x', 0), X)) :: inst, used') end) |
167 let |
168 vars ([], Name.context) |> #1; |
168 val (x', used') = Name.variant (if Name.is_bound x then "u" else x) used; |
|
169 in if x = x' andalso i = 0 then (inst, used') else ((v, mk ((x', 0), X)) :: inst, used') end; |
169 |
170 |
170 fun zero_var_indexes_inst ts = |
171 fun zero_var_indexes_inst ts = |
171 let |
172 let |
172 val tvars = sort Term_Ord.tvar_ord (fold Term.add_tvars ts []); |
173 val (instT, _) = |
173 val instT = map (apsnd TVar) (zero_var_inst tvars); |
174 TVars.fold (zero_var_inst TVar o #1) |
174 val vars = sort Term_Ord.var_ord (map (apsnd (instantiateT instT)) (fold Term.add_vars ts [])); |
175 ((fold o fold_types o fold_atyps) (fn TVar v => |
175 val inst = map (apsnd Var) (zero_var_inst vars); |
176 TVars.insert (K true) (v, ()) | _ => I) ts TVars.empty) |
|
177 ([], Name.context); |
|
178 val (inst, _) = |
|
179 Vars.fold (zero_var_inst Var o #1) |
|
180 ((fold o fold_aterms) (fn Var (xi, T) => |
|
181 Vars.insert (K true) ((xi, instantiateT instT T), ()) | _ => I) ts Vars.empty) |
|
182 ([], Name.context); |
176 in (instT, inst) end; |
183 in (instT, inst) end; |
177 |
184 |
178 fun zero_var_indexes t = instantiate (zero_var_indexes_inst [t]) t; |
185 fun zero_var_indexes t = instantiate (zero_var_indexes_inst [t]) t; |
179 |
186 |
180 end; |
187 end; |