diff options
Diffstat (limited to 'pretyping/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 64 |
1 files changed, 32 insertions, 32 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index b82f18da7..b6e8f9d13 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -440,12 +440,12 @@ let compute_var_aliases sign = (match kind_of_term t with | Var id' -> let aliases_of_id = - try Idmap.find id' aliases with Not_found -> [] in - Idmap.add id (aliases_of_id@[t]) aliases + try Id.Map.find id' aliases with Not_found -> [] in + Id.Map.add id (aliases_of_id@[t]) aliases | _ -> - Idmap.add id [t] aliases) + Id.Map.add id [t] aliases) | None -> aliases) - sign Idmap.empty + sign Id.Map.empty let compute_rel_aliases var_aliases rels = snd (List.fold_right (fun (_,b,t) (n,aliases) -> @@ -455,7 +455,7 @@ let compute_rel_aliases var_aliases rels = (match kind_of_term t with | Var id' -> let aliases_of_n = - try Idmap.find id' var_aliases with Not_found -> [] in + try Id.Map.find id' var_aliases with Not_found -> [] in Int.Map.add n (aliases_of_n@[t]) aliases | Rel p -> let aliases_of_n = @@ -480,7 +480,7 @@ let lift_aliases n (var_aliases,rel_aliases as aliases) = let get_alias_chain_of aliases x = match kind_of_term x with | Rel n -> (try Int.Map.find n (snd aliases) with Not_found -> []) - | Var id -> (try Idmap.find id (fst aliases) with Not_found -> []) + | Var id -> (try Id.Map.find id (fst aliases) with Not_found -> []) | _ -> [] let normalize_alias_opt aliases x = @@ -508,7 +508,7 @@ let extend_alias (_,b,_) (var_aliases,rel_aliases) = (match kind_of_term t with | Var id' -> let aliases_of_binder = - try Idmap.find id' var_aliases with Not_found -> [] in + try Id.Map.find id' var_aliases with Not_found -> [] in Int.Map.add 1 (aliases_of_binder@[t]) rel_aliases | Rel p -> let aliases_of_binder = @@ -545,15 +545,15 @@ let rec expand_vars_in_term_using aliases t = match kind_of_term t with let expand_vars_in_term env = expand_vars_in_term_using (make_alias_map env) let free_vars_and_rels_up_alias_expansion aliases c = - let acc1 = ref Int.Set.empty and acc2 = ref Idset.empty in - let cache_rel = ref Int.Set.empty and cache_var = ref Idset.empty in + let acc1 = ref Int.Set.empty and acc2 = ref Id.Set.empty in + let cache_rel = ref Int.Set.empty and cache_var = ref Id.Set.empty in let is_in_cache depth = function | Rel n -> Int.Set.mem (n-depth) !cache_rel - | Var s -> Idset.mem s !cache_var + | Var s -> Id.Set.mem s !cache_var | _ -> false in let put_in_cache depth = function | Rel n -> cache_rel := Int.Set.add (n-depth) !cache_rel - | Var s -> cache_var := Idset.add s !cache_var + | Var s -> cache_var := Id.Set.add s !cache_var | _ -> () in let rec frec (aliases,depth) c = match kind_of_term c with @@ -562,11 +562,11 @@ let free_vars_and_rels_up_alias_expansion aliases c = put_in_cache depth ck; let c = expansion_of_var aliases c in match kind_of_term c with - | Var id -> acc2 := Idset.add id !acc2 + | Var id -> acc2 := Id.Set.add id !acc2 | Rel n -> if n >= depth+1 then acc1 := Int.Set.add (n-depth) !acc1 | _ -> frec (aliases,depth) c end | Const _ | Ind _ | Construct _ -> - acc2 := List.fold_right Idset.add (vars_of_global (Global.env()) c) !acc2 + acc2 := List.fold_right Id.Set.add (vars_of_global (Global.env()) c) !acc2 | _ -> iter_constr_with_full_binders (fun d (aliases,depth) -> (extend_alias d aliases,depth+1)) @@ -580,10 +580,10 @@ let free_vars_and_rels_up_alias_expansion aliases c = (************************************) type clear_dependency_error = -| OccurHypInSimpleClause of identifier option +| OccurHypInSimpleClause of Id.t option | EvarTypingBreak of existential -exception ClearDependencyError of identifier * clear_dependency_error +exception ClearDependencyError of Id.t * clear_dependency_error open Store.Field @@ -624,7 +624,7 @@ let rec check_and_clear_in_constr evdref err ids c = (* Check if some id to clear occurs in the instance a of rid in ev and remember the dependency *) match - List.filter (fun id -> List.mem id ids) (Idset.elements (collect_vars a)) + List.filter (fun id -> List.mem id ids) (Id.Set.elements (collect_vars a)) with | id :: _ -> (hy,ar,(rid,id)::ri) | _ -> @@ -680,7 +680,7 @@ let clear_hyps_in_evi evdref hyps concl ids = match !vk with | VKnone -> vk | VKvalue (v,d) -> - if (List.for_all (fun e -> not (Idset.mem e d)) ids) then + if (List.for_all (fun e -> not (Id.Set.mem e d)) ids) then (* v does depend on any of ids, it's ok *) vk else @@ -728,7 +728,7 @@ let get_actual_deps aliases l t = let (fv_rels,fv_ids) = free_vars_and_rels_up_alias_expansion aliases t in List.filter (fun c -> match kind_of_term c with - | Var id -> Idset.mem id fv_ids + | Var id -> Id.Set.mem id fv_ids | Rel n -> Int.Set.mem n fv_rels | _ -> assert false) l @@ -838,23 +838,23 @@ let make_projectable_subst aliases sigma evi args = let l = try Constrmap.find cstr cstrs with Not_found -> [] in Constrmap.add cstr ((args,id)::l) cstrs | _ -> cstrs in - (rest,Idmap.add id [a,normalize_alias_opt aliases a,id] all,cstrs) + (rest,Id.Map.add id [a,normalize_alias_opt aliases a,id] all,cstrs) | Some c, a::rest -> let a = whd_evar sigma a in (match kind_of_term c with | Var id' -> let idc = normalize_alias_var evar_aliases id' in - let sub = try Idmap.find idc all with Not_found -> [] in + let sub = try Id.Map.find idc all with Not_found -> [] in if List.exists (fun (c,_,_) -> eq_constr a c) sub then (rest,all,cstrs) else (rest, - Idmap.add idc ((a,normalize_alias_opt aliases a,id)::sub) all, + Id.Map.add idc ((a,normalize_alias_opt aliases a,id)::sub) all, cstrs) | _ -> - (rest,Idmap.add id [a,normalize_alias_opt aliases a,id] all,cstrs)) + (rest,Id.Map.add id [a,normalize_alias_opt aliases a,id] all,cstrs)) | _ -> anomaly "Instance does not match its signature") - sign (Array.rev_to_list args,Idmap.empty,Constrmap.empty) in + sign (Array.rev_to_list args,Id.Map.empty,Constrmap.empty) in (full_subst,cstr_subst) let make_pure_subst evi args = @@ -993,10 +993,10 @@ let find_projectable_constructor env evd cstr k args cstr_subst = type evar_projection = | ProjectVar -| ProjectEvar of existential * evar_info * identifier * evar_projection +| ProjectEvar of existential * evar_info * Id.t * evar_projection exception NotUnique -exception NotUniqueInType of (identifier * evar_projection) list +exception NotUniqueInType of (Id.t * evar_projection) list let rec assoc_up_to_alias sigma aliases y yc = function | [] -> raise Not_found @@ -1039,7 +1039,7 @@ let rec find_projectable_vars with_evars aliases sigma y subst = | _ -> anomaly "More than one non var in aliases class of evar instance" else subst' in - Idmap.fold is_projectable subst [] + Id.Map.fold is_projectable subst [] (* [filter_solution] checks if one and only one possible projection exists * among a set of solutions to a projection problem *) @@ -1199,13 +1199,13 @@ let filter_candidates evd evk filter candidates = | Some l, Some filter -> let ids = List.map pi1 (List.filter_with filter (evar_context evi)) in Some (List.filter (fun a -> - List.subset (Idset.elements (collect_vars a)) ids) l) + List.subset (Id.Set.elements (collect_vars a)) ids) l) let closure_of_filter evd evk filter = let evi = Evd.find_undefined evd evk in let vars = collect_vars (evar_concl evi) in let ids = List.map pi1 (evar_context evi) in - let test id b = b || Idset.mem id vars in + let test id b = b || Id.Set.mem id vars in let newfilter = List.map2 test ids filter in if eq_filter newfilter (evar_filter evi) then None else Some newfilter @@ -1372,7 +1372,7 @@ let rec is_constrainable_in k (ev,(fv_rels,fv_ids) as g) t = | Ind _ -> Array.for_all (is_constrainable_in k g) args | Prod (_,t1,t2) -> is_constrainable_in k g t1 && is_constrainable_in k g t2 | Evar (ev',_) -> not (Int.equal ev' ev) (*If ev' needed, one may also try to restrict it*) - | Var id -> Idset.mem id fv_ids + | Var id -> Id.Set.mem id fv_ids | Rel n -> n <= k || Int.Set.mem n fv_rels | Sort _ -> true | _ -> (* We don't try to be more clever *) true @@ -1380,7 +1380,7 @@ let rec is_constrainable_in k (ev,(fv_rels,fv_ids) as g) t = let has_constrainable_free_vars evd aliases k ev (fv_rels,fv_ids as fvs) t = let t = expansion_of_var aliases t in match kind_of_term t with - | Var id -> Idset.mem id fv_ids + | Var id -> Id.Set.mem id fv_ids | Rel n -> n <= k || Int.Set.mem n fv_rels | _ -> is_constrainable_in k (ev,fvs) t @@ -1536,7 +1536,7 @@ let solve_candidates conv_algo env evd (evk,argsv as ev) rhs = *) exception NotInvertibleUsingOurAlgorithm of constr -exception NotEnoughInformationToProgress of (identifier * evar_projection) list +exception NotEnoughInformationToProgress of (Id.t * evar_projection) list exception OccurCheckIn of evar_map * constr let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs = @@ -1954,7 +1954,7 @@ let empty_valcon = None (* Builds a value constraint *) let mk_valcon c = Some c -let idx = id_of_string "x" +let idx = Id.of_string "x" (* Refining an evar to a product *) |