wneuper/isa: src/HOL/Tools/ATP/atp_problem.ML@8d8d3c1f1854

     1 (*  Title:      HOL/Tools/ATP/atp_problem.ML

     2     Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA

     3     Author:     Jasmin Blanchette, TU Muenchen

     5 Abstract representation of ATP problems and TPTP syntax.

     6 *)

     8 signature ATP_PROBLEM =

     9 sig

    10   datatype ('a, 'b) ho_term =

    11     ATerm of 'a * ('a, 'b) ho_term list |

    12     AAbs of ('a * 'b) * ('a, 'b) ho_term

    13   datatype quantifier = AForall | AExists

    14   datatype connective = ANot | AAnd | AOr | AImplies | AIff

    15   datatype ('a, 'b, 'c) formula =

    16     AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c) formula |

    17     AConn of connective * ('a, 'b, 'c) formula list |

    18     AAtom of 'c

    20   datatype 'a ho_type =

    21     AType of 'a * 'a ho_type list |

    22     AFun of 'a ho_type * 'a ho_type |

    23     ATyAbs of 'a list * 'a ho_type

    25   datatype tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic

    26   datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit

    27   datatype thf_flavor = THF_Without_Choice | THF_With_Choice

    28   datatype dfg_flavor = DFG_Unsorted | DFG_Sorted

    30   datatype atp_format =

    31     CNF |

    32     CNF_UEQ |

    33     FOF |

    34     TFF of tptp_polymorphism * tptp_explicitness |

    35     THF of tptp_polymorphism * tptp_explicitness * thf_flavor |

    36     DFG of dfg_flavor

    38   datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture

    39   datatype 'a problem_line =

    40     Decl of string * 'a * 'a ho_type |

    41     Formula of string * formula_kind

    42                * ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula

    43                * (string, string ho_type) ho_term option

    44                * (string, string ho_type) ho_term option

    45   type 'a problem = (string * 'a problem_line list) list

    47   val isabelle_info_prefix : string

    48   val isabelle_info : atp_format -> string -> (string, 'a) ho_term option

    49   val introN : string

    50   val elimN : string

    51   val simpN : string

    52   val eqN : string

    53   val tptp_cnf : string

    54   val tptp_fof : string

    55   val tptp_tff : string

    56   val tptp_thf : string

    57   val tptp_has_type : string

    58   val tptp_type_of_types : string

    59   val tptp_bool_type : string

    60   val tptp_individual_type : string

    61   val tptp_fun_type : string

    62   val tptp_product_type : string

    63   val tptp_forall : string

    64   val tptp_ho_forall : string

    65   val tptp_pi_binder : string

    66   val tptp_exists : string

    67   val tptp_ho_exists : string

    68   val tptp_choice : string

    69   val tptp_not : string

    70   val tptp_and : string

    71   val tptp_or : string

    72   val tptp_implies : string

    73   val tptp_if : string

    74   val tptp_iff : string

    75   val tptp_not_iff : string

    76   val tptp_app : string

    77   val tptp_not_infix : string

    78   val tptp_equal : string

    79   val tptp_old_equal : string

    80   val tptp_false : string

    81   val tptp_true : string

    82   val tptp_empty_list : string

    83   val is_tptp_equal : string -> bool

    84   val is_built_in_tptp_symbol : string -> bool

    85   val is_tptp_variable : string -> bool

    86   val is_tptp_user_symbol : string -> bool

    87   val atype_of_types : (string * string) ho_type

    88   val bool_atype : (string * string) ho_type

    89   val individual_atype : (string * string) ho_type

    90   val mk_anot : ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula

    91   val mk_aconn :

    92     connective -> ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula

    93     -> ('a, 'b, 'c) formula

    94   val aconn_fold :

    95     bool option -> (bool option -> 'a -> 'b -> 'b) -> connective * 'a list

    96     -> 'b -> 'b

    97   val aconn_map :

    98     bool option -> (bool option -> 'a -> ('b, 'c, 'd) formula)

    99     -> connective * 'a list -> ('b, 'c, 'd) formula

   100   val formula_fold :

   101     bool option -> (bool option -> 'c -> 'd -> 'd) -> ('a, 'b, 'c) formula

   102     -> 'd -> 'd

   103   val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula

   104   val is_format_higher_order : atp_format -> bool

   105   val is_format_typed : atp_format -> bool

   106   val lines_for_atp_problem : atp_format -> string problem -> string list

   107   val ensure_cnf_problem :

   108     (string * string) problem -> (string * string) problem

   109   val filter_cnf_ueq_problem :

   110     (string * string) problem -> (string * string) problem

   111   val declared_syms_in_problem : (string * ''a) problem -> (string * ''a) list

   112   val nice_atp_problem :

   113     bool -> atp_format -> ('a * (string * string) problem_line list) list

   114     -> ('a * string problem_line list) list

   115        * (string Symtab.table * string Symtab.table) option

   116 end;

   118 structure ATP_Problem : ATP_PROBLEM =

   119 struct

   121 open ATP_Util

   124 (** ATP problem **)

   126 datatype ('a, 'b) ho_term =

   127   ATerm of 'a * ('a, 'b) ho_term list |

   128   AAbs of ('a * 'b) * ('a, 'b) ho_term

   129 datatype quantifier = AForall | AExists

   130 datatype connective = ANot | AAnd | AOr | AImplies | AIff

   131 datatype ('a, 'b, 'c) formula =

   132   AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c) formula |

   133   AConn of connective * ('a, 'b, 'c) formula list |

   134   AAtom of 'c

   136 datatype 'a ho_type =

   137   AType of 'a * 'a ho_type list |

   138   AFun of 'a ho_type * 'a ho_type |

   139   ATyAbs of 'a list * 'a ho_type

   141 datatype tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic

   142 datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit

   143 datatype thf_flavor = THF_Without_Choice | THF_With_Choice

   144 datatype dfg_flavor = DFG_Unsorted | DFG_Sorted

   146 datatype atp_format =

   147   CNF |

   148   CNF_UEQ |

   149   FOF |

   150   TFF of tptp_polymorphism * tptp_explicitness |

   151   THF of tptp_polymorphism * tptp_explicitness * thf_flavor |

   152   DFG of dfg_flavor

   154 datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture

   155 datatype 'a problem_line =

   156   Decl of string * 'a * 'a ho_type |

   157   Formula of string * formula_kind * ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula

   158              * (string, string ho_type) ho_term option * (string, string ho_type) ho_term option

   159 type 'a problem = (string * 'a problem_line list) list

   161 val isabelle_info_prefix = "isabelle_"

   163 (* Currently, only newer versions of SPASS, with sorted DFG format support, can

   164    process Isabelle metainformation. *)

   165 fun isabelle_info (DFG DFG_Sorted) s =

   166     SOME (ATerm ("[]", [ATerm (isabelle_info_prefix ^ s, [])]))

   167   | isabelle_info _ _ = NONE

   169 val introN = "intro"

   170 val elimN = "elim"

   171 val simpN = "simp"

   172 val eqN = "eq"

   174 fun extract_isabelle_info (SOME (ATerm ("[]", [ATerm (s, [])]))) =

   175     try (unprefix isabelle_info_prefix) s

   176   | extract_isabelle_info _ = NONE

   178 (* official TPTP syntax *)

   179 val tptp_cnf = "cnf"

   180 val tptp_fof = "fof"

   181 val tptp_tff = "tff"

   182 val tptp_thf = "thf"

   183 val tptp_has_type = ":"

   184 val tptp_type_of_types = "$tType"

   185 val tptp_bool_type = "$o"

   186 val tptp_individual_type = "$i"

   187 val tptp_fun_type = ">"

   188 val tptp_product_type = "*"

   189 val tptp_forall = "!"

   190 val tptp_ho_forall = "!!"

   191 val tptp_pi_binder = "!>"

   192 val tptp_exists = "?"

   193 val tptp_ho_exists = "??"

   194 val tptp_choice = "@+"

   195 val tptp_not = "~"

   196 val tptp_and = "&"

   197 val tptp_or = "|"

   198 val tptp_implies = "=>"

   199 val tptp_if = "<="

   200 val tptp_iff = "<=>"

   201 val tptp_not_iff = "<~>"

   202 val tptp_app = "@"

   203 val tptp_not_infix = "!"

   204 val tptp_equal = "="

   205 val tptp_old_equal = "equal"

   206 val tptp_false = "$false"

   207 val tptp_true = "$true"

   208 val tptp_empty_list = "[]"

   210 fun is_tptp_equal s = (s = tptp_equal orelse s = tptp_old_equal)

   211 fun is_built_in_tptp_symbol s =

   212   s = tptp_old_equal orelse not (Char.isAlpha (String.sub (s, 0)))

   213 fun is_tptp_variable s = Char.isUpper (String.sub (s, 0))

   214 val is_tptp_user_symbol = not o (is_tptp_variable orf is_built_in_tptp_symbol)

   216 val atype_of_types = AType (`I tptp_type_of_types, [])

   217 val bool_atype = AType (`I tptp_bool_type, [])

   218 val individual_atype = AType (`I tptp_individual_type, [])

   220 fun raw_polarities_of_conn ANot = (SOME false, NONE)

   221   | raw_polarities_of_conn AAnd = (SOME true, SOME true)

   222   | raw_polarities_of_conn AOr = (SOME true, SOME true)

   223   | raw_polarities_of_conn AImplies = (SOME false, SOME true)

   224   | raw_polarities_of_conn AIff = (NONE, NONE)

   225 fun polarities_of_conn NONE = K (NONE, NONE)

   226   | polarities_of_conn (SOME pos) =

   227     raw_polarities_of_conn #> not pos ? pairself (Option.map not)

   229 fun mk_anot (AConn (ANot, [phi])) = phi

   230   | mk_anot phi = AConn (ANot, [phi])

   231 fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])

   233 fun aconn_fold pos f (ANot, [phi]) = f (Option.map not pos) phi

   234   | aconn_fold pos f (AImplies, [phi1, phi2]) =

   235     f (Option.map not pos) phi1 #> f pos phi2

   236   | aconn_fold pos f (AAnd, phis) = fold (f pos) phis

   237   | aconn_fold pos f (AOr, phis) = fold (f pos) phis

   238   | aconn_fold _ f (_, phis) = fold (f NONE) phis

   240 fun aconn_map pos f (ANot, [phi]) = AConn (ANot, [f (Option.map not pos) phi])

   241   | aconn_map pos f (AImplies, [phi1, phi2]) =

   242     AConn (AImplies, [f (Option.map not pos) phi1, f pos phi2])

   243   | aconn_map pos f (AAnd, phis) = AConn (AAnd, map (f pos) phis)

   244   | aconn_map pos f (AOr, phis) = AConn (AOr, map (f pos) phis)

   245   | aconn_map _ f (c, phis) = AConn (c, map (f NONE) phis)

   247 fun formula_fold pos f =

   248   let

   249     fun fld pos (AQuant (_, _, phi)) = fld pos phi

   250       | fld pos (AConn conn) = aconn_fold pos fld conn

   251       | fld pos (AAtom tm) = f pos tm

   252   in fld pos end

   254 fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi)

   255   | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)

   256   | formula_map f (AAtom tm) = AAtom (f tm)

   258 fun is_format_higher_order (THF _) = true

   259   | is_format_higher_order _ = false

   260 fun is_format_typed (TFF _) = true

   261   | is_format_typed (THF _) = true

   262   | is_format_typed (DFG DFG_Sorted) = true

   263   | is_format_typed _ = false

   265 fun tptp_string_for_kind Axiom = "axiom"

   266   | tptp_string_for_kind Definition = "definition"

   267   | tptp_string_for_kind Lemma = "lemma"

   268   | tptp_string_for_kind Hypothesis = "hypothesis"

   269   | tptp_string_for_kind Conjecture = "conjecture"

   271 fun tptp_string_for_app format func args =

   272   if is_format_higher_order format then

   273     "(" ^ space_implode (" " ^ tptp_app ^ " ") (func :: args) ^ ")"

   274   else

   275     func ^ "(" ^ commas args ^ ")"

   277 fun flatten_type (ATyAbs (tys, ty)) = ATyAbs (tys, flatten_type ty)

   278   | flatten_type (ty as AFun (ty1 as AType _, ty2)) =

   279     (case flatten_type ty2 of

   280        AFun (ty' as AType (s, tys), ty) =>

   281        AFun (AType (tptp_product_type,

   282                     ty1 :: (if s = tptp_product_type then tys else [ty'])), ty)

   283      | _ => ty)

   284   | flatten_type (ty as AType _) = ty

   285   | flatten_type _ =

   286     raise Fail "unexpected higher-order type in first-order format"

   288 val dfg_individual_type = "ii" (* cannot clash *)

   290 fun str_for_type format ty =

   291   let

   292     val dfg = (format = DFG DFG_Sorted)

   293     fun str _ (AType (s, [])) =

   294         if dfg andalso s = tptp_individual_type then dfg_individual_type else s

   295       | str _ (AType (s, tys)) =

   296         let val ss = tys |> map (str false) in

   297           if s = tptp_product_type then

   298             ss |> space_implode

   299                       (if dfg then ", " else " " ^ tptp_product_type ^ " ")

   300                |> (not dfg andalso length ss > 1) ? enclose "(" ")"

   301           else

   302             tptp_string_for_app format s ss

   303         end

   304       | str rhs (AFun (ty1, ty2)) =

   305         (str false ty1 |> dfg ? enclose "(" ")") ^ " " ^

   306         (if dfg then "" else tptp_fun_type ^ " ") ^ str true ty2

   307         |> not rhs ? enclose "(" ")"

   308       | str _ (ATyAbs (ss, ty)) =

   309         tptp_pi_binder ^ "[" ^

   310         commas (map (suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types))

   311                     ss) ^ "]: " ^ str false ty

   312   in str true ty end

   314 fun string_for_type (format as THF _) ty = str_for_type format ty

   315   | string_for_type format ty = str_for_type format (flatten_type ty)

   317 fun tptp_string_for_quantifier AForall = tptp_forall

   318   | tptp_string_for_quantifier AExists = tptp_exists

   320 fun tptp_string_for_connective ANot = tptp_not

   321   | tptp_string_for_connective AAnd = tptp_and

   322   | tptp_string_for_connective AOr = tptp_or

   323   | tptp_string_for_connective AImplies = tptp_implies

   324   | tptp_string_for_connective AIff = tptp_iff

   326 fun string_for_bound_var format (s, ty) =

   327   s ^

   328   (if is_format_typed format then

   329      " " ^ tptp_has_type ^ " " ^

   330      (ty |> the_default (AType (tptp_individual_type, []))

   331          |> string_for_type format)

   332    else

   333      "")

   335 fun is_format_with_choice (THF (_, _, THF_With_Choice)) = true

   336   | is_format_with_choice _ = false

   338 fun tptp_string_for_term _ (ATerm (s, [])) = s

   339   | tptp_string_for_term format (ATerm (s, ts)) =

   340     (if s = tptp_empty_list then

   341        (* used for lists in the optional "source" field of a derivation *)

   342        "[" ^ commas (map (tptp_string_for_term format) ts) ^ "]"

   343      else if is_tptp_equal s then

   344        space_implode (" " ^ tptp_equal ^ " ")

   345                      (map (tptp_string_for_term format) ts)

   346        |> is_format_higher_order format ? enclose "(" ")"

   347      else case (s = tptp_ho_forall orelse s = tptp_ho_exists,

   348                 s = tptp_choice andalso is_format_with_choice format, ts) of

   349        (true, _, [AAbs ((s', ty), tm)]) =>

   350        (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever

   351           possible, to work around LEO-II 1.2.8 parser limitation. *)

   352        tptp_string_for_formula format

   353            (AQuant (if s = tptp_ho_forall then AForall else AExists,

   354                     [(s', SOME ty)], AAtom tm))

   355      | (_, true, [AAbs ((s', ty), tm)]) =>

   356        (* There is code in "ATP_Problem_Generate" to ensure that "Eps" is always

   357           applied to an abstraction. *)

   358        tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^

   359        tptp_string_for_term format tm ^ ""

   360        |> enclose "(" ")"

   361      | _ => tptp_string_for_app format s (map (tptp_string_for_term format) ts))

   362   | tptp_string_for_term (format as THF _) (AAbs ((s, ty), tm)) =

   363     "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "]: " ^

   364     tptp_string_for_term format tm ^ ")"

   365   | tptp_string_for_term _ _ =

   366     raise Fail "unexpected term in first-order format"

   367 and tptp_string_for_formula format (AQuant (q, xs, phi)) =

   368     tptp_string_for_quantifier q ^

   369     "[" ^ commas (map (string_for_bound_var format) xs) ^ "]: " ^

   370     tptp_string_for_formula format phi

   371     |> enclose "(" ")"

   372   | tptp_string_for_formula format

   373         (AConn (ANot, [AAtom (ATerm ("=" (* tptp_equal *), ts))])) =

   374     space_implode (" " ^ tptp_not_infix ^ tptp_equal ^ " ")

   375                   (map (tptp_string_for_term format) ts)

   376     |> is_format_higher_order format ? enclose "(" ")"

   377   | tptp_string_for_formula format (AConn (c, [phi])) =

   378     tptp_string_for_connective c ^ " " ^

   379     (tptp_string_for_formula format phi

   380      |> is_format_higher_order format ? enclose "(" ")")

   381     |> enclose "(" ")"

   382   | tptp_string_for_formula format (AConn (c, phis)) =

   383     space_implode (" " ^ tptp_string_for_connective c ^ " ")

   384                   (map (tptp_string_for_formula format) phis)

   385     |> enclose "(" ")"

   386   | tptp_string_for_formula format (AAtom tm) = tptp_string_for_term format tm

   388 fun the_source (SOME source) = source

   389   | the_source NONE =

   390     ATerm ("inference",

   391            ATerm ("isabelle", []) :: replicate 2 (ATerm ("[]", [])))

   393 fun tptp_string_for_format CNF = tptp_cnf

   394   | tptp_string_for_format CNF_UEQ = tptp_cnf

   395   | tptp_string_for_format FOF = tptp_fof

   396   | tptp_string_for_format (TFF _) = tptp_tff

   397   | tptp_string_for_format (THF _) = tptp_thf

   398   | tptp_string_for_format (DFG _) = raise Fail "non-TPTP format"

   400 fun tptp_string_for_problem_line format (Decl (ident, sym, ty)) =

   401     tptp_string_for_format format ^ "(" ^ ident ^ ", type,\n    " ^ sym ^

   402     " : " ^ string_for_type format ty ^ ").\n"

   403   | tptp_string_for_problem_line format

   404                                  (Formula (ident, kind, phi, source, info)) =

   405     tptp_string_for_format format ^ "(" ^ ident ^ ", " ^

   406     tptp_string_for_kind kind ^ ",\n    (" ^

   407     tptp_string_for_formula format phi ^ ")" ^

   408     (case (source, info) of

   409        (NONE, NONE) => ""

   410      | (SOME tm, NONE) => ", " ^ tptp_string_for_term format tm

   411      | (_, SOME tm) =>

   412        ", " ^ tptp_string_for_term format (the_source source) ^

   413        ", " ^ tptp_string_for_term format tm) ^ ").\n"

   415 fun tptp_lines format =

   416   maps (fn (_, []) => []

   417          | (heading, lines) =>

   418            "\n% " ^ heading ^ " (" ^ string_of_int (length lines) ^ ")\n" ::

   419            map (tptp_string_for_problem_line format) lines)

   421 fun arity_of_type (AFun (_, ty)) = 1 + arity_of_type ty

   422   | arity_of_type _ = 0

   424 fun binder_atypes (AFun (ty1, ty2)) = ty1 :: binder_atypes ty2

   425   | binder_atypes _ = []

   427 fun is_function_type (AFun (_, ty)) = is_function_type ty

   428   | is_function_type (AType (s, _)) =

   429     s <> tptp_type_of_types andalso s <> tptp_bool_type

   430   | is_function_type _ = false

   432 fun is_predicate_type (AFun (_, ty)) = is_predicate_type ty

   433   | is_predicate_type (AType (s, _)) = (s = tptp_bool_type)

   434   | is_predicate_type _ = false

   435 fun is_nontrivial_predicate_type (AFun (_, ty)) = is_predicate_type ty

   436   | is_nontrivial_predicate_type _ = false

   438 fun dfg_string_for_formula flavor info =

   439   let

   440     fun suffix_tag top_level s =

   441       if top_level then

   442         case extract_isabelle_info info of

   443           SOME s' => if s' = simpN then s ^ ":lr"

   444                      else if s' = eqN then s ^ ":lt"

   445                      else s

   446         | NONE => s

   447       else

   448         s

   449     fun str_for_term top_level (ATerm (s, tms)) =

   450         (if is_tptp_equal s then "equal" |> suffix_tag top_level

   451          else if s = tptp_true then "true"

   452          else if s = tptp_false then "false"

   453          else s) ^

   454         (if null tms then ""

   455          else "(" ^ commas (map (str_for_term false) tms) ^ ")")

   456       | str_for_term _ _ = raise Fail "unexpected term in first-order format"

   457     fun str_for_quant AForall = "forall"

   458       | str_for_quant AExists = "exists"

   459     fun str_for_conn _ ANot = "not"

   460       | str_for_conn _ AAnd = "and"

   461       | str_for_conn _ AOr = "or"

   462       | str_for_conn _ AImplies = "implies"

   463       | str_for_conn top_level AIff = "equiv" |> suffix_tag top_level

   464     fun str_for_formula top_level (AQuant (q, xs, phi)) =

   465         str_for_quant q ^ "(" ^ "[" ^

   466         commas (map (string_for_bound_var (DFG flavor)) xs) ^ "], " ^

   467         str_for_formula top_level phi ^ ")"

   468       | str_for_formula top_level (AConn (c, phis)) =

   469         str_for_conn top_level c ^ "(" ^

   470         commas (map (str_for_formula false) phis) ^ ")"

   471       | str_for_formula top_level (AAtom tm) = str_for_term top_level tm

   472   in str_for_formula true end

   474 fun dfg_lines flavor problem =

   475   let

   476     val sorted = (flavor = DFG_Sorted)

   477     val format = DFG flavor

   478     fun ary sym ty =

   479       "(" ^ sym ^ ", " ^ string_of_int (arity_of_type ty) ^ ")"

   480     fun fun_typ sym ty =

   481       "function(" ^ sym ^ ", " ^ string_for_type format ty ^ ")."

   482     fun pred_typ sym ty =

   483       "predicate(" ^

   484       commas (sym :: map (string_for_type format) (binder_atypes ty)) ^ ")."

   485     fun formula pred (Formula (ident, kind, phi, _, info)) =

   486         if pred kind then

   487           SOME ("formula(" ^ dfg_string_for_formula flavor info phi ^ ", " ^

   488                 ident ^ ").")

   489         else

   490           NONE

   491       | formula _ _ = NONE

   492     fun filt f = problem |> map (map_filter f o snd) |> flat

   493     val func_aries =

   494       filt (fn Decl (_, sym, ty) =>

   495                if is_function_type ty then SOME (ary sym ty) else NONE

   496              | _ => NONE)

   497       |> commas |> enclose "functions [" "]."

   498     val pred_aries =

   499       filt (fn Decl (_, sym, ty) =>

   500                if is_predicate_type ty then SOME (ary sym ty) else NONE

   501              | _ => NONE)

   502       |> commas |> enclose "predicates [" "]."

   503     fun sorts () =

   504       filt (fn Decl (_, sym, AType (s, [])) =>

   505                if s = tptp_type_of_types then SOME sym else NONE

   506              | _ => NONE) @ [dfg_individual_type]

   507       |> commas |> enclose "sorts [" "]."

   508     val syms = [func_aries, pred_aries] @ (if sorted then [sorts ()] else [])

   509     fun func_sigs () =

   510       filt (fn Decl (_, sym, ty) =>

   511                if is_function_type ty then SOME (fun_typ sym ty) else NONE

   512              | _ => NONE)

   513     fun pred_sigs () =

   514       filt (fn Decl (_, sym, ty) =>

   515                if is_nontrivial_predicate_type ty then SOME (pred_typ sym ty)

   516                else NONE

   517              | _ => NONE)

   518     val decls = if sorted then func_sigs () @ pred_sigs () else []

   519     val axioms = filt (formula (curry (op <>) Conjecture))

   520     val conjs = filt (formula (curry (op =) Conjecture))

   521     fun list_of _ [] = []

   522       | list_of heading ss =

   523         "list_of_" ^ heading ^ ".\n" :: map (suffix "\n") ss @

   524         ["end_of_list.\n\n"]

   525   in

   526     "\nbegin_problem(isabelle).\n\n" ::

   527     list_of "descriptions"

   528             ["name({**}).", "author({**}).", "status(unknown).",

   529              "description({**})."] @

   530     list_of "symbols" syms @

   531     list_of "declarations" decls @

   532     list_of "formulae(axioms)" axioms @

   533     list_of "formulae(conjectures)" conjs @

   534     ["end_problem.\n"]

   535   end

   537 fun lines_for_atp_problem format problem =

   538   "% This file was generated by Isabelle (most likely Sledgehammer)\n\

   539   \% " ^ timestamp () ^ "\n" ::

   540   (case format of

   541      DFG flavor => dfg_lines flavor

   542    | _ => tptp_lines format) problem

   545 (** CNF (Metis) and CNF UEQ (Waldmeister) **)

   547 fun is_problem_line_negated (Formula (_, _, AConn (ANot, _), _, _)) = true

   548   | is_problem_line_negated _ = false

   550 fun is_problem_line_cnf_ueq (Formula (_, _, AAtom (ATerm ((s, _), _)), _, _)) =

   551     is_tptp_equal s

   552   | is_problem_line_cnf_ueq _ = false

   554 fun open_conjecture_term (ATerm ((s, s'), tms)) =

   555     ATerm (if is_tptp_variable s then (s |> Name.desymbolize false, s')

   556            else (s, s'), tms |> map open_conjecture_term)

   557   | open_conjecture_term _ = raise Fail "unexpected higher-order term"

   558 fun open_formula conj =

   559   let

   560     (* We are conveniently assuming that all bound variable names are

   561        distinct, which should be the case for the formulas we generate. *)

   562     fun opn (pos as SOME true) (AQuant (AForall, _, phi)) = opn pos phi

   563       | opn (pos as SOME false) (AQuant (AExists, _, phi)) = opn pos phi

   564       | opn pos (AConn (ANot, [phi])) = mk_anot (opn (Option.map not pos) phi)

   565       | opn pos (AConn (c, [phi1, phi2])) =

   566         let val (pos1, pos2) = polarities_of_conn pos c in

   567           AConn (c, [opn pos1 phi1, opn pos2 phi2])

   568         end

   569       | opn _ (AAtom t) = AAtom (t |> conj ? open_conjecture_term)

   570       | opn _ phi = phi

   571   in opn (SOME (not conj)) end

   572 fun open_formula_line (Formula (ident, kind, phi, source, info)) =

   573     Formula (ident, kind, open_formula (kind = Conjecture) phi, source, info)

   574   | open_formula_line line = line

   576 fun negate_conjecture_line (Formula (ident, Conjecture, phi, source, info)) =

   577     Formula (ident, Hypothesis, mk_anot phi, source, info)

   578   | negate_conjecture_line line = line

   580 exception CLAUSIFY of unit

   582 (* This "clausification" only expands syntactic sugar, such as "phi => psi" to

   583    "~ phi | psi" and "phi <=> psi" to "~ phi | psi" and "~ psi | phi". We don't

   584    attempt to distribute conjunctions over disjunctions. *)

   585 fun clausify_formula pos (phi as AAtom _) = [phi |> not pos ? mk_anot]

   586   | clausify_formula pos (AConn (ANot, [phi])) = clausify_formula (not pos) phi

   587   | clausify_formula true (AConn (AOr, [phi1, phi2])) =

   588     (phi1, phi2) |> pairself (clausify_formula true)

   589                  |> uncurry (map_product (mk_aconn AOr))

   590   | clausify_formula false (AConn (AAnd, [phi1, phi2])) =

   591     (phi1, phi2) |> pairself (clausify_formula false)

   592                  |> uncurry (map_product (mk_aconn AOr))

   593   | clausify_formula true (AConn (AImplies, [phi1, phi2])) =

   594     clausify_formula true (AConn (AOr, [mk_anot phi1, phi2]))

   595   | clausify_formula true (AConn (AIff, phis)) =

   596     clausify_formula true (AConn (AImplies, phis)) @

   597     clausify_formula true (AConn (AImplies, rev phis))

   598   | clausify_formula _ _ = raise CLAUSIFY ()

   600 fun clausify_formula_line (Formula (ident, kind, phi, source, info)) =

   601     let

   602       val (n, phis) = phi |> try (clausify_formula true) |> these |> `length

   603     in

   604       map2 (fn phi => fn j =>

   605                Formula (ident ^ replicate_string (j - 1) "x", kind, phi, source,

   606                         info))

   607            phis (1 upto n)

   608     end

   609   | clausify_formula_line _ = []

   611 fun ensure_cnf_problem_line line =

   612   line |> open_formula_line |> negate_conjecture_line |> clausify_formula_line

   614 fun ensure_cnf_problem problem =

   615   problem |> map (apsnd (maps ensure_cnf_problem_line))

   617 fun filter_cnf_ueq_problem problem =

   618   problem

   619   |> map (apsnd (map open_formula_line

   620                  #> filter is_problem_line_cnf_ueq

   621                  #> map negate_conjecture_line))

   622   |> (fn problem =>

   623          let

   624            val lines = problem |> maps snd

   625            val conjs = lines |> filter is_problem_line_negated

   626          in if length conjs = 1 andalso conjs <> lines then problem else [] end)

   629 (** Symbol declarations **)

   631 fun add_declared_syms_in_problem_line (Decl (_, sym, _)) = insert (op =) sym

   632   | add_declared_syms_in_problem_line _ = I

   633 fun declared_syms_in_problem problem =

   634   fold (fold add_declared_syms_in_problem_line o snd) problem []

   636 (** Nice names **)

   638 fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs

   639 fun pool_map f xs =

   640   pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []

   642 val no_qualifiers =

   643   let

   644     fun skip [] = []

   645       | skip (#"." :: cs) = skip cs

   646       | skip (c :: cs) = if Char.isAlphaNum c then skip cs else c :: keep cs

   647     and keep [] = []

   648       | keep (#"." :: cs) = skip cs

   649       | keep (c :: cs) = c :: keep cs

   650   in String.explode #> rev #> keep #> rev #> String.implode end

   652 (* Long names can slow down the ATPs. *)

   653 val max_readable_name_size = 20

   655 (* "equal" is reserved by some ATPs. "op" is also reserved, to avoid the

   656    unreadable "op_1", "op_2", etc., in the problem files. "eq" is reserved to

   657    ensure that "HOL.eq" is correctly mapped to equality (not clear whether this

   658    is still necessary). *)

   659 val reserved_nice_names = [tptp_old_equal, "op", "eq"]

   661 fun readable_name protect full_name s =

   662   (if s = full_name then

   663      s

   664    else

   665      s |> no_qualifiers

   666        |> perhaps (try (unprefix "'"))

   667        |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0)))

   668        |> (fn s =>

   669               if size s > max_readable_name_size then

   670                 String.substring (s, 0, max_readable_name_size div 2 - 4) ^

   671                 string_of_int (hash_string full_name) ^

   672                 String.extract (s, size s - max_readable_name_size div 2 + 4,

   673                                 NONE)

   674               else

   675                 s)

   676        |> (fn s =>

   677               if member (op =) reserved_nice_names s then full_name else s))

   678   |> protect

   680 fun nice_name _ (full_name, _) NONE = (full_name, NONE)

   681   | nice_name protect (full_name, desired_name) (SOME the_pool) =

   682     if is_built_in_tptp_symbol full_name then

   683       (full_name, SOME the_pool)

   684     else case Symtab.lookup (fst the_pool) full_name of

   685       SOME nice_name => (nice_name, SOME the_pool)

   686     | NONE =>

   687       let

   688         val nice_prefix = readable_name protect full_name desired_name

   689         fun add j =

   690           let

   691             val nice_name =

   692               nice_prefix ^ (if j = 0 then "" else string_of_int j)

   693           in

   694             case Symtab.lookup (snd the_pool) nice_name of

   695               SOME full_name' =>

   696               if full_name = full_name' then (nice_name, the_pool)

   697               else add (j + 1)

   698             | NONE =>

   699               (nice_name,

   700                (Symtab.update_new (full_name, nice_name) (fst the_pool),

   701                 Symtab.update_new (nice_name, full_name) (snd the_pool)))

   702           end

   703       in add 0 |> apsnd SOME end

   705 fun avoid_clash_with_dfg_keywords s =

   706   let val n = String.size s in

   707     if n < 2 orelse String.isSubstring "_" s then

   708       s

   709     else

   710       String.substring (s, 0, n - 1) ^

   711       String.str (Char.toUpper (String.sub (s, n - 1)))

   712   end

   714 fun nice_atp_problem readable_names format problem =

   715   let

   716     val empty_pool =

   717       if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE

   718     val nice_name =

   719       nice_name (case format of DFG _ => avoid_clash_with_dfg_keywords | _ => I)

   720     fun nice_type (AType (name, tys)) =

   721         nice_name name ##>> pool_map nice_type tys #>> AType

   722       | nice_type (AFun (ty1, ty2)) = nice_type ty1 ##>> nice_type ty2 #>> AFun

   723       | nice_type (ATyAbs (names, ty)) =

   724         pool_map nice_name names ##>> nice_type ty #>> ATyAbs

   725     fun nice_term (ATerm (name, ts)) =

   726         nice_name name ##>> pool_map nice_term ts #>> ATerm

   727       | nice_term (AAbs ((name, ty), tm)) =

   728         nice_name name ##>> nice_type ty ##>> nice_term tm #>> AAbs

   729     fun nice_formula (AQuant (q, xs, phi)) =

   730         pool_map nice_name (map fst xs)

   731         ##>> pool_map (fn NONE => pair NONE

   732                         | SOME ty => nice_type ty #>> SOME) (map snd xs)

   733         ##>> nice_formula phi

   734         #>> (fn ((ss, ts), phi) => AQuant (q, ss ~~ ts, phi))

   735       | nice_formula (AConn (c, phis)) =

   736         pool_map nice_formula phis #>> curry AConn c

   737       | nice_formula (AAtom tm) = nice_term tm #>> AAtom

   738     fun nice_problem_line (Decl (ident, sym, ty)) =

   739         nice_name sym ##>> nice_type ty #>> (fn (sym, ty) => Decl (ident, sym, ty))

   740       | nice_problem_line (Formula (ident, kind, phi, source, info)) =

   741         nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source, info))

   742     fun nice_problem problem =

   743       pool_map (fn (heading, lines) =>

   744                    pool_map nice_problem_line lines #>> pair heading) problem

   745   in nice_problem problem empty_pool end

   747 end;

author	blanchet
	Wed, 01 Feb 2012 17:16:55 +0100
changeset 47219	8d8d3c1f1854
parent 47210	b99ca1a7c63b
child 47221	69f2d19f7d33
permissions	-rw-r--r--