Module Symkat

module Symkat: sig .. end

High-level interface of the library, main entry point for standalone program

val hk : bool Pervasives.ref

do we use Hopcroft and Karp's version?

val congruence : bool Pervasives.ref

do we use up-to congruence

val ssf : bool Pervasives.ref

do we put expressions in strict star form first?

val trace : bool Pervasives.ref

do we trace unifications in Format.str_formatter

val construction : [ `Antimirov | `Brzozowski | `IlieYu ] Pervasives.ref

which construction do we use

val equiv : ?hyps:Hypotheses.t -> Kat.expr -> Kat.expr -> Kat.gstring option

equivalence check, using the above parameters; returns a counter-example if any. If hyps is specified, exploit the corresponding hypotheses (see module Hypotheses).

val compare : ?hyps:Hypotheses.t ->
       Kat.expr ->
       Kat.expr ->
       (Kat.expr' * Kat.expr') *
       [ `D of Kat.gstring * Kat.gstring
       | `E
       | `G of Kat.gstring
       | `L of Kat.gstring ]

full comparison: compare ~hyps x y returns

`E if x and y are equivalent,
`L w if x is strictly contained in y (then w is a witness for strictness),
`G w if y is strictly contained in x (then w is a witness for strictness),
`D(w1,w2) if x and y are incomparable (then w1 is a witness against x<=y, and w2 is a witness against y<=x). Also return the actually compared terms, in symbolic form. Exploit hypotheses if asked to.

val check : [ `D | `E | `G | `L ] -> ?hyps:string -> string -> string -> unit

utility for verifications: check two expressions for equivalence (`E), difference (`D), left-to-right inclusion (`L), or right-to-left inclusion (`G). Exploit hypotheses if asked to.