src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 42558 3d9930cb6770
parent 42557 ae0deb39a254
child 42560 7bb3796a4975
equal deleted inserted replaced
42557:ae0deb39a254 42558:3d9930cb6770
    74   {name: string,
    74   {name: string,
    75    kind: formula_kind,
    75    kind: formula_kind,
    76    combformula: (name, combtyp, combterm) formula,
    76    combformula: (name, combtyp, combterm) formula,
    77    ctypes_sorts: typ list}
    77    ctypes_sorts: typ list}
    78 
    78 
    79 fun map_combformula f
    79 fun update_combformula f
    80         ({name, kind, combformula, ctypes_sorts} : translated_formula) =
    80         ({name, kind, combformula, ctypes_sorts} : translated_formula) =
    81   {name = name, kind = kind, combformula = f combformula,
    81   {name = name, kind = kind, combformula = f combformula,
    82    ctypes_sorts = ctypes_sorts} : translated_formula
    82    ctypes_sorts = ctypes_sorts} : translated_formula
       
    83 
       
    84 fun fact_lift f ({combformula, ...} : translated_formula) = f combformula
    83 
    85 
    84 datatype type_system =
    86 datatype type_system =
    85   Many_Typed |
    87   Many_Typed |
    86   Mangled of bool |
    88   Mangled of bool |
    87   Args of bool |
    89   Args of bool |
   637 
   639 
   638 (** "hBOOL" and "hAPP" **)
   640 (** "hBOOL" and "hAPP" **)
   639 
   641 
   640 type repair_info = {pred_sym: bool, min_arity: int, max_arity: int}
   642 type repair_info = {pred_sym: bool, min_arity: int, max_arity: int}
   641 
   643 
   642 fun consider_combterm_for_repair top_level tm =
   644 fun consider_combterm_for_repair explicit_apply =
   643   let val (head, args) = strip_combterm_comb tm in
   645   let
   644     (case head of
   646     fun aux top_level tm =
   645        CombConst ((s, _), _, _) =>
   647       let val (head, args) = strip_combterm_comb tm in
   646        if String.isPrefix bound_var_prefix s then
   648         (case head of
   647          I
   649            CombConst ((s, _), _, _) =>
   648        else
   650            if String.isPrefix bound_var_prefix s then
   649          let val n = length args in
   651              I
   650            Symtab.map_default
   652            else
   651                (s, {pred_sym = true, min_arity = n, max_arity = 0})
   653              let val arity = length args in
   652                (fn {pred_sym, min_arity, max_arity} =>
   654                Symtab.map_default
   653                    {pred_sym = pred_sym andalso top_level,
   655                    (s, {pred_sym = true,
   654                     min_arity = Int.min (n, min_arity),
   656                         min_arity = if explicit_apply then 0 else arity,
   655                     max_arity = Int.max (n, max_arity)})
   657                         max_arity = 0})
   656         end
   658                    (fn {pred_sym, min_arity, max_arity} =>
   657      | _ => I)
   659                        {pred_sym = pred_sym andalso top_level,
   658     #> fold (consider_combterm_for_repair false) args
   660                         min_arity = Int.min (arity, min_arity),
   659   end
   661                         max_arity = Int.max (arity, max_arity)})
   660 
   662             end
   661 fun consider_fact_for_repair ({combformula, ...} : translated_formula) =
   663          | _ => I)
   662   formula_fold (consider_combterm_for_repair true) combformula
   664         #> fold (aux false) args
       
   665       end
       
   666   in aux true end
       
   667 
       
   668 fun consider_fact_for_repair explicit_apply =
       
   669   fact_lift (formula_fold (consider_combterm_for_repair explicit_apply))
   663 
   670 
   664 (* The "equal" entry is needed for helper facts if the problem otherwise does
   671 (* The "equal" entry is needed for helper facts if the problem otherwise does
   665    not involve equality. The "$false" and $"true" entries are needed to ensure
   672    not involve equality. The "$false" and $"true" entries are needed to ensure
   666    that no "hBOOL" is introduced for them. The "hBOOL" entry is needed to ensure
   673    that no "hBOOL" is introduced for them. The "hBOOL" entry is needed to ensure
   667    that no "hAPP"s are introduced for passing arguments to it. *)
   674    that no "hAPP"s are introduced for passing arguments to it. *)
   671    ("$true", {pred_sym = true, min_arity = 0, max_arity = 0}),
   678    ("$true", {pred_sym = true, min_arity = 0, max_arity = 0}),
   672    (make_fixed_const boolify_base,
   679    (make_fixed_const boolify_base,
   673     {pred_sym = true, min_arity = 1, max_arity = 1})]
   680     {pred_sym = true, min_arity = 1, max_arity = 1})]
   674 
   681 
   675 fun sym_table_for_facts explicit_apply facts =
   682 fun sym_table_for_facts explicit_apply facts =
   676   if explicit_apply then
   683   Symtab.empty |> fold Symtab.default default_sym_table_entries
   677     NONE
   684                |> fold (consider_fact_for_repair explicit_apply) facts
   678   else
   685 
   679     SOME (Symtab.empty |> fold Symtab.default default_sym_table_entries
   686 fun min_arity_of sym_tab s =
   680                        |> fold consider_fact_for_repair facts)
   687   case Symtab.lookup sym_tab s of
   681 
   688     SOME ({min_arity, ...} : repair_info) => min_arity
   682 fun min_arity_of (SOME sym_tab) s =
   689   | NONE =>
   683     (case Symtab.lookup sym_tab s of
   690     case strip_prefix_and_unascii const_prefix s of
   684        SOME ({min_arity, ...} : repair_info) => min_arity
       
   685      | NONE => 0)
       
   686   | min_arity_of NONE s =
       
   687     if s = "equal" then
       
   688       2
       
   689     else case strip_prefix_and_unascii const_prefix s of
       
   690       SOME s =>
   691       SOME s =>
   691       let val s = s |> unmangled_const |> fst |> invert_const in
   692       let val s = s |> unmangled_const |> fst |> invert_const in
   692         if s = boolify_base then 1
   693         if s = boolify_base then 1
   693         else if s = explicit_app_base then 2
   694         else if s = explicit_app_base then 2
   694         else if s = type_pred_base then 1
   695         else if s = type_pred_base then 1
   698 
   699 
   699 (* True if the constant ever appears outside of the top-level position in
   700 (* True if the constant ever appears outside of the top-level position in
   700    literals, or if it appears with different arities (e.g., because of different
   701    literals, or if it appears with different arities (e.g., because of different
   701    type instantiations). If false, the constant always receives all of its
   702    type instantiations). If false, the constant always receives all of its
   702    arguments and is used as a predicate. *)
   703    arguments and is used as a predicate. *)
   703 fun is_pred_sym (SOME sym_tab) s =
   704 fun is_pred_sym sym_tab s =
   704     (case Symtab.lookup sym_tab s of
   705   case Symtab.lookup sym_tab s of
   705        SOME {pred_sym, min_arity, max_arity} =>
   706     SOME {pred_sym, min_arity, max_arity} =>
   706        pred_sym andalso min_arity = max_arity
   707     pred_sym andalso min_arity = max_arity
   707      | NONE => false)
   708   | NONE => false
   708   | is_pred_sym NONE s =
       
   709     (case AList.lookup (op =) default_sym_table_entries s of
       
   710        SOME {pred_sym, ...} => pred_sym
       
   711      | NONE => false)
       
   712 
   709 
   713 val boolify_combconst =
   710 val boolify_combconst =
   714   CombConst (`make_fixed_const boolify_base,
   711   CombConst (`make_fixed_const boolify_base,
   715              combtyp_from_typ @{typ "bool => bool"}, [])
   712              combtyp_from_typ @{typ "bool => bool"}, [])
   716 fun boolify tm = CombApp (boolify_combconst, tm)
   713 fun boolify tm = CombApp (boolify_combconst, tm)
   750 fun repair_combterm type_sys sym_tab =
   747 fun repair_combterm type_sys sym_tab =
   751   repair_pred_syms_in_combterm sym_tab
   748   repair_pred_syms_in_combterm sym_tab
   752   #> repair_apps_in_combterm sym_tab
   749   #> repair_apps_in_combterm sym_tab
   753   #> repair_combterm_consts type_sys
   750   #> repair_combterm_consts type_sys
   754 val repair_combformula = formula_map oo repair_combterm
   751 val repair_combformula = formula_map oo repair_combterm
   755 val repair_fact = map_combformula oo repair_combformula
   752 val repair_fact = update_combformula oo repair_combformula
   756 
   753 
   757 fun is_const_relevant type_sys sym_tab s =
   754 fun is_const_relevant type_sys sym_tab s =
   758   not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso
   755   not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso
   759   (type_sys = Many_Typed orelse not (is_pred_sym sym_tab s))
   756   (type_sys = Many_Typed orelse not (is_pred_sym sym_tab s))
   760 
   757 
   767        ? Symtab.insert_list (op =) (s, (s', ty_args, ty))
   764        ? Symtab.insert_list (op =) (s, (s', ty_args, ty))
   768      | _ => I)
   765      | _ => I)
   769     #> fold (consider_combterm_consts type_sys sym_tab) args
   766     #> fold (consider_combterm_consts type_sys sym_tab) args
   770   end
   767   end
   771 
   768 
   772 fun consider_fact_consts type_sys sym_tab
   769 fun consider_fact_consts type_sys sym_tab =
   773                          ({combformula, ...} : translated_formula) =
   770   fact_lift (formula_fold (consider_combterm_consts type_sys sym_tab))
   774   formula_fold (consider_combterm_consts type_sys sym_tab) combformula
       
   775 
   771 
   776 (* FIXME: needed? *)
   772 (* FIXME: needed? *)
   777 fun const_table_for_facts type_sys sym_tab facts =
   773 fun const_table_for_facts type_sys sym_tab facts =
   778   Symtab.empty |> member (op =) [Many_Typed, Mangled true, Args true] type_sys
   774   Symtab.empty |> member (op =) [Many_Typed, Mangled true, Args true] type_sys
   779                   ? fold (consider_fact_consts type_sys sym_tab) facts
   775                   ? fold (consider_fact_consts type_sys sym_tab) facts