author  paulson 
Tue, 28 Feb 2006 11:09:50 +0100  
changeset 19155  b294c097767e 
parent 18920  7635e0060cd4 
child 19176  52b6ecd0433a 
permissions  rwrr 
15347  1 
(* Author: Jia Meng, Cambridge University Computer Laboratory 
2 
ID: $Id$ 

3 
Copyright 2004 University of Cambridge 

4 

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

6 
Typed equality is treated differently. 

7 
*) 

8 

9 
signature RES_CLAUSE = 

10 
sig 

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

13 
type fol_type 

14 
type typ_var 

15 
type type_literal 

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

17 
val arity_clause_thy: theory > arityClause list 

18 
val ascii_of : string > string 

19 
val bracket_pack : string list > string 

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

21 
val classrel_clauses_thy: theory > classrelClause list 

22 
val clause_eq : clause * clause > bool 

23 
val clause_prefix : string 

24 
val clause2tptp : clause > string * string list 

25 
val const_prefix : string 

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

27 
val fixed_var_prefix : string 

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

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

30 
val get_axiomName : clause > string 

31 
val hash_clause : clause > int 

32 
val init : theory > unit 

33 
val isMeta : string > bool 

34 
val isTaut : clause > bool 

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

35 
val keep_types : bool ref 
18868  36 
val list_ord : ('a * 'b > order) > 'a list * 'b list > order 
18920  37 
val make_axiom_clause : Term.term > string * int > clause option 
17888  38 
val make_conjecture_clauses : term list > clause list 
18868  39 
val make_fixed_const : string > string 
40 
val make_fixed_type_const : string > string 

41 
val make_fixed_type_var : string > string 

42 
val make_fixed_var : string > string 

43 
val make_schematic_type_var : string * int > string 

44 
val make_schematic_var : string * int > string 

45 
val make_type_class : string > string 

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

47 
val mk_typ_var_sort : Term.typ > typ_var * sort 

48 
val paren_pack : string list > string 

49 
val schematic_var_prefix : string 

50 
val special_equal : bool ref 

51 
val string_of_fol_type : fol_type > string 

52 
val tconst_prefix : string 

53 
val tfree_prefix : string 

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

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

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

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

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

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

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

66 
structure ResClause : RES_CLAUSE = 
15347  67 
struct 
68 

69 
(* Added for typed equality *) 

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

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

72 

73 

74 
val schematic_var_prefix = "V_"; 

75 
val fixed_var_prefix = "v_"; 

76 

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

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

78 
val tfree_prefix = "t_"; 
15347  79 

80 
val clause_prefix = "cls_"; 

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

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

82 
val clrelclause_prefix = "clsrel_"; 
15347  83 

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

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

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

86 
val class_prefix = "class_"; 
15347  87 

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

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

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

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

94 
("op <", "less"), 

95 
("op &", "and"), 

96 
("op ", "or"), 

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

99 
("op *", "times"), 

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

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

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

15347  108 

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

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

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

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

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

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

116 
The character _ goes to __ 

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

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

119 
local 

120 

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

122 

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

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

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

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

129 
else "" 

15347  130 

15610  131 
in 
132 

133 
val ascii_of = String.translate ascii_of_c; 

134 

135 
end; 

15347  136 

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

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

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

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

140 

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

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

142 

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

143 

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

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

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

146 
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

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

148 

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

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

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

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

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

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

156 
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

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

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

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

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

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

163 

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

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

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

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

168 

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

169 
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

170 
 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

171 

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

172 
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

173 

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

175 

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

176 

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

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

179 
val keep_types = ref true; 
15347  180 

181 
datatype kind = Axiom  Hypothesis  Conjecture; 

182 
fun name_of_kind Axiom = "axiom" 

183 
 name_of_kind Hypothesis = "hypothesis" 

184 
 name_of_kind Conjecture = "conjecture"; 

185 

186 
type clause_id = int; 

187 
type axiom_name = string; 

188 

189 

190 
type polarity = bool; 

191 

18869
00741f7280f7
removal of ResClause.num_of_clauses and other simplifications
paulson
parents:
18868
diff
changeset

192 
(* "tag" is used for vampire specific syntax FIXME REMOVE *) 
15347  193 
type tag = bool; 
194 

195 

196 
(**** Isabelle FOL clauses ****) 

197 

198 
val tagged = ref false; 

199 

200 
type pred_name = string; 

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

201 

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

202 
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

203 

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

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

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

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

208 

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

209 
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

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

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

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

213 

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

214 
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

215 
 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

216 
 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

217 

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

218 

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

15347  221 

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

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

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

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

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

227 

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

230 

231 

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

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

235 
axiom_name: axiom_name, 

236 
kind: kind, 

237 
literals: literal list, 

18869
00741f7280f7
removal of ResClause.num_of_clauses and other simplifications
paulson
parents:
18868
diff
changeset

238 
types_sorts: (typ_var * sort) list}; 
00741f7280f7
removal of ResClause.num_of_clauses and other simplifications
paulson
parents:
18868
diff
changeset

239 

00741f7280f7
removal of ResClause.num_of_clauses and other simplifications
paulson
parents:
18868
diff
changeset

240 
fun get_axiomName (Clause cls) = #axiom_name cls; 
15347  241 

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

242 
exception CLAUSE of string * term; 
15347  243 

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

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

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

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

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

248 

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

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

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

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

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

253 

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

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

255 

18869
00741f7280f7
removal of ResClause.num_of_clauses and other simplifications
paulson
parents:
18868
diff
changeset

256 
fun make_clause (clause_id, axiom_name, kind, literals, types_sorts) = 
17317
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

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

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

260 
Clause {clause_id = clause_id, axiom_name = axiom_name, kind = kind, 
18869
00741f7280f7
removal of ResClause.num_of_clauses and other simplifications
paulson
parents:
18868
diff
changeset

261 
literals = literals, types_sorts = types_sorts}; 
17317
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

262 

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

263 

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

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

265 
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

266 

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

267 
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

268 

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

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

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

271 
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

272 

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

273 

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

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

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

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

278 
val t = make_fixed_type_const a 
18798  279 
in (Comp(t,folTyps), ts) end 
280 
 type_of (TFree (a,s)) = (AtomF(make_fixed_type_var a), [(FOLTFree a, s)]) 

281 
 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

282 
and types_of Ts = 
18798  283 
let val (folTyps,ts) = ListPair.unzip (map type_of Ts) 
284 
in (folTyps, union_all ts) end; 

15390  285 

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

286 

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

287 
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

288 

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

291 
val isMeta = String.isPrefix "METAHYP1_" 

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

292 

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

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

297 
 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

298 
 pred_name_type t = raise CLAUSE("Predicate input unexpected", t); 
15347  299 

15615  300 

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

301 
(* For typed equality *) 
15615  302 
(* here "arg_typ" is the type of "="'s argument's type, not the type of the equality *) 
303 
(* Find type of equality arg *) 

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

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

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

306 
in folT end; 
15347  307 

18798  308 
fun fun_name_type (Const(c,T)) args = (make_fixed_const c, const_types_of (c,T)) 
309 
 fun_name_type (Free(x,T)) args = 

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

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

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

312 
 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

313 

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

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

315 
TVars it contains.*) 
15347  316 
fun term_of (Var(ind_nm,T)) = 
18798  317 
let val (folType,ts) = type_of T 
318 
in (UVar(make_schematic_var ind_nm, folType), ts) end 

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

321 
in 
18798  322 
if isMeta x then (UVar(make_schematic_var(x,0),folType), ts) 
323 
else (Fun(make_fixed_var x, [folType], []), ts) 

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

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

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

326 
let val (f,args) = strip_comb app 
18798  327 
val (funName,(contys,ts1)) = fun_name_type f args 
328 
val (args',ts2) = terms_of args 

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

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

331 
end 
18798  332 
and terms_of ts = ListPair.unzip (map term_of ts) 
15390  333 

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

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

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

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

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

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

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

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

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

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

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

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

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

348 
end; 
15347  349 

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

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

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

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

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

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

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

356 
(pred_of (strip_comb term), polarity, tag); 
15347  357 

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

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

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

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

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

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

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

367 

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

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

369 

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

370 

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

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

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

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

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

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

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

377 
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

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

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

380 

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

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

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

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

384 
 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

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

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

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

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

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

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

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

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

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

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

396 
 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

397 

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

398 

18920  399 
fun term_ord (UVar _, UVar _) = EQUAL 
400 
 term_ord (UVar _, _) = LESS 

401 
 term_ord (Fun _, UVar _) = GREATER 

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

402 
 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

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

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

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

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

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

408 

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

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

411 
 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

412 

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

413 

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

414 

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

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

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

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

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

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

420 

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

421 

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

422 
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

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

424 
 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

425 

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

426 
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

427 

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

428 

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

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

430 

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

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

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

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

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

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

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

437 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

453 

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

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

455 

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

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

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

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

459 
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

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

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

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

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

464 

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

465 

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

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

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

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

469 
 2 => (false,(vars,tvars))) 
18920  470 
 term_eq (UVar _,_) vtvars = (false,vtvars) 
18409
080094128a09
Added functions to test equivalence between clauses.
mengj
parents:
18403
diff
changeset

471 
 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

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

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

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

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

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

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

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

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

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

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

482 

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

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

484 

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

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

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

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

488 
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

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

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

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

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

493 

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

494 

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

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

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

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

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

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

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

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

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

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

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

505 

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

506 

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

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

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

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

510 

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

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

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

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

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

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

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

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

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

519 

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

520 

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

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

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

524 

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

525 

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

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

527 

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

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

529 

18920  530 
fun hashw_term (UVar _, w) = w 
18449  531 
 hashw_term (Fun(f,tps,args), w) = 
532 
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

533 

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

536 

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

539 

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

542 

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

543 

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

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

546 
 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

547 
sorts_on_typs (v,s) (*IGNORE sort "type"*) 
18798  548 
 sorts_on_typs ((FOLTVar indx), s::ss) = 
549 
LTVar(make_type_class s, make_schematic_type_var indx) :: 

550 
sorts_on_typs ((FOLTVar indx), ss) 

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

552 
LTFree(make_type_class s, make_fixed_type_var x) :: 

553 
sorts_on_typs ((FOLTFree x), ss); 

15347  554 

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

555 

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

558 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

574 

17999  575 

18869
00741f7280f7
removal of ResClause.num_of_clauses and other simplifications
paulson
parents:
18868
diff
changeset

576 
(** make axiom and conjecture clauses. **) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

577 

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

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

579 
 get_tvar_strs ((FOLTVar indx,s)::tss) = 
18920  580 
(make_schematic_type_var indx) ins (get_tvar_strs tss) 
581 
 get_tvar_strs((FOLTFree x,s)::tss) = get_tvar_strs tss 

15347  582 

18869
00741f7280f7
removal of ResClause.num_of_clauses and other simplifications
paulson
parents:
18868
diff
changeset

583 
(* check if a clause is firstorder before making a conjecture clause*) 
17888  584 
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

585 
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

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

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

588 
in 
18869
00741f7280f7
removal of ResClause.num_of_clauses and other simplifications
paulson
parents:
18868
diff
changeset

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

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

591 

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

592 
fun make_conjecture_clauses_aux _ [] = [] 
17888  593 
 make_conjecture_clauses_aux n (t::ts) = 
594 
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

595 

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

596 
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

597 

18920  598 
(** Too general means, positive equality literal with a variable X as one operand, 
599 
when X does not occur properly in the other operand. This rules out clearly 

600 
inconsistent clauses such as V=aV=b, though it by no means guarantees soundness. **) 

601 

602 
fun occurs a (UVar(b,_)) = a=b 

603 
 occurs a (Fun (_,_,ts)) = exists (occurs a) ts 

604 

605 
(*Is the first operand a variable that does not properly occur in the second operand?*) 

606 
fun too_general_terms (UVar _, UVar _) = false 

607 
 too_general_terms (Fun _, _) = false 

608 
 too_general_terms (UVar (a,_), t) = not (occurs a t); 

609 

610 
fun too_general_lit (Literal (true,Predicate("equal",_,[x,y]),_)) = 

611 
too_general_terms (x,y) orelse too_general_terms(y,x) 

612 
 too_general_lit _ = false; 

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

613 

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

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

615 
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

616 
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

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

618 
val (lits,types_sorts) = literals_of_term term 
15347  619 
in 
18920  620 
if forall too_general_lit lits then 
621 
(Output.debug ("Omitting " ^ ax_name ^ ": equalities are too general"); 

622 
NONE) 

623 
else SOME (make_clause(cls_id, ax_name, Axiom, sort_lits lits, types_sorts)) 

15347  624 
end; 
625 

626 

627 
(**** Isabelle arities ****) 

628 

629 
exception ARCLAUSE of string; 

630 

631 
type class = string; 

632 
type tcons = string; 

633 

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

15347  636 

637 
datatype arityClause = 

638 
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

639 
axiom_name: axiom_name, 
15347  640 
kind: kind, 
641 
conclLit: arLit, 

642 
premLits: arLit list}; 

643 

644 

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

15347  647 

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

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

649 
 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

650 
 pack_sort(tvar, cls::srt) = (make_type_class cls, tvar) :: pack_sort(tvar, srt); 
15347  651 

18868  652 
fun make_TVarLit (b, (cls,str)) = TVarLit(b, (cls,str)); 
653 
fun make_TConsLit (b, (cls,tcons,tvars)) = 

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

15347  655 

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

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

657 
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

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

660 
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

661 
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

662 
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

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

664 
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

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

666 
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

667 
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

668 
end; 
15347  669 

670 

671 
(**** Isabelle class relations ****) 

672 

673 
datatype classrelClause = 

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

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

677 

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

678 
fun make_axiom_classrelClause n subclass superclass = 
18868  679 
ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of subclass ^ 
680 
"_" ^ Int.toString n, 

681 
subclass = make_type_class subclass, 

682 
superclass = make_type_class superclass}; 

15347  683 

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

684 
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

685 
 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

686 
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

687 
 classrelClauses_of_aux n sub (sup::sups) = 
18868  688 
make_axiom_classrelClause n sub sup :: classrelClauses_of_aux (n+1) sub sups; 
15347  689 

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

690 
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

691 

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

693 

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

696 

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

698 

699 

700 
(** Isabelle arities **) 

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

701 

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

702 
fun arity_clause _ (tcons, []) = [] 
19155  703 
 arity_clause n (tcons, ("HOL.type",_)::ars) = (*ignore*) 
18411
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

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

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

706 
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

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

708 

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

709 
fun multi_arity_clause [] = [] 
19155  710 
 multi_arity_clause ((tcons,ars) :: tc_arlists) = 
711 
(*Reversal ensures that older entries always get the same axiom name*) 

712 
arity_clause 0 (tcons, rev ars) @ 

713 
multi_arity_clause tc_arlists 

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

714 

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

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

716 
let val arities = #arities (Type.rep_tsig (Sign.tsig_of thy)) 
19155  717 
in multi_arity_clause (rev (Symtab.dest arities)) end; 
17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

718 

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

719 

18868  720 
(**** Find occurrences of predicates in clauses ****) 
721 

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

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

724 

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

726 

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

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

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

730 

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

732 

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

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

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

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

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

737 

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

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

741 

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

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

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

744 

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

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

748 

749 
fun preds_of_clauses clauses clsrel_clauses arity_clauses = 

750 
Symtab.dest 

751 
(foldl add_classrelClause_preds 

752 
(foldl add_arityClause_preds 

753 
(foldl add_clause_preds Symtab.empty clauses) 

754 
arity_clauses) 

755 
clsrel_clauses) 

18798  756 

18868  757 
(*** Find occurrences of functions in clauses ***) 
758 

759 
fun add_foltype_funcs (AtomV _, funcs) = funcs 

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

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

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

763 

764 
fun add_folterm_funcs (UVar _, funcs) = funcs 

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

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

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

768 
foldl add_foltype_funcs 

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

770 
tms) 

771 
tys 

18798  772 

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

775 

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

777 

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

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

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

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

781 

18868  782 
fun add_clause_funcs (Clause {literals, ...}, funcs) = 
783 
foldl add_literal_funcs funcs literals 

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

785 

786 
fun funcs_of_clauses clauses arity_clauses = 

787 
Symtab.dest (foldl add_arityClause_funcs 

788 
(foldl add_clause_funcs Symtab.empty clauses) 

789 
arity_clauses) 

790 

791 

792 
(**** Stringoriented operations ****) 

15347  793 

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

795 

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

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

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

799 
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

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

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

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

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

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

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

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

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

808 
 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

809 
 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

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

811 
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

812 
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

813 
in name ^ (paren_pack (terms_as_strings @ typs')) end; 
15347  814 

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

816 
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

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

818 
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

819 
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

820 
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

821 

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

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

823 
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

824 

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

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

826 
string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx); 
18863  827 

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

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

830 

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

831 

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

833 

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

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

837 

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

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

839 

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

841 
 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

842 

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

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

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

846 

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

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

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

851 

18869
00741f7280f7
removal of ResClause.num_of_clauses and other simplifications
paulson
parents:
18868
diff
changeset

852 
fun dfg_clause_aux (Clause{literals, types_sorts, ...}) = 
18868  853 
let val lits = map dfg_literal literals 
18869
00741f7280f7
removal of ResClause.num_of_clauses and other simplifications
paulson
parents:
18868
diff
changeset

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

855 
val tvar_lits_strs = 
18869
00741f7280f7
removal of ResClause.num_of_clauses and other simplifications
paulson
parents:
18868
diff
changeset

856 
if !keep_types then map dfg_of_typeLit tvar_lits else [] 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

857 
val tfree_lits = 
18869
00741f7280f7
removal of ResClause.num_of_clauses and other simplifications
paulson
parents:
18868
diff
changeset

858 
if !keep_types then map dfg_of_typeLit tfree_lits else [] 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

862 

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

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

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

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

866 

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

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

869 

18868  870 
fun dfg_vars (Clause {literals,...}) = 
18920  871 
union_all (map get_uvars (List.concat (map dfg_folterms literals))) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

872 

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

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

876 
val vars = dfg_vars cls 
18798  877 
val tvars = get_tvar_strs types_sorts 
878 
val knd = name_of_kind kind 

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

882 

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

884 

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

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

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

887 

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

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

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

890 

17234  891 
fun string_of_symbols predstr funcstr = 
892 
"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

893 

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

895 

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

899 

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

902 

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

903 
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

904 
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

905 

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

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

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

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

910 

18863  911 
fun dfg_classrelLits sub sup = 
912 
let val tvar = "(T)" 

913 
in 

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

915 
end; 

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

916 

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

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

920 

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

922 
let val arcls_id = string_of_arClauseID arcls 

923 
val knd = name_of_kind kind 

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

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

18863  926 
in 
18868  927 
"clause( %(" ^ knd ^ ")\n" ^ 
928 
dfg_forall tvars ("or( " ^ commas lits ^ ")") ^ ",\n" ^ 

929 
arcls_id ^ ").\n\n" 

18863  930 
end; 
931 

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

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

934 
let 

935 
val conjectures = make_conjecture_clauses (map prop_of ths) 

18868  936 
val (dfg_clss, tfree_litss) = ListPair.unzip (map clause2dfg conjectures) 
18863  937 
val clss = conjectures @ axclauses 
18868  938 
val funcs = funcs_of_clauses clss arity_clauses 
939 
and preds = preds_of_clauses clss classrel_clauses arity_clauses 

18863  940 
and probname = Path.pack (Path.base (Path.unpack filename)) 
18868  941 
val (axstrs, _) = ListPair.unzip (map clause2dfg axclauses) 
18863  942 
val tfree_clss = map dfg_tfree_clause (union_all tfree_litss) 
19155  943 
val out = TextIO.openOut filename 
18863  944 
in 
18868  945 
TextIO.output (out, string_of_start probname); 
946 
TextIO.output (out, string_of_descrip probname); 

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

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

949 
writeln_strs out axstrs; 

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

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

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

953 
writeln_strs out tfree_clss; 

954 
writeln_strs out dfg_clss; 

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

956 
TextIO.closeOut out 

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

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

958 

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

959 

18869
00741f7280f7
removal of ResClause.num_of_clauses and other simplifications
paulson
parents:
18868
diff
changeset

960 
(**** Produce TPTP files ****) 
18868  961 

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

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

964 
 tptp_sign false s = "" ^ s 

965 

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

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

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

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

970 
else (if pol then "++" else "") 
15347  971 
in 
972 
tagged_pol ^ pred_string 

973 
end; 

974 

18798  975 
fun tptp_of_typeLit (LTVar (s,ty)) = "" ^ s ^ "(" ^ ty ^ ")" 
976 
 tptp_of_typeLit (LTFree (s,ty)) = "++" ^ s ^ "(" ^ ty ^ ")"; 

15347  977 

978 
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

979 
"input_clause(" ^ string_of_clausename (cls_id,ax_name) ^ "," ^ 
18863  980 
knd ^ "," ^ lits ^ ").\n"; 
15347  981 

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

982 
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

983 
"input_clause(" ^ string_of_type_clsname (cls_id,ax_name,idx) ^ "," ^ 
18863  984 
knd ^ ",[" ^ tfree_lit ^ "]).\n"; 
15347  985 

18869
00741f7280f7
removal of ResClause.num_of_clauses and other simplifications
paulson
parents:
18868
diff
changeset

986 
fun tptp_type_lits (Clause {literals, types_sorts, ...}) = 
00741f7280f7
removal of ResClause.num_of_clauses and other simplifications
paulson
parents:
18868
diff
changeset

987 
let val lits = map tptp_literal literals 
00741f7280f7
removal of ResClause.num_of_clauses and other simplifications
paulson
parents:
18868
diff
changeset

988 
val (tvar_lits,tfree_lits) = add_typs_aux types_sorts 
00741f7280f7
removal of ResClause.num_of_clauses and other simplifications
paulson
parents:
18868
diff
changeset

989 
val tvar_lits_strs = 
00741f7280f7
removal of ResClause.num_of_clauses and other simplifications
paulson
parents:
18868
diff
changeset

990 
if !keep_types then map tptp_of_typeLit tvar_lits else [] 
00741f7280f7
removal of ResClause.num_of_clauses and other simplifications
paulson
parents:
18868
diff
changeset

991 
val tfree_lits = 
00741f7280f7
removal of ResClause.num_of_clauses and other simplifications
paulson
parents:
18868
diff
changeset

992 
if !keep_types then map tptp_of_typeLit tfree_lits else [] 
15347  993 
in 
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset

994 
(tvar_lits_strs @ lits, tfree_lits) 
15347  995 
end; 
996 

18869
00741f7280f7
removal of ResClause.num_of_clauses and other simplifications
paulson
parents:
18868
diff
changeset

997 
fun clause2tptp (cls as Clause {clause_id, axiom_name, kind, ...}) = 
17422  998 
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

999 
(*"lits" includes the typing assumptions (TVars)*) 
18869
00741f7280f7
removal of ResClause.num_of_clauses and other simplifications
paulson
parents:
18868
diff
changeset

1000 
val knd = name_of_kind kind 
00741f7280f7
removal of ResClause.num_of_clauses and other simplifications
paulson
parents:
18868
diff
changeset

1001 
val cls_str = gen_tptp_cls(clause_id, axiom_name, knd, bracket_pack lits) 
15608  1002 
in 
1003 
(cls_str,tfree_lits) 

1004 
end; 

1005 

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

15608  1008 

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

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

1011 
 tptp_of_arLit (TVarLit(b,(c,str))) = 
18868  1012 
tptp_sign b (c ^ "(" ^ str ^ ")") 
15347  1013 

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

1016 
val knd = name_of_kind kind 

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

1018 
in 

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

1020 
end; 

15347  1021 

1022 
fun tptp_classrelLits sub sup = 

1023 
let val tvar = "(T)" 

1024 
in 

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

1025 
"[" ^ sub ^ tvar ^ ",++" ^ sup ^ tvar ^ "]" 
15347  1026 
end; 
1027 

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

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

1030 

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

1033 
let 

1034 
val clss = make_conjecture_clauses (map prop_of ths) 

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

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

1037 
val out = TextIO.openOut filename 

1038 
in 

18869
00741f7280f7
removal of ResClause.num_of_clauses and other simplifications
paulson
parents:
18868
diff
changeset

1039 
List.app (curry TextIO.output out o #1 o clause2tptp) axclauses; 
18863  1040 
writeln_strs out tfree_clss; 
1041 
writeln_strs out tptp_clss; 

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

18863  1044 
TextIO.closeOut out 
1045 
end; 

1046 

15347  1047 
end; 