From: Stefano Zacchiroli Date: Fri, 23 Jan 2004 16:37:30 +0000 (+0000) Subject: moved here term_of_uri X-Git-Tag: V_0_2_3~162 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=892c8a3420c36f192b2afdb6ffe146f98f92e2f5;p=helm.git moved here term_of_uri --- diff --git a/helm/ocaml/cic/helmLibraryObjects.ml b/helm/ocaml/cic/helmLibraryObjects.ml index 1d7e9285e..4a1a1dad0 100644 --- a/helm/ocaml/cic/helmLibraryObjects.ml +++ b/helm/ocaml/cic/helmLibraryObjects.ml @@ -1,4 +1,3 @@ - (** {2 Auxiliary functions} *) let uri = UriManager.uri_of_string @@ -7,6 +6,47 @@ let const ?(subst = []) uri = Cic.Const (uri, subst) let var ?(subst = []) uri = Cic.Var (uri, subst) let mutconstruct ?(subst = []) uri typeno consno = Cic.MutConstruct (uri, typeno, consno, subst) +let mutind ?(subst = []) uri typeno = Cic.MutInd (uri, typeno, subst) + +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))) + +let term_of_uri uri = + let s = UriManager.string_of_uri uri in + try + (* Constant *) + (* TODO explicit substitutions? *) + let len = String.length s in + let sub = String.sub s (len -4) 4 in + if sub = ".con" then + const uri + else if sub = ".var" then + var uri + else + (try + (* Inductive Type *) + let (uri, typeno) = indtyuri_of_uri s in + mutind uri typeno + with + | UriManager.IllFormedUri _ | Failure _ | Invalid_argument _ -> + (* Constructor of an Inductive Type *) + let (uri, typeno, consno) = indconuri_of_uri s in + mutconstruct uri typeno consno) + with + | Invalid_argument _ -> raise (UriManager.IllFormedUri s) (** {2 Helm's objects shorthands} *)