src/Pure/Isar/theory_target.ML
changeset 25462 dad0291cb76a
parent 25395 e83bef45e6a7
child 25485 33840a854e63
     1.1 --- a/src/Pure/Isar/theory_target.ML	Fri Nov 23 21:09:34 2007 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Fri Nov 23 21:09:35 2007 +0100
     1.3 @@ -2,15 +2,17 @@
     1.4      ID:         $Id$
     1.5      Author:     Makarius
     1.6  
     1.7 -Common theory/locale/class targets.
     1.8 +Common theory/locale/class/instantiation targets.
     1.9  *)
    1.10  
    1.11  signature THEORY_TARGET =
    1.12  sig
    1.13 -  val peek: local_theory -> {target: string, is_locale: bool, is_class: bool}
    1.14 +  val peek: local_theory -> {target: string, is_locale: bool,
    1.15 +    is_class: bool, instantiation: arity list}
    1.16    val init: string option -> theory -> local_theory
    1.17    val begin: string -> Proof.context -> local_theory
    1.18    val context: xstring -> theory -> local_theory
    1.19 +  val instantiation: arity list -> theory -> local_theory
    1.20  end;
    1.21  
    1.22  structure TheoryTarget: THEORY_TARGET =
    1.23 @@ -18,12 +20,14 @@
    1.24  
    1.25  (* context data *)
    1.26  
    1.27 -datatype target = Target of {target: string, is_locale: bool, is_class: bool};
    1.28 +datatype target = Target of {target: string, is_locale: bool,
    1.29 +  is_class: bool, instantiation: arity list};
    1.30  
    1.31 -fun make_target target is_locale is_class =
    1.32 -  Target {target = target, is_locale = is_locale, is_class = is_class};
    1.33 +fun make_target target is_locale is_class instantiation =
    1.34 +  Target {target = target, is_locale = is_locale,
    1.35 +    is_class = is_class, instantiation = instantiation};
    1.36  
    1.37 -val global_target = make_target "" false false;
    1.38 +val global_target = make_target "" false false [];
    1.39  
    1.40  structure Data = ProofDataFun
    1.41  (
    1.42 @@ -36,7 +40,7 @@
    1.43  
    1.44  (* pretty *)
    1.45  
    1.46 -fun pretty (Target {target, is_locale, is_class}) ctxt =
    1.47 +fun pretty (Target {target, is_locale, is_class, instantiation}) ctxt =
    1.48    let
    1.49      val thy = ProofContext.theory_of ctxt;
    1.50      val target_name = (if is_class then "class " else "locale ") ^ Locale.extern thy target;
    1.51 @@ -186,13 +190,18 @@
    1.52               Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
    1.53    end;
    1.54  
    1.55 -fun declare_const (ta as Target {target, is_locale, is_class}) depends ((c, T), mx) lthy =
    1.56 +fun declare_const (ta as Target {target, is_locale, is_class, instantiation}) depends ((c, T), mx) lthy =
    1.57    let
    1.58      val pos = ContextPosition.properties_of lthy;
    1.59      val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
    1.60      val U = map #2 xs ---> T;
    1.61      val (mx1, mx2, mx3) = fork_mixfix ta mx;
    1.62 -    val (const, lthy') = lthy |> LocalTheory.theory_result (Sign.declare_const pos (c, U, mx3));
    1.63 +    val declare_const = if null instantiation
    1.64 +      then Sign.declare_const pos (c, U, mx3)
    1.65 +      else case Class.instantiation_const lthy c
    1.66 +       of SOME c' => Class.declare_overloaded (c', U, mx3)
    1.67 +        | NONE => Sign.declare_const pos (c, U, mx3);
    1.68 +    val (const, lthy') = lthy |> LocalTheory.theory_result declare_const;
    1.69      val t = Term.list_comb (const, map Free xs);
    1.70    in
    1.71      lthy'
    1.72 @@ -204,7 +213,7 @@
    1.73  
    1.74  (* abbrev *)
    1.75  
    1.76 -fun abbrev (ta as Target {target, is_locale, is_class}) prmode ((c, mx), t) lthy =
    1.77 +fun abbrev (ta as Target {target, is_locale, is_class, instantiation}) prmode ((c, mx), t) lthy =
    1.78    let
    1.79      val pos = ContextPosition.properties_of lthy;
    1.80      val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
    1.81 @@ -236,7 +245,7 @@
    1.82  
    1.83  (* define *)
    1.84  
    1.85 -fun define (ta as Target {target, is_locale, is_class})
    1.86 +fun define (ta as Target {target, is_locale, is_class, instantiation})
    1.87      kind ((c, mx), ((name, atts), rhs)) lthy =
    1.88    let
    1.89      val thy = ProofContext.theory_of lthy;
    1.90 @@ -253,12 +262,18 @@
    1.91      val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def);
    1.92  
    1.93      (*def*)
    1.94 +    val is_instantiation = not (null instantiation)
    1.95 +      andalso is_some (Class.instantiation_const lthy c);
    1.96 +    val define_const = if not is_instantiation
    1.97 +      then (fn name => fn eq => Thm.add_def false (name, Logic.mk_equals eq))
    1.98 +      else (fn name => fn (Const (c, _), rhs) => Class.define_overloaded name (c, rhs));
    1.99      val (global_def, lthy3) = lthy2
   1.100 -      |> LocalTheory.theory_result (Thm.add_def false (name', Logic.mk_equals (lhs', rhs')));
   1.101 -    val def = LocalDefs.trans_terms lthy3
   1.102 +      |> LocalTheory.theory_result (define_const name' (lhs', rhs'));
   1.103 +    val def = if not is_instantiation then LocalDefs.trans_terms lthy3
   1.104        [(*c == global.c xs*)     local_def,
   1.105         (*global.c xs == rhs'*)  global_def,
   1.106 -       (*rhs' == rhs*)          Thm.symmetric rhs_conv];
   1.107 +       (*rhs' == rhs*)          Thm.symmetric rhs_conv]
   1.108 +      else Thm.transitive local_def global_def;
   1.109  
   1.110      (*note*)
   1.111      val ([(res_name, [res])], lthy4) = lthy3
   1.112 @@ -298,14 +313,18 @@
   1.113  local
   1.114  
   1.115  fun init_target _ NONE = global_target
   1.116 -  | init_target thy (SOME target) = make_target target true (Class.is_class thy target);
   1.117 +  | init_target thy (SOME target) = make_target target true (Class.is_class thy target) [];
   1.118 +
   1.119 +fun init_instantiaton arities = make_target "" false false arities
   1.120  
   1.121 -fun init_ctxt (Target {target, is_locale, is_class}) =
   1.122 -  if not is_locale then ProofContext.init
   1.123 -  else if not is_class then Locale.init target
   1.124 -  else Class.init target;
   1.125 +fun init_ctxt (Target {target, is_locale, is_class, instantiation}) =
   1.126 +  if null instantiation then
   1.127 +    if not is_locale then ProofContext.init
   1.128 +    else if not is_class then Locale.init target
   1.129 +    else Class.init target
   1.130 +  else Class.instantiation instantiation;
   1.131  
   1.132 -fun init_lthy (ta as Target {target, ...}) =
   1.133 +fun init_lthy (ta as Target {target, instantiation, ...}) =
   1.134    Data.put ta #>
   1.135    LocalTheory.init (NameSpace.base target)
   1.136     {pretty = pretty ta,
   1.137 @@ -317,7 +336,7 @@
   1.138      term_syntax = term_syntax ta,
   1.139      declaration = declaration ta,
   1.140      reinit = fn lthy => init_lthy_ctxt ta (ProofContext.theory_of lthy),
   1.141 -    exit = LocalTheory.target_of}
   1.142 +    exit = if null instantiation then LocalTheory.target_of else Class.end_instantiation}
   1.143  and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta;
   1.144  
   1.145  in
   1.146 @@ -328,6 +347,9 @@
   1.147  fun context "-" thy = init NONE thy
   1.148    | context target thy = init (SOME (Locale.intern thy target)) thy;
   1.149  
   1.150 +fun instantiation raw_arities thy =
   1.151 +  init_lthy_ctxt (init_instantiaton (map (Sign.cert_arity thy) raw_arities)) thy;
   1.152 +
   1.153  end;
   1.154  
   1.155  end;