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

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

    56   val bound_var_prefix : string

    57   val schematic_var_prefix: string

    58   val fixed_var_prefix: string

    59   val tvar_prefix: string

    60   val tfree_prefix: string

    61   val const_prefix: string

    62   val type_const_prefix: string

    63   val class_prefix: string

    64   val skolem_const_prefix : string

    65   val old_skolem_const_prefix : string

    66   val new_skolem_const_prefix : string

    67   val fact_prefix : string

    68   val conjecture_prefix : string

    69   val helper_prefix : string

    70   val typed_helper_suffix : string

    71   val predicator_name : string

    72   val app_op_name : string

    73   val type_pred_name : string

    74   val simple_type_prefix : string

    75   val ascii_of: string -> string

    76   val unascii_of: string -> string

    77   val strip_prefix_and_unascii : string -> string -> string option

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

    79   val invert_const: string -> string

    80   val unproxify_const: string -> string

    81   val make_bound_var : string -> string

    82   val make_schematic_var : string * int -> string

    83   val make_fixed_var : string -> string

    84   val make_schematic_type_var : string * int -> string

    85   val make_fixed_type_var : string -> string

    86   val make_fixed_const : string -> string

    87   val make_fixed_type_const : string -> string

    88   val make_type_class : string -> string

    89   val new_skolem_var_name_from_const : string -> string

    90   val num_type_args : theory -> string -> int

    91   val make_arity_clauses :

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

    93   val make_class_rel_clauses :

    94     theory -> class list -> class list -> class_rel_clause list

    95   val combtyp_of : combterm -> typ

    96   val strip_combterm_comb : combterm -> combterm * combterm list

    97   val atyps_of : typ -> typ list

    98   val combterm_from_term :

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

   100   val is_locality_global : locality -> bool

   101   val type_sys_from_string : string -> type_system

   102   val polymorphism_of_type_sys : type_system -> polymorphism

   103   val level_of_type_sys : type_system -> type_level

   104   val is_type_sys_virtually_sound : type_system -> bool

   105   val is_type_sys_fairly_sound : type_system -> bool

   106   val choose_format : format list -> type_system -> format * type_system

   107   val raw_type_literals_for_types : typ list -> type_literal list

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

   109   val translate_atp_fact :

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

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

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

   113   val tfree_classes_of_terms : term list -> string list

   114   val tvar_classes_of_terms : term list -> string list

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

   116   val prepare_atp_problem :

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

   118     -> bool option -> bool -> bool -> term list -> term

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

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

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

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

   123 end;

   125 structure ATP_Translate : ATP_TRANSLATE =

   126 struct

   128 open ATP_Util

   129 open ATP_Problem

   131 type name = string * string

   133 (* FIXME: avoid *)

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

   136 (* experimental *)

   137 val generate_useful_info = false

   139 fun useful_isabelle_info s =

   140   if generate_useful_info then

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

   142   else

   143     NONE

   145 val intro_info = useful_isabelle_info "intro"

   146 val elim_info = useful_isabelle_info "elim"

   147 val simp_info = useful_isabelle_info "simp"

   149 val type_tag_name = "ti"

   151 val bound_var_prefix = "B_"

   152 val schematic_var_prefix = "V_"

   153 val fixed_var_prefix = "v_"

   155 val tvar_prefix = "T_"

   156 val tfree_prefix = "t_"

   158 val const_prefix = "c_"

   159 val type_const_prefix = "tc_"

   160 val class_prefix = "cl_"

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

   163 val old_skolem_const_prefix = skolem_const_prefix ^ "o"

   164 val new_skolem_const_prefix = skolem_const_prefix ^ "n"

   166 val type_decl_prefix = "ty_"

   167 val sym_decl_prefix = "sy_"

   168 val sym_formula_prefix = "sym_"

   169 val fact_prefix = "fact_"

   170 val conjecture_prefix = "conj_"

   171 val helper_prefix = "help_"

   172 val class_rel_clause_prefix = "crel_"

   173 val arity_clause_prefix = "arity_"

   174 val tfree_clause_prefix = "tfree_"

   176 val typed_helper_suffix = "_T"

   177 val untyped_helper_suffix = "_U"

   179 val predicator_name = "hBOOL"

   180 val app_op_name = "hAPP"

   181 val type_pred_name = "is"

   182 val simple_type_prefix = "ty_"

   184 (* Freshness almost guaranteed! *)

   185 val sledgehammer_weak_prefix = "Sledgehammer:"

   187 (*Escaping of special characters.

   188   Alphanumeric characters are left unchanged.

   189   The character _ goes to __

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

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

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

   194 fun stringN_of_int 0 _ = ""

   195   | stringN_of_int k n =

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

   198 fun ascii_of_char c =

   199   if Char.isAlphaNum c then

   200     String.str c

   201   else if c = #"_" then

   202     "__"

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

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

   205   else

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

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

   209 val ascii_of = String.translate ascii_of_char

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

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

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

   215 val unascii_of =

   216   let

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

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

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

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

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

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

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

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

   225         else

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

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

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

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

   230           end

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

   232   in un [] o String.explode end

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

   235    un-ASCII'd. *)

   236 fun strip_prefix_and_unascii s1 s =

   237   if String.isPrefix s1 s then

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

   239   else

   240     NONE

   242 val proxies =

   243   [("c_False",

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

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

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

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

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

   249    ("c_implies",

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

   251    ("equal",

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

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

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

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

   258 val const_trans_table =

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   275   |> Symtab.make

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

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

   279 val const_trans_table_inv =

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

   281 val const_trans_table_unprox =

   282   Symtab.empty

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

   285 val invert_const = perhaps (Symtab.lookup const_trans_table_inv)

   286 val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)

   288 fun lookup_const c =

   289   case Symtab.lookup const_trans_table c of

   290     SOME c' => c'

   291   | NONE => ascii_of c

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

   294 fun trim_type_var s =

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

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

   298 fun ascii_of_indexname (v,0) = ascii_of v

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

   301 fun make_bound_var x = bound_var_prefix ^ ascii_of x

   302 fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v

   303 fun make_fixed_var x = fixed_var_prefix ^ ascii_of x

   305 fun make_schematic_type_var (x,i) =

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

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

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

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

   311   | make_fixed_const c = const_prefix ^ lookup_const c

   313 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c

   315 fun make_type_class clas = class_prefix ^ ascii_of clas

   317 fun new_skolem_var_name_from_const s =

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

   319     nth ss (length ss - 2)

   320   end

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

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

   324    constant name. *)

   325 fun num_type_args thy s =

   326   if String.isPrefix skolem_const_prefix s then

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

   328   else

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

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

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

   334 datatype type_literal =

   335   TyLitVar of name * name |

   336   TyLitFree of name * name

   339 (** Isabelle arities **)

   341 datatype arity_literal =

   342   TConsLit of name * name * name list |

   343   TVarLit of name * name

   345 fun gen_TVars 0 = []

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

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

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

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

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

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

   354 type arity_clause =

   355   {name: string,

   356    prem_lits: arity_literal list,

   357    concl_lits: arity_literal}

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

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

   361   let

   362     val tvars = gen_TVars (length args)

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

   364   in

   365     {name = name,

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

   367      concl_lits = TConsLit (`make_type_class cls,

   368                             `make_fixed_type_const tcons,

   369                             tvars ~~ tvars)}

   370   end

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

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

   374       arity_clause seen n (tcons,ars)

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

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

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

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

   379       else

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

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

   383 fun multi_arity_clause [] = []

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

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

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

   388   provided its arguments have the corresponding sorts.*)

   389 fun type_class_pairs thy tycons classes =

   390   let

   391     val alg = Sign.classes_of thy

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

   393     fun add_class tycon class =

   394       cons (class, domain_sorts tycon class)

   395       handle Sorts.CLASS_ERROR _ => I

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

   397   in map try_classes tycons end

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

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

   401   | iter_type_class_pairs thy tycons classes =

   402       let val cpairs = type_class_pairs thy tycons classes

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

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

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

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

   408 fun make_arity_clauses thy tycons =

   409   iter_type_class_pairs thy tycons ##> multi_arity_clause

   412 (** Isabelle class relations **)

   414 type class_rel_clause =

   415   {name: string,

   416    subclass: name,

   417    superclass: name}

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

   420 fun class_pairs _ [] _ = []

   421   | class_pairs thy subs supers =

   422       let

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

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

   425         fun add_supers sub = fold (add_super sub) supers

   426       in fold add_supers subs [] end

   428 fun make_class_rel_clause (sub,super) =

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

   430    subclass = `make_type_class sub,

   431    superclass = `make_type_class super}

   433 fun make_class_rel_clauses thy subs supers =

   434   map make_class_rel_clause (class_pairs thy subs supers)

   436 datatype combterm =

   437   CombConst of name * typ * typ list |

   438   CombVar of name * typ |

   439   CombApp of combterm * combterm

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

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

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

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

   446 fun strip_combterm_comb u =

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

   448         |   stripc  x =  x

   449     in stripc(u,[]) end

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

   453 fun new_skolem_const_name s num_T_args =

   454   [new_skolem_const_prefix, s, string_of_int num_T_args]

   455   |> space_implode Long_Name.separator

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

   458    infomation. *)

   459 fun combterm_from_term thy bs (P $ Q) =

   460     let

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

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

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

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

   465     let

   466       val tvar_list =

   467         (if String.isPrefix old_skolem_const_prefix c then

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

   469          else

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

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

   472     in (c', atyps_of T) end

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

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

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

   476     (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then

   477        let

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

   479          val s' = new_skolem_const_name s (length Ts)

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

   481      else

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

   483   | combterm_from_term _ bs (Bound j) =

   484     nth bs j

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

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

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

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

   491 fun is_locality_global Local = false

   492   | is_locality_global Assum = false

   493   | is_locality_global Chained = false

   494   | is_locality_global _ = true

   496 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic

   497 datatype type_level =

   498   All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types

   499 datatype type_heaviness = Heavy | Light

   501 datatype type_system =

   502   Simple_Types of type_level |

   503   Preds of polymorphism * type_level * type_heaviness |

   504   Tags of polymorphism * type_level * type_heaviness

   506 fun try_unsuffixes ss s =

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

   509 fun type_sys_from_string s =

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

   511      SOME s => (SOME Polymorphic, s)

   512    | NONE =>

   513      case try (unprefix "mono_") s of

   514        SOME s => (SOME Monomorphic, s)

   515      | NONE =>

   516        case try (unprefix "mangled_") s of

   517          SOME s => (SOME Mangled_Monomorphic, s)

   518        | NONE => (NONE, s))

   519   ||> (fn s =>

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

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

   522             SOME s => (Nonmonotonic_Types, s)

   523           | NONE =>

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

   525               SOME s => (Finite_Types, s)

   526             | NONE => (All_Types, s))

   527   ||> apsnd (fn s =>

   528                 case try (unsuffix "_heavy") s of

   529                   SOME s => (Heavy, s)

   530                 | NONE => (Light, s))

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

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

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

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

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

   536            Tags (Polymorphic, All_Types, heaviness)

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

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

   539            Tags (Polymorphic, level, Heavy)

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

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

   542            Preds (poly, Const_Arg_Types, Light)

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

   544            Preds (Polymorphic, No_Types, Light)

   545          | _ => raise Same.SAME)

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

   548 fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic

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

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

   552 fun level_of_type_sys (Simple_Types level) = level

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

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

   556 fun heaviness_of_type_sys (Simple_Types _) = Heavy

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

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

   560 fun is_type_level_virtually_sound level =

   561   level = All_Types orelse level = Nonmonotonic_Types

   562 val is_type_sys_virtually_sound =

   563   is_type_level_virtually_sound o level_of_type_sys

   565 fun is_type_level_fairly_sound level =

   566   is_type_level_virtually_sound level orelse level = Finite_Types

   567 val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys

   569 fun is_setting_higher_order THF (Simple_Types _) = true

   570   | is_setting_higher_order _ _ = false

   572 fun choose_format formats (Simple_Types level) =

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

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

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

   576   | choose_format formats type_sys =

   577     (case hd formats of

   578        CNF_UEQ =>

   579        (CNF_UEQ, case type_sys of

   580                    Preds stuff =>

   581                    (if is_type_sys_fairly_sound type_sys then Preds else Tags)

   582                        stuff

   583                  | _ => type_sys)

   584      | format => (format, type_sys))

   586 type translated_formula =

   587   {name: string,

   588    locality: locality,

   589    kind: formula_kind,

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

   591    atomic_types: typ list}

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

   594                           : translated_formula) =

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

   596    atomic_types = atomic_types} : translated_formula

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

   600 val type_instance = Sign.typ_instance o Proof_Context.theory_of

   602 fun insert_type ctxt get_T x xs =

   603   let val T = get_T x in

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

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

   606   end

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

   609 datatype type_arg_policy =

   610   Explicit_Type_Args of bool |

   611   Mangled_Type_Args of bool |

   612   No_Type_Args

   614 fun should_drop_arg_type_args (Simple_Types _) =

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

   616   | should_drop_arg_type_args type_sys =

   617     level_of_type_sys type_sys = All_Types andalso

   618     heaviness_of_type_sys type_sys = Heavy

   620 fun general_type_arg_policy type_sys =

   621   if level_of_type_sys type_sys = No_Types then

   622     No_Type_Args

   623   else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then

   624     Mangled_Type_Args (should_drop_arg_type_args type_sys)

   625   else

   626     Explicit_Type_Args (should_drop_arg_type_args type_sys)

   628 fun type_arg_policy type_sys s =

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

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

   631     No_Type_Args

   632   else

   633     general_type_arg_policy type_sys

   635 (*Make literals for sorted type variables*)

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

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

   638     generic_sorts_on_type ((x, i), ss)

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

   640           I

   641         else if i = ~1 then

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

   643         else

   644           cons (TyLitVar (`make_type_class s,

   645                           (make_schematic_type_var (x, i), x))))

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

   647   | sorts_on_tfree _ = []

   648 fun sorts_on_tvar (TVar z) = generic_sorts_on_type z

   649   | sorts_on_tvar _ = []

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

   652 fun raw_type_literals_for_types Ts =

   653   union_all (map sorts_on_tfree Ts @ map sorts_on_tvar Ts)

   655 fun type_literals_for_types type_sys sorts_on_typ Ts =

   656   if level_of_type_sys type_sys = No_Types then []

   657   else union_all (map sorts_on_typ Ts)

   659 fun mk_aconns c phis =

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

   661     fold_rev (mk_aconn c) phis' phi'

   662   end

   663 fun mk_ahorn [] phi = phi

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

   665 fun mk_aquant _ [] phi = phi

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

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

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

   670 fun close_universally atom_vars phi =

   671   let

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

   673         formula_vars (map fst xs @ bounds) phi

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

   675       | formula_vars bounds (AAtom tm) =

   676         union (op =) (atom_vars tm []

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

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

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

   681   | combterm_vars (CombConst _) = I

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

   683 fun close_combformula_universally phi = close_universally combterm_vars phi

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

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

   687 fun close_formula_universally phi = close_universally term_vars phi

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

   690 val homo_infinite_type = Type (homo_infinite_type_name, [])

   692 fun fo_term_from_typ higher_order =

   693   let

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

   695       ATerm (case (higher_order, s) of

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

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

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

   699                     else `make_fixed_type_const s,

   700              map term Ts)

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

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

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

   704   in term end

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

   707 val mangled_type_sep = "\000"

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

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

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

   712     ^ ")"

   714 val bool_atype = AType (`I tptp_bool_type)

   716 fun make_simple_type s =

   717   if s = tptp_bool_type orelse s = tptp_fun_type orelse

   718      s = tptp_individual_type then

   719     s

   720   else

   721     simple_type_prefix ^ ascii_of s

   723 fun ho_type_from_fo_term higher_order pred_sym ary =

   724   let

   725     fun to_atype ty =

   726       AType ((make_simple_type (generic_mangled_type_name fst ty),

   727               generic_mangled_type_name snd ty))

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

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

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

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

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

   733   in if higher_order then to_ho else to_fo ary end

   735 fun mangled_type higher_order pred_sym ary =

   736   ho_type_from_fo_term higher_order pred_sym ary o fo_term_from_typ higher_order

   738 fun mangled_const_name T_args (s, s') =

   739   let

   740     val ty_args = map (fo_term_from_typ false) T_args

   741     fun type_suffix f g =

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

   743                 o generic_mangled_type_name f) ty_args ""

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

   746 val parse_mangled_ident =

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

   749 fun parse_mangled_type x =

   750   (parse_mangled_ident

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

   752                     [] >> ATerm) x

   753 and parse_mangled_types x =

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

   756 fun unmangled_type s =

   757   s |> suffix ")" |> raw_explode

   758     |> Scan.finite Symbol.stopper

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

   760                                                 quote s)) parse_mangled_type))

   761     |> fst

   763 val unmangled_const_name = space_explode mangled_type_sep #> hd

   764 fun unmangled_const s =

   765   let val ss = space_explode mangled_type_sep s in

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

   767   end

   769 fun introduce_proxies format type_sys =

   770   let

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

   772         CombApp (intro top_level tm1, intro false tm2)

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

   774         (case proxify_const s of

   775            SOME (_, proxy_base) =>

   776            if top_level orelse is_setting_higher_order format type_sys then

   777              case (top_level, s) of

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

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

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

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

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

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

   784              | (false, s) =>

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

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

   787              | _ => (name, [])

   788            else

   789              (proxy_base |>> prefix const_prefix, T_args)

   790           | NONE => (name, T_args))

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

   792       | intro _ tm = tm

   793   in intro true end

   795 fun combformula_from_prop thy format type_sys eq_as_iff =

   796   let

   797     fun do_term bs t atomic_types =

   798       combterm_from_term thy bs (Envir.eta_contract t)

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

   800       ||> union (op =) atomic_types

   801     fun do_quant bs q s T t' =

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

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

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

   805       end

   806     and do_conn bs c t1 t2 =

   807       do_formula bs t1 ##>> do_formula bs t2

   808       #>> uncurry (mk_aconn c)

   809     and do_formula bs t =

   810       case t of

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

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

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

   814         do_quant bs AForall s T t'

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

   816         do_quant bs AExists s T t'

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

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

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

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

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

   822       | _ => do_term bs t

   823   in do_formula [] end

   825 fun presimplify_term ctxt =

   826   Skip_Proof.make_thm (Proof_Context.theory_of ctxt)

   827   #> Meson.presimplify ctxt

   828   #> prop_of

   830 fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j

   831 fun conceal_bounds Ts t =

   832   subst_bounds (map (Free o apfst concealed_bound_name)

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

   834 fun reveal_bounds Ts =

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

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

   838 fun extensionalize_term ctxt t =

   839   let val thy = Proof_Context.theory_of ctxt in

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

   841       |> prop_of |> Logic.dest_equals |> snd

   842   end

   844 fun introduce_combinators_in_term ctxt kind t =

   845   let val thy = Proof_Context.theory_of ctxt in

   846     if Meson.is_fol_term thy t then

   847       t

   848     else

   849       let

   850         fun aux Ts t =

   851           case t of

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

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

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

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

   856             aux Ts (t0 $ eta_expand Ts t1 1)

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

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

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

   860             aux Ts (t0 $ eta_expand Ts t1 1)

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

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

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

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

   865               $ t1 $ t2 =>

   866             t0 $ aux Ts t1 $ aux Ts t2

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

   868                    t

   869                  else

   870                    t |> conceal_bounds Ts

   871                      |> Envir.eta_contract

   872                      |> cterm_of thy

   873                      |> Meson_Clausify.introduce_combinators_in_cterm

   874                      |> prop_of |> Logic.dest_equals |> snd

   875                      |> reveal_bounds Ts

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

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

   878       handle THM _ =>

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

   880              if kind = Conjecture then HOLogic.false_const

   881              else HOLogic.true_const

   882   end

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

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

   886 fun freeze_term t =

   887   let

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

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

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

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

   892       | aux t = t

   893   in t |> exists_subterm is_Var t ? aux end

   895 fun preprocess_prop ctxt presimp kind t =

   896   let

   897     val thy = Proof_Context.theory_of ctxt

   898     val t = t |> Envir.beta_eta_contract

   899               |> transform_elim_prop

   900               |> Object_Logic.atomize_term thy

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

   902   in

   903     t |> need_trueprop ? HOLogic.mk_Trueprop

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

   905       |> extensionalize_term ctxt

   906       |> presimp ? presimplify_term ctxt

   907       |> introduce_combinators_in_term ctxt kind

   908   end

   910 (* making fact and conjecture formulas *)

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

   912   let

   913     val (combformula, atomic_types) =

   914       combformula_from_prop thy format type_sys eq_as_iff t []

   915   in

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

   917      atomic_types = atomic_types}

   918   end

   920 fun make_fact ctxt format type_sys keep_trivial eq_as_iff preproc presimp

   921               ((name, loc), t) =

   922   let val thy = Proof_Context.theory_of ctxt in

   923     case (keep_trivial,

   924           t |> preproc ? preprocess_prop ctxt presimp Axiom

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

   926       (false,

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

   928       if s = tptp_true then NONE else SOME formula

   929     | (_, formula) => SOME formula

   930   end

   932 fun make_conjecture ctxt format prem_kind type_sys preproc ts =

   933   let

   934     val thy = Proof_Context.theory_of ctxt

   935     val last = length ts - 1

   936   in

   937     map2 (fn j => fn t =>

   938              let

   939                val (kind, maybe_negate) =

   940                  if j = last then

   941                    (Conjecture, I)

   942                  else

   943                    (prem_kind,

   944                     if prem_kind = Conjecture then update_combformula mk_anot

   945                     else I)

   946               in

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

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

   949                                   General kind

   950                   |> maybe_negate

   951               end)

   952          (0 upto last) ts

   953   end

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

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

   958   | deep_freeze_atyp T = T

   959 val deep_freeze_type = map_atyps deep_freeze_atyp

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

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

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

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

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

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

   968   | should_encode_type _ _ All_Types _ = true

   969   | should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T

   970   | should_encode_type _ _ _ _ = false

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

   973                              should_predicate_on_var T =

   974     (heaviness = Heavy orelse should_predicate_on_var ()) andalso

   975     should_encode_type ctxt nonmono_Ts level T

   976   | should_predicate_on_type _ _ _ _ _ = false

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

   979     String.isPrefix bound_var_prefix s

   980   | is_var_or_bound_var (CombVar _) = true

   981   | is_var_or_bound_var _ = false

   983 datatype tag_site = Top_Level | Eq_Arg | Elsewhere

   985 fun should_tag_with_type _ _ _ Top_Level _ _ = false

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

   987     (case heaviness of

   988        Heavy => should_encode_type ctxt nonmono_Ts level T

   989      | Light =>

   990        case (site, is_var_or_bound_var u) of

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

   992        | _ => false)

   993   | should_tag_with_type _ _ _ _ _ _ = false

   995 fun homogenized_type ctxt nonmono_Ts level =

   996   let

   997     val should_encode = should_encode_type ctxt nonmono_Ts level

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

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

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

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

  1002   in homo end

  1004 (** "hBOOL" and "hAPP" **)

  1006 type sym_info =

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

  1009 fun add_combterm_syms_to_table ctxt explicit_apply =

  1010   let

  1011     fun consider_var_arity const_T var_T max_ary =

  1012       let

  1013         fun iter ary T =

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

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

  1016       in iter 0 const_T end

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

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

  1019         (case head of

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

  1021            if String.isPrefix bound_var_prefix s then

  1022              if explicit_apply = NONE andalso can dest_funT T then

  1023                let

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

  1025                    {pred_sym = pred_sym,

  1026                     min_ary =

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

  1028                     max_ary = max_ary, types = types}

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

  1030                in

  1031                  if pointer_eq (ho_var_Ts', ho_var_Ts) then accum

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

  1033                end

  1034              else

  1035                accum

  1036            else

  1037              let

  1038                val ary = length args

  1039              in

  1040                (ho_var_Ts,

  1041                 case Symtab.lookup sym_tab s of

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

  1043                   let

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

  1045                     val min_ary =

  1046                       if is_some explicit_apply orelse

  1047                          pointer_eq (types', types) then

  1048                         min_ary

  1049                       else

  1050                         fold (consider_var_arity T) ho_var_Ts min_ary

  1051                   in

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

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

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

  1055                                        types = types'})

  1056                                   sym_tab

  1057                   end

  1058                 | NONE =>

  1059                   let

  1060                     val min_ary =

  1061                       case explicit_apply of

  1062                         SOME true => 0

  1063                       | SOME false => ary

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

  1065                   in

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

  1067                                            min_ary = min_ary, max_ary = ary,

  1068                                            types = [T]})

  1069                                       sym_tab

  1070                   end)

  1071              end

  1072          | _ => accum)

  1073         |> fold (add false) args

  1074       end

  1075   in add true end

  1076 fun add_fact_syms_to_table ctxt explicit_apply =

  1077   fact_lift (formula_fold NONE

  1078                           (K (add_combterm_syms_to_table ctxt explicit_apply)))

  1080 val default_sym_table_entries : (string * sym_info) list =

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

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

  1083    (make_fixed_const predicator_name,

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

  1085   ([tptp_false, tptp_true]

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

  1088 fun sym_table_for_facts ctxt explicit_apply facts =

  1089   Symtab.empty

  1090   |> fold Symtab.default default_sym_table_entries

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

  1093 fun min_arity_of sym_tab s =

  1094   case Symtab.lookup sym_tab s of

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

  1096   | NONE =>

  1097     case strip_prefix_and_unascii const_prefix s of

  1098       SOME s =>

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

  1100         if s = predicator_name then 1

  1101         else if s = app_op_name then 2

  1102         else if s = type_pred_name then 1

  1103         else 0

  1104       end

  1105     | NONE => 0

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

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

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

  1110    arguments and is used as a predicate. *)

  1111 fun is_pred_sym sym_tab s =

  1112   case Symtab.lookup sym_tab s of

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

  1114     pred_sym andalso min_ary = max_ary

  1115   | NONE => false

  1117 val predicator_combconst =

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

  1119 fun predicator tm = CombApp (predicator_combconst, tm)

  1121 fun introduce_predicators_in_combterm sym_tab tm =

  1122   case strip_combterm_comb tm of

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

  1124     if is_pred_sym sym_tab s then tm else predicator tm

  1125   | _ => predicator tm

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

  1129 fun explicit_app arg head =

  1130   let

  1131     val head_T = combtyp_of head

  1132     val (arg_T, res_T) = dest_funT head_T

  1133     val explicit_app =

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

  1135                  [arg_T, res_T])

  1136   in list_app explicit_app [head, arg] end

  1137 fun list_explicit_app head args = fold explicit_app args head

  1139 fun introduce_explicit_apps_in_combterm sym_tab =

  1140   let

  1141     fun aux tm =

  1142       case strip_combterm_comb tm of

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

  1144         args |> map aux

  1145              |> chop (min_arity_of sym_tab s)

  1146              |>> list_app head

  1147              |-> list_explicit_app

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

  1149   in aux end

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

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

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

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

  1156 fun filter_type_args _ _ _ [] = []

  1157   | filter_type_args thy s arity T_args =

  1158     let

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

  1160       val U = if s = app_op_name then

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

  1162               else

  1163                 s |> Sign.the_const_type thy

  1164     in

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

  1166         [] => []

  1167       | res_U_vars =>

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

  1169           U_args ~~ T_args

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

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

  1172                               SOME T

  1173                             else

  1174                               NONE)

  1175         end

  1176     end

  1177     handle TYPE _ => T_args

  1179 fun enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys =

  1180   let

  1181     val thy = Proof_Context.theory_of ctxt

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

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

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

  1185         let

  1186           val level = level_of_type_sys type_sys

  1187           val (T, T_args) =

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

  1189                anyway, by distinguishing overloads only on the homogenized

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

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

  1192             if s = const_prefix ^ app_op_name andalso

  1193                length T_args = 2 andalso

  1194                not (is_type_sys_virtually_sound type_sys) andalso

  1195                heaviness_of_type_sys type_sys = Heavy then

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

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

  1198                                     (T --> T, tl Ts)

  1199                                   end)

  1200             else

  1201               (T, T_args)

  1202         in

  1203           (case strip_prefix_and_unascii const_prefix s of

  1204              NONE => (name, T_args)

  1205            | SOME s'' =>

  1206              let

  1207                val s'' = invert_const s''

  1208                fun filtered_T_args false = T_args

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

  1210              in

  1211                case type_arg_policy type_sys s'' of

  1212                  Explicit_Type_Args drop_args =>

  1213                  (name, filtered_T_args drop_args)

  1214                | Mangled_Type_Args drop_args =>

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

  1216                | No_Type_Args => (name, [])

  1217              end)

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

  1219         end

  1220       | aux _ tm = tm

  1221   in aux 0 end

  1223 fun repair_combterm ctxt format nonmono_Ts type_sys sym_tab =

  1224   not (is_setting_higher_order format type_sys)

  1225   ? (introduce_explicit_apps_in_combterm sym_tab

  1226      #> introduce_predicators_in_combterm sym_tab)

  1227   #> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys

  1228 fun repair_fact ctxt format nonmono_Ts type_sys sym_tab =

  1229   update_combformula (formula_map

  1230       (repair_combterm ctxt format nonmono_Ts type_sys sym_tab))

  1232 (** Helper facts **)

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

  1235 val helper_table =

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

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

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

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

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

  1241    ("fequal",

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

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

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

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

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

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

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

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

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

  1251    ("fNot",

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

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

  1254    ("fconj",

  1255     (false,

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

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

  1258    ("fdisj",

  1259     (false,

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

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

  1262    ("fimplies",

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

  1264                     "~ fimplies P Q | ~ P | Q"

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

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

  1268 fun ti_ti_helper_fact () =

  1269   let

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

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

  1272   in

  1273     Formula (helper_prefix ^ "ti_ti", Axiom,

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

  1275              |> close_formula_universally, simp_info, NONE)

  1276   end

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

  1279   case strip_prefix_and_unascii const_prefix s of

  1280     SOME mangled_s =>

  1281     let

  1282       val thy = Proof_Context.theory_of ctxt

  1283       val unmangled_s = mangled_s |> unmangled_const_name

  1284       fun dub_and_inst c needs_fairly_sound (th, j) =

  1285         ((c ^ "_" ^ string_of_int j ^

  1286           (if needs_fairly_sound then typed_helper_suffix

  1287            else untyped_helper_suffix),

  1288           General),

  1289          let val t = th |> prop_of in

  1290            t |> ((case general_type_arg_policy type_sys of

  1291                     Mangled_Type_Args _ => true

  1292                   | _ => false) andalso

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

  1294                 ? (case types of

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

  1296                    | _ => I)

  1297          end)

  1298       fun make_facts eq_as_iff =

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

  1300       val fairly_sound = is_type_sys_fairly_sound type_sys

  1301     in

  1302       helper_table

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

  1304                   if metis_s <> unmangled_s orelse

  1305                      (needs_fairly_sound andalso not fairly_sound) then

  1306                     []

  1307                   else

  1308                     ths ~~ (1 upto length ths)

  1309                     |> map (dub_and_inst mangled_s needs_fairly_sound)

  1310                     |> make_facts (not needs_fairly_sound))

  1311     end

  1312   | NONE => []

  1313 fun helper_facts_for_sym_table ctxt format type_sys sym_tab =

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

  1315                   []

  1317 fun translate_atp_fact ctxt format type_sys keep_trivial =

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

  1320 (***************************************************************)

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

  1322 (***************************************************************)

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

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

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

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

  1331 fun classes_of_terms get_Ts =

  1332   map (map #2 o get_Ts)

  1333   #> List.foldl add_classes Symtab.empty

  1334   #> delete_type #> Symtab.keys

  1336 val tfree_classes_of_terms = classes_of_terms OldTerm.term_tfrees

  1337 val tvar_classes_of_terms = classes_of_terms OldTerm.term_tvars

  1339 (*fold type constructors*)

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

  1341   | fold_type_consts _ _ x = x

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

  1344 fun add_type_consts_in_term thy =

  1345   let

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

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

  1348       | aux (Const x) =

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

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

  1351       | aux _ = I

  1352   in aux end

  1354 fun type_consts_of_terms thy ts =

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

  1357 fun translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t

  1358                        rich_facts =

  1359   let

  1360     val thy = Proof_Context.theory_of ctxt

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

  1362     val (facts, fact_names) =

  1363       rich_facts

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

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

  1366       |> ListPair.unzip

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

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

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

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

  1371     val all_ts = goal_t :: fact_ts

  1372     val subs = tfree_classes_of_terms all_ts

  1373     val supers = tvar_classes_of_terms all_ts

  1374     val tycons = type_consts_of_terms thy all_ts

  1375     val conjs =

  1376       hyp_ts @ [concl_t]

  1377       |> make_conjecture ctxt format prem_kind type_sys preproc

  1378     val (supers', arity_clauses) =

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

  1380       else make_arity_clauses thy tycons supers

  1381     val class_rel_clauses = make_class_rel_clauses thy subs supers'

  1382   in

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

  1384   end

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

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

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

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

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

  1393 fun type_pred_combterm ctxt nonmono_Ts type_sys T tm =

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

  1395            |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys,

  1396            tm)

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

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

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

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

  1402   | is_var_nonmonotonic_in_formula pos phi _ name =

  1403     formula_fold pos (var_occurs_positively_naked_in_term name) phi false

  1405 fun mk_const_aterm x T_args args =

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

  1408 fun tag_with_type ctxt format nonmono_Ts type_sys T tm =

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

  1410   |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys

  1411   |> term_from_combterm ctxt format nonmono_Ts type_sys Top_Level

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

  1413 and term_from_combterm ctxt format nonmono_Ts type_sys =

  1414   let

  1415     fun aux site u =

  1416       let

  1417         val (head, args) = strip_combterm_comb u

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

  1419           case head of

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

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

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

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

  1424                        else Elsewhere

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

  1426         val T = combtyp_of u

  1427       in

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

  1429                 tag_with_type ctxt format nonmono_Ts type_sys T

  1430               else

  1431                 I)

  1432       end

  1433   in aux end

  1434 and formula_from_combformula ctxt format nonmono_Ts type_sys

  1435                              should_predicate_on_var =

  1436   let

  1437     val higher_order = is_setting_higher_order format type_sys

  1438     val do_term = term_from_combterm ctxt format nonmono_Ts type_sys Top_Level

  1439     val do_bound_type =

  1440       case type_sys of

  1441         Simple_Types level =>

  1442         homogenized_type ctxt nonmono_Ts level 0

  1443         #> mangled_type higher_order false 0 #> SOME

  1444       | _ => K NONE

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

  1446       if should_predicate_on_type ctxt nonmono_Ts type_sys

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

  1448         CombVar (name, T)

  1449         |> type_pred_combterm ctxt nonmono_Ts type_sys T

  1450         |> do_term |> AAtom |> SOME

  1451       else

  1452         NONE

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

  1454         let

  1455           val phi = phi |> do_formula pos

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

  1457         in

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

  1459                                         | SOME T => do_bound_type T)),

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

  1461                       (map_filter

  1462                            (fn (_, NONE) => NONE

  1463                              | (s, SOME T) =>

  1464                                do_out_of_bound_type pos phi universal (s, T))

  1465                            xs)

  1466                       phi)

  1467         end

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

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

  1470   in do_formula o SOME end

  1472 fun bound_tvars type_sys Ts =

  1473   mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)

  1474                 (type_literals_for_types type_sys sorts_on_tvar Ts))

  1476 fun formula_for_fact ctxt format nonmono_Ts type_sys

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

  1478   combformula

  1479   |> close_combformula_universally

  1480   |> formula_from_combformula ctxt format nonmono_Ts type_sys

  1481                               is_var_nonmonotonic_in_formula true

  1482   |> bound_tvars type_sys atomic_types

  1483   |> close_formula_universally

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

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

  1487    the remote provers might care. *)

  1488 fun formula_line_for_fact ctxt format prefix nonmono_Ts type_sys

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

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

  1491                      else string_of_int j ^ "_") ^

  1492            ascii_of name,

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

  1494            case locality of

  1495              Intro => intro_info

  1496            | Elim => elim_info

  1497            | Simp => simp_info

  1498            | _ => NONE)

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

  1501                                        : class_rel_clause) =

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

  1503     Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,

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

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

  1506              |> close_formula_universally, intro_info, NONE)

  1507   end

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

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

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

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

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

  1515                                    : arity_clause) =

  1516   Formula (arity_clause_prefix ^ ascii_of name, Axiom,

  1517            mk_ahorn (map (formula_from_fo_literal o apfst not

  1518                           o fo_literal_from_arity_literal) prem_lits)

  1519                     (formula_from_fo_literal

  1520                          (fo_literal_from_arity_literal concl_lits))

  1521            |> close_formula_universally, intro_info, NONE)

  1523 fun formula_line_for_conjecture ctxt format nonmono_Ts type_sys

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

  1525   Formula (conjecture_prefix ^ name, kind,

  1526            formula_from_combformula ctxt format nonmono_Ts type_sys

  1527                is_var_nonmonotonic_in_formula false

  1528                (close_combformula_universally combformula)

  1529            |> bound_tvars type_sys atomic_types

  1530            |> close_formula_universally, NONE, NONE)

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

  1533   atomic_types |> type_literals_for_types type_sys sorts_on_tfree

  1534                |> map fo_literal_from_type_literal

  1536 fun formula_line_for_free_type j lit =

  1537   Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,

  1538            formula_from_fo_literal lit, NONE, NONE)

  1539 fun formula_lines_for_free_types type_sys facts =

  1540   let

  1541     val litss = map (free_type_literals type_sys) facts

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

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

  1545 (** Symbol declarations **)

  1547 fun should_declare_sym type_sys pred_sym s =

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

  1549   (case type_sys of

  1550      Simple_Types _ => true

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

  1552    | _ => not pred_sym)

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

  1555   let

  1556     fun add_combterm in_conj tm =

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

  1558         (case head of

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

  1560            let val pred_sym = is_pred_sym repaired_sym_tab s in

  1561              if should_declare_sym type_sys pred_sym s then

  1562                Symtab.map_default (s, [])

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

  1564                                          in_conj))

  1565              else

  1566                I

  1567            end

  1568          | _ => I)

  1569         #> fold (add_combterm in_conj) args

  1570       end

  1571     fun add_fact in_conj =

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

  1573   in

  1574     Symtab.empty

  1575     |> is_type_sys_fairly_sound type_sys

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

  1577   end

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

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

  1581 val known_infinite_types =

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

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

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

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

  1587   | add_combterm_nonmonotonic_types ctxt level _

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

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

  1590      (case level of

  1591         Nonmonotonic_Types =>

  1592         not (is_type_surely_infinite ctxt known_infinite_types T)

  1593       | Finite_Types => is_type_surely_finite ctxt T

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

  1595   | add_combterm_nonmonotonic_types _ _ _ _ = I

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

  1597                                             : translated_formula) =

  1598   formula_fold (SOME (kind <> Conjecture))

  1599                (add_combterm_nonmonotonic_types ctxt level) combformula

  1600 fun nonmonotonic_types_for_facts ctxt type_sys facts =

  1601   let val level = level_of_type_sys type_sys in

  1602     if level = Nonmonotonic_Types orelse level = Finite_Types then

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

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

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

  1606             nonmonotonic types not being empty. *)

  1607          |> insert_type ctxt I @{typ bool}

  1608     else

  1609       []

  1610   end

  1612 fun decl_line_for_sym ctxt format nonmono_Ts type_sys s

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

  1614   let

  1615     val (higher_order, T_arg_Ts, level) =

  1616       case type_sys of

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

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

  1619   in

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

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

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

  1623   end

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

  1627 fun formula_line_for_pred_sym_decl ctxt format conj_sym_kind nonmono_Ts type_sys

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

  1629   let

  1630     val (kind, maybe_negate) =

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

  1632       else (Axiom, I)

  1633     val (arg_Ts, res_T) = chop_fun ary T

  1634     val bound_names =

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

  1636     val bounds =

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

  1638     val bound_Ts =

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

  1640                              else NONE)

  1641   in

  1642     Formula (sym_formula_prefix ^ s ^

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

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

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

  1646              |> type_pred_combterm ctxt nonmono_Ts type_sys res_T

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

  1648              |> formula_from_combformula ctxt format nonmono_Ts type_sys

  1649                                          (K (K (K (K true)))) true

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

  1651              |> close_formula_universally

  1652              |> maybe_negate,

  1653              intro_info, NONE)

  1654   end

  1656 fun formula_lines_for_tag_sym_decl ctxt format conj_sym_kind nonmono_Ts type_sys

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

  1658   let

  1659     val ident_base =

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

  1661     val (kind, maybe_negate) =

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

  1663       else (Axiom, I)

  1664     val (arg_Ts, res_T) = chop_fun ary T

  1665     val bound_names =

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

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

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

  1669     val atomic_Ts = atyps_of T

  1670     fun eq tms =

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

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

  1673       |> bound_tvars type_sys atomic_Ts

  1674       |> close_formula_universally

  1675       |> maybe_negate

  1676     val should_encode = should_encode_type ctxt nonmono_Ts All_Types

  1677     val tag_with = tag_with_type ctxt format nonmono_Ts type_sys

  1678     val add_formula_for_res =

  1679       if should_encode res_T then

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

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

  1682                        simp_info, NONE))

  1683       else

  1684         I

  1685     fun add_formula_for_arg k =

  1686       let val arg_T = nth arg_Ts k in

  1687         if should_encode arg_T then

  1688           case chop k bounds of

  1689             (bounds1, bound :: bounds2) =>

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

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

  1692                                cst bounds],

  1693                            simp_info, NONE))

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

  1695         else

  1696           I

  1697       end

  1698   in

  1699     [] |> not pred_sym ? add_formula_for_res

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

  1701   end

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

  1705 fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts type_sys

  1706                                 (s, decls) =

  1707   case type_sys of

  1708     Simple_Types _ =>

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

  1710   | Preds _ =>

  1711     let

  1712       val decls =

  1713         case decls of

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

  1715           let val T = result_type_of_decl decl in

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

  1717                        o result_type_of_decl) decls' then

  1718               [decl]

  1719             else

  1720               decls

  1721           end

  1722         | _ => decls

  1723       val n = length decls

  1724       val decls =

  1725         decls

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

  1727                    o result_type_of_decl)

  1728     in

  1729       (0 upto length decls - 1, decls)

  1730       |-> map2 (formula_line_for_pred_sym_decl ctxt format conj_sym_kind

  1731                                                nonmono_Ts type_sys n s)

  1732     end

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

  1734     (case heaviness of

  1735        Heavy => []

  1736      | Light =>

  1737        let val n = length decls in

  1738          (0 upto n - 1 ~~ decls)

  1739          |> maps (formula_lines_for_tag_sym_decl ctxt format conj_sym_kind

  1740                                                  nonmono_Ts type_sys n s)

  1741        end)

  1743 fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts

  1744                                      type_sys sym_decl_tab =

  1745   sym_decl_tab

  1746   |> Symtab.dest

  1747   |> sort_wrt fst

  1748   |> rpair []

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

  1750                                                      nonmono_Ts type_sys)

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

  1753     level = Nonmonotonic_Types orelse level = Finite_Types

  1754   | should_add_ti_ti_helper _ = false

  1756 fun offset_of_heading_in_problem _ [] j = j

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

  1758     if heading = needle then j

  1759     else offset_of_heading_in_problem needle problem (j + length lines)

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

  1762 val explicit_declsN = "Explicit typings"

  1763 val factsN = "Relevant facts"

  1764 val class_relsN = "Class relationships"

  1765 val aritiesN = "Arities"

  1766 val helpersN = "Helper facts"

  1767 val conjsN = "Conjectures"

  1768 val free_typesN = "Type variables"

  1770 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys

  1771                         explicit_apply readable_names preproc hyp_ts concl_t

  1772                         facts =

  1773   let

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

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

  1776       translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t

  1777                          facts

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

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

  1780     val repair = repair_fact ctxt format nonmono_Ts type_sys sym_tab

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

  1782     val repaired_sym_tab =

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

  1784     val helpers =

  1785       repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_sys

  1786                        |> map repair

  1787     val lavish_nonmono_Ts =

  1788       if null nonmono_Ts orelse

  1789          polymorphism_of_type_sys type_sys <> Polymorphic then

  1790         nonmono_Ts

  1791       else

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

  1793     val sym_decl_lines =

  1794       (conjs, helpers @ facts)

  1795       |> sym_decl_table_for_facts ctxt type_sys repaired_sym_tab

  1796       |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind

  1797                                           lavish_nonmono_Ts type_sys

  1798     val helper_lines =

  1799       0 upto length helpers - 1 ~~ helpers

  1800       |> map (formula_line_for_fact ctxt format helper_prefix lavish_nonmono_Ts

  1801                                     type_sys)

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

  1803           else I)

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

  1805        FLOTTER hack. *)

  1806     val problem =

  1807       [(explicit_declsN, sym_decl_lines),

  1808        (factsN,

  1809         map (formula_line_for_fact ctxt format fact_prefix nonmono_Ts type_sys)

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

  1811        (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),

  1812        (aritiesN, map formula_line_for_arity_clause arity_clauses),

  1813        (helpersN, helper_lines),

  1814        (conjsN,

  1815         map (formula_line_for_conjecture ctxt format nonmono_Ts type_sys)

  1816             conjs),

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

  1818     val problem =

  1819       problem

  1820       |> (case format of

  1821             CNF => ensure_cnf_problem

  1822           | CNF_UEQ => filter_cnf_ueq_problem

  1823           | _ => I)

  1824       |> (if is_format_typed format then

  1825             declare_undeclared_syms_in_atp_problem type_decl_prefix

  1826                                                    implicit_declsN

  1827           else

  1828             I)

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

  1830     val helpers_offset = offset_of_heading_in_problem helpersN problem 0

  1831     val typed_helpers =

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

  1833                      if String.isSuffix typed_helper_suffix name then SOME j

  1834                      else NONE)

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

  1836                   ~~ helpers)

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

  1838       if min_ary > 0 then

  1839         case strip_prefix_and_unascii const_prefix s of

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

  1841         | NONE => I

  1842       else

  1843         I

  1844   in

  1845     (problem,

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

  1847      offset_of_heading_in_problem conjsN problem 0,

  1848      offset_of_heading_in_problem factsN problem 0,

  1849      fact_names |> Vector.fromList,

  1850      typed_helpers,

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

  1852   end

  1854 (* FUDGE *)

  1855 val conj_weight = 0.0

  1856 val hyp_weight = 0.1

  1857 val fact_min_weight = 0.2

  1858 val fact_max_weight = 1.0

  1859 val type_info_default_weight = 0.8

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

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

  1863   #> fold (add_term_weights weight) tms

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

  1865     formula_fold NONE (K (add_term_weights weight)) phi

  1866   | add_problem_line_weights _ _ = I

  1868 fun add_conjectures_weights [] = I

  1869   | add_conjectures_weights conjs =

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

  1871       add_problem_line_weights conj_weight conj

  1872       #> fold (add_problem_line_weights hyp_weight) hyps

  1873     end

  1875 fun add_facts_weights facts =

  1876   let

  1877     val num_facts = length facts

  1878     fun weight_of j =

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

  1880                         / Real.fromInt num_facts

  1881   in

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

  1883     |> fold (uncurry add_problem_line_weights)

  1884   end

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

  1887 fun atp_problem_weights problem =

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

  1889     Symtab.empty

  1890     |> add_conjectures_weights (get free_typesN @ get conjsN)

  1891     |> add_facts_weights (get factsN)

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

  1893             [explicit_declsN, class_relsN, aritiesN]

  1894     |> Symtab.dest

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

  1896   end

  1898 end;

author	blanchet
	Tue, 31 May 2011 16:38:36 +0200
changeset 43942	1d46d85cd78b
parent 43939	e88e974c4846
child 43943	9a42899ec169
permissions	-rw-r--r--