src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 43000 bd424c3dde46
parent 42998 1c80902d0456
child 43001 f3492698dfc7
equal deleted inserted replaced
42999:0db96016bdbf 43000:bd424c3dde46
   340 
   340 
   341 fun introduce_proxies format type_sys tm =
   341 fun introduce_proxies format type_sys tm =
   342   let
   342   let
   343     fun aux ary top_level (CombApp (tm1, tm2)) =
   343     fun aux ary top_level (CombApp (tm1, tm2)) =
   344         CombApp (aux (ary + 1) top_level tm1, aux 0 false tm2)
   344         CombApp (aux (ary + 1) top_level tm1, aux 0 false tm2)
   345       | aux ary top_level (CombConst (name as (s, s'), T, T_args)) =
   345       | aux ary top_level (CombConst (name as (s, _), T, T_args)) =
   346         (case proxify_const s of
   346         (case proxify_const s of
   347            SOME proxy_base =>
   347            SOME (proxy_ary, proxy_base) =>
   348            (* Proxies are not needed in THF, except for partially applied
   348            if top_level orelse is_setting_higher_order format type_sys then
   349               equality since THF does not provide any syntax for it. *)
   349              case (top_level, s) of
   350            if top_level orelse
   350                (_, "c_False") => (`I tptp_false, [])
   351               (is_setting_higher_order format type_sys andalso
   351              | (_, "c_True") => (`I tptp_true, [])
   352                (s <> "equal" orelse ary = 2)) then
   352              | (false, "c_Not") => (`I tptp_not, [])
   353              (case s of
   353              | (false, "c_conj") => (`I tptp_and, [])
   354                 "c_False" => (tptp_false, s')
   354              | (false, "c_disj") => (`I tptp_or, [])
   355               | "c_True" => (tptp_true, s')
   355              | (false, "c_implies") => (`I tptp_implies, [])
   356               | _ => name, [])
   356              | (false, s) =>
       
   357                (* Proxies are not needed in THF, but we generate them for "="
       
   358                   when it is not fully applied to work around parsing bugs in
       
   359                   the provers ("= @ x @ x" is challenging to some). *)
       
   360                if is_tptp_equal s andalso ary = proxy_ary then
       
   361                  (`I tptp_equal, [])
       
   362                else
       
   363                  (proxy_base |>> prefix const_prefix, T_args)
       
   364              | _ => (name, [])
   357            else
   365            else
   358              (proxy_base |>> prefix const_prefix, T_args)
   366              (proxy_base |>> prefix const_prefix, T_args)
   359           | NONE => (name, T_args))
   367           | NONE => (name, T_args))
   360         |> (fn (name, T_args) => CombConst (name, T, T_args))
   368         |> (fn (name, T_args) => CombConst (name, T, T_args))
   361       | aux _ _ tm = tm
   369       | aux _ _ tm = tm
   592   in aux true end
   600   in aux true end
   593 fun add_fact_syms_to_table explicit_apply =
   601 fun add_fact_syms_to_table explicit_apply =
   594   fact_lift (formula_fold NONE (K (add_combterm_syms_to_table explicit_apply)))
   602   fact_lift (formula_fold NONE (K (add_combterm_syms_to_table explicit_apply)))
   595 
   603 
   596 val default_sym_table_entries : (string * sym_info) list =
   604 val default_sym_table_entries : (string * sym_info) list =
   597   [("equal", {pred_sym = true, min_ary = 2, max_ary = 2, typ = NONE}),
   605   [(tptp_equal, {pred_sym = true, min_ary = 2, max_ary = 2, typ = NONE}),
       
   606    (tptp_old_equal, {pred_sym = true, min_ary = 2, max_ary = 2, typ = NONE}),
   598    (make_fixed_const predicator_name,
   607    (make_fixed_const predicator_name,
   599     {pred_sym = true, min_ary = 1, max_ary = 1, typ = NONE})] @
   608     {pred_sym = true, min_ary = 1, max_ary = 1, typ = NONE})] @
   600   ([tptp_false, tptp_true]
   609   ([tptp_false, tptp_true]
   601    |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, typ = NONE}))
   610    |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, typ = NONE}))
   602 
   611 
   749   let
   758   let
   750     fun var s = ATerm (`I s, [])
   759     fun var s = ATerm (`I s, [])
   751     fun tag tm = ATerm (`make_fixed_const type_tag_name, [var "X", tm])
   760     fun tag tm = ATerm (`make_fixed_const type_tag_name, [var "X", tm])
   752   in
   761   in
   753     Formula (helper_prefix ^ "ti_ti", Axiom,
   762     Formula (helper_prefix ^ "ti_ti", Axiom,
   754              AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")]))
   763              AAtom (ATerm (`I tptp_equal, [tag (tag (var "Y")), tag (var "Y")]))
   755              |> close_formula_universally, simp_info, NONE)
   764              |> close_formula_universally, simp_info, NONE)
   756   end
   765   end
   757 
   766 
   758 fun helper_facts_for_sym ctxt format type_sys (s, {typ, ...} : sym_info) =
   767 fun helper_facts_for_sym ctxt format type_sys (s, {typ, ...} : sym_info) =
   759   case strip_prefix_and_unascii const_prefix s of
   768   case strip_prefix_and_unascii const_prefix s of
   837            |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys,
   846            |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys,
   838            tm)
   847            tm)
   839 
   848 
   840 fun var_occurs_positively_naked_in_term _ (SOME false) _ accum = accum
   849 fun var_occurs_positively_naked_in_term _ (SOME false) _ accum = accum
   841   | var_occurs_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
   850   | var_occurs_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
   842     accum orelse (s = "equal" andalso member (op =) tms (ATerm (name, [])))
   851     accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
   843 fun is_var_nonmonotonic_in_formula _ _ (SOME false) _ = false
   852 fun is_var_nonmonotonic_in_formula _ _ (SOME false) _ = false
   844   | is_var_nonmonotonic_in_formula pos phi _ name =
   853   | is_var_nonmonotonic_in_formula pos phi _ name =
   845     formula_fold pos (var_occurs_positively_naked_in_term name) phi false
   854     formula_fold pos (var_occurs_positively_naked_in_term name) phi false
   846 
   855 
   847 fun mk_const_aterm x T_args args =
   856 fun mk_const_aterm x T_args args =
   860         val (x as (s, _), T_args) =
   869         val (x as (s, _), T_args) =
   861           case head of
   870           case head of
   862             CombConst (name, _, T_args) => (name, T_args)
   871             CombConst (name, _, T_args) => (name, T_args)
   863           | CombVar (name, _) => (name, [])
   872           | CombVar (name, _) => (name, [])
   864           | CombApp _ => raise Fail "impossible \"CombApp\""
   873           | CombApp _ => raise Fail "impossible \"CombApp\""
   865         val arg_site = if site = Top_Level andalso s = "equal" then Eq_Arg
   874         val arg_site = if site = Top_Level andalso is_tptp_equal s then Eq_Arg
   866                        else Elsewhere
   875                        else Elsewhere
   867         val t = mk_const_aterm x T_args (map (aux arg_site) args)
   876         val t = mk_const_aterm x T_args (map (aux arg_site) args)
   868         val T = combtyp_of u
   877         val T = combtyp_of u
   869       in
   878       in
   870         t |> (if should_tag_with_type ctxt nonmono_Ts type_sys site u T then
   879         t |> (if should_tag_with_type ctxt nonmono_Ts type_sys site u T then
  1030 
  1039 
  1031 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
  1040 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
  1032    out with monotonicity" paper presented at CADE 2011. *)
  1041    out with monotonicity" paper presented at CADE 2011. *)
  1033 fun add_combterm_nonmonotonic_types _ _ (SOME false) _ = I
  1042 fun add_combterm_nonmonotonic_types _ _ (SOME false) _ = I
  1034   | add_combterm_nonmonotonic_types ctxt level _
  1043   | add_combterm_nonmonotonic_types ctxt level _
  1035         (CombApp (CombApp (CombConst (("equal", _), Type (_, [T, _]), _), tm1),
  1044         (CombApp (CombApp (CombConst ((s, _), Type (_, [T, _]), _), tm1), tm2)) =
  1036                   tm2)) =
  1045     (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
  1037     (exists is_var_or_bound_var [tm1, tm2] andalso
       
  1038      (case level of
  1046      (case level of
  1039         Nonmonotonic_Types =>
  1047         Nonmonotonic_Types =>
  1040         not (is_type_surely_infinite ctxt known_infinite_types T)
  1048         not (is_type_surely_infinite ctxt known_infinite_types T)
  1041       | Finite_Types => is_type_surely_finite ctxt T
  1049       | Finite_Types => is_type_surely_finite ctxt T
  1042       | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
  1050       | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
  1115     val bounds = bound_names |> map (fn name => ATerm (name, []))
  1123     val bounds = bound_names |> map (fn name => ATerm (name, []))
  1116     val cst = mk_const_aterm (s, s') T_args
  1124     val cst = mk_const_aterm (s, s') T_args
  1117     val atomic_Ts = atyps_of T
  1125     val atomic_Ts = atyps_of T
  1118     fun eq tms =
  1126     fun eq tms =
  1119       (if pred_sym then AConn (AIff, map AAtom tms)
  1127       (if pred_sym then AConn (AIff, map AAtom tms)
  1120        else AAtom (ATerm (`I "equal", tms)))
  1128        else AAtom (ATerm (`I tptp_equal, tms)))
  1121       |> bound_atomic_types format type_sys atomic_Ts
  1129       |> bound_atomic_types format type_sys atomic_Ts
  1122       |> close_formula_universally
  1130       |> close_formula_universally
  1123       |> maybe_negate
  1131       |> maybe_negate
  1124     val should_encode = should_encode_type ctxt nonmono_Ts All_Types
  1132     val should_encode = should_encode_type ctxt nonmono_Ts All_Types
  1125     val tag_with = tag_with_type ctxt format nonmono_Ts type_sys
  1133     val tag_with = tag_with_type ctxt format nonmono_Ts type_sys