author | paulson |
Thu, 12 Oct 2006 15:50:43 +0200 | |
changeset 20997 | 4b500d78cb4f |
parent 20953 | 1ea394dc2a0f |
child 21108 | 04d8e6eb9a2e |
permissions | -rw-r--r-- |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
1 |
(* ID: $Id$ |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
2 |
Author: Jia Meng, NICTA |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
3 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
4 |
FOL clauses translated from HOL formulae. Combinators are used to represent lambda terms. |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
5 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
6 |
*) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
7 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
8 |
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
|
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 |
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
|
11 |
|
20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
12 |
(* 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
|
13 |
val ext = thm "HOL.ext"; |
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
14 |
val comb_I = thm "Reconstruction.COMBI_def"; |
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
15 |
val comb_K = thm "Reconstruction.COMBK_def"; |
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
16 |
val comb_B = thm "Reconstruction.COMBB_def"; |
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
17 |
val comb_C = thm "Reconstruction.COMBC_def"; |
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
18 |
val comb_S = thm "Reconstruction.COMBS_def"; |
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
19 |
val comb_B' = thm "Reconstruction.COMBB'_def"; |
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
20 |
val comb_C' = thm "Reconstruction.COMBC'_def"; |
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
21 |
val comb_S' = thm "Reconstruction.COMBS'_def"; |
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
22 |
val fequal_imp_equal = thm "Reconstruction.fequal_imp_equal"; |
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
23 |
val equal_imp_fequal = thm "Reconstruction.equal_imp_fequal"; |
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
24 |
|
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
25 |
|
20997 | 26 |
(*A flag to set if we use extra combinators B',C',S', currently FALSE as the 5 standard |
27 |
combinators appear to work best.*) |
|
28 |
val use_combB'C'S' = 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
|
29 |
|
20644 | 30 |
val combI_count = ref 0; |
31 |
val combK_count = ref 0; |
|
32 |
val combB_count = ref 0; |
|
33 |
val combC_count = ref 0; |
|
34 |
val combS_count = ref 0; |
|
35 |
||
36 |
val combB'_count = ref 0; |
|
37 |
val combC'_count = ref 0; |
|
38 |
val combS'_count = ref 0; |
|
39 |
||
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
|
40 |
|
20644 | 41 |
fun increI count_comb = if count_comb then combI_count := !combI_count + 1 else (); |
42 |
fun increK count_comb = if count_comb then combK_count := !combK_count + 1 else (); |
|
43 |
fun increB count_comb = if count_comb then combB_count := !combB_count + 1 else (); |
|
44 |
fun increC count_comb = if count_comb then combC_count := !combC_count + 1 else (); |
|
45 |
fun increS count_comb = if count_comb then combS_count := !combS_count + 1 else (); |
|
46 |
fun increB' count_comb = if count_comb then combB'_count := !combB'_count + 1 else (); |
|
47 |
fun increC' count_comb = if count_comb then combC'_count := !combC'_count + 1 else (); |
|
48 |
fun increS' count_comb = if count_comb then combS'_count := !combS'_count + 1 else (); |
|
49 |
||
50 |
||
51 |
exception DECRE_COMB of string; |
|
20953
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
52 |
fun decreB count_comb n = |
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
53 |
if count_comb then |
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
54 |
if !combB_count >= n then combB_count := !combB_count - n else raise DECRE_COMB "COMBB" |
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
55 |
else (); |
20644 | 56 |
|
20953
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
57 |
fun decreC count_comb n = |
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
58 |
if count_comb then |
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
59 |
if !combC_count >= n then combC_count := !combC_count - n else raise DECRE_COMB "COMBC" |
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
60 |
else (); |
20644 | 61 |
|
20953
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
62 |
fun decreS count_comb n = |
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
63 |
if count_comb then |
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
64 |
if !combS_count >= n then combS_count := !combS_count - n else raise DECRE_COMB "COMBS" |
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
65 |
else (); |
20130
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
66 |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
67 |
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
|
68 |
|
20644 | 69 |
fun init thy = (combI_count:=0; combK_count:=0;combB_count:=0;combC_count:=0;combS_count:=0;combB'_count:=0;combC'_count:=0;combS'_count:=0; |
20022 | 70 |
const_typargs := Sign.const_typargs thy); |
19198
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
71 |
|
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
|
72 |
(**********************************************************************) |
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 |
(* 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
|
74 |
(**********************************************************************) |
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 |
|
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
|
76 |
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
|
77 |
| 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
|
78 |
| 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
|
79 |
| 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
|
80 |
|
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
|
81 |
|
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
|
82 |
exception BND of term; |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
83 |
|
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
|
84 |
fun decre_bndVar (Bound n) = Bound (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
|
85 |
| decre_bndVar (P $ Q) = (decre_bndVar P) $ (decre_bndVar Q) |
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
|
86 |
| decre_bndVar t = |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
87 |
case t of Const(_,_) => t |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
88 |
| Free(_,_) => t |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
89 |
| Var(_,_) => t |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
90 |
| Abs(_,_,_) => raise BND(t); (*should not occur*) |
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
|
91 |
|
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
|
92 |
|
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
|
93 |
(*******************************************) |
20953
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
94 |
fun mk_compact_comb (tm as (Const("Reconstruction.COMBB",_)$p) $ (Const("Reconstruction.COMBB",_)$q$r)) Bnds count_comb = |
20644 | 95 |
let val tp_p = Term.type_of1(Bnds,p) |
96 |
val tp_q = Term.type_of1(Bnds,q) |
|
97 |
val tp_r = Term.type_of1(Bnds,r) |
|
98 |
val typ = Term.type_of1(Bnds,tm) |
|
99 |
val typ_B' = [tp_p,tp_q,tp_r] ---> typ |
|
100 |
val _ = increB' count_comb |
|
101 |
val _ = decreB count_comb 2 |
|
102 |
in |
|
20953
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
103 |
Const("Reconstruction.COMBB'",typ_B') $ p $ q $ r |
20644 | 104 |
end |
20953
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
105 |
| mk_compact_comb (tm as (Const("Reconstruction.COMBC",_) $ (Const("Reconstruction.COMBB",_)$p$q) $ r)) Bnds count_comb = |
20644 | 106 |
let val tp_p = Term.type_of1(Bnds,p) |
107 |
val tp_q = Term.type_of1(Bnds,q) |
|
108 |
val tp_r = Term.type_of1(Bnds,r) |
|
109 |
val typ = Term.type_of1(Bnds,tm) |
|
110 |
val typ_C' = [tp_p,tp_q,tp_r] ---> typ |
|
111 |
val _ = increC' count_comb |
|
112 |
val _ = decreC count_comb 1 |
|
113 |
val _ = decreB count_comb 1 |
|
114 |
in |
|
20953
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
115 |
Const("Reconstruction.COMBC'",typ_C') $ p $ q $ r |
20644 | 116 |
end |
20953
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
117 |
| mk_compact_comb (tm as (Const("Reconstruction.COMBS",_) $ (Const("Reconstruction.COMBB",_)$p$q) $ r)) Bnds count_comb = |
20644 | 118 |
let val tp_p = Term.type_of1(Bnds,p) |
119 |
val tp_q = Term.type_of1(Bnds,q) |
|
120 |
val tp_r = Term.type_of1(Bnds,r) |
|
121 |
val typ = Term.type_of1(Bnds,tm) |
|
122 |
val typ_S' = [tp_p,tp_q,tp_r] ---> typ |
|
123 |
val _ = increS' count_comb |
|
124 |
val _ = decreS count_comb 1 |
|
125 |
val _ = decreB count_comb 1 |
|
126 |
in |
|
20953
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
127 |
Const("Reconstruction.COMBS'",typ_S') $ p $ q $ r |
20644 | 128 |
end |
129 |
| mk_compact_comb tm _ _ = tm; |
|
130 |
||
131 |
fun compact_comb t Bnds count_comb = if !use_combB'C'S' then mk_compact_comb t Bnds count_comb else t; |
|
132 |
||
20130
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
133 |
fun lam2comb (Abs(x,tp,Bound 0)) _ count_comb = |
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
|
134 |
let val tpI = Type("fun",[tp,tp]) |
20644 | 135 |
val _ = increI count_comb |
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
|
136 |
in |
20953
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
137 |
Const("Reconstruction.COMBI",tpI) |
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
|
138 |
end |
20130
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
139 |
| lam2comb (Abs(x,tp,Bound n)) Bnds count_comb = |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
140 |
let val (Bound n') = decre_bndVar (Bound n) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
141 |
val tb = List.nth(Bnds,n') |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
142 |
val tK = Type("fun",[tb,Type("fun",[tp,tb])]) |
20644 | 143 |
val _ = increK count_comb |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
144 |
in |
20953
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
145 |
Const("Reconstruction.COMBK",tK) $ (Bound n') |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
146 |
end |
20130
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
147 |
| lam2comb (Abs(x,t1,Const(c,t2))) _ count_comb = |
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
|
148 |
let val tK = Type("fun",[t2,Type("fun",[t1,t2])]) |
20644 | 149 |
val _ = increK count_comb |
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
|
150 |
in |
20953
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
151 |
Const("Reconstruction.COMBK",tK) $ Const(c,t2) |
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
|
152 |
end |
20130
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
153 |
| lam2comb (Abs(x,t1,Free(v,t2))) _ count_comb = |
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
|
154 |
let val tK = Type("fun",[t2,Type("fun",[t1,t2])]) |
20644 | 155 |
val _ = increK count_comb |
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
|
156 |
in |
20953
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
157 |
Const("Reconstruction.COMBK",tK) $ Free(v,t2) |
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
|
158 |
end |
20130
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
159 |
| lam2comb (Abs(x,t1,Var(ind,t2))) _ count_comb = |
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
|
160 |
let val tK = Type("fun",[t2,Type("fun",[t1,t2])]) |
20644 | 161 |
val _ = increK count_comb |
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
|
162 |
in |
20953
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
163 |
Const("Reconstruction.COMBK",tK) $ Var(ind,t2) |
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
|
164 |
end |
20130
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
165 |
| lam2comb (t as (Abs(x,t1,P$(Bound 0)))) Bnds count_comb = |
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
|
166 |
let val nfreeP = not(is_free P 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
|
167 |
val tr = Term.type_of1(t1::Bnds,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
|
168 |
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
|
169 |
if nfreeP then (decre_bndVar 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
|
170 |
else ( |
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
|
171 |
let val tI = Type("fun",[t1,t1]) |
20130
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
172 |
val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb |
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
|
173 |
val tp' = Term.type_of1(Bnds,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
|
174 |
val tS = Type("fun",[tp',Type("fun",[tI,tr])]) |
20644 | 175 |
val _ = increI count_comb |
176 |
val _ = increS count_comb |
|
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
|
177 |
in |
20953
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
178 |
compact_comb (Const("Reconstruction.COMBS",tS) $ P' $ Const("Reconstruction.COMBI",tI)) Bnds count_comb |
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
|
179 |
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
|
180 |
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
|
181 |
|
20130
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
182 |
| lam2comb (t as (Abs(x,t1,P$Q))) Bnds count_comb = |
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
|
183 |
let val (nfreeP,nfreeQ) = (not(is_free P 0),not(is_free Q 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
|
184 |
val tpq = Term.type_of1(t1::Bnds, P$Q) |
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 |
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
|
186 |
if(nfreeP andalso nfreeQ) then ( |
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 |
let val tK = Type("fun",[tpq,Type("fun",[t1,tpq])]) |
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 |
val PQ' = decre_bndVar(P $ Q) |
20644 | 189 |
val _ = increK count_comb |
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
|
190 |
in |
20953
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
191 |
Const("Reconstruction.COMBK",tK) $ PQ' |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
192 |
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
|
193 |
else ( |
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 |
if nfreeP then ( |
20130
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
195 |
let val Q' = lam2comb (Abs(x,t1,Q)) Bnds count_comb |
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
|
196 |
val P' = decre_bndVar 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
|
197 |
val tp = Term.type_of1(Bnds,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
|
198 |
val tq' = Term.type_of1(Bnds, Q') |
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 |
val tB = Type("fun",[tp,Type("fun",[tq',Type("fun",[t1,tpq])])]) |
20644 | 200 |
val _ = increB count_comb |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
201 |
in |
20953
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
202 |
compact_comb (Const("Reconstruction.COMBB",tB) $ P' $ Q') Bnds count_comb |
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
|
203 |
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
|
204 |
else ( |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
205 |
if nfreeQ then ( |
20130
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
206 |
let val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb |
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
|
207 |
val Q' = decre_bndVar Q |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
208 |
val tq = Term.type_of1(Bnds,Q') |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
209 |
val tp' = Term.type_of1(Bnds, 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
|
210 |
val tC = Type("fun",[tp',Type("fun",[tq,Type("fun",[t1,tpq])])]) |
20644 | 211 |
val _ = increC count_comb |
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
|
212 |
in |
20953
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
213 |
compact_comb (Const("Reconstruction.COMBC",tC) $ P' $ Q') Bnds count_comb |
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
|
214 |
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
|
215 |
else( |
20130
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
216 |
let val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb |
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
217 |
val Q' = lam2comb (Abs(x,t1,Q)) Bnds count_comb |
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
|
218 |
val tp' = Term.type_of1(Bnds,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
|
219 |
val tq' = Term.type_of1(Bnds,Q') |
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
|
220 |
val tS = Type("fun",[tp',Type("fun",[tq',Type("fun",[t1,tpq])])]) |
20644 | 221 |
val _ = increS count_comb |
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
|
222 |
in |
20953
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
223 |
compact_comb (Const("Reconstruction.COMBS",tS) $ P' $ Q') Bnds count_comb |
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
|
224 |
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
|
225 |
end |
20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
226 |
| lam2comb (t as (Abs(x,t1,_))) _ _ = raise ResClause.CLAUSE("HOL CLAUSE",t); |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
227 |
|
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
|
228 |
(*********************) |
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
|
229 |
|
20130
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
230 |
fun to_comb (Abs(x,tp,b)) Bnds count_comb = |
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
231 |
let val b' = to_comb b (tp::Bnds) count_comb |
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
232 |
in lam2comb (Abs(x,tp,b')) Bnds count_comb end |
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
233 |
| to_comb (P $ Q) Bnds count_comb = ((to_comb P Bnds count_comb) $ (to_comb Q Bnds count_comb)) |
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
234 |
| 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
|
235 |
|
20644 | 236 |
|
20130
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
237 |
fun comb_of t count_comb = to_comb t [] count_comb; |
20644 | 238 |
|
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 |
(* print a term containing combinators, used for debugging *) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
240 |
exception TERM_COMB of term; |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
241 |
|
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
|
242 |
fun string_of_term (Const(c,t)) = c |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
243 |
| string_of_term (Free(v,t)) = v |
20360 | 244 |
| string_of_term (Var((x,n),t)) = x ^ "_" ^ (string_of_int n) |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
245 |
| string_of_term (P $ Q) = |
20360 | 246 |
"(" ^ string_of_term P ^ " " ^ string_of_term Q ^ ")" |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
247 |
| string_of_term t = raise TERM_COMB (t); |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
248 |
|
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
|
249 |
|
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 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
251 |
(******************************************************) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
252 |
(* 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
|
253 |
(******************************************************) |
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
|
254 |
|
20281
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
mengj
parents:
20274
diff
changeset
|
255 |
datatype type_level = T_FULL | T_PARTIAL | T_CONST | T_NONE; |
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
mengj
parents:
20274
diff
changeset
|
256 |
|
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
mengj
parents:
20274
diff
changeset
|
257 |
val typ_level = ref T_CONST; |
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
mengj
parents:
20274
diff
changeset
|
258 |
|
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
mengj
parents:
20274
diff
changeset
|
259 |
fun full_types () = (typ_level:=T_FULL); |
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
mengj
parents:
20274
diff
changeset
|
260 |
fun partial_types () = (typ_level:=T_PARTIAL); |
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
mengj
parents:
20274
diff
changeset
|
261 |
fun const_types_only () = (typ_level:=T_CONST); |
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
mengj
parents:
20274
diff
changeset
|
262 |
fun no_types () = (typ_level:=T_NONE); |
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
mengj
parents:
20274
diff
changeset
|
263 |
|
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
mengj
parents:
20274
diff
changeset
|
264 |
|
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
mengj
parents:
20274
diff
changeset
|
265 |
fun find_typ_level () = !typ_level; |
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
mengj
parents:
20274
diff
changeset
|
266 |
|
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
mengj
parents:
20274
diff
changeset
|
267 |
|
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
|
268 |
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
|
269 |
datatype kind = Axiom | Conjecture; |
20360 | 270 |
|
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
271 |
fun name_of_kind Axiom = "axiom" |
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
|
272 |
| name_of_kind Conjecture = "conjecture"; |
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
|
273 |
|
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
|
274 |
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
|
275 |
type indexname = Term.indexname; |
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
|
276 |
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
|
277 |
type csort = Term.sort; |
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
278 |
type ctyp = ResClause.fol_type; |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
279 |
|
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
280 |
val string_of_ctyp = ResClause.string_of_fol_type; |
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 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
282 |
type ctyp_var = ResClause.typ_var; |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
283 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
284 |
type ctype_literal = ResClause.type_literal; |
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 |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
287 |
datatype combterm = CombConst of string * ctyp * ctyp 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
|
288 |
| CombFree of string * ctyp |
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 |
| CombVar of string * ctyp |
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 |
| CombApp of combterm * combterm * ctyp |
19452 | 291 |
| Bool of combterm; |
20360 | 292 |
|
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 |
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
|
294 |
|
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
|
295 |
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
|
296 |
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
|
297 |
axiom_name: axiom_name, |
19964 | 298 |
th: thm, |
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
|
299 |
kind: kind, |
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
|
300 |
literals: literal list, |
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
|
301 |
ctypes_sorts: (ctyp_var * csort) list, |
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
|
302 |
ctvar_type_literals: ctype_literal list, |
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 |
ctfree_type_literals: ctype_literal list}; |
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
|
304 |
|
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
|
305 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
306 |
fun string_of_kind (Clause cls) = name_of_kind (#kind 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
|
307 |
fun get_axiomName (Clause cls) = #axiom_name 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
|
308 |
fun get_clause_id (Clause cls) = #clause_id 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
|
309 |
|
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
310 |
fun get_literals (c as Clause(cls)) = #literals cls; |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
311 |
|
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
|
312 |
|
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
|
313 |
(*********************************************************************) |
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
|
314 |
(* 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
|
315 |
(*********************************************************************) |
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
|
316 |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
317 |
fun isFalse (Literal(pol,Bool(CombConst(c,_,_)))) = |
20360 | 318 |
(pol andalso c = "c_False") orelse |
319 |
(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
|
320 |
| 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
|
321 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
322 |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
323 |
fun isTrue (Literal (pol,Bool(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
|
324 |
(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
|
325 |
(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
|
326 |
| 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
|
327 |
|
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
|
328 |
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
|
329 |
|
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
330 |
fun type_of (Type (a, Ts)) = |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
331 |
let val (folTypes,ts) = types_of Ts |
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
|
332 |
val t = ResClause.make_fixed_type_const a |
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
|
333 |
in |
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
334 |
(ResClause.mk_fol_type("Comp",t,folTypes),ts) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
335 |
end |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
336 |
| type_of (tp as (TFree(a,s))) = |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
337 |
let val t = ResClause.make_fixed_type_var a |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
338 |
in |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
339 |
(ResClause.mk_fol_type("Fixed",t,[]),[ResClause.mk_typ_var_sort tp]) |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
340 |
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
|
341 |
| type_of (tp as (TVar(v,s))) = |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
342 |
let val t = ResClause.make_schematic_type_var v |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
343 |
in |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
344 |
(ResClause.mk_fol_type("Var",t,[]),[ResClause.mk_typ_var_sort tp]) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
345 |
end |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
346 |
|
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
347 |
and types_of Ts = |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
348 |
let val foltyps_ts = map type_of Ts |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
349 |
val (folTyps,ts) = ListPair.unzip foltyps_ts |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
350 |
in |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
351 |
(folTyps,ResClause.union_all ts) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
352 |
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
|
353 |
|
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
|
354 |
(* 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
|
355 |
fun simp_type_of (Type (a, Ts)) = |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
356 |
let val typs = map simp_type_of Ts |
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
|
357 |
val t = ResClause.make_fixed_type_const a |
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
|
358 |
in |
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
359 |
ResClause.mk_fol_type("Comp",t,typs) |
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
|
360 |
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
|
361 |
| simp_type_of (TFree (a,s)) = ResClause.mk_fol_type("Fixed",ResClause.make_fixed_type_var a,[]) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
362 |
| simp_type_of (TVar (v,s)) = ResClause.mk_fol_type("Var",ResClause.make_schematic_type_var v,[]); |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
363 |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
364 |
|
20865
2cfa020109c1
Changed and removed some functions related to combinators, since they are Isabelle constants now.
mengj
parents:
20864
diff
changeset
|
365 |
fun const_type_of (c,t) = |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
366 |
let val (tp,ts) = type_of t |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
367 |
val tvars = !const_typargs(c,t) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
368 |
val tvars' = map simp_type_of tvars |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
369 |
in |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
370 |
(tp,ts,tvars') |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
371 |
end; |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
372 |
|
20644 | 373 |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
374 |
fun is_bool_type (Type("bool",[])) = true |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
375 |
| is_bool_type _ = 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
|
376 |
|
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
|
377 |
|
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
|
378 |
(* 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
|
379 |
fun combterm_of (Const(c,t)) = |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
380 |
let val (tp,ts,tvar_list) = const_type_of (c,t) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
381 |
val is_bool = is_bool_type t |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
382 |
val c' = CombConst(ResClause.make_fixed_const c,tp,tvar_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
|
383 |
val c'' = if is_bool then Bool(c') else c' |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
384 |
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
|
385 |
(c'',ts) |
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
|
386 |
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
|
387 |
| combterm_of (Free(v,t)) = |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
388 |
let val (tp,ts) = type_of t |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
389 |
val is_bool = is_bool_type 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
|
390 |
val v' = if ResClause.isMeta v then CombVar(ResClause.make_schematic_var(v,0),tp) |
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 |
else CombFree(ResClause.make_fixed_var v,tp) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
392 |
val v'' = if is_bool then Bool(v') else v' |
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 |
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
|
394 |
(v'',ts) |
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 |
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
|
396 |
| combterm_of (Var(v,t)) = |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
397 |
let val (tp,ts) = type_of t |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
398 |
val is_bool = is_bool_type 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
|
399 |
val v' = CombVar(ResClause.make_schematic_var v,tp) |
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
|
400 |
val v'' = if is_bool then Bool(v') else v' |
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
|
401 |
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
|
402 |
(v'',ts) |
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
|
403 |
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
|
404 |
| combterm_of (t as (P $ Q)) = |
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
|
405 |
let val (P',tsP) = combterm_of 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
|
406 |
val (Q',tsQ) = combterm_of Q |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
407 |
val tp = Term.type_of t |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
408 |
val tp' = simp_type_of tp |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
409 |
val is_bool = is_bool_type tp |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
410 |
val t' = CombApp(P',Q',tp') |
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 |
val t'' = if is_bool then Bool(t') else t' |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
412 |
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
|
413 |
(t'',tsP union tsQ) |
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
|
414 |
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
|
415 |
|
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 |
fun predicate_of ((Const("Not",_) $ P), polarity) = |
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 |
predicate_of (P, not polarity) |
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
|
418 |
| predicate_of (term,polarity) = (combterm_of term,polarity); |
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
|
419 |
|
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 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
421 |
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
|
422 |
| literals_of_term1 args (Const("op |",_) $ P $ Q) = |
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 |
let val args' = 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
|
424 |
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
|
425 |
literals_of_term1 args' Q |
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 |
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
|
427 |
| literals_of_term1 (lits,ts) 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
|
428 |
let val ((pred,ts'),pol) = predicate_of (P,true) |
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
|
429 |
val lits' = Literal(pol,pred)::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
|
430 |
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
|
431 |
(lits',ts union ts') |
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
|
432 |
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
|
433 |
|
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
|
434 |
|
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
|
435 |
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
|
436 |
|
20274 | 437 |
fun occurs a (CombVar(b,_)) = a = b |
438 |
| occurs a (CombApp(t1,t2,_)) = (occurs a t1) orelse (occurs a t2) |
|
439 |
| occurs _ _ = false |
|
440 |
||
441 |
fun too_general_terms (CombVar(v,_), t) = not (occurs v t) |
|
442 |
| too_general_terms _ = false; |
|
443 |
||
20360 | 444 |
fun too_general_lit (Literal(true,(Bool(CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))))) = |
445 |
too_general_terms (t1,t2) orelse too_general_terms (t2,t1) |
|
20274 | 446 |
| too_general_lit _ = false; |
447 |
||
20130
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
448 |
(* forbid a clause that contains hBOOL(V) *) |
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
449 |
fun too_general [] = false |
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
450 |
| too_general (lit::lits) = |
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
451 |
case lit of Literal(_,Bool(CombVar(_,_))) => true |
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
452 |
| _ => too_general lits; |
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
453 |
|
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
|
454 |
(* making axiom and conjecture clauses *) |
20274 | 455 |
exception MAKE_CLAUSE |
20130
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
456 |
fun make_clause(clause_id,axiom_name,kind,thm,is_user) = |
19444
085568445283
Take conjectures and axioms as thms when convert them to ResHolClause.clause format.
mengj
parents:
19354
diff
changeset
|
457 |
let val term = prop_of thm |
20130
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
458 |
val term' = comb_of term is_user |
20016 | 459 |
val (lits,ctypes_sorts) = literals_of_term term' |
18856
4669dec681f4
tidy-up of res_clause.ML, removing the "predicates" field
paulson
parents:
18725
diff
changeset
|
460 |
val (ctvar_lits,ctfree_lits) = ResClause.add_typs_aux ctypes_sorts |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
461 |
in |
20016 | 462 |
if forall isFalse lits |
463 |
then error "Problem too trivial for resolution (empty clause)" |
|
20360 | 464 |
else if too_general lits |
465 |
then (Output.debug ("Omitting " ^ axiom_name ^ ": clause contains universal predicates"); |
|
466 |
raise MAKE_CLAUSE) |
|
20274 | 467 |
else |
20281
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
mengj
parents:
20274
diff
changeset
|
468 |
if (!typ_level <> T_FULL) andalso kind=Axiom andalso forall too_general_lit lits |
20360 | 469 |
then (Output.debug ("Omitting " ^ axiom_name ^ ": equalities are too general"); |
470 |
raise MAKE_CLAUSE) |
|
20016 | 471 |
else |
472 |
Clause {clause_id = clause_id, axiom_name = axiom_name, th = thm, kind = kind, |
|
473 |
literals = lits, ctypes_sorts = ctypes_sorts, |
|
474 |
ctvar_type_literals = ctvar_lits, |
|
475 |
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
|
476 |
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
|
477 |
|
20016 | 478 |
|
20360 | 479 |
fun make_axiom_clause thm (ax_name,cls_id,is_user) = |
480 |
make_clause(cls_id,ax_name,Axiom,thm,is_user); |
|
20016 | 481 |
|
20130
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
482 |
fun make_axiom_clauses [] user_lemmas = [] |
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
483 |
| make_axiom_clauses ((thm,(name,id))::thms) user_lemmas = |
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
484 |
let val is_user = name mem user_lemmas |
20360 | 485 |
val cls = SOME (make_axiom_clause thm (name,id,is_user)) |
486 |
handle MAKE_CLAUSE => NONE |
|
20130
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
487 |
val clss = make_axiom_clauses thms user_lemmas |
19354 | 488 |
in |
20130
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
489 |
case cls of NONE => clss |
20360 | 490 |
| SOME(cls') => if isTaut cls' then clss |
491 |
else (name,cls')::clss |
|
19354 | 492 |
end; |
493 |
||
494 |
||
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
|
495 |
fun make_conjecture_clauses_aux _ [] = [] |
20421 | 496 |
| make_conjecture_clauses_aux n (th::ths) = |
497 |
make_clause(n,"conjecture",Conjecture,th,true) :: |
|
498 |
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
|
499 |
|
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
|
500 |
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
|
501 |
|
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
|
502 |
|
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
|
503 |
(**********************************************************************) |
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
|
504 |
(* 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
|
505 |
(* TPTP used by Vampire and E *) |
19720 | 506 |
(* 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
|
507 |
(**********************************************************************) |
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
|
508 |
|
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
|
509 |
val type_wrapper = "typeinfo"; |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
510 |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
511 |
fun wrap_type (c,t) = |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
512 |
case !typ_level of T_FULL => type_wrapper ^ (ResClause.paren_pack [c,t]) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
513 |
| _ => c; |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
514 |
|
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
|
515 |
|
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
|
516 |
val bool_tp = ResClause.make_fixed_type_const "bool"; |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
517 |
|
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
|
518 |
val app_str = "hAPP"; |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
519 |
|
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
|
520 |
val bool_str = "hBOOL"; |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
521 |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
522 |
exception STRING_OF_COMBTERM of int; |
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
|
523 |
|
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
|
524 |
(* convert literals of clauses into strings *) |
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
525 |
fun string_of_combterm1_aux _ (CombConst(c,tp,_)) = |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
526 |
let val tp' = string_of_ctyp tp |
20864
bb75b876b260
Now the DFG output includes correct declarations of c_fequal, but not hEXTENT
paulson
parents:
20791
diff
changeset
|
527 |
val c' = if c = "equal" then "c_fequal" else c |
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
528 |
in |
19452 | 529 |
(wrap_type (c',tp'),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
|
530 |
end |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
531 |
| string_of_combterm1_aux _ (CombFree(v,tp)) = |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
532 |
let val tp' = string_of_ctyp tp |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
533 |
in |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
534 |
(wrap_type (v,tp'),tp') |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
535 |
end |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
536 |
| string_of_combterm1_aux _ (CombVar(v,tp)) = |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
537 |
let val tp' = string_of_ctyp tp |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
538 |
in |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
539 |
(wrap_type (v,tp'),tp') |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
540 |
end |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
541 |
| string_of_combterm1_aux is_pred (CombApp(t1,t2,tp)) = |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
542 |
let val (s1,tp1) = string_of_combterm1_aux is_pred t1 |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
543 |
val (s2,tp2) = string_of_combterm1_aux is_pred t2 |
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
544 |
val tp' = ResClause.string_of_fol_type tp |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
545 |
val r = case !typ_level of T_FULL => type_wrapper ^ (ResClause.paren_pack [(app_str ^ (ResClause.paren_pack [s1,s2])),tp']) |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
546 |
| T_PARTIAL => app_str ^ (ResClause.paren_pack [s1,s2,tp1]) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
547 |
| T_NONE => app_str ^ (ResClause.paren_pack [s1,s2]) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
548 |
| T_CONST => raise STRING_OF_COMBTERM (1) (*should not happen, if happened may be a bug*) |
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
549 |
in (r,tp') |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
550 |
|
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
551 |
end |
19452 | 552 |
| string_of_combterm1_aux is_pred (Bool(CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))) = |
553 |
if is_pred then |
|
554 |
let val (s1,_) = string_of_combterm1_aux false t1 |
|
555 |
val (s2,_) = string_of_combterm1_aux false t2 |
|
556 |
in |
|
557 |
("equal" ^ (ResClause.paren_pack [s1,s2]),bool_tp) |
|
558 |
end |
|
559 |
else |
|
560 |
let val (t,_) = string_of_combterm1_aux false (CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2)) |
|
561 |
in |
|
562 |
(t,bool_tp) |
|
563 |
end |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
564 |
| string_of_combterm1_aux is_pred (Bool(t)) = |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
565 |
let val (t',_) = string_of_combterm1_aux false t |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
566 |
val r = if is_pred then bool_str ^ (ResClause.paren_pack [t']) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
567 |
else 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
|
568 |
in |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
569 |
(r,bool_tp) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
570 |
end; |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
571 |
|
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
572 |
fun string_of_combterm1 is_pred term = fst (string_of_combterm1_aux is_pred term); |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
573 |
|
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
574 |
fun string_of_combterm2 _ (CombConst(c,tp,tvars)) = |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
575 |
let val tvars' = map string_of_ctyp tvars |
20864
bb75b876b260
Now the DFG output includes correct declarations of c_fequal, but not hEXTENT
paulson
parents:
20791
diff
changeset
|
576 |
val c' = if c = "equal" then "c_fequal" else c |
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
577 |
in |
19452 | 578 |
c' ^ (ResClause.paren_pack tvars') |
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
579 |
end |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
580 |
| string_of_combterm2 _ (CombFree(v,tp)) = v |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
581 |
| string_of_combterm2 _ (CombVar(v,tp)) = v |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
582 |
| string_of_combterm2 is_pred (CombApp(t1,t2,tp)) = |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
583 |
let val s1 = string_of_combterm2 is_pred t1 |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
584 |
val s2 = string_of_combterm2 is_pred t2 |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
585 |
in |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
586 |
app_str ^ (ResClause.paren_pack [s1,s2]) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
587 |
end |
19452 | 588 |
| string_of_combterm2 is_pred (Bool(CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))) = |
589 |
if is_pred then |
|
590 |
let val s1 = string_of_combterm2 false t1 |
|
591 |
val s2 = string_of_combterm2 false t2 |
|
592 |
in |
|
593 |
("equal" ^ (ResClause.paren_pack [s1,s2])) |
|
594 |
end |
|
595 |
else |
|
596 |
string_of_combterm2 false (CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2)) |
|
597 |
||
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
598 |
| string_of_combterm2 is_pred (Bool(t)) = |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
599 |
let val t' = string_of_combterm2 false 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
|
600 |
in |
18200 | 601 |
if is_pred then bool_str ^ (ResClause.paren_pack [t']) |
602 |
else 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
|
603 |
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
|
604 |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
605 |
|
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
606 |
|
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
607 |
fun string_of_combterm is_pred term = |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
608 |
case !typ_level of T_CONST => string_of_combterm2 is_pred term |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
609 |
| _ => string_of_combterm1 is_pred term; |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
610 |
|
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
611 |
|
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
|
612 |
fun string_of_clausename (cls_id,ax_name) = |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
613 |
ResClause.clause_prefix ^ ResClause.ascii_of ax_name ^ "_" ^ Int.toString cls_id; |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
614 |
|
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
|
615 |
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
|
616 |
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
|
617 |
|
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
|
618 |
|
19720 | 619 |
(* tptp format *) |
620 |
||
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
|
621 |
fun tptp_literal (Literal(pol,pred)) = |
18200 | 622 |
let val pred_string = string_of_combterm true 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
|
623 |
val pol_str = if pol then "++" else "--" |
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
|
624 |
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
|
625 |
pol_str ^ pred_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
|
626 |
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
|
627 |
|
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
|
628 |
|
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
|
629 |
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
|
630 |
let val lits = map tptp_literal (#literals cls) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
631 |
val ctvar_lits_strs = |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
632 |
case !typ_level of T_NONE => [] |
20360 | 633 |
| _ => map ResClause.tptp_of_typeLit (#ctvar_type_literals cls) |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
634 |
val ctfree_lits = |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
635 |
case !typ_level of T_NONE => [] |
20360 | 636 |
| _ => map ResClause.tptp_of_typeLit (#ctfree_type_literals cls) |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
637 |
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
|
638 |
(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
|
639 |
end; |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
640 |
|
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
641 |
|
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
|
642 |
fun clause2tptp 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
|
643 |
let val (lits,ctfree_lits) = tptp_type_lits 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
|
644 |
val cls_id = get_clause_id 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
|
645 |
val ax_name = get_axiomName 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
|
646 |
val knd = string_of_kind 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
|
647 |
val lits_str = ResClause.bracket_pack 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
|
648 |
val cls_str = ResClause.gen_tptp_cls(cls_id,ax_name,knd,lits_str) |
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
|
649 |
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
|
650 |
(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
|
651 |
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
|
652 |
|
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
|
653 |
|
19720 | 654 |
(* dfg format *) |
655 |
fun dfg_literal (Literal(pol,pred)) = ResClause.dfg_sign pol (string_of_combterm true pred); |
|
656 |
||
657 |
fun dfg_clause_aux (Clause{literals, ctypes_sorts, ...}) = |
|
658 |
let val lits = map dfg_literal literals |
|
659 |
val (tvar_lits,tfree_lits) = ResClause.add_typs_aux ctypes_sorts |
|
660 |
val tvar_lits_strs = |
|
661 |
case !typ_level of T_NONE => [] |
|
20360 | 662 |
| _ => map ResClause.dfg_of_typeLit tvar_lits |
19720 | 663 |
val tfree_lits = |
664 |
case !typ_level of T_NONE => [] |
|
20360 | 665 |
| _ => map ResClause.dfg_of_typeLit tfree_lits |
19720 | 666 |
in |
667 |
(tvar_lits_strs @ lits, tfree_lits) |
|
668 |
end; |
|
669 |
||
670 |
fun get_uvars (CombConst(_,_,_)) vars = vars |
|
671 |
| get_uvars (CombFree(_,_)) vars = vars |
|
672 |
| get_uvars (CombVar(v,tp)) vars = (v::vars) |
|
673 |
| get_uvars (CombApp(P,Q,tp)) vars = get_uvars P (get_uvars Q vars) |
|
674 |
| get_uvars (Bool(c)) vars = get_uvars c vars; |
|
675 |
||
676 |
||
677 |
fun get_uvars_l (Literal(_,c)) = get_uvars c []; |
|
678 |
||
679 |
fun dfg_vars (Clause {literals,...}) = ResClause.union_all (map get_uvars_l literals); |
|
680 |
||
681 |
fun clause2dfg (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) = |
|
682 |
let val (lits,tfree_lits) = dfg_clause_aux cls |
|
683 |
val vars = dfg_vars cls |
|
684 |
val tvars = ResClause.get_tvar_strs ctypes_sorts |
|
685 |
val knd = name_of_kind kind |
|
686 |
val lits_str = commas lits |
|
687 |
val cls_str = ResClause.gen_dfg_cls(clause_id, axiom_name, knd, lits_str, tvars@vars) |
|
688 |
in (cls_str, tfree_lits) end; |
|
689 |
||
690 |
||
691 |
fun init_funcs_tab funcs = |
|
19724 | 692 |
let val tp = !typ_level |
20865
2cfa020109c1
Changed and removed some functions related to combinators, since they are Isabelle constants now.
mengj
parents:
20864
diff
changeset
|
693 |
val funcs1 = case tp of T_PARTIAL => Symtab.update ("hAPP",3) funcs |
2cfa020109c1
Changed and removed some functions related to combinators, since they are Isabelle constants now.
mengj
parents:
20864
diff
changeset
|
694 |
| _ => Symtab.update ("hAPP",2) funcs |
19724 | 695 |
val funcs2 = case tp of T_FULL => Symtab.update ("typeinfo",2) funcs1 |
696 |
| _ => funcs1 |
|
697 |
in |
|
20865
2cfa020109c1
Changed and removed some functions related to combinators, since they are Isabelle constants now.
mengj
parents:
20864
diff
changeset
|
698 |
funcs2 |
19724 | 699 |
end; |
19720 | 700 |
|
701 |
||
19725
ada9bb1faba5
Changed the DFG format's functions' declaration procedure.
mengj
parents:
19724
diff
changeset
|
702 |
fun add_funcs (CombConst(c,_,tvars),funcs) = |
ada9bb1faba5
Changed the DFG format's functions' declaration procedure.
mengj
parents:
19724
diff
changeset
|
703 |
if c = "equal" then foldl ResClause.add_foltype_funcs funcs tvars |
ada9bb1faba5
Changed the DFG format's functions' declaration procedure.
mengj
parents:
19724
diff
changeset
|
704 |
else |
ada9bb1faba5
Changed the DFG format's functions' declaration procedure.
mengj
parents:
19724
diff
changeset
|
705 |
(case !typ_level of T_CONST => foldl ResClause.add_foltype_funcs (Symtab.update(c,length tvars) funcs) tvars |
ada9bb1faba5
Changed the DFG format's functions' declaration procedure.
mengj
parents:
19724
diff
changeset
|
706 |
| _ => foldl ResClause.add_foltype_funcs (Symtab.update(c,0) funcs) tvars) |
19724 | 707 |
| add_funcs (CombFree(v,ctp),funcs) = ResClause.add_foltype_funcs (ctp,Symtab.update (v,0) funcs) |
19720 | 708 |
| add_funcs (CombVar(_,ctp),funcs) = ResClause.add_foltype_funcs (ctp,funcs) |
709 |
| add_funcs (CombApp(P,Q,_),funcs) = add_funcs(P,add_funcs (Q,funcs)) |
|
710 |
| add_funcs (Bool(t),funcs) = add_funcs (t,funcs); |
|
711 |
||
712 |
||
713 |
fun add_literal_funcs (Literal(_,c), funcs) = add_funcs (c,funcs); |
|
714 |
||
715 |
fun add_clause_funcs (Clause {literals, ...}, funcs) = |
|
716 |
foldl add_literal_funcs funcs literals |
|
717 |
handle Symtab.DUP a => raise ERROR ("function " ^ a ^ " has multiple arities") |
|
718 |
||
719 |
fun funcs_of_clauses clauses arity_clauses = |
|
720 |
Symtab.dest (foldl ResClause.add_arityClause_funcs |
|
721 |
(foldl add_clause_funcs (init_funcs_tab Symtab.empty) clauses) |
|
722 |
arity_clauses) |
|
723 |
||
724 |
fun preds_of clsrel_clauses arity_clauses = |
|
725 |
Symtab.dest |
|
726 |
(foldl ResClause.add_classrelClause_preds |
|
727 |
(foldl ResClause.add_arityClause_preds |
|
728 |
(Symtab.update ("hBOOL",1) Symtab.empty) |
|
729 |
arity_clauses) |
|
730 |
clsrel_clauses) |
|
731 |
||
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
732 |
|
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
733 |
(**********************************************************************) |
19198
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
734 |
(* write clauses to files *) |
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
735 |
(**********************************************************************) |
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
736 |
|
20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
737 |
local |
19198
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
738 |
|
20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
739 |
val cnf_helper_thms = ResAxioms.cnf_rules_pairs o (map ResAxioms.pairname) |
20644 | 740 |
|
20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
741 |
in |
20644 | 742 |
|
20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
743 |
fun get_helper_clauses () = |
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
744 |
let val IK = if !combI_count > 0 orelse !combK_count > 0 then (Output.debug "Include combinator I K"; cnf_helper_thms [comb_I,comb_K]) else [] |
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
745 |
val BC = if !combB_count > 0 orelse !combC_count > 0 then (Output.debug "Include combinator B C"; cnf_helper_thms [comb_B,comb_C]) else [] |
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
746 |
val S = if !combS_count > 0 then (Output.debug "Include combinator S"; cnf_helper_thms [comb_S]) else [] |
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
747 |
val B'C' = if !combB'_count > 0 orelse !combC'_count > 0 then (Output.debug "Include combinator B' C'"; cnf_helper_thms [comb_B', comb_C']) else [] |
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
748 |
val S' = if !combS'_count > 0 then (Output.debug "Include combinator S'"; cnf_helper_thms [comb_S']) else [] |
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
749 |
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
|
750 |
in |
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
751 |
make_axiom_clauses (other @ IK @ BC @ S @ B'C' @ S') [] |
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
752 |
end |
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
753 |
|
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
754 |
end |
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
755 |
|
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
756 |
(* tptp format *) |
19491
cd6c71c57f53
changed the functions for getting HOL helper clauses.
mengj
parents:
19452
diff
changeset
|
757 |
|
19198
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
758 |
(* write TPTP format to a single file *) |
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
759 |
(* when "get_helper_clauses" is called, "include_combS" and "include_min_comb" should have correct values already *) |
20130
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
760 |
fun tptp_write_file thms filename (axclauses,classrel_clauses,arity_clauses) user_lemmas= |
19444
085568445283
Take conjectures and axioms as thms when convert them to ResHolClause.clause format.
mengj
parents:
19354
diff
changeset
|
761 |
let val clss = make_conjecture_clauses thms |
20130
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
762 |
val (clnames,axclauses') = ListPair.unzip (make_axiom_clauses axclauses user_lemmas) |
19198
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
763 |
val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp clss) |
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
764 |
val tfree_clss = map ResClause.tptp_tfree_clause (foldl (op union_string) [] tfree_litss) |
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
765 |
val out = TextIO.openOut filename |
20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
766 |
val helper_clauses = (#2 o ListPair.unzip o get_helper_clauses) () |
19198
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
767 |
in |
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
768 |
List.app (curry TextIO.output out o #1 o clause2tptp) axclauses'; |
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
769 |
ResClause.writeln_strs out tfree_clss; |
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
770 |
ResClause.writeln_strs out tptp_clss; |
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
771 |
List.app (curry TextIO.output out o ResClause.tptp_classrelClause) classrel_clauses; |
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
772 |
List.app (curry TextIO.output out o ResClause.tptp_arity_clause) arity_clauses; |
20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
773 |
List.app (curry TextIO.output out o #1 o clause2tptp) helper_clauses; |
20022 | 774 |
TextIO.closeOut out; |
775 |
clnames |
|
19198
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
776 |
end; |
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
777 |
|
19720 | 778 |
|
20644 | 779 |
|
19720 | 780 |
(* dfg format *) |
781 |
||
20130
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
782 |
fun dfg_write_file thms filename (axclauses,classrel_clauses,arity_clauses) user_lemmas = |
19720 | 783 |
let val _ = Output.debug ("Preparing to write the DFG file " ^ filename) |
784 |
val conjectures = make_conjecture_clauses thms |
|
20130
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset
|
785 |
val (clnames,axclauses') = ListPair.unzip (make_axiom_clauses axclauses user_lemmas) |
19720 | 786 |
val (dfg_clss,tfree_litss) = ListPair.unzip (map clause2dfg conjectures) |
787 |
and probname = Path.pack (Path.base (Path.unpack filename)) |
|
788 |
val (axstrs,_) = ListPair.unzip (map clause2dfg axclauses') |
|
789 |
val tfree_clss = map ResClause.dfg_tfree_clause (ResClause.union_all tfree_litss) |
|
790 |
val out = TextIO.openOut filename |
|
20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
791 |
val helper_clauses = (#2 o ListPair.unzip o get_helper_clauses) () |
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
792 |
val helper_clauses_strs = (#1 o ListPair.unzip o (map clause2dfg)) helper_clauses |
20864
bb75b876b260
Now the DFG output includes correct declarations of c_fequal, but not hEXTENT
paulson
parents:
20791
diff
changeset
|
793 |
val funcs = funcs_of_clauses (helper_clauses @ conjectures @ axclauses') arity_clauses |
bb75b876b260
Now the DFG output includes correct declarations of c_fequal, but not hEXTENT
paulson
parents:
20791
diff
changeset
|
794 |
and preds = preds_of classrel_clauses arity_clauses |
19720 | 795 |
in |
796 |
TextIO.output (out, ResClause.string_of_start probname); |
|
797 |
TextIO.output (out, ResClause.string_of_descrip probname); |
|
798 |
TextIO.output (out, ResClause.string_of_symbols (ResClause.string_of_funcs funcs) (ResClause.string_of_preds preds)); |
|
799 |
TextIO.output (out, "list_of_clauses(axioms,cnf).\n"); |
|
800 |
ResClause.writeln_strs out axstrs; |
|
801 |
List.app (curry TextIO.output out o ResClause.dfg_classrelClause) classrel_clauses; |
|
802 |
List.app (curry TextIO.output out o ResClause.dfg_arity_clause) arity_clauses; |
|
20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
803 |
ResClause.writeln_strs out helper_clauses_strs; |
19720 | 804 |
TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"); |
805 |
ResClause.writeln_strs out tfree_clss; |
|
806 |
ResClause.writeln_strs out dfg_clss; |
|
20953
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
807 |
TextIO.output (out, "end_of_list.\n\n"); |
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset
|
808 |
(*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
|
809 |
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
|
810 |
TextIO.output (out, "end_problem.\n"); |
20022 | 811 |
TextIO.closeOut out; |
812 |
clnames |
|
19720 | 813 |
end; |
814 |
||
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
|
815 |
end |