author  paulson 
Tue, 28 Nov 2006 16:19:01 +0100  
changeset 21573  8a7a68c0096c 
parent 21561  cfd2258f0b23 
child 21617  4664489469fc 
permissions  rwrr 
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

1 
(* ID: $Id$ 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

2 
Author: Jia Meng, NICTA 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

3 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

4 
FOL clauses translated from HOL formulae. Combinators are used to represent lambda terms. 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

5 
*) 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

6 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

7 
structure ResHolClause = 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

8 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

9 
struct 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

10 

20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset

11 
(* theorems for combinators and function extensionality *) 
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset

12 
val ext = thm "HOL.ext"; 
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset

13 
val comb_I = thm "ATP_Linkup.COMBI_def"; 
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset

14 
val comb_K = thm "ATP_Linkup.COMBK_def"; 
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset

15 
val comb_B = thm "ATP_Linkup.COMBB_def"; 
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset

16 
val comb_C = thm "ATP_Linkup.COMBC_def"; 
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset

17 
val comb_S = thm "ATP_Linkup.COMBS_def"; 
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset

18 
val comb_B' = thm "ATP_Linkup.COMBB'_def"; 
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset

19 
val comb_C' = thm "ATP_Linkup.COMBC'_def"; 
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset

20 
val comb_S' = thm "ATP_Linkup.COMBS'_def"; 
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset

21 
val fequal_imp_equal = thm "ATP_Linkup.fequal_imp_equal"; 
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset

22 
val equal_imp_fequal = thm "ATP_Linkup.equal_imp_fequal"; 
20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset

23 

21108  24 
(*A flag to set if we use the Turner optimizations. Currently FALSE, as the 5 standard 
20997  25 
combinators appear to work best.*) 
21108  26 
val use_Turner = ref false; 
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

27 

18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset

28 
val const_typargs = ref (Library.K [] : (string*typ > typ list)); 
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset

29 

21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

30 
fun init thy = (const_typargs := Sign.const_typargs thy); 
19198
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset

31 

17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

32 
(**********************************************************************) 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

33 
(* convert a Term.term with lambdas into a Term.term with combinators *) 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

34 
(**********************************************************************) 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

35 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

36 
fun is_free (Bound(a)) n = (a = n) 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

37 
 is_free (Abs(x,_,b)) n = (is_free b (n+1)) 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

38 
 is_free (P $ Q) n = ((is_free P n) orelse (is_free Q n)) 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

39 
 is_free _ _ = false; 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

40 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

41 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

42 
(*******************************************) 
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

43 
fun mk_compact_comb (tm as (Const("ATP_Linkup.COMBB",_)$p) $ (Const("ATP_Linkup.COMBB",_)$q$r)) bnds = 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

44 
let val tp_p = Term.type_of1(bnds,p) 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

45 
val tp_q = Term.type_of1(bnds,q) 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

46 
val tp_r = Term.type_of1(bnds,r) 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

47 
val typ = Term.type_of1(bnds,tm) 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

48 
val typ_B' = [tp_p,tp_q,tp_r] > typ 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

49 
in 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

50 
Const("ATP_Linkup.COMBB'",typ_B') $ p $ q $ r 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

51 
end 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

52 
 mk_compact_comb (tm as (Const("ATP_Linkup.COMBC",_) $ (Const("ATP_Linkup.COMBB",_)$p$q) $ r)) bnds = 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

53 
let val tp_p = Term.type_of1(bnds,p) 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

54 
val tp_q = Term.type_of1(bnds,q) 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

55 
val tp_r = Term.type_of1(bnds,r) 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

56 
val typ = Term.type_of1(bnds,tm) 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

57 
val typ_C' = [tp_p,tp_q,tp_r] > typ 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

58 
in 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

59 
Const("ATP_Linkup.COMBC'",typ_C') $ p $ q $ r 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

60 
end 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

61 
 mk_compact_comb (tm as (Const("ATP_Linkup.COMBS",_) $ (Const("ATP_Linkup.COMBB",_)$p$q) $ r)) bnds = 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

62 
let val tp_p = Term.type_of1(bnds,p) 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

63 
val tp_q = Term.type_of1(bnds,q) 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

64 
val tp_r = Term.type_of1(bnds,r) 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

65 
val typ = Term.type_of1(bnds,tm) 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

66 
val typ_S' = [tp_p,tp_q,tp_r] > typ 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

67 
in 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

68 
Const("ATP_Linkup.COMBS'",typ_S') $ p $ q $ r 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

69 
end 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

70 
 mk_compact_comb tm _ = tm; 
20644  71 

21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

72 
fun compact_comb t bnds = 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

73 
if !use_Turner then mk_compact_comb t bnds else t; 
20644  74 

21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

75 
fun lam2comb (Abs(x,tp,Bound 0)) _ = Const("ATP_Linkup.COMBI",tp>tp) 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

76 
 lam2comb (Abs(x,tp,Bound n)) bnds = 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

77 
let val tb = List.nth(bnds,n1) 
21108  78 
in 
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

79 
Const("ATP_Linkup.COMBK", [tb,tp] > tb) $ Bound (n1) 
21108  80 
end 
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

81 
 lam2comb (Abs(x,t1,Const(c,t2))) _ = Const("ATP_Linkup.COMBK",[t2,t1] > t2) $ Const(c,t2) 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

82 
 lam2comb (Abs(x,t1,Free(v,t2))) _ = Const("ATP_Linkup.COMBK",[t2,t1] > t2) $ Free(v,t2) 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

83 
 lam2comb (Abs(x,t1,Var(ind,t2))) _ = Const("ATP_Linkup.COMBK", [t2,t1] > t2) $ Var(ind,t2) 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

84 
 lam2comb (t as (Abs(x,t1,P$(Bound 0)))) bnds = 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

85 
if is_free P 0 then 
21135  86 
let val tI = [t1] > t1 
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

87 
val P' = lam2comb (Abs(x,t1,P)) bnds 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

88 
val tp' = Term.type_of1(bnds,P') 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

89 
val tr = Term.type_of1(t1::bnds,P) 
21135  90 
val tS = [tp',tI] > tr 
21108  91 
in 
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset

92 
compact_comb (Const("ATP_Linkup.COMBS",tS) $ P' $ 
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

93 
Const("ATP_Linkup.COMBI",tI)) bnds 
21108  94 
end 
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

95 
else incr_boundvars ~1 P 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

96 
 lam2comb (t as (Abs(x,t1,P$Q))) bnds = 
21108  97 
let val nfreeP = not(is_free P 0) 
98 
and nfreeQ = not(is_free Q 0) 

21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

99 
val tpq = Term.type_of1(t1::bnds, P$Q) 
21108  100 
in 
101 
if nfreeP andalso nfreeQ 

102 
then 

21135  103 
let val tK = [tpq,t1] > tpq 
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

104 
val PQ' = incr_boundvars ~1 (P $ Q) 
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

105 
in 
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset

106 
Const("ATP_Linkup.COMBK",tK) $ PQ' 
21108  107 
end 
108 
else if nfreeP then 

21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

109 
let val Q' = lam2comb (Abs(x,t1,Q)) bnds 
21135  110 
val P' = incr_boundvars ~1 P 
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

111 
val tp = Term.type_of1(bnds,P') 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

112 
val tq' = Term.type_of1(bnds, Q') 
21135  113 
val tB = [tp,tq',t1] > tpq 
21108  114 
in 
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

115 
compact_comb (Const("ATP_Linkup.COMBB",tB) $ P' $ Q') bnds 
21108  116 
end 
117 
else if nfreeQ then 

21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

118 
let val P' = lam2comb (Abs(x,t1,P)) bnds 
21135  119 
val Q' = incr_boundvars ~1 Q 
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

120 
val tq = Term.type_of1(bnds,Q') 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

121 
val tp' = Term.type_of1(bnds, P') 
21135  122 
val tC = [tp',tq,t1] > tpq 
21108  123 
in 
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

124 
compact_comb (Const("ATP_Linkup.COMBC",tC) $ P' $ Q') bnds 
21108  125 
end 
126 
else 

21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

127 
let val P' = lam2comb (Abs(x,t1,P)) bnds 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

128 
val Q' = lam2comb (Abs(x,t1,Q)) bnds 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

129 
val tp' = Term.type_of1(bnds,P') 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

130 
val tq' = Term.type_of1(bnds,Q') 
21135  131 
val tS = [tp',tq',t1] > tpq 
21108  132 
in 
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

133 
compact_comb (Const("ATP_Linkup.COMBS",tS) $ P' $ Q') bnds 
21108  134 
end 
135 
end 

21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

136 
 lam2comb (t as (Abs(x,t1,_))) _ = raise ResClause.CLAUSE("HOL CLAUSE",t); 
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

137 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

138 
(*********************) 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

139 

21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

140 
fun to_comb (Abs(x,tp,b)) bnds = 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

141 
lam2comb (Abs(x, tp, to_comb b (tp::bnds))) bnds 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

142 
 to_comb (P $ Q) bnds = (to_comb P bnds) $ (to_comb Q bnds) 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

143 
 to_comb t _ = t; 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

144 

17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

145 
(* print a term containing combinators, used for debugging *) 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

146 
exception TERM_COMB of term; 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

147 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

148 
fun string_of_term (Const(c,t)) = c 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

149 
 string_of_term (Free(v,t)) = v 
20360  150 
 string_of_term (Var((x,n),t)) = x ^ "_" ^ (string_of_int n) 
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

151 
 string_of_term (P $ Q) = 
20360  152 
"(" ^ string_of_term P ^ " " ^ string_of_term Q ^ ")" 
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

153 
 string_of_term t = raise TERM_COMB (t); 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

154 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

155 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

156 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

157 
(******************************************************) 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

158 
(* data types for typed combinator expressions *) 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

159 
(******************************************************) 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

160 

20281
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial or constanttyped.
mengj
parents:
20274
diff
changeset

161 
datatype type_level = T_FULL  T_PARTIAL  T_CONST  T_NONE; 
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial or constanttyped.
mengj
parents:
20274
diff
changeset

162 

16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial or constanttyped.
mengj
parents:
20274
diff
changeset

163 
val typ_level = ref T_CONST; 
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial or constanttyped.
mengj
parents:
20274
diff
changeset

164 

16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial or constanttyped.
mengj
parents:
20274
diff
changeset

165 
fun full_types () = (typ_level:=T_FULL); 
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial or constanttyped.
mengj
parents:
20274
diff
changeset

166 
fun partial_types () = (typ_level:=T_PARTIAL); 
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial or constanttyped.
mengj
parents:
20274
diff
changeset

167 
fun const_types_only () = (typ_level:=T_CONST); 
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial or constanttyped.
mengj
parents:
20274
diff
changeset

168 
fun no_types () = (typ_level:=T_NONE); 
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial or constanttyped.
mengj
parents:
20274
diff
changeset

169 

16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial or constanttyped.
mengj
parents:
20274
diff
changeset

170 
fun find_typ_level () = !typ_level; 
16733b31e1cf
Only ignore too general axiom clauses, if the translation is partial or constanttyped.
mengj
parents:
20274
diff
changeset

171 

17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

172 
type axiom_name = string; 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

173 
type polarity = bool; 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

174 
type clause_id = int; 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

175 

21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

176 
datatype combterm = CombConst of string * ResClause.fol_type * ResClause.fol_type list 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

177 
 CombFree of string * ResClause.fol_type 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

178 
 CombVar of string * ResClause.fol_type 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

179 
 CombApp of combterm * combterm * ResClause.fol_type 
20360  180 

17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

181 
datatype literal = Literal of polarity * combterm; 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

182 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

183 
datatype clause = 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

184 
Clause of {clause_id: clause_id, 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

185 
axiom_name: axiom_name, 
19964  186 
th: thm, 
21509
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset

187 
kind: ResClause.kind, 
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

188 
literals: literal list, 
21561  189 
ctypes_sorts: (ResClause.typ_var * Term.sort) list, 
190 
ctvar_type_literals: ResClause.type_literal list, 

191 
ctfree_type_literals: ResClause.type_literal list}; 

17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

192 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

193 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

194 
(*********************************************************************) 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

195 
(* convert a clause with type Term.term to a clause with type clause *) 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

196 
(*********************************************************************) 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

197 

21561  198 
fun isFalse (Literal(pol, CombConst(c,_,_))) = 
20360  199 
(pol andalso c = "c_False") orelse 
200 
(not pol andalso c = "c_True") 

17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

201 
 isFalse _ = false; 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

202 

21561  203 
fun isTrue (Literal (pol, CombConst(c,_,_))) = 
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

204 
(pol andalso c = "c_True") orelse 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

205 
(not pol andalso c = "c_False") 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

206 
 isTrue _ = false; 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

207 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

208 
fun isTaut (Clause {literals,...}) = exists isTrue literals; 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

209 

18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset

210 
fun type_of (Type (a, Ts)) = 
21561  211 
let val (folTypes,ts) = types_of Ts 
212 
val t = ResClause.make_fixed_type_const a 

213 
in 

21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

214 
(ResClause.mk_fol_type("Comp",t,folTypes), ts) 
21561  215 
end 
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset

216 
 type_of (tp as (TFree(a,s))) = 
21561  217 
let val t = ResClause.make_fixed_type_var a 
218 
in 

21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

219 
(ResClause.mk_fol_type("Fixed",t,[]), [ResClause.mk_typ_var_sort tp]) 
21561  220 
end 
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset

221 
 type_of (tp as (TVar(v,s))) = 
21561  222 
let val t = ResClause.make_schematic_type_var v 
223 
in 

21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

224 
(ResClause.mk_fol_type("Var",t,[]), [ResClause.mk_typ_var_sort tp]) 
21561  225 
end 
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset

226 
and types_of Ts = 
21561  227 
let val foltyps_ts = map type_of Ts 
228 
val (folTyps,ts) = ListPair.unzip foltyps_ts 

229 
in 

21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

230 
(folTyps, ResClause.union_all ts) 
21561  231 
end; 
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

232 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

233 
(* same as above, but no gathering of sort information *) 
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset

234 
fun simp_type_of (Type (a, Ts)) = 
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

235 
let val typs = map simp_type_of Ts 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

236 
val t = ResClause.make_fixed_type_const a 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

237 
in 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

238 
ResClause.mk_fol_type("Comp",t,typs) 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

239 
end 
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset

240 
 simp_type_of (TFree (a,s)) = ResClause.mk_fol_type("Fixed",ResClause.make_fixed_type_var a,[]) 
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset

241 
 simp_type_of (TVar (v,s)) = ResClause.mk_fol_type("Var",ResClause.make_schematic_type_var v,[]); 
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset

242 

18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset

243 

20865
2cfa020109c1
Changed and removed some functions related to combinators, since they are Isabelle constants now.
mengj
parents:
20864
diff
changeset

244 
fun const_type_of (c,t) = 
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset

245 
let val (tp,ts) = type_of t 
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset

246 
val tvars = !const_typargs(c,t) 
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset

247 
in 
21561  248 
(tp, ts, map simp_type_of tvars) 
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset

249 
end; 
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset

250 

17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

251 
(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *) 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

252 
fun combterm_of (Const(c,t)) = 
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

253 
let val (tp,ts,tvar_list) = const_type_of (c,t) 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

254 
val c' = CombConst(ResClause.make_fixed_const c,tp,tvar_list) 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

255 
in 
21561  256 
(c',ts) 
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

257 
end 
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

258 
 combterm_of (Free(v,t)) = 
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

259 
let val (tp,ts) = type_of t 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

260 
val v' = if ResClause.isMeta v then CombVar(ResClause.make_schematic_var(v,0),tp) 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

261 
else CombFree(ResClause.make_fixed_var v,tp) 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

262 
in 
21561  263 
(v',ts) 
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

264 
end 
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

265 
 combterm_of (Var(v,t)) = 
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

266 
let val (tp,ts) = type_of t 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

267 
val v' = CombVar(ResClause.make_schematic_var v,tp) 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

268 
in 
21561  269 
(v',ts) 
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

270 
end 
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

271 
 combterm_of (t as (P $ Q)) = 
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

272 
let val (P',tsP) = combterm_of P 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

273 
val (Q',tsQ) = combterm_of Q 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

274 
val tp = Term.type_of t 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

275 
val t' = CombApp(P',Q', simp_type_of tp) 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

276 
in 
21561  277 
(t',tsP union tsQ) 
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

278 
end; 
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

279 

21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

280 
fun predicate_of ((Const("Not",_) $ P), polarity) = predicate_of (P, not polarity) 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

281 
 predicate_of (t,polarity) = (combterm_of t, polarity); 
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

282 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

283 
fun literals_of_term1 args (Const("Trueprop",_) $ P) = literals_of_term1 args P 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

284 
 literals_of_term1 args (Const("op ",_) $ P $ Q) = 
21509
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset

285 
literals_of_term1 (literals_of_term1 args P) Q 
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

286 
 literals_of_term1 (lits,ts) P = 
21509
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset

287 
let val ((pred,ts'),pol) = predicate_of (P,true) 
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset

288 
in 
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset

289 
(Literal(pol,pred)::lits, ts union ts') 
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset

290 
end; 
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

291 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

292 
fun literals_of_term P = literals_of_term1 ([],[]) P; 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

293 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

294 
(* making axiom and conjecture clauses *) 
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

295 
fun make_clause(clause_id,axiom_name,kind,th) = 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

296 
let val (lits,ctypes_sorts) = literals_of_term (to_comb (prop_of th) []) 
18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18725
diff
changeset

297 
val (ctvar_lits,ctfree_lits) = ResClause.add_typs_aux ctypes_sorts 
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

298 
in 
20016  299 
if forall isFalse lits 
300 
then error "Problem too trivial for resolution (empty clause)" 

301 
else 

21509
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset

302 
Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind, 
20016  303 
literals = lits, ctypes_sorts = ctypes_sorts, 
304 
ctvar_type_literals = ctvar_lits, 

305 
ctfree_type_literals = ctfree_lits} 

17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

306 
end; 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

307 

20016  308 

21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

309 
fun add_axiom_clause ((th,(name,id)), pairs) = 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

310 
let val cls = make_clause(id, name, ResClause.Axiom, th) 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

311 
in 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

312 
if isTaut cls then pairs else (name,cls)::pairs 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

313 
end; 
19354  314 

21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

315 
val make_axiom_clauses = foldl add_axiom_clause []; 
19354  316 

17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

317 
fun make_conjecture_clauses_aux _ [] = [] 
20421  318 
 make_conjecture_clauses_aux n (th::ths) = 
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

319 
make_clause(n,"conjecture", ResClause.Conjecture, th) :: 
20421  320 
make_conjecture_clauses_aux (n+1) ths; 
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

321 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

322 
val make_conjecture_clauses = make_conjecture_clauses_aux 0; 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

323 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

324 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

325 
(**********************************************************************) 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

326 
(* convert clause into ATP specific formats: *) 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

327 
(* TPTP used by Vampire and E *) 
19720  328 
(* DFG used by SPASS *) 
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

329 
(**********************************************************************) 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

330 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

331 
val type_wrapper = "typeinfo"; 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

332 

21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

333 
fun wrap_type (c,tp) = case !typ_level of 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

334 
T_FULL => type_wrapper ^ ResClause.paren_pack [c, ResClause.string_of_fol_type tp] 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

335 
 _ => c; 
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset

336 

17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

337 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

338 
val bool_tp = ResClause.make_fixed_type_const "bool"; 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

339 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

340 
val app_str = "hAPP"; 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

341 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

342 
val bool_str = "hBOOL"; 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

343 

21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

344 
fun type_of_combterm (CombConst(c,tp,_)) = tp 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

345 
 type_of_combterm (CombFree(v,tp)) = tp 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

346 
 type_of_combterm (CombVar(v,tp)) = tp 
21561  347 
 type_of_combterm (CombApp(t1,t2,tp)) = tp; 
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

348 

21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

349 
fun string_of_combterm1 (CombConst(c,tp,_)) = 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

350 
let val c' = if c = "equal" then "c_fequal" else c 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

351 
in wrap_type (c',tp) end 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

352 
 string_of_combterm1 (CombFree(v,tp)) = wrap_type (v,tp) 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

353 
 string_of_combterm1 (CombVar(v,tp)) = wrap_type (v,tp) 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

354 
 string_of_combterm1 (CombApp(t1,t2,tp)) = 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

355 
let val s1 = string_of_combterm1 t1 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

356 
val s2 = string_of_combterm1 t2 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

357 
in 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

358 
case !typ_level of 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

359 
T_FULL => type_wrapper ^ 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

360 
ResClause.paren_pack 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

361 
[app_str ^ ResClause.paren_pack [s1,s2], 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

362 
ResClause.string_of_fol_type tp] 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

363 
 T_PARTIAL => app_str ^ ResClause.paren_pack 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

364 
[s1,s2, ResClause.string_of_fol_type (type_of_combterm t1)] 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

365 
 T_NONE => app_str ^ ResClause.paren_pack [s1,s2] 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

366 
 T_CONST => raise ERROR "string_of_combterm1" 
21561  367 
end; 
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset

368 

21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

369 
fun string_of_combterm2 (CombConst(c,tp,tvars)) = 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

370 
let val tvars' = map ResClause.string_of_fol_type tvars 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

371 
val c' = if c = "equal" then "c_fequal" else c 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

372 
in 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

373 
c' ^ ResClause.paren_pack tvars' 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

374 
end 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

375 
 string_of_combterm2 (CombFree(v,tp)) = v 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

376 
 string_of_combterm2 (CombVar(v,tp)) = v 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

377 
 string_of_combterm2 (CombApp(t1,t2,_)) = 
21561  378 
app_str ^ ResClause.paren_pack [string_of_combterm2 t1, string_of_combterm2 t2]; 
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset

379 

21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

380 
fun string_of_combterm t = 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

381 
case !typ_level of T_CONST => string_of_combterm2 t 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

382 
 _ => string_of_combterm1 t; 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

383 

21561  384 
fun string_of_predicate (CombApp(CombApp(CombConst("equal",_,_),t1,_),t2,_)) = 
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

385 
("equal" ^ ResClause.paren_pack [string_of_combterm t1, string_of_combterm t2]) 
21561  386 
 string_of_predicate t = 
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

387 
bool_str ^ ResClause.paren_pack [string_of_combterm t] 
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset

388 

17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

389 
fun string_of_clausename (cls_id,ax_name) = 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

390 
ResClause.clause_prefix ^ ResClause.ascii_of ax_name ^ "_" ^ Int.toString cls_id; 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

391 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

392 
fun string_of_type_clsname (cls_id,ax_name,idx) = 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

393 
string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx); 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

394 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

395 

21561  396 
(*** tptp format ***) 
19720  397 

21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

398 
fun tptp_of_equality pol (t1,t2) = 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

399 
let val eqop = if pol then " = " else " != " 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

400 
in string_of_combterm t1 ^ eqop ^ string_of_combterm t2 end; 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

401 

21561  402 
fun tptp_literal (Literal(pol, CombApp(CombApp(CombConst("equal",_,_),t1,_),t2,_))) = 
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

403 
tptp_of_equality pol (t1,t2) 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

404 
 tptp_literal (Literal(pol,pred)) = 
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

405 
ResClause.tptp_sign pol (string_of_predicate pred); 
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

406 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

407 
fun tptp_type_lits (Clause cls) = 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

408 
let val lits = map tptp_literal (#literals cls) 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

409 
val ctvar_lits_strs = 
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset

410 
case !typ_level of T_NONE => [] 
20360  411 
 _ => map ResClause.tptp_of_typeLit (#ctvar_type_literals cls) 
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

412 
val ctfree_lits = 
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset

413 
case !typ_level of T_NONE => [] 
20360  414 
 _ => map ResClause.tptp_of_typeLit (#ctfree_type_literals cls) 
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

415 
in 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

416 
(ctvar_lits_strs @ lits, ctfree_lits) 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

417 
end; 
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset

418 

443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset

419 

21509
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset

420 
fun clause2tptp (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) = 
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

421 
let val (lits,ctfree_lits) = tptp_type_lits cls 
21509
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset

422 
val cls_str = ResClause.gen_tptp_cls(clause_id,axiom_name,kind,lits) 
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

423 
in 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

424 
(cls_str,ctfree_lits) 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

425 
end; 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

426 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

427 

21561  428 
(*** dfg format ***) 
429 

21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

430 
fun dfg_literal (Literal(pol,pred)) = ResClause.dfg_sign pol (string_of_predicate pred); 
19720  431 

432 
fun dfg_clause_aux (Clause{literals, ctypes_sorts, ...}) = 

433 
let val lits = map dfg_literal literals 

434 
val (tvar_lits,tfree_lits) = ResClause.add_typs_aux ctypes_sorts 

435 
val tvar_lits_strs = 

436 
case !typ_level of T_NONE => [] 

20360  437 
 _ => map ResClause.dfg_of_typeLit tvar_lits 
19720  438 
val tfree_lits = 
439 
case !typ_level of T_NONE => [] 

20360  440 
 _ => map ResClause.dfg_of_typeLit tfree_lits 
19720  441 
in 
442 
(tvar_lits_strs @ lits, tfree_lits) 

443 
end; 

444 

445 
fun get_uvars (CombConst(_,_,_)) vars = vars 

446 
 get_uvars (CombFree(_,_)) vars = vars 

447 
 get_uvars (CombVar(v,tp)) vars = (v::vars) 

21561  448 
 get_uvars (CombApp(P,Q,tp)) vars = get_uvars P (get_uvars Q vars); 
19720  449 

450 
fun get_uvars_l (Literal(_,c)) = get_uvars c []; 

451 

452 
fun dfg_vars (Clause {literals,...}) = ResClause.union_all (map get_uvars_l literals); 

453 

454 
fun clause2dfg (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) = 

455 
let val (lits,tfree_lits) = dfg_clause_aux cls 

456 
val vars = dfg_vars cls 

457 
val tvars = ResClause.get_tvar_strs ctypes_sorts 

21509
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset

458 
val knd = ResClause.name_of_kind kind 
19720  459 
val lits_str = commas lits 
460 
val cls_str = ResClause.gen_dfg_cls(clause_id, axiom_name, knd, lits_str, tvars@vars) 

461 
in (cls_str, tfree_lits) end; 

462 

463 

464 
fun init_funcs_tab funcs = 

21561  465 
let val funcs1 = case !typ_level of T_PARTIAL => Symtab.update ("hAPP",3) funcs 
20865
2cfa020109c1
Changed and removed some functions related to combinators, since they are Isabelle constants now.
mengj
parents:
20864
diff
changeset

466 
 _ => Symtab.update ("hAPP",2) funcs 
19724  467 
in 
21561  468 
Symtab.update ("typeinfo",2) funcs1 
19724  469 
end; 
19720  470 

471 

19725
ada9bb1faba5
Changed the DFG format's functions' declaration procedure.
mengj
parents:
19724
diff
changeset

472 
fun add_funcs (CombConst(c,_,tvars),funcs) = 
21561  473 
if c = "equal" then foldl ResClause.add_foltype_funcs funcs tvars 
474 
else 

475 
(case !typ_level of 

476 
T_CONST => foldl ResClause.add_foltype_funcs (Symtab.update(c,length tvars) funcs) tvars 

477 
 _ => foldl ResClause.add_foltype_funcs (Symtab.update(c,0) funcs) tvars) 

19724  478 
 add_funcs (CombFree(v,ctp),funcs) = ResClause.add_foltype_funcs (ctp,Symtab.update (v,0) funcs) 
19720  479 
 add_funcs (CombVar(_,ctp),funcs) = ResClause.add_foltype_funcs (ctp,funcs) 
21561  480 
 add_funcs (CombApp(P,Q,_),funcs) = add_funcs(P,add_funcs (Q,funcs)); 
19720  481 

482 
fun add_literal_funcs (Literal(_,c), funcs) = add_funcs (c,funcs); 

483 

484 
fun add_clause_funcs (Clause {literals, ...}, funcs) = 

485 
foldl add_literal_funcs funcs literals 

486 
handle Symtab.DUP a => raise ERROR ("function " ^ a ^ " has multiple arities") 

487 

488 
fun funcs_of_clauses clauses arity_clauses = 

489 
Symtab.dest (foldl ResClause.add_arityClause_funcs 

490 
(foldl add_clause_funcs (init_funcs_tab Symtab.empty) clauses) 

491 
arity_clauses) 

492 

21398
11996e938dfe
Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents:
21254
diff
changeset

493 
fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) = 
11996e938dfe
Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents:
21254
diff
changeset

494 
foldl ResClause.add_type_sort_preds preds ctypes_sorts 
11996e938dfe
Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents:
21254
diff
changeset

495 
handle Symtab.DUP a => raise ERROR ("predicate " ^ a ^ " has multiple arities") 
11996e938dfe
Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents:
21254
diff
changeset

496 

11996e938dfe
Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents:
21254
diff
changeset

497 
(*Higherorder clauses have only the predicates hBOOL and type classes.*) 
11996e938dfe
Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents:
21254
diff
changeset

498 
fun preds_of_clauses clauses clsrel_clauses arity_clauses = 
19720  499 
Symtab.dest 
500 
(foldl ResClause.add_classrelClause_preds 

501 
(foldl ResClause.add_arityClause_preds 

21398
11996e938dfe
Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents:
21254
diff
changeset

502 
(Symtab.update ("hBOOL",1) 
11996e938dfe
Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents:
21254
diff
changeset

503 
(foldl add_clause_preds Symtab.empty clauses)) 
19720  504 
arity_clauses) 
505 
clsrel_clauses) 

506 

18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset

507 

21398
11996e938dfe
Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents:
21254
diff
changeset

508 

18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset

509 
(**********************************************************************) 
19198
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset

510 
(* write clauses to files *) 
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset

511 
(**********************************************************************) 
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset

512 

21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

513 

8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

514 
val init_counters = 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

515 
Symtab.make [("c_COMBI", 0), ("c_COMBK", 0), 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

516 
("c_COMBB", 0), ("c_COMBC", 0), 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

517 
("c_COMBS", 0), ("c_COMBB_e", 0), 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

518 
("c_COMBC_e", 0), ("c_COMBS_e", 0)]; 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

519 

8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

520 
fun count_combterm (CombConst(c,tp,_), ct) = 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

521 
(case Symtab.lookup ct c of NONE => ct (*no counter*) 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

522 
 SOME n => Symtab.update (c,n+1) ct) 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

523 
 count_combterm (CombFree(v,tp), ct) = ct 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

524 
 count_combterm (CombVar(v,tp), ct) = ct 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

525 
 count_combterm (CombApp(t1,t2,tp), ct) = count_combterm(t1, count_combterm(t2, ct)); 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

526 

8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

527 
fun count_literal (Literal(_,t), ct) = count_combterm(t,ct); 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

528 

8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

529 
fun count_clause (Clause{literals,...}, ct) = foldl count_literal ct literals; 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

530 

8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

531 
fun count_user_clause user_lemmas (Clause{axiom_name,literals,...}, ct) = 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

532 
if axiom_name mem_string user_lemmas then foldl count_literal ct literals 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

533 
else ct; 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

534 

20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset

535 
val cnf_helper_thms = ResAxioms.cnf_rules_pairs o (map ResAxioms.pairname) 
20644  536 

21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

537 
fun get_helper_clauses ct = 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

538 
let fun needed c = valOf (Symtab.lookup ct c) > 0 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

539 
val IK = if needed "c_COMBI" orelse needed "c_COMBK" 
21135  540 
then (Output.debug "Include combinator I K"; cnf_helper_thms [comb_I,comb_K]) 
541 
else [] 

21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

542 
val BC = if needed "c_COMBB" orelse needed "c_COMBC" 
21135  543 
then (Output.debug "Include combinator B C"; cnf_helper_thms [comb_B,comb_C]) 
544 
else [] 

21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

545 
val S = if needed "c_COMBS" 
21135  546 
then (Output.debug "Include combinator S"; cnf_helper_thms [comb_S]) 
547 
else [] 

21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

548 
val B'C' = if needed "c_COMBB_e" orelse needed "c_COMBC_e" 
21135  549 
then (Output.debug "Include combinator B' C'"; cnf_helper_thms [comb_B', comb_C']) 
550 
else [] 

21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

551 
val S' = if needed "c_COMBS_e" 
21135  552 
then (Output.debug "Include combinator S'"; cnf_helper_thms [comb_S']) 
553 
else [] 

20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset

554 
val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal] 
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset

555 
in 
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

556 
make_axiom_clauses (other @ IK @ BC @ S @ B'C' @ S') 
20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset

557 
end 
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset

558 

497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset

559 
(* tptp format *) 
19491
cd6c71c57f53
changed the functions for getting HOL helper clauses.
mengj
parents:
19452
diff
changeset

560 

19198
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset

561 
(* write TPTP format to a single file *) 
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

562 
fun tptp_write_file thms filename (axclauses,classrel_clauses,arity_clauses) user_lemmas = 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

563 
let val conjectures = make_conjecture_clauses thms 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

564 
val (clnames,axclauses') = ListPair.unzip (make_axiom_clauses axclauses) 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

565 
val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp conjectures) 
19198
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset

566 
val tfree_clss = map ResClause.tptp_tfree_clause (foldl (op union_string) [] tfree_litss) 
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset

567 
val out = TextIO.openOut filename 
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

568 
val ct = foldl (count_user_clause user_lemmas) 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

569 
(foldl count_clause init_counters conjectures) 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

570 
axclauses' 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

571 
val helper_clauses = map #2 (get_helper_clauses ct) 
19198
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset

572 
in 
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset

573 
List.app (curry TextIO.output out o #1 o clause2tptp) axclauses'; 
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset

574 
ResClause.writeln_strs out tfree_clss; 
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset

575 
ResClause.writeln_strs out tptp_clss; 
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset

576 
List.app (curry TextIO.output out o ResClause.tptp_classrelClause) classrel_clauses; 
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset

577 
List.app (curry TextIO.output out o ResClause.tptp_arity_clause) arity_clauses; 
20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset

578 
List.app (curry TextIO.output out o #1 o clause2tptp) helper_clauses; 
20022  579 
TextIO.closeOut out; 
580 
clnames 

19198
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset

581 
end; 
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset

582 

19720  583 

20644  584 

19720  585 
(* dfg format *) 
586 

20130
5303e5928285
Only include combinators if required by goals and user specified lemmas.
mengj
parents:
20125
diff
changeset

587 
fun dfg_write_file thms filename (axclauses,classrel_clauses,arity_clauses) user_lemmas = 
19720  588 
let val _ = Output.debug ("Preparing to write the DFG file " ^ filename) 
589 
val conjectures = make_conjecture_clauses thms 

21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

590 
val (clnames,axclauses') = ListPair.unzip (make_axiom_clauses axclauses) 
19720  591 
val (dfg_clss,tfree_litss) = ListPair.unzip (map clause2dfg conjectures) 
592 
and probname = Path.pack (Path.base (Path.unpack filename)) 

21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

593 
val axstrs = map (#1 o clause2dfg) axclauses' 
19720  594 
val tfree_clss = map ResClause.dfg_tfree_clause (ResClause.union_all tfree_litss) 
595 
val out = TextIO.openOut filename 

21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

596 
val ct = foldl (count_user_clause user_lemmas) 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

597 
(foldl count_clause init_counters conjectures) 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

598 
axclauses' 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

599 
val helper_clauses = map #2 (get_helper_clauses ct) 
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset

600 
val helper_clauses_strs = map (#1 o clause2dfg) helper_clauses 
20864
bb75b876b260
Now the DFG output includes correct declarations of c_fequal, but not hEXTENT
paulson
parents:
20791
diff
changeset

601 
val funcs = funcs_of_clauses (helper_clauses @ conjectures @ axclauses') arity_clauses 
21398
11996e938dfe
Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents:
21254
diff
changeset

602 
and preds = preds_of_clauses axclauses' classrel_clauses arity_clauses 
19720  603 
in 
604 
TextIO.output (out, ResClause.string_of_start probname); 

605 
TextIO.output (out, ResClause.string_of_descrip probname); 

606 
TextIO.output (out, ResClause.string_of_symbols (ResClause.string_of_funcs funcs) (ResClause.string_of_preds preds)); 

607 
TextIO.output (out, "list_of_clauses(axioms,cnf).\n"); 

608 
ResClause.writeln_strs out axstrs; 

609 
List.app (curry TextIO.output out o ResClause.dfg_classrelClause) classrel_clauses; 

610 
List.app (curry TextIO.output out o ResClause.dfg_arity_clause) arity_clauses; 

20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset

611 
ResClause.writeln_strs out helper_clauses_strs; 
19720  612 
TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"); 
613 
ResClause.writeln_strs out tfree_clss; 

614 
ResClause.writeln_strs out dfg_clss; 

20953
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset

615 
TextIO.output (out, "end_of_list.\n\n"); 
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset

616 
(*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*) 
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset

617 
TextIO.output (out, "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n"); 
1ea394dc2a0f
Combinators require the theory name; added settings for SPASS
paulson
parents:
20865
diff
changeset

618 
TextIO.output (out, "end_problem.\n"); 
20022  619 
TextIO.closeOut out; 
620 
clnames 

19720  621 
end; 
622 

21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21135
diff
changeset

623 
end 