+++ /dev/null
-(* Copyright (C) 2000-2002, 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/.
- *)
-
-(****************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
-(* Ferruccio Guidi <fguidi@cs.unibo.it> *)
-(* 15/01/2003 *)
-(* *)
-(* *)
-(****************************************************************************)
-
-exception IllFormedUri of string;;
-
-let string_of_cic_textual_parser_uri uri =
- let module C = Cic in
- let module CTP = CicTextualParser0 in
- let uri' =
- match uri with
- CTP.ConUri uri -> UriManager.string_of_uri uri
- | CTP.VarUri uri -> UriManager.string_of_uri uri
- | CTP.IndTyUri (uri,tyno) ->
- UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1)
- | CTP.IndConUri (uri,tyno,consno) ->
- UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^
- string_of_int consno
- in
- (* 4 = String.length "cic:" *)
- String.sub uri' 4 (String.length uri' - 4)
-;;
-
-let cic_textual_parser_uri_of_string uri' =
- try
- (* Constant *)
- if String.sub uri' (String.length uri' - 4) 4 = ".con" then
- CicTextualParser0.ConUri (UriManager.uri_of_string uri')
- else
- if String.sub uri' (String.length uri' - 4) 4 = ".var" then
- CicTextualParser0.VarUri (UriManager.uri_of_string uri')
- else
- (try
- (* Inductive Type *)
- let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
- CicTextualParser0.IndTyUri (uri'',typeno)
- with
- UriManager.IllFormedUri _
- | CicTextualParser0.LexerFailure _
- | Invalid_argument _ ->
- (* Constructor of an Inductive Type *)
- let uri'',typeno,consno =
- CicTextualLexer.indconuri_of_uri uri'
- in
- CicTextualParser0.IndConUri (uri'',typeno,consno)
- )
- with
- UriManager.IllFormedUri _
- | CicTextualParser0.LexerFailure _
- | Invalid_argument _ ->
- raise (IllFormedUri uri')
-;;
-
-(* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *)
-let wrong_xpointer_format_from_wrong_xpointer_format' uri =
- try
- let index_sharp = String.index uri '#' in
- let index_rest = index_sharp + 10 in
- let baseuri = String.sub uri 0 index_sharp in
- let rest =
- String.sub uri index_rest (String.length uri - index_rest - 1)
- in
- baseuri ^ "#" ^ rest
- with Not_found -> uri
-;;
-
-let term_of_cic_textual_parser_uri uri =
- let module C = Cic in
- let module CTP = CicTextualParser0 in
- match uri with
- CTP.ConUri uri -> C.Const (uri,[])
- | CTP.VarUri uri -> C.Var (uri,[])
- | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[])
- | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[])
-;;
-
-(* conversion functions *****************************************************)
-
-type uriref = UriManager.uri * (int list)
-
-let string_of_uriref (uri, fi) =
- let module UM = UriManager in
- let str = UM.string_of_uri uri in
- let xp t = "#xpointer(1/" ^ string_of_int (t + 1) in
- match fi with
- | [] -> str
- | [t] -> str ^ xp t ^ ")"
- | t :: c :: _ -> str ^ xp t ^ "/" ^ string_of_int c ^ ")"
+++ /dev/null
-(* Copyright (C) 2000-2002, 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/.
- *)
-
-(****************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
-(* Ferruccio Guidi <fguidi@cs.unibo.it> *)
-(* 15/01/2003 *)
-(* *)
-(* *)
-(****************************************************************************)
-
-exception IllFormedUri of string
-
-val string_of_cic_textual_parser_uri : CicTextualParser0.uri -> string
-val cic_textual_parser_uri_of_string : string -> CicTextualParser0.uri
-val term_of_cic_textual_parser_uri: CicTextualParser0.uri -> Cic.term
-val wrong_xpointer_format_from_wrong_xpointer_format' : string -> string
-
-type uriref = UriManager.uri * (int list)
-
-val string_of_uriref : uriref -> string
projects / helm.git / commitdiff