src/HOL/Tools/ATP/atp_translate.ML
changeset 43101 1d46d85cd78b
parent 43098 e88e974c4846
child 43102 9a42899ec169
equal deleted inserted replaced
43100:49347c6354b5 43101:1d46d85cd78b
   101   val type_sys_from_string : string -> type_system
   101   val type_sys_from_string : string -> type_system
   102   val polymorphism_of_type_sys : type_system -> polymorphism
   102   val polymorphism_of_type_sys : type_system -> polymorphism
   103   val level_of_type_sys : type_system -> type_level
   103   val level_of_type_sys : type_system -> type_level
   104   val is_type_sys_virtually_sound : type_system -> bool
   104   val is_type_sys_virtually_sound : type_system -> bool
   105   val is_type_sys_fairly_sound : type_system -> bool
   105   val is_type_sys_fairly_sound : type_system -> bool
       
   106   val choose_format : format list -> type_system -> format * type_system
   106   val raw_type_literals_for_types : typ list -> type_literal list
   107   val raw_type_literals_for_types : typ list -> type_literal list
   107   val unmangled_const : string -> string * string fo_term list
   108   val unmangled_const : string -> string * string fo_term list
   108   val translate_atp_fact :
   109   val translate_atp_fact :
   109     Proof.context -> format -> type_system -> bool -> (string * locality) * thm
   110     Proof.context -> format -> type_system -> bool -> (string * locality) * thm
   110     -> translated_formula option * ((string * locality) * thm)
   111     -> translated_formula option * ((string * locality) * thm)
   565   is_type_level_virtually_sound level orelse level = Finite_Types
   566   is_type_level_virtually_sound level orelse level = Finite_Types
   566 val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
   567 val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
   567 
   568 
   568 fun is_setting_higher_order THF (Simple_Types _) = true
   569 fun is_setting_higher_order THF (Simple_Types _) = true
   569   | is_setting_higher_order _ _ = false
   570   | is_setting_higher_order _ _ = false
       
   571 
       
   572 fun choose_format formats (Simple_Types level) =
       
   573     if member (op =) formats THF then (THF, Simple_Types level)
       
   574     else if member (op =) formats TFF then (TFF, Simple_Types level)
       
   575     else choose_format formats (Preds (Mangled_Monomorphic, level, Heavy))
       
   576   | choose_format formats type_sys =
       
   577     (case hd formats of
       
   578        CNF_UEQ =>
       
   579        (CNF_UEQ, case type_sys of
       
   580                    Preds stuff =>
       
   581                    (if is_type_sys_fairly_sound type_sys then Preds else Tags)
       
   582                        stuff
       
   583                  | _ => type_sys)
       
   584      | format => (format, type_sys))
   570 
   585 
   571 type translated_formula =
   586 type translated_formula =
   572   {name: string,
   587   {name: string,
   573    locality: locality,
   588    locality: locality,
   574    kind: formula_kind,
   589    kind: formula_kind,
  1754 
  1769 
  1755 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys
  1770 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys
  1756                         explicit_apply readable_names preproc hyp_ts concl_t
  1771                         explicit_apply readable_names preproc hyp_ts concl_t
  1757                         facts =
  1772                         facts =
  1758   let
  1773   let
       
  1774     val (format, type_sys) = choose_format [format] type_sys
  1759     val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
  1775     val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
  1760       translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
  1776       translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
  1761                          facts
  1777                          facts
  1762     val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
  1778     val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
  1763     val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys
  1779     val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys