]> matita.cs.unibo.it Git - helm.git/blob - helm/interface/annotationParser2.ml
Main code clean-up.
[helm.git] / helm / interface / annotationParser2.ml
1 (* Copyright (C) 2000, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 exception IllFormedXml of int;;
27
28 (* Utility functions that transform a Pxp attribute into something useful *)
29
30 let string_of_attr a =
31  let module T = Pxp_types in
32   match a with
33      T.Value s -> s
34    | _ -> raise (IllFormedXml 0)
35 ;;
36
37 exception DontKnowWhatToDo;;
38
39 let rec string_of_annotations n =
40  let module D = Pxp_document in
41  let module T = Pxp_types in
42   match n#node_type with
43      D.T_element s ->
44       "<" ^ s ^
45       List.fold_right
46        (fun att i ->
47          match n#attribute att with
48             T.Value s -> " " ^ att ^ "=\"" ^ s ^ "\"" ^ i
49           | T.Implied_value -> i
50           | T.Valuelist l -> " " ^ att ^ "=\"" ^ String.concat " " l ^ "\"" ^ i
51        ) (n#attribute_names) "" ^
52       (match n#sub_nodes with
53           [] -> "/>"
54         | l ->
55            ">" ^
56            String.concat "" (List.map string_of_annotations l) ^
57            "</" ^ s ^ ">"
58       )
59    | D.T_data -> n#data
60    | _ -> raise DontKnowWhatToDo
61 ;;
62
63 let get_annotation n =
64  String.concat "" (List.map string_of_annotations (n#sub_nodes))
65 ;;
66
67 let annotate_object ann obj =
68  let module C = Cic in
69   let rann =
70    match obj with
71       C.ADefinition (_, rann, _, _, _, _) -> rann
72     | C.AAxiom (_, rann, _, _, _) -> rann
73     | C.AVariable (_, rann, _, _, _) -> rann
74     | C.ACurrentProof (_, rann, _, _, _, _) -> rann
75     | C.AInductiveDefinition (_, rann, _, _, _) -> rann
76   in
77    rann := Some ann
78 ;;
79
80 let annotate_term ann term =
81  let module C = Cic in
82   let rann =
83    match term with
84       C.ARel (_, rann, _, _) -> rann
85     | C.AVar (_, rann, _) -> rann
86     | C.AMeta (_, rann, _) -> rann
87     | C.ASort (_, rann, _) -> rann
88     | C.AImplicit (_, rann) -> rann
89     | C.ACast (_, rann, _, _) -> rann
90     | C.AProd (_, rann, _, _, _) -> rann
91     | C.ALambda (_, rann, _, _, _) -> rann
92     | C.ALetIn (_, rann, _, _, _) -> rann
93     | C.AAppl (_, rann, _) -> rann
94     | C.AConst (_, rann, _, _) -> rann
95     | C.AAbst (_, rann, _) -> rann
96     | C.AMutInd (_, rann, _, _, _) -> rann
97     | C.AMutConstruct (_, rann, _, _, _, _) -> rann
98     | C.AMutCase (_, rann, _, _, _, _, _, _) -> rann
99     | C.AFix (_, rann, _, _) -> rann
100     | C.ACoFix (_, rann, _, _) -> rann
101   in
102    rann := Some ann
103 ;;
104
105 let annotate ids_to_targets n =
106  let module D = Pxp_document in
107  let module C = Cic in
108   let annotate_elem n =
109    let ntype = n # node_type in
110    match ntype with
111      D.T_element "Annotation" ->
112        let of_uri = string_of_attr (n # attribute "of") in
113         begin
114          try
115           match Hashtbl.find ids_to_targets of_uri with
116              C.Object o -> annotate_object (get_annotation n) o
117            | C.Term t -> annotate_term (get_annotation n) t
118          with
119           Not_found -> assert false
120         end
121    | D.T_element _ | D.T_data ->
122       raise (IllFormedXml 1)
123    | _ -> raise DontKnowWhatToDo
124   in
125    match n # node_type with
126       D.T_element "Annotations" ->
127        List.iter annotate_elem (n # sub_nodes)
128     | _ -> raise (IllFormedXml 2)
129 ;;