--- /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 ^ ")"
+
+let uriref_of_string str =
+ try
+ let i0 = String.index str '#' in
+ let u = UriManager.uri_of_string (String.sub str 0 i0) in
+ let i2 = pred (String.length str) in
+ let i0 = i0 + 12 in
+ try
+ let i1 = String.index_from str i0 '/' in
+ u, [pred (int_of_string (String.sub str i0 (i1 - i0)));
+ int_of_string (String.sub str (succ i1) (i2 - succ i1))]
+ with Not_found ->
+ u, [pred (int_of_string (String.sub str i0 (i2 - i0)))]
+ with Not_found -> UriManager.uri_of_string str, []
+
+(* object inspection ********************************************************)
+
+exception CurrentProof
+
+exception InductiveDefinition
+
+exception IllFormedFragment
+
+let get_object (u, fi) =
+ let nth l i =
+ try List.nth l i with Failure "nth" -> raise IllFormedFragment
+ in
+ match (CicEnvironment.get_obj u) with
+ | Cic.Constant (_, Some t, ty, _) -> t, ty
+ | Cic.Constant (_, None, ty, _) -> Cic.Const (u, []), ty
+ | Cic.Variable (_, Some t, ty, _) -> t, ty
+ | Cic.Variable (_, None, ty, _) -> Cic.Var (u, []), ty
+ | Cic.CurrentProof (_, me, t, ty, _) -> raise CurrentProof
+ | Cic.InductiveDefinition (tl, _, _) ->
+ match fi with
+ | [] -> raise InductiveDefinition
+ | [i] ->
+ let _, _, ty, _ = nth tl i in
+ Cic.MutInd (u, i, []), ty
+ | [i; j] ->
+ let _, _, _, cl = nth tl i in
+ let _, ty = nth cl (pred j) in
+ Cic.MutConstruct (u, i, j, []), ty
+ | _ -> raise IllFormedFragment
projects / helm.git / blobdiff