author  paulson 
Wed, 21 Dec 2005 12:06:08 +0100  
changeset 18449  e314fb38307d 
parent 18439  4b517881ac7e 
child 18676  5bce9fddce2e 
permissions  rwrr 
15347  1 
(* Author: Jia Meng, Cambridge University Computer Laboratory 
2 
ID: $Id$ 

3 
Copyright 2004 University of Cambridge 

4 

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

6 
Typed equality is treated differently. 

7 
*) 

8 

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

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

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

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

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

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

15 

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

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

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

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

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

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

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

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

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

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

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

27 

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

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

29 
val clauses2dfg : clause list > string > clause list > clause list > 
17422  30 
(string * int) list > (string * int) list > string 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

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

32 

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

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

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

35 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

50 

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

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

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

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

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

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

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

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

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

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

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

61 
val make_type_class : String.string > string 
17999  62 
val isMeta : String.string > bool 
63 

64 
type typ_var 

65 
val mk_typ_var_sort : Term.typ > typ_var * sort 

66 
type type_literal 

67 
val add_typs_aux2 : (typ_var * string list) list > type_literal list * type_literal list 

68 
val gen_tptp_cls : int * string * string * string > string 

69 
val gen_tptp_type_cls : int * string * string * string * int > string 

70 
val tptp_of_typeLit : type_literal > string 

18275  71 

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

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

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

75 

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

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

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

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

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

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

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

82 
(string * string) list * (string * string) list > bool * ((string * string) list * (string * string) list) 
4b517881ac7e
Added functions for fol_type; also put some functions to the signature, used by ResHolClause.
mengj
parents:
18420
diff
changeset

83 
val check_var_pairs: ''a * ''b > (''a * ''b) list > int 
15347  84 
end; 
85 

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

86 
structure ResClause : RES_CLAUSE = 
15347  87 
struct 
88 

89 
(* Added for typed equality *) 

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

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

92 

93 

94 
val schematic_var_prefix = "V_"; 

95 
val fixed_var_prefix = "v_"; 

96 

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

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

98 
val tfree_prefix = "t_"; 
15347  99 

100 
val clause_prefix = "cls_"; 

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

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

102 
val clrelclause_prefix = "clsrel_"; 
15347  103 

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

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

105 
val tconst_prefix = "tc_"; 
15347  106 

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

107 
val class_prefix = "class_"; 
15347  108 

109 

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

15347  112 

17775  113 
(*Provide readable names for the more common symbolic functions*) 
15347  114 
val const_trans_table = 
115 
Symtab.make [("op =", "equal"), 

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

117 
("op <", "less"), 

118 
("op &", "and"), 

119 
("op ", "or"), 

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

122 
("op *", "times"), 

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

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

15347  129 

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

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

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

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

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

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

137 
The character _ goes to __ 

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

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

140 
local 

141 

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

143 

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

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

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

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

150 
else "" 

15347  151 

15610  152 
in 
153 

154 
val ascii_of = String.translate ascii_of_c; 

155 

156 
end; 

15347  157 

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

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

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

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

161 

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

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

163 

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

164 

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

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

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

167 
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

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

169 

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

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

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

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

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

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

177 
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

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

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

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

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

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

184 

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

185 
fun lookup_type_const c = 
17412  186 
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

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

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

189 

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

190 
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

191 
 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

192 

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

193 
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

194 

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

196 

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

197 

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

198 

15347  199 
(***** definitions and functions for FOL clauses, prepared for conversion into TPTP format or SPASS format. *****) 
200 

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

201 
val keep_types = ref true; 
15347  202 

203 
datatype kind = Axiom  Hypothesis  Conjecture; 

204 
fun name_of_kind Axiom = "axiom" 

205 
 name_of_kind Hypothesis = "hypothesis" 

206 
 name_of_kind Conjecture = "conjecture"; 

207 

208 
type clause_id = int; 

209 
type axiom_name = string; 

210 

211 

212 
type polarity = bool; 

213 

214 
type indexname = Term.indexname; 

215 

216 

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

218 
type tag = bool; 

219 

220 

221 
(**** Isabelle FOL clauses ****) 

222 

223 
val tagged = ref false; 

224 

225 
type pred_name = string; 

226 
type sort = Term.sort; 

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

227 

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

228 

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

229 

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

230 
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

231 

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

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

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

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

235 

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

236 
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

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

238 
 string_of_fol_type (Comp(tcon,tps)) = 
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

239 
let val tstrs = map string_of_fol_type tps 
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

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

241 
tcon ^ (paren_pack tstrs) 
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

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

243 

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

244 
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

245 
 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

246 
 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

247 

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

248 

15347  249 

250 
datatype type_literal = LTVar of string  LTFree of string; 

251 

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

252 
datatype folTerm = UVar of string * fol_type 
18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

253 
 Fun of string * fol_type list * folTerm list; 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

254 
datatype predicate = Predicate of pred_name * fol_type list * folTerm list; 
15347  255 

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

257 

17999  258 
fun mk_typ_var_sort (TFree(a,s)) = (FOLTFree a,s) 
259 
 mk_typ_var_sort (TVar(v,s)) = (FOLTVar v,s); 

260 

261 

15347  262 

263 
(* ML datatype used to repsent one single clause: disjunction of literals. *) 

264 
datatype clause = 

265 
Clause of {clause_id: clause_id, 

266 
axiom_name: axiom_name, 

267 
kind: kind, 

268 
literals: literal list, 

269 
types_sorts: (typ_var * sort) list, 

270 
tvar_type_literals: type_literal list, 

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

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

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

273 
predicates: (string*int) list, 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

274 
functions: (string*int) list}; 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

275 

15347  276 

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

277 
exception CLAUSE of string * term; 
15347  278 

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

279 
fun get_literals (c as Clause(cls)) = #literals cls; 
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

280 

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

281 
fun components_of_literal (Literal (pol,pred,tag)) = ((pol,pred),tag); 
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

282 

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

283 
fun predicate_name (Predicate(predname,_,_)) = predname; 
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

284 

15347  285 

286 
(*** make clauses ***) 

287 

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

288 
fun isFalse (Literal (pol,Predicate(a,_,[]),_)) = 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

289 
(pol andalso a = "c_False") orelse 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

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

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

292 

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

293 
fun isTrue (Literal (pol,Predicate(a,_,[]),_)) = 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

294 
(pol andalso a = "c_True") orelse 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

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

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

297 

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

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

299 

17234  300 
fun make_clause (clause_id,axiom_name,kind,literals, 
301 
types_sorts,tvar_type_literals, 

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

302 
tfree_type_literals,tvars, predicates, functions) = 
17317
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

303 
if forall isFalse literals 
17234  304 
then error "Problem too trivial for resolution (empty clause)" 
305 
else 

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

306 
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

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

308 
tvar_type_literals = tvar_type_literals, 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

309 
tfree_type_literals = tfree_type_literals, 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

310 
tvars = tvars, predicates = predicates, 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

312 

15347  313 

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

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

315 

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

316 
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

317 

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

318 
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

319 

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

320 
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

321 

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

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

323 

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

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

325 

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

326 

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

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

328 
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

329 

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

330 
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

331 

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

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

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

334 
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

335 

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

336 

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

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

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

339 
fun type_of (Type (a, Ts)) = 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

340 
let val (folTyps, (ts, funcs)) = types_of Ts 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

341 
val t = make_fixed_type_const a 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

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

343 
(Comp(t,folTyps), (ts, (t, length Ts)::funcs)) 
18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

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

345 
 type_of (TFree (a,s)) = 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

346 
let val t = make_fixed_type_var a 
18402
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

347 
in (AtomF(t), ([((FOLTFree a),s)], [(t,0)])) end 
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

348 
 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

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

350 
let val foltyps_ts = map type_of Ts 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

351 
val (folTyps,ts_funcs) = ListPair.unzip foltyps_ts 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

352 
val (ts, funcslist) = ListPair.unzip ts_funcs 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

354 
(folTyps, (union_all ts, union_all funcslist)) 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

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

356 

15390  357 

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

358 

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

359 
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

360 

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

363 
val isMeta = String.isPrefix "METAHYP1_" 

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

364 

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

365 
fun pred_name_type (Const(c,T)) = 
18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

366 
let val (contys,(folTyps,funcs)) = const_types_of (c,T) 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

367 
in (make_fixed_const c, (contys,folTyps), funcs) end 
15390  368 
 pred_name_type (Free(x,T)) = 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

369 
if isMeta x then raise CLAUSE("Predicate Not First Order 1", Free(x,T)) 
18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

370 
else (make_fixed_var x, ([],[]), []) 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

371 
 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

372 
 pred_name_type t = raise CLAUSE("Predicate input unexpected", t); 
15347  373 

15615  374 

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

375 
(* For typed equality *) 
15615  376 
(* here "arg_typ" is the type of "="'s argument's type, not the type of the equality *) 
377 
(* Find type of equality arg *) 

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

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

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

380 
in folT end; 
15347  381 

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

382 
fun fun_name_type (Const("op =",T)) args = (*FIXME: Is this special treatment of = needed??*) 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

383 
let val t = make_fixed_const "op =" 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

384 
in (t, ([eq_arg_type T], []), [(t,2)]) end 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

385 
 fun_name_type (Const(c,T)) args = 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

386 
let val t = make_fixed_const c 
18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

387 
val (contys, (folTyps,funcs)) = const_types_of (c,T) 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

388 
val arity = num_typargs(c,T) + length args 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

390 
(t, (contys,folTyps), ((t,arity)::funcs)) 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

392 
 fun_name_type (Free(x,T)) args = 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

393 
let val t = make_fixed_var x 
18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

394 
in (t, ([],[]), [(t, length args)]) end 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

395 
 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

396 

15615  397 

15347  398 
fun term_of (Var(ind_nm,T)) = 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

399 
let val (folType,(ts,funcs)) = type_of T 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

401 
(UVar(make_schematic_var ind_nm, folType), (ts, funcs)) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

402 
end 
15347  403 
 term_of (Free(x,T)) = 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

404 
let val (folType, (ts,funcs)) = type_of T 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

406 
if isMeta x then (UVar(make_schematic_var(x,0),folType), 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

407 
(ts, ((make_schematic_var(x,0)),0)::funcs)) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

409 
(Fun(make_fixed_var x, [folType], []), 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

410 
(ts, ((make_fixed_var x),0)::funcs)) 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

412 
 term_of (Const(c,T)) = (* impossible to be equality *) 
18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

413 
let val (contys, (folTyps,funcs)) = const_types_of (c,T) 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

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

415 
(Fun(make_fixed_const c, contys, []), 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

416 
(folTyps, ((make_fixed_const c),0)::funcs)) 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

419 
let val (f,args) = strip_comb app 
18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

420 
val _ = case f of Const(_,_) => () 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

421 
 Free(s,_) => 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

422 
if isMeta s 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

423 
then raise CLAUSE("Function Not First Order 2", f) 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

424 
else () 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

425 
 _ => raise CLAUSE("Function Not First Order 3", f); 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

426 
val (funName,(contys,ts1),funcs) = fun_name_type f args 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

427 
val (args',(ts2,funcs')) = terms_of args 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

429 
(Fun(funName,contys,args'), 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

430 
(union_all (ts1::ts2), 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

431 
union_all(funcs::funcs'))) 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

433 
and terms_of ts = 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

434 
let val (args, ts_funcs) = ListPair.unzip (map term_of ts) 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

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

436 
(args, ListPair.unzip ts_funcs) 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

437 
end 
15390  438 

15347  439 

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

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

441 
let val arg_typ = eq_arg_type typ 
18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

442 
val (args',(ts,funcs)) = terms_of args 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

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

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

445 
(Predicate(equal_name,[arg_typ],args'), 
17775  446 
union_all ts, 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

447 
[((make_fixed_var equal_name), 2)], 
17775  448 
union_all funcs) 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

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

450 
 pred_of (pred,args) = 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

451 
let val (predName,(predType,ts1), pfuncs) = pred_name_type pred 
18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

452 
val (args',(ts2,ffuncs)) = terms_of args 
17775  453 
val ts3 = union_all (ts1::ts2) 
454 
val ffuncs' = union_all ffuncs 

17888  455 
val newfuncs = pfuncs union ffuncs' 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

456 
val arity = 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

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

458 
Const (c,T) => num_typargs(c,T) + length args 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

459 
 _ => length args 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

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

461 
(Predicate(predName,predType,args'), ts3, 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

462 
[(predName, arity)], newfuncs) 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

463 
end; 
15347  464 

465 

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

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

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

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

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

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

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

472 
(pred_of (strip_comb term), polarity, tag); 
15347  473 

17888  474 
fun literals_of_term1 args (Const("Trueprop",_) $ P) = literals_of_term1 args P 
475 
 literals_of_term1 (args as (lits, ts, preds, funcs)) (Const("op ",_) $ P $ Q) = 

476 
let val (lits', ts', preds', funcs') = literals_of_term1 args P 

17234  477 
in 
17888  478 
literals_of_term1 (lits', ts', preds' union preds, funcs' union funcs) Q 
17234  479 
end 
17888  480 
 literals_of_term1 (lits, ts, preds, funcs) P = 
481 
let val ((pred, ts', preds', funcs'), pol, tag) = predicate_of (P,true,false) 

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

482 
val lits' = Literal(pol,pred,tag) :: lits 
17234  483 
in 
17888  484 
(lits', ts union ts', preds' union preds, funcs' union funcs) 
17234  485 
end; 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

486 

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

487 

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

489 

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

490 

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

491 

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

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

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

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

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

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

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

498 
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

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

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

501 

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

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

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

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

505 
 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

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

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

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

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

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

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

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

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

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

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

516 

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

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

518 
 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

519 

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

520 

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

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

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

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

524 
 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

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

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

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

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

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

530 

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

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

532 

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

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

534 
 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

535 

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

536 

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

537 

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

538 
fun predicate_ord (Predicate(predname1,ftyps1,ftms1),Predicate(predname2,ftyps2,ftms2)) = 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

539 
let val predname_ord = string_ord (predname1,predname2) 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

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

541 
case predname_ord of EQUAL => 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

542 
let val ftms_ord = terms_ord(ftms1,ftms2) 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

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

544 
case ftms_ord of EQUAL => types_ord(ftyps1,ftyps2) 
df0c0f35c897
Changed literals' ordering and the functions for sorting literals.
mengj
parents:
18402
diff
changeset

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

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

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

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

549 

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

550 
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

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

552 
 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

553 

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

554 
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

555 

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

556 

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

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

558 

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

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

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

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

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

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

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

565 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

581 

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

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

583 

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

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

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

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

587 
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

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

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

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

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

592 

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

593 

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

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

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

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

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

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

599 
 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

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

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

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

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

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

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

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

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

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

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

610 

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

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

612 

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

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

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

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

616 
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

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

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

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

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

621 

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

622 

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

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

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

625 
if (predname1 = predname2) then terms_eq (tms1,tms2) vtvars 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

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

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

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

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

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

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

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

633 

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

634 

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

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

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

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

638 

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

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

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

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

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

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

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

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

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

647 

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

648 

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

649 
(*Equality of two clauses up to variable renaming*) 
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18411
diff
changeset

650 
fun clause_eq (cls1,cls2) = 
18409
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

651 
let val lits1 = get_literals cls1 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

652 
val lits2 = get_literals cls2 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

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

654 
length lits1 = length lits2 andalso #1 (lits_eq (lits1,lits2) ([],[])) 
18409
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

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

656 

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

657 

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

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

659 

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

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

661 

18449  662 
fun hashw_term (UVar(_,_), w) = w 
663 
 hashw_term (Fun(f,tps,args), w) = 

664 
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

665 

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

668 

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

671 

18449  672 
fun hash_clause clause = Word.toIntX (xor_words (map hash1_literal (get_literals clause))); 
18402
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

673 

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

674 

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

675 
(* FIX: not sure what to do with these funcs *) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

676 

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

677 
(*Make literals for sorted type variables*) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

679 
 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

680 
sorts_on_typs (v,s) (*IGNORE sort "type"*) 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

682 
LTVar((make_type_class s) ^ 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

683 
"(" ^ (make_schematic_type_var indx) ^ ")") :: 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

684 
(sorts_on_typs ((FOLTVar indx), ss)) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

685 
 sorts_on_typs ((FOLTFree x), (s::ss)) = 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

686 
LTFree((make_type_class s) ^ "(" ^ (make_fixed_type_var x) ^ ")") :: 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

687 
(sorts_on_typs ((FOLTFree x), ss)); 
15347  688 

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

689 

17312  690 
(*UGLY: seems to be parsing the "show sorts" output, removing anything that 
691 
starts with a left parenthesis.*) 

692 
fun remove_type str = hd (String.fields (fn c => c = #"(") str); 

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

693 

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

694 
fun pred_of_sort (LTVar x) = ((remove_type x),1) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

695 
 pred_of_sort (LTFree x) = ((remove_type x),1) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

696 

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

697 

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

698 

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

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

700 
The first is for TVars, the second for TFrees.*) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

701 
fun add_typs_aux [] preds = ([],[], preds) 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

703 
let val vs = sorts_on_typs (FOLTVar indx, s) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

704 
val preds' = (map pred_of_sort vs)@preds 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

706 
in 
17775  707 
(vs union vss, fss, preds'') 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

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

710 
let val fs = sorts_on_typs (FOLTFree x, s) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

711 
val preds' = (map pred_of_sort fs)@preds 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

713 
in 
17775  714 
(vss, fs union fss, preds'') 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

716 

17999  717 
fun add_typs_aux2 [] = ([],[]) 
718 
 add_typs_aux2 ((FOLTVar indx,s)::tss) = 

719 
let val vs = sorts_on_typs (FOLTVar indx,s) 

720 
val (vss,fss) = add_typs_aux2 tss 

721 
in 

722 
(vs union vss,fss) 

723 
end 

724 
 add_typs_aux2 ((FOLTFree x,s)::tss) = 

725 
let val fs = sorts_on_typs (FOLTFree x,s) 

726 
val (vss,fss) = add_typs_aux2 tss 

727 
in 

728 
(vss,fs union fss) 

729 
end; 

730 

731 

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

732 
fun add_typs (Clause cls) preds = add_typs_aux (#types_sorts cls) preds 
15347  733 

734 

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

736 

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

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

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

739 
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

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

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

743 
 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

744 

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

745 
(* FIX add preds and funcs to add typs aux here *) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

746 

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

747 
fun make_axiom_clause_thm thm (ax_name,cls_id) = 
17888  748 
let val (lits,types_sorts, preds, funcs) = literals_of_term (prop_of thm) 
18402
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

749 
val lits' = sort_lits lits 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

751 
val tvars = get_tvar_strs types_sorts 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

753 
make_clause(cls_id,ax_name,Axiom, 
18402
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

754 
lits',types_sorts,tvar_lits,tfree_lits, 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

755 
tvars, preds, funcs) 
15347  756 
end; 
757 

758 

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

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

761 
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

762 
handle TERM("check_is_fol_term",_) => raise CLAUSE("Goal is not FOL",t) 
d236379ea408
 before converting axiom and conjecture clauses into ResClause.clause format, perform "check_is_fol_term" first.
mengj
parents:
18056
diff
changeset

763 
val (lits,types_sorts, preds, funcs) = literals_of_term t 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

765 
val tvars = get_tvar_strs types_sorts 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

767 
make_clause(n,"conjecture",Conjecture, 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

768 
lits,types_sorts,tvar_lits,tfree_lits, 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

771 

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

772 
fun make_conjecture_clauses_aux _ [] = [] 
17888  773 
 make_conjecture_clauses_aux n (t::ts) = 
774 
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

775 

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

776 
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

777 

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

778 

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

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

780 
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

781 
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

782 
handle TERM("check_is_fol_term",_) => raise CLAUSE("Axiom is not FOL", term) 
d236379ea408
 before converting axiom and conjecture clauses into ResClause.clause format, perform "check_is_fol_term" first.
mengj
parents:
18056
diff
changeset

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

784 
val lits' = sort_lits lits 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

786 
val tvars = get_tvar_strs types_sorts 
15347  787 
in 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

788 
make_clause(cls_id,ax_name,Axiom, 
18402
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

789 
lits',types_sorts,tvar_lits,tfree_lits, 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

790 
tvars, preds,funcs) 
15347  791 
end; 
792 

793 

794 

795 

796 
(**** Isabelle arities ****) 

797 

798 
exception ARCLAUSE of string; 

799 

800 

801 
type class = string; 

802 
type tcons = string; 

803 

804 

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

806 

807 
datatype arityClause = 

808 
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

809 
axiom_name: axiom_name, 
15347  810 
kind: kind, 
811 
conclLit: arLit, 

812 
premLits: arLit list}; 

813 

814 

815 
fun get_TVars 0 = [] 

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

816 
 get_TVars n = ("T_" ^ (Int.toString n)) :: get_TVars (n1); 
15347  817 

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

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

819 
 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

820 
 pack_sort(tvar, cls::srt) = (make_type_class cls, tvar) :: pack_sort(tvar, srt); 
15347  821 

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

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

824 

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

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

826 
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

827 
let val nargs = length args 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

828 
val tvars = get_TVars nargs 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

829 
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

830 
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

831 
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

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

833 
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

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

835 
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

836 
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

837 
end; 
15347  838 

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

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

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

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

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

843 
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

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

845 
in 1 + num_tfree_lits end; 
15347  846 

847 

848 
(**** Isabelle class relations ****) 

849 

850 
datatype classrelClause = 

851 
ClassrelClause of {clause_id: clause_id, 

852 
subclass: class, 

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

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

854 

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

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

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

857 
subclass = subclass, superclass = superclass}; 
15347  858 

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

859 
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

860 
 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

861 
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

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

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

864 
:: classrelClauses_of_aux (n+1) sub sups; 
15347  865 

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

866 
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

867 

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

868 

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

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

870 

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

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

872 
 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

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

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

875 
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

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

877 

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

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

879 
 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

880 
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

881 

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

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

883 
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

884 
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

885 

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

886 

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

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

888 

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

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

890 

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

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

892 
fun classrel_clauses_classrel (C: Sorts.classes) = map classrelClauses_of (Graph.dest C); 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

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

894 

15347  895 

896 

897 
(****!!!! Changed for typed equality !!!!****) 

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

898 

15347  899 
fun wrap_eq_type typ t = eq_typ_wrapper ^"(" ^ t ^ "," ^ typ ^ ")"; 
900 

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

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

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

904 
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

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

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

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

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

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

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

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

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

913 
 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

914 
 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

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

916 
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

917 
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

918 
in name ^ (paren_pack (terms_as_strings @ typs')) end; 
15347  919 

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

921 
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

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

923 
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

924 
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

925 
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

926 

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

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

928 
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

929 

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

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

931 
string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx); 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

932 

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

933 

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

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

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

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

937 

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

938 
fun dfg_literal (Literal(pol,pred,tag)) = 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

939 
let val pred_string = string_of_predicate pred 
17234  940 
in 
941 
if pol then pred_string else "not(" ^pred_string ^ ")" 

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

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

943 

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

944 

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

945 
(* FIX: what does this mean? *) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

946 
(*fun dfg_of_typeLit (LTVar x) = "not(" ^ x ^ ")" 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

947 
 dfg_of_typeLit (LTFree x) = "(" ^ x ^ ")";*) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

948 

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

949 
fun dfg_of_typeLit (LTVar x) = x 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

951 

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

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

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

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

955 

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

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

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

958 

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

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

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

961 
"or(" ^ lits ^ ")" ^ forall_close(vars,tvars) ^ ",\n" ^ 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

962 
string_of_clausename (cls_id,ax_name) ^ ")."; 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

963 

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

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

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

966 
"or( " ^ tfree_lit ^ ")" ^ forall_close(vars,tvars) ^ ",\n" ^ 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

967 
string_of_type_clsname (cls_id,ax_name,idx) ^ ")."; 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

968 

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

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

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

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

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

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

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

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

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

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

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

980 

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

981 

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

982 
fun dfg_folterms (Literal(pol,pred,tag)) = 
18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

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

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

985 

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

986 

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

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

989 

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

990 

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

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

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

993 

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

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

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

996 

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

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

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

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

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

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

1003 

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

1004 

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

1005 
fun dfg_tvars (Clause cls) =(#tvars cls) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1006 

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

1007 

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

1008 

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

1009 
(* make this return funcs and preds too? *) 
18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

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

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

1012 

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

1013 

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

1014 

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

1015 
fun concat_with sep [] = "" 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1016 
 concat_with sep [x] = "(" ^ x ^ ")" 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1017 
 concat_with sep (x::xs) = "(" ^ x ^ ")" ^ sep ^ (concat_with sep xs); 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1018 

17234  1019 
fun dfg_pred (Literal(pol,pred,tag)) ax_name = 
1020 
(string_of_predname pred) ^ " " ^ ax_name 

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

1021 

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

1022 
fun dfg_clause cls = 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1023 
let val (lits,tfree_lits) = dfg_clause_aux cls 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1024 
(*"lits" includes the typing assumptions (TVars)*) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1025 
val vars = dfg_vars cls 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1026 
val tvars = dfg_tvars cls 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1027 
val knd = string_of_kind cls 
17234  1028 
val lits_str = commas lits 
17317
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

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

1030 
val axname = get_axiomName cls 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

1031 
val cls_str = gen_dfg_cls(cls_id,axname,knd,lits_str,tvars, vars) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1032 
fun typ_clss k [] = [] 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

1034 
(gen_dfg_type_cls(cls_id,axname,knd,tfree,k, tvars,vars)) :: 
17234  1035 
(typ_clss (k+1) tfrees) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

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

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

1039 

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

1040 
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

1041 

17234  1042 
fun string_of_preds preds = 
1043 
"predicates[" ^ (concat_with ", " (map string_of_arity preds)) ^ "].\n"; 

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

1044 

17234  1045 
fun string_of_funcs funcs = 
1046 
"functions[" ^ (concat_with ", " (map string_of_arity funcs)) ^ "].\n" ; 

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

1047 

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

1048 

17234  1049 
fun string_of_symbols predstr funcstr = 
1050 
"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

1051 

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

1052 

17234  1053 
fun string_of_axioms axstr = 
1054 
"list_of_clauses(axioms,cnf).\n" ^ axstr ^ "end_of_list.\n\n"; 

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

1055 

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

1056 

17234  1057 
fun string_of_conjectures conjstr = 
1058 
"list_of_clauses(conjectures,cnf).\n" ^ conjstr ^ "end_of_list.\n\n"; 

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

1059 

17234  1060 
fun string_of_descrip () = 
1061 
"list_of_descriptions.\nname({*[ File : ],[ Names :]*}).\nauthor({*[ Source :]*}).\nstatus(unknown).\ndescription({*[ Refs :]*}).\nend_of_list.\n\n" 

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

1062 

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

1063 

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

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

1065 

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

1066 

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

1067 
fun string_of_end () = "end_problem.\n%"; 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1068 

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

1069 

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

1070 
fun clause2dfg cls = 
17234  1071 
let val (lits,tfree_lits) = dfg_clause_aux cls 
1072 
(*"lits" includes the typing assumptions (TVars)*) 

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

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

1074 
val ax_name = get_axiomName cls 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1075 
val vars = dfg_vars cls 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1076 
val tvars = dfg_tvars cls 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1077 
val funcs = funcs_of_cls cls 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1078 
val preds = preds_of_cls cls 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1079 
val knd = string_of_kind cls 
17234  1080 
val lits_str = commas lits 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1081 
val cls_str = gen_dfg_cls(cls_id,ax_name,knd,lits_str,tvars,vars) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

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

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

1085 

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

1086 

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

1087 

17234  1088 
fun tfree_dfg_clause tfree_lit = 
17422  1089 
"clause( %(conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ")." 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1090 

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

1091 

17422  1092 
fun gen_dfg_file probname axioms conjectures funcs preds = 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1093 
let val axstrs_tfrees = (map clause2dfg axioms) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1094 
val (axstrs, atfrees) = ListPair.unzip axstrs_tfrees 
17764  1095 
val axstr = (space_implode "\n" axstrs) ^ "\n\n" 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1096 
val conjstrs_tfrees = (map clause2dfg conjectures) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1097 
val (conjstrs, atfrees) = ListPair.unzip conjstrs_tfrees 
17775  1098 
val tfree_clss = map tfree_dfg_clause (union_all atfrees) 
17764  1099 
val conjstr = (space_implode "\n" (tfree_clss@conjstrs)) ^ "\n\n" 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1100 
val funcstr = string_of_funcs funcs 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1101 
val predstr = string_of_preds preds 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

1103 
(string_of_start probname) ^ (string_of_descrip ()) ^ 
17764  1104 
(string_of_symbols funcstr predstr) ^ 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1105 
(string_of_axioms axstr) ^ 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

1108 

17422  1109 
fun clauses2dfg [] probname axioms conjectures funcs preds = 
17775  1110 
let val funcs' = (union_all(map funcs_of_cls axioms)) @ funcs 
1111 
val preds' = (union_all(map preds_of_cls axioms)) @ preds 

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

1112 
in 
17422  1113 
gen_dfg_file probname axioms conjectures funcs' preds' 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1114 
end 
17422  1115 
 clauses2dfg (cls::clss) probname axioms conjectures funcs preds = 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1116 
let val (lits,tfree_lits) = dfg_clause_aux cls 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

1119 
val ax_name = get_axiomName cls 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1120 
val vars = dfg_vars cls 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1121 
val tvars = dfg_tvars cls 
17888  1122 
val funcs' = (funcs_of_cls cls) union funcs 
1123 
val preds' = (preds_of_cls cls) union preds 

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

1124 
val knd = string_of_kind cls 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1125 
val lits_str = concat_with ", " lits 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1126 
val axioms' = if knd = "axiom" then (cls::axioms) else axioms 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1127 
val conjectures' = 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1128 
if knd = "conjecture" then (cls::conjectures) else conjectures 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1129 
in 
17422  1130 
clauses2dfg clss probname axioms' conjectures' funcs' preds' 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

1132 

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

1133 

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

1134 
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

1135 
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

1136 

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

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

1138 

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

1139 
(*FIXME!!! currently is TPTP format!*) 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1140 
fun dfg_of_arLit (TConsLit(b,(c,t,args))) = 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1141 
let val pol = if b then "++" else "" 
18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

1142 
val arg_strs = paren_pack args 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

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

1144 
pol ^ c ^ "(" ^ t ^ arg_strs ^ ")" 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

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

1146 
 dfg_of_arLit (TVarLit(b,(c,str))) = 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1147 
let val pol = if b then "++" else "" 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

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

1149 
pol ^ c ^ "(" ^ str ^ ")" 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

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

1151 

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

1152 

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

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

1154 

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

1155 

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

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

1157 

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

1158 

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

1159 

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

1160 
(*FIXME: would this have variables in a forall? *) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1161 

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

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

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

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

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

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

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

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

1169 
"clause( %(" ^ knd ^ ")\n" ^ "or( " ^ (bracket_pack all_lits) ^ ")),\n" ^ 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1170 
arcls_id ^ ")." 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

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

1172 

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

1173 

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

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

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

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

1177 

15347  1178 
fun tptp_literal (Literal(pol,pred,tag)) = 
1179 
let val pred_string = string_of_predicate pred 

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

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

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

1182 
else (if pol then "++" else "") 
15347  1183 
in 
1184 
tagged_pol ^ pred_string 

1185 
end; 

1186 

1187 
fun tptp_of_typeLit (LTVar x) = "" ^ x 

1188 
 tptp_of_typeLit (LTFree x) = "++" ^ x; 

1189 

1190 

1191 
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

1192 
"input_clause(" ^ string_of_clausename (cls_id,ax_name) ^ "," ^ 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

1193 
knd ^ "," ^ lits ^ ")."; 
15347  1194 

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

1195 
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

1196 
"input_clause(" ^ string_of_type_clsname (cls_id,ax_name,idx) ^ "," ^ 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1197 
knd ^ ",[" ^ tfree_lit ^ "])."; 
15347  1198 

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

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

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

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

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

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

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

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

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

1210 
(tvar_lits_strs @ lits, tfree_lits) 
15347  1211 
end; 
1212 

1213 
fun tptp_clause cls = 

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

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

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

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

1219 
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

1220 
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

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

1223 
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

1224 
typ_clss (k+1) tfrees 
15347  1225 
in 
1226 
cls_str :: (typ_clss 0 tfree_lits) 

1227 
end; 

1228 

15608  1229 
fun clause2tptp cls = 
17422  1230 
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

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

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

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

1235 
val lits_str = bracket_pack lits 
15608  1236 
val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) 
1237 
in 

1238 
(cls_str,tfree_lits) 

1239 
end; 

1240 

1241 

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

1242 
fun tfree_clause tfree_lit = 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1243 
"input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "])."; 
15608  1244 

15347  1245 

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

1246 
fun tptp_of_arLit (TConsLit(b,(c,t,args))) = 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1247 
let val pol = if b then "++" else "" 
18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

1248 
val arg_strs = paren_pack args 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

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

1250 
pol ^ c ^ "(" ^ t ^ arg_strs ^ ")" 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

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

1252 
 tptp_of_arLit (TVarLit(b,(c,str))) = 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1253 
let val pol = if b then "++" else "" 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

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

1255 
pol ^ c ^ "(" ^ str ^ ")" 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1256 
end; 
15347  1257 

1258 

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

1259 
fun tptp_of_conclLit (ArityClause arcls) = tptp_of_arLit (#conclLit arcls); 
15347  1260 

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

1261 
fun tptp_of_premLits (ArityClause arcls) = map tptp_of_arLit (#premLits arcls); 
15347  1262 

1263 
fun tptp_arity_clause arcls = 

1264 
let val arcls_id = string_of_arClauseID arcls 

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

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

1266 
val prems_lits = tptp_of_premLits arcls 
15347  1267 
val knd = string_of_arKind arcls 
1268 
val all_lits = concl_lit :: prems_lits 

1269 
in 

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

1270 
"input_clause(" ^ arcls_id ^ "," ^ knd ^ "," ^ 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1271 
(bracket_pack all_lits) ^ ")." 
15347  1272 
end; 
1273 

1274 
fun tptp_classrelLits sub sup = 

1275 
let val tvar = "(T)" 

1276 
in 

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

1277 
"[" ^ sub ^ tvar ^ ",++" ^ sup ^ tvar ^ "]" 
15347  1278 
end; 
1279 