wenzelm@44163: (* Title: HOL/Tools/ATP/atp_translate.ML blanchet@38506: Author: Fabian Immler, TU Muenchen blanchet@38506: Author: Makarius blanchet@38506: Author: Jasmin Blanchette, TU Muenchen blanchet@38506: blanchet@39734: Translation of HOL to FOL for Sledgehammer. blanchet@38506: *) blanchet@38506: blanchet@43926: signature ATP_TRANSLATE = blanchet@38506: sig nik@44535: type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term blanchet@43977: type connective = ATP_Problem.connective blanchet@43977: type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula blanchet@43780: type format = ATP_Problem.format blanchet@43580: type formula_kind = ATP_Problem.formula_kind blanchet@38506: type 'a problem = 'a ATP_Problem.problem blanchet@43926: blanchet@44282: datatype locality = blanchet@44282: General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum | blanchet@44282: Chained blanchet@43484: blanchet@44491: datatype order = First_Order | Higher_Order blanchet@43484: datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic blanchet@43484: datatype type_level = blanchet@44233: All_Types | Noninf_Nonmono_Types | Fin_Nonmono_Types | Const_Arg_Types | blanchet@44233: No_Types blanchet@43969: datatype type_heaviness = Heavyweight | Lightweight blanchet@43484: blanchet@44493: datatype type_enc = blanchet@44491: Simple_Types of order * type_level | blanchet@43708: Preds of polymorphism * type_level * type_heaviness | blanchet@43708: Tags of polymorphism * type_level * type_heaviness blanchet@43484: blanchet@43926: val bound_var_prefix : string blanchet@44367: val schematic_var_prefix : string blanchet@44367: val fixed_var_prefix : string blanchet@44367: val tvar_prefix : string blanchet@44367: val tfree_prefix : string blanchet@44367: val const_prefix : string blanchet@44367: val type_const_prefix : string blanchet@44367: val class_prefix : string blanchet@43926: val skolem_const_prefix : string blanchet@43926: val old_skolem_const_prefix : string blanchet@43926: val new_skolem_const_prefix : string blanchet@43966: val type_decl_prefix : string blanchet@43966: val sym_decl_prefix : string blanchet@43966: val preds_sym_formula_prefix : string blanchet@43970: val lightweight_tags_sym_formula_prefix : string blanchet@40445: val fact_prefix : string blanchet@38506: val conjecture_prefix : string blanchet@43750: val helper_prefix : string blanchet@43966: val class_rel_clause_prefix : string blanchet@43966: val arity_clause_prefix : string blanchet@43966: val tfree_clause_prefix : string blanchet@43750: val typed_helper_suffix : string blanchet@43966: val untyped_helper_suffix : string blanchet@44000: val type_tag_idempotence_helper_name : string blanchet@43807: val predicator_name : string blanchet@43807: val app_op_name : string blanchet@43945: val type_tag_name : string blanchet@43807: val type_pred_name : string blanchet@43803: val simple_type_prefix : string blanchet@44015: val prefixed_predicator_name : string blanchet@43971: val prefixed_app_op_name : string blanchet@43971: val prefixed_type_tag_name : string blanchet@44367: val ascii_of : string -> string blanchet@44367: val unascii_of : string -> string blanchet@43926: val strip_prefix_and_unascii : string -> string -> string option blanchet@44000: val proxy_table : (string * (string * (thm * (string * string)))) list blanchet@44000: val proxify_const : string -> (string * string) option blanchet@44367: val invert_const : string -> string blanchet@44367: val unproxify_const : string -> string blanchet@43934: val new_skolem_var_name_from_const : string -> string blanchet@43934: val num_type_args : theory -> string -> int blanchet@44089: val atp_irrelevant_consts : string list blanchet@44089: val atp_schematic_consts_of : term -> typ list Symtab.table blanchet@43926: val is_locality_global : locality -> bool blanchet@44493: val type_enc_from_string : string -> type_enc blanchet@44493: val polymorphism_of_type_enc : type_enc -> polymorphism blanchet@44493: val level_of_type_enc : type_enc -> type_level blanchet@44493: val is_type_enc_virtually_sound : type_enc -> bool blanchet@44493: val is_type_enc_fairly_sound : type_enc -> bool blanchet@44493: val choose_format : format list -> type_enc -> format * type_enc blanchet@43977: val mk_aconns : blanchet@43977: connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula nik@44535: val unmangled_const : string -> string * (string, 'b) ho_term list blanchet@43971: val unmangled_const_name : string -> string blanchet@44035: val helper_table : ((string * bool) * thm list) list blanchet@44372: val factsN : string blanchet@40240: val prepare_atp_problem : blanchet@44493: Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool blanchet@44175: -> bool -> bool -> bool -> term list -> term blanchet@44175: -> ((string * locality) * term) list blanchet@43412: -> string problem * string Symtab.table * int * int blanchet@44055: * (string * locality) list vector * int list * int Symtab.table blanchet@41561: val atp_problem_weights : string problem -> (string * real) list blanchet@38506: end; blanchet@38506: blanchet@43926: structure ATP_Translate : ATP_TRANSLATE = blanchet@38506: struct blanchet@38506: blanchet@43926: open ATP_Util blanchet@38506: open ATP_Problem blanchet@43926: blanchet@43926: type name = string * string blanchet@43926: blanchet@43511: (* experimental *) blanchet@43511: val generate_useful_info = false blanchet@38506: blanchet@43748: fun useful_isabelle_info s = blanchet@43748: if generate_useful_info then blanchet@43748: SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])])) blanchet@43748: else blanchet@43748: NONE blanchet@43748: blanchet@43748: val intro_info = useful_isabelle_info "intro" blanchet@43748: val elim_info = useful_isabelle_info "elim" blanchet@43748: val simp_info = useful_isabelle_info "simp" blanchet@43748: blanchet@43926: val bound_var_prefix = "B_" blanchet@43926: val schematic_var_prefix = "V_" blanchet@43926: val fixed_var_prefix = "v_" blanchet@43926: blanchet@43926: val tvar_prefix = "T_" blanchet@43926: val tfree_prefix = "t_" blanchet@43926: blanchet@43926: val const_prefix = "c_" blanchet@43926: val type_const_prefix = "tc_" blanchet@43926: val class_prefix = "cl_" blanchet@43926: blanchet@43926: val skolem_const_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko" blanchet@43926: val old_skolem_const_prefix = skolem_const_prefix ^ "o" blanchet@43926: val new_skolem_const_prefix = skolem_const_prefix ^ "n" blanchet@43926: blanchet@43839: val type_decl_prefix = "ty_" blanchet@43839: val sym_decl_prefix = "sy_" blanchet@43966: val preds_sym_formula_prefix = "psy_" blanchet@43970: val lightweight_tags_sym_formula_prefix = "tsy_" blanchet@40445: val fact_prefix = "fact_" blanchet@38506: val conjecture_prefix = "conj_" blanchet@38506: val helper_prefix = "help_" blanchet@44000: val class_rel_clause_prefix = "clar_" blanchet@38506: val arity_clause_prefix = "arity_" blanchet@43926: val tfree_clause_prefix = "tfree_" blanchet@38506: blanchet@43750: val typed_helper_suffix = "_T" blanchet@43750: val untyped_helper_suffix = "_U" blanchet@44000: val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem" blanchet@43750: blanchet@43807: val predicator_name = "hBOOL" blanchet@43807: val app_op_name = "hAPP" blanchet@43945: val type_tag_name = "ti" blanchet@43807: val type_pred_name = "is" blanchet@43803: val simple_type_prefix = "ty_" blanchet@43402: blanchet@44015: val prefixed_predicator_name = const_prefix ^ predicator_name blanchet@43971: val prefixed_app_op_name = const_prefix ^ app_op_name blanchet@43971: val prefixed_type_tag_name = const_prefix ^ type_tag_name blanchet@43971: blanchet@38506: (* Freshness almost guaranteed! *) blanchet@38506: val sledgehammer_weak_prefix = "Sledgehammer:" blanchet@38506: blanchet@43926: (*Escaping of special characters. blanchet@43926: Alphanumeric characters are left unchanged. blanchet@43926: The character _ goes to __ blanchet@43926: Characters in the range ASCII space to / go to _A to _P, respectively. blanchet@43926: Other characters go to _nnn where nnn is the decimal ASCII code.*) blanchet@43934: val upper_a_minus_space = Char.ord #"A" - Char.ord #" " blanchet@43926: blanchet@43926: fun stringN_of_int 0 _ = "" blanchet@43926: | stringN_of_int k n = blanchet@43926: stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10) blanchet@43926: blanchet@43926: fun ascii_of_char c = blanchet@43926: if Char.isAlphaNum c then blanchet@43926: String.str c blanchet@43926: else if c = #"_" then blanchet@43926: "__" blanchet@43926: else if #" " <= c andalso c <= #"/" then blanchet@43926: "_" ^ String.str (Char.chr (Char.ord c + upper_a_minus_space)) blanchet@43926: else blanchet@43926: (* fixed width, in case more digits follow *) blanchet@43926: "_" ^ stringN_of_int 3 (Char.ord c) blanchet@43926: blanchet@43926: val ascii_of = String.translate ascii_of_char blanchet@43926: blanchet@43926: (** Remove ASCII armoring from names in proof files **) blanchet@43926: blanchet@43926: (* We don't raise error exceptions because this code can run inside a worker blanchet@43926: thread. Also, the errors are impossible. *) blanchet@43926: val unascii_of = blanchet@43926: let blanchet@43926: fun un rcs [] = String.implode(rev rcs) blanchet@43926: | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *) blanchet@43926: (* Three types of _ escapes: __, _A to _P, _nnn *) blanchet@44367: | un rcs (#"_" :: #"_" :: cs) = un (#"_" :: rcs) cs blanchet@43926: | un rcs (#"_" :: c :: cs) = blanchet@43926: if #"A" <= c andalso c<= #"P" then blanchet@43926: (* translation of #" " to #"/" *) blanchet@43926: un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs blanchet@43926: else blanchet@44367: let val digits = List.take (c :: cs, 3) handle General.Subscript => [] in blanchet@43926: case Int.fromString (String.implode digits) of blanchet@43926: SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2)) blanchet@44367: | NONE => un (c :: #"_" :: rcs) cs (* ERROR *) blanchet@43926: end blanchet@43926: | un rcs (c :: cs) = un (c :: rcs) cs blanchet@43926: in un [] o String.explode end blanchet@43926: blanchet@43926: (* If string s has the prefix s1, return the result of deleting it, blanchet@43926: un-ASCII'd. *) blanchet@43926: fun strip_prefix_and_unascii s1 s = blanchet@43926: if String.isPrefix s1 s then blanchet@43926: SOME (unascii_of (String.extract (s, size s1, NONE))) blanchet@43926: else blanchet@43926: NONE blanchet@43926: blanchet@44000: val proxy_table = blanchet@44000: [("c_False", (@{const_name False}, (@{thm fFalse_def}, blanchet@44000: ("fFalse", @{const_name ATP.fFalse})))), blanchet@44000: ("c_True", (@{const_name True}, (@{thm fTrue_def}, blanchet@44000: ("fTrue", @{const_name ATP.fTrue})))), blanchet@44000: ("c_Not", (@{const_name Not}, (@{thm fNot_def}, blanchet@44000: ("fNot", @{const_name ATP.fNot})))), blanchet@44000: ("c_conj", (@{const_name conj}, (@{thm fconj_def}, blanchet@44000: ("fconj", @{const_name ATP.fconj})))), blanchet@44000: ("c_disj", (@{const_name disj}, (@{thm fdisj_def}, blanchet@44000: ("fdisj", @{const_name ATP.fdisj})))), blanchet@44000: ("c_implies", (@{const_name implies}, (@{thm fimplies_def}, blanchet@44000: ("fimplies", @{const_name ATP.fimplies})))), blanchet@44000: ("equal", (@{const_name HOL.eq}, (@{thm fequal_def}, nik@44537: ("fequal", @{const_name ATP.fequal})))), nik@44537: ("c_All", (@{const_name All}, (@{thm fAll_def}, nik@44537: ("fAll", @{const_name ATP.fAll})))), nik@44537: ("c_Ex", (@{const_name Ex}, (@{thm fEx_def}, nik@44537: ("fEx", @{const_name ATP.fEx}))))] blanchet@43926: blanchet@44000: val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd) blanchet@43926: blanchet@43926: (* Readable names for the more common symbolic functions. Do not mess with the blanchet@43926: table unless you know what you are doing. *) blanchet@43926: val const_trans_table = blanchet@43926: [(@{type_name Product_Type.prod}, "prod"), blanchet@43926: (@{type_name Sum_Type.sum}, "sum"), blanchet@43926: (@{const_name False}, "False"), blanchet@43926: (@{const_name True}, "True"), blanchet@43926: (@{const_name Not}, "Not"), blanchet@43926: (@{const_name conj}, "conj"), blanchet@43926: (@{const_name disj}, "disj"), blanchet@43926: (@{const_name implies}, "implies"), blanchet@43926: (@{const_name HOL.eq}, "equal"), nik@44537: (@{const_name All}, "All"), nik@44537: (@{const_name Ex}, "Ex"), blanchet@43926: (@{const_name If}, "If"), blanchet@43926: (@{const_name Set.member}, "member"), blanchet@43926: (@{const_name Meson.COMBI}, "COMBI"), blanchet@43926: (@{const_name Meson.COMBK}, "COMBK"), blanchet@43926: (@{const_name Meson.COMBB}, "COMBB"), blanchet@43926: (@{const_name Meson.COMBC}, "COMBC"), blanchet@43926: (@{const_name Meson.COMBS}, "COMBS")] blanchet@43926: |> Symtab.make blanchet@44000: |> fold (Symtab.update o swap o snd o snd o snd) proxy_table blanchet@43926: blanchet@43926: (* Invert the table of translations between Isabelle and ATPs. *) blanchet@43926: val const_trans_table_inv = blanchet@43926: const_trans_table |> Symtab.dest |> map swap |> Symtab.make blanchet@43926: val const_trans_table_unprox = blanchet@43926: Symtab.empty blanchet@44000: |> fold (fn (_, (isa, (_, (_, atp)))) => Symtab.update (atp, isa)) proxy_table blanchet@43926: blanchet@43926: val invert_const = perhaps (Symtab.lookup const_trans_table_inv) blanchet@43926: val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox) blanchet@43926: blanchet@43926: fun lookup_const c = blanchet@43926: case Symtab.lookup const_trans_table c of blanchet@43926: SOME c' => c' blanchet@43926: | NONE => ascii_of c blanchet@43926: blanchet@44489: fun ascii_of_indexname (v, 0) = ascii_of v blanchet@44489: | ascii_of_indexname (v, i) = ascii_of v ^ "_" ^ string_of_int i blanchet@43926: blanchet@43926: fun make_bound_var x = bound_var_prefix ^ ascii_of x blanchet@43926: fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v blanchet@43926: fun make_fixed_var x = fixed_var_prefix ^ ascii_of x blanchet@43926: blanchet@44489: fun make_schematic_type_var (x, i) = blanchet@44489: tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i)) blanchet@44489: fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x)) blanchet@43926: blanchet@44489: (* "HOL.eq" is mapped to the ATP's equality. *) blanchet@44489: fun make_fixed_const @{const_name HOL.eq} = tptp_old_equal blanchet@43926: | make_fixed_const c = const_prefix ^ lookup_const c blanchet@43926: blanchet@43926: fun make_fixed_type_const c = type_const_prefix ^ lookup_const c blanchet@43926: blanchet@43926: fun make_type_class clas = class_prefix ^ ascii_of clas blanchet@43926: blanchet@43934: fun new_skolem_var_name_from_const s = blanchet@43934: let val ss = s |> space_explode Long_Name.separator in blanchet@43934: nth ss (length ss - 2) blanchet@43934: end blanchet@43934: blanchet@43934: (* The number of type arguments of a constant, zero if it's monomorphic. For blanchet@43934: (instances of) Skolem pseudoconstants, this information is encoded in the blanchet@43934: constant name. *) blanchet@43934: fun num_type_args thy s = blanchet@43934: if String.isPrefix skolem_const_prefix s then blanchet@43934: s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the blanchet@43934: else blanchet@43934: (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length blanchet@43934: blanchet@44089: (* These are either simplified away by "Meson.presimplify" (most of the time) or blanchet@44089: handled specially via "fFalse", "fTrue", ..., "fequal". *) blanchet@44089: val atp_irrelevant_consts = blanchet@44089: [@{const_name False}, @{const_name True}, @{const_name Not}, blanchet@44089: @{const_name conj}, @{const_name disj}, @{const_name implies}, blanchet@44089: @{const_name HOL.eq}, @{const_name If}, @{const_name Let}] blanchet@44089: blanchet@44089: val atp_monomorph_bad_consts = blanchet@44089: atp_irrelevant_consts @ blanchet@44089: (* These are ignored anyway by the relevance filter (unless they appear in blanchet@44089: higher-order places) but not by the monomorphizer. *) blanchet@44089: [@{const_name all}, @{const_name "==>"}, @{const_name "=="}, blanchet@44089: @{const_name Trueprop}, @{const_name All}, @{const_name Ex}, blanchet@44089: @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}] blanchet@44089: blanchet@44099: fun add_schematic_const (x as (_, T)) = blanchet@44099: Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x blanchet@44099: val add_schematic_consts_of = blanchet@44099: Term.fold_aterms (fn Const (x as (s, _)) => blanchet@44099: not (member (op =) atp_monomorph_bad_consts s) blanchet@44099: ? add_schematic_const x blanchet@44099: | _ => I) blanchet@44099: fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty blanchet@44089: blanchet@43926: (** Definitions and functions for FOL clauses and formulas for TPTP **) blanchet@43926: blanchet@43926: (* The first component is the type class; the second is a "TVar" or "TFree". *) blanchet@43926: datatype type_literal = blanchet@43926: TyLitVar of name * name | blanchet@43926: TyLitFree of name * name blanchet@43926: blanchet@43926: blanchet@43926: (** Isabelle arities **) blanchet@43926: blanchet@43926: datatype arity_literal = blanchet@43926: TConsLit of name * name * name list | blanchet@43926: TVarLit of name * name blanchet@43926: blanchet@43926: fun gen_TVars 0 = [] blanchet@43934: | gen_TVars n = ("T_" ^ string_of_int n) :: gen_TVars (n-1) blanchet@43926: blanchet@44104: val type_class = the_single @{sort type} blanchet@44104: blanchet@44104: fun add_packed_sort tvar = blanchet@44104: fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar)) blanchet@43926: blanchet@43927: type arity_clause = blanchet@44367: {name : string, blanchet@44367: prem_lits : arity_literal list, blanchet@44367: concl_lits : arity_literal} blanchet@43926: blanchet@43926: (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *) blanchet@43926: fun make_axiom_arity_clause (tcons, name, (cls, args)) = blanchet@43926: let blanchet@43926: val tvars = gen_TVars (length args) blanchet@43926: val tvars_srts = ListPair.zip (tvars, args) blanchet@43926: in blanchet@43927: {name = name, blanchet@44104: prem_lits = [] |> fold (uncurry add_packed_sort) tvars_srts |> map TVarLit, blanchet@43927: concl_lits = TConsLit (`make_type_class cls, blanchet@43927: `make_fixed_type_const tcons, blanchet@43927: tvars ~~ tvars)} blanchet@43926: end blanchet@43926: blanchet@43926: fun arity_clause _ _ (_, []) = [] blanchet@44366: | arity_clause seen n (tcons, ("HOL.type", _) :: ars) = (* ignore *) blanchet@44366: arity_clause seen n (tcons, ars) blanchet@44366: | arity_clause seen n (tcons, (ar as (class, _)) :: ars) = blanchet@44366: if member (op =) seen class then blanchet@44366: (* multiple arities for the same (tycon, class) pair *) blanchet@44366: make_axiom_arity_clause (tcons, blanchet@44366: lookup_const tcons ^ "___" ^ ascii_of class ^ "_" ^ string_of_int n, blanchet@44366: ar) :: blanchet@44366: arity_clause seen (n + 1) (tcons, ars) blanchet@44366: else blanchet@44366: make_axiom_arity_clause (tcons, lookup_const tcons ^ "___" ^ blanchet@44366: ascii_of class, ar) :: blanchet@44366: arity_clause (class :: seen) n (tcons, ars) blanchet@43926: blanchet@43926: fun multi_arity_clause [] = [] blanchet@43926: | multi_arity_clause ((tcons, ars) :: tc_arlists) = blanchet@43926: arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists blanchet@43926: blanchet@44489: (* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in blanchet@44489: theory thy provided its arguments have the corresponding sorts. *) blanchet@43926: fun type_class_pairs thy tycons classes = blanchet@43934: let blanchet@43934: val alg = Sign.classes_of thy blanchet@43934: fun domain_sorts tycon = Sorts.mg_domain alg tycon o single blanchet@43934: fun add_class tycon class = blanchet@43934: cons (class, domain_sorts tycon class) blanchet@43934: handle Sorts.CLASS_ERROR _ => I blanchet@43934: fun try_classes tycon = (tycon, fold (add_class tycon) classes []) blanchet@43934: in map try_classes tycons end blanchet@43926: blanchet@43926: (*Proving one (tycon, class) membership may require proving others, so iterate.*) blanchet@43926: fun iter_type_class_pairs _ _ [] = ([], []) blanchet@43926: | iter_type_class_pairs thy tycons classes = blanchet@44104: let blanchet@44104: fun maybe_insert_class s = blanchet@44104: (s <> type_class andalso not (member (op =) classes s)) blanchet@44104: ? insert (op =) s blanchet@44104: val cpairs = type_class_pairs thy tycons classes blanchet@44104: val newclasses = blanchet@44104: [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) cpairs blanchet@44104: val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses blanchet@44107: in (classes' @ classes, union (op =) cpairs' cpairs) end blanchet@43926: blanchet@43926: fun make_arity_clauses thy tycons = blanchet@43926: iter_type_class_pairs thy tycons ##> multi_arity_clause blanchet@43926: blanchet@43926: blanchet@43926: (** Isabelle class relations **) blanchet@43926: blanchet@43927: type class_rel_clause = blanchet@44367: {name : string, blanchet@44367: subclass : name, blanchet@44367: superclass : name} blanchet@43926: blanchet@44489: (* Generate all pairs (sub, super) such that sub is a proper subclass of super blanchet@44489: in theory "thy". *) blanchet@43926: fun class_pairs _ [] _ = [] blanchet@43926: | class_pairs thy subs supers = blanchet@43926: let blanchet@43926: val class_less = Sorts.class_less (Sign.classes_of thy) blanchet@43926: fun add_super sub super = class_less (sub, super) ? cons (sub, super) blanchet@43926: fun add_supers sub = fold (add_super sub) supers blanchet@43926: in fold add_supers subs [] end blanchet@43926: blanchet@44489: fun make_class_rel_clause (sub, super) = blanchet@44489: {name = sub ^ "_" ^ super, subclass = `make_type_class sub, blanchet@43927: superclass = `make_type_class super} blanchet@43926: blanchet@43926: fun make_class_rel_clauses thy subs supers = blanchet@43934: map make_class_rel_clause (class_pairs thy subs supers) blanchet@43926: blanchet@43926: datatype combterm = blanchet@43926: CombConst of name * typ * typ list | blanchet@43926: CombVar of name * typ | nik@44536: CombApp of combterm * combterm | nik@44536: CombAbs of (name * typ) * combterm blanchet@43926: blanchet@43926: fun combtyp_of (CombConst (_, T, _)) = T blanchet@43926: | combtyp_of (CombVar (_, T)) = T blanchet@43926: | combtyp_of (CombApp (t1, _)) = snd (dest_funT (combtyp_of t1)) nik@44536: | combtyp_of (CombAbs ((_, T), tm)) = T --> combtyp_of tm blanchet@43926: blanchet@43926: (*gets the head of a combinator application, along with the list of arguments*) blanchet@43926: fun strip_combterm_comb u = blanchet@44367: let blanchet@44367: fun stripc (CombApp (t, u), ts) = stripc (t, u :: ts) blanchet@44367: | stripc x = x blanchet@44367: in stripc (u, []) end blanchet@43926: blanchet@43926: fun atyps_of T = fold_atyps (insert (op =)) T [] blanchet@43926: blanchet@43926: fun new_skolem_const_name s num_T_args = blanchet@43926: [new_skolem_const_prefix, s, string_of_int num_T_args] blanchet@43926: |> space_implode Long_Name.separator blanchet@43926: blanchet@43926: (* Converts a term (with combinators) into a combterm. Also accumulates sort blanchet@43926: infomation. *) blanchet@43926: fun combterm_from_term thy bs (P $ Q) = blanchet@43926: let blanchet@43926: val (P', P_atomics_Ts) = combterm_from_term thy bs P blanchet@43926: val (Q', Q_atomics_Ts) = combterm_from_term thy bs Q blanchet@43926: in (CombApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end blanchet@43926: | combterm_from_term thy _ (Const (c, T)) = blanchet@43926: let blanchet@43926: val tvar_list = blanchet@43926: (if String.isPrefix old_skolem_const_prefix c then blanchet@43926: [] |> Term.add_tvarsT T |> map TVar blanchet@43926: else blanchet@43926: (c, T) |> Sign.const_typargs thy) blanchet@43926: val c' = CombConst (`make_fixed_const c, T, tvar_list) blanchet@43926: in (c', atyps_of T) end blanchet@43926: | combterm_from_term _ _ (Free (v, T)) = blanchet@43926: (CombConst (`make_fixed_var v, T, []), atyps_of T) blanchet@43926: | combterm_from_term _ _ (Var (v as (s, _), T)) = blanchet@43926: (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then blanchet@43926: let blanchet@43926: val Ts = T |> strip_type |> swap |> op :: blanchet@43926: val s' = new_skolem_const_name s (length Ts) blanchet@43926: in CombConst (`make_fixed_const s', T, Ts) end blanchet@43926: else blanchet@43926: CombVar ((make_schematic_var v, s), T), atyps_of T) blanchet@43926: | combterm_from_term _ bs (Bound j) = blanchet@43926: nth bs j blanchet@43926: |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T)) nik@44536: | combterm_from_term thy bs (Abs (s, T, t)) = nik@44537: let nik@44537: fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string nik@44537: val s = vary s nik@44537: val (tm, atomic_Ts) = combterm_from_term thy ((s, T) :: bs) t nik@44537: in nik@44536: (CombAbs ((`make_bound_var s, T), tm), nik@44536: union (op =) atomic_Ts (atyps_of T)) nik@44536: end blanchet@43926: blanchet@44282: datatype locality = blanchet@44282: General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum | blanchet@44282: Chained blanchet@43926: blanchet@43926: (* (quasi-)underapproximation of the truth *) blanchet@43926: fun is_locality_global Local = false blanchet@43926: | is_locality_global Assum = false blanchet@43926: | is_locality_global Chained = false blanchet@43926: | is_locality_global _ = true blanchet@43926: blanchet@44491: datatype order = First_Order | Higher_Order blanchet@43484: datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic blanchet@43484: datatype type_level = blanchet@44233: All_Types | Noninf_Nonmono_Types | Fin_Nonmono_Types | Const_Arg_Types | blanchet@44233: No_Types blanchet@43969: datatype type_heaviness = Heavyweight | Lightweight blanchet@43484: blanchet@44493: datatype type_enc = blanchet@44491: Simple_Types of order * type_level | blanchet@43708: Preds of polymorphism * type_level * type_heaviness | blanchet@43708: Tags of polymorphism * type_level * type_heaviness blanchet@43484: blanchet@43559: fun try_unsuffixes ss s = blanchet@43559: fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE blanchet@43559: blanchet@44493: fun type_enc_from_string s = blanchet@43587: (case try (unprefix "poly_") s of blanchet@43587: SOME s => (SOME Polymorphic, s) blanchet@43484: | NONE => blanchet@43484: case try (unprefix "mono_") s of blanchet@43587: SOME s => (SOME Monomorphic, s) blanchet@43587: | NONE => blanchet@43587: case try (unprefix "mangled_") s of blanchet@43587: SOME s => (SOME Mangled_Monomorphic, s) blanchet@43587: | NONE => (NONE, s)) blanchet@43484: ||> (fn s => blanchet@44491: (* "_query" and "_bang" are for the ASCII-challenged Metis and blanchet@44491: Mirabelle. *) blanchet@43559: case try_unsuffixes ["?", "_query"] s of blanchet@44233: SOME s => (Noninf_Nonmono_Types, s) blanchet@43484: | NONE => blanchet@43559: case try_unsuffixes ["!", "_bang"] s of blanchet@44233: SOME s => (Fin_Nonmono_Types, s) blanchet@43484: | NONE => (All_Types, s)) blanchet@43699: ||> apsnd (fn s => blanchet@43708: case try (unsuffix "_heavy") s of blanchet@43969: SOME s => (Heavyweight, s) blanchet@43969: | NONE => (Lightweight, s)) blanchet@43708: |> (fn (poly, (level, (heaviness, core))) => blanchet@43708: case (core, (poly, level, heaviness)) of blanchet@44491: ("simple", (NONE, _, Lightweight)) => blanchet@44491: Simple_Types (First_Order, level) blanchet@44491: | ("simple_higher", (NONE, _, Lightweight)) => nik@44535: if level = Noninf_Nonmono_Types then raise Same.SAME nik@44535: else Simple_Types (Higher_Order, level) blanchet@43723: | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness) blanchet@43755: | ("tags", (SOME Polymorphic, _, _)) => blanchet@44232: Tags (Polymorphic, level, heaviness) blanchet@43723: | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness) blanchet@43969: | ("args", (SOME poly, All_Types (* naja *), Lightweight)) => blanchet@43969: Preds (poly, Const_Arg_Types, Lightweight) blanchet@43969: | ("erased", (NONE, All_Types (* naja *), Lightweight)) => blanchet@43969: Preds (Polymorphic, No_Types, Lightweight) blanchet@43618: | _ => raise Same.SAME) blanchet@43618: handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".") blanchet@43484: blanchet@44493: fun is_type_enc_higher_order (Simple_Types (Higher_Order, _)) = true blanchet@44493: | is_type_enc_higher_order _ = false blanchet@44491: blanchet@44493: fun polymorphism_of_type_enc (Simple_Types _) = Mangled_Monomorphic blanchet@44493: | polymorphism_of_type_enc (Preds (poly, _, _)) = poly blanchet@44493: | polymorphism_of_type_enc (Tags (poly, _, _)) = poly blanchet@43484: blanchet@44493: fun level_of_type_enc (Simple_Types (_, level)) = level blanchet@44493: | level_of_type_enc (Preds (_, level, _)) = level blanchet@44493: | level_of_type_enc (Tags (_, level, _)) = level blanchet@43699: blanchet@44493: fun heaviness_of_type_enc (Simple_Types _) = Heavyweight blanchet@44493: | heaviness_of_type_enc (Preds (_, _, heaviness)) = heaviness blanchet@44493: | heaviness_of_type_enc (Tags (_, _, heaviness)) = heaviness blanchet@43702: blanchet@43557: fun is_type_level_virtually_sound level = blanchet@44233: level = All_Types orelse level = Noninf_Nonmono_Types blanchet@44493: val is_type_enc_virtually_sound = blanchet@44493: is_type_level_virtually_sound o level_of_type_enc blanchet@43484: blanchet@43484: fun is_type_level_fairly_sound level = blanchet@44233: is_type_level_virtually_sound level orelse level = Fin_Nonmono_Types blanchet@44493: val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc blanchet@43484: blanchet@44491: fun choose_format formats (Simple_Types (order, level)) = blanchet@44491: if member (op =) formats THF then blanchet@44491: (THF, Simple_Types (order, level)) blanchet@44491: else if member (op =) formats TFF then blanchet@44491: (TFF, Simple_Types (First_Order, level)) blanchet@44491: else blanchet@44491: choose_format formats (Preds (Mangled_Monomorphic, level, Heavyweight)) blanchet@44493: | choose_format formats type_enc = blanchet@43942: (case hd formats of blanchet@43942: CNF_UEQ => blanchet@44493: (CNF_UEQ, case type_enc of blanchet@43942: Preds stuff => blanchet@44493: (if is_type_enc_fairly_sound type_enc then Tags else Preds) blanchet@43942: stuff blanchet@44493: | _ => type_enc) blanchet@44493: | format => (format, type_enc)) blanchet@43942: blanchet@40358: type translated_formula = blanchet@44367: {name : string, blanchet@44367: locality : locality, blanchet@44367: kind : formula_kind, blanchet@44367: combformula : (name, typ, combterm) formula, blanchet@44367: atomic_types : typ list} blanchet@38506: blanchet@43511: fun update_combformula f ({name, locality, kind, combformula, atomic_types} blanchet@43511: : translated_formula) = blanchet@43511: {name = name, locality = locality, kind = kind, combformula = f combformula, blanchet@43433: atomic_types = atomic_types} : translated_formula blanchet@43413: blanchet@43429: fun fact_lift f ({combformula, ...} : translated_formula) = f combformula blanchet@43429: blanchet@43905: val type_instance = Sign.typ_instance o Proof_Context.theory_of blanchet@43905: blanchet@43905: fun insert_type ctxt get_T x xs = blanchet@43905: let val T = get_T x in blanchet@43905: if exists (curry (type_instance ctxt) T o get_T) xs then xs blanchet@43905: else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs blanchet@43905: end blanchet@43547: blanchet@43618: (* The Booleans indicate whether all type arguments should be kept. *) blanchet@43618: datatype type_arg_policy = blanchet@43618: Explicit_Type_Args of bool | blanchet@43618: Mangled_Type_Args of bool | blanchet@43618: No_Type_Args blanchet@41384: blanchet@43707: fun should_drop_arg_type_args (Simple_Types _) = blanchet@43707: false (* since TFF doesn't support overloading *) blanchet@44493: | should_drop_arg_type_args type_enc = blanchet@44493: level_of_type_enc type_enc = All_Types andalso blanchet@44493: heaviness_of_type_enc type_enc = Heavyweight blanchet@43702: blanchet@44493: fun type_arg_policy type_enc s = blanchet@44495: if s = type_tag_name then blanchet@44493: (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then blanchet@44490: Mangled_Type_Args blanchet@44490: else blanchet@44490: Explicit_Type_Args) false blanchet@44495: else case type_enc of blanchet@44495: Tags (_, All_Types, Heavyweight) => No_Type_Args blanchet@44495: | _ => blanchet@44495: if level_of_type_enc type_enc = No_Types orelse blanchet@44495: s = @{const_name HOL.eq} orelse blanchet@44495: (s = app_op_name andalso blanchet@44495: level_of_type_enc type_enc = Const_Arg_Types) then blanchet@44495: No_Type_Args blanchet@44495: else blanchet@44495: should_drop_arg_type_args type_enc blanchet@44495: |> (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then blanchet@44495: Mangled_Type_Args blanchet@44495: else blanchet@44495: Explicit_Type_Args) blanchet@43088: blanchet@44495: (* Make literals for sorted type variables. *) blanchet@44104: fun generic_add_sorts_on_type (_, []) = I blanchet@44104: | generic_add_sorts_on_type ((x, i), s :: ss) = blanchet@44104: generic_add_sorts_on_type ((x, i), ss) blanchet@44104: #> (if s = the_single @{sort HOL.type} then blanchet@43934: I blanchet@43934: else if i = ~1 then blanchet@44104: insert (op =) (TyLitFree (`make_type_class s, `make_fixed_type_var x)) blanchet@43934: else blanchet@44104: insert (op =) (TyLitVar (`make_type_class s, blanchet@44104: (make_schematic_type_var (x, i), x)))) blanchet@44104: fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S) blanchet@44104: | add_sorts_on_tfree _ = I blanchet@44104: fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z blanchet@44104: | add_sorts_on_tvar _ = I blanchet@43926: blanchet@44493: fun type_literals_for_types type_enc add_sorts_on_typ Ts = blanchet@44493: [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts blanchet@41385: blanchet@43405: fun mk_aconns c phis = blanchet@43405: let val (phis', phi') = split_last phis in blanchet@43405: fold_rev (mk_aconn c) phis' phi' blanchet@43405: end blanchet@38506: fun mk_ahorn [] phi = phi blanchet@43405: | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi]) blanchet@43393: fun mk_aquant _ [] phi = phi blanchet@43393: | mk_aquant q xs (phi as AQuant (q', xs', phi')) = blanchet@43393: if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi) blanchet@43393: | mk_aquant q xs phi = AQuant (q, xs, phi) blanchet@38506: blanchet@43393: fun close_universally atom_vars phi = blanchet@41393: let blanchet@41393: fun formula_vars bounds (AQuant (_, xs, phi)) = blanchet@43397: formula_vars (map fst xs @ bounds) phi blanchet@41393: | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis blanchet@43393: | formula_vars bounds (AAtom tm) = blanchet@43397: union (op =) (atom_vars tm [] blanchet@43397: |> filter_out (member (op =) bounds o fst)) blanchet@43393: in mk_aquant AForall (formula_vars [] phi []) phi end blanchet@43393: blanchet@43402: fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2] blanchet@43393: | combterm_vars (CombConst _) = I blanchet@43445: | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T) nik@44536: | combterm_vars (CombAbs (_, tm)) = combterm_vars tm blanchet@43545: fun close_combformula_universally phi = close_universally combterm_vars phi blanchet@43393: nik@44535: fun term_vars bounds (ATerm (name as (s, _), tms)) = nik@44535: (is_tptp_variable s andalso not (member (op =) bounds name)) nik@44535: ? insert (op =) (name, NONE) #> fold (term_vars bounds) tms nik@44535: | term_vars bounds (AAbs ((name, _), tm)) = term_vars (name :: bounds) tm nik@44535: fun close_formula_universally phi = close_universally (term_vars []) phi blanchet@41393: blanchet@43835: val homo_infinite_type_name = @{type_name ind} (* any infinite type *) blanchet@43835: val homo_infinite_type = Type (homo_infinite_type_name, []) blanchet@43835: nik@44535: fun ho_term_from_typ format type_enc = blanchet@43835: let blanchet@43835: fun term (Type (s, Ts)) = blanchet@44493: ATerm (case (is_type_enc_higher_order type_enc, s) of blanchet@43835: (true, @{type_name bool}) => `I tptp_bool_type blanchet@43835: | (true, @{type_name fun}) => `I tptp_fun_type blanchet@44019: | _ => if s = homo_infinite_type_name andalso blanchet@44019: (format = TFF orelse format = THF) then blanchet@44019: `I tptp_individual_type blanchet@44019: else blanchet@44019: `make_fixed_type_const s, blanchet@43835: map term Ts) blanchet@43835: | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, []) blanchet@43835: | term (TVar ((x as (s, _)), _)) = blanchet@43835: ATerm ((make_schematic_type_var x, s), []) blanchet@43835: in term end blanchet@43433: nik@44535: fun ho_term_for_type_arg format type_enc T = nik@44535: if T = dummyT then NONE else SOME (ho_term_from_typ format type_enc T) blanchet@44264: blanchet@43433: (* This shouldn't clash with anything else. *) blanchet@43413: val mangled_type_sep = "\000" blanchet@43413: blanchet@43433: fun generic_mangled_type_name f (ATerm (name, [])) = f name blanchet@43433: | generic_mangled_type_name f (ATerm (name, tys)) = blanchet@43626: f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys) blanchet@43626: ^ ")" nik@44535: | generic_mangled_type_name f _ = raise Fail "unexpected type abstraction" blanchet@43413: blanchet@43839: val bool_atype = AType (`I tptp_bool_type) blanchet@43839: blanchet@43926: fun make_simple_type s = blanchet@43926: if s = tptp_bool_type orelse s = tptp_fun_type orelse blanchet@43926: s = tptp_individual_type then blanchet@43926: s blanchet@43926: else blanchet@43926: simple_type_prefix ^ ascii_of s blanchet@43926: nik@44535: fun ho_type_from_ho_term type_enc pred_sym ary = blanchet@43804: let blanchet@43804: fun to_atype ty = blanchet@43804: AType ((make_simple_type (generic_mangled_type_name fst ty), blanchet@43804: generic_mangled_type_name snd ty)) blanchet@43804: fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1)) blanchet@43839: fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty blanchet@43835: | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys nik@44535: | to_fo ary _ = raise Fail "unexpected type abstraction" blanchet@43835: fun to_ho (ty as ATerm ((s, _), tys)) = nik@44535: if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty nik@44535: | to_ho _ = raise Fail "unexpected type abstraction" blanchet@44493: in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end blanchet@43804: nik@44536: fun ho_type_from_typ format type_enc pred_sym ary = nik@44535: ho_type_from_ho_term type_enc pred_sym ary nik@44535: o ho_term_from_typ format type_enc blanchet@43804: blanchet@44493: fun mangled_const_name format type_enc T_args (s, s') = blanchet@43804: let nik@44535: val ty_args = T_args |> map_filter (ho_term_for_type_arg format type_enc) blanchet@43804: fun type_suffix f g = blanchet@43804: fold_rev (curry (op ^) o g o prefix mangled_type_sep blanchet@43804: o generic_mangled_type_name f) ty_args "" blanchet@43804: in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end blanchet@43413: blanchet@43413: val parse_mangled_ident = blanchet@43413: Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode blanchet@43413: blanchet@43413: fun parse_mangled_type x = blanchet@43413: (parse_mangled_ident blanchet@43413: -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")") blanchet@43413: [] >> ATerm) x blanchet@43413: and parse_mangled_types x = blanchet@43413: (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x blanchet@43413: blanchet@43413: fun unmangled_type s = blanchet@43413: s |> suffix ")" |> raw_explode blanchet@43413: |> Scan.finite Symbol.stopper blanchet@43413: (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^ blanchet@43413: quote s)) parse_mangled_type)) blanchet@43413: |> fst blanchet@43413: blanchet@43432: val unmangled_const_name = space_explode mangled_type_sep #> hd blanchet@43413: fun unmangled_const s = blanchet@43413: let val ss = space_explode mangled_type_sep s in blanchet@43413: (hd ss, map unmangled_type (tl ss)) blanchet@43413: end blanchet@43413: blanchet@44493: fun introduce_proxies type_enc = blanchet@43439: let blanchet@43858: fun intro top_level (CombApp (tm1, tm2)) = blanchet@43858: CombApp (intro top_level tm1, intro false tm2) blanchet@43858: | intro top_level (CombConst (name as (s, _), T, T_args)) = blanchet@43441: (case proxify_const s of blanchet@44000: SOME proxy_base => blanchet@44493: if top_level orelse is_type_enc_higher_order type_enc then blanchet@43841: case (top_level, s) of blanchet@43841: (_, "c_False") => (`I tptp_false, []) blanchet@43841: | (_, "c_True") => (`I tptp_true, []) blanchet@43841: | (false, "c_Not") => (`I tptp_not, []) blanchet@43841: | (false, "c_conj") => (`I tptp_and, []) blanchet@43841: | (false, "c_disj") => (`I tptp_or, []) blanchet@43841: | (false, "c_implies") => (`I tptp_implies, []) nik@44537: | (false, "c_All") => (`I tptp_ho_forall, []) nik@44537: | (false, "c_Ex") => (`I tptp_ho_exists, []) blanchet@43841: | (false, s) => blanchet@43858: if is_tptp_equal s then (`I tptp_equal, []) blanchet@43858: else (proxy_base |>> prefix const_prefix, T_args) blanchet@43841: | _ => (name, []) blanchet@43440: else blanchet@43445: (proxy_base |>> prefix const_prefix, T_args) blanchet@43445: | NONE => (name, T_args)) blanchet@43445: |> (fn (name, T_args) => CombConst (name, T, T_args)) nik@44536: | intro _ (CombAbs (bound, tm)) = CombAbs (bound, intro false tm) blanchet@43858: | intro _ tm = tm blanchet@43858: in intro true end blanchet@43439: blanchet@44493: fun combformula_from_prop thy type_enc eq_as_iff = blanchet@38506: let blanchet@43439: fun do_term bs t atomic_types = blanchet@41388: combterm_from_term thy bs (Envir.eta_contract t) blanchet@44493: |>> (introduce_proxies type_enc #> AAtom) blanchet@43439: ||> union (op =) atomic_types blanchet@38506: fun do_quant bs q s T t' = wenzelm@44206: let val s = singleton (Name.variant_list (map fst bs)) s in blanchet@38743: do_formula ((s, T) :: bs) t' blanchet@43433: #>> mk_aquant q [(`make_bound_var s, SOME T)] blanchet@38743: end blanchet@38506: and do_conn bs c t1 t2 = blanchet@44039: do_formula bs t1 ##>> do_formula bs t2 #>> uncurry (mk_aconn c) blanchet@38506: and do_formula bs t = blanchet@38506: case t of blanchet@43937: @{const Trueprop} $ t1 => do_formula bs t1 blanchet@43937: | @{const Not} $ t1 => do_formula bs t1 #>> mk_anot blanchet@38506: | Const (@{const_name All}, _) $ Abs (s, T, t') => blanchet@38506: do_quant bs AForall s T t' blanchet@38506: | Const (@{const_name Ex}, _) $ Abs (s, T, t') => blanchet@38506: do_quant bs AExists s T t' haftmann@39028: | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2 haftmann@39028: | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2 haftmann@39019: | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2 haftmann@39093: | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 => blanchet@41388: if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t blanchet@41388: | _ => do_term bs t blanchet@38506: in do_formula [] end blanchet@38506: blanchet@44105: fun presimplify_term _ [] t = t blanchet@44105: | presimplify_term ctxt presimp_consts t = blanchet@44105: t |> exists_Const (member (op =) presimp_consts o fst) t blanchet@44105: ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt) blanchet@44105: #> Meson.presimplify ctxt blanchet@44105: #> prop_of) blanchet@38506: wenzelm@41739: fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j blanchet@38506: fun conceal_bounds Ts t = blanchet@38506: subst_bounds (map (Free o apfst concealed_bound_name) blanchet@38506: (0 upto length Ts - 1 ~~ Ts), t) blanchet@38506: fun reveal_bounds Ts = blanchet@38506: subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j)) blanchet@38506: (0 upto length Ts - 1 ~~ Ts)) blanchet@38506: blanchet@44106: fun is_fun_equality (@{const_name HOL.eq}, blanchet@44106: Type (_, [Type (@{type_name fun}, _), _])) = true blanchet@44106: | is_fun_equality _ = false blanchet@44106: blanchet@43612: fun extensionalize_term ctxt t = blanchet@44106: if exists_Const is_fun_equality t then blanchet@44106: let val thy = Proof_Context.theory_of ctxt in blanchet@44106: t |> cterm_of thy |> Meson.extensionalize_conv ctxt blanchet@44106: |> prop_of |> Logic.dest_equals |> snd blanchet@44106: end blanchet@44106: else blanchet@44106: t blanchet@38831: nik@44537: fun process_abstractions_in_term ctxt type_enc kind t = wenzelm@43232: let val thy = Proof_Context.theory_of ctxt in blanchet@38716: if Meson.is_fol_term thy t then blanchet@38716: t blanchet@38716: else blanchet@38716: let blanchet@38716: fun aux Ts t = blanchet@38716: case t of blanchet@38716: @{const Not} $ t1 => @{const Not} $ aux Ts t1 blanchet@38716: | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') => blanchet@38716: t0 $ Abs (s, T, aux (T :: Ts) t') blanchet@38890: | (t0 as Const (@{const_name All}, _)) $ t1 => blanchet@38890: aux Ts (t0 $ eta_expand Ts t1 1) blanchet@38716: | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') => blanchet@38716: t0 $ Abs (s, T, aux (T :: Ts) t') blanchet@38890: | (t0 as Const (@{const_name Ex}, _)) $ t1 => blanchet@38890: aux Ts (t0 $ eta_expand Ts t1 1) haftmann@39028: | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 haftmann@39028: | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 haftmann@39019: | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 haftmann@39093: | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _]))) blanchet@38716: $ t1 $ t2 => blanchet@38716: t0 $ aux Ts t1 $ aux Ts t2 blanchet@38716: | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then blanchet@38716: t nik@44537: else if is_type_enc_higher_order type_enc then nik@44537: t |> Envir.eta_contract blanchet@38716: else blanchet@38716: t |> conceal_bounds Ts blanchet@38716: |> Envir.eta_contract blanchet@38716: |> cterm_of thy blanchet@40071: |> Meson_Clausify.introduce_combinators_in_cterm blanchet@38716: |> prop_of |> Logic.dest_equals |> snd blanchet@38716: |> reveal_bounds Ts blanchet@39616: val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single blanchet@38716: in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end blanchet@38716: handle THM _ => blanchet@38716: (* A type variable of sort "{}" will make abstraction fail. *) blanchet@38836: if kind = Conjecture then HOLogic.false_const blanchet@38836: else HOLogic.true_const blanchet@38716: end blanchet@38506: blanchet@38506: (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the blanchet@43224: same in Sledgehammer to prevent the discovery of unreplayable proofs. *) blanchet@38506: fun freeze_term t = blanchet@38506: let blanchet@38506: fun aux (t $ u) = aux t $ aux u blanchet@38506: | aux (Abs (s, T, t)) = Abs (s, T, aux t) blanchet@38506: | aux (Var ((s, i), T)) = blanchet@38506: Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T) blanchet@38506: | aux t = t blanchet@38506: in t |> exists_subterm is_Var t ? aux end blanchet@38506: nik@44536: fun preprocess_prop ctxt type_enc presimp_consts kind t = blanchet@38506: let wenzelm@43232: val thy = Proof_Context.theory_of ctxt blanchet@38831: val t = t |> Envir.beta_eta_contract blanchet@43785: |> transform_elim_prop blanchet@41459: |> Object_Logic.atomize_term thy blanchet@43434: val need_trueprop = (fastype_of t = @{typ bool}) blanchet@43937: in blanchet@43937: t |> need_trueprop ? HOLogic.mk_Trueprop blanchet@43937: |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) [] blanchet@43937: |> extensionalize_term ctxt blanchet@44105: |> presimplify_term ctxt presimp_consts blanchet@43961: |> perhaps (try (HOLogic.dest_Trueprop)) nik@44537: |> process_abstractions_in_term ctxt type_enc kind blanchet@43937: end blanchet@43937: blanchet@43937: (* making fact and conjecture formulas *) blanchet@44493: fun make_formula thy type_enc eq_as_iff name loc kind t = blanchet@43937: let blanchet@43803: val (combformula, atomic_types) = blanchet@44493: combformula_from_prop thy type_enc eq_as_iff t [] blanchet@38506: in blanchet@43511: {name = name, locality = loc, kind = kind, combformula = combformula, blanchet@43433: atomic_types = atomic_types} blanchet@38506: end blanchet@38506: blanchet@44493: fun make_fact ctxt format type_enc eq_as_iff preproc presimp_consts blanchet@43835: ((name, loc), t) = blanchet@43937: let val thy = Proof_Context.theory_of ctxt in nik@44536: case t |> preproc ? preprocess_prop ctxt type_enc presimp_consts Axiom blanchet@44493: |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name blanchet@44491: loc Axiom of blanchet@44153: formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} => blanchet@43937: if s = tptp_true then NONE else SOME formula blanchet@44153: | formula => SOME formula blanchet@43937: end blanchet@43432: blanchet@44493: fun make_conjecture ctxt format prem_kind type_enc preproc presimp_consts ts = blanchet@43937: let blanchet@43937: val thy = Proof_Context.theory_of ctxt blanchet@43937: val last = length ts - 1 blanchet@43937: in blanchet@43580: map2 (fn j => fn t => blanchet@43580: let blanchet@43580: val (kind, maybe_negate) = blanchet@43580: if j = last then blanchet@43580: (Conjecture, I) blanchet@43580: else blanchet@43580: (prem_kind, blanchet@43580: if prem_kind = Conjecture then update_combformula mk_anot blanchet@43580: else I) blanchet@43580: in blanchet@44105: t |> preproc ? nik@44536: (preprocess_prop ctxt type_enc presimp_consts kind #> freeze_term) blanchet@44493: |> make_formula thy type_enc (format <> CNF) (string_of_int j) blanchet@44491: Local kind blanchet@43803: |> maybe_negate blanchet@43580: end) blanchet@38836: (0 upto last) ts blanchet@38836: end blanchet@38506: blanchet@43552: (** Finite and infinite type inference **) blanchet@43552: blanchet@43755: fun deep_freeze_atyp (TVar (_, S)) = TFree ("v", S) blanchet@43755: | deep_freeze_atyp T = T blanchet@43755: val deep_freeze_type = map_atyps deep_freeze_atyp blanchet@43755: blanchet@43552: (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are blanchet@43552: dangerous because their "exhaust" properties can easily lead to unsound ATP blanchet@43552: proofs. On the other hand, all HOL infinite types can be given the same blanchet@43552: models in first-order logic (via Löwenheim-Skolem). *) blanchet@43552: blanchet@43755: fun should_encode_type ctxt (nonmono_Ts as _ :: _) _ T = blanchet@43755: exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts blanchet@43707: | should_encode_type _ _ All_Types _ = true blanchet@44434: | should_encode_type ctxt _ Fin_Nonmono_Types T = blanchet@44434: is_type_surely_finite ctxt false T blanchet@43552: | should_encode_type _ _ _ _ = false blanchet@43552: blanchet@43708: fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness)) blanchet@43705: should_predicate_on_var T = blanchet@43969: (heaviness = Heavyweight orelse should_predicate_on_var ()) andalso blanchet@43747: should_encode_type ctxt nonmono_Ts level T blanchet@43705: | should_predicate_on_type _ _ _ _ _ = false blanchet@43552: blanchet@43707: fun is_var_or_bound_var (CombConst ((s, _), _, _)) = blanchet@43707: String.isPrefix bound_var_prefix s blanchet@43707: | is_var_or_bound_var (CombVar _) = true blanchet@43707: | is_var_or_bound_var _ = false blanchet@43707: blanchet@44232: datatype tag_site = blanchet@44232: Top_Level of bool option | blanchet@44232: Eq_Arg of bool option | blanchet@44232: Elsewhere blanchet@43700: blanchet@44232: fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false blanchet@44232: | should_tag_with_type ctxt nonmono_Ts (Tags (poly, level, heaviness)) site blanchet@44232: u T = blanchet@43708: (case heaviness of blanchet@43969: Heavyweight => should_encode_type ctxt nonmono_Ts level T blanchet@43969: | Lightweight => blanchet@43707: case (site, is_var_or_bound_var u) of blanchet@44232: (Eq_Arg pos, true) => blanchet@44232: (* The first disjunct prevents a subtle soundness issue explained in blanchet@44232: Blanchette's Ph.D. thesis. See also blanchet@44232: "formula_lines_for_lightweight_tags_sym_decl". *) blanchet@44232: (pos <> SOME false andalso poly = Polymorphic andalso blanchet@44232: level <> All_Types andalso heaviness = Lightweight andalso blanchet@44232: exists (fn T' => type_instance ctxt (T', T)) nonmono_Ts) orelse blanchet@44232: should_encode_type ctxt nonmono_Ts level T blanchet@43700: | _ => false) blanchet@43700: | should_tag_with_type _ _ _ _ _ _ = false blanchet@43552: blanchet@43835: fun homogenized_type ctxt nonmono_Ts level = blanchet@43835: let blanchet@43835: val should_encode = should_encode_type ctxt nonmono_Ts level blanchet@43835: fun homo 0 T = if should_encode T then T else homo_infinite_type blanchet@43835: | homo ary (Type (@{type_name fun}, [T1, T2])) = blanchet@43835: homo 0 T1 --> homo (ary - 1) T2 blanchet@43835: | homo _ _ = raise Fail "expected function type" blanchet@43835: in homo end blanchet@43552: blanchet@43444: (** "hBOOL" and "hAPP" **) blanchet@41561: blanchet@43445: type sym_info = blanchet@43905: {pred_sym : bool, min_ary : int, max_ary : int, types : typ list} blanchet@43434: blanchet@43905: fun add_combterm_syms_to_table ctxt explicit_apply = blanchet@43429: let blanchet@43905: fun consider_var_arity const_T var_T max_ary = blanchet@43905: let blanchet@43905: fun iter ary T = blanchet@44051: if ary = max_ary orelse type_instance ctxt (var_T, T) orelse blanchet@44051: type_instance ctxt (T, var_T) then blanchet@44051: ary blanchet@44051: else blanchet@44051: iter (ary + 1) (range_type T) blanchet@43905: in iter 0 const_T end blanchet@44042: fun add_var_or_bound_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) = blanchet@44042: if explicit_apply = NONE andalso blanchet@44042: (can dest_funT T orelse T = @{typ bool}) then blanchet@44042: let blanchet@44042: val bool_vars' = bool_vars orelse body_type T = @{typ bool} blanchet@44042: fun repair_min_arity {pred_sym, min_ary, max_ary, types} = blanchet@44042: {pred_sym = pred_sym andalso not bool_vars', blanchet@44054: min_ary = fold (fn T' => consider_var_arity T' T) types min_ary, blanchet@44042: max_ary = max_ary, types = types} blanchet@44042: val fun_var_Ts' = blanchet@44042: fun_var_Ts |> can dest_funT T ? insert_type ctxt I T blanchet@44042: in blanchet@44042: if bool_vars' = bool_vars andalso blanchet@44042: pointer_eq (fun_var_Ts', fun_var_Ts) then blanchet@44042: accum blanchet@44008: else blanchet@44054: ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_arity) sym_tab) blanchet@44042: end blanchet@44042: else blanchet@44042: accum blanchet@44042: fun add top_level tm (accum as ((bool_vars, fun_var_Ts), sym_tab)) = blanchet@44042: let val (head, args) = strip_combterm_comb tm in blanchet@43429: (case head of blanchet@43434: CombConst ((s, _), T, _) => blanchet@43429: if String.isPrefix bound_var_prefix s then blanchet@44042: add_var_or_bound_var T accum blanchet@43429: else blanchet@43980: let val ary = length args in blanchet@44042: ((bool_vars, fun_var_Ts), blanchet@43905: case Symtab.lookup sym_tab s of blanchet@43905: SOME {pred_sym, min_ary, max_ary, types} => blanchet@43905: let blanchet@44042: val pred_sym = blanchet@44042: pred_sym andalso top_level andalso not bool_vars blanchet@43905: val types' = types |> insert_type ctxt I T blanchet@43905: val min_ary = blanchet@43905: if is_some explicit_apply orelse blanchet@43905: pointer_eq (types', types) then blanchet@43905: min_ary blanchet@43905: else blanchet@44042: fold (consider_var_arity T) fun_var_Ts min_ary blanchet@43905: in blanchet@44042: Symtab.update (s, {pred_sym = pred_sym, blanchet@43905: min_ary = Int.min (ary, min_ary), blanchet@43905: max_ary = Int.max (ary, max_ary), blanchet@43905: types = types'}) blanchet@43905: sym_tab blanchet@43905: end blanchet@43905: | NONE => blanchet@43905: let blanchet@44042: val pred_sym = top_level andalso not bool_vars blanchet@43905: val min_ary = blanchet@43905: case explicit_apply of blanchet@43905: SOME true => 0 blanchet@43905: | SOME false => ary blanchet@44042: | NONE => fold (consider_var_arity T) fun_var_Ts ary blanchet@43905: in blanchet@44042: Symtab.update_new (s, {pred_sym = pred_sym, blanchet@43905: min_ary = min_ary, max_ary = ary, blanchet@43905: types = [T]}) blanchet@43905: sym_tab blanchet@43905: end) blanchet@43905: end blanchet@44042: | CombVar (_, T) => add_var_or_bound_var T accum nik@44537: | CombAbs ((_, T), tm) => nik@44537: accum |> add_var_or_bound_var T |> add false tm blanchet@43905: | _ => accum) blanchet@43905: |> fold (add false) args blanchet@43429: end blanchet@43905: in add true end blanchet@43905: fun add_fact_syms_to_table ctxt explicit_apply = blanchet@43905: fact_lift (formula_fold NONE blanchet@43905: (K (add_combterm_syms_to_table ctxt explicit_apply))) blanchet@38506: blanchet@43980: val default_sym_tab_entries : (string * sym_info) list = blanchet@44015: (prefixed_predicator_name, blanchet@43980: {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) :: blanchet@43439: ([tptp_false, tptp_true] blanchet@43980: |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @ blanchet@43980: ([tptp_equal, tptp_old_equal] blanchet@43980: |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []})) blanchet@41388: blanchet@43905: fun sym_table_for_facts ctxt explicit_apply facts = blanchet@44042: ((false, []), Symtab.empty) blanchet@44042: |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd blanchet@43980: |> fold Symtab.update default_sym_tab_entries blanchet@38506: blanchet@43429: fun min_arity_of sym_tab s = blanchet@43429: case Symtab.lookup sym_tab s of blanchet@43445: SOME ({min_ary, ...} : sym_info) => min_ary blanchet@43429: | NONE => blanchet@43429: case strip_prefix_and_unascii const_prefix s of blanchet@43418: SOME s => blanchet@43441: let val s = s |> unmangled_const_name |> invert_const in blanchet@43807: if s = predicator_name then 1 blanchet@43807: else if s = app_op_name then 2 blanchet@43807: else if s = type_pred_name then 1 blanchet@43428: else 0 blanchet@43418: end blanchet@38506: | NONE => 0 blanchet@38506: blanchet@38506: (* True if the constant ever appears outside of the top-level position in blanchet@38506: literals, or if it appears with different arities (e.g., because of different blanchet@38506: type instantiations). If false, the constant always receives all of its blanchet@38506: arguments and is used as a predicate. *) blanchet@43429: fun is_pred_sym sym_tab s = blanchet@43429: case Symtab.lookup sym_tab s of blanchet@43445: SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) => blanchet@43445: pred_sym andalso min_ary = max_ary blanchet@43429: | NONE => false blanchet@38506: blanchet@43439: val predicator_combconst = blanchet@43807: CombConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, []) blanchet@43439: fun predicator tm = CombApp (predicator_combconst, tm) blanchet@38506: blanchet@43439: fun introduce_predicators_in_combterm sym_tab tm = blanchet@43413: case strip_combterm_comb tm of blanchet@43413: (CombConst ((s, _), _, _), _) => blanchet@43439: if is_pred_sym sym_tab s then tm else predicator tm blanchet@43439: | _ => predicator tm blanchet@38506: blanchet@43415: fun list_app head args = fold (curry (CombApp o swap)) args head blanchet@38506: blanchet@43971: val app_op = `make_fixed_const app_op_name blanchet@43971: blanchet@43415: fun explicit_app arg head = blanchet@43415: let blanchet@43433: val head_T = combtyp_of head blanchet@43563: val (arg_T, res_T) = dest_funT head_T blanchet@43415: val explicit_app = blanchet@43971: CombConst (app_op, head_T --> head_T, [arg_T, res_T]) blanchet@43415: in list_app explicit_app [head, arg] end blanchet@43415: fun list_explicit_app head args = fold explicit_app args head blanchet@43415: blanchet@43436: fun introduce_explicit_apps_in_combterm sym_tab = blanchet@43415: let blanchet@43415: fun aux tm = blanchet@43415: case strip_combterm_comb tm of blanchet@43415: (head as CombConst ((s, _), _, _), args) => blanchet@43415: args |> map aux blanchet@43428: |> chop (min_arity_of sym_tab s) blanchet@43415: |>> list_app head blanchet@43415: |-> list_explicit_app blanchet@43415: | (head, args) => list_explicit_app head (map aux args) blanchet@43415: in aux end blanchet@43415: blanchet@43618: fun chop_fun 0 T = ([], T) blanchet@43618: | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) = blanchet@43618: chop_fun (n - 1) ran_T |>> cons dom_T blanchet@43618: | chop_fun _ _ = raise Fail "unexpected non-function" blanchet@43618: blanchet@43651: fun filter_type_args _ _ _ [] = [] blanchet@43651: | filter_type_args thy s arity T_args = blanchet@43705: let blanchet@43705: (* will throw "TYPE" for pseudo-constants *) blanchet@43807: val U = if s = app_op_name then blanchet@43705: @{typ "('a => 'b) => 'a => 'b"} |> Logic.varifyT_global blanchet@43705: else blanchet@43705: s |> Sign.the_const_type thy blanchet@43705: in blanchet@43652: case Term.add_tvarsT (U |> chop_fun arity |> snd) [] of blanchet@43652: [] => [] blanchet@43652: | res_U_vars => blanchet@43652: let val U_args = (s, U) |> Sign.const_typargs thy in blanchet@43652: U_args ~~ T_args blanchet@44264: |> map (fn (U, T) => blanchet@44264: if member (op =) res_U_vars (dest_TVar U) then T blanchet@44264: else dummyT) blanchet@43652: end blanchet@43651: end blanchet@43651: handle TYPE _ => T_args blanchet@43618: blanchet@44493: fun enforce_type_arg_policy_in_combterm ctxt format type_enc = blanchet@43618: let blanchet@43618: val thy = Proof_Context.theory_of ctxt blanchet@43618: fun aux arity (CombApp (tm1, tm2)) = blanchet@43618: CombApp (aux (arity + 1) tm1, aux 0 tm2) blanchet@43618: | aux arity (CombConst (name as (s, _), T, T_args)) = blanchet@44020: (case strip_prefix_and_unascii const_prefix s of blanchet@44020: NONE => (name, T_args) blanchet@44020: | SOME s'' => blanchet@44020: let blanchet@44020: val s'' = invert_const s'' blanchet@44020: fun filtered_T_args false = T_args blanchet@44020: | filtered_T_args true = filter_type_args thy s'' arity T_args blanchet@44020: in blanchet@44493: case type_arg_policy type_enc s'' of blanchet@44020: Explicit_Type_Args drop_args => blanchet@44020: (name, filtered_T_args drop_args) blanchet@44020: | Mangled_Type_Args drop_args => blanchet@44493: (mangled_const_name format type_enc (filtered_T_args drop_args) blanchet@44020: name, []) blanchet@44020: | No_Type_Args => (name, []) blanchet@44020: end) blanchet@44020: |> (fn (name, T_args) => CombConst (name, T, T_args)) nik@44536: | aux _ (CombAbs (bound, tm)) = CombAbs (bound, aux 0 tm) blanchet@43618: | aux _ tm = tm blanchet@43618: in aux 0 end blanchet@43444: blanchet@44493: fun repair_combterm ctxt format type_enc sym_tab = blanchet@44493: not (is_type_enc_higher_order type_enc) blanchet@43835: ? (introduce_explicit_apps_in_combterm sym_tab blanchet@43835: #> introduce_predicators_in_combterm sym_tab) blanchet@44493: #> enforce_type_arg_policy_in_combterm ctxt format type_enc blanchet@44493: fun repair_fact ctxt format type_enc sym_tab = blanchet@43571: update_combformula (formula_map blanchet@44493: (repair_combterm ctxt format type_enc sym_tab)) blanchet@43444: blanchet@43444: (** Helper facts **) blanchet@43444: blanchet@44035: (* The Boolean indicates that a fairly sound type encoding is needed. *) blanchet@43926: val helper_table = blanchet@44035: [(("COMBI", false), @{thms Meson.COMBI_def}), blanchet@44035: (("COMBK", false), @{thms Meson.COMBK_def}), blanchet@44035: (("COMBB", false), @{thms Meson.COMBB_def}), blanchet@44035: (("COMBC", false), @{thms Meson.COMBC_def}), blanchet@44035: (("COMBS", false), @{thms Meson.COMBS_def}), blanchet@44035: (("fFalse", false), [@{lemma "~ fFalse" by (unfold fFalse_def) fast}]), blanchet@44035: (("fFalse", true), @{thms True_or_False}), blanchet@44035: (("fTrue", false), [@{lemma "fTrue" by (unfold fTrue_def) fast}]), blanchet@44035: (("fTrue", true), @{thms True_or_False}), blanchet@44035: (("fNot", false), blanchet@44035: @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1] blanchet@44035: fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}), blanchet@44035: (("fconj", false), blanchet@44035: @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q" blanchet@44035: by (unfold fconj_def) fast+}), blanchet@44035: (("fdisj", false), blanchet@44035: @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q" blanchet@44035: by (unfold fdisj_def) fast+}), blanchet@44035: (("fimplies", false), blanchet@44051: @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" "~ fimplies P Q | ~ P | Q" blanchet@44035: by (unfold fimplies_def) fast+}), nik@44537: (("fequal", true), nik@44537: (* This is a lie: Higher-order equality doesn't need a sound type encoding. nik@44537: However, this is done so for backward compatibility: Including the nik@44537: equality helpers by default in Metis breaks a few existing proofs. *) nik@44537: @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1] nik@44537: fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}), nik@44537: (("fAll", false), []), (*TODO: add helpers*) nik@44537: (("fEx", false), []), (*TODO: add helpers*) blanchet@44035: (("If", true), @{thms if_True if_False True_or_False})] blanchet@44035: |> map (apsnd (map zero_var_indexes)) blanchet@43926: blanchet@43971: val type_tag = `make_fixed_const type_tag_name blanchet@43971: blanchet@44000: fun type_tag_idempotence_fact () = blanchet@43444: let blanchet@43444: fun var s = ATerm (`I s, []) blanchet@44000: fun tag tm = ATerm (type_tag, [var "T", tm]) blanchet@44048: val tagged_a = tag (var "A") blanchet@43444: in blanchet@44000: Formula (type_tag_idempotence_helper_name, Axiom, blanchet@44048: AAtom (ATerm (`I tptp_equal, [tag tagged_a, tagged_a])) blanchet@43748: |> close_formula_universally, simp_info, NONE) blanchet@43444: end blanchet@43444: blanchet@44493: fun should_specialize_helper type_enc t = blanchet@44495: polymorphism_of_type_enc type_enc = Mangled_Monomorphic andalso blanchet@44495: level_of_type_enc type_enc <> No_Types andalso blanchet@44495: not (null (Term.hidden_polymorphism t)) blanchet@44000: blanchet@44493: fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) = blanchet@43444: case strip_prefix_and_unascii const_prefix s of blanchet@43444: SOME mangled_s => blanchet@43444: let blanchet@43444: val thy = Proof_Context.theory_of ctxt blanchet@43444: val unmangled_s = mangled_s |> unmangled_const_name blanchet@44495: fun dub needs_fairly_sound j k = blanchet@44495: (unmangled_s ^ "_" ^ string_of_int j ^ "_" ^ string_of_int k ^ blanchet@44495: (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^ blanchet@44495: (if needs_fairly_sound then typed_helper_suffix blanchet@44495: else untyped_helper_suffix), blanchet@44495: Helper) blanchet@44000: fun dub_and_inst needs_fairly_sound (th, j) = blanchet@44495: let val t = prop_of th in blanchet@44495: if should_specialize_helper type_enc t then blanchet@44495: map (fn T => specialize_type thy (invert_const unmangled_s, T) t) blanchet@44495: types blanchet@44495: else blanchet@44495: [t] blanchet@44495: end blanchet@44495: |> map (fn (k, t) => (dub needs_fairly_sound j k, t)) o tag_list 1 blanchet@44000: val make_facts = blanchet@44493: map_filter (make_fact ctxt format type_enc false false []) blanchet@44493: val fairly_sound = is_type_enc_fairly_sound type_enc blanchet@43444: in blanchet@43926: helper_table blanchet@44035: |> maps (fn ((helper_s, needs_fairly_sound), ths) => blanchet@44000: if helper_s <> unmangled_s orelse blanchet@43765: (needs_fairly_sound andalso not fairly_sound) then blanchet@43444: [] blanchet@43444: else blanchet@43444: ths ~~ (1 upto length ths) blanchet@44495: |> maps (dub_and_inst needs_fairly_sound) blanchet@44000: |> make_facts) blanchet@43444: end blanchet@43444: | NONE => [] blanchet@44493: fun helper_facts_for_sym_table ctxt format type_enc sym_tab = blanchet@44493: Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab blanchet@43803: [] blanchet@43444: blanchet@43926: (***************************************************************) blanchet@43926: (* Type Classes Present in the Axiom or Conjecture Clauses *) blanchet@43926: (***************************************************************) blanchet@43926: blanchet@43926: fun set_insert (x, s) = Symtab.update (x, ()) s blanchet@43926: blanchet@43926: fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts) blanchet@43926: blanchet@43926: (* Remove this trivial type class (FIXME: similar code elsewhere) *) blanchet@43926: fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset blanchet@43926: blanchet@43934: fun classes_of_terms get_Ts = blanchet@43962: map (map snd o get_Ts) blanchet@43934: #> List.foldl add_classes Symtab.empty blanchet@43934: #> delete_type #> Symtab.keys blanchet@43926: blanchet@43934: val tfree_classes_of_terms = classes_of_terms OldTerm.term_tfrees blanchet@43934: val tvar_classes_of_terms = classes_of_terms OldTerm.term_tvars blanchet@43926: blanchet@44489: fun fold_type_constrs f (Type (s, Ts)) x = blanchet@44489: fold (fold_type_constrs f) Ts (f (s, x)) blanchet@44030: | fold_type_constrs _ _ x = x blanchet@43926: blanchet@43926: (*Type constructors used to instantiate overloaded constants are the only ones needed.*) blanchet@44030: fun add_type_constrs_in_term thy = blanchet@43926: let blanchet@44029: fun add (Const (@{const_name Meson.skolem}, _) $ _) = I blanchet@44022: | add (t $ u) = add t #> add u blanchet@44029: | add (Const (x as (s, _))) = blanchet@44029: if String.isPrefix skolem_const_prefix s then I blanchet@44030: else x |> Sign.const_typargs thy |> fold (fold_type_constrs set_insert) blanchet@44022: | add (Abs (_, _, u)) = add u blanchet@44022: | add _ = I blanchet@44022: in add end blanchet@43926: blanchet@44030: fun type_constrs_of_terms thy ts = blanchet@44030: Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty) blanchet@43926: blanchet@44493: fun translate_formulas ctxt format prem_kind type_enc preproc hyp_ts concl_t blanchet@44055: facts = blanchet@43444: let blanchet@43444: val thy = Proof_Context.theory_of ctxt blanchet@44063: val fact_ts = facts |> map snd blanchet@44105: val presimp_consts = Meson.presimplified_consts ctxt blanchet@44493: val make_fact = make_fact ctxt format type_enc true preproc presimp_consts blanchet@43444: val (facts, fact_names) = blanchet@44105: facts |> map (fn (name, t) => (name, t) |> make_fact |> rpair name) blanchet@44055: |> map_filter (try (apfst the)) blanchet@44055: |> ListPair.unzip blanchet@43444: (* Remove existing facts from the conjecture, as this can dramatically blanchet@43444: boost an ATP's performance (for some reason). *) blanchet@44033: val hyp_ts = blanchet@44033: hyp_ts blanchet@44033: |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t) blanchet@43444: val goal_t = Logic.list_implies (hyp_ts, concl_t) blanchet@43444: val all_ts = goal_t :: fact_ts blanchet@43444: val subs = tfree_classes_of_terms all_ts blanchet@43444: val supers = tvar_classes_of_terms all_ts blanchet@44030: val tycons = type_constrs_of_terms thy all_ts blanchet@43835: val conjs = blanchet@43937: hyp_ts @ [concl_t] blanchet@44493: |> make_conjecture ctxt format prem_kind type_enc preproc presimp_consts blanchet@43444: val (supers', arity_clauses) = blanchet@44493: if level_of_type_enc type_enc = No_Types then ([], []) blanchet@43444: else make_arity_clauses thy tycons supers blanchet@43444: val class_rel_clauses = make_class_rel_clauses thy subs supers' blanchet@43444: in blanchet@43444: (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses)) blanchet@43444: end blanchet@43444: blanchet@43444: fun fo_literal_from_type_literal (TyLitVar (class, name)) = blanchet@43444: (true, ATerm (class, [ATerm (name, [])])) blanchet@43444: | fo_literal_from_type_literal (TyLitFree (class, name)) = blanchet@43444: (true, ATerm (class, [ATerm (name, [])])) blanchet@43444: blanchet@43444: fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot blanchet@43444: blanchet@43971: val type_pred = `make_fixed_const type_pred_name blanchet@43971: blanchet@44493: fun type_pred_combterm ctxt format type_enc T tm = blanchet@44020: CombApp (CombConst (type_pred, T --> @{typ bool}, [T]) blanchet@44493: |> enforce_type_arg_policy_in_combterm ctxt format type_enc, tm) blanchet@43444: blanchet@44282: fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum blanchet@44282: | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum = blanchet@43841: accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, []))) nik@44535: | is_var_positively_naked_in_term name _ _ _ = true blanchet@44364: fun should_predicate_on_var_in_formula pos phi (SOME true) name = blanchet@44282: formula_fold pos (is_var_positively_naked_in_term name) phi false blanchet@44364: | should_predicate_on_var_in_formula _ _ _ _ = true blanchet@43705: nik@44536: fun mk_aterm format type_enc name T_args args = nik@44536: ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args) blanchet@43835: blanchet@44493: fun tag_with_type ctxt format nonmono_Ts type_enc pos T tm = blanchet@43971: CombConst (type_tag, T --> T, [T]) blanchet@44493: |> enforce_type_arg_policy_in_combterm ctxt format type_enc nik@44536: |> ho_term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos) blanchet@43700: |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])) nik@44536: and ho_term_from_combterm ctxt format nonmono_Ts type_enc = blanchet@43444: let blanchet@43803: fun aux site u = blanchet@43803: let blanchet@43803: val (head, args) = strip_combterm_comb u nik@44536: val pos = nik@44536: case site of nik@44536: Top_Level pos => pos nik@44536: | Eq_Arg pos => pos nik@44536: | Elsewhere => NONE nik@44536: val t = blanchet@43803: case head of nik@44536: CombConst (name as (s, _), _, T_args) => nik@44536: let nik@44536: val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere nik@44536: in nik@44536: mk_aterm format type_enc name T_args (map (aux arg_site) args) nik@44536: end nik@44537: | CombVar (name, _) => mk_aterm format type_enc name [] (map (aux Elsewhere) args) nik@44536: | CombAbs ((name, T), tm) => nik@44536: AAbs ((name, ho_type_from_typ format type_enc true 0 T), aux Elsewhere tm) blanchet@43803: | CombApp _ => raise Fail "impossible \"CombApp\"" blanchet@43803: val T = combtyp_of u blanchet@43803: in blanchet@44493: t |> (if should_tag_with_type ctxt nonmono_Ts type_enc site u T then blanchet@44493: tag_with_type ctxt format nonmono_Ts type_enc pos T blanchet@43803: else blanchet@43803: I) blanchet@43803: end blanchet@43803: in aux end blanchet@44493: and formula_from_combformula ctxt format nonmono_Ts type_enc blanchet@43803: should_predicate_on_var = blanchet@43700: let blanchet@44232: fun do_term pos = nik@44536: ho_term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos) blanchet@43444: val do_bound_type = blanchet@44493: case type_enc of blanchet@44491: Simple_Types (_, level) => blanchet@43835: homogenized_type ctxt nonmono_Ts level 0 nik@44536: #> ho_type_from_typ format type_enc false 0 #> SOME blanchet@43552: | _ => K NONE blanchet@43747: fun do_out_of_bound_type pos phi universal (name, T) = blanchet@44493: if should_predicate_on_type ctxt nonmono_Ts type_enc blanchet@43747: (fn () => should_predicate_on_var pos phi universal name) T then blanchet@43705: CombVar (name, T) blanchet@44493: |> type_pred_combterm ctxt format type_enc T blanchet@44232: |> do_term pos |> AAtom |> SOME blanchet@43444: else blanchet@43444: NONE blanchet@43747: fun do_formula pos (AQuant (q, xs, phi)) = blanchet@43747: let blanchet@43747: val phi = phi |> do_formula pos blanchet@43747: val universal = Option.map (q = AExists ? not) pos blanchet@43747: in blanchet@43705: AQuant (q, xs |> map (apsnd (fn NONE => NONE blanchet@43705: | SOME T => do_bound_type T)), blanchet@43705: (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd)) blanchet@43705: (map_filter blanchet@43705: (fn (_, NONE) => NONE blanchet@43705: | (s, SOME T) => blanchet@43747: do_out_of_bound_type pos phi universal (s, T)) blanchet@43747: xs) blanchet@43705: phi) blanchet@43705: end blanchet@43747: | do_formula pos (AConn conn) = aconn_map pos do_formula conn blanchet@44232: | do_formula pos (AAtom tm) = AAtom (do_term pos tm) blanchet@44364: in do_formula end blanchet@43444: blanchet@44493: fun bound_tvars type_enc Ts = blanchet@43592: mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal) blanchet@44493: (type_literals_for_types type_enc add_sorts_on_tvar Ts)) blanchet@43592: blanchet@43444: (* Each fact is given a unique fact number to avoid name clashes (e.g., because blanchet@43444: of monomorphization). The TPTP explicitly forbids name clashes, and some of blanchet@43444: the remote provers might care. *) blanchet@44372: fun formula_line_for_fact ctxt format prefix encode freshen pos nonmono_Ts blanchet@44493: type_enc (j, {name, locality, kind, combformula, atomic_types}) = blanchet@44372: (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, blanchet@44364: kind, blanchet@44364: combformula blanchet@44364: |> close_combformula_universally blanchet@44493: |> formula_from_combformula ctxt format nonmono_Ts type_enc blanchet@44364: should_predicate_on_var_in_formula blanchet@44372: (if pos then SOME true else NONE) blanchet@44493: |> bound_tvars type_enc atomic_types blanchet@44364: |> close_formula_universally, blanchet@44364: NONE, blanchet@44364: case locality of blanchet@44364: Intro => intro_info blanchet@44364: | Elim => elim_info blanchet@44364: | Simp => simp_info blanchet@44364: | _ => NONE) blanchet@44364: |> Formula blanchet@43444: blanchet@43927: fun formula_line_for_class_rel_clause ({name, subclass, superclass, ...} blanchet@43927: : class_rel_clause) = blanchet@43444: let val ty_arg = ATerm (`I "T", []) in blanchet@43448: Formula (class_rel_clause_prefix ^ ascii_of name, Axiom, blanchet@43444: AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), blanchet@43444: AAtom (ATerm (superclass, [ty_arg]))]) blanchet@43748: |> close_formula_universally, intro_info, NONE) blanchet@43444: end blanchet@43444: blanchet@43444: fun fo_literal_from_arity_literal (TConsLit (c, t, args)) = blanchet@43444: (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)])) blanchet@43444: | fo_literal_from_arity_literal (TVarLit (c, sort)) = blanchet@43444: (false, ATerm (c, [ATerm (sort, [])])) blanchet@43444: blanchet@43927: fun formula_line_for_arity_clause ({name, prem_lits, concl_lits, ...} blanchet@43927: : arity_clause) = blanchet@44366: Formula (arity_clause_prefix ^ name, Axiom, blanchet@43444: mk_ahorn (map (formula_from_fo_literal o apfst not blanchet@43766: o fo_literal_from_arity_literal) prem_lits) blanchet@43444: (formula_from_fo_literal blanchet@43766: (fo_literal_from_arity_literal concl_lits)) blanchet@43748: |> close_formula_universally, intro_info, NONE) blanchet@43444: blanchet@44493: fun formula_line_for_conjecture ctxt format nonmono_Ts type_enc blanchet@43939: ({name, kind, combformula, atomic_types, ...} : translated_formula) = blanchet@43448: Formula (conjecture_prefix ^ name, kind, blanchet@44493: formula_from_combformula ctxt format nonmono_Ts type_enc blanchet@44364: should_predicate_on_var_in_formula (SOME false) blanchet@43780: (close_combformula_universally combformula) blanchet@44493: |> bound_tvars type_enc atomic_types blanchet@43444: |> close_formula_universally, NONE, NONE) blanchet@43444: blanchet@44493: fun free_type_literals type_enc ({atomic_types, ...} : translated_formula) = blanchet@44493: atomic_types |> type_literals_for_types type_enc add_sorts_on_tfree blanchet@43444: |> map fo_literal_from_type_literal blanchet@43444: blanchet@43444: fun formula_line_for_free_type j lit = blanchet@43926: Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, blanchet@43444: formula_from_fo_literal lit, NONE, NONE) blanchet@44493: fun formula_lines_for_free_types type_enc facts = blanchet@43444: let blanchet@44493: val litss = map (free_type_literals type_enc) facts blanchet@43444: val lits = fold (union (op =)) litss [] blanchet@43444: in map2 formula_line_for_free_type (0 upto length lits - 1) lits end blanchet@43444: blanchet@43444: (** Symbol declarations **) blanchet@43415: blanchet@44493: fun should_declare_sym type_enc pred_sym s = blanchet@43839: is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso blanchet@44493: (case type_enc of blanchet@43765: Simple_Types _ => true blanchet@43969: | Tags (_, _, Lightweight) => true blanchet@43765: | _ => not pred_sym) blanchet@43413: blanchet@44493: fun sym_decl_table_for_facts ctxt type_enc repaired_sym_tab (conjs, facts) = blanchet@43445: let blanchet@43568: fun add_combterm in_conj tm = blanchet@43445: let val (head, args) = strip_combterm_comb tm in blanchet@43445: (case head of blanchet@43445: CombConst ((s, s'), T, T_args) => blanchet@43445: let val pred_sym = is_pred_sym repaired_sym_tab s in blanchet@44493: if should_declare_sym type_enc pred_sym s then blanchet@43447: Symtab.map_default (s, []) blanchet@43755: (insert_type ctxt #3 (s', T_args, T, pred_sym, length args, blanchet@43755: in_conj)) blanchet@43445: else blanchet@43445: I blanchet@43445: end nik@44537: | CombAbs (_, tm) => add_combterm in_conj tm blanchet@43445: | _ => I) blanchet@43568: #> fold (add_combterm in_conj) args blanchet@43445: end blanchet@43568: fun add_fact in_conj = blanchet@43705: fact_lift (formula_fold NONE (K (add_combterm in_conj))) blanchet@43568: in blanchet@43568: Symtab.empty blanchet@44493: |> is_type_enc_fairly_sound type_enc blanchet@43568: ? (fold (add_fact true) conjs #> fold (add_fact false) facts) blanchet@43568: end blanchet@43445: blanchet@43555: (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it blanchet@43555: out with monotonicity" paper presented at CADE 2011. *) blanchet@44434: fun add_combterm_nonmonotonic_types _ _ _ _ (SOME false) _ = I blanchet@44434: | add_combterm_nonmonotonic_types ctxt level sound locality _ blanchet@44020: (CombApp (CombApp (CombConst ((s, _), Type (_, [T, _]), _), tm1), blanchet@44020: tm2)) = blanchet@43841: (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso blanchet@43700: (case level of blanchet@44233: Noninf_Nonmono_Types => blanchet@44151: not (is_locality_global locality) orelse blanchet@44434: not (is_type_surely_infinite ctxt sound T) blanchet@44434: | Fin_Nonmono_Types => is_type_surely_finite ctxt false T blanchet@43755: | _ => true)) ? insert_type ctxt I (deep_freeze_type T) blanchet@44434: | add_combterm_nonmonotonic_types _ _ _ _ _ _ = I blanchet@44434: fun add_fact_nonmonotonic_types ctxt level sound blanchet@44434: ({kind, locality, combformula, ...} : translated_formula) = blanchet@43705: formula_fold (SOME (kind <> Conjecture)) blanchet@44434: (add_combterm_nonmonotonic_types ctxt level sound locality) blanchet@44434: combformula blanchet@44493: fun nonmonotonic_types_for_facts ctxt type_enc sound facts = blanchet@44493: let val level = level_of_type_enc type_enc in blanchet@44233: if level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types then blanchet@44434: [] |> fold (add_fact_nonmonotonic_types ctxt level sound) facts blanchet@43755: (* We must add "bool" in case the helper "True_or_False" is added blanchet@43755: later. In addition, several places in the code rely on the list of blanchet@43755: nonmonotonic types not being empty. *) blanchet@43755: |> insert_type ctxt I @{typ bool} blanchet@43755: else blanchet@43755: [] blanchet@43700: end blanchet@43547: blanchet@44493: fun decl_line_for_sym ctxt format nonmono_Ts type_enc s blanchet@43835: (s', T_args, T, pred_sym, ary, _) = blanchet@43835: let blanchet@44019: val (T_arg_Ts, level) = blanchet@44493: case type_enc of blanchet@44491: Simple_Types (_, level) => ([], level) blanchet@44019: | _ => (replicate (length T_args) homo_infinite_type, No_Types) blanchet@43835: in blanchet@43839: Decl (sym_decl_prefix ^ s, (s, s'), blanchet@43835: (T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary)) nik@44536: |> ho_type_from_typ format type_enc pred_sym (length T_arg_Ts + ary)) blanchet@43835: end blanchet@43450: blanchet@43966: fun formula_line_for_preds_sym_decl ctxt format conj_sym_kind nonmono_Ts blanchet@44493: poly_nonmono_Ts type_enc n s j (s', T_args, T, _, ary, in_conj) = blanchet@43450: let blanchet@43580: val (kind, maybe_negate) = blanchet@43580: if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot) blanchet@43580: else (Axiom, I) blanchet@43618: val (arg_Ts, res_T) = chop_fun ary T blanchet@44262: val num_args = length arg_Ts blanchet@43450: val bound_names = blanchet@44262: 1 upto num_args |> map (`I o make_bound_var o string_of_int) blanchet@43700: val bounds = blanchet@43450: bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, [])) blanchet@44264: val sym_needs_arg_types = n > 1 orelse exists (curry (op =) dummyT) T_args blanchet@44264: fun should_keep_arg_type T = blanchet@44264: sym_needs_arg_types orelse blanchet@44493: not (should_predicate_on_type ctxt nonmono_Ts type_enc (K false) T) blanchet@43450: val bound_Ts = blanchet@44264: arg_Ts |> map (fn T => if should_keep_arg_type T then SOME T else NONE) blanchet@43450: in blanchet@43966: Formula (preds_sym_formula_prefix ^ s ^ blanchet@43580: (if n > 1 then "_" ^ string_of_int j else ""), kind, blanchet@43450: CombConst ((s, s'), T, T_args) blanchet@43700: |> fold (curry (CombApp o swap)) bounds blanchet@44493: |> type_pred_combterm ctxt format type_enc res_T blanchet@43804: |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts) blanchet@44493: |> formula_from_combformula ctxt format poly_nonmono_Ts type_enc blanchet@44364: (K (K (K (K true)))) (SOME true) blanchet@44493: |> n > 1 ? bound_tvars type_enc (atyps_of T) blanchet@43580: |> close_formula_universally blanchet@43580: |> maybe_negate, blanchet@43748: intro_info, NONE) blanchet@43450: end blanchet@43450: blanchet@43970: fun formula_lines_for_lightweight_tags_sym_decl ctxt format conj_sym_kind blanchet@44493: poly_nonmono_Ts type_enc n s blanchet@44264: (j, (s', T_args, T, pred_sym, ary, in_conj)) = blanchet@43700: let blanchet@43700: val ident_base = blanchet@43970: lightweight_tags_sym_formula_prefix ^ s ^ blanchet@43966: (if n > 1 then "_" ^ string_of_int j else "") blanchet@43721: val (kind, maybe_negate) = blanchet@43721: if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot) blanchet@43721: else (Axiom, I) blanchet@43700: val (arg_Ts, res_T) = chop_fun ary T blanchet@43700: val bound_names = blanchet@43700: 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int) blanchet@43700: val bounds = bound_names |> map (fn name => ATerm (name, [])) nik@44536: val cst = mk_aterm format type_enc (s, s') T_args blanchet@43701: val atomic_Ts = atyps_of T blanchet@43705: fun eq tms = blanchet@43705: (if pred_sym then AConn (AIff, map AAtom tms) blanchet@43841: else AAtom (ATerm (`I tptp_equal, tms))) blanchet@44493: |> bound_tvars type_enc atomic_Ts blanchet@43701: |> close_formula_universally blanchet@43721: |> maybe_negate blanchet@44232: (* See also "should_tag_with_type". *) blanchet@44232: fun should_encode T = blanchet@44264: should_encode_type ctxt poly_nonmono_Ts All_Types T orelse blanchet@44493: (case type_enc of blanchet@44232: Tags (Polymorphic, level, Lightweight) => blanchet@44232: level <> All_Types andalso Monomorph.typ_has_tvars T blanchet@44232: | _ => false) blanchet@44493: val tag_with = tag_with_type ctxt format poly_nonmono_Ts type_enc NONE blanchet@43700: val add_formula_for_res = blanchet@43700: if should_encode res_T then blanchet@43721: cons (Formula (ident_base ^ "_res", kind, blanchet@43835: eq [tag_with res_T (cst bounds), cst bounds], blanchet@43748: simp_info, NONE)) blanchet@43700: else blanchet@43700: I blanchet@43700: fun add_formula_for_arg k = blanchet@43700: let val arg_T = nth arg_Ts k in blanchet@43700: if should_encode arg_T then blanchet@43700: case chop k bounds of blanchet@43700: (bounds1, bound :: bounds2) => blanchet@43721: cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind, blanchet@43835: eq [cst (bounds1 @ tag_with arg_T bound :: bounds2), blanchet@43835: cst bounds], blanchet@43748: simp_info, NONE)) blanchet@43700: | _ => raise Fail "expected nonempty tail" blanchet@43700: else blanchet@43700: I blanchet@43700: end blanchet@43700: in blanchet@43705: [] |> not pred_sym ? add_formula_for_res blanchet@43700: |> fold add_formula_for_arg (ary - 1 downto 0) blanchet@43700: end blanchet@43700: blanchet@43707: fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd blanchet@43707: blanchet@44264: fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts blanchet@44493: poly_nonmono_Ts type_enc (s, decls) = blanchet@44493: case type_enc of blanchet@43839: Simple_Types _ => blanchet@44493: decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_enc s) blanchet@43839: | Preds _ => blanchet@43839: let blanchet@43839: val decls = blanchet@43839: case decls of blanchet@43839: decl :: (decls' as _ :: _) => blanchet@43839: let val T = result_type_of_decl decl in blanchet@43839: if forall (curry (type_instance ctxt o swap) T blanchet@43839: o result_type_of_decl) decls' then blanchet@43839: [decl] blanchet@43839: else blanchet@43839: decls blanchet@43839: end blanchet@43839: | _ => decls blanchet@43839: val n = length decls blanchet@43839: val decls = blanchet@44493: decls |> filter (should_predicate_on_type ctxt poly_nonmono_Ts type_enc blanchet@44264: (K true) blanchet@44264: o result_type_of_decl) blanchet@43839: in blanchet@43839: (0 upto length decls - 1, decls) blanchet@43966: |-> map2 (formula_line_for_preds_sym_decl ctxt format conj_sym_kind blanchet@44493: nonmono_Ts poly_nonmono_Ts type_enc n s) blanchet@43839: end blanchet@43839: | Tags (_, _, heaviness) => blanchet@43839: (case heaviness of blanchet@43969: Heavyweight => [] blanchet@43969: | Lightweight => blanchet@43839: let val n = length decls in blanchet@43839: (0 upto n - 1 ~~ decls) blanchet@43970: |> maps (formula_lines_for_lightweight_tags_sym_decl ctxt format blanchet@44493: conj_sym_kind poly_nonmono_Ts type_enc n s) blanchet@43839: end) blanchet@43450: blanchet@43797: fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts blanchet@44493: poly_nonmono_Ts type_enc sym_decl_tab = blanchet@43839: sym_decl_tab blanchet@43839: |> Symtab.dest blanchet@43839: |> sort_wrt fst blanchet@43839: |> rpair [] blanchet@43839: |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind blanchet@44493: nonmono_Ts poly_nonmono_Ts type_enc) blanchet@43414: blanchet@44026: fun needs_type_tag_idempotence (Tags (poly, level, heaviness)) = blanchet@44026: poly <> Mangled_Monomorphic andalso blanchet@44026: ((level = All_Types andalso heaviness = Lightweight) orelse blanchet@44233: level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types) blanchet@44000: | needs_type_tag_idempotence _ = false blanchet@43702: blanchet@43780: fun offset_of_heading_in_problem _ [] j = j blanchet@43780: | offset_of_heading_in_problem needle ((heading, lines) :: problem) j = blanchet@43780: if heading = needle then j blanchet@43780: else offset_of_heading_in_problem needle problem (j + length lines) blanchet@43780: blanchet@43839: val implicit_declsN = "Should-be-implicit typings" blanchet@43839: val explicit_declsN = "Explicit typings" blanchet@41405: val factsN = "Relevant facts" blanchet@41405: val class_relsN = "Class relationships" blanchet@43414: val aritiesN = "Arities" blanchet@41405: val helpersN = "Helper facts" blanchet@41405: val conjsN = "Conjectures" blanchet@41561: val free_typesN = "Type variables" blanchet@41405: blanchet@44100: val explicit_apply = NONE (* for experimental purposes *) blanchet@44100: blanchet@44493: fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc sound blanchet@44364: exporter readable_names preproc hyp_ts concl_t facts = blanchet@38506: let blanchet@44493: val (format, type_enc) = choose_format [format] type_enc blanchet@41561: val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) = blanchet@44493: translate_formulas ctxt format prem_kind type_enc preproc hyp_ts concl_t blanchet@43937: facts blanchet@43905: val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply blanchet@44434: val nonmono_Ts = blanchet@44493: conjs @ facts |> nonmonotonic_types_for_facts ctxt type_enc sound blanchet@44493: val repair = repair_fact ctxt format type_enc sym_tab blanchet@43552: val (conjs, facts) = (conjs, facts) |> pairself (map repair) blanchet@43905: val repaired_sym_tab = blanchet@43905: conjs @ facts |> sym_table_for_facts ctxt (SOME false) blanchet@43444: val helpers = blanchet@44493: repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc blanchet@43803: |> map repair blanchet@44264: val poly_nonmono_Ts = blanchet@44054: if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse blanchet@44493: polymorphism_of_type_enc type_enc <> Polymorphic then blanchet@43765: nonmono_Ts blanchet@43765: else blanchet@43765: [TVar (("'a", 0), HOLogic.typeS)] blanchet@43550: val sym_decl_lines = blanchet@43596: (conjs, helpers @ facts) blanchet@44493: |> sym_decl_table_for_facts ctxt type_enc repaired_sym_tab blanchet@44264: |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts blanchet@44493: poly_nonmono_Ts type_enc blanchet@43750: val helper_lines = blanchet@43797: 0 upto length helpers - 1 ~~ helpers blanchet@44372: |> map (formula_line_for_fact ctxt format helper_prefix I false true blanchet@44493: poly_nonmono_Ts type_enc) blanchet@44493: |> (if needs_type_tag_idempotence type_enc then blanchet@44000: cons (type_tag_idempotence_fact ()) blanchet@44000: else blanchet@44000: I) blanchet@43393: (* Reordering these might confuse the proof reconstruction code or the SPASS blanchet@43880: FLOTTER hack. *) blanchet@38506: val problem = blanchet@43839: [(explicit_declsN, sym_decl_lines), blanchet@43797: (factsN, blanchet@44372: map (formula_line_for_fact ctxt format fact_prefix ascii_of blanchet@44372: (not exporter) (not exporter) nonmono_Ts blanchet@44493: type_enc) blanchet@43797: (0 upto length facts - 1 ~~ facts)), blanchet@43416: (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses), blanchet@43416: (aritiesN, map formula_line_for_arity_clause arity_clauses), blanchet@43750: (helpersN, helper_lines), blanchet@43803: (conjsN, blanchet@44493: map (formula_line_for_conjecture ctxt format nonmono_Ts type_enc) blanchet@43803: conjs), blanchet@44493: (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs))] blanchet@43414: val problem = blanchet@43432: problem blanchet@43933: |> (case format of blanchet@43933: CNF => ensure_cnf_problem blanchet@43933: | CNF_UEQ => filter_cnf_ueq_problem blanchet@43933: | _ => I) blanchet@43839: |> (if is_format_typed format then blanchet@43839: declare_undeclared_syms_in_atp_problem type_decl_prefix blanchet@43839: implicit_declsN blanchet@43839: else blanchet@43839: I) blanchet@43933: val (problem, pool) = problem |> nice_atp_problem readable_names blanchet@43750: val helpers_offset = offset_of_heading_in_problem helpersN problem 0 blanchet@43750: val typed_helpers = blanchet@43750: map_filter (fn (j, {name, ...}) => blanchet@43750: if String.isSuffix typed_helper_suffix name then SOME j blanchet@43750: else NONE) blanchet@43750: ((helpers_offset + 1 upto helpers_offset + length helpers) blanchet@43750: ~~ helpers) blanchet@43649: fun add_sym_arity (s, {min_ary, ...} : sym_info) = blanchet@43620: if min_ary > 0 then blanchet@43620: case strip_prefix_and_unascii const_prefix s of blanchet@43620: SOME s => Symtab.insert (op =) (s, min_ary) blanchet@43620: | NONE => I blanchet@43620: else blanchet@43620: I blanchet@38506: in blanchet@38506: (problem, blanchet@38506: case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty, blanchet@43456: offset_of_heading_in_problem conjsN problem 0, blanchet@43412: offset_of_heading_in_problem factsN problem 0, blanchet@43620: fact_names |> Vector.fromList, blanchet@43750: typed_helpers, blanchet@43620: Symtab.empty |> Symtab.fold add_sym_arity sym_tab) blanchet@38506: end blanchet@38506: blanchet@41561: (* FUDGE *) blanchet@41561: val conj_weight = 0.0 blanchet@42641: val hyp_weight = 0.1 blanchet@42641: val fact_min_weight = 0.2 blanchet@41561: val fact_max_weight = 1.0 blanchet@43479: val type_info_default_weight = 0.8 blanchet@41561: blanchet@41561: fun add_term_weights weight (ATerm (s, tms)) = nik@44535: is_tptp_user_symbol s ? Symtab.default (s, weight) nik@44535: #> fold (add_term_weights weight) tms nik@44535: | add_term_weights weight (AAbs (_, tm)) = add_term_weights weight tm blanchet@43448: fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) = blanchet@43705: formula_fold NONE (K (add_term_weights weight)) phi blanchet@43399: | add_problem_line_weights _ _ = I blanchet@41561: blanchet@41561: fun add_conjectures_weights [] = I blanchet@41561: | add_conjectures_weights conjs = blanchet@41561: let val (hyps, conj) = split_last conjs in blanchet@41561: add_problem_line_weights conj_weight conj blanchet@41561: #> fold (add_problem_line_weights hyp_weight) hyps blanchet@41561: end blanchet@41561: blanchet@41561: fun add_facts_weights facts = blanchet@41561: let blanchet@41561: val num_facts = length facts blanchet@41561: fun weight_of j = blanchet@41561: fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j blanchet@41561: / Real.fromInt num_facts blanchet@41561: in blanchet@41561: map weight_of (0 upto num_facts - 1) ~~ facts blanchet@41561: |> fold (uncurry add_problem_line_weights) blanchet@41561: end blanchet@41561: blanchet@41561: (* Weights are from 0.0 (most important) to 1.0 (least important). *) blanchet@41561: fun atp_problem_weights problem = blanchet@43479: let val get = these o AList.lookup (op =) problem in blanchet@43479: Symtab.empty blanchet@43479: |> add_conjectures_weights (get free_typesN @ get conjsN) blanchet@43479: |> add_facts_weights (get factsN) blanchet@43479: |> fold (fold (add_problem_line_weights type_info_default_weight) o get) blanchet@43839: [explicit_declsN, class_relsN, aritiesN] blanchet@43479: |> Symtab.dest blanchet@43479: |> sort (prod_ord Real.compare string_ord o pairself swap) blanchet@43479: end blanchet@41561: blanchet@38506: end;