src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 42019 a9445d87bc3e
parent 41963 d8c3b26b3da4
child 42020 2da02764d523
equal deleted inserted replaced
41996:1d7735ae4273 42019:a9445d87bc3e
   116 val narrowing_engine = File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")
   116 val narrowing_engine = File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")
   117 
   117 
   118 fun exec verbose code =
   118 fun exec verbose code =
   119   ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)
   119   ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)
   120 
   120 
   121 fun value ctxt (get, put, put_ml) (code, value) =
   121 fun value ctxt (get, put, put_ml) (code, value) size =
   122   let
   122   let
   123     val tmp_prefix = "Quickcheck_Narrowing"
   123     val tmp_prefix = "Quickcheck_Narrowing"
   124     fun run in_path = 
   124     fun run in_path = 
   125       let
   125       let
   126         val code_file = Path.append in_path (Path.basic "Code.hs")
   126         val code_file = Path.append in_path (Path.basic "Code.hs")
   127         val narrowing_engine_file = Path.append in_path (Path.basic "Narrowing_Engine.hs")
   127         val narrowing_engine_file = Path.append in_path (Path.basic "Narrowing_Engine.hs")
   128         val main_file = Path.append in_path (Path.basic "Main.hs")
   128         val main_file = Path.append in_path (Path.basic "Main.hs")
   129         val main = "module Main where {\n\n" ^
   129         val main = "module Main where {\n\n" ^
   130           "import Narrowing_Engine;\n" ^
   130           "import Narrowing_Engine;\n" ^
   131           "import Code;\n\n" ^
   131           "import Code;\n\n" ^
   132           "main = Narrowing_Engine.smallCheck 7 (Code.value ())\n\n" ^
   132           "main = Narrowing_Engine.smallCheck " ^ string_of_int size ^ " (Code.value ())\n\n" ^
   133           "}\n"
   133           "}\n"
   134         val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
   134         val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
   135           (unprefix "module Code where {" code)
   135           (unprefix "module Code where {" code)
   136         val _ = File.write code_file code'
   136         val _ = File.write code_file code'
   137         val _ = File.write narrowing_engine_file narrowing_engine
   137         val _ = File.write narrowing_engine_file narrowing_engine
   152     val ctxt' = ctxt
   152     val ctxt' = ctxt
   153       |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
   153       |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
   154       |> Context.proof_map (exec false ml_code);
   154       |> Context.proof_map (exec false ml_code);
   155   in get ctxt' () end;
   155   in get ctxt' () end;
   156 
   156 
   157 fun evaluation cookie thy evaluator vs_t args =
   157 fun evaluation cookie thy evaluator vs_t args size =
   158   let
   158   let
   159     val ctxt = ProofContext.init_global thy;
   159     val ctxt = ProofContext.init_global thy;
   160     val (program_code, value_name) = evaluator vs_t;
   160     val (program_code, value_name) = evaluator vs_t;
   161     val value_code = space_implode " "
   161     val value_code = space_implode " "
   162       (value_name :: "()" :: map (enclose "(" ")") args);
   162       (value_name :: "()" :: map (enclose "(" ")") args);
   163   in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end;
   163   in Exn.interruptible_capture (value ctxt cookie (program_code, value_code)) size end;
   164 
   164 
   165 fun dynamic_value_strict cookie thy postproc t args =
   165 fun dynamic_value_strict cookie thy postproc t args size =
   166   let
   166   let
   167     fun evaluator naming program ((_, vs_ty), t) deps =
   167     fun evaluator naming program ((_, vs_ty), t) deps =
   168       evaluation cookie thy (Code_Target.evaluator thy target naming program deps) (vs_ty, t) args;
   168       evaluation cookie thy (Code_Target.evaluator thy target naming program deps) (vs_ty, t) args size;
   169   in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
   169   in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
   170 
   170 
   171 (* counterexample generator *)
   171 (* counterexample generator *)
   172   
   172   
   173 structure Counterexample = Proof_Data
   173 structure Counterexample = Proof_Data
   183     val thy = ProofContext.theory_of ctxt
   183     val thy = ProofContext.theory_of ctxt
   184     fun ensure_testable t =
   184     fun ensure_testable t =
   185       Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
   185       Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
   186     val t = dynamic_value_strict
   186     val t = dynamic_value_strict
   187       (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
   187       (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
   188       thy (Option.map o map) (ensure_testable t) []
   188       thy (Option.map o map) (ensure_testable t) [] size
   189   in
   189   in
   190     (t, NONE)
   190     (t, NONE)
   191   end;
   191   end;
   192 
   192 
   193 
   193