X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnReference.ml;h=be6760bf19e3702bf7da7d204b3a066b8a6313a1;hb=46b91f34b693dabbd351ba813f5190051b09a117;hp=81a08af4e6bc3037ce24ebc2dac8290c9163af23;hpb=7f5d0adf3d44aa3e52e882dbe5f42358b8ee96cf;p=helm.git diff --git a/helm/software/components/ng_kernel/nReference.ml b/helm/software/components/ng_kernel/nReference.ml index 81a08af4e..be6760bf1 100644 --- a/helm/software/components/ng_kernel/nReference.ml +++ b/helm/software/components/ng_kernel/nReference.ml @@ -1,39 +1,27 @@ -(* 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/. - *) +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id$ *) exception IllFormedReference of string Lazy.t type spec = | Decl - | Def - | Fix of int * int (* fixno, recparamno *) + | Def of int (* height *) + | Fix of int * int * int (* fixno, recparamno, height *) | CoFix of int - | Ind of bool * int (* inductive, indtyno *) - | Con of int * int (* indtyno, constrno *) + | Ind of bool * int * int (* inductive, indtyno, leftno *) + | Con of int * int * int (* indtyno, constrno, leftno *) -type reference = Ref of int * NUri.uri * spec +type reference = Ref of NUri.uri * spec let eq = (==);; @@ -65,14 +53,25 @@ let uri_suffix_of_ref_suffix = function ;; let reference_of_string = - let counter = ref 0 in - let c () = incr counter; !counter in + let get3 s dot = + let comma2 = String.rindex s ',' in + let comma = String.rindex_from s (comma2-1) ',' in + let s_i = String.sub s (dot+5) (comma-dot-5) in + let s_j = String.sub s (comma+1) (comma2-comma-1) in + let s_h = String.sub s (comma2+1) (String.length s-comma2-2) in + let i = int_of_string s_i in + let j = int_of_string s_j in + let h = int_of_string s_h in + i,j,h + 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-dot-5)) in i @@ -87,12 +86,12 @@ fun s -> 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 (), 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 b,i = get2 s dot in Ref (c (), u, Ind (b=1,i)) - | "con" -> let i,j = get2 s dot in Ref (c (), u, Con (i,j)) + | "dec" -> Ref (u, Decl) + | "def" -> let i = get1 s dot in Ref (u, Def i) + | "fix" -> let i,j,h = get3 s dot in Ref (u, Fix (i,j,h)) + | "cfx" -> let i = get1 s dot in Ref (u, CoFix (i)) + | "ind" -> let b,i,l = get3 s dot in Ref (u, Ind (b=1,i,l)) + | "con" -> let i,j,l = get3 s dot in Ref (u, Con (i,j,l)) | _ -> raise Not_found with Not_found -> raise (IllFormedReference (lazy s)) in @@ -100,41 +99,54 @@ fun s -> new_reference ;; -let string_of_reference (Ref (_,u,indinfo)) = +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 match indinfo with | Decl -> s2 ^ ".dec" - | Def -> s2 ^ ".def" - | Fix (i,j) -> s2 ^ ".fix(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")" + | Def h -> s2 ^ ".def(" ^ string_of_int h ^ ")" + | Fix (i,j,h) -> + s2 ^ ".fix(" ^ string_of_int i ^ "," ^ + string_of_int j ^ "," ^ string_of_int h ^ ")" | CoFix i -> s2 ^ ".cfx(" ^ string_of_int i ^ ")" - | Ind (b,i)->s2 ^".ind(" ^(if b then "1" else "0")^ "," ^ string_of_int i ^")" - | Con (i,j) -> s2 ^ ".con(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")" + | Ind (b,i,l)->s2 ^".ind(" ^(if b then "1" else "0")^ "," ^ string_of_int i ^ + "," ^ string_of_int l ^ ")" + | Con (i,j,l) -> s2 ^ ".con(" ^ string_of_int i ^ "," ^ string_of_int j ^ + "," ^ string_of_int l ^ ")" ;; let mk_constructor j = function - | Ref (d, u, Ind (_,i)) -> - reference_of_string (string_of_reference (Ref (d, u, Con (i,j)))) - | _ -> assert false + | Ref (u, Ind (_,i,l)) -> + reference_of_string (string_of_reference (Ref (u, Con (i,j,l)))) + | r -> + raise (IllFormedReference (lazy ("NON INDUCTIVE TYPE REFERENCE: " ^ + string_of_reference r))); +;; +let mk_indty b = function + | Ref (u, Con (i,_,l)) -> + reference_of_string (string_of_reference (Ref (u, Ind (b,i,l)))) + | r -> + raise (IllFormedReference (lazy + ("NON INDUCTIVE TYPE CONSTRUCTOR REFERENCE: " ^ string_of_reference r))); ;; let mk_fix i j = function - | Ref (d, u, Fix _) -> - reference_of_string (string_of_reference (Ref (d, u, Fix (i,j)))) + | Ref (u, Fix (_,_,h)) -> + reference_of_string (string_of_reference (Ref (u, Fix (i,j,h)))) | _ -> assert false ;; let mk_cofix i = function - | Ref (d, u, CoFix _) -> - reference_of_string (string_of_reference (Ref (d, u, CoFix i))) + | Ref (u, CoFix _) -> + reference_of_string (string_of_reference (Ref (u, CoFix i))) | _ -> assert false ;; -let reference_of_ouri u indinfo = - let u = NUri.nuri_of_ouri u in - reference_of_string (string_of_reference (Ref (max_int,u,indinfo))) +let reference_of_spec u spec = + reference_of_string (string_of_reference (Ref (u, spec))) ;; -let ouri_of_reference (Ref (_,u,_)) = NUri.ouri_of_nuri u;; + +