# HG changeset patch # User haftmann # Date 1393412272 -3600 # Node ID 9fc71814b8c183afe24d7fcfc5dcddfafe658cf8 # Parent 565a20b22f098e3f3ef6a10574e5fde6a3acc96d prefer proof context over background theory diff -r 565a20b22f09 -r 9fc71814b8c1 NEWS --- 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. diff -r 565a20b22f09 -r 9fc71814b8c1 src/Doc/Codegen/Further.thy --- 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"} \\ diff -r 565a20b22f09 -r 9fc71814b8c1 src/HOL/HOL.thy --- 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" diff -r 565a20b22f09 -r 9fc71814b8c1 src/HOL/Library/Code_Abstract_Nat.thy --- 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)); diff -r 565a20b22f09 -r 9fc71814b8c1 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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; diff -r 565a20b22f09 -r 9fc71814b8c1 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- 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 diff -r 565a20b22f09 -r 9fc71814b8c1 src/HOL/Tools/Quickcheck/exhaustive_generators.ML --- 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 = diff -r 565a20b22f09 -r 9fc71814b8c1 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- 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) => diff -r 565a20b22f09 -r 9fc71814b8c1 src/HOL/Tools/Quickcheck/random_generators.ML --- 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 diff -r 565a20b22f09 -r 9fc71814b8c1 src/HOL/Tools/code_evaluation.ML --- 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; diff -r 565a20b22f09 -r 9fc71814b8c1 src/Tools/Code/code_preproc.ML --- 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*) diff -r 565a20b22f09 -r 9fc71814b8c1 src/Tools/Code/code_runtime.ML --- 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 diff -r 565a20b22f09 -r 9fc71814b8c1 src/Tools/Code/code_simp.ML --- 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; diff -r 565a20b22f09 -r 9fc71814b8c1 src/Tools/Code/code_target.ML --- 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; diff -r 565a20b22f09 -r 9fc71814b8c1 src/Tools/Code/code_thingol.ML --- 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; diff -r 565a20b22f09 -r 9fc71814b8c1 src/Tools/nbe.ML --- 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