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
79 | C.AMutInd (id,_,_,_)
80 | C.AMutConstruct (id,_,_,_,_) ->
81 set_target id (C.Term t)
82 | C.AMutCase (id,_,_,_,ot,it,pl) ->
83 set_target id (C.Term t) ;
84 List.iter add_target_term (ot::it::pl)
85 | C.AFix (id,_,ifl) ->
86 set_target id (C.Term t) ;
88 (function (_,_,ty,bo) ->
92 | C.ACoFix (id,_,cfl) ->
93 set_target id (C.Term t) ;
95 (function (_,ty,bo) ->
100 let add_target_obj annobj =
102 C.ADefinition (id,_,bo,ty,_) ->
103 set_target id (C.Object annobj) ;
106 | C.AAxiom (id,_,ty,_) ->
107 set_target id (C.Object annobj) ;
109 | C.AVariable (id,_,None,ty) ->
110 set_target id (C.Object annobj) ;
112 | C.AVariable (id,_,Some bo,ty) ->
113 set_target id (C.Object annobj) ;
116 | C.ACurrentProof (id,_,cl,bo,ty) ->
117 set_target id (C.Object annobj) ;
118 List.iter (function (cid,_,context, t) as annconj ->
119 set_target cid (C.Conjecture annconj) ;
121 (function ((hid,h) as annhyp) ->
122 set_target hid (C.Hypothesis annhyp) ;
124 Some (_,C.ADecl at) -> add_target_term at
125 | Some (_,C.ADef at) -> add_target_term at
128 add_target_term t) cl ;
131 | C.AInductiveDefinition (id,itl,_,_) ->
132 set_target id (C.Object annobj) ;
134 (function (_,_,arity,cl) ->
135 add_target_term arity ;
136 List.iter (function (_,ty,_) -> add_target_term ty) cl
139 add_target_obj annobj ;