1(* ========================================================================= *)
2(* FIRST ORDER LOGIC ATOMS                                                   *)
3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
4(* ========================================================================= *)
5
6signature Atom =
7sig
8
9(* ------------------------------------------------------------------------- *)
10(* A type for storing first order logic atoms.                               *)
11(* ------------------------------------------------------------------------- *)
12
13type relationName = Name.name
14
15type relation = relationName * int
16
17type atom = relationName * Term.term list
18
19(* ------------------------------------------------------------------------- *)
20(* Constructors and destructors.                                             *)
21(* ------------------------------------------------------------------------- *)
22
23val name : atom -> relationName
24
25val arguments : atom -> Term.term list
26
27val arity : atom -> int
28
29val relation : atom -> relation
30
31val functions : atom -> NameAritySet.set
32
33val functionNames : atom -> NameSet.set
34
35(* Binary relations *)
36
37val mkBinop : relationName -> Term.term * Term.term -> atom
38
39val destBinop : relationName -> atom -> Term.term * Term.term
40
41val isBinop : relationName -> atom -> bool
42
43(* ------------------------------------------------------------------------- *)
44(* The size of an atom in symbols.                                           *)
45(* ------------------------------------------------------------------------- *)
46
47val symbols : atom -> int
48
49(* ------------------------------------------------------------------------- *)
50(* A total comparison function for atoms.                                    *)
51(* ------------------------------------------------------------------------- *)
52
53val compare : atom * atom -> order
54
55val equal : atom -> atom -> bool
56
57(* ------------------------------------------------------------------------- *)
58(* Subterms.                                                                 *)
59(* ------------------------------------------------------------------------- *)
60
61val subterm : atom -> Term.path -> Term.term
62
63val subterms : atom -> (Term.path * Term.term) list
64
65val replace : atom -> Term.path * Term.term -> atom
66
67val find : (Term.term -> bool) -> atom -> Term.path option
68
69(* ------------------------------------------------------------------------- *)
70(* Free variables.                                                           *)
71(* ------------------------------------------------------------------------- *)
72
73val freeIn : Term.var -> atom -> bool
74
75val freeVars : atom -> NameSet.set
76
77(* ------------------------------------------------------------------------- *)
78(* Substitutions.                                                            *)
79(* ------------------------------------------------------------------------- *)
80
81val subst : Subst.subst -> atom -> atom
82
83(* ------------------------------------------------------------------------- *)
84(* Matching.                                                                 *)
85(* ------------------------------------------------------------------------- *)
86
87val match : Subst.subst -> atom -> atom -> Subst.subst  (* raises Error *)
88
89(* ------------------------------------------------------------------------- *)
90(* Unification.                                                              *)
91(* ------------------------------------------------------------------------- *)
92
93val unify : Subst.subst -> atom -> atom -> Subst.subst  (* raises Error *)
94
95(* ------------------------------------------------------------------------- *)
96(* The equality relation.                                                    *)
97(* ------------------------------------------------------------------------- *)
98
99val eqRelationName : relationName
100
101val eqRelation : relation
102
103val mkEq : Term.term * Term.term -> atom
104
105val destEq : atom -> Term.term * Term.term
106
107val isEq : atom -> bool
108
109val mkRefl : Term.term -> atom
110
111val destRefl : atom -> Term.term
112
113val isRefl : atom -> bool
114
115val sym : atom -> atom  (* raises Error if given a refl *)
116
117val lhs : atom -> Term.term
118
119val rhs : atom -> Term.term
120
121(* ------------------------------------------------------------------------- *)
122(* Special support for terms with type annotations.                          *)
123(* ------------------------------------------------------------------------- *)
124
125val typedSymbols : atom -> int
126
127val nonVarTypedSubterms : atom -> (Term.path * Term.term) list
128
129(* ------------------------------------------------------------------------- *)
130(* Parsing and pretty printing.                                              *)
131(* ------------------------------------------------------------------------- *)
132
133val pp : atom Print.pp
134
135val toString : atom -> string
136
137val fromString : string -> atom
138
139val parse : Term.term Parse.quotation -> atom
140
141end
142