author  paulson 
Fri, 02 Sep 2005 17:55:24 +0200  
changeset 17234  12a9393c5d77 
parent 17230  77e93bf303a5 
child 17261  193b84a70ca4 
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 

13 
exception ARCLAUSE of string 

14 
exception CLAUSE of string 

15 
type arityClause 

16 
type classrelClause 

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

17 
val classrelClauses_of : string * string list > classrelClause list 
15347  18 
type clause 
16925
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset

19 
val init : theory > unit 
15347  20 
val keep_types : bool ref 
21 
val make_axiom_arity_clause : 

22 
string * (string * string list list) > arityClause 

23 
val make_axiom_classrelClause : 

15531  24 
string * string option > classrelClause 
15347  25 
val make_axiom_clause : Term.term > string * int > clause 
26 
val make_conjecture_clause : Term.term > clause 

27 
val make_conjecture_clause_thm : Thm.thm > clause 

28 
val make_hypothesis_clause : Term.term > clause 

29 
val special_equal : bool ref 

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

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

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

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

33 

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

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

35 
val clause2dfg : clause > string * string list 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

36 
val clauses2dfg : clause list > string > clause list > clause list > 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

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

39 

15347  40 
val tptp_arity_clause : arityClause > string 
41 
val tptp_classrelClause : classrelClause > string 

42 
val tptp_clause : clause > string list 

43 
val tptp_clauses2str : string list > string 

15608  44 
val clause2tptp : clause > string * string list 
45 
val tfree_clause : string > string 

16953  46 
val schematic_var_prefix : string 
47 
val fixed_var_prefix : string 

48 
val tvar_prefix : string 

49 
val tfree_prefix : string 

50 
val clause_prefix : string 

51 
val arclause_prefix : string 

52 
val const_prefix : string 

53 
val tconst_prefix : string 

54 
val class_prefix : string 

15347  55 
end; 
56 

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

57 
structure ResClause: RES_CLAUSE = 
15347  58 
struct 
59 

60 
(* Added for typed equality *) 

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

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

63 

64 

65 
val schematic_var_prefix = "V_"; 

66 
val fixed_var_prefix = "v_"; 

67 

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

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

69 
val tfree_prefix = "t_"; 
15347  70 

71 
val clause_prefix = "cls_"; 

72 

73 
val arclause_prefix = "arcls_" 

74 

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

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

76 
val tconst_prefix = "tc_"; 
15347  77 

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

78 
val class_prefix = "class_"; 
15347  79 

80 

81 
(**** some useful functions ****) 

82 

83 
val const_trans_table = 

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

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

86 
("op <", "less"), 

87 
("op &", "and"), 

88 
("op ", "or"), 

89 
("op >", "implies"), 

90 
("op :", "in"), 

91 
("op Un", "union"), 

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

93 

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

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

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

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

97 
("~=>", "t_map")]; 
15347  98 

15610  99 
(*Escaping of special characters. 
100 
Alphanumeric characters are left unchanged. 

101 
The character _ goes to __ 

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

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

104 
local 

105 

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

107 

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

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

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

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

114 
else "" 

15347  115 

15610  116 
in 
117 

118 
val ascii_of = String.translate ascii_of_c; 

119 

120 
end; 

15347  121 

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

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

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

124 
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

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

126 

16903  127 
fun ascii_of_indexname (v,0) = ascii_of v 
128 
 ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ string_of_int i; 

15347  129 

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

130 
fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v); 
15347  131 
fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x); 
132 

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

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

135 
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

136 
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); 
15347  137 

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

138 
fun make_fixed_const c = 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

139 
case Symtab.lookup (const_trans_table,c) of 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

140 
SOME c' => c' 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

141 
 NONE => const_prefix ^ (ascii_of c); 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

142 

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

143 
fun make_fixed_type_const c = 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

144 
case Symtab.lookup (type_const_trans_table,c) of 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

145 
SOME c' => c' 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

147 

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

148 
fun make_type_class clas = class_prefix ^ (ascii_of clas); 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

149 

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

150 

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

151 

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

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

154 
val keep_types = ref true; 
15347  155 
fun untyped () = (keep_types := false); 
156 
fun typed () = (keep_types := true); 

157 

158 

159 
datatype kind = Axiom  Hypothesis  Conjecture; 

160 
fun name_of_kind Axiom = "axiom" 

161 
 name_of_kind Hypothesis = "hypothesis" 

162 
 name_of_kind Conjecture = "conjecture"; 

163 

164 
type clause_id = int; 

165 
type axiom_name = string; 

166 

167 

168 
type polarity = bool; 

169 

170 
type indexname = Term.indexname; 

171 

172 

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

174 
type tag = bool; 

175 

176 

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

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

178 

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

180 
let val id = !id_ref 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

181 
in id_ref := id + 1; id end; 
15347  182 

183 

184 

185 
(**** Isabelle FOL clauses ****) 

186 

187 
(* by default it is false *) 

188 
val tagged = ref false; 

189 

190 
type pred_name = string; 

191 
type sort = Term.sort; 

192 
type fol_type = string; 

193 

194 

195 
datatype type_literal = LTVar of string  LTFree of string; 

196 

197 

198 
datatype folTerm = UVar of string * fol_type Fun of string * fol_type * folTerm list; 

199 
datatype predicate = Predicate of pred_name * fol_type * folTerm list; 

200 

201 

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

203 

204 

205 
datatype typ_var = FOLTVar of indexname  FOLTFree of string; 

206 

207 

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

209 
datatype clause = 

210 
Clause of {clause_id: clause_id, 

211 
axiom_name: axiom_name, 

212 
kind: kind, 

213 
literals: literal list, 

214 
types_sorts: (typ_var * sort) list, 

215 
tvar_type_literals: type_literal list, 

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

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

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

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

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

220 

15347  221 

222 

223 
exception CLAUSE of string; 

224 

225 

226 

227 
(*** make clauses ***) 

228 

17234  229 
fun make_clause (clause_id,axiom_name,kind,literals, 
230 
types_sorts,tvar_type_literals, 

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

231 
tfree_type_literals,tvars, predicates, functions) = 
17234  232 
if null literals 
233 
then error "Problem too trivial for resolution (empty clause)" 

234 
else 

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

235 
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

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

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

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

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

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

241 

15347  242 

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

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

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

245 

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

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

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

248 
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

249 

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

251 

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

252 

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

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

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

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

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

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

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

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

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

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

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

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

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

266 
((t ^ (ResLib.list_to_string folTyps)),(ts', (t, length Ts)::funcs') ) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

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

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

271 
 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

272 

15390  273 

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

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

275 
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

276 

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

279 
val isMeta = String.isPrefix "METAHYP1_" 

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

280 

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

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

282 
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

283 
in (make_fixed_const c, (typof,folTyps), funcs) end 
15390  284 
 pred_name_type (Free(x,T)) = 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

286 
else (make_fixed_var x, ("",[]), []) 
15347  287 
 pred_name_type (Var(_,_)) = raise CLAUSE("Predicate Not First Order") 
288 
 pred_name_type _ = raise CLAUSE("Predicate input unexpected"); 

289 

15615  290 

291 
(* For type equality *) 

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

293 
(* Find type of equality arg *) 

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

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

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

296 
in folT end; 
15347  297 

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

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

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

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

301 
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

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

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

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

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

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

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

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

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

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

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

312 
 fun_name_type _ args = raise CLAUSE("Function Not First Order"); 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

313 

15615  314 

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

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

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

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

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

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

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

323 
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

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

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

326 
(Fun(make_fixed_var x,folType,[]), (ts, ((make_fixed_var x),0)::funcs)) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

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

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

331 
(Fun(make_fixed_const c,folType,[]),(ts, ((make_fixed_const c),0)::funcs)) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

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

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

336 
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

337 
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

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

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

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

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

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

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

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

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

346 
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

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

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

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

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

351 
(ResLib.flat_noDup ts, 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

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

355 
case f of Const ("op =", typ) => term_of_eq (f,args) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

357 
 Free(s,_) => if isMeta s 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

358 
then raise CLAUSE("Function Not First Order") 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

361 
end 
15390  362 
 term_of _ = raise CLAUSE("Function Not First Order"); 
363 

15347  364 

365 
fun pred_of_eq ((Const ("op =", typ)),args) = 

366 
let val arg_typ = eq_arg_type typ 

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

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

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

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

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

372 
ResLib.flat_noDup ts, 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

373 
[((make_fixed_var equal_name), 2)], 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

374 
(ResLib.flat_noDup funcs)) 
15347  375 
end; 
376 

377 
(* The input "pred" cannot be an equality *) 

378 
fun pred_of_nonEq (pred,args) = 

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

379 
let val (predName,(predType,ts1), pfuncs) = pred_name_type pred 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

381 
val (ts2,ffuncs) = ListPair.unzip ts_funcs 
15347  382 
val ts3 = ResLib.flat_noDup (ts1::ts2) 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

383 
val ffuncs' = (ResLib.flat_noDup ffuncs) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

384 
val newfuncs = distinct (pfuncs@ffuncs') 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

387 
Const (c,_) => 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

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

391 
 _ => length args 
15347  392 
in 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

393 
(Predicate(predName,predType,args'), ts3, 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

394 
[(predName, arity)], newfuncs) 
15347  395 
end; 
396 

397 

398 
(* Changed for typed equality *) 

399 
(* First check if the predicate is an equality or not, then call different functions for equality and nonequalities *) 

400 
fun predicate_of term = 

401 
let val (pred,args) = strip_comb term 

402 
in 

403 
case pred of (Const ("op =", _)) => pred_of_eq (pred,args) 

404 
 _ => pred_of_nonEq (pred,args) 

405 
end; 

406 

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

409 
 literals_of_term ((Const("op ",_) $ P $ Q),(lits,ts), preds,funcs) = 
17234  410 
let val (lits',ts', preds', funcs') = 
411 
literals_of_term(P,(lits,ts), preds,funcs) 

412 
in 

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

414 
distinct(funcs'@funcs)) 

415 
end 

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

416 
 literals_of_term ((Const("Not",_) $ P),(lits,ts), preds, funcs) = 
17234  417 
let val (pred,ts', preds', funcs') = predicate_of P 
418 
val lits' = Literal(false,pred,false) :: lits 

419 
val ts'' = ResLib.no_rep_app ts ts' 

420 
in 

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

422 
end 

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

423 
 literals_of_term (P,(lits,ts), preds, funcs) = 
17234  424 
let val (pred,ts', preds', funcs') = predicate_of P 
425 
val lits' = Literal(true,pred,false) :: lits 

426 
val ts'' = ResLib.no_rep_app ts ts' 

427 
in 

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

429 
end; 

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

430 

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

431 

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

432 
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

433 

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

434 

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

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

436 

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

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

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

439 
 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

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

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

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

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

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

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

446 
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

447 
(sorts_on_typs ((FOLTFree x), ss)); 
15347  448 

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

449 

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

450 
(*FIXME: duplicate code that needs removal??*) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

451 

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

452 
fun takeUntil ch [] res = (res, []) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

453 
 takeUntil ch (x::xs) res = if x = ch 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

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

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

457 
takeUntil ch xs (res@[x]) 
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 
fun remove_type str = let val exp = explode str 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

460 
val (first,rest) = (takeUntil "(" exp []) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

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

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

464 

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

465 
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

466 
 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

467 

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

468 

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

469 

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

470 

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

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

472 
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

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

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

475 
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

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

477 
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

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

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

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

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

482 
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

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

484 
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

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

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

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

488 

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

489 

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

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

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

492 
let val vs = sorts_on_typs (FOLTVar indx, s) 
16199
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset

493 
val (vss,fss) = add_typs_aux tss 
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset

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

495 
(ResLib.no_rep_app vs vss, fss) 
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset

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

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

498 
let val fs = sorts_on_typs (FOLTFree x, s) 
16199
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset

499 
val (vss,fss) = add_typs_aux tss 
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset

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

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

502 
end;*) 
15347  503 

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

504 

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

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

507 

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

509 

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

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

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

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

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

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

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

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

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

518 

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

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

520 

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

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

522 
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

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

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

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

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

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

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

531 

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

532 

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

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

534 
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

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

536 
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

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

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

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

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

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

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

543 

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

544 

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

545 
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

546 
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

547 
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

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

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

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

552 
tvars, preds,funcs) 
15347  553 
end; 
554 

555 

556 
fun make_hypothesis_clause term = 

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

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

559 
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

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

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

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

564 
tvars, preds, funcs) 
15347  565 
end; 
566 

567 
fun make_conjecture_clause term = 

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

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

570 
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

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

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

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

575 
tvars, preds, funcs) 
15347  576 
end; 
577 

578 

579 

580 
(**** Isabelle arities ****) 

581 

582 
exception ARCLAUSE of string; 

583 

584 

585 
type class = string; 

586 
type tcons = string; 

587 

588 

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

590 

591 
datatype arityClause = 

592 
ArityClause of {clause_id: clause_id, 

593 
kind: kind, 

594 
conclLit: arLit, 

595 
premLits: arLit list}; 

596 

597 

598 
fun get_TVars 0 = [] 

599 
 get_TVars n = ("T_" ^ (string_of_int n)) :: get_TVars (n1); 

600 

601 

602 

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

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

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

606 

607 

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

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

610 

611 

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

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

614 

615 

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

617 
let val cls_id = generate_id() 

618 
val nargs = length args 

619 
val tvars = get_TVars nargs 

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

15774  621 
val tvars_srts = ListPair.zip (tvars,args) 
15347  622 
val tvars_srts' = ResLib.flat_noDup(map pack_sort tvars_srts) 
623 
val false_tvars_srts' = ResLib.pair_ins false tvars_srts' 

624 
val premLits = map make_TVarLit false_tvars_srts' 

625 
in 

626 
make_arity_clause (cls_id,Axiom,conclLit,premLits) 

627 
end; 

628 

629 

630 

631 
(**** Isabelle class relations ****) 

632 

633 

634 
datatype classrelClause = 

635 
ClassrelClause of {clause_id: clause_id, 

636 
subclass: class, 

15531  637 
superclass: class option}; 
15347  638 

639 
fun make_classrelClause (clause_id,subclass,superclass) = 

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

641 

642 

643 
fun make_axiom_classrelClause (subclass,superclass) = 

644 
let val cls_id = generate_id() 

645 
val sub = make_type_class subclass 

15531  646 
val sup = case superclass of NONE => NONE 
647 
 SOME s => SOME (make_type_class s) 

15347  648 
in 
649 
make_classrelClause(cls_id,sub,sup) 

650 
end; 

651 

652 

653 

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

15531  655 
 classrelClauses_of_aux (sub,(sup::sups)) = make_axiom_classrelClause(sub,SOME sup) :: (classrelClauses_of_aux (sub,sups)); 
15347  656 

657 

658 
fun classrelClauses_of (sub,sups) = 

15531  659 
case sups of [] => [make_axiom_classrelClause (sub,NONE)] 
15347  660 
 _ => classrelClauses_of_aux (sub, sups); 
661 

662 

663 

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

664 
(***** convert clauses to DFG format *****) 
15347  665 

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

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

667 
clause_prefix ^ string_of_int (#clause_id cls); 
15347  668 

669 
fun string_of_kind (Clause cls) = name_of_kind (#kind cls); 

670 

671 
fun string_of_axiomName (Clause cls) = #axiom_name cls; 

672 

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

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

674 

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

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

678 
fun string_of_equality (typ,terms) = 

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

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

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

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

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

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

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

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

686 
and string_of_term (UVar(x,_)) = x 
15615  687 
 string_of_term (Fun("equal",typ,terms)) = string_of_equality(typ,terms) 
688 
 string_of_term (Fun (name,typ,[])) = name 

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

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

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

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

692 
if !keep_types andalso typ<>"" 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

693 
then name ^ (ResLib.list_to_string (terms' @ [typ])) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

694 
else name ^ (ResLib.list_to_string terms') 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

695 
end; 
15347  696 

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

17234  698 
fun string_of_predicate (Predicate("equal",typ,terms)) = 
699 
string_of_equality(typ,terms) 

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

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

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

702 
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

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

704 
if !keep_types andalso typ<>"" 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

705 
then name ^ (ResLib.list_to_string (terms_as_strings @ [typ])) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

706 
else name ^ (ResLib.list_to_string terms_as_strings) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

707 
end; 
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 
(********************************) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

712 
(* Code for producing DFG files *) 
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 

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

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

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

719 
end; 
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 

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

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

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

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

725 

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

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

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

728 

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

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

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

731 
 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

732 

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

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

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

735 

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

736 
fun gen_dfg_cls (cls_id,ax_name,knd,lits,tvars,vars) = 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

737 
let val ax_str = 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

738 
if ax_name = "" then cls_id 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

739 
else cls_id ^ "_" ^ ascii_of ax_name 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

741 
"clause( %(" ^ knd ^ ")\n" ^ forall_open(vars,tvars) ^ 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

742 
"or(" ^ lits ^ ")" ^ forall_close(vars,tvars) ^ ",\n" ^ 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

745 

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

746 
fun gen_dfg_type_cls (cls_id,knd,tfree_lit,idx,tvars,vars) = 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

747 
let val ax_str = cls_id ^ "_tcs" ^ (string_of_int idx) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

749 
"clause( %(" ^ knd ^ ")\n" ^ forall_open(vars,tvars) ^ 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

750 
"or( " ^ tfree_lit ^ ")" ^ forall_close(vars,tvars) ^ ",\n" ^ 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

753 

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

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

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

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

757 
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

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

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

760 
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

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

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

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

765 

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

766 

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

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

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

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

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

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

772 

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

773 

17234  774 
fun get_uvars (UVar(str,typ)) = [str] 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

776 

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 is_uvar (UVar(str,typ)) = true 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

779 
 is_uvar (Fun (str,typ,tlist)) = false; 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

780 

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

781 
fun uvar_name (UVar(str,typ)) = str 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

782 
 uvar_name _ = (raise CLAUSE("Not a variable")); 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

783 

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

784 

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

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

786 
 mergelist (x::xs ) = x@(mergelist xs) 
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 
fun dfg_vars (Clause cls) = 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

790 
let val lits = (#literals cls) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

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

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

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

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

796 

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

797 

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

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

799 

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

800 

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

801 

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

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

803 
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

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

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

806 

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

807 

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

808 
(* make this return funcs and preds too? *) 
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 string_of_predicate (Predicate("equal",typ,terms)) = string_of_equality(typ,terms) 
15347  811 
 string_of_predicate (Predicate(name,_,[])) = name 
812 
 string_of_predicate (Predicate(name,typ,terms)) = 

16903  813 
let val terms_as_strings = map string_of_term terms 
814 
in 

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

815 
if !keep_types andalso typ<>"" 
16903  816 
then name ^ (ResLib.list_to_string (terms_as_strings @ [typ])) 
817 
else name ^ (ResLib.list_to_string terms_as_strings) 

818 
end; 

15347  819 

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

820 

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

821 

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

822 

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

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

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

825 
 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

826 

17234  827 
fun dfg_pred (Literal(pol,pred,tag)) ax_name = 
828 
(string_of_predname pred) ^ " " ^ ax_name 

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

829 

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

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

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

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

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

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

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

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

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

839 
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

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

841 
 typ_clss k (tfree :: tfrees) = 
17234  842 
(gen_dfg_type_cls(cls_id,knd,tfree,k, tvars,vars)) :: 
843 
(typ_clss (k+1) tfrees) 

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

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

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

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

847 

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

848 
fun clause_info cls = (string_of_axiomName cls, string_of_clauseID cls); 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

849 

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

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

851 

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

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

853 

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

854 
fun string_of_arity (name, num) = name ^"," ^ (string_of_int num) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

855 

17234  856 
fun string_of_preds preds = 
857 
"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

858 

17234  859 
fun string_of_funcs funcs = 
860 
"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

861 

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

862 

17234  863 
fun string_of_symbols predstr funcstr = 
864 
"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

865 

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

866 

17234  867 
fun string_of_axioms axstr = 
868 
"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

869 

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

870 

17234  871 
fun string_of_conjectures conjstr = 
872 
"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

873 

17234  874 
fun string_of_descrip () = 
875 
"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

876 

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

877 

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

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

879 

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

880 

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

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

882 

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

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

884 
val dfg_clauses2str = ResLib.list2str_sep delim; 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

885 

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

886 

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

887 
fun clause2dfg cls = 
17234  888 
let val (lits,tfree_lits) = dfg_clause_aux cls 
889 
(*"lits" includes the typing assumptions (TVars)*) 

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

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

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

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

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

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

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

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

898 
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

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

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

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

902 

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

903 

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

904 

17234  905 
fun tfree_dfg_clause tfree_lit = 
906 
"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

907 

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

908 

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

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

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

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

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

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

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

915 
val tfree_clss = map tfree_dfg_clause ((ResLib.flat_noDup atfrees) \\ tfrees) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

916 
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

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

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

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

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

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

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

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

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

925 

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

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

927 
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

928 
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

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

930 
gen_dfg_file probname axioms conjectures funcs' preds' tfrees 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

931 
(*(probname, axioms, conjectures, funcs, preds)*) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

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

935 
(*"lits" includes the typing assumptions (TVars)*) 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

936 
val cls_id = string_of_clauseID cls 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

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

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

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

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

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

944 
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

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

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

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

948 
clauses2dfg clss probname axioms' conjectures' funcs' preds' tfrees 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

950 

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

951 

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

952 
fun fileout f str = let val out = TextIO.openOut f 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

954 
ResLib.writeln_strs out str; TextIO.closeOut out 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

956 

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

957 
(*val filestr = clauses2dfg newcls "flump" [] [] [] []; 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

959 
(* fileout "flump.dfg" [filestr];*) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

960 

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

961 

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

962 
(*FIX: ask Jia what this is for *) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

963 

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

964 

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

965 
fun string_of_arClauseID (ArityClause arcls) = arclause_prefix ^ string_of_int(#clause_id arcls); 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

966 

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

967 

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

968 
fun string_of_arLit (TConsLit(b,(c,t,args))) = 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

969 
let val pol = if b then "++" else "" 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

970 
val arg_strs = (case args of [] => ""  _ => ResLib.list_to_string args) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

972 
pol ^ c ^ "(" ^ t ^ arg_strs ^ ")" 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

974 
 string_of_arLit (TVarLit(b,(c,str))) = 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

975 
let val pol = if b then "++" else "" 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

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

978 
end; 
15347  979 

980 

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

981 
fun string_of_conclLit (ArityClause arcls) = string_of_arLit (#conclLit arcls); 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

982 

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

983 

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

984 
fun strings_of_premLits (ArityClause arcls) = map string_of_arLit (#premLits arcls); 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

985 

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

986 

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

987 
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

988 

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

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

990 

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

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

992 
let val arcls_id = string_of_arClauseID arcls 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

993 
val concl_lit = string_of_conclLit arcls 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

994 
val prems_lits = strings_of_premLits arcls 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

995 
val knd = string_of_arKind arcls 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

996 
val all_lits = concl_lit :: prems_lits 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

998 

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

999 
"clause( %(" ^ knd ^ ")\n" ^ "or( " ^ (ResLib.list_to_string' all_lits) ^ ")),\n" ^ 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

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

1002 

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

1003 

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

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

1005 

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

1006 
(* FIX later. Doesn't seem to be used in clasimp *) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1007 

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

1008 
(*fun tptp_classrelLits sub sup = 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1009 
let val tvar = "(T)" 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

1011 
case sup of NONE => "[++" ^ sub ^ tvar ^ "]" 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1012 
 (SOME supcls) => "[" ^ sub ^ tvar ^ ",++" ^ supcls ^ tvar ^ "]" 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

1014 

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

1015 

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

1016 
fun tptp_classrelClause (ClassrelClause cls) = 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1017 
let val relcls_id = clrelclause_prefix ^ string_of_int(#clause_id cls) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1018 
val sub = #subclass cls 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1019 
val sup = #superclass cls 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

1020 
val lits = tptp_classrelLits sub sup 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

1022 
"input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ")." 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

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

1025 

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

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

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

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

1029 

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

1030 

15347  1031 

1032 
fun tptp_literal (Literal(pol,pred,tag)) = 

1033 
let val pred_string = string_of_predicate pred 

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

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

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

1036 
else (if pol then "++" else "") 
15347  1037 
in 
1038 
tagged_pol ^ pred_string 

1039 
end; 

1040 

1041 

1042 

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

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

1045 

1046 

1047 
fun gen_tptp_cls (cls_id,ax_name,knd,lits) = 

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

1048 
let val ax_str = (if ax_name = "" then "" else ("_" ^ ascii_of ax_name)) 
15347  1049 
in 
1050 
"input_clause(" ^ cls_id ^ ax_str ^ "," ^ knd ^ "," ^ lits ^ ")." 

1051 
end; 

1052 

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

1053 
fun gen_tptp_type_cls (cls_id,knd,tfree_lit,idx) = 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1054 
"input_clause(" ^ cls_id ^ "_tcs" ^ (string_of_int idx) ^ "," ^ 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1055 
knd ^ ",[" ^ tfree_lit ^ "])."; 
15347  1056 

1057 

1058 
fun tptp_clause_aux (Clause cls) = 

1059 
let val lits = map tptp_literal (#literals cls) 

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

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

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

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

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

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

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

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

1067 
else [] 
15347  1068 
in 
1069 
(tvar_lits_strs @ lits,tfree_lits) 

1070 
end; 

1071 

15608  1072 

15347  1073 
fun tptp_clause cls = 
1074 
let val (lits,tfree_lits) = tptp_clause_aux cls (*"lits" includes the typing assumptions (TVars)*) 

1075 
val cls_id = string_of_clauseID cls 

1076 
val ax_name = string_of_axiomName cls 

1077 
val knd = string_of_kind cls 

1078 
val lits_str = ResLib.list_to_string' lits 

1079 
val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) fun typ_clss k [] = [] 

1080 
 typ_clss k (tfree :: tfrees) = 

1081 
(gen_tptp_type_cls(cls_id,knd,tfree,k)) :: (typ_clss (k+1) tfrees) 

1082 
in 

1083 
cls_str :: (typ_clss 0 tfree_lits) 

1084 
end; 

1085 

1086 

15608  1087 
fun clause2tptp cls = 
1088 
let val (lits,tfree_lits) = tptp_clause_aux cls (*"lits" includes the typing assumptions (TVars)*) 

1089 
val cls_id = string_of_clauseID cls 

1090 
val ax_name = string_of_axiomName cls 

1091 
val knd = string_of_kind cls 

1092 
val lits_str = ResLib.list_to_string' lits 

1093 
val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) 

1094 
in 

1095 
(cls_str,tfree_lits) 

1096 
end; 

1097 

1098 

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

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

1100 
"input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "])."; 
15608  1101 

15347  1102 
val delim = "\n"; 
1103 
val tptp_clauses2str = ResLib.list2str_sep delim; 

1104 

1105 

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

1106 
fun string_of_arClauseID (ArityClause arcls) = 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

1107 
arclause_prefix ^ string_of_int(#clause_id arcls); 
15347  1108 

1109 

1110 
fun string_of_arLit (TConsLit(b,(c,t,args))) = 

1111 
let val pol = if b then "++" else "" 

1112 
val arg_strs = (case args of [] => ""  _ => ResLib.list_to_string args) 

1113 
in 

1114 
pol ^ c ^ "(" ^ t ^ arg_strs ^ ")" 

1115 
end 

1116 
 string_of_arLit (TVarLit(b,(c,str))) = 

1117 
let val pol = if b then "++" else "" 

1118 
in 

1119 
pol ^ c ^ "(" ^ str ^ ")" 

1120 
end; 

1121 

1122 

1123 
fun string_of_conclLit (ArityClause arcls) = string_of_arLit (#conclLit arcls); 

1124 

17234  1125 
fun strings_of_premLits (ArityClause arcls) = 
1126 
map string_of_arLit (#premLits arcls); 

15347  1127 

1128 

1129 
fun string_of_arKind (ArityClause arcls) = name_of_kind(#kind arcls); 

1130 

1131 
fun tptp_arity_clause arcls = 

1132 
let val arcls_id = string_of_arClauseID arcls 

1133 
val concl_lit = string_of_conclLit arcls 

1134 
val prems_lits = strings_of_premLits arcls 

1135 
val knd = string_of_arKind arcls 

1136 
val all_lits = concl_lit :: prems_lits 

1137 
in 

15452  1138 
"input_clause(" ^ arcls_id ^ "," ^ knd ^ "," ^ (ResLib.list_to_string' all_lits) ^ ")." 
15347  1139 
end; 
1140 

1141 

1142 
val clrelclause_prefix = "relcls_"; 

1143 

1144 
fun tptp_classrelLits sub sup = 

1145 
let val tvar = "(T)" 

1146 
in 

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

15347  1149 
end; 
1150 

1151 

1152 
fun tptp_classrelClause (ClassrelClause cls) = 

1153 
let val relcls_id = clrelclause_prefix ^ string_of_int(#clause_id cls) 

1154 
val sub = #subclass cls 

1155 
val sup = #superclass cls 

1156 
val lits = tptp_classrelLits sub sup 

1157 
in 

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

1159 
end; 

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

1160 

15347  1161 
end; 