# HG changeset patch # User blanchet # Date 1280244775 -7200 # Node ID ee6c11ae807759f45dbc4c3e7d5690c10968e18e # Parent 3ad3e3ca24511ca22f4f36b86a2245e854495a73 renamed file diff -r 3ad3e3ca2451 -r ee6c11ae8077 src/HOL/Tools/ATP_Manager/atp_problem.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/ATP_Manager/atp_problem.ML Tue Jul 27 17:32:55 2010 +0200 @@ -0,0 +1,153 @@ +(* Title: HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML + Author: Jia Meng, NICTA + Author: Jasmin Blanchette, TU Muenchen + +TPTP syntax. +*) + +signature SLEDGEHAMMER_TPTP_FORMAT = +sig + type kind = Metis_Clauses.kind + + datatype 'a fo_term = ATerm of 'a * 'a fo_term list + datatype quantifier = AForall | AExists + datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff + datatype ('a, 'b) formula = + AQuant of quantifier * 'a list * ('a, 'b) formula | + AConn of connective * ('a, 'b) formula list | + APred of 'b + + datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula + type 'a problem = (string * 'a problem_line list) list + + val is_tptp_variable : string -> bool + val strings_for_tptp_problem : + (string * string problem_line list) list -> string list + val nice_tptp_problem : + bool -> ('a * (string * string) problem_line list) list + -> ('a * string problem_line list) list + * (string Symtab.table * string Symtab.table) option +end; + +structure Sledgehammer_TPTP_Format : SLEDGEHAMMER_TPTP_FORMAT = +struct + +open Sledgehammer_Util + +type kind = Metis_Clauses.kind + +(** ATP problem **) + +datatype 'a fo_term = ATerm of 'a * 'a fo_term list +datatype quantifier = AForall | AExists +datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff +datatype ('a, 'b) formula = + AQuant of quantifier * 'a list * ('a, 'b) formula | + AConn of connective * ('a, 'b) formula list | + APred of 'b + +datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula +type 'a problem = (string * 'a problem_line list) list + +fun string_for_term (ATerm (s, [])) = s + | string_for_term (ATerm (s, ts)) = + if s = "equal" then space_implode " = " (map string_for_term ts) + else s ^ "(" ^ commas (map string_for_term ts) ^ ")" +fun string_for_quantifier AForall = "!" + | string_for_quantifier AExists = "?" +fun string_for_connective ANot = "~" + | string_for_connective AAnd = "&" + | string_for_connective AOr = "|" + | string_for_connective AImplies = "=>" + | string_for_connective AIf = "<=" + | string_for_connective AIff = "<=>" + | string_for_connective ANotIff = "<~>" +fun string_for_formula (AQuant (q, xs, phi)) = + string_for_quantifier q ^ "[" ^ commas xs ^ "]: " ^ + string_for_formula phi + | string_for_formula (AConn (ANot, [APred (ATerm ("equal", ts))])) = + space_implode " != " (map string_for_term ts) + | string_for_formula (AConn (c, [phi])) = + string_for_connective c ^ " " ^ string_for_formula phi + | string_for_formula (AConn (c, phis)) = + "(" ^ space_implode (" " ^ string_for_connective c ^ " ") + (map string_for_formula phis) ^ ")" + | string_for_formula (APred tm) = string_for_term tm + +fun string_for_problem_line (Fof (ident, kind, phi)) = + "fof(" ^ ident ^ ", " ^ + (case kind of Axiom => "axiom" | Conjecture => "conjecture") ^ ",\n" ^ + " (" ^ string_for_formula phi ^ ")).\n" +fun strings_for_tptp_problem problem = + "% This file was generated by Isabelle (most likely Sledgehammer)\n\ + \% " ^ timestamp () ^ "\n" :: + maps (fn (_, []) => [] + | (heading, lines) => + "\n% " ^ heading ^ " (" ^ Int.toString (length lines) ^ ")\n" :: + map string_for_problem_line lines) problem + +fun is_tptp_variable s = Char.isUpper (String.sub (s, 0)) + + +(** Nice names **) + +fun empty_name_pool readable_names = + if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE + +fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs +fun pool_map f xs = + pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs [] + +(* "equal" is reserved by some ATPs. "op" is also reserved, to avoid the + unreadable "op_1", "op_2", etc., in the problem files. *) +val reserved_nice_names = ["equal", "op"] +fun readable_name full_name s = + if s = full_name then + s + else + let + val s = s |> Long_Name.base_name + |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0))) + in if member (op =) reserved_nice_names s then full_name else s end + +fun nice_name (full_name, _) NONE = (full_name, NONE) + | nice_name (full_name, desired_name) (SOME the_pool) = + case Symtab.lookup (fst the_pool) full_name of + SOME nice_name => (nice_name, SOME the_pool) + | NONE => + let + val nice_prefix = readable_name full_name desired_name + fun add j = + let + val nice_name = nice_prefix ^ + (if j = 0 then "" else "_" ^ Int.toString j) + in + case Symtab.lookup (snd the_pool) nice_name of + SOME full_name' => + if full_name = full_name' then (nice_name, the_pool) + else add (j + 1) + | NONE => + (nice_name, + (Symtab.update_new (full_name, nice_name) (fst the_pool), + Symtab.update_new (nice_name, full_name) (snd the_pool))) + end + in add 0 |> apsnd SOME end + + +fun nice_term (ATerm (name, ts)) = + nice_name name ##>> pool_map nice_term ts #>> ATerm +fun nice_formula (AQuant (q, xs, phi)) = + pool_map nice_name xs ##>> nice_formula phi + #>> (fn (xs, phi) => AQuant (q, xs, phi)) + | nice_formula (AConn (c, phis)) = + pool_map nice_formula phis #>> curry AConn c + | nice_formula (APred tm) = nice_term tm #>> APred +fun nice_problem_line (Fof (ident, kind, phi)) = + nice_formula phi #>> (fn phi => Fof (ident, kind, phi)) +fun nice_problem problem = + pool_map (fn (heading, lines) => + pool_map nice_problem_line lines #>> pair heading) problem +fun nice_tptp_problem readable_names problem = + nice_problem problem (empty_name_pool readable_names) + +end; diff -r 3ad3e3ca2451 -r ee6c11ae8077 src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Tue Jul 27 17:32:10 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,153 +0,0 @@ -(* Title: HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML - Author: Jia Meng, NICTA - Author: Jasmin Blanchette, TU Muenchen - -TPTP syntax. -*) - -signature SLEDGEHAMMER_TPTP_FORMAT = -sig - type kind = Metis_Clauses.kind - - datatype 'a fo_term = ATerm of 'a * 'a fo_term list - datatype quantifier = AForall | AExists - datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff - datatype ('a, 'b) formula = - AQuant of quantifier * 'a list * ('a, 'b) formula | - AConn of connective * ('a, 'b) formula list | - APred of 'b - - datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula - type 'a problem = (string * 'a problem_line list) list - - val is_tptp_variable : string -> bool - val strings_for_tptp_problem : - (string * string problem_line list) list -> string list - val nice_tptp_problem : - bool -> ('a * (string * string) problem_line list) list - -> ('a * string problem_line list) list - * (string Symtab.table * string Symtab.table) option -end; - -structure Sledgehammer_TPTP_Format : SLEDGEHAMMER_TPTP_FORMAT = -struct - -open Sledgehammer_Util - -type kind = Metis_Clauses.kind - -(** ATP problem **) - -datatype 'a fo_term = ATerm of 'a * 'a fo_term list -datatype quantifier = AForall | AExists -datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff -datatype ('a, 'b) formula = - AQuant of quantifier * 'a list * ('a, 'b) formula | - AConn of connective * ('a, 'b) formula list | - APred of 'b - -datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula -type 'a problem = (string * 'a problem_line list) list - -fun string_for_term (ATerm (s, [])) = s - | string_for_term (ATerm (s, ts)) = - if s = "equal" then space_implode " = " (map string_for_term ts) - else s ^ "(" ^ commas (map string_for_term ts) ^ ")" -fun string_for_quantifier AForall = "!" - | string_for_quantifier AExists = "?" -fun string_for_connective ANot = "~" - | string_for_connective AAnd = "&" - | string_for_connective AOr = "|" - | string_for_connective AImplies = "=>" - | string_for_connective AIf = "<=" - | string_for_connective AIff = "<=>" - | string_for_connective ANotIff = "<~>" -fun string_for_formula (AQuant (q, xs, phi)) = - string_for_quantifier q ^ "[" ^ commas xs ^ "]: " ^ - string_for_formula phi - | string_for_formula (AConn (ANot, [APred (ATerm ("equal", ts))])) = - space_implode " != " (map string_for_term ts) - | string_for_formula (AConn (c, [phi])) = - string_for_connective c ^ " " ^ string_for_formula phi - | string_for_formula (AConn (c, phis)) = - "(" ^ space_implode (" " ^ string_for_connective c ^ " ") - (map string_for_formula phis) ^ ")" - | string_for_formula (APred tm) = string_for_term tm - -fun string_for_problem_line (Fof (ident, kind, phi)) = - "fof(" ^ ident ^ ", " ^ - (case kind of Axiom => "axiom" | Conjecture => "conjecture") ^ ",\n" ^ - " (" ^ string_for_formula phi ^ ")).\n" -fun strings_for_tptp_problem problem = - "% This file was generated by Isabelle (most likely Sledgehammer)\n\ - \% " ^ timestamp () ^ "\n" :: - maps (fn (_, []) => [] - | (heading, lines) => - "\n% " ^ heading ^ " (" ^ Int.toString (length lines) ^ ")\n" :: - map string_for_problem_line lines) problem - -fun is_tptp_variable s = Char.isUpper (String.sub (s, 0)) - - -(** Nice names **) - -fun empty_name_pool readable_names = - if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE - -fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs -fun pool_map f xs = - pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs [] - -(* "equal" is reserved by some ATPs. "op" is also reserved, to avoid the - unreadable "op_1", "op_2", etc., in the problem files. *) -val reserved_nice_names = ["equal", "op"] -fun readable_name full_name s = - if s = full_name then - s - else - let - val s = s |> Long_Name.base_name - |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0))) - in if member (op =) reserved_nice_names s then full_name else s end - -fun nice_name (full_name, _) NONE = (full_name, NONE) - | nice_name (full_name, desired_name) (SOME the_pool) = - case Symtab.lookup (fst the_pool) full_name of - SOME nice_name => (nice_name, SOME the_pool) - | NONE => - let - val nice_prefix = readable_name full_name desired_name - fun add j = - let - val nice_name = nice_prefix ^ - (if j = 0 then "" else "_" ^ Int.toString j) - in - case Symtab.lookup (snd the_pool) nice_name of - SOME full_name' => - if full_name = full_name' then (nice_name, the_pool) - else add (j + 1) - | NONE => - (nice_name, - (Symtab.update_new (full_name, nice_name) (fst the_pool), - Symtab.update_new (nice_name, full_name) (snd the_pool))) - end - in add 0 |> apsnd SOME end - - -fun nice_term (ATerm (name, ts)) = - nice_name name ##>> pool_map nice_term ts #>> ATerm -fun nice_formula (AQuant (q, xs, phi)) = - pool_map nice_name xs ##>> nice_formula phi - #>> (fn (xs, phi) => AQuant (q, xs, phi)) - | nice_formula (AConn (c, phis)) = - pool_map nice_formula phis #>> curry AConn c - | nice_formula (APred tm) = nice_term tm #>> APred -fun nice_problem_line (Fof (ident, kind, phi)) = - nice_formula phi #>> (fn phi => Fof (ident, kind, phi)) -fun nice_problem problem = - pool_map (fn (heading, lines) => - pool_map nice_problem_line lines #>> pair heading) problem -fun nice_tptp_problem readable_names problem = - nice_problem problem (empty_name_pool readable_names) - -end;