author  wenzelm 
Sun, 05 Jun 2005 11:31:22 +0200  
changeset 16259  aed1a8ae4b23 
parent 16157  1764cc98bafd 
child 16357  f1275d2a1dee 
permissions  rwrr 
15789
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15787
diff
changeset

1 
(* ID: $Id$ 
16259  2 
Author: Claire Quigley 
3 
Copyright 2004 University of Cambridge 

15789
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15787
diff
changeset

4 
*) 
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15787
diff
changeset

5 

15642  6 
(******************) 
7 
(* complete later *) 

8 
(******************) 

9 

15684
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15658
diff
changeset

10 
structure Recon_Transfer = 
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15658
diff
changeset

11 
struct 
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15658
diff
changeset

12 

5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15658
diff
changeset

13 
open Recon_Parse 
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15658
diff
changeset

14 
infixr 8 ++; infixr 7 >>; infixr 6 ; 
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15658
diff
changeset

15 

15642  16 
fun not_newline ch = not (ch = "\n"); 
17 

18 

19 

15919
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

20 
(* 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

21 
fun fill_cls_array array n [] = () 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

22 
 fill_cls_array array n (x::xs) = let val _ = Array.update (array, n,x) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

23 
in 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

24 
fill_cls_array array (n+1) (xs) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

25 
end; 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

26 

b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

27 

b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

28 

b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

29 
fun memo_add_clauses ((name:string, (cls:Thm.thm list)), symtable)= 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

30 
symtable := Symtab.update((name , cls), !symtable); 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

31 

b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

32 

b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

33 
fun memo_add_all ([], symtable) = () 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

34 
 memo_add_all ((x::xs),symtable) = let val _ = memo_add_clauses (x, symtable) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

35 
in 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

36 
memo_add_all (xs, symtable) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

37 
end 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

38 

b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

39 
fun memo_find_clause (name, (symtable: Thm.thm list Symtab.table ref)) = case Symtab.lookup (!symtable,name) of 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

40 
NONE => [] 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

41 
SOME cls => cls ; 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

42 

b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

43 

b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

44 
fun retrieve_clause array symtable clausenum = let 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

45 
val (name, clnum) = Array.sub(array, clausenum) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

46 
val clauses = memo_find_clause (name, symtable) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

47 
val clause = get_nth clnum clauses 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

48 
in 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

49 
(name, clause) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

50 
end 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

51 
*) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

52 

15642  53 
(* Versions that include type information *) 
54 

16157  55 
fun string_of_thm thm = 
56 
let val _ = set show_sorts 

57 
val str = Display.string_of_thm thm 

58 
val no_returns =List.filter not_newline (explode str) 

59 
val _ = reset show_sorts 

60 
in 

61 
implode no_returns 

62 
end 

15642  63 

64 

65 
(* check separate args in the watcher program for separating strings with a * or ; or something *) 

66 

67 
fun clause_strs_to_string [] str = str 

68 
 clause_strs_to_string (x::xs) str = clause_strs_to_string xs (str^x^"%") 

69 

70 
fun thmvars_to_string [] str = str 

71 
 thmvars_to_string (x::xs) str = thmvars_to_string xs (str^x^"%") 

72 

73 

74 
fun proofstep_to_string Axiom = "Axiom()" 

16091  75 
 proofstep_to_string (Binary ((a,b), (c,d)))= 
76 
"Binary(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))" 

77 
 proofstep_to_string (Factor (a,b,c)) = 

78 
"Factor("^(string_of_int a)^","^(string_of_int b)^","^(string_of_int c)^")" 

79 
 proofstep_to_string (Para ((a,b), (c,d)))= 

80 
"Para(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))" 

81 
 proofstep_to_string (MRR ((a,b), (c,d))) = 

82 
"MRR(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))" 

83 
 proofstep_to_string (Rewrite((a,b),(c,d))) = 

84 
"Rewrite(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))" 

15642  85 

86 
fun list_to_string [] liststr = liststr 

87 
 list_to_string (x::[]) liststr = liststr^(string_of_int x) 

88 
 list_to_string (x::xs) liststr = list_to_string xs (liststr^(string_of_int x)^",") 

89 

90 

16091  91 
fun proof_to_string (num,(step,clause_strs, thmvars)) = (string_of_int num)^(proofstep_to_string step)^"["^(clause_strs_to_string clause_strs "")^"]["^(thmvars_to_string thmvars "")^"]" 
15642  92 

93 

94 
fun proofs_to_string [] str = str 

95 
 proofs_to_string (x::xs) str = let val newstr = proof_to_string x 

96 
in 

97 
proofs_to_string xs (str^newstr) 

98 
end 

99 

100 

101 

102 
fun init_proofstep_to_string (num, step, clause_strs) = (string_of_int num)^" "^(proofstep_to_string step)^" "^(clause_strs_to_string clause_strs "")^" " 

103 

104 
fun init_proofsteps_to_string [] str = str 

105 
 init_proofsteps_to_string (x::xs) str = let val newstr = init_proofstep_to_string x 

106 
in 

107 
init_proofsteps_to_string xs (str^newstr) 

108 
end 

109 

110 

111 

112 
(*** get a string representing the Isabelle ordered axioms ***) 

113 

16061  114 
fun origAx_to_string (num,(meta,thmvars)) = 
115 
let val clause_strs = ReconOrderClauses.get_meta_lits_bracket meta 

116 
in 

16091  117 
(string_of_int num)^"OrigAxiom()["^ 
118 
(clause_strs_to_string clause_strs "")^"]["^ 

16061  119 
(thmvars_to_string thmvars "")^"]" 
120 
end 

15642  121 

122 

123 
fun origAxs_to_string [] str = str 

124 
 origAxs_to_string (x::xs) str = let val newstr = origAx_to_string x 

125 
in 

126 
origAxs_to_string xs (str^newstr) 

127 
end 

128 

129 

130 
(*** get a string representing the Isabelle ordered axioms not used in the spass proof***) 

131 

16061  132 
fun extraAx_to_string (num, (meta,thmvars)) = 
133 
let val clause_strs = ReconOrderClauses.get_meta_lits_bracket meta 

134 
in 

16091  135 
(string_of_int num)^"ExtraAxiom()["^ 
16061  136 
(clause_strs_to_string clause_strs "")^"]"^ 
137 
"["^(thmvars_to_string thmvars "")^"]" 

138 
end; 

15642  139 

16061  140 
fun extraAxs_to_string [] str = str 
141 
 extraAxs_to_string (x::xs) str = 

142 
let val newstr = extraAx_to_string x 

143 
in 

144 
extraAxs_to_string xs (str^newstr) 

145 
end; 

15642  146 

147 
fun is_axiom ( num:int,Axiom, str) = true 

148 
 is_axiom (num, _,_) = false 

149 

150 
fun get_init_axioms xs = List.filter (is_axiom) ( xs) 

151 

152 
fun get_step_nums [] nums = nums 

153 
 get_step_nums (( num:int,Axiom, str)::xs) nums = get_step_nums xs (nums@[num]) 

154 

15774  155 
exception Noassoc; 
156 

157 
fun assoc_snd a [] = raise Noassoc 

15642  158 
 assoc_snd a ((x, y)::t) = if a = y then x else assoc_snd a t; 
159 

160 
(* change to be something using check_order instead of a = y > returns true if ASSERTION not raised in checkorder, false otherwise *) 

161 

162 
(*fun get_assoc_snds [] xs assocs= assocs 

163 
 get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_snd x ys))]) 

164 
*) 

165 
(*FIX  should this have vars in it? *) 

16061  166 
fun there_out_of_order xs ys = (ReconOrderClauses.checkorder xs ys [] ([],[],[]); true) 
15774  167 
handle _ => false 
15642  168 

15774  169 
fun assoc_out_of_order a [] = raise Noassoc 
15642  170 
 assoc_out_of_order a ((b,c)::t) = if there_out_of_order a c then b else assoc_out_of_order a t; 
171 

172 
fun get_assoc_snds [] xs assocs= assocs 

173 
 get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_out_of_order x ys))]) 

174 

175 
fun add_if_not_inlist [] xs newlist = newlist 

16157  176 
 add_if_not_inlist (y::ys) xs newlist = if (not (y mem xs)) then 
15642  177 
add_if_not_inlist ys xs (y::newlist) 
178 
else add_if_not_inlist ys xs (newlist) 

179 

15700  180 
(*Flattens a list of list of strings to one string*) 
181 
fun onestr ls = String.concat (map String.concat ls); 

15642  182 

183 
fun thmstrings [] str = str 

184 
 thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x)) 

185 

15919
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

186 
fun is_clasimp_ax clasimp_num n = n <=clasimp_num 
15642  187 

15919
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

188 

b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

189 

b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

190 
fun retrieve_axioms clause_arr [] = [] 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

191 
 retrieve_axioms clause_arr (x::xs) = [Array.sub(clause_arr, x)]@ 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

192 
(retrieve_axioms clause_arr xs) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

193 

16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

194 
fun subone x = x  1 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

195 

2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

196 
fun numstr [] = "" 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

197 
 numstr (x::xs) = (string_of_int x)^"%"^(numstr xs) 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

198 

15919
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

199 

b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

200 
(* retrieve the axioms that were obtained from the clasimpset *) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

201 

b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

202 
fun get_clasimp_cls clause_arr clasimp_num step_nums = 
16157  203 
let val realnums = map subone step_nums 
204 
val clasimp_nums = List.filter (is_clasimp_ax (clasimp_num  1)) realnums 

16259  205 
val axnums = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "axnums"))) 
16157  206 
val _ = TextIO.output(axnums,(numstr clasimp_nums)) 
207 
val _ = TextIO.closeOut(axnums) 

208 
in 

209 
retrieve_axioms clause_arr clasimp_nums 

210 
end 

15919
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

211 

16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

212 

2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

213 
(* add array and table here, so can retrieve clasimp axioms *) 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

214 

16157  215 
fun get_axiom_names proof_steps thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses = 
216 
let 

217 
(* not sure why this is necessary again, but seems to be *) 

218 
val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) 

219 
val axioms = get_init_axioms proof_steps 

220 
val step_nums = get_step_nums axioms [] 

221 

222 
(***********************************************) 

223 
(* here need to add the clauses from clause_arr*) 

224 
(***********************************************) 

225 

226 
val (clasimp_names_cls) = get_clasimp_cls clause_arr num_of_clauses step_nums 

227 
val clasimp_names = map (#1 o ResClause.clause_info o #1) clasimp_names_cls 

228 

229 
val _ = File.write (File.tmp_path (Path.basic "clasimp_names")) 

230 
(concat clasimp_names) 

231 
val _ = (print_mode := (["xsymbols", "symbols"] @ ! print_mode)) 

232 
in 

233 
clasimp_names 

234 
end 

16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

235 

2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

236 
fun numclstr (vars, []) str = str 
16157  237 
 numclstr ( vars, ((num, thm)::rest)) str = 
238 
let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" " 

239 
in 

240 
numclstr (vars,rest) newstr 

241 
end 

15919
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

242 

16157  243 
fun addvars c (a,b) = (a,b,c) 
15919
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

244 

b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

245 
fun get_axioms_used proof_steps thms clause_arr num_of_clauses = 
16061  246 
let 
16259  247 
(*val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_ax_thmstr"))) 
16061  248 
val _ = TextIO.output (outfile, thmstring) 
249 

250 
val _ = TextIO.closeOut outfile*) 

251 
(* not sure why this is necessary again, but seems to be *) 

15782  252 

16061  253 
val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) 
254 
val axioms = get_init_axioms proof_steps 

255 
val step_nums = get_step_nums axioms [] 

15919
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

256 

16061  257 
(***********************************************) 
258 
(* here need to add the clauses from clause_arr*) 

259 
(***********************************************) 

15919
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

260 

16061  261 
(* val clasimp_names_cls = get_clasimp_cls clause_arr num_of_clauses step_nums 
262 
val clasimp_names = map #1 clasimp_names_cls 

263 
val clasimp_cls = map #2 clasimp_names_cls 

16259  264 
val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "clasimp_names"))) val clasimp_namestr = concat clasimp_names 
16061  265 
val _ = TextIO.output (outfile,clasimp_namestr) 
266 

267 
val _ = TextIO.closeOut outfile 

15919
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

268 
*) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

269 

16061  270 
val clauses =(*(clasimp_cls)@*)( make_clauses thms) 
271 

272 
val vars = map thm_vars clauses 

273 

274 
val distvars = distinct (fold append vars []) 

275 
val clause_terms = map prop_of clauses 

276 
val clause_frees = List.concat (map term_frees clause_terms) 

15642  277 

16061  278 
val frees = map lit_string_with_nums clause_frees; 
15642  279 

16061  280 
val distfrees = distinct frees 
15642  281 

16061  282 
val metas = map Meson.make_meta_clause clauses 
283 
val ax_strs = map #3 axioms 

15642  284 

16061  285 
(* literals of all axioms, not just those used by spass *) 
286 
val meta_strs = map ReconOrderClauses.get_meta_lits metas 

287 

288 
val metas_and_strs = ListPair.zip (metas,meta_strs) 

16259  289 
val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_clauses"))); 
16061  290 
val _ = TextIO.output (outfile, onestr ax_strs) 
291 

292 
val _ = TextIO.closeOut outfile 

16259  293 
val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_metastrs"))); 
16061  294 
val _ = TextIO.output (outfile, onestr meta_strs) 
295 
val _ = TextIO.closeOut outfile 

15642  296 

16061  297 
(* get list of axioms as thms with their variables *) 
15642  298 

16061  299 
val ax_metas = get_assoc_snds ax_strs metas_and_strs [] 
300 
val ax_vars = map thm_vars ax_metas 

301 
val ax_with_vars = ListPair.zip (ax_metas,ax_vars) 

15642  302 

16061  303 
(* get list of extra axioms as thms with their variables *) 
304 
val extra_metas = add_if_not_inlist metas ax_metas [] 

305 
val extra_vars = map thm_vars extra_metas 

306 
val extra_with_vars = if (not (extra_metas = []) ) 

307 
then 

308 
ListPair.zip (extra_metas,extra_vars) 

309 
else 

310 
[] 

15642  311 

16061  312 
(* val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) 
16259  313 
val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_metas"))) 
15642  314 

16061  315 
val _ = TextIO.output (outfile, ((thmstrings ax_metas ""))) 
316 
val _ = TextIO.closeOut outfile 

16259  317 
val foo_metas = File.platform_path(File.tmp_path (Path.basic "foo_metas")) 
318 
val foo_metas2 = File.platform_path(File.tmp_path (Path.basic "foo_metas2")) 

16061  319 
val execperl = Unix.execute("/usr/bin/perl", ["remchars.pl", " <", foo_metas, " >", foo_metas2]) 
16259  320 
val infile = TextIO.openIn(File.platform_path(File.tmp_path (Path.basic "foo_metas2"))) 
16061  321 
val ax_metas_str = TextIO.inputLine (infile) 
322 
val _ = TextIO.closeIn infile 

323 
val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*) 

324 

325 
in 

326 
(distfrees,distvars, extra_with_vars,ax_with_vars, (*clasimp_names*)(ListPair.zip (step_nums,ax_metas))) 

327 
end 

328 

15642  329 

16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

330 

15642  331 

332 
(*********************************************************************) 

333 
(* Pass in spass string of proof and string version of isabelle goal *) 

334 
(* Get out reconstruction steps as a string to be sent to Isabelle *) 

335 
(*********************************************************************) 

336 

337 

16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

338 
fun rules_to_string [] str = str 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

339 
 rules_to_string [x] str = str^x 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

340 
 rules_to_string (x::xs) str = rules_to_string xs (str^x^" ") 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

341 

15642  342 

16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

343 
val dummy_tac = PRIMITIVE(fn thm => thm ); 
15642  344 

345 

16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

346 
fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses = 
16259  347 
let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "thmstringfile"))); val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr^"goalstr is: "^goalstring^" num of clauses is: "^(string_of_int num_of_clauses))) 
16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

348 
val _ = TextIO.closeOut outfile 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

349 

2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

350 
(***********************************) 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

351 
(* parse spass proof into datatype *) 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

352 
(***********************************) 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

353 

2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

354 
val tokens = #1(lex proofstr) 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

355 
val proof_steps1 = parse tokens 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

356 
val proof_steps = just_change_space proof_steps1 
16259  357 
val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_parse"))); val _ = TextIO.output (outfile, ("Did parsing on "^proofstr)) 
16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

358 
val _ = TextIO.closeOut outfile 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

359 

16259  360 
val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_thmstring_at_parse"))); val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring)) 
16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

361 
val _ = TextIO.closeOut outfile 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

362 
(************************************) 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

363 
(* recreate original subgoal as thm *) 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

364 
(************************************) 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

365 

2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

366 
(* get axioms as correctly numbered clauses w.r.t. the Spass proof *) 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

367 
(* need to get prems_of thm, then get right one of the prems, relating to whichever*) 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

368 
(* subgoal this is, and turn it into meta_clauses *) 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

369 
(* should prob add array and table here, so that we can get axioms*) 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

370 
(* produced from the clasimpset rather than the problem *) 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

371 

2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

372 
val (axiom_names) = get_axiom_names proof_steps thms clause_arr num_of_clauses 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

373 
val ax_str = "Rules from clasimpset used in proof found by SPASS: "^(rules_to_string axiom_names "") 
16259  374 
val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "reconstrfile"))); val _ = TextIO.output (outfile, ("reconstring is: "^ax_str^" "^goalstring)) 
16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

375 
val _ = TextIO.closeOut outfile 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

376 

2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

377 
in 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

378 
TextIO.output (toParent, ax_str^"\n"); 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

379 
TextIO.flushOut toParent; 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

380 
TextIO.output (toParent, "goalstring: "^goalstring^"\n"); 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

381 
TextIO.flushOut toParent; 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

382 
TextIO.output (toParent, "thmstring: "^thmstring^"\n"); 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

383 
TextIO.flushOut toParent; 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

384 

2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

385 
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

386 
(* Attempt to prevent several signals from turning up simultaneously *) 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

387 
Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

388 
end 
16259  389 
handle _ => (let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_handler"))); 
16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

390 

2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

391 
val _ = TextIO.output (outfile, ("In exception handler")); 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

392 
val _ = TextIO.closeOut outfile 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

393 
in 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

394 
TextIO.output (toParent,"Proof found but translation failed!" ^"\n"); 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

395 
TextIO.flushOut toParent; 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

396 
TextIO.output (toParent, thmstring^"\n"); 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

397 
TextIO.flushOut toParent; 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

398 
TextIO.output (toParent, goalstring^"\n"); 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

399 
TextIO.flushOut toParent; 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

400 
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

401 
(* Attempt to prevent several signals from turning up simultaneously *) 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

402 
Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

403 
end) 
15642  404 

405 

406 

15919
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

407 
fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses = 
16259  408 
let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "thmstringfile"))); 
16061  409 
(* val sign = sign_of_thm thm 
410 
val prems = prems_of thm 

411 
val prems_string = concat_with_and (map (Sign.string_of_term sign) prems) "" 

412 
val _ = warning ("thmstring is: "^thmstring);(*("thm in spassStrtoRec: "^(concat_with_and (map string_of_thm thms) "")^*)*) 

413 
val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr)) 

414 
(*val _ = TextIO.output (outfile, (("in spassStrto Reconstr")));*) 

415 
val _ = TextIO.closeOut outfile 

15782  416 

16061  417 
val tokens = #1(lex proofstr) 
15782  418 

16061  419 

15919
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

420 

16061  421 
(***********************************) 
422 
(* parse spass proof into datatype *) 

423 
(***********************************) 

15642  424 

16061  425 
val proof_steps1 = parse tokens 
426 
val proof_steps = just_change_space proof_steps1 

15642  427 

16259  428 
val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_parse"))); val _ = TextIO.output (outfile, ("Did parsing on "^proofstr)) 
16061  429 
val _ = TextIO.closeOut outfile 
430 

16259  431 
val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_thmstring_at_parse"))); val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring)) 
16061  432 
val _ = TextIO.closeOut outfile 
433 
(************************************) 

434 
(* recreate original subgoal as thm *) 

435 
(************************************) 

436 

437 
(* get axioms as correctly numbered clauses w.r.t. the Spass proof *) 

438 
(* need to get prems_of thm, then get right one of the prems, relating to whichever*) 

439 
(* subgoal this is, and turn it into meta_clauses *) 

440 
(* should prob add array and table here, so that we can get axioms*) 

441 
(* produced from the clasimpset rather than the problem *) 

442 
val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps thms clause_arr num_of_clauses 

443 

444 
(*val numcls_string = numclstr ( vars, numcls) ""*) 

16259  445 
val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_axiom"))); val _ = TextIO.output (outfile,"got axioms") 
16061  446 
val _ = TextIO.closeOut outfile 
447 

448 
(************************************) 

449 
(* translate proof *) 

450 
(************************************) 

16259  451 
val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_steps"))); val _ = TextIO.output (outfile, ("about to translate proof, steps: "^(init_proofsteps_to_string proof_steps ""))) 
16061  452 
val _ = TextIO.closeOut outfile 
453 
val (newthm,proof) = translate_proof numcls proof_steps vars 

16259  454 
val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_steps2"))); val _ = TextIO.output (outfile, ("translated proof, steps: "^(init_proofsteps_to_string proof_steps ""))) 
16061  455 
val _ = TextIO.closeOut outfile 
456 
(***************************************************) 

457 
(* transfer necessary steps as strings to Isabelle *) 

458 
(***************************************************) 

459 
(* turn the proof into a string *) 

460 
val reconProofStr = proofs_to_string proof "" 

461 
(* do the bit for the Isabelle ordered axioms at the top *) 

462 
val ax_nums = map #1 numcls 

463 
val ax_strs = map ReconOrderClauses.get_meta_lits_bracket (map #2 numcls) 

464 
val numcls_strs = ListPair.zip (ax_nums,ax_strs) 

465 
val num_cls_vars = map (addvars vars) numcls_strs; 

466 
val reconIsaAxStr = origAxs_to_string (ListPair.zip (ax_nums,ax_with_vars)) "" 

467 

468 
val extra_nums = if (not (extra_with_vars = [])) then (1 upto (length extra_with_vars)) else [] 

469 
val reconExtraAxStr = extraAxs_to_string ( ListPair.zip (extra_nums,extra_with_vars)) "" 

470 
val frees_str = "["^(thmvars_to_string frees "")^"]" 

16259  471 
val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "reconstringfile"))); 
15642  472 

16061  473 
val _ = TextIO.output (outfile, (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)) 
474 
val _ = TextIO.closeOut outfile 

475 
val reconstr = (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr) 

476 
in 

477 
TextIO.output (toParent, reconstr^"\n"); 

478 
TextIO.flushOut toParent; 

479 
TextIO.output (toParent, thmstring^"\n"); 

480 
TextIO.flushOut toParent; 

481 
TextIO.output (toParent, goalstring^"\n"); 

482 
TextIO.flushOut toParent; 

483 

484 
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); 

485 
(* Attempt to prevent several signals from turning up simultaneously *) 

486 
Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac 

487 
end 

16259  488 
handle _ => (let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_handler"))); 
15642  489 

16061  490 
val _ = TextIO.output (outfile, ("In exception handler")); 
491 
val _ = TextIO.closeOut outfile 

492 
in 

493 
TextIO.output (toParent,"Proof found but translation failed!" ^"\n"); 

494 
TextIO.flushOut toParent; 

495 
TextIO.output (toParent, thmstring^"\n"); 

496 
TextIO.flushOut toParent; 

497 
TextIO.output (toParent, goalstring^"\n"); 

498 
TextIO.flushOut toParent; 

499 
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); 

500 
(* Attempt to prevent several signals from turning up simultaneously *) 

501 
Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac 

502 
end) 

15642  503 

504 

505 

506 

507 

508 
(**********************************************************************************) 

509 
(* At other end, want to turn back into datatype so can apply reconstruct_proof. *) 

510 
(* This will be done by the signal handler *) 

511 
(**********************************************************************************) 

512 

513 
(* Parse in the string version of the proof steps for reconstruction *) 

514 
(* Isar format: cl1 [BINARY 0 cl2 0];cl1 [PARAMOD 0 cl2 0]; cl1 [DEMOD 0 cl2];cl1 [FACTOR 1 2];*) 

515 

516 

517 
val term_numstep = 

518 
(number ++ (a (Other ",")) ++ number) >> (fn (a, (_, c)) => (a, c)) 

519 

520 
val extraaxiomstep = (a (Word "ExtraAxiom"))++ (a (Other "(")) ++(a (Other ")")) 

521 
>> (fn (_) => ExtraAxiom) 

522 

523 

524 

525 
val origaxiomstep = (a (Word "OrigAxiom"))++ (a (Other "(")) ++(a (Other ")")) 

526 
>> (fn (_) => OrigAxiom) 

527 

528 

529 
val axiomstep = (a (Word "Axiom"))++ (a (Other "(")) ++(a (Other ")")) 

530 
>> (fn (_) => Axiom) 

531 

532 

533 

534 

535 
val binarystep = (a (Word "Binary")) ++ (a (Other "(")) ++ (a (Other "(")) 

536 
++ term_numstep ++ (a (Other ")")) ++ (a (Other ",")) 

537 
++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")")) 

538 
>> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => Binary (c,e)) 

539 

540 

541 
val parastep = (a (Word "Para")) ++ (a (Other "(")) ++ (a (Other "(")) 

542 
++ term_numstep ++ (a (Other ")")) ++ (a (Other ",")) 

543 
++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")")) 

544 
>> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => Para(c, e)) 

545 

546 
val mrrstep = (a (Word "MRR")) ++ (a (Other "(")) ++ (a (Other "(")) 

547 
++ term_numstep ++ (a (Other ")")) ++ (a (Other ",")) 

548 
++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")")) 

549 
>> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => MRR(c, e)) 

550 

551 

552 
val factorstep = (a (Word "Factor")) ++ (a (Other "(")) 

553 
++ number ++ (a (Other ",")) 

554 
++ number ++ (a (Other ",")) 

555 
++ number ++ (a (Other ")")) 

556 

557 
>> (fn (_, (_, (c, (_, (e,(_,(f,_))))))) => Factor (c,e,f)) 

558 

559 

560 
val rewritestep = (a (Word "Rewrite")) ++ (a (Other "(")) ++ (a (Other "(")) 

561 
++ term_numstep ++ (a (Other ")")) ++ (a (Other ",")) 

562 
++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")")) 

563 
>> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => Rewrite (c,e)) 

564 

565 
val obviousstep = (a (Word "Obvious")) ++ (a (Other "(")) 

566 
++ term_numstep ++ (a (Other ")")) 

567 
>> (fn (_, (_, (c,_))) => Obvious (c)) 

568 

569 
val methodstep = extraaxiomstep  origaxiomstep  axiomstep binarystep  factorstep parastep  mrrstep  rewritestep  obviousstep 

570 

571 

572 
val number_list_step = 

15739
bb2acfed8212
yet more tidying up: removal of some references to Main
paulson
parents:
15700
diff
changeset

573 
( number ++ many ((a (Other ",") ++ number)>> #2)) 
15642  574 
>> (fn (a,b) => (a::b)) 
575 

576 
val numberlist_step = a (Other "[") ++ a (Other "]") 

577 
>>(fn (_,_) => ([]:int list)) 

578 
 a (Other "[") ++ number_list_step ++ a (Other "]") 

579 
>>(fn (_,(a,_)) => a) 

580 

581 

582 

583 
(** change this to allow P (x U) *) 

584 
fun arglist_step input = ( word ++ many word >> (fn (a, b) => (a^" "^(implode_with_space b))) 

585 
word >> (fn (a) => (a)))input 

586 

587 

588 
fun literal_step input = (word ++ a (Other "(") ++ arglist_step ++ a (Other ")") 

589 
>>(fn (a, (b, (c,d))) => (a^" ("^(c)^")")) 

590 
 arglist_step >> (fn (a) => (a)))input 

591 

592 

593 

594 
(* fun term_step input = (a (Other "~") ++ arglist_step ++ a (Other "%")>> (fn (a,(b,c)) => ("~ "^b)) 

595 
 arglist_step ++ a (Other "%")>> (fn (a,b) => a ))input 

596 
*) 

597 

598 

599 
fun term_step input = (a (Other "~") ++ literal_step ++ a (Other "%")>> (fn (a,(b,c)) => ("~ "^b)) 

600 
 literal_step ++ a (Other "%")>> (fn (a,b) => a ))input 

601 

602 

603 

604 

605 
val term_list_step = 

606 
( term_step ++ many ( term_step)) 

607 
>> (fn (a,b) => (a::b)) 

608 

609 

610 
val term_lists_step = a (Other "[") ++ a (Other "]") 

611 
>>(fn (_,_) => ([]:string list)) 

612 
 a (Other "[") ++ term_list_step ++ a (Other "]") 

613 
>>(fn (_,(a,_)) => a) 

614 

615 

616 

617 

618 
fun anytoken_step input = (word>> (fn (a) => a) ) input 

619 
handle NOPARSE_WORD => (number>> (fn (a) => string_of_int a) ) input 

620 
handle NOPARSE_NUMBER => (other_char >> (fn(a) => a)) input 

621 

622 

623 

624 
fun goalstring_step input= (anytoken_step ++ many (anytoken_step ) 

625 
>> (fn (a,b) => (a^" "^(implode b)))) input 

626 

627 

628 

629 
val linestep = number ++ methodstep ++ term_lists_step ++ term_lists_step 

630 
>> (fn (a, (b, (c,d))) => (a,(b,c,d))) 

631 

632 
val lines_step = many linestep 

633 

15739
bb2acfed8212
yet more tidying up: removal of some references to Main
paulson
parents:
15700
diff
changeset

634 
val alllines_step = (term_lists_step ++ lines_step ) ++ finished >> #1 
15642  635 

15739
bb2acfed8212
yet more tidying up: removal of some references to Main
paulson
parents:
15700
diff
changeset

636 
val parse_step = #1 o alllines_step 
15642  637 

638 

639 
(* 

640 
val reconstr ="[P%x%xa%xb%]1OrigAxiom()[P x%~ P U%][U%]3OrigAxiom()[P U%~ P x%][U%]5OrigAxiom()[~ P xa%~ P U%][U%]7OrigAxiom()[P U%P xb%][U%]1Axiom()[P x%~ P U%][U%]3Axiom()[P U%~ P x%][U%]5Axiom()[~ P U%~ P xa%][U%]7Axiom()[P U%P xb%][U%]9Factor(5,0,1)[~ P xa%][]10Binary((9,0),(3,0))[~ P x%][]11Binary((10,0),(1,0))[~ P U%][U%]12Factor(7,0,1)[P xb%][]14Binary((11,0),(12,0))[][]%(EX x::'a::type. ALL y::'a::type. (P::'a::type => bool) x = P y) >(EX x::'a::type. P x) = (ALL y::'a::type. P y)" 

641 
*) 

642 

643 
(************************************************************) 

644 
(* Construct an Isar style proof from a list of proof steps *) 

645 
(************************************************************) 

646 
(* want to assume all axioms, then do haves for the other clauses*) 

647 
(* then show for the last step *) 

648 

649 
(* replace ~ by not here *) 

650 
fun change_nots [] = [] 

651 
 change_nots (x::xs) = if x = "~" 

652 
then 

653 
["\\", "<", "n", "o", "t", ">"]@(change_nots xs) 

654 
else (x::(change_nots xs)) 

655 

656 
(* 

657 
fun clstrs_to_string [] str = str 

658 
 clstrs_to_string (x::[]) str = str^x 

659 
 clstrs_to_string (x::xs) str = clstrs_to_string xs (str^(x^"; ")) 

660 
*) 

661 
fun clstrs_to_string [] str = implode (change_nots (explode str)) 

662 
 clstrs_to_string (x::[]) str = implode (change_nots (explode (str^x))) 

663 
 clstrs_to_string (x::xs) str = implode (change_nots (explode (clstrs_to_string xs (str^(x^"; "))))) 

664 

665 

666 

667 
fun thmvars_to_quantstring [] str = str 

668 
 thmvars_to_quantstring (x::[]) str =str^x^". " 

669 
 thmvars_to_quantstring (x::xs) str = thmvars_to_quantstring xs (str^(x^" ")) 

670 

671 

16091  672 
fun clause_strs_to_isar clstrs [] = "\"\\<lbrakk>"^(clstrs_to_string clstrs "")^"\\<rbrakk> \\<Longrightarrow> False\"" 
673 
 clause_strs_to_isar clstrs thmvars = "\"\\<And>"^(thmvars_to_quantstring thmvars "")^"\\<lbrakk>"^(clstrs_to_string clstrs "")^"\\<rbrakk> \\<Longrightarrow> False\"" 

15642  674 

675 
fun frees_to_string [] str = implode (change_nots (explode str)) 

676 
 frees_to_string (x::[]) str = implode (change_nots (explode (str^x))) 

677 
 frees_to_string (x::xs) str = implode (change_nots (explode (frees_to_string xs (str^(x^" "))))) 

678 

679 
fun frees_to_isar_str [] = "" 

680 
 frees_to_isar_str clstrs = (frees_to_string clstrs "") 

681 

682 

683 
(***********************************************************************) 

684 
(* functions for producing assumptions for the Isabelle ordered axioms *) 

685 
(***********************************************************************) 

686 
(*val str = "[P%x%xa%xb%]1OrigAxiom()[P x%~ P U%][U%]3OrigAxiom()[P U%~ P x%][U%]5OrigAxiom()[~ P xa%~ P U%][U%]7OrigAxiom()[P U%P xb%][U%]1Axiom()[P x%~ P U%][U%]3Axiom()[P U%~ P x%][U%]5Axiom()[~ P U%~ P xa%][U%]7Axiom()[P U%P xb%][U%]9Factor(5,0,1)[~ P xa%][]10Binary((9,0),(3,0))[~ P x%][]11Binary((10,0),(1,0))[~ P U%][U%]12Factor(7,0,1)[P xb%][]14Binary((11,0),(12,0))[][]"; 

687 
num, rule, clausestrs, vars*) 

688 

689 

690 
(* assume the extra clauses  not used in Spass proof *) 

691 

692 
fun is_extraaxiom_step ( num:int,(ExtraAxiom, str, tstr)) = true 

693 
 is_extraaxiom_step (num, _) = false 

694 

695 
fun get_extraaxioms xs = List.filter (is_extraaxiom_step) ( xs) 

696 

697 
fun assume_isar_extraaxiom [] str = str 

698 
 assume_isar_extraaxiom ((numb,(step, clstr, thmvars))::xs) str = assume_isar_extraaxiom xs (str^"and cl"^(string_of_int numb)^"': "^(clause_strs_to_isar clstr thmvars)^"\n " ) 

699 

700 

701 

702 
fun assume_isar_extraaxioms [] = "" 

703 
assume_isar_extraaxioms ((numb,(step, clstrs, thmstrs))::xs) = let val str = "assume cl"^(string_of_int numb)^"': "^(clause_strs_to_isar clstrs thmstrs)^"\n" 

704 
in 

705 
assume_isar_extraaxiom xs str 

706 
end 

707 

708 
(* assume the Isabelle ordered clauses *) 

709 

710 
fun is_origaxiom_step ( num:int,(OrigAxiom, str, tstr)) = true 

711 
 is_origaxiom_step (num, _) = false 

712 

713 
fun get_origaxioms xs = List.filter (is_origaxiom_step) ( xs) 

714 

715 
fun assume_isar_origaxiom [] str = str 

716 
 assume_isar_origaxiom ((numb,(step, clstr, thmvars))::xs) str = assume_isar_origaxiom xs (str^"and cl"^(string_of_int numb)^"': "^(clause_strs_to_isar clstr thmvars)^"\n " ) 

717 

718 

719 

720 
fun assume_isar_origaxioms ((numb,(step, clstrs, thmstrs))::xs) = let val str = "assume cl"^(string_of_int numb)^"': "^(clause_strs_to_isar clstrs thmstrs)^"\n" 

721 
in 

722 
assume_isar_origaxiom xs str 

723 
end 

724 

725 

726 

727 
fun is_axiom_step ( num:int,(Axiom, str, tstr)) = true 

728 
 is_axiom_step (num, _) = false 

729 

730 
fun get_axioms xs = List.filter (is_axiom_step) ( xs) 

731 

732 
fun have_isar_axiomline (numb,(step, clstrs, thmstrs))="have cl"^(string_of_int numb)^": "^(clause_strs_to_isar clstrs thmstrs)^"\n" 

733 

734 
fun by_isar_axiomline (numb,(step, clstrs, thmstrs))="by (rule cl"^ (string_of_int numb)^"') \n" 

735 

736 

737 
fun isar_axiomline (numb, (step, clstrs, thmstrs)) = (have_isar_axiomline (numb,(step,clstrs, thmstrs )))^( by_isar_axiomline(numb,(step,clstrs, thmstrs )) ) 

738 

739 

740 
fun isar_axiomlines [] str = str 

741 
 isar_axiomlines (x::xs) str = isar_axiomlines xs (str^(isar_axiomline x)) 

742 

743 

744 
fun have_isar_line (numb,(step, clstrs, thmstrs))="have cl"^(string_of_int numb)^": "^(clause_strs_to_isar clstrs thmstrs)^"\n" 

745 

746 

16091  747 
fun by_isar_line ((Binary ((a,b), (c,d)))) = 
748 
"by(rule cl"^ 

749 
(string_of_int a)^" [binary "^(string_of_int b)^" cl"^ 

750 
(string_of_int c)^" "^(string_of_int d)^"])\n" 

751 
 by_isar_line ( (Para ((a,b), (c,d)))) = 

752 
"by (rule cl"^ 

753 
(string_of_int a)^" [paramod "^(string_of_int b)^" cl"^ 

754 
(string_of_int c)^" "^(string_of_int d)^"])\n" 

755 
 by_isar_line ((Factor ((a,b,c)))) = 

756 
"by (rule cl"^(string_of_int a)^" [factor "^(string_of_int b)^" "^ 

757 
(string_of_int c)^" ])\n" 

758 
 by_isar_line ( (Rewrite ((a,b),(c,d)))) = 

759 
"by (rule cl"^(string_of_int a)^" [demod "^(string_of_int b)^" "^ 

760 
(string_of_int c)^" "^(string_of_int d)^" ])\n" 

761 
 by_isar_line ( (Obvious ((a,b)))) = 

762 
"by (rule cl"^(string_of_int a)^" [obvious "^(string_of_int b)^" ])\n" 

15642  763 

764 
fun isar_line (numb, (step, clstrs, thmstrs)) = (have_isar_line (numb,(step,clstrs, thmstrs )))^( by_isar_line step) 

765 

766 

767 
fun isar_lines [] str = str 

768 
 isar_lines (x::xs) str = isar_lines xs (str^(isar_line x)) 

769 

770 
fun last_isar_line (numb,( step, clstrs,thmstrs)) = "show \"False\"\n"^(by_isar_line step) 

771 

772 

16091  773 
fun to_isar_proof (frees, xs, goalstring) = 
774 
let val extraaxioms = get_extraaxioms xs 

775 
val extraax_num = length extraaxioms 

776 
val origaxioms_and_steps = Library.drop (extraax_num, xs) 

777 

778 
val origaxioms = get_origaxioms origaxioms_and_steps 

779 
val origax_num = length origaxioms 

780 
val axioms_and_steps = Library.drop (origax_num + extraax_num, xs) 

781 
val axioms = get_axioms axioms_and_steps 

782 

783 
val steps = Library.drop (origax_num, axioms_and_steps) 

784 
val firststeps = ReconOrderClauses.butlast steps 

785 
val laststep = ReconOrderClauses.last steps 

786 
val goalstring = implode(ReconOrderClauses.butlast(explode goalstring)) 

787 

788 
val isar_proof = 

789 
("show \""^goalstring^"\"\n")^ 

790 
("proof (rule ccontr,skolemize, make_clauses) \n")^ 

791 
("fix "^(frees_to_isar_str frees)^"\n")^ 

792 
(assume_isar_extraaxioms extraaxioms)^ 

793 
(assume_isar_origaxioms origaxioms)^ 

794 
(isar_axiomlines axioms "")^ 

795 
(isar_lines firststeps "")^ 

796 
(last_isar_line laststep)^ 

797 
("qed") 

16259  798 
val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "isar_proof_file"))); 
16091  799 

800 
val _ = TextIO.output (outfile, isar_proof) 

801 
val _ = TextIO.closeOut outfile 

802 
in 

803 
isar_proof 

804 
end; 

15642  805 

806 
(* get fix vars from axioms  all Frees *) 

807 
(* check each clause for metavars and /\ over them at each step*) 

808 

809 
(*******************************************************) 

810 
(* This assumes the thm list "numcls" is still there *) 

811 
(* In reality, should probably label it with an *) 

812 
(* ID number identifying the subgoal. This could *) 

813 
(* be passed over to the watcher, e.g. numcls25 *) 

814 
(*******************************************************) 

815 

816 
(* val str = "[S%x%P%R%Q%]1ExtraAxiom()[~ Q U%~ R U%][U%]2ExtraAxiom()[~ Q U%~ P U%][U%]3ExtraAxiom()[Q U%R U%][U%]1OrigAxiom()[S x%][]2OrigAxiom()[P U%R U%][U%]6OrigAxiom()[~ S U%~ P U%][U%]7OrigAxiom()[~ S U%~ R U%][U%]1Axiom()[S x%][]2Axiom()[R U%P U%][U%]6Axiom()[~ P U%~ S U%][U%]7Axiom()[~ R U%~ S U%][U%]8Binary((6,1),(1,0))[~ P x%][]9Binary((7,1),(1,0))[~ R x%][]19Binary((9,0),(2,0))[P x%][]25Binary((8,0),(19,0))[][]"; 

817 

818 
val str = "[P%x%xa%xb%]1OrigAxiom()[P x%~ P U%][U%]3OrigAxiom()[P U%~ P x%][U%]5OrigAxiom()[~ P xa%~ P U%][U%]7OrigAxiom()[P U%P xb%][U%]1Axiom()[P x%~ P U%][U%]3Axiom()[P U%~ P x%][U%]5Axiom()[~ P U%~ P xa%][U%]7Axiom()[P U%P xb%][U%]9Factor(5,0,1)[~ P xa%][]10Binary((9,0),(3,0))[~ P x%][]11Binary((10,0),(1,0))[~ P U%][U%]12Factor(7,0,1)[P xb%][]14Binary((11,0),(12,0))[][]"; 

819 

820 
val reconstr = "[P%Q%x%xa%]1OrigAxiom()[~ P U%][U%]3OrigAxiom()[Q U%][U%]5OrigAxiom()[P (x U)%~ Q (xa U)%][U%]9Binary((7,0),(3,0))[][]7Binary((1,0),(5,0))[~ Q (xa U)%][U%]5Axiom()[P (x U)%~ Q (xa U)%][U%]3Axiom()[Q U%][U%]1Axiom()[~ P U%][U%](ALL xb::'a::type. (~ (P::'a::type => bool) ((x::'a::type => 'a::type) xb)  (Q::'a::type => bool) ((xa::'a::type => 'a::type) xb)) & P xb & ~ Q xb)"; 

821 

822 

823 
val reconstr = "[P%x%xa%xb%]1OrigAxiom()[P x%~ P U%][U%]3OrigAxiom()[P U%~ P x%][U%]5OrigAxiom()[~ P xa%~ P U%][U%]7OrigAxiom()[P U%P xb%][U%]1Axiom()[P x%~ P U%][U%]3Axiom()[P U%~ P x%][U%]5Axiom()[~ P U%~ P xa%][U%]7Axiom()[P U%P xb%][U%]9Factor(5,0,1)[~ P xa%][]10Binary((9,0),(3,0))[~ P x%][]11Binary((10,0),(1,0))[~ P U%][U%]12Factor(7,0,1)[P xb%][]14Binary((11,0),(12,0))[][]"; 

824 

825 
val thmstring = " (ALL xa::'a::type. (~ (P::'a::type => bool) (x::'a::type)  P xa) & (~ P xa  P x)) & (((P::'a::type => bool) (xa::'a::type)  (ALL x::'a::type. P x)) &((ALL x::'a::type. ~ P x)  ~ P (xb::'a::type)))"; 

826 
*) 

827 

15739
bb2acfed8212
yet more tidying up: removal of some references to Main
paulson
parents:
15700
diff
changeset

828 
fun apply_res_thm str goalstring = let val tokens = #1 (lex str); 
15642  829 

830 
val (frees,recon_steps) = parse_step tokens 

831 
val isar_str = to_isar_proof (frees, recon_steps, goalstring) 

16259  832 
val foo = TextIO.openOut (File.platform_path(File.tmp_path (Path.basic "foobar"))); 
15642  833 
in 
834 
TextIO.output(foo,(isar_str));TextIO.closeOut foo;Pretty.writeln(Pretty.str isar_str); () 

835 
end 

836 

837 

16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

838 

2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

839 

15684
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15658
diff
changeset

840 
end; 