--- a/src/HOL/Orderings.thy Mon Jan 04 19:43:59 2010 +0100
+++ b/src/HOL/Orderings.thy Mon Jan 04 19:44:46 2010 +0100
@@ -550,44 +550,6 @@
*}
-subsection {* Name duplicates *}
-
-lemmas order_less_le = less_le
-lemmas order_eq_refl = preorder_class.eq_refl
-lemmas order_less_irrefl = preorder_class.less_irrefl
-lemmas order_le_less = order_class.le_less
-lemmas order_le_imp_less_or_eq = order_class.le_imp_less_or_eq
-lemmas order_less_imp_le = preorder_class.less_imp_le
-lemmas order_less_imp_not_eq = order_class.less_imp_not_eq
-lemmas order_less_imp_not_eq2 = order_class.less_imp_not_eq2
-lemmas order_neq_le_trans = order_class.neq_le_trans
-lemmas order_le_neq_trans = order_class.le_neq_trans
-
-lemmas order_antisym = antisym
-lemmas order_less_not_sym = preorder_class.less_not_sym
-lemmas order_less_asym = preorder_class.less_asym
-lemmas order_eq_iff = order_class.eq_iff
-lemmas order_antisym_conv = order_class.antisym_conv
-lemmas order_less_trans = preorder_class.less_trans
-lemmas order_le_less_trans = preorder_class.le_less_trans
-lemmas order_less_le_trans = preorder_class.less_le_trans
-lemmas order_less_imp_not_less = preorder_class.less_imp_not_less
-lemmas order_less_imp_triv = preorder_class.less_imp_triv
-lemmas order_less_asym' = preorder_class.less_asym'
-
-lemmas linorder_linear = linear
-lemmas linorder_less_linear = linorder_class.less_linear
-lemmas linorder_le_less_linear = linorder_class.le_less_linear
-lemmas linorder_le_cases = linorder_class.le_cases
-lemmas linorder_not_less = linorder_class.not_less
-lemmas linorder_not_le = linorder_class.not_le
-lemmas linorder_neq_iff = linorder_class.neq_iff
-lemmas linorder_neqE = linorder_class.neqE
-lemmas linorder_antisym_conv1 = linorder_class.antisym_conv1
-lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
-lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
-
-
subsection {* Bounded quantifiers *}
syntax
@@ -698,7 +660,7 @@
assume r: "!!x y. x < y ==> f x < f y"
assume "a < b" hence "f a < f b" by (rule r)
also assume "f b < c"
- finally (order_less_trans) show ?thesis .
+ finally (less_trans) show ?thesis .
qed
lemma order_less_subst1: "(a::'a::order) < f b ==> (b::'b::order) < c ==>
@@ -707,7 +669,7 @@
assume r: "!!x y. x < y ==> f x < f y"
assume "a < f b"
also assume "b < c" hence "f b < f c" by (rule r)
- finally (order_less_trans) show ?thesis .
+ finally (less_trans) show ?thesis .
qed
lemma order_le_less_subst2: "(a::'a::order) <= b ==> f b < (c::'c::order) ==>
@@ -716,7 +678,7 @@
assume r: "!!x y. x <= y ==> f x <= f y"
assume "a <= b" hence "f a <= f b" by (rule r)
also assume "f b < c"
- finally (order_le_less_trans) show ?thesis .
+ finally (le_less_trans) show ?thesis .
qed
lemma order_le_less_subst1: "(a::'a::order) <= f b ==> (b::'b::order) < c ==>
@@ -725,7 +687,7 @@
assume r: "!!x y. x < y ==> f x < f y"
assume "a <= f b"
also assume "b < c" hence "f b < f c" by (rule r)
- finally (order_le_less_trans) show ?thesis .
+ finally (le_less_trans) show ?thesis .
qed
lemma order_less_le_subst2: "(a::'a::order) < b ==> f b <= (c::'c::order) ==>
@@ -734,7 +696,7 @@
assume r: "!!x y. x < y ==> f x < f y"
assume "a < b" hence "f a < f b" by (rule r)
also assume "f b <= c"
- finally (order_less_le_trans) show ?thesis .
+ finally (less_le_trans) show ?thesis .
qed
lemma order_less_le_subst1: "(a::'a::order) < f b ==> (b::'b::order) <= c ==>
@@ -743,7 +705,7 @@
assume r: "!!x y. x <= y ==> f x <= f y"
assume "a < f b"
also assume "b <= c" hence "f b <= f c" by (rule r)
- finally (order_less_le_trans) show ?thesis .
+ finally (less_le_trans) show ?thesis .
qed
lemma order_subst1: "(a::'a::order) <= f b ==> (b::'b::order) <= c ==>
@@ -876,8 +838,6 @@
ord_eq_less_trans
trans
-(* FIXME cleanup *)
-
text {* These support proving chains of decreasing inequalities
a >= b >= c ... in Isar proofs. *}
@@ -1070,12 +1030,12 @@
lemma min_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> min x least = least"
apply (simp add: min_def)
-apply (blast intro: order_antisym)
+apply (blast intro: antisym)
done
lemma max_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> max x least = x"
apply (simp add: max_def)
-apply (blast intro: order_antisym)
+apply (blast intro: antisym)
done
@@ -1107,7 +1067,7 @@
lemma wellorder_Least_lemma:
fixes k :: 'a
assumes "P k"
- shows "P (LEAST x. P x)" and "(LEAST x. P x) \<le> k"
+ shows LeastI: "P (LEAST x. P x)" and Least_le: "(LEAST x. P x) \<le> k"
proof -
have "P (LEAST x. P x) \<and> (LEAST x. P x) \<le> k"
using assms proof (induct k rule: less_induct)
@@ -1132,9 +1092,6 @@
then show "P (LEAST x. P x)" and "(LEAST x. P x) \<le> k" by auto
qed
-lemmas LeastI = wellorder_Least_lemma(1)
-lemmas Least_le = wellorder_Least_lemma(2)
-
-- "The following 3 lemmas are due to Brian Huffman"
lemma LeastI_ex: "\<exists>x. P x \<Longrightarrow> P (Least P)"
by (erule exE) (erule LeastI)
@@ -1174,7 +1131,7 @@
bot_bool_eq: "bot = False"
instance proof
-qed (auto simp add: le_bool_def less_bool_def top_bool_eq bot_bool_eq)
+qed (auto simp add: bot_bool_eq top_bool_eq less_bool_def, auto simp add: le_bool_def)
end
@@ -1221,10 +1178,10 @@
instance "fun" :: (type, preorder) preorder proof
qed (auto simp add: le_fun_def less_fun_def
- intro: order_trans order_antisym intro!: ext)
+ intro: order_trans antisym intro!: ext)
instance "fun" :: (type, order) order proof
-qed (auto simp add: le_fun_def intro: order_antisym ext)
+qed (auto simp add: le_fun_def intro: antisym ext)
instantiation "fun" :: (type, top) top
begin
@@ -1257,4 +1214,42 @@
lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x"
unfolding le_fun_def by simp
+
+subsection {* Name duplicates *}
+
+lemmas order_eq_refl = preorder_class.eq_refl
+lemmas order_less_irrefl = preorder_class.less_irrefl
+lemmas order_less_imp_le = preorder_class.less_imp_le
+lemmas order_less_not_sym = preorder_class.less_not_sym
+lemmas order_less_asym = preorder_class.less_asym
+lemmas order_less_trans = preorder_class.less_trans
+lemmas order_le_less_trans = preorder_class.le_less_trans
+lemmas order_less_le_trans = preorder_class.less_le_trans
+lemmas order_less_imp_not_less = preorder_class.less_imp_not_less
+lemmas order_less_imp_triv = preorder_class.less_imp_triv
+lemmas order_less_asym' = preorder_class.less_asym'
+
+lemmas order_less_le = order_class.less_le
+lemmas order_le_less = order_class.le_less
+lemmas order_le_imp_less_or_eq = order_class.le_imp_less_or_eq
+lemmas order_less_imp_not_eq = order_class.less_imp_not_eq
+lemmas order_less_imp_not_eq2 = order_class.less_imp_not_eq2
+lemmas order_neq_le_trans = order_class.neq_le_trans
+lemmas order_le_neq_trans = order_class.le_neq_trans
+lemmas order_antisym = order_class.antisym
+lemmas order_eq_iff = order_class.eq_iff
+lemmas order_antisym_conv = order_class.antisym_conv
+
+lemmas linorder_linear = linorder_class.linear
+lemmas linorder_less_linear = linorder_class.less_linear
+lemmas linorder_le_less_linear = linorder_class.le_less_linear
+lemmas linorder_le_cases = linorder_class.le_cases
+lemmas linorder_not_less = linorder_class.not_less
+lemmas linorder_not_le = linorder_class.not_le
+lemmas linorder_neq_iff = linorder_class.neq_iff
+lemmas linorder_neqE = linorder_class.neqE
+lemmas linorder_antisym_conv1 = linorder_class.antisym_conv1
+lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
+lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
+
end
--- a/src/Pure/Isar/code.ML Mon Jan 04 19:43:59 2010 +0100
+++ b/src/Pure/Isar/code.ML Mon Jan 04 19:44:46 2010 +0100
@@ -234,53 +234,35 @@
local
type data = Object.T Datatab.table;
-fun create_data data = Synchronized.var "code data" data;
-fun empty_data () = create_data Datatab.empty : data Synchronized.var;
+fun empty_dataref () = Synchronized.var "code data" (NONE : (data * theory_ref) option);
-structure Code_Data = TheoryDataFun
+structure Code_Data = Theory_Data
(
- type T = spec * data Synchronized.var;
+ type T = spec * (data * theory_ref) option Synchronized.var;
val empty = (make_spec (false, (((Symtab.empty, Symtab.empty), Symtab.empty),
- (Symtab.empty, (Symtab.empty, Symtab.empty)))), empty_data ());
- fun copy (spec, data) = (spec, create_data (Synchronized.value data));
- val extend = copy;
- fun merge _ ((spec1, _), (spec2, _)) =
- (merge_spec (spec1, spec2), empty_data ());
+ (Symtab.empty, (Symtab.empty, Symtab.empty)))), empty_dataref ());
+ val extend = I
+ fun merge ((spec1, _), (spec2, _)) =
+ (merge_spec (spec1, spec2), empty_dataref ());
);
-fun thy_data f thy = f ((snd o Code_Data.get) thy);
-
-fun get_ensure_init kind data =
- case Datatab.lookup (Synchronized.value data) kind
- of SOME x => x
- | NONE => let val y = invoke_init kind
- in (Synchronized.change data (Datatab.update (kind, y)); y) end;
-
in
(* access to executable code *)
val the_exec = fst o Code_Data.get;
-fun map_exec_purge f =
- Code_Data.map (fn (exec, data) => (f exec, empty_data ()));
+fun map_exec_purge f = Code_Data.map (fn (exec, _) => (f exec, empty_dataref ()));
-val purge_data = (Code_Data.map o apsnd) (fn _ => empty_data ());
+val purge_data = (Code_Data.map o apsnd) (fn _ => empty_dataref ());
fun change_eqns delete c f = (map_exec_purge o map_eqns
o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, [])), [])))
o apfst) (fn (_, eqns) => (true, f eqns));
-fun del_eqns c = change_eqns true c (K (false, []));
-
(* tackling equation history *)
-fun get_eqns thy c =
- Symtab.lookup ((the_eqns o the_exec) thy) c
- |> Option.map (snd o snd o fst)
- |> these;
-
fun continue_history thy = if (history_concluded o the_exec) thy
then thy
|> (Code_Data.map o apfst o map_history_concluded) (K false)
@@ -297,30 +279,28 @@
#> map_history_concluded (K true))
|> SOME;
-val _ = Context.>> (Context.map_theory (Code_Data.init
- #> Theory.at_begin continue_history
- #> Theory.at_end conclude_history));
+val _ = Context.>> (Context.map_theory (Theory.at_begin continue_history #> Theory.at_end conclude_history));
(* access to data dependent on abstract executable code *)
-fun change_data (kind, mk, dest) =
+fun change_yield_data (kind, mk, dest) theory f =
let
- fun chnge data_ref f =
- let
- val data = get_ensure_init kind data_ref;
- val data' = f (dest data);
- in (Synchronized.change data_ref (Datatab.update (kind, mk data')); data') end;
- in thy_data chnge end;
+ val dataref = (snd o Code_Data.get) theory;
+ val (datatab, thy_ref) = case Synchronized.value dataref
+ of SOME (datatab, thy_ref) => if Theory.eq_thy (theory, Theory.deref thy_ref)
+ then (datatab, thy_ref)
+ else (Datatab.empty, Theory.check_thy theory)
+ | NONE => (Datatab.empty, Theory.check_thy theory)
+ val data = case Datatab.lookup datatab kind
+ of SOME data => data
+ | NONE => invoke_init kind;
+ val result as (x, data') = f (dest data);
+ val _ = Synchronized.change dataref
+ ((K o SOME) (Datatab.update (kind, mk data') datatab, thy_ref));
+ in result end;
-fun change_yield_data (kind, mk, dest) =
- let
- fun chnge data_ref f =
- let
- val data = get_ensure_init kind data_ref;
- val (x, data') = f (dest data);
- in (x, (Synchronized.change data_ref (Datatab.update (kind, mk data')); data')) end;
- in thy_data chnge end;
+fun change_data ops theory f = change_yield_data ops theory (f #> pair ()) |> snd;
end; (*local*)
@@ -574,7 +554,9 @@
in map2 (fn vs => Thm.certify_instantiate (vs ~~ vts, [])) vss thms end;
fun these_eqns thy c =
- get_eqns thy c
+ Symtab.lookup ((the_eqns o the_exec) thy) c
+ |> Option.map (snd o snd o fst)
+ |> these
|> (map o apfst) (Thm.transfer thy)
|> burrow_fst (standard_typscheme thy);
@@ -709,38 +691,6 @@
val add_signature_cmd = gen_add_signature read_const read_signature;
-(* datatypes *)
-
-structure Type_Interpretation =
- Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
-
-fun add_datatype raw_cs thy =
- let
- val cs = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) raw_cs;
- val (tyco, vs_cos) = constrset_of_consts thy cs;
- val old_cs = (map fst o snd o get_datatype thy) tyco;
- fun drop_outdated_cases cases = fold Symtab.delete_safe
- (Symtab.fold (fn (c, (_, (_, cos))) =>
- if exists (member (op =) old_cs) cos
- then insert (op =) c else I) cases []) cases;
- in
- thy
- |> fold (del_eqns o fst) cs
- |> map_exec_purge
- ((map_dtyps o Symtab.map_default (tyco, [])) (cons (serial (), vs_cos))
- #> (map_cases o apfst) drop_outdated_cases)
- |> Type_Interpretation.data (tyco, serial ())
- end;
-
-fun type_interpretation f = Type_Interpretation.interpretation
- (fn (tyco, _) => fn thy => f (tyco, get_datatype thy tyco) thy);
-
-fun add_datatype_cmd raw_cs thy =
- let
- val cs = map (read_bare_const thy) raw_cs;
- in add_datatype cs thy end;
-
-
(* code equations *)
fun gen_add_eqn default (thm, proper) thy =
@@ -773,6 +723,56 @@
of SOME (thm, _) => change_eqns true (const_eqn thy thm) (del_thm thm) thy
| NONE => thy;
+fun del_eqns c = change_eqns true c (K (false, []));
+
+
+(* cases *)
+
+fun add_case thm thy =
+ let
+ val (c, (k, case_pats)) = case_cert thm;
+ val _ = case filter_out (is_constr thy) case_pats
+ of [] => ()
+ | cs => error ("Non-constructor(s) in case certificate: " ^ commas (map quote cs));
+ val entry = (1 + Int.max (1, length case_pats), (k, case_pats))
+ in (map_exec_purge o map_cases o apfst) (Symtab.update (c, entry)) thy end;
+
+fun add_undefined c thy =
+ (map_exec_purge o map_cases o apsnd) (Symtab.update (c, ())) thy;
+
+
+(* datatypes *)
+
+structure Type_Interpretation =
+ Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
+
+fun add_datatype raw_cs thy =
+ let
+ val cs = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) raw_cs;
+ val (tyco, vs_cos) = constrset_of_consts thy cs;
+ val old_cs = (map fst o snd o get_datatype thy) tyco;
+ fun drop_outdated_cases cases = fold Symtab.delete_safe
+ (Symtab.fold (fn (c, (_, (_, cos))) =>
+ if exists (member (op =) old_cs) cos
+ then insert (op =) c else I) cases []) cases;
+ in
+ thy
+ |> fold (del_eqns o fst) cs
+ |> map_exec_purge
+ ((map_dtyps o Symtab.map_default (tyco, [])) (cons (serial (), vs_cos))
+ #> (map_cases o apfst) drop_outdated_cases)
+ |> Type_Interpretation.data (tyco, serial ())
+ end;
+
+fun type_interpretation f = Type_Interpretation.interpretation
+ (fn (tyco, _) => fn thy => f (tyco, get_datatype thy tyco) thy);
+
+fun add_datatype_cmd raw_cs thy =
+ let
+ val cs = map (read_bare_const thy) raw_cs;
+ in add_datatype cs thy end;
+
+
(* c.f. src/HOL/Tools/recfun_codegen.ML *)
structure Code_Target_Attr = Theory_Data
@@ -789,7 +789,6 @@
let
val attr = the_default ((K o K) I) (Code_Target_Attr.get thy);
in thy |> add_warning_eqn thm |> attr prefix thm end;
-
(* setup *)
val _ = Context.>> (Context.map_theory
@@ -807,21 +806,6 @@
"declare theorems for code generation"
end));
-
-(* cases *)
-
-fun add_case thm thy =
- let
- val (c, (k, case_pats)) = case_cert thm;
- val _ = case filter_out (is_constr thy) case_pats
- of [] => ()
- | cs => error ("Non-constructor(s) in case certificate: " ^ commas (map quote cs));
- val entry = (1 + Int.max (1, length case_pats), (k, case_pats))
- in (map_exec_purge o map_cases o apfst) (Symtab.update (c, entry)) thy end;
-
-fun add_undefined c thy =
- (map_exec_purge o map_cases o apsnd) (Symtab.update (c, ())) thy;
-
end; (*struct*)
--- a/src/Pure/axclass.ML Mon Jan 04 19:43:59 2010 +0100
+++ b/src/Pure/axclass.ML Mon Jan 04 19:44:46 2010 +0100
@@ -118,7 +118,6 @@
(
type T = axclasses * (instances * inst_params);
val empty = ((Symtab.empty, []), (([], Symtab.empty), (Symtab.empty, Symtab.empty)));
- val copy = I;
val extend = I;
fun merge pp ((axclasses1, (instances1, inst_params1)), (axclasses2, (instances2, inst_params2))) =
(merge_axclasses pp (axclasses1, axclasses2),
--- a/src/Pure/context.ML Mon Jan 04 19:43:59 2010 +0100
+++ b/src/Pure/context.ML Mon Jan 04 19:44:46 2010 +0100
@@ -83,7 +83,7 @@
include CONTEXT
structure Theory_Data:
sig
- val declare: Object.T -> (Object.T -> Object.T) -> (Object.T -> Object.T) ->
+ val declare: Object.T -> (Object.T -> Object.T) ->
(Pretty.pp -> Object.T * Object.T -> Object.T) -> serial
val get: serial -> (Object.T -> 'a) -> theory -> 'a
val put: serial -> ('a -> Object.T) -> 'a -> theory -> theory
@@ -112,7 +112,6 @@
type kind =
{empty: Object.T,
- copy: Object.T -> Object.T,
extend: Object.T -> Object.T,
merge: Pretty.pp -> Object.T * Object.T -> Object.T};
@@ -126,18 +125,16 @@
in
fun invoke_empty k = invoke (K o #empty) k ();
-val invoke_copy = invoke #copy;
val invoke_extend = invoke #extend;
fun invoke_merge pp = invoke (fn kind => #merge kind pp);
-fun declare_theory_data empty copy extend merge =
+fun declare_theory_data empty extend merge =
let
val k = serial ();
- val kind = {empty = empty, copy = copy, extend = extend, merge = merge};
+ val kind = {empty = empty, extend = extend, merge = merge};
val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind)));
in k end;
-val copy_data = Datatab.map' invoke_copy;
val extend_data = Datatab.map' invoke_extend;
fun merge_data pp (data1, data2) =
@@ -341,7 +338,7 @@
val (self', data', ancestry') =
if draft then (self, data, ancestry) (*destructive change!*)
else if #stage history > 0
- then (NONE, copy_data data, ancestry)
+ then (NONE, data, ancestry)
else (NONE, extend_data data, make_ancestry [thy] (extend_ancestors_of thy));
val ids' = insert_id draft id ids;
val data'' = f data';
@@ -357,9 +354,8 @@
let
val Theory ({draft, id, ids, ...}, data, ancestry, history) = thy;
val ids' = insert_id draft id ids;
- val data' = copy_data data;
val thy' = SYNCHRONIZED (fn () =>
- (check_thy thy; create_thy NONE true ids' data' ancestry history));
+ (check_thy thy; create_thy NONE true ids' data ancestry history));
in thy' end;
val pre_pure_thy = create_thy NONE true Inttab.empty
@@ -430,9 +426,9 @@
val declare = declare_theory_data;
fun get k dest thy =
- dest ((case Datatab.lookup (data_of thy) k of
+ dest (case Datatab.lookup (data_of thy) k of
SOME x => x
- | NONE => invoke_copy k (invoke_empty k))); (*adhoc value*)
+ | NONE => invoke_empty k); (*adhoc value*)
fun put k mk x = modify_thy (Datatab.update (k, mk x));
@@ -582,7 +578,6 @@
sig
type T
val empty: T
- val copy: T -> T
val extend: T -> T
val merge: Pretty.pp -> T * T -> T
end;
@@ -604,7 +599,6 @@
val kind = Context.Theory_Data.declare
(Data Data.empty)
- (fn Data x => Data (Data.copy x))
(fn Data x => Data (Data.extend x))
(fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)));
@@ -639,7 +633,6 @@
(
type T = Data.T;
val empty = Data.empty;
- val copy = I;
val extend = Data.extend;
fun merge _ = Data.merge;
);
--- a/src/Pure/sign.ML Mon Jan 04 19:43:59 2010 +0100
+++ b/src/Pure/sign.ML Mon Jan 04 19:44:46 2010 +0100
@@ -151,7 +151,6 @@
structure SignData = TheoryDataFun
(
type T = sign;
- val copy = I;
fun extend (Sign {syn, tsig, consts, ...}) =
make_sign (Name_Space.default_naming, syn, tsig, consts);
--- a/src/Pure/theory.ML Mon Jan 04 19:43:59 2010 +0100
+++ b/src/Pure/theory.ML Mon Jan 04 19:44:46 2010 +0100
@@ -91,7 +91,6 @@
type T = thy;
val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;
val empty = make_thy (empty_axioms, Defs.empty, ([], []));
- val copy = I;
fun extend (Thy {axioms = _, defs, wrappers}) = make_thy (empty_axioms, defs, wrappers);
--- a/src/Tools/Code/code_ml.ML Mon Jan 04 19:43:59 2010 +0100
+++ b/src/Tools/Code/code_ml.ML Mon Jan 04 19:44:46 2010 +0100
@@ -481,8 +481,6 @@
let
val consts = fold Code_Thingol.add_constnames (t :: ts) [];
val vars = reserved
- |> intro_base_names
- (is_none o syntax_const) deresolve consts
|> intro_vars ((fold o Code_Thingol.fold_varnames)
(insert (op =)) ts []);
in concat [
--- a/src/Tools/Code/code_preproc.ML Mon Jan 04 19:43:59 2010 +0100
+++ b/src/Tools/Code/code_preproc.ML Mon Jan 04 19:44:46 2010 +0100
@@ -282,7 +282,7 @@
of SOME classess => (classess, ([], []))
| NONE => let
val all_classes = complete_proper_sort thy [class];
- val superclasses = remove (op =) class all_classes
+ val superclasses = remove (op =) class all_classes;
val classess = map (complete_proper_sort thy)
(Sign.arity_sorts thy tyco [class]);
val inst_params = inst_params thy tyco all_classes;
--- a/src/Tools/Code/code_printer.ML Mon Jan 04 19:43:59 2010 +0100
+++ b/src/Tools/Code/code_printer.ML Mon Jan 04 19:44:46 2010 +0100
@@ -60,6 +60,7 @@
val brackify: fixity -> Pretty.T list -> Pretty.T
val brackify_infix: int * lrx -> fixity -> Pretty.T list -> Pretty.T
val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
+ val applify: string -> string -> fixity -> Pretty.T -> Pretty.T list -> Pretty.T
type tyco_syntax
type simple_const_syntax
@@ -220,6 +221,11 @@
else p
end;
+fun applify opn cls fxy_ctxt p [] = p
+ | applify opn cls fxy_ctxt p ps =
+ (if (fixity BR fxy_ctxt) then enclose "(" ")" else Pretty.block)
+ (p @@ enum "," opn cls ps);
+
(* generic syntax *)
--- a/src/Tools/Code/code_target.ML Mon Jan 04 19:43:59 2010 +0100
+++ b/src/Tools/Code/code_target.ML Mon Jan 04 19:44:46 2010 +0100
@@ -153,7 +153,7 @@
fun the_name_syntax (Target { name_syntax_table = NameSyntaxTable x, ... }) = x;
fun the_module_alias (Target { module_alias , ... }) = module_alias;
-structure CodeTargetData = Theory_Data
+structure Targets = Theory_Data
(
type T = (target Symtab.table * string list) * int;
val empty = ((Symtab.empty, []), 80);
@@ -163,17 +163,17 @@
Library.merge (op =) (exc1, exc2)), Int.max (width1, width2));
);
-val abort_allowed = snd o fst o CodeTargetData.get;
+val abort_allowed = snd o fst o Targets.get;
-val the_default_width = snd o CodeTargetData.get;
+val the_default_width = snd o Targets.get;
-fun assert_target thy target = if Symtab.defined ((fst o fst) (CodeTargetData.get thy)) target
+fun assert_target thy target = if Symtab.defined ((fst o fst) (Targets.get thy)) target
then target
else error ("Unknown code target language: " ^ quote target);
fun put_target (target, seri) thy =
let
- val lookup_target = Symtab.lookup ((fst o fst) (CodeTargetData.get thy));
+ val lookup_target = Symtab.lookup ((fst o fst) (Targets.get thy));
val _ = case seri
of Extends (super, _) => if is_some (lookup_target super) then ()
else error ("Unknown code target language: " ^ quote super)
@@ -189,11 +189,10 @@
else ();
in
thy
- |> (CodeTargetData.map o apfst o apfst oo Symtab.map_default)
+ |> (Targets.map o apfst o apfst o Symtab.update)
(target, make_target ((serial (), seri), (([], Symtab.empty),
(mk_name_syntax_table ((Symtab.empty, Symreltab.empty), (Symtab.empty, Symtab.empty)),
Symtab.empty))))
- ((map_target o apfst o apsnd o K) seri)
end;
fun add_target (target, seri) = put_target (target, Serializer seri);
@@ -205,7 +204,7 @@
val _ = assert_target thy target;
in
thy
- |> (CodeTargetData.map o apfst o apfst o Symtab.map_entry target o map_target) f
+ |> (Targets.map o apfst o apfst o Symtab.map_entry target o map_target) f
end;
fun map_reserved target =
@@ -217,7 +216,7 @@
fun map_module_alias target =
map_target_data target o apsnd o apsnd o apsnd;
-fun set_default_code_width k = (CodeTargetData.map o apsnd) (K k);
+fun set_default_code_width k = (Targets.map o apsnd) (K k);
(** serializer usage **)
@@ -226,7 +225,7 @@
fun the_literals thy =
let
- val ((targets, _), _) = CodeTargetData.get thy;
+ val ((targets, _), _) = Targets.get thy;
fun literals target = case Symtab.lookup targets target
of SOME data => (case the_serializer data
of Serializer (_, literals) => literals
@@ -284,7 +283,7 @@
fun mount_serializer thy alt_serializer target some_width module args naming program names =
let
- val ((targets, abortable), default_width) = CodeTargetData.get thy;
+ val ((targets, abortable), default_width) = Targets.get thy;
fun collapse_hierarchy target =
let
val data = case Symtab.lookup targets target
@@ -457,7 +456,7 @@
fun gen_allow_abort prep_const raw_c thy =
let
val c = prep_const thy raw_c;
- in thy |> (CodeTargetData.map o apfst o apsnd) (insert (op =) c) end;
+ in thy |> (Targets.map o apfst o apsnd) (insert (op =) c) end;
(* concrete syntax *)