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 (* creates a hashtable mapping each unique id to a node of the annotated
47 let get_ids_to_targets annobj =
49 let ids_to_targets = Hashtbl.create 503 in
50 let set_target id target =
52 ignore (Hashtbl.find ids_to_targets id) ;
53 raise (MoreThanOneTargetFor id)
55 Not_found -> Hashtbl.add ids_to_targets id target
57 let rec add_target_term t =
64 set_target id (C.Term t)
65 | C.ACast (id,va,ty) ->
66 set_target id (C.Term t) ;
69 | C.AProd (id,_,so,ta)
70 | C.ALambda (id,_,so,ta)
71 | C.ALetIn (id,_,so,ta) ->
72 set_target id (C.Term t) ;
76 set_target id (C.Term t) ;
77 List.iter add_target_term l
80 | C.AMutInd (id,_,_,_)
81 | C.AMutConstruct (id,_,_,_,_) ->
82 set_target id (C.Term t)
83 | C.AMutCase (id,_,_,_,ot,it,pl) ->
84 set_target id (C.Term t) ;
85 List.iter add_target_term (ot::it::pl)
86 | C.AFix (id,_,ifl) ->
87 set_target id (C.Term t) ;
89 (function (_,_,ty,bo) ->
93 | C.ACoFix (id,_,cfl) ->
94 set_target id (C.Term t) ;
96 (function (_,ty,bo) ->
101 let add_target_obj annobj =
103 C.ADefinition (id,_,bo,ty,_) ->
104 set_target id (C.Object annobj) ;
107 | C.AAxiom (id,_,ty,_) ->
108 set_target id (C.Object annobj) ;
110 | C.AVariable (id,_,None,ty) ->
111 set_target id (C.Object annobj) ;
113 | C.AVariable (id,_,Some bo,ty) ->
114 set_target id (C.Object annobj) ;
117 | C.ACurrentProof (id,_,cl,bo,ty) ->
118 set_target id (C.Object annobj) ;
119 List.iter (function (_,context, t) ->
122 Some (_,C.ADecl at) -> add_target_term at
123 | Some (_,C.ADef at) -> add_target_term at
126 add_target_term t) cl ;
129 | C.AInductiveDefinition (id,itl,_,_) ->
130 set_target id (C.Object annobj) ;
132 (function (_,_,arity,cl) ->
133 add_target_term arity ;
134 List.iter (function (_,ty,_) -> add_target_term ty) cl
137 add_target_obj annobj ;