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