sultana@47715: (*  Title:      HOL/TPTP/TPTP_Parser/tptp_syntax.ML
sultana@47715:     Author:     Nik Sultana, Cambridge University Computer Laboratory
sultana@47715: 
sultana@47715: TPTP abstract syntax and parser-related definitions.
sultana@47715: *)
sultana@47715: 
sultana@47715: signature TPTP_SYNTAX =
sultana@47715: sig
sultana@47715:   exception TPTP_SYNTAX of string
sultana@47715:   val debug: ('a -> unit) -> 'a -> unit
sultana@47715: 
sultana@47715: (*Note that in THF "^ [X] : ^ [Y] : f @ g" should parse
sultana@47715:   as "(^ [X] : (^ [Y] : f)) @ g"
sultana@47715: *)
sultana@47715: 
sultana@47715:   datatype number_kind = Int_num | Real_num | Rat_num
sultana@47715: 
sultana@47715:   datatype status_value =
sultana@47715:       Suc | Unp | Sap | Esa | Sat | Fsa
sultana@47715:     | Thm | Eqv | Tac | Wec | Eth | Tau
sultana@47715:     | Wtc | Wth | Cax | Sca | Tca | Wca
sultana@47715:     | Cup | Csp | Ecs | Csa | Cth | Ceq
sultana@47715:     | Unc | Wcc | Ect | Fun | Uns | Wuc
sultana@47715:     | Wct | Scc | Uca | Noc
sultana@47715: 
sultana@47715:   type name = string
sultana@47715:   type atomic_word = string
sultana@47715:   type inference_rule = atomic_word
sultana@47715:   type file_info = name option
sultana@47715:   type single_quoted = string
sultana@47715:   type file_name = single_quoted
sultana@47715:   type creator_name = atomic_word
sultana@47715:   type variable = string
sultana@47715:   type upper_word = string
sultana@47715: 
sultana@47715:   datatype language = FOF | CNF | TFF | THF | FOT | TFF_with_arithmetic
sultana@47715:   and role =
sultana@47715:      Role_Axiom | Role_Hypothesis | Role_Definition | Role_Assumption |
sultana@47715:      Role_Lemma | Role_Theorem | Role_Conjecture | Role_Negated_Conjecture |
sultana@47715:      Role_Plain | Role_Fi_Domain | Role_Fi_Functors | Role_Fi_Predicates |
sultana@47715:      Role_Type | Role_Unknown
sultana@47715: 
sultana@47715:   and general_data = (*Bind of variable * formula_data*)
sultana@47715:      Atomic_Word of string
sultana@47715:    | Application of string * general_term list (*general_function*)
sultana@47715:    | V of upper_word (*variable*)
sultana@47715:    | Number of number_kind * string
sultana@47715:    | Distinct_Object of string
sultana@47715:    | (*formula_data*) Formula_Data of language * tptp_formula (* $thf(<thf_formula>) *)
sultana@47715:    | (*formula_data*) Term_Data of tptp_term
sultana@47715: 
sultana@47715:   and interpreted_symbol =
sultana@47715:     UMinus | Sum | Difference | Product | Quotient | Quotient_E |
sultana@47715:     Quotient_T | Quotient_F | Remainder_E | Remainder_T | Remainder_F |
sultana@47715:     Floor | Ceiling | Truncate | Round | To_Int | To_Rat | To_Real |
sultana@48218:     (*FIXME these should be in defined_pred, but that's not being used in TPTP*)
sultana@47715:     Less | LessEq | Greater | GreaterEq | EvalEq | Is_Int | Is_Rat |
sultana@48218:     Distinct | Apply
sultana@47715: 
sultana@47715:   and logic_symbol = Equals | NEquals | Or | And | Iff | If | Fi | Xor |
sultana@47715:     Nor | Nand | Not | Op_Forall | Op_Exists |
sultana@48218:     (*FIXME these should be in defined_pred, but that's not being used in TPTP*)
sultana@47715:     True | False
sultana@47715: 
sultana@47715:   and quantifier = (*interpreted binders*)
sultana@47715:     Forall | Exists | Epsilon | Iota | Lambda | Dep_Prod | Dep_Sum
sultana@47715: 
sultana@47715:   and tptp_base_type =
sultana@47715:     Type_Ind | Type_Bool | Type_Type | Type_Int | Type_Rat | Type_Real
sultana@47715: 
sultana@47715:   and symbol =
sultana@47715:       Uninterpreted of string
sultana@47715:     | Interpreted_ExtraLogic of interpreted_symbol
sultana@47715:     | Interpreted_Logic of logic_symbol
sultana@47715:     | TypeSymbol of tptp_base_type
sultana@47715:     | System of string
sultana@47715: 
sultana@47715:   and general_term =
sultana@47715:       General_Data of general_data (*general_data*)
sultana@47715:     | General_Term of general_data * general_term (*general_data : general_term*)
sultana@47715:     | General_List of general_term list
sultana@47715: 
sultana@47715:   and tptp_term =
sultana@47715:       Term_Func of symbol * tptp_term list
sultana@47715:     | Term_Var of string
sultana@47715:     | Term_Conditional of tptp_formula * tptp_term * tptp_term
sultana@47715:     | Term_Num of number_kind * string
sultana@47715:     | Term_Distinct_Object of string
sultana@48215:     | Term_Let of tptp_let list * tptp_term (*FIXME remove list?*)
sultana@47715: 
sultana@47715:   and tptp_atom =
sultana@47715:       TFF_Typed_Atom of symbol * tptp_type option (*only TFF*)
sultana@47715:     | THF_Atom_term of tptp_term   (*from here on, only THF*)
sultana@47715:     | THF_Atom_conn_term of symbol
sultana@47715: 
sultana@47715:   and tptp_formula =
sultana@47715:       Pred of symbol * tptp_term list
sultana@47715:     | Fmla of symbol * tptp_formula list
sultana@47715:     | Sequent of tptp_formula list * tptp_formula list
sultana@47715:     | Quant of quantifier * (string * tptp_type option) list * tptp_formula
sultana@47715:     | Conditional of tptp_formula * tptp_formula * tptp_formula
sultana@48215:     | Let of tptp_let list * tptp_formula (*FIXME remove list?*)
sultana@47715:     | Atom of tptp_atom
sultana@48218:     | Type_fmla of tptp_type
sultana@47715:     | THF_typing of tptp_formula * tptp_type (*only THF*)
sultana@47715: 
sultana@47715:   and tptp_let =
sultana@47715:       Let_fmla of (string * tptp_type option) * tptp_formula
sultana@48215:     | Let_term of (string * tptp_type option) * tptp_term (*only TFF*)
sultana@47715: 
sultana@47715:   and tptp_type =
sultana@47715:       Prod_type of tptp_type * tptp_type
sultana@47715:     | Fn_type of tptp_type * tptp_type
sultana@47715:     | Atom_type of string
sultana@47715:     | Defined_type of tptp_base_type
sultana@47715:     | Sum_type of tptp_type * tptp_type (*only THF*)
sultana@48215:     | Fmla_type of tptp_formula
sultana@47715:     | Subtype of symbol * symbol (*only THF*)
sultana@47715: 
sultana@47715:   type general_list = general_term list
sultana@47715:   type parent_details = general_list
sultana@47715:   type useful_info = general_term list
sultana@47715:   type info = useful_info
sultana@47715: 
sultana@47715:   type annotation = general_term * general_term list
sultana@47715: 
sultana@47715:   exception DEQUOTE of string
sultana@47715: 
sultana@47715:   type position = string * int * int
sultana@47715: 
sultana@47715:   datatype tptp_line =
sultana@48218:       Annotated_Formula of position * language * string * role *
sultana@48218:         tptp_formula * annotation option
sultana@48440:    |  Include of position * string * string list
sultana@47715: 
sultana@47715:   type tptp_problem = tptp_line list
sultana@47715: 
sultana@47715:   val dequote : single_quoted -> single_quoted
sultana@47715: 
sultana@47715:   val role_to_string : role -> string
sultana@47715: 
sultana@47715:   val status_to_string : status_value -> string
sultana@47715: 
sultana@47715:   val nameof_tff_atom_type : tptp_type -> string
sultana@47715: 
sultana@48440:   val pos_of_line : tptp_line -> position
sultana@48440: 
sultana@47715:   (*Returns the list of all files included in a directory and its
sultana@47715:   subdirectories. This is only used for testing the parser/interpreter against
sultana@47715:   all THF problems.*)
sultana@47715:   val get_file_list : Path.T -> Path.T list
sultana@47715: 
sultana@47715:   val string_of_tptp_term : tptp_term -> string
sultana@47715:   val string_of_tptp_formula : tptp_formula -> string
sultana@47715: 
sultana@47715: end
sultana@47715: 
sultana@47715: 
sultana@47715: structure TPTP_Syntax : TPTP_SYNTAX =
sultana@47715: struct
sultana@47715: 
sultana@47715: exception TPTP_SYNTAX of string
sultana@47715: 
sultana@47715: datatype number_kind = Int_num | Real_num | Rat_num
sultana@47715: 
sultana@47715: datatype status_value =
sultana@47715:     Suc | Unp | Sap | Esa | Sat | Fsa
sultana@47715:   | Thm | Eqv | Tac | Wec | Eth | Tau
sultana@47715:   | Wtc | Wth | Cax | Sca | Tca | Wca
sultana@47715:   | Cup | Csp | Ecs | Csa | Cth | Ceq
sultana@47715:   | Unc | Wcc | Ect | Fun | Uns | Wuc
sultana@47715:   | Wct | Scc | Uca | Noc
sultana@47715: 
sultana@47715: type name = string
sultana@47715: type atomic_word = string
sultana@47715: type inference_rule = atomic_word
sultana@47715: type file_info = name option
sultana@47715: type single_quoted = string
sultana@47715: type file_name = single_quoted
sultana@47715: type creator_name = atomic_word
sultana@47715: type variable = string
sultana@47715: type upper_word = string
sultana@47715: 
sultana@47715: datatype language = FOF | CNF | TFF | THF | FOT | TFF_with_arithmetic
sultana@47715: and role =
sultana@47715:   Role_Axiom | Role_Hypothesis | Role_Definition | Role_Assumption |
sultana@47715:   Role_Lemma | Role_Theorem | Role_Conjecture | Role_Negated_Conjecture |
sultana@47715:   Role_Plain | Role_Fi_Domain | Role_Fi_Functors | Role_Fi_Predicates |
sultana@47715:   Role_Type | Role_Unknown
sultana@47715: and general_data = (*Bind of variable * formula_data*)
sultana@47715:     Atomic_Word of string
sultana@47715:   | Application of string * (general_term list)
sultana@47715:   | V of upper_word (*variable*)
sultana@47715:   | Number of number_kind * string
sultana@47715:   | Distinct_Object of string
sultana@47715:   | (*formula_data*) Formula_Data of language * tptp_formula (* $thf(<thf_formula>) *)
sultana@47715:   | (*formula_data*) Term_Data of tptp_term
sultana@47715: 
sultana@47715:   and interpreted_symbol =
sultana@47715:     UMinus | Sum | Difference | Product | Quotient | Quotient_E |
sultana@47715:     Quotient_T | Quotient_F | Remainder_E | Remainder_T | Remainder_F |
sultana@47715:     Floor | Ceiling | Truncate | Round | To_Int | To_Rat | To_Real |
sultana@47715:     Less | LessEq | Greater | GreaterEq | EvalEq | Is_Int | Is_Rat |
sultana@48215:     Distinct |
sultana@48218:     Apply
sultana@47715: 
sultana@47715:   and logic_symbol = Equals | NEquals | Or | And | Iff | If | Fi | Xor |
sultana@47715:     Nor | Nand | Not | Op_Forall | Op_Exists |
sultana@47715:     True | False
sultana@47715: 
sultana@47715:   and quantifier = (*interpreted binders*)
sultana@47715:     Forall | Exists | Epsilon | Iota | Lambda | Dep_Prod | Dep_Sum
sultana@47715: 
sultana@47715:   and tptp_base_type =
sultana@47715:     Type_Ind | Type_Bool | Type_Type | Type_Int | Type_Rat | Type_Real
sultana@47715: 
sultana@47715:   and symbol =
sultana@47715:       Uninterpreted of string
sultana@47715:     | Interpreted_ExtraLogic of interpreted_symbol
sultana@47715:     | Interpreted_Logic of logic_symbol
sultana@47715:     | TypeSymbol of tptp_base_type
sultana@47715:     | System of string
sultana@47715: 
sultana@47715:   and general_term =
sultana@47715:       General_Data of general_data (*general_data*)
sultana@47715:     | General_Term of general_data * general_term (*general_data : general_term*)
sultana@47715:     | General_List of general_term list
sultana@47715: 
sultana@47715:   and tptp_term =
sultana@47715:       Term_Func of symbol * tptp_term list
sultana@47715:     | Term_Var of string
sultana@47715:     | Term_Conditional of tptp_formula * tptp_term * tptp_term
sultana@47715:     | Term_Num of number_kind * string
sultana@47715:     | Term_Distinct_Object of string
sultana@48215:     | Term_Let of tptp_let list * tptp_term (*FIXME remove list?*)
sultana@47715: 
sultana@47715:   and tptp_atom =
sultana@47715:       TFF_Typed_Atom of symbol * tptp_type option (*only TFF*)
sultana@47715:     | THF_Atom_term of tptp_term   (*from here on, only THF*)
sultana@47715:     | THF_Atom_conn_term of symbol
sultana@47715: 
sultana@47715:   and tptp_formula =
sultana@47715:       Pred of symbol * tptp_term list
sultana@47715:     | Fmla of symbol * tptp_formula list
sultana@47715:     | Sequent of tptp_formula list * tptp_formula list
sultana@47715:     | Quant of quantifier * (string * tptp_type option) list * tptp_formula
sultana@47715:     | Conditional of tptp_formula * tptp_formula * tptp_formula
sultana@47715:     | Let of tptp_let list * tptp_formula
sultana@47715:     | Atom of tptp_atom
sultana@48218:     | Type_fmla of tptp_type
sultana@47715:     | THF_typing of tptp_formula * tptp_type
sultana@47715: 
sultana@47715:   and tptp_let =
sultana@48218:       Let_fmla of (string * tptp_type option) * tptp_formula
sultana@48218:     | Let_term of (string * tptp_type option) * tptp_term
sultana@47715: 
sultana@47715:   and tptp_type =
sultana@47715:       Prod_type of tptp_type * tptp_type
sultana@47715:     | Fn_type of tptp_type * tptp_type
sultana@47715:     | Atom_type of string
sultana@47715:     | Defined_type of tptp_base_type
sultana@48218:     | Sum_type of tptp_type * tptp_type
sultana@48218:     | Fmla_type of tptp_formula
sultana@48218:     | Subtype of symbol * symbol
sultana@47715: 
sultana@47715: type general_list = general_term list
sultana@47715: type parent_details = general_list
sultana@47715: type useful_info = general_term list
sultana@47715: type info = useful_info
sultana@47715: 
sultana@47715: (*type annotation = (source * info option)*)
sultana@47715: type annotation = general_term * general_term list
sultana@47715: 
sultana@47715: exception DEQUOTE of string
sultana@47715: 
sultana@47715: type position = string * int * int
sultana@47715: 
sultana@47715: datatype tptp_line =
sultana@47715:     Annotated_Formula of position * language * string * role * tptp_formula * annotation option
sultana@48440:  |  Include of position * string * string list
sultana@47715: 
sultana@47715: type tptp_problem = tptp_line list
sultana@47715: 
sultana@47715: fun debug f x = if !Runtime.debug then (f x; ()) else ()
sultana@47715: 
sultana@47715: fun nameof_tff_atom_type (Atom_type str) = str
sultana@47715:   | nameof_tff_atom_type _ = raise TPTP_SYNTAX "nameof_tff_atom_type called on non-atom type"
sultana@47715: 
sultana@48440: fun pos_of_line tptp_line =
sultana@48440:   case tptp_line of
sultana@48440:       Annotated_Formula (position, _, _, _, _, _) => position
sultana@48440:    |  Include (position, _, _) => position
sultana@48440: 
sultana@47715: (*Used for debugging. Returns all files contained within a directory or its
sultana@47715: subdirectories. Follows symbolic links, filters away directories.*)
sultana@47715: fun get_file_list path =
sultana@47715:   let
sultana@47715:     fun check_file_entry f rest =
sultana@47715:       let
sultana@47715:         (*NOTE needed since no File.is_link and File.read_link*)
sultana@47715:         val f_str = Path.implode f
sultana@47715:       in
sultana@47715:         if File.is_dir f then
sultana@47715:           rest @ get_file_list f
sultana@47715:         else if OS.FileSys.isLink f_str then
sultana@47715:           (*follow links -- NOTE this breaks if links are relative paths*)
sultana@47715:           check_file_entry (Path.explode (OS.FileSys.readLink f_str)) rest
sultana@47715:         else f :: rest
sultana@47715:       end
sultana@47715:   in
sultana@47715:     File.read_dir path
sultana@47715:     |> map
sultana@47715:         (Path.explode
sultana@47715:         #> Path.append path)
sultana@47715:     |> (fn l => fold check_file_entry l [])
sultana@47715:   end
sultana@47715: 
sultana@47715: fun role_to_string role =
sultana@47715:   case role of
sultana@47715:       Role_Axiom => "axiom"
sultana@47715:     | Role_Hypothesis => "hypothesis"
sultana@47715:     | Role_Definition => "definition"
sultana@47715:     | Role_Assumption => "assumption"
sultana@47715:     | Role_Lemma => "lemma"
sultana@47715:     | Role_Theorem => "theorem"
sultana@47715:     | Role_Conjecture => "conjecture"
sultana@47715:     | Role_Negated_Conjecture => "negated_conjecture"
sultana@47715:     | Role_Plain => "plain"
sultana@47715:     | Role_Fi_Domain => "fi_domain"
sultana@47715:     | Role_Fi_Functors => "fi_functors"
sultana@47715:     | Role_Fi_Predicates => "fi_predicates"
sultana@47715:     | Role_Type => "type"
sultana@47715:     | Role_Unknown => "unknown"
sultana@47715: 
sultana@47715: (*accepts a string "'abc'" and returns "abc"*)
sultana@47715: fun dequote str : single_quoted =
sultana@47715:   if str = "" then
sultana@47715:     raise (DEQUOTE "empty string")
sultana@47715:   else
sultana@47715:     (unprefix "'" str
sultana@47715:     |> unsuffix "'"
sultana@47715:     handle (Fail str) =>
sultana@47715:       if str = "unprefix" then
sultana@47715:         raise DEQUOTE ("string doesn't open with quote:" ^ str)
sultana@47715:       else if str = "unsuffix" then
sultana@47715:         raise DEQUOTE ("string doesn't close with quote:" ^ str)
sultana@47715:       else raise Fail str)
sultana@47715: 
sultana@47715: 
sultana@47715: (* Printing parsed TPTP formulas *)
sultana@47715: (*FIXME this is not pretty-printing, just printing*)
sultana@47715: 
sultana@47715: fun status_to_string status_value =
sultana@47715:   case status_value of
wenzelm@48325:       Suc => "suc"  | Unp => "unp"
sultana@47715:     | Sap => "sap"  | Esa => "esa"
sultana@47715:     | Sat => "sat"  | Fsa => "fsa"
sultana@47715:     | Thm => "thm"  | Wuc => "wuc"
wenzelm@48325:     | Eqv => "eqv"  | Tac => "tac"
wenzelm@48325:     | Wec => "wec"  | Eth => "eth"
wenzelm@48325:     | Tau => "tau"  | Wtc => "wtc"
wenzelm@48325:     | Wth => "wth"  | Cax => "cax"
wenzelm@48325:     | Sca => "sca"  | Tca => "tca"
wenzelm@48325:     | Wca => "wca"  | Cup => "cup"
wenzelm@48325:     | Csp => "csp"  | Ecs => "ecs"
wenzelm@48325:     | Csa => "csa"  | Cth => "cth"
wenzelm@48325:     | Ceq => "ceq"  | Unc => "unc"
wenzelm@48325:     | Wcc => "wcc"  | Ect => "ect"
wenzelm@48325:     | Fun => "fun"  | Uns => "uns"
wenzelm@48325:     | Wct => "wct"  | Scc => "scc"
wenzelm@48325:     | Uca => "uca"  | Noc => "noc"
sultana@47715: 
sultana@47715: fun string_of_tptp_term x =
sultana@47715:   case x of
sultana@47715:       Term_Func (symbol, tptp_term_list) =>
sultana@47715:         "(" ^ string_of_symbol symbol ^ " " ^
wenzelm@48297:         space_implode " " (map string_of_tptp_term tptp_term_list) ^ ")"
sultana@47715:     | Term_Var str => str
sultana@47715:     | Term_Conditional (tptp_formula, tptp_term1, tptp_term2) => "" (*FIXME*)
sultana@47715:     | Term_Num (_, str) => str
sultana@47715:     | Term_Distinct_Object str => str
sultana@47715: 
sultana@47715: and string_of_symbol (Uninterpreted str) = str
sultana@47715:   | string_of_symbol (Interpreted_ExtraLogic interpreted_symbol) = string_of_interpreted_symbol interpreted_symbol
sultana@47715:   | string_of_symbol (Interpreted_Logic logic_symbol) = string_of_logic_symbol logic_symbol
sultana@47715:   | string_of_symbol (TypeSymbol tptp_base_type) = string_of_tptp_base_type tptp_base_type
sultana@47715:   | string_of_symbol (System str) = str
sultana@47715: 
sultana@47715: and string_of_tptp_base_type Type_Ind = "$i"
sultana@47715:   | string_of_tptp_base_type Type_Bool = "$o"
sultana@47715:   | string_of_tptp_base_type Type_Type = "$tType"
sultana@47715:   | string_of_tptp_base_type Type_Int = "$int"
sultana@47715:   | string_of_tptp_base_type Type_Rat = "$rat"
sultana@47715:   | string_of_tptp_base_type Type_Real = "$real"
sultana@47715: 
sultana@47715: and string_of_interpreted_symbol x =
sultana@47715:   case x of
sultana@47715:       UMinus => "$uminus"
sultana@47715:     | Sum => "$sum"
sultana@47715:     | Difference => "$difference"
sultana@47715:     | Product => "$product"
sultana@47715:     | Quotient => "$quotient"
sultana@47715:     | Quotient_E => "$quotient_e"
sultana@47715:     | Quotient_T => "$quotient_t"
sultana@47715:     | Quotient_F => "$quotient_f"
sultana@47715:     | Remainder_E => "$remainder_e"
sultana@47715:     | Remainder_T => "$remainder_t"
sultana@47715:     | Remainder_F => "$remainder_f"
sultana@47715:     | Floor => "$floor"
sultana@47715:     | Ceiling => "$ceiling"
sultana@47715:     | Truncate => "$truncate"
sultana@47715:     | Round => "$round"
sultana@47715:     | To_Int => "$to_int"
sultana@47715:     | To_Rat => "$to_rat"
sultana@47715:     | To_Real => "$to_real"
sultana@47715:     | Less => "$less"
sultana@47715:     | LessEq => "$lesseq"
sultana@47715:     | Greater => "$greater"
sultana@47715:     | GreaterEq => "$greatereq"
sultana@47715:     | EvalEq => "$evaleq"
sultana@47715:     | Is_Int => "$is_int"
sultana@47715:     | Is_Rat => "$is_rat"
sultana@47715:     | Apply => "@"
sultana@47715: 
sultana@47715: and string_of_logic_symbol Equals = "="
sultana@47715:   | string_of_logic_symbol NEquals = "!="
sultana@47715:   | string_of_logic_symbol Or = "|"
sultana@47715:   | string_of_logic_symbol And = "&"
sultana@47715:   | string_of_logic_symbol Iff = "<=>"
sultana@47715:   | string_of_logic_symbol If = "=>"
sultana@47715:   | string_of_logic_symbol Fi = "<="
sultana@47715:   | string_of_logic_symbol Xor = "<~>"
sultana@47715:   | string_of_logic_symbol Nor = "~|"
sultana@47715:   | string_of_logic_symbol Nand = "~&"
sultana@47715:   | string_of_logic_symbol Not = "~"
sultana@47715:   | string_of_logic_symbol Op_Forall = "!!"
sultana@47715:   | string_of_logic_symbol Op_Exists = "??"
sultana@47715:   | string_of_logic_symbol True = "$true"
sultana@47715:   | string_of_logic_symbol False = "$false"
sultana@47715: 
sultana@47715: and string_of_quantifier Forall = "!"
sultana@47715:   | string_of_quantifier Exists  = "?"
sultana@47715:   | string_of_quantifier Epsilon  = "@+"
sultana@47715:   | string_of_quantifier Iota  = "@-"
sultana@47715:   | string_of_quantifier Lambda  = "^"
sultana@47715:   | string_of_quantifier Dep_Prod = "!>"
sultana@47715:   | string_of_quantifier Dep_Sum  = "?*"
sultana@47715: 
sultana@47715: and string_of_tptp_atom (TFF_Typed_Atom (symbol, tptp_type_option)) =
sultana@47715:     (case tptp_type_option of
sultana@47715:        NONE => string_of_symbol symbol
sultana@47715:      | SOME tptp_type =>
sultana@47715:          string_of_symbol symbol ^ " : " ^ string_of_tptp_type tptp_type)
sultana@47715:   | string_of_tptp_atom (THF_Atom_term tptp_term) = string_of_tptp_term tptp_term
sultana@47715:   | string_of_tptp_atom (THF_Atom_conn_term symbol) = string_of_symbol symbol
sultana@47715: 
sultana@47715: and string_of_tptp_formula (Pred (symbol, tptp_term_list)) =
sultana@47715:       "(" ^ string_of_symbol symbol ^
wenzelm@48297:       space_implode " " (map string_of_tptp_term tptp_term_list) ^ ")"
sultana@47715:   | string_of_tptp_formula (Fmla (symbol, tptp_formula_list)) =
sultana@47715:       "(" ^
sultana@47715:       string_of_symbol symbol ^
wenzelm@48297:       space_implode " " (map string_of_tptp_formula tptp_formula_list) ^ ")"
sultana@47715:   | string_of_tptp_formula (Sequent (tptp_formula_list1, tptp_formula_list2)) = "" (*FIXME*)
sultana@47715:   | string_of_tptp_formula (Quant (quantifier, varlist, tptp_formula)) =
sultana@47715:       string_of_quantifier quantifier ^ "[" ^
wenzelm@48297:       space_implode ", " (map (fn (n, ty) =>
sultana@47715:         case ty of
sultana@47715:           NONE => n
sultana@47715:         | SOME ty => n ^ " : " ^ string_of_tptp_type ty) varlist) ^ "] : (" ^
sultana@47715:       string_of_tptp_formula tptp_formula ^ ")"
sultana@47715:   | string_of_tptp_formula (Conditional _) = "" (*FIXME*)
sultana@47715:   | string_of_tptp_formula (Let _) = "" (*FIXME*)
sultana@47715:   | string_of_tptp_formula (Atom tptp_atom) = string_of_tptp_atom tptp_atom
sultana@48218:   | string_of_tptp_formula (Type_fmla tptp_type) = string_of_tptp_type tptp_type
sultana@47715:   | string_of_tptp_formula (THF_typing (tptp_formula, tptp_type)) =
sultana@47715:       string_of_tptp_formula tptp_formula ^ " : " ^ string_of_tptp_type tptp_type
sultana@47715: 
sultana@47715: and string_of_tptp_type (Prod_type (tptp_type1, tptp_type2)) =
sultana@47715:       string_of_tptp_type tptp_type1 ^ " * " ^ string_of_tptp_type tptp_type2
sultana@47715:   | string_of_tptp_type (Fn_type (tptp_type1, tptp_type2)) =
sultana@47715:       string_of_tptp_type tptp_type1 ^ " > " ^ string_of_tptp_type tptp_type2
sultana@47715:   | string_of_tptp_type (Atom_type str) = str
sultana@47715:   | string_of_tptp_type (Defined_type tptp_base_type) =
sultana@47715:       string_of_tptp_base_type tptp_base_type
sultana@47715:   | string_of_tptp_type (Sum_type (tptp_type1, tptp_type2)) = ""
sultana@47715:   | string_of_tptp_type (Fmla_type tptp_formula) = string_of_tptp_formula tptp_formula
sultana@47715:   | string_of_tptp_type (Subtype (symbol1, symbol2)) =
sultana@47715:       string_of_symbol symbol1 ^ " << " ^ string_of_symbol symbol2
sultana@47715: 
sultana@47715: end