4 FOL clauses translated from HOL formulae. |
4 FOL clauses translated from HOL formulae. |
5 *) |
5 *) |
6 |
6 |
7 signature SLEDGEHAMMER_HOL_CLAUSE = |
7 signature SLEDGEHAMMER_HOL_CLAUSE = |
8 sig |
8 sig |
9 val ext: thm |
9 type kind = Sledgehammer_FOL_Clause.kind |
10 val comb_I: thm |
10 type fol_type = Sledgehammer_FOL_Clause.fol_type |
11 val comb_K: thm |
11 type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause |
12 val comb_B: thm |
12 type arity_clause = Sledgehammer_FOL_Clause.arity_clause |
13 val comb_C: thm |
|
14 val comb_S: thm |
|
15 val minimize_applies: bool |
|
16 type axiom_name = string |
13 type axiom_name = string |
17 type polarity = bool |
14 type polarity = bool |
18 type clause_id = int |
15 type hol_clause_id = int |
|
16 |
19 datatype combterm = |
17 datatype combterm = |
20 CombConst of string * Sledgehammer_FOL_Clause.fol_type * Sledgehammer_FOL_Clause.fol_type list (*Const and Free*) |
18 CombConst of string * fol_type * fol_type list (* Const and Free *) | |
21 | CombVar of string * Sledgehammer_FOL_Clause.fol_type |
19 CombVar of string * fol_type | |
22 | CombApp of combterm * combterm |
20 CombApp of combterm * combterm |
23 datatype literal = Literal of polarity * combterm |
21 datatype literal = Literal of polarity * combterm |
24 datatype clause = Clause of {clause_id: clause_id, axiom_name: axiom_name, th: thm, |
22 datatype hol_clause = |
25 kind: Sledgehammer_FOL_Clause.kind,literals: literal list, ctypes_sorts: typ list} |
23 HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm, |
26 val type_of_combterm: combterm -> Sledgehammer_FOL_Clause.fol_type |
24 kind: kind, literals: literal list, ctypes_sorts: typ list} |
27 val strip_comb: combterm -> combterm * combterm list |
25 |
28 val literals_of_term: theory -> term -> literal list * typ list |
26 val type_of_combterm : combterm -> fol_type |
29 exception TOO_TRIVIAL |
27 val strip_combterm_comb : combterm -> combterm * combterm list |
30 val make_conjecture_clauses: bool -> theory -> thm list -> clause list |
28 val literals_of_term : theory -> term -> literal list * typ list |
31 val make_axiom_clauses: bool -> |
29 exception TRIVIAL |
32 theory -> |
30 val make_conjecture_clauses : bool -> theory -> thm list -> hol_clause list |
33 (thm * (axiom_name * clause_id)) list -> (axiom_name * clause) list |
31 val make_axiom_clauses : bool -> theory -> |
34 val get_helper_clauses: bool -> |
32 (thm * (axiom_name * hol_clause_id)) list -> (axiom_name * hol_clause) list |
35 theory -> |
33 val get_helper_clauses : bool -> theory -> bool -> |
36 bool -> |
34 hol_clause list * (thm * (axiom_name * hol_clause_id)) list * string list -> |
37 clause list * (thm * (axiom_name * clause_id)) list * string list -> |
35 hol_clause list |
38 clause list |
36 val write_tptp_file : bool -> Path.T -> |
39 val tptp_write_file: bool -> Path.T -> |
37 hol_clause list * hol_clause list * hol_clause list * hol_clause list * |
40 clause list * clause list * clause list * clause list * |
38 classrel_clause list * arity_clause list -> |
41 Sledgehammer_FOL_Clause.classrelClause list * Sledgehammer_FOL_Clause.arityClause list -> |
|
42 int * int |
39 int * int |
43 val dfg_write_file: bool -> Path.T -> |
40 val write_dfg_file : bool -> Path.T -> |
44 clause list * clause list * clause list * clause list * |
41 hol_clause list * hol_clause list * hol_clause list * hol_clause list * |
45 Sledgehammer_FOL_Clause.classrelClause list * Sledgehammer_FOL_Clause.arityClause list -> |
42 classrel_clause list * arity_clause list -> int * int |
46 int * int |
|
47 end |
43 end |
48 |
44 |
49 structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE = |
45 structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE = |
50 struct |
46 struct |
51 |
47 |
52 structure SFC = Sledgehammer_FOL_Clause; |
48 open Sledgehammer_FOL_Clause |
53 |
49 open Sledgehammer_Fact_Preprocessor |
54 (* theorems for combinators and function extensionality *) |
|
55 val ext = thm "HOL.ext"; |
|
56 val comb_I = thm "Sledgehammer.COMBI_def"; |
|
57 val comb_K = thm "Sledgehammer.COMBK_def"; |
|
58 val comb_B = thm "Sledgehammer.COMBB_def"; |
|
59 val comb_C = thm "Sledgehammer.COMBC_def"; |
|
60 val comb_S = thm "Sledgehammer.COMBS_def"; |
|
61 val fequal_imp_equal = thm "Sledgehammer.fequal_imp_equal"; |
|
62 val equal_imp_fequal = thm "Sledgehammer.equal_imp_fequal"; |
|
63 |
|
64 |
50 |
65 (* Parameter t_full below indicates that full type information is to be |
51 (* Parameter t_full below indicates that full type information is to be |
66 exported *) |
52 exported *) |
67 |
53 |
68 (*If true, each function will be directly applied to as many arguments as possible, avoiding |
54 (* If true, each function will be directly applied to as many arguments as |
69 use of the "apply" operator. Use of hBOOL is also minimized.*) |
55 possible, avoiding use of the "apply" operator. Use of hBOOL is also |
|
56 minimized. *) |
70 val minimize_applies = true; |
57 val minimize_applies = true; |
71 |
58 |
72 fun min_arity_of const_min_arity c = the_default 0 (Symtab.lookup const_min_arity c); |
59 fun min_arity_of const_min_arity c = the_default 0 (Symtab.lookup const_min_arity c); |
73 |
60 |
74 (*True if the constant ever appears outside of the top-level position in literals. |
61 (*True if the constant ever appears outside of the top-level position in literals. |
82 (* data types for typed combinator expressions *) |
69 (* data types for typed combinator expressions *) |
83 (******************************************************) |
70 (******************************************************) |
84 |
71 |
85 type axiom_name = string; |
72 type axiom_name = string; |
86 type polarity = bool; |
73 type polarity = bool; |
87 type clause_id = int; |
74 type hol_clause_id = int; |
88 |
75 |
89 datatype combterm = CombConst of string * SFC.fol_type * SFC.fol_type list (*Const and Free*) |
76 datatype combterm = |
90 | CombVar of string * SFC.fol_type |
77 CombConst of string * fol_type * fol_type list (* Const and Free *) | |
91 | CombApp of combterm * combterm |
78 CombVar of string * fol_type | |
|
79 CombApp of combterm * combterm |
92 |
80 |
93 datatype literal = Literal of polarity * combterm; |
81 datatype literal = Literal of polarity * combterm; |
94 |
82 |
95 datatype clause = |
83 datatype hol_clause = |
96 Clause of {clause_id: clause_id, |
84 HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm, |
97 axiom_name: axiom_name, |
85 kind: kind, literals: literal list, ctypes_sorts: typ list}; |
98 th: thm, |
|
99 kind: SFC.kind, |
|
100 literals: literal list, |
|
101 ctypes_sorts: typ list}; |
|
102 |
86 |
103 |
87 |
104 (*********************************************************************) |
88 (*********************************************************************) |
105 (* convert a clause with type Term.term to a clause with type clause *) |
89 (* convert a clause with type Term.term to a clause with type clause *) |
106 (*********************************************************************) |
90 (*********************************************************************) |
107 |
91 |
108 fun isFalse (Literal(pol, CombConst(c,_,_))) = |
92 fun isFalse (Literal(pol, CombConst(c,_,_))) = |
109 (pol andalso c = "c_False") orelse |
93 (pol andalso c = "c_False") orelse (not pol andalso c = "c_True") |
110 (not pol andalso c = "c_True") |
|
111 | isFalse _ = false; |
94 | isFalse _ = false; |
112 |
95 |
113 fun isTrue (Literal (pol, CombConst(c,_,_))) = |
96 fun isTrue (Literal (pol, CombConst(c,_,_))) = |
114 (pol andalso c = "c_True") orelse |
97 (pol andalso c = "c_True") orelse |
115 (not pol andalso c = "c_False") |
98 (not pol andalso c = "c_False") |
116 | isTrue _ = false; |
99 | isTrue _ = false; |
117 |
100 |
118 fun isTaut (Clause {literals,...}) = exists isTrue literals; |
101 fun isTaut (HOLClause {literals,...}) = exists isTrue literals; |
119 |
102 |
120 fun type_of dfg (Type (a, Ts)) = |
103 fun type_of dfg (Type (a, Ts)) = |
121 let val (folTypes,ts) = types_of dfg Ts |
104 let val (folTypes,ts) = types_of dfg Ts |
122 in (SFC.Comp(SFC.make_fixed_type_const dfg a, folTypes), ts) end |
105 in (Comp(make_fixed_type_const dfg a, folTypes), ts) end |
123 | type_of _ (tp as TFree (a, _)) = |
106 | type_of _ (tp as TFree (a, _)) = (AtomF (make_fixed_type_var a), [tp]) |
124 (SFC.AtomF (SFC.make_fixed_type_var a), [tp]) |
107 | type_of _ (tp as TVar (v, _)) = (AtomV (make_schematic_type_var v), [tp]) |
125 | type_of _ (tp as TVar (v, _)) = |
|
126 (SFC.AtomV (SFC.make_schematic_type_var v), [tp]) |
|
127 and types_of dfg Ts = |
108 and types_of dfg Ts = |
128 let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts) |
109 let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts) |
129 in (folTyps, SFC.union_all ts) end; |
110 in (folTyps, union_all ts) end; |
130 |
111 |
131 (* same as above, but no gathering of sort information *) |
112 (* same as above, but no gathering of sort information *) |
132 fun simp_type_of dfg (Type (a, Ts)) = |
113 fun simp_type_of dfg (Type (a, Ts)) = |
133 SFC.Comp(SFC.make_fixed_type_const dfg a, map (simp_type_of dfg) Ts) |
114 Comp(make_fixed_type_const dfg a, map (simp_type_of dfg) Ts) |
134 | simp_type_of _ (TFree (a, _)) = SFC.AtomF(SFC.make_fixed_type_var a) |
115 | simp_type_of _ (TFree (a, _)) = AtomF (make_fixed_type_var a) |
135 | simp_type_of _ (TVar (v, _)) = SFC.AtomV(SFC.make_schematic_type_var v); |
116 | simp_type_of _ (TVar (v, _)) = AtomV (make_schematic_type_var v); |
136 |
117 |
137 |
118 |
138 fun const_type_of dfg thy (c,t) = |
119 fun const_type_of dfg thy (c,t) = |
139 let val (tp,ts) = type_of dfg t |
120 let val (tp,ts) = type_of dfg t |
140 in (tp, ts, map (simp_type_of dfg) (Sign.const_typargs thy (c,t))) end; |
121 in (tp, ts, map (simp_type_of dfg) (Sign.const_typargs thy (c,t))) end; |
141 |
122 |
142 (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *) |
123 (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *) |
143 fun combterm_of dfg thy (Const(c,t)) = |
124 fun combterm_of dfg thy (Const(c,t)) = |
144 let val (tp,ts,tvar_list) = const_type_of dfg thy (c,t) |
125 let val (tp,ts,tvar_list) = const_type_of dfg thy (c,t) |
145 val c' = CombConst(SFC.make_fixed_const dfg c, tp, tvar_list) |
126 val c' = CombConst(make_fixed_const dfg c, tp, tvar_list) |
146 in (c',ts) end |
127 in (c',ts) end |
147 | combterm_of dfg _ (Free(v,t)) = |
128 | combterm_of dfg _ (Free(v,t)) = |
148 let val (tp,ts) = type_of dfg t |
129 let val (tp,ts) = type_of dfg t |
149 val v' = CombConst(SFC.make_fixed_var v, tp, []) |
130 val v' = CombConst(make_fixed_var v, tp, []) |
150 in (v',ts) end |
131 in (v',ts) end |
151 | combterm_of dfg _ (Var(v,t)) = |
132 | combterm_of dfg _ (Var(v,t)) = |
152 let val (tp,ts) = type_of dfg t |
133 let val (tp,ts) = type_of dfg t |
153 val v' = CombVar(SFC.make_schematic_var v,tp) |
134 val v' = CombVar(make_schematic_var v,tp) |
154 in (v',ts) end |
135 in (v',ts) end |
155 | combterm_of dfg thy (P $ Q) = |
136 | combterm_of dfg thy (P $ Q) = |
156 let val (P',tsP) = combterm_of dfg thy P |
137 let val (P',tsP) = combterm_of dfg thy P |
157 val (Q',tsQ) = combterm_of dfg thy Q |
138 val (Q',tsQ) = combterm_of dfg thy Q |
158 in (CombApp(P',Q'), union (op =) tsP tsQ) end |
139 in (CombApp(P',Q'), union (op =) tsP tsQ) end |
159 | combterm_of _ _ (t as Abs _) = raise SFC.CLAUSE ("HOL CLAUSE", t); |
140 | combterm_of _ _ (t as Abs _) = raise CLAUSE ("HOL CLAUSE", t); |
160 |
141 |
161 fun predicate_of dfg thy ((Const("Not",_) $ P), polarity) = predicate_of dfg thy (P, not polarity) |
142 fun predicate_of dfg thy ((@{const Not} $ P), polarity) = predicate_of dfg thy (P, not polarity) |
162 | predicate_of dfg thy (t,polarity) = (combterm_of dfg thy (Envir.eta_contract t), polarity); |
143 | predicate_of dfg thy (t,polarity) = (combterm_of dfg thy (Envir.eta_contract t), polarity); |
163 |
144 |
164 fun literals_of_term1 dfg thy args (Const("Trueprop",_) $ P) = literals_of_term1 dfg thy args P |
145 fun literals_of_term1 dfg thy args (@{const Trueprop} $ P) = literals_of_term1 dfg thy args P |
165 | literals_of_term1 dfg thy args (Const("op |",_) $ P $ Q) = |
146 | literals_of_term1 dfg thy args (@{const "op |"} $ P $ Q) = |
166 literals_of_term1 dfg thy (literals_of_term1 dfg thy args P) Q |
147 literals_of_term1 dfg thy (literals_of_term1 dfg thy args P) Q |
167 | literals_of_term1 dfg thy (lits,ts) P = |
148 | literals_of_term1 dfg thy (lits,ts) P = |
168 let val ((pred,ts'),pol) = predicate_of dfg thy (P,true) |
149 let val ((pred,ts'),pol) = predicate_of dfg thy (P,true) |
169 in |
150 in |
170 (Literal(pol,pred)::lits, union (op =) ts ts') |
151 (Literal(pol,pred)::lits, union (op =) ts ts') |
171 end; |
152 end; |
172 |
153 |
173 fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P; |
154 fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P; |
174 val literals_of_term = literals_of_term_dfg false; |
155 val literals_of_term = literals_of_term_dfg false; |
175 |
156 |
176 (* Problem too trivial for resolution (empty clause) *) |
157 (* Trivial problem, which resolution cannot handle (empty clause) *) |
177 exception TOO_TRIVIAL; |
158 exception TRIVIAL; |
178 |
159 |
179 (* making axiom and conjecture clauses *) |
160 (* making axiom and conjecture clauses *) |
180 fun make_clause dfg thy (clause_id,axiom_name,kind,th) = |
161 fun make_clause dfg thy (clause_id, axiom_name, kind, th) = |
181 let val (lits,ctypes_sorts) = literals_of_term_dfg dfg thy (prop_of th) |
162 let val (lits,ctypes_sorts) = literals_of_term_dfg dfg thy (prop_of th) |
182 in |
163 in |
183 if forall isFalse lits |
164 if forall isFalse lits then |
184 then raise TOO_TRIVIAL |
165 raise TRIVIAL |
185 else |
166 else |
186 Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind, |
167 HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th, |
187 literals = lits, ctypes_sorts = ctypes_sorts} |
168 kind = kind, literals = lits, ctypes_sorts = ctypes_sorts} |
188 end; |
169 end; |
189 |
170 |
190 |
171 |
191 fun add_axiom_clause dfg thy ((th,(name,id)), pairs) = |
172 fun add_axiom_clause dfg thy ((th,(name,id)), pairs) = |
192 let val cls = make_clause dfg thy (id, name, SFC.Axiom, th) |
173 let val cls = make_clause dfg thy (id, name, Axiom, th) |
193 in |
174 in |
194 if isTaut cls then pairs else (name,cls)::pairs |
175 if isTaut cls then pairs else (name,cls)::pairs |
195 end; |
176 end; |
196 |
177 |
197 fun make_axiom_clauses dfg thy = List.foldl (add_axiom_clause dfg thy) []; |
178 fun make_axiom_clauses dfg thy = List.foldl (add_axiom_clause dfg thy) []; |
198 |
179 |
199 fun make_conjecture_clauses_aux _ _ _ [] = [] |
180 fun make_conjecture_clauses_aux _ _ _ [] = [] |
200 | make_conjecture_clauses_aux dfg thy n (th::ths) = |
181 | make_conjecture_clauses_aux dfg thy n (th::ths) = |
201 make_clause dfg thy (n,"conjecture", SFC.Conjecture, th) :: |
182 make_clause dfg thy (n,"conjecture", Conjecture, th) :: |
202 make_conjecture_clauses_aux dfg thy (n+1) ths; |
183 make_conjecture_clauses_aux dfg thy (n+1) ths; |
203 |
184 |
204 fun make_conjecture_clauses dfg thy = make_conjecture_clauses_aux dfg thy 0; |
185 fun make_conjecture_clauses dfg thy = make_conjecture_clauses_aux dfg thy 0; |
205 |
186 |
206 |
187 |
249 val args1 = List.take(args, nargs) |
230 val args1 = List.take(args, nargs) |
250 handle Subscript => error ("string_of_applic: " ^ c ^ " has arity " ^ |
231 handle Subscript => error ("string_of_applic: " ^ c ^ " has arity " ^ |
251 Int.toString nargs ^ " but is applied to " ^ |
232 Int.toString nargs ^ " but is applied to " ^ |
252 space_implode ", " args) |
233 space_implode ", " args) |
253 val args2 = List.drop(args, nargs) |
234 val args2 = List.drop(args, nargs) |
254 val targs = if not t_full then map SFC.string_of_fol_type tvars |
235 val targs = if not t_full then map string_of_fol_type tvars else [] |
255 else [] |
|
256 in |
236 in |
257 string_apply (c ^ SFC.paren_pack (args1@targs), args2) |
237 string_apply (c ^ paren_pack (args1@targs), args2) |
258 end |
238 end |
259 | string_of_applic _ _ (CombVar (v, _), args) = string_apply (v, args) |
239 | string_of_applic _ _ (CombVar (v, _), args) = string_apply (v, args) |
260 | string_of_applic _ _ _ = error "string_of_applic"; |
240 | string_of_applic _ _ _ = error "string_of_applic"; |
261 |
241 |
262 fun wrap_type_if t_full cnh (head, s, tp) = |
242 fun wrap_type_if t_full cnh (head, s, tp) = |
263 if head_needs_hBOOL cnh head then wrap_type t_full (s, tp) else s; |
243 if head_needs_hBOOL cnh head then wrap_type t_full (s, tp) else s; |
264 |
244 |
265 fun string_of_combterm (params as (t_full, cma, cnh)) t = |
245 fun string_of_combterm (params as (t_full, cma, cnh)) t = |
266 let val (head, args) = strip_comb t |
246 let val (head, args) = strip_combterm_comb t |
267 in wrap_type_if t_full cnh (head, |
247 in wrap_type_if t_full cnh (head, |
268 string_of_applic t_full cma (head, map (string_of_combterm (params)) args), |
248 string_of_applic t_full cma (head, map (string_of_combterm (params)) args), |
269 type_of_combterm t) |
249 type_of_combterm t) |
270 end; |
250 end; |
271 |
251 |
272 (*Boolean-valued terms are here converted to literals.*) |
252 (*Boolean-valued terms are here converted to literals.*) |
273 fun boolify params t = |
253 fun boolify params t = |
274 "hBOOL" ^ SFC.paren_pack [string_of_combterm params t]; |
254 "hBOOL" ^ paren_pack [string_of_combterm params t]; |
275 |
255 |
276 fun string_of_predicate (params as (_,_,cnh)) t = |
256 fun string_of_predicate (params as (_,_,cnh)) t = |
277 case t of |
257 case t of |
278 (CombApp(CombApp(CombConst("equal",_,_), t1), t2)) => |
258 (CombApp(CombApp(CombConst("equal",_,_), t1), t2)) => |
279 (*DFG only: new TPTP prefers infix equality*) |
259 (*DFG only: new TPTP prefers infix equality*) |
280 ("equal" ^ SFC.paren_pack [string_of_combterm params t1, string_of_combterm params t2]) |
260 ("equal" ^ paren_pack [string_of_combterm params t1, string_of_combterm params t2]) |
281 | _ => |
261 | _ => |
282 case #1 (strip_comb t) of |
262 case #1 (strip_combterm_comb t) of |
283 CombConst(c,_,_) => if needs_hBOOL cnh c then boolify params t else string_of_combterm params t |
263 CombConst(c,_,_) => if needs_hBOOL cnh c then boolify params t else string_of_combterm params t |
284 | _ => boolify params t; |
264 | _ => boolify params t; |
285 |
265 |
286 |
266 |
287 (*** tptp format ***) |
267 (*** tptp format ***) |
288 |
268 |
289 fun tptp_of_equality params pol (t1,t2) = |
269 fun tptp_of_equality params pol (t1,t2) = |
290 let val eqop = if pol then " = " else " != " |
270 let val eqop = if pol then " = " else " != " |
291 in string_of_combterm params t1 ^ eqop ^ string_of_combterm params t2 end; |
271 in string_of_combterm params t1 ^ eqop ^ string_of_combterm params t2 end; |
292 |
272 |
293 fun tptp_literal params (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) = |
273 fun tptp_literal params (Literal(pol, CombApp(CombApp(CombConst("equal", _, _), t1), t2))) = |
294 tptp_of_equality params pol (t1,t2) |
274 tptp_of_equality params pol (t1,t2) |
295 | tptp_literal params (Literal(pol,pred)) = |
275 | tptp_literal params (Literal(pol,pred)) = |
296 SFC.tptp_sign pol (string_of_predicate params pred); |
276 tptp_sign pol (string_of_predicate params pred); |
297 |
277 |
298 (*Given a clause, returns its literals paired with a list of literals concerning TFrees; |
278 (*Given a clause, returns its literals paired with a list of literals concerning TFrees; |
299 the latter should only occur in conjecture clauses.*) |
279 the latter should only occur in conjecture clauses.*) |
300 fun tptp_type_lits params pos (Clause{literals, ctypes_sorts, ...}) = |
280 fun tptp_type_lits params pos (HOLClause {literals, ctypes_sorts, ...}) = |
301 (map (tptp_literal params) literals, |
281 (map (tptp_literal params) literals, |
302 map (SFC.tptp_of_typeLit pos) (SFC.add_typs ctypes_sorts)); |
282 map (tptp_of_typeLit pos) (add_typs ctypes_sorts)); |
303 |
283 |
304 fun clause2tptp params (cls as Clause {axiom_name, clause_id, kind, ...}) = |
284 fun clause2tptp params (cls as HOLClause {axiom_name, clause_id, kind, ...}) = |
305 let val (lits,tylits) = tptp_type_lits params (kind = SFC.Conjecture) cls |
285 let val (lits,tylits) = tptp_type_lits params (kind = Conjecture) cls |
306 in |
286 in |
307 (SFC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits) |
287 (gen_tptp_cls (clause_id, axiom_name, kind, lits, tylits), tylits) |
308 end; |
288 end; |
309 |
289 |
310 |
290 |
311 (*** dfg format ***) |
291 (*** dfg format ***) |
312 |
292 |
313 fun dfg_literal params (Literal(pol,pred)) = SFC.dfg_sign pol (string_of_predicate params pred); |
293 fun dfg_literal params (Literal(pol,pred)) = dfg_sign pol (string_of_predicate params pred); |
314 |
294 |
315 fun dfg_type_lits params pos (Clause{literals, ctypes_sorts, ...}) = |
295 fun dfg_type_lits params pos (HOLClause {literals, ctypes_sorts, ...}) = |
316 (map (dfg_literal params) literals, |
296 (map (dfg_literal params) literals, |
317 map (SFC.dfg_of_typeLit pos) (SFC.add_typs ctypes_sorts)); |
297 map (dfg_of_typeLit pos) (add_typs ctypes_sorts)); |
318 |
298 |
319 fun get_uvars (CombConst _) vars = vars |
299 fun get_uvars (CombConst _) vars = vars |
320 | get_uvars (CombVar(v,_)) vars = (v::vars) |
300 | get_uvars (CombVar(v,_)) vars = (v::vars) |
321 | get_uvars (CombApp(P,Q)) vars = get_uvars P (get_uvars Q vars); |
301 | get_uvars (CombApp(P,Q)) vars = get_uvars P (get_uvars Q vars); |
322 |
302 |
323 fun get_uvars_l (Literal(_,c)) = get_uvars c []; |
303 fun get_uvars_l (Literal(_,c)) = get_uvars c []; |
324 |
304 |
325 fun dfg_vars (Clause {literals,...}) = SFC.union_all (map get_uvars_l literals); |
305 fun dfg_vars (HOLClause {literals,...}) = union_all (map get_uvars_l literals); |
326 |
306 |
327 fun clause2dfg params (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) = |
307 fun clause2dfg params (cls as HOLClause {axiom_name, clause_id, kind, |
328 let val (lits,tylits) = dfg_type_lits params (kind = SFC.Conjecture) cls |
308 ctypes_sorts, ...}) = |
|
309 let val (lits,tylits) = dfg_type_lits params (kind = Conjecture) cls |
329 val vars = dfg_vars cls |
310 val vars = dfg_vars cls |
330 val tvars = SFC.get_tvar_strs ctypes_sorts |
311 val tvars = get_tvar_strs ctypes_sorts |
331 in |
312 in |
332 (SFC.gen_dfg_cls(clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits) |
313 (gen_dfg_cls (clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits) |
333 end; |
314 end; |
334 |
315 |
335 |
316 |
336 (** For DFG format: accumulate function and predicate declarations **) |
317 (** For DFG format: accumulate function and predicate declarations **) |
337 |
318 |
338 fun addtypes tvars tab = List.foldl SFC.add_foltype_funcs tab tvars; |
319 fun addtypes tvars tab = List.foldl add_foltype_funcs tab tvars; |
339 |
320 |
340 fun add_decls (t_full, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) = |
321 fun add_decls (t_full, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) = |
341 if c = "equal" then (addtypes tvars funcs, preds) |
322 if c = "equal" then (addtypes tvars funcs, preds) |
342 else |
323 else |
343 let val arity = min_arity_of cma c |
324 let val arity = min_arity_of cma c |
346 in |
327 in |
347 if needs_hBOOL cnh c then (addtypes tvars (addit funcs), preds) |
328 if needs_hBOOL cnh c then (addtypes tvars (addit funcs), preds) |
348 else (addtypes tvars funcs, addit preds) |
329 else (addtypes tvars funcs, addit preds) |
349 end |
330 end |
350 | add_decls _ (CombVar(_,ctp), (funcs,preds)) = |
331 | add_decls _ (CombVar(_,ctp), (funcs,preds)) = |
351 (SFC.add_foltype_funcs (ctp,funcs), preds) |
332 (add_foltype_funcs (ctp,funcs), preds) |
352 | add_decls params (CombApp(P,Q),decls) = add_decls params (P,add_decls params (Q,decls)); |
333 | add_decls params (CombApp(P,Q),decls) = add_decls params (P,add_decls params (Q,decls)); |
353 |
334 |
354 fun add_literal_decls params (Literal(_,c), decls) = add_decls params (c,decls); |
335 fun add_literal_decls params (Literal (_,c), decls) = add_decls params (c,decls); |
355 |
336 |
356 fun add_clause_decls params (Clause {literals, ...}, decls) = |
337 fun add_clause_decls params (HOLClause {literals, ...}, decls) = |
357 List.foldl (add_literal_decls params) decls literals |
338 List.foldl (add_literal_decls params) decls literals |
358 handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities") |
339 handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities") |
359 |
340 |
360 fun decls_of_clauses params clauses arity_clauses = |
341 fun decls_of_clauses params clauses arity_clauses = |
361 let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) SFC.init_functab) |
342 let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) init_functab) |
362 val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty |
343 val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty |
363 val (functab,predtab) = (List.foldl (add_clause_decls params) (init_functab, init_predtab) clauses) |
344 val (functab,predtab) = (List.foldl (add_clause_decls params) (init_functab, init_predtab) clauses) |
364 in |
345 in |
365 (Symtab.dest (List.foldl SFC.add_arityClause_funcs functab arity_clauses), |
346 (Symtab.dest (List.foldl add_arity_clause_funcs functab arity_clauses), |
366 Symtab.dest predtab) |
347 Symtab.dest predtab) |
367 end; |
348 end; |
368 |
349 |
369 fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) = |
350 fun add_clause_preds (HOLClause {ctypes_sorts, ...}, preds) = |
370 List.foldl SFC.add_type_sort_preds preds ctypes_sorts |
351 List.foldl add_type_sort_preds preds ctypes_sorts |
371 handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities") |
352 handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities") |
372 |
353 |
373 (*Higher-order clauses have only the predicates hBOOL and type classes.*) |
354 (*Higher-order clauses have only the predicates hBOOL and type classes.*) |
374 fun preds_of_clauses clauses clsrel_clauses arity_clauses = |
355 fun preds_of_clauses clauses clsrel_clauses arity_clauses = |
375 Symtab.dest |
356 Symtab.dest |
376 (List.foldl SFC.add_classrelClause_preds |
357 (List.foldl add_classrel_clause_preds |
377 (List.foldl SFC.add_arityClause_preds |
358 (List.foldl add_arity_clause_preds |
378 (List.foldl add_clause_preds Symtab.empty clauses) |
359 (List.foldl add_clause_preds Symtab.empty clauses) |
379 arity_clauses) |
360 arity_clauses) |
380 clsrel_clauses) |
361 clsrel_clauses) |
381 |
362 |
382 |
363 |
383 (**********************************************************************) |
364 (**********************************************************************) |
384 (* write clauses to files *) |
365 (* write clauses to files *) |
385 (**********************************************************************) |
366 (**********************************************************************) |
386 |
367 |
387 val init_counters = |
368 val init_counters = |
388 Symtab.make [("c_COMBI", 0), ("c_COMBK", 0), |
369 Symtab.make [("c_COMBI", 0), ("c_COMBK", 0), ("c_COMBB", 0), ("c_COMBC", 0), |
389 ("c_COMBB", 0), ("c_COMBC", 0), |
370 ("c_COMBS", 0)]; |
390 ("c_COMBS", 0)]; |
|
391 |
371 |
392 fun count_combterm (CombConst (c, _, _), ct) = |
372 fun count_combterm (CombConst (c, _, _), ct) = |
393 (case Symtab.lookup ct c of NONE => ct (*no counter*) |
373 (case Symtab.lookup ct c of NONE => ct (*no counter*) |
394 | SOME n => Symtab.update (c,n+1) ct) |
374 | SOME n => Symtab.update (c,n+1) ct) |
395 | count_combterm (CombVar _, ct) = ct |
375 | count_combterm (CombVar _, ct) = ct |
396 | count_combterm (CombApp(t1,t2), ct) = count_combterm(t1, count_combterm(t2, ct)); |
376 | count_combterm (CombApp(t1,t2), ct) = count_combterm(t1, count_combterm(t2, ct)); |
397 |
377 |
398 fun count_literal (Literal(_,t), ct) = count_combterm(t,ct); |
378 fun count_literal (Literal(_,t), ct) = count_combterm(t,ct); |
399 |
379 |
400 fun count_clause (Clause{literals,...}, ct) = List.foldl count_literal ct literals; |
380 fun count_clause (HOLClause {literals, ...}, ct) = |
401 |
381 List.foldl count_literal ct literals; |
402 fun count_user_clause user_lemmas (Clause{axiom_name,literals,...}, ct) = |
382 |
|
383 fun count_user_clause user_lemmas (HOLClause {axiom_name, literals, ...}, ct) = |
403 if axiom_name mem_string user_lemmas then List.foldl count_literal ct literals |
384 if axiom_name mem_string user_lemmas then List.foldl count_literal ct literals |
404 else ct; |
385 else ct; |
405 |
386 |
406 fun cnf_helper_thms thy = |
387 fun cnf_helper_thms thy = cnf_rules_pairs thy o map pairname |
407 Sledgehammer_Fact_Preprocessor.cnf_rules_pairs thy |
|
408 o map Sledgehammer_Fact_Preprocessor.pairname |
|
409 |
388 |
410 fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) = |
389 fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) = |
411 if isFO then [] (*first-order*) |
390 if isFO then |
|
391 [] |
412 else |
392 else |
413 let |
393 let |
414 val axclauses = map #2 (make_axiom_clauses dfg thy axcls) |
394 val axclauses = map #2 (make_axiom_clauses dfg thy axcls) |
415 val ct0 = List.foldl count_clause init_counters conjectures |
395 val ct0 = List.foldl count_clause init_counters conjectures |
416 val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses |
396 val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses |
417 fun needed c = the (Symtab.lookup ct c) > 0 |
397 fun needed c = the (Symtab.lookup ct c) > 0 |
418 val IK = if needed "c_COMBI" orelse needed "c_COMBK" |
398 val IK = if needed "c_COMBI" orelse needed "c_COMBK" |
419 then cnf_helper_thms thy [comb_I,comb_K] |
399 then cnf_helper_thms thy [@{thm COMBI_def}, @{thm COMBK_def}] |
420 else [] |
400 else [] |
421 val BC = if needed "c_COMBB" orelse needed "c_COMBC" |
401 val BC = if needed "c_COMBB" orelse needed "c_COMBC" |
422 then cnf_helper_thms thy [comb_B,comb_C] |
402 then cnf_helper_thms thy [@{thm COMBB_def}, @{thm COMBC_def}] |
423 else [] |
403 else [] |
424 val S = if needed "c_COMBS" |
404 val S = if needed "c_COMBS" then cnf_helper_thms thy [@{thm COMBS_def}] |
425 then cnf_helper_thms thy [comb_S] |
|
426 else [] |
405 else [] |
427 val other = cnf_helper_thms thy [fequal_imp_equal,equal_imp_fequal] |
406 val other = cnf_helper_thms thy [@{thm fequal_imp_equal}, |
|
407 @{thm equal_imp_fequal}] |
428 in |
408 in |
429 map #2 (make_axiom_clauses dfg thy (other @ IK @ BC @ S)) |
409 map #2 (make_axiom_clauses dfg thy (other @ IK @ BC @ S)) |
430 end; |
410 end; |
431 |
411 |
432 (*Find the minimal arity of each function mentioned in the term. Also, note which uses |
412 (*Find the minimal arity of each function mentioned in the term. Also, note which uses |
433 are not at top level, to see if hBOOL is needed.*) |
413 are not at top level, to see if hBOOL is needed.*) |
434 fun count_constants_term toplev t (const_min_arity, const_needs_hBOOL) = |
414 fun count_constants_term toplev t (const_min_arity, const_needs_hBOOL) = |
435 let val (head, args) = strip_comb t |
415 let val (head, args) = strip_combterm_comb t |
436 val n = length args |
416 val n = length args |
437 val (const_min_arity, const_needs_hBOOL) = fold (count_constants_term false) args (const_min_arity, const_needs_hBOOL) |
417 val (const_min_arity, const_needs_hBOOL) = fold (count_constants_term false) args (const_min_arity, const_needs_hBOOL) |
438 in |
418 in |
439 case head of |
419 case head of |
440 CombConst (a,_,_) => (*predicate or function version of "equal"?*) |
420 CombConst (a,_,_) => (*predicate or function version of "equal"?*) |
467 |> fold count_constants_clause helper_clauses |
448 |> fold count_constants_clause helper_clauses |
468 val _ = List.app (display_arity const_needs_hBOOL) (Symtab.dest (const_min_arity)) |
449 val _ = List.app (display_arity const_needs_hBOOL) (Symtab.dest (const_min_arity)) |
469 in (const_min_arity, const_needs_hBOOL) end |
450 in (const_min_arity, const_needs_hBOOL) end |
470 else (Symtab.empty, Symtab.empty); |
451 else (Symtab.empty, Symtab.empty); |
471 |
452 |
472 (* tptp format *) |
453 (* TPTP format *) |
473 |
454 |
474 fun tptp_write_file t_full file clauses = |
455 fun write_tptp_file t_full file clauses = |
475 let |
456 let |
476 val (conjectures, axclauses, _, helper_clauses, |
457 val (conjectures, axclauses, _, helper_clauses, |
477 classrel_clauses, arity_clauses) = clauses |
458 classrel_clauses, arity_clauses) = clauses |
478 val (cma, cnh) = count_constants clauses |
459 val (cma, cnh) = count_constants clauses |
479 val params = (t_full, cma, cnh) |
460 val params = (t_full, cma, cnh) |
480 val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures) |
461 val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures) |
481 val tfree_clss = map SFC.tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss) |
462 val tfree_clss = map tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss) |
482 val _ = |
463 val _ = |
483 File.write_list file ( |
464 File.write_list file ( |
484 map (#1 o (clause2tptp params)) axclauses @ |
465 map (#1 o (clause2tptp params)) axclauses @ |
485 tfree_clss @ |
466 tfree_clss @ |
486 tptp_clss @ |
467 tptp_clss @ |
487 map SFC.tptp_classrelClause classrel_clauses @ |
468 map tptp_classrel_clause classrel_clauses @ |
488 map SFC.tptp_arity_clause arity_clauses @ |
469 map tptp_arity_clause arity_clauses @ |
489 map (#1 o (clause2tptp params)) helper_clauses) |
470 map (#1 o (clause2tptp params)) helper_clauses) |
490 in (length axclauses + 1, length tfree_clss + length tptp_clss) |
471 in (length axclauses + 1, length tfree_clss + length tptp_clss) |
491 end; |
472 end; |
492 |
473 |
493 |
474 |
494 (* dfg format *) |
475 (* DFG format *) |
495 |
476 |
496 fun dfg_write_file t_full file clauses = |
477 fun write_dfg_file t_full file clauses = |
497 let |
478 let |
498 val (conjectures, axclauses, _, helper_clauses, |
479 val (conjectures, axclauses, _, helper_clauses, |
499 classrel_clauses, arity_clauses) = clauses |
480 classrel_clauses, arity_clauses) = clauses |
500 val (cma, cnh) = count_constants clauses |
481 val (cma, cnh) = count_constants clauses |
501 val params = (t_full, cma, cnh) |
482 val params = (t_full, cma, cnh) |
502 val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures) |
483 val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures) |
503 and probname = Path.implode (Path.base file) |
484 and probname = Path.implode (Path.base file) |
504 val axstrs = map (#1 o (clause2dfg params)) axclauses |
485 val axstrs = map (#1 o (clause2dfg params)) axclauses |
505 val tfree_clss = map SFC.dfg_tfree_clause (SFC.union_all tfree_litss) |
486 val tfree_clss = map dfg_tfree_clause (union_all tfree_litss) |
506 val helper_clauses_strs = map (#1 o (clause2dfg params)) helper_clauses |
487 val helper_clauses_strs = map (#1 o (clause2dfg params)) helper_clauses |
507 val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses |
488 val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses |
508 and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses |
489 and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses |
509 val _ = |
490 val _ = |
510 File.write_list file ( |
491 File.write_list file ( |
511 SFC.string_of_start probname :: |
492 string_of_start probname :: |
512 SFC.string_of_descrip probname :: |
493 string_of_descrip probname :: |
513 SFC.string_of_symbols (SFC.string_of_funcs funcs) |
494 string_of_symbols (string_of_funcs funcs) |
514 (SFC.string_of_preds (cl_preds @ ty_preds)) :: |
495 (string_of_preds (cl_preds @ ty_preds)) :: |
515 "list_of_clauses(axioms,cnf).\n" :: |
496 "list_of_clauses(axioms,cnf).\n" :: |
516 axstrs @ |
497 axstrs @ |
517 map SFC.dfg_classrelClause classrel_clauses @ |
498 map dfg_classrel_clause classrel_clauses @ |
518 map SFC.dfg_arity_clause arity_clauses @ |
499 map dfg_arity_clause arity_clauses @ |
519 helper_clauses_strs @ |
500 helper_clauses_strs @ |
520 ["end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"] @ |
501 ["end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"] @ |
521 tfree_clss @ |
502 tfree_clss @ |
522 dfg_clss @ |
503 dfg_clss @ |
523 ["end_of_list.\n\n", |
504 ["end_of_list.\n\n", |