From: Claudio Sacerdoti Coen Date: Fri, 24 Jun 2005 08:43:21 +0000 (+0000) Subject: cicPxpParser.ml*, cicParser2.ml* and cicParser3.ml definitely removed X-Git-Tag: INDEXING_NO_PROOFS~83 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1b1ae2b73035d4a09792ee53c51e7c6dd5bbd41c;p=helm.git cicPxpParser.ml*, cicParser2.ml* and cicParser3.ml definitely removed in favour of the cicPushParser.ml* (renamed to cicParser.ml*) --- diff --git a/helm/ocaml/cic/.depend b/helm/ocaml/cic/.depend index 88357dc67..9cf7fc911 100644 --- a/helm/ocaml/cic/.depend +++ b/helm/ocaml/cic/.depend @@ -1,6 +1,5 @@ unshare.cmi: cic.cmo deannotate.cmi: cic.cmo -cicPushParser.cmi: cic.cmo cicParser.cmi: cic.cmo cicUtil.cmi: cic.cmo helmLibraryObjects.cmi: cic.cmo @@ -12,11 +11,9 @@ cicUniv.cmo: cicUniv.cmi cicUniv.cmx: cicUniv.cmi deannotate.cmo: cic.cmo deannotate.cmi deannotate.cmx: cic.cmx deannotate.cmi -cicPushParser.cmo: deannotate.cmi cicUniv.cmi cic.cmo cicPushParser.cmi -cicPushParser.cmx: deannotate.cmx cicUniv.cmx cic.cmx cicPushParser.cmi -cicParser.cmo: cicPushParser.cmi cicParser.cmi -cicParser.cmx: cicPushParser.cmx cicParser.cmi -cicUtil.cmo: cicUniv.cmi cic.cmo cicUtil.cmi -cicUtil.cmx: cicUniv.cmx cic.cmx cicUtil.cmi +cicParser.cmo: deannotate.cmi cicUniv.cmi cic.cmo cicParser.cmi +cicParser.cmx: deannotate.cmx cicUniv.cmx cic.cmx cicParser.cmi +cicUtil.cmo: cic.cmo cicUtil.cmi +cicUtil.cmx: cic.cmx cicUtil.cmi helmLibraryObjects.cmo: cic.cmo helmLibraryObjects.cmi helmLibraryObjects.cmx: cic.cmx helmLibraryObjects.cmi diff --git a/helm/ocaml/cic/Makefile b/helm/ocaml/cic/Makefile index 0d0957e8f..37009b545 100644 --- a/helm/ocaml/cic/Makefile +++ b/helm/ocaml/cic/Makefile @@ -6,7 +6,6 @@ INTERFACE_FILES = \ unshare.mli \ cicUniv.mli \ deannotate.mli \ - cicPushParser.mli \ cicParser.mli \ cicUtil.mli \ helmLibraryObjects.mli diff --git a/helm/ocaml/cic/cicParser.ml b/helm/ocaml/cic/cicParser.ml index c46a20a98..619e947f2 100644 --- a/helm/ocaml/cic/cicParser.ml +++ b/helm/ocaml/cic/cicParser.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2000-2005, HELM Team. +(* Copyright (C) 2004-2005, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -20,8 +20,698 @@ * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. + * http://helm.cs.unibo.it/ *) -include CicPushParser.CicParser +let debug_print = prerr_endline +open Printf + +(* ZACK TODO element from the DTD still to be handled: + + + + + + + +*) + +exception Getter_failure of string * string +exception Parser_failure of string + +type stack_entry = + | Arg of string * Cic.annterm (* relative uri, term *) + (* constants' body and types resides in differne files, thus we can't simple + * keep constants in Cic_obj stack entries *) + | Cic_attributes of Cic.attribute list + | Cic_constant_body of string * string * UriManager.uri list * Cic.annterm + * Cic.attribute list + (* id, for, params, body, object attributes *) + | Cic_constant_type of string * string * UriManager.uri list * Cic.annterm + * Cic.attribute list + (* id, name, params, type, object attributes *) + | Cic_term of Cic.annterm (* term *) + | Cic_obj of Cic.annobj (* object *) + | Cofix_fun of Cic.id * string * Cic.annterm * Cic.annterm + (* id, name, type, body *) + | Constructor of string * Cic.annterm (* name, type *) + | Decl of Cic.id * Cic.name * Cic.annterm (* id, binder, source *) + | Def of Cic.id * Cic.name * Cic.annterm (* id, binder, source *) + | Fix_fun of Cic.id * string * int * Cic.annterm * Cic.annterm + (* id, name, ind. index, type, body *) + | Inductive_type of string * string * bool * Cic.annterm * + (string * Cic.annterm) list (* id, name, inductive, arity, constructors *) + | Meta_subst of Cic.annterm option + | Obj_class of Cic.object_class + | Obj_field of string (* field name *) + | Obj_generated + | Tag of string * (string * string) list (* tag name, attributes *) + (* ZACK TODO add file position to tag stack entry so that when attribute + * errors occur, the position of their _start_tag_ could be printed + * instead of the current position (usually the end tag) *) + +type ctxt = { + mutable stack: stack_entry list; + mutable xml_parser: XmlPushParser.xml_parser option; + mutable filename: string; + uri: UriManager.uri; +} + +let string_of_stack ctxt = + "[" ^ (String.concat "; " + (List.map + (function + | Arg (reluri, _) -> sprintf "Arg %s" reluri + | Cic_attributes _ -> "Cic_attributes" + | Cic_constant_body (id, name, _, _, _) -> + sprintf "Cic_constant_body %s (id=%s)" name id + | Cic_constant_type (id, name, _, _, _) -> + sprintf "Cic_constant_type %s (id=%s)" name id + | Cic_term _ -> "Cic_term" + | Cic_obj _ -> "Cic_obj" + | Constructor (name, _) -> "Constructor " ^ name + | Cofix_fun (id, _, _, _) -> sprintf "Cofix_fun (id=%s)" id + | Decl (id, _, _) -> sprintf "Decl (id=%s)" id + | Def (id, _, _) -> sprintf "Def (id=%s)" id + | Fix_fun (id, _, _, _, _) -> sprintf "Fix_fun (id=%s)" id + | Inductive_type (id, name, _, _, _) -> + sprintf "Inductive_type %s (id=%s)" name id + | Meta_subst _ -> "Meta_subst" + | Obj_class _ -> "Obj_class" + | Obj_field name -> "Obj_field " ^ name + | Obj_generated -> "Obj_generated" + | Tag (tag, _) -> "Tag " ^ tag) + ctxt.stack)) ^ "]" + +let compare_attrs (a1, v1) (a2, v2) = Pervasives.compare a1 a2 +let sort_attrs = List.sort compare_attrs + +let new_parser_context uri = { + stack = []; + xml_parser = None; + filename = "-"; + uri = uri; +} + +let get_parser ctxt = + match ctxt.xml_parser with + | Some p -> p + | None -> assert false + +(** {2 Error handling} *) + +let parse_error ctxt msg = + let (line, col) = XmlPushParser.get_position (get_parser ctxt) in + raise (Parser_failure (sprintf "[%s: line %d, column %d] %s" + ctxt.filename line col msg)) + +let attribute_error ctxt tag = + parse_error ctxt ("wrong attribute set for " ^ tag) + +(** {2 Parsing context management} *) + +let pop ctxt = +(* debug_print "pop";*) + match ctxt.stack with + | hd :: tl -> (ctxt.stack <- tl) + | _ -> assert false + +let push ctxt v = +(* debug_print "push";*) + ctxt.stack <- v :: ctxt.stack + +let set_top ctxt v = +(* debug_print "set_top";*) + match ctxt.stack with + | _ :: tl -> (ctxt.stack <- v :: tl) + | _ -> assert false + + (** pop the last tag from the open tags stack returning a pair *) +let pop_tag ctxt = + match ctxt.stack with + | Tag (tag, attrs) :: tl -> + ctxt.stack <- tl; + (tag, attrs) + | _ -> parse_error ctxt "unexpected extra content" + + (** pop the last tag from the open tags stack returning its attributes. + * Attributes are returned as a list of pair _sorted_ by + * attribute name *) +let pop_tag_attrs ctxt = sort_attrs (snd (pop_tag ctxt)) + +let pop_cics ctxt = + let rec aux acc stack = + match stack with + | Cic_term t :: tl -> aux (t :: acc) tl + | tl -> acc, tl + in + let values, new_stack = aux [] ctxt.stack in + ctxt.stack <- new_stack; + values + +let pop_class_modifiers ctxt = + let rec aux acc stack = + match stack with + | (Cic_term (Cic.ASort _) as m) :: tl + | (Obj_field _ as m) :: tl -> + aux (m :: acc) tl + | tl -> acc, tl + in + let values, new_stack = aux [] ctxt.stack in + ctxt.stack <- new_stack; + values + +let pop_meta_substs ctxt = + let rec aux acc stack = + match stack with + | Meta_subst t :: tl -> aux (t :: acc) tl + | tl -> acc, tl + in + let values, new_stack = aux [] ctxt.stack in + ctxt.stack <- new_stack; + values + +let pop_fix_funs ctxt = + let rec aux acc stack = + match stack with + | Fix_fun (id, name, index, typ, body) :: tl -> + aux ((id, name, index, typ, body) :: acc) tl + | tl -> acc, tl + in + let values, new_stack = aux [] ctxt.stack in + ctxt.stack <- new_stack; + values + +let pop_cofix_funs ctxt = + let rec aux acc stack = + match stack with + | Cofix_fun (id, name, typ, body) :: tl -> + aux ((id, name, typ, body) :: acc) tl + | tl -> acc, tl + in + let values, new_stack = aux [] ctxt.stack in + ctxt.stack <- new_stack; + values + +let pop_constructors ctxt = + let rec aux acc stack = + match stack with + | Constructor (name, t) :: tl -> aux ((name, t) :: acc) tl + | tl -> acc, tl + in + let values, new_stack = aux [] ctxt.stack in + ctxt.stack <- new_stack; + values + +let pop_inductive_types ctxt = + let rec aux acc stack = + match stack with + | Inductive_type (id, name, ind, arity, ctors) :: tl -> + aux ((id, name, ind, arity, ctors) :: acc) tl + | tl -> acc, tl + in + let values, new_stack = aux [] ctxt.stack in + if values = [] then + parse_error ctxt "no \"InductiveType\" element found"; + ctxt.stack <- new_stack; + values + + (** travels the stack (without popping) for the first term subject of explicit + * named substitution and return its URI *) +let find_base_uri ctxt = + let rec aux = function + | Cic_term (Cic.AConst (_, uri, _)) :: _ + | Cic_term (Cic.AMutInd (_, uri, _, _)) :: _ + | Cic_term (Cic.AMutConstruct (_, uri, _, _, _)) :: _ + | Cic_term (Cic.AVar (_, uri, _)) :: _ -> + uri + | Arg _ :: tl -> aux tl + | _ -> parse_error ctxt "no \"arg\" element found" + in + UriManager.buri_of_uri (aux ctxt.stack) + + (** backwardly eats the stack building an explicit named substitution from Arg + * stack entries *) +let pop_subst ctxt base_uri = + let rec aux acc stack = + match stack with + | Arg (rel_uri, term) :: tl -> + let uri = UriManager.uri_of_string (base_uri ^ "/" ^ rel_uri) in + aux ((uri, term) :: acc) tl + | tl -> acc, tl + in + let subst, new_stack = aux [] ctxt.stack in + if subst = [] then + parse_error ctxt "no \"arg\" element found"; + ctxt.stack <- new_stack; + subst + +let pop_cic ctxt = + match ctxt.stack with + | Cic_term t :: tl -> + ctxt.stack <- tl; + t + | _ -> parse_error ctxt "no cic term found" + +let pop_obj_attributes ctxt = + match ctxt.stack with + | Cic_attributes attributes :: tl -> + ctxt.stack <- tl; + attributes + | _ -> [] + +(** {2 Auxiliary functions} *) + +let uri_of_string = UriManager.uri_of_string + +let uri_list_of_string = + let space_RE = Str.regexp " " in + fun s -> + List.map uri_of_string (Str.split space_RE s) + +let sort_of_string ctxt = function + | "Prop" -> Cic.Prop + | "Set" -> Cic.Set + | "Type" -> Cic.Type (CicUniv.fresh ~uri:ctxt.uri ()) +(* | "Type" -> CicUniv.restart_numbering (); |+ useful only to test parser +| *) + | "CProp" -> Cic.CProp + | _ -> parse_error ctxt "sort expected" + +let patch_subst ctxt subst = function + | Cic.AConst (id, uri, _) -> Cic.AConst (id, uri, subst) + | Cic.AMutInd (id, uri, typeno, _) -> + Cic.AMutInd (id, uri, typeno, subst) + | Cic.AMutConstruct (id, uri, typeno, consno, _) -> + Cic.AMutConstruct (id, uri, typeno, consno, subst) + | Cic.AVar (id, uri, _) -> Cic.AVar (id, uri, subst) + | _ -> + parse_error ctxt + ("only \"CONST\", \"VAR\", \"MUTIND\", and \"MUTCONSTRUCT\" can be" ^ + " instantiated") + + (** backwardly eats the stack seeking for the first open tag carrying + * "helm:exception" attributes. If found return Some of a pair containing + * exception name and argument. Return None otherwise *) +let find_helm_exception ctxt = + let rec aux = function + | [] -> None + | Tag (_, attrs) :: tl -> + (try + let exn = List.assoc "helm:exception" attrs in + let arg = + try List.assoc "helm:exception_arg" attrs with Not_found -> "" + in + Some (exn, arg) + with Not_found -> aux tl) + | _ :: tl -> aux tl + in + aux ctxt.stack + +(** {2 Push parser callbacks} + * each callback needs to be instantiated to a parsing context *) + +let start_element ctxt tag attrs = +(* debug_print (sprintf "<%s%s>" tag (match attrs with | [] -> "" | _ -> " " ^ String.concat " " (List.map (fun (a,v) -> sprintf "%s=\"%s\"" a v) attrs)));*) + push ctxt (Tag (tag, attrs)) + +let end_element ctxt tag = +(* debug_print (sprintf "" tag);*) +(* debug_print (string_of_stack ctxt);*) + let attribute_error () = attribute_error ctxt tag in + let parse_error = parse_error ctxt in + let sort_of_string = sort_of_string ctxt in + match tag with + | "REL" -> + push ctxt (Cic_term + (match pop_tag_attrs ctxt with + | ["binder", binder; "id", id; "idref", idref; "sort", _; + "value", value] -> + Cic.ARel (id, idref, int_of_string value, binder) + | _ -> attribute_error ())) + | "VAR" -> + push ctxt (Cic_term + (match pop_tag_attrs ctxt with + | ["id", id; "sort", _; "uri", uri] -> + Cic.AVar (id, uri_of_string uri, []) + | _ -> attribute_error ())) + | "CONST" -> + push ctxt (Cic_term + (match pop_tag_attrs ctxt with + | ["id", id; "sort", _; "uri", uri] -> + Cic.AConst (id, uri_of_string uri, []) + | _ -> attribute_error ())) + | "SORT" -> + push ctxt (Cic_term + (match pop_tag_attrs ctxt with + | ["id", id; "value", sort] -> Cic.ASort (id, sort_of_string sort) + | _ -> attribute_error ())) + | "APPLY" -> + let args = pop_cics ctxt in + push ctxt (Cic_term + (match pop_tag_attrs ctxt with + | ["id", id; "sort", _] -> Cic.AAppl (id, args) + | _ -> attribute_error ())) + | "decl" -> + let source = pop_cic ctxt in + push ctxt + (match pop_tag_attrs ctxt with + | ["binder", binder; "id", id; "type", _] -> + Decl (id, Cic.Name binder, source) + | ["id", id; "type", _] -> Decl (id, Cic.Anonymous, source) + | _ -> attribute_error ()) + | "def" -> (* same as "decl" above *) + let source = pop_cic ctxt in + push ctxt + (match pop_tag_attrs ctxt with + | ["binder", binder; "id", id; "sort", _] -> + Def (id, Cic.Name binder, source) + | ["id", id; "sort", _] -> Def (id, Cic.Anonymous, source) + | _ -> attribute_error ()) + | "arity" (* transparent elements (i.e. which contain a CIC) *) + | "body" + | "inductiveTerm" + | "pattern" + | "patternsType" + | "target" + | "term" + | "type" -> + let term = pop_cic ctxt in + pop ctxt; (* pops start tag matching current end tag (e.g. ) *) + push ctxt (Cic_term term) + | "substitution" -> (* optional transparent elements (i.e. which _may_ + * contain a CIC) *) + set_top ctxt (* replace *) + (match ctxt.stack with + | Cic_term term :: tl -> + ctxt.stack <- tl; + (Meta_subst (Some term)) + | _ -> Meta_subst None) + | "PROD" -> + let target = pop_cic ctxt in + let rec add_decl target = function + | Decl (id, binder, source) :: tl -> + add_decl (Cic.AProd (id, binder, source, target)) tl + | tl -> + ctxt.stack <- tl; + target + in + let term = add_decl target ctxt.stack in + (match pop_tag_attrs ctxt with + | ["type", _] -> () + | _ -> attribute_error ()); + push ctxt (Cic_term term) + | "LAMBDA" -> + let target = pop_cic ctxt in + let rec add_decl target = function + | Decl (id, binder, source) :: tl -> + add_decl (Cic.ALambda (id, binder, source, target)) tl + | tl -> + ctxt.stack <- tl; + target + in + let term = add_decl target ctxt.stack in + (match pop_tag_attrs ctxt with + | ["sort", _] -> () + | _ -> attribute_error ()); + push ctxt (Cic_term term) + | "LETIN" -> + let target = pop_cic ctxt in + let rec add_def target = function + | Def (id, binder, source) :: tl -> + add_def (Cic.ALetIn (id, binder, source, target)) tl + | tl -> + ctxt.stack <- tl; + target + in + let term = add_def target ctxt.stack in + (match pop_tag_attrs ctxt with + | ["sort", _] -> () + | _ -> attribute_error ()); + push ctxt (Cic_term term) + | "CAST" -> + let typ = pop_cic ctxt in + let term = pop_cic ctxt in + push ctxt (Cic_term + (match pop_tag_attrs ctxt with + | ["id", id; "sort", _] -> Cic.ACast (id, term, typ) + | _ -> attribute_error ())); + | "IMPLICIT" -> + push ctxt (Cic_term + (match pop_tag_attrs ctxt with + | ["id", id] -> Cic.AImplicit (id, None) + | ["annotation", annotation; "id", id] -> + let implicit_annotation = + match annotation with + | "closed" -> `Closed + | "hole" -> `Hole + | "type" -> `Type + | _ -> parse_error "invalid value for \"annotation\" attribute" + in + Cic.AImplicit (id, Some implicit_annotation) + | _ -> attribute_error ())) + | "META" -> + let meta_substs = pop_meta_substs ctxt in + push ctxt (Cic_term + (match pop_tag_attrs ctxt with + | ["id", id; "no", no; "sort", _] -> + Cic.AMeta (id, int_of_string no, meta_substs) + | _ -> attribute_error ())); + | "MUTIND" -> + push ctxt (Cic_term + (match pop_tag_attrs ctxt with + | ["id", id; "noType", noType; "uri", uri] -> + Cic.AMutInd (id, uri_of_string uri, int_of_string noType, []) + | _ -> attribute_error ())); + | "MUTCONSTRUCT" -> + push ctxt (Cic_term + (match pop_tag_attrs ctxt with + | ["id", id; "noConstr", noConstr; "noType", noType; "sort", _; + "uri", uri] -> + Cic.AMutConstruct (id, uri_of_string uri, int_of_string noType, + int_of_string noConstr, []) + | _ -> attribute_error ())); + | "FixFunction" -> + let body = pop_cic ctxt in + let typ = pop_cic ctxt in + push ctxt + (match pop_tag_attrs ctxt with + | ["id", id; "name", name; "recIndex", recIndex] -> + Fix_fun (id, name, int_of_string recIndex, typ, body) + | _ -> attribute_error ()) + | "CofixFunction" -> + let body = pop_cic ctxt in + let typ = pop_cic ctxt in + push ctxt + (match pop_tag_attrs ctxt with + | ["id", id; "name", name] -> + Cofix_fun (id, name, typ, body) + | _ -> attribute_error ()) + | "FIX" -> + let fix_funs = pop_fix_funs ctxt in + push ctxt (Cic_term + (match pop_tag_attrs ctxt with + | ["id", id; "noFun", noFun; "sort", _] -> + Cic.AFix (id, int_of_string noFun, fix_funs) + | _ -> attribute_error ())) + | "COFIX" -> + let cofix_funs = pop_cofix_funs ctxt in + push ctxt (Cic_term + (match pop_tag_attrs ctxt with + | ["id", id; "noFun", noFun; "sort", _] -> + Cic.ACoFix (id, int_of_string noFun, cofix_funs) + | _ -> attribute_error ())) + | "MUTCASE" -> + (match pop_cics ctxt with + | patternsType :: inductiveTerm :: patterns -> + push ctxt (Cic_term + (match pop_tag_attrs ctxt with + | ["id", id; "noType", noType; "sort", _; "uriType", uriType] -> + Cic.AMutCase (id, uri_of_string uriType, int_of_string noType, + patternsType, inductiveTerm, patterns) + | _ -> attribute_error ())) + | _ -> parse_error "invalid \"MUTCASE\" content") + | "Constructor" -> + let typ = pop_cic ctxt in + push ctxt + (match pop_tag_attrs ctxt with + | ["name", name] -> Constructor (name, typ) + | _ -> attribute_error ()) + | "InductiveType" -> + let constructors = pop_constructors ctxt in + let arity = pop_cic ctxt in + push ctxt + (match pop_tag_attrs ctxt with + | ["id", id; "inductive", inductive; "name", name] -> + Inductive_type (id, name, bool_of_string inductive, arity, + constructors) + | _ -> attribute_error ()) + | "InductiveDefinition" -> + let inductive_types = pop_inductive_types ctxt in + let obj_attributes = pop_obj_attributes ctxt in + push ctxt (Cic_obj + (match pop_tag_attrs ctxt with + | ["id", id; "noParams", noParams; "params", params] -> + Cic.AInductiveDefinition (id, inductive_types, + uri_list_of_string params, int_of_string noParams, obj_attributes) + | _ -> attribute_error ())) + | "ConstantType" -> + let typ = pop_cic ctxt in + let obj_attributes = pop_obj_attributes ctxt in + push ctxt + (match pop_tag_attrs ctxt with + | ["id", id; "name", name; "params", params] -> + Cic_constant_type (id, name, uri_list_of_string params, typ, + obj_attributes) + | _ -> attribute_error ()) + | "ConstantBody" -> + let body = pop_cic ctxt in + let obj_attributes = pop_obj_attributes ctxt in + push ctxt + (match pop_tag_attrs ctxt with + | ["for", for_; "id", id; "params", params] -> + Cic_constant_body (id, for_, uri_list_of_string params, body, + obj_attributes) + | _ -> attribute_error ()) + | "Variable" -> + let typ = pop_cic ctxt in + let body = + match pop_cics ctxt with + | [] -> None + | [t] -> Some t + | _ -> parse_error "wrong content for \"Variable\"" + in + let obj_attributes = pop_obj_attributes ctxt in + push ctxt (Cic_obj + (match pop_tag_attrs ctxt with + | ["id", id; "name", name; "params", params] -> + Cic.AVariable (id, name, body, typ, uri_list_of_string params, + obj_attributes) + | _ -> attribute_error ())) + | "arg" -> + let term = pop_cic ctxt in + push ctxt + (match pop_tag_attrs ctxt with + | ["relUri", relUri] -> Arg (relUri, term) + | _ -> attribute_error ()) + | "instantiate" -> + (* explicit named substitution handling: when the end tag of an element + * subject of exlicit named subst (MUTIND, MUTCONSTRUCT, CONST, VAR) it + * is stored on the stack with no substitutions (i.e. []). When the end + * tag of an "instantiate" element is found we patch the term currently + * on the stack with the substitution built from "instantiate" children + *) + (* XXX inefficiency here: first travels the elements in order to + * find the baseUri, then in order to build the explicit named subst *) + let base_uri = find_base_uri ctxt in + let subst = pop_subst ctxt base_uri in + let term = pop_cic ctxt in + (* comment from CicParser3.ml: + * CSC: the "id" optional attribute should be parsed and reflected in + * Cic.annterm and id = string_of_xml_attr (n#attribute "id") *) + (* replace *) + set_top ctxt (Cic_term (patch_subst ctxt subst term)) + | "attributes" -> + let rec aux acc = function (* retrieve object attributes *) + | Obj_class c :: tl -> aux (`Class c :: acc) tl + | Obj_generated :: tl -> aux (`Generated :: acc) tl + | tl -> acc, tl + in + let obj_attrs, new_stack = aux [] ctxt.stack in + ctxt.stack <- new_stack; + set_top ctxt (Cic_attributes obj_attrs) + | "generated" -> set_top ctxt Obj_generated + | "field" -> + push ctxt + (match pop_tag_attrs ctxt with + | ["name", name] -> Obj_field name + | _ -> attribute_error ()) + | "class" -> + let class_modifiers = pop_class_modifiers ctxt in + push ctxt + (match pop_tag_attrs ctxt with + | ["value", "coercion"] -> Obj_class `Coercion + | ["value", "elim"] -> + (match class_modifiers with + | [Cic_term (Cic.ASort (_, sort))] -> Obj_class (`Elim sort) + | _ -> + parse_error + "unexpected extra content for \"elim\" object class") + | ["value", "record"] -> + let fields = + List.map + (function + | Obj_field name -> name + | _ -> + parse_error + "unexpected extra content for \"record\" object class") + class_modifiers + in + Obj_class (`Record fields) + | ["value", "projection"] -> Obj_class `Projection + | _ -> attribute_error ()) + | tag -> + match find_helm_exception ctxt with + | Some (exn, arg) -> raise (Getter_failure (exn, arg)) + | None -> parse_error (sprintf "unknown element \"%s\"" tag) + +(** {2 Parser internals} *) + +let parse uri filename = + let ctxt = new_parser_context uri in + ctxt.filename <- filename; + let module P = XmlPushParser in + let callbacks = { + P.default_callbacks with + P.start_element = Some (start_element ctxt); + P.end_element = Some (end_element ctxt); + } in + let xml_parser = P.create_parser callbacks in + ctxt.xml_parser <- Some xml_parser; + try + (try + P.parse xml_parser (`Gzip_file filename); + with exn -> + ctxt.xml_parser <- None; + (* ZACK: the above "<- None" is vital for garbage collection. Without it + * we keep in memory a circular structure parser -> callbacks -> ctxt -> + * parser. I don't know if the ocaml garbage collector is supposed to + * collect such structures, but for sure the expat bindings will (orribly) + * leak when used in conjunction with such structures *) + raise exn); + ctxt.xml_parser <- None; (* ZACK: same comment as above *) +(* debug_print (string_of_stack stack);*) + (* assert (List.length ctxt.stack = 1) *) + List.hd ctxt.stack + with + | Failure "int_of_string" -> parse_error ctxt "integer number expected" + | Invalid_argument "bool_of_string" -> parse_error ctxt "boolean expected" + | P.Parse_error msg -> parse_error ctxt ("parse error: " ^ msg) + | Parser_failure _ + | Getter_failure _ as exn -> + raise exn + | exn -> + raise (Parser_failure ("uncaught exception: " ^ Printexc.to_string exn)) + +(** {2 API implementation} *) + +let annobj_of_xml uri filename filenamebody = + match filenamebody with + | None -> + (match parse uri filename with + | Cic_constant_type (id, name, params, typ, obj_attributes) -> + Cic.AConstant (id, None, name, None, typ, params, obj_attributes) + | Cic_obj obj -> obj + | _ -> raise (Parser_failure ("no object found in " ^ filename))) + | Some filenamebody -> + (match parse uri filename, parse uri filenamebody with + | Cic_constant_type (type_id, name, params, typ, obj_attributes), + Cic_constant_body (body_id, _, _, body, _) -> + Cic.AConstant (type_id, Some body_id, name, Some body, typ, params,[]) + | _ -> + raise (Parser_failure (sprintf "no constant found in %s, %s" + filename filenamebody))) + +let obj_of_xml uri filename filenamebody = + Deannotate.deannotate_obj (annobj_of_xml uri filename filenamebody) diff --git a/helm/ocaml/cic/cicParser2.ml b/helm/ocaml/cic/cicParser2.ml deleted file mode 100644 index b641c649e..000000000 --- a/helm/ocaml/cic/cicParser2.ml +++ /dev/null @@ -1,258 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 24/01/2000 *) -(* *) -(* This module is the objects level of a parser for cic objects from xml *) -(* files to the internal representation. It uses the module cicParser3 *) -(* cicParser3 (terms level) and it is used only through cicParser2 (top *) -(* level). *) -(* *) -(******************************************************************************) - -exception IllFormedXml of int;; -exception NotImplemented;; - - (* TODO ZACK implement attributes parsing from XML. ATM, parsing always - * returns the empty list of attributes reported here *) -let obj_attributes = [] -let get_obj_attributes (n: 'a Pxp_document.node) = - obj_attributes - -(* Utility functions that transform a Pxp attribute into something useful *) - -let uri_list_of_attr a = - let module T = Pxp_types in - match a with - T.Value s -> - List.map UriManager.uri_of_string (Str.split (Str.regexp " ") s) - | _ -> raise (IllFormedXml 0) -;; - -let string_of_attr a = - let module T = Pxp_types in - match a with - T.Value s -> s - | _ -> raise (IllFormedXml 0) -;; - -let int_of_attr a = - int_of_string (string_of_attr a) -;; - -let bool_of_attr a = - bool_of_string (string_of_attr a) -;; - -let name_of_attr a = - let module T = Pxp_types in - let module C = Cic in - match a with - T.Value s -> C.Name s - | T.Implied_value -> C.Anonymous - | _ -> raise (IllFormedXml 0) -;; - -(* Other utility functions *) - -let get_content n = - match n#sub_nodes with - [ t ] -> t - | _ -> raise (IllFormedXml 1) -;; - -(* Functions that, given the list of sons of a node of the cic dom (objects *) -(* level), retrieve the internal representation associated to the node. *) -(* Everytime a cic term subtree is found, it is translated to the internal *) -(* representation using the method to_cic_term defined in cicParser3. *) -(* Each function raise IllFormedXml if something goes wrong, but this should *) -(* be impossible due to the presence of the dtd *) -(* The functions should really be obvious looking at their name and the cic *) -(* dtd *) - -(* called when a CurrentProof is found *) -let get_conjs_value l = - let rec rget (c, v) l = - let module D = Pxp_document in - match l with - [] -> (c, v) - | conj::tl when conj#node_type = D.T_element "Conjecture" -> - let no = int_of_attr (conj#attribute "no") in - let id = string_of_attr (conj#attribute "id") in - let typ,canonical_context = - match List.rev (conj#sub_nodes) with - [] -> raise (IllFormedXml 13) - | typ::canonical_context -> - (get_content typ)#extension#to_cic_term [], - List.map - (function n -> - let id = string_of_attr (n#attribute "id") in - match n#node_type with - D.T_element "Decl" -> - let name = name_of_attr (n#attribute "name") in - let term = (get_content n)#extension#to_cic_term [] in - id, Some (name,Cic.ADecl term) - | D.T_element "Def" -> - let name = name_of_attr (n#attribute "name") in - let term = (get_content n)#extension#to_cic_term [] in - id, Some (name,Cic.ADef term) - | D.T_element "Hidden" -> id, None - | _ -> raise (IllFormedXml 14) - ) canonical_context - in - rget ((id, no, canonical_context, typ)::c, v) tl - | value::tl when value#node_type = D.T_element "body" -> - let v' = (get_content value)#extension#to_cic_term [] in - (match v with - None -> rget (c, Some v') tl - | _ -> raise (IllFormedXml 2) - ) - | _ -> raise (IllFormedXml 4) - in - match rget ([], None) l with - (revc, Some v) -> (List.rev revc, v) - | _ -> raise (IllFormedXml 5) -;; - -(* used only by get_inductive_types; called one time for each inductive *) -(* definitions in a block of inductive definitions *) -let get_names_arity_constructors l = - let rec rget (a,c) l = - let module D = Pxp_document in - match l with - [] -> (a, c) - | arity::tl when arity#node_type = D.T_element "arity" -> - let a' = (get_content arity)#extension#to_cic_term [] in - rget (Some a',c) tl - | con::tl when con#node_type = D.T_element "Constructor" -> - let id = string_of_attr (con#attribute "name") - and ty = (get_content con)#extension#to_cic_term [] in - rget (a,(id,ty)::c) tl - | _ -> raise (IllFormedXml 9) - in - match rget (None,[]) l with - (Some a, c) -> (a, List.rev c) - | _ -> raise (IllFormedXml 8) -;; - -(* called when an InductiveDefinition is found *) -let rec get_inductive_types = - function - [] -> [] - | he::tl -> - let tyname = string_of_attr (he#attribute "name") - and inductive = bool_of_attr (he#attribute "inductive") - and xid = string_of_attr (he#attribute "id") - and (arity,cons) = - get_names_arity_constructors (he#sub_nodes) - in - (xid,tyname,inductive,arity,cons)::(get_inductive_types tl) -;; - -(* This is the main function and also the only one used directly from *) -(* cicParser. Given the root of the dom tree, it returns the internal *) -(* representation of the cic object described in the tree *) -(* It uses the previous functions and the to_cic_term method defined *) -(* in cicParser3 (used for subtrees that encode cic terms) *) -let rec get_term (n : CicParser3.cic_term Pxp_document.node) nbody -= - let module U = UriManager in - let module D = Pxp_document in - let module C = Cic in - let obj_attrs = get_obj_attributes n in - let ntype = n#node_type in - match ntype with - D.T_element "ConstantType" -> - let name = string_of_attr (n # attribute "name") in - let params = uri_list_of_attr (n#attribute "params") in - let xid = string_of_attr (n#attribute "id") in - let typ = (get_content n)#extension#to_cic_term [] in - (match nbody with - None -> - (* Axiom *) - C.AConstant (xid, None, name, None, typ, params, obj_attrs) - | Some nbody' -> - let nbodytype = nbody'#node_type in - match nbodytype with - D.T_element "ConstantBody" -> -(*CSC: the attribute "for" is ignored and not checked - let for_ = string_of_attr (nbody'#attribute "for") in -*) - let paramsbody = uri_list_of_attr (nbody'#attribute "params") in - let xidbody = string_of_attr (nbody'#attribute "id") in - let value = (get_content nbody')#extension#to_cic_term [] in - if paramsbody = params then - C.AConstant (xid, Some xidbody, name, Some value, typ, params, - obj_attrs) - else - raise (IllFormedXml 6) - | D.T_element "CurrentProof" -> -(*CSC: the attribute "of" is ignored and not checked - let for_ = string_of_attr (nbody'#attribute "of") in -*) - let xidbody = string_of_attr (nbody'#attribute "id") in - let sons = nbody'#sub_nodes in - let (conjs, value) = get_conjs_value sons in - C.ACurrentProof (xid, xidbody, name, conjs, value, typ, params, - obj_attrs) - | D.T_element _ - | D.T_data - | _ -> raise (IllFormedXml 6) - ) - | D.T_element "InductiveDefinition" -> - let sons = n#sub_nodes - and xid = string_of_attr (n#attribute "id") in - let inductiveTypes = get_inductive_types sons - and params = uri_list_of_attr (n#attribute "params") - and nparams = int_of_attr (n#attribute "noParams") in - C.AInductiveDefinition (xid, inductiveTypes, params, nparams, obj_attrs) - | D.T_element "Variable" -> - let name = string_of_attr (n#attribute "name") - and params = uri_list_of_attr (n#attribute "params") - and xid = string_of_attr (n#attribute "id") - and (body, typ) = - let sons = n#sub_nodes in - match sons with - [b ; t] when - b#node_type = D.T_element "body" && - t#node_type = D.T_element "type" -> - let b' = get_content b - and t' = get_content t in - (Some (b'#extension#to_cic_term []), t'#extension#to_cic_term []) - | [t] when t#node_type = D.T_element "type" -> - let t' = get_content t in - (None, t'#extension#to_cic_term []) - | _ -> raise (IllFormedXml 6) - in - C.AVariable (xid,name,body,typ,params,obj_attrs) - | D.T_element _ - | D.T_data - | _ -> raise (IllFormedXml 7) -;; diff --git a/helm/ocaml/cic/cicParser2.mli b/helm/ocaml/cic/cicParser2.mli deleted file mode 100644 index 1d95f35ee..000000000 --- a/helm/ocaml/cic/cicParser2.mli +++ /dev/null @@ -1,52 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 24/01/2000 *) -(* *) -(* This module is the objects level of a parser for cic objects from xml *) -(* files to the internal representation. It uses the module cicParser3 *) -(* cicParser3 (terms level) and it is used only through cicParser2 (top *) -(* level). *) -(* *) -(******************************************************************************) - -exception IllFormedXml of int -exception NotImplemented - -(* This is the main function and also the only one used directly from *) -(* cicParser. Given the root of the dom tree and, possibly, also the *) -(* root of the dom tree of the constant body, it returns the internal *) -(* representation of the cic object described in the tree(s). *) -(* It uses the previous functions and the to_cic_term method defined *) -(* in cicParser3 (used for subtrees that encode cic terms) *) -val get_term : - CicParser3.cic_term Pxp_document.node -> - CicParser3.cic_term Pxp_document.node option -> - Cic.annobj diff --git a/helm/ocaml/cic/cicParser3.ml b/helm/ocaml/cic/cicParser3.ml deleted file mode 100644 index 940e03e2b..000000000 --- a/helm/ocaml/cic/cicParser3.ml +++ /dev/null @@ -1,556 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 24/01/2000 *) -(* *) -(* This module is the terms level of a parser for cic objects from xml *) -(* files to the internal representation. It is used by the module cicParser2 *) -(* (objects level). It defines an extension of the standard dom using the *) -(* object-oriented extension machinery of markup: an object with a method *) -(* to_cic_term that returns the internal representation of the subtree is *) -(* added to each node of the dom tree *) -(* *) -(******************************************************************************) - -exception IllFormedXml of int;; - -(* Utility functions to map a markup attribute to something useful *) - -let uri = ref (UriManager.uri_of_string "cic:/none.con") - -let set_uri u = - uri := u - -let cic_attr_of_xml_attr = - function - Pxp_types.Value s -> Cic.Name s - | Pxp_types.Implied_value -> Cic.Anonymous - | _ -> raise (IllFormedXml 1) - -let cic_sort_of_xml_attr = - function - Pxp_types.Value "Prop" -> Cic.Prop - | Pxp_types.Value "Set" -> Cic.Set - | Pxp_types.Value "Type" -> - Cic.Type (CicUniv.fresh ~uri:!uri ()) (* ORRIBLE HACK *) - | _ -> raise (IllFormedXml 2) - -let int_of_xml_attr = - function - Pxp_types.Value n -> int_of_string n - | _ -> raise (IllFormedXml 3) - -let uri_of_xml_attr = - function - Pxp_types.Value s -> UriManager.uri_of_string s - | _ -> raise (IllFormedXml 4) - -let string_of_xml_attr = - function - Pxp_types.Value s -> s - | _ -> raise (IllFormedXml 5) - -let binder_of_xml_attr = - function - Pxp_types.Value s -> s - | _ -> raise (IllFormedXml 17) -;; - -(* the "interface" of the class linked to each node of the dom tree *) - -class virtual cic_term = - object (self) - - (* fields and methods always required by markup *) - val mutable node = (None : cic_term Pxp_document.node option) - - method clone = {< >} - method node = - match node with - None -> - assert false - | Some n -> n - method set_node n = - node <- Some n - - (* a method that returns the internal representation of the tree (term) *) - (* rooted in this node *) - method virtual to_cic_term : - (UriManager.uri * Cic.annterm) list -> Cic.annterm - end -;; - -(* the class of the objects linked to nodes that are not roots of cic terms *) -class eltype_not_of_cic = - object (self) - - inherit cic_term - - method to_cic_term _ = raise (IllFormedXml 6) - end -;; - -(* the class of the objects linked to nodes whose content is a cic term *) -(* (syntactic sugar xml entities) e.g. ... *) -class eltype_transparent = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - assert (exp_named_subst = []) ; - let n = self#node in - match n#sub_nodes with - [ t ] -> t#extension#to_cic_term [] - | _ -> raise (IllFormedXml 7) - end -;; - -(* A class for each cic node type *) - -class eltype_fix = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - assert (exp_named_subst = []) ; - let n = self#node in - let nofun = int_of_xml_attr (n#attribute "noFun") - and id = string_of_xml_attr (n#attribute "id") - and functions = - let sons = n#sub_nodes in - List.map - (function - f when f#node_type = Pxp_document.T_element "FixFunction" -> - let name = string_of_xml_attr (f#attribute "name") - and id = string_of_xml_attr (f#attribute "id") - and recindex = int_of_xml_attr (f#attribute "recIndex") - and (ty, body) = - match f#sub_nodes with - [t ; b] when - t#node_type = Pxp_document.T_element "type" && - b#node_type = Pxp_document.T_element "body" -> - (t#extension#to_cic_term [], b#extension#to_cic_term []) - | _ -> raise (IllFormedXml 14) - in - (id, name, recindex, ty, body) - | _ -> raise (IllFormedXml 13) - ) sons - in - Cic.AFix (id, nofun, functions) - end -;; - -class eltype_cofix = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - assert (exp_named_subst = []) ; - let n = self#node in - let nofun = int_of_xml_attr (n#attribute "noFun") - and id = string_of_xml_attr (n#attribute "id") - and functions = - let sons = n#sub_nodes in - List.map - (function - f when f#node_type = Pxp_document.T_element "CofixFunction" -> - let name = string_of_xml_attr (f#attribute "name") - and id = string_of_xml_attr (f#attribute "id") - and (ty, body) = - match f#sub_nodes with - [t ; b] when - t#node_type = Pxp_document.T_element "type" && - b#node_type = Pxp_document.T_element "body" -> - (t#extension#to_cic_term [], b#extension#to_cic_term []) - | _ -> raise (IllFormedXml 16) - in - (id, name, ty, body) - | _ -> raise (IllFormedXml 15) - ) sons - in - Cic.ACoFix (id, nofun, functions) - end -;; - -class eltype_implicit = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - assert (exp_named_subst = []) ; - let n = self#node in - let id = string_of_xml_attr (n#attribute "id") in - Cic.AImplicit (id, None) - end -;; - -class eltype_rel = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - assert (exp_named_subst = []) ; - let n = self#node in - let value = int_of_xml_attr (n#attribute "value") - and binder = binder_of_xml_attr (n#attribute "binder") - and id = string_of_xml_attr (n#attribute "id") - and idref = string_of_xml_attr (n#attribute "idref") in - Cic.ARel (id,idref,value,binder) - end -;; - -class eltype_meta = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - assert (exp_named_subst = []) ; - let n = self#node in - let value = int_of_xml_attr (n#attribute "no") - and id = string_of_xml_attr (n#attribute "id") - in - let local_context = - let sons = n#sub_nodes in - List.map - (function substitution -> - match substitution#sub_nodes with - [] -> None - | [he] -> Some (he#extension#to_cic_term []) - | _ -> raise (IllFormedXml 20) - ) sons - in - Cic.AMeta (id,value,local_context) - end -;; - -class eltype_var = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - assert (exp_named_subst = []) ; - let n = self#node in - let uri = uri_of_xml_attr (n#attribute "uri") - and xid = string_of_xml_attr (n#attribute "id") in -(*CSC: BIG BUG: [] MUST BE REPLACED WITH THE PARSED EXPLICIT NAMED SUBSTITUTION *) - Cic.AVar (xid,uri,[]) - end -;; - -class eltype_apply = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - assert (exp_named_subst = []) ; - let n = self#node in - let children = n#sub_nodes - and id = string_of_xml_attr (n#attribute "id") in - if List.length children < 2 then raise (IllFormedXml 8) - else - Cic.AAppl - (id,List.map (fun x -> x#extension#to_cic_term []) children) - end -;; - -class eltype_cast = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - assert (exp_named_subst = []) ; - let n = self#node in - let sons = n#sub_nodes - and id = string_of_xml_attr (n#attribute "id") in - match sons with - [te ; ty] when - te#node_type = Pxp_document.T_element "term" && - ty#node_type = Pxp_document.T_element "type" -> - let term = te#extension#to_cic_term [] - and typ = ty#extension#to_cic_term [] in - Cic.ACast (id,term,typ) - | _ -> raise (IllFormedXml 9) - end -;; - -class eltype_sort = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - assert (exp_named_subst = []) ; - let n = self#node in - let sort = cic_sort_of_xml_attr (n#attribute "value") - and id = string_of_xml_attr (n#attribute "id") in - Cic.ASort (id,sort) - end -;; - -class eltype_const = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - let module U = UriManager in - let n = self#node in - let value = uri_of_xml_attr (n#attribute "uri") - and id = string_of_xml_attr (n#attribute "id") in - Cic.AConst (id,value, exp_named_subst) - end -;; - -class eltype_mutind = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - let module U = UriManager in - let n = self#node in - let name = uri_of_xml_attr (n#attribute "uri") - and noType = int_of_xml_attr (n#attribute "noType") - and id = string_of_xml_attr (n#attribute "id") in - Cic.AMutInd - (id,name, noType, exp_named_subst) - end -;; - -class eltype_mutconstruct = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - let module U = UriManager in - let n = self#node in - let name = uri_of_xml_attr (n#attribute "uri") - and noType = int_of_xml_attr (n#attribute "noType") - and noConstr = int_of_xml_attr (n#attribute "noConstr") - and id = string_of_xml_attr (n#attribute "id") in - Cic.AMutConstruct - (id, name, noType, noConstr, exp_named_subst) - end -;; - -class eltype_prod = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - assert (exp_named_subst = []) ; - let n = self#node in - let sons = n#sub_nodes in - let rec get_decls_and_target = - function - [t] when t#node_type = Pxp_document.T_element "target" -> - [],t#extension#to_cic_term [] - | s::tl when s#node_type = Pxp_document.T_element "decl" -> - let decls,target = get_decls_and_target tl in - let id = string_of_xml_attr (s#attribute "id") in - let binder = cic_attr_of_xml_attr (s#attribute "binder") in - (id,binder,s#extension#to_cic_term [])::decls, target - | _ -> raise (IllFormedXml 10) - in - let decls,target = get_decls_and_target sons in - List.fold_right - (fun (id,b,s) t -> Cic.AProd (id,b,s,t)) - decls target - end -;; - -class eltype_mutcase = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - assert (exp_named_subst = []) ; - let module U = UriManager in - let n = self#node in - let sons = n#sub_nodes - and id = string_of_xml_attr (n#attribute "id") in - match sons with - ty::te::patterns when - ty#node_type = Pxp_document.T_element "patternsType" && - te#node_type = Pxp_document.T_element "inductiveTerm" -> - let ci = uri_of_xml_attr (n#attribute "uriType") - and typeno = int_of_xml_attr (n#attribute "noType") - and inductiveType = ty#extension#to_cic_term [] - and inductiveTerm = te#extension#to_cic_term [] - and lpattern = - List.map (fun x -> x#extension#to_cic_term []) patterns - in - Cic.AMutCase (id,ci, typeno,inductiveType,inductiveTerm,lpattern) - | _ -> raise (IllFormedXml 11) - end -;; - -class eltype_lambda = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - assert (exp_named_subst = []) ; - let n = self#node in - let sons = n#sub_nodes in - let rec get_decls_and_target = - function - [t] when t#node_type = Pxp_document.T_element "target" -> - [],t#extension#to_cic_term [] - | s::tl when s#node_type = Pxp_document.T_element "decl" -> - let decls,target = get_decls_and_target tl in - let id = string_of_xml_attr (s#attribute "id") in - let binder = cic_attr_of_xml_attr (s#attribute "binder") in - (id,binder,s#extension#to_cic_term [])::decls, target - | _ -> raise (IllFormedXml 12) - in - let decls,target = get_decls_and_target sons in - List.fold_right - (fun (id,b,s) t -> Cic.ALambda (id,b,s,t)) - decls target - end -;; - -class eltype_letin = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - assert (exp_named_subst = []) ; - let n = self#node in - let sons = n#sub_nodes in - let rec get_defs_and_target = - function - [t] when t#node_type = Pxp_document.T_element "target" -> - [],t#extension#to_cic_term [] - | s::tl when s#node_type = Pxp_document.T_element "def" -> - let defs,target = get_defs_and_target tl in - let id = string_of_xml_attr (s#attribute "id") in - let binder = cic_attr_of_xml_attr (s#attribute "binder") in - (id,binder,s#extension#to_cic_term [])::defs, target - | _ -> raise (IllFormedXml 12) - in - let defs,target = get_defs_and_target sons in - List.fold_right - (fun (id,b,s) t -> Cic.ALetIn (id,b,s,t)) - defs target - end -;; - -class eltype_instantiate = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - assert (exp_named_subst = []) ; - let n = self#node in -(* CSC: this optional attribute should be parsed and reflected in Cic.annterm - and id = string_of_xml_attr (n#attribute "id") -*) - match n#sub_nodes with - t::l -> - let baseUri = - UriManager.buri_of_uri (uri_of_xml_attr (t#attribute "uri")) in - let exp_named_subst = - List.map - (function - n when n#node_type = Pxp_document.T_element "arg" -> - let relUri = string_of_xml_attr (n#attribute "relUri") in - let uri = UriManager.uri_of_string (baseUri ^ "/" ^ relUri) in - let arg = - match n#sub_nodes with - [ t ] -> t#extension#to_cic_term [] - | _ -> raise (IllFormedXml 7) - in - (uri, arg) - | _ -> raise (IllFormedXml 7) - ) l - in - t#extension#to_cic_term exp_named_subst - | _ -> raise (IllFormedXml 7) - end -;; - - -(* The definition of domspec, an hashtable that maps each node type to the *) -(* object that must be linked to it. Used by markup. *) - -let domspec = - let module D = Pxp_document in - D.make_spec_from_alist - ~data_exemplar: (new D.data_impl (new eltype_not_of_cic)) - ~default_element_exemplar: (new D.element_impl (new eltype_not_of_cic)) - ~element_alist: - [ "REL", (new D.element_impl (new eltype_rel)) ; - "VAR", (new D.element_impl (new eltype_var)) ; - "META", (new D.element_impl (new eltype_meta)) ; - "SORT", (new D.element_impl (new eltype_sort)) ; - "IMPLICIT", (new D.element_impl (new eltype_implicit)) ; - "CAST", (new D.element_impl (new eltype_cast)) ; - "PROD", (new D.element_impl (new eltype_prod)) ; - "LAMBDA", (new D.element_impl (new eltype_lambda)) ; - "LETIN", (new D.element_impl (new eltype_letin)) ; - "APPLY", (new D.element_impl (new eltype_apply)) ; - "CONST", (new D.element_impl (new eltype_const)) ; - "MUTIND", (new D.element_impl (new eltype_mutind)) ; - "MUTCONSTRUCT", (new D.element_impl (new eltype_mutconstruct)) ; - "MUTCASE", (new D.element_impl (new eltype_mutcase)) ; - "FIX", (new D.element_impl (new eltype_fix)) ; - "COFIX", (new D.element_impl (new eltype_cofix)) ; - "instantiate", (new D.element_impl (new eltype_instantiate)) ; - "arity", (new D.element_impl (new eltype_transparent)) ; - "term", (new D.element_impl (new eltype_transparent)) ; - "type", (new D.element_impl (new eltype_transparent)) ; - "body", (new D.element_impl (new eltype_transparent)) ; - "decl", (new D.element_impl (new eltype_transparent)) ; - "def", (new D.element_impl (new eltype_transparent)) ; - "target", (new D.element_impl (new eltype_transparent)) ; - "letintarget", (new D.element_impl (new eltype_transparent)) ; - "patternsType", (new D.element_impl (new eltype_transparent)) ; - "inductiveTerm", (new D.element_impl (new eltype_transparent)) ; - "pattern", (new D.element_impl (new eltype_transparent)) - ] - () -;; diff --git a/helm/ocaml/cic/cicParser3.mli b/helm/ocaml/cic/cicParser3.mli deleted file mode 100644 index b9b8b6d11..000000000 --- a/helm/ocaml/cic/cicParser3.mli +++ /dev/null @@ -1,67 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 24/01/2000 *) -(* *) -(* This module is the terms level of a parser for cic objects from xml *) -(* files to the internal representation. It is used by the module cicParser2 *) -(* (objects level). It defines an extension of the standard dom using the *) -(* object-oriented extension machinery of markup: an object with a method *) -(* to_cic_term that returns the internal representation of the subtree is *) -(* added to each node of the dom tree *) -(* *) -(******************************************************************************) - -exception IllFormedXml of int - -(* the "interface" of the class linked to each node of the dom tree *) -class virtual cic_term : - object ('a) - - (* fields and methods ever required by markup *) - val mutable node : cic_term Pxp_document.node option - method clone : 'a - method node : cic_term Pxp_document.node - method set_node : cic_term Pxp_document.node -> unit - - (* a method that returns the internal representation of the tree (term) *) - (* rooted in this node *) - method virtual to_cic_term : - (UriManager.uri * Cic.annterm) list -> Cic.annterm - - end - -(* The definition of domspec, an hashtable that maps each node type to the *) -(* object that must be linked to it. Used by markup. *) -val domspec : cic_term Pxp_document.spec - -(** orrible hack *) -val set_uri: UriManager.uri -> unit - diff --git a/helm/ocaml/cic/cicPushParser.ml b/helm/ocaml/cic/cicPushParser.ml deleted file mode 100644 index 2c4ded396..000000000 --- a/helm/ocaml/cic/cicPushParser.ml +++ /dev/null @@ -1,723 +0,0 @@ -(* Copyright (C) 2004-2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -let debug_print = prerr_endline - -open Printf - -(* ZACK TODO element from the DTD still to be handled: - - - - - - - -*) - -module CicParser = -struct - -exception Getter_failure of string * string -exception Parser_failure of string - -type stack_entry = - | Arg of string * Cic.annterm (* relative uri, term *) - (* constants' body and types resides in differne files, thus we can't simple - * keep constants in Cic_obj stack entries *) - | Cic_attributes of Cic.attribute list - | Cic_constant_body of string * string * UriManager.uri list * Cic.annterm - * Cic.attribute list - (* id, for, params, body, object attributes *) - | Cic_constant_type of string * string * UriManager.uri list * Cic.annterm - * Cic.attribute list - (* id, name, params, type, object attributes *) - | Cic_term of Cic.annterm (* term *) - | Cic_obj of Cic.annobj (* object *) - | Cofix_fun of Cic.id * string * Cic.annterm * Cic.annterm - (* id, name, type, body *) - | Constructor of string * Cic.annterm (* name, type *) - | Decl of Cic.id * Cic.name * Cic.annterm (* id, binder, source *) - | Def of Cic.id * Cic.name * Cic.annterm (* id, binder, source *) - | Fix_fun of Cic.id * string * int * Cic.annterm * Cic.annterm - (* id, name, ind. index, type, body *) - | Inductive_type of string * string * bool * Cic.annterm * - (string * Cic.annterm) list (* id, name, inductive, arity, constructors *) - | Meta_subst of Cic.annterm option - | Obj_class of Cic.object_class - | Obj_field of string (* field name *) - | Obj_generated - | Tag of string * (string * string) list (* tag name, attributes *) - (* ZACK TODO add file position to tag stack entry so that when attribute - * errors occur, the position of their _start_tag_ could be printed - * instead of the current position (usually the end tag) *) - -type ctxt = { - mutable stack: stack_entry list; - mutable xml_parser: XmlPushParser.xml_parser option; - mutable filename: string; - uri: UriManager.uri; -} - -let string_of_stack ctxt = - "[" ^ (String.concat "; " - (List.map - (function - | Arg (reluri, _) -> sprintf "Arg %s" reluri - | Cic_attributes _ -> "Cic_attributes" - | Cic_constant_body (id, name, _, _, _) -> - sprintf "Cic_constant_body %s (id=%s)" name id - | Cic_constant_type (id, name, _, _, _) -> - sprintf "Cic_constant_type %s (id=%s)" name id - | Cic_term _ -> "Cic_term" - | Cic_obj _ -> "Cic_obj" - | Constructor (name, _) -> "Constructor " ^ name - | Cofix_fun (id, _, _, _) -> sprintf "Cofix_fun (id=%s)" id - | Decl (id, _, _) -> sprintf "Decl (id=%s)" id - | Def (id, _, _) -> sprintf "Def (id=%s)" id - | Fix_fun (id, _, _, _, _) -> sprintf "Fix_fun (id=%s)" id - | Inductive_type (id, name, _, _, _) -> - sprintf "Inductive_type %s (id=%s)" name id - | Meta_subst _ -> "Meta_subst" - | Obj_class _ -> "Obj_class" - | Obj_field name -> "Obj_field " ^ name - | Obj_generated -> "Obj_generated" - | Tag (tag, _) -> "Tag " ^ tag) - ctxt.stack)) ^ "]" - -let compare_attrs (a1, v1) (a2, v2) = Pervasives.compare a1 a2 -let sort_attrs = List.sort compare_attrs - -let new_parser_context uri = { - stack = []; - xml_parser = None; - filename = "-"; - uri = uri; -} - -let get_parser ctxt = - match ctxt.xml_parser with - | Some p -> p - | None -> assert false - -(** {2 Error handling} *) - -let parse_error ctxt msg = - let (line, col) = XmlPushParser.get_position (get_parser ctxt) in - raise (Parser_failure (sprintf "[%s: line %d, column %d] %s" - ctxt.filename line col msg)) - -let attribute_error ctxt tag = - parse_error ctxt ("wrong attribute set for " ^ tag) - -(** {2 Parsing context management} *) - -let pop ctxt = -(* debug_print "pop";*) - match ctxt.stack with - | hd :: tl -> (ctxt.stack <- tl) - | _ -> assert false - -let push ctxt v = -(* debug_print "push";*) - ctxt.stack <- v :: ctxt.stack - -let set_top ctxt v = -(* debug_print "set_top";*) - match ctxt.stack with - | _ :: tl -> (ctxt.stack <- v :: tl) - | _ -> assert false - - (** pop the last tag from the open tags stack returning a pair *) -let pop_tag ctxt = - match ctxt.stack with - | Tag (tag, attrs) :: tl -> - ctxt.stack <- tl; - (tag, attrs) - | _ -> parse_error ctxt "unexpected extra content" - - (** pop the last tag from the open tags stack returning its attributes. - * Attributes are returned as a list of pair _sorted_ by - * attribute name *) -let pop_tag_attrs ctxt = sort_attrs (snd (pop_tag ctxt)) - -let pop_cics ctxt = - let rec aux acc stack = - match stack with - | Cic_term t :: tl -> aux (t :: acc) tl - | tl -> acc, tl - in - let values, new_stack = aux [] ctxt.stack in - ctxt.stack <- new_stack; - values - -let pop_class_modifiers ctxt = - let rec aux acc stack = - match stack with - | (Cic_term (Cic.ASort _) as m) :: tl - | (Obj_field _ as m) :: tl -> - aux (m :: acc) tl - | tl -> acc, tl - in - let values, new_stack = aux [] ctxt.stack in - ctxt.stack <- new_stack; - values - -let pop_meta_substs ctxt = - let rec aux acc stack = - match stack with - | Meta_subst t :: tl -> aux (t :: acc) tl - | tl -> acc, tl - in - let values, new_stack = aux [] ctxt.stack in - ctxt.stack <- new_stack; - values - -let pop_fix_funs ctxt = - let rec aux acc stack = - match stack with - | Fix_fun (id, name, index, typ, body) :: tl -> - aux ((id, name, index, typ, body) :: acc) tl - | tl -> acc, tl - in - let values, new_stack = aux [] ctxt.stack in - ctxt.stack <- new_stack; - values - -let pop_cofix_funs ctxt = - let rec aux acc stack = - match stack with - | Cofix_fun (id, name, typ, body) :: tl -> - aux ((id, name, typ, body) :: acc) tl - | tl -> acc, tl - in - let values, new_stack = aux [] ctxt.stack in - ctxt.stack <- new_stack; - values - -let pop_constructors ctxt = - let rec aux acc stack = - match stack with - | Constructor (name, t) :: tl -> aux ((name, t) :: acc) tl - | tl -> acc, tl - in - let values, new_stack = aux [] ctxt.stack in - ctxt.stack <- new_stack; - values - -let pop_inductive_types ctxt = - let rec aux acc stack = - match stack with - | Inductive_type (id, name, ind, arity, ctors) :: tl -> - aux ((id, name, ind, arity, ctors) :: acc) tl - | tl -> acc, tl - in - let values, new_stack = aux [] ctxt.stack in - if values = [] then - parse_error ctxt "no \"InductiveType\" element found"; - ctxt.stack <- new_stack; - values - - (** travels the stack (without popping) for the first term subject of explicit - * named substitution and return its URI *) -let find_base_uri ctxt = - let rec aux = function - | Cic_term (Cic.AConst (_, uri, _)) :: _ - | Cic_term (Cic.AMutInd (_, uri, _, _)) :: _ - | Cic_term (Cic.AMutConstruct (_, uri, _, _, _)) :: _ - | Cic_term (Cic.AVar (_, uri, _)) :: _ -> - uri - | Arg _ :: tl -> aux tl - | _ -> parse_error ctxt "no \"arg\" element found" - in - UriManager.buri_of_uri (aux ctxt.stack) - - (** backwardly eats the stack building an explicit named substitution from Arg - * stack entries *) -let pop_subst ctxt base_uri = - let rec aux acc stack = - match stack with - | Arg (rel_uri, term) :: tl -> - let uri = UriManager.uri_of_string (base_uri ^ "/" ^ rel_uri) in - aux ((uri, term) :: acc) tl - | tl -> acc, tl - in - let subst, new_stack = aux [] ctxt.stack in - if subst = [] then - parse_error ctxt "no \"arg\" element found"; - ctxt.stack <- new_stack; - subst - -let pop_cic ctxt = - match ctxt.stack with - | Cic_term t :: tl -> - ctxt.stack <- tl; - t - | _ -> parse_error ctxt "no cic term found" - -let pop_obj_attributes ctxt = - match ctxt.stack with - | Cic_attributes attributes :: tl -> - ctxt.stack <- tl; - attributes - | _ -> [] - -(** {2 Auxiliary functions} *) - -let uri_of_string = UriManager.uri_of_string - -let uri_list_of_string = - let space_RE = Str.regexp " " in - fun s -> - List.map uri_of_string (Str.split space_RE s) - -let sort_of_string ctxt = function - | "Prop" -> Cic.Prop - | "Set" -> Cic.Set - | "Type" -> Cic.Type (CicUniv.fresh ~uri:ctxt.uri ()) -(* | "Type" -> CicUniv.restart_numbering (); |+ useful only to test parser +| *) - | "CProp" -> Cic.CProp - | _ -> parse_error ctxt "sort expected" - -let patch_subst ctxt subst = function - | Cic.AConst (id, uri, _) -> Cic.AConst (id, uri, subst) - | Cic.AMutInd (id, uri, typeno, _) -> - Cic.AMutInd (id, uri, typeno, subst) - | Cic.AMutConstruct (id, uri, typeno, consno, _) -> - Cic.AMutConstruct (id, uri, typeno, consno, subst) - | Cic.AVar (id, uri, _) -> Cic.AVar (id, uri, subst) - | _ -> - parse_error ctxt - ("only \"CONST\", \"VAR\", \"MUTIND\", and \"MUTCONSTRUCT\" can be" ^ - " instantiated") - - (** backwardly eats the stack seeking for the first open tag carrying - * "helm:exception" attributes. If found return Some of a pair containing - * exception name and argument. Return None otherwise *) -let find_helm_exception ctxt = - let rec aux = function - | [] -> None - | Tag (_, attrs) :: tl -> - (try - let exn = List.assoc "helm:exception" attrs in - let arg = - try List.assoc "helm:exception_arg" attrs with Not_found -> "" - in - Some (exn, arg) - with Not_found -> aux tl) - | _ :: tl -> aux tl - in - aux ctxt.stack - -(** {2 Push parser callbacks} - * each callback needs to be instantiated to a parsing context *) - -let start_element ctxt tag attrs = -(* debug_print (sprintf "<%s%s>" tag (match attrs with | [] -> "" | _ -> " " ^ String.concat " " (List.map (fun (a,v) -> sprintf "%s=\"%s\"" a v) attrs)));*) - push ctxt (Tag (tag, attrs)) - -let end_element ctxt tag = -(* debug_print (sprintf "" tag);*) -(* debug_print (string_of_stack ctxt);*) - let attribute_error () = attribute_error ctxt tag in - let parse_error = parse_error ctxt in - let sort_of_string = sort_of_string ctxt in - match tag with - | "REL" -> - push ctxt (Cic_term - (match pop_tag_attrs ctxt with - | ["binder", binder; "id", id; "idref", idref; "sort", _; - "value", value] -> - Cic.ARel (id, idref, int_of_string value, binder) - | _ -> attribute_error ())) - | "VAR" -> - push ctxt (Cic_term - (match pop_tag_attrs ctxt with - | ["id", id; "sort", _; "uri", uri] -> - Cic.AVar (id, uri_of_string uri, []) - | _ -> attribute_error ())) - | "CONST" -> - push ctxt (Cic_term - (match pop_tag_attrs ctxt with - | ["id", id; "sort", _; "uri", uri] -> - Cic.AConst (id, uri_of_string uri, []) - | _ -> attribute_error ())) - | "SORT" -> - push ctxt (Cic_term - (match pop_tag_attrs ctxt with - | ["id", id; "value", sort] -> Cic.ASort (id, sort_of_string sort) - | _ -> attribute_error ())) - | "APPLY" -> - let args = pop_cics ctxt in - push ctxt (Cic_term - (match pop_tag_attrs ctxt with - | ["id", id; "sort", _] -> Cic.AAppl (id, args) - | _ -> attribute_error ())) - | "decl" -> - let source = pop_cic ctxt in - push ctxt - (match pop_tag_attrs ctxt with - | ["binder", binder; "id", id; "type", _] -> - Decl (id, Cic.Name binder, source) - | ["id", id; "type", _] -> Decl (id, Cic.Anonymous, source) - | _ -> attribute_error ()) - | "def" -> (* same as "decl" above *) - let source = pop_cic ctxt in - push ctxt - (match pop_tag_attrs ctxt with - | ["binder", binder; "id", id; "sort", _] -> - Def (id, Cic.Name binder, source) - | ["id", id; "sort", _] -> Def (id, Cic.Anonymous, source) - | _ -> attribute_error ()) - | "arity" (* transparent elements (i.e. which contain a CIC) *) - | "body" - | "inductiveTerm" - | "pattern" - | "patternsType" - | "target" - | "term" - | "type" -> - let term = pop_cic ctxt in - pop ctxt; (* pops start tag matching current end tag (e.g. ) *) - push ctxt (Cic_term term) - | "substitution" -> (* optional transparent elements (i.e. which _may_ - * contain a CIC) *) - set_top ctxt (* replace *) - (match ctxt.stack with - | Cic_term term :: tl -> - ctxt.stack <- tl; - (Meta_subst (Some term)) - | _ -> Meta_subst None) - | "PROD" -> - let target = pop_cic ctxt in - let rec add_decl target = function - | Decl (id, binder, source) :: tl -> - add_decl (Cic.AProd (id, binder, source, target)) tl - | tl -> - ctxt.stack <- tl; - target - in - let term = add_decl target ctxt.stack in - (match pop_tag_attrs ctxt with - | ["type", _] -> () - | _ -> attribute_error ()); - push ctxt (Cic_term term) - | "LAMBDA" -> - let target = pop_cic ctxt in - let rec add_decl target = function - | Decl (id, binder, source) :: tl -> - add_decl (Cic.ALambda (id, binder, source, target)) tl - | tl -> - ctxt.stack <- tl; - target - in - let term = add_decl target ctxt.stack in - (match pop_tag_attrs ctxt with - | ["sort", _] -> () - | _ -> attribute_error ()); - push ctxt (Cic_term term) - | "LETIN" -> - let target = pop_cic ctxt in - let rec add_def target = function - | Def (id, binder, source) :: tl -> - add_def (Cic.ALetIn (id, binder, source, target)) tl - | tl -> - ctxt.stack <- tl; - target - in - let term = add_def target ctxt.stack in - (match pop_tag_attrs ctxt with - | ["sort", _] -> () - | _ -> attribute_error ()); - push ctxt (Cic_term term) - | "CAST" -> - let typ = pop_cic ctxt in - let term = pop_cic ctxt in - push ctxt (Cic_term - (match pop_tag_attrs ctxt with - | ["id", id; "sort", _] -> Cic.ACast (id, term, typ) - | _ -> attribute_error ())); - | "IMPLICIT" -> - push ctxt (Cic_term - (match pop_tag_attrs ctxt with - | ["id", id] -> Cic.AImplicit (id, None) - | ["annotation", annotation; "id", id] -> - let implicit_annotation = - match annotation with - | "closed" -> `Closed - | "hole" -> `Hole - | "type" -> `Type - | _ -> parse_error "invalid value for \"annotation\" attribute" - in - Cic.AImplicit (id, Some implicit_annotation) - | _ -> attribute_error ())) - | "META" -> - let meta_substs = pop_meta_substs ctxt in - push ctxt (Cic_term - (match pop_tag_attrs ctxt with - | ["id", id; "no", no; "sort", _] -> - Cic.AMeta (id, int_of_string no, meta_substs) - | _ -> attribute_error ())); - | "MUTIND" -> - push ctxt (Cic_term - (match pop_tag_attrs ctxt with - | ["id", id; "noType", noType; "uri", uri] -> - Cic.AMutInd (id, uri_of_string uri, int_of_string noType, []) - | _ -> attribute_error ())); - | "MUTCONSTRUCT" -> - push ctxt (Cic_term - (match pop_tag_attrs ctxt with - | ["id", id; "noConstr", noConstr; "noType", noType; "sort", _; - "uri", uri] -> - Cic.AMutConstruct (id, uri_of_string uri, int_of_string noType, - int_of_string noConstr, []) - | _ -> attribute_error ())); - | "FixFunction" -> - let body = pop_cic ctxt in - let typ = pop_cic ctxt in - push ctxt - (match pop_tag_attrs ctxt with - | ["id", id; "name", name; "recIndex", recIndex] -> - Fix_fun (id, name, int_of_string recIndex, typ, body) - | _ -> attribute_error ()) - | "CofixFunction" -> - let body = pop_cic ctxt in - let typ = pop_cic ctxt in - push ctxt - (match pop_tag_attrs ctxt with - | ["id", id; "name", name] -> - Cofix_fun (id, name, typ, body) - | _ -> attribute_error ()) - | "FIX" -> - let fix_funs = pop_fix_funs ctxt in - push ctxt (Cic_term - (match pop_tag_attrs ctxt with - | ["id", id; "noFun", noFun; "sort", _] -> - Cic.AFix (id, int_of_string noFun, fix_funs) - | _ -> attribute_error ())) - | "COFIX" -> - let cofix_funs = pop_cofix_funs ctxt in - push ctxt (Cic_term - (match pop_tag_attrs ctxt with - | ["id", id; "noFun", noFun; "sort", _] -> - Cic.ACoFix (id, int_of_string noFun, cofix_funs) - | _ -> attribute_error ())) - | "MUTCASE" -> - (match pop_cics ctxt with - | patternsType :: inductiveTerm :: patterns -> - push ctxt (Cic_term - (match pop_tag_attrs ctxt with - | ["id", id; "noType", noType; "sort", _; "uriType", uriType] -> - Cic.AMutCase (id, uri_of_string uriType, int_of_string noType, - patternsType, inductiveTerm, patterns) - | _ -> attribute_error ())) - | _ -> parse_error "invalid \"MUTCASE\" content") - | "Constructor" -> - let typ = pop_cic ctxt in - push ctxt - (match pop_tag_attrs ctxt with - | ["name", name] -> Constructor (name, typ) - | _ -> attribute_error ()) - | "InductiveType" -> - let constructors = pop_constructors ctxt in - let arity = pop_cic ctxt in - push ctxt - (match pop_tag_attrs ctxt with - | ["id", id; "inductive", inductive; "name", name] -> - Inductive_type (id, name, bool_of_string inductive, arity, - constructors) - | _ -> attribute_error ()) - | "InductiveDefinition" -> - let inductive_types = pop_inductive_types ctxt in - let obj_attributes = pop_obj_attributes ctxt in - push ctxt (Cic_obj - (match pop_tag_attrs ctxt with - | ["id", id; "noParams", noParams; "params", params] -> - Cic.AInductiveDefinition (id, inductive_types, - uri_list_of_string params, int_of_string noParams, obj_attributes) - | _ -> attribute_error ())) - | "ConstantType" -> - let typ = pop_cic ctxt in - let obj_attributes = pop_obj_attributes ctxt in - push ctxt - (match pop_tag_attrs ctxt with - | ["id", id; "name", name; "params", params] -> - Cic_constant_type (id, name, uri_list_of_string params, typ, - obj_attributes) - | _ -> attribute_error ()) - | "ConstantBody" -> - let body = pop_cic ctxt in - let obj_attributes = pop_obj_attributes ctxt in - push ctxt - (match pop_tag_attrs ctxt with - | ["for", for_; "id", id; "params", params] -> - Cic_constant_body (id, for_, uri_list_of_string params, body, - obj_attributes) - | _ -> attribute_error ()) - | "Variable" -> - let typ = pop_cic ctxt in - let body = - match pop_cics ctxt with - | [] -> None - | [t] -> Some t - | _ -> parse_error "wrong content for \"Variable\"" - in - let obj_attributes = pop_obj_attributes ctxt in - push ctxt (Cic_obj - (match pop_tag_attrs ctxt with - | ["id", id; "name", name; "params", params] -> - Cic.AVariable (id, name, body, typ, uri_list_of_string params, - obj_attributes) - | _ -> attribute_error ())) - | "arg" -> - let term = pop_cic ctxt in - push ctxt - (match pop_tag_attrs ctxt with - | ["relUri", relUri] -> Arg (relUri, term) - | _ -> attribute_error ()) - | "instantiate" -> - (* explicit named substitution handling: when the end tag of an element - * subject of exlicit named subst (MUTIND, MUTCONSTRUCT, CONST, VAR) it - * is stored on the stack with no substitutions (i.e. []). When the end - * tag of an "instantiate" element is found we patch the term currently - * on the stack with the substitution built from "instantiate" children - *) - (* XXX inefficiency here: first travels the elements in order to - * find the baseUri, then in order to build the explicit named subst *) - let base_uri = find_base_uri ctxt in - let subst = pop_subst ctxt base_uri in - let term = pop_cic ctxt in - (* comment from CicParser3.ml: - * CSC: the "id" optional attribute should be parsed and reflected in - * Cic.annterm and id = string_of_xml_attr (n#attribute "id") *) - (* replace *) - set_top ctxt (Cic_term (patch_subst ctxt subst term)) - | "attributes" -> - let rec aux acc = function (* retrieve object attributes *) - | Obj_class c :: tl -> aux (`Class c :: acc) tl - | Obj_generated :: tl -> aux (`Generated :: acc) tl - | tl -> acc, tl - in - let obj_attrs, new_stack = aux [] ctxt.stack in - ctxt.stack <- new_stack; - set_top ctxt (Cic_attributes obj_attrs) - | "generated" -> set_top ctxt Obj_generated - | "field" -> - push ctxt - (match pop_tag_attrs ctxt with - | ["name", name] -> Obj_field name - | _ -> attribute_error ()) - | "class" -> - let class_modifiers = pop_class_modifiers ctxt in - push ctxt - (match pop_tag_attrs ctxt with - | ["value", "coercion"] -> Obj_class `Coercion - | ["value", "elim"] -> - (match class_modifiers with - | [Cic_term (Cic.ASort (_, sort))] -> Obj_class (`Elim sort) - | _ -> - parse_error - "unexpected extra content for \"elim\" object class") - | ["value", "record"] -> - let fields = - List.map - (function - | Obj_field name -> name - | _ -> - parse_error - "unexpected extra content for \"record\" object class") - class_modifiers - in - Obj_class (`Record fields) - | ["value", "projection"] -> Obj_class `Projection - | _ -> attribute_error ()) - | tag -> - match find_helm_exception ctxt with - | Some (exn, arg) -> raise (Getter_failure (exn, arg)) - | None -> parse_error (sprintf "unknown element \"%s\"" tag) - -(** {2 Parser internals} *) - -let parse uri filename = - let ctxt = new_parser_context uri in - ctxt.filename <- filename; - let module P = XmlPushParser in - let callbacks = { - P.default_callbacks with - P.start_element = Some (start_element ctxt); - P.end_element = Some (end_element ctxt); - } in - let xml_parser = P.create_parser callbacks in - ctxt.xml_parser <- Some xml_parser; - try - (try - P.parse xml_parser (`Gzip_file filename); - with exn -> - ctxt.xml_parser <- None; - (* ZACK: the above "<- None" is vital for garbage collection. Without it - * we keep in memory a circular structure parser -> callbacks -> ctxt -> - * parser. I don't know if the ocaml garbage collector is supposed to - * collect such structures, but for sure the expat bindings will (orribly) - * leak when used in conjunction with such structures *) - raise exn); - ctxt.xml_parser <- None; (* ZACK: same comment as above *) -(* debug_print (string_of_stack stack);*) - (* assert (List.length ctxt.stack = 1) *) - List.hd ctxt.stack - with - | Failure "int_of_string" -> parse_error ctxt "integer number expected" - | Invalid_argument "bool_of_string" -> parse_error ctxt "boolean expected" - | P.Parse_error msg -> parse_error ctxt ("parse error: " ^ msg) - | Parser_failure _ - | Getter_failure _ as exn -> - raise exn - | exn -> - raise (Parser_failure ("uncaught exception: " ^ Printexc.to_string exn)) - -(** {2 API implementation} *) - -let annobj_of_xml uri filename filenamebody = - match filenamebody with - | None -> - (match parse uri filename with - | Cic_constant_type (id, name, params, typ, obj_attributes) -> - Cic.AConstant (id, None, name, None, typ, params, obj_attributes) - | Cic_obj obj -> obj - | _ -> raise (Parser_failure ("no object found in " ^ filename))) - | Some filenamebody -> - (match parse uri filename, parse uri filenamebody with - | Cic_constant_type (type_id, name, params, typ, obj_attributes), - Cic_constant_body (body_id, _, _, body, _) -> - Cic.AConstant (type_id, Some body_id, name, Some body, typ, params,[]) - | _ -> - raise (Parser_failure (sprintf "no constant found in %s, %s" - filename filenamebody))) - -let obj_of_xml uri filename filenamebody = - Deannotate.deannotate_obj (annobj_of_xml uri filename filenamebody) - -end - diff --git a/helm/ocaml/cic/cicPushParser.mli b/helm/ocaml/cic/cicPushParser.mli deleted file mode 100644 index d08913321..000000000 --- a/helm/ocaml/cic/cicPushParser.mli +++ /dev/null @@ -1,48 +0,0 @@ -(* Copyright (C) 2004-2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -module CicParser: -sig - (** raised for exception received by the getter (i.e. embedded in the source - * XML document). Arguments are values of "helm:exception" and - * "helm:exception_arg" attributes *) - exception Getter_failure of string * string - - (** generic parser failure *) - exception Parser_failure of string - - (* given the filename of an xml file of a cic object, it returns its - * internal annotated representation. In the case of constants (whose type - * is splitted from the body), a second xml file (for the body) must be - * provided. *) - val annobj_of_xml: UriManager.uri -> string -> string option -> Cic.annobj - - (* given the filename of an xml file of a cic object, it returns its - * internal logical representation. In the case of constants (whose type is - * splitted from the body), a second xml file (for the body) must be - * provided. *) - val obj_of_xml : UriManager.uri -> string -> string option -> Cic.obj -end - diff --git a/helm/ocaml/cic/cicPxpParser.ml b/helm/ocaml/cic/cicPxpParser.ml deleted file mode 100644 index 8fdefc250..000000000 --- a/helm/ocaml/cic/cicPxpParser.ml +++ /dev/null @@ -1,103 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 24/01/2000 *) -(* *) -(* This is the main (top level) module of a parser for cic objects from xml *) -(* files to the internal representation. It uses the modules cicParser2 *) -(* (objects level) and cicParser3 (terms level) *) -(* *) -(******************************************************************************) - -module CicParser = -struct - -exception Getter_failure of string * string -exception Parser_failure of string - - (** tries to recover from a parse error caused by the parsing of a getter - * error message (e.g. Key_not_found exception). Unfortunately we have to - * re-parse xml document to extract exception data *) -let try_recover exn filename = - let rc = ref None in - (try - let entity_manager = - Pxp_ev_parser.create_entity_manager ~is_document:true - PxpHelmConf.pxp_config (Pxp_types.from_file filename) - in - let pull_parser = - Pxp_ev_parser.create_pull_parser PxpHelmConf.pxp_config - (`Entry_document []) entity_manager - in - let rec find_exn p = - match p () with - | None -> () - | Some (Pxp_types.E_start_tag ("html", attrs, _, _)) -> - let exn = List.assoc "helm:exception" attrs in - let arg = - try List.assoc "helm:exception_arg" attrs with Not_found -> "" - in - rc := Some (Getter_failure (exn, arg)) - | _ -> find_exn p - in - find_exn pull_parser - with _ -> raise (Parser_failure (Printexc.to_string exn))); - match !rc with - | None -> raise (Parser_failure (Printexc.to_string exn)) - | Some exn -> raise exn - -let parse_document filename = - try - Pxp_tree_parser.parse_document_entity PxpHelmConf.pxp_config - (Pxp_types.from_file ~alt:[PxpUrlResolver.url_resolver] filename) - CicParser3.domspec - with exn -> - raise (try_recover exn filename) - -(* given the filename of an xml file of a cic object it returns its internal *) -(* representation. *) -let annobj_of_xml uri filename filenamebody = - CicParser3.set_uri uri; - let root, rootbody = - let doc = parse_document filename in - let docroot = doc#root in - match filenamebody with - None -> docroot,None - | Some filename -> - let docbody = parse_document filename in - docroot,Some docbody#root - in - CicParser2.get_term root rootbody - -let obj_of_xml uri filename filenamebody = - Deannotate.deannotate_obj (annobj_of_xml uri filename filenamebody) - -end - diff --git a/helm/ocaml/cic/cicPxpParser.mli b/helm/ocaml/cic/cicPxpParser.mli deleted file mode 100644 index a1915ec47..000000000 --- a/helm/ocaml/cic/cicPxpParser.mli +++ /dev/null @@ -1,61 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 24/01/2000 *) -(* *) -(* This is the main (top level) module of a parser for cic objects from xml *) -(* files to the internal representation. It uses the modules cicParser2 *) -(* (objects level) and cicParser3 (terms level) *) -(* *) -(******************************************************************************) - -module CicParser: -sig - (** raised for exception received by the getter (i.e. embedded in the source - * XML document). Arguments are values of "helm:exception" and - * "helm:exception_arg" attributes *) - exception Getter_failure of string * string - - (** generic parser failure *) - exception Parser_failure of string - - (* given the filename of an xml file of a cic object, it returns its - * internal annotated representation. In the case of constants (whose type - * is splitted from the body), a second xml file (for the body) must be - * provided. *) - val annobj_of_xml: UriManager.uri -> string -> string option -> Cic.annobj - - (* given the filename of an xml file of a cic object, it returns its - * internal logical representation. In the case of constants (whose type is - * splitted from the body), a second xml file (for the body) must be - * provided. *) - val obj_of_xml : UriManager.uri -> string -> string option -> Cic.obj -end -