added is_class;
authorwenzelm
Sun Oct 14 00:18:05 2007 +0200 (2007-10-14)
changeset 250240615bb9955dd
parent 25023 52eb78ebb370
child 25025 17c845095a47
added is_class;
tuned signature of add_const/abbrev_in_class;
removed obsolete class_of_locale/locale_of_class;
tuned name prefixing: Sign.full_name does the job;
src/Pure/Isar/class.ML
     1.1 --- a/src/Pure/Isar/class.ML	Sat Oct 13 17:16:46 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Sun Oct 14 00:18:05 2007 +0200
     1.3 @@ -19,13 +19,11 @@
     1.4    val class_cmd: bstring -> xstring list -> Element.context Locale.element list
     1.5      -> xstring list -> theory -> string * Proof.context
     1.6    val init: class -> Proof.context -> Proof.context;
     1.7 -  val add_const_in_class: string -> (string * term) * Syntax.mixfix
     1.8 -    -> theory -> string * theory
     1.9 -  val add_abbrev_in_class: string -> Syntax.mode -> (string * term) * mixfix
    1.10 -    -> theory -> string * theory
    1.11 +  val add_const_in_class: string -> (string * mixfix) * term -> theory -> string * theory
    1.12 +  val add_abbrev_in_class: string -> Syntax.mode -> (string * mixfix) * term -> theory ->
    1.13 +    string * theory
    1.14    val remove_constraint: class -> string -> Proof.context -> Proof.context
    1.15 -  val class_of_locale: theory -> string -> class option
    1.16 -  val locale_of_class: theory -> class -> string
    1.17 +  val is_class: theory -> string -> bool
    1.18    val these_params: theory -> sort -> (string * (string * typ)) list
    1.19    val intro_classes_tac: thm list -> tactic
    1.20    val default_intro_classes_tac: thm list -> tactic
    1.21 @@ -170,9 +168,9 @@
    1.22  
    1.23  fun add_inst_def (class, tyco) (c, ty) thy =
    1.24    let
    1.25 -    val tyco_base = NameSpace.base tyco;
    1.26 -    val name_inst = NameSpace.base class ^ "_" ^ tyco_base ^ "_inst";
    1.27 -    val c_inst_base = NameSpace.base c ^ "_" ^ tyco_base;
    1.28 +    val tyco_base = Sign.base_name tyco;
    1.29 +    val name_inst = Sign.base_name class ^ "_" ^ tyco_base ^ "_inst";
    1.30 +    val c_inst_base = Sign.base_name c ^ "_" ^ tyco_base;
    1.31    in
    1.32      thy
    1.33      |> Sign.sticky_prefix name_inst
    1.34 @@ -362,16 +360,15 @@
    1.35  
    1.36  (* queries *)
    1.37  
    1.38 +val is_class = Symtab.defined o snd o ClassData.get;
    1.39 +
    1.40  val lookup_class_data = Option.map rep_class_data oo try o Graph.get_node
    1.41    o fst o ClassData.get;
    1.42 -fun class_of_locale thy = Symtab.lookup ((snd o ClassData.get) thy);
    1.43  
    1.44  fun the_class_data thy class = case lookup_class_data thy class
    1.45   of NONE => error ("Undeclared class " ^ quote class)
    1.46    | SOME data => data;
    1.47  
    1.48 -val locale_of_class = #locale oo the_class_data;
    1.49 -
    1.50  val ancestry = Graph.all_succs o fst o ClassData.get;
    1.51  
    1.52  fun these_params thy =
    1.53 @@ -469,6 +466,8 @@
    1.54  
    1.55  (** rule calculation, tactics and methods **)
    1.56  
    1.57 +val class_prefix = Logic.const_of_class o Sign.base_name;
    1.58 +
    1.59  fun class_intro thy locale class sups =
    1.60    let
    1.61      fun class_elim class =
    1.62 @@ -500,11 +499,10 @@
    1.63  
    1.64  fun class_interpretation class facts defs thy =
    1.65    let
    1.66 -    val { locale, inst, ... } = the_class_data thy class;
    1.67 +    val inst = #inst (the_class_data thy class);
    1.68      val tac = ALLGOALS (ProofContext.fact_tac facts);
    1.69 -    val prfx = Logic.const_of_class (NameSpace.base class);
    1.70    in
    1.71 -    prove_interpretation tac ((false, prfx), []) (Locale.Locale locale)
    1.72 +    prove_interpretation tac ((false, class_prefix class), []) (Locale.Locale class)
    1.73        (inst, defs) thy
    1.74    end;
    1.75  
    1.76 @@ -727,14 +725,14 @@
    1.77                Const ((fst o the o AList.lookup (op =) consts) c, ty)
    1.78            | subst t = t;
    1.79          fun prep_asm ((name, atts), ts) =
    1.80 -          ((NameSpace.base name, map (Attrib.attribute_i thy) atts),
    1.81 +          ((Sign.base_name name, map (Attrib.attribute_i thy) atts),
    1.82              (map o map_aterms) subst ts);
    1.83        in
    1.84          Locale.global_asms_of thy name_locale
    1.85          |> map prep_asm
    1.86        end;
    1.87      fun note_intro name_axclass class_intro =
    1.88 -      PureThy.note_thmss_qualified "" ((Logic.const_of_class o NameSpace.base) name_axclass)
    1.89 +      PureThy.note_thmss_qualified "" (class_prefix name_axclass)
    1.90          [(("intro", []), [([class_intro], [])])]
    1.91        #> snd
    1.92    in
    1.93 @@ -784,23 +782,19 @@
    1.94      val typidx = find_index (fn TFree (w, _) => Name.aT = w | _ => false) typargs;
    1.95    in (c, (rhs, (ty, typidx))) end;
    1.96  
    1.97 -fun add_const_in_class class ((c, rhs), syn) thy =
    1.98 +fun add_const_in_class class ((c, mx), rhs) thy =
    1.99    let
   1.100 -    val prfx = (Logic.const_of_class o NameSpace.base) class;
   1.101 -    fun mk_name c =
   1.102 -      let
   1.103 -        val n1 = Sign.full_name thy c;
   1.104 -        val n2 = NameSpace.qualifier n1;
   1.105 -        val n3 = NameSpace.base n1;
   1.106 -      in NameSpace.implode [n2, prfx, n3] end;
   1.107 -    val rhs' = export_fixes thy class rhs;
   1.108 +    val prfx = class_prefix class;
   1.109 +    val thy' = thy |> Sign.add_path prfx;
   1.110 +
   1.111 +    val rhs' = export_fixes thy' class rhs;
   1.112      val subst_typ = Term.map_type_tfree (fn var as (w, sort) =>
   1.113        if w = Name.aT then TFree (w, [class]) else TFree var);
   1.114      val ty' = Term.fastype_of rhs';
   1.115      val ty'' = subst_typ ty';
   1.116 -    val c' = mk_name c;
   1.117 +    val c' = Sign.full_name thy' c;
   1.118      val def = (c, Logic.mk_equals (Const (c', ty'), rhs'));
   1.119 -    val (syn', _) = fork_mixfix true true syn;
   1.120 +    val (mx', _) = fork_mixfix true true mx;
   1.121      fun interpret def thy =
   1.122        let
   1.123          val def' = symmetric def;
   1.124 @@ -813,9 +807,8 @@
   1.125          |-> (fn entry => register_operation class (entry, SOME def'))
   1.126        end;
   1.127    in
   1.128 -    thy
   1.129 -    |> Sign.add_path prfx
   1.130 -    |> Sign.declare_const [] (c, ty', syn') |> snd
   1.131 +    thy'
   1.132 +    |> Sign.declare_const [] (c, ty', mx') |> snd
   1.133      |> Sign.parent_path
   1.134      |> Sign.sticky_prefix prfx
   1.135      |> PureThy.add_defs_i false [(def, [])]
   1.136 @@ -827,22 +820,17 @@
   1.137  
   1.138  (* abbreviation in class target *)
   1.139  
   1.140 -fun add_abbrev_in_class class prmode ((c, rhs), syn) thy =
   1.141 +fun add_abbrev_in_class class prmode ((c, mx), rhs) thy =
   1.142    let
   1.143 -    val prfx = (Logic.const_of_class o NameSpace.base) class;
   1.144 -    fun mk_name c =
   1.145 -      let
   1.146 -        val n1 = Sign.full_name thy c;
   1.147 -        val n2 = NameSpace.qualifier n1;
   1.148 -        val n3 = NameSpace.base n1;
   1.149 -      in NameSpace.implode [n2, prfx, prfx, n3] end;
   1.150 -    val c' = mk_name c;
   1.151 +    val prfx = class_prefix class;
   1.152 +    val naming = Sign.naming_of thy |> NameSpace.add_path prfx |> NameSpace.add_path prfx; (* FIXME !? *)
   1.153 +    val c' = NameSpace.full naming c;
   1.154      val rhs' = export_fixes thy class rhs;
   1.155      val ty' = Term.fastype_of rhs';
   1.156      val entry = mk_operation_entry thy (c', rhs);
   1.157    in
   1.158      thy
   1.159 -    |> Sign.notation true prmode [(Const (c', ty'), syn)]
   1.160 +    |> Sign.notation true prmode [(Const (c', ty'), mx)]
   1.161      |> register_operation class (entry, NONE)
   1.162      |> pair c'
   1.163    end;