From 813025418906707f7bbbf43732fc0e8d5cfc6943 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 5 Feb 2008 15:54:52 +0000 Subject: [PATCH] uri and references(uri) --- helm/software/components/ng_kernel/.depend | 11 ++-- helm/software/components/ng_kernel/Makefile | 2 +- .../components/ng_kernel/nReference.ml | 62 +++++++++---------- .../components/ng_kernel/nReference.mli | 2 +- helm/software/components/ng_kernel/nUri.ml | 37 +++++++++++ helm/software/components/ng_kernel/nUri.mli | 7 +++ 6 files changed, 84 insertions(+), 37 deletions(-) create mode 100644 helm/software/components/ng_kernel/nUri.ml create mode 100644 helm/software/components/ng_kernel/nUri.mli diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend index 497730e2b..5fb3278ed 100644 --- a/helm/software/components/ng_kernel/.depend +++ b/helm/software/components/ng_kernel/.depend @@ -1,13 +1,16 @@ nCicEnvironment.cmi: nReference.cmi nCic.cmo nCicTypeChecker.cmi: nCic.cmo +nReference.cmi: nUri.cmi oCic2NCic.cmi: nCic.cmo -nCicEnvironment.cmo: oCic2NCic.cmi nCicEnvironment.cmi -nCicEnvironment.cmx: oCic2NCic.cmx nCicEnvironment.cmi +nCicEnvironment.cmo: oCic2NCic.cmi nReference.cmi nCicEnvironment.cmi +nCicEnvironment.cmx: oCic2NCic.cmx nReference.cmx nCicEnvironment.cmi nCicTypeChecker.cmo: nCicTypeChecker.cmi nCicTypeChecker.cmx: nCicTypeChecker.cmi -nReference.cmo: nReference.cmi -nReference.cmx: nReference.cmi +nReference.cmo: nUri.cmi nReference.cmi +nReference.cmx: nUri.cmx nReference.cmi oCicTypeChecker.cmo: oCic2NCic.cmi nCicTypeChecker.cmi oCicTypeChecker.cmi oCicTypeChecker.cmx: oCic2NCic.cmx nCicTypeChecker.cmx oCicTypeChecker.cmi oCic2NCic.cmo: oCic2NCic.cmi oCic2NCic.cmx: oCic2NCic.cmi +nUri.cmo: nUri.cmi +nUri.cmx: nUri.cmi diff --git a/helm/software/components/ng_kernel/Makefile b/helm/software/components/ng_kernel/Makefile index 209170288..65c0ab906 100644 --- a/helm/software/components/ng_kernel/Makefile +++ b/helm/software/components/ng_kernel/Makefile @@ -2,7 +2,7 @@ PACKAGE = ng_kernel PREDICATES = INTERFACE_FILES = \ - nCicEnvironment.mli nCicTypeChecker.mli nReference.mli oCicTypeChecker.mli oCic2NCic.mli + nCicEnvironment.mli nCicTypeChecker.mli nReference.mli oCicTypeChecker.mli oCic2NCic.mli nUri.mli IMPLEMENTATION_FILES = \ nCic.ml $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = diff --git a/helm/software/components/ng_kernel/nReference.ml b/helm/software/components/ng_kernel/nReference.ml index bcdd4713e..ad93584fb 100644 --- a/helm/software/components/ng_kernel/nReference.ml +++ b/helm/software/components/ng_kernel/nReference.ml @@ -33,12 +33,10 @@ type spec = | Ind of int | Con of int * int (* indtyno, constrno *) -type reference = Ref of int * string * spec +type reference = Ref of int * NUri.uri * spec let eq = (==);; -let string_of_reference (Ref (_,s,_)) = s;; - module OrderedStrings = struct type t = string @@ -46,9 +44,9 @@ module OrderedStrings = end ;; -module MapStringsToUri = Map.Make(OrderedStrings);; +module MapStringsToReference = Map.Make(OrderedStrings);; -let set_of_reference = ref MapStringsToUri.empty;; +let set_of_reference = ref MapStringsToReference.empty;; (* '.' not allowed in path and foo * @@ -60,6 +58,14 @@ let set_of_reference = ref MapStringsToUri.empty;; * Con of int * int cic:/path/foo.con(i,j) *) +let uri_suffix_of_ref_suffix = function + | "dec" + | "def" -> "con" + | "ind" + | "con" -> "ind" + | _ -> assert false +;; + let reference_of_string = let counter = ref 0 in let c () = incr counter; !counter in @@ -74,52 +80,46 @@ let reference_of_string = i in fun s -> - try MapStringsToUri.find s !set_of_reference + try MapStringsToReference.find s !set_of_reference with Not_found -> let new_reference = try let dot = String.rindex s '.' in + let prefix = String.sub s 0 (dot+1) in let suffix = String.sub s (dot+1) 3 in + let u = NUri.uri_of_string (prefix ^ uri_suffix_of_ref_suffix suffix) in match suffix with - | "dec" -> Ref (c (), s, Decl) - | "def" -> Ref (c (), s, Def) - | "fix" -> let i,j = get2 s dot in Ref (c (), s, Fix (i,j)) - | "cfx" -> let i = get1 s dot in Ref (c (), s, CoFix (i)) - | "ind" -> let i = get1 s dot in Ref (c (), s, Ind (i)) - | "con" -> let i,j = get2 s dot in Ref (c (), s, Con (i,j)) + | "dec" -> Ref (c (), u, Decl) + | "def" -> Ref (c (), u, Def) + | "fix" -> let i,j = get2 s dot in Ref (c (), u, Fix (i,j)) + | "cfx" -> let i = get1 s dot in Ref (c (), u, CoFix (i)) + | "ind" -> let i = get1 s dot in Ref (c (), u, Ind (i)) + | "con" -> let i,j = get2 s dot in Ref (c (), u, Con (i,j)) | _ -> raise Not_found with Not_found -> raise (IllFormedReference (lazy s)) in - set_of_reference := MapStringsToUri.add s new_reference !set_of_reference; + set_of_reference := MapStringsToReference.add s new_reference !set_of_reference; new_reference ;; -let reference_of_ouri u indinfo = - let s = UriManager.string_of_uri u in +let string_of_reference (Ref (_,u,indinfo)) = + let s = NUri.string_of_uri u in let dot = String.rindex s '.' in let s2 = String.sub s 0 dot in - let ns = match indinfo with + match indinfo with | Decl -> s2 ^ ".dec" | Def -> s2 ^ ".def" | Fix (i,j) -> s2 ^ ".fix(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")" | CoFix i -> s2 ^ ".cfx(" ^ string_of_int i ^ ")" | Ind i -> s2 ^ ".ind(" ^ string_of_int i ^ ")" | Con (i,j) -> s2 ^ ".con(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")" - in reference_of_string ns ;; -let ouri_of_reference u = - let s = string_of_reference u in - let dot = String.rindex s '.' in - let prefix = String.sub s 0 dot in - let suffix = String.sub s (dot+1) 3 in - let os = - match suffix with - | "dec" - | "def" -> prefix ^ ".con" - | "ind" - | "con" -> prefix ^ ".ind" - | _ -> assert false - in - UriManager.uri_of_string os +let reference_of_ouri u indinfo = + let u = NUri.uri_of_string (UriManager.string_of_uri u) in + reference_of_string (string_of_reference (Ref (~-1,u,indinfo))) +;; + +let ouri_of_reference (Ref (_,u,_)) = + UriManager.uri_of_string (NUri.string_of_uri u) ;; diff --git a/helm/software/components/ng_kernel/nReference.mli b/helm/software/components/ng_kernel/nReference.mli index 116e30ac9..1904f99c9 100644 --- a/helm/software/components/ng_kernel/nReference.mli +++ b/helm/software/components/ng_kernel/nReference.mli @@ -33,7 +33,7 @@ type spec = | Ind of int | Con of int * int (* indtyno, constrno *) -type reference = Ref of int * string * spec +type reference = Ref of int * NUri.uri * spec val eq: reference -> reference -> bool val string_of_reference: reference -> string diff --git a/helm/software/components/ng_kernel/nUri.ml b/helm/software/components/ng_kernel/nUri.ml new file mode 100644 index 000000000..1b7d51943 --- /dev/null +++ b/helm/software/components/ng_kernel/nUri.ml @@ -0,0 +1,37 @@ +type uri = int * string (* shareno, URI *) + +let string_of_uri (_, uri) = uri;; + +module OrderedStrings = + struct + type t = string + let compare (s1 : t) (s2 : t) = compare s1 s2 + end +;; + +module MapStringsToUri = Map.Make(OrderedStrings);; + +let set_of_uri = ref MapStringsToUri.empty;; + +let uri_of_string = + let counter = ref 0 in + let c () = incr counter; !counter in +fun s -> + try MapStringsToUri.find s !set_of_uri + with Not_found -> + let new_uri = c(), s in + set_of_uri := MapStringsToUri.add s new_uri !set_of_uri; + new_uri +;; + +let eq = (==);; +let compare (n1,_) (n2,_) = n2 - n1;; + +module HT = struct + type t = uri + let equal = eq + let compare = compare + let hash (n,_) = n;; +end;; + +module UriHash = Hashtbl.Make(HT);; diff --git a/helm/software/components/ng_kernel/nUri.mli b/helm/software/components/ng_kernel/nUri.mli new file mode 100644 index 000000000..d0dcb723a --- /dev/null +++ b/helm/software/components/ng_kernel/nUri.mli @@ -0,0 +1,7 @@ +type uri + +val string_of_uri: uri -> string +val uri_of_string: string -> uri +val eq: uri -> uri -> bool + +module UriHash: Hashtbl.S with type key = uri -- 2.39.2