src/Tools/Metis/src/Term.sig

+(* ========================================================================= *)
+(* FIRST ORDER LOGIC TERMS                                                   *)
+(* Copyright (c) 2001 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
+
+val equal : term -> term -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* 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 Print.pp
+
+val pathToString : path -> string
+
+(* ------------------------------------------------------------------------- *)
+(* Free variables.                                                           *)
+(* ------------------------------------------------------------------------- *)
+
+val freeIn : var -> term -> bool
+
+val freeVars : term -> NameSet.set
+
+val freeVarsList : term list -> 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 hasTypeFunctionName : functionName
+
+val hasTypeFunction : function
+
+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 appName : Name.name
+
+val mkApp : term * term -> term
+
+val destApp : term -> term * term
+
+val isApp : term -> bool
+
+val listMkApp : term * term list -> term
+
+val stripApp : term -> term * term list
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty printing.                                              *)
+(* ------------------------------------------------------------------------- *)
+
+(* Infix symbols *)
+
+val infixes : Print.infixes ref
+
+(* The negation symbol *)
+
+val negation : string ref
+
+(* Binder symbols *)
+
+val binders : string list ref
+
+(* Bracket symbols *)
+
+val brackets : (string * string) list ref
+
+(* Pretty printing *)
+
+val pp : term Print.pp
+
+val toString : term -> string
+
+(* Parsing *)
+
+val fromString : string -> term
+
+val parse : term Parse.quotation -> term
+
+end