|
(* Title: HOL/Tools/ATP/atp_problem_generate.ML
Author: Fabian Immler, TU Muenchen
Author: Makarius
Author: Jasmin Blanchette, TU Muenchen
Author: Martin Desharnais, UniBw Muenchen
Translation of HOL to FOL for Metis and Sledgehammer.
*)
signature ATP_PROBLEM_GENERATE =
sig
type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term
type atp_connective = ATP_Problem.atp_connective
type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula
type atp_format = ATP_Problem.atp_format
type atp_formula_role = ATP_Problem.atp_formula_role
type 'a atp_problem = 'a ATP_Problem.atp_problem
datatype mode = Metis | Sledgehammer | Sledgehammer_Completish of int | Exporter | Translator
datatype scope = Global | Local | Assum | Chained
datatype status = General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def | Rec_Def
type stature = scope * status
datatype strictness = Strict | Non_Strict
datatype uniformity = Uniform | Non_Uniform
datatype ctr_optim = With_Ctr_Optim | Without_Ctr_Optim
datatype type_level =
All_Types |
Undercover_Types |
Nonmono_Types of strictness * uniformity |
Const_Types of ctr_optim |
No_Types
type type_enc
val no_lamsN : string
val hide_lamsN : string
val liftingN : string
val combsN : string
val combs_and_liftingN : string
val combs_or_liftingN : string
val lam_liftingN : string
val keep_lamsN : string
val schematic_var_prefix : string
val fixed_var_prefix : string
val tvar_prefix : string
val tfree_prefix : string
val const_prefix : string
val type_const_prefix : string
val class_prefix : string
val lam_lifted_prefix : string
val lam_lifted_mono_prefix : string
val lam_lifted_poly_prefix : string
val skolem_const_prefix : string
val old_skolem_const_prefix : string
val new_skolem_const_prefix : string
val combinator_prefix : string
val class_decl_prefix : string
val type_decl_prefix : string
val sym_decl_prefix : string
val datatype_decl_prefix : string
val class_memb_prefix : string
val guards_sym_formula_prefix : string
val tags_sym_formula_prefix : string
val fact_prefix : string
val conjecture_prefix : string
val helper_prefix : string
val subclass_prefix : string
val tcon_clause_prefix : string
val tfree_clause_prefix : string
val lam_fact_prefix : string
val typed_helper_suffix : string
val untyped_helper_suffix : string
val predicator_name : string
val app_op_name : string
val type_guard_name : string
val type_tag_name : string
val native_type_prefix : string
val prefixed_predicator_name : string
val prefixed_app_op_name : string
val prefixed_type_tag_name : string
val ascii_of : string -> string
val unascii_of : string -> string
val unprefix_and_unascii : string -> string -> string option
val proxy_table : (string * (string * (thm * (string * string)))) list
val proxify_const : string -> (string * string) option
val invert_const : string -> string
val unproxify_const : string -> string
val new_skolem_var_name_of_const : string -> string
val atp_logical_consts : string list
val atp_irrelevant_consts : string list
val atp_widely_irrelevant_consts : string list
val is_irrelevant_const : string -> bool
val is_widely_irrelevant_const : string -> bool
val atp_schematic_consts_of : term -> typ list Symtab.table
val is_type_enc_higher_order : type_enc -> bool
val is_type_enc_polymorphic : type_enc -> bool
val level_of_type_enc : type_enc -> type_level
val is_type_enc_sound : type_enc -> bool
val type_enc_of_string : strictness -> string -> type_enc
val adjust_type_enc : atp_format -> type_enc -> type_enc
val is_first_order_lambda_free : term -> bool
val do_cheaply_conceal_lambdas : typ list -> term -> term
val mk_aconns :
atp_connective -> ('a, 'b, 'c, 'd) atp_formula list
-> ('a, 'b, 'c, 'd) atp_formula
val unmangled_type : string -> (string, 'a) ATP_Problem.atp_term
val unmangled_const : string -> string * (string, 'b) atp_term list
val unmangled_const_name : string -> string list
val helper_table : ((string * bool) * (status * thm) list) list
val trans_lams_of_string :
Proof.context -> type_enc -> string -> term list -> term list * term list
val string_of_status : status -> string
val factsN : string
val generate_atp_problem : Proof.context -> bool -> atp_format -> atp_formula_role -> type_enc ->
mode -> string -> bool -> bool -> bool -> term list -> term ->
((string * stature) * term) list -> string atp_problem * string Symtab.table
* (string * term) list * int Symtab.table
val atp_problem_selection_weights : string atp_problem -> (string * real) list
val atp_problem_term_order_info : string atp_problem -> (string * int) list
end;
structure ATP_Problem_Generate : ATP_PROBLEM_GENERATE =
struct
open ATP_Util
open ATP_Problem
datatype mode = Metis | Sledgehammer | Sledgehammer_Completish of int | Exporter | Translator
datatype scope = Global | Local | Assum | Chained
datatype status = General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def | Rec_Def
type stature = scope * status
datatype order =
First_Order |
Higher_Order of thf_flavor
datatype phantom_policy = Without_Phantom_Type_Vars | With_Phantom_Type_Vars
datatype polymorphism =
Type_Class_Polymorphic |
Raw_Polymorphic of phantom_policy |
Raw_Monomorphic |
Mangled_Monomorphic
datatype strictness = Strict | Non_Strict
datatype uniformity = Uniform | Non_Uniform
datatype ctr_optim = With_Ctr_Optim | Without_Ctr_Optim
datatype type_level =
All_Types |
Undercover_Types |
Nonmono_Types of strictness * uniformity |
Const_Types of ctr_optim |
No_Types
datatype type_enc =
Native of order * fool * polymorphism * type_level |
Guards of polymorphism * type_level |
Tags of polymorphism * type_level
(* not clear whether ATPs prefer to have their negative variables tagged *)
val tag_neg_vars = false
fun is_type_enc_native (Native _) = true
| is_type_enc_native _ = false
fun is_type_enc_full_higher_order (Native (Higher_Order THF_Lambda_Free, _, _, _)) = false
| is_type_enc_full_higher_order (Native (Higher_Order _, _, _, _)) = true
| is_type_enc_full_higher_order _ = false
fun is_type_enc_fool (Native (_, With_FOOL, _, _)) = true
| is_type_enc_fool _ = false
fun is_type_enc_higher_order (Native (Higher_Order _, _, _, _)) = true
| is_type_enc_higher_order _ = false
fun polymorphism_of_type_enc (Native (_, _, poly, _)) = poly
| polymorphism_of_type_enc (Guards (poly, _)) = poly
| polymorphism_of_type_enc (Tags (poly, _)) = poly
fun is_type_enc_polymorphic type_enc =
(case polymorphism_of_type_enc type_enc of
Raw_Polymorphic _ => true
| Type_Class_Polymorphic => true
| _ => false)
fun is_type_enc_mangling type_enc =
polymorphism_of_type_enc type_enc = Mangled_Monomorphic
fun level_of_type_enc (Native (_, _, _, level)) = level
| level_of_type_enc (Guards (_, level)) = level
| level_of_type_enc (Tags (_, level)) = level
fun is_type_level_uniform (Nonmono_Types (_, Non_Uniform)) = false
| is_type_level_uniform Undercover_Types = false
| is_type_level_uniform _ = true
fun is_type_level_sound (Const_Types _) = false
| is_type_level_sound No_Types = false
| is_type_level_sound _ = true
val is_type_enc_sound = is_type_level_sound o level_of_type_enc
fun is_type_level_monotonicity_based (Nonmono_Types _) = true
| is_type_level_monotonicity_based _ = false
val no_lamsN = "no_lams" (* used internally; undocumented *)
val hide_lamsN = "hide_lams"
val liftingN = "lifting"
val combsN = "combs"
val combs_and_liftingN = "combs_and_lifting"
val combs_or_liftingN = "combs_or_lifting"
val keep_lamsN = "keep_lams"
val lam_liftingN = "lam_lifting" (* legacy FIXME: remove *)
val bound_var_prefix = "B_"
val all_bound_var_prefix = "A_"
val exist_bound_var_prefix = "E_"
val schematic_var_prefix = "V_"
val fixed_var_prefix = "v_"
val tvar_prefix = "T_"
val tfree_prefix = "tf_"
val const_prefix = "c_"
val type_const_prefix = "t_"
val native_type_prefix = "n_"
val class_prefix = "cl_"
(* Freshness almost guaranteed! *)
val atp_prefix = "ATP" ^ Long_Name.separator
val atp_weak_prefix = "ATP:"
val atp_weak_suffix = ":ATP"
val lam_lifted_prefix = atp_weak_prefix ^ "Lam"
val lam_lifted_mono_prefix = lam_lifted_prefix ^ "m"
val lam_lifted_poly_prefix = lam_lifted_prefix ^ "p"
val skolem_const_prefix = atp_prefix ^ "Sko"
val old_skolem_const_prefix = skolem_const_prefix ^ "o"
val new_skolem_const_prefix = skolem_const_prefix ^ "n"
val combinator_prefix = "COMB"
val class_decl_prefix = "cl_"
val type_decl_prefix = "ty_"
val sym_decl_prefix = "sy_"
val datatype_decl_prefix = "dt_"
val class_memb_prefix = "cm_"
val guards_sym_formula_prefix = "gsy_"
val tags_sym_formula_prefix = "tsy_"
val uncurried_alias_eq_prefix = "unc_"
val fact_prefix = "fact_"
val conjecture_prefix = "conj_"
val helper_prefix = "help_"
val subclass_prefix = "subcl_"
val tcon_clause_prefix = "tcon_"
val tfree_clause_prefix = "tfree_"
val lam_fact_prefix = "ATP.lambda_"
val typed_helper_suffix = "_T"
val untyped_helper_suffix = "_U"
val predicator_name = "pp"
val app_op_name = "aa"
val type_guard_name = "gg"
val type_tag_name = "tt"
val prefixed_predicator_name = const_prefix ^ predicator_name
val prefixed_app_op_name = const_prefix ^ app_op_name
val prefixed_type_tag_name = const_prefix ^ type_tag_name
(*Escaping of special characters.
Alphanumeric characters are left unchanged.
The character _ goes to __.
Characters in the range ASCII space to / go to _A to _P, respectively.
Other characters go to _nnn where nnn is the decimal ASCII code. *)
val upper_a_minus_space = Char.ord #"A" - Char.ord #" "
fun ascii_of_char c =
if Char.isAlphaNum c then
String.str c
else if c = #"_" then
"__"
else if #" " <= c andalso c <= #"/" then
"_" ^ String.str (Char.chr (Char.ord c + upper_a_minus_space))
else
(* fixed width, in case more digits follow *)
"_" ^ stringN_of_int 3 (Char.ord c)
val ascii_of = String.translate ascii_of_char
(** Remove ASCII armoring from names in proof files **)
(* We don't raise error exceptions because this code can run inside a worker
thread. Also, the errors are impossible. *)
val unascii_of =
let
fun un rcs [] = String.implode (rev rcs)
| un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *)
(* Three types of _ escapes: __, _A to _P, _nnn *)
| un rcs (#"_" :: #"_" :: cs) = un (#"_" :: rcs) cs
| un rcs (#"_" :: c :: cs) =
if #"A" <= c andalso c<= #"P" then
(* translation of #" " to #"/" *)
un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs
else
let val digits = List.take (c :: cs, 3) handle General.Subscript => [] in
(case Int.fromString (String.implode digits) of
SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))
| NONE => un (c :: #"_" :: rcs) cs (* ERROR *))
end
| un rcs (c :: cs) = un (c :: rcs) cs
in un [] o String.explode end
(* If string s has the prefix s1, return the result of deleting it,
un-ASCII'd. *)
fun unprefix_and_unascii s1 s =
if String.isPrefix s1 s then
SOME (unascii_of (String.extract (s, size s1, NONE)))
else
NONE
val proxy_table =
[("c_False", (\<^const_name>\<open>False\<close>, (@{thm fFalse_def}, ("fFalse", \<^const_name>\<open>fFalse\<close>)))),
("c_True", (\<^const_name>\<open>True\<close>, (@{thm fTrue_def}, ("fTrue", \<^const_name>\<open>fTrue\<close>)))),
("c_Not", (\<^const_name>\<open>Not\<close>, (@{thm fNot_def}, ("fNot", \<^const_name>\<open>fNot\<close>)))),
("c_conj", (\<^const_name>\<open>conj\<close>, (@{thm fconj_def}, ("fconj", \<^const_name>\<open>fconj\<close>)))),
("c_disj", (\<^const_name>\<open>disj\<close>, (@{thm fdisj_def}, ("fdisj", \<^const_name>\<open>fdisj\<close>)))),
("c_implies", (\<^const_name>\<open>implies\<close>, (@{thm fimplies_def}, ("fimplies", \<^const_name>\<open>fimplies\<close>)))),
("equal", (\<^const_name>\<open>HOL.eq\<close>, (@{thm fequal_def}, ("fequal", \<^const_name>\<open>fequal\<close>)))),
("c_All", (\<^const_name>\<open>All\<close>, (@{thm fAll_def}, ("fAll", \<^const_name>\<open>fAll\<close>)))),
("c_Ex", (\<^const_name>\<open>Ex\<close>, (@{thm fEx_def}, ("fEx", \<^const_name>\<open>fEx\<close>))))]
val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
(* Readable names for the more common symbolic functions. Do not mess with the
table unless you know what you are doing. *)
val const_trans_table =
[(\<^const_name>\<open>False\<close>, "False"),
(\<^const_name>\<open>True\<close>, "True"),
(\<^const_name>\<open>Not\<close>, "Not"),
(\<^const_name>\<open>conj\<close>, "conj"),
(\<^const_name>\<open>disj\<close>, "disj"),
(\<^const_name>\<open>implies\<close>, "implies"),
(\<^const_name>\<open>HOL.eq\<close>, "equal"),
(\<^const_name>\<open>All\<close>, "All"),
(\<^const_name>\<open>Ex\<close>, "Ex"),
(\<^const_name>\<open>If\<close>, "If"),
(\<^const_name>\<open>Set.member\<close>, "member"),
(\<^const_name>\<open>Meson.COMBI\<close>, combinator_prefix ^ "I"),
(\<^const_name>\<open>Meson.COMBK\<close>, combinator_prefix ^ "K"),
(\<^const_name>\<open>Meson.COMBB\<close>, combinator_prefix ^ "B"),
(\<^const_name>\<open>Meson.COMBC\<close>, combinator_prefix ^ "C"),
(\<^const_name>\<open>Meson.COMBS\<close>, combinator_prefix ^ "S")]
|> Symtab.make
|> fold (Symtab.update o swap o snd o snd o snd) proxy_table
(* Invert the table of translations between Isabelle and ATPs. *)
val const_trans_table_inv =
const_trans_table |> Symtab.dest |> map swap |> Symtab.make
val const_trans_table_unprox =
Symtab.empty
|> fold (fn (_, (isa, (_, (_, atp)))) => Symtab.update (atp, isa)) proxy_table
val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)
fun lookup_const c =
(case Symtab.lookup const_trans_table c of
SOME c' => c'
| NONE => ascii_of c)
fun ascii_of_indexname (v, 0) = ascii_of v
| ascii_of_indexname (v, i) = ascii_of v ^ "_" ^ string_of_int i
fun make_bound_var x = bound_var_prefix ^ ascii_of x
fun make_all_bound_var x = all_bound_var_prefix ^ ascii_of x
fun make_exist_bound_var x = exist_bound_var_prefix ^ ascii_of x
fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
fun make_tvar (s, i) = tvar_prefix ^ ascii_of_indexname (unquote_tvar s, i)
fun make_tfree s = tfree_prefix ^ ascii_of (unquote_tvar s)
fun tvar_name ((x as (s, _)), _) = (make_tvar x, s)
(* "HOL.eq" and choice are mapped to the ATP's equivalents *)
local
val choice_const = (fst o dest_Const o HOLogic.choice_const) dummyT
fun default c = const_prefix ^ lookup_const c
in
fun make_fixed_const _ \<^const_name>\<open>HOL.eq\<close> = tptp_old_equal
| make_fixed_const (SOME (Native (Higher_Order THF_With_Choice, _, _, _))) c =
if c = choice_const then tptp_choice else default c
| make_fixed_const _ c = default c
end
fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
fun make_class clas = class_prefix ^ ascii_of clas
fun new_skolem_var_name_of_const s =
let val ss = Long_Name.explode s
in nth ss (length ss - 2) end
(* These are ignored anyway by the relevance filter (unless they appear in
higher-order places) but not by the monomorphizer. *)
val atp_logical_consts =
[\<^const_name>\<open>Pure.prop\<close>, \<^const_name>\<open>Pure.conjunction\<close>,
\<^const_name>\<open>Pure.all\<close>, \<^const_name>\<open>Pure.imp\<close>, \<^const_name>\<open>Pure.eq\<close>,
\<^const_name>\<open>Trueprop\<close>, \<^const_name>\<open>All\<close>, \<^const_name>\<open>Ex\<close>,
\<^const_name>\<open>Ex1\<close>, \<^const_name>\<open>Ball\<close>, \<^const_name>\<open>Bex\<close>]
(* These are either simplified away by "Meson.presimplify" (most of the time) or
handled specially via "fFalse", "fTrue", ..., "fequal". *)
val atp_irrelevant_consts =
[\<^const_name>\<open>False\<close>, \<^const_name>\<open>True\<close>, \<^const_name>\<open>Not\<close>, \<^const_name>\<open>conj\<close>,
\<^const_name>\<open>disj\<close>, \<^const_name>\<open>implies\<close>, \<^const_name>\<open>HOL.eq\<close>, \<^const_name>\<open>If\<close>,
\<^const_name>\<open>Let\<close>]
val atp_widely_irrelevant_consts = atp_logical_consts @ atp_irrelevant_consts
val atp_irrelevant_const_tab = Symtab.make (map (rpair ()) atp_irrelevant_consts)
val atp_widely_irrelevant_const_tab = Symtab.make (map (rpair ()) atp_widely_irrelevant_consts)
val is_irrelevant_const = Symtab.defined atp_irrelevant_const_tab
val is_widely_irrelevant_const = Symtab.defined atp_widely_irrelevant_const_tab
fun add_schematic_const (x as (_, T)) =
Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x
val add_schematic_consts_of =
Term.fold_aterms (fn Const (x as (s, _)) =>
not (member (op =) atp_widely_irrelevant_consts s)
? add_schematic_const x
| _ => I)
fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
val tvar_a_str = "'a"
val tvar_a_z = ((tvar_a_str, 0), \<^sort>\<open>type\<close>)
val tvar_a = TVar tvar_a_z
val tvar_a_name = tvar_name tvar_a_z
val itself_name = `make_fixed_type_const \<^type_name>\<open>itself\<close>
val TYPE_name = `(make_fixed_const NONE) \<^const_name>\<open>Pure.type\<close>
val tvar_a_atype = AType ((tvar_a_name, []), [])
val a_itself_atype = AType ((itself_name, []), [tvar_a_atype])
(** Definitions and functions for FOL clauses and formulas for TPTP **)
(** Type class membership **)
(* In our data structures, [] exceptionally refers to the top class, not to
the empty class. *)
val class_of_types = the_single \<^sort>\<open>type\<close>
fun normalize_classes cls = if member (op =) cls class_of_types then [] else cls
(* Arity of type constructor "s :: (arg1, ..., argN) res" *)
fun make_axiom_tcon_clause (s, name, (cl, args)) =
let
val args = args |> map normalize_classes
val tvars =
1 upto length args |> map (fn j => TVar ((tvar_a_str, j), \<^sort>\<open>type\<close>))
in (name, args ~~ tvars, (cl, Type (s, tvars))) end
(* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in
theory thy provided its arguments have the corresponding sorts. *)
fun class_pairs thy tycons cls =
let
val alg = Sign.classes_of thy
fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
fun add_class tycon cl =
cons (cl, domain_sorts tycon cl)
handle Sorts.CLASS_ERROR _ => I
fun try_classes tycon = (tycon, fold (add_class tycon) cls [])
in map try_classes tycons end
(* Proving one (tycon, class) membership may require proving others, so
iterate. *)
fun all_class_pairs _ _ _ [] = ([], [])
| all_class_pairs thy tycons old_cls cls =
let
val old_cls' = cls @ old_cls
fun maybe_insert_class s = not (member (op =) old_cls' s) ? insert (op =) s
val pairs = class_pairs thy tycons cls
val new_cls = fold (fold (fold (fold maybe_insert_class) o snd) o snd) pairs []
val (cls', pairs') = all_class_pairs thy tycons old_cls' new_cls
in (cls' @ cls, union (op =) pairs' pairs) end
fun tcon_clause _ _ [] = []
| tcon_clause seen n ((_, []) :: rest) = tcon_clause seen n rest
| tcon_clause seen n ((tcons, (ar as (cl, _)) :: ars) :: rest) =
if cl = class_of_types then
tcon_clause seen n ((tcons, ars) :: rest)
else if member (op =) seen cl then
(* multiple clauses for the same (tycon, cl) pair *)
make_axiom_tcon_clause (tcons,
lookup_const tcons ^ "___" ^ ascii_of cl ^ "_" ^ string_of_int n, ar) ::
tcon_clause seen (n + 1) ((tcons, ars) :: rest)
else
make_axiom_tcon_clause (tcons, lookup_const tcons ^ "___" ^ ascii_of cl, ar) ::
tcon_clause (cl :: seen) n ((tcons, ars) :: rest)
fun make_tcon_clauses thy tycons =
all_class_pairs thy tycons [] ##> tcon_clause [] 1
(** Isabelle class relations **)
(* Generate a list ("sub", "supers") such that "sub" is a proper subclass of all
"supers". *)
fun make_subclass_pairs thy subs supers =
let
val class_less = curry (Sorts.class_less (Sign.classes_of thy))
fun supers_of sub = (sub, filter (class_less sub) supers)
in map supers_of subs |> filter_out (null o snd) end
(* intermediate terms *)
datatype iterm =
IConst of (string * string) * typ * typ list |
IVar of (string * string) * typ |
IApp of iterm * iterm |
IAbs of ((string * string) * typ) * iterm
fun ityp_of (IConst (_, T, _)) = T
| ityp_of (IVar (_, T)) = T
| ityp_of (IApp (t1, _)) = snd (dest_funT (ityp_of t1))
| ityp_of (IAbs ((_, T), tm)) = T --> ityp_of tm
(*gets the head of a combinator application, along with the list of arguments*)
fun strip_iterm_comb u =
let
fun stripc (IApp (t, u), ts) = stripc (t, u :: ts)
| stripc x = x
in stripc (u, []) end
fun atomic_types_of T = fold_atyps (insert (op =)) T []
fun new_skolem_const_name s num_T_args =
[new_skolem_const_prefix, s, string_of_int num_T_args]
|> Long_Name.implode
val alpha_to_beta = Logic.varifyT_global \<^typ>\<open>'a => 'b\<close>
val alpha_to_beta_to_alpha_to_beta = alpha_to_beta --> alpha_to_beta
fun robust_const_type thy s =
if s = app_op_name then
alpha_to_beta_to_alpha_to_beta
else if String.isPrefix lam_lifted_prefix s then
alpha_to_beta
else
(* Old Skolems throw a "TYPE" exception here, which will be caught. *)
s |> Sign.the_const_type thy
fun ary_of (Type (\<^type_name>\<open>fun\<close>, [_, T])) = 1 + ary_of T
| ary_of _ = 0
(* This function only makes sense if "T" is as general as possible. *)
fun robust_const_type_args thy (s, T) =
if s = app_op_name then
let val (T1, T2) = T |> domain_type |> dest_funT in [T1, T2] end
else if String.isPrefix old_skolem_const_prefix s then
[] |> Term.add_tvarsT T |> rev |> map TVar
else if String.isPrefix lam_lifted_prefix s then
if String.isPrefix lam_lifted_poly_prefix s then
let val (T1, T2) = T |> dest_funT in [T1, T2] end
else
[]
else
(s, T) |> Sign.const_typargs thy
(* Converts an Isabelle/HOL term (with combinators) into an intermediate term. Also accumulates sort
infomation. *)
fun iterm_of_term thy type_enc bs (P $ Q) =
let
val (P', P_atomics_Ts) = iterm_of_term thy type_enc bs P
val (Q', Q_atomics_Ts) = iterm_of_term thy type_enc bs Q
in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
| iterm_of_term thy type_enc _ (Const (c, T)) =
(IConst (`(make_fixed_const (SOME type_enc)) c, T, robust_const_type_args thy (c, T)),
atomic_types_of T)
| iterm_of_term _ _ _ (Free (s, T)) = (IConst (`make_fixed_var s, T, []), atomic_types_of T)
| iterm_of_term _ type_enc _ (Var (v as (s, _), T)) =
(if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
let
val Ts = T |> strip_type |> swap |> op ::
val s' = new_skolem_const_name s (length Ts)
in IConst (`(make_fixed_const (SOME type_enc)) s', T, Ts) end
else
IVar ((make_schematic_var v, s), T), atomic_types_of T)
| iterm_of_term _ _ bs (Bound j) =
nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atomic_types_of T))
| iterm_of_term thy type_enc bs (Abs (s, T, t)) =
let
fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
val s = vary s
val name = `make_bound_var s
val (tm, atomic_Ts) = iterm_of_term thy type_enc ((s, (name, T)) :: bs) t
in
(IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T))
end
(* "_query" and "_at" are for the ASCII-challenged Metis and Mirabelle. *)
val queries = ["?", "_query"]
val ats = ["@", "_at"]
fun try_unsuffixes ss s =
fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
fun type_enc_of_string strictness s =
let
val (poly, s) =
(case try (unprefix "tc_") s of
SOME s => (SOME Type_Class_Polymorphic, s)
| NONE =>
(case try (unprefix "poly_") s of
SOME s => (SOME (Raw_Polymorphic With_Phantom_Type_Vars), s)
| NONE =>
(case try (unprefix "ml_poly_") s of
SOME s => (SOME (Raw_Polymorphic Without_Phantom_Type_Vars), s)
| NONE =>
(case try (unprefix "raw_mono_") s of
SOME s => (SOME Raw_Monomorphic, s)
| NONE =>
(case try (unprefix "mono_") s of
SOME s => (SOME Mangled_Monomorphic, s)
| NONE => (NONE, s))))))
val (level, s) =
case try_unsuffixes queries s of
SOME s =>
(case try_unsuffixes queries s of
SOME s => (Nonmono_Types (strictness, Non_Uniform), s)
| NONE => (Nonmono_Types (strictness, Uniform), s))
| NONE =>
(case try_unsuffixes ats s of
SOME s => (Undercover_Types, s)
| NONE => (All_Types, s))
fun native_of_string s =
let
val (fool, core) =
(case try (unsuffix "_fool") s of
SOME s => (With_FOOL, s)
| NONE => (Without_FOOL, s))
in
(case (core, poly) of
("native", SOME poly) =>
(case (poly, level) of
(Mangled_Monomorphic, _) =>
if is_type_level_uniform level then
Native (First_Order, fool, Mangled_Monomorphic, level)
else
raise Same.SAME
| (Raw_Monomorphic, _) => raise Same.SAME
| (poly, All_Types) => Native (First_Order, fool, poly, All_Types))
| ("native_higher", SOME poly) =>
(case (poly, level) of
(_, Nonmono_Types _) => raise Same.SAME
| (_, Undercover_Types) => raise Same.SAME
| (Mangled_Monomorphic, _) =>
if is_type_level_uniform level then
Native (Higher_Order THF_With_Choice, fool, Mangled_Monomorphic, level)
else
raise Same.SAME
| (poly as Raw_Polymorphic _, All_Types) =>
Native (Higher_Order THF_With_Choice, fool, poly, All_Types)
| _ => raise Same.SAME))
end
fun nonnative_of_string core =
(case (core, poly, level) of
("guards", SOME poly, _) =>
if (poly = Mangled_Monomorphic andalso level = Undercover_Types) orelse
poly = Type_Class_Polymorphic then
raise Same.SAME
else
Guards (poly, level)
| ("tags", SOME poly, _) =>
if (poly = Mangled_Monomorphic andalso level = Undercover_Types) orelse
poly = Type_Class_Polymorphic then
raise Same.SAME
else
Tags (poly, level)
| ("args", SOME poly, All_Types (* naja *)) =>
if poly = Type_Class_Polymorphic then raise Same.SAME
else Guards (poly, Const_Types Without_Ctr_Optim)
| ("args", SOME poly, Nonmono_Types (_, Uniform) (* naja *)) =>
if poly = Mangled_Monomorphic orelse poly = Type_Class_Polymorphic then
raise Same.SAME
else
Guards (poly, Const_Types With_Ctr_Optim)
| ("erased", NONE, All_Types (* naja *)) =>
Guards (Raw_Polymorphic With_Phantom_Type_Vars, No_Types)
| _ => raise Same.SAME)
in
if String.isPrefix "native" s then
native_of_string s
else
nonnative_of_string s
end
handle Same.SAME => error ("Unknown type encoding: " ^ quote s)
fun min_hologic THF_Lambda_Free _ = THF_Lambda_Free
| min_hologic _ THF_Lambda_Free = THF_Lambda_Free
| min_hologic THF_Without_Choice _ = THF_Without_Choice
| min_hologic _ THF_Without_Choice = THF_Without_Choice
| min_hologic _ _ = THF_With_Choice
fun adjust_hologic hologic (Higher_Order hologic') = Higher_Order (min_hologic hologic hologic')
| adjust_hologic _ type_enc = type_enc
fun adjust_fool Without_FOOL _ = Without_FOOL
| adjust_fool _ fool = fool
fun no_type_classes Type_Class_Polymorphic = Raw_Polymorphic With_Phantom_Type_Vars
| no_type_classes poly = poly
fun adjust_type_enc (THF (fool, Polymorphic, hologic)) (Native (order, fool', poly, level)) =
Native (adjust_hologic hologic order, adjust_fool fool fool', no_type_classes poly, level)
| adjust_type_enc (THF (fool, Monomorphic, hologic)) (Native (order, fool', _, level)) =
Native (adjust_hologic hologic order, adjust_fool fool fool', Mangled_Monomorphic, level)
| adjust_type_enc (TFF (fool, Monomorphic)) (Native (_, fool', _, level)) =
Native (First_Order, adjust_fool fool fool', Mangled_Monomorphic, level)
| adjust_type_enc (DFG Polymorphic) (Native (_, _, poly, level)) =
Native (First_Order, Without_FOOL, poly, level)
| adjust_type_enc (DFG Monomorphic) (Native (_, _, _, level)) =
Native (First_Order, Without_FOOL, Mangled_Monomorphic, level)
| adjust_type_enc (TFF (fool, _)) (Native (_, fool', poly, level)) =
Native (First_Order, adjust_fool fool fool', no_type_classes poly, level)
| adjust_type_enc format (Native (_, _, poly, level)) =
adjust_type_enc format (Guards (no_type_classes poly, level))
| adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
(if is_type_enc_sound type_enc then Tags else Guards) stuff
| adjust_type_enc _ type_enc = type_enc
fun is_first_order_lambda_free t =
(case t of
\<^const>\<open>Not\<close> $ t1 => is_first_order_lambda_free t1
| Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t') => is_first_order_lambda_free t'
| Const (\<^const_name>\<open>All\<close>, _) $ t1 => is_first_order_lambda_free t1
| Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, _, t') => is_first_order_lambda_free t'
| Const (\<^const_name>\<open>Ex\<close>, _) $ t1 => is_first_order_lambda_free t1
| \<^const>\<open>HOL.conj\<close> $ t1 $ t2 => is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
| \<^const>\<open>HOL.disj\<close> $ t1 $ t2 => is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
| \<^const>\<open>HOL.implies\<close> $ t1 $ t2 =>
is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
| Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [\<^typ>\<open>bool\<close>, _])) $ t1 $ t2 =>
is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
| _ => not (exists_subterm (fn Abs _ => true | _ => false) t))
fun simple_translate_lambdas do_lambdas ctxt type_enc t =
if is_first_order_lambda_free t then
t
else
let
fun trans_first_order Ts t =
(case t of
\<^const>\<open>Not\<close> $ t1 => \<^const>\<open>Not\<close> $ trans_first_order Ts t1
| (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ Abs (s, T, t') =>
t0 $ Abs (s, T, trans_first_order (T :: Ts) t')
| (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ t1 =>
trans_first_order Ts (t0 $ eta_expand Ts t1 1)
| (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ Abs (s, T, t') =>
t0 $ Abs (s, T, trans_first_order (T :: Ts) t')
| (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ t1 =>
trans_first_order Ts (t0 $ eta_expand Ts t1 1)
| (t0 as \<^const>\<open>HOL.conj\<close>) $ t1 $ t2 =>
t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2
| (t0 as \<^const>\<open>HOL.disj\<close>) $ t1 $ t2 =>
t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2
| (t0 as \<^const>\<open>HOL.implies\<close>) $ t1 $ t2 =>
t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2
| (t0 as Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [\<^typ>\<open>bool\<close>, _]))) $ t1 $ t2 =>
t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2
| _ =>
if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
else t |> Envir.eta_contract |> do_lambdas ctxt Ts)
fun trans_fool Ts t =
(case t of
(t0 as Const (\<^const_name>\<open>All\<close>, _)) $ Abs (s, T, t') =>
t0 $ Abs (s, T, trans_fool (T :: Ts) t')
| (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ t1 => trans_fool Ts (t0 $ eta_expand Ts t1 1)
| (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ Abs (s, T, t') =>
t0 $ Abs (s, T, trans_fool (T :: Ts) t')
| (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ t1 => trans_fool Ts (t0 $ eta_expand Ts t1 1)
| t1 $ t2 => trans_fool Ts t1 $ trans_fool Ts t2
| Abs _ => t |> Envir.eta_contract |> do_lambdas ctxt Ts
| _ => t)
val trans = if is_type_enc_fool type_enc then trans_fool else trans_first_order
val (t, ctxt') = yield_singleton (Variable.import_terms true) t ctxt
in t |> trans [] |> singleton (Variable.export_terms ctxt' ctxt) end
fun do_cheaply_conceal_lambdas Ts (t1 $ t2) =
do_cheaply_conceal_lambdas Ts t1
$ do_cheaply_conceal_lambdas Ts t2
| do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) =
Const (lam_lifted_poly_prefix ^ serial_string (),
T --> fastype_of1 (T :: Ts, t))
| do_cheaply_conceal_lambdas _ t = t
fun concealed_bound_name j = atp_weak_prefix ^ string_of_int j
fun conceal_bounds Ts t =
subst_bounds (map (Free o apfst concealed_bound_name)
(0 upto length Ts - 1 ~~ Ts), t)
fun reveal_bounds Ts =
subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
(0 upto length Ts - 1 ~~ Ts))
fun do_introduce_combinators ctxt Ts t =
(t |> conceal_bounds Ts
|> Thm.cterm_of ctxt
|> Meson_Clausify.introduce_combinators_in_cterm ctxt
|> Thm.prop_of |> Logic.dest_equals |> snd
|> reveal_bounds Ts)
(* A type variable of sort "{}" will make abstraction fail. *)
handle THM _ => t |> do_cheaply_conceal_lambdas Ts
val introduce_combinators = simple_translate_lambdas do_introduce_combinators
fun constify_lifted (t $ u) = constify_lifted t $ constify_lifted u
| constify_lifted (Abs (s, T, t)) = Abs (s, T, constify_lifted t)
| constify_lifted (Free (x as (s, _))) =
(if String.isPrefix lam_lifted_prefix s then Const else Free) x
| constify_lifted t = t
fun lift_lams_part_1 ctxt type_enc =
map hol_close_form #> rpair ctxt
#-> Lambda_Lifting.lift_lambdas
(SOME ((if is_type_enc_polymorphic type_enc then
lam_lifted_poly_prefix
else
lam_lifted_mono_prefix) ^ "_a"))
Lambda_Lifting.is_quantifier
#> fst
fun lift_lams_part_2 ctxt type_enc (facts, lifted) =
(facts, lifted)
(* Lambda-lifting sometimes leaves some lambdas around; we need some way to
get rid of them *)
|> apply2 (map (introduce_combinators ctxt type_enc))
|> apply2 (map constify_lifted)
(* Requires bound variables not to clash with any schematic variables (as
should be the case right after lambda-lifting). *)
|>> map (hol_open_form (unprefix hol_close_form_prefix))
||> map (hol_open_form I)
fun lift_lams ctxt type_enc = lift_lams_part_2 ctxt type_enc o lift_lams_part_1 ctxt type_enc
fun intentionalize_def (Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t)) =
intentionalize_def t
| intentionalize_def (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ u) =
let
fun lam T t = Abs (Name.uu, T, t)
val (head, args) = strip_comb t ||> rev
val head_T = fastype_of head
val n = length args
val arg_Ts = head_T |> binder_types |> take n |> rev
val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
| intentionalize_def t = t
type ifact =
{name : string,
stature : stature,
role : atp_formula_role,
iformula : (string * string, typ, iterm, string * string) atp_formula,
atomic_types : typ list}
fun update_iformula f ({name, stature, role, iformula, atomic_types} : ifact) =
{name = name, stature = stature, role = role, iformula = f iformula, atomic_types = atomic_types}
: ifact
fun ifact_lift f ({iformula, ...} : ifact) = f iformula
fun insert_type thy get_T x xs =
let val T = get_T x in
if exists (type_instance thy T o get_T) xs then xs
else x :: filter_out (type_generalization thy T o get_T) xs
end
fun chop_fun 0 T = ([], T)
| chop_fun n (Type (\<^type_name>\<open>fun\<close>, [dom_T, ran_T])) =
chop_fun (n - 1) ran_T |>> cons dom_T
| chop_fun _ T = ([], T)
fun filter_type_args thy ctrss type_enc s ary T_args =
let val poly = polymorphism_of_type_enc type_enc in
if s = type_tag_name then (* FIXME: why not "type_guard_name" as well? *)
T_args
else
(case type_enc of
Native (_, _, Raw_Polymorphic _, _) => T_args
| Native (_, _, Type_Class_Polymorphic, _) => T_args
| _ =>
let
fun gen_type_args _ _ [] = []
| gen_type_args keep strip_ty T_args =
let
val U = robust_const_type thy s
val (binder_Us, body_U) = strip_ty U
val in_U_vars = fold Term.add_tvarsT binder_Us []
val out_U_vars = Term.add_tvarsT body_U []
fun filt (U_var, T) =
if keep (member (op =) in_U_vars U_var,
member (op =) out_U_vars U_var) then
T
else
dummyT
val U_args = (s, U) |> robust_const_type_args thy
in map (filt o apfst dest_TVar) (U_args ~~ T_args) end
handle TYPE _ => T_args
fun is_always_ctr (s', T') =
s' = s andalso type_equiv thy (T', robust_const_type thy s')
val noninfer_type_args = gen_type_args (not o fst) (chop_fun ary)
val ctr_infer_type_args = gen_type_args fst strip_type
val level = level_of_type_enc type_enc
in
if level = No_Types orelse s = \<^const_name>\<open>HOL.eq\<close> orelse
(case level of Const_Types _ => s = app_op_name | _ => false) then
[]
else if poly = Mangled_Monomorphic then
T_args
else if level = All_Types then
(case type_enc of
Guards _ => noninfer_type_args T_args
| Tags _ => [])
else if level = Undercover_Types then
noninfer_type_args T_args
else if level <> Const_Types Without_Ctr_Optim andalso
exists (exists is_always_ctr) ctrss then
ctr_infer_type_args T_args
else
T_args
end)
end
fun raw_atp_type_of_typ type_enc =
let
fun term (Type (s, Ts)) =
AType
((if s = \<^type_name>\<open>fun\<close> andalso is_type_enc_higher_order type_enc then
`I tptp_fun_type
else if s = \<^type_name>\<open>bool\<close> andalso
(is_type_enc_full_higher_order type_enc orelse is_type_enc_fool type_enc) then
`I tptp_bool_type
else
`make_fixed_type_const s, []), map term Ts)
| term (TFree (s, _)) = AType ((`make_tfree s, []), [])
| term (TVar z) = AType ((tvar_name z, []), [])
in term end
fun atp_term_of_atp_type (AType ((name, _), tys)) = ATerm ((name, []), map atp_term_of_atp_type tys)
| atp_term_of_atp_type _ = raise Fail "unexpected type"
fun atp_type_of_type_arg type_enc T =
if T = dummyT then NONE else SOME (raw_atp_type_of_typ type_enc T)
(* This shouldn't clash with anything else. *)
val uncurried_alias_sep = "\000"
val mangled_type_sep = "\001"
val ascii_of_uncurried_alias_sep = ascii_of uncurried_alias_sep
fun generic_mangled_type_name f (AType ((name, _), [])) = f name
| generic_mangled_type_name f (AType ((name, _), tys)) =
f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys) ^ ")"
| generic_mangled_type_name _ _ = raise Fail "unexpected type"
fun mangled_type type_enc = generic_mangled_type_name fst o raw_atp_type_of_typ type_enc
fun make_native_type s =
if s = tptp_bool_type orelse s = tptp_fun_type orelse s = tptp_individual_type then s
else native_type_prefix ^ ascii_of s
fun native_atp_type_of_raw_atp_type type_enc pred_sym ary =
let
fun to_mangled_atype ty =
AType (((make_native_type (generic_mangled_type_name fst ty),
generic_mangled_type_name snd ty), []), [])
fun to_poly_atype (AType ((name, clss), tys)) = AType ((name, clss), map to_poly_atype tys)
| to_poly_atype _ = raise Fail "unexpected type"
val to_atype =
if is_type_enc_polymorphic type_enc then to_poly_atype
else to_mangled_atype
fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
fun to_ho (ty as AType (((s, _), _), tys)) =
if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
| to_ho _ = raise Fail "unexpected type"
fun to_lfho (ty as AType (((s, _), _), tys)) =
if s = tptp_fun_type then to_afun to_ho to_lfho tys
else if pred_sym then bool_atype
else to_atype ty
| to_lfho _ = raise Fail "unexpected type"
fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
| to_fo ary (AType (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
| to_fo _ _ = raise Fail "unexpected type"
in
if is_type_enc_full_higher_order type_enc then to_ho
else if is_type_enc_higher_order type_enc then to_lfho
else to_fo ary
end
fun native_atp_type_of_typ type_enc pred_sym ary =
native_atp_type_of_raw_atp_type type_enc pred_sym ary o raw_atp_type_of_typ type_enc
(* Make atoms for sorted type variables. *)
fun generic_add_sorts_on_type _ [] = I
| generic_add_sorts_on_type T (s :: ss) =
generic_add_sorts_on_type T ss
#> (if s = the_single \<^sort>\<open>type\<close> then I else insert (op =) (s, T))
fun add_sorts_on_tfree (T as TFree (_, S)) = generic_add_sorts_on_type T S
| add_sorts_on_tfree _ = I
fun add_sorts_on_tvar (T as TVar (_, S)) = generic_add_sorts_on_type T S
| add_sorts_on_tvar _ = I
fun process_type_args type_enc T_args =
if is_type_enc_native type_enc then
(map (native_atp_type_of_typ type_enc false 0) T_args, [])
else
([], map_filter (Option.map atp_term_of_atp_type o atp_type_of_type_arg type_enc) T_args)
fun class_atom type_enc (cl, T) =
let
val cl = `make_class cl
val (ty_args, tm_args) = process_type_args type_enc [T]
val tm_args =
tm_args @
(case type_enc of
Native (_, _, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
[ATerm ((TYPE_name, ty_args), [])]
| _ => [])
in AAtom (ATerm ((cl, ty_args), tm_args)) end
fun class_atoms type_enc (cls, T) =
map (fn cl => class_atom type_enc (cl, T)) cls
fun class_membs_of_types type_enc add_sorts_on_typ Ts =
[] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
fun mk_aconns c = split_last #> uncurry (fold_rev (mk_aconn c))
fun mk_ahorn [] phi = phi
| mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
fun mk_aquant _ [] phi = phi
| mk_aquant q xs (phi as AQuant (q', xs', phi')) =
if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
| mk_aquant q xs phi = AQuant (q, xs, phi)
fun mk_atyquant _ [] phi = phi
| mk_atyquant q xs (phi as ATyQuant (q', xs', phi')) =
if q = q' then ATyQuant (q, xs @ xs', phi') else ATyQuant (q, xs, phi)
| mk_atyquant q xs phi = ATyQuant (q, xs, phi)
fun close_universally add_term_vars phi =
let
fun add_formula_vars bounds (ATyQuant (_, _, phi)) =
add_formula_vars bounds phi
| add_formula_vars bounds (AQuant (_, xs, phi)) =
add_formula_vars (map fst xs @ bounds) phi
| add_formula_vars bounds (AConn (_, phis)) =
fold (add_formula_vars bounds) phis
| add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm
in mk_aquant AForall (rev (add_formula_vars [] phi [])) phi end
fun add_term_vars bounds (ATerm ((name as (s, _), _), tms)) =
(if is_tptp_variable s andalso
not (String.isPrefix tvar_prefix s) andalso
not (member (op =) bounds name) then
insert (op =) (name, NONE)
else
I)
#> fold (add_term_vars bounds) tms
| add_term_vars bounds (AAbs (((name, _), tm), args)) =
add_term_vars (name :: bounds) tm #> fold (add_term_vars bounds) args
fun close_formula_universally phi = close_universally add_term_vars phi
fun add_iterm_vars bounds (IApp (tm1, tm2)) =
fold (add_iterm_vars bounds) [tm1, tm2]
| add_iterm_vars _ (IConst _) = I
| add_iterm_vars bounds (IVar (name, T)) =
not (member (op =) bounds name) ? insert (op =) (name, SOME T)
| add_iterm_vars bounds (IAbs (_, tm)) = add_iterm_vars bounds tm
fun aliased_uncurried ary (s, s') =
(s ^ ascii_of_uncurried_alias_sep ^ string_of_int ary, s' ^ string_of_int ary)
fun unaliased_uncurried (s, s') =
(case space_explode uncurried_alias_sep s of
[_] => (s, s')
| [s1, s2] => (s1, unsuffix s2 s')
| _ => raise Fail "ill-formed explicit application alias")
fun raw_mangled_const_name type_name ty_args (s, s') =
let
fun type_suffix f g =
fold_rev (prefix o g o prefix mangled_type_sep o type_name f) ty_args ""
in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
fun mangled_const_name type_enc =
map_filter (atp_type_of_type_arg type_enc)
#> raw_mangled_const_name generic_mangled_type_name
val parse_mangled_ident =
Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
fun parse_mangled_type x =
(parse_mangled_ident
-- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
[] >> (ATerm o apfst (rpair []))) x
and parse_mangled_types x =
(parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
fun unmangled_type s =
s |> suffix ")" |> raw_explode
|> Scan.finite Symbol.stopper
(Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
quote s)) parse_mangled_type))
|> fst
fun unmangled_const_name s =
(s, s) |> unaliased_uncurried |> fst |> space_explode mangled_type_sep
fun unmangled_const s =
let val ss = unmangled_const_name s in
(hd ss, map unmangled_type (tl ss))
end
val unmangled_invert_const = invert_const o hd o unmangled_const_name
fun vars_of_iterm vars (IConst ((s, _), _, _)) = insert (op =) s vars
| vars_of_iterm vars (IVar ((s, _), _)) = insert (op =) s vars
| vars_of_iterm vars (IApp (tm1, tm2)) = union (op =) (vars_of_iterm vars tm1) (vars_of_iterm vars tm2)
| vars_of_iterm vars (IAbs (_, tm)) = vars_of_iterm vars tm
fun generate_unique_name gen unique n =
let val x = gen n in
if unique x then x else generate_unique_name gen unique (n + 1)
end
fun eta_expand_quantifier_body (tm as IAbs _) = tm
| eta_expand_quantifier_body tm =
let
(* We accumulate all variables because E 2.5 does not support variable shadowing. *)
val vars = vars_of_iterm [] tm
val x = generate_unique_name
(fn n => "X" ^ (if n = 0 then "" else string_of_int n))
(fn name => not (exists (equal name) vars)) 0
val T = domain_type (ityp_of tm)
in
IAbs ((`I x, T), IApp (tm, IConst (`I x, T, [])))
end
fun introduce_proxies_in_iterm type_enc =
let
fun tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _])) [] =
(* Eta-expand "!!" and "??", to work around LEO-II, Leo-III, and Satallax parser
limitations. This works in conjunction with special code in "ATP_Problem" that uses the
syntactic sugar "!" and "?" whenever possible. *)
IAbs ((`I "P", p_T),
IApp (IConst (`I ho_quant, T, []),
IAbs ((`I "X", x_T),
IApp (IConst (`I "P", p_T, []),
IConst (`I "X", x_T, [])))))
| tweak_ho_quant ho_quant T _ = IConst (`I ho_quant, T, [])
fun tweak_ho_equal T argc =
if argc = 2 then
IConst (`I tptp_equal, T, [])
else
(* Eta-expand partially applied THF equality, because the LEO-II and Satallax parsers
complain about not being able to infer the type of "=". *)
let val i_T = domain_type T in
IAbs ((`I "Y", i_T),
IAbs ((`I "Z", i_T),
IApp (IApp (IConst (`I tptp_equal, T, []),
IConst (`I "Y", i_T, [])),
IConst (`I "Z", i_T, []))))
end
fun intro top_level args (IApp (tm1, tm2)) =
let
val tm1' = intro top_level (tm2 :: args) tm1
val tm2' = intro false [] tm2
val tm2'' =
(case tm1' of
IConst ((s, _), _, _) =>
if s = tptp_ho_forall orelse s = tptp_ho_exists then
eta_expand_quantifier_body tm2'
else
tm2'
| _ => tm2')
in
IApp (tm1', tm2'')
end
| intro top_level args (IConst (name as (s, _), T, T_args)) =
(case proxify_const s of
SOME proxy_base =>
let
val argc = length args
fun plain_const () = IConst (name, T, [])
fun proxy_const () = IConst (proxy_base |>> prefix const_prefix, T, T_args)
fun handle_fool card x = if card = argc then x else proxy_const ()
in
if top_level then
(case s of
"c_False" => IConst (`I tptp_false, T, [])
| "c_True" => IConst (`I tptp_true, T, [])
| _ => plain_const ())
else if is_type_enc_full_higher_order type_enc then
(case s of
"c_False" => IConst (`I tptp_false, T, [])
| "c_True" => IConst (`I tptp_true, T, [])
| "c_Not" => IConst (`I tptp_not, T, [])
| "c_conj" => IConst (`I tptp_and, T, [])
| "c_disj" => IConst (`I tptp_or, T, [])
| "c_implies" => IConst (`I tptp_implies, T, [])
| "c_All" => tweak_ho_quant tptp_ho_forall T args
| "c_Ex" => tweak_ho_quant tptp_ho_exists T args
| s =>
if is_tptp_equal s then
tweak_ho_equal T argc
else
plain_const ())
else if is_type_enc_fool type_enc then
(case s of
"c_False" => IConst (`I tptp_false, T, [])
| "c_True" => IConst (`I tptp_true, T, [])
| "c_Not" => handle_fool 1 (IConst (`I tptp_not, T, []))
| "c_conj" => handle_fool 2 (IConst (`I tptp_and, T, []))
| "c_disj" => handle_fool 2 (IConst (`I tptp_or, T, []))
| "c_implies" => handle_fool 2 (IConst (`I tptp_implies, T, []))
| "c_All" => handle_fool 1 (tweak_ho_quant tptp_ho_forall T args)
| "c_Ex" => handle_fool 1 (tweak_ho_quant tptp_ho_exists T args)
| s =>
if is_tptp_equal s then
handle_fool 2 (IConst (`I tptp_equal, T, []))
else
plain_const ())
else
proxy_const ()
end
| NONE =>
if s = tptp_choice then
tweak_ho_quant tptp_choice T args
else
IConst (name, T, T_args))
| intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm)
| intro _ _ tm = tm
in intro true [] end
fun mangle_type_args_in_const type_enc (name as (s, _)) T_args =
if String.isPrefix const_prefix s andalso is_type_enc_mangling type_enc then
(mangled_const_name type_enc T_args name, [])
else
(name, T_args)
fun mangle_type_args_in_iterm type_enc =
if is_type_enc_mangling type_enc then
let
fun mangle (IApp (tm1, tm2)) = IApp (mangle tm1, mangle tm2)
| mangle (tm as IConst (_, _, [])) = tm
| mangle (IConst (name, T, T_args)) =
mangle_type_args_in_const type_enc name T_args
|> (fn (name, T_args) => IConst (name, T, T_args))
| mangle (IAbs (bound, tm)) = IAbs (bound, mangle tm)
| mangle tm = tm
in mangle end
else
I
fun filter_type_args_in_const _ _ _ _ _ [] = []
| filter_type_args_in_const thy ctrss type_enc ary s T_args =
(case unprefix_and_unascii const_prefix s of
NONE => if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then [] else T_args
| SOME s'' => filter_type_args thy ctrss type_enc (unmangled_invert_const s'') ary T_args)
fun filter_type_args_in_iterm thy ctrss type_enc =
let
fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2)
| filt ary (IConst (name as (s, _), T, T_args)) =
filter_type_args_in_const thy ctrss type_enc ary s T_args
|> (fn T_args => IConst (name, T, T_args))
| filt _ (IAbs (bound, tm)) = IAbs (bound, filt 0 tm)
| filt _ tm = tm
in filt 0 end
fun iformula_of_prop ctxt type_enc iff_for_eq =
let
val thy = Proof_Context.theory_of ctxt
fun do_term bs t atomic_Ts =
iterm_of_term thy type_enc bs (Envir.eta_contract t)
|>> (introduce_proxies_in_iterm type_enc
#> mangle_type_args_in_iterm type_enc #> AAtom)
||> union (op =) atomic_Ts
fun do_quant bs q pos s T t' =
let
val s = singleton (Name.variant_list (map fst bs)) s
val universal = Option.map (q = AExists ? not) pos
val name =
s |> `(case universal of
SOME true => make_all_bound_var
| SOME false => make_exist_bound_var
| NONE => make_bound_var)
in
do_formula ((s, (name, T)) :: bs) pos t'
#>> mk_aquant q [(name, SOME T)]
##> union (op =) (atomic_types_of T)
end
and do_conn bs c pos1 t1 pos2 t2 =
do_formula bs pos1 t1 ##>> do_formula bs pos2 t2 #>> uncurry (mk_aconn c)
and do_formula bs pos t =
(case t of
\<^const>\<open>Trueprop\<close> $ t1 => do_formula bs pos t1
| \<^const>\<open>Not\<close> $ t1 => do_formula bs (Option.map not pos) t1 #>> mk_anot
| Const (\<^const_name>\<open>All\<close>, _) $ Abs (s, T, t') => do_quant bs AForall pos s T t'
| (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ t1 =>
do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1)
| Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (s, T, t') => do_quant bs AExists pos s T t'
| (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ t1 =>
do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1)
| \<^const>\<open>HOL.conj\<close> $ t1 $ t2 => do_conn bs AAnd pos t1 pos t2
| \<^const>\<open>HOL.disj\<close> $ t1 $ t2 => do_conn bs AOr pos t1 pos t2
| \<^const>\<open>HOL.implies\<close> $ t1 $ t2 => do_conn bs AImplies (Option.map not pos) t1 pos t2
| Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [\<^typ>\<open>bool\<close>, _])) $ t1 $ t2 =>
if iff_for_eq then do_conn bs AIff NONE t1 NONE t2 else do_term bs t
| _ => do_term bs t)
in do_formula [] end
fun presimplify_term ctxt t =
if exists_Const (member (op =) Meson.presimplified_consts o fst) t then
t |> Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
|> Meson.presimplify ctxt
|> Thm.prop_of
else
t
fun preprocess_abstractions_in_terms trans_lams facts =
let
val (facts, lambda_ts) =
facts |> map (snd o snd) |> trans_lams
|>> map2 (fn (name, (role, _)) => fn t => (name, (role, t))) facts
val lam_facts =
map2 (fn t => fn j =>
((lam_fact_prefix ^ Int.toString j,
(Global, Non_Rec_Def)), (Axiom, t)))
lambda_ts (1 upto length lambda_ts)
in (facts, lam_facts) end
(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate this in Sledgehammer to
prevent the discovery of unreplayable proofs. *)
fun freeze_term t =
let
(* Freshness is desirable for completeness, but not for soundness. *)
fun indexed_name (s, i) = s ^ "_" ^ string_of_int i ^ atp_weak_suffix
fun freeze (t $ u) = freeze t $ freeze u
| freeze (Abs (s, T, t)) = Abs (s, T, freeze t)
| freeze (Var (x, T)) = Free (indexed_name x, T)
| freeze t = t
fun freeze_tvar (x, S) = TFree (indexed_name x, S)
in
t |> exists_subterm is_Var t ? freeze
|> exists_type (exists_subtype is_TVar) t
? map_types (map_type_tvar freeze_tvar)
end
fun presimp_prop ctxt type_enc t =
let
val t = t |> Envir.beta_eta_contract
|> transform_elim_prop
|> Object_Logic.atomize_term ctxt
val need_trueprop = (fastype_of t = \<^typ>\<open>bool\<close>)
val is_ho = is_type_enc_full_higher_order type_enc
in
t |> need_trueprop ? HOLogic.mk_Trueprop
|> (if is_ho then unextensionalize_def
else cong_extensionalize_term ctxt #> abs_extensionalize_term ctxt)
|> presimplify_term ctxt
|> HOLogic.dest_Trueprop
end
handle TERM _ => \<^const>\<open>True\<close>
(* Satallax prefers "=" to "<=>" (for definitions) and Metis (CNF) requires "=" for technical
reasons. *)
fun should_use_iff_for_eq CNF _ = false
| should_use_iff_for_eq (THF _) format = not (is_type_enc_full_higher_order format)
| should_use_iff_for_eq _ _ = true
fun make_formula ctxt format type_enc iff_for_eq name stature role t =
let
val iff_for_eq = iff_for_eq andalso should_use_iff_for_eq format type_enc
val (iformula, atomic_Ts) =
iformula_of_prop ctxt type_enc iff_for_eq (SOME (role <> Conjecture)) t []
|>> close_universally add_iterm_vars
in
{name = name, stature = stature, role = role, iformula = iformula, atomic_types = atomic_Ts}
end
fun make_fact ctxt format type_enc iff_for_eq ((name, stature), t) =
(case make_formula ctxt format type_enc iff_for_eq name stature Axiom t of
formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
if s = tptp_true then NONE else SOME formula
| formula => SOME formula)
fun make_conjecture ctxt format type_enc =
map (fn ((name, stature), (role, t)) =>
let val t' = t |> role = Conjecture ? s_not in
make_formula ctxt format type_enc true name stature role t'
end)
(** Finite and infinite type inference **)
fun tvar_footprint thy s ary =
(case unprefix_and_unascii const_prefix s of
SOME s =>
let fun tvars_of T = [] |> Term.add_tvarsT T |> map fst in
s |> unmangled_invert_const |> robust_const_type thy |> chop_fun ary |> fst |> map tvars_of
end
| NONE => [])
handle TYPE _ => []
fun type_arg_cover thy pos s ary =
if is_tptp_equal s then
if pos = SOME false then [] else 0 upto ary - 1
else
let
val footprint = tvar_footprint thy s ary
val eq = (s = \<^const_name>\<open>HOL.eq\<close>)
fun cover _ [] = []
| cover seen ((i, tvars) :: args) =
cover (union (op =) seen tvars) args
|> (eq orelse exists (fn tvar => not (member (op =) seen tvar)) tvars)
? cons i
in
if forall null footprint then
[]
else
0 upto length footprint - 1 ~~ footprint
|> sort (rev_order o list_ord Term_Ord.indexname_ord o apply2 snd)
|> cover []
end
type monotonicity_info =
{maybe_finite_Ts : typ list,
surely_infinite_Ts : typ list,
maybe_nonmono_Ts : typ list}
(* These types witness that the type classes they belong to allow infinite
models and hence that any types with these type classes is monotonic. *)
val known_infinite_types = [\<^typ>\<open>nat\<close>, HOLogic.intT, HOLogic.realT, \<^typ>\<open>nat => bool\<close>]
fun is_type_kind_of_surely_infinite ctxt strictness cached_Ts T =
strictness <> Strict andalso is_type_surely_infinite ctxt true cached_Ts T
(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
dangerous because their "exhaust" properties can easily lead to unsound ATP
proofs. On the other hand, all HOL infinite types can be given the same
models in first-order logic (via Loewenheim-Skolem). *)
fun should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts, maybe_nonmono_Ts}
(Nonmono_Types (strictness, _)) T =
let val thy = Proof_Context.theory_of ctxt in
(exists (type_intersect thy T) maybe_nonmono_Ts andalso
not (exists (type_instance thy T) surely_infinite_Ts orelse
(not (member (type_equiv thy) maybe_finite_Ts T) andalso
is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts T)))
end
| should_encode_type _ _ level _ = (level = All_Types orelse level = Undercover_Types)
fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T =
should_guard_var () andalso should_encode_type ctxt mono level T
| should_guard_type _ _ _ _ _ = false
fun is_maybe_universal_name s =
String.isPrefix bound_var_prefix s orelse
String.isPrefix all_bound_var_prefix s
fun is_maybe_universal_var (IConst ((s, _), _, _)) = is_maybe_universal_name s
| is_maybe_universal_var (IVar _) = true
| is_maybe_universal_var _ = false
datatype site =
Top_Level of bool option |
Eq_Arg of bool option |
Arg of string * int * int |
Elsewhere
fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
| should_tag_with_type ctxt mono (Tags (_, level)) site u T =
let val thy = Proof_Context.theory_of ctxt in
(case level of
Nonmono_Types (_, Non_Uniform) =>
(case (site, is_maybe_universal_var u) of
(Eq_Arg pos, true) =>
(pos <> SOME false orelse tag_neg_vars) andalso should_encode_type ctxt mono level T
| _ => false)
| Undercover_Types =>
(case (site, is_maybe_universal_var u) of
(Eq_Arg pos, true) => pos <> SOME false
| (Arg (s, j, ary), true) => member (op =) (type_arg_cover thy NONE s ary) j
| _ => false)
| _ => should_encode_type ctxt mono level T)
end
| should_tag_with_type _ _ _ _ _ _ = false
(** predicators and application operators **)
type sym_info = {pred_sym : bool, min_ary : int, max_ary : int, types : typ list, in_conj : bool}
fun default_sym_tab_entries type_enc =
let
fun mk_sym_info pred n =
{pred_sym = pred, min_ary = n, max_ary = n, types = [], in_conj = false}
in
(make_fixed_const NONE \<^const_name>\<open>undefined\<close>, mk_sym_info false 0) ::
(map (rpair (mk_sym_info true 0)) [tptp_false, tptp_true]) @
(map (rpair (mk_sym_info true 1)) tptp_unary_builtins) @
(map (rpair (mk_sym_info true 2)) (tptp_old_equal :: tptp_binary_builtins))
|> not (is_type_enc_fool type_enc orelse is_type_enc_full_higher_order type_enc)
? cons (prefixed_predicator_name, mk_sym_info true 1)
end
datatype app_op_level =
Min_App_Op |
Sufficient_App_Op |
Sufficient_App_Op_And_Predicator |
Full_App_Op_And_Predicator
fun add_iterm_syms_to_sym_table ctxt app_op_level conj_fact =
let
val thy = Proof_Context.theory_of ctxt
fun consider_var_ary const_T var_T max_ary =
let
fun iter ary T =
if ary = max_ary orelse type_instance thy var_T T orelse type_instance thy T var_T then
ary
else
iter (ary + 1) (range_type T)
in iter 0 const_T end
fun add_universal_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
if (app_op_level = Sufficient_App_Op andalso can dest_funT T) orelse
(app_op_level = Sufficient_App_Op_And_Predicator andalso
(can dest_funT T orelse T = \<^typ>\<open>bool\<close>)) then
let
val bool_vars' =
bool_vars orelse
(app_op_level = Sufficient_App_Op_And_Predicator andalso body_type T = \<^typ>\<open>bool\<close>)
fun repair_min_ary {pred_sym, min_ary, max_ary, types, in_conj} =
{pred_sym = pred_sym andalso not bool_vars',
min_ary = fold (fn T' => consider_var_ary T' T) types min_ary,
max_ary = max_ary, types = types, in_conj = in_conj}
val fun_var_Ts' = fun_var_Ts |> can dest_funT T ? insert_type thy I T
in
if bool_vars' = bool_vars andalso fun_var_Ts' = fun_var_Ts then accum
else ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_ary) sym_tab)
end
else
accum
fun add_iterm_syms top_level tm (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
let val (head, args) = strip_iterm_comb tm in
(case head of
IConst ((s, _), T, _) =>
if is_maybe_universal_name s then
add_universal_var T accum
else if String.isPrefix exist_bound_var_prefix s then
accum
else
let val ary = length args in
((bool_vars, fun_var_Ts),
(case Symtab.lookup sym_tab s of
SOME {pred_sym, min_ary, max_ary, types, in_conj} =>
let
val pred_sym = pred_sym andalso top_level andalso not bool_vars
val types' = types |> insert_type thy I T
val in_conj = in_conj orelse conj_fact
val min_ary =
if (app_op_level = Sufficient_App_Op orelse
app_op_level = Sufficient_App_Op_And_Predicator)
andalso types' <> types then
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.90 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
