src/HOL/Tools/ATP/atp_translate.ML
changeset 44754 265174356212
parent 44742 68e34e7f01ab
child 44768 a7bc1bdb8bb4
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Sep 06 18:07:44 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Sep 06 18:13:36 2011 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4    type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
     1.5    type connective = ATP_Problem.connective
     1.6    type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
     1.7 -  type format = ATP_Problem.format
     1.8 +  type tptp_format = ATP_Problem.tptp_format
     1.9    type formula_kind = ATP_Problem.formula_kind
    1.10    type 'a problem = 'a ATP_Problem.problem
    1.11  
    1.12 @@ -92,7 +92,7 @@
    1.13    val level_of_type_enc : type_enc -> type_level
    1.14    val is_type_enc_quasi_sound : type_enc -> bool
    1.15    val is_type_enc_fairly_sound : type_enc -> bool
    1.16 -  val adjust_type_enc : format -> type_enc -> type_enc
    1.17 +  val adjust_type_enc : tptp_format -> type_enc -> type_enc
    1.18    val mk_aconns :
    1.19      connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
    1.20    val unmangled_const : string -> string * (string, 'b) ho_term list
    1.21 @@ -100,7 +100,7 @@
    1.22    val helper_table : ((string * bool) * thm list) list
    1.23    val factsN : string
    1.24    val prepare_atp_problem :
    1.25 -    Proof.context -> format -> formula_kind -> formula_kind -> type_enc
    1.26 +    Proof.context -> tptp_format -> formula_kind -> formula_kind -> type_enc
    1.27      -> bool -> string -> bool -> bool -> term list -> term
    1.28      -> ((string * locality) * term) list
    1.29      -> string problem * string Symtab.table * int * int
    1.30 @@ -142,7 +142,7 @@
    1.31  (* TFF1 is still in development, and it is still unclear whether symbols will be
    1.32     allowed to have types like "$tType > $o" (i.e., "![A : $tType] : $o"), with
    1.33     "dummy" type variables. *)
    1.34 -val exploit_tff1_dummy_type_vars = false
    1.35 +val avoid_first_order_dummy_type_vars = true
    1.36  
    1.37  val bound_var_prefix = "B_"
    1.38  val all_bound_var_prefix = "BA_"
    1.39 @@ -325,8 +325,8 @@
    1.40    fun default c = const_prefix ^ lookup_const c
    1.41  in
    1.42    fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
    1.43 -    | make_fixed_const (SOME (THF0 THF_With_Choice)) c =
    1.44 -        if c = choice_const then tptp_choice else default c
    1.45 +    | make_fixed_const (SOME (THF (_, _, THF_With_Choice))) c =
    1.46 +      if c = choice_const then tptp_choice else default c
    1.47      | make_fixed_const _ c = default c
    1.48  end
    1.49  
    1.50 @@ -587,7 +587,9 @@
    1.51              | _ => raise Same.SAME)
    1.52           | ("simple_higher", (SOME poly, _, Nonuniform)) =>
    1.53             (case (poly, level) of
    1.54 -              (_, Noninf_Nonmono_Types _) => raise Same.SAME
    1.55 +              (Polymorphic, All_Types) =>
    1.56 +              Simple_Types (Higher_Order, Polymorphic, All_Types)
    1.57 +            | (_, Noninf_Nonmono_Types _) => raise Same.SAME
    1.58              | (Mangled_Monomorphic, _) =>
    1.59                Simple_Types (Higher_Order, Mangled_Monomorphic, level)
    1.60              | _ => raise Same.SAME)
    1.61 @@ -631,12 +633,13 @@
    1.62    | is_type_level_monotonicity_based Fin_Nonmono_Types = true
    1.63    | is_type_level_monotonicity_based _ = false
    1.64  
    1.65 -fun adjust_type_enc (THF0 _) (Simple_Types (order, Polymorphic, level)) =
    1.66 +fun adjust_type_enc (THF (TPTP_Monomorphic, _, _))
    1.67 +                    (Simple_Types (order, _, level)) =
    1.68      Simple_Types (order, Mangled_Monomorphic, level)
    1.69 -  | adjust_type_enc (THF0 _) type_enc = type_enc
    1.70 -  | adjust_type_enc (TFF (TFF_Monomorphic, _)) (Simple_Types (_, _, level)) =
    1.71 +  | adjust_type_enc (THF _) type_enc = type_enc
    1.72 +  | adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Simple_Types (_, _, level)) =
    1.73      Simple_Types (First_Order, Mangled_Monomorphic, level)
    1.74 -  | adjust_type_enc (TFF (_, _)) (Simple_Types (_, poly, level)) =
    1.75 +  | adjust_type_enc (TFF _) (Simple_Types (_, poly, level)) =
    1.76      Simple_Types (First_Order, poly, level)
    1.77    | adjust_type_enc format (Simple_Types (_, poly, level)) =
    1.78      adjust_type_enc format (Guards (poly, level, Uniform))
    1.79 @@ -746,8 +749,9 @@
    1.80  fun type_class_formula type_enc class arg =
    1.81    AAtom (ATerm (class, arg ::
    1.82        (case type_enc of
    1.83 -         Simple_Types (_, Polymorphic, _) =>
    1.84 -         if exploit_tff1_dummy_type_vars then [] else [ATerm (TYPE_name, [arg])]
    1.85 +         Simple_Types (First_Order, Polymorphic, _) =>
    1.86 +         if avoid_first_order_dummy_type_vars then [ATerm (TYPE_name, [arg])]
    1.87 +         else []
    1.88         | _ => [])))
    1.89  fun formulas_for_types type_enc add_sorts_on_typ Ts =
    1.90    [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
    1.91 @@ -1779,18 +1783,19 @@
    1.92  
    1.93  (** Symbol declarations **)
    1.94  
    1.95 -fun decl_line_for_class s =
    1.96 +fun decl_line_for_class order s =
    1.97    let val name as (s, _) = `make_type_class s in
    1.98      Decl (sym_decl_prefix ^ s, name,
    1.99 -          if exploit_tff1_dummy_type_vars then
   1.100 -            AFun (atype_of_types, bool_atype)
   1.101 +          if order = First_Order andalso avoid_first_order_dummy_type_vars then
   1.102 +            ATyAbs ([tvar_a_name], AFun (a_itself_atype, bool_atype))
   1.103            else
   1.104 -            ATyAbs ([tvar_a_name], AFun (a_itself_atype, bool_atype)))
   1.105 +            AFun (atype_of_types, bool_atype))
   1.106    end
   1.107  
   1.108  fun decl_lines_for_classes type_enc classes =
   1.109    case type_enc of
   1.110 -    Simple_Types (_, Polymorphic, _) => map decl_line_for_class classes
   1.111 +    Simple_Types (order, Polymorphic, _) =>
   1.112 +    map (decl_line_for_class order) classes
   1.113    | _ => []
   1.114  
   1.115  fun sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
   1.116 @@ -2232,7 +2237,8 @@
   1.117              CNF => ensure_cnf_problem
   1.118            | CNF_UEQ => filter_cnf_ueq_problem
   1.119            | FOF => I
   1.120 -          | TFF (_, TFF_Implicit) => I
   1.121 +          | TFF (_, TPTP_Implicit) => I
   1.122 +          | THF (_, TPTP_Implicit, _) => I
   1.123            | _ => declare_undeclared_syms_in_atp_problem type_decl_prefix
   1.124                                                          implicit_declsN)
   1.125      val (problem, pool) = problem |> nice_atp_problem readable_names