src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 42576 a8a80a2a34be
parent 42575 ad700c4f2471
child 42577 78414ec6fa4e
equal deleted inserted replaced
42575:ad700c4f2471 42576:a8a80a2a34be
   751   not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso
   751   not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso
   752   (type_sys = Many_Typed orelse not pred_sym)
   752   (type_sys = Many_Typed orelse not pred_sym)
   753 
   753 
   754 fun add_combterm_syms_to_decl_table type_sys repaired_sym_tab =
   754 fun add_combterm_syms_to_decl_table type_sys repaired_sym_tab =
   755   let
   755   let
   756     fun aux tm =
   756     fun declare_sym (decl as (_, _, T, _, _)) decls =
       
   757       if exists (curry Type.raw_instance T o #3) decls then decls
       
   758       else decl :: filter_out ((fn T' => Type.raw_instance (T', T)) o #3) decls
       
   759     fun do_term tm =
   757       let val (head, args) = strip_combterm_comb tm in
   760       let val (head, args) = strip_combterm_comb tm in
   758         (case head of
   761         (case head of
   759            CombConst ((s, s'), T, T_args) =>
   762            CombConst ((s, s'), T, T_args) =>
   760            let val pred_sym = is_pred_sym repaired_sym_tab s in
   763            let val pred_sym = is_pred_sym repaired_sym_tab s in
   761              if should_declare_sym type_sys pred_sym s then
   764              if should_declare_sym type_sys pred_sym s then
   762                Symtab.insert_list (op =)
   765                Symtab.map_default (s, [])
   763                    (s, (s', T_args, T, pred_sym, length args))
   766                    (declare_sym (s', T_args, T, pred_sym, length args))
   764              else
   767              else
   765                I
   768                I
   766            end
   769            end
   767          | _ => I)
   770          | _ => I)
   768         #> fold aux args
   771         #> fold do_term args
   769       end
   772       end
   770   in aux end
   773   in do_term end
   771 fun add_fact_syms_to_decl_table type_sys repaired_sym_tab =
   774 fun add_fact_syms_to_decl_table type_sys repaired_sym_tab =
   772   fact_lift (formula_fold
   775   fact_lift (formula_fold
   773       (add_combterm_syms_to_decl_table type_sys repaired_sym_tab))
   776       (add_combterm_syms_to_decl_table type_sys repaired_sym_tab))
   774 fun sym_decl_table_for_facts type_sys repaired_sym_tab facts =
   777 fun sym_decl_table_for_facts type_sys repaired_sym_tab facts =
   775   Symtab.empty |> type_system_declares_sym_types type_sys
   778   Symtab.empty |> type_system_declares_sym_types type_sys