From a458a3e72fd374b106481a7e98f4000369c6ae61 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 23 Jun 2005 17:05:01 +0000 Subject: [PATCH] Much simpler (and slightly more performant) implementation of the UriManager. --- helm/matita/matitaScript.ml | 2 +- helm/matita/matitaSync.ml | 7 +- helm/ocaml/metadata/metadataConstraints.ml | 60 +++--- helm/ocaml/metadata/metadataExtractor.ml | 11 +- helm/ocaml/tactics/autoTactic.ml | 7 +- helm/ocaml/urimanager/uriManager.ml | 235 ++++++++------------- helm/ocaml/urimanager/uriManager.mli | 17 +- 7 files changed, 139 insertions(+), 200 deletions(-) diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index c7859a7c7..1f8add6a0 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -169,7 +169,7 @@ let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text let term = disambiguate term status in let uri = match term with - | Cic.MutInd (uri,n,_) -> UriManager.uri_of_string (UriManager.string_of_uriref (uri,[n])) + | Cic.MutInd (uri,n,_) -> UriManager.uri_of_uriref uri n None | _ -> failwith "Not a MutInd" in let l = MQ.elim ~dbd uri in diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index 472ab3a92..df29edc3b 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -32,12 +32,13 @@ open MatitaTypes let extract_alias types uri = fst(List.fold_left ( fun (acc,i) (name, _, _, cl) -> - ((name, UriManager.string_of_uriref (uri,[i])) + (name, UriManager.string_of_uri (UriManager.uri_of_uriref uri i None)) :: (fst(List.fold_left ( fun (acc,j) (name,_) -> - (((name,UriManager.string_of_uriref (uri,[i;j])) :: acc) , j+1) - ) (acc,1) cl))),i+1 + (((name,UriManager.string_of_uri (UriManager.uri_of_uriref uri i + (Some j))) :: acc) , j+1) + ) (acc,1) cl)),i+1 ) ([],0) types) let env_of_list l env = diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml index fb2a49424..602ee49b9 100644 --- a/helm/ocaml/metadata/metadataConstraints.ml +++ b/helm/ocaml/metadata/metadataConstraints.ml @@ -214,9 +214,6 @@ let merge n a b = in filter_by_card n res -let string_of_uriref i = - UriManager.uri_of_string (UriManager.string_of_uriref i) - let rec inspect_children n childs = List.fold_left (fun res term -> merge n (inspect_conclusion n term) res) @@ -242,10 +239,10 @@ and inspect_conclusion n t = SetSet.singleton (UriManagerSet.singleton u) | Cic.MutInd (u, t, exp_named_subst) -> SetSet.singleton (UriManagerSet.singleton - (string_of_uriref (u, [t]))) + (UriManager.uri_of_uriref u t None)) | Cic.MutConstruct (u, t, c, exp_named_subst) -> SetSet.singleton (UriManagerSet.singleton - (string_of_uriref (u, [t; c]))) + (UriManager.uri_of_uriref u t (Some c))) | Cic.Cast (t, _) -> inspect_conclusion n t | Cic.Prod (_, s, t) -> merge n (inspect_conclusion n s) (inspect_conclusion n t) @@ -254,13 +251,12 @@ and inspect_conclusion n t = | Cic.LetIn (_, s, t) -> merge n (inspect_conclusion n s) (inspect_conclusion n t) | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) -> - let suri = u in - add_root (n-1) suri l + add_root (n-1) u l | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) -> - let suri = string_of_uriref (u, [t]) in - add_root (n-1) suri l + let uri = UriManager.uri_of_uriref u t None in + add_root (n-1) uri l | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) -> - let suri = string_of_uriref (u, [t; c]) in + let suri = UriManager.uri_of_uriref u t (Some c) in add_root (n-1) suri l | Cic.Appl l -> SetSet.empty @@ -284,35 +280,33 @@ let rec inspect_term n t = | Cic.Const (u,exp_named_subst) -> Some u, SetSet.empty | Cic.MutInd (u, t, exp_named_subst) -> - let uri = string_of_uriref (u, [t]) in + let uri = UriManager.uri_of_uriref u t None in Some uri, SetSet.empty | Cic.MutConstruct (u, t, c, exp_named_subst) -> - let uri = string_of_uriref (u, [t; c]) in + let uri = UriManager.uri_of_uriref u t (Some c) in Some uri, SetSet.empty | Cic.Cast (t, _) -> inspect_term n t | Cic.Prod (_, _, t) -> inspect_term n t | Cic.LetIn (_, _, t) -> inspect_term n t | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) -> - let suri = u in let childunion = inspect_children (n-1) l in - Some suri, childunion + Some u, childunion | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) -> - let suri = string_of_uriref (u, [t]) in + let suri = UriManager.uri_of_uriref u t None in if u = HelmLibraryObjects.Logic.eq_URI && n>1 then (* equality is handled in a special way: in particular, the type, if defined, is always added to the prefix, and n is not decremented - it should have been n-2 *) match l with Cic.Const (u1,exp_named_subst1)::l1 -> - let suri1 = u1 in - let inconcl = add_root (n-1) suri1 l1 in + let inconcl = add_root (n-1) u1 l1 in Some suri, inconcl | Cic.MutInd (u1, t1, exp_named_subst1)::l1 -> - let suri1 = string_of_uriref (u1, [t1]) in + let suri1 = UriManager.uri_of_uriref u1 t1 None in let inconcl = add_root (n-1) suri1 l1 in Some suri, inconcl | Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 -> - let suri1 = string_of_uriref (u1, [t1; c1]) in + let suri1 = UriManager.uri_of_uriref u1 t1 (Some c1) in let inconcl = add_root (n-1) suri1 l1 in Some suri, inconcl | _ :: _ -> Some suri, SetSet.empty @@ -321,7 +315,7 @@ let rec inspect_term n t = let childunion = inspect_children (n-1) l in Some suri, childunion | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) -> - let suri = string_of_uriref (u, [t; c]) in + let suri = UriManager.uri_of_uriref u t(Some c) in let childunion = inspect_children (n-1) l in Some suri, childunion | _ -> None, SetSet.empty @@ -360,10 +354,10 @@ and signature_concl = | Cic.Const (u,exp_named_subst) -> UriManagerSet.singleton u | Cic.MutInd (u, t, exp_named_subst) -> - let uri = string_of_uriref (u, [t]) in + let uri = UriManager.uri_of_uriref u t None in UriManagerSet.singleton uri | Cic.MutConstruct (u, t, c, exp_named_subst) -> - let uri = string_of_uriref (u, [t;c]) in + let uri = UriManager.uri_of_uriref u t (Some c) in UriManagerSet.singleton uri | Cic.Cast (t, _) -> signature_concl t | Cic.Prod (_, s, t) -> @@ -383,25 +377,23 @@ let rec signature_of = function | Cic.Prod (_, _, t) -> signature_of t | Cic.LetIn (_, _, t) -> signature_of t | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) -> - let suri = u in - Some (suri, []), add l + Some (u, []), add l | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) -> - let suri = string_of_uriref (u, [t]) in + let suri = UriManager.uri_of_uriref u t None in if u = HelmLibraryObjects.Logic.eq_URI then (* equality is handled in a special way: in particular, the type, if defined, is always added to the prefix, and n is not decremented - it should have been n-2 *) match l with Cic.Const (u1,exp_named_subst1)::l1 -> - let suri1 = u1 in - let inconcl = UriManagerSet.remove suri1 (add l1) in - Some (suri, [suri1]), inconcl + let inconcl = UriManagerSet.remove u1 (add l1) in + Some (suri, [u1]), inconcl | Cic.MutInd (u1, t1, exp_named_subst1)::l1 -> - let suri1 = string_of_uriref (u1, [t1]) in + let suri1 = UriManager.uri_of_uriref u1 t1 None in let inconcl = UriManagerSet.remove suri1 (add l1) in Some (suri, [suri1]), inconcl | Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 -> - let suri1 = string_of_uriref (u1, [t1;c1]) in + let suri1 = UriManager.uri_of_uriref u1 t1 (Some c1) in let inconcl = UriManagerSet.remove suri1 (add l1) in Some (suri, [suri1]), inconcl | _ :: _ -> Some (suri, []), UriManagerSet.empty @@ -409,7 +401,7 @@ let rec signature_of = function else Some (suri, []), add l | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) -> - let suri = string_of_uriref (u, [t;c]) in + let suri = UriManager.uri_of_uriref u t (Some c) in Some (suri, []), add l | t -> None, signature_concl t @@ -429,7 +421,7 @@ let must_of_prefix ?(where = `Conclusion) m s = | `Conclusion -> [`InConclusion] | `Statement -> [`InConclusion; `InHypothesis; `MainHypothesis None] in - let s' = List.map (fun u -> `Obj (u, positions)) s in + let s' = List.map (fun (u:UriManager.uri) -> `Obj (u, positions)) s in `Obj (m, [`MainConclusion None]) :: s' let escape = Str.global_replace (Str.regexp_string "\'") "\\'" @@ -474,7 +466,7 @@ let myspeciallist_of_facts = [0,UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"] let myspeciallist = [0,UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"; - (* 0,UriManager.uri_of_string "cic:/Coq/Init/Logic/sym_eq.con"; *) + (* 0,"cic:/Coq/Init/Logic/sym_eq.con"; *) 0,UriManager.uri_of_string "cic:/Coq/Init/Logic/trans_eq.con"; 0,UriManager.uri_of_string "cic:/Coq/Init/Logic/f_equal.con"; 0,UriManager.uri_of_string "cic:/Coq/Init/Logic/f_equal2.con"; @@ -485,7 +477,7 @@ let compute_exactly ~(dbd:Mysql.dbd) ?(facts=false) ~where main prefixes = List.concat (List.map (fun (m,s) -> - if ((m = 0) && (main = UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI)) then + if ((m = 0) && (UriManager.eq main (UriManager.uri_of_string (HelmLibraryObjects.Logic.eq_XURI)))) then (if facts then myspeciallist_of_facts else myspeciallist) else diff --git a/helm/ocaml/metadata/metadataExtractor.ml b/helm/ocaml/metadata/metadataExtractor.ml index 5a7522b90..50407ac7c 100644 --- a/helm/ocaml/metadata/metadataExtractor.ml +++ b/helm/ocaml/metadata/metadataExtractor.ml @@ -72,9 +72,6 @@ let var_has_body uri = | Cic.Variable (_, Some body, _, _, _), _ -> true | _ -> false -let string_of_uriref s = - UriManager.uri_of_string (UriManager.string_of_uriref s) - let compute_term pos term = let rec aux (pos: position) set = function | Cic.Var (uri, subst) when var_has_body uri -> @@ -138,12 +135,12 @@ let compute_term pos term = (fun set (_, term) -> aux (next_pos pos) set term) set subst | Cic.MutInd (uri, typeno, subst) -> - let uri = string_of_uriref (uri, [typeno]) in + let uri = UriManager.uri_of_uriref uri typeno None in let set = S.add (`Obj (uri, pos)) set in List.fold_left (fun set (_, term) -> aux (next_pos pos) set term) set subst | Cic.MutConstruct (uri, typeno, consno, subst) -> - let uri = string_of_uriref (uri, [typeno; consno]) in + let uri = UriManager.uri_of_uriref uri typeno (Some consno) in let set = S.add (`Obj (uri, pos)) set in List.fold_left (fun set (_, term) -> aux (next_pos pos) set term) set subst @@ -244,13 +241,13 @@ let compute_metas term = let compute_type pos uri typeno (name, _, ty, constructors) = let consno = ref 0 in let type_metadata = - (string_of_uriref (uri, [typeno]), name, (compute_term pos ty)) + (UriManager.uri_of_uriref uri typeno None, name, (compute_term pos ty)) in let constructors_metadata = List.map (fun (name, term) -> incr consno; - let uri = string_of_uriref (uri, [typeno; !consno]) in + let uri = UriManager.uri_of_uriref uri typeno (Some !consno) in (uri, name, (compute_term pos term))) constructors in diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml index c2407ee73..13dac415f 100644 --- a/helm/ocaml/tactics/autoTactic.ml +++ b/helm/ocaml/tactics/autoTactic.ml @@ -27,6 +27,11 @@ (* let debug_print = fun _ -> () *) +let experimental_hint = + let profile = CicUtil.profile "experimental_hint" in + fun ~dbd ~facts ?signature status -> + profile (MetadataQuery.experimental_hint ~dbd ~facts ?signature) status + let search_theorems_in_context status = let (proof, goal) = status in let module C = Cic in @@ -291,7 +296,7 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals new_search_theorems (fun status -> List.map snd - (MetadataQuery.experimental_hint + (experimental_hint ~dbd ~facts:facts ?signature:sign status)) dbd proof goal (depth-1) new_sign in let all_choices = diff --git a/helm/ocaml/urimanager/uriManager.ml b/helm/ocaml/urimanager/uriManager.ml index 4eae6799d..8fe8beaa4 100644 --- a/helm/ocaml/urimanager/uriManager.ml +++ b/helm/ocaml/urimanager/uriManager.ml @@ -24,12 +24,10 @@ *) (* -* "cic:/a/b/c.con" => [| "cic:/a" ; "cic:/a/b" ; "cic:/a/b/c.con" ; "c"; "" |] -* "cic:/a/b/c.ind#xpointer(1/1)" => -* [| "cic:/a" ; "cic:/a/b" ; "cic:/a/b/c.con" ; "c"; "#xpointer(1/1)" |] -* "cic:/a/b/c.ind#xpointer(1/1/1)" => -* [| "cic:/a" ; "cic:/a/b" ; "cic:/a/b/c.con" ; "c"; "#xpointer(1/1/1)" |] -*) + * "cic:/a/b/c.con" => ("cic:/a/b/c.con", id ) + * "cic:/a/b/c.ind#xpointer(1/1)" => ("cic:/a/b/c.con#xpointer(1/1)", id) + * "cic:/a/b/c.ind#xpointer(1/1/1)" => ("cic:/a/b/c.con#xpointer(1/1/1)", id) + *) let fresh_id = let id = ref 0 in @@ -37,23 +35,28 @@ let fresh_id = incr id; !id -type uri = string array * int;; +(* (uriwithxpointer, uniqueid) + * where uniqueid is used to build a set of uri *) +type uri = string * int;; let eq uri1 uri2 = uri1 == uri2 ;; let string_of_uri (uri,_) = - match uri.(Array.length uri - 1) with - | "" -> - uri.(Array.length uri - 3) - | _ -> - String.concat "#" - [ uri.(Array.length uri - 3); uri.(Array.length uri - 1) ] + uri -let name_of_uri (uri,_) = uri.(Array.length uri - 2);; -let buri_of_uri (uri,_) = uri.(Array.length uri - 4);; -let depth_of_uri (uri,_) = Array.length uri - 3;; +let name_of_uri (uri, _) = + let xpointer_offset = + try String.rindex uri '#' with Not_found -> String.length uri - 1 + in + let index1 = String.rindex_from uri xpointer_offset '/' + 1 in + let index2 = String.rindex uri '.' in + String.sub uri index1 (index2 - index1) + +let buri_of_uri (uri,_) = + let index = String.rindex uri '/' in + String.sub uri 0 index module OrderedStrings = struct @@ -62,151 +65,99 @@ module OrderedStrings = end ;; -module SetOfStrings = Map.Make(OrderedStrings);; +module MapStringsToUri = Map.Make(OrderedStrings);; -(*CSC: commento obsoleto ed errato *) -(* Invariant: the map is the identity function, *) -(* i.e. (SetOfStrings.find str !set_of_uri) == str *) -let set_of_uri = ref SetOfStrings.empty;; -let set_of_prefixes = ref SetOfStrings.empty;; +(* Invariant: the map is the identity function, + * i.e. + * let str' = (MapStringsToUri.find str !set_of_uri) in + * str' == (MapStringsToUri.find str' !set_of_uri) + *) +let set_of_uri = ref MapStringsToUri.empty;; - (* hash conses an uri *) -let add_to_uriset ?suri uri = - let lookup_suri suri = - try - SetOfStrings.find suri !set_of_uri - with Not_found -> assert false - in - let suri = - match suri with - | None -> string_of_uri uri - | Some suri -> suri - in - if not(SetOfStrings.mem suri !set_of_uri) then - set_of_uri := SetOfStrings.add suri uri !set_of_uri; - lookup_suri suri - - -(* similar to uri_of_string, but used for prefixes of uris *) -let normalize prefix = - try - SetOfStrings.find prefix !set_of_prefixes - with - Not_found -> - set_of_prefixes := SetOfStrings.add prefix prefix !set_of_prefixes ; - prefix -;; +let uri_of_string suri = + try + MapStringsToUri.find suri !set_of_uri + with Not_found -> +prerr_endline ("@@@ " ^ suri); + let new_uri = suri, fresh_id () in + set_of_uri := MapStringsToUri.add suri new_uri !set_of_uri; + new_uri exception IllFormedUri of string;; -let mk_prefixes str xpointer = - let rec aux curi = - function - [he] -> - let prefix_uri = curi ^ "/" ^ he - and name = List.hd (Str.split (Str.regexp "\\.") he) in - [ normalize prefix_uri ; name ] - | he::tl -> - let prefix_uri = curi ^ "/" ^ he in - (normalize prefix_uri)::(aux prefix_uri tl) - | _ -> raise (IllFormedUri str) - in - let tokens = (Str.split (Str.regexp "/") str) in - (* ty = "cic:" *) - let (ty, sp) = - (try (List.hd tokens, List.tl tokens) - with Failure "hd" | Failure "tl" -> - raise (IllFormedUri str)) - in - (aux ty sp) @ [xpointer] -;; - - -let sharp_rex = - Str.regexp "#" -;; - -let uri_of_string str = - let base, xpointer = - match Str.split sharp_rex str with - | [base] -> base,"" - | [base; xpointer] -> base,xpointer - | _ -> raise (IllFormedUri str) - in - try - SetOfStrings.find str !set_of_uri - with - Not_found -> - let uri = Array.of_list (mk_prefixes base xpointer), fresh_id () in - add_to_uriset ~suri:str uri +let strip_xpointer ((uri,_) as olduri) = + try + let index = String.rindex uri '#' in + let no_xpointer = String.sub uri 0 index in + uri_of_string no_xpointer + with + Not_found -> olduri + +let clear_suffix uri ?(pat2="") pat1 = + try + let index = String.rindex uri '.' in + let index' = index + 1 in + let suffix = String.sub uri index' (String.length uri - index') in + if pat1 = suffix || pat2 = suffix then + String.sub uri 0 index + else + uri + with + Not_found -> assert false + +let has_suffix uri pat = + try + let index = String.rindex uri '.' + 1 in + let suffix = String.sub uri index (String.length uri - index) in + pat = suffix + with + Not_found -> assert false + +let _types = "types" +let _dottypes = ".types" +let _ann = "ann" +let _dotann = ".ann" +let _var = "var" +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 strip_xpointer (uri,_) = - let stripped_uri = Array.copy uri in - stripped_uri.(Array.length uri - 1) <- ""; (* reset xpointer field *) - let new_uri = stripped_uri,fresh_id () in - let suri = string_of_uri new_uri in - add_to_uriset ~suri new_uri - - -let cicuri_of_uri uri = - let completeuri = string_of_uri uri in - let newcompleteuri = - (Str.replace_first (Str.regexp "\\.types$") "" - (Str.replace_first (Str.regexp "\\.ann$") "" completeuri)) - in - if completeuri = newcompleteuri then - uri - else - let uri = fst uri in - let newuri = Array.copy uri in - newuri.(Array.length uri - 3) <- newcompleteuri ; - add_to_uriset (newuri,fresh_id ()) +let annuri_of_uri (uri , _) = + uri_of_string ((clear_suffix uri _ann) ^ _dotann) ;; -let annuri_of_uri uri = - let completeuri = string_of_uri uri in - if Str.string_match (Str.regexp ".*\\.ann$") completeuri 0 then - uri - else - let uri = fst uri in - let newuri = Array.copy uri in - newuri.(Array.length uri - 3) <- completeuri ^ ".ann" ; - add_to_uriset (newuri,fresh_id ()) +let uri_is_annuri (uri, _) = + has_suffix uri _ann ;; -let uri_is_annuri uri = - Str.string_match (Str.regexp ".*\\.ann$") (string_of_uri uri) 0 +let uri_is_var (uri, _) = + has_suffix uri _var ;; -let bodyuri_of_uri uri = - let struri = string_of_uri uri in - if Str.string_match (Str.regexp ".*\\.con$") (string_of_uri uri) 0 then - let uri = fst uri in - let newuri = Array.copy uri in - newuri.(Array.length uri - 3) <- struri ^ ".body" ; - Some (add_to_uriset (newuri,fresh_id ())) +let bodyuri_of_uri (uri, _) = + if has_suffix uri _con then + Some (uri_of_string (uri ^ _dotbody)) else - None + None ;; -let innertypesuri_of_uri uri = - let cicuri = cicuri_of_uri uri in - let newuri = Array.copy (fst cicuri) in - newuri.(Array.length (fst cicuri) - 3) <- (string_of_uri cicuri) ^ ".types" ; - add_to_uriset (newuri,fresh_id ()) +let innertypesuri_of_uri (uri, _) = + uri_of_string ((clear_suffix uri _types) ^ _dottypes) ;; -type uriref = uri * (int list) - -let string_of_uriref (uri, fi) = - let str = 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 uri_of_uriref (uri, _) typeno consno = + let typeno = typeno + 1 in + let suri = + match consno with + | None -> Printf.sprintf "%s%s%d)" uri _xpointer typeno + | Some n -> Printf.sprintf "%s%s%d/%d)" uri _xpointer typeno n + in + uri_of_string suri let compare (_,id1) (_,id2) = id1 - id2 diff --git a/helm/ocaml/urimanager/uriManager.mli b/helm/ocaml/urimanager/uriManager.mli index 771def7c1..27bf862b8 100644 --- a/helm/ocaml/urimanager/uriManager.mli +++ b/helm/ocaml/urimanager/uriManager.mli @@ -35,7 +35,6 @@ val uri_of_string : string -> uri val string_of_uri : uri -> string (* complete uri *) val name_of_uri : uri -> string (* name only (without extension)*) val buri_of_uri : uri -> string (* base uri only *) -val depth_of_uri : uri -> int (* length of the path *) (* given an uri, returns the uri of the corresponding cic file, *) (* i.e. removes the [.types][.ann] suffix *) @@ -47,8 +46,8 @@ val strip_xpointer: uri -> uri (* remove trailing #xpointer..., if any *) (* i.e. adds the .ann suffix if not already present *) val annuri_of_uri : uri -> uri -(* given an uri, tells if it refers to an annotation *) val uri_is_annuri : uri -> bool +val uri_is_var : 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 *) @@ -57,16 +56,10 @@ val bodyuri_of_uri : uri -> uri option (* given an uri, it gives back the uri of its inner types *) val innertypesuri_of_uri : uri -> uri -(* -val mutind_uri: uri -> int -> uri -val mutconstruct_uri: uri -> int -> int -> uri -val mutind: uri -> uri * int -val mutconstruct: uri -> uri * int * int -*) - - (* builder for MutInd and MutConstruct URIs *) -type uriref = uri * (int list) -val string_of_uriref : uriref -> string +(* builder for MutInd and MutConstruct URIs + * [uri] -> [typeno] -> [consno option] + *) +val uri_of_uriref : uri -> int -> int option -> uri module UriSet: Set.S with type elt = uri -- 2.39.2