2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
14 exception IllFormedReference of string Lazy.t
18 | Def of int (* height *)
19 | Fix of int * int * int (* fixno, recparamno, height *)
21 | Ind of bool * int * int (* inductive, indtyno, leftno *)
22 | Con of int * int * int (* indtyno, constrno, leftno *)
24 type reference = Ref of NUri.uri * spec
28 let compare (Ref (u1,s1)) (Ref (u2,s2)) =
29 let res = NUri.compare u1 u2 in
30 if res = 0 then compare s1 s2 else res
33 let hash (Ref (uri,spec)) =
34 Hashtbl.hash spec + NUri.hash uri
37 module OrderedStrings =
40 let compare (s1 : t) (s2 : t) = Pervasives.compare s1 s2
44 module MapStringsToReference = Map.Make(OrderedStrings);;
46 let set_of_reference = ref MapStringsToReference.empty;;
48 (* Note: valid ELPI constant
49 * '#' not allowed in path and name
51 * Decl cic:/path/name#dec
52 * Def cic:/path/name#def:i
53 * Fix of int * int cic:/path/name#fix:i:j:h
54 * CoFix of int cic:/path/name#cfx:i
55 * Ind of int cic:/path/name#ind:b:i:l
56 * Con of int * int cic:/path/name#con:i:j:l
59 let uri_suffix_of_ref_suffix = function
60 | "dec" | "fix" | "cfx" | "def" -> "con"
61 | "ind" | "con" -> "ind"
62 | x -> prerr_endline (x ^ " not a valid suffix"); assert false
65 let reference_of_string =
67 let comma2 = String.rindex s ':' in
68 let comma = String.rindex_from s (comma2-1) ':' in
69 let s_i = String.sub s (dot+5) (comma-dot-5) in
70 let s_j = String.sub s (comma+1) (comma2-comma-1) in
71 let s_h = String.sub s (comma2+1) (String.length s-comma2-1) in
72 let i = int_of_string s_i in
73 let j = int_of_string s_j in
74 let h = int_of_string s_h in
79 let comma = String.rindex s ':' in
80 let i = int_of_string (String.sub s (dot+5) (comma-dot-5)) in
81 let j = int_of_string (String.sub s (comma+1) (String.length s-comma-1)) in
86 let i = int_of_string (String.sub s (dot+5) (String.length s-dot-5)) in
90 try MapStringsToReference.find s !set_of_reference
94 let dot = String.rindex s '#' in
95 let prefix = String.sub s 0 dot in
96 let suffix = String.sub s (dot+1) 3 in
97 let u = NUri.uri_of_string (prefix ^ "." ^ uri_suffix_of_ref_suffix suffix) in
99 | "dec" -> Ref (u, Decl)
100 | "def" -> let i = get1 s dot in Ref (u, Def i)
101 | "fix" -> let i,j,h = get3 s dot in Ref (u, Fix (i,j,h))
102 | "cfx" -> let i = get1 s dot in Ref (u, CoFix (i))
103 | "ind" -> let b,i,l = get3 s dot in Ref (u, Ind (b=1,i,l))
104 | "con" -> let i,j,l = get3 s dot in Ref (u, Con (i,j,l))
105 | _ -> raise Not_found
106 with Not_found -> raise (IllFormedReference (lazy s))
108 set_of_reference := MapStringsToReference.add s new_reference !set_of_reference;
112 let string_of_reference (Ref (u,indinfo)) =
113 let s = NUri.string_of_uri u in
114 let dot = String.rindex s '.' in
115 let s2 = String.sub s 0 dot in
117 | Decl -> s2 ^ "#dec"
118 | Def h -> s2 ^ "#def:" ^ string_of_int h
120 s2 ^ "#fix:" ^ string_of_int i ^ ":" ^
121 string_of_int j ^ ":" ^ string_of_int h
122 | CoFix i -> s2 ^ "#cfx:" ^ string_of_int i
123 | Ind (b,i,l)->s2 ^"#ind:" ^(if b then "1" else "0")^ ":" ^ string_of_int i ^
124 ":" ^ string_of_int l
125 | Con (i,j,l) -> s2 ^ "#con:" ^ string_of_int i ^ ":" ^ string_of_int j ^
126 ":" ^ string_of_int l
129 let mk_constructor j = function
130 | Ref (u, Ind (_,i,l)) ->
131 reference_of_string (string_of_reference (Ref (u, Con (i,j,l))))
133 raise (IllFormedReference (lazy ("NON INDUCTIVE TYPE REFERENCE: " ^
134 string_of_reference r)));
136 let mk_indty b = function
137 | Ref (u, Con (i,_,l)) ->
138 reference_of_string (string_of_reference (Ref (u, Ind (b,i,l))))
140 raise (IllFormedReference (lazy
141 ("NON INDUCTIVE TYPE CONSTRUCTOR REFERENCE: " ^ string_of_reference r)));
144 let mk_fix i j = function
145 | Ref (u, Fix (_,_,h)) ->
146 reference_of_string (string_of_reference (Ref (u, Fix (i,j,h))))
150 let mk_cofix i = function
151 | Ref (u, CoFix _) ->
152 reference_of_string (string_of_reference (Ref (u, CoFix i)))
156 let reference_of_spec u spec =
157 reference_of_string (string_of_reference (Ref (u, spec)))