X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicUniv.ml;h=3d92f33358f1b76929027eb0366da95bea03d7ec;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=7f8266876ddbcaf891d03c8e8bc0bc8086eba685;hpb=9d3dcd6970c1e24c8191f268c441e42c8d8b6c89;p=helm.git diff --git a/helm/ocaml/cic/cicUniv.ml b/helm/ocaml/cic/cicUniv.ml index 7f8266876..3d92f3335 100644 --- a/helm/ocaml/cic/cicUniv.ml +++ b/helm/ocaml/cic/cicUniv.ml @@ -38,7 +38,7 @@ (** switch implementation **) (*****************************************************************************) -let fast_implementation = ref false ;; +let fast_implementation = ref true ;; (*****************************************************************************) (** open **) @@ -98,28 +98,7 @@ let are_entry_eq v1 v2 = (are_set_eq v1.one_s_gt v2.one_s_gt ) && (are_set_eq v1.one_s_eq v2.one_s_eq ) - -(* ocaml 3.07 doesn't have MAP.equal, 3.08 has it! *) -(* - let are_ugraph_eq308 g h = - MAL.equal are_entry_eq g h -*) -let are_ugraph_eq307 g h = - try - MAL.fold ( - fun k v b -> - if not b then - raise (Failure "Different") - else - try - let k_h = MAL.find k h in - are_entry_eq v k_h - with Not_found -> true - ) g true - with - Failure "Different" -> false - -let are_ugraph_eq = are_ugraph_eq307 +let are_ugraph_eq = MAL.equal are_entry_eq (*****************************************************************************) (** Pretty printings **) @@ -128,8 +107,8 @@ 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)) - | None -> (string_of_int i) + "(" ^ ((string_of_int i) ^ "," ^ (UriManager.string_of_uri u) ^ ")") + | None -> "(" ^ (string_of_int i) ^ ",None)" let string_of_universe_set l = SOF.fold (fun x s -> s ^ (string_of_universe x) ^ " ") l "" @@ -142,13 +121,13 @@ let string_of_node n = "i_gegt: " ^ (string_of_universe_set n.in_gegt_of) ^ "}\n" let string_of_arc (a,u,v) = - "(" ^ (string_of_universe u) ^ " " ^ a ^ " " ^ (string_of_universe v) ^ ")" + (string_of_universe u) ^ " " ^ a ^ " " ^ (string_of_universe v) 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 = @@ -178,7 +157,7 @@ let partial = ref 0.0 ;; let reset_spent_time () = time_spent := 0.0;; let get_spent_time () = !time_spent ;; let begin_spending () = - assert (!partial = 0.0); + (*assert (!partial = 0.0);*) partial := Unix.gettimeofday () ;; @@ -241,7 +220,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 +236,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 @@ -293,7 +272,7 @@ and add_ge_arc_fast u v m = let rv = repr v m' in let rv' = {rv with in_gegt_of = SOF.add u rv.in_gegt_of} in let m'' = MAL.add v rv' m' in - adjust_fast u m'' + adjust_fast u m'' and add_eq_arc_fast u v m = let ru = repr u m in @@ -318,7 +297,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 @@ -419,26 +398,29 @@ exception UniverseInconsistency of string let error arc node1 closure_type node2 closure = let s = "\n ===== Universe Inconsistency detected =====\n\n" ^ - "\tUnable to add "^ (string_of_arc arc) ^ " cause " ^ - (string_of_universe node1) ^ " is in the " ^ - closure_type ^ " closure {" ^ - (string_of_universe_set closure) ^ "} of " ^ - (string_of_universe node2) ^ "\n\n" ^ + " Unable to add\n" ^ + "\t" ^ (string_of_arc arc) ^ "\n" ^ + " cause\n" ^ + "\t" ^ (string_of_universe node1) ^ "\n" ^ + " is in the " ^ closure_type ^ " closure\n" ^ + "\t{" ^ (string_of_universe_set closure) ^ "}\n" ^ + " of\n" ^ + "\t" ^ (string_of_universe node2) ^ "\n\n" ^ " ===== Universe Inconsistency detected =====\n" in prerr_endline s; raise (UniverseInconsistency s) -let fill_empty_nodes_with_uri g uri = +let fill_empty_nodes_with_uri g l 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 = SOF.fold (fun e s -> SOF.add (fill_empty_universe e) s) s SOF.empty in - let fill_empty_entry e = { + let fill_empty_entry e = { e with eq_closure = (fill_empty_set e.eq_closure) ; ge_closure = (fill_empty_set e.ge_closure) ; gt_closure = (fill_empty_set e.gt_closure) ; @@ -452,7 +434,8 @@ let fill_empty_nodes_with_uri g uri = fun k v m -> MAL.add (fill_empty_universe k) (fill_empty_entry v) m) m MAL.empty in - m' + let l' = List.map fill_empty_universe l in + m',l' (*****************************************************************************) @@ -463,14 +446,30 @@ type universe_graph = bag let empty_ugraph = empty_bag -let current_index = ref (-1) - -let restart_numbering () = current_index := (-1) - -let fresh () = - current_index := !current_index + 1; - (!current_index,None) +let current_index_anon = ref (-1) +let current_index_named = ref (-1) + +let restart_numbering () = current_index_named := (-1) + +let fresh ?uri ?id () = + let i = + match uri,id with + | None,None -> + current_index_anon := !current_index_anon + 1; + !current_index_anon + | None, Some _ -> assert false + | Some _, None -> + current_index_named := !current_index_named + 1; + !current_index_named + | Some _, Some id -> id + in + (i,uri) +let name_universe u uri = + match u with + | (i, None) -> (i, Some uri) + | _ -> u + let print_ugraph g = prerr_endline (string_of_bag g) @@ -521,9 +520,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*) (*****************************************************************************) @@ -560,37 +559,41 @@ 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) + (SOF.union v.one_s_gt v.gt_closure) (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) + (SOF.union v.one_s_ge v.ge_closure) + (SOF.fold ( + fun u x -> + let m = add_eq k u x in m) + (SOF.union v.one_s_eq v.eq_closure) x))) + ) m1 m2 in - merge_brutal u v + merge_brutal u v (*****************************************************************************) (** Xml sesialization and parsing **) (*****************************************************************************) +let xml_of_universe name u = + match u with + | (i,Some u) -> + Xml.xml_empty name [ + None,"id",(string_of_int i) ; + None,"uri",(UriManager.string_of_uri u)] + | (_,None) -> + raise (Failure "we can serialize only universes with uri") + 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") - ) (SOF.elements s) + List.map (xml_of_universe "node") (SOF.elements s) in List.fold_left (fun s x -> [< s ; x >] ) [<>] l @@ -616,9 +619,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) ; @@ -626,15 +629,19 @@ let xml_of_entry u e = let content = xml_of_entry_content e in ent content -let write_xml_of_ugraph filename m = - let o = open_out filename in - output_string o "\n"; - Xml.pp_to_outchan ( - Xml.xml_nempty "ugraph" [] ( - MAL.fold ( - fun k v s -> [< s ; (xml_of_entry k v) >]) - m [<>])) o; - close_out o +let write_xml_of_ugraph filename m l = + let tokens = + [< + Xml.xml_cdata "\n"; + Xml.xml_nempty "ugraph" [] + ([< (MAL.fold ( fun k v s -> [< s ; (xml_of_entry k v) >]) m [<>]) ; + (List.fold_left + (fun s u -> [< s ; xml_of_universe "owned_node" u >]) [<>] l) >])>] + in + Xml.pp ~gzip:true tokens (Some filename) + +let univno = fst + let rec clean_ugraph m f = let m' = @@ -651,18 +658,20 @@ let rec clean_ugraph m f = } in MAL.add k v' x ) m' MAL.empty in let e_l = - MAL.fold (fun k v l -> if v = empty_entry then k::l else l) m'' [] + MAL.fold (fun k v l -> if v = empty_entry && not(f k) then + begin + k::l end else l) m'' [] in if e_l != [] then clean_ugraph m'' (fun u -> (f u) && not (List.mem u e_l)) else - m'' + MAL.fold + (fun k v x -> if v <> empty_entry then MAL.add k v x else x) + m'' MAL.empty 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}) @@ -675,83 +684,50 @@ let assigner_of = | s -> raise (Failure ("unsupported tag " ^ s)) ;; -let cb_factory m = +let cb_factory m l = + 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 + let current_assign = ref (assigner_of "in_gegt_of") in + { 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 + | "ugraph" -> () + | "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)) + | "owned_node" -> + let id = int_of_string (List.assoc "id" attlist) in + let uri = List.assoc "uri" attlist in + l := (id,Some (UriManager.uri_of_string uri)) :: !l + | s -> current_assign := assigner_of s + ) + } ;; -(* alternative implementation *) -let mapl = [ - ("ge_closure",0);("gt_closure",1);("eq_closure",2); - ("in_gegt_of", 3); - ("one_s_ge", 4);("one_s_gt", 5);("one_s_eq", 6)] -;; - -let assigner_of' s = List.assoc s mapl ;; - -let entry_of_array a = { - ge_closure = a.(0); gt_closure = a.(1); eq_closure = a.(2); - in_gegt_of = a.(3); - one_s_ge = a.(4); one_s_gt = a.(5); one_s_eq = a.(6)} -;; - -let cb_factory' m = - 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 - | _ -> () -;; - - -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 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; - !result +let ugraph_and_univlist_of_xml filename = + let module XPP = XmlPushParser in + let result_map = ref MAL.empty in + let result_list = ref [] in + let cb = cb_factory result_map result_list in + 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_map, !result_list (*****************************************************************************) @@ -770,18 +746,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 @@ -789,16 +765,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 @@ -823,18 +799,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 @@ -843,12 +819,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; @@ -858,8 +834,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 @@ -869,35 +845,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 ;; @@ -929,12 +905,12 @@ let recons_graph graph = MAL.add (recons_univ universe) (recons_entry entry) map) graph MAL.empty -let assert_univs_have_uri graph = - let assert_univ u = +let assert_univ u = match u with | (_,None) -> raise (UniverseInconsistency "This universe graph has a hole") | _ -> () - in + +let assert_univs_have_uri graph univlist = let assert_set s = SOF.iter (fun u -> assert_univ u) s in @@ -947,7 +923,25 @@ let assert_univs_have_uri graph = assert_set e.one_s_ge; assert_set e.one_s_gt; in - MAL.iter (fun k v -> assert_univ k; assert_entry v)graph + MAL.iter (fun k v -> assert_univ k; assert_entry v)graph; + List.iter assert_univ univlist + +let eq u1 u2 = + match u1,u2 with + | (id1, Some uri1),(id2, Some uri2) -> + id1 = id2 && UriManager.eq uri1 uri2 + | (id1, None),(id2, None) -> id1 = id2 + | _ -> false + +let compare (id1, uri1) (id2, uri2) = + let cmp = id1 - id2 in + if cmp = 0 then + match uri1,uri2 with + | None, None -> 0 + | Some _, None -> 1 + | None, Some _ -> ~-1 + | Some uri1, Some uri2 -> UriManager.compare uri1 uri2 + else + cmp - (* EOF *)