src/Pure/sign.ML
changeset 28861 f53abb0733ee
parent 28792 1d80cee865de
child 28863 32e83a854e5e
     1.1 --- a/src/Pure/sign.ML	Thu Nov 20 14:51:40 2008 +0100
     1.2 +++ b/src/Pure/sign.ML	Thu Nov 20 14:55:25 2008 +0100
     1.3 @@ -18,6 +18,7 @@
     1.4    val name_decl: (string * 'a -> theory -> 'b * theory)
     1.5      -> Name.binding * 'a -> theory -> (string * 'b) * theory
     1.6    val full_name: theory -> bstring -> string
     1.7 +  val full_binding: theory -> Name.binding -> string
     1.8    val full_name_path: theory -> string -> bstring -> string
     1.9    val declare_name: theory -> string -> NameSpace.T -> NameSpace.T
    1.10    val syn_of: theory -> Syntax.syntax
    1.11 @@ -93,10 +94,10 @@
    1.12    val del_modesyntax: Syntax.mode -> (bstring * string * mixfix) list -> theory -> theory
    1.13    val del_modesyntax_i: Syntax.mode -> (bstring * typ * mixfix) list -> theory -> theory
    1.14    val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
    1.15 +  val declare_const: Properties.T -> (Name.binding * typ) * mixfix -> theory -> term * theory
    1.16    val add_consts: (bstring * string * mixfix) list -> theory -> theory
    1.17    val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
    1.18 -  val declare_const: Properties.T -> (Name.binding * typ) * mixfix -> theory -> term * theory
    1.19 -  val add_abbrev: string -> Properties.T -> bstring * term -> theory -> (term * term) * theory
    1.20 +  val add_abbrev: string -> Properties.T -> Name.binding * term -> theory -> (term * term) * theory
    1.21    val revert_abbrev: string -> string -> theory -> theory
    1.22    val add_const_constraint: string * typ option -> theory -> theory
    1.23    val primitive_class: string * class list -> theory -> theory
    1.24 @@ -190,20 +191,21 @@
    1.25  val naming_of = #naming o rep_sg;
    1.26  val base_name = NameSpace.base;
    1.27  
    1.28 -fun name_decl decl (binding, x) thy =
    1.29 +fun name_decl decl (b, x) thy =
    1.30    let
    1.31      val naming = naming_of thy;
    1.32 -    val (naming', name) = Name.namify naming binding;
    1.33 +    val (naming', name) = Name.namify naming b;
    1.34    in
    1.35      thy
    1.36      |> map_naming (K naming')
    1.37 -    |> decl (Name.name_of binding, x)
    1.38 +    |> decl (Name.name_of b, x)
    1.39      |>> pair name
    1.40      ||> map_naming (K naming)
    1.41    end;
    1.42  
    1.43  val namify = Name.namify o naming_of;
    1.44  val full_name = NameSpace.full o naming_of;
    1.45 +val full_binding = NameSpace.full_binding o naming_of;
    1.46  fun full_name_path thy elems = NameSpace.full (NameSpace.add_path elems (naming_of thy));
    1.47  val declare_name = NameSpace.declare o naming_of;
    1.48  
    1.49 @@ -520,15 +522,16 @@
    1.50    let
    1.51      val ctxt = ProofContext.init thy;
    1.52      val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
    1.53 -    fun prep (raw_c, raw_T, raw_mx) =
    1.54 +    fun prep (raw_b, raw_T, raw_mx) =
    1.55        let
    1.56 -        val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
    1.57 -        val full_c = full_name thy c;
    1.58 -        val c' = if authentic then Syntax.constN ^ full_c else c;
    1.59 +        val (mx_name, mx) = Syntax.const_mixfix (Name.name_of raw_b) raw_mx;
    1.60 +        val b = Name.map_name (K mx_name) raw_b;
    1.61 +        val c = full_binding thy b;
    1.62 +        val c_syn = if authentic then Syntax.constN ^ c else Name.name_of b;
    1.63          val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
    1.64 -          cat_error msg ("in declaration of constant " ^ quote c);
    1.65 +          cat_error msg ("in declaration of constant " ^ quote (Name.display b));
    1.66          val T' = Logic.varifyT T;
    1.67 -      in ((c, T'), (c', T', mx), Const (full_c, T)) end;
    1.68 +      in ((b, T'), (c_syn, T', mx), Const (c, T)) end;
    1.69      val args = map prep raw_args;
    1.70      val tags' = tags |> Properties.put (Markup.theory_nameN, Context.theory_name thy);
    1.71    in
    1.72 @@ -538,18 +541,19 @@
    1.73      |> pair (map #3 args)
    1.74    end;
    1.75  
    1.76 +fun bindify (name, T, mx) = (Name.binding name, T, mx);
    1.77 +
    1.78  in
    1.79  
    1.80 -val add_consts = snd oo gen_add_consts Syntax.parse_typ false [];
    1.81 -val add_consts_i = snd oo gen_add_consts (K I) false [];
    1.82 +fun add_consts args = snd o gen_add_consts Syntax.parse_typ false [] (map bindify args);
    1.83 +fun add_consts_i args = snd o gen_add_consts (K I) false [] (map bindify args);
    1.84  
    1.85  fun declare_const tags ((b, T), mx) thy =
    1.86    let
    1.87 -    val c = Name.name_of b;
    1.88      val pos = Name.pos_of b;
    1.89      val tags' = Position.default_properties pos tags;
    1.90 -    val ([const as Const (full_c, _)], thy') = gen_add_consts (K I) true tags' [(c, T, mx)] thy;
    1.91 -    val _ = Position.report (Markup.const_decl full_c) pos;
    1.92 +    val ([const as Const (c, _)], thy') = gen_add_consts (K I) true tags' [(b, T, mx)] thy;
    1.93 +    val _ = Position.report (Markup.const_decl c) pos;
    1.94    in (const, thy') end;
    1.95  
    1.96  end;
    1.97 @@ -557,14 +561,14 @@
    1.98  
    1.99  (* abbreviations *)
   1.100  
   1.101 -fun add_abbrev mode tags (c, raw_t) thy =
   1.102 +fun add_abbrev mode tags (b, raw_t) thy =
   1.103    let
   1.104      val pp = Syntax.pp_global thy;
   1.105      val prep_tm = no_frees pp o Term.no_dummy_patterns o cert_term_abbrev thy;
   1.106      val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
   1.107 -      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
   1.108 +      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Name.display b));
   1.109      val (res, consts') = consts_of thy
   1.110 -      |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode tags (c, t);
   1.111 +      |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode tags (b, t);
   1.112    in (res, thy |> map_consts (K consts')) end;
   1.113  
   1.114  fun revert_abbrev mode c = map_consts (Consts.revert_abbrev mode c);