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> *)
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 *)
40 (******************************************************************************)
42 exception IllFormedXml of int;;
44 (* The hashtable from the current identifiers to the object or the terms *)
45 let ids_to_targets = ref None;;
47 (* The list of tokens of the current section path. *)
48 (* Used to resolve relative URIs *)
49 let current_sp = ref [];;
51 (* The uri of the object been parsed *)
52 let current_uri = ref (UriManager.uri_of_string "cic:/.xml");;
54 (* True if annotation really matter *)
55 let process_annotations = ref false;;
57 (* Utility functions to map a markup attribute to something useful *)
59 let cic_attr_of_xml_attr =
61 Pxp_types.Value s -> Cic.Name s
62 | Pxp_types.Implied_value -> Cic.Anonimous
63 | _ -> raise (IllFormedXml 1)
65 let cic_sort_of_xml_attr =
67 Pxp_types.Value "Prop" -> Cic.Prop
68 | Pxp_types.Value "Set" -> Cic.Set
69 | Pxp_types.Value "Type" -> Cic.Type
70 | _ -> raise (IllFormedXml 2)
74 Pxp_types.Value n -> int_of_string n
75 | _ -> raise (IllFormedXml 3)
79 Pxp_types.Value s -> UriManager.uri_of_string s
80 | _ -> raise (IllFormedXml 4)
82 let string_of_xml_attr =
84 Pxp_types.Value s -> s
85 | _ -> raise (IllFormedXml 5)
87 let binder_of_xml_attr =
89 Pxp_types.Value s -> if !process_annotations then Some s else None
90 | _ -> raise (IllFormedXml 17)
93 let register_id id node =
94 if !process_annotations then
95 match !ids_to_targets with
97 | Some ids_to_targets ->
98 Hashtbl.add ids_to_targets id (Cic.Term node)
101 (* the "interface" of the class linked to each node of the dom tree *)
103 class virtual cic_term =
106 (* fields and methods ever required by markup *)
107 val mutable node = (None : cic_term Pxp_document.node option)
118 (* a method that returns the internal representation of the tree (term) *)
119 (* rooted in this node *)
120 method virtual to_cic_term : Cic.annterm
124 (* the class of the objects linked to nodes that are not roots of cic terms *)
125 class eltype_not_of_cic =
130 method to_cic_term = raise (IllFormedXml 6)
134 (* the class of the objects linked to nodes whose content is a cic term *)
135 (* (syntactic sugar xml entities) e.g. <type> ... </type> *)
136 class eltype_transparent =
143 match n#sub_nodes with
144 [ t ] -> t#extension#to_cic_term
145 | _ -> raise (IllFormedXml 7)
149 (* A class for each cic node type *)
158 let nofun = int_of_xml_attr (n#attribute "noFun")
159 and id = string_of_xml_attr (n#attribute "id")
161 let sons = n#sub_nodes in
164 f when f#node_type = Pxp_document.T_element "FixFunction" ->
165 let name = string_of_xml_attr (f#attribute "name")
166 and recindex = int_of_xml_attr (f#attribute "recIndex")
168 match f#sub_nodes with
170 t#node_type = Pxp_document.T_element "type" &&
171 b#node_type = Pxp_document.T_element "body" ->
172 (t#extension#to_cic_term, b#extension#to_cic_term)
173 | _ -> raise (IllFormedXml 14)
175 (name, recindex, ty, body)
176 | _ -> raise (IllFormedXml 13)
179 let res = Cic.AFix (id, ref None, nofun, functions) in
192 let nofun = int_of_xml_attr (n#attribute "noFun")
193 and id = string_of_xml_attr (n#attribute "id")
195 let sons = n#sub_nodes in
198 f when f#node_type = Pxp_document.T_element "CofixFunction" ->
199 let name = string_of_xml_attr (f#attribute "name")
201 match f#sub_nodes with
203 t#node_type = Pxp_document.T_element "type" &&
204 b#node_type = Pxp_document.T_element "body" ->
205 (t#extension#to_cic_term, b#extension#to_cic_term)
206 | _ -> raise (IllFormedXml 16)
209 | _ -> raise (IllFormedXml 15)
212 let res = Cic.ACoFix (id, ref None, nofun, functions) in
218 class eltype_implicit =
225 let id = string_of_xml_attr (n#attribute "id") in
226 let res = Cic.AImplicit (id, ref None) in
239 let value = int_of_xml_attr (n#attribute "value")
240 and binder = binder_of_xml_attr (n#attribute "binder")
241 and id = string_of_xml_attr (n#attribute "id") in
242 let res = Cic.ARel (id,ref None,value,binder) in
255 let value = int_of_xml_attr (n#attribute "no")
256 and id = string_of_xml_attr (n#attribute "id") in
257 let res = Cic.AMeta (id,ref None,value) in
270 let name = string_of_xml_attr (n#attribute "relUri")
271 and xid = string_of_xml_attr (n#attribute "id") in
272 match Str.split (Str.regexp ",") name with
278 | (n,he::tl) when n > 0 -> "/" ^ he ^ aux (n - 1, tl)
279 | _ -> raise (IllFormedXml 19)
281 aux (List.length !current_sp - n,!current_sp)
286 (UriManager.uri_of_string
287 ("cic:" ^ get_prefix (int_of_string index) ^ id ^ ".var"))
292 | _ -> raise (IllFormedXml 18)
303 let children = n#sub_nodes
304 and id = string_of_xml_attr (n#attribute "id") in
305 if List.length children < 2 then raise (IllFormedXml 8)
309 (id,ref None,List.map (fun x -> x#extension#to_cic_term) children)
323 let sons = n#sub_nodes
324 and id = string_of_xml_attr (n#attribute "id") in
327 te#node_type = Pxp_document.T_element "term" &&
328 ty#node_type = Pxp_document.T_element "type" ->
329 let term = te#extension#to_cic_term
330 and typ = ty#extension#to_cic_term in
331 let res = Cic.ACast (id,ref None,term,typ) in
334 | _ -> raise (IllFormedXml 9)
345 let sort = cic_sort_of_xml_attr (n#attribute "value")
346 and id = string_of_xml_attr (n#attribute "id") in
347 let res = Cic.ASort (id,ref None,sort) in
360 let value = uri_of_xml_attr (n#attribute "uri")
361 and id = string_of_xml_attr (n#attribute "id") in
362 let res = Cic.AAbst (id,ref None,value) in
374 let module U = UriManager in
376 let value = uri_of_xml_attr (n#attribute "uri")
377 and id = string_of_xml_attr (n#attribute "id") in
379 Cic.AConst (id,ref None,value, U.relative_depth !current_uri value 0)
386 class eltype_mutind =
392 let module U = UriManager in
394 let name = uri_of_xml_attr (n#attribute "uri")
395 and noType = int_of_xml_attr (n#attribute "noType")
396 and id = string_of_xml_attr (n#attribute "id") in
399 (id,ref None,name, U.relative_depth !current_uri name 0, noType)
406 class eltype_mutconstruct =
412 let module U = UriManager in
414 let name = uri_of_xml_attr (n#attribute "uri")
415 and noType = int_of_xml_attr (n#attribute "noType")
416 and noConstr = int_of_xml_attr (n#attribute "noConstr")
417 and id = string_of_xml_attr (n#attribute "id") in
420 (id, ref None, name, U.relative_depth !current_uri name 0,
435 let sons = n#sub_nodes
436 and id = string_of_xml_attr (n#attribute "id") in
439 s#node_type = Pxp_document.T_element "source" &&
440 t#node_type = Pxp_document.T_element "target" ->
441 let name = cic_attr_of_xml_attr (t#attribute "binder")
442 and source = s#extension#to_cic_term
443 and target = t#extension#to_cic_term in
444 let res = Cic.AProd (id,ref None,name,source,target) in
447 | _ -> raise (IllFormedXml 10)
451 class eltype_mutcase =
457 let module U = UriManager in
459 let sons = n#sub_nodes
460 and id = string_of_xml_attr (n#attribute "id") in
462 ty::te::patterns when
463 ty#node_type = Pxp_document.T_element "patternsType" &&
464 te#node_type = Pxp_document.T_element "inductiveTerm" ->
465 let ci = uri_of_xml_attr (n#attribute "uriType")
466 and typeno = int_of_xml_attr (n#attribute "noType")
467 and inductiveType = ty#extension#to_cic_term
468 and inductiveTerm = te#extension#to_cic_term
469 and lpattern= List.map (fun x -> x#extension#to_cic_term) patterns
472 Cic.AMutCase (id,ref None,ci,U.relative_depth !current_uri ci 0,
473 typeno,inductiveType,inductiveTerm,lpattern)
477 | _ -> raise (IllFormedXml 11)
481 class eltype_lambda =
488 let sons = n#sub_nodes
489 and id = string_of_xml_attr (n#attribute "id") in
492 s#node_type = Pxp_document.T_element "source" &&
493 t#node_type = Pxp_document.T_element "target" ->
494 let name = cic_attr_of_xml_attr (t#attribute "binder")
495 and source = s#extension#to_cic_term
496 and target = t#extension#to_cic_term in
497 let res = Cic.ALambda (id,ref None,name,source,target) in
500 | _ -> raise (IllFormedXml 12)
511 let sons = n#sub_nodes
512 and id = string_of_xml_attr (n#attribute "id") in
515 s#node_type = Pxp_document.T_element "term" &&
516 t#node_type = Pxp_document.T_element "letintarget" ->
517 let name = cic_attr_of_xml_attr (t#attribute "binder")
518 and source = s#extension#to_cic_term
519 and target = t#extension#to_cic_term in
520 let res = Cic.ALetIn (id,ref None,name,source,target) in
523 | _ -> raise (IllFormedXml 12)
527 (* The definition of domspec, an hashtable that maps each node type to the *)
528 (* object that must be linked to it. Used by markup. *)
531 let module D = Pxp_document in
532 D.make_spec_from_alist
533 ~data_exemplar: (new D.data_impl (new eltype_not_of_cic))
534 ~default_element_exemplar: (new D.element_impl (new eltype_not_of_cic))
536 [ "REL", (new D.element_impl (new eltype_rel)) ;
537 "VAR", (new D.element_impl (new eltype_var)) ;
538 "META", (new D.element_impl (new eltype_meta)) ;
539 "SORT", (new D.element_impl (new eltype_sort)) ;
540 "IMPLICIT", (new D.element_impl (new eltype_implicit)) ;
541 "CAST", (new D.element_impl (new eltype_cast)) ;
542 "PROD", (new D.element_impl (new eltype_prod)) ;
543 "LAMBDA", (new D.element_impl (new eltype_lambda)) ;
544 "LETIN", (new D.element_impl (new eltype_letin)) ;
545 "APPLY", (new D.element_impl (new eltype_apply)) ;
546 "CONST", (new D.element_impl (new eltype_const)) ;
547 "ABST", (new D.element_impl (new eltype_abst)) ;
548 "MUTIND", (new D.element_impl (new eltype_mutind)) ;
549 "MUTCONSTRUCT", (new D.element_impl (new eltype_mutconstruct)) ;
550 "MUTCASE", (new D.element_impl (new eltype_mutcase)) ;
551 "FIX", (new D.element_impl (new eltype_fix)) ;
552 "COFIX", (new D.element_impl (new eltype_cofix)) ;
553 "arity", (new D.element_impl (new eltype_transparent)) ;
554 "term", (new D.element_impl (new eltype_transparent)) ;
555 "type", (new D.element_impl (new eltype_transparent)) ;
556 "body", (new D.element_impl (new eltype_transparent)) ;
557 "source", (new D.element_impl (new eltype_transparent)) ;
558 "target", (new D.element_impl (new eltype_transparent)) ;
559 "patternsType", (new D.element_impl (new eltype_transparent)) ;
560 "inductiveTerm", (new D.element_impl (new eltype_transparent)) ;
561 "pattern", (new D.element_impl (new eltype_transparent))