1 (* Title: HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML |
|
2 Author: Jia Meng, NICTA |
|
3 Author: Jasmin Blanchette, TU Muenchen |
|
4 |
|
5 FOL clauses translated from HOL formulas. |
|
6 *) |
|
7 |
|
8 signature SLEDGEHAMMER_HOL_CLAUSE = |
|
9 sig |
|
10 type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm |
|
11 type name = Sledgehammer_FOL_Clause.name |
|
12 type name_pool = Sledgehammer_FOL_Clause.name_pool |
|
13 type kind = Sledgehammer_FOL_Clause.kind |
|
14 type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause |
|
15 type arity_clause = Sledgehammer_FOL_Clause.arity_clause |
|
16 type polarity = bool |
|
17 |
|
18 datatype combtyp = |
|
19 TyVar of name | |
|
20 TyFree of name | |
|
21 TyConstr of name * combtyp list |
|
22 datatype combterm = |
|
23 CombConst of name * combtyp * combtyp list (* Const and Free *) | |
|
24 CombVar of name * combtyp | |
|
25 CombApp of combterm * combterm |
|
26 datatype literal = Literal of polarity * combterm |
|
27 datatype hol_clause = |
|
28 HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind, |
|
29 literals: literal list, ctypes_sorts: typ list} |
|
30 |
|
31 val type_of_combterm : combterm -> combtyp |
|
32 val strip_combterm_comb : combterm -> combterm * combterm list |
|
33 val literals_of_term : theory -> term -> literal list * typ list |
|
34 val conceal_skolem_somes : |
|
35 int -> (string * term) list -> term -> (string * term) list * term |
|
36 exception TRIVIAL of unit |
|
37 val make_conjecture_clauses : theory -> thm list -> hol_clause list |
|
38 val make_axiom_clauses : theory -> cnf_thm list -> (string * hol_clause) list |
|
39 end |
|
40 |
|
41 structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE = |
|
42 struct |
|
43 |
|
44 open Sledgehammer_Util |
|
45 open Sledgehammer_FOL_Clause |
|
46 open Sledgehammer_Fact_Preprocessor |
|
47 |
|
48 (******************************************************) |
|
49 (* data types for typed combinator expressions *) |
|
50 (******************************************************) |
|
51 |
|
52 type polarity = bool |
|
53 |
|
54 datatype combtyp = |
|
55 TyVar of name | |
|
56 TyFree of name | |
|
57 TyConstr of name * combtyp list |
|
58 |
|
59 datatype combterm = |
|
60 CombConst of name * combtyp * combtyp list (* Const and Free *) | |
|
61 CombVar of name * combtyp | |
|
62 CombApp of combterm * combterm |
|
63 |
|
64 datatype literal = Literal of polarity * combterm; |
|
65 |
|
66 datatype hol_clause = |
|
67 HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind, |
|
68 literals: literal list, ctypes_sorts: typ list} |
|
69 |
|
70 (*********************************************************************) |
|
71 (* convert a clause with type Term.term to a clause with type clause *) |
|
72 (*********************************************************************) |
|
73 |
|
74 (*Result of a function type; no need to check that the argument type matches.*) |
|
75 fun result_type (TyConstr (_, [_, tp2])) = tp2 |
|
76 | result_type _ = raise Fail "non-function type" |
|
77 |
|
78 fun type_of_combterm (CombConst (_, tp, _)) = tp |
|
79 | type_of_combterm (CombVar (_, tp)) = tp |
|
80 | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1) |
|
81 |
|
82 (*gets the head of a combinator application, along with the list of arguments*) |
|
83 fun strip_combterm_comb u = |
|
84 let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts) |
|
85 | stripc x = x |
|
86 in stripc(u,[]) end |
|
87 |
|
88 fun isFalse (Literal (pol, CombConst ((c, _), _, _))) = |
|
89 (pol andalso c = "c_False") orelse (not pol andalso c = "c_True") |
|
90 | isFalse _ = false; |
|
91 |
|
92 fun isTrue (Literal (pol, CombConst ((c, _), _, _))) = |
|
93 (pol andalso c = "c_True") orelse |
|
94 (not pol andalso c = "c_False") |
|
95 | isTrue _ = false; |
|
96 |
|
97 fun isTaut (HOLClause {literals,...}) = exists isTrue literals; |
|
98 |
|
99 fun type_of (Type (a, Ts)) = |
|
100 let val (folTypes,ts) = types_of Ts in |
|
101 (TyConstr (`make_fixed_type_const a, folTypes), ts) |
|
102 end |
|
103 | type_of (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp]) |
|
104 | type_of (tp as TVar (x, _)) = |
|
105 (TyVar (make_schematic_type_var x, string_of_indexname x), [tp]) |
|
106 and types_of Ts = |
|
107 let val (folTyps, ts) = ListPair.unzip (map type_of Ts) in |
|
108 (folTyps, union_all ts) |
|
109 end |
|
110 |
|
111 (* same as above, but no gathering of sort information *) |
|
112 fun simp_type_of (Type (a, Ts)) = |
|
113 TyConstr (`make_fixed_type_const a, map simp_type_of Ts) |
|
114 | simp_type_of (TFree (a, _)) = TyFree (`make_fixed_type_var a) |
|
115 | simp_type_of (TVar (x, _)) = |
|
116 TyVar (make_schematic_type_var x, string_of_indexname x) |
|
117 |
|
118 (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *) |
|
119 fun combterm_of thy (Const (c, T)) = |
|
120 let |
|
121 val (tp, ts) = type_of T |
|
122 val tvar_list = |
|
123 (if String.isPrefix skolem_theory_name c then |
|
124 [] |> Term.add_tvarsT T |> map TVar |
|
125 else |
|
126 (c, T) |> Sign.const_typargs thy) |
|
127 |> map simp_type_of |
|
128 val c' = CombConst (`make_fixed_const c, tp, tvar_list) |
|
129 in (c',ts) end |
|
130 | combterm_of _ (Free(v, T)) = |
|
131 let val (tp,ts) = type_of T |
|
132 val v' = CombConst (`make_fixed_var v, tp, []) |
|
133 in (v',ts) end |
|
134 | combterm_of _ (Var(v, T)) = |
|
135 let val (tp,ts) = type_of T |
|
136 val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp) |
|
137 in (v',ts) end |
|
138 | combterm_of thy (P $ Q) = |
|
139 let val (P', tsP) = combterm_of thy P |
|
140 val (Q', tsQ) = combterm_of thy Q |
|
141 in (CombApp (P', Q'), union (op =) tsP tsQ) end |
|
142 | combterm_of _ (t as Abs _) = raise CLAUSE ("HOL clause", t) |
|
143 |
|
144 fun predicate_of thy ((@{const Not} $ P), polarity) = |
|
145 predicate_of thy (P, not polarity) |
|
146 | predicate_of thy (t, polarity) = |
|
147 (combterm_of thy (Envir.eta_contract t), polarity) |
|
148 |
|
149 fun literals_of_term1 args thy (@{const Trueprop} $ P) = |
|
150 literals_of_term1 args thy P |
|
151 | literals_of_term1 args thy (@{const "op |"} $ P $ Q) = |
|
152 literals_of_term1 (literals_of_term1 args thy P) thy Q |
|
153 | literals_of_term1 (lits, ts) thy P = |
|
154 let val ((pred, ts'), pol) = predicate_of thy (P, true) in |
|
155 (Literal (pol, pred) :: lits, union (op =) ts ts') |
|
156 end |
|
157 val literals_of_term = literals_of_term1 ([], []) |
|
158 |
|
159 fun skolem_name i j num_T_args = |
|
160 skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^ |
|
161 skolem_infix ^ "g" |
|
162 |
|
163 fun conceal_skolem_somes i skolem_somes t = |
|
164 if exists_Const (curry (op =) @{const_name skolem_id} o fst) t then |
|
165 let |
|
166 fun aux skolem_somes |
|
167 (t as (Const (@{const_name skolem_id}, Type (_, [_, T])) $ _)) = |
|
168 let |
|
169 val (skolem_somes, s) = |
|
170 if i = ~1 then |
|
171 (skolem_somes, @{const_name undefined}) |
|
172 else case AList.find (op aconv) skolem_somes t of |
|
173 s :: _ => (skolem_somes, s) |
|
174 | [] => |
|
175 let |
|
176 val s = skolem_theory_name ^ "." ^ |
|
177 skolem_name i (length skolem_somes) |
|
178 (length (Term.add_tvarsT T [])) |
|
179 in ((s, t) :: skolem_somes, s) end |
|
180 in (skolem_somes, Const (s, T)) end |
|
181 | aux skolem_somes (t1 $ t2) = |
|
182 let |
|
183 val (skolem_somes, t1) = aux skolem_somes t1 |
|
184 val (skolem_somes, t2) = aux skolem_somes t2 |
|
185 in (skolem_somes, t1 $ t2) end |
|
186 | aux skolem_somes (Abs (s, T, t')) = |
|
187 let val (skolem_somes, t') = aux skolem_somes t' in |
|
188 (skolem_somes, Abs (s, T, t')) |
|
189 end |
|
190 | aux skolem_somes t = (skolem_somes, t) |
|
191 in aux skolem_somes t end |
|
192 else |
|
193 (skolem_somes, t) |
|
194 |
|
195 (* Trivial problem, which resolution cannot handle (empty clause) *) |
|
196 exception TRIVIAL of unit |
|
197 |
|
198 (* making axiom and conjecture clauses *) |
|
199 fun make_clause thy (clause_id, axiom_name, kind, th) skolem_somes = |
|
200 let |
|
201 val (skolem_somes, t) = |
|
202 th |> prop_of |> conceal_skolem_somes clause_id skolem_somes |
|
203 val (lits, ctypes_sorts) = literals_of_term thy t |
|
204 in |
|
205 if forall isFalse lits then |
|
206 raise TRIVIAL () |
|
207 else |
|
208 (skolem_somes, |
|
209 HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th, |
|
210 kind = kind, literals = lits, ctypes_sorts = ctypes_sorts}) |
|
211 end |
|
212 |
|
213 fun add_axiom_clause thy (th, ((name, id), _ : thm)) (skolem_somes, clss) = |
|
214 let |
|
215 val (skolem_somes, cls) = make_clause thy (id, name, Axiom, th) skolem_somes |
|
216 in (skolem_somes, clss |> not (isTaut cls) ? cons (name, cls)) end |
|
217 |
|
218 fun make_axiom_clauses thy clauses = |
|
219 ([], []) |> fold_rev (add_axiom_clause thy) clauses |> snd |
|
220 |
|
221 fun make_conjecture_clauses thy = |
|
222 let |
|
223 fun aux _ _ [] = [] |
|
224 | aux n skolem_somes (th :: ths) = |
|
225 let |
|
226 val (skolem_somes, cls) = |
|
227 make_clause thy (n, "conjecture", Conjecture, th) skolem_somes |
|
228 in cls :: aux (n + 1) skolem_somes ths end |
|
229 in aux 0 [] end |
|
230 |
|
231 end; |
|