--- a/src/Pure/Isar/theory_target.ML Fri Nov 23 21:09:34 2007 +0100
+++ b/src/Pure/Isar/theory_target.ML Fri Nov 23 21:09:35 2007 +0100
@@ -2,15 +2,17 @@
ID: $Id$
Author: Makarius
-Common theory/locale/class targets.
+Common theory/locale/class/instantiation targets.
*)
signature THEORY_TARGET =
sig
- val peek: local_theory -> {target: string, is_locale: bool, is_class: bool}
+ val peek: local_theory -> {target: string, is_locale: bool,
+ is_class: bool, instantiation: arity list}
val init: string option -> theory -> local_theory
val begin: string -> Proof.context -> local_theory
val context: xstring -> theory -> local_theory
+ val instantiation: arity list -> theory -> local_theory
end;
structure TheoryTarget: THEORY_TARGET =
@@ -18,12 +20,14 @@
(* context data *)
-datatype target = Target of {target: string, is_locale: bool, is_class: bool};
+datatype target = Target of {target: string, is_locale: bool,
+ is_class: bool, instantiation: arity list};
-fun make_target target is_locale is_class =
- Target {target = target, is_locale = is_locale, is_class = is_class};
+fun make_target target is_locale is_class instantiation =
+ Target {target = target, is_locale = is_locale,
+ is_class = is_class, instantiation = instantiation};
-val global_target = make_target "" false false;
+val global_target = make_target "" false false [];
structure Data = ProofDataFun
(
@@ -36,7 +40,7 @@
(* pretty *)
-fun pretty (Target {target, is_locale, is_class}) ctxt =
+fun pretty (Target {target, is_locale, is_class, instantiation}) ctxt =
let
val thy = ProofContext.theory_of ctxt;
val target_name = (if is_class then "class " else "locale ") ^ Locale.extern thy target;
@@ -186,13 +190,18 @@
Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
end;
-fun declare_const (ta as Target {target, is_locale, is_class}) depends ((c, T), mx) lthy =
+fun declare_const (ta as Target {target, is_locale, is_class, instantiation}) depends ((c, T), mx) lthy =
let
val pos = ContextPosition.properties_of lthy;
val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
val U = map #2 xs ---> T;
val (mx1, mx2, mx3) = fork_mixfix ta mx;
- val (const, lthy') = lthy |> LocalTheory.theory_result (Sign.declare_const pos (c, U, mx3));
+ val declare_const = if null instantiation
+ then Sign.declare_const pos (c, U, mx3)
+ else case Class.instantiation_const lthy c
+ of SOME c' => Class.declare_overloaded (c', U, mx3)
+ | NONE => Sign.declare_const pos (c, U, mx3);
+ val (const, lthy') = lthy |> LocalTheory.theory_result declare_const;
val t = Term.list_comb (const, map Free xs);
in
lthy'
@@ -204,7 +213,7 @@
(* abbrev *)
-fun abbrev (ta as Target {target, is_locale, is_class}) prmode ((c, mx), t) lthy =
+fun abbrev (ta as Target {target, is_locale, is_class, instantiation}) prmode ((c, mx), t) lthy =
let
val pos = ContextPosition.properties_of lthy;
val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
@@ -236,7 +245,7 @@
(* define *)
-fun define (ta as Target {target, is_locale, is_class})
+fun define (ta as Target {target, is_locale, is_class, instantiation})
kind ((c, mx), ((name, atts), rhs)) lthy =
let
val thy = ProofContext.theory_of lthy;
@@ -253,12 +262,18 @@
val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def);
(*def*)
+ val is_instantiation = not (null instantiation)
+ andalso is_some (Class.instantiation_const lthy c);
+ val define_const = if not is_instantiation
+ then (fn name => fn eq => Thm.add_def false (name, Logic.mk_equals eq))
+ else (fn name => fn (Const (c, _), rhs) => Class.define_overloaded name (c, rhs));
val (global_def, lthy3) = lthy2
- |> LocalTheory.theory_result (Thm.add_def false (name', Logic.mk_equals (lhs', rhs')));
- val def = LocalDefs.trans_terms lthy3
+ |> LocalTheory.theory_result (define_const name' (lhs', rhs'));
+ val def = if not is_instantiation then LocalDefs.trans_terms lthy3
[(*c == global.c xs*) local_def,
(*global.c xs == rhs'*) global_def,
- (*rhs' == rhs*) Thm.symmetric rhs_conv];
+ (*rhs' == rhs*) Thm.symmetric rhs_conv]
+ else Thm.transitive local_def global_def;
(*note*)
val ([(res_name, [res])], lthy4) = lthy3
@@ -298,14 +313,18 @@
local
fun init_target _ NONE = global_target
- | init_target thy (SOME target) = make_target target true (Class.is_class thy target);
+ | init_target thy (SOME target) = make_target target true (Class.is_class thy target) [];
+
+fun init_instantiaton arities = make_target "" false false arities
-fun init_ctxt (Target {target, is_locale, is_class}) =
- if not is_locale then ProofContext.init
- else if not is_class then Locale.init target
- else Class.init target;
+fun init_ctxt (Target {target, is_locale, is_class, instantiation}) =
+ if null instantiation then
+ if not is_locale then ProofContext.init
+ else if not is_class then Locale.init target
+ else Class.init target
+ else Class.instantiation instantiation;
-fun init_lthy (ta as Target {target, ...}) =
+fun init_lthy (ta as Target {target, instantiation, ...}) =
Data.put ta #>
LocalTheory.init (NameSpace.base target)
{pretty = pretty ta,
@@ -317,7 +336,7 @@
term_syntax = term_syntax ta,
declaration = declaration ta,
reinit = fn lthy => init_lthy_ctxt ta (ProofContext.theory_of lthy),
- exit = LocalTheory.target_of}
+ exit = if null instantiation then LocalTheory.target_of else Class.end_instantiation}
and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta;
in
@@ -328,6 +347,9 @@
fun context "-" thy = init NONE thy
| context target thy = init (SOME (Locale.intern thy target)) thy;
+fun instantiation raw_arities thy =
+ init_lthy_ctxt (init_instantiaton (map (Sign.cert_arity thy) raw_arities)) thy;
+
end;
end;