* http://helm.cs.unibo.it/
*)
- (** index a Cic.Constant object and insert resulting metadata into the db
- * PRE_EVAL(dbd) *)
-val index_constant:
- dbd:Mysql.dbd ->
- owner:string ->
- uri:UriManager.uri -> body:Cic.term option -> ty:Cic.term ->
- unit
- (** index a Cic.InductiveDefinition object and insert resulting metadata into
- * the db
- * PRE_EVAL(dbd) *)
-val index_inductive_def:
- dbd:Mysql.dbd ->
- owner:string ->
- uri:UriManager.uri -> types:Cic.inductiveType list ->
- unit
+val index_obj: dbd:Mysql.dbd -> uri:UriManager.uri -> unit
+
(* TODO Zack indexing of variables and (perhaps?) incomplete proofs *)
- (** remove from the db all metadata pertaining to a given owner *)
-val clean: dbd:Mysql.dbd -> unit
+ (** remove from the db all metadata pertaining to a given owner
+ * @return list of uris removed from the db *)
+val clean: dbd:Mysql.dbd -> string list
+val unindex: dbd:Mysql.dbd -> uri:UriManager.uri -> unit
+
+val count_distinct:
+ [`Conclusion | `Hypothesis | `Statement ] ->
+ MetadataTypes.metadata list ->
+ int