Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/HOL/TPTP/TPTP_Parser/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 28 kB

Quellcode-Bibliothek tptp_syntax.ML Sprache: SML

(*  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 ^ " " ^
        implode_space (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 ^
      implode_space (map string_of_tptp_term tptp_term_list) ^ ")"
  | string_of_tptp_formula (Fmla (symbol, tptp_formula_list)) =
      "(" ^
      string_of_symbol symbol ^
      implode_space (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

quality100%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.4Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.