author  paulson 
Tue, 20 Sep 2005 18:43:39 +0200  
changeset 17525  ae5bb6001afb 
parent 17422  3b237822985d 
child 17745  38b4d8bf2627 
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 
val classrelClauses_of : string * string list > classrelClause list 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

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

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

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

25 
string * (string * string list list) > arityClause 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

26 
val make_axiom_classrelClause : string * string option > classrelClause 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

27 
val make_axiom_clause : Term.term > string * int > clause 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

28 
val make_conjecture_clause : Term.term > clause 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

29 
val make_conjecture_clause_thm : Thm.thm > clause 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

30 
val make_hypothesis_clause : Term.term > clause 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

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

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

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

34 

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

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

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

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

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

40 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

55 
val class_prefix : string 
15347  56 
end; 
57 

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

58 
structure ResClause: RES_CLAUSE = 
15347  59 
struct 
60 

61 
(* Added for typed equality *) 

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

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

64 

65 

66 
val schematic_var_prefix = "V_"; 

67 
val fixed_var_prefix = "v_"; 

68 

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

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

70 
val tfree_prefix = "t_"; 
15347  71 

72 
val clause_prefix = "cls_"; 

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

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

74 
val clrelclause_prefix = "clsrel_"; 
15347  75 

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

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

77 
val tconst_prefix = "tc_"; 
15347  78 

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

79 
val class_prefix = "class_"; 
15347  80 

81 

82 
(**** some useful functions ****) 

83 

84 
val const_trans_table = 

85 
Symtab.make [("op =", "equal"), 

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

87 
("op <", "less"), 

88 
("op &", "and"), 

89 
("op ", "or"), 

17375  90 
("op +", "plus"), 
91 
("op ", "minus"), 

92 
("op *", "times"), 

15347  93 
("op >", "implies"), 
17375  94 
("{}", "emptyset"), 
15347  95 
("op :", "in"), 
96 
("op Un", "union"), 

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

98 

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

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

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

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

102 
("~=>", "t_map")]; 
15347  103 

15610  104 
(*Escaping of special characters. 
105 
Alphanumeric characters are left unchanged. 

106 
The character _ goes to __ 

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

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

109 
local 

110 

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

112 

15347  113 
fun ascii_of_c c = 
15610  114 
if Char.isAlphaNum c then String.str c 
115 
else if c = #"_" then "__" 

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

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

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

119 
else "" 

15347  120 

15610  121 
in 
122 

123 
val ascii_of = String.translate ascii_of_c; 

124 

125 
end; 

15347  126 

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

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

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

129 

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

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

131 

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

132 

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

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

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

135 
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

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

137 

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

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

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

141 
fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v); 
15347  142 
fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x); 
143 

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

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

146 
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

147 
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); 
15347  148 

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

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

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

153 

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

154 
fun make_fixed_type_const c = 
17412  155 
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

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

158 

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

160 

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

161 

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

162 

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

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

165 
val keep_types = ref true; 
15347  166 

167 
datatype kind = Axiom  Hypothesis  Conjecture; 

168 
fun name_of_kind Axiom = "axiom" 

169 
 name_of_kind Hypothesis = "hypothesis" 

170 
 name_of_kind Conjecture = "conjecture"; 

171 

172 
type clause_id = int; 

173 
type axiom_name = string; 

174 

175 

176 
type polarity = bool; 

177 

178 
type indexname = Term.indexname; 

179 

180 

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

182 
type tag = bool; 

183 

184 

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

185 
val id_ref = ref 0; 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

186 

15347  187 
fun generate_id () = 
17317
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

188 
let val id = !id_ref 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

189 
in id_ref := id + 1; id end; 
15347  190 

191 

192 

193 
(**** Isabelle FOL clauses ****) 

194 

195 
val tagged = ref false; 

196 

197 
type pred_name = string; 

198 
type sort = Term.sort; 

199 
type fol_type = string; 

200 

201 

202 
datatype type_literal = LTVar of string  LTFree of string; 

203 

204 

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

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

206 
 Fun of string * fol_type * folTerm list; 
15347  207 
datatype predicate = Predicate of pred_name * fol_type * folTerm list; 
208 

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

210 

211 
datatype typ_var = FOLTVar of indexname  FOLTFree of string; 

212 

213 

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

215 
datatype clause = 

216 
Clause of {clause_id: clause_id, 

217 
axiom_name: axiom_name, 

218 
kind: kind, 

219 
literals: literal list, 

220 
types_sorts: (typ_var * sort) list, 

221 
tvar_type_literals: type_literal list, 

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

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

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

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

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

226 

15347  227 

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

228 
exception CLAUSE of string * term; 
15347  229 

230 

231 
(*** make clauses ***) 

232 

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

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

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

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

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

237 

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

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

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

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

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

242 

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

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

244 

17234  245 
fun make_clause (clause_id,axiom_name,kind,literals, 
246 
types_sorts,tvar_type_literals, 

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

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

248 
if forall isFalse literals 
17234  249 
then error "Problem too trivial for resolution (empty clause)" 
250 
else 

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

251 
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

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

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

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

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

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

257 

15347  258 

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

259 
(** Some Clause destructor functions **) 
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 
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

262 

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

263 
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

264 

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

265 
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

266 

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

267 
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

268 

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

269 
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

270 

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

271 

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

272 

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

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

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

275 

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

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

277 
producing any clauses!*) 
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset

278 
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

279 

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

281 

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

282 

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

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

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

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

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

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

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

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

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

292 
val ts' = ResLib.flat_noDup ts 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

293 
val funcs' = ResLib.flat_noDup funcslist 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

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

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

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

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

300 
in (t, ([((FOLTFree a),s)],[(t,0)]) ) end 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

301 
 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

302 

15390  303 

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

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

305 
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

306 

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

309 
val isMeta = String.isPrefix "METAHYP1_" 

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

310 

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

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

312 
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

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

315 
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

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

317 
 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

318 
 pred_name_type t = raise CLAUSE("Predicate input unexpected", t); 
15347  319 

15615  320 

321 
(* For type equality *) 

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

323 
(* Find type of equality arg *) 

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

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

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

326 
in folT end; 
15347  327 

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

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

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

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

331 
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

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

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

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

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

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

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

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

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

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

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

342 
 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

343 

15615  344 

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

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

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

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

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

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

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

353 
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

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

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

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

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

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

359 
 term_of (Const(c,T)) = (* impossible to be equality *) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

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

363 
(ts, ((make_fixed_const c),0)::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 
 term_of (app as (t $ a)) = 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

368 
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

369 
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

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

371 
val ts3 = ResLib.flat_noDup (ts1::ts2) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

372 
val funcs'' = ResLib.flat_noDup((funcs::funcs')) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

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

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

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

378 
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

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

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

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

382 
(Fun(equal_name,arg_typ,args'), 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

383 
(ResLib.flat_noDup ts, 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

384 
(make_fixed_var equal_name, 2):: ResLib.flat_noDup funcs)) 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

387 
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

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

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

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

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

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

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

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

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

15347  397 

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

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

399 
let val arg_typ = eq_arg_type typ 
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 (ts,funcs) = ListPair.unzip ts_funcs 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

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

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

404 
(Predicate(equal_name,arg_typ,args'), 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

405 
ResLib.flat_noDup ts, 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

406 
[((make_fixed_var equal_name), 2)], 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

407 
(ResLib.flat_noDup funcs)) 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

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

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

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

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

412 
val (ts2,ffuncs) = ListPair.unzip ts_funcs 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

413 
val ts3 = ResLib.flat_noDup (ts1::ts2) 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

414 
val ffuncs' = (ResLib.flat_noDup ffuncs) 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

426 
end; 
15347  427 

428 

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

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

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

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

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

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

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

435 
(pred_of (strip_comb term), polarity, tag); 
15347  436 

17234  437 
fun literals_of_term ((Const("Trueprop",_) $ P),lits_ts, preds, funcs) = 
438 
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

439 
 literals_of_term ((Const("op ",_) $ P $ Q),(lits,ts), preds,funcs) = 
17234  440 
let val (lits',ts', preds', funcs') = 
441 
literals_of_term(P,(lits,ts), preds,funcs) 

442 
in 

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

444 
distinct(funcs'@funcs)) 

445 
end 

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

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

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

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

449 
val lits' = Literal(pol,pred,tag) :: lits 
17234  450 
val ts'' = ResLib.no_rep_app ts ts' 
451 
in 

452 
(lits',ts'', distinct(preds'@preds), distinct(funcs'@funcs)) 

453 
end; 

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

454 

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

455 

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

456 
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

457 

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

458 

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

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

460 

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

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

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

463 
 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

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

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

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

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

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

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

470 
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

471 
(sorts_on_typs ((FOLTFree x), ss)); 
15347  472 

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

473 

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

476 
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

477 

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

478 
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

479 
 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

480 

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

481 

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

482 

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

483 

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

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

485 
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

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

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

488 
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

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

490 
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

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

492 
(ResLib.no_rep_app vs vss, fss, preds'') 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

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

495 
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

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

497 
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

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

499 
(vss, ResLib.no_rep_app fs fss,preds'') 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

501 

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

502 
fun add_typs (Clause cls) preds = add_typs_aux (#types_sorts cls) preds 
15347  503 

504 

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

506 

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

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

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

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

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

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

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

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

514 
 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

515 

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

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

517 

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

518 
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

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 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

523 
make_clause(cls_id,ax_name,Axiom, 
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) 
15347  526 
end; 
527 

528 

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

529 

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

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

531 
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

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

533 
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

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

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

536 
make_clause(cls_id,"",Conjecture, 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

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

540 

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

541 

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

542 
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

543 
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

544 
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

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

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

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

549 
tvars, preds,funcs) 
15347  550 
end; 
551 

552 

553 
fun make_hypothesis_clause term = 

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

554 
let val (lits,types_sorts, preds, funcs) = literals_of_term (term,([],[]),[],[]) 
15347  555 
val cls_id = generate_id() 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

556 
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

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

559 
make_clause(cls_id,"",Hypothesis, 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

564 
fun make_conjecture_clause term = 

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

565 
let val (lits,types_sorts, preds, funcs) = literals_of_term (term,([],[]),[],[]) 
15347  566 
val cls_id = generate_id() 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

567 
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

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

570 
make_clause(cls_id,"",Conjecture, 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

572 
tvars, preds, funcs) 
15347  573 
end; 
574 

575 

576 

577 
(**** Isabelle arities ****) 

578 

579 
exception ARCLAUSE of string; 

580 

581 

582 
type class = string; 

583 
type tcons = string; 

584 

585 

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

587 

588 
datatype arityClause = 

589 
ArityClause of {clause_id: clause_id, 

590 
kind: kind, 

591 
conclLit: arLit, 

592 
premLits: arLit list}; 

593 

594 

595 
fun get_TVars 0 = [] 

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

596 
 get_TVars n = ("T_" ^ (Int.toString n)) :: get_TVars (n1); 
15347  597 

598 

599 

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

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

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

603 

604 

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

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

607 

608 

609 
fun make_arity_clause (clause_id,kind,conclLit,premLits) = 

610 
ArityClause {clause_id = clause_id, kind = kind, conclLit = conclLit, premLits = premLits}; 

611 

612 

613 
fun make_axiom_arity_clause (tcons,(res,args)) = 

614 
let val cls_id = generate_id() 

615 
val nargs = length args 

616 
val tvars = get_TVars nargs 

617 
val conclLit = make_TConsLit(true,(res,tcons,tvars)) 

15774  618 
val tvars_srts = ListPair.zip (tvars,args) 
15347  619 
val tvars_srts' = ResLib.flat_noDup(map pack_sort tvars_srts) 
620 
val false_tvars_srts' = ResLib.pair_ins false tvars_srts' 

621 
val premLits = map make_TVarLit false_tvars_srts' 

622 
in 

623 
make_arity_clause (cls_id,Axiom,conclLit,premLits) 

624 
end; 

625 

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

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

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

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

629 
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

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

631 
in 1 + num_tfree_lits end; 
15347  632 

633 

634 
(**** Isabelle class relations ****) 

635 

636 

637 
datatype classrelClause = 

638 
ClassrelClause of {clause_id: clause_id, 

639 
subclass: class, 

15531  640 
superclass: class option}; 
15347  641 

642 
fun make_classrelClause (clause_id,subclass,superclass) = 

643 
ClassrelClause {clause_id = clause_id,subclass = subclass, superclass = superclass}; 

644 

645 

646 
fun make_axiom_classrelClause (subclass,superclass) = 

647 
let val cls_id = generate_id() 

648 
val sub = make_type_class subclass 

15531  649 
val sup = case superclass of NONE => NONE 
650 
 SOME s => SOME (make_type_class s) 

15347  651 
in 
652 
make_classrelClause(cls_id,sub,sup) 

653 
end; 

654 

655 

656 

657 
fun classrelClauses_of_aux (sub,[]) = [] 

15531  658 
 classrelClauses_of_aux (sub,(sup::sups)) = make_axiom_classrelClause(sub,SOME sup) :: (classrelClauses_of_aux (sub,sups)); 
15347  659 

660 

661 
fun classrelClauses_of (sub,sups) = 

15531  662 
case sups of [] => [make_axiom_classrelClause (sub,NONE)] 
15347  663 
 _ => classrelClauses_of_aux (sub, sups); 
664 

665 

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

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

667 

15347  668 
fun wrap_eq_type typ t = eq_typ_wrapper ^"(" ^ t ^ "," ^ typ ^ ")"; 
669 

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

671 
fun string_of_equality (typ,terms) = 

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

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

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

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

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

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

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

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

679 
and string_of_term (UVar(x,_)) = x 
15615  680 
 string_of_term (Fun("equal",typ,terms)) = string_of_equality(typ,terms) 
681 
 string_of_term (Fun (name,typ,[])) = name 

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

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

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

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

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

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

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

688 
end; 
15347  689 

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

17234  691 
fun string_of_predicate (Predicate("equal",typ,terms)) = 
692 
string_of_equality(typ,terms) 

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

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

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

695 
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

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

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

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

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

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

701 

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

702 

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

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

704 
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

705 

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

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

707 
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

708 

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

709 

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

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

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

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

713 

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

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

715 
let val pred_string = string_of_predicate pred 
17234  716 
in 
717 
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

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

719 

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

720 

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

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

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

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

724 

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

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

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

727 

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

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

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

730 
 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

731 

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

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

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

734 

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

735 
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

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

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

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

739 

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

740 
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

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

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

743 
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

744 

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

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

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

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

748 
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

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

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

751 
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

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

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

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

756 

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

757 

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

758 
fun dfg_folterms (Literal(pol,pred,tag)) = 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

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

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

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

765 
fun get_uvars (UVar(a,typ)) = [a] 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

766 
 get_uvars (Fun (_,typ,tlist)) = ResLib.flat_noDup(map get_uvars tlist) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

767 

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

768 

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

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

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

771 

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

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

773 
 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

774 

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

775 
fun mergelist [] = [] 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

776 
 mergelist (x::xs ) = x @ mergelist xs 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

777 

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

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

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

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

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

782 
ResLib.flat_noDup(map get_uvars folterms) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

784 

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

785 

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

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

787 

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

788 

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

789 

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

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

791 
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

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

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

794 

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

797 

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

798 
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

799 
string_of_equality(typ,terms) 
15347  800 
 string_of_predicate (Predicate(name,_,[])) = name 
801 
 string_of_predicate (Predicate(name,typ,terms)) = 

16903  802 
let val terms_as_strings = map string_of_term terms 
803 
in 

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

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

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

806 
else name ^ (paren_pack terms_as_strings) 
16903  807 
end; 
15347  808 

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

809 

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

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

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

812 
 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

813 

17234  814 
fun dfg_pred (Literal(pol,pred,tag)) ax_name = 
815 
(string_of_predname pred) ^ " " ^ ax_name 

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

816 

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

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

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

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

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

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

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

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

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

826 
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

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

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

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

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

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

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

834 

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

835 
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

836 

17234  837 
fun string_of_preds preds = 
838 
"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

839 

17234  840 
fun string_of_funcs funcs = 
841 
"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

842 

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

843 

17234  844 
fun string_of_symbols predstr funcstr = 
845 
"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

846 

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

847 

17234  848 
fun string_of_axioms axstr = 
849 
"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

850 

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

851 

17234  852 
fun string_of_conjectures conjstr = 
853 
"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

854 

17234  855 
fun string_of_descrip () = 
856 
"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

857 

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

858 

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

859 
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

860 

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

861 

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

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

863 

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

864 
val delim = "\n"; 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

865 
val dfg_clauses2str = ResLib.list2str_sep delim; 
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 
fun clause2dfg cls = 
17234  869 
let val (lits,tfree_lits) = dfg_clause_aux cls 
870 
(*"lits" includes the typing assumptions (TVars)*) 

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

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

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

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

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

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

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

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

879 
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

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

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

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

883 

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

884 

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

885 

17234  886 
fun tfree_dfg_clause tfree_lit = 
17422  887 
"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

888 

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

889 

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

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

892 
val (axstrs, atfrees) = ListPair.unzip axstrs_tfrees 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

893 
val axstr = ResLib.list2str_sep delim axstrs 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

895 
val (conjstrs, atfrees) = ListPair.unzip conjstrs_tfrees 
17422  896 
val tfree_clss = map tfree_dfg_clause (ResLib.flat_noDup atfrees) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

897 
val conjstr = ResLib.list2str_sep delim (tfree_clss@conjstrs) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

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

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

901 
(string_of_start probname) ^ (string_of_descrip ()) ^ 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

902 
(string_of_symbols funcstr predstr ) ^ 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

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

906 

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

908 
let val funcs' = (ResLib.flat_noDup(map funcs_of_cls axioms)) @ funcs 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

909 
val preds' = (ResLib.flat_noDup(map preds_of_cls axioms)) @ preds 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

924 
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

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

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

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

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

930 

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

931 

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

932 
fun string_of_arClauseID (ArityClause arcls) = 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

933 
arclause_prefix ^ Int.toString(#clause_id arcls); 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

934 

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

935 
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

936 

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

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

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

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

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

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

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

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

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

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

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

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

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

949 

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

950 

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

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

952 

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

953 

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

954 
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

955 

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

956 

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

957 

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

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

959 

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

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

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

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

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

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

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

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

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

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

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

970 

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

971 

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

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

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

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

975 

15347  976 
fun tptp_literal (Literal(pol,pred,tag)) = 
977 
let val pred_string = string_of_predicate pred 

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

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

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

980 
else (if pol then "++" else "") 
15347  981 
in 
982 
tagged_pol ^ pred_string 

983 
end; 

984 

985 

986 

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

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

989 

990 

991 
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

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

993 
knd ^ "," ^ lits ^ ")."; 
15347  994 

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

995 
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

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

997 
knd ^ ",[" ^ tfree_lit ^ "])."; 
15347  998 

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

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

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

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

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

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

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

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

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

1010 
(tvar_lits_strs @ lits, tfree_lits) 
15347  1011 
end; 
1012 

1013 
fun tptp_clause cls = 

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

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

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

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

1019 
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

1020 
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

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

1023 
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

1024 
typ_clss (k+1) tfrees 
15347  1025 
in 
1026 
cls_str :: (typ_clss 0 tfree_lits) 

1027 
end; 

1028 

15608  1029 
fun clause2tptp cls = 
17422  1030 
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

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

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

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

1035 
val lits_str = bracket_pack lits 
15608  1036 
val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) 
1037 
in 

1038 
(cls_str,tfree_lits) 

1039 
end; 

1040 

1041 

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

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

1043 
"input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "])."; 
15608  1044 

15347  1045 
val delim = "\n"; 
1046 
val tptp_clauses2str = ResLib.list2str_sep delim; 

1047 

1048 

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

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

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

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

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

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

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

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

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

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

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

1059 
end; 
15347  1060 

1061 

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

1062 
fun tptp_of_conclLit (ArityClause arcls) = tptp_of_arLit (#conclLit arcls); 
15347  1063 

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

1064 
fun tptp_of_premLits (ArityClause arcls) = map tptp_of_arLit (#premLits arcls); 
15347  1065 

1066 
fun tptp_arity_clause arcls = 

1067 
let val arcls_id = string_of_arClauseID arcls 

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

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

1069 
val prems_lits = tptp_of_premLits arcls 
15347  1070 
val knd = string_of_arKind arcls 
1071 
val all_lits = concl_lit :: prems_lits 

1072 
in 

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

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

1074 
(bracket_pack all_lits) ^ ")." 
15347  1075 
end; 
1076 

1077 
fun tptp_classrelLits sub sup = 

1078 
let val tvar = "(T)" 

1079 
in 

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

15347  1082 
end; 
1083 

1084 

1085 
fun tptp_classrelClause (ClassrelClause cls) = 

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

1086 
let val relcls_id = clrelclause_prefix ^ Int.toString(#clause_id cls) 
15347  1087 
val sub = #subclass cls 
1088 
val sup = #superclass cls 

1089 
val lits = tptp_classrelLits sub sup 

1090 
in 

1091 
"input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ")." 

1092 
end; 

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

1093 

15347  1094 
end; 