From e2fb8962f72096d3f0bb19f40b00a3502a11e932 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 24 Jun 2005 07:40:39 +0000 Subject: [PATCH] New functions UriManager.uri_is_var, UriManager.uri_is_con. --- helm/matita/matitaGui.ml | 8 +------- helm/ocaml/cic/cicUtil.ml | 4 ++-- helm/ocaml/cic/helmLibraryObjects.ml | 25 ------------------------- helm/ocaml/tactics/metadataQuery.ml | 6 +----- helm/ocaml/tactics/tacticChaser.ml | 6 +----- helm/ocaml/urimanager/uriManager.ml | 18 ++++++------------ helm/ocaml/urimanager/uriManager.mli | 1 + 7 files changed, 12 insertions(+), 56 deletions(-) diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 8915f7681..34cf20afa 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -401,12 +401,6 @@ let instance = singleton gui let non p x = not (p x) -let is_var_uri s = - let s = UriManager.string_of_uri s in - try - String.sub s (String.length s - 4) 4 = ".var" - with Invalid_argument _ -> false - (* this is a shit and should be changed :-{ *) let interactive_uri_choice ?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "") @@ -416,7 +410,7 @@ let interactive_uri_choice ~id uris = let gui = instance () in - let nonvars_uris = lazy (List.filter (non is_var_uri) uris) in + let nonvars_uris = lazy (List.filter (non UriManager.uri_is_var) uris) in if (selection_mode <> `SINGLE) && (Helm_registry.get_bool "matita.auto_disambiguation") then diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml index 81055e681..149a9bc2e 100644 --- a/helm/ocaml/cic/cicUtil.ml +++ b/helm/ocaml/cic/cicUtil.ml @@ -141,9 +141,9 @@ let slash_RE = Str.regexp "/" let term_of_uri uri = let s = UriManager.string_of_uri uri in try - (if String.sub s (String.length s - 4) 4 = ".con" then + (if UriManager.uri_is_con uri then Cic.Const (uri, []) - else if String.sub s (String.length s - 4) 4 = ".var" then + else if UriManager.uri_is_var uri then Cic.Var (uri, []) else if not (Str.string_match xpointer_RE s 0) then raise (UriManager.IllFormedUri s) diff --git a/helm/ocaml/cic/helmLibraryObjects.ml b/helm/ocaml/cic/helmLibraryObjects.ml index 6ebdf8e1f..defc33f6c 100644 --- a/helm/ocaml/cic/helmLibraryObjects.ml +++ b/helm/ocaml/cic/helmLibraryObjects.ml @@ -24,31 +24,6 @@ let indconuri_of_uri uri = int_of_string (String.sub uri index_con (String.length uri - index_con))) -(* (* NO LONGER USED, see CicUtil.term_of_uri *) -let term_of_uri ?(subst = []) uri = - let s = UriManager.string_of_uri uri in - try - (* Constant *) - let len = String.length s in - let sub = String.sub s (len -4) 4 in - if sub = ".con" then - const ~subst uri - else if sub = ".var" then - var ~subst uri - else - (try - (* Inductive Type *) - let (uri, typeno) = indtyuri_of_uri s in - mutind ~subst uri typeno - with - | UriManager.IllFormedUri _ | Failure _ | Invalid_argument _ -> - (* Constructor of an Inductive Type *) - let (uri, typeno, consno) = indconuri_of_uri s in - mutconstruct ~subst uri typeno consno) - with - | Invalid_argument _ | Not_found -> raise (UriManager.IllFormedUri s) -*) - (** {2 Helm's objects shorthands} *) module Logic = diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index c1dd20ecc..ed4418dd2 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -43,11 +43,7 @@ let sqlpat_of_shellglob = (Pcre.replace ~rex:uscore_RE ~templ:"\\_" shellglob))) -let nonvar s = - let s = UriManager.string_of_uri s in - let len = String.length s in - let suffix = String.sub s (len-4) 4 in - not (suffix = ".var") +let nonvar uri = not (UriManager.uri_is_var uri) let locate ~(dbd:Mysql.dbd) ?(vars = false) pat = let sql_pat = sqlpat_of_shellglob pat in diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml index 2d1b0dcfd..de356a3d1 100644 --- a/helm/ocaml/tactics/tacticChaser.ml +++ b/helm/ocaml/tactics/tacticChaser.ml @@ -125,11 +125,7 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st (* List.iter (fun (n,u) -> prerr_endline ((string_of_int n) ^ " " ^u)) uris; *) (* delete all .var uris *) - let isvar (_,s) = - let len = String.length s in - let suffix = String.sub s (len-4) 4 in - not (suffix = ".var") in - let uris = List.filter isvar uris in + let uris = List.filter UriManager.is_var uris in (* delete all not "cic:/Coq" uris *) (* let uris = diff --git a/helm/ocaml/urimanager/uriManager.ml b/helm/ocaml/urimanager/uriManager.ml index 4c489a9fd..f701125ed 100644 --- a/helm/ocaml/urimanager/uriManager.ml +++ b/helm/ocaml/urimanager/uriManager.ml @@ -122,21 +122,15 @@ let _dotbody = ".body" let _con = "con" let _xpointer = "#xpointer(1/" -let cicuri_of_uri (uri, _) = - uri_of_string (clear_suffix uri ~pat2:_types _ann) -;; +let cicuri_of_uri (uri, _) = uri_of_string (clear_suffix uri ~pat2:_types _ann) -let annuri_of_uri (uri , _) = - uri_of_string ((clear_suffix uri _ann) ^ _dotann) -;; +let annuri_of_uri (uri , _) = uri_of_string ((clear_suffix uri _ann) ^ _dotann) -let uri_is_annuri (uri, _) = - has_suffix uri _ann -;; +let uri_is_annuri (uri, _) = has_suffix uri _ann -let uri_is_var (uri, _) = - has_suffix uri _var -;; +let uri_is_var (uri, _) = has_suffix uri _var + +let uri_is_con (uri, _) = has_suffix uri _con let bodyuri_of_uri (uri, _) = if has_suffix uri _con then diff --git a/helm/ocaml/urimanager/uriManager.mli b/helm/ocaml/urimanager/uriManager.mli index 27bf862b8..bed9db29e 100644 --- a/helm/ocaml/urimanager/uriManager.mli +++ b/helm/ocaml/urimanager/uriManager.mli @@ -48,6 +48,7 @@ val annuri_of_uri : uri -> uri val uri_is_annuri : uri -> bool val uri_is_var : uri -> bool +val uri_is_con : uri -> bool (* given an uri of a constant, it gives back the uri of its body *) (* it gives back None if the uri refers to a Variable or MutualInductiveType *) -- 2.39.2