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