(* *)
(******************************************************************************)
-let get_annotation_from_term annterm =
- let module C = Cic in
- match annterm with
- C.ARel (_,ann,_,_) -> ann
- | C.AVar (_,ann,_) -> ann
- | C.AMeta (_,ann,_) -> ann
- | C.ASort (_,ann,_) -> ann
- | C.AImplicit (_,ann) -> ann
- | C.ACast (_,ann,_,_) -> ann
- | C.AProd (_,ann,_,_,_) -> ann
- | C.ALambda (_,ann,_,_,_) -> ann
- | C.ALetIn (_,ann,_,_,_) -> ann
- | C.AAppl (_,ann,_) -> ann
- | C.AConst (_,ann,_,_) -> ann
- | C.AAbst (_,ann,_) -> ann
- | C.AMutInd (_,ann,_,_,_) -> ann
- | C.AMutConstruct (_,ann,_,_,_,_)-> ann
- | C.AMutCase (_,ann,_,_,_,_,_,_) -> ann
- | C.AFix (_,ann,_,_) -> ann
- | C.ACoFix (_,ann,_,_) -> ann
-;;
-
-let get_annotation_from_obj annobj =
- let module C = Cic in
- match annobj with
- C.ADefinition (_,ann,_,_,_,_) -> ann
- | C.AAxiom (_,ann,_,_,_) -> ann
- | C.AVariable (_,ann,_,_,_) -> ann
- | C.ACurrentProof (_,ann,_,_,_,_) -> ann
- | C.AInductiveDefinition (_,ann,_,_,_) -> ann
+let get_annotation ids_to_annotations xpath =
+ try
+ Some (Hashtbl.find ids_to_annotations xpath)
+ with
+ Not_found -> None
;;
-exception IdUnknown of string;;
+exception MoreThanOneTargetFor of Cic.id;;
-let get_annotation (annobj,ids_to_targets) xpath =
- try
- match Hashtbl.find ids_to_targets xpath with
- Cic.Object annobj -> get_annotation_from_obj annobj
- | Cic.Term annterm -> get_annotation_from_term annterm
- with
- Not_found -> raise (IdUnknown xpath)
+(* 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
;;