1(* ========================================================================= *) 2(* FIRST ORDER LOGIC TERMS *) 3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6signature Term = 7sig 8 9(* ------------------------------------------------------------------------- *) 10(* A type of first order logic terms. *) 11(* ------------------------------------------------------------------------- *) 12 13type var = Name.name 14 15type functionName = Name.name 16 17type function = functionName * int 18 19type const = functionName 20 21datatype term = 22 Var of var 23 | Fn of functionName * term list 24 25(* ------------------------------------------------------------------------- *) 26(* Constructors and destructors. *) 27(* ------------------------------------------------------------------------- *) 28 29(* Variables *) 30 31val destVar : term -> var 32 33val isVar : term -> bool 34 35val equalVar : var -> term -> bool 36 37(* Functions *) 38 39val destFn : term -> functionName * term list 40 41val isFn : term -> bool 42 43val fnName : term -> functionName 44 45val fnArguments : term -> term list 46 47val fnArity : term -> int 48 49val fnFunction : term -> function 50 51val functions : term -> NameAritySet.set 52 53val functionNames : term -> NameSet.set 54 55(* Constants *) 56 57val mkConst : const -> term 58 59val destConst : term -> const 60 61val isConst : term -> bool 62 63(* Binary functions *) 64 65val mkBinop : functionName -> term * term -> term 66 67val destBinop : functionName -> term -> term * term 68 69val isBinop : functionName -> term -> bool 70 71(* ------------------------------------------------------------------------- *) 72(* The size of a term in symbols. *) 73(* ------------------------------------------------------------------------- *) 74 75val symbols : term -> int 76 77(* ------------------------------------------------------------------------- *) 78(* A total comparison function for terms. *) 79(* ------------------------------------------------------------------------- *) 80 81val compare : term * term -> order 82 83val equal : term -> term -> bool 84 85(* ------------------------------------------------------------------------- *) 86(* Subterms. *) 87(* ------------------------------------------------------------------------- *) 88 89type path = int list 90 91val subterm : term -> path -> term 92 93val subterms : term -> (path * term) list 94 95val replace : term -> path * term -> term 96 97val find : (term -> bool) -> term -> path option 98 99val ppPath : path Print.pp 100 101val pathToString : path -> string 102 103(* ------------------------------------------------------------------------- *) 104(* Free variables. *) 105(* ------------------------------------------------------------------------- *) 106 107val freeIn : var -> term -> bool 108 109val freeVars : term -> NameSet.set 110 111val freeVarsList : term list -> NameSet.set 112 113(* ------------------------------------------------------------------------- *) 114(* Fresh variables. *) 115(* ------------------------------------------------------------------------- *) 116 117val newVar : unit -> term 118 119val newVars : int -> term list 120 121val variantPrime : NameSet.set -> var -> var 122 123val variantNum : NameSet.set -> var -> var 124 125(* ------------------------------------------------------------------------- *) 126(* Special support for terms with type annotations. *) 127(* ------------------------------------------------------------------------- *) 128 129val hasTypeFunctionName : functionName 130 131val hasTypeFunction : function 132 133val isTypedVar : term -> bool 134 135val typedSymbols : term -> int 136 137val nonVarTypedSubterms : term -> (path * term) list 138 139(* ------------------------------------------------------------------------- *) 140(* Special support for terms with an explicit function application operator. *) 141(* ------------------------------------------------------------------------- *) 142 143val appName : Name.name 144 145val mkApp : term * term -> term 146 147val destApp : term -> term * term 148 149val isApp : term -> bool 150 151val listMkApp : term * term list -> term 152 153val stripApp : term -> term * term list 154 155(* ------------------------------------------------------------------------- *) 156(* Parsing and pretty printing. *) 157(* ------------------------------------------------------------------------- *) 158 159(* Infix symbols *) 160 161val infixes : Print.infixes ref 162 163(* The negation symbol *) 164 165val negation : string ref 166 167(* Binder symbols *) 168 169val binders : string list ref 170 171(* Bracket symbols *) 172 173val brackets : (string * string) list ref 174 175(* Pretty printing *) 176 177val pp : term Print.pp 178 179val toString : term -> string 180 181(* Parsing *) 182 183val fromString : string -> term 184 185val parse : term Parse.quotation -> term 186 187end 188