X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnReference.ml;h=e209d05bef8e8d3c28b13093addee5f4be070b69;hb=95adf6dc8e29a71adc34e71eafe3f427990126e0;hp=2692075e02796a5c3958e066854513d2de720059;hpb=13ea06251e64004ad537d5c71b4082af52085ff0;p=helm.git diff --git a/helm/software/components/ng_kernel/nReference.ml b/helm/software/components/ng_kernel/nReference.ml index 2692075e0..e209d05be 100644 --- a/helm/software/components/ng_kernel/nReference.ml +++ b/helm/software/components/ng_kernel/nReference.ml @@ -1,46 +1,39 @@ -(* 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 int - | 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 = (==);; +let compare (Ref (u1,s1)) (Ref (u2,s2)) = + let res = NUri.compare u1 u2 in + if res = 0 then compare s1 s2 else res +;; + module OrderedStrings = struct type t = string - let compare (s1 : t) (s2 : t) = compare s1 s2 + let compare (s1 : t) (s2 : t) = Pervasives.compare s1 s2 end ;; @@ -65,14 +58,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 +91,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 i = get1 s dot in Ref (c (), u, Ind (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,29 +104,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 i -> s2 ^ ".ind(" ^ 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)))) + | 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 (u, Fix (_,_,h)) -> + reference_of_string (string_of_reference (Ref (u, Fix (i,j,h)))) | _ -> 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 mk_cofix i = function + | Ref (u, CoFix _) -> + reference_of_string (string_of_reference (Ref (u, CoFix i))) + | _ -> assert false ;; -let ouri_of_reference (Ref (_,u,_)) = NUri.ouri_of_nuri u;; +let reference_of_spec u spec = + reference_of_string (string_of_reference (Ref (u, spec))) +;; + + +