1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML Fri Mar 09 15:38:55 2012 +0000
1.3 @@ -0,0 +1,489 @@
1.4 +(* Title: HOL/TPTP/TPTP_Parser/tptp_syntax.ML
1.5 + Author: Nik Sultana, Cambridge University Computer Laboratory
1.6 +
1.7 +TPTP abstract syntax and parser-related definitions.
1.8 +*)
1.9 +
1.10 +signature TPTP_SYNTAX =
1.11 +sig
1.12 + exception TPTP_SYNTAX of string
1.13 + val debug: ('a -> unit) -> 'a -> unit
1.14 +
1.15 +(*Note that in THF "^ [X] : ^ [Y] : f @ g" should parse
1.16 + as "(^ [X] : (^ [Y] : f)) @ g"
1.17 +*)
1.18 +
1.19 + datatype number_kind = Int_num | Real_num | Rat_num
1.20 +
1.21 + datatype status_value =
1.22 + Suc | Unp | Sap | Esa | Sat | Fsa
1.23 + | Thm | Eqv | Tac | Wec | Eth | Tau
1.24 + | Wtc | Wth | Cax | Sca | Tca | Wca
1.25 + | Cup | Csp | Ecs | Csa | Cth | Ceq
1.26 + | Unc | Wcc | Ect | Fun | Uns | Wuc
1.27 + | Wct | Scc | Uca | Noc
1.28 +
1.29 + type name = string
1.30 + type atomic_word = string
1.31 + type inference_rule = atomic_word
1.32 + type file_info = name option
1.33 + type single_quoted = string
1.34 + type file_name = single_quoted
1.35 + type creator_name = atomic_word
1.36 + type variable = string
1.37 + type upper_word = string
1.38 +
1.39 + datatype language = FOF | CNF | TFF | THF | FOT | TFF_with_arithmetic
1.40 + and role =
1.41 + Role_Axiom | Role_Hypothesis | Role_Definition | Role_Assumption |
1.42 + Role_Lemma | Role_Theorem | Role_Conjecture | Role_Negated_Conjecture |
1.43 + Role_Plain | Role_Fi_Domain | Role_Fi_Functors | Role_Fi_Predicates |
1.44 + Role_Type | Role_Unknown
1.45 +
1.46 + and general_data = (*Bind of variable * formula_data*)
1.47 + Atomic_Word of string
1.48 + | Application of string * general_term list (*general_function*)
1.49 + | V of upper_word (*variable*)
1.50 + | Number of number_kind * string
1.51 + | Distinct_Object of string
1.52 + | (*formula_data*) Formula_Data of language * tptp_formula (* $thf(<thf_formula>) *)
1.53 + | (*formula_data*) Term_Data of tptp_term
1.54 +
1.55 + and interpreted_symbol =
1.56 + UMinus | Sum | Difference | Product | Quotient | Quotient_E |
1.57 + Quotient_T | Quotient_F | Remainder_E | Remainder_T | Remainder_F |
1.58 + Floor | Ceiling | Truncate | Round | To_Int | To_Rat | To_Real |
1.59 + (*these should be in defined_pred, but that's not being used in TPTP*)
1.60 + Less | LessEq | Greater | GreaterEq | EvalEq | Is_Int | Is_Rat |
1.61 + Apply (*this is just a matter of convenience*)
1.62 +
1.63 + and logic_symbol = Equals | NEquals | Or | And | Iff | If | Fi | Xor |
1.64 + Nor | Nand | Not | Op_Forall | Op_Exists |
1.65 + (*these should be in defined_pred, but that's not being used in TPTP*)
1.66 + True | False
1.67 +
1.68 + and quantifier = (*interpreted binders*)
1.69 + Forall | Exists | Epsilon | Iota | Lambda | Dep_Prod | Dep_Sum
1.70 +
1.71 + and tptp_base_type =
1.72 + Type_Ind | Type_Bool | Type_Type | Type_Int | Type_Rat | Type_Real
1.73 +
1.74 + and symbol =
1.75 + Uninterpreted of string
1.76 + | Interpreted_ExtraLogic of interpreted_symbol
1.77 + | Interpreted_Logic of logic_symbol
1.78 + | TypeSymbol of tptp_base_type
1.79 + | System of string
1.80 +
1.81 + and general_term =
1.82 + General_Data of general_data (*general_data*)
1.83 + | General_Term of general_data * general_term (*general_data : general_term*)
1.84 + | General_List of general_term list
1.85 +
1.86 + and tptp_term =
1.87 + Term_Func of symbol * tptp_term list
1.88 + | Term_Var of string
1.89 + | Term_Conditional of tptp_formula * tptp_term * tptp_term
1.90 + | Term_Num of number_kind * string
1.91 + | Term_Distinct_Object of string
1.92 +
1.93 + and tptp_atom =
1.94 + TFF_Typed_Atom of symbol * tptp_type option (*only TFF*)
1.95 + | THF_Atom_term of tptp_term (*from here on, only THF*)
1.96 + | THF_Atom_conn_term of symbol
1.97 +
1.98 + and tptp_formula =
1.99 + Pred of symbol * tptp_term list
1.100 + | Fmla of symbol * tptp_formula list
1.101 + | Sequent of tptp_formula list * tptp_formula list
1.102 + | Quant of quantifier * (string * tptp_type option) list * tptp_formula
1.103 + | Conditional of tptp_formula * tptp_formula * tptp_formula
1.104 + | Let of tptp_let list * tptp_formula
1.105 + | Atom of tptp_atom
1.106 + | THF_type of tptp_type
1.107 + | THF_typing of tptp_formula * tptp_type (*only THF*)
1.108 +
1.109 + and tptp_let =
1.110 + Let_fmla of (string * tptp_type option) * tptp_formula
1.111 + | Let_term of (string * tptp_type option) * tptp_term (*only TFF*)
1.112 +
1.113 + and tptp_type =
1.114 + Prod_type of tptp_type * tptp_type
1.115 + | Fn_type of tptp_type * tptp_type
1.116 + | Atom_type of string
1.117 + | Defined_type of tptp_base_type
1.118 + | Sum_type of tptp_type * tptp_type (*only THF*)
1.119 + | Fmla_type of tptp_formula (*only THF*)
1.120 + | Subtype of symbol * symbol (*only THF*)
1.121 +
1.122 + type general_list = general_term list
1.123 + type parent_details = general_list
1.124 + type useful_info = general_term list
1.125 + type info = useful_info
1.126 +
1.127 + type annotation = general_term * general_term list
1.128 +
1.129 + exception DEQUOTE of string
1.130 +
1.131 + type position = string * int * int
1.132 +
1.133 + datatype tptp_line =
1.134 + Annotated_Formula of position * language * string * role * tptp_formula * annotation option
1.135 + | Include of string * string list
1.136 +
1.137 + type tptp_problem = tptp_line list
1.138 +
1.139 + val dequote : single_quoted -> single_quoted
1.140 +
1.141 + val role_to_string : role -> string
1.142 +
1.143 + val status_to_string : status_value -> string
1.144 +
1.145 + val nameof_tff_atom_type : tptp_type -> string
1.146 +
1.147 + (*Returns the list of all files included in a directory and its
1.148 + subdirectories. This is only used for testing the parser/interpreter against
1.149 + all THF problems.*)
1.150 + val get_file_list : Path.T -> Path.T list
1.151 +
1.152 + val string_of_tptp_term : tptp_term -> string
1.153 + val string_of_tptp_formula : tptp_formula -> string
1.154 +
1.155 +end
1.156 +
1.157 +
1.158 +structure TPTP_Syntax : TPTP_SYNTAX =
1.159 +struct
1.160 +
1.161 +exception TPTP_SYNTAX of string
1.162 +
1.163 +datatype number_kind = Int_num | Real_num | Rat_num
1.164 +
1.165 +datatype status_value =
1.166 + Suc | Unp | Sap | Esa | Sat | Fsa
1.167 + | Thm | Eqv | Tac | Wec | Eth | Tau
1.168 + | Wtc | Wth | Cax | Sca | Tca | Wca
1.169 + | Cup | Csp | Ecs | Csa | Cth | Ceq
1.170 + | Unc | Wcc | Ect | Fun | Uns | Wuc
1.171 + | Wct | Scc | Uca | Noc
1.172 +
1.173 +type name = string
1.174 +type atomic_word = string
1.175 +type inference_rule = atomic_word
1.176 +type file_info = name option
1.177 +type single_quoted = string
1.178 +type file_name = single_quoted
1.179 +type creator_name = atomic_word
1.180 +type variable = string
1.181 +type upper_word = string
1.182 +
1.183 +datatype language = FOF | CNF | TFF | THF | FOT | TFF_with_arithmetic
1.184 +and role =
1.185 + Role_Axiom | Role_Hypothesis | Role_Definition | Role_Assumption |
1.186 + Role_Lemma | Role_Theorem | Role_Conjecture | Role_Negated_Conjecture |
1.187 + Role_Plain | Role_Fi_Domain | Role_Fi_Functors | Role_Fi_Predicates |
1.188 + Role_Type | Role_Unknown
1.189 +and general_data = (*Bind of variable * formula_data*)
1.190 + Atomic_Word of string
1.191 + | Application of string * (general_term list)
1.192 + | V of upper_word (*variable*)
1.193 + | Number of number_kind * string
1.194 + | Distinct_Object of string
1.195 + | (*formula_data*) Formula_Data of language * tptp_formula (* $thf(<thf_formula>) *)
1.196 + | (*formula_data*) Term_Data of tptp_term
1.197 +
1.198 + and interpreted_symbol =
1.199 + UMinus | Sum | Difference | Product | Quotient | Quotient_E |
1.200 + Quotient_T | Quotient_F | Remainder_E | Remainder_T | Remainder_F |
1.201 + Floor | Ceiling | Truncate | Round | To_Int | To_Rat | To_Real |
1.202 + (*these should be in defined_pred, but that's not being used in TPTP*)
1.203 + Less | LessEq | Greater | GreaterEq | EvalEq | Is_Int | Is_Rat |
1.204 + Apply (*this is just a matter of convenience*)
1.205 +
1.206 + and logic_symbol = Equals | NEquals | Or | And | Iff | If | Fi | Xor |
1.207 + Nor | Nand | Not | Op_Forall | Op_Exists |
1.208 + (*these should be in defined_pred, but that's not being used in TPTP*)
1.209 + True | False
1.210 +
1.211 + and quantifier = (*interpreted binders*)
1.212 + Forall | Exists | Epsilon | Iota | Lambda | Dep_Prod | Dep_Sum
1.213 +
1.214 + and tptp_base_type =
1.215 + Type_Ind | Type_Bool | Type_Type | Type_Int | Type_Rat | Type_Real
1.216 +
1.217 + and symbol =
1.218 + Uninterpreted of string
1.219 + | Interpreted_ExtraLogic of interpreted_symbol
1.220 + | Interpreted_Logic of logic_symbol
1.221 + | TypeSymbol of tptp_base_type
1.222 + | System of string
1.223 +
1.224 + and general_term =
1.225 + General_Data of general_data (*general_data*)
1.226 + | General_Term of general_data * general_term (*general_data : general_term*)
1.227 + | General_List of general_term list
1.228 +
1.229 + and tptp_term =
1.230 + Term_Func of symbol * tptp_term list
1.231 + | Term_Var of string
1.232 + | Term_Conditional of tptp_formula * tptp_term * tptp_term
1.233 + | Term_Num of number_kind * string
1.234 + | Term_Distinct_Object of string
1.235 +
1.236 + and tptp_atom =
1.237 + TFF_Typed_Atom of symbol * tptp_type option (*only TFF*)
1.238 + | THF_Atom_term of tptp_term (*from here on, only THF*)
1.239 + | THF_Atom_conn_term of symbol
1.240 +
1.241 + and tptp_formula =
1.242 + Pred of symbol * tptp_term list
1.243 + | Fmla of symbol * tptp_formula list
1.244 + | Sequent of tptp_formula list * tptp_formula list
1.245 + | Quant of quantifier * (string * tptp_type option) list * tptp_formula
1.246 + | Conditional of tptp_formula * tptp_formula * tptp_formula
1.247 + | Let of tptp_let list * tptp_formula
1.248 + | Atom of tptp_atom
1.249 + | THF_type of tptp_type
1.250 + | THF_typing of tptp_formula * tptp_type
1.251 +
1.252 + and tptp_let =
1.253 + Let_fmla of (string * tptp_type option) * tptp_formula (*both TFF and THF*)
1.254 + | Let_term of (string * tptp_type option) * tptp_term (*only TFF*)
1.255 +
1.256 + and tptp_type =
1.257 + Prod_type of tptp_type * tptp_type
1.258 + | Fn_type of tptp_type * tptp_type
1.259 + | Atom_type of string
1.260 + | Defined_type of tptp_base_type
1.261 + | Sum_type of tptp_type * tptp_type (*only THF*)
1.262 + | Fmla_type of tptp_formula (*only THF*)
1.263 + | Subtype of symbol * symbol (*only THF*)
1.264 +
1.265 +type general_list = general_term list
1.266 +type parent_details = general_list
1.267 +type useful_info = general_term list
1.268 +type info = useful_info
1.269 +
1.270 +(*type annotation = (source * info option)*)
1.271 +type annotation = general_term * general_term list
1.272 +
1.273 +exception DEQUOTE of string
1.274 +
1.275 +(*
1.276 +datatype defined_functor =
1.277 + ITE_T | UMINUS | SUM | DIFFERENCE | PRODUCT | QUOTIENT | QUOTIENT_E |
1.278 + QUOTIENT_T | QUOTIENT_F | REMAINDER_E | REMAINDER_T | REMAINDER_F |
1.279 + FLOOR | CEILING | TRUNCATE | ROUND | TO_INT | TO_RAT | TO_REAL
1.280 +*)
1.281 +
1.282 +type position = string * int * int
1.283 +
1.284 +datatype tptp_line =
1.285 + Annotated_Formula of position * language * string * role * tptp_formula * annotation option
1.286 + | Include of string * string list
1.287 +
1.288 +type tptp_problem = tptp_line list
1.289 +
1.290 +fun debug f x = if !Runtime.debug then (f x; ()) else ()
1.291 +
1.292 +fun nameof_tff_atom_type (Atom_type str) = str
1.293 + | nameof_tff_atom_type _ = raise TPTP_SYNTAX "nameof_tff_atom_type called on non-atom type"
1.294 +
1.295 +(*Used for debugging. Returns all files contained within a directory or its
1.296 +subdirectories. Follows symbolic links, filters away directories.*)
1.297 +fun get_file_list path =
1.298 + let
1.299 + fun check_file_entry f rest =
1.300 + let
1.301 + (*NOTE needed since no File.is_link and File.read_link*)
1.302 + val f_str = Path.implode f
1.303 + in
1.304 + if File.is_dir f then
1.305 + rest @ get_file_list f
1.306 + else if OS.FileSys.isLink f_str then
1.307 + (*follow links -- NOTE this breaks if links are relative paths*)
1.308 + check_file_entry (Path.explode (OS.FileSys.readLink f_str)) rest
1.309 + else f :: rest
1.310 + end
1.311 + in
1.312 + File.read_dir path
1.313 + |> map
1.314 + (Path.explode
1.315 + #> Path.append path)
1.316 + |> (fn l => fold check_file_entry l [])
1.317 + end
1.318 +
1.319 +fun role_to_string role =
1.320 + case role of
1.321 + Role_Axiom => "axiom"
1.322 + | Role_Hypothesis => "hypothesis"
1.323 + | Role_Definition => "definition"
1.324 + | Role_Assumption => "assumption"
1.325 + | Role_Lemma => "lemma"
1.326 + | Role_Theorem => "theorem"
1.327 + | Role_Conjecture => "conjecture"
1.328 + | Role_Negated_Conjecture => "negated_conjecture"
1.329 + | Role_Plain => "plain"
1.330 + | Role_Fi_Domain => "fi_domain"
1.331 + | Role_Fi_Functors => "fi_functors"
1.332 + | Role_Fi_Predicates => "fi_predicates"
1.333 + | Role_Type => "type"
1.334 + | Role_Unknown => "unknown"
1.335 +
1.336 +(*accepts a string "'abc'" and returns "abc"*)
1.337 +fun dequote str : single_quoted =
1.338 + if str = "" then
1.339 + raise (DEQUOTE "empty string")
1.340 + else
1.341 + (unprefix "'" str
1.342 + |> unsuffix "'"
1.343 + handle (Fail str) =>
1.344 + if str = "unprefix" then
1.345 + raise DEQUOTE ("string doesn't open with quote:" ^ str)
1.346 + else if str = "unsuffix" then
1.347 + raise DEQUOTE ("string doesn't close with quote:" ^ str)
1.348 + else raise Fail str)
1.349 +
1.350 +
1.351 +(* Printing parsed TPTP formulas *)
1.352 +(*FIXME this is not pretty-printing, just printing*)
1.353 +
1.354 +fun status_to_string status_value =
1.355 + case status_value of
1.356 + Suc => "suc" | Unp => "unp"
1.357 + | Sap => "sap" | Esa => "esa"
1.358 + | Sat => "sat" | Fsa => "fsa"
1.359 + | Thm => "thm" | Wuc => "wuc"
1.360 + | Eqv => "eqv" | Tac => "tac"
1.361 + | Wec => "wec" | Eth => "eth"
1.362 + | Tau => "tau" | Wtc => "wtc"
1.363 + | Wth => "wth" | Cax => "cax"
1.364 + | Sca => "sca" | Tca => "tca"
1.365 + | Wca => "wca" | Cup => "cup"
1.366 + | Csp => "csp" | Ecs => "ecs"
1.367 + | Csa => "csa" | Cth => "cth"
1.368 + | Ceq => "ceq" | Unc => "unc"
1.369 + | Wcc => "wcc" | Ect => "ect"
1.370 + | Fun => "fun" | Uns => "uns"
1.371 + | Wct => "wct" | Scc => "scc"
1.372 + | Uca => "uca" | Noc => "noc"
1.373 +
1.374 +fun string_of_tptp_term x =
1.375 + case x of
1.376 + Term_Func (symbol, tptp_term_list) =>
1.377 + "(" ^ string_of_symbol symbol ^ " " ^
1.378 + String.concatWith " " (map string_of_tptp_term tptp_term_list) ^ ")"
1.379 + | Term_Var str => str
1.380 + | Term_Conditional (tptp_formula, tptp_term1, tptp_term2) => "" (*FIXME*)
1.381 + | Term_Num (_, str) => str
1.382 + | Term_Distinct_Object str => str
1.383 +
1.384 +and string_of_symbol (Uninterpreted str) = str
1.385 + | string_of_symbol (Interpreted_ExtraLogic interpreted_symbol) = string_of_interpreted_symbol interpreted_symbol
1.386 + | string_of_symbol (Interpreted_Logic logic_symbol) = string_of_logic_symbol logic_symbol
1.387 + | string_of_symbol (TypeSymbol tptp_base_type) = string_of_tptp_base_type tptp_base_type
1.388 + | string_of_symbol (System str) = str
1.389 +
1.390 +and string_of_tptp_base_type Type_Ind = "$i"
1.391 + | string_of_tptp_base_type Type_Bool = "$o"
1.392 + | string_of_tptp_base_type Type_Type = "$tType"
1.393 + | string_of_tptp_base_type Type_Int = "$int"
1.394 + | string_of_tptp_base_type Type_Rat = "$rat"
1.395 + | string_of_tptp_base_type Type_Real = "$real"
1.396 +
1.397 +and string_of_interpreted_symbol x =
1.398 + case x of
1.399 + UMinus => "$uminus"
1.400 + | Sum => "$sum"
1.401 + | Difference => "$difference"
1.402 + | Product => "$product"
1.403 + | Quotient => "$quotient"
1.404 + | Quotient_E => "$quotient_e"
1.405 + | Quotient_T => "$quotient_t"
1.406 + | Quotient_F => "$quotient_f"
1.407 + | Remainder_E => "$remainder_e"
1.408 + | Remainder_T => "$remainder_t"
1.409 + | Remainder_F => "$remainder_f"
1.410 + | Floor => "$floor"
1.411 + | Ceiling => "$ceiling"
1.412 + | Truncate => "$truncate"
1.413 + | Round => "$round"
1.414 + | To_Int => "$to_int"
1.415 + | To_Rat => "$to_rat"
1.416 + | To_Real => "$to_real"
1.417 + | Less => "$less"
1.418 + | LessEq => "$lesseq"
1.419 + | Greater => "$greater"
1.420 + | GreaterEq => "$greatereq"
1.421 + | EvalEq => "$evaleq"
1.422 + | Is_Int => "$is_int"
1.423 + | Is_Rat => "$is_rat"
1.424 + | Apply => "@"
1.425 +
1.426 +and string_of_logic_symbol Equals = "="
1.427 + | string_of_logic_symbol NEquals = "!="
1.428 + | string_of_logic_symbol Or = "|"
1.429 + | string_of_logic_symbol And = "&"
1.430 + | string_of_logic_symbol Iff = "<=>"
1.431 + | string_of_logic_symbol If = "=>"
1.432 + | string_of_logic_symbol Fi = "<="
1.433 + | string_of_logic_symbol Xor = "<~>"
1.434 + | string_of_logic_symbol Nor = "~|"
1.435 + | string_of_logic_symbol Nand = "~&"
1.436 + | string_of_logic_symbol Not = "~"
1.437 + | string_of_logic_symbol Op_Forall = "!!"
1.438 + | string_of_logic_symbol Op_Exists = "??"
1.439 + | string_of_logic_symbol True = "$true"
1.440 + | string_of_logic_symbol False = "$false"
1.441 +
1.442 +and string_of_quantifier Forall = "!"
1.443 + | string_of_quantifier Exists = "?"
1.444 + | string_of_quantifier Epsilon = "@+"
1.445 + | string_of_quantifier Iota = "@-"
1.446 + | string_of_quantifier Lambda = "^"
1.447 + | string_of_quantifier Dep_Prod = "!>"
1.448 + | string_of_quantifier Dep_Sum = "?*"
1.449 +
1.450 +and string_of_tptp_atom (TFF_Typed_Atom (symbol, tptp_type_option)) =
1.451 + (case tptp_type_option of
1.452 + NONE => string_of_symbol symbol
1.453 + | SOME tptp_type =>
1.454 + string_of_symbol symbol ^ " : " ^ string_of_tptp_type tptp_type)
1.455 + | string_of_tptp_atom (THF_Atom_term tptp_term) = string_of_tptp_term tptp_term
1.456 + | string_of_tptp_atom (THF_Atom_conn_term symbol) = string_of_symbol symbol
1.457 +
1.458 +and string_of_tptp_formula (Pred (symbol, tptp_term_list)) =
1.459 + "(" ^ string_of_symbol symbol ^
1.460 + String.concatWith " " (map string_of_tptp_term tptp_term_list) ^ ")"
1.461 + | string_of_tptp_formula (Fmla (symbol, tptp_formula_list)) =
1.462 + "(" ^
1.463 + string_of_symbol symbol ^
1.464 + String.concatWith " " (map string_of_tptp_formula tptp_formula_list) ^ ")"
1.465 + | string_of_tptp_formula (Sequent (tptp_formula_list1, tptp_formula_list2)) = "" (*FIXME*)
1.466 + | string_of_tptp_formula (Quant (quantifier, varlist, tptp_formula)) =
1.467 + string_of_quantifier quantifier ^ "[" ^
1.468 + String.concatWith ", " (map (fn (n, ty) =>
1.469 + case ty of
1.470 + NONE => n
1.471 + | SOME ty => n ^ " : " ^ string_of_tptp_type ty) varlist) ^ "] : (" ^
1.472 + string_of_tptp_formula tptp_formula ^ ")"
1.473 + | string_of_tptp_formula (Conditional _) = "" (*FIXME*)
1.474 + | string_of_tptp_formula (Let _) = "" (*FIXME*)
1.475 + | string_of_tptp_formula (Atom tptp_atom) = string_of_tptp_atom tptp_atom
1.476 + | string_of_tptp_formula (THF_type tptp_type) = string_of_tptp_type tptp_type
1.477 + | string_of_tptp_formula (THF_typing (tptp_formula, tptp_type)) =
1.478 + string_of_tptp_formula tptp_formula ^ " : " ^ string_of_tptp_type tptp_type
1.479 +
1.480 +and string_of_tptp_type (Prod_type (tptp_type1, tptp_type2)) =
1.481 + string_of_tptp_type tptp_type1 ^ " * " ^ string_of_tptp_type tptp_type2
1.482 + | string_of_tptp_type (Fn_type (tptp_type1, tptp_type2)) =
1.483 + string_of_tptp_type tptp_type1 ^ " > " ^ string_of_tptp_type tptp_type2
1.484 + | string_of_tptp_type (Atom_type str) = str
1.485 + | string_of_tptp_type (Defined_type tptp_base_type) =
1.486 + string_of_tptp_base_type tptp_base_type
1.487 + | string_of_tptp_type (Sum_type (tptp_type1, tptp_type2)) = ""
1.488 + | string_of_tptp_type (Fmla_type tptp_formula) = string_of_tptp_formula tptp_formula
1.489 + | string_of_tptp_type (Subtype (symbol1, symbol2)) =
1.490 + string_of_symbol symbol1 ^ " << " ^ string_of_symbol symbol2
1.491 +
1.492 +end