src/Tools/Metis/src/Subst.sig

 (* ========================================================================= *)
 (* FIRST ORDER LOGIC SUBSTITUTIONS                                           *)
-(* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License       *)
 (* ========================================================================= *)
 
 signature Subst =
 sig
 

 
 val insert : subst -> Term.var * Term.term -> subst
 
 val singleton : Term.var * Term.term -> subst
 
-val union : subst -> subst -> subst
-
 val toList : subst -> (Term.var * Term.term) list
 
 val fromList : (Term.var * Term.term) list -> subst
 
 val foldl : (Term.var * Term.term * 'a -> 'a) -> 'a -> subst -> 'a
 
 val foldr : (Term.var * Term.term * 'a -> 'a) -> 'a -> subst -> 'a
 
-val pp : subst Parser.pp
+val pp : subst Print.pp
 
 val toString : subst -> string
 
 (* ------------------------------------------------------------------------- *)
 (* Normalizing removes identity substitutions.                               *)

 (* ------------------------------------------------------------------------- *)
 
 val compose : subst -> subst -> subst
 
 (* ------------------------------------------------------------------------- *)
-(* Substitutions can be inverted iff they are renaming substitutions.        *) 
+(* Creating the union of two compatible substitutions.                       *)
+(* ------------------------------------------------------------------------- *)
+
+val union : subst -> subst -> subst  (* raises Error *)
+
+(* ------------------------------------------------------------------------- *)
+(* Substitutions can be inverted iff they are renaming substitutions.        *)
 (* ------------------------------------------------------------------------- *)
 
 val invert : subst -> subst  (* raises Error *)
 
 val isRenaming : subst -> bool

 (* ------------------------------------------------------------------------- *)
 (* Creating a substitution to freshen variables.                             *)
 (* ------------------------------------------------------------------------- *)
 
 val freshVars : NameSet.set -> subst
+
+(* ------------------------------------------------------------------------- *)
+(* Free variables.                                                           *)
+(* ------------------------------------------------------------------------- *)
+
+val redexes : subst -> NameSet.set
+
+val residueFreeVars : subst -> NameSet.set
+
+val freeVars : subst -> NameSet.set
+
+(* ------------------------------------------------------------------------- *)
+(* Functions.                                                                *)
+(* ------------------------------------------------------------------------- *)
+
+val functions : subst -> NameAritySet.set
 
 (* ------------------------------------------------------------------------- *)
 (* Matching for first order logic terms.                                     *)
 (* ------------------------------------------------------------------------- *)