author  paulson 
Tue, 22 Nov 2005 10:09:11 +0100  
changeset 18218  9a7ffce389c3 
parent 18199  d236379ea408 
child 18275  86cefba6d325 
permissions  rwrr 
15347  1 
(* Author: Jia Meng, Cambridge University Computer Laboratory 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

2 

15347  3 
ID: $Id$ 
4 
Copyright 2004 University of Cambridge 

5 

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

7 
Typed equality is treated differently. 

8 
*) 

9 

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

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

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

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

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

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

16 

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

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

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

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

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

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

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

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

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

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

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

28 

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

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

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

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

33 

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

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

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

36 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

51 

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

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

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

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

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

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

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

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

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

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

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

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

65 
type typ_var 

66 
val mk_typ_var_sort : Term.typ > typ_var * sort 

67 
type type_literal 

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

69 
val gen_tptp_cls : int * string * string * string > string 

70 
val gen_tptp_type_cls : int * string * string * string * int > string 

71 
val tptp_of_typeLit : type_literal > string 

15347  72 
end; 
73 

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

74 
structure ResClause: RES_CLAUSE = 
15347  75 
struct 
76 

77 
(* Added for typed equality *) 

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

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

80 

81 

82 
val schematic_var_prefix = "V_"; 

83 
val fixed_var_prefix = "v_"; 

84 

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

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

86 
val tfree_prefix = "t_"; 
15347  87 

88 
val clause_prefix = "cls_"; 

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

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

90 
val clrelclause_prefix = "clsrel_"; 
15347  91 

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

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

93 
val tconst_prefix = "tc_"; 
15347  94 

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

95 
val class_prefix = "class_"; 
15347  96 

97 

17775  98 
fun union_all xss = foldl (op union) [] xss; 
99 

15347  100 

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

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

105 
("op <", "less"), 

106 
("op &", "and"), 

107 
("op ", "or"), 

17375  108 
("op +", "plus"), 
109 
("op ", "minus"), 

110 
("op *", "times"), 

15347  111 
("op >", "implies"), 
17375  112 
("{}", "emptyset"), 
15347  113 
("op :", "in"), 
114 
("op Un", "union"), 

115 
("op Int", "inter")]; 

116 

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

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

118 
Symtab.make [("*", "t_prod"), 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

119 
("+", "t_sum"), 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

120 
("~=>", "t_map")]; 
15347  121 

15610  122 
(*Escaping of special characters. 
123 
Alphanumeric characters are left unchanged. 

124 
The character _ goes to __ 

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

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

127 
local 

128 

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

130 

15347  131 
fun ascii_of_c c = 
15610  132 
if Char.isAlphaNum c then String.str c 
133 
else if c = #"_" then "__" 

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

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

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

137 
else "" 

15347  138 

15610  139 
in 
140 

141 
val ascii_of = String.translate ascii_of_c; 

142 

143 
end; 

15347  144 

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

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

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

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

148 

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

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

150 

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

151 

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

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

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

154 
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

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

156 

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

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

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

160 
fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v); 
15347  161 
fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x); 
162 

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

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

164 
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

165 
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); 
15347  166 

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

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

169 
SOME c' => c' 
17261  170 
 NONE => const_prefix ^ ascii_of c; 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

171 

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

172 
fun make_fixed_type_const c = 
17412  173 
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

174 
SOME c' => c' 
17261  175 
 NONE => tconst_prefix ^ ascii_of c; 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

176 

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

178 

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

179 

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

180 

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

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

183 
val keep_types = ref true; 
15347  184 

185 
datatype kind = Axiom  Hypothesis  Conjecture; 

186 
fun name_of_kind Axiom = "axiom" 

187 
 name_of_kind Hypothesis = "hypothesis" 

188 
 name_of_kind Conjecture = "conjecture"; 

189 

190 
type clause_id = int; 

191 
type axiom_name = string; 

192 

193 

194 
type polarity = bool; 

195 

196 
type indexname = Term.indexname; 

197 

198 

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

200 
type tag = bool; 

201 

202 

203 
(**** Isabelle FOL clauses ****) 

204 

205 
val tagged = ref false; 

206 

207 
type pred_name = string; 

208 
type sort = Term.sort; 

209 
type fol_type = string; 

210 

211 
datatype type_literal = LTVar of string  LTFree of string; 

212 

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

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

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

215 
datatype predicate = Predicate of pred_name * fol_type list * folTerm list; 
15347  216 

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

218 

219 
datatype typ_var = FOLTVar of indexname  FOLTFree of string; 

220 

17999  221 
fun mk_typ_var_sort (TFree(a,s)) = (FOLTFree a,s) 
222 
 mk_typ_var_sort (TVar(v,s)) = (FOLTVar v,s); 

223 

224 

15347  225 

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

227 
datatype clause = 

228 
Clause of {clause_id: clause_id, 

229 
axiom_name: axiom_name, 

230 
kind: kind, 

231 
literals: literal list, 

232 
types_sorts: (typ_var * sort) list, 

233 
tvar_type_literals: type_literal list, 

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

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

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

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

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

238 

15347  239 

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

240 
exception CLAUSE of string * term; 
15347  241 

242 

243 
(*** make clauses ***) 

244 

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

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

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

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

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

249 

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

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

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

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

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

254 

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

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

256 

17234  257 
fun make_clause (clause_id,axiom_name,kind,literals, 
258 
types_sorts,tvar_type_literals, 

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

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

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

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

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

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

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

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

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

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

269 

15347  270 

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

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

272 

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

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

274 

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

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

276 

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

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

278 

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

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

280 

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

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

282 

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

283 

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

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

285 
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

286 

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

287 
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

288 

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

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

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

291 
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

292 

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

293 

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

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

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

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

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

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

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

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

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

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

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

304 
in (t, ([((FOLTFree a),s)], [(t,0)])) end 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

305 
 type_of (TVar (v, s)) = (make_schematic_type_var v, ([((FOLTVar v),s)], [])) 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

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

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

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

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

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

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

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

313 

15390  314 

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

315 
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

316 

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

319 
val isMeta = String.isPrefix "METAHYP1_" 

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

320 

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

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

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

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

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

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

327 
 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

328 
 pred_name_type t = raise CLAUSE("Predicate input unexpected", t); 
15347  329 

15615  330 

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

331 
(* For typed equality *) 
15615  332 
(* here "arg_typ" is the type of "="'s argument's type, not the type of the equality *) 
333 
(* Find type of equality arg *) 

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

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

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

336 
in folT end; 
15347  337 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

351 
 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

352 

15615  353 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

389 
 term_of t = raise CLAUSE("Function Not First Order 4", t) 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

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

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

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

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

394 
end 
15390  395 

15347  396 

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

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

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

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

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

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

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

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

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

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

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

409 
val (args',(ts2,ffuncs)) = terms_of args 
17775  410 
val ts3 = union_all (ts1::ts2) 
411 
val ffuncs' = union_all ffuncs 

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

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

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

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

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

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

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

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

420 
end; 
15347  421 

422 

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

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

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

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

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

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

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

429 
(pred_of (strip_comb term), polarity, tag); 
15347  430 

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

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

17234  434 
in 
17888  435 
literals_of_term1 (lits', ts', preds' union preds, funcs' union funcs) Q 
17234  436 
end 
17888  437 
 literals_of_term1 (lits, ts, preds, funcs) P = 
438 
let val ((pred, ts', preds', funcs'), pol, tag) = predicate_of (P,true,false) 

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

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

443 

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

444 

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

446 

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

447 

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

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

449 

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

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

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

452 
 sorts_on_typs (v, "HOL.type" :: s) = 
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset

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

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

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

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

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

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

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

460 
(sorts_on_typs ((FOLTFree x), ss)); 
15347  461 

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

462 

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

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

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

466 

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

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

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

469 

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

470 

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

471 

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

472 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

490 

17999  491 
fun add_typs_aux2 [] = ([],[]) 
492 
 add_typs_aux2 ((FOLTVar indx,s)::tss) = 

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

494 
val (vss,fss) = add_typs_aux2 tss 

495 
in 

496 
(vs union vss,fss) 

497 
end 

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

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

500 
val (vss,fss) = add_typs_aux2 tss 

501 
in 

502 
(vss,fs union fss) 

503 
end; 

504 

505 

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

506 
fun add_typs (Clause cls) preds = add_typs_aux (#types_sorts cls) preds 
15347  507 

508 

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

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

510 

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

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

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

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

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

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

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

518 

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

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

520 

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

521 
fun make_axiom_clause_thm thm (ax_name,cls_id) = 
17888  522 
let val (lits,types_sorts, preds, funcs) = literals_of_term (prop_of thm) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

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

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

526 
make_clause(cls_id,ax_name,Axiom, 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

528 
tvars, preds, funcs) 
15347  529 
end; 
530 

531 

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

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

534 
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

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

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

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

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

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

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

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

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

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

544 

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

545 
fun make_conjecture_clauses_aux _ [] = [] 
17888  546 
 make_conjecture_clauses_aux n (t::ts) = 
547 
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

548 

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

549 
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

550 

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

551 

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

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

553 
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

554 
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

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

556 
val (lits,types_sorts, preds,funcs) = literals_of_term term 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

560 
make_clause(cls_id,ax_name,Axiom, 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

562 
tvars, preds,funcs) 
15347  563 
end; 
564 

565 

566 

567 

568 
(**** Isabelle arities ****) 

569 

570 
exception ARCLAUSE of string; 

571 

572 

573 
type class = string; 

574 
type tcons = string; 

575 

576 

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

578 

579 
datatype arityClause = 

580 
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

581 
axiom_name: axiom_name, 
15347  582 
kind: kind, 
583 
conclLit: arLit, 

584 
premLits: arLit list}; 

585 

586 

587 
fun get_TVars 0 = [] 

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

588 
 get_TVars n = ("T_" ^ (Int.toString n)) :: get_TVars (n1); 
15347  589 

590 

591 

592 
fun pack_sort(_,[]) = raise ARCLAUSE("Empty Sort Found") 

593 
 pack_sort(tvar, [cls]) = [(make_type_class cls, tvar)] 

594 
 pack_sort(tvar, cls::srt) = (make_type_class cls,tvar) :: (pack_sort(tvar, srt)); 

595 

596 

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

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

599 

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

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

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

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

603 
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

604 
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

605 
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

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

607 
ArityClause {clause_id = n, kind = Axiom, 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

608 
axiom_name = tcons, 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

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

610 
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

611 
end; 
15347  612 

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

613 
(*The number of clauses generated from cls, including type clauses*) 
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset

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

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

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

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

618 
in 1 + num_tfree_lits end; 
15347  619 

620 

621 
(**** Isabelle class relations ****) 

622 

623 

624 
datatype classrelClause = 

625 
ClassrelClause of {clause_id: clause_id, 

626 
subclass: class, 

15531  627 
superclass: class option}; 
15347  628 

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

629 

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

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

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

632 
subclass = subclass, superclass = superclass}; 
15347  633 

634 

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

635 
fun classrelClauses_of_aux n sub [] = [] 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

636 
 classrelClauses_of_aux n sub (sup::sups) = 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

637 
make_axiom_classrelClause n sub (SOME sup) :: classrelClauses_of_aux (n+1) sub sups; 
15347  638 

639 

640 
fun classrelClauses_of (sub,sups) = 

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

641 
case sups of [] => [make_axiom_classrelClause 0 sub NONE] 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

642 
 _ => classrelClauses_of_aux 0 sub sups; 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

643 

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

644 

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

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

646 

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

647 

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

648 
fun arity_clause _ (tcons, []) = [] 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

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

650 
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

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

652 

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

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

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

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

656 

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

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

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

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

660 

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

661 

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

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

663 

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

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

665 

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

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

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

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

669 

15347  670 

671 

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

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

673 

15347  674 
fun wrap_eq_type typ t = eq_typ_wrapper ^"(" ^ t ^ "," ^ typ ^ ")"; 
675 

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

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

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

679 
let val [tstr1,tstr2] = map string_of_term terms 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

682 
then "equal(" ^ (wrap_eq_type typ tstr1) ^ "," ^ 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

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

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

687 
 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

688 
 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

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

690 
let val terms_as_strings = map string_of_term terms 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

691 
in name ^ (paren_pack (terms_as_strings @ typs)) end 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

692 
 string_of_term _ = error "string_of_term"; 
15347  693 

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

695 
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

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

697 
let val terms_as_strings = map string_of_term terms 
18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

698 
in name ^ (paren_pack (terms_as_strings @ typs)) end 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

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

700 

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

701 

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

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

703 
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

704 

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

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

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

707 

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

708 

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

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

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

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

712 

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

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

714 
let val pred_string = string_of_predicate pred 
17234  715 
in 
716 
if pol then pred_string else "not(" ^pred_string ^ ")" 

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

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

718 

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

719 

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

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

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

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

723 

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

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

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

726 

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

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

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

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

730 

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

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

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

733 

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

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

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

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

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

738 

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

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

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

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

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

743 

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

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

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

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

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

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

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

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

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

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

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

755 

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

756 

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

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

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

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

760 

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

761 

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

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

764 

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

765 

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

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

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

768 

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

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

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

771 

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

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

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

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

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

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

778 

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

779 

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

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

781 

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

782 

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

783 

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

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

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

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

787 

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

788 

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

789 

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

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

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

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

793 

17234  794 
fun dfg_pred (Literal(pol,pred,tag)) ax_name = 
795 
(string_of_predname pred) ^ " " ^ ax_name 

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

796 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

814 

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

815 
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

816 

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

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

819 

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

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

822 

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

823 

17234  824 
fun string_of_symbols predstr funcstr = 
825 
"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

826 

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

827 

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

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

830 

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

831 

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

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

834 

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

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

837 

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

838 

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

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

840 

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

841 

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

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

843 

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

844 

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

845 
fun clause2dfg cls = 
17234  846 
let val (lits,tfree_lits) = dfg_clause_aux cls 
847 
(*"lits" includes the typing assumptions (TVars)*) 

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

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

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

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

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

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

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

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

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

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

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

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

860 

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

861 

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

862 

17234  863 
fun tfree_dfg_clause tfree_lit = 
17422  864 
"clause( %(conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ")." 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

865 

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

866 

17422  867 
fun gen_dfg_file probname axioms conjectures funcs preds = 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

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

872 
val (conjstrs, atfrees) = ListPair.unzip conjstrs_tfrees 
17775  873 
val tfree_clss = map tfree_dfg_clause (union_all atfrees) 
17764  874 
val conjstr = (space_implode "\n" (tfree_clss@conjstrs)) ^ "\n\n" 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

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

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

878 
(string_of_start probname) ^ (string_of_descrip ()) ^ 
17764  879 
(string_of_symbols funcstr predstr) ^ 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

880 
(string_of_axioms axstr) ^ 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

883 

17422  884 
fun clauses2dfg [] probname axioms conjectures funcs preds = 
17775  885 
let val funcs' = (union_all(map funcs_of_cls axioms)) @ funcs 
886 
val preds' = (union_all(map preds_of_cls axioms)) @ preds 

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

887 
in 
17422  888 
gen_dfg_file probname axioms conjectures funcs' preds' 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

889 
end 
17422  890 
 clauses2dfg (cls::clss) probname axioms conjectures funcs preds = 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

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

894 
val ax_name = get_axiomName cls 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

895 
val vars = dfg_vars cls 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

896 
val tvars = dfg_tvars cls 
17888  897 
val funcs' = (funcs_of_cls cls) union funcs 
898 
val preds' = (preds_of_cls cls) union preds 

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

899 
val knd = string_of_kind cls 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

900 
val lits_str = concat_with ", " lits 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

901 
val axioms' = if knd = "axiom" then (cls::axioms) else axioms 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

902 
val conjectures' = 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

903 
if knd = "conjecture" then (cls::conjectures) else conjectures 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

904 
in 
17422  905 
clauses2dfg clss probname axioms' conjectures' funcs' preds' 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

907 

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

908 

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

909 
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

910 
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

911 

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

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

913 

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

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

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

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

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

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

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

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

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

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

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

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

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

926 

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

927 

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

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

929 

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

930 

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

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

932 

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

933 

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

934 

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

935 
(*FIXME: would this have variables in a forall? *) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

936 

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

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

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

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

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

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

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

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

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

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

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

947 

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

948 

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

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

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

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

952 

15347  953 
fun tptp_literal (Literal(pol,pred,tag)) = 
954 
let val pred_string = string_of_predicate pred 

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

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

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

957 
else (if pol then "++" else "") 
15347  958 
in 
959 
tagged_pol ^ pred_string 

960 
end; 

961 

962 
fun tptp_of_typeLit (LTVar x) = "" ^ x 

963 
 tptp_of_typeLit (LTFree x) = "++" ^ x; 

964 

965 

966 
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

967 
"input_clause(" ^ string_of_clausename (cls_id,ax_name) ^ "," ^ 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

968 
knd ^ "," ^ lits ^ ")."; 
15347  969 

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

970 
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

971 
"input_clause(" ^ string_of_type_clsname (cls_id,ax_name,idx) ^ "," ^ 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

972 
knd ^ ",[" ^ tfree_lit ^ "])."; 
15347  973 

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

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

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

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

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

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

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

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

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

985 
(tvar_lits_strs @ lits, tfree_lits) 
15347  986 
end; 
987 

988 
fun tptp_clause cls = 

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

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

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

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

994 
val lits_str = bracket_pack lits 
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset

995 
val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) 
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset

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

998 
gen_tptp_type_cls(cls_id,ax_name,knd,tfree,k) :: 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

999 
typ_clss (k+1) tfrees 
15347  1000 
in 
1001 
cls_str :: (typ_clss 0 tfree_lits) 

1002 
end; 

1003 

15608  1004 
fun clause2tptp cls = 
17422  1005 
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

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

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

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

1010 
val lits_str = bracket_pack lits 
15608  1011 
val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) 
1012 
in 

1013 
(cls_str,tfree_lits) 

1014 
end; 

1015 

1016 

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

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

1018 
"input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "])."; 
15608  1019 

15347  1020 

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

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

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

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

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

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

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

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

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

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

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

1031 
end; 
15347  1032 

1033 

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

1034 
fun tptp_of_conclLit (ArityClause arcls) = tptp_of_arLit (#conclLit arcls); 
15347  1035 

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

1036 
fun tptp_of_premLits (ArityClause arcls) = map tptp_of_arLit (#premLits arcls); 
15347  1037 

1038 
fun tptp_arity_clause arcls = 

1039 
let val arcls_id = string_of_arClauseID arcls 

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

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

1041 
val prems_lits = tptp_of_premLits arcls 
15347  1042 
val knd = string_of_arKind arcls 
1043 
val all_lits = concl_lit :: prems_lits 

1044 
in 

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

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

1046 
(bracket_pack all_lits) ^ ")." 
15347  1047 
end; 
1048 

1049 
fun tptp_classrelLits sub sup = 

1050 
let val tvar = "(T)" 

1051 
in 

15531  1052 
case sup of NONE => "[++" ^ sub ^ tvar ^ "]" 
1053 
 (SOME supcls) => "[" ^ sub ^ tvar ^ ",++" ^ supcls ^ tvar ^ "]" 

15347  1054 
end; 
1055 

1056 

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

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

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

1059 
Int.toString clause_id 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

1060 
val lits = tptp_classrelLits (make_type_class subclass) 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

1061 
(Option.map make_type_class superclass) 
15347  1062 
in 
1063 
"input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ")." 

1064 
end; 

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

1065 

15347  1066 
end; 