wneuper/isa: src/HOL/Tools/ATP/atp_translate.ML@4dce7f2bb59f

     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML

     2     Author:     Fabian Immler, TU Muenchen

     3     Author:     Makarius

     4     Author:     Jasmin Blanchette, TU Muenchen

     6 Translation of HOL to FOL for Sledgehammer.

     7 *)

     9 signature ATP_TRANSLATE =

    10 sig

    11   type 'a fo_term = 'a ATP_Problem.fo_term

    12   type format = ATP_Problem.format

    13   type formula_kind = ATP_Problem.formula_kind

    14   type 'a problem = 'a ATP_Problem.problem

    16   type name = string * string

    18   datatype type_literal =

    19     TyLitVar of name * name |

    20     TyLitFree of name * name

    22   datatype arity_literal =

    23     TConsLit of name * name * name list |

    24     TVarLit of name * name

    26   type arity_clause =

    27     {name: string,

    28      prem_lits: arity_literal list,

    29      concl_lits: arity_literal}

    31   type class_rel_clause =

    32     {name: string,

    33      subclass: name,

    34      superclass: name}

    36   datatype combterm =

    37     CombConst of name * typ * typ list |

    38     CombVar of name * typ |

    39     CombApp of combterm * combterm

    41   datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained

    43   datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic

    44   datatype type_level =

    45     All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types

    46   datatype type_heaviness = Heavy | Light

    48   datatype type_system =

    49     Simple_Types of type_level |

    50     Preds of polymorphism * type_level * type_heaviness |

    51     Tags of polymorphism * type_level * type_heaviness

    53   type translated_formula

    55   val readable_names : bool Config.T

    56   val type_tag_name : string

    57   val bound_var_prefix : string

    58   val schematic_var_prefix: string

    59   val fixed_var_prefix: string

    60   val tvar_prefix: string

    61   val tfree_prefix: string

    62   val const_prefix: string

    63   val type_const_prefix: string

    64   val class_prefix: string

    65   val skolem_const_prefix : string

    66   val old_skolem_const_prefix : string

    67   val new_skolem_const_prefix : string

    68   val fact_prefix : string

    69   val conjecture_prefix : string

    70   val helper_prefix : string

    71   val typed_helper_suffix : string

    72   val predicator_name : string

    73   val app_op_name : string

    74   val type_pred_name : string

    75   val simple_type_prefix : string

    76   val ascii_of: string -> string

    77   val unascii_of: string -> string

    78   val strip_prefix_and_unascii : string -> string -> string option

    79   val proxify_const : string -> (int * (string * string)) option

    80   val invert_const: string -> string

    81   val unproxify_const: string -> string

    82   val make_bound_var : string -> string

    83   val make_schematic_var : string * int -> string

    84   val make_fixed_var : string -> string

    85   val make_schematic_type_var : string * int -> string

    86   val make_fixed_type_var : string -> string

    87   val make_fixed_const : string -> string

    88   val make_fixed_type_const : string -> string

    89   val make_type_class : string -> string

    90   val make_arity_clauses :

    91     theory -> string list -> class list -> class list * arity_clause list

    92   val make_class_rel_clauses :

    93     theory -> class list -> class list -> class_rel_clause list

    94   val combtyp_of : combterm -> typ

    95   val strip_combterm_comb : combterm -> combterm * combterm list

    96   val atyps_of : typ -> typ list

    97   val combterm_from_term :

    98     theory -> (string * typ) list -> term -> combterm * typ list

    99   val is_locality_global : locality -> bool

   100   val type_sys_from_string : string -> type_system

   101   val polymorphism_of_type_sys : type_system -> polymorphism

   102   val level_of_type_sys : type_system -> type_level

   103   val is_type_sys_virtually_sound : type_system -> bool

   104   val is_type_sys_fairly_sound : type_system -> bool

   105   val raw_type_literals_for_types : typ list -> type_literal list

   106   val unmangled_const : string -> string * string fo_term list

   107   val translate_atp_fact :

   108     Proof.context -> format -> type_system -> bool -> (string * locality) * thm

   109     -> translated_formula option * ((string * locality) * thm)

   110   val helper_table : (string * (bool * thm list)) list

   111   val tfree_classes_of_terms : term list -> string list

   112   val tvar_classes_of_terms : term list -> string list

   113   val type_consts_of_terms : theory -> term list -> string list

   114   val prepare_atp_problem :

   115     Proof.context -> format -> formula_kind -> formula_kind -> type_system

   116     -> bool option -> term list -> term

   117     -> (translated_formula option * ((string * 'a) * thm)) list

   118     -> string problem * string Symtab.table * int * int

   119        * (string * 'a) list vector * int list * int Symtab.table

   120   val atp_problem_weights : string problem -> (string * real) list

   121 end;

   123 structure ATP_Translate : ATP_TRANSLATE =

   124 struct

   126 open ATP_Util

   127 open ATP_Problem

   129 type name = string * string

   131 (* FIXME: avoid *)

   132 fun union_all xss = fold (union (op =)) xss []

   134 (* experimental *)

   135 val generate_useful_info = false

   137 fun useful_isabelle_info s =

   138   if generate_useful_info then

   139     SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))

   140   else

   141     NONE

   143 val intro_info = useful_isabelle_info "intro"

   144 val elim_info = useful_isabelle_info "elim"

   145 val simp_info = useful_isabelle_info "simp"

   147 (* Readable names are often much shorter, especially if types are mangled in

   148    names. Also, the logic for generating legal SNARK sort names is only

   149    implemented for readable names. Finally, readable names are, well, more

   150    readable. For these reason, they are enabled by default. *)

   151 val readable_names =

   152   Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true)

   154 val type_tag_name = "ti"

   156 val bound_var_prefix = "B_"

   157 val schematic_var_prefix = "V_"

   158 val fixed_var_prefix = "v_"

   160 val tvar_prefix = "T_"

   161 val tfree_prefix = "t_"

   163 val const_prefix = "c_"

   164 val type_const_prefix = "tc_"

   165 val class_prefix = "cl_"

   167 val skolem_const_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko"

   168 val old_skolem_const_prefix = skolem_const_prefix ^ "o"

   169 val new_skolem_const_prefix = skolem_const_prefix ^ "n"

   171 val type_decl_prefix = "ty_"

   172 val sym_decl_prefix = "sy_"

   173 val sym_formula_prefix = "sym_"

   174 val fact_prefix = "fact_"

   175 val conjecture_prefix = "conj_"

   176 val helper_prefix = "help_"

   177 val class_rel_clause_prefix = "crel_";

   178 val arity_clause_prefix = "arity_"

   179 val tfree_clause_prefix = "tfree_"

   181 val typed_helper_suffix = "_T"

   182 val untyped_helper_suffix = "_U"

   184 val predicator_name = "hBOOL"

   185 val app_op_name = "hAPP"

   186 val type_pred_name = "is"

   187 val simple_type_prefix = "ty_"

   189 (* Freshness almost guaranteed! *)

   190 val sledgehammer_weak_prefix = "Sledgehammer:"

   192 (*Escaping of special characters.

   193   Alphanumeric characters are left unchanged.

   194   The character _ goes to __

   195   Characters in the range ASCII space to / go to _A to _P, respectively.

   196   Other characters go to _nnn where nnn is the decimal ASCII code.*)

   197 val upper_a_minus_space = Char.ord #"A" - Char.ord #" ";

   199 fun stringN_of_int 0 _ = ""

   200   | stringN_of_int k n =

   201     stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)

   203 fun ascii_of_char c =

   204   if Char.isAlphaNum c then

   205     String.str c

   206   else if c = #"_" then

   207     "__"

   208   else if #" " <= c andalso c <= #"/" then

   209     "_" ^ String.str (Char.chr (Char.ord c + upper_a_minus_space))

   210   else

   211     (* fixed width, in case more digits follow *)

   212     "_" ^ stringN_of_int 3 (Char.ord c)

   214 val ascii_of = String.translate ascii_of_char

   216 (** Remove ASCII armoring from names in proof files **)

   218 (* We don't raise error exceptions because this code can run inside a worker

   219    thread. Also, the errors are impossible. *)

   220 val unascii_of =

   221   let

   222     fun un rcs [] = String.implode(rev rcs)

   223       | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *)

   224         (* Three types of _ escapes: __, _A to _P, _nnn *)

   225       | un rcs (#"_" :: #"_" :: cs) = un (#"_"::rcs) cs

   226       | un rcs (#"_" :: c :: cs) =

   227         if #"A" <= c andalso c<= #"P" then

   228           (* translation of #" " to #"/" *)

   229           un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs

   230         else

   231           let val digits = List.take (c::cs, 3) handle Subscript => [] in

   232             case Int.fromString (String.implode digits) of

   233               SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))

   234             | NONE => un (c:: #"_"::rcs) cs (* ERROR *)

   235           end

   236       | un rcs (c :: cs) = un (c :: rcs) cs

   237   in un [] o String.explode end

   239 (* If string s has the prefix s1, return the result of deleting it,

   240    un-ASCII'd. *)

   241 fun strip_prefix_and_unascii s1 s =

   242   if String.isPrefix s1 s then

   243     SOME (unascii_of (String.extract (s, size s1, NONE)))

   244   else

   245     NONE

   247 val proxies =

   248   [("c_False",

   249     (@{const_name False}, (0, ("fFalse", @{const_name ATP.fFalse})))),

   250    ("c_True", (@{const_name True}, (0, ("fTrue", @{const_name ATP.fTrue})))),

   251    ("c_Not", (@{const_name Not}, (1, ("fNot", @{const_name ATP.fNot})))),

   252    ("c_conj", (@{const_name conj}, (2, ("fconj", @{const_name ATP.fconj})))),

   253    ("c_disj", (@{const_name disj}, (2, ("fdisj", @{const_name ATP.fdisj})))),

   254    ("c_implies",

   255     (@{const_name implies}, (2, ("fimplies", @{const_name ATP.fimplies})))),

   256    ("equal",

   257     (@{const_name HOL.eq}, (2, ("fequal", @{const_name ATP.fequal}))))]

   259 val proxify_const = AList.lookup (op =) proxies #> Option.map snd

   261 (* Readable names for the more common symbolic functions. Do not mess with the

   262    table unless you know what you are doing. *)

   263 val const_trans_table =

   264   [(@{type_name Product_Type.prod}, "prod"),

   265    (@{type_name Sum_Type.sum}, "sum"),

   266    (@{const_name False}, "False"),

   267    (@{const_name True}, "True"),

   268    (@{const_name Not}, "Not"),

   269    (@{const_name conj}, "conj"),

   270    (@{const_name disj}, "disj"),

   271    (@{const_name implies}, "implies"),

   272    (@{const_name HOL.eq}, "equal"),

   273    (@{const_name If}, "If"),

   274    (@{const_name Set.member}, "member"),

   275    (@{const_name Meson.COMBI}, "COMBI"),

   276    (@{const_name Meson.COMBK}, "COMBK"),

   277    (@{const_name Meson.COMBB}, "COMBB"),

   278    (@{const_name Meson.COMBC}, "COMBC"),

   279    (@{const_name Meson.COMBS}, "COMBS")]

   280   |> Symtab.make

   281   |> fold (Symtab.update o swap o snd o snd o snd) proxies

   283 (* Invert the table of translations between Isabelle and ATPs. *)

   284 val const_trans_table_inv =

   285   const_trans_table |> Symtab.dest |> map swap |> Symtab.make

   286 val const_trans_table_unprox =

   287   Symtab.empty

   288   |> fold (fn (_, (isa, (_, (_, metis)))) => Symtab.update (metis, isa)) proxies

   290 val invert_const = perhaps (Symtab.lookup const_trans_table_inv)

   291 val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)

   293 fun lookup_const c =

   294   case Symtab.lookup const_trans_table c of

   295     SOME c' => c'

   296   | NONE => ascii_of c

   298 (*Remove the initial ' character from a type variable, if it is present*)

   299 fun trim_type_var s =

   300   if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)

   301   else raise Fail ("trim_type: Malformed type variable encountered: " ^ s)

   303 fun ascii_of_indexname (v,0) = ascii_of v

   304   | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ string_of_int i

   306 fun make_bound_var x = bound_var_prefix ^ ascii_of x

   307 fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v

   308 fun make_fixed_var x = fixed_var_prefix ^ ascii_of x

   310 fun make_schematic_type_var (x,i) =

   311       tvar_prefix ^ (ascii_of_indexname (trim_type_var x, i))

   312 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x))

   314 (* HOL.eq MUST BE "equal" because it's built into ATPs. *)

   315 fun make_fixed_const @{const_name HOL.eq} = "equal"

   316   | make_fixed_const c = const_prefix ^ lookup_const c

   318 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c

   320 fun make_type_class clas = class_prefix ^ ascii_of clas

   322 (** Definitions and functions for FOL clauses and formulas for TPTP **)

   324 (* The first component is the type class; the second is a "TVar" or "TFree". *)

   325 datatype type_literal =

   326   TyLitVar of name * name |

   327   TyLitFree of name * name

   330 (** Isabelle arities **)

   332 datatype arity_literal =

   333   TConsLit of name * name * name list |

   334   TVarLit of name * name

   336 fun gen_TVars 0 = []

   337   | gen_TVars n = ("T_" ^ string_of_int n) :: gen_TVars (n-1);

   339 fun pack_sort (_,[])  = []

   340   | pack_sort (tvar, "HOL.type" :: srt) =

   341     pack_sort (tvar, srt) (* IGNORE sort "type" *)

   342   | pack_sort (tvar, cls :: srt) =

   343     (`make_type_class cls, `I tvar) :: pack_sort (tvar, srt)

   345 type arity_clause =

   346   {name: string,

   347    prem_lits: arity_literal list,

   348    concl_lits: arity_literal}

   350 (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)

   351 fun make_axiom_arity_clause (tcons, name, (cls, args)) =

   352   let

   353     val tvars = gen_TVars (length args)

   354     val tvars_srts = ListPair.zip (tvars, args)

   355   in

   356     {name = name,

   357      prem_lits = map TVarLit (union_all (map pack_sort tvars_srts)),

   358      concl_lits = TConsLit (`make_type_class cls,

   359                             `make_fixed_type_const tcons,

   360                             tvars ~~ tvars)}

   361   end

   363 fun arity_clause _ _ (_, []) = []

   364   | arity_clause seen n (tcons, ("HOL.type",_)::ars) =  (*ignore*)

   365       arity_clause seen n (tcons,ars)

   366   | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =

   367       if member (op =) seen class then (*multiple arities for the same tycon, class pair*)

   368           make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ string_of_int n, ar) ::

   369           arity_clause seen (n+1) (tcons,ars)

   370       else

   371           make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) ::

   372           arity_clause (class::seen) n (tcons,ars)

   374 fun multi_arity_clause [] = []

   375   | multi_arity_clause ((tcons, ars) :: tc_arlists) =

   376       arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists

   378 (*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy

   379   provided its arguments have the corresponding sorts.*)

   380 fun type_class_pairs thy tycons classes =

   381   let val alg = Sign.classes_of thy

   382       fun domain_sorts tycon = Sorts.mg_domain alg tycon o single

   383       fun add_class tycon class =

   384         cons (class, domain_sorts tycon class)

   385         handle Sorts.CLASS_ERROR _ => I

   386       fun try_classes tycon = (tycon, fold (add_class tycon) classes [])

   387   in  map try_classes tycons  end;

   389 (*Proving one (tycon, class) membership may require proving others, so iterate.*)

   390 fun iter_type_class_pairs _ _ [] = ([], [])

   391   | iter_type_class_pairs thy tycons classes =

   392       let val cpairs = type_class_pairs thy tycons classes

   393           val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))

   394             |> subtract (op =) classes |> subtract (op =) HOLogic.typeS

   395           val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses

   396       in (union (op =) classes' classes, union (op =) cpairs' cpairs) end;

   398 fun make_arity_clauses thy tycons =

   399   iter_type_class_pairs thy tycons ##> multi_arity_clause

   402 (** Isabelle class relations **)

   404 type class_rel_clause =

   405   {name: string,

   406    subclass: name,

   407    superclass: name}

   409 (*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)

   410 fun class_pairs _ [] _ = []

   411   | class_pairs thy subs supers =

   412       let

   413         val class_less = Sorts.class_less (Sign.classes_of thy)

   414         fun add_super sub super = class_less (sub, super) ? cons (sub, super)

   415         fun add_supers sub = fold (add_super sub) supers

   416       in fold add_supers subs [] end

   418 fun make_class_rel_clause (sub,super) =

   419   {name = sub ^ "_" ^ super,

   420    subclass = `make_type_class sub,

   421    superclass = `make_type_class super}

   423 fun make_class_rel_clauses thy subs supers =

   424   map make_class_rel_clause (class_pairs thy subs supers);

   426 datatype combterm =

   427   CombConst of name * typ * typ list |

   428   CombVar of name * typ |

   429   CombApp of combterm * combterm

   431 fun combtyp_of (CombConst (_, T, _)) = T

   432   | combtyp_of (CombVar (_, T)) = T

   433   | combtyp_of (CombApp (t1, _)) = snd (dest_funT (combtyp_of t1))

   435 (*gets the head of a combinator application, along with the list of arguments*)

   436 fun strip_combterm_comb u =

   437     let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)

   438         |   stripc  x =  x

   439     in stripc(u,[]) end

   441 fun atyps_of T = fold_atyps (insert (op =)) T []

   443 fun new_skolem_const_name s num_T_args =

   444   [new_skolem_const_prefix, s, string_of_int num_T_args]

   445   |> space_implode Long_Name.separator

   447 (* Converts a term (with combinators) into a combterm. Also accumulates sort

   448    infomation. *)

   449 fun combterm_from_term thy bs (P $ Q) =

   450     let

   451       val (P', P_atomics_Ts) = combterm_from_term thy bs P

   452       val (Q', Q_atomics_Ts) = combterm_from_term thy bs Q

   453     in (CombApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end

   454   | combterm_from_term thy _ (Const (c, T)) =

   455     let

   456       val tvar_list =

   457         (if String.isPrefix old_skolem_const_prefix c then

   458            [] |> Term.add_tvarsT T |> map TVar

   459          else

   460            (c, T) |> Sign.const_typargs thy)

   461       val c' = CombConst (`make_fixed_const c, T, tvar_list)

   462     in (c', atyps_of T) end

   463   | combterm_from_term _ _ (Free (v, T)) =

   464     (CombConst (`make_fixed_var v, T, []), atyps_of T)

   465   | combterm_from_term _ _ (Var (v as (s, _), T)) =

   466     (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then

   467        let

   468          val Ts = T |> strip_type |> swap |> op ::

   469          val s' = new_skolem_const_name s (length Ts)

   470        in CombConst (`make_fixed_const s', T, Ts) end

   471      else

   472        CombVar ((make_schematic_var v, s), T), atyps_of T)

   473   | combterm_from_term _ bs (Bound j) =

   474     nth bs j

   475     |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T))

   476   | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"

   478 datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained

   480 (* (quasi-)underapproximation of the truth *)

   481 fun is_locality_global Local = false

   482   | is_locality_global Assum = false

   483   | is_locality_global Chained = false

   484   | is_locality_global _ = true

   486 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic

   487 datatype type_level =

   488   All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types

   489 datatype type_heaviness = Heavy | Light

   491 datatype type_system =

   492   Simple_Types of type_level |

   493   Preds of polymorphism * type_level * type_heaviness |

   494   Tags of polymorphism * type_level * type_heaviness

   496 fun try_unsuffixes ss s =

   497   fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE

   499 fun type_sys_from_string s =

   500   (case try (unprefix "poly_") s of

   501      SOME s => (SOME Polymorphic, s)

   502    | NONE =>

   503      case try (unprefix "mono_") s of

   504        SOME s => (SOME Monomorphic, s)

   505      | NONE =>

   506        case try (unprefix "mangled_") s of

   507          SOME s => (SOME Mangled_Monomorphic, s)

   508        | NONE => (NONE, s))

   509   ||> (fn s =>

   510           (* "_query" and "_bang" are for the ASCII-challenged Mirabelle. *)

   511           case try_unsuffixes ["?", "_query"] s of

   512             SOME s => (Nonmonotonic_Types, s)

   513           | NONE =>

   514             case try_unsuffixes ["!", "_bang"] s of

   515               SOME s => (Finite_Types, s)

   516             | NONE => (All_Types, s))

   517   ||> apsnd (fn s =>

   518                 case try (unsuffix "_heavy") s of

   519                   SOME s => (Heavy, s)

   520                 | NONE => (Light, s))

   521   |> (fn (poly, (level, (heaviness, core))) =>

   522          case (core, (poly, level, heaviness)) of

   523            ("simple", (NONE, _, Light)) => Simple_Types level

   524          | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)

   525          | ("tags", (SOME Polymorphic, All_Types, _)) =>

   526            Tags (Polymorphic, All_Types, heaviness)

   527          | ("tags", (SOME Polymorphic, _, _)) =>

   528            (* The actual light encoding is very unsound. *)

   529            Tags (Polymorphic, level, Heavy)

   530          | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)

   531          | ("args", (SOME poly, All_Types (* naja *), Light)) =>

   532            Preds (poly, Const_Arg_Types, Light)

   533          | ("erased", (NONE, All_Types (* naja *), Light)) =>

   534            Preds (Polymorphic, No_Types, Light)

   535          | _ => raise Same.SAME)

   536   handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")

   538 fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic

   539   | polymorphism_of_type_sys (Preds (poly, _, _)) = poly

   540   | polymorphism_of_type_sys (Tags (poly, _, _)) = poly

   542 fun level_of_type_sys (Simple_Types level) = level

   543   | level_of_type_sys (Preds (_, level, _)) = level

   544   | level_of_type_sys (Tags (_, level, _)) = level

   546 fun heaviness_of_type_sys (Simple_Types _) = Heavy

   547   | heaviness_of_type_sys (Preds (_, _, heaviness)) = heaviness

   548   | heaviness_of_type_sys (Tags (_, _, heaviness)) = heaviness

   550 fun is_type_level_virtually_sound level =

   551   level = All_Types orelse level = Nonmonotonic_Types

   552 val is_type_sys_virtually_sound =

   553   is_type_level_virtually_sound o level_of_type_sys

   555 fun is_type_level_fairly_sound level =

   556   is_type_level_virtually_sound level orelse level = Finite_Types

   557 val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys

   559 fun is_setting_higher_order THF (Simple_Types _) = true

   560   | is_setting_higher_order _ _ = false

   562 type translated_formula =

   563   {name: string,

   564    locality: locality,

   565    kind: formula_kind,

   566    combformula: (name, typ, combterm) formula,

   567    atomic_types: typ list}

   569 fun update_combformula f ({name, locality, kind, combformula, atomic_types}

   570                           : translated_formula) =

   571   {name = name, locality = locality, kind = kind, combformula = f combformula,

   572    atomic_types = atomic_types} : translated_formula

   574 fun fact_lift f ({combformula, ...} : translated_formula) = f combformula

   576 val type_instance = Sign.typ_instance o Proof_Context.theory_of

   578 fun insert_type ctxt get_T x xs =

   579   let val T = get_T x in

   580     if exists (curry (type_instance ctxt) T o get_T) xs then xs

   581     else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs

   582   end

   584 (* The Booleans indicate whether all type arguments should be kept. *)

   585 datatype type_arg_policy =

   586   Explicit_Type_Args of bool |

   587   Mangled_Type_Args of bool |

   588   No_Type_Args

   590 fun should_drop_arg_type_args (Simple_Types _) =

   591     false (* since TFF doesn't support overloading *)

   592   | should_drop_arg_type_args type_sys =

   593     level_of_type_sys type_sys = All_Types andalso

   594     heaviness_of_type_sys type_sys = Heavy

   596 fun general_type_arg_policy type_sys =

   597   if level_of_type_sys type_sys = No_Types then

   598     No_Type_Args

   599   else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then

   600     Mangled_Type_Args (should_drop_arg_type_args type_sys)

   601   else

   602     Explicit_Type_Args (should_drop_arg_type_args type_sys)

   604 fun type_arg_policy type_sys s =

   605   if s = @{const_name HOL.eq} orelse

   606      (s = app_op_name andalso level_of_type_sys type_sys = Const_Arg_Types) then

   607     No_Type_Args

   608   else

   609     general_type_arg_policy type_sys

   611 (*Make literals for sorted type variables*)

   612 fun sorts_on_typs_aux (_, [])   = []

   613   | sorts_on_typs_aux ((x,i),  s::ss) =

   614       let val sorts = sorts_on_typs_aux ((x,i), ss)

   615       in

   616           if s = the_single @{sort HOL.type} then sorts

   617           else if i = ~1 then TyLitFree (`make_type_class s, `make_fixed_type_var x) :: sorts

   618           else TyLitVar (`make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts

   619       end;

   621 fun sorts_on_typs (TFree (a, s)) = sorts_on_typs_aux ((a, ~1), s)

   622   | sorts_on_typs (TVar (v, s)) = sorts_on_typs_aux (v, s)

   623   | sorts_on_typs _ = raise Fail "expected \"TVar\" or \"TFree\""

   625 (*Given a list of sorted type variables, return a list of type literals.*)

   626 val raw_type_literals_for_types = union_all o map sorts_on_typs

   628 fun type_literals_for_types format type_sys kind Ts =

   629   if level_of_type_sys type_sys = No_Types orelse format = CNF_UEQ then

   630     []

   631   else

   632     Ts |> raw_type_literals_for_types

   633        |> filter (fn TyLitVar _ => kind <> Conjecture

   634                    | TyLitFree _ => kind = Conjecture)

   636 fun mk_aconns c phis =

   637   let val (phis', phi') = split_last phis in

   638     fold_rev (mk_aconn c) phis' phi'

   639   end

   640 fun mk_ahorn [] phi = phi

   641   | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])

   642 fun mk_aquant _ [] phi = phi

   643   | mk_aquant q xs (phi as AQuant (q', xs', phi')) =

   644     if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)

   645   | mk_aquant q xs phi = AQuant (q, xs, phi)

   647 fun close_universally atom_vars phi =

   648   let

   649     fun formula_vars bounds (AQuant (_, xs, phi)) =

   650         formula_vars (map fst xs @ bounds) phi

   651       | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis

   652       | formula_vars bounds (AAtom tm) =

   653         union (op =) (atom_vars tm []

   654                       |> filter_out (member (op =) bounds o fst))

   655   in mk_aquant AForall (formula_vars [] phi []) phi end

   657 fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2]

   658   | combterm_vars (CombConst _) = I

   659   | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T)

   660 fun close_combformula_universally phi = close_universally combterm_vars phi

   662 fun term_vars (ATerm (name as (s, _), tms)) =

   663   is_tptp_variable s ? insert (op =) (name, NONE) #> fold term_vars tms

   664 fun close_formula_universally phi = close_universally term_vars phi

   666 val homo_infinite_type_name = @{type_name ind} (* any infinite type *)

   667 val homo_infinite_type = Type (homo_infinite_type_name, [])

   669 fun fo_term_from_typ higher_order =

   670   let

   671     fun term (Type (s, Ts)) =

   672       ATerm (case (higher_order, s) of

   673                (true, @{type_name bool}) => `I tptp_bool_type

   674              | (true, @{type_name fun}) => `I tptp_fun_type

   675              | _ => if s = homo_infinite_type_name then `I tptp_individual_type

   676                     else `make_fixed_type_const s,

   677              map term Ts)

   678     | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])

   679     | term (TVar ((x as (s, _)), _)) =

   680       ATerm ((make_schematic_type_var x, s), [])

   681   in term end

   683 (* This shouldn't clash with anything else. *)

   684 val mangled_type_sep = "\000"

   686 fun generic_mangled_type_name f (ATerm (name, [])) = f name

   687   | generic_mangled_type_name f (ATerm (name, tys)) =

   688     f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)

   689     ^ ")"

   691 val bool_atype = AType (`I tptp_bool_type)

   693 fun make_simple_type s =

   694   if s = tptp_bool_type orelse s = tptp_fun_type orelse

   695      s = tptp_individual_type then

   696     s

   697   else

   698     simple_type_prefix ^ ascii_of s

   700 fun ho_type_from_fo_term higher_order pred_sym ary =

   701   let

   702     fun to_atype ty =

   703       AType ((make_simple_type (generic_mangled_type_name fst ty),

   704               generic_mangled_type_name snd ty))

   705     fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))

   706     fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty

   707       | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys

   708     fun to_ho (ty as ATerm ((s, _), tys)) =

   709       if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty

   710   in if higher_order then to_ho else to_fo ary end

   712 fun mangled_type higher_order pred_sym ary =

   713   ho_type_from_fo_term higher_order pred_sym ary o fo_term_from_typ higher_order

   715 fun mangled_const_name T_args (s, s') =

   716   let

   717     val ty_args = map (fo_term_from_typ false) T_args

   718     fun type_suffix f g =

   719       fold_rev (curry (op ^) o g o prefix mangled_type_sep

   720                 o generic_mangled_type_name f) ty_args ""

   721   in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end

   723 val parse_mangled_ident =

   724   Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode

   726 fun parse_mangled_type x =

   727   (parse_mangled_ident

   728    -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")

   729                     [] >> ATerm) x

   730 and parse_mangled_types x =

   731   (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x

   733 fun unmangled_type s =

   734   s |> suffix ")" |> raw_explode

   735     |> Scan.finite Symbol.stopper

   736            (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^

   737                                                 quote s)) parse_mangled_type))

   738     |> fst

   740 val unmangled_const_name = space_explode mangled_type_sep #> hd

   741 fun unmangled_const s =

   742   let val ss = space_explode mangled_type_sep s in

   743     (hd ss, map unmangled_type (tl ss))

   744   end

   746 fun introduce_proxies format type_sys =

   747   let

   748     fun intro top_level (CombApp (tm1, tm2)) =

   749         CombApp (intro top_level tm1, intro false tm2)

   750       | intro top_level (CombConst (name as (s, _), T, T_args)) =

   751         (case proxify_const s of

   752            SOME (_, proxy_base) =>

   753            if top_level orelse is_setting_higher_order format type_sys then

   754              case (top_level, s) of

   755                (_, "c_False") => (`I tptp_false, [])

   756              | (_, "c_True") => (`I tptp_true, [])

   757              | (false, "c_Not") => (`I tptp_not, [])

   758              | (false, "c_conj") => (`I tptp_and, [])

   759              | (false, "c_disj") => (`I tptp_or, [])

   760              | (false, "c_implies") => (`I tptp_implies, [])

   761              | (false, s) =>

   762                if is_tptp_equal s then (`I tptp_equal, [])

   763                else (proxy_base |>> prefix const_prefix, T_args)

   764              | _ => (name, [])

   765            else

   766              (proxy_base |>> prefix const_prefix, T_args)

   767           | NONE => (name, T_args))

   768         |> (fn (name, T_args) => CombConst (name, T, T_args))

   769       | intro _ tm = tm

   770   in intro true end

   772 fun combformula_from_prop thy format type_sys eq_as_iff =

   773   let

   774     fun do_term bs t atomic_types =

   775       combterm_from_term thy bs (Envir.eta_contract t)

   776       |>> (introduce_proxies format type_sys #> AAtom)

   777       ||> union (op =) atomic_types

   778     fun do_quant bs q s T t' =

   779       let val s = Name.variant (map fst bs) s in

   780         do_formula ((s, T) :: bs) t'

   781         #>> mk_aquant q [(`make_bound_var s, SOME T)]

   782       end

   783     and do_conn bs c t1 t2 =

   784       do_formula bs t1 ##>> do_formula bs t2

   785       #>> uncurry (mk_aconn c)

   786     and do_formula bs t =

   787       case t of

   788         @{const Not} $ t1 => do_formula bs t1 #>> mk_anot

   789       | Const (@{const_name All}, _) $ Abs (s, T, t') =>

   790         do_quant bs AForall s T t'

   791       | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>

   792         do_quant bs AExists s T t'

   793       | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2

   794       | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2

   795       | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2

   796       | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>

   797         if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t

   798       | _ => do_term bs t

   799   in do_formula [] end

   801 fun presimplify_term ctxt =

   802   Skip_Proof.make_thm (Proof_Context.theory_of ctxt)

   803   #> Meson.presimplify ctxt

   804   #> prop_of

   806 fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j

   807 fun conceal_bounds Ts t =

   808   subst_bounds (map (Free o apfst concealed_bound_name)

   809                     (0 upto length Ts - 1 ~~ Ts), t)

   810 fun reveal_bounds Ts =

   811   subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))

   812                     (0 upto length Ts - 1 ~~ Ts))

   814 fun extensionalize_term ctxt t =

   815   let val thy = Proof_Context.theory_of ctxt in

   816     t |> cterm_of thy |> Meson.extensionalize_conv ctxt

   817       |> prop_of |> Logic.dest_equals |> snd

   818   end

   820 fun introduce_combinators_in_term ctxt kind t =

   821   let val thy = Proof_Context.theory_of ctxt in

   822     if Meson.is_fol_term thy t then

   823       t

   824     else

   825       let

   826         fun aux Ts t =

   827           case t of

   828             @{const Not} $ t1 => @{const Not} $ aux Ts t1

   829           | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>

   830             t0 $ Abs (s, T, aux (T :: Ts) t')

   831           | (t0 as Const (@{const_name All}, _)) $ t1 =>

   832             aux Ts (t0 $ eta_expand Ts t1 1)

   833           | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>

   834             t0 $ Abs (s, T, aux (T :: Ts) t')

   835           | (t0 as Const (@{const_name Ex}, _)) $ t1 =>

   836             aux Ts (t0 $ eta_expand Ts t1 1)

   837           | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2

   838           | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2

   839           | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2

   840           | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))

   841               $ t1 $ t2 =>

   842             t0 $ aux Ts t1 $ aux Ts t2

   843           | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then

   844                    t

   845                  else

   846                    t |> conceal_bounds Ts

   847                      |> Envir.eta_contract

   848                      |> cterm_of thy

   849                      |> Meson_Clausify.introduce_combinators_in_cterm

   850                      |> prop_of |> Logic.dest_equals |> snd

   851                      |> reveal_bounds Ts

   852         val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single

   853       in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end

   854       handle THM _ =>

   855              (* A type variable of sort "{}" will make abstraction fail. *)

   856              if kind = Conjecture then HOLogic.false_const

   857              else HOLogic.true_const

   858   end

   860 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the

   861    same in Sledgehammer to prevent the discovery of unreplayable proofs. *)

   862 fun freeze_term t =

   863   let

   864     fun aux (t $ u) = aux t $ aux u

   865       | aux (Abs (s, T, t)) = Abs (s, T, aux t)

   866       | aux (Var ((s, i), T)) =

   867         Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)

   868       | aux t = t

   869   in t |> exists_subterm is_Var t ? aux end

   871 (* making fact and conjecture formulas *)

   872 fun make_formula ctxt format type_sys eq_as_iff presimp name loc kind t =

   873   let

   874     val thy = Proof_Context.theory_of ctxt

   875     val t = t |> Envir.beta_eta_contract

   876               |> transform_elim_prop

   877               |> Object_Logic.atomize_term thy

   878     val need_trueprop = (fastype_of t = @{typ bool})

   879     val t = t |> need_trueprop ? HOLogic.mk_Trueprop

   880               |> Raw_Simplifier.rewrite_term thy

   881                      (Meson.unfold_set_const_simps ctxt) []

   882               |> extensionalize_term ctxt

   883               |> presimp ? presimplify_term ctxt

   884               |> perhaps (try (HOLogic.dest_Trueprop))

   885               |> introduce_combinators_in_term ctxt kind

   886               |> kind <> Axiom ? freeze_term

   887     val (combformula, atomic_types) =

   888       combformula_from_prop thy format type_sys eq_as_iff t []

   889   in

   890     {name = name, locality = loc, kind = kind, combformula = combformula,

   891      atomic_types = atomic_types}

   892   end

   894 fun make_fact ctxt format type_sys keep_trivial eq_as_iff presimp

   895               ((name, loc), t) =

   896   case (keep_trivial,

   897         make_formula ctxt format type_sys eq_as_iff presimp name loc Axiom t) of

   898     (false, formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...}) =>

   899     if s = tptp_true then NONE else SOME formula

   900   | (_, formula) => SOME formula

   902 fun make_conjecture ctxt format prem_kind type_sys ts =

   903   let val last = length ts - 1 in

   904     map2 (fn j => fn t =>

   905              let

   906                val (kind, maybe_negate) =

   907                  if j = last then

   908                    (Conjecture, I)

   909                  else

   910                    (prem_kind,

   911                     if prem_kind = Conjecture then update_combformula mk_anot

   912                     else I)

   913               in

   914                 t |> make_formula ctxt format type_sys true true

   915                                   (string_of_int j) General kind

   916                   |> maybe_negate

   917               end)

   918          (0 upto last) ts

   919   end

   921 (** Finite and infinite type inference **)

   923 fun deep_freeze_atyp (TVar (_, S)) = TFree ("v", S)

   924   | deep_freeze_atyp T = T

   925 val deep_freeze_type = map_atyps deep_freeze_atyp

   927 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are

   928    dangerous because their "exhaust" properties can easily lead to unsound ATP

   929    proofs. On the other hand, all HOL infinite types can be given the same

   930    models in first-order logic (via Löwenheim-Skolem). *)

   932 fun should_encode_type ctxt (nonmono_Ts as _ :: _) _ T =

   933     exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts

   934   | should_encode_type _ _ All_Types _ = true

   935   | should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T

   936   | should_encode_type _ _ _ _ = false

   938 fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness))

   939                              should_predicate_on_var T =

   940     (heaviness = Heavy orelse should_predicate_on_var ()) andalso

   941     should_encode_type ctxt nonmono_Ts level T

   942   | should_predicate_on_type _ _ _ _ _ = false

   944 fun is_var_or_bound_var (CombConst ((s, _), _, _)) =

   945     String.isPrefix bound_var_prefix s

   946   | is_var_or_bound_var (CombVar _) = true

   947   | is_var_or_bound_var _ = false

   949 datatype tag_site = Top_Level | Eq_Arg | Elsewhere

   951 fun should_tag_with_type _ _ _ Top_Level _ _ = false

   952   | should_tag_with_type ctxt nonmono_Ts (Tags (_, level, heaviness)) site u T =

   953     (case heaviness of

   954        Heavy => should_encode_type ctxt nonmono_Ts level T

   955      | Light =>

   956        case (site, is_var_or_bound_var u) of

   957          (Eq_Arg, true) => should_encode_type ctxt nonmono_Ts level T

   958        | _ => false)

   959   | should_tag_with_type _ _ _ _ _ _ = false

   961 fun homogenized_type ctxt nonmono_Ts level =

   962   let

   963     val should_encode = should_encode_type ctxt nonmono_Ts level

   964     fun homo 0 T = if should_encode T then T else homo_infinite_type

   965       | homo ary (Type (@{type_name fun}, [T1, T2])) =

   966         homo 0 T1 --> homo (ary - 1) T2

   967       | homo _ _ = raise Fail "expected function type"

   968   in homo end

   970 (** "hBOOL" and "hAPP" **)

   972 type sym_info =

   973   {pred_sym : bool, min_ary : int, max_ary : int, types : typ list}

   975 fun add_combterm_syms_to_table ctxt explicit_apply =

   976   let

   977     fun consider_var_arity const_T var_T max_ary =

   978       let

   979         fun iter ary T =

   980           if ary = max_ary orelse type_instance ctxt (var_T, T) then ary

   981           else iter (ary + 1) (range_type T)

   982       in iter 0 const_T end

   983     fun add top_level tm (accum as (ho_var_Ts, sym_tab)) =

   984       let val (head, args) = strip_combterm_comb tm in

   985         (case head of

   986            CombConst ((s, _), T, _) =>

   987            if String.isPrefix bound_var_prefix s then

   988              if explicit_apply = NONE andalso can dest_funT T then

   989                let

   990                  fun repair_min_arity {pred_sym, min_ary, max_ary, types} =

   991                    {pred_sym = pred_sym,

   992                     min_ary =

   993                       fold (fn T' => consider_var_arity T' T) types min_ary,

   994                     max_ary = max_ary, types = types}

   995                  val ho_var_Ts' = ho_var_Ts |> insert_type ctxt I T

   996                in

   997                  if pointer_eq (ho_var_Ts', ho_var_Ts) then accum

   998                  else (ho_var_Ts', Symtab.map (K repair_min_arity) sym_tab)

   999                end

  1000              else

  1001                accum

  1002            else

  1003              let

  1004                val ary = length args

  1005              in

  1006                (ho_var_Ts,

  1007                 case Symtab.lookup sym_tab s of

  1008                   SOME {pred_sym, min_ary, max_ary, types} =>

  1009                   let

  1010                     val types' = types |> insert_type ctxt I T

  1011                     val min_ary =

  1012                       if is_some explicit_apply orelse

  1013                          pointer_eq (types', types) then

  1014                         min_ary

  1015                       else

  1016                         fold (consider_var_arity T) ho_var_Ts min_ary

  1017                   in

  1018                     Symtab.update (s, {pred_sym = pred_sym andalso top_level,

  1019                                        min_ary = Int.min (ary, min_ary),

  1020                                        max_ary = Int.max (ary, max_ary),

  1021                                        types = types'})

  1022                                   sym_tab

  1023                   end

  1024                 | NONE =>

  1025                   let

  1026                     val min_ary =

  1027                       case explicit_apply of

  1028                         SOME true => 0

  1029                       | SOME false => ary

  1030                       | NONE => fold (consider_var_arity T) ho_var_Ts ary

  1031                   in

  1032                     Symtab.update_new (s, {pred_sym = top_level,

  1033                                            min_ary = min_ary, max_ary = ary,

  1034                                            types = [T]})

  1035                                       sym_tab

  1036                   end)

  1037              end

  1038          | _ => accum)

  1039         |> fold (add false) args

  1040       end

  1041   in add true end

  1042 fun add_fact_syms_to_table ctxt explicit_apply =

  1043   fact_lift (formula_fold NONE

  1044                           (K (add_combterm_syms_to_table ctxt explicit_apply)))

  1046 val default_sym_table_entries : (string * sym_info) list =

  1047   [(tptp_equal, {pred_sym = true, min_ary = 2, max_ary = 2, types = []}),

  1048    (tptp_old_equal, {pred_sym = true, min_ary = 2, max_ary = 2, types = []}),

  1049    (make_fixed_const predicator_name,

  1050     {pred_sym = true, min_ary = 1, max_ary = 1, types = []})] @

  1051   ([tptp_false, tptp_true]

  1052    |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []}))

  1054 fun sym_table_for_facts ctxt explicit_apply facts =

  1055   Symtab.empty

  1056   |> fold Symtab.default default_sym_table_entries

  1057   |> pair [] |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd

  1059 fun min_arity_of sym_tab s =

  1060   case Symtab.lookup sym_tab s of

  1061     SOME ({min_ary, ...} : sym_info) => min_ary

  1062   | NONE =>

  1063     case strip_prefix_and_unascii const_prefix s of

  1064       SOME s =>

  1065       let val s = s |> unmangled_const_name |> invert_const in

  1066         if s = predicator_name then 1

  1067         else if s = app_op_name then 2

  1068         else if s = type_pred_name then 1

  1069         else 0

  1070       end

  1071     | NONE => 0

  1073 (* True if the constant ever appears outside of the top-level position in

  1074    literals, or if it appears with different arities (e.g., because of different

  1075    type instantiations). If false, the constant always receives all of its

  1076    arguments and is used as a predicate. *)

  1077 fun is_pred_sym sym_tab s =

  1078   case Symtab.lookup sym_tab s of

  1079     SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>

  1080     pred_sym andalso min_ary = max_ary

  1081   | NONE => false

  1083 val predicator_combconst =

  1084   CombConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, [])

  1085 fun predicator tm = CombApp (predicator_combconst, tm)

  1087 fun introduce_predicators_in_combterm sym_tab tm =

  1088   case strip_combterm_comb tm of

  1089     (CombConst ((s, _), _, _), _) =>

  1090     if is_pred_sym sym_tab s then tm else predicator tm

  1091   | _ => predicator tm

  1093 fun list_app head args = fold (curry (CombApp o swap)) args head

  1095 fun explicit_app arg head =

  1096   let

  1097     val head_T = combtyp_of head

  1098     val (arg_T, res_T) = dest_funT head_T

  1099     val explicit_app =

  1100       CombConst (`make_fixed_const app_op_name, head_T --> head_T,

  1101                  [arg_T, res_T])

  1102   in list_app explicit_app [head, arg] end

  1103 fun list_explicit_app head args = fold explicit_app args head

  1105 fun introduce_explicit_apps_in_combterm sym_tab =

  1106   let

  1107     fun aux tm =

  1108       case strip_combterm_comb tm of

  1109         (head as CombConst ((s, _), _, _), args) =>

  1110         args |> map aux

  1111              |> chop (min_arity_of sym_tab s)

  1112              |>> list_app head

  1113              |-> list_explicit_app

  1114       | (head, args) => list_explicit_app head (map aux args)

  1115   in aux end

  1117 fun chop_fun 0 T = ([], T)

  1118   | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =

  1119     chop_fun (n - 1) ran_T |>> cons dom_T

  1120   | chop_fun _ _ = raise Fail "unexpected non-function"

  1122 fun filter_type_args _ _ _ [] = []

  1123   | filter_type_args thy s arity T_args =

  1124     let

  1125       (* will throw "TYPE" for pseudo-constants *)

  1126       val U = if s = app_op_name then

  1127                 @{typ "('a => 'b) => 'a => 'b"} |> Logic.varifyT_global

  1128               else

  1129                 s |> Sign.the_const_type thy

  1130     in

  1131       case Term.add_tvarsT (U |> chop_fun arity |> snd) [] of

  1132         [] => []

  1133       | res_U_vars =>

  1134         let val U_args = (s, U) |> Sign.const_typargs thy in

  1135           U_args ~~ T_args

  1136           |> map_filter (fn (U, T) =>

  1137                             if member (op =) res_U_vars (dest_TVar U) then

  1138                               SOME T

  1139                             else

  1140                               NONE)

  1141         end

  1142     end

  1143     handle TYPE _ => T_args

  1145 fun enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys =

  1146   let

  1147     val thy = Proof_Context.theory_of ctxt

  1148     fun aux arity (CombApp (tm1, tm2)) =

  1149         CombApp (aux (arity + 1) tm1, aux 0 tm2)

  1150       | aux arity (CombConst (name as (s, _), T, T_args)) =

  1151         let

  1152           val level = level_of_type_sys type_sys

  1153           val (T, T_args) =

  1154             (* Aggressively merge most "hAPPs" if the type system is unsound

  1155                anyway, by distinguishing overloads only on the homogenized

  1156                result type. Don't do it for lightweight type systems, though,

  1157                since it leads to too many unsound proofs. *)

  1158             if s = const_prefix ^ app_op_name andalso

  1159                length T_args = 2 andalso

  1160                not (is_type_sys_virtually_sound type_sys) andalso

  1161                heaviness_of_type_sys type_sys = Heavy then

  1162               T_args |> map (homogenized_type ctxt nonmono_Ts level 0)

  1163                      |> (fn Ts => let val T = hd Ts --> nth Ts 1 in

  1164                                     (T --> T, tl Ts)

  1165                                   end)

  1166             else

  1167               (T, T_args)

  1168         in

  1169           (case strip_prefix_and_unascii const_prefix s of

  1170              NONE => (name, T_args)

  1171            | SOME s'' =>

  1172              let

  1173                val s'' = invert_const s''

  1174                fun filtered_T_args false = T_args

  1175                  | filtered_T_args true = filter_type_args thy s'' arity T_args

  1176              in

  1177                case type_arg_policy type_sys s'' of

  1178                  Explicit_Type_Args drop_args =>

  1179                  (name, filtered_T_args drop_args)

  1180                | Mangled_Type_Args drop_args =>

  1181                  (mangled_const_name (filtered_T_args drop_args) name, [])

  1182                | No_Type_Args => (name, [])

  1183              end)

  1184           |> (fn (name, T_args) => CombConst (name, T, T_args))

  1185         end

  1186       | aux _ tm = tm

  1187   in aux 0 end

  1189 fun repair_combterm ctxt format nonmono_Ts type_sys sym_tab =

  1190   not (is_setting_higher_order format type_sys)

  1191   ? (introduce_explicit_apps_in_combterm sym_tab

  1192      #> introduce_predicators_in_combterm sym_tab)

  1193   #> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys

  1194 fun repair_fact ctxt format nonmono_Ts type_sys sym_tab =

  1195   update_combformula (formula_map

  1196       (repair_combterm ctxt format nonmono_Ts type_sys sym_tab))

  1198 (** Helper facts **)

  1200 (* The Boolean indicates that a fairly sound type encoding is needed. *)

  1201 val helper_table =

  1202   [("COMBI", (false, @{thms Meson.COMBI_def})),

  1203    ("COMBK", (false, @{thms Meson.COMBK_def})),

  1204    ("COMBB", (false, @{thms Meson.COMBB_def})),

  1205    ("COMBC", (false, @{thms Meson.COMBC_def})),

  1206    ("COMBS", (false, @{thms Meson.COMBS_def})),

  1207    ("fequal",

  1208     (* This is a lie: Higher-order equality doesn't need a sound type encoding.

  1209        However, this is done so for backward compatibility: Including the

  1210        equality helpers by default in Metis breaks a few existing proofs. *)

  1211     (true, @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]

  1212                   fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),

  1213    ("fFalse", (true, @{thms True_or_False})),

  1214    ("fFalse", (false, [@{lemma "~ fFalse" by (unfold fFalse_def) fast}])),

  1215    ("fTrue", (true, @{thms True_or_False})),

  1216    ("fTrue", (false, [@{lemma "fTrue" by (unfold fTrue_def) fast}])),

  1217    ("fNot",

  1218     (false, @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]

  1219                    fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),

  1220    ("fconj",

  1221     (false,

  1222      @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"

  1223          by (unfold fconj_def) fast+})),

  1224    ("fdisj",

  1225     (false,

  1226      @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"

  1227          by (unfold fdisj_def) fast+})),

  1228    ("fimplies",

  1229     (false, @{lemma "P | fimplies P Q" "~ Q | fimplies P Q"

  1230                     "~ fimplies P Q | ~ P | Q"

  1231                 by (unfold fimplies_def) fast+})),

  1232    ("If", (true, @{thms if_True if_False True_or_False}))]

  1234 fun ti_ti_helper_fact () =

  1235   let

  1236     fun var s = ATerm (`I s, [])

  1237     fun tag tm = ATerm (`make_fixed_const type_tag_name, [var "X", tm])

  1238   in

  1239     Formula (helper_prefix ^ "ti_ti", Axiom,

  1240              AAtom (ATerm (`I tptp_equal, [tag (tag (var "Y")), tag (var "Y")]))

  1241              |> close_formula_universally, simp_info, NONE)

  1242   end

  1244 fun helper_facts_for_sym ctxt format type_sys (s, {types, ...} : sym_info) =

  1245   case strip_prefix_and_unascii const_prefix s of

  1246     SOME mangled_s =>

  1247     let

  1248       val thy = Proof_Context.theory_of ctxt

  1249       val unmangled_s = mangled_s |> unmangled_const_name

  1250       fun dub_and_inst c needs_fairly_sound (th, j) =

  1251         ((c ^ "_" ^ string_of_int j ^

  1252           (if needs_fairly_sound then typed_helper_suffix

  1253            else untyped_helper_suffix),

  1254           General),

  1255          let val t = th |> prop_of in

  1256            t |> ((case general_type_arg_policy type_sys of

  1257                     Mangled_Type_Args _ => true

  1258                   | _ => false) andalso

  1259                  not (null (Term.hidden_polymorphism t)))

  1260                 ? (case types of

  1261                      [T] => specialize_type thy (invert_const unmangled_s, T)

  1262                    | _ => I)

  1263          end)

  1264       fun make_facts eq_as_iff =

  1265         map_filter (make_fact ctxt format type_sys false eq_as_iff false)

  1266       val fairly_sound = is_type_sys_fairly_sound type_sys

  1267     in

  1268       helper_table

  1269       |> maps (fn (metis_s, (needs_fairly_sound, ths)) =>

  1270                   if metis_s <> unmangled_s orelse

  1271                      (needs_fairly_sound andalso not fairly_sound) then

  1272                     []

  1273                   else

  1274                     ths ~~ (1 upto length ths)

  1275                     |> map (dub_and_inst mangled_s needs_fairly_sound)

  1276                     |> make_facts (not needs_fairly_sound))

  1277     end

  1278   | NONE => []

  1279 fun helper_facts_for_sym_table ctxt format type_sys sym_tab =

  1280   Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_sys) sym_tab

  1281                   []

  1283 fun translate_atp_fact ctxt format type_sys keep_trivial =

  1284   `(make_fact ctxt format type_sys keep_trivial true true o apsnd prop_of)

  1286 (***************************************************************)

  1287 (* Type Classes Present in the Axiom or Conjecture Clauses     *)

  1288 (***************************************************************)

  1290 fun set_insert (x, s) = Symtab.update (x, ()) s

  1292 fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)

  1294 (* Remove this trivial type class (FIXME: similar code elsewhere) *)

  1295 fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset

  1297 fun tfree_classes_of_terms ts =

  1298   let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts

  1299   in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;

  1301 fun tvar_classes_of_terms ts =

  1302   let val sorts_list = map (map #2 o OldTerm.term_tvars) ts

  1303   in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;

  1305 (*fold type constructors*)

  1306 fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))

  1307   | fold_type_consts _ _ x = x;

  1309 (*Type constructors used to instantiate overloaded constants are the only ones needed.*)

  1310 fun add_type_consts_in_term thy =

  1311   let

  1312     fun aux (Const (@{const_name Meson.skolem}, _) $ _) = I

  1313       | aux (t $ u) = aux t #> aux u

  1314       | aux (Const x) =

  1315         fold (fold_type_consts set_insert) (Sign.const_typargs thy x)

  1316       | aux (Abs (_, _, u)) = aux u

  1317       | aux _ = I

  1318   in aux end

  1320 fun type_consts_of_terms thy ts =

  1321   Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);

  1324 fun translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t

  1325                        rich_facts =

  1326   let

  1327     val thy = Proof_Context.theory_of ctxt

  1328     val fact_ts = map (prop_of o snd o snd) rich_facts

  1329     val (facts, fact_names) =

  1330       rich_facts

  1331       |> map_filter (fn (NONE, _) => NONE

  1332                       | (SOME fact, (name, _)) => SOME (fact, name))

  1333       |> ListPair.unzip

  1334     (* Remove existing facts from the conjecture, as this can dramatically

  1335        boost an ATP's performance (for some reason). *)

  1336     val hyp_ts = hyp_ts |> filter_out (member (op aconv) fact_ts)

  1337     val goal_t = Logic.list_implies (hyp_ts, concl_t)

  1338     val all_ts = goal_t :: fact_ts

  1339     val subs = tfree_classes_of_terms all_ts

  1340     val supers = tvar_classes_of_terms all_ts

  1341     val tycons = type_consts_of_terms thy all_ts

  1342     val conjs =

  1343       hyp_ts @ [concl_t] |> make_conjecture ctxt format prem_kind type_sys

  1344     val (supers', arity_clauses) =

  1345       if level_of_type_sys type_sys = No_Types then ([], [])

  1346       else make_arity_clauses thy tycons supers

  1347     val class_rel_clauses = make_class_rel_clauses thy subs supers'

  1348   in

  1349     (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses))

  1350   end

  1352 fun fo_literal_from_type_literal (TyLitVar (class, name)) =

  1353     (true, ATerm (class, [ATerm (name, [])]))

  1354   | fo_literal_from_type_literal (TyLitFree (class, name)) =

  1355     (true, ATerm (class, [ATerm (name, [])]))

  1357 fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot

  1359 fun type_pred_combterm ctxt nonmono_Ts type_sys T tm =

  1360   CombApp (CombConst (`make_fixed_const type_pred_name, T --> @{typ bool}, [T])

  1361            |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys,

  1362            tm)

  1364 fun var_occurs_positively_naked_in_term _ (SOME false) _ accum = accum

  1365   | var_occurs_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =

  1366     accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))

  1367 fun is_var_nonmonotonic_in_formula _ _ (SOME false) _ = false

  1368   | is_var_nonmonotonic_in_formula pos phi _ name =

  1369     formula_fold pos (var_occurs_positively_naked_in_term name) phi false

  1371 fun mk_const_aterm x T_args args =

  1372   ATerm (x, map (fo_term_from_typ false) T_args @ args)

  1374 fun tag_with_type ctxt format nonmono_Ts type_sys T tm =

  1375   CombConst (`make_fixed_const type_tag_name, T --> T, [T])

  1376   |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys

  1377   |> term_from_combterm ctxt format nonmono_Ts type_sys Top_Level

  1378   |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))

  1379 and term_from_combterm ctxt format nonmono_Ts type_sys =

  1380   let

  1381     fun aux site u =

  1382       let

  1383         val (head, args) = strip_combterm_comb u

  1384         val (x as (s, _), T_args) =

  1385           case head of

  1386             CombConst (name, _, T_args) => (name, T_args)

  1387           | CombVar (name, _) => (name, [])

  1388           | CombApp _ => raise Fail "impossible \"CombApp\""

  1389         val arg_site = if site = Top_Level andalso is_tptp_equal s then Eq_Arg

  1390                        else Elsewhere

  1391         val t = mk_const_aterm x T_args (map (aux arg_site) args)

  1392         val T = combtyp_of u

  1393       in

  1394         t |> (if should_tag_with_type ctxt nonmono_Ts type_sys site u T then

  1395                 tag_with_type ctxt format nonmono_Ts type_sys T

  1396               else

  1397                 I)

  1398       end

  1399   in aux end

  1400 and formula_from_combformula ctxt format nonmono_Ts type_sys

  1401                              should_predicate_on_var =

  1402   let

  1403     val higher_order = is_setting_higher_order format type_sys

  1404     val do_term = term_from_combterm ctxt format nonmono_Ts type_sys Top_Level

  1405     val do_bound_type =

  1406       case type_sys of

  1407         Simple_Types level =>

  1408         homogenized_type ctxt nonmono_Ts level 0

  1409         #> mangled_type higher_order false 0 #> SOME

  1410       | _ => K NONE

  1411     fun do_out_of_bound_type pos phi universal (name, T) =

  1412       if should_predicate_on_type ctxt nonmono_Ts type_sys

  1413              (fn () => should_predicate_on_var pos phi universal name) T then

  1414         CombVar (name, T)

  1415         |> type_pred_combterm ctxt nonmono_Ts type_sys T

  1416         |> do_term |> AAtom |> SOME

  1417       else

  1418         NONE

  1419     fun do_formula pos (AQuant (q, xs, phi)) =

  1420         let

  1421           val phi = phi |> do_formula pos

  1422           val universal = Option.map (q = AExists ? not) pos

  1423         in

  1424           AQuant (q, xs |> map (apsnd (fn NONE => NONE

  1425                                         | SOME T => do_bound_type T)),

  1426                   (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))

  1427                       (map_filter

  1428                            (fn (_, NONE) => NONE

  1429                              | (s, SOME T) =>

  1430                                do_out_of_bound_type pos phi universal (s, T))

  1431                            xs)

  1432                       phi)

  1433         end

  1434       | do_formula pos (AConn conn) = aconn_map pos do_formula conn

  1435       | do_formula _ (AAtom tm) = AAtom (do_term tm)

  1436   in do_formula o SOME end

  1438 fun bound_atomic_types format type_sys Ts =

  1439   mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)

  1440                 (type_literals_for_types format type_sys Axiom Ts))

  1442 fun formula_for_fact ctxt format nonmono_Ts type_sys

  1443                      ({combformula, atomic_types, ...} : translated_formula) =

  1444   combformula

  1445   |> close_combformula_universally

  1446   |> formula_from_combformula ctxt format nonmono_Ts type_sys

  1447                               is_var_nonmonotonic_in_formula true

  1448   |> bound_atomic_types format type_sys atomic_types

  1449   |> close_formula_universally

  1451 (* Each fact is given a unique fact number to avoid name clashes (e.g., because

  1452    of monomorphization). The TPTP explicitly forbids name clashes, and some of

  1453    the remote provers might care. *)

  1454 fun formula_line_for_fact ctxt format prefix nonmono_Ts type_sys

  1455                           (j, formula as {name, locality, kind, ...}) =

  1456   Formula (prefix ^ (if polymorphism_of_type_sys type_sys = Polymorphic then ""

  1457                      else string_of_int j ^ "_") ^

  1458            ascii_of name,

  1459            kind, formula_for_fact ctxt format nonmono_Ts type_sys formula, NONE,

  1460            case locality of

  1461              Intro => intro_info

  1462            | Elim => elim_info

  1463            | Simp => simp_info

  1464            | _ => NONE)

  1466 fun formula_line_for_class_rel_clause ({name, subclass, superclass, ...}

  1467                                        : class_rel_clause) =

  1468   let val ty_arg = ATerm (`I "T", []) in

  1469     Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,

  1470              AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),

  1471                                AAtom (ATerm (superclass, [ty_arg]))])

  1472              |> close_formula_universally, intro_info, NONE)

  1473   end

  1475 fun fo_literal_from_arity_literal (TConsLit (c, t, args)) =

  1476     (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))

  1477   | fo_literal_from_arity_literal (TVarLit (c, sort)) =

  1478     (false, ATerm (c, [ATerm (sort, [])]))

  1480 fun formula_line_for_arity_clause ({name, prem_lits, concl_lits, ...}

  1481                                    : arity_clause) =

  1482   Formula (arity_clause_prefix ^ ascii_of name, Axiom,

  1483            mk_ahorn (map (formula_from_fo_literal o apfst not

  1484                           o fo_literal_from_arity_literal) prem_lits)

  1485                     (formula_from_fo_literal

  1486                          (fo_literal_from_arity_literal concl_lits))

  1487            |> close_formula_universally, intro_info, NONE)

  1489 fun formula_line_for_conjecture ctxt format nonmono_Ts type_sys

  1490         ({name, kind, combformula, ...} : translated_formula) =

  1491   Formula (conjecture_prefix ^ name, kind,

  1492            formula_from_combformula ctxt format nonmono_Ts type_sys

  1493                is_var_nonmonotonic_in_formula false

  1494                (close_combformula_universally combformula)

  1495            |> close_formula_universally, NONE, NONE)

  1497 fun free_type_literals format type_sys

  1498                        ({atomic_types, ...} : translated_formula) =

  1499   atomic_types |> type_literals_for_types format type_sys Conjecture

  1500                |> map fo_literal_from_type_literal

  1502 fun formula_line_for_free_type j lit =

  1503   Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,

  1504            formula_from_fo_literal lit, NONE, NONE)

  1505 fun formula_lines_for_free_types format type_sys facts =

  1506   let

  1507     val litss = map (free_type_literals format type_sys) facts

  1508     val lits = fold (union (op =)) litss []

  1509   in map2 formula_line_for_free_type (0 upto length lits - 1) lits end

  1511 (** Symbol declarations **)

  1513 fun should_declare_sym type_sys pred_sym s =

  1514   is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso

  1515   (case type_sys of

  1516      Simple_Types _ => true

  1517    | Tags (_, _, Light) => true

  1518    | _ => not pred_sym)

  1520 fun sym_decl_table_for_facts ctxt type_sys repaired_sym_tab (conjs, facts) =

  1521   let

  1522     fun add_combterm in_conj tm =

  1523       let val (head, args) = strip_combterm_comb tm in

  1524         (case head of

  1525            CombConst ((s, s'), T, T_args) =>

  1526            let val pred_sym = is_pred_sym repaired_sym_tab s in

  1527              if should_declare_sym type_sys pred_sym s then

  1528                Symtab.map_default (s, [])

  1529                    (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,

  1530                                          in_conj))

  1531              else

  1532                I

  1533            end

  1534          | _ => I)

  1535         #> fold (add_combterm in_conj) args

  1536       end

  1537     fun add_fact in_conj =

  1538       fact_lift (formula_fold NONE (K (add_combterm in_conj)))

  1539   in

  1540     Symtab.empty

  1541     |> is_type_sys_fairly_sound type_sys

  1542        ? (fold (add_fact true) conjs #> fold (add_fact false) facts)

  1543   end

  1545 (* These types witness that the type classes they belong to allow infinite

  1546    models and hence that any types with these type classes is monotonic. *)

  1547 val known_infinite_types =

  1548   [@{typ nat}, Type ("Int.int", []), @{typ "nat => bool"}]

  1550 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it

  1551    out with monotonicity" paper presented at CADE 2011. *)

  1552 fun add_combterm_nonmonotonic_types _ _ (SOME false) _ = I

  1553   | add_combterm_nonmonotonic_types ctxt level _

  1554         (CombApp (CombApp (CombConst ((s, _), Type (_, [T, _]), _), tm1), tm2)) =

  1555     (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso

  1556      (case level of

  1557         Nonmonotonic_Types =>

  1558         not (is_type_surely_infinite ctxt known_infinite_types T)

  1559       | Finite_Types => is_type_surely_finite ctxt T

  1560       | _ => true)) ? insert_type ctxt I (deep_freeze_type T)

  1561   | add_combterm_nonmonotonic_types _ _ _ _ = I

  1562 fun add_fact_nonmonotonic_types ctxt level ({kind, combformula, ...}

  1563                                             : translated_formula) =

  1564   formula_fold (SOME (kind <> Conjecture))

  1565                (add_combterm_nonmonotonic_types ctxt level) combformula

  1566 fun nonmonotonic_types_for_facts ctxt type_sys facts =

  1567   let val level = level_of_type_sys type_sys in

  1568     if level = Nonmonotonic_Types orelse level = Finite_Types then

  1569       [] |> fold (add_fact_nonmonotonic_types ctxt level) facts

  1570          (* We must add "bool" in case the helper "True_or_False" is added

  1571             later. In addition, several places in the code rely on the list of

  1572             nonmonotonic types not being empty. *)

  1573          |> insert_type ctxt I @{typ bool}

  1574     else

  1575       []

  1576   end

  1578 fun decl_line_for_sym ctxt format nonmono_Ts type_sys s

  1579                       (s', T_args, T, pred_sym, ary, _) =

  1580   let

  1581     val (higher_order, T_arg_Ts, level) =

  1582       case type_sys of

  1583         Simple_Types level => (format = THF, [], level)

  1584       | _ => (false, replicate (length T_args) homo_infinite_type, No_Types)

  1585   in

  1586     Decl (sym_decl_prefix ^ s, (s, s'),

  1587           (T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary))

  1588           |> mangled_type higher_order pred_sym (length T_arg_Ts + ary))

  1589   end

  1591 fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false

  1593 fun formula_line_for_pred_sym_decl ctxt format conj_sym_kind nonmono_Ts type_sys

  1594                                    n s j (s', T_args, T, _, ary, in_conj) =

  1595   let

  1596     val (kind, maybe_negate) =

  1597       if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)

  1598       else (Axiom, I)

  1599     val (arg_Ts, res_T) = chop_fun ary T

  1600     val bound_names =

  1601       1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)

  1602     val bounds =

  1603       bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, []))

  1604     val bound_Ts =

  1605       arg_Ts |> map (fn T => if n > 1 orelse is_polymorphic_type T then SOME T

  1606                              else NONE)

  1607   in

  1608     Formula (sym_formula_prefix ^ s ^

  1609              (if n > 1 then "_" ^ string_of_int j else ""), kind,

  1610              CombConst ((s, s'), T, T_args)

  1611              |> fold (curry (CombApp o swap)) bounds

  1612              |> type_pred_combterm ctxt nonmono_Ts type_sys res_T

  1613              |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)

  1614              |> formula_from_combformula ctxt format nonmono_Ts type_sys

  1615                                          (K (K (K (K true)))) true

  1616              |> n > 1 ? bound_atomic_types format type_sys (atyps_of T)

  1617              |> close_formula_universally

  1618              |> maybe_negate,

  1619              intro_info, NONE)

  1620   end

  1622 fun formula_lines_for_tag_sym_decl ctxt format conj_sym_kind nonmono_Ts type_sys

  1623         n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =

  1624   let

  1625     val ident_base =

  1626       sym_formula_prefix ^ s ^ (if n > 1 then "_" ^ string_of_int j else "")

  1627     val (kind, maybe_negate) =

  1628       if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)

  1629       else (Axiom, I)

  1630     val (arg_Ts, res_T) = chop_fun ary T

  1631     val bound_names =

  1632       1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)

  1633     val bounds = bound_names |> map (fn name => ATerm (name, []))

  1634     val cst = mk_const_aterm (s, s') T_args

  1635     val atomic_Ts = atyps_of T

  1636     fun eq tms =

  1637       (if pred_sym then AConn (AIff, map AAtom tms)

  1638        else AAtom (ATerm (`I tptp_equal, tms)))

  1639       |> bound_atomic_types format type_sys atomic_Ts

  1640       |> close_formula_universally

  1641       |> maybe_negate

  1642     val should_encode = should_encode_type ctxt nonmono_Ts All_Types

  1643     val tag_with = tag_with_type ctxt format nonmono_Ts type_sys

  1644     val add_formula_for_res =

  1645       if should_encode res_T then

  1646         cons (Formula (ident_base ^ "_res", kind,

  1647                        eq [tag_with res_T (cst bounds), cst bounds],

  1648                        simp_info, NONE))

  1649       else

  1650         I

  1651     fun add_formula_for_arg k =

  1652       let val arg_T = nth arg_Ts k in

  1653         if should_encode arg_T then

  1654           case chop k bounds of

  1655             (bounds1, bound :: bounds2) =>

  1656             cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,

  1657                            eq [cst (bounds1 @ tag_with arg_T bound :: bounds2),

  1658                                cst bounds],

  1659                            simp_info, NONE))

  1660           | _ => raise Fail "expected nonempty tail"

  1661         else

  1662           I

  1663       end

  1664   in

  1665     [] |> not pred_sym ? add_formula_for_res

  1666        |> fold add_formula_for_arg (ary - 1 downto 0)

  1667   end

  1669 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd

  1671 fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts type_sys

  1672                                 (s, decls) =

  1673   case type_sys of

  1674     Simple_Types _ =>

  1675     decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_sys s)

  1676   | Preds _ =>

  1677     let

  1678       val decls =

  1679         case decls of

  1680           decl :: (decls' as _ :: _) =>

  1681           let val T = result_type_of_decl decl in

  1682             if forall (curry (type_instance ctxt o swap) T

  1683                        o result_type_of_decl) decls' then

  1684               [decl]

  1685             else

  1686               decls

  1687           end

  1688         | _ => decls

  1689       val n = length decls

  1690       val decls =

  1691         decls

  1692         |> filter (should_predicate_on_type ctxt nonmono_Ts type_sys (K true)

  1693                    o result_type_of_decl)

  1694     in

  1695       (0 upto length decls - 1, decls)

  1696       |-> map2 (formula_line_for_pred_sym_decl ctxt format conj_sym_kind

  1697                                                nonmono_Ts type_sys n s)

  1698     end

  1699   | Tags (_, _, heaviness) =>

  1700     (case heaviness of

  1701        Heavy => []

  1702      | Light =>

  1703        let val n = length decls in

  1704          (0 upto n - 1 ~~ decls)

  1705          |> maps (formula_lines_for_tag_sym_decl ctxt format conj_sym_kind

  1706                                                  nonmono_Ts type_sys n s)

  1707        end)

  1709 fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts

  1710                                      type_sys sym_decl_tab =

  1711   sym_decl_tab

  1712   |> Symtab.dest

  1713   |> sort_wrt fst

  1714   |> rpair []

  1715   |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind

  1716                                                      nonmono_Ts type_sys)

  1718 fun should_add_ti_ti_helper (Tags (Polymorphic, level, Heavy)) =

  1719     level = Nonmonotonic_Types orelse level = Finite_Types

  1720   | should_add_ti_ti_helper _ = false

  1722 fun offset_of_heading_in_problem _ [] j = j

  1723   | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =

  1724     if heading = needle then j

  1725     else offset_of_heading_in_problem needle problem (j + length lines)

  1727 val implicit_declsN = "Should-be-implicit typings"

  1728 val explicit_declsN = "Explicit typings"

  1729 val factsN = "Relevant facts"

  1730 val class_relsN = "Class relationships"

  1731 val aritiesN = "Arities"

  1732 val helpersN = "Helper facts"

  1733 val conjsN = "Conjectures"

  1734 val free_typesN = "Type variables"

  1736 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys

  1737                         explicit_apply hyp_ts concl_t facts =

  1738   let

  1739     val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =

  1740       translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t facts

  1741     val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply

  1742     val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys

  1743     val repair = repair_fact ctxt format nonmono_Ts type_sys sym_tab

  1744     val (conjs, facts) = (conjs, facts) |> pairself (map repair)

  1745     val repaired_sym_tab =

  1746       conjs @ facts |> sym_table_for_facts ctxt (SOME false)

  1747     val helpers =

  1748       repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_sys

  1749                        |> map repair

  1750     val lavish_nonmono_Ts =

  1751       if null nonmono_Ts orelse

  1752          polymorphism_of_type_sys type_sys <> Polymorphic then

  1753         nonmono_Ts

  1754       else

  1755         [TVar (("'a", 0), HOLogic.typeS)]

  1756     val sym_decl_lines =

  1757       (conjs, helpers @ facts)

  1758       |> sym_decl_table_for_facts ctxt type_sys repaired_sym_tab

  1759       |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind

  1760                                           lavish_nonmono_Ts type_sys

  1761     val helper_lines =

  1762       0 upto length helpers - 1 ~~ helpers

  1763       |> map (formula_line_for_fact ctxt format helper_prefix lavish_nonmono_Ts

  1764                                     type_sys)

  1765       |> (if should_add_ti_ti_helper type_sys then cons (ti_ti_helper_fact ())

  1766           else I)

  1767     (* Reordering these might confuse the proof reconstruction code or the SPASS

  1768        FLOTTER hack. *)

  1769     val problem =

  1770       [(explicit_declsN, sym_decl_lines),

  1771        (factsN,

  1772         map (formula_line_for_fact ctxt format fact_prefix nonmono_Ts type_sys)

  1773             (0 upto length facts - 1 ~~ facts)),

  1774        (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),

  1775        (aritiesN, map formula_line_for_arity_clause arity_clauses),

  1776        (helpersN, helper_lines),

  1777        (conjsN,

  1778         map (formula_line_for_conjecture ctxt format nonmono_Ts type_sys)

  1779             conjs),

  1780        (free_typesN,

  1781         formula_lines_for_free_types format type_sys (facts @ conjs))]

  1782     val problem =

  1783       problem

  1784       |> (if format = CNF_UEQ then filter_cnf_ueq_problem else I)

  1785       |> (if is_format_typed format then

  1786             declare_undeclared_syms_in_atp_problem type_decl_prefix

  1787                                                    implicit_declsN

  1788           else

  1789             I)

  1790     val (problem, pool) =

  1791       problem |> nice_atp_problem (Config.get ctxt readable_names)

  1792     val helpers_offset = offset_of_heading_in_problem helpersN problem 0

  1793     val typed_helpers =

  1794       map_filter (fn (j, {name, ...}) =>

  1795                      if String.isSuffix typed_helper_suffix name then SOME j

  1796                      else NONE)

  1797                  ((helpers_offset + 1 upto helpers_offset + length helpers)

  1798                   ~~ helpers)

  1799     fun add_sym_arity (s, {min_ary, ...} : sym_info) =

  1800       if min_ary > 0 then

  1801         case strip_prefix_and_unascii const_prefix s of

  1802           SOME s => Symtab.insert (op =) (s, min_ary)

  1803         | NONE => I

  1804       else

  1805         I

  1806   in

  1807     (problem,

  1808      case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,

  1809      offset_of_heading_in_problem conjsN problem 0,

  1810      offset_of_heading_in_problem factsN problem 0,

  1811      fact_names |> Vector.fromList,

  1812      typed_helpers,

  1813      Symtab.empty |> Symtab.fold add_sym_arity sym_tab)

  1814   end

  1816 (* FUDGE *)

  1817 val conj_weight = 0.0

  1818 val hyp_weight = 0.1

  1819 val fact_min_weight = 0.2

  1820 val fact_max_weight = 1.0

  1821 val type_info_default_weight = 0.8

  1823 fun add_term_weights weight (ATerm (s, tms)) =

  1824   is_tptp_user_symbol s ? Symtab.default (s, weight)

  1825   #> fold (add_term_weights weight) tms

  1826 fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =

  1827     formula_fold NONE (K (add_term_weights weight)) phi

  1828   | add_problem_line_weights _ _ = I

  1830 fun add_conjectures_weights [] = I

  1831   | add_conjectures_weights conjs =

  1832     let val (hyps, conj) = split_last conjs in

  1833       add_problem_line_weights conj_weight conj

  1834       #> fold (add_problem_line_weights hyp_weight) hyps

  1835     end

  1837 fun add_facts_weights facts =

  1838   let

  1839     val num_facts = length facts

  1840     fun weight_of j =

  1841       fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j

  1842                         / Real.fromInt num_facts

  1843   in

  1844     map weight_of (0 upto num_facts - 1) ~~ facts

  1845     |> fold (uncurry add_problem_line_weights)

  1846   end

  1848 (* Weights are from 0.0 (most important) to 1.0 (least important). *)

  1849 fun atp_problem_weights problem =

  1850   let val get = these o AList.lookup (op =) problem in

  1851     Symtab.empty

  1852     |> add_conjectures_weights (get free_typesN @ get conjsN)

  1853     |> add_facts_weights (get factsN)

  1854     |> fold (fold (add_problem_line_weights type_info_default_weight) o get)

  1855             [explicit_declsN, class_relsN, aritiesN]

  1856     |> Symtab.dest

  1857     |> sort (prod_ord Real.compare string_ord o pairself swap)

  1858   end

  1860 end;

author	blanchet
	Tue, 31 May 2011 16:38:36 +0200
changeset 43927	4dce7f2bb59f
parent 43926	0a2f5b86bdd7
child 43933	93ec303e1917
permissions	-rw-r--r--