src/Tools/Metis/src/Term.sig

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Term.sig	Wed Jun 20 22:07:52 2007 +0200
@@ -0,0 +1,177 @@
+(* ========================================================================= *)
+(* FIRST ORDER LOGIC TERMS                                                   *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Term =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type of first order logic terms.                                        *)
+(* ------------------------------------------------------------------------- *)
+
+type var = Name.name
+
+type functionName = Name.name
+
+type function = functionName * int
+
+type const = functionName
+
+datatype term =
+    Var of var
+  | Fn of functionName * term list
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors and destructors.                                             *)
+(* ------------------------------------------------------------------------- *)
+
+(* Variables *)
+
+val destVar : term -> var
+
+val isVar : term -> bool
+
+val equalVar : var -> term -> bool
+
+(* Functions *)
+
+val destFn : term -> functionName * term list
+
+val isFn : term -> bool
+
+val fnName : term -> functionName
+
+val fnArguments : term -> term list
+
+val fnArity : term -> int
+
+val fnFunction : term -> function
+
+val functions : term -> NameAritySet.set
+
+val functionNames : term -> NameSet.set
+
+(* Constants *)
+
+val mkConst : const -> term
+
+val destConst : term -> const
+
+val isConst : term -> bool
+
+(* Binary functions *)
+
+val mkBinop : functionName -> term * term -> term
+
+val destBinop : functionName -> term -> term * term
+
+val isBinop : functionName -> term -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* The size of a term in symbols.                                            *)
+(* ------------------------------------------------------------------------- *)
+
+val symbols : term -> int
+
+(* ------------------------------------------------------------------------- *)
+(* A total comparison function for terms.                                    *)
+(* ------------------------------------------------------------------------- *)
+
+val compare : term * term -> order
+
+(* ------------------------------------------------------------------------- *)
+(* Subterms.                                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+type path = int list
+
+val subterm : term -> path -> term
+
+val subterms : term -> (path * term) list
+
+val replace : term -> path * term -> term
+
+val find : (term -> bool) -> term -> path option
+
+val ppPath : path Parser.pp
+
+val pathToString : path -> string
+
+(* ------------------------------------------------------------------------- *)
+(* Free variables.                                                           *)
+(* ------------------------------------------------------------------------- *)
+
+val freeIn : var -> term -> bool
+
+val freeVars : term -> NameSet.set
+
+(* ------------------------------------------------------------------------- *)
+(* Fresh variables.                                                          *)
+(* ------------------------------------------------------------------------- *)
+
+val newVar : unit -> term
+
+val newVars : int -> term list
+
+val variantPrime : NameSet.set -> var -> var
+
+val variantNum : NameSet.set -> var -> var
+
+(* ------------------------------------------------------------------------- *)
+(* Special support for terms with type annotations.                          *)
+(* ------------------------------------------------------------------------- *)
+
+val isTypedVar : term -> bool
+
+val typedSymbols : term -> int
+
+val nonVarTypedSubterms : term -> (path * term) list
+
+(* ------------------------------------------------------------------------- *)
+(* Special support for terms with an explicit function application operator. *)
+(* ------------------------------------------------------------------------- *)
+
+val mkComb : term * term -> term
+
+val destComb : term -> term * term
+
+val isComb : term -> bool
+
+val listMkComb : term * term list -> term
+
+val stripComb : term -> term * term list
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty printing.                                              *)
+(* ------------------------------------------------------------------------- *)
+
+(* Infix symbols *)
+
+val infixes : Parser.infixities ref
+
+(* The negation symbol *)
+
+val negation : Name.name ref
+
+(* Binder symbols *)
+
+val binders : Name.name list ref
+
+(* Bracket symbols *)
+
+val brackets : (Name.name * Name.name) list ref
+
+(* Pretty printing *)
+
+val pp : term Parser.pp
+
+val toString : term -> string
+
+(* Parsing *)
+
+val fromString : string -> term
+
+val parse : term Parser.quotation -> term
+
+end