# HG changeset patch # User blanchet # Date 1305637896 -7200 # Node ID 1558741f8a72f39c56fc8e050740314e06791742 # Parent 8794ec73ec1377f586c6c9ab0b626cfb24098d5a started implementing "shallow" type systems, based on ideas by Claessen et al. diff -r 8794ec73ec13 -r 1558741f8a72 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Tue May 17 15:11:36 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Tue May 17 15:11:36 2011 +0200 @@ -151,10 +151,6 @@ | level_of_type_sys (Preds (_, level, _)) = level | level_of_type_sys (Tags (_, level, _)) = level -fun depth_of_type_sys (Simple_Types _) = Shallow - | depth_of_type_sys (Preds (_, _, depth)) = depth - | depth_of_type_sys (Tags (_, _, depth)) = depth - fun is_type_level_virtually_sound level = level = All_Types orelse level = Nonmonotonic_Types val is_type_sys_virtually_sound = @@ -203,7 +199,7 @@ s <> type_pred_base andalso s <> type_tag_name andalso (s = @{const_name HOL.eq} orelse level_of_type_sys type_sys = No_Types orelse (case type_sys of - Tags (_, All_Types, _) => true + Tags (_, All_Types, Deep) => true | _ => polymorphism_of_type_sys type_sys <> Mangled_Monomorphic andalso member (op =) boring_consts s)) @@ -213,8 +209,6 @@ Mangled_Type_Args of bool | No_Type_Args -(* FIXME: Find out whether and when erasing the non-result type arguments is - sound. *) fun general_type_arg_policy type_sys = if level_of_type_sys type_sys = No_Types then No_Type_Args @@ -497,13 +491,23 @@ exists (curry Type.raw_instance T) nonmono_Ts | should_encode_type _ _ _ _ = false -fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, _)) T = - should_encode_type ctxt nonmono_Ts level T +fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, depth)) T = + (case depth of + Deep => should_encode_type ctxt nonmono_Ts level T + | Shallow => error "Not implemented yet.") | should_predicate_on_type _ _ _ _ = false -fun should_tag_with_type ctxt nonmono_Ts (Tags (_, level, _)) T = - should_encode_type ctxt nonmono_Ts level T - | should_tag_with_type _ _ _ _ = false +datatype tag_site = Top_Level | Eq_Arg | Elsewhere + +fun should_tag_with_type _ _ _ Top_Level _ _ = false + | should_tag_with_type ctxt nonmono_Ts (Tags (_, level, depth)) site u T = + (case depth of + Deep => should_encode_type ctxt nonmono_Ts level T + | Shallow => + case (site, u) of + (Eq_Arg, CombVar _) => should_encode_type ctxt nonmono_Ts level T + | _ => false) + | should_tag_with_type _ _ _ _ _ _ = false val homo_infinite_T = @{typ ind} (* any infinite type *) @@ -772,31 +776,33 @@ |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys |> AAtom -fun formula_from_combformula ctxt nonmono_Ts type_sys = +fun tag_with_type ctxt nonmono_Ts type_sys T tm = + CombConst (`make_fixed_const type_tag_name, T --> T, [T]) + |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys + |> term_from_combterm ctxt nonmono_Ts type_sys Top_Level + |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])) +and term_from_combterm ctxt nonmono_Ts type_sys site u = let - fun tag_with_type type_sys T tm = - CombConst (`make_fixed_const type_tag_name, T --> T, [T]) - |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys - |> do_term true - |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])) - and do_term top_level u = - let - val (head, args) = strip_combterm_comb u - val (x, T_args) = - case head of - CombConst (name, _, T_args) => (name, T_args) - | CombVar (name, _) => (name, []) - | CombApp _ => raise Fail "impossible \"CombApp\"" - val t = ATerm (x, map fo_term_from_typ T_args @ - map (do_term false) args) - val T = combtyp_of u - in - t |> (if not top_level andalso - should_tag_with_type ctxt nonmono_Ts type_sys T then - tag_with_type type_sys T - else - I) - end + val (head, args) = strip_combterm_comb u + val (x as (s, _), T_args) = + case head of + CombConst (name, _, T_args) => (name, T_args) + | CombVar (name, _) => (name, []) + | CombApp _ => raise Fail "impossible \"CombApp\"" + val arg_site = if site = Top_Level andalso s = "equal" then Eq_Arg + else Elsewhere + val t = ATerm (x, map fo_term_from_typ T_args @ + map (term_from_combterm ctxt nonmono_Ts type_sys arg_site) + args) + val T = combtyp_of u + in + t |> (if should_tag_with_type ctxt nonmono_Ts type_sys site u T then + tag_with_type ctxt nonmono_Ts type_sys T + else + I) + end +and formula_from_combformula ctxt nonmono_Ts type_sys = + let val do_bound_type = case type_sys of Simple_Types level => @@ -817,7 +823,8 @@ | (s, SOME T) => do_out_of_bound_type (s, T)) xs) (do_formula phi)) | do_formula (AConn (c, phis)) = AConn (c, map do_formula phis) - | do_formula (AAtom tm) = AAtom (do_term true tm) + | do_formula (AAtom tm) = + AAtom (term_from_combterm ctxt nonmono_Ts type_sys Top_Level tm) in do_formula end fun bound_atomic_types type_sys Ts = @@ -940,22 +947,30 @@ (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it out with monotonicity" paper presented at CADE 2011. *) -fun add_combterm_nonmonotonic_types _ (SOME false) _ = I - | add_combterm_nonmonotonic_types ctxt _ +fun add_combterm_nonmonotonic_types _ _ (SOME false) _ = I + | add_combterm_nonmonotonic_types ctxt level _ (CombApp (CombApp (CombConst (("equal", _), Type (_, [T, _]), _), tm1), tm2)) = (exists is_var_or_bound_var [tm1, tm2] andalso - not (is_type_surely_infinite ctxt T)) ? insert_type I T - | add_combterm_nonmonotonic_types _ _ _ = I -fun add_fact_nonmonotonic_types ctxt ({kind, combformula, ...} - : translated_formula) = - formula_fold (kind <> Conjecture) (add_combterm_nonmonotonic_types ctxt) - combformula + (case level of + Nonmonotonic_Types => not (is_type_surely_infinite ctxt T) + | Finite_Types => is_type_surely_finite ctxt T + | _ => true)) ? insert_type I T + | add_combterm_nonmonotonic_types _ _ _ _ = I +fun add_fact_nonmonotonic_types ctxt level ({kind, combformula, ...} + : translated_formula) = + formula_fold (kind <> Conjecture) + (add_combterm_nonmonotonic_types ctxt level) combformula fun add_nonmonotonic_types_for_facts ctxt type_sys facts = - level_of_type_sys type_sys = Nonmonotonic_Types - ? (fold (add_fact_nonmonotonic_types ctxt) facts - (* in case helper "True_or_False" is included *) - #> insert_type I @{typ bool}) + let val level = level_of_type_sys type_sys in + (level = Nonmonotonic_Types orelse + (case type_sys of + Tags (poly, _, Shallow) => poly <> Polymorphic + | _ => false)) + ? (fold (add_fact_nonmonotonic_types ctxt level) facts + (* in case helper "True_or_False" is included *) + #> insert_type I @{typ bool}) + end fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd @@ -972,8 +987,8 @@ fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false -fun formula_line_for_sym_decl ctxt conj_sym_kind nonmono_Ts type_sys n s j - (s', T_args, T, _, ary, in_conj) = +fun formula_line_for_pred_sym_decl ctxt conj_sym_kind nonmono_Ts type_sys n s j + (s', T_args, T, _, ary, in_conj) = let val (kind, maybe_negate) = if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot) @@ -981,7 +996,7 @@ val (arg_Ts, res_T) = chop_fun ary T val bound_names = 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int) - val bound_tms = + val bounds = bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, [])) val bound_Ts = arg_Ts |> map (fn T => if n > 1 orelse is_polymorphic_type T then SOME T @@ -990,7 +1005,7 @@ Formula (sym_decl_prefix ^ s ^ (if n > 1 then "_" ^ string_of_int j else ""), kind, CombConst ((s, s'), T, T_args) - |> fold (curry (CombApp o swap)) bound_tms + |> fold (curry (CombApp o swap)) bounds |> type_pred_combatom ctxt nonmono_Ts type_sys res_T |> mk_aquant AForall (bound_names ~~ bound_Ts) |> formula_from_combformula ctxt nonmono_Ts type_sys @@ -1000,11 +1015,56 @@ NONE, NONE) end +fun formula_lines_for_tag_sym_decl ctxt nonmono_Ts type_sys n s + (j, (s', T_args, T, _, ary, _)) = + let + val ident_base = + sym_decl_prefix ^ s ^ (if n > 1 then "_" ^ string_of_int j else "") + val (arg_Ts, res_T) = chop_fun ary T + val bound_names = + 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int) + val bounds = bound_names |> map (fn name => ATerm (name, [])) + fun const args = ATerm ((s, s'), map fo_term_from_typ T_args @ args) + fun eq tm1 tm2 = ATerm (`I "equal", [tm1, tm2]) + val should_encode = + should_encode_type ctxt nonmono_Ts + (if polymorphism_of_type_sys type_sys = Polymorphic then All_Types + else Nonmonotonic_Types) + val tag_with = tag_with_type ctxt nonmono_Ts type_sys + val add_formula_for_res = + if should_encode res_T then + cons (Formula (ident_base ^ "_res", Axiom, + AAtom (eq (tag_with res_T (const bounds)) + (const bounds)) + |> close_formula_universally, + NONE, NONE)) + else + I + fun add_formula_for_arg k = + let val arg_T = nth arg_Ts k in + if should_encode arg_T then + case chop k bounds of + (bounds1, bound :: bounds2) => + cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), Axiom, + AAtom (eq (const (bounds1 @ + tag_with arg_T bound :: bounds2)) + (const bounds)) + |> close_formula_universally, + NONE, NONE)) + | _ => raise Fail "expected nonempty tail" + else + I + end + in + [] |> add_formula_for_res + |> fold add_formula_for_arg (ary - 1 downto 0) + end + fun problem_lines_for_sym_decls ctxt conj_sym_kind nonmono_Ts type_sys (s, decls) = case type_sys of Simple_Types level => map (decl_line_for_sym ctxt nonmono_Ts level s) decls - | _ => + | Preds _ => let val decls = case decls of @@ -1023,9 +1083,17 @@ o result_type_of_decl) in (0 upto length decls - 1, decls) - |-> map2 (formula_line_for_sym_decl ctxt conj_sym_kind nonmono_Ts type_sys - n s) + |-> map2 (formula_line_for_pred_sym_decl ctxt conj_sym_kind nonmono_Ts + type_sys n s) end + | Tags (_, _, depth) => + (case depth of + Deep => [] + | Shallow => + let val n = length decls in + (0 upto n - 1 ~~ decls) + |> maps (formula_lines_for_tag_sym_decl ctxt nonmono_Ts type_sys n s) + end) fun problem_lines_for_sym_decl_table ctxt conj_sym_kind nonmono_Ts type_sys sym_decl_tab = @@ -1094,7 +1162,7 @@ (0 upto length helpers - 1 ~~ helpers) |> (case type_sys of Tags (Polymorphic, level, _) => - is_type_level_partial level + is_type_level_partial level (* ### FIXME *) ? cons (ti_ti_helper_fact ()) | _ => I)), (conjsN, map (formula_line_for_conjecture ctxt nonmono_Ts type_sys)