yet more tidying of Isabelle-ATP link
authorpaulson
Thu Sep 08 13:24:19 2005 +0200 (2005-09-08)
changeset 17312159783c74f75
parent 17311 5b1d47d920ce
child 17313 7d97f60293ae
yet more tidying of Isabelle-ATP link
src/HOL/Tools/ATP/VampCommunication.ML
src/HOL/Tools/ATP/recon_order_clauses.ML
src/HOL/Tools/ATP/recon_parse.ML
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/ATP/recon_translate_proof.ML
src/HOL/Tools/res_clause.ML
     1.1 --- a/src/HOL/Tools/ATP/VampCommunication.ML	Wed Sep 07 21:07:09 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/VampCommunication.ML	Thu Sep 08 13:24:19 2005 +0200
     1.3 @@ -33,7 +33,7 @@
     1.4          [rtac ccontr, ResLib.atomize_tac, skolemize_tac,
     1.5  	 METAHYPS(fn negs =>
     1.6  		     (Recon_Transfer.vampString_to_lemmaString proofextract thmstring 
     1.7 -		       goalstring toParent ppid negs clause_arr  num_of_clauses ))]) sg_num
     1.8 +		       goalstring toParent ppid negs clause_arr num_of_clauses))]) sg_num
     1.9  
    1.10  
    1.11  fun transferVampInput (fromChild, toParent, ppid,thmstring,goalstring, 
     2.1 --- a/src/HOL/Tools/ATP/recon_order_clauses.ML	Wed Sep 07 21:07:09 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/recon_order_clauses.ML	Thu Sep 08 13:24:19 2005 +0200
     2.3 @@ -23,8 +23,6 @@
     2.4  fun numlist 0 = []
     2.5  |   numlist n = (numlist (n - 1))@[n]
     2.6  
     2.7 -
     2.8 -fun last(x::xs) = if xs=[] then x else last xs
     2.9  fun butlast []= []
    2.10  |   butlast(x::xs) = if xs=[] then [] else (x::(butlast xs))
    2.11  
    2.12 @@ -44,7 +42,7 @@
    2.13  fun contains_eq str = "=" mem str 
    2.14  
    2.15  fun eq_not_neq str = let val uptoeq = fst(takeUntil "=" str [])
    2.16 -                     in (last uptoeq) <> "~" end
    2.17 +                     in (List.last uptoeq) <> "~" end
    2.18                     
    2.19  fun get_eq_strs str =  if eq_not_neq  str   (*not an inequality *)
    2.20                         then 
     3.1 --- a/src/HOL/Tools/ATP/recon_parse.ML	Wed Sep 07 21:07:09 2005 +0200
     3.2 +++ b/src/HOL/Tools/ATP/recon_parse.ML	Thu Sep 08 13:24:19 2005 +0200
     3.3 @@ -25,8 +25,6 @@
     3.4  (* Parser combinators *)
     3.5  
     3.6  exception Noparse;
     3.7 -exception VampError of string;
     3.8 -
     3.9  
    3.10  fun (parser1 ++ parser2) input =
    3.11        let
    3.12 @@ -158,53 +156,18 @@
    3.13       fun lex s =  alltokens  (explode s)
    3.14  
    3.15  
    3.16 -(*********************************************************)
    3.17 -(*  Temporary code to "parse" Vampire proofs             *)
    3.18 -(*********************************************************)
    3.19  
    3.20 -fun num_int (Number n) = n
    3.21 -|   num_int _ = raise VampError "Not a number"
    3.22 -
    3.23 - fun takeUntil ch [] res  = (res, [])
    3.24 - |   takeUntil ch (x::xs) res = if   x = ch 
    3.25 -                                then
    3.26 -                                     (res, xs)
    3.27 -                                else
    3.28 -                                     takeUntil ch xs (res@[x])
    3.29 -       
    3.30 -fun linenums [] nums = nums
    3.31 -|   linenums (x::xs) nums = let val (fst, rest ) = takeUntil (Other "%") (x::xs) []
    3.32 -                                in 
    3.33 -				  if rest = [] 
    3.34 -				  then 
    3.35 -				      nums
    3.36 -				  else
    3.37 -			          let val first = hd rest
    3.38 -				
    3.39 -			          in
    3.40 -				    if (first = (Other "*") ) 
    3.41 -				    then 
    3.42 -					
    3.43 -					 linenums rest ((num_int (hd (tl rest)))::nums)
    3.44 -				     else
    3.45 -					  linenums rest ((num_int first)::nums)
    3.46 -			         end
    3.47 -                                end
    3.48 +(*String contains multiple lines, terminated with newline characters.
    3.49 +  A list consisting of the first number in each line is returned. *)
    3.50 +fun get_linenums proofstr = 
    3.51 +  let val numerics = String.tokens (not o Char.isDigit)
    3.52 +      fun firstno [] = NONE
    3.53 +        | firstno (x::xs) = Int.fromString x
    3.54 +      val lines = String.tokens (fn c => c = #"\n") proofstr
    3.55 +  in  List.mapPartial (firstno o numerics) lines  end
    3.56  
    3.57  
    3.58 -(* This relies on a Vampire proof line starting "% Number" or "% * Number"*)
    3.59 -(* Check this is right *)
    3.60 -
    3.61 -fun get_linenums proofstr = let (*val s = extract_proof proofstr*)
    3.62 -                                val tokens = #1(lex proofstr)
    3.63 -	                 
    3.64 -	                    in
    3.65 -		                rev (linenums tokens [])
    3.66 -		            end
    3.67 -
    3.68  (************************************************************)
    3.69 -(************************************************************)
    3.70 -
    3.71  
    3.72  (**************************************************)
    3.73  (* Code to parse SPASS proofs                     *)
     4.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Sep 07 21:07:09 2005 +0200
     4.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Sep 08 13:24:19 2005 +0200
     4.3 @@ -3,10 +3,6 @@
     4.4      Copyright   2004  University of Cambridge
     4.5  *)
     4.6  
     4.7 -(******************)
     4.8 -(* complete later *)
     4.9 -(******************)
    4.10 -
    4.11  structure Recon_Transfer =
    4.12  struct
    4.13  
    4.14 @@ -104,10 +100,8 @@
    4.15  	  extraAxs_to_string xs (str^newstr)
    4.16        end;
    4.17  
    4.18 -fun is_axiom ( num:int,Axiom, str) = true
    4.19 -|   is_axiom (num, _,_) = false
    4.20 -
    4.21 -fun get_init_axioms xs = List.filter (is_axiom) ( xs)
    4.22 +fun is_axiom (_,Axiom,str) = true
    4.23 +|   is_axiom (_,_,_) = false
    4.24  
    4.25  fun get_step_nums [] nums = nums
    4.26  |   get_step_nums (( num:int,Axiom, str)::xs) nums = get_step_nums xs (nums@[num])
    4.27 @@ -159,23 +153,22 @@
    4.28  
    4.29  (* retrieve the axioms that were obtained from the clasimpset *)
    4.30  
    4.31 -fun get_clasimp_cls clause_arr clasimp_num step_nums = 
    4.32 +fun get_clasimp_cls (clause_arr: (ResClause.clause * thm) array) clasimp_num step_nums = 
    4.33      let val realnums = map subone step_nums	
    4.34  	val clasimp_nums = List.filter (is_clasimp_ax (clasimp_num - 1)) realnums
    4.35  (*	val axnums = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "axnums")))     
    4.36  	val _ = TextIO.output(axnums,(numstr clasimp_nums))
    4.37  	val _ = TextIO.closeOut(axnums)*)
    4.38      in
    4.39 -	retrieve_axioms clause_arr  clasimp_nums
    4.40 +	retrieve_axioms clause_arr clasimp_nums
    4.41      end
    4.42  
    4.43  
    4.44 -
    4.45  (*****************************************************)
    4.46  (* get names of clasimp axioms used                  *)
    4.47  (*****************************************************)
    4.48  
    4.49 - fun get_axiom_names step_nums thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses  =
    4.50 + fun get_axiom_names step_nums thms clause_arr num_of_clauses =
    4.51     let 
    4.52       (* not sure why this is necessary again, but seems to be *)
    4.53        val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    4.54 @@ -184,7 +177,7 @@
    4.55       (* here need to add the clauses from clause_arr*)
    4.56       (***********************************************)
    4.57    
    4.58 -      val (clasimp_names_cls) = get_clasimp_cls clause_arr num_of_clauses step_nums 
    4.59 +      val clasimp_names_cls = get_clasimp_cls clause_arr num_of_clauses step_nums 
    4.60        val clasimp_names = map (#1 o ResClause.clause_info o #1) clasimp_names_cls
    4.61    
    4.62        val _ = File.write (File.tmp_path (Path.basic "clasimp_names"))                                                               
    4.63 @@ -195,7 +188,7 @@
    4.64     end
    4.65     
    4.66   fun get_axiom_names_spass proof_steps thms clause_arr num_of_clauses  =
    4.67 -   get_axiom_names (get_step_nums (get_init_axioms proof_steps) []) 
    4.68 +   get_axiom_names (get_step_nums (List.filter is_axiom proof_steps) []) 
    4.69                         thms clause_arr num_of_clauses;
    4.70      
    4.71   fun get_axiom_names_vamp_E proofstr thms clause_arr num_of_clauses  =
    4.72 @@ -217,7 +210,7 @@
    4.73   fun get_axioms_used proof_steps thms clause_arr num_of_clauses  =
    4.74       let 
    4.75  	val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    4.76 -	val axioms = get_init_axioms proof_steps
    4.77 +	val axioms = (List.filter is_axiom) proof_steps
    4.78  	val step_nums = get_step_nums axioms []
    4.79  
    4.80  	val clauses =(*(clasimp_cls)@*)( make_clauses thms)
    4.81 @@ -322,9 +315,7 @@
    4.82    let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler"
    4.83    in 
    4.84       TextIO.output (toParent,"Proof found but parsing failed for resolution proof: "^(remove_linebreaks proofstr)^"\n" );
    4.85 -      TextIO.flushOut toParent;
    4.86         TextIO.output (toParent, (remove_linebreaks thmstring)^"\n");
    4.87 -       TextIO.flushOut toParent;
    4.88         TextIO.output (toParent, ( (remove_linebreaks goalstring)^"\n"));
    4.89         TextIO.flushOut toParent;
    4.90        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    4.91 @@ -343,11 +334,12 @@
    4.92      (* get vampire axiom names         *)
    4.93      (***********************************)
    4.94  
    4.95 -     val axiom_names = get_axiom_names_vamp_E proofstr  thms clause_arr  num_of_clauses
    4.96 +     val axiom_names = get_axiom_names_vamp_E proofstr thms clause_arr num_of_clauses
    4.97       val ax_str = "Rules from clasimpset used in proof found by Vampire: " ^
    4.98                    rules_to_string axiom_names
    4.99      in 
   4.100 -	 File.append(File.tmp_path (Path.basic "reconstrfile")) ("reconstring is: "^ax_str^"  "^goalstring);
   4.101 +	 File.append(File.tmp_path (Path.basic "reconstrfile")) 
   4.102 +	            ("reconstring is: "^ax_str^"  "^goalstring);
   4.103           TextIO.output (toParent, ax_str^"\n");
   4.104  	 TextIO.output (toParent, "goalstring: "^goalstring^"\n");
   4.105  	 TextIO.output (toParent, "thmstring: "^thmstring^"\n");
   4.106 @@ -383,9 +375,10 @@
   4.107       val ax_str = "Rules from clasimpset used in proof found by E: " ^
   4.108                    rules_to_string axiom_names
   4.109      in 
   4.110 -	 File.append(File.tmp_path (Path.basic "reconstrfile")) ("reconstring is: "^ax_str^"  "^goalstring);
   4.111 +	 File.append(File.tmp_path (Path.basic "reconstrfile"))
   4.112 +	            ("reconstring is: "^ax_str^"  "^goalstring);
   4.113           TextIO.output (toParent, ax_str^"\n");
   4.114 -	 TextIO.flushOut toParent;
   4.115 +	 TextIO.output (toParent, "goalstring: "^goalstring^"\n");
   4.116  	 TextIO.output (toParent, "thmstring: "^thmstring^"\n");
   4.117  	 TextIO.flushOut toParent;
   4.118  
   4.119 @@ -771,7 +764,7 @@
   4.120  	
   4.121  	val steps = Library.drop (origax_num, axioms_and_steps)
   4.122  	val firststeps = ReconOrderClauses.butlast steps
   4.123 -	val laststep = ReconOrderClauses.last steps
   4.124 +	val laststep = List.last steps
   4.125  	val goalstring = implode(ReconOrderClauses.butlast(explode goalstring))
   4.126  	
   4.127  	val isar_proof = 
     5.1 --- a/src/HOL/Tools/ATP/recon_translate_proof.ML	Wed Sep 07 21:07:09 2005 +0200
     5.2 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML	Thu Sep 08 13:24:19 2005 +0200
     5.3 @@ -259,25 +259,6 @@
     5.4     end
     5.5     handle Option => reconstruction_failed "follow_standard_para"
     5.6  
     5.7 -(*              
     5.8 -fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs= 
     5.9 -                          let 
    5.10 -                            val th1 =  valOf (assoc (thml,clause1))
    5.11 -                            val th2 =  valOf (assoc (thml,clause2)) 
    5.12 -                            val eq_lit_th = select_literal (lit1+1) th1
    5.13 -                            val mod_lit_th = select_literal (lit2+1) th2
    5.14 -                            val eqsubst = eq_lit_th RSN (2,rev_subst)
    5.15 -                            val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
    5.16 -			    val newth' =negate_nead newth 
    5.17 -                            val (res, numlist, symlist, nsymlist)  = (rearrange_clause newth' clause_strs allvars)
    5.18 -                            val thmvars = thm_vars res
    5.19 -                         in 
    5.20 -                           (res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars))
    5.21 -                         end
    5.22 -			 handle Option => reconstruction_failed "follow_standard_para"
    5.23 -
    5.24 -*)
    5.25 -
    5.26  
    5.27  (********************************)
    5.28  (* Reconstruct a rewriting step *)
    5.29 @@ -401,22 +382,6 @@
    5.30  (* follow through the res. proof, creating an Isabelle theorem *)
    5.31  (***************************************************************)
    5.32  
    5.33 -
    5.34 -
    5.35 -(*fun is_proof_char ch = (case ch of 
    5.36 -                       
    5.37 -                        "(" => true
    5.38 -                       |  ")" => true
    5.39 -                         | ":" => true
    5.40 -                        |  "'" => true
    5.41 -                        |  "&" => true
    5.42 -                        | "|" => true
    5.43 -                        | "~" => true
    5.44 -                        |  "." => true
    5.45 -                        |(is_alpha ) => true
    5.46 -                       |(is_digit) => true
    5.47 -                         | _ => false)*)
    5.48 -
    5.49  fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126)) orelse (ch = " ")
    5.50  
    5.51  fun proofstring x = let val exp = explode x 
    5.52 @@ -424,35 +389,6 @@
    5.53                          List.filter (is_proof_char ) exp
    5.54                      end
    5.55  
    5.56 -
    5.57 -(*
    5.58 -
    5.59 -fun follow clauses [] allvars thml recons = 
    5.60 -                             let (* val _ = reset show_sorts*)
    5.61 -                              val thmstring = Meson.concat_with_and (map string_of_thm (map snd thml))
    5.62 -                              val thmproofstring = proofstring ( thmstring)
    5.63 -                            val no_returns = no_lines thmproofstring
    5.64 -                            val thmstr = implode no_returns
    5.65 -                               val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "thml_file")))
    5.66 -                               val _ = TextIO.output(outfile, "thmstr is "^thmstr)
    5.67 -                               val _ = TextIO.flushOut outfile;
    5.68 -                               val _ =  TextIO.closeOut outfile
    5.69 -                                 (*val _ = set show_sorts*)
    5.70 -                             in
    5.71 -                                  ((snd( hd thml)), recons)
    5.72 -                             end
    5.73 -      | follow clauses (h::t) allvars thml recons 
    5.74 -        = let
    5.75 -            val (thml', recons') = follow_line clauses allvars  thml h recons
    5.76 -            val  (thm, recons_list) = follow clauses t  allvars thml' recons'
    5.77 -            
    5.78 -
    5.79 -          in
    5.80 -             (thm,recons_list)
    5.81 -          end
    5.82 -
    5.83 -*)
    5.84 -
    5.85  fun replace_clause_strs [] recons newrecons = (newrecons)
    5.86  |   replace_clause_strs ((thmnum, thm)::thml)    
    5.87                    ((clausenum,(step,clause_strs,thmvars))::recons) newrecons = 
    5.88 @@ -477,17 +413,11 @@
    5.89  	 (thm,recons_list)
    5.90        end
    5.91  
    5.92 -
    5.93 -
    5.94  (* Assume we have the cnf clauses as a list of (clauseno, clause) *)
    5.95   (* and the proof as a list of the proper datatype *)
    5.96  (* take the cnf clauses of the goal and the proof from the res. prover *)
    5.97  (* as a list of type Proofstep and return the thm goal ==> False *)
    5.98  
    5.99 -fun first_pair (a,b,c) = (a,b);
   5.100 -
   5.101 -fun second_pair (a,b,c) = (b,c);
   5.102 -
   5.103  (* takes original axioms, proof_steps parsed from spass, variables *)
   5.104  
   5.105  fun translate_proof clauses proof allvars
   5.106 @@ -496,10 +426,4 @@
   5.107               (thm, (recons))
   5.108            end
   5.109    
   5.110 -
   5.111 -
   5.112 -fun remove_tinfo [] = []
   5.113 -  | remove_tinfo ( (clausenum, step, T_info, newstrs)::xs) =
   5.114 -      (clausenum, step , newstrs)::(remove_tinfo xs)
   5.115 -
   5.116  end;
     6.1 --- a/src/HOL/Tools/res_clause.ML	Wed Sep 07 21:07:09 2005 +0200
     6.2 +++ b/src/HOL/Tools/res_clause.ML	Thu Sep 08 13:24:19 2005 +0200
     6.3 @@ -448,20 +448,9 @@
     6.4        (sorts_on_typs ((FOLTFree x), ss));
     6.5  
     6.6  
     6.7 -(*FIXME: duplicate code that needs removal??*)
     6.8 -
     6.9 -fun takeUntil ch [] res  = (res, [])
    6.10 - |   takeUntil ch (x::xs) res = if   x = ch 
    6.11 -                                then
    6.12 -                                     (res, xs)
    6.13 -                                else
    6.14 -                                     takeUntil ch xs (res@[x])
    6.15 -
    6.16 -fun remove_type str = let val exp = explode str
    6.17 -		 	  val (first,rest) =  (takeUntil "(" exp [])
    6.18 -                      in
    6.19 -                        implode first
    6.20 -		      end
    6.21 +(*UGLY: seems to be parsing the "show sorts" output, removing anything that
    6.22 +  starts with a left parenthesis.*)
    6.23 +fun remove_type str = hd (String.fields (fn c => c = #"(") str);
    6.24  
    6.25  fun pred_of_sort (LTVar x) = ((remove_type x),1)
    6.26  |   pred_of_sort (LTFree x) = ((remove_type x),1)
    6.27 @@ -487,22 +476,6 @@
    6.28  	  (vss, ResLib.no_rep_app fs fss,preds'')
    6.29        end;
    6.30  
    6.31 -
    6.32 -(*fun add_typs_aux [] = ([],[])
    6.33 -  | add_typs_aux ((FOLTVar indx,s)::tss) = 
    6.34 -      let val vs = sorts_on_typs (FOLTVar indx, s)
    6.35 -	  val (vss,fss) = add_typs_aux tss
    6.36 -      in
    6.37 -	  (ResLib.no_rep_app vs vss, fss)
    6.38 -      end
    6.39 -  | add_typs_aux ((FOLTFree x,s)::tss) =
    6.40 -      let val fs = sorts_on_typs (FOLTFree x, s)
    6.41 -	  val (vss,fss) = add_typs_aux tss
    6.42 -      in
    6.43 -	  (vss, ResLib.no_rep_app fs fss)
    6.44 -      end;*)
    6.45 -
    6.46 -
    6.47  fun add_typs (Clause cls) preds  = add_typs_aux (#types_sorts cls) preds 
    6.48  
    6.49