src/Pure/Isar/class.ML
changeset 63347 e344dc82f6c2
parent 62939 ef8d840f39fb
child 66337 a849ce33923d
     1.1 --- a/src/Pure/Isar/class.ML	Wed Jun 22 11:10:18 2016 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Wed Jun 22 16:04:03 2016 +0200
     1.3 @@ -12,18 +12,18 @@
     1.4    val base_sort: theory -> class -> sort
     1.5    val rules: theory -> class -> thm option * thm
     1.6    val these_defs: theory -> sort -> thm list
     1.7 -  val these_operations: theory -> sort
     1.8 -    -> (string * (class * ((typ * term) * bool))) list
     1.9 +  val these_operations: theory -> sort -> (string * (class * ((typ * term) * bool))) list
    1.10    val print_classes: Proof.context -> unit
    1.11    val init: class -> theory -> Proof.context
    1.12    val begin: class list -> sort -> Proof.context -> Proof.context
    1.13 -  val const: class -> (binding * mixfix) * term -> term list * term list -> local_theory -> local_theory
    1.14 -  val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
    1.15 +  val const: class -> (binding * mixfix) * term -> term list * term list ->
    1.16 +    local_theory -> local_theory
    1.17 +  val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> local_theory ->
    1.18 +    (term * term) * local_theory
    1.19    val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
    1.20    val class_prefix: string -> string
    1.21 -  val register: class -> class list -> ((string * typ) * (string * typ)) list
    1.22 -    -> sort -> morphism -> morphism -> thm option -> thm option -> thm
    1.23 -    -> theory -> theory
    1.24 +  val register: class -> class list -> ((string * typ) * (string * typ)) list ->
    1.25 +    sort -> morphism -> morphism -> thm option -> thm option -> thm -> theory -> theory
    1.26  
    1.27    (*instances*)
    1.28    val instantiation: string list * (string * sort) list * sort -> theory -> local_theory
    1.29 @@ -160,6 +160,11 @@
    1.30  
    1.31  val export_morphism = #export_morph oo the_class_data;
    1.32  
    1.33 +fun pretty_param ctxt (c, ty) =
    1.34 +  Pretty.block
    1.35 +   [Name_Space.pretty ctxt (Proof_Context.const_space ctxt) c, Pretty.str " ::",
    1.36 +    Pretty.brk 1, Syntax.pretty_typ ctxt ty];
    1.37 +
    1.38  fun print_classes ctxt =
    1.39    let
    1.40      val thy = Proof_Context.theory_of ctxt;
    1.41 @@ -167,7 +172,6 @@
    1.42  
    1.43      val class_space = Proof_Context.class_space ctxt;
    1.44      val type_space = Proof_Context.type_space ctxt;
    1.45 -    val const_space = Proof_Context.const_space ctxt;
    1.46  
    1.47      val arities =
    1.48        Symtab.empty
    1.49 @@ -183,10 +187,7 @@
    1.50          val Ss = Sorts.mg_domain algebra tyco [class];
    1.51        in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
    1.52  
    1.53 -    fun prt_param (c, ty) =
    1.54 -      Pretty.block
    1.55 -       [Name_Space.pretty ctxt const_space c, Pretty.str " ::",
    1.56 -        Pretty.brk 1, Syntax.pretty_typ ctxt (Type.strip_sorts_dummy ty)];
    1.57 +    fun prt_param (c, ty) = pretty_param ctxt (c, Type.strip_sorts_dummy ty);
    1.58  
    1.59      fun prt_entry class =
    1.60        Pretty.block
    1.61 @@ -607,16 +608,28 @@
    1.62  
    1.63  (* target *)
    1.64  
    1.65 -fun define_overloaded (c, U) v (b_def, rhs) =
    1.66 -  Local_Theory.background_theory_result (Axclass.declare_overloaded (c, U)
    1.67 -  ##>> Axclass.define_overloaded b_def (c, rhs))
    1.68 -  ##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v))
    1.69 -  ##> Local_Theory.map_contexts (K synchronize_inst_syntax);
    1.70 +fun define_overloaded (c, U) b (b_def, rhs) lthy =
    1.71 +  let
    1.72 +    val name = Binding.name_of b;
    1.73 +    val pos = Binding.pos_of b;
    1.74 +    val _ =
    1.75 +      if Context_Position.is_reported lthy pos then
    1.76 +        Position.report_text pos Markup.class_parameter
    1.77 +          (Pretty.string_of
    1.78 +            (Pretty.block [Pretty.keyword1 "class", Pretty.brk 1,
    1.79 +                Pretty.str "parameter", Pretty.brk 1, pretty_param lthy (c, U)]))
    1.80 +      else ();
    1.81 +  in
    1.82 +    lthy |> Local_Theory.background_theory_result
    1.83 +      (Axclass.declare_overloaded (c, U) ##>> Axclass.define_overloaded b_def (c, rhs))
    1.84 +    ||> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = name))
    1.85 +    ||> Local_Theory.map_contexts (K synchronize_inst_syntax)
    1.86 +  end;
    1.87  
    1.88  fun foundation (((b, U), mx), (b_def, rhs)) params lthy =
    1.89    (case instantiation_param lthy b of
    1.90      SOME c =>
    1.91 -      if Mixfix.is_empty mx then lthy |> define_overloaded (c, U) (Binding.name_of b) (b_def, rhs)
    1.92 +      if Mixfix.is_empty mx then lthy |> define_overloaded (c, U) b (b_def, rhs)
    1.93        else error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
    1.94    | NONE => lthy |> Generic_Target.theory_target_foundation (((b, U), mx), (b_def, rhs)) params);
    1.95