src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 42998 1c80902d0456
parent 42994 fe291ab75eb5
child 43000 bd424c3dde46
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri May 27 10:30:07 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri May 27 10:30:07 2011 +0200
     1.3 @@ -81,8 +81,9 @@
     1.4  val readable_names =
     1.5    Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true)
     1.6  
     1.7 -val type_decl_prefix = "type_"
     1.8 -val sym_decl_prefix = "sym_"
     1.9 +val type_decl_prefix = "ty_"
    1.10 +val sym_decl_prefix = "sy_"
    1.11 +val sym_formula_prefix = "sym_"
    1.12  val fact_prefix = "fact_"
    1.13  val conjecture_prefix = "conj_"
    1.14  val helper_prefix = "help_"
    1.15 @@ -184,27 +185,6 @@
    1.16  fun is_setting_higher_order THF (Simple_Types _) = true
    1.17    | is_setting_higher_order _ _ = false
    1.18  
    1.19 -fun aconn_fold pos f (ANot, [phi]) = f (Option.map not pos) phi
    1.20 -  | aconn_fold pos f (AImplies, [phi1, phi2]) =
    1.21 -    f (Option.map not pos) phi1 #> f pos phi2
    1.22 -  | aconn_fold pos f (AAnd, phis) = fold (f pos) phis
    1.23 -  | aconn_fold pos f (AOr, phis) = fold (f pos) phis
    1.24 -  | aconn_fold _ f (_, phis) = fold (f NONE) phis
    1.25 -
    1.26 -fun aconn_map pos f (ANot, [phi]) = AConn (ANot, [f (Option.map not pos) phi])
    1.27 -  | aconn_map pos f (AImplies, [phi1, phi2]) =
    1.28 -    AConn (AImplies, [f (Option.map not pos) phi1, f pos phi2])
    1.29 -  | aconn_map pos f (AAnd, phis) = AConn (AAnd, map (f pos) phis)
    1.30 -  | aconn_map pos f (AOr, phis) = AConn (AOr, map (f pos) phis)
    1.31 -  | aconn_map _ f (c, phis) = AConn (c, map (f NONE) phis)
    1.32 -
    1.33 -fun formula_fold pos f =
    1.34 -  let
    1.35 -    fun aux pos (AQuant (_, _, phi)) = aux pos phi
    1.36 -      | aux pos (AConn conn) = aconn_fold pos aux conn
    1.37 -      | aux pos (AAtom tm) = f pos tm
    1.38 -  in aux pos end
    1.39 -
    1.40  type translated_formula =
    1.41    {name: string,
    1.42     locality: locality,
    1.43 @@ -282,8 +262,7 @@
    1.44  fun close_combformula_universally phi = close_universally combterm_vars phi
    1.45  
    1.46  fun term_vars (ATerm (name as (s, _), tms)) =
    1.47 -  is_atp_variable s ? insert (op =) (name, NONE)
    1.48 -  #> fold term_vars tms
    1.49 +  is_tptp_variable s ? insert (op =) (name, NONE) #> fold term_vars tms
    1.50  fun close_formula_universally phi = close_universally term_vars phi
    1.51  
    1.52  val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
    1.53 @@ -311,14 +290,15 @@
    1.54      f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
    1.55      ^ ")"
    1.56  
    1.57 +val bool_atype = AType (`I tptp_bool_type)
    1.58 +
    1.59  fun ho_type_from_fo_term higher_order pred_sym ary =
    1.60    let
    1.61      fun to_atype ty =
    1.62        AType ((make_simple_type (generic_mangled_type_name fst ty),
    1.63                generic_mangled_type_name snd ty))
    1.64      fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
    1.65 -    fun to_fo 0 ty =
    1.66 -        if pred_sym then AType (`I tptp_bool_type) else to_atype ty
    1.67 +    fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
    1.68        | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
    1.69      fun to_ho (ty as ATerm ((s, _), tys)) =
    1.70        if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
    1.71 @@ -1013,8 +993,7 @@
    1.72    end
    1.73  
    1.74  fun should_declare_sym type_sys pred_sym s =
    1.75 -  not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso
    1.76 -  not (String.isPrefix tptp_special_prefix s) andalso
    1.77 +  is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso
    1.78    (case type_sys of
    1.79       Simple_Types _ => true
    1.80     | Tags (_, _, Light) => true
    1.81 @@ -1086,7 +1065,7 @@
    1.82          Simple_Types level => (format = THF, [], level)
    1.83        | _ => (false, replicate (length T_args) homo_infinite_type, No_Types)
    1.84    in
    1.85 -    Decl (type_decl_prefix ^ s, (s, s'),
    1.86 +    Decl (sym_decl_prefix ^ s, (s, s'),
    1.87            (T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary))
    1.88            |> mangled_type higher_order pred_sym (length T_arg_Ts + ary))
    1.89    end
    1.90 @@ -1108,7 +1087,7 @@
    1.91        arg_Ts |> map (fn T => if n > 1 orelse is_polymorphic_type T then SOME T
    1.92                               else NONE)
    1.93    in
    1.94 -    Formula (sym_decl_prefix ^ s ^
    1.95 +    Formula (sym_formula_prefix ^ s ^
    1.96               (if n > 1 then "_" ^ string_of_int j else ""), kind,
    1.97               CombConst ((s, s'), T, T_args)
    1.98               |> fold (curry (CombApp o swap)) bounds
    1.99 @@ -1126,7 +1105,7 @@
   1.100          n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =
   1.101    let
   1.102      val ident_base =
   1.103 -      sym_decl_prefix ^ s ^ (if n > 1 then "_" ^ string_of_int j else "")
   1.104 +      sym_formula_prefix ^ s ^ (if n > 1 then "_" ^ string_of_int j else "")
   1.105      val (kind, maybe_negate) =
   1.106        if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
   1.107        else (Axiom, I)
   1.108 @@ -1173,74 +1152,50 @@
   1.109  
   1.110  fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts type_sys
   1.111                                  (s, decls) =
   1.112 -  (if member (op =) [TFF, THF] format then
   1.113 -     decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_sys s)
   1.114 -   else
   1.115 -     []) @
   1.116 -  (case type_sys of
   1.117 -     Simple_Types _ => []
   1.118 -   | Preds _ =>
   1.119 -     let
   1.120 -       val decls =
   1.121 -         case decls of
   1.122 -           decl :: (decls' as _ :: _) =>
   1.123 -           let val T = result_type_of_decl decl in
   1.124 -             if forall (curry (type_instance ctxt o swap) T
   1.125 -                        o result_type_of_decl) decls' then
   1.126 -               [decl]
   1.127 -             else
   1.128 -               decls
   1.129 -           end
   1.130 -         | _ => decls
   1.131 -       val n = length decls
   1.132 -       val decls =
   1.133 -         decls
   1.134 -         |> filter (should_predicate_on_type ctxt nonmono_Ts type_sys (K true)
   1.135 -                    o result_type_of_decl)
   1.136 -     in
   1.137 -       (0 upto length decls - 1, decls)
   1.138 -       |-> map2 (formula_line_for_pred_sym_decl ctxt format conj_sym_kind
   1.139 -                                                nonmono_Ts type_sys n s)
   1.140 -     end
   1.141 -   | Tags (_, _, heaviness) =>
   1.142 -     (case heaviness of
   1.143 -        Heavy => []
   1.144 -      | Light =>
   1.145 -        let val n = length decls in
   1.146 -          (0 upto n - 1 ~~ decls)
   1.147 -          |> maps (formula_lines_for_tag_sym_decl ctxt format conj_sym_kind
   1.148 -                                                  nonmono_Ts type_sys n s)
   1.149 -        end))
   1.150 +  case type_sys of
   1.151 +    Simple_Types _ =>
   1.152 +    decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_sys s)
   1.153 +  | Preds _ =>
   1.154 +    let
   1.155 +      val decls =
   1.156 +        case decls of
   1.157 +          decl :: (decls' as _ :: _) =>
   1.158 +          let val T = result_type_of_decl decl in
   1.159 +            if forall (curry (type_instance ctxt o swap) T
   1.160 +                       o result_type_of_decl) decls' then
   1.161 +              [decl]
   1.162 +            else
   1.163 +              decls
   1.164 +          end
   1.165 +        | _ => decls
   1.166 +      val n = length decls
   1.167 +      val decls =
   1.168 +        decls
   1.169 +        |> filter (should_predicate_on_type ctxt nonmono_Ts type_sys (K true)
   1.170 +                   o result_type_of_decl)
   1.171 +    in
   1.172 +      (0 upto length decls - 1, decls)
   1.173 +      |-> map2 (formula_line_for_pred_sym_decl ctxt format conj_sym_kind
   1.174 +                                               nonmono_Ts type_sys n s)
   1.175 +    end
   1.176 +  | Tags (_, _, heaviness) =>
   1.177 +    (case heaviness of
   1.178 +       Heavy => []
   1.179 +     | Light =>
   1.180 +       let val n = length decls in
   1.181 +         (0 upto n - 1 ~~ decls)
   1.182 +         |> maps (formula_lines_for_tag_sym_decl ctxt format conj_sym_kind
   1.183 +                                                 nonmono_Ts type_sys n s)
   1.184 +       end)
   1.185  
   1.186  fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
   1.187                                       type_sys sym_decl_tab =
   1.188 -  Symtab.fold_rev
   1.189 -      (append o problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts
   1.190 -                                            type_sys)
   1.191 -      sym_decl_tab []
   1.192 -
   1.193 -fun add_simple_types_in_type (AFun (ty1, ty2)) =
   1.194 -    fold add_simple_types_in_type [ty1, ty2]
   1.195 -  | add_simple_types_in_type (AType name) = insert (op =) name
   1.196 -
   1.197 -fun add_simple_types_in_formula (AQuant (_, xs, phi)) =
   1.198 -    fold add_simple_types_in_type (map_filter snd xs)
   1.199 -    #> add_simple_types_in_formula phi
   1.200 -  | add_simple_types_in_formula (AConn (_, phis)) =
   1.201 -    fold add_simple_types_in_formula phis
   1.202 -  | add_simple_types_in_formula (AAtom _) = I
   1.203 -
   1.204 -fun add_simple_types_in_problem_line (Decl (_, _, ty)) =
   1.205 -    add_simple_types_in_type ty
   1.206 -  | add_simple_types_in_problem_line (Formula (_, _, phi, _, _)) =
   1.207 -    add_simple_types_in_formula phi
   1.208 -
   1.209 -fun simple_types_in_problem problem =
   1.210 -  fold (fold add_simple_types_in_problem_line o snd) problem []
   1.211 -  |> filter_out (String.isPrefix tptp_special_prefix o fst)
   1.212 -
   1.213 -fun decl_line_for_simple_type (s, s') =
   1.214 -  Decl (type_decl_prefix ^ s, (s, s'), AType (`I tptp_type_of_types))
   1.215 +  sym_decl_tab
   1.216 +  |> Symtab.dest
   1.217 +  |> sort_wrt fst
   1.218 +  |> rpair []
   1.219 +  |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
   1.220 +                                                     nonmono_Ts type_sys)
   1.221  
   1.222  fun should_add_ti_ti_helper (Tags (Polymorphic, level, Heavy)) =
   1.223      level = Nonmonotonic_Types orelse level = Finite_Types
   1.224 @@ -1251,8 +1206,8 @@
   1.225      if heading = needle then j
   1.226      else offset_of_heading_in_problem needle problem (j + length lines)
   1.227  
   1.228 -val type_declsN = "Types"
   1.229 -val sym_declsN = "Symbol types"
   1.230 +val implicit_declsN = "Should-be-implicit typings"
   1.231 +val explicit_declsN = "Explicit typings"
   1.232  val factsN = "Relevant facts"
   1.233  val class_relsN = "Class relationships"
   1.234  val aritiesN = "Arities"
   1.235 @@ -1293,7 +1248,7 @@
   1.236      (* Reordering these might confuse the proof reconstruction code or the SPASS
   1.237         Flotter hack. *)
   1.238      val problem =
   1.239 -      [(sym_declsN, sym_decl_lines),
   1.240 +      [(explicit_declsN, sym_decl_lines),
   1.241         (factsN,
   1.242          map (formula_line_for_fact ctxt format fact_prefix nonmono_Ts type_sys)
   1.243              (0 upto length facts - 1 ~~ facts)),
   1.244 @@ -1307,13 +1262,12 @@
   1.245          formula_lines_for_free_types format type_sys (facts @ conjs))]
   1.246      val problem =
   1.247        problem
   1.248 -      |> (case type_sys of
   1.249 -            Simple_Types _ =>
   1.250 -            cons (type_declsN, problem |> simple_types_in_problem
   1.251 -                                       |> map decl_line_for_simple_type)
   1.252 -          | _ => I)
   1.253 -    val problem =
   1.254 -      problem |> (if format = CNF_UEQ then filter_cnf_ueq_problem else I)
   1.255 +      |> (if format = CNF_UEQ then filter_cnf_ueq_problem else I)
   1.256 +      |> (if is_format_typed format then
   1.257 +            declare_undeclared_syms_in_atp_problem type_decl_prefix
   1.258 +                                                   implicit_declsN
   1.259 +          else
   1.260 +            I)
   1.261      val (problem, pool) =
   1.262        problem |> nice_atp_problem (Config.get ctxt readable_names)
   1.263      val helpers_offset = offset_of_heading_in_problem helpersN problem 0
   1.264 @@ -1348,8 +1302,7 @@
   1.265  val type_info_default_weight = 0.8
   1.266  
   1.267  fun add_term_weights weight (ATerm (s, tms)) =
   1.268 -  (not (is_atp_variable s) andalso s <> "equal" andalso
   1.269 -   not (String.isPrefix tptp_special_prefix s)) ? Symtab.default (s, weight)
   1.270 +  is_tptp_user_symbol s ? Symtab.default (s, weight)
   1.271    #> fold (add_term_weights weight) tms
   1.272  fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
   1.273      formula_fold NONE (K (add_term_weights weight)) phi
   1.274 @@ -1380,7 +1333,7 @@
   1.275      |> add_conjectures_weights (get free_typesN @ get conjsN)
   1.276      |> add_facts_weights (get factsN)
   1.277      |> fold (fold (add_problem_line_weights type_info_default_weight) o get)
   1.278 -            [sym_declsN, class_relsN, aritiesN]
   1.279 +            [explicit_declsN, class_relsN, aritiesN]
   1.280      |> Symtab.dest
   1.281      |> sort (prod_ord Real.compare string_ord o pairself swap)
   1.282    end