equal
deleted
inserted
replaced
13 datatype ('a, 'b) formula = |
13 datatype ('a, 'b) formula = |
14 AQuant of quantifier * 'a list * ('a, 'b) formula | |
14 AQuant of quantifier * 'a list * ('a, 'b) formula | |
15 AConn of connective * ('a, 'b) formula list | |
15 AConn of connective * ('a, 'b) formula list | |
16 AAtom of 'b |
16 AAtom of 'b |
17 |
17 |
18 datatype kind = Axiom | Conjecture |
18 datatype kind = Axiom | Hypothesis | Conjecture |
19 datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula |
19 datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula |
20 type 'a problem = (string * 'a problem_line list) list |
20 type 'a problem = (string * 'a problem_line list) list |
21 |
21 |
22 val timestamp : unit -> string |
22 val timestamp : unit -> string |
23 val is_tptp_variable : string -> bool |
23 val is_tptp_variable : string -> bool |
40 datatype ('a, 'b) formula = |
40 datatype ('a, 'b) formula = |
41 AQuant of quantifier * 'a list * ('a, 'b) formula | |
41 AQuant of quantifier * 'a list * ('a, 'b) formula | |
42 AConn of connective * ('a, 'b) formula list | |
42 AConn of connective * ('a, 'b) formula list | |
43 AAtom of 'b |
43 AAtom of 'b |
44 |
44 |
45 datatype kind = Axiom | Conjecture |
45 datatype kind = Axiom | Hypothesis | Conjecture |
46 datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula |
46 datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula |
47 type 'a problem = (string * 'a problem_line list) list |
47 type 'a problem = (string * 'a problem_line list) list |
48 |
48 |
49 val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now |
49 val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now |
50 |
50 |
74 (map string_for_formula phis) ^ ")" |
74 (map string_for_formula phis) ^ ")" |
75 | string_for_formula (AAtom tm) = string_for_term tm |
75 | string_for_formula (AAtom tm) = string_for_term tm |
76 |
76 |
77 fun string_for_problem_line (Fof (ident, kind, phi)) = |
77 fun string_for_problem_line (Fof (ident, kind, phi)) = |
78 "fof(" ^ ident ^ ", " ^ |
78 "fof(" ^ ident ^ ", " ^ |
79 (case kind of Axiom => "axiom" | Conjecture => "conjecture") ^ ",\n" ^ |
79 (case kind of |
80 " (" ^ string_for_formula phi ^ ")).\n" |
80 Axiom => "axiom" |
|
81 | Hypothesis => "hypothesis" |
|
82 | Conjecture => "conjecture") ^ |
|
83 ",\n (" ^ string_for_formula phi ^ ")).\n" |
81 fun strings_for_tptp_problem problem = |
84 fun strings_for_tptp_problem problem = |
82 "% This file was generated by Isabelle (most likely Sledgehammer)\n\ |
85 "% This file was generated by Isabelle (most likely Sledgehammer)\n\ |
83 \% " ^ timestamp () ^ "\n" :: |
86 \% " ^ timestamp () ^ "\n" :: |
84 maps (fn (_, []) => [] |
87 maps (fn (_, []) => [] |
85 | (heading, lines) => |
88 | (heading, lines) => |