+(* creates a hashtable mapping each unique id to a node of the annotated
+object *)
+let get_ids_to_targets annobj =
+ let module C = Cic in
+ let ids_to_targets = Hashtbl.create 503 in
+ let set_target id target =
+ try
+ ignore (Hashtbl.find ids_to_targets id) ;
+ raise (MoreThanOneTargetFor id)
+ with
+ Not_found -> Hashtbl.add ids_to_targets id target
+ in
+ let rec add_target_term t =
+ match t with
+ C.ARel (id,_,_,_)
+ | C.AMeta (id,_,_)
+ | C.ASort (id,_)
+ | C.AImplicit (id, _) ->
+ set_target id (C.Term t)
+ | C.ACast (id,va,ty) ->
+ set_target id (C.Term t) ;
+ add_target_term va ;
+ add_target_term ty
+ | C.AProd (id,_,so,ta)
+ | C.ALambda (id,_,so,ta)
+ | C.ALetIn (id,_,so,ta) ->
+ set_target id (C.Term t) ;
+ add_target_term so ;
+ add_target_term ta
+ | C.AAppl (id,l) ->
+ set_target id (C.Term t) ;
+ List.iter add_target_term l
+ | C.AVar (id,_,exp_named_subst)
+ | C.AConst (id,_,exp_named_subst)
+ | C.AMutInd (id,_,_,exp_named_subst)
+ | C.AMutConstruct (id,_,_,_,exp_named_subst) ->
+ set_target id (C.Term t) ;
+ List.iter (function (_,t) -> add_target_term t) exp_named_subst
+ | C.AMutCase (id,_,_,ot,it,pl) ->
+ set_target id (C.Term t) ;
+ List.iter add_target_term (ot::it::pl)
+ | C.AFix (id,_,ifl) ->
+ set_target id (C.Term t) ;
+ List.iter
+ (function (_,_,_,ty,bo) ->
+ add_target_term ty ;
+ add_target_term bo
+ ) ifl
+ | C.ACoFix (id,_,cfl) ->
+ set_target id (C.Term t) ;
+ List.iter
+ (function (_,_,ty,bo) ->
+ add_target_term ty ;
+ add_target_term bo
+ ) cfl
+ in
+ let add_target_obj annobj =
+ match annobj with
+ C.AConstant (id,idbody,_,bo,ty,_,_) ->
+ set_target id (C.Object annobj) ;
+ (match idbody,bo with
+ Some idbody,Some bo ->
+ set_target idbody (C.ConstantBody annobj) ;
+ add_target_term bo
+ | None, None -> ()
+ | _,_ -> assert false
+ ) ;
+ add_target_term ty
+ | C.AVariable (id,_,None,ty,_,_) ->
+ set_target id (C.Object annobj) ;
+ add_target_term ty
+ | C.AVariable (id,_,Some bo,ty,_,_) ->
+ set_target id (C.Object annobj) ;
+ add_target_term bo ;
+ add_target_term ty
+ | C.ACurrentProof (id,idbody,_,cl,bo,ty,_,_) ->
+ set_target id (C.Object annobj) ;
+ set_target idbody (C.ConstantBody annobj) ;
+ List.iter (function (cid,_,context, t) as annconj ->
+ set_target cid (C.Conjecture annconj) ;
+ List.iter
+ (function ((hid,h) as annhyp) ->
+ set_target hid (C.Hypothesis annhyp) ;
+ match h with
+ Some (_,C.ADecl at) -> add_target_term at
+ | Some (_,C.ADef at) -> add_target_term at
+ | None -> ()
+ ) context;
+ add_target_term t) cl ;
+ add_target_term bo ;
+ add_target_term ty
+ | C.AInductiveDefinition (id,itl,_,_,_) ->
+ set_target id (C.Object annobj) ;
+ List.iter
+ (function (_,_,_,arity,cl) ->
+ add_target_term arity ;
+ List.iter (function (_,ty) -> add_target_term ty) cl
+ ) itl
+ in
+ add_target_obj annobj ;
+ ids_to_targets