src/HOL/Tools/ATP/recon_transfer_proof.ML
author quigley
Wed Jun 22 20:26:31 2005 +0200 (2005-06-22)
changeset 16548 aa36ae6b955e
parent 16520 7a9cda53bfa2
child 16803 014090d1e64b
permissions -rw-r--r--
Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
Will now signal if ATP has run out of time and then kill the watcher.
     1 (*  ID:         $Id$
     2     Author:     Claire Quigley
     3     Copyright   2004  University of Cambridge
     4 *)
     5 
     6 (******************)
     7 (* complete later *)
     8 (******************)
     9 
    10 structure Recon_Transfer =
    11 struct
    12 open Recon_Parse
    13 infixr 8 ++; infixr 7 >>; infixr 6 ||;
    14 
    15 fun not_newline ch = not (ch = "\n");
    16 
    17 
    18 
    19 (*
    20 fun fill_cls_array array n [] = ()
    21 |   fill_cls_array array n (x::xs) = let val _ = Array.update (array, n,x)
    22                                      in
    23                                         fill_cls_array array (n+1) (xs)
    24                                      end;
    25 
    26 
    27 
    28 fun memo_add_clauses ((name:string, (cls:Thm.thm list)), symtable)=
    29                         symtable := Symtab.update((name , cls), !symtable);
    30       	       
    31 
    32 fun memo_add_all ([], symtable) = ()
    33 |   memo_add_all ((x::xs),symtable) = let val _ = memo_add_clauses (x, symtable)
    34                            in
    35                                memo_add_all (xs, symtable)
    36                            end
    37 
    38 fun memo_find_clause (name, (symtable: Thm.thm list Symtab.table ref)) = case Symtab.lookup (!symtable,name) of
    39       	        NONE =>  []
    40                 |SOME cls  => cls ;
    41       	        	
    42 
    43 fun retrieve_clause array symtable clausenum = let
    44                                                   val (name, clnum) = Array.sub(array, clausenum)
    45                                                   val clauses = memo_find_clause (name, symtable)
    46                                                   val clause = get_nth clnum clauses
    47                                                in
    48                                                   (name, clause)
    49                                                end
    50  *)                                             
    51 
    52 (* Versions that include type information *)
    53  
    54 fun string_of_thm thm =
    55   let val _ = set show_sorts
    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 
    63 
    64 (* check separate args in the watcher program for separating strings with a * or ; or something *)
    65 
    66 fun clause_strs_to_string [] str = str
    67 |   clause_strs_to_string (x::xs) str = clause_strs_to_string xs (str^x^"%")
    68 
    69 fun thmvars_to_string [] str = str
    70 |   thmvars_to_string (x::xs) str = thmvars_to_string xs (str^x^"%")
    71 
    72 
    73 fun proofstep_to_string Axiom = "Axiom()"
    74 |   proofstep_to_string  (Binary ((a,b), (c,d)))=
    75       "Binary(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"
    76 |   proofstep_to_string (Factor (a,b,c)) =
    77       "Factor("^(string_of_int a)^","^(string_of_int b)^","^(string_of_int c)^")"
    78 |   proofstep_to_string  (Para ((a,b), (c,d)))= 
    79       "Para(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"
    80 |   proofstep_to_string  (MRR ((a,b), (c,d))) =
    81       "MRR(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"
    82 (*|   proofstep_to_string (Rewrite((a,b),(c,d))) =
    83       "Rewrite(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"*)
    84 
    85 fun list_to_string [] liststr = liststr
    86 |   list_to_string (x::[]) liststr = liststr^(string_of_int x)
    87 |   list_to_string (x::xs) liststr = list_to_string xs (liststr^(string_of_int x)^",")
    88 
    89 
    90 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 "")^"]"
    91  
    92 
    93 fun proofs_to_string [] str = str
    94 |   proofs_to_string (x::xs) str = let val newstr = proof_to_string x 
    95                                    in
    96                                        proofs_to_string xs (str^newstr)
    97                                    end
    98 
    99 
   100 
   101 fun init_proofstep_to_string (num, step, clause_strs) = (string_of_int num)^" "^(proofstep_to_string step)^" "^(clause_strs_to_string clause_strs "")^" "
   102 
   103 fun init_proofsteps_to_string [] str = str
   104 |   init_proofsteps_to_string (x::xs) str = let val newstr = init_proofstep_to_string x 
   105                                    in
   106                                        init_proofsteps_to_string xs (str^newstr)
   107                                    end
   108   
   109 
   110 
   111 (*** get a string representing the Isabelle ordered axioms ***)
   112 
   113 fun origAx_to_string (num,(meta,thmvars)) =
   114     let val clause_strs = ReconOrderClauses.get_meta_lits_bracket meta
   115     in
   116        (string_of_int num)^"OrigAxiom()["^
   117        (clause_strs_to_string clause_strs "")^"]["^
   118        (thmvars_to_string thmvars "")^"]"
   119     end
   120 
   121 
   122 fun  origAxs_to_string [] str = str
   123 |   origAxs_to_string (x::xs) str = let val newstr = origAx_to_string x 
   124                                    in
   125                                        origAxs_to_string xs (str^newstr)
   126                                    end
   127 
   128 
   129 (*** get a string representing the Isabelle ordered axioms not used in the spass proof***)
   130 
   131 fun extraAx_to_string (num, (meta,thmvars)) =
   132    let val clause_strs = ReconOrderClauses.get_meta_lits_bracket meta
   133    in
   134       (string_of_int num)^"ExtraAxiom()["^
   135       (clause_strs_to_string clause_strs "")^"]"^
   136       "["^(thmvars_to_string thmvars "")^"]"
   137    end;
   138 
   139 fun extraAxs_to_string [] str = str
   140 |   extraAxs_to_string (x::xs) str =
   141       let val newstr = extraAx_to_string x 
   142       in
   143 	  extraAxs_to_string xs (str^newstr)
   144       end;
   145 
   146 fun is_axiom ( num:int,Axiom, str) = true
   147 |   is_axiom (num, _,_) = false
   148 
   149 fun get_init_axioms xs = List.filter (is_axiom) ( xs)
   150 
   151 fun get_step_nums [] nums = nums
   152 |   get_step_nums (( num:int,Axiom, str)::xs) nums = get_step_nums xs (nums@[num])
   153 
   154 exception Noassoc;
   155 
   156 fun assoc_snd a [] = raise Noassoc
   157   | assoc_snd a ((x, y)::t) = if a = y then x else assoc_snd a t;
   158 
   159 (* change to be something using check_order  instead of a = y --> returns true if ASSERTION not raised in checkorder, false otherwise *)
   160 
   161 (*fun get_assoc_snds [] xs assocs= assocs
   162 |   get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_snd x ys))])
   163 *)
   164 (*FIX - should this have vars in it? *)
   165 fun there_out_of_order xs ys = (ReconOrderClauses.checkorder xs ys [] ([],[],[]); true) 
   166                                handle _ => false
   167 
   168 fun assoc_out_of_order a [] = raise Noassoc
   169 |   assoc_out_of_order a ((b,c)::t) = if there_out_of_order a c then b else assoc_out_of_order a t;
   170 
   171 fun get_assoc_snds [] xs assocs= assocs
   172 |   get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_out_of_order x ys))])
   173 
   174 fun add_if_not_inlist [] xs newlist = newlist
   175 |   add_if_not_inlist (y::ys) xs newlist = if (not (y mem xs)) then 
   176                                       add_if_not_inlist ys xs (y::newlist)
   177                                         else add_if_not_inlist ys xs (newlist)
   178 
   179 (*Flattens a list of list of strings to one string*)
   180 fun onestr ls = String.concat (map String.concat ls);
   181 
   182 fun thmstrings [] str = str
   183 |   thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x))
   184 
   185 fun is_clasimp_ax clasimp_num n = n <=clasimp_num 
   186 
   187 
   188 
   189 fun retrieve_axioms clause_arr  [] = []
   190 |   retrieve_axioms clause_arr  (x::xs) =  [Array.sub(clause_arr, x)]@
   191  						     (retrieve_axioms clause_arr  xs)
   192 
   193 fun subone x = x - 1
   194 
   195 fun numstr [] = ""
   196 |   numstr (x::xs) = (string_of_int x)^"%"^(numstr xs)
   197 
   198 
   199 (* retrieve the axioms that were obtained from the clasimpset *)
   200 
   201 fun get_clasimp_cls clause_arr clasimp_num step_nums = 
   202     let val realnums = map subone step_nums	
   203 	val clasimp_nums = List.filter (is_clasimp_ax (clasimp_num - 1)) realnums
   204 (*	val axnums = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "axnums")))     
   205 	val _ = TextIO.output(axnums,(numstr clasimp_nums))
   206 	val _ = TextIO.closeOut(axnums)*)
   207     in
   208 	retrieve_axioms clause_arr  clasimp_nums
   209     end
   210 
   211 
   212 
   213 (*****************************************************)
   214 (* get names of clasimp axioms used                  *)
   215 (*****************************************************)
   216 
   217  fun get_axiom_names proof_steps thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses  =
   218    let 
   219      (* not sure why this is necessary again, but seems to be *)
   220       val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
   221       val axioms = get_init_axioms proof_steps
   222       val step_nums = get_step_nums axioms []
   223   
   224      (***********************************************)
   225      (* here need to add the clauses from clause_arr*)
   226      (***********************************************)
   227   
   228       val (clasimp_names_cls) = get_clasimp_cls clause_arr num_of_clauses step_nums 
   229       val clasimp_names = map (#1 o ResClause.clause_info o #1) clasimp_names_cls
   230   
   231       val _ = File.write (File.tmp_path (Path.basic "clasimp_names"))                                                               
   232                          (concat clasimp_names)
   233       val _ = (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
   234    in
   235       clasimp_names
   236    end
   237     
   238  fun get_axiom_names_vamp proofstr thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses  =
   239    let 
   240      (* not sure why this is necessary again, but seems to be *)
   241       val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
   242       val step_nums =get_linenums proofstr
   243   
   244      (***********************************************)
   245      (* here need to add the clauses from clause_arr*)
   246      (***********************************************)
   247   
   248       val (clasimp_names_cls) = get_clasimp_cls clause_arr num_of_clauses step_nums 
   249       val clasimp_names = map (#1 o ResClause.clause_info o #1) clasimp_names_cls
   250   
   251       val _ = File.write (File.tmp_path (Path.basic "clasimp_names"))                                                               
   252                          (concat clasimp_names)
   253       val _ = (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
   254    in
   255       clasimp_names
   256    end
   257     
   258 
   259 
   260 
   261 (***********************************************)
   262 (* get axioms for reconstruction               *)
   263 (***********************************************)
   264 fun numclstr (vars, []) str = str
   265 |   numclstr ( vars, ((num, thm)::rest)) str =
   266       let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" "
   267       in
   268         numclstr  (vars,rest) newstr
   269       end
   270 
   271 fun addvars c (a,b)  = (a,b,c)
   272 
   273  fun get_axioms_used proof_steps thms clause_arr num_of_clauses  =
   274      let 
   275 	 (*val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_ax_thmstr")))                                                                      
   276 	 val _ = TextIO.output (outfile, thmstring)
   277 	 
   278 	 val _ =  TextIO.closeOut outfile*)
   279 	(* not sure why this is necessary again, but seems to be *)
   280 
   281 	val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
   282 	val axioms = get_init_axioms proof_steps
   283 	val step_nums = get_step_nums axioms []
   284 
   285        (***********************************************)
   286        (* here need to add the clauses from clause_arr*)
   287        (***********************************************)
   288 
   289        (* val clasimp_names_cls = get_clasimp_cls clause_arr   num_of_clauses step_nums   
   290 	val clasimp_names = map #1 clasimp_names_cls
   291 	val clasimp_cls = map #2 clasimp_names_cls
   292 	val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "clasimp_names")))                                                            val clasimp_namestr = concat clasimp_names                            
   293 	 val _ = TextIO.output (outfile,clasimp_namestr)
   294 	 
   295 	 val _ =  TextIO.closeOut outfile
   296 *)
   297 
   298 	val clauses =(*(clasimp_cls)@*)( make_clauses thms)
   299 	
   300 	val vars = map thm_vars clauses
   301        
   302 	val distvars = distinct (fold append vars [])
   303 	val clause_terms = map prop_of clauses  
   304 	val clause_frees = List.concat (map term_frees clause_terms)
   305 
   306 	val frees = map lit_string_with_nums clause_frees;
   307 
   308 	val distfrees = distinct frees
   309 
   310 	val metas = map Meson.make_meta_clause clauses
   311 	val ax_strs = map #3 axioms
   312 
   313 	(* literals of -all- axioms, not just those used by spass *)
   314 	val meta_strs = map ReconOrderClauses.get_meta_lits metas
   315        
   316 	val metas_and_strs = ListPair.zip (metas,meta_strs)
   317 	 val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_clauses")));                                                                       
   318 	 val _ = TextIO.output (outfile, onestr ax_strs)
   319 	 
   320 	 val _ =  TextIO.closeOut outfile
   321 	 val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_metastrs")));                                                                       
   322 	 val _ = TextIO.output (outfile, onestr meta_strs)
   323 	 val _ =  TextIO.closeOut outfile
   324 
   325 	(* get list of axioms as thms with their variables *)
   326 
   327 	val ax_metas = get_assoc_snds ax_strs metas_and_strs []
   328 	val ax_vars = map thm_vars ax_metas
   329 	val ax_with_vars = ListPair.zip (ax_metas,ax_vars)
   330 
   331 	(* get list of extra axioms as thms with their variables *)
   332 	val extra_metas = add_if_not_inlist metas ax_metas []
   333 	val extra_vars = map thm_vars extra_metas
   334 	val extra_with_vars = if (not (extra_metas = []) ) 
   335 			      then
   336 				     ListPair.zip (extra_metas,extra_vars)
   337 			      else
   338 				     []
   339 
   340        (* val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
   341        val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_metas")))
   342 
   343        val _ = TextIO.output (outfile, ((thmstrings ax_metas "")))
   344        val _ =  TextIO.closeOut outfile
   345       val foo_metas =  File.platform_path(File.tmp_path (Path.basic "foo_metas"))
   346       val foo_metas2 =   File.platform_path(File.tmp_path (Path.basic "foo_metas2"))
   347 	val execperl = Unix.execute("/usr/bin/perl", ["remchars.pl", "  <", foo_metas, "  >", foo_metas2])
   348      val infile = TextIO.openIn(File.platform_path(File.tmp_path (Path.basic "foo_metas2")))
   349     val ax_metas_str = TextIO.inputLine (infile)
   350     val _ = TextIO.closeIn infile
   351        val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*)
   352        
   353      in
   354 	(distfrees,distvars, extra_with_vars,ax_with_vars, (*clasimp_names*)(ListPair.zip (step_nums,ax_metas)))
   355      end
   356     
   357 
   358                                         
   359 
   360 (*********************************************************************)
   361 (* Pass in spass string of proof and string version of isabelle goal *)
   362 (* Get out reconstruction steps as a string to be sent to Isabelle   *)
   363 (*********************************************************************)
   364 
   365 
   366 fun rules_to_string [] str = str
   367 |   rules_to_string [x] str = str^x
   368 |   rules_to_string (x::xs) str = rules_to_string xs (str^x^"   ")
   369                                   
   370 
   371 val dummy_tac = PRIMITIVE(fn thm => thm );
   372 
   373 
   374 (*val  proofstr = "1242[0:Inp] ||  -> equal(const_List_Orev(tconst_fun(tconst_List_Olist(U),tconst_List_Olist(U)),const_List_Olist_ONil),const_List_Olist_ONil)**.\
   375 \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))** -> .\
   377 \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] ||  -> .";*)
   379 
   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 [] = ""
   388 |   subst_for a b (x::xs) = if (x = a)
   389 				   then 
   390 					(b^(subst_for a b  xs))
   391 				   else
   392 					x^(subst_for a b xs)
   393 
   394 
   395 fun remove_linebreaks str = let val strlist = explode str
   396 			    in
   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 
   406 
   407 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")));          
   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)))
   410 
   411               	val _ =  TextIO.closeOut outfile
   412 
   413                  (***********************************)
   414                  (* parse spass proof into datatype *)
   415                  (***********************************)
   416          
   417                   val tokens = #1(lex proofstr)
   418                   val proof_steps1 = parse tokens
   419                   val proof_steps = just_change_space proof_steps1
   420                   val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_parse")));        val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
   421                                                   val _ =  TextIO.closeOut outfile
   422                                                 
   423                                                   val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_thmstring_at_parse")));                                        val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
   424                                                   val _ =  TextIO.closeOut outfile
   425                                               (************************************)
   426                                               (* recreate original subgoal as thm *)
   427                                               (************************************)
   428                                                 
   429                                                   (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
   430                                                   (* need to get prems_of thm, then get right one of the prems, relating to whichever*)
   431                                                   (* subgoal this is, and turn it into meta_clauses *)
   432                                                   (* should prob add array and table here, so that we can get axioms*)
   433                                                   (* produced from the clasimpset rather than the problem *)
   434 
   435                                                   val (axiom_names) = get_axiom_names proof_steps  thms clause_arr  num_of_clauses
   436                                                   val ax_str = "Rules from clasimpset used in proof found by SPASS: "^(rules_to_string axiom_names "")
   437                                                   val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "reconstrfile")));                                                     val _ = TextIO.output (outfile, ("reconstring is: "^ax_str^"  "^goalstring))
   438                                                   val _ =  TextIO.closeOut outfile
   439                                                    
   440                                               in 
   441                                                    TextIO.output (toParent, ax_str^"\n");
   442                                                    TextIO.flushOut toParent;
   443                                         	   TextIO.output (toParent, "goalstring: "^goalstring^"\n");
   444                                          	   TextIO.flushOut toParent;
   445                                          	   TextIO.output (toParent, "thmstring: "^thmstring^"\n");
   446                                          	   TextIO.flushOut toParent;
   447                                           
   448                                          	   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   449                                          	  (* Attempt to prevent several signals from turning up simultaneously *)
   450                                          	   Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
   451                                               end
   452                                               handle _ => (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_handler")));
   453 
   454                                                   val _ = TextIO.output (outfile, ("In exception handler"));
   455                                                   val _ =  TextIO.closeOut outfile
   456                                               in 
   457                                                  TextIO.output (toParent,"Proof found but parsing failed for resolution proof: "^(remove_linebreaks proofstr)^"\n" );
   458                                                   TextIO.flushOut toParent;
   459 						   TextIO.output (toParent, (remove_linebreaks thmstring)^"\n");
   460                                          	   TextIO.flushOut toParent;
   461                                          	   TextIO.output (toParent, ( (remove_linebreaks goalstring)^"\n"));
   462                                          	   TextIO.flushOut toParent;
   463             					  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   464                                          	  (* Attempt to prevent several signals from turning up simultaneously *)
   465                                          	  Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
   466                                               end)
   467 
   468 
   469 fun vampString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   470            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)))
   471                                                val _ =  TextIO.closeOut outfile
   472 
   473                                               (***********************************)
   474                                               (* get vampire axiom names         *)
   475                                               (***********************************)
   476          
   477                                                val (axiom_names) = get_axiom_names_vamp proofstr  thms clause_arr  num_of_clauses
   478                                                val ax_str = "Rules from clasimpset used in proof found by Vampire: "^(rules_to_string axiom_names "")
   479                                                val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "reconstrfile")));                                                    val _ = TextIO.output (outfile, ("reconstring is: "^ax_str^"  "^goalstring))
   480                                                val _ =  TextIO.closeOut outfile
   481                                                    
   482                                               in 
   483                                                    TextIO.output (toParent, ax_str^"\n");
   484                                                    TextIO.flushOut toParent;
   485                                         	   TextIO.output (toParent, "goalstring: "^goalstring^"\n");
   486                                          	   TextIO.flushOut toParent;
   487                                          	   TextIO.output (toParent, "thmstring: "^thmstring^"\n");
   488                                          	   TextIO.flushOut toParent;
   489                                           
   490                                          	   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   491                                          	  (* Attempt to prevent several signals from turning up simultaneously *)
   492                                          	   Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
   493                                               end
   494                                               handle _ => (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_handler")));
   495 
   496                                                   val _ = TextIO.output (outfile, ("In exception handler"));
   497                                                   val _ =  TextIO.closeOut outfile
   498                                               in 
   499                                                   TextIO.output (toParent,"Proof found by Vampire but translation failed for resolution proof: "^(remove_linebreaks proofstr) );
   500                                                   TextIO.flushOut toParent;
   501 						   TextIO.output (toParent, thmstring^"\n");
   502                                          	   TextIO.flushOut toParent;
   503                                          	   TextIO.output (toParent, goalstring^"\n");
   504                                          	   TextIO.flushOut toParent;
   505             					  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   506                                          	  (* Attempt to prevent several signals from turning up simultaneously *)
   507                                          	  Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
   508                                               end)
   509 
   510 
   511 
   512 
   513 (* val proofstr = "1582[0:Inp] || -> v_P*.\
   514                  \1583[0:Inp] || v_P* -> .\
   515 		 \1584[0:MRR:1583.0,1582.0] || -> ."; *)
   516 
   517 fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   518       let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "thmstringfile")));                                        
   519 	  (* val sign = sign_of_thm thm
   520 	 val prems = prems_of thm
   521 	 val prems_string =  concat_with_and (map (Sign.string_of_term sign) prems) "" 
   522 	  val _ = warning ("thmstring is: "^thmstring);(*("thm in spassStrtoRec: "^(concat_with_and (map string_of_thm thms) "")^*)*)
   523 	  val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr))
   524 (*val _ = TextIO.output (outfile, (("in spassStrto Reconstr")));*)
   525 	  val _ =  TextIO.closeOut outfile
   526 
   527 	  val tokens = #1(lex proofstr)
   528 
   529 	    
   530 
   531       (***********************************)
   532       (* parse spass proof into datatype *)
   533       (***********************************)
   534 
   535 	  val proof_steps1 = parse tokens
   536 	  val proof_steps = just_change_space proof_steps1
   537 
   538 	  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_parse")));                                                                                          val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
   539 	  val _ =  TextIO.closeOut outfile
   540 	
   541 	  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_thmstring_at_parse")));                                                                             val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
   542 	  val _ =  TextIO.closeOut outfile
   543       (************************************)
   544       (* recreate original subgoal as thm *)
   545       (************************************)
   546 	
   547 	  (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
   548 	  (* need to get prems_of thm, then get right one of the prems, relating to whichever*)
   549 	  (* subgoal this is, and turn it into meta_clauses *)
   550 	  (* should prob add array and table here, so that we can get axioms*)
   551 	  (* produced from the clasimpset rather than the problem *)
   552 	  val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps  thms clause_arr  num_of_clauses
   553 	  
   554 	  (*val numcls_string = numclstr ( vars, numcls) ""*)
   555 	  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_axiom")));                                                                            val _ = TextIO.output (outfile,"got axioms")
   556 	  val _ =  TextIO.closeOut outfile
   557 	    
   558       (************************************)
   559       (* translate proof                  *)
   560       (************************************)
   561 	  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 "")))
   562 	  val _ =  TextIO.closeOut outfile
   563 	  val (newthm,proof) = translate_proof numcls  proof_steps vars
   564 	  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 "")))
   565 	  val _ =  TextIO.closeOut outfile
   566       (***************************************************)
   567       (* transfer necessary steps as strings to Isabelle *)
   568       (***************************************************)
   569 	  (* turn the proof into a string *)
   570 	  val reconProofStr = proofs_to_string proof ""
   571 	  (* do the bit for the Isabelle ordered axioms at the top *)
   572 	  val ax_nums = map #1 numcls
   573 	  val ax_strs = map ReconOrderClauses.get_meta_lits_bracket (map #2 numcls)
   574 	  val numcls_strs = ListPair.zip (ax_nums,ax_strs)
   575 	  val num_cls_vars =  map (addvars vars) numcls_strs;
   576 	  val reconIsaAxStr = origAxs_to_string (ListPair.zip (ax_nums,ax_with_vars)) ""
   577 	  
   578 	  val extra_nums = if (not (extra_with_vars = [])) then (1 upto (length extra_with_vars)) else []
   579 	  val reconExtraAxStr = extraAxs_to_string ( ListPair.zip (extra_nums,extra_with_vars)) ""
   580 	  val frees_str = "["^(thmvars_to_string frees "")^"]"
   581 	  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "reconstringfile")));
   582 
   583 	  val _ = TextIO.output (outfile, (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr))
   584 	  val _ =  TextIO.closeOut outfile
   585 	  val reconstr = (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
   586       in 
   587 	   TextIO.output (toParent, reconstr^"\n");
   588 	   TextIO.flushOut toParent;
   589 	   TextIO.output (toParent, thmstring^"\n");
   590 	   TextIO.flushOut toParent;
   591 	   TextIO.output (toParent, goalstring^"\n");
   592 	   TextIO.flushOut toParent;
   593   
   594 	   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   595 	  (* Attempt to prevent several signals from turning up simultaneously *)
   596 	   Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
   597       end
   598       handle _ => (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_handler")));
   599 
   600 	  val _ = TextIO.output (outfile, ("In exception handler"));
   601 	  val _ =  TextIO.closeOut outfile
   602       in 
   603 	   TextIO.output (toParent,"Proof found but translation failed for resolution proof:"^(remove_linebreaks proofstr) ^"\n");
   604 	  TextIO.flushOut toParent;
   605 	TextIO.output (toParent, thmstring^"\n");
   606 	   TextIO.flushOut toParent;
   607 	   TextIO.output (toParent, goalstring^"\n");
   608 	   TextIO.flushOut toParent;
   609 	  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   610 	  (* Attempt to prevent several signals from turning up simultaneously *)
   611 	  Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
   612       end)
   613 
   614 
   615 
   616 
   617 
   618 (**********************************************************************************)
   619 (* At other end, want to turn back into datatype so can apply reconstruct_proof.  *)
   620 (* This will be done by the signal handler                                        *)
   621 (**********************************************************************************)
   622 
   623 (* Parse in the string version of the proof steps for reconstruction *)
   624 (* Isar format: cl1 [BINARY 0 cl2 0];cl1 [PARAMOD 0 cl2 0]; cl1 [DEMOD 0 cl2];cl1 [FACTOR 1 2];*)
   625 
   626 
   627  val term_numstep =
   628         (number ++ (a (Other ",")) ++ number) >> (fn (a, (_, c)) => (a, c))
   629 
   630 val extraaxiomstep = (a (Word "ExtraAxiom"))++ (a (Other "(")) ++(a (Other ")"))
   631             >> (fn (_) => ExtraAxiom)
   632 
   633 
   634 
   635 val origaxiomstep = (a (Word "OrigAxiom"))++ (a (Other "(")) ++(a (Other ")"))
   636             >> (fn (_) => OrigAxiom)
   637 
   638 
   639  val axiomstep = (a (Word "Axiom"))++ (a (Other "(")) ++(a (Other ")"))
   640             >> (fn (_) => Axiom)
   641      
   642 
   643 
   644       
   645  val binarystep = (a (Word "Binary")) ++ (a (Other "(")) ++ (a (Other "(")) 
   646                    ++ term_numstep  ++ (a (Other ")")) ++ (a (Other ","))
   647                    ++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")"))
   648             >> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => Binary (c,e))
   649       
   650 
   651  val parastep = (a (Word "Para")) ++ (a (Other "(")) ++ (a (Other "(")) 
   652                    ++ term_numstep  ++ (a (Other ")")) ++ (a (Other ","))
   653                    ++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")"))
   654             >> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => Para(c, e))
   655       
   656  val mrrstep = (a (Word "MRR")) ++ (a (Other "(")) ++ (a (Other "(")) 
   657                    ++ term_numstep  ++ (a (Other ")")) ++ (a (Other ","))
   658                    ++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")"))
   659             >> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => MRR(c, e))
   660       
   661 
   662  val factorstep = (a (Word "Factor")) ++ (a (Other "("))
   663                     ++ number ++ (a (Other ","))
   664                        ++ number ++ (a (Other ","))
   665                        ++ number ++  (a (Other ")"))
   666                    
   667             >> (fn (_, (_, (c, (_, (e,(_,(f,_))))))) =>  Factor (c,e,f))
   668 
   669 
   670 (*val rewritestep = (a (Word "Rewrite"))  ++ (a (Other "(")) ++ (a (Other "(")) 
   671                    ++ term_numstep  ++ (a (Other ")")) ++ (a (Other ","))
   672                    ++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")"))
   673             >> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => Rewrite (c,e))*)
   674 
   675 val obviousstep = (a (Word "Obvious")) ++ (a (Other "(")) 
   676                    ++ term_numstep  ++ (a (Other ")")) 
   677             >> (fn (_, (_, (c,_))) => Obvious (c))
   678 
   679  val methodstep = extraaxiomstep || origaxiomstep || axiomstep ||binarystep || factorstep|| parastep || mrrstep || (*rewritestep ||*) obviousstep
   680 
   681 
   682  val number_list_step =
   683         ( number ++ many ((a (Other ",") ++ number)>> #2))
   684         >> (fn (a,b) => (a::b))
   685         
   686  val numberlist_step = a (Other "[")  ++ a (Other "]")
   687                         >>(fn (_,_) => ([]:int list))
   688                        || a (Other "[") ++ number_list_step ++ a (Other "]")
   689                         >>(fn (_,(a,_)) => a)
   690                     
   691 
   692 
   693 (** change this to allow P (x U) *)
   694  fun arglist_step input = ( word ++ many  word >> (fn (a, b) => (a^" "^(implode_with_space b)))
   695                            ||word >> (fn (a) => (a)))input
   696                 
   697 
   698 fun literal_step input = (word ++ a (Other "(") ++ arglist_step ++  a (Other ")")
   699                                           >>(fn (a, (b, (c,d))) => (a^" ("^(c)^")"))
   700                         || arglist_step >> (fn (a) => (a)))input
   701                            
   702 
   703 
   704 (* fun term_step input = (a (Other "~") ++ arglist_step ++ a (Other "%")>> (fn (a,(b,c)) => ("~ "^b))
   705                      ||  arglist_step ++ a (Other "%")>> (fn (a,b) => a ))input
   706 *)
   707 
   708 
   709  fun term_step input = (a (Other "~") ++ literal_step ++ a (Other "%")>> (fn (a,(b,c)) => ("~ "^b))
   710                      ||  literal_step ++ a (Other "%")>> (fn (a,b) => a ))input
   711 
   712 
   713          
   714 
   715  val term_list_step =
   716         (  term_step ++ many ( term_step))
   717         >> (fn (a,b) => (a::b))
   718         
   719  
   720 val term_lists_step = a (Other "[")  ++ a (Other "]")
   721                         >>(fn (_,_) => ([]:string list))
   722                        || a (Other "[") ++ term_list_step ++ a (Other "]")
   723                         >>(fn (_,(a,_)) => a)
   724                      
   725 
   726 
   727 
   728 fun anytoken_step input  = (word>> (fn (a) => a)  ) input
   729                        handle NOPARSE_WORD => (number>> (fn (a) => string_of_int a)  ) input
   730                       handle NOPARSE_NUMBER => (other_char >> (fn(a) => a)) input
   731 
   732 
   733 
   734 fun goalstring_step input= (anytoken_step ++ many (anytoken_step )
   735                   >> (fn (a,b) =>  (a^" "^(implode b)))) input
   736 
   737 
   738 
   739  val linestep = number ++ methodstep ++ term_lists_step ++ term_lists_step
   740                 >> (fn (a, (b, (c,d))) => (a,(b,c,d)))
   741     
   742  val lines_step = many linestep
   743 
   744  val alllines_step = (term_lists_step ++ lines_step ) ++ finished >> #1
   745     
   746  val parse_step = #1 o alllines_step
   747 
   748 
   749  (*
   750 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)"
   751 *)
   752 
   753 (************************************************************)
   754 (* Construct an Isar style proof from a list of proof steps *)
   755 (************************************************************)
   756 (* want to assume all axioms, then do haves for the other clauses*)
   757 (* then show for the last step *)
   758 
   759 (* replace ~ by not here *)
   760 fun change_nots [] = []
   761 |   change_nots (x::xs) = if x = "~" 
   762                           then 
   763                              ["\\", "<", "n", "o", "t", ">"]@(change_nots xs)
   764                           else (x::(change_nots xs))
   765 
   766 (*
   767 fun clstrs_to_string [] str = str
   768 |   clstrs_to_string (x::[]) str = str^x
   769 |   clstrs_to_string (x::xs) str = clstrs_to_string xs (str^(x^"; "))
   770 *)
   771 fun clstrs_to_string [] str = implode (change_nots (explode str))
   772 |   clstrs_to_string (x::[]) str = implode (change_nots (explode (str^x)))
   773 |   clstrs_to_string (x::xs) str = implode (change_nots (explode (clstrs_to_string xs (str^(x^"; ")))))
   774 
   775 
   776 
   777 fun thmvars_to_quantstring [] str = str
   778 |   thmvars_to_quantstring (x::[]) str =str^x^". "
   779 |   thmvars_to_quantstring (x::xs) str = thmvars_to_quantstring xs (str^(x^" "))
   780 
   781 
   782 fun clause_strs_to_isar clstrs [] =  "\"\\<lbrakk>"^(clstrs_to_string clstrs "")^"\\<rbrakk> \\<Longrightarrow> False\""
   783 |   clause_strs_to_isar clstrs thmvars = "\"\\<And>"^(thmvars_to_quantstring thmvars "")^"\\<lbrakk>"^(clstrs_to_string clstrs "")^"\\<rbrakk> \\<Longrightarrow> False\""
   784 
   785 fun frees_to_string [] str = implode (change_nots (explode str))
   786 |   frees_to_string (x::[]) str = implode (change_nots (explode (str^x)))
   787 |   frees_to_string  (x::xs) str = implode (change_nots (explode (frees_to_string xs (str^(x^" ")))))
   788 
   789 fun frees_to_isar_str [] =  ""
   790 |   frees_to_isar_str  clstrs = (frees_to_string clstrs "")
   791 
   792 
   793 (***********************************************************************)
   794 (* functions for producing assumptions for the Isabelle ordered axioms *)
   795 (***********************************************************************)
   796 (*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))[][]";       
   797 num, rule, clausestrs, vars*)
   798 
   799 
   800 (* assume the extra clauses - not used in Spass proof *)
   801 
   802 fun is_extraaxiom_step ( num:int,(ExtraAxiom, str, tstr)) = true
   803 |   is_extraaxiom_step (num, _) = false
   804 
   805 fun get_extraaxioms xs = List.filter (is_extraaxiom_step) ( xs)
   806 
   807 fun assume_isar_extraaxiom [] str  = str
   808 |   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 " )
   809 
   810 
   811 
   812 fun assume_isar_extraaxioms  [] = ""
   813 |assume_isar_extraaxioms ((numb,(step, clstrs, thmstrs))::xs) = let val str = "assume cl"^(string_of_int numb)^"': "^(clause_strs_to_isar clstrs thmstrs)^"\n" 
   814                                          in
   815                                              assume_isar_extraaxiom xs str
   816                                          end
   817 
   818 (* assume the Isabelle ordered clauses *)
   819 
   820 fun is_origaxiom_step ( num:int,(OrigAxiom, str, tstr)) = true
   821 |   is_origaxiom_step (num, _) = false
   822 
   823 fun get_origaxioms xs = List.filter (is_origaxiom_step) ( xs)
   824 
   825 fun assume_isar_origaxiom [] str  = str
   826 |   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 " )
   827 
   828 
   829 
   830 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" 
   831                                          in
   832                                              assume_isar_origaxiom xs str
   833                                          end
   834 
   835 
   836 
   837 fun is_axiom_step ( num:int,(Axiom, str, tstr)) = true
   838 |   is_axiom_step (num, _) = false
   839 
   840 fun get_axioms xs = List.filter  (is_axiom_step) ( xs)
   841 
   842 fun have_isar_axiomline (numb,(step, clstrs, thmstrs))="have cl"^(string_of_int numb)^": "^(clause_strs_to_isar clstrs thmstrs)^"\n"
   843 
   844 fun  by_isar_axiomline (numb,(step, clstrs, thmstrs))="by (rule cl"^ (string_of_int numb)^"') \n"
   845 
   846 
   847 fun isar_axiomline (numb, (step, clstrs, thmstrs))  = (have_isar_axiomline (numb,(step,clstrs, thmstrs )))^( by_isar_axiomline(numb,(step,clstrs, thmstrs )) )
   848 
   849 
   850 fun isar_axiomlines [] str = str
   851 |   isar_axiomlines (x::xs) str = isar_axiomlines xs (str^(isar_axiomline x))
   852 
   853 
   854 fun have_isar_line (numb,(step, clstrs, thmstrs))="have cl"^(string_of_int numb)^": "^(clause_strs_to_isar clstrs thmstrs)^"\n"
   855 (*FIX: ask Larry to add and mrr attribute *)
   856 
   857 fun by_isar_line ((Binary ((a,b), (c,d)))) = 
   858     "by(rule cl"^
   859 		(string_of_int a)^" [binary "^(string_of_int b)^" cl"^
   860 		(string_of_int c)^" "^(string_of_int d)^"])\n"
   861 |by_isar_line ((MRR ((a,b), (c,d)))) = 
   862     "by(rule cl"^
   863 		(string_of_int a)^" [binary "^(string_of_int b)^" cl"^
   864 		(string_of_int c)^" "^(string_of_int d)^"])\n"
   865 |   by_isar_line ( (Para ((a,b), (c,d)))) =
   866     "by (rule cl"^
   867 		(string_of_int a)^" [paramod "^(string_of_int b)^" cl"^
   868 		(string_of_int c)^" "^(string_of_int d)^"])\n"
   869 |   by_isar_line ((Factor ((a,b,c)))) = 
   870     "by (rule cl"^(string_of_int a)^" [factor "^(string_of_int b)^" "^
   871 		(string_of_int c)^" ])\n"
   872 (*|   by_isar_line ( (Rewrite ((a,b),(c,d)))) =
   873     "by (rule cl"^(string_of_int a)^" [demod "^(string_of_int b)^" "^
   874 		(string_of_int c)^" "^(string_of_int d)^" ])\n"*)
   875 |   by_isar_line ( (Obvious ((a,b)))) =
   876     "by (rule cl"^(string_of_int a)^" [obvious "^(string_of_int b)^" ])\n"
   877 
   878 fun isar_line (numb, (step, clstrs, thmstrs))  = (have_isar_line (numb,(step,clstrs, thmstrs )))^( by_isar_line step)
   879 
   880 
   881 fun isar_lines [] str = str
   882 |   isar_lines (x::xs) str = isar_lines xs (str^(isar_line x))
   883 
   884 fun last_isar_line (numb,( step, clstrs,thmstrs)) = "show \"False\"\n"^(by_isar_line step)
   885 
   886 
   887 fun to_isar_proof (frees, xs, goalstring) =
   888     let val extraaxioms = get_extraaxioms xs
   889 	val extraax_num = length extraaxioms
   890 	val origaxioms_and_steps = Library.drop (extraax_num, xs)  
   891 	
   892 	val origaxioms = get_origaxioms origaxioms_and_steps
   893 	val origax_num = length origaxioms
   894 	val axioms_and_steps = Library.drop (origax_num + extraax_num, xs)  
   895 	val axioms = get_axioms axioms_and_steps
   896 	
   897 	val steps = Library.drop (origax_num, axioms_and_steps)
   898 	val firststeps = ReconOrderClauses.butlast steps
   899 	val laststep = ReconOrderClauses.last steps
   900 	val goalstring = implode(ReconOrderClauses.butlast(explode goalstring))
   901 	
   902 	val isar_proof = 
   903 		("show \""^goalstring^"\"\n")^
   904 		("proof (rule ccontr,skolemize, make_clauses) \n")^
   905 		("fix "^(frees_to_isar_str frees)^"\n")^
   906 		(assume_isar_extraaxioms extraaxioms)^
   907 		(assume_isar_origaxioms origaxioms)^
   908 		(isar_axiomlines axioms "")^
   909 		(isar_lines firststeps "")^
   910 		(last_isar_line laststep)^
   911 		("qed")
   912 	val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "isar_proof_file")));
   913 	
   914 	val _ = TextIO.output (outfile, isar_proof)
   915 	val _ =  TextIO.closeOut outfile
   916     in
   917 	isar_proof
   918     end;
   919 
   920 (* get fix vars from axioms - all Frees *)
   921 (* check each clause for meta-vars and /\ over them at each step*)
   922 
   923 (*******************************************************)
   924 (* This assumes the thm list  "numcls" is still there  *)
   925 (* In reality, should probably label it with an        *)
   926 (* ID number identifying the subgoal.  This could      *)
   927 (* be passed over to the watcher, e.g.  numcls25       *)
   928 (*******************************************************)
   929 
   930 (* 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))[][]";
   931 
   932 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))[][]";
   933 
   934 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)";
   935 
   936 
   937 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))[][]";
   938 
   939 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)))";
   940 *)
   941 
   942 fun apply_res_thm str goalstring  = let val tokens = #1 (lex str);
   943 				val _ = File.append (File.tmp_path (Path.basic "applyres")) 
   944 			           ("str is: "^str^" goalstr is: "^goalstring^"\n")	
   945                                    val (frees,recon_steps) = parse_step tokens 
   946                                    val isar_str = to_isar_proof (frees, recon_steps, goalstring)
   947                                    val foo =   TextIO.openOut (File.platform_path(File.tmp_path (Path.basic "foobar")));
   948                                in 
   949                                   TextIO.output(foo,(isar_str));TextIO.closeOut foo;Pretty.writeln(Pretty.str  isar_str); () 
   950                                end 
   951 
   952 
   953 (* val reconstr = reconstr^"[P%]51Axiom()[~P%]52Axiom[P%][]53MRR((52,0),(51,0))[][]";
   954 *)
   955 end;