Removed remaining references to Main.thy in reconstruction code.
authorquigley
Wed Apr 20 16:03:17 2005 +0200 (2005-04-20)
changeset 15779aed221aff642
parent 15778 98af3693f6b3
child 15780 6744bba5561d
Removed remaining references to Main.thy in reconstruction code.
bin/isabelle-process
build
etc/settings
lib/Tools/dimacs2hol
lib/Tools/latex
lib/Tools/mkdir
src/HOL/IsaMakefile
src/HOL/Tools/meson.ML
src/HOL/Tools/res_atp.ML
src/Pure/mk
     1.1 --- a/bin/isabelle-process	Wed Apr 20 14:18:33 2005 +0200
     1.2 +++ b/bin/isabelle-process	Wed Apr 20 16:03:17 2005 +0200
     1.3 @@ -1,7 +1,10 @@
     1.4  #!/usr/bin/env bash
     1.5  #
     1.6 +
     1.7  # $Id$
     1.8 +
     1.9  # Author: Markus Wenzel, TU Muenchen
    1.10 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
    1.11  #
    1.12  # Isabelle process startup script.
    1.13  
    1.14 @@ -30,7 +33,6 @@
    1.15    echo "    -C           tell ML system to copy output image"
    1.16    echo "    -I           startup Isar interaction mode"
    1.17    echo "    -P           startup Proof General interaction mode"
    1.18 -  echo "    -X           startup PGIP interaction mode"
    1.19    echo "    -c           tell ML system to compress output image"
    1.20    echo "    -e MLTEXT    pass MLTEXT to the ML session"
    1.21    echo "    -f           pass 'Session.finish();' to the ML session"
    1.22 @@ -69,7 +71,7 @@
    1.23  READONLY=""
    1.24  NOWRITE=""
    1.25  
    1.26 -while getopts "XCIPce:fm:qruw" OPT
    1.27 +while getopts "CIPce:fm:qruw" OPT
    1.28  do
    1.29    case "$OPT" in
    1.30      C)
    1.31 @@ -81,9 +83,6 @@
    1.32      P)
    1.33        PROOFGENERAL=true
    1.34        ;;
    1.35 -    X)
    1.36 -      PGIP=true
    1.37 -      ;;
    1.38      c)
    1.39        COMPRESS=true
    1.40        ;;
    1.41 @@ -209,9 +208,7 @@
    1.42  
    1.43  [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
    1.44  
    1.45 -if [ -n "$PGIP" ]; then
    1.46 -  MLTEXT="$MLTEXT; ProofGeneral.init_pgip $ISAR;"
    1.47 -elif [ -n "$PROOFGENERAL" ]; then
    1.48 +if [ -n "$PROOFGENERAL" ]; then
    1.49    MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
    1.50  elif [ "$ISAR" = true ]; then
    1.51    MLTEXT="$MLTEXT; Isar.main();"
     2.1 --- a/build	Wed Apr 20 14:18:33 2005 +0200
     2.2 +++ b/build	Wed Apr 20 16:03:17 2005 +0200
     2.3 @@ -112,6 +112,8 @@
     2.4    echo "  ML_HOME=$ML_HOME"
     2.5    echo "  ML_OPTIONS=$ML_OPTIONS"
     2.6    echo "  ML_PLATFORM=$ML_PLATFORM"
     2.7 +  echo "  ISABELLE_INTERFACE=$ISABELLE_INTERFACE"
     2.8 +  echo "ISABELLE_OUTPUT=$ISABELLE_OUTPUT"
     2.9    echo
    2.10    echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
    2.11  fi
    2.12 @@ -154,6 +156,7 @@
    2.13    echo "ML_HOME=$ML_HOME"
    2.14    echo "ML_OPTIONS=$ML_OPTIONS"
    2.15    echo "ML_PLATFORM=$ML_PLATFORM"
    2.16 +  echo "ISABELLE_OUTPUT=$ISABELLE_OUTPUT"
    2.17    echo
    2.18    echo "ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
    2.19    echo
     3.1 --- a/etc/settings	Wed Apr 20 14:18:33 2005 +0200
     3.2 +++ b/etc/settings	Wed Apr 20 16:03:17 2005 +0200
     3.3 @@ -120,14 +120,14 @@
     3.4  ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
     3.5  
     3.6  # Heap output location. ML system identifier is appended automatically later on.
     3.7 -if [ "$THIS_IS_ISABELLE_BUILD" = true ]; then
     3.8 -  #Isabelle build tells us to store heaps etc. within the distribution.
     3.9 -  ISABELLE_OUTPUT="$ISABELLE_HOME/heaps"
    3.10 -  ISABELLE_BROWSER_INFO="$ISABELLE_HOME/browser_info"
    3.11 -else
    3.12 +#if [ "$THIS_IS_ISABELLE_BUILD" = true ]; then
    3.13 +#  Isabelle build tells us to store heaps etc. within the distribution.
    3.14 + # ISABELLE_OUTPUT="$ISABELLE_HOME/heaps"
    3.15 + # ISABELLE_BROWSER_INFO="$ISABELLE_HOME/browser_info"
    3.16 +#else
    3.17    ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
    3.18    ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
    3.19 -fi
    3.20 +#fi
    3.21  
    3.22  # Site settings check -- just to make it a little bit harder to copy this file!
    3.23  [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \
    3.24 @@ -181,7 +181,8 @@
    3.25  ISAMODE_OPTIONS=""
    3.26  
    3.27  # Proof General path, look in a variety of places
    3.28 -ISABELLE_INTERFACE=$(choosefrom \
    3.29 +ISABELLE_INTERFACE=$(choosefrom\
    3.30 +  "/homes/clq20/IsabelleCVS/isabelle/ProofGeneral/isar/interface"\
    3.31    "$ISABELLE_HOME/contrib/ProofGeneral/isar/interface" \
    3.32    "$ISABELLE_HOME/../ProofGeneral/isar/interface" \
    3.33    "/usr/share/ProofGeneral/isar/interface" \
     4.1 --- a/lib/Tools/dimacs2hol	Wed Apr 20 14:18:33 2005 +0200
     4.2 +++ b/lib/Tools/dimacs2hol	Wed Apr 20 16:03:17 2005 +0200
     4.3 @@ -46,6 +46,6 @@
     4.4  ## main
     4.5  
     4.6  #set by configure
     4.7 -AUTO_PERL=perl
     4.8 +AUTO_PERL=/usr/bin/perl
     4.9  
    4.10  "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/dimacs2hol.pl" "$@"
     5.1 --- a/lib/Tools/latex	Wed Apr 20 14:18:33 2005 +0200
     5.2 +++ b/lib/Tools/latex	Wed Apr 20 16:03:17 2005 +0200
     5.3 @@ -73,7 +73,7 @@
     5.4  # operations
     5.5  
     5.6  #set by configure
     5.7 -AUTO_PERL=perl
     5.8 +AUTO_PERL=/usr/bin/perl
     5.9  
    5.10  function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
    5.11  function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
     6.1 --- a/lib/Tools/mkdir	Wed Apr 20 14:18:33 2005 +0200
     6.2 +++ b/lib/Tools/mkdir	Wed Apr 20 16:03:17 2005 +0200
     6.3 @@ -1,3 +1,4 @@
     6.4 +
     6.5  #!/usr/bin/env bash
     6.6  #
     6.7  # $Id$
     6.8 @@ -285,4 +286,3 @@
     6.9  
    6.10  EOF
    6.11  fi
    6.12 -
     7.1 --- a/src/HOL/IsaMakefile	Wed Apr 20 14:18:33 2005 +0200
     7.2 +++ b/src/HOL/IsaMakefile	Wed Apr 20 16:03:17 2005 +0200
     7.3 @@ -119,7 +119,7 @@
     7.4   Tools/ATP/recon_transfer_proof.ML Tools/ATP/res_clasimpset.ML \
     7.5   Tools/ATP/VampireCommunication.ML Tools/ATP/SpassCommunication.ML Tools/ATP/modUnix.ML  \
     7.6   Tools/ATP/watcher.sig Tools/ATP/watcher.ML   Tools/res_atp.ML\
     7.7 -  document/root.tex hologic.ML simpdata.ML thy_syntax.ML
     7.8 +  ##document/root.tex hologic.ML simpdata.ML thy_syntax.ML
     7.9  	@$(ISATOOL) usedir -b -g true $(HOL_PROOF_OBJECTS) $(OUT)/Pure HOL
    7.10  
    7.11  
     8.1 --- a/src/HOL/Tools/meson.ML	Wed Apr 20 14:18:33 2005 +0200
     8.2 +++ b/src/HOL/Tools/meson.ML	Wed Apr 20 16:03:17 2005 +0200
     8.3 @@ -451,11 +451,6 @@
     8.4    SUBGOAL
     8.5      (fn (prop,_) =>
     8.6       let val ts = Logic.strip_assums_hyp prop
     8.7 -         
     8.8 -         val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "skolem")))
     8.9 -         val _ = TextIO.output(outfile, "in skolemize_tac ");
    8.10 -         val _ = TextIO.flushOut outfile;
    8.11 -         val _ =  TextIO.closeOut outfile
    8.12       in EVERY1 
    8.13  	 [METAHYPS
    8.14  	    (fn hyps => (cut_facts_tac (map (skolemize o make_nnf) hyps) 1
     9.1 --- a/src/HOL/Tools/res_atp.ML	Wed Apr 20 14:18:33 2005 +0200
     9.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Apr 20 16:03:17 2005 +0200
     9.3 @@ -8,9 +8,12 @@
     9.4  (*Jia: changed: isar_atp now processes entire proof context.  fetch thms from delta simpset/claset*)
     9.5  (*Claire: changed: added actual watcher calls *)
     9.6  
     9.7 +
     9.8  signature RES_ATP = 
     9.9  sig
    9.10  val trace_res : bool ref
    9.11 +val subgoals: Thm.thm list
    9.12 +val traceflag : bool ref
    9.13  val axiom_file : Path.T
    9.14  val hyps_file : Path.T
    9.15  val isar_atp : ProofContext.context * Thm.thm -> unit
    9.16 @@ -25,8 +28,9 @@
    9.17  
    9.18  struct
    9.19  
    9.20 +val subgoals = [];
    9.21  
    9.22 -
    9.23 +val traceflag = ref true;
    9.24  (* used for debug *)
    9.25  val debug = ref false;
    9.26  
    9.27 @@ -141,7 +145,7 @@
    9.28  (*********************************************************************)
    9.29  
    9.30  fun call_resolve_tac sign thms sg_term (childin, childout,pid) n  = let
    9.31 -                             val thmstring = Meson.concat_with_and (map string_of_thm thms)
    9.32 +                             val thmstring = Meson.concat_with_and (map string_of_thm thms) 
    9.33                               val thm_no = length thms
    9.34                               val _ = warning ("number of thms is : "^(string_of_int thm_no))
    9.35                               val _ = warning ("thmstring in call_res is: "^thmstring)
    9.36 @@ -157,7 +161,7 @@
    9.37                               val clauses = make_clauses thms
    9.38                               val _ =( warning ("called make_clauses "))*)
    9.39                               (*val _ = tptp_inputs clauses prob_file*)
    9.40 -                             val thmstring = Meson.concat_with_and (map string_of_thm thms)
    9.41 +                             val thmstring = Meson.concat_with_and (map string_of_thm thms) 
    9.42                             
    9.43                               val goalstr = Sign.string_of_term sign sg_term 
    9.44                               val goalproofstring = proofstring goalstr
    9.45 @@ -169,6 +173,9 @@
    9.46                               val thmstr = implode no_returns
    9.47                              
    9.48                               val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)
    9.49 +                             val axfile = (File.sysify_path axiom_file)
    9.50 +                             val hypsfile = (File.sysify_path hyps_file)
    9.51 +                             val clasimpfile = (File.sysify_path clasimp_file)
    9.52                               val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "hellofile")))
    9.53                               val _ = TextIO.output(outfile, "prob file path is "^probfile^" thmstring is "^thmstr^" goalstring is "^goalstring);
    9.54                               val _ = TextIO.flushOut outfile;
    9.55 @@ -180,7 +187,7 @@
    9.56                              Watcher.callResProvers(childout,
    9.57                              [("spass",thmstr,goalstring,"/homes/clq20/bin/SPASS",  
    9.58                               "-FullRed=0%-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof", 
    9.59 -                             probfile)]);
    9.60 +                             clasimpfile, axfile, hypsfile, probfile)]);
    9.61  
    9.62                             (* with paramodulation *)
    9.63                             (*Watcher.callResProvers(childout,
    9.64 @@ -193,36 +200,14 @@
    9.65                             dummy_tac
    9.66                           end
    9.67  
    9.68 -(************************************************)
    9.69 -(* pass in subgoal as a term and watcher info   *)
    9.70 -(* process subgoal into skolemized, negated form*)
    9.71 -(* then call call_resolve_tac to send to ATP    *)
    9.72 -(************************************************)
    9.73 -(*
    9.74 -fun resolve_tac sg_term  (childin, childout,pid) = 
    9.75 -   let val _ = warning ("in resolve_tac ")
    9.76 -   in
    9.77 -   SELECT_GOAL
    9.78 -  (EVERY1 [rtac ccontr,atomize_tac,skolemize_tac,  METAHYPS(fn negs => (warning ("calling call_resolve_tac next ");dummy_tac (*call_resolve_tac negs sg_term (childin, childout,pid)*)))])
    9.79 -   end;
    9.80 -
    9.81 -*)
    9.82 -
    9.83 -
    9.84 -(* Need to replace call_atp_tac_tfrees with call res_provers as it's the dummy one *)
    9.85 -
    9.86  (**********************************************************)
    9.87  (* write out the current subgoal as a tptp file, probN,   *)
    9.88  (* then call dummy_tac - should be call_res_tac           *)
    9.89  (**********************************************************)
    9.90 -(* should call call_res_tac here, not resolve_tac *)
    9.91 -(* if we take tptpinputs out it gets into call_res_tac then falls over as usual after printing out goalstring. but if we leave it in it falls over here *)
    9.92  
    9.93 -(* dummy tac vs.  Doesn't call resolve_tac *)
    9.94  
    9.95  fun call_atp_tac_tfrees sign thms n tfrees sg_term (childin, childout,pid) = 
    9.96 -                                         ( warning("ths for tptp: " ^ 
    9.97 -                                                   Meson.concat_with_and (map string_of_thm thms));
    9.98 +                                         (
    9.99                                             warning("in call_atp_tac_tfrees");
   9.100                                             
   9.101                                             tptp_inputs_tfrees (make_clauses thms) n tfrees;
   9.102 @@ -235,16 +220,14 @@
   9.103      val _ = warning ("sg_term :" ^ (Sign.string_of_term sign sg_term))
   9.104     
   9.105     in
   9.106 +
   9.107  SELECT_GOAL
   9.108    (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
   9.109 -  METAHYPS(fn negs => (warning("calling  call_atp_tac_tfrees with negs"
   9.110 -                               ^ Meson.concat_with_and (map string_of_thm negs));
   9.111 -           call_atp_tac_tfrees sign negs n tfrees sg_term (childin, childout,pid) ))]) n st
   9.112 +  METAHYPS(fn negs => ( call_atp_tac_tfrees sign negs n tfrees sg_term (childin, childout,pid) ))]) n st
   9.113  end;
   9.114  
   9.115  
   9.116 -fun isar_atp_g tfrees sg_term (childin, childout, pid) n = 
   9.117 -                                        
   9.118 +fun isar_atp_g tfrees sg_term (childin, childout, pid) n =       
   9.119  ((warning("in isar_atp_g"));atp_tac_tfrees tfrees sg_term (childin, childout, pid) n);
   9.120  
   9.121  
   9.122 @@ -265,13 +248,15 @@
   9.123                              in   
   9.124                                   
   9.125                  		(warning("in isar_atp_goal'"));
   9.126 -                                (warning("thmstring in isar_atp_goal: "^thmstring));
   9.127 +                                (warning("thmstring in isar_atp_goal': "^thmstring));
   9.128   				 isar_atp_g tfree_lits  sg_term (childin, childout, pid) k thm; 
   9.129                                   isar_atp_goal' thm (k+1) n tfree_lits  (childin, childout, pid) 
   9.130                              end);
   9.131  
   9.132  
   9.133 -fun isar_atp_goal thm n_subgoals tfree_lits   (childin, childout, pid) = (if (!debug) then warning (string_of_thm thm) else (isar_atp_goal' thm 1 n_subgoals tfree_lits  (childin, childout, pid) ));
   9.134 +fun isar_atp_goal thm n_subgoals tfree_lits   (childin, childout, pid) = 
   9.135 +              (if (!debug) then warning (string_of_thm thm) 
   9.136 +               else (isar_atp_goal' thm 1 n_subgoals tfree_lits  (childin, childout, pid) ));
   9.137  
   9.138  (**************************************************)
   9.139  (* convert clauses from "assume" to conjecture.   *)
   9.140 @@ -285,7 +270,8 @@
   9.141  fun isar_atp_aux thms thm n_subgoals  (childin, childout, pid) = 
   9.142      let val tfree_lits = isar_atp_h thms 
   9.143      in
   9.144 -	(warning("in isar_atp_aux"));isar_atp_goal thm n_subgoals tfree_lits   (childin, childout, pid)
   9.145 +	(warning("in isar_atp_aux"));
   9.146 +         isar_atp_goal thm n_subgoals tfree_lits   (childin, childout, pid)
   9.147      end;
   9.148  
   9.149  (******************************************************************)
   9.150 @@ -294,20 +280,26 @@
   9.151  (* passes all subgoals on to isar_atp_aux for further processing  *)
   9.152  (* turns off xsymbol at start of function, restoring it at end    *)
   9.153  (******************************************************************)
   9.154 -
   9.155 +(*FIX changed to clasimp_file *)
   9.156  fun isar_atp' (thms, thm) =
   9.157      let val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
   9.158          val _= (warning ("in isar_atp'"))
   9.159 -        val prems = prems_of thm
   9.160 +        val prems  = prems_of thm
   9.161          val sign = sign_of_thm thm
   9.162 -        val thms_string = Meson.concat_with_and (map string_of_thm thms)
   9.163 +        val thms_string = Meson.concat_with_and (map string_of_thm thms) 
   9.164          val thmstring = string_of_thm thm
   9.165 -        val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems)
   9.166 +        val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   9.167          (* set up variables for writing out the clasimps to a tptp file *)
   9.168 -        val _ = write_out_clasimp (File.sysify_path axiom_file)
   9.169 +
   9.170 +        (* val clause_arr = write_out_clasimp (File.sysify_path clasimp_file) clause_arr*)
   9.171 +        (*val _ = (warning ("clasimp_file is this: "^(File.sysify_path clasimp_file)) )  *)
   9.172          (* cq: add write out clasimps to file *)
   9.173 -        (* cq:create watcher and pass to isar_atp_aux *)                    
   9.174 -        val (childin,childout,pid) = Watcher.createWatcher()
   9.175 +        (* cq:create watcher and pass to isar_atp_aux *) 
   9.176 +        (*val tenth_ax = fst( Array.sub(clause_arr, 10))  
   9.177 +        val _ = (warning ("tenth axiom in array is: "^tenth_ax))         
   9.178 +        val _ = (warning ("num_of_clauses is: "^(string_of_int (!num_of_clauses))) )  *)      
   9.179 +                               
   9.180 +        val (childin,childout,pid) = Watcher.createWatcher(thm)
   9.181          val pidstring = string_of_int(Word.toInt (Word.fromLargeWord ( Posix.Process.pidToWord pid )))
   9.182      in
   9.183  	case prems of [] => () 
   9.184 @@ -367,6 +359,7 @@
   9.185  (* what about clasimpset - it should already be in the ax file - perhaps append to ax file rather than just *)
   9.186  (* write out ? Or keep as a separate file and then cat them all together in the watcher, like we do with the *)
   9.187  (*claset file and prob file*)
   9.188 +(* FIX*)
   9.189  fun isar_local_thms (delta_cs, delta_ss_thms) =
   9.190      let val thms_cs = get_thms_cs delta_cs
   9.191  	val thms_ss = get_thms_ss delta_ss_thms
   9.192 @@ -392,11 +385,11 @@
   9.193          val sg_prems = prems_of thm
   9.194          val sign = sign_of_thm thm
   9.195          val prem_no = length sg_prems
   9.196 -        val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) sg_prems)
   9.197 +        val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) sg_prems) 
   9.198      in
   9.199            (warning ("initial thm in isar_atp: "^thmstring));
   9.200            (warning ("subgoals in isar_atp: "^prems_string));
   9.201 -    	   (warning ("number of subgoals in isar_atp: "^(string_of_int prem_no)));
   9.202 +    	  (warning ("number of subgoals in isar_atp: "^(string_of_int prem_no)));
   9.203            (isar_local_thms (d_cs,d_ss_thms); (warning("about to call isar_atp'"));
   9.204             isar_atp' (prems, thm))
   9.205      end;
    10.1 --- a/src/Pure/mk	Wed Apr 20 14:18:33 2005 +0200
    10.2 +++ b/src/Pure/mk	Wed Apr 20 16:03:17 2005 +0200
    10.3 @@ -87,6 +87,9 @@
    10.4  if [ -z "$RAW" ]; then
    10.5    ITEM="Pure"
    10.6    echo "Building $ITEM ..."
    10.7 +
    10.8 +  echo "raw is $RAW item is $ITEM isabelle is $ISABELLE"
    10.9 +
   10.10    LOG="$LOGDIR/$ITEM"
   10.11  
   10.12    "$ISABELLE" $COPY \