author  paulson 
Tue, 09 Oct 2007 18:14:00 +0200  
changeset 24937  340523598914 
parent 24385  ab62948281a9 
child 24940  8f9dea697b8d 
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, 

24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24385
diff
changeset

100 
ctypes_sorts: (RC.typ_var * Term.sort) 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

101 

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

102 

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

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 

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

110 
 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

111 

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

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

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

115 
 isTrue _ = false; 
24311  116 

117 
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

118 

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

119 
fun type_of (Type (a, Ts)) = 
21561  120 
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

121 
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

122 
 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

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

124 
 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

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

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

127 
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

128 
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

129 

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

130 
(* same as above, but no gathering of sort information *) 
24311  131 
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

132 
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

133 
 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

134 
 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

135 

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

136 

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

137 
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

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

139 
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

140 

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

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

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

143 
let val (tp,ts,tvar_list) = const_type_of thy (c,t) 
24311  144 
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

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

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

147 
let val (tp,ts) = type_of t 
24311  148 
val v' = if RC.isMeta v then CombVar(RC.make_schematic_var(v,0),tp) 
149 
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

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

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

152 
let val (tp,ts) = type_of t 
24311  153 
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

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

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

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

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

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

159 
 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

160 

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

161 
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

162 
 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

163 

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

164 
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

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

166 
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

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

168 
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

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

171 
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

172 

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

173 
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

174 

0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. 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 
(* making axiom and conjecture clauses *) 
24323
9aa7b5708eac
removed stateful init: operations take proper theory argument;
wenzelm
parents:
24311
diff
changeset

176 
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

177 
let val (lits,ctypes_sorts) = literals_of_term thy (prop_of th) 
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

178 
in 
24311  179 
if forall isFalse lits 
180 
then error "Problem too trivial for resolution (empty clause)" 

181 
else 

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

24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24385
diff
changeset

183 
literals = lits, ctypes_sorts = 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

184 
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

185 

20016  186 

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

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

188 
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

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

190 
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

191 
end; 
19354  192 

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

193 
fun make_axiom_clauses thy = foldl (add_axiom_clause thy) []; 
19354  194 

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

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

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

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

198 
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

199 

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

200 
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

201 

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

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

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

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

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 

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

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

210 
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

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

212 

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

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

214 
 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

215 
 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

216 

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

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

219 
let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts) 
22064  220 
 stripc x = x 
221 
in stripc(u,[]) end; 

222 

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

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

224 

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

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

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

227 

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

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

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

231 
else s; 
24311  232 

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

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

234 

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

236 
 rev_apply (v, arg::args) = apply [rev_apply (v, args), arg]; 
22064  237 

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

239 

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

241 
direct function application.*) 

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

242 
fun string_of_applic (CombConst(c,tp,tvars), args) = 
22064  243 
let val c = if c = "equal" then "c_fequal" else c 
244 
val nargs = min_arity_of c 

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

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

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

250 
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

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

252 
in 
24311  253 
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

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

255 
 string_of_applic (CombVar(v,tp), args) = string_apply (v, args) 
22064  256 
 string_of_applic _ = raise ERROR "string_of_applic"; 
257 

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

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

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

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

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

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

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

266 

22064  267 
(*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

268 
fun boolify t = "hBOOL" ^ RC.paren_pack [string_of_combterm t]; 
22064  269 

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

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

275 
 _ => 

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

278 
 _ => boolify t; 

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

279 

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

281 
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

282 

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

284 
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

285 

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

286 

21561  287 
(*** tptp format ***) 
19720  288 

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

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

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

291 
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

292 

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

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

296 
RC.tptp_sign pol (string_of_predicate pred); 
24311  297 

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

24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24385
diff
changeset

300 
fun tptp_type_lits pos (Clause{literals, ctypes_sorts, ...}) = 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24385
diff
changeset

301 
(map tptp_literal literals, 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24385
diff
changeset

302 
map (RC.tptp_of_typeLit pos) (RC.add_typs ctypes_sorts)); 
24311  303 

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

304 
fun clause2tptp (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) = 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24385
diff
changeset

305 
let val (lits,tylits) = tptp_type_lits (kind = RC.Conjecture) cls 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24385
diff
changeset

306 
in 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24385
diff
changeset

307 
(RC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits) 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24385
diff
changeset

308 
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

309 

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

310 

21561  311 
(*** dfg format ***) 
312 

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

313 
fun dfg_literal (Literal(pol,pred)) = RC.dfg_sign pol (string_of_predicate pred); 
19720  314 

24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24385
diff
changeset

315 
fun dfg_type_lits pos (Clause{literals, ctypes_sorts, ...}) = 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24385
diff
changeset

316 
(map dfg_literal literals, 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24385
diff
changeset

317 
map (RC.dfg_of_typeLit pos) (RC.add_typs ctypes_sorts)); 
19720  318 

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

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

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

321 
 get_uvars (CombApp(P,Q)) vars = get_uvars P (get_uvars Q vars); 
19720  322 

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

324 

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

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

19720  327 
fun clause2dfg (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) = 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24385
diff
changeset

328 
let val (lits,tylits) = dfg_type_lits (kind = RC.Conjecture) cls 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24385
diff
changeset

329 
val vars = dfg_vars cls 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24385
diff
changeset

330 
val tvars = RC.get_tvar_strs ctypes_sorts 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24385
diff
changeset

331 
in 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24385
diff
changeset

332 
(RC.gen_dfg_cls(clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits) 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24385
diff
changeset

333 
end; 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24385
diff
changeset

334 

19720  335 

22064  336 
(** For DFG format: accumulate function and predicate declarations **) 
19720  337 

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

338 
fun addtypes tvars tab = foldl RC.add_foltype_funcs tab tvars; 
19720  339 

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

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

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

344 
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

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

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

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

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

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

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

352 
 add_decls (CombApp(P,Q),decls) = add_decls(P,add_decls (Q,decls)); 
19720  353 

22064  354 
fun add_literal_decls (Literal(_,c), decls) = add_decls (c,decls); 
19720  355 

22064  356 
fun add_clause_decls (Clause {literals, ...}, decls) = 
357 
foldl add_literal_decls decls literals 

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

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

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

364 
in 

24311  365 
(Symtab.dest (foldl RC.add_arityClause_funcs functab arity_clauses), 
22064  366 
Symtab.dest predtab) 
367 
end; 

19720  368 

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

369 
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

370 
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

371 
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

372 

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

373 
(*Higherorder clauses have only the predicates hBOOL and type classes.*) 
24311  374 
fun preds_of_clauses clauses clsrel_clauses arity_clauses = 
19720  375 
Symtab.dest 
24311  376 
(foldl RC.add_classrelClause_preds 
377 
(foldl RC.add_arityClause_preds 

378 
(foldl add_clause_preds Symtab.empty clauses) 

379 
arity_clauses) 

380 
clsrel_clauses) 

19720  381 

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

382 

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

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

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

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

386 

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

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

388 
Symtab.make [("c_COMBI", 0), ("c_COMBK", 0), 
24311  389 
("c_COMBB", 0), ("c_COMBC", 0), 
390 
("c_COMBS", 0), ("c_COMBB_e", 0), 

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

392 

393 
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

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

395 
 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

396 
 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

397 
 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

398 

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

399 
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

400 

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

401 
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

402 

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

404 
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

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

406 

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

407 
val cnf_helper_thms = ResAxioms.cnf_rules_pairs o (map ResAxioms.pairname) 
20644  408 

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

409 
fun get_helper_clauses thy isFO (conjectures, axclauses, user_lemmas) = 
23386  410 
if isFO then [] (*firstorder*) 
411 
else 

22064  412 
let val ct0 = foldl count_clause init_counters conjectures 
413 
val ct = foldl (count_user_clause user_lemmas) ct0 axclauses 

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

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

417 
else [] 

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

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

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

423 
else [] 

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

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

426 
else [] 

427 
val S' = if needed "c_COMBS_e" 

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

429 
else [] 

430 
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

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

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

434 

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

437 
fun count_constants_term toplev t = 

438 
let val (head, args) = strip_comb t 

439 
val n = length args 

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

441 
in 

442 
case head of 

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

445 
in 

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

447 
if toplev then () 

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

449 
end 

450 
 ts => () 

22064  451 
end; 
452 

453 
(*A literal is a toplevel term*) 

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

455 

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

457 

458 
fun display_arity (c,n) = 

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

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

463 
if !minimize_applies then 
24311  464 
(const_min_arity := Symtab.empty; 
23386  465 
const_needs_hBOOL := Symtab.empty; 
466 
List.app count_constants_clause conjectures; 

22064  467 
List.app count_constants_clause axclauses; 
468 
List.app count_constants_clause helper_clauses; 

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

470 
else (); 

471 

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

472 
(* tptp format *) 
24311  473 

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

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

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

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

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

479 
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

480 
val helper_clauses = get_helper_clauses thy isFO (conjectures, axclauses, user_lemmas) 
24311  481 
val _ = count_constants (conjectures, axclauses, helper_clauses); 
482 
val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp conjectures) 

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

22064  484 
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

485 
in 
24311  486 
List.app (curry TextIO.output out o #1 o clause2tptp) axclauses; 
487 
RC.writeln_strs out tfree_clss; 

488 
RC.writeln_strs out tptp_clss; 

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

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

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

492 
TextIO.closeOut out; 

493 
clnames 

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

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

495 

19720  496 

497 
(* dfg format *) 

498 

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

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

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

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

503 
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

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

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

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

510 
val out = TextIO.openOut filename 

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

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

513 
and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses 

19720  514 
in 
24311  515 
TextIO.output (out, RC.string_of_start probname); 
516 
TextIO.output (out, RC.string_of_descrip probname); 

517 
TextIO.output (out, RC.string_of_symbols 

518 
(RC.string_of_funcs funcs) 

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

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

521 
RC.writeln_strs out axstrs; 

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

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

524 
RC.writeln_strs out helper_clauses_strs; 

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

526 
RC.writeln_strs out tfree_clss; 

527 
RC.writeln_strs out dfg_clss; 

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

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

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

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

532 
TextIO.closeOut out; 

533 
clnames 

19720  534 
end; 
535 

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

536 
end 