src/HOL/Tools/ATP/atp_translate.ML
changeset 43139 9ed5d8ad8fa0
parent 43136 cf5cda219058
child 43159 29b55f292e0b
equal deleted inserted replaced
43138:818521a90356 43139:9ed5d8ad8fa0
  1054                  else (ho_var_Ts', Symtab.map (K repair_min_arity) sym_tab)
  1054                  else (ho_var_Ts', Symtab.map (K repair_min_arity) sym_tab)
  1055                end
  1055                end
  1056              else
  1056              else
  1057                accum
  1057                accum
  1058            else
  1058            else
  1059              let
  1059              let val ary = length args in
  1060                val ary = length args
       
  1061              in
       
  1062                (ho_var_Ts,
  1060                (ho_var_Ts,
  1063                 case Symtab.lookup sym_tab s of
  1061                 case Symtab.lookup sym_tab s of
  1064                   SOME {pred_sym, min_ary, max_ary, types} =>
  1062                   SOME {pred_sym, min_ary, max_ary, types} =>
  1065                   let
  1063                   let
  1066                     val types' = types |> insert_type ctxt I T
  1064                     val types' = types |> insert_type ctxt I T
  1097   in add true end
  1095   in add true end
  1098 fun add_fact_syms_to_table ctxt explicit_apply =
  1096 fun add_fact_syms_to_table ctxt explicit_apply =
  1099   fact_lift (formula_fold NONE
  1097   fact_lift (formula_fold NONE
  1100                           (K (add_combterm_syms_to_table ctxt explicit_apply)))
  1098                           (K (add_combterm_syms_to_table ctxt explicit_apply)))
  1101 
  1099 
  1102 val default_sym_table_entries : (string * sym_info) list =
  1100 val default_sym_tab_entries : (string * sym_info) list =
  1103   [(tptp_equal, {pred_sym = true, min_ary = 2, max_ary = 2, types = []}),
  1101   (make_fixed_const predicator_name,
  1104    (tptp_old_equal, {pred_sym = true, min_ary = 2, max_ary = 2, types = []}),
  1102    {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) ::
  1105    (make_fixed_const predicator_name,
       
  1106     {pred_sym = true, min_ary = 1, max_ary = 1, types = []})] @
       
  1107   ([tptp_false, tptp_true]
  1103   ([tptp_false, tptp_true]
  1108    |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []}))
  1104    |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @
       
  1105   ([tptp_equal, tptp_old_equal]
       
  1106    |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []}))
  1109 
  1107 
  1110 fun sym_table_for_facts ctxt explicit_apply facts =
  1108 fun sym_table_for_facts ctxt explicit_apply facts =
  1111   Symtab.empty
  1109   Symtab.empty
  1112   |> fold Symtab.default default_sym_table_entries
       
  1113   |> pair [] |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
  1110   |> pair [] |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
       
  1111   |> fold Symtab.update default_sym_tab_entries
  1114 
  1112 
  1115 fun min_arity_of sym_tab s =
  1113 fun min_arity_of sym_tab s =
  1116   case Symtab.lookup sym_tab s of
  1114   case Symtab.lookup sym_tab s of
  1117     SOME ({min_ary, ...} : sym_info) => min_ary
  1115     SOME ({min_ary, ...} : sym_info) => min_ary
  1118   | NONE =>
  1116   | NONE =>