1 (* Copyright (C) 2004-2005, 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://helm.cs.unibo.it/
26 let debug_print = prerr_endline
30 (* ZACK TODO element from the DTD still to be handled:
31 <!ELEMENT CurrentProof (Conjecture*,body)>
32 <!ELEMENT Sequent %sequent;>
33 <!ELEMENT Conjecture %sequent;>
34 <!ELEMENT Decl %term;>
36 <!ELEMENT Hidden EMPTY>
37 <!ELEMENT Goal %term;>
38 <!ELEMENT MUTCASE (patternsType,inductiveTerm,pattern* )>
44 exception Getter_failure of string * string
45 exception Parser_failure of string
48 | Arg of string * Cic.annterm (* relative uri, term *)
49 (* constants' body and types resides in differne files, thus we can't simple
50 * keep constants in Cic_obj stack entries *)
51 | Cic_attributes of Cic.attribute list
52 | Cic_constant_body of string * string * UriManager.uri list * Cic.annterm
54 (* id, for, params, body, object attributes *)
55 | Cic_constant_type of string * string * UriManager.uri list * Cic.annterm
57 (* id, name, params, type, object attributes *)
58 | Cic_term of Cic.annterm (* term *)
59 | Cic_obj of Cic.annobj (* object *)
60 | Cofix_fun of Cic.id * string * Cic.annterm * Cic.annterm
61 (* id, name, type, body *)
62 | Constructor of string * Cic.annterm (* name, type *)
63 | Decl of Cic.id * Cic.name * Cic.annterm (* id, binder, source *)
64 | Def of Cic.id * Cic.name * Cic.annterm (* id, binder, source *)
65 | Fix_fun of Cic.id * string * int * Cic.annterm * Cic.annterm
66 (* id, name, ind. index, type, body *)
67 | Inductive_type of string * string * bool * Cic.annterm *
68 (string * Cic.annterm) list (* id, name, inductive, arity, constructors *)
69 | Meta_subst of Cic.annterm option
70 | Tag of string * (string * string) list (* tag name, attributes *)
71 (* ZACK TODO add file position to tag stack entry so that when attribute
72 * errors occur, the position of their _start_tag_ could be printed
73 * instead of the current position (usually the end tag) *)
76 mutable stack: stack_entry list;
77 mutable xml_parser: XmlPushParser.xml_parser option;
78 mutable filename: string;
82 let string_of_stack ctxt =
83 "[" ^ (String.concat "; "
86 | Arg (reluri, _) -> sprintf "Arg %s" reluri
87 | Cic_attributes _ -> "Cic_attributes"
88 | Cic_constant_body (id, name, _, _, _) ->
89 sprintf "Cic_constant_body %s (id=%s)" name id
90 | Cic_constant_type (id, name, _, _, _) ->
91 sprintf "Cic_constant_type %s (id=%s)" name id
92 | Cic_term _ -> "Cic_term"
93 | Cic_obj _ -> "Cic_obj"
94 | Constructor (name, _) -> "Constructor " ^ name
95 | Cofix_fun (id, _, _, _) -> sprintf "Cofix_fun (id=%s)" id
96 | Decl (id, _, _) -> sprintf "Decl (id=%s)" id
97 | Def (id, _, _) -> sprintf "Def (id=%s)" id
98 | Fix_fun (id, _, _, _, _) -> sprintf "Fix_fun (id=%s)" id
99 | Inductive_type (id, name, _, _, _) ->
100 sprintf "Inductive_type %s (id=%s)" name id
101 | Meta_subst _ -> "Meta_subst"
102 | Tag (tag, _) -> "Tag " ^ tag)
105 let compare_attrs (a1, v1) (a2, v2) = Pervasives.compare a1 a2
106 let sort_attrs = List.sort compare_attrs
108 let new_parser_context uri = {
115 let get_parser ctxt =
116 match ctxt.xml_parser with
118 | None -> assert false
120 (** {2 Error handling} *)
122 let parse_error ctxt msg =
123 let (line, col) = XmlPushParser.get_position (get_parser ctxt) in
124 raise (Parser_failure (sprintf "[%s: line %d, column %d] %s"
125 ctxt.filename line col msg))
127 let attribute_error ctxt tag =
128 parse_error ctxt ("wrong attribute set for " ^ tag)
130 (** {2 Parsing context management} *)
133 (* debug_print "pop";*)
134 match ctxt.stack with
135 | hd :: tl -> (ctxt.stack <- tl)
139 (* debug_print "push";*)
140 ctxt.stack <- v :: ctxt.stack
143 (* debug_print "set_top";*)
144 match ctxt.stack with
145 | _ :: tl -> (ctxt.stack <- v :: tl)
148 (** pop the last tag from the open tags stack returning a pair <tag_name,
151 match ctxt.stack with
152 | Tag (tag, attrs) :: tl ->
155 | _ -> parse_error ctxt "unexpected extra content"
157 (** pop the last tag from the open tags stack returning its attributes.
158 * Attributes are returned as a list of pair <name, value> _sorted_ by
160 let pop_tag_attrs ctxt = sort_attrs (snd (pop_tag ctxt))
163 let rec aux acc stack =
165 | Cic_term t :: tl -> aux (t :: acc) tl
168 let values, new_stack = aux [] ctxt.stack in
169 ctxt.stack <- new_stack;
172 let pop_meta_substs ctxt =
173 let rec aux acc stack =
175 | Meta_subst t :: tl -> aux (t :: acc) tl
178 let values, new_stack = aux [] ctxt.stack in
179 ctxt.stack <- new_stack;
182 let pop_fix_funs ctxt =
183 let rec aux acc stack =
185 | Fix_fun (id, name, index, typ, body) :: tl ->
186 aux ((id, name, index, typ, body) :: acc) tl
189 let values, new_stack = aux [] ctxt.stack in
190 ctxt.stack <- new_stack;
193 let pop_cofix_funs ctxt =
194 let rec aux acc stack =
196 | Cofix_fun (id, name, typ, body) :: tl ->
197 aux ((id, name, typ, body) :: acc) tl
200 let values, new_stack = aux [] ctxt.stack in
201 ctxt.stack <- new_stack;
204 let pop_constructors ctxt =
205 let rec aux acc stack =
207 | Constructor (name, t) :: tl -> aux ((name, t) :: acc) tl
210 let values, new_stack = aux [] ctxt.stack in
211 ctxt.stack <- new_stack;
214 let pop_inductive_types ctxt =
215 let rec aux acc stack =
217 | Inductive_type (id, name, ind, arity, ctors) :: tl ->
218 aux ((id, name, ind, arity, ctors) :: acc) tl
221 let values, new_stack = aux [] ctxt.stack in
223 parse_error ctxt "no \"InductiveType\" element found";
224 ctxt.stack <- new_stack;
227 (** travels the stack (without popping) for the first term subject of explicit
228 * named substitution and return its URI *)
229 let find_base_uri ctxt =
230 let rec aux = function
231 | Cic_term (Cic.AConst (_, uri, _)) :: _
232 | Cic_term (Cic.AMutInd (_, uri, _, _)) :: _
233 | Cic_term (Cic.AMutConstruct (_, uri, _, _, _)) :: _
234 | Cic_term (Cic.AVar (_, uri, _)) :: _ ->
236 | Arg _ :: tl -> aux tl
237 | _ -> parse_error ctxt "no \"arg\" element found"
239 UriManager.buri_of_uri (aux ctxt.stack)
241 (** backwardly eats the stack building an explicit named substitution from Arg
243 let pop_subst ctxt base_uri =
244 let rec aux acc stack =
246 | Arg (rel_uri, term) :: tl ->
247 let uri = UriManager.uri_of_string (base_uri ^ "/" ^ rel_uri) in
248 aux ((uri, term) :: acc) tl
251 let subst, new_stack = aux [] ctxt.stack in
253 parse_error ctxt "no \"arg\" element found";
254 ctxt.stack <- new_stack;
258 match ctxt.stack with
259 | Cic_term t :: tl ->
262 | _ -> parse_error ctxt "no cic term found"
264 let pop_obj_attributes ctxt =
265 match ctxt.stack with
266 | Cic_attributes attributes :: tl ->
271 (** {2 Auxiliary functions} *)
273 let uri_of_string = UriManager.uri_of_string
275 let uri_list_of_string =
276 let space_RE = Str.regexp " " in
278 List.map uri_of_string (Str.split space_RE s)
280 let sort_of_string ctxt = function
284 (* CicUniv.restart_numbering (); |+ useful only to test parser +| *)
285 Cic.Type (CicUniv.fresh ~uri:ctxt.uri ())
286 | _ -> parse_error ctxt "sort expected"
288 let patch_subst ctxt subst = function
289 | Cic.AConst (id, uri, _) -> Cic.AConst (id, uri, subst)
290 | Cic.AMutInd (id, uri, typeno, _) ->
291 Cic.AMutInd (id, uri, typeno, subst)
292 | Cic.AMutConstruct (id, uri, typeno, consno, _) ->
293 Cic.AMutConstruct (id, uri, typeno, consno, subst)
294 | Cic.AVar (id, uri, _) -> Cic.AVar (id, uri, subst)
297 ("only \"CONST\", \"VAR\", \"MUTIND\", and \"MUTCONSTRUCT\" can be" ^
300 (** backwardly eats the stack seeking for the first open tag carrying
301 * "helm:exception" attributes. If found return Some of a pair containing
302 * exception name and argument. Return None otherwise *)
303 let find_helm_exception ctxt =
304 let rec aux = function
306 | Tag (_, attrs) :: tl ->
308 let exn = List.assoc "helm:exception" attrs in
310 try List.assoc "helm:exception_arg" attrs with Not_found -> ""
313 with Not_found -> aux tl)
318 (** {2 Push parser callbacks}
319 * each callback needs to be instantiated to a parsing context *)
321 let start_element ctxt tag attrs =
322 (* debug_print (sprintf "<%s%s>" tag (match attrs with | [] -> "" | _ -> " " ^ String.concat " " (List.map (fun (a,v) -> sprintf "%s=\"%s\"" a v) attrs)));*)
323 push ctxt (Tag (tag, attrs))
325 let end_element ctxt tag =
326 (* debug_print (sprintf "</%s>" tag);*)
327 (* debug_print (string_of_stack ctxt);*)
328 let attribute_error () = attribute_error ctxt tag in
329 let parse_error = parse_error ctxt in
330 let sort_of_string = sort_of_string ctxt in
334 (match pop_tag_attrs ctxt with
335 | ["binder", binder; "id", id; "idref", idref; "sort", _;
337 Cic.ARel (id, idref, int_of_string value, binder)
338 | _ -> attribute_error ()))
341 (match pop_tag_attrs ctxt with
342 | ["id", id; "sort", _; "uri", uri] ->
343 Cic.AVar (id, uri_of_string uri, [])
344 | _ -> attribute_error ()))
347 (match pop_tag_attrs ctxt with
348 | ["id", id; "sort", _; "uri", uri] ->
349 Cic.AConst (id, uri_of_string uri, [])
350 | _ -> attribute_error ()))
353 (match pop_tag_attrs ctxt with
354 | ["id", id; "value", sort] -> Cic.ASort (id, sort_of_string sort)
355 | _ -> attribute_error ()))
357 let args = pop_cics ctxt in
359 (match pop_tag_attrs ctxt with
360 | ["id", id; "sort", _] -> Cic.AAppl (id, args)
361 | _ -> attribute_error ()))
363 let source = pop_cic ctxt in
365 (match pop_tag_attrs ctxt with
366 | ["binder", binder; "id", id; "type", _] ->
367 Decl (id, Cic.Name binder, source)
368 | ["id", id; "type", _] -> Decl (id, Cic.Anonymous, source)
369 | _ -> attribute_error ())
370 | "def" -> (* same as "decl" above *)
371 let source = pop_cic ctxt in
373 (match pop_tag_attrs ctxt with
374 | ["binder", binder; "id", id; "sort", _] ->
375 Def (id, Cic.Name binder, source)
376 | ["id", id; "sort", _] -> Def (id, Cic.Anonymous, source)
377 | _ -> attribute_error ())
378 | "arity" (* transparent elements (i.e. which contain a CIC) *)
386 let term = pop_cic ctxt in
387 pop ctxt; (* pops start tag matching current end tag (e.g. <arity>) *)
388 push ctxt (Cic_term term)
389 | "substitution" -> (* optional transparent elements (i.e. which _may_
391 set_top ctxt (* replace <substitution> *)
392 (match ctxt.stack with
393 | Cic_term term :: tl ->
395 (Meta_subst (Some term))
396 | _ -> Meta_subst None)
398 let target = pop_cic ctxt in
399 let rec add_decl target = function
400 | Decl (id, binder, source) :: tl ->
401 add_decl (Cic.AProd (id, binder, source, target)) tl
406 let term = add_decl target ctxt.stack in
407 (match pop_tag_attrs ctxt with
409 | _ -> attribute_error ());
410 push ctxt (Cic_term term)
412 let target = pop_cic ctxt in
413 let rec add_decl target = function
414 | Decl (id, binder, source) :: tl ->
415 add_decl (Cic.ALambda (id, binder, source, target)) tl
420 let term = add_decl target ctxt.stack in
421 (match pop_tag_attrs ctxt with
423 | _ -> attribute_error ());
424 push ctxt (Cic_term term)
426 let target = pop_cic ctxt in
427 let rec add_def target = function
428 | Def (id, binder, source) :: tl ->
429 add_def (Cic.ALetIn (id, binder, source, target)) tl
434 let term = add_def target ctxt.stack in
435 (match pop_tag_attrs ctxt with
437 | _ -> attribute_error ());
438 push ctxt (Cic_term term)
440 let typ = pop_cic ctxt in
441 let term = pop_cic ctxt in
443 (match pop_tag_attrs ctxt with
444 | ["id", id; "sort", _] -> Cic.ACast (id, term, typ)
445 | _ -> attribute_error ()));
448 (match pop_tag_attrs ctxt with
449 | ["id", id] -> Cic.AImplicit (id, None)
450 | ["annotation", annotation; "id", id] ->
451 let implicit_annotation =
452 match annotation with
453 | "closed" -> `Closed
456 | _ -> parse_error "invalid value for \"annotation\" attribute"
458 Cic.AImplicit (id, Some implicit_annotation)
459 | _ -> attribute_error ()))
461 let meta_substs = pop_meta_substs ctxt in
463 (match pop_tag_attrs ctxt with
464 | ["id", id; "no", no; "sort", _] ->
465 Cic.AMeta (id, int_of_string no, meta_substs)
466 | _ -> attribute_error ()));
469 (match pop_tag_attrs ctxt with
470 | ["id", id; "noType", noType; "uri", uri] ->
471 Cic.AMutInd (id, uri_of_string uri, int_of_string noType, [])
472 | _ -> attribute_error ()));
475 (match pop_tag_attrs ctxt with
476 | ["id", id; "noConstr", noConstr; "noType", noType; "sort", _;
478 Cic.AMutConstruct (id, uri_of_string uri, int_of_string noType,
479 int_of_string noConstr, [])
480 | _ -> attribute_error ()));
482 let body = pop_cic ctxt in
483 let typ = pop_cic ctxt in
485 (match pop_tag_attrs ctxt with
486 | ["id", id; "name", name; "recIndex", recIndex] ->
487 Fix_fun (id, name, int_of_string recIndex, typ, body)
488 | _ -> attribute_error ())
490 let body = pop_cic ctxt in
491 let typ = pop_cic ctxt in
493 (match pop_tag_attrs ctxt with
494 | ["id", id; "name", name] ->
495 Cofix_fun (id, name, typ, body)
496 | _ -> attribute_error ())
498 let fix_funs = pop_fix_funs ctxt in
500 (match pop_tag_attrs ctxt with
501 | ["id", id; "noFun", noFun; "sort", _] ->
502 Cic.AFix (id, int_of_string noFun, fix_funs)
503 | _ -> attribute_error ()))
505 let cofix_funs = pop_cofix_funs ctxt in
507 (match pop_tag_attrs ctxt with
508 | ["id", id; "noFun", noFun; "sort", _] ->
509 Cic.ACoFix (id, int_of_string noFun, cofix_funs)
510 | _ -> attribute_error ()))
512 (match pop_cics ctxt with
513 | patternsType :: inductiveTerm :: patterns ->
515 (match pop_tag_attrs ctxt with
516 | ["id", id; "noType", noType; "sort", _; "uriType", uriType] ->
517 Cic.AMutCase (id, uri_of_string uriType, int_of_string noType,
518 patternsType, inductiveTerm, patterns)
519 | _ -> attribute_error ()))
520 | _ -> parse_error "invalid \"MUTCASE\" content")
522 let typ = pop_cic ctxt in
524 (match pop_tag_attrs ctxt with
525 | ["name", name] -> Constructor (name, typ)
526 | _ -> attribute_error ())
528 let constructors = pop_constructors ctxt in
529 let arity = pop_cic ctxt in
531 (match pop_tag_attrs ctxt with
532 | ["id", id; "inductive", inductive; "name", name] ->
533 Inductive_type (id, name, bool_of_string inductive, arity,
535 | _ -> attribute_error ())
536 | "InductiveDefinition" ->
537 let inductive_types = pop_inductive_types ctxt in
538 let obj_attributes = pop_obj_attributes ctxt in
540 (match pop_tag_attrs ctxt with
541 | ["id", id; "noParams", noParams; "params", params] ->
542 Cic.AInductiveDefinition (id, inductive_types,
543 uri_list_of_string params, int_of_string noParams, obj_attributes)
544 | _ -> attribute_error ()))
546 let typ = pop_cic ctxt in
547 let obj_attributes = pop_obj_attributes ctxt in
549 (match pop_tag_attrs ctxt with
550 | ["id", id; "name", name; "params", params] ->
551 Cic_constant_type (id, name, uri_list_of_string params, typ,
553 | _ -> attribute_error ())
555 let body = pop_cic ctxt in
556 let obj_attributes = pop_obj_attributes ctxt in
558 (match pop_tag_attrs ctxt with
559 | ["for", for_; "id", id; "params", params] ->
560 Cic_constant_body (id, for_, uri_list_of_string params, body,
562 | _ -> attribute_error ())
564 let typ = pop_cic ctxt in
566 match pop_cics ctxt with
569 | _ -> parse_error "wrong content for \"Variable\""
571 let obj_attributes = pop_obj_attributes ctxt in
573 (match pop_tag_attrs ctxt with
574 | ["id", id; "name", name; "params", params] ->
575 Cic.AVariable (id, name, body, typ, uri_list_of_string params,
577 | _ -> attribute_error ()))
579 let term = pop_cic ctxt in
581 (match pop_tag_attrs ctxt with
582 | ["relUri", relUri] -> Arg (relUri, term)
583 | _ -> attribute_error ())
585 (* explicit named substitution handling: when the end tag of an element
586 * subject of exlicit named subst (MUTIND, MUTCONSTRUCT, CONST, VAR) it
587 * is stored on the stack with no substitutions (i.e. []). When the end
588 * tag of an "instantiate" element is found we patch the term currently
589 * on the stack with the substitution built from "instantiate" children
591 (* XXX inefficiency here: first travels the <arg> elements in order to
592 * find the baseUri, then in order to build the explicit named subst *)
593 let base_uri = find_base_uri ctxt in
594 let subst = pop_subst ctxt base_uri in
595 let term = pop_cic ctxt in
596 (* comment from CicParser3.ml:
597 * CSC: the "id" optional attribute should be parsed and reflected in
598 * Cic.annterm and id = string_of_xml_attr (n#attribute "id") *)
599 (* replace <instantiate> *)
600 set_top ctxt (Cic_term (patch_subst ctxt subst term))
602 let (_, attrs) = pop_tag ctxt in
603 let rec mk_obj_attributes acc = function
605 | ("generated", "true") :: tl ->
606 mk_obj_attributes (`Generated :: acc) tl
607 | ("class", "coercion") :: tl ->
608 mk_obj_attributes (`Class `Coercion :: acc) tl
609 | ("class", "record") :: tl ->
610 mk_obj_attributes (`Class `Record :: acc) tl
611 | ("class", "projection") :: tl ->
612 mk_obj_attributes (`Class `Projection :: acc) tl
613 | ("class", "elimProp") :: tl ->
614 mk_obj_attributes (`Class (`Elim Cic.Prop) :: acc) tl
615 | ("class", "elimSet") :: tl ->
616 mk_obj_attributes (`Class (`Elim Cic.Set) :: acc) tl
617 | ("class", "elimType") :: tl ->
618 let univ = CicUniv.fresh ~uri:ctxt.uri () in
619 mk_obj_attributes (`Class (`Elim (Cic.Type univ)) :: acc) tl
620 | _ -> attribute_error ()
622 push ctxt (Cic_attributes (mk_obj_attributes [] attrs))
624 match find_helm_exception ctxt with
625 | Some (exn, arg) -> raise (Getter_failure (exn, arg))
626 | None -> parse_error (sprintf "unknown element \"%s\"" tag)
628 (** {2 Parser internals} *)
630 let parse uri filename =
631 let ctxt = new_parser_context uri in
632 ctxt.filename <- filename;
633 let module P = XmlPushParser in
635 P.default_callbacks with
636 P.start_element = Some (start_element ctxt);
637 P.end_element = Some (end_element ctxt);
639 let xml_parser = P.create_parser callbacks in
640 ctxt.xml_parser <- Some xml_parser;
642 P.parse xml_parser (`File filename);
643 (* debug_print (string_of_stack stack);*)
646 | Failure "int_of_string" -> parse_error ctxt "integer number expected"
647 | Invalid_argument "bool_of_string" -> parse_error ctxt "boolean expected"
649 | Getter_failure _ as exn ->
652 raise (Parser_failure ("uncaught exception: " ^ Printexc.to_string exn))
654 (** {2 API implementation} *)
656 let annobj_of_xml uri filename filenamebody =
657 match filenamebody with
659 (match parse uri filename with
660 | Cic_constant_type (id, name, params, typ, obj_attributes) ->
661 Cic.AConstant (id, None, name, None, typ, params, obj_attributes)
663 | _ -> raise (Parser_failure ("no object found in " ^ filename)))
664 | Some filenamebody ->
665 (match parse uri filename, parse uri filenamebody with
666 | Cic_constant_type (type_id, name, params, typ, obj_attributes),
667 Cic_constant_body (body_id, _, _, body, _) ->
668 Cic.AConstant (type_id, Some body_id, name, Some body, typ, params,[])
670 raise (Parser_failure (sprintf "no constant found in %s, %s"
671 filename filenamebody)))
673 let obj_of_xml uri filename filenamebody =
674 Deannotate.deannotate_obj (annobj_of_xml uri filename filenamebody)