unshare.cmi: cic.cmo
deannotate.cmi: cic.cmo
-cicPushParser.cmi: cic.cmo
cicParser.cmi: cic.cmo
cicUtil.cmi: cic.cmo
helmLibraryObjects.cmi: cic.cmo
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
unshare.mli \
cicUniv.mli \
deannotate.mli \
- cicPushParser.mli \
cicParser.mli \
cicUtil.mli \
helmLibraryObjects.mli
-(* 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
* 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:
+ <!ELEMENT CurrentProof (Conjecture*,body)>
+ <!ELEMENT Sequent %sequent;>
+ <!ELEMENT Conjecture %sequent;>
+ <!ELEMENT Decl %term;>
+ <!ELEMENT Def %term;>
+ <!ELEMENT Hidden EMPTY>
+ <!ELEMENT Goal %term;>
+*)
+
+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 <tag_name,
+ * attribute_list> *)
+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 <name, value> _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 "</%s>" 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. <arity>) *)
+ push ctxt (Cic_term term)
+ | "substitution" -> (* optional transparent elements (i.e. which _may_
+ * contain a CIC) *)
+ set_top ctxt (* replace <substitution> *)
+ (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 <arg> 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 <instantiate> *)
+ 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)
+++ /dev/null
-(* 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 <sacerdot@@cs.unibo.it> *)
-(* 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)
-;;
+++ /dev/null
-(* 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 <sacerdot@cs.unibo.it> *)
-(* 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
+++ /dev/null
-(* 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 <sacerdot@cs.unibo.it> *)
-(* 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. <type> ... </type> *)
-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))
- ]
- ()
-;;
+++ /dev/null
-(* 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 <sacerdot@cs.unibo.it> *)
-(* 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
-
+++ /dev/null
-(* 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:
- <!ELEMENT CurrentProof (Conjecture*,body)>
- <!ELEMENT Sequent %sequent;>
- <!ELEMENT Conjecture %sequent;>
- <!ELEMENT Decl %term;>
- <!ELEMENT Def %term;>
- <!ELEMENT Hidden EMPTY>
- <!ELEMENT Goal %term;>
-*)
-
-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 <tag_name,
- * attribute_list> *)
-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 <name, value> _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 "</%s>" 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. <arity>) *)
- push ctxt (Cic_term term)
- | "substitution" -> (* optional transparent elements (i.e. which _may_
- * contain a CIC) *)
- set_top ctxt (* replace <substitution> *)
- (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 <arg> 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 <instantiate> *)
- 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
-
+++ /dev/null
-(* 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
-
+++ /dev/null
-(* 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 <sacerdot@cs.unibo.it> *)
-(* 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
-
+++ /dev/null
-(* 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 <sacerdot@cs.unibo.it> *)
-(* 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
-
projects / helm.git / commitdiff