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