X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicUtil.mli;h=b6fd7459dea6176bbf931a2c4e513c4fffc54472;hb=7ca56e8a1f819df077d544b890c49ae59fdf3aa7;hp=29657f401874ca46c865727666ffec8295bd02e7;hpb=e51a16c072144e4cabc8fc70841aa4e94a9325b6;p=helm.git diff --git a/helm/ocaml/cic/cicUtil.mli b/helm/ocaml/cic/cicUtil.mli index 29657f401..b6fd7459d 100644 --- a/helm/ocaml/cic/cicUtil.mli +++ b/helm/ocaml/cic/cicUtil.mli @@ -36,5 +36,26 @@ val clean_up_local_context : val is_closed : Cic.term -> bool val is_meta_closed : Cic.term -> bool -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: UriManager.uri -> Cic.term (** @raise UriManager.IllFormedUri *) +val uri_of_term: Cic.term -> UriManager.uri (** @raise Invalid_argument "uri_of_term" *) + +val id_of_annterm: Cic.annterm -> Cic.id + +(** {2 Cic selectors} *) + +val params_of_obj: Cic.obj -> UriManager.uri list +val attributes_of_obj: Cic.obj -> Cic.attribute list + +(** mk_rels [howmany] [from] + * creates a list of [howmany] rels starting from [from] in decreasing order *) +val mk_rels : int -> int -> Cic.term list + +(** {2 Uri hash consing} *) +val rehash_term: Cic.term -> Cic.term +val rehash_obj: Cic.obj -> Cic.obj