]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic/cicParser3.ml
Debugging code removed to achieve more tail-recursivity.
[helm.git] / helm / ocaml / cic / cicParser3.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 terms level of a parser for cic objects from xml        *)
34 (* files to the internal representation. It is used by the module cicParser2  *)
35 (* (objects level). It defines an extension of the standard dom using the     *)
36 (* object-oriented extension machinery of markup: an object with a method     *)
37 (* to_cic_term that returns the internal representation of the subtree is     *)
38 (* added to each node of the dom tree                                         *)
39 (*                                                                            *)
40 (******************************************************************************)
41
42 exception IllFormedXml of int;;
43
44 (* The list of tokens of the current section path. *)
45 (* Used to resolve relative URIs                   *)
46 let current_sp = ref [];;
47
48 (* The uri of the object been parsed *)
49 let current_uri = ref (UriManager.uri_of_string "cic:/.xml");;
50
51 (* Utility functions to map a markup attribute to something useful *)
52
53 let cic_attr_of_xml_attr =
54  function
55     Pxp_types.Value s       -> Cic.Name s
56   | Pxp_types.Implied_value -> Cic.Anonimous
57   | _             -> raise (IllFormedXml 1)
58
59 let cic_sort_of_xml_attr =
60  function
61     Pxp_types.Value "Prop" -> Cic.Prop
62   | Pxp_types.Value "Set"  -> Cic.Set
63   | Pxp_types.Value "Type" -> Cic.Type
64   | _            -> raise (IllFormedXml 2)
65
66 let int_of_xml_attr =
67  function
68     Pxp_types.Value n -> int_of_string n
69   | _       -> raise (IllFormedXml 3)
70
71 let uri_of_xml_attr =
72  function
73     Pxp_types.Value s -> UriManager.uri_of_string s
74   | _       -> raise (IllFormedXml 4)
75
76 let string_of_xml_attr =
77  function
78     Pxp_types.Value s -> s
79   | _       -> raise (IllFormedXml 5)
80
81 let binder_of_xml_attr =
82  function
83     Pxp_types.Value s -> s
84   | _       -> raise (IllFormedXml 17)
85 ;;
86
87 (* the "interface" of the class linked to each node of the dom tree *)
88
89 class virtual cic_term =
90   object (self)
91
92     (* fields and methods ever required by markup *)
93     val mutable node = (None : cic_term Pxp_document.node option)
94
95     method clone = {< >} 
96     method node =
97       match node with
98           None ->
99             assert false
100         | Some n -> n
101     method set_node n =
102       node <- Some n
103
104     (* a method that returns the internal representation of the tree (term) *)
105     (* rooted in this node                                                  *)
106     method virtual to_cic_term : Cic.annterm
107   end
108 ;;
109
110 (* the class of the objects linked to nodes that are not roots of cic terms *)
111 class eltype_not_of_cic =
112   object (self)
113
114      inherit cic_term
115
116      method to_cic_term = raise (IllFormedXml 6)
117   end
118 ;;
119
120 (* the class of the objects linked to nodes whose content is a cic term *)
121 (* (syntactic sugar xml entities) e.g. <type> ... </type>               *)
122 class eltype_transparent =
123   object (self)
124
125     inherit cic_term
126
127     method to_cic_term =
128      let n = self#node in
129       match n#sub_nodes with
130          [ t ]  -> t#extension#to_cic_term
131        | _  -> raise (IllFormedXml 7)
132   end
133 ;;
134
135 (* A class for each cic node type *)
136
137 class eltype_fix =
138   object (self)
139
140     inherit cic_term
141
142     method to_cic_term =
143      let n = self#node in
144       let nofun = int_of_xml_attr (n#attribute "noFun")
145       and id = string_of_xml_attr (n#attribute "id")
146       and functions =
147        let sons = n#sub_nodes in
148         List.map
149          (function
150              f when f#node_type = Pxp_document.T_element "FixFunction" ->
151               let name = string_of_xml_attr (f#attribute "name")
152               and recindex = int_of_xml_attr (f#attribute "recIndex")
153               and (ty, body) =
154                match f#sub_nodes with
155                   [t ; b] when
156                     t#node_type = Pxp_document.T_element "type" &&
157                     b#node_type = Pxp_document.T_element "body" ->
158                      (t#extension#to_cic_term, b#extension#to_cic_term)
159                 | _ -> raise (IllFormedXml 14)
160               in
161                (name, recindex, ty, body)
162            | _ -> raise (IllFormedXml 13)
163          ) sons
164       in
165        Cic.AFix (id, nofun, functions)
166   end
167 ;;
168
169 class eltype_cofix =
170   object (self)
171
172     inherit cic_term
173
174     method to_cic_term =
175      let n = self#node in
176       let nofun = int_of_xml_attr (n#attribute "noFun")
177       and id = string_of_xml_attr (n#attribute "id")
178       and functions =
179        let sons = n#sub_nodes in
180         List.map
181          (function
182              f when f#node_type = Pxp_document.T_element "CofixFunction" ->
183               let name = string_of_xml_attr (f#attribute "name")
184               and (ty, body) =
185                match f#sub_nodes with
186                   [t ; b] when
187                     t#node_type = Pxp_document.T_element "type" &&
188                     b#node_type = Pxp_document.T_element "body" ->
189                      (t#extension#to_cic_term, b#extension#to_cic_term)
190                 | _ -> raise (IllFormedXml 16)
191               in
192                (name, ty, body)
193            | _ -> raise (IllFormedXml 15)
194          ) sons
195       in
196        Cic.ACoFix (id, nofun, functions)
197   end
198 ;;
199
200 class eltype_implicit =
201   object (self)
202
203     inherit cic_term
204
205     method to_cic_term =
206      let n = self#node in
207       let id = string_of_xml_attr (n#attribute "id") in
208        Cic.AImplicit id
209   end
210 ;;
211
212 class eltype_rel =
213   object (self)
214
215     inherit cic_term
216
217     method to_cic_term =
218      let n = self#node in
219       let value  = int_of_xml_attr (n#attribute "value")
220       and binder = binder_of_xml_attr (n#attribute "binder")
221       and id = string_of_xml_attr (n#attribute "id") in
222        Cic.ARel (id,value,binder)
223   end
224 ;;
225
226 class eltype_meta =
227   object (self)
228
229     inherit cic_term
230
231     method to_cic_term =
232      let n = self#node in
233       let value = int_of_xml_attr (n#attribute "no")
234       and id = string_of_xml_attr (n#attribute "id") in
235        Cic.AMeta (id,value)
236   end
237 ;;
238
239 class eltype_var =
240   object (self)
241
242     inherit cic_term
243
244     method to_cic_term =
245      let n = self#node in
246       let name = string_of_xml_attr (n#attribute "relUri")
247       and xid = string_of_xml_attr (n#attribute "id") in
248        match Str.split (Str.regexp ",") name with
249           [index; id] ->
250            let get_prefix n =
251             let rec aux =
252              function
253                 (0,_) -> "/"
254               | (n,he::tl) when n > 0 -> "/" ^ he ^ aux (n - 1, tl)
255               | _ -> raise (IllFormedXml 19)
256             in   
257              aux (List.length !current_sp - n,!current_sp)
258            in
259             Cic.AVar
260              (xid, 
261               (UriManager.uri_of_string
262                ("cic:" ^ get_prefix (int_of_string index) ^ id ^ ".var"))
263              )
264         | _ -> raise (IllFormedXml 18)
265   end
266 ;;
267
268 class eltype_apply =
269   object (self)
270
271     inherit cic_term
272
273     method to_cic_term =
274      let n = self#node in
275       let children = n#sub_nodes
276       and id = string_of_xml_attr (n#attribute "id") in
277        if List.length children < 2 then raise (IllFormedXml 8)
278        else
279         Cic.AAppl
280          (id,List.map (fun x -> x#extension#to_cic_term) children)
281   end
282 ;;
283
284 class eltype_cast =
285   object (self)
286
287     inherit cic_term
288
289     method to_cic_term =
290      let n = self#node in
291       let sons = n#sub_nodes
292       and id = string_of_xml_attr (n#attribute "id") in
293        match sons with
294           [te ; ty] when
295             te#node_type = Pxp_document.T_element "term" &&
296             ty#node_type = Pxp_document.T_element "type" ->
297              let term = te#extension#to_cic_term
298              and typ  = ty#extension#to_cic_term in
299               Cic.ACast (id,term,typ)
300         | _  -> raise (IllFormedXml 9)
301   end
302 ;;
303
304 class eltype_sort =
305   object (self)
306
307     inherit cic_term
308
309     method to_cic_term =
310      let n = self#node in
311       let sort = cic_sort_of_xml_attr (n#attribute "value")
312       and id = string_of_xml_attr (n#attribute "id") in
313        Cic.ASort (id,sort)
314   end
315 ;;
316
317 class eltype_abst =
318   object (self)
319
320     inherit cic_term
321
322     method to_cic_term =
323      let n = self#node in
324       let value = uri_of_xml_attr (n#attribute "uri")
325       and id = string_of_xml_attr (n#attribute "id") in
326        Cic.AAbst (id,value)
327   end
328 ;;
329
330 class eltype_const =
331   object (self)
332
333     inherit cic_term
334
335     method to_cic_term =
336      let module U = UriManager in
337       let n = self#node in
338        let value = uri_of_xml_attr (n#attribute "uri")
339        and id = string_of_xml_attr (n#attribute "id") in
340         Cic.AConst (id,value, U.relative_depth !current_uri value 0)
341   end
342 ;;
343
344 class eltype_mutind =
345   object (self)
346
347     inherit cic_term
348
349     method to_cic_term =
350      let module U = UriManager in
351       let n = self#node in
352        let name = uri_of_xml_attr (n#attribute "uri")
353        and noType = int_of_xml_attr (n#attribute "noType")
354        and id = string_of_xml_attr (n#attribute "id") in
355         Cic.AMutInd
356          (id,name, U.relative_depth !current_uri name 0, noType)
357   end
358 ;;
359
360 class eltype_mutconstruct =
361   object (self)
362
363     inherit cic_term
364
365     method to_cic_term =
366      let module U = UriManager in
367       let n = self#node in
368        let name = uri_of_xml_attr (n#attribute "uri")
369        and noType = int_of_xml_attr (n#attribute "noType")
370        and noConstr = int_of_xml_attr (n#attribute "noConstr")
371        and id = string_of_xml_attr (n#attribute "id") in
372         Cic.AMutConstruct
373          (id, name, U.relative_depth !current_uri name 0,
374          noType, noConstr)
375   end
376 ;;
377
378 class eltype_prod =
379   object (self)
380
381     inherit cic_term
382
383     method to_cic_term =
384      let n = self#node in
385       let sons = n#sub_nodes
386       and id = string_of_xml_attr (n#attribute "id") in
387        match sons with
388           [s ; t] when
389             s#node_type = Pxp_document.T_element "source" &&
390             t#node_type = Pxp_document.T_element "target" ->
391              let name = cic_attr_of_xml_attr (t#attribute "binder")
392              and source = s#extension#to_cic_term
393              and target = t#extension#to_cic_term in
394               Cic.AProd (id,name,source,target)
395         | _  -> raise (IllFormedXml 10)
396   end
397 ;;
398
399 class eltype_mutcase =
400   object (self)
401
402     inherit cic_term
403
404     method to_cic_term =
405      let module U = UriManager in
406       let n = self#node in
407        let sons = n#sub_nodes
408        and id = string_of_xml_attr (n#attribute "id") in
409         match sons with
410            ty::te::patterns when
411              ty#node_type = Pxp_document.T_element "patternsType" &&
412              te#node_type = Pxp_document.T_element "inductiveTerm" ->
413               let ci = uri_of_xml_attr (n#attribute "uriType")
414               and typeno = int_of_xml_attr (n#attribute "noType")
415               and inductiveType = ty#extension#to_cic_term
416               and inductiveTerm = te#extension#to_cic_term
417               and lpattern= List.map (fun x -> x#extension#to_cic_term) patterns
418               in
419                Cic.AMutCase (id,ci,U.relative_depth !current_uri ci 0,
420                 typeno,inductiveType,inductiveTerm,lpattern)
421          | _  -> raise (IllFormedXml 11)
422   end
423 ;;
424
425 class eltype_lambda =
426   object (self)
427
428     inherit cic_term
429
430     method to_cic_term =
431      let n = self#node in
432       let sons = n#sub_nodes
433       and id = string_of_xml_attr (n#attribute "id") in
434        match sons with
435           [s ; t] when
436             s#node_type = Pxp_document.T_element "source" &&
437             t#node_type = Pxp_document.T_element "target" ->
438              let name = cic_attr_of_xml_attr (t#attribute "binder")
439              and source = s#extension#to_cic_term
440              and target = t#extension#to_cic_term in
441               Cic.ALambda (id,name,source,target)
442         | _  -> raise (IllFormedXml 12)
443   end
444 ;;
445
446 class eltype_letin =
447   object (self)
448
449     inherit cic_term
450
451     method to_cic_term =
452      let n = self#node in
453       let sons = n#sub_nodes
454       and id = string_of_xml_attr (n#attribute "id") in
455        match sons with
456           [s ; t] when
457             s#node_type = Pxp_document.T_element "term" &&
458             t#node_type = Pxp_document.T_element "letintarget" ->
459              let name = cic_attr_of_xml_attr (t#attribute "binder")
460              and source = s#extension#to_cic_term
461              and target = t#extension#to_cic_term in
462               Cic.ALetIn (id,name,source,target)
463         | _  -> raise (IllFormedXml 12)
464   end
465 ;;
466
467 (* The definition of domspec, an hashtable that maps each node type to the *)
468 (* object that must be linked to it. Used by markup.                       *)
469
470 let domspec =
471  let module D = Pxp_document in
472   D.make_spec_from_alist
473    ~data_exemplar: (new D.data_impl (new eltype_not_of_cic))
474    ~default_element_exemplar: (new D.element_impl (new eltype_not_of_cic))
475    ~element_alist:
476     [ "REL",           (new D.element_impl (new eltype_rel)) ;
477       "VAR",           (new D.element_impl (new eltype_var)) ;
478       "META",          (new D.element_impl (new eltype_meta)) ;
479       "SORT",          (new D.element_impl (new eltype_sort)) ;
480       "IMPLICIT",      (new D.element_impl (new eltype_implicit)) ;
481       "CAST",          (new D.element_impl (new eltype_cast)) ;
482       "PROD",          (new D.element_impl (new eltype_prod)) ;
483       "LAMBDA",        (new D.element_impl (new eltype_lambda)) ;
484       "LETIN",         (new D.element_impl (new eltype_letin)) ;
485       "APPLY",         (new D.element_impl (new eltype_apply)) ;
486       "CONST",         (new D.element_impl (new eltype_const)) ;
487       "ABST",          (new D.element_impl (new eltype_abst)) ;
488       "MUTIND",        (new D.element_impl (new eltype_mutind)) ;
489       "MUTCONSTRUCT",  (new D.element_impl (new eltype_mutconstruct)) ;
490       "MUTCASE",       (new D.element_impl (new eltype_mutcase)) ;
491       "FIX",           (new D.element_impl (new eltype_fix)) ;
492       "COFIX",         (new D.element_impl (new eltype_cofix)) ;
493       "arity",         (new D.element_impl (new eltype_transparent)) ;
494       "term",          (new D.element_impl (new eltype_transparent)) ;
495       "type",          (new D.element_impl (new eltype_transparent)) ;
496       "body",          (new D.element_impl (new eltype_transparent)) ;
497       "source",        (new D.element_impl (new eltype_transparent)) ;
498       "target",        (new D.element_impl (new eltype_transparent)) ;
499       "letintarget",   (new D.element_impl (new eltype_transparent)) ;
500       "patternsType",  (new D.element_impl (new eltype_transparent)) ;
501       "inductiveTerm", (new D.element_impl (new eltype_transparent)) ;
502       "pattern",       (new D.element_impl (new eltype_transparent))
503     ]
504    ()
505 ;;