author  paulson 
Tue, 21 Aug 2007 18:27:14 +0200  
changeset 24385  ab62948281a9 
parent 24323  9aa7b5708eac 
child 24937  340523598914 
permissions  rwrr 
24311  1 
(* ID: $Id$ 
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

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 

24311  4 
FOL clauses translated from HOL formulae. 
22825
bd774e01d6d5
Fixing bugs in the partialtyped and fullytyped translations
paulson
parents:
22130
diff
changeset

5 

bd774e01d6d5
Fixing bugs in the partialtyped and fullytyped translations
paulson
parents:
22130
diff
changeset

6 
The combinator code needs to be deleted after the translation paper has been published. 
bd774e01d6d5
Fixing bugs in the partialtyped and fullytyped translations
paulson
parents:
22130
diff
changeset

7 
It cannot be used with proof reconstruction because combinators are not introduced by proof. 
bd774e01d6d5
Fixing bugs in the partialtyped and fullytyped translations
paulson
parents:
22130
diff
changeset

8 
The Turner combinators (B', C', S') yield no improvement and should be deleted. 
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

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

10 

24311  11 
signature RES_HOL_CLAUSE = 
12 
sig 

13 
val ext: thm 

14 
val comb_I: thm 

15 
val comb_K: thm 

16 
val comb_B: thm 

17 
val comb_C: thm 

18 
val comb_S: thm 

24385
ab62948281a9
Deleted the partiallytyped translation and the combinator code.
paulson
parents:
24323
diff
changeset

19 
datatype type_level = T_FULL  T_CONST 
24311  20 
val typ_level: type_level ref 
21 
val minimize_applies: bool ref 

22 
type axiom_name = string 

23 
type polarity = bool 

24 
type clause_id = int 

25 
datatype combterm = 

26 
CombConst of string * ResClause.fol_type * ResClause.fol_type list (*Const and Free*) 

27 
 CombVar of string * ResClause.fol_type 

28 
 CombApp of combterm * combterm 

29 
datatype literal = Literal of polarity * combterm 

30 
val strip_comb: combterm > combterm * combterm list 

24323
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

31 
val literals_of_term: theory > term > literal list * (ResClause.typ_var * sort) list 
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

32 
val tptp_write_file: theory > bool > thm list > string > 
24311  33 
(thm * (axiom_name * clause_id)) list * ResClause.classrelClause list * 
34 
ResClause.arityClause list > string list > axiom_name list 

24323
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

35 
val dfg_write_file: theory > bool > thm list > string > 
24311  36 
(thm * (axiom_name * clause_id)) list * ResClause.classrelClause list * 
37 
ResClause.arityClause list > string list > axiom_name list 

38 
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

39 

24311  40 
structure ResHolClause: RES_HOL_CLAUSE = 
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

41 
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

42 

22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

43 
structure RC = ResClause; 
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

44 

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

45 
(* 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

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

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

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

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

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

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

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

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

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

55 
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

56 
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

57 

22825
bd774e01d6d5
Fixing bugs in the partialtyped and fullytyped translations
paulson
parents:
22130
diff
changeset

58 

bd774e01d6d5
Fixing bugs in the partialtyped and fullytyped translations
paulson
parents:
22130
diff
changeset

59 
(*The different translations of types*) 
24385
ab62948281a9
Deleted the partiallytyped translation and the combinator code.
paulson
parents:
24323
diff
changeset

60 
datatype type_level = T_FULL  T_CONST; 
22825
bd774e01d6d5
Fixing bugs in the partialtyped and fullytyped translations
paulson
parents:
22130
diff
changeset

61 

bd774e01d6d5
Fixing bugs in the partialtyped and fullytyped translations
paulson
parents:
22130
diff
changeset

62 
val typ_level = ref T_CONST; 
bd774e01d6d5
Fixing bugs in the partialtyped and fullytyped translations
paulson
parents:
22130
diff
changeset

63 

22064  64 
(*If true, each function will be directly applied to as many arguments as possible, avoiding 
24385
ab62948281a9
Deleted the partiallytyped translation and the combinator code.
paulson
parents:
24323
diff
changeset

65 
use of the "apply" operator. Use of hBOOL is also minimized.*) 
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

66 
val minimize_applies = ref true; 
22064  67 

68 
val const_min_arity = ref (Symtab.empty : int Symtab.table); 

69 

70 
val const_needs_hBOOL = ref (Symtab.empty : bool Symtab.table); 

71 

72 
fun min_arity_of c = getOpt (Symtab.lookup(!const_min_arity) c, 0); 

73 

22825
bd774e01d6d5
Fixing bugs in the partialtyped and fullytyped translations
paulson
parents:
22130
diff
changeset

74 
(*True if the constant ever appears outside of the toplevel position in literals. 
bd774e01d6d5
Fixing bugs in the partialtyped and fullytyped translations
paulson
parents:
22130
diff
changeset

75 
If false, the constant always receives all of its arguments and is used as a predicate.*) 
24385
ab62948281a9
Deleted the partiallytyped translation and the combinator code.
paulson
parents:
24323
diff
changeset

76 
fun needs_hBOOL c = not (!minimize_applies) orelse 
22064  77 
getOpt (Symtab.lookup(!const_needs_hBOOL) c, false); 
78 

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

79 

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

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

81 
(* 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

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

83 

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

84 
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

85 
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

86 
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

87 

23386  88 
datatype combterm = CombConst of string * RC.fol_type * RC.fol_type list (*Const and Free*) 
24311  89 
 CombVar of string * RC.fol_type 
90 
 CombApp of combterm * combterm 

91 

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

92 
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

93 

24311  94 
datatype clause = 
95 
Clause of {clause_id: clause_id, 

96 
axiom_name: axiom_name, 

97 
th: thm, 

98 
kind: RC.kind, 

99 
literals: literal list, 

100 
ctypes_sorts: (RC.typ_var * Term.sort) list, 

101 
ctvar_type_literals: RC.type_literal list, 

22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

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

103 

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

104 

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

106 
(* 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

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

108 

21561  109 
fun isFalse (Literal(pol, CombConst(c,_,_))) = 
20360  110 
(pol andalso c = "c_False") orelse 
111 
(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

112 
 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

113 

21561  114 
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

115 
(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

116 
(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

117 
 isTrue _ = false; 
24311  118 

119 
fun isTaut (Clause {literals,...}) = exists isTrue literals; 

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

120 

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

121 
fun type_of (Type (a, Ts)) = 
21561  122 
let val (folTypes,ts) = types_of Ts 
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

123 
in (RC.Comp(RC.make_fixed_type_const a, folTypes), ts) end 
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset

124 
 type_of (tp as (TFree(a,s))) = 
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

125 
(RC.AtomF (RC.make_fixed_type_var a), [RC.mk_typ_var_sort tp]) 
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset

126 
 type_of (tp as (TVar(v,s))) = 
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

127 
(RC.AtomV (RC.make_schematic_type_var v), [RC.mk_typ_var_sort tp]) 
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset

128 
and types_of Ts = 
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

129 
let val (folTyps,ts) = ListPair.unzip (map type_of Ts) 
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

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

131 

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

132 
(* same as above, but no gathering of sort information *) 
24311  133 
fun simp_type_of (Type (a, Ts)) = 
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

134 
RC.Comp(RC.make_fixed_type_const a, map simp_type_of Ts) 
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

135 
 simp_type_of (TFree (a,s)) = RC.AtomF(RC.make_fixed_type_var a) 
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

136 
 simp_type_of (TVar (v,s)) = RC.AtomV(RC.make_schematic_type_var v); 
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset

137 

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

138 

24323
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

139 
fun const_type_of thy (c,t) = 
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

140 
let val (tp,ts) = type_of t 
24323
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

141 
in (tp, ts, map simp_type_of (Sign.const_typargs thy (c,t))) end; 
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset

142 

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

143 
(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *) 
24323
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

144 
fun combterm_of thy (Const(c,t)) = 
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

145 
let val (tp,ts,tvar_list) = const_type_of thy (c,t) 
24311  146 
val c' = CombConst(RC.make_fixed_const c, tp, tvar_list) 
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

147 
in (c',ts) end 
24323
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

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

149 
let val (tp,ts) = type_of t 
24311  150 
val v' = if RC.isMeta v then CombVar(RC.make_schematic_var(v,0),tp) 
151 
else CombConst(RC.make_fixed_var v, tp, []) 

22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

152 
in (v',ts) end 
24323
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

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

154 
let val (tp,ts) = type_of t 
24311  155 
val v' = CombVar(RC.make_schematic_var v,tp) 
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

156 
in (v',ts) end 
24385
ab62948281a9
Deleted the partiallytyped translation and the combinator code.
paulson
parents:
24323
diff
changeset

157 
 combterm_of thy (P $ Q) = 
24323
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

158 
let val (P',tsP) = combterm_of thy P 
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

159 
val (Q',tsQ) = combterm_of thy Q 
24385
ab62948281a9
Deleted the partiallytyped translation and the combinator code.
paulson
parents:
24323
diff
changeset

160 
in (CombApp(P',Q'), tsP union tsQ) end 
ab62948281a9
Deleted the partiallytyped translation and the combinator code.
paulson
parents:
24323
diff
changeset

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

162 

24323
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

163 
fun predicate_of thy ((Const("Not",_) $ P), polarity) = predicate_of thy (P, not polarity) 
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

164 
 predicate_of thy (t,polarity) = (combterm_of thy 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

165 

24323
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

166 
fun literals_of_term1 thy args (Const("Trueprop",_) $ P) = literals_of_term1 thy args P 
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

167 
 literals_of_term1 thy args (Const("op ",_) $ P $ Q) = 
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

168 
literals_of_term1 thy (literals_of_term1 thy args P) Q 
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

169 
 literals_of_term1 thy (lits,ts) P = 
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

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

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

173 
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

174 

24323
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

175 
fun literals_of_term thy P = literals_of_term1 thy ([],[]) P; 
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

176 

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

177 
(* making axiom and conjecture clauses *) 
24323
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

178 
fun make_clause thy (clause_id,axiom_name,kind,th) = 
24385
ab62948281a9
Deleted the partiallytyped translation and the combinator code.
paulson
parents:
24323
diff
changeset

179 
let val (lits,ctypes_sorts) = literals_of_term thy (prop_of th) 
24311  180 
val (ctvar_lits,ctfree_lits) = RC.add_typs_aux ctypes_sorts 
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset

181 
in 
24311  182 
if forall isFalse lits 
183 
then error "Problem too trivial for resolution (empty clause)" 

184 
else 

185 
Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind, 

186 
literals = lits, ctypes_sorts = ctypes_sorts, 

187 
ctvar_type_literals = ctvar_lits, 

188 
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

189 
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

190 

20016  191 

24323
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

192 
fun add_axiom_clause thy ((th,(name,id)), pairs) = 
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

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

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

195 
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

196 
end; 
19354  197 

24323
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

198 
fun make_axiom_clauses thy = foldl (add_axiom_clause thy) []; 
19354  199 

24323
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

200 
fun make_conjecture_clauses_aux _ _ [] = [] 
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

201 
 make_conjecture_clauses_aux thy n (th::ths) = 
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

202 
make_clause thy (n,"conjecture", RC.Conjecture, th) :: 
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

203 
make_conjecture_clauses_aux thy (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

204 

24323
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

205 
fun make_conjecture_clauses thy = make_conjecture_clauses_aux thy 0; 
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

206 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. 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 
(**********************************************************************) 
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. 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 
(* 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

210 
(* TPTP used by Vampire and E *) 
19720  211 
(* 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

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

213 

22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

214 
(*Result of a function type; no need to check that the argument type matches.*) 
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

215 
fun result_type (RC.Comp ("tc_fun", [_, tp2])) = tp2 
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

216 
 result_type _ = raise ERROR "result_type" 
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

217 

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

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

219 
 type_of_combterm (CombVar(v,tp)) = tp 
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

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

221 

22064  222 
(*gets the head of a combinator application, along with the list of arguments*) 
223 
fun strip_comb u = 

22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

224 
let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts) 
22064  225 
 stripc x = x 
226 
in stripc(u,[]) end; 

227 

22851
7b7d6e1c70b6
Firstorder variant of the fullytyped translation
paulson
parents:
22825
diff
changeset

228 
val type_wrapper = "ti"; 
7b7d6e1c70b6
Firstorder variant of the fullytyped translation
paulson
parents:
22825
diff
changeset

229 

7b7d6e1c70b6
Firstorder variant of the fullytyped translation
paulson
parents:
22825
diff
changeset

230 
fun head_needs_hBOOL (CombConst(c,_,_)) = needs_hBOOL c 
7b7d6e1c70b6
Firstorder variant of the fullytyped translation
paulson
parents:
22825
diff
changeset

231 
 head_needs_hBOOL _ = true; 
7b7d6e1c70b6
Firstorder variant of the fullytyped translation
paulson
parents:
22825
diff
changeset

232 

24311  233 
fun wrap_type (s, tp) = 
22851
7b7d6e1c70b6
Firstorder variant of the fullytyped translation
paulson
parents:
22825
diff
changeset

234 
if !typ_level=T_FULL then 
7b7d6e1c70b6
Firstorder variant of the fullytyped translation
paulson
parents:
22825
diff
changeset

235 
type_wrapper ^ RC.paren_pack [s, RC.string_of_fol_type tp] 
7b7d6e1c70b6
Firstorder variant of the fullytyped translation
paulson
parents:
22825
diff
changeset

236 
else s; 
24311  237 

22851
7b7d6e1c70b6
Firstorder variant of the fullytyped translation
paulson
parents:
22825
diff
changeset

238 
fun apply ss = "hAPP" ^ RC.paren_pack ss; 
7b7d6e1c70b6
Firstorder variant of the fullytyped translation
paulson
parents:
22825
diff
changeset

239 

22064  240 
fun rev_apply (v, []) = v 
22851
7b7d6e1c70b6
Firstorder variant of the fullytyped translation
paulson
parents:
22825
diff
changeset

241 
 rev_apply (v, arg::args) = apply [rev_apply (v, args), arg]; 
22064  242 

243 
fun string_apply (v, args) = rev_apply (v, rev args); 

244 

245 
(*Apply an operator to the argument strings, using either the "apply" operator or 

246 
direct function application.*) 

22851
7b7d6e1c70b6
Firstorder variant of the fullytyped translation
paulson
parents:
22825
diff
changeset

247 
fun string_of_applic (CombConst(c,tp,tvars), args) = 
22064  248 
let val c = if c = "equal" then "c_fequal" else c 
249 
val nargs = min_arity_of c 

22851
7b7d6e1c70b6
Firstorder variant of the fullytyped translation
paulson
parents:
22825
diff
changeset

250 
val args1 = List.take(args, nargs) 
22064  251 
handle Subscript => raise ERROR ("string_of_applic: " ^ c ^ " has arity " ^ 
24311  252 
Int.toString nargs ^ " but is applied to " ^ 
253 
space_implode ", " args) 

22064  254 
val args2 = List.drop(args, nargs) 
22851
7b7d6e1c70b6
Firstorder variant of the fullytyped translation
paulson
parents:
22825
diff
changeset

255 
val targs = if !typ_level = T_CONST then map RC.string_of_fol_type tvars 
7b7d6e1c70b6
Firstorder variant of the fullytyped translation
paulson
parents:
22825
diff
changeset

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

257 
in 
24311  258 
string_apply (c ^ RC.paren_pack (args1@targs), args2) 
21513
9e9fff87dc6c
Conversion of "equal" to "=" for TSTP format; big tidyup
paulson
parents:
21509
diff
changeset

259 
end 
22851
7b7d6e1c70b6
Firstorder variant of the fullytyped translation
paulson
parents:
22825
diff
changeset

260 
 string_of_applic (CombVar(v,tp), args) = string_apply (v, args) 
22064  261 
 string_of_applic _ = raise ERROR "string_of_applic"; 
262 

22851
7b7d6e1c70b6
Firstorder variant of the fullytyped translation
paulson
parents:
22825
diff
changeset

263 
fun wrap_type_if (head, s, tp) = if head_needs_hBOOL head then wrap_type (s, tp) else s; 
24311  264 

24385
ab62948281a9
Deleted the partiallytyped translation and the combinator code.
paulson
parents:
24323
diff
changeset

265 
fun string_of_combterm t = 
22064  266 
let val (head, args) = strip_comb t 
24311  267 
in wrap_type_if (head, 
24385
ab62948281a9
Deleted the partiallytyped translation and the combinator code.
paulson
parents:
24323
diff
changeset

268 
string_of_applic (head, map string_of_combterm args), 
22851
7b7d6e1c70b6
Firstorder variant of the fullytyped translation
paulson
parents:
22825
diff
changeset

269 
type_of_combterm t) 
7b7d6e1c70b6
Firstorder variant of the fullytyped translation
paulson
parents:
22825
diff
changeset

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

271 

22064  272 
(*Booleanvalued terms are here converted to literals.*) 
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

273 
fun boolify t = "hBOOL" ^ RC.paren_pack [string_of_combterm t]; 
22064  274 

24311  275 
fun string_of_predicate t = 
22064  276 
case t of 
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

277 
(CombApp(CombApp(CombConst("equal",_,_), t1), t2)) => 
24311  278 
(*DFG only: new TPTP prefers infix equality*) 
279 
("equal" ^ RC.paren_pack [string_of_combterm t1, string_of_combterm t2]) 

280 
 _ => 

22064  281 
case #1 (strip_comb t) of 
282 
CombConst(c,_,_) => if needs_hBOOL c then boolify t else string_of_combterm t 

283 
 _ => boolify t; 

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

284 

24311  285 
fun string_of_clausename (cls_id,ax_name) = 
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

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

287 

24311  288 
fun string_of_type_clsname (cls_id,ax_name,idx) = 
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

289 
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

290 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. 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 

21561  292 
(*** tptp format ***) 
19720  293 

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

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

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

296 
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

297 

24311  298 
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

299 
tptp_of_equality pol (t1,t2) 
24311  300 
 tptp_literal (Literal(pol,pred)) = 
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

301 
RC.tptp_sign pol (string_of_predicate pred); 
24311  302 

22064  303 
(*Given a clause, returns its literals paired with a list of literals concerning TFrees; 
304 
the latter should only occur in conjecture clauses.*) 

24311  305 
fun tptp_type_lits (Clause 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

306 
let val lits = map tptp_literal (#literals cls) 
24311  307 
val ctvar_lits_strs = map RC.tptp_of_typeLit (#ctvar_type_literals cls) 
308 
val ctfree_lits = map RC.tptp_of_typeLit (#ctfree_type_literals cls) 

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

309 
in 
24311  310 
(ctvar_lits_strs @ lits, ctfree_lits) 
311 
end; 

312 

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

313 
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

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

316 
in 
24311  317 
(cls_str,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

318 
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

319 

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

320 

21561  321 
(*** dfg format ***) 
322 

22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

323 
fun dfg_literal (Literal(pol,pred)) = RC.dfg_sign pol (string_of_predicate pred); 
19720  324 

24311  325 
fun dfg_clause_aux (Clause{literals, ctypes_sorts, ...}) = 
19720  326 
let val lits = map dfg_literal literals 
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

327 
val (tvar_lits,tfree_lits) = RC.add_typs_aux ctypes_sorts 
22825
bd774e01d6d5
Fixing bugs in the partialtyped and fullytyped translations
paulson
parents:
22130
diff
changeset

328 
val tvar_lits_strs = map RC.dfg_of_typeLit tvar_lits 
24311  329 
val tfree_lits = map RC.dfg_of_typeLit tfree_lits 
19720  330 
in 
331 
(tvar_lits_strs @ lits, tfree_lits) 

24311  332 
end; 
19720  333 

22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

334 
fun get_uvars (CombConst _) vars = vars 
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

335 
 get_uvars (CombVar(v,_)) vars = (v::vars) 
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

336 
 get_uvars (CombApp(P,Q)) vars = get_uvars P (get_uvars Q vars); 
19720  337 

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

339 

22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

340 
fun dfg_vars (Clause {literals,...}) = RC.union_all (map get_uvars_l literals); 
24311  341 

19720  342 
fun clause2dfg (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) = 
24311  343 
let val (lits,tfree_lits) = dfg_clause_aux cls 
19720  344 
val vars = dfg_vars cls 
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

345 
val tvars = RC.get_tvar_strs ctypes_sorts 
24311  346 
val knd = RC.name_of_kind kind 
347 
val lits_str = commas lits 

348 
val cls_str = RC.gen_dfg_cls(clause_id, axiom_name, knd, lits_str, tvars@vars) 

19720  349 
in (cls_str, tfree_lits) end; 
350 

22064  351 
(** For DFG format: accumulate function and predicate declarations **) 
19720  352 

22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

353 
fun addtypes tvars tab = foldl RC.add_foltype_funcs tab tvars; 
19720  354 

22825
bd774e01d6d5
Fixing bugs in the partialtyped and fullytyped translations
paulson
parents:
22130
diff
changeset

355 
fun add_decls (CombConst(c,tp,tvars), (funcs,preds)) = 
22064  356 
if c = "equal" then (addtypes tvars funcs, preds) 
21561  357 
else 
24385
ab62948281a9
Deleted the partiallytyped translation and the combinator code.
paulson
parents:
24323
diff
changeset

358 
let val arity = min_arity_of c 
ab62948281a9
Deleted the partiallytyped translation and the combinator code.
paulson
parents:
24323
diff
changeset

359 
val ntys = if !typ_level = T_CONST then length tvars else 0 
ab62948281a9
Deleted the partiallytyped translation and the combinator code.
paulson
parents:
24323
diff
changeset

360 
val addit = Symtab.update(c, arity+ntys) 
ab62948281a9
Deleted the partiallytyped translation and the combinator code.
paulson
parents:
24323
diff
changeset

361 
in 
ab62948281a9
Deleted the partiallytyped translation and the combinator code.
paulson
parents:
24323
diff
changeset

362 
if needs_hBOOL c then (addtypes tvars (addit funcs), preds) 
ab62948281a9
Deleted the partiallytyped translation and the combinator code.
paulson
parents:
24323
diff
changeset

363 
else (addtypes tvars funcs, addit preds) 
ab62948281a9
Deleted the partiallytyped translation and the combinator code.
paulson
parents:
24323
diff
changeset

364 
end 
24311  365 
 add_decls (CombVar(_,ctp), (funcs,preds)) = 
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

366 
(RC.add_foltype_funcs (ctp,funcs), preds) 
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

367 
 add_decls (CombApp(P,Q),decls) = add_decls(P,add_decls (Q,decls)); 
19720  368 

22064  369 
fun add_literal_decls (Literal(_,c), decls) = add_decls (c,decls); 
19720  370 

22064  371 
fun add_clause_decls (Clause {literals, ...}, decls) = 
372 
foldl add_literal_decls decls literals 

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

22064  375 
fun decls_of_clauses clauses arity_clauses = 
24385
ab62948281a9
Deleted the partiallytyped translation and the combinator code.
paulson
parents:
24323
diff
changeset

376 
let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) RC.init_functab) 
22064  377 
val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty 
378 
val (functab,predtab) = (foldl add_clause_decls (init_functab, init_predtab) clauses) 

379 
in 

24311  380 
(Symtab.dest (foldl RC.add_arityClause_funcs functab arity_clauses), 
22064  381 
Symtab.dest predtab) 
382 
end; 

19720  383 

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

384 
fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) = 
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

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

386 
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

387 

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

388 
(*Higherorder clauses have only the predicates hBOOL and type classes.*) 
24311  389 
fun preds_of_clauses clauses clsrel_clauses arity_clauses = 
19720  390 
Symtab.dest 
24311  391 
(foldl RC.add_classrelClause_preds 
392 
(foldl RC.add_arityClause_preds 

393 
(foldl add_clause_preds Symtab.empty clauses) 

394 
arity_clauses) 

395 
clsrel_clauses) 

19720  396 

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

397 

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

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

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

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

401 

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

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

403 
Symtab.make [("c_COMBI", 0), ("c_COMBK", 0), 
24311  404 
("c_COMBB", 0), ("c_COMBC", 0), 
405 
("c_COMBS", 0), ("c_COMBB_e", 0), 

406 
("c_COMBC_e", 0), ("c_COMBS_e", 0)]; 

407 

408 
fun count_combterm (CombConst(c,tp,_), ct) = 

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

409 
(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

410 
 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

411 
 count_combterm (CombVar(v,tp), ct) = ct 
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset

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

413 

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

414 
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

415 

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

416 
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

417 

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

419 
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

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

421 

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

422 
val cnf_helper_thms = ResAxioms.cnf_rules_pairs o (map ResAxioms.pairname) 
20644  423 

24323
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

424 
fun get_helper_clauses thy isFO (conjectures, axclauses, user_lemmas) = 
23386  425 
if isFO then [] (*firstorder*) 
426 
else 

22064  427 
let val ct0 = foldl count_clause init_counters conjectures 
428 
val ct = foldl (count_user_clause user_lemmas) ct0 axclauses 

429 
fun needed c = valOf (Symtab.lookup ct c) > 0 

24311  430 
val IK = if needed "c_COMBI" orelse needed "c_COMBK" 
431 
then (Output.debug (fn () => "Include combinator I K"); cnf_helper_thms [comb_I,comb_K]) 

432 
else [] 

433 
val BC = if needed "c_COMBB" orelse needed "c_COMBC" 

434 
then (Output.debug (fn () => "Include combinator B C"); cnf_helper_thms [comb_B,comb_C]) 

21135  435 
else [] 
24311  436 
val S = if needed "c_COMBS" 
437 
then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms [comb_S]) 

438 
else [] 

439 
val B'C' = if needed "c_COMBB_e" orelse needed "c_COMBC_e" 

440 
then (Output.debug (fn () => "Include combinator B' C'"); cnf_helper_thms [comb_B', comb_C']) 

441 
else [] 

442 
val S' = if needed "c_COMBS_e" 

443 
then (Output.debug (fn () => "Include combinator S'"); cnf_helper_thms [comb_S']) 

444 
else [] 

445 
val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal] 

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

446 
in 
24323
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

447 
map #2 (make_axiom_clauses thy (other @ IK @ BC @ S @ B'C' @ S')) 
23386  448 
end; 
20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset

449 

22064  450 
(*Find the minimal arity of each function mentioned in the term. Also, note which uses 
451 
are not at top level, to see if hBOOL is needed.*) 

452 
fun count_constants_term toplev t = 

453 
let val (head, args) = strip_comb t 

454 
val n = length args 

455 
val _ = List.app (count_constants_term false) args 

456 
in 

457 
case head of 

24311  458 
CombConst (a,_,_) => (*predicate or function version of "equal"?*) 
459 
let val a = if a="equal" andalso not toplev then "c_fequal" else a 

460 
in 

461 
const_min_arity := Symtab.map_default (a,n) (curry Int.min n) (!const_min_arity); 

462 
if toplev then () 

463 
else const_needs_hBOOL := Symtab.update (a,true) (!const_needs_hBOOL) 

464 
end 

465 
 ts => () 

22064  466 
end; 
467 

468 
(*A literal is a toplevel term*) 

469 
fun count_constants_lit (Literal (_,t)) = count_constants_term true t; 

470 

471 
fun count_constants_clause (Clause{literals,...}) = List.app count_constants_lit literals; 

472 

473 
fun display_arity (c,n) = 

24311  474 
Output.debug (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^ 
22064  475 
(if needs_hBOOL c then " needs hBOOL" else "")); 
476 

24311  477 
fun count_constants (conjectures, axclauses, helper_clauses) = 
24385
ab62948281a9
Deleted the partiallytyped translation and the combinator code.
paulson
parents:
24323
diff
changeset

478 
if !minimize_applies then 
24311  479 
(const_min_arity := Symtab.empty; 
23386  480 
const_needs_hBOOL := Symtab.empty; 
481 
List.app count_constants_clause conjectures; 

22064  482 
List.app count_constants_clause axclauses; 
483 
List.app count_constants_clause helper_clauses; 

484 
List.app display_arity (Symtab.dest (!const_min_arity))) 

485 
else (); 

486 

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

487 
(* tptp format *) 
24311  488 

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

489 
(* write TPTP format to a single file *) 
24323
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

490 
fun tptp_write_file thy isFO thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas = 
23386  491 
let val _ = Output.debug (fn () => ("Preparing to write the TPTP file " ^ filename)) 
492 
val _ = RC.dfg_format := false 

24323
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

493 
val conjectures = make_conjecture_clauses thy thms 
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

494 
val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses thy ax_tuples) 
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

495 
val helper_clauses = get_helper_clauses thy isFO (conjectures, axclauses, user_lemmas) 
24311  496 
val _ = count_constants (conjectures, axclauses, helper_clauses); 
497 
val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp conjectures) 

498 
val tfree_clss = map RC.tptp_tfree_clause (foldl (op union_string) [] tfree_litss) 

22064  499 
val out = TextIO.openOut filename 
19198
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset

500 
in 
24311  501 
List.app (curry TextIO.output out o #1 o clause2tptp) axclauses; 
502 
RC.writeln_strs out tfree_clss; 

503 
RC.writeln_strs out tptp_clss; 

504 
List.app (curry TextIO.output out o RC.tptp_classrelClause) classrel_clauses; 

505 
List.app (curry TextIO.output out o RC.tptp_arity_clause) arity_clauses; 

506 
List.app (curry TextIO.output out o #1 o clause2tptp) helper_clauses; 

507 
TextIO.closeOut out; 

508 
clnames 

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

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

510 

19720  511 

20644  512 

19720  513 
(* dfg format *) 
514 

24323
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

515 
fun dfg_write_file thy isFO thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas = 
23386  516 
let val _ = Output.debug (fn () => ("Preparing to write the DFG file " ^ filename)) 
517 
val _ = RC.dfg_format := true 

24323
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

518 
val conjectures = make_conjecture_clauses thy thms 
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

519 
val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses thy ax_tuples) 
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

520 
val helper_clauses = get_helper_clauses thy isFO (conjectures, axclauses, user_lemmas) 
24311  521 
val _ = count_constants (conjectures, axclauses, helper_clauses); 
24323
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

522 
val (dfg_clss, tfree_litss) = ListPair.unzip (map clause2dfg conjectures) 
24311  523 
and probname = Path.implode (Path.base (Path.explode filename)) 
524 
val axstrs = map (#1 o clause2dfg) axclauses 

525 
val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss) 

526 
val out = TextIO.openOut filename 

527 
val helper_clauses_strs = map (#1 o clause2dfg) helper_clauses 

528 
val (funcs,cl_preds) = decls_of_clauses (helper_clauses @ conjectures @ axclauses) arity_clauses 

529 
and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses 

19720  530 
in 
24311  531 
TextIO.output (out, RC.string_of_start probname); 
532 
TextIO.output (out, RC.string_of_descrip probname); 

533 
TextIO.output (out, RC.string_of_symbols 

534 
(RC.string_of_funcs funcs) 

535 
(RC.string_of_preds (cl_preds @ ty_preds))); 

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

537 
RC.writeln_strs out axstrs; 

538 
List.app (curry TextIO.output out o RC.dfg_classrelClause) classrel_clauses; 

539 
List.app (curry TextIO.output out o RC.dfg_arity_clause) arity_clauses; 

540 
RC.writeln_strs out helper_clauses_strs; 

541 
TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"); 

542 
RC.writeln_strs out tfree_clss; 

543 
RC.writeln_strs out dfg_clss; 

544 
TextIO.output (out, "end_of_list.\n\n"); 

545 
(*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*) 

546 
TextIO.output (out, "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n"); 

547 
TextIO.output (out, "end_problem.\n"); 

548 
TextIO.closeOut out; 

549 
clnames 

19720  550 
end; 
551 

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

552 
end 