exception EmptyUri of string;;
-(* given an uri u it returns the list of tokens of the base uri of u *)
-(* e.g.: token_of_uri "cic:/a/b/c/d.xml" returns ["a" ; "b" ; "c"] *)
-let tokens_of_uri uri =
- let uri' = UriManager.string_of_uri uri in
- let rec chop_list =
- function
- [] -> raise (EmptyUri uri')
- | [fn] -> []
- | he::[fn] -> [he]
- | he::tl -> he::(chop_list tl)
- in
- let trimmed_uri = Str.replace_first (Str.regexp "cic:") "" uri' in
- let list_of_tokens = Str.split (Str.regexp "/") trimmed_uri in
- chop_list list_of_tokens
-;;
-
(* given the filename of an xml file of a cic object it returns its internal *)
(* representation. *)
-let annobj_of_xml filename filenamebody uri =
+let annobj_of_xml filename filenamebody =
let module Y = Pxp_yacc in
try
let root, rootbody =
- (* sets the current base uri to resolve relative URIs *)
- CicParser3.current_sp := tokens_of_uri uri ;
- CicParser3.current_uri := uri ;
- let config = {Y.default_config with Y.warner = new warner} in
- let doc =
- Y.parse_document_entity config
- (Y.from_file ~alt:[PxpUrlResolver.url_resolver] filename)
- CicParser3.domspec in
+ let config = {Y.default_config with Y.warner = new warner} in
+ let doc =
+ Y.parse_document_entity config
+ (Y.from_file ~alt:[PxpUrlResolver.url_resolver] filename)
+ CicParser3.domspec in
(* CSC: Until PXP bug is resolved *)
PxpUrlResolver.url_resolver#close_all ;
- let docroot = doc#root in
- match filenamebody with
- None -> docroot,None
- | Some filename ->
- let docbody =
- Y.parse_document_entity config
- (Y.from_file ~alt:[PxpUrlResolver.url_resolver] filename)
- CicParser3.domspec
- in
+ let docroot = doc#root in
+ match filenamebody with
+ None -> docroot,None
+ | Some filename ->
+ let docbody =
+ Y.parse_document_entity config
+ (Y.from_file ~alt:[PxpUrlResolver.url_resolver] filename)
+ CicParser3.domspec
+ in
(* CSC: Until PXP bug is resolved *)
PxpUrlResolver.url_resolver#close_all ;
- docroot,Some docbody#root
+ docroot,Some docbody#root
in
CicParser2.get_term root rootbody
with
raise e
;;
-let obj_of_xml filename filenamebody uri =
- Deannotate.deannotate_obj (annobj_of_xml filename filenamebody uri)
+let obj_of_xml filename filenamebody =
+ Deannotate.deannotate_obj (annobj_of_xml filename filenamebody)
;;
(* *)
(******************************************************************************)
-(* given the filename of an xml file of a cic object and it's uri, it returns *)
+(* 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 : string -> string option -> UriManager.uri -> Cic.annobj
+val annobj_of_xml : string -> string option -> Cic.annobj
-(* given the filename of an xml file of a cic object and it's uri, it returns *)
+(* 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 : string -> string option -> UriManager.uri -> Cic.obj
+val obj_of_xml : string -> string option -> Cic.obj
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 &&
- U.eq (U.uri_of_string for_) !CicParser3.current_uri
- then
+ if paramsbody = params then
C.AConstant (xid, Some xidbody, name, Some value, typ, params)
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 value = (get_content nbody')#extension#to_cic_term [] in
let sons = nbody'#sub_nodes in
let (conjs, value) = get_conjs_value sons in
- if U.eq (U.uri_of_string for_) !CicParser3.current_uri then
- C.ACurrentProof (xid, xidbody, name, conjs, value, typ, params)
- else
- raise (IllFormedXml 6)
+ C.ACurrentProof (xid, xidbody, name, conjs, value, typ, params)
| D.T_element _
| D.T_data
| _ -> raise (IllFormedXml 6)
exception IllFormedXml of int;;
-(* The list of tokens of the current section path. *)
-(* Used to resolve relative URIs *)
-let current_sp = ref [];;
-
-(* The uri of the object been parsed *)
-let current_uri = ref (UriManager.uri_of_string "cic:/.xml");;
-
(* Utility functions to map a markup attribute to something useful *)
let cic_attr_of_xml_attr =
exception IllFormedXml of int
-val current_sp : string list ref
-val current_uri : UriManager.uri ref
-
(* the "interface" of the class linked to each node of the dom tree *)
class virtual cic_term :
object ('a)
projects / helm.git / commitdiff