--- a/src/HOL/Extraction.thy Tue Nov 17 14:10:31 2009 +0100
+++ b/src/HOL/Extraction.thy Tue Nov 17 15:55:30 2009 +0100
@@ -13,20 +13,6 @@
subsection {* Setup *}
setup {*
-let
-fun realizes_set_proc (Const ("realizes", Type ("fun", [Type ("Null", []), _])) $ r $
- (Const ("op :", _) $ x $ S)) = (case strip_comb S of
- (Var (ixn, U), ts) => SOME (list_comb (Var (ixn, U), ts @ [x]))
- | (Free (s, U), ts) => SOME (list_comb (Free (s, U), ts @ [x]))
- | _ => NONE)
- | realizes_set_proc (Const ("realizes", Type ("fun", [T, _])) $ r $
- (Const ("op :", _) $ x $ S)) = (case strip_comb S of
- (Var (ixn, U), ts) => SOME (list_comb (Var (ixn, T --> U), r :: ts @ [x]))
- | (Free (s, U), ts) => SOME (list_comb (Free (s, T --> U), r :: ts @ [x]))
- | _ => NONE)
- | realizes_set_proc _ = NONE;
-
-in
Extraction.add_types
[("bool", ([], NONE))] #>
Extraction.set_preprocessor (fn thy =>
@@ -35,7 +21,6 @@
Proofterm.rewrite_proof thy
(RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o
ProofRewriteRules.elim_vars (curry Const @{const_name default}))
-end
*}
lemmas [extraction_expand] =
--- a/src/HOL/Nominal/nominal_datatype.ML Tue Nov 17 14:10:31 2009 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Tue Nov 17 15:55:30 2009 +0100
@@ -568,7 +568,7 @@
val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
thy3
|> Sign.map_naming Name_Space.conceal
- |> Inductive.add_inductive_global (serial ())
+ |> Inductive.add_inductive_global
{quiet_mode = false, verbose = false, alt_name = Binding.name big_rep_name,
coind = false, no_elim = true, no_ind = false, skip_mono = true, fork_mono = false}
(map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
@@ -1511,7 +1511,7 @@
val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
thy10
|> Sign.map_naming Name_Space.conceal
- |> Inductive.add_inductive_global (serial ())
+ |> Inductive.add_inductive_global
{quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
(map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
--- a/src/HOL/Nominal/nominal_primrec.ML Tue Nov 17 14:10:31 2009 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Tue Nov 17 15:55:30 2009 +0100
@@ -239,7 +239,7 @@
local
-fun gen_primrec set_group prep_spec prep_term invs fctxt raw_fixes raw_params raw_spec lthy =
+fun gen_primrec prep_spec prep_term invs fctxt raw_fixes raw_params raw_spec lthy =
let
val (fixes', spec) = fst (prep_spec (raw_fixes @ raw_params) raw_spec lthy);
val fixes = List.take (fixes', length raw_fixes);
@@ -280,7 +280,6 @@
else primrec_err ("functions " ^ commas_quote names2 ^
"\nare not mutually recursive");
val (defs_thms, lthy') = lthy |>
- set_group ? Local_Theory.set_group (serial ()) |>
fold_map (apfst (snd o snd) oo Local_Theory.define Thm.definitionK o fst) defs';
val qualify = Binding.qualify false
(space_implode "_" (map (Long_Name.base_name o #1) defs));
@@ -384,8 +383,8 @@
in
-val add_primrec = gen_primrec false Specification.check_spec (K I);
-val add_primrec_cmd = gen_primrec true Specification.read_spec Syntax.read_term;
+val add_primrec = gen_primrec Specification.check_spec (K I);
+val add_primrec_cmd = gen_primrec Specification.read_spec Syntax.read_term;
end;
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Tue Nov 17 14:10:31 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Tue Nov 17 15:55:30 2009 +0100
@@ -155,7 +155,7 @@
val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
thy0
|> Sign.map_naming Name_Space.conceal
- |> Inductive.add_inductive_global (serial ())
+ |> Inductive.add_inductive_global
{quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name',
coind = false, no_elim = false, no_ind = true, skip_mono = true, fork_mono = false}
(map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Tue Nov 17 14:10:31 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Tue Nov 17 15:55:30 2009 +0100
@@ -174,7 +174,7 @@
val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
thy1
|> Sign.map_naming Name_Space.conceal
- |> Inductive.add_inductive_global (serial ())
+ |> Inductive.add_inductive_global
{quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
coind = false, no_elim = true, no_ind = false, skip_mono = true, fork_mono = false}
(map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
--- a/src/HOL/Tools/Function/fun.ML Tue Nov 17 14:10:31 2009 +0100
+++ b/src/HOL/Tools/Function/fun.ML Tue Nov 17 15:55:30 2009 +0100
@@ -151,15 +151,11 @@
domintros=false, partials=false, tailrec=false }
fun gen_fun add config fixes statements int lthy =
- let val group = serial () in
- lthy
- |> Local_Theory.set_group group
- |> add fixes statements config
- |> by_pat_completeness_auto int
- |> Local_Theory.restore
- |> Local_Theory.set_group group
- |> termination_by (Function_Common.get_termination_prover lthy) int
- end;
+ lthy
+ |> add fixes statements config
+ |> by_pat_completeness_auto int
+ |> Local_Theory.restore
+ |> termination_by (Function_Common.get_termination_prover lthy) int
val add_fun = gen_fun Function.add_function
val add_fun_cmd = gen_fun Function.add_function_cmd
--- a/src/HOL/Tools/Function/function.ML Tue Nov 17 14:10:31 2009 +0100
+++ b/src/HOL/Tools/Function/function.ML Tue Nov 17 15:55:30 2009 +0100
@@ -20,8 +20,6 @@
val termination_proof : term option -> local_theory -> Proof.state
val termination_proof_cmd : string option -> local_theory -> Proof.state
- val termination : term option -> local_theory -> Proof.state
- val termination_cmd : string option -> local_theory -> Proof.state
val setup : theory -> theory
val get_congs : Proof.context -> thm list
@@ -119,7 +117,6 @@
end
in
lthy
- |> is_external ? Local_Theory.set_group (serial ())
|> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
|> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
end
@@ -170,18 +167,8 @@
|> Proof.theorem_i NONE afterqed [[(goal, [])]]
end
-val termination_proof = gen_termination_proof Syntax.check_term;
-val termination_proof_cmd = gen_termination_proof Syntax.read_term;
-
-fun termination term_opt lthy =
- lthy
- |> Local_Theory.set_group (serial ())
- |> termination_proof term_opt;
-
-fun termination_cmd term_opt lthy =
- lthy
- |> Local_Theory.set_group (serial ())
- |> termination_proof_cmd term_opt;
+val termination_proof = gen_termination_proof Syntax.check_term
+val termination_proof_cmd = gen_termination_proof Syntax.read_term
(* Datatype hook to declare datatype congs as "function_congs" *)
@@ -217,13 +204,13 @@
val _ =
OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal
(function_parser default_config
- >> (fn ((config, fixes), statements) => add_function_cmd fixes statements config));
+ >> (fn ((config, fixes), statements) => add_function_cmd fixes statements config))
val _ =
OuterSyntax.local_theory_to_proof "termination" "prove termination of a recursive function" K.thy_goal
- (Scan.option P.term >> termination_cmd);
+ (Scan.option P.term >> termination_proof_cmd)
-end;
+end
end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Tue Nov 17 14:10:31 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Tue Nov 17 15:55:30 2009 +0100
@@ -354,7 +354,7 @@
val (ind_result, thy') =
thy
|> Sign.map_naming Name_Space.conceal
- |> Inductive.add_inductive_global (serial ())
+ |> Inductive.add_inductive_global
{quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
(map (fn (s, T) =>
--- a/src/HOL/Tools/inductive.ML Tue Nov 17 14:10:31 2009 +0100
+++ b/src/HOL/Tools/inductive.ML Tue Nov 17 15:55:30 2009 +0100
@@ -51,7 +51,7 @@
(Attrib.binding * string) list ->
(Facts.ref * Attrib.src list) list ->
bool -> local_theory -> inductive_result * local_theory
- val add_inductive_global: serial -> inductive_flags ->
+ val add_inductive_global: inductive_flags ->
((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
thm list -> theory -> inductive_result * theory
val arities_of: thm -> (string * int) list
@@ -886,19 +886,17 @@
coind = coind, no_elim = false, no_ind = false, skip_mono = false, fork_mono = not int};
in
lthy
- |> Local_Theory.set_group (serial ())
|> gen_add_inductive_i mk_def flags cs (map (apfst Binding.name_of o fst) ps) intrs monos
end;
val add_inductive_i = gen_add_inductive_i add_ind_def;
val add_inductive = gen_add_inductive add_ind_def;
-fun add_inductive_global group flags cnames_syn pnames pre_intros monos thy =
+fun add_inductive_global flags cnames_syn pnames pre_intros monos thy =
let
val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
val ctxt' = thy
|> Theory_Target.init NONE
- |> Local_Theory.set_group group
|> add_inductive_i flags cnames_syn pnames pre_intros monos |> snd
|> Local_Theory.exit;
val info = #2 (the_inductive ctxt' name);
--- a/src/HOL/Tools/inductive_realizer.ML Tue Nov 17 14:10:31 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Tue Nov 17 15:55:30 2009 +0100
@@ -350,7 +350,7 @@
(** realizability predicate **)
val (ind_info, thy3') = thy2 |>
- Inductive.add_inductive_global (serial ())
+ Inductive.add_inductive_global
{quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
rlzpreds rlzparams (map (fn (rintr, intr) =>
--- a/src/HOL/Tools/primrec.ML Tue Nov 17 14:10:31 2009 +0100
+++ b/src/HOL/Tools/primrec.ML Tue Nov 17 15:55:30 2009 +0100
@@ -265,7 +265,7 @@
local
-fun gen_primrec set_group prep_spec raw_fixes raw_spec lthy =
+fun gen_primrec prep_spec raw_fixes raw_spec lthy =
let
val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy);
fun attr_bindings prefix = map (fn ((b, attrs), _) =>
@@ -275,7 +275,6 @@
map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]);
in
lthy
- |> set_group ? Local_Theory.set_group (serial ())
|> add_primrec_simple fixes (map snd spec)
|-> (fn (prefix, simps) => fold_map Local_Theory.note (attr_bindings prefix ~~ simps)
#-> (fn simps' => Local_Theory.note (simp_attr_binding prefix, maps snd simps')))
@@ -284,8 +283,8 @@
in
-val add_primrec = gen_primrec false Specification.check_spec;
-val add_primrec_cmd = gen_primrec true Specification.read_spec;
+val add_primrec = gen_primrec Specification.check_spec;
+val add_primrec_cmd = gen_primrec Specification.read_spec;
end;
--- a/src/HOLCF/Tools/fixrec.ML Tue Nov 17 14:10:31 2009 +0100
+++ b/src/HOLCF/Tools/fixrec.ML Tue Nov 17 15:55:30 2009 +0100
@@ -421,7 +421,6 @@
(* code adapted from HOL/Tools/primrec.ML *)
fun gen_fixrec
- (set_group : bool)
prep_spec
(strict : bool)
raw_fixes
@@ -473,8 +472,8 @@
in
-val add_fixrec = gen_fixrec false Specification.check_spec;
-val add_fixrec_cmd = gen_fixrec true Specification.read_spec;
+val add_fixrec = gen_fixrec Specification.check_spec;
+val add_fixrec_cmd = gen_fixrec Specification.read_spec;
end; (* local *)
--- a/src/Pure/General/name_space.ML Tue Nov 17 14:10:31 2009 +0100
+++ b/src/Pure/General/name_space.ML Tue Nov 17 15:55:30 2009 +0100
@@ -34,8 +34,11 @@
type naming
val default_naming: naming
val conceal: naming -> naming
- val set_group: serial -> naming -> naming
+ val get_group: naming -> serial option
+ val set_group: serial option -> naming -> naming
val set_theory_name: string -> naming -> naming
+ val new_group: naming -> naming
+ val reset_group: naming -> naming
val add_path: string -> naming -> naming
val root_path: naming -> naming
val parent_path: naming -> naming
@@ -241,12 +244,18 @@
val conceal = map_naming (fn (_, group, theory_name, path) =>
(true, group, theory_name, path));
-fun set_group group = map_naming (fn (conceal, _, theory_name, path) =>
- (conceal, SOME group, theory_name, path));
-
fun set_theory_name theory_name = map_naming (fn (conceal, group, _, path) =>
(conceal, group, theory_name, path));
+
+fun get_group (Naming {group, ...}) = group;
+
+fun set_group group = map_naming (fn (conceal, _, theory_name, path) =>
+ (conceal, group, theory_name, path));
+
+fun new_group naming = set_group (SOME (serial ())) naming;
+val reset_group = set_group NONE;
+
fun add_path elems = map_path (fn path => path @ [(elems, false)]);
val root_path = map_path (fn _ => []);
val parent_path = map_path (perhaps (try (#1 o split_last)));
--- a/src/Pure/Isar/local_theory.ML Tue Nov 17 14:10:31 2009 +0100
+++ b/src/Pure/Isar/local_theory.ML Tue Nov 17 15:55:30 2009 +0100
@@ -14,7 +14,8 @@
val full_name: local_theory -> binding -> string
val map_naming: (Name_Space.naming -> Name_Space.naming) -> local_theory -> local_theory
val conceal: local_theory -> local_theory
- val set_group: serial -> local_theory -> local_theory
+ val new_group: local_theory -> local_theory
+ val reset_group: local_theory -> local_theory
val restore_naming: local_theory -> local_theory -> local_theory
val target_of: local_theory -> Proof.context
val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
@@ -42,7 +43,7 @@
val term_syntax: bool -> declaration -> local_theory -> local_theory
val declaration: bool -> declaration -> local_theory -> local_theory
val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
- val init: string -> operations -> Proof.context -> local_theory
+ val init: serial option -> string -> operations -> Proof.context -> local_theory
val restore: local_theory -> local_theory
val reinit: local_theory -> local_theory
val exit: local_theory -> Proof.context
@@ -114,7 +115,8 @@
(f naming, theory_prefix, operations, target));
val conceal = map_naming Name_Space.conceal;
-val set_group = map_naming o Name_Space.set_group;
+val new_group = map_naming Name_Space.new_group;
+val reset_group = map_naming Name_Space.reset_group;
val restore_naming = map_naming o K o naming_of;
@@ -203,9 +205,10 @@
(* init *)
-fun init theory_prefix operations target =
+fun init group theory_prefix operations target =
let val naming =
Sign.naming_of (ProofContext.theory_of target)
+ |> Name_Space.set_group group
|> Name_Space.mandatory_path theory_prefix;
in
target |> Data.map
@@ -215,8 +218,8 @@
end;
fun restore lthy =
- let val {theory_prefix, operations, target, ...} = get_lthy lthy
- in init theory_prefix operations target end;
+ let val {naming, theory_prefix, operations, target} = get_lthy lthy
+ in init (Name_Space.get_group naming) theory_prefix operations target end;
val reinit = checkpoint o operation #reinit;
--- a/src/Pure/Isar/theory_target.ML Tue Nov 17 14:10:31 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML Tue Nov 17 15:55:30 2009 +0100
@@ -324,7 +324,7 @@
fun init_lthy (ta as Target {target, instantiation, overloading, ...}) =
Data.put ta #>
- Local_Theory.init (Long_Name.base_name target)
+ Local_Theory.init NONE (Long_Name.base_name target)
{pretty = pretty ta,
abbrev = abbrev ta,
define = define ta,
--- a/src/Pure/Isar/toplevel.ML Tue Nov 17 14:10:31 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML Tue Nov 17 15:55:30 2009 +0100
@@ -302,7 +302,8 @@
local
fun apply_tr int (Init (_, f, exit)) (State (NONE, _)) =
- State (SOME (Theory (Context.Theory (Theory.checkpoint (f int)), NONE), exit), NONE)
+ State (SOME (Theory (Context.Theory
+ (Theory.checkpoint (Runtime.controlled_execution f int)), NONE), exit), NONE)
| apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _), _), _)) =
State (NONE, prev)
| apply_tr _ CommitExit (State (NONE, SOME (Theory (Context.Theory thy, _), exit))) =
@@ -419,7 +420,13 @@
| _ => raise UNDEF));
fun theory' f = transaction (fn int =>
- (fn Theory (Context.Theory thy, _) => Theory (Context.Theory (f int thy), NONE)
+ (fn Theory (Context.Theory thy, _) =>
+ let val thy' = thy
+ |> Sign.new_group
+ |> Theory.checkpoint
+ |> f int
+ |> Sign.reset_group;
+ in Theory (Context.Theory thy', NONE) end
| _ => raise UNDEF));
fun theory f = theory' (K f);
@@ -442,7 +449,10 @@
(fn Theory (gthy, _) =>
let
val finish = loc_finish loc gthy;
- val lthy' = f int (loc_begin loc gthy);
+ val lthy' = loc_begin loc gthy
+ |> Local_Theory.new_group
+ |> f int
+ |> Local_Theory.reset_group;
in Theory (finish lthy', SOME lthy') end
| _ => raise UNDEF));
@@ -491,14 +501,14 @@
in
fun local_theory_to_proof' loc f = begin_proof
- (fn int => fn gthy => f int (loc_begin loc gthy))
- (loc_finish loc);
+ (fn int => fn gthy => f int (Local_Theory.new_group (loc_begin loc gthy)))
+ (fn gthy => loc_finish loc gthy o Local_Theory.reset_group);
fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f);
fun theory_to_proof f = begin_proof
- (K (fn Context.Theory thy => f thy | _ => raise UNDEF))
- (K (Context.Theory o ProofContext.theory_of));
+ (K (fn Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy)) | _ => raise UNDEF))
+ (K (Context.Theory o Sign.reset_group o ProofContext.theory_of));
end;
@@ -531,7 +541,7 @@
fun skip_proof_to_theory pred = transaction (fn _ =>
(fn SkipProof (d, (gthy, _)) => if pred d then Theory (gthy, NONE) else raise UNDEF
- | _ => raise UNDEF));
+ | _ => raise UNDEF));
--- a/src/Pure/sign.ML Tue Nov 17 14:10:31 2009 +0100
+++ b/src/Pure/sign.ML Tue Nov 17 15:55:30 2009 +0100
@@ -121,6 +121,8 @@
val del_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
val add_trrules_i: ast Syntax.trrule list -> theory -> theory
val del_trrules_i: ast Syntax.trrule list -> theory -> theory
+ val new_group: theory -> theory
+ val reset_group: theory -> theory
val add_path: string -> theory -> theory
val root_path: theory -> theory
val parent_path: theory -> theory
@@ -610,6 +612,9 @@
(* naming *)
+val new_group = map_naming Name_Space.new_group;
+val reset_group = map_naming Name_Space.reset_group;
+
val add_path = map_naming o Name_Space.add_path;
val root_path = map_naming Name_Space.root_path;
val parent_path = map_naming Name_Space.parent_path;