]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/ng_kernel/nReference.ml
added invalidate
[helm.git] / helm / software / components / ng_kernel / nReference.ml
1 (* Copyright (C) 2000, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 exception IllFormedReference of string Lazy.t
27
28 type spec = 
29  | Decl 
30  | Def
31  | Fix of int * int (* fixno, recparamno *)
32  | CoFix of int
33  | Ind of int
34  | Con of int * int (* indtyno, constrno *)
35
36 type reference = Ref of int * NUri.uri * spec
37
38 let eq = (==);;
39
40 module OrderedStrings =
41  struct
42   type t = string
43   let compare (s1 : t) (s2 : t) = compare s1 s2
44  end
45 ;;
46
47 module MapStringsToReference = Map.Make(OrderedStrings);;
48
49 let set_of_reference = ref MapStringsToReference.empty;;
50
51 (* '.' not allowed in path and foo
52  *
53  * Decl                   cic:/path/foo.dec
54  * Def                    cic:/path/foo.def
55  * Fix of int * int       cic:/path/foo.fix(i,j)
56  * CoFix of int           cic:/path/foo.cfx(i)
57  * Ind of int             cic:/path/foo.ind(i)
58  * Con of int * int       cic:/path/foo.con(i,j)
59  *)
60
61 let uri_suffix_of_ref_suffix = function
62     | "dec" | "fix" | "cfx" | "def" -> "con"
63     | "ind" | "con" -> "ind"
64     | x -> prerr_endline (x ^ " not a valid suffix"); assert false
65 ;;
66
67 let reference_of_string =
68   let counter = ref 0 in 
69   let c () = incr counter; !counter in 
70   let get2 s dot =
71     let comma = String.rindex s ',' in
72     let i = int_of_string (String.sub s (dot+5) (comma-dot-5)) in
73     let j = int_of_string (String.sub s (comma+1) (String.length s-comma-2)) in
74     i,j
75   in
76   let get1 s dot =
77     let i = int_of_string (String.sub s (dot+5) (String.length s-1-dot-5)) in
78     i
79   in
80 fun s ->
81   try MapStringsToReference.find s !set_of_reference
82   with Not_found ->
83     let new_reference =
84       try
85         let dot = String.rindex s '.' in
86         let prefix = String.sub s 0 (dot+1) in
87         let suffix = String.sub s (dot+1) 3 in
88         let u = NUri.uri_of_string (prefix ^ uri_suffix_of_ref_suffix suffix) in
89         match suffix with
90         | "dec" -> Ref (c (), u, Decl)
91         | "def" -> Ref (c (), u, Def)
92         | "fix" -> let i,j = get2 s dot in Ref (c (), u, Fix (i,j))
93         | "cfx" -> let i = get1 s dot in Ref (c (), u, CoFix (i))
94         | "ind" -> let i = get1 s dot in Ref (c (), u, Ind (i))
95         | "con" -> let i,j = get2 s dot in Ref (c (), u, Con (i,j))
96         | _ -> raise Not_found
97       with Not_found -> raise (IllFormedReference (lazy s))
98     in
99     set_of_reference := MapStringsToReference.add s new_reference !set_of_reference;
100     new_reference
101 ;;
102
103 let string_of_reference (Ref (_,u,indinfo)) =
104   let s = NUri.string_of_uri u in
105   let dot = String.rindex s '.' in
106   let s2 = String.sub s 0 dot in
107   match indinfo with
108   | Decl ->  s2 ^ ".dec"
109   | Def -> s2 ^ ".def"
110   | Fix (i,j)  -> s2 ^ ".fix(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")"
111   | CoFix i -> s2 ^ ".cfx(" ^ string_of_int i ^ ")"
112   | Ind i -> s2 ^ ".ind(" ^ string_of_int i ^ ")"
113   | Con (i,j) -> s2 ^ ".con(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")"
114 ;;
115
116 let mk_constructor j = function
117   | Ref (d, u, Ind i) -> 
118       reference_of_string (string_of_reference (Ref (d, u, Con (i,j))))
119   | _ -> assert false
120 ;;
121
122 let reference_of_ouri u indinfo =
123   let u = NUri.nuri_of_ouri u in
124   reference_of_string (string_of_reference (Ref (max_int,u,indinfo)))
125 ;;
126
127 let ouri_of_reference (Ref (_,u,_)) = NUri.ouri_of_nuri u;;
128