prefer proof context over background theory
authorhaftmann
Wed Feb 26 11:57:52 2014 +0100 (2014-02-26)
changeset 557579fc71814b8c1
parent 55756 565a20b22f09
child 55758 385f7573f8f5
prefer proof context over background theory
NEWS
src/Doc/Codegen/Further.thy
src/HOL/HOL.thy
src/HOL/Library/Code_Abstract_Nat.thy
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/Quickcheck/random_generators.ML
src/HOL/Tools/code_evaluation.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_runtime.ML
src/Tools/Code/code_simp.ML
src/Tools/Code/code_target.ML
src/Tools/Code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/NEWS	Wed Feb 26 10:10:38 2014 +0100
     1.2 +++ b/NEWS	Wed Feb 26 11:57:52 2014 +0100
     1.3 @@ -91,9 +91,14 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Code generator: explicit proof contexts in many ML interfaces.
     1.8 +INCOMPATIBILITY.
     1.9 +
    1.10  * Code generator: minimize exported identifiers by default.
    1.11 +Minor INCOMPATIBILITY.
    1.12  
    1.13  * Code generation for SML and OCaml: dropped arcane "no_signatures" option.
    1.14 +Minor INCOMPATIBILITY.
    1.15  
    1.16  * Simproc "finite_Collect" is no longer enabled by default, due to
    1.17  spurious crashes and other surprises.  Potential INCOMPATIBILITY.
     2.1 --- a/src/Doc/Codegen/Further.thy	Wed Feb 26 10:10:38 2014 +0100
     2.2 +++ b/src/Doc/Codegen/Further.thy	Wed Feb 26 11:57:52 2014 +0100
     2.3 @@ -258,7 +258,7 @@
     2.4    @{index_ML Code_Preproc.map_pre: "(Proof.context -> Proof.context) -> theory -> theory"} \\
     2.5    @{index_ML Code_Preproc.map_post: "(Proof.context -> Proof.context) -> theory -> theory"} \\
     2.6    @{index_ML Code_Preproc.add_functrans: "
     2.7 -    string * (theory -> (thm * bool) list -> (thm * bool) list option)
     2.8 +    string * (Proof.context -> (thm * bool) list -> (thm * bool) list option)
     2.9        -> theory -> theory"} \\
    2.10    @{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\
    2.11    @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\
     3.1 --- a/src/HOL/HOL.thy	Wed Feb 26 10:10:38 2014 +0100
     3.2 +++ b/src/HOL/HOL.thy	Wed Feb 26 11:57:52 2014 +0100
     3.3 @@ -1903,20 +1903,21 @@
     3.4  
     3.5  subsubsection {* Evaluation and normalization by evaluation *}
     3.6  
     3.7 -ML {*
     3.8 -fun eval_tac ctxt =
     3.9 -  let val conv = Code_Runtime.dynamic_holds_conv (Proof_Context.theory_of ctxt)
    3.10 -  in CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN' rtac TrueI end
    3.11 -*}
    3.12 -
    3.13 -method_setup eval = {* Scan.succeed (SIMPLE_METHOD' o eval_tac) *}
    3.14 -  "solve goal by evaluation"
    3.15 +method_setup eval = {*
    3.16 +let
    3.17 +  fun eval_tac ctxt =
    3.18 +    let val conv = Code_Runtime.dynamic_holds_conv ctxt
    3.19 +    in CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN' rtac TrueI end
    3.20 +in
    3.21 +  Scan.succeed (SIMPLE_METHOD' o eval_tac)
    3.22 +end
    3.23 +*} "solve goal by evaluation"
    3.24  
    3.25  method_setup normalization = {*
    3.26    Scan.succeed (fn ctxt =>
    3.27      SIMPLE_METHOD'
    3.28        (CHANGED_PROP o
    3.29 -        (CONVERSION (Nbe.dynamic_conv (Proof_Context.theory_of ctxt))
    3.30 +        (CONVERSION (Nbe.dynamic_conv ctxt)
    3.31            THEN_ALL_NEW (TRY o rtac TrueI))))
    3.32  *} "solve goal by normalization"
    3.33  
     4.1 --- a/src/HOL/Library/Code_Abstract_Nat.thy	Wed Feb 26 10:10:38 2014 +0100
     4.2 +++ b/src/HOL/Library/Code_Abstract_Nat.thy	Wed Feb 26 11:57:52 2014 +0100
     4.3 @@ -50,8 +50,9 @@
     4.4  setup {*
     4.5  let
     4.6  
     4.7 -fun remove_suc thy thms =
     4.8 +fun remove_suc ctxt thms =
     4.9    let
    4.10 +    val thy = Proof_Context.theory_of ctxt;
    4.11      val vname = singleton (Name.variant_list (map fst
    4.12        (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
    4.13      val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
     5.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Feb 26 10:10:38 2014 +0100
     5.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Feb 26 11:57:52 2014 +0100
     5.3 @@ -1914,7 +1914,7 @@
     5.4            in
     5.5              rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Limited_Sequence.yieldn k
     5.6                (Code_Runtime.dynamic_value_strict (Dseq_Random_Result.get, put_dseq_random_result, "Predicate_Compile_Core.put_dseq_random_result")
     5.7 -                thy NONE (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> Limited_Sequence.map proc)
     5.8 +                ctxt NONE (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> Limited_Sequence.map proc)
     5.9                    t' [] nrandom size
    5.10                  |> Random_Engine.run)
    5.11                depth true)) ())
    5.12 @@ -1922,14 +1922,14 @@
    5.13        | DSeq =>
    5.14            rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Limited_Sequence.yieldn k
    5.15              (Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
    5.16 -              thy NONE Limited_Sequence.map t' []) (Code_Numeral.natural_of_integer (the_single arguments)) true)) ())
    5.17 +              ctxt NONE Limited_Sequence.map t' []) (Code_Numeral.natural_of_integer (the_single arguments)) true)) ())
    5.18        | Pos_Generator_DSeq =>
    5.19            let
    5.20              val depth = Code_Numeral.natural_of_integer (the_single arguments)
    5.21            in
    5.22              rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Lazy_Sequence.yieldn k
    5.23                (Code_Runtime.dynamic_value_strict (New_Dseq_Result.get, put_new_dseq_result, "Predicate_Compile_Core.put_new_dseq_result")
    5.24 -              thy NONE (fn proc => fn g => fn depth => g depth |> Lazy_Sequence.map proc)
    5.25 +              ctxt NONE (fn proc => fn g => fn depth => g depth |> Lazy_Sequence.map proc)
    5.26                t' [] depth))) ())
    5.27            end
    5.28        | New_Pos_Random_DSeq =>
    5.29 @@ -1943,7 +1943,7 @@
    5.30                (fn () => fst (Lazy_Sequence.yieldn k
    5.31                  (Code_Runtime.dynamic_value_strict
    5.32                    (Lseq_Random_Stats_Result.get, put_lseq_random_stats_result, "Predicate_Compile_Core.put_lseq_random_stats_result")
    5.33 -                  thy NONE
    5.34 +                  ctxt NONE
    5.35                    (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
    5.36                      |> Lazy_Sequence.map (apfst proc))
    5.37                      t' [] nrandom size seed depth))) ()))
    5.38 @@ -1951,7 +1951,7 @@
    5.39                (TimeLimit.timeLimit time_limit (fn () => fst (Lazy_Sequence.yieldn k
    5.40                  (Code_Runtime.dynamic_value_strict
    5.41                    (Lseq_Random_Result.get, put_lseq_random_result, "Predicate_Compile_Core.put_lseq_random_result")
    5.42 -                  thy NONE
    5.43 +                  ctxt NONE
    5.44                    (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
    5.45                      |> Lazy_Sequence.map proc)
    5.46                      t' [] nrandom size seed depth))) ())
    5.47 @@ -1959,7 +1959,7 @@
    5.48        | _ =>
    5.49            rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Predicate.yieldn k
    5.50              (Code_Runtime.dynamic_value_strict (Pred_Result.get, put_pred_result, "Predicate_Compile_Core.put_pred_result")
    5.51 -              thy NONE Predicate.map t' []))) ()))
    5.52 +              ctxt NONE Predicate.map t' []))) ()))
    5.53       handle TimeLimit.TimeOut => error "Reached timeout during execution of values"
    5.54    in ((T, ts), statistics) end;
    5.55  
     6.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Feb 26 10:10:38 2014 +0100
     6.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Feb 26 11:57:52 2014 +0100
     6.3 @@ -296,7 +296,7 @@
     6.4            let
     6.5              val compiled_term =
     6.6                Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Quickcheck.put_dseq_result")
     6.7 -                thy4 (SOME target)
     6.8 +                (Proof_Context.init_global thy4) (SOME target)
     6.9                  (fn proc => fn g => fn n => fn size => fn s => g n size s |>> (Limited_Sequence.map o map) proc)
    6.10                  qc_term []
    6.11            in
    6.12 @@ -309,7 +309,7 @@
    6.13              val compiled_term =
    6.14                Code_Runtime.dynamic_value_strict
    6.15                  (Lseq_Result.get, put_lseq_result, "Predicate_Compile_Quickcheck.put_lseq_result")
    6.16 -                thy4 (SOME target)
    6.17 +                (Proof_Context.init_global thy4) (SOME target)
    6.18                  (fn proc => fn g => fn nrandom => fn size => fn s => fn depth =>
    6.19                    g nrandom size s depth |> (Lazy_Sequence.map o map) proc)
    6.20                    qc_term []
    6.21 @@ -325,7 +325,7 @@
    6.22              val compiled_term =
    6.23                Code_Runtime.dynamic_value_strict
    6.24                  (New_Dseq_Result.get, put_new_dseq_result, "Predicate_Compile_Quickcheck.put_new_dseq_result")
    6.25 -                thy4 (SOME target)
    6.26 +                (Proof_Context.init_global thy4) (SOME target)
    6.27                  (fn proc => fn g => fn depth => g depth |> (Lazy_Sequence.map o map) proc)
    6.28                  qc_term []
    6.29            in
    6.30 @@ -336,7 +336,7 @@
    6.31              val compiled_term =
    6.32                Code_Runtime.dynamic_value_strict
    6.33                  (CPS_Result.get, put_cps_result, "Predicate_Compile_Quickcheck.put_cps_result")
    6.34 -                thy4 (SOME target)
    6.35 +                (Proof_Context.init_global thy4) (SOME target)
    6.36                  (fn proc => fn g => fn depth => g depth |> Option.map (apsnd (map proc)))
    6.37                  qc_term []
    6.38            in
    6.39 @@ -346,7 +346,7 @@
    6.40            let
    6.41              val compiled_term = Code_Runtime.dynamic_value_strict
    6.42                (Pred_Result.get, put_pred_result, "Predicate_Compile_Quickcheck.put_pred_result")
    6.43 -                thy4 (SOME target) (fn proc => fn g => fn depth => fn nrandom => fn size => fn seed =>
    6.44 +                (Proof_Context.init_global thy4) (SOME target) (fn proc => fn g => fn depth => fn nrandom => fn size => fn seed =>
    6.45                    g depth nrandom size seed |> (Predicate.map o map) proc)
    6.46                  qc_term []
    6.47            in
     7.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Wed Feb 26 10:10:38 2014 +0100
     7.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Wed Feb 26 11:57:52 2014 +0100
     7.3 @@ -471,7 +471,6 @@
     7.4  
     7.5  fun compile_generator_expr_raw ctxt ts =
     7.6    let
     7.7 -    val thy = Proof_Context.theory_of ctxt
     7.8      val mk_generator_expr = 
     7.9        if Config.get ctxt fast then mk_fast_generator_expr
    7.10        else if Config.get ctxt bounded_forall then mk_bounded_forall_generator_expr
    7.11 @@ -479,7 +478,7 @@
    7.12      val t' = mk_parametric_generator_expr mk_generator_expr ctxt ts;
    7.13      val compile = Code_Runtime.dynamic_value_strict
    7.14        (Counterexample.get, put_counterexample, "Exhaustive_Generators.put_counterexample")
    7.15 -      thy (SOME target) (fn proc => fn g =>
    7.16 +      ctxt (SOME target) (fn proc => fn g =>
    7.17          fn card => fn genuine_only => fn size => g card genuine_only size
    7.18            |> (Option.map o apsnd o map) proc) t' []
    7.19    in
    7.20 @@ -497,12 +496,11 @@
    7.21  
    7.22  fun compile_generator_exprs_raw ctxt ts =
    7.23    let
    7.24 -    val thy = Proof_Context.theory_of ctxt
    7.25      val ts' = map (fn t => mk_generator_expr ctxt (t, [])) ts;
    7.26      val compiles = Code_Runtime.dynamic_value_strict
    7.27        (Counterexample_Batch.get, put_counterexample_batch,
    7.28          "Exhaustive_Generators.put_counterexample_batch")
    7.29 -      thy (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc))
    7.30 +      ctxt (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc))
    7.31        (HOLogic.mk_list @{typ "natural => term list option"} ts') []
    7.32    in
    7.33      map (fn compile => fn size => compile size
    7.34 @@ -515,12 +513,11 @@
    7.35  
    7.36  fun compile_validator_exprs_raw ctxt ts =
    7.37    let
    7.38 -    val thy = Proof_Context.theory_of ctxt
    7.39      val ts' = map (mk_validator_expr ctxt) ts
    7.40    in
    7.41      Code_Runtime.dynamic_value_strict
    7.42        (Validator_Batch.get, put_validator_batch, "Exhaustive_Generators.put_validator_batch")
    7.43 -      thy (SOME target) (K I) (HOLogic.mk_list @{typ "natural => bool"} ts') []
    7.44 +      ctxt (SOME target) (K I) (HOLogic.mk_list @{typ "natural => bool"} ts') []
    7.45    end;
    7.46  
    7.47  fun compile_validator_exprs ctxt ts =
     8.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Feb 26 10:10:38 2014 +0100
     8.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Feb 26 11:57:52 2014 +0100
     8.3 @@ -303,13 +303,12 @@
     8.4      with_tmp_dir tmp_prefix run
     8.5    end;
     8.6  
     8.7 -fun dynamic_value_strict opts cookie thy postproc t =
     8.8 +fun dynamic_value_strict opts cookie ctxt postproc t =
     8.9    let
    8.10 -    val ctxt = Proof_Context.init_global thy
    8.11      fun evaluator program ((_, vs_ty), t) deps =
    8.12        Exn.interruptible_capture (value opts ctxt cookie)
    8.13 -        (Code_Target.evaluator thy target program deps true (vs_ty, t));
    8.14 -  in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
    8.15 +        (Code_Target.evaluator ctxt target program deps true (vs_ty, t));
    8.16 +  in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_result o postproc) evaluator t) end;
    8.17  
    8.18  (** counterexample generator **)
    8.19  
    8.20 @@ -462,7 +461,7 @@
    8.21          val execute = dynamic_value_strict (true, opts)
    8.22            ((K true, fn _ => error ""), (Existential_Counterexample.get, Existential_Counterexample.put,
    8.23              "Narrowing_Generators.put_existential_counterexample"))
    8.24 -          thy (apfst o Option.map o map_counterexample)
    8.25 +          ctxt (apfst o Option.map o map_counterexample)
    8.26        in  
    8.27          case act execute (mk_property qs prop_t) of 
    8.28            SOME (counterexample, result) => Quickcheck.Result
    8.29 @@ -488,7 +487,7 @@
    8.30          val execute = dynamic_value_strict (false, opts)
    8.31            ((is_genuine, counterexample_of),
    8.32              (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample"))
    8.33 -          thy (apfst o Option.map o apsnd o map)
    8.34 +          ctxt (apfst o Option.map o apsnd o map)
    8.35        in
    8.36          case act execute (ensure_testable (finitize t')) of 
    8.37            SOME (counterexample, result) =>
     9.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Feb 26 10:10:38 2014 +0100
     9.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Feb 26 11:57:52 2014 +0100
     9.3 @@ -406,7 +406,6 @@
     9.4      
     9.5  fun compile_generator_expr_raw ctxt ts =
     9.6    let
     9.7 -    val thy = Proof_Context.theory_of ctxt
     9.8      val iterations = Config.get ctxt Quickcheck.iterations
     9.9    in
    9.10      if Config.get ctxt Quickcheck.report then
    9.11 @@ -414,7 +413,7 @@
    9.12          val t' = mk_parametric_reporting_generator_expr ctxt ts;
    9.13          val compile = Code_Runtime.dynamic_value_strict
    9.14            (Counterexample_Report.get, put_counterexample_report, "Random_Generators.put_counterexample_report")
    9.15 -          thy (SOME target)
    9.16 +          ctxt (SOME target)
    9.17            (fn proc => fn g => fn c => fn b => fn s => g c b s
    9.18              #>> (apfst o Option.map o apsnd o map) proc) t' [];
    9.19          fun single_tester c b s = compile c b s |> Random_Engine.run
    9.20 @@ -436,7 +435,7 @@
    9.21          val t' = mk_parametric_generator_expr ctxt ts;
    9.22          val compile = Code_Runtime.dynamic_value_strict
    9.23            (Counterexample.get, put_counterexample, "Random_Generators.put_counterexample")
    9.24 -          thy (SOME target)
    9.25 +          ctxt (SOME target)
    9.26            (fn proc => fn g => fn c => fn b => fn s => g c b s
    9.27              #>> (Option.map o apsnd o map) proc) t' [];
    9.28          fun single_tester c b s = compile c b s |> Random_Engine.run
    10.1 --- a/src/HOL/Tools/code_evaluation.ML	Wed Feb 26 10:10:38 2014 +0100
    10.2 +++ b/src/HOL/Tools/code_evaluation.ML	Wed Feb 26 11:57:52 2014 +0100
    10.3 @@ -6,14 +6,14 @@
    10.4  
    10.5  signature CODE_EVALUATION =
    10.6  sig
    10.7 -  val dynamic_value: theory -> term -> term option
    10.8 -  val dynamic_value_strict: theory -> term -> term
    10.9 -  val dynamic_value_exn: theory -> term -> term Exn.result
   10.10 -  val static_value: theory -> string list -> typ list -> term -> term option
   10.11 -  val static_value_strict: theory -> string list -> typ list -> term -> term
   10.12 -  val static_value_exn: theory -> string list -> typ list -> term -> term Exn.result
   10.13 -  val dynamic_conv: theory -> conv
   10.14 -  val static_conv: theory -> string list -> typ list -> conv
   10.15 +  val dynamic_value: Proof.context -> term -> term option
   10.16 +  val dynamic_value_strict: Proof.context -> term -> term
   10.17 +  val dynamic_value_exn: Proof.context -> term -> term Exn.result
   10.18 +  val static_value: Proof.context -> string list -> typ list -> Proof.context -> term -> term option
   10.19 +  val static_value_strict: Proof.context -> string list -> typ list -> Proof.context -> term -> term
   10.20 +  val static_value_exn: Proof.context -> string list -> typ list -> Proof.context -> term -> term Exn.result
   10.21 +  val dynamic_conv: Proof.context -> conv
   10.22 +  val static_conv: Proof.context -> string list -> typ list -> Proof.context -> conv
   10.23    val put_term: (unit -> term) -> Proof.context -> Proof.context
   10.24    val tracing: string -> 'a -> 'a
   10.25    val setup: theory -> theory
   10.26 @@ -171,44 +171,48 @@
   10.27  
   10.28  fun term_of_const_for thy = Axclass.unoverload_const thy o dest_Const o HOLogic.term_of_const;
   10.29  
   10.30 -fun gen_dynamic_value dynamic_value thy t =
   10.31 -  dynamic_value cookie thy NONE I (mk_term_of t) [];
   10.32 +fun gen_dynamic_value dynamic_value ctxt t =
   10.33 +  dynamic_value cookie ctxt NONE I (mk_term_of t) [];
   10.34  
   10.35  val dynamic_value = gen_dynamic_value Code_Runtime.dynamic_value;
   10.36  val dynamic_value_strict = gen_dynamic_value Code_Runtime.dynamic_value_strict;
   10.37  val dynamic_value_exn = gen_dynamic_value Code_Runtime.dynamic_value_exn;
   10.38  
   10.39 -fun gen_static_value static_value thy consts Ts =
   10.40 -  static_value cookie thy NONE I (union (op =) (map (term_of_const_for thy) Ts) consts)
   10.41 -  o mk_term_of;
   10.42 +fun gen_static_value static_value ctxt consts Ts =
   10.43 +  let
   10.44 +    val static_value' = static_value cookie ctxt NONE I
   10.45 +      (union (op =) (map (term_of_const_for (Proof_Context.theory_of ctxt)) Ts) consts)
   10.46 +  in fn ctxt' => fn t => static_value' ctxt' (mk_term_of t) end;
   10.47  
   10.48  val static_value = gen_static_value Code_Runtime.static_value;
   10.49  val static_value_strict = gen_static_value Code_Runtime.static_value_strict;
   10.50  val static_value_exn = gen_static_value Code_Runtime.static_value_exn;
   10.51  
   10.52 -fun certify_eval thy value conv ct =
   10.53 +fun certify_eval ctxt value conv ct =
   10.54    let
   10.55 +    val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
   10.56      val t = Thm.term_of ct;
   10.57      val T = fastype_of t;
   10.58 -    val mk_eq = Thm.mk_binop (Thm.cterm_of thy (Const ("==", T --> T --> propT)));
   10.59 -  in case value t
   10.60 +    val mk_eq = Thm.mk_binop (cert (Const ("==", T --> T --> propT)));
   10.61 +  in case value ctxt t
   10.62     of NONE => Thm.reflexive ct
   10.63 -    | SOME t' => conv (mk_eq ct (Thm.cterm_of thy t')) RS @{thm eq_eq_TrueD}
   10.64 +    | SOME t' => conv ctxt (mk_eq ct (cert t')) RS @{thm eq_eq_TrueD}
   10.65          handle THM _ =>
   10.66 -          error ("Failed to certify evaluation result of " ^ Syntax.string_of_term_global thy t)
   10.67 +          error ("Failed to certify evaluation result of " ^ Syntax.string_of_term ctxt t)
   10.68    end;
   10.69  
   10.70 -fun dynamic_conv thy = certify_eval thy (dynamic_value thy)
   10.71 -  (Code_Runtime.dynamic_holds_conv thy);
   10.72 +fun dynamic_conv ctxt = certify_eval ctxt dynamic_value
   10.73 +  Code_Runtime.dynamic_holds_conv;
   10.74  
   10.75 -fun static_conv thy consts Ts =
   10.76 +fun static_conv ctxt consts Ts =
   10.77    let
   10.78      val eqs = "==" :: @{const_name HOL.eq} ::
   10.79 -      map (fn T => Axclass.unoverload_const thy (@{const_name HOL.equal}, T)) Ts;
   10.80 -        (*assumes particular code equations for "==" etc.*)
   10.81 +      map (fn T => Axclass.unoverload_const (Proof_Context.theory_of ctxt)
   10.82 +        (@{const_name HOL.equal}, T)) Ts; (*assumes particular code equations for "==" etc.*)
   10.83 +    val value = static_value ctxt consts Ts;
   10.84 +    val holds = Code_Runtime.static_holds_conv ctxt (union (op =) eqs consts);
   10.85    in
   10.86 -    certify_eval thy (static_value thy consts Ts)
   10.87 -      (Code_Runtime.static_holds_conv thy (union (op =) eqs consts))
   10.88 +    fn ctxt' => certify_eval ctxt' value holds
   10.89    end;
   10.90  
   10.91  
   10.92 @@ -225,6 +229,6 @@
   10.93    #> Code.datatype_interpretation ensure_term_of_code
   10.94    #> Code.abstype_interpretation ensure_abs_term_of_code
   10.95    #> Context.theory_map (Syntax_Phases.term_check 0 "termify" check_termify)
   10.96 -  #> Value.add_evaluator ("code", dynamic_value_strict o Proof_Context.theory_of);
   10.97 +  #> Value.add_evaluator ("code", dynamic_value_strict);
   10.98  
   10.99  end;
    11.1 --- a/src/Tools/Code/code_preproc.ML	Wed Feb 26 10:10:38 2014 +0100
    11.2 +++ b/src/Tools/Code/code_preproc.ML	Wed Feb 26 11:57:52 2014 +0100
    11.3 @@ -10,27 +10,29 @@
    11.4    val map_pre: (Proof.context -> Proof.context) -> theory -> theory
    11.5    val map_post: (Proof.context -> Proof.context) -> theory -> theory
    11.6    val add_unfold: thm -> theory -> theory
    11.7 -  val add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory
    11.8 +  val add_functrans: string * (Proof.context -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory
    11.9    val del_functrans: string -> theory -> theory
   11.10 -  val simple_functrans: (theory -> thm list -> thm list option)
   11.11 -    -> theory -> (thm * bool) list -> (thm * bool) list option
   11.12 -  val print_codeproc: theory -> unit
   11.13 +  val simple_functrans: (Proof.context -> thm list -> thm list option)
   11.14 +    -> Proof.context -> (thm * bool) list -> (thm * bool) list option
   11.15 +  val print_codeproc: Proof.context -> unit
   11.16  
   11.17    type code_algebra
   11.18    type code_graph
   11.19    val cert: code_graph -> string -> Code.cert
   11.20    val sortargs: code_graph -> string -> sort list
   11.21    val all: code_graph -> string list
   11.22 -  val pretty: theory -> code_graph -> Pretty.T
   11.23 +  val pretty: Proof.context -> code_graph -> Pretty.T
   11.24    val obtain: bool -> theory -> string list -> term list -> code_algebra * code_graph
   11.25 -  val dynamic_conv: theory
   11.26 +  val dynamic_conv: Proof.context
   11.27      -> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
   11.28 -  val dynamic_value: theory -> ((term -> term) -> 'a -> 'a)
   11.29 +  val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'a)
   11.30      -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
   11.31 -  val static_conv: theory -> string list
   11.32 -    -> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
   11.33 -  val static_value: theory -> ((term -> term) -> 'a -> 'a) -> string list
   11.34 -    -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
   11.35 +  val static_conv: Proof.context -> string list
   11.36 +    -> (code_algebra -> code_graph -> Proof.context -> (string * sort) list -> term -> conv)
   11.37 +    -> Proof.context -> conv
   11.38 +  val static_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> string list
   11.39 +    -> (code_algebra -> code_graph -> Proof.context -> (string * sort) list -> term -> 'a)
   11.40 +    -> Proof.context -> term -> 'a
   11.41  
   11.42    val setup: theory -> theory
   11.43  end
   11.44 @@ -45,7 +47,7 @@
   11.45  datatype thmproc = Thmproc of {
   11.46    pre: simpset,
   11.47    post: simpset,
   11.48 -  functrans: (string * (serial * (theory -> (thm * bool) list -> (thm * bool) list option))) list
   11.49 +  functrans: (string * (serial * (Proof.context -> (thm * bool) list -> (thm * bool) list option))) list
   11.50  };
   11.51  
   11.52  fun make_thmproc ((pre, post), functrans) =
   11.53 @@ -110,9 +112,10 @@
   11.54  
   11.55  (* post- and preprocessing *)
   11.56  
   11.57 -fun no_variables_conv conv ct =
   11.58 +fun no_variables_conv ctxt conv ct =
   11.59    let
   11.60 -    val cert = Thm.cterm_of (Thm.theory_of_cterm ct);
   11.61 +    val thy = Proof_Context.theory_of ctxt;
   11.62 +    val cert = Thm.cterm_of thy;
   11.63      val all_vars = fold_aterms (fn t as Free _ => insert (op aconvc) (cert t)
   11.64        | t as Var _ => insert (op aconvc) (cert t)
   11.65        | _ => I) (Thm.term_of ct) [];
   11.66 @@ -128,48 +131,52 @@
   11.67  
   11.68  fun trans_conv_rule conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
   11.69  
   11.70 -fun term_of_conv thy conv =
   11.71 -  Thm.cterm_of thy
   11.72 -  #> conv
   11.73 +fun term_of_conv ctxt conv =
   11.74 +  Thm.cterm_of (Proof_Context.theory_of ctxt)
   11.75 +  #> conv ctxt
   11.76    #> Thm.prop_of
   11.77    #> Logic.dest_equals
   11.78    #> snd;
   11.79  
   11.80 -fun term_of_conv_resubst thy conv t =
   11.81 +fun term_of_conv_resubst ctxt conv t =
   11.82    let
   11.83      val all_vars = fold_aterms (fn t as Free _ => insert (op aconv) t
   11.84        | t as Var _ => insert (op aconv) t
   11.85        | _ => I) t [];
   11.86      val resubst = curry (Term.betapplys o swap) all_vars;
   11.87 -  in (resubst, term_of_conv thy conv (fold_rev lambda all_vars t)) end;
   11.88 -
   11.89 -fun global_simpset_context thy ss =
   11.90 -  Proof_Context.init_global thy
   11.91 -  |> put_simpset ss;
   11.92 +  in (resubst, term_of_conv ctxt conv (fold_rev lambda all_vars t)) end;
   11.93  
   11.94 -fun preprocess_conv thy =
   11.95 +fun preprocess_conv ctxt =
   11.96    let
   11.97 -    val pre = global_simpset_context thy ((#pre o the_thmproc) thy);
   11.98 -  in
   11.99 -    Simplifier.rewrite pre
  11.100 -    #> trans_conv_rule (Axclass.unoverload_conv thy)
  11.101 +    val thy = Proof_Context.theory_of ctxt;
  11.102 +    val ss = (#pre o the_thmproc) thy;
  11.103 +  in fn ctxt' =>
  11.104 +    Simplifier.rewrite (put_simpset ss ctxt')
  11.105 +    #> trans_conv_rule (Axclass.unoverload_conv (Proof_Context.theory_of ctxt'))
  11.106    end;
  11.107  
  11.108 -fun preprocess_term thy = term_of_conv_resubst thy (preprocess_conv thy);
  11.109 -
  11.110 -fun postprocess_conv thy =
  11.111 +fun preprocess_term ctxt =
  11.112    let
  11.113 -    val post = global_simpset_context thy ((#post o the_thmproc) thy);
  11.114 -  in
  11.115 -    Axclass.overload_conv thy
  11.116 -    #> trans_conv_rule (Simplifier.rewrite post)
  11.117 +    val conv = preprocess_conv ctxt;
  11.118 +  in fn ctxt' => term_of_conv_resubst ctxt' conv end;
  11.119 +
  11.120 +fun postprocess_conv ctxt =
  11.121 +  let
  11.122 +    val thy = Proof_Context.theory_of ctxt;
  11.123 +    val ss = (#post o the_thmproc) thy;
  11.124 +  in fn ctxt' =>
  11.125 +    Axclass.overload_conv (Proof_Context.theory_of ctxt')
  11.126 +    #> trans_conv_rule (Simplifier.rewrite (put_simpset ss ctxt'))
  11.127    end;
  11.128  
  11.129 -fun postprocess_term thy = term_of_conv thy (postprocess_conv thy);
  11.130 +fun postprocess_term ctxt =
  11.131 +  let
  11.132 +    val conv = postprocess_conv ctxt;
  11.133 +  in fn ctxt' => term_of_conv ctxt' conv end;
  11.134  
  11.135 -fun print_codeproc thy =
  11.136 +fun print_codeproc ctxt =
  11.137    let
  11.138 -    val ctxt = Proof_Context.init_global thy;
  11.139 +    val thy = Proof_Context.theory_of ctxt;
  11.140      val pre = (#pre o the_thmproc) thy;
  11.141      val post = (#post o the_thmproc) thy;
  11.142      val functrans = (map fst o #functrans o the_thmproc) thy;
  11.143 @@ -193,7 +200,7 @@
  11.144      ]
  11.145    end;
  11.146  
  11.147 -fun simple_functrans f thy eqns = case f thy (map fst eqns)
  11.148 +fun simple_functrans f ctxt eqns = case f ctxt (map fst eqns)
  11.149   of SOME thms' => SOME (map (rpair (forall snd eqns)) thms')
  11.150    | NONE => NONE;
  11.151  
  11.152 @@ -210,12 +217,16 @@
  11.153  fun sortargs eqngr = map snd o fst o get_node eqngr;
  11.154  fun all eqngr = Graph.keys eqngr;
  11.155  
  11.156 -fun pretty thy eqngr =
  11.157 -  AList.make (snd o Graph.get_node eqngr) (Graph.keys eqngr)
  11.158 -  |> (map o apfst) (Code.string_of_const thy)
  11.159 -  |> sort (string_ord o pairself fst)
  11.160 -  |> map (fn (s, cert) => (Pretty.block o Pretty.fbreaks) (Pretty.str s :: Code.pretty_cert thy cert))
  11.161 -  |> Pretty.chunks;
  11.162 +fun pretty ctxt eqngr =
  11.163 +  let
  11.164 +    val thy = Proof_Context.theory_of ctxt;
  11.165 +  in
  11.166 +    AList.make (snd o Graph.get_node eqngr) (Graph.keys eqngr)
  11.167 +    |> (map o apfst) (Code.string_of_const thy)
  11.168 +    |> sort (string_ord o pairself fst)
  11.169 +    |> map (fn (s, cert) => (Pretty.block o Pretty.fbreaks) (Pretty.str s :: Code.pretty_cert thy cert))
  11.170 +    |> Pretty.chunks
  11.171 +  end;
  11.172  
  11.173  
  11.174  (** the Waisenhaus algorithm **)
  11.175 @@ -269,17 +280,18 @@
  11.176     of SOME (lhs, cert) => ((lhs, []), cert)
  11.177      | NONE => let
  11.178          val thy = Proof_Context.theory_of ctxt;
  11.179 -        val functrans = (map (fn (_, (_, f)) => f thy)
  11.180 +        val functrans = (map (fn (_, (_, f)) => f ctxt)
  11.181            o #functrans o the_thmproc) thy;
  11.182          val cert = Code.get_cert thy { functrans = functrans, ss = simpset_of ctxt } c; (*FIXME*)
  11.183          val (lhs, rhss) =
  11.184            Code.typargs_deps_of_cert thy cert;
  11.185        in ((lhs, rhss), cert) end;
  11.186  
  11.187 -fun obtain_instance thy arities (inst as (class, tyco)) =
  11.188 +fun obtain_instance ctxt arities (inst as (class, tyco)) =
  11.189    case AList.lookup (op =) arities inst
  11.190     of SOME classess => (classess, ([], []))
  11.191      | NONE => let
  11.192 +        val thy = Proof_Context.theory_of ctxt;
  11.193          val all_classes = complete_proper_sort thy [class];
  11.194          val super_classes = remove (op =) class all_classes;
  11.195          val classess = map (complete_proper_sort thy)
  11.196 @@ -331,7 +343,7 @@
  11.197    if member (op =) insts inst then vardeps_data
  11.198    else let
  11.199      val (classess, (super_classes, inst_params)) =
  11.200 -      obtain_instance (Proof_Context.theory_of ctxt) arities inst;
  11.201 +      obtain_instance ctxt arities inst;
  11.202    in
  11.203      vardeps_data
  11.204      |> (apsnd o apsnd) (insert (op =) inst)
  11.205 @@ -381,8 +393,9 @@
  11.206  
  11.207  (* applying instantiations *)
  11.208  
  11.209 -fun dicts_of thy (proj_sort, algebra) (T, sort) =
  11.210 +fun dicts_of ctxt (proj_sort, algebra) (T, sort) =
  11.211    let
  11.212 +    val thy = Proof_Context.theory_of ctxt;
  11.213      fun class_relation (x, _) _ = x;
  11.214      fun type_constructor (tyco, _) xs class =
  11.215        inst_params thy tyco (Sorts.complete_sort algebra [class])
  11.216 @@ -395,14 +408,15 @@
  11.217         handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
  11.218    end;
  11.219  
  11.220 -fun add_arity thy vardeps (class, tyco) =
  11.221 +fun add_arity ctxt vardeps (class, tyco) =
  11.222    AList.default (op =) ((class, tyco),
  11.223      map_range (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k))
  11.224 -      (Sign.arity_number thy tyco));
  11.225 +      (Sign.arity_number (Proof_Context.theory_of ctxt) tyco));
  11.226  
  11.227 -fun add_cert thy vardeps (c, (proto_lhs, proto_cert)) (rhss, eqngr) =
  11.228 +fun add_cert ctxt vardeps (c, (proto_lhs, proto_cert)) (rhss, eqngr) =
  11.229    if can (Graph.get_node eqngr) c then (rhss, eqngr)
  11.230    else let
  11.231 +    val thy = Proof_Context.theory_of ctxt;
  11.232      val lhs = map_index (fn (k, (v, _)) =>
  11.233        (v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs;
  11.234      val cert = proto_cert
  11.235 @@ -412,20 +426,21 @@
  11.236      val eqngr' = Graph.new_node (c, (vs, cert)) eqngr;
  11.237    in (map (pair c) rhss' @ rhss, eqngr') end;
  11.238  
  11.239 -fun extend_arities_eqngr thy cs ts (arities, (eqngr : code_graph)) =
  11.240 +fun extend_arities_eqngr raw_ctxt cs ts (arities, (eqngr : code_graph)) =
  11.241    let
  11.242 +    val thy = Proof_Context.theory_of raw_ctxt;
  11.243      val {pre, ...} = the_thmproc thy;
  11.244 -    val ctxt = thy |> Proof_Context.init_global |> put_simpset pre;
  11.245 +    val ctxt = put_simpset pre raw_ctxt;
  11.246      val cs_rhss = (fold o fold_aterms) (fn Const (c_ty as (c, _)) =>
  11.247        insert (op =) (c, (map (styp_of NONE) o Sign.const_typargs thy) c_ty) | _ => I) ts [];
  11.248      val (vardeps, (eqntab, insts)) = empty_vardeps_data
  11.249        |> fold (ensure_fun ctxt arities eqngr) cs
  11.250        |> fold (ensure_rhs ctxt arities eqngr) cs_rhss;
  11.251 -    val arities' = fold (add_arity thy vardeps) insts arities;
  11.252 +    val arities' = fold (add_arity ctxt vardeps) insts arities;
  11.253      val algebra = Sorts.subalgebra (Context.pretty_global thy) (is_proper_class thy)
  11.254        (AList.lookup (op =) arities') (Sign.classes_of thy);
  11.255 -    val (rhss, eqngr') = Symtab.fold (add_cert thy vardeps) eqntab ([], eqngr);
  11.256 -    fun deps_of (c, rhs) = c :: maps (dicts_of thy algebra)
  11.257 +    val (rhss, eqngr') = Symtab.fold (add_cert ctxt vardeps) eqntab ([], eqngr);
  11.258 +    fun deps_of (c, rhs) = c :: maps (dicts_of ctxt algebra)
  11.259        (rhs ~~ sortargs eqngr' c);
  11.260      val eqngr'' = fold (fn (c, rhs) => fold
  11.261        (curry Graph.add_edge c) (deps_of rhs)) rhss eqngr';
  11.262 @@ -444,59 +459,62 @@
  11.263  (** retrieval and evaluation interfaces **)
  11.264  
  11.265  fun obtain ignore_cache thy consts ts = apsnd snd
  11.266 -  (Wellsorted.change_yield (if ignore_cache then NONE else SOME thy) (extend_arities_eqngr thy consts ts));
  11.267 +  (Wellsorted.change_yield (if ignore_cache then NONE else SOME thy)
  11.268 +    (extend_arities_eqngr (Proof_Context.init_global thy) consts ts));
  11.269  
  11.270  fun dest_cterm ct = let val t = Thm.term_of ct in (Term.add_tfrees t [], t) end;
  11.271  
  11.272 -fun dynamic_conv thy conv = no_variables_conv (fn ct =>
  11.273 +fun dynamic_conv ctxt conv = no_variables_conv ctxt (fn ct =>
  11.274    let
  11.275 -    val thm1 = preprocess_conv thy ct;
  11.276 +    val thm1 = preprocess_conv ctxt ctxt ct;
  11.277      val ct' = Thm.rhs_of thm1;
  11.278      val (vs', t') = dest_cterm ct';
  11.279      val consts = fold_aterms
  11.280        (fn Const (c, _) => insert (op =) c | _ => I) t' [];
  11.281 -    val (algebra', eqngr') = obtain false thy consts [t'];
  11.282 +    val (algebra', eqngr') = obtain false (Proof_Context.theory_of ctxt) consts [t'];
  11.283      val thm2 = conv algebra' eqngr' vs' t' ct';
  11.284 -    val thm3 = postprocess_conv thy (Thm.rhs_of thm2);
  11.285 +    val thm3 = postprocess_conv ctxt ctxt (Thm.rhs_of thm2);
  11.286    in
  11.287      Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
  11.288        error ("could not construct evaluation proof:\n"
  11.289 -      ^ (cat_lines o map (Display.string_of_thm_global thy)) [thm1, thm2, thm3])
  11.290 +      ^ (cat_lines o map (Display.string_of_thm ctxt)) [thm1, thm2, thm3])
  11.291    end);
  11.292  
  11.293 -fun dynamic_value thy postproc evaluator t =
  11.294 +fun dynamic_value ctxt postproc evaluator t =
  11.295    let
  11.296 -    val (resubst, t') = preprocess_term thy t;
  11.297 +    val (resubst, t') = preprocess_term ctxt ctxt t;
  11.298      val vs' = Term.add_tfrees t' [];
  11.299      val consts = fold_aterms
  11.300        (fn Const (c, _) => insert (op =) c | _ => I) t' [];
  11.301 -    val (algebra', eqngr') = obtain false thy consts [t'];
  11.302 +    val (algebra', eqngr') = obtain false (Proof_Context.theory_of ctxt) consts [t'];
  11.303    in
  11.304      t'
  11.305      |> evaluator algebra' eqngr' vs'
  11.306 -    |> postproc (postprocess_term thy o resubst)
  11.307 +    |> postproc (postprocess_term ctxt ctxt o resubst)
  11.308    end;
  11.309  
  11.310 -fun static_conv thy consts conv =
  11.311 +fun static_conv ctxt consts conv =
  11.312    let
  11.313 -    val (algebra, eqngr) = obtain true thy consts [];
  11.314 +    val (algebra, eqngr) = obtain true (Proof_Context.theory_of ctxt) consts [];
  11.315 +    val pre_conv = preprocess_conv ctxt;
  11.316      val conv' = conv algebra eqngr;
  11.317 -  in
  11.318 -    no_variables_conv ((preprocess_conv thy)
  11.319 -      then_conv (fn ct => uncurry conv' (dest_cterm ct) ct)
  11.320 -      then_conv (postprocess_conv thy))
  11.321 +    val post_conv = postprocess_conv ctxt;
  11.322 +  in fn ctxt' => no_variables_conv ctxt' ((pre_conv ctxt')
  11.323 +    then_conv (fn ct => uncurry (conv' ctxt') (dest_cterm ct) ct)
  11.324 +    then_conv (post_conv ctxt'))
  11.325    end;
  11.326  
  11.327 -fun static_value thy postproc consts evaluator =
  11.328 +fun static_value ctxt postproc consts evaluator =
  11.329    let
  11.330 -    val (algebra, eqngr) = obtain true thy consts [];
  11.331 +    val (algebra, eqngr) = obtain true (Proof_Context.theory_of ctxt) consts [];
  11.332 +    val preproc = preprocess_term ctxt;
  11.333      val evaluator' = evaluator algebra eqngr;
  11.334 -    val postproc' = postprocess_term thy;
  11.335 -  in 
  11.336 -    preprocess_term thy
  11.337 +    val postproc' = postprocess_term ctxt;
  11.338 +  in fn ctxt' => 
  11.339 +    preproc ctxt'
  11.340      #-> (fn resubst => fn t => t
  11.341 -      |> evaluator' (Term.add_tfrees t [])
  11.342 -      |> postproc (postproc' o resubst))
  11.343 +      |> evaluator' ctxt' (Term.add_tfrees t [])
  11.344 +      |> postproc (postproc' ctxt' o resubst))
  11.345    end;
  11.346  
  11.347  
  11.348 @@ -518,7 +536,6 @@
  11.349  
  11.350  val _ =
  11.351    Outer_Syntax.improper_command @{command_spec "print_codeproc"} "print code preprocessor setup"
  11.352 -    (Scan.succeed (Toplevel.unknown_theory o
  11.353 -      Toplevel.keep (print_codeproc o Toplevel.theory_of)));
  11.354 +    (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_codeproc o Toplevel.context_of)));
  11.355  
  11.356  end; (*struct*)
    12.1 --- a/src/Tools/Code/code_runtime.ML	Wed Feb 26 10:10:38 2014 +0100
    12.2 +++ b/src/Tools/Code/code_runtime.ML	Wed Feb 26 11:57:52 2014 +0100
    12.3 @@ -11,20 +11,20 @@
    12.4      (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string ->
    12.5      string * string -> 'a
    12.6    type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string
    12.7 -  val dynamic_value: 'a cookie -> theory -> string option
    12.8 +  val dynamic_value: 'a cookie -> Proof.context -> string option
    12.9      -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a option
   12.10 -  val dynamic_value_strict: 'a cookie -> theory -> string option
   12.11 +  val dynamic_value_strict: 'a cookie -> Proof.context -> string option
   12.12      -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a
   12.13 -  val dynamic_value_exn: 'a cookie -> theory -> string option
   12.14 +  val dynamic_value_exn: 'a cookie -> Proof.context -> string option
   12.15      -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a Exn.result
   12.16 -  val static_value: 'a cookie -> theory -> string option
   12.17 -    -> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a option
   12.18 -  val static_value_strict: 'a cookie -> theory -> string option
   12.19 -    -> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a
   12.20 -  val static_value_exn: 'a cookie -> theory -> string option
   12.21 -    -> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a Exn.result
   12.22 -  val dynamic_holds_conv: theory -> conv
   12.23 -  val static_holds_conv: theory -> string list -> conv
   12.24 +  val static_value: 'a cookie -> Proof.context -> string option
   12.25 +    -> ((term -> term) -> 'a -> 'a) -> string list -> Proof.context -> term -> 'a option
   12.26 +  val static_value_strict: 'a cookie -> Proof.context -> string option
   12.27 +    -> ((term -> term) -> 'a -> 'a) -> string list -> Proof.context -> term -> 'a
   12.28 +  val static_value_exn: 'a cookie -> Proof.context -> string option
   12.29 +    -> ((term -> term) -> 'a -> 'a) -> string list -> Proof.context -> term -> 'a Exn.result
   12.30 +  val dynamic_holds_conv: Proof.context -> conv
   12.31 +  val static_holds_conv: Proof.context -> string list -> Proof.context -> conv
   12.32    val code_reflect: (string * string list option) list -> string list -> string
   12.33      -> string option -> theory -> theory
   12.34    datatype truth = Holds
   12.35 @@ -83,21 +83,19 @@
   12.36  
   12.37  type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string;
   12.38  
   12.39 -fun reject_vars thy t =
   12.40 -  let
   12.41 -    val ctxt = Proof_Context.init_global thy;
   12.42 -  in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end;
   12.43 +fun reject_vars ctxt t =
   12.44 +  ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t);
   12.45  
   12.46 -fun obtain_evaluator thy some_target program consts expr =
   12.47 -  Code_Target.evaluator thy (the_default target some_target) program consts false expr
   12.48 -  |> apfst (fn ml_modules => space_implode "\n\n" (map snd ml_modules));
   12.49 +fun obtain_evaluator ctxt some_target program consts =
   12.50 +  let
   12.51 +    val evaluator' = Code_Target.evaluator ctxt (the_default target some_target) program consts false;
   12.52 +  in
   12.53 +    evaluator'
   12.54 +    #> apfst (fn ml_modules => space_implode "\n\n" (map snd ml_modules))
   12.55 +  end;
   12.56  
   12.57 -fun obtain_evaluator' thy some_target program =
   12.58 -  obtain_evaluator thy some_target program o map Constant;
   12.59 -
   12.60 -fun evaluation cookie thy evaluator vs_t args =
   12.61 +fun evaluation cookie ctxt evaluator vs_t args =
   12.62    let
   12.63 -    val ctxt = Proof_Context.init_global thy;
   12.64      val (program_code, value_name) = evaluator vs_t;
   12.65      val value_code = space_implode " "
   12.66        (value_name :: "()" :: map (enclose "(" ")") args);
   12.67 @@ -108,36 +106,39 @@
   12.68      | General.Bind => NONE
   12.69      | General.Fail _ => NONE;
   12.70  
   12.71 -fun dynamic_value_exn cookie thy some_target postproc t args =
   12.72 +fun dynamic_value_exn cookie ctxt some_target postproc t args =
   12.73    let
   12.74 -    val _ = reject_vars thy t;
   12.75 +    val _ = reject_vars ctxt t;
   12.76      val _ = if ! trace
   12.77 -      then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term_global thy t))
   12.78 +      then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term ctxt t))
   12.79        else ()
   12.80      fun evaluator program ((_, vs_ty), t) deps =
   12.81 -      evaluation cookie thy (obtain_evaluator thy some_target program deps) (vs_ty, t) args;
   12.82 -  in Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t end;
   12.83 +      evaluation cookie ctxt (obtain_evaluator ctxt some_target program deps) (vs_ty, t) args;
   12.84 +  in Code_Thingol.dynamic_value ctxt (Exn.map_result o postproc) evaluator t end;
   12.85  
   12.86 -fun dynamic_value_strict cookie thy some_target postproc t args =
   12.87 -  Exn.release (dynamic_value_exn cookie thy some_target postproc t args);
   12.88 +fun dynamic_value_strict cookie ctxt some_target postproc t args =
   12.89 +  Exn.release (dynamic_value_exn cookie ctxt some_target postproc t args);
   12.90  
   12.91 -fun dynamic_value cookie thy some_target postproc t args =
   12.92 -  partiality_as_none (dynamic_value_exn cookie thy some_target postproc t args);
   12.93 +fun dynamic_value cookie ctxt some_target postproc t args =
   12.94 +  partiality_as_none (dynamic_value_exn cookie ctxt some_target postproc t args);
   12.95  
   12.96 -fun static_evaluator cookie thy some_target program consts' =
   12.97 +fun static_evaluator cookie ctxt some_target program consts' =
   12.98    let
   12.99 -    val evaluator = obtain_evaluator' thy some_target program consts'
  12.100 -  in fn ((_, vs_ty), t) => fn _ => evaluation cookie thy evaluator (vs_ty, t) [] end;
  12.101 +    val evaluator = obtain_evaluator ctxt some_target program (map Constant consts');
  12.102 +    val evaluation' = evaluation cookie ctxt evaluator;
  12.103 +  in fn _ => fn ((_, vs_ty), t) => fn _ => evaluation' (vs_ty, t) [] end;
  12.104  
  12.105 -fun static_value_exn cookie thy some_target postproc consts =
  12.106 -  Code_Thingol.static_value thy (Exn.map_result o postproc) consts
  12.107 -    (static_evaluator cookie thy some_target) o reject_vars thy;
  12.108 +fun static_value_exn cookie ctxt some_target postproc consts =
  12.109 +  let
  12.110 +    val evaluator = Code_Thingol.static_value ctxt (Exn.map_result o postproc) consts
  12.111 +      (static_evaluator cookie ctxt some_target);
  12.112 +  in fn ctxt' => evaluator ctxt' o reject_vars ctxt' end;
  12.113  
  12.114 -fun static_value_strict cookie thy some_target postproc consts =
  12.115 -  Exn.release o static_value_exn cookie thy some_target postproc consts;
  12.116 +fun static_value_strict cookie ctxt some_target postproc consts =
  12.117 +  Exn.release oo static_value_exn cookie ctxt some_target postproc consts;
  12.118  
  12.119  fun static_value cookie thy some_target postproc consts =
  12.120 -  partiality_as_none o static_value_exn cookie thy some_target postproc consts;
  12.121 +  partiality_as_none oo static_value_exn cookie thy some_target postproc consts;
  12.122  
  12.123  
  12.124  (* evaluation for truth or nothing *)
  12.125 @@ -151,18 +152,19 @@
  12.126  val put_truth = Truth_Result.put;
  12.127  val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append this "put_truth");
  12.128  
  12.129 -val reject_vars = fn thy => tap (reject_vars thy o Thm.term_of);
  12.130 +val reject_vars = fn ctxt => tap (reject_vars ctxt o Thm.term_of);
  12.131  
  12.132  local
  12.133  
  12.134 -fun check_holds thy evaluator vs_t ct =
  12.135 +fun check_holds ctxt evaluator vs_t ct =
  12.136    let
  12.137 +    val thy = Proof_Context.theory_of ctxt;
  12.138      val t = Thm.term_of ct;
  12.139      val _ = if fastype_of t <> propT
  12.140        then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t)
  12.141        else ();
  12.142      val iff = Thm.cterm_of thy (Term.Const ("==", propT --> propT --> propT));
  12.143 -    val result = case partiality_as_none (evaluation truth_cookie thy evaluator vs_t [])
  12.144 +    val result = case partiality_as_none (evaluation truth_cookie ctxt evaluator vs_t [])
  12.145       of SOME Holds => true
  12.146        | _ => false;
  12.147    in
  12.148 @@ -171,34 +173,39 @@
  12.149  
  12.150  val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result
  12.151    (Thm.add_oracle (@{binding holds_by_evaluation},
  12.152 -  fn (thy, evaluator, vs_t, ct) => check_holds thy evaluator vs_t ct)));
  12.153 +  fn (ctxt, evaluator, vs_t, ct) => check_holds ctxt evaluator vs_t ct)));
  12.154  
  12.155 -fun check_holds_oracle thy evaluator ((_, vs_ty), t) deps ct =
  12.156 -  raw_check_holds_oracle (thy, evaluator, (vs_ty, t), ct);
  12.157 +fun check_holds_oracle ctxt evaluator ((_, vs_ty), t) deps ct =
  12.158 +  raw_check_holds_oracle (ctxt, evaluator, (vs_ty, t), ct);
  12.159  
  12.160  in
  12.161  
  12.162 -fun dynamic_holds_conv thy = Code_Thingol.dynamic_conv thy
  12.163 +fun dynamic_holds_conv ctxt = Code_Thingol.dynamic_conv ctxt
  12.164    (fn program => fn vs_t => fn deps =>
  12.165 -    check_holds_oracle thy (obtain_evaluator thy NONE program deps) vs_t deps)
  12.166 -      o reject_vars thy;
  12.167 +    check_holds_oracle ctxt (obtain_evaluator ctxt NONE program deps) vs_t deps)
  12.168 +      o reject_vars ctxt;
  12.169  
  12.170 -fun static_holds_conv thy consts = Code_Thingol.static_conv thy consts
  12.171 -  (fn program => fn consts' =>
  12.172 -    check_holds_oracle thy (obtain_evaluator' thy NONE program consts'))
  12.173 -      o reject_vars thy;
  12.174 +fun static_holds_conv ctxt consts =
  12.175 +  Code_Thingol.static_conv ctxt consts (fn program => fn consts' =>
  12.176 +    let
  12.177 +      val evaluator' = obtain_evaluator ctxt NONE program (map Constant consts')
  12.178 +    in
  12.179 +      fn ctxt' => fn vs_t => fn deps => check_holds_oracle ctxt' evaluator' vs_t deps o reject_vars ctxt'
  12.180 +    end);
  12.181 +
  12.182 +(* o reject_vars ctxt'*)
  12.183  
  12.184  end; (*local*)
  12.185  
  12.186  
  12.187  (** instrumentalization **)
  12.188  
  12.189 -fun evaluation_code thy module_name tycos consts =
  12.190 +fun evaluation_code ctxt module_name tycos consts =
  12.191    let
  12.192 -    val ctxt = Proof_Context.init_global thy;
  12.193 +    val thy = Proof_Context.theory_of ctxt;
  12.194      val program = Code_Thingol.consts_program thy consts;
  12.195      val (ml_modules, target_names) =
  12.196 -      Code_Target.produce_code_for thy
  12.197 +      Code_Target.produce_code_for ctxt
  12.198          target NONE module_name [] program false (map Constant consts @ map Type_Constructor tycos);
  12.199      val ml_code = space_implode "\n\n" (map snd ml_modules);
  12.200      val (consts', tycos') = chop (length consts) target_names;
  12.201 @@ -234,7 +241,7 @@
  12.202      val tycos' = fold (insert (op =)) new_tycos tycos;
  12.203      val consts' = fold (insert (op =)) new_consts consts;
  12.204      val acc_code = Lazy.lazy (fn () =>
  12.205 -      evaluation_code (Proof_Context.theory_of ctxt) structure_generated tycos' consts'
  12.206 +      evaluation_code ctxt structure_generated tycos' consts'
  12.207        |> apsnd snd);
  12.208    in Code_Antiq_Data.put ((tycos', consts'), (false, acc_code)) ctxt end;
  12.209  
  12.210 @@ -330,12 +337,13 @@
  12.211  
  12.212  fun gen_code_reflect prep_type prep_const raw_datatypes raw_functions module_name some_file thy  =
  12.213    let
  12.214 +    val ctxt = Proof_Context.init_global thy;
  12.215      val datatypes = map (fn (raw_tyco, raw_cos) =>
  12.216 -      (prep_type thy raw_tyco, (Option.map o map) (prep_const thy) raw_cos)) raw_datatypes;
  12.217 +      (prep_type ctxt raw_tyco, (Option.map o map) (prep_const thy) raw_cos)) raw_datatypes;
  12.218      val (tycos, constrs) = map_split (uncurry (check_datatype thy)) datatypes
  12.219        |> apsnd flat;
  12.220      val functions = map (prep_const thy) raw_functions;
  12.221 -    val result = evaluation_code thy module_name tycos (constrs @ functions)
  12.222 +    val result = evaluation_code ctxt module_name tycos (constrs @ functions)
  12.223        |> (apsnd o apsnd) (chop (length constrs));
  12.224    in
  12.225      thy
  12.226 @@ -440,7 +448,7 @@
  12.227    |-> (fn ([Const (const, _)], _) =>
  12.228      Code_Target.set_printings (Constant (const,
  12.229        [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))]))
  12.230 -  #> tap (fn thy => Code_Target.produce_code thy false [const] target NONE structure_generated []));
  12.231 +  #> tap (fn thy => Code_Target.produce_code (Proof_Context.init_global thy) false [const] target NONE structure_generated []));
  12.232  
  12.233  fun process_file filepath (definienda, thy) =
  12.234    let
    13.1 --- a/src/Tools/Code/code_simp.ML	Wed Feb 26 10:10:38 2014 +0100
    13.2 +++ b/src/Tools/Code/code_simp.ML	Wed Feb 26 11:57:52 2014 +0100
    13.3 @@ -7,11 +7,11 @@
    13.4  signature CODE_SIMP =
    13.5  sig
    13.6    val map_ss: (Proof.context -> Proof.context) -> theory -> theory
    13.7 -  val dynamic_conv: theory -> conv
    13.8 -  val dynamic_tac: theory -> int -> tactic
    13.9 -  val dynamic_value: theory -> term -> term
   13.10 -  val static_conv: theory -> simpset option -> string list -> conv
   13.11 -  val static_tac: theory -> simpset option -> string list -> Proof.context -> int -> tactic
   13.12 +  val dynamic_conv: Proof.context -> conv
   13.13 +  val dynamic_tac: Proof.context -> int -> tactic
   13.14 +  val dynamic_value: Proof.context -> term -> term
   13.15 +  val static_conv: Proof.context -> simpset option -> string list -> Proof.context -> conv
   13.16 +  val static_tac: Proof.context -> simpset option -> string list -> Proof.context -> int -> tactic
   13.17    val setup: theory -> theory
   13.18    val trace: bool Config.T
   13.19  end;
   13.20 @@ -31,11 +31,11 @@
   13.21  
   13.22  fun map_ss f thy = Simpset.map (simpset_map (Proof_Context.init_global thy) f) thy;
   13.23  
   13.24 -fun simpset_default thy some_ss = the_default (Simpset.get thy) some_ss;
   13.25 +fun simpset_default ctxt some_ss = the_default (Simpset.get (Proof_Context.theory_of ctxt)) some_ss;
   13.26  
   13.27 -fun simp_ctxt_default thy some_ss =
   13.28 -  Proof_Context.init_global thy
   13.29 -  |> put_simpset (simpset_default thy some_ss);
   13.30 +(*fun simp_ctxt_default ctxt some_ss =
   13.31 +  Proof_Context.init_global ctxt
   13.32 +  |> put_simpset (simpset_default ctxt some_ss);*)
   13.33  
   13.34  
   13.35  (* diagnostic *)
   13.36 @@ -50,7 +50,7 @@
   13.37    end;
   13.38  
   13.39  
   13.40 -(* build simpset and conversion from program *)
   13.41 +(* build simpset context and conversion from program *)
   13.42  
   13.43  fun add_stmt (Code_Thingol.Fun ((_, eqs), some_cong)) ss =
   13.44        ss
   13.45 @@ -63,43 +63,49 @@
   13.46  
   13.47  val add_program = Code_Symbol.Graph.fold (add_stmt o fst o snd);
   13.48  
   13.49 -fun simp_ctxt_program thy some_ss program =
   13.50 -  simp_ctxt_default thy some_ss
   13.51 -  |> add_program program;
   13.52 +fun simpset_program ctxt some_ss program =
   13.53 +  simpset_map ctxt (add_program program) (simpset_default ctxt some_ss);
   13.54  
   13.55 -fun rewrite_modulo thy some_ss program =
   13.56 -  Simplifier.full_rewrite (simp_ctxt_program thy some_ss program |> set_trace);
   13.57 +fun rewrite_modulo ctxt some_ss program =
   13.58 +  let
   13.59 +    val ss = simpset_program ctxt some_ss program;
   13.60 +  in fn ctxt => Simplifier.full_rewrite (ctxt |> put_simpset ss |> set_trace) end;
   13.61  
   13.62 -fun conclude_tac thy some_ss =
   13.63 -  Simplifier.full_simp_tac o Simplifier.put_simpset (simpset_default thy some_ss);
   13.64 +fun conclude_tac ctxt some_ss =
   13.65 +  let
   13.66 +    val ss = simpset_default ctxt some_ss
   13.67 +  in fn ctxt => Simplifier.full_simp_tac (ctxt |> put_simpset ss) end;
   13.68  
   13.69  
   13.70  (* evaluation with dynamic code context *)
   13.71  
   13.72 -fun dynamic_conv thy = Code_Thingol.dynamic_conv thy
   13.73 -  (fn program => fn _ => fn _ => rewrite_modulo thy NONE program);
   13.74 +fun dynamic_conv ctxt = Code_Thingol.dynamic_conv ctxt
   13.75 +  (fn program => fn _ => fn _ => rewrite_modulo ctxt NONE program ctxt);
   13.76  
   13.77 -fun dynamic_tac thy = CONVERSION (dynamic_conv thy) THEN' conclude_tac thy NONE (Proof_Context.init_global thy);
   13.78 +fun dynamic_tac ctxt = CONVERSION (dynamic_conv ctxt)
   13.79 +  THEN' conclude_tac ctxt NONE ctxt;
   13.80  
   13.81 -fun dynamic_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_conv thy o Thm.cterm_of thy;
   13.82 +fun dynamic_value ctxt =
   13.83 +  snd o Logic.dest_equals o Thm.prop_of o dynamic_conv ctxt o Thm.cterm_of (Proof_Context.theory_of ctxt);
   13.84  
   13.85  val setup =
   13.86    Method.setup @{binding code_simp}
   13.87 -    (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac o Proof_Context.theory_of)))
   13.88 +    (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac)))
   13.89      "simplification with code equations"
   13.90 -  #> Value.add_evaluator ("simp", dynamic_value o Proof_Context.theory_of);
   13.91 +  #> Value.add_evaluator ("simp", dynamic_value);
   13.92  
   13.93  
   13.94  (* evaluation with static code context *)
   13.95  
   13.96 -fun static_conv thy some_ss consts =
   13.97 -  Code_Thingol.static_conv_simple thy consts
   13.98 -    (fn program => fn _ => fn _ => rewrite_modulo thy some_ss program);
   13.99 +fun static_conv ctxt some_ss consts =
  13.100 +  Code_Thingol.static_conv_simple ctxt consts
  13.101 +    (fn program => let val conv' = rewrite_modulo ctxt some_ss program
  13.102 +     in fn ctxt' => fn _ => fn _ => conv' ctxt' end);
  13.103  
  13.104 -fun static_tac thy some_ss consts =
  13.105 +fun static_tac ctxt some_ss consts =
  13.106    let
  13.107 -    val conv = static_conv thy some_ss consts;
  13.108 -    val tac = conclude_tac thy some_ss;
  13.109 -  in fn ctxt => CONVERSION conv THEN' tac ctxt end;
  13.110 +    val conv = static_conv ctxt some_ss consts;
  13.111 +    val tac = conclude_tac ctxt some_ss;
  13.112 +  in fn ctxt' => CONVERSION (conv ctxt') THEN' (tac ctxt') end;
  13.113  
  13.114  end;
    14.1 --- a/src/Tools/Code/code_target.ML	Wed Feb 26 10:10:38 2014 +0100
    14.2 +++ b/src/Tools/Code/code_target.ML	Wed Feb 26 11:57:52 2014 +0100
    14.3 @@ -6,29 +6,29 @@
    14.4  
    14.5  signature CODE_TARGET =
    14.6  sig
    14.7 -  val cert_tyco: theory -> string -> string
    14.8 -  val read_tyco: theory -> string -> string
    14.9 +  val cert_tyco: Proof.context -> string -> string
   14.10 +  val read_tyco: Proof.context -> string -> string
   14.11  
   14.12 -  val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list
   14.13 +  val export_code_for: Proof.context -> Path.T option -> string -> int option -> string -> Token.T list
   14.14      -> Code_Thingol.program -> bool -> Code_Symbol.T list -> unit
   14.15 -  val produce_code_for: theory -> string -> int option -> string -> Token.T list
   14.16 +  val produce_code_for: Proof.context -> string -> int option -> string -> Token.T list
   14.17      -> Code_Thingol.program -> bool -> Code_Symbol.T list -> (string * string) list * string option list
   14.18 -  val present_code_for: theory -> string -> int option -> string -> Token.T list
   14.19 +  val present_code_for: Proof.context -> string -> int option -> string -> Token.T list
   14.20      -> Code_Thingol.program -> Code_Symbol.T list * Code_Symbol.T list -> string
   14.21 -  val check_code_for: theory -> string -> bool -> Token.T list
   14.22 +  val check_code_for: Proof.context -> string -> bool -> Token.T list
   14.23      -> Code_Thingol.program -> bool -> Code_Symbol.T list -> unit
   14.24  
   14.25 -  val export_code: theory -> bool -> string list
   14.26 +  val export_code: Proof.context -> bool -> string list
   14.27      -> (((string * string) * Path.T option) * Token.T list) list -> unit
   14.28 -  val produce_code: theory -> bool -> string list
   14.29 +  val produce_code: Proof.context -> bool -> string list
   14.30      -> string -> int option -> string -> Token.T list -> (string * string) list * string option list
   14.31 -  val present_code: theory -> string list -> Code_Symbol.T list
   14.32 +  val present_code: Proof.context -> string list -> Code_Symbol.T list
   14.33      -> string -> int option -> string -> Token.T list -> string
   14.34 -  val check_code: theory -> bool -> string list
   14.35 +  val check_code: Proof.context -> bool -> string list
   14.36      -> ((string * bool) * Token.T list) list -> unit
   14.37  
   14.38    val generatedN: string
   14.39 -  val evaluator: theory -> string -> Code_Thingol.program
   14.40 +  val evaluator: Proof.context -> string -> Code_Thingol.program
   14.41      -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
   14.42      -> (string * string) list * string
   14.43  
   14.44 @@ -40,8 +40,8 @@
   14.45    val extend_target: string *
   14.46        (string * (Code_Thingol.program -> Code_Thingol.program))
   14.47      -> theory -> theory
   14.48 -  val assert_target: theory -> string -> string
   14.49 -  val the_literals: theory -> string -> literals
   14.50 +  val assert_target: Proof.context -> string -> string
   14.51 +  val the_literals: Proof.context -> string -> literals
   14.52    type serialization
   14.53    val parse_args: 'a parser -> Token.T list -> 'a
   14.54    val serialization: (int -> Path.T option -> 'a -> unit)
   14.55 @@ -83,45 +83,45 @@
   14.56  
   14.57  (** checking and parsing of symbols **)
   14.58  
   14.59 -fun cert_const thy const =
   14.60 +fun cert_const ctxt const =
   14.61    let
   14.62 -    val _ = if Sign.declared_const thy const then ()
   14.63 +    val _ = if Sign.declared_const (Proof_Context.theory_of ctxt) const then ()
   14.64        else error ("No such constant: " ^ quote const);
   14.65    in const end;
   14.66  
   14.67 -fun cert_tyco thy tyco =
   14.68 +fun read_const ctxt = Code.read_const (Proof_Context.theory_of ctxt);
   14.69 +
   14.70 +fun cert_tyco ctxt tyco =
   14.71    let
   14.72 -    val _ = if Sign.declared_tyname thy tyco then ()
   14.73 +    val _ = if Sign.declared_tyname (Proof_Context.theory_of ctxt) tyco then ()
   14.74        else error ("No such type constructor: " ^ quote tyco);
   14.75    in tyco end;
   14.76  
   14.77 -fun read_tyco thy = #1 o dest_Type
   14.78 -  o Proof_Context.read_type_name_proper (Proof_Context.init_global thy) true;
   14.79 +fun read_tyco ctxt = #1 o dest_Type
   14.80 +  o Proof_Context.read_type_name_proper ctxt true;
   14.81  
   14.82 -fun cert_class thy class =
   14.83 +fun cert_class ctxt class =
   14.84    let
   14.85 -    val _ = Axclass.get_info thy class;
   14.86 +    val _ = Axclass.get_info (Proof_Context.theory_of ctxt) class;
   14.87    in class end;
   14.88  
   14.89 -fun read_class thy = Proof_Context.read_class (Proof_Context.init_global thy);
   14.90 -
   14.91  val parse_classrel_ident = Parse.class --| @{keyword "<"} -- Parse.class;
   14.92  
   14.93 -fun cert_inst thy (class, tyco) =
   14.94 -  (cert_class thy class, cert_tyco thy tyco);
   14.95 +fun cert_inst ctxt (class, tyco) =
   14.96 +  (cert_class ctxt class, cert_tyco ctxt tyco);
   14.97  
   14.98 -fun read_inst thy (raw_tyco, raw_class) =
   14.99 -  (read_tyco thy raw_tyco, read_class thy raw_class);
  14.100 +fun read_inst ctxt (raw_tyco, raw_class) =
  14.101 +  (read_tyco ctxt raw_tyco, Proof_Context.read_class ctxt raw_class);
  14.102  
  14.103  val parse_inst_ident = Parse.xname --| @{keyword "::"} -- Parse.class;
  14.104  
  14.105 -fun cert_syms thy =
  14.106 -  Code_Symbol.map_attr (apfst (cert_const thy)) (apfst (cert_tyco thy))
  14.107 -    (apfst (cert_class thy)) ((apfst o pairself) (cert_class thy)) (apfst (cert_inst thy)) I;
  14.108 +fun cert_syms ctxt =
  14.109 +  Code_Symbol.map_attr (apfst (cert_const ctxt)) (apfst (cert_tyco ctxt))
  14.110 +    (apfst (cert_class ctxt)) ((apfst o pairself) (cert_class ctxt)) (apfst (cert_inst ctxt)) I;
  14.111  
  14.112 -fun read_syms thy =
  14.113 -  Code_Symbol.map_attr (apfst (Code.read_const thy)) (apfst (read_tyco thy))
  14.114 -    (apfst (read_class thy)) ((apfst o pairself) (read_class thy)) (apfst (read_inst thy)) I;
  14.115 +fun read_syms ctxt =
  14.116 +  Code_Symbol.map_attr (apfst (read_const ctxt)) (apfst (read_tyco ctxt))
  14.117 +    (apfst (Proof_Context.read_class ctxt)) ((apfst o pairself) (Proof_Context.read_class ctxt)) (apfst (read_inst ctxt)) I;
  14.118  
  14.119  fun check_name is_module s =
  14.120    let
  14.121 @@ -231,7 +231,8 @@
  14.122      (Symtab.join (merge_target true) (target1, target2), Int.max (width1, width2));
  14.123  );
  14.124  
  14.125 -fun assert_target thy target = if Symtab.defined (fst (Targets.get thy)) target
  14.126 +fun assert_target ctxt target =
  14.127 +  if Symtab.defined (fst (Targets.get (Proof_Context.theory_of ctxt))) target
  14.128    then target
  14.129    else error ("Unknown code target language: " ^ quote target);
  14.130  
  14.131 @@ -264,7 +265,7 @@
  14.132  
  14.133  fun map_target_data target f thy =
  14.134    let
  14.135 -    val _ = assert_target thy target;
  14.136 +    val _ = assert_target (Proof_Context.init_global thy) target;
  14.137    in
  14.138      thy
  14.139      |> (Targets.map o apfst o Symtab.map_entry target o map_target o apsnd) f
  14.140 @@ -284,9 +285,9 @@
  14.141  
  14.142  (* montage *)
  14.143  
  14.144 -fun the_fundamental thy =
  14.145 +fun the_fundamental ctxt =
  14.146    let
  14.147 -    val (targets, _) = Targets.get thy;
  14.148 +    val (targets, _) = Targets.get (Proof_Context.theory_of ctxt);
  14.149      fun fundamental target = case Symtab.lookup targets target
  14.150       of SOME data => (case the_description data
  14.151           of Fundamental data => data
  14.152 @@ -294,11 +295,11 @@
  14.153        | NONE => error ("Unknown code target language: " ^ quote target);
  14.154    in fundamental end;
  14.155  
  14.156 -fun the_literals thy = #literals o the_fundamental thy;
  14.157 +fun the_literals ctxt = #literals o the_fundamental ctxt;
  14.158  
  14.159 -fun collapse_hierarchy thy =
  14.160 +fun collapse_hierarchy ctxt =
  14.161    let
  14.162 -    val (targets, _) = Targets.get thy;
  14.163 +    val (targets, _) = Targets.get (Proof_Context.theory_of ctxt);
  14.164      fun collapse target =
  14.165        let
  14.166          val data = case Symtab.lookup targets target
  14.167 @@ -314,15 +315,15 @@
  14.168  
  14.169  local
  14.170  
  14.171 -fun activate_target thy target =
  14.172 +fun activate_target ctxt target =
  14.173    let
  14.174 +    val thy = Proof_Context.theory_of ctxt;
  14.175      val (_, default_width) = Targets.get thy;
  14.176 -    val (modify, data) = collapse_hierarchy thy target;
  14.177 +    val (modify, data) = collapse_hierarchy ctxt target;
  14.178    in (default_width, data, modify) end;
  14.179  
  14.180 -fun project_program thy syms_hidden syms1 program2 =
  14.181 +fun project_program ctxt syms_hidden syms1 program2 =
  14.182    let
  14.183 -    val ctxt = Proof_Context.init_global thy;
  14.184      val syms2 = subtract (op =) syms_hidden syms1;
  14.185      val program3 = Code_Symbol.Graph.restrict (not o member (op =) syms_hidden) program2;
  14.186      val syms4 = Code_Symbol.Graph.all_succs program3 syms2;
  14.187 @@ -334,17 +335,17 @@
  14.188      val program4 = Code_Symbol.Graph.restrict (member (op =) syms4) program3;
  14.189    in (syms4, program4) end;
  14.190  
  14.191 -fun prepare_serializer thy (serializer : serializer) reserved identifiers
  14.192 +fun prepare_serializer ctxt (serializer : serializer) reserved identifiers
  14.193      printings module_name args proto_program syms =
  14.194    let
  14.195      val syms_hidden = Code_Symbol.symbols_of printings;
  14.196 -    val (syms_all, program) = project_program thy syms_hidden syms proto_program;
  14.197 +    val (syms_all, program) = project_program ctxt syms_hidden syms proto_program;
  14.198      fun select_include (name, (content, cs)) =
  14.199        if null cs orelse exists (fn c => member (op =) syms_all (Constant c)) cs
  14.200        then SOME (name, content) else NONE;
  14.201      val includes = map_filter select_include (Code_Symbol.dest_module_data printings);
  14.202    in
  14.203 -    (serializer args (Proof_Context.init_global thy) {
  14.204 +    (serializer args ctxt {
  14.205        module_name = module_name,
  14.206        reserved_syms = reserved,
  14.207        identifiers = identifiers,
  14.208 @@ -355,62 +356,62 @@
  14.209        (syms_all, program))
  14.210    end;
  14.211  
  14.212 -fun mount_serializer thy target some_width module_name args program syms =
  14.213 +fun mount_serializer ctxt target some_width module_name args program syms =
  14.214    let
  14.215 -    val (default_width, data, modify) = activate_target thy target;
  14.216 +    val (default_width, data, modify) = activate_target ctxt target;
  14.217      val serializer = case the_description data
  14.218       of Fundamental seri => #serializer seri;
  14.219      val (prepared_serializer, (prepared_syms, prepared_program)) =
  14.220 -      prepare_serializer thy serializer
  14.221 +      prepare_serializer ctxt serializer
  14.222          (the_reserved data) (the_identifiers data) (the_printings data)
  14.223          module_name args (modify program) syms
  14.224      val width = the_default default_width some_width;
  14.225    in (fn program => fn syms => prepared_serializer syms program width, (prepared_syms, prepared_program)) end;
  14.226  
  14.227 -fun invoke_serializer thy target some_width raw_module_name args program all_public syms =
  14.228 +fun invoke_serializer ctxt target some_width raw_module_name args program all_public syms =
  14.229    let
  14.230      val module_name = if raw_module_name = "" then ""
  14.231        else (check_name true raw_module_name; raw_module_name)
  14.232 -    val (mounted_serializer, (prepared_syms, prepared_program)) = mount_serializer thy
  14.233 -      target some_width module_name args program syms;
  14.234 +    val (mounted_serializer, (prepared_syms, prepared_program)) =
  14.235 +      mount_serializer ctxt target some_width module_name args program syms;
  14.236    in mounted_serializer prepared_program (if all_public then prepared_syms else []) end;
  14.237  
  14.238  fun assert_module_name "" = error "Empty module name not allowed here"
  14.239    | assert_module_name module_name = module_name;
  14.240  
  14.241 -fun using_master_directory thy =
  14.242 -  Option.map (Path.append (File.pwd ()) o Path.append (Thy_Load.master_directory thy));
  14.243 +fun using_master_directory ctxt =
  14.244 +  Option.map (Path.append (File.pwd ()) o Path.append (Thy_Load.master_directory (Proof_Context.theory_of ctxt)));
  14.245  
  14.246  in
  14.247  
  14.248  val generatedN = "Generated_Code";
  14.249  
  14.250 -fun export_code_for thy some_path target some_width module_name args =
  14.251 -  export (using_master_directory thy some_path)
  14.252 -  ooo invoke_serializer thy target some_width module_name args;
  14.253 +fun export_code_for ctxt some_path target some_width module_name args =
  14.254 +  export (using_master_directory ctxt some_path)
  14.255 +  ooo invoke_serializer ctxt target some_width module_name args;
  14.256  
  14.257 -fun produce_code_for thy target some_width module_name args =
  14.258 +fun produce_code_for ctxt target some_width module_name args =
  14.259    let
  14.260 -    val serializer = invoke_serializer thy target some_width (assert_module_name module_name) args;
  14.261 +    val serializer = invoke_serializer ctxt target some_width (assert_module_name module_name) args;
  14.262    in fn program => fn all_public => fn syms =>
  14.263      produce (serializer program all_public syms) |> apsnd (fn deresolve => map deresolve syms)
  14.264    end;
  14.265  
  14.266 -fun present_code_for thy target some_width module_name args =
  14.267 +fun present_code_for ctxt target some_width module_name args =
  14.268    let
  14.269 -    val serializer = invoke_serializer thy target some_width (assert_module_name module_name) args;
  14.270 +    val serializer = invoke_serializer ctxt target some_width (assert_module_name module_name) args;
  14.271    in fn program => fn (syms, selects) =>
  14.272      present selects (serializer program false syms)
  14.273    end;
  14.274  
  14.275 -fun check_code_for thy target strict args program all_public syms =
  14.276 +fun check_code_for ctxt target strict args program all_public syms =
  14.277    let
  14.278      val { env_var, make_destination, make_command } =
  14.279 -      (#check o the_fundamental thy) target;
  14.280 +      (#check o the_fundamental ctxt) target;
  14.281      fun ext_check p =
  14.282        let
  14.283          val destination = make_destination p;
  14.284 -        val _ = export (SOME destination) (invoke_serializer thy target (SOME 80)
  14.285 +        val _ = export (SOME destination) (invoke_serializer ctxt target (SOME 80)
  14.286            generatedN args program all_public syms);
  14.287          val cmd = make_command generatedN;
  14.288        in
  14.289 @@ -443,10 +444,10 @@
  14.290      val value_name = the (deresolve Code_Symbol.value);
  14.291    in (program_code, value_name) end;
  14.292  
  14.293 -fun evaluator thy target program syms =
  14.294 +fun evaluator ctxt target program syms =
  14.295    let
  14.296      val (mounted_serializer, (_, prepared_program)) =
  14.297 -      mount_serializer thy target NONE generatedN [] program syms;
  14.298 +      mount_serializer ctxt target NONE generatedN [] program syms;
  14.299    in evaluation mounted_serializer prepared_program syms end;
  14.300  
  14.301  end; (* local *)
  14.302 @@ -457,60 +458,66 @@
  14.303  fun prep_destination "" = NONE
  14.304    | prep_destination s = SOME (Path.explode s);
  14.305  
  14.306 -fun export_code thy all_public cs seris =
  14.307 +fun export_code ctxt all_public cs seris =
  14.308    let
  14.309 +    val thy = Proof_Context.theory_of ctxt;
  14.310      val program = Code_Thingol.consts_program thy cs;
  14.311      val _ = map (fn (((target, module_name), some_path), args) =>
  14.312 -      export_code_for thy some_path target NONE module_name args program all_public (map Constant cs)) seris;
  14.313 +      export_code_for ctxt some_path target NONE module_name args program all_public (map Constant cs)) seris;
  14.314    in () end;
  14.315  
  14.316 -fun export_code_cmd all_public raw_cs seris thy =
  14.317 -  export_code thy all_public
  14.318 -    (Code_Thingol.read_const_exprs thy raw_cs)
  14.319 +fun export_code_cmd all_public raw_cs seris ctxt =
  14.320 +  export_code ctxt all_public
  14.321 +    (Code_Thingol.read_const_exprs ctxt raw_cs)
  14.322      ((map o apfst o apsnd) prep_destination seris);
  14.323  
  14.324 -fun produce_code thy all_public cs target some_width some_module_name args =
  14.325 +fun produce_code ctxt all_public cs target some_width some_module_name args =
  14.326    let
  14.327 +    val thy = Proof_Context.theory_of ctxt;
  14.328      val program = Code_Thingol.consts_program thy cs;
  14.329 -  in produce_code_for thy target some_width some_module_name args program all_public (map Constant cs) end;
  14.330 +  in produce_code_for ctxt target some_width some_module_name args program all_public (map Constant cs) end;
  14.331  
  14.332 -fun present_code thy cs syms target some_width some_module_name args =
  14.333 +fun present_code ctxt cs syms target some_width some_module_name args =
  14.334    let
  14.335 +    val thy = Proof_Context.theory_of ctxt;
  14.336      val program = Code_Thingol.consts_program thy cs;
  14.337 -  in present_code_for thy target some_width some_module_name args program (map Constant cs, syms) end;
  14.338 +  in present_code_for ctxt target some_width some_module_name args program (map Constant cs, syms) end;
  14.339  
  14.340 -fun check_code thy all_public cs seris =
  14.341 +fun check_code ctxt all_public cs seris =
  14.342    let
  14.343 +    val thy = Proof_Context.theory_of ctxt;
  14.344      val program = Code_Thingol.consts_program thy cs;
  14.345      val _ = map (fn ((target, strict), args) =>
  14.346 -      check_code_for thy target strict args program all_public (map Constant cs)) seris;
  14.347 +      check_code_for ctxt target strict args program all_public (map Constant cs)) seris;
  14.348    in () end;
  14.349  
  14.350 -fun check_code_cmd all_public raw_cs seris thy =
  14.351 -  check_code thy all_public
  14.352 -    (Code_Thingol.read_const_exprs thy raw_cs) seris;
  14.353 +fun check_code_cmd all_public raw_cs seris ctxt =
  14.354 +  check_code ctxt all_public
  14.355 +    (Code_Thingol.read_const_exprs ctxt raw_cs) seris;
  14.356  
  14.357  local
  14.358  
  14.359  val parse_const_terms = Scan.repeat1 Args.term
  14.360 -  >> (fn ts => fn thy => map (Code.check_const thy) ts);
  14.361 +  >> (fn ts => fn ctxt => map (Code.check_const (Proof_Context.theory_of ctxt)) ts);
  14.362  
  14.363  fun parse_names category parse internalize mark_symbol =
  14.364    Scan.lift (Args.parens (Args.$$$ category)) |-- Scan.repeat1 parse
  14.365 -  >> (fn xs => fn thy => map (mark_symbol o internalize thy) xs);
  14.366 +  >> (fn xs => fn ctxt => map (mark_symbol o internalize ctxt) xs);
  14.367  
  14.368  val parse_consts = parse_names "consts" Args.term
  14.369 -  Code.check_const Constant;
  14.370 +  (Code.check_const o Proof_Context.theory_of) Constant;
  14.371  
  14.372  val parse_types = parse_names "types" (Scan.lift Args.name)
  14.373 -  Sign.intern_type Type_Constructor;
  14.374 +  (Sign.intern_type o Proof_Context.theory_of) Type_Constructor;
  14.375  
  14.376  val parse_classes = parse_names "classes" (Scan.lift Args.name)
  14.377 -  Sign.intern_class Type_Class;
  14.378 +  (Sign.intern_class o Proof_Context.theory_of) Type_Class;
  14.379  
  14.380  val parse_instances = parse_names "instances" (Scan.lift (Args.name --| Args.$$$ "::" -- Args.name))
  14.381 -  (fn thy => fn (raw_tyco, raw_class) => (Sign.intern_class thy raw_tyco, Sign.intern_type thy raw_class))
  14.382 -    Class_Instance;
  14.383 +  (fn ctxt => fn (raw_tyco, raw_class) =>
  14.384 +    let
  14.385 +      val thy = Proof_Context.theory_of ctxt;
  14.386 +    in (Sign.intern_class thy raw_tyco, Sign.intern_type thy raw_class) end) Class_Instance;
  14.387  
  14.388  in
  14.389  
  14.390 @@ -520,11 +527,9 @@
  14.391        Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances)
  14.392        -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))
  14.393      (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target, some_width)) =>
  14.394 -      let val thy = Proof_Context.theory_of ctxt in
  14.395 -        present_code thy (mk_cs thy)
  14.396 -          (maps (fn f => f thy) mk_stmtss)
  14.397 -          target some_width "Example" []
  14.398 -      end);
  14.399 +        present_code ctxt (mk_cs ctxt)
  14.400 +          (maps (fn f => f ctxt) mk_stmtss)
  14.401 +          target some_width "Example" []);
  14.402  
  14.403  end;
  14.404  
  14.405 @@ -535,7 +540,7 @@
  14.406  
  14.407  fun add_reserved target sym thy =
  14.408    let
  14.409 -    val (_, data) = collapse_hierarchy thy target;
  14.410 +    val (_, data) = collapse_hierarchy (Proof_Context.init_global thy) target;
  14.411      val _ = if member (op =) (the_reserved data) sym
  14.412        then error ("Reserved symbol " ^ quote sym ^ " already declared")
  14.413        else ();
  14.414 @@ -547,13 +552,13 @@
  14.415  
  14.416  (* checking of syntax *)
  14.417  
  14.418 -fun check_const_syntax thy target c syn =
  14.419 -  if Code_Printer.requires_args syn > Code.args_number thy c
  14.420 +fun check_const_syntax ctxt target c syn =
  14.421 +  if Code_Printer.requires_args syn > Code.args_number (Proof_Context.theory_of ctxt) c
  14.422    then error ("Too many arguments in syntax for constant " ^ quote c)
  14.423 -  else Code_Printer.prep_const_syntax thy (the_literals thy target) c syn;
  14.424 +  else Code_Printer.prep_const_syntax (Proof_Context.theory_of ctxt) (the_literals ctxt target) c syn;
  14.425  
  14.426 -fun check_tyco_syntax thy target tyco syn =
  14.427 -  if fst syn <> Sign.arity_number thy tyco
  14.428 +fun check_tyco_syntax ctxt target tyco syn =
  14.429 +  if fst syn <> Sign.arity_number (Proof_Context.theory_of ctxt) tyco
  14.430    then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
  14.431    else syn;
  14.432  
  14.433 @@ -569,14 +574,14 @@
  14.434        (arrange false) (arrange false) (arrange true) x
  14.435    end;
  14.436  
  14.437 -fun cert_name_decls thy = cert_syms thy #> arrange_name_decls;
  14.438 +fun cert_name_decls ctxt = cert_syms ctxt #> arrange_name_decls;
  14.439  
  14.440 -fun read_name_decls thy = read_syms thy #> arrange_name_decls;
  14.441 +fun read_name_decls ctxt = read_syms ctxt #> arrange_name_decls;
  14.442  
  14.443  fun set_identifier (target, sym_name) = map_identifiers target (Code_Symbol.set_data sym_name);
  14.444  
  14.445  fun gen_set_identifiers prep_name_decl raw_name_decls thy =
  14.446 -  fold set_identifier (prep_name_decl thy raw_name_decls) thy;
  14.447 +  fold set_identifier (prep_name_decl (Proof_Context.init_global thy) raw_name_decls) thy;
  14.448  
  14.449  val set_identifiers = gen_set_identifiers cert_name_decls;
  14.450  val set_identifiers_cmd = gen_set_identifiers read_name_decls;
  14.451 @@ -584,26 +589,26 @@
  14.452  
  14.453  (* custom printings *)
  14.454  
  14.455 -fun arrange_printings prep_const thy =
  14.456 +fun arrange_printings prep_const ctxt =
  14.457    let
  14.458      fun arrange check (sym, target_syns) =
  14.459 -      map (fn (target, some_syn) => (target, (sym, Option.map (check thy target sym) some_syn))) target_syns;
  14.460 +      map (fn (target, some_syn) => (target, (sym, Option.map (check ctxt target sym) some_syn))) target_syns;
  14.461    in
  14.462      Code_Symbol.maps_attr'
  14.463        (arrange check_const_syntax) (arrange check_tyco_syntax)
  14.464          (arrange ((K o K o K) I)) (arrange ((K o K o K) I)) (arrange ((K o K o K) I))
  14.465 -        (arrange (fn thy => fn _ => fn _ => fn (raw_content, raw_cs) =>
  14.466 -          (Code_Printer.str raw_content, map (prep_const thy) raw_cs)))
  14.467 +        (arrange (fn ctxt => fn _ => fn _ => fn (raw_content, raw_cs) =>
  14.468 +          (Code_Printer.str raw_content, map (prep_const ctxt) raw_cs)))
  14.469    end;
  14.470  
  14.471 -fun cert_printings thy = cert_syms thy #> arrange_printings cert_const thy;
  14.472 +fun cert_printings ctxt = cert_syms ctxt #> arrange_printings cert_const ctxt;
  14.473  
  14.474 -fun read_printings thy = read_syms thy #> arrange_printings Code.read_const thy;
  14.475 +fun read_printings ctxt = read_syms ctxt #> arrange_printings read_const ctxt;
  14.476  
  14.477  fun set_printing (target, sym_syn) = map_printings target (Code_Symbol.set_data sym_syn);
  14.478  
  14.479  fun gen_set_printings prep_print_decl raw_print_decls thy =
  14.480 -  fold set_printing (prep_print_decl thy raw_print_decls) thy;
  14.481 +  fold set_printing (prep_print_decl (Proof_Context.init_global thy) raw_print_decls) thy;
  14.482  
  14.483  val set_printings = gen_set_printings cert_printings;
  14.484  val set_printings_cmd = gen_set_printings read_printings;
  14.485 @@ -680,18 +685,18 @@
  14.486  
  14.487  val _ =
  14.488    Outer_Syntax.command @{command_spec "export_code"} "generate executable code for constants"
  14.489 -    (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
  14.490 +    (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.context_of)));
  14.491  
  14.492  
  14.493  (** external entrance point -- for codegen tool **)
  14.494  
  14.495  fun codegen_tool thyname cmd_expr =
  14.496    let
  14.497 -    val thy = Thy_Info.get_theory thyname;
  14.498 +    val ctxt = Proof_Context.init_global (Thy_Info.get_theory thyname);
  14.499      val parse = Scan.read Token.stopper (Parse.!!! code_exprP) o
  14.500        (filter Token.is_proper o Outer_Syntax.scan Position.none);
  14.501    in case parse cmd_expr
  14.502 -   of SOME f => (writeln "Now generating code..."; f thy)
  14.503 +   of SOME f => (writeln "Now generating code..."; f ctxt)
  14.504      | NONE => error ("Bad directive " ^ quote cmd_expr)
  14.505    end;
  14.506  
    15.1 --- a/src/Tools/Code/code_thingol.ML	Wed Feb 26 10:10:38 2014 +0100
    15.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Feb 26 11:57:52 2014 +0100
    15.3 @@ -79,27 +79,28 @@
    15.4    val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt
    15.5    val is_constr: program -> Code_Symbol.T -> bool
    15.6    val is_case: stmt -> bool
    15.7 -  val group_stmts: theory -> program
    15.8 +  val group_stmts: Proof.context -> program
    15.9      -> ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list
   15.10        * ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list)) list
   15.11  
   15.12 -  val read_const_exprs: theory -> string list -> string list
   15.13 +  val read_const_exprs: Proof.context -> string list -> string list
   15.14    val consts_program: theory -> string list -> program
   15.15 -  val dynamic_conv: theory -> (program
   15.16 +  val dynamic_conv: Proof.context -> (program
   15.17      -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> conv)
   15.18      -> conv
   15.19 -  val dynamic_value: theory -> ((term -> term) -> 'a -> 'a) -> (program
   15.20 +  val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> (program
   15.21      -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> 'a)
   15.22      -> term -> 'a
   15.23 -  val static_conv: theory -> string list -> (program -> string list
   15.24 -    -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> conv)
   15.25 -    -> conv
   15.26 -  val static_conv_simple: theory -> string list
   15.27 -    -> (program -> (string * sort) list -> term -> conv) -> conv
   15.28 -  val static_value: theory -> ((term -> term) -> 'a -> 'a) -> string list ->
   15.29 +  val static_conv: Proof.context -> string list -> (program -> string list
   15.30 +    -> Proof.context -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> conv)
   15.31 +    -> Proof.context -> conv
   15.32 +  val static_conv_simple: Proof.context -> string list
   15.33 +    -> (program -> Proof.context -> (string * sort) list -> term -> conv)
   15.34 +    -> Proof.context -> conv
   15.35 +  val static_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> string list ->
   15.36      (program -> string list
   15.37 -      -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> 'a)
   15.38 -    -> term -> 'a
   15.39 +      -> Proof.context -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> 'a)
   15.40 +    -> Proof.context -> term -> 'a
   15.41  end;
   15.42  
   15.43  structure Code_Thingol: CODE_THINGOL =
   15.44 @@ -334,7 +335,7 @@
   15.45    rev (Code_Symbol.Graph.strong_conn program)
   15.46    |> map (AList.make (Code_Symbol.Graph.get_node program));
   15.47  
   15.48 -fun group_stmts thy program =
   15.49 +fun group_stmts ctxt program =
   15.50    let
   15.51      fun is_fun (_, Fun _) = true | is_fun _ = false;
   15.52      fun is_datatypecons (_, Datatypecons _) = true | is_datatypecons _ = false;
   15.53 @@ -351,8 +352,7 @@
   15.54        else if forall (is_fun orf is_classinst) stmts
   15.55        then ([], [], List.partition is_fun stmts)
   15.56        else error ("Illegal mutual dependencies: " ^ (commas
   15.57 -        o map (Code_Symbol.quote (Proof_Context.init_global thy)
   15.58 -        o fst)) stmts);
   15.59 +        o map (Code_Symbol.quote ctxt o fst)) stmts);
   15.60    in
   15.61      linear_stmts program
   15.62      |> map group
   15.63 @@ -388,12 +388,11 @@
   15.64  
   15.65  exception PERMISSIVE of unit;
   15.66  
   15.67 -fun translation_error thy program permissive some_thm deps msg sub_msg =
   15.68 +fun translation_error ctxt program permissive some_thm deps msg sub_msg =
   15.69    if permissive
   15.70    then raise PERMISSIVE ()
   15.71    else
   15.72      let
   15.73 -      val ctxt = Proof_Context.init_global thy;
   15.74        val thm_msg =
   15.75          Option.map (fn thm => "in code equation " ^ Display.string_of_thm ctxt thm) some_thm;
   15.76        val dep_msg = if null (tl deps) then NONE
   15.77 @@ -409,14 +408,14 @@
   15.78  fun maybe_permissive f prgrm =
   15.79    f prgrm |>> SOME handle PERMISSIVE () => (NONE, prgrm);
   15.80  
   15.81 -fun not_wellsorted thy program permissive some_thm deps ty sort e =
   15.82 +fun not_wellsorted ctxt program permissive some_thm deps ty sort e =
   15.83    let
   15.84 -    val err_class = Sorts.class_error (Context.pretty_global thy) e;
   15.85 +    val err_class = Sorts.class_error (Context.pretty ctxt) e;
   15.86      val err_typ =
   15.87 -      "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort " ^
   15.88 -        Syntax.string_of_sort_global thy sort;
   15.89 +      "Type " ^ Syntax.string_of_typ ctxt ty ^ " not of sort " ^
   15.90 +        Syntax.string_of_sort ctxt sort;
   15.91    in
   15.92 -    translation_error thy program permissive some_thm deps
   15.93 +    translation_error ctxt program permissive some_thm deps
   15.94        "Wellsortedness error" (err_typ ^ "\n" ^ err_class)
   15.95    end;
   15.96  
   15.97 @@ -442,25 +441,25 @@
   15.98        | tag (Free _) (t as Free _) = t
   15.99        | tag (Var _) (t as Var _) = t
  15.100        | tag (Bound _) (t as Bound _) = t;
  15.101 -  in
  15.102 -    tag
  15.103 -  end
  15.104 +  in tag end
  15.105  
  15.106 -fun annotate thy algbr eqngr (c, ty) args rhs =
  15.107 +fun annotate ctxt algbr eqngr (c, ty) args rhs =
  15.108    let
  15.109 -    val ctxt = Proof_Context.init_global thy |> Config.put Type_Infer_Context.const_sorts false
  15.110 -    val erase = map_types (fn _ => Type_Infer.anyT [])
  15.111 -    val reinfer = singleton (Type_Infer_Context.infer_types ctxt)
  15.112 -    val lhs = list_comb (Const (c, ty), map (map_types Type.strip_sorts o fst) args)
  15.113 -    val reinferred_rhs = snd (Logic.dest_equals (reinfer (Logic.mk_equals (lhs, erase rhs))))
  15.114 +    val erase = map_types (fn _ => Type_Infer.anyT []);
  15.115 +    val reinfer = singleton (Type_Infer_Context.infer_types ctxt);
  15.116 +    val lhs = list_comb (Const (c, ty), map (map_types Type.strip_sorts o fst) args);
  15.117 +    val reinferred_rhs = snd (Logic.dest_equals (reinfer (Logic.mk_equals (lhs, erase rhs))));
  15.118 +  in tag_term algbr eqngr reinferred_rhs rhs end
  15.119 +
  15.120 +fun annotate_eqns ctxt algbr eqngr (c, ty) eqns =
  15.121 +  let
  15.122 +    val ctxt' = ctxt |> Proof_Context.theory_of |> Proof_Context.init_global
  15.123 +      |> Config.put Type_Infer_Context.const_sorts false;
  15.124 +      (*avoid spurious fixed variables: there is no eigen context for equations*)
  15.125    in
  15.126 -    tag_term algbr eqngr reinferred_rhs rhs
  15.127 -  end
  15.128 -
  15.129 -fun annotate_eqns thy algbr eqngr (c, ty) eqns = 
  15.130 -  map (apfst (fn (args, (rhs, some_abs)) => (args,
  15.131 -    (annotate thy algbr eqngr (c, ty) args rhs, some_abs)))) eqns
  15.132 -
  15.133 +    map (apfst (fn (args, (rhs, some_abs)) => (args,
  15.134 +      (annotate ctxt' algbr eqngr (c, ty) args rhs, some_abs)))) eqns
  15.135 +  end;
  15.136  
  15.137  (* abstract dictionary construction *)
  15.138  
  15.139 @@ -470,7 +469,7 @@
  15.140      Global of (string * class) * typarg_witness list list
  15.141    | Local of string * (int * sort);
  15.142  
  15.143 -fun construct_dictionaries thy (proj_sort, algebra) permissive some_thm (ty, sort) (deps, program) =
  15.144 +fun construct_dictionaries ctxt (proj_sort, algebra) permissive some_thm (ty, sort) (deps, program) =
  15.145    let
  15.146      fun class_relation ((Weakening (classrels, x)), sub_class) super_class =
  15.147        Weakening ((sub_class, super_class) :: classrels, x);
  15.148 @@ -484,42 +483,44 @@
  15.149        {class_relation = K (Sorts.classrel_derivation algebra class_relation),
  15.150         type_constructor = type_constructor,
  15.151         type_variable = type_variable} (ty, proj_sort sort)
  15.152 -      handle Sorts.CLASS_ERROR e => not_wellsorted thy program permissive some_thm deps ty sort e;
  15.153 +      handle Sorts.CLASS_ERROR e => not_wellsorted ctxt program permissive some_thm deps ty sort e;
  15.154    in (typarg_witnesses, (deps, program)) end;
  15.155  
  15.156  
  15.157  (* translation *)
  15.158  
  15.159 -fun ensure_tyco thy algbr eqngr permissive tyco =
  15.160 +fun ensure_tyco ctxt algbr eqngr permissive tyco =
  15.161    let
  15.162 +    val thy = Proof_Context.theory_of ctxt;
  15.163      val ((vs, cos), _) = Code.get_type thy tyco;
  15.164      val stmt_datatype =
  15.165 -      fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
  15.166 +      fold_map (translate_tyvar_sort ctxt algbr eqngr permissive) vs
  15.167        #>> map fst
  15.168        ##>> fold_map (fn (c, (vs, tys)) =>
  15.169 -        ensure_const thy algbr eqngr permissive c
  15.170 +        ensure_const ctxt algbr eqngr permissive c
  15.171          ##>> pair (map (unprefix "'" o fst) vs)
  15.172 -        ##>> fold_map (translate_typ thy algbr eqngr permissive) tys) cos
  15.173 +        ##>> fold_map (translate_typ ctxt algbr eqngr permissive) tys) cos
  15.174        #>> Datatype;
  15.175    in ensure_stmt Type_Constructor stmt_datatype tyco end
  15.176 -and ensure_const thy algbr eqngr permissive c =
  15.177 +and ensure_const ctxt algbr eqngr permissive c =
  15.178    let
  15.179 +    val thy = Proof_Context.theory_of ctxt;
  15.180      fun stmt_datatypecons tyco =
  15.181 -      ensure_tyco thy algbr eqngr permissive tyco
  15.182 +      ensure_tyco ctxt algbr eqngr permissive tyco
  15.183        #>> Datatypecons;
  15.184      fun stmt_classparam class =
  15.185 -      ensure_class thy algbr eqngr permissive class
  15.186 +      ensure_class ctxt algbr eqngr permissive class
  15.187        #>> Classparam;
  15.188      fun stmt_fun cert = case Code.equations_of_cert thy cert
  15.189       of (_, NONE) => pair NoStmt
  15.190        | ((vs, ty), SOME eqns) =>
  15.191            let
  15.192 -            val eqns' = annotate_eqns thy algbr eqngr (c, ty) eqns
  15.193 +            val eqns' = annotate_eqns ctxt algbr eqngr (c, ty) eqns
  15.194              val some_case_cong = Code.get_case_cong thy c;
  15.195            in
  15.196 -            fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
  15.197 -            ##>> translate_typ thy algbr eqngr permissive ty
  15.198 -            ##>> translate_eqns thy algbr eqngr permissive eqns'
  15.199 +            fold_map (translate_tyvar_sort ctxt algbr eqngr permissive) vs
  15.200 +            ##>> translate_typ ctxt algbr eqngr permissive ty
  15.201 +            ##>> translate_eqns ctxt algbr eqngr permissive eqns'
  15.202              #>>
  15.203               (fn (_, NONE) => NoStmt
  15.204                 | (tyscm, SOME eqns) => Fun ((tyscm, eqns), some_case_cong))
  15.205 @@ -530,26 +531,28 @@
  15.206           of SOME class => stmt_classparam class
  15.207            | NONE => stmt_fun (Code_Preproc.cert eqngr c))
  15.208    in ensure_stmt Constant stmt_const c end
  15.209 -and ensure_class thy (algbr as (_, algebra)) eqngr permissive class =
  15.210 +and ensure_class ctxt (algbr as (_, algebra)) eqngr permissive class =
  15.211    let
  15.212 +    val thy = Proof_Context.theory_of ctxt;
  15.213      val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
  15.214      val cs = #params (Axclass.get_info thy class);
  15.215      val stmt_class =
  15.216        fold_map (fn super_class =>
  15.217 -        ensure_classrel thy algbr eqngr permissive (class, super_class)) super_classes
  15.218 -      ##>> fold_map (fn (c, ty) => ensure_const thy algbr eqngr permissive c
  15.219 -        ##>> translate_typ thy algbr eqngr permissive ty) cs
  15.220 +        ensure_classrel ctxt algbr eqngr permissive (class, super_class)) super_classes
  15.221 +      ##>> fold_map (fn (c, ty) => ensure_const ctxt algbr eqngr permissive c
  15.222 +        ##>> translate_typ ctxt algbr eqngr permissive ty) cs
  15.223        #>> (fn info => Class (unprefix "'" Name.aT, info))
  15.224    in ensure_stmt Type_Class stmt_class class end
  15.225 -and ensure_classrel thy algbr eqngr permissive (sub_class, super_class) =
  15.226 +and ensure_classrel ctxt algbr eqngr permissive (sub_class, super_class) =
  15.227    let
  15.228      val stmt_classrel =
  15.229 -      ensure_class thy algbr eqngr permissive sub_class
  15.230 -      ##>> ensure_class thy algbr eqngr permissive super_class
  15.231 +      ensure_class ctxt algbr eqngr permissive sub_class
  15.232 +      ##>> ensure_class ctxt algbr eqngr permissive super_class
  15.233        #>> Classrel;
  15.234    in ensure_stmt Class_Relation stmt_classrel (sub_class, super_class) end
  15.235 -and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (tyco, class) =
  15.236 +and ensure_inst ctxt (algbr as (_, algebra)) eqngr permissive (tyco, class) =
  15.237    let
  15.238 +    val thy = Proof_Context.theory_of ctxt;
  15.239      val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
  15.240      val these_class_params = these o try (#params o Axclass.get_info thy);
  15.241      val class_params = these_class_params class;
  15.242 @@ -562,8 +565,8 @@
  15.243      val arity_typ = Type (tyco, map TFree vs);
  15.244      val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
  15.245      fun translate_super_instance super_class =
  15.246 -      ensure_class thy algbr eqngr permissive super_class
  15.247 -      ##>> translate_dicts thy algbr eqngr permissive NONE (arity_typ, [super_class])
  15.248 +      ensure_class ctxt algbr eqngr permissive super_class
  15.249 +      ##>> translate_dicts ctxt algbr eqngr permissive NONE (arity_typ, [super_class])
  15.250        #>> (fn (super_class, [Dict ([], Dict_Const (_, dss))]) => (super_class, dss));
  15.251      fun translate_classparam_instance (c, ty) =
  15.252        let
  15.253 @@ -573,14 +576,14 @@
  15.254          val const = (apsnd Logic.unvarifyT_global o dest_Const o snd
  15.255            o Logic.dest_equals o Thm.prop_of) thm;
  15.256        in
  15.257 -        ensure_const thy algbr eqngr permissive c
  15.258 -        ##>> translate_const thy algbr eqngr permissive (SOME thm) (const, NONE)
  15.259 +        ensure_const ctxt algbr eqngr permissive c
  15.260 +        ##>> translate_const ctxt algbr eqngr permissive (SOME thm) (const, NONE)
  15.261          #>> (fn (c, IConst const') => ((c, (const', dom_length)), (thm, true)))
  15.262        end;
  15.263      val stmt_inst =
  15.264 -      ensure_class thy algbr eqngr permissive class
  15.265 -      ##>> ensure_tyco thy algbr eqngr permissive tyco
  15.266 -      ##>> fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
  15.267 +      ensure_class ctxt algbr eqngr permissive class
  15.268 +      ##>> ensure_tyco ctxt algbr eqngr permissive tyco
  15.269 +      ##>> fold_map (translate_tyvar_sort ctxt algbr eqngr permissive) vs
  15.270        ##>> fold_map translate_super_instance super_classes
  15.271        ##>> fold_map translate_classparam_instance class_params
  15.272        ##>> fold_map translate_classparam_instance superclass_params
  15.273 @@ -588,69 +591,72 @@
  15.274            Classinst { class = class, tyco = tyco, vs = vs,
  15.275              superinsts = superinsts, inst_params = inst_params, superinst_params = superinst_params });
  15.276    in ensure_stmt Class_Instance stmt_inst (tyco, class) end
  15.277 -and translate_typ thy algbr eqngr permissive (TFree (v, _)) =
  15.278 +and translate_typ ctxt algbr eqngr permissive (TFree (v, _)) =
  15.279        pair (ITyVar (unprefix "'" v))
  15.280 -  | translate_typ thy algbr eqngr permissive (Type (tyco, tys)) =
  15.281 -      ensure_tyco thy algbr eqngr permissive tyco
  15.282 -      ##>> fold_map (translate_typ thy algbr eqngr permissive) tys
  15.283 +  | translate_typ ctxt algbr eqngr permissive (Type (tyco, tys)) =
  15.284 +      ensure_tyco ctxt algbr eqngr permissive tyco
  15.285 +      ##>> fold_map (translate_typ ctxt algbr eqngr permissive) tys
  15.286        #>> (fn (tyco, tys) => tyco `%% tys)
  15.287 -and translate_term thy algbr eqngr permissive some_thm (Const (c, ty), some_abs) =
  15.288 -      translate_app thy algbr eqngr permissive some_thm (((c, ty), []), some_abs)
  15.289 -  | translate_term thy algbr eqngr permissive some_thm (Free (v, _), some_abs) =
  15.290 +and translate_term ctxt algbr eqngr permissive some_thm (Const (c, ty), some_abs) =
  15.291 +      translate_app ctxt algbr eqngr permissive some_thm (((c, ty), []), some_abs)
  15.292 +  | translate_term ctxt algbr eqngr permissive some_thm (Free (v, _), some_abs) =
  15.293        pair (IVar (SOME v))
  15.294 -  | translate_term thy algbr eqngr permissive some_thm (Abs (v, ty, t), some_abs) =
  15.295 +  | translate_term ctxt algbr eqngr permissive some_thm (Abs (v, ty, t), some_abs) =
  15.296        let
  15.297          val (v', t') = Syntax_Trans.variant_abs (Name.desymbolize false v, ty, t);
  15.298          val v'' = if member (op =) (Term.add_free_names t' []) v'
  15.299            then SOME v' else NONE
  15.300        in
  15.301 -        translate_typ thy algbr eqngr permissive ty
  15.302 -        ##>> translate_term thy algbr eqngr permissive some_thm (t', some_abs)
  15.303 +        translate_typ ctxt algbr eqngr permissive ty
  15.304 +        ##>> translate_term ctxt algbr eqngr permissive some_thm (t', some_abs)
  15.305          #>> (fn (ty, t) => (v'', ty) `|=> t)
  15.306        end
  15.307 -  | translate_term thy algbr eqngr permissive some_thm (t as _ $ _, some_abs) =
  15.308 +  | translate_term ctxt algbr eqngr permissive some_thm (t as _ $ _, some_abs) =
  15.309        case strip_comb t
  15.310         of (Const (c, ty), ts) =>
  15.311 -            translate_app thy algbr eqngr permissive some_thm (((c, ty), ts), some_abs)
  15.312 +            translate_app ctxt algbr eqngr permissive some_thm (((c, ty), ts), some_abs)
  15.313          | (t', ts) =>
  15.314 -            translate_term thy algbr eqngr permissive some_thm (t', some_abs)
  15.315 -            ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts
  15.316 +            translate_term ctxt algbr eqngr permissive some_thm (t', some_abs)
  15.317 +            ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) ts
  15.318              #>> (fn (t, ts) => t `$$ ts)
  15.319 -and translate_eqn thy algbr eqngr permissive ((args, (rhs, some_abs)), (some_thm, proper)) =
  15.320 -  fold_map (translate_term thy algbr eqngr permissive some_thm) args
  15.321 -  ##>> translate_term thy algbr eqngr permissive some_thm (rhs, some_abs)
  15.322 +and translate_eqn ctxt algbr eqngr permissive ((args, (rhs, some_abs)), (some_thm, proper)) =
  15.323 +  fold_map (translate_term ctxt algbr eqngr permissive some_thm) args
  15.324 +  ##>> translate_term ctxt algbr eqngr permissive some_thm (rhs, some_abs)
  15.325    #>> rpair (some_thm, proper)
  15.326 -and translate_eqns thy algbr eqngr permissive eqns =
  15.327 -  maybe_permissive (fold_map (translate_eqn thy algbr eqngr permissive) eqns)
  15.328 -and translate_const thy algbr eqngr permissive some_thm ((c, ty), some_abs) (deps, program) =
  15.329 +and translate_eqns ctxt algbr eqngr permissive eqns =
  15.330 +  maybe_permissive (fold_map (translate_eqn ctxt algbr eqngr permissive) eqns)
  15.331 +and translate_const ctxt algbr eqngr permissive some_thm ((c, ty), some_abs) (deps, program) =
  15.332    let
  15.333 +    val thy = Proof_Context.theory_of ctxt;
  15.334      val _ = if (case some_abs of NONE => true | SOME abs => not (c = abs))
  15.335          andalso Code.is_abstr thy c
  15.336 -        then translation_error thy program permissive some_thm deps
  15.337 +        then translation_error ctxt program permissive some_thm deps
  15.338            "Abstraction violation" ("constant " ^ Code.string_of_const thy c)
  15.339        else ()
  15.340 -  in translate_const_proper thy algbr eqngr permissive some_thm (c, ty) (deps, program) end
  15.341 -and translate_const_proper thy algbr eqngr permissive some_thm (c, ty) =
  15.342 +  in translate_const_proper ctxt algbr eqngr permissive some_thm (c, ty) (deps, program) end
  15.343 +and translate_const_proper ctxt algbr eqngr permissive some_thm (c, ty) =
  15.344    let
  15.345 +    val thy = Proof_Context.theory_of ctxt;
  15.346      val (annotate, ty') = dest_tagged_type ty;
  15.347      val typargs = Sign.const_typargs thy (c, ty');
  15.348      val sorts = Code_Preproc.sortargs eqngr c;
  15.349      val (dom, range) = Term.strip_type ty';
  15.350    in
  15.351 -    ensure_const thy algbr eqngr permissive c
  15.352 -    ##>> fold_map (translate_typ thy algbr eqngr permissive) typargs
  15.353 -    ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (typargs ~~ sorts)
  15.354 -    ##>> fold_map (translate_typ thy algbr eqngr permissive) (range :: dom)
  15.355 +    ensure_const ctxt algbr eqngr permissive c
  15.356 +    ##>> fold_map (translate_typ ctxt algbr eqngr permissive) typargs
  15.357 +    ##>> fold_map (translate_dicts ctxt algbr eqngr permissive some_thm) (typargs ~~ sorts)
  15.358 +    ##>> fold_map (translate_typ ctxt algbr eqngr permissive) (range :: dom)
  15.359      #>> (fn (((c, typargs), dss), range :: dom) =>
  15.360        IConst { sym = Constant c, typargs = typargs, dicts = dss,
  15.361          dom = dom, range = range, annotate = annotate })
  15.362    end
  15.363 -and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
  15.364 -  translate_const thy algbr eqngr permissive some_thm (c_ty, some_abs)
  15.365 -  ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts
  15.366 +and translate_app_const ctxt algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
  15.367 +  translate_const ctxt algbr eqngr permissive some_thm (c_ty, some_abs)
  15.368 +  ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) ts
  15.369    #>> (fn (t, ts) => t `$$ ts)
  15.370 -and translate_case thy algbr eqngr permissive some_thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
  15.371 +and translate_case ctxt algbr eqngr permissive some_thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
  15.372    let
  15.373 +    val thy = Proof_Context.theory_of ctxt;
  15.374      val undefineds = Code.undefineds thy;
  15.375      fun arg_types num_args ty = fst (chop num_args (binder_types ty));
  15.376      val tys = arg_types num_args (snd c_ty);
  15.377 @@ -696,53 +702,53 @@
  15.378                  (case_pats ~~ ts_clause)));
  15.379        in ICase { term = t, typ = ty, clauses = clauses, primitive = t_app `$$ ts } end;
  15.380    in
  15.381 -    translate_const thy algbr eqngr permissive some_thm (c_ty, NONE)
  15.382 -    ##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr permissive some_thm (constr, NONE)
  15.383 +    translate_const ctxt algbr eqngr permissive some_thm (c_ty, NONE)
  15.384 +    ##>> fold_map (fn (constr, n) => translate_const ctxt algbr eqngr permissive some_thm (constr, NONE)
  15.385        #>> rpair n) constrs
  15.386 -    ##>> translate_typ thy algbr eqngr permissive ty
  15.387 -    ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts
  15.388 +    ##>> translate_typ ctxt algbr eqngr permissive ty
  15.389 +    ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) ts
  15.390      #>> (fn (((t, constrs), ty), ts) =>
  15.391        casify constrs ty t ts)
  15.392    end
  15.393 -and translate_app_case thy algbr eqngr permissive some_thm (case_scheme as (num_args, _)) ((c, ty), ts) =
  15.394 +and translate_app_case ctxt algbr eqngr permissive some_thm (case_scheme as (num_args, _)) ((c, ty), ts) =
  15.395    if length ts < num_args then
  15.396      let
  15.397        val k = length ts;
  15.398        val tys = (take (num_args - k) o drop k o fst o strip_type) ty;
  15.399 -      val ctxt = (fold o fold_aterms) Term.declare_term_frees ts Name.context;
  15.400 -      val vs = Name.invent_names ctxt "a" tys;
  15.401 +      val names = (fold o fold_aterms) Term.declare_term_frees ts Name.context;
  15.402 +      val vs = Name.invent_names names "a" tys;
  15.403      in
  15.404 -      fold_map (translate_typ thy algbr eqngr permissive) tys
  15.405 -      ##>> translate_case thy algbr eqngr permissive some_thm case_scheme ((c, ty), ts @ map Free vs)
  15.406 +      fold_map (translate_typ ctxt algbr eqngr permissive) tys
  15.407 +      ##>> translate_case ctxt algbr eqngr permissive some_thm case_scheme ((c, ty), ts @ map Free vs)
  15.408        #>> (fn (tys, t) => map2 (fn (v, _) => pair (SOME v)) vs tys `|==> t)
  15.409      end
  15.410    else if length ts > num_args then
  15.411 -    translate_case thy algbr eqngr permissive some_thm case_scheme ((c, ty), take num_args ts)
  15.412 -    ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) (drop num_args ts)
  15.413 +    translate_case ctxt algbr eqngr permissive some_thm case_scheme ((c, ty), take num_args ts)
  15.414 +    ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) (drop num_args ts)
  15.415      #>> (fn (t, ts) => t `$$ ts)
  15.416    else
  15.417 -    translate_case thy algbr eqngr permissive some_thm case_scheme ((c, ty), ts)
  15.418 -and translate_app thy algbr eqngr permissive some_thm (c_ty_ts as ((c, _), _), some_abs) =
  15.419 -  case Code.get_case_scheme thy c
  15.420 -   of SOME case_scheme => translate_app_case thy algbr eqngr permissive some_thm case_scheme c_ty_ts
  15.421 -    | NONE => translate_app_const thy algbr eqngr permissive some_thm (c_ty_ts, some_abs)
  15.422 -and translate_tyvar_sort thy (algbr as (proj_sort, _)) eqngr permissive (v, sort) =
  15.423 -  fold_map (ensure_class thy algbr eqngr permissive) (proj_sort sort)
  15.424 +    translate_case ctxt algbr eqngr permissive some_thm case_scheme ((c, ty), ts)
  15.425 +and translate_app ctxt algbr eqngr permissive some_thm (c_ty_ts as ((c, _), _), some_abs) =
  15.426 +  case Code.get_case_scheme (Proof_Context.theory_of ctxt) c
  15.427 +   of SOME case_scheme => translate_app_case ctxt algbr eqngr permissive some_thm case_scheme c_ty_ts
  15.428 +    | NONE => translate_app_const ctxt algbr eqngr permissive some_thm (c_ty_ts, some_abs)
  15.429 +and translate_tyvar_sort ctxt (algbr as (proj_sort, _)) eqngr permissive (v, sort) =
  15.430 +  fold_map (ensure_class ctxt algbr eqngr permissive) (proj_sort sort)
  15.431    #>> (fn sort => (unprefix "'" v, sort))
  15.432 -and translate_dicts thy algbr eqngr permissive some_thm (ty, sort) =
  15.433 +and translate_dicts ctxt algbr eqngr permissive some_thm (ty, sort) =
  15.434    let
  15.435      fun mk_dict (Weakening (classrels, x)) =
  15.436 -          fold_map (ensure_classrel thy algbr eqngr permissive) classrels
  15.437 +          fold_map (ensure_classrel ctxt algbr eqngr permissive) classrels
  15.438            ##>> mk_plain_dict x
  15.439            #>> Dict 
  15.440      and mk_plain_dict (Global (inst, dss)) =
  15.441 -          ensure_inst thy algbr eqngr permissive inst
  15.442 +          ensure_inst ctxt algbr eqngr permissive inst
  15.443            ##>> (fold_map o fold_map) mk_dict dss
  15.444            #>> (fn (inst, dss) => Dict_Const (inst, dss))
  15.445        | mk_plain_dict (Local (v, (n, sort))) =
  15.446            pair (Dict_Var (unprefix "'" v, (n, length sort)))
  15.447    in
  15.448 -    construct_dictionaries thy algbr permissive some_thm (ty, sort)
  15.449 +    construct_dictionaries ctxt algbr permissive some_thm (ty, sort)
  15.450      #-> (fn typarg_witnesses => fold_map mk_dict typarg_witnesses)
  15.451    end;
  15.452  
  15.453 @@ -758,7 +764,7 @@
  15.454  fun invoke_generation ignore_cache thy (algebra, eqngr) generate thing =
  15.455    Program.change_yield (if ignore_cache then NONE else SOME thy)
  15.456      (fn program => ([], program)
  15.457 -      |> generate thy algebra eqngr thing
  15.458 +      |> generate (Proof_Context.init_global thy) algebra eqngr thing
  15.459        |-> (fn thing => fn (_, program) => (thing, program)));
  15.460  
  15.461  
  15.462 @@ -766,8 +772,8 @@
  15.463  
  15.464  fun consts_program_internal thy permissive consts =
  15.465    let
  15.466 -    fun generate_consts thy algebra eqngr =
  15.467 -      fold_map (ensure_const thy algebra eqngr permissive);
  15.468 +    fun generate_consts ctxt algebra eqngr =
  15.469 +      fold_map (ensure_const ctxt algebra eqngr permissive);
  15.470    in
  15.471      invoke_generation permissive thy (Code_Preproc.obtain false thy consts [])
  15.472        generate_consts consts
  15.473 @@ -789,17 +795,17 @@
  15.474  
  15.475  (* value evaluation *)
  15.476  
  15.477 -fun ensure_value thy algbr eqngr t =
  15.478 +fun ensure_value ctxt algbr eqngr t =
  15.479    let
  15.480      val ty = fastype_of t;
  15.481      val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
  15.482        o dest_TFree))) t [];
  15.483 -    val t' = annotate thy algbr eqngr (@{const_name dummy_pattern}, ty) [] t;
  15.484 +    val t' = annotate ctxt algbr eqngr (@{const_name dummy_pattern}, ty) [] t;
  15.485      val dummy_constant = Constant @{const_name dummy_pattern};
  15.486      val stmt_value =
  15.487 -      fold_map (translate_tyvar_sort thy algbr eqngr false) vs
  15.488 -      ##>> translate_typ thy algbr eqngr false ty
  15.489 -      ##>> translate_term thy algbr eqngr false NONE (t', NONE)
  15.490 +      fold_map (translate_tyvar_sort ctxt algbr eqngr false) vs
  15.491 +      ##>> translate_typ ctxt algbr eqngr false ty
  15.492 +      ##>> translate_term ctxt algbr eqngr false NONE (t', NONE)
  15.493        #>> (fn ((vs, ty), t) => Fun
  15.494          (((vs, ty), [(([], t), (NONE, true))]), NONE));
  15.495      fun term_value (deps, program1) =
  15.496 @@ -820,62 +826,61 @@
  15.497  fun original_sorts vs =
  15.498    map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v));
  15.499  
  15.500 -fun dynamic_evaluator thy evaluator algebra eqngr vs t =
  15.501 +fun dynamic_evaluator ctxt evaluator algebra eqngr vs t =
  15.502    let
  15.503      val ((program, (((vs', ty'), t'), deps)), _) =
  15.504 -      invoke_generation false thy (algebra, eqngr) ensure_value t;
  15.505 +      invoke_generation false (Proof_Context.theory_of ctxt) (algebra, eqngr) ensure_value t;
  15.506    in evaluator program ((original_sorts vs vs', (vs', ty')), t') deps end;
  15.507  
  15.508 -fun dynamic_conv thy evaluator =
  15.509 -  Code_Preproc.dynamic_conv thy (dynamic_evaluator thy evaluator);
  15.510 +fun dynamic_conv ctxt conv =
  15.511 +  Code_Preproc.dynamic_conv ctxt (dynamic_evaluator ctxt conv);
  15.512  
  15.513 -fun dynamic_value thy postproc evaluator =
  15.514 -  Code_Preproc.dynamic_value thy postproc (dynamic_evaluator thy evaluator);
  15.515 +fun dynamic_value ctxt postproc evaluator =
  15.516 +  Code_Preproc.dynamic_value ctxt postproc (dynamic_evaluator ctxt evaluator);
  15.517  
  15.518 -fun lift_evaluation thy evaluation' algebra eqngr program vs t =
  15.519 +fun lift_evaluation ctxt evaluation algebra eqngr program vs t =
  15.520    let
  15.521      val ((_, (((vs', ty'), t'), deps)), _) =
  15.522 -      ensure_value thy algebra eqngr t ([], program);
  15.523 -  in evaluation' ((original_sorts vs vs', (vs', ty')), t') deps end;
  15.524 +      ensure_value ctxt algebra eqngr t ([], program);
  15.525 +  in evaluation ctxt ((original_sorts vs vs', (vs', ty')), t') deps end;
  15.526  
  15.527 -fun lift_evaluator thy evaluator' consts algebra eqngr =
  15.528 +fun lift_evaluator ctxt evaluator consts algebra eqngr =
  15.529    let
  15.530 -    fun generate_consts thy algebra eqngr =
  15.531 -      fold_map (ensure_const thy algebra eqngr false);
  15.532 +    fun generate_consts ctxt algebra eqngr =
  15.533 +      fold_map (ensure_const ctxt algebra eqngr false);
  15.534      val (consts', program) =
  15.535 -      invoke_generation true thy (algebra, eqngr) generate_consts consts;
  15.536 -    val evaluation' = evaluator' program consts';
  15.537 -  in lift_evaluation thy evaluation' algebra eqngr program end;
  15.538 +      invoke_generation true (Proof_Context.theory_of ctxt) (algebra, eqngr) generate_consts consts;
  15.539 +    val evaluation = evaluator program consts';
  15.540 +  in fn ctxt' => lift_evaluation ctxt' evaluation algebra eqngr program end;
  15.541  
  15.542 -fun lift_evaluator_simple thy evaluator' consts algebra eqngr =
  15.543 +fun lift_evaluator_simple ctxt evaluator consts algebra eqngr =
  15.544    let
  15.545 -    fun generate_consts thy algebra eqngr =
  15.546 -      fold_map (ensure_const thy algebra eqngr false);
  15.547 +    fun generate_consts ctxt algebra eqngr =
  15.548 +      fold_map (ensure_const ctxt algebra eqngr false);
  15.549      val (_, program) =
  15.550 -      invoke_generation true thy (algebra, eqngr) generate_consts consts;
  15.551 -  in evaluator' program end;
  15.552 +      invoke_generation true (Proof_Context.theory_of ctxt) (algebra, eqngr) generate_consts consts;
  15.553 +  in evaluator program end;
  15.554  
  15.555 -fun static_conv thy consts conv =
  15.556 -  Code_Preproc.static_conv thy consts (lift_evaluator thy conv consts);
  15.557 +fun static_conv ctxt consts conv =
  15.558 +  Code_Preproc.static_conv ctxt consts (lift_evaluator ctxt conv consts);
  15.559  
  15.560 -fun static_conv_simple thy consts conv =
  15.561 -  Code_Preproc.static_conv thy consts (lift_evaluator_simple thy conv consts);
  15.562 +fun static_conv_simple ctxt consts conv =
  15.563 +  Code_Preproc.static_conv ctxt consts (lift_evaluator_simple ctxt conv consts);
  15.564  
  15.565 -fun static_value thy postproc consts evaluator =
  15.566 -  Code_Preproc.static_value thy postproc consts (lift_evaluator thy evaluator consts);
  15.567 +fun static_value ctxt postproc consts evaluator =
  15.568 +  Code_Preproc.static_value ctxt postproc consts (lift_evaluator ctxt evaluator consts);
  15.569  
  15.570  
  15.571  (** constant expressions **)
  15.572  
  15.573 -fun read_const_exprs_internal thy =
  15.574 +fun read_const_exprs_internal ctxt =
  15.575    let
  15.576 +    val thy = Proof_Context.theory_of ctxt;
  15.577      fun consts_of thy' = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
  15.578        ((snd o #constants o Consts.dest o Sign.consts_of) thy') [];
  15.579      fun belongs_here thy' c = forall
  15.580        (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy');
  15.581      fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');
  15.582 -
  15.583 -    val ctxt = Proof_Context.init_global thy;
  15.584      fun read_const_expr str =
  15.585        (case Syntax.parse_token ctxt (K NONE) Markup.empty (SOME o Symbol_Pos.implode o #1) str of
  15.586          SOME "_" => ([], consts_of thy)
  15.587 @@ -886,28 +891,30 @@
  15.588        | NONE => ([Code.read_const thy str], []));
  15.589    in pairself flat o split_list o map read_const_expr end;
  15.590  
  15.591 -fun read_const_exprs_all thy = op @ o read_const_exprs_internal thy;
  15.592 +fun read_const_exprs_all ctxt = op @ o read_const_exprs_internal ctxt;
  15.593  
  15.594 -fun read_const_exprs thy const_exprs =
  15.595 +fun read_const_exprs ctxt const_exprs =
  15.596    let
  15.597 -    val (consts, consts_permissive) = read_const_exprs_internal thy const_exprs;
  15.598 -    val consts' = implemented_deps (consts_program_permissive thy consts_permissive);
  15.599 +    val (consts, consts_permissive) = read_const_exprs_internal ctxt const_exprs;
  15.600 +    val consts' = implemented_deps
  15.601 +      (consts_program_permissive ((Proof_Context.theory_of ctxt)) consts_permissive);
  15.602    in union (op =) consts' consts end;
  15.603  
  15.604  
  15.605  (** diagnostic commands **)
  15.606  
  15.607 -fun code_depgr thy consts =
  15.608 +fun code_depgr ctxt consts =
  15.609    let
  15.610 -    val (_, eqngr) = Code_Preproc.obtain true thy consts [];
  15.611 +    val (_, eqngr) = Code_Preproc.obtain true ((Proof_Context.theory_of ctxt)) consts [];
  15.612      val all_consts = Graph.all_succs eqngr consts;
  15.613    in Graph.restrict (member (op =) all_consts) eqngr end;
  15.614  
  15.615 -fun code_thms thy = Pretty.writeln o Code_Preproc.pretty thy o code_depgr thy;
  15.616 +fun code_thms ctxt = Pretty.writeln o Code_Preproc.pretty ctxt o code_depgr ctxt;
  15.617  
  15.618 -fun code_deps thy consts =
  15.619 +fun code_deps ctxt consts =
  15.620    let
  15.621 -    val eqngr = code_depgr thy consts;
  15.622 +    val thy = Proof_Context.theory_of ctxt;
  15.623 +    val eqngr = code_depgr ctxt consts;
  15.624      val constss = Graph.strong_conn eqngr;
  15.625      val mapping = Symtab.empty |> fold (fn consts => fold (fn const =>
  15.626        Symtab.update (const, consts)) consts) constss;
  15.627 @@ -926,8 +933,8 @@
  15.628  
  15.629  local
  15.630  
  15.631 -fun code_thms_cmd thy = code_thms thy o read_const_exprs_all thy;
  15.632 -fun code_deps_cmd thy = code_deps thy o read_const_exprs_all thy;
  15.633 +fun code_thms_cmd ctxt = code_thms ctxt o read_const_exprs_all ctxt;
  15.634 +fun code_deps_cmd ctxt = code_deps ctxt o read_const_exprs_all ctxt;
  15.635  
  15.636  in
  15.637  
  15.638 @@ -935,15 +942,15 @@
  15.639    Outer_Syntax.improper_command @{command_spec "code_thms"}
  15.640      "print system of code equations for code"
  15.641      (Scan.repeat1 Parse.term >> (fn cs =>
  15.642 -      Toplevel.unknown_theory o
  15.643 -      Toplevel.keep (fn state => code_thms_cmd (Toplevel.theory_of state) cs)));
  15.644 +      Toplevel.unknown_context o
  15.645 +      Toplevel.keep (fn state => code_thms_cmd (Toplevel.context_of state) cs)));
  15.646  
  15.647  val _ =
  15.648    Outer_Syntax.improper_command @{command_spec "code_deps"}
  15.649      "visualize dependencies of code equations for code"
  15.650      (Scan.repeat1 Parse.term >> (fn cs =>
  15.651 -      Toplevel.unknown_theory o
  15.652 -      Toplevel.keep (fn state => code_deps_cmd (Toplevel.theory_of state) cs)));
  15.653 +      Toplevel.unknown_context o
  15.654 +      Toplevel.keep (fn state => code_deps_cmd (Toplevel.context_of state) cs)));
  15.655  
  15.656  end;
  15.657  
    16.1 --- a/src/Tools/nbe.ML	Wed Feb 26 10:10:38 2014 +0100
    16.2 +++ b/src/Tools/nbe.ML	Wed Feb 26 11:57:52 2014 +0100
    16.3 @@ -6,10 +6,10 @@
    16.4  
    16.5  signature NBE =
    16.6  sig
    16.7 -  val dynamic_conv: theory -> conv
    16.8 -  val dynamic_value: theory -> term -> term
    16.9 -  val static_conv: theory -> string list -> conv
   16.10 -  val static_value: theory -> string list -> term -> term
   16.11 +  val dynamic_conv: Proof.context -> conv
   16.12 +  val dynamic_value: Proof.context -> term -> term
   16.13 +  val static_conv: Proof.context -> string list -> Proof.context -> conv
   16.14 +  val static_value: Proof.context -> string list -> Proof.context -> term -> term
   16.15  
   16.16    datatype Univ =
   16.17        Const of int * Univ list               (*named (uninterpreted) constants*)
   16.18 @@ -83,8 +83,9 @@
   16.19  
   16.20  in
   16.21  
   16.22 -fun lift_triv_classes_conv thy conv ct =
   16.23 +fun lift_triv_classes_conv ctxt conv ct =
   16.24    let
   16.25 +    val thy = Proof_Context.theory_of ctxt;
   16.26      val algebra = Sign.classes_of thy;
   16.27      val certT = Thm.ctyp_of thy;
   16.28      val triv_classes = get_triv_classes thy;
   16.29 @@ -128,8 +129,9 @@
   16.30      |> strip_of_class
   16.31    end;
   16.32  
   16.33 -fun lift_triv_classes_rew thy rew t =
   16.34 +fun lift_triv_classes_rew ctxt rew t =
   16.35    let
   16.36 +    val thy = Proof_Context.theory_of ctxt;
   16.37      val algebra = Sign.classes_of thy;
   16.38      val triv_classes = get_triv_classes thy;
   16.39      val vs = Term.add_tfrees t [];
   16.40 @@ -388,10 +390,9 @@
   16.41  
   16.42  (* compile equations *)
   16.43  
   16.44 -fun compile_eqnss thy nbe_program raw_deps [] = []
   16.45 -  | compile_eqnss thy nbe_program raw_deps eqnss =
   16.46 +fun compile_eqnss ctxt nbe_program raw_deps [] = []
   16.47 +  | compile_eqnss ctxt nbe_program raw_deps eqnss =
   16.48        let
   16.49 -        val ctxt = Proof_Context.init_global thy;
   16.50          val (deps, deps_vals) = split_list (map_filter
   16.51            (fn dep => Option.map (fn univ => (dep, univ)) (fst ((Code_Symbol.Graph.get_node nbe_program dep)))) raw_deps);
   16.52          val idx_of = raw_deps
   16.53 @@ -453,7 +454,7 @@
   16.54    else (Code_Symbol.Graph.new_node (name, (NONE, maxidx)) nbe_program,
   16.55      (maxidx + 1, Inttab.update_new (maxidx, name) idx_tab));
   16.56  
   16.57 -fun compile_stmts thy stmts_deps =
   16.58 +fun compile_stmts ctxt stmts_deps =
   16.59    let
   16.60      val names = map (fst o fst) stmts_deps;
   16.61      val names_deps = map (fn ((name, _), deps) => (name, deps)) stmts_deps;
   16.62 @@ -463,7 +464,7 @@
   16.63        |> distinct (op =)
   16.64        |> fold (insert (op =)) names;
   16.65      fun compile nbe_program = eqnss
   16.66 -      |> compile_eqnss thy nbe_program refl_deps
   16.67 +      |> compile_eqnss ctxt nbe_program refl_deps
   16.68        |> rpair nbe_program;
   16.69    in
   16.70      fold ensure_const_idx refl_deps
   16.71 @@ -472,12 +473,12 @@
   16.72        #-> fold (fn (name, univ) => (Code_Symbol.Graph.map_node name o apfst) (K (SOME univ))))
   16.73    end;
   16.74  
   16.75 -fun compile_program thy program =
   16.76 +fun compile_program ctxt program =
   16.77    let
   16.78      fun add_stmts names (nbe_program, (maxidx, idx_tab)) = if exists ((can o Code_Symbol.Graph.get_node) nbe_program) names
   16.79        then (nbe_program, (maxidx, idx_tab))
   16.80        else (nbe_program, (maxidx, idx_tab))
   16.81 -        |> compile_stmts thy (map (fn name => ((name, Code_Symbol.Graph.get_node program name),
   16.82 +        |> compile_stmts ctxt (map (fn name => ((name, Code_Symbol.Graph.get_node program name),
   16.83            Code_Symbol.Graph.immediate_succs program name)) names);
   16.84    in
   16.85      fold_rev add_stmts (Code_Symbol.Graph.strong_conn program)
   16.86 @@ -488,12 +489,12 @@
   16.87  
   16.88  (* term evaluation by compilation *)
   16.89  
   16.90 -fun compile_term thy nbe_program deps (vs : (string * sort) list, t) =
   16.91 +fun compile_term ctxt nbe_program deps (vs : (string * sort) list, t) =
   16.92    let 
   16.93      val dict_frees = maps (fn (v, sort) => map_index (curry DFree v o fst) sort) vs;
   16.94    in
   16.95      (Code_Symbol.value, (vs, [([], t)]))
   16.96 -    |> singleton (compile_eqnss thy nbe_program deps)
   16.97 +    |> singleton (compile_eqnss ctxt nbe_program deps)
   16.98      |> snd
   16.99      |> (fn t => apps t (rev dict_frees))
  16.100    end;
  16.101 @@ -506,7 +507,7 @@
  16.102    | typ_of_itype vs (ITyVar v) =
  16.103        TFree ("'" ^ v, (the o AList.lookup (op =) vs) v);
  16.104  
  16.105 -fun term_of_univ thy (idx_tab : Code_Symbol.T Inttab.table) t =
  16.106 +fun term_of_univ ctxt (idx_tab : Code_Symbol.T Inttab.table) t =
  16.107    let
  16.108      fun take_until f [] = []
  16.109        | take_until f (x :: xs) = if f x then [] else x :: take_until f xs;
  16.110 @@ -527,7 +528,7 @@
  16.111              val const = const_of_idx idx;
  16.112              val T = map_type_tvar (fn ((v, i), _) =>
  16.113                Type_Infer.param typidx (v ^ string_of_int i, []))
  16.114 -                (Sign.the_const_type thy const);
  16.115 +                (Sign.the_const_type (Proof_Context.theory_of ctxt) const);
  16.116              val typidx' = typidx + 1;
  16.117            in of_apps bounds (Term.Const (const, T), ts') typidx' end
  16.118        | of_univ bounds (BVar (n, ts)) typidx =
  16.119 @@ -541,9 +542,9 @@
  16.120  
  16.121  (* evaluation with type reconstruction *)
  16.122  
  16.123 -fun eval_term thy (nbe_program, idx_tab) ((vs0, (vs, ty)), t) deps =
  16.124 +fun eval_term raw_ctxt (nbe_program, idx_tab) ((vs0, (vs, ty)), t) deps =
  16.125    let
  16.126 -    val ctxt = Syntax.init_pretty_global thy;
  16.127 +    val ctxt = Syntax.init_pretty_global (Proof_Context.theory_of raw_ctxt);
  16.128      val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
  16.129      val ty' = typ_of_itype vs0 ty;
  16.130      fun type_infer t =
  16.131 @@ -553,8 +554,8 @@
  16.132        if null (Term.add_tvars t []) then t
  16.133        else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t);
  16.134    in
  16.135 -    compile_term thy nbe_program deps (vs, t)
  16.136 -    |> term_of_univ thy idx_tab
  16.137 +    compile_term ctxt nbe_program deps (vs, t)
  16.138 +    |> term_of_univ ctxt idx_tab
  16.139      |> traced (fn t => "Normalized:\n" ^ string_of_term t)
  16.140      |> type_infer
  16.141      |> traced (fn t => "Types inferred:\n" ^ string_of_term t)
  16.142 @@ -571,18 +572,19 @@
  16.143    val empty = (Code_Symbol.Graph.empty, (0, Inttab.empty));
  16.144  );
  16.145  
  16.146 -fun compile ignore_cache thy program =
  16.147 +fun compile ignore_cache ctxt program =
  16.148    let
  16.149      val (nbe_program, (_, idx_tab)) =
  16.150 -      Nbe_Functions.change (if ignore_cache then NONE else SOME thy)
  16.151 -        (compile_program thy program);
  16.152 +      Nbe_Functions.change (if ignore_cache then NONE else SOME (Proof_Context.theory_of ctxt))
  16.153 +        (compile_program ctxt program);
  16.154    in (nbe_program, idx_tab) end;
  16.155  
  16.156  
  16.157  (* evaluation oracle *)
  16.158  
  16.159 -fun mk_equals thy lhs raw_rhs =
  16.160 +fun mk_equals ctxt lhs raw_rhs =
  16.161    let
  16.162 +    val thy = Proof_Context.theory_of ctxt;
  16.163      val ty = Thm.typ_of (Thm.ctyp_of_term lhs);
  16.164      val eq = Thm.cterm_of thy (Term.Const ("==", ty --> ty --> propT));
  16.165      val rhs = Thm.cterm_of thy raw_rhs;
  16.166 @@ -590,28 +592,33 @@
  16.167  
  16.168  val (_, raw_oracle) = Context.>>> (Context.map_theory_result
  16.169    (Thm.add_oracle (@{binding normalization_by_evaluation},
  16.170 -    fn (thy, nbe_program_idx_tab, vsp_ty_t, deps, ct) =>
  16.171 -      mk_equals thy ct (eval_term thy nbe_program_idx_tab vsp_ty_t deps))));
  16.172 +    fn (ctxt, nbe_program_idx_tab, vsp_ty_t, deps, ct) =>
  16.173 +      mk_equals ctxt ct (eval_term ctxt nbe_program_idx_tab vsp_ty_t deps))));
  16.174 +
  16.175 +fun oracle ctxt nbe_program_idx_tab vsp_ty_t deps ct =
  16.176 +  raw_oracle (ctxt, nbe_program_idx_tab, vsp_ty_t, deps, ct);
  16.177  
  16.178 -fun oracle thy nbe_program_idx_tab vsp_ty_t deps ct =
  16.179 -  raw_oracle (thy, nbe_program_idx_tab, vsp_ty_t, deps, ct);
  16.180 +fun dynamic_conv ctxt = lift_triv_classes_conv ctxt
  16.181 +  (Code_Thingol.dynamic_conv ctxt (oracle ctxt o compile false ctxt));
  16.182  
  16.183 -fun dynamic_conv thy = lift_triv_classes_conv thy
  16.184 -  (Code_Thingol.dynamic_conv thy (oracle thy o compile false thy));
  16.185 +fun dynamic_value ctxt = lift_triv_classes_rew ctxt
  16.186 +  (Code_Thingol.dynamic_value ctxt I (eval_term ctxt o compile false ctxt));
  16.187  
  16.188 -fun dynamic_value thy = lift_triv_classes_rew thy
  16.189 -  (Code_Thingol.dynamic_value thy I (eval_term thy o compile false thy));
  16.190 +fun static_conv ctxt consts =
  16.191 +  let
  16.192 +    val evaluator = Code_Thingol.static_conv ctxt consts
  16.193 +      (fn program => fn _ => K (oracle ctxt (compile true ctxt program)));
  16.194 +  in fn ctxt' => lift_triv_classes_conv ctxt' (evaluator ctxt') end;
  16.195  
  16.196 -fun static_conv thy consts = lift_triv_classes_conv thy
  16.197 -  (Code_Thingol.static_conv thy consts (K o oracle thy o compile true thy));
  16.198 -
  16.199 -fun static_value thy consts = lift_triv_classes_rew thy
  16.200 -  (Code_Thingol.static_value thy I consts (K o eval_term thy o compile true thy));
  16.201 +fun static_value ctxt consts =
  16.202 +  let
  16.203 +    val evaluator = Code_Thingol.static_value ctxt I consts
  16.204 +      (fn program => fn _ => K (eval_term ctxt (compile true ctxt program)));
  16.205 +  in fn ctxt' => lift_triv_classes_rew ctxt' (evaluator ctxt') end;
  16.206  
  16.207  
  16.208  (** setup **)
  16.209  
  16.210 -val setup = Value.add_evaluator ("nbe", dynamic_value o Proof_Context.theory_of);
  16.211 +val setup = Value.add_evaluator ("nbe", dynamic_value);
  16.212  
  16.213  end;
  16.214 - 
  16.215 \ No newline at end of file