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