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 list of tokens of the current section path. *)
45 (* Used to resolve relative URIs *)
46 let current_sp = ref [];;
48 (* The uri of the object been parsed *)
49 let current_uri = ref (UriManager.uri_of_string "cic:/.xml");;
51 (* Utility functions to map a markup attribute to something useful *)
53 let cic_attr_of_xml_attr =
55 Pxp_types.Value s -> Cic.Name s
56 | Pxp_types.Implied_value -> Cic.Anonymous
57 | _ -> raise (IllFormedXml 1)
59 let cic_sort_of_xml_attr =
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)
68 Pxp_types.Value n -> int_of_string n
69 | _ -> raise (IllFormedXml 3)
73 Pxp_types.Value s -> UriManager.uri_of_string s
74 | _ -> raise (IllFormedXml 4)
76 let string_of_xml_attr =
78 Pxp_types.Value s -> s
79 | _ -> raise (IllFormedXml 5)
81 let binder_of_xml_attr =
83 Pxp_types.Value s -> s
84 | _ -> raise (IllFormedXml 17)
87 (* the "interface" of the class linked to each node of the dom tree *)
89 class virtual cic_term =
92 (* fields and methods always required by markup *)
93 val mutable node = (None : cic_term Pxp_document.node option)
104 (* a method that returns the internal representation of the tree (term) *)
105 (* rooted in this node *)
106 method virtual to_cic_term :
107 (UriManager.uri * Cic.annterm) list -> Cic.annterm
111 (* the class of the objects linked to nodes that are not roots of cic terms *)
112 class eltype_not_of_cic =
117 method to_cic_term _ = raise (IllFormedXml 6)
121 (* the class of the objects linked to nodes whose content is a cic term *)
122 (* (syntactic sugar xml entities) e.g. <type> ... </type> *)
123 class eltype_transparent =
128 method to_cic_term exp_named_subst =
129 assert (exp_named_subst = []) ;
131 match n#sub_nodes with
132 [ t ] -> t#extension#to_cic_term []
133 | _ -> raise (IllFormedXml 7)
137 (* A class for each cic node type *)
144 method to_cic_term exp_named_subst =
145 assert (exp_named_subst = []) ;
147 let nofun = int_of_xml_attr (n#attribute "noFun")
148 and id = string_of_xml_attr (n#attribute "id")
150 let sons = n#sub_nodes in
153 f when f#node_type = Pxp_document.T_element "FixFunction" ->
154 let name = string_of_xml_attr (f#attribute "name")
155 and id = string_of_xml_attr (f#attribute "id")
156 and recindex = int_of_xml_attr (f#attribute "recIndex")
158 match f#sub_nodes with
160 t#node_type = Pxp_document.T_element "type" &&
161 b#node_type = Pxp_document.T_element "body" ->
162 (t#extension#to_cic_term [], b#extension#to_cic_term [])
163 | _ -> raise (IllFormedXml 14)
165 (id, name, recindex, ty, body)
166 | _ -> raise (IllFormedXml 13)
169 Cic.AFix (id, nofun, functions)
178 method to_cic_term exp_named_subst =
179 assert (exp_named_subst = []) ;
181 let nofun = int_of_xml_attr (n#attribute "noFun")
182 and id = string_of_xml_attr (n#attribute "id")
184 let sons = n#sub_nodes in
187 f when f#node_type = Pxp_document.T_element "CofixFunction" ->
188 let name = string_of_xml_attr (f#attribute "name")
189 and id = string_of_xml_attr (f#attribute "id")
191 match f#sub_nodes with
193 t#node_type = Pxp_document.T_element "type" &&
194 b#node_type = Pxp_document.T_element "body" ->
195 (t#extension#to_cic_term [], b#extension#to_cic_term [])
196 | _ -> raise (IllFormedXml 16)
199 | _ -> raise (IllFormedXml 15)
202 Cic.ACoFix (id, nofun, functions)
206 class eltype_implicit =
211 method to_cic_term exp_named_subst =
212 assert (exp_named_subst = []) ;
214 let id = string_of_xml_attr (n#attribute "id") in
224 method to_cic_term exp_named_subst =
225 assert (exp_named_subst = []) ;
227 let value = int_of_xml_attr (n#attribute "value")
228 and binder = binder_of_xml_attr (n#attribute "binder")
229 and id = string_of_xml_attr (n#attribute "id")
230 and idref = string_of_xml_attr (n#attribute "idref") in
231 Cic.ARel (id,idref,value,binder)
240 method to_cic_term exp_named_subst =
241 assert (exp_named_subst = []) ;
243 let value = int_of_xml_attr (n#attribute "no")
244 and id = string_of_xml_attr (n#attribute "id")
247 let sons = n#sub_nodes in
249 (function substitution ->
250 match substitution#sub_nodes with
252 | [he] -> Some (he#extension#to_cic_term [])
253 | _ -> raise (IllFormedXml 20)
256 Cic.AMeta (id,value,local_context)
265 method to_cic_term exp_named_subst =
266 assert (exp_named_subst = []) ;
268 let uri = uri_of_xml_attr (n#attribute "uri")
269 and xid = string_of_xml_attr (n#attribute "id") in
270 (*CSC: BIG BUG: [] MUST BE REPLACED WITH THE PARSED EXPLICIT NAMED SUBSTITUTION *)
271 Cic.AVar (xid,uri,[])
280 method to_cic_term exp_named_subst =
281 assert (exp_named_subst = []) ;
283 let children = n#sub_nodes
284 and id = string_of_xml_attr (n#attribute "id") in
285 if List.length children < 2 then raise (IllFormedXml 8)
288 (id,List.map (fun x -> x#extension#to_cic_term []) children)
297 method to_cic_term exp_named_subst =
298 assert (exp_named_subst = []) ;
300 let sons = n#sub_nodes
301 and id = string_of_xml_attr (n#attribute "id") in
304 te#node_type = Pxp_document.T_element "term" &&
305 ty#node_type = Pxp_document.T_element "type" ->
306 let term = te#extension#to_cic_term []
307 and typ = ty#extension#to_cic_term [] in
308 Cic.ACast (id,term,typ)
309 | _ -> raise (IllFormedXml 9)
318 method to_cic_term exp_named_subst =
319 assert (exp_named_subst = []) ;
321 let sort = cic_sort_of_xml_attr (n#attribute "value")
322 and id = string_of_xml_attr (n#attribute "id") in
332 method to_cic_term exp_named_subst =
333 let module U = UriManager in
335 let value = uri_of_xml_attr (n#attribute "uri")
336 and id = string_of_xml_attr (n#attribute "id") in
337 Cic.AConst (id,value, exp_named_subst)
341 class eltype_mutind =
346 method to_cic_term exp_named_subst =
347 let module U = UriManager in
349 let name = uri_of_xml_attr (n#attribute "uri")
350 and noType = int_of_xml_attr (n#attribute "noType")
351 and id = string_of_xml_attr (n#attribute "id") in
353 (id,name, noType, exp_named_subst)
357 class eltype_mutconstruct =
362 method to_cic_term exp_named_subst =
363 let module U = UriManager in
365 let name = uri_of_xml_attr (n#attribute "uri")
366 and noType = int_of_xml_attr (n#attribute "noType")
367 and noConstr = int_of_xml_attr (n#attribute "noConstr")
368 and id = string_of_xml_attr (n#attribute "id") in
370 (id, name, noType, noConstr, exp_named_subst)
379 method to_cic_term exp_named_subst =
380 assert (exp_named_subst = []) ;
382 let sons = n#sub_nodes in
383 let rec get_decls_and_target =
385 [t] when t#node_type = Pxp_document.T_element "target" ->
386 [],t#extension#to_cic_term []
387 | s::tl when s#node_type = Pxp_document.T_element "decl" ->
388 let decls,target = get_decls_and_target tl in
389 let id = string_of_xml_attr (s#attribute "id") in
390 let binder = cic_attr_of_xml_attr (s#attribute "binder") in
391 (id,binder,s#extension#to_cic_term [])::decls, target
392 | _ -> raise (IllFormedXml 10)
394 let decls,target = get_decls_and_target sons in
396 (fun (id,b,s) t -> Cic.AProd (id,b,s,t))
401 class eltype_mutcase =
406 method to_cic_term exp_named_subst =
407 assert (exp_named_subst = []) ;
408 let module U = UriManager in
410 let sons = n#sub_nodes
411 and id = string_of_xml_attr (n#attribute "id") in
413 ty::te::patterns when
414 ty#node_type = Pxp_document.T_element "patternsType" &&
415 te#node_type = Pxp_document.T_element "inductiveTerm" ->
416 let ci = uri_of_xml_attr (n#attribute "uriType")
417 and typeno = int_of_xml_attr (n#attribute "noType")
418 and inductiveType = ty#extension#to_cic_term []
419 and inductiveTerm = te#extension#to_cic_term []
421 List.map (fun x -> x#extension#to_cic_term []) patterns
423 Cic.AMutCase (id,ci, typeno,inductiveType,inductiveTerm,lpattern)
424 | _ -> raise (IllFormedXml 11)
428 class eltype_lambda =
433 method to_cic_term exp_named_subst =
434 assert (exp_named_subst = []) ;
436 let sons = n#sub_nodes in
437 let rec get_decls_and_target =
439 [t] when t#node_type = Pxp_document.T_element "target" ->
440 [],t#extension#to_cic_term []
441 | s::tl when s#node_type = Pxp_document.T_element "decl" ->
442 let decls,target = get_decls_and_target tl in
443 let id = string_of_xml_attr (s#attribute "id") in
444 let binder = cic_attr_of_xml_attr (s#attribute "binder") in
445 (id,binder,s#extension#to_cic_term [])::decls, target
446 | _ -> raise (IllFormedXml 12)
448 let decls,target = get_decls_and_target sons in
450 (fun (id,b,s) t -> Cic.ALambda (id,b,s,t))
460 method to_cic_term exp_named_subst =
461 assert (exp_named_subst = []) ;
463 let sons = n#sub_nodes in
464 let rec get_defs_and_target =
466 [t] when t#node_type = Pxp_document.T_element "target" ->
467 [],t#extension#to_cic_term []
468 | s::tl when s#node_type = Pxp_document.T_element "def" ->
469 let defs,target = get_defs_and_target tl in
470 let id = string_of_xml_attr (s#attribute "id") in
471 let binder = cic_attr_of_xml_attr (s#attribute "binder") in
472 (id,binder,s#extension#to_cic_term [])::defs, target
473 | _ -> raise (IllFormedXml 12)
475 let defs,target = get_defs_and_target sons in
477 (fun (id,b,s) t -> Cic.ALetIn (id,b,s,t))
482 class eltype_instantiate =
487 method to_cic_term exp_named_subst =
488 assert (exp_named_subst = []) ;
490 (* CSC: this optional attribute should be parsed and reflected in Cic.annterm
491 and id = string_of_xml_attr (n#attribute "id")
493 match n#sub_nodes with
496 UriManager.buri_of_uri (uri_of_xml_attr (t#attribute "uri")) in
497 let exp_named_subst =
500 n when n#node_type = Pxp_document.T_element "arg" ->
501 let relUri = string_of_xml_attr (n#attribute "relUri") in
502 let uri = UriManager.uri_of_string (baseUri ^ "/" ^ relUri) in
504 match n#sub_nodes with
505 [ t ] -> t#extension#to_cic_term []
506 | _ -> raise (IllFormedXml 7)
509 | _ -> raise (IllFormedXml 7)
512 t#extension#to_cic_term exp_named_subst
513 | _ -> raise (IllFormedXml 7)
518 (* The definition of domspec, an hashtable that maps each node type to the *)
519 (* object that must be linked to it. Used by markup. *)
522 let module D = Pxp_document in
523 D.make_spec_from_alist
524 ~data_exemplar: (new D.data_impl (new eltype_not_of_cic))
525 ~default_element_exemplar: (new D.element_impl (new eltype_not_of_cic))
527 [ "REL", (new D.element_impl (new eltype_rel)) ;
528 "VAR", (new D.element_impl (new eltype_var)) ;
529 "META", (new D.element_impl (new eltype_meta)) ;
530 "SORT", (new D.element_impl (new eltype_sort)) ;
531 "IMPLICIT", (new D.element_impl (new eltype_implicit)) ;
532 "CAST", (new D.element_impl (new eltype_cast)) ;
533 "PROD", (new D.element_impl (new eltype_prod)) ;
534 "LAMBDA", (new D.element_impl (new eltype_lambda)) ;
535 "LETIN", (new D.element_impl (new eltype_letin)) ;
536 "APPLY", (new D.element_impl (new eltype_apply)) ;
537 "CONST", (new D.element_impl (new eltype_const)) ;
538 "MUTIND", (new D.element_impl (new eltype_mutind)) ;
539 "MUTCONSTRUCT", (new D.element_impl (new eltype_mutconstruct)) ;
540 "MUTCASE", (new D.element_impl (new eltype_mutcase)) ;
541 "FIX", (new D.element_impl (new eltype_fix)) ;
542 "COFIX", (new D.element_impl (new eltype_cofix)) ;
543 "instantiate", (new D.element_impl (new eltype_instantiate)) ;
544 "arity", (new D.element_impl (new eltype_transparent)) ;
545 "term", (new D.element_impl (new eltype_transparent)) ;
546 "type", (new D.element_impl (new eltype_transparent)) ;
547 "body", (new D.element_impl (new eltype_transparent)) ;
548 "decl", (new D.element_impl (new eltype_transparent)) ;
549 "def", (new D.element_impl (new eltype_transparent)) ;
550 "target", (new D.element_impl (new eltype_transparent)) ;
551 "letintarget", (new D.element_impl (new eltype_transparent)) ;
552 "patternsType", (new D.element_impl (new eltype_transparent)) ;
553 "inductiveTerm", (new D.element_impl (new eltype_transparent)) ;
554 "pattern", (new D.element_impl (new eltype_transparent))