Integrating the reconstruction files into the building of HOL
authorquigley
Thu Apr 07 18:20:04 2005 +0200 (2005-04-07)
changeset 1567928eb0fe50533
parent 15678 28cc2314c7ff
child 15680 83164f078985
Integrating the reconstruction files into the building of HOL
src/HOL/Tools/meson.ML
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/meson.ML	Thu Apr 07 17:45:51 2005 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Thu Apr 07 18:20:04 2005 +0200
     1.3 @@ -86,6 +86,13 @@
     1.4  	| has _ = false
     1.5    in  has  end;
     1.6  
     1.7 +(* for tracing statements *)
     1.8 + 
     1.9 +fun concat_with_and [] str = str
    1.10 +|   concat_with_and (x::[]) str = str^" ("^x^")"
    1.11 +|   concat_with_and (x::xs) str = (concat_with_and xs (str^"("^x^")"^" & "))
    1.12 +
    1.13 +
    1.14  
    1.15  (**** Clause handling ****)
    1.16  
    1.17 @@ -124,7 +131,7 @@
    1.18  (*Conjunctive normal form, detecting tautologies early.
    1.19    Strips universal quantifiers and breaks up conjunctions. *)
    1.20  fun cnf_aux seen (th,ths) =
    1.21 - let val _= (warning ("in cnf_aux"))
    1.22 + let val _= (warning ("in cnf_aux, th : "^(string_of_thm th)))
    1.23   in if taut_lits (literals(prop_of th) @ seen)  
    1.24    then ths     (*tautology ignored*)
    1.25    else if not (has_consts ["All","op &"] (prop_of th))  
    1.26 @@ -310,8 +317,8 @@
    1.27  (*Pull existential quantifiers (Skolemization)*)
    1.28  fun skolemize th =
    1.29    if not (has_consts ["Ex"] (prop_of th)) then th
    1.30 -  else skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
    1.31 -                              disj_exD, disj_exD1, disj_exD2]))
    1.32 +  else ((warning("in meson.skolemize with th: "^(string_of_thm th)));skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
    1.33 +                              disj_exD, disj_exD1, disj_exD2])))
    1.34      handle THM _ =>
    1.35          skolemize (forward_res skolemize
    1.36                     (tryres (th, [conj_forward, disj_forward, all_forward])))
    1.37 @@ -321,7 +328,7 @@
    1.38  (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
    1.39    The resulting clauses are HOL disjunctions.*)
    1.40  fun make_clauses ths =
    1.41 -    sort_clauses (map (generalize o nodups) (foldr cnf [] ths));
    1.42 +   ( (warning("in make_clauses ths are:"^(concat_with_and (map string_of_thm ths) ""))); sort_clauses (map (generalize o nodups) (foldr cnf [] ths)));
    1.43  
    1.44  (*Convert a list of clauses to (contrapositive) Horn clauses*)
    1.45  fun make_horns ths =
    1.46 @@ -448,9 +455,14 @@
    1.47    SUBGOAL
    1.48      (fn (prop,_) =>
    1.49       let val ts = Logic.strip_assums_hyp prop
    1.50 +         val _ = (warning("in meson.skolemize_tac "))
    1.51 +         val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "skolem")))
    1.52 +         val _ = TextIO.output(outfile, "in skolemize_tac ");
    1.53 +         val _ = TextIO.flushOut outfile;
    1.54 +         val _ =  TextIO.closeOut outfile
    1.55       in EVERY1 
    1.56  	 [METAHYPS
    1.57 -	    (fn hyps => (cut_facts_tac (map (skolemize o make_nnf) hyps) 1
    1.58 +	    (fn hyps => ((warning("in meson.skolemize_tac hyps are: "^(string_of_thm (hd hyps))));cut_facts_tac (map (skolemize o make_nnf) hyps) 1
    1.59                           THEN REPEAT (etac exE 1))),
    1.60  	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
    1.61       end);
     2.1 --- a/src/HOL/Tools/res_atp.ML	Thu Apr 07 17:45:51 2005 +0200
     2.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Apr 07 18:20:04 2005 +0200
     2.3 @@ -8,6 +8,8 @@
     2.4  (*Jia: changed: isar_atp now processes entire proof context.  fetch thms from delta simpset/claset*)
     2.5  (*Claire: changed: added actual watcher calls *)
     2.6  
     2.7 +val traceflag = ref true;
     2.8 +
     2.9  signature RES_ATP = 
    2.10  sig
    2.11  val trace_res : bool ref
    2.12 @@ -175,7 +177,7 @@
    2.13                               val thmstr = implode no_returns
    2.14                              
    2.15                               val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)
    2.16 -                             val outfile = TextIO.openOut("/home/clq20/Jia_Code/hellofile")
    2.17 +                             val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "hellofile")))
    2.18                               val _ = TextIO.output(outfile, "prob file path is "^probfile^" thmstring is "^thmstr^" goalstring is "^goalstring);
    2.19                               val _ = TextIO.flushOut outfile;
    2.20                               val _ =  TextIO.closeOut outfile
    2.21 @@ -223,25 +225,45 @@
    2.22  (**********************************************************)
    2.23  (* should call call_res_tac here, not resolve_tac *)
    2.24  (* 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 *)
    2.25 -fun call_atp_tac_tfrees thms n tfrees sg_term (childin, childout,pid) = 
    2.26 +
    2.27 +(* dummy tac vs.  Doesn't call resolve_tac *)
    2.28  
    2.29 -                                         ( (warning("in call_atp_tac_tfrees"));
    2.30 +fun call_atp_tac_tfrees thms n tfrees sg_term (childin, childout,pid) = 
    2.31 +                                         ( (warning("ths for tptp: "^(concat_with_and (map string_of_thm thms) "")));
    2.32 +                                           (warning("in call_atp_tac_tfrees"));
    2.33 +                                           
    2.34                                             tptp_inputs_tfrees (make_clauses thms) n tfrees;
    2.35 -                                          call_resolve_tac thms sg_term (childin, childout, pid) n;
    2.36 -  					  dummy_tac);
    2.37 +                                           call_resolve_tac thms sg_term (childin, childout, pid) n;
    2.38 +  					   dummy_tac);
    2.39  
    2.40 +
    2.41 +(*
    2.42  fun atp_tac_tfrees tfrees sg_term (childin, childout,pid)  n  = 
    2.43  let val _ = (warning ("in atp_tac_tfrees "))
    2.44     in
    2.45 -SELECT_GOAL
    2.46 -  (EVERY1 [rtac ccontr,atomize_tac,(*skolemize_tac, *)
    2.47 -  METAHYPS(fn negs => ((warning("calling  call_atp_tac_tfrees"));call_atp_tac_tfrees (negs) n tfrees sg_term (childin, childout,pid) ))]) n
    2.48 +SELECT_GOAL (EVERY1 [rtac ccontr,atomize_tac,(*skolemize_tac,*) METAHYPS(fn negs => ((warning("calling  call_atp_tac_tfrees with negs"^(concat_with_and (map  string_of_thm negs) "")));(*make_clauses negs;*)dummy_tac)) ])1
    2.49  end;
    2.50  
    2.51  
    2.52 -fun isar_atp_g tfrees sg_term (childin, childout, pid)  = 
    2.53 +
    2.54 +METAHYPS(fn negs => ((warning("calling  call_atp_tac_tfrees with negs"^(concat_with_and (map  string_of_thm negs) ""))));make_clauses negs;dummy_tac)) 1;
    2.55 +*)
    2.56 +
    2.57 +
    2.58 +fun atp_tac_tfrees tfrees sg_term (childin, childout,pid)  n  = 
    2.59 +let val _ = (warning ("in atp_tac_tfrees "))
    2.60 +    val _ = (warning ("sg_term :"^((Sign.string_of_term Mainsign) sg_term)))
    2.61 +   
    2.62 +   in
    2.63 +SELECT_GOAL
    2.64 +  (EVERY1 [rtac ccontr,atomize_tac, tracify traceflag skolemize_tac, 
    2.65 +  METAHYPS(fn negs => ((warning("calling  call_atp_tac_tfrees with negs"^(concat_with_and (map  string_of_thm negs) "")));call_atp_tac_tfrees (negs) n tfrees sg_term (childin, childout,pid) ))]) n
    2.66 +end;
    2.67 +
    2.68 +
    2.69 +fun isar_atp_g tfrees sg_term (childin, childout, pid) n = 
    2.70                                          
    2.71 -(	(warning("in isar_atp_g"));atp_tac_tfrees tfrees sg_term (childin, childout, pid));
    2.72 +((warning("in isar_atp_g"));atp_tac_tfrees tfrees sg_term (childin, childout, pid) n);
    2.73  
    2.74  
    2.75  
    2.76 @@ -257,9 +279,11 @@
    2.77  	  		else 
    2.78                             (let val  prems = prems_of thm 
    2.79                                  val sg_term = get_nth n prems
    2.80 +                                val thmstring = string_of_thm thm
    2.81                              in   
    2.82                                   
    2.83                  		(warning("in isar_atp_goal'"));
    2.84 +                                (warning("thmstring in isar_atp_goal: "^thmstring));
    2.85   				 isar_atp_g tfree_lits  sg_term (childin, childout, pid) k thm; 
    2.86                                   isar_atp_goal' thm (k+1) n tfree_lits  (childin, childout, pid) 
    2.87                              end);
    2.88 @@ -270,7 +294,8 @@
    2.89  (**************************************************)
    2.90  (* convert clauses from "assume" to conjecture.   *)
    2.91  (* i.e. apply make_clauses and then get tptp for  *)
    2.92 -(* any hypotheses in the goal                     *)
    2.93 +(* any hypotheses in the goal produced by assume  *)
    2.94 +(* statements;                                    *)
    2.95  (* write to file "hyps"                           *)
    2.96  (**************************************************)
    2.97  
    2.98 @@ -375,13 +400,15 @@
    2.99  
   2.100  
   2.101  (* called in Isar automatically *)
   2.102 +
   2.103  fun isar_atp (ctxt,thm) =
   2.104      let val prems = ProofContext.prems_of ctxt
   2.105          val d_cs = Classical.get_delta_claset ctxt 
   2.106          val d_ss_thms = Simplifier.get_delta_simpset ctxt
   2.107          val thmstring = string_of_thm thm
   2.108 -        val prem_no = length prems
   2.109 -        val prems_string = concat_with_and (map string_of_thm prems) ""
   2.110 +        val sg_prems = prems_of thm
   2.111 +        val prem_no = length sg_prems
   2.112 +        val prems_string =  concat_with_and (map (Sign.string_of_term Mainsign) sg_prems) ""
   2.113      in
   2.114           
   2.115            (warning ("initial thm in isar_atp: "^thmstring));