src/Pure/codegen.ML
changeset 24655 24b630fd008f
parent 24634 38db11874724
child 24688 a5754ca5c510
     1.1 --- a/src/Pure/codegen.ML	Thu Sep 20 12:10:23 2007 +0200
     1.2 +++ b/src/Pure/codegen.ML	Thu Sep 20 16:23:12 2007 +0200
     1.3 @@ -75,7 +75,8 @@
     1.4    val test_fn: (int -> (string * term) list option) ref
     1.5    val test_term: theory -> bool -> int -> int -> term -> (string * term) list option
     1.6    val auto_quickcheck: bool ref
     1.7 -  val eval_result: term ref
     1.8 +  val auto_quickcheck_time_limit: Time.time ref
     1.9 +  val eval_result: (unit -> term) ref
    1.10    val eval_term: theory -> term -> term
    1.11    val evaluation_conv: cterm -> thm
    1.12    val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list
    1.13 @@ -945,7 +946,7 @@
    1.14                    [Pretty.str "]"])]],
    1.15              Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"]) ^
    1.16        "\n\nend;\n") ();
    1.17 -    val _ = use_text "" (K (), error) false s;
    1.18 +    val _ = ML_Context.use_mltext s false (SOME (Context.Theory thy));
    1.19      fun iter f k = if k > i then NONE
    1.20        else (case (f () handle Match =>
    1.21            (if quiet then ()
    1.22 @@ -965,9 +966,15 @@
    1.23      val (_, (_, st)) = Proof.get_goal state;
    1.24      val (gi, frees) = Logic.goal_params (prop_of st) i;
    1.25      val gi' = ObjectLogic.atomize_term thy (map_types
    1.26 -      (map_type_tfree (fn p as (s, _) =>
    1.27 -        the_default (the_default (TFree p) default_type)
    1.28 -          (AList.lookup (op =) tvinsts s)))
    1.29 +      (map_type_tfree (fn p as (s, S) =>
    1.30 +        let val T = the_default (the_default (TFree p) default_type)
    1.31 +          (AList.lookup (op =) tvinsts s)
    1.32 +        in if Sign.of_sort thy (T, S) then T
    1.33 +          else error ("Type " ^ Sign.string_of_typ thy T ^
    1.34 +            " to be substituted for variable " ^
    1.35 +            Sign.string_of_typ thy (TFree p) ^ "\ndoes not have sort " ^
    1.36 +            Sign.string_of_sort thy S)
    1.37 +        end))
    1.38        (Logic.list_implies (assms, subst_bounds (frees, strip gi))));
    1.39    in test_term thy quiet size iterations gi' end;
    1.40  
    1.41 @@ -979,22 +986,24 @@
    1.42              ProofContext.pretty_term ctxt t]) cex);
    1.43  
    1.44  val auto_quickcheck = ref true;
    1.45 +val auto_quickcheck_time_limit = ref (Time.fromSeconds 5);
    1.46  
    1.47  fun test_goal' int state =
    1.48    let
    1.49      val ctxt = Proof.context_of state;
    1.50      val assms = map term_of (Assumption.assms_of ctxt)
    1.51 +    val params = get_test_params (Proof.theory_of state)
    1.52    in
    1.53      if int andalso !auto_quickcheck andalso not (!Toplevel.quiet)
    1.54      then
    1.55 -      (case try (test_goal true
    1.56 -           (get_test_params (Proof.theory_of state), []) 1 assms) state of
    1.57 +      (case try (fn state => interrupt_timeout (!auto_quickcheck_time_limit)
    1.58 +           (test_goal true (params, []) 1 assms) state) state of
    1.59           SOME (cex as SOME _) =>
    1.60             Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
    1.61               Pretty.markup Markup.hilite [pretty_counterex ctxt cex]]) state
    1.62         | _ => state)
    1.63      else state
    1.64 -  end;
    1.65 +  end handle Interrupt => state;
    1.66  
    1.67  val _ = Context.add_setup
    1.68    (Context.theory_map (Specification.add_theorem_hook test_goal'));
    1.69 @@ -1002,7 +1011,7 @@
    1.70  
    1.71  (**** Evaluator for terms ****)
    1.72  
    1.73 -val eval_result = ref (Bound 0);
    1.74 +val eval_result = ref (fn () => Bound 0);
    1.75  
    1.76  fun eval_term thy = PrintMode.setmp [] (fn t =>
    1.77    let
    1.78 @@ -1011,18 +1020,19 @@
    1.79      val _ = (null (term_vars t) andalso null (term_frees t)) orelse
    1.80        error "Term to be evaluated contains variables";
    1.81      val (code, gr) = setmp mode ["term_of"]
    1.82 -      (generate_code_i thy [] "Generated") [("result", t)];
    1.83 +      (generate_code_i thy [] "Generated")
    1.84 +      [("result", Abs ("x", TFree ("'a", []), t))];
    1.85      val s = "structure EvalTerm =\nstruct\n\n" ^
    1.86        space_implode "\n" (map snd code) ^
    1.87        "\nopen Generated;\n\n" ^ Pretty.string_of
    1.88 -        (Pretty.block [Pretty.str "val () = Codegen.eval_result :=",
    1.89 +        (Pretty.block [Pretty.str "val () = Codegen.eval_result := (fn () =>",
    1.90            Pretty.brk 1,
    1.91            mk_app false (mk_term_of gr "Generated" false (fastype_of t))
    1.92 -            [Pretty.str "result"],
    1.93 -          Pretty.str ";"])  ^
    1.94 +            [Pretty.str "(result ())"],
    1.95 +          Pretty.str ");"]) ^
    1.96        "\n\nend;\n";
    1.97 -    val _ = use_text "" Output.ml_output false s
    1.98 -  in !eval_result end);
    1.99 +    val _ = ML_Context.use_mltext s false (SOME (Context.Theory thy))
   1.100 +  in !eval_result () end);
   1.101  
   1.102  fun print_evaluated_term s = Toplevel.keep (fn state =>
   1.103    let
   1.104 @@ -1128,8 +1138,8 @@
   1.105         val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode');
   1.106         val (code, gr) = setmp mode mode'' (generate_code thy modules module) xs
   1.107       in ((case opt_fname of
   1.108 -         NONE => use_text "" Output.ml_output false
   1.109 -           (space_implode "\n" (map snd code))
   1.110 +         NONE => ML_Context.use_mltext (space_implode "\n" (map snd code))
   1.111 +           false (SOME (Context.Theory thy))
   1.112         | SOME fname =>
   1.113             if lib then
   1.114               app (fn (name, s) => File.write