author  paulson 
Fri, 02 Sep 2005 15:25:27 +0200  
changeset 17230  77e93bf303a5 
parent 17150  ce2a1aeb42aa 
child 17234  12a9393c5d77 
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 

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

229 
fun make_clause (clause_id,axiom_name,kind,literals,types_sorts,tvar_type_literals, 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

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

231 
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

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

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

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

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

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

237 

15347  238 

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

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

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

241 

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

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

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

244 
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

245 

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

247 

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

248 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

267 
 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

268 

15390  269 

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

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

271 
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

272 

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

275 
val isMeta = String.isPrefix "METAHYP1_" 

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

276 

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

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

278 
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

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

281 
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

282 
else (make_fixed_var x, ("",[]), []) 
15347  283 
 pred_name_type (Var(_,_)) = raise CLAUSE("Predicate Not First Order") 
284 
 pred_name_type _ = raise CLAUSE("Predicate input unexpected"); 

285 

15615  286 

287 
(* For type equality *) 

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

289 
(* Find type of equality arg *) 

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

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

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

292 
in folT end; 
15347  293 

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

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

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

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

297 
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

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

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

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

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

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

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

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

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

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

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

308 
 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

309 

15615  310 

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

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

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

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

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

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

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

319 
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

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

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

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

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

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

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

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

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

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

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

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

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

332 
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

333 
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

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

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

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

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

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

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

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

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

342 
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

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

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

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

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

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

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

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

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

351 
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

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

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

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

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

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

357 
end 
15390  358 
 term_of _ = raise CLAUSE("Function Not First Order"); 
359 

15347  360 

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

362 
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

363 
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

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

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

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

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

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

370 
(ResLib.flat_noDup funcs)) 
15347  371 
end; 
372 

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

374 
fun pred_of_nonEq (pred,args) = 

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

375 
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

376 
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

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

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

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

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

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

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

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

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

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

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

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

390 
[(predName, arity)], newfuncs) 
15347  391 
end; 
392 

393 

394 
(* Changed for typed equality *) 

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

396 
fun predicate_of term = 

397 
let val (pred,args) = strip_comb term 

398 
in 

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

400 
 _ => pred_of_nonEq (pred,args) 

401 
end; 

402 

403 

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

404 

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

405 
fun literals_of_term ((Const("Trueprop",_) $ P),lits_ts, preds, funcs) = literals_of_term(P,lits_ts, preds, funcs) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

406 
 literals_of_term ((Const("op ",_) $ P $ Q),(lits,ts), preds,funcs) = 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

407 
let val (lits',ts', preds', funcs') = literals_of_term(P,(lits,ts), preds,funcs) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

409 
literals_of_term(Q,(lits',ts'), distinct(preds'@preds), distinct(funcs'@funcs)) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

411 
 literals_of_term ((Const("Not",_) $ P),(lits,ts), preds, funcs) = 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

412 
let val (pred,ts', preds', funcs') = predicate_of P 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

413 
val lits' = Literal(false,pred,false) :: lits 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

414 
val ts'' = ResLib.no_rep_app ts ts' 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

416 
(lits',ts'', distinct(preds'@preds), distinct(funcs'@funcs)) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

418 
 literals_of_term (P,(lits,ts), preds, funcs) = 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

419 
let val (pred,ts', preds', funcs') = predicate_of P 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

420 
val lits' = Literal(true,pred,false) :: lits 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

421 
val ts'' = ResLib.no_rep_app ts ts' 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

423 
(lits',ts'', distinct(preds'@preds), distinct(funcs'@funcs)) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

425 

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

426 

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

427 
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

428 

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

429 

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

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

431 

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

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

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

434 
 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

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

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

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

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

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

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

441 
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

442 
(sorts_on_typs ((FOLTFree x), ss)); 
15347  443 

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

444 

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

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

446 

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

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

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

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

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

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

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

453 

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

454 
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

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

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

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

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

459 

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

460 
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

461 
 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

462 

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

463 

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 

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

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

467 
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

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

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

470 
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

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

472 
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

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

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

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

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

477 
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

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

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

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

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

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

483 

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

484 

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

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

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

487 
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

488 
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

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

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

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

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

493 
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

494 
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

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

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

497 
end;*) 
15347  498 

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

499 

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

500 
fun add_typs (Clause cls) preds = add_typs_aux (#types_sorts cls) preds 
15347  501 

502 

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

504 

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

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

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

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

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

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

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

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

512 
 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

513 

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

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

515 

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

516 
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

517 
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

518 
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

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

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

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

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

523 
tvars, preds, funcs) 
15347  524 
end; 
525 

526 

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

527 

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

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

529 
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

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

531 
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

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

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

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

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

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

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

538 

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

539 

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

540 
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

541 
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

542 
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

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

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

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

547 
tvars, preds,funcs) 
15347  548 
end; 
549 

550 

551 
fun make_hypothesis_clause term = 

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

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

554 
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

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

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

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

559 
tvars, preds, funcs) 
15347  560 
end; 
561 

562 
fun make_conjecture_clause term = 

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

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

565 
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

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

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

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

570 
tvars, preds, funcs) 
15347  571 
end; 
572 

573 

574 

575 
(**** Isabelle arities ****) 

576 

577 
exception ARCLAUSE of string; 

578 

579 

580 
type class = string; 

581 
type tcons = string; 

582 

583 

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

585 

586 
datatype arityClause = 

587 
ArityClause of {clause_id: clause_id, 

588 
kind: kind, 

589 
conclLit: arLit, 

590 
premLits: arLit list}; 

591 

592 

593 
fun get_TVars 0 = [] 

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

595 

596 

597 

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

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

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

601 

602 

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

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

605 

606 

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

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

609 

610 

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

612 
let val cls_id = generate_id() 

613 
val nargs = length args 

614 
val tvars = get_TVars nargs 

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

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

619 
val premLits = map make_TVarLit false_tvars_srts' 

620 
in 

621 
make_arity_clause (cls_id,Axiom,conclLit,premLits) 

622 
end; 

623 

624 

625 

626 
(**** Isabelle class relations ****) 

627 

628 

629 
datatype classrelClause = 

630 
ClassrelClause of {clause_id: clause_id, 

631 
subclass: class, 

15531  632 
superclass: class option}; 
15347  633 

634 
fun make_classrelClause (clause_id,subclass,superclass) = 

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

636 

637 

638 
fun make_axiom_classrelClause (subclass,superclass) = 

639 
let val cls_id = generate_id() 

640 
val sub = make_type_class subclass 

15531  641 
val sup = case superclass of NONE => NONE 
642 
 SOME s => SOME (make_type_class s) 

15347  643 
in 
644 
make_classrelClause(cls_id,sub,sup) 

645 
end; 

646 

647 

648 

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

15531  650 
 classrelClauses_of_aux (sub,(sup::sups)) = make_axiom_classrelClause(sub,SOME sup) :: (classrelClauses_of_aux (sub,sups)); 
15347  651 

652 

653 
fun classrelClauses_of (sub,sups) = 

15531  654 
case sups of [] => [make_axiom_classrelClause (sub,NONE)] 
15347  655 
 _ => classrelClauses_of_aux (sub, sups); 
656 

657 

658 

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

659 
(***** convert clauses to DFG format *****) 
15347  660 

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

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

662 
clause_prefix ^ string_of_int (#clause_id cls); 
15347  663 

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

665 

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

667 

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

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

669 

15347  670 
fun wrap_eq_type typ t = eq_typ_wrapper ^"(" ^ t ^ "," ^ typ ^ ")"; 
671 

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

673 
fun string_of_equality (typ,terms) = 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

690 
end; 
15347  691 

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

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

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

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

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

696 
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

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

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

699 
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

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

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

702 

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

703 

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

704 

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

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

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

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

708 

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

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

710 
let val pred_string = string_of_predicate pred 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

711 
val tagged_pol =if pol then pred_string else "not(" ^pred_string ^ ")" 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

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

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

715 

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

716 

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

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

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

719 
 dfg_of_typeLit (LTFree x) = "(" ^ x ^ ")";*) 
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 
fun dfg_of_typeLit (LTVar x) = x 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

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

723 

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

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

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

726 
 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

727 

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

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

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

730 

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

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

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

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

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

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

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

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

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

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

740 

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

741 
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

742 
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

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

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

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

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

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

748 

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

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

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

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

752 
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

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

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

755 
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

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

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

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

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

760 

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

761 

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

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

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

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

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

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

767 

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

768 

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

769 
fun get_uvars (UVar(str,typ)) =(*if (substring (str, 0,2))= "V_" then *)[str] (*else []*) 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

770 
 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

771 

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

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

775 

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

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

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

778 

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

779 

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

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

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

782 

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

783 

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

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

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

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

787 
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

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

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

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

791 

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

792 

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

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

794 

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

795 

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

796 

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

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

798 
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

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

800 
 string_of_predname (Predicate(name,typ,terms)) = name 
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 

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

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

804 

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

805 
fun string_of_predicate (Predicate("equal",typ,terms)) = string_of_equality(typ,terms) 
15347  806 
 string_of_predicate (Predicate(name,_,[])) = name 
807 
 string_of_predicate (Predicate(name,typ,terms)) = 

16903  808 
let val terms_as_strings = map string_of_term terms 
809 
in 

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

810 
if !keep_types andalso typ<>"" 
16903  811 
then name ^ (ResLib.list_to_string (terms_as_strings @ [typ])) 
812 
else name ^ (ResLib.list_to_string terms_as_strings) 

813 
end; 

15347  814 

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

815 

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

816 

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

817 

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

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

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

820 
 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

821 

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

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

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

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

825 

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

826 

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

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

828 

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

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

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

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

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

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

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

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

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

837 
val lits_str = concat_with_comma lits 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

838 
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

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

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

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

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

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

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

845 

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

846 
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

847 

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

848 
fun funcs_of_cls (Clause cls) = #functions cls; 
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 preds_of_cls (Clause cls) = #predicates 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 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

853 

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

854 

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

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

856 

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

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

858 

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

859 

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

860 
fun string_of_symbols predstr funcstr = "list_of_symbols.\n" ^ predstr ^ funcstr ^ "end_of_list.\n\n"; 
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 

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

863 
fun string_of_axioms axstr = "list_of_clauses(axioms,cnf).\n" ^ axstr ^ "end_of_list.\n\n"; 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

864 

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 
fun string_of_conjectures conjstr = "list_of_clauses(conjectures,cnf).\n" ^ conjstr ^ "end_of_list.\n\n"; 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

867 

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

868 
fun string_of_descrip () = "list_of_descriptions.\nname({*[ File : ],[ Names :]*}).\nauthor({*[ Source :]*}).\nstatus(unknown).\ndescription({*[ Refs :]*}).\nend_of_list.\n\n" 
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 

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

871 
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

872 

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

873 

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

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

875 

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

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

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

878 

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

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

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

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

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

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

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

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

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

889 
val lits_str = concat_with_comma lits 
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

890 
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

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

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

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

894 

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

895 

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

896 

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

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

898 

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

899 

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

900 
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

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

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

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

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

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

906 
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

907 
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

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

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

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

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

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

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

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

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

916 

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

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

918 
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

919 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

935 
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

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

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

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

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

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

941 

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

942 

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

943 
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

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

945 
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

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

947 

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

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

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

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

951 

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

952 

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

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

954 

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

955 

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

956 
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

957 

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

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

961 
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

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

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

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

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

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

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

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

969 
end; 
15347  970 

971 

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

972 
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

973 

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

974 

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

975 
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

976 

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

977 

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

978 
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

979 

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

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

981 

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

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

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

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

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

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

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

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

989 

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

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

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

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

993 

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

994 

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

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

996 

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

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

998 

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

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

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

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

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

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

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

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

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

1008 
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

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

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

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

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

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

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

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

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

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

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

1020 

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

1021 

15347  1022 

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

1024 
let val pred_string = string_of_predicate pred 

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

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

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

1027 
else (if pol then "++" else "") 
15347  1028 
in 
1029 
tagged_pol ^ pred_string 

1030 
end; 

1031 

1032 

1033 

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

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

1036 

1037 

1038 
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

1039 
let val ax_str = (if ax_name = "" then "" else ("_" ^ ascii_of ax_name)) 
15347  1040 
in 
1041 
"input_clause(" ^ cls_id ^ ax_str ^ "," ^ knd ^ "," ^ lits ^ ")." 

1042 
end; 

1043 

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

1044 
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

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

1046 
knd ^ ",[" ^ tfree_lit ^ "])."; 
15347  1047 

1048 

1049 
fun tptp_clause_aux (Clause cls) = 

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

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

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

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

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

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

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

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

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

1058 
else [] 
15347  1059 
in 
1060 
(tvar_lits_strs @ lits,tfree_lits) 

1061 
end; 

1062 

15608  1063 

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

1066 
val cls_id = string_of_clauseID cls 

1067 
val ax_name = string_of_axiomName cls 

1068 
val knd = string_of_kind cls 

1069 
val lits_str = ResLib.list_to_string' lits 

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

1071 
 typ_clss k (tfree :: tfrees) = 

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

1073 
in 

1074 
cls_str :: (typ_clss 0 tfree_lits) 

1075 
end; 

1076 

1077 

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

1080 
val cls_id = string_of_clauseID cls 

1081 
val ax_name = string_of_axiomName cls 

1082 
val knd = string_of_kind cls 

1083 
val lits_str = ResLib.list_to_string' lits 

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

1085 
in 

1086 
(cls_str,tfree_lits) 

1087 
end; 

1088 

1089 

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

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

1091 
"input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "])."; 
15608  1092 

15347  1093 
val delim = "\n"; 
1094 
val tptp_clauses2str = ResLib.list2str_sep delim; 

1095 

1096 

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

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

1098 
arclause_prefix ^ string_of_int(#clause_id arcls); 
15347  1099 

1100 

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

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

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

1104 
in 

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

1106 
end 

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

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

1109 
in 

1110 
pol ^ c ^ "(" ^ str ^ ")" 

1111 
end; 

1112 

1113 

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

1115 

1116 

1117 
fun strings_of_premLits (ArityClause arcls) = map string_of_arLit (#premLits arcls); 

1118 

1119 

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

1121 

1122 
fun tptp_arity_clause arcls = 

1123 
let val arcls_id = string_of_arClauseID arcls 

1124 
val concl_lit = string_of_conclLit arcls 

1125 
val prems_lits = strings_of_premLits arcls 

1126 
val knd = string_of_arKind arcls 

1127 
val all_lits = concl_lit :: prems_lits 

1128 
in 

15452  1129 
"input_clause(" ^ arcls_id ^ "," ^ knd ^ "," ^ (ResLib.list_to_string' all_lits) ^ ")." 
15347  1130 

1131 
end; 

1132 

1133 

1134 
val clrelclause_prefix = "relcls_"; 

1135 

1136 

1137 
fun tptp_classrelLits sub sup = 

1138 
let val tvar = "(T)" 

1139 
in 

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

15347  1142 
end; 
1143 

1144 

1145 
fun tptp_classrelClause (ClassrelClause cls) = 

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

1147 
val sub = #subclass cls 

1148 
val sup = #superclass cls 

1149 
val lits = tptp_classrelLits sub sup 

1150 
in 

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

1152 
end; 

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

1153 

15347  1154 
end; 