From 68eea268e230d7eb12cdc416ead471a86a4bb5e4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 23 Sep 2005 12:49:24 +0000 Subject: [PATCH] added parsing of Type:N --- helm/ocaml/cic/cicParser.ml | 19 ++++- helm/ocaml/cic/cicUniv.ml | 145 ++++++++++++++++-------------------- helm/ocaml/cic/cicUniv.mli | 24 ++++-- 3 files changed, 99 insertions(+), 89 deletions(-) diff --git a/helm/ocaml/cic/cicParser.ml b/helm/ocaml/cic/cicParser.ml index 887ed975f..d81521f99 100644 --- a/helm/ocaml/cic/cicParser.ml +++ b/helm/ocaml/cic/cicParser.ml @@ -297,10 +297,23 @@ let uri_list_of_string = let sort_of_string ctxt = function | "Prop" -> Cic.Prop | "Set" -> Cic.Set - | "Type" -> Cic.Type (CicUniv.fresh ~uri:ctxt.uri ()) -(* | "Type" -> CicUniv.restart_numbering (); |+ useful only to test parser +| *) | "CProp" -> Cic.CProp - | _ -> parse_error ctxt "sort expected" + (* THIS CASE IS HERE ONLY TO ALLOW THE PARSING OF COQ LIBRARY + * THIS SHOULD BE REMOVED AS SOON AS univ_maker OR COQ'S EXPORTATION + * IS FIXED *) + | "Type" -> Cic.Type (CicUniv.fresh ~uri:ctxt.uri ()) + | s -> + let len = String.length s in + if not(len > 5) then parse_error ctxt "sort expected"; + if not(String.sub s 0 5 = "Type:") then parse_error ctxt "sort expected"; + try + Cic.Type + (CicUniv.fresh + ~uri:ctxt.uri + ~id:(int_of_string (String.sub s 5 (len - 5))) ()) + with + | Failure "int_of_string" + | Invalid_argument _ -> parse_error ctxt "sort expected" let patch_subst ctxt subst = function | Cic.AConst (id, uri, _) -> Cic.AConst (id, uri, subst) diff --git a/helm/ocaml/cic/cicUniv.ml b/helm/ocaml/cic/cicUniv.ml index 5616cb675..0ea97404e 100644 --- a/helm/ocaml/cic/cicUniv.ml +++ b/helm/ocaml/cic/cicUniv.ml @@ -411,7 +411,7 @@ let error arc node1 closure_type node2 closure = 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) @@ -434,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' (*****************************************************************************) @@ -450,15 +451,17 @@ let current_index_named = ref (-1) let restart_numbering () = current_index_named := (-1) -let fresh ?uri () = +let fresh ?uri ?id () = let i = - match uri with - | None -> + match uri,id with + | None,None -> current_index_anon := !current_index_anon + 1; !current_index_anon - | Some _ -> + | None, Some _ -> assert false + | Some _, None -> current_index_named := !current_index_named + 1; !current_index_named + | Some _, Some id -> id in (i,uri) @@ -571,17 +574,18 @@ let merge_ugraphs 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 @@ -617,15 +621,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' = @@ -664,11 +672,11 @@ 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 + let current_assign = ref (assigner_of "in_gegt_of") in { XPP.default_callbacks with XPP.end_element = Some( fun name -> match name with @@ -679,6 +687,7 @@ let cb_factory m = ); 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 @@ -688,67 +697,25 @@ let cb_factory m = 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 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 - { 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 ugraph_and_univlist_of_xml filename = let module XPP = XmlPushParser in - let result = ref MAL.empty in - let cb = cb_factory result in -(*let cb = cb_factory' result 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 + !result_map, !result_list (*****************************************************************************) @@ -931,7 +898,7 @@ let assert_univ u = | (_,None) -> raise (UniverseInconsistency "This universe graph has a hole") | _ -> () -let assert_univs_have_uri graph = +let assert_univs_have_uri graph univlist = let assert_set s = SOF.iter (fun u -> assert_univ u) s in @@ -944,7 +911,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 *) diff --git a/helm/ocaml/cic/cicUniv.mli b/helm/ocaml/cic/cicUniv.mli index 3eec9b3be..219513012 100644 --- a/helm/ocaml/cic/cicUniv.mli +++ b/helm/ocaml/cic/cicUniv.mli @@ -44,6 +44,7 @@ type universe_graph *) val fresh: ?uri:UriManager.uri -> + ?id:int -> unit -> universe @@ -87,9 +88,12 @@ val clean_ugraph: (* Since fresh() can't add the right uri to each node, you must fill empty nodes with the uri before you serialize the graph to xml + + these empty nodes are also filled in the universe list *) val fill_empty_nodes_with_uri: - universe_graph -> UriManager.uri -> universe_graph + universe_graph -> universe list -> UriManager.uri -> + universe_graph * universe list (* makes a union. @@ -105,16 +109,21 @@ val merge_ugraphs: ugraph to xml file and viceversa *) val write_xml_of_ugraph: - string -> universe_graph -> unit + string -> universe_graph -> universe list -> unit (* given a filename parses the xml and returns the data structure *) -val ugraph_of_xml: - string -> universe_graph +val ugraph_and_univlist_of_xml: + string -> universe_graph * universe list val restart_numbering: unit -> unit +(* + returns the universe number (used to save it do xml) +*) +val univno: universe -> int + (** re-hash-cons URIs contained in the given universe so that phisicaly * equality could be enforced. Mainly used by * CicEnvironment.restore_from_channel *) @@ -125,11 +134,14 @@ val recons_univ: universe -> universe (** consistency chek that should be done before committin the graph to the * cache *) -val assert_univs_have_uri: universe_graph -> unit +val assert_univs_have_uri: universe_graph -> universe list-> unit - (** asserts the univers is named *) + (** asserts the universe is named *) val assert_univ: universe -> unit +val compare: universe -> universe -> int +val eq: universe -> universe -> bool + (* Benchmarking stuff *) -- 2.39.2