1(* ========================================================================= *)
2(* FIRST ORDER LOGIC TERMS                                                   *)
3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
4(* ========================================================================= *)
5
6signature Term =
7sig
8
9(* ------------------------------------------------------------------------- *)
10(* A type of first order logic terms.                                        *)
11(* ------------------------------------------------------------------------- *)
12
13type var = Name.name
14
15type functionName = Name.name
16
17type function = functionName * int
18
19type const = functionName
20
21datatype term =
22    Var of var
23  | Fn of functionName * term list
24
25(* ------------------------------------------------------------------------- *)
26(* Constructors and destructors.                                             *)
27(* ------------------------------------------------------------------------- *)
28
29(* Variables *)
30
31val destVar : term -> var
32
33val isVar : term -> bool
34
35val equalVar : var -> term -> bool
36
37(* Functions *)
38
39val destFn : term -> functionName * term list
40
41val isFn : term -> bool
42
43val fnName : term -> functionName
44
45val fnArguments : term -> term list
46
47val fnArity : term -> int
48
49val fnFunction : term -> function
50
51val functions : term -> NameAritySet.set
52
53val functionNames : term -> NameSet.set
54
55(* Constants *)
56
57val mkConst : const -> term
58
59val destConst : term -> const
60
61val isConst : term -> bool
62
63(* Binary functions *)
64
65val mkBinop : functionName -> term * term -> term
66
67val destBinop : functionName -> term -> term * term
68
69val isBinop : functionName -> term -> bool
70
71(* ------------------------------------------------------------------------- *)
72(* The size of a term in symbols.                                            *)
73(* ------------------------------------------------------------------------- *)
74
75val symbols : term -> int
76
77(* ------------------------------------------------------------------------- *)
78(* A total comparison function for terms.                                    *)
79(* ------------------------------------------------------------------------- *)
80
81val compare : term * term -> order
82
83val equal : term -> term -> bool
84
85(* ------------------------------------------------------------------------- *)
86(* Subterms.                                                                 *)
87(* ------------------------------------------------------------------------- *)
88
89type path = int list
90
91val subterm : term -> path -> term
92
93val subterms : term -> (path * term) list
94
95val replace : term -> path * term -> term
96
97val find : (term -> bool) -> term -> path option
98
99val ppPath : path Print.pp
100
101val pathToString : path -> string
102
103(* ------------------------------------------------------------------------- *)
104(* Free variables.                                                           *)
105(* ------------------------------------------------------------------------- *)
106
107val freeIn : var -> term -> bool
108
109val freeVars : term -> NameSet.set
110
111val freeVarsList : term list -> NameSet.set
112
113(* ------------------------------------------------------------------------- *)
114(* Fresh variables.                                                          *)
115(* ------------------------------------------------------------------------- *)
116
117val newVar : unit -> term
118
119val newVars : int -> term list
120
121val variantPrime : NameSet.set -> var -> var
122
123val variantNum : NameSet.set -> var -> var
124
125(* ------------------------------------------------------------------------- *)
126(* Special support for terms with type annotations.                          *)
127(* ------------------------------------------------------------------------- *)
128
129val hasTypeFunctionName : functionName
130
131val hasTypeFunction : function
132
133val isTypedVar : term -> bool
134
135val typedSymbols : term -> int
136
137val nonVarTypedSubterms : term -> (path * term) list
138
139(* ------------------------------------------------------------------------- *)
140(* Special support for terms with an explicit function application operator. *)
141(* ------------------------------------------------------------------------- *)
142
143val appName : Name.name
144
145val mkApp : term * term -> term
146
147val destApp : term -> term * term
148
149val isApp : term -> bool
150
151val listMkApp : term * term list -> term
152
153val stripApp : term -> term * term list
154
155(* ------------------------------------------------------------------------- *)
156(* Parsing and pretty printing.                                              *)
157(* ------------------------------------------------------------------------- *)
158
159(* Infix symbols *)
160
161val infixes : Print.infixes ref
162
163(* The negation symbol *)
164
165val negation : string ref
166
167(* Binder symbols *)
168
169val binders : string list ref
170
171(* Bracket symbols *)
172
173val brackets : (string * string) list ref
174
175(* Pretty printing *)
176
177val pp : term Print.pp
178
179val toString : term -> string
180
181(* Parsing *)
182
183val fromString : string -> term
184
185val parse : term Parse.quotation -> term
186
187end
188