49 end |
49 end |
50 *) |
50 *) |
51 |
51 |
52 (* Versions that include type information *) |
52 (* Versions that include type information *) |
53 |
53 |
|
54 (* FIXME rename to str_of_thm *) |
54 fun string_of_thm thm = |
55 fun string_of_thm thm = |
55 let val _ = set show_sorts |
56 setmp show_sorts true (Pretty.str_of o Display.pretty_thm) thm; |
56 val str = Display.string_of_thm thm |
|
57 val no_returns =List.filter not_newline (explode str) |
|
58 val _ = reset show_sorts |
|
59 in |
|
60 implode no_returns |
|
61 end |
|
62 |
57 |
63 |
58 |
64 (* check separate args in the watcher program for separating strings with a * or ; or something *) |
59 (* check separate args in the watcher program for separating strings with a * or ; or something *) |
65 |
60 |
66 fun clause_strs_to_string [] str = str |
61 fun clause_strs_to_string [] str = str |
375 \1279[0:Inp] || -> equal(const_Nat_Osize(tconst_fun(tconst_List_Olist(U),tconst_nat),const_List_Olist_ONil),const_0)**.\ |
370 \1279[0:Inp] || -> equal(const_Nat_Osize(tconst_fun(tconst_List_Olist(U),tconst_nat),const_List_Olist_ONil),const_0)**.\ |
376 \1430[0:Inp] || equal(const_Nat_Osize(tconst_fun(tconst_List_Olist(typ__Ha),tconst_nat),const_List_Orev(tconst_fun(tconst_List_Olist(typ__Ha),tconst_List_Olist(typ__Ha)),const_List_Olist_ONil)),const_Nat_Osize(tconst_fun(tconst_List_Olist(typ__Ha),tconst_nat),const_List_Olist_ONil))** -> .\ |
371 \1430[0:Inp] || equal(const_Nat_Osize(tconst_fun(tconst_List_Olist(typ__Ha),tconst_nat),const_List_Orev(tconst_fun(tconst_List_Olist(typ__Ha),tconst_List_Olist(typ__Ha)),const_List_Olist_ONil)),const_Nat_Osize(tconst_fun(tconst_List_Olist(typ__Ha),tconst_nat),const_List_Olist_ONil))** -> .\ |
377 \1453[0:Rew:1279.0,1430.0,1242.0,1430.0,1279.0,1430.0] || equal(const_0,const_0)* -> .\ |
372 \1453[0:Rew:1279.0,1430.0,1242.0,1430.0,1279.0,1430.0] || equal(const_0,const_0)* -> .\ |
378 \1454[0:Obv:1453.0] || -> .";*) |
373 \1454[0:Obv:1453.0] || -> .";*) |
379 |
374 |
380 fun remove_linebreaks str = let val strlist = explode str |
|
381 val nonewlines = filter (not_equal "\n") strlist |
|
382 in |
|
383 implode nonewlines |
|
384 end |
|
385 |
|
386 |
|
387 fun subst_for a b [] = "" |
375 fun subst_for a b [] = "" |
388 | subst_for a b (x::xs) = if (x = a) |
376 | subst_for a b (x :: xs) = |
389 then |
377 if x = a |
390 (b^(subst_for a b xs)) |
378 then |
391 else |
379 b ^ subst_for a b xs |
392 x^(subst_for a b xs) |
380 else |
393 |
381 x ^ subst_for a b xs; |
394 |
382 |
395 fun remove_linebreaks str = let val strlist = explode str |
383 val remove_linebreaks = subst_for "\n" "\t" o explode; |
396 in |
384 val restore_linebreaks = subst_for "\t" "\n" o explode; |
397 subst_for "\n" "\t" strlist |
|
398 end |
|
399 |
|
400 fun restore_linebreaks str = let val strlist = explode str |
|
401 in |
|
402 subst_for "\t" "\n" strlist |
|
403 end |
|
404 |
|
405 |
385 |
406 |
386 |
407 fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses = |
387 fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses = |
408 let val outfile = TextIO.openAppend( File.platform_path(File.tmp_path (Path.basic"thmstringfile"))); |
388 let val outfile = TextIO.openAppend( File.platform_path(File.tmp_path (Path.basic"thmstringfile"))); |
409 val _ = TextIO.output (outfile, ("thmstring is: "^thmstring^"\n proofstr is: "^proofstr^"\n goalstr is: "^goalstring^" \n num of clauses is: "^(string_of_int num_of_clauses))) |
389 val _ = TextIO.output (outfile, ("thmstring is: "^thmstring^"\n proofstr is: "^proofstr^"\n goalstr is: "^goalstring^" \n num of clauses is: "^(string_of_int num_of_clauses))) |