author | paulson |
Mon, 07 May 2007 16:46:42 +0200 | |
changeset 22851 | 7b7d6e1c70b6 |
parent 22825 | bd774e01d6d5 |
child 23386 | 9255c1a75ba9 |
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 |
|
22825
bd774e01d6d5
Fixing bugs in the partial-typed and fully-typed translations
paulson
parents:
22130
diff
changeset
|
4 |
FOL clauses translated from HOL formulae. |
bd774e01d6d5
Fixing bugs in the partial-typed and fully-typed translations
paulson
parents:
22130
diff
changeset
|
5 |
|
bd774e01d6d5
Fixing bugs in the partial-typed and fully-typed translations
paulson
parents:
22130
diff
changeset
|
6 |
The combinator code needs to be deleted after the translation paper has been published. |
bd774e01d6d5
Fixing bugs in the partial-typed and fully-typed translations
paulson
parents:
22130
diff
changeset
|
7 |
It cannot be used with proof reconstruction because combinators are not introduced by proof. |
bd774e01d6d5
Fixing bugs in the partial-typed and fully-typed translations
paulson
parents:
22130
diff
changeset
|
8 |
The Turner combinators (B', C', S') yield no improvement and should be deleted. |
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
|
9 |
*) |
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 |
|
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
|
11 |
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
|
12 |
|
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
|
13 |
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
|
14 |
|
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
15 |
structure RC = ResClause; |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
16 |
|
20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
17 |
(* 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
|
18 |
val ext = thm "HOL.ext"; |
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset
|
19 |
val comb_I = thm "ATP_Linkup.COMBI_def"; |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset
|
20 |
val comb_K = thm "ATP_Linkup.COMBK_def"; |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset
|
21 |
val comb_B = thm "ATP_Linkup.COMBB_def"; |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset
|
22 |
val comb_C = thm "ATP_Linkup.COMBC_def"; |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset
|
23 |
val comb_S = thm "ATP_Linkup.COMBS_def"; |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset
|
24 |
val comb_B' = thm "ATP_Linkup.COMBB'_def"; |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset
|
25 |
val comb_C' = thm "ATP_Linkup.COMBC'_def"; |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset
|
26 |
val comb_S' = thm "ATP_Linkup.COMBS'_def"; |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset
|
27 |
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
|
28 |
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
|
29 |
|
22825
bd774e01d6d5
Fixing bugs in the partial-typed and fully-typed translations
paulson
parents:
22130
diff
changeset
|
30 |
|
bd774e01d6d5
Fixing bugs in the partial-typed and fully-typed translations
paulson
parents:
22130
diff
changeset
|
31 |
(*The different translations of types*) |
bd774e01d6d5
Fixing bugs in the partial-typed and fully-typed translations
paulson
parents:
22130
diff
changeset
|
32 |
datatype type_level = T_FULL | T_PARTIAL | T_CONST; |
bd774e01d6d5
Fixing bugs in the partial-typed and fully-typed translations
paulson
parents:
22130
diff
changeset
|
33 |
|
bd774e01d6d5
Fixing bugs in the partial-typed and fully-typed translations
paulson
parents:
22130
diff
changeset
|
34 |
val typ_level = ref T_CONST; |
bd774e01d6d5
Fixing bugs in the partial-typed and fully-typed translations
paulson
parents:
22130
diff
changeset
|
35 |
|
bd774e01d6d5
Fixing bugs in the partial-typed and fully-typed translations
paulson
parents:
22130
diff
changeset
|
36 |
fun full_types () = (typ_level:=T_FULL); |
bd774e01d6d5
Fixing bugs in the partial-typed and fully-typed translations
paulson
parents:
22130
diff
changeset
|
37 |
fun partial_types () = (typ_level:=T_PARTIAL); |
bd774e01d6d5
Fixing bugs in the partial-typed and fully-typed translations
paulson
parents:
22130
diff
changeset
|
38 |
fun const_types_only () = (typ_level:=T_CONST); |
bd774e01d6d5
Fixing bugs in the partial-typed and fully-typed translations
paulson
parents:
22130
diff
changeset
|
39 |
|
21108 | 40 |
(*A flag to set if we use the Turner optimizations. Currently FALSE, as the 5 standard |
20997 | 41 |
combinators appear to work best.*) |
21108 | 42 |
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
|
43 |
|
22064 | 44 |
(*If true, each function will be directly applied to as many arguments as possible, avoiding |
22825
bd774e01d6d5
Fixing bugs in the partial-typed and fully-typed translations
paulson
parents:
22130
diff
changeset
|
45 |
use of the "apply" operator. Use of hBOOL is also minimized. It only works for the |
bd774e01d6d5
Fixing bugs in the partial-typed and fully-typed translations
paulson
parents:
22130
diff
changeset
|
46 |
constant-typed translation, though it could be tried for the partially-typed one.*) |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
47 |
val minimize_applies = ref true; |
22064 | 48 |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
49 |
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
|
50 |
|
22064 | 51 |
val const_min_arity = ref (Symtab.empty : int Symtab.table); |
52 |
||
53 |
val const_needs_hBOOL = ref (Symtab.empty : bool Symtab.table); |
|
54 |
||
55 |
fun min_arity_of c = getOpt (Symtab.lookup(!const_min_arity) c, 0); |
|
56 |
||
22825
bd774e01d6d5
Fixing bugs in the partial-typed and fully-typed translations
paulson
parents:
22130
diff
changeset
|
57 |
(*True if the constant ever appears outside of the top-level position in literals. |
bd774e01d6d5
Fixing bugs in the partial-typed and fully-typed translations
paulson
parents:
22130
diff
changeset
|
58 |
If false, the constant always receives all of its arguments and is used as a predicate.*) |
22851
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
59 |
fun needs_hBOOL c = not (!minimize_applies) orelse !typ_level=T_PARTIAL orelse |
22064 | 60 |
getOpt (Symtab.lookup(!const_needs_hBOOL) c, false); |
61 |
||
62 |
fun init thy = |
|
63 |
(const_typargs := Sign.const_typargs thy; |
|
64 |
const_min_arity := Symtab.empty; |
|
65 |
const_needs_hBOOL := Symtab.empty); |
|
19198
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
66 |
|
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
|
67 |
(**********************************************************************) |
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
|
68 |
(* 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
|
69 |
(**********************************************************************) |
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
|
70 |
|
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
|
71 |
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
|
72 |
| 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
|
73 |
| 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
|
74 |
| 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
|
75 |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
76 |
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
|
77 |
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
|
78 |
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
|
79 |
val tp_r = Term.type_of1(bnds,r) |
22064 | 80 |
val typ_B' = [tp_p,tp_q,tp_r] ---> Term.type_of1(bnds,tm) |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
81 |
in |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
82 |
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
|
83 |
end |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
84 |
| 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
|
85 |
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
|
86 |
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
|
87 |
val tp_r = Term.type_of1(bnds,r) |
22064 | 88 |
val typ_C' = [tp_p,tp_q,tp_r] ---> Term.type_of1(bnds,tm) |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
89 |
in |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
90 |
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
|
91 |
end |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
92 |
| 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
|
93 |
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
|
94 |
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
|
95 |
val tp_r = Term.type_of1(bnds,r) |
22064 | 96 |
val typ_S' = [tp_p,tp_q,tp_r] ---> Term.type_of1(bnds,tm) |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
97 |
in |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
98 |
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
|
99 |
end |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
100 |
| mk_compact_comb tm _ = tm; |
20644 | 101 |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
102 |
fun compact_comb t bnds = |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
103 |
if !use_Turner then mk_compact_comb t bnds else t; |
20644 | 104 |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
105 |
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
|
106 |
| 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
|
107 |
let val tb = List.nth(bnds,n-1) |
22064 | 108 |
in Const("ATP_Linkup.COMBK", [tb,tp] ---> tb) $ Bound (n-1) end |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
109 |
| 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
|
110 |
| 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
|
111 |
| 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
|
112 |
| 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
|
113 |
if is_free P 0 then |
21135 | 114 |
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
|
115 |
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
|
116 |
val tp' = Term.type_of1(bnds,P') |
22064 | 117 |
val tS = [tp',tI] ---> Term.type_of1(t1::bnds,P) |
21108 | 118 |
in |
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset
|
119 |
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
|
120 |
Const("ATP_Linkup.COMBI",tI)) bnds |
21108 | 121 |
end |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
122 |
else incr_boundvars ~1 P |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
123 |
| lam2comb (t as (Abs(x,t1,P$Q))) bnds = |
21108 | 124 |
let val nfreeP = not(is_free P 0) |
125 |
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
|
126 |
val tpq = Term.type_of1(t1::bnds, P$Q) |
21108 | 127 |
in |
128 |
if nfreeP andalso nfreeQ |
|
129 |
then |
|
21135 | 130 |
let val tK = [tpq,t1] ---> tpq |
22064 | 131 |
in Const("ATP_Linkup.COMBK",tK) $ incr_boundvars ~1 (P $ Q) end |
21108 | 132 |
else if nfreeP then |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
133 |
let val Q' = lam2comb (Abs(x,t1,Q)) bnds |
21135 | 134 |
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
|
135 |
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
|
136 |
val tq' = Term.type_of1(bnds, Q') |
21135 | 137 |
val tB = [tp,tq',t1] ---> tpq |
22064 | 138 |
in compact_comb (Const("ATP_Linkup.COMBB",tB) $ P' $ Q') bnds end |
21108 | 139 |
else if nfreeQ then |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
140 |
let val P' = lam2comb (Abs(x,t1,P)) bnds |
21135 | 141 |
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
|
142 |
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
|
143 |
val tp' = Term.type_of1(bnds, P') |
21135 | 144 |
val tC = [tp',tq,t1] ---> tpq |
22064 | 145 |
in compact_comb (Const("ATP_Linkup.COMBC",tC) $ P' $ Q') bnds end |
21108 | 146 |
else |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
147 |
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
|
148 |
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
|
149 |
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
|
150 |
val tq' = Term.type_of1(bnds,Q') |
21135 | 151 |
val tS = [tp',tq',t1] ---> tpq |
22064 | 152 |
in compact_comb (Const("ATP_Linkup.COMBS",tS) $ P' $ Q') bnds end |
21108 | 153 |
end |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
154 |
| lam2comb (t as (Abs(x,t1,_))) _ = raise RC.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
|
155 |
|
22064 | 156 |
fun to_comb (Abs(x,tp,b)) bnds = lam2comb (Abs(x, tp, to_comb b (tp::bnds))) bnds |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
157 |
| 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
|
158 |
| to_comb t _ = 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
|
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 |
|
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
|
161 |
(******************************************************) |
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
|
162 |
(* 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
|
163 |
(******************************************************) |
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
|
164 |
|
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
|
165 |
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
|
166 |
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
|
167 |
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
|
168 |
|
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
169 |
datatype combterm = CombConst of string * RC.fol_type * RC.fol_type list |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
170 |
| CombFree of string * RC.fol_type |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
171 |
| CombVar of string * RC.fol_type |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
172 |
| CombApp of combterm * combterm |
20360 | 173 |
|
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
|
174 |
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
|
175 |
|
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
|
176 |
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
|
177 |
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
|
178 |
axiom_name: axiom_name, |
19964 | 179 |
th: thm, |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
180 |
kind: RC.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
|
181 |
literals: literal list, |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
182 |
ctypes_sorts: (RC.typ_var * Term.sort) list, |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
183 |
ctvar_type_literals: RC.type_literal list, |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
184 |
ctfree_type_literals: RC.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
|
185 |
|
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
|
186 |
|
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
|
187 |
(*********************************************************************) |
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 |
(* 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
|
189 |
(*********************************************************************) |
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
|
190 |
|
21561 | 191 |
fun isFalse (Literal(pol, CombConst(c,_,_))) = |
20360 | 192 |
(pol andalso c = "c_False") orelse |
193 |
(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
|
194 |
| 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
|
195 |
|
21561 | 196 |
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
|
197 |
(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
|
198 |
(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
|
199 |
| 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
|
200 |
|
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 |
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
|
202 |
|
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
203 |
fun type_of (Type (a, Ts)) = |
21561 | 204 |
let val (folTypes,ts) = types_of Ts |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
205 |
in (RC.Comp(RC.make_fixed_type_const a, folTypes), ts) 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
|
206 |
| type_of (tp as (TFree(a,s))) = |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
207 |
(RC.AtomF (RC.make_fixed_type_var a), [RC.mk_typ_var_sort tp]) |
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
208 |
| type_of (tp as (TVar(v,s))) = |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
209 |
(RC.AtomV (RC.make_schematic_type_var v), [RC.mk_typ_var_sort tp]) |
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 |
and types_of Ts = |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
211 |
let val (folTyps,ts) = ListPair.unzip (map type_of Ts) |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
212 |
in (folTyps, RC.union_all ts) 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
|
213 |
|
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
|
214 |
(* 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
|
215 |
fun simp_type_of (Type (a, Ts)) = |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
216 |
RC.Comp(RC.make_fixed_type_const a, map simp_type_of Ts) |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
217 |
| simp_type_of (TFree (a,s)) = RC.AtomF(RC.make_fixed_type_var a) |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
218 |
| simp_type_of (TVar (v,s)) = RC.AtomV(RC.make_schematic_type_var v); |
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
219 |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
220 |
|
20865
2cfa020109c1
Changed and removed some functions related to combinators, since they are Isabelle constants now.
mengj
parents:
20864
diff
changeset
|
221 |
fun const_type_of (c,t) = |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
222 |
let val (tp,ts) = type_of t |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
223 |
in (tp, ts, map simp_type_of (!const_typargs(c,t))) end; |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
224 |
|
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
|
225 |
(* 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
|
226 |
fun combterm_of (Const(c,t)) = |
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
227 |
let val (tp,ts,tvar_list) = const_type_of (c,t) |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
228 |
val c' = CombConst(RC.make_fixed_const c, tp, tvar_list) |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
229 |
in (c',ts) 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
|
230 |
| combterm_of (Free(v,t)) = |
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
231 |
let val (tp,ts) = type_of t |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
232 |
val v' = if RC.isMeta v then CombVar(RC.make_schematic_var(v,0),tp) |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
233 |
else CombFree(RC.make_fixed_var v,tp) |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
234 |
in (v',ts) 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
|
235 |
| combterm_of (Var(v,t)) = |
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
236 |
let val (tp,ts) = type_of t |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
237 |
val v' = CombVar(RC.make_schematic_var v,tp) |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
238 |
in (v',ts) 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
|
239 |
| combterm_of (t as (P $ Q)) = |
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
240 |
let val (P',tsP) = combterm_of P |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
241 |
val (Q',tsQ) = combterm_of Q |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
242 |
in (CombApp(P',Q'), tsP union tsQ) 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
|
243 |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
244 |
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
|
245 |
| 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
|
246 |
|
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
|
247 |
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
|
248 |
| 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
|
249 |
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
|
250 |
| literals_of_term1 (lits,ts) P = |
21509
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset
|
251 |
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
|
252 |
in |
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset
|
253 |
(Literal(pol,pred)::lits, ts union ts') |
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset
|
254 |
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
|
255 |
|
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
|
256 |
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
|
257 |
|
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 |
(* 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
|
259 |
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
|
260 |
let val (lits,ctypes_sorts) = literals_of_term (to_comb (prop_of th) []) |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
261 |
val (ctvar_lits,ctfree_lits) = RC.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
|
262 |
in |
20016 | 263 |
if forall isFalse lits |
264 |
then error "Problem too trivial for resolution (empty clause)" |
|
265 |
else |
|
21509
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset
|
266 |
Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind, |
20016 | 267 |
literals = lits, ctypes_sorts = ctypes_sorts, |
268 |
ctvar_type_literals = ctvar_lits, |
|
269 |
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
|
270 |
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
|
271 |
|
20016 | 272 |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
273 |
fun add_axiom_clause ((th,(name,id)), pairs) = |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
274 |
let val cls = make_clause(id, name, RC.Axiom, th) |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
275 |
in |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
276 |
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
|
277 |
end; |
19354 | 278 |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
279 |
val make_axiom_clauses = foldl add_axiom_clause []; |
19354 | 280 |
|
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
|
281 |
fun make_conjecture_clauses_aux _ [] = [] |
20421 | 282 |
| make_conjecture_clauses_aux n (th::ths) = |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
283 |
make_clause(n,"conjecture", RC.Conjecture, th) :: |
20421 | 284 |
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
|
285 |
|
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 |
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
|
287 |
|
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
|
288 |
|
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
|
289 |
(**********************************************************************) |
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
|
290 |
(* 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
|
291 |
(* TPTP used by Vampire and E *) |
19720 | 292 |
(* 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
|
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 |
|
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
295 |
(*Result of a function type; no need to check that the argument type matches.*) |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
296 |
fun result_type (RC.Comp ("tc_fun", [_, tp2])) = tp2 |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
297 |
| result_type _ = raise ERROR "result_type" |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
298 |
|
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
299 |
fun type_of_combterm (CombConst(c,tp,_)) = tp |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
300 |
| type_of_combterm (CombFree(v,tp)) = tp |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
301 |
| type_of_combterm (CombVar(v,tp)) = tp |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
302 |
| type_of_combterm (CombApp(t1,t2)) = result_type (type_of_combterm t1); |
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
|
303 |
|
22064 | 304 |
(*gets the head of a combinator application, along with the list of arguments*) |
305 |
fun strip_comb u = |
|
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
306 |
let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts) |
22064 | 307 |
| stripc x = x |
308 |
in stripc(u,[]) end; |
|
309 |
||
22851
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
310 |
val type_wrapper = "ti"; |
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
311 |
|
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
312 |
fun head_needs_hBOOL (CombConst(c,_,_)) = needs_hBOOL c |
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
313 |
| head_needs_hBOOL _ = true; |
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
314 |
|
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
315 |
fun wrap_type (s, tp) = |
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
316 |
if !typ_level=T_FULL then |
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
317 |
type_wrapper ^ RC.paren_pack [s, RC.string_of_fol_type tp] |
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
318 |
else s; |
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
319 |
|
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
320 |
fun apply ss = "hAPP" ^ RC.paren_pack ss; |
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
321 |
|
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
322 |
(*Full (non-optimized) and partial-typed transations*) |
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
323 |
fun string_of_combterm1 (CombConst(c,tp,_)) = |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
324 |
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
|
325 |
in wrap_type (c',tp) end |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
326 |
| 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
|
327 |
| string_of_combterm1 (CombVar(v,tp)) = wrap_type (v,tp) |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
328 |
| string_of_combterm1 (CombApp(t1,t2)) = |
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
329 |
let val s1 = string_of_combterm1 t1 |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
330 |
and s2 = string_of_combterm1 t2 |
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
331 |
in |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
332 |
case !typ_level of |
22851
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
333 |
T_FULL => wrap_type (apply [s1,s2], result_type (type_of_combterm t1)) |
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
334 |
| T_PARTIAL => apply [s1,s2, RC.string_of_fol_type (type_of_combterm t1)] |
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
335 |
| T_CONST => raise ERROR "string_of_combterm1" |
21561 | 336 |
end; |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
337 |
|
22064 | 338 |
fun rev_apply (v, []) = v |
22851
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
339 |
| rev_apply (v, arg::args) = apply [rev_apply (v, args), arg]; |
22064 | 340 |
|
341 |
fun string_apply (v, args) = rev_apply (v, rev args); |
|
342 |
||
343 |
(*Apply an operator to the argument strings, using either the "apply" operator or |
|
344 |
direct function application.*) |
|
22851
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
345 |
fun string_of_applic (CombConst(c,tp,tvars), args) = |
22064 | 346 |
let val c = if c = "equal" then "c_fequal" else c |
347 |
val nargs = min_arity_of c |
|
22851
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
348 |
val args1 = List.take(args, nargs) |
22064 | 349 |
handle Subscript => raise ERROR ("string_of_applic: " ^ c ^ " has arity " ^ |
350 |
Int.toString nargs ^ " but is applied to " ^ |
|
351 |
space_implode ", " args) |
|
352 |
val args2 = List.drop(args, nargs) |
|
22851
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
353 |
val targs = if !typ_level = T_CONST then map RC.string_of_fol_type tvars |
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
354 |
else [] |
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
355 |
in |
22851
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
356 |
string_apply (c ^ RC.paren_pack (args1@targs), args2) |
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
357 |
end |
22851
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
358 |
| string_of_applic (CombFree(v,tp), args) = string_apply (v, args) |
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
359 |
| string_of_applic (CombVar(v,tp), args) = string_apply (v, args) |
22064 | 360 |
| string_of_applic _ = raise ERROR "string_of_applic"; |
361 |
||
22851
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
362 |
fun wrap_type_if (head, s, tp) = if head_needs_hBOOL head then wrap_type (s, tp) else s; |
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
363 |
|
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
364 |
(*Full (if optimized) and constant-typed transations*) |
22064 | 365 |
fun string_of_combterm2 t = |
366 |
let val (head, args) = strip_comb t |
|
22851
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
367 |
in wrap_type_if (head, |
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
368 |
string_of_applic (head, map string_of_combterm2 args), |
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
369 |
type_of_combterm t) |
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
370 |
end; |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
371 |
|
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
372 |
fun string_of_combterm t = |
22851
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
373 |
case (!typ_level,!minimize_applies) of |
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
374 |
(T_PARTIAL, _) => string_of_combterm1 t |
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
375 |
| (T_FULL, false) => string_of_combterm1 t |
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
376 |
| _ => string_of_combterm2 t; |
22064 | 377 |
|
378 |
(*Boolean-valued terms are here converted to literals.*) |
|
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
379 |
fun boolify t = "hBOOL" ^ RC.paren_pack [string_of_combterm t]; |
22064 | 380 |
|
381 |
fun string_of_predicate t = |
|
382 |
case t of |
|
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
383 |
(CombApp(CombApp(CombConst("equal",_,_), t1), t2)) => |
22064 | 384 |
(*DFG only: new TPTP prefers infix equality*) |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
385 |
("equal" ^ RC.paren_pack [string_of_combterm t1, string_of_combterm t2]) |
22064 | 386 |
| _ => |
387 |
case #1 (strip_comb t) of |
|
388 |
CombConst(c,_,_) => if needs_hBOOL c then boolify t else string_of_combterm t |
|
389 |
| _ => boolify t; |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
390 |
|
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
|
391 |
fun string_of_clausename (cls_id,ax_name) = |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
392 |
RC.clause_prefix ^ RC.ascii_of ax_name ^ "_" ^ Int.toString cls_id; |
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
|
393 |
|
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 |
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
|
395 |
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
|
396 |
|
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
|
397 |
|
21561 | 398 |
(*** tptp format ***) |
19720 | 399 |
|
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
400 |
fun tptp_of_equality pol (t1,t2) = |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
401 |
let val eqop = if pol then " = " else " != " |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
402 |
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
|
403 |
|
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
404 |
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
|
405 |
tptp_of_equality pol (t1,t2) |
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents:
21509
diff
changeset
|
406 |
| tptp_literal (Literal(pol,pred)) = |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
407 |
RC.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
|
408 |
|
22064 | 409 |
(*Given a clause, returns its literals paired with a list of literals concerning TFrees; |
410 |
the latter should only occur in conjecture clauses.*) |
|
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
|
411 |
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
|
412 |
let val lits = map tptp_literal (#literals cls) |
22825
bd774e01d6d5
Fixing bugs in the partial-typed and fully-typed translations
paulson
parents:
22130
diff
changeset
|
413 |
val ctvar_lits_strs = map RC.tptp_of_typeLit (#ctvar_type_literals cls) |
bd774e01d6d5
Fixing bugs in the partial-typed and fully-typed translations
paulson
parents:
22130
diff
changeset
|
414 |
val ctfree_lits = map RC.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 |
|
21509
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset
|
419 |
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
|
420 |
let val (lits,ctfree_lits) = tptp_type_lits cls |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
421 |
val cls_str = RC.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
|
422 |
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
|
423 |
(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
|
424 |
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
|
425 |
|
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 |
|
21561 | 427 |
(*** dfg format ***) |
428 |
||
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
429 |
fun dfg_literal (Literal(pol,pred)) = RC.dfg_sign pol (string_of_predicate pred); |
19720 | 430 |
|
431 |
fun dfg_clause_aux (Clause{literals, ctypes_sorts, ...}) = |
|
432 |
let val lits = map dfg_literal literals |
|
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
433 |
val (tvar_lits,tfree_lits) = RC.add_typs_aux ctypes_sorts |
22825
bd774e01d6d5
Fixing bugs in the partial-typed and fully-typed translations
paulson
parents:
22130
diff
changeset
|
434 |
val tvar_lits_strs = map RC.dfg_of_typeLit tvar_lits |
bd774e01d6d5
Fixing bugs in the partial-typed and fully-typed translations
paulson
parents:
22130
diff
changeset
|
435 |
val tfree_lits = map RC.dfg_of_typeLit tfree_lits |
19720 | 436 |
in |
437 |
(tvar_lits_strs @ lits, tfree_lits) |
|
438 |
end; |
|
439 |
||
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
440 |
fun get_uvars (CombConst _) vars = vars |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
441 |
| get_uvars (CombFree _) vars = vars |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
442 |
| get_uvars (CombVar(v,_)) vars = (v::vars) |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
443 |
| get_uvars (CombApp(P,Q)) vars = get_uvars P (get_uvars Q vars); |
19720 | 444 |
|
445 |
fun get_uvars_l (Literal(_,c)) = get_uvars c []; |
|
446 |
||
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
447 |
fun dfg_vars (Clause {literals,...}) = RC.union_all (map get_uvars_l literals); |
19720 | 448 |
|
449 |
fun clause2dfg (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) = |
|
450 |
let val (lits,tfree_lits) = dfg_clause_aux cls |
|
451 |
val vars = dfg_vars cls |
|
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
452 |
val tvars = RC.get_tvar_strs ctypes_sorts |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
453 |
val knd = RC.name_of_kind kind |
19720 | 454 |
val lits_str = commas lits |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
455 |
val cls_str = RC.gen_dfg_cls(clause_id, axiom_name, knd, lits_str, tvars@vars) |
19720 | 456 |
in (cls_str, tfree_lits) end; |
457 |
||
22064 | 458 |
(** For DFG format: accumulate function and predicate declarations **) |
19720 | 459 |
|
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
460 |
fun addtypes tvars tab = foldl RC.add_foltype_funcs tab tvars; |
19720 | 461 |
|
22825
bd774e01d6d5
Fixing bugs in the partial-typed and fully-typed translations
paulson
parents:
22130
diff
changeset
|
462 |
fun add_decls (CombConst(c,tp,tvars), (funcs,preds)) = |
22064 | 463 |
if c = "equal" then (addtypes tvars funcs, preds) |
21561 | 464 |
else |
465 |
(case !typ_level of |
|
22851
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
466 |
T_PARTIAL => (RC.add_foltype_funcs (tp, Symtab.update(c,0) funcs), preds) |
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
467 |
| _ => |
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
468 |
let val arity = min_arity_of c |
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
469 |
val ntys = if !typ_level = T_CONST then length tvars else 0 |
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
470 |
val addit = Symtab.update(c, arity+ntys) |
22064 | 471 |
in |
472 |
if needs_hBOOL c then (addtypes tvars (addit funcs), preds) |
|
473 |
else (addtypes tvars funcs, addit preds) |
|
22851
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
474 |
end) |
22064 | 475 |
| add_decls (CombFree(v,ctp), (funcs,preds)) = |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
476 |
(RC.add_foltype_funcs (ctp,Symtab.update (v,0) funcs), preds) |
22064 | 477 |
| add_decls (CombVar(_,ctp), (funcs,preds)) = |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
478 |
(RC.add_foltype_funcs (ctp,funcs), preds) |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
479 |
| add_decls (CombApp(P,Q),decls) = add_decls(P,add_decls (Q,decls)); |
19720 | 480 |
|
22064 | 481 |
fun add_literal_decls (Literal(_,c), decls) = add_decls (c,decls); |
19720 | 482 |
|
22064 | 483 |
fun add_clause_decls (Clause {literals, ...}, decls) = |
484 |
foldl add_literal_decls decls literals |
|
19720 | 485 |
handle Symtab.DUP a => raise ERROR ("function " ^ a ^ " has multiple arities") |
486 |
||
22064 | 487 |
fun decls_of_clauses clauses arity_clauses = |
488 |
let val happ_ar = case !typ_level of T_PARTIAL => 3 | _ => 2 |
|
22825
bd774e01d6d5
Fixing bugs in the partial-typed and fully-typed translations
paulson
parents:
22130
diff
changeset
|
489 |
val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",happ_ar) Symtab.empty) |
22064 | 490 |
val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty |
491 |
val (functab,predtab) = (foldl add_clause_decls (init_functab, init_predtab) clauses) |
|
492 |
in |
|
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
493 |
(Symtab.dest (foldl RC.add_arityClause_funcs functab arity_clauses), |
22064 | 494 |
Symtab.dest predtab) |
495 |
end; |
|
19720 | 496 |
|
21398
11996e938dfe
Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents:
21254
diff
changeset
|
497 |
fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) = |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
498 |
foldl RC.add_type_sort_preds preds ctypes_sorts |
21398
11996e938dfe
Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents:
21254
diff
changeset
|
499 |
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
|
500 |
|
11996e938dfe
Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents:
21254
diff
changeset
|
501 |
(*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
|
502 |
fun preds_of_clauses clauses clsrel_clauses arity_clauses = |
19720 | 503 |
Symtab.dest |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
504 |
(foldl RC.add_classrelClause_preds |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
505 |
(foldl RC.add_arityClause_preds |
22064 | 506 |
(foldl add_clause_preds Symtab.empty clauses) |
19720 | 507 |
arity_clauses) |
508 |
clsrel_clauses) |
|
509 |
||
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
510 |
|
21398
11996e938dfe
Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents:
21254
diff
changeset
|
511 |
|
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
512 |
(**********************************************************************) |
19198
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
513 |
(* write clauses to files *) |
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
514 |
(**********************************************************************) |
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
515 |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
516 |
|
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
517 |
val init_counters = |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
518 |
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
|
519 |
("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
|
520 |
("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
|
521 |
("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
|
522 |
|
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
523 |
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
|
524 |
(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
|
525 |
| 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
|
526 |
| 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
|
527 |
| count_combterm (CombVar(v,tp), ct) = ct |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
528 |
| count_combterm (CombApp(t1,t2), ct) = count_combterm(t1, count_combterm(t2, ct)); |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
529 |
|
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
530 |
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
|
531 |
|
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
532 |
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
|
533 |
|
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
534 |
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
|
535 |
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
|
536 |
else ct; |
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
537 |
|
20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
538 |
val cnf_helper_thms = ResAxioms.cnf_rules_pairs o (map ResAxioms.pairname) |
20644 | 539 |
|
22064 | 540 |
fun get_helper_clauses (conjectures, axclauses, user_lemmas) = |
541 |
let val ct0 = foldl count_clause init_counters conjectures |
|
542 |
val ct = foldl (count_user_clause user_lemmas) ct0 axclauses |
|
543 |
fun needed c = valOf (Symtab.lookup ct c) > 0 |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
544 |
val IK = if needed "c_COMBI" orelse needed "c_COMBK" |
22130 | 545 |
then (Output.debug (fn () => "Include combinator I K"); cnf_helper_thms [comb_I,comb_K]) |
21135 | 546 |
else [] |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
547 |
val BC = if needed "c_COMBB" orelse needed "c_COMBC" |
22130 | 548 |
then (Output.debug (fn () => "Include combinator B C"); cnf_helper_thms [comb_B,comb_C]) |
21135 | 549 |
else [] |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
550 |
val S = if needed "c_COMBS" |
22130 | 551 |
then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms [comb_S]) |
21135 | 552 |
else [] |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
553 |
val B'C' = if needed "c_COMBB_e" orelse needed "c_COMBC_e" |
22130 | 554 |
then (Output.debug (fn () => "Include combinator B' C'"); cnf_helper_thms [comb_B', comb_C']) |
21135 | 555 |
else [] |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
556 |
val S' = if needed "c_COMBS_e" |
22130 | 557 |
then (Output.debug (fn () => "Include combinator S'"); cnf_helper_thms [comb_S']) |
21135 | 558 |
else [] |
20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
559 |
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
|
560 |
in |
22064 | 561 |
map #2 (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
|
562 |
end |
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
563 |
|
22064 | 564 |
(*Find the minimal arity of each function mentioned in the term. Also, note which uses |
565 |
are not at top level, to see if hBOOL is needed.*) |
|
566 |
fun count_constants_term toplev t = |
|
567 |
let val (head, args) = strip_comb t |
|
568 |
val n = length args |
|
569 |
val _ = List.app (count_constants_term false) args |
|
570 |
in |
|
571 |
case head of |
|
572 |
CombConst (a,_,_) => (*predicate or function version of "equal"?*) |
|
573 |
let val a = if a="equal" andalso not toplev then "c_fequal" else a |
|
574 |
in |
|
575 |
const_min_arity := Symtab.map_default (a,n) (curry Int.min n) (!const_min_arity); |
|
576 |
if toplev then () |
|
577 |
else const_needs_hBOOL := Symtab.update (a,true) (!const_needs_hBOOL) |
|
578 |
end |
|
579 |
| ts => () |
|
580 |
end; |
|
581 |
||
582 |
(*A literal is a top-level term*) |
|
583 |
fun count_constants_lit (Literal (_,t)) = count_constants_term true t; |
|
584 |
||
585 |
fun count_constants_clause (Clause{literals,...}) = List.app count_constants_lit literals; |
|
586 |
||
587 |
fun display_arity (c,n) = |
|
22130 | 588 |
Output.debug (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^ |
22064 | 589 |
(if needs_hBOOL c then " needs hBOOL" else "")); |
590 |
||
591 |
fun count_constants (conjectures, axclauses, helper_clauses) = |
|
22851
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
592 |
if !minimize_applies andalso !typ_level<>T_PARTIAL then |
22064 | 593 |
(List.app count_constants_clause conjectures; |
594 |
List.app count_constants_clause axclauses; |
|
595 |
List.app count_constants_clause helper_clauses; |
|
596 |
List.app display_arity (Symtab.dest (!const_min_arity))) |
|
597 |
else (); |
|
598 |
||
20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
599 |
(* tptp format *) |
19491
cd6c71c57f53
changed the functions for getting HOL helper clauses.
mengj
parents:
19452
diff
changeset
|
600 |
|
19198
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
601 |
(* write TPTP format to a single file *) |
22064 | 602 |
fun tptp_write_file thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas = |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
603 |
let val conjectures = make_conjecture_clauses thms |
22064 | 604 |
val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses ax_tuples) |
605 |
val helper_clauses = get_helper_clauses (conjectures, axclauses, user_lemmas) |
|
606 |
val _ = count_constants (conjectures, axclauses, helper_clauses); |
|
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
607 |
val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp conjectures) |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
608 |
val tfree_clss = map RC.tptp_tfree_clause (foldl (op union_string) [] tfree_litss) |
22064 | 609 |
val out = TextIO.openOut filename |
19198
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
610 |
in |
22064 | 611 |
List.app (curry TextIO.output out o #1 o clause2tptp) axclauses; |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
612 |
RC.writeln_strs out tfree_clss; |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
613 |
RC.writeln_strs out tptp_clss; |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
614 |
List.app (curry TextIO.output out o RC.tptp_classrelClause) classrel_clauses; |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
615 |
List.app (curry TextIO.output out o RC.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
|
616 |
List.app (curry TextIO.output out o #1 o clause2tptp) helper_clauses; |
20022 | 617 |
TextIO.closeOut out; |
618 |
clnames |
|
19198
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
619 |
end; |
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
620 |
|
19720 | 621 |
|
20644 | 622 |
|
19720 | 623 |
(* dfg format *) |
624 |
||
22064 | 625 |
fun dfg_write_file thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas = |
626 |
let val conjectures = make_conjecture_clauses thms |
|
627 |
val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses ax_tuples) |
|
628 |
val helper_clauses = get_helper_clauses (conjectures, axclauses, user_lemmas) |
|
629 |
val _ = count_constants (conjectures, axclauses, helper_clauses); |
|
19720 | 630 |
val (dfg_clss,tfree_litss) = ListPair.unzip (map clause2dfg conjectures) |
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21617
diff
changeset
|
631 |
and probname = Path.implode (Path.base (Path.explode filename)) |
22064 | 632 |
val axstrs = map (#1 o clause2dfg) axclauses |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
633 |
val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss) |
19720 | 634 |
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
|
635 |
val helper_clauses_strs = map (#1 o clause2dfg) helper_clauses |
22064 | 636 |
val (funcs,cl_preds) = decls_of_clauses (helper_clauses @ conjectures @ axclauses) arity_clauses |
637 |
and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses |
|
19720 | 638 |
in |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
639 |
TextIO.output (out, RC.string_of_start probname); |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
640 |
TextIO.output (out, RC.string_of_descrip probname); |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
641 |
TextIO.output (out, RC.string_of_symbols |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
642 |
(RC.string_of_funcs funcs) |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
643 |
(RC.string_of_preds (cl_preds @ ty_preds))); |
19720 | 644 |
TextIO.output (out, "list_of_clauses(axioms,cnf).\n"); |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
645 |
RC.writeln_strs out axstrs; |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
646 |
List.app (curry TextIO.output out o RC.dfg_classrelClause) classrel_clauses; |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
647 |
List.app (curry TextIO.output out o RC.dfg_arity_clause) arity_clauses; |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
648 |
RC.writeln_strs out helper_clauses_strs; |
19720 | 649 |
TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"); |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
650 |
RC.writeln_strs out tfree_clss; |
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
651 |
RC.writeln_strs out dfg_clss; |
20953
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
652 |
TextIO.output (out, "end_of_list.\n\n"); |
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
653 |
(*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
|
654 |
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
|
655 |
TextIO.output (out, "end_problem.\n"); |
20022 | 656 |
TextIO.closeOut out; |
657 |
clnames |
|
19720 | 658 |
end; |
659 |
||
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset
|
660 |
end |