]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic/cicParser2.ml
- implemented inductive type rendering
[helm.git] / helm / ocaml / cic / 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   (* TODO ZACK implement attributes parsing from XML. ATM, parsing always
44   * returns the empty list of attributes reported here *)
45 let obj_attributes = []
46 let get_obj_attributes (n: 'a Pxp_document.node) =
47   obj_attributes
48
49 (* Utility functions that transform a Pxp attribute into something useful *)
50
51 let uri_list_of_attr a =
52  let module T = Pxp_types in
53   match a with
54      T.Value s ->
55       List.map UriManager.uri_of_string (Str.split (Str.regexp " ") s)
56    | _ -> raise (IllFormedXml 0)
57 ;;
58
59 let string_of_attr a =
60  let module T = Pxp_types in
61   match a with
62      T.Value s -> s
63    | _ -> raise (IllFormedXml 0)
64 ;;
65
66 let int_of_attr a =
67  int_of_string (string_of_attr a)
68 ;;
69
70 let bool_of_attr a =
71  bool_of_string (string_of_attr a)
72 ;;
73
74 let name_of_attr a =
75  let module T = Pxp_types in
76  let module C = Cic in
77   match a with
78      T.Value s -> C.Name s
79    | T.Implied_value -> C.Anonymous
80    | _ -> raise (IllFormedXml 0)
81 ;;
82
83 (* Other utility functions *)
84
85 let get_content n =
86  match n#sub_nodes with
87     [ t ] -> t
88   | _     -> raise (IllFormedXml 1)
89 ;;
90
91 (* Functions that, given the list of sons of a node of the cic dom (objects   *)
92 (* level), retrieve the internal representation associated to the node.       *)
93 (* Everytime a cic term subtree is found, it is translated to the internal    *)
94 (* representation using the method to_cic_term defined in cicParser3.         *)
95 (* Each function raise IllFormedXml if something goes wrong, but this should  *)
96 (* be impossible due to the presence of the dtd                               *)
97 (* The functions should really be obvious looking at their name and the cic   *)
98 (* dtd                                                                        *)
99
100 (* called when a CurrentProof is found *)
101 let get_conjs_value l =
102  let rec rget (c, v) l =
103   let module D = Pxp_document in
104    match l with
105       [] -> (c, v)
106     | conj::tl when conj#node_type = D.T_element "Conjecture" ->
107        let no = int_of_attr (conj#attribute "no") in
108        let id = string_of_attr (conj#attribute "id") in
109        let typ,canonical_context =
110         match List.rev (conj#sub_nodes) with
111            [] -> raise (IllFormedXml 13)
112          | typ::canonical_context ->
113             (get_content typ)#extension#to_cic_term [],
114             List.map
115              (function n ->
116                let id = string_of_attr (n#attribute "id") in
117                 match n#node_type with
118                    D.T_element "Decl" ->
119                     let name = name_of_attr (n#attribute "name") in
120                     let term = (get_content n)#extension#to_cic_term [] in
121                      id, Some (name,Cic.ADecl term)
122                  | D.T_element "Def" ->
123                     let name = name_of_attr (n#attribute "name") in
124                     let term = (get_content n)#extension#to_cic_term [] in
125                      id, Some (name,Cic.ADef term)
126                  | D.T_element "Hidden" -> id, None
127                  | _ -> raise (IllFormedXml 14)
128              ) canonical_context
129        in
130         rget ((id, no, canonical_context, typ)::c, v) tl
131     | value::tl when value#node_type = D.T_element "body" ->
132        let v' = (get_content value)#extension#to_cic_term [] in
133         (match v with
134             None -> rget (c, Some v') tl
135           | _    -> raise (IllFormedXml 2)
136         )
137     | _ -> raise (IllFormedXml 4)
138  in
139   match rget ([], None) l with
140      (revc, Some v) -> (List.rev revc, v)
141    | _ -> raise (IllFormedXml 5)
142 ;;
143
144 (* used only by get_inductive_types; called one time for each inductive  *)
145 (* definitions in a block of inductive definitions                       *)
146 let get_names_arity_constructors l =
147  let rec rget (a,c) l =
148   let module D = Pxp_document in
149    match l with
150       [] -> (a, c)
151     | arity::tl when arity#node_type = D.T_element "arity" ->
152        let a' = (get_content arity)#extension#to_cic_term [] in
153         rget (Some a',c) tl
154     | con::tl when con#node_type = D.T_element "Constructor" ->
155        let id = string_of_attr (con#attribute "name")
156        and ty = (get_content con)#extension#to_cic_term [] in
157          rget (a,(id,ty)::c) tl
158     | _ -> raise (IllFormedXml 9)
159  in
160   match rget (None,[]) l with
161      (Some a, c) -> (a, List.rev c)
162    | _ -> raise (IllFormedXml 8)
163 ;;
164
165 (* called when an InductiveDefinition is found *)
166 let rec get_inductive_types =
167  function
168     []     -> []
169   | he::tl ->
170      let tyname    = string_of_attr (he#attribute "name")
171      and inductive = bool_of_attr   (he#attribute "inductive")
172      and xid = string_of_attr (he#attribute "id")
173      and (arity,cons) =
174       get_names_arity_constructors (he#sub_nodes)
175      in
176       (xid,tyname,inductive,arity,cons)::(get_inductive_types tl)
177 ;;
178
179 (* This is the main function and also the only one used directly from *)
180 (* cicParser. Given the root of the dom tree, it returns the internal *)
181 (* representation of the cic object described in the tree             *)
182 (* It uses the previous functions and the to_cic_term method defined  *)
183 (* in cicParser3 (used for subtrees that encode cic terms)            *)
184 let rec get_term (n : CicParser3.cic_term Pxp_document.node) nbody
185 =
186  let module U = UriManager in
187  let module D = Pxp_document in
188  let module C = Cic in
189   let obj_attrs = get_obj_attributes n in
190   let ntype = n#node_type in
191   match ntype with
192     D.T_element "ConstantType" ->
193       let name = string_of_attr (n # attribute "name") in
194       let params = uri_list_of_attr (n#attribute "params") in
195       let xid = string_of_attr (n#attribute "id") in
196       let typ = (get_content n)#extension#to_cic_term [] in
197        (match nbody with
198            None ->
199             (* Axiom *)
200             C.AConstant (xid, None, name, None, typ, params, obj_attrs)
201          | Some nbody' ->
202             let nbodytype = nbody'#node_type in
203             match nbodytype with
204              D.T_element "ConstantBody" ->
205 (*CSC: the attribute "for" is ignored and not checked
206               let for_ = string_of_attr (nbody'#attribute "for") in
207 *)
208               let paramsbody = uri_list_of_attr (nbody'#attribute "params") in
209               let xidbody = string_of_attr (nbody'#attribute "id") in
210               let value = (get_content nbody')#extension#to_cic_term [] in
211                if paramsbody = params then
212                 C.AConstant (xid, Some xidbody, name, Some value, typ, params,
213                   obj_attrs)
214                else
215                 raise (IllFormedXml 6)
216            | D.T_element "CurrentProof" ->
217 (*CSC: the attribute "of" is ignored and not checked
218               let for_ = string_of_attr (nbody'#attribute "of") in
219 *)
220               let xidbody = string_of_attr (nbody'#attribute "id") in
221               let sons = nbody'#sub_nodes in
222                let (conjs, value) = get_conjs_value sons in
223                 C.ACurrentProof (xid, xidbody, name, conjs, value, typ, params,
224                   obj_attrs)
225            | D.T_element _
226            | D.T_data
227            | _ -> raise (IllFormedXml 6)
228        )
229   | D.T_element "InductiveDefinition" ->
230      let sons = n#sub_nodes
231      and xid = string_of_attr (n#attribute "id") in
232       let inductiveTypes = get_inductive_types sons
233       and params = uri_list_of_attr (n#attribute "params")
234       and nparams = int_of_attr (n#attribute "noParams") in
235        C.AInductiveDefinition (xid, inductiveTypes, params, nparams, obj_attrs)
236   | D.T_element "Variable" ->
237      let name = string_of_attr (n#attribute "name")
238      and params = uri_list_of_attr (n#attribute "params")
239      and xid = string_of_attr (n#attribute "id")
240      and (body, typ) = 
241       let sons = n#sub_nodes in
242        match sons with
243           [b ; t] when
244             b#node_type = D.T_element "body" &&
245             t#node_type = D.T_element "type" ->
246              let b' = get_content b
247              and t' = get_content t in
248               (Some (b'#extension#to_cic_term []), t'#extension#to_cic_term [])
249         | [t] when t#node_type = D.T_element "type" ->
250              let t' = get_content t in
251               (None, t'#extension#to_cic_term [])
252         | _ -> raise (IllFormedXml 6)
253      in
254       C.AVariable (xid,name,body,typ,params,obj_attrs)
255   | D.T_element _
256   | D.T_data
257   | _ -> raise (IllFormedXml 7)
258 ;;