exception AlreadyDefined of UriManager.uri
-val set_object_declaration_hook : (UriManager.uri -> Cic.obj -> unit) -> unit
+type coercion_decl =
+ UriManager.uri -> int (* arity *) ->
+ int (* saturations *) -> string (* baseuri *) ->
+ UriManager.uri list (* lemmas (new objs) *)
-(* this is a pointer to the function which builds the inversion principle *)
-val build_inversion_principle: (UriManager.uri-> Cic.obj -> (UriManager.uri * Cic.obj) list) ref
+(* the add_single_obj fun passed to the callback can raise AlreadyDefined *)
+val add_object_declaration_hook :
+ (add_obj:(UriManager.uri -> Cic.obj -> UriManager.uri list) ->
+ add_coercion:coercion_decl ->
+ UriManager.uri -> Cic.obj -> UriManager.uri list) -> unit
(* adds an object to the library together with all auxiliary lemmas on it *)
(* (e.g. elimination principles, projections, etc.) *)
(* it returns the list of the uris of the auxiliary lemmas generated *)
val add_obj:
- RefinementTool.kit ->
- UriManager.uri -> Cic.obj ->
+ UriManager.uri -> Cic.obj -> pack_coercion_obj:(Cic.obj -> Cic.obj) ->
UriManager.uri list
-(* inverse of add_obj; *)
-(* Warning: it does not remove the dependencies on the object and on its *)
-(* auxiliary lemmas! *)
+(* removes an object (does not remove its associated lemmas) *)
val remove_obj: UriManager.uri -> unit
(* Informs the library that [uri] is a coercion. *)
(* is true are added to the library. *)
(* The list of added objects is returned. *)
val add_coercion:
- add_composites:bool ->
- RefinementTool.kit -> UriManager.uri -> int (* arity *) ->
- int (* saturations *) -> string (* baseuri *) ->
- (UriManager.uri * int * int) list (* URI, arity, saturations *)
-
-(* inverse of add_coercion, removes both the eventually created composite *)
-(* coercions and the information that [uri] and the composites are coercion *)
-val remove_coercion: UriManager.uri -> unit
+ add_composites:bool -> pack_coercion_obj:(Cic.obj -> Cic.obj) -> coercion_decl
-(* this is used when resetting, but the more gracefull push/pop can be used to
- * suspend/resume an execution *)
-val remove_all_coercions: unit -> unit
+(* these just push/pop the coercions database, since the library is not
+ * pushable/poppable *)
val push: unit -> unit
val pop: unit -> unit