author  paulson 
Tue, 31 Jan 2006 10:39:13 +0100  
changeset 18863  a113b6839df1 
parent 18856  4669dec681f4 
child 18868  7cfc21ee0370 
permissions  rwrr 
15347  1 
(* Author: Jia Meng, Cambridge University Computer Laboratory 
2 
ID: $Id$ 

3 
Copyright 2004 University of Cambridge 

4 

5 
ML data structure for storing/printing FOL clauses and arity clauses. 

6 
Typed equality is treated differently. 

7 
*) 

8 

17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

9 
(* works for writeoutclasimp on typed *) 
15347  10 
signature RES_CLAUSE = 
11 
sig 

17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

12 
val keep_types : bool ref 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

13 
val special_equal : bool ref 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

14 
val tagged : bool ref 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

15 

d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

16 
exception ARCLAUSE of string 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

17 
exception CLAUSE of string * term 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

18 
type arityClause 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

19 
type classrelClause 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

20 
type clause 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

21 
val init : theory > unit 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

22 
val make_axiom_clause : Term.term > string * int > clause 
17888  23 
val make_conjecture_clauses : term list > clause list 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

24 
val get_axiomName : clause > string 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

25 
val isTaut : clause > bool 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

26 
val num_of_clauses : clause > int 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

27 

17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

28 
val arity_clause_thy: theory > arityClause list 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

29 
val classrel_clauses_thy: theory > classrelClause list 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

30 

17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

31 
val tptp_arity_clause : arityClause > string 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

32 
val tptp_classrelClause : classrelClause > string 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

33 
val tptp_clause : clause > string list 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

34 
val clause2tptp : clause > string * string list 
18863  35 
val tptp_tfree_clause : string > string 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

36 
val schematic_var_prefix : string 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

37 
val fixed_var_prefix : string 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

38 
val tvar_prefix : string 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

39 
val tfree_prefix : string 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

40 
val clause_prefix : string 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

41 
val arclause_prefix : string 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

42 
val const_prefix : string 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

43 
val tconst_prefix : string 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

44 
val class_prefix : string 
17908
ac97527724ba
More functions are added to the signature of ResClause
mengj
parents:
17888
diff
changeset

45 

ac97527724ba
More functions are added to the signature of ResClause
mengj
parents:
17888
diff
changeset

46 
val union_all : ''a list list > ''a list 
ac97527724ba
More functions are added to the signature of ResClause
mengj
parents:
17888
diff
changeset

47 
val ascii_of : String.string > String.string 
ac97527724ba
More functions are added to the signature of ResClause
mengj
parents:
17888
diff
changeset

48 
val paren_pack : string list > string 
ac97527724ba
More functions are added to the signature of ResClause
mengj
parents:
17888
diff
changeset

49 
val bracket_pack : string list > string 
ac97527724ba
More functions are added to the signature of ResClause
mengj
parents:
17888
diff
changeset

50 
val make_schematic_var : String.string * int > string 
ac97527724ba
More functions are added to the signature of ResClause
mengj
parents:
17888
diff
changeset

51 
val make_fixed_var : String.string > string 
ac97527724ba
More functions are added to the signature of ResClause
mengj
parents:
17888
diff
changeset

52 
val make_schematic_type_var : string * int > string 
ac97527724ba
More functions are added to the signature of ResClause
mengj
parents:
17888
diff
changeset

53 
val make_fixed_type_var : string > string 
ac97527724ba
More functions are added to the signature of ResClause
mengj
parents:
17888
diff
changeset

54 
val make_fixed_const : String.string > string 
ac97527724ba
More functions are added to the signature of ResClause
mengj
parents:
17888
diff
changeset

55 
val make_fixed_type_const : String.string > string 
ac97527724ba
More functions are added to the signature of ResClause
mengj
parents:
17888
diff
changeset

56 
val make_type_class : String.string > string 
17999  57 
val isMeta : String.string > bool 
58 

59 
type typ_var 

60 
val mk_typ_var_sort : Term.typ > typ_var * sort 

61 
type type_literal 

18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

62 
val add_typs_aux : (typ_var * string list) list > type_literal list * type_literal list 
17999  63 
val gen_tptp_cls : int * string * string * string > string 
64 
val gen_tptp_type_cls : int * string * string * string * int > string 

65 
val tptp_of_typeLit : type_literal > string 

18275  66 

18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

67 
(*for hashing*) 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

68 
val clause_eq : clause * clause > bool 
18449  69 
val hash_clause : clause > int 
18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

70 

18439
4b517881ac7e
Added functions for fol_type; also put some functions to the signature, used by ResHolClause.
mengj
parents:
18420
diff
changeset

71 
val list_ord : ('a * 'b > order) > 'a list * 'b list > order 
4b517881ac7e
Added functions for fol_type; also put some functions to the signature, used by ResHolClause.
mengj
parents:
18420
diff
changeset

72 
type fol_type 
4b517881ac7e
Added functions for fol_type; also put some functions to the signature, used by ResHolClause.
mengj
parents:
18420
diff
changeset

73 
val types_ord : fol_type list * fol_type list > order 
4b517881ac7e
Added functions for fol_type; also put some functions to the signature, used by ResHolClause.
mengj
parents:
18420
diff
changeset

74 
val string_of_fol_type : fol_type > string 
4b517881ac7e
Added functions for fol_type; also put some functions to the signature, used by ResHolClause.
mengj
parents:
18420
diff
changeset

75 
val mk_fol_type: string * string * fol_type list > fol_type 
18863  76 
val types_eq: fol_type list * fol_type list > 
77 
(string*string) list * (string*string) list > 

78 
bool * ((string*string) list * (string*string) list) 

18439
4b517881ac7e
Added functions for fol_type; also put some functions to the signature, used by ResHolClause.
mengj
parents:
18420
diff
changeset

79 
val check_var_pairs: ''a * ''b > (''a * ''b) list > int 
18863  80 

81 
val dfg_write_file: thm list > string > 

82 
(clause list * classrelClause list * arityClause list) > unit 

83 
val tptp_write_file: thm list > string > 

84 
(clause list * classrelClause list * arityClause list) > unit 

85 
val writeln_strs: TextIO.outstream > TextIO.vector list > unit 

15347  86 
end; 
87 

18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

88 
structure ResClause : RES_CLAUSE = 
15347  89 
struct 
90 

91 
(* Added for typed equality *) 

92 
val special_equal = ref false; (* by default,equality does not carry type information *) 

93 
val eq_typ_wrapper = "typeinfo"; (* default string *) 

94 

95 

96 
val schematic_var_prefix = "V_"; 

97 
val fixed_var_prefix = "v_"; 

98 

17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

99 
val tvar_prefix = "T_"; 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

100 
val tfree_prefix = "t_"; 
15347  101 

102 
val clause_prefix = "cls_"; 

17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

103 
val arclause_prefix = "clsarity_" 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

104 
val clrelclause_prefix = "clsrel_"; 
15347  105 

17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

106 
val const_prefix = "c_"; 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

107 
val tconst_prefix = "tc_"; 
16199
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset

108 
val class_prefix = "class_"; 
15347  109 

17775  110 
fun union_all xss = foldl (op union) [] xss; 
111 

112 
(*Provide readable names for the more common symbolic functions*) 

15347  113 
val const_trans_table = 
114 
Symtab.make [("op =", "equal"), 

115 
("op <=", "lessequals"), 

116 
("op <", "less"), 

117 
("op &", "and"), 

118 
("op ", "or"), 

17375  119 
("op +", "plus"), 
120 
("op ", "minus"), 

121 
("op *", "times"), 

18676  122 
("Divides.op div", "div"), 
123 
("HOL.divide", "divide"), 

15347  124 
("op >", "implies"), 
17375  125 
("{}", "emptyset"), 
15347  126 
("op :", "in"), 
127 
("op Un", "union"), 

18390  128 
("op Int", "inter"), 
129 
("List.op @", "append")]; 

15347  130 

17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

131 
val type_const_trans_table = 
18411
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

132 
Symtab.make [("*", "prod"), 
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

133 
("+", "sum"), 
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

134 
("~=>", "map")]; 
15347  135 

15610  136 
(*Escaping of special characters. 
137 
Alphanumeric characters are left unchanged. 

138 
The character _ goes to __ 

139 
Characters in the range ASCII space to / go to _A to _P, respectively. 

140 
Other printing characters go to _NNN where NNN is the decimal ASCII code.*) 

141 
local 

142 

143 
val A_minus_space = Char.ord #"A"  Char.ord #" "; 

144 

15347  145 
fun ascii_of_c c = 
15610  146 
if Char.isAlphaNum c then String.str c 
147 
else if c = #"_" then "__" 

148 
else if #" " <= c andalso c <= #"/" 

149 
then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space)) 

150 
else if Char.isPrint c then ("_" ^ Int.toString (Char.ord c)) 

151 
else "" 

15347  152 

15610  153 
in 
154 

155 
val ascii_of = String.translate ascii_of_c; 

156 

157 
end; 

15347  158 

17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

159 
(* convert a list of strings into one single string; surrounded by brackets *) 
18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

160 
fun paren_pack [] = "" (*empty argument list*) 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

161 
 paren_pack strings = "(" ^ commas strings ^ ")"; 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

162 

ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

163 
fun bracket_pack strings = "[" ^ commas strings ^ "]"; 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

164 

ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

165 

16925
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset

166 
(*Remove the initial ' character from a type variable, if it is present*) 
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset

167 
fun trim_type_var s = 
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset

168 
if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE) 
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset

169 
else error ("trim_type: Malformed type variable encountered: " ^ s); 
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset

170 

16903  171 
fun ascii_of_indexname (v,0) = ascii_of v 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

172 
 ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i; 
15347  173 

17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

174 
fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v); 
15347  175 
fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x); 
176 

16925
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset

177 
fun make_schematic_type_var (x,i) = 
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset

178 
tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i)); 
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset

179 
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); 
15347  180 

18411
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

181 
fun lookup_const c = 
17412  182 
case Symtab.lookup const_trans_table c of 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

183 
SOME c' => c' 
18411
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

184 
 NONE => ascii_of c; 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

185 

18411
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

186 
fun lookup_type_const c = 
17412  187 
case Symtab.lookup type_const_trans_table c of 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

188 
SOME c' => c' 
18411
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

189 
 NONE => ascii_of c; 
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

190 

2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

191 
fun make_fixed_const "op =" = "equal" (*MUST BE "equal" because it's builtin to ATPs*) 
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

192 
 make_fixed_const c = const_prefix ^ lookup_const c; 
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

193 

2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

194 
fun make_fixed_type_const c = tconst_prefix ^ lookup_type_const c; 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

195 

17261  196 
fun make_type_class clas = class_prefix ^ ascii_of clas; 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

197 

ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

198 

18798  199 
(***** definitions and functions for FOL clauses, for conversion to TPTP or DFG format. *****) 
15347  200 

17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

201 
val keep_types = ref true; 
15347  202 

203 
datatype kind = Axiom  Hypothesis  Conjecture; 

204 
fun name_of_kind Axiom = "axiom" 

205 
 name_of_kind Hypothesis = "hypothesis" 

206 
 name_of_kind Conjecture = "conjecture"; 

207 

208 
type clause_id = int; 

209 
type axiom_name = string; 

210 

211 

212 
type polarity = bool; 

213 

214 
(* "tag" is used for vampire specific syntax *) 

215 
type tag = bool; 

216 

217 

218 
(**** Isabelle FOL clauses ****) 

219 

220 
val tagged = ref false; 

221 

222 
type pred_name = string; 

18402
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

223 

aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

224 
datatype typ_var = FOLTVar of indexname  FOLTFree of string; 
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

225 

18798  226 
(*FIXME: give the constructors more sensible names*) 
18402
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

227 
datatype fol_type = AtomV of string 
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

228 
 AtomF of string 
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

229 
 Comp of string * fol_type list; 
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

230 

aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

231 
fun string_of_fol_type (AtomV x) = x 
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

232 
 string_of_fol_type (AtomF x) = x 
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

233 
 string_of_fol_type (Comp(tcon,tps)) = 
18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

234 
tcon ^ (paren_pack (map string_of_fol_type tps)); 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

235 

18439
4b517881ac7e
Added functions for fol_type; also put some functions to the signature, used by ResHolClause.
mengj
parents:
18420
diff
changeset

236 
fun mk_fol_type ("Var",x,_) = AtomV(x) 
4b517881ac7e
Added functions for fol_type; also put some functions to the signature, used by ResHolClause.
mengj
parents:
18420
diff
changeset

237 
 mk_fol_type ("Fixed",x,_) = AtomF(x) 
4b517881ac7e
Added functions for fol_type; also put some functions to the signature, used by ResHolClause.
mengj
parents:
18420
diff
changeset

238 
 mk_fol_type ("Comp",con,args) = Comp(con,args) 
4b517881ac7e
Added functions for fol_type; also put some functions to the signature, used by ResHolClause.
mengj
parents:
18420
diff
changeset

239 

4b517881ac7e
Added functions for fol_type; also put some functions to the signature, used by ResHolClause.
mengj
parents:
18420
diff
changeset

240 

18798  241 
(*First string is the type class; the second is a TVar or TFfree*) 
242 
datatype type_literal = LTVar of string * string  LTFree of string * string; 

15347  243 

18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

244 
datatype fol_term = UVar of string * fol_type 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

245 
 Fun of string * fol_type list * fol_term list; 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

246 
datatype predicate = Predicate of pred_name * fol_type list * fol_term list; 
15347  247 

248 
datatype literal = Literal of polarity * predicate * tag; 

249 

17999  250 
fun mk_typ_var_sort (TFree(a,s)) = (FOLTFree a,s) 
251 
 mk_typ_var_sort (TVar(v,s)) = (FOLTVar v,s); 

252 

253 

18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

254 
(*A clause has firstorder literals and other, typerelated literals*) 
15347  255 
datatype clause = 
256 
Clause of {clause_id: clause_id, 

257 
axiom_name: axiom_name, 

258 
kind: kind, 

259 
literals: literal list, 

260 
types_sorts: (typ_var * sort) list, 

261 
tvar_type_literals: type_literal list, 

18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

262 
tfree_type_literals: type_literal list}; 
15347  263 

17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

264 
exception CLAUSE of string * term; 
15347  265 

18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

266 
fun isFalse (Literal (pol,Predicate(pname,_,[]),_)) = 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

267 
(pol andalso pname = "c_False") orelse 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

268 
(not pol andalso pname = "c_True") 
17317
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

269 
 isFalse _ = false; 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

270 

18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

271 
fun isTrue (Literal (pol,Predicate(pname,_,[]),_)) = 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

272 
(pol andalso pname = "c_True") orelse 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

273 
(not pol andalso pname = "c_False") 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

274 
 isTrue _ = false; 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

275 

d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

276 
fun isTaut (Clause {literals,...}) = exists isTrue literals; 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

277 

17234  278 
fun make_clause (clause_id,axiom_name,kind,literals, 
18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

279 
types_sorts,tvar_type_literals,tfree_type_literals) = 
17317
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

280 
if forall isFalse literals 
17234  281 
then error "Problem too trivial for resolution (empty clause)" 
282 
else 

17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

283 
Clause {clause_id = clause_id, axiom_name = axiom_name, kind = kind, 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

284 
literals = literals, types_sorts = types_sorts, 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

285 
tvar_type_literals = tvar_type_literals, 
18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

286 
tfree_type_literals = tfree_type_literals}; 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

287 

15347  288 

17317
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

289 
(** Some Clause destructor functions **) 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

290 

3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

291 
fun string_of_kind (Clause cls) = name_of_kind (#kind cls); 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

292 

3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

293 
fun get_axiomName (Clause cls) = #axiom_name cls; 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

294 

3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

295 
fun get_clause_id (Clause cls) = #clause_id cls; 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

296 

3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

297 

18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

298 
(*Declarations of the current theoryto allow suppressing types.*) 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

299 
val const_typargs = ref (Library.K [] : (string*typ > typ list)); 
17317
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

300 

18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

301 
fun num_typargs(s,T) = if !keep_types then length (!const_typargs (s,T)) else 0; 
16925
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset

302 

0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset

303 
(*Initialize the type suppression mechanism with the current theory before 
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset

304 
producing any clauses!*) 
18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

305 
fun init thy = (const_typargs := Sign.const_typargs thy); 
16925
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset

306 

17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

307 

18402
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

308 
(*Flatten a type to a fol_type while accumulating sort constraints on the TFrees and 
16925
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset

309 
TVars it contains.*) 
18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

310 
fun type_of (Type (a, Ts)) = 
18798  311 
let val (folTyps, ts) = types_of Ts 
18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

312 
val t = make_fixed_type_const a 
18798  313 
in (Comp(t,folTyps), ts) end 
314 
 type_of (TFree (a,s)) = (AtomF(make_fixed_type_var a), [(FOLTFree a, s)]) 

315 
 type_of (TVar (v, s)) = (AtomV(make_schematic_type_var v), [(FOLTVar v, s)]) 

18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

316 
and types_of Ts = 
18798  317 
let val (folTyps,ts) = ListPair.unzip (map type_of Ts) 
318 
in (folTyps, union_all ts) end; 

15390  319 

18439
4b517881ac7e
Added functions for fol_type; also put some functions to the signature, used by ResHolClause.
mengj
parents:
18420
diff
changeset

320 

18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

321 
fun const_types_of (c,T) = types_of (!const_typargs (c,T)); 
16925
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset

322 

16903  323 
(* Any variables created via the METAHYPS tactical should be treated as 
324 
universal vars, although it is represented as "Free(...)" by Isabelle *) 

325 
val isMeta = String.isPrefix "METAHYP1_" 

17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

326 

18798  327 
fun pred_name_type (Const(c,T)) = (make_fixed_const c, const_types_of (c,T)) 
15390  328 
 pred_name_type (Free(x,T)) = 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

329 
if isMeta x then raise CLAUSE("Predicate Not First Order 1", Free(x,T)) 
18798  330 
else (make_fixed_var x, ([],[])) 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

331 
 pred_name_type (v as Var _) = raise CLAUSE("Predicate Not First Order 2", v) 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

332 
 pred_name_type t = raise CLAUSE("Predicate input unexpected", t); 
15347  333 

15615  334 

18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

335 
(* For typed equality *) 
15615  336 
(* here "arg_typ" is the type of "="'s argument's type, not the type of the equality *) 
337 
(* Find type of equality arg *) 

338 
fun eq_arg_type (Type("fun",[T,_])) = 

339 
let val (folT,_) = type_of T; 

17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

340 
in folT end; 
15347  341 

18798  342 
fun fun_name_type (Const(c,T)) args = (make_fixed_const c, const_types_of (c,T)) 
343 
 fun_name_type (Free(x,T)) args = 

344 
if isMeta x then raise CLAUSE("Function Not First Order", Free(x,T)) 

345 
else (make_fixed_var x, ([],[])) 

17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

346 
 fun_name_type f args = raise CLAUSE("Function Not First Order 1", f); 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

347 

18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

348 
(*Convert a term to a fol_term while accumulating sort constraints on the TFrees and 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

349 
TVars it contains.*) 
15347  350 
fun term_of (Var(ind_nm,T)) = 
18798  351 
let val (folType,ts) = type_of T 
352 
in (UVar(make_schematic_var ind_nm, folType), ts) end 

15347  353 
 term_of (Free(x,T)) = 
18798  354 
let val (folType, ts) = type_of T 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

355 
in 
18798  356 
if isMeta x then (UVar(make_schematic_var(x,0),folType), ts) 
357 
else (Fun(make_fixed_var x, [folType], []), ts) 

17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

358 
end 
18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

359 
 term_of app = 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

360 
let val (f,args) = strip_comb app 
18798  361 
val (funName,(contys,ts1)) = fun_name_type f args 
362 
val (args',ts2) = terms_of args 

17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

363 
in 
18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

364 
(Fun(funName,contys,args'), 
18798  365 
(union_all (ts1::ts2))) 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

366 
end 
18798  367 
and terms_of ts = ListPair.unzip (map term_of ts) 
15390  368 

18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

369 
(*Create a predicate value, again accumulating sort constraints.*) 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

370 
fun pred_of (Const("op =", typ), args) = 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

371 
let val arg_typ = eq_arg_type typ 
18798  372 
val (args',ts) = terms_of args 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

373 
val equal_name = make_fixed_const "op =" 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

374 
in 
18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

375 
(Predicate(equal_name,[arg_typ],args'), 
18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

376 
union_all ts) 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

377 
end 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

378 
 pred_of (pred,args) = 
18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

379 
let val (pname, (predType,ts1)) = pred_name_type pred 
18798  380 
val (args',ts2) = terms_of args 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

381 
in 
18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

382 
(Predicate(pname,predType,args'), union_all (ts1::ts2)) 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

383 
end; 
15347  384 

17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

385 
(*Treatment of literals, possibly negated or tagged*) 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

386 
fun predicate_of ((Const("Not",_) $ P), polarity, tag) = 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

387 
predicate_of (P, not polarity, tag) 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

388 
 predicate_of ((Const("HOL.tag",_) $ P), polarity, tag) = 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

389 
predicate_of (P, polarity, true) 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

390 
 predicate_of (term,polarity,tag) = 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

391 
(pred_of (strip_comb term), polarity, tag); 
15347  392 

17888  393 
fun literals_of_term1 args (Const("Trueprop",_) $ P) = literals_of_term1 args P 
18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

394 
 literals_of_term1 args (Const("op ",_) $ P $ Q) = 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

395 
literals_of_term1 (literals_of_term1 args P) Q 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

396 
 literals_of_term1 (lits, ts) P = 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

397 
let val ((pred, ts'), polarity, tag) = predicate_of (P,true,false) 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

398 
val lits' = Literal(polarity,pred,tag) :: lits 
17234  399 
in 
18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

400 
(lits', ts union ts') 
17234  401 
end; 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

402 

18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

403 
val literals_of_term = literals_of_term1 ([],[]); 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

404 

18403
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

405 

df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

406 
fun list_ord _ ([],[]) = EQUAL 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

407 
 list_ord _ ([],_) = LESS 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

408 
 list_ord _ (_,[]) = GREATER 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

409 
 list_ord ord (x::xs, y::ys) = 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

410 
let val xy_ord = ord(x,y) 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

411 
in 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

412 
case xy_ord of EQUAL => list_ord ord (xs,ys) 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

413 
 _ => xy_ord 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

414 
end; 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

415 

df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

416 
fun type_ord (AtomV(_),AtomV(_)) = EQUAL 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

417 
 type_ord (AtomV(_),_) = LESS 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

418 
 type_ord (AtomF(_),AtomV(_)) = GREATER 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

419 
 type_ord (AtomF(f1),AtomF(f2)) = string_ord (f1,f2) 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

420 
 type_ord (AtomF(_),_) = LESS 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

421 
 type_ord (Comp(_,_),AtomV(_)) = GREATER 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

422 
 type_ord (Comp(_,_),AtomF(_)) = GREATER 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

423 
 type_ord (Comp(con1,args1),Comp(con2,args2)) = 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

424 
let val con_ord = string_ord(con1,con2) 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

425 
in 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

426 
case con_ord of EQUAL => types_ord (args1,args2) 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

427 
 _ => con_ord 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

428 
end 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

429 
and 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

430 

df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

431 
types_ord ([],[]) = EQUAL 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

432 
 types_ord (tps1,tps2) = list_ord type_ord (tps1,tps2); 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

433 

18402
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

434 

18403
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

435 
fun term_ord (UVar(_,_),UVar(_,_)) = EQUAL 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

436 
 term_ord (UVar(_,_),_) = LESS 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

437 
 term_ord (Fun(_,_,_),UVar(_)) = GREATER 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

438 
 term_ord (Fun(f1,tps1,tms1),Fun(f2,tps2,tms2)) = 
18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

439 
(case string_ord (f1,f2) of 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

440 
EQUAL => 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

441 
(case terms_ord (tms1,tms2) of EQUAL => types_ord (tps1,tps2) 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

442 
 tms_ord => tms_ord) 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

443 
 fn_ord => fn_ord) 
18403
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

444 

df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

445 
and 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

446 

18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

447 
terms_ord ([],[]) = EQUAL 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

448 
 terms_ord (tms1,tms2) = list_ord term_ord (tms1,tms2); 
18403
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

449 

df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

450 

df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

451 

18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

452 
fun predicate_ord (Predicate(pname1,ftyps1,ftms1),Predicate(pname2,ftyps2,ftms2)) = 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

453 
case string_ord (pname1,pname2) of 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

454 
EQUAL => (case terms_ord(ftms1,ftms2) of EQUAL => types_ord(ftyps1,ftyps2) 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

455 
 ftms_ord => ftms_ord) 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

456 
 pname_ord => pname_ord 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

457 

18402
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

458 

aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

459 
fun literal_ord (Literal(false,_,_),Literal(true,_,_)) = LESS 
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

460 
 literal_ord (Literal(true,_,_),Literal(false,_,_)) = GREATER 
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

461 
 literal_ord (Literal(_,pred1,_),Literal(_,pred2,_)) = predicate_ord(pred1,pred2); 
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

462 

aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

463 
fun sort_lits lits = sort literal_ord lits; 
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

464 

18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

465 

18409
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

466 
(********** clause equivalence ******************) 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

467 

080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

468 
fun check_var_pairs (x,y) [] = 0 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

469 
 check_var_pairs (x,y) ((u,v)::w) = 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

470 
if (x,y) = (u,v) then 1 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

471 
else 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

472 
if (x = u) orelse (y = v) then 2 (*conflict*) 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

473 
else check_var_pairs (x,y) w; 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

474 

080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

475 
fun type_eq (AtomV(v1),AtomV(v2)) (vars,tvars) = 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

476 
(case check_var_pairs (v1,v2) tvars of 0 => (true,(vars,(v1,v2)::tvars)) 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

477 
 1 => (true,(vars,tvars)) 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

478 
 2 => (false,(vars,tvars))) 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

479 
 type_eq (AtomV(_),_) vtvars = (false,vtvars) 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

480 
 type_eq (AtomF(f1),AtomF(f2)) vtvars = (f1=f2,vtvars) 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

481 
 type_eq (AtomF(_),_) vtvars = (false,vtvars) 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

482 
 type_eq (Comp(con1,args1),Comp(con2,args2)) vtvars = 
18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

483 
let val (eq1,vtvars1) = 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

484 
if con1 = con2 then types_eq (args1,args2) vtvars 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

485 
else (false,vtvars) 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

486 
in 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

487 
(eq1,vtvars1) 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

488 
end 
18409
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

489 
 type_eq (Comp(_,_),_) vtvars = (false,vtvars) 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

490 

080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

491 
and 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

492 

18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

493 
types_eq ([],[]) vtvars = (true,vtvars) 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

494 
 types_eq (tp1::tps1,tp2::tps2) vtvars = 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

495 
let val (eq1,vtvars1) = type_eq (tp1,tp2) vtvars 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

496 
val (eq2,vtvars2) = if eq1 then types_eq (tps1,tps2) vtvars1 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

497 
else (eq1,vtvars1) 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

498 
in 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

499 
(eq2,vtvars2) 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

500 
end; 
18409
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

501 

080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

502 

080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

503 
fun term_eq (UVar(v1,tp1),UVar(v2,tp2)) (vars,tvars) = 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

504 
(case check_var_pairs (v1,v2) vars of 0 => type_eq (tp1,tp2) (((v1,v2)::vars),tvars) 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

505 
 1 => type_eq (tp1,tp2) (vars,tvars) 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

506 
 2 => (false,(vars,tvars))) 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

507 
 term_eq (UVar(_,_),_) vtvars = (false,vtvars) 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

508 
 term_eq (Fun(f1,tps1,tms1),Fun(f2,tps2,tms2)) vtvars = 
18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

509 
let val (eq1,vtvars1) = 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

510 
if f1 = f2 then terms_eq (tms1,tms2) vtvars 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

511 
else (false,vtvars) 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

512 
val (eq2,vtvars2) = 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

513 
if eq1 then types_eq (tps1,tps2) vtvars1 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

514 
else (eq1,vtvars1) 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

515 
in 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

516 
(eq2,vtvars2) 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

517 
end 
18409
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

518 
 term_eq (Fun(_,_,_),_) vtvars = (false,vtvars) 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

519 

080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

520 
and 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

521 

18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

522 
terms_eq ([],[]) vtvars = (true,vtvars) 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

523 
 terms_eq (tm1::tms1,tm2::tms2) vtvars = 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

524 
let val (eq1,vtvars1) = term_eq (tm1,tm2) vtvars 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

525 
val (eq2,vtvars2) = if eq1 then terms_eq (tms1,tms2) vtvars1 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

526 
else (eq1,vtvars1) 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

527 
in 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

528 
(eq2,vtvars2) 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

529 
end; 
18409
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

530 

080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

531 

18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

532 
fun pred_eq (Predicate(pname1,tps1,tms1),Predicate(pname2,tps2,tms2)) vtvars = 
18409
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

533 
let val (eq1,vtvars1) = 
18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

534 
if (pname1 = pname2) then terms_eq (tms1,tms2) vtvars 
18409
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

535 
else (false,vtvars) 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

536 
val (eq2,vtvars2) = 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

537 
if eq1 then types_eq (tps1,tps2) vtvars1 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

538 
else (eq1,vtvars1) 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

539 
in 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

540 
(eq2,vtvars2) 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

541 
end; 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

542 

080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

543 

080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

544 
fun lit_eq (Literal(pol1,pred1,_),Literal(pol2,pred2,_)) vtvars = 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

545 
if (pol1 = pol2) then pred_eq (pred1,pred2) vtvars 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

546 
else (false,vtvars); 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

547 

080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

548 
(*must have the same number of literals*) 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

549 
fun lits_eq ([],[]) vtvars = (true,vtvars) 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

550 
 lits_eq (l1::ls1,l2::ls2) vtvars = 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

551 
let val (eq1,vtvars1) = lit_eq (l1,l2) vtvars 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

552 
in 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

553 
if eq1 then lits_eq (ls1,ls2) vtvars1 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

554 
else (false,vtvars1) 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

555 
end; 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

556 

080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

557 

18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

558 
(*Equality of two clauses up to variable renaming*) 
18798  559 
fun clause_eq (Clause{literals=lits1,...}, Clause{literals=lits2,...}) = 
560 
length lits1 = length lits2 andalso #1 (lits_eq (lits1,lits2) ([],[])); 

18409
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

561 

080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

562 

18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

563 
(*** Hash function for clauses ***) 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

564 

9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

565 
val xor_words = List.foldl Word.xorb 0w0; 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

566 

18449  567 
fun hashw_term (UVar(_,_), w) = w 
568 
 hashw_term (Fun(f,tps,args), w) = 

569 
List.foldl hashw_term (Polyhash.hashw_string (f,w)) args; 

18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

570 

18449  571 
fun hashw_pred (Predicate(pn,_,args), w) = 
572 
List.foldl hashw_term (Polyhash.hashw_string (pn,w)) args; 

18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

573 

18449  574 
fun hash1_literal (Literal(true,pred,_)) = hashw_pred (pred, 0w0) 
575 
 hash1_literal (Literal(false,pred,_)) = Word.notb (hashw_pred (pred, 0w0)); 

18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

576 

18798  577 
fun hash_clause (Clause{literals,...}) = 
578 
Word.toIntX (xor_words (map hash1_literal literals)); 

18402
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

579 

aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

580 

18798  581 
(*Make literals for sorted type variables. FIXME: can it use map?*) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

582 
fun sorts_on_typs (_, []) = ([]) 
16199
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset

583 
 sorts_on_typs (v, "HOL.type" :: s) = 
18411
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

584 
sorts_on_typs (v,s) (*IGNORE sort "type"*) 
18798  585 
 sorts_on_typs ((FOLTVar indx), s::ss) = 
586 
LTVar(make_type_class s, make_schematic_type_var indx) :: 

587 
sorts_on_typs ((FOLTVar indx), ss) 

588 
 sorts_on_typs ((FOLTFree x), s::ss) = 

589 
LTFree(make_type_class s, make_fixed_type_var x) :: 

590 
sorts_on_typs ((FOLTFree x), ss); 

15347  591 

17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

592 

18798  593 
fun pred_of_sort (LTVar (s,ty)) = (s,1) 
594 
 pred_of_sort (LTFree (s,ty)) = (s,1) 

17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

595 

16199
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset

596 
(*Given a list of sorted type variables, return two separate lists. 
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset

597 
The first is for TVars, the second for TFrees.*) 
18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

598 
fun add_typs_aux [] = ([],[]) 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

599 
 add_typs_aux ((FOLTVar indx,s)::tss) = 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

600 
let val vs = sorts_on_typs (FOLTVar indx, s) 
18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

601 
val (vss,fss) = add_typs_aux tss 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

602 
in 
18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

603 
(vs union vss, fss) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

604 
end 
18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

605 
 add_typs_aux ((FOLTFree x,s)::tss) = 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

606 
let val fs = sorts_on_typs (FOLTFree x, s) 
18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

607 
val (vss,fss) = add_typs_aux tss 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

608 
in 
18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

609 
(vss, fs union fss) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

610 
end; 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

611 

17999  612 

18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

613 
fun add_typs (Clause cls) = add_typs_aux (#types_sorts cls) 
15347  614 

615 

616 
(** make axiom clauses, hypothesis clauses and conjecture clauses. **) 

17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

617 

ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

618 
fun get_tvar_strs [] = [] 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

619 
 get_tvar_strs ((FOLTVar indx,s)::tss) = 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

620 
let val vstr = make_schematic_type_var indx 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

621 
in 
17888  622 
vstr ins (get_tvar_strs tss) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

623 
end 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

624 
 get_tvar_strs((FOLTFree x,s)::tss) = distinct (get_tvar_strs tss) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

625 

17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

626 
fun make_axiom_clause_thm thm (ax_name,cls_id) = 
18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

627 
let val (lits,types_sorts) = literals_of_term (prop_of thm) 
18402
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

628 
val lits' = sort_lits lits 
18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

629 
val (tvar_lits,tfree_lits) = add_typs_aux types_sorts 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

630 
in 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

631 
make_clause(cls_id,ax_name,Axiom, 
18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

632 
lits',types_sorts,tvar_lits,tfree_lits) 
15347  633 
end; 
634 

635 

18199
d236379ea408
 before converting axiom and conjecture clauses into ResClause.clause format, perform "check_is_fol_term" first.
mengj
parents:
18056
diff
changeset

636 
(* check if a clause is FOL first*) 
17888  637 
fun make_conjecture_clause n t = 
18199
d236379ea408
 before converting axiom and conjecture clauses into ResClause.clause format, perform "check_is_fol_term" first.
mengj
parents:
18056
diff
changeset

638 
let val _ = check_is_fol_term t 
d236379ea408
 before converting axiom and conjecture clauses into ResClause.clause format, perform "check_is_fol_term" first.
mengj
parents:
18056
diff
changeset

639 
handle TERM("check_is_fol_term",_) => raise CLAUSE("Goal is not FOL",t) 
18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

640 
val (lits,types_sorts) = literals_of_term t 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

641 
val (tvar_lits,tfree_lits) = add_typs_aux types_sorts 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

642 
in 
17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

643 
make_clause(n,"conjecture",Conjecture, 
18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

644 
lits,types_sorts,tvar_lits,tfree_lits) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

645 
end; 
17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

646 

1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

647 
fun make_conjecture_clauses_aux _ [] = [] 
17888  648 
 make_conjecture_clauses_aux n (t::ts) = 
649 
make_conjecture_clause n t :: make_conjecture_clauses_aux (n+1) ts 

17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

650 

1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

651 
val make_conjecture_clauses = make_conjecture_clauses_aux 0 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

652 

ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

653 

18199
d236379ea408
 before converting axiom and conjecture clauses into ResClause.clause format, perform "check_is_fol_term" first.
mengj
parents:
18056
diff
changeset

654 
(*before converting an axiom clause to "clause" format, check if it is FOL*) 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

655 
fun make_axiom_clause term (ax_name,cls_id) = 
18199
d236379ea408
 before converting axiom and conjecture clauses into ResClause.clause format, perform "check_is_fol_term" first.
mengj
parents:
18056
diff
changeset

656 
let val _ = check_is_fol_term term 
d236379ea408
 before converting axiom and conjecture clauses into ResClause.clause format, perform "check_is_fol_term" first.
mengj
parents:
18056
diff
changeset

657 
handle TERM("check_is_fol_term",_) => raise CLAUSE("Axiom is not FOL", term) 
18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

658 
val (lits,types_sorts) = literals_of_term term 
18402
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

659 
val lits' = sort_lits lits 
18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

660 
val (tvar_lits,tfree_lits) = add_typs_aux types_sorts 
15347  661 
in 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

662 
make_clause(cls_id,ax_name,Axiom, 
18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

663 
lits',types_sorts,tvar_lits,tfree_lits) 
15347  664 
end; 
665 

666 

667 
(**** Isabelle arities ****) 

668 

669 
exception ARCLAUSE of string; 

670 

671 
type class = string; 

672 
type tcons = string; 

673 

674 
datatype arLit = TConsLit of bool * (class * tcons * string list)  TVarLit of bool * (class * string); 

675 

676 
datatype arityClause = 

677 
ArityClause of {clause_id: clause_id, 

17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

678 
axiom_name: axiom_name, 
15347  679 
kind: kind, 
680 
conclLit: arLit, 

681 
premLits: arLit list}; 

682 

683 

18798  684 
fun gen_TVars 0 = [] 
685 
 gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n1); 

15347  686 

18411
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

687 
fun pack_sort(_,[]) = [] 
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

688 
 pack_sort(tvar, "HOL.type"::srt) = pack_sort(tvar, srt) (*IGNORE sort "type"*) 
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

689 
 pack_sort(tvar, cls::srt) = (make_type_class cls, tvar) :: pack_sort(tvar, srt); 
15347  690 

691 
fun make_TVarLit (b,(cls,str)) = TVarLit(b,(cls,str)); 

692 
fun make_TConsLit (b,(cls,tcons,tvars)) = TConsLit(b,(make_type_class cls,make_fixed_type_const tcons,tvars)); 

693 

18411
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

694 
(*Arity of type constructor tcon :: (arg1,...,argN)res*) 
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

695 
fun make_axiom_arity_clause (tcons, n, (res,args)) = 
17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

696 
let val nargs = length args 
18798  697 
val tvars = gen_TVars nargs 
17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

698 
val tvars_srts = ListPair.zip (tvars,args) 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

699 
val tvars_srts' = union_all(map pack_sort tvars_srts) 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

700 
val false_tvars_srts' = map (pair false) tvars_srts' 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

701 
in 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

702 
ArityClause {clause_id = n, kind = Axiom, 
18411
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

703 
axiom_name = lookup_type_const tcons, 
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

704 
conclLit = make_TConsLit(true, (res,tcons,tvars)), 
17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

705 
premLits = map make_TVarLit false_tvars_srts'} 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

706 
end; 
15347  707 

18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

708 
(*The number of clauses generated from cls, including type clauses. It's always 1 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

709 
except for conjecture clauses.*) 
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset

710 
fun num_of_clauses (Clause cls) = 
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset

711 
let val num_tfree_lits = 
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset

712 
if !keep_types then length (#tfree_type_literals cls) 
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset

713 
else 0 
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset

714 
in 1 + num_tfree_lits end; 
15347  715 

716 

717 
(**** Isabelle class relations ****) 

718 

719 
datatype classrelClause = 

720 
ClassrelClause of {clause_id: clause_id, 

721 
subclass: class, 

18411
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

722 
superclass: class}; 
17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

723 

1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

724 
fun make_axiom_classrelClause n subclass superclass = 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

725 
ClassrelClause {clause_id = n, 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

726 
subclass = subclass, superclass = superclass}; 
15347  727 

17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

728 
fun classrelClauses_of_aux n sub [] = [] 
18411
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

729 
 classrelClauses_of_aux n sub ("HOL.type"::sups) = (*Should be ignored*) 
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

730 
classrelClauses_of_aux n sub sups 
17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

731 
 classrelClauses_of_aux n sub (sup::sups) = 
18411
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

732 
ClassrelClause {clause_id = n, subclass = sub, superclass = sup} 
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

733 
:: classrelClauses_of_aux (n+1) sub sups; 
15347  734 

18411
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

735 
fun classrelClauses_of (sub,sups) = classrelClauses_of_aux 0 sub sups; 
17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

736 

1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

737 

1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

738 
(***** Isabelle arities *****) 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

739 

1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

740 
fun arity_clause _ (tcons, []) = [] 
18411
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

741 
 arity_clause n (tcons, ("HOL.type",_)::ars) = (*Should be ignored*) 
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

742 
arity_clause n (tcons,ars) 
17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

743 
 arity_clause n (tcons, ar::ars) = 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

744 
make_axiom_arity_clause (tcons,n,ar) :: 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

745 
arity_clause (n+1) (tcons,ars); 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

746 

1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

747 
fun multi_arity_clause [] = [] 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

748 
 multi_arity_clause (tcon_ar :: tcons_ars) = 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

749 
arity_clause 0 tcon_ar @ multi_arity_clause tcons_ars 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

750 

1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

751 
fun arity_clause_thy thy = 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

752 
let val arities = #arities (Type.rep_tsig (Sign.tsig_of thy)) 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

753 
in multi_arity_clause (Symtab.dest arities) end; 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

754 

1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

755 

1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

756 
(* Isabelle classes *) 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

757 

1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

758 
type classrelClauses = classrelClause list Symtab.table; 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

759 

1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

760 
val classrel_of = #2 o #classes o Type.rep_tsig o Sign.tsig_of; 
18798  761 

762 
fun classrel_clauses_classrel (C: Sorts.classes) = 

763 
map classrelClauses_of (Graph.dest C); 

764 

17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

765 
val classrel_clauses_thy = List.concat o classrel_clauses_classrel o classrel_of; 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

766 

15347  767 

768 
fun wrap_eq_type typ t = eq_typ_wrapper ^"(" ^ t ^ "," ^ typ ^ ")"; 

769 

18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

770 
(*Only need to wrap equality's arguments with "typeinfo" if the output clauses are typed 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

771 
and if we specifically ask for types to be included. *) 
15347  772 
fun string_of_equality (typ,terms) = 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

773 
let val [tstr1,tstr2] = map string_of_term terms 
18402
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

774 
val typ' = string_of_fol_type typ 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

775 
in 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

776 
if !keep_types andalso !special_equal 
18402
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

777 
then "equal(" ^ (wrap_eq_type typ' tstr1) ^ "," ^ 
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

778 
(wrap_eq_type typ' tstr2) ^ ")" 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

779 
else "equal(" ^ tstr1 ^ "," ^ tstr2 ^ ")" 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

780 
end 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

781 
and string_of_term (UVar(x,_)) = x 
18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

782 
 string_of_term (Fun("equal",[typ],terms)) = string_of_equality(typ,terms) 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

783 
 string_of_term (Fun (name,typs,[])) = name (*Overloaded consts like 0 don't get types!*) 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

784 
 string_of_term (Fun (name,typs,terms)) = 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

785 
let val terms_as_strings = map string_of_term terms 
18402
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

786 
val typs' = if !keep_types then map string_of_fol_type typs else [] 
18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

787 
in name ^ (paren_pack (terms_as_strings @ typs')) end; 
15347  788 

789 
(* before output the string of the predicate, check if the predicate corresponds to an equality or not. *) 

18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

790 
fun string_of_predicate (Predicate("equal",[typ],terms)) = string_of_equality(typ,terms) 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

791 
 string_of_predicate (Predicate(name,typs,terms)) = 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

792 
let val terms_as_strings = map string_of_term terms 
18402
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

793 
val typs' = if !keep_types then map string_of_fol_type typs else [] 
18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

794 
in name ^ (paren_pack (terms_as_strings @ typs')) end; 
17317
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

795 

3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

796 
fun string_of_clausename (cls_id,ax_name) = 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

797 
clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id; 
17317
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

798 

3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

799 
fun string_of_type_clsname (cls_id,ax_name,idx) = 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

800 
string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx); 
18863  801 

802 
(*Write a list of strings to a file*) 

803 
fun writeln_strs os = List.app (fn s => TextIO.output (os,s)); 

804 

17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

805 

ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

806 

ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

807 
(********************************) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

808 
(* Code for producing DFG files *) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

809 
(********************************) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

810 

18863  811 
(*Attach sign in DFG syntax: false means negate.*) 
812 
fun dfg_sign true s = s 

813 
 dfg_sign false s = "not(" ^ s ^ ")" 

814 

815 
fun dfg_literal (Literal(pol,pred,tag)) = dfg_sign pol (string_of_predicate pred) 

17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

816 

18798  817 
fun dfg_of_typeLit (LTVar (s,ty)) = "not(" ^ s ^ "(" ^ ty ^ "))" 
18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

818 
 dfg_of_typeLit (LTFree (s,ty)) = s ^ "(" ^ ty ^ ")"; 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

819 

17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

820 
(*Make the string of universal quantifiers for a clause*) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

821 
fun forall_open ([],[]) = "" 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

822 
 forall_open (vars,tvars) = "forall([" ^ (commas (tvars@vars))^ "],\n" 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

823 

17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

824 
fun forall_close ([],[]) = "" 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

825 
 forall_close (vars,tvars) = ")" 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

826 

17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

827 
fun gen_dfg_cls (cls_id,ax_name,knd,lits,tvars,vars) = 
17317
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

828 
"clause( %(" ^ knd ^ ")\n" ^ forall_open(vars,tvars) ^ 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

829 
"or(" ^ lits ^ ")" ^ forall_close(vars,tvars) ^ ",\n" ^ 
18863  830 
string_of_clausename (cls_id,ax_name) ^ ").\n\n"; 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

831 

18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

832 
(*FIXME: UNUSED*) 
17317
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

833 
fun gen_dfg_type_cls (cls_id,ax_name,knd,tfree_lit,idx,tvars,vars) = 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

834 
"clause( %(" ^ knd ^ ")\n" ^ forall_open(vars,tvars) ^ 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

835 
"or( " ^ tfree_lit ^ ")" ^ forall_close(vars,tvars) ^ ",\n" ^ 
18863  836 
string_of_type_clsname (cls_id,ax_name,idx) ^ ").\n\n"; 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

837 

ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

838 
fun dfg_clause_aux (Clause cls) = 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

839 
let val lits = map dfg_literal (#literals cls) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

840 
val tvar_lits_strs = 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

841 
if !keep_types then map dfg_of_typeLit (#tvar_type_literals cls) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

842 
else [] 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

843 
val tfree_lits = 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

844 
if !keep_types then map dfg_of_typeLit (#tfree_type_literals cls) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

845 
else [] 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

846 
in 
17234  847 
(tvar_lits_strs @ lits, tfree_lits) 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

848 
end; 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

849 

ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

850 

ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

851 
fun dfg_folterms (Literal(pol,pred,tag)) = 
18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

852 
let val Predicate (_, _, folterms) = pred 
18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

853 
in folterms end 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

854 

17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

855 
fun get_uvars (UVar(a,typ)) = [a] 
17775  856 
 get_uvars (Fun (_,typ,tlist)) = union_all(map get_uvars tlist) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

857 

17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

858 
fun is_uvar (UVar _) = true 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

859 
 is_uvar (Fun _) = false; 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

860 

d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

861 
fun uvar_name (UVar(a,_)) = a 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

862 
 uvar_name (Fun (a,_,_)) = raise CLAUSE("Not a variable", Const(a,dummyT)); 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

863 

17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

864 
fun dfg_vars (Clause cls) = 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

865 
let val lits = #literals cls 
18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

866 
val folterms = List.concat (map dfg_folterms lits) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

867 
in 
17775  868 
union_all(map get_uvars folterms) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

869 
end 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

870 

18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

871 
fun string_of_predname (Predicate("equal",_,terms)) = "EQUALITY" 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

872 
 string_of_predname (Predicate(name,_,terms)) = name 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

873 

17234  874 
fun dfg_pred (Literal(pol,pred,tag)) ax_name = 
875 
(string_of_predname pred) ^ " " ^ ax_name 

17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

876 

18798  877 
fun clause2dfg (cls as Clause{axiom_name,clause_id,kind,types_sorts,...}) = 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

878 
let val (lits,tfree_lits) = dfg_clause_aux cls 
18798  879 
(*"lits" includes the typing assumptions (TVars)*) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

880 
val vars = dfg_vars cls 
18798  881 
val tvars = get_tvar_strs types_sorts 
882 
val knd = name_of_kind kind 

17234  883 
val lits_str = commas lits 
18798  884 
val cls_str = gen_dfg_cls(clause_id,axiom_name,knd,lits_str,tvars,vars) 
885 
in (cls_str, tfree_lits) end; 

17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

886 

18798  887 
fun string_of_arity (name, num) = "(" ^ name ^ "," ^ Int.toString num ^ ")" 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

888 

18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

889 
fun string_of_preds [] = "" 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

890 
 string_of_preds preds = "predicates[" ^ commas(map string_of_arity preds) ^ "].\n"; 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

891 

18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

892 
fun string_of_funcs [] = "" 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

893 
 string_of_funcs funcs = "functions[" ^ commas(map string_of_arity funcs) ^ "].\n" ; 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

894 

17234  895 
fun string_of_symbols predstr funcstr = 
896 
"list_of_symbols.\n" ^ predstr ^ funcstr ^ "end_of_list.\n\n"; 

17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

897 

18863  898 
fun write_axioms (out, strs) = 
899 
(TextIO.output (out, "list_of_clauses(axioms,cnf).\n"); 

900 
writeln_strs out strs; 

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

17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

902 

18863  903 
fun write_conjectures (out, strs) = 
904 
(TextIO.output (out, "list_of_clauses(conjectures,cnf).\n"); 

905 
writeln_strs out strs; 

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

17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

907 

18798  908 
fun string_of_start name = "begin_problem(" ^ name ^ ").\n\n"; 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

909 

18863  910 
fun string_of_descrip name = 
911 
"list_of_descriptions.\nname({*" ^ name ^ "*}).\nauthor({*Isabelle*}).\nstatus(unknown).\ndescription({*autogenerated*}).\nend_of_list.\n\n" 

17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

912 

18863  913 
fun dfg_tfree_clause tfree_lit = 
914 
"clause( %(conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ").\n\n" 

915 

18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

916 

4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

917 
(*** Find all occurrences of predicates in types, terms, literals... ***) 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

918 

4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

919 
(*FIXME: multiplearity checking doesn't work, as update_new is the wrong 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

920 
function (it flags repeated declarations of a function, even with the same arity)*) 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

921 

4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

922 
fun update_many (tab, keypairs) = foldl (uncurry Symtab.update) tab keypairs; 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

923 

4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

924 
fun add_predicate_preds (Predicate(pname,tys,tms), preds) = 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

925 
if pname = "equal" then preds (*equality is builtin and requires no declaration*) 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

926 
else Symtab.update (pname, length tys + length tms) preds 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

927 

4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

928 
fun add_literal_preds (Literal(_,pred,_), preds) = add_predicate_preds (pred,preds) 
18798  929 

18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

930 
fun add_type_sort_preds ((FOLTVar indx,s), preds) = 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

931 
update_many (preds, map pred_of_sort (sorts_on_typs (FOLTVar indx, s))) 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

932 
 add_type_sort_preds ((FOLTFree x,s), preds) = 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

933 
update_many (preds, map pred_of_sort (sorts_on_typs (FOLTFree x, s))); 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

934 

4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

935 
fun add_clause_preds (Clause {literals, types_sorts, ...}, preds) = 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

936 
foldl add_literal_preds (foldl add_type_sort_preds preds types_sorts) literals 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

937 
handle Symtab.DUP a => raise ERROR ("predicate " ^ a ^ " has multiple arities") 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

938 

4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

939 
val preds_of_clauses = Symtab.dest o (foldl add_clause_preds Symtab.empty) 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

940 

4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

941 

4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

942 
(*** Find all occurrences of functions in types, terms, literals... ***) 
18798  943 

944 
fun add_foltype_funcs (AtomV _, funcs) = funcs 

18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

945 
 add_foltype_funcs (AtomF a, funcs) = Symtab.update (a,0) funcs 
18798  946 
 add_foltype_funcs (Comp(a,tys), funcs) = 
18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

947 
foldl add_foltype_funcs (Symtab.update (a, length tys) funcs) tys; 
18798  948 

949 
fun add_folterm_funcs (UVar _, funcs) = funcs 

18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

950 
 add_folterm_funcs (Fun(a,tys,[]), funcs) = Symtab.update (a,0) funcs 
18798  951 
(*A constant is a special case: it has no type argument even if overloaded*) 
952 
 add_folterm_funcs (Fun(a,tys,tms), funcs) = 

953 
foldl add_foltype_funcs 

18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

954 
(foldl add_folterm_funcs (Symtab.update (a, length tys + length tms) funcs) 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

955 
tms) 
18798  956 
tys 
957 

958 
fun add_predicate_funcs (Predicate(_,tys,tms), funcs) = 

959 
foldl add_foltype_funcs (foldl add_folterm_funcs funcs tms) tys; 

960 

961 
fun add_literal_funcs (Literal(_,pred,_), funcs) = add_predicate_funcs (pred,funcs) 

962 

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

18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

964 
foldl add_literal_funcs funcs literals 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

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

18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

967 
val funcs_of_clauses = Symtab.dest o (foldl add_clause_funcs Symtab.empty) 
18798  968 

17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

969 
fun string_of_arClauseID (ArityClause {clause_id,axiom_name,...}) = 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

970 
arclause_prefix ^ ascii_of axiom_name ^ "_" ^ Int.toString clause_id; 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

971 

ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

972 
fun string_of_arKind (ArityClause arcls) = name_of_kind(#kind arcls); 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

973 

18863  974 
fun dfg_of_arLit (TConsLit(pol,(c,t,args))) = 
975 
dfg_sign pol (c ^ "(" ^ t ^ paren_pack args ^ ")") 

976 
 dfg_of_arLit (TVarLit(pol,(c,str))) = 

977 
dfg_sign pol (c ^ "(" ^ str ^ ")") 

17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

978 

ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

979 
fun dfg_of_conclLit (ArityClause arcls) = dfg_of_arLit (#conclLit arcls); 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

980 

ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

981 
fun dfg_of_premLits (ArityClause arcls) = map dfg_of_arLit (#premLits arcls); 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

982 

18863  983 
fun dfg_classrelLits sub sup = 
984 
let val tvar = "(T)" 

985 
in 

986 
"not(" ^ sub ^ tvar ^ "), " ^ sup ^ tvar 

987 
end; 

17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

988 

18863  989 
fun dfg_classrelClause (ClassrelClause {clause_id,subclass,superclass,...}) = 
990 
let val relcls_id = clrelclause_prefix ^ ascii_of subclass ^ "_" ^ 

991 
Int.toString clause_id 

992 
val lits = dfg_classrelLits (make_type_class subclass) (make_type_class superclass) 

993 
in 

994 
"clause(\nor( " ^ lits ^ ")),\n" ^ 

995 
relcls_id ^ ").\n\n" 

996 
end; 

17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

997 

ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

998 
fun dfg_arity_clause arcls = 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

999 
let val arcls_id = string_of_arClauseID arcls 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1000 
val concl_lit = dfg_of_conclLit arcls 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1001 
val prems_lits = dfg_of_premLits arcls 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1002 
val knd = string_of_arKind arcls 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1003 
val all_lits = concl_lit :: prems_lits 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1004 
in 
18863  1005 
"clause( %(" ^ knd ^ ")\n" ^ "or( " ^ bracket_pack all_lits ^ ")),\n" ^ 
1006 
arcls_id ^ ").\n\n" 

1007 
end; 

1008 

1009 
(* write out a subgoal in DFG format to the file "xxxx_N"*) 

1010 
fun dfg_write_file ths filename (axclauses,classrel_clauses,arity_clauses) = 

1011 
let 

1012 
val conjectures = make_conjecture_clauses (map prop_of ths) 

1013 
val (dfg_clss,tfree_litss) = ListPair.unzip (map clause2dfg conjectures) 

1014 
val classrel_cls = map dfg_classrelClause classrel_clauses 

1015 
val arity_cls = map dfg_arity_clause arity_clauses 

1016 
val clss = conjectures @ axclauses 

1017 
val funcs = (funcs_of_clauses clss) 

1018 
and preds = (preds_of_clauses clss) 

1019 
val out = TextIO.openOut filename 

1020 
and probname = Path.pack (Path.base (Path.unpack filename)) 

1021 
val axstrs_tfrees = (map clause2dfg axclauses) 

1022 
val (axstrs, _) = ListPair.unzip axstrs_tfrees 

1023 
val tfree_clss = map dfg_tfree_clause (union_all tfree_litss) 

1024 
val funcstr = string_of_funcs funcs 

1025 
val predstr = string_of_preds preds 

1026 
in 

1027 
TextIO.output (out, string_of_start probname); 

1028 
TextIO.output (out, string_of_descrip probname); 

1029 
TextIO.output (out, string_of_symbols funcstr predstr); 

1030 
write_axioms (out, axstrs); 

1031 
write_conjectures (out, tfree_clss@dfg_clss); 

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

1033 
TextIO.closeOut out 

17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1034 
end; 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1035 

ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1036 

ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1037 
(********************************) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1038 
(* code to produce TPTP files *) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1039 
(********************************) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1040 

15347  1041 
fun tptp_literal (Literal(pol,pred,tag)) = 
1042 
let val pred_string = string_of_predicate pred 

17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1043 
val tagged_pol = 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1044 
if (tag andalso !tagged) then (if pol then "+++" else "") 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1045 
else (if pol then "++" else "") 
15347  1046 
in 
1047 
tagged_pol ^ pred_string 

1048 
end; 

1049 

18798  1050 
fun tptp_of_typeLit (LTVar (s,ty)) = "" ^ s ^ "(" ^ ty ^ ")" 
1051 
 tptp_of_typeLit (LTFree (s,ty)) = "++" ^ s ^ "(" ^ ty ^ ")"; 

15347  1052 

1053 

1054 
fun gen_tptp_cls (cls_id,ax_name,knd,lits) = 

17317
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

1055 
"input_clause(" ^ string_of_clausename (cls_id,ax_name) ^ "," ^ 
18863  1056 
knd ^ "," ^ lits ^ ").\n"; 
15347  1057 

17317
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

1058 
fun gen_tptp_type_cls (cls_id,ax_name,knd,tfree_lit,idx) = 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

1059 
"input_clause(" ^ string_of_type_clsname (cls_id,ax_name,idx) ^ "," ^ 
18863  1060 
knd ^ ",[" ^ tfree_lit ^ "]).\n"; 
15347  1061 

17422  1062 
fun tptp_type_lits (Clause cls) = 
15347  1063 
let val lits = map tptp_literal (#literals cls) 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1064 
val tvar_lits_strs = 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1065 
if !keep_types 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1066 
then (map tptp_of_typeLit (#tvar_type_literals cls)) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1067 
else [] 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1068 
val tfree_lits = 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1069 
if !keep_types 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1070 
then (map tptp_of_typeLit (#tfree_type_literals cls)) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1071 
else [] 
15347  1072 
in 
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset

1073 
(tvar_lits_strs @ lits, tfree_lits) 
15347  1074 
end; 
1075 

1076 
fun tptp_clause cls = 

17422  1077 
let val (lits,tfree_lits) = tptp_type_lits cls 
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset

1078 
(*"lits" includes the typing assumptions (TVars)*) 
17317
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

1079 
val cls_id = get_clause_id cls 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

1080 
val ax_name = get_axiomName cls 
15347  1081 
val knd = string_of_kind cls 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1082 
val lits_str = bracket_pack lits 
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset

1083 
val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) 
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset

1084 
fun typ_clss k [] = [] 
15347  1085 
 typ_clss k (tfree :: tfrees) = 
17317
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

1086 
gen_tptp_type_cls(cls_id,ax_name,knd,tfree,k) :: 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

1087 
typ_clss (k+1) tfrees 
15347  1088 
in 
1089 
cls_str :: (typ_clss 0 tfree_lits) 

1090 
end; 

1091 

15608  1092 
fun clause2tptp cls = 
17422  1093 
let val (lits,tfree_lits) = tptp_type_lits cls 
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset

1094 
(*"lits" includes the typing assumptions (TVars)*) 
17317
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

1095 
val cls_id = get_clause_id cls 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

1096 
val ax_name = get_axiomName cls 
15608  1097 
val knd = string_of_kind cls 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1098 
val lits_str = bracket_pack lits 
15608  1099 
val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) 
1100 
in 

1101 
(cls_str,tfree_lits) 

1102 
end; 

1103 

1104 

18863  1105 
fun tptp_tfree_clause tfree_lit = 
1106 
"input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "]).\n"; 

15608  1107 

15347  1108 

17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1109 
fun tptp_of_arLit (TConsLit(b,(c,t,args))) = 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1110 
let val pol = if b then "++" else "" 
18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

1111 
val arg_strs = paren_pack args 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1112 
in 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1113 
pol ^ c ^ "(" ^ t ^ arg_strs ^ ")" 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1114 
end 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1115 
 tptp_of_arLit (TVarLit(b,(c,str))) = 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1116 
let val pol = if b then "++" else "" 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1117 
in 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1118 
pol ^ c ^ "(" ^ str ^ ")" 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1119 
end; 
15347  1120 

1121 

17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1122 
fun tptp_of_conclLit (ArityClause arcls) = tptp_of_arLit (#conclLit arcls); 
15347  1123 

17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1124 
fun tptp_of_premLits (ArityClause arcls) = map tptp_of_arLit (#premLits arcls); 
15347  1125 

1126 
fun tptp_arity_clause arcls = 

1127 
let val arcls_id = string_of_arClauseID arcls 

17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1128 
val concl_lit = tptp_of_conclLit arcls 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1129 
val prems_lits = tptp_of_premLits arcls 
15347  1130 
val knd = string_of_arKind arcls 
1131 
val all_lits = concl_lit :: prems_lits 

1132 
in 

17317
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

1133 
"input_clause(" ^ arcls_id ^ "," ^ knd ^ "," ^ 
18863  1134 
(bracket_pack all_lits) ^ ").\n" 
15347  1135 
end; 
1136 

1137 
fun tptp_classrelLits sub sup = 

1138 
let val tvar = "(T)" 

1139 
in 

18411
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

1140 
"[" ^ sub ^ tvar ^ ",++" ^ sup ^ tvar ^ "]" 
15347  1141 
end; 
1142 

17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

1143 
fun tptp_classrelClause (ClassrelClause {clause_id,subclass,superclass,...}) = 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

1144 
let val relcls_id = clrelclause_prefix ^ ascii_of subclass ^ "_" ^ 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

1145 
Int.toString clause_id 
18411
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

1146 
val lits = tptp_classrelLits (make_type_class subclass) (make_type_class superclass) 
15347  1147 
in 
18863  1148 
"input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ").\n" 
15347  1149 
end; 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1150 

18863  1151 
(* write out a subgoal as tptp clauses to the file "xxxx_N"*) 
1152 
fun tptp_write_file ths filename (axclauses,classrel_clauses,arity_clauses) = 

1153 
let 

1154 
val clss = make_conjecture_clauses (map prop_of ths) 

1155 
val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp clss) 

1156 
val tfree_clss = map tptp_tfree_clause (foldl (op union_string) [] tfree_litss) 

1157 
val classrel_cls = map tptp_classrelClause classrel_clauses 

1158 
val arity_cls = map tptp_arity_clause arity_clauses 

1159 
val out = TextIO.openOut filename 

1160 
in 

1161 
List.app (writeln_strs out o tptp_clause) axclauses; 

1162 
writeln_strs out tfree_clss; 

1163 
writeln_strs out tptp_clss; 

1164 
writeln_strs out classrel_cls; 

1165 
writeln_strs out arity_cls; 

1166 
TextIO.closeOut out 

1167 
end; 

1168 

1169 

15347  1170 
end; 