Module Ic

module Ic: sig .. end

The compiled clauses intern references to predicate objects (i.e. objects of type Predicate.predicate) and information obtained by them. Abolishing a predicate can make a compiled clause unusable.

See also notes for module IcSet.

type sign =

|	Pos	(*	Positive.	*)
|	StratifiedNegAsFailure	(*	Stratified negation as failure. \+(A), where A must be a non-builtin atom. Succeeds iff A is not unifiable with a fact, at time of the call. A is handled like a builtin that has to be ground in subgoal sorting. This kind of negation should work well with stratification and ground facts. More complex expressions within the scope of \+ (conjunctions, existential variables) can be translated into this form.	*)
|	StratifiedNegAsFailureNotSubsumed	(*	See explanation for 'not_subsumed' in user documentation.	*)
|	Findall
|	Neg2

module BodyLiteral: sig .. end

module HeadLiteral: sig .. end

module Aux: sig .. end

module DisjunctiveHead: sig .. end

type clause 

val get_body : clause -> body

val get_head : clause -> head

val get_news : clause -> News.news

val get_id : clause -> string

val get_source : clause -> Term.term

val make_clause : Aux.aux -> Term.term -> clause

val clause_delta_clauses : Predicate.predicate list -> clause -> clause list

val initialize_clause : clause -> News.news -> unit

val eval_clause : clause -> unit

val reset_gen_id : unit -> unit

exception BranchClosed of Fact.proof