src/Pure/codegen.ML
changeset 28271 0e1b07ded55f
parent 28227 77221ee0f7b9
child 28293 f15c2e2ffe1b
     1.1 --- a/src/Pure/codegen.ML	Wed Sep 17 21:27:32 2008 +0200
     1.2 +++ b/src/Pure/codegen.ML	Wed Sep 17 21:27:34 2008 +0200
     1.3 @@ -919,6 +919,7 @@
     1.4  
     1.5  fun test_term thy quiet sz i t =
     1.6    let
     1.7 +    val ctxt = ProofContext.init thy;
     1.8      val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
     1.9        error "Term to be tested contains type variables";
    1.10      val _ = null (term_vars t) orelse
    1.11 @@ -949,7 +950,7 @@
    1.12                    [str "]"])]]),
    1.13            str ");"]) ^
    1.14        "\n\nend;\n";
    1.15 -    val _ = ML_Context.eval_in (SOME (Context.Theory thy)) false Position.none s;
    1.16 +    val _ = ML_Context.eval_in (SOME ctxt) false Position.none s;
    1.17      fun iter f k = if k > i then NONE
    1.18        else (case (f () handle Match =>
    1.19            (if quiet then ()
    1.20 @@ -1018,26 +1019,28 @@
    1.21  val eval_result = ref (fn () => Bound 0);
    1.22  
    1.23  fun eval_term thy t =
    1.24 -  let val e =
    1.25 -    let
    1.26 -      val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
    1.27 -        error "Term to be evaluated contains type variables";
    1.28 -      val _ = (null (term_vars t) andalso null (term_frees t)) orelse
    1.29 -        error "Term to be evaluated contains variables";
    1.30 -      val (code, gr) = setmp mode ["term_of"]
    1.31 -        (generate_code_i thy [] "Generated")
    1.32 -        [("result", Abs ("x", TFree ("'a", []), t))];
    1.33 -      val s = "structure EvalTerm =\nstruct\n\n" ^
    1.34 -        cat_lines (map snd code) ^
    1.35 -        "\nopen Generated;\n\n" ^ string_of
    1.36 -          (Pretty.block [str "val () = Codegen.eval_result := (fn () =>",
    1.37 -            Pretty.brk 1,
    1.38 -            mk_app false (mk_term_of gr "Generated" false (fastype_of t))
    1.39 -              [str "(result ())"],
    1.40 -            str ");"]) ^
    1.41 -        "\n\nend;\n";
    1.42 -      val _ = ML_Context.eval_in (SOME (Context.Theory thy)) false Position.none s;
    1.43 -    in !eval_result end;
    1.44 +  let
    1.45 +    val ctxt = ProofContext.init thy;
    1.46 +    val e =
    1.47 +      let
    1.48 +        val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
    1.49 +          error "Term to be evaluated contains type variables";
    1.50 +        val _ = (null (term_vars t) andalso null (term_frees t)) orelse
    1.51 +          error "Term to be evaluated contains variables";
    1.52 +        val (code, gr) = setmp mode ["term_of"]
    1.53 +          (generate_code_i thy [] "Generated")
    1.54 +          [("result", Abs ("x", TFree ("'a", []), t))];
    1.55 +        val s = "structure EvalTerm =\nstruct\n\n" ^
    1.56 +          cat_lines (map snd code) ^
    1.57 +          "\nopen Generated;\n\n" ^ string_of
    1.58 +            (Pretty.block [str "val () = Codegen.eval_result := (fn () =>",
    1.59 +              Pretty.brk 1,
    1.60 +              mk_app false (mk_term_of gr "Generated" false (fastype_of t))
    1.61 +                [str "(result ())"],
    1.62 +              str ");"]) ^
    1.63 +          "\n\nend;\n";
    1.64 +        val _ = ML_Context.eval_in (SOME ctxt) false Position.none s;
    1.65 +      in !eval_result end;
    1.66    in e () end;
    1.67  
    1.68  exception Evaluation of term;
    1.69 @@ -1110,23 +1113,22 @@
    1.70    (   Scan.repeat1 (P.name --| P.$$$ "=" -- P.term)
    1.71     || Scan.repeat1 (P.term >> pair "")) >>
    1.72    (fn ((((mode', module), opt_fname), modules), xs) => Toplevel.theory (fn thy =>
    1.73 -     let
    1.74 -       val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode');
    1.75 -       val (code, gr) = setmp mode mode'' (generate_code thy modules module) xs
    1.76 -     in ((case opt_fname of
    1.77 -         NONE =>
    1.78 -           ML_Context.eval_in (SOME (Context.Theory thy)) false Position.none
    1.79 -             (cat_lines (map snd code))
    1.80 -       | SOME fname =>
    1.81 -           if lib then
    1.82 -             app (fn (name, s) => File.write
    1.83 -                 (Path.append (Path.explode fname) (Path.basic (name ^ ".ML"))) s)
    1.84 -               (("ROOT", implode (map (fn (name, _) =>
    1.85 -                   "use \"" ^ name ^ ".ML\";\n") code)) :: code)
    1.86 -           else File.write (Path.explode fname) (snd (hd code)));
    1.87 -           if lib then thy
    1.88 -           else map_modules (Symtab.update (module, gr)) thy)
    1.89 -     end));
    1.90 +    let
    1.91 +      val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode');
    1.92 +      val (code, gr) = setmp mode mode'' (generate_code thy modules module) xs;
    1.93 +      val thy' = thy |> Context.theory_map (ML_Context.exec (fn () =>
    1.94 +        (case opt_fname of
    1.95 +          NONE => ML_Context.eval false Position.none (cat_lines (map snd code))
    1.96 +        | SOME fname =>
    1.97 +            if lib then app (fn (name, s) => File.write
    1.98 +                (Path.append (Path.explode fname) (Path.basic (name ^ ".ML"))) s)
    1.99 +              (("ROOT", implode (map (fn (name, _) =>
   1.100 +                  "use \"" ^ name ^ ".ML\";\n") code)) :: code)
   1.101 +            else File.write (Path.explode fname) (snd (hd code)))));
   1.102 +    in
   1.103 +      if lib then thy'
   1.104 +      else map_modules (Symtab.update (module, gr)) thy'
   1.105 +    end));
   1.106  
   1.107  val setup = add_codegen "default" default_codegen
   1.108    #> add_tycodegen "default" default_tycodegen