author  paulson 
Tue, 31 Jan 2006 16:37:06 +0100  
changeset 18868  7cfc21ee0370 
parent 18863  a113b6839df1 
child 18869  00741f7280f7 
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 

9 
signature RES_CLAUSE = 

10 
sig 

18868  11 
exception CLAUSE of string * term 
12 
type clause and arityClause and classrelClause 

13 
type fol_type 

14 
type typ_var 

15 
type type_literal 

16 
val add_typs_aux : (typ_var * string list) list > type_literal list * type_literal list 

17 
val arity_clause_thy: theory > arityClause list 

18 
val ascii_of : string > string 

19 
val bracket_pack : string list > string 

20 
val check_var_pairs: ''a * ''b > (''a * ''b) list > int 

21 
val classrel_clauses_thy: theory > classrelClause list 

22 
val clause_eq : clause * clause > bool 

23 
val clause_prefix : string 

24 
val clause2tptp : clause > string * string list 

25 
val const_prefix : string 

26 
val dfg_write_file: thm list > string > (clause list * classrelClause list * arityClause list) > unit 

27 
val fixed_var_prefix : string 

28 
val gen_tptp_cls : int * string * string * string > string 

29 
val gen_tptp_type_cls : int * string * string * string * int > string 

30 
val get_axiomName : clause > string 

31 
val hash_clause : clause > int 

32 
val init : theory > unit 

33 
val isMeta : string > bool 

34 
val isTaut : clause > bool 

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

35 
val keep_types : bool ref 
18868  36 
val list_ord : ('a * 'b > order) > 'a list * 'b list > order 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

37 
val make_axiom_clause : Term.term > string * int > clause 
17888  38 
val make_conjecture_clauses : term list > clause list 
18868  39 
val make_fixed_const : string > string 
40 
val make_fixed_type_const : string > string 

41 
val make_fixed_type_var : string > string 

42 
val make_fixed_var : string > string 

43 
val make_schematic_type_var : string * int > string 

44 
val make_schematic_var : string * int > string 

45 
val make_type_class : string > string 

46 
val mk_fol_type: string * string * fol_type list > fol_type 

47 
val mk_typ_var_sort : Term.typ > typ_var * sort 

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

48 
val num_of_clauses : clause > int 
18868  49 
val paren_pack : string list > string 
50 
val schematic_var_prefix : string 

51 
val special_equal : bool ref 

52 
val string_of_fol_type : fol_type > string 

53 
val tconst_prefix : string 

54 
val tfree_prefix : string 

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

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

56 
val tptp_classrelClause : classrelClause > string 
18868  57 
val tptp_of_typeLit : type_literal > string 
18863  58 
val tptp_tfree_clause : string > string 
18868  59 
val tptp_write_file: thm list > string > (clause list * classrelClause list * arityClause list) > unit 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

60 
val tvar_prefix : string 
18868  61 
val types_eq: fol_type list * fol_type list > (string*string) list * (string*string) list > bool * ((string*string) list * (string*string) list) 
62 
val types_ord : fol_type list * fol_type list > order 

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

63 
val union_all : ''a list list > ''a list 
18863  64 
val writeln_strs: TextIO.outstream > TextIO.vector list > unit 
15347  65 
end; 
66 

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

67 
structure ResClause : RES_CLAUSE = 
15347  68 
struct 
69 

70 
(* Added for typed equality *) 

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

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

73 

74 

75 
val schematic_var_prefix = "V_"; 

76 
val fixed_var_prefix = "v_"; 

77 

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

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

79 
val tfree_prefix = "t_"; 
15347  80 

81 
val clause_prefix = "cls_"; 

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

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

83 
val clrelclause_prefix = "clsrel_"; 
15347  84 

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

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

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

87 
val class_prefix = "class_"; 
15347  88 

17775  89 
fun union_all xss = foldl (op union) [] xss; 
90 

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

15347  92 
val const_trans_table = 
93 
Symtab.make [("op =", "equal"), 

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

95 
("op <", "less"), 

96 
("op &", "and"), 

97 
("op ", "or"), 

17375  98 
("op +", "plus"), 
99 
("op ", "minus"), 

100 
("op *", "times"), 

18676  101 
("Divides.op div", "div"), 
102 
("HOL.divide", "divide"), 

15347  103 
("op >", "implies"), 
17375  104 
("{}", "emptyset"), 
15347  105 
("op :", "in"), 
106 
("op Un", "union"), 

18390  107 
("op Int", "inter"), 
108 
("List.op @", "append")]; 

15347  109 

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

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

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

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

113 
("~=>", "map")]; 
15347  114 

15610  115 
(*Escaping of special characters. 
116 
Alphanumeric characters are left unchanged. 

117 
The character _ goes to __ 

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

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

120 
local 

121 

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

123 

15347  124 
fun ascii_of_c c = 
15610  125 
if Char.isAlphaNum c then String.str c 
126 
else if c = #"_" then "__" 

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

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

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

130 
else "" 

15347  131 

15610  132 
in 
133 

134 
val ascii_of = String.translate ascii_of_c; 

135 

136 
end; 

15347  137 

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

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

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

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

141 

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

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

143 

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

144 

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

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

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

147 
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

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

149 

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

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

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

153 
fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v); 
15347  154 
fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x); 
155 

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

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

157 
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

158 
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); 
15347  159 

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

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

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

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

164 

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

165 
fun lookup_type_const c = 
17412  166 
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

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

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

169 

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

170 
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

171 
 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

172 

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

173 
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

174 

17261  175 
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

176 

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

177 

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

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

180 
val keep_types = ref true; 
15347  181 

182 
datatype kind = Axiom  Hypothesis  Conjecture; 

183 
fun name_of_kind Axiom = "axiom" 

184 
 name_of_kind Hypothesis = "hypothesis" 

185 
 name_of_kind Conjecture = "conjecture"; 

186 

187 
type clause_id = int; 

188 
type axiom_name = string; 

189 

190 

191 
type polarity = bool; 

192 

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

194 
type tag = bool; 

195 

196 

197 
(**** Isabelle FOL clauses ****) 

198 

199 
val tagged = ref false; 

200 

201 
type pred_name = string; 

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

202 

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

203 
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

204 

18798  205 
(*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

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

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

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

209 

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

210 
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

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

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

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

214 

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

215 
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

216 
 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

217 
 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

218 

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

219 

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

15347  222 

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

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

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

225 
datatype predicate = Predicate of pred_name * fol_type list * fol_term list; 
15347  226 

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

228 

17999  229 
fun mk_typ_var_sort (TFree(a,s)) = (FOLTFree a,s) 
230 
 mk_typ_var_sort (TVar(v,s)) = (FOLTVar v,s); 

231 

232 

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

233 
(*A clause has firstorder literals and other, typerelated literals*) 
15347  234 
datatype clause = 
235 
Clause of {clause_id: clause_id, 

236 
axiom_name: axiom_name, 

237 
kind: kind, 

238 
literals: literal list, 

239 
types_sorts: (typ_var * sort) list, 

240 
tvar_type_literals: type_literal list, 

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

241 
tfree_type_literals: type_literal list}; 
15347  242 

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

243 
exception CLAUSE of string * term; 
15347  244 

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

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

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

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

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

249 

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

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

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

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

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

254 

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

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

256 

17234  257 
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

258 
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

259 
if forall isFalse literals 
17234  260 
then error "Problem too trivial for resolution (empty clause)" 
261 
else 

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

262 
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

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

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

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

266 

15347  267 

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

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

269 

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

270 
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

271 

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

272 
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

273 

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

274 
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

275 

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

276 

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

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

278 
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

279 

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

280 
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

281 

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

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

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

284 
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

285 

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

286 

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

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

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

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

291 
val t = make_fixed_type_const a 
18798  292 
in (Comp(t,folTyps), ts) end 
293 
 type_of (TFree (a,s)) = (AtomF(make_fixed_type_var a), [(FOLTFree a, s)]) 

294 
 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

295 
and types_of Ts = 
18798  296 
let val (folTyps,ts) = ListPair.unzip (map type_of Ts) 
297 
in (folTyps, union_all ts) end; 

15390  298 

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

299 

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

300 
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

301 

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

304 
val isMeta = String.isPrefix "METAHYP1_" 

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

305 

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

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

310 
 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

311 
 pred_name_type t = raise CLAUSE("Predicate input unexpected", t); 
15347  312 

15615  313 

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

314 
(* For typed equality *) 
15615  315 
(* here "arg_typ" is the type of "="'s argument's type, not the type of the equality *) 
316 
(* Find type of equality arg *) 

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

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

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

319 
in folT end; 
15347  320 

18798  321 
fun fun_name_type (Const(c,T)) args = (make_fixed_const c, const_types_of (c,T)) 
322 
 fun_name_type (Free(x,T)) args = 

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

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

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

325 
 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

326 

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

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

328 
TVars it contains.*) 
15347  329 
fun term_of (Var(ind_nm,T)) = 
18798  330 
let val (folType,ts) = type_of T 
331 
in (UVar(make_schematic_var ind_nm, folType), ts) end 

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

334 
in 
18798  335 
if isMeta x then (UVar(make_schematic_var(x,0),folType), ts) 
336 
else (Fun(make_fixed_var x, [folType], []), ts) 

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

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

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

339 
let val (f,args) = strip_comb app 
18798  340 
val (funName,(contys,ts1)) = fun_name_type f args 
341 
val (args',ts2) = terms_of args 

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

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

344 
end 
18798  345 
and terms_of ts = ListPair.unzip (map term_of ts) 
15390  346 

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

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

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

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

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

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

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

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

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

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

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

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

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

361 
end; 
15347  362 

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

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

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

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

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

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

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

369 
(pred_of (strip_comb term), polarity, tag); 
15347  370 

17888  371 
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

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

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

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

375 
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

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

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

380 

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

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

382 

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

383 

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

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

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

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

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

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

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

390 
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

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

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

393 

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

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

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

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

397 
 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

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

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

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

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

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

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

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

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

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

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

408 

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

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

410 
 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

411 

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

412 

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

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

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

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

416 
 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

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

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

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

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

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

422 

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

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

424 

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

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

426 
 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

427 

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

428 

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

429 

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

430 
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

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

432 
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

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

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

435 

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

436 

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

437 
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

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

439 
 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

440 

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

441 
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

442 

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

443 

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

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

445 

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

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

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

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

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

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

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

452 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

468 

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

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

470 

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

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

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

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

474 
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

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

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

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

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

479 

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

480 

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

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

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

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

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

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

486 
 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

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

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

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

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

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

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

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

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

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

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

497 

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

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

499 

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

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

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

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

503 
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

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

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

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

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

508 

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

509 

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

510 
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

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

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

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

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

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

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

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

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

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

520 

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

521 

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

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

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

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

525 

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

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

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

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

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

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

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

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

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

534 

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

535 

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

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

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

539 

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

540 

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

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

542 

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

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

544 

18449  545 
fun hashw_term (UVar(_,_), w) = w 
546 
 hashw_term (Fun(f,tps,args), w) = 

547 
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

548 

18449  549 
fun hashw_pred (Predicate(pn,_,args), w) = 
550 
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

551 

18449  552 
fun hash1_literal (Literal(true,pred,_)) = hashw_pred (pred, 0w0) 
553 
 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

554 

18798  555 
fun hash_clause (Clause{literals,...}) = 
556 
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

557 

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

558 

18798  559 
(*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

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

561 
 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

562 
sorts_on_typs (v,s) (*IGNORE sort "type"*) 
18798  563 
 sorts_on_typs ((FOLTVar indx), s::ss) = 
564 
LTVar(make_type_class s, make_schematic_type_var indx) :: 

565 
sorts_on_typs ((FOLTVar indx), ss) 

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

567 
LTFree(make_type_class s, make_fixed_type_var x) :: 

568 
sorts_on_typs ((FOLTFree x), ss); 

15347  569 

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

570 

18798  571 
fun pred_of_sort (LTVar (s,ty)) = (s,1) 
572 
 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

573 

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

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

575 
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

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

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

578 
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

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

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

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

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

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

584 
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

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

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

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

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

589 

17999  590 

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

591 
fun add_typs (Clause cls) = add_typs_aux (#types_sorts cls) 
15347  592 

593 

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

595 

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

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

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

598 
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

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

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

602 
 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

603 

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

604 
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

605 
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

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

607 
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

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

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

610 
lits',types_sorts,tvar_lits,tfree_lits) 
15347  611 
end; 
612 

613 

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

614 
(* check if a clause is FOL first*) 
17888  615 
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

616 
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

617 
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

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

619 
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

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

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

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

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

624 

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

625 
fun make_conjecture_clauses_aux _ [] = [] 
17888  626 
 make_conjecture_clauses_aux n (t::ts) = 
627 
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

628 

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

629 
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

630 

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

631 

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

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

633 
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

634 
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

635 
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

636 
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

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

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

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

641 
lits',types_sorts,tvar_lits,tfree_lits) 
15347  642 
end; 
643 

644 

645 
(**** Isabelle arities ****) 

646 

647 
exception ARCLAUSE of string; 

648 

649 
type class = string; 

650 
type tcons = string; 

651 

18868  652 
datatype arLit = TConsLit of bool * (class * tcons * string list) 
653 
 TVarLit of bool * (class * string); 

15347  654 

655 
datatype arityClause = 

656 
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

657 
axiom_name: axiom_name, 
15347  658 
kind: kind, 
659 
conclLit: arLit, 

660 
premLits: arLit list}; 

661 

662 

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

15347  665 

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

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

667 
 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

668 
 pack_sort(tvar, cls::srt) = (make_type_class cls, tvar) :: pack_sort(tvar, srt); 
15347  669 

18868  670 
fun make_TVarLit (b, (cls,str)) = TVarLit(b, (cls,str)); 
671 
fun make_TConsLit (b, (cls,tcons,tvars)) = 

672 
TConsLit(b, (make_type_class cls, make_fixed_type_const tcons, tvars)); 

15347  673 

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

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

675 
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

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

678 
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

679 
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

680 
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

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

682 
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

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

684 
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

685 
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

686 
end; 
15347  687 

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

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

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

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

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

692 
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

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

694 
in 1 + num_tfree_lits end; 
15347  695 

696 

697 
(**** Isabelle class relations ****) 

698 

699 
datatype classrelClause = 

18868  700 
ClassrelClause of {axiom_name: axiom_name, 
15347  701 
subclass: class, 
18411
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

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

703 

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

704 
fun make_axiom_classrelClause n subclass superclass = 
18868  705 
ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of subclass ^ 
706 
"_" ^ Int.toString n, 

707 
subclass = make_type_class subclass, 

708 
superclass = make_type_class superclass}; 

15347  709 

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

710 
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

711 
 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

712 
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

713 
 classrelClauses_of_aux n sub (sup::sups) = 
18868  714 
make_axiom_classrelClause n sub sup :: classrelClauses_of_aux (n+1) sub sups; 
15347  715 

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

716 
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

717 

18868  718 
val classrel_of = #2 o #classes o Type.rep_tsig o Sign.tsig_of; 
17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

719 

18868  720 
fun classrel_clauses_classrel (C: Sorts.classes) = 
721 
map classrelClauses_of (Graph.dest C); 

722 

723 
val classrel_clauses_thy = List.concat o classrel_clauses_classrel o classrel_of; 

724 

725 

726 
(** Isabelle arities **) 

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

727 

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

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

729 
 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

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

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

732 
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

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

734 

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

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

736 
 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

737 
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

738 

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

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

740 
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

741 
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

742 

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

743 

18868  744 
(**** Find occurrences of predicates in clauses ****) 
745 

746 
(*FIXME: multiplearity checking doesn't work, as update_new is the wrong 

747 
function (it flags repeated declarations of a function, even with the same arity)*) 

748 

749 
fun update_many (tab, keypairs) = foldl (uncurry Symtab.update) tab keypairs; 

750 

751 
fun add_predicate_preds (Predicate(pname,tys,tms), preds) = 

752 
if pname = "equal" then preds (*equality is builtin and requires no declaration*) 

753 
else Symtab.update (pname, length tys + length tms) preds 

754 

755 
fun add_literal_preds (Literal(_,pred,_), preds) = add_predicate_preds (pred,preds) 

756 

757 
fun add_type_sort_preds ((FOLTVar indx,s), preds) = 

758 
update_many (preds, map pred_of_sort (sorts_on_typs (FOLTVar indx, s))) 

759 
 add_type_sort_preds ((FOLTFree x,s), preds) = 

760 
update_many (preds, map pred_of_sort (sorts_on_typs (FOLTFree x, s))); 

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

761 

18868  762 
fun add_clause_preds (Clause {literals, types_sorts, ...}, preds) = 
763 
foldl add_literal_preds (foldl add_type_sort_preds preds types_sorts) literals 

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

765 

766 
fun add_classrelClause_preds (ClassrelClause {subclass,superclass,...}, preds) = 

767 
Symtab.update (subclass,1) (Symtab.update (superclass,1) preds); 

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

768 

18868  769 
fun add_arityClause_preds (ArityClause {conclLit,...}, preds) = 
770 
let val TConsLit(_, (tclass, _, _)) = conclLit 

771 
in Symtab.update (tclass,1) preds end; 

772 

773 
fun preds_of_clauses clauses clsrel_clauses arity_clauses = 

774 
Symtab.dest 

775 
(foldl add_classrelClause_preds 

776 
(foldl add_arityClause_preds 

777 
(foldl add_clause_preds Symtab.empty clauses) 

778 
arity_clauses) 

779 
clsrel_clauses) 

18798  780 

18868  781 
(*** Find occurrences of functions in clauses ***) 
782 

783 
fun add_foltype_funcs (AtomV _, funcs) = funcs 

784 
 add_foltype_funcs (AtomF a, funcs) = Symtab.update (a,0) funcs 

785 
 add_foltype_funcs (Comp(a,tys), funcs) = 

786 
foldl add_foltype_funcs (Symtab.update (a, length tys) funcs) tys; 

787 

788 
fun add_folterm_funcs (UVar _, funcs) = funcs 

789 
 add_folterm_funcs (Fun(a,tys,[]), funcs) = Symtab.update (a,0) funcs 

790 
(*A constant is a special case: it has no type argument even if overloaded*) 

791 
 add_folterm_funcs (Fun(a,tys,tms), funcs) = 

792 
foldl add_foltype_funcs 

793 
(foldl add_folterm_funcs (Symtab.update (a, length tys + length tms) funcs) 

794 
tms) 

795 
tys 

18798  796 

18868  797 
fun add_predicate_funcs (Predicate(_,tys,tms), funcs) = 
798 
foldl add_foltype_funcs (foldl add_folterm_funcs funcs tms) tys; 

799 

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

801 

802 
fun add_arityClause_funcs (ArityClause {conclLit,...}, funcs) = 

803 
let val TConsLit(_, (_, tcons, tvars)) = conclLit 

804 
in Symtab.update (tcons, length tvars) funcs end; 

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

805 

18868  806 
fun add_clause_funcs (Clause {literals, ...}, funcs) = 
807 
foldl add_literal_funcs funcs literals 

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

809 

810 
fun funcs_of_clauses clauses arity_clauses = 

811 
Symtab.dest (foldl add_arityClause_funcs 

812 
(foldl add_clause_funcs Symtab.empty clauses) 

813 
arity_clauses) 

814 

815 

816 
(**** Stringoriented operations ****) 

15347  817 

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

819 

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

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

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

823 
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

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

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

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

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

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

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

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

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

832 
 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

833 
 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

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

835 
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

836 
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

837 
in name ^ (paren_pack (terms_as_strings @ typs')) end; 
15347  838 

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

840 
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

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

842 
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

843 
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

844 
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

845 

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

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

847 
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

848 

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

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

850 
string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx); 
18863  851 

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

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

854 

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

855 

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

857 

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

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

861 

862 
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

863 

18798  864 
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

865 
 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

866 

18868  867 
(*Enclose the clause body by quantifiers, if necessary*) 
868 
fun dfg_forall [] body = body 

869 
 dfg_forall vars body = "forall([" ^ commas vars ^ "],\n" ^ body ^ ")" 

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

870 

18868  871 
fun gen_dfg_cls (cls_id, ax_name, knd, lits, vars) = 
872 
"clause( %(" ^ knd ^ ")\n" ^ 

873 
dfg_forall vars ("or(" ^ lits ^ ")") ^ ",\n" ^ 

18863  874 
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

875 

18868  876 
fun dfg_clause_aux (Clause{literals, tvar_type_literals, tfree_type_literals, ...}) = 
877 
let val lits = map dfg_literal literals 

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

878 
val tvar_lits_strs = 
18868  879 
if !keep_types then map dfg_of_typeLit tvar_type_literals 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

881 
val tfree_lits = 
18868  882 
if !keep_types then map dfg_of_typeLit tfree_type_literals 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

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

887 

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

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

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

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

891 

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

892 
fun get_uvars (UVar(a,typ)) = [a] 
18868  893 
 get_uvars (Fun (_,typ,tlist)) = union_all(map get_uvars tlist) 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

894 

18868  895 
fun dfg_vars (Clause {literals,...}) = 
896 
let val folterms = List.concat (map dfg_folterms literals) 

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

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

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

900 

18798  901 
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

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

904 
val vars = dfg_vars cls 
18798  905 
val tvars = get_tvar_strs types_sorts 
906 
val knd = name_of_kind kind 

17234  907 
val lits_str = commas lits 
18868  908 
val cls_str = gen_dfg_cls(clause_id, axiom_name, knd, lits_str, tvars@vars) 
18798  909 
in (cls_str, tfree_lits) end; 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

910 

18798  911 
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

912 

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

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

914 
 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

915 

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

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

917 
 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

918 

17234  919 
fun string_of_symbols predstr funcstr = 
920 
"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

921 

18798  922 
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

923 

18863  924 
fun string_of_descrip name = 
18868  925 
"list_of_descriptions.\nname({*" ^ name ^ 
926 
"*}).\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

927 

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

930 

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

931 
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

932 
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

933 

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

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

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

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

938 

18863  939 
fun dfg_classrelLits sub sup = 
940 
let val tvar = "(T)" 

941 
in 

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

943 
end; 

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

944 

18868  945 
fun dfg_classrelClause (ClassrelClause {axiom_name,subclass,superclass,...}) = 
946 
"clause(forall([T],\nor( " ^ dfg_classrelLits subclass superclass ^ ")),\n" ^ 

947 
axiom_name ^ ").\n\n"; 

948 

949 
fun dfg_arity_clause (arcls as ArityClause{kind,conclLit,premLits,...}) = 

950 
let val arcls_id = string_of_arClauseID arcls 

951 
val knd = name_of_kind kind 

952 
val TConsLit(_, (_,_,tvars)) = conclLit 

953 
val lits = map dfg_of_arLit (conclLit :: premLits) 

18863  954 
in 
18868  955 
"clause( %(" ^ knd ^ ")\n" ^ 
956 
dfg_forall tvars ("or( " ^ commas lits ^ ")") ^ ",\n" ^ 

957 
arcls_id ^ ").\n\n" 

18863  958 
end; 
959 

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

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

962 
let 

963 
val conjectures = make_conjecture_clauses (map prop_of ths) 

18868  964 
val (dfg_clss, tfree_litss) = ListPair.unzip (map clause2dfg conjectures) 
18863  965 
val clss = conjectures @ axclauses 
18868  966 
val funcs = funcs_of_clauses clss arity_clauses 
967 
and preds = preds_of_clauses clss classrel_clauses arity_clauses 

18863  968 
val out = TextIO.openOut filename 
969 
and probname = Path.pack (Path.base (Path.unpack filename)) 

18868  970 
val (axstrs, _) = ListPair.unzip (map clause2dfg axclauses) 
18863  971 
val tfree_clss = map dfg_tfree_clause (union_all tfree_litss) 
972 
in 

18868  973 
TextIO.output (out, string_of_start probname); 
974 
TextIO.output (out, string_of_descrip probname); 

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

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

977 
writeln_strs out axstrs; 

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

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

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

981 
writeln_strs out tfree_clss; 

982 
writeln_strs out dfg_clss; 

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

984 
TextIO.closeOut out 

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

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

986 

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

987 

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

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

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

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

991 

18868  992 

993 
(*Attach sign in TPTP syntax: false means negate.*) 

994 
fun tptp_sign true s = "++" ^ s 

995 
 tptp_sign false s = "" ^ s 

996 

997 
fun tptp_literal (Literal(pol,pred,tag)) = (*FIXME REMOVE TAGGING*) 

15347  998 
let val pred_string = string_of_predicate pred 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

1001 
else (if pol then "++" else "") 
15347  1002 
in 
1003 
tagged_pol ^ pred_string 

1004 
end; 

1005 

18798  1006 
fun tptp_of_typeLit (LTVar (s,ty)) = "" ^ s ^ "(" ^ ty ^ ")" 
1007 
 tptp_of_typeLit (LTFree (s,ty)) = "++" ^ s ^ "(" ^ ty ^ ")"; 

15347  1008 

1009 

1010 
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

1011 
"input_clause(" ^ string_of_clausename (cls_id,ax_name) ^ "," ^ 
18863  1012 
knd ^ "," ^ lits ^ ").\n"; 
15347  1013 

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

1014 
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

1015 
"input_clause(" ^ string_of_type_clsname (cls_id,ax_name,idx) ^ "," ^ 
18863  1016 
knd ^ ",[" ^ tfree_lit ^ "]).\n"; 
15347  1017 

17422  1018 
fun tptp_type_lits (Clause cls) = 
15347  1019 
let val lits = map tptp_literal (#literals cls) 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

1021 
if !keep_types 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1022 
then (map tptp_of_typeLit (#tvar_type_literals cls)) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

1025 
if !keep_types 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1026 
then (map tptp_of_typeLit (#tfree_type_literals cls)) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1027 
else [] 
15347  1028 
in 
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset

1029 
(tvar_lits_strs @ lits, tfree_lits) 
15347  1030 
end; 
1031 

1032 
fun tptp_clause cls = 

17422  1033 
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

1034 
(*"lits" includes the typing assumptions (TVars)*) 
17317
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

1035 
val cls_id = get_clause_id cls 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

1036 
val ax_name = get_axiomName cls 
15347  1037 
val knd = string_of_kind cls 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1038 
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

1039 
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

1040 
fun typ_clss k [] = [] 
15347  1041 
 typ_clss k (tfree :: tfrees) = 
17317
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

1042 
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

1043 
typ_clss (k+1) tfrees 
15347  1044 
in 
1045 
cls_str :: (typ_clss 0 tfree_lits) 

1046 
end; 

1047 

15608  1048 
fun clause2tptp cls = 
17422  1049 
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

1050 
(*"lits" includes the typing assumptions (TVars)*) 
17317
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

1051 
val cls_id = get_clause_id cls 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

1052 
val ax_name = get_axiomName cls 
15608  1053 
val knd = string_of_kind cls 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1054 
val lits_str = bracket_pack lits 
15608  1055 
val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) 
1056 
in 

1057 
(cls_str,tfree_lits) 

1058 
end; 

1059 

1060 

18863  1061 
fun tptp_tfree_clause tfree_lit = 
1062 
"input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "]).\n"; 

15608  1063 

15347  1064 

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

1065 
fun tptp_of_arLit (TConsLit(b,(c,t,args))) = 
18868  1066 
tptp_sign b (c ^ "(" ^ t ^ paren_pack args ^ ")") 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1067 
 tptp_of_arLit (TVarLit(b,(c,str))) = 
18868  1068 
tptp_sign b (c ^ "(" ^ str ^ ")") 
15347  1069 

18868  1070 
fun tptp_arity_clause (arcls as ArityClause{kind,conclLit,premLits,...}) = 
1071 
let val arcls_id = string_of_arClauseID arcls 

1072 
val knd = name_of_kind kind 

1073 
val lits = map tptp_of_arLit (conclLit :: premLits) 

1074 
in 

1075 
"input_clause(" ^ arcls_id ^ "," ^ knd ^ "," ^ bracket_pack lits ^ ").\n" 

1076 
end; 

15347  1077 

1078 
fun tptp_classrelLits sub sup = 

1079 
let val tvar = "(T)" 

1080 
in 

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

1081 
"[" ^ sub ^ tvar ^ ",++" ^ sup ^ tvar ^ "]" 
15347  1082 
end; 
1083 

18868  1084 
fun tptp_classrelClause (ClassrelClause {axiom_name,subclass,superclass,...}) = 
1085 
"input_clause(" ^ axiom_name ^ ",axiom," ^ tptp_classrelLits subclass superclass ^ ").\n" 

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

1086 

18863  1087 
(* write out a subgoal as tptp clauses to the file "xxxx_N"*) 
1088 
fun tptp_write_file ths filename (axclauses,classrel_clauses,arity_clauses) = 

1089 
let 

1090 
val clss = make_conjecture_clauses (map prop_of ths) 

1091 
val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp clss) 

1092 
val tfree_clss = map tptp_tfree_clause (foldl (op union_string) [] tfree_litss) 

1093 
val out = TextIO.openOut filename 

1094 
in 

1095 
List.app (writeln_strs out o tptp_clause) axclauses; 

1096 
writeln_strs out tfree_clss; 

1097 
writeln_strs out tptp_clss; 

18868  1098 
List.app (curry TextIO.output out o tptp_classrelClause) classrel_clauses; 
1099 
List.app (curry TextIO.output out o tptp_arity_clause) arity_clauses; 

18863  1100 
TextIO.closeOut out 
1101 
end; 

1102 

15347  1103 
end; 