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