From 49bb3bff65173f6f443b66d2d3120d8d9843144e Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 23 Jan 2004 16:37:57 +0000 Subject: [PATCH] moved term_of_uri in cic/ --- helm/ocaml/cic_disambiguation/disambiguate.ml | 49 ++++--------------- 1 file changed, 9 insertions(+), 40 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index b2df644d2..0e2b59079 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -82,48 +82,10 @@ let refine metasenv context term = debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ; Ko -let indtyuri_of_uri uri = - let index_sharp = String.index uri '#' in - let index_num = index_sharp + 3 in - (UriManager.uri_of_string (String.sub uri 0 index_sharp), - int_of_string(String.sub uri index_num (String.length uri - index_num)) - 1) - -let indconuri_of_uri uri = - let index_sharp = String.index uri '#' in - let index_div = String.rindex uri '/' in - let index_con = index_div + 1 in - (UriManager.uri_of_string (String.sub uri 0 index_sharp), - int_of_string - (String.sub uri (index_sharp + 3) (index_div - index_sharp - 3)) - 1, - int_of_string - (String.sub uri index_con (String.length uri - index_con))) - - (* TODO move it to Cic *) -let term_of_uri uri = - try - (* Constant *) - (* TODO explicit substitutions? *) - let len = String.length uri in - if String.sub uri (len - 4) 4 = ".con" then - Cic.Const (uri_of_string uri, []) - else if String.sub uri (len - 4) 4 = ".var" then - Cic.Var (uri_of_string uri, []) - else - (try - (* Inductive Type *) - let uri',typeno = indtyuri_of_uri uri in - Cic.MutInd (uri', typeno, []) - with - | UriManager.IllFormedUri _ | Failure _ | Invalid_argument _ -> - (* Constructor of an Inductive Type *) - let uri',typeno,consno = indconuri_of_uri uri in - Cic.MutConstruct (uri', typeno, consno, [])) - with - | Invalid_argument _ -> raise (UriManager.IllFormedUri uri) - let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () = snd (Environment.find item env) env num args + (* TODO move it to Cic *) let find_in_environment name context = let rec aux acc = function | [] -> raise Not_found @@ -337,7 +299,14 @@ module Make (C: Callbacks) = uris in List.map - (fun uri -> (uri, let term = term_of_uri uri in fun _ _ _ -> term)) + (fun uri -> + (uri, + let term = + try + HelmLibraryObjects.term_of_uri (UriManager.uri_of_string uri) + with _ -> assert false + in + fun _ _ _ -> term)) uris' let disambiguate_term mqi_handle context metasenv term ~aliases:current_env -- 2.39.2