1(* ========================================================================= *)
2(* SUBSTITUTIONS ON FIRST-ORDER TERMS AND FORMULAS                           *)
3(* Copyright (c) 2002-2004 Joe Hurd.                                         *)
4(* ========================================================================= *)
5
6signature mlibSubst =
7sig
8
9type 'a pp           = 'a mlibUseful.pp
10type ('a, 'b) maplet = ('a, 'b) mlibUseful.maplet
11type term            = mlibTerm.term
12type formula         = mlibTerm.formula
13
14type subst
15
16val |<>|          : subst
17val ::>           : (string, term) maplet * subst -> subst
18val @>            : subst * subst -> subst
19val null          : subst -> bool
20val term_subst    : subst -> term -> term
21val formula_subst : subst -> formula -> formula
22val find_redex    : string -> subst -> term option
23val norm          : subst -> subst       (* Removes identity substitutions *)
24val restrict      : string list -> subst -> subst
25val refine        : subst -> subst -> subst
26val is_renaming   : subst -> bool
27val to_maplets    : subst -> (string, term) maplet list
28val from_maplets  : (string, term) maplet list -> subst
29val foldl         : ((string, term) maplet -> 'a -> 'a) -> 'a -> subst -> 'a
30val foldr         : ((string, term) maplet -> 'a -> 'a) -> 'a -> subst -> 'a
31val pp_subst      : subst pp
32
33end
34