src/HOL/Tools/ATP_Manager/atp_systems.ML
changeset 37499 5ff37037fbec
parent 37498 b426cbdb5a23
child 37506 32a1ee39c49b
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jun 22 14:28:22 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jun 22 14:48:46 2010 +0200
     1.3 @@ -115,10 +115,15 @@
     1.4        (j :: hd shape) :: tl shape
     1.5      end
     1.6  
     1.7 -fun generic_prover overlord get_facts prepare write_file home_var executable
     1.8 -        args proof_delims known_failures name
     1.9 -        ({debug, full_types, explicit_apply, isar_proof, isar_shrink_factor,
    1.10 -         ...} : params) minimize_command
    1.11 +(* generic TPTP-based provers *)
    1.12 +
    1.13 +fun generic_tptp_prover
    1.14 +        (name, {home_var, executable, arguments, proof_delims, known_failures,
    1.15 +                max_axiom_clauses, prefers_theory_relevant})
    1.16 +        ({debug, overlord, full_types, explicit_apply, respect_no_atp,
    1.17 +          relevance_threshold, relevance_convergence, theory_relevant,
    1.18 +          defs_relevant, isar_proof, isar_shrink_factor, ...} : params)
    1.19 +        minimize_command timeout
    1.20          ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
    1.21           : problem) =
    1.22    let
    1.23 @@ -129,14 +134,18 @@
    1.24      val goal_cls = List.concat goal_clss
    1.25      val the_filtered_clauses =
    1.26        (case filtered_clauses of
    1.27 -        NONE => get_facts relevance_override goal goal_cls
    1.28 +        NONE => relevant_facts full_types respect_no_atp relevance_threshold
    1.29 +                    relevance_convergence defs_relevant max_axiom_clauses
    1.30 +                    (the_default prefers_theory_relevant theory_relevant)
    1.31 +                    relevance_override goal goal_cls
    1.32        | SOME fcls => fcls);
    1.33      val the_axiom_clauses =
    1.34        (case axiom_clauses of
    1.35          NONE => the_filtered_clauses
    1.36        | SOME axcls => axcls);
    1.37      val (internal_thm_names, clauses) =
    1.38 -      prepare goal_cls the_axiom_clauses the_filtered_clauses thy
    1.39 +      prepare_clauses full_types goal_cls the_axiom_clauses the_filtered_clauses
    1.40 +                      thy
    1.41  
    1.42      (* path to unique problem file *)
    1.43      val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
    1.44 @@ -161,10 +170,10 @@
    1.45      fun command_line probfile =
    1.46        (if Config.get ctxt measure_runtime then
    1.47           "TIMEFORMAT='%3U'; { time " ^
    1.48 -         space_implode " " [File.shell_path command, args,
    1.49 +         space_implode " " [File.shell_path command, arguments timeout,
    1.50                              File.shell_path probfile] ^ " ; } 2>&1"
    1.51         else
    1.52 -         space_implode " " ["exec", File.shell_path command, args,
    1.53 +         space_implode " " ["exec", File.shell_path command, arguments timeout,
    1.54                              File.shell_path probfile, "2>&1"]) ^
    1.55        (if overlord then
    1.56           " | sed 's/,/, /g' \
    1.57 @@ -189,7 +198,8 @@
    1.58        if Config.get ctxt measure_runtime then split_time s else (s, 0)
    1.59      fun run_on probfile =
    1.60        if File.exists command then
    1.61 -        write_file full_types explicit_apply probfile clauses
    1.62 +        write_tptp_file (debug andalso overlord) full_types explicit_apply
    1.63 +                        probfile clauses
    1.64          |> pair (apfst split_time' (bash_output (command_line probfile)))
    1.65        else if home = "" then
    1.66          error ("The environment variable " ^ quote home_var ^ " is not set.")
    1.67 @@ -233,25 +243,7 @@
    1.68       proof = proof, internal_thm_names = internal_thm_names,
    1.69       conjecture_shape = conjecture_shape,
    1.70       filtered_clauses = the_filtered_clauses}
    1.71 -  end;
    1.72 -
    1.73 -
    1.74 -(* generic TPTP-based provers *)
    1.75 -
    1.76 -fun generic_tptp_prover
    1.77 -        (name, {home_var, executable, arguments, proof_delims, known_failures,
    1.78 -                max_axiom_clauses, prefers_theory_relevant})
    1.79 -        (params as {debug, overlord, full_types, respect_no_atp,
    1.80 -                    relevance_threshold, relevance_convergence, theory_relevant,
    1.81 -                    defs_relevant, ...})
    1.82 -        minimize_command timeout =
    1.83 -  generic_prover overlord
    1.84 -      (relevant_facts full_types respect_no_atp relevance_threshold
    1.85 -                      relevance_convergence defs_relevant max_axiom_clauses
    1.86 -                      (the_default prefers_theory_relevant theory_relevant))
    1.87 -      (prepare_clauses full_types) (write_tptp_file (debug andalso overlord))
    1.88 -      home_var executable (arguments timeout) proof_delims known_failures name
    1.89 -      params minimize_command
    1.90 +  end
    1.91  
    1.92  fun tptp_prover name p = (name, generic_tptp_prover (name, p));
    1.93