--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Atom.sig Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,141 @@
+(* ========================================================================= *)
+(* FIRST ORDER LOGIC ATOMS *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Atom =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type for storing first order logic atoms. *)
+(* ------------------------------------------------------------------------- *)
+
+type relationName = Name.name
+
+type relation = relationName * int
+
+type atom = relationName * Term.term list
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors and destructors. *)
+(* ------------------------------------------------------------------------- *)
+
+val name : atom -> relationName
+
+val arguments : atom -> Term.term list
+
+val arity : atom -> int
+
+val relation : atom -> relation
+
+val functions : atom -> NameAritySet.set
+
+val functionNames : atom -> NameSet.set
+
+(* Binary relations *)
+
+val mkBinop : relationName -> Term.term * Term.term -> atom
+
+val destBinop : relationName -> atom -> Term.term * Term.term
+
+val isBinop : relationName -> atom -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* The size of an atom in symbols. *)
+(* ------------------------------------------------------------------------- *)
+
+val symbols : atom -> int
+
+(* ------------------------------------------------------------------------- *)
+(* A total comparison function for atoms. *)
+(* ------------------------------------------------------------------------- *)
+
+val compare : atom * atom -> order
+
+val equal : atom -> atom -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Subterms. *)
+(* ------------------------------------------------------------------------- *)
+
+val subterm : atom -> Term.path -> Term.term
+
+val subterms : atom -> (Term.path * Term.term) list
+
+val replace : atom -> Term.path * Term.term -> atom
+
+val find : (Term.term -> bool) -> atom -> Term.path option
+
+(* ------------------------------------------------------------------------- *)
+(* Free variables. *)
+(* ------------------------------------------------------------------------- *)
+
+val freeIn : Term.var -> atom -> bool
+
+val freeVars : atom -> NameSet.set
+
+(* ------------------------------------------------------------------------- *)
+(* Substitutions. *)
+(* ------------------------------------------------------------------------- *)
+
+val subst : Subst.subst -> atom -> atom
+
+(* ------------------------------------------------------------------------- *)
+(* Matching. *)
+(* ------------------------------------------------------------------------- *)
+
+val match : Subst.subst -> atom -> atom -> Subst.subst (* raises Error *)
+
+(* ------------------------------------------------------------------------- *)
+(* Unification. *)
+(* ------------------------------------------------------------------------- *)
+
+val unify : Subst.subst -> atom -> atom -> Subst.subst (* raises Error *)
+
+(* ------------------------------------------------------------------------- *)
+(* The equality relation. *)
+(* ------------------------------------------------------------------------- *)
+
+val eqRelationName : relationName
+
+val eqRelation : relation
+
+val mkEq : Term.term * Term.term -> atom
+
+val destEq : atom -> Term.term * Term.term
+
+val isEq : atom -> bool
+
+val mkRefl : Term.term -> atom
+
+val destRefl : atom -> Term.term
+
+val isRefl : atom -> bool
+
+val sym : atom -> atom (* raises Error if given a refl *)
+
+val lhs : atom -> Term.term
+
+val rhs : atom -> Term.term
+
+(* ------------------------------------------------------------------------- *)
+(* Special support for terms with type annotations. *)
+(* ------------------------------------------------------------------------- *)
+
+val typedSymbols : atom -> int
+
+val nonVarTypedSubterms : atom -> (Term.path * Term.term) list
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty printing. *)
+(* ------------------------------------------------------------------------- *)
+
+val pp : atom Print.pp
+
+val toString : atom -> string
+
+val fromString : string -> atom
+
+val parse : Term.term Parse.quotation -> atom
+
+end