author  paulson 
Fri, 14 Oct 2005 10:19:50 +0200  
changeset 17845  1438291d57f0 
parent 17775  2679ba74411f 
child 17888  116a8d1c7a67 
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 
17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

24 
val make_conjecture_clauses : thm 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 
15347  51 
end; 
52 

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

53 
structure ResClause: RES_CLAUSE = 
15347  54 
struct 
55 

56 
(* Added for typed equality *) 

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

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

59 

60 

61 
val schematic_var_prefix = "V_"; 

62 
val fixed_var_prefix = "v_"; 

63 

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

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

65 
val tfree_prefix = "t_"; 
15347  66 

67 
val clause_prefix = "cls_"; 

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

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

69 
val clrelclause_prefix = "clsrel_"; 
15347  70 

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

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

72 
val tconst_prefix = "tc_"; 
15347  73 

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

74 
val class_prefix = "class_"; 
15347  75 

76 

17775  77 
fun union_all xss = foldl (op union) [] xss; 
78 

15347  79 

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

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

84 
("op <", "less"), 

85 
("op &", "and"), 

86 
("op ", "or"), 

17375  87 
("op +", "plus"), 
88 
("op ", "minus"), 

89 
("op *", "times"), 

15347  90 
("op >", "implies"), 
17375  91 
("{}", "emptyset"), 
15347  92 
("op :", "in"), 
93 
("op Un", "union"), 

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

95 

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

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

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

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

99 
("~=>", "t_map")]; 
15347  100 

15610  101 
(*Escaping of special characters. 
102 
Alphanumeric characters are left unchanged. 

103 
The character _ goes to __ 

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

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

106 
local 

107 

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

109 

15347  110 
fun ascii_of_c c = 
15610  111 
if Char.isAlphaNum c then String.str c 
112 
else if c = #"_" then "__" 

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

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

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

116 
else "" 

15347  117 

15610  118 
in 
119 

120 
val ascii_of = String.translate ascii_of_c; 

121 

122 
end; 

15347  123 

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

124 
(* convert a list of strings into one single string; surrounded by brackets *) 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

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

126 

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

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

128 

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

129 

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

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

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

132 
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

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

134 

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

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

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

138 
fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v); 
15347  139 
fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x); 
140 

16903  141 
(*Type variables contain _H because the character ' translates to that.*) 
16925
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset

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

143 
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

144 
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); 
15347  145 

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

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

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

150 

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

151 
fun make_fixed_type_const c = 
17412  152 
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

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

155 

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

157 

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

158 

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

159 

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

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

162 
val keep_types = ref true; 
15347  163 

164 
datatype kind = Axiom  Hypothesis  Conjecture; 

165 
fun name_of_kind Axiom = "axiom" 

166 
 name_of_kind Hypothesis = "hypothesis" 

167 
 name_of_kind Conjecture = "conjecture"; 

168 

169 
type clause_id = int; 

170 
type axiom_name = string; 

171 

172 

173 
type polarity = bool; 

174 

175 
type indexname = Term.indexname; 

176 

177 

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

179 
type tag = bool; 

180 

181 

182 
(**** Isabelle FOL clauses ****) 

183 

184 
val tagged = ref false; 

185 

186 
type pred_name = string; 

187 
type sort = Term.sort; 

188 
type fol_type = string; 

189 

190 

191 
datatype type_literal = LTVar of string  LTFree of string; 

192 

193 

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

194 
datatype folTerm = UVar of string * fol_type 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

195 
 Fun of string * fol_type * folTerm list; 
15347  196 
datatype predicate = Predicate of pred_name * fol_type * folTerm list; 
197 

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

199 

200 
datatype typ_var = FOLTVar of indexname  FOLTFree of string; 

201 

202 

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

204 
datatype clause = 

205 
Clause of {clause_id: clause_id, 

206 
axiom_name: axiom_name, 

207 
kind: kind, 

208 
literals: literal list, 

209 
types_sorts: (typ_var * sort) list, 

210 
tvar_type_literals: type_literal list, 

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

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

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

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

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

215 

15347  216 

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

217 
exception CLAUSE of string * term; 
15347  218 

219 

220 
(*** make clauses ***) 

221 

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

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

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

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

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

226 

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

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

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

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

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

231 

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

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

233 

17234  234 
fun make_clause (clause_id,axiom_name,kind,literals, 
235 
types_sorts,tvar_type_literals, 

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

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

237 
if forall isFalse literals 
17234  238 
then error "Problem too trivial for resolution (empty clause)" 
239 
else 

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

240 
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

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

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

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

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

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

246 

15347  247 

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

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

249 

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

250 
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

251 

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

252 
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

253 

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

254 
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

255 

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

256 
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

257 

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

258 
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

259 

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

260 

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

261 

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

262 
(*Definitions of the current theoryto allow suppressing types.*) 
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset

263 
val curr_defs = ref Defs.empty; 
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset

264 

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

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

266 
producing any clauses!*) 
17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

267 
fun init thy = (curr_defs := Theory.defs_of thy); 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

268 

16976  269 
fun no_types_needed s = Defs.monomorphic (!curr_defs) s; 
16925
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset

270 

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

271 

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

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

273 
TVars it contains.*) 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

274 
fun type_of (Type (a, [])) = 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

275 
let val t = make_fixed_type_const a 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

276 
in (t,([],[(t,0)])) end 
15347  277 
 type_of (Type (a, Ts)) = 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

280 
val (ts, funcslist) = ListPair.unzip ts_funcs 
17775  281 
val ts' = union_all ts 
282 
val funcs' = union_all funcslist 

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

283 
val t = make_fixed_type_const a 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

284 
in 
17764  285 
((t ^ paren_pack folTyps), (ts', (t, length Ts)::funcs')) 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

287 
 type_of (TFree (a, s)) = 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

288 
let val t = make_fixed_type_var a 
17764  289 
in (t, ([((FOLTFree a),s)],[(t,0)])) end 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

290 
 type_of (TVar (v, s)) = (make_schematic_type_var v, ([((FOLTVar v),s)], [])) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

291 

15390  292 

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

293 
fun maybe_type_of c T = 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

294 
if no_types_needed c then ("",([],[])) else type_of T; 
16925
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset

295 

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

298 
val isMeta = String.isPrefix "METAHYP1_" 

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

299 

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

300 
fun pred_name_type (Const(c,T)) = 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

301 
let val (typof,(folTyps,funcs)) = maybe_type_of c T 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

304 
if isMeta x then raise CLAUSE("Predicate Not First Order 1", Free(x,T)) 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

306 
 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

307 
 pred_name_type t = raise CLAUSE("Predicate input unexpected", t); 
15347  308 

15615  309 

310 
(* For type equality *) 

311 
(* here "arg_typ" is the type of "="'s argument's type, not the type of the equality *) 

312 
(* Find type of equality arg *) 

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

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

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

315 
in folT end; 
15347  316 

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

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

318 
let val t = make_fixed_const c 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

319 
val (typof, (folTyps,funcs)) = maybe_type_of c T 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

320 
val arity = if !keep_types andalso not (no_types_needed c) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

321 
then 1 + length args 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

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

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

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

327 
let val t = make_fixed_var x 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

329 
(t, ("",[]), [(t, length args)]) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

331 
 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

332 

15615  333 

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

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

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

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

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

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

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

342 
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

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

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

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

346 
(ts, ((make_fixed_var x),0)::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 
 term_of (Const(c,T)) = (* impossible to be equality *) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

349 
let val (folType,(ts,funcs)) = type_of T 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

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

351 
(Fun(make_fixed_const c, folType, []), 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

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

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

354 
 term_of (app as (t $ a)) = 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

355 
let val (f,args) = strip_comb app 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

356 
fun term_of_aux () = 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

357 
let val (funName,(funType,ts1),funcs) = fun_name_type f args 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

358 
val (args',ts_funcs) = ListPair.unzip (map term_of args) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

359 
val (ts2,funcs') = ListPair.unzip ts_funcs 
17775  360 
val ts3 = union_all (ts1::ts2) 
361 
val funcs'' = union_all(funcs::funcs') 

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

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

363 
(Fun(funName,funType,args'), (ts3,funcs'')) 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

365 
fun term_of_eq ((Const ("op =", typ)),args) = 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

366 
let val arg_typ = eq_arg_type typ 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

367 
val (args',ts_funcs) = ListPair.unzip (map term_of args) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

369 
val equal_name = make_fixed_const ("op =") 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

371 
(Fun(equal_name,arg_typ,args'), 
17775  372 
(union_all ts, 
373 
(make_fixed_var equal_name, 2):: union_all funcs)) 

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

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

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

376 
case f of Const ("op =", typ) => term_of_eq (f,args) 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

377 
 Const(_,_) => term_of_aux () 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

378 
 Free(s,_) => 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

379 
if isMeta s 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

380 
then raise CLAUSE("Function Not First Order 2", f) 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

381 
else term_of_aux() 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

382 
 _ => raise CLAUSE("Function Not First Order 3", f) 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

384 
 term_of t = raise CLAUSE("Function Not First Order 4", t); 
15390  385 

15347  386 

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

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

388 
let val arg_typ = eq_arg_type typ 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

389 
val (args',ts_funcs) = ListPair.unzip (map term_of args) 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

390 
val (ts,funcs) = ListPair.unzip ts_funcs 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

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

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

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

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

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

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

399 
let val (predName,(predType,ts1), pfuncs) = pred_name_type pred 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

400 
val (args',ts_funcs) = ListPair.unzip (map term_of args) 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

401 
val (ts2,ffuncs) = ListPair.unzip ts_funcs 
17775  402 
val ts3 = union_all (ts1::ts2) 
403 
val ffuncs' = union_all ffuncs 

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

404 
val newfuncs = distinct (pfuncs@ffuncs') 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

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

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

407 
Const (c,_) => 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

408 
if !keep_types andalso not (no_types_needed c) 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

409 
then 1 + length args 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

410 
else length args 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

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

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

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

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

415 
end; 
15347  416 

417 

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

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

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

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

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

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

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

424 
(pred_of (strip_comb term), polarity, tag); 
15347  425 

17234  426 
fun literals_of_term ((Const("Trueprop",_) $ P),lits_ts, preds, funcs) = 
427 
literals_of_term(P,lits_ts, preds, funcs) 

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

428 
 literals_of_term ((Const("op ",_) $ P $ Q),(lits,ts), preds,funcs) = 
17234  429 
let val (lits',ts', preds', funcs') = 
430 
literals_of_term(P,(lits,ts), preds,funcs) 

431 
in 

432 
literals_of_term(Q, (lits',ts'), distinct(preds'@preds), 

433 
distinct(funcs'@funcs)) 

434 
end 

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

435 
 literals_of_term (P,(lits,ts), preds, funcs) = 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

436 
let val ((pred,ts', preds', funcs'), pol, tag) = 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

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

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

442 

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 
fun literals_of_thm thm = literals_of_term (prop_of thm, ([],[]), [], []); 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

445 

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

448 

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

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

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

451 
 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

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

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

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

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

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

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

458 
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

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

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

461 

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

464 
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

465 

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

466 
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

467 
 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

468 

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 

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

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

473 
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

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

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

476 
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

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

478 
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

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

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

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

483 
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

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

485 
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

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

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

489 

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

490 
fun add_typs (Clause cls) preds = add_typs_aux (#types_sorts cls) preds 
15347  491 

492 

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

494 

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

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

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

497 
let val vstr = make_schematic_type_var indx 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

498 
val vstrs = get_tvar_strs tss 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

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

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

502 
 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

503 

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

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

505 

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

506 
fun make_axiom_clause_thm thm (ax_name,cls_id) = 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

507 
let val (lits,types_sorts, preds, funcs) = literals_of_thm thm 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

508 
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

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

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

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

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

513 
tvars, preds, funcs) 
15347  514 
end; 
515 

516 

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

517 

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

518 
fun make_conjecture_clause n thm = 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

519 
let val (lits,types_sorts, preds, funcs) = literals_of_thm thm 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

520 
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

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

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

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

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

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

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

527 

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

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

529 
 make_conjecture_clauses_aux n (th::ths) = 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

530 
make_conjecture_clause n th :: make_conjecture_clauses_aux (n+1) ths 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

531 

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

532 
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

533 

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

534 

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

535 
fun make_axiom_clause term (ax_name,cls_id) = 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

536 
let 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

537 
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

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

540 
make_clause(cls_id,ax_name,Axiom, 
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) 
15347  543 
end; 
544 

545 

546 

547 

548 
(**** Isabelle arities ****) 

549 

550 
exception ARCLAUSE of string; 

551 

552 

553 
type class = string; 

554 
type tcons = string; 

555 

556 

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

558 

559 
datatype arityClause = 

560 
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

561 
axiom_name: axiom_name, 
15347  562 
kind: kind, 
563 
conclLit: arLit, 

564 
premLits: arLit list}; 

565 

566 

567 
fun get_TVars 0 = [] 

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

568 
 get_TVars n = ("T_" ^ (Int.toString n)) :: get_TVars (n1); 
15347  569 

570 

571 

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

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

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

575 

576 

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

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

579 

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

580 
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

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

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

583 
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

584 
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

585 
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

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

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

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

589 
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

590 
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

591 
end; 
15347  592 

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

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

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

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

596 
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

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

598 
in 1 + num_tfree_lits end; 
15347  599 

600 

601 
(**** Isabelle class relations ****) 

602 

603 

604 
datatype classrelClause = 

605 
ClassrelClause of {clause_id: clause_id, 

606 
subclass: class, 

15531  607 
superclass: class option}; 
15347  608 

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

609 

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

610 
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

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

612 
subclass = subclass, superclass = superclass}; 
15347  613 

614 

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

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

616 
 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

617 
make_axiom_classrelClause n sub (SOME sup) :: classrelClauses_of_aux (n+1) sub sups; 
15347  618 

619 

620 
fun classrelClauses_of (sub,sups) = 

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

621 
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

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

623 

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

624 

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

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

626 

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

627 

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

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

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

630 
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

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

632 

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

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

634 
 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

635 
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

636 

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

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

638 
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

639 
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

640 

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

641 

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

642 
(* Isabelle classes *) 
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 
type classrelClauses = classrelClause list Symtab.table; 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

645 

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

646 
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

647 
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

648 
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

649 

15347  650 

651 

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

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

653 

15347  654 
fun wrap_eq_type typ t = eq_typ_wrapper ^"(" ^ t ^ "," ^ typ ^ ")"; 
655 

656 
(* Only need to wrap equality's arguments with "typeinfo" if the output clauses are typed && if we specifically ask for types to be included. *) 

657 
fun string_of_equality (typ,terms) = 

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

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

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

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

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

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

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

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

665 
and string_of_term (UVar(x,_)) = x 
15615  666 
 string_of_term (Fun("equal",typ,terms)) = string_of_equality(typ,terms) 
667 
 string_of_term (Fun (name,typ,[])) = name 

668 
 string_of_term (Fun (name,typ,terms)) = 

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

669 
let val terms' = map string_of_term terms 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

671 
if !keep_types andalso typ<>"" 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

672 
then name ^ (paren_pack (terms' @ [typ])) 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

673 
else name ^ (paren_pack terms') 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

674 
end; 
15347  675 

676 
(* before output the string of the predicate, check if the predicate corresponds to an equality or not. *) 

17234  677 
fun string_of_predicate (Predicate("equal",typ,terms)) = 
678 
string_of_equality(typ,terms) 

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

679 
 string_of_predicate (Predicate(name,_,[])) = name 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

681 
let val terms_as_strings = map string_of_term terms 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

683 
if !keep_types andalso typ<>"" 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

684 
then name ^ (paren_pack (terms_as_strings @ [typ])) 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

685 
else name ^ (paren_pack terms_as_strings) 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

687 

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

688 

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

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

690 
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

691 

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

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

693 
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

694 

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

695 

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

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

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

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

699 

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

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

701 
let val pred_string = string_of_predicate pred 
17234  702 
in 
703 
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

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

705 

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

706 

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

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

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

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

710 

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

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

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

713 

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

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

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

716 
 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

717 

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

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

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

720 

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

721 
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

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

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

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

725 

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

726 
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

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

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

729 
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

730 

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

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

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

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

734 
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

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

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

737 
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

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

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

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

742 

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_folterms (Literal(pol,pred,tag)) = 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

745 
let val Predicate (predname, foltype, folterms) = pred 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

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

749 

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

750 

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

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

753 

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

754 

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

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

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

757 

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

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

759 
 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

760 

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

761 
fun mergelist [] = [] 
17764  762 
 mergelist (x::xs) = x @ mergelist xs 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

763 

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

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

765 
let val lits = #literals cls 
17317
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

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

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

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

770 

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

771 

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

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

773 

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

774 

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

775 

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

776 
(* make this return funcs and preds too? *) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

777 
fun string_of_predname (Predicate("equal",typ,terms)) = "EQUALITY" 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

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

780 

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 
(* make this return funcs and preds too? *) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

783 

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

784 
fun string_of_predicate (Predicate("equal",typ,terms)) = 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

785 
string_of_equality(typ,terms) 
15347  786 
 string_of_predicate (Predicate(name,_,[])) = name 
787 
 string_of_predicate (Predicate(name,typ,terms)) = 

16903  788 
let val terms_as_strings = map string_of_term terms 
789 
in 

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

790 
if !keep_types andalso typ<>"" 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

791 
then name ^ (paren_pack (terms_as_strings @ [typ])) 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

792 
else name ^ (paren_pack terms_as_strings) 
16903  793 
end; 
15347  794 

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

795 

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

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

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

798 
 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

799 

17234  800 
fun dfg_pred (Literal(pol,pred,tag)) ax_name = 
801 
(string_of_predname pred) ^ " " ^ ax_name 

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

802 

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

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

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

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

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

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

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

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

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

812 
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

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

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

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

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

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

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

820 

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

821 
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

822 

17234  823 
fun string_of_preds preds = 
824 
"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

825 

17234  826 
fun string_of_funcs funcs = 
827 
"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

828 

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

829 

17234  830 
fun string_of_symbols predstr funcstr = 
831 
"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

832 

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

833 

17234  834 
fun string_of_axioms axstr = 
835 
"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

836 

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

837 

17234  838 
fun string_of_conjectures conjstr = 
839 
"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

840 

17234  841 
fun string_of_descrip () = 
842 
"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

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

846 

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

847 

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

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

849 

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

850 

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

851 
fun clause2dfg cls = 
17234  852 
let val (lits,tfree_lits) = dfg_clause_aux cls 
853 
(*"lits" includes the typing assumptions (TVars)*) 

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

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

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

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

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

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

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

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

862 
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

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

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

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

866 

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

867 

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

868 

17234  869 
fun tfree_dfg_clause tfree_lit = 
17422  870 
"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

871 

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

872 

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

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

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

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

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

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

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

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

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

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

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

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

889 

17422  890 
fun clauses2dfg [] probname axioms conjectures funcs preds = 
17775  891 
let val funcs' = (union_all(map funcs_of_cls axioms)) @ funcs 
892 
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

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

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

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

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

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

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

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

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

903 
val funcs' = distinct((funcs_of_cls cls)@funcs) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

904 
val preds' = distinct((preds_of_cls cls)@preds) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

907 
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

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

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

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

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

913 

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

914 

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

915 
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

916 
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

917 

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

918 
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

919 

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

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

921 
fun dfg_of_arLit (TConsLit(b,(c,t,args))) = 
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 
val arg_strs = (case args of [] => ""  _ => paren_pack args) 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

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

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

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

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

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

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

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

931 
end; 
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 
fun dfg_of_conclLit (ArityClause arcls) = dfg_of_arLit (#conclLit arcls); 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

935 

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

936 

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

937 
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

938 

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

939 

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

940 

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

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

942 

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

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

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

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

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

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

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

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

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

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

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

953 

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

954 

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

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

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

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

958 

15347  959 
fun tptp_literal (Literal(pol,pred,tag)) = 
960 
let val pred_string = string_of_predicate pred 

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

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

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

963 
else (if pol then "++" else "") 
15347  964 
in 
965 
tagged_pol ^ pred_string 

966 
end; 

967 

968 

969 

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

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

972 

973 

974 
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

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

976 
knd ^ "," ^ lits ^ ")."; 
15347  977 

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

978 
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

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

980 
knd ^ ",[" ^ tfree_lit ^ "])."; 
15347  981 

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

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

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

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

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

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

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

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

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

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

996 
fun tptp_clause cls = 

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

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

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

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

1002 
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

1003 
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

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

1006 
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

1007 
typ_clss (k+1) tfrees 
15347  1008 
in 
1009 
cls_str :: (typ_clss 0 tfree_lits) 

1010 
end; 

1011 

15608  1012 
fun clause2tptp cls = 
17422  1013 
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

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

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

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

1018 
val lits_str = bracket_pack lits 
15608  1019 
val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) 
1020 
in 

1021 
(cls_str,tfree_lits) 

1022 
end; 

1023 

1024 

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

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

1026 
"input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "])."; 
15608  1027 

15347  1028 

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

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

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

1031 
val arg_strs = (case args of [] => ""  _ => paren_pack args) 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

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

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

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

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

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

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

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

1039 
end; 
15347  1040 

1041 

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

1042 
fun tptp_of_conclLit (ArityClause arcls) = tptp_of_arLit (#conclLit arcls); 
15347  1043 

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

1044 
fun tptp_of_premLits (ArityClause arcls) = map tptp_of_arLit (#premLits arcls); 
15347  1045 

1046 
fun tptp_arity_clause arcls = 

1047 
let val arcls_id = string_of_arClauseID arcls 

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

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

1049 
val prems_lits = tptp_of_premLits arcls 
15347  1050 
val knd = string_of_arKind arcls 
1051 
val all_lits = concl_lit :: prems_lits 

1052 
in 

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

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

1054 
(bracket_pack all_lits) ^ ")." 
15347  1055 
end; 
1056 

1057 
fun tptp_classrelLits sub sup = 

1058 
let val tvar = "(T)" 

1059 
in 

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

15347  1062 
end; 
1063 

1064 

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

1065 
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

1066 
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

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

1068 
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

1069 
(Option.map make_type_class superclass) 
15347  1070 
in 
1071 
"input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ")." 

1072 
end; 

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

1073 

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

1074 

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

1075 

15347  1076 
end; 