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