From: Enrico Tassi Date: Tue, 5 Feb 2008 15:23:08 +0000 (+0000) Subject: uri -> reference (2) X-Git-Tag: make_still_working~5632 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=085cfc8bc4f775e8879a31c6de35d08aed500332;p=helm.git uri -> reference (2) --- diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend index 960471d4e..497730e2b 100644 --- a/helm/software/components/ng_kernel/.depend +++ b/helm/software/components/ng_kernel/.depend @@ -1,14 +1,12 @@ -nCicEnvironment.cmi: nUriManager.cmi nCic.cmo +nCicEnvironment.cmi: nReference.cmi nCic.cmo nCicTypeChecker.cmi: nCic.cmo oCic2NCic.cmi: nCic.cmo -nCic.cmo: nUriManager.cmi -nCic.cmx: nUriManager.cmx nCicEnvironment.cmo: oCic2NCic.cmi nCicEnvironment.cmi nCicEnvironment.cmx: oCic2NCic.cmx nCicEnvironment.cmi nCicTypeChecker.cmo: nCicTypeChecker.cmi nCicTypeChecker.cmx: nCicTypeChecker.cmi -nUriManager.cmo: nUriManager.cmi -nUriManager.cmx: nUriManager.cmi +nReference.cmo: nReference.cmi +nReference.cmx: nReference.cmi oCicTypeChecker.cmo: oCic2NCic.cmi nCicTypeChecker.cmi oCicTypeChecker.cmi oCicTypeChecker.cmx: oCic2NCic.cmx nCicTypeChecker.cmx oCicTypeChecker.cmi oCic2NCic.cmo: oCic2NCic.cmi diff --git a/helm/software/components/ng_kernel/Makefile b/helm/software/components/ng_kernel/Makefile index 143fefa1a..209170288 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 nUriManager.mli oCicTypeChecker.mli oCic2NCic.mli + nCicEnvironment.mli nCicTypeChecker.mli nReference.mli oCicTypeChecker.mli oCic2NCic.mli IMPLEMENTATION_FILES = \ nCic.ml $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml index 10d3c198d..278f7fff5 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.ml +++ b/helm/software/components/ng_kernel/nCicEnvironment.ml @@ -1,6 +1,6 @@ -let get_checked_obj nuri = - let ouri = NUriManager.ouri_of_nuri nuri in +let get_checked_obj reference = + let ouri = NReference.ouri_of_reference reference in let o,_ = CicEnvironment.get_cooked_obj ~trust:false CicUniv.oblivion_ugraph ouri diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli index d8b733dc3..20945d08d 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.mli +++ b/helm/software/components/ng_kernel/nCicEnvironment.mli @@ -26,6 +26,6 @@ (* NG: minimal wrapper on the old cicEnvironment, should provide only the * functions strictly necessary to the typechecking algorithm *) -val get_checked_obj : NUriManager.uri -> NCic.obj +val get_checked_obj : NReference.reference -> NCic.obj (* EOF *) diff --git a/helm/software/components/ng_kernel/nReference.ml b/helm/software/components/ng_kernel/nReference.ml new file mode 100644 index 000000000..bcdd4713e --- /dev/null +++ b/helm/software/components/ng_kernel/nReference.ml @@ -0,0 +1,125 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +exception IllFormedReference of string Lazy.t + +type spec = + | Decl + | Def + | Fix of int * int (* fixno, recparamno *) + | CoFix of int + | Ind of int + | Con of int * int (* indtyno, constrno *) + +type reference = Ref of int * string * spec + +let eq = (==);; + +let string_of_reference (Ref (_,s,_)) = s;; + +module OrderedStrings = + struct + type t = string + let compare (s1 : t) (s2 : t) = compare s1 s2 + end +;; + +module MapStringsToUri = Map.Make(OrderedStrings);; + +let set_of_reference = ref MapStringsToUri.empty;; + +(* '.' not allowed in path and foo + * + * Decl cic:/path/foo.dec + * Def cic:/path/foo.def + * Fix of int * int cic:/path/foo.fix(i,j) + * CoFix of int cic:/path/foo.cfx(i) + * Ind of int cic:/path/foo.ind(i) + * Con of int * int cic:/path/foo.con(i,j) + *) + +let reference_of_string = + let counter = ref 0 in + let c () = incr counter; !counter in + let get2 s dot = + let comma = String.rindex s ',' in + let i = int_of_string (String.sub s (dot+5) (comma-dot-5)) in + let j = int_of_string (String.sub s (comma+1) (String.length s-comma-2)) in + i,j + in + let get1 s dot = + let i = int_of_string (String.sub s (dot+5) (String.length s-1)) in + i + in +fun s -> + try MapStringsToUri.find s !set_of_reference + with Not_found -> + let new_reference = + try + let dot = String.rindex s '.' in + let suffix = String.sub s (dot+1) 3 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)) + | _ -> raise Not_found + with Not_found -> raise (IllFormedReference (lazy s)) + in + set_of_reference := MapStringsToUri.add s new_reference !set_of_reference; + new_reference +;; + +let reference_of_ouri u indinfo = + let s = UriManager.string_of_uri u in + let dot = String.rindex s '.' in + let s2 = String.sub s 0 dot in + let ns = 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 +;; diff --git a/helm/software/components/ng_kernel/nReference.mli b/helm/software/components/ng_kernel/nReference.mli new file mode 100644 index 000000000..116e30ac9 --- /dev/null +++ b/helm/software/components/ng_kernel/nReference.mli @@ -0,0 +1,44 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +exception IllFormedReference of string Lazy.t + +type spec = + | Decl + | Def + | Fix of int * int (* fixno, recparamno *) + | CoFix of int + | Ind of int + | Con of int * int (* indtyno, constrno *) + +type reference = Ref of int * string * spec + +val eq: reference -> reference -> bool +val string_of_reference: reference -> string + + +(* CACCA *) +val reference_of_ouri: UriManager.uri -> spec -> reference +val ouri_of_reference: reference -> UriManager.uri diff --git a/helm/software/components/ng_kernel/nUriManager.ml b/helm/software/components/ng_kernel/nUriManager.ml deleted file mode 100644 index 745f9359c..000000000 --- a/helm/software/components/ng_kernel/nUriManager.ml +++ /dev/null @@ -1,125 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -exception IllFormedReference of string Lazy.t - -type spec = - | Decl - | Def - | Fix of int * int (* fixno, recparamno *) - | CoFix of int - | Ind of int - | Con of int * int (* indtyno, constrno *) - -type reference = Ref of int * string * spec - -let eq = (==);; - -let string_of_reference (Uri (_,s,_)) = s;; - -module OrderedStrings = - struct - type t = string - let compare (s1 : t) (s2 : t) = compare s1 s2 - end -;; - -module MapStringsToUri = Map.Make(OrderedStrings);; - -let set_of_reference = ref MapStringsToUri.empty;; - -(* '.' not allowed in path and foo - * - * Decl cic:/path/foo.dec - * Def cic:/path/foo.def - * Fix of int * int cic:/path/foo.fix(i,j) - * CoFix of int cic:/path/foo.cfx(i) - * Ind of int cic:/path/foo.ind(i) - * Con of int * int cic:/path/foo.con(i,j) - *) - -let reference_of_string = - let counter = ref 0 in - let c () = incr counter; !counter in - let get2 s dot = - let comma = String.rindex s ',' in - let i = int_of_string (String.sub s (dot+5) (comma-dot-5)) in - let j = int_of_string (String.sub s (comma+1) (String.length s-comma-2)) in - i,j - in - let get1 s dot = - let i = int_of_string (String.sub s (dot+5) (String.length s-1)) in - i - in -fun s -> - try MapStringsToUri.find s !set_of_reference - with Not_found -> - let new_reference = - try - let dot = String.rindex s '.' in - let suffix = String.sub s (dot+1) 3 in - match suffix with - | "dec" -> Uri (c (), s, Decl) - | "def" -> Uri (c (), s, Def) - | "fix" -> let i,j = get2 s dot in Uri (c (), s, Fix (i,j)) - | "cfx" -> let i = get1 s dot in Uri (c (), s, CoFix (i)) - | "ind" -> let i = get1 s dot in Uri (c (), s, Ind (i)) - | "con" -> let i,j = get2 s dot in Uri (c (), s, Con (i,j)) - | _ -> raise Not_found - with Not_found -> raise (IllFormedUri (lazy s)) - in - set_of_reference := MapStringsToUri.add s new_reference !set_of_reference; - new_reference -;; - -let reference_of_ouri u indinfo = - let s = UriManager.string_of_uri u in - let dot = String.rindex s '.' in - let s2 = String.sub s 0 dot in - let ns = 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 -;; diff --git a/helm/software/components/ng_kernel/nUriManager.mli b/helm/software/components/ng_kernel/nUriManager.mli deleted file mode 100644 index 116e30ac9..000000000 --- a/helm/software/components/ng_kernel/nUriManager.mli +++ /dev/null @@ -1,44 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -exception IllFormedReference of string Lazy.t - -type spec = - | Decl - | Def - | Fix of int * int (* fixno, recparamno *) - | CoFix of int - | Ind of int - | Con of int * int (* indtyno, constrno *) - -type reference = Ref of int * string * spec - -val eq: reference -> reference -> bool -val string_of_reference: reference -> string - - -(* CACCA *) -val reference_of_ouri: UriManager.uri -> spec -> reference -val ouri_of_reference: reference -> UriManager.uri