let resolve name =
try
HExtlib.filter_map
- (fun (name',nref) -> if name'=name then Some nref else None) !aliases
+ (fun (_,name',nref) -> if name'=name then Some nref else None) !aliases
with
Not_found -> raise (ObjectNotFound (lazy name))
;;
+let aliases_of uri =
+ try
+ HExtlib.filter_map
+ (fun (uri',_,nref) -> if NUri.eq uri' uri then Some nref else None) !aliases
+ with
+ Not_found -> raise (ObjectNotFound (lazy (NUri.string_of_uri uri)))
+;;
+
let add_obj u obj =
storage := (u,obj)::!storage;
let _,height,_,_,obj = obj in
let references =
match obj with
NCic.Constant (_,name,None,_,_) ->
- [name,NReference.reference_of_spec u NReference.Decl]
+ [u,name,NReference.reference_of_spec u NReference.Decl]
| NCic.Constant (_,name,Some _,_,_) ->
- [name,NReference.reference_of_spec u (NReference.Def height)]
+ [u,name,NReference.reference_of_spec u (NReference.Def height)]
| NCic.Fixpoint (is_ind,fl,_) ->
HExtlib.list_mapi
(fun (_,name,recno,_,_) i ->
if is_ind then
- name,NReference.reference_of_spec u (NReference.Fix(i,recno,height))
+ u,name,NReference.reference_of_spec u(NReference.Fix(i,recno,height))
else
- name,NReference.reference_of_spec u (NReference.CoFix i)) fl
+ u,name,NReference.reference_of_spec u (NReference.CoFix i)) fl
| NCic.Inductive (inductive,leftno,il,_) ->
List.flatten
(HExtlib.list_mapi
(fun (_,iname,_,cl) i ->
HExtlib.list_mapi
(fun (_,cname,_) j->
- cname,NReference.reference_of_spec u (NReference.Con (i,j,leftno))
+ u,cname,
+ NReference.reference_of_spec u (NReference.Con (i,j+1,leftno))
) cl @
- [iname,
+ [u,iname,
NReference.reference_of_spec u
(NReference.Ind (inductive,i,leftno))]
) il)