module TD:TopDown.S
module Const:TopDown.CONST
typeconst =
Const.t
val set_debug : bool -> unit
module T:sig
..end
module Lit:sig
..end
module C:sig
..end
This module is used for variable bindings.
module Subst:sig
..end
typescope =
Subst.scope
exception UnifFail
For TopDown.S.unify
and TopDown.S.match_
, the optional parameter oc
is used to
enable or disable occur-check. It is disabled by default.
val unify : ?oc:bool ->
?subst:Subst.t ->
T.t ->
scope -> T.t -> scope -> Subst.t
Unify the two terms.
UnifFail
if it failsval match_ : ?oc:bool ->
?subst:Subst.t ->
T.t ->
scope -> T.t -> scope -> Subst.t
match_ a sa b sb
matches the pattern a
in scope sa
with term
b
in scope sb
.
UnifFail
if it failsval alpha_equiv : ?subst:Subst.t ->
T.t ->
scope -> T.t -> scope -> Subst.t
Test for alpha equivalence.
UnifFail
if it failsval are_alpha_equiv : T.t -> T.t -> bool
Special version of alpha_equiv
, using distinct scopes for the two
terms to test, and discarding the result
val clause_are_alpha_equiv : C.t -> C.t -> bool
Alpha equivalence of clauses.
The built-in functions are symbols that have a special meaning. The meaning is given by a set of OCaml functions that can evaluate applications of the function symbol to arguments.
For instance, sum
is a special built-in function that tries to add its
arguments if those are constants.
Note that a constant will never be interpreted.
module BuiltinFun:sig
..end
The following hashtables use alpha-equivalence checking instead of regular, syntactic equality
module TVariantTbl:Hashtbl.S
with type key = T.t
module CVariantTbl:Hashtbl.S
with type key = C.t
An index is a specialized data structured that is used to efficiently store and retrieve data by a key, where the key is a term. Retrieval involves finding all data associated with terms that match, or unify with, a given term.
module Index:
Rewriting consists in having a set of rules, oriented from left to right,
that we will write l -> r
(say "l rewrites to r"). Any term t that l matches
is rewritten into r by replacing it by sigma(r), where sigma(l) = t.
module Rewriting:sig
..end
A DB stores facts and clauses, that constitute a logic program. Facts and clauses can only be added.
Non-stratified programs will be rejected with NonStratifiedProgram.
exception NonStratifiedProgram
module DB:sig
..end
val ask : ?oc:bool ->
?with_rules:C.t list ->
?with_facts:T.t list ->
DB.t -> T.t -> T.t list
Returns the answers to a query in a given DB. Additional facts and rules can be added in a local scope.
oc
: enable occur-check in unification (default false
)val ask_lits : ?oc:bool ->
?with_rules:C.t list ->
?with_facts:T.t list ->
DB.t ->
T.t list -> Lit.t list -> T.t list
Extension of TopDown.S.ask
, where the query ranges over the list of
variables (the term list), all of which must be bound in
the list of literals that form a constraint.
ask_lits db vars lits
queries over variables vars
with
the constraints given by lits
.
Conceptually, the query adds a clause (v1, ..., vn) :- lits, which should respect the same safety constraint as other clauses.