src/Pure/Isar/attrib.ML
changeset 16458 4c6fd0c01d28
parent 16344 a52fe1277902
child 16498 9d265401fee0
     1.1 --- a/src/Pure/Isar/attrib.ML	Fri Jun 17 18:33:42 2005 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Fri Jun 17 18:35:27 2005 +0200
     1.3 @@ -8,8 +8,9 @@
     1.4  signature BASIC_ATTRIB =
     1.5  sig
     1.6    val print_attributes: theory -> unit
     1.7 -  val Attribute: bstring -> (Args.src -> theory attribute) * (Args.src -> ProofContext.context attribute)
     1.8 -    -> string -> unit
     1.9 +  val Attribute: bstring ->
    1.10 +    (Args.src -> theory attribute) * (Args.src -> ProofContext.context attribute) ->
    1.11 +    string -> unit
    1.12  end;
    1.13  
    1.14  signature ATTRIB =
    1.15 @@ -17,8 +18,8 @@
    1.16    include BASIC_ATTRIB
    1.17    type src
    1.18    exception ATTRIB_FAIL of (string * Position.T) * exn
    1.19 -  val intern: Sign.sg -> xstring -> string
    1.20 -  val intern_src: Sign.sg -> src -> src
    1.21 +  val intern: theory -> xstring -> string
    1.22 +  val intern_src: theory -> src -> src
    1.23    val global_attribute_i: theory -> src -> theory attribute
    1.24    val global_attribute: theory -> src -> theory attribute
    1.25    val local_attribute_i: theory -> src -> ProofContext.context attribute
    1.26 @@ -33,9 +34,12 @@
    1.27    val global_thm: theory * Args.T list -> thm * (theory * Args.T list)
    1.28    val global_thms: theory * Args.T list -> thm list * (theory * Args.T list)
    1.29    val global_thmss: theory * Args.T list -> thm list * (theory * Args.T list)
    1.30 -  val local_thm: ProofContext.context * Args.T list -> thm * (ProofContext.context * Args.T list)
    1.31 -  val local_thms: ProofContext.context * Args.T list -> thm list * (ProofContext.context * Args.T list)
    1.32 -  val local_thmss: ProofContext.context * Args.T list -> thm list * (ProofContext.context * Args.T list)
    1.33 +  val local_thm: ProofContext.context * Args.T list ->
    1.34 +    thm * (ProofContext.context * Args.T list)
    1.35 +  val local_thms: ProofContext.context * Args.T list ->
    1.36 +    thm list * (ProofContext.context * Args.T list)
    1.37 +  val local_thmss: ProofContext.context * Args.T list ->
    1.38 +    thm list * (ProofContext.context * Args.T list)
    1.39    val syntax: ('a * Args.T list -> 'a attribute * ('a * Args.T list)) -> src -> 'a attribute
    1.40    val no_args: 'a attribute -> src -> 'a attribute
    1.41    val add_del_args: 'a attribute -> 'a attribute -> src -> 'a attribute
    1.42 @@ -50,10 +54,10 @@
    1.43  
    1.44  (** attributes theory data **)
    1.45  
    1.46 -(* data kind 'Isar/attributes' *)
    1.47 +(* datatype attributes *)
    1.48  
    1.49 -structure AttributesDataArgs =
    1.50 -struct
    1.51 +structure AttributesData = TheoryDataFun
    1.52 +(struct
    1.53    val name = "Isar/attributes";
    1.54    type T =
    1.55      ((((src -> theory attribute) * (src -> ProofContext.context attribute))
    1.56 @@ -61,9 +65,9 @@
    1.57  
    1.58    val empty = NameSpace.empty_table;
    1.59    val copy = I;
    1.60 -  val prep_ext = I;
    1.61 +  val extend = I;
    1.62  
    1.63 -  fun merge tables = NameSpace.merge_tables eq_snd tables handle Symtab.DUPS dups =>
    1.64 +  fun merge _ tables = NameSpace.merge_tables eq_snd tables handle Symtab.DUPS dups =>
    1.65      error ("Attempt to merge different versions of attribute(s) " ^ commas_quote dups);
    1.66  
    1.67    fun print _ attribs =
    1.68 @@ -74,16 +78,15 @@
    1.69        [Pretty.big_list "attributes:" (map prt_attr (NameSpace.extern_table attribs))]
    1.70        |> Pretty.chunks |> Pretty.writeln
    1.71      end;
    1.72 -end;
    1.73 +end);
    1.74  
    1.75 -structure AttributesData = TheoryDataFun(AttributesDataArgs);
    1.76  val _ = Context.add_setup [AttributesData.init];
    1.77  val print_attributes = AttributesData.print;
    1.78  
    1.79  
    1.80  (* interning *)
    1.81  
    1.82 -val intern = NameSpace.intern o #1 o AttributesData.get_sg;
    1.83 +val intern = NameSpace.intern o #1 o AttributesData.get;
    1.84  val intern_src = Args.map_name o intern;
    1.85  
    1.86  
    1.87 @@ -103,10 +106,10 @@
    1.88    in attr end;
    1.89  
    1.90  val global_attribute_i = gen_attribute fst;
    1.91 -fun global_attribute thy = global_attribute_i thy o intern_src (Theory.sign_of thy);
    1.92 +fun global_attribute thy = global_attribute_i thy o intern_src thy;
    1.93  
    1.94  val local_attribute_i = gen_attribute snd;
    1.95 -fun local_attribute thy = local_attribute_i thy o intern_src (Theory.sign_of thy);
    1.96 +fun local_attribute thy = local_attribute_i thy o intern_src thy;
    1.97  
    1.98  val context_attribute_i = local_attribute_i o ProofContext.theory_of;
    1.99  val context_attribute = local_attribute o ProofContext.theory_of;
   1.100 @@ -133,10 +136,9 @@
   1.101  
   1.102  fun add_attributes raw_attrs thy =
   1.103    let
   1.104 -    val sg = Theory.sign_of thy;
   1.105      val new_attrs = raw_attrs |> map (fn (name, (f, g), comment) =>
   1.106        (name, (((f, g), comment), stamp ())));
   1.107 -    fun add attrs = NameSpace.extend_table (Sign.naming_of sg) (attrs, new_attrs)
   1.108 +    fun add attrs = NameSpace.extend_table (Sign.naming_of thy) (attrs, new_attrs)
   1.109        handle Symtab.DUPS dups =>
   1.110          error ("Duplicate declaration of attributes(s) " ^ commas_quote dups);
   1.111    in AttributesData.map add thy end;
   1.112 @@ -157,7 +159,7 @@
   1.113  
   1.114  fun gen_thm theory_of attrib get pick = Scan.depend (fn st =>
   1.115    Scan.ahead Args.name -- Args.named_fact (fn name => get st (name, NONE)) --
   1.116 -  Scan.option Args.thm_sel -- Args.opt_attribs (intern (Theory.sign_of (theory_of st)))
   1.117 +  Scan.option Args.thm_sel -- Args.opt_attribs (intern (theory_of st))
   1.118    >> (fn (((name, fact), sel), srcs) =>
   1.119      let
   1.120        val ths = PureThy.select_thm (name, sel) fact;
   1.121 @@ -238,24 +240,24 @@
   1.122  fun the_type types xi = the (types xi)
   1.123    handle Option.Option => error_var "No such variable in theorem: " xi;
   1.124  
   1.125 -fun unify_types sign types ((unifier, maxidx), (xi, u)) =
   1.126 +fun unify_types thy types ((unifier, maxidx), (xi, u)) =
   1.127    let
   1.128      val T = the_type types xi;
   1.129      val U = Term.fastype_of u;
   1.130      val maxidx' = Int.max (maxidx, Int.max (#2 xi, Term.maxidx_of_term u));
   1.131    in
   1.132 -    Type.unify (Sign.tsig_of sign) (unifier, maxidx') (T, U)
   1.133 +    Type.unify (Sign.tsig_of thy) (unifier, maxidx') (T, U)
   1.134        handle Type.TUNIFY => error_var "Incompatible type for instantiation of " xi
   1.135    end;
   1.136  
   1.137  fun typ_subst env = apsnd (Term.typ_subst_TVars env);
   1.138  fun subst env = apsnd (Term.subst_TVars env);
   1.139  
   1.140 -fun instantiate sign envT env thm =
   1.141 +fun instantiate thy envT env thm =
   1.142    let
   1.143      val (_, sorts) = Drule.types_sorts thm;
   1.144 -    fun prepT (a, T) = (Thm.ctyp_of sign (TVar (a, the_sort sorts a)), Thm.ctyp_of sign T);
   1.145 -    fun prep (xi, t) = pairself (Thm.cterm_of sign) (Var (xi, Term.fastype_of t), t);
   1.146 +    fun prepT (a, T) = (Thm.ctyp_of thy (TVar (a, the_sort sorts a)), Thm.ctyp_of thy T);
   1.147 +    fun prep (xi, t) = pairself (Thm.cterm_of thy) (Var (xi, Term.fastype_of t), t);
   1.148    in
   1.149      Drule.instantiate (map prepT (distinct envT),
   1.150        map prep (gen_distinct (fn ((xi, t), (yj, u)) => xi = yj andalso t aconv u) env)) thm
   1.151 @@ -266,7 +268,7 @@
   1.152  fun read_instantiate init mixed_insts (context, thm) =
   1.153    let
   1.154      val ctxt = init context;
   1.155 -    val sign = ProofContext.sign_of ctxt;
   1.156 +    val thy = ProofContext.theory_of ctxt;
   1.157  
   1.158      val (type_insts, term_insts) = List.partition (is_tvar o #1) (map #2 mixed_insts);
   1.159      val internal_insts = term_insts |> List.mapPartial
   1.160 @@ -290,23 +292,23 @@
   1.161            | Args.Typ T => T
   1.162            | _ => error_var "Type argument expected for " xi);
   1.163        in
   1.164 -        if Sign.of_sort sign (T, S) then (xi, T)
   1.165 +        if Sign.of_sort thy (T, S) then (xi, T)
   1.166          else error_var "Incompatible sort for typ instantiation of " xi
   1.167        end;
   1.168  
   1.169      val type_insts' = map readT type_insts;
   1.170 -    val thm' = instantiate sign type_insts' [] thm;
   1.171 +    val thm' = instantiate thy type_insts' [] thm;
   1.172  
   1.173  
   1.174      (* internal term instantiations *)
   1.175  
   1.176      val types' = #1 (Drule.types_sorts thm');
   1.177      val unifier = map (apsnd snd) (Vartab.dest (#1
   1.178 -      (Library.foldl (unify_types sign types') ((Vartab.empty, 0), internal_insts))));
   1.179 +      (Library.foldl (unify_types thy types') ((Vartab.empty, 0), internal_insts))));
   1.180  
   1.181      val type_insts'' = map (typ_subst unifier) type_insts';
   1.182      val internal_insts'' = map (subst unifier) internal_insts;
   1.183 -    val thm'' = instantiate sign unifier internal_insts'' thm';
   1.184 +    val thm'' = instantiate thy unifier internal_insts'' thm';
   1.185  
   1.186  
   1.187      (* external term instantiations *)
   1.188 @@ -323,7 +325,7 @@
   1.189  
   1.190      val external_insts''' = xs ~~ ts;
   1.191      val term_insts''' = internal_insts''' @ external_insts''';
   1.192 -    val thm''' = instantiate sign inferred external_insts''' thm'';
   1.193 +    val thm''' = instantiate thy inferred external_insts''' thm'';
   1.194    in
   1.195  
   1.196      (* assign internalized values *)