src/Pure/Isar/theory_target.ML
changeset 29358 efdfe5dfe008
parent 29252 ea97aa6aeba2
child 29360 a5be60c3674e
     1.1 --- a/src/Pure/Isar/theory_target.ML	Mon Jan 05 15:35:42 2009 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Mon Jan 05 15:36:24 2009 +0100
     1.3 @@ -13,6 +13,7 @@
     1.4    val begin: string -> Proof.context -> local_theory
     1.5    val context: xstring -> theory -> local_theory
     1.6    val instantiation: string list * (string * sort) list * sort -> theory -> local_theory
     1.7 +  val instantiation_cmd: xstring list * sort * xstring -> theory -> local_theory
     1.8    val overloading: (string * (string * typ) * bool) list -> theory -> local_theory
     1.9    val overloading_cmd: (string * string * bool) list -> theory -> local_theory
    1.10  end;
    1.11 @@ -82,7 +83,7 @@
    1.12    Pretty.block [Pretty.str "theory", Pretty.brk 1,
    1.13        Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] ::
    1.14      (if not (null overloading) then [Overloading.pretty ctxt]
    1.15 -     else if not (null (#1 instantiation)) then [Class.pretty_instantiation ctxt]
    1.16 +     else if not (null (#1 instantiation)) then [Class_Target.pretty_instantiation ctxt]
    1.17       else pretty_thy ctxt target is_locale is_class);
    1.18  
    1.19  
    1.20 @@ -108,7 +109,7 @@
    1.21  
    1.22  fun class_target (Target {target, ...}) f =
    1.23    LocalTheory.raw_theory f #>
    1.24 -  LocalTheory.target (Class.refresh_syntax target);
    1.25 +  LocalTheory.target (Class_Target.refresh_syntax target);
    1.26  
    1.27  
    1.28  (* notes *)
    1.29 @@ -207,7 +208,7 @@
    1.30      val (prefix', _) = Binding.dest b';
    1.31      val class_global = Binding.base_name b = Binding.base_name b'
    1.32        andalso not (null prefix')
    1.33 -      andalso (fst o snd o split_last) prefix' = Class.class_prefix target;
    1.34 +      andalso (fst o snd o split_last) prefix' = Class_Target.class_prefix target;
    1.35    in
    1.36      not (is_class andalso (similar_body orelse class_global)) ?
    1.37        (Context.mapping_result
    1.38 @@ -231,11 +232,11 @@
    1.39      val (mx1, mx2, mx3) = fork_mixfix ta mx;
    1.40      fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
    1.41      val declare_const =
    1.42 -      (case Class.instantiation_param lthy c of
    1.43 +      (case Class_Target.instantiation_param lthy c of
    1.44          SOME c' =>
    1.45            if mx3 <> NoSyn then syntax_error c'
    1.46            else LocalTheory.theory_result (AxClass.declare_overloaded (c', U))
    1.47 -            ##> Class.confirm_declaration c
    1.48 +            ##> Class_Target.confirm_declaration c
    1.49          | NONE =>
    1.50              (case Overloading.operation lthy c of
    1.51                SOME (c', _) =>
    1.52 @@ -248,7 +249,7 @@
    1.53    in
    1.54      lthy'
    1.55      |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default tags ((b, mx2), t))
    1.56 -    |> is_class ? class_target ta (Class.declare target tags ((c, mx1), t))
    1.57 +    |> is_class ? class_target ta (Class_Target.declare target tags ((c, mx1), t))
    1.58      |> LocalDefs.add_def ((b, NoSyn), t)
    1.59    end;
    1.60  
    1.61 @@ -275,7 +276,7 @@
    1.62          #-> (fn (lhs, _) =>
    1.63            let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
    1.64              term_syntax ta (locale_const ta prmode tags ((b, mx2), lhs')) #>
    1.65 -            is_class ? class_target ta (Class.abbrev target prmode tags ((c, mx1), t'))
    1.66 +            is_class ? class_target ta (Class_Target.abbrev target prmode tags ((c, mx1), t'))
    1.67            end)
    1.68        else
    1.69          LocalTheory.theory
    1.70 @@ -311,7 +312,7 @@
    1.71          SOME (_, checked) =>
    1.72            (fn name => fn (Const (c, _), rhs) => Overloading.define checked name (c, rhs))
    1.73        | NONE =>
    1.74 -          if is_none (Class.instantiation_param lthy c)
    1.75 +          if is_none (Class_Target.instantiation_param lthy c)
    1.76            then (fn name => fn eq => Thm.add_def false false (name, Logic.mk_equals eq))
    1.77            else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs)));
    1.78      val (global_def, lthy3) = lthy2
    1.79 @@ -334,14 +335,14 @@
    1.80  fun init_target _ NONE = global_target
    1.81    | init_target thy (SOME target) =
    1.82        make_target target (NewLocale.test_locale thy (NewLocale.intern thy target))
    1.83 -      true (Class.is_class thy target) ([], [], []) [];
    1.84 +      true (Class_Target.is_class thy target) ([], [], []) [];
    1.85  
    1.86  fun init_ctxt (Target {target, new_locale, is_locale, is_class, instantiation, overloading}) =
    1.87 -  if not (null (#1 instantiation)) then Class.init_instantiation instantiation
    1.88 +  if not (null (#1 instantiation)) then Class_Target.init_instantiation instantiation
    1.89    else if not (null overloading) then Overloading.init overloading
    1.90    else if not is_locale then ProofContext.init
    1.91    else if not is_class then locale_init new_locale target
    1.92 -  else Class.init target;
    1.93 +  else Class_Target.init target;
    1.94  
    1.95  fun init_lthy (ta as Target {target, instantiation, overloading, ...}) =
    1.96    Data.put ta #>
    1.97 @@ -355,11 +356,20 @@
    1.98      declaration = declaration ta,
    1.99      reinit = fn lthy => init_lthy_ctxt ta (ProofContext.theory_of lthy),
   1.100      exit = LocalTheory.target_of o
   1.101 -      (if not (null (#1 instantiation)) then Class.conclude_instantiation
   1.102 +      (if not (null (#1 instantiation)) then Class_Target.conclude_instantiation
   1.103         else if not (null overloading) then Overloading.conclude
   1.104         else I)}
   1.105  and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta;
   1.106  
   1.107 +fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
   1.108 +  let
   1.109 +    val all_arities = map (fn raw_tyco => Sign.read_arity thy
   1.110 +      (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
   1.111 +    val tycos = map #1 all_arities;
   1.112 +    val (_, sorts, sort) = hd all_arities;
   1.113 +    val vs = Name.names Name.context Name.aT sorts;
   1.114 +  in (tycos, vs, sort) end;
   1.115 +
   1.116  fun gen_overloading prep_const raw_ops thy =
   1.117    let
   1.118      val ctxt = ProofContext.init thy;
   1.119 @@ -377,6 +387,8 @@
   1.120        (NewLocale.test_locale thy (NewLocale.intern thy target)) thy target)) thy;
   1.121  
   1.122  fun instantiation arities = init_lthy_ctxt (make_target "" false false false arities []);
   1.123 +fun instantiation_cmd raw_arities thy =
   1.124 +  instantiation (read_multi_arity thy raw_arities) thy;
   1.125  
   1.126  val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
   1.127  val overloading_cmd = gen_overloading Syntax.read_term;