From 8162b79d06aef1443b05a11448bce19ec9bf320e Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 30 May 2005 17:14:34 +0000 Subject: [PATCH] added uri_of_term --- helm/ocaml/cic/cicUtil.ml | 13 ++++++++++++- helm/ocaml/cic/cicUtil.mli | 12 +++++++----- 2 files changed, 19 insertions(+), 6 deletions(-) diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml index f2ea4171b..54bd178a0 100644 --- a/helm/ocaml/cic/cicUtil.ml +++ b/helm/ocaml/cic/cicUtil.ml @@ -23,10 +23,11 @@ * http://helm.cs.unibo.it/ *) +open Printf + exception Meta_not_found of int exception Subst_not_found of int - let lookup_meta index metasenv = try List.find (fun (index', _, _) -> index = index') metasenv @@ -160,6 +161,16 @@ let term_of_uri s = | Failure _ | Not_found -> raise (UriManager.IllFormedUri s) +let uri_of_term = function + | Cic.Const (uri, []) + | Cic.Var (uri, []) -> UriManager.string_of_uri uri + | Cic.MutInd (baseuri, tyno, []) -> + 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 + | _ -> raise (Invalid_argument "uri_of_term") + let select ~term ~context = let rec aux context term = match (context, term) with diff --git a/helm/ocaml/cic/cicUtil.mli b/helm/ocaml/cic/cicUtil.mli index 4deec7241..650758eed 100644 --- a/helm/ocaml/cic/cicUtil.mli +++ b/helm/ocaml/cic/cicUtil.mli @@ -36,16 +36,18 @@ val clean_up_local_context : val is_closed : Cic.term -> bool val is_meta_closed : Cic.term -> bool - (** @raise UriManager.IllFormedUri *) -val term_of_uri: string -> Cic.term + (** @raise Failure "not enough prods" *) +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 *) +val term_of_uri: string -> Cic.term (** @raise UriManager.IllFormedUri *) +val uri_of_term: Cic.term -> string (** @raise Invalid_argument "uri_of_term" *) (** packing/unpacking of several terms into a single one *) val pack: Cic.term list -> Cic.term val unpack: Cic.term -> Cic.term list - (** @raise Failure "not enough prods" *) -val strip_prods: int -> Cic.term -> Cic.term - (** {2 Cic selectors} *) val params_of_obj: Cic.obj -> UriManager.uri list -- 2.39.2