1(* ========================================================================= *) 2(* FIRST ORDER LOGIC SUBSTITUTIONS *) 3(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6signature Subst = 7sig 8 9(* ------------------------------------------------------------------------- *) 10(* A type of first order logic substitutions. *) 11(* ------------------------------------------------------------------------- *) 12 13type subst 14 15(* ------------------------------------------------------------------------- *) 16(* Basic operations. *) 17(* ------------------------------------------------------------------------- *) 18 19val empty : subst 20 21val null : subst -> bool 22 23val size : subst -> int 24 25val peek : subst -> Term.var -> Term.term option 26 27val insert : subst -> Term.var * Term.term -> subst 28 29val singleton : Term.var * Term.term -> subst 30 31val toList : subst -> (Term.var * Term.term) list 32 33val fromList : (Term.var * Term.term) list -> subst 34 35val foldl : (Term.var * Term.term * 'a -> 'a) -> 'a -> subst -> 'a 36 37val foldr : (Term.var * Term.term * 'a -> 'a) -> 'a -> subst -> 'a 38 39val pp : subst Print.pp 40 41val toString : subst -> string 42 43(* ------------------------------------------------------------------------- *) 44(* Normalizing removes identity substitutions. *) 45(* ------------------------------------------------------------------------- *) 46 47val normalize : subst -> subst 48 49(* ------------------------------------------------------------------------- *) 50(* Applying a substitution to a first order logic term. *) 51(* ------------------------------------------------------------------------- *) 52 53val subst : subst -> Term.term -> Term.term 54 55(* ------------------------------------------------------------------------- *) 56(* Restricting a substitution to a smaller set of variables. *) 57(* ------------------------------------------------------------------------- *) 58 59val restrict : subst -> NameSet.set -> subst 60 61val remove : subst -> NameSet.set -> subst 62 63(* ------------------------------------------------------------------------- *) 64(* Composing two substitutions so that the following identity holds: *) 65(* *) 66(* subst (compose sub1 sub2) tm = subst sub2 (subst sub1 tm) *) 67(* ------------------------------------------------------------------------- *) 68 69val compose : subst -> subst -> subst 70 71(* ------------------------------------------------------------------------- *) 72(* Creating the union of two compatible substitutions. *) 73(* ------------------------------------------------------------------------- *) 74 75val union : subst -> subst -> subst (* raises Error *) 76 77(* ------------------------------------------------------------------------- *) 78(* Substitutions can be inverted iff they are renaming substitutions. *) 79(* ------------------------------------------------------------------------- *) 80 81val invert : subst -> subst (* raises Error *) 82 83val isRenaming : subst -> bool 84 85(* ------------------------------------------------------------------------- *) 86(* Creating a substitution to freshen variables. *) 87(* ------------------------------------------------------------------------- *) 88 89val freshVars : NameSet.set -> subst 90 91(* ------------------------------------------------------------------------- *) 92(* Free variables. *) 93(* ------------------------------------------------------------------------- *) 94 95val redexes : subst -> NameSet.set 96 97val residueFreeVars : subst -> NameSet.set 98 99val freeVars : subst -> NameSet.set 100 101(* ------------------------------------------------------------------------- *) 102(* Functions. *) 103(* ------------------------------------------------------------------------- *) 104 105val functions : subst -> NameAritySet.set 106 107(* ------------------------------------------------------------------------- *) 108(* Matching for first order logic terms. *) 109(* ------------------------------------------------------------------------- *) 110 111val match : subst -> Term.term -> Term.term -> subst (* raises Error *) 112 113(* ------------------------------------------------------------------------- *) 114(* Unification for first order logic terms. *) 115(* ------------------------------------------------------------------------- *) 116 117val unify : subst -> Term.term -> Term.term -> subst (* raises Error *) 118 119end 120