src/HOL/Tools/Quickcheck/narrowing_generators.ML
author bulwahn
Wed Apr 06 10:58:18 2011 +0200 (2011-04-06)
changeset 42258 79cb339d8989
parent 42214 9ca13615c619
child 42361 23f352990944
permissions -rw-r--r--
changing ensure_sort_datatype call in narrowing quickcheck (missed in 1491b7209e76)
     1 (*  Title:      HOL/Tools/Quickcheck/narrowing_generators.ML
     2     Author:     Lukas Bulwahn, TU Muenchen
     3 
     4 Narrowing-based counterexample generation.
     5 *)
     6 
     7 signature NARROWING_GENERATORS =
     8 sig
     9   val compile_generator_expr:
    10     Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
    11   val put_counterexample: (unit -> term list option) -> Proof.context -> Proof.context
    12   val finite_functions : bool Config.T
    13   val setup: theory -> theory
    14 end;
    15 
    16 structure Narrowing_Generators : NARROWING_GENERATORS =
    17 struct
    18 
    19 (* configurations *)
    20 
    21 val (finite_functions, setup_finite_functions) =
    22   Attrib.config_bool "quickcheck_finite_functions" (K true)
    23 
    24 (* narrowing specific names and types *)
    25 
    26 exception FUNCTION_TYPE;
    27 
    28 val narrowingN = "narrowing";
    29 
    30 fun narrowingT T =
    31   @{typ Quickcheck_Narrowing.code_int} --> Type (@{type_name Quickcheck_Narrowing.cons}, [T])
    32 
    33 fun mk_empty T = Const (@{const_name Quickcheck_Narrowing.empty}, narrowingT T)
    34 
    35 fun mk_cons c T = Const (@{const_name Quickcheck_Narrowing.cons}, T --> narrowingT T) $ Const (c, T)
    36 
    37 fun mk_apply (T, t) (U, u) =
    38   let
    39     val (_, U') = dest_funT U
    40   in
    41     (U', Const (@{const_name Quickcheck_Narrowing.apply},
    42       narrowingT U --> narrowingT T --> narrowingT U') $ u $ t)
    43   end
    44   
    45 fun mk_sum (t, u) =
    46   let
    47     val T = fastype_of t
    48   in
    49     Const (@{const_name Quickcheck_Narrowing.sum}, T --> T --> T) $ t $ u
    50   end
    51 
    52 (* creating narrowing instances *)
    53 
    54 fun mk_equations descr vs tycos narrowings (Ts, Us) =
    55   let
    56     fun mk_call T =
    57       (T, Const (@{const_name "Quickcheck_Narrowing.narrowing_class.narrowing"}, narrowingT T))
    58     fun mk_aux_call fTs (k, _) (tyco, Ts) =
    59       let
    60         val T = Type (tyco, Ts)
    61         val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
    62       in
    63         (T, nth narrowings k)
    64       end
    65     fun mk_consexpr simpleT (c, xs) =
    66       let
    67         val Ts = map fst xs
    68       in snd (fold mk_apply xs (Ts ---> simpleT, mk_cons c (Ts ---> simpleT))) end
    69     fun mk_rhs exprs = foldr1 mk_sum exprs
    70     val rhss =
    71       Datatype_Aux.interpret_construction descr vs
    72         { atyp = mk_call, dtyp = mk_aux_call }
    73       |> (map o apfst) Type
    74       |> map (fn (T, cs) => map (mk_consexpr T) cs)
    75       |> map mk_rhs
    76     val lhss = narrowings
    77     val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
    78   in
    79     eqs
    80   end
    81   
    82 fun instantiate_narrowing_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
    83   let
    84     val _ = Datatype_Aux.message config "Creating narrowing generators ...";
    85     val narrowingsN = map (prefix (narrowingN ^ "_")) (names @ auxnames);
    86   in
    87     thy
    88     |> Class.instantiation (tycos, vs, @{sort narrowing})
    89     |> Quickcheck_Common.define_functions
    90       (fn narrowings => mk_equations descr vs tycos narrowings (Ts, Us), NONE)
    91       prfx [] narrowingsN (map narrowingT (Ts @ Us))
    92     |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    93   end;
    94 
    95 (* testing framework *)
    96 
    97 val target = "Haskell"
    98 
    99 (* invocation of Haskell interpreter *)
   100 
   101 val narrowing_engine = File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")
   102 
   103 fun exec verbose code =
   104   ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)
   105 
   106 fun value ctxt (get, put, put_ml) (code, value) size =
   107   let
   108     val tmp_prefix = "Quickcheck_Narrowing"
   109     fun run in_path = 
   110       let
   111         val code_file = Path.append in_path (Path.basic "Code.hs")
   112         val narrowing_engine_file = Path.append in_path (Path.basic "Narrowing_Engine.hs")
   113         val main_file = Path.append in_path (Path.basic "Main.hs")
   114         val main = "module Main where {\n\n" ^
   115           "import Narrowing_Engine;\n" ^
   116           "import Code;\n\n" ^
   117           "main = Narrowing_Engine.depthCheck " ^ string_of_int size ^ " (Code.value ())\n\n" ^
   118           "}\n"
   119         val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
   120           (unprefix "module Code where {" code)
   121         val _ = File.write code_file code'
   122         val _ = File.write narrowing_engine_file narrowing_engine
   123         val _ = File.write main_file main
   124         val executable = File.shell_path (Path.append in_path (Path.basic "isa_lsc"))
   125         val cmd = "( exec \"$ISABELLE_GHC\" -fglasgow-exts " ^
   126           (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
   127           " -o " ^ executable ^ "; ) && " ^ executable
   128       in
   129         bash_output cmd
   130       end
   131     val result = Isabelle_System.with_tmp_dir tmp_prefix run
   132     val output_value = the_default "NONE"
   133       (try (snd o split_last o filter_out (fn s => s = "") o split_lines o fst) result)
   134       |> translate_string (fn s => if s = "\\" then "\\\\" else s)
   135     val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
   136       ^ " (fn () => " ^ output_value ^ ")) (ML_Context.the_generic_context ())))";
   137     val ctxt' = ctxt
   138       |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
   139       |> Context.proof_map (exec false ml_code);
   140   in get ctxt' () end;
   141 
   142 fun evaluation cookie thy evaluator vs_t args size =
   143   let
   144     val ctxt = ProofContext.init_global thy;
   145     val (program_code, value_name) = evaluator vs_t;
   146     val value_code = space_implode " "
   147       (value_name :: "()" :: map (enclose "(" ")") args);
   148   in Exn.interruptible_capture (value ctxt cookie (program_code, value_code)) size end;
   149 
   150 fun dynamic_value_strict cookie thy postproc t args size =
   151   let
   152     fun evaluator naming program ((_, vs_ty), t) deps =
   153       evaluation cookie thy (Code_Target.evaluator thy target naming program deps) (vs_ty, t) args size;
   154   in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
   155 
   156 (* counterexample generator *)
   157   
   158 structure Counterexample = Proof_Data
   159 (
   160   type T = unit -> term list option
   161   fun init _ () = error "Counterexample"
   162 )
   163 
   164 val put_counterexample = Counterexample.put
   165 
   166 fun finitize_functions t =
   167   let
   168     val ((names, Ts), t') = apfst split_list (strip_abs t)
   169     fun mk_eval_ffun dT rT =
   170       Const (@{const_name "Quickcheck_Narrowing.eval_ffun"}, 
   171         Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT]) --> dT --> rT)
   172     fun mk_eval_cfun dT rT =
   173       Const (@{const_name "Quickcheck_Narrowing.eval_cfun"}, 
   174         Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT]) --> dT --> rT)
   175     fun eval_function (T as Type (@{type_name fun}, [dT, rT])) =
   176       let
   177         val (rt', rT') = eval_function rT
   178       in
   179         case dT of
   180           Type (@{type_name fun}, _) =>
   181             (fn t => absdummy (dT, rt' (mk_eval_cfun dT rT' $ incr_boundvars 1 t $ Bound 0)),
   182             Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT']))
   183         | _ => (fn t => absdummy (dT, rt' (mk_eval_ffun dT rT' $ incr_boundvars 1 t $ Bound 0)),
   184             Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT']))
   185       end
   186       | eval_function T = (I, T)
   187     val (tt, Ts') = split_list (map eval_function Ts)
   188     val t'' = subst_bounds (map2 (fn f => fn x => f x) (rev tt) (map_index (Bound o fst) Ts), t')
   189   in
   190     list_abs (names ~~ Ts', t'')
   191   end
   192 
   193 fun compile_generator_expr ctxt [(t, eval_terms)] [_, size] =
   194   let
   195     val thy = ProofContext.theory_of ctxt
   196     val t' = list_abs_free (Term.add_frees t [], t)
   197     val t'' = if Config.get ctxt finite_functions then finitize_functions t' else t'
   198     fun ensure_testable t =
   199       Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
   200     val result = dynamic_value_strict
   201       (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
   202       thy (Option.map o map) (ensure_testable t'') [] size
   203   in
   204     (result, NONE)
   205   end;
   206 
   207 
   208 val setup =
   209   Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
   210     (((@{sort typerep}, @{sort term_of}), @{sort narrowing}), instantiate_narrowing_datatype))
   211   #> setup_finite_functions
   212   #> Context.theory_map
   213     (Quickcheck.add_generator ("narrowing", compile_generator_expr))
   214     
   215 end;