sig
type symbol = int
type var = int
type units = (AAC_matcher.symbol * AAC_matcher.symbol) list
type ext_units = {
unit_for : AAC_matcher.units;
is_ac : (AAC_matcher.symbol * bool) list;
}
type 'a mset = ('a * int) list
val linear : 'a AAC_matcher.mset -> 'a list
module Terms :
sig
type t =
Dot of
(AAC_matcher.symbol * AAC_matcher.Terms.t * AAC_matcher.Terms.t)
| Plus of
(AAC_matcher.symbol * AAC_matcher.Terms.t * AAC_matcher.Terms.t)
| Sym of (AAC_matcher.symbol * AAC_matcher.Terms.t array)
| Var of AAC_matcher.var
| Unit of AAC_matcher.symbol
val equal_aac :
AAC_matcher.units ->
AAC_matcher.Terms.t -> AAC_matcher.Terms.t -> bool
type nf_term
val nf_term_compare :
AAC_matcher.Terms.nf_term -> AAC_matcher.Terms.nf_term -> int
val nf_equal :
AAC_matcher.Terms.nf_term -> AAC_matcher.Terms.nf_term -> bool
val sprint_nf_term : AAC_matcher.Terms.nf_term -> string
val term_of_t :
AAC_matcher.units -> AAC_matcher.Terms.t -> AAC_matcher.Terms.nf_term
val t_of_term : AAC_matcher.Terms.nf_term -> AAC_matcher.Terms.t
end
module Subst :
sig
type t
val sprint : AAC_matcher.Subst.t -> string
val instantiate :
AAC_matcher.Subst.t -> AAC_matcher.Terms.t -> AAC_matcher.Terms.t
val to_list :
AAC_matcher.Subst.t -> (AAC_matcher.var * AAC_matcher.Terms.t) list
end
val matcher :
?strict:bool ->
AAC_matcher.ext_units ->
AAC_matcher.Terms.t ->
AAC_matcher.Terms.t -> AAC_matcher.Subst.t AAC_search_monad.m
val subterm :
?strict:bool ->
AAC_matcher.ext_units ->
AAC_matcher.Terms.t ->
AAC_matcher.Terms.t ->
(int * AAC_matcher.Terms.t * AAC_matcher.Subst.t AAC_search_monad.m)
AAC_search_monad.m
end