# HG changeset patch # User wenzelm # Date 1303307734 -7200 # Node ID 5611f178a7471800ff8102872d870f360245ba35 # Parent 7ec150fcf3dc23431750f4a158bad1d5841c6c95 eliminated global references / critical sections via context data; misc tuning and modernization; diff -r 7ec150fcf3dc -r 5611f178a747 src/HOL/Library/SML_Quickcheck.thy --- a/src/HOL/Library/SML_Quickcheck.thy Wed Apr 20 14:33:33 2011 +0200 +++ b/src/HOL/Library/SML_Quickcheck.thy Wed Apr 20 15:55:34 2011 +0200 @@ -11,17 +11,17 @@ fn ctxt => fn [(t, eval_terms)] => let val prop = list_abs_free (Term.add_frees t [], t) - val test_fun = Codegen.test_term ctxt prop + val test_fun = Codegen.test_term ctxt prop val iterations = Config.get ctxt Quickcheck.iterations fun iterate size 0 = NONE | iterate size j = - let - val result = test_fun size handle Match => - (if Config.get ctxt Quickcheck.quiet then () - else warning "Exception Match raised during quickcheck"; NONE) - in - case result of NONE => iterate size (j - 1) | SOME q => SOME q - end + let + val result = test_fun size handle Match => + (if Config.get ctxt Quickcheck.quiet then () + else warning "Exception Match raised during quickcheck"; NONE) + in + case result of NONE => iterate size (j - 1) | SOME q => SOME q + end in fn [_, size] => (iterate size iterations, NONE) end)) *} diff -r 7ec150fcf3dc -r 5611f178a747 src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Wed Apr 20 14:33:33 2011 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Wed Apr 20 15:55:34 2011 +0200 @@ -6,12 +6,12 @@ signature INDUCTIVE_CODEGEN = sig - val add : string option -> int option -> attribute - val test_fn : (int * int * int -> term list option) Unsynchronized.ref (* FIXME *) - val test_term: - Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option - val setup : theory -> theory - val quickcheck_setup : theory -> theory + val add: string option -> int option -> attribute + val poke_test_fn: (int * int * int -> term list option) -> unit + val test_term: Proof.context -> (term * term list) list -> int list -> + term list option * Quickcheck.report option + val setup: theory -> theory + val quickcheck_setup: theory -> theory end; structure Inductive_Codegen : INDUCTIVE_CODEGEN = @@ -792,10 +792,18 @@ Scan.option (Args.$$$ "params" |-- Args.colon |-- Parse.nat) >> uncurry add)) "introduction rules for executable predicates"; + (**** Quickcheck involving inductive predicates ****) -val test_fn : (int * int * int -> term list option) Unsynchronized.ref = - Unsynchronized.ref (fn _ => NONE); +structure Result = Proof_Data +( + type T = int * int * int -> term list option; + fun init _ = (fn _ => NONE); +); + +val get_test_fn = Result.get; +fun poke_test_fn f = Context.>> (Context.map_proof (Result.put f)); + fun strip_imp p = let val (q, r) = HOLogic.dest_imp p @@ -814,56 +822,61 @@ val (size_offset, setup_size_offset) = Attrib.config_int "ind_quickcheck_size_offset" (K 0); fun test_term ctxt [(t, [])] = - let - val t' = list_abs_free (Term.add_frees t [], t) - val thy = Proof_Context.theory_of ctxt; - val (xs, p) = strip_abs t'; - val args' = map_index (fn (i, (_, T)) => ("arg" ^ string_of_int i, T)) xs; - val args = map Free args'; - val (ps, q) = strip_imp p; - val Ts = map snd xs; - val T = Ts ---> HOLogic.boolT; - val rl = Logic.list_implies - (map (HOLogic.mk_Trueprop o curry subst_bounds (rev args)) ps @ - [HOLogic.mk_Trueprop (HOLogic.mk_not (subst_bounds (rev args, q)))], - HOLogic.mk_Trueprop (list_comb (Free ("quickcheckp", T), args))); - val (_, thy') = Inductive.add_inductive_global - {quiet_mode=true, verbose=false, alt_name=Binding.empty, coind=false, - no_elim=true, no_ind=false, skip_mono=false, fork_mono=false} - [((Binding.name "quickcheckp", T), NoSyn)] [] - [(Attrib.empty_binding, rl)] [] (Theory.copy thy); - val pred = HOLogic.mk_Trueprop (list_comb - (Const (Sign.intern_const thy' "quickcheckp", T), - map Term.dummy_pattern Ts)); - val (code, gr) = - Codegen.generate_code_i thy' ["term_of", "test", "random_ind"] [] "Generated" - [("testf", pred)]; - val s = "structure TestTerm =\nstruct\n\n" ^ - cat_lines (map snd code) ^ - "\nopen Generated;\n\n" ^ Codegen.string_of - (Pretty.block [Codegen.str "val () = Inductive_Codegen.test_fn :=", - Pretty.brk 1, Codegen.str "(fn p =>", Pretty.brk 1, - Codegen.str "case Seq.pull (testf p) of", Pretty.brk 1, - Codegen.str "SOME ", mk_tuple [mk_tuple (map (Codegen.str o fst) args'), Codegen.str "_"], - Codegen.str " =>", Pretty.brk 1, Codegen.str "SOME ", - Pretty.enum "," "[" "]" - (map (fn (s, T) => Pretty.block - [Codegen.mk_term_of gr "Generated" false T, Pretty.brk 1, Codegen.str s]) args'), - Pretty.brk 1, - Codegen.str "| NONE => NONE);"]) ^ - "\n\nend;\n"; - val test_fn' = NAMED_CRITICAL "codegen" (fn () => - (ML_Context.eval_text_in (SOME ctxt) false Position.none s; ! test_fn)); - val values = Config.get ctxt random_values; - val bound = Config.get ctxt depth_bound; - val start = Config.get ctxt depth_start; - val offset = Config.get ctxt size_offset; - fun test [k] = (deepen bound (fn i => - (Output.urgent_message ("Search depth: " ^ string_of_int i); - test_fn' (i, values, k+offset))) start, NONE); - in test end - | test_term ctxt [(t, _)] = error "Option eval is not supported by tester SML_inductive" - | test_term ctxt _ = error "Compilation of multiple instances is not supported by tester SML_inductive"; + let + val t' = list_abs_free (Term.add_frees t [], t) + val thy = Proof_Context.theory_of ctxt; + val (xs, p) = strip_abs t'; + val args' = map_index (fn (i, (_, T)) => ("arg" ^ string_of_int i, T)) xs; + val args = map Free args'; + val (ps, q) = strip_imp p; + val Ts = map snd xs; + val T = Ts ---> HOLogic.boolT; + val rl = Logic.list_implies + (map (HOLogic.mk_Trueprop o curry subst_bounds (rev args)) ps @ + [HOLogic.mk_Trueprop (HOLogic.mk_not (subst_bounds (rev args, q)))], + HOLogic.mk_Trueprop (list_comb (Free ("quickcheckp", T), args))); + val (_, thy') = Inductive.add_inductive_global + {quiet_mode=true, verbose=false, alt_name=Binding.empty, coind=false, + no_elim=true, no_ind=false, skip_mono=false, fork_mono=false} + [((Binding.name "quickcheckp", T), NoSyn)] [] + [(Attrib.empty_binding, rl)] [] (Theory.copy thy); + val pred = HOLogic.mk_Trueprop (list_comb + (Const (Sign.intern_const thy' "quickcheckp", T), + map Term.dummy_pattern Ts)); + val (code, gr) = + Codegen.generate_code_i thy' ["term_of", "test", "random_ind"] [] "Generated" + [("testf", pred)]; + val s = "structure Test_Term =\nstruct\n\n" ^ + cat_lines (map snd code) ^ + "\nopen Generated;\n\n" ^ Codegen.string_of + (Pretty.block [Codegen.str "val () = Inductive_Codegen.poke_test_fn", + Pretty.brk 1, Codegen.str "(fn p =>", Pretty.brk 1, + Codegen.str "case Seq.pull (testf p) of", Pretty.brk 1, + Codegen.str "SOME ", + mk_tuple [mk_tuple (map (Codegen.str o fst) args'), Codegen.str "_"], + Codegen.str " =>", Pretty.brk 1, Codegen.str "SOME ", + Pretty.enum "," "[" "]" + (map (fn (s, T) => Pretty.block + [Codegen.mk_term_of gr "Generated" false T, Pretty.brk 1, Codegen.str s]) args'), + Pretty.brk 1, + Codegen.str "| NONE => NONE);"]) ^ + "\n\nend;\n"; + val test_fn = + ctxt + |> Context.proof_map + (ML_Context.exec (fn () => ML_Context.eval_text false Position.none s)) + |> get_test_fn; + val values = Config.get ctxt random_values; + val bound = Config.get ctxt depth_bound; + val start = Config.get ctxt depth_start; + val offset = Config.get ctxt size_offset; + fun test [k] = (deepen bound (fn i => + (Output.urgent_message ("Search depth: " ^ string_of_int i); + test_fn (i, values, k+offset))) start, NONE); + in test end + | test_term ctxt [_] = error "Option eval is not supported by tester SML_inductive" + | test_term ctxt _ = + error "Compilation of multiple instances is not supported by tester SML_inductive"; val quickcheck_setup = setup_depth_bound #> diff -r 7ec150fcf3dc -r 5611f178a747 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Wed Apr 20 14:33:33 2011 +0200 +++ b/src/Pure/codegen.ML Wed Apr 20 15:55:34 2011 +0200 @@ -74,9 +74,9 @@ val mk_type: bool -> typ -> Pretty.T val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T - val test_fn: (int -> term list option) Unsynchronized.ref (* FIXME *) + val poke_test_fn: (int -> term list option) -> unit + val poke_eval_fn: (unit -> term) -> unit val test_term: Proof.context -> term -> int -> term list option - val eval_result: (unit -> term) Unsynchronized.ref (* FIXME *) val eval_term: Proof.context -> term -> term val evaluation_conv: Proof.context -> conv val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list @@ -850,6 +850,21 @@ [mk_term_of gr module true T, mk_type true T]) Ts))); +(**** Implicit results ****) + +structure Result = Proof_Data +( + type T = (int -> term list option) * (unit -> term); + fun init _ = (fn _ => NONE, fn () => Bound 0); +); + +val get_test_fn = #1 o Result.get; +val get_eval_fn = #2 o Result.get; + +fun poke_test_fn f = Context.>> (Context.map_proof (Result.map (fn (_, g) => (f, g)))); +fun poke_eval_fn g = Context.>> (Context.map_proof (Result.map (fn (f, _) => (f, g)))); + + (**** Test data generators ****) fun mk_gen gr module p xs a (TVar ((s, i), _)) = str @@ -867,19 +882,16 @@ [mk_gen gr module true xs a T, mk_type true T]) Ts) @ (if member (op =) xs s then [str a] else [])))); -val test_fn : (int -> term list option) Unsynchronized.ref = - Unsynchronized.ref (fn _ => NONE); - fun test_term ctxt t = let val thy = Proof_Context.theory_of ctxt; val (code, gr) = generate_code_i thy ["term_of", "test"] [] "Generated" [("testf", t)]; val Ts = map snd (fst (strip_abs t)); val args = map_index (fn (i, T) => ("arg" ^ string_of_int i, T)) Ts; - val s = "structure TestTerm =\nstruct\n\n" ^ + val s = "structure Test_Term =\nstruct\n\n" ^ cat_lines (map snd code) ^ "\nopen Generated;\n\n" ^ string_of - (Pretty.block [str "val () = Codegen.test_fn :=", + (Pretty.block [str "val () = Codegen.poke_test_fn", Pretty.brk 1, str ("(fn i =>"), Pretty.brk 1, mk_let (map (fn (s, T) => (mk_tuple [str s, str (s ^ "_t")], @@ -893,42 +905,39 @@ Pretty.enum "," "[" "]" (map (fn (s, _) => str (s ^ "_t ()")) args)]]), str ");"]) ^ "\n\nend;\n"; - val test_fn' = NAMED_CRITICAL "codegen" (fn () => - (ML_Context.eval_text_in (SOME ctxt) false Position.none s; ! test_fn)); - in test_fn' end; - + in + ctxt + |> Context.proof_map (ML_Context.exec (fn () => ML_Context.eval_text false Position.none s)) + |> get_test_fn + end; (**** Evaluator for terms ****) -val eval_result = Unsynchronized.ref (fn () => Bound 0); - fun eval_term ctxt t = let - val e = - let - val thy = Proof_Context.theory_of ctxt; - val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse - error "Term to be evaluated contains type variables"; - val _ = (null (Term.add_vars t []) andalso null (Term.add_frees t [])) orelse - error "Term to be evaluated contains variables"; - val (code, gr) = - generate_code_i thy ["term_of"] [] "Generated" - [("result", Abs ("x", TFree ("'a", []), t))]; - val s = "structure EvalTerm =\nstruct\n\n" ^ - cat_lines (map snd code) ^ - "\nopen Generated;\n\n" ^ string_of - (Pretty.block [str "val () = Codegen.eval_result := (fn () =>", - Pretty.brk 1, - mk_app false (mk_term_of gr "Generated" false (fastype_of t)) - [str "(result ())"], - str ");"]) ^ - "\n\nend;\n"; - in - NAMED_CRITICAL "codegen" (fn () => - (ML_Context.eval_text_in (SOME ctxt) false Position.none s; ! eval_result)) - end - in e () end; + val thy = Proof_Context.theory_of ctxt; + val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse + error "Term to be evaluated contains type variables"; + val _ = (null (Term.add_vars t []) andalso null (Term.add_frees t [])) orelse + error "Term to be evaluated contains variables"; + val (code, gr) = + generate_code_i thy ["term_of"] [] "Generated" + [("result", Abs ("x", TFree ("'a", []), t))]; + val s = "structure Eval_Term =\nstruct\n\n" ^ + cat_lines (map snd code) ^ + "\nopen Generated;\n\n" ^ string_of + (Pretty.block [str "val () = Codegen.poke_eval_fn (fn () =>", + Pretty.brk 1, + mk_app false (mk_term_of gr "Generated" false (fastype_of t)) + [str "(result ())"], + str ");"]) ^ + "\n\nend;\n"; + val eval_fn = + ctxt + |> Context.proof_map (ML_Context.exec (fn () => ML_Context.eval_text false Position.none s)) + |> get_eval_fn; + in eval_fn () end; val (_, evaluation_oracle) = Context.>>> (Context.map_theory_result (Thm.add_oracle (Binding.name "evaluation", fn (ctxt, ct) =>