1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (******************************************************************************)
30 (* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
34 (******************************************************************************)
36 let get_annotation ids_to_annotations xpath =
38 Some (Hashtbl.find ids_to_annotations xpath)
43 exception MoreThanOneTargetFor of Cic.id;;
45 let get_ids_to_targets annobj =
47 let ids_to_targets = Hashtbl.create 503 in
48 let set_target id target =
50 ignore (Hashtbl.find ids_to_targets id) ;
51 raise (MoreThanOneTargetFor id)
53 Not_found -> Hashtbl.add ids_to_targets id target
55 let rec add_target_term t =
62 set_target id (C.Term t)
63 | C.ACast (id,va,ty) ->
64 set_target id (C.Term t) ;
67 | C.AProd (id,_,so,ta)
68 | C.ALambda (id,_,so,ta)
69 | C.ALetIn (id,_,so,ta) ->
70 set_target id (C.Term t) ;
74 set_target id (C.Term t) ;
75 List.iter add_target_term l
78 | C.AMutInd (id,_,_,_)
79 | C.AMutConstruct (id,_,_,_,_) ->
80 set_target id (C.Term t)
81 | C.AMutCase (id,_,_,_,ot,it,pl) ->
82 set_target id (C.Term t) ;
83 List.iter add_target_term (ot::it::pl)
84 | C.AFix (id,_,ifl) ->
85 set_target id (C.Term t) ;
87 (function (_,_,ty,bo) ->
91 | C.ACoFix (id,_,cfl) ->
92 set_target id (C.Term t) ;
94 (function (_,ty,bo) ->
99 let add_target_obj annobj =
101 C.ADefinition (id,_,bo,ty,_) ->
102 set_target id (C.Object annobj) ;
105 | C.AAxiom (id,_,ty,_) ->
106 set_target id (C.Object annobj) ;
108 | C.AVariable (id,_,None,ty) ->
109 set_target id (C.Object annobj) ;
111 | C.AVariable (id,_,Some bo,ty) ->
112 set_target id (C.Object annobj) ;
115 | C.ACurrentProof (id,_,cl,bo,ty) ->
116 set_target id (C.Object annobj) ;
117 List.iter (function (_,t) -> add_target_term t) cl ;
120 | C.AInductiveDefinition (id,itl,_,_) ->
121 set_target id (C.Object annobj) ;
123 (function (_,_,arity,cl) ->
124 add_target_term arity ;
125 List.iter (function (_,ty,_) -> add_target_term ty) cl
128 add_target_obj annobj ;