--- a/NEWS Wed Feb 26 10:10:38 2014 +0100
+++ b/NEWS Wed Feb 26 11:57:52 2014 +0100
@@ -91,9 +91,14 @@
*** HOL ***
+* Code generator: explicit proof contexts in many ML interfaces.
+INCOMPATIBILITY.
+
* Code generator: minimize exported identifiers by default.
+Minor INCOMPATIBILITY.
* Code generation for SML and OCaml: dropped arcane "no_signatures" option.
+Minor INCOMPATIBILITY.
* Simproc "finite_Collect" is no longer enabled by default, due to
spurious crashes and other surprises. Potential INCOMPATIBILITY.
--- a/src/Doc/Codegen/Further.thy Wed Feb 26 10:10:38 2014 +0100
+++ b/src/Doc/Codegen/Further.thy Wed Feb 26 11:57:52 2014 +0100
@@ -258,7 +258,7 @@
@{index_ML Code_Preproc.map_pre: "(Proof.context -> Proof.context) -> theory -> theory"} \\
@{index_ML Code_Preproc.map_post: "(Proof.context -> Proof.context) -> theory -> theory"} \\
@{index_ML Code_Preproc.add_functrans: "
- string * (theory -> (thm * bool) list -> (thm * bool) list option)
+ string * (Proof.context -> (thm * bool) list -> (thm * bool) list option)
-> theory -> theory"} \\
@{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\
@{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\
--- a/src/HOL/HOL.thy Wed Feb 26 10:10:38 2014 +0100
+++ b/src/HOL/HOL.thy Wed Feb 26 11:57:52 2014 +0100
@@ -1903,20 +1903,21 @@
subsubsection {* Evaluation and normalization by evaluation *}
-ML {*
-fun eval_tac ctxt =
- let val conv = Code_Runtime.dynamic_holds_conv (Proof_Context.theory_of ctxt)
- in CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN' rtac TrueI end
-*}
-
-method_setup eval = {* Scan.succeed (SIMPLE_METHOD' o eval_tac) *}
- "solve goal by evaluation"
+method_setup eval = {*
+let
+ fun eval_tac ctxt =
+ let val conv = Code_Runtime.dynamic_holds_conv ctxt
+ in CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN' rtac TrueI end
+in
+ Scan.succeed (SIMPLE_METHOD' o eval_tac)
+end
+*} "solve goal by evaluation"
method_setup normalization = {*
Scan.succeed (fn ctxt =>
SIMPLE_METHOD'
(CHANGED_PROP o
- (CONVERSION (Nbe.dynamic_conv (Proof_Context.theory_of ctxt))
+ (CONVERSION (Nbe.dynamic_conv ctxt)
THEN_ALL_NEW (TRY o rtac TrueI))))
*} "solve goal by normalization"
--- a/src/HOL/Library/Code_Abstract_Nat.thy Wed Feb 26 10:10:38 2014 +0100
+++ b/src/HOL/Library/Code_Abstract_Nat.thy Wed Feb 26 11:57:52 2014 +0100
@@ -50,8 +50,9 @@
setup {*
let
-fun remove_suc thy thms =
+fun remove_suc ctxt thms =
let
+ val thy = Proof_Context.theory_of ctxt;
val vname = singleton (Name.variant_list (map fst
(fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Feb 26 10:10:38 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Feb 26 11:57:52 2014 +0100
@@ -1914,7 +1914,7 @@
in
rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Limited_Sequence.yieldn k
(Code_Runtime.dynamic_value_strict (Dseq_Random_Result.get, put_dseq_random_result, "Predicate_Compile_Core.put_dseq_random_result")
- thy NONE (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> Limited_Sequence.map proc)
+ ctxt NONE (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> Limited_Sequence.map proc)
t' [] nrandom size
|> Random_Engine.run)
depth true)) ())
@@ -1922,14 +1922,14 @@
| DSeq =>
rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Limited_Sequence.yieldn k
(Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
- thy NONE Limited_Sequence.map t' []) (Code_Numeral.natural_of_integer (the_single arguments)) true)) ())
+ ctxt NONE Limited_Sequence.map t' []) (Code_Numeral.natural_of_integer (the_single arguments)) true)) ())
| Pos_Generator_DSeq =>
let
val depth = Code_Numeral.natural_of_integer (the_single arguments)
in
rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Lazy_Sequence.yieldn k
(Code_Runtime.dynamic_value_strict (New_Dseq_Result.get, put_new_dseq_result, "Predicate_Compile_Core.put_new_dseq_result")
- thy NONE (fn proc => fn g => fn depth => g depth |> Lazy_Sequence.map proc)
+ ctxt NONE (fn proc => fn g => fn depth => g depth |> Lazy_Sequence.map proc)
t' [] depth))) ())
end
| New_Pos_Random_DSeq =>
@@ -1943,7 +1943,7 @@
(fn () => fst (Lazy_Sequence.yieldn k
(Code_Runtime.dynamic_value_strict
(Lseq_Random_Stats_Result.get, put_lseq_random_stats_result, "Predicate_Compile_Core.put_lseq_random_stats_result")
- thy NONE
+ ctxt NONE
(fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
|> Lazy_Sequence.map (apfst proc))
t' [] nrandom size seed depth))) ()))
@@ -1951,7 +1951,7 @@
(TimeLimit.timeLimit time_limit (fn () => fst (Lazy_Sequence.yieldn k
(Code_Runtime.dynamic_value_strict
(Lseq_Random_Result.get, put_lseq_random_result, "Predicate_Compile_Core.put_lseq_random_result")
- thy NONE
+ ctxt NONE
(fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
|> Lazy_Sequence.map proc)
t' [] nrandom size seed depth))) ())
@@ -1959,7 +1959,7 @@
| _ =>
rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Predicate.yieldn k
(Code_Runtime.dynamic_value_strict (Pred_Result.get, put_pred_result, "Predicate_Compile_Core.put_pred_result")
- thy NONE Predicate.map t' []))) ()))
+ ctxt NONE Predicate.map t' []))) ()))
handle TimeLimit.TimeOut => error "Reached timeout during execution of values"
in ((T, ts), statistics) end;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Feb 26 10:10:38 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Feb 26 11:57:52 2014 +0100
@@ -296,7 +296,7 @@
let
val compiled_term =
Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Quickcheck.put_dseq_result")
- thy4 (SOME target)
+ (Proof_Context.init_global thy4) (SOME target)
(fn proc => fn g => fn n => fn size => fn s => g n size s |>> (Limited_Sequence.map o map) proc)
qc_term []
in
@@ -309,7 +309,7 @@
val compiled_term =
Code_Runtime.dynamic_value_strict
(Lseq_Result.get, put_lseq_result, "Predicate_Compile_Quickcheck.put_lseq_result")
- thy4 (SOME target)
+ (Proof_Context.init_global thy4) (SOME target)
(fn proc => fn g => fn nrandom => fn size => fn s => fn depth =>
g nrandom size s depth |> (Lazy_Sequence.map o map) proc)
qc_term []
@@ -325,7 +325,7 @@
val compiled_term =
Code_Runtime.dynamic_value_strict
(New_Dseq_Result.get, put_new_dseq_result, "Predicate_Compile_Quickcheck.put_new_dseq_result")
- thy4 (SOME target)
+ (Proof_Context.init_global thy4) (SOME target)
(fn proc => fn g => fn depth => g depth |> (Lazy_Sequence.map o map) proc)
qc_term []
in
@@ -336,7 +336,7 @@
val compiled_term =
Code_Runtime.dynamic_value_strict
(CPS_Result.get, put_cps_result, "Predicate_Compile_Quickcheck.put_cps_result")
- thy4 (SOME target)
+ (Proof_Context.init_global thy4) (SOME target)
(fn proc => fn g => fn depth => g depth |> Option.map (apsnd (map proc)))
qc_term []
in
@@ -346,7 +346,7 @@
let
val compiled_term = Code_Runtime.dynamic_value_strict
(Pred_Result.get, put_pred_result, "Predicate_Compile_Quickcheck.put_pred_result")
- thy4 (SOME target) (fn proc => fn g => fn depth => fn nrandom => fn size => fn seed =>
+ (Proof_Context.init_global thy4) (SOME target) (fn proc => fn g => fn depth => fn nrandom => fn size => fn seed =>
g depth nrandom size seed |> (Predicate.map o map) proc)
qc_term []
in
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Wed Feb 26 10:10:38 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Wed Feb 26 11:57:52 2014 +0100
@@ -471,7 +471,6 @@
fun compile_generator_expr_raw ctxt ts =
let
- val thy = Proof_Context.theory_of ctxt
val mk_generator_expr =
if Config.get ctxt fast then mk_fast_generator_expr
else if Config.get ctxt bounded_forall then mk_bounded_forall_generator_expr
@@ -479,7 +478,7 @@
val t' = mk_parametric_generator_expr mk_generator_expr ctxt ts;
val compile = Code_Runtime.dynamic_value_strict
(Counterexample.get, put_counterexample, "Exhaustive_Generators.put_counterexample")
- thy (SOME target) (fn proc => fn g =>
+ ctxt (SOME target) (fn proc => fn g =>
fn card => fn genuine_only => fn size => g card genuine_only size
|> (Option.map o apsnd o map) proc) t' []
in
@@ -497,12 +496,11 @@
fun compile_generator_exprs_raw ctxt ts =
let
- val thy = Proof_Context.theory_of ctxt
val ts' = map (fn t => mk_generator_expr ctxt (t, [])) ts;
val compiles = Code_Runtime.dynamic_value_strict
(Counterexample_Batch.get, put_counterexample_batch,
"Exhaustive_Generators.put_counterexample_batch")
- thy (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc))
+ ctxt (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc))
(HOLogic.mk_list @{typ "natural => term list option"} ts') []
in
map (fn compile => fn size => compile size
@@ -515,12 +513,11 @@
fun compile_validator_exprs_raw ctxt ts =
let
- val thy = Proof_Context.theory_of ctxt
val ts' = map (mk_validator_expr ctxt) ts
in
Code_Runtime.dynamic_value_strict
(Validator_Batch.get, put_validator_batch, "Exhaustive_Generators.put_validator_batch")
- thy (SOME target) (K I) (HOLogic.mk_list @{typ "natural => bool"} ts') []
+ ctxt (SOME target) (K I) (HOLogic.mk_list @{typ "natural => bool"} ts') []
end;
fun compile_validator_exprs ctxt ts =
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Feb 26 10:10:38 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Feb 26 11:57:52 2014 +0100
@@ -303,13 +303,12 @@
with_tmp_dir tmp_prefix run
end;
-fun dynamic_value_strict opts cookie thy postproc t =
+fun dynamic_value_strict opts cookie ctxt postproc t =
let
- val ctxt = Proof_Context.init_global thy
fun evaluator program ((_, vs_ty), t) deps =
Exn.interruptible_capture (value opts ctxt cookie)
- (Code_Target.evaluator thy target program deps true (vs_ty, t));
- in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
+ (Code_Target.evaluator ctxt target program deps true (vs_ty, t));
+ in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_result o postproc) evaluator t) end;
(** counterexample generator **)
@@ -462,7 +461,7 @@
val execute = dynamic_value_strict (true, opts)
((K true, fn _ => error ""), (Existential_Counterexample.get, Existential_Counterexample.put,
"Narrowing_Generators.put_existential_counterexample"))
- thy (apfst o Option.map o map_counterexample)
+ ctxt (apfst o Option.map o map_counterexample)
in
case act execute (mk_property qs prop_t) of
SOME (counterexample, result) => Quickcheck.Result
@@ -488,7 +487,7 @@
val execute = dynamic_value_strict (false, opts)
((is_genuine, counterexample_of),
(Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample"))
- thy (apfst o Option.map o apsnd o map)
+ ctxt (apfst o Option.map o apsnd o map)
in
case act execute (ensure_testable (finitize t')) of
SOME (counterexample, result) =>
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Wed Feb 26 10:10:38 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Wed Feb 26 11:57:52 2014 +0100
@@ -406,7 +406,6 @@
fun compile_generator_expr_raw ctxt ts =
let
- val thy = Proof_Context.theory_of ctxt
val iterations = Config.get ctxt Quickcheck.iterations
in
if Config.get ctxt Quickcheck.report then
@@ -414,7 +413,7 @@
val t' = mk_parametric_reporting_generator_expr ctxt ts;
val compile = Code_Runtime.dynamic_value_strict
(Counterexample_Report.get, put_counterexample_report, "Random_Generators.put_counterexample_report")
- thy (SOME target)
+ ctxt (SOME target)
(fn proc => fn g => fn c => fn b => fn s => g c b s
#>> (apfst o Option.map o apsnd o map) proc) t' [];
fun single_tester c b s = compile c b s |> Random_Engine.run
@@ -436,7 +435,7 @@
val t' = mk_parametric_generator_expr ctxt ts;
val compile = Code_Runtime.dynamic_value_strict
(Counterexample.get, put_counterexample, "Random_Generators.put_counterexample")
- thy (SOME target)
+ ctxt (SOME target)
(fn proc => fn g => fn c => fn b => fn s => g c b s
#>> (Option.map o apsnd o map) proc) t' [];
fun single_tester c b s = compile c b s |> Random_Engine.run
--- a/src/HOL/Tools/code_evaluation.ML Wed Feb 26 10:10:38 2014 +0100
+++ b/src/HOL/Tools/code_evaluation.ML Wed Feb 26 11:57:52 2014 +0100
@@ -6,14 +6,14 @@
signature CODE_EVALUATION =
sig
- val dynamic_value: theory -> term -> term option
- val dynamic_value_strict: theory -> term -> term
- val dynamic_value_exn: theory -> term -> term Exn.result
- val static_value: theory -> string list -> typ list -> term -> term option
- val static_value_strict: theory -> string list -> typ list -> term -> term
- val static_value_exn: theory -> string list -> typ list -> term -> term Exn.result
- val dynamic_conv: theory -> conv
- val static_conv: theory -> string list -> typ list -> conv
+ val dynamic_value: Proof.context -> term -> term option
+ val dynamic_value_strict: Proof.context -> term -> term
+ val dynamic_value_exn: Proof.context -> term -> term Exn.result
+ val static_value: Proof.context -> string list -> typ list -> Proof.context -> term -> term option
+ val static_value_strict: Proof.context -> string list -> typ list -> Proof.context -> term -> term
+ val static_value_exn: Proof.context -> string list -> typ list -> Proof.context -> term -> term Exn.result
+ val dynamic_conv: Proof.context -> conv
+ val static_conv: Proof.context -> string list -> typ list -> Proof.context -> conv
val put_term: (unit -> term) -> Proof.context -> Proof.context
val tracing: string -> 'a -> 'a
val setup: theory -> theory
@@ -171,44 +171,48 @@
fun term_of_const_for thy = Axclass.unoverload_const thy o dest_Const o HOLogic.term_of_const;
-fun gen_dynamic_value dynamic_value thy t =
- dynamic_value cookie thy NONE I (mk_term_of t) [];
+fun gen_dynamic_value dynamic_value ctxt t =
+ dynamic_value cookie ctxt NONE I (mk_term_of t) [];
val dynamic_value = gen_dynamic_value Code_Runtime.dynamic_value;
val dynamic_value_strict = gen_dynamic_value Code_Runtime.dynamic_value_strict;
val dynamic_value_exn = gen_dynamic_value Code_Runtime.dynamic_value_exn;
-fun gen_static_value static_value thy consts Ts =
- static_value cookie thy NONE I (union (op =) (map (term_of_const_for thy) Ts) consts)
- o mk_term_of;
+fun gen_static_value static_value ctxt consts Ts =
+ let
+ val static_value' = static_value cookie ctxt NONE I
+ (union (op =) (map (term_of_const_for (Proof_Context.theory_of ctxt)) Ts) consts)
+ in fn ctxt' => fn t => static_value' ctxt' (mk_term_of t) end;
val static_value = gen_static_value Code_Runtime.static_value;
val static_value_strict = gen_static_value Code_Runtime.static_value_strict;
val static_value_exn = gen_static_value Code_Runtime.static_value_exn;
-fun certify_eval thy value conv ct =
+fun certify_eval ctxt value conv ct =
let
+ val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
val t = Thm.term_of ct;
val T = fastype_of t;
- val mk_eq = Thm.mk_binop (Thm.cterm_of thy (Const ("==", T --> T --> propT)));
- in case value t
+ val mk_eq = Thm.mk_binop (cert (Const ("==", T --> T --> propT)));
+ in case value ctxt t
of NONE => Thm.reflexive ct
- | SOME t' => conv (mk_eq ct (Thm.cterm_of thy t')) RS @{thm eq_eq_TrueD}
+ | SOME t' => conv ctxt (mk_eq ct (cert t')) RS @{thm eq_eq_TrueD}
handle THM _ =>
- error ("Failed to certify evaluation result of " ^ Syntax.string_of_term_global thy t)
+ error ("Failed to certify evaluation result of " ^ Syntax.string_of_term ctxt t)
end;
-fun dynamic_conv thy = certify_eval thy (dynamic_value thy)
- (Code_Runtime.dynamic_holds_conv thy);
+fun dynamic_conv ctxt = certify_eval ctxt dynamic_value
+ Code_Runtime.dynamic_holds_conv;
-fun static_conv thy consts Ts =
+fun static_conv ctxt consts Ts =
let
val eqs = "==" :: @{const_name HOL.eq} ::
- map (fn T => Axclass.unoverload_const thy (@{const_name HOL.equal}, T)) Ts;
- (*assumes particular code equations for "==" etc.*)
+ map (fn T => Axclass.unoverload_const (Proof_Context.theory_of ctxt)
+ (@{const_name HOL.equal}, T)) Ts; (*assumes particular code equations for "==" etc.*)
+ val value = static_value ctxt consts Ts;
+ val holds = Code_Runtime.static_holds_conv ctxt (union (op =) eqs consts);
in
- certify_eval thy (static_value thy consts Ts)
- (Code_Runtime.static_holds_conv thy (union (op =) eqs consts))
+ fn ctxt' => certify_eval ctxt' value holds
end;
@@ -225,6 +229,6 @@
#> Code.datatype_interpretation ensure_term_of_code
#> Code.abstype_interpretation ensure_abs_term_of_code
#> Context.theory_map (Syntax_Phases.term_check 0 "termify" check_termify)
- #> Value.add_evaluator ("code", dynamic_value_strict o Proof_Context.theory_of);
+ #> Value.add_evaluator ("code", dynamic_value_strict);
end;
--- a/src/Tools/Code/code_preproc.ML Wed Feb 26 10:10:38 2014 +0100
+++ b/src/Tools/Code/code_preproc.ML Wed Feb 26 11:57:52 2014 +0100
@@ -10,27 +10,29 @@
val map_pre: (Proof.context -> Proof.context) -> theory -> theory
val map_post: (Proof.context -> Proof.context) -> theory -> theory
val add_unfold: thm -> theory -> theory
- val add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory
+ val add_functrans: string * (Proof.context -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory
val del_functrans: string -> theory -> theory
- val simple_functrans: (theory -> thm list -> thm list option)
- -> theory -> (thm * bool) list -> (thm * bool) list option
- val print_codeproc: theory -> unit
+ val simple_functrans: (Proof.context -> thm list -> thm list option)
+ -> Proof.context -> (thm * bool) list -> (thm * bool) list option
+ val print_codeproc: Proof.context -> unit
type code_algebra
type code_graph
val cert: code_graph -> string -> Code.cert
val sortargs: code_graph -> string -> sort list
val all: code_graph -> string list
- val pretty: theory -> code_graph -> Pretty.T
+ val pretty: Proof.context -> code_graph -> Pretty.T
val obtain: bool -> theory -> string list -> term list -> code_algebra * code_graph
- val dynamic_conv: theory
+ val dynamic_conv: Proof.context
-> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
- val dynamic_value: theory -> ((term -> term) -> 'a -> 'a)
+ val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'a)
-> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
- val static_conv: theory -> string list
- -> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
- val static_value: theory -> ((term -> term) -> 'a -> 'a) -> string list
- -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
+ val static_conv: Proof.context -> string list
+ -> (code_algebra -> code_graph -> Proof.context -> (string * sort) list -> term -> conv)
+ -> Proof.context -> conv
+ val static_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> string list
+ -> (code_algebra -> code_graph -> Proof.context -> (string * sort) list -> term -> 'a)
+ -> Proof.context -> term -> 'a
val setup: theory -> theory
end
@@ -45,7 +47,7 @@
datatype thmproc = Thmproc of {
pre: simpset,
post: simpset,
- functrans: (string * (serial * (theory -> (thm * bool) list -> (thm * bool) list option))) list
+ functrans: (string * (serial * (Proof.context -> (thm * bool) list -> (thm * bool) list option))) list
};
fun make_thmproc ((pre, post), functrans) =
@@ -110,9 +112,10 @@
(* post- and preprocessing *)
-fun no_variables_conv conv ct =
+fun no_variables_conv ctxt conv ct =
let
- val cert = Thm.cterm_of (Thm.theory_of_cterm ct);
+ val thy = Proof_Context.theory_of ctxt;
+ val cert = Thm.cterm_of thy;
val all_vars = fold_aterms (fn t as Free _ => insert (op aconvc) (cert t)
| t as Var _ => insert (op aconvc) (cert t)
| _ => I) (Thm.term_of ct) [];
@@ -128,48 +131,52 @@
fun trans_conv_rule conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
-fun term_of_conv thy conv =
- Thm.cterm_of thy
- #> conv
+fun term_of_conv ctxt conv =
+ Thm.cterm_of (Proof_Context.theory_of ctxt)
+ #> conv ctxt
#> Thm.prop_of
#> Logic.dest_equals
#> snd;
-fun term_of_conv_resubst thy conv t =
+fun term_of_conv_resubst ctxt conv t =
let
val all_vars = fold_aterms (fn t as Free _ => insert (op aconv) t
| t as Var _ => insert (op aconv) t
| _ => I) t [];
val resubst = curry (Term.betapplys o swap) all_vars;
- in (resubst, term_of_conv thy conv (fold_rev lambda all_vars t)) end;
-
-fun global_simpset_context thy ss =
- Proof_Context.init_global thy
- |> put_simpset ss;
+ in (resubst, term_of_conv ctxt conv (fold_rev lambda all_vars t)) end;
-fun preprocess_conv thy =
+fun preprocess_conv ctxt =
let
- val pre = global_simpset_context thy ((#pre o the_thmproc) thy);
- in
- Simplifier.rewrite pre
- #> trans_conv_rule (Axclass.unoverload_conv thy)
+ val thy = Proof_Context.theory_of ctxt;
+ val ss = (#pre o the_thmproc) thy;
+ in fn ctxt' =>
+ Simplifier.rewrite (put_simpset ss ctxt')
+ #> trans_conv_rule (Axclass.unoverload_conv (Proof_Context.theory_of ctxt'))
end;
-fun preprocess_term thy = term_of_conv_resubst thy (preprocess_conv thy);
-
-fun postprocess_conv thy =
+fun preprocess_term ctxt =
let
- val post = global_simpset_context thy ((#post o the_thmproc) thy);
- in
- Axclass.overload_conv thy
- #> trans_conv_rule (Simplifier.rewrite post)
+ val conv = preprocess_conv ctxt;
+ in fn ctxt' => term_of_conv_resubst ctxt' conv end;
+
+fun postprocess_conv ctxt =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val ss = (#post o the_thmproc) thy;
+ in fn ctxt' =>
+ Axclass.overload_conv (Proof_Context.theory_of ctxt')
+ #> trans_conv_rule (Simplifier.rewrite (put_simpset ss ctxt'))
end;
-fun postprocess_term thy = term_of_conv thy (postprocess_conv thy);
+fun postprocess_term ctxt =
+ let
+ val conv = postprocess_conv ctxt;
+ in fn ctxt' => term_of_conv ctxt' conv end;
-fun print_codeproc thy =
+fun print_codeproc ctxt =
let
- val ctxt = Proof_Context.init_global thy;
+ val thy = Proof_Context.theory_of ctxt;
val pre = (#pre o the_thmproc) thy;
val post = (#post o the_thmproc) thy;
val functrans = (map fst o #functrans o the_thmproc) thy;
@@ -193,7 +200,7 @@
]
end;
-fun simple_functrans f thy eqns = case f thy (map fst eqns)
+fun simple_functrans f ctxt eqns = case f ctxt (map fst eqns)
of SOME thms' => SOME (map (rpair (forall snd eqns)) thms')
| NONE => NONE;
@@ -210,12 +217,16 @@
fun sortargs eqngr = map snd o fst o get_node eqngr;
fun all eqngr = Graph.keys eqngr;
-fun pretty thy eqngr =
- AList.make (snd o Graph.get_node eqngr) (Graph.keys eqngr)
- |> (map o apfst) (Code.string_of_const thy)
- |> sort (string_ord o pairself fst)
- |> map (fn (s, cert) => (Pretty.block o Pretty.fbreaks) (Pretty.str s :: Code.pretty_cert thy cert))
- |> Pretty.chunks;
+fun pretty ctxt eqngr =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ in
+ AList.make (snd o Graph.get_node eqngr) (Graph.keys eqngr)
+ |> (map o apfst) (Code.string_of_const thy)
+ |> sort (string_ord o pairself fst)
+ |> map (fn (s, cert) => (Pretty.block o Pretty.fbreaks) (Pretty.str s :: Code.pretty_cert thy cert))
+ |> Pretty.chunks
+ end;
(** the Waisenhaus algorithm **)
@@ -269,17 +280,18 @@
of SOME (lhs, cert) => ((lhs, []), cert)
| NONE => let
val thy = Proof_Context.theory_of ctxt;
- val functrans = (map (fn (_, (_, f)) => f thy)
+ val functrans = (map (fn (_, (_, f)) => f ctxt)
o #functrans o the_thmproc) thy;
val cert = Code.get_cert thy { functrans = functrans, ss = simpset_of ctxt } c; (*FIXME*)
val (lhs, rhss) =
Code.typargs_deps_of_cert thy cert;
in ((lhs, rhss), cert) end;
-fun obtain_instance thy arities (inst as (class, tyco)) =
+fun obtain_instance ctxt arities (inst as (class, tyco)) =
case AList.lookup (op =) arities inst
of SOME classess => (classess, ([], []))
| NONE => let
+ val thy = Proof_Context.theory_of ctxt;
val all_classes = complete_proper_sort thy [class];
val super_classes = remove (op =) class all_classes;
val classess = map (complete_proper_sort thy)
@@ -331,7 +343,7 @@
if member (op =) insts inst then vardeps_data
else let
val (classess, (super_classes, inst_params)) =
- obtain_instance (Proof_Context.theory_of ctxt) arities inst;
+ obtain_instance ctxt arities inst;
in
vardeps_data
|> (apsnd o apsnd) (insert (op =) inst)
@@ -381,8 +393,9 @@
(* applying instantiations *)
-fun dicts_of thy (proj_sort, algebra) (T, sort) =
+fun dicts_of ctxt (proj_sort, algebra) (T, sort) =
let
+ val thy = Proof_Context.theory_of ctxt;
fun class_relation (x, _) _ = x;
fun type_constructor (tyco, _) xs class =
inst_params thy tyco (Sorts.complete_sort algebra [class])
@@ -395,14 +408,15 @@
handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
end;
-fun add_arity thy vardeps (class, tyco) =
+fun add_arity ctxt vardeps (class, tyco) =
AList.default (op =) ((class, tyco),
map_range (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k))
- (Sign.arity_number thy tyco));
+ (Sign.arity_number (Proof_Context.theory_of ctxt) tyco));
-fun add_cert thy vardeps (c, (proto_lhs, proto_cert)) (rhss, eqngr) =
+fun add_cert ctxt vardeps (c, (proto_lhs, proto_cert)) (rhss, eqngr) =
if can (Graph.get_node eqngr) c then (rhss, eqngr)
else let
+ val thy = Proof_Context.theory_of ctxt;
val lhs = map_index (fn (k, (v, _)) =>
(v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs;
val cert = proto_cert
@@ -412,20 +426,21 @@
val eqngr' = Graph.new_node (c, (vs, cert)) eqngr;
in (map (pair c) rhss' @ rhss, eqngr') end;
-fun extend_arities_eqngr thy cs ts (arities, (eqngr : code_graph)) =
+fun extend_arities_eqngr raw_ctxt cs ts (arities, (eqngr : code_graph)) =
let
+ val thy = Proof_Context.theory_of raw_ctxt;
val {pre, ...} = the_thmproc thy;
- val ctxt = thy |> Proof_Context.init_global |> put_simpset pre;
+ val ctxt = put_simpset pre raw_ctxt;
val cs_rhss = (fold o fold_aterms) (fn Const (c_ty as (c, _)) =>
insert (op =) (c, (map (styp_of NONE) o Sign.const_typargs thy) c_ty) | _ => I) ts [];
val (vardeps, (eqntab, insts)) = empty_vardeps_data
|> fold (ensure_fun ctxt arities eqngr) cs
|> fold (ensure_rhs ctxt arities eqngr) cs_rhss;
- val arities' = fold (add_arity thy vardeps) insts arities;
+ val arities' = fold (add_arity ctxt vardeps) insts arities;
val algebra = Sorts.subalgebra (Context.pretty_global thy) (is_proper_class thy)
(AList.lookup (op =) arities') (Sign.classes_of thy);
- val (rhss, eqngr') = Symtab.fold (add_cert thy vardeps) eqntab ([], eqngr);
- fun deps_of (c, rhs) = c :: maps (dicts_of thy algebra)
+ val (rhss, eqngr') = Symtab.fold (add_cert ctxt vardeps) eqntab ([], eqngr);
+ fun deps_of (c, rhs) = c :: maps (dicts_of ctxt algebra)
(rhs ~~ sortargs eqngr' c);
val eqngr'' = fold (fn (c, rhs) => fold
(curry Graph.add_edge c) (deps_of rhs)) rhss eqngr';
@@ -444,59 +459,62 @@
(** retrieval and evaluation interfaces **)
fun obtain ignore_cache thy consts ts = apsnd snd
- (Wellsorted.change_yield (if ignore_cache then NONE else SOME thy) (extend_arities_eqngr thy consts ts));
+ (Wellsorted.change_yield (if ignore_cache then NONE else SOME thy)
+ (extend_arities_eqngr (Proof_Context.init_global thy) consts ts));
fun dest_cterm ct = let val t = Thm.term_of ct in (Term.add_tfrees t [], t) end;
-fun dynamic_conv thy conv = no_variables_conv (fn ct =>
+fun dynamic_conv ctxt conv = no_variables_conv ctxt (fn ct =>
let
- val thm1 = preprocess_conv thy ct;
+ val thm1 = preprocess_conv ctxt ctxt ct;
val ct' = Thm.rhs_of thm1;
val (vs', t') = dest_cterm ct';
val consts = fold_aterms
(fn Const (c, _) => insert (op =) c | _ => I) t' [];
- val (algebra', eqngr') = obtain false thy consts [t'];
+ val (algebra', eqngr') = obtain false (Proof_Context.theory_of ctxt) consts [t'];
val thm2 = conv algebra' eqngr' vs' t' ct';
- val thm3 = postprocess_conv thy (Thm.rhs_of thm2);
+ val thm3 = postprocess_conv ctxt ctxt (Thm.rhs_of thm2);
in
Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
error ("could not construct evaluation proof:\n"
- ^ (cat_lines o map (Display.string_of_thm_global thy)) [thm1, thm2, thm3])
+ ^ (cat_lines o map (Display.string_of_thm ctxt)) [thm1, thm2, thm3])
end);
-fun dynamic_value thy postproc evaluator t =
+fun dynamic_value ctxt postproc evaluator t =
let
- val (resubst, t') = preprocess_term thy t;
+ val (resubst, t') = preprocess_term ctxt ctxt t;
val vs' = Term.add_tfrees t' [];
val consts = fold_aterms
(fn Const (c, _) => insert (op =) c | _ => I) t' [];
- val (algebra', eqngr') = obtain false thy consts [t'];
+ val (algebra', eqngr') = obtain false (Proof_Context.theory_of ctxt) consts [t'];
in
t'
|> evaluator algebra' eqngr' vs'
- |> postproc (postprocess_term thy o resubst)
+ |> postproc (postprocess_term ctxt ctxt o resubst)
end;
-fun static_conv thy consts conv =
+fun static_conv ctxt consts conv =
let
- val (algebra, eqngr) = obtain true thy consts [];
+ val (algebra, eqngr) = obtain true (Proof_Context.theory_of ctxt) consts [];
+ val pre_conv = preprocess_conv ctxt;
val conv' = conv algebra eqngr;
- in
- no_variables_conv ((preprocess_conv thy)
- then_conv (fn ct => uncurry conv' (dest_cterm ct) ct)
- then_conv (postprocess_conv thy))
+ val post_conv = postprocess_conv ctxt;
+ in fn ctxt' => no_variables_conv ctxt' ((pre_conv ctxt')
+ then_conv (fn ct => uncurry (conv' ctxt') (dest_cterm ct) ct)
+ then_conv (post_conv ctxt'))
end;
-fun static_value thy postproc consts evaluator =
+fun static_value ctxt postproc consts evaluator =
let
- val (algebra, eqngr) = obtain true thy consts [];
+ val (algebra, eqngr) = obtain true (Proof_Context.theory_of ctxt) consts [];
+ val preproc = preprocess_term ctxt;
val evaluator' = evaluator algebra eqngr;
- val postproc' = postprocess_term thy;
- in
- preprocess_term thy
+ val postproc' = postprocess_term ctxt;
+ in fn ctxt' =>
+ preproc ctxt'
#-> (fn resubst => fn t => t
- |> evaluator' (Term.add_tfrees t [])
- |> postproc (postproc' o resubst))
+ |> evaluator' ctxt' (Term.add_tfrees t [])
+ |> postproc (postproc' ctxt' o resubst))
end;
@@ -518,7 +536,6 @@
val _ =
Outer_Syntax.improper_command @{command_spec "print_codeproc"} "print code preprocessor setup"
- (Scan.succeed (Toplevel.unknown_theory o
- Toplevel.keep (print_codeproc o Toplevel.theory_of)));
+ (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_codeproc o Toplevel.context_of)));
end; (*struct*)
--- a/src/Tools/Code/code_runtime.ML Wed Feb 26 10:10:38 2014 +0100
+++ b/src/Tools/Code/code_runtime.ML Wed Feb 26 11:57:52 2014 +0100
@@ -11,20 +11,20 @@
(Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string ->
string * string -> 'a
type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string
- val dynamic_value: 'a cookie -> theory -> string option
+ val dynamic_value: 'a cookie -> Proof.context -> string option
-> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a option
- val dynamic_value_strict: 'a cookie -> theory -> string option
+ val dynamic_value_strict: 'a cookie -> Proof.context -> string option
-> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a
- val dynamic_value_exn: 'a cookie -> theory -> string option
+ val dynamic_value_exn: 'a cookie -> Proof.context -> string option
-> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a Exn.result
- val static_value: 'a cookie -> theory -> string option
- -> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a option
- val static_value_strict: 'a cookie -> theory -> string option
- -> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a
- val static_value_exn: 'a cookie -> theory -> string option
- -> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a Exn.result
- val dynamic_holds_conv: theory -> conv
- val static_holds_conv: theory -> string list -> conv
+ val static_value: 'a cookie -> Proof.context -> string option
+ -> ((term -> term) -> 'a -> 'a) -> string list -> Proof.context -> term -> 'a option
+ val static_value_strict: 'a cookie -> Proof.context -> string option
+ -> ((term -> term) -> 'a -> 'a) -> string list -> Proof.context -> term -> 'a
+ val static_value_exn: 'a cookie -> Proof.context -> string option
+ -> ((term -> term) -> 'a -> 'a) -> string list -> Proof.context -> term -> 'a Exn.result
+ val dynamic_holds_conv: Proof.context -> conv
+ val static_holds_conv: Proof.context -> string list -> Proof.context -> conv
val code_reflect: (string * string list option) list -> string list -> string
-> string option -> theory -> theory
datatype truth = Holds
@@ -83,21 +83,19 @@
type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string;
-fun reject_vars thy t =
- let
- val ctxt = Proof_Context.init_global thy;
- in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end;
+fun reject_vars ctxt t =
+ ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t);
-fun obtain_evaluator thy some_target program consts expr =
- Code_Target.evaluator thy (the_default target some_target) program consts false expr
- |> apfst (fn ml_modules => space_implode "\n\n" (map snd ml_modules));
+fun obtain_evaluator ctxt some_target program consts =
+ let
+ val evaluator' = Code_Target.evaluator ctxt (the_default target some_target) program consts false;
+ in
+ evaluator'
+ #> apfst (fn ml_modules => space_implode "\n\n" (map snd ml_modules))
+ end;
-fun obtain_evaluator' thy some_target program =
- obtain_evaluator thy some_target program o map Constant;
-
-fun evaluation cookie thy evaluator vs_t args =
+fun evaluation cookie ctxt evaluator vs_t args =
let
- val ctxt = Proof_Context.init_global thy;
val (program_code, value_name) = evaluator vs_t;
val value_code = space_implode " "
(value_name :: "()" :: map (enclose "(" ")") args);
@@ -108,36 +106,39 @@
| General.Bind => NONE
| General.Fail _ => NONE;
-fun dynamic_value_exn cookie thy some_target postproc t args =
+fun dynamic_value_exn cookie ctxt some_target postproc t args =
let
- val _ = reject_vars thy t;
+ val _ = reject_vars ctxt t;
val _ = if ! trace
- then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term_global thy t))
+ then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term ctxt t))
else ()
fun evaluator program ((_, vs_ty), t) deps =
- evaluation cookie thy (obtain_evaluator thy some_target program deps) (vs_ty, t) args;
- in Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t end;
+ evaluation cookie ctxt (obtain_evaluator ctxt some_target program deps) (vs_ty, t) args;
+ in Code_Thingol.dynamic_value ctxt (Exn.map_result o postproc) evaluator t end;
-fun dynamic_value_strict cookie thy some_target postproc t args =
- Exn.release (dynamic_value_exn cookie thy some_target postproc t args);
+fun dynamic_value_strict cookie ctxt some_target postproc t args =
+ Exn.release (dynamic_value_exn cookie ctxt some_target postproc t args);
-fun dynamic_value cookie thy some_target postproc t args =
- partiality_as_none (dynamic_value_exn cookie thy some_target postproc t args);
+fun dynamic_value cookie ctxt some_target postproc t args =
+ partiality_as_none (dynamic_value_exn cookie ctxt some_target postproc t args);
-fun static_evaluator cookie thy some_target program consts' =
+fun static_evaluator cookie ctxt some_target program consts' =
let
- val evaluator = obtain_evaluator' thy some_target program consts'
- in fn ((_, vs_ty), t) => fn _ => evaluation cookie thy evaluator (vs_ty, t) [] end;
+ val evaluator = obtain_evaluator ctxt some_target program (map Constant consts');
+ val evaluation' = evaluation cookie ctxt evaluator;
+ in fn _ => fn ((_, vs_ty), t) => fn _ => evaluation' (vs_ty, t) [] end;
-fun static_value_exn cookie thy some_target postproc consts =
- Code_Thingol.static_value thy (Exn.map_result o postproc) consts
- (static_evaluator cookie thy some_target) o reject_vars thy;
+fun static_value_exn cookie ctxt some_target postproc consts =
+ let
+ val evaluator = Code_Thingol.static_value ctxt (Exn.map_result o postproc) consts
+ (static_evaluator cookie ctxt some_target);
+ in fn ctxt' => evaluator ctxt' o reject_vars ctxt' end;
-fun static_value_strict cookie thy some_target postproc consts =
- Exn.release o static_value_exn cookie thy some_target postproc consts;
+fun static_value_strict cookie ctxt some_target postproc consts =
+ Exn.release oo static_value_exn cookie ctxt some_target postproc consts;
fun static_value cookie thy some_target postproc consts =
- partiality_as_none o static_value_exn cookie thy some_target postproc consts;
+ partiality_as_none oo static_value_exn cookie thy some_target postproc consts;
(* evaluation for truth or nothing *)
@@ -151,18 +152,19 @@
val put_truth = Truth_Result.put;
val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append this "put_truth");
-val reject_vars = fn thy => tap (reject_vars thy o Thm.term_of);
+val reject_vars = fn ctxt => tap (reject_vars ctxt o Thm.term_of);
local
-fun check_holds thy evaluator vs_t ct =
+fun check_holds ctxt evaluator vs_t ct =
let
+ val thy = Proof_Context.theory_of ctxt;
val t = Thm.term_of ct;
val _ = if fastype_of t <> propT
then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t)
else ();
val iff = Thm.cterm_of thy (Term.Const ("==", propT --> propT --> propT));
- val result = case partiality_as_none (evaluation truth_cookie thy evaluator vs_t [])
+ val result = case partiality_as_none (evaluation truth_cookie ctxt evaluator vs_t [])
of SOME Holds => true
| _ => false;
in
@@ -171,34 +173,39 @@
val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result
(Thm.add_oracle (@{binding holds_by_evaluation},
- fn (thy, evaluator, vs_t, ct) => check_holds thy evaluator vs_t ct)));
+ fn (ctxt, evaluator, vs_t, ct) => check_holds ctxt evaluator vs_t ct)));
-fun check_holds_oracle thy evaluator ((_, vs_ty), t) deps ct =
- raw_check_holds_oracle (thy, evaluator, (vs_ty, t), ct);
+fun check_holds_oracle ctxt evaluator ((_, vs_ty), t) deps ct =
+ raw_check_holds_oracle (ctxt, evaluator, (vs_ty, t), ct);
in
-fun dynamic_holds_conv thy = Code_Thingol.dynamic_conv thy
+fun dynamic_holds_conv ctxt = Code_Thingol.dynamic_conv ctxt
(fn program => fn vs_t => fn deps =>
- check_holds_oracle thy (obtain_evaluator thy NONE program deps) vs_t deps)
- o reject_vars thy;
+ check_holds_oracle ctxt (obtain_evaluator ctxt NONE program deps) vs_t deps)
+ o reject_vars ctxt;
-fun static_holds_conv thy consts = Code_Thingol.static_conv thy consts
- (fn program => fn consts' =>
- check_holds_oracle thy (obtain_evaluator' thy NONE program consts'))
- o reject_vars thy;
+fun static_holds_conv ctxt consts =
+ Code_Thingol.static_conv ctxt consts (fn program => fn consts' =>
+ let
+ val evaluator' = obtain_evaluator ctxt NONE program (map Constant consts')
+ in
+ fn ctxt' => fn vs_t => fn deps => check_holds_oracle ctxt' evaluator' vs_t deps o reject_vars ctxt'
+ end);
+
+(* o reject_vars ctxt'*)
end; (*local*)
(** instrumentalization **)
-fun evaluation_code thy module_name tycos consts =
+fun evaluation_code ctxt module_name tycos consts =
let
- val ctxt = Proof_Context.init_global thy;
+ val thy = Proof_Context.theory_of ctxt;
val program = Code_Thingol.consts_program thy consts;
val (ml_modules, target_names) =
- Code_Target.produce_code_for thy
+ Code_Target.produce_code_for ctxt
target NONE module_name [] program false (map Constant consts @ map Type_Constructor tycos);
val ml_code = space_implode "\n\n" (map snd ml_modules);
val (consts', tycos') = chop (length consts) target_names;
@@ -234,7 +241,7 @@
val tycos' = fold (insert (op =)) new_tycos tycos;
val consts' = fold (insert (op =)) new_consts consts;
val acc_code = Lazy.lazy (fn () =>
- evaluation_code (Proof_Context.theory_of ctxt) structure_generated tycos' consts'
+ evaluation_code ctxt structure_generated tycos' consts'
|> apsnd snd);
in Code_Antiq_Data.put ((tycos', consts'), (false, acc_code)) ctxt end;
@@ -330,12 +337,13 @@
fun gen_code_reflect prep_type prep_const raw_datatypes raw_functions module_name some_file thy =
let
+ val ctxt = Proof_Context.init_global thy;
val datatypes = map (fn (raw_tyco, raw_cos) =>
- (prep_type thy raw_tyco, (Option.map o map) (prep_const thy) raw_cos)) raw_datatypes;
+ (prep_type ctxt raw_tyco, (Option.map o map) (prep_const thy) raw_cos)) raw_datatypes;
val (tycos, constrs) = map_split (uncurry (check_datatype thy)) datatypes
|> apsnd flat;
val functions = map (prep_const thy) raw_functions;
- val result = evaluation_code thy module_name tycos (constrs @ functions)
+ val result = evaluation_code ctxt module_name tycos (constrs @ functions)
|> (apsnd o apsnd) (chop (length constrs));
in
thy
@@ -440,7 +448,7 @@
|-> (fn ([Const (const, _)], _) =>
Code_Target.set_printings (Constant (const,
[(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))]))
- #> tap (fn thy => Code_Target.produce_code thy false [const] target NONE structure_generated []));
+ #> tap (fn thy => Code_Target.produce_code (Proof_Context.init_global thy) false [const] target NONE structure_generated []));
fun process_file filepath (definienda, thy) =
let
--- a/src/Tools/Code/code_simp.ML Wed Feb 26 10:10:38 2014 +0100
+++ b/src/Tools/Code/code_simp.ML Wed Feb 26 11:57:52 2014 +0100
@@ -7,11 +7,11 @@
signature CODE_SIMP =
sig
val map_ss: (Proof.context -> Proof.context) -> theory -> theory
- val dynamic_conv: theory -> conv
- val dynamic_tac: theory -> int -> tactic
- val dynamic_value: theory -> term -> term
- val static_conv: theory -> simpset option -> string list -> conv
- val static_tac: theory -> simpset option -> string list -> Proof.context -> int -> tactic
+ val dynamic_conv: Proof.context -> conv
+ val dynamic_tac: Proof.context -> int -> tactic
+ val dynamic_value: Proof.context -> term -> term
+ val static_conv: Proof.context -> simpset option -> string list -> Proof.context -> conv
+ val static_tac: Proof.context -> simpset option -> string list -> Proof.context -> int -> tactic
val setup: theory -> theory
val trace: bool Config.T
end;
@@ -31,11 +31,11 @@
fun map_ss f thy = Simpset.map (simpset_map (Proof_Context.init_global thy) f) thy;
-fun simpset_default thy some_ss = the_default (Simpset.get thy) some_ss;
+fun simpset_default ctxt some_ss = the_default (Simpset.get (Proof_Context.theory_of ctxt)) some_ss;
-fun simp_ctxt_default thy some_ss =
- Proof_Context.init_global thy
- |> put_simpset (simpset_default thy some_ss);
+(*fun simp_ctxt_default ctxt some_ss =
+ Proof_Context.init_global ctxt
+ |> put_simpset (simpset_default ctxt some_ss);*)
(* diagnostic *)
@@ -50,7 +50,7 @@
end;
-(* build simpset and conversion from program *)
+(* build simpset context and conversion from program *)
fun add_stmt (Code_Thingol.Fun ((_, eqs), some_cong)) ss =
ss
@@ -63,43 +63,49 @@
val add_program = Code_Symbol.Graph.fold (add_stmt o fst o snd);
-fun simp_ctxt_program thy some_ss program =
- simp_ctxt_default thy some_ss
- |> add_program program;
+fun simpset_program ctxt some_ss program =
+ simpset_map ctxt (add_program program) (simpset_default ctxt some_ss);
-fun rewrite_modulo thy some_ss program =
- Simplifier.full_rewrite (simp_ctxt_program thy some_ss program |> set_trace);
+fun rewrite_modulo ctxt some_ss program =
+ let
+ val ss = simpset_program ctxt some_ss program;
+ in fn ctxt => Simplifier.full_rewrite (ctxt |> put_simpset ss |> set_trace) end;
-fun conclude_tac thy some_ss =
- Simplifier.full_simp_tac o Simplifier.put_simpset (simpset_default thy some_ss);
+fun conclude_tac ctxt some_ss =
+ let
+ val ss = simpset_default ctxt some_ss
+ in fn ctxt => Simplifier.full_simp_tac (ctxt |> put_simpset ss) end;
(* evaluation with dynamic code context *)
-fun dynamic_conv thy = Code_Thingol.dynamic_conv thy
- (fn program => fn _ => fn _ => rewrite_modulo thy NONE program);
+fun dynamic_conv ctxt = Code_Thingol.dynamic_conv ctxt
+ (fn program => fn _ => fn _ => rewrite_modulo ctxt NONE program ctxt);
-fun dynamic_tac thy = CONVERSION (dynamic_conv thy) THEN' conclude_tac thy NONE (Proof_Context.init_global thy);
+fun dynamic_tac ctxt = CONVERSION (dynamic_conv ctxt)
+ THEN' conclude_tac ctxt NONE ctxt;
-fun dynamic_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_conv thy o Thm.cterm_of thy;
+fun dynamic_value ctxt =
+ snd o Logic.dest_equals o Thm.prop_of o dynamic_conv ctxt o Thm.cterm_of (Proof_Context.theory_of ctxt);
val setup =
Method.setup @{binding code_simp}
- (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac o Proof_Context.theory_of)))
+ (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac)))
"simplification with code equations"
- #> Value.add_evaluator ("simp", dynamic_value o Proof_Context.theory_of);
+ #> Value.add_evaluator ("simp", dynamic_value);
(* evaluation with static code context *)
-fun static_conv thy some_ss consts =
- Code_Thingol.static_conv_simple thy consts
- (fn program => fn _ => fn _ => rewrite_modulo thy some_ss program);
+fun static_conv ctxt some_ss consts =
+ Code_Thingol.static_conv_simple ctxt consts
+ (fn program => let val conv' = rewrite_modulo ctxt some_ss program
+ in fn ctxt' => fn _ => fn _ => conv' ctxt' end);
-fun static_tac thy some_ss consts =
+fun static_tac ctxt some_ss consts =
let
- val conv = static_conv thy some_ss consts;
- val tac = conclude_tac thy some_ss;
- in fn ctxt => CONVERSION conv THEN' tac ctxt end;
+ val conv = static_conv ctxt some_ss consts;
+ val tac = conclude_tac ctxt some_ss;
+ in fn ctxt' => CONVERSION (conv ctxt') THEN' (tac ctxt') end;
end;
--- a/src/Tools/Code/code_target.ML Wed Feb 26 10:10:38 2014 +0100
+++ b/src/Tools/Code/code_target.ML Wed Feb 26 11:57:52 2014 +0100
@@ -6,29 +6,29 @@
signature CODE_TARGET =
sig
- val cert_tyco: theory -> string -> string
- val read_tyco: theory -> string -> string
+ val cert_tyco: Proof.context -> string -> string
+ val read_tyco: Proof.context -> string -> string
- val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list
+ val export_code_for: Proof.context -> Path.T option -> string -> int option -> string -> Token.T list
-> Code_Thingol.program -> bool -> Code_Symbol.T list -> unit
- val produce_code_for: theory -> string -> int option -> string -> Token.T list
+ val produce_code_for: Proof.context -> string -> int option -> string -> Token.T list
-> Code_Thingol.program -> bool -> Code_Symbol.T list -> (string * string) list * string option list
- val present_code_for: theory -> string -> int option -> string -> Token.T list
+ val present_code_for: Proof.context -> string -> int option -> string -> Token.T list
-> Code_Thingol.program -> Code_Symbol.T list * Code_Symbol.T list -> string
- val check_code_for: theory -> string -> bool -> Token.T list
+ val check_code_for: Proof.context -> string -> bool -> Token.T list
-> Code_Thingol.program -> bool -> Code_Symbol.T list -> unit
- val export_code: theory -> bool -> string list
+ val export_code: Proof.context -> bool -> string list
-> (((string * string) * Path.T option) * Token.T list) list -> unit
- val produce_code: theory -> bool -> string list
+ val produce_code: Proof.context -> bool -> string list
-> string -> int option -> string -> Token.T list -> (string * string) list * string option list
- val present_code: theory -> string list -> Code_Symbol.T list
+ val present_code: Proof.context -> string list -> Code_Symbol.T list
-> string -> int option -> string -> Token.T list -> string
- val check_code: theory -> bool -> string list
+ val check_code: Proof.context -> bool -> string list
-> ((string * bool) * Token.T list) list -> unit
val generatedN: string
- val evaluator: theory -> string -> Code_Thingol.program
+ val evaluator: Proof.context -> string -> Code_Thingol.program
-> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
-> (string * string) list * string
@@ -40,8 +40,8 @@
val extend_target: string *
(string * (Code_Thingol.program -> Code_Thingol.program))
-> theory -> theory
- val assert_target: theory -> string -> string
- val the_literals: theory -> string -> literals
+ val assert_target: Proof.context -> string -> string
+ val the_literals: Proof.context -> string -> literals
type serialization
val parse_args: 'a parser -> Token.T list -> 'a
val serialization: (int -> Path.T option -> 'a -> unit)
@@ -83,45 +83,45 @@
(** checking and parsing of symbols **)
-fun cert_const thy const =
+fun cert_const ctxt const =
let
- val _ = if Sign.declared_const thy const then ()
+ val _ = if Sign.declared_const (Proof_Context.theory_of ctxt) const then ()
else error ("No such constant: " ^ quote const);
in const end;
-fun cert_tyco thy tyco =
+fun read_const ctxt = Code.read_const (Proof_Context.theory_of ctxt);
+
+fun cert_tyco ctxt tyco =
let
- val _ = if Sign.declared_tyname thy tyco then ()
+ val _ = if Sign.declared_tyname (Proof_Context.theory_of ctxt) tyco then ()
else error ("No such type constructor: " ^ quote tyco);
in tyco end;
-fun read_tyco thy = #1 o dest_Type
- o Proof_Context.read_type_name_proper (Proof_Context.init_global thy) true;
+fun read_tyco ctxt = #1 o dest_Type
+ o Proof_Context.read_type_name_proper ctxt true;
-fun cert_class thy class =
+fun cert_class ctxt class =
let
- val _ = Axclass.get_info thy class;
+ val _ = Axclass.get_info (Proof_Context.theory_of ctxt) class;
in class end;
-fun read_class thy = Proof_Context.read_class (Proof_Context.init_global thy);
-
val parse_classrel_ident = Parse.class --| @{keyword "<"} -- Parse.class;
-fun cert_inst thy (class, tyco) =
- (cert_class thy class, cert_tyco thy tyco);
+fun cert_inst ctxt (class, tyco) =
+ (cert_class ctxt class, cert_tyco ctxt tyco);
-fun read_inst thy (raw_tyco, raw_class) =
- (read_tyco thy raw_tyco, read_class thy raw_class);
+fun read_inst ctxt (raw_tyco, raw_class) =
+ (read_tyco ctxt raw_tyco, Proof_Context.read_class ctxt raw_class);
val parse_inst_ident = Parse.xname --| @{keyword "::"} -- Parse.class;
-fun cert_syms thy =
- Code_Symbol.map_attr (apfst (cert_const thy)) (apfst (cert_tyco thy))
- (apfst (cert_class thy)) ((apfst o pairself) (cert_class thy)) (apfst (cert_inst thy)) I;
+fun cert_syms ctxt =
+ Code_Symbol.map_attr (apfst (cert_const ctxt)) (apfst (cert_tyco ctxt))
+ (apfst (cert_class ctxt)) ((apfst o pairself) (cert_class ctxt)) (apfst (cert_inst ctxt)) I;
-fun read_syms thy =
- Code_Symbol.map_attr (apfst (Code.read_const thy)) (apfst (read_tyco thy))
- (apfst (read_class thy)) ((apfst o pairself) (read_class thy)) (apfst (read_inst thy)) I;
+fun read_syms ctxt =
+ Code_Symbol.map_attr (apfst (read_const ctxt)) (apfst (read_tyco ctxt))
+ (apfst (Proof_Context.read_class ctxt)) ((apfst o pairself) (Proof_Context.read_class ctxt)) (apfst (read_inst ctxt)) I;
fun check_name is_module s =
let
@@ -231,7 +231,8 @@
(Symtab.join (merge_target true) (target1, target2), Int.max (width1, width2));
);
-fun assert_target thy target = if Symtab.defined (fst (Targets.get thy)) target
+fun assert_target ctxt target =
+ if Symtab.defined (fst (Targets.get (Proof_Context.theory_of ctxt))) target
then target
else error ("Unknown code target language: " ^ quote target);
@@ -264,7 +265,7 @@
fun map_target_data target f thy =
let
- val _ = assert_target thy target;
+ val _ = assert_target (Proof_Context.init_global thy) target;
in
thy
|> (Targets.map o apfst o Symtab.map_entry target o map_target o apsnd) f
@@ -284,9 +285,9 @@
(* montage *)
-fun the_fundamental thy =
+fun the_fundamental ctxt =
let
- val (targets, _) = Targets.get thy;
+ val (targets, _) = Targets.get (Proof_Context.theory_of ctxt);
fun fundamental target = case Symtab.lookup targets target
of SOME data => (case the_description data
of Fundamental data => data
@@ -294,11 +295,11 @@
| NONE => error ("Unknown code target language: " ^ quote target);
in fundamental end;
-fun the_literals thy = #literals o the_fundamental thy;
+fun the_literals ctxt = #literals o the_fundamental ctxt;
-fun collapse_hierarchy thy =
+fun collapse_hierarchy ctxt =
let
- val (targets, _) = Targets.get thy;
+ val (targets, _) = Targets.get (Proof_Context.theory_of ctxt);
fun collapse target =
let
val data = case Symtab.lookup targets target
@@ -314,15 +315,15 @@
local
-fun activate_target thy target =
+fun activate_target ctxt target =
let
+ val thy = Proof_Context.theory_of ctxt;
val (_, default_width) = Targets.get thy;
- val (modify, data) = collapse_hierarchy thy target;
+ val (modify, data) = collapse_hierarchy ctxt target;
in (default_width, data, modify) end;
-fun project_program thy syms_hidden syms1 program2 =
+fun project_program ctxt syms_hidden syms1 program2 =
let
- val ctxt = Proof_Context.init_global thy;
val syms2 = subtract (op =) syms_hidden syms1;
val program3 = Code_Symbol.Graph.restrict (not o member (op =) syms_hidden) program2;
val syms4 = Code_Symbol.Graph.all_succs program3 syms2;
@@ -334,17 +335,17 @@
val program4 = Code_Symbol.Graph.restrict (member (op =) syms4) program3;
in (syms4, program4) end;
-fun prepare_serializer thy (serializer : serializer) reserved identifiers
+fun prepare_serializer ctxt (serializer : serializer) reserved identifiers
printings module_name args proto_program syms =
let
val syms_hidden = Code_Symbol.symbols_of printings;
- val (syms_all, program) = project_program thy syms_hidden syms proto_program;
+ val (syms_all, program) = project_program ctxt syms_hidden syms proto_program;
fun select_include (name, (content, cs)) =
if null cs orelse exists (fn c => member (op =) syms_all (Constant c)) cs
then SOME (name, content) else NONE;
val includes = map_filter select_include (Code_Symbol.dest_module_data printings);
in
- (serializer args (Proof_Context.init_global thy) {
+ (serializer args ctxt {
module_name = module_name,
reserved_syms = reserved,
identifiers = identifiers,
@@ -355,62 +356,62 @@
(syms_all, program))
end;
-fun mount_serializer thy target some_width module_name args program syms =
+fun mount_serializer ctxt target some_width module_name args program syms =
let
- val (default_width, data, modify) = activate_target thy target;
+ val (default_width, data, modify) = activate_target ctxt target;
val serializer = case the_description data
of Fundamental seri => #serializer seri;
val (prepared_serializer, (prepared_syms, prepared_program)) =
- prepare_serializer thy serializer
+ prepare_serializer ctxt serializer
(the_reserved data) (the_identifiers data) (the_printings data)
module_name args (modify program) syms
val width = the_default default_width some_width;
in (fn program => fn syms => prepared_serializer syms program width, (prepared_syms, prepared_program)) end;
-fun invoke_serializer thy target some_width raw_module_name args program all_public syms =
+fun invoke_serializer ctxt target some_width raw_module_name args program all_public syms =
let
val module_name = if raw_module_name = "" then ""
else (check_name true raw_module_name; raw_module_name)
- val (mounted_serializer, (prepared_syms, prepared_program)) = mount_serializer thy
- target some_width module_name args program syms;
+ val (mounted_serializer, (prepared_syms, prepared_program)) =
+ mount_serializer ctxt target some_width module_name args program syms;
in mounted_serializer prepared_program (if all_public then prepared_syms else []) end;
fun assert_module_name "" = error "Empty module name not allowed here"
| assert_module_name module_name = module_name;
-fun using_master_directory thy =
- Option.map (Path.append (File.pwd ()) o Path.append (Thy_Load.master_directory thy));
+fun using_master_directory ctxt =
+ Option.map (Path.append (File.pwd ()) o Path.append (Thy_Load.master_directory (Proof_Context.theory_of ctxt)));
in
val generatedN = "Generated_Code";
-fun export_code_for thy some_path target some_width module_name args =
- export (using_master_directory thy some_path)
- ooo invoke_serializer thy target some_width module_name args;
+fun export_code_for ctxt some_path target some_width module_name args =
+ export (using_master_directory ctxt some_path)
+ ooo invoke_serializer ctxt target some_width module_name args;
-fun produce_code_for thy target some_width module_name args =
+fun produce_code_for ctxt target some_width module_name args =
let
- val serializer = invoke_serializer thy target some_width (assert_module_name module_name) args;
+ val serializer = invoke_serializer ctxt target some_width (assert_module_name module_name) args;
in fn program => fn all_public => fn syms =>
produce (serializer program all_public syms) |> apsnd (fn deresolve => map deresolve syms)
end;
-fun present_code_for thy target some_width module_name args =
+fun present_code_for ctxt target some_width module_name args =
let
- val serializer = invoke_serializer thy target some_width (assert_module_name module_name) args;
+ val serializer = invoke_serializer ctxt target some_width (assert_module_name module_name) args;
in fn program => fn (syms, selects) =>
present selects (serializer program false syms)
end;
-fun check_code_for thy target strict args program all_public syms =
+fun check_code_for ctxt target strict args program all_public syms =
let
val { env_var, make_destination, make_command } =
- (#check o the_fundamental thy) target;
+ (#check o the_fundamental ctxt) target;
fun ext_check p =
let
val destination = make_destination p;
- val _ = export (SOME destination) (invoke_serializer thy target (SOME 80)
+ val _ = export (SOME destination) (invoke_serializer ctxt target (SOME 80)
generatedN args program all_public syms);
val cmd = make_command generatedN;
in
@@ -443,10 +444,10 @@
val value_name = the (deresolve Code_Symbol.value);
in (program_code, value_name) end;
-fun evaluator thy target program syms =
+fun evaluator ctxt target program syms =
let
val (mounted_serializer, (_, prepared_program)) =
- mount_serializer thy target NONE generatedN [] program syms;
+ mount_serializer ctxt target NONE generatedN [] program syms;
in evaluation mounted_serializer prepared_program syms end;
end; (* local *)
@@ -457,60 +458,66 @@
fun prep_destination "" = NONE
| prep_destination s = SOME (Path.explode s);
-fun export_code thy all_public cs seris =
+fun export_code ctxt all_public cs seris =
let
+ val thy = Proof_Context.theory_of ctxt;
val program = Code_Thingol.consts_program thy cs;
val _ = map (fn (((target, module_name), some_path), args) =>
- export_code_for thy some_path target NONE module_name args program all_public (map Constant cs)) seris;
+ export_code_for ctxt some_path target NONE module_name args program all_public (map Constant cs)) seris;
in () end;
-fun export_code_cmd all_public raw_cs seris thy =
- export_code thy all_public
- (Code_Thingol.read_const_exprs thy raw_cs)
+fun export_code_cmd all_public raw_cs seris ctxt =
+ export_code ctxt all_public
+ (Code_Thingol.read_const_exprs ctxt raw_cs)
((map o apfst o apsnd) prep_destination seris);
-fun produce_code thy all_public cs target some_width some_module_name args =
+fun produce_code ctxt all_public cs target some_width some_module_name args =
let
+ val thy = Proof_Context.theory_of ctxt;
val program = Code_Thingol.consts_program thy cs;
- in produce_code_for thy target some_width some_module_name args program all_public (map Constant cs) end;
+ in produce_code_for ctxt target some_width some_module_name args program all_public (map Constant cs) end;
-fun present_code thy cs syms target some_width some_module_name args =
+fun present_code ctxt cs syms target some_width some_module_name args =
let
+ val thy = Proof_Context.theory_of ctxt;
val program = Code_Thingol.consts_program thy cs;
- in present_code_for thy target some_width some_module_name args program (map Constant cs, syms) end;
+ in present_code_for ctxt target some_width some_module_name args program (map Constant cs, syms) end;
-fun check_code thy all_public cs seris =
+fun check_code ctxt all_public cs seris =
let
+ val thy = Proof_Context.theory_of ctxt;
val program = Code_Thingol.consts_program thy cs;
val _ = map (fn ((target, strict), args) =>
- check_code_for thy target strict args program all_public (map Constant cs)) seris;
+ check_code_for ctxt target strict args program all_public (map Constant cs)) seris;
in () end;
-fun check_code_cmd all_public raw_cs seris thy =
- check_code thy all_public
- (Code_Thingol.read_const_exprs thy raw_cs) seris;
+fun check_code_cmd all_public raw_cs seris ctxt =
+ check_code ctxt all_public
+ (Code_Thingol.read_const_exprs ctxt raw_cs) seris;
local
val parse_const_terms = Scan.repeat1 Args.term
- >> (fn ts => fn thy => map (Code.check_const thy) ts);
+ >> (fn ts => fn ctxt => map (Code.check_const (Proof_Context.theory_of ctxt)) ts);
fun parse_names category parse internalize mark_symbol =
Scan.lift (Args.parens (Args.$$$ category)) |-- Scan.repeat1 parse
- >> (fn xs => fn thy => map (mark_symbol o internalize thy) xs);
+ >> (fn xs => fn ctxt => map (mark_symbol o internalize ctxt) xs);
val parse_consts = parse_names "consts" Args.term
- Code.check_const Constant;
+ (Code.check_const o Proof_Context.theory_of) Constant;
val parse_types = parse_names "types" (Scan.lift Args.name)
- Sign.intern_type Type_Constructor;
+ (Sign.intern_type o Proof_Context.theory_of) Type_Constructor;
val parse_classes = parse_names "classes" (Scan.lift Args.name)
- Sign.intern_class Type_Class;
+ (Sign.intern_class o Proof_Context.theory_of) Type_Class;
val parse_instances = parse_names "instances" (Scan.lift (Args.name --| Args.$$$ "::" -- Args.name))
- (fn thy => fn (raw_tyco, raw_class) => (Sign.intern_class thy raw_tyco, Sign.intern_type thy raw_class))
- Class_Instance;
+ (fn ctxt => fn (raw_tyco, raw_class) =>
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ in (Sign.intern_class thy raw_tyco, Sign.intern_type thy raw_class) end) Class_Instance;
in
@@ -520,11 +527,9 @@
Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances)
-- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))
(fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target, some_width)) =>
- let val thy = Proof_Context.theory_of ctxt in
- present_code thy (mk_cs thy)
- (maps (fn f => f thy) mk_stmtss)
- target some_width "Example" []
- end);
+ present_code ctxt (mk_cs ctxt)
+ (maps (fn f => f ctxt) mk_stmtss)
+ target some_width "Example" []);
end;
@@ -535,7 +540,7 @@
fun add_reserved target sym thy =
let
- val (_, data) = collapse_hierarchy thy target;
+ val (_, data) = collapse_hierarchy (Proof_Context.init_global thy) target;
val _ = if member (op =) (the_reserved data) sym
then error ("Reserved symbol " ^ quote sym ^ " already declared")
else ();
@@ -547,13 +552,13 @@
(* checking of syntax *)
-fun check_const_syntax thy target c syn =
- if Code_Printer.requires_args syn > Code.args_number thy c
+fun check_const_syntax ctxt target c syn =
+ if Code_Printer.requires_args syn > Code.args_number (Proof_Context.theory_of ctxt) c
then error ("Too many arguments in syntax for constant " ^ quote c)
- else Code_Printer.prep_const_syntax thy (the_literals thy target) c syn;
+ else Code_Printer.prep_const_syntax (Proof_Context.theory_of ctxt) (the_literals ctxt target) c syn;
-fun check_tyco_syntax thy target tyco syn =
- if fst syn <> Sign.arity_number thy tyco
+fun check_tyco_syntax ctxt target tyco syn =
+ if fst syn <> Sign.arity_number (Proof_Context.theory_of ctxt) tyco
then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
else syn;
@@ -569,14 +574,14 @@
(arrange false) (arrange false) (arrange true) x
end;
-fun cert_name_decls thy = cert_syms thy #> arrange_name_decls;
+fun cert_name_decls ctxt = cert_syms ctxt #> arrange_name_decls;
-fun read_name_decls thy = read_syms thy #> arrange_name_decls;
+fun read_name_decls ctxt = read_syms ctxt #> arrange_name_decls;
fun set_identifier (target, sym_name) = map_identifiers target (Code_Symbol.set_data sym_name);
fun gen_set_identifiers prep_name_decl raw_name_decls thy =
- fold set_identifier (prep_name_decl thy raw_name_decls) thy;
+ fold set_identifier (prep_name_decl (Proof_Context.init_global thy) raw_name_decls) thy;
val set_identifiers = gen_set_identifiers cert_name_decls;
val set_identifiers_cmd = gen_set_identifiers read_name_decls;
@@ -584,26 +589,26 @@
(* custom printings *)
-fun arrange_printings prep_const thy =
+fun arrange_printings prep_const ctxt =
let
fun arrange check (sym, target_syns) =
- map (fn (target, some_syn) => (target, (sym, Option.map (check thy target sym) some_syn))) target_syns;
+ map (fn (target, some_syn) => (target, (sym, Option.map (check ctxt target sym) some_syn))) target_syns;
in
Code_Symbol.maps_attr'
(arrange check_const_syntax) (arrange check_tyco_syntax)
(arrange ((K o K o K) I)) (arrange ((K o K o K) I)) (arrange ((K o K o K) I))
- (arrange (fn thy => fn _ => fn _ => fn (raw_content, raw_cs) =>
- (Code_Printer.str raw_content, map (prep_const thy) raw_cs)))
+ (arrange (fn ctxt => fn _ => fn _ => fn (raw_content, raw_cs) =>
+ (Code_Printer.str raw_content, map (prep_const ctxt) raw_cs)))
end;
-fun cert_printings thy = cert_syms thy #> arrange_printings cert_const thy;
+fun cert_printings ctxt = cert_syms ctxt #> arrange_printings cert_const ctxt;
-fun read_printings thy = read_syms thy #> arrange_printings Code.read_const thy;
+fun read_printings ctxt = read_syms ctxt #> arrange_printings read_const ctxt;
fun set_printing (target, sym_syn) = map_printings target (Code_Symbol.set_data sym_syn);
fun gen_set_printings prep_print_decl raw_print_decls thy =
- fold set_printing (prep_print_decl thy raw_print_decls) thy;
+ fold set_printing (prep_print_decl (Proof_Context.init_global thy) raw_print_decls) thy;
val set_printings = gen_set_printings cert_printings;
val set_printings_cmd = gen_set_printings read_printings;
@@ -680,18 +685,18 @@
val _ =
Outer_Syntax.command @{command_spec "export_code"} "generate executable code for constants"
- (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
+ (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.context_of)));
(** external entrance point -- for codegen tool **)
fun codegen_tool thyname cmd_expr =
let
- val thy = Thy_Info.get_theory thyname;
+ val ctxt = Proof_Context.init_global (Thy_Info.get_theory thyname);
val parse = Scan.read Token.stopper (Parse.!!! code_exprP) o
(filter Token.is_proper o Outer_Syntax.scan Position.none);
in case parse cmd_expr
- of SOME f => (writeln "Now generating code..."; f thy)
+ of SOME f => (writeln "Now generating code..."; f ctxt)
| NONE => error ("Bad directive " ^ quote cmd_expr)
end;
--- a/src/Tools/Code/code_thingol.ML Wed Feb 26 10:10:38 2014 +0100
+++ b/src/Tools/Code/code_thingol.ML Wed Feb 26 11:57:52 2014 +0100
@@ -79,27 +79,28 @@
val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt
val is_constr: program -> Code_Symbol.T -> bool
val is_case: stmt -> bool
- val group_stmts: theory -> program
+ val group_stmts: Proof.context -> program
-> ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list
* ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list)) list
- val read_const_exprs: theory -> string list -> string list
+ val read_const_exprs: Proof.context -> string list -> string list
val consts_program: theory -> string list -> program
- val dynamic_conv: theory -> (program
+ val dynamic_conv: Proof.context -> (program
-> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> conv)
-> conv
- val dynamic_value: theory -> ((term -> term) -> 'a -> 'a) -> (program
+ val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> (program
-> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> 'a)
-> term -> 'a
- val static_conv: theory -> string list -> (program -> string list
- -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> conv)
- -> conv
- val static_conv_simple: theory -> string list
- -> (program -> (string * sort) list -> term -> conv) -> conv
- val static_value: theory -> ((term -> term) -> 'a -> 'a) -> string list ->
+ val static_conv: Proof.context -> string list -> (program -> string list
+ -> Proof.context -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> conv)
+ -> Proof.context -> conv
+ val static_conv_simple: Proof.context -> string list
+ -> (program -> Proof.context -> (string * sort) list -> term -> conv)
+ -> Proof.context -> conv
+ val static_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> string list ->
(program -> string list
- -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> 'a)
- -> term -> 'a
+ -> Proof.context -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> 'a)
+ -> Proof.context -> term -> 'a
end;
structure Code_Thingol: CODE_THINGOL =
@@ -334,7 +335,7 @@
rev (Code_Symbol.Graph.strong_conn program)
|> map (AList.make (Code_Symbol.Graph.get_node program));
-fun group_stmts thy program =
+fun group_stmts ctxt program =
let
fun is_fun (_, Fun _) = true | is_fun _ = false;
fun is_datatypecons (_, Datatypecons _) = true | is_datatypecons _ = false;
@@ -351,8 +352,7 @@
else if forall (is_fun orf is_classinst) stmts
then ([], [], List.partition is_fun stmts)
else error ("Illegal mutual dependencies: " ^ (commas
- o map (Code_Symbol.quote (Proof_Context.init_global thy)
- o fst)) stmts);
+ o map (Code_Symbol.quote ctxt o fst)) stmts);
in
linear_stmts program
|> map group
@@ -388,12 +388,11 @@
exception PERMISSIVE of unit;
-fun translation_error thy program permissive some_thm deps msg sub_msg =
+fun translation_error ctxt program permissive some_thm deps msg sub_msg =
if permissive
then raise PERMISSIVE ()
else
let
- val ctxt = Proof_Context.init_global thy;
val thm_msg =
Option.map (fn thm => "in code equation " ^ Display.string_of_thm ctxt thm) some_thm;
val dep_msg = if null (tl deps) then NONE
@@ -409,14 +408,14 @@
fun maybe_permissive f prgrm =
f prgrm |>> SOME handle PERMISSIVE () => (NONE, prgrm);
-fun not_wellsorted thy program permissive some_thm deps ty sort e =
+fun not_wellsorted ctxt program permissive some_thm deps ty sort e =
let
- val err_class = Sorts.class_error (Context.pretty_global thy) e;
+ val err_class = Sorts.class_error (Context.pretty ctxt) e;
val err_typ =
- "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort " ^
- Syntax.string_of_sort_global thy sort;
+ "Type " ^ Syntax.string_of_typ ctxt ty ^ " not of sort " ^
+ Syntax.string_of_sort ctxt sort;
in
- translation_error thy program permissive some_thm deps
+ translation_error ctxt program permissive some_thm deps
"Wellsortedness error" (err_typ ^ "\n" ^ err_class)
end;
@@ -442,25 +441,25 @@
| tag (Free _) (t as Free _) = t
| tag (Var _) (t as Var _) = t
| tag (Bound _) (t as Bound _) = t;
- in
- tag
- end
+ in tag end
-fun annotate thy algbr eqngr (c, ty) args rhs =
+fun annotate ctxt algbr eqngr (c, ty) args rhs =
let
- val ctxt = Proof_Context.init_global thy |> Config.put Type_Infer_Context.const_sorts false
- val erase = map_types (fn _ => Type_Infer.anyT [])
- val reinfer = singleton (Type_Infer_Context.infer_types ctxt)
- val lhs = list_comb (Const (c, ty), map (map_types Type.strip_sorts o fst) args)
- val reinferred_rhs = snd (Logic.dest_equals (reinfer (Logic.mk_equals (lhs, erase rhs))))
+ val erase = map_types (fn _ => Type_Infer.anyT []);
+ val reinfer = singleton (Type_Infer_Context.infer_types ctxt);
+ val lhs = list_comb (Const (c, ty), map (map_types Type.strip_sorts o fst) args);
+ val reinferred_rhs = snd (Logic.dest_equals (reinfer (Logic.mk_equals (lhs, erase rhs))));
+ in tag_term algbr eqngr reinferred_rhs rhs end
+
+fun annotate_eqns ctxt algbr eqngr (c, ty) eqns =
+ let
+ val ctxt' = ctxt |> Proof_Context.theory_of |> Proof_Context.init_global
+ |> Config.put Type_Infer_Context.const_sorts false;
+ (*avoid spurious fixed variables: there is no eigen context for equations*)
in
- tag_term algbr eqngr reinferred_rhs rhs
- end
-
-fun annotate_eqns thy algbr eqngr (c, ty) eqns =
- map (apfst (fn (args, (rhs, some_abs)) => (args,
- (annotate thy algbr eqngr (c, ty) args rhs, some_abs)))) eqns
-
+ map (apfst (fn (args, (rhs, some_abs)) => (args,
+ (annotate ctxt' algbr eqngr (c, ty) args rhs, some_abs)))) eqns
+ end;
(* abstract dictionary construction *)
@@ -470,7 +469,7 @@
Global of (string * class) * typarg_witness list list
| Local of string * (int * sort);
-fun construct_dictionaries thy (proj_sort, algebra) permissive some_thm (ty, sort) (deps, program) =
+fun construct_dictionaries ctxt (proj_sort, algebra) permissive some_thm (ty, sort) (deps, program) =
let
fun class_relation ((Weakening (classrels, x)), sub_class) super_class =
Weakening ((sub_class, super_class) :: classrels, x);
@@ -484,42 +483,44 @@
{class_relation = K (Sorts.classrel_derivation algebra class_relation),
type_constructor = type_constructor,
type_variable = type_variable} (ty, proj_sort sort)
- handle Sorts.CLASS_ERROR e => not_wellsorted thy program permissive some_thm deps ty sort e;
+ handle Sorts.CLASS_ERROR e => not_wellsorted ctxt program permissive some_thm deps ty sort e;
in (typarg_witnesses, (deps, program)) end;
(* translation *)
-fun ensure_tyco thy algbr eqngr permissive tyco =
+fun ensure_tyco ctxt algbr eqngr permissive tyco =
let
+ val thy = Proof_Context.theory_of ctxt;
val ((vs, cos), _) = Code.get_type thy tyco;
val stmt_datatype =
- fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
+ fold_map (translate_tyvar_sort ctxt algbr eqngr permissive) vs
#>> map fst
##>> fold_map (fn (c, (vs, tys)) =>
- ensure_const thy algbr eqngr permissive c
+ ensure_const ctxt algbr eqngr permissive c
##>> pair (map (unprefix "'" o fst) vs)
- ##>> fold_map (translate_typ thy algbr eqngr permissive) tys) cos
+ ##>> fold_map (translate_typ ctxt algbr eqngr permissive) tys) cos
#>> Datatype;
in ensure_stmt Type_Constructor stmt_datatype tyco end
-and ensure_const thy algbr eqngr permissive c =
+and ensure_const ctxt algbr eqngr permissive c =
let
+ val thy = Proof_Context.theory_of ctxt;
fun stmt_datatypecons tyco =
- ensure_tyco thy algbr eqngr permissive tyco
+ ensure_tyco ctxt algbr eqngr permissive tyco
#>> Datatypecons;
fun stmt_classparam class =
- ensure_class thy algbr eqngr permissive class
+ ensure_class ctxt algbr eqngr permissive class
#>> Classparam;
fun stmt_fun cert = case Code.equations_of_cert thy cert
of (_, NONE) => pair NoStmt
| ((vs, ty), SOME eqns) =>
let
- val eqns' = annotate_eqns thy algbr eqngr (c, ty) eqns
+ val eqns' = annotate_eqns ctxt algbr eqngr (c, ty) eqns
val some_case_cong = Code.get_case_cong thy c;
in
- fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
- ##>> translate_typ thy algbr eqngr permissive ty
- ##>> translate_eqns thy algbr eqngr permissive eqns'
+ fold_map (translate_tyvar_sort ctxt algbr eqngr permissive) vs
+ ##>> translate_typ ctxt algbr eqngr permissive ty
+ ##>> translate_eqns ctxt algbr eqngr permissive eqns'
#>>
(fn (_, NONE) => NoStmt
| (tyscm, SOME eqns) => Fun ((tyscm, eqns), some_case_cong))
@@ -530,26 +531,28 @@
of SOME class => stmt_classparam class
| NONE => stmt_fun (Code_Preproc.cert eqngr c))
in ensure_stmt Constant stmt_const c end
-and ensure_class thy (algbr as (_, algebra)) eqngr permissive class =
+and ensure_class ctxt (algbr as (_, algebra)) eqngr permissive class =
let
+ val thy = Proof_Context.theory_of ctxt;
val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
val cs = #params (Axclass.get_info thy class);
val stmt_class =
fold_map (fn super_class =>
- ensure_classrel thy algbr eqngr permissive (class, super_class)) super_classes
- ##>> fold_map (fn (c, ty) => ensure_const thy algbr eqngr permissive c
- ##>> translate_typ thy algbr eqngr permissive ty) cs
+ ensure_classrel ctxt algbr eqngr permissive (class, super_class)) super_classes
+ ##>> fold_map (fn (c, ty) => ensure_const ctxt algbr eqngr permissive c
+ ##>> translate_typ ctxt algbr eqngr permissive ty) cs
#>> (fn info => Class (unprefix "'" Name.aT, info))
in ensure_stmt Type_Class stmt_class class end
-and ensure_classrel thy algbr eqngr permissive (sub_class, super_class) =
+and ensure_classrel ctxt algbr eqngr permissive (sub_class, super_class) =
let
val stmt_classrel =
- ensure_class thy algbr eqngr permissive sub_class
- ##>> ensure_class thy algbr eqngr permissive super_class
+ ensure_class ctxt algbr eqngr permissive sub_class
+ ##>> ensure_class ctxt algbr eqngr permissive super_class
#>> Classrel;
in ensure_stmt Class_Relation stmt_classrel (sub_class, super_class) end
-and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (tyco, class) =
+and ensure_inst ctxt (algbr as (_, algebra)) eqngr permissive (tyco, class) =
let
+ val thy = Proof_Context.theory_of ctxt;
val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
val these_class_params = these o try (#params o Axclass.get_info thy);
val class_params = these_class_params class;
@@ -562,8 +565,8 @@
val arity_typ = Type (tyco, map TFree vs);
val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
fun translate_super_instance super_class =
- ensure_class thy algbr eqngr permissive super_class
- ##>> translate_dicts thy algbr eqngr permissive NONE (arity_typ, [super_class])
+ ensure_class ctxt algbr eqngr permissive super_class
+ ##>> translate_dicts ctxt algbr eqngr permissive NONE (arity_typ, [super_class])
#>> (fn (super_class, [Dict ([], Dict_Const (_, dss))]) => (super_class, dss));
fun translate_classparam_instance (c, ty) =
let
@@ -573,14 +576,14 @@
val const = (apsnd Logic.unvarifyT_global o dest_Const o snd
o Logic.dest_equals o Thm.prop_of) thm;
in
- ensure_const thy algbr eqngr permissive c
- ##>> translate_const thy algbr eqngr permissive (SOME thm) (const, NONE)
+ ensure_const ctxt algbr eqngr permissive c
+ ##>> translate_const ctxt algbr eqngr permissive (SOME thm) (const, NONE)
#>> (fn (c, IConst const') => ((c, (const', dom_length)), (thm, true)))
end;
val stmt_inst =
- ensure_class thy algbr eqngr permissive class
- ##>> ensure_tyco thy algbr eqngr permissive tyco
- ##>> fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
+ ensure_class ctxt algbr eqngr permissive class
+ ##>> ensure_tyco ctxt algbr eqngr permissive tyco
+ ##>> fold_map (translate_tyvar_sort ctxt algbr eqngr permissive) vs
##>> fold_map translate_super_instance super_classes
##>> fold_map translate_classparam_instance class_params
##>> fold_map translate_classparam_instance superclass_params
@@ -588,69 +591,72 @@
Classinst { class = class, tyco = tyco, vs = vs,
superinsts = superinsts, inst_params = inst_params, superinst_params = superinst_params });
in ensure_stmt Class_Instance stmt_inst (tyco, class) end
-and translate_typ thy algbr eqngr permissive (TFree (v, _)) =
+and translate_typ ctxt algbr eqngr permissive (TFree (v, _)) =
pair (ITyVar (unprefix "'" v))
- | translate_typ thy algbr eqngr permissive (Type (tyco, tys)) =
- ensure_tyco thy algbr eqngr permissive tyco
- ##>> fold_map (translate_typ thy algbr eqngr permissive) tys
+ | translate_typ ctxt algbr eqngr permissive (Type (tyco, tys)) =
+ ensure_tyco ctxt algbr eqngr permissive tyco
+ ##>> fold_map (translate_typ ctxt algbr eqngr permissive) tys
#>> (fn (tyco, tys) => tyco `%% tys)
-and translate_term thy algbr eqngr permissive some_thm (Const (c, ty), some_abs) =
- translate_app thy algbr eqngr permissive some_thm (((c, ty), []), some_abs)
- | translate_term thy algbr eqngr permissive some_thm (Free (v, _), some_abs) =
+and translate_term ctxt algbr eqngr permissive some_thm (Const (c, ty), some_abs) =
+ translate_app ctxt algbr eqngr permissive some_thm (((c, ty), []), some_abs)
+ | translate_term ctxt algbr eqngr permissive some_thm (Free (v, _), some_abs) =
pair (IVar (SOME v))
- | translate_term thy algbr eqngr permissive some_thm (Abs (v, ty, t), some_abs) =
+ | translate_term ctxt algbr eqngr permissive some_thm (Abs (v, ty, t), some_abs) =
let
val (v', t') = Syntax_Trans.variant_abs (Name.desymbolize false v, ty, t);
val v'' = if member (op =) (Term.add_free_names t' []) v'
then SOME v' else NONE
in
- translate_typ thy algbr eqngr permissive ty
- ##>> translate_term thy algbr eqngr permissive some_thm (t', some_abs)
+ translate_typ ctxt algbr eqngr permissive ty
+ ##>> translate_term ctxt algbr eqngr permissive some_thm (t', some_abs)
#>> (fn (ty, t) => (v'', ty) `|=> t)
end
- | translate_term thy algbr eqngr permissive some_thm (t as _ $ _, some_abs) =
+ | translate_term ctxt algbr eqngr permissive some_thm (t as _ $ _, some_abs) =
case strip_comb t
of (Const (c, ty), ts) =>
- translate_app thy algbr eqngr permissive some_thm (((c, ty), ts), some_abs)
+ translate_app ctxt algbr eqngr permissive some_thm (((c, ty), ts), some_abs)
| (t', ts) =>
- translate_term thy algbr eqngr permissive some_thm (t', some_abs)
- ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts
+ translate_term ctxt algbr eqngr permissive some_thm (t', some_abs)
+ ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) ts
#>> (fn (t, ts) => t `$$ ts)
-and translate_eqn thy algbr eqngr permissive ((args, (rhs, some_abs)), (some_thm, proper)) =
- fold_map (translate_term thy algbr eqngr permissive some_thm) args
- ##>> translate_term thy algbr eqngr permissive some_thm (rhs, some_abs)
+and translate_eqn ctxt algbr eqngr permissive ((args, (rhs, some_abs)), (some_thm, proper)) =
+ fold_map (translate_term ctxt algbr eqngr permissive some_thm) args
+ ##>> translate_term ctxt algbr eqngr permissive some_thm (rhs, some_abs)
#>> rpair (some_thm, proper)
-and translate_eqns thy algbr eqngr permissive eqns =
- maybe_permissive (fold_map (translate_eqn thy algbr eqngr permissive) eqns)
-and translate_const thy algbr eqngr permissive some_thm ((c, ty), some_abs) (deps, program) =
+and translate_eqns ctxt algbr eqngr permissive eqns =
+ maybe_permissive (fold_map (translate_eqn ctxt algbr eqngr permissive) eqns)
+and translate_const ctxt algbr eqngr permissive some_thm ((c, ty), some_abs) (deps, program) =
let
+ val thy = Proof_Context.theory_of ctxt;
val _ = if (case some_abs of NONE => true | SOME abs => not (c = abs))
andalso Code.is_abstr thy c
- then translation_error thy program permissive some_thm deps
+ then translation_error ctxt program permissive some_thm deps
"Abstraction violation" ("constant " ^ Code.string_of_const thy c)
else ()
- in translate_const_proper thy algbr eqngr permissive some_thm (c, ty) (deps, program) end
-and translate_const_proper thy algbr eqngr permissive some_thm (c, ty) =
+ in translate_const_proper ctxt algbr eqngr permissive some_thm (c, ty) (deps, program) end
+and translate_const_proper ctxt algbr eqngr permissive some_thm (c, ty) =
let
+ val thy = Proof_Context.theory_of ctxt;
val (annotate, ty') = dest_tagged_type ty;
val typargs = Sign.const_typargs thy (c, ty');
val sorts = Code_Preproc.sortargs eqngr c;
val (dom, range) = Term.strip_type ty';
in
- ensure_const thy algbr eqngr permissive c
- ##>> fold_map (translate_typ thy algbr eqngr permissive) typargs
- ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (typargs ~~ sorts)
- ##>> fold_map (translate_typ thy algbr eqngr permissive) (range :: dom)
+ ensure_const ctxt algbr eqngr permissive c
+ ##>> fold_map (translate_typ ctxt algbr eqngr permissive) typargs
+ ##>> fold_map (translate_dicts ctxt algbr eqngr permissive some_thm) (typargs ~~ sorts)
+ ##>> fold_map (translate_typ ctxt algbr eqngr permissive) (range :: dom)
#>> (fn (((c, typargs), dss), range :: dom) =>
IConst { sym = Constant c, typargs = typargs, dicts = dss,
dom = dom, range = range, annotate = annotate })
end
-and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
- translate_const thy algbr eqngr permissive some_thm (c_ty, some_abs)
- ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts
+and translate_app_const ctxt algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
+ translate_const ctxt algbr eqngr permissive some_thm (c_ty, some_abs)
+ ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) ts
#>> (fn (t, ts) => t `$$ ts)
-and translate_case thy algbr eqngr permissive some_thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
+and translate_case ctxt algbr eqngr permissive some_thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
let
+ val thy = Proof_Context.theory_of ctxt;
val undefineds = Code.undefineds thy;
fun arg_types num_args ty = fst (chop num_args (binder_types ty));
val tys = arg_types num_args (snd c_ty);
@@ -696,53 +702,53 @@
(case_pats ~~ ts_clause)));
in ICase { term = t, typ = ty, clauses = clauses, primitive = t_app `$$ ts } end;
in
- translate_const thy algbr eqngr permissive some_thm (c_ty, NONE)
- ##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr permissive some_thm (constr, NONE)
+ translate_const ctxt algbr eqngr permissive some_thm (c_ty, NONE)
+ ##>> fold_map (fn (constr, n) => translate_const ctxt algbr eqngr permissive some_thm (constr, NONE)
#>> rpair n) constrs
- ##>> translate_typ thy algbr eqngr permissive ty
- ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts
+ ##>> translate_typ ctxt algbr eqngr permissive ty
+ ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) ts
#>> (fn (((t, constrs), ty), ts) =>
casify constrs ty t ts)
end
-and translate_app_case thy algbr eqngr permissive some_thm (case_scheme as (num_args, _)) ((c, ty), ts) =
+and translate_app_case ctxt algbr eqngr permissive some_thm (case_scheme as (num_args, _)) ((c, ty), ts) =
if length ts < num_args then
let
val k = length ts;
val tys = (take (num_args - k) o drop k o fst o strip_type) ty;
- val ctxt = (fold o fold_aterms) Term.declare_term_frees ts Name.context;
- val vs = Name.invent_names ctxt "a" tys;
+ val names = (fold o fold_aterms) Term.declare_term_frees ts Name.context;
+ val vs = Name.invent_names names "a" tys;
in
- fold_map (translate_typ thy algbr eqngr permissive) tys
- ##>> translate_case thy algbr eqngr permissive some_thm case_scheme ((c, ty), ts @ map Free vs)
+ fold_map (translate_typ ctxt algbr eqngr permissive) tys
+ ##>> translate_case ctxt algbr eqngr permissive some_thm case_scheme ((c, ty), ts @ map Free vs)
#>> (fn (tys, t) => map2 (fn (v, _) => pair (SOME v)) vs tys `|==> t)
end
else if length ts > num_args then
- translate_case thy algbr eqngr permissive some_thm case_scheme ((c, ty), take num_args ts)
- ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) (drop num_args ts)
+ translate_case ctxt algbr eqngr permissive some_thm case_scheme ((c, ty), take num_args ts)
+ ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) (drop num_args ts)
#>> (fn (t, ts) => t `$$ ts)
else
- translate_case thy algbr eqngr permissive some_thm case_scheme ((c, ty), ts)
-and translate_app thy algbr eqngr permissive some_thm (c_ty_ts as ((c, _), _), some_abs) =
- case Code.get_case_scheme thy c
- of SOME case_scheme => translate_app_case thy algbr eqngr permissive some_thm case_scheme c_ty_ts
- | NONE => translate_app_const thy algbr eqngr permissive some_thm (c_ty_ts, some_abs)
-and translate_tyvar_sort thy (algbr as (proj_sort, _)) eqngr permissive (v, sort) =
- fold_map (ensure_class thy algbr eqngr permissive) (proj_sort sort)
+ translate_case ctxt algbr eqngr permissive some_thm case_scheme ((c, ty), ts)
+and translate_app ctxt algbr eqngr permissive some_thm (c_ty_ts as ((c, _), _), some_abs) =
+ case Code.get_case_scheme (Proof_Context.theory_of ctxt) c
+ of SOME case_scheme => translate_app_case ctxt algbr eqngr permissive some_thm case_scheme c_ty_ts
+ | NONE => translate_app_const ctxt algbr eqngr permissive some_thm (c_ty_ts, some_abs)
+and translate_tyvar_sort ctxt (algbr as (proj_sort, _)) eqngr permissive (v, sort) =
+ fold_map (ensure_class ctxt algbr eqngr permissive) (proj_sort sort)
#>> (fn sort => (unprefix "'" v, sort))
-and translate_dicts thy algbr eqngr permissive some_thm (ty, sort) =
+and translate_dicts ctxt algbr eqngr permissive some_thm (ty, sort) =
let
fun mk_dict (Weakening (classrels, x)) =
- fold_map (ensure_classrel thy algbr eqngr permissive) classrels
+ fold_map (ensure_classrel ctxt algbr eqngr permissive) classrels
##>> mk_plain_dict x
#>> Dict
and mk_plain_dict (Global (inst, dss)) =
- ensure_inst thy algbr eqngr permissive inst
+ ensure_inst ctxt algbr eqngr permissive inst
##>> (fold_map o fold_map) mk_dict dss
#>> (fn (inst, dss) => Dict_Const (inst, dss))
| mk_plain_dict (Local (v, (n, sort))) =
pair (Dict_Var (unprefix "'" v, (n, length sort)))
in
- construct_dictionaries thy algbr permissive some_thm (ty, sort)
+ construct_dictionaries ctxt algbr permissive some_thm (ty, sort)
#-> (fn typarg_witnesses => fold_map mk_dict typarg_witnesses)
end;
@@ -758,7 +764,7 @@
fun invoke_generation ignore_cache thy (algebra, eqngr) generate thing =
Program.change_yield (if ignore_cache then NONE else SOME thy)
(fn program => ([], program)
- |> generate thy algebra eqngr thing
+ |> generate (Proof_Context.init_global thy) algebra eqngr thing
|-> (fn thing => fn (_, program) => (thing, program)));
@@ -766,8 +772,8 @@
fun consts_program_internal thy permissive consts =
let
- fun generate_consts thy algebra eqngr =
- fold_map (ensure_const thy algebra eqngr permissive);
+ fun generate_consts ctxt algebra eqngr =
+ fold_map (ensure_const ctxt algebra eqngr permissive);
in
invoke_generation permissive thy (Code_Preproc.obtain false thy consts [])
generate_consts consts
@@ -789,17 +795,17 @@
(* value evaluation *)
-fun ensure_value thy algbr eqngr t =
+fun ensure_value ctxt algbr eqngr t =
let
val ty = fastype_of t;
val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
o dest_TFree))) t [];
- val t' = annotate thy algbr eqngr (@{const_name dummy_pattern}, ty) [] t;
+ val t' = annotate ctxt algbr eqngr (@{const_name dummy_pattern}, ty) [] t;
val dummy_constant = Constant @{const_name dummy_pattern};
val stmt_value =
- fold_map (translate_tyvar_sort thy algbr eqngr false) vs
- ##>> translate_typ thy algbr eqngr false ty
- ##>> translate_term thy algbr eqngr false NONE (t', NONE)
+ fold_map (translate_tyvar_sort ctxt algbr eqngr false) vs
+ ##>> translate_typ ctxt algbr eqngr false ty
+ ##>> translate_term ctxt algbr eqngr false NONE (t', NONE)
#>> (fn ((vs, ty), t) => Fun
(((vs, ty), [(([], t), (NONE, true))]), NONE));
fun term_value (deps, program1) =
@@ -820,62 +826,61 @@
fun original_sorts vs =
map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v));
-fun dynamic_evaluator thy evaluator algebra eqngr vs t =
+fun dynamic_evaluator ctxt evaluator algebra eqngr vs t =
let
val ((program, (((vs', ty'), t'), deps)), _) =
- invoke_generation false thy (algebra, eqngr) ensure_value t;
+ invoke_generation false (Proof_Context.theory_of ctxt) (algebra, eqngr) ensure_value t;
in evaluator program ((original_sorts vs vs', (vs', ty')), t') deps end;
-fun dynamic_conv thy evaluator =
- Code_Preproc.dynamic_conv thy (dynamic_evaluator thy evaluator);
+fun dynamic_conv ctxt conv =
+ Code_Preproc.dynamic_conv ctxt (dynamic_evaluator ctxt conv);
-fun dynamic_value thy postproc evaluator =
- Code_Preproc.dynamic_value thy postproc (dynamic_evaluator thy evaluator);
+fun dynamic_value ctxt postproc evaluator =
+ Code_Preproc.dynamic_value ctxt postproc (dynamic_evaluator ctxt evaluator);
-fun lift_evaluation thy evaluation' algebra eqngr program vs t =
+fun lift_evaluation ctxt evaluation algebra eqngr program vs t =
let
val ((_, (((vs', ty'), t'), deps)), _) =
- ensure_value thy algebra eqngr t ([], program);
- in evaluation' ((original_sorts vs vs', (vs', ty')), t') deps end;
+ ensure_value ctxt algebra eqngr t ([], program);
+ in evaluation ctxt ((original_sorts vs vs', (vs', ty')), t') deps end;
-fun lift_evaluator thy evaluator' consts algebra eqngr =
+fun lift_evaluator ctxt evaluator consts algebra eqngr =
let
- fun generate_consts thy algebra eqngr =
- fold_map (ensure_const thy algebra eqngr false);
+ fun generate_consts ctxt algebra eqngr =
+ fold_map (ensure_const ctxt algebra eqngr false);
val (consts', program) =
- invoke_generation true thy (algebra, eqngr) generate_consts consts;
- val evaluation' = evaluator' program consts';
- in lift_evaluation thy evaluation' algebra eqngr program end;
+ invoke_generation true (Proof_Context.theory_of ctxt) (algebra, eqngr) generate_consts consts;
+ val evaluation = evaluator program consts';
+ in fn ctxt' => lift_evaluation ctxt' evaluation algebra eqngr program end;
-fun lift_evaluator_simple thy evaluator' consts algebra eqngr =
+fun lift_evaluator_simple ctxt evaluator consts algebra eqngr =
let
- fun generate_consts thy algebra eqngr =
- fold_map (ensure_const thy algebra eqngr false);
+ fun generate_consts ctxt algebra eqngr =
+ fold_map (ensure_const ctxt algebra eqngr false);
val (_, program) =
- invoke_generation true thy (algebra, eqngr) generate_consts consts;
- in evaluator' program end;
+ invoke_generation true (Proof_Context.theory_of ctxt) (algebra, eqngr) generate_consts consts;
+ in evaluator program end;
-fun static_conv thy consts conv =
- Code_Preproc.static_conv thy consts (lift_evaluator thy conv consts);
+fun static_conv ctxt consts conv =
+ Code_Preproc.static_conv ctxt consts (lift_evaluator ctxt conv consts);
-fun static_conv_simple thy consts conv =
- Code_Preproc.static_conv thy consts (lift_evaluator_simple thy conv consts);
+fun static_conv_simple ctxt consts conv =
+ Code_Preproc.static_conv ctxt consts (lift_evaluator_simple ctxt conv consts);
-fun static_value thy postproc consts evaluator =
- Code_Preproc.static_value thy postproc consts (lift_evaluator thy evaluator consts);
+fun static_value ctxt postproc consts evaluator =
+ Code_Preproc.static_value ctxt postproc consts (lift_evaluator ctxt evaluator consts);
(** constant expressions **)
-fun read_const_exprs_internal thy =
+fun read_const_exprs_internal ctxt =
let
+ val thy = Proof_Context.theory_of ctxt;
fun consts_of thy' = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
((snd o #constants o Consts.dest o Sign.consts_of) thy') [];
fun belongs_here thy' c = forall
(fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy');
fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');
-
- val ctxt = Proof_Context.init_global thy;
fun read_const_expr str =
(case Syntax.parse_token ctxt (K NONE) Markup.empty (SOME o Symbol_Pos.implode o #1) str of
SOME "_" => ([], consts_of thy)
@@ -886,28 +891,30 @@
| NONE => ([Code.read_const thy str], []));
in pairself flat o split_list o map read_const_expr end;
-fun read_const_exprs_all thy = op @ o read_const_exprs_internal thy;
+fun read_const_exprs_all ctxt = op @ o read_const_exprs_internal ctxt;
-fun read_const_exprs thy const_exprs =
+fun read_const_exprs ctxt const_exprs =
let
- val (consts, consts_permissive) = read_const_exprs_internal thy const_exprs;
- val consts' = implemented_deps (consts_program_permissive thy consts_permissive);
+ val (consts, consts_permissive) = read_const_exprs_internal ctxt const_exprs;
+ val consts' = implemented_deps
+ (consts_program_permissive ((Proof_Context.theory_of ctxt)) consts_permissive);
in union (op =) consts' consts end;
(** diagnostic commands **)
-fun code_depgr thy consts =
+fun code_depgr ctxt consts =
let
- val (_, eqngr) = Code_Preproc.obtain true thy consts [];
+ val (_, eqngr) = Code_Preproc.obtain true ((Proof_Context.theory_of ctxt)) consts [];
val all_consts = Graph.all_succs eqngr consts;
in Graph.restrict (member (op =) all_consts) eqngr end;
-fun code_thms thy = Pretty.writeln o Code_Preproc.pretty thy o code_depgr thy;
+fun code_thms ctxt = Pretty.writeln o Code_Preproc.pretty ctxt o code_depgr ctxt;
-fun code_deps thy consts =
+fun code_deps ctxt consts =
let
- val eqngr = code_depgr thy consts;
+ val thy = Proof_Context.theory_of ctxt;
+ val eqngr = code_depgr ctxt consts;
val constss = Graph.strong_conn eqngr;
val mapping = Symtab.empty |> fold (fn consts => fold (fn const =>
Symtab.update (const, consts)) consts) constss;
@@ -926,8 +933,8 @@
local
-fun code_thms_cmd thy = code_thms thy o read_const_exprs_all thy;
-fun code_deps_cmd thy = code_deps thy o read_const_exprs_all thy;
+fun code_thms_cmd ctxt = code_thms ctxt o read_const_exprs_all ctxt;
+fun code_deps_cmd ctxt = code_deps ctxt o read_const_exprs_all ctxt;
in
@@ -935,15 +942,15 @@
Outer_Syntax.improper_command @{command_spec "code_thms"}
"print system of code equations for code"
(Scan.repeat1 Parse.term >> (fn cs =>
- Toplevel.unknown_theory o
- Toplevel.keep (fn state => code_thms_cmd (Toplevel.theory_of state) cs)));
+ Toplevel.unknown_context o
+ Toplevel.keep (fn state => code_thms_cmd (Toplevel.context_of state) cs)));
val _ =
Outer_Syntax.improper_command @{command_spec "code_deps"}
"visualize dependencies of code equations for code"
(Scan.repeat1 Parse.term >> (fn cs =>
- Toplevel.unknown_theory o
- Toplevel.keep (fn state => code_deps_cmd (Toplevel.theory_of state) cs)));
+ Toplevel.unknown_context o
+ Toplevel.keep (fn state => code_deps_cmd (Toplevel.context_of state) cs)));
end;
--- a/src/Tools/nbe.ML Wed Feb 26 10:10:38 2014 +0100
+++ b/src/Tools/nbe.ML Wed Feb 26 11:57:52 2014 +0100
@@ -6,10 +6,10 @@
signature NBE =
sig
- val dynamic_conv: theory -> conv
- val dynamic_value: theory -> term -> term
- val static_conv: theory -> string list -> conv
- val static_value: theory -> string list -> term -> term
+ val dynamic_conv: Proof.context -> conv
+ val dynamic_value: Proof.context -> term -> term
+ val static_conv: Proof.context -> string list -> Proof.context -> conv
+ val static_value: Proof.context -> string list -> Proof.context -> term -> term
datatype Univ =
Const of int * Univ list (*named (uninterpreted) constants*)
@@ -83,8 +83,9 @@
in
-fun lift_triv_classes_conv thy conv ct =
+fun lift_triv_classes_conv ctxt conv ct =
let
+ val thy = Proof_Context.theory_of ctxt;
val algebra = Sign.classes_of thy;
val certT = Thm.ctyp_of thy;
val triv_classes = get_triv_classes thy;
@@ -128,8 +129,9 @@
|> strip_of_class
end;
-fun lift_triv_classes_rew thy rew t =
+fun lift_triv_classes_rew ctxt rew t =
let
+ val thy = Proof_Context.theory_of ctxt;
val algebra = Sign.classes_of thy;
val triv_classes = get_triv_classes thy;
val vs = Term.add_tfrees t [];
@@ -388,10 +390,9 @@
(* compile equations *)
-fun compile_eqnss thy nbe_program raw_deps [] = []
- | compile_eqnss thy nbe_program raw_deps eqnss =
+fun compile_eqnss ctxt nbe_program raw_deps [] = []
+ | compile_eqnss ctxt nbe_program raw_deps eqnss =
let
- val ctxt = Proof_Context.init_global thy;
val (deps, deps_vals) = split_list (map_filter
(fn dep => Option.map (fn univ => (dep, univ)) (fst ((Code_Symbol.Graph.get_node nbe_program dep)))) raw_deps);
val idx_of = raw_deps
@@ -453,7 +454,7 @@
else (Code_Symbol.Graph.new_node (name, (NONE, maxidx)) nbe_program,
(maxidx + 1, Inttab.update_new (maxidx, name) idx_tab));
-fun compile_stmts thy stmts_deps =
+fun compile_stmts ctxt stmts_deps =
let
val names = map (fst o fst) stmts_deps;
val names_deps = map (fn ((name, _), deps) => (name, deps)) stmts_deps;
@@ -463,7 +464,7 @@
|> distinct (op =)
|> fold (insert (op =)) names;
fun compile nbe_program = eqnss
- |> compile_eqnss thy nbe_program refl_deps
+ |> compile_eqnss ctxt nbe_program refl_deps
|> rpair nbe_program;
in
fold ensure_const_idx refl_deps
@@ -472,12 +473,12 @@
#-> fold (fn (name, univ) => (Code_Symbol.Graph.map_node name o apfst) (K (SOME univ))))
end;
-fun compile_program thy program =
+fun compile_program ctxt program =
let
fun add_stmts names (nbe_program, (maxidx, idx_tab)) = if exists ((can o Code_Symbol.Graph.get_node) nbe_program) names
then (nbe_program, (maxidx, idx_tab))
else (nbe_program, (maxidx, idx_tab))
- |> compile_stmts thy (map (fn name => ((name, Code_Symbol.Graph.get_node program name),
+ |> compile_stmts ctxt (map (fn name => ((name, Code_Symbol.Graph.get_node program name),
Code_Symbol.Graph.immediate_succs program name)) names);
in
fold_rev add_stmts (Code_Symbol.Graph.strong_conn program)
@@ -488,12 +489,12 @@
(* term evaluation by compilation *)
-fun compile_term thy nbe_program deps (vs : (string * sort) list, t) =
+fun compile_term ctxt nbe_program deps (vs : (string * sort) list, t) =
let
val dict_frees = maps (fn (v, sort) => map_index (curry DFree v o fst) sort) vs;
in
(Code_Symbol.value, (vs, [([], t)]))
- |> singleton (compile_eqnss thy nbe_program deps)
+ |> singleton (compile_eqnss ctxt nbe_program deps)
|> snd
|> (fn t => apps t (rev dict_frees))
end;
@@ -506,7 +507,7 @@
| typ_of_itype vs (ITyVar v) =
TFree ("'" ^ v, (the o AList.lookup (op =) vs) v);
-fun term_of_univ thy (idx_tab : Code_Symbol.T Inttab.table) t =
+fun term_of_univ ctxt (idx_tab : Code_Symbol.T Inttab.table) t =
let
fun take_until f [] = []
| take_until f (x :: xs) = if f x then [] else x :: take_until f xs;
@@ -527,7 +528,7 @@
val const = const_of_idx idx;
val T = map_type_tvar (fn ((v, i), _) =>
Type_Infer.param typidx (v ^ string_of_int i, []))
- (Sign.the_const_type thy const);
+ (Sign.the_const_type (Proof_Context.theory_of ctxt) const);
val typidx' = typidx + 1;
in of_apps bounds (Term.Const (const, T), ts') typidx' end
| of_univ bounds (BVar (n, ts)) typidx =
@@ -541,9 +542,9 @@
(* evaluation with type reconstruction *)
-fun eval_term thy (nbe_program, idx_tab) ((vs0, (vs, ty)), t) deps =
+fun eval_term raw_ctxt (nbe_program, idx_tab) ((vs0, (vs, ty)), t) deps =
let
- val ctxt = Syntax.init_pretty_global thy;
+ val ctxt = Syntax.init_pretty_global (Proof_Context.theory_of raw_ctxt);
val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
val ty' = typ_of_itype vs0 ty;
fun type_infer t =
@@ -553,8 +554,8 @@
if null (Term.add_tvars t []) then t
else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t);
in
- compile_term thy nbe_program deps (vs, t)
- |> term_of_univ thy idx_tab
+ compile_term ctxt nbe_program deps (vs, t)
+ |> term_of_univ ctxt idx_tab
|> traced (fn t => "Normalized:\n" ^ string_of_term t)
|> type_infer
|> traced (fn t => "Types inferred:\n" ^ string_of_term t)
@@ -571,18 +572,19 @@
val empty = (Code_Symbol.Graph.empty, (0, Inttab.empty));
);
-fun compile ignore_cache thy program =
+fun compile ignore_cache ctxt program =
let
val (nbe_program, (_, idx_tab)) =
- Nbe_Functions.change (if ignore_cache then NONE else SOME thy)
- (compile_program thy program);
+ Nbe_Functions.change (if ignore_cache then NONE else SOME (Proof_Context.theory_of ctxt))
+ (compile_program ctxt program);
in (nbe_program, idx_tab) end;
(* evaluation oracle *)
-fun mk_equals thy lhs raw_rhs =
+fun mk_equals ctxt lhs raw_rhs =
let
+ val thy = Proof_Context.theory_of ctxt;
val ty = Thm.typ_of (Thm.ctyp_of_term lhs);
val eq = Thm.cterm_of thy (Term.Const ("==", ty --> ty --> propT));
val rhs = Thm.cterm_of thy raw_rhs;
@@ -590,28 +592,33 @@
val (_, raw_oracle) = Context.>>> (Context.map_theory_result
(Thm.add_oracle (@{binding normalization_by_evaluation},
- fn (thy, nbe_program_idx_tab, vsp_ty_t, deps, ct) =>
- mk_equals thy ct (eval_term thy nbe_program_idx_tab vsp_ty_t deps))));
+ fn (ctxt, nbe_program_idx_tab, vsp_ty_t, deps, ct) =>
+ mk_equals ctxt ct (eval_term ctxt nbe_program_idx_tab vsp_ty_t deps))));
+
+fun oracle ctxt nbe_program_idx_tab vsp_ty_t deps ct =
+ raw_oracle (ctxt, nbe_program_idx_tab, vsp_ty_t, deps, ct);
-fun oracle thy nbe_program_idx_tab vsp_ty_t deps ct =
- raw_oracle (thy, nbe_program_idx_tab, vsp_ty_t, deps, ct);
+fun dynamic_conv ctxt = lift_triv_classes_conv ctxt
+ (Code_Thingol.dynamic_conv ctxt (oracle ctxt o compile false ctxt));
-fun dynamic_conv thy = lift_triv_classes_conv thy
- (Code_Thingol.dynamic_conv thy (oracle thy o compile false thy));
+fun dynamic_value ctxt = lift_triv_classes_rew ctxt
+ (Code_Thingol.dynamic_value ctxt I (eval_term ctxt o compile false ctxt));
-fun dynamic_value thy = lift_triv_classes_rew thy
- (Code_Thingol.dynamic_value thy I (eval_term thy o compile false thy));
+fun static_conv ctxt consts =
+ let
+ val evaluator = Code_Thingol.static_conv ctxt consts
+ (fn program => fn _ => K (oracle ctxt (compile true ctxt program)));
+ in fn ctxt' => lift_triv_classes_conv ctxt' (evaluator ctxt') end;
-fun static_conv thy consts = lift_triv_classes_conv thy
- (Code_Thingol.static_conv thy consts (K o oracle thy o compile true thy));
-
-fun static_value thy consts = lift_triv_classes_rew thy
- (Code_Thingol.static_value thy I consts (K o eval_term thy o compile true thy));
+fun static_value ctxt consts =
+ let
+ val evaluator = Code_Thingol.static_value ctxt I consts
+ (fn program => fn _ => K (eval_term ctxt (compile true ctxt program)));
+ in fn ctxt' => lift_triv_classes_rew ctxt' (evaluator ctxt') end;
(** setup **)
-val setup = Value.add_evaluator ("nbe", dynamic_value o Proof_Context.theory_of);
+val setup = Value.add_evaluator ("nbe", dynamic_value);
end;
-
\ No newline at end of file