]> matita.cs.unibo.it Git - helm.git/commitdiff
moved to xmlPushParser
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 13 Jun 2005 09:56:21 +0000 (09:56 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 13 Jun 2005 09:56:21 +0000 (09:56 +0000)
helm/ocaml/cic/cicUniv.ml

index abb50a196482da30fee62ecdaf33e53c967c9d1a..e79a2a9d9eae1034188ac38a7eaec416c528062a 100644 (file)
@@ -108,9 +108,9 @@ let are_ugraph_eq307 g h =
   try
     MAL.fold (
       fun k v b -> 
-       if not b then 
-         raise (Failure "Different") 
-       else
+        if not b then 
+          raise (Failure "Different") 
+        else
           try
             let k_h = MAL.find k h in
             are_entry_eq v k_h
@@ -128,7 +128,7 @@ let are_ugraph_eq = are_ugraph_eq307
 let string_of_universe (i,u) = 
   match u with
       Some u ->
-       "(" ^ ((string_of_int i) ^ "," ^ (UriManager.string_of_uri u) ^ ")")
+        "(" ^ ((string_of_int i) ^ "," ^ (UriManager.string_of_uri u) ^ ")")
     | None -> "(" ^ (string_of_int i) ^ ",None)"
 
 let string_of_universe_set l = 
@@ -148,7 +148,7 @@ let string_of_mal m =
   let rc = ref "" in
   MAL.iter (fun k v ->  
     rc := !rc ^ sprintf "%s --> %s" (string_of_universe k) 
-             (string_of_node v)) m;
+              (string_of_node v)) m;
   !rc
 
 let string_of_bag b = 
@@ -241,7 +241,7 @@ and closure_gt_fast ru m =
       
 and print_rec_status u ru =
   print_endline ("Aggiusto " ^ (string_of_universe u) ^ 
-                "e ottengo questa chiusura\n " ^ (string_of_node ru))
+                 "e ottengo questa chiusura\n " ^ (string_of_node ru))
 
 and adjust_fast u m =
   let ru = repr u m in
@@ -257,26 +257,26 @@ and adjust_fast u m =
       m
     else
       begin
-       let ru' = {
-         eq_closure = eq_c;
-         ge_closure = ge_c;
-         gt_closure = gt_c;
-         in_gegt_of = ru.in_gegt_of;
-         one_s_eq = ru.one_s_eq;
-         one_s_ge = ru.one_s_ge;
-         one_s_gt = ru.one_s_gt}
-       in
-       let m = MAL.add u ru' m in
-       let m =
+        let ru' = {
+          eq_closure = eq_c;
+          ge_closure = ge_c;
+          gt_closure = gt_c;
+          in_gegt_of = ru.in_gegt_of;
+          one_s_eq = ru.one_s_eq;
+          one_s_ge = ru.one_s_ge;
+          one_s_gt = ru.one_s_gt}
+        in
+        let m = MAL.add u ru' m in
+        let m =
             SOF.fold (fun x m -> adjust_fast  x m) 
               (SOF.union ru'.eq_closure ru'.in_gegt_of) m
               (* TESI: 
                    ru'.in_gegt_of m 
               *)
         in
-         m (*adjust_fast  u m*)
+          m (*adjust_fast  u m*)
       end
-       
+        
 and add_gt_arc_fast u v m =
   let ru = repr u m in
   let ru' = {ru with one_s_gt = SOF.add v ru.one_s_gt} in
@@ -318,7 +318,7 @@ let closure_of u m =
     let j = ru.one_s_eq in
     let _Uj = merge_closures (fun x -> x.eq_closure) j m in
     let one_step_eq = ru.one_s_eq in
-           (SOF.union one_step_eq _Uj)
+            (SOF.union one_step_eq _Uj)
   in
   let ge_c = 
     let j = SOF.union ru.one_s_ge (SOF.union ru.one_s_gt ru.one_s_eq) in
@@ -435,7 +435,7 @@ let error arc node1 closure_type node2 closure =
 let fill_empty_nodes_with_uri g uri =
   let fill_empty_universe u =
     match u with
-       (i,None) -> (i,Some uri)
+        (i,None) -> (i,Some uri)
       | (i,Some _) as u -> u
   in
   let fill_empty_set s =
@@ -533,9 +533,9 @@ let add_gt ?(fast=(!fast_implementation)) u v b =
 (*        begin
           if SOF.mem u rv.eq_closure then
             error ("GT",u,v) u "EQ" v rv.eq_closure
-         else*)
-           add_gt fast u v b
-(*     end
+          else*)
+            add_gt fast u v b
+(*        end
     end*)
 
 (*****************************************************************************)
@@ -572,18 +572,18 @@ let merge_ugraphs u v =
     else
       let m1 = u in 
       let m2 = v in 
-       MAL.fold (
-         fun k v x -> 
-           (SOF.fold (
-              fun u x -> 
-                let m = add_gt k u x in m) v.one_s_gt 
+        MAL.fold (
+          fun k v x -> 
+            (SOF.fold (
+               fun u x -> 
+                 let m = add_gt k u x in m) v.one_s_gt 
                (SOF.fold (
-                 fun u x -> 
-                   let m = add_ge k u x in m) v.one_s_ge
-                 (SOF.fold (
-                    fun u x -> 
-                      let m = add_eq k u x in m) v.one_s_eq x)))
-       ) m1 m2
+                  fun u x -> 
+                    let m = add_ge k u x in m) v.one_s_ge
+                  (SOF.fold (
+                     fun u x -> 
+                       let m = add_eq k u x in m) v.one_s_eq x)))
+        ) m1 m2
   in
     merge_brutal u v
 
@@ -596,12 +596,12 @@ let xml_of_set s =
   let l = 
     List.map (
       function 
-         (i,Some u) -> 
-           Xml.xml_empty "node" [
-             None,"id",(string_of_int i) ;
-             None,"uri",(UriManager.string_of_uri u)]
-       | (_,None) -> 
-           raise (Failure "we can serialize only universes with uri")
+          (i,Some u) -> 
+            Xml.xml_empty "node" [
+              None,"id",(string_of_int i) ;
+              None,"uri",(UriManager.string_of_uri u)]
+        | (_,None) -> 
+            raise (Failure "we can serialize only universes with uri")
     ) (SOF.elements s) 
   in
     List.fold_left (fun s x -> [< s ; x >] ) [<>] l
@@ -628,9 +628,9 @@ let xml_of_entry u e =
   let (i,u') = u in
   let u'' = 
     match u' with 
-       Some x -> x 
+        Some x -> x 
       | None -> 
-         raise (Failure "we can serialize only universes (entry) with uri")
+          raise (Failure "we can serialize only universes (entry) with uri")
   in
   let ent = Xml.xml_nempty "entry" [
     None,"id",(string_of_int i) ; 
@@ -673,8 +673,6 @@ let rec clean_ugraph m f =
 let clean_ugraph g l =
   clean_ugraph g (fun u -> List.mem u l)
 
-open Pxp_types ;;
-
 let assigner_of = 
   function
     "ge_closure" -> (fun e u->{e with ge_closure=SOF.add u e.ge_closure})
@@ -688,26 +686,32 @@ let assigner_of =
 ;;
 
 let cb_factory m = 
+  let module XPP = XmlPushParser in
   let current_node = ref (0,None) in
   let current_entry = ref empty_entry in
   let current_assign = ref (assigner_of "in_ge_of") in
-    function 
-      | E_error exn -> raise (Failure (Pxp_types.string_of_exn exn))
-      | E_start_tag ("entry",attlist,_,_) -> 
-         let id = List.assoc "id" attlist in      
-         let uri = List.assoc "uri" attlist in
-           current_node := (int_of_string id,Some (UriManager.uri_of_string uri))
-      | E_start_tag ("node",attlist,_,_) -> 
-         let id = int_of_string (List.assoc "id" attlist) in
-         let uri = List.assoc "uri" attlist in 
-           current_entry := !current_assign !current_entry 
-             (id,Some (UriManager.uri_of_string uri))
-      | E_start_tag (s,_,_,_) -> 
-         current_assign := assigner_of s
-      | E_end_tag ("entry",_) -> 
-         m := MAL.add !current_node !current_entry !m;
-         current_entry := empty_entry
+  { XPP.default_callbacks with
+    XPP.end_element = Some( fun name ->
+      match name with
+      | "entry" -> 
+          m := MAL.add !current_node !current_entry !m;
+          current_entry := empty_entry
       | _ -> ()
+    );
+    XPP.start_element = Some( fun name attlist ->
+      match name with
+      | "entry" -> 
+          let id = List.assoc "id" attlist in      
+          let uri = List.assoc "uri" attlist in
+          current_node := (int_of_string id,Some (UriManager.uri_of_string uri))
+      | "node" -> 
+          let id = int_of_string (List.assoc "id" attlist) in
+          let uri = List.assoc "uri" attlist in        
+            current_entry := !current_assign !current_entry 
+              (id,Some (UriManager.uri_of_string uri))
+      | s -> current_assign := assigner_of s
+    )
+  }
 ;; 
 
 (* alternative implementation *)
@@ -726,43 +730,45 @@ let entry_of_array a = {
 ;;
 
 let cb_factory' m = 
+  let module XPP = XmlPushParser in
   let current_node = ref (0,None) in
   let current_entry = Array.create 7 SOF.empty in
   let current_assign = ref 0 in
-    function 
-      | E_error exn -> raise (Failure (Pxp_types.string_of_exn exn))
-      | E_start_tag ("entry",attlist,_,_) -> 
-          let id = List.assoc "id" attlist in      
-          let uri = List.assoc "uri" attlist in
-            current_node := (int_of_string id,Some (UriManager.uri_of_string uri))
-      | E_start_tag ("node",attlist,_,_) -> 
-         let id = int_of_string (List.assoc "id" attlist) in
-         let uri = List.assoc "uri" attlist in 
-           current_entry.(!current_assign) <- 
-           SOF.add (id,Some (UriManager.uri_of_string uri)) 
-             current_entry.(!current_assign) 
-      | E_start_tag (s,_,_,_) -> 
-         current_assign := assigner_of' s
-      | E_end_tag ("entry",_) -> 
-         m := MAL.add !current_node (entry_of_array current_entry) !m;
-         Array.fill current_entry 0 7 SOF.empty 
+  { XPP.default_callbacks with
+    XPP.start_element = Some( fun name attlist ->
+      match name with
+      | "entry" -> 
+          let id = List.assoc "id" attlist in      
+          let uri = List.assoc "uri" attlist in
+          current_node := (int_of_string id,Some (UriManager.uri_of_string uri))
+      | "node" -> 
+          let id = int_of_string (List.assoc "id" attlist) in
+          let uri = List.assoc "uri" attlist in        
+          current_entry.(!current_assign) <- 
+            SOF.add (id,Some (UriManager.uri_of_string uri)) 
+              current_entry.(!current_assign) 
+      | s -> current_assign := assigner_of' s
+    );
+    XPP.end_element = Some( fun name -> 
+      match name with
+      | "entry" -> 
+          m := MAL.add !current_node (entry_of_array current_entry) !m;
+          Array.fill current_entry 0 7 SOF.empty 
       | _ -> ()
+    );
+  }
 ;;
 
      
 let ugraph_of_xml filename =
-  let module PX = Pxp_ev_parser in
-  let module NE = Netconversion in 
-  let config = default_config in
-  let entry = `Entry_document [] in
-  let encoding = `Enc_iso88591 in
-  let source = from_file ~system_encoding:encoding filename in
-  let entity_manager = 
-    PX.create_entity_manager ~is_document:true config source in
+  let module XPP = XmlPushParser in
   let result = ref MAL.empty in
   let cb = cb_factory result in
 (*let cb = cb_factory' result in*)
-  PX.process_entity config entry entity_manager cb;
+  let xml_parser = XPP.create_parser cb in
+  let xml_source = `Gzip_file filename in
+  (try XPP.parse xml_parser xml_source
+   with (XPP.Parse_error err) as exn -> raise exn);
   !result
 
 \f
@@ -782,18 +788,18 @@ let randomize_actionlist n m =
     let node2 = Random.int m in
     let op = 
       let r = Random.float 1.0 in
-       if r < ge_percent then 
-         Ge 
-       else (if r < (ge_percent +. gt_percent) then 
-         Gt 
-       else 
-         Eq) 
+        if r < ge_percent then 
+          Ge 
+        else (if r < (ge_percent +. gt_percent) then 
+          Gt 
+        else 
+          Eq) 
     in
       op,node1,node2      
   in
   let rec aux n =
     match n with 
-       0 -> []
+        0 -> []
       | n -> (random_step ())::(aux (n-1))
   in
     aux n
@@ -801,16 +807,16 @@ let randomize_actionlist n m =
 let print_action_list l =
   let string_of_step (op,node1,node2) =
     (match op with
-        Ge -> "Ge"
+         Ge -> "Ge"
        | Gt -> "Gt"
        | Eq -> "Eq") ^ 
     "," ^ (string_of_int node1) ^ ","   ^ (string_of_int node2) 
   in
   let rec aux l =
     match l with 
-       [] -> "]"
+        [] -> "]"
       | a::tl ->
-         ";" ^ (string_of_step a) ^ (aux tl)
+          ";" ^ (string_of_step a) ^ (aux tl)
   in
   let body = aux l in
   let l_body = (String.length body) - 1 in
@@ -835,18 +841,18 @@ let _ =
   let prform_step ?(fast=false) (t,u,v) g =
     let f,str = 
       match t with
-         Ge -> add_ge,">="
-       | Gt -> add_gt,">"
-       | Eq -> add_eq,"="
+          Ge -> add_ge,">="
+        | Gt -> add_gt,">"
+        | Eq -> add_eq,"="
     in
       d_print_endline (
-       "Aggiungo " ^ 
-       (string_of_int u) ^
-       " " ^ str ^ " " ^ 
-       (string_of_int v));
+        "Aggiungo " ^ 
+        (string_of_int u) ^
+        " " ^ str ^ " " ^ 
+        (string_of_int v));
       let g' = f ~fast (u,None) (v,None) g in
-       (*print_ugraph g' ;*)
-       g'
+        (*print_ugraph g' ;*)
+        g'
   in
   let fail = ref false in
   let time1 = Unix.gettimeofday () in
@@ -855,12 +861,12 @@ let _ =
     try 
       d_print_endline "SAFE";
       List.fold_left (
-       fun g e -> 
-         n_safe := !n_safe + 1;
-         prform_step e g
+        fun g e -> 
+          n_safe := !n_safe + 1;
+          prform_step e g
       ) empty_ugraph action_list
     with
-       UniverseInconsistency s -> fail:=true;empty_bag
+        UniverseInconsistency s -> fail:=true;empty_bag
   in
   let time2 = Unix.gettimeofday () in
   d_print_ugraph g_safe;
@@ -870,8 +876,8 @@ let _ =
     try
       d_print_endline "FAST";
       List.fold_left (
-       fun g e ->
-         n_test := !n_test + 1;
+        fun g e ->
+          n_test := !n_test + 1;
           prform_step ~fast:true e g
       ) empty_ugraph action_list
     with
@@ -881,35 +887,35 @@ let _ =
   d_print_ugraph g_test;
     if are_ugraph_eq g_safe g_test && !n_test = !n_safe then
       begin
-       let num_eq = 
-         List.fold_left (
-           fun s (e,_,_) -> 
-             if e = Eq then s+1 else s 
-         ) 0 action_list 
-       in
-       let num_gt = 
-         List.fold_left (
+        let num_eq = 
+          List.fold_left (
+            fun s (e,_,_) -> 
+              if e = Eq then s+1 else s 
+          ) 0 action_list 
+        in
+        let num_gt = 
+          List.fold_left (
             fun s (e,_,_) ->
               if e = Gt then s+1 else s
           ) 0 action_list
         in
-       let num_ge = max_edges - num_gt - num_eq in
-       let time_fast = (time4 -. time3) in
-       let time_safe = (time2 -. time1) in
-       let gap = ((time_safe -. time_fast) *. 100.0) /. time_safe in
-       let fail = if !fail then 1 else 0 in
-         print_endline 
-           (sprintf 
-              "OK %d safe %1.4f fast %1.4f %% %1.2f #eq %d #gt %d #ge %d %d" 
-              fail time_safe time_fast gap num_eq num_gt num_ge !n_safe);
-         exit 0
+        let num_ge = max_edges - num_gt - num_eq in
+        let time_fast = (time4 -. time3) in
+        let time_safe = (time2 -. time1) in
+        let gap = ((time_safe -. time_fast) *. 100.0) /. time_safe in
+        let fail = if !fail then 1 else 0 in
+          print_endline 
+            (sprintf 
+               "OK %d safe %1.4f fast %1.4f %% %1.2f #eq %d #gt %d #ge %d %d" 
+               fail time_safe time_fast gap num_eq num_gt num_ge !n_safe);
+          exit 0
       end
     else
       begin
-       print_endline "FAIL";
+        print_endline "FAIL";
         print_ugraph g_safe;
         print_ugraph g_test;
-       exit 1
+        exit 1
       end
 ;;