X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_annotations%2FcicAnnotation2Xml.ml;h=1961a2bc2c726ddd7c920729bd2998e6d7ea003d;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=c5410b0804779f047fc2c9359c173044d74927f3;hpb=5a92117eeff70048d29e91ba24e113155d956e1b;p=helm.git

diff --git a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml
index c5410b080..1961a2bc2 100644
--- a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml
+++ b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml
@@ -25,127 +25,62 @@
 
 (*CSC codice cut & paste da cicPp e xmlcommand *)
 
-exception ImpossiblePossible;;
 exception NotImplemented;;
-exception BinderNotSpecified;;
 
 let dtdname = "http://www.cs.unibo.it/helm/dtd/annotations.dtd";;
 
+let get_ann ids_to_annotations =
+ CicXPath.get_annotation ids_to_annotations
+;;
+
+let print_ann i2a id =
+ let module X = Xml in
+  let ann = get_ann i2a id in
+   match ann with
+      None -> [<>]
+    | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
+;;
+
 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
-let print_term =
+(* It takes in input a hash table mapping ids to annotations, an annotated 
+term, and gives back a Xml.token Stream.t representing the .ann file *)
+let print_term i2a =
  let rec aux =
   let module C = Cic in
   let module X = Xml in
   let module U = UriManager in
     function
-       C.ARel (id,ann,_,_) ->
-        (match !ann with
-            None -> [<>]
-          | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-        )
-     | C.AVar (id,ann,_) ->
-        (match !ann with
-            None -> [<>]
-          | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-        )
-     | C.AMeta (id,ann,_) ->
-        (match !ann with
-            None -> [<>]
-          | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-        )
-     | C.ASort (id,ann,_) ->
-        (match !ann with
-            None -> [<>]
-          | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-        )
+       C.ARel (id,_,_) -> print_ann i2a id
+     | C.AVar (id,_) -> print_ann i2a id
+     | C.AMeta (id,_,_) -> print_ann i2a id
+     | C.ASort (id,_) -> print_ann i2a id
      | C.AImplicit _ -> raise NotImplemented
-     | C.AProd (id,ann,_,s,t) ->
-        [< (match !ann with
-               None -> [<>]
-             | Some ann ->
-                (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-           ) ;
-           aux s ;
-           aux t
-        >]
-     | C.ACast (id,ann,v,t) ->
-        [< (match !ann with
-               None -> [<>]
-             | Some ann ->
-                (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-           ) ;
-           aux v ;
-           aux t
-        >]
-     | C.ALambda (id,ann,_,s,t) ->
-        [< (match !ann with
-               None -> [<>]
-             | Some ann ->
-                (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-           ) ;
-           aux s ;
-           aux t
-        >]
-     | C.ALetIn (id,ann,_,s,t) ->
-        [< (match !ann with
-               None -> [<>]
-             | Some ann ->
-                (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-           ) ;
-           aux s ;
-           aux t
-        >]
-     | C.AAppl (id,ann,li) ->
-        [< (match !ann with
-               None -> [<>]
-             | Some ann ->
-                (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-           ) ;
+     | C.AProd (id,_,s,t) -> [< print_ann i2a id ; aux s ; aux t >]
+     | C.ACast (id,v,t) -> [< print_ann i2a id ; aux v ; aux t >]
+     | C.ALambda (id,_,s,t) -> [< print_ann i2a id ; aux s ; aux t >]
+     | C.ALetIn (id,_,s,t) -> [< print_ann i2a id ; aux s ; aux t >]
+     | C.AAppl (id,li) ->
+        [< print_ann i2a id ;
            List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>]
         >]
-     | C.AConst (id,ann,_,_) ->
-        (match !ann with
-            None -> [<>]
-          | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-        )
-     | C.AAbst (id,ann,_) -> raise NotImplemented
-     | C.AMutInd (id,ann,_,_,_) ->
-        (match !ann with
-            None -> [<>]
-          | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-        )
-     | C.AMutConstruct (id,ann,_,_,_,_) ->
-        (match !ann with
-            None -> [<>]
-          | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-        )
-     | C.AMutCase (id,ann,_,_,_,ty,te,patterns) ->
-        [< (match !ann with
-               None -> [<>]
-             | Some ann ->
-                (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-           ) ;
+     | C.AConst (id,_,_) -> print_ann i2a id
+     | C.AMutInd (id,_,_,_) -> print_ann i2a id
+     | C.AMutConstruct (id,_,_,_,_) -> print_ann i2a id
+     | C.AMutCase (id,_,_,_,ty,te,patterns) ->
+        [< print_ann i2a id ;
            aux ty ;
            aux te ;
            List.fold_right
             (fun x i -> [< aux x ; i>])
             patterns [<>]
         >]
-     | C.AFix (id, ann, _, funs) ->
-        [< (match !ann with
-               None -> [<>]
-             | Some ann ->
-                (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-           ) ;
+     | C.AFix (id,_,funs) ->
+        [< print_ann i2a id ;
            List.fold_right
             (fun (_,_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>]
         >]
-     | C.ACoFix (id, ann,no,funs) ->
-        [< (match !ann with
-               None -> [<>]
-             | Some ann ->
-                (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-           ) ;
+     | C.ACoFix (id,no,funs) ->
+        [< print_ann i2a id ;
            List.fold_right
             (fun (_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>]
         >]
@@ -153,14 +88,14 @@ let print_term =
   aux
 ;;
 
-let print_mutual_inductive_type (_,_,arity,constructors) =
- [< print_term arity ;
+let print_mutual_inductive_type i2a (_,_,arity,constructors) =
+ [< print_term i2a arity ;
     List.fold_right
-     (fun (name,ty,_) i -> [< print_term ty ; i >]) constructors [<>]
+     (fun (name,ty,_) i -> [< print_term i2a ty ; i >]) constructors [<>]
  >]
 ;;
 
-let pp_annotation obj curi =
+let pp_annotation obj i2a curi =
  let module C = Cic in
  let module X = Xml in
   [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
@@ -169,57 +104,47 @@ let pp_annotation obj curi =
       ["of", UriManager.string_of_uri (UriManager.cicuri_of_uri curi)]
       begin
        match obj with
-         C.ADefinition (xid, ann, _, te, ty, _) ->
-          [< (match !ann with
-                 None -> [<>]
-               | Some ann ->
-                  X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
-             ) ;
-             print_term te ;
-             print_term ty
-          >]
-       | C.AAxiom (xid, ann, _, ty, _) ->
-          [< (match !ann with
-                 None -> [<>]
-               | Some ann ->
-                  X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
-             ) ;
-             print_term ty
-          >]
-       | C.AVariable (xid, ann, _, bo, ty) ->
-          [< (match !ann with
-                 None -> [<>]
-               | Some ann ->
-                  X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
-             ) ;
+         C.ADefinition (xid, _, te, ty, _) ->
+          [< print_ann i2a xid ; print_term i2a te ; print_term i2a ty >]
+       | C.AAxiom (xid, _, ty, _) -> [< print_ann i2a xid ; print_term i2a ty >]
+       | C.AVariable (xid, _, bo, ty) ->
+          [< print_ann i2a xid ;
              (match bo with
                  None -> [<>]
-               | Some bo -> print_term bo
+               | Some bo -> print_term i2a bo
              ) ;
-             print_term ty
+             print_term i2a ty
           >]
-       | C.ACurrentProof (xid, ann, _, conjs, bo, ty) ->
-          [< (match !ann with
-                 None -> [<>]
-               | Some ann ->
-                  X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
-             ) ;
+       | C.ACurrentProof (xid, _, conjs, bo, ty) ->
+          [< print_ann i2a xid ;
              List.fold_right
-              (fun (_,t) i -> [< print_term t ; i >])
-              conjs [<>] ;
-             print_term bo ;
-             print_term ty
+              (fun (cid, _, context, t) i ->
+                [< print_ann i2a cid ;
+                   List.fold_right
+		    (fun (hid,context_entry) i -> 
+		      [<print_ann i2a hid ;
+                        (match context_entry with
+			    Some (_,C.ADecl at) -> print_term i2a at
+		          | Some (_,C.ADef at) -> print_term i2a at
+		          | None -> [< >]
+                        ) ; i
+                       >]
+		    ) context [< >];
+		   print_term i2a t ; i
+                >]
+              ) conjs [<>] ;
+             print_term i2a bo ;
+             print_term i2a ty
           >]
-       | C.AInductiveDefinition (xid, ann, tys, params, paramsno) ->
-          [< (match !ann with
-                 None -> [<>]
-               | Some ann ->
-                  X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
-             ) ;
+       | C.AInductiveDefinition (xid, tys, params, paramsno) ->
+          [< print_ann i2a xid ;
              List.fold_right
-              (fun x i -> [< print_mutual_inductive_type x ; i >])
+              (fun x i -> [< print_mutual_inductive_type i2a x ; i >])
               tys [< >]
           >]
       end
   >]
 ;;
+
+
+