author  paulson 
Fri, 27 Jan 2006 18:29:33 +0100  
changeset 18798  ca02a2077955 
parent 18676  5bce9fddce2e 
child 18856  4669dec681f4 
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 
18798  29 
val clauses2dfg : string > clause list > clause list > string 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

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

31 

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

32 
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

33 
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

34 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

49 

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

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

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

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

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

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

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

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

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

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

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

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

63 
type typ_var 

64 
val mk_typ_var_sort : Term.typ > typ_var * sort 

65 
type type_literal 

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

67 
val gen_tptp_cls : int * string * string * string > string 

68 
val gen_tptp_type_cls : int * string * string * string * int > string 

69 
val tptp_of_typeLit : type_literal > string 

18275  70 

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

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

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

74 

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

75 
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

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

77 
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

78 
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

79 
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

80 
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

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

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

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

85 
structure ResClause : RES_CLAUSE = 
15347  86 
struct 
87 

88 
(* Added for typed equality *) 

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

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

91 

92 

93 
val schematic_var_prefix = "V_"; 

94 
val fixed_var_prefix = "v_"; 

95 

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

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

97 
val tfree_prefix = "t_"; 
15347  98 

99 
val clause_prefix = "cls_"; 

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

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

101 
val clrelclause_prefix = "clsrel_"; 
15347  102 

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

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

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

105 
val class_prefix = "class_"; 
15347  106 

17775  107 
fun union_all xss = foldl (op union) [] xss; 
108 

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

15347  110 
val const_trans_table = 
111 
Symtab.make [("op =", "equal"), 

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

113 
("op <", "less"), 

114 
("op &", "and"), 

115 
("op ", "or"), 

17375  116 
("op +", "plus"), 
117 
("op ", "minus"), 

118 
("op *", "times"), 

18676  119 
("Divides.op div", "div"), 
120 
("HOL.divide", "divide"), 

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

18390  125 
("op Int", "inter"), 
126 
("List.op @", "append")]; 

15347  127 

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

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

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

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

131 
("~=>", "map")]; 
15347  132 

15610  133 
(*Escaping of special characters. 
134 
Alphanumeric characters are left unchanged. 

135 
The character _ goes to __ 

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

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

138 
local 

139 

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

141 

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

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

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

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

148 
else "" 

15347  149 

15610  150 
in 
151 

152 
val ascii_of = String.translate ascii_of_c; 

153 

154 
end; 

15347  155 

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

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

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

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

159 

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

160 
fun bracket_pack strings = "[" ^ commas strings ^ "]"; 
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 

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

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

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

165 
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

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

167 

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

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

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

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

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

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

175 
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

176 
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); 
15347  177 

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

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

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

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

182 

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

183 
fun lookup_type_const c = 
17412  184 
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

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

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

187 

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

188 
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

189 
 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

190 

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

191 
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

192 

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

194 

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

195 

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

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

198 
val keep_types = ref true; 
15347  199 

200 
datatype kind = Axiom  Hypothesis  Conjecture; 

201 
fun name_of_kind Axiom = "axiom" 

202 
 name_of_kind Hypothesis = "hypothesis" 

203 
 name_of_kind Conjecture = "conjecture"; 

204 

205 
type clause_id = int; 

206 
type axiom_name = string; 

207 

208 

209 
type polarity = bool; 

210 

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

212 
type tag = bool; 

213 

214 

215 
(**** Isabelle FOL clauses ****) 

216 

217 
val tagged = ref false; 

218 

219 
type pred_name = string; 

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

220 

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

221 
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

222 

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

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

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

226 
 Comp of string * fol_type list; 
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 
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

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

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

231 
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

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

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

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

235 

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

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

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

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

239 

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

240 

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

15347  243 

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

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

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

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

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

249 

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

252 

253 

15347  254 

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

256 
datatype clause = 

257 
Clause of {clause_id: clause_id, 

258 
axiom_name: axiom_name, 

259 
kind: kind, 

260 
literals: literal list, 

261 
types_sorts: (typ_var * sort) list, 

262 
tvar_type_literals: type_literal list, 

18798  263 
tfree_type_literals: type_literal list, 
264 
predicates: (string*int) list}; 

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

265 

15347  266 

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

267 
exception CLAUSE of string * term; 
15347  268 

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

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

270 

15347  271 

272 
(*** make clauses ***) 

273 

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

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

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

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

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

278 

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

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

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

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

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

283 

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

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

285 

17234  286 
fun make_clause (clause_id,axiom_name,kind,literals, 
287 
types_sorts,tvar_type_literals, 

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

289 
if forall isFalse literals 
17234  290 
then error "Problem too trivial for resolution (empty clause)" 
291 
else 

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

292 
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

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

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

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

297 

15347  298 

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

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

300 

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

301 
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

302 

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

303 
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

304 

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

305 
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

306 

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

307 
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

308 

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

309 

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

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

311 
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

312 

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

313 
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

314 

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

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

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

317 
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

318 

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

319 

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

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

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

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

324 
val t = make_fixed_type_const a 
18798  325 
in (Comp(t,folTyps), ts) end 
326 
 type_of (TFree (a,s)) = (AtomF(make_fixed_type_var a), [(FOLTFree a, s)]) 

327 
 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

328 
and types_of Ts = 
18798  329 
let val (folTyps,ts) = ListPair.unzip (map type_of Ts) 
330 
in (folTyps, union_all ts) end; 

15390  331 

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

332 

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

333 
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

334 

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

337 
val isMeta = String.isPrefix "METAHYP1_" 

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

338 

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

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

343 
 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

344 
 pred_name_type t = raise CLAUSE("Predicate input unexpected", t); 
15347  345 

15615  346 

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

347 
(* For typed equality *) 
15615  348 
(* here "arg_typ" is the type of "="'s argument's type, not the type of the equality *) 
349 
(* Find type of equality arg *) 

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

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

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

352 
in folT end; 
15347  353 

18798  354 
fun fun_name_type (Const(c,T)) args = (make_fixed_const c, const_types_of (c,T)) 
355 
 fun_name_type (Free(x,T)) args = 

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

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

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

358 
 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

359 

15347  360 
fun term_of (Var(ind_nm,T)) = 
18798  361 
let val (folType,ts) = type_of T 
362 
in (UVar(make_schematic_var ind_nm, folType), ts) end 

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

365 
in 
18798  366 
if isMeta x then (UVar(make_schematic_var(x,0),folType), ts) 
367 
else (Fun(make_fixed_var x, [folType], []), ts) 

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

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

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

370 
let val (f,args) = strip_comb app 
18798  371 
val (funName,(contys,ts1)) = fun_name_type f args 
372 
val (args',ts2) = terms_of args 

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

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

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

376 
end 
18798  377 
and terms_of ts = ListPair.unzip (map term_of ts) 
15390  378 

15347  379 

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

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

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

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

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

385 
(Predicate(equal_name,[arg_typ],args'), 
17775  386 
union_all ts, 
18798  387 
[((make_fixed_var equal_name), 2)]) 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

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

389 
 pred_of (pred,args) = 
18798  390 
let val (predName, (predType,ts1)) = pred_name_type pred 
391 
val (args',ts2) = terms_of args 

17775  392 
val ts3 = union_all (ts1::ts2) 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

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

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

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

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

397 
in 
18798  398 
(Predicate(predName,predType,args'), ts3, [(predName, arity)]) 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

399 
end; 
15347  400 

401 

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

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

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

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

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

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

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

408 
(pred_of (strip_comb term), polarity, tag); 
15347  409 

17888  410 
fun literals_of_term1 args (Const("Trueprop",_) $ P) = literals_of_term1 args P 
18798  411 
 literals_of_term1 (args as (lits, ts, preds)) (Const("op ",_) $ P $ Q) = 
412 
let val (lits', ts', preds') = literals_of_term1 args P 

17234  413 
in 
18798  414 
literals_of_term1 (lits', ts', preds' union preds) Q 
17234  415 
end 
18798  416 
 literals_of_term1 (lits, ts, preds) P = 
417 
let val ((pred, ts', preds'), pol, tag) = predicate_of (P,true,false) 

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

418 
val lits' = Literal(pol,pred,tag) :: lits 
17234  419 
in 
18798  420 
(lits', ts union ts', preds' union preds) 
17234  421 
end; 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

422 

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

423 

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

425 

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

426 

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

427 

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

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

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

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

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

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

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

434 
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

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

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

437 

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

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

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

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

441 
 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

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

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

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

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

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

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

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

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

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

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

452 

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

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

454 
 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

455 

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

456 

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

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

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

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

460 
 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

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

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

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

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

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

466 

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

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

468 

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

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

470 
 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

471 

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

472 

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

473 

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

474 
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

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

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

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

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

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

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

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

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

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

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

485 

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

486 
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

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

488 
 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

489 

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

490 
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

491 

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

492 

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

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

494 

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

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

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

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

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

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

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

501 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

517 

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

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

519 

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

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

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

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

523 
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

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

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

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

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

528 

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

529 

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

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

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

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

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

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

535 
 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

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

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

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

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

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

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

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

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

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

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

546 

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

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

548 

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

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

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

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

552 
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

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

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

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

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

557 

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 pred_eq (Predicate(predname1,tps1,tms1),Predicate(predname2,tps2,tms2)) vtvars = 
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

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

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

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

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

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

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

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

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

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

569 

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

570 

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

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

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

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

574 

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

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

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

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

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

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

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

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

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

583 

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

584 

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

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

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

588 

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

589 

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

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

591 

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

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

593 

18449  594 
fun hashw_term (UVar(_,_), w) = w 
595 
 hashw_term (Fun(f,tps,args), w) = 

596 
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

597 

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

600 

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

603 

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

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

606 

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

607 

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

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

610 
 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

611 
sorts_on_typs (v,s) (*IGNORE sort "type"*) 
18798  612 
 sorts_on_typs ((FOLTVar indx), s::ss) = 
613 
LTVar(make_type_class s, make_schematic_type_var indx) :: 

614 
sorts_on_typs ((FOLTVar indx), ss) 

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

616 
LTFree(make_type_class s, make_fixed_type_var x) :: 

617 
sorts_on_typs ((FOLTFree x), ss); 

15347  618 

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

619 

18798  620 
fun pred_of_sort (LTVar (s,ty)) = (s,1) 
621 
 pred_of_sort (LTFree (s,ty)) = (s,1) 

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

622 

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

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

624 
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

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

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

627 
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

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

629 
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

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

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

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

634 
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

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

636 
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

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

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

640 

17999  641 
fun add_typs_aux2 [] = ([],[]) 
642 
 add_typs_aux2 ((FOLTVar indx,s)::tss) = 

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

644 
val (vss,fss) = add_typs_aux2 tss 

645 
in 

646 
(vs union vss,fss) 

647 
end 

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

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

650 
val (vss,fss) = add_typs_aux2 tss 

651 
in 

652 
(vss,fs union fss) 

653 
end; 

654 

655 

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

656 
fun add_typs (Clause cls) preds = add_typs_aux (#types_sorts cls) preds 
15347  657 

658 

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

660 

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

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

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

663 
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

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

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

667 
 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

668 

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

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

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

672 
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

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

674 
make_clause(cls_id,ax_name,Axiom, 
18798  675 
lits',types_sorts,tvar_lits,tfree_lits,preds) 
15347  676 
end; 
677 

678 

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

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

681 
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

682 
handle TERM("check_is_fol_term",_) => raise CLAUSE("Goal is not FOL",t) 
18798  683 
val (lits,types_sorts, preds) = literals_of_term t 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

684 
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

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

686 
make_clause(n,"conjecture",Conjecture, 
18798  687 
lits,types_sorts,tvar_lits,tfree_lits,preds) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

689 

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

690 
fun make_conjecture_clauses_aux _ [] = [] 
17888  691 
 make_conjecture_clauses_aux n (t::ts) = 
692 
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

693 

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

694 
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

695 

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

696 

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

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

698 
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

699 
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

700 
handle TERM("check_is_fol_term",_) => raise CLAUSE("Axiom is not FOL", term) 
18798  701 
val (lits,types_sorts, preds) = literals_of_term term 
18402
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

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

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

705 
make_clause(cls_id,ax_name,Axiom, 
18798  706 
lits',types_sorts,tvar_lits,tfree_lits,preds) 
15347  707 
end; 
708 

709 

710 

711 

712 
(**** Isabelle arities ****) 

713 

714 
exception ARCLAUSE of string; 

715 

716 
type class = string; 

717 
type tcons = string; 

718 

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

720 

721 
datatype arityClause = 

722 
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

723 
axiom_name: axiom_name, 
15347  724 
kind: kind, 
725 
conclLit: arLit, 

726 
premLits: arLit list}; 

727 

728 

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

15347  731 

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

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

733 
 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

734 
 pack_sort(tvar, cls::srt) = (make_type_class cls, tvar) :: pack_sort(tvar, srt); 
15347  735 

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

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

738 

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

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

740 
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

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

743 
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

744 
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

745 
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

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

747 
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

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

749 
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

750 
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

751 
end; 
15347  752 

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

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

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

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

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

757 
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

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

759 
in 1 + num_tfree_lits end; 
15347  760 

761 

762 
(**** Isabelle class relations ****) 

763 

764 
datatype classrelClause = 

765 
ClassrelClause of {clause_id: clause_id, 

766 
subclass: class, 

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

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

768 

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

769 
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

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

771 
subclass = subclass, superclass = superclass}; 
15347  772 

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

773 
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

774 
 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

775 
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

776 
 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

777 
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

778 
:: classrelClauses_of_aux (n+1) sub sups; 
15347  779 

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

780 
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

781 

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

782 

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

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

784 

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

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

786 
 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

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

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

789 
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

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

791 

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

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

793 
 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

794 
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

795 

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

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

797 
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

798 
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

799 

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

800 

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

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

802 

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

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

804 

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

805 
val classrel_of = #2 o #classes o Type.rep_tsig o Sign.tsig_of; 
18798  806 

807 
fun classrel_clauses_classrel (C: Sorts.classes) = 

808 
map classrelClauses_of (Graph.dest C); 

809 

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

810 
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

811 

15347  812 

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

814 

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

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

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

818 
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

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

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

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

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

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

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

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

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

827 
 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

828 
 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

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

830 
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

831 
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

832 
in name ^ (paren_pack (terms_as_strings @ typs')) end; 
15347  833 

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

835 
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

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

837 
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

838 
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

839 
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

840 

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

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

842 
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

843 

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

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

845 
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

846 

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

847 

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

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

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

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

851 

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

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

853 
let val pred_string = string_of_predicate pred 
17234  854 
in 
855 
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

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

857 

18798  858 
fun dfg_of_typeLit (LTVar (s,ty)) = "not(" ^ s ^ "(" ^ ty ^ "))" 
859 
 dfg_of_typeLit (LTFree (s,ty)) = "(" ^ s ^ "(" ^ ty ^ "))"; 

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

860 

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

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

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

863 
 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

864 

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

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

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

867 

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

868 
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

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

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

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

872 

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

873 
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

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

875 
"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

876 
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

877 

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

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

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

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

881 
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

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

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

884 
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

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

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

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

889 

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

890 

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

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

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

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

894 

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

895 
fun get_uvars (UVar(a,typ)) = [a] 
17775  896 
 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

897 

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

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

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

900 

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

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

902 
 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

903 

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

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

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

906 
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

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

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

910 

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

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

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

913 

17234  914 
fun dfg_pred (Literal(pol,pred,tag)) ax_name = 
915 
(string_of_predname pred) ^ " " ^ ax_name 

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

916 

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

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

920 
val vars = dfg_vars cls 
18798  921 
val tvars = get_tvar_strs types_sorts 
922 
val preds = preds_of_cls cls 

923 
val knd = name_of_kind kind 

17234  924 
val lits_str = commas lits 
18798  925 
val cls_str = gen_dfg_cls(clause_id,axiom_name,knd,lits_str,tvars,vars) 
926 
in (cls_str, tfree_lits) end; 

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

927 

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

929 

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

932 

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

935 

17234  936 
fun string_of_symbols predstr funcstr = 
937 
"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

938 

17234  939 
fun string_of_axioms axstr = 
940 
"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

941 

17234  942 
fun string_of_conjectures conjstr = 
943 
"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

944 

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

946 

18798  947 
fun string_of_descrip name = "list_of_descriptions.\nname({*" ^ name ^ "*}).\nauthor({*Isabelle*}).\nstatus(unknown).\ndescription({*autogenerated*}).\nend_of_list.\n\n" 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

948 

17234  949 
fun tfree_dfg_clause tfree_lit = 
17422  950 
"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

951 

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

953 
let val axstrs_tfrees = (map clause2dfg axioms) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

954 
val (axstrs, atfrees) = ListPair.unzip axstrs_tfrees 
17764  955 
val axstr = (space_implode "\n" axstrs) ^ "\n\n" 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

956 
val conjstrs_tfrees = (map clause2dfg conjectures) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

957 
val (conjstrs, atfrees) = ListPair.unzip conjstrs_tfrees 
17775  958 
val tfree_clss = map tfree_dfg_clause (union_all atfrees) 
17764  959 
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

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

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

962 
in 
18798  963 
string_of_start probname ^ string_of_descrip probname ^ 
964 
string_of_symbols funcstr predstr ^ 

965 
string_of_axioms axstr ^ 

966 
string_of_conjectures conjstr ^ "end_problem.\n" 

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

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

968 

18798  969 
fun add_clause_preds (cls,preds) = (preds_of_cls cls) union preds; 
970 
val preds_of_clauses = foldl add_clause_preds [] 

971 

972 
(*FIXME: can replace expensive list operations (ins) by trees (symtab)*) 

973 

974 
fun add_foltype_funcs (AtomV _, funcs) = funcs 

975 
 add_foltype_funcs (AtomF a, funcs) = (a,0) ins funcs 

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

977 
foldl add_foltype_funcs ((a, length tys) ins funcs) tys; 

978 

979 
fun add_folterm_funcs (UVar _, funcs) = funcs 

980 
 add_folterm_funcs (Fun(a,tys,[]), funcs) = (a,0) ins funcs 

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

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

983 
foldl add_foltype_funcs 

984 
(foldl add_folterm_funcs ((a, length tys + length tms) ins funcs) tms) 

985 
tys 

986 

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

988 
foldl add_foltype_funcs (foldl add_folterm_funcs funcs tms) tys; 

989 

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

991 

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

993 
foldl add_literal_funcs funcs literals; 

994 

995 
val funcs_of_clauses = foldl add_clause_funcs [] 

996 

997 

998 
fun clauses2dfg probname axioms conjectures = 

999 
let val clss = conjectures @ axioms 

1000 
in 

1001 
gen_dfg_file probname axioms conjectures 

1002 
(funcs_of_clauses clss) (preds_of_clauses clss) 

1003 
end 

17150
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 

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

1006 
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

1007 
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

1008 

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

1009 
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

1010 

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

1011 
(*FIXME!!! currently is TPTP format!*) 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1012 
fun dfg_of_arLit (TConsLit(b,(c,t,args))) = 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1013 
let val pol = if b then "++" else "" 
18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

1014 
val arg_strs = paren_pack args 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

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

1016 
pol ^ c ^ "(" ^ t ^ arg_strs ^ ")" 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

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

1018 
 dfg_of_arLit (TVarLit(b,(c,str))) = 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1019 
let val pol = if b then "++" else "" 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

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

1021 
pol ^ c ^ "(" ^ str ^ ")" 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

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

1023 

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

1024 

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

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

1026 

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

1027 

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

1028 
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

1029 

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

1030 

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

1031 

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

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

1033 

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

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

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

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

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

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

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

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

1041 
"clause( %(" ^ knd ^ ")\n" ^ "or( " ^ (bracket_pack all_lits) ^ ")),\n" ^ 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1042 
arcls_id ^ ")." 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

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

1044 

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

1045 

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

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

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

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

1049 

15347  1050 
fun tptp_literal (Literal(pol,pred,tag)) = 
1051 
let val pred_string = string_of_predicate pred 

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

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

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

1054 
else (if pol then "++" else "") 
15347  1055 
in 
1056 
tagged_pol ^ pred_string 

1057 
end; 

1058 

18798  1059 
fun tptp_of_typeLit (LTVar (s,ty)) = "" ^ s ^ "(" ^ ty ^ ")" 
1060 
 tptp_of_typeLit (LTFree (s,ty)) = "++" ^ s ^ "(" ^ ty ^ ")"; 

15347  1061 

1062 

1063 
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

1064 
"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

1065 
knd ^ "," ^ lits ^ ")."; 
15347  1066 

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

1067 
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

1068 
"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

1069 
knd ^ ",[" ^ tfree_lit ^ "])."; 
15347  1070 

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

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

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

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

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

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

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

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

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

1082 
(tvar_lits_strs @ lits, tfree_lits) 
15347  1083 
end; 
1084 

1085 
fun tptp_clause cls = 

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

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

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

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

1091 
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

1092 
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

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

1095 
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

1096 
typ_clss (k+1) tfrees 
15347  1097 
in 
1098 
cls_str :: (typ_clss 0 tfree_lits) 

1099 
end; 

1100 

15608  1101 
fun clause2tptp cls = 
17422  1102 
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

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

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

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

1107 
val lits_str = bracket_pack lits 
15608  1108 
val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) 
1109 
in 

1110 
(cls_str,tfree_lits) 

1111 
end; 

1112 

1113 

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

1114 
fun tfree_clause tfree_lit = 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1115 
"input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "])."; 
15608  1116 

15347  1117 

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

1118 
fun tptp_of_arLit (TConsLit(b,(c,t,args))) = 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1119 
let val pol = if b then "++" else "" 
18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

1120 
val arg_strs = paren_pack args 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

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

1122 
pol ^ c ^ "(" ^ t ^ arg_strs ^ ")" 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

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

1124 
 tptp_of_arLit (TVarLit(b,(c,str))) = 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1125 
let val pol = if b then "++" else "" 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

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

1127 
pol ^ c ^ "(" ^ str ^ ")" 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1128 
end; 
15347  1129 

1130 

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

1131 
fun tptp_of_conclLit (ArityClause arcls) = tptp_of_arLit (#conclLit arcls); 
15347  1132 

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

1133 
fun tptp_of_premLits (ArityClause arcls) = map tptp_of_arLit (#premLits arcls); 
15347  1134 

1135 
fun tptp_arity_clause arcls = 

1136 
let val arcls_id = string_of_arClauseID arcls 

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

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

1138 
val prems_lits = tptp_of_premLits arcls 
15347  1139 
val knd = string_of_arKind arcls 
1140 
val all_lits = concl_lit :: prems_lits 

1141 
in 

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

1142 
"input_clause(" ^ arcls_id ^ "," ^ knd ^ "," ^ 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

1143 
(bracket_pack all_lits) ^ ")." 
15347  1144 
end; 
1145 

1146 
fun tptp_classrelLits sub sup = 

1147 
let val tvar = "(T)" 

1148 
in 

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

1149 
"[" ^ sub ^ tvar ^ ",++" ^ sup ^ tvar ^ "]" 
15347  1150 
end; 
1151 

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

1152 
fun tptp_classrelClause (ClassrelClause {clause_id,subclass,superclass,...}) = 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

1153 
let val relcls_id = clrelclause_prefix ^ ascii_of subclass ^ "_" ^ 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

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

1155 
val lits = tptp_classrelLits (make_type_class subclass) (make_type_class superclass) 
15347  1156 
in 
1157 
"input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ")." 

1158 
end; 

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

1159 

15347  1160 
end; 