X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicParser3.ml;h=82ca496924225edcb6fdf30b41b6fa4e83e78588;hb=ae326f646ef4c01b43d6da04201b427d1e175400;hp=ff356b13e0b58fe99515e4d5882c61faa2c70341;hpb=538b694e70fafbf298f27cf57cae13928bac95af;p=helm.git

diff --git a/helm/ocaml/cic/cicParser3.ml b/helm/ocaml/cic/cicParser3.ml
index ff356b13e..82ca49692 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
 ;;
 
@@ -254,9 +232,7 @@ class eltype_meta =
      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
+       Cic.AMeta (id,value)
   end
 ;;
 
@@ -280,15 +256,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 +276,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 +296,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,9 +310,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
+       Cic.ASort (id,sort)
   end
 ;;
 
@@ -359,9 +323,7 @@ class eltype_abst =
      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.AAbst (id,value)
   end
 ;;
 
@@ -375,11 +337,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 +352,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 +369,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 +391,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 +416,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 +438,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 +459,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
 ;;