eliminated extraneous wrapping of public records;
authorwenzelm
Thu Oct 15 11:49:27 2009 +0200 (2009-10-15)
changeset 3294172d48e333b77
parent 32940 51d450f278ce
child 32942 b6711ec9de26
eliminated extraneous wrapping of public records;
tuned;
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Tools/ATP_Manager/atp_manager.ML
src/HOL/Tools/ATP_Manager/atp_minimal.ML
src/HOL/Tools/ATP_Manager/atp_wrapper.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Oct 15 11:23:03 2009 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Oct 15 11:49:27 2009 +0200
     1.3 @@ -307,8 +307,7 @@
     1.4        (case hard_timeout of
     1.5          NONE => I
     1.6        | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
     1.7 -    val (ATP_Wrapper.Prover_Result {success, message, theorem_names,
     1.8 -      runtime=time_atp, ...}, time_isa) =
     1.9 +    val ({success, message, theorem_names, runtime=time_atp, ...}, time_isa) =
    1.10        time_limit (Mirabelle.cpu_time atp) timeout
    1.11    in
    1.12      if success then (message, SH_OK (time_isa, time_atp, theorem_names))
     2.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Oct 15 11:23:03 2009 +0200
     2.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Oct 15 11:49:27 2009 +0200
     2.3 @@ -325,7 +325,7 @@
     2.4              val problem =
     2.5                ATP_Wrapper.atp_problem_of_goal (! full_types) i (Proof.get_goal proof_state);
     2.6              val result =
     2.7 -              let val ATP_Wrapper.Prover_Result {success, message, ...} = prover problem (! timeout);
     2.8 +              let val {success, message, ...} = prover problem (! timeout);
     2.9                in (success, message) end
    2.10                handle ResHolClause.TOO_TRIVIAL =>   (* FIXME !? *)
    2.11                    (true, "Empty clause: Try this command: " ^
     3.1 --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Thu Oct 15 11:23:03 2009 +0200
     3.2 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Thu Oct 15 11:49:27 2009 +0200
     3.3 @@ -97,10 +97,10 @@
     3.4     ("# Cannot determine problem status within resource limit", Timeout),
     3.5     ("Error", Error)]
     3.6  
     3.7 -fun produce_answer result =
     3.8 +fun produce_answer (result: ATP_Wrapper.prover_result) =
     3.9    let
    3.10 -    val ATP_Wrapper.Prover_Result {success, message, proof=result_string,
    3.11 -      internal_thm_names=thm_name_vec, filtered_clauses=filtered, ...} = result
    3.12 +    val {success, message, proof = result_string,
    3.13 +      internal_thm_names = thm_name_vec, filtered_clauses = filtered, ...} = result
    3.14    in
    3.15    if success then
    3.16      (Success (Vector.foldr op:: [] thm_name_vec, filtered), result_string)
    3.17 @@ -125,12 +125,12 @@
    3.18      val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
    3.19      val _ = debug_fn (fn () => print_names name_thm_pairs)
    3.20      val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
    3.21 -    val problem = ATP_Wrapper.ATP_Problem {
    3.22 -      with_full_types = ! ATP_Manager.full_types,
    3.23 +    val problem =
    3.24 +     {with_full_types = ! ATP_Manager.full_types,
    3.25        subgoal = subgoalno,
    3.26        goal = Proof.get_goal state,
    3.27        axiom_clauses = SOME axclauses,
    3.28 -      filtered_clauses = filtered }
    3.29 +      filtered_clauses = filtered}
    3.30      val (result, proof) = produce_answer (prover problem time_limit)
    3.31      val _ = println (string_of_result result)
    3.32      val _ = debug proof
     4.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Thu Oct 15 11:23:03 2009 +0200
     4.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Thu Oct 15 11:49:27 2009 +0200
     4.3 @@ -12,28 +12,27 @@
     4.4    val setup: theory -> theory
     4.5  
     4.6    (*prover configuration, problem format, and prover result*)
     4.7 -  datatype prover_config = Prover_Config of {
     4.8 -    command: Path.T,
     4.9 +  type prover_config =
    4.10 +   {command: Path.T,
    4.11      arguments: int -> string,
    4.12      max_new_clauses: int,
    4.13      insert_theory_const: bool,
    4.14 -    emit_structured_proof: bool }
    4.15 -  datatype atp_problem = ATP_Problem of {
    4.16 -    with_full_types: bool,
    4.17 +    emit_structured_proof: bool}
    4.18 +  type atp_problem =
    4.19 +   {with_full_types: bool,
    4.20      subgoal: int,
    4.21      goal: Proof.context * (thm list * thm),
    4.22      axiom_clauses: (thm * (string * int)) list option,
    4.23 -    filtered_clauses: (thm * (string * int)) list option }
    4.24 -  val atp_problem_of_goal: bool -> int -> Proof.context * (thm list * thm) ->
    4.25 -    atp_problem
    4.26 -  datatype prover_result = Prover_Result of {
    4.27 -    success: bool,
    4.28 +    filtered_clauses: (thm * (string * int)) list option}
    4.29 +  val atp_problem_of_goal: bool -> int -> Proof.context * (thm list * thm) -> atp_problem
    4.30 +  type prover_result =
    4.31 +   {success: bool,
    4.32      message: string,
    4.33      theorem_names: string list,
    4.34      runtime: int,
    4.35      proof: string,
    4.36      internal_thm_names: string Vector.vector,
    4.37 -    filtered_clauses: (thm * (string * int)) list }
    4.38 +    filtered_clauses: (thm * (string * int)) list}
    4.39    type prover = atp_problem -> int -> prover_result
    4.40  
    4.41    (*common provers*)
    4.42 @@ -67,37 +66,37 @@
    4.43  
    4.44  (* prover configuration, problem format, and prover result *)
    4.45  
    4.46 -datatype prover_config = Prover_Config of {
    4.47 -  command: Path.T,
    4.48 +type prover_config =
    4.49 + {command: Path.T,
    4.50    arguments: int -> string,
    4.51    max_new_clauses: int,
    4.52    insert_theory_const: bool,
    4.53 -  emit_structured_proof: bool }
    4.54 +  emit_structured_proof: bool};
    4.55  
    4.56 -datatype atp_problem = ATP_Problem of {
    4.57 -  with_full_types: bool,
    4.58 +type atp_problem =
    4.59 + {with_full_types: bool,
    4.60    subgoal: int,
    4.61    goal: Proof.context * (thm list * thm),
    4.62    axiom_clauses: (thm * (string * int)) list option,
    4.63 -  filtered_clauses: (thm * (string * int)) list option }
    4.64 +  filtered_clauses: (thm * (string * int)) list option};
    4.65  
    4.66 -fun atp_problem_of_goal with_full_types subgoal goal = ATP_Problem {
    4.67 -  with_full_types = with_full_types,
    4.68 +fun atp_problem_of_goal with_full_types subgoal goal : atp_problem =
    4.69 + {with_full_types = with_full_types,
    4.70    subgoal = subgoal,
    4.71    goal = goal,
    4.72    axiom_clauses = NONE,
    4.73 -  filtered_clauses = NONE }
    4.74 +  filtered_clauses = NONE};
    4.75  
    4.76 -datatype prover_result = Prover_Result of {
    4.77 -  success: bool,
    4.78 +type prover_result =
    4.79 + {success: bool,
    4.80    message: string,
    4.81 -  theorem_names: string list,  (* relevant theorems *)
    4.82 -  runtime: int,  (* user time of the ATP, in milliseconds *)
    4.83 +  theorem_names: string list,  (*relevant theorems*)
    4.84 +  runtime: int,  (*user time of the ATP, in milliseconds*)
    4.85    proof: string,
    4.86    internal_thm_names: string Vector.vector,
    4.87 -  filtered_clauses: (thm * (string * int)) list }
    4.88 +  filtered_clauses: (thm * (string * int)) list};
    4.89  
    4.90 -type prover = atp_problem -> int -> prover_result
    4.91 +type prover = atp_problem -> int -> prover_result;
    4.92  
    4.93  
    4.94  (* basic template *)
    4.95 @@ -106,7 +105,7 @@
    4.96    Exn.capture f path
    4.97    |> tap (fn _ => cleanup path)
    4.98    |> Exn.release
    4.99 -  |> tap (after path)
   4.100 +  |> tap (after path);
   4.101  
   4.102  fun external_prover relevance_filter preparer writer cmd args find_failure produce_answer
   4.103    axiom_clauses filtered_clauses name subgoalno goal =
   4.104 @@ -178,9 +177,9 @@
   4.105          (produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoalno))
   4.106      val _ = Output.debug (fn () => "Sledgehammer response (rc = " ^ string_of_int rc ^ "):\n" ^ proof)
   4.107    in
   4.108 -    Prover_Result {success=success, message=message,
   4.109 -      theorem_names=real_thm_names, runtime=time, proof=proof,
   4.110 -      internal_thm_names = thm_names, filtered_clauses=the_filtered_clauses}
   4.111 +    {success = success, message = message,
   4.112 +      theorem_names = real_thm_names, runtime = time, proof = proof,
   4.113 +      internal_thm_names = thm_names, filtered_clauses = the_filtered_clauses}
   4.114    end
   4.115  
   4.116  
   4.117 @@ -188,10 +187,9 @@
   4.118  
   4.119  fun gen_tptp_prover (name, prover_config) problem timeout =
   4.120    let
   4.121 -    val Prover_Config {max_new_clauses, insert_theory_const,
   4.122 -      emit_structured_proof, command, arguments} = prover_config
   4.123 -    val ATP_Problem {with_full_types, subgoal, goal, axiom_clauses,
   4.124 -      filtered_clauses} = problem
   4.125 +    val {max_new_clauses, insert_theory_const, emit_structured_proof, command, arguments} =
   4.126 +      prover_config
   4.127 +    val {with_full_types, subgoal, goal, axiom_clauses, filtered_clauses} = problem
   4.128    in
   4.129      external_prover
   4.130        (ResAtp.get_relevant max_new_clauses insert_theory_const)
   4.131 @@ -201,7 +199,7 @@
   4.132        (arguments timeout)
   4.133        ResReconstruct.find_failure
   4.134        (if emit_structured_proof then ResReconstruct.structured_proof
   4.135 -        else ResReconstruct.lemma_list false)
   4.136 +       else ResReconstruct.lemma_list false)
   4.137        axiom_clauses
   4.138        filtered_clauses
   4.139        name
   4.140 @@ -212,6 +210,7 @@
   4.141  fun tptp_prover (name, config) = (name, gen_tptp_prover (name, config))
   4.142  
   4.143  
   4.144 +
   4.145  (** common provers **)
   4.146  
   4.147  (* Vampire *)
   4.148 @@ -221,13 +220,13 @@
   4.149  val vampire_max_new_clauses = 60
   4.150  val vampire_insert_theory_const = false
   4.151  
   4.152 -fun vampire_prover_config full = Prover_Config {
   4.153 -  command = Path.explode "$VAMPIRE_HOME/vampire",
   4.154 +fun vampire_prover_config full : prover_config =
   4.155 + {command = Path.explode "$VAMPIRE_HOME/vampire",
   4.156    arguments = (fn timeout => "--output_syntax tptp --mode casc" ^
   4.157      " -t " ^ string_of_int timeout),
   4.158    max_new_clauses = vampire_max_new_clauses,
   4.159    insert_theory_const = vampire_insert_theory_const,
   4.160 -  emit_structured_proof = full }
   4.161 +  emit_structured_proof = full}
   4.162  
   4.163  val vampire = tptp_prover ("vampire", vampire_prover_config false)
   4.164  val vampire_full = tptp_prover ("vampire_full", vampire_prover_config true)
   4.165 @@ -238,13 +237,13 @@
   4.166  val eprover_max_new_clauses = 100
   4.167  val eprover_insert_theory_const = false
   4.168  
   4.169 -fun eprover_config full = Prover_Config {
   4.170 -  command = Path.explode "$E_HOME/eproof",
   4.171 +fun eprover_config full : prover_config =
   4.172 + {command = Path.explode "$E_HOME/eproof",
   4.173    arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev" ^
   4.174      " --silent --cpu-limit=" ^ string_of_int timeout),
   4.175    max_new_clauses = eprover_max_new_clauses,
   4.176    insert_theory_const = eprover_insert_theory_const,
   4.177 -  emit_structured_proof = full }
   4.178 +  emit_structured_proof = full}
   4.179  
   4.180  val eprover = tptp_prover ("e", eprover_config false)
   4.181  val eprover_full = tptp_prover ("e_full", eprover_config true)
   4.182 @@ -255,20 +254,19 @@
   4.183  val spass_max_new_clauses = 40
   4.184  val spass_insert_theory_const = true
   4.185  
   4.186 -fun spass_config insert_theory_const = Prover_Config {
   4.187 -  command = Path.explode "$SPASS_HOME/SPASS",
   4.188 +fun spass_config insert_theory_const: prover_config =
   4.189 + {command = Path.explode "$SPASS_HOME/SPASS",
   4.190    arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^
   4.191      " -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout),
   4.192    max_new_clauses = spass_max_new_clauses,
   4.193    insert_theory_const = insert_theory_const,
   4.194 -  emit_structured_proof = false }
   4.195 +  emit_structured_proof = false}
   4.196  
   4.197  fun gen_dfg_prover (name, prover_config) problem timeout =
   4.198    let
   4.199 -    val Prover_Config {max_new_clauses, insert_theory_const,
   4.200 -      emit_structured_proof, command, arguments} = prover_config
   4.201 -    val ATP_Problem {with_full_types, subgoal, goal, axiom_clauses,
   4.202 -      filtered_clauses} = problem
   4.203 +    val {max_new_clauses, insert_theory_const, emit_structured_proof, command, arguments} =
   4.204 +      prover_config
   4.205 +    val {with_full_types, subgoal, goal, axiom_clauses, filtered_clauses} = problem
   4.206    in
   4.207      external_prover
   4.208        (ResAtp.get_relevant max_new_clauses insert_theory_const)
   4.209 @@ -316,13 +314,13 @@
   4.210      NONE => error ("No system like " ^ quote prefix ^ " at SystemOnTPTP")
   4.211    | SOME sys => sys)
   4.212  
   4.213 -fun remote_prover_config prover_prefix args max_new insert_tc = Prover_Config {
   4.214 -  command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
   4.215 +fun remote_prover_config prover_prefix args max_new insert_tc: prover_config =
   4.216 + {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
   4.217    arguments = (fn timeout => args ^ " -t " ^ string_of_int timeout ^ " -s " ^
   4.218      get_the_system prover_prefix),
   4.219    max_new_clauses = max_new,
   4.220    insert_theory_const = insert_tc,
   4.221 -  emit_structured_proof = false }
   4.222 +  emit_structured_proof = false}
   4.223  
   4.224  val remote_vampire = tptp_prover ("remote_vampire", remote_prover_config
   4.225    "Vampire---9" "" vampire_max_new_clauses vampire_insert_theory_const)