X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicParser3.ml;h=8f87504acdc9239e5dd36d49947ad7738b3342a6;hb=8f89cdd08d9ee0a243cf84201bf42e5503759ee3;hp=ff356b13e0b58fe99515e4d5882c61faa2c70341;hpb=5a92117eeff70048d29e91ba24e113155d956e1b;p=helm.git diff --git a/helm/ocaml/cic/cicParser3.ml b/helm/ocaml/cic/cicParser3.ml index ff356b13e..8f87504ac 100644 --- a/helm/ocaml/cic/cicParser3.ml +++ b/helm/ocaml/cic/cicParser3.ml @@ -41,9 +41,6 @@ exception IllFormedXml of int;; -(* The hashtable from the current identifiers to the object or the terms *) -let ids_to_targets = ref None;; - (* The list of tokens of the current section path. *) (* Used to resolve relative URIs *) let current_sp = ref [];; @@ -51,9 +48,6 @@ let current_sp = ref [];; (* The uri of the object been parsed *) let current_uri = ref (UriManager.uri_of_string "cic:/.xml");; -(* True if annotation really matter *) -let process_annotations = ref false;; - (* Utility functions to map a markup attribute to something useful *) let cic_attr_of_xml_attr = @@ -86,18 +80,10 @@ let string_of_xml_attr = let binder_of_xml_attr = function - Pxp_types.Value s -> if !process_annotations then Some s else None + Pxp_types.Value s -> s | _ -> raise (IllFormedXml 17) ;; -let register_id id node = - if !process_annotations then - match !ids_to_targets with - None -> assert false - | Some ids_to_targets -> - Hashtbl.add ids_to_targets id (Cic.Term node) -;; - (* the "interface" of the class linked to each node of the dom tree *) class virtual cic_term = @@ -176,9 +162,7 @@ class eltype_fix = | _ -> raise (IllFormedXml 13) ) sons in - let res = Cic.AFix (id, ref None, nofun, functions) in - register_id id res ; - res + Cic.AFix (id, nofun, functions) end ;; @@ -209,9 +193,7 @@ class eltype_cofix = | _ -> raise (IllFormedXml 15) ) sons in - let res = Cic.ACoFix (id, ref None, nofun, functions) in - register_id id res ; - res + Cic.ACoFix (id, nofun, functions) end ;; @@ -223,9 +205,7 @@ class eltype_implicit = method to_cic_term = let n = self#node in let id = string_of_xml_attr (n#attribute "id") in - let res = Cic.AImplicit (id, ref None) in - register_id id res ; - res + Cic.AImplicit id end ;; @@ -239,9 +219,7 @@ class eltype_rel = 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") in - let res = Cic.ARel (id,ref None,value,binder) in - register_id id res ; - res + Cic.ARel (id,value,binder) end ;; @@ -253,10 +231,19 @@ class eltype_meta = method to_cic_term = 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 res = Cic.AMeta (id,ref None,value) in - register_id id res ; - res + 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 ;; @@ -280,15 +267,11 @@ class eltype_var = in aux (List.length !current_sp - n,!current_sp) in - let res = - Cic.AVar - (xid,ref None, - (UriManager.uri_of_string - ("cic:" ^ get_prefix (int_of_string index) ^ id ^ ".var")) - ) - in - register_id id res ; - res + Cic.AVar + (xid, + (UriManager.uri_of_string + ("cic:" ^ get_prefix (int_of_string index) ^ id ^ ".var")) + ) | _ -> raise (IllFormedXml 18) end ;; @@ -304,12 +287,8 @@ class eltype_apply = and id = string_of_xml_attr (n#attribute "id") in if List.length children < 2 then raise (IllFormedXml 8) else - let res = - Cic.AAppl - (id,ref None,List.map (fun x -> x#extension#to_cic_term) children) - in - register_id id res ; - res + Cic.AAppl + (id,List.map (fun x -> x#extension#to_cic_term) children) end ;; @@ -328,9 +307,7 @@ class eltype_cast = ty#node_type = Pxp_document.T_element "type" -> let term = te#extension#to_cic_term and typ = ty#extension#to_cic_term in - let res = Cic.ACast (id,ref None,term,typ) in - register_id id res ; - res + Cic.ACast (id,term,typ) | _ -> raise (IllFormedXml 9) end ;; @@ -344,24 +321,7 @@ class eltype_sort = 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 - let res = Cic.ASort (id,ref None,sort) in - register_id id res ; - res - end -;; - -class eltype_abst = - object (self) - - inherit cic_term - - method to_cic_term = - let n = self#node in - let value = uri_of_xml_attr (n#attribute "uri") - and id = string_of_xml_attr (n#attribute "id") in - let res = Cic.AAbst (id,ref None,value) in - register_id id res ; - res + Cic.ASort (id,sort) end ;; @@ -375,11 +335,7 @@ class eltype_const = let n = self#node in let value = uri_of_xml_attr (n#attribute "uri") and id = string_of_xml_attr (n#attribute "id") in - let res = - Cic.AConst (id,ref None,value, U.relative_depth !current_uri value 0) - in - register_id id res ; - res + Cic.AConst (id,value, U.relative_depth !current_uri value 0) end ;; @@ -394,12 +350,8 @@ class eltype_mutind = 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 - let res = - Cic.AMutInd - (id,ref None,name, U.relative_depth !current_uri name 0, noType) - in - register_id id res ; - res + Cic.AMutInd + (id,name, U.relative_depth !current_uri name 0, noType) end ;; @@ -415,13 +367,9 @@ class eltype_mutconstruct = 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 - let res = - Cic.AMutConstruct - (id, ref None, name, U.relative_depth !current_uri name 0, - noType, noConstr) - in - register_id id res ; - res + Cic.AMutConstruct + (id, name, U.relative_depth !current_uri name 0, + noType, noConstr) end ;; @@ -441,9 +389,7 @@ class eltype_prod = let name = cic_attr_of_xml_attr (t#attribute "binder") and source = s#extension#to_cic_term and target = t#extension#to_cic_term in - let res = Cic.AProd (id,ref None,name,source,target) in - register_id id res ; - res + Cic.AProd (id,name,source,target) | _ -> raise (IllFormedXml 10) end ;; @@ -468,12 +414,8 @@ class eltype_mutcase = and inductiveTerm = te#extension#to_cic_term and lpattern= List.map (fun x -> x#extension#to_cic_term) patterns in - let res = - Cic.AMutCase (id,ref None,ci,U.relative_depth !current_uri ci 0, - typeno,inductiveType,inductiveTerm,lpattern) - in - register_id id res ; - res + Cic.AMutCase (id,ci,U.relative_depth !current_uri ci 0, + typeno,inductiveType,inductiveTerm,lpattern) | _ -> raise (IllFormedXml 11) end ;; @@ -494,9 +436,7 @@ class eltype_lambda = let name = cic_attr_of_xml_attr (t#attribute "binder") and source = s#extension#to_cic_term and target = t#extension#to_cic_term in - let res = Cic.ALambda (id,ref None,name,source,target) in - register_id id res ; - res + Cic.ALambda (id,name,source,target) | _ -> raise (IllFormedXml 12) end ;; @@ -517,9 +457,7 @@ class eltype_letin = let name = cic_attr_of_xml_attr (t#attribute "binder") and source = s#extension#to_cic_term and target = t#extension#to_cic_term in - let res = Cic.ALetIn (id,ref None,name,source,target) in - register_id id res ; - res + Cic.ALetIn (id,name,source,target) | _ -> raise (IllFormedXml 12) end ;; @@ -544,7 +482,6 @@ let domspec = "LETIN", (new D.element_impl (new eltype_letin)) ; "APPLY", (new D.element_impl (new eltype_apply)) ; "CONST", (new D.element_impl (new eltype_const)) ; - "ABST", (new D.element_impl (new eltype_abst)) ; "MUTIND", (new D.element_impl (new eltype_mutind)) ; "MUTCONSTRUCT", (new D.element_impl (new eltype_mutconstruct)) ; "MUTCASE", (new D.element_impl (new eltype_mutcase)) ;