--- a/src/Pure/Isar/theory_target.ML Mon Aug 09 09:57:38 2010 +0200
+++ b/src/Pure/Isar/theory_target.ML Mon Aug 09 09:57:50 2010 +0200
@@ -274,44 +274,9 @@
fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
-fun declare_const (ta as Target {target, is_locale, is_class, ...})
- extra_tfrees xs ((b, T), mx) lthy =
- let
- val type_params = map (Logic.mk_type o TFree) extra_tfrees;
- val term_params =
- rev (Variable.fixes_of (Local_Theory.target_of lthy))
- |> map_filter (fn (_, x) =>
- (case AList.lookup (op =) xs x of
- SOME T => SOME (Free (x, T))
- | NONE => NONE));
- val params = type_params @ term_params;
-
- val U = map Term.fastype_of params ---> T;
- val (mx1, mx2, mx3) = prep_mixfix lthy ta (b, extra_tfrees) mx;
- val (const, lthy') = lthy |>
- (case Class_Target.instantiation_param lthy b of
- SOME c' =>
- if mx3 <> NoSyn then syntax_error c'
- else Local_Theory.theory_result (AxClass.declare_overloaded (c', U))
- ##> Class_Target.confirm_declaration b
- | NONE =>
- (case Overloading.operation lthy b of
- SOME (c', _) =>
- if mx3 <> NoSyn then syntax_error c'
- else Local_Theory.theory_result (Overloading.declare (c', U))
- ##> Overloading.confirm b
- | NONE => Local_Theory.theory_result (Sign.declare_const ((b, U), mx3))));
- val t = Term.list_comb (const, params);
- in
- lthy'
- |> is_locale ? syntax_declaration ta false (locale_const ta Syntax.mode_default ((b, mx2), t))
- |> is_class ? class_target ta (Class_Target.declare target ((b, mx1), (type_params, t)))
- |> Local_Defs.add_def ((b, NoSyn), t)
- end;
-
in
-fun define ta ((b, mx), ((name, atts), rhs)) lthy =
+fun define (ta as Target {target, is_locale, is_class, ...}) ((b, mx), ((name, atts), rhs)) lthy =
let
val thy = ProofContext.theory_of lthy;
val thy_ctxt = ProofContext.init_global thy;
@@ -328,12 +293,42 @@
val extra_tfrees = rev (subtract (op =) tfreesT (Term.add_tfrees rhs []));
(*const*)
- val ((lhs, local_def), lthy2) = lthy |> declare_const ta extra_tfrees xs ((b, T), mx);
+ val type_params = map (Logic.mk_type o TFree) extra_tfrees;
+ val term_params =
+ rev (Variable.fixes_of (Local_Theory.target_of lthy))
+ |> map_filter (fn (_, x) =>
+ (case AList.lookup (op =) xs x of
+ SOME T => SOME (Free (x, T))
+ | NONE => NONE));
+ val params = type_params @ term_params;
+
+ val U = map Term.fastype_of params ---> T;
+ val (mx1, mx2, mx3) = prep_mixfix lthy ta (b, extra_tfrees) mx;
+
+ val (const, lthy2) = lthy |>
+ (case Class_Target.instantiation_param lthy b of
+ SOME c' =>
+ if mx3 <> NoSyn then syntax_error c'
+ else Local_Theory.theory_result (AxClass.declare_overloaded (c', U))
+ ##> Class_Target.confirm_declaration b
+ | NONE =>
+ (case Overloading.operation lthy b of
+ SOME (c', _) =>
+ if mx3 <> NoSyn then syntax_error c'
+ else Local_Theory.theory_result (Overloading.declare (c', U))
+ ##> Overloading.confirm b
+ | NONE => Local_Theory.theory_result (Sign.declare_const ((b, U), mx3))));
+ val t = Term.list_comb (const, params);
+
+ val ((lhs, local_def), lthy3) = lthy2
+ |> is_locale ? syntax_declaration ta false (locale_const ta Syntax.mode_default ((b, mx2), t))
+ |> is_class ? class_target ta (Class_Target.declare target ((b, mx1), (type_params, t)))
+ |> Local_Defs.add_def ((b, NoSyn), t);
val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def);
val Const (head, _) = Term.head_of lhs';
(*def*)
- val (global_def, lthy3) = lthy2
+ val (global_def, lthy4) = lthy3
|> Local_Theory.theory_result
(case Overloading.operation lthy b of
SOME (_, checked) => Overloading.define checked name' (head, rhs')
@@ -341,15 +336,15 @@
if is_some (Class_Target.instantiation_param lthy b)
then AxClass.define_overloaded name' (head, rhs')
else Thm.add_def false false (name', Logic.mk_equals (lhs', rhs')) #>> snd);
- val def = Local_Defs.trans_terms lthy3
+ val def = Local_Defs.trans_terms lthy4
[(*c == global.c xs*) local_def,
(*global.c xs == rhs'*) global_def,
(*rhs' == rhs*) Thm.symmetric rhs_conv];
(*note*)
- val ([(res_name, [res])], lthy4) = lthy3
+ val ([(res_name, [res])], lthy5) = lthy4
|> notes ta "" [((name', atts), [([def], [])])];
- in ((lhs, (res_name, res)), lthy4) end;
+ in ((lhs, (res_name, res)), lthy5) end;
end;
@@ -358,50 +353,51 @@
local
-fun init_target _ NONE = global_target
- | init_target thy (SOME target) =
- if Locale.defined thy target
- then make_target target true (Class_Target.is_class thy target) ([], [], []) []
- else error ("No such locale: " ^ quote target);
-
-fun init_ctxt (Target {target, is_locale, is_class, instantiation, overloading}) =
+fun init_data (Target {target, is_locale, is_class, instantiation, overloading}) =
if not (null (#1 instantiation)) then Class_Target.init_instantiation instantiation
else if not (null overloading) then Overloading.init overloading
else if not is_locale then ProofContext.init_global
else if not is_class then Locale.init target
else Class_Target.init target;
-fun init_lthy (ta as Target {target, instantiation, overloading, ...}) =
- Data.put ta #>
- Local_Theory.init NONE (Long_Name.base_name target)
- {pretty = pretty ta,
- abbrev = abbrev ta,
- define = define ta,
- notes = notes ta,
- declaration = declaration ta,
- syntax_declaration = syntax_declaration ta,
- reinit = fn lthy => init_lthy_ctxt ta (ProofContext.theory_of lthy),
- exit = Local_Theory.target_of o
- (if not (null (#1 instantiation)) then Class_Target.conclude_instantiation
- else if not (null overloading) then Overloading.conclude
- else I)}
-and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta;
+fun init_target (ta as Target {target, instantiation, overloading, ...}) thy =
+ thy
+ |> init_data ta
+ |> Data.put ta
+ |> Local_Theory.init NONE (Long_Name.base_name target)
+ {pretty = pretty ta,
+ abbrev = abbrev ta,
+ define = define ta,
+ notes = notes ta,
+ declaration = declaration ta,
+ syntax_declaration = syntax_declaration ta,
+ reinit = init_target ta o ProofContext.theory_of,
+ exit = Local_Theory.target_of o
+ (if not (null (#1 instantiation)) then Class_Target.conclude_instantiation
+ else if not (null overloading) then Overloading.conclude
+ else I)};
+
+fun named_target _ NONE = global_target
+ | named_target thy (SOME target) =
+ if Locale.defined thy target
+ then make_target target true (Class_Target.is_class thy target) ([], [], []) []
+ else error ("No such locale: " ^ quote target);
fun gen_overloading prep_const raw_ops thy =
let
val ctxt = ProofContext.init_global thy;
val ops = raw_ops |> map (fn (name, const, checked) =>
(name, Term.dest_Const (prep_const ctxt const), checked));
- in thy |> init_lthy_ctxt (make_target "" false false ([], [], []) ops) end;
+ in thy |> init_target (make_target "" false false ([], [], []) ops) end;
in
-fun init target thy = init_lthy_ctxt (init_target thy target) thy;
+fun init target thy = init_target (named_target thy target) thy;
fun context_cmd "-" thy = init NONE thy
| context_cmd target thy = init (SOME (Locale.intern thy target)) thy;
-fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []);
+fun instantiation arities = init_target (make_target "" false false arities []);
fun instantiation_cmd arities thy = instantiation (Class_Target.read_multi_arity thy arities) thy;
val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);