sig
type emitted_status =
True
| False_if_reachable
| False_and_reachable
| Dont_know
module Emitted_status :
sig
type t = emitted_status
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
end
exception Inconsistent_emitted_status of Property_status.emitted_status *
Property_status.emitted_status
val emit :
Emitter.t ->
hyps:Property.t list ->
Property.t -> ?distinct:bool -> Property_status.emitted_status -> unit
val emit_and_get :
Emitter.t ->
hyps:Property.t list ->
Property.t ->
?distinct:bool ->
Property_status.emitted_status -> Property_status.emitted_status
val logical_consequence :
Emitter.t -> Property.t -> Property.t list -> unit
val legal_dependency_cycle : Emitter.t -> Property.Set.t -> unit
val self : State.t
type emitter_with_properties = private {
emitter : Emitter.Usable_emitter.t;
mutable properties : Property.t list;
logical_consequence : bool;
}
type inconsistent = private {
valid : Property_status.emitter_with_properties list;
invalid : Property_status.emitter_with_properties list;
}
type status = private
Never_tried
| Best of Property_status.emitted_status *
Property_status.emitter_with_properties list
| Inconsistent of Property_status.inconsistent
type t = status
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code : Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
val get : Property.t -> Property_status.status
val iter_on_statuses :
(Property_status.emitter_with_properties ->
Property_status.emitted_status -> unit) ->
Property.t -> unit
val fold_on_statuses :
(Property_status.emitter_with_properties ->
Property_status.emitted_status -> 'a -> 'a) ->
Property.t -> 'a -> 'a
module Consolidation :
sig
type pending =
Property.Set.t Emitter.Usable_emitter.Map.t
Emitter.Usable_emitter.Map.t
type consolidated_status = private
Never_tried
| Considered_valid
| Valid of Emitter.Usable_emitter.Set.t
| Valid_under_hyp of Property_status.Consolidation.pending
| Unknown of Property_status.Consolidation.pending
| Invalid of Emitter.Usable_emitter.Set.t
| Invalid_under_hyp of Property_status.Consolidation.pending
| Invalid_but_dead of Property_status.Consolidation.pending
| Valid_but_dead of Property_status.Consolidation.pending
| Unknown_but_dead of Property_status.Consolidation.pending
| Inconsistent of string
type t = consolidated_status
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
val get : Property.t -> t
val get_conjunction : Property.t list -> t
end
module Feedback :
sig
type t =
Never_tried
| Considered_valid
| Valid
| Valid_under_hyp
| Unknown
| Invalid
| Invalid_under_hyp
| Invalid_but_dead
| Valid_but_dead
| Unknown_but_dead
| Inconsistent
val get : Property.t -> Property_status.Feedback.t
val get_conjunction : Property.t list -> Property_status.Feedback.t
val pretty : Format.formatter -> Property_status.Feedback.t -> unit
end
module Consolidation_graph :
sig
type t
val get : Property.t -> Property_status.Consolidation_graph.t
val dump :
Property_status.Consolidation_graph.t -> Format.formatter -> unit
end
val iter : (Property.t -> unit) -> unit
val fold : (Property.t -> 'a -> 'a) -> 'a -> 'a
val register : Property.t -> unit
val register_property_add_hook : (Property.t -> unit) -> unit
val remove : Property.t -> unit
val register_property_remove_hook : (Property.t -> unit) -> unit
val merge : old:Property.t list -> Property.t list -> unit
val automatically_proven : Property.t -> bool
end