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