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

     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_sys =

    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 bound_var_prefix : string

    56   val schematic_var_prefix: string

    57   val fixed_var_prefix: string

    58   val tvar_prefix: string

    59   val tfree_prefix: string

    60   val const_prefix: string

    61   val type_const_prefix: string

    62   val class_prefix: string

    63   val skolem_const_prefix : string

    64   val old_skolem_const_prefix : string

    65   val new_skolem_const_prefix : string

    66   val type_decl_prefix : string

    67   val sym_decl_prefix : string

    68   val preds_sym_formula_prefix : string

    69   val tags_sym_formula_prefix : string

    70   val fact_prefix : string

    71   val conjecture_prefix : string

    72   val helper_prefix : string

    73   val class_rel_clause_prefix : string

    74   val arity_clause_prefix : string

    75   val tfree_clause_prefix : string

    76   val typed_helper_suffix : string

    77   val untyped_helper_suffix : string

    78   val predicator_name : string

    79   val app_op_name : string

    80   val type_tag_name : string

    81   val type_pred_name : string

    82   val simple_type_prefix : string

    83   val ascii_of: string -> string

    84   val unascii_of: string -> string

    85   val strip_prefix_and_unascii : string -> string -> string option

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

    87   val invert_const: string -> string

    88   val unproxify_const: string -> string

    89   val make_bound_var : string -> string

    90   val make_schematic_var : string * int -> string

    91   val make_fixed_var : string -> string

    92   val make_schematic_type_var : string * int -> string

    93   val make_fixed_type_var : string -> string

    94   val make_fixed_const : string -> string

    95   val make_fixed_type_const : string -> string

    96   val make_type_class : string -> string

    97   val new_skolem_var_name_from_const : string -> string

    98   val num_type_args : theory -> string -> int

    99   val make_arity_clauses :

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

   101   val make_class_rel_clauses :

   102     theory -> class list -> class list -> class_rel_clause list

   103   val combtyp_of : combterm -> typ

   104   val strip_combterm_comb : combterm -> combterm * combterm list

   105   val atyps_of : typ -> typ list

   106   val combterm_from_term :

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

   108   val is_locality_global : locality -> bool

   109   val type_sys_from_string : string -> type_sys

   110   val polymorphism_of_type_sys : type_sys -> polymorphism

   111   val level_of_type_sys : type_sys -> type_level

   112   val is_type_sys_virtually_sound : type_sys -> bool

   113   val is_type_sys_fairly_sound : type_sys -> bool

   114   val choose_format : format list -> type_sys -> format * type_sys

   115   val raw_type_literals_for_types : typ list -> type_literal list

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

   117   val translate_atp_fact :

   118     Proof.context -> format -> type_sys -> bool -> (string * locality) * thm

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

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

   121   val tfree_classes_of_terms : term list -> string list

   122   val tvar_classes_of_terms : term list -> string list

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

   124   val prepare_atp_problem :

   125     Proof.context -> format -> formula_kind -> formula_kind -> type_sys

   126     -> bool option -> bool -> bool -> term list -> term

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

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

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

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

   131 end;

   133 structure ATP_Translate : ATP_TRANSLATE =

   134 struct

   136 open ATP_Util

   137 open ATP_Problem

   139 type name = string * string

   141 (* FIXME: avoid *)

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

   144 (* experimental *)

   145 val generate_useful_info = false

   147 fun useful_isabelle_info s =

   148   if generate_useful_info then

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

   150   else

   151     NONE

   153 val intro_info = useful_isabelle_info "intro"

   154 val elim_info = useful_isabelle_info "elim"

   155 val simp_info = useful_isabelle_info "simp"

   157 val bound_var_prefix = "B_"

   158 val schematic_var_prefix = "V_"

   159 val fixed_var_prefix = "v_"

   161 val tvar_prefix = "T_"

   162 val tfree_prefix = "t_"

   164 val const_prefix = "c_"

   165 val type_const_prefix = "tc_"

   166 val class_prefix = "cl_"

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

   169 val old_skolem_const_prefix = skolem_const_prefix ^ "o"

   170 val new_skolem_const_prefix = skolem_const_prefix ^ "n"

   172 val type_decl_prefix = "ty_"

   173 val sym_decl_prefix = "sy_"

   174 val preds_sym_formula_prefix = "psy_"

   175 val tags_sym_formula_prefix = "tsy_"

   176 val fact_prefix = "fact_"

   177 val conjecture_prefix = "conj_"

   178 val helper_prefix = "help_"

   179 val class_rel_clause_prefix = "crel_"

   180 val arity_clause_prefix = "arity_"

   181 val tfree_clause_prefix = "tfree_"

   183 val typed_helper_suffix = "_T"

   184 val untyped_helper_suffix = "_U"

   186 val predicator_name = "hBOOL"

   187 val app_op_name = "hAPP"

   188 val type_tag_name = "ti"

   189 val type_pred_name = "is"

   190 val simple_type_prefix = "ty_"

   192 (* Freshness almost guaranteed! *)

   193 val sledgehammer_weak_prefix = "Sledgehammer:"

   195 (*Escaping of special characters.

   196   Alphanumeric characters are left unchanged.

   197   The character _ goes to __

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

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

   200 val upper_a_minus_space = Char.ord #"A" - Char.ord #" "

   202 fun stringN_of_int 0 _ = ""

   203   | stringN_of_int k n =

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

   206 fun ascii_of_char c =

   207   if Char.isAlphaNum c then

   208     String.str c

   209   else if c = #"_" then

   210     "__"

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

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

   213   else

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

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

   217 val ascii_of = String.translate ascii_of_char

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

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

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

   223 val unascii_of =

   224   let

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

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

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

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

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

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

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

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

   233         else

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

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

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

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

   238           end

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

   240   in un [] o String.explode end

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

   243    un-ASCII'd. *)

   244 fun strip_prefix_and_unascii s1 s =

   245   if String.isPrefix s1 s then

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

   247   else

   248     NONE

   250 val proxies =

   251   [("c_False",

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

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

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

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

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

   257    ("c_implies",

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

   259    ("equal",

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

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

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

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

   266 val const_trans_table =

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   283   |> Symtab.make

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

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

   287 val const_trans_table_inv =

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

   289 val const_trans_table_unprox =

   290   Symtab.empty

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

   293 val invert_const = perhaps (Symtab.lookup const_trans_table_inv)

   294 val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)

   296 fun lookup_const c =

   297   case Symtab.lookup const_trans_table c of

   298     SOME c' => c'

   299   | NONE => ascii_of c

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

   302 fun trim_type_var s =

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

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

   306 fun ascii_of_indexname (v,0) = ascii_of v

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

   309 fun make_bound_var x = bound_var_prefix ^ ascii_of x

   310 fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v

   311 fun make_fixed_var x = fixed_var_prefix ^ ascii_of x

   313 fun make_schematic_type_var (x,i) =

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

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

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

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

   319   | make_fixed_const c = const_prefix ^ lookup_const c

   321 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c

   323 fun make_type_class clas = class_prefix ^ ascii_of clas

   325 fun new_skolem_var_name_from_const s =

   326   let val ss = s |> space_explode Long_Name.separator in

   327     nth ss (length ss - 2)

   328   end

   330 (* The number of type arguments of a constant, zero if it's monomorphic. For

   331    (instances of) Skolem pseudoconstants, this information is encoded in the

   332    constant name. *)

   333 fun num_type_args thy s =

   334   if String.isPrefix skolem_const_prefix s then

   335     s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the

   336   else

   337     (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length

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

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

   342 datatype type_literal =

   343   TyLitVar of name * name |

   344   TyLitFree of name * name

   347 (** Isabelle arities **)

   349 datatype arity_literal =

   350   TConsLit of name * name * name list |

   351   TVarLit of name * name

   353 fun gen_TVars 0 = []

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

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

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

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

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

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

   362 type arity_clause =

   363   {name: string,

   364    prem_lits: arity_literal list,

   365    concl_lits: arity_literal}

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

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

   369   let

   370     val tvars = gen_TVars (length args)

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

   372   in

   373     {name = name,

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

   375      concl_lits = TConsLit (`make_type_class cls,

   376                             `make_fixed_type_const tcons,

   377                             tvars ~~ tvars)}

   378   end

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

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

   382       arity_clause seen n (tcons,ars)

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

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

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

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

   387       else

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

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

   391 fun multi_arity_clause [] = []

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

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

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

   396   provided its arguments have the corresponding sorts.*)

   397 fun type_class_pairs thy tycons classes =

   398   let

   399     val alg = Sign.classes_of thy

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

   401     fun add_class tycon class =

   402       cons (class, domain_sorts tycon class)

   403       handle Sorts.CLASS_ERROR _ => I

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

   405   in map try_classes tycons end

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

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

   409   | iter_type_class_pairs thy tycons classes =

   410       let val cpairs = type_class_pairs thy tycons classes

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

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

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

   414       in (union (op =) classes' classes, union (op =) cpairs' cpairs) end

   416 fun make_arity_clauses thy tycons =

   417   iter_type_class_pairs thy tycons ##> multi_arity_clause

   420 (** Isabelle class relations **)

   422 type class_rel_clause =

   423   {name: string,

   424    subclass: name,

   425    superclass: name}

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

   428 fun class_pairs _ [] _ = []

   429   | class_pairs thy subs supers =

   430       let

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

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

   433         fun add_supers sub = fold (add_super sub) supers

   434       in fold add_supers subs [] end

   436 fun make_class_rel_clause (sub,super) =

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

   438    subclass = `make_type_class sub,

   439    superclass = `make_type_class super}

   441 fun make_class_rel_clauses thy subs supers =

   442   map make_class_rel_clause (class_pairs thy subs supers)

   444 datatype combterm =

   445   CombConst of name * typ * typ list |

   446   CombVar of name * typ |

   447   CombApp of combterm * combterm

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

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

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

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

   454 fun strip_combterm_comb u =

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

   456         |   stripc  x =  x

   457     in stripc(u,[]) end

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

   461 fun new_skolem_const_name s num_T_args =

   462   [new_skolem_const_prefix, s, string_of_int num_T_args]

   463   |> space_implode Long_Name.separator

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

   466    infomation. *)

   467 fun combterm_from_term thy bs (P $ Q) =

   468     let

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

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

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

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

   473     let

   474       val tvar_list =

   475         (if String.isPrefix old_skolem_const_prefix c then

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

   477          else

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

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

   480     in (c', atyps_of T) end

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

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

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

   484     (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then

   485        let

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

   487          val s' = new_skolem_const_name s (length Ts)

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

   489      else

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

   491   | combterm_from_term _ bs (Bound j) =

   492     nth bs j

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

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

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

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

   499 fun is_locality_global Local = false

   500   | is_locality_global Assum = false

   501   | is_locality_global Chained = false

   502   | is_locality_global _ = true

   504 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic

   505 datatype type_level =

   506   All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types

   507 datatype type_heaviness = Heavy | Light

   509 datatype type_sys =

   510   Simple_Types of type_level |

   511   Preds of polymorphism * type_level * type_heaviness |

   512   Tags of polymorphism * type_level * type_heaviness

   514 fun try_unsuffixes ss s =

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

   517 fun type_sys_from_string s =

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

   519      SOME s => (SOME Polymorphic, s)

   520    | NONE =>

   521      case try (unprefix "mono_") s of

   522        SOME s => (SOME Monomorphic, s)

   523      | NONE =>

   524        case try (unprefix "mangled_") s of

   525          SOME s => (SOME Mangled_Monomorphic, s)

   526        | NONE => (NONE, s))

   527   ||> (fn s =>

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

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

   530             SOME s => (Nonmonotonic_Types, s)

   531           | NONE =>

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

   533               SOME s => (Finite_Types, s)

   534             | NONE => (All_Types, s))

   535   ||> apsnd (fn s =>

   536                 case try (unsuffix "_heavy") s of

   537                   SOME s => (Heavy, s)

   538                 | NONE => (Light, s))

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

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

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

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

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

   544            Tags (Polymorphic, All_Types, heaviness)

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

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

   547            Tags (Polymorphic, level, Heavy)

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

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

   550            Preds (poly, Const_Arg_Types, Light)

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

   552            Preds (Polymorphic, No_Types, Light)

   553          | _ => raise Same.SAME)

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

   556 fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic

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

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

   560 fun level_of_type_sys (Simple_Types level) = level

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

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

   564 fun heaviness_of_type_sys (Simple_Types _) = Heavy

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

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

   568 fun is_type_level_virtually_sound level =

   569   level = All_Types orelse level = Nonmonotonic_Types

   570 val is_type_sys_virtually_sound =

   571   is_type_level_virtually_sound o level_of_type_sys

   573 fun is_type_level_fairly_sound level =

   574   is_type_level_virtually_sound level orelse level = Finite_Types

   575 val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys

   577 fun is_setting_higher_order THF (Simple_Types _) = true

   578   | is_setting_higher_order _ _ = false

   580 fun choose_format formats (Simple_Types level) =

   581     if member (op =) formats THF then (THF, Simple_Types level)

   582     else if member (op =) formats TFF then (TFF, Simple_Types level)

   583     else choose_format formats (Preds (Mangled_Monomorphic, level, Heavy))

   584   | choose_format formats type_sys =

   585     (case hd formats of

   586        CNF_UEQ =>

   587        (CNF_UEQ, case type_sys of

   588                    Preds stuff =>

   589                    (if is_type_sys_fairly_sound type_sys then Preds else Tags)

   590                        stuff

   591                  | _ => type_sys)

   592      | format => (format, type_sys))

   594 type translated_formula =

   595   {name: string,

   596    locality: locality,

   597    kind: formula_kind,

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

   599    atomic_types: typ list}

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

   602                           : translated_formula) =

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

   604    atomic_types = atomic_types} : translated_formula

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

   608 val type_instance = Sign.typ_instance o Proof_Context.theory_of

   610 fun insert_type ctxt get_T x xs =

   611   let val T = get_T x in

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

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

   614   end

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

   617 datatype type_arg_policy =

   618   Explicit_Type_Args of bool |

   619   Mangled_Type_Args of bool |

   620   No_Type_Args

   622 fun should_drop_arg_type_args (Simple_Types _) =

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

   624   | should_drop_arg_type_args type_sys =

   625     level_of_type_sys type_sys = All_Types andalso

   626     heaviness_of_type_sys type_sys = Heavy

   628 fun general_type_arg_policy (Tags (_, All_Types, Heavy)) = No_Type_Args

   629   | general_type_arg_policy type_sys =

   630     if level_of_type_sys type_sys = No_Types then

   631       No_Type_Args

   632     else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then

   633       Mangled_Type_Args (should_drop_arg_type_args type_sys)

   634     else

   635       Explicit_Type_Args (should_drop_arg_type_args type_sys)

   637 fun type_arg_policy type_sys s =

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

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

   640     No_Type_Args

   641   else if s = type_tag_name then

   642     Explicit_Type_Args false

   643   else

   644     general_type_arg_policy type_sys

   646 (*Make literals for sorted type variables*)

   647 fun generic_sorts_on_type (_, []) = []

   648   | generic_sorts_on_type ((x, i), s :: ss) =

   649     generic_sorts_on_type ((x, i), ss)

   650     |> (if s = the_single @{sort HOL.type} then

   651           I

   652         else if i = ~1 then

   653           cons (TyLitFree (`make_type_class s, `make_fixed_type_var x))

   654         else

   655           cons (TyLitVar (`make_type_class s,

   656                           (make_schematic_type_var (x, i), x))))

   657 fun sorts_on_tfree (TFree (s, S)) = generic_sorts_on_type ((s, ~1), S)

   658   | sorts_on_tfree _ = []

   659 fun sorts_on_tvar (TVar z) = generic_sorts_on_type z

   660   | sorts_on_tvar _ = []

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

   663 fun raw_type_literals_for_types Ts =

   664   union_all (map sorts_on_tfree Ts @ map sorts_on_tvar Ts)

   666 fun type_literals_for_types type_sys sorts_on_typ Ts =

   667   if level_of_type_sys type_sys = No_Types then []

   668   else union_all (map sorts_on_typ Ts)

   670 fun mk_aconns c phis =

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

   672     fold_rev (mk_aconn c) phis' phi'

   673   end

   674 fun mk_ahorn [] phi = phi

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

   676 fun mk_aquant _ [] phi = phi

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

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

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

   681 fun close_universally atom_vars phi =

   682   let

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

   684         formula_vars (map fst xs @ bounds) phi

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

   686       | formula_vars bounds (AAtom tm) =

   687         union (op =) (atom_vars tm []

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

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

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

   692   | combterm_vars (CombConst _) = I

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

   694 fun close_combformula_universally phi = close_universally combterm_vars phi

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

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

   698 fun close_formula_universally phi = close_universally term_vars phi

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

   701 val homo_infinite_type = Type (homo_infinite_type_name, [])

   703 fun fo_term_from_typ higher_order =

   704   let

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

   706       ATerm (case (higher_order, s) of

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

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

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

   710                     else `make_fixed_type_const s,

   711              map term Ts)

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

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

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

   715   in term end

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

   718 val mangled_type_sep = "\000"

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

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

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

   723     ^ ")"

   725 val bool_atype = AType (`I tptp_bool_type)

   727 fun make_simple_type s =

   728   if s = tptp_bool_type orelse s = tptp_fun_type orelse

   729      s = tptp_individual_type then

   730     s

   731   else

   732     simple_type_prefix ^ ascii_of s

   734 fun ho_type_from_fo_term higher_order pred_sym ary =

   735   let

   736     fun to_atype ty =

   737       AType ((make_simple_type (generic_mangled_type_name fst ty),

   738               generic_mangled_type_name snd ty))

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

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

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

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

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

   744   in if higher_order then to_ho else to_fo ary end

   746 fun mangled_type higher_order pred_sym ary =

   747   ho_type_from_fo_term higher_order pred_sym ary o fo_term_from_typ higher_order

   749 fun mangled_const_name T_args (s, s') =

   750   let

   751     val ty_args = map (fo_term_from_typ false) T_args

   752     fun type_suffix f g =

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

   754                 o generic_mangled_type_name f) ty_args ""

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

   757 val parse_mangled_ident =

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

   760 fun parse_mangled_type x =

   761   (parse_mangled_ident

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

   763                     [] >> ATerm) x

   764 and parse_mangled_types x =

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

   767 fun unmangled_type s =

   768   s |> suffix ")" |> raw_explode

   769     |> Scan.finite Symbol.stopper

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

   771                                                 quote s)) parse_mangled_type))

   772     |> fst

   774 val unmangled_const_name = space_explode mangled_type_sep #> hd

   775 fun unmangled_const s =

   776   let val ss = space_explode mangled_type_sep s in

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

   778   end

   780 fun introduce_proxies format type_sys =

   781   let

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

   783         CombApp (intro top_level tm1, intro false tm2)

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

   785         (case proxify_const s of

   786            SOME (_, proxy_base) =>

   787            if top_level orelse is_setting_higher_order format type_sys then

   788              case (top_level, s) of

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

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

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

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

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

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

   795              | (false, s) =>

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

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

   798              | _ => (name, [])

   799            else

   800              (proxy_base |>> prefix const_prefix, T_args)

   801           | NONE => (name, T_args))

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

   803       | intro _ tm = tm

   804   in intro true end

   806 fun combformula_from_prop thy format type_sys eq_as_iff =

   807   let

   808     fun do_term bs t atomic_types =

   809       combterm_from_term thy bs (Envir.eta_contract t)

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

   811       ||> union (op =) atomic_types

   812     fun do_quant bs q s T t' =

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

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

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

   816       end

   817     and do_conn bs c t1 t2 =

   818       do_formula bs t1 ##>> do_formula bs t2

   819       #>> uncurry (mk_aconn c)

   820     and do_formula bs t =

   821       case t of

   822         @{const Trueprop} $ t1 => do_formula bs t1

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

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

   825         do_quant bs AForall s T t'

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

   827         do_quant bs AExists s T t'

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

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

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

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

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

   833       | _ => do_term bs t

   834   in do_formula [] end

   836 fun presimplify_term ctxt =

   837   Skip_Proof.make_thm (Proof_Context.theory_of ctxt)

   838   #> Meson.presimplify ctxt

   839   #> prop_of

   841 fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j

   842 fun conceal_bounds Ts t =

   843   subst_bounds (map (Free o apfst concealed_bound_name)

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

   845 fun reveal_bounds Ts =

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

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

   849 fun extensionalize_term ctxt t =

   850   let val thy = Proof_Context.theory_of ctxt in

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

   852       |> prop_of |> Logic.dest_equals |> snd

   853   end

   855 fun introduce_combinators_in_term ctxt kind t =

   856   let val thy = Proof_Context.theory_of ctxt in

   857     if Meson.is_fol_term thy t then

   858       t

   859     else

   860       let

   861         fun aux Ts t =

   862           case t of

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

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

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

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

   867             aux Ts (t0 $ eta_expand Ts t1 1)

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

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

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

   871             aux Ts (t0 $ eta_expand Ts t1 1)

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

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

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

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

   876               $ t1 $ t2 =>

   877             t0 $ aux Ts t1 $ aux Ts t2

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

   879                    t

   880                  else

   881                    t |> conceal_bounds Ts

   882                      |> Envir.eta_contract

   883                      |> cterm_of thy

   884                      |> Meson_Clausify.introduce_combinators_in_cterm

   885                      |> prop_of |> Logic.dest_equals |> snd

   886                      |> reveal_bounds Ts

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

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

   889       handle THM _ =>

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

   891              if kind = Conjecture then HOLogic.false_const

   892              else HOLogic.true_const

   893   end

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

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

   897 fun freeze_term t =

   898   let

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

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

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

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

   903       | aux t = t

   904   in t |> exists_subterm is_Var t ? aux end

   906 fun preprocess_prop ctxt presimp kind t =

   907   let

   908     val thy = Proof_Context.theory_of ctxt

   909     val t = t |> Envir.beta_eta_contract

   910               |> transform_elim_prop

   911               |> Object_Logic.atomize_term thy

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

   913   in

   914     t |> need_trueprop ? HOLogic.mk_Trueprop

   915       |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) []

   916       |> extensionalize_term ctxt

   917       |> presimp ? presimplify_term ctxt

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

   919       |> introduce_combinators_in_term ctxt kind

   920   end

   922 (* making fact and conjecture formulas *)

   923 fun make_formula thy format type_sys eq_as_iff name loc kind t =

   924   let

   925     val (combformula, atomic_types) =

   926       combformula_from_prop thy format type_sys eq_as_iff t []

   927   in

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

   929      atomic_types = atomic_types}

   930   end

   932 fun make_fact ctxt format type_sys keep_trivial eq_as_iff preproc presimp

   933               ((name, loc), t) =

   934   let val thy = Proof_Context.theory_of ctxt in

   935     case (keep_trivial,

   936           t |> preproc ? preprocess_prop ctxt presimp Axiom

   937             |> make_formula thy format type_sys eq_as_iff name loc Axiom) of

   938       (false,

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

   940       if s = tptp_true then NONE else SOME formula

   941     | (_, formula) => SOME formula

   942   end

   944 fun make_conjecture ctxt format prem_kind type_sys preproc ts =

   945   let

   946     val thy = Proof_Context.theory_of ctxt

   947     val last = length ts - 1

   948   in

   949     map2 (fn j => fn t =>

   950              let

   951                val (kind, maybe_negate) =

   952                  if j = last then

   953                    (Conjecture, I)

   954                  else

   955                    (prem_kind,

   956                     if prem_kind = Conjecture then update_combformula mk_anot

   957                     else I)

   958               in

   959                 t |> preproc ? (preprocess_prop ctxt true kind #> freeze_term)

   960                   |> make_formula thy format type_sys true (string_of_int j)

   961                                   General kind

   962                   |> maybe_negate

   963               end)

   964          (0 upto last) ts

   965   end

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

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

   970   | deep_freeze_atyp T = T

   971 val deep_freeze_type = map_atyps deep_freeze_atyp

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

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

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

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

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

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

   980   | should_encode_type _ _ All_Types _ = true

   981   | should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T

   982   | should_encode_type _ _ _ _ = false

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

   985                              should_predicate_on_var T =

   986     (heaviness = Heavy orelse should_predicate_on_var ()) andalso

   987     should_encode_type ctxt nonmono_Ts level T

   988   | should_predicate_on_type _ _ _ _ _ = false

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

   991     String.isPrefix bound_var_prefix s

   992   | is_var_or_bound_var (CombVar _) = true

   993   | is_var_or_bound_var _ = false

   995 datatype tag_site = Top_Level | Eq_Arg | Elsewhere

   997 fun should_tag_with_type _ _ _ Top_Level _ _ = false

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

   999     (case heaviness of

  1000        Heavy => should_encode_type ctxt nonmono_Ts level T

  1001      | Light =>

  1002        case (site, is_var_or_bound_var u) of

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

  1004        | _ => false)

  1005   | should_tag_with_type _ _ _ _ _ _ = false

  1007 fun homogenized_type ctxt nonmono_Ts level =

  1008   let

  1009     val should_encode = should_encode_type ctxt nonmono_Ts level

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

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

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

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

  1014   in homo end

  1016 (** "hBOOL" and "hAPP" **)

  1018 type sym_info =

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

  1021 fun add_combterm_syms_to_table ctxt explicit_apply =

  1022   let

  1023     fun consider_var_arity const_T var_T max_ary =

  1024       let

  1025         fun iter ary T =

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

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

  1028       in iter 0 const_T end

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

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

  1031         (case head of

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

  1033            if String.isPrefix bound_var_prefix s then

  1034              if explicit_apply = NONE andalso can dest_funT T then

  1035                let

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

  1037                    {pred_sym = pred_sym,

  1038                     min_ary =

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

  1040                     max_ary = max_ary, types = types}

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

  1042                in

  1043                  if pointer_eq (ho_var_Ts', ho_var_Ts) then accum

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

  1045                end

  1046              else

  1047                accum

  1048            else

  1049              let

  1050                val ary = length args

  1051              in

  1052                (ho_var_Ts,

  1053                 case Symtab.lookup sym_tab s of

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

  1055                   let

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

  1057                     val min_ary =

  1058                       if is_some explicit_apply orelse

  1059                          pointer_eq (types', types) then

  1060                         min_ary

  1061                       else

  1062                         fold (consider_var_arity T) ho_var_Ts min_ary

  1063                   in

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

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

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

  1067                                        types = types'})

  1068                                   sym_tab

  1069                   end

  1070                 | NONE =>

  1071                   let

  1072                     val min_ary =

  1073                       case explicit_apply of

  1074                         SOME true => 0

  1075                       | SOME false => ary

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

  1077                   in

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

  1079                                            min_ary = min_ary, max_ary = ary,

  1080                                            types = [T]})

  1081                                       sym_tab

  1082                   end)

  1083              end

  1084          | _ => accum)

  1085         |> fold (add false) args

  1086       end

  1087   in add true end

  1088 fun add_fact_syms_to_table ctxt explicit_apply =

  1089   fact_lift (formula_fold NONE

  1090                           (K (add_combterm_syms_to_table ctxt explicit_apply)))

  1092 val default_sym_table_entries : (string * sym_info) list =

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

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

  1095    (make_fixed_const predicator_name,

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

  1097   ([tptp_false, tptp_true]

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

  1100 fun sym_table_for_facts ctxt explicit_apply facts =

  1101   Symtab.empty

  1102   |> fold Symtab.default default_sym_table_entries

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

  1105 fun min_arity_of sym_tab s =

  1106   case Symtab.lookup sym_tab s of

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

  1108   | NONE =>

  1109     case strip_prefix_and_unascii const_prefix s of

  1110       SOME s =>

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

  1112         if s = predicator_name then 1

  1113         else if s = app_op_name then 2

  1114         else if s = type_pred_name then 1

  1115         else 0

  1116       end

  1117     | NONE => 0

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

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

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

  1122    arguments and is used as a predicate. *)

  1123 fun is_pred_sym sym_tab s =

  1124   case Symtab.lookup sym_tab s of

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

  1126     pred_sym andalso min_ary = max_ary

  1127   | NONE => false

  1129 val predicator_combconst =

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

  1131 fun predicator tm = CombApp (predicator_combconst, tm)

  1133 fun introduce_predicators_in_combterm sym_tab tm =

  1134   case strip_combterm_comb tm of

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

  1136     if is_pred_sym sym_tab s then tm else predicator tm

  1137   | _ => predicator tm

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

  1141 fun explicit_app arg head =

  1142   let

  1143     val head_T = combtyp_of head

  1144     val (arg_T, res_T) = dest_funT head_T

  1145     val explicit_app =

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

  1147                  [arg_T, res_T])

  1148   in list_app explicit_app [head, arg] end

  1149 fun list_explicit_app head args = fold explicit_app args head

  1151 fun introduce_explicit_apps_in_combterm sym_tab =

  1152   let

  1153     fun aux tm =

  1154       case strip_combterm_comb tm of

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

  1156         args |> map aux

  1157              |> chop (min_arity_of sym_tab s)

  1158              |>> list_app head

  1159              |-> list_explicit_app

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

  1161   in aux end

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

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

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

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

  1168 fun filter_type_args _ _ _ [] = []

  1169   | filter_type_args thy s arity T_args =

  1170     let

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

  1172       val U = if s = app_op_name then

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

  1174               else

  1175                 s |> Sign.the_const_type thy

  1176     in

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

  1178         [] => []

  1179       | res_U_vars =>

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

  1181           U_args ~~ T_args

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

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

  1184                               SOME T

  1185                             else

  1186                               NONE)

  1187         end

  1188     end

  1189     handle TYPE _ => T_args

  1191 fun enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys =

  1192   let

  1193     val thy = Proof_Context.theory_of ctxt

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

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

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

  1197         let

  1198           val level = level_of_type_sys type_sys

  1199           val (T, T_args) =

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

  1201                anyway, by distinguishing overloads only on the homogenized

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

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

  1204             if s = const_prefix ^ app_op_name andalso

  1205                length T_args = 2 andalso

  1206                not (is_type_sys_virtually_sound type_sys) andalso

  1207                heaviness_of_type_sys type_sys = Heavy then

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

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

  1210                                     (T --> T, tl Ts)

  1211                                   end)

  1212             else

  1213               (T, T_args)

  1214         in

  1215           (case strip_prefix_and_unascii const_prefix s of

  1216              NONE => (name, T_args)

  1217            | SOME s'' =>

  1218              let

  1219                val s'' = invert_const s''

  1220                fun filtered_T_args false = T_args

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

  1222              in

  1223                case type_arg_policy type_sys s'' of

  1224                  Explicit_Type_Args drop_args =>

  1225                  (name, filtered_T_args drop_args)

  1226                | Mangled_Type_Args drop_args =>

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

  1228                | No_Type_Args => (name, [])

  1229              end)

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

  1231         end

  1232       | aux _ tm = tm

  1233   in aux 0 end

  1235 fun repair_combterm ctxt format nonmono_Ts type_sys sym_tab =

  1236   not (is_setting_higher_order format type_sys)

  1237   ? (introduce_explicit_apps_in_combterm sym_tab

  1238      #> introduce_predicators_in_combterm sym_tab)

  1239   #> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys

  1240 fun repair_fact ctxt format nonmono_Ts type_sys sym_tab =

  1241   update_combformula (formula_map

  1242       (repair_combterm ctxt format nonmono_Ts type_sys sym_tab))

  1244 (** Helper facts **)

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

  1247 val helper_table =

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

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

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

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

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

  1253    ("fequal",

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

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

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

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

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

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

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

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

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

  1263    ("fNot",

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

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

  1266    ("fconj",

  1267     (false,

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

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

  1270    ("fdisj",

  1271     (false,

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

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

  1274    ("fimplies",

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

  1276                     "~ fimplies P Q | ~ P | Q"

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

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

  1280 fun ti_ti_helper_fact () =

  1281   let

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

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

  1284   in

  1285     Formula (helper_prefix ^ "ti_ti", Axiom,

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

  1287              |> close_formula_universally, simp_info, NONE)

  1288   end

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

  1291   case strip_prefix_and_unascii const_prefix s of

  1292     SOME mangled_s =>

  1293     let

  1294       val thy = Proof_Context.theory_of ctxt

  1295       val unmangled_s = mangled_s |> unmangled_const_name

  1296       fun dub_and_inst c needs_fairly_sound (th, j) =

  1297         ((c ^ "_" ^ string_of_int j ^

  1298           (if needs_fairly_sound then typed_helper_suffix

  1299            else untyped_helper_suffix),

  1300           General),

  1301          let val t = th |> prop_of in

  1302            t |> ((case general_type_arg_policy type_sys of

  1303                     Mangled_Type_Args _ => true

  1304                   | _ => false) andalso

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

  1306                 ? (case types of

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

  1308                    | _ => I)

  1309          end)

  1310       fun make_facts eq_as_iff =

  1311         map_filter (make_fact ctxt format type_sys true false eq_as_iff false)

  1312       val fairly_sound = is_type_sys_fairly_sound type_sys

  1313     in

  1314       helper_table

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

  1316                   if metis_s <> unmangled_s orelse

  1317                      (needs_fairly_sound andalso not fairly_sound) then

  1318                     []

  1319                   else

  1320                     ths ~~ (1 upto length ths)

  1321                     |> map (dub_and_inst mangled_s needs_fairly_sound)

  1322                     |> make_facts (not needs_fairly_sound))

  1323     end

  1324   | NONE => []

  1325 fun helper_facts_for_sym_table ctxt format type_sys sym_tab =

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

  1327                   []

  1329 fun translate_atp_fact ctxt format type_sys keep_trivial =

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

  1332 (***************************************************************)

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

  1334 (***************************************************************)

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

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

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

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

  1343 fun classes_of_terms get_Ts =

  1344   map (map snd o get_Ts)

  1345   #> List.foldl add_classes Symtab.empty

  1346   #> delete_type #> Symtab.keys

  1348 val tfree_classes_of_terms = classes_of_terms OldTerm.term_tfrees

  1349 val tvar_classes_of_terms = classes_of_terms OldTerm.term_tvars

  1351 (*fold type constructors*)

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

  1353   | fold_type_consts _ _ x = x

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

  1356 fun add_type_consts_in_term thy =

  1357   let

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

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

  1360       | aux (Const x) =

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

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

  1363       | aux _ = I

  1364   in aux end

  1366 fun type_consts_of_terms thy ts =

  1367   Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty)

  1369 fun translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t

  1370                        rich_facts =

  1371   let

  1372     val thy = Proof_Context.theory_of ctxt

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

  1374     val (facts, fact_names) =

  1375       rich_facts

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

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

  1378       |> ListPair.unzip

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

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

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

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

  1383     val all_ts = goal_t :: fact_ts

  1384     val subs = tfree_classes_of_terms all_ts

  1385     val supers = tvar_classes_of_terms all_ts

  1386     val tycons = type_consts_of_terms thy all_ts

  1387     val conjs =

  1388       hyp_ts @ [concl_t]

  1389       |> make_conjecture ctxt format prem_kind type_sys preproc

  1390     val (supers', arity_clauses) =

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

  1392       else make_arity_clauses thy tycons supers

  1393     val class_rel_clauses = make_class_rel_clauses thy subs supers'

  1394   in

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

  1396   end

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

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

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

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

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

  1405 fun type_pred_combterm ctxt nonmono_Ts type_sys T tm =

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

  1407            |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys,

  1408            tm)

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

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

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

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

  1414   | is_var_nonmonotonic_in_formula pos phi _ name =

  1415     formula_fold pos (var_occurs_positively_naked_in_term name) phi false

  1417 fun mk_const_aterm x T_args args =

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

  1420 fun tag_with_type ctxt format nonmono_Ts type_sys T tm =

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

  1422   |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys

  1423   |> term_from_combterm ctxt format nonmono_Ts type_sys Top_Level

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

  1425 and term_from_combterm ctxt format nonmono_Ts type_sys =

  1426   let

  1427     fun aux site u =

  1428       let

  1429         val (head, args) = strip_combterm_comb u

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

  1431           case head of

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

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

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

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

  1436                        else Elsewhere

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

  1438         val T = combtyp_of u

  1439       in

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

  1441                 tag_with_type ctxt format nonmono_Ts type_sys T

  1442               else

  1443                 I)

  1444       end

  1445   in aux end

  1446 and formula_from_combformula ctxt format nonmono_Ts type_sys

  1447                              should_predicate_on_var =

  1448   let

  1449     val higher_order = is_setting_higher_order format type_sys

  1450     val do_term = term_from_combterm ctxt format nonmono_Ts type_sys Top_Level

  1451     val do_bound_type =

  1452       case type_sys of

  1453         Simple_Types level =>

  1454         homogenized_type ctxt nonmono_Ts level 0

  1455         #> mangled_type higher_order false 0 #> SOME

  1456       | _ => K NONE

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

  1458       if should_predicate_on_type ctxt nonmono_Ts type_sys

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

  1460         CombVar (name, T)

  1461         |> type_pred_combterm ctxt nonmono_Ts type_sys T

  1462         |> do_term |> AAtom |> SOME

  1463       else

  1464         NONE

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

  1466         let

  1467           val phi = phi |> do_formula pos

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

  1469         in

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

  1471                                         | SOME T => do_bound_type T)),

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

  1473                       (map_filter

  1474                            (fn (_, NONE) => NONE

  1475                              | (s, SOME T) =>

  1476                                do_out_of_bound_type pos phi universal (s, T))

  1477                            xs)

  1478                       phi)

  1479         end

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

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

  1482   in do_formula o SOME end

  1484 fun bound_tvars type_sys Ts =

  1485   mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)

  1486                 (type_literals_for_types type_sys sorts_on_tvar Ts))

  1488 fun formula_for_fact ctxt format nonmono_Ts type_sys

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

  1490   combformula

  1491   |> close_combformula_universally

  1492   |> formula_from_combformula ctxt format nonmono_Ts type_sys

  1493                               is_var_nonmonotonic_in_formula true

  1494   |> bound_tvars type_sys atomic_types

  1495   |> close_formula_universally

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

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

  1499    the remote provers might care. *)

  1500 fun formula_line_for_fact ctxt format prefix nonmono_Ts type_sys

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

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

  1503                      else string_of_int j ^ "_") ^

  1504            ascii_of name,

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

  1506            case locality of

  1507              Intro => intro_info

  1508            | Elim => elim_info

  1509            | Simp => simp_info

  1510            | _ => NONE)

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

  1513                                        : class_rel_clause) =

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

  1515     Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,

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

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

  1518              |> close_formula_universally, intro_info, NONE)

  1519   end

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

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

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

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

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

  1527                                    : arity_clause) =

  1528   Formula (arity_clause_prefix ^ ascii_of name, Axiom,

  1529            mk_ahorn (map (formula_from_fo_literal o apfst not

  1530                           o fo_literal_from_arity_literal) prem_lits)

  1531                     (formula_from_fo_literal

  1532                          (fo_literal_from_arity_literal concl_lits))

  1533            |> close_formula_universally, intro_info, NONE)

  1535 fun formula_line_for_conjecture ctxt format nonmono_Ts type_sys

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

  1537   Formula (conjecture_prefix ^ name, kind,

  1538            formula_from_combformula ctxt format nonmono_Ts type_sys

  1539                is_var_nonmonotonic_in_formula false

  1540                (close_combformula_universally combformula)

  1541            |> bound_tvars type_sys atomic_types

  1542            |> close_formula_universally, NONE, NONE)

  1544 fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) =

  1545   atomic_types |> type_literals_for_types type_sys sorts_on_tfree

  1546                |> map fo_literal_from_type_literal

  1548 fun formula_line_for_free_type j lit =

  1549   Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,

  1550            formula_from_fo_literal lit, NONE, NONE)

  1551 fun formula_lines_for_free_types type_sys facts =

  1552   let

  1553     val litss = map (free_type_literals type_sys) facts

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

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

  1557 (** Symbol declarations **)

  1559 fun should_declare_sym type_sys pred_sym s =

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

  1561   (case type_sys of

  1562      Simple_Types _ => true

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

  1564    | _ => not pred_sym)

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

  1567   let

  1568     fun add_combterm in_conj tm =

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

  1570         (case head of

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

  1572            let val pred_sym = is_pred_sym repaired_sym_tab s in

  1573              if should_declare_sym type_sys pred_sym s then

  1574                Symtab.map_default (s, [])

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

  1576                                          in_conj))

  1577              else

  1578                I

  1579            end

  1580          | _ => I)

  1581         #> fold (add_combterm in_conj) args

  1582       end

  1583     fun add_fact in_conj =

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

  1585   in

  1586     Symtab.empty

  1587     |> is_type_sys_fairly_sound type_sys

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

  1589   end

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

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

  1593 val known_infinite_types =

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

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

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

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

  1599   | add_combterm_nonmonotonic_types ctxt level _

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

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

  1602      (case level of

  1603         Nonmonotonic_Types =>

  1604         not (is_type_surely_infinite ctxt known_infinite_types T)

  1605       | Finite_Types => is_type_surely_finite ctxt T

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

  1607   | add_combterm_nonmonotonic_types _ _ _ _ = I

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

  1609                                             : translated_formula) =

  1610   formula_fold (SOME (kind <> Conjecture))

  1611                (add_combterm_nonmonotonic_types ctxt level) combformula

  1612 fun nonmonotonic_types_for_facts ctxt type_sys facts =

  1613   let val level = level_of_type_sys type_sys in

  1614     if level = Nonmonotonic_Types orelse level = Finite_Types then

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

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

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

  1618             nonmonotonic types not being empty. *)

  1619          |> insert_type ctxt I @{typ bool}

  1620     else

  1621       []

  1622   end

  1624 fun decl_line_for_sym ctxt format nonmono_Ts type_sys s

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

  1626   let

  1627     val (higher_order, T_arg_Ts, level) =

  1628       case type_sys of

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

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

  1631   in

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

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

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

  1635   end

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

  1639 fun formula_line_for_preds_sym_decl ctxt format conj_sym_kind nonmono_Ts

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

  1641   let

  1642     val (kind, maybe_negate) =

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

  1644       else (Axiom, I)

  1645     val (arg_Ts, res_T) = chop_fun ary T

  1646     val bound_names =

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

  1648     val bounds =

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

  1650     val bound_Ts =

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

  1652                              else NONE)

  1653   in

  1654     Formula (preds_sym_formula_prefix ^ s ^

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

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

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

  1658              |> type_pred_combterm ctxt nonmono_Ts type_sys res_T

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

  1660              |> formula_from_combformula ctxt format nonmono_Ts type_sys

  1661                                          (K (K (K (K true)))) true

  1662              |> n > 1 ? bound_tvars type_sys (atyps_of T)

  1663              |> close_formula_universally

  1664              |> maybe_negate,

  1665              intro_info, NONE)

  1666   end

  1668 fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind nonmono_Ts

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

  1670   let

  1671     val ident_base =

  1672       tags_sym_formula_prefix ^ s ^

  1673       (if n > 1 then "_" ^ string_of_int j else "")

  1674     val (kind, maybe_negate) =

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

  1676       else (Axiom, I)

  1677     val (arg_Ts, res_T) = chop_fun ary T

  1678     val bound_names =

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

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

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

  1682     val atomic_Ts = atyps_of T

  1683     fun eq tms =

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

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

  1686       |> bound_tvars type_sys atomic_Ts

  1687       |> close_formula_universally

  1688       |> maybe_negate

  1689     val should_encode = should_encode_type ctxt nonmono_Ts All_Types

  1690     val tag_with = tag_with_type ctxt format nonmono_Ts type_sys

  1691     val add_formula_for_res =

  1692       if should_encode res_T then

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

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

  1695                        simp_info, NONE))

  1696       else

  1697         I

  1698     fun add_formula_for_arg k =

  1699       let val arg_T = nth arg_Ts k in

  1700         if should_encode arg_T then

  1701           case chop k bounds of

  1702             (bounds1, bound :: bounds2) =>

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

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

  1705                                cst bounds],

  1706                            simp_info, NONE))

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

  1708         else

  1709           I

  1710       end

  1711   in

  1712     [] |> not pred_sym ? add_formula_for_res

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

  1714   end

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

  1718 fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts type_sys

  1719                                 (s, decls) =

  1720   case type_sys of

  1721     Simple_Types _ =>

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

  1723   | Preds _ =>

  1724     let

  1725       val decls =

  1726         case decls of

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

  1728           let val T = result_type_of_decl decl in

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

  1730                        o result_type_of_decl) decls' then

  1731               [decl]

  1732             else

  1733               decls

  1734           end

  1735         | _ => decls

  1736       val n = length decls

  1737       val decls =

  1738         decls

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

  1740                    o result_type_of_decl)

  1741     in

  1742       (0 upto length decls - 1, decls)

  1743       |-> map2 (formula_line_for_preds_sym_decl ctxt format conj_sym_kind

  1744                                                 nonmono_Ts type_sys n s)

  1745     end

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

  1747     (case heaviness of

  1748        Heavy => []

  1749      | Light =>

  1750        let val n = length decls in

  1751          (0 upto n - 1 ~~ decls)

  1752          |> maps (formula_lines_for_tags_sym_decl ctxt format conj_sym_kind

  1753                                                   nonmono_Ts type_sys n s)

  1754        end)

  1756 fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts

  1757                                      type_sys sym_decl_tab =

  1758   sym_decl_tab

  1759   |> Symtab.dest

  1760   |> sort_wrt fst

  1761   |> rpair []

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

  1763                                                      nonmono_Ts type_sys)

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

  1766     level = Nonmonotonic_Types orelse level = Finite_Types

  1767   | should_add_ti_ti_helper _ = false

  1769 fun offset_of_heading_in_problem _ [] j = j

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

  1771     if heading = needle then j

  1772     else offset_of_heading_in_problem needle problem (j + length lines)

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

  1775 val explicit_declsN = "Explicit typings"

  1776 val factsN = "Relevant facts"

  1777 val class_relsN = "Class relationships"

  1778 val aritiesN = "Arities"

  1779 val helpersN = "Helper facts"

  1780 val conjsN = "Conjectures"

  1781 val free_typesN = "Type variables"

  1783 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys

  1784                         explicit_apply readable_names preproc hyp_ts concl_t

  1785                         facts =

  1786   let

  1787     val (format, type_sys) = choose_format [format] type_sys

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

  1789       translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t

  1790                          facts

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

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

  1793     val repair = repair_fact ctxt format nonmono_Ts type_sys sym_tab

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

  1795     val repaired_sym_tab =

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

  1797     val helpers =

  1798       repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_sys

  1799                        |> map repair

  1800     val lavish_nonmono_Ts =

  1801       if null nonmono_Ts orelse

  1802          polymorphism_of_type_sys type_sys <> Polymorphic then

  1803         nonmono_Ts

  1804       else

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

  1806     val sym_decl_lines =

  1807       (conjs, helpers @ facts)

  1808       |> sym_decl_table_for_facts ctxt type_sys repaired_sym_tab

  1809       |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind

  1810                                           lavish_nonmono_Ts type_sys

  1811     val helper_lines =

  1812       0 upto length helpers - 1 ~~ helpers

  1813       |> map (formula_line_for_fact ctxt format helper_prefix lavish_nonmono_Ts

  1814                                     type_sys)

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

  1816           else I)

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

  1818        FLOTTER hack. *)

  1819     val problem =

  1820       [(explicit_declsN, sym_decl_lines),

  1821        (factsN,

  1822         map (formula_line_for_fact ctxt format fact_prefix nonmono_Ts type_sys)

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

  1824        (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),

  1825        (aritiesN, map formula_line_for_arity_clause arity_clauses),

  1826        (helpersN, helper_lines),

  1827        (conjsN,

  1828         map (formula_line_for_conjecture ctxt format nonmono_Ts type_sys)

  1829             conjs),

  1830        (free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))]

  1831     val problem =

  1832       problem

  1833       |> (case format of

  1834             CNF => ensure_cnf_problem

  1835           | CNF_UEQ => filter_cnf_ueq_problem

  1836           | _ => I)

  1837       |> (if is_format_typed format then

  1838             declare_undeclared_syms_in_atp_problem type_decl_prefix

  1839                                                    implicit_declsN

  1840           else

  1841             I)

  1842     val (problem, pool) = problem |> nice_atp_problem readable_names

  1843     val helpers_offset = offset_of_heading_in_problem helpersN problem 0

  1844     val typed_helpers =

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

  1846                      if String.isSuffix typed_helper_suffix name then SOME j

  1847                      else NONE)

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

  1849                   ~~ helpers)

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

  1851       if min_ary > 0 then

  1852         case strip_prefix_and_unascii const_prefix s of

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

  1854         | NONE => I

  1855       else

  1856         I

  1857   in

  1858     (problem,

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

  1860      offset_of_heading_in_problem conjsN problem 0,

  1861      offset_of_heading_in_problem factsN problem 0,

  1862      fact_names |> Vector.fromList,

  1863      typed_helpers,

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

  1865   end

  1867 (* FUDGE *)

  1868 val conj_weight = 0.0

  1869 val hyp_weight = 0.1

  1870 val fact_min_weight = 0.2

  1871 val fact_max_weight = 1.0

  1872 val type_info_default_weight = 0.8

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

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

  1876   #> fold (add_term_weights weight) tms

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

  1878     formula_fold NONE (K (add_term_weights weight)) phi

  1879   | add_problem_line_weights _ _ = I

  1881 fun add_conjectures_weights [] = I

  1882   | add_conjectures_weights conjs =

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

  1884       add_problem_line_weights conj_weight conj

  1885       #> fold (add_problem_line_weights hyp_weight) hyps

  1886     end

  1888 fun add_facts_weights facts =

  1889   let

  1890     val num_facts = length facts

  1891     fun weight_of j =

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

  1893                         / Real.fromInt num_facts

  1894   in

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

  1896     |> fold (uncurry add_problem_line_weights)

  1897   end

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

  1900 fun atp_problem_weights problem =

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

  1902     Symtab.empty

  1903     |> add_conjectures_weights (get free_typesN @ get conjsN)

  1904     |> add_facts_weights (get factsN)

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

  1906             [explicit_declsN, class_relsN, aritiesN]

  1907     |> Symtab.dest

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

  1909   end

  1911 end;

author	blanchet
	Wed, 01 Jun 2011 10:29:43 +0200
changeset 43966	ddf63baabdec
parent 43962	5df3777f376d
child 43969	a19826080596
permissions	-rw-r--r--