From e466e614d63da993d6380cf166bbb041b46f04cd Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 20 Oct 2004 10:54:33 +0000 Subject: [PATCH] added term_of_uri --- helm/ocaml/cic/cicUtil.ml | 25 +++++++++++++++++++++++++ helm/ocaml/cic/cicUtil.mli | 3 +++ 2 files changed, 28 insertions(+) diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml index 29b03a07e..36c266ba7 100644 --- a/helm/ocaml/cic/cicUtil.ml +++ b/helm/ocaml/cic/cicUtil.ml @@ -141,3 +141,28 @@ let meta_closed t = visit_t f r t in try visit_t (fun x -> x) () t; false with Exit -> true + +let xpointer_RE = Str.regexp "[^#]+#xpointer(\\(.*\\))" +let slash_RE = Str.regexp "/" + +let term_of_uri s = + let uri = UriManager.uri_of_string s in + try + (if String.sub s (String.length s - 4) 4 = ".con" then + Cic.Const (uri, []) + else if String.sub s (String.length s - 4) 4 = ".var" then + Cic.Var (uri, []) + else if not (Str.string_match xpointer_RE s 0) then + raise (UriManager.IllFormedUri s) + else + (match Str.split slash_RE (Str.matched_group 1 s) with + | [_; tyno] -> Cic.MutInd (uri, int_of_string tyno - 1, []) + | [_; tyno; consno] -> + Cic.MutConstruct + (uri, int_of_string tyno - 1, int_of_string consno, []) + | _ -> raise Exit)) + with + | Exit + | Failure _ + | Not_found -> raise (UriManager.IllFormedUri s) + diff --git a/helm/ocaml/cic/cicUtil.mli b/helm/ocaml/cic/cicUtil.mli index 24383061c..0b98e51fa 100644 --- a/helm/ocaml/cic/cicUtil.mli +++ b/helm/ocaml/cic/cicUtil.mli @@ -36,3 +36,6 @@ val clean_up_local_context : val is_closed : Cic.term -> bool val meta_closed : Cic.term -> bool + +val term_of_uri: string -> Cic.term + -- 2.39.2