author | paulson |
Tue, 28 Nov 2006 16:19:01 +0100 | |
changeset 21573 | 8a7a68c0096c |
parent 21561 | cfd2258f0b23 |
child 21617 | 4664489469fc |
permissions | -rw-r--r-- |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
1 |
(* ID: $Id$ |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
2 |
Author: Jia Meng, NICTA |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
3 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
4 |
FOL clauses translated from HOL formulae. Combinators are used to represent lambda terms. |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
5 |
*) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
6 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
7 |
structure ResHolClause = |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
8 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
9 |
struct |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
10 |
|
20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
11 |
(* theorems for combinators and function extensionality *) |
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
12 |
val ext = thm "HOL.ext"; |
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset
|
13 |
val comb_I = thm "ATP_Linkup.COMBI_def"; |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset
|
14 |
val comb_K = thm "ATP_Linkup.COMBK_def"; |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset
|
15 |
val comb_B = thm "ATP_Linkup.COMBB_def"; |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset
|
16 |
val comb_C = thm "ATP_Linkup.COMBC_def"; |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset
|
17 |
val comb_S = thm "ATP_Linkup.COMBS_def"; |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset
|
18 |
val comb_B' = thm "ATP_Linkup.COMBB'_def"; |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset
|
19 |
val comb_C' = thm "ATP_Linkup.COMBC'_def"; |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset
|
20 |
val comb_S' = thm "ATP_Linkup.COMBS'_def"; |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset
|
21 |
val fequal_imp_equal = thm "ATP_Linkup.fequal_imp_equal"; |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset
|
22 |
val equal_imp_fequal = thm "ATP_Linkup.equal_imp_fequal"; |
20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
23 |
|
21108 | 24 |
(*A flag to set if we use the Turner optimizations. Currently FALSE, as the 5 standard |
20997 | 25 |
combinators appear to work best.*) |
21108 | 26 |
val use_Turner = ref false; |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
27 |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
28 |
val const_typargs = ref (Library.K [] : (string*typ -> typ list)); |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
29 |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
30 |
fun init thy = (const_typargs := Sign.const_typargs thy); |
19198
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
31 |
|
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
32 |
(**********************************************************************) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
33 |
(* convert a Term.term with lambdas into a Term.term with combinators *) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
34 |
(**********************************************************************) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
35 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
36 |
fun is_free (Bound(a)) n = (a = n) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
37 |
| is_free (Abs(x,_,b)) n = (is_free b (n+1)) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
38 |
| is_free (P $ Q) n = ((is_free P n) orelse (is_free Q n)) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
39 |
| is_free _ _ = false; |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
40 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
41 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
42 |
(*******************************************) |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
43 |
fun mk_compact_comb (tm as (Const("ATP_Linkup.COMBB",_)$p) $ (Const("ATP_Linkup.COMBB",_)$q$r)) bnds = |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
44 |
let val tp_p = Term.type_of1(bnds,p) |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
45 |
val tp_q = Term.type_of1(bnds,q) |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
46 |
val tp_r = Term.type_of1(bnds,r) |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
47 |
val typ = Term.type_of1(bnds,tm) |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
48 |
val typ_B' = [tp_p,tp_q,tp_r] ---> typ |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
49 |
in |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
50 |
Const("ATP_Linkup.COMBB'",typ_B') $ p $ q $ r |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
51 |
end |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
52 |
| mk_compact_comb (tm as (Const("ATP_Linkup.COMBC",_) $ (Const("ATP_Linkup.COMBB",_)$p$q) $ r)) bnds = |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
53 |
let val tp_p = Term.type_of1(bnds,p) |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
54 |
val tp_q = Term.type_of1(bnds,q) |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
55 |
val tp_r = Term.type_of1(bnds,r) |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
56 |
val typ = Term.type_of1(bnds,tm) |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
57 |
val typ_C' = [tp_p,tp_q,tp_r] ---> typ |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
58 |
in |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
59 |
Const("ATP_Linkup.COMBC'",typ_C') $ p $ q $ r |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
60 |
end |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
61 |
| mk_compact_comb (tm as (Const("ATP_Linkup.COMBS",_) $ (Const("ATP_Linkup.COMBB",_)$p$q) $ r)) bnds = |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
62 |
let val tp_p = Term.type_of1(bnds,p) |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
63 |
val tp_q = Term.type_of1(bnds,q) |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
64 |
val tp_r = Term.type_of1(bnds,r) |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
65 |
val typ = Term.type_of1(bnds,tm) |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
66 |
val typ_S' = [tp_p,tp_q,tp_r] ---> typ |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
67 |
in |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
68 |
Const("ATP_Linkup.COMBS'",typ_S') $ p $ q $ r |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
69 |
end |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
70 |
| mk_compact_comb tm _ = tm; |
20644 | 71 |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
72 |
fun compact_comb t bnds = |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
73 |
if !use_Turner then mk_compact_comb t bnds else t; |
20644 | 74 |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
75 |
fun lam2comb (Abs(x,tp,Bound 0)) _ = Const("ATP_Linkup.COMBI",tp-->tp) |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
76 |
| lam2comb (Abs(x,tp,Bound n)) bnds = |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
77 |
let val tb = List.nth(bnds,n-1) |
21108 | 78 |
in |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
79 |
Const("ATP_Linkup.COMBK", [tb,tp] ---> tb) $ Bound (n-1) |
21108 | 80 |
end |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
81 |
| lam2comb (Abs(x,t1,Const(c,t2))) _ = Const("ATP_Linkup.COMBK",[t2,t1] ---> t2) $ Const(c,t2) |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
82 |
| lam2comb (Abs(x,t1,Free(v,t2))) _ = Const("ATP_Linkup.COMBK",[t2,t1] ---> t2) $ Free(v,t2) |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
83 |
| lam2comb (Abs(x,t1,Var(ind,t2))) _ = Const("ATP_Linkup.COMBK", [t2,t1] ---> t2) $ Var(ind,t2) |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
84 |
| lam2comb (t as (Abs(x,t1,P$(Bound 0)))) bnds = |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
85 |
if is_free P 0 then |
21135 | 86 |
let val tI = [t1] ---> t1 |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
87 |
val P' = lam2comb (Abs(x,t1,P)) bnds |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
88 |
val tp' = Term.type_of1(bnds,P') |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
89 |
val tr = Term.type_of1(t1::bnds,P) |
21135 | 90 |
val tS = [tp',tI] ---> tr |
21108 | 91 |
in |
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset
|
92 |
compact_comb (Const("ATP_Linkup.COMBS",tS) $ P' $ |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
93 |
Const("ATP_Linkup.COMBI",tI)) bnds |
21108 | 94 |
end |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
95 |
else incr_boundvars ~1 P |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
96 |
| lam2comb (t as (Abs(x,t1,P$Q))) bnds = |
21108 | 97 |
let val nfreeP = not(is_free P 0) |
98 |
and nfreeQ = not(is_free Q 0) |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
99 |
val tpq = Term.type_of1(t1::bnds, P$Q) |
21108 | 100 |
in |
101 |
if nfreeP andalso nfreeQ |
|
102 |
then |
|
21135 | 103 |
let val tK = [tpq,t1] ---> tpq |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
104 |
val PQ' = incr_boundvars ~1 (P $ Q) |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
105 |
in |
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset
|
106 |
Const("ATP_Linkup.COMBK",tK) $ PQ' |
21108 | 107 |
end |
108 |
else if nfreeP then |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
109 |
let val Q' = lam2comb (Abs(x,t1,Q)) bnds |
21135 | 110 |
val P' = incr_boundvars ~1 P |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
111 |
val tp = Term.type_of1(bnds,P') |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
112 |
val tq' = Term.type_of1(bnds, Q') |
21135 | 113 |
val tB = [tp,tq',t1] ---> tpq |
21108 | 114 |
in |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
115 |
compact_comb (Const("ATP_Linkup.COMBB",tB) $ P' $ Q') bnds |
21108 | 116 |
end |
117 |
else if nfreeQ then |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
118 |
let val P' = lam2comb (Abs(x,t1,P)) bnds |
21135 | 119 |
val Q' = incr_boundvars ~1 Q |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
120 |
val tq = Term.type_of1(bnds,Q') |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
121 |
val tp' = Term.type_of1(bnds, P') |
21135 | 122 |
val tC = [tp',tq,t1] ---> tpq |
21108 | 123 |
in |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
124 |
compact_comb (Const("ATP_Linkup.COMBC",tC) $ P' $ Q') bnds |
21108 | 125 |
end |
126 |
else |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
127 |
let val P' = lam2comb (Abs(x,t1,P)) bnds |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
128 |
val Q' = lam2comb (Abs(x,t1,Q)) bnds |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
129 |
val tp' = Term.type_of1(bnds,P') |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
130 |
val tq' = Term.type_of1(bnds,Q') |
21135 | 131 |
val tS = [tp',tq',t1] ---> tpq |
21108 | 132 |
in |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
133 |
compact_comb (Const("ATP_Linkup.COMBS",tS) $ P' $ Q') bnds |
21108 | 134 |
end |
135 |
end |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
136 |
| lam2comb (t as (Abs(x,t1,_))) _ = raise ResClause.CLAUSE("HOL CLAUSE",t); |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
137 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
138 |
(*********************) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
139 |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
140 |
fun to_comb (Abs(x,tp,b)) bnds = |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
141 |
lam2comb (Abs(x, tp, to_comb b (tp::bnds))) bnds |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
142 |
| to_comb (P $ Q) bnds = (to_comb P bnds) $ (to_comb Q bnds) |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
143 |
| to_comb t _ = t; |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
144 |
|
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
145 |
(* print a term containing combinators, used for debugging *) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
146 |
exception TERM_COMB of term; |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
147 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
148 |
fun string_of_term (Const(c,t)) = c |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
149 |
| string_of_term (Free(v,t)) = v |
20360 | 150 |
| string_of_term (Var((x,n),t)) = x ^ "_" ^ (string_of_int n) |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
151 |
| string_of_term (P $ Q) = |
20360 | 152 |
"(" ^ string_of_term P ^ " " ^ string_of_term Q ^ ")" |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
153 |
| string_of_term t = raise TERM_COMB (t); |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
154 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
155 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
156 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
157 |
(******************************************************) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
158 |
(* data types for typed combinator expressions *) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
159 |
(******************************************************) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
160 |
|
20281
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
mengj
parents:
20274
diff
changeset
|
161 |
datatype type_level = T_FULL | T_PARTIAL | T_CONST | T_NONE; |
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
mengj
parents:
20274
diff
changeset
|
162 |
|
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
mengj
parents:
20274
diff
changeset
|
163 |
val typ_level = ref T_CONST; |
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
mengj
parents:
20274
diff
changeset
|
164 |
|
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
mengj
parents:
20274
diff
changeset
|
165 |
fun full_types () = (typ_level:=T_FULL); |
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
mengj
parents:
20274
diff
changeset
|
166 |
fun partial_types () = (typ_level:=T_PARTIAL); |
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
mengj
parents:
20274
diff
changeset
|
167 |
fun const_types_only () = (typ_level:=T_CONST); |
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
mengj
parents:
20274
diff
changeset
|
168 |
fun no_types () = (typ_level:=T_NONE); |
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
mengj
parents:
20274
diff
changeset
|
169 |
|
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
mengj
parents:
20274
diff
changeset
|
170 |
fun find_typ_level () = !typ_level; |
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
mengj
parents:
20274
diff
changeset
|
171 |
|
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
172 |
type axiom_name = string; |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
173 |
type polarity = bool; |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
174 |
type clause_id = int; |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
175 |
|
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
176 |
datatype combterm = CombConst of string * ResClause.fol_type * ResClause.fol_type list |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
177 |
| CombFree of string * ResClause.fol_type |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
178 |
| CombVar of string * ResClause.fol_type |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
179 |
| CombApp of combterm * combterm * ResClause.fol_type |
20360 | 180 |
|
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
181 |
datatype literal = Literal of polarity * combterm; |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
182 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
183 |
datatype clause = |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
184 |
Clause of {clause_id: clause_id, |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
185 |
axiom_name: axiom_name, |
19964 | 186 |
th: thm, |
21509
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset
|
187 |
kind: ResClause.kind, |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
188 |
literals: literal list, |
21561 | 189 |
ctypes_sorts: (ResClause.typ_var * Term.sort) list, |
190 |
ctvar_type_literals: ResClause.type_literal list, |
|
191 |
ctfree_type_literals: ResClause.type_literal list}; |
|
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
192 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
193 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
194 |
(*********************************************************************) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
195 |
(* convert a clause with type Term.term to a clause with type clause *) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
196 |
(*********************************************************************) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
197 |
|
21561 | 198 |
fun isFalse (Literal(pol, CombConst(c,_,_))) = |
20360 | 199 |
(pol andalso c = "c_False") orelse |
200 |
(not pol andalso c = "c_True") |
|
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
201 |
| isFalse _ = false; |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
202 |
|
21561 | 203 |
fun isTrue (Literal (pol, CombConst(c,_,_))) = |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
204 |
(pol andalso c = "c_True") orelse |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
205 |
(not pol andalso c = "c_False") |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
206 |
| isTrue _ = false; |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
207 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
208 |
fun isTaut (Clause {literals,...}) = exists isTrue literals; |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
209 |
|
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
210 |
fun type_of (Type (a, Ts)) = |
21561 | 211 |
let val (folTypes,ts) = types_of Ts |
212 |
val t = ResClause.make_fixed_type_const a |
|
213 |
in |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
214 |
(ResClause.mk_fol_type("Comp",t,folTypes), ts) |
21561 | 215 |
end |
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
216 |
| type_of (tp as (TFree(a,s))) = |
21561 | 217 |
let val t = ResClause.make_fixed_type_var a |
218 |
in |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
219 |
(ResClause.mk_fol_type("Fixed",t,[]), [ResClause.mk_typ_var_sort tp]) |
21561 | 220 |
end |
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
221 |
| type_of (tp as (TVar(v,s))) = |
21561 | 222 |
let val t = ResClause.make_schematic_type_var v |
223 |
in |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
224 |
(ResClause.mk_fol_type("Var",t,[]), [ResClause.mk_typ_var_sort tp]) |
21561 | 225 |
end |
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
226 |
and types_of Ts = |
21561 | 227 |
let val foltyps_ts = map type_of Ts |
228 |
val (folTyps,ts) = ListPair.unzip foltyps_ts |
|
229 |
in |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
230 |
(folTyps, ResClause.union_all ts) |
21561 | 231 |
end; |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
232 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
233 |
(* same as above, but no gathering of sort information *) |
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
234 |
fun simp_type_of (Type (a, Ts)) = |
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
235 |
let val typs = map simp_type_of Ts |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
236 |
val t = ResClause.make_fixed_type_const a |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
237 |
in |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
238 |
ResClause.mk_fol_type("Comp",t,typs) |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
239 |
end |
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
240 |
| simp_type_of (TFree (a,s)) = ResClause.mk_fol_type("Fixed",ResClause.make_fixed_type_var a,[]) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
241 |
| simp_type_of (TVar (v,s)) = ResClause.mk_fol_type("Var",ResClause.make_schematic_type_var v,[]); |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
242 |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
243 |
|
20865
2cfa020109c1
Changed and removed some functions related to combinators, since they are Isabelle constants now.
mengj
parents:
20864
diff
changeset
|
244 |
fun const_type_of (c,t) = |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
245 |
let val (tp,ts) = type_of t |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
246 |
val tvars = !const_typargs(c,t) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
247 |
in |
21561 | 248 |
(tp, ts, map simp_type_of tvars) |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
249 |
end; |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
250 |
|
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
251 |
(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
252 |
fun combterm_of (Const(c,t)) = |
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
253 |
let val (tp,ts,tvar_list) = const_type_of (c,t) |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
254 |
val c' = CombConst(ResClause.make_fixed_const c,tp,tvar_list) |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
255 |
in |
21561 | 256 |
(c',ts) |
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
257 |
end |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
258 |
| combterm_of (Free(v,t)) = |
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
259 |
let val (tp,ts) = type_of t |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
260 |
val v' = if ResClause.isMeta v then CombVar(ResClause.make_schematic_var(v,0),tp) |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
261 |
else CombFree(ResClause.make_fixed_var v,tp) |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
262 |
in |
21561 | 263 |
(v',ts) |
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
264 |
end |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
265 |
| combterm_of (Var(v,t)) = |
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
266 |
let val (tp,ts) = type_of t |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
267 |
val v' = CombVar(ResClause.make_schematic_var v,tp) |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
268 |
in |
21561 | 269 |
(v',ts) |
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
270 |
end |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
271 |
| combterm_of (t as (P $ Q)) = |
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
272 |
let val (P',tsP) = combterm_of P |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
273 |
val (Q',tsQ) = combterm_of Q |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
274 |
val tp = Term.type_of t |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
275 |
val t' = CombApp(P',Q', simp_type_of tp) |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
276 |
in |
21561 | 277 |
(t',tsP union tsQ) |
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
278 |
end; |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
279 |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
280 |
fun predicate_of ((Const("Not",_) $ P), polarity) = predicate_of (P, not polarity) |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
281 |
| predicate_of (t,polarity) = (combterm_of t, polarity); |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
282 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
283 |
fun literals_of_term1 args (Const("Trueprop",_) $ P) = literals_of_term1 args P |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
284 |
| literals_of_term1 args (Const("op |",_) $ P $ Q) = |
21509
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset
|
285 |
literals_of_term1 (literals_of_term1 args P) Q |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
286 |
| literals_of_term1 (lits,ts) P = |
21509
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset
|
287 |
let val ((pred,ts'),pol) = predicate_of (P,true) |
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset
|
288 |
in |
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset
|
289 |
(Literal(pol,pred)::lits, ts union ts') |
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset
|
290 |
end; |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
291 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
292 |
fun literals_of_term P = literals_of_term1 ([],[]) P; |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
293 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
294 |
(* making axiom and conjecture clauses *) |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
295 |
fun make_clause(clause_id,axiom_name,kind,th) = |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
296 |
let val (lits,ctypes_sorts) = literals_of_term (to_comb (prop_of th) []) |
18856
4669dec681f4
tidy-up of res_clause.ML, removing the "predicates" field
paulson
parents:
18725
diff
changeset
|
297 |
val (ctvar_lits,ctfree_lits) = ResClause.add_typs_aux ctypes_sorts |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
298 |
in |
20016 | 299 |
if forall isFalse lits |
300 |
then error "Problem too trivial for resolution (empty clause)" |
|
301 |
else |
|
21509
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset
|
302 |
Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind, |
20016 | 303 |
literals = lits, ctypes_sorts = ctypes_sorts, |
304 |
ctvar_type_literals = ctvar_lits, |
|
305 |
ctfree_type_literals = ctfree_lits} |
|
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
306 |
end; |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
307 |
|
20016 | 308 |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
309 |
fun add_axiom_clause ((th,(name,id)), pairs) = |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
310 |
let val cls = make_clause(id, name, ResClause.Axiom, th) |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
311 |
in |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
312 |
if isTaut cls then pairs else (name,cls)::pairs |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
313 |
end; |
19354 | 314 |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
315 |
val make_axiom_clauses = foldl add_axiom_clause []; |
19354 | 316 |
|
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
317 |
fun make_conjecture_clauses_aux _ [] = [] |
20421 | 318 |
| make_conjecture_clauses_aux n (th::ths) = |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
319 |
make_clause(n,"conjecture", ResClause.Conjecture, th) :: |
20421 | 320 |
make_conjecture_clauses_aux (n+1) ths; |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
321 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
322 |
val make_conjecture_clauses = make_conjecture_clauses_aux 0; |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
323 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
324 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
325 |
(**********************************************************************) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
326 |
(* convert clause into ATP specific formats: *) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
327 |
(* TPTP used by Vampire and E *) |
19720 | 328 |
(* DFG used by SPASS *) |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
329 |
(**********************************************************************) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
330 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
331 |
val type_wrapper = "typeinfo"; |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
332 |
|
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
333 |
fun wrap_type (c,tp) = case !typ_level of |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
334 |
T_FULL => type_wrapper ^ ResClause.paren_pack [c, ResClause.string_of_fol_type tp] |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
335 |
| _ => c; |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
336 |
|
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
337 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
338 |
val bool_tp = ResClause.make_fixed_type_const "bool"; |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
339 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
340 |
val app_str = "hAPP"; |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
341 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
342 |
val bool_str = "hBOOL"; |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
343 |
|
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
344 |
fun type_of_combterm (CombConst(c,tp,_)) = tp |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
345 |
| type_of_combterm (CombFree(v,tp)) = tp |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
346 |
| type_of_combterm (CombVar(v,tp)) = tp |
21561 | 347 |
| type_of_combterm (CombApp(t1,t2,tp)) = tp; |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
348 |
|
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
349 |
fun string_of_combterm1 (CombConst(c,tp,_)) = |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
350 |
let val c' = if c = "equal" then "c_fequal" else c |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
351 |
in wrap_type (c',tp) end |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
352 |
| string_of_combterm1 (CombFree(v,tp)) = wrap_type (v,tp) |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
353 |
| string_of_combterm1 (CombVar(v,tp)) = wrap_type (v,tp) |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
354 |
| string_of_combterm1 (CombApp(t1,t2,tp)) = |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
355 |
let val s1 = string_of_combterm1 t1 |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
356 |
val s2 = string_of_combterm1 t2 |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
357 |
in |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
358 |
case !typ_level of |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
359 |
T_FULL => type_wrapper ^ |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
360 |
ResClause.paren_pack |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
361 |
[app_str ^ ResClause.paren_pack [s1,s2], |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
362 |
ResClause.string_of_fol_type tp] |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
363 |
| T_PARTIAL => app_str ^ ResClause.paren_pack |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
364 |
[s1,s2, ResClause.string_of_fol_type (type_of_combterm t1)] |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
365 |
| T_NONE => app_str ^ ResClause.paren_pack [s1,s2] |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
366 |
| T_CONST => raise ERROR "string_of_combterm1" |
21561 | 367 |
end; |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
368 |
|
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
369 |
fun string_of_combterm2 (CombConst(c,tp,tvars)) = |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
370 |
let val tvars' = map ResClause.string_of_fol_type tvars |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
371 |
val c' = if c = "equal" then "c_fequal" else c |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
372 |
in |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
373 |
c' ^ ResClause.paren_pack tvars' |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
374 |
end |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
375 |
| string_of_combterm2 (CombFree(v,tp)) = v |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
376 |
| string_of_combterm2 (CombVar(v,tp)) = v |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
377 |
| string_of_combterm2 (CombApp(t1,t2,_)) = |
21561 | 378 |
app_str ^ ResClause.paren_pack [string_of_combterm2 t1, string_of_combterm2 t2]; |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
379 |
|
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
380 |
fun string_of_combterm t = |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
381 |
case !typ_level of T_CONST => string_of_combterm2 t |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
382 |
| _ => string_of_combterm1 t; |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
383 |
|
21561 | 384 |
fun string_of_predicate (CombApp(CombApp(CombConst("equal",_,_),t1,_),t2,_)) = |
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
385 |
("equal" ^ ResClause.paren_pack [string_of_combterm t1, string_of_combterm t2]) |
21561 | 386 |
| string_of_predicate t = |
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
387 |
bool_str ^ ResClause.paren_pack [string_of_combterm t] |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
388 |
|
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
389 |
fun string_of_clausename (cls_id,ax_name) = |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
390 |
ResClause.clause_prefix ^ ResClause.ascii_of ax_name ^ "_" ^ Int.toString cls_id; |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
391 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
392 |
fun string_of_type_clsname (cls_id,ax_name,idx) = |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
393 |
string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx); |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
394 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
395 |
|
21561 | 396 |
(*** tptp format ***) |
19720 | 397 |
|
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
398 |
fun tptp_of_equality pol (t1,t2) = |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
399 |
let val eqop = if pol then " = " else " != " |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
400 |
in string_of_combterm t1 ^ eqop ^ string_of_combterm t2 end; |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
401 |
|
21561 | 402 |
fun tptp_literal (Literal(pol, CombApp(CombApp(CombConst("equal",_,_),t1,_),t2,_))) = |
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
403 |
tptp_of_equality pol (t1,t2) |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
404 |
| tptp_literal (Literal(pol,pred)) = |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
405 |
ResClause.tptp_sign pol (string_of_predicate pred); |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
406 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
407 |
fun tptp_type_lits (Clause cls) = |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
408 |
let val lits = map tptp_literal (#literals cls) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
409 |
val ctvar_lits_strs = |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
410 |
case !typ_level of T_NONE => [] |
20360 | 411 |
| _ => map ResClause.tptp_of_typeLit (#ctvar_type_literals cls) |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
412 |
val ctfree_lits = |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
413 |
case !typ_level of T_NONE => [] |
20360 | 414 |
| _ => map ResClause.tptp_of_typeLit (#ctfree_type_literals cls) |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
415 |
in |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
416 |
(ctvar_lits_strs @ lits, ctfree_lits) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
417 |
end; |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
418 |
|
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
419 |
|
21509
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset
|
420 |
fun clause2tptp (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) = |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
421 |
let val (lits,ctfree_lits) = tptp_type_lits cls |
21509
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset
|
422 |
val cls_str = ResClause.gen_tptp_cls(clause_id,axiom_name,kind,lits) |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
423 |
in |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
424 |
(cls_str,ctfree_lits) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
425 |
end; |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
426 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
427 |
|
21561 | 428 |
(*** dfg format ***) |
429 |
||
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
430 |
fun dfg_literal (Literal(pol,pred)) = ResClause.dfg_sign pol (string_of_predicate pred); |
19720 | 431 |
|
432 |
fun dfg_clause_aux (Clause{literals, ctypes_sorts, ...}) = |
|
433 |
let val lits = map dfg_literal literals |
|
434 |
val (tvar_lits,tfree_lits) = ResClause.add_typs_aux ctypes_sorts |
|
435 |
val tvar_lits_strs = |
|
436 |
case !typ_level of T_NONE => [] |
|
20360 | 437 |
| _ => map ResClause.dfg_of_typeLit tvar_lits |
19720 | 438 |
val tfree_lits = |
439 |
case !typ_level of T_NONE => [] |
|
20360 | 440 |
| _ => map ResClause.dfg_of_typeLit tfree_lits |
19720 | 441 |
in |
442 |
(tvar_lits_strs @ lits, tfree_lits) |
|
443 |
end; |
|
444 |
||
445 |
fun get_uvars (CombConst(_,_,_)) vars = vars |
|
446 |
| get_uvars (CombFree(_,_)) vars = vars |
|
447 |
| get_uvars (CombVar(v,tp)) vars = (v::vars) |
|
21561 | 448 |
| get_uvars (CombApp(P,Q,tp)) vars = get_uvars P (get_uvars Q vars); |
19720 | 449 |
|
450 |
fun get_uvars_l (Literal(_,c)) = get_uvars c []; |
|
451 |
||
452 |
fun dfg_vars (Clause {literals,...}) = ResClause.union_all (map get_uvars_l literals); |
|
453 |
||
454 |
fun clause2dfg (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) = |
|
455 |
let val (lits,tfree_lits) = dfg_clause_aux cls |
|
456 |
val vars = dfg_vars cls |
|
457 |
val tvars = ResClause.get_tvar_strs ctypes_sorts |
|
21509
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset
|
458 |
val knd = ResClause.name_of_kind kind |
19720 | 459 |
val lits_str = commas lits |
460 |
val cls_str = ResClause.gen_dfg_cls(clause_id, axiom_name, knd, lits_str, tvars@vars) |
|
461 |
in (cls_str, tfree_lits) end; |
|
462 |
||
463 |
||
464 |
fun init_funcs_tab funcs = |
|
21561 | 465 |
let val funcs1 = case !typ_level of T_PARTIAL => Symtab.update ("hAPP",3) funcs |
20865
2cfa020109c1
Changed and removed some functions related to combinators, since they are Isabelle constants now.
mengj
parents:
20864
diff
changeset
|
466 |
| _ => Symtab.update ("hAPP",2) funcs |
19724 | 467 |
in |
21561 | 468 |
Symtab.update ("typeinfo",2) funcs1 |
19724 | 469 |
end; |
19720 | 470 |
|
471 |
||
19725
ada9bb1faba5
Changed the DFG format's functions' declaration procedure.
mengj
parents:
19724
diff
changeset
|
472 |
fun add_funcs (CombConst(c,_,tvars),funcs) = |
21561 | 473 |
if c = "equal" then foldl ResClause.add_foltype_funcs funcs tvars |
474 |
else |
|
475 |
(case !typ_level of |
|
476 |
T_CONST => foldl ResClause.add_foltype_funcs (Symtab.update(c,length tvars) funcs) tvars |
|
477 |
| _ => foldl ResClause.add_foltype_funcs (Symtab.update(c,0) funcs) tvars) |
|
19724 | 478 |
| add_funcs (CombFree(v,ctp),funcs) = ResClause.add_foltype_funcs (ctp,Symtab.update (v,0) funcs) |
19720 | 479 |
| add_funcs (CombVar(_,ctp),funcs) = ResClause.add_foltype_funcs (ctp,funcs) |
21561 | 480 |
| add_funcs (CombApp(P,Q,_),funcs) = add_funcs(P,add_funcs (Q,funcs)); |
19720 | 481 |
|
482 |
fun add_literal_funcs (Literal(_,c), funcs) = add_funcs (c,funcs); |
|
483 |
||
484 |
fun add_clause_funcs (Clause {literals, ...}, funcs) = |
|
485 |
foldl add_literal_funcs funcs literals |
|
486 |
handle Symtab.DUP a => raise ERROR ("function " ^ a ^ " has multiple arities") |
|
487 |
||
488 |
fun funcs_of_clauses clauses arity_clauses = |
|
489 |
Symtab.dest (foldl ResClause.add_arityClause_funcs |
|
490 |
(foldl add_clause_funcs (init_funcs_tab Symtab.empty) clauses) |
|
491 |
arity_clauses) |
|
492 |
||
21398
11996e938dfe
Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents:
21254
diff
changeset
|
493 |
fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) = |
11996e938dfe
Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents:
21254
diff
changeset
|
494 |
foldl ResClause.add_type_sort_preds preds ctypes_sorts |
11996e938dfe
Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents:
21254
diff
changeset
|
495 |
handle Symtab.DUP a => raise ERROR ("predicate " ^ a ^ " has multiple arities") |
11996e938dfe
Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents:
21254
diff
changeset
|
496 |
|
11996e938dfe
Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents:
21254
diff
changeset
|
497 |
(*Higher-order clauses have only the predicates hBOOL and type classes.*) |
11996e938dfe
Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents:
21254
diff
changeset
|
498 |
fun preds_of_clauses clauses clsrel_clauses arity_clauses = |
19720 | 499 |
Symtab.dest |
500 |
(foldl ResClause.add_classrelClause_preds |
|
501 |
(foldl ResClause.add_arityClause_preds |
|
21398
11996e938dfe
Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents:
21254
diff
changeset
|
502 |
(Symtab.update ("hBOOL",1) |
11996e938dfe
Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents:
21254
diff
changeset
|
503 |
(foldl add_clause_preds Symtab.empty clauses)) |
19720 | 504 |
arity_clauses) |
505 |
clsrel_clauses) |
|
506 |
||
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
507 |
|
21398
11996e938dfe
Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents:
21254
diff
changeset
|
508 |
|
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
509 |
(**********************************************************************) |
19198
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
510 |
(* write clauses to files *) |
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
511 |
(**********************************************************************) |
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
512 |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
513 |
|
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
514 |
val init_counters = |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
515 |
Symtab.make [("c_COMBI", 0), ("c_COMBK", 0), |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
516 |
("c_COMBB", 0), ("c_COMBC", 0), |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
517 |
("c_COMBS", 0), ("c_COMBB_e", 0), |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
518 |
("c_COMBC_e", 0), ("c_COMBS_e", 0)]; |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
519 |
|
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
520 |
fun count_combterm (CombConst(c,tp,_), ct) = |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
521 |
(case Symtab.lookup ct c of NONE => ct (*no counter*) |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
522 |
| SOME n => Symtab.update (c,n+1) ct) |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
523 |
| count_combterm (CombFree(v,tp), ct) = ct |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
524 |
| count_combterm (CombVar(v,tp), ct) = ct |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
525 |
| count_combterm (CombApp(t1,t2,tp), ct) = count_combterm(t1, count_combterm(t2, ct)); |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
526 |
|
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
527 |
fun count_literal (Literal(_,t), ct) = count_combterm(t,ct); |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
528 |
|
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
529 |
fun count_clause (Clause{literals,...}, ct) = foldl count_literal ct literals; |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
530 |
|
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
531 |
fun count_user_clause user_lemmas (Clause{axiom_name,literals,...}, ct) = |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
532 |
if axiom_name mem_string user_lemmas then foldl count_literal ct literals |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
533 |
else ct; |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
534 |
|
20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
535 |
val cnf_helper_thms = ResAxioms.cnf_rules_pairs o (map ResAxioms.pairname) |
20644 | 536 |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
537 |
fun get_helper_clauses ct = |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
538 |
let fun needed c = valOf (Symtab.lookup ct c) > 0 |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
539 |
val IK = if needed "c_COMBI" orelse needed "c_COMBK" |
21135 | 540 |
then (Output.debug "Include combinator I K"; cnf_helper_thms [comb_I,comb_K]) |
541 |
else [] |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
542 |
val BC = if needed "c_COMBB" orelse needed "c_COMBC" |
21135 | 543 |
then (Output.debug "Include combinator B C"; cnf_helper_thms [comb_B,comb_C]) |
544 |
else [] |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
545 |
val S = if needed "c_COMBS" |
21135 | 546 |
then (Output.debug "Include combinator S"; cnf_helper_thms [comb_S]) |
547 |
else [] |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
548 |
val B'C' = if needed "c_COMBB_e" orelse needed "c_COMBC_e" |
21135 | 549 |
then (Output.debug "Include combinator B' C'"; cnf_helper_thms [comb_B', comb_C']) |
550 |
else [] |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
551 |
val S' = if needed "c_COMBS_e" |
21135 | 552 |
then (Output.debug "Include combinator S'"; cnf_helper_thms [comb_S']) |
553 |
else [] |
|
20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
554 |
val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal] |
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
555 |
in |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
556 |
make_axiom_clauses (other @ IK @ BC @ S @ B'C' @ S') |
20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
557 |
end |
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
558 |
|
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
559 |
(* tptp format *) |
19491
cd6c71c57f53
changed the functions for getting HOL helper clauses.
mengj
parents:
19452
diff
changeset
|
560 |
|
19198
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
561 |
(* write TPTP format to a single file *) |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
562 |
fun tptp_write_file thms filename (axclauses,classrel_clauses,arity_clauses) user_lemmas = |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
563 |
let val conjectures = make_conjecture_clauses thms |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
564 |
val (clnames,axclauses') = ListPair.unzip (make_axiom_clauses axclauses) |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
565 |
val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp conjectures) |
19198
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
566 |
val tfree_clss = map ResClause.tptp_tfree_clause (foldl (op union_string) [] tfree_litss) |
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
567 |
val out = TextIO.openOut filename |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
568 |
val ct = foldl (count_user_clause user_lemmas) |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
569 |
(foldl count_clause init_counters conjectures) |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
570 |
axclauses' |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
571 |
val helper_clauses = map #2 (get_helper_clauses ct) |
19198
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
572 |
in |
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
573 |
List.app (curry TextIO.output out o #1 o clause2tptp) axclauses'; |
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
574 |
ResClause.writeln_strs out tfree_clss; |
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
575 |
ResClause.writeln_strs out tptp_clss; |
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
576 |
List.app (curry TextIO.output out o ResClause.tptp_classrelClause) classrel_clauses; |
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
577 |
List.app (curry TextIO.output out o ResClause.tptp_arity_clause) arity_clauses; |
20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
578 |
List.app (curry TextIO.output out o #1 o clause2tptp) helper_clauses; |
20022 | 579 |
TextIO.closeOut out; |
580 |
clnames |
|
19198
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
581 |
end; |
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
582 |
|
19720 | 583 |
|
20644 | 584 |
|
19720 | 585 |
(* dfg format *) |
586 |
||
20130
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
587 |
fun dfg_write_file thms filename (axclauses,classrel_clauses,arity_clauses) user_lemmas = |
19720 | 588 |
let val _ = Output.debug ("Preparing to write the DFG file " ^ filename) |
589 |
val conjectures = make_conjecture_clauses thms |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
590 |
val (clnames,axclauses') = ListPair.unzip (make_axiom_clauses axclauses) |
19720 | 591 |
val (dfg_clss,tfree_litss) = ListPair.unzip (map clause2dfg conjectures) |
592 |
and probname = Path.pack (Path.base (Path.unpack filename)) |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
593 |
val axstrs = map (#1 o clause2dfg) axclauses' |
19720 | 594 |
val tfree_clss = map ResClause.dfg_tfree_clause (ResClause.union_all tfree_litss) |
595 |
val out = TextIO.openOut filename |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
596 |
val ct = foldl (count_user_clause user_lemmas) |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
597 |
(foldl count_clause init_counters conjectures) |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
598 |
axclauses' |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
599 |
val helper_clauses = map #2 (get_helper_clauses ct) |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
600 |
val helper_clauses_strs = map (#1 o clause2dfg) helper_clauses |
20864
bb75b876b260
Now the DFG output includes correct declarations of c_fequal, but not hEXTENT
paulson
parents:
20791
diff
changeset
|
601 |
val funcs = funcs_of_clauses (helper_clauses @ conjectures @ axclauses') arity_clauses |
21398
11996e938dfe
Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents:
21254
diff
changeset
|
602 |
and preds = preds_of_clauses axclauses' classrel_clauses arity_clauses |
19720 | 603 |
in |
604 |
TextIO.output (out, ResClause.string_of_start probname); |
|
605 |
TextIO.output (out, ResClause.string_of_descrip probname); |
|
606 |
TextIO.output (out, ResClause.string_of_symbols (ResClause.string_of_funcs funcs) (ResClause.string_of_preds preds)); |
|
607 |
TextIO.output (out, "list_of_clauses(axioms,cnf).\n"); |
|
608 |
ResClause.writeln_strs out axstrs; |
|
609 |
List.app (curry TextIO.output out o ResClause.dfg_classrelClause) classrel_clauses; |
|
610 |
List.app (curry TextIO.output out o ResClause.dfg_arity_clause) arity_clauses; |
|
20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
611 |
ResClause.writeln_strs out helper_clauses_strs; |
19720 | 612 |
TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"); |
613 |
ResClause.writeln_strs out tfree_clss; |
|
614 |
ResClause.writeln_strs out dfg_clss; |
|
20953
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
615 |
TextIO.output (out, "end_of_list.\n\n"); |
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
616 |
(*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*) |
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
617 |
TextIO.output (out, "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n"); |
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
618 |
TextIO.output (out, "end_problem.\n"); |
20022 | 619 |
TextIO.closeOut out; |
620 |
clnames |
|
19720 | 621 |
end; |
622 |
||
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset
|
623 |
end |