]> matita.cs.unibo.it Git - helm.git/blob - helm/interface/cicParser2.ml
Main code clean-up.
[helm.git] / helm / interface / cicParser2.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 (******************************************************************************)
27 (*                                                                            *)
28 (*                               PROJECT HELM                                 *)
29 (*                                                                            *)
30 (*                Claudio Sacerdoti Coen <sacerdot@@cs.unibo.it>              *)
31 (*                                 24/01/2000                                 *)
32 (*                                                                            *)
33 (* This module is the objects level of a parser for cic objects from xml      *)
34 (* files to the internal representation. It uses the module cicParser3        *)
35 (* cicParser3 (terms level) and it is used only through cicParser2 (top       *)
36 (* level).                                                                    *)
37 (*                                                                            *)
38 (******************************************************************************)
39
40 exception IllFormedXml of int;;
41 exception NotImplemented;;
42
43 (* Utility functions that transform a Pxp attribute into something useful *)
44
45 (* mk_absolute_uris "n1: v1 ... vn n2 : u1 ... un ...."      *)
46 (* returns [(n1,[absolute_uri_for_v1 ; ... ; absolute_uri_for_vn]) ; (n2,...) *)
47 let mk_absolute_uris s =
48  let l = (Str.split (Str.regexp ":") s) in
49   let absolute_of_relative n v =
50    let module P3 = CicParser3 in
51     let rec mkburi =
52      function
53         (0,_) -> "/"
54       | (n,he::tl) when n > 0 ->
55          "/" ^ he ^ mkburi (n - 1, tl)
56       | _ -> raise (IllFormedXml 12)
57     in
58      let m = List.length !P3.current_sp - (int_of_string n) in
59       let buri = mkburi (m, !P3.current_sp) in
60        UriManager.uri_of_string ("cic:" ^ buri ^ v ^ ".var")
61   in
62    let rec absolutize =
63     function
64        [] -> []
65      | [no ; vs] ->
66         let vars = (Str.split (Str.regexp " ") vs) in
67          [(int_of_string no, List.map (absolute_of_relative no) vars)]
68      | no::vs::tl -> 
69         let vars = (Str.split (Str.regexp " ") vs) in
70          let rec add_prefix =
71           function
72              [no2] -> ([], no2)
73            | he::tl ->
74               let (pvars, no2) = add_prefix tl in
75                ((absolute_of_relative no he)::pvars, no2)
76            | _ -> raise (IllFormedXml 11)
77          in
78           let (pvars, no2) = add_prefix vars in
79            (int_of_string no, pvars)::(absolutize (no2::tl))
80      | _ -> raise (IllFormedXml 10)
81    in
82     (* last parameter must be applied first *)
83     absolutize l
84 ;;
85
86 let option_uri_list_of_attr a1 a2 =
87  let module T = Pxp_types in
88   let parameters =
89    match a1 with
90       T.Value s -> mk_absolute_uris s
91     | _ -> raise (IllFormedXml 0)
92   in
93    match a2 with
94       T.Value "POSSIBLE" -> Cic.Possible parameters
95     | T.Implied_value -> Cic.Actual parameters
96     | _ -> raise (IllFormedXml 0)
97 ;;
98
99 let uri_list_of_attr a =
100  let module T = Pxp_types in
101   match a with
102      T.Value s -> mk_absolute_uris s
103    | _ -> raise (IllFormedXml 0)
104 ;;
105
106 let string_of_attr a =
107  let module T = Pxp_types in
108   match a with
109      T.Value s -> s
110    | _ -> raise (IllFormedXml 0)
111 ;;
112
113 let int_of_attr a =
114  int_of_string (string_of_attr a)
115 ;;
116
117 let bool_of_attr a =
118  bool_of_string (string_of_attr a)
119 ;;
120
121 (* Other utility functions *)
122
123 let get_content n =
124  match n#sub_nodes with
125     [ t ] -> t
126   | _     -> raise (IllFormedXml 1)
127 ;;
128
129 let register_id id node =
130  if !CicParser3.process_annotations then
131   match !CicParser3.ids_to_targets with
132      None -> assert false
133    | Some ids_to_targets ->
134       Hashtbl.add ids_to_targets id (Cic.Object node)
135 ;;
136
137 (* Functions that, given the list of sons of a node of the cic dom (objects   *)
138 (* level), retrieve the internal representation associated to the node.       *)
139 (* Everytime a cic term subtree is found, it is translated to the internal    *)
140 (* representation using the method to_cic_term defined in cicParser3.         *)
141 (* Each function raise IllFormedXml if something goes wrong, but this should  *)
142 (* be impossible due to the presence of the dtd                               *)
143 (* The functions should really be obvious looking at their name and the cic   *)
144 (* dtd                                                                        *)
145
146 (* called when a CurrentProof is found *)
147 let get_conjs_value_type l =
148  let rec rget (c, v, t) l =
149   let module D = Pxp_document in
150    match l with
151       [] -> (c, v, t)
152     | conj::tl when conj#node_type = D.T_element "Conjecture" ->
153        let no = int_of_attr (conj#attribute "no")
154        and typ = (get_content conj)#extension#to_cic_term in
155         rget ((no, typ)::c, v, t) tl
156     | value::tl when value#node_type = D.T_element "body" ->
157        let v' = (get_content value)#extension#to_cic_term in
158         (match v with
159             None -> rget (c, Some v', t) tl
160           | _    -> raise (IllFormedXml 2)
161         )
162     | typ::tl when typ#node_type = D.T_element "type" ->
163        let t' = (get_content typ)#extension#to_cic_term in
164         (match t with
165             None -> rget (c, v, Some t') tl
166           | _    -> raise (IllFormedXml 3)
167         )
168     | _ -> raise (IllFormedXml 4)
169  in
170   match rget ([], None, None) l with
171      (c, Some v, Some t) -> (c, v, t)
172    | _ -> raise (IllFormedXml 5)
173 ;;
174
175 (* used only by get_inductive_types; called one time for each inductive  *)
176 (* definitions in a block of inductive definitions                       *)
177 let get_names_arity_constructors l =
178  let rec rget (a,c) l =
179   let module D = Pxp_document in
180    match l with
181       [] -> (a, c)
182     | arity::tl when arity#node_type = D.T_element "arity" ->
183        let a' = (get_content arity)#extension#to_cic_term in
184         rget (Some a',c) tl
185     | con::tl when con#node_type = D.T_element "Constructor" ->
186        let id = string_of_attr (con#attribute "name")
187        and ty = (get_content con)#extension#to_cic_term in
188          rget (a,(id,ty,ref None)::c) tl
189     | _ -> raise (IllFormedXml 9)
190  in
191   match rget (None,[]) l with
192      (Some a, c) -> (a, List.rev c)
193    | _ -> raise (IllFormedXml 8)
194 ;;
195
196 (* called when an InductiveDefinition is found *)
197 let rec get_inductive_types =
198  function
199     []     -> []
200   | he::tl ->
201      let tyname    = string_of_attr (he#attribute "name")
202      and inductive = bool_of_attr   (he#attribute "inductive")
203      and (arity,cons) =
204       get_names_arity_constructors (he#sub_nodes)
205      in
206       (tyname,inductive,arity,cons)::(get_inductive_types tl) (*CSC 0 a caso *)
207 ;;
208
209 (* This is the main function and also the only one used directly from *)
210 (* cicParser. Given the root of the dom tree, it returns the internal *)
211 (* representation of the cic object described in the tree             *)
212 (* It uses the previous functions and the to_cic_term method defined  *)
213 (* in cicParser3 (used for subtrees that encode cic terms)            *)
214 let rec get_term n =
215  let module D = Pxp_document in
216  let module C = Cic in
217   let ntype = n # node_type in
218   match ntype with
219     D.T_element "Definition" ->
220       let id = string_of_attr (n # attribute "name")
221       and params =
222        option_uri_list_of_attr (n#attribute "params") (n#attribute "paramMode")
223       and (value, typ) = 
224        let sons = n#sub_nodes in
225         match sons with
226           [v ; t] when
227             v#node_type = D.T_element "body" &&
228             t#node_type = D.T_element "type" ->
229              let v' = get_content v
230              and t' = get_content t in
231               (v'#extension#to_cic_term, t'#extension#to_cic_term)
232         | _ -> raise (IllFormedXml 6)
233       and xid = string_of_attr (n#attribute "id") in
234        let res = C.ADefinition (xid, ref None, id, value, typ, params) in
235         register_id xid res ;
236         res
237   | D.T_element "Axiom" ->
238       let id = string_of_attr (n # attribute "name")
239       and params = uri_list_of_attr (n # attribute "params")
240       and typ = 
241        (get_content (get_content n))#extension#to_cic_term
242       and xid = string_of_attr (n#attribute "id") in
243        let res = C.AAxiom (xid, ref None, id, typ, params) in
244         register_id xid res ;
245         res
246   | D.T_element "CurrentProof" ->
247      let name = string_of_attr (n#attribute "name")
248      and xid = string_of_attr (n#attribute "id") in
249      let sons = n#sub_nodes in
250       let (conjs, value, typ) = get_conjs_value_type sons in
251        let res = C.ACurrentProof (xid, ref None, name, conjs, value, typ) in
252         register_id xid res ;
253         res
254   | D.T_element "InductiveDefinition" ->
255      let sons = n#sub_nodes
256      and xid = string_of_attr (n#attribute "id") in
257       let inductiveTypes = get_inductive_types sons
258       and params = uri_list_of_attr (n#attribute "params")
259       and nparams = int_of_attr (n#attribute "noParams") in
260        let res =
261         C.AInductiveDefinition (xid, ref None, inductiveTypes, params, nparams)
262        in
263         register_id xid res ;
264         res
265   | D.T_element "Variable" ->
266      let name = string_of_attr (n#attribute "name")
267      and xid = string_of_attr (n#attribute "id")
268      and (body, typ) = 
269       let sons = n#sub_nodes in
270        match sons with
271           [b ; t] when
272             b#node_type = D.T_element "body" &&
273             t#node_type = D.T_element "type" ->
274              let b' = get_content b
275              and t' = get_content t in
276               (Some (b'#extension#to_cic_term), t'#extension#to_cic_term)
277         | [t] when t#node_type = D.T_element "type" ->
278              let t' = get_content t in
279               (None, t'#extension#to_cic_term)
280         | _ -> raise (IllFormedXml 6)
281      in
282       let res = C.AVariable (xid,ref None,name,body,typ) in
283        register_id xid res ;
284        res
285   | D.T_element _
286   | D.T_data
287   | _ ->
288      raise (IllFormedXml 7)
289 ;;