From 405d288cca88e63515164a8d42d60087e305615c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 17 Jun 2005 13:28:22 +0000 Subject: [PATCH] more strings to UriManager.uri --- helm/matita/matitaEngine.ml | 6 +++--- helm/matita/matitaSync.ml | 2 +- helm/ocaml/cic/cicUtil.ml | 14 ++++++++------ helm/ocaml/cic/cicUtil.mli | 5 ++--- .../cic_disambiguation/cicTextualParser2.ml | 10 +++++----- helm/ocaml/cic_disambiguation/disambiguate.ml | 4 ++-- helm/ocaml/cic_notation/cicNotationMatcher.ml | 4 ++-- helm/ocaml/cic_omdoc/content.mli | 2 +- helm/ocaml/cic_omdoc/content2cic.ml | 3 ++- helm/ocaml/cic_unification/coercGraph.ml | 10 ++++------ helm/ocaml/tactics/metadataQuery.ml | 16 ++++++++++------ 11 files changed, 40 insertions(+), 36 deletions(-) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index a74df9313..14eab882c 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -212,11 +212,11 @@ let eval_coercion status coercion = let context = [] in let src_uri = let ty_src = CicReduction.whd context ty_src in - UriManager.uri_of_string (CicUtil.uri_of_term ty_src) + CicUtil.uri_of_term ty_src in let tgt_uri = let ty_tgt = CicReduction.whd context ty_tgt in - UriManager.uri_of_string (CicUtil.uri_of_term ty_tgt) + CicUtil.uri_of_term ty_tgt in let new_coercions = (* also adds them to the Db *) @@ -288,7 +288,7 @@ let eval_command status cmd = {status with aliases = DisambiguateTypes.Environment.add (DisambiguateTypes.Id id) - ("boh?",(fun _ _ _ -> CicUtil.term_of_uri uri)) + ("boh?",(fun _ _ _ -> CicUtil.term_of_uri (UriManager.uri_of_string uri))) status.aliases } | TacticAst.Symbol_alias (symb, instance, desc) -> {status with aliases = diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index 6573e3982..472ab3a92 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -41,7 +41,7 @@ let extract_alias types uri = ) ([],0) types) let env_of_list l env = - let l' = List.map (fun (name,suri) -> name,suri,CicUtil.term_of_uri suri) l in + let l' = List.map (fun (name,suri) -> name,suri,CicUtil.term_of_uri (UriManager.uri_of_string suri)) l in DisambiguateTypes.env_of_list l' env let add_aliases_for_inductive_def status types suri = diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml index a0b035278..a3649ca36 100644 --- a/helm/ocaml/cic/cicUtil.ml +++ b/helm/ocaml/cic/cicUtil.ml @@ -138,8 +138,8 @@ let rec is_meta_closed = let xpointer_RE = Str.regexp "\\([^#]+\\)#xpointer(\\(.*\\))" let slash_RE = Str.regexp "/" -let term_of_uri s = - let uri = UriManager.uri_of_string s in +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 Cic.Const (uri, []) @@ -163,12 +163,14 @@ let term_of_uri s = let uri_of_term = function | Cic.Const (uri, []) - | Cic.Var (uri, []) -> UriManager.string_of_uri uri + | Cic.Var (uri, []) -> uri | Cic.MutInd (baseuri, tyno, []) -> - sprintf "%s#xpointer(1/%d)" (UriManager.string_of_uri baseuri) (tyno + 1) + UriManager.uri_of_string + (sprintf "%s#xpointer(1/%d)" (UriManager.string_of_uri baseuri) (tyno+1)) | Cic.MutConstruct (baseuri, tyno, consno, []) -> - sprintf "%s#xpointer(1/%d/%d)" (UriManager.string_of_uri baseuri) - (tyno + 1) consno + UriManager.uri_of_string + (sprintf "%s#xpointer(1/%d/%d)" (UriManager.string_of_uri baseuri) + (tyno + 1) consno) | _ -> raise (Invalid_argument "uri_of_term") let select ~term ~context = diff --git a/helm/ocaml/cic/cicUtil.mli b/helm/ocaml/cic/cicUtil.mli index 0b6e2242a..a64a983f7 100644 --- a/helm/ocaml/cic/cicUtil.mli +++ b/helm/ocaml/cic/cicUtil.mli @@ -41,9 +41,8 @@ val strip_prods: int -> Cic.term -> Cic.term (** conversions between terms which are fully representable as uris (Var, Const, * Mutind, and MutConstruct) and corresponding tree representations *) -(*CSC: horrible: the strings are URIs. To change also DisambiguateTypes.* *) -val term_of_uri: string -> Cic.term (** @raise UriManager.IllFormedUri *) -val uri_of_term: Cic.term -> string (** @raise Invalid_argument "uri_of_term" *) +val term_of_uri: UriManager.uri -> Cic.term (** @raise UriManager.IllFormedUri *) +val uri_of_term: Cic.term -> UriManager.uri (** @raise Invalid_argument "uri_of_term" *) (* (** packing/unpacking of several terms into a single one *) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index bba6fef7c..b223eb3fd 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -53,9 +53,9 @@ let fresh_num_instance = else (fun () -> 0) -let choice_of_uri uri = - let term = CicUtil.term_of_uri uri in - (uri, (fun _ _ _ -> term)) +let choice_of_uri suri = + let term = CicUtil.term_of_uri (UriManager.uri_of_string suri) in + (suri, (fun _ _ _ -> term)) let grammar = Grammar.gcreate cic_lexer @@ -683,8 +683,8 @@ module EnvironmentP3 = alias: [ (* return a pair from an alias *) [ IDENT "alias"; choice = - [ IDENT "id"; id = IDENT; SYMBOL "="; uri = URI -> - (Id id, choice_of_uri uri) + [ IDENT "id"; id = IDENT; SYMBOL "="; suri = URI -> + (Id id, choice_of_uri suri) | IDENT "symbol"; symbol = QSTRING; PAREN "("; IDENT "instance"; instance = NUM; PAREN ")"; SYMBOL "="; dsc = QSTRING -> diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 27122ef1d..6b5e3f833 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -230,7 +230,7 @@ let interpretate_term ~context ~env ~uri ~is_path ast = let cic = if is_uri ast then (* we have the URI, build the term out of it *) try - CicUtil.term_of_uri name + CicUtil.term_of_uri (UriManager.uri_of_string name) with UriManager.IllFormedUri _ -> CicTextualParser2.fail loc "Ill formed URI" else @@ -638,7 +638,7 @@ module Make (C: Callbacks) = (UriManager.string_of_uri uri, let term = try - CicUtil.term_of_uri (UriManager.string_of_uri uri) + CicUtil.term_of_uri uri with exn -> debug_print (UriManager.string_of_uri uri); debug_print (Printexc.to_string exn); diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml index 08a4617f7..46469e769 100644 --- a/helm/ocaml/cic_notation/cicNotationMatcher.ml +++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml @@ -317,7 +317,7 @@ struct struct type cic_mask_t = Blob - | Uri of string + | Uri of UriManager.uri | Appl of cic_mask_t list let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t) @@ -335,7 +335,7 @@ struct Hashtbl.hash mask, tl let mask_of_appl_pattern = function - | Pt.UriPattern s -> Uri s, [] + | Pt.UriPattern s -> Uri (UriManager.uri_of_string s), [] | Pt.VarPattern _ -> Blob, [] | Pt.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl diff --git a/helm/ocaml/cic_omdoc/content.mli b/helm/ocaml/cic_omdoc/content.mli index 99869b9b4..c1122b8f2 100644 --- a/helm/ocaml/cic_omdoc/content.mli +++ b/helm/ocaml/cic_omdoc/content.mli @@ -130,7 +130,7 @@ and premise = and lemma = { lemma_id: id; lemma_name : string; - lemma_uri: string + lemma_uri: string } ;; diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml index fdc2cea1c..339492d19 100644 --- a/helm/ocaml/cic_omdoc/content2cic.ml +++ b/helm/ocaml/cic_omdoc/content2cic.ml @@ -210,7 +210,8 @@ let proof2cic deannotate p = with Not_found -> prerr_endline ("Not_found in arg2cic: premise " ^ (match prem.Con.premise_binder with None -> "previous" | Some p -> p) ^ ", xref=" ^ prem.Con.premise_xref); raise Not_found)) - | Con.Lemma lemma -> CicUtil.term_of_uri lemma.Con.lemma_uri + | Con.Lemma lemma -> + CicUtil.term_of_uri (UriManager.uri_of_string lemma.Con.lemma_uri) | Con.Term t -> deannotate t | Con.ArgProof p -> proof2cic [] p (* empty! *) | Con.ArgMethod s -> raise TO_DO diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml index fa18530e5..c1056b6ec 100644 --- a/helm/ocaml/cic_unification/coercGraph.ml +++ b/helm/ocaml/cic_unification/coercGraph.ml @@ -31,8 +31,8 @@ let debug_print = if debug then prerr_endline else ignore (* searches a coercion fron src to tgt in the !coercions list *) let look_for_coercion src tgt = try - let src = UriManager.uri_of_string (CicUtil.uri_of_term src) in - let tgt = UriManager.uri_of_string (CicUtil.uri_of_term tgt) in + let src = CicUtil.uri_of_term src in + let tgt = CicUtil.uri_of_term tgt in let l = CoercDb.find_coercion (fun (s,t) -> UriManager.eq s src && UriManager.eq t tgt) @@ -46,7 +46,7 @@ let look_for_coercion src tgt = (UriManager.name_of_uri src) (UriManager.name_of_uri tgt) (UriManager.name_of_uri u)); - Some (CicUtil.term_of_uri (UriManager.string_of_uri u)) + Some (CicUtil.term_of_uri u) with Invalid_argument s -> debug_print (":( coercion non trovata (fallita la uri_of_term): " ^ s); None @@ -133,9 +133,7 @@ let close_coercion_graph src tgt uri = match l with | [] -> assert false | he :: tl -> - let term_of_uri' uri = - CicUtil.term_of_uri (UriManager.string_of_uri uri) - in + let term_of_uri' uri = CicUtil.term_of_uri uri in let first_step = Cic.Constant ("", Some (term_of_uri' he), Cic.Sort Cic.Prop, [], obj_attrs) diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index 644e764ef..c1dd20ecc 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -211,7 +211,7 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) = (* debug_print ("STO APPLICANDO " ^ uri); *) PET.apply_tactic (PrimitiveTactics.apply_tac - ~term:(CicUtil.term_of_uri (UriManager.string_of_uri uri))) + ~term:(CicUtil.term_of_uri uri)) status in let goal_list = @@ -242,7 +242,7 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) = let close_with_types s metasenv context = Constr.UriManagerSet.fold (fun e bag -> - let t = CicUtil.term_of_uri (UriManager.string_of_uri e) in + let t = CicUtil.term_of_uri e in let ty, _ = CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph in @@ -281,7 +281,7 @@ let experimental_hint | Some (main,_) -> let ty, _ = CicTypeChecker.type_of_aux' - metasenv context (CicUtil.term_of_uri (UriManager.string_of_uri main)) CicUniv.empty_ugraph + metasenv context (CicUtil.term_of_uri main) CicUniv.empty_ugraph in Constr.constants_of ty in @@ -313,7 +313,7 @@ let experimental_hint let (subst,(proof, goal_list)) = (* debug_print ("STO APPLICANDO" ^ uri); *) PrimitiveTactics.apply_tac_verbose - ~term:(CicUtil.term_of_uri (UriManager.string_of_uri uri)) + ~term:(CicUtil.term_of_uri uri) status in let goal_list = @@ -484,7 +484,9 @@ let fwd_simpl ~dbd t = let map inners row = match row.(0), row.(1), row.(2) with | Some source, Some inner, Some index -> - source, List.mem (int_of_string index, inner) inners + source, + List.mem + (int_of_string index, (UriManager.uri_of_string inner)) inners | _ -> "", false in let rec rank ranks (source, ok) = @@ -505,7 +507,9 @@ let fwd_simpl ~dbd t = | Some (outer, inners) -> let select = "source, h_inner, h_index" in let from = "genLemma" in - let where = Printf.sprintf "h_outer = \"%s\"" (Mysql.escape outer) in + let where = + Printf.sprintf "h_outer = \"%s\"" + (Mysql.escape (UriManager.string_of_uri outer)) in let query = Printf.sprintf "SELECT %s FROM %s WHERE %s" select from where in let result = Mysql.exec dbd query in let lemmas = Mysql.map result ~f:(map inners) in -- 2.39.2