Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
authorpaulson
Tue Mar 07 16:46:54 2006 +0100 (2006-03-07 ago)
changeset 192054ec788c69f82
parent 19204 b8f7de7ef629
child 19206 79053aa24abf
Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Tue Mar 07 16:45:04 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Mar 07 16:46:54 2006 +0100
     1.3 @@ -15,14 +15,14 @@
     1.4    val time_limit: int ref
     1.5     
     1.6    datatype mode = Auto | Fol | Hol
     1.7 -  val write_subgoal_file: mode -> Proof.context -> Thm.thm list -> Thm.thm list -> int -> string
     1.8 +  val write_subgoal_file: mode -> Proof.context -> thm list -> thm list -> int -> string
     1.9    val vampire_time: int ref
    1.10    val eprover_time: int ref
    1.11    val run_vampire: int -> unit
    1.12    val run_eprover: int -> unit
    1.13    val vampireLimit: unit -> int
    1.14    val eproverLimit: unit -> int
    1.15 -  val atp_method: (ProofContext.context -> Thm.thm list -> int -> Tactical.tactic) ->
    1.16 +  val atp_method: (ProofContext.context -> thm list -> int -> Tactical.tactic) ->
    1.17  		  Method.src -> ProofContext.context -> Method.method
    1.18    val cond_rm_tmp: string -> unit
    1.19    val keep_atp_input: bool ref
    1.20 @@ -33,10 +33,10 @@
    1.21    val hol_no_types: unit -> unit
    1.22    val hol_typ_level: unit -> ResHolClause.type_level
    1.23    val run_relevance_filter: bool ref
    1.24 -
    1.25 +  val invoke_atp_ml : ProofContext.context * thm -> unit
    1.26  end;
    1.27  
    1.28 -structure ResAtp: RES_ATP =
    1.29 +structure ResAtp : RES_ATP =
    1.30  struct
    1.31  
    1.32  (********************************************************************)
    1.33 @@ -341,6 +341,8 @@
    1.34  
    1.35  datatype mode = Auto | Fol | Hol;
    1.36  
    1.37 +val linkup_logic_mode = ref Fol;
    1.38 +
    1.39  fun tptp_writer logic goals filename (axioms,classrels,arities) =
    1.40      if is_fol_logic logic then ResClause.tptp_write_file goals filename (axioms, classrels, arities)
    1.41      else
    1.42 @@ -468,7 +470,9 @@
    1.43  		  negs_clauses::(get_neg_subgoals (n - 1))
    1.44  	      end
    1.45        val neg_subgoals = get_neg_subgoals (length goals) 
    1.46 -      val goals_logic = problem_logic_goals neg_subgoals
    1.47 +      val goals_logic = case !linkup_logic_mode of Auto => problem_logic_goals neg_subgoals
    1.48 +						 | Fol => FOL
    1.49 +						 | Hol => HOL
    1.50        val keep_types = if is_fol_logic goals_logic then !ResClause.keep_types else is_typed_hol ()
    1.51        val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else []
    1.52        val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
    1.53 @@ -522,15 +526,12 @@
    1.54  
    1.55  (** the Isar toplevel hook **)
    1.56  
    1.57 -val invoke_atp = Toplevel.unknown_proof o Toplevel.keep (fn state =>
    1.58 -  let
    1.59 -    val proof = Toplevel.proof_of state
    1.60 -    val (ctxt, (_, goal)) = Proof.get_goal proof;
    1.61 -    val thy = ProofContext.theory_of ctxt;
    1.62 +fun invoke_atp_ml (ctxt, goal) =
    1.63 +  let val thy = ProofContext.theory_of ctxt;
    1.64    in
    1.65      Output.debug ("subgoals in isar_atp:\n" ^ 
    1.66 -           Pretty.string_of (ProofContext.pretty_term ctxt
    1.67 -             (Logic.mk_conjunction_list (Thm.prems_of goal))));
    1.68 +		  Pretty.string_of (ProofContext.pretty_term ctxt
    1.69 +		    (Logic.mk_conjunction_list (Thm.prems_of goal))));
    1.70      Output.debug ("current theory: " ^ Context.theory_name thy);
    1.71      hook_count := !hook_count +1;
    1.72      Output.debug ("in hook for time: " ^ Int.toString (!hook_count));
    1.73 @@ -538,14 +539,19 @@
    1.74      ResHolClause.init thy;
    1.75      if !destdir = "" andalso !time_limit > 0 then isar_atp (ctxt, goal)
    1.76      else isar_atp_writeonly (ctxt, goal)
    1.77 -  end);
    1.78 +  end;
    1.79 +
    1.80 +val invoke_atp = Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep
    1.81 + (fn state =>
    1.82 +  let val (ctxt, (_, goal)) = Proof.get_goal (Toplevel.proof_of state)
    1.83 +  in  invoke_atp_ml (ctxt, goal)  end);
    1.84  
    1.85  val call_atpP =
    1.86    OuterSyntax.command 
    1.87      "ProofGeneral.call_atp" 
    1.88      "call automatic theorem provers" 
    1.89      OuterKeyword.diag
    1.90 -    (Scan.succeed (Toplevel.no_timing o invoke_atp));
    1.91 +    (Scan.succeed invoke_atp);
    1.92  
    1.93  val _ = OuterSyntax.add_parsers [call_atpP];
    1.94