X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Furimanager%2FuriManager.ml;h=b4bf073e2733401ffe760a1aa5ab14ff444563c9;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=b8da7d91eddec50f086251bf863da6df40f99e66;hpb=c63e8332bdded20ff61d47bd5951a80c29b41942;p=helm.git diff --git a/helm/ocaml/urimanager/uriManager.ml b/helm/ocaml/urimanager/uriManager.ml index b8da7d91e..b4bf073e2 100644 --- a/helm/ocaml/urimanager/uriManager.ml +++ b/helm/ocaml/urimanager/uriManager.ml @@ -77,16 +77,63 @@ module MapStringsToUri = Map.Make(OrderedStrings);; *) let set_of_uri = ref MapStringsToUri.empty;; +exception IllFormedUri of string;; + +let _dottypes = ".types" +let _types = "types",5 +let _dotuniv = ".univ" +let _univ = "univ",4 +let _dotann = ".ann" +let _ann = "ann",3 +let _var = "var",3 +let _dotbody = ".body" +let _con = "con",3 +let _ind = "ind",3 +let _xpointer = "#xpointer(1/" +let _con3 = "con" +let _var3 = "var" +let _ind3 = "ind" +let _ann3 = "ann" +let _univ4 = "univ" +let _types5 = "types" +let _xpointer8 = "xpointer" +let _cic5 = "cic:/" + +let is_malformed suri = + try + if String.sub suri 0 5 <> _cic5 then true + else + let len = String.length suri - 5 in + let last5 = String.sub suri len 5 in + let last4 = String.sub last5 1 4 in + let last3 = String.sub last5 2 3 in + if last3 = _con3 || last3 = _var3 || last3 = _ind3 || + last3 = _ann3 || last5 = _types5 || last5 = _dotbody || + last4 = _univ4 then + false + else + try + let index = String.rindex suri '#' + 1 in + let xptr = String.sub suri index 8 in + if xptr = _xpointer8 then + false + else + true + with Not_found -> true + with Invalid_argument _ -> true + (* hash conses an uri *) let uri_of_string suri = try MapStringsToUri.find suri !set_of_uri with Not_found -> - let new_uri = suri, fresh_id () in - set_of_uri := MapStringsToUri.add suri new_uri !set_of_uri; - new_uri + if is_malformed suri then + raise (IllFormedUri suri) + else + let new_uri = suri, fresh_id () in + set_of_uri := MapStringsToUri.add suri new_uri !set_of_uri; + new_uri -exception IllFormedUri of string;; let strip_xpointer ((uri,_) as olduri) = try @@ -115,14 +162,6 @@ let has_suffix uri (pat,n) = with Not_found -> assert false -let _dottypes = ".types" -let _types = "types",5 -let _ann = "ann",3 -let _dotann = ".ann" -let _var = "var",3 -let _dotbody = ".body" -let _con = "con",3 -let _xpointer = "#xpointer(1/" let cicuri_of_uri (uri, _) = uri_of_string (clear_suffix uri ~pat2:_types _ann) @@ -134,6 +173,8 @@ let uri_is_var (uri, _) = has_suffix uri _var let uri_is_con (uri, _) = has_suffix uri _con +let uri_is_ind (uri, _) = has_suffix uri _ind + let bodyuri_of_uri (uri, _) = if has_suffix uri _con then Some (uri_of_string (uri ^ _dotbody)) @@ -141,9 +182,15 @@ let bodyuri_of_uri (uri, _) = None ;; +(* these are bugged! + * we should remove _types, _univ, _ann all toghether *) let innertypesuri_of_uri (uri, _) = uri_of_string ((clear_suffix uri _types) ^ _dottypes) ;; +let univgraphuri_of_uri (uri,_) = + uri_of_string ((clear_suffix uri _univ) ^ _dotuniv) +;; + let uri_of_uriref (uri, _) typeno consno = let typeno = typeno + 1 in @@ -164,3 +211,13 @@ end module UriSet = Set.Make (OrderedUri) +module HashedUri = +struct + type t = uri + let equal = eq + let hash = snd +end + +module UriHashtbl = Hashtbl.Make (HashedUri) + +