1679 fun should_specialize_helper type_enc t = |
1679 fun should_specialize_helper type_enc t = |
1680 polymorphism_of_type_enc type_enc <> Polymorphic andalso |
1680 polymorphism_of_type_enc type_enc <> Polymorphic andalso |
1681 level_of_type_enc type_enc <> No_Types andalso |
1681 level_of_type_enc type_enc <> No_Types andalso |
1682 not (null (Term.hidden_polymorphism t)) |
1682 not (null (Term.hidden_polymorphism t)) |
1683 |
1683 |
1684 fun add_helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) = |
1684 fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) = |
1685 case unprefix_and_unascii const_prefix s of |
1685 case unprefix_and_unascii const_prefix s of |
1686 SOME mangled_s => |
1686 SOME mangled_s => |
1687 let |
1687 let |
1688 val thy = Proof_Context.theory_of ctxt |
1688 val thy = Proof_Context.theory_of ctxt |
1689 val unmangled_s = mangled_s |> unmangled_const_name |> hd |
1689 val unmangled_s = mangled_s |> unmangled_const_name |> hd |
1703 |> tag_list 1 |
1703 |> tag_list 1 |
1704 |> map (fn (k, t) => ((dub needs_fairly_sound j k, (Global, Def)), t)) |
1704 |> map (fn (k, t) => ((dub needs_fairly_sound j k, (Global, Def)), t)) |
1705 val make_facts = map_filter (make_fact ctxt format type_enc false) |
1705 val make_facts = map_filter (make_fact ctxt format type_enc false) |
1706 val fairly_sound = is_type_enc_fairly_sound type_enc |
1706 val fairly_sound = is_type_enc_fairly_sound type_enc |
1707 in |
1707 in |
1708 fold (fn ((helper_s, needs_fairly_sound), ths) => |
1708 helper_table |
1709 if helper_s <> unmangled_s orelse |
1709 |> maps (fn ((helper_s, needs_fairly_sound), ths) => |
1710 (needs_fairly_sound andalso not fairly_sound) then |
1710 if helper_s <> unmangled_s orelse |
1711 I |
1711 (needs_fairly_sound andalso not fairly_sound) then |
1712 else |
1712 [] |
1713 ths ~~ (1 upto length ths) |
1713 else |
1714 |> maps (dub_and_inst needs_fairly_sound) |
1714 ths ~~ (1 upto length ths) |
1715 |> make_facts |
1715 |> maps (dub_and_inst needs_fairly_sound) |
1716 |> union (op = o pairself #iformula)) |
1716 |> make_facts) |
1717 helper_table |
|
1718 end |
1717 end |
1719 | NONE => I |
1718 | NONE => [] |
1720 fun helper_facts_for_sym_table ctxt format type_enc sym_tab = |
1719 fun helper_facts_for_sym_table ctxt format type_enc sym_tab = |
1721 Symtab.fold_rev (add_helper_facts_for_sym ctxt format type_enc) sym_tab [] |
1720 Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab |
|
1721 [] |
1722 |
1722 |
1723 (***************************************************************) |
1723 (***************************************************************) |
1724 (* Type Classes Present in the Axiom or Conjecture Clauses *) |
1724 (* Type Classes Present in the Axiom or Conjecture Clauses *) |
1725 (***************************************************************) |
1725 (***************************************************************) |
1726 |
1726 |