1 (* Copyright (C) 2000-2002, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (****************************************************************************)
30 (* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
31 (* Ferruccio Guidi <fguidi@cs.unibo.it> *)
35 (****************************************************************************)
37 exception IllFormedUri of string;;
39 let string_of_cic_textual_parser_uri uri =
41 let module CTP = CicTextualParser0 in
44 CTP.ConUri uri -> UriManager.string_of_uri uri
45 | CTP.VarUri uri -> UriManager.string_of_uri uri
46 | CTP.IndTyUri (uri,tyno) ->
47 UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1)
48 | CTP.IndConUri (uri,tyno,consno) ->
49 UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^
52 (* 4 = String.length "cic:" *)
53 String.sub uri' 4 (String.length uri' - 4)
56 let cic_textual_parser_uri_of_string uri' =
59 if String.sub uri' (String.length uri' - 4) 4 = ".con" then
60 CicTextualParser0.ConUri (UriManager.uri_of_string uri')
62 if String.sub uri' (String.length uri' - 4) 4 = ".var" then
63 CicTextualParser0.VarUri (UriManager.uri_of_string uri')
67 let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
68 CicTextualParser0.IndTyUri (uri'',typeno)
70 UriManager.IllFormedUri _
71 | CicTextualParser0.LexerFailure _
72 | Invalid_argument _ ->
73 (* Constructor of an Inductive Type *)
74 let uri'',typeno,consno =
75 CicTextualLexer.indconuri_of_uri uri'
77 CicTextualParser0.IndConUri (uri'',typeno,consno)
80 UriManager.IllFormedUri _
81 | CicTextualParser0.LexerFailure _
82 | Invalid_argument _ ->
83 raise (IllFormedUri uri')
86 (* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *)
87 let wrong_xpointer_format_from_wrong_xpointer_format' uri =
89 let index_sharp = String.index uri '#' in
90 let index_rest = index_sharp + 10 in
91 let baseuri = String.sub uri 0 index_sharp in
93 String.sub uri index_rest (String.length uri - index_rest - 1)
99 let term_of_cic_textual_parser_uri uri =
100 let module C = Cic in
101 let module CTP = CicTextualParser0 in
103 CTP.ConUri uri -> C.Const (uri,[])
104 | CTP.VarUri uri -> C.Var (uri,[])
105 | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[])
106 | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[])
109 (* conversion functions *****************************************************)
111 type uriref = UriManager.uri * (int list)
113 let string_of_uriref (uri, fi) =
114 let module UM = UriManager in
115 let str = UM.string_of_uri uri in
116 let xp t = "#xpointer(1/" ^ string_of_int (t + 1) in
119 | [t] -> str ^ xp t ^ ")"
120 | t :: c :: _ -> str ^ xp t ^ "/" ^ string_of_int c ^ ")"
122 let uriref_of_string str =
124 let i0 = String.index str '#' in
125 let u = UriManager.uri_of_string (String.sub str 0 i0) in
126 let i2 = pred (String.length str) in
129 let i1 = String.index_from str i0 '/' in
130 u, [pred (int_of_string (String.sub str i0 (i1 - i0)));
131 int_of_string (String.sub str (succ i1) (i2 - succ i1))]
133 u, [pred (int_of_string (String.sub str i0 (i2 - i0)))]
134 with Not_found -> UriManager.uri_of_string str, []
136 (* object inspection ********************************************************)
138 exception CurrentProof
140 exception InductiveDefinition
142 exception IllFormedFragment
144 let get_object (u, fi) =
146 try List.nth l i with Failure "nth" -> raise IllFormedFragment
148 match (CicEnvironment.get_obj u) with
149 | Cic.Constant (_, Some t, ty, _) -> t, ty
150 | Cic.Constant (_, None, ty, _) -> Cic.Const (u, []), ty
151 | Cic.Variable (_, Some t, ty, _) -> t, ty
152 | Cic.Variable (_, None, ty, _) -> Cic.Var (u, []), ty
153 | Cic.CurrentProof (_, me, t, ty, _) -> raise CurrentProof
154 | Cic.InductiveDefinition (tl, _, _) ->
156 | [] -> raise InductiveDefinition
158 let _, _, ty, _ = nth tl i in
159 Cic.MutInd (u, i, []), ty
161 let _, _, _, cl = nth tl i in
162 let _, ty = nth cl (pred j) in
163 Cic.MutConstruct (u, i, j, []), ty
164 | _ -> raise IllFormedFragment