1.1 --- a/src/Pure/codegen.ML Mon Sep 22 13:56:03 2008 +0200
1.2 +++ b/src/Pure/codegen.ML Mon Sep 22 13:56:04 2008 +0200
1.3 @@ -77,10 +77,7 @@
1.4 val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T
1.5 val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T
1.6 val test_fn: (int -> (string * term) list option) ref
1.7 - val test_term: theory -> bool -> int -> int -> term -> (string * term) list option
1.8 - val test_term': Proof.context -> term -> int -> term list option
1.9 - val auto_quickcheck: bool ref
1.10 - val auto_quickcheck_time_limit: int ref
1.11 + val test_term: Proof.context -> term -> int -> term list option
1.12 val eval_result: (unit -> term) ref
1.13 val eval_term: theory -> term -> term
1.14 val evaluation_conv: cterm -> thm
1.15 @@ -918,7 +915,7 @@
1.16
1.17 val test_fn : (int -> (string * term) list option) ref = ref (fn _ => NONE);
1.18
1.19 -fun test_term' ctxt t =
1.20 +fun test_term ctxt t =
1.21 let
1.22 val thy = ProofContext.theory_of ctxt;
1.23 val (code, gr) = setmp mode ["term_of", "test"]
1.24 @@ -950,101 +947,6 @@
1.25 val _ = ML_Context.eval_in (SOME ctxt) false Position.none s;
1.26 in ! test_fn #> (Option.map o map) snd end;
1.27
1.28 -fun test_term thy quiet sz i t =
1.29 - let
1.30 - val ctxt = ProofContext.init thy;
1.31 - val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
1.32 - error "Term to be tested contains type variables";
1.33 - val _ = null (term_vars t) orelse
1.34 - error "Term to be tested contains schematic variables";
1.35 - val frees = map dest_Free (term_frees t);
1.36 - val frees' = frees ~~
1.37 - map (fn i => "arg" ^ string_of_int i) (1 upto length frees);
1.38 - val (code, gr) = setmp mode ["term_of", "test"]
1.39 - (generate_code_i thy [] "Generated") [("testf", list_abs_free (frees, t))];
1.40 - val s = "structure TestTerm =\nstruct\n\n" ^
1.41 - cat_lines (map snd code) ^
1.42 - "\nopen Generated;\n\n" ^ string_of
1.43 - (Pretty.block [str "val () = Codegen.test_fn :=",
1.44 - Pretty.brk 1, str ("(fn i =>"), Pretty.brk 1,
1.45 - mk_let (map (fn ((s, T), s') =>
1.46 - (mk_tuple [str s', str (s' ^ "_t")],
1.47 - Pretty.block [mk_gen gr "Generated" false [] "" T, Pretty.brk 1,
1.48 - str "i"])) frees')
1.49 - (Pretty.block [str "if ",
1.50 - mk_app false (str "testf") (map (str o snd) frees'),
1.51 - Pretty.brk 1, str "then NONE",
1.52 - Pretty.brk 1, str "else ",
1.53 - Pretty.block [str "SOME ", Pretty.block (str "[" ::
1.54 - flat (separate [str ",", Pretty.brk 1]
1.55 - (map (fn ((s, T), s') => [Pretty.block
1.56 - [str ("(" ^ quote (Symbol.escape s) ^ ","), Pretty.brk 1,
1.57 - str (s' ^ "_t ())")]]) frees')) @
1.58 - [str "]"])]]),
1.59 - str ");"]) ^
1.60 - "\n\nend;\n";
1.61 - val _ = ML_Context.eval_in (SOME ctxt) false Position.none s;
1.62 - fun iter f k = if k > i then NONE
1.63 - else (case (f () handle Match =>
1.64 - (if quiet then ()
1.65 - else warning "Exception Match raised in generated code"; NONE)) of
1.66 - NONE => iter f (k+1) | SOME x => SOME x);
1.67 - fun test k = if k > sz then NONE
1.68 - else (if quiet then () else priority ("Test data size: " ^ string_of_int k);
1.69 - case iter (fn () => !test_fn k) 1 of
1.70 - NONE => test (k+1) | SOME x => SOME x);
1.71 - in test 0 end;
1.72 -
1.73 -fun test_goal quiet ({size, iterations, default_type}, tvinsts) i assms state =
1.74 - let
1.75 - val thy = Proof.theory_of state;
1.76 - fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t
1.77 - | strip t = t;
1.78 - val (_, (_, st)) = Proof.get_goal state;
1.79 - val (gi, frees) = Logic.goal_params (prop_of st) i;
1.80 - val gi' = ObjectLogic.atomize_term thy (map_types
1.81 - (map_type_tfree (fn p as (s, S) =>
1.82 - let val T = the_default (the_default (TFree p) default_type)
1.83 - (AList.lookup (op =) tvinsts s)
1.84 - in if Sign.of_sort thy (T, S) then T
1.85 - else error ("Type " ^ Syntax.string_of_typ_global thy T ^
1.86 - " to be substituted for variable " ^
1.87 - Syntax.string_of_typ_global thy (TFree p) ^ "\ndoes not have sort " ^
1.88 - Syntax.string_of_sort_global thy S)
1.89 - end))
1.90 - (Logic.list_implies (assms, subst_bounds (frees, strip gi))));
1.91 - in test_term thy quiet size iterations gi' end;
1.92 -
1.93 -fun pretty_counterex ctxt NONE = Pretty.str "No counterexamples found."
1.94 - | pretty_counterex ctxt (SOME cex) =
1.95 - Pretty.chunks (Pretty.str "Counterexample found:\n" ::
1.96 - map (fn (s, t) =>
1.97 - Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) cex);
1.98 -
1.99 -val auto_quickcheck = ref false;
1.100 -val auto_quickcheck_time_limit = ref 5000;
1.101 -
1.102 -fun test_goal' int state =
1.103 - let
1.104 - val ctxt = Proof.context_of state;
1.105 - val assms = map term_of (Assumption.assms_of ctxt);
1.106 - val params = get_test_params (Proof.theory_of state);
1.107 - fun test () =
1.108 - let
1.109 - val res = TimeLimit.timeLimit (Time.fromMilliseconds (!auto_quickcheck_time_limit))
1.110 - (try (test_goal true (params, []) 1 assms)) state;
1.111 - in
1.112 - case res of
1.113 - NONE => state
1.114 - | SOME NONE => state
1.115 - | SOME cex => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
1.116 - Pretty.mark Markup.hilite (pretty_counterex ctxt cex)]) state
1.117 - end handle TimeLimit.TimeOut => (warning "Auto quickcheck: timeout."; state);
1.118 - in
1.119 - if int andalso !auto_quickcheck andalso not (!Toplevel.quiet)
1.120 - then test ()
1.121 - else state
1.122 - end;
1.123
1.124
1.125 (**** Evaluator for terms ****)
1.126 @@ -1165,12 +1067,10 @@
1.127 val setup = add_codegen "default" default_codegen
1.128 #> add_tycodegen "default" default_tycodegen
1.129 #> Value.add_evaluator ("SML", eval_term o ProofContext.theory_of)
1.130 - #> Quickcheck.add_generator ("SML", test_term')
1.131 + #> Quickcheck.add_generator ("SML", test_term)
1.132 #> Code.add_attribute ("unfold", Scan.succeed (Thm.declaration_attribute
1.133 (fn thm => Context.mapping (add_unfold thm #> Code.add_inline thm) I)));
1.134
1.135 -val _ = Context.>> (Specification.add_theorem_hook test_goal');
1.136 -
1.137 val _ =
1.138 OuterSyntax.command "code_library"
1.139 "generates code for terms (one structure for each theory)" K.thy_decl
1.140 @@ -1181,37 +1081,4 @@
1.141 "generates code for terms (single structure, incremental)" K.thy_decl
1.142 (parse_code false);
1.143
1.144 -val params =
1.145 - [("size", P.nat >> (K o set_size)),
1.146 - ("iterations", P.nat >> (K o set_iterations)),
1.147 - ("default_type", P.typ >> set_default_type)];
1.148 -
1.149 -val parse_test_params = P.short_ident :|-- (fn s =>
1.150 - P.$$$ "=" |-- (AList.lookup (op =) params s |> the_default Scan.fail));
1.151 -
1.152 -fun parse_tyinst xs =
1.153 - (P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn thy =>
1.154 - fn (x, ys) => (x, (v, Syntax.read_typ_global thy s) :: ys))) xs;
1.155 -
1.156 -val _ =
1.157 - OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl
1.158 - (P.$$$ "[" |-- P.list1 parse_test_params --| P.$$$ "]" >>
1.159 - (fn fs => Toplevel.theory (fn thy =>
1.160 - map_test_params (Library.apply (map (fn f => f thy) fs)) thy)));
1.161 -
1.162 -val _ =
1.163 - OuterSyntax.command "quickcheck" "try to find counterexample for subgoal" K.diag
1.164 - (Scan.option (P.$$$ "[" |-- P.list1
1.165 - ( parse_test_params >> (fn f => fn thy => apfst (f thy))
1.166 - || parse_tyinst) --| P.$$$ "]") -- Scan.optional P.nat 1 >>
1.167 - (fn (ps, g) => Toplevel.keep (fn st => Toplevel.proof_of st |>
1.168 - test_goal false (Library.apply (the_default []
1.169 - (Option.map (map (fn f => f (Toplevel.theory_of st))) ps))
1.170 - (get_test_params (Toplevel.theory_of st), [])) g [] |>
1.171 - pretty_counterex (Toplevel.context_of st) |> Pretty.writeln)));
1.172 -
1.173 end;
1.174 -
1.175 -val auto_quickcheck = Codegen.auto_quickcheck;
1.176 -val auto_quickcheck_time_limit = Codegen.auto_quickcheck_time_limit;
1.177 -