6 Translation of HOL to FOL for Sledgehammer. |
6 Translation of HOL to FOL for Sledgehammer. |
7 *) |
7 *) |
8 |
8 |
9 signature ATP_TRANSLATE = |
9 signature ATP_TRANSLATE = |
10 sig |
10 sig |
11 type 'a fo_term = 'a ATP_Problem.fo_term |
11 type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term |
12 type connective = ATP_Problem.connective |
12 type connective = ATP_Problem.connective |
13 type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula |
13 type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula |
14 type format = ATP_Problem.format |
14 type format = ATP_Problem.format |
15 type formula_kind = ATP_Problem.formula_kind |
15 type formula_kind = ATP_Problem.formula_kind |
16 type 'a problem = 'a ATP_Problem.problem |
16 type 'a problem = 'a ATP_Problem.problem |
81 val is_type_enc_virtually_sound : type_enc -> bool |
81 val is_type_enc_virtually_sound : type_enc -> bool |
82 val is_type_enc_fairly_sound : type_enc -> bool |
82 val is_type_enc_fairly_sound : type_enc -> bool |
83 val choose_format : format list -> type_enc -> format * type_enc |
83 val choose_format : format list -> type_enc -> format * type_enc |
84 val mk_aconns : |
84 val mk_aconns : |
85 connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula |
85 connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula |
86 val unmangled_const : string -> string * string fo_term list |
86 val unmangled_const : string -> string * (string, 'b) ho_term list |
87 val unmangled_const_name : string -> string |
87 val unmangled_const_name : string -> string |
88 val helper_table : ((string * bool) * thm list) list |
88 val helper_table : ((string * bool) * thm list) list |
89 val factsN : string |
89 val factsN : string |
90 val prepare_atp_problem : |
90 val prepare_atp_problem : |
91 Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool |
91 Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool |
543 |> (fn (poly, (level, (heaviness, core))) => |
543 |> (fn (poly, (level, (heaviness, core))) => |
544 case (core, (poly, level, heaviness)) of |
544 case (core, (poly, level, heaviness)) of |
545 ("simple", (NONE, _, Lightweight)) => |
545 ("simple", (NONE, _, Lightweight)) => |
546 Simple_Types (First_Order, level) |
546 Simple_Types (First_Order, level) |
547 | ("simple_higher", (NONE, _, Lightweight)) => |
547 | ("simple_higher", (NONE, _, Lightweight)) => |
548 Simple_Types (Higher_Order, level) |
548 if level = Noninf_Nonmono_Types then raise Same.SAME |
|
549 else Simple_Types (Higher_Order, level) |
549 | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness) |
550 | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness) |
550 | ("tags", (SOME Polymorphic, _, _)) => |
551 | ("tags", (SOME Polymorphic, _, _)) => |
551 Tags (Polymorphic, level, heaviness) |
552 Tags (Polymorphic, level, heaviness) |
552 | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness) |
553 | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness) |
553 | ("args", (SOME poly, All_Types (* naja *), Lightweight)) => |
554 | ("args", (SOME poly, All_Types (* naja *), Lightweight)) => |
696 fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2] |
697 fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2] |
697 | combterm_vars (CombConst _) = I |
698 | combterm_vars (CombConst _) = I |
698 | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T) |
699 | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T) |
699 fun close_combformula_universally phi = close_universally combterm_vars phi |
700 fun close_combformula_universally phi = close_universally combterm_vars phi |
700 |
701 |
701 fun term_vars (ATerm (name as (s, _), tms)) = |
702 fun term_vars bounds (ATerm (name as (s, _), tms)) = |
702 is_tptp_variable s ? insert (op =) (name, NONE) #> fold term_vars tms |
703 (is_tptp_variable s andalso not (member (op =) bounds name)) |
703 fun close_formula_universally phi = close_universally term_vars phi |
704 ? insert (op =) (name, NONE) #> fold (term_vars bounds) tms |
|
705 | term_vars bounds (AAbs ((name, _), tm)) = term_vars (name :: bounds) tm |
|
706 fun close_formula_universally phi = close_universally (term_vars []) phi |
704 |
707 |
705 val homo_infinite_type_name = @{type_name ind} (* any infinite type *) |
708 val homo_infinite_type_name = @{type_name ind} (* any infinite type *) |
706 val homo_infinite_type = Type (homo_infinite_type_name, []) |
709 val homo_infinite_type = Type (homo_infinite_type_name, []) |
707 |
710 |
708 fun fo_term_from_typ format type_enc = |
711 fun ho_term_from_typ format type_enc = |
709 let |
712 let |
710 fun term (Type (s, Ts)) = |
713 fun term (Type (s, Ts)) = |
711 ATerm (case (is_type_enc_higher_order type_enc, s) of |
714 ATerm (case (is_type_enc_higher_order type_enc, s) of |
712 (true, @{type_name bool}) => `I tptp_bool_type |
715 (true, @{type_name bool}) => `I tptp_bool_type |
713 | (true, @{type_name fun}) => `I tptp_fun_type |
716 | (true, @{type_name fun}) => `I tptp_fun_type |
720 | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, []) |
723 | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, []) |
721 | term (TVar ((x as (s, _)), _)) = |
724 | term (TVar ((x as (s, _)), _)) = |
722 ATerm ((make_schematic_type_var x, s), []) |
725 ATerm ((make_schematic_type_var x, s), []) |
723 in term end |
726 in term end |
724 |
727 |
725 fun fo_term_for_type_arg format type_enc T = |
728 fun ho_term_for_type_arg format type_enc T = |
726 if T = dummyT then NONE else SOME (fo_term_from_typ format type_enc T) |
729 if T = dummyT then NONE else SOME (ho_term_from_typ format type_enc T) |
727 |
730 |
728 (* This shouldn't clash with anything else. *) |
731 (* This shouldn't clash with anything else. *) |
729 val mangled_type_sep = "\000" |
732 val mangled_type_sep = "\000" |
730 |
733 |
731 fun generic_mangled_type_name f (ATerm (name, [])) = f name |
734 fun generic_mangled_type_name f (ATerm (name, [])) = f name |
732 | generic_mangled_type_name f (ATerm (name, tys)) = |
735 | generic_mangled_type_name f (ATerm (name, tys)) = |
733 f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys) |
736 f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys) |
734 ^ ")" |
737 ^ ")" |
|
738 | generic_mangled_type_name f _ = raise Fail "unexpected type abstraction" |
735 |
739 |
736 val bool_atype = AType (`I tptp_bool_type) |
740 val bool_atype = AType (`I tptp_bool_type) |
737 |
741 |
738 fun make_simple_type s = |
742 fun make_simple_type s = |
739 if s = tptp_bool_type orelse s = tptp_fun_type orelse |
743 if s = tptp_bool_type orelse s = tptp_fun_type orelse |
740 s = tptp_individual_type then |
744 s = tptp_individual_type then |
741 s |
745 s |
742 else |
746 else |
743 simple_type_prefix ^ ascii_of s |
747 simple_type_prefix ^ ascii_of s |
744 |
748 |
745 fun ho_type_from_fo_term type_enc pred_sym ary = |
749 fun ho_type_from_ho_term type_enc pred_sym ary = |
746 let |
750 let |
747 fun to_atype ty = |
751 fun to_atype ty = |
748 AType ((make_simple_type (generic_mangled_type_name fst ty), |
752 AType ((make_simple_type (generic_mangled_type_name fst ty), |
749 generic_mangled_type_name snd ty)) |
753 generic_mangled_type_name snd ty)) |
750 fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1)) |
754 fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1)) |
751 fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty |
755 fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty |
752 | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys |
756 | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys |
|
757 | to_fo ary _ = raise Fail "unexpected type abstraction" |
753 fun to_ho (ty as ATerm ((s, _), tys)) = |
758 fun to_ho (ty as ATerm ((s, _), tys)) = |
754 if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty |
759 if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty |
|
760 | to_ho _ = raise Fail "unexpected type abstraction" |
755 in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end |
761 in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end |
756 |
762 |
757 fun mangled_type format type_enc pred_sym ary = |
763 fun mangled_type format type_enc pred_sym ary = |
758 ho_type_from_fo_term type_enc pred_sym ary |
764 ho_type_from_ho_term type_enc pred_sym ary |
759 o fo_term_from_typ format type_enc |
765 o ho_term_from_typ format type_enc |
760 |
766 |
761 fun mangled_const_name format type_enc T_args (s, s') = |
767 fun mangled_const_name format type_enc T_args (s, s') = |
762 let |
768 let |
763 val ty_args = T_args |> map_filter (fo_term_for_type_arg format type_enc) |
769 val ty_args = T_args |> map_filter (ho_term_for_type_arg format type_enc) |
764 fun type_suffix f g = |
770 fun type_suffix f g = |
765 fold_rev (curry (op ^) o g o prefix mangled_type_sep |
771 fold_rev (curry (op ^) o g o prefix mangled_type_sep |
766 o generic_mangled_type_name f) ty_args "" |
772 o generic_mangled_type_name f) ty_args "" |
767 in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end |
773 in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end |
768 |
774 |
1442 |> enforce_type_arg_policy_in_combterm ctxt format type_enc, tm) |
1448 |> enforce_type_arg_policy_in_combterm ctxt format type_enc, tm) |
1443 |
1449 |
1444 fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum |
1450 fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum |
1445 | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum = |
1451 | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum = |
1446 accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, []))) |
1452 accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, []))) |
|
1453 | is_var_positively_naked_in_term name _ _ _ = true |
1447 fun should_predicate_on_var_in_formula pos phi (SOME true) name = |
1454 fun should_predicate_on_var_in_formula pos phi (SOME true) name = |
1448 formula_fold pos (is_var_positively_naked_in_term name) phi false |
1455 formula_fold pos (is_var_positively_naked_in_term name) phi false |
1449 | should_predicate_on_var_in_formula _ _ _ _ = true |
1456 | should_predicate_on_var_in_formula _ _ _ _ = true |
1450 |
1457 |
1451 fun mk_const_aterm format type_enc x T_args args = |
1458 fun mk_const_aterm format type_enc x T_args args = |
1452 ATerm (x, map_filter (fo_term_for_type_arg format type_enc) T_args @ args) |
1459 ATerm (x, map_filter (ho_term_for_type_arg format type_enc) T_args @ args) |
1453 |
1460 |
1454 fun tag_with_type ctxt format nonmono_Ts type_enc pos T tm = |
1461 fun tag_with_type ctxt format nonmono_Ts type_enc pos T tm = |
1455 CombConst (type_tag, T --> T, [T]) |
1462 CombConst (type_tag, T --> T, [T]) |
1456 |> enforce_type_arg_policy_in_combterm ctxt format type_enc |
1463 |> enforce_type_arg_policy_in_combterm ctxt format type_enc |
1457 |> term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos) |
1464 |> term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos) |
1922 val fact_min_weight = 0.2 |
1929 val fact_min_weight = 0.2 |
1923 val fact_max_weight = 1.0 |
1930 val fact_max_weight = 1.0 |
1924 val type_info_default_weight = 0.8 |
1931 val type_info_default_weight = 0.8 |
1925 |
1932 |
1926 fun add_term_weights weight (ATerm (s, tms)) = |
1933 fun add_term_weights weight (ATerm (s, tms)) = |
1927 is_tptp_user_symbol s ? Symtab.default (s, weight) |
1934 is_tptp_user_symbol s ? Symtab.default (s, weight) |
1928 #> fold (add_term_weights weight) tms |
1935 #> fold (add_term_weights weight) tms |
|
1936 | add_term_weights weight (AAbs (_, tm)) = add_term_weights weight tm |
1929 fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) = |
1937 fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) = |
1930 formula_fold NONE (K (add_term_weights weight)) phi |
1938 formula_fold NONE (K (add_term_weights weight)) phi |
1931 | add_problem_line_weights _ _ = I |
1939 | add_problem_line_weights _ _ = I |
1932 |
1940 |
1933 fun add_conjectures_weights [] = I |
1941 fun add_conjectures_weights [] = I |