merged
authorbulwahn
Tue, 31 May 2011 18:13:00 +0200
changeset 43115 6773d8a9e351
parent 43114 b9fca691addd (diff)
parent 43111 61faa204c810 (current diff)
child 43116 e0add071fa10
merged
src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue May 31 17:15:14 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue May 31 18:13:00 2011 +0200
@@ -6,8 +6,7 @@
 
 signature NARROWING_GENERATORS =
 sig
-  val compile_generator_expr:
-    Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
+  val test_term: Proof.context -> bool * bool -> term * term list -> Quickcheck.result
   val put_counterexample: (unit -> term list option) -> Proof.context -> Proof.context
   val finite_functions : bool Config.T
   val overlord : bool Config.T
@@ -197,8 +196,9 @@
     val _ = Isabelle_System.mkdirs path;
   in Exn.release (Exn.capture f path) end;
   
-fun value ctxt (get, put, put_ml) (code, value) size =
+fun value ctxt (get, put, put_ml) (code, value_name) =
   let
+    fun message s = if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message s
     val tmp_prefix = "Quickcheck_Narrowing"
     val with_tmp_dir =
       if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir 
@@ -208,45 +208,55 @@
         val narrowing_engine_file = Path.append in_path (Path.basic "Narrowing_Engine.hs")
         val main_file = Path.append in_path (Path.basic "Main.hs")
         val main = "module Main where {\n\n" ^
+          "import System;\n" ^
           "import Narrowing_Engine;\n" ^
           "import Code;\n\n" ^
-          "main = Narrowing_Engine.depthCheck " ^ string_of_int size ^ " (Code.value ())\n\n" ^
+          "main = getArgs >>= \\[size] -> Narrowing_Engine.depthCheck (read size) (Code.value ())\n\n" ^
           "}\n"
         val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
           (unprefix "module Code where {" code)
         val _ = File.write code_file code'
         val _ = File.write narrowing_engine_file narrowing_engine
         val _ = File.write main_file main
-        val executable = File.shell_path (Path.append in_path (Path.basic "isa_lsc"))
-        val cmd = "( exec \"$ISABELLE_GHC\" -fglasgow-exts " ^
+        val executable = File.shell_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing"))
+        val cmd = "exec \"$ISABELLE_GHC\" -fglasgow-exts " ^
           (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
-          " -o " ^ executable ^ "; ) && " ^ executable
-      in
-        bash_output cmd
+          " -o " ^ executable ^ ";"
+        val _ = if bash cmd <> 0 then
+          error "Compilation failed!"
+        else
+          ()
+        fun with_size k =
+          if k > Config.get ctxt Quickcheck.size then
+            NONE
+          else
+            let
+              val _ = message ("Test data size: " ^ string_of_int k)
+              val (response, _) = bash_output (executable ^ " " ^ string_of_int k)
+            in
+              if response = "NONE\n" then with_size (k + 1) else SOME response
+            end
+      in case with_size 0 of
+           NONE => NONE
+         | SOME response =>
+           let
+             val output_value = the_default "NONE"
+               (try (snd o split_last o filter_out (fn s => s = "") o split_lines) response)
+               |> translate_string (fn s => if s = "\\" then "\\\\" else s)
+             val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
+               ^ " (fn () => " ^ output_value ^ ")) (ML_Context.the_generic_context ())))";
+             val ctxt' = ctxt
+               |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
+               |> Context.proof_map (exec false ml_code);
+           in get ctxt' () end     
       end
-    val result = with_tmp_dir tmp_prefix run
-    val output_value = the_default "NONE"
-      (try (snd o split_last o filter_out (fn s => s = "") o split_lines o fst) result)
-      |> translate_string (fn s => if s = "\\" then "\\\\" else s)
-    val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
-      ^ " (fn () => " ^ output_value ^ ")) (ML_Context.the_generic_context ())))";
-    val ctxt' = ctxt
-      |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
-      |> Context.proof_map (exec false ml_code);
-  in get ctxt' () end;
+  in with_tmp_dir tmp_prefix run end;
 
-fun evaluation cookie thy evaluator vs_t args size =
+fun dynamic_value_strict cookie thy postproc t =
   let
-    val ctxt = Proof_Context.init_global thy;
-    val (program_code, value_name) = evaluator vs_t;
-    val value_code = space_implode " "
-      (value_name :: "()" :: map (enclose "(" ")") args);
-  in Exn.interruptible_capture (value ctxt cookie (program_code, value_code)) size end;
-
-fun dynamic_value_strict cookie thy postproc t args size =
-  let
-    fun evaluator naming program ((_, vs_ty), t) deps =
-      evaluation cookie thy (Code_Target.evaluator thy target naming program deps) (vs_ty, t) args size;
+    val ctxt = Proof_Context.init_global thy
+    fun evaluator naming program ((_, vs_ty), t) deps = Exn.interruptible_capture (value ctxt cookie)
+      (Code_Target.evaluator thy target naming program deps (vs_ty, t));    
   in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
 
 (** counterexample generator **)
@@ -286,7 +296,9 @@
     list_abs (names ~~ Ts', t'')
   end
 
-fun compile_generator_expr ctxt [(t, eval_terms)] [_, size] =
+(** tester **)
+  
+fun test_term  ctxt (limit_time, is_interactive) (t, eval_terms) =
   let
     val thy = Proof_Context.theory_of ctxt
     val t' = list_abs_free (Term.add_frees t [], t)
@@ -295,11 +307,22 @@
       Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
     val result = dynamic_value_strict
       (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
-      thy (Option.map o map) (ensure_testable t'') [] size
+      thy (Option.map o map) (ensure_testable t'')
   in
-    (result, NONE)
+    Quickcheck.Result {counterexample = Option.map ((curry (op ~~)) (Term.add_free_names t [])) result,
+      evaluation_terms = Option.map (K []) result, timings = [], reports = []}
   end;
 
+fun test_goals ctxt (limit_time, is_interactive) insts goals =
+  let
+    val correct_inst_goals = Quickcheck.instantiate_goals ctxt insts goals
+  in
+    if Config.get ctxt Quickcheck.finite_types then
+      error "Quickcheck-Narrowing does not support finite_types"
+    else
+      Quickcheck.collect_results (test_term ctxt (limit_time, is_interactive)) (maps (map snd) correct_inst_goals) []
+  end
+
 (* setup *)
 
 val setup =
@@ -307,7 +330,6 @@
   #> Code.datatype_interpretation ensure_partial_term_of_code
   #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
     (((@{sort typerep}, @{sort term_of}), @{sort narrowing}), instantiate_narrowing_datatype))
-  #> Context.theory_map
-    (Quickcheck.add_generator ("narrowing", compile_generator_expr))
+  #> Context.theory_map (Quickcheck.add_tester ("narrowing", test_goals))
     
 end;
\ No newline at end of file
--- a/src/Tools/quickcheck.ML	Tue May 31 17:15:14 2011 +0200
+++ b/src/Tools/quickcheck.ML	Tue May 31 18:13:00 2011 +0200
@@ -31,16 +31,6 @@
   datatype report = Report of
     { iterations : int, raised_match_errors : int,
       satisfied_assms : int list, positive_concl_tests : int }
-  (* registering generators *)
-  val add_generator:
-    string * (Proof.context -> (term * term list) list -> int list -> term list option * report option)
-      -> Context.generic -> Context.generic
-  val add_batch_generator:
-    string * (Proof.context -> term list -> (int -> term list option) list)
-      -> Context.generic -> Context.generic
-  val add_batch_validator:
-    string * (Proof.context -> term list -> (int -> bool) list)
-      -> Context.generic -> Context.generic
   (* quickcheck's result *)
   datatype result =
     Result of
@@ -50,6 +40,23 @@
       reports : (int * report) list}
   val counterexample_of : result -> (string * term) list option
   val timings_of : result -> (string * int) list
+  (* registering generators *)
+  val add_generator:
+    string * (Proof.context -> (term * term list) list -> int list -> term list option * report option)
+      -> Context.generic -> Context.generic
+  val add_tester:
+    string * (Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list)
+      -> Context.generic -> Context.generic
+  val add_batch_generator:
+    string * (Proof.context -> term list -> (int -> term list option) list)
+      -> Context.generic -> Context.generic
+  val add_batch_validator:
+    string * (Proof.context -> term list -> (int -> bool) list)
+      -> Context.generic -> Context.generic
+  (* basic operations *)
+  val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list
+    -> (typ option * (term * term list)) list list
+  val collect_results: ('a -> result) -> 'a list -> result list -> result list
   (* testing terms and proof states *)
   val test_term: Proof.context -> bool * bool -> term * term list -> result
   val test_goal_terms:
@@ -174,17 +181,19 @@
 structure Data = Generic_Data
 (
   type T =
-    ((string * (Proof.context -> (term * term list) list -> int list -> term list option * report option)) list
+    (((string * (Proof.context -> (term * term list) list -> int list -> term list option * report option)) list
+      * (string * (Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list)) list)
       * ((string * (Proof.context -> term list -> (int -> term list option) list)) list
       * ((string * (Proof.context -> term list -> (int -> bool) list)) list)))
       * test_params;
-  val empty = (([], ([], [])), Test_Params {default_type = [], expect = No_Expectation});
+  val empty = ((([], []), ([], [])), Test_Params {default_type = [], expect = No_Expectation});
   val extend = I;
-  fun merge (((generators1, (batch_generators1, batch_validators1)), params1),
-    ((generators2, (batch_generators2, batch_validators2)), params2)) : T =
-    ((AList.merge (op =) (K true) (generators1, generators2),
-     (AList.merge (op =) (K true) (batch_generators1, batch_generators2),
-      AList.merge (op =) (K true) (batch_validators1, batch_validators2))),
+  fun merge ((((generators1, testers1), (batch_generators1, batch_validators1)), params1),
+    (((generators2, testers2), (batch_generators2, batch_validators2)), params2)) : T =
+    (((AList.merge (op =) (K true) (generators1, generators2),
+       AList.merge (op =) (K true) (testers1, testers2)),
+      (AList.merge (op =) (K true) (batch_generators1, batch_generators2),
+       AList.merge (op =) (K true) (batch_validators1, batch_validators2))),
       merge_test_params (params1, params2));
 );
 
@@ -196,7 +205,9 @@
 
 val map_test_params = Data.map o apsnd o map_test_params'
 
-val add_generator = Data.map o apfst o apfst o AList.update (op =);
+val add_generator = Data.map o apfst o apfst o apfst o AList.update (op =);
+
+val add_tester = Data.map o apfst o apfst o apsnd o AList.update (op =);
 
 val add_batch_generator = Data.map o apfst o apsnd o apfst o AList.update (op =);
 
@@ -223,12 +234,15 @@
   end
 
 val mk_tester =
-  gen_mk_tester (fn ctxt => AList.lookup (op =) ((fst o fst o Data.get o Context.Proof) ctxt))
+  gen_mk_tester (fn ctxt => AList.lookup (op =) ((fst o fst o fst o Data.get o Context.Proof) ctxt))
 val mk_batch_tester =
   gen_mk_tester (fn ctxt => AList.lookup (op =) ((fst o snd o fst o Data.get o Context.Proof) ctxt))
 val mk_batch_validator =
   gen_mk_tester (fn ctxt => AList.lookup (op =) ((snd o snd o fst o Data.get o Context.Proof) ctxt))
 
+  
+fun lookup_tester ctxt = AList.lookup (op =) ((snd o fst o fst o Data.get o Context.Proof) ctxt)
+
 (* testing propositions *)
 
 fun check_test_term t =
@@ -403,7 +417,7 @@
 
 datatype wellsorted_error = Wellsorted_Error of string | Term of term * term list
 
-fun test_goal_terms lthy (limit_time, is_interactive) insts check_goals =
+fun instantiate_goals lthy insts goals =
   let
     fun map_goal_and_eval_terms f (check_goal, eval_terms) = (f check_goal, map f eval_terms)
     val thy = Proof_Context.theory_of lthy
@@ -417,7 +431,7 @@
               (map_goal_and_eval_terms (monomorphic_term thy insts T) (check_goal, eval_terms))
               handle WELLSORTED s => (SOME T, Wellsorted_Error s)) default_insts
         else
-          [(NONE, Term (Object_Logic.atomize_term thy check_goal, eval_terms))]) check_goals
+          [(NONE, Term (Object_Logic.atomize_term thy check_goal, eval_terms))]) goals
     val error_msg =
       cat_lines
         (maps (map_filter (fn (_, Term t) => NONE | (_, Wellsorted_Error s) => SOME s)) inst_goals)
@@ -428,20 +442,28 @@
         [[]] => error error_msg
       | xs => xs
     val _ = if Config.get lthy quiet then () else warning error_msg
-    fun collect_results f [] results = results
-      | collect_results f (t :: ts) results =
-        let
-          val result = f t
-        in
-          if found_counterexample result then
-            (result :: results)
-          else
-            collect_results f ts (result :: results)
-        end
+  in
+    correct_inst_goals
+  end
+
+fun collect_results f [] results = results
+  | collect_results f (t :: ts) results =
+    let
+      val result = f t
+    in
+      if found_counterexample result then
+        (result :: results)
+      else
+        collect_results f ts (result :: results)
+    end  
+
+fun test_goal_terms lthy (limit_time, is_interactive) insts goals =
+  let
     fun test_term' goal =
       case goal of
         [(NONE, t)] => test_term lthy (limit_time, is_interactive) t
       | ts => test_term_with_increasing_cardinality lthy (limit_time, is_interactive) (map snd ts)
+    val correct_inst_goals = instantiate_goals lthy insts goals
   in
     if Config.get lthy finite_types then
       collect_results test_term' correct_inst_goals []
@@ -465,13 +487,14 @@
      of NONE => Assumption.all_assms_of lthy
       | SOME locale => Assumption.local_assms_of lthy (Locale.init locale thy);
     val proto_goal = Logic.list_implies (map Thm.term_of assms, subst_bounds (frees, strip gi));
-    val check_goals = case some_locale
+    val goals = case some_locale
      of NONE => [(proto_goal, eval_terms)]
       | SOME locale =>
         map (fn (_, phi) => (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms))
           (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
+    val test_goals = the_default test_goal_terms (lookup_tester lthy (Config.get lthy tester))
   in
-    test_goal_terms lthy (time_limit, is_interactive) insts check_goals
+    test_goals lthy (time_limit, is_interactive) insts goals
   end
 
 (* pretty printing *)
@@ -544,7 +567,9 @@
   | read_expectation "counterexample" = Counterexample
   | read_expectation s = error ("Not an expectation value: " ^ s)
 
-fun valid_tester_name genctxt = AList.defined (op =) (fst (fst (Data.get genctxt)))
+fun valid_tester_name genctxt name =
+  AList.defined (op =) (fst (fst (fst (Data.get genctxt)))) name orelse
+    AList.defined (op =) (snd (fst (fst (Data.get genctxt)))) name
 
 fun parse_tester name genctxt =
   if valid_tester_name genctxt name then