module Logic:`TopDown.S`

`with type Const.t = const`

module Const:`TopDown.CONST`

type`const =`

`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`

type`scope =`

`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.

**Raises**

`UnifFail`

if it fails`val 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 fails`val alpha_equiv : ``?subst:Subst.t ->`

T.t ->

scope -> T.t -> scope -> Subst.t

Test for alpha equivalence.

**Raises**

`UnifFail`

if it fails`val 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.

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`

module Index:

`l -> r`

(say "l rewrites to r"). Any term t that l matches
is 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.

**Returns** a list of answers, each of which is a list of terms that
map to the given list of variables.